Tristan Ravitch
cc85cfe657
Clean up and document the macaw-symbolic API
...
This cleanup consolidates the interface to macaw symbolic into two (and a half)
modules:
- Data.Macaw.Symbolic for clients who just need to symbolically simulate
machine code
- Data.Macaw.Symbolic.Backend for clients that need to implement new
architectures
- Data.Macaw.Symbolic.Memory provides a reusable example implementation of
machine pointer to LLVM memory model pointer mapping
Most functions are now documented and are grouped by use case. There are two
worked (compiling) examples in the haddocks that show how to translate Macaw
into Crucible and then symbolically simulate the results (including setting up
all aspects of Crucible). The examples are included in the symbolic/examples
directory and can be loaded with GHCi to type check them.
The Data.Macaw.Symbolic.Memory module still needs a worked example.
There were very few changes to actual code as part of this overhaul, but there
are a few places where complicated functions were hidden behind newtypes, as
users never need to construct the values themselves (e.g., MacawArchEvalFn and
MacawSymbolicArchFunctions). There was also a slight consolidation of
constraint synonyms to reduce duplication. All callers will have to be updated.
There is also now a README for macaw-symbolic that explains its purpose and
includes pointers to the new haddocks.
This commit also fixes up the (minor) breakage in the macaw-x86-symbolic
implementation from the API changes.
2019-01-10 18:20:54 -08:00
Kevin Quick
98807daee2
Added -Wcompat for warnings about future compatibility.
2019-01-10 13:43:27 -08:00
Luke Maurer
46cdd8be82
Adapt to Nonce-based registerized CFGs
2019-01-03 12:10:24 -08:00
Andrei Stefanescu
3f39c614e9
Add support for RepMovs and RepStos.
2018-11-27 02:23:36 -08:00
Kevin Quick
3c7e222676
Add missing import for previous change.
2018-11-26 11:26:01 -08:00
Kevin Quick
b92f008676
Merge branch 'master' of github.com:GaloisInc/macaw
2018-11-25 23:53:28 -08:00
Kevin Quick
3f8769a424
[x86_symbolic] add semantics for X86Div, X86Rem, X86IDiv, and X86IRem.
2018-11-25 22:02:18 -08:00
Kevin Quick
01b8175e7f
[x86_symbolic] Update cabal specification for compliance.
2018-11-25 22:01:40 -08:00
Kevin Quick
0ee3f7df2d
[x86_symbolic] more info for unimplemented statement and termstmt semantics.
2018-11-25 22:00:19 -08:00
Kevin Quick
3f77e763e9
Implement NoStarIsType for GHC 8.6.
2018-11-21 18:27:42 +00:00
Kevin Quick
6212a69233
[x86] Add semantics for sqrtss and sqrtsd.
2018-10-31 11:46:01 -07:00
Tristan Ravitch
563547fee5
Add semantics for minss, maxss, minsp, and maxsp (x86)
2018-10-23 15:18:40 -07:00
Andrei Stefanescu
59b756c185
Add symbolic semantics for X86 sse_ucomis and sse_cvttsx2si.
2018-09-19 18:47:47 -07:00
Andrei Stefanescu
c5f0806751
Add symbolic semantics to X86 SSE floats.
2018-09-18 22:07:17 -07:00
Brian Huffman
a3d7376179
Adapt to changed crucible-llvm exports.
2018-08-27 16:16:32 -07:00
Brian Huffman
c29d4c924a
Merge branch 'master' into saw-script
2018-08-27 10:27:00 -07:00
Kevin Quick
5f4ca911e0
Update for interleave and Endian from Data.Parameterized.
2018-08-25 16:18:57 -07:00
Brian Huffman
a33202b583
Adapt to changes in crucible-llvm package.
2018-08-20 16:38:20 -07:00
Joe Hendrix
3ec8a34893
Fix Crucible symbol name error.
2018-07-21 14:14:42 -07:00
Joe Hendrix
564c94a744
Fix missing case.
2018-07-21 14:14:31 -07:00
Joe Hendrix
dc4a4f0f5f
Merge remote-tracking branch 'public/stable' into jhx-x86-improvements
2018-07-20 20:32:09 -07:00
Rob Dockins
f14222e4a4
Update to track crucible API changes
2018-07-20 18:41:54 -07:00
Joe Hendrix
2184fab0bc
Update macaw-symbol tests so they at least compile.
2018-07-20 10:07:49 -07:00
Joe Hendrix
494f6c176d
Updates to Macaw.
2018-06-06 11:48:45 -07:00
Rob Dockins
f74d999896
Bump crucible submodule again
2018-05-17 14:06:24 -07:00
Rob Dockins
c382b59bed
Bump crucible submodule to pull in crucible/what4 split refactor,
...
and update macaw-symbolic and macax-x86-symbolic.
2018-05-15 15:58:14 -07:00
Tristan Ravitch
aee0e1dee6
x86-symbolic: Translate statements and terminators into crucible
...
Note: the interpretations for symbolic execution are *not* implemented yet
2018-05-10 07:58:29 -04:00
Rob Dockins
643989f4b6
Update Macaw libraries for recent Crucible changes
2018-05-02 17:21:26 -07:00
Joe Hendrix
9047cb41fb
Fix warnings in macaw-base; Fix errors in macaw-symbolic.
...
This also makes some changes to eliminate a couple redundent
type-class constraints in CrucGen.hs which propagated to other changes.
2018-04-24 01:17:03 -07:00
Joe Hendrix
265f61e206
Merge branch 'master' of github.com:GaloisInc/macaw
2018-03-29 16:30:29 -07:00
Joe Hendrix
007405db1d
Improve robustness of elf loader, and start trying to parse relocations in objects.
2018-03-29 15:21:31 -07:00
Iavor Diatchki
1a22cf0a90
Correct implementation of vpalignr
2018-03-27 15:28:46 -07:00
Iavor Diatchki
0f3b97b8bf
Definition for Unpack
2018-03-27 10:46:47 -07:00
Iavor Diatchki
cb9cef128e
Implement vpinsrq and structore for the rest of the vector insert instruction
2018-03-26 13:17:03 -07:00
Iavor Diatchki
789322f9c8
Call error explicitly, so that we know what needs implementing.
2018-03-23 17:44:41 -07:00
Iavor Diatchki
79a4cdf39e
Add support for forcing allocation of fresh bits (as opposed to pointer/bits)
2018-03-22 13:11:22 -07:00
Iavor Diatchki
81aeca9e0b
Generate a fresh value for a register.
2018-03-20 19:04:00 -07:00
Iavor Diatchki
9c7070f8e6
Haddock comments fixes, thanks to Brian
2018-03-09 09:51:55 -08:00
Iavor Diatchki
53dca44cc0
Add a function to update a register assignment.
2018-03-08 17:17:14 -08:00
Iavor Diatchki
07e52b16ce
Revert back to the previous order of indexing.
...
This matches the Intel spec, and seems to match manual tests.
2018-03-08 15:06:10 -08:00
Iavor Diatchki
82e1dc0ebc
Add shift right for vectors.
2018-03-08 11:20:41 -08:00
Iavor Diatchki
ae54d2e078
Bit 4 seems to be for the 1st argument, and bit 0 for the snd.
2018-03-07 17:07:00 -08:00
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
