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

Use shared pointers, not raw pointers, for caching sorts

Browse Source
This commit is contained in:
Martin Blicha 2023-07-27 12:05:43 +02:00
parent b65c37029d
commit 779db2d84f
4 changed files with 20 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -128,11 +128,11 @@ void CHCSmtLib2Interface::declareVariable(std::string const& _name, SortPointer
else if (!m_variables.count(_name)) else if (!m_variables.count(_name))
{ {
m_variables.insert(_name); m_variables.insert(_name);
write("(declare-var |" + _name + "| " + toSmtLibSort(*_sort) + ')'); write("(declare-var |" + _name + "| " + toSmtLibSort(_sort) + ')');
} }
} }
std::string CHCSmtLib2Interface::toSmtLibSort(Sort const& _sort) std::string CHCSmtLib2Interface::toSmtLibSort(SortPointer _sort)
{ {
return m_smtlib2->toSmtLibSort(_sort); return m_smtlib2->toSmtLibSort(_sort);
} }
@ -149,7 +149,7 @@ std::string CHCSmtLib2Interface::forall()
{ {
solAssert(sort, ""); solAssert(sort, "");
if (sort->kind != Kind::Function) if (sort->kind != Kind::Function)
vars += " (" + name + " " + toSmtLibSort(*sort) + ")"; vars += " (" + name + " " + toSmtLibSort(sort) + ")";
} }
vars += ")"; vars += ")";
return vars; return vars;
@ -165,7 +165,7 @@ void CHCSmtLib2Interface::declareFunction(std::string const& _name, SortPointer
auto fSort = std::dynamic_pointer_cast<FunctionSort>(_sort); auto fSort = std::dynamic_pointer_cast<FunctionSort>(_sort);
smtAssert(fSort->codomain); smtAssert(fSort->codomain);
std::string domain = toSmtLibSort(fSort->domain); std::string domain = toSmtLibSort(fSort->domain);
std::string codomain = toSmtLibSort(*fSort->codomain); std::string codomain = toSmtLibSort(fSort->codomain);
m_variables.insert(_name); m_variables.insert(_name);
write( write(
"(declare-fun |" + "(declare-fun |" +
@ -309,10 +309,9 @@ namespace
}); });
if (it != m_smtlib2Interface.sortNames().end()) { if (it != m_smtlib2Interface.sortNames().end()) {
if (it->first->kind == Kind::Tuple) { if (it->first->kind == Kind::Tuple) {
auto const* tupleSort = dynamic_cast<TupleSort const*>(it->first); auto tupleSort = std::dynamic_pointer_cast<TupleSort>(it->first);
smtAssert(tupleSort); smtAssert(tupleSort);
// TODO: This is cumbersome, we should really store shared_pointer instead of raw pointer in the sortNames return tupleSort;
return std::make_shared<TupleSort>(tupleSort->name, tupleSort->members, tupleSort->components);
} }
} }
} else { } else {

2
libsmtutil/CHCSmtLib2Interface.h
View File

@ -66,7 +66,7 @@ public:
SMTLib2Interface* smtlib2Interface() const { return m_smtlib2.get(); } SMTLib2Interface* smtlib2Interface() const { return m_smtlib2.get(); }
private: private:
std::string toSmtLibSort(Sort const& _sort); std::string toSmtLibSort(SortPointer _sort);
std::string toSmtLibSort(std::vector<SortPointer> const& _sort); std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
void writeHeader(); void writeHeader();

22
libsmtutil/SMTLib2Interface.cpp
View File

@ -83,7 +83,7 @@ void SMTLib2Interface::declareVariable(std::string const& _name, SortPointer con
else if (!m_variables.count(_name)) else if (!m_variables.count(_name))
{ {
m_variables.emplace(_name, _sort); m_variables.emplace(_name, _sort);
write("(declare-fun |" + _name + "| () " + toSmtLibSort(*_sort) + ')'); write("(declare-fun |" + _name + "| () " + toSmtLibSort(_sort) + ')');
} }
} }
@ -96,7 +96,7 @@ void SMTLib2Interface::declareFunction(std::string const& _name, SortPointer con
{ {
auto const& fSort = std::dynamic_pointer_cast<FunctionSort>(_sort); auto const& fSort = std::dynamic_pointer_cast<FunctionSort>(_sort);
std::string domain = toSmtLibSort(fSort->domain); std::string domain = toSmtLibSort(fSort->domain);
std::string codomain = toSmtLibSort(*fSort->codomain); std::string codomain = toSmtLibSort(fSort->codomain);
m_variables.emplace(_name, _sort); m_variables.emplace(_name, _sort);
write( write(
"(declare-fun |" + "(declare-fun |" +
@ -246,7 +246,7 @@ std::string SMTLib2Interface::toSExpr(Expression const& _expr)
smtAssert(sortSort, ""); smtAssert(sortSort, "");
auto arraySort = std::dynamic_pointer_cast<ArraySort>(sortSort->inner); auto arraySort = std::dynamic_pointer_cast<ArraySort>(sortSort->inner);
smtAssert(arraySort, ""); smtAssert(arraySort, "");
sexpr += "(as const " + toSmtLibSort(*arraySort) + ") "; sexpr += "(as const " + toSmtLibSort(arraySort) + ") ";
sexpr += toSExpr(_expr.arguments.at(1)); sexpr += toSExpr(_expr.arguments.at(1));
} }
else if (_expr.name == "tuple_get") else if (_expr.name == "tuple_get")
@ -275,14 +275,14 @@ std::string SMTLib2Interface::toSExpr(Expression const& _expr)
return sexpr; return sexpr;
} }
std::string SMTLib2Interface::toSmtLibSort(Sort const& _sort) std::string SMTLib2Interface::toSmtLibSort(SortPointer _sort)
{ {
if (!m_sortNames.count(&_sort)) if (!m_sortNames.count(_sort))
{ {
auto smtLibName = sortToString(_sort); auto smtLibName = sortToString(*_sort);
m_sortNames[&_sort] = smtLibName; m_sortNames[_sort] = smtLibName;
} }
return m_sortNames.at(&_sort); return m_sortNames.at(_sort);
} }
std::string SMTLib2Interface::sortToString(Sort const& _sort) std::string SMTLib2Interface::sortToString(Sort const& _sort)
@ -299,7 +299,7 @@ std::string SMTLib2Interface::sortToString(Sort const& _sort)
{ {
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort); auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
smtAssert(arraySort.domain && arraySort.range, ""); smtAssert(arraySort.domain && arraySort.range, "");
return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')'; return "(Array " + toSmtLibSort(arraySort.domain) + ' ' + toSmtLibSort(arraySort.range) + ')';
} }
case Kind::Tuple: case Kind::Tuple:
{ {
@ -311,7 +311,7 @@ std::string SMTLib2Interface::sortToString(Sort const& _sort)
std::string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName); std::string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName);
smtAssert(tupleSort.members.size() == tupleSort.components.size(), ""); smtAssert(tupleSort.members.size() == tupleSort.components.size(), "");
for (unsigned i = 0; i < tupleSort.members.size(); ++i) for (unsigned i = 0; i < tupleSort.members.size(); ++i)
decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")"; decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(tupleSort.components.at(i)) + ")";
decl += "))))"; decl += "))))";
m_userSorts.emplace_back(tupleName, decl); m_userSorts.emplace_back(tupleName, decl);
write(decl); write(decl);
@ -328,7 +328,7 @@ std::string SMTLib2Interface::toSmtLibSort(std::vector<SortPointer> const& _sort
{ {
std::string ssort("("); std::string ssort("(");
for (auto const& sort: _sorts) for (auto const& sort: _sorts)
ssort += toSmtLibSort(*sort) + " "; ssort += toSmtLibSort(sort) + " ";
ssort += ")"; ssort += ")";
return ssort; return ssort;
} }

5
libsmtutil/SMTLib2Interface.h
View File

@ -62,7 +62,7 @@ public:
// Used by CHCSmtLib2Interface // Used by CHCSmtLib2Interface
std::string toSExpr(Expression const& _expr); std::string toSExpr(Expression const& _expr);
std::string toSmtLibSort(Sort const& _sort); std::string toSmtLibSort(SortPointer _sort);
std::string toSmtLibSort(std::vector<SortPointer> const& _sort); std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
std::map<std::string, SortPointer> variables() { return m_variables; } std::map<std::string, SortPointer> variables() { return m_variables; }
@ -90,9 +90,8 @@ private:
/// It needs to be a vector so that the declaration order is kept, /// It needs to be a vector so that the declaration order is kept,
/// otherwise solvers cannot parse the queries. /// otherwise solvers cannot parse the queries.
std::vector<std::pair<std::string, std::string>> m_userSorts; std::vector<std::pair<std::string, std::string>> m_userSorts;
// TODO: Should this remember shared_pointer?
// TODO: Shouldn't sorts be unique objects? // TODO: Shouldn't sorts be unique objects?
std::map<Sort const*, std::string> m_sortNames; std::map<SortPointer, std::string> m_sortNames;
std::vector<std::string> m_unhandledQueries; std::vector<std::string> m_unhandledQueries;