GitHub/avmplus
1
0 Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Files
master
avmplus/doc/verifier.html
T
dmcallis 65a0592776 Initial source code drop 
Source code drop for the Actionscript virtual machine in the Adobe
Flash Player for December 2013
2013-12-02 16:04:04 -08:00

1335 lines
31 KiB
HTML
Raw Permalink Blame History

<!-- This Source Code Form is subject to the terms of the Mozilla Public
- License, v. 2.0. If a copy of the MPL was not distributed with this
- file, You can obtain one at http://mozilla.org/MPL/2.0/. -->
<h1>Notes on the AVM Bytecode Verifier</h1>
Jeff Dyer, Adobe Systems
<hr>
<pre>
Revision History:
November 26, 2008: second draft, reviewed by Tom and Lars
November 20, 2008: initial draft, not reviewed
Known Problems:
- certain abstract operations are yet to be defined
- handling of null as a type modifier
- dead code is not ignored as it is in AVM
- more and better examples of verification errors and their resolution
</pre>
<hr>
<h2>Introduction</h2>
<P><span class="pcounter"></span>ABC (originally for Action Block Code) is the language executed by the AVM (ActionScript
Virtual Machine of Tamarin). The full definition of ABC includes a specification of its
syntax, static semantics and runtime behavior. Within the static semantics are
constraints on the bytecode of each executed method (methods that are not
executed are not subject to these constraints.) A bytecode verifier is the mechanism
that enforces such static constraints on sequences of bytecode.
<P><span class="pcounter"></span>This document describes the AVM bytecode verifier using an abstract machine and
the translation of concrete ABC instructions into operations of that abstract machine.
The abstract machine described here accepts the same set of programs that the AVM verifier
accepts. This is the set of ABC programs that is allowed to be executed by the AVM.
<P><span class="pcounter"></span>This document does not describe the syntactic or structural constraints on ABC files
that do not involve ABC bytecode. Those rules are defined in the AVM2 Overview [3] and elsewhere.
<P><span class="pcounter"></span>The audience for this document includes developers who are working on and
compiler writers who are targeting the AVM. The reader might find helpful to think of
this as an alternative interpretation of ABC programs; that is, to not
confuse the meaning of types and control flow with that of a particular source
language or even the dynamic behavior of the ABC instructions.
<h2>Invariants</h2>
<P><span class="pcounter"></span>
The following invariants are checked during verification:
<ul>
<li> Operand stack does not underflow or overflow
<li> Scope stack does not underflow or overflow
<li> Storage locations always have an unambiguous state
<li> Instruction operands are valid references and have their expected types
<li> Instruction pointers point to the beginning of an instruction
<li> Constant pool indices point to valid constant pool entries
</ul>
<P><span class="pcounter"></span>There are many other constraints on the syntax and semantics of an ABC file. For
example it is essential that
<ul>
<li> Base classes exist and are not declared 'final'
<li> Class methods that are overridden are not declared 'final'
<li> ...more here
</ul>
<P><span class="pcounter"></span>Such constraints are assumed by this spec to have been checked before bytecode
verification.
<h2>Abstract Machine</h2>
<h3>Machine State</h3>
<P><span class="pcounter"></span>The abstract machine state includes the following components:
<ul>
<li> Operand stack of a maximum size containing zero or more types
<li> Scope stack of a maximum size containing one or more types
<li> Local registers of a maximum size, each containing a type
<li> Index of the current instruction
</ul>
<P><span class="pcounter"></span>We refer to stack elements and local registers as locations in the machine state.
A valid machine state is one whose stack sizes and type of each location are known
to be consistent when reached by all possible control flow paths. A valid bytecode
sequence is one with only valid machine states.
<P><span class="pcounter"></span>Accessible locations are initialized to the type Any and so are never in an undefined
(or killed) state.
<h3>Machine Context</h3>
<P><span class="pcounter"></span>
In addition to the state that is mutated in the course of method verification, there is
additional state that represents the context of the method. That environment
includes:
<ul>
<li> Method being verfied including method body and map of machine states for that method
<li> Lexically visible bindings (name to type) outside the method
<li> Constant pool
<li> Script domain (contains top-level fixed definitions)
</ul>
<h3>Machine Types</h3>
<P><span class="pcounter"></span>
The verifier type system is factored somewhat differently than that of ActionScript or
any other normal object oriented language, for that matter. The key difference is
that there are six root types, none of which are compatible with any of the others.
ActionScript, in contrast, has one root type Any with which all other types are
assignment compatible. The reason for this deviation is that the verifier type system
reflects the compatibility rules of the underlying machine values.
<P><span class="pcounter"></span>
The root types of the abstract machine are:
<ul>
<li> Atom* (consists of Any, Undefined, Object)
<li> Int*
<li> UInt*
<li> Boolean*
<li> Number*
<li> Reference* (consists of Null and any sub-class of Object, including String and
Namespace)
</ul>
<p class="note"><b>NOTE</b>&nbsp;&nbsp; String and Namespace are special in that there are instructions that expect
those types, but otherwise they are treated as all other Reference* types.
<P><span class="pcounter"></span>
Two types are considered consistent if they are the same machine type and they
merge to a concrete type that is the same machine type. We use the term 'type' to
refer to both a machine types (e.g. Atom*) and the concrete types (e.g. Any and
Object) without qualification unless the distinction is important and unclear.
<P><span class="pcounter"></span>
The rules for merging types are:
<ul>
<li> Two identical types merge as the same type
<li> Two Atom* types merge as type Any
<li> Two Reference* types merge as the type that is the most derived common
base class. Two Reference* types are consistent only if they merge to another
Reference* type (i.e. not Object)
<li> All other type combinations result in a merge error
</ul>
<h3>Abstract Operators</h3>
<P><span class="pcounter"></span>
The following operators are the primitives that define possible state transitions of the
abstract machine.
<ul>
<li> Push type
<li> Pop [count]
<li> Coerce type
<li> Check type [index]
<li> Peek symbol [index]
<li> Swap
<li> Load index
<li> Store index
<li> PushScope type
<li> PopScope
<li> Jump offset
<li> Throws
<li> PopName
<li> FindName
<li> FindDefName
<li> GetSlot
<li> GetProp
<li> SetSlot
<li> SetProp
</ul>
<P><span class="pcounter"></span>
<b>Push <i>type</i></b>. Push the specified type onto the operand stack. Raises an error if the
number of elements on the operand stack is equal to the maximum stack size.
<P><span class="pcounter"></span>
<b>Pop <i>[count]</i></b>. Pop count types from the operand stack. If unspecified count is 1.
Raises an error if count is greater than the number of elements on the operand
stack.
<P><span class="pcounter"></span>
<b>Coerce <i>type</i></b>. Change the type on the top of the stack to the given type. Raises no
error.
<P><span class="pcounter"></span>
<b>Check <i>type [index]</i></b>. Check that the type at the location of index is of the given
type. If index is not provided, then check the type on the top of the stack. Raises an
error if index does not indicate a valid location or if the type at that location is not
compatible with the specified type.
<P><span class="pcounter"></span>
<b>Peek <i>symbol [index]</i></b>. Bind meta-name symbol to the type at the location of index.
If index is not provided, then binds the type on the top of the operand stack. Raises an
error if index does not indicate a valid location.
<P><span class="pcounter"></span>
<b>Swap</b>. Swap the two values on the top of the operand stack. Raises an error if fewer
than two elements are on the operand stack.
<P><span class="pcounter"></span>
<b>Load <i>index</i></b>. Load the type of local at index onto the stack. Raises an error if index
does not indicate a valid local register.
<P><span class="pcounter"></span>
<b>Store <i>index</i></b>. Store the type on the top of the stack into local <i>index</i>. Raises an
error if index does not indicate a valid local register.
<P><span class="pcounter"></span>
<b>PushScope <i>type</i></b>. Push the specified type onto the scope stack. Check that it
matches the expected type. [<b>FIXME</b> how is the pushed type constrainted?]. Raises an error if
the number of elements on the scope stack is equal to the maximum stack size.
<P><span class="pcounter"></span>
<b>PopScope</b>. Pop the top type from the scope stack.
<P><span class="pcounter"></span>
<b>Jump <i>offset</i></b>. Merge the current machine state with the state associated with the
instruction indicated by offset. The meaning of merge depends on the direction of the
control flow causing the merge.
<P><span class="pcounter"></span>
Two machine states merge on a forward edge if each of the following conditions
hold:
<ul>
<li> operand stack is the same size
<li> scope stack is the same size
<li> scope type at each scope stack location is consistent
<li> type at each value location (operand stack and locals) are consistent
</ul>
<P><span class="pcounter"></span>
A merge of a backward edge is more constrained than a merge on a forward edge.
On a backward edge it is a verifier error if the merged type is different than the
target type. This includes the notNull attribute of that type. The reason for this
limitation is that by the time a backward edge is verified, the state of the machine
may have been used by a preceding instruction and so the type state cannot safely
be modified.
<P><span class="pcounter"></span>
Raises an error if offset does not refer to the beginning of an instruction or if the
current machine and the state associated with that offset are not consistent.
<P><span class="pcounter"></span>
<b>Throws</b>. The Throws operation saves the current abstract machine state, configures
the scope and operand stacks for the exception handlers, jumps (as if by the Jump
operator) to each of the catch handlers, and then restores the saved machine state.
Raises no error.
PopName name. Pop a name from the operand stack. The structure of a name
value depends on the kind of name be referenced. Raise an error if the type(s) on
the operand stack are either too few or incompatible with the name kind specified by
the instruction operand.
<P><span class="pcounter"></span>
<b>FindName <i>name</i></b>. Resolve the name constructed from the instruction operand and
element(s) on the operand stack to a type in the scope stack by searching the scope
stack for a type that contains the given name. If found push the found type onto the
operand stack. Otherwise push the global type onto the operand stack.
<P><span class="pcounter"></span>
<b>FindDefName <i>name</i></b>. FIXME
<P><span class="pcounter"></span>
<b>GetSlot <i>index</i></b>. FIXME
<P><span class="pcounter"></span>
<b>GetName <i>name</i></b>. FIXME
<P><span class="pcounter"></span>
<b>SetSlot <i>index</i></b>. FIXME
<P><span class="pcounter"></span>
<b>SetName <i>name</i></b>. FIXME
<h3>Interpreter Loop</h3>
<P><span class="pcounter"></span>
The interpreter loop scans the bytecode in a single forward pass interpreting each
bytecode with the abstract meaning given below. After an instruction is interpreted,
the current machine state is merged with the input state of the next instruction as
though there is an implicit edge in the control flow graph to that instruction.
<P><span class="pcounter"></span>
If an invariant is violated during execution of an operator or the subsequent merge
with the input state of the next instruction, the bytecode sequence is considered
invalid and verification terminates.
<p class="note"><b>NOTE</b>&nbsp;&nbsp; Machine state is merged with the state of the next instruction even if there is
no direct path to that instruction. This allows the machine state to be approximated
without using an iterative data flow algorithm. The burden on the compiler that
generates the bytecode is to configure the types of live variables before entering the
loop through one of these imaginary edges.
<hr>
<PRE>
R1=0
&#60;fixup>
jump L2
&#60;dead>
L1: label
&#60;body>
R1=R1+1
L2: if &#60;condition> L1
</PRE>
<hr>
Example 1
<P><span class="pcounter"></span>
The machine state at 'jump L2' will be merged with the state at 'L1: label'. Any
intervening '<dead>' code will be ignored by the verifier and thus have no effect on
the interpreter state. This approximates reality where L1 is reached through the back
edge at L2. What is missing is an accounting of the effect that '<body>' has on the
machine state at L1. The code generator (or author) of this code must either insert
coerce and kill instructions in the region of '<fixup>', or reorganize the control flow
so that the condition comes before the body of the loop.
<hr>
<PRE>
R1=0
L2: if &#60;condition> L1
&#60;body>
R1=R1+1
jump L2
L1: label
</PRE>
<hr>
Example 2
<P><span class="pcounter"></span>
In this configuration every use is preceded by an actual definition of a locations
state. Any location that is used in <body> will have to be defined before <body> is
entered or inside of <body> but before it is used. A later redefinition of that location
will still be limited to the current restrictions on type merging on backedges.]
<P><span class="pcounter"></span>
<p class="fixme"><b>FIXME</b>&nbsp;&nbsp; the logic of dead code identification is not straightforward and needs to be
defined
<P><span class="pcounter"></span>
If the interpreter reaches the end of the bytecode, then the bytecode is valid.
<h4>Control Flow Graphs</h4>
<P><span class="pcounter"></span>
We have already seen that an implicit edge in the control flow graph (CFG) is created
to each instruction from the previous instruction. Here is the complete list of rules
used to create the CFG for a method.
<ul>
<li> to every instruction from the previous instruction
<li> to every exception handler from every in scope instruction that can throw an
exception
<li> from every jump to every jump target (including lookupswitch)
</ul>
<h3>ABC Instructions</h3>
<P><span class="pcounter"></span>
The abstract interpretation of ABC bytecode can be expressed in the abstract
machine operations defined above. The following is such a mapping from ABC
instruction to the abstract operators.
<P><span class="pcounter"></span>
<p class="fixme"><b>FIXME</b>&nbsp;&nbsp; this mapping is currently only approximate, and undoubtedly buggy. But is
good enough to get us started in the debugging process.]
<P><span class="pcounter"></span>
For the most part the notation is self-evident. Parens following an instruction name
indicate the type case for that particular definition. <code>!</code> (e.g. <code>!String</code>) indicates that <code>Null</code>
is excluded from the reference type being named.
<pre>
<b>abs_jump</b>:
; FIXME need definition
<b>add (!String, _)</b>: ; NOTE ! means nonNull
<b>add (_, !String)</b>:
Throws
Pop
Pop
Push String
<b>add (Numeric, Numeric)</b>: ; NOTE Numeric means converts to Number
Throws
Pop
Pop
Push Number
<b>add</b>:
Throws
Pop
Pop
Push Object
<b>add_d</b>:
; ERROR invalid instruction
<b>add_i</b>:
Throws
Pop
Pop
Push Int
<b>applytype argc</b>:
Throws
Pop argc+1
Push Any ; FIXME might be more specific if jitting
<b>astype type</b>:
Throws
Pop
Push type
<b>astypelate</b>:
Throws
Check Class
Peek c
Pop
Pop
Push instanceTypeOf(c)
; FIXME define instanceTypeOf
<b>bitand</b>:
Throws
Pop
Pop
Push Int
<b>bitnot</b>:
Throws
Pop
Push Int
<b>bitor</b>:
<b>bitxor</b>:
; REF bitand
<b>call argc</b>:
Throws
Pop argc+2
Push Any
<b>callinterface</b>:
<b>callmethod</b>:
; ERROR invalid instruction
<b>callproperty name</b>:
<b>callproplex name</b>:
<b>callpropvoid name</b>:
Throws
; CHECK name is not an attribute name
PopName name
<b>callstatic method argc</b>:
<b>callsuper method argc</b>:
<b>callsupervoid method argc</b>:
Throws
Pop argc+1
Push method.resultType
; ASSERT method has parameter types
CheckArgs ; FIXME needs definition
<b>checkfilter</b>:
Throws
Pop
Push Any
<b>coerce type</b>:
Throws
Pop
Push type
<b>coerce_a</b>:
Throws
Pop
Push Any
<b>coerce_b</b>:
Throws
Pop
Push Boolean
<b>coerce_d</b>:
Throws
Pop
Push Number
<b>coerce_i</b>:
Throws
Pop
Push Int
<b>coerce_o</b>:
Throws
Pop
Push Object
<b>coerce_s</b>:
Throws
Pop
Push String
<b>coerce_u</b>:
Throws
Pop
Push Uint
<b>concat</b>:
; ERROR invalid instruction (see add)
<b>construct name argc</b>:
Throws
Pop argc
Peek class
InstanceTypeOf(class) ; FIXME needs definition
<b>constructprop name argc</b>:
Throws
; CHECK name is not an attribute name
PopName name
<b>constructsuper argc</b>:
Throws
Pop argc+1
; CHECK base class is not null
<b>convert_b</b>:
; REF coerce_b
<b>convert_d</b>:
; REF coerce_d
<b>convert_i</b>:
; REF coerce_i
<b>convert_o</b>:
Peek t
Pop
Push t
<b>convert_s</b>:
Pop
Push String
<b>convert_u</b>:
; REF coerce_u
<b>debug</b>:
<b>debugfile</b>:
<b>debugline</b>:
Throws
<b>declocal</b>:
Throws
Load index
Coerce Number
Store index
<b>declocal_i</b>:
Throws
Load index
Coerce Int
Store index
<b>decrement</b>:
Throws
Pop
Push Number
<b>decrement_i</b>:
Throws
Pop
Push Int
<b>deleteproperty name</b>:
Throws
PopName name
<b>divide</b>:
Throws
Pop 2
Push Number
<b>dup</b>:
Peek t
Push t
<b>dxns</b>:
Throws
<b>dxnslate</b>:
Throws
Pop
<b>equals</b>:
Throws
Pop 2
Push Boolean
<b>esc_xattr</b>:
<b>esc_xelem</b>:
; REF convert_s
<b>finddef name</b>:
Throws
FindDefName name
<b>findproperty name</b>:
<b>findpropstrict name</b>:
Throws
; CHECK scope stack is not empty
FindName name
<b>getdescendants name</b>:
Throws
PopName name
Push Any
<b>getglobalscope</b>:
Push typeOfGlobalScope()
<b>getglobalslot index</b>:
Push typeOfGlobalSlot(index)
<b>getlex name</b>:
Throws
; CHECK scope stack is not empty
FindName name
GetProp name
<b>getlocal index</b>:
Load index
<b>getlocal0</b>:
Load 0
<b>getlocal1</b>:
Load 1
<b>getlocal2</b>:
Load 2
<b>getlocal3</b>:
Load 3
<b>getouterscope index</b>:
OuterScopeAt index ; FIXME needs definition
<b>getproperty name</b>:
Throws
GetProp name
<b>getscopeobject index</b>:
ScopeAt index ; FIXME needs definition
<b>getslot index</b>:
GetSlot index
<b>getsuper name</b>:
Throws
; CHECK name is not an attribute name
GetSuper
GetProp name
<b>greaterequals</b>:
<b>greaterthan</b>:
Throws
Pop 2
Push Boolean
<b>hasnext</b>:
Throws
Check Int
Peek t ; FIXME what this?
Pop 2
Push Int
<b>hasnext2 index1 index2</b>:
Throws
Check Any index1
Check Int index2
Push Boolean
<b>ifeq offset</b>:
Throws
Pop 2
Jump offset
<b>iffalse offset</b>:
Pop
Jump offset
<b>ifge offset</b>:
<b>ifgt offset</b>:
<b>ifle offset</b>:
<b>iflt offset</b>:
<b>ifne offset</b>:
<b>ifnge offset</b>:
<b>ifngt offset</b>:
<b>ifnle offset</b>:
<b>ifnlt offset</b>:
; REF ifeq
<b>ifstricteq offset</b>:
<b>ifstrictneq offset</b>:
Pop 2
Jump offset
<b>iftrue offset</b>:
; REF iffalse
<b>in</b>:
; REF equals
<b>inclocal index</b>:
; REF declocal
<b>inclocal_i index</b>:
; REF declocal_i
<b>increment</b>:
; REF decrement
<b>increment_i</b>:
; REF decrement_i
<b>initproperty name</b>:
Throws
Pop
PopName name
Pop
<b>instanceof</b>:
; REF equals
<b>istype name</b>:
Throws
Pop
Push Boolean
; FIXME the verifier code doesn't actually do this.
<b>istypelate</b>:
Throws
Pop 2
Push Boolean
<b>jump offset</b>:
Jump offset
<b>kill index</b>:
Push Undefined
Store index
<b>label</b>:
; NOTE do nothing
<b>lessequals</b>:
<b>lessthan</b>:
; REF greaterthan
<b>lf64</b>:
<b>lf32</b>:
Throws
Pop
Push Number
<b>li32</b>:
<b>li16</b>:
<b>li8</b>:
Throws
Pop
Push Int
<b>lookupswitch offset count targets[count]</b>:
Check Int
Pop
Jump offset
JumpAll targets ; FIXME needs definition
<b>lshift</b>:
Throws
Pop 2
Push Int
<b>modulo</b>:
<b>multiply</b>:
; REF divide
<b>multiply_i</b>:
; REF add_i
<b>negate</b>:
Pop
Push Number
<b>negate_i</b>:
Throws
Push Int
<b>newactivation</b>:
; CHECK need_activation flag is set in method info
Throws
GetActivationScope ; FIXME needs definition
<b>newarray argc</b>:
Throws
Pop argc
Push Array
<b>newcatch index</b>:
Throws
GetHandlerScope index
<b>newclass index</b>:
Throws
Pop
GetClassScope index ; FIXME needs definition
; FIXME to simplistic
<b>newfunction index</b>:
Throws
Pop
GetFunctionScope index ; FIXME needs definition
; FIXME what's missing?
<b>newobject argc</b>:
Throws
; CHECK every other operand < 2*argc is a String
Pop 2*argc
Push Object
<b>nextname</b>:
<b>nextvalue</b>:
Throws
Check Int
Pop 2
Push Any
<b>nop</b>:
; NOTE do nothing
<b>not</b>:
Pop
Push Boolean
<b>pop</b>:
Pop
<b>popscope</b>:
PopScope
<b>pushbyte b</b>:
Push Int
<b>pushdouble d</b>:
Push Number
<b>pushfalse</b>:
Push Boolean
<b>pushint v</b>:
Push Int
<b>pushnamespace index</b>:
Push Namespace
<b>pushnan</b>:
Push Number
<b>pushnull</b>:
Push Null
<b>pushscope</b>:
Peek s
Pop
PushScope s
<b>pushshort v</b>:
Push Int
<b>pushstring index</b>:
Push String
<b>pushtrue</b>:
Push Boolean
<b>pushuint</b>:
Push Uint
<b>pushundefined</b>:
Push Undefined
<b>pushwith</b>:
Peek s
Pop
PushScope s
<b>returnvalue</b>:
Pop
<b>returnvoid</b>:
; NOTE do nothing
<b>rshift</b>:
; REF lshift
<b>setglobalslot index</b>:
; CHECK scope stack is not empty
Pop
<b>setlocal index</b>:
Store index
<b>setlocal0</b>:
Store 0
<b>setlocal1</b>:
Store 1
<b>setlocal2</b>:
Store 2
<b>setlocal3</b>:
Store 3
<b>setproperty</b>:
; REF initproperty
<b>setslot index</b>:
Throws
Pop 2
<b>setsuper name</b>:
Throws
; CHECK name is not an attribute name
PopName
Pop 2
<b>sf32</b>:
<b>sf64</b>:
<b>si16</b>:
<b>si32</b>:
<b>si8</b>:
Throws
Pop 2
<b>strictequals</b>:
; REF equals
<b>subtract</b>:
; REF divide
<b>subtract_i</b>:
; REF add_i
<b>swap</b>:
Swap
<b>sxi1</b>:
<b>sxi8</b>:
<b>sxi16</b>:
Pop
Push Int
<b>throw</b>:
Pop
Throws
<b>timestamp</b>:
; ERROR invalid instruction
<b>typeof</b>:
Pop
Push String
<b>urshift</b>:
Throws
Pop 2
Push Uint
</pre>
<h2>Working Examples</h2>
In this section we review some common verify errors and how to avoid them.
<h3>Inconsistent Types on a Forward Edge</h3>
The following is an example of an unsuccessful merge between an Int and UInt
resulting in a verfication error. That error will be avoided if the integer values were
both coerced to the Atom* type Any before being stored in local slot 2.
<pre>
verify <anonymous>()
stack:
scope: [global]
locals: Object * * *
0:pushbyte 0
stack: int
scope: [global]
locals: Object * * *
2:setlocal2 <b><-- Insert coerce_a</b>
stack:
scope: [global]
locals: Object * int *
.
.
.
9:iffalse 16
stack:
scope: [global]
locals: Object * int int
13:getlocal3
stack: int
scope: [global]
locals: Object * int int
14:convert_u
stack: uint
scope: [global]
locals: Object * int int
15:setlocal2 <b><-- Insert coerce_a</b>
VerifyError: Error #1068: int and uint cannot be reconciled.
</pre>
<h3>Inconsistent Type on a Backward Edge</h3>
<h4>Forward Edge</h4>
On a forward edge <code>null</code> and <code>String</code> merge to <code>String?</code>.
<pre>
function f (b) {
var x = null
if (b) {
x = "foo"
}
}
</pre>
The above ActionScript code might be compiled as the following acceptable bytecode.
<pre>
verify <anonymous>()
stack:
scope: [global]
locals: Object * *
0:pushnull
stack: null
scope: [global]
locals: Object * *
1:setlocal2
stack:
scope: [global]
locals: Object * null
.
.
.
4:iffalse 11
stack:
scope: [global]
locals: Object * null
8:pushstring <span class="literal">
stack: String
scope: [global]
locals: Object * null
10:setlocal2
B0:
stack:
scope: [global]
locals: Object * String?
11:returnvoid
</pre>
<h4>Backward Edge</h4>
However, on a backward edge <code>String?</code> and <code>null</code> do not merge. This is for the simple
reason that the merge on the backward edge causes the type to
change: <code>null</code> -> <code>String?</code>.
<pre>
function f (b) {
var x = null
while (b) {
x = "foo"
}
}
</pre>
<P><span class="pcounter"></span>
A naive compiler might compile the above code as below. It would do well to
insert <code>coerce_s</code> as indicated.
<pre>
verify <anonymous>()
stack:
scope: [global]
locals: Object * *
0:pushnull
stack: null
scope: [global]
locals: Object * *
1:setlocal2 <b><-- Insert coerce_s here</b>
stack:
scope: [global]
locals: Object * null
2:jump 10
B0:
stack:
scope: [global]
locals: Object? * null
6:label
stack:
scope: [global]
locals: Object? * null
7:pushstring </span>
stack: String
scope: [global]
locals: Object? * null
9:setlocal2
B1:
stack:
scope: [global]
locals: Object? * String?
10:getlocal1
stack: *
scope: [global]
locals: Object? * String?
11:convert_b
stack: Boolean
scope: [global]
locals: Object? * String?
12:iftrue 6
VerifyError: Error #1068: null and String cannot be reconciled.
</pre>
<h3>Unbalanced Stack</h3>
An unbalanced stack results when two or more paths that lead to the same control
flow point lead to different stack depths. Here is an example:
<pre>
verify <anonymous>()
stack:
scope: [global]
locals: Object *
0:getlocal1
stack: *
scope: [global]
locals: Object *
1:convert_b
stack: Boolean
scope: [global]
locals: Object *
2:iffalse 9
stack:
scope: [global]
locals: Object *
6:pushfalse
stack: Boolean
scope: [global]
locals: Object *
7:dup <b><-- either don't dup or move extra push outside of branch</b>
stack: Boolean Boolean
scope: [global]
locals: Object *
8:coerce_a
VerifyError: Error #1030: Stack depth is unbalanced. 2 != 0.
</pre>
<h2>References</h2>
<P><span class="pcounter"></span>
[1] <a href='http:<i>pauillac.inria.fr/~xleroy/publi/bytecode-verification-JAR.pdf'>
"Java bytecode verification: algorithms and formalizations", Xavier Leroy
</a>
<P><span class="pcounter"></span>
[2] <a href='ftp:</i>ftp.kestrel.edu/pub/papers/coglio/ccpe03.pdf'>
"Improving the official specification of Java bytecode verification", Alessandro Coglio
</a>
<P><span class="pcounter"></span>
[3] <a href=http://www.adobe.com/devnet/actionscript/articles/avm2overview.pdf>
"ActionScript Virtual Machine 2 Overview", Adobe Systems
</a>
Reference in new issue View Git Blame Copy Permalink