Tristan Ravitch
ffaa912b74
Convert from applicative to nested binds in the TH code
...
This makes the generated splices much easier to read, which will be helpful for debugging.
2017-10-18 22:40:53 -07:00
Tristan Ravitch
28b7b68881
Fill out more of the PPC semantics translation
...
This covers all of the floating point used so far, as well as memory operations.
Note that this commit relies on changes that aren't pushed to macaw yet.
2017-10-18 17:48:07 -07:00
Tristan Ravitch
d893ce8dcb
Fix the BVConcat translation
2017-10-18 17:47:29 -07:00
Tristan Ravitch
601ea06e07
Fix a TH bug
...
We were generating a literal TH expression when we meant to generate a splice
2017-10-18 17:46:47 -07:00
Tristan Ravitch
344b253bf8
Add missing cases for the XER reg
2017-10-18 17:42:42 -07:00
Tristan Ravitch
f2f3b33fca
Convert floating point round to single precision
2017-10-18 17:42:42 -07:00
Ben Selfridge
74b5d85beb
Added test skeleton, rearranged some TH stuff
2017-10-18 14:27:29 -07:00
Tristan Ravitch
ace4520846
Update to the latest macaw
2017-10-18 10:29:57 -07:00
Tristan Ravitch
49545299d9
Add cases for FP operation translation
2017-10-18 08:49:09 -07:00
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
