Commit Graph

360 Commits

Author SHA1 Message Date
Tristan Ravitch
fcb694ccb9 Add a test for conditional branches
It doesn't pass yet.  It is hung up on an unsupported register type (Crrc, used
in a compare).
2017-11-06 17:19:16 -08:00
Tristan Ravitch
11a754b3ed Add support for conditional branches 2017-11-06 17:18:59 -08:00
Tristan Ravitch
8db18882fa Factor out the implementations of some of the TH translations
These operations generate a lot of code, so it is helpful to factor them out and
reduce the burden on the type checker.  Factoring these two definitions out cuts
the generated code nearly in half.
2017-11-06 15:43:32 -08:00
Tristan Ravitch
6a45dc0893 [ppc] Fix an issue with floating point translation
The change is actually in the semantics (semmc), where we were extracting the
wrong part of the 128 bit vector registers to operate on.  Many operations were
being simplified to zero, which manifest as unused fprc registers.
2017-11-06 14:25:54 -08:00
Tristan Ravitch
15078b2bde Remove more unused imports 2017-11-06 10:22:16 -08:00
Tristan Ravitch
4e1db21b08 Remove another piece of commented-out code 2017-11-06 10:15:18 -08:00
Tristan Ravitch
15b3ba466d Remove some unused imports 2017-11-06 10:14:33 -08:00
Tristan Ravitch
e2e3744808 Remove an unused value 2017-11-06 10:13:49 -08:00
Tristan Ravitch
0ed78396cf Remove some obsolete commented-out code 2017-11-06 10:13:06 -08:00
Tristan Ravitch
a9baec5d39 Port to the latest macaw
This makes the architecture-specific terminator statement handling actually work
2017-11-06 10:11:34 -08:00
Tristan Ravitch
5e47bf6ce9 Improve the PPC test suite
It now checks to ensure that expected blocks are actually the expected number of bytes
2017-11-05 20:51:57 -08:00
Tristan Ravitch
0c81c13570 Remove an unused simplifier 2017-11-05 20:19:37 -08:00
Tristan Ravitch
b726a5ab7c Add semantics for TRAP (no arguments) 2017-11-04 23:00:28 -07:00
Tristan Ravitch
17d00036f1 Fix a bug with the syscall instruction semantics
The previous implementation missed an IP update, which is required to prevent
macaw from treating the syscall instruction as its own basic block.  Also factor
out the implementation of SC so that we can re-use it later for TW.
2017-11-04 22:42:01 -07:00
Tristan Ravitch
e765345a7b Add support for the Syscall arch-specific terminator 2017-11-04 16:23:12 -07:00
Tristan Ravitch
eaaa4abce7 Switch to a ContT-based PPCGenerator monad
This is required to support both block splitting and early returns due to other
block terminators.
2017-11-04 13:38:57 -07:00
Tristan Ravitch
f6d3f0f1de Save the simplified IP at each decoding step
If we don't do this, the saved IP is unsimplified and contains expressions,
which means that the next decoding step won't simplify properly (it would
require recursive simplification, which we would prefer to avoid).
2017-11-03 20:03:52 -07:00
Tristan Ravitch
6f475c4e79 Expand the simplifier
It is now architecture-independent and covers enough (in principle) to work for
PowerPC computed jumps
2017-11-03 18:18:07 -07:00
Ben Selfridge
e2a71d62ca Deleted a few turds 2017-11-03 16:36:06 -07:00
Ben Selfridge
8d530b4f3f Deleted old export of PPCWidth from PPCReg.hs 2017-11-03 15:23:24 -07:00
Ben Selfridge
eff3fa6425 Consolidated constraints into one: PPCArchConstraints 2017-11-03 15:20:46 -07:00
Ben Selfridge
7dd2a2a385 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-11-03 15:19:51 -07:00
Ben Selfridge
889c988d4b Added Base.hs, for some reason magit didn't warn me it hadn't been added 2017-11-03 15:18:05 -07:00
Tristan Ravitch
0e9b739503 Implement test_bit_dynamic in the TH translation of semantics
It translates to a BVTestBit (since here we know which bit to extract, whereas
we don't in the semantics).
2017-11-03 15:07:52 -07:00
Ben Selfridge
a7c7600a20 Removed unused functions from TH.hs and put them in a standalone module 2017-11-02 11:43:27 -07:00
Tristan Ravitch
c788aebab8 Update the dismantle submodule
This fixes a bug in parsing the stdu instruction that was causing our test to
implode.  It still isn't right, but it gets farther (and parses two instructions
out of the block).
2017-10-31 22:23:57 -07:00
Tristan Ravitch
81310c9c0f Implement a very simple simplifier for use in the disassembler
This simplifier just evaluates some constant forms that appear as IP value
updates.  This is enough to let us pass the check we need to without relying on
the full rewriter, which is too heavyweight for our needs.  Furthermore, macaw
itself calls the rewriter, so duplicating that effort is very wasteful.
2017-10-31 22:04:28 -07:00
David Johnson
c611717735
Tracing to track rewriting bug 2017-10-31 18:52:12 -07:00
Ben Selfridge
f3f07ff099 Adding rewriting to macaw-ppc translation 2017-10-27 21:08:47 -07:00
Ben Selfridge
16839e30c1 Test runs, fails at identifyCall 2017-10-27 14:29:04 -07:00
Ben Selfridge
bc2dc76be6 Working on findElfEntryPoint, which does a double-lookup for PowerPC. 2017-10-26 18:38:47 -07:00
Ben Selfridge
0a1d46c581 Finally have an actual PPC binary for test-just-exit test. 2017-10-25 15:02:16 -07:00
Ben Selfridge
be61b37569 fixed test case, which was x86. now it's powerpc. test still fails. 2017-10-24 17:22:57 -07:00
Ben Selfridge
2ada779a1f test-just-exit 2017-10-24 17:21:00 -07:00
Ben Selfridge
2a7213f416 Added a simple test, which fails. 2017-10-24 16:36:36 -07:00
Tristan Ravitch
0fb90e5d6b Update dismantle and semmc
This adds some more general instances needed for higher-level dependencies
2017-10-23 18:06:32 -07:00
Tristan Ravitch
8379d76da5 [ppc] Fix a bug in the translation of BVConcat
The second bitvector was never actually used
2017-10-23 09:47:12 -07:00
Tristan Ravitch
dd91bc2fe8 Rename the cabal.project file
Users should symlink the file the correct name locally; this makes it easier to
use the project as a submodule
2017-10-23 09:46:00 -07:00
Tristan Ravitch
ffaa912b74 Convert from applicative to nested binds in the TH code
This makes the generated splices much easier to read, which will be helpful for debugging.
2017-10-18 22:40:53 -07:00
Tristan Ravitch
28b7b68881 Fill out more of the PPC semantics translation
This covers all of the floating point used so far, as well as memory operations.
Note that this commit relies on changes that aren't pushed to macaw yet.
2017-10-18 17:48:07 -07:00
Tristan Ravitch
d893ce8dcb Fix the BVConcat translation 2017-10-18 17:47:29 -07:00
Tristan Ravitch
601ea06e07 Fix a TH bug
We were generating a literal TH expression when we meant to generate a splice
2017-10-18 17:46:47 -07:00
Tristan Ravitch
344b253bf8 Add missing cases for the XER reg 2017-10-18 17:42:42 -07:00
Tristan Ravitch
f2f3b33fca Convert floating point round to single precision 2017-10-18 17:42:42 -07:00
Ben Selfridge
74b5d85beb Added test skeleton, rearranged some TH stuff 2017-10-18 14:27:29 -07:00
Tristan Ravitch
ace4520846 Update to the latest macaw 2017-10-18 10:29:57 -07:00
Tristan Ravitch
49545299d9 Add cases for FP operation translation 2017-10-18 08:49:09 -07:00
Tristan Ravitch
13def38f25 Fix some compilation errors with an improved evaluator in semmc 2017-10-17 21:38:53 -07:00
Tristan Ravitch
2a7c5bd541 Extend the uninterpreted function evaluator
It is currently very messy because the ppc.is_r0 function breaks some
abstraction boundaries that make it very irregular.  There is some common code
that can probably be factored out, but it will still be a mess.

The other big change is handling the read_mem calls.
2017-10-17 19:16:31 -07:00
Tristan Ravitch
eb8b78b372 Add support for a number of new uninterpreted functions
This covers evaluating all of the statically-evaluated functions in expression
contexts (e.g., is_r0 and the memory reference extraction functions).

The expansion seems pretty reasonable.

There are still some cases to handle w.r.t. floating point elementary functions
and memory reads and writes, which need to be handled a bit differently.

Note: we also have to call the formula simplifier soon.
2017-10-17 17:07:03 -07:00