Merge branch 'master' into descendant-locksets

Author: dabund24

.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

scripts/bash-completion.sh

@@ -25,7 +25,7 @@ _goblint ()
     IFS=$'\n'
     local words cword cur
     _get_comp_words_by_ref -n = cur words cword # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
-    COMPREPLY=($(${words[0]} --complete "${words[@]:1:cword}"))
+    COMPREPLY=($(${words[0]/#\~/$HOME} --complete "${words[@]:1:cword}"))
     __ltrim_equal_completions "$cur" # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
 }
 
@@ -45,7 +45,7 @@ _regtest ()
         *)
             local words cword cur
             _get_comp_words_by_ref -n = cur words cword # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
-            COMPREPLY=($($(dirname ${words[0]})/goblint --complete "${words[@]:3:cword}"))
+            COMPREPLY=($($(dirname ${words[0]/#\~/$HOME})/goblint --complete "${words[@]:3:cword}"))
             __ltrim_equal_completions "$cur" # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
             ;;
     esac

src/analyses/base.ml

@@ -169,14 +169,27 @@ struct
 
   let iDtoIdx x = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) x (* TODO: proper castkind *)
 
+  (** Unary float predicates return non-zero for [true].
+      @see C11 7.12.3 *)
+  let fd_unary_pred = function
+    | Some true -> ID.of_excl_list IInt [Z.zero]
+    | Some false -> ID.of_int IInt Z.zero
+    | None -> ID.top_of IInt
+
+  (** Binary float predicates return one for [true].
+      @see C11 7.12.14, 6.5.8, 6.5.9 *)
+  let fd_binary_pred = function
+    | Some b -> ID.of_bool IInt b
+    | None -> ID.top_of IInt
+
   let unop_ID = function
     | Neg  -> ID.neg
     | BNot -> ID.lognot
     | LNot -> ID.c_lognot
 
   let unop_FD = function
     | Neg  -> (fun v -> (Float (FD.neg v):value))
-    | LNot -> (fun c -> Int (FD.eq c (FD.of_const (FD.get_fkind c) 0.)))
+    | LNot -> (fun c -> Int (fd_unary_pred (FD.eq c (FD.of_const (FD.get_fkind c) 0.))))
     | BNot -> failwith "BNot on a value of type float!"
 
 
@@ -256,7 +269,7 @@ struct
     | Ge -> FD.ge
     | Eq -> FD.eq
     | Ne -> FD.ne
-    | _ -> (fun _ _ -> ID.top ())
+    | _ -> (fun _ _ -> None)
 
   let is_int_returning_binop_FD = function
     | Lt | Gt | Le | Ge | Eq | Ne -> true
@@ -280,7 +293,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) ->
@@ -332,7 +345,10 @@ struct
       (* Pointer subtracted by a value (e-i) is very similar *)
       (* Cast n to the (signed) ptrdiff_ikind, then add the its negated value. *)
       | MinusPI ->
-        let n = ID.neg (ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) n) in (* TODO: proper castkind *)
+        let n = (* only speculative during ID.neg *)
+          let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+          ID.neg (ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) n) (* TODO: proper castkind *)
+        in
         Address (ad_concat_map (addToAddr n) p)
       | Mod -> Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) (* we assume that address is actually casted to int first*)
       | _ -> Address AD.top_ptr
@@ -346,7 +362,8 @@ struct
     (* For the float values, we apply the float domain operators *)
     | Float v1, Float v2 when is_int_returning_binop_FD op ->
       let result_ik = Cilfacade.get_ikind t in
-      Int (ID.cast_to ~kind:Internal result_ik (int_returning_binop_FD op v1 v2)) (* TODO: proper castkind *)
+      assert (result_ik = IInt);
+      Int (fd_binary_pred (int_returning_binop_FD op v1 v2))
     | Float v1, Float v2 -> Float (binop_FD (Cilfacade.get_fkind t) op v1 v2)
     (* For address +/- value, we try to do some elementary ptr arithmetic *)
     | Address p, Int n
@@ -929,11 +946,8 @@ struct
         Address (AD.map array_start (eval_lv ~man st lval))
       | CastE (_, t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~man st (Const (CStr (x,e))) (* TODO safe? *)
       | CastE (kind, t, exp) ->
-        (let v = eval_rv ~man st exp in
-         try
-           VD.cast ~kind ~torg:(Cilfacade.typeOf exp) t v
-         with Cilfacade.TypeOfError _  ->
-           VD.cast ~kind t v)
+        let v = eval_rv ~man st exp in
+        VD.cast ~kind t v
       | SizeOf _
       | Real _
       | Imag _
@@ -2061,7 +2075,7 @@ struct
             if not (ThreadIdDomain.Thread.is_main tid) then ( (* Only non-main return constitutes an implicit pthread_exit according to man page (https://github.com/goblint/analyzer/issues/1767#issuecomment-3642590227). *)
               (* Evaluate exp and cast the resulting value to the void-pointer-type.
                  Casting to the right type here avoids precision loss on joins. *)
-              let rv = VD.cast ~kind:Internal ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType rv in (* TODO: proper castkind *)
+              let rv = VD.cast ~kind:Internal Cil.voidPtrType rv in (* TODO: proper castkind *)
               man.sideg (V.thread tid) (G.create_thread rv)
             );
             Priv.thread_return ask (priv_getg man.global) (priv_sideg man.sideg) tid st'
@@ -2648,7 +2662,8 @@ struct
              | _, None
              | None, _ -> ID.top_of ik
              | Some mx, Some mm when Z.equal mx mm -> ID.top_of ik
-             | _, _ ->
+             | _, _ -> (* ID.neg will not overflow *)
+               let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in (* ID.neg is our internal implementation of abs *)
                let x1 = ID.neg (ID.meet (ID.ending ik Z.zero) xcast) in
                let x2 = ID.meet (ID.starting ik Z.zero) xcast in
                ID.join x1 x2
@@ -2661,11 +2676,11 @@ struct
           | Nan (fk, str) when Cil.isPointerType (Cilfacade.typeOf str) -> Float (FD.nan_of fk)
           | Nan _ -> failwith ("non-pointer argument in call to function "^f.vname)
           | Inf fk -> Float (FD.inf_of fk)
-          | Isfinite x -> Int (ID.cast_to ~kind:Internal IInt (apply_unary FDouble FD.isfinite x)) (* TODO: proper castkind *)
-          | Isinf x -> Int (ID.cast_to ~kind:Internal IInt (apply_unary FDouble FD.isinf x)) (* TODO: proper castkind *)
-          | Isnan x -> Int (ID.cast_to ~kind:Internal IInt (apply_unary FDouble FD.isnan x)) (* TODO: proper castkind *)
-          | Isnormal x -> Int (ID.cast_to ~kind:Internal IInt (apply_unary FDouble FD.isnormal x)) (* TODO: proper castkind *)
-          | Signbit x -> Int (ID.cast_to ~kind:Internal IInt (apply_unary FDouble FD.signbit x)) (* TODO: proper castkind *)
+          | Isfinite x -> Int (fd_unary_pred (apply_unary FDouble FD.isfinite x))
+          | Isinf x -> Int (fd_unary_pred (apply_unary FDouble FD.isinf x))
+          | Isnan x -> Int (fd_unary_pred (apply_unary FDouble FD.isnan x))
+          | Isnormal x -> Int (fd_unary_pred (apply_unary FDouble FD.isnormal x))
+          | Signbit x -> Int (fd_unary_pred (apply_unary FDouble FD.signbit x))
           | Ceil (fk,x) -> Float (apply_unary fk FD.ceil x)
           | Floor (fk,x) -> Float (apply_unary fk FD.floor x)
           | Fabs (fk, x) -> Float (apply_unary fk FD.fabs x)
@@ -2676,12 +2691,12 @@ struct
           | Cos (fk, x) -> Float (apply_unary fk FD.cos x)
           | Sin (fk, x) -> Float (apply_unary fk FD.sin x)
           | Tan (fk, x) -> Float (apply_unary fk FD.tan x)
-          | Isgreater (x,y) -> Int(ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.gt x y)) (* TODO: proper castkind *)
-          | Isgreaterequal (x,y) -> Int(ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.ge x y)) (* TODO: proper castkind *)
-          | Isless (x,y) -> Int(ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.lt x y)) (* TODO: proper castkind *)
-          | Islessequal (x,y) -> Int(ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.le x y)) (* TODO: proper castkind *)
-          | Islessgreater (x,y) -> Int(ID.c_logor (ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.gt x y))) (* TODO: proper castkind *)
-          | Isunordered (x,y) -> Int(ID.cast_to ~kind:Internal IInt (apply_binary FDouble FD.unordered x y)) (* TODO: proper castkind *)
+          | Isgreater (x,y) -> Int(fd_binary_pred (apply_binary FDouble FD.gt x y))
+          | Isgreaterequal (x,y) -> Int(fd_binary_pred (apply_binary FDouble FD.ge x y))
+          | Isless (x,y) -> Int(fd_binary_pred (apply_binary FDouble FD.lt x y))
+          | Islessequal (x,y) -> Int(fd_binary_pred (apply_binary FDouble FD.le x y))
+          | Islessgreater (x,y) -> Int(ID.c_logor (fd_binary_pred (apply_binary FDouble FD.lt x y)) (fd_binary_pred (apply_binary FDouble FD.gt x y)))
+          | Isunordered (x,y) -> Int(fd_binary_pred (apply_binary FDouble FD.unordered x y))
           | Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y)
           | Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y)
           | Sqrt (fk, x) -> Float (apply_unary fk FD.sqrt x)

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

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