Merge pull request #1354 from goblint/issue_1302

Fix unsound join for `top` with empty environment in `ApronDomain`

src/analyses/apron/relationAnalysis.apron.ml

@@ -44,10 +44,10 @@ struct
     if ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.relation.context" ~removeAttr:"relation.no-context" ~keepAttr:"relation.context" fd then
       x
     else
-      D.bot () (* just like startstate, heterogeneous RD.bot () means top over empty set of variables *)
+      D.top ()
 
-  let exitstate  _ = { rel = RD.bot (); priv = Priv.startstate () }
-  let startstate _ = { rel = RD.bot (); priv = Priv.startstate () }
+  let exitstate  _ = { rel = RD.top (); priv = Priv.startstate () }
+  let startstate _ = { rel = RD.top (); priv = Priv.startstate () }
 
   (* Functions for manipulating globals as temporary locals. *)
 

src/analyses/apron/relationPriv.apron.ml

@@ -127,7 +127,7 @@ struct
     {st with rel = rel_local}
 
   let threadenter ask getg (st: relation_components_t): relation_components_t =
-    {rel = RD.bot (); priv = startstate ()}
+    {rel = RD.top (); priv = startstate ()}
 
   let iter_sys_vars getg vq vf = ()
   let invariant_vars ask getg st = []
@@ -489,7 +489,11 @@ struct
     in
     let get_mutex_inits = getg V.mutex_inits in
     let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in
-    RD.join get_mutex_global_g get_mutex_inits'
+    if not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *)
+      (* This is an escaped variable whose value was never side-effected to get_mutex_inits' *)
+      get_mutex_global_g
+    else
+      RD.join get_mutex_global_g get_mutex_inits'
 
   let get_mutex_global_g_with_mutex_inits_atomic ask getg =
     (* Unprotected invariant is one big relation. *)
@@ -527,12 +531,15 @@ struct
     else
       rel_local (* Keep write local as if it were protected by the atomic section. *)
 
-  let write_global ?(invariant=false) (ask: Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
+  (** Like write global but has option to skip meet with current value, as the value will not have been side-effected to a useful location thus far *)
+  let write_global_internal ?(skip_meet=false)  ?(invariant=false) (ask: Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
     let atomic = Param.handle_atomic && ask.f MustBeAtomic in
     let rel = st.rel in
     (* lock *)
     let rel =
-      if atomic && RD.mem_var rel (AV.global g) then
+      if skip_meet then
+        rel
+      else if atomic && RD.mem_var rel (AV.global g) then
         rel (* Read previous unpublished unprotected write in current atomic section. *)
       else if atomic then
         RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg) (* Read unprotected invariant as full relation. *)
@@ -564,6 +571,9 @@ struct
       {st with rel = rel_local} (* Keep write local as if it were protected by the atomic section. *)
 
 
+  let write_global = write_global_internal ~skip_meet:false
+  let write_escape = write_global_internal ~skip_meet:true
+
   let lock ask getg (st: relation_components_t) m =
     let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
     (* TODO: somehow actually unneeded here? *)
@@ -626,13 +636,17 @@ struct
         st
       else
         let rel = st.rel in
-        let rel_side = RD.keep_filter rel (fun var ->
+        (* Replace with remove_filter once issues are fixed *)
+        let g_vars = List.filter (fun var ->
             match AV.find_metadata var with
             | Some (Global _) -> true
             | _ -> false
-          )
+          ) (RD.vars rel)
         in
-        sideg V.mutex_inits rel_side;
+        let rel_side = RD.keep_vars rel g_vars in
+        (* If no globals are contained here, none need to be published *)
+        (* https://github.com/goblint/analyzer/pull/1354 *)
+        if g_vars <> [] then sideg V.mutex_inits rel_side;
         let rel_local = RD.remove_filter rel (fun var ->
             match AV.find_metadata var with
             | Some (Global g) -> is_unprotected ask g
@@ -662,11 +676,11 @@ struct
   let escape node ask getg sideg (st:relation_components_t) escaped : relation_components_t =
     let esc_vars = EscapeDomain.EscapedVars.elements escaped in
     let esc_vars = List.filter (fun v -> not v.vglob && RD.Tracked.varinfo_tracked v && RD.mem_var st.rel (AV.local v)) esc_vars in
-    let escape_one (x:varinfo) st = write_global ask getg sideg st x x in
+    let escape_one (x:varinfo) st = write_escape ask getg sideg st x x in
     List.fold_left (fun st v -> escape_one v st) st esc_vars
 
   let threadenter ask getg (st: relation_components_t): relation_components_t =
-    {rel = RD.bot (); priv = startstate ()}
+    {rel = RD.top (); priv = startstate ()}
 
   let init () = ()
   let finalize () = ()
@@ -799,7 +813,7 @@ struct
   let lock_get_m oct local_m get_m =
     let joined = LRD.join local_m get_m in
     if M.tracing then M.traceli "relationpriv" "lock_get_m:\n  get=%a\n  joined=%a\n" LRD.pretty get_m LRD.pretty joined;
-    let r = LRD.fold (fun _ -> RD.meet) joined (RD.bot ()) in (* bot is top with empty env *)
+    let r = LRD.fold (fun _ -> RD.meet) joined (RD.top ()) in
     if M.tracing then M.trace "relationpriv" "meet=%a\n" RD.pretty r;
     let r = RD.meet oct r in
     if M.tracing then M.traceu "relationpriv" "-> %a\n" RD.pretty r;
@@ -1220,7 +1234,7 @@ struct
 
   let threadenter ask getg (st: relation_components_t): relation_components_t =
     let _,lmust,l = st.priv in
-    {rel = RD.bot (); priv = (W.bot (),lmust,l)}
+    {rel = RD.top (); priv = (W.bot (),lmust,l)}
 
   let iter_sys_vars getg vq vf =
     match vq with

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -305,9 +305,9 @@ struct
 
   let is_bot_env t = t.d = None
 
-  let top () = failwith "D.top ()"
+  let top () = {d = Some (Matrix.empty ()); env = Environment.make [||] [||]}
 
-  let is_top _ = false
+  let is_top t = Environment.equal empty_env t.env && GobOption.exists Matrix.is_empty t.d
 
   let is_top_env t = (not @@ Environment.equal empty_env t.env) && GobOption.exists Matrix.is_empty t.d
 

src/cdomains/apron/apronDomain.apron.ml

@@ -659,14 +659,15 @@ struct
 
   let empty_env = Environment.make [||] [||]
 
+  (* top and bottom over the empty environment are different, pending  https://github.com/goblint/analyzer/issues/1380 *)
   let bot () =
-    top_env empty_env
+    bot_env empty_env
 
   let top () =
-    failwith "D2.top"
+    top_env empty_env
 
-  let is_bot = equal (bot ())
-  let is_top _ = false
+  let is_bot x = equal (bot ()) x
+  let is_top x = equal (top ()) x
 
   let strengthening_enabled = GobConfig.get_bool "ana.apron.strengthening"
 

tests/regression/46-apron2/79-context-insens.c

@@ -0,0 +1,28 @@
+// PARAM: --enable annotation.goblint_relation_track --set ana.activated[+] apron --set ana.activated[+] memLeak --set ana.ctx_insens "['base','mallocWrapper','mutexEvents','assert','apron','memLeak']" --set ana.malloc.unique_address_count 2
+
+// Adapted from https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/list-properties/list_search-1.c
+#include <goblint.h>
+
+typedef struct thing {
+	int key;
+} thing;
+
+thing *container;
+
+int insert(int k __attribute__((__goblint_relation_track__))) {
+  container = (thing*) malloc(sizeof(thing));
+  container->key = k;
+  return 0;
+}
+
+int main(void){
+  insert(2);
+  insert(5);
+
+  if(container !=0) { // Used to detect dead code after loop head
+
+  }
+
+  __goblint_check(1); // Should be reachable
+  return 0;
+}