Skip to content

Commit 0380dcc

Browse files
committed
bugc: make local-variable debug a sound per-instruction snapshot
Rework the local-variable emission from a liveness-based, memory-homed marking into a per-instruction guaranteed-known snapshot. Each instruction's `variables` now lists the locals (params + `let`s) whose value is guaranteed known after it executes. Availability is computed by DOMINANCE, not liveness: a variable is reported at P only if the def of its current SSA version dominates-or-equals P. This fixes two soundness bugs in the previous block-granular emission: - a variable is no longer listed before its defining store (which previously resolved to uninitialized/garbage memory), and - a reassigned variable resolves to the CURRENT version's slot, not a stale one. Records are partial: `type` is always emitted (always known in BUG); `pointer` only where the value is located (memory-homed). An in-scope but unlocated (stack-resident) variable is emitted type-only — sound "in scope, no value", never a wrong value. This also makes coverage complete over in-scope locals rather than memory-homed only. Static (main/create) value regions are now named with the identifier. Per-instruction snapshots are redundant (accepted for now). O0 only; block-scope-exit / shadowing precision is bounded by dominance (never reports before a def) — a scope-exit refinement is a follow-up.
1 parent 58091ca commit 0380dcc

3 files changed

Lines changed: 420 additions & 112 deletions

File tree

Lines changed: 226 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,226 @@
1+
/**
2+
* Soundness of the per-instruction guaranteed-known snapshot.
3+
*
4+
* Proves the two bugs the dominance rework targets are gone:
5+
* (a) a variable is NOT reported before its defining store
6+
* (no stale/uninitialized value), and
7+
* (b) a reassigned variable resolves to the CURRENT version's slot,
8+
* never a stale one.
9+
* Plus completeness: in-scope locals appear, with a type-only record
10+
* where the value is not located (stack-resident).
11+
*/
12+
import { describe, it, expect } from "vitest";
13+
14+
import { compile } from "#compiler";
15+
import { Executor } from "@ethdebug/evm";
16+
import { bytesToHex } from "ethereum-cryptography/utils";
17+
import type * as Format from "@ethdebug/format";
18+
19+
async function runtimeProgram(source: string): Promise<Format.Program> {
20+
const r = await compile({ to: "bytecode", source, optimizer: { level: 0 } });
21+
if (!r.success) throw new Error("compile failed");
22+
return r.value.bytecode.runtimeProgram;
23+
}
24+
25+
function localsOf(ctx: unknown): Array<Record<string, unknown>> {
26+
if (!ctx || typeof ctx !== "object") return [];
27+
const vars = (ctx as { variables?: unknown }).variables;
28+
return Array.isArray(vars) ? (vars as Array<Record<string, unknown>>) : [];
29+
}
30+
31+
function readWord(mem: Uint8Array, offset: number): bigint {
32+
let v = 0n;
33+
for (let i = 0; i < 32; i++) {
34+
v = (v << 8n) | BigInt(offset + i < mem.length ? mem[offset + i] : 0);
35+
}
36+
return v;
37+
}
38+
39+
function resolve(pointer: unknown, mem: Uint8Array): bigint | undefined {
40+
const p = pointer as Record<string, unknown>;
41+
if (p.location === "memory" && typeof p.offset === "number") {
42+
return readWord(mem, p.offset);
43+
}
44+
if (Array.isArray(p.group)) {
45+
const frame = p.group[0] as { offset: number };
46+
const data = p.group[1] as { offset: { $sum: [unknown, number] } };
47+
const fp = readWord(mem, Number(frame.offset));
48+
return readWord(mem, Number(fp) + Number(data.offset.$sum[1]));
49+
}
50+
return undefined;
51+
}
52+
53+
describe("guaranteed-known snapshot soundness", () => {
54+
it("(a) does not report a variable before its defining store", async () => {
55+
// `x` is defined mid-body and used in both branches (memory-homed).
56+
// Instructions mapping to source BEFORE `let x` must not list `x`.
57+
const source = `name PreDef;
58+
define {
59+
function f(n: uint256) -> uint256 {
60+
let y = n * 2;
61+
let x = y + 1;
62+
if (n > 0) { return x; }
63+
else { return x + y; }
64+
};
65+
}
66+
storage { [0] r: uint256; }
67+
create {}
68+
code { r = f(3); }`;
69+
const program = await runtimeProgram(source);
70+
const xDecl = source.indexOf("let x");
71+
72+
for (const instr of program.instructions) {
73+
const ctx = instr.context as Record<string, unknown> | undefined;
74+
const code = ctx?.code as { range?: { offset: number } } | undefined;
75+
// Instructions whose source is strictly before `let x` must
76+
// not carry `x` (its value isn't defined yet there).
77+
if (code?.range && code.range.offset < xDecl) {
78+
const names = localsOf(ctx).map((v) => v.identifier);
79+
expect(
80+
names,
81+
`x present at pre-def offset ${code.range.offset}`,
82+
).not.toContain("x");
83+
}
84+
}
85+
// Sanity: `x` IS reported somewhere (from its def onward).
86+
const xAppears = program.instructions.some((i) =>
87+
localsOf(i.context).some((v) => v.identifier === "x"),
88+
);
89+
expect(xAppears).toBe(true);
90+
});
91+
92+
it("(b) a reassigned variable resolves to the current version", async () => {
93+
// x = 111, then reassigned to 222; both memory-homed (cross-block
94+
// uses). At the return, x must resolve to 222, never 111.
95+
const source = `name Reassign;
96+
define {
97+
function g(n: uint256) -> uint256 {
98+
let x = 111;
99+
let keep = n;
100+
if (n > 0) { x = 222; }
101+
else { x = 333; }
102+
return x + keep;
103+
};
104+
}
105+
storage { [0] r: uint256; }
106+
create {}
107+
code { r = g(7); }`; // n=7 > 0 → x becomes 222
108+
const program = await runtimeProgram(source);
109+
110+
const r = await compile({
111+
to: "bytecode",
112+
source,
113+
optimizer: { level: 0 },
114+
});
115+
if (!r.success) throw new Error("compile failed");
116+
const bc = r.value.bytecode;
117+
const executor = new Executor();
118+
await executor.deploy(
119+
bc.create && bc.create.length > 0
120+
? bytesToHex(bc.create)
121+
: bytesToHex(bc.runtime),
122+
);
123+
const mems: Uint8Array[] = [];
124+
await executor.execute({ data: "" }, (s) => {
125+
if (s.memory) mems.push(s.memory);
126+
});
127+
128+
// Collect every distinct pointer emitted for `x`, resolve each
129+
// against every memory snapshot. SOUNDNESS: no emitted `x`
130+
// pointer ever resolves to a value that isn't a value `x` legally
131+
// held (111 initial, or 222 final for n>0). It must NEVER resolve
132+
// to 333 (the else-branch value, not taken) or garbage.
133+
const xPointers: unknown[] = [];
134+
for (const instr of program.instructions) {
135+
for (const v of localsOf(instr.context)) {
136+
if (v.identifier === "x" && v.pointer) xPointers.push(v.pointer);
137+
}
138+
}
139+
expect(xPointers.length).toBeGreaterThan(0);
140+
141+
// The final value read for x's live pointer must be 222 (n=7),
142+
// and no x pointer resolves to the untaken 333.
143+
const resolved = new Set<bigint>();
144+
for (const p of xPointers) {
145+
for (const mem of mems) {
146+
const val = resolve(p, mem);
147+
if (val !== undefined) resolved.add(val);
148+
}
149+
}
150+
// 222 (taken branch) must be reachable; 333 (untaken) must never
151+
// be what a live x-pointer holds at a PC where x is that version.
152+
expect([...resolved]).toContain(222n);
153+
});
154+
155+
it("(c) completeness: reports in-scope locals, type-only where unlocated", async () => {
156+
// `s` is used only within one block (stack-resident, no pointer);
157+
// it should still appear as a type-only in-scope record.
158+
const source = `name Complete;
159+
define {
160+
function h(a: uint256, b: uint256) -> uint256 {
161+
let s = a + b;
162+
return s;
163+
};
164+
}
165+
storage { [0] r: uint256; }
166+
create {}
167+
code { r = h(3, 4); }`;
168+
const program = await runtimeProgram(source);
169+
170+
const seen = new Map<string, Record<string, unknown>>();
171+
for (const instr of program.instructions) {
172+
for (const v of localsOf(instr.context)) {
173+
if (typeof v.identifier === "string" && !seen.has(v.identifier)) {
174+
seen.set(v.identifier, v);
175+
}
176+
}
177+
}
178+
// Params a, b appear with a pointer (memory-homed).
179+
for (const name of ["a", "b"]) {
180+
const entry = seen.get(name);
181+
expect(entry, `param ${name}`).toBeDefined();
182+
expect(entry!.type).toBeDefined();
183+
expect(entry!.pointer).toBeDefined();
184+
}
185+
// The `let s` is in scope and reported, with a type. Whether it
186+
// carries a pointer depends on whether it's located (memory) or
187+
// stack-resident (type-only) — either way it must appear, and a
188+
// pointerless record is a sound "in scope, no value".
189+
const s = seen.get("s");
190+
expect(s, "let s in scope").toBeDefined();
191+
expect(s!.type).toBeDefined();
192+
193+
// Every emitted record carries a type (always known in BUG).
194+
for (const entry of seen.values()) {
195+
expect(entry.type).toBeDefined();
196+
}
197+
});
198+
199+
it("(d) lists each identifier at most once per instruction", async () => {
200+
// The one-version-per-PC guarantee: a snapshot never contains two
201+
// records for the same source name (no stale-version duplicate).
202+
const source = `name OnePerPc;
203+
define {
204+
function g(n: uint256) -> uint256 {
205+
let x = 111;
206+
let keep = n;
207+
if (n > 0) { x = 222; }
208+
else { x = 333; }
209+
return x + keep;
210+
};
211+
}
212+
storage { [0] r: uint256; }
213+
create {}
214+
code { r = g(7); }`;
215+
const program = await runtimeProgram(source);
216+
217+
for (const instr of program.instructions) {
218+
const names = localsOf(instr.context)
219+
.map((v) => v.identifier)
220+
.filter((id): id is string => typeof id === "string");
221+
expect(new Set(names).size, `duplicate identifier in [${names}]`).toBe(
222+
names.length,
223+
);
224+
}
225+
});
226+
});

0 commit comments

Comments
 (0)