Commit Graph

282 Commits

Author SHA1 Message Date
Kevin Quick
e35acdcb19
Minor comment fixup. 2018-03-01 10:59:11 -08:00
Kevin Quick
84eb0a0a80 Revert "Add BVUrem App support."
This reverts commit 6a0a59e298.

Do not want to add BVUrem because divide by zero can cause an
exception and this will greatly increase the complexity for analysis.
2018-03-01 10:57:28 -08:00
Kevin Quick
6a0a59e298
Add BVUrem App support. 2018-02-21 20:39:57 -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
Iavor Diatchki
62ae9ae130 Merge branch 'master' of github.com:GaloisInc/macaw 2018-01-24 14:35:08 -08:00
Iavor Diatchki
712537c421 Enough infrastructure to define one instruction. 2018-01-24 14:35:03 -08:00
Joe Hendrix
cfeabfde05
Minor cleanups. 2018-01-24 10:49:12 -08:00
Joe Hendrix
c1d82cdfc4
Merge branch 'master' of github.com:GaloisInc/macaw 2018-01-23 16:07:38 -08:00
Joe Hendrix
b3cd6fd049
Fix loop in X86 bvUle simplification. 2018-01-23 16:06:54 -08:00
Iavor Diatchki
da4f1b873e Needs only Functor 2018-01-23 16:02:38 -08:00
Iavor Diatchki
04408c595a Move semantics function to a separate module.
This is yet to be defined.
2018-01-23 16:01:50 -08:00
Iavor Diatchki
d0deaf055f Merge branch 'master' of github.com:GaloisInc/macaw 2018-01-23 15:28:25 -08:00
Iavor Diatchki
1b359da739 Define a pretty printer, and appT 2018-01-23 15:28:20 -08:00
Joe Hendrix
679108d73e
Merge branch 'master' of github.com:GaloisInc/macaw 2018-01-23 15:17:12 -08:00
Joe Hendrix
e94689bd7a
Continued macaw-symbolic progress. 2018-01-23 15:16:26 -08:00
Iavor Diatchki
8d4e940bb7 More simplifications; revert back to original.
It would appear that once the lifted wrapper functions were
in places, the types happen to match.
2018-01-23 15:09:38 -08:00
Iavor Diatchki
aed0e53342 Simplify TraversableFC instace, add FunctorFC 2018-01-23 14:38:27 -08:00
Iavor Diatchki
000dc189f8 Merge branch 'master' of github.com:GaloisInc/macaw 2018-01-23 14:30:34 -08:00
Iavor Diatchki
66ad7e521b Define the traversableFC instance. 2018-01-23 14:30:29 -08:00