Pass Escaped Locals to Callee as They Need to Be Considered Globals

src/analyses/base.ml

@@ -498,7 +498,9 @@ struct
   let context (fd: fundec) (st: store): store =
     let f keep drop_fn (st: store) = if keep then st else { st with cpa = drop_fn st.cpa} in
     st |>
-    f (not !GU.earlyglobs) (CPA.filter (fun k v -> not (Basetype.Variables.is_global k) || is_excluded_from_earlyglobs k))
+    (* Here earlyglobs only drops syntactic globals from the context and does not consider e.g. escaped globals. *)
+    (* This is equivalent to having escaped globals excluded from earlyglobs for contexts *)
+    f (not !GU.earlyglobs) (CPA.filter (fun k v -> (not k.vglob) || is_excluded_from_earlyglobs k))
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.non-ptr" ~removeAttr:"base.no-non-ptr" ~keepAttr:"base.non-ptr" fd) drop_non_ptrs
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.int" ~removeAttr:"base.no-int" ~keepAttr:"base.int" fd) drop_ints
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval" ~removeAttr:"base.no-interval" ~keepAttr:"base.interval" fd) drop_interval
@@ -2131,7 +2133,8 @@ struct
           ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st);
         Priv.threadenter (Analyses.ask_of_ctx ctx) st
       ) else
-        let globals = CPA.filter (fun k v -> Basetype.Variables.is_global k) st.cpa in
+        (* use is_global to account for values that became globals because they were saved into global variables *)
+        let globals = CPA.filter (fun k v -> is_global (Analyses.ask_of_ctx ctx) k) st.cpa in
         (* let new_cpa = if !GU.earlyglobs || ThreadFlag.is_multi ctx.ask then CPA.filter (fun k v -> is_private ctx.ask ctx.local k) globals else globals in *)
         let new_cpa = globals in
         {st with cpa = new_cpa}

src/analyses/basePriv.ml

@@ -47,7 +47,7 @@ end
 
 let old_threadenter (type d) ask (st: d BaseDomain.basecomponents_t) =
   (* Copy-paste from Base make_entry *)
-  let globals = CPA.filter (fun k v -> Basetype.Variables.is_global k) st.cpa in
+  let globals = CPA.filter (fun k v -> is_global ask k) st.cpa in
   (* let new_cpa = if !GU.earlyglobs || ThreadFlag.is_multi ctx.ask then CPA.filter (fun k v -> is_private ctx.ask ctx.local k) globals else globals in *)
   let new_cpa = globals in
   {st with cpa = new_cpa}

src/cdomains/basetype.ml

@@ -22,7 +22,6 @@ module Variables =
 struct
   include CilType.Varinfo
   let trace_enabled = true
-  let is_global v = v.vglob
   let show x =
     if RichVarinfo.BiVarinfoMap.Collection.mem_varinfo x then
       let description = RichVarinfo.BiVarinfoMap.Collection.describe_varinfo x in

tests/regression/11-heap/03-linked.c

@@ -0,0 +1,37 @@
+#include <assert.h>
+
+struct list
+{
+    int n;
+    struct list *next;
+};
+
+void *allocate_memory()
+{
+    return malloc(8U);
+}
+
+struct list *append(struct list *l, int n)
+{
+    struct list *new_el;
+
+    new_el = allocate_memory();
+
+    new_el->n = n;
+    new_el->next = l;
+
+    return new_el;
+}
+
+int main()
+{
+    struct list *l, m;
+    l = &m;
+    l->next = 0;
+    l->n = 0;
+
+    l = append(l, 1);
+    l = append(l, 2);
+
+    assert(l->next->next->n == 0); //UNKNOWN
+}

tests/regression/45-escape/05-global-single-threaded.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+int* ptr;
+int nine = 9;
+
+int other() {
+    assert(*ptr == 8); //UNKNOWN!
+}
+
+int main()
+{
+    int g = 8;
+    int top;
+
+    if(top) {
+        ptr = &g;
+    } else {
+        ptr = &nine;
+    }
+
+    other();
+}