mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
[SMTChecker] Add ArraySort and array operations
This commit is contained in:
parent
60fbc32fdf
commit
20accf1a90
@ -164,6 +164,10 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
|
|||||||
return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
|
return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
|
||||||
else if (n == "/")
|
else if (n == "/")
|
||||||
return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
|
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.
|
// Cannot reach here.
|
||||||
solAssert(false, "");
|
solAssert(false, "");
|
||||||
return arguments[0];
|
return arguments[0];
|
||||||
@ -182,6 +186,11 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
|
|||||||
FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);
|
FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);
|
||||||
return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain));
|
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:
|
default:
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
@ -144,6 +144,11 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
|
|||||||
return "Int";
|
return "Int";
|
||||||
case Kind::Bool:
|
case Kind::Bool:
|
||||||
return "Bool";
|
return "Bool";
|
||||||
|
case Kind::Array:
|
||||||
|
{
|
||||||
|
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
|
||||||
|
return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
|
||||||
|
}
|
||||||
default:
|
default:
|
||||||
solAssert(false, "Invalid SMT sort");
|
solAssert(false, "Invalid SMT sort");
|
||||||
}
|
}
|
||||||
|
@ -46,7 +46,8 @@ enum class Kind
|
|||||||
{
|
{
|
||||||
Int,
|
Int,
|
||||||
Bool,
|
Bool,
|
||||||
Function
|
Function,
|
||||||
|
Array
|
||||||
};
|
};
|
||||||
|
|
||||||
struct Sort
|
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.
|
/// C++ representation of an SMTLIB2 expression.
|
||||||
class Expression
|
class Expression
|
||||||
{
|
{
|
||||||
@ -109,7 +124,9 @@ public:
|
|||||||
{"+", 2},
|
{"+", 2},
|
||||||
{"-", 2},
|
{"-", 2},
|
||||||
{"*", 2},
|
{"*", 2},
|
||||||
{"/", 2}
|
{"/", 2},
|
||||||
|
{"select", 2},
|
||||||
|
{"store", 3}
|
||||||
};
|
};
|
||||||
return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size();
|
return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size();
|
||||||
}
|
}
|
||||||
@ -127,6 +144,36 @@ public:
|
|||||||
return !std::move(_a) || std::move(_b);
|
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)
|
friend Expression operator!(Expression _a)
|
||||||
{
|
{
|
||||||
return Expression("not", std::move(_a), Kind::Bool);
|
return Expression("not", std::move(_a), Kind::Bool);
|
||||||
|
@ -43,6 +43,10 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
|
|||||||
smt::SortPointer returnSort = smtSort(*returnTypes.at(0));
|
smt::SortPointer returnSort = smtSort(*returnTypes.at(0));
|
||||||
return make_shared<smt::FunctionSort>(parameterSorts, returnSort);
|
return make_shared<smt::FunctionSort>(parameterSorts, returnSort);
|
||||||
}
|
}
|
||||||
|
case smt::Kind::Array:
|
||||||
|
{
|
||||||
|
solUnimplementedAssert(false, "Invalid type");
|
||||||
|
}
|
||||||
}
|
}
|
||||||
solAssert(false, "Invalid type");
|
solAssert(false, "Invalid type");
|
||||||
}
|
}
|
||||||
|
@ -163,6 +163,10 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
|
|||||||
return arguments[0] * arguments[1];
|
return arguments[0] * arguments[1];
|
||||||
else if (n == "/")
|
else if (n == "/")
|
||||||
return arguments[0] / arguments[1];
|
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.
|
// Cannot reach here.
|
||||||
solAssert(false, "");
|
solAssert(false, "");
|
||||||
return arguments[0];
|
return arguments[0];
|
||||||
@ -176,6 +180,11 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
|
|||||||
return m_context.bool_sort();
|
return m_context.bool_sort();
|
||||||
case Kind::Int:
|
case Kind::Int:
|
||||||
return m_context.int_sort();
|
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:
|
default:
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user