Skip to content

Commit

Permalink
Merge pull request #1212 from goblint/libfuns-concrat
Browse files Browse the repository at this point in the history 
Add missing library functions for large Concrat benchmarks
  • Loading branch information
@sim642
sim642 authored Oct 26, 2023
2 parents 03131eb + a457854 commit 5a35656
Showing 1 changed file with 47 additions and 3 deletions.
50 changes: 47 additions & 3 deletions src/analyses/libraryFunctions.ml
View file
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.[
("ftruncate", unknown [drop "fd" []; drop "length" []]);
("mkfifo", unknown [drop "pathname" [r]; drop "mode" []]);
("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 @@ -384,7 +394,15 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("unlink", unknown [drop "pathname" [r]]);
("popen", unknown [drop "command" [r]; drop "type" [r]]);
("stat", unknown [drop "pathname" [r]; drop "statbuf" [w]]);
("statfs", unknown [drop "path" [r]; drop "buf" [w]]);
("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);
("srandom", unknown [drop "seed" []]);
("random", special [] Rand);
("posix_memalign", unknown [drop "memptr" [w]; drop "alignment" []; drop "size" []]); (* TODO: Malloc *)
]

(** Pthread functions. *)
Expand All @@ -393,6 +411,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 All @@ -414,6 +433,10 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("pthread_mutex_unlock", special [__ "mutex" []] @@ fun mutex -> Unlock mutex);
("__pthread_mutex_unlock", special [__ "mutex" []] @@ fun mutex -> Unlock mutex);
("pthread_mutexattr_init", unknown [drop "attr" [w]]);
("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_rwlock_init", unknown [drop "rwlock" [w]; drop "attr" [r]]);
("pthread_rwlock_destroy", unknown [drop "rwlock" [f]]);
Expand Down Expand Up @@ -444,6 +467,8 @@ 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" []]);
Expand Down Expand Up @@ -516,6 +541,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 @@ -524,6 +555,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 @@ -534,7 +566,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 @@ -579,6 +612,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 @@ -595,6 +629,8 @@ 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" []]);
Expand All @@ -604,6 +640,10 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("mount", unknown [drop "source" [r]; drop "target" [r]; drop "filesystemtype" [r]; drop "mountflags" []; drop "data" [r]]);
("umount", unknown [drop "target" [r]]);
("umount2", unknown [drop "target" [r]; drop "flags" []]);
("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 @@ -990,6 +1030,11 @@ let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("deflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "level" []; drop "method" []; drop "windowBits" []; drop "memLevel" []; drop "strategy" []; drop "version" [r]; drop "stream_size" []]);
("deflateEnd", unknown [drop "strm" [f_deep]]);
("zlibVersion", unknown []);
("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 @@ -1187,7 +1232,6 @@ let invalidate_actions = [
"ioctl", writesAll;(*unsafe*)
"fstat__extinline", writesAll;(*unsafe*)
"scandir", writes [1;3;4];(*keep [1;3;4]*)
"sigwait", writesAllButFirst 1 readsAll;(*drop 1*)
"bindtextdomain", readsAll;(*safe*)
"textdomain", readsAll;(*safe*)
"dcgettext", readsAll;(*safe*)
Expand Down

0 comments on commit 5a35656

Please sign in to comment.