Fix unknown thread invalidation ordering

src/analyses/apron/relationAnalysis.apron.ml

@@ -675,10 +675,22 @@ 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]
+      [Priv.threadenter (Analyses.ask_of_man man) man.global st]
 
   let threadspawn man ~multiple lval f args fman =
-    man.local
+    match Cilfacade.find_varinfo_fundec f with
+    | _ -> man.local
+    | exception Not_found ->
+      (* [man.local] already contains the invalidated thread-create result.
+         Add the unknown thread's invalidations to that same state. When this is
+         the first spawn, publish the combined state as the initialization
+         snapshot; later spawns use ordinary privatized writes. *)
+      let st = special_unknown_invalidate man f args in
+      let ask = Analyses.ask_of_man man in
+      if ThreadFlag.has_ever_been_multi ask then
+        st
+      else
+        Priv.enter_multithreaded ask man.global man.sideg st
 
   let event man e oman =
     let ask = Analyses.ask_of_man man in

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