Tristan Ravitch
32d37e1a31
Delete an obsolete comment
2017-11-07 11:36:36 -08:00
Tristan Ravitch
ec9695d29b
Fix the initial PreBlock state w.r.t. block ids
...
We were initializing the next PreBlock ID as 0, which caused that block id to be
reused later (the initial block is given ID 0)
2017-11-07 11:28:01 -08:00
Tristan Ravitch
e405e23b93
Fix a bug where we were generating macaw bitvector literals with negative integer components
...
Apparently this is not allowed, and caused an assertion failure in a pretty printer.
2017-11-07 11:24:57 -08:00
Tristan Ravitch
48bfd87165
Add a missing register (XER) to the macaw register state
2017-11-06 19:44:19 -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
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
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
2a7213f416
Added a simple test, which fails.
2017-10-24 16:36:36 -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
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
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
Ben Selfridge
ccd344f027
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-17 12:32:40 -07:00
Ben Selfridge
0649ea4f0c
Nearly done with semmc->macaw, need to complete addEltTH function
2017-10-17 12:27:57 -07:00
Tristan Ravitch
07c48afe46
Add instantiations for some uninterpreted functions
...
This covers functions that are used to isolate locations to be defined from
composite operands (e.g., the base registers of memrr and memri operands).
2017-10-17 11:51:11 -07:00
Tristan Ravitch
cf0a6df0da
Simplify the sequencing of our generated monadic PPCGenerator actions
...
We were building up a list and calling sequence; instead, just generate a single
do block directly
2017-10-16 19:51:32 -07:00
Ben Selfridge
1a5946bd0d
Nearly done with semmc -> macaw, need to complete a few more cases
2017-10-16 16:40:51 -07:00
Ben Selfridge
e2121de437
Finished bound variable case in addEltTH
2017-10-16 15:53:28 -07:00
Ben Selfridge
17e44dae2a
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-16 15:37:49 -07:00
