Kevin Quick
419b977d6b
Add the new function handle return type, used for recursion bounding.
2019-08-07 09:51:57 -07:00
Kevin Quick
2353ad9f6d
Merge branch 'master' into nonce_handle_deparameterize
2019-07-19 17:06:50 -07:00
Kevin Quick
48c3ba1fed
[symbolic] additional nonce-related adjustments from 'ST h' to 'IO'.
2019-07-19 09:40:24 -07:00
Kevin Quick
80de5d94e5
[symbolic] update for use of safe Nonce in crucible.
...
Update for compatibility with Crucible changes in
https://github.com/GaloisInc/crucible/pull/285 .
2019-07-19 00:13:00 -07:00
Kevin Quick
f525351621
Handle conversions for Float Mux in macaw-ppc.
2019-07-11 13:55:01 -07:00
Joe Hendrix
6a4b75852f
Fix missing case in macaw-symbolic
2019-05-30 23:39:38 -07:00
Joe Hendrix
c6a7ba7cd6
Rename pblock fields to be more descriptive.
2019-04-29 22:21:10 -07:00
Joe Hendrix
315cd2f9f0
Cleanups to macaw-symbolic
2019-04-29 21:30:59 -07:00
Joe Hendrix
70ea5b9036
Remove ParsedIte
2019-04-29 20:46:54 -07:00
Joe Hendrix
8aa4650683
Introduce ParsedBranch constructor.
2019-04-29 10:49:00 -07:00
Joe Hendrix
3331a19571
Drop support for branches within blocks.
2019-04-28 13:19:20 -07:00
Joe Hendrix
15676a2e45
Bump versions; Update macaw-symbol for conditional write.
2019-04-17 21:36:49 -07:00
Joe Hendrix
4267dca987
Get x86_symbolic test cases in runable state.
2019-03-25 20:29:35 -07:00
Joe Hendrix
82b96fb62a
Fix warnings; improve PLTStub comment.
2019-03-25 19:27:46 -07:00
Aaron Tomb
70981ba8ea
Initial attempt at adapting to structured errors
2019-03-06 10:26:41 -08:00
Iavor Diatchki
65ca5447ea
Merge branch 'master' of github.com:GaloisInc/macaw
2019-02-27 16:20:55 -08:00
Iavor Diatchki
1471740282
Only skip assignment if we are assigned to our own initial value.
2019-02-27 15:45:12 -08:00
Kevin Quick
45f5c5e7af
Update cabal version for fields used.
2019-02-27 11:52:18 -08:00
Kevin Quick
f8fce2175e
Sorting of pragma declarations in CrucGen.
2019-02-27 11:51:53 -08:00
Kevin Quick
b53b79471c
Add NondecreasingIndentation pragma to match code formatting.
2019-02-27 11:51:16 -08:00
Kevin Quick
60a3d39e98
More haddock updates for function argument information.
2019-02-27 11:35:20 -08:00
Kevin Quick
fcff1b7c3d
Update all source files for NoStarIsType pragma.
2019-02-27 11:35:09 -08:00
Kevin Quick
8ea677f7ed
[symbolic] Haddock fixes.
2019-02-27 09:30:55 -08:00
Kevin Quick
a1e6f1b841
Update NoStarIsType spec for backward compatibility.
2019-02-27 09:30:26 -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
b80ab8fb67
[symbolic] update to latest crucible.
2019-02-19 08:24:45 -08:00
Luke Maurer
b23ba5820d
CrucGen: Support for jump tables
...
This needed a bit more surgery than one would like, since we need to
translate the indirect jump to an if-else chain, which means creating a
bunch of "extra" blocks from within the `CrucGen` monad.
2019-02-15 18:35:25 -08:00
Tristan Ravitch
1d3610a783
Revert "Fill in undefineds with nonsense so pretty printing works"
...
This reverts commit 86ef62645d
2019-02-15 08:35:17 -08:00
Langston Barrett
274808a8ae
update parameterized-utils submodule
2019-02-11 11:47:19 -08:00
Kevin Quick
5f12c3da88
[symbolic] Remove unneeded debug import.
2019-02-08 17:31:30 -08:00
Kevin Quick
edb486c6b3
Added toCrucibleEndian in symbolic and use for memory setup in refinement.
...
Requires updated macaw-loader BinaryFormat information.
2019-02-08 17:30:18 -08:00
Andrei Stefanescu
45e4251bf3
[refinement] Add an unbounded memory allocation at the bottom of the allocation stack.
2019-02-07 17:23:02 -08:00
Andrei Stefanescu
cca17b1c39
[refinement] Handle a code address as an LLVM pointer.
2019-02-06 20:13:47 -08:00
Andrei Stefanescu
cb8245d009
Map each memory segment in the binary using a What4 array.
2019-02-05 20:53:40 -08:00
Andrei Stefanescu
f7f7b6cac3
Merge branch 'master' into refinement
2019-02-04 15:39:19 -08:00
Andrei Stefanescu
87fc7c5439
Fix termStmtToJump.
2019-02-04 13:36:48 -08:00
Andrei Stefanescu
595c98efb8
Add proper mkBlockPathCFG.
2019-02-01 16:13:35 -08:00
Andrei Stefanescu
8ee9196cf6
Add Crucible translation of block paths.
2019-01-31 21:48:44 -08:00
Andrei Stefanescu
620b54e5af
Handle all ParsedTermStmt constructors in termStmtToReturn.
2019-01-30 20:24:03 -08:00
Luke Maurer
957addd204
CrucGen: Use SetStruct rather than making a new one from scratch
...
This means far fewer instructions (and hence fewer registers), and in
turn a lot less heap space. Peak memory usage is cut in half running
Brittle on a PPC64 exe with standard library.
2019-01-29 10:37:38 -08:00
Luke Maurer
b049a52ae9
CrucGen: Cache BV<->Ptr conversions
...
There was a fair amount of churn in generated Crucible CFGs due to
values redundantly getting converted back and forth.
2019-01-29 10:01:36 -08:00
Andrei Stefanescu
533dc131a4
Add register lookup and update functions in ArchVals.
2019-01-29 01:21:25 -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
Luke Maurer
12daa3a17b
Make CrucGen stricter
...
Most crucially, make the `CrucGen` monad itself strict. The heap was
filling up with old `CrucGenState`s being held onto by unevaluated
computations, since *every* computation was lazy. Plugged a few other
sources of `CrucGenState` leaks as well.
2019-01-28 14:47:06 -08:00
Andrei Stefanescu
d0dd34a5bd
[refinement] Initial setup for symbolic execution of a parsed block.
2019-01-25 22:46:57 -08:00
Joe Hendrix
ab066e2743
Merge remote-tracking branch 'public/master' into jhx/block-addr-removal
2019-01-22 11:12:25 -05:00
Joe Hendrix
8bf0d00e66
Fix warnings; crucible changes.
2019-01-22 10:25:45 -05:00
Joe Hendrix
0eac4d6b49
Remove blockAddr; update dependencies
2019-01-22 05:07:52 -05:00
Kevin Quick
7eabf2d01a
Handle additional side conditions returned by loadRawWithSideConditions.
2019-01-21 12:20:48 -08:00
