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
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
Tristan Ravitch
620b6f5980
Plumb through a parameter for the semantics lookup function
...
This is the function that will be generated via TH for PPC32 and PPC64.
2017-10-03 11:55:40 -07:00
