diff --git a/coverage/index.html b/coverage/index.html index 3e8ce78a..583692ca 100644 --- a/coverage/index.html +++ b/coverage/index.html @@ -419,9 +419,9 @@

77.17%

- + - 87% (28 / 32) + 88% (30 / 34) src/data_structures/synchronizer.ml @@ -430,7 +430,7 @@

77.17%

- 100% (16 / 16) + 100% (14 / 14) src/data_structures/wq.ml diff --git a/coverage/src/ast/types.ml.html b/coverage/src/ast/types.ml.html index 5008f194..49661e41 100644 --- a/coverage/src/ast/types.ml.html +++ b/coverage/src/ast/types.ml.html @@ -2303,8 +2303,8 @@

48.51%

| F64 -> pf fmt "f64" let num_type_eq t1 t2 = - match (t1, t2) with - | I32, I32 | I64, I64 | F32, F32 | F64, F64 -> true + match (t1, t2) with + | I32, I32 | I64, I64 | F32, F32 | F64, F64 -> true | _, _ -> false let compare_num_type t1 t2 = @@ -2604,8 +2604,8 @@

48.51%

| Ref_type t -> pp_ref_type fmt t let val_type_eq t1 t2 = - match (t1, t2) with - | Num_type t1, Num_type t2 -> num_type_eq t1 t2 + match (t1, t2) with + | Num_type t1, Num_type t2 -> num_type_eq t1 t2 | Ref_type t1, Ref_type t2 -> ref_type_eq t1 t2 | _, _ -> false @@ -2620,7 +2620,7 @@

48.51%

let pp_param fmt (id, vt) = pf fmt "(param%a %a)" pp_id_opt id pp_val_type vt -let param_eq (_, t1) (_, t2) = val_type_eq t1 t2 +let param_eq (_, t1) (_, t2) = val_type_eq t1 t2 let compare_param (_, t1) (_, t2) = compare_val_type t1 t2 @@ -2628,7 +2628,7 @@

48.51%

let pp_param_type fmt params = list ~sep:sp pp_param fmt params -let param_type_eq t1 t2 = List.equal param_eq t1 t2 +let param_type_eq t1 t2 = List.equal param_eq t1 t2 let compare_param_type t1 t2 = List.compare compare_param t1 t2 @@ -2638,7 +2638,7 @@

48.51%

let pp_result_type fmt results = list ~sep:sp pp_result_ fmt results -let result_type_eq t1 t2 = List.equal val_type_eq t1 t2 +let result_type_eq t1 t2 = List.equal val_type_eq t1 t2 let compare_result_type t1 t2 = List.compare compare_val_type t1 t2 @@ -2677,7 +2677,7 @@

48.51%

results let func_type_eq (pt1, rt1) (pt2, rt2) = - param_type_eq pt1 pt2 && result_type_eq rt1 rt2 + param_type_eq pt1 pt2 && result_type_eq rt1 rt2 let compare_func_type (pt1, rt1) (pt2, rt2) = let pt = compare_param_type pt1 pt2 in diff --git a/coverage/src/cmd/cmd_sym.ml.html b/coverage/src/cmd/cmd_sym.ml.html index e817d549..cf9ae3d1 100644 --- a/coverage/src/cmd/cmd_sym.ml.html +++ b/coverage/src/cmd/cmd_sym.ml.html @@ -369,10 +369,10 @@

90.22%

let res_queue = Wq.make () in let path_count = ref 0 in let callback v = - let open Symbolic_choice_intf in + let open Symbolic_choice_intf in incr path_count; - match (fail_mode, v) with - | _, (EVal (Ok ()), _) -> () + match (fail_mode, v) with + | _, (EVal (Ok ()), _) -> () | _, (EVal (Error e), thread) -> Wq.push (`Error e, thread) res_queue | (`Both | `Trap_only), (ETrap (t, m), thread) -> Wq.push (`ETrap (t, m), thread) res_queue diff --git a/coverage/src/data_structures/env_id.ml.html b/coverage/src/data_structures/env_id.ml.html index 42d2404a..22b3877d 100644 --- a/coverage/src/data_structures/env_id.ml.html +++ b/coverage/src/data_structures/env_id.ml.html @@ -112,14 +112,14 @@

77.78%

let last = succ last in ({ c; last }, r) -let get i c = Map.find i c.c +let get i c = Map.find i c.c let map f c = { c with c = Map.map f c.c } module Tbl = Hashtbl.Make (struct include Int - let hash x = x + let hash x = x end)
diff --git a/coverage/src/data_structures/func_id.ml.html b/coverage/src/data_structures/func_id.ml.html index 61c01df0..d9aef144 100644 --- a/coverage/src/data_structures/func_id.ml.html +++ b/coverage/src/data_structures/func_id.ml.html @@ -105,8 +105,8 @@

100.00%

(last, { c; last = succ last }) let get i c = - let v, _ = IMap.find i c.c in - v + let v, _ = IMap.find i c.c in + v let get_typ i c = let _, t = IMap.find i c.c in diff --git a/coverage/src/data_structures/stack.ml.html b/coverage/src/data_structures/stack.ml.html index 084cc4ba..61f3386e 100644 --- a/coverage/src/data_structures/stack.ml.html +++ b/coverage/src/data_structures/stack.ml.html @@ -525,17 +525,17 @@

96.00%

let empty = [] - let push s v = v :: s + let push s v = v :: s - let push_bool s b = push s (I32 (V.Bool.int32 b)) + let push_bool s b = push s (I32 (V.Bool.int32 b)) - let push_const_i32 s i = push s (I32 (V.const_i32 i)) + let push_const_i32 s i = push s (I32 (V.const_i32 i)) - let push_i32 s i = push s (I32 i) + let push_i32 s i = push s (I32 i) let push_i32_of_int s i = push_const_i32 s (Int32.of_int i) - let push_const_i64 s i = push s (I64 (V.const_i64 i)) + let push_const_i64 s i = push s (I64 (V.const_i64 i)) let push_i64 s i = push s (I64 i) @@ -554,22 +554,22 @@

96.00%

let pp fmt (s : t) = Fmt.list ~sep:(fun fmt () -> Fmt.string fmt " ; ") V.pp fmt s - let pop = function [] -> raise Empty | hd :: tl -> (hd, tl) + let pop = function [] -> raise Empty | hd :: tl -> (hd, tl) - let drop = function [] -> raise Empty | _hd :: tl -> tl + let drop = function [] -> raise Empty | _hd :: tl -> tl let pop_i32 s = - let hd, tl = pop s in - match hd with I32 n -> (n, tl) | _ -> assert false + let hd, tl = pop s in + match hd with I32 n -> (n, tl) | _ -> assert false let pop2_i32 s = - let n2, s = pop s in - let n1, tl = pop s in - match (n1, n2) with I32 n1, I32 n2 -> ((n1, n2), tl) | _ -> assert false + let n2, s = pop s in + let n1, tl = pop s in + match (n1, n2) with I32 n1, I32 n2 -> ((n1, n2), tl) | _ -> assert false let pop_i64 s = - let hd, tl = pop s in - match hd with I64 n -> (n, tl) | _ -> assert false + let hd, tl = pop s in + match hd with I64 n -> (n, tl) | _ -> assert false let pop2_i64 s = let n2, s = pop s in @@ -603,17 +603,17 @@

96.00%

match hd with Ref hd -> (hd, tl) | _ -> assert false let pop_bool s = - let hd, tl = pop s in - match hd with I32 n -> (V.I32.to_bool n, tl) | _ -> assert false + let hd, tl = pop s in + match hd with I32 n -> (V.I32.to_bool n, tl) | _ -> assert false let pop_n s n = - (List.filteri (fun i _hd -> i < n) s, List.filteri (fun i _hd -> i >= n) s) + (List.filteri (fun i _hd -> i < n) s, List.filteri (fun i _hd -> i >= n) s) - let keep s n = List.filteri (fun i _hd -> i < n) s + let keep s n = List.filteri (fun i _hd -> i < n) s let rec drop_n s n = - if n = 0 then s - else match s with [] -> assert false | _ :: tl -> drop_n tl (n - 1) + if n = 0 then s + else match s with [] -> assert false | _ :: tl -> drop_n tl (n - 1) end diff --git a/coverage/src/data_structures/synchronizer.ml.html b/coverage/src/data_structures/synchronizer.ml.html index f9fb31ab..950d93f8 100644 --- a/coverage/src/data_structures/synchronizer.ml.html +++ b/coverage/src/data_structures/synchronizer.ml.html @@ -3,7 +3,7 @@ synchronizer.ml — Coverage report - + @@ -15,7 +15,7 @@

src/data_structures/synchronizer.ml

-

87.50%

+

88.24%

diff --git a/coverage/src/data_structures/wq.ml.html b/coverage/src/data_structures/wq.ml.html index a5feebbd..6ebcc6f8 100644 --- a/coverage/src/data_structures/wq.ml.html +++ b/coverage/src/data_structures/wq.ml.html @@ -53,9 +53,8 @@

100.00%

- - - + +
@@ -93,7 +92,6 @@

100.00%

31 32 33 -34 
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
 (* Copyright © 2021-2024 OCamlPro *)
@@ -117,18 +115,17 @@ 
100.00%

 
 let push v q = Synchronizer.write v q
 
-let work_while f q = Synchronizer.work_while f q
+let work_while f q = Synchronizer.work_while f q
 
 let fail = Synchronizer.fail
 
 let make () =
   let q = Queue.create () in
   let writter v condvar =
-    let was_empty = Queue.is_empty q in
-    Queue.push v q;
-    if was_empty then Condition.broadcast condvar
+    Queue.push v q;
+    Condition.signal condvar
   in
-  Synchronizer.init (fun () -> Queue.take_opt q) writter
+  Synchronizer.init (fun () -> Queue.take_opt q) writter
diff --git a/coverage/src/interpret/interpret.ml.html b/coverage/src/interpret/interpret.ml.html index 84a32279..48f33337 100644 --- a/coverage/src/interpret/interpret.ml.html +++ b/coverage/src/interpret/interpret.ml.html @@ -3253,7 +3253,7 @@

91.97%

let ( = ) = eq - let eqz v = v = zero + let eqz v = v = zero let min_int = const_i32 Int32.min_int end @@ -3291,25 +3291,25 @@

91.97%

let page_size = const_i64 65_536L let pop_choice stack = - let b, stack = Stack.pop_bool stack in - let* b = select b in - return (b, stack) + let b, stack = Stack.pop_bool stack in + let* b = select b in + return (b, stack) let ( let> ) v f = - let* v = select v in - f v + let* v = select v in + f v let const = const_i32 - let consti i = const_i32 (Int32.of_int i) + let consti i = const_i32 (Int32.of_int i) let exec_iunop stack nn op = - match nn with - | S32 -> + match nn with + | S32 -> let n, stack = Stack.pop_i32 stack in - let res = + let res = let open I32 in - match op with Clz -> clz n | Ctz -> ctz n | Popcnt -> popcnt n + match op with Clz -> clz n | Ctz -> ctz n | Popcnt -> popcnt n in Stack.push_i32 stack res | S64 -> @@ -3352,15 +3352,15 @@

91.97%

Stack.push_f64 stack res let exec_ibinop (stack : Stack.t) nn (op : ibinop) : Stack.t Choice.t = - match nn with - | S32 -> + match nn with + | S32 -> let (n1, n2), stack = Stack.pop2_i32 stack in - let+ res = + let+ res = let open I32 in match op with - | Add -> Choice.return @@ add n1 n2 + | Add -> Choice.return @@ add n1 n2 | Sub -> Choice.return @@ sub n1 n2 - | Mul -> Choice.return @@ mul n1 n2 + | Mul -> Choice.return @@ mul n1 n2 | Div s -> begin let> cond = eqz n2 in if cond then Choice.trap Integer_divide_by_zero @@ -3372,24 +3372,24 @@

91.97%

else Choice.return @@ div n1 n2 | U -> Choice.return @@ unsigned_div n1 n2 end - | Rem s -> begin - let> cond = eqz n2 in - if cond then Choice.trap Integer_divide_by_zero + | Rem s -> begin + let> cond = eqz n2 in + if cond then Choice.trap Integer_divide_by_zero else - match s with + match s with | S -> Choice.return @@ rem n1 n2 - | U -> Choice.return @@ unsigned_rem n1 n2 + | U -> Choice.return @@ unsigned_rem n1 n2 end - | And -> Choice.return @@ logand n1 n2 + | And -> Choice.return @@ logand n1 n2 | Or -> Choice.return @@ logor n1 n2 | Xor -> Choice.return @@ logxor n1 n2 - | Shl -> Choice.return @@ shl n1 n2 - | Shr S -> Choice.return @@ shr_s n1 n2 - | Shr U -> Choice.return @@ shr_u n1 n2 + | Shl -> Choice.return @@ shl n1 n2 + | Shr S -> Choice.return @@ shr_s n1 n2 + | Shr U -> Choice.return @@ shr_u n1 n2 | Rotl -> Choice.return @@ rotl n1 n2 | Rotr -> Choice.return @@ rotr n1 n2 in - Stack.push_i32 stack res + Stack.push_i32 stack res | S64 -> let (n1, n2), stack = Stack.pop2_i64 stack in let+ res = @@ -3459,10 +3459,10 @@

91.97%

| Copysign -> copy_sign f1 f2 ) let exec_itestop stack nn op = - match nn with - | S32 -> + match nn with + | S32 -> let n, stack = Stack.pop_i32 stack in - let res = match op with Eqz -> I32.eq_const n 0l in + let res = match op with Eqz -> I32.eq_const n 0l in Stack.push_bool stack res | S64 -> let n, stack = Stack.pop_i64 stack in @@ -3470,22 +3470,22 @@

91.97%

Stack.push_bool stack res let exec_irelop stack nn (op : irelop) = - match nn with - | S32 -> + match nn with + | S32 -> let (n1, n2), stack = Stack.pop2_i32 stack in - let res = + let res = let open I32 in match op with - | Eq -> eq n1 n2 - | Ne -> ne n1 n2 - | Lt S -> lt n1 n2 - | Lt U -> lt_u n1 n2 - | Gt S -> gt n1 n2 + | Eq -> eq n1 n2 + | Ne -> ne n1 n2 + | Lt S -> lt n1 n2 + | Lt U -> lt_u n1 n2 + | Gt S -> gt n1 n2 | Gt U -> gt_u n1 n2 - | Le S -> le n1 n2 + | Le S -> le n1 n2 | Le U -> le_u n1 n2 - | Ge S -> ge n1 n2 - | Ge U -> ge_u n1 n2 + | Ge S -> ge n1 n2 + | Ge U -> ge_u n1 n2 in Stack.push_bool stack res | S64 -> @@ -3680,8 +3680,8 @@

91.97%

end let init_local (_id, t) : Value.t = - match t with - | Num_type I32 -> I32 I32.zero + match t with + | Num_type I32 -> I32 I32.zero | Num_type I64 -> I64 I64.zero | Num_type F32 -> F32 F32.zero | Num_type F64 -> F64 F64.zero @@ -3693,10 +3693,10 @@

91.97%

type extern_func = Extern_func.extern_func let exec_extern_func env stack (f : extern_func) = - let pop_arg (type ty) stack (arg : ty Extern_func.telt) : + let pop_arg (type ty) stack (arg : ty Extern_func.telt) : (ty * Stack.t) Choice.t = - match arg with - | I32 -> Choice.return @@ Stack.pop_i32 stack + match arg with + | I32 -> Choice.return @@ Stack.pop_i32 stack | I64 -> Choice.return @@ Stack.pop_i64 stack | F32 -> Choice.return @@ Stack.pop_f32 stack | F64 -> Choice.return @@ Stack.pop_f64 stack @@ -3710,49 +3710,49 @@

91.97%

let rec split_args : type f r. Stack.t -> (f, r) Extern_func.atype -> Stack.t * Stack.t = fun stack ty -> - let[@local] split_one_arg args = - let elt, stack = Stack.pop stack in - let elts, stack = split_args stack args in - (elt :: elts, stack) + let[@local] split_one_arg args = + let elt, stack = Stack.pop stack in + let elts, stack = split_args stack args in + (elt :: elts, stack) in match ty with | Mem args -> split_args stack args - | Arg (_, args) -> split_one_arg args + | Arg (_, args) -> split_one_arg args | UArg args -> split_args stack args | NArg (_, _, args) -> split_one_arg args - | Res -> ([], stack) + | Res -> ([], stack) in let rec apply : type f r. Stack.t -> (f, r) Extern_func.atype -> f -> r Choice.t = fun stack ty f -> - match ty with + match ty with | Mem args -> - let* mem = Env.get_memory env mem_0 in - apply stack args (f mem) - | Arg (arg, args) -> - let* v, stack = pop_arg stack arg in - apply stack args (f v) + let* mem = Env.get_memory env mem_0 in + apply stack args (f mem) + | Arg (arg, args) -> + let* v, stack = pop_arg stack arg in + apply stack args (f v) | UArg args -> apply stack args (f ()) | NArg (_, arg, args) -> let* v, stack = pop_arg stack arg in apply stack args (f v) - | Res -> Choice.return f + | Res -> Choice.return f in let (Extern_func.Extern_func (Func (atype, rtype), func)) = f in let args, stack = split_args stack atype in - let* r = apply (List.rev args) atype func in - let push_val (type ty) (arg : ty Extern_func.telt) (v : ty) stack = + let* r = apply (List.rev args) atype func in + let push_val (type ty) (arg : ty Extern_func.telt) (v : ty) stack = match arg with - | I32 -> Stack.push_i32 stack v + | I32 -> Stack.push_i32 stack v | I64 -> Stack.push_i64 stack v | F32 -> Stack.push_f32 stack v | F64 -> Stack.push_f64 stack v | Externref ty -> Stack.push_as_externref stack ty v in let+ r in - match (rtype, r) with - | R0, () -> stack - | R1 t1, v1 -> push_val t1 v1 stack + match (rtype, r) with + | R0, () -> stack + | R1 t1, v1 -> push_val t1 v1 stack | R2 (t1, t2), (v1, v2) -> push_val t1 v1 stack |> push_val t2 v2 | R3 (t1, t2, t3), (v1, v2, v3) -> push_val t1 v1 stack |> push_val t2 v2 |> push_val t3 v3 @@ -3777,12 +3777,12 @@

91.97%

let of_list = Array.of_list - let get t i = Array.unsafe_get t i + let get t i = Array.unsafe_get t i let set t i v = - let locals = Array.copy t in - Array.unsafe_set locals i v; - locals + let locals = Array.copy t in + Array.unsafe_set locals i v; + locals end type pc = binary instr list @@ -3863,19 +3863,19 @@

91.97%

calls count.calls let empty_count name = - { name; enter = 0; instructions = 0; calls = Hashtbl.create 0 } + { name; enter = 0; instructions = 0; calls = Hashtbl.create 0 } let count_instruction state = - state.count.instructions <- state.count.instructions + 1 + state.count.instructions <- state.count.instructions + 1 let enter_function_count count func_name func = - let c = + let c = match Hashtbl.find_opt count.calls func with - | None -> + | None -> let c = empty_count func_name in - Hashtbl.add count.calls func c; - c - | Some c -> c + Hashtbl.add count.calls func c; + c + | Some c -> c in c.enter <- c.enter + 1; c @@ -3885,50 +3885,50 @@

91.97%

| Continue of exec_state let return (state : exec_state) = - let args = Stack.keep state.stack (List.length state.func_rt) in - match state.return_state with - | None -> Return args - | Some state -> + let args = Stack.keep state.stack (List.length state.func_rt) in + match state.return_state with + | None -> Return args + | Some state -> let stack = args @ state.stack in Continue { state with stack } let branch (state : exec_state) n = - let block_stack = Stack.drop_n state.block_stack n in - match block_stack with + let block_stack = Stack.drop_n state.block_stack n in + match block_stack with | [] -> Choice.return (return state) - | block :: block_stack_tl -> + | block :: block_stack_tl -> let block_stack = - if block.is_loop then block_stack else block_stack_tl + if block.is_loop then block_stack else block_stack_tl in - let args = Stack.keep state.stack (List.length block.branch_rt) in - let stack = args @ block.stack in + let args = Stack.keep state.stack (List.length block.branch_rt) in + let stack = args @ block.stack in Choice.return (Continue { state with block_stack; pc = block.branch; stack }) let end_block (state : exec_state) = - match state.block_stack with - | [] -> Choice.return (return state) - | block :: block_stack -> - let args = Stack.keep state.stack (List.length block.continue_rt) in - let stack = args @ block.stack in + match state.block_stack with + | [] -> Choice.return (return state) + | block :: block_stack -> + let args = Stack.keep state.stack (List.length block.continue_rt) in + let stack = args @ block.stack in Choice.return (Continue { state with block_stack; pc = block.continue; stack }) end let exec_block (state : State.exec_state) ~is_loop (bt : binary block_type option) expr = - let pt, rt = + let pt, rt = match bt with | None -> ([], []) - | Some (Bt_raw ((None | Some _), (pt, rt))) -> (List.map snd pt, rt) + | Some (Bt_raw ((None | Some _), (pt, rt))) -> (List.map snd pt, rt) in let block : State.block = - let branch_rt, branch = if is_loop then (pt, expr) else (rt, state.pc) in + let branch_rt, branch = if is_loop then (pt, expr) else (rt, state.pc) in { branch ; branch_rt ; continue = state.pc ; continue_rt = rt - ; stack = Stack.drop_n state.stack (List.length pt) + ; stack = Stack.drop_n state.stack (List.length pt) ; is_loop } in @@ -3938,17 +3938,17 @@

91.97%

let exec_func ~return ~id (state : State.exec_state) env (func : binary Types.func) = - Log.debug1 "calling func : func %s@." - (Option.value func.id ~default:"anonymous"); - let (Bt_raw ((None | Some _), (param_type, result_type))) = func.type_f in - let args, stack = Stack.pop_n state.stack (List.length param_type) in - let return_state = - if return then state.return_state else Some { state with stack } + Log.debug1 "calling func : func %s@." + (Option.value func.id ~default:"anonymous"); + let (Bt_raw ((None | Some _), (param_type, result_type))) = func.type_f in + let args, stack = Stack.pop_n state.stack (List.length param_type) in + let return_state = + if return then state.return_state else Some { state with stack } in let locals = - State.Locals.of_list @@ List.rev args @ List.map init_local func.locals + State.Locals.of_list @@ List.rev args @ List.map init_local func.locals in - State. + State. { stack = [] ; locals ; pc = func.body @@ -3957,24 +3957,24 @@

91.97%

; return_state ; env ; envs = state.envs - ; count = enter_function_count state.count func.id id + ; count = enter_function_count state.count func.id id } let exec_vfunc ~return (state : State.exec_state) (func : Func_intf.t) = - match func with - | WASM (id, func, env_id) -> + match func with + | WASM (id, func, env_id) -> let env = Env_id.get env_id state.envs in - let id = Raw id in - Choice.return (State.Continue (exec_func ~return ~id state env func)) - | Extern f -> + let id = Raw id in + Choice.return (State.Continue (exec_func ~return ~id state env func)) + | Extern f -> let f = Env.get_extern_func state.env f in - let+ stack = exec_extern_func state.env state.stack f in - let state = { state with stack } in - if return then State.return state else State.Continue state + let+ stack = exec_extern_func state.env state.stack f in + let state = { state with stack } in + if return then State.return state else State.Continue state let func_type (state : State.exec_state) (f : Func_intf.t) = - match f with - | WASM (_, func, _) -> + match f with + | WASM (_, func, _) -> let (Bt_raw ((None | Some _), t)) = func.type_f in t | Extern f -> @@ -4001,57 +4001,57 @@

91.97%

let call_indirect ~return (state : State.exec_state) (tbl_i, (Bt_raw ((None | Some _), typ_i) : binary block_type)) = - let fun_i, stack = Stack.pop_i32 state.stack in - let state = { state with stack } in - let* t = Env.get_table state.env tbl_i in - let _null, ref_kind = Table.typ t in - match ref_kind with - | Func_ht -> + let fun_i, stack = Stack.pop_i32 state.stack in + let state = { state with stack } in + let* t = Env.get_table state.env tbl_i in + let _null, ref_kind = Table.typ t in + match ref_kind with + | Func_ht -> let size = Table.size t in - let> out_of_bounds = I32.(le_u (consti size) fun_i) in - if out_of_bounds then Choice.trap Undefined_element + let> out_of_bounds = I32.(le_u (consti size) fun_i) in + if out_of_bounds then Choice.trap Undefined_element else - let* fun_i = Choice.select_i32 fun_i in - let fun_i = Int32.to_int fun_i in - let f_ref = Table.get t fun_i in - begin + let* fun_i = Choice.select_i32 fun_i in + let fun_i = Int32.to_int fun_i in + let f_ref = Table.get t fun_i in + begin match Ref.get_func f_ref with | Null -> Choice.trap (Uninitialized_element fun_i) | Type_mismatch -> Choice.trap Element_type_error - | Ref_value func -> + | Ref_value func -> let ft = func_type state func in - let ft' = typ_i in - if not (Types.func_type_eq ft ft') then + let ft' = typ_i in + if not (Types.func_type_eq ft ft') then Choice.trap Indirect_call_type_mismatch - else exec_vfunc ~return state func + else exec_vfunc ~return state func end | _ -> Choice.trap Indirect_call_type_mismatch let exec_instr instr (state : State.exec_state) : State.instr_result Choice.t = - State.count_instruction state; - let stack = state.stack in + State.count_instruction state; + let stack = state.stack in let env = state.env in let locals = state.locals in - let st stack = Choice.return (State.Continue { state with stack }) in + let st stack = Choice.return (State.Continue { state with stack }) in Log.debug2 "stack : [ %a ]@." Stack.pp stack; - Log.debug2 "running instr: %a@." Types.pp_instr instr; - match instr with + Log.debug2 "running instr: %a@." Types.pp_instr instr; + match instr with | Return -> Choice.return (State.return state) | Nop -> Choice.return (State.Continue state) | Unreachable -> Choice.trap Unreachable - | I32_const n -> st @@ Stack.push_const_i32 stack n - | I64_const n -> st @@ Stack.push_const_i64 stack n + | I32_const n -> st @@ Stack.push_const_i32 stack n + | I64_const n -> st @@ Stack.push_const_i64 stack n | F32_const f -> st @@ Stack.push_const_f32 stack f | F64_const f -> st @@ Stack.push_const_f64 stack f - | I_unop (nn, op) -> st @@ exec_iunop stack nn op + | I_unop (nn, op) -> st @@ exec_iunop stack nn op | F_unop (nn, op) -> st @@ exec_funop stack nn op - | I_binop (nn, op) -> - let* stack = exec_ibinop stack nn op in - st stack + | I_binop (nn, op) -> + let* stack = exec_ibinop stack nn op in + st stack | F_binop (nn, op) -> st @@ exec_fbinop stack nn op - | I_testop (nn, op) -> st @@ exec_itestop stack nn op - | I_relop (nn, op) -> st @@ exec_irelop stack nn op + | I_testop (nn, op) -> st @@ exec_itestop stack nn op + | I_relop (nn, op) -> st @@ exec_irelop stack nn op | F_relop (nn, op) -> st @@ exec_frelop stack nn op | I_extend8_s nn -> begin match nn with @@ -4110,31 +4110,31 @@

91.97%

| Ref_func (Raw i) -> let f = Env.get_func env i in st @@ Stack.push stack (ref_func f) - | Drop -> st @@ Stack.drop stack - | Local_get (Raw i) -> st @@ Stack.push stack (State.Locals.get locals i) - | Local_set (Raw i) -> + | Drop -> st @@ Stack.drop stack + | Local_get (Raw i) -> st @@ Stack.push stack (State.Locals.get locals i) + | Local_set (Raw i) -> let v, stack = Stack.pop stack in - let locals = State.Locals.set locals i v in - Choice.return (State.Continue { state with locals; stack }) + let locals = State.Locals.set locals i v in + Choice.return (State.Continue { state with locals; stack }) | If_else (_id, bt, e1, e2) -> let* b, stack = pop_choice stack in let state = { state with stack } in exec_block state ~is_loop:false bt (if b then e1 else e2) | Call (Raw i) -> begin let func = Env.get_func env i in - exec_vfunc ~return:false state func + exec_vfunc ~return:false state func end | Return_call (Raw i) -> begin let func = Env.get_func env i in exec_vfunc ~return:true state func end - | Br (Raw i) -> State.branch state i - | Br_if (Raw i) -> - let* b, stack = pop_choice stack in - let state = { state with stack } in - if b then State.branch state i else Choice.return (State.Continue state) - | Loop (_id, bt, e) -> exec_block state ~is_loop:true bt e - | Block (_id, bt, e) -> exec_block state ~is_loop:false bt e + | Br (Raw i) -> State.branch state i + | Br_if (Raw i) -> + let* b, stack = pop_choice stack in + let state = { state with stack } in + if b then State.branch state i else Choice.return (State.Continue state) + | Loop (_id, bt, e) -> exec_block state ~is_loop:true bt e + | Block (_id, bt, e) -> exec_block state ~is_loop:false bt e | Memory_size -> let* mem = Env.get_memory env mem_0 in let len = Memory.size_in_pages mem in @@ -4199,13 +4199,13 @@

91.97%

let> out_of_bounds = Memory.blit_string mem data ~src ~dst ~len in if out_of_bounds then Choice.trap Out_of_bounds_memory_access else st stack - | Select _t -> - if use_ite_for_select then begin + | Select _t -> + if use_ite_for_select then begin let b, stack = Stack.pop_bool stack in - let o2, stack = Stack.pop stack in - let o1, stack = Stack.pop stack in - let* res = P.select b ~if_true:o1 ~if_false:o2 in - st @@ Stack.push stack res + let o2, stack = Stack.pop stack in + let o1, stack = Stack.pop stack in + let* res = P.select b ~if_true:o1 ~if_false:o2 in + st @@ Stack.push stack res end else begin let* b, stack = pop_choice stack in @@ -4213,24 +4213,24 @@

91.97%

let o1, stack = Stack.pop stack in st @@ Stack.push stack (if b then o1 else o2) end - | Local_tee (Raw i) -> + | Local_tee (Raw i) -> let v, stack = Stack.pop stack in - let locals = State.Locals.set locals i v in - let stack = Stack.push stack v in - Choice.return (State.Continue { state with locals; stack }) - | Global_get (Raw i) -> - let* g = Env.get_global env i in - st @@ Stack.push stack (Global.value g) - | Global_set (Raw i) -> - let* global = Env.get_global env i in - let v, stack = + let locals = State.Locals.set locals i v in + let stack = Stack.push stack v in + Choice.return (State.Continue { state with locals; stack }) + | Global_get (Raw i) -> + let* g = Env.get_global env i in + st @@ Stack.push stack (Global.value g) + | Global_set (Raw i) -> + let* global = Env.get_global env i in + let v, stack = match Global.typ global with | Ref_type _rt -> Stack.pop_ref stack - | Num_type nt -> ( + | Num_type nt -> ( match nt with - | I32 -> + | I32 -> let v, stack = Stack.pop_i32 stack in - (I32 v, stack) + (I32 v, stack) | I64 -> let v, stack = Stack.pop_i64 stack in (I64 v, stack) @@ -4242,7 +4242,7 @@

91.97%

(F64 v, stack) ) in Global.set_value global v; - st stack + st stack | Table_get (Raw i) -> let* t = Env.get_table env i in let i, stack = Stack.pop_i32 stack in @@ -4388,71 +4388,71 @@

91.97%

match nn with | S32 -> Stack.push_i32 stack res | S64 -> Stack.push_i64 stack (I64.of_int32 res) ) - | I_load8 (nn, sx, { offset; _ }) -> ( - let* mem = Env.get_memory env mem_0 in - let pos, stack = Stack.pop_i32 stack in - let offset = const offset in - let addr = I32.(pos + offset) in + | I_load8 (nn, sx, { offset; _ }) -> ( + let* mem = Env.get_memory env mem_0 in + let pos, stack = Stack.pop_i32 stack in + let offset = const offset in + let addr = I32.(pos + offset) in let> out_of_bounds = - Bool.or_ I32.(offset < const 0l) - @@ Bool.or_ - I32.(lt_u (Memory.size mem) (addr + const 1l)) - I32.(pos < const 0l) + Bool.or_ I32.(offset < const 0l) + @@ Bool.or_ + I32.(lt_u (Memory.size mem) (addr + const 1l)) + I32.(pos < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access + if out_of_bounds then Choice.trap Out_of_bounds_memory_access else - let* res = - (match sx with S -> Memory.load_8_s | U -> Memory.load_8_u) mem addr + let* res = + (match sx with S -> Memory.load_8_s | U -> Memory.load_8_u) mem addr in - st + st @@ match nn with - | S32 -> Stack.push_i32 stack res + | S32 -> Stack.push_i32 stack res | S64 -> Stack.push_i64 stack (I64.of_int32 res) ) - | I_store8 (nn, { offset; _ }) -> - let* mem = Env.get_memory env mem_0 in - let n, stack = + | I_store8 (nn, { offset; _ }) -> + let* mem = Env.get_memory env mem_0 in + let n, stack = match nn with - | S32 -> + | S32 -> let n, stack = Stack.pop_i32 stack in - (n, stack) + (n, stack) | S64 -> let n, stack = Stack.pop_i64 stack in (I64.to_int32 n, stack) in let pos, stack = Stack.pop_i32 stack in - let offset = const offset in - let addr = I32.(pos + offset) in + let offset = const offset in + let addr = I32.(pos + offset) in let> out_of_bounds = - Bool.or_ I32.(offset < const 0l) - @@ Bool.or_ - I32.(lt_u (Memory.size mem) (addr + const 1l)) - I32.(pos < const 0l) + Bool.or_ I32.(offset < const 0l) + @@ Bool.or_ + I32.(lt_u (Memory.size mem) (addr + const 1l)) + I32.(pos < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_8 mem ~addr n in + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin + let* () = Memory.store_8 mem ~addr n in (* Thread memory ? *) - st stack + st stack end - | I_load (nn, { offset; _ }) -> - let* mem = Env.get_memory env mem_0 in - let pos, stack = Stack.pop_i32 stack in - let memory_length = Memory.size mem in - let offset = const offset in - let addr = I32.(pos + offset) in + | I_load (nn, { offset; _ }) -> + let* mem = Env.get_memory env mem_0 in + let pos, stack = Stack.pop_i32 stack in + let memory_length = Memory.size mem in + let offset = const offset in + let addr = I32.(pos + offset) in let> out_of_bounds = - Bool.or_ I32.(offset < const 0l) I32.(pos < const 0l) + Bool.or_ I32.(offset < const 0l) I32.(pos < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin match nn with - | S32 -> - let> out_of_bounds = I32.(lt_u memory_length (addr + const 4l)) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access + | S32 -> + let> out_of_bounds = I32.(lt_u memory_length (addr + const 4l)) in + if out_of_bounds then Choice.trap Out_of_bounds_memory_access else - let* res = Memory.load_32 mem addr in - st @@ Stack.push_i32 stack res + let* res = Memory.load_32 mem addr in + st @@ Stack.push_i32 stack res | S64 -> let> out_of_bounds = I32.(lt_u memory_length (addr + const 8l)) in if out_of_bounds then Choice.trap Out_of_bounds_memory_access @@ -4487,36 +4487,36 @@

91.97%

let res = F64.of_bits res in st @@ Stack.push_f64 stack res end - | I_store (nn, { offset; _ }) -> ( - let* mem = Env.get_memory env mem_0 in - let memory_length = Memory.size mem in - let offset = const offset in - match nn with - | S32 -> + | I_store (nn, { offset; _ }) -> ( + let* mem = Env.get_memory env mem_0 in + let memory_length = Memory.size mem in + let offset = const offset in + match nn with + | S32 -> let n, stack = Stack.pop_i32 stack in - let pos, stack = Stack.pop_i32 stack in - let addr = I32.(pos + offset) in + let pos, stack = Stack.pop_i32 stack in + let addr = I32.(pos + offset) in let> out_of_bounds = - Bool.or_ I32.(lt_u memory_length (addr + const 4l)) - @@ I32.(pos < const 0l) + Bool.or_ I32.(lt_u memory_length (addr + const 4l)) + @@ I32.(pos < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_32 mem ~addr n in - st stack + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin + let* () = Memory.store_32 mem ~addr n in + st stack end - | S64 -> + | S64 -> let n, stack = Stack.pop_i64 stack in - let pos, stack = Stack.pop_i32 stack in - let addr = I32.(pos + offset) in + let pos, stack = Stack.pop_i32 stack in + let addr = I32.(pos + offset) in let> out_of_bounds = - Bool.or_ I32.(lt_u memory_length (addr + const 8l)) - @@ I32.(pos < const 0l) + Bool.or_ I32.(lt_u memory_length (addr + const 8l)) + @@ I32.(pos < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access - else begin - let* () = Memory.store_64 mem ~addr n in - st stack + if out_of_bounds then Choice.trap Out_of_bounds_memory_access + else begin + let* () = Memory.store_64 mem ~addr n in + st stack end ) | F_store (nn, { offset; _ }) -> ( let* mem = Env.get_memory env mem_0 in @@ -4619,20 +4619,20 @@

91.97%

let* data = Env.get_data env i in Env.drop_data data; st stack - | Br_table (inds, Raw i) -> + | Br_table (inds, Raw i) -> let target, stack = Stack.pop_i32 stack in - let> out = I32.(ge_u target (const (Int32.of_int (Array.length inds)))) in - let* target = - if out then return i + let> out = I32.(ge_u target (const (Int32.of_int (Array.length inds)))) in + let* target = + if out then return i else - let+ target = Choice.select_i32 target in - let target = Int32.to_int target in - let (Raw i) = inds.(target) in - i + let+ target = Choice.select_i32 target in + let target = Int32.to_int target in + let (Raw i) = inds.(target) in + i in - let state = { state with stack } in + let state = { state with stack } in State.branch state target - | Call_indirect (Raw tbl_i, typ_i) -> + | Call_indirect (Raw tbl_i, typ_i) -> call_indirect ~return:false state (tbl_i, typ_i) | Return_call_indirect (Raw tbl_i, typ_i) -> call_indirect ~return:true state (tbl_i, typ_i) @@ -4662,19 +4662,19 @@

91.97%

st stack let rec loop (state : State.exec_state) = - match state.pc with - | instr :: pc -> begin - let* state = exec_instr instr { state with pc } in - match state with - | State.Continue state -> loop state + match state.pc with + | instr :: pc -> begin + let* state = exec_instr instr { state with pc } in + match state with + | State.Continue state -> loop state | State.Return res -> Choice.return res end - | [] -> ( + | [] -> ( Log.debug2 "stack : [ %a ]@." Stack.pp state.stack; - let* state = State.end_block state in - match state with - | State.Continue state -> loop state - | State.Return res -> Choice.return res ) + let* state = State.end_block state in + match state with + | State.Continue state -> loop state + | State.Return res -> Choice.return res ) let exec_expr envs env locals stack expr bt = let count = State.empty_count (Some "start") in @@ -4693,7 +4693,7 @@

91.97%

} in let+ state = loop state in - (state, count) + (state, count) let modul envs (modul : Module_to_run.t) = Log.debug0 "interpreting ...@\n"; @@ -4709,13 +4709,13 @@

91.97%

exec_expr envs env (State.Locals.of_list []) Stack.empty to_run None in - Log.profile3 "Exec module %s@.%a@." - (Option.value (Module_to_run.id modul) ~default:"anonymous") + Log.profile3 "Exec module %s@.%a@." + (Option.value (Module_to_run.id modul) ~default:"anonymous") State.print_count count ) (Choice.return ()) (Module_to_run.to_run modul) in - Ok () + Ok () end with | Trap msg -> Choice.return (Error (`Msg msg)) diff --git a/coverage/src/link/link_env.ml.html b/coverage/src/link/link_env.ml.html index d24a3d53..185f1898 100644 --- a/coverage/src/link/link_env.ml.html +++ b/coverage/src/link/link_env.ml.html @@ -477,21 +477,21 @@

94.74%

let _ : _ IMap.t = IMap.merge (apply recover_elem) backup.elem into.elem in () -let id (env : _ t) = env.id +let id (env : _ t) = env.id -let get_global (env : _ t) id = IMap.find id env.globals +let get_global (env : _ t) id = IMap.find id env.globals -let get_memory (env : _ t) id = IMap.find id env.memories +let get_memory (env : _ t) id = IMap.find id env.memories -let get_table (env : _ t) id = IMap.find id env.tables +let get_table (env : _ t) id = IMap.find id env.tables -let get_func (env : _ t) id = IMap.find id env.functions +let get_func (env : _ t) id = IMap.find id env.functions let get_data (env : _ t) id = IMap.find id env.data let get_elem (env : _ t) id = IMap.find id env.elem -let get_extern_func env id = Func_id.get id env.extern_funcs +let get_extern_func env id = Func_id.get id env.extern_funcs module Build = struct type t = diff --git a/coverage/src/primitives/int32.ml.html b/coverage/src/primitives/int32.ml.html index dde80d03..95baf33e 100644 --- a/coverage/src/primitives/int32.ml.html +++ b/coverage/src/primitives/int32.ml.html @@ -365,7 +365,7 @@

99.25%

let eq (x : int32) y = equal x y -let ne (x : int32) y = compare x y <> 0 +let ne (x : int32) y = compare x y <> 0 let lt (x : int32) y = compare x y < 0 @@ -386,8 +386,8 @@

99.25%

(* If bit (32 - 1) is set, sx will sign-extend t to maintain the * invariant that small ints are stored sign-extended inside a wider int. *) let sx x = - Int64.to_int32 - @@ Int64.shift_right (Int64.shift_left (Int64.of_int32 x) 32) 32 + Int64.to_int32 + @@ Int64.shift_right (Int64.shift_left (Int64.of_int32 x) 32) 32 (* We don't override min_int and max_int since those are used * by other functions (like parsing), and rely on it being @@ -399,11 +399,11 @@

99.25%

let high_int = logxor low_int minus_one (* WebAssembly's shifts mask the shift count according to the 32. *) -let shift f x y = f x (to_int (logand y 31l)) +let shift f x y = f x (to_int (logand y 31l)) -let shl x y = sx (shift shift_left x y) +let shl x y = sx (shift shift_left x y) -let shr_s x y = shift shift_right x y +let shr_s x y = shift shift_right x y let shr_u x y = sx (shift shift_right_logical x y) @@ -416,8 +416,8 @@

99.25%

logor (shr_u x n) (shl x (sub 32l n)) let extend_s n x = - let shift = 32 - n in - shift_right (shift_left x shift) shift + let shift = 32 - n in + shift_right (shift_left x shift) shift (* String conversion that allows leading signs and unsigned values *) diff --git a/coverage/src/primitives/int64.ml.html b/coverage/src/primitives/int64.ml.html index f1cd5dce..3b3f2c56 100644 --- a/coverage/src/primitives/int64.ml.html +++ b/coverage/src/primitives/int64.ml.html @@ -456,11 +456,11 @@

94.74%

let high_int = logxor low_int minus_one (* WebAssembly's shifts mask the shift count according to the bitwidth. *) -let shift f x y = f x (to_int (logand y (of_int 63))) +let shift f x y = f x (to_int (logand y (of_int 63))) let shl x y = shift shift_left x y -let shr_s x y = shift shift_right x y +let shr_s x y = shift shift_right x y let shr_u x y = shift shift_right_logical x y diff --git a/coverage/src/symbolic/solver.ml.html b/coverage/src/symbolic/solver.ml.html index 76abb7a8..32be95b8 100644 --- a/coverage/src/symbolic/solver.ml.html +++ b/coverage/src/symbolic/solver.ml.html @@ -94,24 +94,24 @@

100.00%

type t = S : ('a solver_module * 'a) -> t [@@unboxed] let fresh solver () = - let module Mapping = (val Smtml.Solver_dispatcher.mappings_of_solver solver) + let module Mapping = (val Smtml.Solver_dispatcher.mappings_of_solver solver) in let module Mapping = Mapping.Fresh.Make () in let module Batch = Smtml.Solver.Batch (Mapping) in let solver = Batch.create ~logic:QF_BVFP () in - S ((module Batch), solver) + S ((module Batch), solver) let check (S (solver_module, s)) pc = - let module Solver = (val solver_module) in + let module Solver = (val solver_module) in Solver.check s pc let model (S (solver_module, s)) ~symbols ~pc = - let module Solver = (val solver_module) in + let module Solver = (val solver_module) in match Solver.check s pc with - | `Sat -> begin + | `Sat -> begin match Solver.model ?symbols s with | None -> assert false - | Some model -> model + | Some model -> model end | `Unsat | `Unknown -> assert false diff --git a/coverage/src/symbolic/symbolic.ml.html b/coverage/src/symbolic/symbolic.ml.html index 2038bd5b..340ce0a2 100644 --- a/coverage/src/symbolic/symbolic.ml.html +++ b/coverage/src/symbolic/symbolic.ml.html @@ -357,9 +357,9 @@

83.87%

let select (c : Value.vbool) ~(if_true : Value.t) ~(if_false : Value.t) : Value.t Choice.t = - match (if_true, if_false) with - | I32 if_true, I32 if_false -> - Choice.return (Value.I32 (Value.Bool.select_expr c ~if_true ~if_false)) + match (if_true, if_false) with + | I32 if_true, I32 if_false -> + Choice.return (Value.I32 (Value.Bool.select_expr c ~if_true ~if_false)) | I64 if_true, I64 if_false -> Choice.return (Value.I64 (Value.Bool.select_expr c ~if_true ~if_false)) | F32 if_true, F32 if_false -> @@ -384,25 +384,25 @@

83.87%

module Memory = struct include Memory - let load_8_s m a = Choice.lift_mem @@ load_8_s m a + let load_8_s m a = Choice.lift_mem @@ load_8_s m a - let load_8_u m a = Choice.lift_mem @@ load_8_u m a + let load_8_u m a = Choice.lift_mem @@ load_8_u m a let load_16_s m a = Choice.lift_mem @@ load_16_s m a let load_16_u m a = Choice.lift_mem @@ load_16_u m a - let load_32 m a = Choice.lift_mem @@ load_32 m a + let load_32 m a = Choice.lift_mem @@ load_32 m a let load_64 m a = Choice.lift_mem @@ load_64 m a - let store_8 m ~addr v = Choice.lift_mem @@ store_8 m ~addr v + let store_8 m ~addr v = Choice.lift_mem @@ store_8 m ~addr v let store_16 m ~addr v = Choice.lift_mem @@ store_16 m ~addr v - let store_32 m ~addr v = Choice.lift_mem @@ store_32 m ~addr v + let store_32 m ~addr v = Choice.lift_mem @@ store_32 m ~addr v - let store_64 m ~addr v = Choice.lift_mem @@ store_64 m ~addr v + let store_64 m ~addr v = Choice.lift_mem @@ store_64 m ~addr v end module Data = struct @@ -417,10 +417,10 @@

83.87%

type t' = Env_id.t let get_memory env id = - let orig_mem = Link_env.get_memory env id in - let f (t : thread) = - let memories = Thread.memories t in - Memory.get_memory (Link_env.id env) orig_mem memories id + let orig_mem = Link_env.get_memory env id in + let f (t : thread) = + let memories = Thread.memories t in + Memory.get_memory (Link_env.id env) orig_mem memories id in Choice.with_thread f @@ -430,7 +430,7 @@

83.87%

let get_table (env : t) i : Table.t Choice.t = let orig_table = Link_env.get_table env i in - let f (t : thread) = + let f (t : thread) = let tables = Thread.tables t in Symbolic_table.get_table (Link_env.id env) orig_table tables i in @@ -443,10 +443,10 @@

83.87%

Choice.return data let get_global (env : t) i : Global.t Choice.t = - let orig_global = Link_env.get_global env i in - let f (t : thread) = - let globals = Thread.globals t in - Symbolic_global.get_global (Link_env.id env) orig_global globals i + let orig_global = Link_env.get_global env i in + let f (t : thread) = + let globals = Thread.globals t in + Symbolic_global.get_global (Link_env.id env) orig_global globals i in Choice.with_thread f @@ -467,7 +467,7 @@

83.87%

let env (t : t) = t.env - let id (t : t) = t.id + let id (t : t) = t.id let to_run (t : t) = t.to_run end diff --git a/coverage/src/symbolic/symbolic_choice.ml.html b/coverage/src/symbolic/symbolic_choice.ml.html index d43cc78b..3e75c792 100644 --- a/coverage/src/symbolic/symbolic_choice.ml.html +++ b/coverage/src/symbolic/symbolic_choice.ml.html @@ -1023,42 +1023,42 @@

95.69%

| Stop let run (Sched mxf : ('a, 'wls) t) (wls : 'wls) : ('a, 'wls) status = - mxf wls + mxf wls - let return x : _ t = Sched (Fun.const (Now x)) + let return x : _ t = Sched (Fun.const (Now x)) let return_status status = Sched (Fun.const status) let rec bind (mx : ('a, 'wls) t) (f : 'a -> ('b, 'wls) t) : ('b, 'wls) t = - Sched + Sched (fun wls -> - let rec unfold_status (x : ('a, 'wls) status) : ('b, 'wls) status = - match x with - | Now x -> run (f x) wls - | Yield (prio, lx) -> Yield (prio, bind lx f) - | Choice (mx1, mx2) -> + let rec unfold_status (x : ('a, 'wls) status) : ('b, 'wls) status = + match x with + | Now x -> run (f x) wls + | Yield (prio, lx) -> Yield (prio, bind lx f) + | Choice (mx1, mx2) -> let mx1' = unfold_status mx1 in - let mx2' = unfold_status mx2 in - Choice (mx1', mx2') - | Stop -> Stop + let mx2' = unfold_status mx2 in + Choice (mx1', mx2') + | Stop -> Stop in - unfold_status (run mx wls) ) + unfold_status (run mx wls) ) let ( let* ) = bind let map x f = - let* x in - return (f x) + let* x in + return (f x) let ( let+ ) = map let yield prio = return_status (Yield (prio, Sched (Fun.const (Now ())))) - let choose a b = Sched (fun wls -> Choice (run a wls, run b wls)) + let choose a b = Sched (fun wls -> Choice (run a wls, run b wls)) let stop : ('a, 'b) t = return_status Stop - let worker_local : ('a, 'a) t = Sched (fun wls -> Now wls) + let worker_local : ('a, 'a) t = Sched (fun wls -> Now wls) end module Scheduler = struct @@ -1076,27 +1076,27 @@

95.69%

let add_init_task sched task = Wq.push task sched.work_queue let work wls sched callback = - let rec handle_status (t : _ Schedulable.status) write_back = - match t with - | Stop -> () - | Now x -> callback x - | Yield (_prio, f) -> write_back f - | Choice (m1, m2) -> + let rec handle_status (t : _ Schedulable.status) write_back = + match t with + | Stop -> () + | Now x -> callback x + | Yield (_prio, f) -> write_back f + | Choice (m1, m2) -> handle_status m1 write_back; - handle_status m2 write_back + handle_status m2 write_back in Wq.work_while - (fun f write_back -> handle_status (Schedulable.run f wls) write_back) + (fun f write_back -> handle_status (Schedulable.run f wls) write_back) sched.work_queue let spawn_worker sched wls_init callback callback_init callback_close = callback_init (); Domain.spawn (fun () -> - Fun.protect - ~finally:(fun () -> callback_close ()) + Fun.protect + ~finally:(fun () -> callback_close ()) (fun () -> - let wls = wls_init () in - try work wls sched callback + let wls = wls_init () in + try work wls sched callback with e -> let bt = Printexc.get_raw_backtrace () in Wq.fail sched.work_queue; @@ -1112,46 +1112,46 @@

95.69%

type ('a, 's) t = St of ('s -> ('a * 's, Solver.t) M.t) [@@unboxed] - let run (St mxf) st = mxf st + let run (St mxf) st = mxf st - let return x = St (fun st -> M.return (x, st)) + let return x = St (fun st -> M.return (x, st)) let lift (x : ('a, _) M.t) : ('a, 's) t = let ( let+ ) = M.( let+ ) in St (fun (st : 's) -> - let+ x in - (x, st) ) + let+ x in + (x, st) ) let bind mx f = - St + St (fun st -> - let ( let* ) = M.( let* ) in - let* x, new_st = run mx st in - run (f x) new_st ) + let ( let* ) = M.( let* ) in + let* x, new_st = run mx st in + run (f x) new_st ) let ( let* ) = bind let map x f = - let* x in - return (f x) + let* x in + return (f x) - let liftF2 f x y = St (fun st -> f (run x st) (run y st)) + let liftF2 f x y = St (fun st -> f (run x st) (run y st)) let ( let+ ) = map - let with_state f = St (fun st -> M.return (f st)) + let with_state f = St (fun st -> M.return (f st)) - let modify_state f = St (fun st -> M.return ((), f st)) + let modify_state f = St (fun st -> M.return ((), f st)) let project_state (project_and_backup : 'st1 -> 'st2 * 'backup) restore other = - St + St (fun st -> - let ( let+ ) = M.( let+ ) in + let ( let+ ) = M.( let+ ) in let proj, backup = project_and_backup st in - let+ res, new_state = run other proj in - (res, restore backup new_state) ) + let+ res, new_state = run other proj in + (res, restore backup new_state) ) end module Eval = struct @@ -1163,28 +1163,28 @@

95.69%

type ('a, 's) t = ('a eval, 's) M.t - let return x : _ t = M.return (EVal x) + let return x : _ t = M.return (EVal x) let lift x = - let ( let+ ) = M.( let+ ) in + let ( let+ ) = M.( let+ ) in let+ x in - EVal x + EVal x let bind (mx : _ t) f : _ t = - let ( let* ) = M.( let* ) in + let ( let* ) = M.( let* ) in let* mx in - match mx with - | EVal x -> f x + match mx with + | EVal x -> f x | ETrap _ as mx -> M.return mx | EAssert _ as mx -> M.return mx let ( let* ) = bind let map mx f = - let ( let+ ) = M.( let+ ) in + let ( let+ ) = M.( let+ ) in let+ mx in - match mx with - | EVal x -> EVal (f x) + match mx with + | EVal x -> EVal (f x) | ETrap _ as mx -> mx | EAssert _ as mx -> mx @@ -1262,27 +1262,27 @@

95.69%

lift v let with_thread (f : Thread.t -> 'a) : 'a t = - let x = State.with_state (fun st -> (f st, st)) in - lift x + let x = State.with_state (fun st -> (f st, st)) in + lift x let thread = with_thread Fun.id - let modify_thread f = lift (State.modify_state f) + let modify_thread f = lift (State.modify_state f) - let set_thread st = modify_thread (Fun.const st) + let set_thread st = modify_thread (Fun.const st) let clone_thread = modify_thread Thread.clone let solver = lift_schedulable Schedulable.worker_local let choose a b = - let a = + let a = let* () = clone_thread in - a + a in let b = let* () = clone_thread in - b + b in State.liftF2 Schedulable.choose a b @@ -1320,17 +1320,17 @@

95.69%

include CoreImpl.Make (Thread) let add_pc (c : Symbolic_value.vbool) = - match Smtml.Expr.view c with + match Smtml.Expr.view c with | Val True -> return () - | Val False -> stop - | _ -> + | Val False -> stop + | _ -> let* thread in - let new_thread = Thread.add_pc thread c in - set_thread new_thread + let new_thread = Thread.add_pc thread c in + set_thread new_thread [@@inline] let add_breadcrumb crumb = - modify_thread (fun t -> Thread.add_breadcrumb t crumb) + modify_thread (fun t -> Thread.add_breadcrumb t crumb) let with_new_symbol ty f = let* thread in @@ -1349,113 +1349,113 @@

95.69%

*) let check_reachability = let* () = yield in - let* thread in - let* solver in - let pc = Thread.pc thread in - match Solver.check solver pc with - | `Sat -> return () - | `Unsat | `Unknown -> stop + let* thread in + let* solver in + let pc = Thread.pc thread in + match Solver.check solver pc with + | `Sat -> return () + | `Unsat | `Unknown -> stop let get_model_or_stop symbol = - let* () = yield in - let* solver in - let+ thread in - let pc = Thread.pc thread in - match Solver.check solver pc with - | `Unsat | `Unknown -> stop - | `Sat -> begin + let* () = yield in + let* solver in + let+ thread in + let pc = Thread.pc thread in + match Solver.check solver pc with + | `Unsat | `Unknown -> stop + | `Sat -> begin let symbols = [ symbol ] |> Option.some in - let model = Solver.model solver ~symbols ~pc in - match Smtml.Model.evaluate model symbol with + let model = Solver.model solver ~symbols ~pc in + match Smtml.Model.evaluate model symbol with | None -> Fmt.failwith "Unreachable: The model exists so this symbol should evaluate" - | Some v -> return v + | Some v -> return v end let select_inner ~explore_first (cond : Symbolic_value.vbool) = - let v = Smtml.Expr.simplify cond in - match Smtml.Expr.view v with - | Val True -> return true - | Val False -> return false + let v = Smtml.Expr.simplify cond in + match Smtml.Expr.view v with + | Val True -> return true + | Val False -> return false | Val (Num (I32 _)) -> Fmt.failwith "unreachable (type error)" - | _ -> + | _ -> let true_branch = - let* () = add_pc v in - let* () = add_breadcrumb 1l in - let+ () = check_reachability in - true + let* () = add_pc v in + let* () = add_breadcrumb 1l in + let+ () = check_reachability in + true in let false_branch = - let* () = add_pc (Symbolic_value.Bool.not v) in - let* () = add_breadcrumb 0l in - let+ () = check_reachability in - false + let* () = add_pc (Symbolic_value.Bool.not v) in + let* () = add_breadcrumb 0l in + let+ () = check_reachability in + false in - if explore_first then choose true_branch false_branch - else choose false_branch true_branch + if explore_first then choose true_branch false_branch + else choose false_branch true_branch [@@inline] let select (cond : Symbolic_value.vbool) = - select_inner cond ~explore_first:true + select_inner cond ~explore_first:true [@@inline] let summary_symbol (e : Smtml.Expr.t) = - let* thread in - match Smtml.Expr.view e with + let* thread in + match Smtml.Expr.view e with | Symbol sym -> return (None, sym) - | _ -> + | _ -> let num_symbols = Thread.symbols thread in - let+ () = modify_thread Thread.incr_symbols in - let sym_name = Fmt.str "choice_i32_%i" num_symbols in - let sym_type = Smtml.Ty.Ty_bitv 32 in + let+ () = modify_thread Thread.incr_symbols in + let sym_name = Fmt.str "choice_i32_%i" num_symbols in + let sym_type = Smtml.Ty.Ty_bitv 32 in let sym = Smtml.Symbol.make sym_type sym_name in - let assign = Smtml.Expr.(relop Ty_bool Eq (symbol sym) e) in + let assign = Smtml.Expr.(relop Ty_bool Eq (symbol sym) e) in (Some assign, sym) let select_i32 (i : Symbolic_value.int32) = - let sym_int = Smtml.Expr.simplify i in - match Smtml.Expr.view sym_int with - | Val (Num (I32 i)) -> return i - | _ -> - let* assign, symbol = summary_symbol sym_int in - let* () = - match assign with Some assign -> add_pc assign | None -> return () + let sym_int = Smtml.Expr.simplify i in + match Smtml.Expr.view sym_int with + | Val (Num (I32 i)) -> return i + | _ -> + let* assign, symbol = summary_symbol sym_int in + let* () = + match assign with Some assign -> add_pc assign | None -> return () in - let rec generator () = - let* possible_value = get_model_or_stop symbol in - let* possible_value in - let i = + let rec generator () = + let* possible_value = get_model_or_stop symbol in + let* possible_value in + let i = match possible_value with - | Smtml.Value.Num (I32 i) -> i + | Smtml.Value.Num (I32 i) -> i | _ -> Fmt.failwith "Unreachable: found symbol must be a value" in let s = Smtml.Expr.symbol symbol in - let this_value_cond = + let this_value_cond = let open Smtml.Expr in - Bitv.I32.(s = v i) + Bitv.I32.(s = v i) in let not_this_value_cond = let open Smtml.Expr in (* != is **not** the physical inequality here *) - Bitv.I32.(s != v i) + Bitv.I32.(s != v i) in let this_val_branch = - let* () = add_breadcrumb i in - let+ () = add_pc this_value_cond in - i + let* () = add_breadcrumb i in + let+ () = add_pc this_value_cond in + i in let not_this_val_branch = - let* () = add_pc not_this_value_cond in - generator () + let* () = add_pc not_this_value_cond in + generator () in choose this_val_branch not_this_val_branch in generator () let assertion c = - let* assertion_true = select_inner c ~explore_first:false in - if assertion_true then return () + let* assertion_true = select_inner c ~explore_first:false in + if assertion_true then return () else let* thread in let* solver in diff --git a/coverage/src/symbolic/symbolic_choice_with_memory.ml.html b/coverage/src/symbolic/symbolic_choice_with_memory.ml.html index d5e0509d..3f59e326 100644 --- a/coverage/src/symbolic/symbolic_choice_with_memory.ml.html +++ b/coverage/src/symbolic/symbolic_choice_with_memory.ml.html @@ -52,7 +52,7 @@

100.00%

include Symbolic_choice.Make (Thread_with_memory) let lift_mem (mem_op : 'a Symbolic_choice_without_memory.t) : 'a t = - Symbolic_choice.CoreImpl.State.project_state Thread_with_memory.project + Symbolic_choice.CoreImpl.State.project_state Thread_with_memory.project Thread_with_memory.restore mem_op diff --git a/coverage/src/symbolic/symbolic_global.ml.html b/coverage/src/symbolic/symbolic_global.ml.html index 26be1830..42283e61 100644 --- a/coverage/src/symbolic/symbolic_global.ml.html +++ b/coverage/src/symbolic/symbolic_global.ml.html @@ -172,7 +172,7 @@

94.87%

module ITbl = Hashtbl.Make (struct include Int - let hash x = x + let hash x = x end) type t = @@ -184,16 +184,16 @@

94.87%

let init () = Env_id.Tbl.create 0 -let global_copy r = { r with value = r.value } +let global_copy r = { r with value = r.value } let clone collection = (* TODO: this is ugly and should be rewritten... *) - let s = Env_id.Tbl.to_seq collection in - Env_id.Tbl.of_seq - @@ Seq.map + let s = Env_id.Tbl.to_seq collection in + Env_id.Tbl.of_seq + @@ Seq.map (fun (i, t) -> - let s = ITbl.to_seq t in - (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, global_copy a)) s) ) + let s = ITbl.to_seq t in + (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, global_copy a)) s) ) s let convert_values (v : Concrete_value.t) : Symbolic_value.t = @@ -210,29 +210,29 @@

94.87%

{ value = convert_values orig_global.value; orig = orig_global } let get_env env_id tables = - match Env_id.Tbl.find_opt tables env_id with - | Some env -> env + match Env_id.Tbl.find_opt tables env_id with + | Some env -> env | None -> let t = ITbl.create 0 in Env_id.Tbl.add tables env_id t; t let get_global env_id (orig_global : Concrete_global.t) collection g_id = - let env = get_env env_id collection in - match ITbl.find_opt env g_id with - | Some t -> t + let env = get_env env_id collection in + match ITbl.find_opt env g_id with + | Some t -> t | None -> let t = convert orig_global in ITbl.add env g_id t; t -let value v = v.value +let value v = v.value -let set_value v x = v.value <- x +let set_value v x = v.value <- x let mut v = v.orig.mut -let typ v = v.orig.typ +let typ v = v.orig.typ diff --git a/coverage/src/symbolic/symbolic_memory_concretizing.ml.html b/coverage/src/symbolic/symbolic_memory_concretizing.ml.html index 5d8d0ed7..e051d7c3 100644 --- a/coverage/src/symbolic/symbolic_memory_concretizing.ml.html +++ b/coverage/src/symbolic/symbolic_memory_concretizing.ml.html @@ -360,48 +360,48 @@

92.13%

let clone m = (* TODO: Make chunk copying lazy *) - { data = Hashtbl.create 16 + { data = Hashtbl.create 16 ; parent = Some m - ; chunks = Hashtbl.copy m.chunks + ; chunks = Hashtbl.copy m.chunks } let address a = - let open Symbolic_choice_without_memory in + let open Symbolic_choice_without_memory in match Smtml.Expr.view a with - | Val (Num (I32 i)) -> return i - | Ptr { base; offset } -> - select_i32 Symbolic_value.(I32.add (const_i32 base) offset) + | Val (Num (I32 i)) -> return i + | Ptr { base; offset } -> + select_i32 Symbolic_value.(I32.add (const_i32 base) offset) | _ -> select_i32 a let address_i32 a = a let rec load_byte { parent; data; _ } a = - try Hashtbl.find data a - with Not_found -> ( + try Hashtbl.find data a + with Not_found -> ( match parent with - | None -> Smtml.Expr.value (Num (I8 0)) - | Some parent -> load_byte parent a ) + | None -> Smtml.Expr.value (Num (I8 0)) + | Some parent -> load_byte parent a ) (* TODO: don't rebuild so many values it generates unecessary hc lookups *) let merge_extracts (e1, h, m1) (e2, m2, l) = - let ty = Smtml.Expr.ty e1 in - if m1 = m2 && Smtml.Expr.equal e1 e2 then - if h - l = Smtml.Ty.size ty then e1 - else Smtml.Expr.make (Extract (e1, h, l)) + let ty = Smtml.Expr.ty e1 in + if m1 = m2 && Smtml.Expr.equal e1 e2 then + if h - l = Smtml.Ty.size ty then e1 + else Smtml.Expr.make (Extract (e1, h, l)) else - Smtml.Expr.( - make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))) ) + Smtml.Expr.( + make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))) ) let concat ~msb ~lsb offset = - assert (offset > 0 && offset <= 8); - match (Smtml.Expr.view msb, Smtml.Expr.view lsb) with - | Val (Num (I8 i1)), Val (Num (I8 i2)) -> - Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2)) - | Val (Num (I8 i1)), Val (Num (I32 i2)) -> + assert (offset > 0 && offset <= 8); + match (Smtml.Expr.view msb, Smtml.Expr.view lsb) with + | Val (Num (I8 i1)), Val (Num (I8 i2)) -> + Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2)) + | Val (Num (I8 i1)), Val (Num (I32 i2)) -> let offset = offset * 8 in if offset < 32 then - Symbolic_value.const_i32 - Int32.(logor (shl (of_int i1) (of_int offset)) i2) + Symbolic_value.const_i32 + Int32.(logor (shl (of_int i1) (of_int offset)) i2) else let i1' = Int64.of_int i1 in let i2' = Int64.of_int32 i2 in @@ -409,31 +409,31 @@

92.13%

| Val (Num (I8 i1)), Val (Num (I64 i2)) -> let offset = Int64.of_int (offset * 8) in Symbolic_value.const_i64 Int64.(logor (shl (of_int i1) offset) i2) - | Extract (e1, h, m1), Extract (e2, m2, l) -> + | Extract (e1, h, m1), Extract (e2, m2, l) -> merge_extracts (e1, h, m1) (e2, m2, l) - | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) -> - Smtml.Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))) - | _ -> Smtml.Expr.make (Concat (msb, lsb)) + | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) -> + Smtml.Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))) + | _ -> Smtml.Expr.make (Concat (msb, lsb)) let loadn m a n = - let rec loop addr size i acc = - if i = size then acc + let rec loop addr size i acc = + if i = size then acc else - let addr' = Int32.(add addr (of_int i)) in + let addr' = Int32.(add addr (of_int i)) in let byte = load_byte m addr' in - loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc) + loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc) in let v0 = load_byte m a in - loop a n 1 v0 + loop a n 1 v0 let extract v pos = - match Smtml.Expr.view v with + match Smtml.Expr.view v with | Val (Num (I8 _)) -> v - | Val (Num (I32 i)) -> - let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in + | Val (Num (I32 i)) -> + let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in Smtml.Expr.value (Num (I8 i')) - | Val (Num (I64 i)) -> - let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in + | Val (Num (I64 i)) -> + let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in Smtml.Expr.value (Num (I8 i')) | Cvtop (_, Zero_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym)) @@ -441,64 +441,64 @@

92.13%

(_, Sign_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym)) -> sym - | _ -> Smtml.Expr.make (Extract (v, pos + 1, pos)) + | _ -> Smtml.Expr.make (Extract (v, pos + 1, pos)) let storen m a v n = - for i = 0 to n - 1 do - let a' = Int32.add a (Int32.of_int i) in - let v' = extract v i in - Hashtbl.replace m.data a' v' + for i = 0 to n - 1 do + let a' = Int32.add a (Int32.of_int i) in + let v' = extract v i in + Hashtbl.replace m.data a' v' done let validate_address m a range = - let open Symbolic_choice_without_memory in + let open Symbolic_choice_without_memory in match Smtml.Expr.view a with - | Val (Num (I32 _)) -> + | Val (Num (I32 _)) -> (* An i32 is not a pointer to a heap chunk, so its valid *) return (Ok a) - | Ptr { base; offset = start_offset } -> ( + | Ptr { base; offset = start_offset } -> ( let open Symbolic_value in match Hashtbl.find m.chunks base with | exception Not_found -> return (Error Trap.Memory_leak_use_after_free) - | chunk_size -> + | chunk_size -> let+ is_out_of_bounds = - let range = const_i32 (Int32.of_int (range - 1)) in + let range = const_i32 (Int32.of_int (range - 1)) in (* end_offset: last byte we will read/write *) - let end_offset = I32.add start_offset range in - select - (Bool.or_ - (I32.ge_u start_offset chunk_size) - (I32.ge_u end_offset chunk_size) ) + let end_offset = I32.add start_offset range in + select + (Bool.or_ + (I32.ge_u start_offset chunk_size) + (I32.ge_u end_offset chunk_size) ) in - if is_out_of_bounds then Error Trap.Memory_heap_buffer_overflow - else Ok a ) + if is_out_of_bounds then Error Trap.Memory_heap_buffer_overflow + else Ok a ) | _ -> (* A symbolic expression is valid, but we print to check if Ptr's are passing through here *) Log.debug2 "Saw a symbolic address: %a@." Smtml.Expr.pp a; return (Ok a) let ptr v = - let open Symbolic_choice_without_memory in + let open Symbolic_choice_without_memory in match Smtml.Expr.view v with - | Ptr { base; _ } -> return base + | Ptr { base; _ } -> return base | _ -> Log.debug2 {|free: cannot fetch pointer base of "%a"|} Smtml.Expr.pp v; let* () = add_pc @@ Smtml.Expr.value False in assert false let free m p = - let open Symbolic_choice_without_memory in - let+ base = ptr p in - if not @@ Hashtbl.mem m.chunks base then + let open Symbolic_choice_without_memory in + let+ base = ptr p in + if not @@ Hashtbl.mem m.chunks base then Fmt.failwith "Memory leak double free"; - Hashtbl.remove m.chunks base; - Symbolic_value.const_i32 base + Hashtbl.remove m.chunks base; + Symbolic_value.const_i32 base let realloc m ~ptr ~size = - let open Symbolic_choice_without_memory in - let+ base = address ptr in - Hashtbl.replace m.chunks base size; - Smtml.Expr.ptr base (Symbolic_value.const_i32 0l) + let open Symbolic_choice_without_memory in + let+ base = address ptr in + Hashtbl.replace m.chunks base size; + Smtml.Expr.ptr base (Symbolic_value.const_i32 0l) end include Symbolic_memory_make.Make (Backend) diff --git a/coverage/src/symbolic/symbolic_memory_make.ml.html b/coverage/src/symbolic/symbolic_memory_make.ml.html index 5f6ca5da..9afb9ee8 100644 --- a/coverage/src/symbolic/symbolic_memory_make.ml.html +++ b/coverage/src/symbolic/symbolic_memory_make.ml.html @@ -439,7 +439,7 @@

87.60%

(Symbolic_value.I32.gt new_size m.size) ~if_true:new_size ~if_false:m.size - let size { size; _ } = Symbolic_value.I32.mul size page_size + let size { size; _ } = Symbolic_value.I32.mul size page_size let size_in_pages { size; _ } = size @@ -468,29 +468,29 @@

87.60%

Symbolic_value.Bool.const false end - let clone m = { data = Backend.clone m.data; size = m.size } + let clone m = { data = Backend.clone m.data; size = m.size } let must_be_valid_address m a n = - let open Symbolic_choice_without_memory in - let* addr = Backend.validate_address m a n in - match addr with Error t -> trap t | Ok ptr -> Backend.address ptr + let open Symbolic_choice_without_memory in + let* addr = Backend.validate_address m a n in + match addr with Error t -> trap t | Ok ptr -> Backend.address ptr let load_8_s m a = - let open Symbolic_choice_without_memory in - let+ a = must_be_valid_address m.data a 1 in - let v = Backend.loadn m.data a 1 in - match Smtml.Expr.view v with - | Val (Num (I8 i8)) -> - Symbolic_value.const_i32 (Int32.extend_s 8 (Int32.of_int i8)) - | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Sign_extend 24) v + let open Symbolic_choice_without_memory in + let+ a = must_be_valid_address m.data a 1 in + let v = Backend.loadn m.data a 1 in + match Smtml.Expr.view v with + | Val (Num (I8 i8)) -> + Symbolic_value.const_i32 (Int32.extend_s 8 (Int32.of_int i8)) + | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Sign_extend 24) v let load_8_u m a = - let open Symbolic_choice_without_memory in - let+ a = must_be_valid_address m.data a 1 in - let v = Backend.loadn m.data a 1 in - match Smtml.Expr.view v with - | Val (Num (I8 i)) -> Symbolic_value.const_i32 (Int32.of_int i) - | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Zero_extend 24) v + let open Symbolic_choice_without_memory in + let+ a = must_be_valid_address m.data a 1 in + let v = Backend.loadn m.data a 1 in + match Smtml.Expr.view v with + | Val (Num (I8 i)) -> Symbolic_value.const_i32 (Int32.of_int i) + | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Zero_extend 24) v let load_16_s m a = let open Symbolic_choice_without_memory in @@ -510,17 +510,17 @@

87.60%

(* TODO: Smtml should do this. Make call to Expr.simplify *) let try_to_remove_extract v = - match Smtml.Expr.view v with + match Smtml.Expr.view v with | Extract ({ node = Concat (({ node = Ptr _; _ } as ptr), _); _ }, 8, 4) -> ptr | Extract ({ node = Concat (_, ({ node = Ptr _; _ } as ptr)); _ }, 4, 0) -> ptr - | _ -> v + | _ -> v let load_32 m a = - let open Symbolic_choice_without_memory in - let+ a = must_be_valid_address m.data a 4 in - try_to_remove_extract @@ Backend.loadn m.data a 4 + let open Symbolic_choice_without_memory in + let+ a = must_be_valid_address m.data a 4 in + try_to_remove_extract @@ Backend.loadn m.data a 4 let load_64 m a = let open Symbolic_choice_without_memory in @@ -528,9 +528,9 @@

87.60%

Backend.loadn m.data a 8 let store_8 m ~addr v = - let open Symbolic_choice_without_memory in - let+ a = must_be_valid_address m.data addr 1 in - Backend.storen m.data a v 1 + let open Symbolic_choice_without_memory in + let+ a = must_be_valid_address m.data addr 1 in + Backend.storen m.data a v 1 let store_16 m ~addr v = let open Symbolic_choice_without_memory in @@ -538,26 +538,26 @@

87.60%

Backend.storen m.data a v 2 let store_32 m ~addr v = - let open Symbolic_choice_without_memory in - let+ a = must_be_valid_address m.data addr 4 in - Backend.storen m.data a v 4 + let open Symbolic_choice_without_memory in + let+ a = must_be_valid_address m.data addr 4 in + Backend.storen m.data a v 4 let store_64 m ~addr v = - let open Symbolic_choice_without_memory in - let+ a = must_be_valid_address m.data addr 8 in - Backend.storen m.data a v 8 + let open Symbolic_choice_without_memory in + let+ a = must_be_valid_address m.data addr 8 in + Backend.storen m.data a v 8 let get_limit_max _m = None (* TODO *) - let free m base = Backend.free m.data base + let free m base = Backend.free m.data base - let realloc m ~ptr ~size = Backend.realloc m.data ~ptr ~size + let realloc m ~ptr ~size = Backend.realloc m.data ~ptr ~size (* TODO: Move this into a separate module? *) module ITbl = Hashtbl.Make (struct include Int - let hash x = x + let hash x = x end) type collection = t ITbl.t Env_id.Tbl.t @@ -568,12 +568,12 @@

87.60%

let clone collection = (* TODO: this is ugly and should be rewritten *) - let s = Env_id.Tbl.to_seq collection in - Env_id.Tbl.of_seq - @@ Seq.map + let s = Env_id.Tbl.to_seq collection in + Env_id.Tbl.of_seq + @@ Seq.map (fun (i, t) -> - let s = ITbl.to_seq t in - (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, clone a)) s) ) + let s = ITbl.to_seq t in + (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, clone a)) s) ) s let convert (orig_mem : Concrete_memory.t) : t = @@ -581,17 +581,17 @@

87.60%

create s let get_env env_id memories = - match Env_id.Tbl.find_opt memories env_id with - | Some env -> env + match Env_id.Tbl.find_opt memories env_id with + | Some env -> env | None -> let t = ITbl.create 0 in Env_id.Tbl.add memories env_id t; t let get_memory env_id (orig_memory : Concrete_memory.t) collection g_id = - let env = get_env env_id collection in - match ITbl.find_opt env g_id with - | Some t -> t + let env = get_env env_id collection in + match ITbl.find_opt env g_id with + | Some t -> t | None -> let t = convert orig_memory in ITbl.add env g_id t; diff --git a/coverage/src/symbolic/symbolic_table.ml.html b/coverage/src/symbolic/symbolic_table.ml.html index 33d61490..966eeb53 100644 --- a/coverage/src/symbolic/symbolic_table.ml.html +++ b/coverage/src/symbolic/symbolic_table.ml.html @@ -224,7 +224,7 @@

71.11%

module ITbl = Hashtbl.Make (struct include Int - let hash x = x + let hash x = x end) type t = @@ -233,7 +233,7 @@

71.11%

; typ : binary ref_type } -let clone_t { limits; data; typ } = { typ; limits; data = Array.copy data } +let clone_t { limits; data; typ } = { typ; limits; data = Array.copy data } type collection = t ITbl.t Env_id.Tbl.t @@ -241,12 +241,12 @@

71.11%

let clone (collection : collection) = (* TODO: this is ugly and should be rewritten *) - let s = Env_id.Tbl.to_seq collection in - Env_id.Tbl.of_seq - @@ Seq.map + let s = Env_id.Tbl.to_seq collection in + Env_id.Tbl.of_seq + @@ Seq.map (fun (i, t) -> - let s = ITbl.to_seq t in - (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, clone_t a)) s) ) + let s = ITbl.to_seq t in + (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, clone_t a)) s) ) s let convert_ref_values (v : Concrete_value.ref_value) : Symbolic_value.ref_value @@ -260,8 +260,8 @@

71.11%

} let get_env env_id tables = - match Env_id.Tbl.find_opt tables env_id with - | Some env -> env + match Env_id.Tbl.find_opt tables env_id with + | Some env -> env | None -> let t = ITbl.create 0 in Env_id.Tbl.add tables env_id t; @@ -269,21 +269,21 @@

71.11%

let get_table env_id (orig_table : Concrete_table.t) (collection : collection) t_id = - let env = get_env env_id collection in - match ITbl.find_opt env t_id with - | Some t -> t + let env = get_env env_id collection in + match ITbl.find_opt env t_id with + | Some t -> t | None -> let t = convert orig_table in ITbl.add env t_id t; t -let get t i = t.data.(i) +let get t i = t.data.(i) let set t i v = t.data.(i) <- v -let size t = Array.length t.data +let size t = Array.length t.data -let typ t = t.typ +let typ t = t.typ let max_size t = t.limits.max diff --git a/coverage/src/symbolic/symbolic_value.ml.html b/coverage/src/symbolic/symbolic_value.ml.html index 284eb0bf..8ba18c2d 100644 --- a/coverage/src/symbolic/symbolic_value.ml.html +++ b/coverage/src/symbolic/symbolic_value.ml.html @@ -1012,9 +1012,9 @@

85.66%

| F64 of float64 | Ref of ref_value -let const_i32 (i : Int32.t) : int32 = value (Num (I32 i)) +let const_i32 (i : Int32.t) : int32 = value (Num (I32 i)) -let const_i64 (i : Int64.t) : int64 = value (Num (I64 i)) +let const_i64 (i : Int64.t) : int64 = value (Num (I64 i)) let const_f32 (f : Float32.t) : float32 = value (Num (F32 (Float32.to_bits f))) @@ -1043,8 +1043,8 @@

85.66%

module Ref = struct let get_func (r : ref_value) : Func_intf.t Value_intf.get_ref = - match r with - | Funcref (Some f) -> Ref_value f + match r with + | Funcref (Some f) -> Ref_value f | Funcref None -> Null | Externref _ -> Type_mismatch @@ -1059,22 +1059,22 @@

85.66%

end module Bool = struct - let const b = Bool.v b + let const b = Bool.v b - let not e = Bool.not e + let not e = Bool.not e - let or_ e1 e2 = Bool.or_ e1 e2 + let or_ e1 e2 = Bool.or_ e1 e2 - let and_ e1 e2 = Bool.and_ e1 e2 + let and_ e1 e2 = Bool.and_ e1 e2 let int32 e = - match view e with - | Val True -> const_i32 1l - | Val False -> const_i32 0l + match view e with + | Val True -> const_i32 1l + | Val False -> const_i32 0l | Cvtop (Ty_bitv 32, ToBool, e') -> e' - | _ -> make (Cvtop (Ty_bitv 32, OfBool, e)) + | _ -> make (Cvtop (Ty_bitv 32, OfBool, e)) - let select_expr c ~if_true ~if_false = Bool.ite c if_true if_false + let select_expr c ~if_true ~if_false = Bool.ite c if_true if_false let pp ppf (e : vbool) = Expr.pp ppf e end @@ -1084,7 +1084,7 @@

85.66%

let zero = const_i32 0l - let clz e = unop ty Clz e + let clz e = unop ty Clz e let ctz e = unop ty Ctz e @@ -1092,11 +1092,11 @@

85.66%

(* TODO *) assert false - let add e1 e2 = binop ty Add e1 e2 + let add e1 e2 = binop ty Add e1 e2 let sub e1 e2 = binop ty Sub e1 e2 - let mul e1 e2 = binop ty Mul e1 e2 + let mul e1 e2 = binop ty Mul e1 e2 let div e1 e2 = binop ty Div e1 e2 @@ -1104,18 +1104,18 @@

85.66%

let rem e1 e2 = binop ty Rem e1 e2 - let unsigned_rem e1 e2 = binop ty RemU e1 e2 + let unsigned_rem e1 e2 = binop ty RemU e1 e2 let boolify e = - match view e with - | Val (Num (I32 0l)) -> Some (Bool.const false) - | Val (Num (I32 1l)) -> Some (Bool.const true) - | Cvtop (_, OfBool, cond) -> Some cond - | _ -> None + match view e with + | Val (Num (I32 0l)) -> Some (Bool.const false) + | Val (Num (I32 1l)) -> Some (Bool.const true) + | Cvtop (_, OfBool, cond) -> Some cond + | _ -> None let logand e1 e2 = - match (boolify e1, boolify e2) with - | Some b1, Some b2 -> Bool.int32 (Bool.and_ b1 b2) + match (boolify e1, boolify e2) with + | Some b1, Some b2 -> Bool.int32 (Bool.and_ b1 b2) | _ -> binop ty And e1 e2 let logor e1 e2 = @@ -1125,57 +1125,57 @@

85.66%

let logxor e1 e2 = binop ty Xor e1 e2 - let shl e1 e2 = binop ty Shl e1 e2 + let shl e1 e2 = binop ty Shl e1 e2 - let shr_s e1 e2 = binop ty ShrA e1 e2 + let shr_s e1 e2 = binop ty ShrA e1 e2 - let shr_u e1 e2 = binop ty ShrL e1 e2 + let shr_u e1 e2 = binop ty ShrL e1 e2 let rotl e1 e2 = binop ty Rotl e1 e2 let rotr e1 e2 = binop ty Rotr e1 e2 let eq_const e c = - match view e with - | Cvtop (_, OfBool, cond) -> begin - match c with 0l -> Bool.not cond | 1l -> cond | _ -> Bool.const false + match view e with + | Cvtop (_, OfBool, cond) -> begin + match c with 0l -> Bool.not cond | 1l -> cond | _ -> Bool.const false end - | _ -> relop Ty_bool Eq e (const_i32 c) + | _ -> relop Ty_bool Eq e (const_i32 c) let eq e1 e2 = - if phys_equal e1 e2 then Bool.const true else relop Ty_bool Eq e1 e2 + if phys_equal e1 e2 then Bool.const true else relop Ty_bool Eq e1 e2 let ne e1 e2 = - if phys_equal e1 e2 then Bool.const false else relop Ty_bool Ne e1 e2 + if phys_equal e1 e2 then Bool.const false else relop Ty_bool Ne e1 e2 let lt e1 e2 = - if phys_equal e1 e2 then Bool.const false else relop ty Lt e1 e2 + if phys_equal e1 e2 then Bool.const false else relop ty Lt e1 e2 let gt e1 e2 = - if phys_equal e1 e2 then Bool.const false else relop ty Gt e1 e2 + if phys_equal e1 e2 then Bool.const false else relop ty Gt e1 e2 let lt_u e1 e2 = - if phys_equal e1 e2 then Bool.const false else relop ty LtU e1 e2 + if phys_equal e1 e2 then Bool.const false else relop ty LtU e1 e2 let gt_u e1 e2 = if phys_equal e1 e2 then Bool.const false else relop ty GtU e1 e2 - let le e1 e2 = if phys_equal e1 e2 then Bool.const true else relop ty Le e1 e2 + let le e1 e2 = if phys_equal e1 e2 then Bool.const true else relop ty Le e1 e2 - let ge e1 e2 = if phys_equal e1 e2 then Bool.const true else relop ty Ge e1 e2 + let ge e1 e2 = if phys_equal e1 e2 then Bool.const true else relop ty Ge e1 e2 let le_u e1 e2 = - if phys_equal e1 e2 then Bool.const true else relop ty LeU e1 e2 + if phys_equal e1 e2 then Bool.const true else relop ty LeU e1 e2 let ge_u e1 e2 = - if phys_equal e1 e2 then Bool.const true else relop ty GeU e1 e2 + if phys_equal e1 e2 then Bool.const true else relop ty GeU e1 e2 let to_bool (e : vbool) = - match view e with - | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l - | Ptr _ -> Bool.const true - | Cvtop (_, OfBool, cond) -> cond - | _ -> make (Cvtop (ty, ToBool, e)) + match view e with + | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l + | Ptr _ -> Bool.const true + | Cvtop (_, OfBool, cond) -> cond + | _ -> make (Cvtop (ty, ToBool, e)) let trunc_f32_s x = cvtop ty TruncSF32 x diff --git a/coverage/src/symbolic/symbolic_wasm_ffi.ml.html b/coverage/src/symbolic/symbolic_wasm_ffi.ml.html index 3a7e49d4..139ee1fd 100644 --- a/coverage/src/symbolic/symbolic_wasm_ffi.ml.html +++ b/coverage/src/symbolic/symbolic_wasm_ffi.ml.html @@ -262,13 +262,13 @@

100.00%

module Value = Symbolic_value let assume_i32 (i : Value.int32) : unit Choice.t = - Choice.add_pc @@ Value.I32.to_bool i + Choice.add_pc @@ Value.I32.to_bool i let assume_positive_i32 (i : Value.int32) : unit Choice.t = Choice.add_pc @@ Value.I32.ge i Value.I32.zero let assert_i32 (i : Value.int32) : unit Choice.t = - Choice.assertion @@ Value.I32.to_bool i + Choice.assertion @@ Value.I32.to_bool i let symbol_i8 () = Choice.with_new_symbol (Ty_bitv 8) (fun sym -> @@ -289,10 +289,10 @@

100.00%

let abort () : unit Choice.t = Choice.add_pc @@ Value.Bool.const false let alloc m (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t = - Choice.lift_mem @@ Memory.realloc m ~ptr:base ~size + Choice.lift_mem @@ Memory.realloc m ~ptr:base ~size let free m (ptr : Value.int32) : Value.int32 Choice.t = - Choice.lift_mem @@ Memory.free m ptr + Choice.lift_mem @@ Memory.free m ptr let exit (_p : Value.int32) : unit Choice.t = abort () end diff --git a/coverage/src/symbolic/thread.ml.html b/coverage/src/symbolic/thread.ml.html index c9bf76e2..2c076004 100644 --- a/coverage/src/symbolic/thread.ml.html +++ b/coverage/src/symbolic/thread.ml.html @@ -178,7 +178,7 @@

100.00%

} let create symbols symbol_set pc memories tables globals breadcrumbs = - { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs } + { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs } let init () = let symbols = 0 in @@ -190,34 +190,34 @@

100.00%

let breadcrumbs = [] in create symbols symbol_set pc memories tables globals breadcrumbs - let symbols t = t.symbols + let symbols t = t.symbols - let symbols_set t = t.symbol_set + let symbols_set t = t.symbol_set - let pc t = t.pc + let pc t = t.pc - let memories t = t.memories + let memories t = t.memories - let tables t = t.tables + let tables t = t.tables - let globals t = t.globals + let globals t = t.globals - let breadcrumbs t = t.breadcrumbs + let breadcrumbs t = t.breadcrumbs let add_symbol t s = { t with symbol_set = s :: t.symbol_set } - let add_pc t c = { t with pc = c :: t.pc } + let add_pc t c = { t with pc = c :: t.pc } - let add_breadcrumb t crumb = { t with breadcrumbs = crumb :: t.breadcrumbs } + let add_breadcrumb t crumb = { t with breadcrumbs = crumb :: t.breadcrumbs } - let incr_symbols t = { t with symbols = succ t.symbols } + let incr_symbols t = { t with symbols = succ t.symbols } let clone { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs } = - let memories = Memory.clone memories in - let tables = Symbolic_table.clone tables in - let globals = Symbolic_global.clone globals in - { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs } + let memories = Memory.clone memories in + let tables = Symbolic_table.clone tables in + let globals = Symbolic_global.clone globals in + { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs } end diff --git a/coverage/src/symbolic/thread_with_memory.ml.html b/coverage/src/symbolic/thread_with_memory.ml.html index 778cce94..ce74b843 100644 --- a/coverage/src/symbolic/thread_with_memory.ml.html +++ b/coverage/src/symbolic/thread_with_memory.ml.html @@ -102,33 +102,33 @@

100.00%

include Thread.Make (Symbolic_memory_concretizing) let project (th : t) : Thread_without_memory.t * _ = - let projected = + let projected = let symbols = symbols th in - let symbols_set = symbols_set th in - let pc = pc th in - let memories = Thread_without_memory.Memory.init () in - let tables = tables th in - let globals = globals th in - let breadcrumbs = breadcrumbs th in - Thread_without_memory.create symbols symbols_set pc memories tables globals + let symbols_set = symbols_set th in + let pc = pc th in + let memories = Thread_without_memory.Memory.init () in + let tables = tables th in + let globals = globals th in + let breadcrumbs = breadcrumbs th in + Thread_without_memory.create symbols symbols_set pc memories tables globals breadcrumbs in let backup = memories th in - (projected, backup) + (projected, backup) let restore backup th = - let symbols = Thread_without_memory.symbols th in - let symbols_set = Thread_without_memory.symbols_set th in - let pc = Thread_without_memory.pc th in - let memories = + let symbols = Thread_without_memory.symbols th in + let symbols_set = Thread_without_memory.symbols_set th in + let pc = Thread_without_memory.pc th in + let memories = if Thread_without_memory.memories th then Symbolic_memory_concretizing.clone backup - else backup + else backup in let tables = Thread_without_memory.tables th in - let globals = Thread_without_memory.globals th in - let breadcrumbs = Thread_without_memory.breadcrumbs th in - create symbols symbols_set pc memories tables globals breadcrumbs + let globals = Thread_without_memory.globals th in + let breadcrumbs = Thread_without_memory.breadcrumbs th in + create symbols symbols_set pc memories tables globals breadcrumbs diff --git a/coverage/src/symbolic/thread_without_memory.ml.html b/coverage/src/symbolic/thread_without_memory.ml.html index 8a230920..e3816ebe 100644 --- a/coverage/src/symbolic/thread_without_memory.ml.html +++ b/coverage/src/symbolic/thread_without_memory.ml.html @@ -56,9 +56,9 @@

100.00%

include Thread.Make (struct type collection = bool - let init () = false + let init () = false - let clone _ = true + let clone _ = true end) diff --git a/coverage/src/utils/log.ml.html b/coverage/src/utils/log.ml.html index d08739a2..67bdea5d 100644 --- a/coverage/src/utils/log.ml.html +++ b/coverage/src/utils/log.ml.html @@ -91,13 +91,13 @@

83.33%

Fmt.flush Fmt.stderr () end -let debug1 t a : unit = if !debug_on then Fmt.epr t a +let debug1 t a : unit = if !debug_on then Fmt.epr t a -let debug2 t a b : unit = if !debug_on then Fmt.epr t a b +let debug2 t a b : unit = if !debug_on then Fmt.epr t a b let debug5 t a b c d e : unit = if !debug_on then Fmt.epr t a b c d e -let profile3 t a b c : unit = if !profiling_on then Fmt.epr t a b c +let profile3 t a b c : unit = if !profiling_on then Fmt.epr t a b c (* TODO: remove this *) let err f = Fmt.failwith f