Kevin Quick
3eeaed08a2
Merge branch 'master' of github.com:GaloisInc/macaw
2019-02-08 08:30:26 -08:00
Andrei Stefanescu
c67e474a19
[refinement] Move symbolic execution code in its own module.
2019-02-07 19:43:58 -08:00
Andrei Stefanescu
5b93187d5b
[refinement] Update .cabal file.
2019-02-07 17:25:52 -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
Kevin Quick
33540121f5
Merge branch 'master' of github.com:GaloisInc/macaw
2019-02-07 17:15:24 -08:00
Kevin Quick
3baf55376b
[refinement] update run-refinement for summary and verbose modes.
2019-02-07 17:15:00 -08:00
Andrei Stefanescu
ec9acfc1e1
[refinement] Add llvm compiled ppc64 binary files.
2019-02-07 17:00:10 -08:00
Kevin Quick
e47887a9f1
[refinement] add note to sample input for refinement tests.
2019-02-07 16:43:11 -08:00
Kevin Quick
3c6492b6fb
[refinement] add additional comment and showsearch info to RefinementTests.
2019-02-07 16:41:34 -08:00
Kevin Quick
94bfcc9654
Merge branch 'refinement'
2019-02-07 16:40:39 -08:00
Kevin Quick
35a16c587b
Merge branch 'master' of github.com:GaloisInc/macaw
2019-02-07 16:36:54 -08:00
Andrei Stefanescu
9121f0a439
[refinement] Add llvm compiled binary files.
2019-02-07 16:20:24 -08:00
Andrei Stefanescu
6da8c69374
[refinement] Add llvm compiled binary files.
2019-02-07 16:19:18 -08:00
Kevin Quick
59b55dd10a
[refinement] Update README for tests/samples.
2019-02-07 16:15:49 -08:00
Kevin Quick
35ff0c18ab
[refinement] Added nested switch/case test source.
2019-02-07 16:14:12 -08:00
Kevin Quick
7bb72b4b19
[refinement] Update expected refined test results for switching.x86.
...
The tests/samples/switching.c example now gets refined successfully so
this updates the expected file for that output.
2019-02-07 16:09:23 -08:00
Kevin Quick
2454ee25fc
[refinement] Track all solutions and ensure latest function is analyzed.
...
For each discovered transfer refinement, the Discovery process must be
re-started from scratch for the particular target function in
question. The implication is that subsequent refinements for the same
nominal function must use the newer version, and that all previous
refinements must be re-applied each time the function Discovery
process is repeated.
These changes ensure that both of these occur during the refinement
iterations.
2019-02-07 15:54:39 -08:00
Andrei Stefanescu
0d66b159e1
[refinement] Map model pointers back to addresses.
2019-02-07 01:09:59 -08:00
Andrei Stefanescu
cca17b1c39
[refinement] Handle a code address as an LLVM pointer.
2019-02-06 20:13:47 -08:00
Kevin Quick
2fadfcc05a
[refinement] Update run-refinement for Refinement use of loaded elf info.
2019-02-06 20:10:11 -08:00
Kevin Quick
13224a91ce
[refinement] updates for merge of Some removal and updateDiscovery.
2019-02-06 17:58:21 -08:00
Kevin Quick
36a8be1c4e
Merge branch 'refinement' of github.com:GaloisInc/macaw into refinement
2019-02-06 17:51:21 -08:00
Kevin Quick
eb3bc794c1
[refinement] Add ability to updateDiscovery for new targets.
...
After the SMT evaluation has identified possible targets for a
previously unknown transfer TermStmt, the updateDiscovery will update
the DiscoveryState (using a locally-supplied TermStmt rewriter) to
resolve the transfer targets.
2019-02-06 17:47:18 -08:00
Kevin Quick
5136973565
[base] remove unneeded import.
2019-02-06 17:44:46 -08:00
Kevin Quick
166af1bd20
[base] documentation updates.
2019-02-06 17:43:56 -08:00
Kevin Quick
03e48c7baf
[base] Add external TermStmt Rewriter capability.
...
The caller (e.g. macaw-refinement) can provide an additional Rewriter
operation that can operate on TermStmts for blocks (typically those
for which a previous Discovery was unable to determine a transfer
target). There is an additional
entrypoint ('addDiscoveredFunctionBlockTargets') that will allow this
additional rewriter to be supplied for updating an existing
DiscoveryState.
2019-02-06 17:41:40 -08:00
Kevin Quick
a4e1a58a98
[base] code simplification and removal of widely scoped variable.
2019-02-06 17:38:58 -08:00
Kevin Quick
83a1b2fb4c
[base] Allow the Rewriter to generate additional blocks.
...
Some of the TermStmt and other elements might generate new blocks as
part of the Rewrite operation (e.g. adding a new 'Branch' TermStmt) so
this change allows the rewrite context to update the generated block
labels and collect these newly generated blocks for inclusing in the
results passed to the parser.
2019-02-06 17:36:04 -08:00
Kevin Quick
7ead2c0247
[refinement] Use BlockLabel and StatementLabel type aliases.
...
Both map to Word64 but the named aliases clarify which is intended to
be used where.
2019-02-06 14:42:11 -08:00
Andrei Stefanescu
72c54dcf15
[refinement] Remove traceM statement.
2019-02-05 21:31:13 -08:00
Andrei Stefanescu
3aae34297f
[refinement][first version] Get successor candidates for classification failure blocks.
2019-02-05 21:08:13 -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
Kevin Quick
d9ee884a90
Documentation/comment fixes.
2019-02-03 10:57:01 -08:00
Andrei Stefanescu
f22a33aefe
[refinement] Refine one function at a time.
2019-02-01 16:29:13 -08:00
Andrei Stefanescu
595c98efb8
Add proper mkBlockPathCFG.
2019-02-01 16:13:35 -08:00
Kevin Quick
beb0f95c0b
[refinement] Provide list of forward path blocks to smt solving.
...
Currently smt solving just uses the first block of the first path,
which is not correct, but the framework for providing the list of
paths is now present.
2019-02-01 00:17:03 -08:00
Kevin Quick
2cbccd768c
Merge branch 'refinement' of github.com:GaloisInc/macaw into refinement
2019-01-31 22:29:59 -08:00
Kevin Quick
f282ac6913
[refinement] remove uneeded case catchall.
2019-01-31 22:29:31 -08:00
Kevin Quick
f60b39162c
[refinement] whitespace formatting.
2019-01-31 22:29:14 -08:00
Kevin Quick
243f70c9e6
[refinement] explicitly import Prelude last to avoid unneeded import errs.
2019-01-31 22:27:59 -08:00
Andrei Stefanescu
1e2e9aaee0
[refinement] Use mkBlockPathCFG.
2019-01-31 21:50:38 -08:00
Andrei Stefanescu
8ee9196cf6
Add Crucible translation of block paths.
2019-01-31 21:48:44 -08:00
Kevin Quick
5c2e0edeaa
[refinement] implement getBlock block lookup function.
2019-01-31 17:44:43 -08:00
Kevin Quick
bd0e57cfc1
[refinement] Invoke SMT solution at path-focused framework location.
...
The previous implementation invoked the SMT solver at the top level
for prototyping. This version moves the SMT solver invocation to the
intended location in the algorithm where the path is successively
extended and solutions are compared to identify the "best" refinement
solution.
2019-01-31 17:10:48 -08:00
Kevin Quick
ff2ec55f2c
[refinement] update run-refinement tool for changes in library.
...
Additional constraints and the refinement operations are now run in a
MonadIO context.
2019-01-31 14:55:26 -08:00
Andrei Stefanescu
23d67998ce
[refinement] Test finding successors for a single unclassified macaw block.
2019-01-30 20:27:35 -08:00
Andrei Stefanescu
620b54e5af
Handle all ParsedTermStmt constructors in termStmtToReturn.
2019-01-30 20:24:03 -08:00
Kevin Quick
9ba5473302
[refinement] only run refined tests if specified.
...
This prevents refined validation tests from causing problems with base
tests when only the latter is being run.
2019-01-30 09:14:22 -08:00
