clean some code

src/assigned.ml

@@ -121,13 +121,8 @@ let name kind ~get_name values =
 let check_type_id (types : simplified str_type Named.t)
   (check : Grouped.type_check) =
   let id, func_type = check in
-  let* id =
-    match id with
-    | Raw i -> Ok i
-    | Text name -> (
-      match String_map.find_opt name types.named with
-      | None -> error_s "internal error: can't find type with name %s" name
-      | Some t -> Ok t )
+  let id =
+    match id with Raw i -> i | Text name -> String_map.find name types.named
   in
   (* TODO more efficient version of that *)
   match Indexed.get_at id types.values with
@@ -137,10 +132,10 @@ let check_type_id (types : simplified str_type Named.t)
     if not (equal_func_types func_type func_type') then
       Error "inline function type"
     else Ok ()
-  | Some _ -> Error "TODO: Simplify.check_type_id"
+  | Some _ -> assert false
 
 let of_grouped (modul : Grouped.t) : t Result.t =
-  Log.debug "assigning    ...@\n";
+  Log.debug0 "assigning    ...@\n";
   let* typ = assign_types modul in
   let* global =
     name "global"

src/check.ml

@@ -24,7 +24,7 @@ let empty_env () =
   }
 
 let modul m =
-  Log.debug "checking     ...@\n";
+  Log.debug0 "checking     ...@\n";
   let add_global =
     let seen = Hashtbl.create 512 in
     function

src/choice_monad.ml

@@ -23,13 +23,13 @@ let check (sym_bool : vbool) (state : Thread.t) : bool =
   | Val False -> true
   | _ ->
     let check = no :: pc in
-    Format.printf "CHECK:@.%a"
-      (Format.pp_list ~pp_sep:Format.pp_print_newline Expr.pp)
+    Format.pp_std "CHECK:@.%a"
+      (Format.pp_list ~pp_sep:Format.pp_newline Expr.pp)
       check;
     let module Solver = (val solver_module) in
     let r = Solver.check solver check in
     let msg = if r then "KO" else "OK" in
-    Format.printf "@./CHECK %s@." msg;
+    Format.pp_std "@./CHECK %s@." msg;
     not r
 
 (* TODO: make this a CLI flag ? *)
@@ -77,7 +77,7 @@ struct
       | false, false -> M.empty
       | true, false | false, true -> M.return (sat_true, state)
       | true, true ->
-        if print_choice then Format.printf "CHOICE: %a@." Expr.pp v;
+        if print_choice then Format.pp_std "CHOICE: %a@." Expr.pp v;
         let state1 = Thread.clone { state with pc = with_v } in
         let state2 = Thread.clone { state with pc = with_not_v } in
         M.cons (true, state1) (M.return (false, state2)) )
@@ -125,7 +125,7 @@ struct
           match model with
           | None -> assert false (* ? *)
           | Some model -> (
-            Format.printf "Model:@.%a@." Model.pp model;
+            Format.pp_std "Model:@.%a@." Model.pp model;
             let v = Model.evaluate model sym in
             match v with
             | None -> assert false (* ? *)
@@ -390,7 +390,7 @@ module WQ = struct
   let take_as_producer q =
     Mutex.lock q.mutex;
     q.producers <- q.producers - 1;
-    (* Format.printf "TAKE COUNT %i@." q.producers; *)
+    (* Format.pp_std "TAKE COUNT %i@." q.producers; *)
     let r =
       try
         while Queue.is_empty q.queue do
@@ -401,7 +401,7 @@ module WQ = struct
         q.producers <- q.producers + 1;
         Some v
       with Exit ->
-        (* Format.printf "@.@.TAKE EXIT@.@."; *)
+        (* Format.pp_std "@.@.TAKE EXIT@.@."; *)
         Condition.broadcast q.cond;
         None
     in

src/cmd_opt.ml

@@ -14,7 +14,7 @@ let optimize_file ~unsafe filename =
 let cmd debug unsafe (file : string) =
   if debug then Log.debug_on := true;
   match optimize_file ~unsafe file with
-  | Ok modul -> Format.printf "%a@\n" Simplified.Pp.modul modul
+  | Ok modul -> Format.pp_std "%a@\n" Simplified.Pp.modul modul
   | Error e ->
-    Format.eprintf "%s@." e;
+    Format.pp_err "%s@." e;
     exit 1

src/cmd_run.ml

@@ -36,5 +36,5 @@ let cmd profiling debug unsafe optimize files =
   match result with
   | Ok () -> ()
   | Error e ->
-    Format.eprintf "%s@." e;
+    Format.pp_err "%s@\n" e;
     exit 1

src/cmd_script.ml

@@ -19,5 +19,5 @@ let cmd profiling debug optimize files no_exhaustion =
   match result with
   | Ok () -> ()
   | Error e ->
-    Format.eprintf "%s@." e;
+    Format.pp_err "%s@." e;
     exit 1

src/cmd_sym.ml

@@ -11,7 +11,7 @@ let print_path_condition = false
 
 let print_extern_module : Symbolic.P.extern_func Link.extern_module =
   let print_i32 (i : Value.int32) : unit Choice.t =
-    Printf.printf "%s\n%!" (Expr.to_string i);
+    Format.pp_std "%s@\n" (Expr.to_string i);
     Choice.return ()
   in
   (* we need to describe their types *)
@@ -47,7 +47,6 @@ let assert_extern_module : Symbolic.P.extern_func Link.extern_module =
 let names = [| "plop"; "foo"; "bar" |]
 
 let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
-  let sprintf = Printf.sprintf in
   let sym_cnt = Atomic.make 0 in
   let mk_symbol = Encoding.Symbol.mk_symbol in
   let symbolic_i32 (i : Value.int32) : Value.int32 Choice.t =
@@ -60,13 +59,13 @@ let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
     in
     let id = Atomic.fetch_and_add sym_cnt 1 in
     let r =
-      Expr.mk_symbol @@ mk_symbol (Ty_bitv S32) (sprintf "%s_%i" name id)
+      Expr.mk_symbol @@ mk_symbol (Ty_bitv S32) (Format.sprintf "%s_%i" name id)
     in
     Choice.return r
   in
   let symbol ty () : Value.int32 Choice.t =
     let id = Atomic.fetch_and_add sym_cnt 1 in
-    let r = Expr.mk_symbol @@ mk_symbol ty (sprintf "symbol_%i" id) in
+    let r = Expr.mk_symbol @@ mk_symbol ty (Format.sprintf "symbol_%i" id) in
     Choice.return r
   in
   let assume_i32 (i : Value.int32) : unit Choice.t =
@@ -250,21 +249,21 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure workspace
       (fun (result, thread) ->
         let pc = Thread.pc thread in
         if print_path_condition then
-          Format.printf "PATH CONDITION:@\n%a@\n" Expr.pp_list pc;
+          Format.pp_std "PATH CONDITION:@\n%a@\n" Expr.pp_list pc;
         let model = get_model solver pc in
         let result =
           match result with
           | Choice_monad_intf.EVal (Ok ()) -> None
           | EAssert assertion ->
-            Format.printf "Assert failure: %a@\n" Expr.pp assertion;
-            Format.printf "Model:@\n  @[<v>%a@]@\n" Encoding.Model.pp model;
+            Format.pp_std "Assert failure: %a@\n" Expr.pp assertion;
+            Format.pp_std "Model:@\n  @[<v>%a@]@\n" Encoding.Model.pp model;
             Some pc
           | ETrap tr ->
-            Format.printf "Trap: %s@\n" (Trap.to_string tr);
-            Format.printf "Model:@\n  @[<v>%a@]@\n" Encoding.Model.pp model;
+            Format.pp_std "Trap: %s@\n" (Trap.to_string tr);
+            Format.pp_std "Model:@\n  @[<v>%a@]@\n" Encoding.Model.pp model;
             Some pc
           | EVal (Error e) ->
-            Format.eprintf "Error: %s@\n" e;
+            Format.pp_err "Error: %s@\n" e;
             exit 1
         in
         let testcase =
@@ -280,18 +279,18 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure workspace
   let () =
     if no_stop_at_failure then
       let failures = Seq.fold_left (fun n _ -> succ n) 0 failing in
-      if failures = 0 then Format.printf "All OK@\n"
-      else Format.printf "Reached %i problems!@\n" failures
+      if failures = 0 then Format.pp_std "All OK@\n"
+      else Format.pp_err "Reached %i problems!@\n" failures
     else
       match failing () with
-      | Nil -> Format.printf "All OK@\n"
-      | Cons (_thread, _) -> Format.printf "Reached problem!@\n"
+      | Nil -> Format.pp_std "All OK@\n"
+      | Cons (_thread, _) -> Format.pp_err "Reached problem!@\n"
   in
   let time = !Thread.Solver.solver_time in
   let count = !Thread.Solver.solver_count in
   if print_solver_time then begin
-    Format.printf "@\n";
-    Format.printf "Solver time %fs@\n" time;
-    Format.printf "      calls %i@\n" count;
-    Format.printf "  mean time %fms@\n" (1000. *. time /. float count)
+    Format.pp_std "@\n";
+    Format.pp_std "Solver time %fs@\n" time;
+    Format.pp_std "      calls %i@\n" count;
+    Format.pp_std "  mean time %fms@\n" (1000. *. time /. float count)
   end

src/concrete.ml

@@ -94,8 +94,6 @@ module P = struct
     let drop_elem = Link_env.drop_elem
 
     let drop_data = Link_env.drop_data
-
-    let pp = Link_env.pp
   end
 
   module Module_to_run = struct

src/concrete_memory.ml

@@ -62,8 +62,6 @@ let blit_string mem str ~src ~dst ~len =
   ( Bytes.unsafe_blit_string str src mem.data dst len;
     false )
 
-let get_data { data; _ } = data
-
 let get_limit_max { limits; _ } = Option.map Int64.of_int limits.max
 
 let get_limits { limits; _ } = limits

src/concrete_memory.mli

@@ -1,8 +1,6 @@
 (** runtime memory *)
 type t
 
-val get_data : t -> bytes
-
 val get_limit_max : t -> int64 option
 
 val get_limits : t -> Types.limits

src/concrete_value.ml

@@ -3,6 +3,7 @@
 (* Copyright © 2021 Pierre Chambart *)
 
 open Types
+open Format
 
 module Make_extern_func (V : Func_intf.Value_types) (M : Func_intf.Monad_type) =
 struct
@@ -64,7 +65,7 @@ struct
   type t = Func_intf.t
 
   let fresh =
-    let r = ref (-1) in
+    let r = ref ~-1 in
     fun () ->
       incr r;
       !r
@@ -76,24 +77,23 @@ struct
   (*   | Extern (Extern_func (t, _f)) -> extern_type t *)
 end
 
-module Concrete_value_types = struct
-  type int32 = Int32.t
-
-  type int64 = Int64.t
+module Func = struct
+  include
+    Make_extern_func
+      (struct
+        type int32 = Int32.t
 
-  type float32 = Float32.t
+        type int64 = Int64.t
 
-  type float64 = Float64.t
+        type float32 = Float32.t
 
-  type vbool = bool
-end
+        type float64 = Float64.t
 
-module Id_monad = struct
-  type 'a t = 'a
-end
-
-module Func = struct
-  include Make_extern_func (Concrete_value_types) (Id_monad)
+        type vbool = bool
+      end)
+      (struct
+        type 'a t = 'a
+      end)
 end
 
 type externref = E : 'a Type.Id.t * 'a -> externref
@@ -106,13 +106,19 @@ type ref_value =
   | Funcref of Func_intf.t option
   | Arrayref of unit Array.t option
 
+let pp_ref_value fmt = function
+  | Externref _ -> pp fmt "externref"
+  | Funcref _ -> pp fmt "funcref"
+  | Arrayref _ -> pp fmt "array"
+
 type t =
   | I32 of Int32.t
   | I64 of Int64.t
   | F32 of Float32.t
   | F64 of Float64.t
   | Ref of ref_value
 
+(* TODO: make a new kind of instr for this *)
 let of_instr (i : simplified instr) : t =
   match i with
   | I32_const c -> I32 c
@@ -126,24 +132,22 @@ let to_instr = function
   | I64 c -> I64_const c
   | F32 c -> F32_const c
   | F64 c -> F64_const c
-  | _ -> assert false
-
-let pp_ref fmt = function
-  | Externref _ -> Format.fprintf fmt "externref"
-  | Funcref _ -> Format.fprintf fmt "funcref"
-  | Arrayref _ -> Format.fprintf fmt "array"
+  | Ref _ -> assert false
 
 let pp fmt = function
-  | I32 i -> Format.fprintf fmt "i32.const %ld" i
-  | I64 i -> Format.fprintf fmt "i64.const %Ld" i
-  | F32 f -> Format.fprintf fmt "f32.const %a" Float32.pp f
-  | F64 f -> Format.fprintf fmt "f64.const %a" Float64.pp f
-  | Ref r -> pp_ref fmt r
+  | I32 i -> pp fmt "i32.const %ld" i
+  | I64 i -> pp fmt "i64.const %Ld" i
+  | F32 f -> pp fmt "f32.const %a" Float32.pp f
+  | F64 f -> pp fmt "f64.const %a" Float64.pp f
+  | Ref r -> pp_ref_value fmt r
 
 let ref_null' = function
   | Func_ht -> Funcref None
   | Extern_ht -> Externref None
-  | _ -> failwith "TODO ref_null' Value.ml"
+  | Array_ht -> Arrayref None
+  | Any_ht | None_ht | Eq_ht | I31_ht | Struct_ht | No_func_ht | No_extern_ht
+  | Def_ht _ ->
+    assert false
 
 let ref_null typ = Ref (ref_null' typ)
 
@@ -152,4 +156,6 @@ let ref_func (f : Func.t) : t = Ref (Funcref (Some f))
 let ref_externref (type x) (t : x Type.Id.t) (v : x) : t =
   Ref (Externref (Some (E (t, v))))
 
-let ref_is_null = function Funcref None | Externref None -> true | _ -> false
+let ref_is_null = function
+  | Funcref None | Externref None | Arrayref None -> true
+  | Funcref (Some _) | Externref (Some _) | Arrayref (Some _) -> false

src/dune

@@ -36,7 +36,6 @@
   link
   link_env
   log
-  memory_limits
   menhir_parser
   named
   optimize

src/env_id.ml

@@ -4,26 +4,23 @@
 
 type t = int
 
-module IMap = Map.Make (Int)
+module Map = Map.Make (Int)
 
 type 'a collection =
-  { c : 'a IMap.t
+  { c : 'a Map.t
   ; last : int
   }
 
-let empty = { c = IMap.empty; last = 0 }
+let empty = { c = Map.empty; last = 0 }
 
-let with_fresh_id f c =
+let with_fresh_id f { c; last } =
   let open Syntax in
-  let last = c.last in
-  let* e, r = f last in
-  Ok ({ c = IMap.add c.last e c.c; last = c.last + 1 }, r)
+  let+ e, r = f last in
+  let c = Map.add last e c in
+  let last = succ last in
+  ({ c; last }, r)
 
-let get i c = IMap.find i c.c
-
-let pp ppf i = Format.fprintf ppf "f_%i" i
-
-module Map = IMap
+let get i c = Map.find i c.c
 
 module Tbl = Hashtbl.Make (struct
   include Int