Repeated Array.sub of the same array and index retains a redundant bounds check

[tanyongkiam]

Summary

Two consecutive safe array reads using the same array and index retain two
identical bounds checks, even when there is no intervening call, store, or other
mutation. The compiler does eliminate the duplicate element load, but not the
second check and its failure branch.

This is a realistic missed optimization for code that reuses an array element
within an expression or basic block. In a small x64-64 benchmark, manually
binding the element once made the loop 1.44–1.56× faster.

Reproducer

Repeated source form:

fun get_twice a i = Array.sub a i + Array.sub a i;

fun repeat n a acc =
  if n = 0 then acc
  else repeat (n - 1) a (acc + get_twice a 5);

fun main () =
  let
    val n = Option.valOf
      (Int.fromString (List.hd (CommandLine.arguments ())))
    val a = Array.tabulate 10 (fn i => i)
  in
    print_int (repeat n a 0);
    print "\n"
  end;

main ();

Source-hoisted control:

fun get_twice a i =
  let val x = Array.sub a i
  in x + x end;

fun repeat n a acc =
  if n = 0 then acc
  else repeat (n - 1) a (acc + get_twice a 5);

fun main () =
  let
    val n = Option.valOf
      (Int.fromString (List.hd (CommandLine.arguments ())))
    val a = Array.tabulate 10 (fn i => i)
  in
    print_int (repeat n a 0);
    print "\n"
  end;

main ();

Compile both normally for x64-64 and run each with argument 100000000.
For example, from an x64-64 build directory:

./cake < repeated.cml > repeated.S
cc -O2 repeated.S basis_ffi.c -lm -o repeated
./repeated 100000000

Three paired runs gave:

Form	Run 1	Run 2	Run 3
Repeated Array.sub	0.58 s	0.59 s	0.39 s
Source-hoisted element	0.38 s	0.41 s	0.25 s

Both programs print the same result. The paired slowdown of the repeated form
was 1.44–1.56×. Exact timings will vary; the generated-code difference below is
the primary evidence.

The measurements used CakeML
535ff9fb8b11b2f49662e21b3f95401ea5f8ed0e. The relevant lowering files are
unchanged at 0fe74ee25d03a7d6d72892927edcaf5ae9677e10.

Generated-code evidence

For the repeated form, get_twice contains:

1. one load of the array header/length;
2. a bounds comparison and branch to the Subscript path;
3. one load of the selected element;
4. the same bounds comparison and another branch to the Subscript path;
5. the addition of the already-loaded element to itself.

There is no call, store, index change, or array change between the two checks.
The two relevant x64 fragments are:

cmp    %r8,%rax
jb     <first-success>
...
<first-success>:
...
mov    0x8(%rdx),%rdx
cmp    %r8,%rax
jb     <second-success>
...

The source-hoisted control has one header/length load, one bounds check, and one
element load. In this build, the repeated get_twice body was 172 bytes versus
148 bytes for the control.

Safe Array.sub is still represented explicitly as a bounds test followed by
the element read when it enters ClosLang
(flat_to_closScript.sml).
The check is expanded into a header load and unsigned comparison during
DataLang-to-WordLang lowering
(data_to_wordScript.sml).

Expected result

When a safe access to the same array and index is dominated by an already
successful identical check, and nothing relevant has changed, the second check
should be eliminated. The generated code should retain one element load and one
possible Subscript path for this example.

Useful regression coverage would include:

• the direct repeated-access example above;
• checks dominated through a simple successful branch;
• changed array or index values, for which the earlier check is insufficient;
• intervening calls or mutations, according to the chosen analysis policy;
• the corresponding vector, byte-array, byte-vector, and string operations.

Design note

This report intentionally does not prescribe an IR or pass. The semantic bounds
operation exists at several higher levels and becomes a machine comparison
later, so local path facts, common-subexpression treatment, range analysis, and
other designs are all plausible. The requested outcome is the removal of
provably redundant checks while preserving Subscript behavior.

Written by Codex (OpenAI).