Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

-DO NOT ACCEPT- New memory model #5

Open
wants to merge 18 commits into
base: master
Choose a base branch
from
Open

-DO NOT ACCEPT- New memory model #5

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
51b248c
Fixed the assembly names of some instructions which produces
sdasgup3 Jan 31, 2019
07c5c3c
Merge branch 'master' into disambiguate_mnemonic_names
Andrew-Miranti Feb 2, 2019
7532c1d
Fix some missing opcodes
Andrew-Miranti Feb 3, 2019
956e1df
Make opcodes tokens
Andrew-Miranti Feb 4, 2019
df47ed7
Merge conflict resolve
Andrew-Miranti Feb 4, 2019
c43b75f
Changes to make decoder compile
Andrew-Miranti Feb 6, 2019
9b8787e
Minor syntax updates because I was getting strange kompile errors
Andrew-Miranti Feb 12, 2019
b64e647
The memory model migration begins. Removing lots of call sites into …
Andrew-Miranti Feb 12, 2019
54631d4
Hello World Works!
Andrew-Miranti Feb 16, 2019
9048f0a
Run-on-elf script added for automatically using the semantics on a el…
Andrew-Miranti Feb 20, 2019
ff7c42a
Finished run-on-elf.py
Andrew-Miranti Feb 23, 2019
b3fb4fa
New test case found issue with rel operands
Andrew-Miranti Feb 24, 2019
a3bef8f
Convert Immediate operand from Int or hexconstant to MInt
sdasgup3 Feb 25, 2019
5286c22
Woops
Andrew-Miranti Feb 28, 2019
4eaeb6a
Update to how relative jumps work, now consistent with disassembly fo…
Andrew-Miranti Mar 12, 2019
b757149
Use 0 rather than undefMInt for uninitialized memory
Andrew-Miranti Mar 14, 2019
5ce11ad
Merge in jump changes
Andrew-Miranti Mar 14, 2019
859a029
Ran most of the gcc torture tests. Have now lost the results for the…
Andrew-Miranti Apr 5, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
2 changes: 2 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,3 +7,5 @@
*.swo
semantics/underTestInstructions/*
semantics/x86-instructions-semantics.k
bin/
a.out
11 changes: 11 additions & 0 deletions docs/z3_artifcats/array2.z3
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(declare-const a3 (Array Int Int))
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(assert (not (= x y)))
(check-sat)
(get-model)
7 changes: 7 additions & 0 deletions docs/z3_artifcats/datatypes.z3
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
(declare-const p1 (Pair Int Int))
(declare-const p2 (Pair Int Int))
(assert (= p1 p2))
(assert (> (second p1) 20))
(check-sat)
(get-model)
9 changes: 7 additions & 2 deletions scripts/process_spec.pl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ BEGIN
"$home/Github/strata-data/data-regs/instructions/";
my $script = "~/x86-semantics/scripts/process_spec.pl";
my $UTInstructionsPath = "underTestInstructions/";

my $DECODER_DIR = "/home/andrewmiranti/Documents/University/Grad/decoder"; # TEMPORARY
my $help = "";
my $stratum = "";
my $readmod = "";
Expand Down Expand Up @@ -313,11 +313,16 @@ BEGIN
execute("mkdir -p $UTInstructionsPath");
createSingleFileDefn();
execute("git status x86-instructions-semantics.k");
# execute(
#"time kompile x86-semantics.k --syntax-module X86-SYNTAX --main-module X86-SEMANTICS --debug -v --backend $backend -I ~/Github/llvm-verified-backend/ -I ~/Github/llvm-verified-backend/common/x86-config/",
# 1
# );
execute(
"time kompile x86-semantics.k --syntax-module X86-SYNTAX --main-module X86-SEMANTICS --debug -v --backend $backend -I ~/Github/llvm-verified-backend/ -I ~/Github/llvm-verified-backend/common/x86-config/",
"time kompile x86-semantics.k --syntax-module ELF-SYNTAX --main-module X86-SEMANTICS --debug -v --backend $backend -I . -I ./common/ -I $DECODER_DIR",
1
);


exit(0);
}

Expand Down
32 changes: 32 additions & 0 deletions semantics/builtins.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
module BUILTINS
syntax Builtin ::= "putchar" [token]
| "getchar" [token]
| "printf" [token]
| "fprintf" [token]
| "sprintf" [token]
| "snprintf" [token]
| "scanf" [token]
| "fscanf" [token]
| "__isoc99_fscanf" [token]
| "sscanf" [token]
| "_IO_putc" [token]
| "fputc" [token]
| "fopen" [token]
| "freopen" [token]
| "fclose" [token]
| "fflush" [token]
| "fwrite" [token]
| "fread" [token]
| "fputs" [token]
| "puts" [token]
| "feof" [token]
| "fgetc" [token]
| "getc" [token]
| "fgets" [token]
| "gets" [token]
| "fseek" [token]
| "rewind" [token]
| "malloc" [token]
| "free" [token]
| "sqrt" [token]
endmodule
Loading