michareiser / eschecker Goto Github PK

Type inference should support function calls. The implementation will use inlining of the function calls to replicate the whole context of the call side.

This change does not include support for this, apply, call or anonymous functions.

Symbol Table

The symbol extracter creates symbols for members in the enclosing scope instead of appending them to the symbol of which they are a member of. A symbol for each identifier is required to be able to resolve the type for a symbol when performing the type inference. Therefore every member
needs a unique symbol too.

The problem with the current implementation is, that the identifier always creates an entry in the scope and always tries to resolve the identifier from the scope, ignoring
where the identifier is used. So maybe it would be the best if the visitor does not use an explicit identifier handler and instead checks very identifiers can be used, e.g. in functions, classes, variable declarations, member expressions and so on.

The symbol table contains a symbol for each possible symbol and therefore might not be too precise.
The symbol table does not support aliasing.

Implement a structure that can represent a control flow graph.

The current implementation of type is mutable. For the data flow analysis, a immutable type implementation is required for a distinct type environment between each CFG node (an alternative is to copy the state between the cfg nodes, this requires a lot of copying). This requires that the substitution of types can no longer be performed by setting up an object chain with resolvesTo and depending on reference equality. Instead a new identifier needs to be introduced that uniquely identifies a type in a type environment.

Therefor each type get a new unique id (use _.uniqueId) and implements the substitute(old, newT) function. The substitute function replaced all occurrences of the old type in this with the newT type.
The TypeEnvironment and RefinementContext needs to have a substitute function to that substitutes a type in the whole type environment

Crate a intra procedural CFG that supports the following statements

• ExpressionStatement, BlockStatement, EmptyStatement, VariableDeclaration
• if
• while
• for loop
• for in / for of
• do while
• Switch
• Function declarations
• try & catch & finally
• classes
• LabeledStatement

The analyzer should detect read and write operations to undefined variables. The following simple examples should result in an error:

console.log(x);

x = 10;

The analyzer should also report errors when a variable is accessed before it is defined.

console.log(x);
const x = 10;

console.log(y);
let y = 9;

The analyzer should tread let and var definitions the same way as accessing variables before their declaration is considered as bad practice and might lead to confusing results.

Instead of throwing an exception if unification fails or for soft failures during refinement (e.g. not when something is not implemented, but potentially nullpointer) add an error object to the context and collect all errors.

This means some assumptions are required when unification has failed. To reduce follow up errors, return Any in case the unification has failed.

Add support for IF-Statements to the type Inference algorithm. The following edge cases need to be
supported, as they are widely used.

Type inference needs to be branch specific

function (x) {
  if (typeof(x) === 'string') { // inside the branch x is of type string
    x = parseInt(x, 10); // type changes from string to int
  }
  return x * x; // the type of x is always number
}

The possible types of a variable after an if statement need to be the most common between all branches

if (y > 10) {
  x = 10;  // x is typeof number
else {
  x = null; // x is typeof Null
}

return x + 10; // x is typeof Maybe<number>

variables defined in the outer scope are available in inner scopes. Variables defined in inner scopes are not available in outer scopes

OK

const x = 10;
function test () {
  console.log(x);
}

ERROR

console.log(x);
function test() {
    const x = 10;
}

The type inference algorithm needs to support structural types, also known as record types. The order in which the record type properties occur is not important.

A record type defines the shape of an object literal, but is not used to describe classes, even if both semantics are very similar. The important difference is that classes use nominal typing (subtyping is not given by having the same structure).

A record type is defined as

record = propList
probList = prop | prop propList
prop = name : t

where a property has a label (it's name) and a type.

Unification:
The unification of the record types is a new record type that contains the properties of both types.
The unification (or subtyping) for type S and T fails if S does not contain at least the properties of T or where the property types cannot be unified. The order of the property names doesn't matter. To simplify the ordering it's suggested to keep an ordered Set with the property names in a record.

Involved expressions:

• Object Literal
• Assignment Expression where the left hand side is a PropertyExpression

Tasks

• Extending Symbol extraction algorithm for object literals

• Definition of record type. The record type needs to override equals as the equality of a record type is not given by just comparing the parameter types.

• Adding refinement rule for object literals and adjusting the assignment expression refinement rule.

• The unification rule for same types needs to be extracted or adjusted so that it does not apply for Records. Records unification is not only based on the type parameter but also with the associated names.

  Implementing the unification of record types

Record types can only be unified with other record types or with null, which leads to Maybe

The current implementation defines the left and right parameter type as any to allow arbitrary left and right hand sides of the operator. This results in an inferred any type for the left and right hand side ignoring what ever the type has been before as the unification of any and T always results in any.

The == and != should allow an arbitrary left or right hand side parameter type but should not have any effect on the types of them.

A basic support for try-catch-finally statement in the control flow graph have been implemented with #19. The implementation fails when more complex structures are used. This issue should be used to track the pending tasks needed to have a full support for try-catch-finally-statements. The current implementation only supports a subset as I think that try statements are not that common in javascript code (except maybe in unit testing frameworks).

The current control flow graph construction terminates when a continue, return or break statement is used inside a try-finally statement. Supporting these cases is non trivial and requires additional tracking that is not present at the moment. The problematic can be explained at the following code

while(x) {
    try {
        try {
            break;
        } catch (a) {
        } finally {
            foo();
        }
        fooFollow();
    } catch (b) {
        console.log("Error");
    } finally {
        bar();
    }
    barFollow();
}
END();

The successor of the break statement is not as usual the while statement itself, instead the first finally handler is the direct successor. This also means that the finally statement of the inner try statement needs an UNCONDITIONAL edge to the finally statement of the outer edge as the finally. And the outer finally needs an edge to the while loop to model the break statement correctly.

In this turn, the mayThrowException function in the cfg-builder should be revised to check if all expressions that might throw an exception are listed.