diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index f0b2a45701..74e45f9aa0 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -466,32 +466,23 @@ struct (* Give the set of reachables from argument. *) let reachables (ask: Queries.ask) es = - let reachable acc e = - Option.bind acc (fun st -> - let ad = ask.f (Queries.ReachableFrom e) in - if Queries.AD.is_top ad then - None - else - Some (Queries.AD.join ad st)) + let reachable st e = + let ad = ask.f (Queries.ReachableFrom e) in + Queries.AD.join ad st in - List.fold_left reachable (Some (Queries.AD.empty ())) es + List.fold_left reachable (Queries.AD.empty ()) es 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 *) - let to_cil_lval x = Option.map Cil.var @@ RV.to_cil_varinfo x in - RD.vars st.rel |> List.filter_map to_cil_lval - | 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 @@ -512,6 +503,36 @@ struct if RD.is_bot_env res then raise Deadcode; {st with rel = res} + let special_unknown_invalidate man f args = + (* 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 + 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 man.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 man man.local deep_addrs in + let shallow_lvals = List.concat_map lvallist shallow_addrs in + List.fold_left (invalidate_one (Analyses.ask_of_man man) man) st' shallow_lvals + + let special man r f args = let ask = Analyses.ask_of_man man in let st = man.local in @@ -542,31 +563,7 @@ struct assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true ) st r | _, _ -> - 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 man st deep_addrs in - let shallow_lvals = List.concat_map lvallist shallow_addrs in - let st' = List.fold_left (invalidate_one ask man) st' shallow_lvals in + let st' = special_unknown_invalidate man f args in (* invalidate lval if present *) Option.map_default (invalidate_one ask man st') st' r @@ -669,21 +666,19 @@ struct let threadenter man ~multiple lval f args = let st = man.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_man man)) then + ignore (Priv.enter_multithreaded (Analyses.ask_of_man man) man.global man.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_man man)) then - ignore (Priv.enter_multithreaded (Analyses.ask_of_man man) man.global man.sideg st); let st' = Priv.threadenter (Analyses.ask_of_man man) man.global st in let new_rel = make_callee_rel ~thread:true man 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 man f args] let threadspawn man ~multiple lval f args fman = man.local 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] diff --git a/tests/regression/46-apron2/93-invalidate-more.c b/tests/regression/46-apron2/93-invalidate-more.c new file mode 100644 index 0000000000..acf3944b10 --- /dev/null +++ b/tests/regression/46-apron2/93-invalidate-more.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); + + // Use to fail as debug was invalidated + __goblint_check(debug <= 3); + return 0; +} 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..1a2814a6a2 --- /dev/null +++ b/tests/regression/46-apron2/94-weird.t @@ -0,0 +1,19 @@ +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 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) + [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 + [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