Commit Graph

519 Commits

Author SHA1 Message Date
Kevin Quick
d4c7f1f457
[macaw-arm] initial (incomplete) implementation of checkForReturnAddr.
The ArchitectureInfo checkForReturnAddr is used to check if a specific
value corresponds to the symbolic "ReturnAddr", indicating that the
target is the original call location (this is used to identify
tail-call recursion or identify that a return has been performed from
the primary function via identifyReturn).

The current implementation simply checks for ReturnAddr in the Link
Register (LR), but it needs to be enhanced to detect ARM semantic
manipulation of ReturnAddr (clearing the low bit(s), etc.).
2018-12-14 15:06:37 -08:00
Kevin Quick
294299a8eb
[macaw-ppc] ArchitecturInfo updates: mkInitialRegsForBlock, checkForReturnAddr. 2018-12-13 22:48:26 -08:00
Kevin Quick
f63f9972eb
[macaw-semmc] Update test imports to avoid import warnings. 2018-12-13 16:56:16 -08:00
Kevin Quick
a53c88f88e
[macaw-arm] Update for new Macaw Memory function names.
The old names are deprecated in favor of the new naming scheme; no
functionality change.
2018-12-13 16:55:15 -08:00
Kevin Quick
dae9104fb9
[macaw-arm] Add mkInitialRegsForBlock and update instr to Seq.
For latest macaw-base.
2018-12-13 16:48:01 -08:00
Tristan Ravitch
83b8d6787a Merge branch 'master' of github.com:GaloisInc/macaw-semmc into HEAD 2018-12-09 15:57:50 -08:00
Tristan Ravitch
8776a1fa5d Improve error reporting in TH generated semantics
There was an error case in function interpretation in the TH generated
code (when a function couldn't be evaluated for a given operand).  This
shouldn't happen for well-formed code, but can be a problem when macaw finds
invalid code that happens to decode as a real instruction (with an invalid
operand).

The old code called error, which caused macaw to fail with a hard stop.  This
commit changes the call to be to `fail` instead, which fires off an exception
that is properly handled (giving us a ClassifyFailure instead).
2018-12-09 15:55:45 -08:00
Kevin Quick
28afd098e4 Additional updates for fix to issue 15. 2018-12-03 23:20:19 -08:00
Kevin Quick
a75d9ea7aa Fix syntax error from previous change. 2018-12-03 22:47:33 -08:00
Daniel Wagner
718467815b fix GaloisInc/semmc/issues/15
We now thread a snapshot of the register state from the beginning of the
instruction evaluation through each instruction's semantics instead of
re-fetching register values each time we need it and potentially seeing
incorrect, partially modified register values.
2018-12-03 17:34:18 -05:00
Tristan Ravitch
72040c023d Fix handling of InstructionStart
The field it contains is supposed to be the instruction offset in its basic
block; overflowing it can cause significant problems during symbolic simulation.
2018-11-28 20:26:58 -08:00
Tristan Ravitch
30b5d2e091 Update macaw-arm and macaw-ppc to emit extra metadata
There is a new metadata statement that tracks the start address of each
instruction.  This is used in the translation to Crucible to provide better
error messages.  The x86 backend was already updated, this commit adds the
metadata to the ARM and PowerPC backends.
2018-11-28 10:22:25 -08:00
Tristan Ravitch
95091a5fb3 Submodule updates 2018-11-27 13:57:36 -08:00
Tristan Ravitch
f2f1698f4e Add macaw-ppc-symbolic to cabal.project 2018-11-27 13:57:20 -08:00
Andrei Stefanescu
76ff48eec0 Propagate changes for X86_64 RepMovs and RepStos. 2018-11-27 10:31:03 -08:00
Tristan Ravitch
fa570e0c1a Merge branch 'master' of github.com:GaloisInc/macaw-semmc 2018-11-25 08:40:25 -08:00
Tristan Ravitch
d64a1fc5be Stop generating NOINLINE pragmas for individual instruction semantics functions
Benchmarking shows that the NOINILINE pragma actually makes compile times
longer
2018-11-25 08:39:44 -08:00
Kevin Quick
0731c5c686
Add MonadFail for Generator for GHC 8.6 2018-11-20 23:37:21 +00:00
Tristan Ravitch
c0df904033 Submodule updates
The code already depended on these, but the submodules were a bit out of date
2018-11-09 23:43:31 -08:00
Nathan Collins
0d3c00e744 Move stack.yaml to stack-ghc-8.2.yaml
To avoid conflicting stack.yaml files when crucible is used a
submodule in another repo with a top level stack.yaml.

Also, update the README to include creating a stack.yaml symlink
before building with stack the first time.
2018-10-30 16:16:16 -07:00
Tristan Ravitch
ff79eba6aa ppc: Use the new HasTOC class
This avoids a hard dependency on the exact format of ArchBinaryData for PowerPC
2018-10-30 11:01:46 -07:00
Tristan Ravitch
ebcbbe6c5c Remove the BinaryAddrWidth type family 2018-10-30 10:34:56 -07:00
Kevin Quick
d464403a25
Update tests from deprecated relativeSegmentAddr to segoffAddr. 2018-10-29 15:55:41 -07:00
Kevin Quick
d05deabef2 Added macaw-loader submodule. 2018-10-29 15:54:25 -07:00
Kevin Quick
730f855c71
Update to use macaw-loader for uniform binary loading. 2018-10-29 15:51:42 -07:00
Tristan Ravitch
ee58037c2d Make the powerpc tests more verbose when encountering a translation error 2018-10-24 10:26:55 -07:00
Tristan Ravitch
f1ac01edd9 Update to the latest macaw 2018-10-23 11:49:23 -07:00
Andrei Stefanescu
f3f2732663 Fix PPC SBVToFloat translation. 2018-09-19 18:45:50 -07:00
Andrei Stefanescu
1c002f160b Minor fixes. 2018-09-18 21:56:17 -07:00
Andrei Stefanescu
32961d20cb Use name instead of nonce id for uninterpreted functions. 2018-09-14 19:01:27 -07:00
Andrei Stefanescu
85ef5b4f0b Add float le and float round. 2018-09-14 19:01:19 -07:00
Andrei Stefanescu
4b498807fd Handle floating-point rounding. 2018-09-12 11:10:23 -07:00
Andrei Stefanescu
5acc20cdb2
Merge pull request #2 from GaloisInc/floating-point
Add floating-point to PPC.
2018-09-06 14:52:26 -07:00
Andrei Stefanescu
b0c98ccc5c Use op name as argument instead of uninterpreted function name. 2018-09-06 14:47:37 -07:00
Andrei Stefanescu
dab4f92ed9 Use BVSelect instead of BVTrunc. 2018-09-06 14:47:37 -07:00
Andrei Stefanescu
f448a4ae9f Add symbolic semantics to PPC floats. 2018-09-06 14:47:37 -07:00
Andrei Stefanescu
2886c86e2b Add floats to Macaw-PPC. 2018-09-06 14:47:37 -07:00
Andrei Stefanescu
54e33d8f5c Add float helpers in Macaw-SemMC. 2018-09-06 14:47:37 -07:00
Kevin Quick
932b3df9ff
[ppc-symbolic] Update LLVM memory model pointer import for newer crucible. 2018-08-27 15:25:37 -07:00
Kevin Quick
8c437abf51
[arm] Add notes for disassembly process and ISETSTATE management. 2018-08-22 15:05:51 -07:00
Tristan Ravitch
9605843388 Update submodules
The code was updated to deal with the latest changes to crucible (the addition
of the floating point unit type parameter), but the submodules for this repo
were not.
2018-08-21 18:30:52 -07:00
Tristan Ravitch
0da0c6c73b Merge branch 'master' of github.com:GaloisInc/macaw-semmc 2018-08-20 22:28:19 -07:00
Tristan Ravitch
c718b41dc6 arm: Add a test with mixed ARM and Thumb code 2018-08-20 22:28:04 -07:00
Andrei Stefanescu
09443f5bed
Merge pull request #1 from GaloisInc/latest-crucible
Update macaw-ppc and macaw-arm to use the latest crucible
2018-08-17 15:48:01 -07:00
Andrei Stefanescu
fcf39588e1 Update macaw-ppc and macaw-arm to use the latest What4.ExprBuilder. 2018-08-16 20:20:50 -07:00
Tristan Ravitch
f7b87224a4 Update to the latest macaw
In macaw core, the type of the arch-specific 'disassemble' function changed to
no longer take a Memory, and to pass the maximum offset as an Int instead of a
MemWord.  It also removed the jump table entry size (which is no longer
required).

The removal of the Memory parameter required a bit of a change in how the
instruction parsers are structured, but it isn't a huge change (the "memory
contents after an address" can be computed from a MemSegmentOff, too).
2018-08-16 10:26:55 -07:00
Tristan Ravitch
d5cab147e5 Remove some GHC optimization flags
The goal with these flags was to improve compile times by reducing the number of
times that the simplifier runs.  It seems like that sometimes causes compiler
errors (e.g., the register allocator crash we hit sometimes) - presumably the
register allocator makes some assumptions about how much the simplifier is run.
2018-08-14 20:32:57 -07:00
Tristan Ravitch
70f4943ba1 Update to the latest semmc 2018-08-14 16:17:51 -07:00
Kevin Quick
c10f18de6b
Submodule update for crucible, dismantle, macaw, and semmc. 2018-08-10 15:51:09 -07:00
Kevin Quick
75aee53b79
[arm] Update tests for new memoryForElf returns. 2018-08-10 15:47:56 -07:00