cerc-io/solidity
11
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

Fix CHC cex order

Browse Source
This commit is contained in:
Leonardo Alt
2021-03-11 10:36:40 +01:00
parent ec1c89d798
commit 6fd76e830d
19 changed files with 64 additions and 38 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/CHC.cpp
+28 -4
View File
@@ -38,6 +38,7 @@
#include <z3_version.h>
#endif
#include <charconv>
#include <queue>
using namespace std;
@@ -949,8 +950,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
{
string suffix = contract->name() + "_" + to_string(contract->id());
m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + suffix, PredicateType::Interface, contract);
m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract);
m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + uniquePrefix() + "_" + suffix, PredicateType::Interface, contract);
m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + uniquePrefix() + "_" + suffix, PredicateType::NondetInterface, contract);
m_constructorSummaries[contract] = createConstructorBlock(*contract, "summary_constructor");
m_contractInitializers[contract] = createConstructorBlock(*contract, "contract_initializer");
@@ -1104,7 +1105,7 @@ Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract
{
return createSymbolicBlock(
constructorSort(_contract, state()),
_prefix + "_" + contractSuffix(_contract) + "_" + uniquePrefix(),
_prefix + "_" + uniquePrefix() + "_" + contractSuffix(_contract),
PredicateType::ConstructorSummary,
&_contract,
&_contract
@@ -1622,7 +1623,30 @@ map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph c
map<unsigned, vector<unsigned>> calls;
auto compare = [&](unsigned _a, unsigned _b) {
return _graph.nodes.at(_a).name > _graph.nodes.at(_b).name;
auto extract = [&](string const& _s) {
// We want to sort sibling predicates in the counterexample graph by their unique predicate id.
// For most predicates, this actually doesn't matter.
// The cases where this matters are internal and external function calls which have the form:
// summary_<CALLID>_<suffix>
// nondet_call_<CALLID>_<suffix>
// Those have the extra unique <CALLID> numbers based on the traversal order, and are necessary
// to infer the call order so that's shown property in the counterexample trace.
// Predicates that do not have a CALLID have a predicate id at the end of <suffix>,
// so the assertion below should still hold.
auto beg = _s.data();
while (beg != _s.data() + _s.size() && !isdigit(*beg)) ++beg;
auto end = beg;
while (end != _s.data() + _s.size() && isdigit(*end)) ++end;
solAssert(beg != end, "Expected to find numerical call or predicate id.");
int result;
auto [p, ec] = std::from_chars(beg, end, result);
solAssert(ec == std::errc(), "Id should be a number.");
return result;
};
return extract(_graph.nodes.at(_a).name) > extract(_graph.nodes.at(_b).name);
};
queue<pair<unsigned, unsigned>> q;