Commit Graph

507 Commits

Author SHA1 Message Date
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
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
Daniel Wagner
5597b12c01 cleanup: test_bit_dynamic is now a defined function 2018-08-07 17:36:29 -04:00
Tristan Ravitch
feb2521a0b Silence a warning around the ipVal in TH-generated semantics code
Most instructions don't reference this variable, but it is in the signature of
every semantics function, leading to many unused variable warnings.  This commit
adds an underscore prefix to the variable name to silence the warning.
2018-07-26 22:07:15 -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
6bc8f9e835 Shuffle the Map/MapF import aliases for clarity and consistency 2018-07-26 14:36:37 -07:00
Tristan Ravitch
48b5aa405f Fix a warning w.r.t. StringExpr 2018-07-26 14:36:22 -07:00
Tristan Ravitch
981b775c7c Update submodules 2018-07-24 16:57:36 -07:00
Tristan Ravitch
7a512574dd x86: Fix a bug in the BinaryLoader implementation
The binary loader for x86_64/ELF was adding all symbol values as code discovery
roots.  We only want to add the addresses of code objects.
2018-07-09 17:26:42 -07:00
Tristan Ravitch
7e6dc9ee8c arm: Relax the base version bounds for macaw-arm 2018-07-08 22:28:58 -07:00