aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--libsolidity/formal/SMTChecker.cpp32
-rw-r--r--libsolidity/formal/SMTChecker.h18
-rw-r--r--test/libsolidity/SMTChecker.cpp47
3 files changed, 76 insertions, 21 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index a8529795..a64024b3 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -91,15 +91,16 @@ bool SMTChecker::visit(IfStatement const& _node)
checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
- visitBranch(_node.trueStatement(), expr(_node.condition()));
+ auto countersEndFalse = m_currentSequenceCounter;
+ auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
if (_node.falseStatement())
{
- visitBranch(*_node.falseStatement(), !expr(_node.condition()));
+ countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
}
- resetVariables(touchedVariables);
+ mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse);
return false;
}
@@ -506,12 +507,12 @@ void SMTChecker::assignment(Declaration const& _variable, smt::Expression const&
m_interface->addAssertion(newValue(_variable) == _value);
}
-void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
{
- visitBranch(_statement, &_condition);
+ return visitBranch(_statement, &_condition);
}
-void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
+SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
{
VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
@@ -522,7 +523,8 @@ void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const*
popPathCondition();
m_conditionalExecutionHappened = true;
- m_currentSequenceCounter = sequenceCountersStart;
+ std::swap(sequenceCountersStart, m_currentSequenceCounter);
+ return sequenceCountersStart;
}
void SMTChecker::checkCondition(
@@ -702,6 +704,22 @@ void SMTChecker::resetVariables(vector<Declaration const*> _variables)
}
}
+void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse)
+{
+ set<Declaration const*> uniqueVars(_variables.begin(), _variables.end());
+ for (auto const* decl: uniqueVars)
+ {
+ int trueCounter = _countersEndTrue.at(decl);
+ int falseCounter = _countersEndFalse.at(decl);
+ solAssert(trueCounter != falseCounter, "");
+ m_interface->addAssertion(newValue(*decl) == smt::Expression::ite(
+ _condition,
+ valueAtSequence(*decl, trueCounter),
+ valueAtSequence(*decl, falseCounter))
+ );
+ }
+}
+
bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
{
if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index d4c2cf6f..b57f0f96 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -75,10 +75,14 @@ private:
void assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location);
void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
- // Visits the branch given by the statement, pushes and pops the SMT checker.
- // @param _condition if present, asserts that this condition is true within the branch.
- void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
- void visitBranch(Statement const& _statement, smt::Expression _condition);
+ /// Maps a variable to an SSA index.
+ using VariableSequenceCounters = std::map<Declaration const*, int>;
+
+ /// Visits the branch given by the statement, pushes and pops the current path conditions.
+ /// @param _condition if present, asserts that this condition is true within the branch.
+ /// @returns the variable sequence counter after visiting the branch.
+ VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+ VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression _condition);
/// Check that a condition can be satisfied.
void checkCondition(
@@ -106,6 +110,10 @@ private:
void initializeLocalVariables(FunctionDefinition const& _function);
void resetVariables(std::vector<Declaration const*> _variables);
+ /// Given two different branches and the touched variables,
+ /// merge the touched variables into after-branch ite variables
+ /// using the branch condition as guard.
+ void mergeVariables(std::vector<Declaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse);
/// Tries to create an uninitialized variable and returns true on success.
/// This fails if the type is not supported.
bool createVariable(VariableDeclaration const& _varDecl);
@@ -134,8 +142,6 @@ private:
static smt::Expression minValue(IntegerType const& _t);
static smt::Expression maxValue(IntegerType const& _t);
- using VariableSequenceCounters = std::map<Declaration const*, int>;
-
/// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
smt::Expression expr(Expression const& _e);
/// Creates the expression (value can be arbitrary)
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 3a65aa43..2a1609cc 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -168,9 +168,9 @@ BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars)
CHECK_SUCCESS_NO_WARNINGS(text);
}
-BOOST_AUTO_TEST_CASE(branches_clear_variables)
+BOOST_AUTO_TEST_CASE(branches_merge_variables)
{
- // Only clears accessed variables
+ // Branch does not touch variable a
string text = R"(
contract C {
function f(uint x) public pure {
@@ -182,7 +182,7 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables)
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
- // It is just a plain clear and will not combine branches.
+ // Positive branch touches variable a, but assertion should still hold.
text = R"(
contract C {
function f(uint x) public pure {
@@ -194,8 +194,8 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables)
}
}
)";
- CHECK_WARNING(text, "Assertion violation happens here");
- // Clear also works on the else branch
+ CHECK_SUCCESS_NO_WARNINGS(text);
+ // Negative branch touches variable a, but assertion should still hold.
text = R"(
contract C {
function f(uint x) public pure {
@@ -208,8 +208,8 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables)
}
}
)";
- CHECK_WARNING(text, "Assertion violation happens here");
- // Variable is not cleared, if it is only read.
+ CHECK_SUCCESS_NO_WARNINGS(text);
+ // Variable is not merged, if it is only read.
text = R"(
contract C {
function f(uint x) public pure {
@@ -224,6 +224,36 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables)
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
+ // Variable is reset in both branches
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ uint a = 2;
+ if (x > 10) {
+ a = 3;
+ } else {
+ a = 3;
+ }
+ assert(a == 3);
+ }
+ }
+ )";
+ CHECK_SUCCESS_NO_WARNINGS(text);
+ // Variable is reset in both branches
+ text = R"(
+ contract C {
+ function f(uint x) public pure {
+ uint a = 2;
+ if (x > 10) {
+ a = 3;
+ } else {
+ a = 4;
+ }
+ assert(a >= 3);
+ }
+ }
+ )";
+ CHECK_SUCCESS_NO_WARNINGS(text);
}
BOOST_AUTO_TEST_CASE(branches_assert_condition)
@@ -262,7 +292,7 @@ BOOST_AUTO_TEST_CASE(branches_assert_condition)
CHECK_SUCCESS_NO_WARNINGS(text);
}
-BOOST_AUTO_TEST_CASE(ways_to_clear_variables)
+BOOST_AUTO_TEST_CASE(ways_to_merge_variables)
{
string text = R"(
contract C {
@@ -275,6 +305,7 @@ BOOST_AUTO_TEST_CASE(ways_to_clear_variables)
}
}
)";
+ CHECK_WARNING(text, "Assertion violation happens here");
text = R"(
contract C {
function f(uint x) public pure {
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-11 17:36:41 +0800