Merge pull request #1646 from goblint/issue_1535

michael-schwarz · web-flow · commit d81fcc46f37d · 2025-07-17T16:39:51.000+02:00
Relational: Use same invalidation strategy as base
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
@@ -466,32 +466,23 @@ struct
 
   (* Give the set of reachables from argument. *)
   let reachables (ask: Queries.ask) es =
-    let reachable acc e =
-      Option.bind acc (fun st ->
-        let ad = ask.f (Queries.ReachableFrom e) in
-        if Queries.AD.is_top ad then
-          None
-        else
-          Some (Queries.AD.join ad st))
+    let reachable st e =
+      let ad = ask.f (Queries.ReachableFrom e) in
+      Queries.AD.join ad st
     in
-    List.fold_left reachable (Some (Queries.AD.empty ())) es
+    List.fold_left reachable (Queries.AD.empty ()) es
 
 
   let forget_reachable man st es =
     let ask = Analyses.ask_of_man man in
     let rs =
-      match reachables ask es with
-      | None ->
-        (* top reachable, so try to invalidate everything *)
-        let to_cil_lval x = Option.map Cil.var @@ RV.to_cil_varinfo x in
-        RD.vars st.rel |> List.filter_map to_cil_lval
-      | Some ad ->
-        let to_cil addr rs =
-          match addr with
-          | Queries.AD.Addr.Addr mval -> (ValueDomain.Addr.Mval.to_cil mval) :: rs
-          | _ -> rs
-        in
-        Queries.AD.fold to_cil ad []
+      let ad = reachables ask es in
+      let to_cil addr rs =
+        match addr with
+        | Queries.AD.Addr.Addr mval -> (ValueDomain.Addr.Mval.to_cil mval) :: rs
+        | _ -> rs
+      in
+      Queries.AD.fold to_cil ad []
     in
     List.fold_left (fun st lval ->
         invalidate_one ask man st lval
@@ -512,6 +503,36 @@ struct
       if RD.is_bot_env res then raise Deadcode;
       {st with rel = res}
 
+  let special_unknown_invalidate man f args =
+    (* No warning here, base already produces the appropriate warnings *)
+    let desc = LibraryFunctions.find f in
+    let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
+    let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
+    let deep_addrs =
+      if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
+        foldGlobals !Cilfacade.current_file (fun acc global ->
+            match global with
+            | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
+              mkAddrOf (Var vi, NoOffset) :: acc
+            (* TODO: what about GVarDecl? *)
+            | _ -> acc
+          ) deep_addrs
+      )
+      else
+        deep_addrs
+    in
+    let lvallist e =
+      match man.ask (Queries.MayPointTo e) with
+      | ad when Queries.AD.is_top ad -> []
+      | ad ->
+        Queries.AD.to_mval ad
+        |> List.map ValueDomain.Addr.Mval.to_cil
+    in
+    let st' = forget_reachable man man.local deep_addrs in
+    let shallow_lvals = List.concat_map lvallist shallow_addrs in
+    List.fold_left (invalidate_one (Analyses.ask_of_man man) man) st' shallow_lvals
+
+
   let special man r f args =
     let ask = Analyses.ask_of_man man in
     let st = man.local in
@@ -542,31 +563,7 @@ struct
          assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
         ) st r
     | _, _ ->
-      let lvallist e =
-        match ask.f (Queries.MayPointTo e) with
-        | ad when Queries.AD.is_top ad -> []
-        | ad ->
-          Queries.AD.to_mval ad
-          |> List.map ValueDomain.Addr.Mval.to_cil
-      in
-      let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
-      let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
-      let deep_addrs =
-        if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
-          foldGlobals !Cilfacade.current_file (fun acc global ->
-              match global with
-              | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
-                mkAddrOf (Var vi, NoOffset) :: acc
-              (* TODO: what about GVarDecl? *)
-              | _ -> acc
-            ) deep_addrs
-        )
-        else
-          deep_addrs
-      in
-      let st' = forget_reachable man st deep_addrs in
-      let shallow_lvals = List.concat_map lvallist shallow_addrs in
-      let st' = List.fold_left (invalidate_one ask man) st' shallow_lvals in
+      let st' = special_unknown_invalidate man f args in
       (* invalidate lval if present *)
       Option.map_default (invalidate_one ask man st') st' r
 
@@ -669,21 +666,19 @@ struct
 
   let threadenter man ~multiple lval f args =
     let st = man.local in
+    (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
+       Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
+       sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
+       EnterMultithreaded events only execute after threadenter and threadspawn. *)
+    if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man)) then
+      ignore (Priv.enter_multithreaded (Analyses.ask_of_man man) man.global man.sideg st);
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
-      (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
-         Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
-         sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
-         EnterMultithreaded events only execute after threadenter and threadspawn. *)
-      if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man)) then
-        ignore (Priv.enter_multithreaded (Analyses.ask_of_man man) man.global man.sideg st);
       let st' = Priv.threadenter (Analyses.ask_of_man man) man.global st in
       let new_rel = make_callee_rel ~thread:true man fd args in
       [{st' with rel = new_rel}]
     | exception Not_found ->
-      (* Unknown functions *)
-      (* TODO: do something like base? *)
-      failwith "relation.threadenter: unknown function"
+      [special_unknown_invalidate man f args]
 
   let threadspawn man ~multiple lval f args fman =
     man.local
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2150,12 +2150,6 @@ struct
     (* TODO: make this is_private PrivParam dependent? PerMutexOplusPriv should keep *)
     let st' =
       if thread then (
-        (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
-           Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
-           sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
-           EnterMultithreaded events only execute after threadenter and threadspawn. *)
-        if not (ThreadFlag.has_ever_been_multi ask) then
-          ignore (Priv.enter_multithreaded ask (priv_getg man.global) (priv_sideg man.sideg) st);
         Priv.threadenter ask st
       ) else
         (* use is_global to account for values that became globals because they were saved into global variables *)
@@ -2967,6 +2961,13 @@ struct
     combine_one man.local after
 
   let threadenter man ~multiple (lval: lval option) (f: varinfo) (args: exp list): D.t list =
+    (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
+       Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
+       sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
+       EnterMultithreaded events only execute after threadenter and threadspawn. *)
+    let st = man.local in
+    if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man)) then
+      ignore (Priv.enter_multithreaded (Analyses.ask_of_man man) (priv_getg man.global) (priv_sideg man.sideg) st);
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
       [make_entry ~thread:true man fd args]
diff --git a/tests/regression/46-apron2/93-invalidate-more.c b/tests/regression/46-apron2/93-invalidate-more.c
@@ -0,0 +1,22 @@
+// SKIP PARAM: --set ana.activated[+] apron --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <goblint.h>
+#include <stdio.h>
+
+int debug;
+int other;
+
+int main() {
+  int top;
+
+  // Needed so Base & DefExc doesn't find this information because it invalidates less
+  if(top) {
+    debug = 3;
+  }
+
+  fscanf(stdin, "%d", &other);
+
+   // Use to fail as debug was invalidated
+  __goblint_check(debug <= 3);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/94-weird.c b/tests/regression/46-apron2/94-weird.c
@@ -0,0 +1,15 @@
+// CRAM SKIP
+#include<pthread.h>
+pthread_mutex_t c;
+int d, e, f;
+
+void b(void* arg);
+
+void main(int argc, char *argv) {
+  pthread_t t;
+  e = pthread_create(&t, 0, b, &f);
+  pthread_mutex_lock(&c);
+  d++;
+  pthread_mutex_unlock(&c);
+  pthread_mutex_lock(&c);
+}
diff --git a/tests/regression/46-apron2/94-weird.t b/tests/regression/46-apron2/94-weird.t
@@ -0,0 +1,19 @@
+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
+  [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)
+  [Info][Witness] witness validation summary:
+    confirmed: 0
+    unconfirmed: 1
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 1
+  [Error][Imprecise][Unsound] Function definition missing
diff --git a/tests/regression/46-apron2/94-weird.yml b/tests/regression/46-apron2/94-weird.yml
@@ -0,0 +1,30 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "2.0"
+    uuid: 271d28bc-9fe6-4b18-9b7c-6bb68c7d5dcf
+    creation_time: 2025-07-15T14:56:13Z
+    producer:
+      name: Goblint
+      version: heads/issue_1535-0-g2accba23c-dirty
+      command_line: '''./goblint'' ''--conf'' ''conf/traces-rel.json'' ''--set'' ''ana.activated[+]''
+        ''threadJoins'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set'' ''ana.path_sens[+]''
+        ''threadflag'' ''--set'' ''ana.relation.privatization'' ''mutex-meet-tid''
+        ''2.c'' ''--sets'' ''exp.relation.prec-dump'' ''cluster.prec'' ''--html''
+        ''--enable'' ''witness.yaml.enabled'' ''--set'' ''witness.yaml.path'' ''1.yml'''
+    task:
+      input_files:
+      - 94-weird.c
+      input_file_hashes:
+        94-weird.c: c67808107b2da394e33439894ea1ae3c5e5c3628a08c9371eaa31ee3efbc8414
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 94-weird.c
+        line: 11
+        column: 3
+        function: main
+      value: (long long )f + 2147483648LL >= (long long )e
+      format: c_expression
