From ec84a7dc9b7ed9cfd5b562ee570c6ad13bdfbeb7 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 22 Nov 2018 14:48:31 +0100 Subject: [SMTChecker] Refactor setZeroValue and setUnknownValue --- libsolidity/formal/SMTChecker.cpp | 18 ++++++++++++++---- libsolidity/formal/SMTChecker.h | 2 ++ libsolidity/formal/SymbolicTypes.cpp | 29 +++++++++++++++++++++++++++++ libsolidity/formal/SymbolicTypes.h | 10 ++++++++++ libsolidity/formal/SymbolicVariables.cpp | 22 ---------------------- libsolidity/formal/SymbolicVariables.h | 21 +++------------------ 6 files changed, 58 insertions(+), 44 deletions(-) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index caf7e5fa..bb9b498f 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -409,7 +409,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall) auto const& symbolicVar = m_specialVariables.at(gasLeft); unsigned index = symbolicVar->index(); // We set the current value to unknown anyway to add type constraints. - symbolicVar->setUnknownValue(); + setUnknownValue(*symbolicVar); if (index > 0) m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); } @@ -597,7 +597,7 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e { auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); m_specialVariables.emplace(_name, result.second); - result.second->setUnknownValue(); + setUnknownValue(*result.second); if (result.first) m_errorReporter.warning( _expr.location(), @@ -1071,13 +1071,23 @@ smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl) void SMTChecker::setZeroValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - m_variables.at(&_decl)->setZeroValue(); + setZeroValue(*m_variables.at(&_decl)); +} + +void SMTChecker::setZeroValue(SymbolicVariable& _variable) +{ + smt::setSymbolicZeroValue(_variable, *m_interface); } void SMTChecker::setUnknownValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - m_variables.at(&_decl)->setUnknownValue(); + setUnknownValue(*m_variables.at(&_decl)); +} + +void SMTChecker::setUnknownValue(SymbolicVariable& _variable) +{ + smt::setSymbolicUnknownValue(_variable, *m_interface); } smt::Expression SMTChecker::expr(Expression const& _e) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 8ead5564..5f51beb7 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -157,8 +157,10 @@ private: /// Sets the value of the declaration to zero. void setZeroValue(VariableDeclaration const& _decl); + void setZeroValue(SymbolicVariable& _variable); /// Resets the variable to an unknown value (in its range). void setUnknownValue(VariableDeclaration const& decl); + void setUnknownValue(SymbolicVariable& _variable); /// Returns the expression corresponding to the AST node. Throws if the expression does not exist. smt::Expression expr(Expression const& _e); diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index a12ab142..c297c807 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -169,3 +169,32 @@ smt::Expression dev::solidity::maxValue(IntegerType const& _type) { return smt::Expression(_type.maxValue()); } + +void dev::solidity::smt::setSymbolicZeroValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface) +{ + setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _interface); +} + +void dev::solidity::smt::setSymbolicZeroValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface) +{ + if (isInteger(_type->category())) + _interface.addAssertion(_expr == 0); + else if (isBool(_type->category())) + _interface.addAssertion(_expr == smt::Expression(false)); +} + +void dev::solidity::smt::setSymbolicUnknownValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface) +{ + setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _interface); +} + +void dev::solidity::smt::setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface) +{ + if (isInteger(_type->category())) + { + auto intType = dynamic_cast(_type.get()); + solAssert(intType, ""); + _interface.addAssertion(_expr >= minValue(*intType)); + _interface.addAssertion(_expr <= maxValue(*intType)); + } +} diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 6af2a0a0..984653b3 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -55,5 +55,15 @@ std::pair> newSymbolicVariable(Type cons smt::Expression minValue(IntegerType const& _type); smt::Expression maxValue(IntegerType const& _type); +namespace smt +{ + +void setSymbolicZeroValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface); +void setSymbolicZeroValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface); +void setSymbolicUnknownValue(SymbolicVariable const& _variable, smt::SolverInterface& _interface); +void setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface); + +} + } } diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 399e18f8..efaeb97a 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -62,15 +62,6 @@ smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const return m_interface.newVariable(uniqueSymbol(_index), make_shared(smt::Kind::Bool)); } -void SymbolicBoolVariable::setZeroValue() -{ - m_interface.addAssertion(currentValue() == smt::Expression(false)); -} - -void SymbolicBoolVariable::setUnknownValue() -{ -} - SymbolicIntVariable::SymbolicIntVariable( TypePointer _type, string const& _uniqueName, @@ -86,19 +77,6 @@ smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const return m_interface.newVariable(uniqueSymbol(_index), make_shared(smt::Kind::Int)); } -void SymbolicIntVariable::setZeroValue() -{ - m_interface.addAssertion(currentValue() == 0); -} - -void SymbolicIntVariable::setUnknownValue() -{ - auto intType = dynamic_cast(m_type.get()); - solAssert(intType, ""); - m_interface.addAssertion(currentValue() >= minValue(*intType)); - m_interface.addAssertion(currentValue() <= maxValue(*intType)); -} - SymbolicAddressVariable::SymbolicAddressVariable( string const& _uniqueName, smt::SolverInterface& _interface diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 13b944a5..fcf32760 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -64,20 +64,15 @@ public: unsigned index() const { return m_ssa->index(); } unsigned& index() { return m_ssa->index(); } - /// Sets the var to the default value of its type. - /// Inherited types must implement. - virtual void setZeroValue() = 0; - /// The unknown value is the full range of valid values. - /// It is sub-type dependent, but not mandatory. - virtual void setUnknownValue() {} + TypePointer const& type() const { return m_type; } protected: std::string uniqueSymbol(unsigned _index) const; - TypePointer m_type = nullptr; + TypePointer m_type; std::string m_uniqueName; smt::SolverInterface& m_interface; - std::shared_ptr m_ssa = nullptr; + std::shared_ptr m_ssa; }; /** @@ -92,11 +87,6 @@ public: smt::SolverInterface& _interface ); - /// Sets the var to false. - void setZeroValue(); - /// Does nothing since the SMT solver already knows the valid values for Bool. - void setUnknownValue(); - protected: smt::Expression valueAtIndex(int _index) const; }; @@ -113,11 +103,6 @@ public: smt::SolverInterface& _interface ); - /// Sets the var to 0. - void setZeroValue(); - /// Sets the variable to the full valid value range. - void setUnknownValue(); - protected: smt::Expression valueAtIndex(int _index) const; }; -- cgit