aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/SMTChecker.cpp151
-rw-r--r--libsolidity/formal/SMTChecker.h24
-rw-r--r--libsolidity/formal/SymbolicTypes.cpp37
-rw-r--r--libsolidity/formal/SymbolicTypes.h6
4 files changed, 133 insertions, 85 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 17dc11ac..dc14f4c2 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -90,8 +90,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
m_interface->reset();
m_pathConditions.clear();
m_expressions.clear();
- m_specialVariables.clear();
- m_uninterpretedFunctions.clear();
+ m_globalContext.clear();
m_uninterpretedTerms.clear();
resetStateVariables();
initializeLocalVariables(_function);
@@ -268,16 +267,9 @@ void SMTChecker::endVisit(Assignment const& _assignment)
else if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide()))
{
VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration);
- if (knownVariable(decl))
- {
- assignment(decl, _assignment.rightHandSide(), _assignment.location());
- defineExpr(_assignment, expr(_assignment.rightHandSide()));
- }
- else
- m_errorReporter.warning(
- _assignment.location(),
- "Assertion checker does not yet implement such assignments."
- );
+ solAssert(knownVariable(decl), "");
+ assignment(decl, _assignment.rightHandSide(), _assignment.location());
+ defineExpr(_assignment, expr(_assignment.rightHandSide()));
}
else
m_errorReporter.warning(
@@ -288,7 +280,11 @@ void SMTChecker::endVisit(Assignment const& _assignment)
void SMTChecker::endVisit(TupleExpression const& _tuple)
{
- if (_tuple.isInlineArray() || _tuple.components().size() != 1)
+ if (
+ _tuple.isInlineArray() ||
+ _tuple.components().size() != 1 ||
+ !isSupportedType(_tuple.components()[0]->annotation().type->category())
+ )
m_errorReporter.warning(
_tuple.location(),
"Assertion checker does not yet implement tuples and inline arrays."
@@ -399,18 +395,30 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
- if (funType.kind() == FunctionType::Kind::Assert)
+ switch (funType.kind())
+ {
+ case FunctionType::Kind::Assert:
visitAssert(_funCall);
- else if (funType.kind() == FunctionType::Kind::Require)
+ break;
+ case FunctionType::Kind::Require:
visitRequire(_funCall);
- else if (funType.kind() == FunctionType::Kind::GasLeft)
+ break;
+ case FunctionType::Kind::GasLeft:
visitGasLeft(_funCall);
- else if (funType.kind() == FunctionType::Kind::BlockHash)
- visitBlockHash(_funCall);
- else if (funType.kind() == FunctionType::Kind::Internal)
+ break;
+ case FunctionType::Kind::Internal:
inlineFunctionCall(_funCall);
- else
- {
+ break;
+ case FunctionType::Kind::KECCAK256:
+ case FunctionType::Kind::ECRecover:
+ case FunctionType::Kind::SHA256:
+ case FunctionType::Kind::RIPEMD160:
+ case FunctionType::Kind::BlockHash:
+ case FunctionType::Kind::AddMod:
+ case FunctionType::Kind::MulMod:
+ abstractFunctionCall(_funCall);
+ break;
+ default:
m_errorReporter.warning(
_funCall.location(),
"Assertion checker does not yet implement this type of function call."
@@ -442,8 +450,8 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
string gasLeft = "gasleft()";
// We increase the variable index since gasleft changes
// inside a tx.
- defineSpecialVariable(gasLeft, _funCall, true);
- auto const& symbolicVar = m_specialVariables.at(gasLeft);
+ defineGlobalVariable(gasLeft, _funCall, true);
+ auto const& symbolicVar = m_globalContext.at(gasLeft);
unsigned index = symbolicVar->index();
// We set the current value to unknown anyway to add type constraints.
setUnknownValue(*symbolicVar);
@@ -451,21 +459,6 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
}
-void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
-{
- string blockHash = "blockhash";
- auto const& arguments = _funCall.arguments();
- solAssert(arguments.size() == 1, "");
- smt::SortPointer paramSort = smtSort(*arguments.at(0)->annotation().type);
- smt::SortPointer returnSort = smtSort(*_funCall.annotation().type);
- defineUninterpretedFunction(
- blockHash,
- make_shared<smt::FunctionSort>(vector<smt::SortPointer>{paramSort}, returnSort)
- );
- defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments.at(0))}));
- m_uninterpretedTerms.push_back(&_funCall);
-}
-
void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
{
FunctionDefinition const* _funDef = nullptr;
@@ -533,29 +526,32 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
}
}
+void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
+{
+ vector<smt::Expression> smtArguments;
+ for (auto const& arg: _funCall.arguments())
+ smtArguments.push_back(expr(*arg));
+ defineExpr(_funCall, (*m_expressions.at(&_funCall.expression()))(smtArguments));
+ m_uninterpretedTerms.push_back(&_funCall);
+ setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface);
+}
+
void SMTChecker::endVisit(Identifier const& _identifier)
{
if (_identifier.annotation().lValueRequested)
{
// 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()))
+ else if (dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
- if (
- fun->kind() == FunctionType::Kind::Assert ||
- fun->kind() == FunctionType::Kind::Require ||
- fun->kind() == FunctionType::Kind::GasLeft ||
- fun->kind() == FunctionType::Kind::BlockHash
- )
- return;
- createExpr(_identifier);
+ visitFunctionIdentifier(_identifier);
}
else if (isSupportedType(_identifier.annotation().type->category()))
{
if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
defineExpr(_identifier, currentValue(*decl));
else if (_identifier.name() == "now")
- defineSpecialVariable(_identifier.name(), _identifier);
+ defineGlobalVariable(_identifier.name(), _identifier);
else
// TODO: handle MagicVariableDeclaration here
m_errorReporter.warning(
@@ -565,6 +561,20 @@ void SMTChecker::endVisit(Identifier const& _identifier)
}
}
+void SMTChecker::visitFunctionIdentifier(Identifier const& _identifier)
+{
+ auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type);
+ if (fType.returnParameterTypes().size() > 1)
+ {
+ m_errorReporter.warning(
+ _identifier.location(),
+ "Assertion checker does not yet support functions with more than one return parameter."
+ );
+ }
+ defineGlobalFunction(fType.richIdentifier(), _identifier);
+ m_expressions.emplace(&_identifier, m_globalContext.at(fType.richIdentifier()));
+}
+
void SMTChecker::endVisit(Literal const& _literal)
{
Type const& type = *_literal.annotation().type;
@@ -616,7 +626,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
_memberAccess.location(),
"Assertion checker does not yet support this expression."
);
- defineSpecialVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
+ defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
return false;
}
else
@@ -628,30 +638,39 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
return true;
}
-void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
+void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
{
- if (!knownSpecialVariable(_name))
+ if (!knownGlobalSymbol(_name))
{
auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
- m_specialVariables.emplace(_name, result.second);
+ m_globalContext.emplace(_name, result.second);
setUnknownValue(*result.second);
if (result.first)
m_errorReporter.warning(
_expr.location(),
- "Assertion checker does not yet support this special variable."
+ "Assertion checker does not yet support this global variable."
);
}
else if (_increaseIndex)
- m_specialVariables.at(_name)->increaseIndex();
+ m_globalContext.at(_name)->increaseIndex();
// The default behavior is not to increase the index since
- // most of the special values stay the same throughout a tx.
- defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
+ // most of the global values stay the same throughout a tx.
+ if (isSupportedType(_expr.annotation().type->category()))
+ defineExpr(_expr, m_globalContext.at(_name)->currentValue());
}
-void SMTChecker::defineUninterpretedFunction(string const& _name, smt::SortPointer _sort)
+void SMTChecker::defineGlobalFunction(string const& _name, Expression const& _expr)
{
- if (!m_uninterpretedFunctions.count(_name))
- m_uninterpretedFunctions.emplace(_name, m_interface->newVariable(_name, _sort));
+ if (!knownGlobalSymbol(_name))
+ {
+ auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
+ m_globalContext.emplace(_name, result.second);
+ if (result.first)
+ m_errorReporter.warning(
+ _expr.location(),
+ "Assertion checker does not yet support the type of this function."
+ );
+ }
}
void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
@@ -831,10 +850,13 @@ void SMTChecker::checkCondition(
expressionsToEvaluate.emplace_back(currentValue(*var.first));
expressionNames.push_back(var.first->name());
}
- for (auto const& var: m_specialVariables)
+ for (auto const& var: m_globalContext)
{
- expressionsToEvaluate.emplace_back(var.second->currentValue());
- expressionNames.push_back(var.first);
+ if (smtKind(var.second->type()->category()) != smt::Kind::Function)
+ {
+ expressionsToEvaluate.emplace_back(var.second->currentValue());
+ expressionNames.push_back(var.first);
+ }
}
for (auto const& uf: m_uninterpretedTerms)
{
@@ -1147,9 +1169,9 @@ bool SMTChecker::knownExpr(Expression const& _e) const
return m_expressions.count(&_e);
}
-bool SMTChecker::knownSpecialVariable(string const& _var) const
+bool SMTChecker::knownGlobalSymbol(string const& _var) const
{
- return m_specialVariables.count(_var);
+ return m_globalContext.count(_var);
}
void SMTChecker::createExpr(Expression const& _e)
@@ -1172,6 +1194,7 @@ void SMTChecker::createExpr(Expression const& _e)
void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
{
createExpr(_e);
+ solAssert(isSupportedType(*_e.annotation().type), "Equality operator applied to type that is not fully supported");
m_interface->addAssertion(expr(_e) == _value);
}
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 34724848..9f8c04ab 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -84,16 +84,18 @@ private:
void compareOperation(BinaryOperation const& _op);
void booleanOperation(BinaryOperation const& _op);
- void visitAssert(FunctionCall const&);
- void visitRequire(FunctionCall const&);
- void visitGasLeft(FunctionCall const&);
- void visitBlockHash(FunctionCall const&);
+ void visitAssert(FunctionCall const& _funCall);
+ void visitRequire(FunctionCall const& _funCall);
+ void visitGasLeft(FunctionCall const& _funCall);
/// Visits the FunctionDefinition of the called function
/// if available and inlines the return value.
- void inlineFunctionCall(FunctionCall const&);
+ void inlineFunctionCall(FunctionCall const& _funCall);
+ /// Creates an uninterpreted function call.
+ void abstractFunctionCall(FunctionCall const& _funCall);
+ void visitFunctionIdentifier(Identifier const& _identifier);
- void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
- void defineUninterpretedFunction(std::string const& _name, smt::SortPointer _sort);
+ void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
+ void defineGlobalFunction(std::string const& _name, Expression const& _expr);
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
@@ -176,8 +178,8 @@ private:
/// Creates the expression and sets its value.
void defineExpr(Expression const& _e, smt::Expression _value);
- /// Checks if special variable was seen.
- bool knownSpecialVariable(std::string const& _var) const;
+ /// Checks if special variable or function was seen.
+ bool knownGlobalSymbol(std::string const& _var) const;
/// Adds a new path condition
void pushPathCondition(smt::Expression const& _e);
@@ -205,9 +207,7 @@ private:
/// repeated calls to the same function.
std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
- std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables;
- /// Stores the declaration of an Uninterpreted Function.
- std::unordered_map<std::string, smt::Expression> m_uninterpretedFunctions;
+ std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_globalContext;
/// Stores the instances of an Uninterpreted Function applied to arguments.
/// Used to retrieve models.
std::vector<Expression const*> m_uninterpretedTerms;
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index c297c807..3cfaa271 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -38,15 +38,25 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
solAssert(fType, "");
vector<smt::SortPointer> parameterSorts = smtSort(fType->parameterTypes());
auto returnTypes = fType->returnParameterTypes();
- // TODO remove this when we support tuples.
- solAssert(returnTypes.size() == 1, "");
- smt::SortPointer returnSort = smtSort(*returnTypes.at(0));
+ smt::SortPointer returnSort;
+ // TODO change this when we support tuples.
+ if (returnTypes.size() == 0)
+ // We cannot declare functions without a return sort, so we use the smallest.
+ returnSort = make_shared<smt::Sort>(smt::Kind::Bool);
+ else if (returnTypes.size() > 1)
+ // Abstract sort.
+ returnSort = make_shared<smt::Sort>(smt::Kind::Int);
+ else
+ returnSort = smtSort(*returnTypes.at(0));
return make_shared<smt::FunctionSort>(parameterSorts, returnSort);
}
case smt::Kind::Array:
{
solUnimplementedAssert(false, "Invalid type");
}
+ default:
+ // Abstract case.
+ return make_shared<smt::Sort>(smt::Kind::Int);
}
solAssert(false, "Invalid type");
}
@@ -65,13 +75,21 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
return smt::Kind::Int;
else if (isBool(_category))
return smt::Kind::Bool;
- solAssert(false, "Invalid type");
+ else if (isFunction(_category))
+ return smt::Kind::Function;
+ // Abstract case.
+ return smt::Kind::Int;
}
bool dev::solidity::isSupportedType(Type::Category _category)
{
return isNumber(_category) ||
- isBool(_category) ||
+ isBool(_category);
+}
+
+bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category)
+{
+ return isSupportedType(_category) ||
isFunction(_category);
}
@@ -84,7 +102,7 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
bool abstract = false;
shared_ptr<SymbolicVariable> var;
TypePointer type = _type.shared_from_this();
- if (!isSupportedType(_type))
+ if (!isSupportedTypeDeclaration(_type))
{
abstract = true;
var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
@@ -92,7 +110,7 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
else if (isBool(_type.category()))
var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver);
else if (isFunction(_type.category()))
- var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
+ var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _solver);
else if (isInteger(_type.category()))
var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
else if (isFixedBytes(_type.category()))
@@ -122,6 +140,11 @@ bool dev::solidity::isSupportedType(Type const& _type)
return isSupportedType(_type.category());
}
+bool dev::solidity::isSupportedTypeDeclaration(Type const& _type)
+{
+ return isSupportedTypeDeclaration(_type.category());
+}
+
bool dev::solidity::isInteger(Type::Category _category)
{
return _category == Type::Category::Integer;
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 984653b3..2c568f5b 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -34,10 +34,12 @@ std::vector<smt::SortPointer> smtSort(std::vector<TypePointer> const& _types);
/// Returns the SMT kind that models the Solidity type type category _category.
smt::Kind smtKind(Type::Category _category);
-/// So far int, bool and address are supported.
-/// Returns true if type is supported.
+/// Returns true if type is fully supported (declaration and operations).
bool isSupportedType(Type::Category _category);
bool isSupportedType(Type const& _type);
+/// Returns true if type is partially supported (declaration).
+bool isSupportedTypeDeclaration(Type::Category _category);
+bool isSupportedTypeDeclaration(Type const& _type);
bool isInteger(Type::Category _category);
bool isRational(Type::Category _category);
generated by cgit (git 2.34.1) at 2024-11-17 23:08:49 +0800