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

[SMTChecker] Implement uninterpreted functions and use it for blockhash()

Browse Source
This commit is contained in:
Leonardo Alt 2018-10-25 16:00:09 +02:00
parent 92ebf66067
commit 70bb0eaf95
17 changed files with 110 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -6,6 +6,8 @@ Language Features:
Compiler Features:
* Build System: LLL is not built anymore by default. Must configure it with CMake as `-DLLL=ON`.
* Code generator: Do not perform redundant double cleanup on unsigned integers when loading from calldata.
* SMTChecker: Support ``msg``, ``tx`` and ``block`` member variables.
* SMTChecker: Support ``gasleft()`` and ``blockhash()`` functions.
Bugfixes:

10
libsolidity/formal/CVC4Interface.cpp
View File

@ -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;
}

3
libsolidity/formal/CVC4Interface.h
View File

@ -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;

22
libsolidity/formal/SMTChecker.cpp
View File

@ -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;

6
libsolidity/formal/SMTChecker.h
View File

@ -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;

20
libsolidity/formal/SMTLib2Interface.cpp
View File

@ -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(), "");

3
libsolidity/formal/SMTLib2Interface.h
View File

@ -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);

2
libsolidity/formal/SMTPortfolio.cpp
View File

@ -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);

2
libsolidity/formal/SMTPortfolio.h
View File

@ -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;

27
libsolidity/formal/SolverInterface.h
View File

@ -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;

9
libsolidity/formal/SymbolicTypes.cpp
View File

@ -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) ||

3
libsolidity/formal/SymbolicTypes.h
View File

@ -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);

5
libsolidity/formal/SymbolicVariables.cpp
View File

@ -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);

2
libsolidity/formal/SymbolicVariables.h
View File

@ -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()

10
libsolidity/formal/Z3Interface.cpp
View File

@ -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;
}

3
libsolidity/formal/Z3Interface.h
View File

@ -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;

8
test/libsolidity/smtCheckerTests/special/blockhash.sol
View File

@ -2,9 +2,13 @@ pragma experimental SMTChecker;
contract C
{
function f() public payable {
function f(uint x) public payable {
assert(blockhash(x) > 0);
assert(blockhash(2) > 0);
uint y = x;
assert(blockhash(x) == blockhash(y));
}
}
// ----
// Warning: (79-103): Assertion violation happens here
// Warning: (85-109): Assertion violation happens here
// Warning: (113-137): Assertion violation happens here