Commit Graph

1398 Commits

Author SHA1 Message Date
Kevin Quick
0ad281c853
[refinement] Implement determination of block transfer target addr(s). 2019-01-28 16:07:25 -08:00
Kevin Quick
9af8877cbd
[refinement] A block may transfer to multiple destinations (ite). 2019-01-28 15:18:32 -08:00
Kevin Quick
e5f1a60c88
[refinement] implement back-path builder. 2019-01-28 15:06:44 -08:00
Kevin Quick
dafc6252b4
[refinement] more haddock documentation for the Path module. 2019-01-28 15:05:47 -08:00
Kevin Quick
de06514a06
[refinement] Add pretty printer for FuncBlockPath. 2019-01-28 15:04:21 -08:00
Kevin Quick
87b3494f77
[refinement] add documentation for takePath function. 2019-01-28 15:02:43 -08:00
Kevin Quick
183ec2661d
[refinement] implement pathTo: find back-path to a specific block. 2019-01-28 15:01:46 -08:00
Kevin Quick
f9e179fb46
[refinement] Add MemWidth constraint. 2019-01-28 15:00:25 -08:00
Kevin Quick
53cf6acdf0
[refinement] sort/format imports for UnknownTransfer. 2019-01-28 14:58:05 -08:00
Luke Maurer
8d3c501fd0 Coerce PPCTermStmts rather than returning new ones when rewriting
This was eating up a surprising amount of heap space.
2019-01-28 14:48:25 -08:00
Luke Maurer
7d720b74f6 Add new crucGenRegStructType to MacawSymbolicArchFunctions for PPC 2019-01-28 14:48: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
bc5442a223 Force entire statement list when filtering it
Keeping it lazy meant that the entire list would stick around in memory
for a while; now the statements that aren't kept are garbage-collected.
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
Kevin Quick
138666b410
[refinement] a function may have multiple paths to different exit points.
An "exit point" is a block which does not transfer to another block
within the function.  An exit may be a RET or a JMP or an ite
representing different JMP targets; at this time it is assumed that
the latter cannot mix external and internal JMP targets.
2019-01-28 11:14:33 -08:00
Kevin Quick
263f852924
[refinement] Split out modules for Path handling, Function/Block utilities. 2019-01-28 10:50:35 -08:00
Kevin Quick
6412cd6312 [refinement] build trivial path (just initial block) 2019-01-26 13:34:01 -08:00
Kevin Quick
08c66d4b36
Merge branch 'refinement' of github.com:GaloisInc/macaw into refinement 2019-01-26 00:04:37 -08:00
Kevin Quick
9b4d8a8b04
[refinement] fill out more framework functions for path management. 2019-01-26 00:01:07 -08:00
Andrei Stefanescu
d0dd34a5bd [refinement] Initial setup for symbolic execution of a parsed block. 2019-01-25 22:46:57 -08:00
Kevin Quick
ab93845f00
[refinement] add process for refining an unknown transfer block.
Execution framework for determining the best refinement (if any) for a
particular block by extracting the CFG for that function and iterating
over successively larger paths leading to the unknown transfer block.

The core solution-generation via SMT/Crucible/What4 is still mocked out.
2019-01-25 16:04:55 -08:00
Kevin Quick
3b5e03122a
[refinement] iterate through unknown transfer failures to resolve
Updates the unknown transfer resolution module to iterate through the
set of blocks with unknown transfer results, attempting to refine the
unknown transfer failures recursively so that any newly discovered
blocks are also attempted (if necessary) and generating a (possibly
updated) DiscoveryState where any refined unknown transfer conditions
replace the original information.

Does not yet perform the actual refinement, just provides the
framework that would attempt to refine each unknown transfer.
2019-01-25 09:43:25 -08:00
Kevin Quick
f52d9214b0
[refinement] enable run-refinement to show refined discovery output. 2019-01-25 09:41:57 -08:00
Kevin Quick
16dfcaab0d
[refinement] Add initial refinement framework. 2019-01-24 14:49:47 -08:00
Tristan Ravitch
05249a4632 Change some calls to fail into translation errors
These `getCallTarget` and `doJump` were calling `fail` if they saw an argument
type that we hadn't thought to handle yet.  This change turns those errors into
TranslationError statements, allowing macaw to continue exploring code.

This came up recently in a glibc-based example where macaw ended up exploring
unaligned code and creating a strange jump to a far pointer, which doesn't make
much sense in x86_64 mode.
2019-01-23 13:22:03 -08:00
Kevin Quick
fb605a41d0
[refinement] update test generation and add refinement tests. 2019-01-23 12:04:41 -08:00
Kevin Quick
94402a4d47 Merge branch 'master' into refinement 2019-01-23 10:58:50 -08:00
Kevin Quick
e9511f956a Merge branch 'refinement' of localhost:work/SuitCASE/macaw into refinement 2019-01-23 10:58:02 -08:00
Kevin Quick
ab64d4698d
[refinement] add initial refinement framework calls. 2019-01-23 10:56:53 -08:00
Kevin Quick
1d9c6d7ae0
[refinement] Add 32-bit PPC support to tests. 2019-01-23 00:02:49 -08:00
Kevin Quick
74f6b11947
[refinement] add run-refinement support for 32-bit PPC. 2019-01-22 23:58:50 -08:00
Kevin Quick
522121b7d8
Update gitignore. 2019-01-22 23:46:33 -08:00
Kevin Quick
97bc56587c
[refinement] add per-block summary output to run-refinement tool. 2019-01-22 23:38:15 -08:00
Kevin Quick
63d24be712
[refinement] add binary versions of test samples. 2019-01-22 23:36:48 -08:00
Kevin Quick
fb869eedf7
[refinement] add some test sources to the test/samples. 2019-01-22 23:35:01 -08:00
Kevin Quick
db53801493 Merge branch 'master' of github.com:GaloisInc/macaw-semmc 2019-01-22 23:18:00 -08:00
Kevin Quick
4e32007436
[ppc] Use pretty representation for IP in error messages. 2019-01-22 23:17:24 -08:00
Tristan Ravitch
b0de116aa8 Update submodules
Includes a minor breaking change from macaw
2019-01-22 21:37:39 -08:00
Kevin Quick
08d4dcd832
[refinement] Add test framework to compare output to expected output. 2019-01-22 20:04:26 -08:00
Joe Hendrix
0451046cab
Merge pull request #22 from GaloisInc/jhx/exports
Additional exports
2019-01-22 16:26:38 -05:00
Joe Hendrix
a5e3ba7247
Additional exports 2019-01-22 15:51:38 -05:00
Joe Hendrix
ed05584dcf
Merge pull request #21 from GaloisInc/jhx/block-addr-removal
block addr removal
2019-01-22 14:21:25 -05:00
Joe Hendrix
3eb92f34e1
Add x86_tests 2019-01-22 13:25:37 -05:00
Joe Hendrix
6d1cc603d0
Merge remote-tracking branch 'public/jhx/minor-additions' into jhx/block-addr-removal
Also fixes some warnings.
2019-01-22 11:32:00 -05: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
23186a4991
Minor comments; fix stack.yaml 2019-01-22 05:36:17 -05:00
Joe Hendrix
0eac4d6b49
Remove blockAddr; update dependencies 2019-01-22 05:07:52 -05:00
Kevin Quick
fa891367ef Merge branch 'master' into refinement 2019-01-21 12:22:53 -08:00
Kevin Quick
7eabf2d01a
Handle additional side conditions returned by loadRawWithSideConditions. 2019-01-21 12:20:48 -08:00