Skip to content

Commit 4577aeb

Browse files
ekpyronekpyron
authored
Merge pull request argotorg#14655 from ethereum/new-analysis-fixed-type-variables
Fixed type variables for functions, type classes and types in new analysis
2 parents 1906cf1 + 8e210d2 commit 4577aeb

File tree

12 files changed

+259
-135
lines changed

12 files changed

+259
-135
lines changed

‎libsolidity/experimental/analysis/TypeInference.cpp‎

Lines changed: 40 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@
3333
#include <libyul/AST.h>
3434

3535
#include <boost/algorithm/string.hpp>
36+
3637
#include <range/v3/view/transform.hpp>
3738

3839
using namespace solidity;
@@ -166,6 +167,13 @@ bool TypeInference::visit(FunctionDefinition const& _functionDefinition)
166167
return false;
167168
}
168169

170+
void TypeInference::endVisit(FunctionDefinition const& _functionDefinition)
171+
{
172+
solAssert(m_expressionContext == ExpressionContext::Term);
173+
174+
m_env->fixTypeVars(TypeEnvironmentHelpers{*m_env}.typeVars(type(_functionDefinition)));
175+
}
176+
169177
void TypeInference::endVisit(Return const& _return)
170178
{
171179
solAssert(m_currentFunctionType);
@@ -204,6 +212,8 @@ bool TypeInference::visit(TypeClassDefinition const& _typeClassDefinition)
204212
solAssert(m_analysis.annotation<TypeClassRegistration>(_typeClassDefinition).typeClass.has_value());
205213
TypeClass typeClass = m_analysis.annotation<TypeClassRegistration>(_typeClassDefinition).typeClass.value();
206214
Type typeVar = m_typeSystem.typeClassVariable(typeClass);
215+
unify(type(_typeClassDefinition.typeVariable()), typeVar, _typeClassDefinition.location());
216+
207217
auto& typeMembersAnnotation = annotation().members[typeConstructor(&_typeClassDefinition)];
208218

209219
for (auto subNode: _typeClassDefinition.subNodes())
@@ -235,7 +245,6 @@ bool TypeInference::visit(TypeClassDefinition const& _typeClassDefinition)
235245
m_errorReporter.typeError(1807_error, _typeClassDefinition.location(), "Function " + functionName + " depends on invalid type variable.");
236246
}
237247

238-
unify(type(_typeClassDefinition.typeVariable()), m_typeSystem.freshTypeVariable({{typeClass}}), _typeClassDefinition.location());
239248
for (auto instantiation: m_analysis.annotation<TypeRegistration>(_typeClassDefinition).instantiations | ranges::views::values)
240249
// TODO: recursion-safety? Order of instantiation?
241250
instantiation->accept(*this);
@@ -663,6 +672,7 @@ bool TypeInference::visit(TypeClassInstantiation const& _typeClassInstantiation)
663672
}) | ranges::to<std::vector<Sort>>;
664673
}
665674
}
675+
m_env->fixTypeVars(arguments);
666676

667677
Type instanceType{TypeConstant{*typeConstructor, arguments}};
668678

@@ -682,12 +692,8 @@ bool TypeInference::visit(TypeClassInstantiation const& _typeClassInstantiation)
682692

683693
auto const& classFunctions = annotation().typeClassFunctions.at(typeClass);
684694

685-
TypeEnvironment newEnv = m_env->clone();
686-
if (!newEnv.unify(m_typeSystem.typeClassVariable(typeClass), instanceType).empty())
687-
{
688-
m_errorReporter.typeError(4686_error, _typeClassInstantiation.location(), "Unification of class and instance variable failed.");
689-
return false;
690-
}
695+
solAssert(std::holds_alternative<TypeVariable>(m_typeSystem.typeClassVariable(typeClass)));
696+
TypeVariable classVar = std::get<TypeVariable>(m_typeSystem.typeClassVariable(typeClass));
691697

692698
for (auto [name, classFunctionType]: classFunctions)
693699
{
@@ -696,11 +702,22 @@ bool TypeInference::visit(TypeClassInstantiation const& _typeClassInstantiation)
696702
m_errorReporter.typeError(6948_error, _typeClassInstantiation.location(), "Missing function: " + name);
697703
continue;
698704
}
705+
Type instantiatedClassFunctionType = TypeEnvironmentHelpers{*m_env}.substitute(classFunctionType, classVar, instanceType);
706+
699707
Type instanceFunctionType = functionTypes.at(name);
700708
functionTypes.erase(name);
701709

702-
if (!newEnv.typeEquals(instanceFunctionType, classFunctionType))
703-
m_errorReporter.typeError(7428_error, _typeClassInstantiation.location(), "Type mismatch for function " + name + " " + TypeEnvironmentHelpers{newEnv}.typeToString(instanceFunctionType) + " != " + TypeEnvironmentHelpers{newEnv}.typeToString(classFunctionType));
710+
if (!m_env->typeEquals(instanceFunctionType, instantiatedClassFunctionType))
711+
m_errorReporter.typeError(
712+
7428_error,
713+
_typeClassInstantiation.location(),
714+
fmt::format(
715+
"Instantiation function '{}' does not match the declaration in the type class ({} != {}).",
716+
name,
717+
TypeEnvironmentHelpers{*m_env}.typeToString(instanceFunctionType),
718+
TypeEnvironmentHelpers{*m_env}.typeToString(instantiatedClassFunctionType)
719+
)
720+
);
704721
}
705722

706723
if (!functionTypes.empty())
@@ -760,12 +777,21 @@ bool TypeInference::visit(TypeDefinition const& _typeDefinition)
760777
return false;
761778

762779
if (_typeDefinition.arguments())
780+
{
781+
ScopedSaveAndRestore expressionContext{m_expressionContext, ExpressionContext::Type};
763782
_typeDefinition.arguments()->accept(*this);
783+
}
764784

765785
std::vector<Type> arguments;
766786
if (_typeDefinition.arguments())
767-
for (size_t i = 0; i < _typeDefinition.arguments()->parameters().size(); ++i)
768-
arguments.emplace_back(m_typeSystem.freshTypeVariable({}));
787+
for (ASTPointer<VariableDeclaration> argumentDeclaration: _typeDefinition.arguments()->parameters())
788+
{
789+
solAssert(argumentDeclaration);
790+
Type typeVar = type(*argumentDeclaration);
791+
solAssert(std::holds_alternative<TypeVariable>(typeVar));
792+
arguments.emplace_back(typeVar);
793+
}
794+
m_env->fixTypeVars(arguments);
769795

770796
Type definedType = type(&_typeDefinition, arguments);
771797
if (arguments.empty())
@@ -791,6 +817,9 @@ bool TypeInference::visit(TypeDefinition const& _typeDefinition)
791817
solAssert(newlyInserted, fmt::format("Members of type '{}' are already defined.", m_typeSystem.constructorInfo(constructor).name));
792818
if (underlyingType)
793819
{
820+
// Undeclared type variables are not allowed in type definitions and we fixed all the declared ones.
821+
solAssert(!TypeEnvironmentHelpers{*m_env}.hasGenericTypeVars(*underlyingType));
822+
794823
members->second.emplace("abs", TypeMember{helper.functionType(*underlyingType, definedType)});
795824
members->second.emplace("rep", TypeMember{helper.functionType(definedType, *underlyingType)});
796825
}

‎libsolidity/experimental/analysis/TypeInference.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ class TypeInference: public ASTConstVisitor
5757
bool visit(VariableDeclaration const& _variableDeclaration) override;
5858

5959
bool visit(FunctionDefinition const& _functionDefinition) override;
60+
void endVisit(FunctionDefinition const& _functionDefinition) override;
6061
bool visit(ParameterList const&) override { return true; }
6162
void endVisit(ParameterList const& _parameterList) override;
6263
bool visit(SourceUnit const&) override { return true; }

‎libsolidity/experimental/ast/TypeSystem.cpp‎

Lines changed: 33 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -50,18 +50,21 @@ std::vector<TypeEnvironment::UnificationFailure> TypeEnvironment::unify(Type _a,
5050
[&](TypeVariable _left, TypeVariable _right) {
5151
if (_left.index() == _right.index())
5252
solAssert(_left.sort() == _right.sort());
53+
else if (isFixedTypeVar(_left) && isFixedTypeVar(_right))
54+
unificationFailure();
55+
else if (isFixedTypeVar(_left))
56+
failures += instantiate(_right, _left);
57+
else if (isFixedTypeVar(_right))
58+
failures += instantiate(_left, _right);
59+
else if (_left.sort() <= _right.sort())
60+
failures += instantiate(_left, _right);
61+
else if (_right.sort() <= _left.sort())
62+
failures += instantiate(_right, _left);
5363
else
5464
{
55-
if (_left.sort() <= _right.sort())
56-
failures += instantiate(_left, _right);
57-
else if (_right.sort() <= _left.sort())
58-
failures += instantiate(_right, _left);
59-
else
60-
{
61-
Type newVar = m_typeSystem.freshVariable(_left.sort() + _right.sort());
62-
failures += instantiate(_left, newVar);
63-
failures += instantiate(_right, newVar);
64-
}
65+
Type newVar = m_typeSystem.freshVariable(_left.sort() + _right.sort());
66+
failures += instantiate(_left, newVar);
67+
failures += instantiate(_right, newVar);
6568
}
6669
},
6770
[&](TypeVariable _var, auto) {
@@ -112,6 +115,23 @@ bool TypeEnvironment::typeEquals(Type _lhs, Type _rhs) const
112115
}, resolve(_lhs), resolve(_rhs));
113116
}
114117

118+
119+
bool TypeEnvironment::isFixedTypeVar(Type const& _typeVar) const
120+
{
121+
return
122+
std::holds_alternative<TypeVariable>(_typeVar) &&
123+
m_fixedTypeVariables.count(std::get<TypeVariable>(_typeVar).index()) != 0;
124+
}
125+
126+
void TypeEnvironment::fixTypeVars(std::vector<Type> const& _typeVars)
127+
{
128+
for (Type const& typeVar: _typeVars)
129+
{
130+
solAssert(std::holds_alternative<TypeVariable>(typeVar));
131+
m_fixedTypeVariables.insert(std::get<TypeVariable>(typeVar).index());
132+
}
133+
}
134+
115135
TypeEnvironment TypeEnvironment::clone() const
116136
{
117137
TypeEnvironment result{m_typeSystem};
@@ -263,6 +283,7 @@ TypeConstructor TypeSystem::declareTypeConstructor(std::string _name, std::strin
263283
std::generate_n(std::back_inserter(argumentSorts), _arguments, [&](){ return Sort{{primitiveClass(PrimitiveClass::Type)}}; });
264284
std::vector<Type> argumentTypes;
265285
std::generate_n(std::back_inserter(argumentTypes), _arguments, [&](){ return freshVariable({}); });
286+
m_globalTypeEnvironment.fixTypeVars(argumentTypes);
266287
auto error = instantiateClass(type(constructor, argumentTypes), Arity{argumentSorts, primitiveClass(PrimitiveClass::Type)});
267288
solAssert(!error, *error);
268289
}
@@ -281,6 +302,8 @@ std::variant<TypeClass, std::string> TypeSystem::declareTypeClass(std::string _n
281302
Type typeVariable = (_primitive ? freshVariable({{typeClass}}) : freshTypeVariable({{typeClass}}));
282303
solAssert(std::holds_alternative<TypeVariable>(typeVariable));
283304

305+
m_globalTypeEnvironment.fixTypeVars({typeVariable});
306+
284307
m_typeClasses.emplace_back(TypeClassInfo{
285308
typeVariable,
286309
_name,

‎libsolidity/experimental/ast/TypeSystem.h‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,9 @@ class TypeEnvironment
7474
TypeSystem& typeSystem() { return m_typeSystem; }
7575
TypeSystem const& typeSystem() const { return m_typeSystem; }
7676

77+
bool isFixedTypeVar(Type const& _typeVar) const;
78+
void fixTypeVars(std::vector<Type> const& _typeVars);
79+
7780
private:
7881
TypeEnvironment(TypeEnvironment&& _env):
7982
m_typeSystem(_env.m_typeSystem),
@@ -83,7 +86,15 @@ class TypeEnvironment
8386
[[nodiscard]] std::vector<TypeEnvironment::UnificationFailure> instantiate(TypeVariable _variable, Type _type);
8487

8588
TypeSystem& m_typeSystem;
89+
90+
/// For each @a TypeVariable (identified by its index) stores the type is has been successfully
91+
/// unified with. Used for type resolution. Note that @a Type may itself be a type variable
92+
/// or may contain type variables so resolution must be recursive.
8693
std::map<size_t, Type> m_typeVariables;
94+
95+
/// Type variables marked as fixed free type variables (as opposed to generic type variables).
96+
/// Identified by their indices.
97+
std::set<size_t> m_fixedTypeVariables;
8798
};
8899

89100
class TypeSystem

‎libsolidity/experimental/ast/TypeSystemHelper.cpp‎

Lines changed: 39 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@
2525

2626
#include <libsolutil/Visitor.h>
2727

28+
#include <range/v3/algorithm/any_of.hpp>
2829
#include <range/v3/to_container.hpp>
2930
#include <range/v3/view/drop_exactly.hpp>
3031
#include <range/v3/view/drop_last.hpp>
@@ -287,9 +288,46 @@ std::vector<experimental::Type> TypeEnvironmentHelpers::typeVars(Type _type) con
287288
};
288289
typeVarsImpl(_type, typeVarsImpl);
289290
return typeVars;
291+
}
292+
290293

294+
bool TypeEnvironmentHelpers::hasGenericTypeVars(Type const& _type) const
295+
{
296+
return ranges::any_of(
297+
TypeEnvironmentHelpers{*this}.typeVars(_type),
298+
[&](Type const& _maybeTypeVar) {
299+
solAssert(std::holds_alternative<TypeVariable>(_maybeTypeVar));
300+
return !env.isFixedTypeVar(_maybeTypeVar);
301+
}
302+
);
291303
}
292304

305+
experimental::Type TypeEnvironmentHelpers::substitute(
306+
Type const& _type,
307+
Type const& _partToReplace,
308+
Type const& _replacement
309+
) const
310+
{
311+
using ranges::views::transform;
312+
using ranges::to;
313+
314+
if (env.typeEquals(_type, _partToReplace))
315+
return _replacement;
316+
317+
auto recurse = [&](Type const& _t) { return substitute(_t, _partToReplace, _replacement); };
318+
319+
return visit(util::GenericVisitor{
320+
[&](TypeConstant const& _typeConstant) -> Type {
321+
return TypeConstant{
322+
_typeConstant.constructor,
323+
_typeConstant.arguments | transform(recurse) | to<std::vector<Type>>,
324+
};
325+
},
326+
[&](auto const& _type) -> Type {
327+
return _type;
328+
},
329+
}, env.resolve(_type));
330+
}
293331

294332
std::string TypeSystemHelpers::sortToString(Sort _sort) const
295333
{
@@ -381,7 +419,7 @@ std::string TypeEnvironmentHelpers::typeToString(Type const& _type) const
381419
while (index /= 26)
382420
varName += static_cast<char>('a' + (index%26));
383421
reverse(varName.begin(), varName.end());
384-
stream << '\'' << varName;
422+
stream << (env.isFixedTypeVar(_type) ? "'" : "?") << varName;
385423
switch (_type.sort().classes.size())
386424
{
387425
case 0:

‎libsolidity/experimental/ast/TypeSystemHelper.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,10 @@ struct TypeEnvironmentHelpers
5555
std::string typeToString(Type const& _type) const;
5656
std::string canonicalTypeName(Type _type) const;
5757
std::vector<Type> typeVars(Type _type) const;
58+
59+
bool hasGenericTypeVars(Type const& _type) const;
60+
61+
Type substitute(Type const& _type, Type const& _partToReplace, Type const& _replacement) const;
5862
};
5963

6064
}

‎test/libsolidity/syntaxTests/experimental/builtin/builtin_type_definition.sol‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -40,14 +40,14 @@ contract C {
4040
// Info 4164: (94-124): Inferred type: word
4141
// Info 4164: (125-161): Inferred type: integer
4242
// Info 4164: (162-192): Inferred type: ()
43-
// Info 4164: (194-228): Inferred type: tfun(('u:type, 'v:type), 'u:type -> 'v:type)
43+
// Info 4164: (194-228): Inferred type: tfun(('s:type, 't:type), 's:type -> 't:type)
4444
// Info 4164: (202-208): Inferred type: ('s:type, 't:type)
4545
// Info 4164: (203-204): Inferred type: 's:type
4646
// Info 4164: (206-207): Inferred type: 't:type
47-
// Info 4164: (229-265): Inferred type: tfun(('y:type, 'z:type), ('y:type, 'z:type))
48-
// Info 4164: (238-244): Inferred type: ('w:type, 'x:type)
49-
// Info 4164: (239-240): Inferred type: 'w:type
50-
// Info 4164: (242-243): Inferred type: 'x:type
47+
// Info 4164: (229-265): Inferred type: tfun(('u:type, 'v:type), ('u:type, 'v:type))
48+
// Info 4164: (238-244): Inferred type: ('u:type, 'v:type)
49+
// Info 4164: (239-240): Inferred type: 'u:type
50+
// Info 4164: (242-243): Inferred type: 'v:type
5151
// Info 4164: (284-584): Inferred type: () -> ()
5252
// Info 4164: (292-294): Inferred type: ()
5353
// Info 4164: (318-325): Inferred type: void
@@ -84,9 +84,9 @@ contract C {
8484
// Info 4164: (525-529): Inferred type: word
8585
// Info 4164: (540-553): Inferred type: bool
8686
// Info 4164: (540-550): Inferred type: (bool, word) -> bool
87-
// Info 4164: (540-544): Inferred type: ('bl:type, 'bm:type)
87+
// Info 4164: (540-544): Inferred type: (?bh:type, ?bi:type)
8888
// Info 4164: (551-552): Inferred type: (bool, word)
8989
// Info 4164: (563-577): Inferred type: word
9090
// Info 4164: (563-574): Inferred type: (bool, word) -> word
91-
// Info 4164: (563-567): Inferred type: ('bq:type, 'br:type)
91+
// Info 4164: (563-567): Inferred type: (?bm:type, ?bn:type)
9292
// Info 4164: (575-576): Inferred type: (bool, word)

‎test/libsolidity/syntaxTests/experimental/inference/instantiation_member_type_does_not_match_declaration.sol‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
pragma experimental solidity;
2+
3+
type T;
4+
type U;
5+
6+
class Self: C {
7+
function f(self: Self);
8+
}
9+
10+
instantiation T: C {
11+
function f(self: U) {}
12+
}
13+
// ====
14+
// EVMVersion: >=constantinople
15+
// compileViaYul: true
16+
// ----
17+
// Warning 2264: (0-29): Experimental features are turned on. Do not use experimental features on live deployments.
18+
// TypeError 7428: (95-144): Instantiation function 'f' does not match the declaration in the type class (U -> () != T -> ()).

‎test/libsolidity/syntaxTests/experimental/inference/polymorphic_function_call.sol‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -15,18 +15,18 @@ function run(a: T, b: U(T), c: U(U(T))) {
1515
// ----
1616
// Warning 2264: (0-29): Experimental features are turned on. Do not use experimental features on live deployments.
1717
// Info 4164: (31-38): Inferred type: T
18-
// Info 4164: (39-49): Inferred type: tfun('u:type, U('u:type))
18+
// Info 4164: (39-49): Inferred type: tfun('t:type, U('t:type))
1919
// Info 4164: (45-48): Inferred type: 't:type
2020
// Info 4164: (46-47): Inferred type: 't:type
21-
// Info 4164: (51-82): Inferred type: ('x:type, 'y:type, U('ba:type)) -> ()
22-
// Info 4164: (61-79): Inferred type: ('x:type, 'y:type, U('ba:type))
23-
// Info 4164: (62-63): Inferred type: 'x:type
24-
// Info 4164: (65-69): Inferred type: 'y:type
25-
// Info 4164: (68-69): Inferred type: 'y:type
26-
// Info 4164: (71-78): Inferred type: U('ba:type)
27-
// Info 4164: (74-78): Inferred type: U('ba:type)
28-
// Info 4164: (74-75): Inferred type: tfun('ba:type, U('ba:type))
29-
// Info 4164: (76-77): Inferred type: 'ba:type
21+
// Info 4164: (51-82): Inferred type: ('w:type, 'x:type, U('z:type)) -> ()
22+
// Info 4164: (61-79): Inferred type: ('w:type, 'x:type, U('z:type))
23+
// Info 4164: (62-63): Inferred type: 'w:type
24+
// Info 4164: (65-69): Inferred type: 'x:type
25+
// Info 4164: (68-69): Inferred type: 'x:type
26+
// Info 4164: (71-78): Inferred type: U('z:type)
27+
// Info 4164: (74-78): Inferred type: U('z:type)
28+
// Info 4164: (74-75): Inferred type: tfun('z:type, U('z:type))
29+
// Info 4164: (76-77): Inferred type: 'z:type
3030
// Info 4164: (84-159): Inferred type: (T, U(T), U(U(T))) -> ()
3131
// Info 4164: (96-123): Inferred type: (T, U(T), U(U(T)))
3232
// Info 4164: (97-101): Inferred type: T

0 commit comments

Comments
 (0)