wyc.builder

Class CodeGenerator

java.lang.Object

wyc.builder.CodeGenerator

public final class CodeGenerator
extends Object

Responsible for compiling the declarations, statements and expression found in a WhileyFile into WyIL declarations and bytecode blocks. For example:

 type nat is (int x) where x >= 0

 function f(nat x) -> int:
    return x-1
 

The code generator is responsible for generating the code for the constraint on nat, as well as compiling the function's statements into their corresponding WyIL bytecodes. For example, the code generated constraint on type nat would look like this:

 type nat is int
 where:
     load x
     const 0
     ifge goto exit
     fail("type constraint not satisfied")
  .exit:
 

This WyIL bytecode simply compares the local variable x against 0. Here, x represents the value held in a variable of type nat. If the constraint fails, then the given message is printed.

Author:

David J. Pearce

Constructor Summary

Constructors

Constructor and Description
CodeGenerator(CompileTask builder) Construct a code generator object for translating WhileyFiles into WyilFiles.

Method Summary

Modifier and Type	Method and Description
static String	freshLabel()
WyilFile	generate(WhileyFile whileyFile, wyfs.lang.Path.Entry<WyilFile> target) Generate a WyilFile from a given WhileyFile by translating all of the declarations, statements and expressions into WyIL declarations and bytecode blocks.
wyc.builder.CodeGenerator.FlowResult	generateAndCondition(Expr.BinOp condition, wyc.builder.CodeGenerator.EnclosingScope scope) Translate a source-level conjunction into a sequence of WyIL bytecodes.
int	generateAsStmt(Expr.FunctionOrMethodCall expr, wyc.builder.CodeGenerator.EnclosingScope scope) Generate an invoke expression as a statement.
int	generateAsStmt(Expr.IndirectFunctionOrMethodCall expr, wyc.builder.CodeGenerator.EnclosingScope scope) Generate an indirect invoke expression as a statement.
wyc.builder.CodeGenerator.FlowResult	generateCondition(Expr condition, wyc.builder.CodeGenerator.EnclosingScope scope) Translate a source-level conditional expression into WyIL bytecodes, using a given scope mapping named variables to locations.
int	generateExpression(Expr expression, wyc.builder.CodeGenerator.EnclosingScope scope) Translate a source-level expression into a WYIL bytecode block, using a given environment mapping named variables to registers.
int	generateFunctionOrMethodCall(Expr.FunctionOrMethodCall expr, wyc.builder.CodeGenerator.EnclosingScope scope)
int	generateIndirectFunctionOrMethodCall(Expr.IndirectFunctionOrMethodCall expr, wyc.builder.CodeGenerator.EnclosingScope scope)
wyc.builder.CodeGenerator.FlowResult	generateIsCondition(Expr.BinOp condition, wyc.builder.CodeGenerator.EnclosingScope scope) Translate a source-level type test.
int[]	generateMultipleReturns(List<Expr> expressions, wyc.builder.CodeGenerator.EnclosingScope scope) Translate a source-level expression into a WyIL bytecode block, using a given environment mapping named variables to registers.
wyc.builder.CodeGenerator.FlowResult	generateNotCondition(Expr.UnOp condition, wyc.builder.CodeGenerator.EnclosingScope scope)
wyc.builder.CodeGenerator.FlowResult	generateOrCondition(Expr.BinOp condition, wyc.builder.CodeGenerator.EnclosingScope scope) Translate a source-level disjunction into a sequence of WyIL bytecodes.
List<Integer>	toIntegerList(int... items)

Methods inherited from class java.lang.Object

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

Constructor Detail

CodeGenerator

public CodeGenerator(CompileTask builder)

Construct a code generator object for translating WhileyFiles into WyilFiles.

Parameters:

builder - The enclosing builder instance which provides access to the global namespace.

Method Detail

generate

public WyilFile generate(WhileyFile whileyFile,
                         wyfs.lang.Path.Entry<WyilFile> target)

Generate a WyilFile from a given WhileyFile by translating all of the declarations, statements and expressions into WyIL declarations and bytecode blocks.

Parameters:

whileyFile - The WhileyFile to be translated.

Returns:

generateAsStmt

public int generateAsStmt(Expr.FunctionOrMethodCall expr,
                          wyc.builder.CodeGenerator.EnclosingScope scope)
                   throws wybs.util.ResolveError

Generate an invoke expression as a statement. There are only limited cases where this can arise. In particular, when a method is invoked and the return value is ignored. In such case, we generate an assignment with and empty left-hand side.

Parameters:

expr - The expression to be translated as a statement

scope - The enclosing scope of the expression

Throws:

wybs.util.ResolveError

generateAsStmt

public int generateAsStmt(Expr.IndirectFunctionOrMethodCall expr,
                          wyc.builder.CodeGenerator.EnclosingScope scope)
                   throws wybs.util.ResolveError

Generate an indirect invoke expression as a statement. There are only limited cases where this can arise. In particular, when a method is invoked and the return value is ignored. In such case, we generate an assignment with and empty left-hand side.

Parameters:

expr - The expression to be translated as a statement

scope - The enclosing scope of the expression

Throws:

wybs.util.ResolveError

generateCondition

public wyc.builder.CodeGenerator.FlowResult generateCondition(Expr condition,
                                                              wyc.builder.CodeGenerator.EnclosingScope scope)
                                                       throws wybs.util.ResolveError

Translate a source-level conditional expression into WyIL bytecodes, using a given scope mapping named variables to locations. This produces a location index, and updates two environments which represent two sides of the same coin.

Parameters:

condition -

scope -

Returns:

A flow result where both true and false scopes are unaliased.

Throws:

wybs.util.ResolveError

generateAndCondition

public wyc.builder.CodeGenerator.FlowResult generateAndCondition(Expr.BinOp condition,
                                                                 wyc.builder.CodeGenerator.EnclosingScope scope)
                                                          throws wybs.util.ResolveError

Translate a source-level conjunction into a sequence of WyIL bytecodes. The key challenge here is to correctly propagate the scope information into the lhs and rhs. Since the rhs is only executed when the lhs holds, we use the "true scope" from the lhs when translating the rhs. For example:

 x is int && x >= 0
 

Here, the true scope coming out of the lhs will identify x with type int. This is necessary for the rhs to make sense. Observe that this is exploiting the fact that operators have short circuiting behaviour in Whiley.

Parameters:

condition - Condition being translated

scope - Enclosing scope going into this condition.

Returns:

Throws:

wybs.util.ResolveError

generateOrCondition

public wyc.builder.CodeGenerator.FlowResult generateOrCondition(Expr.BinOp condition,
                                                                wyc.builder.CodeGenerator.EnclosingScope scope)
                                                         throws wybs.util.ResolveError

Translate a source-level disjunction into a sequence of WyIL bytecodes. The key challenge here is to correctly propagate the scope information into the lhs and rhs. Since the rhs is only executed when the lhs doesn't hold, we use the "false scope" from the lhs when translating the rhs. For example:

 x is null || x >= 0
 

Here, assume x is declared with type int|null. Then, the false scope coming out of the lhs will identify x with type int. This is necessary for the rhs to make sense. Observe that this is exploiting the fact that operators have short circuiting behaviour in Whiley.

Parameters:

condition - Condition being translated

scope - Enclosing scope going into this condition.

Returns:

Throws:

wybs.util.ResolveError

generateIsCondition

public wyc.builder.CodeGenerator.FlowResult generateIsCondition(Expr.BinOp condition,
                                                                wyc.builder.CodeGenerator.EnclosingScope scope)
                                                         throws wybs.util.ResolveError

Translate a source-level type test. This produces two potentially updated scopes, one for the true branch and one for the false branch. In the case of a variable being retyped, then the true branch contains the updated type whilst the false branch contains the negated type. For example:

 x is int
 

Assum x is declared with type int|null. Then on the true branch x has type int&(int|null) which reduces to int. And, on the false branch, x has type !int&(int|null) which reduces to null.

Parameters:

condition -

scope -

Returns:

Throws:

wybs.util.ResolveError

generateNotCondition

public wyc.builder.CodeGenerator.FlowResult generateNotCondition(Expr.UnOp condition,
                                                                 wyc.builder.CodeGenerator.EnclosingScope scope)
                                                          throws wybs.util.ResolveError

Throws:

wybs.util.ResolveError

generateMultipleReturns

public int[] generateMultipleReturns(List<Expr> expressions,
                                     wyc.builder.CodeGenerator.EnclosingScope scope)
                              throws wybs.util.ResolveError

Translate a source-level expression into a WyIL bytecode block, using a given environment mapping named variables to registers. This expression may generate zero or more results.

Parameters:

expression -

scope -

Returns:

Throws:

wybs.util.ResolveError

generateExpression

public int generateExpression(Expr expression,
                              wyc.builder.CodeGenerator.EnclosingScope scope)

Translate a source-level expression into a WYIL bytecode block, using a given environment mapping named variables to registers. The result of the expression is stored in a given target register.

Parameters:

expression - --- Source-level expression to be translated

scope - --- Enclosing scope of the condition

Returns:

--- the register

generateFunctionOrMethodCall

public int generateFunctionOrMethodCall(Expr.FunctionOrMethodCall expr,
                                        wyc.builder.CodeGenerator.EnclosingScope scope)
                                 throws wybs.util.ResolveError

Throws:

wybs.util.ResolveError

generateIndirectFunctionOrMethodCall

public int generateIndirectFunctionOrMethodCall(Expr.IndirectFunctionOrMethodCall expr,
                                                wyc.builder.CodeGenerator.EnclosingScope scope)
                                         throws wybs.util.ResolveError

Throws:

wybs.util.ResolveError

toIntegerList

public List<Integer> toIntegerList(int... items)

freshLabel

public static String freshLabel()