1540 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Joe Hendrix	46be7aa52b	Implement new registerUse analysis. ... The new registerUse analysis uses a three phase process: Phase 1 computes invariants about the start state of each block. It will indicate when registers/stack locations store stack offsets, and where callee saved registers are stashed. It also memoizes information about stack reads and writes to simplify later passes. Phase 2 is a demand analysis that computes which registers and stack locations must be available to execute the program. It then propagates those constraints across blocks in the function. Phase 3 combines the information into a form relevant for function recovery.	2020-02-06 19:26:46 -08:00
Joe Hendrix	9433737292	Bump macaw base version	2020-02-06 19:16:23 -08:00
Joe Hendrix	0236aa5d9a	Introduce separate stack-analysis algorithm.	2020-02-06 19:16:23 -08:00
Sam Breese	a52698beae	Merge pull request #103 from GaloisInc/bmi2 ... Semantics for MULX from BMI2 and all of ADX	2020-02-03 16:13:26 -05:00
Andrei Stefanescu	16f80bde82	Merge branch 'master' into bmi2	2020-02-03 09:58:21 -08:00
Tristan Ravitch	e3aaf47a50	Tr/update submodules (#105) ... The main change here is in macaw-semmc to account for a change to the BVOrBits operation in Crucible.	2020-01-25 12:25:38 -08:00
Tristan Ravitch	d119a9ed5a	Update submodules (#104) ... The main change here is in macaw-semmc to account for a change to the BVOrBits operation in Crucible.	2020-01-17 16:17:30 -08:00
Tristan Ravitch	312274e2f3	Merge pull request #101 from GaloisInc/tr/update-crucible-dec19 ... Update the crucible submodule	2019-12-19 16:21:34 -08:00
Tristan Ravitch	6b490a8193	Update the crucible submodule ... The only real code change required is that simulation failure messages have an extra argument. The goal with this update is to pull in some fixes to the solver feature detection for yices in the latest crucible.	2019-12-19 15:03:09 -08:00
Samuel Breese	fb1611a127	Semantics for MULX from BMI2 and all of ADX	2019-12-19 10:43:54 -05:00
Tristan Ravitch	a744ca7a95	Merge pull request #95 from GaloisInc/tr/block-classifier-context-type ... Change the BlockClassifierContext in Discovery into a datatype (from …	2019-12-06 11:23:26 -08:00
Tristan Ravitch	c1d4155f3d	Merge branch 'master' into tr/block-classifier-context-type	2019-12-06 10:56:44 -08:00
Joe Hendrix	95c2a3026e	Merge pull request #97 from GaloisInc/jhx/dependency ... This adds dependency analysis from Reopt to macaw	2019-12-04 15:59:30 -08:00
Joe Hendrix	145bca4591	Add reopt dependency analysis to macaw.	2019-12-04 15:23:44 -08:00
Joe Hendrix	4f30c21c29	Merge pull request #89 from GaloisInc/jhx/jumptest ... Add testcase for non-zero index jumptable.	2019-12-04 15:22:24 -08:00
Joe Hendrix	1ed99917b4	Add testcase for non-zero index jumptable.	2019-12-04 14:31:45 -08:00
Tristan Ravitch	a21db268de	Merge pull request #96 from GaloisInc/tr/crucible-string-macaw-semmc ... Update macaw-semmc to work with crucible changes	2019-12-03 10:17:18 -08:00
Tristan Ravitch	62eb2deb1f	Update macaw-semmc to work with crucible changes ... The improved string support in Crucible adds a parameter to string reprs; this change accommodates that. Earlier changes added the necessary support in the rest of macaw.	2019-12-02 18:42:46 -08:00
Tristan Ravitch	4f56645ac8	Merge pull request #93 from GaloisInc/rwd/strings2 ... Update macaw-symbolic with changes to string literals in what4	2019-12-02 17:27:08 -08:00
Tristan Ravitch	5509548372	Change the BlockClassifierContext in Discovery into a datatype (from a tuple) ... I'm about to add a new field, and the 7-tuple was a bit confusing.	2019-11-27 11:57:13 -08:00
Rob Dockins	d068667ed8	Merge branch 'master' into rwd/strings2	2019-11-23 18:53:37 -08:00
Tristan Ravitch	b44e8c480f	Update the semmc submodule ... This brings it up to master. The submodule has some improvements to synthesis, but they changed some APIs.	2019-11-21 20:42:05 -08:00
Tristan Ravitch	9e9eb1b770	Fix macaw-ppc compilation ... Fixes #80, which removed a type parameter from `IntraJumpBounds`	2019-11-19 17:28:40 -08:00
Joe Hendrix	82350074ea	Merge pull request #87 from GaloisInc/jhx/jump-bounds ... Fix jump bounds to support non-zero indices.	2019-11-19 15:21:50 -08:00
Joe Hendrix	999d67168a	Update crucible	2019-11-19 14:54:29 -08:00
Joe Hendrix	df9b5bbe27	Support for offset jump tables.	2019-11-19 14:52:58 -08:00
Rob Dockins	13aefd82f2	Update macaw-symbolic with changes to string literals in what4	2019-11-15 14:39:38 -08:00
Tristan Ravitch	3da105d44e	Remove unused submodules ... We now use the hackage releases of these packages.	2019-11-12 18:13:00 -08:00
Tristan Ravitch	989cc65f7a	Move active submodules from submodules to deps ... This was an artifact of merging macaw-semmc into macaw. This commit unifies the two directories. There are some remaining submodules in the old directory: these are obsolete and will be removed in a separate commit.	2019-11-12 18:13:00 -08:00
Tristan Ravitch	4c7a69b11d	Update macaw-ppc to account for recent changes in macaw-base ... The main changes are: - `postCallAbsState` was removed from the architecture info - `mkInitialRegsForBlock` was renamed to `initialBlockRegs` and takes slightly different parameters - There is a new type family and some new functions in the architecture info relating to post-block/terminator abstract state construction PowerPC doesn't need any extra information to compute post-block abstract states, so we use () as the ArchBlockPrecond type.	2019-11-12 17:27:14 -08:00
Tristan Ravitch	1c5abc6728	Documentation updates in macaw-base	2019-11-12 17:27:14 -08:00
Andrew Kent	587aa7ea6b	Update crux/crucible code to use float mode reprs; bump submodules	2019-11-05 15:23:51 -08:00
Joe Hendrix	5bf14c21b0	Merge pull request #80 from GaloisInc/jhx/bounds-fix ... Jhx/bounds fix	2019-10-28 15:41:31 -07:00
Joe Hendrix	1cc36b4d0c	Propagate correct stack value after call.	2019-10-28 13:49:00 -07:00
Joe Hendrix	cf8c33398e	Additional exports; bounds pretty printing.	2019-10-28 13:47:59 -07:00
Joe Hendrix	bca1b3c711	Merge pull request #79 from GaloisInc/jhx/div ... Division changes	2019-10-22 16:32:52 -07:00
Joe Hendrix	4369c712ba	Fix macaw-x86-symbolic errors.	2019-10-22 08:28:16 -07:00
Joe Hendrix	7d7ec5ff01	Fix style; add comments	2019-10-22 08:07:50 -07:00
Joe Hendrix	1be68af2a0	Fix warnings.	2019-10-21 21:18:54 -07:00
Joe Hendrix	1596e9ca19	Update macaw-x86-symbolic for divmod changes.	2019-10-21 20:24:35 -07:00
Joe Hendrix	81d0469fbe	Group mod/div x86 functions.	2019-10-21 14:59:43 -07:00
Joe Hendrix	900488aa85	Merge pull request #78 from GaloisInc/jhx/register-use ... Generalizations to support reopt.	2019-10-21 14:17:57 -07:00
Joe Hendrix	d5a51ff9c3	Cleanups to jump bounds.	2019-10-17 23:33:57 -07:00
Joe Hendrix	26f29f3005	Generalizations to support reopt.	2019-10-16 13:57:19 -07:00
Joe Hendrix	9a112fcf0e	Merge pull request #76 from GaloisInc/jhx/absdomain-fix ... Remove spurius calls to error in AbsState bvsbb.	2019-10-03 14:20:57 -07:00
Joe Hendrix	d16f2b2ea0	Remove spurius calls to error in AbsState bvsbb.	2019-10-02 12:32:42 -07:00
Kevin Quick	74faea610a	Merge pull request #75 from GaloisInc/haddock_fix2 ... [base] Fix GHC 8.4.4 haddock	2019-10-01 21:56:32 -07:00
Kevin Quick	4536e9d33e	[base] Fix GHC 8.4.4 haddock	2019-10-01 14:09:18 -07:00
Joe Hendrix	8bc16d198a	Merge pull request #74 from GaloisInc/jhx/x86-deadcode ... AbsVal/x86 cleanups	2019-09-23 16:24:44 -07:00
Joe Hendrix	744424d28b	Remove unused X86PrimLoc.	2019-09-20 15:19:37 -07:00