Iavor Diatchki
89529ed7e3
Be more lenient when interpreting bogus expressions.
...
Previously we were asserting that some bogus-y things don't happen.
Unfortunately, these expressions can occur in code that was not
directly written by the user (e.g., comparisons for setting various
machine flags). To allow for that, we allow the expressions, but
give them undefined values. So the proof will succeed only if it
does not depend on the values of these bogus comparisons.
2018-03-07 10:22:46 -08:00
Iavor Diatchki
357a526589
Export symbol names, so can add interpretations to them.
2018-03-02 15:35:22 -08:00
Iavor Diatchki
df32ca44aa
Add a function for convenient lookup of Macaw registers in a Crucible asgn.
2018-03-02 11:35:47 -08:00
Iavor Diatchki
7c1992d991
There are only 12 FP status registers; 3 of the bits are for TOP, which is separate
2018-02-15 13:58:02 -08:00
Iavor Diatchki
b5995421ea
Port x86-symbolic to the new pointer representation
2018-02-12 13:27:57 -08:00
Iavor Diatchki
9200b2bcdd
Rename module, to avoid name class with module from macaw-x86
2018-01-31 14:41:45 -08:00
Iavor Diatchki
ef1d277c12
Make test build (but not yet function)
2018-01-30 15:55:22 -08:00
Iavor Diatchki
737d4fc0c5
Fix test (still does not work, but for other reasons)
2018-01-30 15:50:34 -08:00
Iavor Diatchki
1f62f90585
Export symFun creation functions
2018-01-30 15:50:20 -08:00
Iavor Diatchki
d70768fe1c
Add generation of uninterpreted functions for complex instructions.
2018-01-30 10:40:46 -08:00
Iavor Diatchki
01b9008d0f
Add uninterpreted functions for more complex instructions.
2018-01-29 17:50:33 -08:00
Iavor Diatchki
e92be789ab
Pass in the type intrinsics when evaluating.
2018-01-26 14:43:45 -08:00
Iavor Diatchki
3a240e9154
Even partiy + scaffolding for cariless multiplication.
2018-01-26 11:36:19 -08:00
Iavor Diatchki
54662612ea
The pointwise operations, so far.
2018-01-25 15:59:32 -08:00
Iavor Diatchki
6088ccc3dd
Pointwise shift
2018-01-25 15:54:08 -08:00
Iavor Diatchki
f2c8eace6c
Write shiffleD in the same style as the rest.
2018-01-25 15:38:58 -08:00
Iavor Diatchki
dc1bfacfa5
Some more operations
2018-01-25 15:29:47 -08:00
Iavor Diatchki
68cf758664
Fix shifting. Allow using big and little endian splits.
2018-01-24 17:08:02 -08:00
Iavor Diatchki
405f6779f1
Factor out common gunk
2018-01-24 15:15:00 -08:00
Iavor Diatchki
3f9bcd8461
Implement shffule
2018-01-24 15:02:43 -08:00
Iavor Diatchki
712537c421
Enough infrastructure to define one instruction.
2018-01-24 14:35:03 -08:00
Iavor Diatchki
da4f1b873e
Needs only Functor
2018-01-23 16:02:38 -08:00
Iavor Diatchki
04408c595a
Move semantics function to a separate module.
...
This is yet to be defined.
2018-01-23 16:01:50 -08:00
Iavor Diatchki
1b359da739
Define a pretty printer, and appT
2018-01-23 15:28:20 -08:00
Iavor Diatchki
8d4e940bb7
More simplifications; revert back to original.
...
It would appear that once the lifted wrapper functions were
in places, the types happen to match.
2018-01-23 15:09:38 -08:00
Iavor Diatchki
aed0e53342
Simplify TraversableFC instace, add FunctorFC
2018-01-23 14:38:27 -08:00
Iavor Diatchki
66ad7e521b
Define the traversableFC instance.
2018-01-23 14:30:29 -08:00
Joe Hendrix
d1bdff9866
Additional code for macaw-symbolic.
2018-01-22 16:58:33 -08:00
Joe Hendrix
365aa7fb39
Additional macaw-symbolic progress.
2018-01-22 16:38:17 -08:00
Joe Hendrix
8b97faa731
More progress on Macaw symbolic; compile fixes for Macaw changes.
2018-01-22 15:28:20 -08:00
Joe Hendrix
1ffd97b0b9
Update macaw-symbolic to work with AVX code.
2018-01-16 15:42:36 -08:00
Joe Hendrix
48001ea6f1
Add updated flexdis constraints.
2018-01-16 15:37:30 -08:00
Joe Hendrix
b7e06e64ee
Progress on macaw-symbolic and macaw-x86-symbolic.
2018-01-16 15:06:31 -08:00
Joe Hendrix
824b245eaa
Add macaw-x86-symbolic
2018-01-02 22:50:23 -08:00
