Trace globals

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 `<optimized out>`.
+
+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 `<globalInst>` 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
 

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 = [

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]

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]:
         <instrs> #traceInstr(I, POS)
-              => #appendFileJSONLn(PATH, generateInstrTrace(I, POS, STACK, LOCALS, MEM, PM))
+              => #appendFileJSONLn(
+                    PATH,
+                    generateInstrTrace(I, POS, STACK, LOCALS, MEM, PM, moduleGlobals(CUR))
+                 )
                  ...
         </instrs>
         <ioDir> PATH </ioDir>
@@ -74,16 +76,21 @@ The `traceInstr` rule performs the actual logging. It:
         <prevMem> PM => MEM </prevMem>
 
     // 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]:
         <instrs> #traceInstr(I, POS)
-              => #appendFileJSONLn(PATH, generateInstrTrace(I, POS, STACK, LOCALS, .SparseBytes, .SparseBytes))
+              => #appendFileJSONLn(
+                    PATH,
+                    generateInstrTrace(I, POS, STACK, LOCALS, .SparseBytes, .SparseBytes, moduleGlobals(CUR))
+                 )
                  ...
         </instrs>
         <ioDir> PATH </ioDir>
         <valstack> STACK </valstack>
         <locals> LOCALS </locals>
+        <curModIdx> CUR </curModIdx>
       [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 `<moduleInst>` and `<globalInst>` 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 `<curModIdx>` 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) ]]
+         <moduleInst>
+           <modIdx> MODIDX </modIdx>
+           <globalAddrs> GADDRS </globalAddrs>
+           ...
+         </moduleInst>
+
+    // No module instance to read globals from: `<curModIdx>` is `.Int`, or names a module
+    // with no `<moduleInst>`. Reports no globals rather than leaving the record unevaluated.
+    rule moduleGlobals(_) => .Map   [owise]
+```
+
+`globalVals` resolves `<globalAddrs>` (module index |-> `<gAddr>`) to module index |-> `Val`,
+looking up each `<globalInst>` 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) ]]
+         <globalInst>
+           <gAddr>  GADDR </gAddr>
+           <gValue> VAL   </gValue>
+           ...
+         </globalInst>
+```
+
+An address with no `<globalInst>` is skipped rather than reported as `null`, which a
+consumer would read as a value. `allocglobal` adds the address to `<globalAddrs>` and the
+`<globalInst>` to `<globals>` 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,15 +499,17 @@ 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)
       => {
           "kind"     : "hostCall" ,
           "module"   : MOD ,
           "function" : FUNC ,
-          "locals"   : Locals2JSON(LOCALS)
+          "locals"   : ValMap2JSON(LOCALS)
       }
 
     syntax JSON ::= generateContractDataTrace(ContractId, StorageType, String, List)   [function]

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 `<optimized out>`. The index space matters: DWARF's
+`DW_OP_WASM_location` global operand is a module index, not the store-level
+`<gAddr>` 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 <gAddr> 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)