diff --git a/docs/tracing.md b/docs/tracing.md index bc852d3..ad535cc 100644 --- a/docs/tracing.md +++ b/docs/tracing.md @@ -46,6 +46,21 @@ For the formal specification of how each value and type is serialized, see [`jso | `instr` | array | The instruction and its operands encoded as a JSON array. The first element is the instruction name, followed by its operands, e.g. `i64.const 255` is encoded as `["const", "i64", 255]`. | | `stack` | array | The value stack at the time of execution. Each entry is a `[type, value]` pair, e.g. `["i64", 4]`. | | `locals` | object | The local variable bindings at the time of execution, keyed by index. Each value is a `[type, value]` pair. | +| `globals`| object | The executing module's WebAssembly globals, keyed by **module-relative index**. Each value is a `[type, value]` pair, like `locals`. See [Globals](#globals) below. | + +### Globals + +Every instruction record carries the executing module's globals. Unlike `mem` this is repeated in full on every record and is never `null`: a module has only a handful of globals, so a consumer reads them off the current record with no scan. + +```json +{"pos": 605, "instr": ["local.get", 0], "stack": [], "locals": {}, "globals": {"0": ["i32", 1048560]}} +``` + +The keys are **module-relative** global indices — the index space DWARF's `DW_OP_WASM_location` global operand uses — not the store-level global addresses the semantics allocate. A debugger can therefore index the object directly with a DWARF global index. This is what lets it resolve Rust variables whose location, or whose frame base, reads a global instead of the shadow stack in linear memory; at `-O0` that is `__stack_pointer`, so without this field those variables read as ``. + +A global appears only once it has been allocated, which happens after its own *initializer* has been evaluated. So the records that evaluate a module's initializers report the globals declared before them and not the one being defined: the first such record carries `{}`, the second carries global 0, and so on. + +The values are read live from the `` cells at each traced instruction — see `tracing.md`'s *Reading Globals*. Nothing is mirrored and no `wasm-semantics` rule is shadowed, so the reported values cannot drift from the real ones. ### Example diff --git a/pyproject.toml b/pyproject.toml index b375bb8..747cf87 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "komet" -version = "0.1.87" +version = "0.1.88" description = "K tooling for the Soroban platform" requires-python = "~=3.10" dependencies = [ diff --git a/src/komet/kdist/soroban-semantics/json-utils.md b/src/komet/kdist/soroban-semantics/json-utils.md index 8683517..2997301 100644 --- a/src/komet/kdist/soroban-semantics/json-utils.md +++ b/src/komet/kdist/soroban-semantics/json-utils.md @@ -244,17 +244,17 @@ Additional elements carry the instruction's operands — types, operator names ( These functions serialize the runtime state captured at each trace point. -`Locals2JSON` serializes the local variable map as a JSON object, with local indices as string keys and their values serialized with `Val2JSON`. +`ValMap2JSON` serializes an index-keyed map of wasm values as a JSON object, with the indices as string keys and the values serialized with `Val2JSON`. It serves both the `locals` and the `globals` fields of a trace record — locals are keyed by local index, globals by module-relative global index. `ValStack2JSON` serializes the value stack as a JSON array, preserving the stack order from top to bottom. ```k - syntax JSON ::= Locals2JSON(Map) [function] - syntax JSONs ::= Locals2JSONs(Map) [function] + syntax JSON ::= ValMap2JSON(Map) [function] + syntax JSONs ::= ValMap2JSONs(Map) [function] // -------------------------------------------------- - rule Locals2JSON( M:Map ) => { Locals2JSONs(M) } - rule Locals2JSONs( .Map) => .JSONs - rule Locals2JSONs( (I:Int |-> V:Val) REST:Map ) => Int2String(I) : Val2JSON(V), Locals2JSONs( REST ) + rule ValMap2JSON( M:Map ) => { ValMap2JSONs(M) } + rule ValMap2JSONs( .Map) => .JSONs + rule ValMap2JSONs( (I:Int |-> V:Val) REST:Map ) => Int2String(I) : Val2JSON(V), ValMap2JSONs( REST ) syntax JSON ::= ValStack2JSON(ValStack) [function, total] syntax JSONs ::= ValStack2JSONs(ValStack) [function, total] diff --git a/src/komet/kdist/soroban-semantics/tracing.md b/src/komet/kdist/soroban-semantics/tracing.md index 99ad305..c16c19d 100644 --- a/src/komet/kdist/soroban-semantics/tracing.md +++ b/src/komet/kdist/soroban-semantics/tracing.md @@ -46,15 +46,17 @@ Two internal instructions drive the tracing mechanism: ### Logging -The `traceInstr` rule performs the actual logging. It: - -1. Generates the trace data for instruction `I` using the current value stack and locals. -2. Appends it as a JSON record to the trace file. +`traceInstr` generates the trace data for instruction `I` from the current value stack, +locals, memory and globals, and appends it as a JSON record to the trace file. Globals come +from `moduleGlobals(CUR)` (see *Reading Globals*). ```k rule [traceInstr]: #traceInstr(I, POS) - => #appendFileJSONLn(PATH, generateInstrTrace(I, POS, STACK, LOCALS, MEM, PM)) + => #appendFileJSONLn( + PATH, + generateInstrTrace(I, POS, STACK, LOCALS, MEM, PM, moduleGlobals(CUR)) + ) ... PATH @@ -74,16 +76,21 @@ The `traceInstr` rule performs the actual logging. It: PM => MEM // Fallback for programs without a linear memory (e.g. text-format tests): still - // trace, with an empty memory so `mem` is always `null`. Guarantees `#traceInstr` - // is always consumed even when the memory-matching rule above cannot fire. + // trace, with an empty memory so `mem` is always `null`. Guarantees `#traceInstr` is + // always consumed even when the memory-matching rule above cannot fire. Globals are + // still reported: `moduleGlobals` does not depend on there being a linear memory. rule [traceInstr-nomem]: #traceInstr(I, POS) - => #appendFileJSONLn(PATH, generateInstrTrace(I, POS, STACK, LOCALS, .SparseBytes, .SparseBytes)) + => #appendFileJSONLn( + PATH, + generateInstrTrace(I, POS, STACK, LOCALS, .SparseBytes, .SparseBytes, moduleGlobals(CUR)) + ) ... PATH STACK LOCALS + CUR [owise] ``` @@ -187,6 +194,60 @@ The `#resetAlreadyTraced` appended by `insert-traceInstr` after the `#block`/`#l [priority(20)] ``` +### Reading Globals + +`moduleGlobals(MODIDX)` returns module `MODIDX`'s globals as a `Map` of module-relative +index |-> `Val` — the same shape as `locals`, so `ValMap2JSON` serializes both. Module index +is the index space DWARF's `DW_OP_WASM_location` global operand uses, so a debugger can +index the object directly. + +These rules read `` and `` as [function +context](https://github.com/runtimeverification/k/blob/master/docs/user_manual.md#matching-global-context-in-function-rules). + +The argument is an `OptionalInt` so a caller can pass `` through unchanged. +Constraining it to `Int` would stop `traceInstr-nomem`'s `owise` from matching when no +module is current, wedging `#traceInstr` instead of tracing it. + +```k + syntax Map ::= moduleGlobals(modIdx: OptionalInt) [function] + // -------------------------------------------------------------- + rule [[ moduleGlobals(MODIDX:Int) => globalVals(GADDRS) ]] + + MODIDX + GADDRS + ... + + + // No module instance to read globals from: `` is `.Int`, or names a module + // with no ``. Reports no globals rather than leaving the record unevaluated. + rule moduleGlobals(_) => .Map [owise] +``` + +`globalVals` resolves `` (module index |-> ``) to module index |-> `Val`, +looking up each `` by its address. + +```k + syntax Map ::= globalVals(addrs: Map) [function] + // -------------------------------------------------- + rule globalVals(.Map) => .Map + + rule [[ globalVals((IDX:Int |-> GADDR:Int) REST) => (IDX |-> VAL) globalVals(REST) ]] + + GADDR + VAL + ... + +``` + +An address with no `` is skipped rather than reported as `null`, which a +consumer would read as a value. `allocglobal` adds the address to `` and the +`` to `` in a single step, so this should be unreachable; it exists so +that a dangling address cannot wedge the tracer. + +```k + rule globalVals((_IDX |-> _GADDR) REST) => globalVals(REST) [owise] +``` + ## Instruction Filter `shouldTraceInstr` filters out instructions that should not be traced in text format programs. @@ -401,24 +462,31 @@ Instruction records (`kind: "instr"`) have four further fields: lowercase hex), or `null` when memory is unchanged. Zero-gaps are omitted; a consumer reconstructs memory by taking the most recent non-`null` snapshot at or before the record and treating unwritten bytes as `0`. +- `globals` — the executing module's wasm globals, keyed by MODULE-RELATIVE index (a + decimal string, as with `locals`), each value a `[type, value]` pair. Unlike `mem` this + is repeated in full on every record and never `null`: a module has only a handful of + globals, so a consumer reads them off the current record with no scan. Each Soroban VM operation has its own set of fields, built by its own `generate*Trace` function below; see `docs/tracing.md` for the full format of each. Records are written one per line to the trace file. ```k - syntax JSON ::= generateInstrTrace(Instr, OptionalInt, ValStack, Map, SparseBytes, SparseBytes) [function] + syntax JSON ::= generateInstrTrace(Instr, OptionalInt, ValStack, locals: Map, SparseBytes, SparseBytes, globals: Map) [function] // --------------------------------------------------------- - rule generateInstrTrace(I:Instr, OFFSET, VS:ValStack, LOCALS:Map, MEM:SparseBytes, PM:SparseBytes) + rule generateInstrTrace(I:Instr, OFFSET, VS:ValStack, LOCALS:Map, MEM:SparseBytes, PM:SparseBytes, GLOBALS:Map) => { "kind" : "instr" , "pos" : #if OFFSET ==K .Int #then null #else {OFFSET}:>Int #fi , "instr" : Instr2JSON(I) , "stack" : ValStack2JSON(VS) , - "locals" : Locals2JSON(LOCALS) , + "locals" : ValMap2JSON(LOCALS) , // Full sparse snapshot of linear memory when it changed since the previous // snapshot, else `null` (memory unchanged — reuse the most recent snapshot). - "mem" : #if MEM ==K PM #then null #else [ memRuns(MEM, 0) ] #fi + "mem" : #if MEM ==K PM #then null #else [ memRuns(MEM, 0) ] #fi , + // Read by `moduleGlobals`, already keyed by module-relative index; the same + // index |-> Val shape as `locals`, so the same serializer applies. + "globals": ValMap2JSON(GLOBALS) } // Serializes a SparseBytes memory as a JSON array of `{ "addr", "bytes" }` runs, one @@ -431,7 +499,9 @@ Records are written one per line to the trace file. rule memRuns(SBChunk(#empty(N)) REST, OFF) => memRuns(REST, OFF +Int N) rule memRuns(SBChunk(#bytes(BS)) REST, OFF) => ({ "addr" : OFF , "bytes" : Bytes2Hex(BS) }, memRuns(REST, OFF +Int lengthBytes(BS))) +``` +```k syntax JSON ::= generateHostCallTrace(String, String, Map) [function] // ------------------------------------------------------------------------- rule generateHostCallTrace(MOD, FUNC, LOCALS) @@ -439,7 +509,7 @@ Records are written one per line to the trace file. "kind" : "hostCall" , "module" : MOD , "function" : FUNC , - "locals" : Locals2JSON(LOCALS) + "locals" : ValMap2JSON(LOCALS) } syntax JSON ::= generateContractDataTrace(ContractId, StorageType, String, List) [function] diff --git a/src/tests/integration/test_globals_tracing.py b/src/tests/integration/test_globals_tracing.py new file mode 100644 index 0000000..04da4b1 --- /dev/null +++ b/src/tests/integration/test_globals_tracing.py @@ -0,0 +1,132 @@ +"""Golden test for in-K per-step WebAssembly globals tracing. + +Deploys the `increment` example contract and invokes `increment(5)` with tracing +enabled, then asserts every instruction record carries a `globals` object: the +executing module's globals keyed by MODULE-RELATIVE global index. + +A debugger needs these to resolve Rust variables whose DWARF location (or whose +frame base) reads a global rather than the shadow stack in linear memory — at +-O0 that is the `__stack_pointer` global, so without this field those variables +degrade to ``. The index space matters: DWARF's +`DW_OP_WASM_location` global operand is a module index, not the store-level +`` the semantics allocate, so the two must not be confused. + +Companion to test_memory_tracing.py, which covers the `mem` field the same way. +""" + +from __future__ import annotations + +import json +from pathlib import Path + +from pyk.kast.inner import KSort +from pyk.ktool.krun import KRunOutput + +from komet.kasmer import Kasmer +from komet.kast.syntax import ( + account_id, + call_tx, + contract_id, + deploy_contract, + sc_u32, + set_account, + set_exit_code, + steps_of, + upload_wasm, +) +from komet.utils import concrete_tracing_definition + +WASM = Path(__file__).parent / 'data' / 'increment.wasm' + + +def _run_trace(tmp_path: Path) -> list[dict]: + trace_file = tmp_path / 'trace.jsonl' + kasmer = Kasmer(definition=concrete_tracing_definition(), trace_file=trace_file) + + contract = kasmer.kast_from_wasm(WASM) + steps = steps_of( + [ + set_exit_code(1), + upload_wasm(b'test', contract), + set_account(b'test-account', 9876543210), + deploy_contract(b'test-account', b'test-contract', b'test'), + call_tx( + account_id(b'test-account'), + contract_id(b'test-contract'), + 'increment', + [sc_u32(5)], + sc_u32(5), + ), + set_exit_code(0), + ] + ) + cmap, pmap = kasmer.config_vars() + proc = kasmer.concrete_definition.krun_with_kast( + steps, sort=KSort('Steps'), output=KRunOutput.KORE, cmap=cmap, pmap=pmap + ) + assert proc.returncode == 0, proc.stderr + assert trace_file.is_file(), 'no trace produced' + return [json.loads(line) for line in trace_file.read_text().splitlines() if line.strip()] + + +def _instruction_records(records: list[dict]) -> list[dict]: + """Instruction records carry a value stack; VM event records do not.""" + return [r for r in records if 'stack' in r] + + +def test_globals_field_present_and_wellformed(tmp_path: Path) -> None: + records = _run_trace(tmp_path) + instr = _instruction_records(records) + assert instr, 'expected instruction records' + + for record in instr: + assert 'globals' in record, f'instruction record missing globals: {record}' + globals_ = record['globals'] + assert isinstance(globals_, dict), f'globals must be an object: {globals_}' + for key, value in globals_.items(): + # Keys are decimal module-relative indices, as strings (like `locals`). + assert key.isdigit(), f'global key must be a decimal index: {key!r}' + # Values are [type, value] pairs, exactly like locals and stack entries. + assert isinstance(value, list) and len(value) == 2, f'bad global value: {value}' + assert isinstance(value[0], str), f'global type must be a string: {value}' + + +def test_globals_use_module_relative_indices(tmp_path: Path) -> None: + """The keys are module indices (dense from 0), not store-level addresses.""" + records = _run_trace(tmp_path) + instr = _instruction_records(records) + + seen_nonempty = False + for record in instr: + indices = sorted(int(k) for k in record['globals']) + if not indices: + continue + seen_nonempty = True + # A module's globals are indexed 0..n-1, so the set must be exactly that + # range. A store-level keying would drift once a second module + # (the Soroban host's own, or another contract) allocates globals. + assert indices == list(range(len(indices))), f'non-dense global indices: {indices}' + + assert seen_nonempty, 'expected at least one record with a global (the shadow-stack pointer)' + + +def test_shadow_stack_pointer_moves(tmp_path: Path) -> None: + """The contract's -O0 prologue moves __stack_pointer, so global 0 changes.""" + records = _run_trace(tmp_path) + instr = _instruction_records(records) + + values = [r['globals']['0'][1] for r in instr if '0' in r['globals']] + assert values, 'expected a global 0 (the shadow-stack pointer)' + assert len(set(values)) > 1, f'expected global 0 to change during execution, saw {set(values)}' + + +def test_globals_are_repeated_every_step(tmp_path: Path) -> None: + """Unlike `mem`, globals are never change-suppressed: there are only a few, + so a consumer reads them off the current record with no scan.""" + records = _run_trace(tmp_path) + instr = _instruction_records(records) + + # No record uses `null` to mean "unchanged" the way `mem` does. + assert all(r['globals'] is not None for r in instr) + # And the field is present on every single instruction record, not just some. + assert all('globals' in r for r in instr) diff --git a/uv.lock b/uv.lock index 83f4faa..d9596b5 100644 --- a/uv.lock +++ b/uv.lock @@ -679,7 +679,7 @@ wheels = [ [[package]] name = "komet" -version = "0.1.87" +version = "0.1.88" source = { editable = "." } dependencies = [ { name = "pykwasm" },