Merge pull request #1641 from goblint/witness_val_fail_cherrypick

Fixes for Self-Validation Issues

Author: michael-schwarz

src/analyses/apron/relationAnalysis.apron.ml

@@ -56,7 +56,8 @@ struct
       Priv.read_global ask getg st g x
     else (
       let rel = st.rel in
-      let g_var = RV.global g in
+      (* If it has escaped and we have never been multi-threaded, we can still refer to the local *)
+      let g_var = if g.vglob then RV.global g else RV.local g in
       let x_var = RV.local x in
       let rel' = RD.add_vars rel [g_var] in
       let rel' = RD.assign_var rel' x_var g_var in
@@ -602,6 +603,10 @@ struct
           | Some (Local v) ->
             if VH.mem v_ins_inv v then
               keep_global
+            else if ThreadEscape.has_escaped ask v then
+              (* Escaped local variables should be read in via their v#in# variables, this apron var may refer to stale values only *)
+              (* and is not a sound description of the C variable. *)
+              false
             else
               keep_local
           | _ -> false

tests/regression/46-apron2/95-witness-mm-escape.c

@@ -0,0 +1,19 @@
+// CRAM SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+#include <pthread.h>
+#include <goblint.h>
+
+int *b;
+pthread_mutex_t e;
+
+void main() {
+
+    int g = 8;
+    int a;
+    if(a) {
+        g = 10;
+    }
+
+    b = &g;
+
+    pthread_mutex_lock(&e);
+}

tests/regression/46-apron2/95-witness-mm-escape.t

@@ -0,0 +1,29 @@
+  $ goblint --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml 95-witness-mm-escape.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Success][Witness] invariant confirmed: 0 <= g (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 0 <= *b (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: g <= 127 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: *b <= 127 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: -8LL + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 2147483648LL + (long long )a >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483638LL + (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483637LL - (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 10LL - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 2147483647LL - (long long )a >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483658LL + (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483657LL - (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: b == & g (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: g != 0 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: *b != 0 (95-witness-mm-escape.c:19:1)
+  [Info][Witness] witness validation summary:
+    confirmed: 15
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 15