Commit Graph

24 Commits

Author SHA1 Message Date
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
Kevin Quick
d53ad182e8
Add genExecInstructionLogging and genExecInstructionLogStdErr.
Allows generatino of exec instructions with logging output to stderr
or another designated location, which can be useful for diagnostic
purposes.
2018-02-22 15:54:35 -08:00
Kevin Quick
ef503793b7
Show unsupported Crucible elt in error message. 2018-02-20 08:46:57 -08:00
Kevin Quick
c94f02d071
Add semantics support for BVUrem operation. 2018-02-20 08:43:55 -08:00
Kevin Quick
22bbdf7ee7
Common ExtractValue instances for sharing amongst architectures. 2018-02-07 11:34:38 -08:00
Ben Selfridge
5cf4c68498 Fixed a bug I introduced because of a delete in the wrong buffer 2018-01-05 14:23:11 -08:00
Tristan Ravitch
b7359957bf Remove the Witness type and related constraint magic
This change uses ShapeReprs, and requires changes from dismantle and semmc
2017-12-17 21:29:17 -08:00
Tristan Ravitch
f1b0775be8 Update to the new parameterized-utils List
This replaces the old ShapedList from dismantle-tablegen
2017-12-13 21:56:29 -08:00
Tristan Ravitch
269c329b93 Factor out the rest of the architecture-independent code
The PowerPC bits are now in macaw-ppc and the rest now lives in macaw-semmc.
2017-12-10 20:53:03 -08:00
Tristan Ravitch
7bcc90c83d Start migrating shareable TH code from macaw-ppc to macaw-semmc
This change still needs some work, but no other code depends on it yet
2017-12-06 17:28:23 -08:00
Tristan Ravitch
7256fd597f Generalize the generator monad, the TH helper monad, and the simplifier
This code was mostly architecture independent already, so this commit moves it
to the macaw-semmc module so that it can be shared with the ARM backend.  I
still plan to move the main TH module with the SimpleBuilder to macaw
translation, but that requires a few other changes first.
2017-11-26 23:31:04 -08:00
Ben Selfridge
65a7e8c17c second commit 2017-09-29 09:37:45 -07:00
Ben Selfridge
bf9b320e38 first commit 2017-08-28 15:48:55 -07:00