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 #10510 from blishko/struct_in_cex

Browse Source 
[SMTChecker] Adding support for reporting values of structs in CEX in CHC engine
This commit is contained in:
Leonardo 2020-12-08 18:09:31 +01:00 committed by GitHub
commit e78ca14368
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 33 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -12,6 +12,7 @@ Compiler Features:
* SMTChecker: Support struct constructor. * SMTChecker: Support struct constructor.
* SMTChecker: Support getters. * SMTChecker: Support getters.
* SMTChecker: Support early returns in the CHC engine. * SMTChecker: Support early returns in the CHC engine.
* SMTChecker: Report struct values in counterexamples from CHC engine.
* Standard-Json: Properly filter the requested output artifacts. * Standard-Json: Properly filter the requested output artifacts.
Bugfixes: Bugfixes:

33
libsolidity/formal/Predicate.cpp
View File

@ -302,7 +302,15 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort); auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort);
solAssert(tupleSort.components.size() == 2, ""); solAssert(tupleSort.components.size() == 2, "");
auto length = stoul(_expr.arguments.at(1).name); unsigned long length;
try
{
length = stoul(_expr.arguments.at(1).name);
}
catch(out_of_range const&)
{
return {};
}
// Limit this counterexample size to 1k. // Limit this counterexample size to 1k.
// Some OSs give you "unlimited" memory through swap and other virtual memory, // Some OSs give you "unlimited" memory through swap and other virtual memory,
// so purely relying on bad_alloc being thrown is not a good idea. // so purely relying on bad_alloc being thrown is not a good idea.
@ -321,6 +329,22 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
// Solver gave a concrete array but length is too large. // Solver gave a concrete array but length is too large.
} }
} }
if (smt::isNonRecursiveStruct(*_type))
{
auto const& structType = dynamic_cast<StructType const&>(*_type);
solAssert(_expr.name == "tuple_constructor", "");
auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort);
auto members = structType.structDefinition().members();
solAssert(tupleSort.components.size() == members.size(), "");
solAssert(_expr.arguments.size() == members.size(), "");
vector<string> elements;
for (unsigned i = 0; i < members.size(); ++i)
{
optional<string> elementStr = expressionToString(_expr.arguments.at(i), members[i]->type());
elements.push_back(members[i]->name() + (elementStr.has_value() ? ": " + elementStr.value() : ""));
}
return "{" + boost::algorithm::join(elements, ", ") + "}";
}
return {}; return {};
} }
@ -366,5 +390,12 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
return true; return true;
} }
// Special base case, not supported yet.
if (_expr.name.rfind("(_ as-array") == 0)
{
// Z3 expression representing reinterpretation of a different term as an array
return false;
}
solAssert(false, ""); solAssert(false, "");
} }