Fixes [TO BE SQUASHED]

This commit is contained in:
chriseth 2019-03-25 17:16:33 +01:00
parent cf09cd51f0
commit 1981f182e6

View File

@ -107,7 +107,7 @@ public:
case dev::solidity::Instruction::COINBASE: case dev::solidity::Instruction::COINBASE:
case dev::solidity::Instruction::CREATE: case dev::solidity::Instruction::CREATE:
case dev::solidity::Instruction::CREATE2: case dev::solidity::Instruction::CREATE2:
return ValueConstraint::bitRange(160, 0); return ValueConstraint::bitRange(159, 0);
case dev::solidity::Instruction::CALL: case dev::solidity::Instruction::CALL:
case dev::solidity::Instruction::CALLCODE: case dev::solidity::Instruction::CALLCODE:
@ -167,17 +167,22 @@ ValueConstraint ValueConstraint::bitRange(size_t _highest, size_t _lowest)
ValueConstraint ValueConstraint::valueFromBits(u256 _minBits, u256 _maxBits) ValueConstraint ValueConstraint::valueFromBits(u256 _minBits, u256 _maxBits)
{ {
int highestBit = highestBitSet(_maxBits); // If x fulfills the bit restriction, i.e. minb_i <= x_i <= maxb_i,
// then by monotonicity sum_i 2^i minb_i <= sum_i 2^i x_i <= sum_i 2^i maxb_i
// and thus _minBits and _maxBits are also valid value range constraints.
return ValueConstraint{ return ValueConstraint{
0, _minBits,
u256(-1) >> (255 - highestBit), _maxBits,
move(_minBits), _minBits,
move(_maxBits) _maxBits
}; };
} }
ValueConstraint ValueConstraint::bitsFromValue(u256 _minValue, u256 _maxValue) ValueConstraint ValueConstraint::bitsFromValue(u256 _minValue, u256 _maxValue)
{ {
if (_minValue == _maxValue)
return constant(_minValue);
int highestBit = highestBitSet(_maxValue); int highestBit = highestBitSet(_maxValue);
return ValueConstraint{ return ValueConstraint{
move(_minValue), move(_minValue),
@ -225,8 +230,8 @@ ValueConstraint ValueConstraint::operator-(ValueConstraint const& _other)
return ValueConstraint{}; // underflow return ValueConstraint{}; // underflow
else else
return bitsFromValue( return bitsFromValue(
maxValue - _other.minValue, minValue - _other.maxValue,
minValue - _other.maxValue maxValue - _other.minValue
); );
} }