Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add missing library functions for large Concrat benchmarks #1212

Merged
merged 12 commits into from
Oct 26, 2023
Merged

Add missing library functions for large Concrat benchmarks #1212

Changes from 10 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
56cf37e
Add missing library functions for concrat/dnspod-sr
sim642 Oct 9, 2023
a13e2b9
Add mremap library function for concrat/kona
sim642 Oct 9, 2023
5307813
Add missing library functions for concrat/lmdb
sim642 Oct 9, 2023
25ef4ce
Add missing library functions for concrat/minimap2
sim642 Oct 9, 2023
9f614eb
Add missing library functions for concrat/phpspy
sim642 Oct 9, 2023
c222508
Add alphasort library function for concrat/ProcDump-for-Linux
sim642 Oct 9, 2023
969d315
Add missing library functions for concrat/Remotery
sim642 Oct 9, 2023
0122821
Add missing library functions for concrat/siege
sim642 Oct 9, 2023
c630a39
Add warn library function for concrat/the_silver_searcher
sim642 Oct 9, 2023
0af8ba7
Add zError library function for concrat/the_silver_searcher
sim642 Oct 9, 2023
85ce4b2
Add some missing library functions for concrat/sysbench
sim642 Oct 10, 2023
a457854
Merge branch 'master' into libfuns-concrat
sim642 Oct 10, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 44 additions & 3 deletions src/analyses/libraryFunctions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("getc", unknown [drop "stream" [r_deep; w_deep]]);
("fgets", unknown [drop "str" [w]; drop "count" []; drop "stream" [r_deep; w_deep]]);
("fopen", unknown [drop "pathname" [r]; drop "mode" [r]]);
("freopen", unknown [drop "pathname" [r]; drop "mode" [r]; drop "stream" [r_deep; w_deep]]);
("printf", unknown (drop "format" [r] :: VarArgs (drop' [r])));
("fprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "format" [r] :: VarArgs (drop' [r])));
("sprintf", unknown (drop "buffer" [w] :: drop "format" [r] :: VarArgs (drop' [r])));
Expand Down Expand Up @@ -110,6 +111,7 @@ 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? *)
("asprintf", unknown (drop "strp" [w] :: drop "format" [r] :: VarArgs (drop' [r_deep]))); (* TODO: glibc section? *)
("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? *)
("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]]);
Expand Down Expand Up @@ -246,6 +248,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("mkfifo", unknown [drop "pathname" [r]; drop "mode" []]);
("ntohs", unknown [drop "netshort" []]);
("alarm", unknown [drop "seconds" []]);
("pread", unknown [drop "fd" []; drop "buf" [w]; drop "count" []; drop "offset" []]);
("pwrite", unknown [drop "fd" []; drop "buf" [r]; drop "count" []; drop "offset" []]);
("hstrerror", unknown [drop "err" []]);
("inet_ntoa", unknown ~attrs:[ThreadUnsafe] [drop "in" []]);
Expand All @@ -265,6 +268,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("access", unknown [drop "pathname" [r]; drop "mode" []]);
("ttyname", unknown ~attrs:[ThreadUnsafe] [drop "fd" []]);
("shm_open", unknown [drop "name" [r]; drop "oflag" []; drop "mode" []]);
("shmget", unknown [drop "key" []; drop "size" []; drop "shmflag" []]);
("shmat", unknown [drop "shmid" []; drop "shmaddr" []; drop "shmflag" []]) (* TODO: shmaddr? *);
("shmdt", unknown [drop "shmaddr" []]) (* TODO: shmaddr? *);
("sched_get_priority_max", unknown [drop "policy" []]);
("mprotect", unknown [drop "addr" []; drop "len" []; drop "prot" []]);
("ftime", unknown [drop "tp" [w]]);
Expand Down Expand Up @@ -334,6 +340,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("execl", unknown (drop "path" [r] :: drop "arg" [r] :: VarArgs (drop' [r])));
("statvfs", unknown [drop "path" [r]; drop "buf" [w]]);
("readlink", unknown [drop "path" [r]; drop "buf" [w]; drop "bufsz" []]);
("wcwidth", unknown [drop "c" []]);
("wcswidth", unknown [drop "s" [r]; drop "n" []]);
("link", unknown [drop "oldpath" [r]; drop "newpath" [r]]);
("renameat", unknown [drop "olddirfd" []; drop "oldpath" [r]; drop "newdirfd" []; drop "newpath" [r]]);
Expand Down Expand Up @@ -364,6 +371,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("sigdelset", unknown [drop "set" [r; w]; drop "signum" []]);
("sigismember", unknown [drop "set" [r]; drop "signum" []]);
("sigprocmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]);
("sigwait", unknown [drop "set" [r]; drop "sig" [w]]);
("sigwaitinfo", unknown [drop "set" [r]; drop "info" [w]]);
("sigtimedwait", unknown [drop "set" [r]; drop "info" [w]; drop "timeout" [r]]);
("fork", unknown []);
("dlopen", unknown [drop "filename" [r]; drop "flag" []]);
("dlerror", unknown ~attrs:[ThreadUnsafe] []);
Expand All @@ -373,6 +383,12 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("uname", unknown [drop "buf" [w_deep]]);
("strcasecmp", unknown [drop "s1" [r]; drop "s2" [r]]);
("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]);
("fsync", unknown [drop "fd" []]);
("fdatasync", unknown [drop "fd" []]);
("getrusage", unknown [drop "who" []; drop "usage" [w]]);
("alphasort", unknown [drop "a" [r]; drop "b" [r]]);
("gmtime_r", unknown [drop "timer" [r]; drop "result" [w]]);
("rand_r", special [drop "seedp" [r; w]] Rand);
]

(** Pthread functions. *)
Expand All @@ -381,6 +397,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *)
("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
("pthread_kill", unknown [drop "thread" []; drop "sig" []]);
("pthread_equal", unknown [drop "t1" []; drop "t2" []]);
("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
("__pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
("pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond);
Expand Down Expand Up @@ -432,11 +449,17 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("pthread_key_create", unknown [drop "key" [w]; drop "destructor" [s]]);
("pthread_key_delete", unknown [drop "key" [f]]);
("pthread_cancel", unknown [drop "thread" []]);
("pthread_testcancel", unknown []);
("pthread_setcancelstate", unknown [drop "state" []; drop "oldstate" [w]]);
("pthread_setcanceltype", unknown [drop "type" []; drop "oldtype" [w]]);
("pthread_detach", unknown [drop "thread" []]);
("pthread_attr_setschedpolicy", unknown [drop "attr" [r; w]; drop "policy" []]);
("pthread_condattr_init", unknown [drop "attr" [w]]);
("pthread_condattr_setclock", unknown [drop "attr" [w]; drop "clock_id" []]);
("pthread_mutexattr_getpshared", unknown [drop "attr" [r]; drop "pshared" [w]]);
("pthread_mutexattr_setpshared", unknown [drop "attr" [w]; drop "pshared" []]);
("pthread_mutexattr_getrobust", unknown [drop "attr" [r]; drop "pshared" [w]]);
("pthread_mutexattr_setrobust", unknown [drop "attr" [w]; drop "pshared" []]);
("pthread_mutexattr_destroy", unknown [drop "attr" [f]]);
("pthread_attr_setschedparam", unknown [drop "attr" [r; w]; drop "param" [r]]);
("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]);
Expand Down Expand Up @@ -503,6 +526,12 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("__atomic_clear", unknown [drop "ptr" [w]; drop "memorder" []]);
("__atomic_compare_exchange_n", unknown [drop "ptr" [r; w]; drop "expected" [r; w]; drop "desired" []; drop "weak" []; drop "success_memorder" []; drop "failure_memorder" []]);
("__atomic_compare_exchange", unknown [drop "ptr" [r; w]; drop "expected" [r; w]; drop "desired" [r]; drop "weak" []; drop "success_memorder" []; drop "failure_memorder" []]);
("__atomic_add_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
("__atomic_sub_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
("__atomic_and_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
("__atomic_xor_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
("__atomic_or_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
("__atomic_nand_fetch", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
("__atomic_fetch_add", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
("__atomic_fetch_sub", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
("__atomic_fetch_and", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
Expand All @@ -511,6 +540,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("__atomic_fetch_nand", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
("__atomic_test_and_set", unknown [drop "ptr" [r; w]; drop "memorder" []]);
("__atomic_thread_fence", unknown [drop "memorder" []]);
("__sync_bool_compare_and_swap", unknown [drop "ptr" [r; w]; drop "oldval" []; drop "newval" []]);
("__sync_fetch_and_add", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
("__sync_fetch_and_sub", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]);
Expand All @@ -521,7 +551,8 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
("fputs_unlocked", unknown [drop "s" [r]; drop "stream" [w]]);
("futimesat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "times" [r]]);
("error", unknown ((drop "status" []):: (drop "errnum" []) :: (drop "format" [r]) :: (VarArgs (drop' [r]))));
("error", unknown ((drop "status" []) :: (drop "errnum" []) :: (drop "format" [r]) :: (VarArgs (drop' [r]))));
("warn", unknown (drop "format" [r] :: VarArgs (drop' [r])));
("gettext", unknown [drop "msgid" [r]]);
("euidaccess", unknown [drop "pathname" [r]; drop "mode" []]);
("rpmatch", unknown [drop "response" [r]]);
Expand Down Expand Up @@ -566,6 +597,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
("atoq", unknown [drop "nptr" [r]]);
("strchrnul", unknown [drop "s" [r]; drop "c" []]);
("getdtablesize", unknown []);
("daemon", unknown [drop "nochdir" []; drop "noclose" []]);
]

let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
Expand All @@ -582,12 +614,18 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("__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" []]);
("mremap", unknown (drop "old_address" [] :: drop "old_size" [] :: drop "new_size" [] :: drop "flags" [] :: VarArgs (drop "new_address" [])));
("msync", unknown [drop "addr" []; drop "len" []; drop "flags" []]);
("inotify_init1", unknown [drop "flags" []]);
("inotify_add_watch", unknown [drop "fd" []; drop "pathname" [r]; drop "mask" []]);
("inotify_rm_watch", unknown [drop "fd" []; drop "wd" []]);
("fts_open", unknown [drop "path_argv" [r_deep]; drop "options" []; drop "compar" [s]]); (* TODO: use Call instead of Spawn *)
("fts_read", unknown [drop "ftsp" [r_deep; w_deep]]);
("fts_close", unknown [drop "ftsp" [f_deep]]);
("statfs", unknown [drop "path" [r]; drop "buf" [w]]);
("fstatfs", unknown [drop "fd" []; drop "buf" [w]]);
("cfmakeraw", unknown [drop "termios" [r; w]]);
("process_vm_readv", unknown [drop "pid" []; drop "local_iov" [w_deep]; drop "liovcnt" []; drop "remote_iov" []; drop "riovcnt" []; drop "flags" []]);
]

let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType)))
Expand Down Expand Up @@ -969,6 +1007,11 @@ let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("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]]);
("zError", unknown [drop "err" []]);
("gzopen", unknown [drop "path" [r]; drop "mode" [r]]);
("gzdopen", unknown [drop "fd" []; drop "mode" [r]]);
("gzread", unknown [drop "file" [r_deep; w_deep]; drop "buf" [w]; drop "len" []]);
("gzclose", unknown [drop "file" [f_deep]]);
]

let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
Expand Down Expand Up @@ -1126,7 +1169,6 @@ let invalidate_actions = [
"lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*)
"umount2", readsAll;(*safe*)
"waitpid", readsAll;(*safe*)
"statfs", writes [1;3;4];(*keep [1;3;4]*)
"mount", readsAll;(*safe*)
"__open_alias", readsAll;(*safe*)
"__open_2", readsAll;(*safe*)
Expand All @@ -1135,7 +1177,6 @@ let invalidate_actions = [
"umount", readsAll;(*safe*)
"scandir", writes [1;3;4];(*keep [1;3;4]*)
"unlink", readsAll;(*safe*)
"sigwait", writesAllButFirst 1 readsAll;(*drop 1*)
"bindtextdomain", readsAll;(*safe*)
"textdomain", readsAll;(*safe*)
"dcgettext", readsAll;(*safe*)
Expand Down
Loading