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

Hack to get around problem in Z3

Browse Source
This commit is contained in:
Martin Blicha 2023-08-11 12:44:34 +02:00
parent 8c99c125c4
commit 3a01b432c4
1 changed files with 18 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
libsolidity/formal/SymbolicTypes.cpp
View File

@ -23,12 +23,24 @@
#include <libsolidity/ast/TypeProvider.h> #include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/ast/Types.h> #include <libsolidity/ast/Types.h>
#include <libsolutil/CommonData.h> #include <libsolutil/CommonData.h>
#include <algorithm>
#include <memory> #include <memory>
#include <vector> #include <vector>
using namespace solidity::util; using namespace solidity::util;
using namespace solidity::smtutil; using namespace solidity::smtutil;
namespace
{
// HACK to get around Z3 bug in printing type names with spaces (https://github.com/Z3Prover/z3/issues/6850)
void sanitizeTypeName(std::string& name)
{
std::replace(name.begin(), name.end(), ' ', '_');
std::replace(name.begin(), name.end(), '(', '[');
std::replace(name.begin(), name.end(), ')', ']');
}
}
namespace solidity::frontend::smt namespace solidity::frontend::smt
{ {
@ -118,13 +130,16 @@ SortPointer smtSort(frontend::Type const& _type)
else if (baseType->category() == frontend::Type::Category::FixedBytes) else if (baseType->category() == frontend::Type::Category::FixedBytes)
tupleName = "fixedbytes"; tupleName = "fixedbytes";
else else
{
tupleName = arrayType->baseType()->toString(true); tupleName = arrayType->baseType()->toString(true);
}
tupleName += "_array"; tupleName += "_array";
} }
else else
tupleName = _type.toString(true); tupleName = _type.toString(true);
sanitizeTypeName(tupleName);
tupleName += "_tuple"; tupleName += "_tuple";
return std::make_shared<TupleSort>( return std::make_shared<TupleSort>(
@ -136,7 +151,9 @@ SortPointer smtSort(frontend::Type const& _type)
case Kind::Tuple: case Kind::Tuple:
{ {
std::vector<std::string> members; std::vector<std::string> members;
auto const& tupleName = _type.toString(true); auto tupleName = _type.toString(true);
sanitizeTypeName(tupleName);
std::vector<SortPointer> sorts; std::vector<SortPointer> sorts;
if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type)) if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type))