Introduce let@ binding operator

src/analyses/base.ml

@@ -274,9 +274,9 @@
       let rec addToOffset n (t:typ option) = function
         | `Index (i, `NoOffset) ->
           (* Binary operations on pointer types should not generate warnings in SV-COMP *)
-          GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
+          let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
           (* If we have arrived at the last Offset and it is an Index, we add our integer to it *)
           `Index(IdxDom.add i (iDtoIdx n), `NoOffset)
         | `Field (f, `NoOffset) ->
           (* If we have arrived at the last Offset and it is a Field,
            * then check if we're subtracting exactly its offsetof.

src/analyses/baseInvariant.ml

@@ -894,6 +894,6 @@
   let invariant man st exp tv =
     (* The computations that happen here are not computations that happen in the programs *)
     (* Any overflow during the forward evaluation will already have been flagged here *)
-    GobRef.wrap AnalysisState.executing_speculative_computations true
-    @@ fun () -> invariant man st exp tv
+    let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+    invariant man st exp tv
 end

src/analyses/basePriv.ml

@@ -2031,7 +2031,7 @@ struct
     v
 
   let dump () =
-    Out_channel.with_open_bin (get_string "exp.priv-prec-dump") @@ fun f ->
+    let@ f = Out_channel.with_open_bin (get_string "exp.priv-prec-dump") in
     (* LVH.iter (fun (l, x) v ->
         Logs.debug "%a %a = %a" CilType.Location.pretty l CilType.Varinfo.pretty x VD.pretty v
       ) lvh; *)

src/autoTune.ml

@@ -62,13 +62,13 @@
 
   method! vinst = function
     | Call (_, Lval (Var f, NoOffset), args,_,_) when LibraryFunctions.is_special f ->
-      Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo f) ~finally:Fun.id @@ fun () ->
+      let@ () = Goblint_backtrace.protect ~mark:(fun () -> Cilfacade.FunVarinfo f) ~finally:Fun.id in
       let desc = LibraryFunctions.find f in
       begin match desc.special args with
         | Malloc _
         | Alloca _ when inloop -> raise Found
         | _ -> DoChildren
       end
     | _ -> DoChildren
 end
 
@@ -96,13 +96,13 @@
 
 let findMallocWrappers () =
   let isMalloc f =
-    Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () ->
+    let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) in
     if LibraryFunctions.is_special f then
       let desc = LibraryFunctions.find f in
       let args = functionArgs f in
       GobOption.exists (fun args -> match desc.special args with Malloc _ -> true | _ -> false) args
     else
       false
   in
   (ResettableLazy.force functionCallMaps).calling
   |> FunctionCallMap.filter (fun _ allCalled -> FunctionSet.exists isMalloc allCalled)
@@ -177,25 +177,25 @@
 
 let hasFunction pred =
   let relevant_static var =
-    Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () ->
+    let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) in
     if LibraryFunctions.is_special var then
       let desc = LibraryFunctions.find var in
       GobOption.exists (fun args -> pred desc args) (functionArgs var)
     else
       false
   in
   let relevant_dynamic var =
-    Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () ->
+    let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) in
     if LibraryFunctions.is_special var then
       let desc = LibraryFunctions.find var in
       (* We don't really have arguments at hand, so we cheat and just feed it a list of MyCFG.unknown_exp of appropriate length *)
       match unrollType var.vtype with
       | TFun (_, args, _, _) ->
         let args = BatOption.map_default (List.map (fun (x,_,_) -> MyCFG.unknown_exp)) [] args in
         pred desc args
       | _ -> false
     else
       false
   in
   let calls = ResettableLazy.force functionCallMaps in
   calls.calledBy |> FunctionCallMap.exists (fun var _ -> relevant_static var) ||

src/cdomain/value/cdomains/offset.ml

@@ -217,7 +217,8 @@
         (* Interval of floor and ceil division in case bitfield offset. *)
         let bytes_offset = Idx.of_interval (Cilfacade.ptrdiff_ikind ()) Z.(fdiv bits_offset eight, cdiv bits_offset eight) in
         let remaining_offset = offset_to_index_offset ~typ:field.ftype o in
-        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bytes_offset remaining_offset
+        let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+        Idx.add bytes_offset remaining_offset
       | `Index (x, o) ->
         let (item_typ, item_size_in_bytes) =
           match Option.map unrollType typ with
@@ -228,9 +229,13 @@
             (None, Idx.top ())
         in
         (* Binary operations on offsets should not generate overflow warnings in SV-COMP *)
-        let bytes_offset = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.mul item_size_in_bytes x in
+        let bytes_offset =
+          let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+          Idx.mul item_size_in_bytes x
+        in
         let remaining_offset = offset_to_index_offset ?typ:item_typ o in
-        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bytes_offset remaining_offset
+        let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+        Idx.add bytes_offset remaining_offset
     in
     offset_to_index_offset ?typ offs
 

src/cdomain/value/util/wideningThresholds.ml

@@ -115,15 +115,15 @@
   method! vinst (i: instr) =
     match i with
     | Call (_, Lval (Var f, NoOffset), args, _, _) when LibraryFunctions.is_special f ->
-      Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () ->
+      let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) in
       let desc = LibraryFunctions.find f in
       begin match desc.special args with
         | Assert { exp; _ } ->
           EH.replace exps exp ();
           DoChildren
         | _ ->
           DoChildren
       end
     | _ ->
       DoChildren
 

src/cdomains/apron/sharedFunctions.apron.ml

@@ -153,12 +153,12 @@
                   outside of the apron-related expression conversion.
               *)
               let simplify e =
-                GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
+                let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
                 let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a))   in
                 let simp = query e ikind in
                 let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ikind simp in
                 if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty simp;
                 BatOption.map_default (fun c -> Const (CInt (c, ikind, None))) e const
               in
               let texpr1 e = texpr1_expr_of_cil_exp (simplify e) in
               let bop_near op e1 e2 =  Binop (op, texpr1 e1, texpr1 e2, Int, Near) in
@@ -177,11 +177,13 @@
                   | false -> (* Cast is not injective - we now try to establish suitable ranges manually  *)
                     let t_ik = Cilfacade.get_ikind t in
                     (* retrieving a valuerange for a non-injective cast works by a query to the value-domain with subsequent value extraction from domtuple - which should be speculative, since it is not program code *)
-                    let const,res = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
+                    let const,res =
+                      let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
                       (* try to evaluate e by EvalInt Query *)
                       let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a))  in
                       (* convert response to a constant *)
-                      IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res, res in
+                      IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res, res
+                    in
                     match const with
                     | Some c -> Cst (Coeff.s_of_z c) (* Got a constant value -> use it straight away *)
                     (* I gotten top, we can not guarantee injectivity *)

src/common/framework/cfgTools.ml

@@ -600,7 +600,7 @@ let fprint_hash_dot cfg  =
     let extraNodeStyles node = []
   end
   in
-  Out_channel.with_open_text "cfg.dot" @@ fun out ->
+  let@ out = Out_channel.with_open_text "cfg.dot" in
   let iter_edges f = H.iter (fun n es -> List.iter (f n) es) cfg in
   let ppf = Format.formatter_of_out_channel out in
   fprint_dot (module CfgPrinters (NoExtraNodeStyles)) iter_edges ppf;
@@ -663,7 +663,7 @@ let dead_code_cfg ~path (module FileCfg: MyCFG.FileCfg) live =
         let dot_file_name = fd.svar.vname^".dot" in
         let file_dir = GobSys.mkdir_or_exists_absolute Fpath.(base_dir / c_file_name) in
         let fname = Fpath.(file_dir / dot_file_name) in
-        Out_channel.with_open_text (Fpath.to_string fname) @@ fun out ->
+        let@ out = Out_channel.with_open_text (Fpath.to_string fname) in
         let ppf = Format.formatter_of_out_channel out in
         fprint_fundec_html_dot (module FileCfg.Cfg) live fd ppf;
         Format.pp_print_flush ppf ();

src/incremental/serialize.ml

@@ -20,7 +20,7 @@ let gob_results_dir op =
 let server () = GobConfig.get_bool "server.enabled"
 
 let marshal obj fileName  =
-  Out_channel.with_open_bin (Fpath.to_string fileName) @@ fun chan ->
+  let@ chan = Out_channel.with_open_bin (Fpath.to_string fileName) in
   Marshal.to_channel chan obj []
 
 let unmarshal fileName =

src/solver/sLR.ml

@@ -481,7 +481,7 @@ module PrintInfluence =
   struct
     module S1 = Sol (S) (HM)
     let solve x y =
-      Out_channel.with_open_text "test.dot" @@ fun ch ->
+      let@ ch = Out_channel.with_open_text "test.dot" in
       let r = S1.solve x y in
       let f k _ =
         let q = if HM.mem S1.wpoint k then " shape=box style=rounded" else "" in

src/transform/deadCode.ml

@@ -174,12 +174,12 @@
        the main function(s). Dead functions and globals are removed, since there is no
        chain of syntactic references to them from the main function(s). *)
     let open GoblintCil.RmUnused in
-    GobRef.wrap keepUnused false @@ fun () ->
+    let@ () = GobRef.wrap keepUnused false in
     removeUnused
       ~isRoot:(function
           | GFun (fd, _) -> List.mem fd.svar.vname (get_string_list "mainfun")
           | _ -> false)
       file
 
   let name = "remove_dead_code"
 

src/transform/evalAssert.ml

@@ -44,11 +44,11 @@
       let is_lock exp args =
         match exp with
         | Lval(Var v,_) when LibraryFunctions.is_special v ->
-          Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo v) @@ fun () ->
+          let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo v) in
           let desc = LibraryFunctions.find v in
           (match desc.special args with
            | Lock _ -> true
            | _ -> false)
         | _ -> false
       in
 

src/transform/transform.ml

@@ -37,9 +37,9 @@
 
   if file_output && List.exists (fun (_, (module T : S)) -> T.requires_file_output) active_transformations then
     let filename = GobConfig.get_string "trans.output" in
-    Out_channel.with_open_text filename @@ fun oc ->
-    GobRef.wrap GoblintCil.lineDirectiveStyle None @@ fun () ->
+    let@ oc = Out_channel.with_open_text filename in
+    let@ () = GobRef.wrap GoblintCil.lineDirectiveStyle None in
     dumpFile defaultCilPrinter oc filename file
 
 let run file name = run_transformations ~file_output:false file [name]
 

src/util/std/gobFun.ml

@@ -0,0 +1,5 @@
+module Syntax =
+struct
+  let (let@) f x = f x
+  (** [let@ x = f in e] is [f @@ fun x -> e]. *)
+end

src/util/std/goblint_std.ml

@@ -5,6 +5,7 @@
     OCaml standard library extensions which are not provided by {!Batteries}. *)
 
 module GobArray = GobArray
+module GobFun = GobFun
 module GobGc = GobGc
 module GobHashtbl = GobHashtbl
 module GobList = GobList
@@ -15,6 +16,8 @@ module GobSys = GobSys
 module GobUnix = GobUnix
 module GobTuple = GobTuple
 
+include GobFun.Syntax
+
 (** {1 Other libraries}
 
     External library extensions. *)

src/witness/witnessUtil.ml

@@ -63,12 +63,12 @@
         List.exists (fun (_, edge) ->
             match edge with
             | Proc (_, Lval (Var fv, NoOffset), args) when LibraryFunctions.is_special fv ->
-              Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo fv) @@ fun () ->
+              let@ () = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo fv) in
               let desc = LibraryFunctions.find fv in
               begin match desc.special args with
                 | Lock _ -> true
                 | _ -> false
               end
             | _ -> false
           ) edges
       ) (Cfg.prev to_node)

tests/regression/cfg/util/cfgDot.ml

@@ -87,7 +87,7 @@ let main () =
 
   GoblintCil.iterGlobals ast (function
       | GFun (fd, _) ->
-        Out_channel.with_open_text (fd.svar.vname ^ ".dot") @@ fun out ->
+        let@ out = Out_channel.with_open_text (fd.svar.vname ^ ".dot") in
         let iter_edges = CfgTools.iter_fd_edges (module Cfg) fd in
         let ppf = Format.formatter_of_out_channel out in
         CfgTools.fprint_dot (module CfgTools.CfgPrinters (LocationExtraNodeStyles)) iter_edges ppf;

tests/regression/cfg/util/dune

@@ -2,8 +2,10 @@
  (name cfgDot)
  (libraries
    goblint-cil
+   goblint_std
    goblint_logs
    goblint_common
    goblint_lib ; TODO: avoid: extract LoopUnrolling and WitnessUtil node predicates from goblint_lib
    fpath)
+ (flags :standard -open Goblint_std)
  (preprocess (pps ppx_deriving.std)))