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

Stronger checks

Browse Source
This commit is contained in:
Martin Blicha 2023-08-03 11:35:01 +02:00
parent 0c13b7ee8f
commit 01ed412714
1 changed files with 18 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -277,13 +277,19 @@ namespace
std::string const& asAtom(SMTLib2Expression const& expr) std::string const& asAtom(SMTLib2Expression const& expr)
{ {
assert(isAtom(expr)); solAssert(isAtom(expr));
return std::get<std::string>(expr.data); return std::get<std::string>(expr.data);
} }
auto const& asSubExpressions(SMTLib2Expression const& expr) auto const& asSubExpressions(SMTLib2Expression const& expr)
{ {
assert(!isAtom(expr)); solAssert(!isAtom(expr));
return std::get<SMTLib2Expression::args_t>(expr.data);
}
auto& asSubExpressions(SMTLib2Expression& expr)
{
solAssert(!isAtom(expr));
return std::get<SMTLib2Expression::args_t>(expr.data); return std::get<SMTLib2Expression::args_t>(expr.data);
} }
@ -496,12 +502,12 @@ namespace
void popScope() void popScope()
{ {
assert(scopeBounds.size() > 0); smtAssert(scopeBounds.size() > 0);
auto bound = scopeBounds.back(); auto bound = scopeBounds.back();
while (varNames.size() > bound) { while (varNames.size() > bound) {
auto const& varName = varNames.back(); auto const& varName = varNames.back();
auto it = bindings.find(varName); auto it = bindings.find(varName);
assert(it != bindings.end()); smtAssert(it != bindings.end());
auto & record = it->second; auto & record = it->second;
record.pop_back(); record.pop_back();
if (record.empty()) if (record.empty())
@ -526,28 +532,28 @@ namespace
{ {
if (isAtom(expr)) if (isAtom(expr))
{ {
auto const& atom = std::get<std::string>(expr.data); auto const& atom = asAtom(expr);
if (bindings.has(atom)) if (bindings.has(atom))
expr = bindings[atom]; expr = bindings[atom];
} }
else else
{ {
auto& subexprs = std::get<SMTLib2Expression::args_t>(expr.data); auto& subexprs = asSubExpressions(expr);
auto const& first = subexprs[0]; auto const& first = subexprs[0];
if (isAtom(first) && std::get<std::string>(first.data) == "let") if (isAtom(first) && asAtom(first) == "let")
{ {
solAssert(!isAtom(subexprs[1])); solAssert(!isAtom(subexprs[1]));
auto& bindingExpressions = std::get<SMTLib2Expression::args_t>(subexprs[1].data); auto& bindingExpressions = asSubExpressions(subexprs[1]);
// process new bindings // process new bindings
std::vector<std::pair<std::string, SMTLib2Expression>> newBindings; std::vector<std::pair<std::string, SMTLib2Expression>> newBindings;
for (auto& binding: bindingExpressions) for (auto& binding: bindingExpressions)
{ {
solAssert(!isAtom(binding)); solAssert(!isAtom(binding));
auto& bindingPair = std::get<SMTLib2Expression::args_t>(binding.data); auto& bindingPair = asSubExpressions(binding);
solAssert(bindingPair.size() == 2); solAssert(bindingPair.size() == 2);
solAssert(isAtom(bindingPair.at(0))); solAssert(isAtom(bindingPair.at(0)));
inlineLetExpressions(bindingPair.at(1), bindings); inlineLetExpressions(bindingPair.at(1), bindings);
newBindings.emplace_back(std::get<std::string>(bindingPair.at(0).data), bindingPair.at(1)); newBindings.emplace_back(asAtom(bindingPair.at(0)), bindingPair.at(1));
} }
bindings.pushScope(); bindings.pushScope();
for (auto&& [name, expr] : newBindings) for (auto&& [name, expr] : newBindings)
@ -582,6 +588,7 @@ namespace
{ {
if (isAtom(_node)) if (isAtom(_node))
return _node; return _node;
solAssert(!asSubExpressions(_node).empty());
return asSubExpressions(_node).back(); return asSubExpressions(_node).back();
} }
} }
@ -615,7 +622,7 @@ CHCSolverInterface::CexGraph CHCSmtLib2Interface::graphFromSMTLib2Expression(SMT
auto isHyperRes = [](SMTLib2Expression const& expr) { auto isHyperRes = [](SMTLib2Expression const& expr) {
if (isAtom(expr)) return false; if (isAtom(expr)) return false;
auto const& subExprs = asSubExpressions(expr); auto const& subExprs = asSubExpressions(expr);
assert(!subExprs.empty()); solAssert(!subExprs.empty());
auto const& op = subExprs.at(0); auto const& op = subExprs.at(0);
if (isAtom(op)) return false; if (isAtom(op)) return false;
auto const& opExprs = asSubExpressions(op); auto const& opExprs = asSubExpressions(op);