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] Add CheckResult::CONFLICTING

Browse Source
This commit is contained in:
Leonardo Alt 2018-06-26 12:41:26 +02:00 committed by Alex Beregszaszi
parent 87a38e1abe
commit 55c1fb60b4
3 changed files with 10 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsolidity/formal/SMTChecker.cpp
View File

@ -617,6 +617,9 @@ void SMTChecker::checkCondition(
case smt::CheckResult::UNKNOWN:
m_errorReporter.warning(_location, _description + " might happen here." + loopComment);
break;
case smt::CheckResult::CONFLICTING:
m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
break;
case smt::CheckResult::ERROR:
m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
break;
@ -644,6 +647,8 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING)
m_errorReporter.warning(_condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound.");
else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE)
{
// everything fine.

7
libsolidity/formal/SMTPortfolio.cpp
View File

@ -92,7 +92,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr)
* This comment explains how this result is decided.
*
* When a solver is queried, there are four possible answers:
* SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, ERROR
* SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, CONFLICTING, ERROR
* We say that a solver _answered_ the query if it returns either:
* SAT or UNSAT
* A solver did not answer the query if it returns either:
@ -107,7 +107,7 @@ void SMTPortfolio::addAssertion(Expression const& _expr)
* because one buggy solver/integration shouldn't break the portfolio.
*
* 2) If at least one solver answers SAT and at least one answers UNSAT, at least one of them is buggy
* and the result is conflicting and we abort.
* and the result is CONFLICTING.
* In the future if we have more than 2 solvers enabled we could go with the majority.
*
* 3) If NO solver answers the query:
@ -135,7 +135,8 @@ pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const&
}
else if (lastResult != result)
{
solAssert(false, "At least two SMT solvers gave opposing results.");
lastResult = CheckResult::CONFLICTING;
break;
}
}
else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR)

2
libsolidity/formal/SolverInterface.h
View File

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