Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,18 @@ All notable changes to EigenScript are documented here.
(the one legitimate empty-expression position) still yields `null` (#494).

### Fixed
- **`args` now rides the trace tape (#471).** The `args` builtin returned
`argv` directly, unwrapped — the last un-taped nondeterminism source
reachable by a pure script, and a hole in the closed-world invariant behind
deterministic replay. A program that branched on `args` recorded a tape
under one invocation and silently diverged when replayed under a different
argv (the exact class chaos-mode `--seed N` scheduling for the #408 task
layer would hit). The recorded argument list now rides the tape as one `N`
record and replay serves it regardless of the live argv. Because `args`
*builds* its list before returning, it uses the `TRACE_NONDET_TAKE` /
`TRACE_NONDET_RECORD` pair (not `TRACE_NONDET_RET`), so under replay the
live list is neither built nor leaked. Regression: `tests/test_replay.sh`
(record under `A B`, replay under `X Y Z`, recorded args win).
- **Circular `import` / `load_file` no longer crashes (#496).** A mutual or
self-referential `import` (a→b→a) or `load_file` used to recurse through
`vm_execute` until the C stack overflowed — SIGSEGV, `rc=139`, uncatchable.
Expand Down
9 changes: 8 additions & 1 deletion docs/TRACE.md
Original file line number Diff line number Diff line change
Expand Up @@ -57,12 +57,19 @@ perspective lands on the tape as an `N` record:
- **Time:** `monotonic_ns`, `monotonic_ms`
- **Environment / files:** `env_get`, `read_text`, `read_bytes`,
`read_bytes_buf`
- **Process:** `args` (command-line arguments — differ across
invocations, so the recorded list is served on replay regardless of
the live argv; #471)
- **HTTP extension:** `http_post` (success and all error paths),
`http_request_body`, `http_session_id`, `http_request_headers`

The hook is the `TRACE_NONDET_RET` macro in `src/trace.h`, used at
every nondet return site — adding a new nondet builtin means wrapping
its return in the same macro.
its return in the same macro. A builtin that *builds* its return value
(a list, buffer, or dict) before returning uses the `TRACE_NONDET_TAKE`
/ `TRACE_NONDET_RECORD` pair instead (`args` does): the early `TAKE`
short-circuits under replay before the value is built, so the live
construction is neither run nor leaked.

## Non-Replayable Builtins (issue #148)

Expand Down
15 changes: 13 additions & 2 deletions src/builtins.c
Original file line number Diff line number Diff line change
Expand Up @@ -1915,15 +1915,26 @@ void eigenscript_set_args(int argc, char **argv) {
g_argv = argv;
}

/* args of null → list of command-line arguments (after the script name) */
/* args of null → list of command-line arguments (after the script name).
*
* argv is a nondeterminism source across invocations (the closed-world
* replay invariant, #471): a program that branches on args records under
* one argv and would silently diverge when replayed under another. So the
* built list rides the tape as one N record and replay serves the recorded
* list regardless of the live argv. The construction happens before the
* return value exists, so this uses the TAKE/RECORD pair rather than
* TRACE_NONDET_RET — under replay the early TAKE short-circuits before the
* list is built, avoiding both the wasted work and the abandoned (leaked)
* live list. */
Value* builtin_args(Value *arg) {
(void)arg;
TRACE_NONDET_TAKE("args");
Value *list = make_list(g_argc > 2 ? g_argc - 2 : 0);
/* g_argv[0] = eigenscript, g_argv[1] = script.eigs, g_argv[2..] = user args */
for (int i = 2; i < g_argc; i++) {
list_append_owned(list, make_str(g_argv[i]));
}
return list;
TRACE_NONDET_RECORD("args", list);
}

/* ---- Path manipulation ---- */
Expand Down
20 changes: 20 additions & 0 deletions tests/test_replay.sh
Original file line number Diff line number Diff line change
Expand Up @@ -290,6 +290,26 @@ else
fail "stale EIGS_REPLAY --version" "rc=$VRC out='$VOUT'"
fi

# ---- #471: args (argv) is a taped nondeterminism source ----
# Record the tape under one argv, then replay the SAME script under a
# DIFFERENT argv. The recorded args must win — a program that branches on
# args would otherwise silently diverge on replay (the closed-world hole).
cat > "$TMPDIR/p_args.eigs" <<'EOF'
print of (args of null)
EOF

TAPE_A="$TMPDIR/args.tape"
REC_A=$(EIGS_TRACE="$TAPE_A" "$EIGS" "$TMPDIR/p_args.eigs" A B 2>&1)
# Live (no replay) under the mutated argv — proves the tape actually overrides.
LIVE_A=$(EIGS_TRACE=/dev/null "$EIGS" "$TMPDIR/p_args.eigs" X Y Z 2>&1)
REP_A=$(EIGS_REPLAY="$TAPE_A" "$EIGS" "$TMPDIR/p_args.eigs" X Y Z 2>&1)

if [ "$REC_A" = '["A", "B"]' ] && [ "$REP_A" = '["A", "B"]' ] && [ "$LIVE_A" = '["X", "Y", "Z"]' ]; then
ok "args replay: recorded argv wins under EIGS_REPLAY with a mutated argv"
else
fail "args replay" "rec='$REC_A' live='$LIVE_A' rep='$REP_A'"
fi

echo
echo "REPLAY: $PASS passed, $FAIL failed"
[ "$FAIL" = "0" ] && exit 0 || exit 1
Loading