Verbose is a small language I build that compiles to native x86-64, to WebAssembly, and also runs in an interpreter. This post walks through one bug that showed up differently in each of those, with real binaries. It stands on its own; no Verbose knowledge needed.
Before reading the first line of a notebook, you check there is something in it. Nobody does it the other way round. Nobody opens an empty notebook, tries to read line one, and then thinks "ah, it was empty, never mind".
In Verbose, that precaution is written like this:
length(i.s) == 0 or byte_at(i.s, 0) > 0
"The text is empty, or its first byte is nonzero." If the text is empty, the question is settled by the first half, and the second half, which reads byte number zero, has no reason to be asked. It cannot be, in fact: an empty text has no byte number zero.
On October 8th this line protected the program perfectly when Verbose compiled it to a native binary. And it protected nothing at all when the same program ran through the interpreter, or through WebAssembly. Here is why, and what it says about a word as simple as "or".
What "or" means, in two parts
There are two separate things in an "or".
The first is its value: true if at least one side is true. Everyone knows the table:
left right left or right
───── ───── ─────────────
false false false
false true true
true false true
true true true ← last two rows: as soon as the left
is true, the result is true,
whatever the right says
The second is its order: what gets computed, and when. That is where everything happens. There are two ways to compute left or right:
"everything first" "short-circuit"
────────────────── ───────────────
1. compute left 1. compute left
2. compute right 2. if left is true → answer true,
3. combine stop there
3. otherwise compute right, and
answer whatever it is
On paper both give the same value; the table does not change. But if computing the right side can fail, the two ways no longer do the same thing at all. The first one fails. The second one never goes there.
That is why writing a guard with an "or" makes sense: you are relying on the order. Short-circuiting is not an optimisation that saves time. It is the reason the line was written.
One program, three executors
A Verbose program can run three ways. The compiler checks the source once, then:
guard.verbose
│
source verification
(types, reads, declared proofs)
│
┌─────────────────────┼─────────────────────┐
▼ ▼ ▼
interpreter native binary WASM module
(Rust, walks the (x86-64 code, (bytecode for the
program tree and a 585-byte ELF) browser or Node)
computes node by
node)
The interpreter is someone reading the recipe aloud and doing it step by step. The native binary is the recipe translated once and for all into moves the processor makes directly. WASM is the same translation, for an imaginary machine the browser knows how to run.
Three translations of one sentence. They have to say the same thing. Take a tiny rule and give it two texts, "abc" and "":
rule first_byte_or_empty
input: i : Input (one field s : text)
output: out : number
logic:
out = if length(i.s) == 0 or byte_at(i.s, 0) > 0 then 1 else 0
Native: right from the start
Compile, run:
$ ./guard-native abc
1
$ ./guard-native ""
1
Both answers are right, and you can see why in the binary itself. Here is the passage, disassembled, just after the length is computed:
address instruction what it does
─────── ────────────────────── ─────────────────────────────────────────
12b cmp rcx, rax compare the length (rax) with 0 (rcx)
12e sete al al = 1 if equal, 0 otherwise
135 test rax, rax is the left side of the "or" true?
138 jne 0x1a6 ← if so: JUMP to 0x1a6, straight to
"answer true"
13e ... only otherwise: recompute the length,
16a cmp rax, rcx check index 0 is inside the text,
178 movzbl (rdx,rax), eax and read the byte
The jump at 0x138 is the short-circuit, in one six-byte instruction. With "", the left side is true, the processor jumps, and the instruction that reads the byte at 0x178 is never reached.
The interpreter: the recipe read in the wrong order
Same rule, same inputs, through the interpreter as it was before October 8th:
$ printf '[{"s":"abc"},{"s":""}]' | verbosec guard.verbose --run first_byte_or_empty --stdin --json
runtime error: byte_at index out of range: index=0, length=0
The empty text makes everything fail. The guard is there, it is correct, and it does nothing.
The interpreter's code explained it in three lines. For a binary operation it did this:
let l = eval_expr(left, ...)?; ① compute the left
let r = eval_expr(right, ...)?; ② compute the right ← fails here
match (op, l, r) {
(Or, Bool(a), Bool(b)) => Ok(Bool(a || b)), ③ combine
...
That is "everything first". The || on the third line does short-circuit, in Rust. But it comes too late: by the time we reach it, r has already been computed, and computing it has already failed. A short-circuit applied to two values you already have protects nothing.
Step through it with s = "":
step what the interpreter computes value
──── ───────────────────────────────────── ───────────────────────
1 length("") 0
2 0 == 0 true ← left
3 byte_at("", 0) ✗ error: index 0,
length 0
— (never reaches "true || ...")
The fix (PR #267) handles and and or before the general path, and decides from the left side alone:
let l = eval_expr(left, ...)?;
if the operator is "and" or "or":
if (and and l is false) or (or and l is true):
answer l, without ever looking at the right
otherwise:
compute the right, require a boolean, answer its value
After:
$ printf '[{"s":"abc"},{"s":""}]' | verbosec guard.verbose --run first_byte_or_empty --stdin --json
[{"out":1},{"out":1}]
Two details that matter. First, source verification still looks at both sides: types, declared reads, proofs. A runtime guard does not excuse a type error in the branch it protects. Second, the native binary compiled before and after the fix is byte-identical (585 bytes, cmp sees no difference). The fix touched only the interpreter, and that is measurable.
WASM: an "or" made with a bitwise OR
Verbose's WebAssembly backend cannot read a byte out of a text yet. So take another guard of the same kind, with a division:
ok = i.n == 0 or 10 / i.n > 0 "n is zero, or ten divided by n is positive"
With n = 0 the left side is true, and the division by zero on the right should never happen. The module from before, 59 bytes, run in Node:
safe_ratio(0) -> trap: divide by zero
safe_ratio(5) = 1
And here is why, in the module itself, disassembled to text:
BEFORE (59 bytes) AFTER (65 bytes)
───────────────── ────────────────
local.get 0 ;; n local.get 0 ;; n
i64.const 0 i64.const 0
i64.eq ;; left: n == 0 i64.eq ;; left: n == 0
i64.extend_i32_u i64.extend_i32_u
i64.const 10 i64.eqz ;; is the left false?
local.get 0 if (result i64)
i64.div_s ;; ← 10 / 0: trap i64.const 10
i64.const 0 local.get 0
i64.gt_s i64.div_s ;; only here
i64.extend_i32_u i64.const 0
i64.or ;; combine both i64.gt_s
i32.wrap_i64 i64.extend_i32_u
else
i64.const 1 ;; true, no division
end
i32.wrap_i64
On the left, "or" is translated as i64.or, a bitwise OR between two numbers. To have two numbers you must compute both first: the division happens every time. That is "everything first", written in bytecode.
On the right (PR #270), an if that carries a result. The division lives in the branch that only runs when the left side is false. Six more bytes per "or". No temporary variable, no memory, just a switch:
safe_ratio(0) = 1
safe_ratio(5) = 1
The fourth place: inside the compiler
One executor remained that nobody thinks about, because it does not run when the program runs: the compiler itself.
When an expression depends only on constants, the compiler computes it once and puts the result in the binary. That is constant folding: 2 + 3 becomes 5 before the program even exists. A good idea. Except when the compiler also folds what the program would never have computed:
ok = 1 == 1 or (-9223372036854775807 - 1) / -1 > 0
The left side is always true. The right side divides the smallest 64-bit integer by minus one, an operation with no result (it overflows a 64-bit integer), which must therefore never happen. It has no reason to: the left side has already answered.
Before PR #268, compiling this line natively gave:
thread '<unnamed>' panicked at src/optimizer.rs:614:51:
attempt to divide with overflow
It is not the program crashing. It is the compiler, busy "preparing" a branch the program would have skipped. The optimiser had decided on its own that anything constant can be computed ahead of time. The corrected rule is more modest: a computation that can fail and has no valid result stays an operation, and it is the control flow, with its short-circuit, that decides whether it runs. Same for computation * 0: the value will be zero, but if computation can fail, it must still be evaluated, in its place.
After:
$ ./fold-after 1
true
A 480-byte native binary that holds the division only in the branch that is never taken.
What it teaches
Three executors, plus a fourth hidden in the compiler. Only one was right. The other three gave "or" the right value every time they got to the end, and got the order wrong. You do not see this kind of gap by testing cases that work: "abc" passed everywhere. You need the case the guard exists to protect, the empty text, the zero divisor, pushed through every path.
That is what Verbose's tests do now: a complete truth table, empty texts, a NUL, multi-byte UTF-8, nested guards, skipped divisions and required ones, run on the real WASM modules in Node and compared with the interpreter. And, as a reverse check, the 194-example corpus compiled before and after: 190 native binaries byte-identical, and the four refusals unchanged.
The limit, named as usual. WebAssembly still cannot read a byte out of a text, hence the division in the example. The interpreter and native code do not yet treat arithmetic overflow the same way, and the documentation says so instead of claiming full parity. And Verbose still has no tag since v0.10.0, about a hundred and forty-four commits further on.
An "or" does not only ask whether one of the two is true. It promises not to look at the second once the first has answered. Three translations out of four had forgotten the promise.
French original on arcker.org.
Top comments (0)