▼evm-redex:   An Executable EVM Specification in PLT Redex
On this page:
current-frame-tracer
current-call-observer
Racket
  top  contents    up   

4 Tracing hook🔗ℹ

parameter

(current-frame-tracer)

 → 
(or/c #f (-> exact-nonnegative-integer?
             (listof byte?)
             (or/c 'runtime 'init)
             (or/c #f (-> exact-nonnegative-integer? byte? any/c any))))
(current-frame-tracer tracer) → void?
  tracer : 
(or/c #f (-> exact-nonnegative-integer?
             (listof byte?)
             (or/c 'runtime 'init)
             (or/c #f (-> exact-nonnegative-integer? byte? any/c any))))
 = #f
Exported by (require evm-redex). The one hook into the execution loop: it reports which instruction each frame actually executed, which is the one fact a tool outside the library cannot reconstruct for itself. Coverage measurement is built on it — the harness lives under "tests/" (in "tests/coverage/"), since it is a way of using the semantics rather than part of them.

When set, the tracer is called once per frame with the frame’s code address, its code, and whether that code is the one installed at the address ('runtime) or a constructor’s init code ('init). It returns either #f (do not trace this frame) or a procedure, which is then called once per step with the pc, the opcode, and the machine after the step — enough to see which way a JUMPI went.

It sits in the driver loop (run / run-trace) rather than in either executor, and that placement is the whole design:

  • Every frame passes through it — the top frame, each CALL/DELEGATECALL/STATICCALL child, and a CREATE’s init code all re-enter run — so nested calls are traced for free.

  • It is oblivious to which backend ran the step, so a trace is identical under EVM_EXEC_BACKEND=spec, and the EVM_ORACLE differential (which runs a step through both executors) does not report it twice.

  • Nothing is added to the machine term, so the Redex/Racket differential oracle and the exec metafunction cache are untouched.

The parameter is read once per frame, not per step: with no tracer installed the per-step cost is a single test of a local #f, which is not measurable.

parameter

(current-call-observer) → (or/c #f procedure?)

(current-call-observer observer) → void?
  observer : (or/c #f procedure?)
 = #f
Exported by (require evm-redex). A coarser companion to current-frame-tracer, fired at each nested CALL/CREATE boundary rather than each step — which is exactly a call tree. When set it is called on 'enter as (observer 'enter kind caller callee value gas depth) and on 'exit as (observer 'exit success? gas-left output); enter/exit nest as a well-formed tree. The simulator’s call trace (#lang evm-redex/sim — simulating transactions) is built on it. Like the frame tracer it lives at the run boundary — backend-agnostic, off by default (cost is one test of a local #f per call), and outside the machine term. Pre-execution failures (depth limit, insufficient balance) that never spawn a child frame are not reported.

  top  contents    up