Kevin Quick
898e7bdb95
[refinement] Added newline to end of expected output file.
2019-02-26 14:51:49 -08:00
Kevin Quick
3fe6fdf949
Sort refinement results for test stability and visual convenience.
2019-02-23 21:33:40 -08:00
Kevin Quick
3e7bd01560
[refinement] Disabled PPC switching test.
...
Attempting to refine the switching test for PPC executables ends up
with a non-terminating Z3 process, so this test is disabled until this
is diagnosed.
2019-02-08 17:32:21 -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
Kevin Quick
d3228847f7
[refinement] add PPC tests expected results.
2019-02-08 14:26:17 -08:00
Kevin Quick
6cb0868d1b
[refinement] import cleanup
2019-02-08 14:20:29 -08:00
Kevin Quick
290e33279a
[refinement] Enable PPC testing.
2019-02-08 14:10:08 -08:00
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
Andrei Stefanescu
9121f0a439
[refinement] Add llvm compiled binary files.
2019-02-07 16:20:24 -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
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
f22a33aefe
[refinement] Refine one function at a time.
2019-02-01 16:29:13 -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
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
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
Kevin Quick
375dd1d656
[refinement] disable PPC testing temporarily
2019-01-30 09:13:52 -08:00
Kevin Quick
1b99c43518
[refinement] run tests only over specified architectures.
2019-01-30 09:13:38 -08:00
Kevin Quick
ebde669a24
[refinement] group tests by name.
2019-01-30 09:12:02 -08:00
Andrei Stefanescu
2efd7bc0e6
Fixes.
2019-01-29 16:29:54 -08:00
Andrei Stefanescu
8bd3ea41d1
Merge branch 'refinement' of github.com:GaloisInc/macaw into refinement
2019-01-29 14:54:06 -08:00
Andrei Stefanescu
5115bce70b
Propagate MonadIO constraint.
2019-01-29 14:54:03 -08:00
Kevin Quick
d2913bb5fe
Merge branch 'refinement' of github.com:GaloisInc/macaw into refinement
2019-01-29 14:33:51 -08:00
Kevin Quick
9945a2898e
[refinement] some updates/fixes to FuncBlockPath building.
2019-01-29 14:33:15 -08:00
Kevin Quick
e410b88b36
[refinement] update FuncBlockPath data element haddocks.
2019-01-29 14:32:05 -08:00
