diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 9e22fff21c..d7c8acbd49 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -102,7 +102,7 @@ struct let sync (ask: Q.ask) getg sideg (st: relation_components_t) reason = let branched_sync () = - if ask.f (Q.MustBeSingleThreaded {since_start = true}) then + if not (ThreadFlag.has_ever_been_multi ask) then st else (* must be like enter_multithreaded *) @@ -351,7 +351,7 @@ struct let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason = let branched_sync () = - if ask.f (Q.MustBeSingleThreaded { since_start= true }) then + if not (ThreadFlag.has_ever_been_multi ask) then st else (* must be like enter_multithreaded *) @@ -647,7 +647,7 @@ struct let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason = let branched_sync () = - if ask.f (Q.MustBeSingleThreaded {since_start = true}) then + if not (ThreadFlag.has_ever_been_multi ask) then st else let rel = st.rel in @@ -1272,7 +1272,7 @@ struct let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason = let branched_sync () = - if ask.f (Q.MustBeSingleThreaded {since_start = true}) then + if not (ThreadFlag.has_ever_been_multi ask) then st else let rel = st.rel in diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index e40db604cf..b56df13c65 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -579,7 +579,7 @@ struct let digest = Digest.current ask in let sidev = GMutex.singleton digest (CPA.singleton x v) in let l' = L.add lm (CPA.singleton x v) l in - let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in + let is_recovered_st = ThreadFlag.has_ever_been_multi ask && not @@ ThreadFlag.is_currently_multi ask in let l' = if is_recovered_st then (* update value of local record for all where it appears *) L.map (update_if_mem x v) l' @@ -705,7 +705,7 @@ struct {st with cpa = CPA.bot (); priv = (W.bot (),lmust,l)} let threadspawn (ask:Queries.ask) get set (st: BaseComponents (D).t) = - let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in + let is_recovered_st = ThreadFlag.has_ever_been_multi ask && not @@ ThreadFlag.is_currently_multi ask in let unprotected_after x = ask.f (Q.MayBePublic {global=x; kind=Write; protection=Weak}) in if is_recovered_st then (* Remove all things that are now unprotected *) diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index b972195bad..1794c1d2eb 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -149,12 +149,14 @@ struct let do_spawns man (xs:(varinfo * (lval option * exp list * bool)) list) = let spawn_one v d = - List.iter (fun (lval, args, multiple) -> man.spawn ~multiple lval v args) d + if get_bool "exp.single-threaded" then ( + M.msg_final Error ~category:Unsound "Thread not spawned"; + M.error ~category:Unsound "Thread not spawned from %a" CilType.Varinfo.pretty v + ) + else + List.iter (fun (lval, args, multiple) -> man.spawn ~multiple lval v args) d in - if get_bool "exp.single-threaded" then - M.msg_final Error ~category:Unsound "Thread not spawned" - else - iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs + iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs let do_sideg man (xs:(V.t * (WideningTokenLifter.TS.t * G.t)) list) = let side_one v dts = diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 133527b1b5..c86f3c4ff6 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -22,9 +22,6 @@ struct let context man _ d = d - let must_be_single_threaded ~since_start man = - man.ask (Queries.MustBeSingleThreaded { since_start }) - let was_malloc_called man = man.global () @@ -142,7 +139,7 @@ struct let warn_for_multi_threaded_due_to_abort man = let malloc_called = was_malloc_called man in - if not (must_be_single_threaded man ~since_start:true) && malloc_called then ( + if ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man) && malloc_called then ( set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program aborted while running in multi-threaded mode. A memory leak might occur" @@ -184,13 +181,14 @@ struct let return man (exp:exp option) (f:fundec) : D.t = (* Check for a valid-memcleanup and memtrack violation in a multi-threaded setting *) (* The check for multi-threadedness is to ensure that valid-memtrack and valid-memclenaup are treated separately for single-threaded programs *) - if (man.ask (Queries.MayBeThreadReturn) && not (must_be_single_threaded man ~since_start:true)) then ( + let ask = Analyses.ask_of_man man in + if man.ask (Queries.MayBeThreadReturn) && ThreadFlag.has_ever_been_multi ask then ( warn_for_thread_return_or_exit man true ); (* Returning from "main" is one possible program exit => need to check for memory leaks *) if f.svar.vname = "main" then ( check_for_mem_leak man; - if not (must_be_single_threaded man ~since_start:false) && was_malloc_called man then begin + if ThreadFlag.is_currently_multi ask && was_malloc_called man then begin set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Possible memory leak: Memory was allocated in a multithreaded program, but not all threads are joined." diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 5875825320..ec85db7caf 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -331,10 +331,10 @@ struct | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound." in let module AD = Queries.AD in - let has_escaped g = oman.ask (Queries.MayEscape g) in + let oask = Analyses.ask_of_man oman in let on_ad ad = let f = function - | AD.Addr.Addr (g,_) when g.vglob || has_escaped g -> old_access (Some g) + | AD.Addr.Addr (g,_) when g.vglob || ThreadEscape.has_escaped oask g -> old_access (Some g) | UnknownPtr -> old_access None | _ -> () in diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index f9aed59f2c..26a6d4ed28 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -321,7 +321,7 @@ struct let acc = part_access None in Access.add_one ~side:(side_access oman {conf; kind; node; exp; acc}) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset) in - let has_escaped g = oman.ask (Queries.MayEscape g) in + let oask = Analyses.ask_of_man oman in (* The following function adds accesses to the lval-set ls -- this is the common case if we have a sound points-to set. *) let on_ad ad includes_uk = @@ -329,7 +329,7 @@ struct let conf = if includes_uk then conf - 10 else conf in let f addr = match addr with - | AD.Addr.Addr (g,o) when g.vglob || has_escaped g -> + | AD.Addr.Addr (g,o) when g.vglob || ThreadEscape.has_escaped oask g -> let coffs = ValueDomain.Offs.to_cil o in add_access conf (Some (g, coffs)) | UnknownPtr -> add_access conf None diff --git a/src/analyses/singleThreadedLifter.ml b/src/analyses/singleThreadedLifter.ml index 3fed5ed222..af2c4aeccf 100644 --- a/src/analyses/singleThreadedLifter.ml +++ b/src/analyses/singleThreadedLifter.ml @@ -7,8 +7,7 @@ module SingleThreadedLifter (S: MCPSpec) = struct include S - let is_multithreaded (ask:Queries.ask) = - not @@ ask.f (MustBeSingleThreaded {since_start = true}) + let is_multithreaded = ThreadFlag.has_ever_been_multi let query ctx = let return_top (type a) (q: a Queries.t) = diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 2bf67f4bb9..f81019f4e6 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -10,6 +10,8 @@ let has_escaped (ask: Queries.ask) (v: varinfo): bool = assert (not v.vglob); if not v.vaddrof then false (* Cannot have escaped without taking address. Override provides extra precision for degenerate ask in base eval_exp used for partitioned arrays. *) + else if GobConfig.get_bool "exp.single-threaded" then + false (* Cannot have escaped if no other threads are assumed to exist. Override provides extra precision for analyzing single-threaded programs without escape analysis. *) else ask.f (Queries.MayEscape v) diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml index 1e0ff7db9f..8e341aed4c 100644 --- a/src/analyses/threadFlag.ml +++ b/src/analyses/threadFlag.ml @@ -6,11 +6,11 @@ open GoblintCil open Analyses let is_currently_multi (ask: Queries.ask): bool = - if !AnalysisState.global_initialization then false else + if !AnalysisState.global_initialization || GobConfig.get_bool "exp.single-threaded" then false else not (ask.f (Queries.MustBeSingleThreaded {since_start = false})) let has_ever_been_multi (ask: Queries.ask): bool = - if !AnalysisState.global_initialization then false else + if !AnalysisState.global_initialization || GobConfig.get_bool "exp.single-threaded" then false else not (ask.f (Queries.MustBeSingleThreaded {since_start = true})) module Spec = diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index cc94866c7e..fa170a5b28 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -34,7 +34,7 @@ struct let warn_for_multi_threaded_access man ?(is_free = false) (heap_var:varinfo) behavior cwe_number = let freeing_threads = man.global heap_var in (* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *) - if man.ask (Queries.MustBeSingleThreaded { since_start = true }) || G.is_empty freeing_threads then () + if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man)) || G.is_empty freeing_threads then () else begin let other_possibly_started current tid joined_threads = match tid with diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 0c51cbaf60..fc7434e6bf 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -471,7 +471,7 @@ struct let d_local = (* if we are multithreaded, we run the risk, that some mutex protected variables got unlocked, so in this case caller state goes to top TODO: !!Unsound, this analysis does not handle this case -> regtest 63 08!! *) - if Queries.AD.is_top tainted || not (man.ask (Queries.MustBeSingleThreaded {since_start = true})) then + if Queries.AD.is_top tainted || ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man) then D.top () else let taint_exp = diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml index ea8572d867..185b6941f7 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/src/analyses/wrapperFunctionAnalysis.ml @@ -176,7 +176,7 @@ module MallocWrapper : MCPSpec = struct | `Lifted tid -> not (Thread.is_unique tid) | _ -> (* The thread analysis may be completely disabled; in this case we fall back on checking whether the program has been single threaded since start *) - not (man.ask (Q.MustBeSingleThreaded {since_start = true})) + ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man) ) | None -> false end diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 6b85a2729c..83b7964fef 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -85,13 +85,13 @@ type _ t = | ReachableFrom: exp -> AD.t t | ReachableUkTypes: exp -> TS.t t | Regions: exp -> LS.t t - | MayEscape: varinfo -> MayBool.t t + | MayEscape: varinfo -> MayBool.t t (** Use via {!ThreadEscape.has_escaped}. *) | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *) | MayBePublicWithout: maybepublicwithout -> MayBool.t t | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t | MustLockset: LockDomain.MustLockset.t t | MustBeAtomic: MustBool.t t - | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t + | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t (** Use via {!ThreadFlag.is_currently_multi} and {!ThreadFlag.has_ever_been_multi}. *) | MustBeUniqueThread: MustBool.t t | CurrentThreadId: ThreadIdDomain.ThreadLifted.t t | ThreadCreateIndexedNode: ThreadNodeLattice.t t diff --git a/tests/regression/00-sanity/42-no-threadflag.c b/tests/regression/00-sanity/42-no-threadflag.c new file mode 100644 index 0000000000..9b1a7689cb --- /dev/null +++ b/tests/regression/00-sanity/42-no-threadflag.c @@ -0,0 +1,11 @@ +// CRAM +#include + +int g; + +int main() { + __goblint_check(g == 0); + g = 1; + __goblint_check(g == 1); + return 0; +} diff --git a/tests/regression/00-sanity/42-no-threadflag.t b/tests/regression/00-sanity/42-no-threadflag.t new file mode 100644 index 0000000000..c67b422c00 --- /dev/null +++ b/tests/regression/00-sanity/42-no-threadflag.t @@ -0,0 +1,48 @@ +Analysis of single-threaded program with threadflag deactivated. +Also no threadid which can tell being single-threaded. + + +With earlyglobs disabled: no threadflag means the same behavior. +Assertions should be unknown, race should be present. + + $ goblint --set ana.activated[-] threadflag --set ana.activated[-] threadid --disable exp.earlyglobs 42-no-threadflag.c + [Warning][Assert] Assertion "g == 0" is unknown. (42-no-threadflag.c:7:3-7:26) + [Warning][Assert] Assertion "g == 1" is unknown. (42-no-threadflag.c:9:3-9:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 5 + dead: 0 + total lines: 5 + [Warning][Race] Memory location g (race with conf. 110): (42-no-threadflag.c:4:5-4:6) + write with mhp:{created={Unknown thread id}} (conf. 110) (exp: & g) (42-no-threadflag.c:8:3-8:8) + read with mhp:{created={Unknown thread id}} (conf. 110) (exp: & g) (42-no-threadflag.c:7:3-7:26) + read with mhp:{created={Unknown thread id}} (conf. 110) (exp: & g) (42-no-threadflag.c:9:3-9:26) + [Info][Race] Memory locations race summary: + safe: 0 + vulnerable: 0 + unsafe: 1 + total memory locations: 1 + + +With single-threaded mode forced. +Assertions should succeed, race should not be present. + + $ goblint --set ana.activated[-] threadflag --set ana.activated[-] threadid --disable exp.earlyglobs --enable exp.single-threaded 42-no-threadflag.c + [Success][Assert] Assertion "g == 0" will succeed (42-no-threadflag.c:7:3-7:26) + [Success][Assert] Assertion "g == 1" will succeed (42-no-threadflag.c:9:3-9:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 5 + dead: 0 + total lines: 5 + + +With single-threaded mode forced, but earlyglobs enabled. +Assertions should be unknown, race should not be present. + + $ goblint --set ana.activated[-] threadflag --set ana.activated[-] threadid --enable exp.earlyglobs --enable exp.single-threaded 42-no-threadflag.c + [Warning][Assert] Assertion "g == 0" is unknown. (42-no-threadflag.c:7:3-7:26) + [Warning][Assert] Assertion "g == 1" is unknown. (42-no-threadflag.c:9:3-9:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 5 + dead: 0 + total lines: 5 + diff --git a/tests/regression/00-sanity/43-no-escape.c b/tests/regression/00-sanity/43-no-escape.c new file mode 100644 index 0000000000..fb57998fdc --- /dev/null +++ b/tests/regression/00-sanity/43-no-escape.c @@ -0,0 +1,13 @@ +// CRAM +#include + + +int main() { + int x = 0; + __goblint_check(x == 0); + x = 1; + __goblint_check(x == 1); + + int *p = &x; // confuse naive escape check + return 0; +} diff --git a/tests/regression/00-sanity/43-no-escape.t b/tests/regression/00-sanity/43-no-escape.t new file mode 100644 index 0000000000..7261ea19fd --- /dev/null +++ b/tests/regression/00-sanity/43-no-escape.t @@ -0,0 +1,29 @@ +Analysis of single-threaded program with escape deactivated. +Also earlyglobs enabled, otherwise MayEscape queries are not used. +Earlyglobs should not matter for local variable. + + +Assertions should be unknown. + + $ goblint --set ana.activated[-] escape --enable exp.earlyglobs 43-no-escape.c + [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global! + [Warning][Assert] Assertion "x == 0" is unknown. (43-no-escape.c:7:3-7:26) + [Warning][Assert] Assertion "x == 1" is unknown. (43-no-escape.c:9:3-9:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + + +With single-threaded mode forced. +Assertions should succeed. + + $ goblint --set ana.activated[-] escape --enable exp.earlyglobs --enable exp.single-threaded 43-no-escape.c + [Warning] Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global! + [Success][Assert] Assertion "x == 0" will succeed (43-no-escape.c:7:3-7:26) + [Success][Assert] Assertion "x == 1" will succeed (43-no-escape.c:9:3-9:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + diff --git a/tests/regression/02-base/32-single-thr.t b/tests/regression/02-base/32-single-thr.t new file mode 100644 index 0000000000..ea000c0150 --- /dev/null +++ b/tests/regression/02-base/32-single-thr.t @@ -0,0 +1,12 @@ + $ goblint --set exp.single-threaded true 32-single-thr.c + [Error][Imprecise][Unsound] Function definition missing for no_spawn (32-single-thr.c:12:3-12:15) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (32-single-thr.c:12:3-12:15) + [Info][Imprecise] Invalidating expressions: & g, (void *)(& f) (32-single-thr.c:12:3-12:15) + [Error][Unsound] Thread not spawned from f (32-single-thr.c:12:3-12:15) + [Warning][Deadcode] Function 'f' is uncalled: 2 LLoC (32-single-thr.c:6:1-8:1) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 4 + dead: 2 (2 in uncalled functions) + total lines: 6 + [Error][Unsound] Thread not spawned + [Error][Imprecise][Unsound] Function definition missing diff --git a/tests/regression/td3/weak-deps.t/run.t b/tests/regression/td3/weak-deps.t/run.t index df51633e13..320de1c1a0 100644 --- a/tests/regression/td3/weak-deps.t/run.t +++ b/tests/regression/td3/weak-deps.t/run.t @@ -1,9 +1,9 @@ $ goblint --set solver td3 --set solvers.td3.weak-deps none -v weak-deps.c 2>&1 | grep 'evals' - [Info] vars = 40 evals = 33 narrow_reuses = 0 + [Info] vars = 34 evals = 33 narrow_reuses = 0 $ goblint --set solver td3 --set solvers.td3.weak-deps eager -v weak-deps.c 2>&1 | grep 'evals' - [Info] vars = 40 evals = 36 narrow_reuses = 0 + [Info] vars = 34 evals = 36 narrow_reuses = 0 $ goblint --set solver td3 --set solvers.td3.weak-deps lazy -v weak-deps.c 2>&1 | grep 'evals' - [Info] vars = 40 evals = 32 narrow_reuses = 0 + [Info] vars = 34 evals = 32 narrow_reuses = 0