From 1635c1cf9660a10bab8fbf4454c627e046d4eb8e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 7 Jun 2020 04:59:33 -0700 Subject: [PATCH] [sledge] Style: Change to less compact ocamlformat style Reviewed By: ngorogiannis Differential Revision: D21720967 fbshipit-source-id: b5794938c --- sledge/.ocamlformat | 3 +++ sledge/bin/domain_itv.ml | 28 ++++++++++++++----- sledge/bin/frontend.ml | 5 +++- sledge/bin/sledge_buck.ml | 25 ++++++++++++----- sledge/bin/sledge_cli.ml | 3 ++- sledge/src/control.ml | 4 ++- sledge/src/domain_used_globals.ml | 25 +++++++++++++---- sledge/src/equality.ml | 6 +++-- sledge/src/equality_test.ml | 19 +++++++++---- sledge/src/exec.ml | 6 +++-- sledge/src/import/import.ml | 17 ++++++++---- sledge/src/import/import0.ml | 15 ++++++++--- sledge/src/llair.ml | 3 ++- sledge/src/sh.ml | 45 +++++++++++++++++++++++-------- sledge/src/solver.ml | 10 +++++-- sledge/src/term.ml | 18 ++++++++++--- sledge/src/term_test.ml | 4 ++- 17 files changed, 180 insertions(+), 56 deletions(-) diff --git a/sledge/.ocamlformat b/sledge/.ocamlformat index e6ef8fdec..f1e2c374e 100644 --- a/sledge/.ocamlformat +++ b/sledge/.ocamlformat @@ -1,5 +1,8 @@ profile = compact break-before-in = fit-or-vertical +break-collection-expressions = fit-or-vertical +break-infix = fit-or-vertical +break-sequences = true margin = 76 parse-docstrings = true wrap-comments = true diff --git a/sledge/bin/domain_itv.ml b/sledge/bin/domain_itv.ml index 34800b695..9372fc2ce 100644 --- a/sledge/bin/domain_itv.ml +++ b/sledge/bin/domain_itv.ml @@ -33,7 +33,8 @@ let sexp_of_t (itv : t) = let sexps = Array.fold (bindings itv) ~init:[] ~f:(fun acc (v, {inf; sup}) -> Sexp.List - [ Sexp.Atom (Var.to_string v); Sexp.Atom (Scalar.to_string inf) + [ Sexp.Atom (Var.to_string v) + ; Sexp.Atom (Scalar.to_string inf) ; Sexp.Atom (Scalar.to_string sup) ] :: acc ) in @@ -239,11 +240,26 @@ let exec_intrinsic ~skip_throw:_ pre aret i _ = let name = Reg.name i in if List.exists - [ "malloc"; "aligned_alloc"; "calloc"; "posix_memalign"; "realloc" - ; "mallocx"; "rallocx"; "xallocx"; "sallocx"; "dallocx"; "sdallocx" - ; "nallocx"; "malloc_usable_size"; "mallctl"; "mallctlnametomib" - ; "mallctlbymib"; "malloc_stats_print"; "strlen" - ; "__cxa_allocate_exception"; "_ZN5folly13usingJEMallocEv" ] + [ "malloc" + ; "aligned_alloc" + ; "calloc" + ; "posix_memalign" + ; "realloc" + ; "mallocx" + ; "rallocx" + ; "xallocx" + ; "sallocx" + ; "dallocx" + ; "sdallocx" + ; "nallocx" + ; "malloc_usable_size" + ; "mallctl" + ; "mallctlnametomib" + ; "mallctlbymib" + ; "malloc_stats_print" + ; "strlen" + ; "__cxa_allocate_exception" + ; "_ZN5folly13usingJEMallocEv" ] ~f:(String.equal name) then Option.map ~f:(Option.some << exec_kill pre) aret else None diff --git a/sledge/bin/frontend.ml b/sledge/bin/frontend.ml index c874cf146..0e308ab17 100644 --- a/sledge/bin/frontend.ml +++ b/sledge/bin/frontend.ml @@ -21,7 +21,10 @@ Reg.demangle := let cxa_demangle = (* char *__cxa_demangle(const char *, char *, size_t *, int * ) *) Foreign.foreign "__cxa_demangle" - ( string @-> ptr char @-> ptr size_t @-> ptr int + ( string + @-> ptr char + @-> ptr size_t + @-> ptr int @-> returning string_opt ) in let null_ptr_char = from_voidp char null in diff --git a/sledge/bin/sledge_buck.ml b/sledge/bin/sledge_buck.ml index 26ed884e6..3321563af 100644 --- a/sledge/bin/sledge_buck.ml +++ b/sledge/bin/sledge_buck.ml @@ -38,7 +38,10 @@ let buck_build ~context target = let open Process in eval ~context (run "buck" - [ "build"; "@mode/" ^ Lazy.force mode; "-c"; "sledge.build=True" + [ "build" + ; "@mode/" ^ Lazy.force mode + ; "-c" + ; "sledge.build=True" ; target ]) (* split a fully-qualified buck target into file and rule *) @@ -151,19 +154,29 @@ let llvm_link_opt ~fuzzer ~bitcode_output modules = |- run (Lazy.force llvm_bin ^ "llvm-link") ("-o=-" :: modules) |- run (Lazy.force llvm_bin ^ "opt") - [ "-o=" ^ bitcode_output; "-internalize" + [ "-o=" ^ bitcode_output + ; "-internalize" ; "-internalize-public-api-list=" ^ String.concat ~sep:"," (Config.find_list "entry-points") - ; "-globaldce"; "-globalopt"; "-mergefunc"; "-constmerge" - ; "-argpromotion"; "-ipsccp"; "-mem2reg"; "-dce"; "-globaldce" - ; "-deadargelim"; "-global-merge-on-const" + ; "-globaldce" + ; "-globalopt" + ; "-mergefunc" + ; "-constmerge" + ; "-argpromotion" + ; "-ipsccp" + ; "-mem2reg" + ; "-dce" + ; "-globaldce" + ; "-deadargelim" + ; "-global-merge-on-const" ; "-global-merge-ignore-single-use=false" ; "-global-merge-group-by-use=false" (* global-merge-max-offset is set to 0 by default. If a global variable has larger allocation size than the max-offset, it is not merged, therefore the global-merge pass is a noop. We set it to something big, so that it merges as much as possible. *) - ; "-global-merge-max-offset=1000000"; "-global-merge" ] ) + ; "-global-merge-max-offset=1000000" + ; "-global-merge" ] ) (** command line interface *) diff --git a/sledge/bin/sledge_cli.ml b/sledge/bin/sledge_cli.ml index 92a777d73..8d5495914 100644 --- a/sledge/bin/sledge_cli.ml +++ b/sledge/bin/sledge_cli.ml @@ -242,5 +242,6 @@ let readme () = Command.run ~version:Version.version ~build_info:Version.build_info (Command.group ~summary ~readme ~preserve_subcommand_order:() [ ("buck", Sledge_buck.main ~command ~analyze:(translate >*> analyze)) - ; ("llvm", llvm_grp); ("analyze", analyze_cmd) + ; ("llvm", llvm_grp) + ; ("analyze", analyze_cmd) ; ("disassemble", disassemble_cmd) ]) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 83cce7404..e3124b198 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -246,7 +246,9 @@ module Make (Dom : Domain_intf.Dom) = struct | _ -> [%Trace.info "done: %a" Edge.pp edge] ; run ~f (pq, ws, bnd) ) - | None -> [%Trace.info "queue empty"] ; () + | None -> + [%Trace.info "queue empty"] ; + () end let exec_jump stk state block Llair.{dst; retreating} = diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml index 54b99ed4f..085e3b5d8 100644 --- a/sledge/src/domain_used_globals.ml +++ b/sledge/src/domain_used_globals.ml @@ -51,11 +51,26 @@ let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals = let name = Reg.name intrinsic in if List.exists - [ "malloc"; "aligned_alloc"; "calloc"; "posix_memalign"; "realloc" - ; "mallocx"; "rallocx"; "xallocx"; "sallocx"; "dallocx"; "sdallocx" - ; "nallocx"; "malloc_usable_size"; "mallctl"; "mallctlnametomib" - ; "mallctlbymib"; "malloc_stats_print"; "strlen" - ; "__cxa_allocate_exception"; "_ZN5folly13usingJEMallocEv" ] + [ "malloc" + ; "aligned_alloc" + ; "calloc" + ; "posix_memalign" + ; "realloc" + ; "mallocx" + ; "rallocx" + ; "xallocx" + ; "sallocx" + ; "dallocx" + ; "sdallocx" + ; "nallocx" + ; "malloc_usable_size" + ; "mallctl" + ; "mallctlnametomib" + ; "mallctlbymib" + ; "malloc_stats_print" + ; "strlen" + ; "__cxa_allocate_exception" + ; "_ZN5folly13usingJEMallocEv" ] ~f:(String.equal name) then List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a) diff --git a/sledge/src/equality.ml b/sledge/src/equality.ml index f91b81ad2..191d12b43 100644 --- a/sledge/src/equality.ml +++ b/sledge/src/equality.ml @@ -144,7 +144,8 @@ end = struct let is_var_in xs e = Option.exists ~f:(Var.Set.mem xs) (Var.of_term e) in - ( is_var_in xs e || is_var_in xs f + ( is_var_in xs e + || is_var_in xs f || (uninterpreted e && Term.exists ~f:(is_var_in xs) e) || (uninterpreted f && Term.exists ~f:(is_var_in xs) f) ) $> fun b -> @@ -1035,7 +1036,8 @@ let solve_classes r (classes, subst, us) xs = else (classes, subst, us_xs) in (classes, subst, Var.Set.union us xs) - |> solve_classes_ |> solve_for_xs r us xs + |> solve_classes_ + |> solve_for_xs r us xs |> [%Trace.retn fun {pf} (classes', subst', _) -> pf "subst: @[%a@]@ classes: @[%a@]" Subst.pp_diff (subst, subst') diff --git a/sledge/src/equality_test.ml b/sledge/src/equality_test.ml index 18400e147..f42fba1dd 100644 --- a/sledge/src/equality_test.ml +++ b/sledge/src/equality_test.ml @@ -60,7 +60,8 @@ let%test_module _ = let%test _ = is_false f1 let%expect_test _ = - pp f1 ; [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}] + pp f1 ; + [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}] let%test _ = is_false (and_eq !1 !1 f1) @@ -103,9 +104,13 @@ let%test_module _ = let r0 = true_ let%expect_test _ = - pp r0 ; [%expect {| {sat= true; rep= [[-1 ↦ ]; [0 ↦ ]]} |}] + pp r0 ; + [%expect {| {sat= true; rep= [[-1 ↦ ]; [0 ↦ ]]} |}] + + let%expect_test _ = + pp_classes r0 ; + [%expect {||}] - let%expect_test _ = pp_classes r0 ; [%expect {||}] let%test _ = difference r0 (f x) (f x) |> Poly.equal (Some (Z.of_int 0)) let%test _ = difference r0 !4 !3 |> Poly.equal (Some (Z.of_int 1)) @@ -364,11 +369,15 @@ let%test_module _ = let r11 = of_eqs [(!16, z - x); (x + !8 - z, z - !16 + !8 - z)] - let%expect_test _ = pp_classes r11 ; [%expect {| (%z_7 + -16) = %x_5 |}] + let%expect_test _ = + pp_classes r11 ; + [%expect {| (%z_7 + -16) = %x_5 |}] let r12 = of_eqs [(!16, z - x); (x + !8 - z, z + !16 + !8 - z)] - let%expect_test _ = pp_classes r12 ; [%expect {| (%z_7 + -16) = %x_5 |}] + let%expect_test _ = + pp_classes r12 ; + [%expect {| (%z_7 + -16) = %x_5 |}] let r13 = of_eqs [(Term.eq x !2, y); (Term.dq x !2, z); (y, z)] diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index 453525f58..a40443b11 100644 --- a/sledge/src/exec.ml +++ b/sledge/src/exec.ml @@ -231,8 +231,10 @@ let memmov_up_spec us dst src len = {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} let memmov_specs us dst src len = - [ memmov_eq_spec us dst src len; memmov_dj_spec us dst src len - ; memmov_dn_spec us dst src len; memmov_up_spec us dst src len ] + [ memmov_eq_spec us dst src len + ; memmov_dj_spec us dst src len + ; memmov_dn_spec us dst src len + ; memmov_up_spec us dst src len ] (* { emp } * alloc r [n × l] diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml index 5d2371e5e..7fb219024 100644 --- a/sledge/src/import/import.ml +++ b/sledge/src/import/import.ml @@ -38,11 +38,15 @@ let checkf cnd fmt = else Format.ikfprintf (fun _ () -> true) Format.str_formatter fmt let check f x = - assert (f x ; true) ; + assert ( + f x ; + true ) ; x let violates f x = - assert (f x ; true) ; + assert ( + f x ; + true ) ; assert false (** Extensions *) @@ -59,8 +63,10 @@ module Invariant = struct Error.to_exn (Error.create_s (Sexp.List - [ Atom "invariant failed"; sexp_of_exn exn - ; Source_code_position.sexp_of_t here; sexp_of_t t ])) + [ Atom "invariant failed" + ; sexp_of_exn exn + ; Source_code_position.sexp_of_t here + ; sexp_of_t t ])) in Printexc.raise_with_backtrace exn bt ) ; true ) @@ -85,7 +91,8 @@ module Array = struct s := s' ; x' in - map_inplace a ~f ; !s + map_inplace a ~f ; + !s end module IArray = IArray diff --git a/sledge/src/import/import0.ml b/sledge/src/import/import0.ml index 807b93a42..07bf4018a 100644 --- a/sledge/src/import/import0.ml +++ b/sledge/src/import/import0.ml @@ -26,9 +26,18 @@ external ( != ) : 'a -> 'a -> bool = "%noteq" let ( >> ) f g x = g (f x) let ( << ) f g x = f (g x) -let ( $ ) f g x = f x ; g x -let ( $> ) x f = f x ; x -let ( <$ ) f x = f x ; x + +let ( $ ) f g x = + f x ; + g x + +let ( $> ) x f = + f x ; + x + +let ( <$ ) f x = + f x ; + x (** Pretty-printer for argument type. *) type 'a pp = Format.formatter -> 'a -> unit diff --git a/sledge/src/llair.ml b/sledge/src/llair.ml index a285692b3..c14a19b9e 100644 --- a/sledge/src/llair.ml +++ b/sledge/src/llair.ml @@ -554,7 +554,8 @@ let set_derived_metadata functions = | None -> (* conservatively assume all virtual calls are recursive *) call.recursive <- true ) ; - jump return ; Option.iter ~f:jump throw + jump return ; + Option.iter ~f:jump throw | Return _ | Throw _ | Unreachable -> () ) ; BlockQ.enqueue_back_exn tips_to_roots src () in diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 214b9b814..58466ec9b 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -46,7 +46,10 @@ let map_seg ~f h = let siz = f h.siz in let arr = f h.arr in if - loc == h.loc && bas == h.bas && len == h.len && siz == h.siz + loc == h.loc + && bas == h.bas + && len == h.len + && siz == h.siz && arr == h.arr then h else {loc; bas; len; siz; arr} @@ -315,7 +318,9 @@ let rec invariant q = List.iter djn ~f:(fun sjn -> assert (Var.Set.is_subset sjn.us ~of_:(Var.Set.union us xs)) ; invariant sjn ) ) - with exc -> [%Trace.info "%a" pp q] ; raise exc + with exc -> + [%Trace.info "%a" pp q] ; + raise exc (** Quantification and Vocabulary *) @@ -437,7 +442,9 @@ let and_cong cong q = | [[]] -> q | _ -> and_cong_ cong (extend_us (Equality.fv cong) q) ) |> - [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q] + [%Trace.retn fun {pf} q -> + pf "%a" pp q ; + invariant q] let star q1 q2 = [%Trace.call fun {pf} -> pf "(%a)@ (%a)" pp q1 pp q2] @@ -532,7 +539,9 @@ let rec pure (e : Term.t) = if Equality.is_false cong then false_ us else exists_fresh xs {emp with us; cong; pure= [e]} ) |> - [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q] + [%Trace.retn fun {pf} q -> + pf "%a" pp q ; + invariant q] let and_ e q = star (pure e) q @@ -543,7 +552,9 @@ let and_subst subst q = ~f:(fun ~key ~data -> and_ (Term.eq key data)) subst ~init:q |> - [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q] + [%Trace.retn fun {pf} q -> + pf "%a" pp q ; + invariant q] let subst sub q = [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q] @@ -646,14 +657,18 @@ let rec norm_ s q = let xs, cong = Equality.apply_subst (Var.Set.union q.us q.xs) s q.cong in exists_fresh xs {q with cong} |> - [%Trace.retn fun {pf} q' -> pf "%a" pp_raw q' ; invariant q'] + [%Trace.retn fun {pf} q' -> + pf "%a" pp_raw q' ; + invariant q'] let norm s q = [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Equality.Subst.pp s pp_raw q] ; (if Equality.Subst.is_empty s then q else norm_ s q) |> - [%Trace.retn fun {pf} q' -> pf "%a" pp_raw q' ; invariant q'] + [%Trace.retn fun {pf} q' -> + pf "%a" pp_raw q' ; + invariant q'] (** rename existentially quantified variables to avoid shadowing, and reduce quantifier scopes by sinking them as low as possible into disjunctions *) @@ -676,7 +691,9 @@ let rec freshen_nested_xs q = (* rename xs to miss all xs in subformulas *) freshen_xs {q with xs; djns} ~wrt:(Var.Set.union q.us xs_below) |> - [%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q'] + [%Trace.retn fun {pf} q' -> + pf "%a" pp q' ; + invariant q'] let rec propagate_equality_ ancestor_vs ancestor_cong q = [%Trace.call fun {pf} -> @@ -706,7 +723,9 @@ let rec propagate_equality_ ancestor_vs ancestor_cong q = assert (is_false cong_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ; star (exists djn_xs cong_djn) q' )) |> - [%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q'] + [%Trace.retn fun {pf} q' -> + pf "%a" pp q' ; + invariant q'] let propagate_equality ancestor_vs ancestor_cong q = [%Trace.call fun {pf} -> @@ -714,7 +733,9 @@ let propagate_equality ancestor_vs ancestor_cong q = ; propagate_equality_ ancestor_vs ancestor_cong q |> - [%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q'] + [%Trace.retn fun {pf} q' -> + pf "%a" pp q' ; + invariant q'] let pp_vss fs vss = Format.fprintf fs "[@[%a@]]" @@ -784,4 +805,6 @@ let simplify q = let q = simplify_ q.us [] q in q |> - [%Trace.retn fun {pf} q' -> pf "@\n" ; invariant q'] + [%Trace.retn fun {pf} q' -> + pf "@\n" ; + invariant q'] diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml index 7ed13ab43..8dc59591d 100644 --- a/sledge/src/solver.ml +++ b/sledge/src/solver.ml @@ -82,7 +82,9 @@ end = struct assert (Var.Set.equal (Var.Set.union us xs) sub.us) ; assert (Var.Set.disjoint us xs) ; assert (Var.Set.is_subset zs ~of_:(Var.Set.union us xs)) - with exc -> [%Trace.info "%a" pp g] ; raise exc + with exc -> + [%Trace.info "%a" pp g] ; + raise exc let with_ ?us ?com ?min ?xs ?sub ?zs ?pgs g = let xs = Option.value xs ~default:g.xs in @@ -651,7 +653,11 @@ let rec excise ({min; xs; sub; zs; pgs} as goal) = else if Sh.is_emp sub then Some (Sh.exists zs (Sh.extend_us xs min)) else if Sh.is_false sub then None else if pgs then - goal |> with_ ~pgs:false |> excise_exists |> excise_pure >>= excise_heap + goal + |> with_ ~pgs:false + |> excise_exists + |> excise_pure + >>= excise_heap >>= excise else None $> fun _ -> [%Trace.info "@[<2>excise fail@ %a@]" pp goal] diff --git a/sledge/src/term.ml b/sledge/src/term.ml index 3d118efdf..7a0976a57 100644 --- a/sledge/src/term.ml +++ b/sledge/src/term.ml @@ -1162,8 +1162,13 @@ let rename sub e = let iter e ~f = match e with | Ap1 (_, x) -> f x - | Ap2 (_, x, y) -> f x ; f y - | Ap3 (_, x, y, z) -> f x ; f y ; f z + | Ap2 (_, x, y) -> + f x ; + f y + | Ap3 (_, x, y, z) -> + f x ; + f y ; + f z | ApN (_, xs) -> IArray.iter ~f xs | And args | Or args -> Set.iter ~f args | Add args | Mul args -> Qset.iter ~f:(fun arg _ -> f arg) args @@ -1210,8 +1215,13 @@ let fold e ~init:s ~f = let rec iter_terms e ~f = ( match e with | Ap1 (_, x) -> iter_terms ~f x - | Ap2 (_, x, y) -> iter_terms ~f x ; iter_terms ~f y - | Ap3 (_, x, y, z) -> iter_terms ~f x ; iter_terms ~f y ; iter_terms ~f z + | Ap2 (_, x, y) -> + iter_terms ~f x ; + iter_terms ~f y + | Ap3 (_, x, y, z) -> + iter_terms ~f x ; + iter_terms ~f y ; + iter_terms ~f z | ApN (_, xs) -> IArray.iter ~f:(iter_terms ~f) xs | And args | Or args -> Set.iter args ~f:(iter_terms ~f) | Add args | Mul args -> diff --git a/sledge/src/term_test.ml b/sledge/src/term_test.ml index c069d2196..63721e454 100644 --- a/sledge/src/term_test.ml +++ b/sledge/src/term_test.ml @@ -79,7 +79,9 @@ let%test_module _ = let%expect_test _ = pp - ( !1 + (!2 * z) + (!3 * y) + ( !1 + + (!2 * z) + + (!3 * y) + (!4 * z * z) + (!5 * y * y) + (!6 * z * y)