Commit Graph

454 Commits

Author SHA1 Message Date
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
Tristan Ravitch
48dfa4d192 Remove an accidentally-committed binary file 2017-11-10 08:18:16 -08:00
Tristan Ravitch
c990077d7b Update the semmc submodule
This update includes many more semantics files covering most of the dotted
instruction variants
2017-11-09 23:31:13 -08:00
Tristan Ravitch
9d750c944a Add a new type of test to PowerPC
It runs code discovery over a large-ish binary to test coverage.  We currently
fail due to unsupported instructions (expected).  This test will guide
priorities on implementing new semantics.
2017-11-09 17:18:20 -08:00
Tristan Ravitch
fc1bd8b077 Add support for more instructions
semmc has semantics for many new instructions.  We also added support for
translating the count leading zero functions.
2017-11-09 17:17:51 -08:00
Tristan Ravitch
6ede8a2511 Add some more detail on the instruction semantics writeup 2017-11-09 15:37:05 -08:00
Tristan Ravitch
d5d1d87fd5 Split some shared helpers out of a test module 2017-11-09 10:43:41 -08:00
Tristan Ravitch
1f9ba647cf Add some documentation on adding instruction semantics 2017-11-09 09:56:17 -08:00
Tristan Ravitch
9b9e1654ec Update the submodules to add more semantics
This focuses on the rotate instructions
2017-11-08 15:47:01 -08:00
Tristan Ravitch
e307c9a82a Add a comment in the test suite 2017-11-08 15:46:40 -08:00
Tristan Ravitch
5e150c15a0 Update to the latest semmc
This includes some new semantics required for the test suite
2017-11-08 10:59:43 -08:00
Tristan Ravitch
e5d20c6acf Fix an expected test output
It looks like I counted the bytes wrong the first time
2017-11-08 10:56:13 -08:00
Tristan Ravitch
b9835b9767 Cleanup and documentation pass 2017-11-07 22:46:06 -08:00
Tristan Ravitch
599a357515 Don't export curPPCState 2017-11-07 21:45:04 -08:00
Tristan Ravitch
a03953ecdc Delete some obsolete comments 2017-11-07 21:36:25 -08:00
Tristan Ravitch
6308df3a8f Add a helper to set register values
This helper additionally simplifies constants.  This is very useful for dealing
with simplifying the instruction pointer.  That is required by the rest of
macaw, which expects IP values it wants to explore to be fully reduced.
2017-11-07 21:16:00 -08:00
Tristan Ravitch
71a432ed18 Improve the test suite
Don't just ensure that found blocks are expected: also ensure that all expected
blocks are found.
2017-11-07 20:50:33 -08:00
Tristan Ravitch
c3d0ede125 Import alignment 2017-11-07 20:29:41 -08:00
Tristan Ravitch
65bc1231fb Implement 'identifyCall' for PowerPC
The current heuristic isn't great, but is probably okay for now.  It just checks
to see if the LNK register is an address plus four.  Something more precise
would require knowing the address of the next instruction, but we can't get that
from the IP, which has already been changed due to the call.
2017-11-07 20:23:11 -08:00
Tristan Ravitch
a648a4c50b Improve the formatting for test failures
Now print addresses as hex values
2017-11-07 20:22:49 -08:00
Tristan Ravitch
fed8e00482 [ppc] Fix the offsets in the call test 2017-11-07 20:22:32 -08:00
Tristan Ravitch
f126dbf5fa Add a (currently failing) test for calls 2017-11-07 17:49:53 -08:00
Tristan Ravitch
48ba00870d Add some extra tracing to 'identifyFunction' 2017-11-07 17:49:36 -08:00
Tristan Ravitch
65c940e334 Remove an unused function 2017-11-07 17:49:28 -08:00
Tristan Ravitch
fdcbbeae39 Fix a bug in register value handling
The semantics of each instruction are atomic updates over the register state.
Prior to this commit, changes were not atomic and updates to register values
were visible to later register definitions, which causes a huge number of
problems.  Now, we take a snapshot of the register state at the beginning of the
instruction and read all values we need from that snapshot.  This way, updates
are isolated from one another.
2017-11-07 17:45:00 -08:00
Tristan Ravitch
fc48993507 Update an expected test result
My understanding of how macaw splits up blocks was incorrect when I wrote the
test initially.  Macaw doesn't split blocks just because a jump happens to land
in the middle of the block, so the middle block in this example is actually a
few instructions longer.
2017-11-07 14:32:51 -08:00
Tristan Ravitch
81fbec6bb9 Improve the layout of the frontier calculation 2017-11-07 13:45:40 -08:00
Tristan Ravitch
a4cbd3a9d0 Make the simplifier more powerful
It now recursively traverses its arguments.  This isn't great from an efficiency
perspective, but we need it to be able to simplify instruction pointers computed
from relative jumps (which involve some sign extensions and shifts).
2017-11-07 13:44:41 -08:00
Tristan Ravitch
0b43f5672e Have 'matchConditionalBranch' simplify the values it returns
These values are new values of the IP to explore, and the code consuming these
values expects them to be BV literals (i.e., simplified from expressions to
values).

The simplifier isn't currently powerful enough to simplify everything we throw
at it, but this is at least the right place to apply it.  If we don't simplify
here, the core of macaw won't know how to follow the IP changes and will miss
blocks.
2017-11-07 11:36:50 -08:00
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
008c422917 Update to the latest semmc
This includes semantics for generalized branch conditional
2017-11-06 22:25:12 -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
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