Rename and split exp.precious_globs to exp.exclude_from_earlyglobs and exp.exclude_from_invalidation

src/analyses/base.ml

@@ -486,7 +486,7 @@ 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_precious_glob k))
+    f (not !GU.earlyglobs) (CPA.filter (fun k v -> not (Basetype.Variables.is_global k) || 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
@@ -1903,7 +1903,7 @@ struct
     in
     let invalids = invalidate_exp exps in
     let is_fav_addr x =
-      List.exists BaseUtil.is_precious_glob (AD.to_var_may x)
+      List.exists BaseUtil.is_excluded_from_invalidation (AD.to_var_may x)
     in
     let invalids' = List.filter (fun (x,_,_) -> not (is_fav_addr x)) invalids in
     if M.tracing && exps <> [] then (

src/analyses/basePriv.ml

@@ -146,7 +146,7 @@ struct
     | x -> (if M.tracing then M.tracec "get" "Using privatized version.\n"; x)
 
   let is_private (a: Q.ask) (v: varinfo): bool =
-    not (ThreadFlag.is_multi a) && is_precious_glob v (* not multi, but precious (earlyglobs) *)
+    not (ThreadFlag.is_multi a) && is_excluded_from_earlyglobs v (* not multi, but excluded from earlyglobs *)
     || not (a.f (Q.MayBePublic {global=v; write=false})) (* usual case where MayBePublic answers *)
 
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
@@ -172,7 +172,7 @@ struct
     let side_var (v: varinfo) (value) (st: BaseComponents.t) =
       if M.tracing then M.traceli "globalize" ~var:v.vname "Tracing for %s\n" v.vname;
       let res =
-        if is_global ask v && ((privates && not (is_precious_glob v)) || not (is_private ask v)) then begin
+        if is_global ask v && ((privates && not (is_excluded_from_earlyglobs v)) || not (is_private ask v)) then begin
           if M.tracing then M.tracec "globalize" "Publishing its value: %a\n" VD.pretty value;
           sideg v value;
           {st with cpa = CPA.remove v st.cpa}
@@ -431,7 +431,7 @@ struct
     | x -> (if M.tracing then M.tracec "get" "Using privatized version.\n"; x)
 
   let is_invisible (a: Q.ask) (v: varinfo): bool =
-    not (ThreadFlag.is_multi a) && is_precious_glob v (* not multi, but precious (earlyglobs) *)
+    not (ThreadFlag.is_multi a) && is_excluded_from_earlyglobs v (* not multi, but excluded from earlyglobs *)
     || not (a.f (Q.MayBePublic {global=v; write=false})) (* usual case where MayBePublic answers *)
   let is_private = is_invisible
 
@@ -451,7 +451,7 @@ struct
     )
 
   let is_protected (a: Q.ask) (v: varinfo): bool =
-    not (ThreadFlag.is_multi a) && is_precious_glob v (* not multi, but precious (earlyglobs) *)
+    not (ThreadFlag.is_multi a) && is_excluded_from_earlyglobs v (* not multi, but excluded from earlyglobs *)
     || not (a.f (Q.MayBePublic {global=v; write=true})) (* usual case where MayBePublic answers *)
 
   let sync ask getg sideg (st: BaseComponents (D).t) reason =
@@ -462,7 +462,7 @@ struct
       let res =
         if is_global ask v then
           let protected = is_protected ask v in
-          if privates && not (is_precious_glob v) || not protected then begin
+          if privates && not (is_excluded_from_earlyglobs v) || not protected then begin
             if M.tracing then M.tracec "globalize" "Publishing its value: %a\n" VD.pretty value;
             sideg v value;
             { st with cpa = CPA.remove v st.cpa; priv = MustVars.remove v st.priv}
@@ -704,7 +704,7 @@ struct
     let s = current_lockset ask in
     let t = current_thread ask in
     let cpa' = CPA.add x v st.cpa in
-    if not (!GU.earlyglobs && is_precious_glob x) then
+    if not (!GU.earlyglobs && is_excluded_from_earlyglobs x) then
       sideg (V.global x) (G.create_weak (GWeak.singleton s (ThreadMap.singleton t v)));
     {st with cpa = cpa'}
 
@@ -761,7 +761,7 @@ struct
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
     let s = current_lockset ask in
     let cpa' = CPA.add x v st.cpa in
-    if not (!GU.earlyglobs && is_precious_glob x) then
+    if not (!GU.earlyglobs && is_excluded_from_earlyglobs x) then
       sideg (V.global x) (G.create_weak (GWeak.singleton s v));
     {st with cpa = cpa'}
 
@@ -831,7 +831,7 @@ struct
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
     let s = current_lockset ask in
     let cpa' = CPA.add x v st.cpa in
-    if not (!GU.earlyglobs && is_precious_glob x) then
+    if not (!GU.earlyglobs && is_excluded_from_earlyglobs x) then
       sideg (V.global x) (G.create_weak (GWeak.singleton s v));
     {st with cpa = cpa'; priv = W.add x st.priv}
 
@@ -972,7 +972,7 @@ struct
       ) l vv
     in
     let cpa' = CPA.add x v st.cpa in
-    if not (!GU.earlyglobs && is_precious_glob x) then (
+    if not (!GU.earlyglobs && is_excluded_from_earlyglobs x) then (
       let v = distr_init getg x v in
       sideg (V.global x) (G.create_weak (GWeak.singleton s v))
     );
@@ -1115,7 +1115,7 @@ struct
     let p' = P.add x (MinLocksets.singleton s) p in
     let p' = P.map (fun s' -> MinLocksets.add s s') p' in
     let cpa' = CPA.add x v st.cpa in
-    if not (!GU.earlyglobs && is_precious_glob x) then (
+    if not (!GU.earlyglobs && is_excluded_from_earlyglobs x) then (
       let v = distr_init getg x v in
       sideg (V.global x) (G.create_weak (GWeak.singleton s (GWeakW.singleton s v)))
     );
@@ -1277,7 +1277,7 @@ struct
       ) l vv
     in
     let cpa' = CPA.add x v st.cpa in
-    if not (!GU.earlyglobs && is_precious_glob x) then (
+    if not (!GU.earlyglobs && is_excluded_from_earlyglobs x) then (
       let v = distr_init getg x v in
       sideg (V.global x) (G.create_weak (GWeak.singleton s (GWeakW.singleton s v)))
     );

src/analyses/baseUtil.ml

@@ -9,11 +9,15 @@ let is_static (v:varinfo): bool = v.vstorage = Static
 
 let is_always_unknown variable = variable.vstorage = Extern || Ciltools.is_volatile_tp variable.vtype
 
-let precious_globs = ref []
-let is_precious_glob v = List.mem v.vname !precious_globs
+let exclude_from_earlyglobs = ref []
+let exclude_from_invalidation = ref []
+
+let is_excluded_from_earlyglobs v = List.mem v.vname !exclude_from_earlyglobs
+let is_excluded_from_invalidation v =  List.mem v.vname !exclude_from_invalidation
 
 let after_config () =
-  precious_globs := get_string_list "exp.precious_globs"
+  exclude_from_earlyglobs := get_string_list "exp.exclude_from_earlyglobs";
+  exclude_from_invalidation := get_string_list "exp.exclude_from_invalidation"
 
 let _ =
-  AfterConfig.register after_config
+  AfterConfig.register after_config

src/analyses/baseUtil.mli

@@ -3,4 +3,5 @@ open Cil
 val is_global: Queries.ask -> varinfo -> bool
 val is_static: varinfo -> bool
 val is_always_unknown: varinfo -> bool
-val is_precious_glob: varinfo -> bool
+val is_excluded_from_earlyglobs: varinfo -> bool
+val is_excluded_from_invalidation: varinfo -> bool

src/analyses/commonPriv.ml

@@ -42,7 +42,7 @@ module Protection =
 struct
   let is_unprotected ask x: bool =
     let multi = ThreadFlag.is_multi ask in
-    (!GU.earlyglobs && not multi && not (is_precious_glob x)) ||
+    (!GU.earlyglobs && not multi && not (is_excluded_from_earlyglobs x)) ||
     (
       multi &&
       ask.f (Q.MayBePublic {global=x; write=true})

src/util/options.schema.json

@@ -1258,14 +1258,22 @@
           "type": "boolean",
           "default": false
         },
-        "precious_globs": {
-          "title": "exp.precious_globs",
+        "exclude_from_earlyglobs": {
+          "title": "exp.exclude_from_earlyglobs",
           "description":
             "Global variables that should be handled flow-sensitively when using earlyglobs.",
           "type": "array",
           "items": { "type": "string" },
           "default": []
         },
+        "exclude_from_invalidation" : {
+          "title": "exp.exclude_from_invalidation",
+          "description":
+            "Global variables that should not be invalidated. This assures the analysis that such globals are only modified through known code",
+          "type": "array",
+          "items": { "type": "string" },
+          "default": []
+        },
         "list-type": {
           "title": "exp.list-type",
           "description": "Use a special abstract value for lists.",

tests/regression/01-cpa/50-earlyglobs_precious.c

@@ -1,8 +1,8 @@
-// PARAM: --set exp.earlyglobs true --set exp.precious_globs[+] "'g'"
+// PARAM: --set exp.earlyglobs true --set exp.exclude_from_earlyglobs[+] "'g'" --set exp.exclude_from_invalidation[+] "'g'"
 
 int g = 10;
 int main(void){
   g = 100;
   assert(g==100);
   return 0;
-}
+}