1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)

open Symbolic_value

module Make (Thread : Thread.S) = struct
  type err =
    | Assert_fail
    | Trap of Trap.t

  type 'a t =
    | M of (Thread.t -> Solver.t -> ('a, err) Prelude.Result.t * Thread.t)
  [@@unboxed]

  type 'a run_result = ('a, err) Prelude.Result.t * Thread.t

  let return v = M (fun t _sol -> (Ok v, t))

  let run (M v) st s : _ run_result = v st s

  let bind v f =
    M
      (fun init_s sol ->
        let v_final, tmp_st = run v init_s sol in
        match v_final with
        | Ok v_final -> run (f v_final) tmp_st sol
        | Error _ as e -> (e, tmp_st) )

  let ( let* ) = bind

  let map v f =
    let* v in
    return (f v)

  let ( let+ ) = map

  let select (vb : vbool) =
    let v = Smtml.Expr.simplify vb in
    match Smtml.Expr.view v with
    | Val True -> return true
    | Val False -> return false
    | _ -> Fmt.failwith "%a" Smtml.Expr.pp v

  let select_i32 (i : int32) =
    let v = Smtml.Expr.simplify i in
    match Smtml.Expr.view v with
    | Val (Num (I32 i)) -> return i
    | _ -> assert false

  let trap t = M (fun th _sol -> (Error (Trap t), th))

  let assertion (vb : vbool) =
    let v = Smtml.Expr.simplify vb in
    match Smtml.Expr.view v with
    | Val True -> return ()
    | Val False -> M (fun th _sol -> (Error Assert_fail, th))
    | _ -> assert false

  let with_thread f = M (fun st _sol -> (Ok (f st), st))

  let thread = M (fun st _sol -> (Ok st, st))

  let solver = M (fun st sol -> (Ok sol, st))

  let add_pc (_vb : vbool) = return ()

  let run ~workers:_ solver t thread = run t thread (Solver.fresh solver ())

  let lift_mem _ = assert false
end

include Make (Thread_with_memory)