From d0abc5359b24a27376cc1a4ba8d0b35e7ca036d2 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 18 Dec 2017 19:43:15 +0100 Subject: [SMTChecker] Variables are merged after branches (ite variables) --- libsolidity/formal/SMTChecker.cpp | 32 +++++++++++++++++++++++++------- libsolidity/formal/SMTChecker.h | 18 ++++++++++++------ 2 files changed, 37 insertions(+), 13 deletions(-) (limited to 'libsolidity/formal') 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 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 _variables) } } +void SMTChecker::mergeVariables(vector const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse) +{ + set 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(_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; + + /// 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 _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 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; - /// 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) -- cgit v1.2.3