cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #3091 from ethereum/smt-cleanup

Browse Source 
Various cleanups to Z3
This commit is contained in:
Alex Beregszaszi 2017-10-17 19:14:43 +01:00 committed by GitHub
commit a17996cdad
4 changed files with 41 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libsolidity/ast/ASTForward.h
View File

@ -57,6 +57,7 @@ class UserDefinedTypeName;
class FunctionTypeName;
class Mapping;
class ArrayTypeName;
class InlineAssembly;
class Statement;
class Block;
class PlaceholderStatement;

18
libsolidity/formal/SMTChecker.cpp
View File

@ -494,10 +494,10 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
{
solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_Variables.count(&_varDecl) == 0, "");
solAssert(m_variables.count(&_varDecl) == 0, "");
m_currentSequenceCounter[&_varDecl] = 0;
m_nextFreeSequenceCounter[&_varDecl] = 1;
m_Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
setValue(_varDecl, _setToZero);
}
else
@ -566,7 +566,7 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t)
smt::Expression SMTChecker::expr(Expression const& _e)
{
if (!m_Expressions.count(&_e))
if (!m_expressions.count(&_e))
{
solAssert(_e.annotation().type, "");
switch (_e.annotation().type->category())
@ -575,24 +575,24 @@ smt::Expression SMTChecker::expr(Expression const& _e)
{
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
solAssert(!rational->isFractional(), "");
m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
break;
}
case Type::Category::Integer:
m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
break;
case Type::Category::Bool:
m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
break;
default:
solAssert(false, "Type not implemented.");
}
}
return m_Expressions.at(&_e);
return m_expressions.at(&_e);
}
smt::Expression SMTChecker::var(Declaration const& _decl)
{
solAssert(m_Variables.count(&_decl), "");
return m_Variables.at(&_decl);
solAssert(m_variables.count(&_decl), "");
return m_variables.at(&_decl);
}

4
libsolidity/formal/SMTChecker.h
View File

@ -103,8 +103,8 @@ private:
std::shared_ptr<smt::SolverInterface> m_interface;
std::map<Declaration const*, int> m_currentSequenceCounter;
std::map<Declaration const*, int> m_nextFreeSequenceCounter;
std::map<Expression const*, smt::Expression> m_Expressions;
std::map<Declaration const*, smt::Expression> m_Variables;
std::map<Expression const*, smt::Expression> m_expressions;
std::map<Declaration const*, smt::Expression> m_variables;
ErrorReporter& m_errorReporter;
FunctionDefinition const* m_currentFunction = nullptr;

50
libsolidity/formal/Z3Interface.cpp
View File

@ -73,28 +73,37 @@ void Z3Interface::addAssertion(Expression const& _expr)
pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
{
CheckResult result;
switch (m_solver.check())
vector<string> values;
try
{
case z3::check_result::sat:
result = CheckResult::SATISFIABLE;
break;
case z3::check_result::unsat:
result = CheckResult::UNSATISFIABLE;
break;
case z3::check_result::unknown:
result = CheckResult::UNKNOWN;
break;
default:
solAssert(false, "");
switch (m_solver.check())
{
case z3::check_result::sat:
result = CheckResult::SATISFIABLE;
break;
case z3::check_result::unsat:
result = CheckResult::UNSATISFIABLE;
break;
case z3::check_result::unknown:
result = CheckResult::UNKNOWN;
break;
default:
solAssert(false, "");
}
if (result != CheckResult::UNSATISFIABLE)
{
z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate)
values.push_back(toString(m.eval(toZ3Expr(e))));
}
}
catch (z3::exception const& _e)
{
result = CheckResult::ERROR;
values.clear();
}
vector<string> values;
if (result != CheckResult::UNSATISFIABLE)
{
z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate)
values.push_back(toString(m.eval(toZ3Expr(e))));
}
return make_pair(result, values);
}
@ -118,8 +127,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
{">=", 2},
{"+", 2},
{"-", 2},
{"*", 2},
{">=", 2}
{"*", 2}
};
string const& n = _expr.name;
if (m_functions.count(n))