search

lifting-bits / remill

Library for lifting machine code to LLVM bitcode
Apache License 2.0
1.25k stars 142 forks source link

Fully model X87 handling of SNaN/QNaN, other exceptional inputs #223

Open ranweiler opened 6 years ago

ranweiler commented 6 years ago

While adding X87 instructions, I've found that we don't model (or sometimes test) various input classes for X87 semantics. This surfaced when I started adding more exhaustive test inputs for the BCD instructions.

Much of this relates to inaccurate modeling of the pushing SNaNs onto the X87 stack. The X87 stack does not appear to typically store SNaNs; at least, they are quietized by fld before being pushed. Our fld semantic pushes an explicitly signaling NaN onto the X87 stack.

Even after fixing this, in our semantics tests, there are cases where we push an SNaN onto the X87 stack (after being quietized), which sets the IE bit. Then we perform an op with ST(0) whose semantic has a line like state.sw.ie = IsSignalingNaN(val);, which always clears the IE flag, since val was quietized when pushed. What we should do is |=, to avoid clearing IE if it was set. See fsqrt, frndint, &c.

Right now, I think we have a situation where the two modeling errors cancel each other out in the existing semantics tests that are sensitive to this. I'm also wondering if this relates to the Travis-only errors we're seeing with ftst, but as I write this issue, Travis is having service issues, so I haven't been able to test that at all.

ranweiler commented 6 years ago

I'd like to wrap up the FBLD/FBSTP impls in #219, but this is a bit of cross-cutting issue, and it might make sense to address first. Otherwise I'll have to do somethign like not test SNaNs, or cut out a partial fix in that PR to get tests all passing.

ranweiler commented 6 years ago

This is mostly done in #224, but it needs one more pass to add NaN test cases to all the instructions that consume the X87 stack. Some of the existing tests (e.g. for fyl2x) just use fldpi and fldlg2 to set up happy path test inputs.