From f41591b3ddfd3e5c065271058dadb3c6b7f31bbb Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 17 Jan 2018 21:02:23 +0100 Subject: [SMTChecker] A little refactoring on SSA vars --- libsolidity/formal/SMTChecker.cpp | 81 +++++++++++++----------------- libsolidity/formal/SMTChecker.h | 12 ++--- libsolidity/formal/SSAVariable.cpp | 66 ++++++++++++++++++++++++ libsolidity/formal/SSAVariable.h | 79 +++++++++++++++++++++++++++++ libsolidity/formal/SymbolicIntVariable.cpp | 54 ++++++++++++++++++++ libsolidity/formal/SymbolicIntVariable.h | 51 +++++++++++++++++++ libsolidity/formal/SymbolicVariable.cpp | 38 ++++++++++++++ libsolidity/formal/SymbolicVariable.h | 68 +++++++++++++++++++++++++ 8 files changed, 395 insertions(+), 54 deletions(-) create mode 100644 libsolidity/formal/SSAVariable.cpp create mode 100644 libsolidity/formal/SSAVariable.h create mode 100644 libsolidity/formal/SymbolicIntVariable.cpp create mode 100644 libsolidity/formal/SymbolicIntVariable.h create mode 100644 libsolidity/formal/SymbolicVariable.cpp create mode 100644 libsolidity/formal/SymbolicVariable.h (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index a64024b3..37dce96c 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -23,6 +23,7 @@ #include #endif +#include #include #include @@ -69,8 +70,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function) // We only handle local variables, so we clear at the beginning of the function. // If we add storage variables, those should be cleared differently. m_interface->reset(); - m_currentSequenceCounter.clear(); - m_nextFreeSequenceCounter.clear(); + m_variables.clear(); m_pathConditions.clear(); m_conditionalExecutionHappened = false; initializeLocalVariables(_function); @@ -91,14 +91,18 @@ bool SMTChecker::visit(IfStatement const& _node) checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE."); - auto countersEndFalse = m_currentSequenceCounter; auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition())); vector touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement()); + decltype(countersEndTrue) countersEndFalse; if (_node.falseStatement()) { countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition())); touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement()); } + else + { + countersEndFalse = m_variables; + } mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse); @@ -152,7 +156,7 @@ bool SMTChecker::visit(ForStatement const& _node) checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE."); } - VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter; + VariableSequenceCounters sequenceCountersStart = m_variables; m_interface->push(); if (_node.condition()) m_interface->addAssertion(expr(*_node.condition())); @@ -163,7 +167,7 @@ bool SMTChecker::visit(ForStatement const& _node) m_interface->pop(); m_conditionalExecutionHappened = true; - m_currentSequenceCounter = sequenceCountersStart; + std::swap(sequenceCountersStart, m_variables); resetVariables(touchedVariables); @@ -514,7 +518,7 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) { - VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter; + VariableSequenceCounters beforeVars = m_variables; if (_condition) pushPathCondition(*_condition); @@ -523,8 +527,9 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s popPathCondition(); m_conditionalExecutionHappened = true; - std::swap(sequenceCountersStart, m_currentSequenceCounter); - return sequenceCountersStart; + std::swap(m_variables, beforeVars); + + return beforeVars; } void SMTChecker::checkCondition( @@ -709,8 +714,8 @@ void SMTChecker::mergeVariables(vector const& _variables, sm set uniqueVars(_variables.begin(), _variables.end()); for (auto const* decl: uniqueVars) { - int trueCounter = _countersEndTrue.at(decl); - int falseCounter = _countersEndFalse.at(decl); + int trueCounter = _countersEndTrue.at(decl).index(); + int falseCounter = _countersEndFalse.at(decl).index(); solAssert(trueCounter != falseCounter, ""); m_interface->addAssertion(newValue(*decl) == smt::Expression::ite( _condition, @@ -724,12 +729,8 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { if (dynamic_cast(_varDecl.type().get())) { - solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, ""); - solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, ""); solAssert(m_variables.count(&_varDecl) == 0, ""); - m_currentSequenceCounter[&_varDecl] = 0; - m_nextFreeSequenceCounter[&_varDecl] = 1; - m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int)); + m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface)); return true; } else @@ -742,11 +743,6 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) } } -string SMTChecker::uniqueSymbol(Declaration const& _decl) -{ - return _decl.name() + "_" + to_string(_decl.id()); -} - string SMTChecker::uniqueSymbol(Expression const& _expr) { return "expr_" + to_string(_expr.id()); @@ -754,48 +750,38 @@ string SMTChecker::uniqueSymbol(Expression const& _expr) bool SMTChecker::knownVariable(Declaration const& _decl) { - return m_currentSequenceCounter.count(&_decl); + return m_variables.count(&_decl); } smt::Expression SMTChecker::currentValue(Declaration const& _decl) { - solAssert(m_currentSequenceCounter.count(&_decl), ""); - return valueAtSequence(_decl, m_currentSequenceCounter.at(&_decl)); + solAssert(knownVariable(_decl), ""); + return m_variables.at(&_decl)(); } -smt::Expression SMTChecker::valueAtSequence(const Declaration& _decl, int _sequence) +smt::Expression SMTChecker::valueAtSequence(Declaration const& _decl, int _sequence) { - return var(_decl)(_sequence); + solAssert(knownVariable(_decl), ""); + return m_variables.at(&_decl)(_sequence); } smt::Expression SMTChecker::newValue(Declaration const& _decl) { - solAssert(m_nextFreeSequenceCounter.count(&_decl), ""); - m_currentSequenceCounter[&_decl] = m_nextFreeSequenceCounter[&_decl]++; - return currentValue(_decl); + solAssert(knownVariable(_decl), ""); + ++m_variables.at(&_decl); + return m_variables.at(&_decl)(); } void SMTChecker::setZeroValue(Declaration const& _decl) { - solAssert(_decl.type()->category() == Type::Category::Integer, ""); - m_interface->addAssertion(currentValue(_decl) == 0); + solAssert(knownVariable(_decl), ""); + m_variables.at(&_decl).setZeroValue(); } void SMTChecker::setUnknownValue(Declaration const& _decl) { - auto const& intType = dynamic_cast(*_decl.type()); - m_interface->addAssertion(currentValue(_decl) >= minValue(intType)); - m_interface->addAssertion(currentValue(_decl) <= maxValue(intType)); -} - -smt::Expression SMTChecker::minValue(IntegerType const& _t) -{ - return smt::Expression(_t.minValue()); -} - -smt::Expression SMTChecker::maxValue(IntegerType const& _t) -{ - return smt::Expression(_t.maxValue()); + solAssert(knownVariable(_decl), ""); + m_variables.at(&_decl).setUnknownValue(); } smt::Expression SMTChecker::expr(Expression const& _e) @@ -842,12 +828,15 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) m_interface->addAssertion(expr(_e) == _value); } -smt::Expression SMTChecker::var(Declaration const& _decl) +smt::Expression SMTChecker::minValue(IntegerType const& _t) { - solAssert(m_variables.count(&_decl), ""); - return m_variables.at(&_decl); + return smt::Expression(_t.minValue()); } +smt::Expression SMTChecker::maxValue(IntegerType const& _t) +{ + return smt::Expression(_t.maxValue()); +} void SMTChecker::popPathCondition() { solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty."); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index b57f0f96..7481e1c8 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -20,6 +20,8 @@ #include +#include + #include #include @@ -76,7 +78,7 @@ private: void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location); /// Maps a variable to an SSA index. - using VariableSequenceCounters = std::map; + 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. @@ -118,7 +120,6 @@ private: /// This fails if the type is not supported. bool createVariable(VariableDeclaration const& _varDecl); - static std::string uniqueSymbol(Declaration const& _decl); static std::string uniqueSymbol(Expression const& _expr); /// @returns true if _delc is a variable that is known at the current point, i.e. @@ -148,9 +149,6 @@ private: void createExpr(Expression const& _e); /// Creates the expression and sets its value. void defineExpr(Expression const& _e, smt::Expression _value); - /// Returns the function declaration corresponding to the given variable. - /// The function takes one argument which is the "sequence number". - smt::Expression var(Declaration const& _decl); /// Adds a new path condition void pushPathCondition(smt::Expression const& _e); @@ -166,10 +164,8 @@ private: std::shared_ptr m_interface; std::shared_ptr m_variableUsage; bool m_conditionalExecutionHappened = false; - std::map m_currentSequenceCounter; - std::map m_nextFreeSequenceCounter; std::map m_expressions; - std::map m_variables; + std::map m_variables; std::vector m_pathConditions; ErrorReporter& m_errorReporter; diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp new file mode 100644 index 00000000..d6e97a8d --- /dev/null +++ b/libsolidity/formal/SSAVariable.cpp @@ -0,0 +1,66 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#include + +#include + +#include + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SSAVariable::SSAVariable(Declaration const* _decl, + smt::SolverInterface& _interface) +{ + resetIndex(); + + if (dynamic_cast(_decl->type().get())) + m_symbVar = make_shared(_decl, _interface); + else + { + //solAssert(false, ""); + } +} + +void SSAVariable::resetIndex() +{ + m_currentSequenceCounter = 0; + m_nextFreeSequenceCounter.reset (new int); + *m_nextFreeSequenceCounter = 1; +} + +int SSAVariable::index() const +{ + return m_currentSequenceCounter; +} + +int SSAVariable::next() const +{ + return *m_nextFreeSequenceCounter; +} + +void SSAVariable::setZeroValue() +{ + m_symbVar->setZeroValue(index()); +} + +void SSAVariable::setUnknownValue() +{ + m_symbVar->setUnknownValue(index()); +} diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h new file mode 100644 index 00000000..3d7eb80c --- /dev/null +++ b/libsolidity/formal/SSAVariable.h @@ -0,0 +1,79 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#pragma once + +#include + +#include + +namespace dev +{ +namespace solidity +{ + +class Declaration; + +/** + * This class represents the SSA representation of a program variable. + */ +class SSAVariable +{ +public: + explicit SSAVariable(Declaration const* _decl, + smt::SolverInterface& _interface); + SSAVariable(SSAVariable const&) = default; + SSAVariable(SSAVariable&&) = default; + SSAVariable& operator=(SSAVariable const&) = default; + SSAVariable& operator=(SSAVariable&&) = default; + + void resetIndex(); + + int index() const; + int next() const; + + int operator++() + { + return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++; + } + + smt::Expression operator()() const + { + return valueAtSequence(index()); + } + + smt::Expression operator()(int _seq) const + { + return valueAtSequence(_seq); + } + + void setZeroValue(); + void setUnknownValue(); + +private: + smt::Expression valueAtSequence(int _seq) const + { + return (*m_symbVar)(_seq); + } + + std::shared_ptr m_symbVar = nullptr; + int m_currentSequenceCounter; + std::shared_ptr m_nextFreeSequenceCounter; +}; + +} +} diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp new file mode 100644 index 00000000..6ed7037f --- /dev/null +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -0,0 +1,54 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#include + +#include + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SymbolicIntVariable::SymbolicIntVariable(Declaration const* _decl, + smt::SolverInterface&_interface) + : SymbolicVariable(_decl, _interface) +{ + solAssert(m_declaration->type()->category() == Type::Category::Integer, ""); + m_expression = make_shared(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Int)); +} + +void SymbolicIntVariable::setZeroValue(int _seq) +{ + m_interface.addAssertion(valueAtSequence(_seq) == 0); +} + +void SymbolicIntVariable::setUnknownValue(int _seq) +{ + auto const& intType = dynamic_cast(*m_declaration->type()); + m_interface.addAssertion(valueAtSequence(_seq) >= minValue(intType)); + m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(intType)); +} + +smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t) const +{ + return smt::Expression(_t.minValue()); +} + +smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t) const +{ + return smt::Expression(_t.maxValue()); +} diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h new file mode 100644 index 00000000..efe05af8 --- /dev/null +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -0,0 +1,51 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#pragma once + +#include + +#include + +namespace dev +{ +namespace solidity +{ + +/** + * Specialization of SymbolicVariable for Integers + */ +class SymbolicIntVariable : public SymbolicVariable +{ +public: + explicit SymbolicIntVariable(Declaration const* _decl, + smt::SolverInterface& _interface); + SymbolicIntVariable(SymbolicIntVariable const&) = default; + SymbolicIntVariable(SymbolicIntVariable&&) = default; + SymbolicIntVariable& operator=(SymbolicIntVariable const&) = default; + SymbolicIntVariable& operator=(SymbolicIntVariable&&) = default; + + void setZeroValue(int _seq); + void setUnknownValue(int _seq); + +private: + smt::Expression minValue(IntegerType const& _t) const; + smt::Expression maxValue(IntegerType const& _t) const; +}; + +} +} diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp new file mode 100644 index 00000000..13f5d9b6 --- /dev/null +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -0,0 +1,38 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#include + +#include + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SymbolicVariable::SymbolicVariable(Declaration const* _decl, + smt::SolverInterface& _interface) + : m_declaration(_decl), + m_interface(_interface) +{ +} + +string SymbolicVariable::uniqueSymbol() const +{ + return m_declaration->name() + "_" + to_string(m_declaration->id()); +} + + diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h new file mode 100644 index 00000000..4de59504 --- /dev/null +++ b/libsolidity/formal/SymbolicVariable.h @@ -0,0 +1,68 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#pragma once + +#include + +#include + +#include + +namespace dev +{ +namespace solidity +{ + +class Declaration; + +/** + * This class represents the symbolic version of a program variable. + */ +class SymbolicVariable +{ +public: + explicit SymbolicVariable(Declaration const* _decl, + smt::SolverInterface& _interface); + SymbolicVariable(SymbolicVariable const&) = default; + SymbolicVariable(SymbolicVariable&&) = default; + SymbolicVariable& operator=(SymbolicVariable const&) = default; + SymbolicVariable& operator=(SymbolicVariable&&) = default; + + smt::Expression operator()(int _seq) const + { + return valueAtSequence(_seq); + } + + std::string uniqueSymbol() const; + + virtual void setZeroValue(int _seq) = 0; + virtual void setUnknownValue(int _seq) = 0; + +protected: + smt::Expression valueAtSequence(int _seq) const + { + return (*m_expression)(_seq); + } + + Declaration const* m_declaration; + std::shared_ptr m_expression = nullptr; + smt::SolverInterface& m_interface; +}; + +} +} -- cgit From 3b2851ee4163bcfbca9e4e23650dfeee1a06653a Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Sat, 17 Feb 2018 09:34:38 +0100 Subject: Integer min and max values placed under SymbolicIntVar instead of SMTChecker --- libsolidity/formal/SMTChecker.cpp | 14 +++----------- libsolidity/formal/SMTChecker.h | 3 --- libsolidity/formal/SymbolicIntVariable.cpp | 4 ++-- libsolidity/formal/SymbolicIntVariable.h | 7 ++++--- 4 files changed, 9 insertions(+), 19 deletions(-) (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 37dce96c..ad42c105 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -24,6 +24,7 @@ #endif #include +#include #include #include @@ -244,14 +245,14 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location) { checkCondition( - _value < minValue(_type), + _value < SymbolicIntVariable::minValue(_type), _location, "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")", "value", &_value ); checkCondition( - _value > maxValue(_type), + _value > SymbolicIntVariable::maxValue(_type), _location, "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")", "value", @@ -828,15 +829,6 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) m_interface->addAssertion(expr(_e) == _value); } -smt::Expression SMTChecker::minValue(IntegerType const& _t) -{ - return smt::Expression(_t.minValue()); -} - -smt::Expression SMTChecker::maxValue(IntegerType const& _t) -{ - return smt::Expression(_t.maxValue()); -} void SMTChecker::popPathCondition() { solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty."); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 7481e1c8..7e7996cf 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -140,9 +140,6 @@ private: /// Resets the variable to an unknown value (in its range). void setUnknownValue(Declaration const& decl); - static smt::Expression minValue(IntegerType const& _t); - static smt::Expression maxValue(IntegerType const& _t); - /// 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/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp index 6ed7037f..c206f1cd 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -43,12 +43,12 @@ void SymbolicIntVariable::setUnknownValue(int _seq) m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(intType)); } -smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t) const +smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t) { return smt::Expression(_t.minValue()); } -smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t) const +smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t) { return smt::Expression(_t.maxValue()); } diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index efe05af8..0066bb75 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -39,12 +39,13 @@ public: SymbolicIntVariable& operator=(SymbolicIntVariable const&) = default; SymbolicIntVariable& operator=(SymbolicIntVariable&&) = default; + /// Sets the var to 0. void setZeroValue(int _seq); + /// Sets the valid interval for the var. void setUnknownValue(int _seq); -private: - smt::Expression minValue(IntegerType const& _t) const; - smt::Expression maxValue(IntegerType const& _t) const; + static smt::Expression minValue(IntegerType const& _t); + static smt::Expression maxValue(IntegerType const& _t); }; } -- cgit From 21c6b80fc98f6d584f240a47d4a01827768f18f3 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Sat, 17 Feb 2018 09:35:37 +0100 Subject: Supported types listed in SSAVariable --- libsolidity/formal/SMTChecker.cpp | 4 ++-- libsolidity/formal/SSAVariable.cpp | 7 ++++++- libsolidity/formal/SSAVariable.h | 9 +++++++++ libsolidity/formal/SymbolicVariable.h | 3 +++ 4 files changed, 20 insertions(+), 3 deletions(-) (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index ad42c105..1da5b291 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -370,7 +370,7 @@ void SMTChecker::endVisit(Identifier const& _identifier) { // Will be translated as part of the node that requested the lvalue. } - else if (dynamic_cast(_identifier.annotation().type.get())) + else if (SSAVariable::supportedType(_identifier.annotation().type.get())) defineExpr(_identifier, currentValue(*decl)); else if (FunctionType const* fun = dynamic_cast(_identifier.annotation().type.get())) { @@ -728,7 +728,7 @@ void SMTChecker::mergeVariables(vector const& _variables, sm bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { - if (dynamic_cast(_varDecl.type().get())) + if (SSAVariable::supportedType(_varDecl.type().get())) { solAssert(m_variables.count(&_varDecl) == 0, ""); m_variables.emplace(&_varDecl, SSAVariable(&_varDecl, *m_interface)); diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index d6e97a8d..7f214687 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -34,10 +34,15 @@ SSAVariable::SSAVariable(Declaration const* _decl, m_symbVar = make_shared(_decl, _interface); else { - //solAssert(false, ""); + solAssert(false, ""); } } +bool SSAVariable::supportedType(Type const* _decl) +{ + return dynamic_cast(_decl); +} + void SSAVariable::resetIndex() { m_currentSequenceCounter = 0; diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index 3d7eb80c..b87693c2 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -34,6 +34,8 @@ class Declaration; class SSAVariable { public: + /// @param _decl Used to determine the type and forwarded to the symbolic var. + /// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver. explicit SSAVariable(Declaration const* _decl, smt::SolverInterface& _interface); SSAVariable(SSAVariable const&) = default; @@ -61,9 +63,14 @@ public: return valueAtSequence(_seq); } + /// These two functions forward the call to the symbolic var + /// which generates the constraints according to the type. void setZeroValue(); void setUnknownValue(); + /// So far Int is supported. + static bool supportedType(Type const* _decl); + private: smt::Expression valueAtSequence(int _seq) const { @@ -72,6 +79,8 @@ private: std::shared_ptr m_symbVar = nullptr; int m_currentSequenceCounter; + /// The next free sequence counter is a shared pointer because we want + /// the copy and the copied to share it. std::shared_ptr m_nextFreeSequenceCounter; }; diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h index 4de59504..66633b73 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -50,7 +50,10 @@ public: std::string uniqueSymbol() const; + /// Sets the var to the default value of its type. virtual void setZeroValue(int _seq) = 0; + /// The unknown value depends on the type. For example, an interval is set for Integers. + /// This is decided by the subclasses. virtual void setUnknownValue(int _seq) = 0; protected: -- cgit From cff0836c032ecee2710f1c17c49eec0a3b4aa9fc Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 28 Feb 2018 18:00:13 +0100 Subject: Fix PR comments --- libsolidity/formal/SSAVariable.cpp | 12 +++++++----- libsolidity/formal/SSAVariable.h | 12 ++++++++---- libsolidity/formal/SymbolicIntVariable.cpp | 8 +++++--- libsolidity/formal/SymbolicIntVariable.h | 10 ++++++---- libsolidity/formal/SymbolicVariable.cpp | 8 +++++--- libsolidity/formal/SymbolicVariable.h | 10 ++++++---- 6 files changed, 37 insertions(+), 23 deletions(-) (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index 7f214687..4e6bcbcb 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -25,13 +25,15 @@ using namespace std; using namespace dev; using namespace dev::solidity; -SSAVariable::SSAVariable(Declaration const* _decl, - smt::SolverInterface& _interface) +SSAVariable::SSAVariable( + Declaration const* _decl, + smt::SolverInterface& _interface +) { resetIndex(); if (dynamic_cast(_decl->type().get())) - m_symbVar = make_shared(_decl, _interface); + m_symbolicVar = make_shared(_decl, _interface); else { solAssert(false, ""); @@ -62,10 +64,10 @@ int SSAVariable::next() const void SSAVariable::setZeroValue() { - m_symbVar->setZeroValue(index()); + m_symbolicVar->setZeroValue(index()); } void SSAVariable::setUnknownValue() { - m_symbVar->setUnknownValue(index()); + m_symbolicVar->setUnknownValue(index()); } diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index b87693c2..4ec92aa1 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -36,8 +36,10 @@ class SSAVariable public: /// @param _decl Used to determine the type and forwarded to the symbolic var. /// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver. - explicit SSAVariable(Declaration const* _decl, - smt::SolverInterface& _interface); + SSAVariable( + Declaration const* _decl, + smt::SolverInterface& _interface + ); SSAVariable(SSAVariable const&) = default; SSAVariable(SSAVariable&&) = default; SSAVariable& operator=(SSAVariable const&) = default; @@ -45,7 +47,9 @@ public: void resetIndex(); + /// This function returns the current index of this SSA variable. int index() const; + /// This function returns the next free index of this SSA variable. int next() const; int operator++() @@ -74,10 +78,10 @@ public: private: smt::Expression valueAtSequence(int _seq) const { - return (*m_symbVar)(_seq); + return (*m_symbolicVar)(_seq); } - std::shared_ptr m_symbVar = nullptr; + std::shared_ptr m_symbolicVar = nullptr; int m_currentSequenceCounter; /// The next free sequence counter is a shared pointer because we want /// the copy and the copied to share it. diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp index c206f1cd..d08dc155 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -23,9 +23,11 @@ using namespace std; using namespace dev; using namespace dev::solidity; -SymbolicIntVariable::SymbolicIntVariable(Declaration const* _decl, - smt::SolverInterface&_interface) - : SymbolicVariable(_decl, _interface) +SymbolicIntVariable::SymbolicIntVariable( + Declaration const* _decl, + smt::SolverInterface& _interface +): + SymbolicVariable(_decl, _interface) { solAssert(m_declaration->type()->category() == Type::Category::Integer, ""); m_expression = make_shared(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Int)); diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index 0066bb75..8a9b5d5d 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -29,11 +29,13 @@ namespace solidity /** * Specialization of SymbolicVariable for Integers */ -class SymbolicIntVariable : public SymbolicVariable +class SymbolicIntVariable: public SymbolicVariable { public: - explicit SymbolicIntVariable(Declaration const* _decl, - smt::SolverInterface& _interface); + SymbolicIntVariable( + Declaration const* _decl, + smt::SolverInterface& _interface + ); SymbolicIntVariable(SymbolicIntVariable const&) = default; SymbolicIntVariable(SymbolicIntVariable&&) = default; SymbolicIntVariable& operator=(SymbolicIntVariable const&) = default; @@ -41,7 +43,7 @@ public: /// Sets the var to 0. void setZeroValue(int _seq); - /// Sets the valid interval for the var. + /// Sets the variable to the full valid value range. void setUnknownValue(int _seq); static smt::Expression minValue(IntegerType const& _t); diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp index 13f5d9b6..629049ea 100644 --- a/libsolidity/formal/SymbolicVariable.cpp +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -23,9 +23,11 @@ using namespace std; using namespace dev; using namespace dev::solidity; -SymbolicVariable::SymbolicVariable(Declaration const* _decl, - smt::SolverInterface& _interface) - : m_declaration(_decl), +SymbolicVariable::SymbolicVariable( + Declaration const* _decl, + smt::SolverInterface& _interface +): + m_declaration(_decl), m_interface(_interface) { } diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h index 66633b73..2b59e57a 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -36,8 +36,10 @@ class Declaration; class SymbolicVariable { public: - explicit SymbolicVariable(Declaration const* _decl, - smt::SolverInterface& _interface); + SymbolicVariable( + Declaration const* _decl, + smt::SolverInterface& _interface + ); SymbolicVariable(SymbolicVariable const&) = default; SymbolicVariable(SymbolicVariable&&) = default; SymbolicVariable& operator=(SymbolicVariable const&) = default; @@ -52,8 +54,8 @@ public: /// Sets the var to the default value of its type. virtual void setZeroValue(int _seq) = 0; - /// The unknown value depends on the type. For example, an interval is set for Integers. - /// This is decided by the subclasses. + /// The unknown value is the full range of valid values, + /// and that's sub-type dependent. virtual void setUnknownValue(int _seq) = 0; protected: -- cgit From 8b1b4b78c043d54f493dc9e2330bf9df5cf93755 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 28 Feb 2018 18:31:11 +0100 Subject: Fix PR comments --- libsolidity/formal/SSAVariable.h | 4 ---- libsolidity/formal/SymbolicIntVariable.h | 4 ---- libsolidity/formal/SymbolicVariable.h | 4 ---- 3 files changed, 12 deletions(-) (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index 4ec92aa1..275e8590 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -40,10 +40,6 @@ public: Declaration const* _decl, smt::SolverInterface& _interface ); - SSAVariable(SSAVariable const&) = default; - SSAVariable(SSAVariable&&) = default; - SSAVariable& operator=(SSAVariable const&) = default; - SSAVariable& operator=(SSAVariable&&) = default; void resetIndex(); diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index 8a9b5d5d..afa25f1b 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -36,10 +36,6 @@ public: Declaration const* _decl, smt::SolverInterface& _interface ); - SymbolicIntVariable(SymbolicIntVariable const&) = default; - SymbolicIntVariable(SymbolicIntVariable&&) = default; - SymbolicIntVariable& operator=(SymbolicIntVariable const&) = default; - SymbolicIntVariable& operator=(SymbolicIntVariable&&) = default; /// Sets the var to 0. void setZeroValue(int _seq); diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h index 2b59e57a..93258250 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -40,10 +40,6 @@ public: Declaration const* _decl, smt::SolverInterface& _interface ); - SymbolicVariable(SymbolicVariable const&) = default; - SymbolicVariable(SymbolicVariable&&) = default; - SymbolicVariable& operator=(SymbolicVariable const&) = default; - SymbolicVariable& operator=(SymbolicVariable&&) = default; smt::Expression operator()(int _seq) const { -- cgit