diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index c7b62e8d16..3913e7218e 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/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. *) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 11c8b54498..5e78a02153 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/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 diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index dacdce659e..944515f4ec 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/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 diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 2b8f360bc5..158d3ca907 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/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" diff --git a/tests/regression/46-apron2/79-context-insens.c b/tests/regression/46-apron2/79-context-insens.c new file mode 100644 index 0000000000..822caae414 --- /dev/null +++ b/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 + +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; +}