Commit Graph

297 Commits

Author SHA1 Message Date
Joe Hendrix
cc2d09a07d
Use type synonym to clarify argument for including BSS. 2018-02-20 16:37:26 -08:00
Joe Hendrix
d8cc235368
Fix bug in loading Elf sections with no data. 2018-02-20 16:28:54 -08:00
Iavor Diatchki
6cafcdf254 More verbose failures. 2018-02-20 11:53:18 -08:00
Joe Hendrix
3e8e01f582
Merge remote-tracking branch 'public/mem-model' into mem-model 2018-02-19 16:11:47 -08:00
Joe Hendrix
0f6d030c86
Initialize variable for storing registers before use. 2018-02-19 12:48:59 -08:00
Iavor Diatchki
22fbaf9d4f Change the types of the patterns, so that matching allows us to learn the type 2018-02-15 17:03:30 -08:00
Iavor Diatchki
7c1992d991 There are only 12 FP status registers; 3 of the bits are for TOP, which is separate 2018-02-15 13:58:02 -08:00
Iavor Diatchki
b8aa67918b Assocaite global memory varaible name with its value. 2018-02-13 16:44:35 -08:00
Iavor Diatchki
470182dccb Only pass around the memory var during execution, not CFG generation. 2018-02-13 10:14:22 -08:00
Iavor Diatchki
b5995421ea Port x86-symbolic to the new pointer representation 2018-02-12 13:27:57 -08:00
Iavor Diatchki
ad5f7ceddb Add write operation 2018-02-12 10:28:39 -08:00
Iavor Diatchki
b57483b1f8 Start on writeMem 2018-02-09 16:59:42 -08:00
Iavor Diatchki
1c07b88ae7 Implement conditional read. 2018-02-09 15:30:06 -08:00
Iavor Diatchki
3c2fdeafe4 Implement reading from memory. 2018-02-09 14:13:39 -08:00
Iavor Diatchki
c772eb31f4 Derive Show instance for Endianness 2018-02-09 14:12:57 -08:00
Iavor Diatchki
86c730043e Cleanup pointer manipulation operations. 2018-02-09 11:41:39 -08:00
Iavor Diatchki
c7bb8d87c4 More memory model. 2018-02-08 16:49:42 -08:00
Iavor Diatchki
561d211972 Get started on integrating the LLVM memory model. 2018-02-06 16:47:13 -08:00
Iavor Diatchki
9200b2bcdd Rename module, to avoid name class with module from macaw-x86 2018-01-31 14:41:45 -08:00
Iavor Diatchki
ef1d277c12 Make test build (but not yet function) 2018-01-30 15:55:22 -08:00
Iavor Diatchki
737d4fc0c5 Fix test (still does not work, but for other reasons) 2018-01-30 15:50:34 -08:00
Iavor Diatchki
1f62f90585 Export symFun creation functions 2018-01-30 15:50:20 -08:00
Iavor Diatchki
d70768fe1c Add generation of uninterpreted functions for complex instructions. 2018-01-30 10:40:46 -08:00
Joe Hendrix
e3a1b35307
Fix macaw-x86 tests. 2018-01-29 23:19:50 -08:00
Joe Hendrix
5f219026ec
Update submodules 2018-01-29 20:14:42 -08:00
Joe Hendrix
197a0b3ed1
Add additional utilities and flexibility for loading elf files. 2018-01-29 18:18:39 -08:00
Joe Hendrix
220dc5bb48
Merge branch 'master' of github.com:GaloisInc/macaw 2018-01-29 17:58:54 -08:00
Iavor Diatchki
01b9008d0f Add uninterpreted functions for more complex instructions. 2018-01-29 17:50:33 -08:00
Joe Hendrix
7e144a51f4
Memory interface renamings. 2018-01-29 11:05:19 -08:00
Joe Hendrix
e1e558239e
Minor cleanups. 2018-01-29 01:06:59 -08:00
Joe Hendrix
ca7ab08124
Merge branch 'master' of github.com:GaloisInc/macaw 2018-01-29 00:22:54 -08:00
Joe Hendrix
cbbec5378c
Haddock improvements; some module reoganization. 2018-01-29 00:20:54 -08:00
Iavor Diatchki
5959bfc6f0 Merge branch 'master' of github.com:GaloisInc/macaw 2018-01-26 14:43:50 -08:00
Iavor Diatchki
e92be789ab Pass in the type intrinsics when evaluating. 2018-01-26 14:43:45 -08:00
Daniel Wagner
c6dcd09738 regression tests for splitting blocks mid-instruction 2018-01-26 14:09:01 -08:00
Daniel Wagner
fbe716607f fix segment equality check 2018-01-26 14:09:01 -08:00
Daniel Wagner
dfa21bc40a modify tail-call test
Previously, we asked macaw to discover three functions in the tail-call
test. One of those only ever appeared as a tail call from another
function; currently macaw isn't smart enough to discover that as its own
function (and that's probably okay for now).
2018-01-26 14:09:01 -08:00
Daniel Wagner
293b13cc47 check that the expected functions are all discovered 2018-01-26 14:09:01 -08:00
Iavor Diatchki
3a240e9154 Even partiy + scaffolding for cariless multiplication. 2018-01-26 11:36:19 -08:00
Iavor Diatchki
9cf05f6f29 Slight improvement to pretty printing. 2018-01-26 11:35:58 -08:00
Iavor Diatchki
a7b5ac73ec Fix comment 2018-01-26 11:35:42 -08:00
Daniel Wagner
fc76fd5dc0 split blocks when we discover a jump into their middle 2018-01-26 10:18:31 -08:00
Daniel Wagner
d61e6d4a7f give an expected block size in x86_64 tests 2018-01-26 10:18:31 -08:00
Iavor Diatchki
54662612ea The pointwise operations, so far. 2018-01-25 15:59:32 -08:00
Iavor Diatchki
6088ccc3dd Pointwise shift 2018-01-25 15:54:08 -08:00
Iavor Diatchki
f2c8eace6c Write shiffleD in the same style as the rest. 2018-01-25 15:38:58 -08:00
Iavor Diatchki
dc1bfacfa5 Some more operations 2018-01-25 15:29:47 -08:00
Iavor Diatchki
68cf758664 Fix shifting. Allow using big and little endian splits. 2018-01-24 17:08:02 -08:00
Iavor Diatchki
405f6779f1 Factor out common gunk 2018-01-24 15:15:00 -08:00
Iavor Diatchki
3f9bcd8461 Implement shffule 2018-01-24 15:02:43 -08:00