Challenge 9 includes a handful of vector instructions used to implement a rounding operation. At the moment, the ASL translator is translating most of the vector instructions, but they are dropped when read into macaw. To support this, we updated macaw to include the semantics for those instructions, however, the resulting terms are now far to complicated and contain too many undefined elements to support code discovery.
There are a number of steps that are likely required to make these terms manageable:
Providing more constrained specifications for the floating point functions (i.e. producing undefined, but bounded values)
adding more term simplification rules to macaw
providing more precise initial values for processor flags specific to vector instructions
adding more variables to the "tracked" global state from ASL (i.e. processor flags that are otherwise always undefined)
Challenge 9 includes a handful of vector instructions used to implement a rounding operation. At the moment, the ASL translator is translating most of the vector instructions, but they are dropped when read into macaw. To support this, we updated macaw to include the semantics for those instructions, however, the resulting terms are now far to complicated and contain too many undefined elements to support code discovery.
There are a number of steps that are likely required to make these terms manageable: