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.
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).
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.
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.
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.
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.
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.
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.
