Merge pull request #1028 from goblint/libfuns-activated

Add option `lib.activated`

Author: sim642

conf/zstd-race.json

@@ -31,6 +31,17 @@
       "lines": true
     }
   },
+  "lib": {
+    "activated": [
+      "c",
+      "posix",
+      "pthread",
+      "gcc",
+      "glibc",
+      "linux-userspace",
+      "zstd"
+    ]
+  },
   "sem": {
     "unknown_function": {
       "spawn": false,

src/analyses/libraryFunctions.ml

@@ -258,8 +258,7 @@ let big_kernel_lock = AddrOf (Cil.var (Goblintutil.create_var (makeGlobalVar "[b
 let console_sem = AddrOf (Cil.var (Goblintutil.create_var (makeGlobalVar "[console semaphore]" intType)))
 
 (** Linux kernel functions. *)
-(* TODO: conditional on kernel option *)
-let linux_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("spin_lock_irqsave", special [__ "lock" []; drop "flags" []] @@ fun lock -> Lock { lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true });
     ("spin_unlock_irqrestore", special [__ "lock" []; drop "flags" []] @@ fun lock -> Unlock lock);
     ("_raw_spin_unlock_irqrestore", special [__ "lock" []; drop "flags" []] @@ fun lock -> Unlock lock);
@@ -396,7 +395,6 @@ let verifier_atomic = AddrOf (Cil.var (Goblintutil.create_var verifier_atomic_va
 
 (** SV-COMP functions.
     Just the ones that require special handling and cannot be stubbed. *)
-(* TODO: conditional on ana.sv-comp.functions option *)
 let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__VERIFIER_atomic_begin", special [] @@ Lock { lock = verifier_atomic; try_ = false; write = true; return_on_success = true });
     ("__VERIFIER_atomic_end", special [] @@ Unlock verifier_atomic);
@@ -427,22 +425,29 @@ let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("wbkgd", unknown [drop "win" [r_deep; w_deep]; drop "ch" []]);
   ]
 
-(* TODO: allow selecting which lists to use *)
-let library_descs = Hashtbl.of_list (List.concat [
-    c_descs_list;
-    posix_descs_list;
-    pthread_descs_list;
-    gcc_descs_list;
-    glibc_desc_list;
-    linux_userspace_descs_list;
-    linux_descs_list;
-    goblint_descs_list;
-    zstd_descs_list;
-    math_descs_list;
-    svcomp_descs_list;
-    ncurses_descs_list;
-  ])
+let libraries = Hashtbl.of_list [
+  ("c", c_descs_list @ math_descs_list);
+  ("posix", posix_descs_list);
+  ("pthread", pthread_descs_list);
+  ("gcc", gcc_descs_list);
+  ("glibc", glibc_desc_list);
+  ("linux-userspace", linux_userspace_descs_list);
+  ("linux-kernel", linux_kernel_descs_list);
+  ("goblint", goblint_descs_list);
+  ("sv-comp", svcomp_descs_list);
+  ("ncurses", ncurses_descs_list);
+  ("zstd", zstd_descs_list);
+]
 
+let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t =
+  ResettableLazy.from_fun (fun () ->
+      let activated = List.unique (GobConfig.get_string_list "lib.activated") in
+      let desc_list = List.concat_map (Hashtbl.find libraries) activated in
+      Hashtbl.of_list desc_list
+    )
+
+let reset_lazy () =
+  ResettableLazy.reset activated_library_descs
 
 type categories = [
   | `Malloc       of exp
@@ -1149,7 +1154,7 @@ let unknown_desc ~f name = (* TODO: remove name argument, unknown function shoul
 
 let find f =
   let name = f.vname in
-  match Hashtbl.find_option library_descs name with
+  match Hashtbl.find_option (ResettableLazy.force activated_library_descs) name with
   | Some desc -> desc
   | None ->
     match get_invalidate_action name with

src/analyses/libraryFunctions.mli

@@ -17,3 +17,5 @@ val is_special: Cil.varinfo -> bool
 
 
 val verifier_atomic_var: Cil.varinfo
+
+val reset_lazy: unit -> unit

src/maingoblint.ml

@@ -157,6 +157,12 @@ let handle_flags () =
   if get_bool "dbg.debug" then
     set_bool "warn.debug" true;
 
+  if get_bool "ana.sv-comp.functions" then
+    set_auto "lib.activated[+]" "sv-comp";
+
+  if get_bool "kernel" then
+    set_auto "lib.activated[+]" "linux-kernel";
+
   match get_string "dbg.dump" with
   | "" -> ()
   | path ->
@@ -356,9 +362,13 @@ let preprocess_files () =
 
   let extra_files = ref [] in
 
-  extra_files := find_custom_include (Fpath.v "stdlib.c") :: find_custom_include (Fpath.v "pthread.c") :: !extra_files;
+  if List.mem "c" (get_string_list "lib.activated") then
+    extra_files := find_custom_include (Fpath.v "stdlib.c") :: !extra_files;
 
-  if get_bool "ana.sv-comp.functions" then
+  if List.mem "pthread" (get_string_list "lib.activated") then
+    extra_files := find_custom_include (Fpath.v "pthread.c") :: !extra_files;
+
+  if List.mem "sv-comp" (get_string_list "lib.activated") then
     extra_files := find_custom_include (Fpath.v "sv-comp.c") :: !extra_files;
 
   let preprocessed = List.concat_map preprocess_arg_file (!extra_files @ List.map Fpath.v (get_string_list "files")) in

src/util/options.schema.json

@@ -1225,6 +1225,45 @@
       },
       "additionalProperties": false
     },
+    "lib": {
+      "title": "Library functions",
+      "description": "Options for library functions",
+      "type": "object",
+      "properties": {
+        "activated": {
+          "title": "lib.activated",
+          "description": "List of activated libraries.",
+          "type": "array",
+          "items": {
+            "type": "string",
+            "enum": [
+              "c",
+              "posix",
+              "pthread",
+              "gcc",
+              "glibc",
+              "linux-userspace",
+              "linux-kernel",
+              "goblint",
+              "sv-comp",
+              "ncurses",
+              "zstd"
+            ]
+          },
+          "default": [
+            "c",
+            "posix",
+            "pthread",
+            "gcc",
+            "glibc",
+            "linux-userspace",
+            "goblint",
+            "ncurses"
+          ]
+        }
+      },
+      "additionalProperties": false
+    },
     "sem": {
       "title": "Semantics",
       "description": "Options for semantics",

src/util/server.ml

@@ -278,6 +278,7 @@ let analyze ?(reset=false) (s: t) =
   PrecisionUtil.reset_lazy ();
   ApronDomain.reset_lazy ();
   AutoTune.reset_lazy ();
+  LibraryFunctions.reset_lazy ();
   Access.reset ();
   s.file <- Some file;
   GobConfig.set_bool "incremental.load" (not fresh);

tests/regression/03-practical/25-zstd-customMem.c

@@ -1,3 +1,4 @@
+// PARAM: --set lib.activated[+] zstd
 // Extracted from zstd
 #include <stddef.h>
 #include <stdlib.h>

tests/regression/06-symbeq/31-zstd-thread-pool.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] symb_locks
+// PARAM: --set ana.activated[+] symb_locks --set lib.activated[+] zstd
 /* SPDX-License-Identifier: BSD-3-Clause */
 /*
  * Copyright (c) Facebook, Inc.

tests/regression/06-symbeq/35-zstd-thread-pool-multi.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] symb_locks --set ana.activated[+] mallocFresh
+// PARAM: --set ana.activated[+] symb_locks --set ana.activated[+] mallocFresh --set lib.activated[+] zstd
 /* SPDX-License-Identifier: BSD-3-Clause */
 /*
  * Copyright (c) Facebook, Inc.

tests/regression/06-symbeq/36-zstd-thread-pool-add.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] symb_locks --set ana.activated[+] var_eq --set exp.extraspecials[+] ZSTD_customMalloc --set exp.extraspecials[+] ZSTD_customCalloc
+// PARAM: --set ana.activated[+] symb_locks --set ana.activated[+] var_eq --set lib.activated[+] zstd --set exp.extraspecials[+] ZSTD_customMalloc --set exp.extraspecials[+] ZSTD_customCalloc
 /* SPDX-License-Identifier: BSD-3-Clause */
 /*
  * Copyright (c) Facebook, Inc.