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

Counterexamples from Eldarica

Browse Source
This commit is contained in:
Leo Alt
2022-05-15 17:43:12 +02:00
parent a3bd01d9fc
commit 3d21f1e4c3
7 changed files with 276 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/Predicate.cpp
+4 -1
View File
@@ -34,6 +34,7 @@
using namespace std;
using boost::algorithm::starts_with;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::smtutil;
using namespace solidity::frontend;
using namespace solidity::frontend::smt;
@@ -496,7 +497,8 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
if (_expr.name == "0")
return "0x0";
// For some reason the code below returns "0x" for "0".
return util::toHex(toCompactBigEndian(bigint(_expr.name)), util::HexPrefix::Add, util::HexCase::Lower);
return toHex(toCompactBigEndian(bigint(_expr.name)), HexPrefix::Add, HexCase::Lower);
//return formatNumberReadable(bigint(_expr.name));
}
catch (out_of_range const&)
{
@@ -506,6 +508,7 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
}
}
//return formatNumberReadable(bigint(_expr.name));
return _expr.name;
}
if (smt::isBool(*_type))
libsolidity/formal/SMTEncoder.cpp
+2 -1
View File
@@ -1063,7 +1063,8 @@ bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const
return false;
return m_settings.contracts.isDefault() ||
m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());
//m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());
m_settings.contracts.has(_contract.sourceUnitName());
}
void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
libsolidity/formal/SymbolicState.cpp
+9
View File
@@ -289,6 +289,15 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFuncti
for (auto paramType: inTypes + outTypes)
name += "_" + paramType->richIdentifier();
while (name.find(" => ") != string::npos)
name.replace(name.find(" => "), 4, "");
while (name.find('(') != string::npos)
name.replace(name.find('('), 1, "$");
while (name.find(')') != string::npos)
name.replace(name.find(')'), 1, "$");
while (name.find(',') != string::npos)
name.replace(name.find(','), 1, "$");
m_abiMembers[funCall] = {name, inTypes, outTypes};
if (functions.count(name))
libsolidity/formal/SymbolicTypes.cpp
+19 -1
View File
@@ -123,6 +123,15 @@ SortPointer smtSort(frontend::Type const& _type)
else
tupleName = _type.toString(true);
while (tupleName.find(" => ") != string::npos)
tupleName.replace(tupleName.find(" => "), 4, "");
while (tupleName.find('(') != string::npos)
tupleName.replace(tupleName.find('('), 1, "$");
while (tupleName.find(')') != string::npos)
tupleName.replace(tupleName.find(')'), 1, "$");
while (tupleName.find(',') != string::npos)
tupleName.replace(tupleName.find(','), 1, "$");
tupleName += "_tuple";
return make_shared<TupleSort>(
@@ -134,9 +143,18 @@ SortPointer smtSort(frontend::Type const& _type)
case Kind::Tuple:
{
vector<string> members;
auto const& tupleName = _type.toString(true);
string tupleName = _type.toString(true);
vector<SortPointer> sorts;
while (tupleName.find(" => ") != string::npos)
tupleName.replace(tupleName.find(" => "), 4, "");
while (tupleName.find('(') != string::npos)
tupleName.replace(tupleName.find('('), 1, "$");
while (tupleName.find(')') != string::npos)
tupleName.replace(tupleName.find(')'), 1, "$");
while (tupleName.find(',') != string::npos)
tupleName.replace(tupleName.find(','), 1, "$");
if (auto const* tupleType = dynamic_cast<frontend::TupleType const*>(&_type))
{
auto const& components = tupleType->components();