Commit Graph

223 Commits

Author SHA1 Message Date
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
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
a24ea27be5 ppc: Implement the abstract evaluator for the TRAP instruction
Basically treat it just like a system call for now.
2017-11-29 20:27:25 -08:00
Tristan Ravitch
52dc736c08 ppc: Add more support for CR and FPSCR instructions 2017-11-29 16:30:46 -08:00
Ben Selfridge
45a898cf5d added double precision load/store 2017-11-29 15:11:12 -08:00
Ben Selfridge
11affb8848 Tests for all single-precision floating point load and store ops 2017-11-29 15:02:07 -08:00
Ben Selfridge
a25a477944 added first actual floating point test instruction (stfs) 2017-11-29 13:08:11 -08:00
Tristan Ravitch
5cea5a8a42 ppc: Fix the expected results of the fp test case 2017-11-29 10:14:20 -08:00
Tristan Ravitch
b033f3788c ppc: Change how we translate instructions represented by arch-specific statements
The old method involved providing the TH code a list of match expressions.  This
made it very difficult to inspect arguments of instructions.  The new approach
has the architecture backend provide a function that gets the first opportunity
to process instructions, which is much more flexible.  This commit also includes
support for a number of cache hint instructions that use the new features.
2017-11-28 21:36:49 -08:00
Ben Selfridge
3d1eb18289 Added support for floating point LT uf 2017-11-28 14:47:28 -08:00
Tristan Ravitch
ef5150e2e1 ppc: Remove an unused module 2017-11-27 22:53:55 -08:00
Tristan Ravitch
df03ddf439 Use more qualified names in the TH-generated SimpleBuilder->Macaw translation
This gives us better name capture properties, allowing us to use more
restrictive imports in the PPC64 and PPC32 modules.
2017-11-27 22:40:18 -08:00
Tristan Ravitch
289e1f33be [ppc] Updates to support some vector instructions
The semantics for many of the vector instructions are incomplete and just set
the target register to undefined.  This is enough for code discovery (for now).
2017-11-27 18:16:19 -08:00
Tristan Ravitch
c7af261d66 Marginally improve compile times
Disable a few optimizations in the TH-generated modules and add a fallthrough
case to prevent the coverage checker from firing.
2017-11-27 08:33:48 -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
221e5b3407 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-11-22 16:31:51 -08:00
Ben Selfridge
e1ffa245c2 added support for is_snan uninterpreted functions 2017-11-22 16:31:36 -08:00
Tristan Ravitch
18d5ac3fe4 Add a translation for the undefined value from semmc 2017-11-21 23:37:17 -08:00
Tristan Ravitch
3b763bf347 Export useful helpers from macaw-ppc
This includes another ELF helper to find function entry points and the
type-level tags to choose between the 32 and 64 bit architectures.
2017-11-21 14:21:37 -08:00
Tristan Ravitch
d49dbc679c [ppc] Make the PPC ELF helpers easier to use
The TOC parser now doesn't require a Memory object, making it easier to actually
instantiate this in derived tools (where the TOC parser needs to be used before
a memory is available).  To do this, we use MemAddr as the base type for the TOC
instead of MemSegmentOff
2017-11-21 14:10:47 -08:00
Tristan Ravitch
80145a0161 Fix a bad exponential behavior bug
The recursive simplifier could exhibit exponential behavior in cases where a
nested tree of irreducable terms were accumulated.  The recursive calls quickly
exploded execution times.

The fix was to remove the recursive calls from the simplifier, but to
incrementally simplify expressions to constants as they are added (via the
addExpr function).  This simplifies as much as the recursive case, but more
efficiently.  This change required exporting the simplifyApp function.
2017-11-16 21:42:30 -05:00
Ben Selfridge
9ce1ffa0c5 Added test case for floating point store. Not really functional yet. 2017-11-16 16:08:25 -08:00
Tristan Ravitch
dbbb0bd947 Add TOC entries to the macaw list of entry points in the test harness
This code now pulls all of the function addresses from the TOC as entry points
for the code discovery search.  This lets us trivially find code reachable via
indirect calls, as the function pointer discovery heuristic doesn't seem to be
well-suited to PowerPC.  I'd like to push on that, but it seems like a good
start for now.
2017-11-16 10:16:22 -05:00