cksystemsgroup / monster

Monster is a symbolic execution engine for 64-bit RISC-U code
https://cksystemsgroup.github.io/monster
MIT License
10 stars 3 forks source link

fix: invertibility conditions DIVU and REMU #141

Closed saraseidl closed 3 years ago

saraseidl commented 3 years ago

DIVU

Regarding the the special case that is invertible, but should not occur according to the assumption that target != current output. So far this case is handled as not invertible. This is just a suggestion to handle it as invertible.

REMU

This adds missing parenthesis and the case s == t => invertible

Summery of invertible, not invertible:

DIVU Lhs: s = 0, t = ones => invertible, but should not happen as this means currently t = ones already s = 0, t != ones => not invertible t = ones, s != {0,1} => not invertible, overflow

DIVU Rhs: t = s = 0 => invertible, but again should not happen

t = 0, s != ones => invertible t = 0, s = ones => not invertible

t = ones, (s = ones) => invertible t = ones, (s != ones) => invertible

s < t => not invertible

github-actions[bot] commented 3 years ago

:tada: This PR is included in version 0.4.0 :tada:

The release is available on:

Your semantic-release bot :package::rocket: