From a36572925450fc31fe95f448a75118f004af537a Mon Sep 17 00:00:00 2001 From: karoliineh Date: Thu, 14 Sep 2023 12:23:21 +0300 Subject: [PATCH 1/3] Add zlib and liblzma functions used in the silver searcher --- src/analyses/libraryFunctions.ml | 18 ++++++++++++++++++ src/util/options.schema.json | 4 +++- 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index e8fabe7dc1..2eb68dd437 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -102,6 +102,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("vprintf", unknown [drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("vfprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("vsprintf", unknown [drop "buffer" [w]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) + ("vasprintf", unknown [drop "strp" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) + ("vsprintf", unknown [drop "str" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("mktime", unknown [drop "tm" [r;w]]); ("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]); ("clearerr", unknown [drop "stream" [w]]); @@ -288,6 +290,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 *) ("fnmatch", unknown [drop "pattern" [r]; drop "string" [r]; drop "flags" []]); + ("realpath", unknown [drop "path" [r]; drop "resolved_path" [w]]); ] (** Pthread functions. *) @@ -824,6 +827,19 @@ let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pcre_version", unknown []); ] +let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ + ("inflate", unknown [drop "strm" [r_deep]; drop "flush" []]); + ("inflateInit2", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []]); + ("inflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []; drop "version" [r]; drop "stream_size" []]); + ("inflateEnd", unknown [drop "strm" [f_deep]]); + ] + +let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ + ("lzma_code", unknown [drop "strm" [r_deep; w_deep]; drop "action" []]); + ("lzma_auto_decoder", unknown [drop "strm" [r_deep; w_deep]; drop "memlimit" []; drop "flags" []]); + ("lzma_end", unknown [drop "strm" [r_deep; w_deep]]); + ] + let libraries = Hashtbl.of_list [ ("c", c_descs_list @ math_descs_list); ("posix", posix_descs_list); @@ -837,6 +853,8 @@ let libraries = Hashtbl.of_list [ ("ncurses", ncurses_descs_list); ("zstd", zstd_descs_list); ("pcre", pcre_descs_list); + ("zlib", zlib_descs_list); + ("liblzma", liblzma_descs_list); ] let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t = diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 1ef73378fb..1b9c7d3fd5 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1285,7 +1285,9 @@ "sv-comp", "ncurses", "zstd", - "pcre" + "pcre", + "zlib", + "liblzma" ] }, "default": [ From 444428467d44a3d188d034c4418d34117543b838 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 18 Sep 2023 11:36:23 +0300 Subject: [PATCH 2/3] Remove duplicate vsprintf and add vsnprintf --- src/analyses/libraryFunctions.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 2eb68dd437..912867d319 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -103,7 +103,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("vfprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("vsprintf", unknown [drop "buffer" [w]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("vasprintf", unknown [drop "strp" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) - ("vsprintf", unknown [drop "str" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) + ("vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("mktime", unknown [drop "tm" [r;w]]); ("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]); ("clearerr", unknown [drop "stream" [w]]); @@ -1089,7 +1089,6 @@ let invalidate_actions = [ "usleep", readsAll; "svc_run", writesAll;(*unsafe*) "dup", readsAll; (*safe*) - "vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) "strcasecmp", readsAll; (*safe*) From 684cfa8c3f45afcefd95a1096e954fad27af8d91 Mon Sep 17 00:00:00 2001 From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com> Date: Mon, 18 Sep 2023 11:37:22 +0300 Subject: [PATCH 3/3] Apply suggestions from code review Co-authored-by: Simmo Saan --- src/analyses/libraryFunctions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 912867d319..b883c7e354 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -828,7 +828,7 @@ let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ] let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ - ("inflate", unknown [drop "strm" [r_deep]; drop "flush" []]); + ("inflate", unknown [drop "strm" [r_deep; w_deep]; drop "flush" []]); ("inflateInit2", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []]); ("inflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []; drop "version" [r]; drop "stream_size" []]); ("inflateEnd", unknown [drop "strm" [f_deep]]); @@ -837,7 +837,7 @@ let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("lzma_code", unknown [drop "strm" [r_deep; w_deep]; drop "action" []]); ("lzma_auto_decoder", unknown [drop "strm" [r_deep; w_deep]; drop "memlimit" []; drop "flags" []]); - ("lzma_end", unknown [drop "strm" [r_deep; w_deep]]); + ("lzma_end", unknown [drop "strm" [r_deep; w_deep; f_deep]]); ] let libraries = Hashtbl.of_list [