Add SMT type support to Solidity arrays

libsolidity/formal/SymbolicTypes.cpp

@@ -57,8 +57,13 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
 			solAssert(mapType, "");
 			return make_shared<smt::ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
 		}
-		// TODO Solidity array
+		else
-		return make_shared<smt::Sort>(smt::Kind::Int);
+		{
+			solAssert(isArray(_type.category()), "");
+			auto arrayType = dynamic_cast<ArrayType const*>(&_type);
+			solAssert(arrayType, "");
+			return make_shared<smt::ArraySort>(make_shared<smt::Sort>(smt::Kind::Int), smtSort(*arrayType->baseType()));
+		}
 	}
 	default:
 		// Abstract case.
@@ -82,7 +87,7 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
 		return smt::Kind::Bool;
 	else if (isFunction(_category))
 		return smt::Kind::Function;
-	else if (isMapping(_category))
+	else if (isMapping(_category) || isArray(_category))
 		return smt::Kind::Array;
 	// Abstract case.
 	return smt::Kind::Int;
@@ -92,7 +97,8 @@ bool dev::solidity::isSupportedType(Type::Category _category)
 {
 	return isNumber(_category) ||
 		isBool(_category) ||
-		isMapping(_category);
+		isMapping(_category) ||
+		isArray(_category);
 }
 
 bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category)
@@ -140,6 +146,8 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
 	}
 	else if (isMapping(_type.category()))
 		var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _solver);
+	else if (isArray(_type.category()))
+		var = make_shared<SymbolicArrayVariable>(type, _uniqueName, _solver);
 	else
 		solAssert(false, "");
 	return make_pair(abstract, var);
@@ -198,6 +206,11 @@ bool dev::solidity::isMapping(Type::Category _category)
 	return _category == Type::Category::Mapping;
 }
 
+bool dev::solidity::isArray(Type::Category _category)
+{
+	return _category == Type::Category::Array;
+}
+
 smt::Expression dev::solidity::minValue(IntegerType const& _type)
 {
 	return smt::Expression(_type.minValue());

libsolidity/formal/SymbolicTypes.h

@@ -48,6 +48,7 @@ bool isNumber(Type::Category _category);
 bool isBool(Type::Category _category);
 bool isFunction(Type::Category _category);
 bool isMapping(Type::Category _category);
+bool isArray(Type::Category _category);
 
 /// Returns a new symbolic variable, according to _type.
 /// Also returns whether the type is abstract or not,

libsolidity/formal/SymbolicVariables.cpp

@@ -136,3 +136,13 @@ SymbolicMappingVariable::SymbolicMappingVariable(
 {
 	solAssert(isMapping(m_type->category()), "");
 }
+
+SymbolicArrayVariable::SymbolicArrayVariable(
+	TypePointer _type,
+	string const& _uniqueName,
+	smt::SolverInterface& _interface
+):
+	SymbolicVariable(move(_type), _uniqueName, _interface)
+{
+	solAssert(isArray(m_type->category()), "");
+}

libsolidity/formal/SymbolicVariables.h

@@ -153,5 +153,18 @@ public:
 	);
 };
 
+/**
+ * Specialization of SymbolicVariable for Array
+ */
+class SymbolicArrayVariable: public SymbolicVariable
+{
+public:
+	SymbolicArrayVariable(
+		TypePointer _type,
+		std::string const& _uniqueName,
+		smt::SolverInterface& _interface
+	);
+};
+
 }
 }

test/libsolidity/smtCheckerTests/simple/static_array.sol

@@ -7,6 +7,3 @@ contract C
 	int[3*1] x;
 }
 // ----
-// Warning: (92-100): Assertion checker does not yet support the type of this variable.
-// Warning: (149-159): Assertion checker does not yet support the type of this variable.
-// Warning: (153-156): Assertion checker does not yet implement this operator on non-integer types.

test/libsolidity/smtCheckerTests/special/msg_data.sol

@@ -8,6 +8,5 @@ contract C
 }
 // ----
 // Warning: (86-101): Assertion checker does not yet support this expression.
-// Warning: (86-94): Assertion checker does not yet support this global variable.
 // Warning: (86-101): Internal error: Expression undefined for SMT solver.
 // Warning: (79-106): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/bytes_1.sol

@@ -9,8 +9,3 @@ contract C
 }
 // ----
 // Warning: (113-127): Unused local variable.
-// Warning: (113-127): Assertion checker does not yet support the type of this variable.
-// Warning: (58-72): Assertion checker does not yet support the type of this variable.
-// Warning: (95-107): Assertion checker does not yet support the type of this variable.
-// Warning: (130-131): Internal error: Expression undefined for SMT solver.
-// Warning: (130-131): Assertion checker does not yet implement this type.

test/libsolidity/smtCheckerTests/types/mapping_unsupported_key_type_1.sol

@@ -9,9 +9,3 @@ contract C
 	}
 }
 // ----
-// Warning: (89-104): Assertion checker does not yet support the type of this variable.
-// Warning: (129-130): Internal error: Expression undefined for SMT solver.
-// Warning: (129-130): Assertion checker does not yet implement this type.
-// Warning: (155-156): Internal error: Expression undefined for SMT solver.
-// Warning: (155-156): Assertion checker does not yet implement this type.
-// Warning: (139-158): Assertion violation happens here