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
Tristan Ravitch
eec7075b46
Implement catchError in a MonadError instance
2017-10-04 10:10:06 -07:00
Ben Selfridge
3a49345b15
Added Semantics directory, had forgotten to add it previously
2017-10-04 10:03:29 -07:00
Ben Selfridge
5de25b8906
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-04 10:00:04 -07:00
Tristan Ravitch
9b8a7bac21
Remove an unused module
...
The rewriters are now in the Arch module
2017-10-04 08:48:52 -07:00
Tristan Ravitch
a851cddebd
Add arch-specific decls + type instances + rewriters
...
This also lets us add 'withArchConstraints' easily.
2017-10-03 18:59:35 -07:00
Tristan Ravitch
8a1195b1c6
Fill in the AddrWidthReprs for PPC
2017-10-03 18:07:21 -07:00
Tristan Ravitch
d1c86fd6d4
Remove unused imports
2017-10-03 18:07:15 -07:00
Tristan Ravitch
c751e02e6c
Use a ConstraintKind to simplify a number of constraint contexts
2017-10-03 18:05:46 -07:00
Tristan Ravitch
adf8a46f91
Implement more of the PPCGenerator state
2017-10-03 18:00:54 -07:00
Tristan Ravitch
2ec88811c5
Add special purpose registers to the definition of 'RegisterInfo'
2017-10-03 16:37:01 -07:00
Tristan Ravitch
171cc0d5ca
Remove an unused module
2017-10-03 16:31:41 -07:00
Tristan Ravitch
4a8828429c
Implement 'RegisterInfo' for PPCReg
2017-10-03 16:31:16 -07:00
Ben Selfridge
ad8d5fc3b4
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-03 14:43:33 -07:00
Tristan Ravitch
dc261436c7
Generalize the type of PPCReg
...
The width of a GPR was formerly fixed to 64 bits. It now reflects the actual arch.
2017-10-03 13:40:11 -07:00
Tristan Ravitch
5e136dceec
Let PPCGenerator report errors
...
It doesn't right now, but the translation from semantics to macaw will have some
opportunities around invalid encodings.
2017-10-03 13:39:59 -07:00
Tristan Ravitch
19b65973fc
Apply the state transformer
...
Committing now to experiment with adding failure modes to PPCGenerator
2017-10-03 13:23:20 -07:00
