cerc-io/solidity
15
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 #5478 from ethereum/smt_refactor_sort_patch3

Browse Source 
[SMTChecker] Add ArraySort and array operations
This commit is contained in:
Alex Beregszaszi 2018-11-22 13:10:35 +00:00 committed by GitHub
commit a5411965e6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 76 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
libsolidity/formal/CVC4Interface.cpp
View File

@ -164,6 +164,10 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
else if (n == "/")
return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
else if (n == "select")
return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]);
else if (n == "store")
return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]);
// Cannot reach here.
solAssert(false, "");
return arguments[0];
@ -182,6 +186,11 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);
return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain));
}
case Kind::Array:
{
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range));
}
default:
break;
}

5
libsolidity/formal/SMTLib2Interface.cpp
View File

@ -144,6 +144,11 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
return "Int";
case Kind::Bool:
return "Bool";
case Kind::Array:
{
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
}
default:
solAssert(false, "Invalid SMT sort");
}

51
libsolidity/formal/SolverInterface.h
View File

@ -46,7 +46,8 @@ enum class Kind
{
Int,
Bool,
Function
Function,
Array
};
struct Sort
@ -79,6 +80,20 @@ struct FunctionSort: public Sort
}
};
struct ArraySort: public Sort
{
/// _domain is the sort of the indices
/// _range is the sort of the values
ArraySort(SortPointer _domain, SortPointer _range):
Sort(Kind::Array), domain(std::move(_domain)), range(std::move(_range)) {}
SortPointer domain;
SortPointer range;
bool operator==(ArraySort const& _other) const
{
return Sort::operator==(_other) && *domain == *_other.domain && *range == *_other.range;
}
};
/// C++ representation of an SMTLIB2 expression.
class Expression
{
@ -109,7 +124,9 @@ public:
{"+", 2},
{"-", 2},
{"*", 2},
{"/", 2}
{"/", 2},
{"select", 2},
{"store", 3}
};
return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size();
}
@ -127,6 +144,36 @@ public:
return !std::move(_a) || std::move(_b);
}
/// select is the SMT representation of an array index access.
static Expression select(Expression _array, Expression _index)
{
solAssert(_array.sort->kind == Kind::Array, "");
auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
solAssert(arraySort, "");
solAssert(*arraySort->domain == *_index.sort, "");
return Expression(
"select",
std::vector<Expression>{std::move(_array), std::move(_index)},
arraySort->range
);
}
/// store is the SMT representation of an assignment to array index.
/// The function is pure and returns the modified array.
static Expression store(Expression _array, Expression _index, Expression _element)
{
solAssert(_array.sort->kind == Kind::Array, "");
auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
solAssert(arraySort, "");
solAssert(*arraySort->domain == *_index.sort, "");
solAssert(*arraySort->range == *_element.sort, "");
return Expression(
"store",
std::vector<Expression>{std::move(_array), std::move(_index), std::move(_element)},
_array.sort
);
}
friend Expression operator!(Expression _a)
{
return Expression("not", std::move(_a), Kind::Bool);

4
libsolidity/formal/SymbolicTypes.cpp
View File

@ -43,6 +43,10 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
smt::SortPointer returnSort = smtSort(*returnTypes.at(0));
return make_shared<smt::FunctionSort>(parameterSorts, returnSort);
}
case smt::Kind::Array:
{
solUnimplementedAssert(false, "Invalid type");
}
}
solAssert(false, "Invalid type");
}

9
libsolidity/formal/Z3Interface.cpp
View File

@ -163,6 +163,10 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return arguments[0] * arguments[1];
else if (n == "/")
return arguments[0] / arguments[1];
else if (n == "select")
return z3::select(arguments[0], arguments[1]);
else if (n == "store")
return z3::store(arguments[0], arguments[1], arguments[2]);
// Cannot reach here.
solAssert(false, "");
return arguments[0];
@ -176,6 +180,11 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
return m_context.bool_sort();
case Kind::Int:
return m_context.int_sort();
case Kind::Array:
{
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
return m_context.array_sort(z3Sort(*arraySort.domain), z3Sort(*arraySort.range));
}
default:
break;
}