Commit Graph

62 Commits

Author SHA1 Message Date
Luke Maurer
68ae66bff5 NatRepr changes 2019-02-13 14:21:48 -08:00
Tristan Ravitch
f260dad575 Turn fail-stop errors into macaw translation failures
Previously, macaw-ppc (and macaw-arm) would call `error` if there were no
semantics available for a decoded instruction.  This was useful during initial
development, but it is a problem for deployment.  Now just turn missing
semantics into TranslationErrors, which appear as block terminators in macaw IR.

This will require more diligence in monitoring TranslationErrors for patterns
that need to be addressed.
2019-02-01 08:37:50 -08:00
Tristan Ravitch
b0de116aa8 Update submodules
Includes a minor breaking change from macaw
2019-01-22 21:37:39 -08:00
Tristan Ravitch
fa8a9c5403 Update to the latest macaw
This includes a minor change: a new required field for the blocks returned by
the machine-specific disassembler.  The information was already readily
available in this backend.
2019-01-10 22:26:36 -08:00
Tristan Ravitch
cfcc1fc0d4 Update to the latest macaw-symbolic
There was some API churn, mostly a few renames and new modules.
2019-01-10 18:23:19 -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
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
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
Kevin Quick
730f855c71
Update to use macaw-loader for uniform binary loading. 2018-10-29 15:51:42 -07:00
Tristan Ravitch
f1ac01edd9 Update to the latest macaw 2018-10-23 11:49:23 -07:00
Andrei Stefanescu
4b498807fd Handle floating-point rounding. 2018-09-12 11:10:23 -07:00
Andrei Stefanescu
dab4f92ed9 Use BVSelect instead of BVTrunc. 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
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
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
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
ebfae218a9 Include symbol values in the entry points list for x86 (when available) 2018-07-08 21:52:28 -07:00
Tristan Ravitch
aee4309c85 Merge branch 'master' of github.com:GaloisInc/macaw-semmc into HEAD 2018-07-03 17:53:41 -07:00
Tristan Ravitch
b417cec636 ppc: Update to the test_bit_dynamic changes in semmc-ppc
This splits test_bit_dynamic into a 32 bit case and a 64 bit case
2018-07-03 17:44:06 -07:00
Luke Maurer
3548613d3a Merge branch 'df' of github.com:GaloisInc/macaw-semmc into df 2018-07-03 13:13:32 -07:00
Luke Maurer
6477e710d4 Use "df_" rather than "_df_" as prefix for defined functions
The underscore squelches potentially useful warnings, since if a defined
function isn't being used, something is indeed wrong.
2018-07-03 13:10:06 -07:00
Luke Maurer
3a44feda6a Whitespace error 2018-07-03 12:23:36 -07:00
Luke Maurer
f6e58bbd47 Support defined functions in TH 2018-07-03 12:23:36 -07:00
Luke Maurer
633df42860 Enable caching in What4 expression builder
With caching disabled, we weren't doing any sharing recovery when
emitting Template Haskell. The cache in the `MacawQ` monad wasn't
helping because the expression builder generates a fresh nonce for each
expression it doesn't find in the cache; with no cache, every
subexpression was distinct from every other one.
2018-06-28 11:11:02 -07:00
Luke Maurer
457c8cec2e Enable caching in What4 expression builder 2018-06-28 10:12:04 -07:00
Luke Maurer
0b37eff77e Whitespace error 2018-06-26 11:35:50 -07:00
Luke Maurer
fbdae275cb Support defined functions in TH 2018-06-26 11:04:07 -07:00
Ben Selfridge
2427ddf048 fixed stack and used Data.Functor.Product instead of hand-rolled type 2018-05-24 14:09:49 -07:00
Tristan Ravitch
b15f360d25 Documentation updates 2018-05-21 17:53:01 -07:00
Tristan Ravitch
7cbd23dbf8 Add a generic interface for finding the entry points of a binary
Includes implementations for x86 and PowerPC 64/32
2018-05-20 21:41:21 -07:00
Tristan Ravitch
c228cca75c Merge branch 'master' of github.com:GaloisInc/macaw-semmc into HEAD 2018-05-18 15:28:59 -07:00
Tristan Ravitch
1ed8d66dc7 Improve the BinaryLoader interface
It is now (optionally) pure via the MonadThrow class.  It also exposes a new
binary format repr, which currently only has constructors for ELF containers.
2018-05-18 15:26:19 -07:00
Kevin Quick
f81f2437ee
Update for crucible reorganization and new what4 module. 2018-05-18 08:33:58 -07:00
Tristan Ravitch
27810cdbf3 Add a draft of a generic binary loading interface, simplify TOC handling on PPC
The generic binary loading interface is instantiated once for each
architecture/binary container pair.  This isn't great, but there is enough
custom work in each setting to justify it.

The binary loading interface isn't finished yet, and needs to learn some
additional operations to support relocation.  It already supports additional
information that is architecture specific and binary container format
specific (that operations will have to use on a per-format basis).

On the PowerPC side, the Table of Contents (TOC) is now architecture-specific
information constructed by the loader (currently from ELF binaries).  The new
TOC data type is in place to support this more easily (the old format was just a
function).
2018-05-17 16:03:04 -07:00
Tristan Ravitch
4bed676ca2 Update to the latest macaw 2018-04-24 10:55:07 -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
f959773cbd Emit the new 'ArchState' macaw statement
This change is in the core generator monad and applied in the PowerPC backend.
This change includes some macaw updates (which required a new elf-edit version).
2018-03-29 18:06:26 -07:00
Tristan Ravitch
ebd52aa11c Remove some unused imports 2018-03-29 11:18:56 -07:00
Tristan Ravitch
13c202f966 Add a comment to setRegVal 2018-03-29 10:01:06 -07:00
Kevin Quick
0c67eddda8
Unsupported functions (nonceAppEval) should error immediately.
Original version was pushing error into generated TH, which was
generating the error statement into the SSA formula; this breaks
formula interpretation at compile time but hides the error.  Instead,
this changes it so that the error is thrown during TH evaluation.
2018-03-10 10:04:03 -08:00
Kevin Quick
a3fe4a0f6b
Modify genExecInstruction to use functions for opcode semantics bodies.
Pass operand and architecture types and instead of

   case opcode of
      ADD -> case operands of
               Just GPR gpr0 :< Nil of ->
                   SSA-semantics

Generate:

    let opc_ADD operands = case operands of
                             Just GPR gpr0 :< Nil of ->
                                SSA-semantics
    in case opcode of
         ADD -> opc_ADD operand

This provides better encapsulation for the individual operands and
more specific control over the types (at the cost of a pair of
additional type specifications in the call).  This also seems to
reduce memory consumption by about half.
2018-03-05 16:02:17 -08:00
Tristan Ravitch
3a2b5ac3f2 Remove the case for BVURem
We don't have a constructor for this in macaw (it has to be an arch-specific function)
2018-03-01 14:48:14 -08:00