How does asm.js handle divide-by-zero?

In javascript, division by zero with "integer" arguments acts like floating points should:

 1/0;    // Infinity
-1/0;    // -Infinity
 0/0;    // NaN

The asm.js spec says that division with integer arguments returns intish, which must be immediately coerced to signed or unsigned. If we do this in javascript, division by zero with "integer" arguments always returns zero after coersion:

(1/0)|0;    // == 0, signed case.
(1/0) >> 0; // == 0, unsigned case.

However, in languages with actual integer types like Java and C, dividing an integer by zero is an error and execution halts somehow (e.g., throws exception, triggers a trap, etc).

This also seems to violate the type signatures specified by asm.js. The type of Infinity and NaN is double and of / is supposedly (from the spec):

(signed, signed) → intish ∧ (unsigned, unsigned) → intish ∧ (double?, double?) → double ∧ (float?, float?) → floatish

However if any of these has a zero denominator, the result is double, so it seems like the type can only be:

(double?, double?) → double

What is expected to happen in asm.js code? Does it follow javascript and return 0 or does divide-by-zero produce a runtime error? If it follows javascript, why is it ok that the typing is wrong? If it produces a runtime error, why doesn't the spec mention it?

asm.js is a subset of JavaScript, so it has to return what JavaScript does: Infinity|0 → 0.

You point out that Infinity is double, but that mixes up the asm.js type system with the C one (in JavaScript those are number): asm.js uses JavaScript type coercion to make intermediate results the "right" type when they aren't. The same thing happens when a small integer in JavaScript would overflow to a double: it gets coerced back into an integer using bitwise operations.

The key here is that it gives the compiler a hint that it doesn't need to calculate all the things JavaScript would usually have it calculate: it doesn't matter if a small integer overflows because it's coerced back into an integer, so the compiler can omit overflow checks and emit straight-line integer arithmetic. Note that it still has to behave correctly for every possible value! The type system basically hints the compiler towards doing a bunch of strength reductions.

Now back to integer division: on x86 this causes a floating-point exception (yes! Integer division causes SIGFPE!). The compiler knows the output is an integer so it can do an integer division, but it can't halt the program if the denominator was zero. There are two options here:

Branch around the division if the input is zero, and return zero directly.
Do the division with the provided input, but at the start of the program install a signal handler, catching SIGFPE. When it faults look up the code location, and if the compiler's metadata says that's a division location then modify the return value to be zero and continue executing.

The former is what V8 and OdinMonkey implement.

On ARM the integer division instruction is defined to always return zero, except ARMv7-R profile of ARM where it faults (the fault is undefined instruction, or can be changed to return zero if SCTRL.DZ == 0). ARM only added the UDIV and SDIV instructions recently with the ARMv7VE extension (virtualization extension), and made it optional in ARMv7-A processors (most phones and tablets use these). You can check for the instruction using /proc/cpuinfo, but note that some kernels are unaware of the instruction! A workaround is to check for the instruction when the process starts by executing the instruction and using sigsetjmp/siglongjmp to catch cases where it's not handled. That has a further caveat of also catching cases where the kernel is being "helpful" and emulating UDIV/IDIV on processors that don't support it! If the instruction isn't present then you have to use the C library's integer division instruction (libgcc or compiler_rt contain functions such as __udivmoddi4). Note that the behavior of this function on divide by zero may vary between implementations and has to be handled with a branch on zero denominator or checked at load time (same as outlined above for UDIV/SDIV).