Replace TypePointer with Type const*

libsolidity/formal/BMC.cpp

@@ -569,7 +569,7 @@ pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
 	Token _op,
 	smtutil::Expression const& _left,
 	smtutil::Expression const& _right,
-	TypePointer const& _commonType,
+	Type const* _commonType,
 	Expression const& _expression
 )
 {

libsolidity/formal/BMC.h

@@ -119,7 +119,7 @@ private:
 		Token _op,
 		smtutil::Expression const& _left,
 		smtutil::Expression const& _right,
-		TypePointer const& _commonType,
+		Type const* _commonType,
 		Expression const& _expression
 	) override;
 

libsolidity/formal/CHC.cpp

@@ -787,7 +787,7 @@ pair<smtutil::Expression, smtutil::Expression> CHC::arithmeticOperation(
 	Token _op,
 	smtutil::Expression const& _left,
 	smtutil::Expression const& _right,
-	TypePointer const& _commonType,
+	Type const* _commonType,
 	frontend::Expression const& _expression
 )
 {

libsolidity/formal/CHC.h

@@ -102,7 +102,7 @@ private:
 		Token _op,
 		smtutil::Expression const& _left,
 		smtutil::Expression const& _right,
-		TypePointer const& _commonType,
+		Type const* _commonType,
 		Expression const& _expression
 	) override;
 	//@}

libsolidity/formal/Predicate.cpp

@@ -308,7 +308,7 @@ vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expr
 	return formatExpressions(outValues, outTypes);
 }
 
-vector<optional<string>> Predicate::formatExpressions(vector<smtutil::Expression> const& _exprs, vector<TypePointer> const& _types) const
+vector<optional<string>> Predicate::formatExpressions(vector<smtutil::Expression> const& _exprs, vector<Type const*> const& _types) const
 {
 	solAssert(_exprs.size() == _types.size(), "");
 	vector<optional<string>> strExprs;
@@ -317,7 +317,7 @@ vector<optional<string>> Predicate::formatExpressions(vector<smtutil::Expression
 	return strExprs;
 }
 
-optional<string> Predicate::expressionToString(smtutil::Expression const& _expr, TypePointer _type) const
+optional<string> Predicate::expressionToString(smtutil::Expression const& _expr, Type const* _type) const
 {
 	if (smt::isNumber(*_type))
 	{
@@ -456,7 +456,7 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
 
 map<string, optional<string>> Predicate::readTxVars(smtutil::Expression const& _tx) const
 {
-	map<string, TypePointer> const txVars{
+	map<string, Type const*> const txVars{
 		{"block.chainid", TypeProvider::uint256()},
 		{"block.coinbase", TypeProvider::address()},
 		{"block.difficulty", TypeProvider::uint256()},

libsolidity/formal/Predicate.h

@@ -145,10 +145,10 @@ public:
 
 private:
 	/// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants.
-	std::vector<std::optional<std::string>> formatExpressions(std::vector<smtutil::Expression> const& _exprs, std::vector<TypePointer> const& _types) const;
+	std::vector<std::optional<std::string>> formatExpressions(std::vector<smtutil::Expression> const& _exprs, std::vector<Type const*> const& _types) const;
 
 	/// @returns a string representation of the SMT expression based on a Solidity type.
-	std::optional<std::string> expressionToString(smtutil::Expression const& _expr, TypePointer _type) const;
+	std::optional<std::string> expressionToString(smtutil::Expression const& _expr, Type const* _type) const;
 
 	/// Recursively fills _array from _expr.
 	/// _expr should have the form `store(store(...(const_array(x_0), i_0, e_0), i_m, e_m), i_k, e_k)`.

libsolidity/formal/SMTEncoder.cpp

@@ -978,7 +978,7 @@ void SMTEncoder::endVisit(ElementaryTypeNameExpression const& _typeName)
 namespace // helpers for SMTEncoder::visitPublicGetter
 {
 
-bool isReturnedFromStructGetter(TypePointer _type)
+bool isReturnedFromStructGetter(Type const* _type)
 {
 	// So far it seems that only Mappings and ordinary Arrays are not returned.
 	auto category = _type->category();
@@ -1016,7 +1016,7 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
 
 	// See FunctionType::FunctionType(VariableDeclaration const& _varDecl)
 	// to understand the return types of public getters.
-	TypePointer type = var->type();
+	Type const* type = var->type();
 	smtutil::Expression currentExpr = currentValue(*var);
 	while (true)
 	{
@@ -1450,7 +1450,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 
 	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
 	solAssert(arrayVar, "");
-	TypePointer baseType = _indexAccess.baseExpression().annotation().type;
+	Type const* baseType = _indexAccess.baseExpression().annotation().type;
 	defineExpr(_indexAccess, smtutil::Expression::select(
 		arrayVar->elements(),
 		expr(*_indexAccess.indexExpression(), keyType(baseType))
@@ -1486,7 +1486,7 @@ void SMTEncoder::indexOrMemberAssignment(Expression const& _expr, smtutil::Expre
 			if (dynamic_cast<Identifier const*>(&base))
 				base.accept(*this);
 
-			TypePointer baseType = base.annotation().type;
+			Type const* baseType = base.annotation().type;
 			auto indexExpr = expr(*indexAccess->indexExpression(), keyType(baseType));
 			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(base));
 			solAssert(symbArray, "");
@@ -1735,7 +1735,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	Token _op,
 	smtutil::Expression const& _left,
 	smtutil::Expression const& _right,
-	TypePointer const& _commonType,
+	Type const* _commonType,
 	Expression const& _operation
 )
 {
@@ -1826,7 +1826,7 @@ smtutil::Expression SMTEncoder::bitwiseOperation(
 	Token _op,
 	smtutil::Expression const& _left,
 	smtutil::Expression const& _right,
-	TypePointer const& _commonType
+	Type const* _commonType
 )
 {
 	static set<Token> validOperators{
@@ -1995,7 +1995,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
 void SMTEncoder::assignment(
 	Expression const& _left,
 	smtutil::Expression const& _right,
-	TypePointer const& _type
+	Type const* _type
 )
 {
 	solAssert(
@@ -2156,7 +2156,7 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression con
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value)
 {
-	TypePointer type = _variable.type();
+	Type const* type = _variable.type();
 	if (type->category() == Type::Category::Mapping)
 		arrayAssignment();
 	assignment(*m_context.variable(_variable), _value);
@@ -2315,16 +2315,16 @@ void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
 	});
 }
 
-void SMTEncoder::resetReferences(TypePointer _type)
+void SMTEncoder::resetReferences(Type const* _type)
 {
 	m_context.resetVariables([&](VariableDeclaration const& _var) {
 		return sameTypeOrSubtype(_var.type(), _type);
 	});
 }
 
-bool SMTEncoder::sameTypeOrSubtype(TypePointer _a, TypePointer _b)
+bool SMTEncoder::sameTypeOrSubtype(Type const* _a, Type const* _b)
 {
-	TypePointer prefix = _a;
+	Type const* prefix = _a;
 	while (
 		prefix->category() == Type::Category::Mapping ||
 		prefix->category() == Type::Category::Array
@@ -2348,7 +2348,7 @@ bool SMTEncoder::sameTypeOrSubtype(TypePointer _a, TypePointer _b)
 	return false;
 }
 
-TypePointer SMTEncoder::typeWithoutPointer(TypePointer const& _type)
+Type const* SMTEncoder::typeWithoutPointer(Type const* _type)
 {
 	if (auto refType = dynamic_cast<ReferenceType const*>(_type))
 		return TypeProvider::withLocationIfReference(refType->location(), _type);
@@ -2419,7 +2419,7 @@ bool SMTEncoder::createVariable(VariableDeclaration const& _varDecl)
 	return true;
 }
 
-smtutil::Expression SMTEncoder::expr(Expression const& _e, TypePointer _targetType)
+smtutil::Expression SMTEncoder::expr(Expression const& _e, Type const* _targetType)
 {
 	if (!m_context.knownExpression(_e))
 	{
@@ -2587,7 +2587,7 @@ Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
 	return base;
 }
 
-TypePointer SMTEncoder::keyType(TypePointer _type)
+Type const* SMTEncoder::keyType(Type const* _type)
 {
 	if (auto const* mappingType = dynamic_cast<MappingType const*>(_type))
 		return mappingType->keyType();

libsolidity/formal/SMTEncoder.h

@@ -62,7 +62,7 @@ public:
 	/// @returns the key type in _type.
 	/// _type must allow IndexAccess, that is,
 	/// it must be either ArrayType or MappingType
-	static TypePointer keyType(TypePointer _type);
+	static Type const* keyType(Type const* _type);
 
 	/// @returns the innermost element in a chain of 1-tuples if applicable,
 	/// otherwise _expr.
@@ -166,7 +166,7 @@ protected:
 		Token _op,
 		smtutil::Expression const& _left,
 		smtutil::Expression const& _right,
-		TypePointer const& _commonType,
+		Type const* _commonType,
 		Expression const& _expression
 	);
 
@@ -174,7 +174,7 @@ protected:
 		Token _op,
 		smtutil::Expression const& _left,
 		smtutil::Expression const& _right,
-		TypePointer const& _commonType
+		Type const* _commonType
 	);
 
 	void compareOperation(BinaryOperation const& _op);
@@ -251,7 +251,7 @@ protected:
 	void assignment(
 		Expression const& _left,
 		smtutil::Expression const& _right,
-		TypePointer const& _type
+		Type const* _type
 	);
 	/// Handle assignments between tuples.
 	void tupleAssignment(Expression const& _left, Expression const& _right);
@@ -284,11 +284,11 @@ protected:
 	/// a subexpression of the same type as _varDecl.
 	void resetReferences(VariableDeclaration const& _varDecl);
 	/// Resets all references/pointers that have type _type.
-	void resetReferences(TypePointer _type);
+	void resetReferences(Type const* _type);
 	/// @returns the type without storage pointer information if it has it.
-	TypePointer typeWithoutPointer(TypePointer const& _type);
+	Type const* typeWithoutPointer(Type const* _type);
 	/// @returns whether _a or a subtype of _a is the same as _b.
-	bool sameTypeOrSubtype(TypePointer _a, TypePointer _b);
+	bool sameTypeOrSubtype(Type const* _a, Type const* _b);
 
 	/// Given two different branches and the touched variables,
 	/// merge the touched variables into after-branch ite variables
@@ -306,7 +306,7 @@ protected:
 	/// Returns the expression corresponding to the AST node.
 	/// If _targetType is not null apply conversion.
 	/// Throws if the expression does not exist.
-	smtutil::Expression expr(Expression const& _e, TypePointer _targetType = nullptr);
+	smtutil::Expression expr(Expression const& _e, Type const* _targetType = nullptr);
 	/// Creates the expression (value can be arbitrary)
 	void createExpr(Expression const& _e);
 	/// Creates the expression and sets its value.

libsolidity/formal/SymbolicState.cpp

@@ -208,8 +208,8 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFuncti
 
 		/// Since each abi.* function may have a different number of input/output parameters,
 		/// we generically compute those types.
-		vector<TypePointer> inTypes;
-		vector<TypePointer> outTypes;
+		vector<frontend::Type const*> inTypes;
+		vector<frontend::Type const*> outTypes;
 		if (t->kind() == FunctionType::Kind::ABIDecode)
 		{
 			/// abi.decode : (bytes, tuple_of_types(return_types)) -> (return_types)

libsolidity/formal/SymbolicState.h

@@ -150,8 +150,8 @@ public:
 	smtutil::Expression abiFunction(FunctionCall const* _funCall);
 	using SymbolicABIFunction = std::tuple<
 		std::string,
-		std::vector<TypePointer>,
-		std::vector<TypePointer>
+		std::vector<frontend::Type const*>,
+		std::vector<frontend::Type const*>
 	>;
 	SymbolicABIFunction const& abiFunctionTypes(FunctionCall const* _funCall) const;
 

libsolidity/formal/SymbolicTypes.cpp

@@ -166,7 +166,7 @@ SortPointer smtSort(frontend::Type const& _type)
 	}
 }
 
-vector<SortPointer> smtSort(vector<frontend::TypePointer> const& _types)
+vector<SortPointer> smtSort(vector<frontend::Type const*> const& _types)
 {
 	vector<SortPointer> sorts;
 	for (auto const& type: _types)
@@ -181,7 +181,7 @@ SortPointer smtSortAbstractFunction(frontend::Type const& _type)
 	return smtSort(_type);
 }
 
-vector<SortPointer> smtSortAbstractFunction(vector<frontend::TypePointer> const& _types)
+vector<SortPointer> smtSortAbstractFunction(vector<frontend::Type const*> const& _types)
 {
 	vector<SortPointer> sorts;
 	for (auto const& type: _types)
@@ -232,7 +232,7 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 {
 	bool abstract = false;
 	shared_ptr<SymbolicVariable> var;
-	frontend::TypePointer type = &_type;
+	frontend::Type const* type = &_type;
 	if (!isSupportedTypeDeclaration(_type))
 	{
 		abstract = true;
@@ -249,7 +249,7 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 			return find_if(
 				begin(params),
 				end(params),
-				[&](TypePointer _paramType) { return _paramType->category() == frontend::Type::Category::Function; }
+				[&](frontend::Type const* _paramType) { return _paramType->category() == frontend::Type::Category::Function; }
 			);
 		};
 		if (
@@ -391,7 +391,7 @@ smtutil::Expression minValue(frontend::IntegerType const& _type)
 	return smtutil::Expression(_type.minValue());
 }
 
-smtutil::Expression minValue(frontend::TypePointer _type)
+smtutil::Expression minValue(frontend::Type const* _type)
 {
 	solAssert(isNumber(*_type), "");
 	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
@@ -413,7 +413,7 @@ smtutil::Expression maxValue(frontend::IntegerType const& _type)
 	return smtutil::Expression(_type.maxValue());
 }
 
-smtutil::Expression maxValue(frontend::TypePointer _type)
+smtutil::Expression maxValue(frontend::Type const* _type)
 {
 	solAssert(isNumber(*_type), "");
 	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
@@ -437,13 +437,13 @@ void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _c
 	setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context);
 }
 
-void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
+void setSymbolicZeroValue(smtutil::Expression _expr, frontend::Type const* _type, EncodingContext& _context)
 {
 	solAssert(_type, "");
 	_context.addAssertion(_expr == zeroValue(_type));
 }
 
-smtutil::Expression zeroValue(frontend::TypePointer const& _type)
+smtutil::Expression zeroValue(frontend::Type const* _type)
 {
 	solAssert(_type, "");
 	if (isSupportedType(*_type))
@@ -496,7 +496,7 @@ smtutil::Expression zeroValue(frontend::TypePointer const& _type)
 	return 0;
 }
 
-bool isSigned(TypePointer const& _type)
+bool isSigned(frontend::Type const* _type)
 {
 	solAssert(smt::isNumber(*_type), "");
 	bool isSigned = false;
@@ -519,7 +519,7 @@ bool isSigned(TypePointer const& _type)
 	return isSigned;
 }
 
-pair<unsigned, bool> typeBvSizeAndSignedness(frontend::TypePointer const& _type)
+pair<unsigned, bool> typeBvSizeAndSignedness(frontend::Type const* _type)
 {
 	if (auto const* intType = dynamic_cast<IntegerType const*>(_type))
 		return {intType->numBits(), intType->isSigned()};
@@ -536,12 +536,12 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
 	setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _context);
 }
 
-void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
+void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::Type const* _type, EncodingContext& _context)
 {
 	_context.addAssertion(symbolicUnknownConstraints(_expr, _type));
 }
 
-smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::TypePointer const& _type)
+smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::Type const* _type)
 {
 	solAssert(_type, "");
 	if (isEnum(*_type) || isInteger(*_type) || isAddress(*_type) || isFixedBytes(*_type))
@@ -553,7 +553,7 @@ smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, fronte
 	return smtutil::Expression(true);
 }
 
-optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)
+optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to)
 {
 	if (_to && _from)
 		// StringLiterals are encoded as SMT arrays in the generic case,

libsolidity/formal/SymbolicTypes.h

@@ -29,11 +29,11 @@ class EncodingContext;
 
 /// Returns the SMT sort that models the Solidity type _type.
 smtutil::SortPointer smtSort(frontend::Type const& _type);
-std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> const& _types);
+std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::Type const*> const& _types);
 /// If _type has type Function, abstract it to Integer.
 /// Otherwise return smtSort(_type).
 smtutil::SortPointer smtSortAbstractFunction(frontend::Type const& _type);
-std::vector<smtutil::SortPointer> smtSortAbstractFunction(std::vector<frontend::TypePointer> const& _types);
+std::vector<smtutil::SortPointer> smtSortAbstractFunction(std::vector<frontend::Type const*> const& _types);
 /// Returns the SMT kind that models the Solidity type type category _category.
 smtutil::Kind smtKind(frontend::Type const& _type);
 
@@ -66,19 +66,19 @@ bool isNonRecursiveStruct(frontend::Type const& _type);
 std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(frontend::Type const& _type, std::string const& _uniqueName, EncodingContext& _context);
 
 smtutil::Expression minValue(frontend::IntegerType const& _type);
-smtutil::Expression minValue(frontend::TypePointer _type);
+smtutil::Expression minValue(frontend::Type const* _type);
 smtutil::Expression maxValue(frontend::IntegerType const& _type);
-smtutil::Expression maxValue(frontend::TypePointer _type);
-smtutil::Expression zeroValue(frontend::TypePointer const& _type);
-bool isSigned(frontend::TypePointer const& _type);
+smtutil::Expression maxValue(frontend::Type const* _type);
+smtutil::Expression zeroValue(frontend::Type const* _type);
+bool isSigned(frontend::Type const* _type);
 
-std::pair<unsigned, bool> typeBvSizeAndSignedness(frontend::TypePointer const& type);
+std::pair<unsigned, bool> typeBvSizeAndSignedness(frontend::Type const* type);
 
 void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context);
-void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
+void setSymbolicZeroValue(smtutil::Expression _expr, frontend::Type const* _type, EncodingContext& _context);
 void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context);
-void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
-smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::TypePointer const& _type);
+void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::Type const* _type, EncodingContext& _context);
+smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::Type const* _type);
 
-std::optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to);
+std::optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to);
 }

libsolidity/formal/SymbolicVariables.cpp

@@ -32,8 +32,8 @@ using namespace solidity::frontend;
 using namespace solidity::frontend::smt;
 
 SymbolicVariable::SymbolicVariable(
-	TypePointer _type,
-	TypePointer _originalType,
+	frontend::Type const* _type,
+	frontend::Type const* _originalType,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -61,7 +61,7 @@ SymbolicVariable::SymbolicVariable(
 	solAssert(m_sort, "");
 }
 
-smtutil::Expression SymbolicVariable::currentValue(frontend::TypePointer const&) const
+smtutil::Expression SymbolicVariable::currentValue(frontend::Type const*) const
 {
 	return valueAtIndex(m_ssa->index());
 }
@@ -105,7 +105,7 @@ smtutil::Expression SymbolicVariable::increaseIndex()
 }
 
 SymbolicBoolVariable::SymbolicBoolVariable(
-	frontend::TypePointer _type,
+	frontend::Type const* _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -115,8 +115,8 @@ SymbolicBoolVariable::SymbolicBoolVariable(
 }
 
 SymbolicIntVariable::SymbolicIntVariable(
-	frontend::TypePointer _type,
-	frontend::TypePointer _originalType,
+	frontend::Type const* _type,
+	frontend::Type const* _originalType,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -134,7 +134,7 @@ SymbolicAddressVariable::SymbolicAddressVariable(
 }
 
 SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
-	frontend::TypePointer _originalType,
+	frontend::Type const* _originalType,
 	unsigned _numBytes,
 	string _uniqueName,
 	EncodingContext& _context
@@ -144,7 +144,7 @@ SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
 }
 
 SymbolicFunctionVariable::SymbolicFunctionVariable(
-	frontend::TypePointer _type,
+	frontend::Type const* _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -165,7 +165,7 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
 	solAssert(m_sort->kind == Kind::Function, "");
 }
 
-smtutil::Expression SymbolicFunctionVariable::currentValue(frontend::TypePointer const& _targetType) const
+smtutil::Expression SymbolicFunctionVariable::currentValue(frontend::Type const* _targetType) const
 {
 	return m_abstract.currentValue(_targetType);
 }
@@ -216,7 +216,7 @@ void SymbolicFunctionVariable::resetDeclaration()
 }
 
 SymbolicEnumVariable::SymbolicEnumVariable(
-	frontend::TypePointer _type,
+	frontend::Type const* _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -226,7 +226,7 @@ SymbolicEnumVariable::SymbolicEnumVariable(
 }
 
 SymbolicTupleVariable::SymbolicTupleVariable(
-	frontend::TypePointer _type,
+	frontend::Type const* _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -245,7 +245,7 @@ SymbolicTupleVariable::SymbolicTupleVariable(
 	solAssert(m_sort->kind == Kind::Tuple, "");
 }
 
-smtutil::Expression SymbolicTupleVariable::currentValue(frontend::TypePointer const& _targetType) const
+smtutil::Expression SymbolicTupleVariable::currentValue(frontend::Type const* _targetType) const
 {
 	if (!_targetType || sort() == smtSort(*_targetType))
 		return SymbolicVariable::currentValue();
@@ -272,8 +272,8 @@ vector<SortPointer> const& SymbolicTupleVariable::components() const
 
 smtutil::Expression SymbolicTupleVariable::component(
 	size_t _index,
-	TypePointer _fromType,
-	TypePointer _toType
+	frontend::Type const* _fromType,
+	frontend::Type const* _toType
 ) const
 {
 	optional<smtutil::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
@@ -284,8 +284,8 @@ smtutil::Expression SymbolicTupleVariable::component(
 }
 
 SymbolicArrayVariable::SymbolicArrayVariable(
-	frontend::TypePointer _type,
-	frontend::TypePointer _originalType,
+	frontend::Type const* _type,
+	frontend::Type const* _originalType,
 	string _uniqueName,
 	EncodingContext& _context
 ):
@@ -318,7 +318,7 @@ SymbolicArrayVariable::SymbolicArrayVariable(
 	solAssert(m_sort->kind == Kind::Array, "");
 }
 
-smtutil::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
+smtutil::Expression SymbolicArrayVariable::currentValue(frontend::Type const* _targetType) const
 {
 	optional<smtutil::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
 	if (conversion)
@@ -343,7 +343,7 @@ smtutil::Expression SymbolicArrayVariable::length() const
 }
 
 SymbolicStructVariable::SymbolicStructVariable(
-	frontend::TypePointer _type,
+	frontend::Type const* _type,
 	string _uniqueName,
 	EncodingContext& _context
 ):

libsolidity/formal/SymbolicVariables.h

@@ -40,8 +40,8 @@ class SymbolicVariable
 {
 public:
 	SymbolicVariable(
-		frontend::TypePointer _type,
-		frontend::TypePointer _originalType,
+		frontend::Type const* _type,
+		frontend::Type const* _originalType,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -55,7 +55,7 @@ public:
 
 	virtual ~SymbolicVariable() = default;
 
-	virtual smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const;
+	virtual smtutil::Expression currentValue(frontend::Type const* _targetType = nullptr) const;
 	std::string currentName() const;
 	virtual smtutil::Expression valueAtIndex(unsigned _index) const;
 	virtual std::string nameAtIndex(unsigned _index) const;
@@ -71,8 +71,8 @@ public:
 	unsigned& index() { return m_ssa->index(); }
 
 	smtutil::SortPointer const& sort() const { return m_sort; }
-	frontend::TypePointer const& type() const { return m_type; }
-	frontend::TypePointer const& originalType() const { return m_originalType; }
+	frontend::Type const* type() const { return m_type; }
+	frontend::Type const* originalType() const { return m_originalType; }
 
 protected:
 	std::string uniqueSymbol(unsigned _index) const;
@@ -80,9 +80,9 @@ protected:
 	/// SMT sort.
 	smtutil::SortPointer m_sort;
 	/// Solidity type, used for size and range in number types.
-	frontend::TypePointer m_type;
+	frontend::Type const* m_type;
 	/// Solidity original type, used for type conversion if necessary.
-	frontend::TypePointer m_originalType;
+	frontend::Type const* m_originalType;
 	std::string m_uniqueName;
 	EncodingContext& m_context;
 	std::unique_ptr<SSAVariable> m_ssa;
@@ -95,7 +95,7 @@ class SymbolicBoolVariable: public SymbolicVariable
 {
 public:
 	SymbolicBoolVariable(
-		frontend::TypePointer _type,
+		frontend::Type const* _type,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -108,8 +108,8 @@ class SymbolicIntVariable: public SymbolicVariable
 {
 public:
 	SymbolicIntVariable(
-		frontend::TypePointer _type,
-		frontend::TypePointer _originalType,
+		frontend::Type const* _type,
+		frontend::Type const* _originalType,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -134,7 +134,7 @@ class SymbolicFixedBytesVariable: public SymbolicIntVariable
 {
 public:
 	SymbolicFixedBytesVariable(
-		frontend::TypePointer _originalType,
+		frontend::Type const* _originalType,
 		unsigned _numBytes,
 		std::string _uniqueName,
 		EncodingContext& _context
@@ -153,7 +153,7 @@ class SymbolicFunctionVariable: public SymbolicVariable
 {
 public:
 	SymbolicFunctionVariable(
-		frontend::TypePointer _type,
+		frontend::Type const* _type,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -163,7 +163,7 @@ public:
 		EncodingContext& _context
 	);
 
-	smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+	smtutil::Expression currentValue(frontend::Type const* _targetType = nullptr) const override;
 
 	// Explicit request the function declaration.
 	smtutil::Expression currentFunctionValue() const;
@@ -202,7 +202,7 @@ class SymbolicEnumVariable: public SymbolicVariable
 {
 public:
 	SymbolicEnumVariable(
-		frontend::TypePointer _type,
+		frontend::Type const* _type,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -215,7 +215,7 @@ class SymbolicTupleVariable: public SymbolicVariable
 {
 public:
 	SymbolicTupleVariable(
-		frontend::TypePointer _type,
+		frontend::Type const* _type,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -225,13 +225,13 @@ public:
 		EncodingContext& _context
 	);
 
-	smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+	smtutil::Expression currentValue(frontend::Type const* _targetType = nullptr) const override;
 
 	std::vector<smtutil::SortPointer> const& components() const;
 	smtutil::Expression component(
 		size_t _index,
-		TypePointer _fromType = nullptr,
-		TypePointer _toType = nullptr
+		frontend::Type const* _fromType = nullptr,
+		frontend::Type const* _toType = nullptr
 	) const;
 };
 
@@ -242,8 +242,8 @@ class SymbolicArrayVariable: public SymbolicVariable
 {
 public:
 	SymbolicArrayVariable(
-		frontend::TypePointer _type,
-		frontend::TypePointer _originalTtype,
+		frontend::Type const* _type,
+		frontend::Type const* _originalTtype,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
@@ -255,7 +255,7 @@ public:
 
 	SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
 
-	smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+	smtutil::Expression currentValue(frontend::Type const* _targetType = nullptr) const override;
 	smtutil::Expression valueAtIndex(unsigned _index) const override;
 	smtutil::Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); }
 	smtutil::Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); }
@@ -276,7 +276,7 @@ class SymbolicStructVariable: public SymbolicVariable
 {
 public:
 	SymbolicStructVariable(
-		frontend::TypePointer _type,
+		frontend::Type const* _type,
 		std::string _uniqueName,
 		EncodingContext& _context
 	);