[ocamlformat] upgrade ocamlformat to 0.8

Reviewed By: mbouaziz

Differential Revision: D10359577

fbshipit-source-id: e7f5286e3

.ocamlformat

@@ -1,3 +1,4 @@
+let-binding-spacing = sparse
 break-cases = nested
 margin = 100
-version = 0.7
+version = 0.8

.ocamlformat.hash

@@ -1 +1 @@
-b3ed72b3997cb7712e54f90d47128d6dd8e18f53
+e2cf2fd21fdc2f79840ddf994403a0c2469b6bfd

Makefile

@@ -684,7 +684,7 @@ endif
 # This is a magical version number that doesn't reinstall the world when added on top of what we
 # have in opam.lock. To upgrade this version number, manually try to install several utop versions
 # until you find one that doesn't recompile the world. TODO(t20828442): get rid of magic
-OPAM_DEV_DEPS = ocamlformat.$$(grep version .ocamlformat | cut -d ' ' -f 3) ocp-indent merlin utop.2.2.0 webbrowser
+OPAM_DEV_DEPS = ocp-indent merlin utop.2.2.0 webbrowser
 
 ifneq ($(EMACS),no)
 OPAM_DEV_DEPS += tuareg
@@ -697,6 +697,8 @@ devsetup: Makefile.autoconf
 	  OPAMSWITCH=$(OPAMSWITCH); $(OPAM) install --yes --no-checksum user-setup $(OPAM_DEV_DEPS))
 	$(QUIET)echo '$(TERM_INFO)*** Running `opam config setup -a`$(TERM_RESET)' >&2
 	$(QUIET)OPAMSWITCH=$(OPAMSWITCH); $(OPAM) config --yes setup -a
+	$(QUIET)$(call silent_on_success,installing ocamlformat,\
+	  OPAMSWITCH=$(OPAMSWITCH); $(OPAM) pin add --yes ocamlformat.$$(grep version .ocamlformat | cut -d ' ' -f 3) https://github.com/ocaml-ppx/ocamlformat.git#$$(grep version .ocamlformat | cut -d ' ' -f 3)-opam1)
 	$(QUIET)echo '$(TERM_INFO)*** Running `opam user-setup`$(TERM_RESET)' >&2
 	$(QUIET)OPAMSWITCH=$(OPAMSWITCH); OPAMYES=1; $(OPAM) user-setup install
 	$(QUIET)if [ "$(PLATFORM)" = "Darwin" ] && [ x"$(GNU_SED)" = x"no" ]; then \

infer/src/IR/HilExp.ml

@@ -210,6 +210,7 @@ let rec eval_arithmetic_binop op e1 e2 =
   | _ ->
       None
 
+
 and eval = function
   | Constant c ->
       Some c

infer/src/base/Config.ml

@@ -1187,9 +1187,9 @@ and () =
        "Do not show reports coming from this type of issue. Each checker can report a range of \
         issue types. This option provides fine-grained filtering over which types of issue should \
         be reported once the checkers have run. In particular, note that disabling issue types \
-        does not make the corresponding checker not run.\n \
+        does not make the corresponding checker not run.\n\
-        By default, the following issue types are disabled: %s.\n\n \
+       \ By default, the following issue types are disabled: %s.\n\n\
-        See also $(b,--report-issue-type).\n"
+       \ See also $(b,--report-issue-type).\n"
        (String.concat ~sep:", " disabled_issues_ids)) ;
   mk true ~long:"enable-issue-type"
     ~deprecated:["enable_checks"; "-enable-checks"]

infer/src/base/Die.mli

@@ -7,9 +7,10 @@
 
 open! IStd
 
-(* WARNING: ONLY USE IF Logging IS NOT AVAILABLE TO YOU FOR SOME REASON (e.g., inside Config). *)
+exception
-
+  (* WARNING: ONLY USE IF Logging IS NOT AVAILABLE TO YOU FOR SOME REASON (e.g., inside Config). *)
-exception InferExternalError of string
+    InferExternalError of
+    string
 
 exception InferInternalError of string
 

infer/src/base/RunState.ml

@@ -45,8 +45,8 @@ let load_and_validate () =
         Error
           (Printf.sprintf
              "'%s' already exists but it is not an empty directory and it does not look like an \
-              infer results directory:\n  \
+              infer results directory:\n\
-              %s\n\
+             \  %s\n\
               Was it created using an older version of infer?"
              Config.results_dir err_msg) )
       msg

infer/src/biabduction/Rearrange.mli

@@ -10,9 +10,8 @@ open! IStd
 
 (** Re-arrangement and extension of structures with fresh variables *)
 
-(* TODO: this description is not clear *)
+exception (* TODO: this description is not clear *)
-
+            ARRAY_ACCESS
-exception ARRAY_ACCESS
 
 val is_only_pt_by_fld_or_param_nonnull :
   Procdesc.t -> Tenv.t -> Prop.normal Prop.t -> Exp.t -> bool

infer/src/checkers/control.ml

@@ -8,6 +8,7 @@
 open! IStd
 module F = Format
 module L = Logging
+
 (* forward dependency analysis for computing set of variables that
    affect the looping behavior of the program
 

infer/src/checkers/dominators.ml

@@ -8,6 +8,7 @@ open! IStd
 open Graph
 module L = Logging
 module CFG = ProcCfg.Normal
+
 (* Use ocamlgraph's dominators functor to get the dominators *)
 module GDoms = Dominator.Make (ProcCfg.MakeOcamlGraph (CFG))
 

infer/src/checkers/uninitDomain.ml

@@ -148,5 +148,6 @@ module Summary = struct
     post = set of uninit local variables of the procedure *)
   type t = Domain.t prepost
 
-  let pp fmt {pre; post} = F.fprintf fmt "@\n Pre: %a @\nPost: %a @\n" Domain.pp pre Domain.pp post
+  let pp fmt {pre; post} =
+    F.fprintf fmt "@\n Pre: %a @\nPost: %a @\n" Domain.pp pre Domain.pp post
 end

infer/src/clang/Capture.ml

@@ -160,7 +160,8 @@ let cc1_capture clang_cmd =
   else if
     Config.skip_analysis_in_path_skips_compilation && CLocation.is_file_blacklisted source_path
   then (
-    L.(debug Capture Quiet) "@\n Skip compilation and analysis of source file %s@\n@\n" source_path ;
+    L.(debug Capture Quiet)
+      "@\n Skip compilation and analysis of source file %s@\n@\n" source_path ;
     () )
   else
     match Config.clang_biniou_file with

infer/src/clang/ClangWrapper.ml

@@ -180,7 +180,7 @@ let exe ~prog ~args =
            files. *)
       L.(debug Capture Quiet)
         "WARNING: `clang -### <args>` returned an empty set of commands to run and no error. Will \
-         run the original command directly:@\n  \
+         run the original command directly:@\n\
-         %s@\n"
+        \  %s@\n"
         (String.concat ~sep:" " @@ (prog :: args)) ;
     Process.create_process_and_wait ~prog ~args )

infer/src/clang/cTL.ml

@@ -1165,6 +1165,7 @@ let rec eval_Atomic pred_name_ args an lcxt =
   | _ ->
       L.(die ExternalError) "Undefined Predicate or wrong set of arguments: '%s'" pred_name
 
+
 and eval_AND an lcxt f1 f2 =
   match eval_formula f1 an lcxt with
   | Some witness1 -> (
@@ -1176,6 +1177,7 @@ and eval_AND an lcxt f1 f2 =
   | None (* we short-circuit the AND evaluation *) ->
       None
 
+
 and eval_OR an lcxt f1 f2 = choose_witness_opt (eval_formula f1 an lcxt) (eval_formula f2 an lcxt)
 
 and eval_Implies an lcxt f1 f2 =
@@ -1183,6 +1185,7 @@ and eval_Implies an lcxt f1 f2 =
   let witness2 = eval_formula f2 an lcxt in
   choose_witness_opt witness1 witness2
 
+
 (* an, lcxt |= EF phi  <=>
    an, lcxt |= phi or exists an' in Successors(st): an', lcxt |= EF phi
 
@@ -1203,6 +1206,7 @@ and eval_EF phi an lcxt trans =
         List.fold_left (Ctl_parser_types.get_direct_successor_nodes an) ~init:witness_opt
           ~f:(fun acc node -> choose_witness_opt (eval_EF phi node lcxt trans) acc )
 
+
 (* an, lcxt |= EX phi  <=> exists an' in Successors(st): an', lcxt |= phi
 
    That is: a (an, lcxt) satifies EX phi if and only if
@@ -1227,6 +1231,7 @@ and eval_EX phi an lcxt trans =
   | _ ->
       witness_opt
 
+
 (* an, lcxt |= E(phi1 U phi2) evaluated using the equivalence
    an, lcxt |= E(phi1 U phi2) <=> an, lcxt |= phi2 or (phi1 and EX(E(phi1 U phi2)))
 
@@ -1237,6 +1242,7 @@ and eval_EU phi1 phi2 an lcxt trans =
   let f = Or (phi2, And (phi1, EX (trans, EU (trans, phi1, phi2)))) in
   eval_formula f an lcxt
 
+
 (* an |= A(phi1 U phi2) evaluated using the equivalence
    an |= A(phi1 U phi2) <=> an |= phi2 or (phi1 and AX(A(phi1 U phi2)))
 
@@ -1246,6 +1252,7 @@ and eval_AU phi1 phi2 an lcxt trans =
   let f = Or (phi2, And (phi1, AX (trans, AU (trans, phi1, phi2)))) in
   eval_formula f an lcxt
 
+
 (* an, lcxt |= InNode[node_type_list] phi <=>
    an is a node of type in node_type_list and an satifies phi
 *)
@@ -1263,6 +1270,7 @@ and in_node node_type_list phi an lctx =
   List.fold_left node_type_list ~init:None ~f:(fun acc node ->
       choose_witness_opt (holds_for_one_node node) acc )
 
+
 (* Intuitive meaning: (an,lcxt) satifies EH[Classes] phi
    if the node an is among the declaration specified by the list Classes and
    there exists a super class in its hierarchy whose declaration satisfy phi.
@@ -1275,6 +1283,7 @@ and eval_EH classes phi an lcxt =
   let f = ET (classes, None, EX (Some Super, EF (Some Super, phi))) in
   eval_formula f an lcxt
 
+
 (* an, lcxt |= ET[T][->l]phi <=>
    eventually we reach a node an' such that an' is among the types defined in T
    and:
@@ -1295,6 +1304,7 @@ and eval_ET tl trs phi an lcxt =
   in
   eval_formula f an lcxt
 
+
 (* Formulas are evaluated on a AST node an and a linter context lcxt *)
 and eval_formula f an lcxt : Ctl_parser_types.ast_node option =
   debug_eval_begin (debug_create_payload an f lcxt) ;

infer/src/clang/cType_to_sil_type.ml

@@ -98,6 +98,7 @@ let rec build_array_type translate_decl tenv (qual_type : Clang_ast_t.qual_type)
   let stride = Option.map ~f:IntLit.of_int stride_opt in
   Typ.Tarray {elt= array_type; length; stride}
 
+
 and type_desc_of_attr_type translate_decl tenv type_info attr_info =
   match type_info.Clang_ast_t.ti_desugared_type with
   | Some type_ptr -> (
@@ -110,6 +111,7 @@ and type_desc_of_attr_type translate_decl tenv type_info attr_info =
   | None ->
       Typ.Tvoid
 
+
 and type_desc_of_c_type translate_decl tenv c_type : Typ.desc =
   let open Clang_ast_t in
   match c_type with
@@ -167,6 +169,7 @@ and type_desc_of_c_type translate_decl tenv c_type : Typ.desc =
       | None ->
           Typ.Tvoid )
 
+
 and decl_ptr_to_type_desc translate_decl tenv decl_ptr : Typ.desc =
   let open Clang_ast_t in
   let typ = Clang_ast_extend.DeclPtr decl_ptr in
@@ -194,6 +197,7 @@ and decl_ptr_to_type_desc translate_decl tenv decl_ptr : Typ.desc =
           (Clang_ast_j.string_of_pointer decl_ptr) ;
         Typ.Tvoid )
 
+
 and clang_type_ptr_to_type_desc translate_decl tenv type_ptr =
   try Clang_ast_extend.TypePointerMap.find type_ptr !CFrontend_config.sil_types_map
   with Caml.Not_found -> (
@@ -205,6 +209,7 @@ and clang_type_ptr_to_type_desc translate_decl tenv type_ptr =
     | _ ->
         Typ.Tvoid )
 
+
 and type_ptr_to_type_desc translate_decl tenv type_ptr : Typ.desc =
   match type_ptr with
   | Clang_ast_types.TypePtr.Ptr _ ->
@@ -226,6 +231,7 @@ and type_ptr_to_type_desc translate_decl tenv type_ptr : Typ.desc =
   | _ ->
       L.(die InternalError) "unknown variant for type_ptr"
 
+
 and qual_type_to_sil_type translate_decl tenv qual_type =
   let desc = type_ptr_to_type_desc translate_decl tenv qual_type.Clang_ast_t.qt_type_ptr in
   let quals = Typ.mk_type_quals ~is_const:qual_type.Clang_ast_t.qt_is_const () in

infer/src/clang/clang_ast_extend.ml

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+
 (* This module adds more variants to some types in AST The implementation extends default one from
    the facebook-clang-plugins repository *)
 
@@ -88,6 +89,7 @@ module TypePointerOrd = struct
         L.(die InternalError)
           "unexpected type_ptr variants: %s, %s" (type_ptr_to_string t1) (type_ptr_to_string t2)
 
+
   and compare_qual_type (qt1 : Clang_ast_t.qual_type) (qt2 : Clang_ast_t.qual_type) =
     if phys_equal qt1 qt2 then 0
     else

infer/src/clang/tableaux.ml

@@ -254,10 +254,10 @@ let add_valid_formulae an checker lcxt cl =
         add_in_set phi acc_set
     | AG _ | AX _ | AF _ | AU _ | EH _ | ET _ | Implies _ ->
         Logging.die InternalError
-          "@\n \
+          "@\n\
-           We should not have operators AG, AX, AF, AU, EH, ET.\n  \
+          \ We should not have operators AG, AX, AF, AU, EH, ET.\n\
-           Failing with formula @\n   \
+          \  Failing with formula @\n\
-           %a@\n"
+          \   %a@\n"
           CTL.Debug.pp_formula phi
     | _ ->
         acc_set

infer/src/concurrency/RacerD.ml

@@ -742,7 +742,8 @@ let get_reporting_explanation_java report_kind tenv pname thread =
     if is_thread_safe_method pname tenv then
       Some
         (F.asprintf
-           "@\n Reporting because current method is annotated %a or overrides an annotated method."
+           "@\n\
+           \ Reporting because current method is annotated %a or overrides an annotated method."
            MF.pp_monospaced "@ThreadSafe")
     else
       match FbThreadSafety.get_fbthreadsafe_class_annot pname tenv with
@@ -788,8 +789,8 @@ let get_reporting_explanation_java report_kind tenv pname thread =
       else
         ( IssueType.thread_safety_violation
         , F.asprintf
-            "@\n \
+            "@\n\
-             Reporting because another access to the same memory occurs on a background thread, \
+            \ Reporting because another access to the same memory occurs on a background thread, \
              although this access may not." )
 
 

infer/src/concurrency/RacerDDomain.ml

@@ -698,8 +698,8 @@ let pp_summary fmt {threads; locks; accesses; return_ownership; return_attribute
 let pp fmt {threads; locks; accesses; ownership; attribute_map; wobbly_paths} =
   F.fprintf fmt
     "Threads: %a, Locks: %a @\n\
-     Accesses %a @\n \
+     Accesses %a @\n\
-     Ownership: %a @\n\
+    \ Ownership: %a @\n\
      Attributes: %a @\n\
      Non-stable Paths: %a@\n"
     ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp

infer/src/unit/TaintTests.ml

@@ -137,9 +137,9 @@ let tests =
         ; read_field_to_id "read_id" "base_id" "f"
         ; var_assign_id "var" "read_id"
         ; invariant
-            "{ base_id$0.f* => (SOURCE -> ?),\n  \
+            "{ base_id$0.f* => (SOURCE -> ?),\n\
-             ret_id$0* => (SOURCE -> ?),\n  \
+            \  ret_id$0* => (SOURCE -> ?),\n\
-             var* => (SOURCE -> ?) }" ] )
+            \  var* => (SOURCE -> ?) }" ] )
     ; ( "source flows to var then cleared"
       , [ assign_to_source "ret_id"
         ; var_assign_id "var" "ret_id"

sledge/src/config.ml

@@ -39,6 +39,7 @@ end = struct
     let (Arg (trm, set)) = List.fold_right ~f:pair args ~init in
     Term.app (Term.const set) trm
 
+
   let args : arg list ref = ref []
 
   let mk ~default arg =
@@ -47,6 +48,7 @@ end = struct
     args := Arg (arg, set) :: !args ;
     var
 
+
   let parse info validate =
     match Term.eval (Term.(ret (const validate $ tuple !args)), info) with
     | `Ok () -> ()
@@ -60,14 +62,17 @@ let input =
   mk ~default:""
     Arg.(required & pos ~rev:true 0 (some string) None & info [])
 
+
 let output =
   let default = None in
   mk ~default Arg.(value & opt (some string) default & info ["o"; "output"])
 
+
 let trace_all =
   let default = false in
   mk ~default Arg.(value & flag & info ["t"; "trace-all"])
 
+
 let info = Term.info "sledge" ~version:Version.version
 
 let validate () = `Ok ()

sledge/src/import/import.ml

@@ -43,11 +43,13 @@ let option_fmt fmt pp ff = function
   | Some x -> Format.fprintf ff fmt pp x
   | None -> ()
 
+
 let rec list_fmt sep pp ff = function
   | [] -> ()
   | [x] -> pp ff x
   | x :: xs -> Format.fprintf ff "%a%( %)%a" pp x sep (list_fmt sep pp) xs
 
+
 let vector_fmt sep pp ff v = list_fmt sep pp ff (Vector.to_list v)
 
 let warn fmt =
@@ -60,6 +62,7 @@ let warn fmt =
       Format.pp_force_newline ff () )
     ff fmt
 
+
 let raisef exn fmt =
   let bt = Caml.Printexc.get_raw_backtrace () in
   let ff = Format.str_formatter in
@@ -72,6 +75,7 @@ let raisef exn fmt =
       Caml.Printexc.raise_with_backtrace exn bt )
     ff fmt
 
+
 exception Unimplemented of string
 
 let todo fmt = raisef (fun msg -> Unimplemented msg) fmt
@@ -82,10 +86,12 @@ let assertf cnd fmt =
   if not cnd then fail fmt
   else Format.ikfprintf (fun _ () -> ()) Format.str_formatter fmt
 
+
 let checkf cnd fmt =
   if not cnd then fail fmt
   else Format.ikfprintf (fun _ () -> true) Format.str_formatter fmt
 
+
 type 'a or_error = ('a, exn * Caml.Printexc.raw_backtrace) Result.t
 
 let or_error f x () =

sledge/src/llair/exp.ml

@@ -70,6 +70,7 @@ let uncurry exp =
   in
   uncurry_ [] exp
 
+
 let rec fmt ff exp =
   let pf fmt =
     Format.pp_open_box ff 2 ;
@@ -125,6 +126,7 @@ let rec fmt ff exp =
   | Rem, [x; y] -> pf "(%a@ %% %a)" fmt x fmt y
   | URem, [x; y] -> pf "(%a@ u%% %a)" fmt x fmt y
 
+
 (** Queries *)
 
 let rec typ_of : t -> Typ.t = function[@warning "p"]
@@ -172,6 +174,7 @@ let rec typ_of : t -> Typ.t = function[@warning "p"]
       typ_of arg
   | AppN {op} -> typ_of op
 
+
 let valid_fld fld elts = 0 <= fld && fld < Vector.length elts
 
 (** Re-exported modules *)
@@ -220,6 +223,7 @@ module Global = struct
       (option_fmt " =@ @[%a@]" fmt)
       init
 
+
   let fmt = fmt
 
   let mk ?init ?(loc = Loc.none) name typ =
@@ -228,6 +232,7 @@ module Global = struct
           Typ.equal typ (Typ.mkPointer ~elt:(typ_of exp)) ) ) ;
     Global {name; init; typ; loc}
 
+
   let of_exp e = match e with Global _ -> Some e | _ -> None
 
   let name = function[@warning "p"] Global {name} -> name
@@ -249,6 +254,7 @@ let locate loc exp =
   | AppN {op; args} -> AppN {op; args; loc}
   | _ -> exp
 
+
 let mkApp1 op arg = App {op; arg; loc= Loc.none}
 
 let mkApp2 op x y = mkApp1 (mkApp1 op x) y
@@ -265,12 +271,14 @@ let mkNondet (typ : Typ.t) msg =
   assert (match typ with Function _ -> false | _ -> true) ;
   Nondet {typ; loc= Loc.none; msg}
 
+
 let mkLabel ~parent ~name = Label {parent; name; loc= Loc.none}
 
 let mkNull (typ : Typ.t) =
   assert (match typ with Opaque _ | Function _ -> false | _ -> true) ;
   Null {typ}
 
+
 let mkPtrFld ~ptr ~fld =
   assert (
     match typ_of ptr with
@@ -278,6 +286,7 @@ let mkPtrFld ~ptr ~fld =
     | _ -> false ) ;
   mkApp1 (PtrFld {fld}) ptr
 
+
 let mkPtrIdx ~ptr ~idx =
   assert (
     match (typ_of ptr, typ_of idx) with
@@ -285,6 +294,7 @@ let mkPtrIdx ~ptr ~idx =
     | _ -> false ) ;
   mkApp2 PtrIdx ptr idx
 
+
 let mkPrjFld ~agg ~fld =
   assert (
     match typ_of agg with
@@ -292,6 +302,7 @@ let mkPrjFld ~agg ~fld =
     | _ -> false ) ;
   mkApp1 (PrjFld {fld}) agg
 
+
 let mkPrjIdx ~arr ~idx =
   assert (
     match (typ_of arr, typ_of idx) with
@@ -299,6 +310,7 @@ let mkPrjIdx ~arr ~idx =
     | _ -> false ) ;
   mkApp2 PrjIdx arr idx
 
+
 let mkUpdFld ~agg ~elt ~fld =
   assert (
     match typ_of agg with
@@ -307,6 +319,7 @@ let mkUpdFld ~agg ~elt ~fld =
     | _ -> false ) ;
   mkApp2 (UpdFld {fld}) agg elt
 
+
 let mkUpdIdx ~arr ~elt ~idx =
   assert (
     match (typ_of arr, typ_of idx) with
@@ -314,6 +327,7 @@ let mkUpdIdx ~arr ~elt ~idx =
     | _ -> false ) ;
   mkApp3 UpdIdx arr elt idx
 
+
 let mkInteger data (typ : Typ.t) =
   assert (
     let in_range num bits =
@@ -324,12 +338,14 @@ let mkInteger data (typ : Typ.t) =
     match typ with Integer {bits} -> in_range data bits | _ -> false ) ;
   Integer {data; typ}
 
+
 let mkBool b = mkInteger (Z.of_int (Bool.to_int b)) Typ.i1
 
 let mkFloat data (typ : Typ.t) =
   assert (match typ with Float _ -> true | _ -> false) ;
   Float {data; typ}
 
+
 let mkArray elts (typ : Typ.t) =
   assert (
     match typ with
@@ -339,6 +355,7 @@ let mkArray elts (typ : Typ.t) =
     | _ -> false ) ;
   mkAppN (Array {typ}) elts
 
+
 let mkStruct elts (typ : Typ.t) =
   assert (
     match typ with
@@ -348,6 +365,7 @@ let mkStruct elts (typ : Typ.t) =
     | _ -> false ) ;
   mkAppN (Struct {typ}) elts
 
+
 let mkStruct_rec key =
   let memo_id = Hashtbl.create key () in
   let dummy = Null {typ= Typ.mkBytes} in
@@ -373,14 +391,17 @@ let mkStruct_rec key =
   in
   Staged.stage mkStruct_
 
+
 let mkCast exp typ =
   assert (Typ.compatible (typ_of exp) typ) ;
   mkApp1 (Cast {typ}) exp
 
+
 let mkConv exp ?(signed = false) typ =
   assert (Typ.compatible (typ_of exp) typ) ;
   mkApp1 (Conv {signed; typ}) exp
 
+
 let mkSelect ~cnd ~thn ~els =
   assert (
     match (typ_of cnd, typ_of thn, typ_of els) with
@@ -390,6 +411,7 @@ let mkSelect ~cnd ~thn ~els =
     | _ -> false ) ;
   mkApp3 Select cnd thn els
 
+
 let binop op x y =
   assertf
     (let typ = typ_of x in
@@ -404,6 +426,7 @@ let binop op x y =
     "ill-typed: %a" fmt (mkApp2 op x y) () ;
   mkApp2 op x y
 
+
 let mkEq = binop Eq
 
 let mkNe = binop Ne

sledge/src/llair/frontend.ml

@@ -14,6 +14,7 @@ let fmt_llvalue ff t = Format.pp_print_string ff (Llvm.string_of_llvalue t)
 let fmt_llblock ff t =
   Format.pp_print_string ff (Llvm.string_of_llvalue (Llvm.value_of_block t))
 
+
 (* gather debug locations *)
 let (scan_locs : Llvm.llmodule -> unit), (find_loc : Llvm.llvalue -> Loc.t)
     =
@@ -81,6 +82,7 @@ let (scan_locs : Llvm.llmodule -> unit), (find_loc : Llvm.llvalue -> Loc.t)
   in
   (scan_locs, find_loc)
 
+
 let ( (scan_names : Llvm.llmodule -> unit)
     , (find_name : Llvm.llvalue -> string) ) =
   let name_tbl = Hashtbl.Poly.create () in
@@ -156,12 +158,15 @@ let ( (scan_names : Llvm.llmodule -> unit)
   let find_name v = Hashtbl.find_exn name_tbl v in
   (scan_names, find_name)
 
+
 let label_of_block : Llvm.llbasicblock -> string =
  fun blk -> find_name (Llvm.value_of_block blk)
 
+
 let anon_struct_name : (Llvm.lltype, string) Hashtbl.t =
   Hashtbl.Poly.create ()
 
+
 let struct_name : Llvm.lltype -> string =
  fun llt ->
   match Llvm.struct_name llt with
@@ -170,6 +175,7 @@ let struct_name : Llvm.lltype -> string =
       Hashtbl.find_or_add anon_struct_name llt ~default:(fun () ->
           Int.to_string (Hashtbl.length anon_struct_name) )
 
+
 let memo_type : (Llvm.lltype, Typ.t) Hashtbl.t = Hashtbl.Poly.create ()
 
 let rec xlate_type : Llvm.lltype -> Typ.t =
@@ -226,12 +232,14 @@ let rec xlate_type : Llvm.lltype -> Typ.t =
       |>
       [%Trace.retn fun pf -> pf "%a" Typ.fmt_defn] )
 
+
 and xlate_type_opt : Llvm.lltype -> Typ.t option =
  fun llt ->
   match Llvm.classify_type llt with
   | Void -> None
   | _ -> Some (xlate_type llt)
 
+
 let rec is_zero : Exp.t -> bool =
  fun exp ->
   match exp with
@@ -241,9 +249,11 @@ let rec is_zero : Exp.t -> bool =
   | App {op; arg} -> is_zero op && is_zero arg
   | _ -> false
 
+
 let suffix_after_space : string -> string =
  fun str -> String.slice str (String.rindex_exn str ' ' + 1) 0
 
+
 let xlate_int : Llvm.llvalue -> Exp.t =
  fun llv ->
   let typ = xlate_type (Llvm.type_of llv) in
@@ -254,12 +264,14 @@ let xlate_int : Llvm.llvalue -> Exp.t =
   in
   Exp.mkInteger data typ
 
+
 let xlate_float : Llvm.llvalue -> Exp.t =
  fun llv ->
   let typ = xlate_type (Llvm.type_of llv) in
   let data = suffix_after_space (Llvm.string_of_llvalue llv) in
   Exp.mkFloat data typ
 
+
 let xlate_name_opt : Llvm.llvalue -> Var.t option =
  fun instr ->
   Option.map
@@ -269,9 +281,11 @@ let xlate_name_opt : Llvm.llvalue -> Var.t option =
       let loc = find_loc instr in
       Var.mk name typ ~loc )
 
+
 let xlate_name : Llvm.llvalue -> Var.t =
  fun instr -> Option.value_exn (xlate_name_opt instr)
 
+
 let xlate_intrinsic_exp : string -> (Exp.t -> Exp.t) option =
  fun name ->
   let i32 = Typ.mkInteger ~bits:32 in
@@ -279,6 +293,7 @@ let xlate_intrinsic_exp : string -> (Exp.t -> Exp.t) option =
   | "llvm.eh.typeid.for" -> Some (fun arg -> Exp.mkCast arg i32)
   | _ -> None
 
+
 let memo_value : (Llvm.llvalue, Exp.t) Hashtbl.t = Hashtbl.Poly.create ()
 
 module Llvalue = struct
@@ -368,6 +383,7 @@ let rec xlate_value : Llvm.llvalue -> Exp.t =
           typ' fmt_llvalue llv () ;
         pf "%a" Exp.fmt exp] )
 
+
 and xlate_opcode : Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
  fun llv opcode ->
   [%Trace.call fun pf -> pf "%a" fmt_llvalue llv]
@@ -529,6 +545,7 @@ and xlate_opcode : Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
       fmt_llvalue llv () ;
     pf "%a" Exp.fmt exp]
 
+
 and xlate_global : Llvm.llvalue -> Global.t =
  fun llg ->
   let init =
@@ -540,6 +557,7 @@ and xlate_global : Llvm.llvalue -> Global.t =
   let g = xlate_name llg in
   Global.mk (Var.name g) (Var.typ g) ~loc:(Var.loc g) ?init
 
+
 let xlate_global : Llvm.llvalue -> Global.t =
  fun llg ->
   [%Trace.call fun pf -> pf "%a" fmt_llvalue llg]
@@ -548,6 +566,7 @@ let xlate_global : Llvm.llvalue -> Global.t =
   |>
   [%Trace.retn fun pf -> pf "%a" Global.fmt]
 
+
 type pop_thunk = Loc.t -> Llair.inst list
 
 let pop_stack_frame_of_function :
@@ -580,6 +599,7 @@ let pop_stack_frame_of_function :
   in
   pop
 
+
 (** construct the types involved in landingpads: i32, std::type_info*, and
     __cxa_exception *)
 let landingpad_typs : Llvm.llvalue -> Typ.t * Typ.t * Typ.t =
@@ -607,12 +627,14 @@ let landingpad_typs : Llvm.llvalue -> Typ.t * Typ.t * Typ.t =
   let cxa_exception = Llvm.struct_type llcontext [|tip; dtor|] in
   (i32, xlate_type tip, xlate_type cxa_exception)
 
+
 (** construct the argument of a landingpad block, mainly fix the encoding
     scheme for landingpad instruction name to block arg name *)
 let landingpad_arg : Llvm.llvalue -> Var.t =
  fun instr ->
   Var.mk (find_name instr ^ ".exc") Typ.i8p ~loc:(find_loc instr)
 
+
 (** [rev_map_phis ~f blk] returns [(retn_arg, rev_args, pos)] by rev_mapping
     over the prefix of [PHI] instructions at the beginning of [blk].
     [retn_arg], if any, is [f] applied to the [PHI] instruction which takes
@@ -669,6 +691,7 @@ let rev_map_phis :
   in
   block_args_ false None [] (Llvm.instr_begin blk)
 
+
 (** [trampoline_args jump_instr dest_block] is the actual arguments to which
     the translation of [dest_block] should be partially-applied, to yield a
     trampoline accepting the return parameter of the block and then jumping
@@ -681,6 +704,7 @@ let trampoline_args : Llvm.llvalue -> Llvm.llbasicblock -> Exp.t vector =
           if Poly.equal pred src then Some (xlate_value arg) else None ) )
   |> snd3 |> Vector.of_list_rev
 
+
 (** [unique_pred blk] is the unique predecessor of [blk], or [None] if there
     are 0 or >1 predecessors. *)
 let unique_pred : Llvm.llbasicblock -> Llvm.llvalue option =
@@ -692,11 +716,13 @@ let unique_pred : Llvm.llbasicblock -> Llvm.llvalue option =
     | Some _ -> None )
   | None -> None
 
+
 (** [return_formal_is_used instr] holds if the return value of [instr] is
     used anywhere. *)
 let return_formal_is_used : Llvm.llvalue -> bool =
  fun instr -> Option.is_some (Llvm.use_begin instr)
 
+
 (** [need_return_trampoline instr blk] holds when the return formal of
     [instr] is used, but the returned to block [blk] does not take it as an
     argument (e.g. if it has multiple predecessors and no PHI node). *)
@@ -706,6 +732,7 @@ let need_return_trampoline : Llvm.llvalue -> Llvm.llbasicblock -> bool =
   && Option.is_none (unique_pred blk)
   && return_formal_is_used instr
 
+
 (** [unique_used_invoke_pred blk] is the unique predecessor of [blk], if it
     is an [Invoke] instruction, whose return value is used. *)
 let unique_used_invoke_pred : Llvm.llbasicblock -> 'a option =
@@ -716,6 +743,7 @@ let unique_used_invoke_pred : Llvm.llbasicblock -> 'a option =
       Some instr
   | _ -> None
 
+
 (** formal parameters accepted by a block *)
 let block_formals : Llvm.llbasicblock -> Var.t list * _ Llvm.llpos =
  fun blk ->
@@ -734,6 +762,7 @@ let block_formals : Llvm.llbasicblock -> Var.t list * _ Llvm.llpos =
       (List.rev_append rev_args (Option.to_list instr_arg), pos)
   | At_end blk -> fail "block_formals: %a" fmt_llblock blk ()
 
+
 (** actual arguments passed by a jump to a block *)
 let jump_args : Llvm.llvalue -> Llvm.llbasicblock -> Exp.t vector =
  fun jmp dst ->
@@ -752,6 +781,7 @@ let jump_args : Llvm.llvalue -> Llvm.llbasicblock -> Exp.t vector =
   in
   Vector.of_list (List.rev_append rev_args (Option.to_list retn_arg))
 
+
 (** An LLVM instruction is translated to a sequence of LLAIR instructions
     and a terminator, plus some additional blocks to which it may refer
     (that is, essentially a function body). These are needed since LLVM and
@@ -774,6 +804,7 @@ let fmt_code ff (insts, term, blocks) =
     (list_fmt "@ " Llair.Block.fmt)
     blocks
 
+
 let rec xlate_func_name llv =
   match Llvm.classify_value llv with
   | Function ->
@@ -788,6 +819,7 @@ let rec xlate_func_name llv =
   | InlineAsm -> todo "inline asm: %a" fmt_llvalue llv ()
   | _ -> fail "unknown function: %a" fmt_llvalue llv ()
 
+
 let xlate_instr :
        pop_thunk
     -> Llvm.llvalue
@@ -1173,6 +1205,7 @@ let xlate_instr :
       fail "xlate_instr: %a" fmt_llvalue instr ()
   | PHI | Invalid | Invalid2 | UserOp1 | UserOp2 -> assert false
 
+
 let rec xlate_instrs : pop_thunk -> _ Llvm.llpos -> code =
  fun pop -> function
   | Before instrI ->
@@ -1183,6 +1216,7 @@ let rec xlate_instrs : pop_thunk -> _ Llvm.llpos -> code =
           (instsI, termI, blocksI @ blocksJN) )
   | At_end blk -> fail "xlate_instrs: %a" fmt_llblock blk ()
 
+
 let xlate_block : pop_thunk -> Llvm.llbasicblock -> Llair.block list =
  fun pop blk ->
   [%Trace.call fun pf -> pf "%a" fmt_llblock blk]
@@ -1196,6 +1230,7 @@ let xlate_block : pop_thunk -> Llvm.llbasicblock -> Llair.block list =
   |>
   [%Trace.retn fun pf blocks -> pf "%s" (List.hd_exn blocks).Llair.lbl]
 
+
 let xlate_function : Llvm.llvalue -> Llair.func =
  fun llf ->
   [%Trace.call fun pf -> pf "%a" fmt_llvalue llf]
@@ -1234,6 +1269,7 @@ let xlate_function : Llvm.llvalue -> Llair.func =
   |>
   [%Trace.retn fun pf -> pf "@\n%a" Llair.Func.fmt]
 
+
 let transform : Llvm.llmodule -> unit =
  fun llmodule ->
   let pm = Llvm.PassManager.create () in
@@ -1245,6 +1281,7 @@ let transform : Llvm.llmodule -> unit =
   Llvm.PassManager.run_module llmodule pm |> (ignore : bool -> _) ;
   Llvm.PassManager.dispose pm
 
+
 exception Invalid_llvm of string
 
 let invalid_llvm : string -> 'a =
@@ -1256,6 +1293,7 @@ let invalid_llvm : string -> 'a =
   Format.printf "@\n%s@\n" msg ;
   raise (Invalid_llvm first_line)
 
+
 let translate : string -> Llair.t =
  fun file ->
   [%Trace.call fun pf -> pf "%s" file]

sledge/src/llair/llair.ml

@@ -66,9 +66,11 @@ let rec dummy_block =
   ; parent= dummy_func
   ; sort_index= 0 }
 
+
 and dummy_func =
   {name= Global.mk "dummy" Typ.i8p; entry= dummy_block; cfg= Vector.empty}
 
+
 module Inst = struct
   type t = inst
 
@@ -79,6 +81,7 @@ module Inst = struct
       | _ -> false ) ;
     Load {reg; ptr; loc}
 
+
   let mkStore ~ptr ~exp ~loc =
     assert (
       match Exp.typ ptr with
@@ -86,6 +89,7 @@ module Inst = struct
       | _ -> false ) ;
     Store {ptr; exp; loc}
 
+
   let mkMemcpy ~dst ~src ~len ~loc =
     assert (
       match (Exp.typ dst, Exp.typ src, Exp.typ len) with
@@ -94,6 +98,7 @@ module Inst = struct
       | _ -> false ) ;
     Memcpy {dst; src; len; loc}
 
+
   let mkMemmov ~dst ~src ~len ~loc =
     assert (
       match (Exp.typ dst, Exp.typ src, Exp.typ len) with
@@ -102,6 +107,7 @@ module Inst = struct
       | _ -> false ) ;
     Memmov {dst; src; len; loc}
 
+
   let mkMemset ~dst ~byt ~len ~loc =
     assert (
       match (Exp.typ dst, Exp.typ byt, Exp.typ len) with
@@ -109,6 +115,7 @@ module Inst = struct
       | _ -> false ) ;
     Memset {dst; byt; len; loc}
 
+
   let mkAlloc ~reg ~num ~loc =
     assert (
       match (Var.typ reg, Exp.typ num) with
@@ -116,6 +123,7 @@ module Inst = struct
       | _ -> false ) ;
     Alloc {reg; num; loc}
 
+
   let mkFree ~ptr ~loc =
     assert (
       match Exp.typ ptr with
@@ -123,10 +131,12 @@ module Inst = struct
       | _ -> false ) ;
     Free {ptr; loc}
 
+
   let mkNondet ~reg ~msg ~loc =
     assert (Option.for_all ~f:(Var.typ >> Typ.is_sized) reg) ;
     Nondet {reg; msg; loc}
 
+
   let fmt ff inst =
     let pf fmt = Format.fprintf ff fmt in
     match inst with
@@ -151,9 +161,11 @@ let fmt_cmnd = vector_fmt "@ " Inst.fmt
 let fmt_args fmt_arg ff args =
   Format.fprintf ff "@ (@[%a@])" (vector_fmt ",@ " fmt_arg) args
 
+
 let fmt_param ff var =
   Format.fprintf ff "%a %a" Typ.fmt (Var.typ var) Var.fmt var
 
+
 module Jump = struct
   type t = jump
 
@@ -172,6 +184,7 @@ module Term = struct
     assert (match Exp.typ key with Integer _ -> true | _ -> false) ;
     Switch {key; tbl; els; loc}
 
+
   let mkISwitch ~ptr ~tbl ~loc =
     assert (
       match Exp.typ ptr with
@@ -179,6 +192,7 @@ module Term = struct
       | _ -> false ) ;
     ISwitch {ptr; tbl; loc}
 
+
   let mkCall ~func ~args ~return ~throw ~ignore_result ~loc =
     assert (
       match Exp.typ func with
@@ -193,6 +207,7 @@ module Term = struct
       ; ignore_result
       ; loc }
 
+
   let mkReturn ~exp ~loc = Return {exp; loc}
 
   let mkThrow ~exc ~loc = Throw {exc; loc}
@@ -239,6 +254,7 @@ module Block = struct
     ) ;
     {dummy_block with lbl; params; cmnd; term}
 
+
   (* blocks in a [t] are uniquely identified by [sort_index] *)
   let compare x y = Int.compare x.sort_index y.sort_index
 
@@ -257,15 +273,18 @@ module Func = struct
   let find functions func =
     Vector.find functions ~f:(fun {name} -> Global.equal func name)
 
+
   let is_undefined = function
     | {entry= {cmnd; term= Unreachable}} -> Vector.is_empty cmnd
     | _ -> false
 
+
   let fold_term {entry; cfg} ~init ~f =
     let fold_block {term} ~init ~f = f init term in
     Vector.fold cfg ~init:(fold_block entry ~init ~f) ~f:(fun z k ->
         fold_block k ~init:z ~f )
 
+
   let mk ~name ~entry ~cfg =
     let func = {name; entry; cfg} in
     let resolve_parent_and_jumps block =
@@ -330,6 +349,7 @@ module Func = struct
       true ) ;
     func
 
+
   let mk_undefined ~name ~params =
     let entry =
       Block.mk ~lbl:"" ~params ~cmnd:Vector.empty ~term:Term.mkUnreachable
@@ -337,6 +357,7 @@ module Func = struct
     let cfg = Vector.empty in
     mk ~name ~entry ~cfg
 
+
   let fmt ff ({name; entry= {params; cmnd; term; sort_index}; cfg} as func)
       =
     let fmt_if cnd str ff = if cnd then Format.fprintf ff str in
@@ -363,6 +384,7 @@ module Block_id = struct
     [%compare: string * Global.t] (x.lbl, x.parent.name)
       (y.lbl, y.parent.name)
 
+
   let hash b = Hashtbl.hash (b.lbl, b.parent.name)
 end
 
@@ -442,6 +464,7 @@ let set_derived_metadata functions =
   sort_functions functions ;
   Vector.of_array functions
 
+
 let mk ~typ_defns ~globals ~functions =
   assert (
     (not
@@ -462,6 +485,7 @@ let mk ~typ_defns ~globals ~functions =
   ; globals= Vector.of_list_rev globals
   ; functions= set_derived_metadata functions }
 
+
 let fmt ff {typ_defns; globals; functions} =
   Format.fprintf ff "@[<v>@[%a@]@ @ @ @[%a@]@ @ @ @[%a@]@]"
     (list_fmt "@\n@\n" Typ.fmt_defn)

sledge/src/llair/loc.ml

@@ -15,6 +15,7 @@ let none = {dir= ""; file= ""; line= 0; col= 0}
 let mk ?(dir = none.dir) ?(file = none.file) ?(col = none.col) ~line =
   {dir; file; line; col}
 
+
 let fmt ff {dir; file; line; col} =
   Format.pp_print_string ff dir ;
   if not (String.is_empty dir) then

sledge/src/llair/typ.ml

@@ -45,6 +45,7 @@ let rec fmt ff typ =
   | Struct {name} | Opaque {name} -> Format.fprintf ff "@[%%%s@]" name
   | Bytes -> Format.fprintf ff "bytes"
 
+
 and fmts ff typs = vector_fmt ",@ " fmt ff typs
 
 let fmt_defn ff = function
@@ -54,6 +55,7 @@ let fmt_defn ff = function
   | Opaque {name} -> Format.fprintf ff "@[<2>%%%s =@ opaque@]" name
   | typ -> fmt ff typ
 
+
 let is_sized = function
   | Function _ | Bytes -> false
   | Integer _ | Float _ | Pointer _ | Array _ | Tuple _ | Struct _ -> true
@@ -62,12 +64,14 @@ let is_sized = function
          as they are not sized but may become sized through linking. *)
       true
 
+
 let rec prim_bit_size_of = function
   | Integer {bits} | Float {bits} -> Some bits
   | Array {elt; len} ->
       Option.map (prim_bit_size_of elt) ~f:(fun n -> n * len)
   | Opaque _ | Function _ | Pointer _ | Tuple _ | Struct _ | Bytes -> None
 
+
 let rec compatible t0 t1 =
   match (t0, t1, prim_bit_size_of t0, prim_bit_size_of t1) with
   | ( (Integer _ | Float _ | Pointer _)
@@ -86,11 +90,13 @@ let rec compatible t0 t1 =
       true
   | _ -> false
 
+
 let mkFunction ~return ~args =
   assert (
     Option.for_all ~f:is_sized return && Vector.for_all ~f:is_sized args ) ;
   Function {return; args}
 
+
 let mkInteger ~bits = Integer {bits}
 
 let mkFloat ~bits ~enc = Float {bits; enc}
@@ -101,12 +107,14 @@ let mkArray ~elt ~len =
   assert (is_sized elt) ;
   Array {elt; len}
 
+
 let defns : (string, t) Hashtbl.t = Hashtbl.create (module String) ()
 
 let mkTuple ~packed elts =
   assert (Vector.for_all ~f:is_sized elts) ;
   Tuple {elts; packed}
 
+
 let mkStruct ~name ~packed elt_thks =
   match Hashtbl.find defns name with
   | Some typ -> typ
@@ -124,6 +132,7 @@ let mkStruct ~name ~packed elt_thks =
           elts.(i) <- elt ) ;
       typ
 
+
 let mkOpaque ~name = Opaque {name}
 
 let mkBytes = Bytes

sledge/src/ppx_trace/ppx_trace.ml

@@ -54,6 +54,7 @@ let rec get_fun_name pat =
             (Selected_ast.To_ocaml.copy_pattern p) )
         pat
 
+
 let vb_stack_with, vb_stack_top =
   let stack = ref [] in
   let with_ x ~f =
@@ -65,6 +66,7 @@ let vb_stack_with, vb_stack_top =
   let top () = List.hd_exn !stack in
   (with_, top)
 
+
 let mapper =
   let value_binding (m : Ast_mapper.mapper) vb =
     vb_stack_with vb.pvb_pat ~f:(fun () ->
@@ -113,6 +115,7 @@ let mapper =
   in
   {Ast_mapper.default_mapper with expr; value_binding}
 
+
 let impl = Selected_ast.Ast.map_structure mapper
 
 ;;

sledge/src/sledge.ml

@@ -32,5 +32,6 @@ let main ~input ~output =
           (Caml.Printexc.to_string exn) ) ;
     Caml.Printexc.raise_with_backtrace exn bt
 
+
 ;;
 Config.run main

sledge/src/trace/trace.ml

@@ -26,6 +26,7 @@ let init ~trace_all:ta =
   Caml.at_exit flush ;
   trace_all := ta
 
+
 (* selective tracing not yet implemented *)
 let enabled _ = !trace_all
 
@@ -35,18 +36,21 @@ let info mod_name fun_name fmt =
     Format.kfprintf (fun ff -> Format.fprintf ff "@]") ff fmt )
   else Format.ifprintf ff fmt
 
+
 let incf rev_prefix name fmt =
   if enabled (name :: rev_prefix) then (
     Format.fprintf ff "@\n@[<2>@[( %s: " name ;
     Format.kfprintf (fun ff -> Format.fprintf ff "@]") ff fmt )
   else Format.ifprintf ff fmt
 
+
 let decf rev_prefix name fmt =
   if enabled (name :: rev_prefix) then (
     Format.fprintf ff "@]@\n@[<2>) %s:@ " name ;
     Format.kfprintf (fun ff -> Format.fprintf ff "@]") ff fmt )
   else Format.ifprintf ff fmt
 
+
 let call mod_name fun_name k = k (incf [mod_name] fun_name)
 
 let retn mod_name fun_name k result =