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 #7040 from ethereum/smt_context_vars

Browse Source 
[SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars
This commit is contained in:
Mathias L. Baumann 2019-07-04 09:46:28 +02:00 committed by GitHub
commit 3b2ebba472
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
10 changed files with 92 additions and 84 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/BMC.cpp
View File

@ -459,7 +459,7 @@ void BMC::abstractFunctionCall(FunctionCall const& _funCall)
smtArguments.push_back(expr(*arg));
defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments));
m_uninterpretedTerms.insert(&_funCall);
setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_context.solver());
setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, m_context);
}
void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)

14
libsolidity/formal/EncodingContext.cpp
View File

@ -24,14 +24,14 @@ using namespace dev;
using namespace dev::solidity::smt;
EncodingContext::EncodingContext(std::shared_ptr<SolverInterface> _solver):
m_thisAddress(make_unique<SymbolicAddressVariable>("this", *_solver)),
m_thisAddress(make_unique<SymbolicAddressVariable>("this", *this)),
m_solver(_solver)
{
auto sort = make_shared<ArraySort>(
make_shared<Sort>(Kind::Int),
make_shared<Sort>(Kind::Int)
);
m_balances = make_unique<SymbolicVariable>(sort, "balances", *m_solver);
m_balances = make_unique<SymbolicVariable>(sort, "balances", *this);
}
void EncodingContext::reset()
@ -56,7 +56,7 @@ bool EncodingContext::createVariable(solidity::VariableDeclaration const& _varDe
{
solAssert(!knownVariable(_varDecl), "");
auto const& type = _varDecl.type();
auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_solver);
auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *this);
m_variables.emplace(&_varDecl, result.second);
return result.first;
}
@ -106,7 +106,7 @@ void EncodingContext::setZeroValue(solidity::VariableDeclaration const& _decl)
void EncodingContext::setZeroValue(SymbolicVariable& _variable)
{
setSymbolicZeroValue(_variable, *m_solver);
setSymbolicZeroValue(_variable, *this);
}
void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl)
@ -117,7 +117,7 @@ void EncodingContext::setUnknownValue(solidity::VariableDeclaration const& _decl
void EncodingContext::setUnknownValue(SymbolicVariable& _variable)
{
setSymbolicUnknownValue(_variable, *m_solver);
setSymbolicUnknownValue(_variable, *this);
}
/// Expressions
@ -144,7 +144,7 @@ bool EncodingContext::createExpression(solidity::Expression const& _e, shared_pt
}
else
{
auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_solver);
auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *this);
m_expressions.emplace(&_e, result.second);
return result.first;
}
@ -166,7 +166,7 @@ shared_ptr<SymbolicVariable> EncodingContext::globalSymbol(string const& _name)
bool EncodingContext::createGlobalSymbol(string const& _name, solidity::Expression const& _expr)
{
solAssert(!knownGlobalSymbol(_name), "");
auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_solver);
auto result = newSymbolicVariable(*_expr.annotation().type, _name, *this);
m_globalContext.emplace(_name, result.second);
setUnknownValue(*result.second);
return result.first;

7
libsolidity/formal/EncodingContext.h
View File

@ -41,6 +41,13 @@ public:
/// Resets the entire context.
void reset();
/// Forwards variable creation to the solver.
Expression newVariable(std::string _name, SortPointer _sort)
{
solAssert(m_solver, "");
return m_solver->newVariable(move(_name), move(_sort));
}
/// Variables.
//@{
/// @returns the symbolic representation of a program variable.

8
libsolidity/formal/SMTEncoder.cpp
View File

@ -473,7 +473,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
solAssert(value, "");
smt::Expression thisBalance = m_context.balance();
setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_context.solver());
setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context);
m_context.transfer(m_context.thisAddress(), expr(address), expr(*value));
break;
@ -615,7 +615,7 @@ void SMTEncoder::endVisit(Literal const& _literal)
auto stringType = TypeProvider::stringMemory();
auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type);
solAssert(stringLit, "");
auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_context.solver());
auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), m_context);
m_context.createExpression(_literal, result.second);
}
m_errorReporter.warning(
@ -687,7 +687,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
if (_memberAccess.memberName() == "balance")
{
defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression())));
setSymbolicUnknownValue(*m_context.expression(_memberAccess), *m_context.solver());
setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_context);
m_uninterpretedTerms.insert(&_memberAccess);
return false;
}
@ -734,7 +734,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
setSymbolicUnknownValue(
expr(_indexAccess),
_indexAccess.annotation().type,
*m_context.solver()
m_context
);
m_uninterpretedTerms.insert(&_indexAccess);
}

50
libsolidity/formal/SymbolicTypes.cpp
View File

@ -118,7 +118,7 @@ bool isSupportedTypeDeclaration(solidity::Type::Category _category)
pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
solidity::Type const& _type,
std::string const& _uniqueName,
SolverInterface& _solver
EncodingContext& _context
)
{
bool abstract = false;
@ -127,39 +127,39 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
if (!isSupportedTypeDeclaration(_type))
{
abstract = true;
var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), _uniqueName, _context);
}
else if (isBool(_type.category()))
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver);
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _context);
else if (isFunction(_type.category()))
var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _solver);
var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _context);
else if (isInteger(_type.category()))
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _context);
else if (isFixedBytes(_type.category()))
{
auto fixedBytesType = dynamic_cast<solidity::FixedBytesType const*>(type);
solAssert(fixedBytesType, "");
var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _solver);
var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _context);
}
else if (isAddress(_type.category()) || isContract(_type.category()))
var = make_shared<SymbolicAddressVariable>(_uniqueName, _solver);
var = make_shared<SymbolicAddressVariable>(_uniqueName, _context);
else if (isEnum(_type.category()))
var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _solver);
var = make_shared<SymbolicEnumVariable>(type, _uniqueName, _context);
else if (isRational(_type.category()))
{
auto rational = dynamic_cast<solidity::RationalNumberType const*>(&_type);
solAssert(rational, "");
if (rational->isFractional())
var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(solidity::TypeProvider::uint256(), _uniqueName, _context);
else
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _context);
}
else if (isMapping(_type.category()))
var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _solver);
var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _context);
else if (isArray(_type.category()))
var = make_shared<SymbolicArrayVariable>(type, _uniqueName, _solver);
var = make_shared<SymbolicArrayVariable>(type, _uniqueName, _context);
else if (isTuple(_type.category()))
var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _solver);
var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
else
solAssert(false, "");
return make_pair(abstract, var);
@ -250,41 +250,41 @@ Expression maxValue(solidity::IntegerType const& _type)
return Expression(_type.maxValue());
}
void setSymbolicZeroValue(SymbolicVariable const& _variable, SolverInterface& _interface)
void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context)
{
setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _interface);
setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context);
}
void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface)
void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context)
{
solAssert(_type, "");
if (isInteger(_type->category()))
_interface.addAssertion(_expr == 0);
_context.addAssertion(_expr == 0);
else if (isBool(_type->category()))
_interface.addAssertion(_expr == Expression(false));
_context.addAssertion(_expr == Expression(false));
}
void setSymbolicUnknownValue(SymbolicVariable const& _variable, SolverInterface& _interface)
void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context)
{
setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _interface);
setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _context);
}
void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface)
void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context)
{
solAssert(_type, "");
if (isEnum(_type->category()))
{
auto enumType = dynamic_cast<solidity::EnumType const*>(_type);
solAssert(enumType, "");
_interface.addAssertion(_expr >= 0);
_interface.addAssertion(_expr < enumType->numberOfMembers());
_context.addAssertion(_expr >= 0);
_context.addAssertion(_expr < enumType->numberOfMembers());
}
else if (isInteger(_type->category()))
{
auto intType = dynamic_cast<solidity::IntegerType const*>(_type);
solAssert(intType, "");
_interface.addAssertion(_expr >= minValue(*intType));
_interface.addAssertion(_expr <= maxValue(*intType));
_context.addAssertion(_expr >= minValue(*intType));
_context.addAssertion(_expr <= maxValue(*intType));
}
}

12
libsolidity/formal/SymbolicTypes.h
View File

@ -17,7 +17,7 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsolidity/ast/AST.h>
#include <libsolidity/ast/Types.h>
@ -58,15 +58,15 @@ bool isTuple(solidity::Type::Category _category);
/// Returns a new symbolic variable, according to _type.
/// Also returns whether the type is abstract or not,
/// which is true for unsupported types.
std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(solidity::Type const& _type, std::string const& _uniqueName, SolverInterface& _solver);
std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(solidity::Type const& _type, std::string const& _uniqueName, EncodingContext& _context);
Expression minValue(solidity::IntegerType const& _type);
Expression maxValue(solidity::IntegerType const& _type);
void setSymbolicZeroValue(SymbolicVariable const& _variable, SolverInterface& _interface);
void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface);
void setSymbolicUnknownValue(SymbolicVariable const& _variable, SolverInterface& _interface);
void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, SolverInterface& _interface);
void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context);
void setSymbolicZeroValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context);
void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context);
void setSymbolicUnknownValue(Expression _expr, solidity::TypePointer const& _type, EncodingContext& _context);
}
}

50
libsolidity/formal/SymbolicVariables.cpp
View File

@ -28,11 +28,11 @@ using namespace dev::solidity::smt;
SymbolicVariable::SymbolicVariable(
solidity::TypePointer _type,
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
m_type(move(_type)),
m_uniqueName(move(_uniqueName)),
m_interface(_interface),
m_context(_context),
m_ssa(make_unique<SSAVariable>())
{
solAssert(m_type, "");
@ -43,11 +43,11 @@ SymbolicVariable::SymbolicVariable(
SymbolicVariable::SymbolicVariable(
SortPointer _sort,
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
m_sort(move(_sort)),
m_uniqueName(move(_uniqueName)),
m_interface(_interface),
m_context(_context),
m_ssa(make_unique<SSAVariable>())
{
solAssert(m_sort, "");
@ -65,7 +65,7 @@ string SymbolicVariable::currentName() const
Expression SymbolicVariable::valueAtIndex(int _index) const
{
return m_interface.newVariable(uniqueSymbol(_index), m_sort);
return m_context.newVariable(uniqueSymbol(_index), m_sort);
}
string SymbolicVariable::uniqueSymbol(unsigned _index) const
@ -82,9 +82,9 @@ Expression SymbolicVariable::increaseIndex()
SymbolicBoolVariable::SymbolicBoolVariable(
solidity::TypePointer _type,
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
SymbolicVariable(move(_type), move(_uniqueName), _interface)
SymbolicVariable(move(_type), move(_uniqueName), _context)
{
solAssert(m_type->category() == solidity::Type::Category::Bool, "");
}
@ -92,44 +92,44 @@ SymbolicBoolVariable::SymbolicBoolVariable(
SymbolicIntVariable::SymbolicIntVariable(
solidity::TypePointer _type,
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
SymbolicVariable(move(_type), move(_uniqueName), _interface)
SymbolicVariable(move(_type), move(_uniqueName), _context)
{
solAssert(isNumber(m_type->category()), "");
}
SymbolicAddressVariable::SymbolicAddressVariable(
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
SymbolicIntVariable(TypeProvider::uint(160), move(_uniqueName), _interface)
SymbolicIntVariable(TypeProvider::uint(160), move(_uniqueName), _context)
{
}
SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
unsigned _numBytes,
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), move(_uniqueName), _interface)
SymbolicIntVariable(TypeProvider::uint(_numBytes * 8), move(_uniqueName), _context)
{
}
SymbolicFunctionVariable::SymbolicFunctionVariable(
solidity::TypePointer _type,
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
SymbolicVariable(move(_type), move(_uniqueName), _interface),
m_declaration(m_interface.newVariable(currentName(), m_sort))
SymbolicVariable(move(_type), move(_uniqueName), _context),
m_declaration(m_context.newVariable(currentName(), m_sort))
{
solAssert(m_type->category() == solidity::Type::Category::Function, "");
}
void SymbolicFunctionVariable::resetDeclaration()
{
m_declaration = m_interface.newVariable(currentName(), m_sort);
m_declaration = m_context.newVariable(currentName(), m_sort);
}
Expression SymbolicFunctionVariable::increaseIndex()
@ -147,9 +147,9 @@ Expression SymbolicFunctionVariable::operator()(vector<Expression> _arguments) c
SymbolicMappingVariable::SymbolicMappingVariable(
solidity::TypePointer _type,
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
SymbolicVariable(move(_type), move(_uniqueName), _interface)
SymbolicVariable(move(_type), move(_uniqueName), _context)
{
solAssert(isMapping(m_type->category()), "");
}
@ -157,9 +157,9 @@ SymbolicMappingVariable::SymbolicMappingVariable(
SymbolicArrayVariable::SymbolicArrayVariable(
solidity::TypePointer _type,
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
SymbolicVariable(move(_type), move(_uniqueName), _interface)
SymbolicVariable(move(_type), move(_uniqueName), _context)
{
solAssert(isArray(m_type->category()), "");
}
@ -167,9 +167,9 @@ SymbolicArrayVariable::SymbolicArrayVariable(
SymbolicEnumVariable::SymbolicEnumVariable(
solidity::TypePointer _type,
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
SymbolicVariable(move(_type), move(_uniqueName), _interface)
SymbolicVariable(move(_type), move(_uniqueName), _context)
{
solAssert(isEnum(m_type->category()), "");
}
@ -177,9 +177,9 @@ SymbolicEnumVariable::SymbolicEnumVariable(
SymbolicTupleVariable::SymbolicTupleVariable(
solidity::TypePointer _type,
string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
):
SymbolicVariable(move(_type), move(_uniqueName), _interface)
SymbolicVariable(move(_type), move(_uniqueName), _context)
{
solAssert(isTuple(m_type->category()), "");
}

25
libsolidity/formal/SymbolicVariables.h
View File

@ -29,6 +29,7 @@ namespace solidity
namespace smt
{
class EncodingContext;
class Type;
/**
@ -40,12 +41,12 @@ public:
SymbolicVariable(
solidity::TypePointer _type,
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
SymbolicVariable(
SortPointer _sort,
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
virtual ~SymbolicVariable() = default;
@ -72,7 +73,7 @@ protected:
/// Solidity type, used for size and range in number types.
solidity::TypePointer m_type;
std::string m_uniqueName;
SolverInterface& m_interface;
EncodingContext& m_context;
std::unique_ptr<SSAVariable> m_ssa;
};
@ -85,7 +86,7 @@ public:
SymbolicBoolVariable(
solidity::TypePointer _type,
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
};
@ -98,7 +99,7 @@ public:
SymbolicIntVariable(
solidity::TypePointer _type,
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
};
@ -110,7 +111,7 @@ class SymbolicAddressVariable: public SymbolicIntVariable
public:
SymbolicAddressVariable(
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
};
@ -123,7 +124,7 @@ public:
SymbolicFixedBytesVariable(
unsigned _numBytes,
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
};
@ -136,7 +137,7 @@ public:
SymbolicFunctionVariable(
solidity::TypePointer _type,
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
Expression increaseIndex();
@ -159,7 +160,7 @@ public:
SymbolicMappingVariable(
solidity::TypePointer _type,
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
};
@ -172,7 +173,7 @@ public:
SymbolicArrayVariable(
solidity::TypePointer _type,
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
};
@ -185,7 +186,7 @@ public:
SymbolicEnumVariable(
solidity::TypePointer _type,
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
};
@ -198,7 +199,7 @@ public:
SymbolicTupleVariable(
solidity::TypePointer _type,
std::string _uniqueName,
SolverInterface& _interface
EncodingContext& _context
);
std::vector<std::shared_ptr<SymbolicVariable>> const& components()

6
test/libsolidity/smtCheckerTestsJSON/multi.json
View File

@ -3,9 +3,9 @@
{
"smtlib2responses":
{
"0x399638a49c613bd393612f518a0bc22e9c7801791f0fa10a760b53c88686763c": "unsat\n",
"0x91c1bd0064608eae1120536e6e62864766bc370782e162d70f05d94a9f184ffc": "sat\n((|EVALEXPR_0| 1))\n",
"0x980a3db3305233a5417ea16e6253211d98818fcaa2ce7d0858f95080160092ef": "sat\n((|EVALEXPR_0| 0))\n"
"0x68fa399769cf119cbe46d5ae578164d39ea67e06eee08eeb37042d08a13a0cd8": "unsat\n",
"0xd78cd71ff120c5b5ecc5020146952f62de0506c4baef7ba499239a2ce2b14343": "sat\n((|EVALEXPR_0| 0))\n",
"0xf74672131cc6b7b3d6b82ed2fa0da2b75d01c9bc32f15d2f77e8e39e174f5a37": "sat\n((|EVALEXPR_0| 1))\n"
}
}
}

2
test/libsolidity/smtCheckerTestsJSON/simple.json
View File

@ -3,7 +3,7 @@
{
"smtlib2responses":
{
"0xc1ec66473d8e3b43cd320f847166c54f779e5e905085a837418d211233144dab": "sat\n((|EVALEXPR_0| 0))\n"
"0x9e377366ae857502a72974bd4e563258a29fa84dd4358cc053057544409da0ea": "sat\n((|EVALEXPR_0| 0))\n"
}
}
}