Reader monad

[ArkadySkv]

Refactor cmd_replay.ml: eliminate global mutable state using Reader monad

OCaml Version

• OCaml: 5.4.0 (same as project's main branch)
• Dependencies: No new dependencies added

Two Approaches Explored

1. Hybrid Approach (Closure-based local state)

let compile_file ~unsafe ~entry_point ~invoke_with_symbols filename model =
  (* Local mutable state *)
  let next = ref (-1) in
  let brk = ref 0l in
  let covered_labels = Hashtbl.create 16 in
  let scopes = ref Symbol_scope.empty in

  let add_sym i =
    let sym = Smtml.Symbol.(Fmt.str "symbol_%d" i @: Smtml.Ty.Ty_bitv 0) in
    scopes := Symbol_scope.symbol sym !scopes
  in

  let symbol_i32 () =
    let i = !next in
    incr next;
    match model.(i) with
    | Concrete_value.I32 n -> add_sym i; Ok n
    | v -> ...
  in
  (* ... *)

Description:

• Moved all mutable state (next, brk, covered_labels, scopes) to the local scope of compile_file.
• Kept helper functions as plain closures capturing the local state.
• Did not introduce a formal Reader monad.

Pros:

• Simple, straightforward refactoring.
• Eliminated global mutable state effectively.
• Minimal changes to existing code.

Cons:

• State management is implicit (via closures), not explicit.
• Harder to test functions in isolation.
• Does not fully align with the Reader monad pattern requested in Issue use a reader monad to re-implement replay #685.

Status: ✅ Tested and working, but abandoned in favor of a more principled approach.

---

2. Reader Monad + Local State (Final Approach)

let symbol_i32 () =
  let open Reader in
  let computation =
    bind get_next (fun i ->
      bind incr_next (fun () ->
        match model.(i) with
        | Concrete_value.I32 n ->
            bind (add_sym i) (fun () -> return n)
        | v -> ...
      )
    )
  in
  run_reader computation

Description:

• Defined a formal Reader module with:
  • type 'a t = env -> 'a Result.t
  • return, bind, run, ask
  • State accessors: get_next, incr_next, get_brk, set_brk, update_scopes, etc.
• Wrapped all symbol_* and alloc functions in the Reader monad.
• Kept cov_label_* and scope functions in Concrete_choice monad (required by FFI interface).
• env record holds all mutable state and is passed explicitly through the monad.

Pros:

• Explicit environment passing (Reader monad pattern).
• Better testability (functions can be tested with mock environments).
• Aligns with functional programming best practices.
• Meets the requirement of Issue use a reader monad to re-implement replay #685 to "use a reader monad".

Cons:

• More code (Reader module + explicit bind calls).
• Slightly more verbose than closures.

Status: ✅ Tested and working. Replay functionality remains intact.

---

🔬 Comparison of Approaches

Aspect	Hybrid (Closures)	Reader Monad (Final)
Global state eliminated	✅ Yes	✅ Yes
Explicit environment	❌ Implicit (closures)	✅ Explicit (env record)
Reader monad pattern	❌ Not formal	✅ Formal Reader module
Testability	🟡 Moderate	✅ High (mock environments)
Code complexity	🟢 Low	🟡 Moderate
Alignment with Issue #685	🟡 Partial	✅ Full
Replay functionality	✅ Intact	✅ Intact

Conclusion: The Reader monad approach is more principled, explicitly manages state, and fully addresses the issue's request. Although slightly more verbose, it improves testability and maintainability, making it the preferred solution.

---

🧪 Testing

Test File: test.wat

(module
  (func $check (param $x i32) (result i32)
    (if (i32.eq (local.get $x) (i32.const 0))
      (then (unreachable))
      (else (return (i32.const 1)))
    )
    (i32.const 0) ;; fallback, though unreachable will trap
  )
  (export "check" (func $check))
)

Step 1: Generate the Model File

Run symbolic execution to produce a model file that captures the concrete value leading to the trap:

./_build/default/src/bin/owi.exe sym \
  --model-out-file model.json \
  --model-format json \
  test.wat \
  --entry-point check \
  --invoke-with-symbols

This command explores the symbolic path where x == 0, causing unreachable, and saves the concrete value 0 for symbol_0 in model.json.

Step 2: Replay the Model

Replay the concrete execution using the generated model:

./_build/default/src/bin/owi.exe replay \
  --replay-file model.json \
  test.wat \
  --entry-point check

Expected Output

owi.exe: [ERROR] unreachable

This PR Closes #685

What This Proves

The replay command correctly reproduces the exact concrete path (and the trap) that was discovered during symbolic execution.

The refactoring (eliminating global mutable state and introducing the Reader monad) did not break replay functionality.

The model file (model.json) is correctly parsed and applied by the replay command.