Fix unknown thread invalidation ordering

src/analyses/apron/relationAnalysis.apron.ml

@@ -561,6 +561,8 @@ struct
           let st = invalidate_one ask man st lv in
           assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
         ) st r
+    | ThreadCreate _, _ ->
+      st (* result is invalidated by the framework after threadspawn *)
     | _, _ ->
       let st' = special_unknown_invalidate man f args in
       (* invalidate lval if present *)
@@ -677,7 +679,10 @@ struct
       let new_rel = make_callee_rel ~thread:true man fd args in
       [{st' with rel = new_rel}]
     | exception Not_found ->
-      [special_unknown_invalidate man f args]
+      (* Keep the creator state for evaluating the unknown function's arguments.
+         The framework applies its special transfer after constructing the
+         complete spawned state. *)
+      [st]
 
   let threadspawn man ~multiple lval f args fman =
     man.local

src/analyses/base.ml

@@ -1226,7 +1226,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local   = st
       ; global  = gs
-      ; spawn   = (fun ?(multiple=false) _ -> failwith "Base to_value_domain_ask should never spawn threads. What is going on?")
+      ; spawn   = (fun ?(multiple=false) ~result_lval _ -> failwith "Base to_value_domain_ask should never spawn threads. What is going on?")
       ; split   = (fun _ -> failwith "Base to_value_domain_ask trying to split paths.")
       ; sideg   = (fun g d -> failwith "Base to_value_domain_ask trying to side effect.")
       }
@@ -1996,7 +1996,7 @@ struct
        let find_fps e xs = Option.map_default (fun x -> x :: xs) xs (Addr.to_var_must e) in
        let vars = AD.fold find_fps adrs [] in (* filter_map from AD to list *)
        let funs = Seq.filter (fun x -> isFunctionType x.vtype) @@ List.to_seq vars in
-       Seq.iter (fun x -> man.spawn None x []) funs
+       Seq.iter (fun x -> man.spawn ~result_lval:None None x []) funs
      | _ -> ()
     );
     match lval with (* this section ensure global variables contain bottom values of the proper type before setting them  *)
@@ -2375,9 +2375,9 @@ struct
     in
     let forks = forkfun man lv f args in
     if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple4.second forks);
-    List.iter (fun (lval, f, args, multiple) -> man.spawn ~multiple lval f args) forks;
     let st: store = man.local in
     let desc = LF.find f in
+    List.iter (fun (lval, f, args, multiple) -> man.spawn ~multiple ~result_lval:lv lval f args) forks;
     let memory_copying dst src n =
       let dest_size = get_size_of_ptr_target man dst in
       let n_intdom = Option.map_default (fun exp -> man.ask (Queries.EvalInt exp)) `Bot n in
@@ -2697,7 +2697,7 @@ struct
       Option.map_default (fun lv -> set ~man st (eval_lv ~man st lv) (Cilfacade.typeOfLval lv) result) st lv
     (* handling thread creations *)
     | ThreadCreate _, _ ->
-      invalidate_ret_lv man.local (* actual results joined via threadspawn *)
+      man.local (* result is invalidated by the framework after threadspawn *)
     (* handling thread joins... sort of *)
     | ThreadJoin { thread = id; ret_var }, _ ->
       let st' =
@@ -2956,8 +2956,9 @@ struct
     | fd ->
       [make_entry ~thread:true man fd args]
     | exception Not_found ->
-      (* Unknown functions *)
-      let st = special_unknown_invalidate man f args in
+      (* Keep the creator state for evaluating the unknown function's arguments.
+         The framework applies its special transfer after constructing the
+         complete spawned state. *)
       [st]
 
   let threadspawn man ~multiple (lval: lval option) (f: varinfo) (args: exp list) fman: D.t =

src/analyses/mCP.ml

@@ -147,14 +147,14 @@ struct
         f ((k,v::a')::a) b
     in f [] xs
 
-  let do_spawns man (xs:(varinfo * (lval option * exp list * bool)) list) =
+  let do_spawns man (xs:(varinfo * (lval option * lval option * exp list * bool)) list) =
     let spawn_one v d =
       if get_bool "exp.single-threaded" then (
         M.msg_final Error ~category:Unsound "Thread not spawned";
         M.error ~category:Unsound "Thread not spawned from %a" CilType.Varinfo.pretty v
       )
       else
-        List.iter (fun (lval, args, multiple) -> man.spawn ~multiple lval v args) d
+        List.iter (fun (result_lval, lval, args, multiple) -> man.spawn ~multiple ~result_lval lval v args) d
     in
     iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
 
@@ -353,8 +353,8 @@ struct
 
   and outer_man tfname ?spawns ?sides ?emits man =
     let spawn = match spawns with
-      | Some spawns -> (fun ?(multiple=false) l v a  -> spawns := (v,(l,a,multiple)) :: !spawns)
-      | None -> (fun ?(multiple=false) v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
+      | Some spawns -> (fun ?(multiple=false) ~result_lval l v a  -> spawns := (v,(result_lval,l,a,multiple)) :: !spawns)
+      | None -> (fun ?(multiple=false) ~result_lval v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
     in
     let sideg = match sides with
       | Some sides -> (fun v g    -> sides  := (v, (!WideningTokenLifter.side_tokens, g)) :: !sides)

src/framework/analyses.ml

@@ -156,7 +156,7 @@ type ('d,'g,'c,'v) man =
   ; edge     : MyCFG.edge
   ; local    : 'd
   ; global   : 'v -> 'g
-  ; spawn    : ?multiple:bool -> lval option -> varinfo -> exp list -> unit
+  ; spawn    : ?multiple:bool -> result_lval:lval option -> lval option -> varinfo -> exp list -> unit
   ; split    : 'd -> Events.t list -> unit
   ; sideg    : 'v -> 'g -> unit
   }

src/framework/constraints.ml

@@ -59,7 +59,7 @@ struct
     if !AnalysisState.postsolving then
       sideg (GVar.contexts f) (G.create_contexts (G.CSet.singleton c))
 
-  let common_man var edge prev_node pval (getl:lv -> ld) sidel demandl getg sideg : (D.t, S.G.t, S.C.t, S.V.t) man * D.t list ref * (lval option * varinfo * exp list * D.t * bool) list ref =
+  let common_man var edge prev_node pval (getl:lv -> ld) sidel demandl getg sideg : (D.t, S.G.t, S.C.t, S.V.t) man * D.t list ref * (lval option * lval option * varinfo * exp list * D.t * bool) list ref =
     let r = ref [] in
     let spawns = ref [] in
     (* now watch this ... *)
@@ -77,31 +77,37 @@ struct
       ; split   = (fun (d:D.t) es -> assert (List.is_empty es); r := d::!r)
       ; sideg   = (fun g d -> sideg (GVar.spec g) (G.create_spec d))
       }
-    and spawn ?(multiple=false) lval f args =
+    and spawn ?(multiple=false) ~result_lval lval f args =
       (* TODO: adjust man node/edge? *)
       (* TODO: don't repeat for all paths that spawn same *)
       let ds = S.threadenter ~multiple man lval f args in
       List.iter (fun d ->
-          spawns := (lval, f, args, d, multiple) :: !spawns;
           match Cilfacade.find_varinfo_fundec f with
           | fd ->
+            spawns := (result_lval, lval, f, args, d, multiple) :: !spawns;
             let c = S.context man fd d in
             sidel (FunctionEntry fd, c) d;
             demandl (Function fd, c)
           | exception Not_found ->
-            (* unknown function *)
+            (* [d] is the combined child state returned by MCP threadenter,
+               so queries use the created thread's ID. *)
+            let rec special_man =
+              { man with
+                ask = (fun (type a) (q: a Queries.t) -> S.query special_man q);
+                local = d;
+                prev_node = Function dummyFunDec;
+              }
+            in
+            let d = S.special special_man None f args in
             M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname;
-            (* actual implementation (e.g. invalidation) is done by threadenter *)
-            (* must still sync for side effects, e.g., old sync-based none privatization soundness in 02-base/51-spawn-special *)
             let rec sync_man =
-              { man with
+              { special_man with
                 ask = (fun (type a) (q: a Queries.t) -> S.query sync_man q);
                 local = d;
-                prev_node = Function dummyFunDec;
               }
             in
-            (* TODO: more accurate man? *)
-            ignore (sync sync_man)
+            let d = sync sync_man in
+            spawns := (result_lval, lval, f, args, d, multiple) :: !spawns
         ) ds
     in
     (* ... nice, right! *)
@@ -124,14 +130,25 @@ struct
         }
       in
       (* TODO: don't forget path dependencies *)
-      let one_spawn (lval, f, args, fd, multiple) =
+      let one_spawn (result_lval, lval, f, args, fd, multiple) =
         let rec fman =
           { man with
             ask = (fun (type a) (q: a Queries.t) -> S.query fman q)
           ; local = fd
           }
         in
-        S.threadspawn man' ~multiple lval f args fman
+        let d = S.threadspawn man' ~multiple lval f args fman in
+        Option.map_default (fun lval ->
+            (* [threadspawn] has processed [EnterMultiThreaded], so this is an
+               ordinary creator assignment in multithreaded mode. *)
+            let rec event_man =
+              { man' with
+                ask = (fun (type a) (q: a Queries.t) -> S.query event_man q);
+                local = d;
+              }
+            in
+            S.event event_man (Events.Assign {lval; exp = MyCFG.unknown_exp}) event_man
+          ) d result_lval
       in
       bigsqcup (List.map one_spawn spawns)
 
@@ -436,7 +453,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = S.startstate Cil.dummyFunDec.svar (* bot and top both silently raise and catch Deadcode in DeadcodeLifter *)
       ; global = (fun g -> G.spec (getg (GVar.spec g)))
-      ; spawn  = (fun ?(multiple=false) v d    -> failwith "Cannot \"spawn\" in query context.")
+      ; spawn  = (fun ?(multiple=false) ~result_lval v d    -> failwith "Cannot \"spawn\" in query context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in query context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"split\" in query context.")
       }

src/framework/control.ml

@@ -311,7 +311,7 @@ struct
         ; edge    = MyCFG.Skip
         ; local   = Spec.D.top ()
         ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
-        ; spawn   = (fun ?(multiple=false) _ -> failwith "Global initializers should never spawn threads. What is going on?")
+        ; spawn   = (fun ?(multiple=false) ~result_lval _ -> failwith "Global initializers should never spawn threads. What is going on?")
         ; split   = (fun _ -> failwith "Global initializers trying to split paths.")
         ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
         }
@@ -423,7 +423,7 @@ struct
         ; edge    = MyCFG.Skip
         ; local   = st
         ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
-        ; spawn   = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+        ; spawn   = (fun ?(multiple=false) ~result_lval _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
         ; split   = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
         ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
         }
@@ -455,7 +455,7 @@ struct
         ; edge    = MyCFG.Skip
         ; local   = st
         ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
-        ; spawn   = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+        ; spawn   = (fun ?(multiple=false) ~result_lval _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
         ; split   = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
         ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
         }
@@ -482,7 +482,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local   = e
       ; global  = (fun g -> EQSys.G.spec (getg (EQSys.GVar.spec g)))
-      ; spawn   = (fun ?(multiple=false) _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
+      ; spawn   = (fun ?(multiple=false) ~result_lval _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
       ; split   = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
       ; sideg   = (fun g d -> sideg (EQSys.GVar.spec g) (EQSys.G.create_spec d))
       }

src/framework/resultQuery.ml

@@ -18,7 +18,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = local
       ; global = (fun g -> try EQSys.G.spec (GHT.find gh (EQSys.GVar.spec g)) with Not_found -> Spec.G.bot ()) (* see 29/29 on why fallback is needed *)
-      ; spawn  = (fun ?(multiple=false) v d    -> failwith "Cannot \"spawn\" in witness context.")
+      ; spawn  = (fun ?(multiple=false) ~result_lval v d    -> failwith "Cannot \"spawn\" in witness context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in witness context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"sideg\" in witness context.")
       }
@@ -37,7 +37,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = local
       ; global = (fun g -> try EQSys.G.spec (GHT.find gh (EQSys.GVar.spec g)) with Not_found -> Spec.G.bot ()) (* TODO: how can be missing? *)
-      ; spawn  = (fun ?(multiple=false) v d    -> failwith "Cannot \"spawn\" in witness context.")
+      ; spawn  = (fun ?(multiple=false) ~result_lval v d    -> failwith "Cannot \"spawn\" in witness context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in witness context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"sideg\" in witness context.")
       }
@@ -57,7 +57,7 @@ struct
       ; edge    = MyCFG.Skip
       ; local  = Spec.startstate GoblintCil.dummyFunDec.svar (* bot and top both silently raise and catch Deadcode in DeadcodeLifter *) (* TODO: is this startstate bad? *)
       ; global = (fun v -> EQSys.G.spec (try GHT.find gh (EQSys.GVar.spec v) with Not_found -> EQSys.G.bot ())) (* TODO: how can be missing? *)
-      ; spawn  = (fun ?(multiple=false) v d   -> failwith "Cannot \"spawn\" in query context.")
+      ; spawn  = (fun ?(multiple=false) ~result_lval v d   -> failwith "Cannot \"spawn\" in query context.")
       ; split  = (fun d es   -> failwith "Cannot \"split\" in query context.")
       ; sideg  = (fun v g    -> failwith "Cannot \"split\" in query context.")
       }

tests/regression/46-apron2/94-weird.t

@@ -1,19 +1,21 @@
-Check that the invariant (long long )f + 2147483648LL >= (long long )e is not confirmed, as it presumes information about f and e which are supposed to be invalidated
-  $ goblint --set dbg.level warning --disable warn.imprecise --disable warn.race --set ana.activated[+] apron --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.loop-head --disable sem.unknown_function.invalidate.globals --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.entry-types[*] invariant_set --set witness.yaml.validate 94-weird.yml 94-weird.c
+Check that the invariant (long long )f + 2147483648LL >= (long long )e is not confirmed, as it presumes information about f and e which are supposed to be invalidated. The two equality invariants check each invalidation independently.
+  $ goblint --set solvers.td3.side_widen never --set dbg.level warning --disable warn.imprecise --disable warn.race --set ana.activated[+] apron --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.loop-head --disable sem.unknown_function.invalidate.globals --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.entry-types[*] invariant_set --set witness.yaml.validate 94-weird.yml 94-weird.c
   [Error][Imprecise][Unsound] Function definition missing for b (94-weird.c:10:3-10:35)
   [Error][Imprecise][Unsound] Created a thread from unknown function b (94-weird.c:10:3-10:35)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
     total lines: 7
   [Warning][Witness] invariant unconfirmed: (long long )f + 2147483648LL >= (long long )e (94-weird.c:11:3)
+  [Warning][Witness] invariant unconfirmed: e == 0 (94-weird.c:11:3)
+  [Warning][Witness] invariant unconfirmed: f == 0 (94-weird.c:11:3)
   [Info][Witness] witness validation summary:
     confirmed: 0
-    unconfirmed: 1
+    unconfirmed: 3
     refuted: 0
     error: 0
     unchecked: 0
     unsupported: 0
     disabled: 0
-    total validation entries: 1
+    total validation entries: 3
   [Error][Imprecise][Unsound] Function definition missing

tests/regression/46-apron2/94-weird.yml

@@ -28,3 +28,21 @@
         function: main
       value: (long long )f + 2147483648LL >= (long long )e
       format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 94-weird.c
+        line: 11
+        column: 3
+        function: main
+      value: e == 0
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 94-weird.c
+        line: 11
+        column: 3
+        function: main
+      value: f == 0
+      format: c_expression

tests/regression/87-once/04-thread.t

@@ -16,4 +16,3 @@
     live: 29
     dead: 0
     total lines: 29
-  [Info][Imprecise] Invalidating expressions: & tmp (04-thread.c:31:13-31:59)