Andrei Stefanescu
5115bce70b
Propagate MonadIO constraint.
2019-01-29 14:54:03 -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
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
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
Kevin Quick
f2b98011ce
Use initSimContext to create a Crucible SimContext.
...
This helps to immunize against changes in SimContext... e.g. the
addition on the profilingMetrics field that initSimContext provides a
default value for.
2019-01-21 12:20:00 -08:00
Nathan Collins
86ef62645d
Fill in undefineds with nonsense so pretty printing works
2019-01-17 14:25:59 -08:00
Kevin Quick
82f4b15a02
Merge branch 'master' into refinement
2019-01-16 10:36:44 -08:00
