Merge pull request #1891 from goblint/let-at

sim642 · web-flow · commit 2326a8472e00 · 2026-01-12T10:58:50.000+02:00
Introduce `let@` binding operator
diff --git a/.semgrep/let.yml b/.semgrep/let.yml
@@ -1,6 +1,8 @@
 rules:
-  - id: let-unit-in
-    pattern: let () = $E in ...
-    message: use ; instead (and, if needed, add surrounding parentheses to preserve precedence)
-    languages: [ocaml]
-    severity: WARNING
+  []
+  # TODO: disabled because semgrep cannot distinguish from let@ which is fine (https://github.com/semgrep/semgrep/issues/11432)
+  # - id: let-unit-in
+  #   pattern: let () = $E in ...
+  #   message: use ; instead (and, if needed, add surrounding parentheses to preserve precedence)
+  #   languages: [ocaml]
+  #   severity: WARNING
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -280,7 +280,7 @@ struct
       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) ->
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
@@ -890,6 +890,6 @@ struct
   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
diff --git a/src/analyses/basePriv.ml b/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; *)
diff --git a/src/autoTune.ml b/src/autoTune.ml
@@ -62,7 +62,7 @@ class findAllocsInLoops = object
 
   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 _
@@ -96,7 +96,7 @@ let functionArgs fd = (ResettableLazy.force functionCallMaps).argLists |> Functi
 
 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
@@ -177,15 +177,15 @@ let disableIntervalContextsInRecursiveFunctions () =
 
 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 *)
diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml
@@ -224,7 +224,8 @@ struct
         (* 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
@@ -235,9 +236,13 @@ struct
             (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
 
diff --git a/src/cdomain/value/util/wideningThresholds.ml b/src/cdomain/value/util/wideningThresholds.ml
@@ -115,7 +115,7 @@ class extractInvariantsVisitor (exps) = object
   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; _ } ->
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -157,7 +157,7 @@ struct
                   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 ~kind:Internal ikind simp in (* TODO: proper castkind *)
@@ -181,11 +181,13 @@ struct
                   | 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 ~kind:Internal t_ik res, res in (* TODO: proper castkind *)
+                      IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ~kind:Internal t_ik res, res (* TODO: proper castkind *)
+                    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 *)
diff --git a/src/common/framework/cfgTools.ml b/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 ();
diff --git a/src/incremental/serialize.ml b/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 =
diff --git a/src/solver/sLR.ml b/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
diff --git a/src/transform/deadCode.ml b/src/transform/deadCode.ml
@@ -174,7 +174,7 @@ module RemoveDeadCode : Transform.S = struct
        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")
diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
@@ -44,7 +44,7 @@ struct
       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
diff --git a/src/transform/transform.ml b/src/transform/transform.ml
@@ -37,8 +37,8 @@ let run_transformations ?(file_output = true) file names ask =
 
   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]
diff --git a/src/util/std/gobFun.ml b/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
diff --git a/src/util/std/goblint_std.ml b/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. *)
diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml
@@ -63,7 +63,7 @@ struct
         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
diff --git a/tests/regression/cfg/util/cfgDot.ml b/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;
diff --git a/tests/regression/cfg/util/dune b/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)))

Original file line number	Diff line number	Diff line change
`@@ -2031,7 +2031,7 @@ struct`
`2031`	`2031`	`v`
`2032`	`2032`
`2033`	`2033`	`let dump () =`
`2034`		`- Out_channel.with_open_bin (get_string "exp.priv-prec-dump") @@ fun f ->`
	`2034`	`+ let@ f = Out_channel.with_open_bin (get_string "exp.priv-prec-dump") in`
`2035`	`2035`	`(* LVH.iter (fun (l, x) v ->`
`2036`	`2036`	`Logs.debug "%a %a = %a" CilType.Location.pretty l CilType.Varinfo.pretty x VD.pretty v`
`2037`	`2037`	`) lvh; *)`