aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/CVC4Interface.cpp73
-rw-r--r--libsolidity/formal/CVC4Interface.h10
-rw-r--r--libsolidity/formal/SMTChecker.cpp80
-rw-r--r--libsolidity/formal/SMTChecker.h74
-rw-r--r--libsolidity/formal/SMTLib2Interface.cpp104
-rw-r--r--libsolidity/formal/SMTLib2Interface.h23
-rw-r--r--libsolidity/formal/SMTPortfolio.cpp25
-rw-r--r--libsolidity/formal/SMTPortfolio.h10
-rw-r--r--libsolidity/formal/SolverInterface.h214
-rw-r--r--libsolidity/formal/SymbolicTypes.cpp73
-rw-r--r--libsolidity/formal/SymbolicTypes.h16
-rw-r--r--libsolidity/formal/SymbolicVariables.cpp31
-rw-r--r--libsolidity/formal/SymbolicVariables.h23
-rw-r--r--libsolidity/formal/Z3Interface.cpp51
-rw-r--r--libsolidity/formal/Z3Interface.h9
15 files changed, 523 insertions, 293 deletions
diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index 6cb91483..de5e4430 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -17,7 +17,7 @@
#include <libsolidity/formal/CVC4Interface.h>
-#include <libsolidity/interface/Exceptions.h>
+#include <liblangutil/Exceptions.h>
#include <libdevcore/CommonIO.h>
@@ -33,8 +33,7 @@ CVC4Interface::CVC4Interface():
void CVC4Interface::reset()
{
- m_constants.clear();
- m_functions.clear();
+ m_variables.clear();
m_solver.reset();
m_solver.setOption("produce-models", true);
m_solver.setTimeLimit(queryTimeout);
@@ -50,25 +49,10 @@ void CVC4Interface::pop()
m_solver.pop();
}
-void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void CVC4Interface::declareVariable(string const& _name, Sort const& _sort)
{
- if (!m_functions.count(_name))
- {
- CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain));
- m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)});
- }
-}
-
-void CVC4Interface::declareInteger(string _name)
-{
- if (!m_constants.count(_name))
- m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())});
-}
-
-void CVC4Interface::declareBool(string _name)
-{
- if (!m_constants.count(_name))
- m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())});
+ if (!m_variables.count(_name))
+ m_variables.insert({_name, m_context.mkVar(_name.c_str(), cvc4Sort(_sort))});
}
void CVC4Interface::addAssertion(Expression const& _expr)
@@ -129,20 +113,19 @@ pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const&
CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
{
- if (_expr.arguments.empty() && m_constants.count(_expr.name))
- return m_constants.at(_expr.name);
+ // Variable
+ if (_expr.arguments.empty() && m_variables.count(_expr.name))
+ return m_variables.at(_expr.name);
+
vector<CVC4::Expr> arguments;
for (auto const& arg: _expr.arguments)
arguments.push_back(toCVC4Expr(arg));
string const& n = _expr.name;
- if (m_functions.count(n))
- return m_context.mkExpr(CVC4::kind::APPLY_UF, m_functions[n], arguments);
- else if (m_constants.count(n))
- {
- solAssert(arguments.empty(), "");
- return m_constants.at(n);
- }
+ // Function application
+ if (!arguments.empty() && m_variables.count(_expr.name))
+ return m_context.mkExpr(CVC4::kind::APPLY_UF, m_variables.at(n), arguments);
+ // Literal
else if (arguments.empty())
{
if (n == "true")
@@ -181,19 +164,33 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
else if (n == "/")
return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
+ else if (n == "select")
+ return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]);
+ else if (n == "store")
+ return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]);
// Cannot reach here.
solAssert(false, "");
return arguments[0];
}
-CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)
+CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
{
- switch (_sort)
+ switch (_sort.kind)
{
- case Sort::Bool:
+ case Kind::Bool:
return m_context.booleanType();
- case Sort::Int:
+ case Kind::Int:
return m_context.integerType();
+ case Kind::Function:
+ {
+ FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);
+ return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain));
+ }
+ case Kind::Array:
+ {
+ auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
+ return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range));
+ }
default:
break;
}
@@ -201,3 +198,11 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)
// Cannot be reached.
return m_context.integerType();
}
+
+vector<CVC4::Type> CVC4Interface::cvc4Sort(vector<SortPointer> const& _sorts)
+{
+ vector<CVC4::Type> cvc4Sorts;
+ for (auto const& _sort: _sorts)
+ cvc4Sorts.push_back(cvc4Sort(*_sort));
+ return cvc4Sorts;
+}
diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h
index cd6d761d..bbe23855 100644
--- a/libsolidity/formal/CVC4Interface.h
+++ b/libsolidity/formal/CVC4Interface.h
@@ -51,21 +51,19 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
- void declareInteger(std::string _name) override;
- void declareBool(std::string _name) override;
+ void declareVariable(std::string const&, Sort const&) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
private:
CVC4::Expr toCVC4Expr(Expression const& _expr);
- CVC4::Type cvc4Sort(smt::Sort _sort);
+ CVC4::Type cvc4Sort(smt::Sort const& _sort);
+ std::vector<CVC4::Type> cvc4Sort(std::vector<smt::SortPointer> const& _sorts);
CVC4::ExprManager m_context;
CVC4::SmtEngine m_solver;
- std::map<std::string, CVC4::Expr> m_constants;
- std::map<std::string, CVC4::Expr> m_functions;
+ std::map<std::string, CVC4::Expr> m_variables;
};
}
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index cc580021..ebb09f0a 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -22,19 +22,29 @@
#include <libsolidity/formal/VariableUsage.h>
#include <libsolidity/formal/SymbolicTypes.h>
-#include <libsolidity/interface/ErrorReporter.h>
+#include <liblangutil/ErrorReporter.h>
#include <boost/range/adaptor/map.hpp>
#include <boost/algorithm/string/replace.hpp>
using namespace std;
using namespace dev;
+using namespace langutil;
using namespace dev::solidity;
-SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback):
- m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)),
+SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
+ m_interface(make_shared<smt::SMTPortfolio>(_smtlib2Responses)),
m_errorReporter(_errorReporter)
{
+#if defined (HAVE_Z3) || defined (HAVE_CVC4)
+ if (!_smtlib2Responses.empty())
+ m_errorReporter.warning(
+ "SMT-LIB2 query responses were given in the auxiliary input, "
+ "but this Solidity binary uses an SMT solver (Z3/CVC4) directly."
+ "These responses will be ignored."
+ "Consider disabling Z3/CVC4 at compilation time in order to use SMT-LIB2 responses."
+ );
+#endif
}
void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
@@ -78,6 +88,9 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
m_interface->reset();
m_pathConditions.clear();
m_expressions.clear();
+ m_specialVariables.clear();
+ m_uninterpretedFunctions.clear();
+ m_uninterpretedTerms.clear();
resetStateVariables();
initializeLocalVariables(_function);
}
@@ -310,9 +323,6 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
);
break;
}
- case Token::Add: // +
- defineExpr(_op, expr(_op.subExpression()));
- break;
case Token::Sub: // -
{
defineExpr(_op, 0 - expr(_op.subExpression()));
@@ -405,16 +415,24 @@ 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));
}
void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
{
- string blockHash = "blockhash()";
- // TODO Define blockhash as an uninterpreted function
- defineSpecialVariable(blockHash, _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)
@@ -451,6 +469,14 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
else if (_funDef && _funDef->isImplemented())
{
vector<smt::Expression> funArgs;
+ auto const& funType = dynamic_cast<FunctionType const*>(_calledExpr->annotation().type.get());
+ solAssert(funType, "");
+ if (funType->bound())
+ {
+ auto const& boundFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
+ solAssert(boundFunction, "");
+ funArgs.push_back(expr(boundFunction->expression()));
+ }
for (auto arg: _funCall.arguments())
funArgs.push_back(expr(*arg));
initializeFunctionCallParameters(*_funDef, funArgs);
@@ -542,6 +568,10 @@ void SMTChecker::endVisit(Return const& _return)
bool SMTChecker::visit(MemberAccess const& _memberAccess)
{
+ auto const& accessType = _memberAccess.annotation().type;
+ if (accessType->category() == Type::Category::Function)
+ return true;
+
auto const& exprType = _memberAccess.expression().annotation().type;
solAssert(exprType, "");
if (exprType->category() == Type::Category::Magic)
@@ -573,7 +603,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(),
@@ -587,6 +617,11 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e
defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
}
+void SMTChecker::defineUninterpretedFunction(string const& _name, smt::SortPointer _sort)
+{
+ if (!m_uninterpretedFunctions.count(_name))
+ m_uninterpretedFunctions.emplace(_name, m_interface->newVariable(_name, _sort));
+}
void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
{
@@ -770,6 +805,11 @@ void SMTChecker::checkCondition(
expressionsToEvaluate.emplace_back(var.second->currentValue());
expressionNames.push_back(var.first);
}
+ for (auto const& uf: m_uninterpretedTerms)
+ {
+ expressionsToEvaluate.emplace_back(expr(*uf));
+ expressionNames.push_back(m_scanner->sourceAt(uf->location()));
+ }
}
smt::CheckResult result;
vector<string> values;
@@ -846,6 +886,10 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
{
// everything fine.
}
+ else if (positiveResult == smt::CheckResult::UNKNOWN || negatedResult == smt::CheckResult::UNKNOWN)
+ {
+ // can't do anything.
+ }
else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
m_errorReporter.warning(_condition.location(), "Condition unreachable.");
else
@@ -1037,13 +1081,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 a7f955dd..34724848 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -25,50 +25,60 @@
#include <libsolidity/interface/ReadFile.h>
-#include <libsolidity/parsing/Scanner.h>
+#include <liblangutil/Scanner.h>
#include <unordered_map>
#include <string>
#include <vector>
+namespace langutil
+{
+class ErrorReporter;
+struct SourceLocation;
+}
+
namespace dev
{
namespace solidity
{
class VariableUsage;
-class ErrorReporter;
class SMTChecker: private ASTConstVisitor
{
public:
- SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback);
+ SMTChecker(langutil::ErrorReporter& _errorReporter, std::map<h256, std::string> const& _smtlib2Responses);
+
+ void analyze(SourceUnit const& _sources, std::shared_ptr<langutil::Scanner> const& _scanner);
- void analyze(SourceUnit const& _sources, std::shared_ptr<Scanner> const& _scanner);
+ /// This is used if the SMT solver is not directly linked into this binary.
+ /// @returns a list of inputs to the SMT solver that were not part of the argument to
+ /// the constructor.
+ std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
private:
// TODO: Check that we do not have concurrent reads and writes to a variable,
// because the order of expression evaluation is undefined
// TODO: or just force a certain order, but people might have a different idea about that.
- virtual bool visit(ContractDefinition const& _node) override;
- virtual void endVisit(ContractDefinition const& _node) override;
- virtual void endVisit(VariableDeclaration const& _node) override;
- virtual bool visit(FunctionDefinition const& _node) override;
- virtual void endVisit(FunctionDefinition const& _node) override;
- virtual bool visit(IfStatement const& _node) override;
- virtual bool visit(WhileStatement const& _node) override;
- virtual bool visit(ForStatement const& _node) override;
- virtual void endVisit(VariableDeclarationStatement const& _node) override;
- virtual void endVisit(Assignment const& _node) override;
- virtual void endVisit(TupleExpression const& _node) override;
- virtual void endVisit(UnaryOperation const& _node) override;
- virtual void endVisit(BinaryOperation const& _node) override;
- virtual void endVisit(FunctionCall const& _node) override;
- virtual void endVisit(Identifier const& _node) override;
- virtual void endVisit(Literal const& _node) override;
- virtual void endVisit(Return const& _node) override;
- virtual bool visit(MemberAccess const& _node) override;
+ bool visit(ContractDefinition const& _node) override;
+ void endVisit(ContractDefinition const& _node) override;
+ void endVisit(VariableDeclaration const& _node) override;
+ bool visit(FunctionDefinition const& _node) override;
+ void endVisit(FunctionDefinition const& _node) override;
+ bool visit(IfStatement const& _node) override;
+ bool visit(WhileStatement const& _node) override;
+ bool visit(ForStatement const& _node) override;
+ void endVisit(VariableDeclarationStatement const& _node) override;
+ void endVisit(Assignment const& _node) override;
+ void endVisit(TupleExpression const& _node) override;
+ void endVisit(UnaryOperation const& _node) override;
+ void endVisit(BinaryOperation const& _node) override;
+ void endVisit(FunctionCall const& _node) override;
+ void endVisit(Identifier const& _node) override;
+ void endVisit(Literal const& _node) override;
+ void endVisit(Return const& _node) override;
+ bool visit(MemberAccess const& _node) override;
void arithmeticOperation(BinaryOperation const& _op);
void compareOperation(BinaryOperation const& _op);
@@ -83,13 +93,14 @@ private:
void inlineFunctionCall(FunctionCall const&);
void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
+ void defineUninterpretedFunction(std::string const& _name, smt::SortPointer _sort);
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
- void assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location);
- void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
+ void assignment(VariableDeclaration const& _variable, Expression const& _value, langutil::SourceLocation const& _location);
+ void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, langutil::SourceLocation const& _location);
/// Maps a variable to an SSA index.
using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;
@@ -103,7 +114,7 @@ private:
/// Check that a condition can be satisfied.
void checkCondition(
smt::Expression _condition,
- SourceLocation const& _location,
+ langutil::SourceLocation const& _location,
std::string const& _description,
std::string const& _additionalValueName = "",
smt::Expression* _additionalValue = nullptr
@@ -116,7 +127,7 @@ private:
std::string const& _description
);
/// Checks that the value is in the range given by the type.
- void checkUnderOverflow(smt::Expression _value, IntegerType const& _Type, SourceLocation const& _location);
+ void checkUnderOverflow(smt::Expression _value, IntegerType const& _Type, langutil::SourceLocation const& _location);
std::pair<smt::CheckResult, std::vector<std::string>>
@@ -151,8 +162,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);
@@ -193,9 +206,14 @@ private:
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;
+ /// Stores the instances of an Uninterpreted Function applied to arguments.
+ /// Used to retrieve models.
+ std::vector<Expression const*> m_uninterpretedTerms;
std::vector<smt::Expression> m_pathConditions;
- ErrorReporter& m_errorReporter;
- std::shared_ptr<Scanner> m_scanner;
+ langutil::ErrorReporter& m_errorReporter;
+ std::shared_ptr<langutil::Scanner> m_scanner;
/// Stores the current path of function calls.
std::vector<FunctionDefinition const*> m_functionPath;
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index a6c1f87c..3cfa01b1 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -17,9 +17,11 @@
#include <libsolidity/formal/SMTLib2Interface.h>
-#include <libsolidity/interface/Exceptions.h>
+#include <liblangutil/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
+#include <libdevcore/Keccak256.h>
+
#include <boost/algorithm/string/predicate.hpp>
#include <boost/algorithm/string/join.hpp>
#include <boost/filesystem/operations.hpp>
@@ -37,8 +39,8 @@ using namespace dev;
using namespace dev::solidity;
using namespace dev::solidity::smt;
-SMTLib2Interface::SMTLib2Interface(ReadCallback::Callback const& _queryCallback):
- m_queryCallback(_queryCallback)
+SMTLib2Interface::SMTLib2Interface(map<h256, string> const& _queryResponses):
+ m_queryResponses(_queryResponses)
{
reset();
}
@@ -47,8 +49,7 @@ void SMTLib2Interface::reset()
{
m_accumulatedOutput.clear();
m_accumulatedOutput.emplace_back();
- m_constants.clear();
- m_functions.clear();
+ m_variables.clear();
write("(set-option :produce-models true)");
write("(set-logic QF_UFLIA)");
}
@@ -64,42 +65,39 @@ void SMTLib2Interface::pop()
m_accumulatedOutput.pop_back();
}
-void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void SMTLib2Interface::declareVariable(string const& _name, Sort const& _sort)
+{
+ if (_sort.kind == Kind::Function)
+ declareFunction(_name, _sort);
+ else if (!m_variables.count(_name))
+ {
+ m_variables.insert(_name);
+ write("(declare-fun |" + _name + "| () " + toSmtLibSort(_sort) + ')');
+ }
+}
+
+void SMTLib2Interface::declareFunction(string const& _name, Sort const& _sort)
{
+ solAssert(_sort.kind == smt::Kind::Function, "");
// TODO Use domain and codomain as key as well
- if (!m_functions.count(_name))
+ if (!m_variables.count(_name))
{
- m_functions.insert(_name);
+ FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
+ string domain = toSmtLibSort(fSort.domain);
+ string codomain = toSmtLibSort(*fSort.codomain);
+ m_variables.insert(_name);
write(
"(declare-fun |" +
_name +
- "| (" +
- (_domain == Sort::Int ? "Int" : "Bool") +
- ") " +
- (_codomain == Sort::Int ? "Int" : "Bool") +
+ "| " +
+ domain +
+ " " +
+ codomain +
")"
);
}
}
-void SMTLib2Interface::declareInteger(string _name)
-{
- if (!m_constants.count(_name))
- {
- m_constants.insert(_name);
- write("(declare-const |" + _name + "| Int)");
- }
-}
-
-void SMTLib2Interface::declareBool(string _name)
-{
- if (!m_constants.count(_name))
- {
- m_constants.insert(_name);
- write("(declare-const |" + _name + "| Bool)");
- }
-}
-
void SMTLib2Interface::addAssertion(Expression const& _expr)
{
write("(assert " + toSExpr(_expr) + ")");
@@ -140,6 +138,33 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
return sexpr;
}
+string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
+{
+ switch (_sort.kind)
+ {
+ case Kind::Int:
+ return "Int";
+ case Kind::Bool:
+ return "Bool";
+ case Kind::Array:
+ {
+ auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
+ return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
+ }
+ default:
+ solAssert(false, "Invalid SMT sort");
+ }
+}
+
+string SMTLib2Interface::toSmtLibSort(vector<SortPointer> const& _sorts)
+{
+ string ssort("(");
+ for (auto const& sort: _sorts)
+ ssort += toSmtLibSort(*sort) + " ";
+ ssort += ")";
+ return ssort;
+}
+
void SMTLib2Interface::write(string _data)
{
solAssert(!m_accumulatedOutput.empty(), "");
@@ -157,8 +182,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
{
auto const& e = _expressionsToEvaluate.at(i);
- solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate.");
- command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + ")\n";
+ solAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate.");
+ command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n";
command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
}
command += "(check-sat)\n";
@@ -189,11 +214,12 @@ vector<string> SMTLib2Interface::parseValues(string::const_iterator _start, stri
string SMTLib2Interface::querySolver(string const& _input)
{
- if (!m_queryCallback)
- BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment("No SMT solver available."));
-
- ReadCallback::Result queryResult = m_queryCallback(_input);
- if (!queryResult.success)
- BOOST_THROW_EXCEPTION(SolverError() << errinfo_comment(queryResult.responseOrErrorMessage));
- return queryResult.responseOrErrorMessage;
+ h256 inputHash = dev::keccak256(_input);
+ if (m_queryResponses.count(inputHash))
+ return m_queryResponses.at(inputHash);
+ else
+ {
+ m_unhandledQueries.push_back(_input);
+ return "unknown\n";
+ }
}
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index eb876a7f..55fc4096 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -19,9 +19,11 @@
#include <libsolidity/formal/SolverInterface.h>
-#include <libsolidity/interface/Exceptions.h>
+#include <liblangutil/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
+#include <libdevcore/FixedHash.h>
+
#include <libdevcore/Common.h>
#include <boost/noncopyable.hpp>
@@ -42,22 +44,26 @@ namespace smt
class SMTLib2Interface: public SolverInterface, public boost::noncopyable
{
public:
- explicit SMTLib2Interface(ReadCallback::Callback const& _queryCallback);
+ explicit SMTLib2Interface(std::map<h256, std::string> const& _queryResponses);
void reset() override;
void push() override;
void pop() override;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
- void declareInteger(std::string _name) override;
- void declareBool(std::string _name) override;
+ void declareVariable(std::string const&, Sort const&) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
+ std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; }
+
private:
+ void declareFunction(std::string const&, Sort const&);
+
std::string toSExpr(Expression const& _expr);
+ std::string toSmtLibSort(Sort const& _sort);
+ std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
void write(std::string _data);
@@ -67,10 +73,11 @@ private:
/// Communicates with the solver via the callback. Throws SMTSolverError on error.
std::string querySolver(std::string const& _input);
- ReadCallback::Callback m_queryCallback;
std::vector<std::string> m_accumulatedOutput;
- std::set<std::string> m_constants;
- std::set<std::string> m_functions;
+ std::set<std::string> m_variables;
+
+ std::map<h256, std::string> const& m_queryResponses;
+ std::vector<std::string> m_unhandledQueries;
};
}
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
index 8b9fe9ce..2a109b89 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -23,27 +23,22 @@
#ifdef HAVE_CVC4
#include <libsolidity/formal/CVC4Interface.h>
#endif
-#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
#include <libsolidity/formal/SMTLib2Interface.h>
-#endif
using namespace std;
using namespace dev;
using namespace dev::solidity;
using namespace dev::solidity::smt;
-SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback)
+SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
{
+ m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses));
#ifdef HAVE_Z3
m_solvers.emplace_back(make_shared<smt::Z3Interface>());
#endif
#ifdef HAVE_CVC4
m_solvers.emplace_back(make_shared<smt::CVC4Interface>());
#endif
-#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
- m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_readCallback)),
-#endif
- (void)_readCallback;
}
void SMTPortfolio::reset()
@@ -64,22 +59,10 @@ void SMTPortfolio::pop()
s->pop();
}
-void SMTPortfolio::declareFunction(string _name, Sort _domain, Sort _codomain)
-{
- for (auto s : m_solvers)
- s->declareFunction(_name, _domain, _codomain);
-}
-
-void SMTPortfolio::declareInteger(string _name)
-{
- for (auto s : m_solvers)
- s->declareInteger(_name);
-}
-
-void SMTPortfolio::declareBool(string _name)
+void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
{
for (auto s : m_solvers)
- s->declareBool(_name);
+ s->declareVariable(_name, _sort);
}
void SMTPortfolio::addAssertion(Expression const& _expr)
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h
index 96c7ff57..7f5ba37e 100644
--- a/libsolidity/formal/SMTPortfolio.h
+++ b/libsolidity/formal/SMTPortfolio.h
@@ -22,8 +22,11 @@
#include <libsolidity/interface/ReadFile.h>
+#include <libdevcore/FixedHash.h>
+
#include <boost/noncopyable.hpp>
+#include <map>
#include <vector>
namespace dev
@@ -42,20 +45,19 @@ namespace smt
class SMTPortfolio: public SolverInterface, public boost::noncopyable
{
public:
- SMTPortfolio(ReadCallback::Callback const& _readCallback);
+ SMTPortfolio(std::map<h256, std::string> const& _smtlib2Responses);
void reset() override;
void push() override;
void pop() override;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
- void declareInteger(std::string _name) override;
- void declareBool(std::string _name) override;
+ void declareVariable(std::string const&, Sort const&) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
+ std::vector<std::string> unhandledQueries() override { return m_solvers.at(0)->unhandledQueries(); }
private:
static bool solverAnswered(CheckResult result);
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index af1cc8e4..4a4b3fb1 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -17,7 +17,7 @@
#pragma once
-#include <libsolidity/interface/Exceptions.h>
+#include <liblangutil/Exceptions.h>
#include <libsolidity/interface/ReadFile.h>
#include <libdevcore/Common.h>
@@ -42,12 +42,68 @@ enum class CheckResult
SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR
};
-enum class Sort
+enum class Kind
{
Int,
Bool,
- IntIntFun, // Function of one Int returning a single Int
- IntBoolFun // Function of one Int returning a single Bool
+ Function,
+ Array
+};
+
+struct Sort
+{
+ Sort(Kind _kind):
+ kind(_kind) {}
+ virtual ~Sort() = default;
+ virtual bool operator==(Sort const& _other) const { return kind == _other.kind; }
+
+ Kind const kind;
+};
+using SortPointer = std::shared_ptr<Sort>;
+
+struct FunctionSort: public Sort
+{
+ FunctionSort(std::vector<SortPointer> _domain, SortPointer _codomain):
+ Sort(Kind::Function), domain(std::move(_domain)), codomain(std::move(_codomain)) {}
+ bool operator==(Sort const& _other) const override
+ {
+ if (!Sort::operator==(_other))
+ return false;
+ auto _otherFunction = dynamic_cast<FunctionSort const*>(&_other);
+ solAssert(_otherFunction, "");
+ if (domain.size() != _otherFunction->domain.size())
+ return false;
+ if (!std::equal(
+ domain.begin(),
+ domain.end(),
+ _otherFunction->domain.begin(),
+ [&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
+ ))
+ return false;
+ return *codomain == *_otherFunction->codomain;
+ }
+
+ std::vector<SortPointer> domain;
+ SortPointer codomain;
+};
+
+struct ArraySort: public Sort
+{
+ /// _domain is the sort of the indices
+ /// _range is the sort of the values
+ ArraySort(SortPointer _domain, SortPointer _range):
+ Sort(Kind::Array), domain(std::move(_domain)), range(std::move(_range)) {}
+ bool operator==(Sort const& _other) const override
+ {
+ if (!Sort::operator==(_other))
+ return false;
+ auto _otherArray = dynamic_cast<ArraySort const*>(&_other);
+ solAssert(_otherArray, "");
+ return *domain == *_otherArray->domain && *range == *_otherArray->range;
+ }
+
+ SortPointer domain;
+ SortPointer range;
};
/// C++ representation of an SMTLIB2 expression.
@@ -55,10 +111,10 @@ class Expression
{
friend class SolverInterface;
public:
- explicit Expression(bool _v): name(_v ? "true" : "false"), sort(Sort::Bool) {}
- Expression(size_t _number): name(std::to_string(_number)), sort(Sort::Int) {}
- Expression(u256 const& _number): name(_number.str()), sort(Sort::Int) {}
- Expression(bigint const& _number): name(_number.str()), sort(Sort::Int) {}
+ explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
+ Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
+ Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
+ Expression(bigint const& _number): Expression(_number.str(), Kind::Int) {}
Expression(Expression const&) = default;
Expression(Expression&&) = default;
@@ -80,17 +136,20 @@ public:
{"+", 2},
{"-", 2},
{"*", 2},
- {"/", 2}
+ {"/", 2},
+ {"select", 2},
+ {"store", 3}
};
return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size();
}
static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
{
- solAssert(_trueValue.sort == _falseValue.sort, "");
+ solAssert(*_trueValue.sort == *_falseValue.sort, "");
+ SortPointer sort = _trueValue.sort;
return Expression("ite", std::vector<Expression>{
std::move(_condition), std::move(_trueValue), std::move(_falseValue)
- }, _trueValue.sort);
+ }, std::move(sort));
}
static Expression implies(Expression _a, Expression _b)
@@ -98,21 +157,51 @@ public:
return !std::move(_a) || std::move(_b);
}
+ /// select is the SMT representation of an array index access.
+ static Expression select(Expression _array, Expression _index)
+ {
+ solAssert(_array.sort->kind == Kind::Array, "");
+ auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
+ solAssert(arraySort, "");
+ solAssert(*arraySort->domain == *_index.sort, "");
+ return Expression(
+ "select",
+ std::vector<Expression>{std::move(_array), std::move(_index)},
+ arraySort->range
+ );
+ }
+
+ /// store is the SMT representation of an assignment to array index.
+ /// The function is pure and returns the modified array.
+ static Expression store(Expression _array, Expression _index, Expression _element)
+ {
+ solAssert(_array.sort->kind == Kind::Array, "");
+ auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
+ solAssert(arraySort, "");
+ solAssert(*arraySort->domain == *_index.sort, "");
+ solAssert(*arraySort->range == *_element.sort, "");
+ return Expression(
+ "store",
+ std::vector<Expression>{std::move(_array), std::move(_index), std::move(_element)},
+ _array.sort
+ );
+ }
+
friend Expression operator!(Expression _a)
{
- return Expression("not", std::move(_a), Sort::Bool);
+ return Expression("not", std::move(_a), Kind::Bool);
}
friend Expression operator&&(Expression _a, Expression _b)
{
- return Expression("and", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression("and", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator||(Expression _a, Expression _b)
{
- return Expression("or", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression("or", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator==(Expression _a, Expression _b)
{
- return Expression("=", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression("=", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator!=(Expression _a, Expression _b)
{
@@ -120,72 +209,64 @@ public:
}
friend Expression operator<(Expression _a, Expression _b)
{
- return Expression("<", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression("<", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator<=(Expression _a, Expression _b)
{
- return Expression("<=", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression("<=", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator>(Expression _a, Expression _b)
{
- return Expression(">", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression(">", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator>=(Expression _a, Expression _b)
{
- return Expression(">=", std::move(_a), std::move(_b), Sort::Bool);
+ return Expression(">=", std::move(_a), std::move(_b), Kind::Bool);
}
friend Expression operator+(Expression _a, Expression _b)
{
- return Expression("+", std::move(_a), std::move(_b), Sort::Int);
+ return Expression("+", std::move(_a), std::move(_b), Kind::Int);
}
friend Expression operator-(Expression _a, Expression _b)
{
- return Expression("-", std::move(_a), std::move(_b), Sort::Int);
+ return Expression("-", std::move(_a), std::move(_b), Kind::Int);
}
friend Expression operator*(Expression _a, Expression _b)
{
- return Expression("*", std::move(_a), std::move(_b), Sort::Int);
+ return Expression("*", std::move(_a), std::move(_b), Kind::Int);
}
friend Expression operator/(Expression _a, Expression _b)
{
- return Expression("/", std::move(_a), std::move(_b), Sort::Int);
+ return Expression("/", std::move(_a), std::move(_b), Kind::Int);
}
- Expression operator()(Expression _a) const
+ Expression operator()(std::vector<Expression> _arguments) const
{
solAssert(
- arguments.empty(),
+ sort->kind == Kind::Function,
"Attempted function application to non-function."
);
- switch (sort)
- {
- case Sort::IntIntFun:
- return Expression(name, _a, Sort::Int);
- case Sort::IntBoolFun:
- return Expression(name, _a, Sort::Bool);
- default:
- solAssert(
- false,
- "Attempted function application to invalid type."
- );
- break;
- }
+ auto fSort = dynamic_cast<FunctionSort const*>(sort.get());
+ solAssert(fSort, "");
+ return Expression(name, std::move(_arguments), fSort->codomain);
}
std::string name;
std::vector<Expression> arguments;
- Sort sort;
+ SortPointer sort;
private:
- /// Manual constructor, should only be used by SolverInterface and this class itself.
- Expression(std::string _name, std::vector<Expression> _arguments, Sort _sort):
- name(std::move(_name)), arguments(std::move(_arguments)), sort(_sort) {}
-
- explicit Expression(std::string _name, Sort _sort):
- Expression(std::move(_name), std::vector<Expression>{}, _sort) {}
- Expression(std::string _name, Expression _arg, Sort _sort):
- Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}, _sort) {}
- Expression(std::string _name, Expression _arg1, Expression _arg2, Sort _sort):
- Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}, _sort) {}
+ /// Manual constructors, should only be used by SolverInterface and this class itself.
+ Expression(std::string _name, std::vector<Expression> _arguments, SortPointer _sort):
+ name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {}
+ Expression(std::string _name, std::vector<Expression> _arguments, Kind _kind):
+ Expression(std::move(_name), std::move(_arguments), std::make_shared<Sort>(_kind)) {}
+
+ explicit Expression(std::string _name, Kind _kind):
+ Expression(std::move(_name), std::vector<Expression>{}, _kind) {}
+ Expression(std::string _name, Expression _arg, Kind _kind):
+ Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}, _kind) {}
+ Expression(std::string _name, Expression _arg1, Expression _arg2, Kind _kind):
+ Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}, _kind) {}
};
DEV_SIMPLE_EXCEPTION(SolverError);
@@ -199,36 +280,12 @@ public:
virtual void push() = 0;
virtual void pop() = 0;
- virtual void declareFunction(std::string _name, Sort _domain, Sort _codomain) = 0;
- Expression newFunction(std::string _name, Sort _domain, Sort _codomain)
- {
- declareFunction(_name, _domain, _codomain);
- solAssert(_domain == Sort::Int, "Function sort not supported.");
- // Subclasses should do something here
- switch (_codomain)
- {
- case Sort::Int:
- return Expression(std::move(_name), {}, Sort::IntIntFun);
- case Sort::Bool:
- return Expression(std::move(_name), {}, Sort::IntBoolFun);
- default:
- solAssert(false, "Function sort not supported.");
- break;
- }
- }
- virtual void declareInteger(std::string _name) = 0;
- Expression newInteger(std::string _name)
+ virtual void declareVariable(std::string const& _name, Sort const& _sort) = 0;
+ Expression newVariable(std::string _name, SortPointer _sort)
{
// Subclasses should do something here
- declareInteger(_name);
- return Expression(std::move(_name), {}, Sort::Int);
- }
- virtual void declareBool(std::string _name) = 0;
- Expression newBool(std::string _name)
- {
- // Subclasses should do something here
- declareBool(_name);
- return Expression(std::move(_name), {}, Sort::Bool);
+ declareVariable(_name, *_sort);
+ return Expression(std::move(_name), {}, std::move(_sort));
}
virtual void addAssertion(Expression const& _expr) = 0;
@@ -238,6 +295,9 @@ public:
virtual std::pair<CheckResult, std::vector<std::string>>
check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
+ /// @returns a list of queries that the system was not able to respond to.
+ virtual std::vector<std::string> unhandledQueries() { return {}; }
+
protected:
// SMT query timeout in milliseconds.
static int const queryTimeout = 10000;
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 3eb1c1ce..c297c807 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -24,6 +24,50 @@
using namespace std;
using namespace dev::solidity;
+smt::SortPointer dev::solidity::smtSort(Type const& _type)
+{
+ switch (smtKind(_type.category()))
+ {
+ case smt::Kind::Int:
+ return make_shared<smt::Sort>(smt::Kind::Int);
+ case smt::Kind::Bool:
+ return make_shared<smt::Sort>(smt::Kind::Bool);
+ case smt::Kind::Function:
+ {
+ auto fType = dynamic_cast<FunctionType 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));
+ return make_shared<smt::FunctionSort>(parameterSorts, returnSort);
+ }
+ case smt::Kind::Array:
+ {
+ solUnimplementedAssert(false, "Invalid type");
+ }
+ }
+ solAssert(false, "Invalid type");
+}
+
+vector<smt::SortPointer> dev::solidity::smtSort(vector<TypePointer> const& _types)
+{
+ vector<smt::SortPointer> sorts;
+ for (auto const& type: _types)
+ sorts.push_back(smtSort(*type));
+ return sorts;
+}
+
+smt::Kind dev::solidity::smtKind(Type::Category _category)
+{
+ if (isNumber(_category))
+ return smt::Kind::Int;
+ else if (isBool(_category))
+ return smt::Kind::Bool;
+ solAssert(false, "Invalid type");
+}
+
bool dev::solidity::isSupportedType(Type::Category _category)
{
return isNumber(_category) ||
@@ -125,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));
+ }
+}
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index dcdd9ea4..984653b3 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -28,6 +28,12 @@ namespace dev
namespace solidity
{
+/// Returns the SMT sort that models the Solidity type _type.
+smt::SortPointer smtSort(Type const& _type);
+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.
bool isSupportedType(Type::Category _category);
@@ -49,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);
+
+}
+
}
}
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index 85818ba0..efaeb97a 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -37,6 +37,11 @@ SymbolicVariable::SymbolicVariable(
{
}
+string SymbolicVariable::currentName() const
+{
+ return uniqueSymbol(m_ssa->index());
+}
+
string SymbolicVariable::uniqueSymbol(unsigned _index) const
{
return m_uniqueName + "_" + to_string(_index);
@@ -54,16 +59,7 @@ SymbolicBoolVariable::SymbolicBoolVariable(
smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
{
- return m_interface.newBool(uniqueSymbol(_index));
-}
-
-void SymbolicBoolVariable::setZeroValue()
-{
- m_interface.addAssertion(currentValue() == smt::Expression(false));
-}
-
-void SymbolicBoolVariable::setUnknownValue()
-{
+ return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Bool));
}
SymbolicIntVariable::SymbolicIntVariable(
@@ -78,20 +74,7 @@ SymbolicIntVariable::SymbolicIntVariable(
smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
{
- return m_interface.newInteger(uniqueSymbol(_index));
-}
-
-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));
+ return m_interface.newVariable(uniqueSymbol(_index), make_shared<smt::Sort>(smt::Kind::Int));
}
SymbolicAddressVariable::SymbolicAddressVariable(
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index 4fd9b245..fcf32760 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -51,6 +51,8 @@ public:
return valueAtIndex(m_ssa->index());
}
+ std::string currentName() const;
+
virtual smt::Expression valueAtIndex(int _index) const = 0;
smt::Expression increaseIndex()
@@ -62,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;
};
/**
@@ -90,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;
};
@@ -111,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;
};
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 9a0ccf48..cb01dc61 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -17,7 +17,7 @@
#include <libsolidity/formal/Z3Interface.h>
-#include <libsolidity/interface/Exceptions.h>
+#include <liblangutil/Exceptions.h>
#include <libdevcore/CommonIO.h>
@@ -51,22 +51,22 @@ void Z3Interface::pop()
m_solver.pop();
}
-void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void Z3Interface::declareVariable(string const& _name, Sort const& _sort)
{
- if (!m_functions.count(_name))
- m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
-}
-
-void Z3Interface::declareInteger(string _name)
-{
- if (!m_constants.count(_name))
- m_constants.insert({_name, m_context.int_const(_name.c_str())});
+ if (_sort.kind == Kind::Function)
+ declareFunction(_name, _sort);
+ else if (!m_constants.count(_name))
+ m_constants.insert({_name, m_context.constant(_name.c_str(), z3Sort(_sort))});
}
-void Z3Interface::declareBool(string _name)
+void Z3Interface::declareFunction(string const& _name, Sort const& _sort)
{
- if (!m_constants.count(_name))
- m_constants.insert({_name, m_context.bool_const(_name.c_str())});
+ solAssert(_sort.kind == smt::Kind::Function, "");
+ if (!m_functions.count(_name))
+ {
+ FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
+ m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain))});
+ }
}
void Z3Interface::addAssertion(Expression const& _expr)
@@ -163,19 +163,28 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return arguments[0] * arguments[1];
else if (n == "/")
return arguments[0] / arguments[1];
+ else if (n == "select")
+ return z3::select(arguments[0], arguments[1]);
+ else if (n == "store")
+ return z3::store(arguments[0], arguments[1], arguments[2]);
// Cannot reach here.
solAssert(false, "");
return arguments[0];
}
-z3::sort Z3Interface::z3Sort(Sort _sort)
+z3::sort Z3Interface::z3Sort(Sort const& _sort)
{
- switch (_sort)
+ switch (_sort.kind)
{
- case Sort::Bool:
+ case Kind::Bool:
return m_context.bool_sort();
- case Sort::Int:
+ case Kind::Int:
return m_context.int_sort();
+ case Kind::Array:
+ {
+ auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
+ return m_context.array_sort(z3Sort(*arraySort.domain), z3Sort(*arraySort.range));
+ }
default:
break;
}
@@ -183,3 +192,11 @@ z3::sort Z3Interface::z3Sort(Sort _sort)
// Cannot be reached.
return m_context.int_sort();
}
+
+z3::sort_vector Z3Interface::z3Sort(vector<SortPointer> const& _sorts)
+{
+ z3::sort_vector z3Sorts(m_context);
+ for (auto const& _sort: _sorts)
+ z3Sorts.push_back(z3Sort(*_sort));
+ return z3Sorts;
+}
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
index 84880ff3..86e1badd 100644
--- a/libsolidity/formal/Z3Interface.h
+++ b/libsolidity/formal/Z3Interface.h
@@ -40,16 +40,17 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
- void declareInteger(std::string _name) override;
- void declareBool(std::string _name) override;
+ void declareVariable(std::string const& _name, Sort const& _sort) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
private:
+ void declareFunction(std::string const& _name, Sort const& _sort);
+
z3::expr toZ3Expr(Expression const& _expr);
- z3::sort z3Sort(smt::Sort _sort);
+ z3::sort z3Sort(smt::Sort const& _sort);
+ z3::sort_vector z3Sort(std::vector<smt::SortPointer> const& _sorts);
z3::context m_context;
z3::solver m_solver;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-28 01:02:41 +0800