cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Small fixes wrt ReasoningBasedSimplifier.

Browse Source
This commit is contained in:
chriseth 2020-09-16 18:08:54 +02:00
parent ef0760614d
commit 6e2d2feb10
3 changed files with 5 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsmtutil/Helpers.h
View File

@ -25,7 +25,7 @@ namespace solidity::smtutil
/// Signed division in SMTLIB2 rounds differently than EVM. /// Signed division in SMTLIB2 rounds differently than EVM.
/// This does not check for division by zero! /// This does not check for division by zero!
inline Expression signedDivision(Expression _left, Expression _right) inline Expression signedDivisionEVM(Expression _left, Expression _right)
{ {
return Expression::ite( return Expression::ite(
_left >= 0, _left >= 0,
@ -42,7 +42,7 @@ inline Expression abs(Expression _value)
/// Signed modulo in SMTLIB2 behaves differently with regards /// Signed modulo in SMTLIB2 behaves differently with regards
/// to the sign than EVM. /// to the sign than EVM.
/// This does not check for modulo by zero! /// This does not check for modulo by zero!
inline Expression signedModulo(Expression _left, Expression _right) inline Expression signedModuloEVM(Expression _left, Expression _right)
{ {
return Expression::ite( return Expression::ite(
_left >= 0, _left >= 0,

2
libsolidity/formal/SMTEncoder.cpp
View File

@ -1506,7 +1506,7 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp
{ {
// Signed division in SMTLIB2 rounds differently for negative division. // Signed division in SMTLIB2 rounds differently for negative division.
if (_type.isSigned()) if (_type.isSigned())
return signedDivision(_left, _right); return signedDivisionEVM(_left, _right);
else else
return _left / _right; return _left / _right;
} }

6
libyul/optimiser/ReasoningBasedSimplifier.cpp
View File

@ -176,12 +176,11 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
// No `wrap()` needed here, because -2**255 / -1 results // No `wrap()` needed here, because -2**255 / -1 results
// in 2**255 which is "converted" to its two's complement // in 2**255 which is "converted" to its two's complement
// representation 2**255 in `signedToUnsigned` // representation 2**255 in `signedToUnsigned`
signedToUnsigned(smtutil::signedDivision( signedToUnsigned(smtutil::signedDivisionEVM(
unsignedToSigned(arguments.at(0)), unsignedToSigned(arguments.at(0)),
unsignedToSigned(arguments.at(1)) unsignedToSigned(arguments.at(1))
)) ))
); );
break;
case evmasm::Instruction::MOD: case evmasm::Instruction::MOD:
return smtutil::Expression::ite( return smtutil::Expression::ite(
arguments.at(1) == constantValue(0), arguments.at(1) == constantValue(0),
@ -192,12 +191,11 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
return smtutil::Expression::ite( return smtutil::Expression::ite(
arguments.at(1) == constantValue(0), arguments.at(1) == constantValue(0),
constantValue(0), constantValue(0),
signedToUnsigned(signedModulo( signedToUnsigned(signedModuloEVM(
unsignedToSigned(arguments.at(0)), unsignedToSigned(arguments.at(0)),
unsignedToSigned(arguments.at(1)) unsignedToSigned(arguments.at(1))
)) ))
); );
break;
case evmasm::Instruction::LT: case evmasm::Instruction::LT:
return booleanValue(arguments.at(0) < arguments.at(1)); return booleanValue(arguments.at(0) < arguments.at(1));
case evmasm::Instruction::SLT: case evmasm::Instruction::SLT: