Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Partially fix unsound join for top with empty environment in ApronDomain #1354

Merged
merged 15 commits into from
Mar 12, 2024
Merged

Partially fix unsound join for top with empty environment in ApronDomain #1354

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
978b5e6
Add failing test case.
jerhard Feb 6, 2024
554a5f0
apronDomain.join: Check for is_bot_env instead of is_bot.
jerhard Feb 6, 2024
2311795
Define bot and top in apron domain correctly.
jerhard Feb 6, 2024
8848276
Adapt relationPriv for bot being proper bot.
jerhard Feb 6, 2024
d2ffcf0
Do not side-effect empty relationship
michael-schwarz Feb 18, 2024
b57fd0f
Fix escape handling
michael-schwarz Feb 18, 2024
8787f59
Add a top to `affeq`?
michael-schwarz Feb 18, 2024
05bd808
Merge branch 'master' into issue_1302
michael-schwarz Feb 18, 2024
c008b83
Merge branch 'master' into issue_1302
michael-schwarz Mar 3, 2024
5f7ce7f
Comment about top and bot over empty environment being different
michael-schwarz Mar 3, 2024
b0465a2
AffEq: Make `top` and `is_top` consistent
michael-schwarz Mar 3, 2024
171443b
Minimize example
michael-schwarz Mar 3, 2024
6c4742c
make function argument explicit to fix gobview test
stilscher Mar 4, 2024
db019b5
Add RelationPriv TODO from PR #1354
sim642 Mar 4, 2024
cdca6b7
Fix RelationPriv indentation (PR #1354)
sim642 Mar 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/analyses/apron/relationAnalysis.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
sim642 marked this conversation as resolved.
Show resolved Hide resolved

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. *)

Expand Down
36 changes: 25 additions & 11 deletions src/analyses/apron/relationPriv.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 = []
Expand Down Expand Up @@ -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' *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this not just a workaround for the actual bug? Seems like escapes should also contribute to mutex_inits.

BasePriv.PerMutexPrivBase and BasePriv.PerMutexMeetTIDPriv side-effect escapes to mutex_inits at least.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, in the base priv this is all not problematic, as it is non-relational. Here, this all becomes fragile, and I think for now we are wise to avoid the set of variables at global unknowns not only shrinking (due to decreasing protection) but also increasing in non-obvious matters due to escapes also being tracked associated with mutex_inits which is supposed to abstract the state at program start. Maybe this is also something for #1380.

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. *)
Expand Down Expand Up @@ -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. *)
Expand Down Expand Up @@ -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? *)
Expand Down Expand Up @@ -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;
Comment on lines +647 to +649
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This sounds like some bottom-top confusion again: if there are no globals (i.e. the environment is empty), then don't side-effect (i.e. side-effect bottom) instead of side-effecting top.
Conditionally flipping a top to bottom seems inconsistent with all other values.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I still think it's conceptually the right thing to do and not just a hack.
The thing is that we abuse the presence of globals in the relation as a no-overhead way to track whether one of the threads being joined possibly was in single-threaded mode.
If none of these threads was single-threaded (g_vars = []), all initial values are guaranteed to have been published and no side -effect is needed.

Does this make sense? If yes, I can write a comment detailing this reasoning.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The thing is that we abuse the presence of globals in the relation as a no-overhead way to track whether one of the threads being joined possibly was in single-threaded mode.

How so? We explicitly check the MustBeSingleThreaded query right before this. Prior to this, nothing is conditional on g_vars = [].

Copy link
Member

@michael-schwarz michael-schwarz Feb 26, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the case of branched thread creation.

  • Case 0: Both ST (single-threaded), nothing to do.
  • Case 1: One thread is ST, and the other one is not. After the join, Q.MustBeSingleThreaded is false, and the globals from the single-threaded side of the join need need to be published. In this case, potentially, g_vars <> []. If g_vars = [] there are no globals, and not causing a side-effect is ok.
  • Case 2: Both MT, nothing should be done. In this case g_vars = []. Earlier $$\bot$$ was side-effected, now $$\top$$ would be side-effected which we need to protect against.

Copy link
Member

@sim642 sim642 Feb 27, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Being multi-threaded doesn't imply g_vars = [], though.

Special-casing [] to flip the lattice is not a natural extension of the behavior on all other environments. I'm afraid we're setting ourselves up for a similar issue about top-bottom confusion that we're trying to fix here.

Suppose the global unknown has a non-bottom relation $R_{\{x\}}$ (on the environment $\{x\}$) and we're side-effecting $\top_\emptyset$ (on the empty environment). What is the join of these two relations?

  1. $R_{\{x\}} \sqsubseteq R_{\{x\}}$ by reflexivity.
  2. $\top_\emptyset \sqsubseteq R_{\{x\}}$ because $\emptyset \subseteq \{x\}$ and $\top_\emptyset \sqsubseteq R_{\{x\}}\vert_\emptyset = \top_\emptyset$ by the definition of heterogeneous $\sqsubseteq$ (e.g. see the unassume paper) and reflexivity.

It therefore follows that $R_{\{x\}}$ itself is an upper bound of $R_{\{x\}}$ and $\top_\emptyset$. Since it's equal to one of the arguments, it's obviously also the least upper bound of the two.

So side-effecting $\top_\emptyset$ should be a no-op (and this special case is not needed) if we have the right lattice. If it isn't, then we still don't have the lattice fully right. And that is completely independent from whatever thread-modular analysis we might be doing: it's just a relational domain property.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Principled fix is delayed to #1380.

let rel_local = RD.remove_filter rel (fun var ->
match AV.find_metadata var with
| Some (Global g) -> is_unprotected ask g
Expand Down Expand Up @@ -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 () = ()
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/cdomains/apron/affineEqualityDomain.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
9 changes: 5 additions & 4 deletions src/cdomains/apron/apronDomain.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
michael-schwarz marked this conversation as resolved.
Show resolved Hide resolved

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"

Expand Down
28 changes: 28 additions & 0 deletions tests/regression/46-apron2/79-context-insens.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
}
Loading