Commit Graph

246 Commits

Author SHA1 Message Date
Luke Maurer
fedf457e02 Support defined functions in PPC32; use all defined functions in PPC 2018-06-29 10:53:48 -07:00
Luke Maurer
33a4805b01 Support for defined functions in PPC64 2018-06-28 15:44:06 -07:00
Tristan Ravitch
cad178cd62 ppc: Fix identifyReturn
Some recent semantics fixes broke a fragile pattern in identifyReturn; there is
now an extra shiftR.
2018-06-14 14:57:32 -07:00
Daniel Wagner
04e867bf4b future-proof alignment detection 2018-06-12 14:18:19 -04:00
Daniel Wagner
9874e6db20 IP alignment rulesfor PPC 2018-06-11 10:36:18 -04:00
Daniel Wagner
9e8279e70c fix alignment detection to match updated extract definition 2018-06-08 11:50:36 -04:00
Daniel Wagner
b7ec429874 add alignment information for PPC64 2018-06-01 15:35:41 -04:00
Tristan Ravitch
9664914923 Update the PowerPC tests to deal with the latest macaw-semmc changes
The new binary loading interface does manage to simplify things
2018-05-21 14:32:29 -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
796e8bc29e ppc: Generalize some error handling around the TOC 2018-05-18 19:31:18 -07:00
Tristan Ravitch
d6c2446a00 Whitespace 2018-05-18 17:52:18 -07:00
Tristan Ravitch
c4118b9fff Clean up the TOC function implementation 2018-05-18 17:50:02 -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
7d306f052d Export more details from macaw-ppc 2018-05-03 16:40:58 -07:00
Tristan Ravitch
6747f0ed44 Generalize the HasRepr instance for PPCPrimFn 2018-05-03 10:00:53 -07:00
Tristan Ravitch
05061a2140 Add a PrettyF instance for PPCReg 2018-05-03 09:46:46 -07:00
Tristan Ravitch
4bed676ca2 Update to the latest macaw 2018-04-24 10:55:07 -07:00
Tristan Ravitch
8f4865e106 Haddock fixes 2018-04-10 10:27:29 -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
76eb501d45 ppc: Improve the register pretty printer 2018-03-29 18:07:25 -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
716092eef1 ppc: Improve the test suite
Now test to ensure that no blocks end in a classification failure (or a
disassembly failure).  Before, many blocks were not classified, which causes
problems downstream.  This required some changes in macaw core in two places:

1. The simplifier needed some additional rules to remove some redundant
   constructions that threw off the abstract interpretation of values.  This was
   particularly an issue while reading return values off of the stack in
   PowerPC.
2. Extending the abstract interpretation to be able to handle more operations (shiftl)
2018-03-28 16:59:12 -07:00
Tristan Ravitch
fdb00dec14 ppc: Initialize the stack pointer in the abstract state
PPC uses r1 for the stack pointer
2018-03-28 16:59:12 -07:00
Tristan Ravitch
d885de3a72 ppc: Implement identifyReturn
We need special treatment of the return, as the low two bits are cleared on
PowerPC, so we can't just rely on pattern matching against the ReturnAddr in the
IP register.
2018-03-28 16:59:12 -07:00
Tristan Ravitch
d3a97edb4b ppc: Implement identifyReturn 2018-03-27 18:19:36 -07:00
Kevin Quick
7d7656bbd7
[ppc] Replace deprecated asLiteralAddr with valueAsMemAddr. 2018-03-27 10:51:16 -07:00
Kevin Quick
5ec4b48e16
[ppc] Update identifyReturn to identify based on IP == LNK
The identifyReturn was previously unused because the Macaw Discovery
performed this test inline, but some architectures have different
semantics so the identifyReturn is now used by the Discovery process.
This implements the return discovery that should be sufficient for the
PPC.
2018-03-27 10:49:30 -07:00
Tristan Ravitch
2d54ca1362 ppc: Fix some expected test output
Recent changes in macaw(-base) mean that we split blocks more aggressively.  The
old expected outputs were conservative - these new values are much more in line
with intuitive expectation (with more aggressive splitting of blocks and less
code duplication between blocks).
2018-03-23 15:14:54 -07: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
Daniel Wagner
851168f9ad let tests compile again 2018-03-01 11:45:59 -05:00
Tristan Ravitch
82bbd93d2a ppc: Add arch statements for hardware transactional memory
These instructions are mostly outside of our model.  That said, they do have
effects on the CPU state that we really should model, but are not yet.
2018-02-28 22:33:10 -08:00
Kevin Quick
e8b9d8a6a4
[ppc] Update for changed Macaw.Memory LoadOptions. 2018-02-22 17:37:40 -08:00
Kevin Quick
22bbdf7ee7
Common ExtractValue instances for sharing amongst architectures. 2018-02-07 11:34:38 -08:00
Tristan Ravitch
aaf2f67ea4 ppc: Add arch-specific statements for some icache instructions 2018-01-22 11:22:24 -08:00
Tristan Ravitch
71e3d868b8 Fix a bug in handling arch-specific statements
The system call instructions TRAP and SC were updating the IP twice, which led
to skipping instructions.  The IP increment for these instructions was already
handled in the abstract interpretation of arch-specific terminators.
2018-01-22 10:34:52 -08:00
Tristan Ravitch
46333f1a09 Submodule updates 2018-01-22 10:26:20 -08:00
Tristan Ravitch
260ac399c6 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2018-01-19 18:12:47 -08:00
Tristan Ravitch
37d6ca6732 Fix a bug where arch-specific statements weren't incrementing the IP 2018-01-19 18:12:15 -08:00
Ben Selfridge
7e47db94a3 Updated macaw-ppc to handle floating-point UFs 2018-01-17 12:54:30 -08:00
Ben Selfridge
f6face9136 Added VSCR for vector semantics 2018-01-08 17:56:00 -08:00
Ben Selfridge
63c2fec79b Simplified code using addArchExpr. 2018-01-05 14:58:15 -08:00
Ben Selfridge
3c3ffbc375 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2018-01-05 13:38:36 -08:00
Ben Selfridge
d95b1f6b3f Updated macaw-ppc code to handle VecN PPCPrimFns. 2018-01-05 13:27:53 -08:00
Tristan Ravitch
2247747bef Update submodules to the latest macaw (and others)
Macaw has removed all floating point expression types, so we duplicate those as
arch-specific functions for PowerPC until the more general floating point
support is ready.
2018-01-02 18:17:32 -08:00
Tristan Ravitch
5a2999089a Remove some tracing 2017-12-18 17:15:05 -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