Commit Graph

113 Commits

Author SHA1 Message Date
Tristan Ravitch
13def38f25 Fix some compilation errors with an improved evaluator in semmc 2017-10-17 21:38:53 -07:00
Tristan Ravitch
2a7c5bd541 Extend the uninterpreted function evaluator
It is currently very messy because the ppc.is_r0 function breaks some
abstraction boundaries that make it very irregular.  There is some common code
that can probably be factored out, but it will still be a mess.

The other big change is handling the read_mem calls.
2017-10-17 19:16:31 -07:00
Tristan Ravitch
eb8b78b372 Add support for a number of new uninterpreted functions
This covers evaluating all of the statically-evaluated functions in expression
contexts (e.g., is_r0 and the memory reference extraction functions).

The expansion seems pretty reasonable.

There are still some cases to handle w.r.t. floating point elementary functions
and memory reads and writes, which need to be handled a bit differently.

Note: we also have to call the formula simplifier soon.
2017-10-17 17:07:03 -07:00
Ben Selfridge
ccd344f027 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-17 12:32:40 -07:00
Ben Selfridge
0649ea4f0c Nearly done with semmc->macaw, need to complete addEltTH function 2017-10-17 12:27:57 -07:00
Tristan Ravitch
07c48afe46 Add instantiations for some uninterpreted functions
This covers functions that are used to isolate locations to be defined from
composite operands (e.g., the base registers of memrr and memri operands).
2017-10-17 11:51:11 -07:00
Tristan Ravitch
db2da637b0 Update the semmc submodule 2017-10-16 23:27:44 -07:00
Tristan Ravitch
cf0a6df0da Simplify the sequencing of our generated monadic PPCGenerator actions
We were building up a list and calling sequence; instead, just generate a single
do block directly
2017-10-16 19:51:32 -07:00
Ben Selfridge
1a5946bd0d Nearly done with semmc -> macaw, need to complete a few more cases 2017-10-16 16:40:51 -07:00
Ben Selfridge
e2121de437 Finished bound variable case in addEltTH 2017-10-16 15:53:28 -07:00
Ben Selfridge
17e44dae2a Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-16 15:37:49 -07:00
Ben Selfridge
fdf03c5c80 Rearranged a few things 2017-10-16 15:37:19 -07:00
Tristan Ravitch
792eb1aaf9 [ppc] Add a helper for turning operands into bitvectors
The main function is 'extractValue', which takes an operand and returns a macaw
bitvector for it (in the PPCGenerator monad).

There are still some missing cases for the memory operands.
2017-10-16 15:11:16 -07:00
Ben Selfridge
690687b0b6 started fixing up the BoundVar case 2017-10-16 14:15:12 -07:00
Ben Selfridge
62d26946dc merging because semmc is being weird 2017-10-16 11:38:38 -07:00
Ben Selfridge
ebe47b74fc work in progress TH translation 2017-10-16 11:35:12 -07:00
Tristan Ravitch
cc00389c44 [ppc] Update the PPC semantics 2017-10-13 17:05:45 -07:00
Ben Selfridge
d48f30f173 Filled out some TH stuff 2017-10-13 14:26:39 -07:00
Tristan Ravitch
1017c51ead Update the semmc submodule to include the FP base set 2017-10-13 14:20:22 -07:00
Ben Selfridge
80d0fb26a6 merging 2017-10-13 13:15:10 -07:00
Ben Selfridge
50884f8af8 merging 2017-10-13 13:14:58 -07:00
Tristan Ravitch
27a81db23f Update the semmc and dismantle submodules
These include changes necessary for floating point support
2017-10-13 11:42:00 -07:00
Tristan Ravitch
c770cb32f1 Update the semmc submodule 2017-10-12 18:12:29 -07:00
Ben Selfridge
6058c2ebec started template haskell stuff 2017-10-12 10:21:48 -07:00
Tristan Ravitch
b5ac6be425 Add some documentation and build some helpful maps for the TH translation 2017-10-12 10:11:16 -07:00
Tristan Ravitch
30ad3f6730 Update the dismantle submodule 2017-10-12 09:11:53 -07:00
Tristan Ravitch
90e66cd252 Update to the latest macaw changes 2017-10-11 21:04:04 -07:00
Tristan Ravitch
e5895833ba Plumb through most of the TH bits to generate 'execInstruction'
The remaining part is 'genCaseBody', which is where we'll write the translator
from ParameterizedFormula to TH Exps.  The semantics are loaded from semmc and
the outer case expression breaking down instructions is all in place.  This has
several accompanying changes in semmc and dismantle.
2017-10-11 18:07:56 -07:00
Ben Selfridge
54f5715c8b filled out locToReg 2017-10-10 15:37:22 -07:00
Ben Selfridge
157c2ce980 merging 2017-10-10 14:53:20 -07:00
Ben Selfridge
773d01b1cd merging 2017-10-10 14:52:14 -07:00
Ben Selfridge
b270a2b9a2 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-10 14:51:54 -07:00
Ben Selfridge
064d0c4e8d Added TestBit, done (for now) with crucible expressions 2017-10-10 14:51:25 -07:00
Ben Selfridge
d0fac23418 Fixed BVSelect a bit; need to re-examine type proofs 2017-10-10 14:35:00 -07:00
Ben Selfridge
578c1c0258 Completed BVConcat and BVSelect 2017-10-10 12:32:20 -07:00
Tristan Ravitch
3b27ccdf30 Update the semmc submodule 2017-10-10 11:50:57 -07:00
Tristan Ravitch
c0889aa8bb Enable formula loading in the TH entry point
Also update the semmc submodule to the required version.
2017-10-09 23:18:33 -07:00
Ben Selfridge
6db1a2d43c rewrote crucAppToExpr in applicative style 2017-10-09 16:07:52 -07:00
Ben Selfridge
b1cbc0548e Completed refactoring of Expr type. 2017-10-09 14:02:52 -07:00
Ben Selfridge
058963f8fe Changed Expr type to be non-recursive 2017-10-09 11:27:59 -07:00
Tristan Ravitch
c1566e7946 Fix an issue with formula loading
Also disable formula loading for now because it raises an exception due to some
unhandled constructs in the parser.
2017-10-06 22:14:34 -07:00
Tristan Ravitch
95361474ae Feed semantics to the genExecInstruction calls
These lists come from semmc and contain the bytestrings of the semantics files
for each opcode.

NOTE: The lists are currently empty (presumably due to bugs), but the logic for
moving data around and setting up a SimpleBuilder instance is at least right.
2017-10-06 16:58:53 -07:00
Tristan Ravitch
42db84f27b Update submodules 2017-10-06 10:05:43 -07:00
Tristan Ravitch
072571d219 Expand the initial abstract state for a block
We needed to note that the LNK register contains the return address
2017-10-04 17:01:56 -07:00
Tristan Ravitch
38cb6cdfd8 Add a note about TranslateError 2017-10-04 17:01:56 -07:00
Ben Selfridge
c76cd00e72 trying to fix git 2017-10-04 16:40:14 -07:00
Tristan Ravitch
0a974b1a15 Add the TH invocation to PPC32 2017-10-04 16:00:18 -07:00
Tristan Ravitch
1e55026ae5 Add a definition of absEvalArchFn
We'll have to expand this as we add functions
2017-10-04 15:55:28 -07:00
Tristan Ravitch
711eabc058 Implement postCallAbsState and absEvalArchStmt
absEvalArchStmt is trivial (for now)
2017-10-04 15:53:03 -07:00
Tristan Ravitch
ac776b7340 Remove a redundant export 2017-10-04 15:51:03 -07:00