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

Review changes.

Browse Source
This commit is contained in:
chriseth 2017-08-21 17:02:47 +02:00
parent 8853183d06
commit cf5e1d6120
6 changed files with 27 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
libsolidity/formal/SMTChecker.cpp
View File

@ -438,7 +438,7 @@ void SMTChecker::checkCondition(
switch (result) switch (result)
{ {
case smt::CheckResult::SAT: case smt::CheckResult::SATISFIABLE:
{ {
std::ostringstream message; std::ostringstream message;
message << _description << " happens here"; message << _description << " happens here";
@ -464,7 +464,7 @@ void SMTChecker::checkCondition(
m_errorReporter.warning(_location, message.str()); m_errorReporter.warning(_location, message.str());
break; break;
} }
case smt::CheckResult::UNSAT: case smt::CheckResult::UNSATISFIABLE:
break; break;
case smt::CheckResult::UNKNOWN: case smt::CheckResult::UNKNOWN:
m_errorReporter.warning(_location, _description + " might happen here."); m_errorReporter.warning(_location, _description + " might happen here.");
@ -484,10 +484,10 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
{ {
solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, ""); solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, ""); solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
solAssert(m_z3Variables.count(&_varDecl) == 0, ""); solAssert(m_Variables.count(&_varDecl) == 0, "");
m_currentSequenceCounter[&_varDecl] = 0; m_currentSequenceCounter[&_varDecl] = 0;
m_nextFreeSequenceCounter[&_varDecl] = 1; m_nextFreeSequenceCounter[&_varDecl] = 1;
m_z3Variables.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); setValue(_varDecl, _setToZero);
} }
else else
@ -556,7 +556,7 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t)
smt::Expression SMTChecker::expr(Expression const& _e) smt::Expression SMTChecker::expr(Expression const& _e)
{ {
if (!m_z3Expressions.count(&_e)) if (!m_Expressions.count(&_e))
{ {
solAssert(_e.annotation().type, ""); solAssert(_e.annotation().type, "");
switch (_e.annotation().type->category()) switch (_e.annotation().type->category())
@ -565,24 +565,24 @@ smt::Expression SMTChecker::expr(Expression const& _e)
{ {
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get())) if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
solAssert(!rational->isFractional(), ""); solAssert(!rational->isFractional(), "");
m_z3Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
break; break;
} }
case Type::Category::Integer: case Type::Category::Integer:
m_z3Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
break; break;
case Type::Category::Bool: case Type::Category::Bool:
m_z3Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
break; break;
default: default:
solAssert(false, "Type not implemented."); solAssert(false, "Type not implemented.");
} }
} }
return m_z3Expressions.at(&_e); return m_Expressions.at(&_e);
} }
smt::Expression SMTChecker::var(Declaration const& _decl) smt::Expression SMTChecker::var(Declaration const& _decl)
{ {
solAssert(m_z3Variables.count(&_decl), ""); solAssert(m_Variables.count(&_decl), "");
return m_z3Variables.at(&_decl); return m_Variables.at(&_decl);
} }

12
libsolidity/formal/SMTChecker.h
View File

@ -71,8 +71,8 @@ private:
void createVariable(VariableDeclaration const& _varDecl, bool _setToZero); void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
std::string uniqueSymbol(Declaration const& _decl); static std::string uniqueSymbol(Declaration const& _decl);
std::string uniqueSymbol(Expression const& _expr); static std::string uniqueSymbol(Expression const& _expr);
/// @returns true if _delc is a variable that is known at the current point, i.e. /// @returns true if _delc is a variable that is known at the current point, i.e.
/// has a valid sequence number /// has a valid sequence number
@ -90,8 +90,8 @@ private:
/// Sets the value of the declaration either to zero or to its intrinsic range. /// Sets the value of the declaration either to zero or to its intrinsic range.
void setValue(Declaration const& _decl, bool _setToZero); void setValue(Declaration const& _decl, bool _setToZero);
smt::Expression minValue(IntegerType const& _t); static smt::Expression minValue(IntegerType const& _t);
smt::Expression maxValue(IntegerType const& _t); static smt::Expression maxValue(IntegerType const& _t);
/// Returns the expression corresponding to the AST node. Creates a new expression /// Returns the expression corresponding to the AST node. Creates a new expression
/// if it does not exist yet. /// if it does not exist yet.
@ -103,8 +103,8 @@ private:
std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<smt::SolverInterface> m_interface;
std::map<Declaration const*, int> m_currentSequenceCounter; std::map<Declaration const*, int> m_currentSequenceCounter;
std::map<Declaration const*, int> m_nextFreeSequenceCounter; std::map<Declaration const*, int> m_nextFreeSequenceCounter;
std::map<Expression const*, smt::Expression> m_z3Expressions; std::map<Expression const*, smt::Expression> m_Expressions;
std::map<Declaration const*, smt::Expression> m_z3Variables; std::map<Declaration const*, smt::Expression> m_Variables;
ErrorReporter& m_errorReporter; ErrorReporter& m_errorReporter;
FunctionDefinition const* m_currentFunction = nullptr; FunctionDefinition const* m_currentFunction = nullptr;

6
libsolidity/formal/SMTLib2Interface.cpp
View File

@ -103,16 +103,16 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con
CheckResult result; CheckResult result;
// TODO proper parsing // TODO proper parsing
if (boost::starts_with(response, "sat\n")) if (boost::starts_with(response, "sat\n"))
result = CheckResult::SAT; result = CheckResult::SATISFIABLE;
else if (boost::starts_with(response, "unsat\n")) else if (boost::starts_with(response, "unsat\n"))
result = CheckResult::UNSAT; result = CheckResult::UNSATISFIABLE;
else if (boost::starts_with(response, "unknown\n")) else if (boost::starts_with(response, "unknown\n"))
result = CheckResult::UNKNOWN; result = CheckResult::UNKNOWN;
else else
result = CheckResult::ERROR; result = CheckResult::ERROR;
vector<string> values; vector<string> values;
if (result != CheckResult::UNSAT && result != CheckResult::ERROR) if (result != CheckResult::UNSATISFIABLE && result != CheckResult::ERROR)
values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend()); values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend());
return make_pair(result, values); return make_pair(result, values);
} }

2
libsolidity/formal/SolverInterface.h
View File

@ -39,7 +39,7 @@ namespace smt
enum class CheckResult enum class CheckResult
{ {
SAT, UNSAT, UNKNOWN, ERROR SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR
}; };
enum class Sort enum class Sort

6
libsolidity/formal/Z3Interface.cpp
View File

@ -78,11 +78,11 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
switch (m_solver.check()) switch (m_solver.check())
{ {
case z3::check_result::sat: case z3::check_result::sat:
result = CheckResult::SAT; result = CheckResult::SATISFIABLE;
cout << "sat" << endl; cout << "sat" << endl;
break; break;
case z3::check_result::unsat: case z3::check_result::unsat:
result = CheckResult::UNSAT; result = CheckResult::UNSATISFIABLE;
cout << "unsat" << endl; cout << "unsat" << endl;
break; break;
case z3::check_result::unknown: case z3::check_result::unknown:
@ -96,7 +96,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
vector<string> values; vector<string> values;
if (result != CheckResult::UNSAT) if (result != CheckResult::UNSATISFIABLE)
{ {
z3::model m = m_solver.get_model(); z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate) for (Expression const& e: _expressionsToEvaluate)

3
scripts/install_deps.sh
View File

@ -317,7 +317,8 @@ case $(uname -s) in
build-essential \ build-essential \
cmake \ cmake \
git \ git \
libboost-all-dev "$install_z3" libboost-all-dev \
"$install_z3"
if [ "$CI" = true ]; then if [ "$CI" = true ]; then
# Install 'eth', for use in the Solidity Tests-over-IPC. # Install 'eth', for use in the Solidity Tests-over-IPC.
# We will not use this 'eth', but its dependencies # We will not use this 'eth', but its dependencies