Improve exp.single-threaded for analysis without threadflag and escape

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

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

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 =

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."

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

src/analyses/raceAnalysis.ml

@@ -321,15 +321,15 @@ 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 =
         let conf = if reach then conf - 20 else conf in
         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

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) =

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)
 

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 =

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

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 =

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

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

tests/regression/00-sanity/42-no-threadflag.c

@@ -0,0 +1,11 @@
+// CRAM
+#include <goblint.h>
+
+int g;
+
+int main() {
+  __goblint_check(g == 0);
+  g = 1;
+  __goblint_check(g == 1);
+  return 0;
+}

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
+

tests/regression/00-sanity/43-no-escape.c

@@ -0,0 +1,13 @@
+// CRAM
+#include <goblint.h>
+
+
+int main() {
+  int x = 0;
+  __goblint_check(x == 0);
+  x = 1;
+  __goblint_check(x == 1);
+
+  int *p = &x; // confuse naive escape check
+  return 0;
+}

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
+

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

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