From 978b5e6c1cda8cd612f1011d4268e79718b5c931 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Feb 2024 12:21:10 +0100 Subject: [PATCH 01/13] Add failing test case. --- .../regression/46-apron2/61-context-insens.c | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 tests/regression/46-apron2/61-context-insens.c diff --git a/tests/regression/46-apron2/61-context-insens.c b/tests/regression/46-apron2/61-context-insens.c new file mode 100644 index 0000000000..43b7c412cc --- /dev/null +++ b/tests/regression/46-apron2/61-context-insens.c @@ -0,0 +1,46 @@ +// PARAM: --set ana.activated "['base', 'threadid', 'threadflag', 'threadreturn','mallocWrapper','mutexEvents','mutex','access','race','escape','expRelation','assert','var_eq','symb_locks','apron','memLeak']" --enable ana.int.interval_set --set ana.ctx_insens "['base', 'threadid', 'threadflag', 'threadreturn','mallocWrapper','mutexEvents','mutex','access','race','escape','expRelation','assert','var_eq','symb_locks','apron','memLeak']" --enable ana.autotune.enabled --set ana.autotune.activated "['octagon']" --set ana.specification "CHECK( init(main()), LTL(G valid-memcleanup) )" --set ana.path_sens "['mutex', 'malloc_null', 'uninit','expsplit','activeSetjmp','memLeak', 'threadflag']" --set ana.malloc.unique_address_count 5 + +// Adapted from https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/list-properties/list_search-1.c +#include +#include +#include + +typedef struct list { + int key; + struct list *next; +} mlist; + +mlist *head; + +mlist* search(mlist *l, int k){ + l = head; + while(l!=0 && l->key!=k) { // Used to detect dead code after loop head + l = l->next; + } + return l; +} + +int insert(mlist *l, int k){ + l = (mlist*)malloc(sizeof(mlist)); + l->key = k; + if (head==0) { + } else { + l->key = k; + l->next = head; + } + head = l; + return 0; +} + +int main(void){ + int i; + mlist *mylist, *temp; + insert(mylist,2); + insert(mylist,5); + + temp = search(head,2); + + __goblint_check(1); // Should be reachable + return 0; +} + From 554a5f03a94b09aae1d17277ebb8ba9bc3a7f0cc Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Feb 2024 12:29:29 +0100 Subject: [PATCH 02/13] apronDomain.join: Check for is_bot_env instead of is_bot. is_bot returned true for some elements for which is_top_env returned true, leading to too small values being returned. --- src/cdomains/apron/apronDomain.apron.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index e78176fc41..01827d9437 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -672,9 +672,9 @@ struct let join x y = (* just to optimize joining folds, which start with bot *) - if is_bot x then (* TODO: also for non-empty env *) + if is_bot_env x then (* TODO: also for non-empty env *) y - else if is_bot y then (* TODO: also for non-empty env *) + else if is_bot_env y then (* TODO: also for non-empty env *) x else ( if M.tracing then M.traceli "apron" "join %a %a\n" pretty x pretty y; From 231179560acf80a20dade058eb3285e7d34fe07c Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Feb 2024 18:09:21 +0100 Subject: [PATCH 03/13] Define bot and top in apron domain correctly. --- src/analyses/apron/relationAnalysis.apron.ml | 6 +++--- src/cdomains/apron/apronDomain.apron.ml | 10 +++++----- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index ea570b338a..3b752a7b53 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/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 01827d9437..f60790845b 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -660,21 +660,21 @@ struct let empty_env = Environment.make [||] [||] 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_top = equal (top ()) let strengthening_enabled = GobConfig.get_bool "ana.apron.strengthening" let join x y = (* just to optimize joining folds, which start with bot *) - if is_bot_env x then (* TODO: also for non-empty env *) + if is_bot x then (* TODO: also for non-empty env *) y - else if is_bot_env y then (* TODO: also for non-empty env *) + else if is_bot y then (* TODO: also for non-empty env *) x else ( if M.tracing then M.traceli "apron" "join %a %a\n" pretty x pretty y; From 8848276821cf785b3106cfb29afccfb9351235b7 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Feb 2024 18:31:47 +0100 Subject: [PATCH 04/13] Adapt relationPriv for bot being proper bot. --- src/analyses/apron/relationPriv.apron.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index b4e23b65cc..669bf1e9a5 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 = [] @@ -599,7 +599,7 @@ struct 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 () = () @@ -732,7 +732,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; @@ -1075,7 +1075,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 From d2ffcf02e35c53aea55c3e79e3845d5ea1dcfd33 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 18 Feb 2024 15:35:47 +0100 Subject: [PATCH 05/13] Do not side-effect empty relationship --- src/analyses/apron/relationPriv.apron.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 669bf1e9a5..321025d2e2 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -565,7 +565,9 @@ struct ) (RD.vars rel) in let rel_side = RD.keep_vars rel g_vars in - sideg V.mutex_inits rel_side; + (* 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 From b57fd0ff52e3a52052c8d75885ffb344f50b46e1 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 18 Feb 2024 16:19:47 +0100 Subject: [PATCH 06/13] Fix escape handling --- src/analyses/apron/relationPriv.apron.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 321025d2e2..47593a8aa3 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -480,7 +480,11 @@ struct let get_mutex_inits = getg V.mutex_inits in let g_var = AV.global g 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 + (* 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 read_global ask getg (st: relation_components_t) g x: RD.t = let rel = st.rel in @@ -500,10 +504,11 @@ struct in rel_local' - let write_global ?(invariant=false) 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 getg sideg (st: relation_components_t) g x: relation_components_t = let rel = st.rel in (* lock *) - let rel = RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g) in + let rel = if not skip_meet then RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g) else rel in (* write *) let g_var = AV.global g in let x_var = AV.local x in @@ -520,6 +525,9 @@ struct in {st with rel = rel_local'} + 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 = (* TODO: somehow actually unneeded here? *) if Locksets.(not (Lockset.mem m (current_lockset ask))) then ( @@ -597,7 +605,7 @@ 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 = From 8787f5942a197bdde612388dda75f40584b70de9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 18 Feb 2024 16:29:02 +0100 Subject: [PATCH 07/13] Add a top to `affeq`? --- src/cdomains/apron/affineEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index ea8a350d3c..55589c6741 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -307,7 +307,7 @@ 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 From 5f7ce7f4fc4bbd7421aebd0e75db05163426e643 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 3 Mar 2024 11:56:06 +0100 Subject: [PATCH 08/13] Comment about top and bot over empty environment being different --- src/cdomains/apron/apronDomain.apron.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index f30030efef..fbfddbe94d 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -659,6 +659,7 @@ 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 () = bot_env empty_env From b0465a2d97efbdaff7629c3d2245ee995221b2ba Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 3 Mar 2024 12:26:04 +0100 Subject: [PATCH 09/13] AffEq: Make `top` and `is_top` consistent --- src/cdomains/apron/affineEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index ed6f2c5936..944515f4ec 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -307,7 +307,7 @@ struct 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 From 171443be205930cb470ca742605f4b007a732b08 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 3 Mar 2024 13:21:44 +0100 Subject: [PATCH 10/13] Minimize example --- .../regression/46-apron2/79-context-insens.c | 42 ++++++------------- 1 file changed, 12 insertions(+), 30 deletions(-) diff --git a/tests/regression/46-apron2/79-context-insens.c b/tests/regression/46-apron2/79-context-insens.c index 43b7c412cc..822caae414 100644 --- a/tests/regression/46-apron2/79-context-insens.c +++ b/tests/regression/46-apron2/79-context-insens.c @@ -1,46 +1,28 @@ -// PARAM: --set ana.activated "['base', 'threadid', 'threadflag', 'threadreturn','mallocWrapper','mutexEvents','mutex','access','race','escape','expRelation','assert','var_eq','symb_locks','apron','memLeak']" --enable ana.int.interval_set --set ana.ctx_insens "['base', 'threadid', 'threadflag', 'threadreturn','mallocWrapper','mutexEvents','mutex','access','race','escape','expRelation','assert','var_eq','symb_locks','apron','memLeak']" --enable ana.autotune.enabled --set ana.autotune.activated "['octagon']" --set ana.specification "CHECK( init(main()), LTL(G valid-memcleanup) )" --set ana.path_sens "['mutex', 'malloc_null', 'uninit','expsplit','activeSetjmp','memLeak', 'threadflag']" --set ana.malloc.unique_address_count 5 +// 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 -#include #include -typedef struct list { +typedef struct thing { int key; - struct list *next; -} mlist; +} thing; -mlist *head; +thing *container; -mlist* search(mlist *l, int k){ - l = head; - while(l!=0 && l->key!=k) { // Used to detect dead code after loop head - l = l->next; - } - return l; -} - -int insert(mlist *l, int k){ - l = (mlist*)malloc(sizeof(mlist)); - l->key = k; - if (head==0) { - } else { - l->key = k; - l->next = head; - } - head = l; +int insert(int k __attribute__((__goblint_relation_track__))) { + container = (thing*) malloc(sizeof(thing)); + container->key = k; return 0; } int main(void){ - int i; - mlist *mylist, *temp; - insert(mylist,2); - insert(mylist,5); + insert(2); + insert(5); - temp = search(head,2); + if(container !=0) { // Used to detect dead code after loop head + + } __goblint_check(1); // Should be reachable return 0; } - From 6c4742cd00186c02f3d451eac2051fb60180f402 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 4 Mar 2024 13:55:08 +0100 Subject: [PATCH 11/13] make function argument explicit to fix gobview test --- src/cdomains/apron/apronDomain.apron.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index fbfddbe94d..158d3ca907 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -666,8 +666,8 @@ struct let top () = top_env empty_env - let is_bot = equal (bot ()) - let is_top = equal (top ()) + let is_bot x = equal (bot ()) x + let is_top x = equal (top ()) x let strengthening_enabled = GobConfig.get_bool "ana.apron.strengthening" From db019b50ac0a5dddb69d7ca5d82fe662accf0484 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 4 Mar 2024 17:39:21 +0200 Subject: [PATCH 12/13] Add RelationPriv TODO from PR #1354 --- src/analyses/apron/relationPriv.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 206e6417df..2383cad5f9 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -489,7 +489,7 @@ struct in let get_mutex_inits = getg V.mutex_inits in let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in - if not (RD.mem_var get_mutex_inits' g_var) then + 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 From cdca6b7c03a4fd5b50cb6d95019097273ff658ca Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 4 Mar 2024 17:39:35 +0200 Subject: [PATCH 13/13] Fix RelationPriv indentation (PR #1354) --- src/analyses/apron/relationPriv.apron.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 2383cad5f9..5e78a02153 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -638,10 +638,10 @@ struct let rel = st.rel in (* 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) + match AV.find_metadata var with + | Some (Global _) -> true + | _ -> false + ) (RD.vars rel) in let rel_side = RD.keep_vars rel g_vars in (* If no globals are contained here, none need to be published *)