wyc.builder

Class FlowTypeChecker

java.lang.Object

wyc.builder.FlowTypeChecker

public class FlowTypeChecker
extends Object

Propagates type information in a flow-sensitive fashion from declared parameter and return types through variable declarations and assigned expressions, to determine types for all intermediate expressions and variables. During this propagation, type checking is performed to ensure types are used soundly. For example:

 function sum(int[] data) -> int:
     int r = 0      // declared int type for r
     for v in data: // infers int type for v, based on type of data
         r = r + v  // infers int type for r + v, based on type of operands
     return r       // infers int type for return expression
 

The flow typing algorithm distinguishes between the declared type of a variable and its known type. That is, the known type at any given point is permitted to be more precise than the declared type (but not vice versa). For example:

 function id(int x) -> int:
    return x

 function f(int y) -> int:
    int|null x = y
    f(x)
 

The above example is considered type safe because the known type of x at the function call is int, which differs from its declared type (i.e. int|null).

Loops present an interesting challenge for type propagation. Consider this example:

 function loopy(int max) -> real:
     var i = 0
     while i < max:
         i = i + 0.5
     return i
 

On the first pass through the loop, variable i is inferred to have type int (based on the type of the constant 0 ). However, the add expression is inferred to have type real (based on the type of the rhs) and, hence, the resulting type inferred for i is real. At this point, the loop must be reconsidered taking into account this updated type for i.

The operation of the flow type checker splits into two stages:

• Global Propagation. During this stage, all named types are checked and expanded.
• Local Propagation. During this stage, types are propagated through statements and expressions (as above).

References

• David J. Pearce and James Noble. Structural and Flow-Sensitive Types for Whiley. Technical Report, Victoria University of Wellington, 2010.

Author:

David J. Pearce

Constructor Summary

Constructors

Constructor and Description
FlowTypeChecker(CompileTask builder)

Method Summary

Modifier and Type	Method and Description
static Type	applySubstitution(List<String> lifetimeParameters, List<String> lifetimeArguments, Type original) Apply a lifetime substitution: Substitute all parameters in original by their arguments.
Type.EffectiveArray	expandAsEffectiveArray(Expr src, WhileyFile.Context context)
Type.EffectiveArray	expandAsEffectiveArray(Type type, wybs.lang.SyntacticElement element, WhileyFile.Context context)
Type.FunctionOrMethod	expandAsEffectiveFunctionOrMethod(Expr src, WhileyFile.Context context)
Type.FunctionOrMethod	expandAsEffectiveFunctionOrMethod(Type type, wybs.lang.SyntacticElement element, WhileyFile.Context context)
Type.EffectiveRecord	expandAsEffectiveRecord(Expr src, WhileyFile.Context context)
Type.EffectiveRecord	expandAsEffectiveRecord(Type type, wybs.lang.SyntacticElement element, WhileyFile.Context context)
Type.Reference	expandAsEffectiveReference(Expr src, WhileyFile.Context context)
Type.Reference	expandAsEffectiveReference(Type type, wybs.lang.SyntacticElement element, WhileyFile.Context context)
Expr	propagate(Expr expr, wyc.builder.FlowTypeChecker.Environment environment, WhileyFile.Context context) Propagate types through a given expression, whilst checking that it is well typed.
void	propagate(List<WhileyFile> files)
void	propagate(WhileyFile.Constant cd) Propagate and check types for a given constant declaration.
void	propagate(WhileyFile.FunctionOrMethodOrProperty d) Propagate and check types for a given function or method declaration.
void	propagate(WhileyFile.Type td) Resolve types for a given type declaration.
void	propagate(WhileyFile wf)
wycc.util.Pair<Expr,wyc.builder.FlowTypeChecker.Environment>	propagateCondition(Expr expr, boolean sign, wyc.builder.FlowTypeChecker.Environment environment, WhileyFile.Context context) Propagate type information through an expression being used as a condition, whilst checking it is well-typed at the same time.
wycc.util.Pair<Constant,Type>	resolveAsConstant(Expr e, WhileyFile.Context context) Resolve a given constant expression as a constant value.
wycc.util.Pair<Constant,Type>	resolveAsConstant(wybs.lang.NameID nid) Resolve a given name as a constant value.
wycc.util.Triple<wybs.lang.NameID,Type.FunctionOrMethod,List<String>>	resolveAsFunctionOrMethod(wybs.lang.NameID nid, List<Type> parameters, List<String> lifetimeArgs, WhileyFile.Context context, wyc.builder.FlowTypeChecker.Environment environment) Responsible for determining the true type of a method or function being invoked.
wycc.util.Triple<wybs.lang.NameID,Type.FunctionOrMethod,List<String>>	resolveAsFunctionOrMethod(String name, List<Type> parameters, List<String> lifetimeArgs, WhileyFile.Context context, wyc.builder.FlowTypeChecker.Environment environment) Responsible for determining the true type of a method or function being invoked.
wycc.util.Triple<wybs.lang.NameID,Type.FunctionOrMethod,List<String>>	resolveAsFunctionOrMethod(String name, WhileyFile.Context context, wyc.builder.FlowTypeChecker.Environment environment) Responsible for determining the true type of a method or function being invoked.
Type.FunctionOrMethod	resolveAsType(wyal.lang.WyalFile.Type.FunctionOrMethodOrProperty t, WhileyFile.Context context)
Type.Function	resolveAsType(wyal.lang.WyalFile.Type.Function t, WhileyFile.Context context)
Type.Method	resolveAsType(wyal.lang.WyalFile.Type.Method t, WhileyFile.Context context)
Type.Property	resolveAsType(wyal.lang.WyalFile.Type.Property t, WhileyFile.Context context)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

FlowTypeChecker

public FlowTypeChecker(CompileTask builder)

Method Detail

propagate

public void propagate(List<WhileyFile> files)

propagate

public void propagate(WhileyFile wf)

propagate

public void propagate(WhileyFile.Type td)
               throws IOException

Resolve types for a given type declaration. If an invariant expression is given, then we have to propagate and resolve types throughout the expression.

Parameters:

td - Type declaration to check.

Throws:

IOException

propagate

public void propagate(WhileyFile.Constant cd)
               throws IOException,
                      wybs.util.ResolveError

Propagate and check types for a given constant declaration.

Parameters:

cd - Constant declaration to check.

Throws:

IOException

wybs.util.ResolveError

propagate

public void propagate(WhileyFile.FunctionOrMethodOrProperty d)
               throws IOException

Propagate and check types for a given function or method declaration.

Parameters:

fd - Function or method declaration to check.

Throws:

IOException

propagateCondition

public wycc.util.Pair<Expr,wyc.builder.FlowTypeChecker.Environment> propagateCondition(Expr expr,
                                                                                       boolean sign,
                                                                                       wyc.builder.FlowTypeChecker.Environment environment,
                                                                                       WhileyFile.Context context)
                                                                                throws wybs.util.ResolveError

Propagate type information through an expression being used as a condition, whilst checking it is well-typed at the same time. When used as a condition (e.g. of an if-statement) an expression may update the environment in accordance with any type tests used within. This is important to ensure that variables are retyped in e.g. if-statements. For example:

 if x is int && x >= 0
    // x is int
 else:
    //
 

Here, the if-condition must update the type of x in the true branch, but *cannot* update the type of x in the false branch.

To handle conditions on the false branch, this function uses a sign flag rather than expanding them using DeMorgan's laws (for efficiency). When determining type for the false branch, the sign flag is initially false. This prevents falsely concluding that e.g. "x is int" holds in the false branch.

Parameters:

expr - Condition expression to type check and propagate through

sign - Indicates how expression should be treated. If true, then expression is treated "as is"; if false, then expression should be treated as negated

environment - Determines the type of all variables immediately going into this expression

context - Enclosing context of this expression (e.g. type declaration, function declaration, etc)

Returns:

Throws:

wybs.util.ResolveError - If a named type within this condition cannot be resolved within the enclosing project.

propagate

public Expr propagate(Expr expr,
                      wyc.builder.FlowTypeChecker.Environment environment,
                      WhileyFile.Context context)

Propagate types through a given expression, whilst checking that it is well typed. In this case, any use of a runtime type test cannot effect callers of this function.

Parameters:

expr - Expression to propagate types through.

environment - Determines the type of all variables immediately going into this expression

context - Enclosing context of this expression (e.g. type declaration, function declaration, etc)

Returns:

resolveAsFunctionOrMethod

public wycc.util.Triple<wybs.lang.NameID,Type.FunctionOrMethod,List<String>> resolveAsFunctionOrMethod(wybs.lang.NameID nid,
                                                                                                       List<Type> parameters,
                                                                                                       List<String> lifetimeArgs,
                                                                                                       WhileyFile.Context context,
                                                                                                       wyc.builder.FlowTypeChecker.Environment environment)
                                                                                                throws IOException,
                                                                                                       wybs.util.ResolveError

Responsible for determining the true type of a method or function being invoked. To do this, it must find the function/method with the most precise type that matches the argument types.

Parameters:

nid -

parameters -

lifetimeArgs - --- lifetime arguments passed on method invocation, or null if none are passed and the compiler has to figure it out

Returns:

nameid, type, given/inferred lifetime arguments

Throws:

IOException

wybs.util.ResolveError

resolveAsFunctionOrMethod

public wycc.util.Triple<wybs.lang.NameID,Type.FunctionOrMethod,List<String>> resolveAsFunctionOrMethod(String name,
                                                                                                       WhileyFile.Context context,
                                                                                                       wyc.builder.FlowTypeChecker.Environment environment)
                                                                                                throws IOException,
                                                                                                       wybs.util.ResolveError

Responsible for determining the true type of a method or function being invoked. In this case, no argument types are given. This means that any match is returned. However, if there are multiple matches, then an ambiguity error is reported.

Parameters:

name - --- function or method name whose type to determine.

context - --- context in which to resolve this name.

Returns:

Throws:

IOException

wybs.util.ResolveError

resolveAsFunctionOrMethod

public wycc.util.Triple<wybs.lang.NameID,Type.FunctionOrMethod,List<String>> resolveAsFunctionOrMethod(String name,
                                                                                                       List<Type> parameters,
                                                                                                       List<String> lifetimeArgs,
                                                                                                       WhileyFile.Context context,
                                                                                                       wyc.builder.FlowTypeChecker.Environment environment)
                                                                                                throws IOException,
                                                                                                       wybs.util.ResolveError

Responsible for determining the true type of a method or function being invoked. To do this, it must find the function/method with the most precise type that matches the argument types.

Parameters:

name - --- name of function or method whose type to determine.

parameters - --- required parameter types for the function or method.

lifetimeArgs - --- lifetime arguments passed on method invocation, or null if none are passed and the compiler has to figure it out

context - --- context in which to resolve this name.

Returns:

nameid, type, given/inferred lifetime arguments

Throws:

IOException

wybs.util.ResolveError

applySubstitution

public static Type applySubstitution(List<String> lifetimeParameters,
                                     List<String> lifetimeArguments,
                                     Type original)

Apply a lifetime substitution: Substitute all parameters in original by their arguments.

Parameters:

lifetimeParameters -

lifetimeArguments -

original -

Returns:

resolveAsType

public Type.Function resolveAsType(wyal.lang.WyalFile.Type.Function t,
                                   WhileyFile.Context context)
                            throws IOException

Throws:

IOException

resolveAsType

public Type.Method resolveAsType(wyal.lang.WyalFile.Type.Method t,
                                 WhileyFile.Context context)
                          throws IOException

Throws:

IOException

resolveAsType

public Type.Property resolveAsType(wyal.lang.WyalFile.Type.Property t,
                                   WhileyFile.Context context)
                            throws IOException

Throws:

IOException

resolveAsType

public Type.FunctionOrMethod resolveAsType(wyal.lang.WyalFile.Type.FunctionOrMethodOrProperty t,
                                           WhileyFile.Context context)
                                    throws IOException

Throws:

IOException

resolveAsConstant

public wycc.util.Pair<Constant,Type> resolveAsConstant(wybs.lang.NameID nid)
                                                throws IOException,
                                                       wybs.util.ResolveError

Resolve a given name as a constant value. This is a global problem, since a constant declaration in one source file may refer to constants declared in other compilation units. This function will actually evaluate constant expressions (e.g. "1+2") to produce actual constant vales.

Constant declarations form a global graph spanning multiple compilation units. In resolving a given constant, this function must traverse those portions of the graph which make up the constant. Constants are not permitted to be declared recursively (i.e. in terms of themselves) and this function will report an error is such a recursive cycle is detected in the constant graph.

Parameters:

nid - Fully qualified name identifier of constant to resolve

Returns:

Constant value representing named constant

Throws:

IOException

wybs.util.ResolveError

resolveAsConstant

public wycc.util.Pair<Constant,Type> resolveAsConstant(Expr e,
                                                       WhileyFile.Context context)

Resolve a given constant expression as a constant value. A constant expression is one which refers only to known and visible constant values, rather than e.g. local variables. Constant expressions may still use operators (e.g. "1+2", or "1+c" where c is a declared constant).

Constant expressions used in a few places in Whiley. In particular, the cases of a switch statement must be defined using constant expressions.

Parameters:

e -

context -

Returns:

expandAsEffectiveArray

public Type.EffectiveArray expandAsEffectiveArray(Expr src,
                                                  WhileyFile.Context context)
                                           throws IOException,
                                                  wybs.util.ResolveError

Throws:

IOException

wybs.util.ResolveError

expandAsEffectiveArray

public Type.EffectiveArray expandAsEffectiveArray(Type type,
                                                  wybs.lang.SyntacticElement element,
                                                  WhileyFile.Context context)
                                           throws IOException,
                                                  wybs.util.ResolveError

Throws:

IOException

wybs.util.ResolveError

expandAsEffectiveRecord

public Type.EffectiveRecord expandAsEffectiveRecord(Expr src,
                                                    WhileyFile.Context context)
                                             throws IOException,
                                                    wybs.util.ResolveError

Throws:

IOException

wybs.util.ResolveError

expandAsEffectiveRecord

public Type.EffectiveRecord expandAsEffectiveRecord(Type type,
                                                    wybs.lang.SyntacticElement element,
                                                    WhileyFile.Context context)
                                             throws IOException,
                                                    wybs.util.ResolveError

Throws:

IOException

wybs.util.ResolveError

expandAsEffectiveReference

public Type.Reference expandAsEffectiveReference(Expr src,
                                                 WhileyFile.Context context)
                                          throws IOException,
                                                 wybs.util.ResolveError

Throws:

IOException

wybs.util.ResolveError

expandAsEffectiveReference

public Type.Reference expandAsEffectiveReference(Type type,
                                                 wybs.lang.SyntacticElement element,
                                                 WhileyFile.Context context)
                                          throws IOException,
                                                 wybs.util.ResolveError

Throws:

IOException

wybs.util.ResolveError

expandAsEffectiveFunctionOrMethod

public Type.FunctionOrMethod expandAsEffectiveFunctionOrMethod(Expr src,
                                                               WhileyFile.Context context)
                                                        throws IOException,
                                                               wybs.util.ResolveError

Throws:

IOException

wybs.util.ResolveError

expandAsEffectiveFunctionOrMethod

public Type.FunctionOrMethod expandAsEffectiveFunctionOrMethod(Type type,
                                                               wybs.lang.SyntacticElement element,
                                                               WhileyFile.Context context)
                                                        throws IOException,
                                                               wybs.util.ResolveError

Throws:

IOException

wybs.util.ResolveError