Merge branch 'goblint:master' into null-byte-arrayDomain

src/analyses/threadAnalysis.ml

@@ -32,13 +32,21 @@ struct
 
   let rec is_not_unique ctx tid =
     let (rep, parents, _) = ctx.global tid in
-    let n = TS.cardinal parents in
-    (* A thread is not unique if it is
-      * a) repeatedly created,
-      * b) created in multiple threads, or
-      * c) created by a thread that is itself multiply created.
-      * Note that starting threads have empty ancestor sets! *)
-    rep || n > 1 || n > 0 && is_not_unique ctx (TS.choose parents)
+    if rep then
+      true (* repeatedly created *)
+    else (
+      let n = TS.cardinal parents in
+      if n > 1 then
+        true (* created in multiple threads *)
+      else if n > 0 then (
+        (* created by single thread *)
+        let parent = TS.choose parents in
+        (* created by itself thread-recursively or by a thread that is itself multiply created *)
+        T.equal tid parent || is_not_unique ctx parent (* equal check needed to avoid infinte self-recursion *)
+      )
+      else
+        false (* no ancestors, starting thread *)
+    )
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     let desc = LibraryFunctions.find f in

src/maingoblint.ml

@@ -417,10 +417,9 @@ let parse_preprocessed preprocessed =
 
   let goblint_cwd = GobFpath.cwd () in
   let get_ast_and_record_deps (preprocessed_file, task_opt) =
-    let transform_file (path_str, system_header) = match path_str with
-      | "<built-in>" | "<command-line>" ->
+    let transform_file (path_str, system_header) = if Str.string_match (Str.regexp "<.+>") path_str 0 then
         (path_str, system_header) (* ignore special "paths" *)
-      | _ ->
+      else
         let path = Fpath.v path_str in
         let path' = if get_bool "pre.transform-paths" then (
             let cwd_opt =
@@ -584,19 +583,19 @@ let do_gobview cilfile =
       let file_dir = Fpath.(run_dir / "files") in
       GobSys.mkdir_or_exists file_dir;
       let file_loc = Hashtbl.create 113 in
-      let counter = ref 0 in
-      let copy path =
+      let copy (path, i) =
         let name, ext = Fpath.split_ext (Fpath.base path) in
-        let unique_name = Fpath.add_ext ext (Fpath.add_ext (string_of_int !counter) name) in
-        counter := !counter + 1;
+        let unique_name = Fpath.add_ext ext (Fpath.add_ext (string_of_int i) name) in
         let dest = Fpath.(file_dir // unique_name) in
         let gobview_path = match Fpath.relativize ~root:run_dir dest with
           | Some p -> Fpath.to_string p
           | None -> failwith "The gobview directory should be a prefix of the paths of c files copied to the gobview directory" in
         Hashtbl.add file_loc (Fpath.to_string path) gobview_path;
-        FileUtil.cp [Fpath.to_string path] (Fpath.to_string dest) in
+        FileUtil.cp [Fpath.to_string path] (Fpath.to_string dest)
+      in
       let source_paths = Preprocessor.FpathH.to_list Preprocessor.dependencies |> List.concat_map (fun (_, m) -> Fpath.Map.fold (fun p _ acc -> p::acc) m []) in
-      List.iter copy source_paths;
+      let source_file_paths = List.filteri_map (fun i e -> if Fpath.is_file_path e then Some (e, i) else None) source_paths in
+      List.iter copy source_file_paths;
       Serialize.marshal file_loc (Fpath.(run_dir / "file_loc.marshalled"));
       (* marshal timing statistics *)
       let stats = Fpath.(run_dir / "stats.marshalled") in

src/solvers/sLRphased.ml

@@ -73,7 +73,7 @@ module Make =
         let effects = ref Set.empty in
         let side y d =
           assert (not (S.Dom.is_bot d));
-          trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
+          if tracing then trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
           let first = not (Set.mem y !effects) in
           effects := Set.add y !effects;
           if first then (
@@ -109,11 +109,11 @@ module Make =
           if wpx then
             if b then
               let nar = narrow old tmp in
-              trace "sol" "NARROW: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
               nar
             else
               let wid = S.Dom.widen old (S.Dom.join old tmp) in
-              trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
+              if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
               wid
           else
             tmp
@@ -163,7 +163,7 @@ module Make =
       and sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
         let v = Enum.fold (fun d z -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) (S.Dom.bot ()) (VS.enum w)
-        in trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
+        in if tracing then trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
       and eq x get set =
         eval_rhs_event x;
         match S.system x with

src/solvers/sLRterm.ml

@@ -64,14 +64,14 @@ module SLR3term =
           HM.replace rho  x (S.Dom.bot ());
           HM.replace infl x (VS.add x VS.empty);
           let c = if side then count_side else count in
-          trace "sol" "INIT: Var: %a with prio %d\n" S.Var.pretty_trace x !c;
+          if tracing then trace "sol" "INIT: Var: %a with prio %d\n" S.Var.pretty_trace x !c;
           HM.replace key x !c; decr c
         end
       in
       let sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
         let v = Enum.fold (fun d z -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) (S.Dom.bot ()) (VS.enum w) in
-        trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
+        if tracing then trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
       in
       let rec iterate b_old prio =
         if H.size !q = 0 || min_key q > prio then ()
@@ -122,7 +122,7 @@ module SLR3term =
           )
           *)
           (* if S.Dom.is_bot d then print_endline "BOT" else *)
-          trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
+          if tracing then trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
           let first = not (Set.mem y !effects) in
           effects := Set.add y !effects;
           if first then (
@@ -156,17 +156,17 @@ module SLR3term =
           if wpx then
             if S.Dom.leq tmp old then (
               let nar = narrow old tmp in
-              trace "sol" "NARROW1: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW1: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
               nar, true
             ) else
             if b_old then (
               let nar = narrow old tmp in
-              trace "sol" "NARROW2: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW2: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
               nar, true
             )
             else (
               let wid = S.Dom.widen old (S.Dom.join old tmp) in
-              trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
+              if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
               wid, false
             )
           else

src/util/cilfacade.ml

@@ -377,7 +377,7 @@ let rec pretty_typsig_like_typ (nameOpt: Pretty.doc option) () ts =
     | _ -> pa
   in
   match ts with
-  | TSBase t -> dn_type () t
+  | TSBase t -> defaultCilPrinter#pType nameOpt () t
   | TSComp (cstruct, cname, a) ->
     let su = if cstruct then "struct" else "union" in
     text (su ^ " " ^ cname ^ " ")

tests/regression/10-synch/07-thread_self_create.c

@@ -0,0 +1,15 @@
+// PARAM: --set ana.activated[+] thread
+// Checks termination of thread analysis with a thread who is its own single parent.
+#include <pthread.h>
+
+void *t_fun(void *arg) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  return 0;
+}

tests/regression/68-longjmp/52-races.c

@@ -0,0 +1,35 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   longjmp(env_buffer, 2);
+   pthread_mutex_unlock(&mutex1);
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+
+   if(!setjmp( env_buffer )) {
+      bar();
+   }
+
+   global = 5; // NORACE
+   pthread_mutex_unlock(&mutex1);
+}

tests/regression/68-longjmp/53-races-no.c

@@ -0,0 +1,36 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global ==3) {
+      longjmp(env_buffer, 2);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+
+   if(!setjmp( env_buffer )) {
+      bar();
+   }
+
+   global = 5; // NORACE
+   pthread_mutex_unlock(&mutex1);
+}

tests/regression/68-longjmp/54-races-actually.c

@@ -0,0 +1,50 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // RACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global == 3) {
+      longjmp(env_buffer, 2);
+   } else {
+      longjmp(env_buffer, 4);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+   int n = 0;
+
+   switch(setjmp( env_buffer )) {
+      case 0:
+         bar();
+         break;
+      case 2:
+         n=1;
+         pthread_mutex_unlock(&mutex1);
+         break;
+      default:
+         break;
+   }
+
+   global = 5; //RACE
+
+   if(n == 0) {
+      pthread_mutex_unlock(&mutex1);
+   }
+}

tests/regression/68-longjmp/55-races-no-return.c

@@ -0,0 +1,50 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; //NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global == 7) {
+      longjmp(env_buffer, 2);
+   } else {
+      longjmp(env_buffer, 4);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+   int n = 0;
+
+   switch(setjmp( env_buffer )) {
+      case 0:
+         bar();
+         break;
+      case 2:
+         n=1;
+         pthread_mutex_unlock(&mutex1);
+         break;
+      default:
+         break;
+   }
+
+   global = 5; //NORACE
+
+   if(n == 0) {
+      pthread_mutex_unlock(&mutex1);
+   }
+}