Merge branch 'master' into queries-ad

dune-project

@@ -44,7 +44,7 @@
     (fileutils (>= 0.6.4))
     cpu
     arg-complete
-    yaml
+    (yaml (>= 3.0.0))
     uuidm
     catapult
     catapult-file

goblint.opam

@@ -41,7 +41,7 @@ depends: [
   "fileutils" {>= "0.6.4"}
   "cpu"
   "arg-complete"
-  "yaml"
+  "yaml" {>= "3.0.0"}
   "uuidm"
   "catapult"
   "catapult-file"

src/analyses/base.ml

@@ -2289,15 +2289,17 @@ struct
           let countval = eval_int (Analyses.ask_of_ctx ctx) gs st n in
           if ID.to_int countval = Some Z.one then (
             set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
-              add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false);
-              eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var))
+              (add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false));
+              (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var)))
             ]
           )
           else (
             let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
             (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
-            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
-                                                          (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
+              (add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
+              (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))
+            ]
           )
         | _ -> st
       end

src/analyses/libraryFunctions.ml

@@ -196,6 +196,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("unsetenv", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]);
     ("lseek", unknown [drop "fd" []; drop "offset" []; drop "whence" []]);
     ("fcntl", unknown (drop "fd" [] :: drop "cmd" [] :: VarArgs (drop' [r; w])));
+    ("__open_missing_mode", unknown []);
     ("fseeko", unknown [drop "stream" [r_deep; w_deep]; drop "offset" []; drop "whence" []]);
     ("fileno", unknown [drop "stream" [r_deep; w_deep]]);
     ("fdopen", unknown [drop "fd" []; drop "mode" [r]]);
@@ -287,6 +288,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("ftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []]); (* TODO: use Call instead of Spawn *)
     ("nftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []; drop "flags" []]); (* TODO: use Call instead of Spawn *)
     ("getaddrinfo", unknown [drop "node" [r]; drop "service" [r]; drop "hints" [r_deep]; drop "res" [w]]); (* only write res non-deep because it doesn't write to existing fields of res *)
+    ("fnmatch", unknown [drop "pattern" [r]; drop "string" [r]; drop "flags" []]);
   ]
 
 (** Pthread functions. *)
@@ -352,6 +354,8 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]);
     ("pthread_attr_setschedparam", unknown [drop "attr" [r; w]; drop "param" [r]]);
     ("sem_timedwait", unknown [drop "sem" [r]; drop "abs_timeout" [r]]); (* no write accesses to sem because sync primitive itself has no race *)
+    ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]);
+    ("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]);
   ]
 
 (** GCC builtin functions.
@@ -462,6 +466,7 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("sysinfo", unknown [drop "info" [w_deep]]);
     ("__xpg_basename", unknown [drop "path" [r]]);
     ("ptrace", unknown (drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); (* man page has 4 arguments, but header has varargs and real-world programs may call with <4 *)
+    ("madvise", unknown [drop "addr" []; drop "length" []; drop "advice" []]);
   ]
 
 let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType)))
@@ -811,6 +816,15 @@ let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("wbkgd", unknown [drop "win" [r_deep; w_deep]; drop "ch" []]);
   ]
 
+let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("pcre_compile", unknown [drop "pattern" [r]; drop "options" []; drop "errptr" [w]; drop "erroffset" [w]; drop "tableptr" [r]]);
+    ("pcre_compile2", unknown [drop "pattern" [r]; drop "options" []; drop "errorcodeptr" [w]; drop "errptr" [w]; drop "erroffset" [w]; drop "tableptr" [r]]);
+    ("pcre_config", unknown [drop "what" []; drop "where" [w]]);
+    ("pcre_exec", unknown [drop "code" [r_deep]; drop "extra" [r_deep]; drop "subject" [r]; drop "length" []; drop "startoffset" []; drop "options" []; drop "ovector" [w]; drop "ovecsize" []]);
+    ("pcre_study", unknown [drop "code" [r_deep]; drop "options" []; drop "errptr" [w]]);
+    ("pcre_version", unknown []);
+  ]
+
 let libraries = Hashtbl.of_list [
     ("c", c_descs_list @ math_descs_list);
     ("posix", posix_descs_list);
@@ -823,6 +837,7 @@ let libraries = Hashtbl.of_list [
     ("sv-comp", svcomp_descs_list);
     ("ncurses", ncurses_descs_list);
     ("zstd", zstd_descs_list);
+    ("pcre", pcre_descs_list);
   ]
 
 let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t =

src/analyses/raceAnalysis.ml

@@ -3,6 +3,128 @@
 open GoblintCil
 open Analyses
 
+(** Data race analysis with tries for offsets and type-based memory locations for open code.
+
+    Accesses are to memory locations ({{!Access.Memo} memos}) which consist of a root and offset.
+    {{!Access.MemoRoot} Root} can be:
+    + variable, if access is to known global variable or alloc-variable;
+    + type, if access is to unknown pointer.
+
+    Accesses are (now) collected to sets for each corresponding memo,
+    after points-to sets are resolved, during postsolving.
+
+    Race checking is performed per-memo,
+    except must additionally account for accesses to other memos (see diagram below):
+    + access to [s.f] can race with access to a prefix like [s], which writes an entire struct at once;
+    + access to [s.f] can race with type-based access like [(struct S).f];
+    + access to [(struct S).f] can race with type-based access to a suffix like [(int)].
+    + access to [(struct T).s.f] can race with type-based access like [(struct S)], which is a combination of the above.
+
+    These are accounted for lazily (unlike in the past).
+
+    Prefixes (a.k.a. inner distribution) are handled using a trie data structure enriched with lattice properties.
+    Race checking starts at the root and passes accesses to ancestor nodes down to children.
+
+    Type suffixes (a.k.a. outer distribution) are handled by computing successive immediate type suffixes transitively
+    and accessing corresponding offsets from corresponding root tries in the global invariant.
+
+    Type suffix prefixes (for the combination of the two) are handled by passing type suffix accesses down when traversing the prefix trie.
+
+    Race checking happens at each trie node with the above three access sets at hand using {!Access.group_may_race}.
+    All necessary combinations between the four classes are handled, but unnecessary repeated work is carefully avoided.
+    E.g. accesses which are pairwise checked at some prefix are not re-checked pairwise at a node.
+    Thus, races (with prefixes or type suffixes) are reported for most precise memos with actual accesses:
+    at the longest prefix and longest type suffix.
+
+    Additionally, accesses between prefix and type suffix intersecting at a node are checked.
+    These races are reported at the unique memo at the intersection of the prefix and the type suffix.
+    This requires an implementation hack to still eagerly do outer distribution, but only of empty access sets.
+    It ensures that corresponding trie nodes exist for traversal later. *)
+
+(** Given C declarations:
+    {@c[
+    struct S {
+      int f;
+    };
+
+    struct T {
+      struct S s;
+    };
+
+    struct T t;
+    ]}
+
+    Example structure of related memos for race checking:
+    {v
+     (int)   (S)     (T)
+        \   /   \   /   \
+          f       s       t
+            \   /   \   /
+              f       s
+                \   /
+                  f
+    v}
+    where:
+    - [(int)] is a type-based memo root for the primitive [int] type;
+    - [(S)] and [(T)] are short for [(struct S)] and [(struct T)], which are type-based memo roots;
+    - prefix relations are indicated by [/], so access paths run diagonally from top-right to bottom-left;
+    - type suffix relations are indicated by [\ ].
+
+    All same-node races:
+    - Race between [t.s.f] and [t.s.f] is checked/reported at [t.s.f].
+    - Race between [t.s] and [t.s] is checked/reported at [t.s].
+    - Race between [t] and [t] is checked/reported at [t].
+    - Race between [(T).s.f] and [(T).s.f] is checked/reported at [(T).s.f].
+    - Race between [(T).s] and [(T).s] is checked/reported at [(T).s].
+    - Race between [(T)] and [(T)] is checked/reported at [(T)].
+    - Race between [(S).f] and [(S).f] is checked/reported at [(S).f].
+    - Race between [(S)] and [(S)] is checked/reported at [(S)].
+    - Race between [(int)] and [(int)] is checked/reported at [(int)].
+
+    All prefix races:
+    - Race between [t.s.f] and [t.s] is checked/reported at [t.s.f].
+    - Race between [t.s.f] and [t] is checked/reported at [t.s.f].
+    - Race between [t.s] and [t] is checked/reported at [t.s].
+    - Race between [(T).s.f] and [(T).s] is checked/reported at [(T).s.f].
+    - Race between [(T).s.f] and [(T)] is checked/reported at [(T).s.f].
+    - Race between [(T).s] and [(T)] is checked/reported at [(T).s].
+    - Race between [(S).f] and [(S)] is checked/reported at [(S).f].
+
+    All type suffix races:
+    - Race between [t.s.f] and [(T).s.f] is checked/reported at [t.s.f].
+    - Race between [t.s.f] and [(S).f] is checked/reported at [t.s.f].
+    - Race between [t.s.f] and [(int)] is checked/reported at [t.s.f].
+    - Race between [(T).s.f] and [(S).f] is checked/reported at [(T).s.f].
+    - Race between [(T).s.f] and [(int)] is checked/reported at [(T).s.f].
+    - Race between [(S).f] and [(int)] is checked/reported at [(S).f].
+    - Race between [t.s] and [(T).s] is checked/reported at [t.s].
+    - Race between [t.s] and [(S)] is checked/reported at [t.s].
+    - Race between [(T).s] and [(S)] is checked/reported at [(T).s].
+    - Race between [t] and [(T)] is checked/reported at [t].
+
+    All type suffix prefix races:
+    - Race between [t.s.f] and [(T).s] is checked/reported at [t.s.f].
+    - Race between [t.s.f] and [(T)] is checked/reported at [t.s.f].
+    - Race between [t.s.f] and [(S)] is checked/reported at [t.s.f].
+    - Race between [(T).s.f] and [(S)] is checked/reported at [(T).s.f].
+    - Race between [t.s] and [(T)] is checked/reported at [t.s].
+
+    All prefix-type suffix races:
+    - Race between [t.s] and [(T).s.f] is checked/reported at [t.s.f].
+    - Race between [t.s] and [(S).f] is checked/reported at [t.s.f].
+    - Race between [t.s] and [(int)] is checked/reported at [t.s.f].
+    - Race between [t] and [(T).s.f] is checked/reported at [t.s.f].
+    - Race between [t] and [(S).f] is checked/reported at [t.s.f].
+    - Race between [t] and [(int)] is checked/reported at [t.s.f].
+    - Race between [t] and [(T).s] is checked/reported at [t.s].
+    - Race between [t] and [(S)] is checked/reported at [t.s].
+    - Race between [(T).s] and [(S).f] is checked/reported at [(T).s.f].
+    - Race between [(T).s] and [(int)] is checked/reported at [(T).s.f].
+    - Race between [(T)] and [(S).f] is checked/reported at [(T).s.f].
+    - Race between [(T)] and [(int)] is checked/reported at [(T).s.f].
+    - Race between [(T)] and [(S)] is checked/reported at [(T).s].
+    - Race between [(S)] and [(int)] is checked/reported at [(S).f]. *)
+
 
 (** Data race analyzer without base --- this is the new standard *)
 module Spec =
@@ -12,7 +134,7 @@ struct
   let name () = "race"
 
   (* Two global invariants:
-     1. memoroot -> (offset -> accesses)  --  used for warnings
+     1. memoroot -> (offset --trie--> accesses)  --  used for warnings
      2. varinfo -> set of memo  --  used for IterSysVars Global *)
 
   module V =
@@ -52,13 +174,22 @@ struct
 
   module OffsetTrie =
   struct
-    include TrieDomain.Make (OneOffset) (Access.AS)
+    (* LiftBot such that add_distribute_outer can side-effect empty set to indicate
+       all offsets that exist for prefix-type_suffix race checking.
+       Otherwise, there are no trie nodes to traverse to where this check must happen. *)
+    include TrieDomain.Make (OneOffset) (Lattice.LiftBot (Access.AS))
+
+    let rec find (offset : Offset.Unit.t) ((accs, children) : t) : value =
+      match offset with
+      | `NoOffset -> accs
+      | `Field (f, offset') -> find offset' (ChildMap.find (Field f) children)
+      | `Index ((), offset') -> find offset' (ChildMap.find Index children)
 
     let rec singleton (offset : Offset.Unit.t) (value : value) : t =
       match offset with
       | `NoOffset -> (value, ChildMap.empty ())
-      | `Field (f, offset') -> (Access.AS.empty (), ChildMap.singleton (Field f) (singleton offset' value))
-      | `Index ((), offset') -> (Access.AS.empty (), ChildMap.singleton Index (singleton offset' value))
+      | `Field (f, offset') -> (`Bot, ChildMap.singleton (Field f) (singleton offset' value))
+      | `Index ((), offset') -> (`Bot, ChildMap.singleton Index (singleton offset' value))
   end
 
   module G =
@@ -96,9 +227,42 @@ struct
 
   let side_access ctx (conf, w, loc, e, a) ((memoroot, offset) as memo) =
     if !AnalysisState.should_warn then
-      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (Access.AS.singleton (conf, w, loc, e, a))));
+      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton (conf, w, loc, e, a)))));
+    side_vars ctx memo
+
+  (** Side-effect empty access set for prefix-type_suffix race checking. *)
+  let side_access_empty ctx ((memoroot, offset) as memo) =
+    if !AnalysisState.should_warn then
+      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.empty ()))));
     side_vars ctx memo
 
+  (** Get immediate type_suffix memo. *)
+  let type_suffix_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option =
+    (* No need to make ana.race.direct-arithmetic return None here,
+       because (int) is empty anyway since Access.add_distribute_outer isn't called. *)
+    match root, offset with
+    | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* global.foo.bar -> (struct S).foo.bar *) (* TODO: Alloc variables void type *)
+    | _, `NoOffset -> None (* primitive type *)
+    | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') (* (struct S).foo.bar -> (struct T).bar *)
+    | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') (* (int[])[*] -> int *)
+    | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *)
+
+  let rec find_type_suffix' ctx ((root, offset) as memo : Access.Memo.t) : Access.AS.t =
+    let trie = G.access (ctx.global (V.access root)) in
+    let accs =
+      match OffsetTrie.find offset trie with
+      | `Lifted accs -> accs
+      | `Bot -> Access.AS.empty ()
+    in
+    let type_suffix = find_type_suffix ctx memo in
+    Access.AS.union accs type_suffix
+
+  (** Find accesses from all type_suffixes transitively. *)
+  and find_type_suffix ctx (memo : Access.Memo.t) : Access.AS.t =
+    match type_suffix_memo memo with
+    | Some type_suffix_memo -> find_type_suffix' ctx type_suffix_memo
+    | None -> Access.AS.empty ()
+
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
     | WarnGlobal g ->
@@ -108,18 +272,27 @@ struct
           (* ignore (Pretty.printf "WarnGlobal %a\n" Access.MemoRoot.pretty g'); *)
           let trie = G.access (ctx.global g) in
           (** Distribute access to contained fields. *)
-          let rec distribute_inner offset (accs, children) ancestor_accs =
-            let ancestor_accs' = Access.AS.union ancestor_accs accs in
-            OffsetTrie.ChildMap.iter (fun child_key child_trie ->
-                distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ancestor_accs'
-              ) children;
-            if not (Access.AS.is_empty accs) then (
+          let rec distribute_inner offset (accs, children) ~prefix ~type_suffix_prefix =
+            let accs =
+              match accs with
+              | `Lifted accs -> accs
+              | `Bot -> Access.AS.empty ()
+            in
+            let type_suffix = find_type_suffix ctx (g', offset) in
+            if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty prefix) && not (Access.AS.is_empty type_suffix)) then (
               let memo = (g', offset) in
               let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in
-              Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs memo) accs
-            )
+              Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe {node=accs; prefix; type_suffix; type_suffix_prefix}) memo
+            );
+
+            (* Recurse to children. *)
+            let prefix' = Access.AS.union prefix accs in
+            let type_suffix_prefix' = Access.AS.union type_suffix_prefix type_suffix in
+            OffsetTrie.ChildMap.iter (fun child_key child_trie ->
+                distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ~prefix:prefix' ~type_suffix_prefix:type_suffix_prefix'
+              ) children;
           in
-          distribute_inner `NoOffset trie (Access.AS.empty ())
+          distribute_inner `NoOffset trie ~prefix:(Access.AS.empty ()) ~type_suffix_prefix:(Access.AS.empty ())
         | `Right _ -> (* vars *)
           ()
       end
@@ -142,11 +315,11 @@ struct
       let loc = Option.get !Node.current_node in
       let add_access conf voffs =
         let a = part_access (Option.map fst voffs) in
-        Access.add (side_access octx (conf, kind, loc, e, a)) e voffs;
+        Access.add ~side:(side_access octx (conf, kind, loc, e, a)) ~side_empty:(side_access_empty octx) e voffs;
       in
       let add_access_struct conf ci =
         let a = part_access None in
-        Access.add_one (side_access octx (conf, kind, loc, e, a)) (`Type (TComp (ci, [])), `NoOffset)
+        Access.add_one ~side:(side_access octx (conf, kind, loc, e, a)) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset)
       in
       let has_escaped g = octx.ask (Queries.MayEscape g) in
       (* The following function adds accesses to the lval-set ls