Skip to content

Commit 631888e

Browse files
sim642sim642
authored
Merge pull request #1174 from goblint/libfuns-concrat
Add and fix library functions for Concrat benchmarks
2 parents eb97eca + 4bc0303 commit 631888e

File tree

5 files changed

+214
-82
lines changed

5 files changed

+214
-82
lines changed

‎src/analyses/libraryDesc.ml

+2-23
Original file line numberDiff line numberDiff line change
@@ -126,31 +126,10 @@ type t = {
126126
attrs: attr list; (** Attributes of function. *)
127127
}
128128

129-
let special_of_old classify_name = fun args ->
130-
match classify_name args with
131-
| `Malloc e -> Malloc e
132-
| `Calloc (count, size) -> Calloc { count; size; }
133-
| `Realloc (ptr, size) -> Realloc { ptr; size; }
134-
| `Lock (try_, write, return_on_success) ->
135-
begin match args with
136-
| [lock] -> Lock { lock ; try_; write; return_on_success; }
137-
| [] -> failwith "lock has no arguments"
138-
| _ -> failwith "lock has multiple arguments"
139-
end
140-
| `Unlock ->
141-
begin match args with
142-
| [arg] -> Unlock arg
143-
| [] -> failwith "unlock has no arguments"
144-
| _ -> failwith "unlock has multiple arguments"
145-
end
146-
| `ThreadCreate (thread, start_routine, arg) -> ThreadCreate { thread; start_routine; arg; }
147-
| `ThreadJoin (thread, ret_var) -> ThreadJoin { thread; ret_var; }
148-
| `Unknown _ -> Unknown
149-
150-
let of_old ?(attrs: attr list=[]) (old_accesses: Accesses.old) (classify_name): t = {
129+
let of_old ?(attrs: attr list=[]) (old_accesses: Accesses.old): t = {
151130
attrs;
152131
accs = Accesses.of_old old_accesses;
153-
special = special_of_old classify_name;
132+
special = fun _ -> Unknown;
154133
}
155134

156135
module MathPrintable = struct

‎src/analyses/libraryFunctions.ml

+67-59
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,10 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
1212
("memset", special [__ "dest" [w]; __ "ch" []; __ "count" []] @@ fun dest ch count -> Memset { dest; ch; count; });
1313
("__builtin_memset", special [__ "dest" [w]; __ "ch" []; __ "count" []] @@ fun dest ch count -> Memset { dest; ch; count; });
1414
("__builtin___memset_chk", special [__ "dest" [w]; __ "ch" []; __ "count" []; drop "os" []] @@ fun dest ch count -> Memset { dest; ch; count; });
15-
("memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src });
15+
("memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); (* TODO: use n *)
1616
("__builtin_memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src });
1717
("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src });
18+
("memccpy", special [__ "dest" [w]; __ "src" [r]; drop "c" []; drop "n" []] @@ fun dest src -> Memcpy {dest; src}); (* C23 *) (* TODO: use n and c *)
1819
("memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src });
1920
("__builtin_memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src });
2021
("__builtin___memmove_chk", special [__ "dest" [w]; __ "src" [r]; drop "count" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src });
@@ -64,6 +65,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
6465
("__builtin_strcmp", special [__ "s1" [r]; __ "s2" [r]] @@ fun s1 s2 -> Strcmp { s1; s2; n = None; });
6566
("strncmp", special [__ "s1" [r]; __ "s2" [r]; __ "n" []] @@ fun s1 s2 n -> Strcmp { s1; s2; n = Some n; });
6667
("malloc", special [__ "size" []] @@ fun size -> Malloc size);
68+
("calloc", special [__ "n" []; __ "size" []] @@ fun n size -> Calloc {count = n; size});
6769
("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size });
6870
("free", special [__ "ptr" [f]] @@ fun ptr -> Free ptr);
6971
("abort", special [] Abort);
@@ -117,12 +119,14 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
117119
("wcrtomb", unknown ~attrs:[ThreadUnsafe] [drop "s" [w]; drop "wc" []; drop "ps" [r_deep; w_deep]]);
118120
("wcstombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r]; drop "size" []]);
119121
("wcsrtombs", unknown ~attrs:[ThreadUnsafe] [drop "dst" [w]; drop "src" [r_deep; w]; drop "size" []; drop "ps" [r_deep; w_deep]]);
122+
("mbstowcs", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []]);
120123
("abs", unknown [drop "j" []]);
121124
("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
122125
("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
123126
("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
124127
("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
125128
("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
129+
("atexit", unknown [drop "function" [s]]);
126130
]
127131

128132
(** C POSIX library functions.
@@ -246,6 +250,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
246250
("timer_gettime", unknown [drop "timerid" []; drop "curr_value" [w_deep]]);
247251
("timer_getoverrun", unknown [drop "timerid" []]);
248252
("lstat", unknown [drop "pathname" [r]; drop "statbuf" [w]]);
253+
("fstat", unknown [drop "fd" []; drop "buf" [w]]);
254+
("fstatat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "buf" [w]; drop "flags" []]);
249255
("getpwnam", unknown [drop "name" [r]]);
250256
("chdir", unknown [drop "path" [r]]);
251257
("closedir", unknown [drop "dirp" [r]]);
@@ -292,12 +298,32 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
292298
("getaddrinfo", unknown [drop "node" [r]; drop "service" [r]; drop "hints" [r_deep]; drop "res" [w]]); (* only write res non-deep because it doesn't write to existing fields of res *)
293299
("fnmatch", unknown [drop "pattern" [r]; drop "string" [r]; drop "flags" []]);
294300
("realpath", unknown [drop "path" [r]; drop "resolved_path" [w]]);
301+
("dprintf", unknown (drop "fd" [] :: drop "format" [r] :: VarArgs (drop' [r])));
302+
("vdprintf", unknown [drop "fd" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
303+
("mkdtemp", unknown [drop "template" [r; w]]);
304+
("mkstemp", unknown [drop "template" [r; w]]);
305+
("regcomp", unknown [drop "preg" [w_deep]; drop "regex" [r]; drop "cflags" []]);
306+
("regexec", unknown [drop "preg" [r_deep]; drop "string" [r]; drop "nmatch" []; drop "pmatch" [w_deep]; drop "eflags" []]);
307+
("regfree", unknown [drop "preg" [f_deep]]);
308+
("ffs", unknown [drop "i" []]);
309+
("_exit", special [drop "status" []] Abort);
310+
("execvp", unknown [drop "file" [r]; drop "argv" [r_deep]]);
311+
("statvfs", unknown [drop "path" [r]; drop "buf" [w]]);
312+
("readlink", unknown [drop "path" [r]; drop "buf" [w]; drop "bufsz" []]);
313+
("wcswidth", unknown [drop "s" [r]; drop "n" []]);
314+
("link", unknown [drop "oldpath" [r]; drop "newpath" [r]]);
315+
("renameat", unknown [drop "olddirfd" []; drop "oldpath" [r]; drop "newdirfd" []; drop "newpath" [r]]);
316+
("posix_fadvise", unknown [drop "fd" []; drop "offset" []; drop "len" []; drop "advice" []]);
317+
("getppid", unknown []);
318+
("lockf", unknown [drop "fd" []; drop "cmd" []; drop "len" []]);
295319
]
296320

297321
(** Pthread functions. *)
298322
let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
299323
("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *)
300324
("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *)
325+
("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
326+
("pthread_kill", unknown [drop "thread" []; drop "sig" []]);
301327
("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
302328
("__pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
303329
("pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond);
@@ -322,16 +348,16 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
322348
("pthread_mutexattr_destroy", unknown [drop "attr" [f]]);
323349
("pthread_rwlock_init", unknown [drop "rwlock" [w]; drop "attr" [r]]);
324350
("pthread_rwlock_destroy", unknown [drop "rwlock" [f]]);
325-
("pthread_rwlock_rdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true});
326-
("pthread_rwlock_tryrdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true});
327-
("pthread_rwlock_wrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true});
351+
("pthread_rwlock_rdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = false});
352+
("pthread_rwlock_tryrdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = true; write = false; return_on_success = false});
353+
("pthread_rwlock_wrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false});
328354
("pthread_rwlock_trywrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = true; write = true; return_on_success = false});
329355
("pthread_rwlock_unlock", special [__ "rwlock" []] @@ fun rwlock -> Unlock rwlock);
330356
("pthread_rwlockattr_init", unknown [drop "attr" [w]]);
331357
("pthread_rwlockattr_destroy", unknown [drop "attr" [f]]);
332358
("pthread_spin_init", unknown [drop "lock" [w]; drop "pshared" []]);
333359
("pthread_spin_destroy", unknown [drop "lock" [f]]);
334-
("pthread_spin_lock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true});
360+
("pthread_spin_lock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false});
335361
("pthread_spin_trylock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = true; write = true; return_on_success = false});
336362
("pthread_spin_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock);
337363
("pthread_attr_init", unknown [drop "attr" [w]]);
@@ -412,6 +438,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
412438
("__sync_fetch_and_add", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
413439
("__sync_fetch_and_sub", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
414440
("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]);
441+
("__builtin_alloca", special [__ "size" []] @@ fun size -> Malloc size);
415442
]
416443

417444
let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -454,6 +481,11 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
454481
("fopencookie", unknown [drop "cookie" []; drop "mode" [r]; drop "io_funcs" [s_deep]]); (* doesn't access cookie but passes it to io_funcs *)
455482
("mempcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src });
456483
("__builtin___mempcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src });
484+
("rawmemchr", unknown [drop "s" [r]; drop "c" []]);
485+
("memrchr", unknown [drop "s" [r]; drop "c" []; drop "n" []]);
486+
("memmem", unknown [drop "haystack" [r]; drop "haystacklen" []; drop "needle" [r]; drop "needlelen" [r]]);
487+
("getifaddrs", unknown [drop "ifap" [w]]);
488+
("freeifaddrs", unknown [drop "ifa" [f_deep]]);
457489
]
458490

459491
let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -470,6 +502,12 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
470502
("__xpg_basename", unknown [drop "path" [r]]);
471503
("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 *)
472504
("madvise", unknown [drop "addr" []; drop "length" []; drop "advice" []]);
505+
("inotify_init1", unknown [drop "flags" []]);
506+
("inotify_add_watch", unknown [drop "fd" []; drop "pathname" [r]; drop "mask" []]);
507+
("inotify_rm_watch", unknown [drop "fd" []; drop "wd" []]);
508+
("fts_open", unknown [drop "path_argv" [r_deep]; drop "options" []; drop "compar" [s]]); (* TODO: use Call instead of Spawn *)
509+
("fts_read", unknown [drop "ftsp" [r_deep; w_deep]]);
510+
("fts_close", unknown [drop "ftsp" [f_deep]]);
473511
]
474512

475513
let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType)))
@@ -530,6 +568,10 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
530568
("__cmpxchg_wrong_size", special [] Abort);
531569
("__xadd_wrong_size", special [] Abort);
532570
("__put_user_bad", special [] Abort);
571+
("kmalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Malloc size);
572+
("__kmalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Malloc size);
573+
("kzalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Calloc {count = Cil.one; size});
574+
("usb_alloc_urb", special [__ "iso_packets" []; drop "mem_flags" []] @@ fun iso_packets -> Malloc MyCFG.unknown_exp);
533575
]
534576

535577
(** Goblint functions. *)
@@ -801,10 +843,14 @@ let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
801843
("wattrset", unknown [drop "win" [r_deep; w_deep]; drop "attrs" []]);
802844
("endwin", unknown []);
803845
("wgetch", unknown [drop "win" [r_deep; w_deep]]);
846+
("wget_wch", unknown [drop "win" [r_deep; w_deep]; drop "wch" [w]]);
847+
("unget_wch", unknown [drop "wch" []]);
804848
("wmove", unknown [drop "win" [r_deep; w_deep]; drop "y" []; drop "x" []]);
805849
("waddch", unknown [drop "win" [r_deep; w_deep]; drop "ch" []]);
850+
("waddnstr", unknown [drop "win" [r_deep; w_deep]; drop "str" [r]; drop "n" []]);
806851
("waddnwstr", unknown [drop "win" [r_deep; w_deep]; drop "wstr" [r]; drop "n" []]);
807852
("wattr_on", unknown [drop "win" [r_deep; w_deep]; drop "attrs" []; drop "opts" []]); (* opts argument currently not used *)
853+
("wattr_off", unknown [drop "win" [r_deep; w_deep]; drop "attrs" []; drop "opts" []]); (* opts argument currently not used *)
808854
("wrefresh", unknown [drop "win" [r_deep; w_deep]]);
809855
("mvprintw", unknown (drop "win" [r_deep; w_deep] :: drop "y" [] :: drop "x" [] :: drop "fmt" [r] :: VarArgs (drop' [r])));
810856
("initscr", unknown []);
@@ -813,10 +859,19 @@ let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
813859
("start_color", unknown []);
814860
("use_default_colors", unknown []);
815861
("wclear", unknown [drop "win" [r_deep; w_deep]]);
862+
("wclrtoeol", unknown [drop "win" [r_deep; w_deep]]);
816863
("can_change_color", unknown []);
817864
("init_color", unknown [drop "color" []; drop "red" []; drop "green" []; drop "blue" []]);
818865
("init_pair", unknown [drop "pair" []; drop "f" [r]; drop "b" [r]]);
819866
("wbkgd", unknown [drop "win" [r_deep; w_deep]; drop "ch" []]);
867+
("keyname", unknown [drop "c" []]);
868+
("newterm", unknown [drop "type" [r]; drop "outfd" [r_deep; w_deep]; drop "infd" [r_deep; w_deep]]);
869+
("cbreak", unknown []);
870+
("nonl", unknown []);
871+
("keypad", unknown [drop "win" [r_deep; w_deep]; drop "bf" []]);
872+
("set_escdelay", unknown [drop "size" []]);
873+
("printw", unknown (drop "fmt" [r] :: VarArgs (drop' [r])));
874+
("werase", unknown [drop "win" [r_deep; w_deep]]);
820875
]
821876

822877
let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -868,46 +923,6 @@ let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t
868923
let reset_lazy () =
869924
ResettableLazy.reset activated_library_descs
870925

871-
type categories = [
872-
| `Malloc of exp
873-
| `Calloc of exp * exp
874-
| `Realloc of exp * exp
875-
| `Lock of bool * bool * bool (* try? * write? * return on success *)
876-
| `Unlock
877-
| `ThreadCreate of exp * exp * exp (* id * f * x *)
878-
| `ThreadJoin of exp * exp (* id * ret_var *)
879-
| `Unknown of string ]
880-
881-
882-
let classify fn exps: categories =
883-
let strange_arguments () =
884-
M.warn ~category:Program "%s arguments are strange!" fn;
885-
`Unknown fn
886-
in
887-
match fn with
888-
| "pthread_join" ->
889-
begin match exps with
890-
| [id; ret_var] -> `ThreadJoin (id, ret_var)
891-
| _ -> strange_arguments ()
892-
end
893-
| "kmalloc" | "__kmalloc" | "usb_alloc_urb" | "__builtin_alloca" ->
894-
begin match exps with
895-
| size::_ -> `Malloc size
896-
| _ -> strange_arguments ()
897-
end
898-
| "kzalloc" ->
899-
begin match exps with
900-
| size::_ -> `Calloc (Cil.one, size)
901-
| _ -> strange_arguments ()
902-
end
903-
| "calloc" ->
904-
begin match exps with
905-
| n::size::_ -> `Calloc (n, size)
906-
| _ -> strange_arguments ()
907-
end
908-
| x -> `Unknown x
909-
910-
911926
module Invalidate =
912927
struct
913928
[@@@warning "-unused-value-declaration"] (* some functions are not used below *)
@@ -1036,7 +1051,6 @@ let invalidate_actions = [
10361051
"sigaddset", writesAll;(*unsafe*)
10371052
"raise", writesAll;(*unsafe*)
10381053
"_strlen", readsAll;(*safe*)
1039-
"__builtin_alloca", readsAll;(*safe*)
10401054
"dlopen", readsAll;(*safe*)
10411055
"dlsym", readsAll;(*safe*)
10421056
"dlclose", readsAll;(*safe*)
@@ -1197,7 +1211,7 @@ let is_safe_uncalled fn_name =
11971211
List.exists (fun r -> Str.string_match r fn_name 0) kernel_safe_uncalled_regex
11981212

11991213

1200-
let unknown_desc ~f name = (* TODO: remove name argument, unknown function shouldn't have classify *)
1214+
let unknown_desc f =
12011215
let old_accesses (kind: AccessKind.t) args = match kind with
12021216
| Write when GobConfig.get_bool "sem.unknown_function.invalidate.args" -> args
12031217
| Write -> []
@@ -1215,16 +1229,10 @@ let unknown_desc ~f name = (* TODO: remove name argument, unknown function shoul
12151229
else
12161230
[]
12171231
in
1218-
let classify_name args =
1219-
match classify name args with
1220-
| `Unknown _ as category ->
1221-
(* TODO: remove hack when all classify are migrated *)
1222-
if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then
1223-
M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname;
1224-
category
1225-
| category -> category
1226-
in
1227-
LibraryDesc.of_old ~attrs old_accesses classify_name
1232+
(* TODO: remove hack when all classify are migrated *)
1233+
if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then
1234+
M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname;
1235+
LibraryDesc.of_old ~attrs old_accesses
12281236

12291237
let find f =
12301238
let name = f.vname in
@@ -1233,9 +1241,9 @@ let find f =
12331241
| None ->
12341242
match get_invalidate_action name with
12351243
| Some old_accesses ->
1236-
LibraryDesc.of_old old_accesses (classify name)
1244+
LibraryDesc.of_old old_accesses
12371245
| None ->
1238-
unknown_desc ~f name
1246+
unknown_desc f
12391247

12401248

12411249
let is_special fv =

0 commit comments

Comments
 (0)