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