Merge branch 'master' into svcomp25-dev

.semgrep/fold.yml

@@ -0,0 +1,26 @@
+rules:
+  - id: fold-exists
+    patterns:
+      - pattern-either:
+        - pattern: $D.fold ... false
+        - pattern: $D.fold_left ... false
+        - pattern: $D.fold_right ... false
+        - pattern: fold ... false
+        - pattern: fold_left ... false
+        - pattern: fold_right ... false
+    message: consider replacing fold with exists
+    languages: [ocaml]
+    severity: WARNING
+
+  - id: fold-for_all
+    patterns:
+      - pattern-either:
+        - pattern: $D.fold ... true
+        - pattern: $D.fold_left ... true
+        - pattern: $D.fold_right ... true
+        - pattern: fold ... true
+        - pattern: fold_left ... true
+        - pattern: fold_right ... true
+    message: consider replacing fold with for_all
+    languages: [ocaml]
+    severity: WARNING

.semgrep/tracing.yml

@@ -8,8 +8,16 @@ rules:
         - pattern: Messages.tracec
         - pattern: Messages.traceu
         - pattern: Messages.traceli
+        - pattern: M.trace
+        - pattern: M.tracel
+        - pattern: M.tracei
+        - pattern: M.tracec
+        - pattern: M.traceu
+        - pattern: M.traceli
       - pattern-not-inside: if Messages.tracing then ...
       - pattern-not-inside: if Messages.tracing && ... then ...
+      - pattern-not-inside: if M.tracing then ...
+      - pattern-not-inside: if M.tracing && ... then ...
     message: trace functions should only be called if tracing is enabled at compile time
     languages: [ocaml]
     severity: WARNING

conf/svcomp-validate.json

@@ -68,6 +68,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]

conf/svcomp.json

@@ -67,6 +67,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]

conf/svcomp25-validate.json

@@ -68,6 +68,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]

conf/svcomp25.json

@@ -67,6 +67,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]

src/analyses/base.ml

@@ -2172,11 +2172,7 @@ struct
         in
         List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
       end
-    | _, _ when get_bool "sem.unknown_function.spawn" ->
-      (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
-         But here we consider all non-ThreadCreate functions also unknown, so old-style LibraryFunctions access
-         definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions).
-         Need this to not have memmove spawn in SV-COMP. *)
+    | _, _ ->
       let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in
       let deep_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = true } args in
       let shallow_flist = collect_invalidate ~deep:false ~ctx ctx.local shallow_args in
@@ -2185,7 +2181,6 @@ struct
       let addrs = List.concat_map AD.to_var_may flist in
       if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
       List.filter_map (create_thread ~multiple:true None None) addrs
-    | _, _ -> []
 
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)
@@ -2656,6 +2651,15 @@ struct
     | Unknown, "__goblint_assume_join" ->
       let id = List.hd args in
       Priv.thread_join ~force:true (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st
+    | ThreadSelf, _ ->
+      begin match lv, ThreadId.get_current (Analyses.ask_of_ctx ctx) with
+        | Some lv, `Lifted tid ->
+          set ~ctx st (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Thread (ValueDomain.Threads.singleton tid))
+        | Some lv, _ ->
+          invalidate_ret_lv st
+        | None, _ ->
+          st
+      end
     | Alloca size, _ -> begin
         match lv with
         | Some lv ->

src/analyses/basePriv.ml

@@ -1040,11 +1040,11 @@ struct
     let s = MustLockset.remove m (current_lockset ask) in
     let t = current_thread ask in
     let side_cpa = CPA.filter (fun x _ ->
-        GWeak.fold (fun s' tm acc ->
+        GWeak.exists (fun s' tm ->
             (* TODO: swap 2^M and T partitioning for lookup by t here first? *)
             let v = ThreadMap.find t tm in
-            (MustLockset.mem m s' && not (VD.is_bot v)) || acc
-          ) (G.weak (getg (V.global x))) false
+            (MustLockset.mem m s' && not (VD.is_bot v))
+          ) (G.weak (getg (V.global x)))
       ) st.cpa
     in
     sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
@@ -1098,9 +1098,9 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let s = MustLockset.remove m (current_lockset ask) in
     let side_cpa = CPA.filter (fun x _ ->
-        GWeak.fold (fun s' v acc ->
-            (MustLockset.mem m s' && not (VD.is_bot v)) || acc
-          ) (G.weak (getg (V.global x))) false
+        GWeak.exists (fun s' v ->
+            (MustLockset.mem m s' && not (VD.is_bot v))
+          ) (G.weak (getg (V.global x)))
       ) st.cpa
     in
     sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));

src/analyses/threadAnalysis.ml

@@ -95,9 +95,7 @@ struct
   let startstate v = D.bot ()
 
   let threadenter ctx ~multiple lval f args =
-    if multiple then
-      (let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in
-       ctx.sideg tid (true, TS.bot (), false));
+    (* ctx is of creator, side-effects to denote non-uniqueness are performed in threadspawn *)
     [D.bot ()]
 
   let threadspawn ctx ~multiple lval f args fctx =
@@ -106,9 +104,9 @@ struct
     let repeated = D.mem tid ctx.local in
     let eff =
       match creator with
-      | `Lifted ctid -> (repeated, TS.singleton ctid, false)
-      | `Top         -> (true,     TS.bot (),         false)
-      | `Bot         -> (false,    TS.bot (),         false)
+      | `Lifted ctid -> (repeated || multiple, TS.singleton ctid, false)
+      | `Top         -> (true, TS.bot (), false)
+      | `Bot         -> (multiple, TS.bot (), false)
     in
     ctx.sideg tid eff;
     D.join ctx.local (D.singleton tid)

src/autoTune.ml

@@ -44,6 +44,34 @@ class functionVisitor(calling, calledBy, argLists, dynamicallyCalled) = object
     DoChildren
 end
 
+exception Found
+class findAllocsInLoops = object
+  inherit nopCilVisitor
+
+  val mutable inloop = false
+
+  method! vstmt stmt =
+    let outOfLoop stmt =
+      match stmt.skind with
+      | Loop _ -> inloop <- false; stmt
+      | _ -> stmt
+    in
+    match stmt.skind with
+    | Loop _ -> inloop <- true; ChangeDoChildrenPost(stmt, outOfLoop)
+    | _ -> DoChildren
+
+  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 desc = LibraryFunctions.find f in
+      begin match desc.special args with
+        | Malloc _
+        | Alloca _ when inloop -> raise Found
+        | _ -> DoChildren
+      end
+    | _ -> DoChildren
+end
+
 type functionCallMaps = {
   calling: FunctionSet.t FunctionCallMap.t;
   calledBy: (FunctionSet.t * int) FunctionCallMap.t;
@@ -157,7 +185,7 @@ let hasFunction pred =
     Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () ->
     if LibraryFunctions.is_special var then
       let desc = LibraryFunctions.find var in
-      GobOption.exists (fun args -> pred (desc.special args)) (functionArgs var)
+      GobOption.exists (fun args -> pred desc args) (functionArgs var)
     else
       false
   in
@@ -169,7 +197,7 @@ let hasFunction pred =
       match unrollType var.vtype with
       | TFun (_, args, _, _) ->
         let args = BatOption.map_default (List.map (fun (x,_,_) -> MyCFG.unknown_exp)) [] args in
-        pred (desc.special args)
+        pred desc args
       | _ -> false
     else
       false
@@ -191,9 +219,10 @@ let enableAnalyses anas =
 
 let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"]
 let reduceThreadAnalyses () =
-  let isThreadCreate = function
+  let isThreadCreate (desc: LibraryDesc.t) args =
+    match desc.special args with
     | LibraryDesc.ThreadCreate _ -> true
-    | _ -> false
+    | _ -> LibraryDesc.Accesses.find_kind desc.accs Spawn args <> []
   in
   let hasThreadCreate = hasFunction isThreadCreate in
   if not @@ hasThreadCreate then (
@@ -229,18 +258,28 @@ let focusOnTermination (spec: Svcomp.Specification.t) =
 let focusOnTermination () =
   List.iter focusOnTermination (Svcomp.Specification.of_option ())
 
-let focusOnSpecification (spec: Svcomp.Specification.t) =
+let concurrencySafety (spec: Svcomp.Specification.t) =
   match spec with
-  | UnreachCall s -> ()
   | NoDataRace -> (*enable all thread analyses*)
     Logs.info "Specification: NoDataRace -> enabling thread analyses \"%s\"" (String.concat ", " notNeccessaryThreadAnalyses);
     enableAnalyses notNeccessaryThreadAnalyses;
-  | NoOverflow -> (*We focus on integer analysis*)
-    set_bool "ana.int.def_exc" true
   | _ -> ()
 
-let focusOnSpecification () =
-  List.iter focusOnSpecification (Svcomp.Specification.of_option ())
+let noOverflows (spec: Svcomp.Specification.t) =
+  match spec with
+  | NoOverflow ->
+    (*We focus on integer analysis*)
+    set_bool "ana.int.def_exc" true;
+    begin
+      try
+        ignore @@ visitCilFileSameGlobals (new findAllocsInLoops) (!Cilfacade.current_file);
+        set_int "ana.malloc.unique_address_count" 1
+      with Found -> set_int "ana.malloc.unique_address_count" 0;
+    end
+  | _ -> ()
+
+let focusOn (f : SvcompSpec.t -> unit) =
+  List.iter f (Svcomp.Specification.of_option ())
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
@@ -446,7 +485,8 @@ let wideningOption factors file =
   }
 
 let activateTmpSpecialAnalysis () =
-  let isMathFun = function
+  let isMathFun (desc: LibraryDesc.t) args =
+    match desc.special args with
     | LibraryDesc.Math _ -> true
     | _ -> false
   in
@@ -487,15 +527,6 @@ let isActivated a = get_bool "ana.autotune.enabled" && List.mem a @@ get_string_
 
 let isTerminationTask () = List.mem Svcomp.Specification.Termination (Svcomp.Specification.of_option ())
 
-let specificationIsActivated () =
-  isActivated "specification" && get_string "ana.specification" <> ""
-
-let specificationTerminationIsActivated () =
-  isActivated "termination"
-
-let specificationMemSafetyIsActivated () =
-  isActivated "memsafetySpecification"
-
 let chooseConfig file =
   let factors = collectFactors visitCilFileSameGlobals file in
   let fileCompplexity = estimateComplexity factors file in
@@ -515,8 +546,9 @@ let chooseConfig file =
   if isActivated "mallocWrappers" then
     findMallocWrappers ();
 
-  if specificationIsActivated () then
-    focusOnSpecification ();
+  if isActivated "concurrencySafetySpecification" then focusOn concurrencySafety;
+
+  if isActivated "noOverflows" then focusOn noOverflows;
 
   if isActivated "enums" && hasEnums file then
     set_bool "ana.int.enums" true;

src/cdomain/value/cdomains/stringDomain.ml

@@ -20,12 +20,12 @@ let reset_lazy () =
 
 
 type t = string option [@@deriving eq, ord, hash]
+(** [None] means top. *)
 
 let hash x =
-  if get_string_domain () = Disjoint then
-    hash x
-  else
-    13859
+  match get_string_domain () with
+  | Disjoint | Flat -> hash x
+  | Unit -> 13859
 
 let show = function
   | Some x -> "\"" ^ x ^ "\""
@@ -39,10 +39,9 @@ include Printable.SimpleShow (
   )
 
 let of_string x =
-  if get_string_domain () = Unit then
-    None
-  else
-    Some x
+  match get_string_domain () with
+  | Unit -> None
+  | Disjoint | Flat -> Some x
 let to_string x = x
 
 (* only keep part before first null byte *)
@@ -91,24 +90,25 @@ let join x y =
   | _, None -> None
   | Some a, Some b when a = b -> Some a
   | Some a, Some b (* when a <> b *) ->
-    if get_string_domain () = Disjoint then
-      raise Lattice.Uncomparable
-    else
-      None
+    match get_string_domain () with
+    | Disjoint -> raise Lattice.Uncomparable
+    | Flat -> None
+    | Unit -> assert false
 
 let meet x y =
   match x, y with
   | None, a
   | a, None -> a
   | Some a, Some b when a = b -> Some a
   | Some a, Some b (* when a <> b *) ->
-    if get_string_domain () = Disjoint then
-      raise Lattice.Uncomparable
-    else
-      raise Lattice.BotValue
+    match get_string_domain () with
+    | Disjoint -> raise Lattice.Uncomparable
+    | Flat -> raise Lattice.BotValue
+    | Unit -> assert false
 
 let repr x =
-  if get_string_domain () = Disjoint then
+  match get_string_domain () with
+  | Disjoint ->
     x (* everything else is kept separate, including strings if not limited *)
-  else
+  | Flat | Unit ->
     None (* all strings together if limited *)

src/cdomain/value/cdomains/threadIdDomain.ml

@@ -83,10 +83,10 @@ struct
       (v, None)
 
   let is_main = function
-    | ({vname; _}, None) -> List.mem vname @@ GobConfig.get_string_list "mainfun"
+    | ({vname; _}, None) -> GobConfig.get_bool "ana.thread.include-node" && List.mem vname @@ GobConfig.get_string_list "mainfun"
     | _ -> false
 
-  let is_unique _ = false (* TODO: should this consider main unique? *)
+  let is_unique = is_main
   let may_create _ _ = true
   let is_must_parent _ _ = false
 end