[sledge] Style: Change to less compact ocamlformat style

Reviewed By: ngorogiannis

Differential Revision: D21720967

fbshipit-source-id: b5794938c

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

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

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

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 *)
 

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) ])

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} =

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)

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')

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)]
 

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]

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

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

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

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']

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]
 

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 ->

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)