mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
[SMTChecker] Report malformed expressions more precisely
This commit is contained in:
Leonardo Alt
parent
fc35c139ca
commit
1221eeebf1
@ -60,17 +60,21 @@ void CVC4Interface::addAssertion(Expression const& _expr)
|
||||
{
|
||||
m_solver.assertFormula(toCVC4Expr(_expr));
|
||||
}
|
||||
catch (CVC4::TypeCheckingException const&)
|
||||
catch (CVC4::TypeCheckingException const& _e)
|
||||
{
|
||||
solAssert(false, "");
|
||||
solAssert(false, _e.what());
|
||||
}
|
||||
catch (CVC4::LogicException const&)
|
||||
catch (CVC4::LogicException const& _e)
|
||||
{
|
||||
solAssert(false, "");
|
||||
solAssert(false, _e.what());
|
||||
}
|
||||
catch (CVC4::UnsafeInterruptException const&)
|
||||
catch (CVC4::UnsafeInterruptException const& _e)
|
||||
{
|
||||
solAssert(false, "");
|
||||
solAssert(false, _e.what());
|
||||
}
|
||||
catch (CVC4::Exception const& _e)
|
||||
{
|
||||
solAssert(false, _e.what());
|
||||
}
|
||||
}
|
||||
|
||||
@ -120,66 +124,82 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
|
||||
for (auto const& arg: _expr.arguments)
|
||||
arguments.push_back(toCVC4Expr(arg));
|
||||
|
||||
string const& n = _expr.name;
|
||||
// Function application
|
||||
if (!arguments.empty() && m_variables.count(_expr.name))
|
||||
return m_context.mkExpr(CVC4::kind::APPLY_UF, m_variables.at(n), arguments);
|
||||
// Literal
|
||||
else if (arguments.empty())
|
||||
try
|
||||
{
|
||||
if (n == "true")
|
||||
return m_context.mkConst(true);
|
||||
else if (n == "false")
|
||||
return m_context.mkConst(false);
|
||||
else
|
||||
try
|
||||
{
|
||||
return m_context.mkConst(CVC4::Rational(n));
|
||||
}
|
||||
catch (...)
|
||||
{
|
||||
solAssert(false, "");
|
||||
}
|
||||
string const& n = _expr.name;
|
||||
// Function application
|
||||
if (!arguments.empty() && m_variables.count(_expr.name))
|
||||
return m_context.mkExpr(CVC4::kind::APPLY_UF, m_variables.at(n), arguments);
|
||||
// Literal
|
||||
else if (arguments.empty())
|
||||
{
|
||||
if (n == "true")
|
||||
return m_context.mkConst(true);
|
||||
else if (n == "false")
|
||||
return m_context.mkConst(false);
|
||||
else
|
||||
try
|
||||
{
|
||||
return m_context.mkConst(CVC4::Rational(n));
|
||||
}
|
||||
catch (CVC4::TypeCheckingException const& _e)
|
||||
{
|
||||
solAssert(false, _e.what());
|
||||
}
|
||||
catch (CVC4::Exception const& _e)
|
||||
{
|
||||
solAssert(false, _e.what());
|
||||
}
|
||||
}
|
||||
|
||||
solAssert(_expr.hasCorrectArity(), "");
|
||||
if (n == "ite")
|
||||
return arguments[0].iteExpr(arguments[1], arguments[2]);
|
||||
else if (n == "not")
|
||||
return arguments[0].notExpr();
|
||||
else if (n == "and")
|
||||
return arguments[0].andExpr(arguments[1]);
|
||||
else if (n == "or")
|
||||
return arguments[0].orExpr(arguments[1]);
|
||||
else if (n == "implies")
|
||||
return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]);
|
||||
else if (n == "=")
|
||||
return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]);
|
||||
else if (n == "<")
|
||||
return m_context.mkExpr(CVC4::kind::LT, arguments[0], arguments[1]);
|
||||
else if (n == "<=")
|
||||
return m_context.mkExpr(CVC4::kind::LEQ, arguments[0], arguments[1]);
|
||||
else if (n == ">")
|
||||
return m_context.mkExpr(CVC4::kind::GT, arguments[0], arguments[1]);
|
||||
else if (n == ">=")
|
||||
return m_context.mkExpr(CVC4::kind::GEQ, arguments[0], arguments[1]);
|
||||
else if (n == "+")
|
||||
return m_context.mkExpr(CVC4::kind::PLUS, arguments[0], arguments[1]);
|
||||
else if (n == "-")
|
||||
return m_context.mkExpr(CVC4::kind::MINUS, arguments[0], arguments[1]);
|
||||
else if (n == "*")
|
||||
return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
|
||||
else if (n == "/")
|
||||
return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
|
||||
else if (n == "mod")
|
||||
return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]);
|
||||
else if (n == "select")
|
||||
return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]);
|
||||
else if (n == "store")
|
||||
return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]);
|
||||
|
||||
solAssert(false, "");
|
||||
}
|
||||
catch (CVC4::TypeCheckingException const& _e)
|
||||
{
|
||||
solAssert(false, _e.what());
|
||||
}
|
||||
catch (CVC4::Exception const& _e)
|
||||
{
|
||||
solAssert(false, _e.what());
|
||||
}
|
||||
|
||||
solAssert(_expr.hasCorrectArity(), "");
|
||||
if (n == "ite")
|
||||
return arguments[0].iteExpr(arguments[1], arguments[2]);
|
||||
else if (n == "not")
|
||||
return arguments[0].notExpr();
|
||||
else if (n == "and")
|
||||
return arguments[0].andExpr(arguments[1]);
|
||||
else if (n == "or")
|
||||
return arguments[0].orExpr(arguments[1]);
|
||||
else if (n == "implies")
|
||||
return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]);
|
||||
else if (n == "=")
|
||||
return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]);
|
||||
else if (n == "<")
|
||||
return m_context.mkExpr(CVC4::kind::LT, arguments[0], arguments[1]);
|
||||
else if (n == "<=")
|
||||
return m_context.mkExpr(CVC4::kind::LEQ, arguments[0], arguments[1]);
|
||||
else if (n == ">")
|
||||
return m_context.mkExpr(CVC4::kind::GT, arguments[0], arguments[1]);
|
||||
else if (n == ">=")
|
||||
return m_context.mkExpr(CVC4::kind::GEQ, arguments[0], arguments[1]);
|
||||
else if (n == "+")
|
||||
return m_context.mkExpr(CVC4::kind::PLUS, arguments[0], arguments[1]);
|
||||
else if (n == "-")
|
||||
return m_context.mkExpr(CVC4::kind::MINUS, arguments[0], arguments[1]);
|
||||
else if (n == "*")
|
||||
return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
|
||||
else if (n == "/")
|
||||
return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
|
||||
else if (n == "mod")
|
||||
return m_context.mkExpr(CVC4::kind::INTS_MODULUS, arguments[0], arguments[1]);
|
||||
else if (n == "select")
|
||||
return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]);
|
||||
else if (n == "store")
|
||||
return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]);
|
||||
// Cannot reach here.
|
||||
solAssert(false, "");
|
||||
return arguments[0];
|
||||
}
|
||||
|
||||
CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
|
||||
|
||||
@ -116,69 +116,77 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
|
||||
for (auto const& arg: _expr.arguments)
|
||||
arguments.push_back(toZ3Expr(arg));
|
||||
|
||||
string const& n = _expr.name;
|
||||
if (m_functions.count(n))
|
||||
return m_functions.at(n)(arguments);
|
||||
else if (m_constants.count(n))
|
||||
try
|
||||
{
|
||||
solAssert(arguments.empty(), "");
|
||||
return m_constants.at(n);
|
||||
string const& n = _expr.name;
|
||||
if (m_functions.count(n))
|
||||
return m_functions.at(n)(arguments);
|
||||
else if (m_constants.count(n))
|
||||
{
|
||||
solAssert(arguments.empty(), "");
|
||||
return m_constants.at(n);
|
||||
}
|
||||
else if (arguments.empty())
|
||||
{
|
||||
if (n == "true")
|
||||
return m_context.bool_val(true);
|
||||
else if (n == "false")
|
||||
return m_context.bool_val(false);
|
||||
else
|
||||
try
|
||||
{
|
||||
return m_context.int_val(n.c_str());
|
||||
}
|
||||
catch (z3::exception const& _e)
|
||||
{
|
||||
solAssert(false, _e.msg());
|
||||
}
|
||||
}
|
||||
|
||||
solAssert(_expr.hasCorrectArity(), "");
|
||||
if (n == "ite")
|
||||
return z3::ite(arguments[0], arguments[1], arguments[2]);
|
||||
else if (n == "not")
|
||||
return !arguments[0];
|
||||
else if (n == "and")
|
||||
return arguments[0] && arguments[1];
|
||||
else if (n == "or")
|
||||
return arguments[0] || arguments[1];
|
||||
else if (n == "implies")
|
||||
return z3::implies(arguments[0], arguments[1]);
|
||||
else if (n == "=")
|
||||
return arguments[0] == arguments[1];
|
||||
else if (n == "<")
|
||||
return arguments[0] < arguments[1];
|
||||
else if (n == "<=")
|
||||
return arguments[0] <= arguments[1];
|
||||
else if (n == ">")
|
||||
return arguments[0] > arguments[1];
|
||||
else if (n == ">=")
|
||||
return arguments[0] >= arguments[1];
|
||||
else if (n == "+")
|
||||
return arguments[0] + arguments[1];
|
||||
else if (n == "-")
|
||||
return arguments[0] - arguments[1];
|
||||
else if (n == "*")
|
||||
return arguments[0] * arguments[1];
|
||||
else if (n == "/")
|
||||
return arguments[0] / arguments[1];
|
||||
else if (n == "mod")
|
||||
return z3::mod(arguments[0], arguments[1]);
|
||||
else if (n == "select")
|
||||
return z3::select(arguments[0], arguments[1]);
|
||||
else if (n == "store")
|
||||
return z3::store(arguments[0], arguments[1], arguments[2]);
|
||||
|
||||
solAssert(false, "");
|
||||
}
|
||||
else if (arguments.empty())
|
||||
catch (z3::exception const& _e)
|
||||
{
|
||||
if (n == "true")
|
||||
return m_context.bool_val(true);
|
||||
else if (n == "false")
|
||||
return m_context.bool_val(false);
|
||||
else
|
||||
try
|
||||
{
|
||||
return m_context.int_val(n.c_str());
|
||||
}
|
||||
catch (...)
|
||||
{
|
||||
solAssert(false, "");
|
||||
}
|
||||
solAssert(false, _e.msg());
|
||||
}
|
||||
|
||||
solAssert(_expr.hasCorrectArity(), "");
|
||||
if (n == "ite")
|
||||
return z3::ite(arguments[0], arguments[1], arguments[2]);
|
||||
else if (n == "not")
|
||||
return !arguments[0];
|
||||
else if (n == "and")
|
||||
return arguments[0] && arguments[1];
|
||||
else if (n == "or")
|
||||
return arguments[0] || arguments[1];
|
||||
else if (n == "implies")
|
||||
return z3::implies(arguments[0], arguments[1]);
|
||||
else if (n == "=")
|
||||
return arguments[0] == arguments[1];
|
||||
else if (n == "<")
|
||||
return arguments[0] < arguments[1];
|
||||
else if (n == "<=")
|
||||
return arguments[0] <= arguments[1];
|
||||
else if (n == ">")
|
||||
return arguments[0] > arguments[1];
|
||||
else if (n == ">=")
|
||||
return arguments[0] >= arguments[1];
|
||||
else if (n == "+")
|
||||
return arguments[0] + arguments[1];
|
||||
else if (n == "-")
|
||||
return arguments[0] - arguments[1];
|
||||
else if (n == "*")
|
||||
return arguments[0] * arguments[1];
|
||||
else if (n == "/")
|
||||
return arguments[0] / arguments[1];
|
||||
else if (n == "mod")
|
||||
return z3::mod(arguments[0], arguments[1]);
|
||||
else if (n == "select")
|
||||
return z3::select(arguments[0], arguments[1]);
|
||||
else if (n == "store")
|
||||
return z3::store(arguments[0], arguments[1], arguments[2]);
|
||||
// Cannot reach here.
|
||||
solAssert(false, "");
|
||||
return arguments[0];
|
||||
}
|
||||
|
||||
z3::sort Z3Interface::z3Sort(Sort const& _sort)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user