From 508d7e2ca658541859e1a867a87579a8c31fb5d7 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 6 Jul 2024 17:02:44 +0200 Subject: [PATCH 1/9] Use same invalidation strategy as base (References #1535) --- src/analyses/apron/relationAnalysis.apron.ml | 7 +++---- tests/regression/46-apron2/98-invalidate.c | 22 ++++++++++++++++++++ 2 files changed, 25 insertions(+), 4 deletions(-) create mode 100644 tests/regression/46-apron2/98-invalidate.c diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index df3cf545c5..f2ea577527 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -469,10 +469,9 @@ struct | None -> None | Some st -> let ad = ask.f (Queries.ReachableFrom e) in - if Queries.AD.is_top ad then - None - else - Some (Queries.AD.join ad st) + (* See https://github.com/goblint/analyzer/issues/1535 *) + let ad = Queries.AD.remove UnknownPtr ad in + Some (Queries.AD.join ad st) in List.fold_right reachable es (Some (Queries.AD.empty ())) diff --git a/tests/regression/46-apron2/98-invalidate.c b/tests/regression/46-apron2/98-invalidate.c new file mode 100644 index 0000000000..948b70e3ce --- /dev/null +++ b/tests/regression/46-apron2/98-invalidate.c @@ -0,0 +1,22 @@ +// SKIP PARAM: --set ana.activated[+] apron --set sem.int.signed_overflow assume_none +#include +#include +#include + +int debug; +int other; + +int main() { + int top; + + // Needed so Base & DefExc doesn't find this information because it invalidates less + if(top) { + debug = 3; + } + + fscanf(stdin, "%d", &other); + + // Fails as debug is invalidated + __goblint_check(debug <= 3); + return 0; +} From 406ad227e1f2b53507e7c76765aafd75da10c0e5 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 17 Dec 2024 16:30:39 +0100 Subject: [PATCH 2/9] Make name unique? --- .../46-apron2/{98-invalidate.c => 98-invalidate-more.c} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename tests/regression/46-apron2/{98-invalidate.c => 98-invalidate-more.c} (100%) diff --git a/tests/regression/46-apron2/98-invalidate.c b/tests/regression/46-apron2/98-invalidate-more.c similarity index 100% rename from tests/regression/46-apron2/98-invalidate.c rename to tests/regression/46-apron2/98-invalidate-more.c From 563a5b1a7ca8be17398ef87f0c58ea0e0812b0e8 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 17 Dec 2024 16:44:02 +0100 Subject: [PATCH 3/9] Support for `threadenter` for unknown function --- src/analyses/apron/relationAnalysis.apron.ml | 72 +++++++++++--------- 1 file changed, 38 insertions(+), 34 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index f2ea577527..2c026de389 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -512,6 +512,36 @@ struct if RD.is_bot_env res then raise Deadcode; {st with rel = res} + + let special_unknown_invalidate ctx f args = + (* No warning here, base already prodcues the appropriate warnings *) + let desc = LibraryFunctions.find f in + let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in + let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in + let deep_addrs = + if List.mem LibraryDesc.InvalidateGlobals desc.attrs then ( + foldGlobals !Cilfacade.current_file (fun acc global -> + match global with + | GVar (vi, _, _) when not (BaseUtil.is_static vi) -> + mkAddrOf (Var vi, NoOffset) :: acc + (* TODO: what about GVarDecl? *) + | _ -> acc + ) deep_addrs + ) + else + deep_addrs + in + let lvallist e = + match ctx.ask (Queries.MayPointTo e) with + | ad when Queries.AD.is_top ad -> [] + | ad -> + Queries.AD.to_mval ad + |> List.map ValueDomain.Addr.Mval.to_cil + in + let st' = forget_reachable ctx ctx.local deep_addrs in + let shallow_lvals = List.concat_map lvallist shallow_addrs in + List.fold_left (invalidate_one (Analyses.ask_of_ctx ctx) ctx) st' shallow_lvals + let special ctx r f args = let ask = Analyses.ask_of_ctx ctx in let st = ctx.local in @@ -547,31 +577,7 @@ struct assert_fn {ctx with local = st} (BinOp (Ge, Lval lv, zero, intType)) true | None -> st) | _, _ -> - let lvallist e = - match ask.f (Queries.MayPointTo e) with - | ad when Queries.AD.is_top ad -> [] - | ad -> - Queries.AD.to_mval ad - |> List.map ValueDomain.Addr.Mval.to_cil - in - let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in - let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in - let deep_addrs = - if List.mem LibraryDesc.InvalidateGlobals desc.attrs then ( - foldGlobals !Cilfacade.current_file (fun acc global -> - match global with - | GVar (vi, _, _) when not (BaseUtil.is_static vi) -> - mkAddrOf (Var vi, NoOffset) :: acc - (* TODO: what about GVarDecl? *) - | _ -> acc - ) deep_addrs - ) - else - deep_addrs - in - let st' = forget_reachable ctx st deep_addrs in - let shallow_lvals = List.concat_map lvallist shallow_addrs in - let st' = List.fold_left (invalidate_one ask ctx) st' shallow_lvals in + let st' = special_unknown_invalidate ctx f args in (* invalidate lval if present *) match r with | Some lv -> invalidate_one ask ctx st' lv @@ -673,21 +679,19 @@ struct let threadenter ctx ~multiple lval f args = let st = ctx.local in + (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread. + Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published... + sync `Thread doesn't help us here, it's not specific to entering multithreaded mode. + EnterMultithreaded events only execute after threadenter and threadspawn. *) + if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then + ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st); match Cilfacade.find_varinfo_fundec f with | fd -> - (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread. - Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published... - sync `Thread doesn't help us here, it's not specific to entering multithreaded mode. - EnterMultithreaded events only execute after threadenter and threadspawn. *) - if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then - ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st); let st' = Priv.threadenter (Analyses.ask_of_ctx ctx) ctx.global st in let new_rel = make_callee_rel ~thread:true ctx fd args in [{st' with rel = new_rel}] | exception Not_found -> - (* Unknown functions *) - (* TODO: do something like base? *) - failwith "relation.threadenter: unknown function" + [special_unknown_invalidate ctx f args] let threadspawn ctx ~multiple lval f args fctx = ctx.local From e03a6f71adf7ca7b10ec9b1782813ee441fb7ae9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 30 Dec 2024 17:04:21 +0100 Subject: [PATCH 4/9] Update comment --- tests/regression/46-apron2/98-invalidate-more.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/46-apron2/98-invalidate-more.c b/tests/regression/46-apron2/98-invalidate-more.c index 948b70e3ce..acf3944b10 100644 --- a/tests/regression/46-apron2/98-invalidate-more.c +++ b/tests/regression/46-apron2/98-invalidate-more.c @@ -16,7 +16,7 @@ int main() { fscanf(stdin, "%d", &other); - // Fails as debug is invalidated + // Use to fail as debug was invalidated __goblint_check(debug <= 3); return 0; } From bb534ffe0ffbb9f244bb84559be30fb9f25cc52a Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 30 Dec 2024 17:27:24 +0100 Subject: [PATCH 5/9] Simplify invalidation Co-authored-by: Simmo Saan --- src/analyses/apron/relationAnalysis.apron.ml | 31 +++++++------------- 1 file changed, 10 insertions(+), 21 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 278f3d70aa..6cae4a3f69 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -465,33 +465,22 @@ struct (* Give the set of reachables from argument. *) let reachables (ask: Queries.ask) es = let reachable e st = - match st with - | None -> None - | Some st -> - let ad = ask.f (Queries.ReachableFrom e) in - (* See https://github.com/goblint/analyzer/issues/1535 *) - let ad = Queries.AD.remove UnknownPtr ad in - Some (Queries.AD.join ad st) + let ad = ask.f (Queries.ReachableFrom e) in + Queries.AD.join ad st in - List.fold_right reachable es (Some (Queries.AD.empty ())) + List.fold_right reachable es (Queries.AD.empty ()) let forget_reachable man st es = let ask = Analyses.ask_of_man man in let rs = - match reachables ask es with - | None -> - (* top reachable, so try to invalidate everything *) - RD.vars st.rel - |> List.filter_map RV.to_cil_varinfo - |> List.map Cil.var - | Some ad -> - let to_cil addr rs = - match addr with - | Queries.AD.Addr.Addr mval -> (ValueDomain.Addr.Mval.to_cil mval) :: rs - | _ -> rs - in - Queries.AD.fold to_cil ad [] + let ad = reachables ask es in + let to_cil addr rs = + match addr with + | Queries.AD.Addr.Addr mval -> (ValueDomain.Addr.Mval.to_cil mval) :: rs + | _ -> rs + in + Queries.AD.fold to_cil ad [] in List.fold_left (fun st lval -> invalidate_one ask man st lval From 2accba23c0a21ead48b08bf80fdd9590a6b25f37 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 15 Jul 2025 16:33:05 +0200 Subject: [PATCH 6/9] Typo --- src/analyses/apron/relationAnalysis.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 941709745d..74e45f9aa0 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -504,7 +504,7 @@ struct {st with rel = res} let special_unknown_invalidate man f args = - (* No warning here, base already prodcues the appropriate warnings *) + (* No warning here, base already produces the appropriate warnings *) let desc = LibraryFunctions.find f in let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in From 9bbe9d3d7a23b8f4edc3efa5d25cdf6774dd46c6 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 15 Jul 2025 17:31:57 +0200 Subject: [PATCH 7/9] Add cram test --- tests/regression/46-apron2/94-weird.c | 15 +++++++++++++ tests/regression/46-apron2/94-weird.t | 26 +++++++++++++++++++++ tests/regression/46-apron2/94-weird.yml | 30 +++++++++++++++++++++++++ 3 files changed, 71 insertions(+) create mode 100644 tests/regression/46-apron2/94-weird.c create mode 100644 tests/regression/46-apron2/94-weird.t create mode 100644 tests/regression/46-apron2/94-weird.yml diff --git a/tests/regression/46-apron2/94-weird.c b/tests/regression/46-apron2/94-weird.c new file mode 100644 index 0000000000..b8b2f720bd --- /dev/null +++ b/tests/regression/46-apron2/94-weird.c @@ -0,0 +1,15 @@ +// CRAM SKIP +#include +pthread_mutex_t c; +int d, e, f; + +void b(void* arg); + +void main(int argc, char *argv) { + pthread_t t; + e = pthread_create(&t, 0, b, &f); + pthread_mutex_lock(&c); + d++; + pthread_mutex_unlock(&c); + pthread_mutex_lock(&c); +} diff --git a/tests/regression/46-apron2/94-weird.t b/tests/regression/46-apron2/94-weird.t new file mode 100644 index 0000000000..3b9891b909 --- /dev/null +++ b/tests/regression/46-apron2/94-weird.t @@ -0,0 +1,26 @@ +Check that the invariant (long long )f + 2147483648LL >= (long long )e is not confirmed, as it presumes information about f and e which are supposed to be invalidated + $ goblint --set ana.activated[+] apron --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.loop-head --disable sem.unknown_function.invalidate.globals --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.entry-types[*] invariant_set --set witness.yaml.validate 94-weird.yml 94-weird.c + [Info][Imprecise] Invalidating expressions: & e (94-weird.c:10:3-10:35) + [Error][Imprecise][Unsound] Function definition missing for b (94-weird.c:10:3-10:35) + [Info][Imprecise] Invalidating expressions: (void * __restrict )(& f) (94-weird.c:10:3-10:35) + [Error][Imprecise][Unsound] Created a thread from unknown function b (94-weird.c:10:3-10:35) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Warning][Witness] invariant unconfirmed: (long long )f + 2147483648LL >= (long long )e (94-weird.c:11:3) + [Info][Witness] witness validation summary: + confirmed: 0 + unconfirmed: 1 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 1 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/46-apron2/94-weird.yml b/tests/regression/46-apron2/94-weird.yml new file mode 100644 index 0000000000..cd34def6d5 --- /dev/null +++ b/tests/regression/46-apron2/94-weird.yml @@ -0,0 +1,30 @@ +- entry_type: invariant_set + metadata: + format_version: "2.0" + uuid: 271d28bc-9fe6-4b18-9b7c-6bb68c7d5dcf + creation_time: 2025-07-15T14:56:13Z + producer: + name: Goblint + version: heads/issue_1535-0-g2accba23c-dirty + command_line: '''./goblint'' ''--conf'' ''conf/traces-rel.json'' ''--set'' ''ana.activated[+]'' + ''threadJoins'' ''--set'' ''ana.activated[+]'' ''apron'' ''--set'' ''ana.path_sens[+]'' + ''threadflag'' ''--set'' ''ana.relation.privatization'' ''mutex-meet-tid'' + ''2.c'' ''--sets'' ''exp.relation.prec-dump'' ''cluster.prec'' ''--html'' + ''--enable'' ''witness.yaml.enabled'' ''--set'' ''witness.yaml.path'' ''1.yml''' + task: + input_files: + - 94-weird.c + input_file_hashes: + 94-weird.c: c67808107b2da394e33439894ea1ae3c5e5c3628a08c9371eaa31ee3efbc8414 + data_model: LP64 + language: C + content: + - invariant: + type: location_invariant + location: + file_name: 94-weird.c + line: 11 + column: 3 + function: main + value: (long long )f + 2147483648LL >= (long long )e + format: c_expression From 7f6c92bee91235c12106dfa2819bc75ee57de02e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 15 Jul 2025 17:40:33 +0200 Subject: [PATCH 8/9] Base `threadenter`: `enter_multithreaded` also for `special_unknown_invalidate` --- src/analyses/base.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 221ac08073..067fbeb1ac 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2150,12 +2150,6 @@ struct (* TODO: make this is_private PrivParam dependent? PerMutexOplusPriv should keep *) let st' = if thread then ( - (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread. - Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published... - sync `Thread doesn't help us here, it's not specific to entering multithreaded mode. - EnterMultithreaded events only execute after threadenter and threadspawn. *) - if not (ThreadFlag.has_ever_been_multi ask) then - ignore (Priv.enter_multithreaded ask (priv_getg man.global) (priv_sideg man.sideg) st); Priv.threadenter ask st ) else (* use is_global to account for values that became globals because they were saved into global variables *) @@ -2967,6 +2961,13 @@ struct combine_one man.local after let threadenter man ~multiple (lval: lval option) (f: varinfo) (args: exp list): D.t list = + (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread. + Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published... + sync `Thread doesn't help us here, it's not specific to entering multithreaded mode. + EnterMultithreaded events only execute after threadenter and threadspawn. *) + let st = man.local in + if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man)) then + ignore (Priv.enter_multithreaded (Analyses.ask_of_man man) (priv_getg man.global) (priv_sideg man.sideg) st); match Cilfacade.find_varinfo_fundec f with | fd -> [make_entry ~thread:true man fd args] From 44a28627e4b8bbc4ee68f28ca1e98c23c30b77f7 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 16 Jul 2025 10:18:21 +0200 Subject: [PATCH 9/9] 46/94: Disable warnings so they align on OS X and Linux --- tests/regression/46-apron2/94-weird.t | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/tests/regression/46-apron2/94-weird.t b/tests/regression/46-apron2/94-weird.t index 3b9891b909..1a2814a6a2 100644 --- a/tests/regression/46-apron2/94-weird.t +++ b/tests/regression/46-apron2/94-weird.t @@ -1,8 +1,6 @@ Check that the invariant (long long )f + 2147483648LL >= (long long )e is not confirmed, as it presumes information about f and e which are supposed to be invalidated - $ goblint --set ana.activated[+] apron --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.loop-head --disable sem.unknown_function.invalidate.globals --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.entry-types[*] invariant_set --set witness.yaml.validate 94-weird.yml 94-weird.c - [Info][Imprecise] Invalidating expressions: & e (94-weird.c:10:3-10:35) + $ goblint --set dbg.level warning --disable warn.imprecise --disable warn.race --set ana.activated[+] apron --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.loop-head --disable sem.unknown_function.invalidate.globals --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.entry-types[*] invariant_set --set witness.yaml.validate 94-weird.yml 94-weird.c [Error][Imprecise][Unsound] Function definition missing for b (94-weird.c:10:3-10:35) - [Info][Imprecise] Invalidating expressions: (void * __restrict )(& f) (94-weird.c:10:3-10:35) [Error][Imprecise][Unsound] Created a thread from unknown function b (94-weird.c:10:3-10:35) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 @@ -18,9 +16,4 @@ Check that the invariant (long long )f + 2147483648LL >= (long long )e is not co unsupported: 0 disabled: 0 total validation entries: 1 - [Info][Race] Memory locations race summary: - safe: 1 - vulnerable: 0 - unsafe: 0 - total memory locations: 1 [Error][Imprecise][Unsound] Function definition missing