cerc-io/solidity
11
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

[SMTChecker] Support check/unchecked

Browse Source
This commit is contained in:
Leonardo Alt
2020-12-30 12:14:30 +01:00
parent eb05826857
commit 78d55e6b4a
74 changed files with 765 additions and 614 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+17 -15
View File
@@ -137,8 +137,7 @@ void BMC::endVisit(ContractDefinition const& _contract)
inlineConstructorHierarchy(_contract);
popCallStack();
/// Check targets created by state variable initialization.
smtutil::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
checkVerificationTargets();
m_verificationTargets.clear();
}
@@ -175,8 +174,7 @@ void BMC::endVisit(FunctionDefinition const& _function)
{
if (isRootFunction())
{
smtutil::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
checkVerificationTargets();
m_verificationTargets.clear();
m_pathConditions.clear();
}
@@ -534,6 +532,7 @@ pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
Expression const& _expression
)
{
// Unchecked does not disable div by 0 checks.
if (_op == Token::Div || _op == Token::Mod)
addVerificationTarget(
VerificationTarget::Type::DivByZero,
@@ -543,6 +542,9 @@ pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
if (!m_checked)
return values;
auto const* intType = dynamic_cast<IntegerType const*>(_commonType);
if (!intType)
intType = TypeProvider::uint256();
@@ -625,13 +627,13 @@ pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
/// Verification targets.
void BMC::checkVerificationTargets(smtutil::Expression const& _constraints)
void BMC::checkVerificationTargets()
{
for (auto& target: m_verificationTargets)
checkVerificationTarget(target, _constraints);
checkVerificationTarget(target);
}
void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
void BMC::checkVerificationTarget(BMCVerificationTarget& _target)
{
switch (_target.type)
{
@@ -639,14 +641,14 @@ void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expre
checkConstantCondition(_target);
break;
case VerificationTarget::Type::Underflow:
checkUnderflow(_target, _constraints);
checkUnderflow(_target);
break;
case VerificationTarget::Type::Overflow:
checkOverflow(_target, _constraints);
checkOverflow(_target);
break;
case VerificationTarget::Type::UnderOverflow:
checkUnderflow(_target, _constraints);
checkOverflow(_target, _constraints);
checkUnderflow(_target);
checkOverflow(_target);
break;
case VerificationTarget::Type::DivByZero:
checkDivByZero(_target);
@@ -672,7 +674,7 @@ void BMC::checkConstantCondition(BMCVerificationTarget& _target)
);
}
void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
void BMC::checkUnderflow(BMCVerificationTarget& _target)
{
solAssert(
_target.type == VerificationTarget::Type::Underflow ||
@@ -693,7 +695,7 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression con
intType = TypeProvider::uint256();
checkCondition(
_target.constraints && _constraints && _target.value < smt::minValue(*intType),
_target.constraints && _target.value < smt::minValue(*intType),
_target.callStack,
_target.modelExpressions,
_target.expression->location(),
@@ -705,7 +707,7 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression con
);
}
void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
void BMC::checkOverflow(BMCVerificationTarget& _target)
{
solAssert(
_target.type == VerificationTarget::Type::Overflow ||
@@ -726,7 +728,7 @@ void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression cons
intType = TypeProvider::uint256();
checkCondition(
_target.constraints && _constraints && _target.value > smt::maxValue(*intType),
_target.constraints && _target.value > smt::maxValue(*intType),
_target.callStack,
_target.modelExpressions,
_target.expression->location(),
libsolidity/formal/BMC.h
+4 -4
View File
@@ -130,11 +130,11 @@ private:
std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> modelExpressions;
};
void checkVerificationTargets(smtutil::Expression const& _constraints);
void checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expression const& _constraints = smtutil::Expression(true));
void checkVerificationTargets();
void checkVerificationTarget(BMCVerificationTarget& _target);
void checkConstantCondition(BMCVerificationTarget& _target);
void checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints);
void checkOverflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints);
void checkUnderflow(BMCVerificationTarget& _target);
void checkOverflow(BMCVerificationTarget& _target);
void checkDivByZero(BMCVerificationTarget& _target);
void checkBalance(BMCVerificationTarget& _target);
void checkAssert(BMCVerificationTarget& _target);
libsolidity/formal/CHC.cpp
+4
View File
@@ -732,11 +732,15 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
frontend::Expression const& _expression
)
{
// Unchecked does not disable div by 0 checks.
if (_op == Token::Mod || _op == Token::Div)
verificationTargetEncountered(&_expression, VerificationTarget::Type::DivByZero, _right == 0);
auto values = SMTEncoder::arithmeticOperation(_op, _left, _right, _commonType, _expression);
if (!m_checked)
return values;
IntegerType const* intType = nullptr;
if (auto const* type = dynamic_cast<IntegerType const*>(_commonType))
intType = type;
libsolidity/formal/SMTEncoder.cpp
+34
View File
@@ -283,6 +283,25 @@ void SMTEncoder::endVisit(FunctionDefinition const&)
m_context.popSolver();
}
bool SMTEncoder::visit(Block const& _block)
{
if (_block.unchecked())
{
solAssert(m_checked, "");
m_checked = false;
}
return true;
}
void SMTEncoder::endVisit(Block const& _block)
{
if (_block.unchecked())
{
solAssert(!m_checked, "");
m_checked = true;
}
}
bool SMTEncoder::visit(InlineAssembly const& _inlineAsm)
{
m_errorReporter.warning(
@@ -745,6 +764,7 @@ void SMTEncoder::initContract(ContractDefinition const& _contract)
createStateVariables(_contract);
clearIndices(m_currentContract, nullptr);
m_variableUsage.setCurrentContract(_contract);
m_checked = true;
}
void SMTEncoder::initFunction(FunctionDefinition const& _function)
@@ -759,6 +779,7 @@ void SMTEncoder::initFunction(FunctionDefinition const& _function)
createLocalVariables(_function);
m_arrayAssignmentHappened = false;
clearIndices(m_currentContract, &_function);
m_checked = true;
}
void SMTEncoder::visitAssert(FunctionCall const& _funCall)
@@ -1762,6 +1783,9 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
}
}();
if (m_checked)
return {valueUnbounded, valueUnbounded};
if (_op == Token::Div || _op == Token::Mod)
{
// mod and unsigned division never underflow/overflow
@@ -2385,6 +2409,16 @@ void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value)
createExpr(_e);
solAssert(_value.sort->kind != smtutil::Kind::Function, "Equality operator applied to type that is not fully supported");
m_context.addAssertion(expr(_e) == _value);
if (
auto type = _e.annotation().type;
m_checked && smt::isNumber(*type)
)
m_context.addAssertion(smtutil::Expression::implies(
currentPathConditions(),
smt::symbolicUnknownConstraints(expr(_e), type)
));
}
void SMTEncoder::popPathCondition()
libsolidity/formal/SMTEncoder.h
+7
View File
@@ -103,6 +103,8 @@ protected:
bool visit(ModifierDefinition const& _node) override;
bool visit(FunctionDefinition const& _node) override;
void endVisit(FunctionDefinition const& _node) override;
bool visit(Block const& _node) override;
void endVisit(Block const& _node) override;
bool visit(PlaceholderStatement const& _node) override;
bool visit(IfStatement const&) override { return false; }
bool visit(WhileStatement const&) override { return false; }
@@ -358,6 +360,11 @@ protected:
/// Used to retrieve models.
std::set<Expression const*> m_uninterpretedTerms;
std::vector<smtutil::Expression> m_pathConditions;
/// Whether the currently visited block uses checked
/// or unchecked arithmetic.
bool m_checked = true;
/// Local SMTEncoder ErrorReporter.
/// This is necessary to show the "No SMT solver available"
/// warning before the others in case it's needed.