Commit Graph

393 Commits

Author SHA1 Message Date
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
Kevin Quick
cd1c676554
[arm] Initial ARM ELF file macaw import and parse. 2017-12-28 16:30:25 -08:00
Kevin Quick
77d4341ac1
Initial tests for analyzing test-just-exit ARM binary. 2017-12-20 15:26:01 -08:00
Kevin Quick
307450ce14
Add generated output files and editor backup files to gitignore. 2017-12-20 10:13:31 -08:00
Kevin Quick
046ce166d3
Initial empty framwork for macaw-arm ARM support. 2017-12-18 17:46:17 -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
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
3838d0964d Submodule updates 2017-11-30 17:13:11 -08:00
Tristan Ravitch
5d2af0328f Update the semmc submodule 2017-11-29 20:27:49 -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
0a24dbf78e Update the semmc submodule 2017-11-29 11:40:14 -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
5347f7b079 Update the semmc submodule with more semantics 2017-11-28 23:10:58 -08:00
Tristan Ravitch
c4675b47e4 ppc: Add some more semantics for the cr logical operations 2017-11-28 22:36:08 -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
Tristan Ravitch
cea6bf38c8 Update the dismantle submodule
Cleans up a warning
2017-11-28 19:46:18 -08:00
Tristan Ravitch
b1e0b07cc1 Update semmc and dismantle 2017-11-28 18:42:32 -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
Tristan Ravitch
1d49256c23 Bump the semmc submodule 2017-11-22 17:04:47 -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
96a787f895 semmc submodule update
This update includes semantics files for the floating point store instructions
2017-11-16 10:17:54 -05: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
Ben Selfridge
399cd4ab6c Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-11-15 18:00:39 -08:00
Ben Selfridge
e1963bcbf2 Added single_to_double for floating point operations 2017-11-15 18:00:19 -08:00
Tristan Ravitch
2092a0fd01 Add a (currently failing) test for indirect call handling
The code pointer discovery in macaw can't handle this case because we never
write the code pointers into memory - we only read them.  We really need a way
to tell macaw about code pointers.

The easy workaround is to pull all of the function entry points out of the TOC
and just seed the macaw search with them, but it would be nice to be able to
identify them from first principles.
2017-11-14 19:00:01 -08:00
Tristan Ravitch
e4d3942094 Update the semmc submodules for some more instruction semantics 2017-11-13 23:33:07 -08:00
Tristan Ravitch
90f066cd5b Add a few more arithmetic and bitwise instructions 2017-11-13 18:05:51 -08:00
Tristan Ravitch
693727330d Update the semmc submodule with more semantics 2017-11-13 16:54:01 -08:00
Tristan Ravitch
94b72b2c73 Improvements for the generated semantics transformers
This change now memoizes translations of SimpleBuilder expression fragments,
which allows us to restore the sharing in semantics formulas.  The generator
re-uses shared sub-expressions automatically now.  This generates less Haskell
code, yielding better code density and fewer terms constructed at run time.  It
also reduces compile times.

It seems to cut the size of the generated TH code by about half.  It also
generates less deeply-nested Haskell code, making the resulting TH splices human
readable.
2017-11-13 10:46:33 -08:00
Tristan Ravitch
0d6877611b Add some bugfixes for popcount in the semmc submodule 2017-11-10 17:22:52 -08:00
Tristan Ravitch
2002afa246 [ppc] Add preliminary support for popcount
It isn't supported in SimpleBuilder, so we use an uninterpreted function in the
formula language for now.
2017-11-10 16:52:38 -08:00
Tristan Ravitch
bbd00f7ef2 [ppc] Add division and a few arch-specific statements
The arch-specific statements are for memory synchronization
2017-11-10 14:48:35 -08:00