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
Kevin Quick
190ed07121
[symbolic] add imports for mappend operator for GHC 8.2.2.
2019-01-12 18:10:16 -08:00
Kevin Quick
fb0d5c4776
Merge branch 'master' into refinement
2019-01-12 17:12:57 -08:00
Tristan Ravitch
379f89ee78
Update to the latest crucible version
...
The llvm memory model was extended with better diagnostics and configurable
handling of undefined behavior. macaw-symbolic uses no undefined behavior
checking, as those operations are only undefined in C.
2019-01-11 23:01:07 -08:00
Tristan Ravitch
7b57ac0c34
Additional haddocks
2019-01-11 13:58:15 -08:00
Tristan Ravitch
bda8ace256
symbolic: Clean up the memory mapping API
...
The API is now cleaner and includes more documentation (with an example). Some
unnecessary types are removed/combined.
2019-01-11 13:21:04 -08:00
Tristan Ravitch
81f8f5a849
Add an extra comment to the backend docs
2019-01-11 13:11:40 -08:00
Kevin Quick
7b50a38d30
Merge branch 'master' into refinement
2019-01-11 09:04:26 -08:00
