Add Instruction-Level Execution Tracing

[bbyalcinkaya]

Adds tracing semantics that write instruction-level execution logs to a specified output file. Each log entry is a JSON record containing the current instruction, its byte offset in the binary (if available), the value stack, and the local variables at the time of execution.

Changes

Semantics:

• Added conditional compilation (via md selectors) for tracing, provided as a separate build target soroban-semantics.llvm-tracing that does not affect the default soroban-semantics.llvm target.

In the tracing target:

• Added <trace> configuration cell that holds the tracing-related data.
• Added tracing.md — the core tracing module. It intercepts instructions during execution, logs the VM state at each traced instruction.
• Added fs.md — defines file operation functions used by the tracing module to append log records to the output file.
• Added json-utils.md — defines JSON serialization functions for WebAssembly values, types, operators, instructions, and runtime structures (value stack, locals).

CLI

• Added --trace-file option to komet run and komet test. When provided, it enables the tracing backend and directs trace output to the specified file. Currently only supported on the LLVM backend.

Usage

$ komet run --help
usage: komet run [-h] [--backend BACKEND] [--trace-file TRACE_FILE] PROGRAM
positional arguments:
  PROGRAM               path to test file
options:
  -h, --help            show this help message and exit
  --backend BACKEND     K backend to use
  --trace-file TRACE_FILE
                        Path to trace output

Example:

komet run --trace-file trace.txt src/tests/integration/data/errors.wast > out.txt

Example trace output (Click)

{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["block"],"stack":[],"locals":{}}
{"pos":null,"instr":["call",3],"stack":[],"locals":{}}
{"pos":null,"instr":["block"],"stack":[],"locals":{}}
{"pos":null,"instr":["call",6],"stack":[],"locals":{}}
{"pos":null,"instr":["block"],"stack":[],"locals":{}}
{"pos":null,"instr":["call",8],"stack":[],"locals":{}}
{"pos":null,"instr":["block"],"stack":[],"locals":{}}
{"pos":null,"instr":["call",7],"stack":[],"locals":{}}
{"pos":null,"instr":["block"],"stack":[],"locals":{}}
{"pos":null,"instr":["unreachable"],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i64",0],"stack":[],"locals":{}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["local.get",0],"stack":[],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["wrap_i64","i32"],"stack":[["i64",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["const","i32",255],"stack":[["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["and","i32"],"stack":[["i32",255],["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["local.tee",1],"stack":[["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["const","i32",2],"stack":[["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["lt_u","i32"],"stack":[["i32",2],["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["br_if",0],"stack":[["i32",1]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["const","i64",8589934595],"stack":[],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["const","i64",4294967299],"stack":[["i64",8589934595]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["local.get",1],"stack":[["i64",4294967299],["i64",8589934595]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["select"],"stack":[["i32",0],["i64",4294967299],["i64",8589934595]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i64",1],"stack":[],"locals":{}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["local.get",0],"stack":[],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["wrap_i64","i32"],"stack":[["i64",1]],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["const","i32",255],"stack":[["i32",1]],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["and","i32"],"stack":[["i32",255],["i32",1]],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["local.tee",1],"stack":[["i32",1]],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["const","i32",2],"stack":[["i32",1]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["lt_u","i32"],"stack":[["i32",2],["i32",1]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["br_if",0],"stack":[["i32",1]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["const","i64",8589934595],"stack":[],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["const","i64",4294967299],"stack":[["i64",8589934595]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["local.get",1],"stack":[["i64",4294967299],["i64",8589934595]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["select"],"stack":[["i32",1],["i64",4294967299],["i64",8589934595]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i64",0],"stack":[],"locals":{}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["local.get",0],"stack":[],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["wrap_i64","i32"],"stack":[["i64",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["const","i32",255],"stack":[["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["and","i32"],"stack":[["i32",255],["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["local.tee",1],"stack":[["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["const","i32",2],"stack":[["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["ge_u","i32"],"stack":[["i32",2],["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["br_if",0],"stack":[["i32",0]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["const","i64",8589934595],"stack":[],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["const","i64",4294967299],"stack":[["i64",8589934595]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["local.get",1],"stack":[["i64",4294967299],["i64",8589934595]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["select"],"stack":[["i32",0],["i64",4294967299],["i64",8589934595]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["call",5],"stack":[["i64",4294967299]],"locals":{"0":["i64",0],"1":["i32",0]}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",4294967299]}}
{"pos":null,"instr":["local.get",0],"stack":[],"locals":{"0":["i64",4294967299]}}
{"pos":null,"instr":["call",0],"stack":[["i64",4294967299]],"locals":{"0":["i64",4294967299]}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",4294967299]}}
{"pos":null,"instr":["hostCall","x","5"],"stack":[],"locals":{"0":["i64",4294967299]}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i64",1],"stack":[],"locals":{}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["local.get",0],"stack":[],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["wrap_i64","i32"],"stack":[["i64",1]],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["const","i32",255],"stack":[["i32",1]],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["and","i32"],"stack":[["i32",255],["i32",1]],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["local.tee",1],"stack":[["i32",1]],"locals":{"0":["i64",1],"1":["i32",0]}}
{"pos":null,"instr":["const","i32",2],"stack":[["i32",1]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["ge_u","i32"],"stack":[["i32",2],["i32",1]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["br_if",0],"stack":[["i32",0]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["const","i64",8589934595],"stack":[],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["const","i64",4294967299],"stack":[["i64",8589934595]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["local.get",1],"stack":[["i64",4294967299],["i64",8589934595]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["select"],"stack":[["i32",1],["i64",4294967299],["i64",8589934595]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["call",5],"stack":[["i64",8589934595]],"locals":{"0":["i64",1],"1":["i32",1]}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",8589934595]}}
{"pos":null,"instr":["local.get",0],"stack":[],"locals":{"0":["i64",8589934595]}}
{"pos":null,"instr":["call",0],"stack":[["i64",8589934595]],"locals":{"0":["i64",8589934595]}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",8589934595]}}
{"pos":null,"instr":["hostCall","x","5"],"stack":[],"locals":{"0":["i64",8589934595]}}

Another example with binary wasm:

komet test -C src/tests/integration/data/soroban/contracts/test_adder/ --id test_add --trace-file trace.txt --max-examples 1

Trace:

{"pos":3,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":11,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":19,"instr":["const","i32",1048576],"stack":[],"locals":{}}
{"pos":null,"instr":["const","i64",4],"stack":[],"locals":{}}
{"pos":null,"instr":["block"],"stack":[],"locals":{"0":["i64",4]}}
{"pos":597,"instr":["block"],"stack":[],"locals":{"0":["i64",4]}}
{"pos":599,"instr":["local.get",0],"stack":[],"locals":{"0":["i64",4]}}
{"pos":601,"instr":["const","i64",255],"stack":[["i64",4]],"locals":{"0":["i64",4]}}
{"pos":604,"instr":["and","i64"],"stack":[["i64",255],["i64",4]],"locals":{"0":["i64",4]}}
{"pos":605,"instr":["const","i64",4],"stack":[["i64",4]],"locals":{"0":["i64",4]}}
{"pos":607,"instr":["eq","i64"],"stack":[["i64",4],["i64",4]],"locals":{"0":["i64",4]}}
{"pos":608,"instr":["br_if",0],"stack":[["i32",1]],"locals":{"0":["i64",4]}}
{"pos":612,"instr":["const","i64",1],"stack":[],"locals":{"0":["i64",4]}}

Since this is a binary input, most lines have a pos field indicating the byte offset in the binary. The first three entries are part of the global initialization. The two entries with "pos": null are instructions inserted by the semantics during execution rather than decoded from the binary. The remaining lines show the execution of the function body.

Trace Format

Each line in the trace file is a JSON record with the following fields:

• pos — byte offset of the instruction in the binary, or null for instructions inserted by the semantics during execution.
• instr — the instruction and its operands.
• stack — the value stack at the time of execution.
• locals — the local variable bindings at the time of execution.

Limitations

Consecutive identical instructions may not be logged correctly for text format programs. This is a known limitation of the <lastTraced> deduplication mechanism. When two identical instructions appear back-to-back and the first does not leave or rewrite to an intermediate value in <instrs>, the second will not be logged. This does not affect binary format programs, where each instruction is wrapped with its position and traced unconditionally. See the comments in tracing.md for more details.