wyil.lang

Class Bytecode.Loop

java.lang.Object

wyil.util.AbstractBytecode

wyil.lang.Bytecode.Loop

All Implemented Interfaces:

Bytecode, Bytecode.Stmt

Direct Known Subclasses:

Bytecode.DoWhile, Bytecode.While

Enclosing interface:

Bytecode

public abstract static class Bytecode.Loop
extends AbstractBytecode
implements Bytecode.Stmt

A loop bytecode has the following layout:

 +--------+-----------+--------------+------------+------+
 | opcode | condition | invariants[] | modified[] | body |
 +--------+-----------+--------------+------------+------+
 

Here, the condition identifies the loop condition which, when false, will cause the loop to terminate. The invariants identifies zero or more operands which must be true on every iteration of the loop. The modified variables are those variables which are, in some sense, modified in the body of the loop. The body identifies a block which forms the body of the loop.

Nested Class Summary

Nested classes/interfaces inherited from interface wyil.lang.Bytecode

Bytecode.AliasDeclaration, Bytecode.Assert, Bytecode.AssertOrAssume, Bytecode.Assign, Bytecode.Assume, Bytecode.Block, Bytecode.Blocks, Bytecode.Break, Bytecode.Case, Bytecode.Const, Bytecode.Continue, Bytecode.Convert, Bytecode.Debug, Bytecode.DoWhile, Bytecode.Expr, Bytecode.Extras, Bytecode.Fail, Bytecode.FieldLoad, Bytecode.If, Bytecode.Index, Bytecode.IndirectInvoke, Bytecode.Invoke, Bytecode.Lambda, Bytecode.Loop, Bytecode.NamedBlock, Bytecode.OperandGroups, Bytecode.Operands, Bytecode.Operator, Bytecode.OperatorKind, Bytecode.Quantifier, Bytecode.QuantifierKind, Bytecode.Range, Bytecode.Return, Bytecode.Schema, Bytecode.Skip, Bytecode.Stmt, Bytecode.StmtExpr, Bytecode.Switch, Bytecode.Util, Bytecode.VariableAccess, Bytecode.VariableDeclaration, Bytecode.While

Field Summary

Fields inherited from class wyil.util.AbstractBytecode

schemas

Fields inherited from interface wyil.lang.Bytecode

BINARY_ASSIGNABLE, BINARY_OPERATOR, NARY_ASSIGNABLE, OPCODE_add, OPCODE_aliasdecl, OPCODE_all, OPCODE_array, OPCODE_arraygen, OPCODE_arrayindex, OPCODE_arraylength, OPCODE_assert, OPCODE_assign, OPCODE_assume, OPCODE_bitwiseand, OPCODE_bitwiseinvert, OPCODE_bitwiseor, OPCODE_bitwisexor, OPCODE_block, OPCODE_break, OPCODE_const, OPCODE_continue, OPCODE_convert, OPCODE_debug, OPCODE_dereference, OPCODE_div, OPCODE_dowhile, OPCODE_eq, OPCODE_fail, OPCODE_fieldload, OPCODE_ge, OPCODE_gt, OPCODE_if, OPCODE_ifelse, OPCODE_ifis, OPCODE_indirectinvoke, OPCODE_invoke, OPCODE_is, OPCODE_lambda, OPCODE_le, OPCODE_logicaland, OPCODE_logicalnot, OPCODE_logicalor, OPCODE_lt, OPCODE_mul, OPCODE_namedblock, OPCODE_ne, OPCODE_neg, OPCODE_newobject, OPCODE_record, OPCODE_rem, OPCODE_return, OPCODE_shl, OPCODE_shr, OPCODE_skip, OPCODE_some, OPCODE_sub, OPCODE_switch, OPCODE_varcopy, OPCODE_vardecl, OPCODE_vardeclinit, OPCODE_varmove, OPCODE_while, UNARY_ASSIGNABLE, UNARY_OPERATOR

Constructor Summary

Constructors

Constructor and Description
Loop(int body, int condition, int[] invariants, int[] modified)

Method Summary

Modifier and Type	Method and Description
int	body() Return the block identifier of the loop body.
int	condition() Return the loop condition operand.
int[]	invariants() Return the array of operands making up the loop invariant.
int[]	modifiedVariables() Return the array of modified variables which are those assigned (in some way) in the body of the loop.

Methods inherited from class wyil.util.AbstractBytecode

equals, getBlock, getBlocks, getOpcode, getOperand, getOperandGroup, getOperands, hashCode, numberOfBlocks, numberOfOperandGroups, numberOfOperands

Methods inherited from class java.lang.Object

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

Methods inherited from interface wyil.lang.Bytecode.Stmt

getBlock, getBlocks, numberOfBlocks

Methods inherited from interface wyil.lang.Bytecode

getOpcode, getOperand, getOperandGroup, getOperands, numberOfOperandGroups, numberOfOperands

Constructor Detail

Loop

public Loop(int body,
            int condition,
            int[] invariants,
            int[] modified)

Method Detail

body

public int body()

Return the block identifier of the loop body.

Returns:

condition

public int condition()

Return the loop condition operand. This must be true for iteration to continue around the loop.

Returns:

invariants

public int[] invariants()

Return the array of operands making up the loop invariant. Each of these corresponds to a "where" clause in the original program.

Returns:

modifiedVariables

public int[] modifiedVariables()

Return the array of modified variables which are those assigned (in some way) in the body of the loop. These cannot be operands, they must be variables. These are needed for verification.