Closed RicoloveFeng closed 2 years ago
Hi RicoloveFeng,
Thanks for reporting the bug! The current dev branch basically consists of an improvement in the Max-SMT encoding, so both the latest release and the dev branch contain this bug. We were not aware of it before.
The fix is easy: in case var1
and var2
are not stack variables (i.e. they do not start with "s..."), and one of the instructions is MSTORE8
, these variables must be cast to int. It seems we failed to notice this bug due to not appearing in any of our tests/experiments.
However, it also reveals some unexpected behavior when removing redundant combinations of MSTORE8
, so we need to look thoroughly into the issue. We will let you know as soon as the full fix is ready.
PUSH1 0 MSTORE8 MSTORE8 PUSH1 0 MSTORE8
I'm using the 2.0 release so I'm not sure whether it was fixed in a dev branch.
To reproduce, simply change the
MSTORE
this example:to
MSTORE8
:Then you will get:
The problem is that in
gasol-optimizer-0.2.0/sfs_generator/gasol_optimization.py
, the functionare_dependent(var1,var2,ins1,ins2)
expect thatvar1
andvar2
areint
, but somehow they are actuallystr
.