Commit Graph

95 Commits

Author SHA1 Message Date
Joe Hendrix
fbb3b300ce
Prep work to get building with warning as errors. 2019-03-25 14:39:33 -07:00
Kevin Quick
a1278e3b92
[macaw-arm] Add test semigroup import for GHC 8.2. 2018-12-14 15:54:20 -08:00
Kevin Quick
642882396b
Build tests using the locally-available gcc arm binary name. 2018-12-14 15:09:47 -08:00
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
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
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
Kevin Quick
8c437abf51
[arm] Add notes for disassembly process and ISETSTATE management. 2018-08-22 15:05:51 -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
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
Kevin Quick
75aee53b79
[arm] Update tests for new memoryForElf returns. 2018-08-10 15:47:56 -07:00
Kevin Quick
454c219b27
[arm] Provide initial IPAlignment implementation. 2018-08-10 15:47:17 -07:00
Kevin Quick
0be37eb737
[arm] Added documentation for ARMReg constructors. 2018-08-10 15:46:08 -07:00
Kevin Quick
031a03a7c9
[arm] Update for Word32 Thumb GPR initialization and register count. 2018-08-10 15:41:22 -07:00
Tristan Ravitch
e1c04f1b5a arm: Fix a compile error
The UnexpectedRelocation constructor changed recently
2018-07-26 22:02:39 -07:00
Tristan Ravitch
ff80d7e676 Improve the TH generator for instruction matchers (i.e., execInstruction)
The previous generator put all of the code for each matcher in a single large
case expression.  While there were individual functions broken out for each case
body, they were all still in the same let expression, which created a huge term.

This refactoring lifts all of the semantics definition bodies to the top
level (with NOINLINE pragmas) to give the code generator less to chew on at a
time.

This improves compile times a little, but, more importantly, works around a bug
in the register allocator in GHC 8.4 that caused a crash in the PowerPC
semantics functions.
2018-07-26 17:17:09 -07:00
Tristan Ravitch
7e6dc9ee8c arm: Relax the base version bounds for macaw-arm 2018-07-08 22:28:58 -07:00
Luke Maurer
47d9d61998 Remove now-unnecessary optimization flags
The spliced TH code has gotten small enough that running multiple
iterations of the simplifier isn't horrible.
2018-07-03 12:24:34 -07:00
Luke Maurer
eaca69e13b Use defined functions to generate TH for ARM 2018-07-03 12:23:36 -07:00
Daniel Wagner
b7ec429874 add alignment information for PPC64 2018-06-01 15:35:41 -04:00
Ben Selfridge
6a5524e464 Fixed macaw-arm bound variable for UF bug 2018-06-01 10:23:34 -07:00
Kevin Quick
138db42d15 [arm] Remove unneeded import. 2018-05-22 13:18:31 -07:00
Kevin Quick
30296f081c [arm] Update for semmc renaming from ARM to AArch32. 2018-05-22 13:18:05 -07:00
Kevin Quick
f81f2437ee
Update for crucible reorganization and new what4 module. 2018-05-18 08:33:58 -07:00
Tristan Ravitch
4bed676ca2 Update to the latest macaw 2018-04-24 10:55:07 -07:00
Tristan Ravitch
1f10c1d36b arm: Update the tests to work with the latest macaw 2018-04-09 15:07:17 -07:00
Tristan Ravitch
b7c3118070 Update the calls to asAtomicStateUpdate
The type of the instruction address changed
2018-03-30 10:52:58 -07:00
Tristan Ravitch
dd655680f7 arm: Use asAtomicStateUpdate to generate a new macaw metadata statement 2018-03-30 09:10:41 -07:00
Tristan Ravitch
b051143e53 arm: Remove unused imports 2018-03-30 09:10:31 -07:00
Tristan Ravitch
d7b0ad9862 arm: Update macaw-arm to compile with the latest macaw (and macaw-semmc) 2018-03-30 09:08:49 -07:00
Kevin Quick
c3f2d13092
[arm] Implement identifyReturn (not properly functional).
The Macaw Discovery now calls the identifyReturn to identify return
statements.  Supply this for ARM, but at present this simply
replicates the original inline code which does not properly detect ARM
return operations because the low bit(s) of the address are always
cleared when writing to the instruction pointer in ARM.
2018-03-27 10:52:50 -07:00
Kevin Quick
9e0c325400
[arm] Fail disassembly if readInstruction returns 0 bytes consumed
Without this check this condition could cause the disassembly to
recurse until all system memory is exhausted.
2018-03-26 16:05:34 -07:00
Kevin Quick
80886bd73d
[arm] Add support for Thumb THINT uninterpreted function. 2018-03-26 16:04:34 -07:00
Kevin Quick
0069d3c907
[arm] Add ExtractValue for Maybe of Thumb LowGPR operand. 2018-03-11 10:54:33 -07:00
Kevin Quick
b0205af9ff
[arm] Added ExtractValue for Thumb AddrModeIs4 operand. 2018-03-11 10:34:44 -07:00
Kevin Quick
c50f01efef
[arm] Added test exe and results for test-just-exit-t32. 2018-03-10 21:55:29 -08:00
Kevin Quick
5e72398ef2
[arm] Add support for the Thumb Reglist operand. 2018-03-10 10:05:52 -08:00
Kevin Quick
1bceb8dc32
[arm] Update for change in export of numGPR from semmc-ppc. 2018-03-10 10:03:01 -08:00
Kevin Quick
491c302bfb
[arm] Add support for ARM Thumb TImm01020S4 operand. 2018-03-07 14:48:34 -08:00
Kevin Quick
ca2c54a98f [arm] Simplification of instruction decode selection wrapping. 2018-03-07 10:19:55 -08:00
Kevin Quick
af590fc7db
[arm] Add support for imm5 operand type. 2018-03-07 10:07:51 -08:00
Kevin Quick
cf9b6c5a30
[arm] Updated disassemble operation to support A32 or T32 block disassembly. 2018-03-07 10:06:29 -08:00
Kevin Quick
acb8812d68
[arm] Fix non-semantics instruction matcher to return Nothing when unrecognized. 2018-03-07 00:42:01 -08:00