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

Merge pull request #5482 from ethereum/smt_refactor_sort_patch4

Browse Source 
[SMTChecker] Refactor setZeroValue and setUnknownValue
This commit is contained in:
Alex Beregszaszi 2018-11-22 16:08:10 +00:00 committed by GitHub
commit b0e4ef7a13
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 58 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
libsolidity/formal/SMTChecker.cpp
View File

@ -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)

2
libsolidity/formal/SMTChecker.h
View File

@ -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);

29
libsolidity/formal/SymbolicTypes.cpp
View File

@ -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<IntegerType const*>(_type.get());
solAssert(intType, "");
_interface.addAssertion(_expr >= minValue(*intType));
_interface.addAssertion(_expr <= maxValue(*intType));
}
}

10
libsolidity/formal/SymbolicTypes.h
View File

@ -55,5 +55,15 @@ std::pair<bool, std::shared_ptr<SymbolicVariable>> 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);
}
}
}

22
libsolidity/formal/SymbolicVariables.cpp
View File

@ -62,15 +62,6 @@ smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(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::Sort>(smt::Kind::Int));
}
void SymbolicIntVariable::setZeroValue()
{
m_interface.addAssertion(currentValue() == 0);
}
void SymbolicIntVariable::setUnknownValue()
{
auto intType = dynamic_cast<IntegerType const*>(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

21
libsolidity/formal/SymbolicVariables.h
View File

@ -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<SSAVariable> m_ssa = nullptr;
std::shared_ptr<SSAVariable> 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;
};