Commit Graph

84 Commits

Author SHA1 Message Date
Joe Hendrix
e204724358
Merge pull request #27 from GaloisInc/jhx/vec
Add vector type and operations.
2019-02-27 08:57:50 -08:00
Joe Hendrix
89ffdf088a
Fix macaw-x86-symbolic and update crucible. 2019-02-27 01:43:53 -08:00
Joe Hendrix
e8d2efcaae
Implement bitcast changes to macaw-symbolic 2019-02-26 17:53:34 -08:00
Kevin Quick
70657ee811
[x86_symbolic] Use stable value for generating x86 register name.
Relying on the underlying Show instance representation for the
register name is more brittle, especially if the Show becomes a
structural representation (e.g. "X86_GP 14") that introduces spaces
and other elements that can cause problems.  Generate the register
name in a more reliable manner for the symbolic variable use case
here.
2019-02-23 21:52:36 -08:00
Joe Hendrix
3b7e12de16
Update to fix build process. 2019-02-15 00:28:35 -08:00
Andrei Stefanescu
f7f7b6cac3 Merge branch 'master' into refinement 2019-02-04 15:39:19 -08:00
Andrei Stefanescu
2620993d3c Add register lookup and update functions in X86 ArchVals. 2019-01-29 01:22:27 -08:00
Luke Maurer
5a8fba6d08 Cache TypeRepr and Position values
Generating the type of the register structure on demand was causing
`TypeRepr` to be the biggest chunk of the heap.  Similarly, we only need
to create a new `Position` when we change the offset.
2019-01-28 14:47:06 -08:00
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