aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/CVC4Interface.cpp10
-rw-r--r--libsolidity/formal/CVC4Interface.h3
-rw-r--r--libsolidity/formal/SMTChecker.cpp22
-rw-r--r--libsolidity/formal/SMTChecker.h6
-rw-r--r--libsolidity/formal/SMTLib2Interface.cpp20
-rw-r--r--libsolidity/formal/SMTLib2Interface.h3
-rw-r--r--libsolidity/formal/SMTPortfolio.cpp2
-rw-r--r--libsolidity/formal/SMTPortfolio.h2
-rw-r--r--libsolidity/formal/SolverInterface.h27
-rw-r--r--libsolidity/formal/SymbolicTypes.cpp9
-rw-r--r--libsolidity/formal/SymbolicTypes.h3
-rw-r--r--libsolidity/formal/SymbolicVariables.cpp5
-rw-r--r--libsolidity/formal/SymbolicVariables.h2
-rw-r--r--libsolidity/formal/Z3Interface.cpp10
-rw-r--r--libsolidity/formal/Z3Interface.h3
15 files changed, 102 insertions, 25 deletions
diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index 6cb91483..11822927 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -50,7 +50,7 @@ void CVC4Interface::pop()
m_solver.pop();
}
-void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void CVC4Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
{
if (!m_functions.count(_name))
{
@@ -201,3 +201,11 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)
// Cannot be reached.
return m_context.integerType();
}
+
+vector<CVC4::Type> CVC4Interface::cvc4Sort(vector<Sort> 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..273dce23 100644
--- a/libsolidity/formal/CVC4Interface.h
+++ b/libsolidity/formal/CVC4Interface.h
@@ -51,7 +51,7 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+ void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
void declareInteger(std::string _name) override;
void declareBool(std::string _name) override;
@@ -61,6 +61,7 @@ public:
private:
CVC4::Expr toCVC4Expr(Expression const& _expr);
CVC4::Type cvc4Sort(smt::Sort _sort);
+ std::vector<CVC4::Type> cvc4Sort(std::vector<smt::Sort> const& _sort);
CVC4::ExprManager m_context;
CVC4::SmtEngine m_solver;
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index cc580021..9a2b9bbf 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -78,6 +78,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);
}
@@ -412,9 +415,12 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
{
- string blockHash = "blockhash()";
- // TODO Define blockhash as an uninterpreted function
- defineSpecialVariable(blockHash, _funCall);
+ string blockHash = "blockhash";
+ defineUninterpretedFunction(blockHash, {smt::Sort::Int}, smt::Sort::Int);
+ auto const& arguments = _funCall.arguments();
+ solAssert(arguments.size() == 1, "");
+ defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments[0])}));
+ m_uninterpretedTerms.push_back(&_funCall);
}
void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
@@ -587,6 +593,11 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e
defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
}
+void SMTChecker::defineUninterpretedFunction(string const& _name, vector<smt::Sort> const& _domain, smt::Sort _codomain)
+{
+ if (!m_uninterpretedFunctions.count(_name))
+ m_uninterpretedFunctions.emplace(_name, m_interface->newFunction(_name, _domain, _codomain));
+}
void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
{
@@ -770,6 +781,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;
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index a7f955dd..869c9c50 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -83,6 +83,7 @@ private:
void inlineFunctionCall(FunctionCall const&);
void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
+ void defineUninterpretedFunction(std::string const& _name, std::vector<smt::Sort> const& _domain, smt::Sort _codomain);
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
@@ -193,6 +194,11 @@ 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;
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index a6c1f87c..54542233 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -64,9 +64,12 @@ void SMTLib2Interface::pop()
m_accumulatedOutput.pop_back();
}
-void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void SMTLib2Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
{
// TODO Use domain and codomain as key as well
+ string domain("");
+ for (auto const& sort: _domain)
+ domain += toSmtLibSort(sort) + ' ';
if (!m_functions.count(_name))
{
m_functions.insert(_name);
@@ -74,7 +77,7 @@ void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomai
"(declare-fun |" +
_name +
"| (" +
- (_domain == Sort::Int ? "Int" : "Bool") +
+ domain +
") " +
(_codomain == Sort::Int ? "Int" : "Bool") +
")"
@@ -140,6 +143,19 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
return sexpr;
}
+string SMTLib2Interface::toSmtLibSort(Sort _sort)
+{
+ switch (_sort)
+ {
+ case Sort::Int:
+ return "Int";
+ case Sort::Bool:
+ return "Bool";
+ default:
+ solAssert(false, "Invalid SMT sort");
+ }
+}
+
void SMTLib2Interface::write(string _data)
{
solAssert(!m_accumulatedOutput.empty(), "");
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index eb876a7f..08ad74da 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -49,7 +49,7 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+ void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
void declareInteger(std::string _name) override;
void declareBool(std::string _name) override;
@@ -58,6 +58,7 @@ public:
private:
std::string toSExpr(Expression const& _expr);
+ std::string toSmtLibSort(Sort _sort);
void write(std::string _data);
diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
index 8b9fe9ce..e1cde04c 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -64,7 +64,7 @@ void SMTPortfolio::pop()
s->pop();
}
-void SMTPortfolio::declareFunction(string _name, Sort _domain, Sort _codomain)
+void SMTPortfolio::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
{
for (auto s : m_solvers)
s->declareFunction(_name, _domain, _codomain);
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h
index 96c7ff57..50bd87d4 100644
--- a/libsolidity/formal/SMTPortfolio.h
+++ b/libsolidity/formal/SMTPortfolio.h
@@ -49,7 +49,7 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+ void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
void declareInteger(std::string _name) override;
void declareBool(std::string _name) override;
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index af1cc8e4..a6618fb5 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -45,9 +45,7 @@ enum class CheckResult
enum class Sort
{
Int,
- Bool,
- IntIntFun, // Function of one Int returning a single Int
- IntBoolFun // Function of one Int returning a single Bool
+ Bool
};
/// C++ representation of an SMTLIB2 expression.
@@ -150,7 +148,7 @@ public:
{
return Expression("/", std::move(_a), std::move(_b), Sort::Int);
}
- Expression operator()(Expression _a) const
+ Expression operator()(std::vector<Expression> _arguments) const
{
solAssert(
arguments.empty(),
@@ -158,10 +156,10 @@ public:
);
switch (sort)
{
- case Sort::IntIntFun:
- return Expression(name, _a, Sort::Int);
- case Sort::IntBoolFun:
- return Expression(name, _a, Sort::Bool);
+ case Sort::Int:
+ return Expression(name, std::move(_arguments), Sort::Int);
+ case Sort::Bool:
+ return Expression(name, std::move(_arguments), Sort::Bool);
default:
solAssert(
false,
@@ -199,18 +197,21 @@ 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)
+ virtual void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) = 0;
+ void declareFunction(std::string _name, Sort _domain, Sort _codomain)
+ {
+ declareFunction(std::move(_name), std::vector<Sort>{std::move(_domain)}, std::move(_codomain));
+ }
+ Expression newFunction(std::string _name, std::vector<Sort> const& _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);
+ return Expression(std::move(_name), {}, Sort::Int);
case Sort::Bool:
- return Expression(std::move(_name), {}, Sort::IntBoolFun);
+ return Expression(std::move(_name), {}, Sort::Bool);
default:
solAssert(false, "Function sort not supported.");
break;
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 3eb1c1ce..78bf861b 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -24,6 +24,15 @@
using namespace std;
using namespace dev::solidity;
+smt::Sort dev::solidity::smtSort(Type::Category _category)
+{
+ if (isNumber(_category))
+ return smt::Sort::Int;
+ else if (isBool(_category))
+ return smt::Sort::Bool;
+ solAssert(false, "Invalid type");
+}
+
bool dev::solidity::isSupportedType(Type::Category _category)
{
return isNumber(_category) ||
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index dcdd9ea4..2639fcb9 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -28,6 +28,9 @@ namespace dev
namespace solidity
{
+/// Returns the SMT sort that models the Solidity type _type.
+smt::Sort smtSort(Type::Category _type);
+
/// So far int, bool and address are supported.
/// Returns true if type is supported.
bool isSupportedType(Type::Category _category);
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index 85818ba0..194c843e 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);
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index 4fd9b245..13b944a5 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()
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 9a0ccf48..2519e41b 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -51,7 +51,7 @@ void Z3Interface::pop()
m_solver.pop();
}
-void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
+void Z3Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
{
if (!m_functions.count(_name))
m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
@@ -183,3 +183,11 @@ z3::sort Z3Interface::z3Sort(Sort _sort)
// Cannot be reached.
return m_context.int_sort();
}
+
+z3::sort_vector Z3Interface::z3Sort(vector<Sort> 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..5eae618e 100644
--- a/libsolidity/formal/Z3Interface.h
+++ b/libsolidity/formal/Z3Interface.h
@@ -40,7 +40,7 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+ void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
void declareInteger(std::string _name) override;
void declareBool(std::string _name) override;
@@ -50,6 +50,7 @@ public:
private:
z3::expr toZ3Expr(Expression const& _expr);
z3::sort z3Sort(smt::Sort _sort);
+ z3::sort_vector z3Sort(std::vector<smt::Sort> const& _sort);
z3::context m_context;
z3::solver m_solver;
generated by cgit (git 2.34.1) at 2024-11-18 07:37:15 +0800