Fix unsound Apron dummy privatization

src/analyses/apron/apronPriv.apron.ml

@@ -44,30 +44,73 @@ module type S =
     val finalize: unit -> unit
   end
 
-
-module Dummy: S = functor (AD: ApronDomain.S2) ->
+(** Top privatization, which doesn't track globals at all.
+    This is unlike base's "none" privatization. which does track globals, but doesn't privatize them. *)
+module Top: S = functor (AD: ApronDomain.S2) ->
 struct
   module D = Lattice.Unit
   module G = Lattice.Unit
   module V = EmptyV
 
-  let name () = "Dummy"
+  type apron_components_t = ApronComponents (AD) (D).t
+
+  module AV = ApronDomain.V
+
+  let name () = "top"
   let startstate () = ()
   let should_join _ _ = true
 
-  let read_global ask getg st g x = st.ApronDomain.apr
-  let write_global ?(invariant=false) ask getg sideg st g x = st
+  let read_global ask getg (st: apron_components_t) g x =
+    let apr = st.apr in
+    assert (not (AD.mem_var apr (AV.global g)));
+    apr
+
+  let write_global ?(invariant=false) ask getg sideg (st: apron_components_t) g x: apron_components_t =
+    let apr = st.apr in
+    assert (not (AD.mem_var apr (AV.global g)));
+    st
 
   let lock ask getg st m = st
   let unlock ask getg sideg st m = st
 
   let thread_join ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
-  let sync ask getg sideg st reason = st
+  let sync (ask: Q.ask) getg sideg (st: apron_components_t) reason =
+    match reason with
+    | `Join ->
+      if (ask.f Q.MustBeSingleThreaded) then
+        st
+      else
+        (* must be like enter_multithreaded *)
+        let apr = st.apr in
+        let apr_local = AD.remove_filter apr (fun var ->
+            match AV.find_metadata var with
+            | Some (Global _) -> true
+            | _ -> false
+          )
+        in
+        {st with apr = apr_local}
+    | `Normal
+    | `Init
+    | `Thread
+    | `Return ->
+      st
+
+  let enter_multithreaded ask getg sideg (st: apron_components_t): apron_components_t =
+    let apr = st.apr in
+    let apr_local = AD.remove_filter apr (fun var ->
+        match AV.find_metadata var with
+        | Some (Global _) -> true
+        | _ -> false
+      )
+    in
+    {st with apr = apr_local}
+
+  let threadenter ask getg (st: apron_components_t): apron_components_t =
+    {apr = AD.bot (); priv = startstate ()}
 
-  let enter_multithreaded ask getg sideg st = st
-  let threadenter ask getg st = st
+  (* TODO: remove escaped locals after PR #742 *)
 
   let init () = ()
   let finalize () = ()
@@ -1166,7 +1209,7 @@ let priv_module: (module S) Lazy.t =
   lazy (
     let module Priv: S =
       (val match get_string "ana.apron.privatization" with
-         | "dummy" -> (module Dummy : S)
+         | "top" -> (module Top : S)
          | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
          | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
          | "mutex-meet" -> (module PerMutexMeetPriv)

src/util/options.schema.json

@@ -747,9 +747,9 @@
             "privatization": {
               "title": "ana.apron.privatization",
               "description":
-                "Which apron privatization to use? dummy/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power",
+                "Which apron privatization to use? top/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power",
               "type": "string",
-              "enum": ["dummy", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
+              "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
               "default": "mutex-meet"
             },
             "priv": {

tests/regression/36-apron/01-octagon_simple.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --enable ana.int.interval  --set ana.base.arrays.domain partitioned  --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval
 // Example from https://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf
 void main(void) {
   int X = 0;

tests/regression/36-apron/02-octagon_interprocudral.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --enable ana.int.interval --set ana.base.arrays.domain partitioned  --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval
 extern int __VERIFIER_nondet_int();
 
 int main(void) {

tests/regression/36-apron/03-problem-signextension.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron']"  --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set ana.activated[+] apron
 // Example from https://github.com/sosy-lab/sv-benchmarks/blob/master/c/bitvector-regression/signextension-1.c
 
 #include <assert.h>

tests/regression/36-apron/04-problem-rec.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set ana.activated[+] apron
 // Example from https://github.com/sosy-lab/sv-benchmarks/blob/master/c/recursive-simple/afterrec-1.c
 void f(int n) {
   if (n<3) return;

tests/regression/36-apron/05-problem-rec2.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set ana.activated[+] apron
 // Example from https://github.com/sosy-lab/sv-benchmarks/blob/master/c/recursive-simple/afterrec_2calls-1.c
 
 void f(int);

tests/regression/36-apron/06-problem-overflow.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set ana.activated[+] apron
 // Example from https://github.com/sosy-lab/sv-benchmarks/blob/master/c/bitvector-loops/overflow_1-2.c
 
 int main(void) {

tests/regression/36-apron/07-problem-pointer.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set ana.activated[+] apron
 extern int __VERIFIER_nondet_int();
 
 void change(int *p) {

tests/regression/36-apron/08-problem-implicitunsignedconversion.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set ana.activated[+] apron
 // Example from https://github.com/sosy-lab/sv-benchmarks/blob/master/c/bitvector-regression/implicitunsignedconversion-1.c
 
 #include <assert.h>

tests/regression/36-apron/64-dummy-sound.c

@@ -0,0 +1,27 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.privatization top
+#include <pthread.h>
+#include <assert.h>
+
+int g;
+
+void *t_fun(void *arg) {
+  // shouldn't have g, x, y in local apron state
+  g = 43;
+  int *p = arg;
+  *p = 11;
+  return NULL;
+}
+
+int main() {
+  g = 42;
+  int x = 10;
+  int y = 20;
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, &x);
+
+  // shouldn't have g, x, y in local apron state
+  assert(g == 42); // UNKNOWN!
+  assert(x == 10); // UNKNOWN!
+  return 0;
+}

tests/regression/36-apron/94-simple-apron-interval.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --enable ana.int.interval  --set ana.base.arrays.domain partitioned  --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy --set ana.apron.domain "interval"
+// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain interval
 // Example from https://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf, adapted
 void main(void) {
   int X = 0;

tests/regression/36-apron/95-simple-polyhedra.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --enable ana.int.interval  --set ana.base.arrays.domain partitioned  --set ana.activated "['base','threadid','threadflag','expRelation','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy --set ana.apron.domain "polyhedra"
+// SKIP PARAM: --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
 // Example from https://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf, adapted
 void main(void) {
   int X = 0;