From c534856dbf8c04107d8fa02a9fee2a3a6a655c19 Mon Sep 17 00:00:00 2001 From: zapashcanon Date: Wed, 4 Dec 2024 12:06:22 +0100 Subject: [PATCH] upgrade ocamlformat version and fmt --- .ocamlformat | 2 +- bench/report/pie_results.ml | 2 +- bench/report/runs.ml | 14 +-- bench/report/time_distribution.ml | 11 +- .../define_host_function/life_game/runweb.ml | 6 +- src/annot/contract.ml | 3 +- src/ast/binary_encoder.ml | 14 +-- src/ast/code_generator.ml | 4 +- src/cmd/cmd_c.ml | 14 +-- src/cmd/cmd_conc.ml | 2 +- src/cmd/cmd_sym.ml | 6 +- src/cmd/cmd_utils.ml | 4 +- src/concolic/concolic_choice.ml | 3 +- src/concolic/concolic_wasm_ffi.ml | 108 +++++++++--------- src/data_structures/named.ml | 2 +- src/interpret/interpret.ml | 10 +- src/primitives/int64.ml | 4 +- src/symbolic/symbolic.ml | 7 +- src/symbolic/symbolic_choice.ml | 26 ++--- src/symbolic/symbolic_wasm_ffi.ml | 4 +- src/text_to_binary/rewrite.ml | 7 +- src/utils/syntax.ml | 12 +- src/utils/tracing.ml | 2 +- src/validate/binary_validate.ml | 4 +- test/fuzz/basic.ml | 8 +- test/fuzz/fuzzer.ml | 14 +-- test/fuzz/interprets.ml | 28 ++--- 27 files changed, 163 insertions(+), 158 deletions(-) diff --git a/.ocamlformat b/.ocamlformat index f1462252f..c365faf03 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,4 +1,4 @@ -version=0.26.2 +version=0.27.0 assignment-operator=end-line break-cases=fit break-fun-decl=wrap diff --git a/bench/report/pie_results.ml b/bench/report/pie_results.ml index f53ac596a..8d72667d8 100644 --- a/bench/report/pie_results.ml +++ b/bench/report/pie_results.ml @@ -107,7 +107,7 @@ let make runs output_dir reference_name = , Format.sprintf "Nothing (%d)" count_nothing ) ] |> List.filter_map (fun ((count, _, _, _) as v) -> - if count = 0 then None else Some v ) + if count = 0 then None else Some v ) |> List.sort (fun (c1, _, _, _) (c2, _, _, _) -> compare c2 c1) |> List.map mk_value |> Cmd.of_list in diff --git a/bench/report/runs.ml b/bench/report/runs.ml index 56867b8a1..cfec01f47 100644 --- a/bench/report/runs.ml +++ b/bench/report/runs.ml @@ -83,11 +83,11 @@ let mean_stime runs = sum_stime runs /. (count_all runs |> float_of_int) let to_distribution ~max_time runs = List.init max_time (fun i -> - List.fold_left - (fun count r -> - let clock = Run.clock r |> int_of_float in - if clock = i then count +. 1. else count ) - 0. runs ) + List.fold_left + (fun count r -> + let clock = Run.clock r |> int_of_float in + if clock = i then count +. 1. else count ) + 0. runs ) let pp_quick_results fmt results = let nothing = ref 0 in @@ -118,8 +118,8 @@ let pp_table_results fmt results = Format.fprintf fmt "| Nothing | Reached | Timeout | Other | Killed | Total |@\n\ |:-------:|:-------:|:-------:|:-----:|:------:|:-----:|@\n\ - | %6i | %6i | %6i | %6i | %6i | %6i |" nothing reached timeout other killed - total + | %6i | %6i | %6i | %6i | %6i | %6i |" + nothing reached timeout other killed total let pp_table_statistics fmt results = let total = sum_clock results in diff --git a/bench/report/time_distribution.ml b/bench/report/time_distribution.ml index 643fbc67e..1924cb0a2 100644 --- a/bench/report/time_distribution.ml +++ b/bench/report/time_distribution.ml @@ -49,11 +49,12 @@ let make runs output_dir reference_name = let output = Gnuplot.Output.create (`Png - Fpath.( - output_dir - // v - (Format.sprintf "results_%s_time_distribution.png" reference_name) - |> to_string ) ) + Fpath.( + output_dir + // v + (Format.sprintf "results_%s_time_distribution.png" + reference_name ) + |> to_string ) ) in let range = Gnuplot.Range.X (min_time, float_of_int max_time) in diff --git a/example/define_host_function/life_game/runweb.ml b/example/define_host_function/life_game/runweb.ml index 028c2fcb4..c1e6b91dc 100644 --- a/example/define_host_function/life_game/runweb.ml +++ b/example/define_host_function/life_game/runweb.ml @@ -6,9 +6,9 @@ let asset_loader path = let () = let server = S.create ~port:8000 () in S.add_route_handler ~meth:`GET server S.Route.return (fun _req -> - S.Response.make_string - ~headers:[ ("Content-Type", "text/html") ] - (Ok (asset_loader "index.html")) ); + S.Response.make_string + ~headers:[ ("Content-Type", "text/html") ] + (Ok (asset_loader "index.html")) ); S.add_route_handler ~meth:`GET server S.Route.(exact "life_browser.js" @/ return) diff --git a/src/annot/contract.ml b/src/annot/contract.ml index 9a8b05878..0fb42c6d2 100644 --- a/src/annot/contract.ml +++ b/src/annot/contract.ml @@ -27,7 +27,8 @@ let pp_contract fmt { funcid; preconditions; postconditions } = Preconditions:@;\ <1 2>@[%a@]@,\ Postconditions:@;\ - <1 2>@[%a@]@]" pp_indice funcid + <1 2>@[%a@]@]" + pp_indice funcid (list ~sep:pp_newline pp_prop) preconditions (list ~sep:pp_newline pp_prop) diff --git a/src/ast/binary_encoder.ml b/src/ast/binary_encoder.ml index f029c525b..be4436a2a 100644 --- a/src/ast/binary_encoder.ml +++ b/src/ast/binary_encoder.ml @@ -663,8 +663,8 @@ let encode_imports buf (funcs, tables, memories, globals) = let encode_functions buf (funcs : binary func list) = let idx = ref 0 in encode_vector_list buf funcs (fun buf func -> - write_block_type_idx buf func.type_f; - incr idx ) + write_block_type_idx buf func.type_f; + incr idx ) (* table: section 4 *) let encode_tables buf tables = encode_vector_list buf tables write_table @@ -707,11 +707,11 @@ let encode_datacount buf datas = (* code: section 10 *) let encode_codes buf funcs = encode_vector_list buf funcs (fun buf { locals; body; _ } -> - let code_buf = Buffer.create 16 in - write_locals code_buf locals; - write_expr code_buf body ~end_op_code:None; - write_u32_of_int buf (Buffer.length code_buf); - Buffer.add_buffer buf code_buf ) + let code_buf = Buffer.create 16 in + write_locals code_buf locals; + write_expr code_buf body ~end_op_code:None; + write_u32_of_int buf (Buffer.length code_buf); + Buffer.add_buffer buf code_buf ) (* data: section 11 *) let encode_datas buf datas = encode_vector_array buf datas write_data diff --git a/src/ast/code_generator.ml b/src/ast/code_generator.ml index b2c3ade79..73beb18f5 100644 --- a/src/ast/code_generator.ml +++ b/src/ast/code_generator.ml @@ -573,11 +573,11 @@ let contract_generate (owi_funcs : (string * int) array) (m : modul) List.init (Array.length tenv.param_types) (fun i -> Local_get (Raw i)) @ [ Call (Raw old_index) ] @ List.init (Array.length tenv.result_types) (fun i -> - Local_set (tenv.result i) ) + Local_set (tenv.result i) ) in let return = List.init (Array.length tenv.result_types) (fun i -> - Local_get (tenv.result i) ) + Local_get (tenv.result i) ) in let* tenv, precond_checker = diff --git a/src/cmd/cmd_c.ml b/src/cmd/cmd_c.ml index 3c71a72d4..1e16b0244 100644 --- a/src/cmd/cmd_c.ml +++ b/src/cmd/cmd_c.ml @@ -80,10 +80,10 @@ let eacsl_instrument eacsl debug ~includes (files : Fpath.t list) : | Error (`Msg e) -> Error (`Msg - (Fmt.str "Frama-C failed: %s" - ( if debug then e - else "run with --debug to get the full error message" ) ) - ) ) + (Fmt.str "Frama-C failed: %s" + ( if debug then e + else "run with --debug to get the full error message" ) ) + ) ) (List.combine files outs) in @@ -128,9 +128,9 @@ let compile ~includes ~opt_lvl debug (files : Fpath.t list) : Fpath.t Result.t = | Error (`Msg e) -> Error (`Msg - (Fmt.str "Clang failed: %s" - ( if debug then e - else "run with --debug to get the full error message" ) ) ) + (Fmt.str "Clang failed: %s" + ( if debug then e + else "run with --debug to get the full error message" ) ) ) in out diff --git a/src/cmd/cmd_conc.ml b/src/cmd/cmd_conc.ml index f8f08284e..45b51a244 100644 --- a/src/cmd/cmd_conc.ml +++ b/src/cmd/cmd_conc.ml @@ -14,7 +14,7 @@ let print_paths = false let ( let** ) (t : 'a Result.t Choice.t) (f : 'a -> 'b Result.t Choice.t) : 'b Result.t Choice.t = Choice.bind t (fun t -> - match t with Error e -> Choice.return (Error e) | Ok x -> f x ) + match t with Error e -> Choice.return (Error e) | Ok x -> f x ) let simplify_then_link ~unsafe ~rac ~srac ~optimize link_state m = let* m = diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml index fa489f929..4a6021ba8 100644 --- a/src/cmd/cmd_sym.ml +++ b/src/cmd/cmd_sym.ml @@ -40,7 +40,7 @@ let run_file ~unsafe ~rac ~srac ~optimize pc filename = let m = Symbolic.convert_module_to_run m in let c = Interpret.SymbolicP.modul link_state.envs m in Choice.bind pc (fun r -> - match r with Error _ -> Choice.return r | Ok () -> c ) + match r with Error _ -> Choice.return r | Ok () -> c ) (* NB: This function propagates potential errors (Result.err) occurring during evaluation (OS, syntax error, etc.), except for Trap and Assert, @@ -80,7 +80,7 @@ let cmd ~profiling ~debug ~unsafe ~rac ~srac ~optimize ~workers in let results = Wq.read_as_seq res_queue ~finalizer:(fun () -> - Array.iter Domain.join join_handles ) + Array.iter Domain.join join_handles ) in let print_bug = function | `ETrap (tr, model) -> @@ -123,7 +123,7 @@ let cmd ~profiling ~debug ~unsafe ~rac ~srac ~optimize ~workers (x, List.rev @@ Thread_with_memory.breadcrumbs thread) ) |> List.of_seq |> List.sort (fun (_, bc1) (_, bc2) -> - List.compare Prelude.Int32.compare bc1 bc2 ) + List.compare Prelude.Int32.compare bc1 bc2 ) |> List.to_seq |> Seq.map fst else results in diff --git a/src/cmd/cmd_utils.ml b/src/cmd/cmd_utils.ml index 9f03d6f6b..bcce9c3c4 100644 --- a/src/cmd/cmd_utils.ml +++ b/src/cmd/cmd_utils.ml @@ -62,8 +62,8 @@ let add_main_as_start (m : Binary.modul) = | Ref_type (Types.No_null, t) -> Error (`Msg - (Fmt.str "can not create default value of type %a" - Types.pp_heap_type t ) ) + (Fmt.str "can not create default value of type %a" + Types.pp_heap_type t ) ) in let+ body = let pt, rt = snd main_type in diff --git a/src/concolic/concolic_choice.ml b/src/concolic/concolic_choice.ml index a57afbc2f..22e41077b 100644 --- a/src/concolic/concolic_choice.ml +++ b/src/concolic/concolic_choice.ml @@ -91,8 +91,7 @@ let ( let+ ) = map let abort = M (fun st -> - (Ok (), { st with pc = Assume (Symbolic_value.Bool.const false) :: st.pc }) - ) + (Ok (), { st with pc = Assume (Symbolic_value.Bool.const false) :: st.pc }) ) let add_pc (c : Concolic_value.V.vbool) = M (fun st -> (Ok (), { st with pc = Assume c.symbolic :: st.pc })) diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml index 289aaaf8f..b38792bc9 100644 --- a/src/concolic/concolic_wasm_ffi.ml +++ b/src/concolic/concolic_wasm_ffi.ml @@ -20,71 +20,71 @@ module M : let symbol_i32 () : Value.int32 Choice.t = Choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value -> - let n = - match forced_value with - | None -> Random.bits32 () - | Some (Num (I32 n)) -> n - | _ -> assert false - in - (I32 n, Value.pair n (Expr.symbol sym)) ) + let n = + match forced_value with + | None -> Random.bits32 () + | Some (Num (I32 n)) -> n + | _ -> assert false + in + (I32 n, Value.pair n (Expr.symbol sym)) ) let symbol_i8 () : Value.int32 Choice.t = Choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value -> - let n = - match forced_value with - | None -> Int32.logand 0xFFl (Random.bits32 ()) - | Some (Num (I32 n)) -> n - | _ -> assert false - in - let sym_expr = - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) - in - (I32 n, Value.pair n sym_expr) ) + let n = + match forced_value with + | None -> Int32.logand 0xFFl (Random.bits32 ()) + | Some (Num (I32 n)) -> n + | _ -> assert false + in + let sym_expr = + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) + in + (I32 n, Value.pair n sym_expr) ) let symbol_char () : Value.int32 Choice.t = Choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value -> - let n = - match forced_value with - | None -> Int32.logand 0xFFl (Random.bits32 ()) - | Some (Num (I32 n)) -> n - | _ -> assert false - in - let sym_expr = - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) - in - (I32 n, Value.pair n sym_expr) ) + let n = + match forced_value with + | None -> Int32.logand 0xFFl (Random.bits32 ()) + | Some (Num (I32 n)) -> n + | _ -> assert false + in + let sym_expr = + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) + in + (I32 n, Value.pair n sym_expr) ) let symbol_i64 () : Value.int64 Choice.t = Choice.with_new_symbol (Ty_bitv 64) (fun sym forced_value -> - let n = - match forced_value with - | None -> Random.bits64 () - | Some (Num (I64 n)) -> n - | _ -> assert false - in - (I64 n, Value.pair n (Expr.symbol sym)) ) + let n = + match forced_value with + | None -> Random.bits64 () + | Some (Num (I64 n)) -> n + | _ -> assert false + in + (I64 n, Value.pair n (Expr.symbol sym)) ) let symbol_f32 () : Value.float32 Choice.t = Choice.with_new_symbol (Ty_fp 32) (fun sym forced_value -> - let n = - match forced_value with - | None -> Random.bits32 () - | Some (Num (F32 n)) -> n - | _ -> assert false - in - let n = Float32.of_bits n in - (F32 n, Value.pair n (Expr.symbol sym)) ) + let n = + match forced_value with + | None -> Random.bits32 () + | Some (Num (F32 n)) -> n + | _ -> assert false + in + let n = Float32.of_bits n in + (F32 n, Value.pair n (Expr.symbol sym)) ) let symbol_f64 () : Value.float64 Choice.t = Choice.with_new_symbol (Ty_fp 64) (fun sym forced_value -> - let n = - match forced_value with - | None -> Random.bits64 () - | Some (Num (F64 n)) -> n - | _ -> assert false - in - let n = Float64.of_bits n in - (F64 n, Value.pair n (Expr.symbol sym)) ) + let n = + match forced_value with + | None -> Random.bits64 () + | Some (Num (F64 n)) -> n + | _ -> assert false + in + let n = Float64.of_bits n in + (F64 n, Value.pair n (Expr.symbol sym)) ) let assume_i32 (i : Value.int32) : unit Choice.t = let c = Value.I32.to_bool i in @@ -127,10 +127,10 @@ module M : let alloc _ (base : Value.int32) (_size : Value.int32) : Value.int32 Choice.t = Choice.bind (i32 base) (fun (base : int32) -> - Choice.return - { Concolic_value.concrete = base - ; symbolic = Expr.ptr base (Symbolic_value.const_i32 0l) - } ) + Choice.return + { Concolic_value.concrete = base + ; symbolic = Expr.ptr base (Symbolic_value.const_i32 0l) + } ) let free _ (p : Value.int32) = (* WHAT ???? *) diff --git a/src/data_structures/named.ml b/src/data_structures/named.ml index 0a1b9b988..50e30fb10 100644 --- a/src/data_structures/named.ml +++ b/src/data_structures/named.ml @@ -28,4 +28,4 @@ let to_array v = if Hashtbl.mem tbl i then assert false else Hashtbl.add tbl i v ) v.values; Array.init (List.length v.values) (fun i -> - match Hashtbl.find_opt tbl i with None -> assert false | Some v -> v ) + match Hashtbl.find_opt tbl i with None -> assert false | Some v -> v ) diff --git a/src/interpret/interpret.ml b/src/interpret/interpret.ml index 7cb8efe6d..54bdd8a26 100644 --- a/src/interpret/interpret.ml +++ b/src/interpret/interpret.ml @@ -501,8 +501,8 @@ module Make (P : Interpret_intf.P) : | Type_mismatch -> Choice.trap Trap.Extern_call_arg_type_mismatch | Null -> Choice.trap Trap.Extern_call_null_arg ) in - let rec split_args : - type f r. Stack.t -> (f, r) Extern_func.atype -> Stack.t * Stack.t = + 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 @@ -516,8 +516,8 @@ module Make (P : Interpret_intf.P) : | NArg (_, _, args) -> split_one_arg args | Res -> ([], stack) in - let rec apply : - type f r. Stack.t -> (f, r) Extern_func.atype -> f -> r Choice.t = + let rec apply : type f r. + Stack.t -> (f, r) Extern_func.atype -> f -> r Choice.t = fun stack ty f -> match ty with | Mem args -> @@ -635,7 +635,7 @@ module Make (P : Interpret_intf.P) : List.sort (fun ((Raw id1 : binary indice), _) ((Raw id2 : binary indice), _) -> - compare id1 id2 ) + compare id1 id2 ) @@ List.of_seq @@ Hashtbl.to_seq tbl in match l with diff --git a/src/primitives/int64.ml b/src/primitives/int64.ml index e380a036f..b843e1c56 100644 --- a/src/primitives/int64.ml +++ b/src/primitives/int64.ml @@ -42,8 +42,8 @@ let popcnt = (x * h01) lsr 56 (* - * Unsigned comparison in terms of signed comparison. - *) + * Unsigned comparison in terms of signed comparison. + *) let cmp_u x op y = op (add x min_int) (add y min_int) let eq (x : int64) y = equal x y diff --git a/src/symbolic/symbolic.ml b/src/symbolic/symbolic.ml index aab9ecc96..29ee747ae 100644 --- a/src/symbolic/symbolic.ml +++ b/src/symbolic/symbolic.ml @@ -5,9 +5,10 @@ module MakeP (Memory : Symbolic_memory_intf.S) (Thread : Thread.S with type Memory.collection = Memory.collection) - (Choice : Choice_intf.Complete - with module V := Symbolic_value - and type thread := Thread.t) = + (Choice : + Choice_intf.Complete + with module V := Symbolic_value + and type thread := Thread.t) = struct module Value = Symbolic_value module Choice = Choice diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 55e81ccf6..18217f6b4 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -102,15 +102,15 @@ module CoreImpl = struct let spawn_worker sched wls_init callback callback_init callback_close = callback_init (); Domain.spawn (fun () -> - Fun.protect - ~finally:(fun () -> callback_close ()) - (fun () -> - let wls = wls_init () in - try work wls sched callback - with e -> - let bt = Printexc.get_raw_backtrace () in - Wq.fail sched.work_queue; - Printexc.raise_with_backtrace e bt ) ) + Fun.protect + ~finally:(fun () -> callback_close ()) + (fun () -> + let wls = wls_init () in + try work wls sched callback + with e -> + let bt = Printexc.get_raw_backtrace () in + Wq.fail sched.work_queue; + Printexc.raise_with_backtrace e bt ) ) end module State = struct @@ -307,8 +307,8 @@ module CoreImpl = struct let sched = init_scheduler () in add_init_task sched (State.run t thread); Array.init workers (fun _i -> - spawn_worker sched (Solver.fresh solver) callback callback_init - callback_end ) + spawn_worker sched (Solver.fresh solver) callback callback_init + callback_end ) let trap t = let* thread in @@ -348,8 +348,8 @@ module Make (Thread : Thread.S) = struct let sym = Fmt.kstr (Smtml.Symbol.make ty) "symbol_%d" n in let+ () = modify_thread (fun thread -> - let thread = Thread.add_symbol thread sym in - Thread.incr_symbols thread ) + let thread = Thread.add_symbol thread sym in + Thread.incr_symbols thread ) in f sym diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index 26a047bc4..90b08c9e8 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -29,11 +29,11 @@ module M : let symbol_i8 () = Choice.with_new_symbol (Ty_bitv 8) (fun sym -> - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) let symbol_char () = Choice.with_new_symbol (Ty_bitv 8) (fun sym -> - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) let symbol_i32 () = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol diff --git a/src/text_to_binary/rewrite.ml b/src/text_to_binary/rewrite.ml index c8b871fce..373156a28 100644 --- a/src/text_to_binary/rewrite.ml +++ b/src/text_to_binary/rewrite.ml @@ -28,7 +28,9 @@ let find (named : 'a Named.t) : _ -> binary indice = function let get error (named : 'a Named.t) indice : 'a Indexed.t Result.t = let (Raw i) = find named indice in (* TODO change Named.t structure to make that sensible *) - match List.nth_opt named.values i with None -> Error error | Some v -> Ok v + match List.nth_opt named.values i with + | None -> Error error + | Some v -> Ok v let find_global (modul : Assigned.t) id : binary indice = find modul.global id @@ -92,8 +94,7 @@ let rewrite_expr (typemap : binary indice TypeMap.t) (modul : Assigned.t) | None -> Ok (locals, next_free_int + 1) | Some name -> if String_map.mem name locals then Error (`Duplicate_local name) - else Ok (String_map.add name next_free_int locals, next_free_int + 1) - ) + else Ok (String_map.add name next_free_int locals, next_free_int + 1) ) (String_map.empty, 0) locals in diff --git a/src/utils/syntax.ml b/src/utils/syntax.ml index 82ba5391c..bf5c822de 100644 --- a/src/utils/syntax.ml +++ b/src/utils/syntax.ml @@ -87,12 +87,12 @@ let array_map f a = try ok @@ Array.init (Array.length a) (fun i -> - let v = Array.get a i in - match f v with - | Error _e as e -> - err := Some e; - raise Exit - | Ok v -> v ) + let v = Array.get a i in + match f v with + | Error _e as e -> + err := Some e; + raise Exit + | Ok v -> v ) with Exit -> Option.get !err let array_fold_left f acc l = diff --git a/src/utils/tracing.ml b/src/utils/tracing.ml index 0c6b9fc4c..8ac2ff5b4 100644 --- a/src/utils/tracing.ml +++ b/src/utils/tracing.ml @@ -29,4 +29,4 @@ let model = let with_ev ev f = Runtime_events.User.write ev Runtime_events.Type.Begin; Fun.protect f ~finally:(fun () -> - Runtime_events.User.write ev Runtime_events.Type.End ) + Runtime_events.User.write ev Runtime_events.Type.End ) diff --git a/src/validate/binary_validate.ml b/src/validate/binary_validate.ml index 0c0505f1b..48b9ae1b7 100644 --- a/src/validate/binary_validate.ml +++ b/src/validate/binary_validate.ml @@ -560,8 +560,8 @@ and typecheck_expr env expr ~is_loop (block_type : binary block_type option) | None -> Error (`Type_mismatch - (Fmt.str "expected a prefix of %a but stack has type %a" Stack.pp pt - Stack.pp previous_stack ) ) + (Fmt.str "expected a prefix of %a but stack has type %a" Stack.pp pt + Stack.pp previous_stack ) ) | Some stack_to_push -> Stack.push rt stack_to_push let typecheck_function (modul : modul) func refs = diff --git a/test/fuzz/basic.ml b/test/fuzz/basic.ml index a2fcf0cc7..7cb2247c5 100644 --- a/test/fuzz/basic.ml +++ b/test/fuzz/basic.ml @@ -21,7 +21,10 @@ let heap_type : text heap_type Crowbar.gen = const Func_ht let ref_type = pair nullable heap_type let limits = - let sup = if true then 10 else 100000 (* TODO: fix max size ? *) in + let sup = + if true then 10 else 100000 + (* TODO: fix max size ? *) + in let* min = range sup in let+ max = option (range ~min (sup - min)) in { min; max } @@ -288,8 +291,7 @@ let global ntyp env = let globals = Env.get_globals ntyp env ~only_mut:false in List.map (fun (name, (_, _)) -> - pair (const (Global_get (Text name))) (const [ S.Push (Num_type ntyp) ]) - ) + pair (const (Global_get (Text name))) (const [ S.Push (Num_type ntyp) ]) ) globals let global_i32 env = global I32 env diff --git a/test/fuzz/fuzzer.ml b/test/fuzz/fuzzer.ml index fb16dec53..9b38e360a 100644 --- a/test/fuzz/fuzzer.ml +++ b/test/fuzz/fuzzer.ml @@ -74,13 +74,13 @@ let check (module I1 : Interprets.INTERPRET) (module I2 : Interprets.INTERPRET) let add_test name gen (module I1 : Interprets.INTERPRET) (module I2 : Interprets.INTERPRET) = Crowbar.add_test ~name [ gen ] (fun m -> - incr global_count; - if Param.debug then Fmt.epr "%a@\n" Owi.Text.pp_modul m; - Fmt.epr "test module %d [got %d timeouts...]@\n@[" !global_count - !timeout_count; - Fmt.flush Fmt.stderr (); - Crowbar.check (check (module I1) (module I2) m); - Fmt.epr "@]" ) + incr global_count; + if Param.debug then Fmt.epr "%a@\n" Owi.Text.pp_modul m; + Fmt.epr "test module %d [got %d timeouts...]@\n@[" !global_count + !timeout_count; + Fmt.flush Fmt.stderr (); + Crowbar.check (check (module I1) (module I2) m); + Fmt.epr "@]" ) let gen (conf : Env.conf) = Crowbar.with_printer Owi.Text.pp_modul (Gen.modul conf) diff --git a/test/fuzz/interprets.ml b/test/fuzz/interprets.ml index 06174cfcb..053199670 100644 --- a/test/fuzz/interprets.ml +++ b/test/fuzz/interprets.ml @@ -27,8 +27,8 @@ let set = let timeout_call_run (run : unit -> unit Result.t) : 'a Result.t = try Fun.protect ~finally:unset (fun () -> - set (); - try run () with Timeout -> Error `Timeout ) + set (); + try run () with Timeout -> Error `Timeout ) with Timeout -> Error `Timeout module Owi_unoptimized : INTERPRET = struct @@ -45,7 +45,7 @@ module Owi_unoptimized : INTERPRET = struct Link.modul Link.empty_state ~name:None simplified in timeout_call_run (fun () -> - Interpret.Concrete.modul link_state.envs regular ) + Interpret.Concrete.modul link_state.envs regular ) let name = "owi" end @@ -65,7 +65,7 @@ module Owi_optimized : INTERPRET = struct Link.modul Link.empty_state ~name:None simplified in timeout_call_run (fun () -> - Interpret.Concrete.modul link_state.envs regular ) + Interpret.Concrete.modul link_state.envs regular ) let name = "owi+optimize" end @@ -87,16 +87,16 @@ module Owi_symbolic : INTERPRET = struct in let regular = Symbolic.convert_module_to_run_minimalist regular in timeout_call_run (fun () -> - let c = Interpret.SymbolicM.modul link_state.envs regular in - let init_thread = Thread_with_memory.init () in - let res, _ = - Symbolic_choice_minimalist.run ~workers:dummy_workers_count - Smtml.Solver_dispatcher.Z3_solver c init_thread - in - match res with - | Ok res -> res - | Error (Trap t) -> Error (`Trap t) - | Error Assert_fail -> Error `Assert_failure ) + let c = Interpret.SymbolicM.modul link_state.envs regular in + let init_thread = Thread_with_memory.init () in + let res, _ = + Symbolic_choice_minimalist.run ~workers:dummy_workers_count + Smtml.Solver_dispatcher.Z3_solver c init_thread + in + match res with + | Ok res -> res + | Error (Trap t) -> Error (`Trap t) + | Error Assert_fail -> Error `Assert_failure ) let name = "owi_symbolic" end