From 44e1c8257015d897e1b2a70d687a30d8ffb9066b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Apr 2023 10:38:33 +0300 Subject: [PATCH 1/5] Add option lib.activated --- src/analyses/libraryFunctions.ml | 39 ++++++++++++++++------------ src/analyses/libraryFunctions.mli | 2 ++ src/util/options.schema.json | 42 +++++++++++++++++++++++++++++++ src/util/server.ml | 1 + 4 files changed, 68 insertions(+), 16 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index dd3015e33d..8fbb950d31 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -427,22 +427,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_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 +1156,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 diff --git a/src/analyses/libraryFunctions.mli b/src/analyses/libraryFunctions.mli index 6a641652bc..cd024b6c94 100644 --- a/src/analyses/libraryFunctions.mli +++ b/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 diff --git a/src/util/options.schema.json b/src/util/options.schema.json index e3673e82c8..ffa4be6717 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1225,6 +1225,48 @@ }, "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", + "linux-kernel", + "goblint", + "sv-comp", + "ncurses", + "zstd" + ] + } + }, + "additionalProperties": false + }, "sem": { "title": "Semantics", "description": "Options for semantics", diff --git a/src/util/server.ml b/src/util/server.ml index b95e4e368e..578fe401ed 100644 --- a/src/util/server.ml +++ b/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); From 1812a7316b5717705e10cd98da1785ce5d72f0c0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Apr 2023 10:44:42 +0300 Subject: [PATCH 2/5] Deactivate zstd library by default --- conf/zstd-race.json | 11 +++++++++++ src/util/options.schema.json | 3 +-- tests/regression/03-practical/25-zstd-customMem.c | 1 + tests/regression/06-symbeq/31-zstd-thread-pool.c | 2 +- .../regression/06-symbeq/35-zstd-thread-pool-multi.c | 2 +- tests/regression/06-symbeq/36-zstd-thread-pool-add.c | 2 +- 6 files changed, 16 insertions(+), 5 deletions(-) diff --git a/conf/zstd-race.json b/conf/zstd-race.json index 72ec5de5b3..d1a8848c06 100644 --- a/conf/zstd-race.json +++ b/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, diff --git a/src/util/options.schema.json b/src/util/options.schema.json index ffa4be6717..313aada83e 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1260,8 +1260,7 @@ "linux-kernel", "goblint", "sv-comp", - "ncurses", - "zstd" + "ncurses" ] } }, diff --git a/tests/regression/03-practical/25-zstd-customMem.c b/tests/regression/03-practical/25-zstd-customMem.c index be7b65429e..dd1db7fb5e 100644 --- a/tests/regression/03-practical/25-zstd-customMem.c +++ b/tests/regression/03-practical/25-zstd-customMem.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] zstd // Extracted from zstd #include #include diff --git a/tests/regression/06-symbeq/31-zstd-thread-pool.c b/tests/regression/06-symbeq/31-zstd-thread-pool.c index 561f4d6c70..60b29b3627 100644 --- a/tests/regression/06-symbeq/31-zstd-thread-pool.c +++ b/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. diff --git a/tests/regression/06-symbeq/35-zstd-thread-pool-multi.c b/tests/regression/06-symbeq/35-zstd-thread-pool-multi.c index 1ef6cf869a..8b404d5e6a 100644 --- a/tests/regression/06-symbeq/35-zstd-thread-pool-multi.c +++ b/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. diff --git a/tests/regression/06-symbeq/36-zstd-thread-pool-add.c b/tests/regression/06-symbeq/36-zstd-thread-pool-add.c index 8544975a29..1b335ee062 100644 --- a/tests/regression/06-symbeq/36-zstd-thread-pool-add.c +++ b/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. From e74b3da9198c785b25e95deb2dc37c8ec3525518 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Apr 2023 10:54:46 +0300 Subject: [PATCH 3/5] Deactivate sv-comp library by default --- src/analyses/libraryFunctions.ml | 1 - src/maingoblint.ml | 5 ++++- src/util/options.schema.json | 1 - 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 8fbb950d31..4ee0ce5111 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -396,7 +396,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); diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 265b7c09e5..4c359186e9 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -157,6 +157,9 @@ 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"; + match get_string "dbg.dump" with | "" -> () | path -> @@ -358,7 +361,7 @@ let preprocess_files () = extra_files := find_custom_include (Fpath.v "stdlib.c") :: find_custom_include (Fpath.v "pthread.c") :: !extra_files; - if get_bool "ana.sv-comp.functions" then + 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 diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 313aada83e..3c40c30db7 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1259,7 +1259,6 @@ "linux-userspace", "linux-kernel", "goblint", - "sv-comp", "ncurses" ] } From 818a06ca14f2a2d563d735433200721d274b01bf Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Apr 2023 10:56:37 +0300 Subject: [PATCH 4/5] Deactivate linux-kernel library by default --- src/analyses/libraryFunctions.ml | 5 ++--- src/maingoblint.ml | 3 +++ src/util/options.schema.json | 1 - 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 4ee0ce5111..c7310d3ff6 100644 --- a/src/analyses/libraryFunctions.ml +++ b/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); @@ -433,7 +432,7 @@ let libraries = Hashtbl.of_list [ ("gcc", gcc_descs_list); ("glibc", glibc_desc_list); ("linux-userspace", linux_userspace_descs_list); - ("linux-kernel", linux_descs_list); + ("linux-kernel", linux_kernel_descs_list); ("goblint", goblint_descs_list); ("sv-comp", svcomp_descs_list); ("ncurses", ncurses_descs_list); diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 4c359186e9..894fa598db 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -160,6 +160,9 @@ let handle_flags () = 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 -> diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 3c40c30db7..235111ef3c 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1257,7 +1257,6 @@ "gcc", "glibc", "linux-userspace", - "linux-kernel", "goblint", "ncurses" ] From 9c17fdc7dd720aa7deebee263b79d5522967220a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 3 Apr 2023 11:00:29 +0300 Subject: [PATCH 5/5] Use stdlib.c and pthread.c stubs only when library activated --- src/maingoblint.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 894fa598db..d2989270f8 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -362,7 +362,11 @@ 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 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;