Tristan Ravitch
48bfd87165
Add a missing register (XER) to the macaw register state
2017-11-06 19:44:19 -08:00
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
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
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
Ben Selfridge
fdf03c5c80
Rearranged a few things
2017-10-16 15:37:19 -07:00
Tristan Ravitch
792eb1aaf9
[ppc] Add a helper for turning operands into bitvectors
...
The main function is 'extractValue', which takes an operand and returns a macaw
bitvector for it (in the PPCGenerator monad).
There are still some missing cases for the memory operands.
2017-10-16 15:11:16 -07:00
Ben Selfridge
690687b0b6
started fixing up the BoundVar case
2017-10-16 14:15:12 -07:00
Ben Selfridge
ebe47b74fc
work in progress TH translation
2017-10-16 11:35:12 -07:00
Ben Selfridge
d48f30f173
Filled out some TH stuff
2017-10-13 14:26:39 -07:00
Ben Selfridge
50884f8af8
merging
2017-10-13 13:14:58 -07:00
Ben Selfridge
6058c2ebec
started template haskell stuff
2017-10-12 10:21:48 -07:00
Tristan Ravitch
b5ac6be425
Add some documentation and build some helpful maps for the TH translation
2017-10-12 10:11:16 -07:00
Tristan Ravitch
90e66cd252
Update to the latest macaw changes
2017-10-11 21:04:04 -07:00
Tristan Ravitch
e5895833ba
Plumb through most of the TH bits to generate 'execInstruction'
...
The remaining part is 'genCaseBody', which is where we'll write the translator
from ParameterizedFormula to TH Exps. The semantics are loaded from semmc and
the outer case expression breaking down instructions is all in place. This has
several accompanying changes in semmc and dismantle.
2017-10-11 18:07:56 -07:00
Ben Selfridge
54f5715c8b
filled out locToReg
2017-10-10 15:37:22 -07:00
Ben Selfridge
b270a2b9a2
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-10 14:51:54 -07:00
Ben Selfridge
064d0c4e8d
Added TestBit, done (for now) with crucible expressions
2017-10-10 14:51:25 -07:00
Ben Selfridge
d0fac23418
Fixed BVSelect a bit; need to re-examine type proofs
2017-10-10 14:35:00 -07:00
Ben Selfridge
578c1c0258
Completed BVConcat and BVSelect
2017-10-10 12:32:20 -07:00
Tristan Ravitch
c0889aa8bb
Enable formula loading in the TH entry point
...
Also update the semmc submodule to the required version.
2017-10-09 23:18:33 -07:00
Ben Selfridge
6db1a2d43c
rewrote crucAppToExpr in applicative style
2017-10-09 16:07:52 -07:00
Ben Selfridge
b1cbc0548e
Completed refactoring of Expr type.
2017-10-09 14:02:52 -07:00
Ben Selfridge
058963f8fe
Changed Expr type to be non-recursive
2017-10-09 11:27:59 -07:00
Tristan Ravitch
c1566e7946
Fix an issue with formula loading
...
Also disable formula loading for now because it raises an exception due to some
unhandled constructs in the parser.
2017-10-06 22:14:34 -07:00
Tristan Ravitch
95361474ae
Feed semantics to the genExecInstruction calls
...
These lists come from semmc and contain the bytestrings of the semantics files
for each opcode.
NOTE: The lists are currently empty (presumably due to bugs), but the logic for
moving data around and setting up a SimpleBuilder instance is at least right.
2017-10-06 16:58:53 -07:00
Tristan Ravitch
072571d219
Expand the initial abstract state for a block
...
We needed to note that the LNK register contains the return address
2017-10-04 17:01:56 -07:00
Tristan Ravitch
38cb6cdfd8
Add a note about TranslateError
2017-10-04 17:01:56 -07:00
Ben Selfridge
c76cd00e72
trying to fix git
2017-10-04 16:40:14 -07:00
Tristan Ravitch
0a974b1a15
Add the TH invocation to PPC32
2017-10-04 16:00:18 -07:00
Tristan Ravitch
1e55026ae5
Add a definition of absEvalArchFn
...
We'll have to expand this as we add functions
2017-10-04 15:55:28 -07:00
Tristan Ravitch
711eabc058
Implement postCallAbsState and absEvalArchStmt
...
absEvalArchStmt is trivial (for now)
2017-10-04 15:53:03 -07:00
Tristan Ravitch
ac776b7340
Remove a redundant export
2017-10-04 15:51:03 -07:00
Tristan Ravitch
f12166c2c3
Add a trivial definition of the architecture-specific abstract evaluation function
2017-10-04 15:46:33 -07:00
Tristan Ravitch
ab29030e14
Implement the initial abstract state
2017-10-04 15:44:59 -07:00
Tristan Ravitch
6a14cfffb8
Implement archDemandContext
...
This required a few more instances and a wrapper around `ArchStmt`
2017-10-04 14:40:36 -07:00
Ben Selfridge
7e563acef8
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-04 14:09:02 -07:00
Ben Selfridge
bb0d7e7341
converting from crucible Elt type to Macaw Apps
2017-10-04 14:08:09 -07:00
Tristan Ravitch
57db5aa6f6
Add a definition of the jump table entry size
2017-10-04 13:26:08 -07:00
Tristan Ravitch
c02b0c605c
Add a trap arch-specific statement
2017-10-04 13:25:56 -07:00
Tristan Ravitch
7f8410ce7f
Fill in some previously undefined IP value calculations
2017-10-04 11:24:16 -07:00
Tristan Ravitch
af6ead250a
Add some documentation
2017-10-04 11:08:42 -07:00
Tristan Ravitch
20f078e9eb
Hook up the execInstruction functions
...
These are now referenced in the necessary spots in the ArchitectureInfo definitions
2017-10-04 10:16:54 -07:00
Tristan Ravitch
498ff33a6d
Finish the disassembler skeleton
...
There are still some IP values to compute, but the shape of the algorithm is there
2017-10-04 10:10:06 -07:00
Tristan Ravitch
047e84c586
Remove an unused import
2017-10-04 10:10:06 -07:00
Tristan Ravitch
48f556ffcb
Add some more helpers for the Generator monad
2017-10-04 10:10:06 -07:00
Tristan Ravitch
00f2b1d423
Add a context that we'll need
2017-10-04 10:10:06 -07:00
Tristan Ravitch
eec7075b46
Implement catchError in a MonadError instance
2017-10-04 10:10:06 -07:00
Ben Selfridge
3a49345b15
Added Semantics directory, had forgotten to add it previously
2017-10-04 10:03:29 -07:00
Ben Selfridge
5de25b8906
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-04 10:00:04 -07:00
Tristan Ravitch
9b8a7bac21
Remove an unused module
...
The rewriters are now in the Arch module
2017-10-04 08:48:52 -07:00
Tristan Ravitch
a851cddebd
Add arch-specific decls + type instances + rewriters
...
This also lets us add 'withArchConstraints' easily.
2017-10-03 18:59:35 -07:00
Tristan Ravitch
8a1195b1c6
Fill in the AddrWidthReprs for PPC
2017-10-03 18:07:21 -07:00
Tristan Ravitch
d1c86fd6d4
Remove unused imports
2017-10-03 18:07:15 -07:00
Tristan Ravitch
c751e02e6c
Use a ConstraintKind to simplify a number of constraint contexts
2017-10-03 18:05:46 -07:00
Tristan Ravitch
adf8a46f91
Implement more of the PPCGenerator state
2017-10-03 18:00:54 -07:00
Tristan Ravitch
2ec88811c5
Add special purpose registers to the definition of 'RegisterInfo'
2017-10-03 16:37:01 -07:00
Tristan Ravitch
171cc0d5ca
Remove an unused module
2017-10-03 16:31:41 -07:00
Tristan Ravitch
4a8828429c
Implement 'RegisterInfo' for PPCReg
2017-10-03 16:31:16 -07:00
Ben Selfridge
ad8d5fc3b4
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-03 14:43:33 -07:00
Tristan Ravitch
dc261436c7
Generalize the type of PPCReg
...
The width of a GPR was formerly fixed to 64 bits. It now reflects the actual arch.
2017-10-03 13:40:11 -07:00
Tristan Ravitch
5e136dceec
Let PPCGenerator report errors
...
It doesn't right now, but the translation from semantics to macaw will have some
opportunities around invalid encodings.
2017-10-03 13:39:59 -07:00
Tristan Ravitch
19b65973fc
Apply the state transformer
...
Committing now to experiment with adding failure modes to PPCGenerator
2017-10-03 13:23:20 -07:00
Tristan Ravitch
620b6f5980
Plumb through a parameter for the semantics lookup function
...
This is the function that will be generated via TH for PPC32 and PPC64.
2017-10-03 11:55:40 -07:00
Tristan Ravitch
6ed9d0d45d
Simplify more type variables and implement the error throwing function for the disassembler
...
We had two different state thread parameters: s and ids. We only need one (for
now), so unify them.
2017-10-03 11:09:23 -07:00
Tristan Ravitch
7aadfdf373
Remove a literal width of 64
...
That should have been a function of the architecture
2017-10-03 10:31:06 -07:00
Tristan Ravitch
083f9b4fa1
Remove a type parameter
...
We don't need the separate w - it is just a function (ArchAddrWidth) of the architecture.
2017-10-03 09:36:41 -07:00
Tristan Ravitch
d5c5d40ddb
Add more disassembly infrastructure
2017-10-02 17:32:59 -07:00
Ben Selfridge
2b810be25a
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-02 14:38:20 -07:00
Tristan Ravitch
7869f0e6c7
More work on disassemble
2017-10-02 14:29:15 -07:00
Tristan Ravitch
385bff0c4d
Move the generator monad into its own module
2017-10-02 14:17:36 -07:00
Tristan Ravitch
4b6b82cd13
Flesh out disassembleFn a bit more
2017-10-02 13:35:51 -07:00
Tristan Ravitch
20e5b5f00d
Add some type instance declarations for ppc32 and ppc64
2017-10-02 13:35:04 -07:00
Ben Selfridge
0526c6ae21
merging
2017-10-02 12:55:52 -07:00
Ben Selfridge
6f0d49f76e
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2017-10-02 12:54:43 -07:00
Tristan Ravitch
90a9c5ff65
Generalize the architecture info def
...
Now we can use the same infrastructure for PPC32 and PPC64. There might be some
rough edges, but we can work around those with type functions.
This change also adds an implementation for the preserved registers across
system calls for macaw.
2017-10-02 11:44:46 -07:00
Ben Selfridge
136d772abf
merging some things
2017-10-02 11:23:08 -07:00
Tristan Ravitch
4d9c7cd028
Split up the functions that will comprise ppc_linux_info
2017-10-02 11:19:34 -07:00
Ben Selfridge
677ba803b3
Added a couple things
2017-10-02 11:10:00 -07:00
Tristan Ravitch
1f1a6d8561
Abstract the stubs to work for ppc32 and ppc64
2017-10-02 10:59:40 -07:00
Tristan Ravitch
61218ca31d
Add stubs for most of the architecture info functions
2017-10-02 10:54:10 -07:00
Tristan Ravitch
45f08a2036
Fill in the endianness of the arch info
2017-10-02 10:37:44 -07:00
Tristan Ravitch
c997e2dada
Use explicit exports for PPCReg
2017-10-02 10:32:58 -07:00
Tristan Ravitch
6b967e1e8a
Fill out the fields of ppc_linux_info
2017-10-02 10:32:05 -07:00
Tristan Ravitch
cdd9647db9
Simplify some helpers in macaw-ppc
...
Use the MonadState combinators and a lift instead of explicitly wrapping
monadic actions.
2017-10-02 10:27:12 -07:00
Tristan Ravitch
202a95b959
Re-use the PPC arch tag (specifically, PPC64) from semmc-ppc
2017-10-02 10:26:51 -07:00
Tristan Ravitch
8820b01805
Depend on semmc/semmc-ppc and enable warnings
2017-10-02 10:26:39 -07:00
Tristan Ravitch
07ff647dcf
Add some missing instances for PPCReg
2017-10-02 09:40:17 -07:00
Ben Selfridge
7a443bfe99
added a few more functions for PPCGenerator
2017-09-29 17:35:29 -07:00
Ben Selfridge
b234b673f9
Added addStmt to PPCGenerator monad
2017-09-29 15:37:41 -07:00
Ben Selfridge
65a7e8c17c
second commit
2017-09-29 09:37:45 -07:00
Ben Selfridge
bf9b320e38
first commit
2017-08-28 15:48:55 -07:00
