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 #5251 from ethereum/smt_refactor_expr_types

Browse Source 
[SMTChecker] Refactor expressions to use SymbolicVariable
This commit is contained in:
chriseth 2018-10-17 22:54:00 +02:00 committed by GitHub
commit c578b21e7c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 62 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

70
libsolidity/formal/SMTChecker.cpp
View File

@ -458,6 +458,12 @@ void SMTChecker::endVisit(Identifier const& _identifier)
{
// Will be translated as part of the node that requested the lvalue.
}
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
return;
createExpr(_identifier);
}
else if (isSupportedType(_identifier.annotation().type->category()))
{
if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
@ -469,25 +475,15 @@ void SMTChecker::endVisit(Identifier const& _identifier)
"Assertion checker does not yet support the type of this variable."
);
}
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
return;
createExpr(_identifier);
}
}
void SMTChecker::endVisit(Literal const& _literal)
{
Type const& type = *_literal.annotation().type;
if (type.category() == Type::Category::Integer || type.category() == Type::Category::Address || type.category() == Type::Category::RationalNumber)
{
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
solAssert(!rational->isFractional(), "");
if (isNumber(type.category()))
defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
}
else if (type.category() == Type::Category::Bool)
else if (isBool(type.category()))
defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
else
m_errorReporter.warning(
@ -917,13 +913,10 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
if (hasVariable(_varDecl))
return true;
auto const& type = _varDecl.type();
if (isSupportedType(type->category()))
{
solAssert(m_variables.count(&_varDecl) == 0, "");
m_variables.emplace(&_varDecl, newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface));
return true;
}
else
solAssert(m_variables.count(&_varDecl) == 0, "");
auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface);
m_variables.emplace(&_varDecl, result.second);
if (result.first)
{
m_errorReporter.warning(
_varDecl.location(),
@ -931,6 +924,7 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
);
return false;
}
return true;
}
string SMTChecker::uniqueSymbol(Expression const& _expr)
@ -980,7 +974,7 @@ smt::Expression SMTChecker::expr(Expression const& _e)
m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
createExpr(_e);
}
return prev(m_expressions.upper_bound(&_e))->second;
return m_expressions.at(&_e)->currentValue();
}
bool SMTChecker::hasExpr(Expression const& _e) const
@ -996,33 +990,17 @@ bool SMTChecker::hasVariable(VariableDeclaration const& _var) const
void SMTChecker::createExpr(Expression const& _e)
{
solAssert(_e.annotation().type, "");
string exprSymbol = uniqueSymbol(_e) + "_" + to_string(m_expressions.count(&_e));
switch (_e.annotation().type->category())
if (hasExpr(_e))
m_expressions.at(&_e)->increaseIndex();
else
{
case Type::Category::RationalNumber:
{
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
solAssert(!rational->isFractional(), "");
m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
break;
}
case Type::Category::Address:
case Type::Category::Integer:
m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
break;
case Type::Category::Bool:
m_expressions.emplace(&_e, m_interface->newBool(exprSymbol));
break;
case Type::Category::Function:
// This should be replaced by a `non-deterministic` type in the future.
m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
break;
default:
m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
m_errorReporter.warning(
_e.location(),
"Assertion checker does not yet implement this type."
);
auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface);
m_expressions.emplace(&_e, result.second);
if (result.first)
m_errorReporter.warning(
_e.location(),
"Assertion checker does not yet implement this type."
);
}
}

3
libsolidity/formal/SMTChecker.h
View File

@ -25,7 +25,6 @@
#include <libsolidity/interface/ReadFile.h>
#include <map>
#include <unordered_map>
#include <string>
#include <vector>
@ -186,7 +185,7 @@ private:
bool m_loopExecutionHappened = false;
/// An Expression may have multiple smt::Expression due to
/// repeated calls to the same function.
std::multimap<Expression const*, smt::Expression> m_expressions;
std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
std::vector<smt::Expression> m_pathConditions;
ErrorReporter& m_errorReporter;

54
libsolidity/formal/SymbolicTypes.cpp
View File

@ -30,27 +30,44 @@ using namespace dev::solidity;
bool dev::solidity::isSupportedType(Type::Category _category)
{
return isInteger(_category) ||
isAddress(_category) ||
isBool(_category);
return isNumber(_category) ||
isBool(_category) ||
isFunction(_category);
}
shared_ptr<SymbolicVariable> dev::solidity::newSymbolicVariable(
pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
Type const& _type,
std::string const& _uniqueName,
smt::SolverInterface& _solver
)
{
bool abstract = false;
shared_ptr<SymbolicVariable> var;
if (!isSupportedType(_type))
return nullptr;
if (isBool(_type.category()))
return make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
{
abstract = true;
var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
}
else if (isBool(_type.category()))
var = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
else if (isFunction(_type.category()))
var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
else if (isInteger(_type.category()))
return make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
else if (isAddress(_type.category()))
return make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver);
var = make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver);
else if (isRational(_type.category()))
{
auto rational = dynamic_cast<RationalNumberType const*>(&_type);
solAssert(rational, "");
if (rational->isFractional())
var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
else
var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
}
else
solAssert(false, "");
return make_pair(abstract, var);
}
bool dev::solidity::isSupportedType(Type const& _type)
@ -63,9 +80,9 @@ bool dev::solidity::isInteger(Type::Category _category)
return _category == Type::Category::Integer;
}
bool dev::solidity::isInteger(Type const& _type)
bool dev::solidity::isRational(Type::Category _category)
{
return isInteger(_type.category());
return _category == Type::Category::RationalNumber;
}
bool dev::solidity::isAddress(Type::Category _category)
@ -73,30 +90,21 @@ bool dev::solidity::isAddress(Type::Category _category)
return _category == Type::Category::Address;
}
bool dev::solidity::isAddress(Type const& _type)
{
return isAddress(_type.category());
}
bool dev::solidity::isNumber(Type::Category _category)
{
return isInteger(_category) ||
isRational(_category) ||
isAddress(_category);
}
bool dev::solidity::isNumber(Type const& _type)
{
return isNumber(_type.category());
}
bool dev::solidity::isBool(Type::Category _category)
{
return _category == Type::Category::Bool;
}
bool dev::solidity::isBool(Type const& _type)
bool dev::solidity::isFunction(Type::Category _category)
{
return isBool(_type.category());
return _category == Type::Category::Function;
}
smt::Expression dev::solidity::minValue(IntegerType const& _type)

14
libsolidity/formal/SymbolicTypes.h
View File

@ -34,18 +34,16 @@ bool isSupportedType(Type::Category _category);
bool isSupportedType(Type const& _type);
bool isInteger(Type::Category _category);
bool isInteger(Type const& _type);
bool isRational(Type::Category _category);
bool isAddress(Type::Category _category);
bool isAddress(Type const& _type);
bool isNumber(Type::Category _category);
bool isNumber(Type const& _type);
bool isBool(Type::Category _category);
bool isBool(Type const& _type);
bool isFunction(Type::Category _category);
std::shared_ptr<SymbolicVariable> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver);
/// 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(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver);
smt::Expression minValue(IntegerType const& _type);
smt::Expression maxValue(IntegerType const& _type);