Skip to content

Commit

Permalink
upgrade ocamlformat version and fmt
Browse files Browse the repository at this point in the history
  • Loading branch information
zapashcanon committed Dec 4, 2024
1 parent e8ccef1 commit c534856
Show file tree
Hide file tree
Showing 27 changed files with 163 additions and 158 deletions.
2 changes: 1 addition & 1 deletion .ocamlformat
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
version=0.26.2
version=0.27.0
assignment-operator=end-line
break-cases=fit
break-fun-decl=wrap
Expand Down
2 changes: 1 addition & 1 deletion bench/report/pie_results.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
14 changes: 7 additions & 7 deletions bench/report/runs.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
11 changes: 6 additions & 5 deletions bench/report/time_distribution.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions example/define_host_function/life_game/runweb.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
3 changes: 2 additions & 1 deletion src/annot/contract.ml
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,8 @@ let pp_contract fmt { funcid; preconditions; postconditions } =
Preconditions:@;\
<1 2>@[<v>%a@]@,\
Postconditions:@;\
<1 2>@[<v>%a@]@]" pp_indice funcid
<1 2>@[<v>%a@]@]"
pp_indice funcid
(list ~sep:pp_newline pp_prop)
preconditions
(list ~sep:pp_newline pp_prop)
Expand Down
14 changes: 7 additions & 7 deletions src/ast/binary_encoder.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/ast/code_generator.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
14 changes: 7 additions & 7 deletions src/cmd/cmd_c.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/cmd/cmd_conc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
6 changes: 3 additions & 3 deletions src/cmd/cmd_sym.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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) ->
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/cmd/cmd_utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions src/concolic/concolic_choice.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 }))
Expand Down
108 changes: 54 additions & 54 deletions src/concolic/concolic_wasm_ffi.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 ???? *)
Expand Down
2 changes: 1 addition & 1 deletion src/data_structures/named.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 )
10 changes: 5 additions & 5 deletions src/interpret/interpret.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 ->
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/primitives/int64.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading

0 comments on commit c534856

Please sign in to comment.