1546 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Daniel Wagner	95dd08bce9	Merge branch 'master' into wip/equiv	2020-02-04 12:21:51 -05: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
Daniel Wagner	c22f140a3b	Merge branch 'tr/new-macaw-symbolic-entry' into wip/equiv	2020-01-13 22:21:51 -05:00
Daniel Wagner	b5c15af0da	start on alternative memory model	2020-01-13 22:11:40 -05:00
Daniel Wagner	e5daa87dd0	fix typo in comment	2020-01-13 22:10:17 -05: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
Tristan Ravitch	b76bfdb395	Add a new entry point to macaw-symbolic ... This version constructs a Crucible CFG for a collection of blocks while preserving control flow between them. It allows the caller to specify blocks that are considered "terminal": those blocks return the current register state. Control flow to blocks no included in the "slice" are directed to synthetic blocks that assume False in order to stop the symbolic simulator from exploring those branches.	2019-12-19 11:21:05 -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
Daniel Wagner	8d275627ba	export a few handy internals	2019-10-30 16:07:21 -04: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
Daniel Wagner	10a1fbc24a	misc. build fixes	2019-10-17 16:38:16 -04: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