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
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
ebe47b74fc
work in progress TH translation
2017-10-16 11:35:12 -07:00
Ben Selfridge
d48f30f173
Filled out some TH stuff
2017-10-13 14:26:39 -07:00
Ben Selfridge
50884f8af8
merging
2017-10-13 13:14:58 -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
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
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
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
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
Tristan Ravitch
f12166c2c3
Add a trivial definition of the architecture-specific abstract evaluation function
2017-10-04 15:46:33 -07:00
Tristan Ravitch
ab29030e14
Implement the initial abstract state
2017-10-04 15:44:59 -07:00
Tristan Ravitch
6a14cfffb8
Implement archDemandContext
...
This required a few more instances and a wrapper around `ArchStmt`
2017-10-04 14:40:36 -07:00
Ben Selfridge
7e563acef8
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-04 14:09:02 -07:00
Ben Selfridge
bb0d7e7341
converting from crucible Elt type to Macaw Apps
2017-10-04 14:08:09 -07:00
Tristan Ravitch
57db5aa6f6
Add a definition of the jump table entry size
2017-10-04 13:26:08 -07:00
Tristan Ravitch
c02b0c605c
Add a trap arch-specific statement
2017-10-04 13:25:56 -07:00
Tristan Ravitch
7f8410ce7f
Fill in some previously undefined IP value calculations
2017-10-04 11:24:16 -07:00
Tristan Ravitch
af6ead250a
Add some documentation
2017-10-04 11:08:42 -07:00
Tristan Ravitch
20f078e9eb
Hook up the execInstruction functions
...
These are now referenced in the necessary spots in the ArchitectureInfo definitions
2017-10-04 10:16:54 -07:00
Tristan Ravitch
498ff33a6d
Finish the disassembler skeleton
...
There are still some IP values to compute, but the shape of the algorithm is there
2017-10-04 10:10:06 -07:00
Tristan Ravitch
047e84c586
Remove an unused import
2017-10-04 10:10:06 -07:00
Tristan Ravitch
48f556ffcb
Add some more helpers for the Generator monad
2017-10-04 10:10:06 -07:00
Tristan Ravitch
00f2b1d423
Add a context that we'll need
2017-10-04 10:10:06 -07:00
