Merge remote-tracking branch 'upstream/master'

.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

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/autoTune.ml

@@ -157,7 +157,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 +169,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 +191,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 (
@@ -446,7 +447,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

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

src/config/options.schema.json

@@ -1544,6 +1544,19 @@
             }
           },
           "additionalProperties": false
+        },
+        "atexit": {
+          "title": "sem.atexit",
+          "type": "object",
+          "properties": {
+            "ignore": {
+              "title": "sem.atexit.ignore",
+              "description": "Ignore atexit callbacks (unsound).",
+              "type": "boolean",
+              "default": false
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false

src/domain/partitionDomain.ml

@@ -31,10 +31,10 @@ struct
   let meet _ _ = failwith "PartitonDomain.Set.meet: unsound"
 
   let collapse (s1:t) (s2:t): bool =
-    let f vf2 res =
-      res || exists (fun vf1 -> S.collapse vf1 vf2) s1
+    let f vf2 =
+      exists (fun vf1 -> S.collapse vf1 vf2) s1
     in
-    fold f s2 false
+    exists f s2
 
   let add e s = join s (singleton e)
 

src/incremental/compareCFG.ml

@@ -131,7 +131,7 @@ let reexamine f1 f2 (same : biDirectionNodeMap) (diffNodes1 : unit NH.t) (module
           false
         end in
     let cond n2 = Node.equal n2 (FunctionEntry f2) || check_all_nodes_in_same (List.map snd (CfgNew.prev n2)) n2 in
-    let forall = NH.fold (fun n2 n1 acc -> acc && cond n2) same.node2to1 true in
+    let forall = NH.fold (fun n2 n1 acc -> acc && cond n2) same.node2to1 true in (* nosemgrep: fold-for_all *) (* cond does side effects *)
     if not forall then repeat () in
   repeat ();
   NH.to_seq same.node1to2, NH.to_seq_keys diffNodes1

src/solver/td3.ml

@@ -49,7 +49,7 @@ module Base =
     open SolverBox.Warrow (S.Dom)
     include Generic.SolverStats (S) (HM)
     module VS = Set.Make (S.Var)
-    let exists_key f hm = HM.fold (fun k _ a -> a || f k) hm false
+    let exists_key f hm = HM.exists (fun k _ -> f k) hm
 
     type solver_data = {
       st: (S.Var.t * S.Dom.t) list; (* needed to destabilize start functions if their start state changed because of some changed global initializer *)
@@ -289,7 +289,7 @@ module Base =
               destabilize_vs y || b || was_stable && List.mem_cmp S.Var.compare y vs
             else
               true
-          ) w false
+          ) w false (* nosemgrep: fold-exists *) (* does side effects *)
       and solve ?reuse_eq x phase =
         if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x);
         init x;

src/util/autoSoundConfig.ml

@@ -12,8 +12,8 @@ let enableSpecAnalyses spec analyses =
   Logs.info "Specification: %s -> enabling soundness analyses \"%s\"" (Svcomp.Specification.to_string [spec]) (String.concat ", " analyses);
   enableAnalyses analyses
 
-let enableOptions options = 
-  let enableOpt option = 
+let enableOptions options =
+  let enableOpt option =
     Logs.info "Setting \"%s\" to true" option;
     set_bool option true
   in
@@ -60,7 +60,8 @@ let enableAnalysesForSpecification () =
 let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceSetjmp"; "poisonVariables"; "expsplit"; "vla"]
 
 let activateLongjmpAnalysesWhenRequired () =
-  let isLongjmp = function
+  let isLongjmp (desc: LibraryDesc.t) args =
+    match desc.special args with
     | LibraryDesc.Longjmp _ -> true
     | _ -> false
   in

src/util/library/libraryDesc.ml

@@ -56,6 +56,7 @@ type special =
   | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool }
   | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
   | ThreadExit of { ret_val: Cil.exp; }
+  | ThreadSelf
   | Globalize of Cil.exp
   | Signal of Cil.exp
   | Broadcast of Cil.exp

src/util/library/libraryDsl.ml

@@ -30,8 +30,20 @@ struct
     | [] -> fail "^::"
 end
 
+type access =
+  | Access of LibraryDesc.Access.t
+  | If of (unit -> bool) * access
+
+let rec eval_access = function
+  | Access acc -> Some acc
+  | If (p, access) ->
+    if p () then
+      eval_access access
+    else
+      None
+
 type ('k, 'l, 'r) arg_desc = {
-  accesses: Access.t list;
+  accesses: access list;
   match_arg: (Cil.exp, 'k, 'r) Pattern.t;
   match_var_args: (Cil.exp list, 'l, 'r) Pattern.t;
 }
@@ -51,15 +63,21 @@ let rec accs: type k r. (k, r) args_desc -> Accesses.t = fun args_desc args ->
   match args_desc, args with
   | [], [] -> []
   | VarArgs arg_desc, args ->
-    List.map (fun acc ->
-        (acc, args)
+    List.filter_map (fun access ->
+        match eval_access access with
+        | Some acc -> Some (acc, args)
+        | None -> None
       ) arg_desc.accesses
   | arg_desc :: args_desc, arg :: args ->
     let accs'' = accs args_desc args in
-    List.fold_left (fun (accs'': (Access.t * Cil.exp list) list) (acc: Access.t) ->
-        match List.assoc_opt acc accs'' with
-        | Some args -> (acc, arg :: args) :: List.remove_assoc acc accs''
-        | None -> (acc, [arg]) :: accs''
+    List.fold_left (fun (accs'': (Access.t * Cil.exp list) list) (access: access) ->
+        match eval_access access with
+        | Some acc ->
+          begin match List.assoc_opt acc accs'' with
+            | Some args -> (acc, arg :: args) :: List.remove_assoc acc accs''
+            | None -> (acc, [arg]) :: accs''
+          end
+        | None -> accs''
       ) accs'' arg_desc.accesses
   | _, _ -> invalid_arg "accs"
 
@@ -94,13 +112,15 @@ let drop (_name: string) accesses = { empty_drop_desc with accesses; }
 let drop' accesses = { empty_drop_desc with accesses; }
 
 
-let r = Access.{ kind = Read; deep = false; }
-let r_deep = Access.{ kind = Read; deep = true; }
-let w = Access.{ kind = Write; deep = false; }
-let w_deep = Access.{ kind = Write; deep = true; }
-let f = Access.{ kind = Free; deep = false; }
-let f_deep = Access.{ kind = Free; deep = true; }
-let s = Access.{ kind = Spawn; deep = false; }
-let s_deep = Access.{ kind = Spawn; deep = true; }
-let c = Access.{ kind = Spawn; deep = false; } (* TODO: Sound, but very imprecise hack for calls to function pointers given as arguments. *)
-let c_deep = Access.{ kind = Spawn; deep = true; }
+let r = Access { kind = Read; deep = false; }
+let r_deep = Access { kind = Read; deep = true; }
+let w = Access { kind = Write; deep = false; }
+let w_deep = Access { kind = Write; deep = true; }
+let f = Access { kind = Free; deep = false; }
+let f_deep = Access { kind = Free; deep = true; }
+let s = Access { kind = Spawn; deep = false; }
+let s_deep = Access { kind = Spawn; deep = true; }
+let c = Access { kind = Spawn; deep = false; } (* TODO: Sound, but very imprecise hack for calls to function pointers given as arguments. *)
+let c_deep = Access { kind = Spawn; deep = true; }
+
+let if_ p access = If (p, access)