This commit is contained in:
chriseth 2022-03-03 20:10:53 +01:00
parent 1efa03201d
commit aa1e56bf2c
3 changed files with 17 additions and 12 deletions

View File

@ -160,8 +160,8 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
// 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 `signedToTwosComplement` // representation 2**255 in `signedToTwosComplement`
signedToTwosComplement(smtutil::signedDivisionEVM( signedToTwosComplement(smtutil::signedDivisionEVM(
twosComplementToSigned(arguments.at(0)), twosComplementToUpscaledUnsigned(arguments.at(0)),
twosComplementToSigned(arguments.at(1)) twosComplementToUpscaledUnsigned(arguments.at(1))
)) ))
); );
case evmasm::Instruction::MOD: case evmasm::Instruction::MOD:
@ -175,18 +175,24 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
arguments.at(1) == constantValue(0), arguments.at(1) == constantValue(0),
constantValue(0), constantValue(0),
signedToTwosComplement(signedModuloEVM( signedToTwosComplement(signedModuloEVM(
twosComplementToSigned(arguments.at(0)), twosComplementToUpscaledUnsigned(arguments.at(0)),
twosComplementToSigned(arguments.at(1)) twosComplementToUpscaledUnsigned(arguments.at(1))
)) ))
); );
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:
return booleanValue(twosComplementToSigned(arguments.at(0)) < twosComplementToSigned(arguments.at(1))); return booleanValue(
twosComplementToUpscaledUnsigned(arguments.at(0)) + smtutil::Expression(bigint(1) << 256) <
twosComplementToUpscaledUnsigned(arguments.at(1)) + smtutil::Expression(bigint(1) << 256)
);
case evmasm::Instruction::GT: case evmasm::Instruction::GT:
return booleanValue(arguments.at(0) > arguments.at(1)); return booleanValue(arguments.at(0) > arguments.at(1));
case evmasm::Instruction::SGT: case evmasm::Instruction::SGT:
return booleanValue(twosComplementToSigned(arguments.at(0)) > twosComplementToSigned(arguments.at(1))); return booleanValue(
twosComplementToUpscaledUnsigned(arguments.at(0)) + smtutil::Expression(bigint(1) << 256) >
twosComplementToUpscaledUnsigned(arguments.at(1)) + smtutil::Expression(bigint(1) << 256)
);
case evmasm::Instruction::EQ: case evmasm::Instruction::EQ:
return booleanValue(arguments.at(0) == arguments.at(1)); return booleanValue(arguments.at(0) == arguments.at(1));
case evmasm::Instruction::ISZERO: case evmasm::Instruction::ISZERO:

View File

@ -105,7 +105,6 @@ shared_ptr<Sort> SMTSolver::defaultSort() const
smtutil::Expression SMTSolver::booleanValue(smtutil::Expression _value) smtutil::Expression SMTSolver::booleanValue(smtutil::Expression _value)
{ {
// TODO should not use ite
return smtutil::Expression::ite(_value, constantValue(1), constantValue(0)); return smtutil::Expression::ite(_value, constantValue(1), constantValue(0));
} }
@ -119,13 +118,12 @@ smtutil::Expression SMTSolver::literalValue(Literal const& _literal)
return smtutil::Expression(valueOfLiteral(_literal)); return smtutil::Expression(valueOfLiteral(_literal));
} }
smtutil::Expression SMTSolver::twosComplementToSigned(smtutil::Expression _value) smtutil::Expression SMTSolver::twosComplementToUpscaledUnsigned(smtutil::Expression _value)
{ {
// TODO will that work for LP?
return smtutil::Expression::ite( return smtutil::Expression::ite(
_value < smtutil::Expression(bigint(1) << 255), _value < smtutil::Expression(bigint(1) << 255),
_value, _value + smtutil::Expression(bigint(1) << 256),
_value - smtutil::Expression(bigint(1) << 256) _value
); );
} }

View File

@ -76,7 +76,8 @@ protected:
static smtutil::Expression booleanValue(smtutil::Expression _value); static smtutil::Expression booleanValue(smtutil::Expression _value);
static smtutil::Expression constantValue(bigint _value); static smtutil::Expression constantValue(bigint _value);
static smtutil::Expression literalValue(Literal const& _literal); static smtutil::Expression literalValue(Literal const& _literal);
static smtutil::Expression twosComplementToSigned(smtutil::Expression _value); /// Returns _value interpreted as a two's complement number and adds 2**256
static smtutil::Expression twosComplementToUpscaledUnsigned(smtutil::Expression _value);
static smtutil::Expression signedToTwosComplement(smtutil::Expression _value); static smtutil::Expression signedToTwosComplement(smtutil::Expression _value);
smtutil::Expression wrap(smtutil::Expression _value); smtutil::Expression wrap(smtutil::Expression _value);