aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorAlex Beregszaszi <alex@rtfs.hu>2018-11-22 21:10:35 +0800
committerGitHub <noreply@github.com>2018-11-22 21:10:35 +0800
commita5411965e6d7abf50f896291d69cab820db6ef87 (patch)
tree227e40834ef555f0f351b54c29564ff9a383785d /libsolidity
parent60fbc32fdfa4657edd3ebb047b7f65626ac3baba (diff)
parent20accf1a90e6b3dd077c67e6d31d1c56fedad5f5 (diff)
downloaddexon-solidity-a5411965e6d7abf50f896291d69cab820db6ef87.tar.gz
dexon-solidity-a5411965e6d7abf50f896291d69cab820db6ef87.tar.zst
dexon-solidity-a5411965e6d7abf50f896291d69cab820db6ef87.zip
Merge pull request #5478 from ethereum/smt_refactor_sort_patch3
[SMTChecker] Add ArraySort and array operations
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/CVC4Interface.cpp9
-rw-r--r--libsolidity/formal/SMTLib2Interface.cpp5
-rw-r--r--libsolidity/formal/SolverInterface.h51
-rw-r--r--libsolidity/formal/SymbolicTypes.cpp4
-rw-r--r--libsolidity/formal/Z3Interface.cpp9
5 files changed, 76 insertions, 2 deletions
diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index cff1717f..de5e4430 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -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;
}
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index bb85860f..55c72cfc 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -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");
}
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 551ef8e9..17e6904c 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -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);
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 2d0107c5..a12ab142 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -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");
}
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 162b0c23..cb01dc61 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -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;
}