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
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
62d26946dc
merging because semmc is being weird
2017-10-16 11:38:38 -07:00
Tristan Ravitch
cc00389c44
[ppc] Update the PPC semantics
2017-10-13 17:05:45 -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
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
30ad3f6730
Update the dismantle submodule
2017-10-12 09:11:53 -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
157c2ce980
merging
2017-10-10 14:53:20 -07:00
Ben Selfridge
773d01b1cd
merging
2017-10-10 14:52:14 -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
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
Ben Selfridge
3a49345b15
Added Semantics directory, had forgotten to add it previously
2017-10-04 10:03:29 -07:00
Ben Selfridge
b234b673f9
Added addStmt to PPCGenerator monad
2017-09-29 15:37:41 -07:00
Ben Selfridge
65a7e8c17c
second commit
2017-09-29 09:37:45 -07:00
Ben Selfridge
bf9b320e38
first commit
2017-08-28 15:48:55 -07:00
