From 759b65ca9baca979556c3334286f21098237b04e Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Tue, 21 May 2024 14:43:49 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20OCamlPro?= =?UTF-8?q?/owi@479cbcb143fe82d1007e6187cca719f3df4bd366=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- coverage/src/cmd/cmd_sym.ml.html | 70 +-- coverage/src/cmd/testcase.ml.html | 28 +- coverage/src/concrete/thread.ml.html | 16 +- coverage/src/data_structures/env_id.ml.html | 4 +- coverage/src/data_structures/func_id.ml.html | 4 +- coverage/src/data_structures/stack.ml.html | 40 +- coverage/src/interpret/interpret.ml.html | 524 +++++++++--------- coverage/src/link/link_env.ml.html | 12 +- coverage/src/primitives/int32.ml.html | 16 +- coverage/src/symbolic/solver.ml.html | 2 +- coverage/src/symbolic/symbolic.ml.html | 64 +-- coverage/src/symbolic/symbolic_choice.ml.html | 268 ++++----- coverage/src/symbolic/symbolic_global.ml.html | 32 +- coverage/src/symbolic/symbolic_memory.ml.html | 134 ++--- coverage/src/symbolic/symbolic_table.ml.html | 30 +- coverage/src/symbolic/symbolic_value.ml.html | 90 +-- coverage/src/utils/log.ml.html | 6 +- coverage/src/utils/syntax.ml.html | 2 +- 18 files changed, 671 insertions(+), 671 deletions(-) diff --git a/coverage/src/cmd/cmd_sym.ml.html b/coverage/src/cmd/cmd_sym.ml.html index 66f53236d..b66518f87 100644 --- a/coverage/src/cmd/cmd_sym.ml.html +++ b/coverage/src/cmd/cmd_sym.ml.html @@ -691,16 +691,16 @@

85.29%

| _ -> sym_expr ) in let assume_i32 (i : Value.int32) : unit Choice.t = - let c = Value.I32.to_bool i in - Choice.add_pc c + let c = Value.I32.to_bool i in + Choice.add_pc c in let assume_positive_i32 (i : Value.int32) : unit Choice.t = let c = Value.I32.ge i Value.I32.zero in Choice.add_pc c in let assert_i32 (i : Value.int32) : unit Choice.t = - let c = Value.I32.to_bool i in - Choice.assertion c + let c = Value.I32.to_bool i in + Choice.assertion c in (* we need to describe their types *) let functions = @@ -738,40 +738,40 @@

85.29%

let abort () : unit Choice.t = Choice.add_pc @@ Value.Bool.const false in let i32 v : int32 Choice.t = - match view v with - | Val (Num (I32 v)) -> Choice.return v + match view v with + | Val (Num (I32 v)) -> Choice.return v | _ -> Log.debug2 {|alloc: cannot allocate base pointer "%a"|} Expr.pp v; Choice.bind (abort ()) (fun () -> Choice.return 666l) in let ptr v : int32 Choice.t = - match view v with - | Ptr (b, _) -> Choice.return b + match view v with + | Ptr (b, _) -> Choice.return b | _ -> Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v; Choice.bind (abort ()) (fun () -> Choice.return 667l) in let alloc (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t = - Choice.bind (i32 base) (fun base -> - Choice.with_thread (fun t -> - let memories = Thread.memories t in - Symbolic_memory.iter + Choice.bind (i32 base) (fun base -> + Choice.with_thread (fun t -> + let memories = Thread.memories t in + Symbolic_memory.iter (fun tbl -> - Symbolic_memory.ITbl.iter + Symbolic_memory.ITbl.iter (fun _ (m : Symbolic_memory.t) -> - Symbolic_memory.replace_size m base size ) + Symbolic_memory.replace_size m base size ) tbl ) memories; - Expr.make (Ptr (base, Value.const_i32 0l)) ) ) + Expr.make (Ptr (base, Value.const_i32 0l)) ) ) in let free (p : Value.int32) : unit Choice.t = - Choice.bind (ptr p) (fun base -> - Choice.with_thread (fun t -> - let memories = Thread.memories t in - Symbolic_memory.iter + Choice.bind (ptr p) (fun base -> + Choice.with_thread (fun t -> + let memories = Thread.memories t in + Symbolic_memory.iter (fun tbl -> - Symbolic_memory.ITbl.iter - (fun _ (m : Symbolic_memory.t) -> Symbolic_memory.free m base) + Symbolic_memory.ITbl.iter + (fun _ (m : Symbolic_memory.t) -> Symbolic_memory.free m base) tbl ) memories ) ) in @@ -901,10 +901,10 @@

85.29%

run_binary_modul ~unsafe ~optimize pc m let get_model ~symbols solver pc = - assert (`Sat = Solver.Z3Batch.check solver pc); + assert (`Sat = Solver.Z3Batch.check solver pc); match Solver.Z3Batch.model ~symbols solver with | None -> assert false - | Some model -> model + | Some model -> model (* NB: This function propagates potential errors (Result.err) occurring during evaluation (OS, syntax error, etc.), except for Trap and Assert, @@ -931,13 +931,13 @@

85.29%

Format.pp_std "Model:@\n @[<v>%a@]@." (Smtml.Model.pp ~no_values) model in let rec print_and_count_failures count_acc results = - match results () with + match results () with | Seq.Nil -> Ok count_acc - | Seq.Cons ((result, thread), tl) -> + | Seq.Cons ((result, thread), tl) -> let pc = Thread.pc thread in - let symbols = thread.symbol_set in + let symbols = thread.symbol_set in let model = get_model ~symbols solver pc in - let* is_err = + let* is_err = let open Symbolic_choice.Multicore in match result with | EAssert assertion -> @@ -946,20 +946,20 @@

85.29%

| ETrap tr -> print_bug (`ETrap (tr, model)); Ok true - | EVal (Ok ()) -> Ok false + | EVal (Ok ()) -> Ok false | EVal (Error e) -> Error e in - let count_acc = if is_err then succ count_acc else count_acc in + let count_acc = if is_err then succ count_acc else count_acc in let* () = if not no_values then - let testcase = - List.sort compare (Smtml.Model.get_bindings model) |> List.map snd + let testcase = + List.sort compare (Smtml.Model.get_bindings model) |> List.map snd in - Testcase.write_testcase ~dir:workspace ~err:is_err testcase + Testcase.write_testcase ~dir:workspace ~err:is_err testcase else Ok () in - if (not is_err) || no_stop_at_failure then - print_and_count_failures count_acc tl + if (not is_err) || no_stop_at_failure then + print_and_count_failures count_acc tl else Ok count_acc in let results = @@ -969,7 +969,7 @@

85.29%

(x, List.rev @@ Thread.breadcrumbs th) ) |> List.of_seq |> List.sort (fun (_, bc1) (_, bc2) -> - List.compare Stdlib.Int32.compare bc1 bc2 ) + List.compare Stdlib.Int32.compare bc1 bc2 ) |> List.to_seq |> Seq.map fst else results in diff --git a/coverage/src/cmd/testcase.ml.html b/coverage/src/cmd/testcase.ml.html index 9c3450290..66d7c3d05 100644 --- a/coverage/src/cmd/testcase.ml.html +++ b/coverage/src/cmd/testcase.ml.html @@ -96,30 +96,30 @@

100.00%

open Syntax let out_testcase ~dst ~err testcase = - let o = Xmlm.make_output ~nl:true ~indent:(Some 2) dst in - let tag ?(atts = []) name = (("", name), atts) in - let atts = if err then Some [ (("", "coversError"), "true") ] else None in - let to_string v = Format.asprintf "%a" Smtml.Value.pp_num v in - let input v = `El (tag "input", [ `Data (to_string v) ]) in - let testcase = `El (tag ?atts "testcase", List.map input testcase) in + let o = Xmlm.make_output ~nl:true ~indent:(Some 2) dst in + let tag ?(atts = []) name = (("", name), atts) in + let atts = if err then Some [ (("", "coversError"), "true") ] else None in + let to_string v = Format.asprintf "%a" Smtml.Value.pp_num v in + let input v = `El (tag "input", [ `Data (to_string v) ]) in + let testcase = `El (tag ?atts "testcase", List.map input testcase) in let dtd = {|<!DOCTYPE testcase PUBLIC "+//IDN sosy-lab.org//DTD test-format testcase 1.1//EN" "https://sosy-lab.org/test-format/testcase-1.1.dtd">|} in Xmlm.output o (`Dtd (Some dtd)); - Xmlm.output_tree Fun.id o testcase + Xmlm.output_tree Fun.id o testcase let write_testcase = let cnt = ref 0 in fun ~dir ~err testcase -> - incr cnt; - let name = Format.ksprintf Fpath.v "testcase-%d.xml" !cnt in - let path = Fpath.append dir name in - let* res = - Bos.OS.File.with_oc path - (fun chan () -> Ok (out_testcase ~dst:(`Channel chan) ~err testcase)) + incr cnt; + let name = Format.ksprintf Fpath.v "testcase-%d.xml" !cnt in + let path = Fpath.append dir name in + let* res = + Bos.OS.File.with_oc path + (fun chan () -> Ok (out_testcase ~dst:(`Channel chan) ~err testcase)) () in - res + res diff --git a/coverage/src/concrete/thread.ml.html b/coverage/src/concrete/thread.ml.html index 34fe45a5b..0c450e38e 100644 --- a/coverage/src/concrete/thread.ml.html +++ b/coverage/src/concrete/thread.ml.html @@ -125,13 +125,13 @@

100.00%

; breadcrumbs : int32 list } -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 @@ -146,10 +146,10 @@

100.00%

} let clone { choices; symbol_set; pc; memories; tables; globals; breadcrumbs } = - let memories = Symbolic_memory.clone memories in - let tables = Symbolic_table.clone tables in - let globals = Symbolic_global.clone globals in - { choices; symbol_set; pc; memories; tables; globals; breadcrumbs } + let memories = Symbolic_memory.clone memories in + let tables = Symbolic_table.clone tables in + let globals = Symbolic_global.clone globals in + { choices; symbol_set; pc; memories; tables; globals; breadcrumbs } diff --git a/coverage/src/data_structures/env_id.ml.html b/coverage/src/data_structures/env_id.ml.html index ed78119c2..94f7efe19 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 60f1efce9..9b5c9d32e 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 58e61aa87..49d1b5501 100644 --- a/coverage/src/data_structures/stack.ml.html +++ b/coverage/src/data_structures/stack.ml.html @@ -581,13 +581,13 @@

82.76%

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) @@ -610,21 +610,21 @@

82.76%

let pp fmt (s : t) = Format.pp_list ~pp_sep:(fun fmt () -> Format.pp_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) + let hd, tl = pop s in + match hd with + | I32 n -> (n, tl) | _ -> Log.err "invalid type (expected i32)" 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) + let n2, s = pop s in + let n1, tl = pop s in + match (n1, n2) with + | I32 n1, I32 n2 -> ((n1, n2), tl) | _ -> Log.err "invalid type (expected i32)" let pop_i64 s = @@ -679,19 +679,19 @@

82.76%

| _ -> Log.err "invalid type (expected ref)" let pop_bool s = - let hd, tl = pop s in - match hd with - | I32 n -> (V.I32.to_bool n, tl) + let hd, tl = pop s in + match hd with + | I32 n -> (V.I32.to_bool n, tl) | _ -> Log.err "invalid type (expected i32 (bool))" 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 [] -> invalid_arg "drop_n" | _ :: tl -> drop_n tl (n - 1) + if n = 0 then s + else match s with [] -> invalid_arg "drop_n" | _ :: tl -> drop_n tl (n - 1) end diff --git a/coverage/src/interpret/interpret.ml.html b/coverage/src/interpret/interpret.ml.html index a8e2caa3c..2a950dd9e 100644 --- a/coverage/src/interpret/interpret.ml.html +++ b/coverage/src/interpret/interpret.ml.html @@ -3333,7 +3333,7 @@

91.59%

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

91.59%

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 p_type_eq (_id1, t1) (_id2, t2) = t1 = t2 + let p_type_eq (_id1, t1) (_id2, t2) = t1 = t2 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 -> @@ -3434,15 +3434,15 @@

91.59%

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 - | Sub -> Choice.return @@ sub n1 n2 - | Mul -> Choice.return @@ mul n1 n2 + | Add -> Choice.return @@ add n1 n2 + | Sub -> Choice.return @@ sub 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 @@ -3454,24 +3454,24 @@

91.59%

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 - | S -> Choice.return @@ rem n1 n2 + match s with + | S -> Choice.return @@ 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 + | 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 | 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 = @@ -3541,10 +3541,10 @@

91.59%

| 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 @@ -3552,22 +3552,22 @@

91.59%

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 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 -> @@ -3761,8 +3761,8 @@

91.59%

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 @@ -3774,10 +3774,10 @@

91.59%

type extern_func = Extern_func.extern_func let exec_extern_func 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 @@ -3791,45 +3791,45 @@

91.59%

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 - | Extern_func.Arg (_, args) -> split_one_arg args + | Extern_func.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 - | Extern_func.Arg (arg, args) -> - let* v, stack = pop_arg stack arg in - apply stack args (f v) + match ty with + | Extern_func.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 = - match arg with - | I32 -> Stack.push_i32 stack v + 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 | 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 @@ -3854,12 +3854,12 @@

91.59%

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 @@ -3936,19 +3936,19 @@

91.59%

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 @@ -3958,50 +3958,50 @@

91.59%

| 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 @@ -4011,17 +4011,17 @@

91.59%

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 @@ -4030,24 +4030,24 @@

91.59%

; 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.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.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 -> @@ -4075,56 +4075,56 @@

91.59%

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 - if ref_kind <> Func_ht then Choice.trap Indirect_call_type_mismatch + 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 + if ref_kind <> Func_ht then Choice.trap Indirect_call_type_mismatch else - let size = Table.size t in - let> out_of_bounds = - Bool.or_ I32.(fun_i < const 0l) @@ I32.(consti size <= fun_i) + let size = Table.size t in + let> out_of_bounds = + Bool.or_ I32.(fun_i < const 0l) @@ I32.(consti size <= fun_i) in - if out_of_bounds then Choice.trap Undefined_element + 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 - match Ref.get_func f_ref with + 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 + 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 pt, rt = func_type state func in - let pt', rt' = typ_i in - if not (rt = rt' && List.equal p_type_eq pt pt') then + let pt', rt' = typ_i in + if not (rt = rt' && List.equal p_type_eq pt pt') then Choice.trap Indirect_call_type_mismatch - else exec_vfunc ~return state func + else exec_vfunc ~return state func 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 + | 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 @@ -4183,31 +4183,31 @@

91.59%

| 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 + | 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 @@ -4276,13 +4276,13 @@

91.59%

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 @@ -4290,25 +4290,25 @@

91.59%

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 - if Global.mut global = Const then Log.err "Can't set const global"; - 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 + if Global.mut global = Const then Log.err "Can't set const global"; + 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) @@ -4320,7 +4320,7 @@

91.59%

(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 @@ -4478,75 +4478,75 @@

91.59%

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.(Memory.size mem < addr + const 1l) - @@ Bool.or_ I32.(pos < const 0l) - @@ Bool.or_ I32.(addr + const 1l < const 0l) - @@ I32.(addr < const 0l) + Bool.or_ I32.(offset < const 0l) + @@ Bool.or_ I32.(Memory.size mem < addr + const 1l) + @@ Bool.or_ I32.(pos < const 0l) + @@ Bool.or_ I32.(addr + const 1l < const 0l) + @@ I32.(addr < 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 = - (if sx = S then Memory.load_8_s else Memory.load_8_u) mem addr + let* res = + (if sx = S then Memory.load_8_s else 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.(Memory.size mem < addr + const 1l) - @@ Bool.or_ I32.(pos < const 0l) - @@ Bool.or_ I32.(addr + const 1l < const 0l) - @@ I32.(addr < const 0l) + Bool.or_ I32.(offset < const 0l) + @@ Bool.or_ I32.(Memory.size mem < addr + const 1l) + @@ Bool.or_ I32.(pos < const 0l) + @@ Bool.or_ I32.(addr + const 1l < const 0l) + @@ I32.(addr < 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) - @@ Bool.or_ I32.(pos < const 0l) - @@ I32.(addr < const 0l) + Bool.or_ I32.(offset < const 0l) + @@ Bool.or_ I32.(pos < const 0l) + @@ I32.(addr < 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 @@ -4581,26 +4581,26 @@

91.59%

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 - let> out_of_bounds = I32.(offset < const 0l) in - if out_of_bounds then Choice.trap Out_of_bounds_memory_access + | 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 + let> out_of_bounds = I32.(offset < const 0l) in + if out_of_bounds then Choice.trap Out_of_bounds_memory_access else - match nn with - | S32 -> + 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 -> let n, stack = Stack.pop_i64 stack in @@ -4736,13 +4736,13 @@

91.59%

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 = 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) @@ -4772,19 +4772,19 @@

91.59%

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 @@ -4803,7 +4803,7 @@

91.59%

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

91.59%

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.modul modul).id + Log.profile3 "Exec module %s@.%a@." + (Option.value (Module_to_run.modul modul).id ~default:"anonymous" ) State.print_count count; - match end_stack with - | [] -> () + match end_stack with + | [] -> () | _ :: _ -> Format.pp_err "non empty stack@\n%a@." Stack.pp end_stack; assert false ) (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 a31d51275..5afd35046 100644 --- a/coverage/src/link/link_env.ml.html +++ b/coverage/src/link/link_env.ml.html @@ -357,21 +357,21 @@

91.18%

; id : Env_id.t } -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 4f0c19ec1..d9a6c9369 100644 --- a/coverage/src/primitives/int32.ml.html +++ b/coverage/src/primitives/int32.ml.html @@ -367,8 +367,8 @@

98.35%

(* 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 @@ -380,11 +380,11 @@

98.35%

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) @@ -397,12 +397,12 @@

98.35%

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 let eq (x : int32) y = x = y -let ne (x : int32) y = x <> y +let ne (x : int32) y = x <> y let lt (x : int32) y = x < y diff --git a/coverage/src/symbolic/solver.ml.html b/coverage/src/symbolic/solver.ml.html index 5dfd34ae7..9fbe7144d 100644 --- a/coverage/src/symbolic/solver.ml.html +++ b/coverage/src/symbolic/solver.ml.html @@ -74,7 +74,7 @@

100.00%

let solver_mod : Z3Batch.t solver_module = (module Z3Batch) let fresh_solver () = - let module Mapping = Smtml.Z3_mappings.Fresh.Make () in + let module Mapping = Smtml.Z3_mappings.Fresh.Make () in let module Batch = Smtml.Solver.Batch (Mapping) in let solver = Batch.create ~logic:QF_BVFP () in S ((module Batch), solver) diff --git a/coverage/src/symbolic/symbolic.ml.html b/coverage/src/symbolic/symbolic.ml.html index 1ac07a572..168c508e4 100644 --- a/coverage/src/symbolic/symbolic.ml.html +++ b/coverage/src/symbolic/symbolic.ml.html @@ -468,9 +468,9 @@

78.21%

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 -> @@ -499,12 +499,12 @@

78.21%

include Symbolic_memory let concretise (a : Smtml.Expr.t) : Smtml.Expr.t Choice.t = - let open Choice in + let open Choice in let open Smtml in match Expr.view a with (* Avoid unecessary re-hashconsing and allocation when the value is already concrete. *) - | Val _ | Ptr (_, { node = Val _; _ }) -> return a + | Val _ | Ptr (_, { node = Val _; _ }) -> return a | Ptr (base, offset) -> let+ offset = select_i32 offset in Expr.make (Ptr (base, Symbolic_value.const_i32 offset)) @@ -513,40 +513,40 @@

78.21%

Symbolic_value.const_i32 v let check_within_bounds m a = - match check_within_bounds m a with + match check_within_bounds m a with | Error t -> Choice.trap t - | Ok (cond, ptr) -> + | Ok (cond, ptr) -> let open Choice in - let* out_of_bounds = select cond in - if out_of_bounds then trap Trap.Memory_heap_buffer_overflow - else return ptr + let* out_of_bounds = select cond in + if out_of_bounds then trap Trap.Memory_heap_buffer_overflow + else return ptr let with_concrete (m : t) a f : 'a Choice.t = - let open Choice in - let* addr = concretise a in - let+ ptr = check_within_bounds m addr in - f m ptr + let open Choice in + let* addr = concretise a in + let+ ptr = check_within_bounds m addr in + f m ptr - let load_8_s m a = with_concrete m a load_8_s + let load_8_s m a = with_concrete m a load_8_s - let load_8_u m a = with_concrete m a load_8_u + let load_8_u m a = with_concrete m a load_8_u let load_16_s m a = with_concrete m a load_16_s let load_16_u m a = with_concrete m a load_16_u - let load_32 m a = with_concrete m a load_32 + let load_32 m a = with_concrete m a load_32 let load_64 m a = with_concrete m a load_64 let store_8 m ~addr v = - with_concrete m addr (fun m addr -> store_8 m ~addr v) + with_concrete m addr (fun m addr -> store_8 m ~addr v) let store_16 m ~addr v = with_concrete m addr (fun m addr -> store_16 m ~addr v) let store_32 m ~addr v = - with_concrete m addr (fun m addr -> store_32 m ~addr v) + with_concrete m addr (fun m addr -> store_32 m ~addr v) let store_64 m ~addr v = with_concrete m addr (fun m addr -> store_64 m ~addr v) @@ -564,10 +564,10 @@

78.21%

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 - Symbolic_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 + Symbolic_memory.get_memory (Link_env.id env) orig_mem memories id in Choice.with_thread f @@ -576,10 +576,10 @@

78.21%

let get_extern_func = Link_env.get_extern_func 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 tables = Thread.tables t in - Symbolic_table.get_table (Link_env.id env) orig_table tables i + let orig_table = Link_env.get_table env i in + let f (t : thread) = + let tables = Thread.tables t in + Symbolic_table.get_table (Link_env.id env) orig_table tables i in Choice.with_thread f @@ -590,10 +590,10 @@

78.21%

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 @@ -614,7 +614,7 @@

78.21%

let env (t : t) = t.env - let modul (t : t) = t.modul + let modul (t : t) = t.modul 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 1e99975db..9393cd58d 100644 --- a/coverage/src/symbolic/symbolic_choice.ml.html +++ b/coverage/src/symbolic/symbolic_choice.ml.html @@ -1308,22 +1308,22 @@

82.19%

} let take q pledge = - Mutex.lock q.mutex; - let r = + Mutex.lock q.mutex; + let r = try - while Queue.is_empty q.queue do - if q.pledges = 0 || q.failed then raise Exit; - Condition.wait q.cond q.mutex + while Queue.is_empty q.queue do + if q.pledges = 0 || q.failed then raise Exit; + Condition.wait q.cond q.mutex done; let v = Queue.pop q.queue in - if pledge then q.pledges <- q.pledges + 1; - Some v - with Exit -> + if pledge then q.pledges <- q.pledges + 1; + Some v + with Exit -> Condition.broadcast q.cond; - None + None in Mutex.unlock q.mutex; - r + r let make_pledge q = Mutex.lock q.mutex; @@ -1331,25 +1331,25 @@

82.19%

Mutex.unlock q.mutex let end_pledge q = - Mutex.lock q.mutex; - q.pledges <- q.pledges - 1; + Mutex.lock q.mutex; + q.pledges <- q.pledges - 1; Condition.broadcast q.cond; - Mutex.unlock q.mutex + Mutex.unlock q.mutex let rec read_as_seq (q : 'a t) ?(finalizer = Fun.const ()) : 'a Seq.t = - fun () -> - match take q false with + fun () -> + match take q false with | None -> finalizer (); Nil - | Some v -> Cons (v, read_as_seq q ~finalizer) + | Some v -> Cons (v, read_as_seq q ~finalizer) let push v q = - Mutex.lock q.mutex; - let was_empty = Queue.is_empty q.queue in - Queue.push v q.queue; - if was_empty then Condition.broadcast q.cond; - Mutex.unlock q.mutex + Mutex.lock q.mutex; + let was_empty = Queue.is_empty q.queue in + Queue.push v q.queue; + if was_empty then Condition.broadcast q.cond; + Mutex.unlock q.mutex let fail q = Mutex.lock q.mutex; @@ -1445,43 +1445,43 @@

82.19%

| Choice of (('a, 'wls) status * ('a, 'wls) status) | Stop - let run (Sched mxf) wls = mxf wls + let run (Sched 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) : _ t = - let rec bind_status (x : _ status) (f : _ -> _ status) : _ status = - match x with - | Now x -> f x - | Yield (prio, lx) -> - Yield (prio, Sched (fun wls -> bind_status (run lx wls) f)) - | Choice (mx1, mx2) -> Choice (bind_status mx1 f, bind_status mx2 f) - | Stop -> Stop + let rec bind_status (x : _ status) (f : _ -> _ status) : _ status = + match x with + | Now x -> f x + | Yield (prio, lx) -> + Yield (prio, Sched (fun wls -> bind_status (run lx wls) f)) + | Choice (mx1, mx2) -> Choice (bind_status mx1 f, bind_status mx2 f) + | Stop -> Stop in Sched (fun wls -> - let argumented_f x = run (f x) wls in + let argumented_f x = run (f x) wls in match run mx wls with - | Yield (prio, mx) -> Yield (prio, bind mx f) - | x -> bind_status x argumented_f ) + | Yield (prio, mx) -> Yield (prio, bind mx f) + | x -> bind_status x argumented_f ) 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 @@ -1505,30 +1505,30 @@

82.19%

let add_init_task sched task = WQ.push task sched.work_queue let rec work wls sched = - let rec handle_status (t : _ Schedulable.status) sched = - match t with - | Stop -> () - | Now x -> WQ.push x sched.res_writer - | Yield (_prio, f) -> WQ.push f sched.work_queue - | Choice (m1, m2) -> + let rec handle_status (t : _ Schedulable.status) sched = + match t with + | Stop -> () + | Now x -> WQ.push x sched.res_writer + | Yield (_prio, f) -> WQ.push f sched.work_queue + | Choice (m1, m2) -> handle_status m1 sched; - handle_status m2 sched + handle_status m2 sched in match WQ.take sched.work_queue true with - | None -> () - | Some f -> begin - handle_status (Schedulable.run f wls) sched; - WQ.end_pledge sched.work_queue; - work wls sched + | None -> () + | Some f -> begin + handle_status (Schedulable.run f wls) sched; + WQ.end_pledge sched.work_queue; + work wls sched end let spawn_worker sched wls_init = WQ.make_pledge sched.res_writer; Domain.spawn (fun () -> - let wls = wls_init () in + let wls = wls_init () in try work wls sched; - WQ.end_pledge sched.res_writer + WQ.end_pledge sched.res_writer with e -> let bt = Printexc.get_raw_backtrace () in WQ.fail sched.work_queue; @@ -1545,37 +1545,37 @@

82.19%

type 'a t = St of (Thread.t -> ('a * Thread.t, solver) 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 = let ( let+ ) = M.( let+ ) in St (fun st -> - 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)) end module Eval = struct @@ -1592,30 +1592,30 @@

82.19%

type 'a t = 'a eval 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 - | ETrap _ as mx -> M.return mx - | EAssert _ as mx -> M.return mx + 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) - | ETrap _ as mx -> mx - | EAssert _ as mx -> mx + match mx with + | EVal x -> EVal (f x) + | ETrap _ as mx -> mx + | EAssert _ as mx -> mx let ( let+ ) = map end @@ -1630,26 +1630,26 @@

82.19%

let lift_schedulable (v : ('a, _) Schedulable.t) : 'a t = lift (State.lift v) - let with_thread f = lift (State.with_state (fun st -> (f st, st))) + let with_thread f = lift (State.with_state (fun st -> (f st, st))) 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 @@ -1671,9 +1671,9 @@

82.19%

WQ.read_as_seq sched.res_writer ~finalizer:(fun () -> Array.iter Domain.join join_handles ) - let trap t = State.return (ETrap t) + let trap t = State.return (ETrap t) - let assertion_fail c = State.return (EAssert c) + let assertion_fail c = State.return (EAssert c) end (* @@ -1684,17 +1684,17 @@

82.19%

include CoreImpl let add_pc (c : vbool) = - match Expr.view c with + match Expr.view c with | Val True -> return () - | Val False -> stop - | _ -> + | Val False -> stop + | _ -> let* thread in - let new_thread = { thread with pc = c :: thread.pc } in + let new_thread = { thread with pc = c :: thread.pc } in set_thread new_thread [@@inline] let add_breadcrumb crumb = - modify_thread (fun t -> { t with breadcrumbs = crumb :: t.breadcrumbs }) + modify_thread (fun t -> { t with breadcrumbs = crumb :: t.breadcrumbs }) (* Yielding is currently done each time the solver is about to be called, @@ -1702,56 +1702,56 @@

82.19%

*) let check_reachability = let* () = yield in - let* (S (solver_module, s)) = solver in - let module Solver = (val solver_module) in + let* (S (solver_module, s)) = solver in + let module Solver = (val solver_module) in let* thread in - match Solver.check s thread.pc with - | `Sat -> return () - | `Unsat | `Unknown -> stop + match Solver.check s thread.pc with + | `Sat -> return () + | `Unsat | `Unknown -> stop let get_model symbol = - let* () = yield in - let* (S (solver_module, s)) = solver in - let module Solver = (val solver_module) in + let* () = yield in + let* (S (solver_module, s)) = solver in + let module Solver = (val solver_module) in let+ thread in - match Solver.check s thread.pc with - | `Unsat | `Unknown -> None - | `Sat -> begin + match Solver.check s thread.pc with + | `Unsat | `Unknown -> None + | `Sat -> begin let model = Solver.model ~symbols:[ symbol ] s in - match model with + match model with | None -> failwith "Unreachable: The problem is sat so a model should exist" - | Some model -> begin + | Some model -> begin match Model.evaluate model symbol with | None -> failwith "Unreachable: The model exists so this symbol should evaluate" - | Some _ as v -> v + | Some _ as v -> v end end let get_model_or_stop symbol = - let* model = get_model symbol in - match model with Some v -> return v | None -> stop + let* model = get_model symbol in + match model with Some v -> return v | None -> stop let select (cond : Symbolic_value.vbool) = - let v = Expr.simplify cond in - match Expr.view v with - | Val True -> return true - | Val False -> return false + let v = Expr.simplify cond in + match Expr.view v with + | Val True -> return true + | Val False -> return false | Val (Num (I32 _)) -> 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 choose true_branch false_branch [@@inline] @@ -1769,42 +1769,42 @@

82.19%

(Some assign, sym) let select_i32 (i : Symbolic_value.int32) = - let sym_int = Expr.simplify i in - match Expr.view sym_int with - | Val (Num (I32 i)) -> return i + let sym_int = Expr.simplify i in + match 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 i = + let* possible_value = get_model_or_stop symbol in + let i = match possible_value with - | Num (I32 i) -> i + | Num (I32 i) -> i | _ -> failwith "Unreachable: found symbol must be a value" in - let this_value_cond = Expr.Bitv.I32.(Expr.mk_symbol symbol = v i) in + let this_value_cond = Expr.Bitv.I32.(Expr.mk_symbol symbol = v i) in let not_this_value_cond = (* != is **not** the physical equality here *) - Expr.Bitv.I32.(Expr.mk_symbol symbol != v i) + Expr.Bitv.I32.(Expr.mk_symbol symbol != 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 c in - if assertion_true then return () else assertion_fail c + let* assertion_true = select c in + if assertion_true then return () else assertion_fail c end diff --git a/coverage/src/symbolic/symbolic_global.ml.html b/coverage/src/symbolic/symbolic_global.ml.html index 12612e450..4b5cc27bc 100644 --- a/coverage/src/symbolic/symbolic_global.ml.html +++ b/coverage/src/symbolic/symbolic_global.ml.html @@ -171,7 +171,7 @@

97.44%

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

97.44%

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 = @@ -209,29 +209,29 @@

97.44%

{ 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 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.ml.html b/coverage/src/symbolic/symbolic_memory.ml.html index 50ed6b8e3..d4b25ae87 100644 --- a/coverage/src/symbolic/symbolic_memory.ml.html +++ b/coverage/src/symbolic/symbolic_memory.ml.html @@ -554,8 +554,8 @@

83.90%

} let i32 v = - match view v with - | Val (Num (I32 i)) -> i + match view v with + | Val (Num (I32 i)) -> i | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v let grow m delta = @@ -566,7 +566,7 @@

83.90%

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

83.90%

end let clone m = - { data = Hashtbl.create 16 + { data = Hashtbl.create 16 ; parent = Some m ; size = m.size - ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *) + ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *) } 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 -> make (Val (Num (I8 0))) - | Some parent -> load_byte parent a ) + | None -> make (Val (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 = Expr.ty e1 in - if m1 = m2 && Expr.equal e1 e2 then - if h - l = Ty.size ty then e1 else make (Extract (e1, h, l)) + let ty = Expr.ty e1 in + if m1 = m2 && Expr.equal e1 e2 then + if h - l = Ty.size ty then e1 else make (Extract (e1, h, l)) else make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))) let concat ~msb ~lsb offset = - assert (offset > 0 && offset <= 8); - match (view msb, view lsb) with - | Val (Num (I8 i1)), Val (Num (I8 i2)) -> - 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 (view msb, view lsb) with + | Val (Num (I8 i1)), Val (Num (I8 i2)) -> + 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 - Value.const_i32 Int32.(logor (shl (of_int i1) (of_int offset)) i2) + 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 @@ -629,34 +629,34 @@

83.90%

| Val (Num (I8 i1)), Val (Num (I64 i2)) -> let offset = Int64.of_int (offset * 8) in 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) -> make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3)) | _ -> 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 load_8_s m a = - let v = loadn m (i32 a) 1 in - match view v with - | Val (Num (I8 i8)) -> Value.const_i32 (Int32.extend_s 8 (Int32.of_int i8)) - | _ -> cvtop (Ty_bitv 32) (Sign_extend 24) v + let v = loadn m (i32 a) 1 in + match view v with + | Val (Num (I8 i8)) -> Value.const_i32 (Int32.extend_s 8 (Int32.of_int i8)) + | _ -> cvtop (Ty_bitv 32) (Sign_extend 24) v let load_8_u m a = - let v = loadn m (i32 a) 1 in - match view v with - | Val (Num (I8 i)) -> Value.const_i32 (Int32.of_int i) - | _ -> cvtop (Ty_bitv 32) (Zero_extend 24) v + let v = loadn m (i32 a) 1 in + match view v with + | Val (Num (I8 i)) -> Value.const_i32 (Int32.of_int i) + | _ -> cvtop (Ty_bitv 32) (Zero_extend 24) v let load_16_s m a = let v = loadn m (i32 a) 2 in @@ -670,14 +670,14 @@

83.90%

| Val (Num (I32 _)) -> v | _ -> cvtop (Ty_bitv 32) (Zero_extend 16) v -let load_32 m a = loadn m (i32 a) 4 +let load_32 m a = loadn m (i32 a) 4 let load_64 m a = loadn m (i32 a) 8 let extract v pos = - match view v with - | Val (Num (I32 i)) -> - let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in + match view v with + | Val (Num (I32 i)) -> + let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in value (Num (I8 i')) | Val (Num (I64 i)) -> let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in @@ -686,67 +686,67 @@

83.90%

| Cvtop (_, Sign_extend 24, ({ node = Symbol _; _ } as sym)) when ty sym = Ty_bitv 8 -> sym - | _ -> make (Extract (v, pos + 1, pos)) + | _ -> make (Extract (v, pos + 1, pos)) let storen m ~addr v n = - let a0 = i32 addr in - for i = 0 to n - 1 do - let addr' = Int32.add a0 (Int32.of_int i) in - let v' = extract v i in - Hashtbl.replace m.data addr' v' + let a0 = i32 addr in + for i = 0 to n - 1 do + let addr' = Int32.add a0 (Int32.of_int i) in + let v' = extract v i in + Hashtbl.replace m.data addr' v' done -let store_8 m ~addr v = storen m ~addr v 1 +let store_8 m ~addr v = storen m ~addr v 1 let store_16 m ~addr v = storen m ~addr v 2 -let store_32 m ~addr v = storen m ~addr v 4 +let store_32 m ~addr v = storen m ~addr v 4 let store_64 m ~addr v = storen m ~addr v 8 let get_limit_max _m = None (* TODO *) let check_within_bounds m a = - match view a with - | Val (Num (I32 _)) -> Ok (Value.Bool.const false, a) - | Ptr (base, offset) -> ( + match view a with + | Val (Num (I32 _)) -> Ok (Value.Bool.const false, a) + | Ptr (base, offset) -> ( match Hashtbl.find m.chunks base with | exception Not_found -> Error Trap.Memory_leak_use_after_free - | size -> - let ptr = Int32.add base (i32 offset) in - let upper_bound = - Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size)) + | size -> + let ptr = Int32.add base (i32 offset) in + let upper_bound = + Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size)) in - Ok (Value.Bool.(or_ (const (ptr < base)) upper_bound), Value.const_i32 ptr) + Ok (Value.Bool.(or_ (const (ptr < base)) upper_bound), Value.const_i32 ptr) ) | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a let free m base = - if not @@ Hashtbl.mem m.chunks base then failwith "Memory leak double free"; - Hashtbl.remove m.chunks base + if not @@ Hashtbl.mem m.chunks base then failwith "Memory leak double free"; + Hashtbl.remove m.chunks base -let replace_size m base size = Hashtbl.replace m.chunks base size +let replace_size m base size = Hashtbl.replace m.chunks base size 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 let init () = Env_id.Tbl.create 0 -let iter f collection = Env_id.Tbl.iter (fun _ tbl -> f tbl) collection +let iter f collection = Env_id.Tbl.iter (fun _ tbl -> f tbl) collection 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 = @@ -754,17 +754,17 @@

83.90%

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 19bdf0bcb..ad6680c1c 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 38a327e2c..effebf02a 100644 --- a/coverage/src/symbolic/symbolic_value.ml.html +++ b/coverage/src/symbolic/symbolic_value.ml.html @@ -965,7 +965,7 @@

85.12%

| 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)) @@ -996,8 +996,8 @@

85.12%

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 @@ -1012,22 +1012,22 @@

85.12%

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 @@ -1037,7 +1037,7 @@

85.12%

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 @@ -1045,81 +1045,81 @@

85.12%

(* 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 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 let unsigned_div e1 e2 = binop ty DivU e1 e2 - let rem e1 e2 = binop ty Rem e1 e2 + let rem e1 e2 = binop ty Rem 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) - | _ -> binop ty And e1 e2 + 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 = match (boolify e1, boolify e2) with | Some b1, Some b2 -> Bool.int32 (Bool.or_ b1 b2) | _ -> binop ty Or e1 e2 - let logxor e1 e2 = binop ty Xor e1 e2 + 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 e1 == e2 then Bool.const true else relop Ty_bool Eq e1 e2 + let eq e1 e2 = if e1 == e2 then Bool.const true else relop Ty_bool Eq e1 e2 - let ne e1 e2 = if e1 == e2 then Bool.const false else relop Ty_bool Ne e1 e2 + let ne e1 e2 = if e1 == e2 then Bool.const false else relop Ty_bool Ne e1 e2 - let lt e1 e2 = if e1 == e2 then Bool.const false else relop ty Lt e1 e2 + let lt e1 e2 = if e1 == e2 then Bool.const false else relop ty Lt e1 e2 - let gt e1 e2 = if e1 == e2 then Bool.const false else relop ty Gt e1 e2 + let gt e1 e2 = if e1 == e2 then Bool.const false else relop ty Gt e1 e2 - let lt_u e1 e2 = if e1 == e2 then Bool.const false else relop ty LtU e1 e2 + let lt_u e1 e2 = if e1 == e2 then Bool.const false else relop ty LtU e1 e2 let gt_u e1 e2 = if e1 == e2 then Bool.const false else relop ty GtU e1 e2 - let le e1 e2 = if e1 == e2 then Bool.const true else relop ty Le e1 e2 + let le e1 e2 = if e1 == e2 then Bool.const true else relop ty Le e1 e2 - let ge e1 e2 = if e1 == e2 then Bool.const true else relop ty Ge e1 e2 + let ge e1 e2 = if e1 == e2 then Bool.const true else relop ty Ge e1 e2 let le_u e1 e2 = if e1 == e2 then Bool.const true else relop ty LeU e1 e2 - let ge_u e1 e2 = if e1 == e2 then Bool.const true else relop ty GeU e1 e2 + let ge_u e1 e2 = if 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 - | Cvtop (_, OfBool, cond) -> cond - | _ -> make (Cvtop (ty, ToBool, e)) + match view e with + | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l + | Cvtop (_, OfBool, cond) -> cond + | _ -> make (Cvtop (ty, ToBool, e)) let trunc_f32_s x = cvtop ty TruncSF32 x diff --git a/coverage/src/utils/log.ml.html b/coverage/src/utils/log.ml.html index e2d7081d9..0333709ea 100644 --- a/coverage/src/utils/log.ml.html +++ b/coverage/src/utils/log.ml.html @@ -77,13 +77,13 @@

81.82%

let debug0 t : unit = if !debug_on then Format.pp_err t -let debug1 t a : unit = if !debug_on then Format.pp_err t a +let debug1 t a : unit = if !debug_on then Format.pp_err t a -let debug2 t a b : unit = if !debug_on then Format.pp_err t a b +let debug2 t a b : unit = if !debug_on then Format.pp_err t a b let debug5 t a b c d e : unit = if !debug_on then Format.pp_err t a b c d e -let profile3 t a b c : unit = if !profiling_on then Format.pp_err t a b c +let profile3 t a b c : unit = if !profiling_on then Format.pp_err t a b c let err f = Format.kasprintf failwith f diff --git a/coverage/src/utils/syntax.ml.html b/coverage/src/utils/syntax.ml.html index cf408e6ac..89d77f9e7 100644 --- a/coverage/src/utils/syntax.ml.html +++ b/coverage/src/utils/syntax.ml.html @@ -221,7 +221,7 @@

81.63%

open Stdlib.Result -let ( let* ) o f = match o with Ok v -> f v | Error _ as e -> e +let ( let* ) o f = match o with Ok v -> f v | Error _ as e -> e let ( let+ ) o f = match o with Ok v -> Ok (f v) | Error _ as e -> e