Tolk: `@pure` function can mutate global fields; call then DCE’d

[Gusarich]

The purity checker misses writes to fields of global variables (e.g. gTens.0 = 888). This allows a function annotated @pure to still emit a global write at runtime. Because calls to @pure functions are treated as removable when their results are unused, DCE can then delete the call and silently remove the global mutation.

Reproduction

Create /tmp/tolk_pure_global_field_mutation_dce.tolk:

tolk 1.0

fun onInternalMessage() { return 0; }

global gTens: (int, int);

@noinline
fun set0_impure() {
    gTens.0 = 777;
}

@pure
@noinline
fun set0_pure() {
    gTens.0 = 888;
}

@method_id(100)
fun call_impure(): int {
    gTens = (1, 2);
    set0_impure();
    return gTens.0;
}

@method_id(101)
fun call_pure(): int {
    gTens = (1, 2);
    set0_pure(); // compiled as removable pure call
    return gTens.0;
}

Compile:

./artifacts/tolk /tmp/tolk_pure_global_field_mutation_dce.tolk > /tmp/tolk_pure_global_field_mutation_dce.fif

Create /tmp/tolk_pure_global_field_mutation_dce_runner.fif:

"/tmp/tolk_pure_global_field_mutation_dce.fif" include <s constant code
100 code 1 runvmx abort"exitcode is not 0" .s cr { drop } depth 1- times
101 code 1 runvmx abort"exitcode is not 0" .s cr { drop } depth 1- times

Run:

./artifacts/fift -I artifacts/lib /tmp/tolk_pure_global_field_mutation_dce_runner.fif

Observed output

777
1

Expected behavior

At minimum, @pure should forbid global writes:

• The compiler should reject gTens.0 = 888 inside @pure with an “impure operation in a pure function” error.

If such writes are allowed, then the call must not be DCE-removable:

• call_pure() should return 888, not 1.

[artyr58]

Hh