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
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
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
Andrei Stefanescu
8eaa0ba377
[refinement] Use flat memory model.
2019-01-29 12:16:21 -08:00
Andrei Stefanescu
d826b6989a
Merge branch 'refinement' of github.com:GaloisInc/macaw into refinement
2019-01-29 01:25:09 -08:00
Andrei Stefanescu
aac908a595
[refinement] Generate IP candidate for single basic block.
2019-01-29 01:23:37 -08:00
Andrei Stefanescu
2620993d3c
Add register lookup and update functions in X86 ArchVals.
2019-01-29 01:22:27 -08:00
Andrei Stefanescu
533dc131a4
Add register lookup and update functions in ArchVals.
2019-01-29 01:21:25 -08:00
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
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
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
