Merge pull request #1603 from goblint/unknown-function-spawn

Fix `sem.unknown_function.spawn` handling in base

src/analyses/base.ml

@@ -2172,11 +2172,7 @@ struct
         in
         List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
       end
-    | _, _ when get_bool "sem.unknown_function.spawn" ->
-      (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
-         But here we consider all non-ThreadCreate functions also unknown, so old-style LibraryFunctions access
-         definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions).
-         Need this to not have memmove spawn in SV-COMP. *)
+    | _, _ ->
       let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in
       let deep_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = true } args in
       let shallow_flist = collect_invalidate ~deep:false ~ctx ctx.local shallow_args in
@@ -2185,7 +2181,6 @@ struct
       let addrs = List.concat_map AD.to_var_may flist in
       if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
       List.filter_map (create_thread ~multiple:true None None) addrs
-    | _, _ -> []
 
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)

src/config/options.schema.json

@@ -1544,6 +1544,19 @@
             }
           },
           "additionalProperties": false
+        },
+        "atexit": {
+          "title": "sem.atexit",
+          "type": "object",
+          "properties": {
+            "ignore": {
+              "title": "sem.atexit.ignore",
+              "description": "Ignore atexit callbacks (unsound).",
+              "type": "boolean",
+              "default": false
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false

src/util/library/libraryDsl.ml

@@ -30,8 +30,20 @@ struct
     | [] -> fail "^::"
 end
 
+type access =
+  | Access of LibraryDesc.Access.t
+  | If of (unit -> bool) * access
+
+let rec eval_access = function
+  | Access acc -> Some acc
+  | If (p, access) ->
+    if p () then
+      eval_access access
+    else
+      None
+
 type ('k, 'l, 'r) arg_desc = {
-  accesses: Access.t list;
+  accesses: access list;
   match_arg: (Cil.exp, 'k, 'r) Pattern.t;
   match_var_args: (Cil.exp list, 'l, 'r) Pattern.t;
 }
@@ -51,15 +63,21 @@ let rec accs: type k r. (k, r) args_desc -> Accesses.t = fun args_desc args ->
   match args_desc, args with
   | [], [] -> []
   | VarArgs arg_desc, args ->
-    List.map (fun acc ->
-        (acc, args)
+    List.filter_map (fun access ->
+        match eval_access access with
+        | Some acc -> Some (acc, args)
+        | None -> None
       ) arg_desc.accesses
   | arg_desc :: args_desc, arg :: args ->
     let accs'' = accs args_desc args in
-    List.fold_left (fun (accs'': (Access.t * Cil.exp list) list) (acc: Access.t) ->
-        match List.assoc_opt acc accs'' with
-        | Some args -> (acc, arg :: args) :: List.remove_assoc acc accs''
-        | None -> (acc, [arg]) :: accs''
+    List.fold_left (fun (accs'': (Access.t * Cil.exp list) list) (access: access) ->
+        match eval_access access with
+        | Some acc ->
+          begin match List.assoc_opt acc accs'' with
+            | Some args -> (acc, arg :: args) :: List.remove_assoc acc accs''
+            | None -> (acc, [arg]) :: accs''
+          end
+        | None -> accs''
       ) accs'' arg_desc.accesses
   | _, _ -> invalid_arg "accs"
 
@@ -94,13 +112,15 @@ let drop (_name: string) accesses = { empty_drop_desc with accesses; }
 let drop' accesses = { empty_drop_desc with accesses; }
 
 
-let r = Access.{ kind = Read; deep = false; }
-let r_deep = Access.{ kind = Read; deep = true; }
-let w = Access.{ kind = Write; deep = false; }
-let w_deep = Access.{ kind = Write; deep = true; }
-let f = Access.{ kind = Free; deep = false; }
-let f_deep = Access.{ kind = Free; deep = true; }
-let s = Access.{ kind = Spawn; deep = false; }
-let s_deep = Access.{ kind = Spawn; deep = true; }
-let c = Access.{ kind = Spawn; deep = false; } (* TODO: Sound, but very imprecise hack for calls to function pointers given as arguments. *)
-let c_deep = Access.{ kind = Spawn; deep = true; }
+let r = Access { kind = Read; deep = false; }
+let r_deep = Access { kind = Read; deep = true; }
+let w = Access { kind = Write; deep = false; }
+let w_deep = Access { kind = Write; deep = true; }
+let f = Access { kind = Free; deep = false; }
+let f_deep = Access { kind = Free; deep = true; }
+let s = Access { kind = Spawn; deep = false; }
+let s_deep = Access { kind = Spawn; deep = true; }
+let c = Access { kind = Spawn; deep = false; } (* TODO: Sound, but very imprecise hack for calls to function pointers given as arguments. *)
+let c_deep = Access { kind = Spawn; deep = true; }
+
+let if_ p access = If (p, access)

src/util/library/libraryDsl.mli

@@ -28,52 +28,57 @@ val special': ?attrs:LibraryDesc.attr list -> (LibraryDesc.special, LibraryDesc.
 (** Create unknown library function descriptor from arguments descriptor, which must {!drop} all arguments. *)
 val unknown: ?attrs:LibraryDesc.attr list -> (LibraryDesc.special, LibraryDesc.special) args_desc -> LibraryDesc.t
 
+(** Argument access descriptor. *)
+type access
 
 (** Argument descriptor, which captures the named argument with accesses for continuation function of {!special}. *)
-val __: string -> LibraryDesc.Access.t list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
+val __: string -> access list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
 
 (** Argument descriptor, which captures an unnamed argument with accesses for continuation function of {!special}. *)
-val __': LibraryDesc.Access.t list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
+val __': access list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc
 
 (** Argument descriptor, which drops (does not capture) the named argument with accesses. *)
-val drop: string -> LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_desc
+val drop: string -> access list -> ('r, 'r, 'r) arg_desc
 
 (** Argument descriptor, which drops (does not capture) an unnamed argument with accesses. *)
-val drop': LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_desc
+val drop': access list -> ('r, 'r, 'r) arg_desc
 
 
 (** Shallow {!AccessKind.Read} access.
     All immediate arguments of function calls are always read, this specifies the reading of pointed-to values. *)
-val r: LibraryDesc.Access.t
+val r: access
 
 (** Deep {!AccessKind.Read} access.
     All immediate arguments of function calls are always read, this specifies the reading of pointed-to values.
     Rarely needed. *)
-val r_deep: LibraryDesc.Access.t
+val r_deep: access
 
 (** Shallow {!AccessKind.Write} access. *)
-val w: LibraryDesc.Access.t
+val w: access
 
 (** Deep {!AccessKind.Write} access.
     Rarely needed. *)
-val w_deep: LibraryDesc.Access.t
+val w_deep: access
 
 (** Shallow {!AccessKind.Free} access. *)
-val f: LibraryDesc.Access.t
+val f: access
 
 (** Deep {!AccessKind.Free} access.
     Rarely needed. *)
-val f_deep: LibraryDesc.Access.t
+val f_deep: access
 
 (** Shallow {!AccessKind.Spawn} access. *)
-val s: LibraryDesc.Access.t
+val s: access
 
 (** Deep {!AccessKind.Spawn} access.
     Rarely needed. *)
-val s_deep: LibraryDesc.Access.t
+val s_deep: access
 
 (** Shallow {!AccessKind.Spawn} access, substituting function pointer calls for now (TODO). *)
-val c: LibraryDesc.Access.t
+val c: access
 
 (** Deep {!AccessKind.Spawn} access, substituting deep function pointer calls for now (TODO)  *)
-val c_deep: LibraryDesc.Access.t
+val c_deep: access
+
+(** Conditional access, e.g. on an option. *)
+val if_: (unit -> bool) -> access -> access

src/util/library/libraryFunctions.ml

@@ -145,7 +145,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
-    ("atexit", unknown [drop "function" [s]]);
+    ("atexit", unknown [drop "function" [if_ (fun () -> not (get_bool "sem.atexit.ignore")) s]]);
     ("atoi", unknown [drop "nptr" [r]]);
     ("atol", unknown [drop "nptr" [r]]);
     ("atoll", unknown [drop "nptr" [r]]);

tests/regression/41-stdlib/08-atexit-no-spawn.c

@@ -1,4 +1,4 @@
-// PARAM: --disable sem.unknown_function.spawn
+// PARAM: --enable sem.atexit.ignore
 #include <stdlib.h>
 #include <goblint.h>