diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 1aa137c76e..715b9b730b 100644 --- a/src/analyses/base.ml +++ b/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 ( diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 42d148ff57..9881534706 100644 --- a/src/analyses/basePriv.ml +++ b/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))) ); diff --git a/src/analyses/baseUtil.ml b/src/analyses/baseUtil.ml index ec66a027ab..202aa54410 100644 --- a/src/analyses/baseUtil.ml +++ b/src/analyses/baseUtil.ml @@ -9,11 +9,5 @@ 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 after_config () = - precious_globs := get_string_list "exp.precious_globs" - -let _ = - AfterConfig.register after_config \ No newline at end of file +let is_excluded_from_earlyglobs v = List.mem v.vname (get_string_list "exp.exclude_from_earlyglobs") +let is_excluded_from_invalidation v = List.mem v.vname (get_string_list "exp.exclude_from_invalidation") diff --git a/src/analyses/baseUtil.mli b/src/analyses/baseUtil.mli index 93eab6e7d3..6b6923c981 100644 --- a/src/analyses/baseUtil.mli +++ b/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 diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index a12ed5a0fd..3c19b778dc 100644 --- a/src/analyses/commonPriv.ml +++ b/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}) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 3f41c22d9b..9edb247c08 100644 --- a/src/util/options.schema.json +++ b/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.", diff --git a/tests/regression/01-cpa/50-earlyglobs_precious.c b/tests/regression/01-cpa/50-earlyglobs_precious.c index 84c084cf92..5328e25997 100644 --- a/tests/regression/01-cpa/50-earlyglobs_precious.c +++ b/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'" int g = 10; int main(void){ g = 100; assert(g==100); return 0; -} \ No newline at end of file +}