This specification definesasm.js, a strict subsetof JavaScript that can be used as a low-level, efficient targetlanguage for compilers. This sublanguage effectively describes a sandboxedvirtual machine for memory-unsafe languages like C or C++. Acombination of static and dynamic validation allows JavaScript enginesto employ an ahead-of-time (AOT) optimizing compilation strategy forvalid asm.js code.
This specification is working towards a candidate draft for asm.jsversion 1. Mozilla's SpiderMonkey JavaScript engine provides anoptimizing implementation of this draft.
case anddefault validation rulesmutdoublish todouble? for symmetry withfloat?Math.fround and singletonfround typefloat support for operators andMath functionsfloat to legal result types forConditionalExpressionMath.min andMath.maxMath.abs issignedunsigned is not anextern type! operator toUnaryExpression operators~~ toUnary Operators section-NumericLiteral cases everywhereunknown, which is no longer needed% isintishThis specification definesasm.js, a strict subset ofJavaScript that can be used as a low-level, efficient target languagefor compilers. The asm.js language provides an abstraction similar tothe C/C++ virtual machine: a large binary heap with efficient loadsand stores, integer and floating-point arithmetic, first-orderfunction definitions, and function pointers.
The asm.js programming model is built around integer andfloating-point arithmetic and a virtual heap represented asatypedarray. While JavaScript does not directly provide constructs fordealing with integers, they can be emulated using two tricks:
As an example of the former, if we haveanInt32Arrayview of the heap calledHEAP32, then we can load the32-bit integer at byte offsetp:
HEAP32[p >> 2]|0
The shift converts the byte offset to a 32-bit element offset, andthe bitwise coercion ensures that an out-of-bounds access is coercedfromundefined back to an integer.
As an example of integer arithmetic, addition can be performed bytaking two integer values, adding them with the built-in additionoperator, and coercing the result back to an integer via the bitwiseor operator:
(x+y)|0
This programming model is directly inspired by the techniquespioneered by theEmscriptenandMandreel compilers.
The asm.js sub-language is defined by astatic type system that can be checkedat JavaScript parse time. Validation of asm.js code is designed to be"pay-as-you-go" in that it is never performed on code that does notrequest it. An asm.jsmodule requests validation by meansof aspecialprologuedirective, similar to that of ECMAScript Edition5'sstrictmode:
function MyAsmModule() { "use asm"; // module body}This explicit directive allows JavaScript engines to avoidperforming pointless and potentially costly validation on otherJavaScript code, and to report validation errors in developer consolesonly where relevant.
Because asm.js is a strict subset of JavaScript, this specificationonly defines the validation logic—the execution semantics issimply that of JavaScript. However, validated asm.js is amenable toahead-of-time (AOT) compilation. Moreover, the code generated by anAOT compiler can be quite efficient, featuring:
Code that fails to validate must fall back to execution bytraditional means, e.g., interpretation and/or just-in-time (JIT)compilation.
Using an asm.js module requires calling its function to obtain anobject containing the module's exports; this is knownaslinking. An asm.js module can also be given access tostandard libraries and custom JavaScript functions through linking. AnAOT implementation must perform certaindynamicchecks to check compile-time assumptions about the linkedlibraries in order to make use of the compiled code.
This figure depicts a simple architecture of an AOT implementationthat otherwise employs a simple interpreter. If either dynamic orstatic validation fails, the implementation must fall back to theinterpreter. But if both validations succeed, calling the moduleexports executes the binary executable code generated by AOTcompilation.
Within an asm.js module, all code is fully statically typed andlimited to the very restrictive asm.js dialect. However, it ispossible to interact with recognized standard JavaScript libraries andeven custom dynamic JavaScript functions.
An asm.js module can take up to three optional parameters,providing access to external JavaScript code and data:
ArrayBufferto act as the asm.js heap.These objects allow asm.js to call into external JavaScript (and toshare its heap buffer with external JavaScript). Conversely, theexports object returned from the module allows external JavaScript tocall into asm.js.
So in the general case, an asm.js module declaration looks like:
function MyAsmModule(stdlib, foreign, heap) { "use asm"; // module body... return { export1: f1, export2: f2, // ... };}Function parameters in asm.js are provided a type annotation bymeans of an explicit coercion on function entry:
function geometricMean(start, end) { start = start|0; // start has type int end = end|0; // end has type int return +exp(+logSum(start, end) / +((end - start)|0));}These annotations serve two purposes: first, to provide thefunction's type signature so that the validator can enforce that allcalls to the function are well-typed; second, to ensure that even ifthe function is exported and called by external JavaScript, itsarguments are dynamically coerced to the expected type. This ensuresthat an AOT implementation can use unboxed value representations,knowing that once the dynamic coercions have completed, the functionbody never needs any runtime type checks.
The following is a small but complete example of an asm.js module.
function GeometricMean(stdlib, foreign, buffer) { "use asm"; var exp = stdlib.Math.exp; var log = stdlib.Math.log; var values = new stdlib.Float64Array(buffer); function logSum(start, end) { start = start|0; end = end|0; var sum = 0.0, p = 0, q = 0; // asm.js forces byte addressing of the heap by requiring shifting by 3 for (p = start << 3, q = end << 3; (p|0) < (q|0); p = (p + 8)|0) { sum = sum + +log(values[p>>3]); } return +sum; } function geometricMean(start, end) { start = start|0; end = end|0; return +exp(+logSum(start, end) / +((end - start)|0)); } return { geometricMean: geometricMean };}In a JavaScript engine that supports AOT compilation of asm.js,calling the module on a proper global object and heap buffer wouldlink the exports object to use the statically compiled functions.
var heap = new ArrayBuffer(0x10000); // 64k heapinit(heap, START, END); // fill a region with input valuesvar fast = GeometricMean(window, null, heap); // produce exports object linked to AOT-compiled codefast.geometricMean(START, END); // computes geometric mean of input values
By contrast, calling the module on a standard library objectcontaining something other than the trueMath.exp orMath.log would fail to produce AOT-compiled code:
var bogusGlobal = { Math: { exp: function(x) { return x; }, log: function(x) { return x; } }, Float64Array: Float64Array};var slow = GeometricMean(bogusGlobal, null, heap); // produces purely-interpreted/JITted versionconsole.log(slow.geometricMean(START, END)); // computes bizarro-geometric mean thanks to bogusGlobalValidation of an asm.js module relies on a static type system thatclassifies and constrains the syntax. This section defines the typesused by the validation logic.
Validation in asm.js limits JavaScript programs to only use operationsthat can be mapped closely to efficient data representations andmachine operations of modern architectures, such as 32-bit integersand integer arithmetic.
The types of asm.js values are inter-related by a subtypingrelation, which can be represented pictorially:
The light boxes represent arbitrary JavaScript values that may flowfreely between asm.js code and external JavaScript code.
The dark boxes represent types that are disallowed from escapinginto external (i.e., non-asm.js) JavaScript code. (These values can begiven efficient, unboxed representations in optimized asm.jsimplementations that would be unsound if they were allowed to escape.)
The meta-variables σ and τ are used to stand for valuetypes.
Thevoid type is the type of functions thatare not supposed to return any useful value. As JavaScript functions,they produce theundefined value, but asm.js code is notallowed to make use of this value; functions with returntypevoid can only be called for effect.
Thedouble type is the type of ordinaryJavaScript double-precision floating-point numbers.
Thesigned type is the type of signed32-bit integers. While there is no direct concept of integers inJavaScript, 32-bit integers can be represented as doubles, and integeroperations can be performed with JavaScript arithmetic, relational,and bitwise operators.
Theunsigned type is the type of unsigned32-bit integers. Again, these are not a first-class concept inJavaScript, but can be represented as floating-point numbers.
Theint type is the type of 32-bit integerswhere the signedness is not known. In asm.js, the type of a variablenever has a known signedness. This allows them to be compiled as32-bit integer registers and memory words. However, thisrepresentation creates an overlap between signed and unsigned numbersthat causes an ambiguity in determining which JavaScript number theyrepresent. For example, the bit pattern0xffffffff couldrepresent 4294967295 or -1, depending on the signedness. For thisreason, values of theint type are disallowed fromescaping into external (non-asm.js) JavaScript code.
Thefixnum type is the type of integers in therange [0, 231)—that is, the range of integers suchthat an unboxed 32-bit representation has the same value whether it isinterpreted as signed or unsigned.
Even though JavaScript only supports floating-point arithmetic,most operations can simulate integer arithmetic by coercing theirresult to an integer. For example, adding two integers may overflowbeyond the 32-bit range, but coercing the result back to an integerproduces the same 32-bit integer as integer addition in, say, C.
Theintish type represents the result of aJavaScript integer operation that must be coerced back to an integerwith an explicit coercion(ToInt32for signed integersandToUint32for unsigned integers). Validation requires allintishvalues to be immediately passed to an operator or standard librarythat performs the appropriate coercion or else dropped via anexpression statement. This way, each integer operation can becompiled directly to machine operations.
The one operator that does not support this approach ismultiplication. (Multiplying two large integers can result in a largeenough double that some lower bits of precision are lost.) So asm.jsdoes not support applying the multiplication operator to integeroperands. Instead, theproposedMath.imulfunction is recommended as the proper means of implementing integermultiplication.
Thedouble? type represents operations thatare expected to produce adouble but may also produceundefined, and so must be coerced back to a numberviaToNumber.Specifically, reading out of bounds from a typed arrayproducesundefined.
Thefloat type is the type of 32-bitfloating-point numbers.
Thefloat? type represents operations thatare expected to produce afloat but, similartodouble?, may also produceundefined andso must be coerced back to a 32-bit floating point numberviafround.Specifically, reading out of bounds from a typed arrayproducesundefined.
Similar to integers, JavaScript can almost support 32-bitfloating-point arithmetic, but requires extra coercions to properlyemulate the 32-bit semantics. As proved inWhen is doublerounding innocuous? (Figueroa 1995), both the 32- and 64-bitversions of standard arithmetic operations produce equivalent resultswhen given 32-bit inputs and coerced to 32-bit outputs.
Thefloatish type,likeintish, represents the result of a JavaScript 32-bitfloating-point operations that must be coerced back to a 32-bitfloating-point value with anexplicitfroundcoercion. Validation requires allfloatish values to beimmediately passed to an operator or standard library that performsthe appropriate coercion or else dropped via an expressionstatement. This way, each 32-bit floating-point operation can becompileddirectly to machine operations.
extern type represents the rootof all types that can escape back into external JavaScript—inother words, the light boxes in the above diagram.Variables and functions defined at the top-level scope of an asm.jsmodule can have additional types beyondthevalue types. These include:
ArrayBufferView typesIntnArray,UintnArray, andFloatnArray;…) → τ) ∧ … ∧ ((σ′, σ′…) → τ′);fround ofMath.fround; andFunction.The "∧" notation for function types serves to representoverloaded functions and operators. For example,theMath.abs function isoverloaded to accept either integers or floating-point numbers, andreturns a different type in each case. Similarly, many oftheoperators have overloaded types.
The meta-variable γ is used to stand for global types.
Validating an asm.js module depends on tracking contextualinformation about the set of definitions and variables in scope. Thissection defines theenvironments used by the validationlogic.
An asm.js module is validated in the context of aglobalenvironment. The global environment maps each global variable toits type as well as indicating whether the variable is mutable:
The meta-variable Δ is used to stand for a global environment.
In addition to theglobal environment, each functionbody in an asm.js module is validated in the context ofavariable environment. The variable environment maps eachfunction parameter and local variable to its value type:
{x : τ, … }
The meta-variable Γ is used to stand for a variable environment.
Looking up a variable's type
is defined by:
mut γ orx :imm γoccurs in ΔIfx does not occur in either environment thentheLookup function has no result.
Validation of an asm.js module is specified by reference totheECMAScriptgrammar, but conceptually operates at the level of abstractsyntax. In particular, an asm.js validator must obey the followingrules:
;) are always ignored, whether inthe top level of a module or inside an asm.js function body.evalorarguments.These rules are otherwise left implicit in the rest of thespecification.
All variables in asm.js are explicitly annotated with typeinformation so that their type can be statically enforced byvalidation.
Every parameter in an asm.js function is provided with an explicittype annotation in the form of a coercion. This coercion serves twopurposes: the first is to make the parameter type statically apparentfor validation; the second is to ensure that if the function isexported, the arguments dynamically provided by external JavaScriptcallers are coerced to the expected type. For example, a bitwise ORcoercion annotates a parameter as having typeint:
function add1(x) { x = x|0; // x : int return (x+1)|0;}In an AOT implementation, the body of the function can beimplemented fully optimized, and the function can be given two entrypoints: an internal entry point for asm.js callers, which arestatically known to provide the proper type, and an external dynamicentry point for JavaScript callers, which must perform the fullcoercions (which might involve arbitrary JavaScript computation, e.g.,via implicit calls tovalueOf).
There are three recognized parameter type annotations:
=x:Identifier|0;=+x:Identifier;=f:Identifier(x:Identifier);The first form annotates a parameter as typeint, thesecond as typedouble, and the third astypefloat. In the latter case,Lookup(Δ, Γ,f) mustbefround.
An asm.js function'sformal return type is determined bythe last statement in the function body, which fornon-void functions is required to beaReturnStatement. This distinguished return statement maytake one of five forms:
return +e:Expression;returne:Expression|0;returnn:-?NumericLiteral;returnf:Identifier(arg:Expression);return;The first form has return typedouble. The second hastypesigned. The third has returntypedouble ifn is composed of a floating-pointliteral, i.e., a numeric literal with the character. inits source; alternatively, ifn is composed of an integerliteral and has its value in the range [-231,231), the return statement has returntypesigned. The fourth form has returntypefloat, and the fifth has returntypevoid.
If the last statement in the function body is notaReturnStatement, or if the function body has no non-emptystatements (other than the initial declarations andcoercions—seeFunctionDeclarations), the function's return type isvoid.
The type of a function declaration
functionf:Identifier(x:Identifier…) { x:Identifier=AssignmentExpression;… vary:Identifier=-?NumericLiteralIdentifier(-?NumericLiteral),…… body:Statement…}is (σ,…) → τ where σ,… are thetypes of the parameters, as provided bytheparameter typeannotations, and τ is the formal return type, as provided bythereturn type annotation. Thevariablef is stored intheglobal environment withtypeimm (σ,…) → τ.
The types of variable declarations are determined by theirinitializer, which may take one of two forms:
-?NumericLiteral(n:-?NumericLiteral)In the first case, the variable type isdoubleifn's source contains the character.;otherwisen may be an integer literal in the range[-231, 232), in which case the variable typeisint.
In the second case, the variable typeisfloat.Lookup(Δ, Γ,f)must befround andn must be a floating-pointliteral with the character. in its source.
A global variable declaration is aVariableStatement nodein one of several allowed forms. Validating global variableannotations takes a Δ as input and produces as output a newΔ′ by adding the variable binding to Δ.
A global program variable is initialized to a literal:
varx:Identifier=n:-?NumericLiteral;varx:Identifier=f:Identifier(n:-?NumericLiteral);The global variablex is stored intheglobal environment withtypemut τ, where τ is determined in the same wayas localvariable typeannotations.
A standard library import is of one of the following two forms:
varx:Identifier=stdlib:Identifier.y:Identifier;varx:Identifier=stdlib:Identifier.Math.y:Identifier;The variablestdlib must match the first parameter ofthemodule declaration. The globalvariablex is stored intheglobal environment withtypeimm γ, where γ is the type oflibraryy orMath.y as specified bythestandard library types.
A foreign import is of one of the following three forms:
varx:Identifier=foreign:Identifier.y:Identifier;varx:Identifier=foreign:Identifier.y:Identifier|0;varx:Identifier=+foreign:Identifier.y:Identifier;The variableforeign must match the second parameter ofthemodule declaration. The globalvariablex is stored intheglobal environment withtypeimm Function for the first form,mutint for the second, andmut double for the third.
A global heap view is of the following form:
varx:Identifier= newstdlib:Identifier.view:Identifier(heap:Identifier);The variablestdlib must match the first parameter ofthemodule declaration and thevariableheap must match the third. Theidentifierview must be one of thestandardArrayBufferViewtype names. The global variablex is stored intheglobal environment withtypeimmview.
A function table is aVariableStatement of the form:
varx:Identifier = [f0:Identifier,f:Identifier,…];The function tablex is stored intheglobal environment withtypeimm ((σ,…) → τ)[n]where (σ,…) → τ is the type off in theglobal environment andn is the length of the array literal.
To ensure that a JavaScript function is a proper asm.js module, itmust first be statically validated. This section specifies thevalidation rules. The rules operate on JavaScript abstract syntax,i.e., the output of a JavaScript parser. The non-terminals refer toparse nodes defined by productions intheECMAScriptgrammar, but note that the asm.js validator only accepts a subsetof legal JavaScript programs.
The result of a validation operation is eitherasuccess, indicating that a parse node is statically validasm.js, or afailure, indicating that the parse node isstatically invalid asm.js.
TheValidateModule rule validates an asm.js module, whichis either aFunctionDeclarationorFunctionExpression node.
Validating a module of the form
functionf:Identifieropt(stdlib:Identifier,foreign:Identifier,heap:Identifieroptoptopt) {
"use asm"; var:VariableStatement… fun:FunctionDeclaration… table:VariableStatement… exports:ReturnStatement}succeeds if:
TheValidateExport rule validates an asm.js module'sexport declaration. An export declaration isaReturnStatement returning either a single asm.js functionor an object literal exporting multiple asm.js functions.
Validating an export declaration node
return{x:Identifier:f:Identifier,… };succeeds if for eachf, Δ(f) =immγ where γ is a function type (σ,…) →τ.
Validating an export declaration node
returnf:Identifier;succeeds if Δ(f) =imm γ whereγ is a function type (σ,…) → τ.
TheValidateFunctionTable rule validates an asm.jsmodule's function table declaration. A function table declaration isaVariableStatement binding an identifier to an arrayliteral.
Validating a function table of the form
varx:Identifier = [f:Identifier,…];succeeds if:
imm ((σ,…) → τ)[n]; andTheValidateFunction rule validates an asm.js functiondeclaration, which is aFunctionDeclaration node.
Validating a function declaration of the form
functionf:Identifier(x:Identifier,…) { x:Identifier=AssignmentExpression;… vary:Identifier=-?NumericLiteralIdentifier(-?NumericLiteral),…… body:Statement…}succeeds if:
imm (σ,…) → τ;TheValidateStatement rule validates an asm.js statement.Each statement is validated in the context of aglobalenvironment Δ, avariable environmentΓ, and an expected return type τ. Unless otherwiseexplicitly stated, a recursive validation of a subterm uses the samecontext as its containing term.
Validating aBlock statement node
{stmt:Statement…}succeedsifValidateStatementsucceeds for eachstmt.
Validating anExpressionStatement node
;succeeds ifValidateCallsucceeds forcexpr with actual return typevoid.
Validating anExpressionStatement node
;succeedsifValidateExpressionsucceeds forexpr with some type σ.
Validating anEmptyStatement node always succeeds.
Validating anIfStatement node
if (expr:Expression)stmt1:Statementelsestmt2:StatementsucceedsifValidateExpressionsucceeds forexpr with a subtype ofintandValidateStatementsucceeds forstmt1 andstmt2.
Validating anIfStatement node
if (expr:Expression)stmt:StatementsucceedsifValidateExpressionsucceeds forexpr with a subtype ofintandValidateStatementsucceeds forstmt.
Validating aReturnStatement node
returnexpr:Expression;succeedsifValidateExpressionsucceeds forexpr with a subtype of the expected return typeτ.
Validating aReturnStatement node
return ;succeeds if the expected return type τ isvoid.
Validating anIterationStatement node
while (expr:Expression)stmt:StatementsucceedsifValidateExpressionsucceeds forexpr with a subtype ofintandValidateStatementsucceeds forstmt.
Validating anIterationStatement node
dostmt:Statementwhile (expr:Expression) ;succeedsifValidateStatementsucceeds forstmtandValidateExpressionsucceeds forexpr with a subtype ofint.
Validate anIterationStatement node
for (init:ExpressionNoInopt;test:Expressionopt;update:Expressionopt)body:Statementsucceeds if:
int (ifpresent);Validating aBreakStatement node
breakIdentifieropt;always succeeds.
Validating aContinueStatement node
continueIdentifieropt;always succeeds.
Validating aLabelledStatement node
:body:StatementsucceedsifValidateStatementsucceeds forbody.
Validating aSwitchStatement node
switch (test:Expression){case:CaseClause…default:DefaultClauseopt}succeeds if
signed;Cases in aswitch block are validated in the contextof aglobal environment Δ, avariableenvironment Γ, and an expected return type τ. Unlessotherwise explicitly stated, a recursive validation of a subterm usesthe same context as its containing term.
Validating aCaseClause node
casen:-?NumericLiteral:stmt:Statement…succeeds if
. character;The default case in aswitch block is validated in thecontext of aglobal environment Δ, avariableenvironment Γ, and an expected return type τ. Unlessotherwise explicitly stated, a recursive validation of a subterm usesthe same context as its containing term.
Validating aDefaultClause node
default :stmt:Statement…succeedsifValidateStatementsucceeds for eachstmt.
Each expression is validated in the context of aglobalenvironment Δ and avariable environmentΓ, and validation produces the type of the expression as aresult. Unless otherwise explicitly stated, a recursive validation ofa subterm uses the same context as its containing term.
Validating anExpression node
, …,exprn:AssignmentExpressionsucceeds with type τ if for everyi<n, one of the following conditions holds:
void; orandValidateExpressionsucceeds forexprn with type τ.
Validating aNumericLiteral node
double if the source contains a. character; orvalidates as typedouble;fixnum if the source does not contain a. character and its numeric value is in the range [0, 231); orunsigned if the source does not contain a. character and its numeric value is in the range [231, 232).Note that the case of negative integer constants is handledunderUnaryExpression.
Note that integer literals outside the range [0, 232)are invalid, i.e., fail to validate.
Validating anIdentifier node
succeeds with type τ ifLookup(Δ, Γ,x) = τ.
Validating aCallExpression node succeeds withtypefloatifValidateFloatCoercionsucceeds.
Validating aMemberExpression node succeeds with typeτifValidateHeapAccesssucceeds with load type τ.
Validating anAssignmentExpression node
=expr:AssignmentExpressionsucceeds with type τifValidateExpressionsucceeds for the nestedAssignmentExpression with type τand one of the following two conditions holds:
Validating anAssignmentExpression node
=rhs:AssignmentExpressionsucceeds with type τifValidateExpressionsucceeds forrhs with type τandValidateHeapAccesssucceeds forlhs with τ as one of its legal store types.
Validating aUnaryExpression node of the form
-NumericLiteralsucceeds with typesigned iftheNumericLiteral source does not contain a.character and the numeric value of the expression is in the range[-231, 0).
Validating aUnaryExpression node of the form
+cexpr:CallExpressionsucceeds with typedoubleifValidateCall succeedsforcexpr with actual return typedouble.
Validating aUnaryExpression node of the form
+-~!arg:UnaryExpressionsucceeds with type τ if the type ofop is …∧ (σ) → τ ∧ …andValidateExpressionsucceeds with a subtype of σ.
Validating aUnaryExpression node of the form
~~arg:UnaryExpressionsucceeds with typesignedifValidateExpressionsucceeds forarg with a subtype of eitherdoubleorfloat?.
Validating aMultiplicativeExpression node
*/%rhs:UnaryExpressionsucceeds with type τ if:
Validating aMultiplicativeExpression node
*n:-?NumericLiteral-?NumericLiteral*expr:UnaryExpressionsucceeds with typeintish if the source ofndoes not contain a. character and -220<n < 220andValidateExpressionexpr with a subtype ofint.
Validating anAdditiveExpression node
+- …+-exprnsucceeds with typeintish if:
int;Otherwise, validating anAdditiveExpression node
+-rhs:MultiplicativeExpressionsucceeds with typedouble if:
double;Validating aShiftExpression node
<<>>>>>rhs:AdditiveExpressionsucceeds with type τ if
Validating aRelationalExpression node
<><=>=rhs:ShiftExpressionsucceeds with type τ if
Validating anEqualityExpression node
==!=rhs:RelationalExpressionsucceeds with type τ if
Validating aBitwiseANDExpression node
&rhs:EqualityExpressionsucceeds with typesignedifValidateExpressionsucceeds forlhs andrhs witha subtype ofintish.
Validating aBitwiseXORExpression node
^rhs:BitwiseANDExpressionsucceeds with typesignedifValidateExpressionsucceeds forlhs andrhs witha subtype ofintish.
Validating aBitwiseORExpression node
|0succeeds with typesignedifValidateCall succeedsforcexpr with actual return typesigned.
Validating aBitwiseORExpression node
|rhs:BitwiseXORExpressionsucceeds with typesignedifValidateExpressionsucceeds forlhs andrhs witha subtype ofintish.
Validating aConditionalExpression node
?cons:AssignmentExpression:alt:AssignmentExpressionsucceeds with type τ if:
int,double, orfloat;int;Validating a parenthesized expression node
(expr:Expression)succeeds with type τifValidateExpressionsucceeds forexpr with type τ.
Each function call expression is validated in the context of aglobal environment Δ and a variable environment Γ, andvalidates against anactual return type τ, which wasprovided from the context in which the function call appears. Arecursive validation of a subterm uses the same context as itscontaining term.
Validating aCallExpression node
(arg:Expression,…)with actual return type τ succeeds if one of the followingconditions holds:
…)→ τ ∧ …andValidateExpressionsucceeds for the firstnargi expressionswith subtypes of their corresponding σi andthe remainingarg expressions with subtypes of σ.Alternatively, validating theCallExpression succeeds withany actual return type τ other thanfloatifLookup(Δ, Γ,f)=FunctionandValidateExpressionsucceeds for eacharg with a subtype ofextern.
Validating aCallExpression node
[index:Expression &n:-?NumericLiteral](arg:Expression,…)succeeds with actual return type τ if:
. character;intish; andEach heap access expression is validated in the context of a globalenvironment Δ and a variable environment Γ, and validationproduces aload type as well as a set of legalstoretypes as a result. These types are determined bytheheap view types corresponding toeachArrayBufferViewtype.
Validating aMemberExpression node
[n:-?NumericLiteral]succeeds with load type σ and store types { τ, … } if:
ArrayBufferViewtype;. character;Validating aMemberExpression node
[expr:Expression>>n:-?NumericLiteral]succeeds with load type σ and store types { τ, … }if:
ArrayBufferViewtype;intish;. character;A call to thefround coercion is validated in thecontext of a global environment Δ and a variable environmentΓ and validates as the typefloat.
Validating aCallExpression node
(cexpr:CallExpression)succeeds with typefloat ifLookup(Δ,Γ,f) =fround andValidateCall succeeds forcexpr with actual return typefloat.
Alternatively, validating aCallExpression node
(arg:Expression)succeeds with typefloat ifLookup(Δ,Γ,f) =froundandValidateExpressionsucceeds forarg with type τ, where τ is a subtypeoffloatish,double?,signed,orunsigned.
An AOT implementation of asm.js must perform some internal dynamicchecks at link time to be able to safely generate AOT-compiledexports. If any of the dynamic checks fails, the result of linkingcannot be an AOT-compiled module. The dynamically checked invariantsare:
return statement without throwing;ArrayBuffer;byteLength must be either 2n forn in [12, 24) or 224 ·n forn ≥ 1;If any of these conditions is not met, AOT compilation may produceinvalid results so the engine should fall back to an interpreted orJIT-compiled implementation.
| Unary Operator | Type |
|---|---|
+ | (signed) →double ∧( unsigned) →double ∧( double?) →double ∧( float?) →double |
- | (int) →intish ∧( double?) →double ∧( float?) →floatish |
~ | (intish) →signed |
! | (int) →int |
Note that the special combined operator~~ may be usedas a coercion fromdouble orfloat?tosigned; seeUnaryExpressions.
| Binary Operator | Type |
|---|---|
+ | (double,double) →double ∧( float?,float?) →floatish |
- | (double?,double?) →double ∧( float?,float?) →floatish |
* | (double?,double?) →double ∧( float?,float?) →floatish |
/ | (signed,signed) →intish ∧( unsigned,unsigned) →intish ∧( double?,double?) →double ∧( float?,float?) →floatish |
% | (signed,signed) →intish ∧( unsigned,unsigned) →intish ∧( double?,double?) →double |
|,&,^,<<,>> | (intish,intish) →signed |
>>> | (intish,intish) →unsigned |
<,<=,>,>=,==,!= | (signed,signed) →int ∧( unsigned,unsigned) →int ∧( double,double) →int ∧( float,float) →int |
| Standard Library | Type |
|---|---|
InfinityNaN | double |
Math.acosMath.asinMath.atanMath.cosMath.sinMath.tanMath.expMath.log | (double?) →double |
Math.ceilMath.floorMath.sqrt | (double?) →double ∧( float?) →float |
Math.abs | (signed) →signed ∧( double?) →double ∧( float?) →float |
Math.minMath.max | (int,int…) →signed ∧( double,double…) →double |
Math.atan2Math.pow | (double?,double?) →double |
Math.imul | (int,int) →signed |
Math.fround | fround |
Math.EMath.LN10Math.LN2Math.LOG2EMath.LOG10EMath.PIMath.SQRT1_2Math.SQRT2 | double |
| View Type | Element Size (Bytes) | Load Type | Store Types |
|---|---|---|---|
Uint8Array | 1 | intish | intish |
Int8Array | 1 | intish | intish |
Uint16Array | 2 | intish | intish |
Int16Array | 2 | intish | intish |
Uint32Array | 4 | intish | intish |
Int32Array | 4 | intish | intish |
Float32Array | 4 | float? | floatish,double? |
Float64Array | 8 | double? | float?,double? |
Thanks to Martin Best, Brendan Eich, Andrew McCreight, and VladVukićević for feedback and encouragement.
Thanks to Benjamin Bouvier, Douglas Crosher, and Dan Gohman forcontributions to the design and implementation, particularly forfloat.
Thanks to Jesse Ruderman and C. Scott Ananian for bug reports.
Thanks to Michael Bebenita for diagrams.