Apron: Track relational information for variables that have their address taken

src/analyses/apron/apronAnalysis.apron.ml

@@ -373,18 +373,18 @@ struct
           invalidate_one ask ctx st (Lval.CilLval.to_lval lval)
         ) rs st
 
-
   let special ctx r f args =
     let ask = Analyses.ask_of_ctx ctx in
     let st = ctx.local in
     let desc = LibraryFunctions.find f in
     match desc.special args, f.vname with
     (* TODO: assert handling from https://github.com/goblint/analyzer/pull/278 *)
-    | `Assert expression -> st
-    | `Unknown "__goblint_check" -> st
-    | `Unknown "__goblint_commit" -> st
-    | `Unknown "__goblint_assert" -> st
-    | `ThreadJoin (id,retvar) ->
+    | Assert expression, _ -> st
+    | Unknown, "__goblint_check" -> st
+    | Unknown, "__goblint_commit" -> st
+    | Unknown, "__goblint_assert" -> st
+    | ThreadJoin { thread = id; ret_var = retvar }, _ ->
+      (* nothing to invalidate as only arguments that have their AddrOf taken may be invalidated *)
       (
         (* Forget value that thread return is assigned to *)
         let st' = forget_reachable ctx st [retvar] in
@@ -394,28 +394,32 @@ struct
         | None -> st'
       )
     | _, _ ->
-      let ask = Analyses.ask_of_ctx ctx in
-      let st' = match LibraryFunctions.get_invalidate_action f.vname with
-        | Some fnc -> forget_reachable ctx st (fnc `Write args)
-        | None ->
-          let st' = if GobConfig.get_bool "sem.unknown_function.invalidate.globals" then (
-            let globals = foldGlobals !Cilfacade.current_file (fun acc global ->
-                match global with
-                | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
-                  (Var vi, NoOffset) :: acc
-                (* TODO: what about GVarDecl? *)
-                | _ -> acc
-              ) []
-            in
-            List.fold_left (invalidate_one ask ctx) st globals)
-          else
-            st
+      let lvallist e =
+        let s = ask.f (Queries.MayPointTo e) in
+        match s with
+        | `Top -> []
+        | `Lifted _ -> List.map (Lval.CilLval.to_lval) (Queries.LS.elements s)
+      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 st' =
+        if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
+          let globals = foldGlobals !Cilfacade.current_file (fun acc global ->
+              match global with
+              | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
+                (Var vi, NoOffset) :: acc
+              (* TODO: what about GVarDecl? *)
+              | _ -> acc
+            ) []
           in
-          if GobConfig.get_bool "sem.unknown_function.invalidate.args" then
-            forget_reachable ctx st' args
-          else
-            st'
+          List.fold_left (invalidate_one ask ctx) st globals
+        )
+        else
+          st
       in
+      let st' = forget_reachable ctx st' deep_addrs in
+      let shallow_lvals = List.concat_map lvallist shallow_addrs in
+      let st' = List.fold_left (invalidate_one ask ctx) st' shallow_lvals in
       (* invalidate lval if present *)
       match r with
       | Some lv -> invalidate_one ask ctx st' lv

src/analyses/apron/apronPriv.apron.ml

@@ -54,12 +54,8 @@ struct
   module V = EmptyV
   module AV = ApronDomain.V
 
-  type apron_components_t = ApronDomain.ApronComponents (AD) (D).t
-
   type apron_components_t = ApronComponents (AD) (D).t
 
-  module AV = ApronDomain.V
-
   let name () = "top"
   let startstate () = ()
   let should_join _ _ = true
@@ -81,6 +77,7 @@ struct
   let thread_return ask getg sideg tid st = st
 
   let sync ask getg sideg st reason = st
+
   let escape node ask getg sideg (st:apron_components_t) escaped:apron_components_t =
     let apr = st.apr in
     let esc_vars = List.filter (fun var -> match AV.find_metadata var with
@@ -97,6 +94,27 @@ struct
     let apr_local = AD.remove_vars apr esc_vars in
     { st with apr = apr_local }
 
+  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 ->
@@ -110,8 +128,6 @@ struct
   let threadenter ask getg (st: apron_components_t): apron_components_t =
     {apr = AD.bot (); priv = startstate ()}
 
-  (* TODO: remove escaped locals after PR #742 *)
-
   let init () = ()
   let finalize () = ()
 end

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','escape']" --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/46-apron2/05-pointer-multilevel.c

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

tests/regression/46-apron2/06-pointer-multilevel-two.c

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

tests/regression/46-apron2/07-escaping-recursion.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron','escape']" --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron','escape']" --set ana.base.privatization none --set ana.apron.privatization top
 // Copy of 01/52 for Apron
 int rec(int i,int* ptr) {
     int top;

tests/regression/46-apron2/08-escape-local-in-pthread-dummy.c

@@ -1,4 +1,4 @@
-// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron','escape']" --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron','escape']" --set ana.base.privatization none --set ana.apron.privatization top
 // Copy of 45 01 for apron
 #include <pthread.h>
 #include <assert.h>

tests/regression/46-apron2/11-names.c

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