diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index f84fe1d4e3..117dcbd236 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -32,6 +32,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_strncat", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; }); ("__builtin___strncat_chk", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; }); ("memcmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); + ("__builtin_memcmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); ("memchr", unknown [drop "s" [r]; drop "c" []; drop "n" []]); ("asctime", unknown ~attrs:[ThreadUnsafe] [drop "time_ptr" [r_deep]]); ("fclose", unknown [drop "stream" [r_deep; w_deep; f_deep]]); @@ -62,6 +63,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("localeconv", unknown ~attrs:[ThreadUnsafe] []); ("localtime", unknown ~attrs:[ThreadUnsafe] [drop "time" [r]]); ("strlen", special [__ "s" [r]] @@ fun s -> Strlen s); + ("__builtin_strlen", special [__ "s" [r]] @@ fun s -> Strlen s); ("strstr", special [__ "haystack" [r]; __ "needle" [r]] @@ fun haystack needle -> Strstr { haystack; needle; }); ("strcmp", special [__ "s1" [r]; __ "s2" [r]] @@ fun s1 s2 -> Strcmp { s1; s2; n = None; }); ("strtok", unknown ~attrs:[ThreadUnsafe] [drop "str" [r; w]; drop "delim" [r]]); @@ -146,6 +148,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("atomic_flag_test_and_set_explicit", unknown [drop "obj" [r; w]; drop "order" []]); ("atomic_load", unknown [drop "obj" [r]]); ("atomic_store", unknown [drop "obj" [w]; drop "desired" []]); + ("_Exit", special [drop "status" []] @@ Abort); ] (** C POSIX library functions. @@ -335,7 +338,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("regexec", unknown [drop "preg" [r_deep]; drop "string" [r]; drop "nmatch" []; drop "pmatch" [w_deep]; drop "eflags" []]); ("regfree", unknown [drop "preg" [f_deep]]); ("ffs", unknown [drop "i" []]); - ("_exit", special [drop "status" []] Abort); + ("_exit", special [drop "status" []] @@ Abort); ("execvp", unknown [drop "file" [r]; drop "argv" [r_deep]]); ("execl", unknown (drop "path" [r] :: drop "arg" [r] :: VarArgs (drop' [r]))); ("statvfs", unknown [drop "path" [r]; drop "buf" [w]]); @@ -505,6 +508,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_unreachable", special' [] @@ fun () -> if get_bool "sem.builtin_unreachable.dead_code" then Abort else Unknown); (* https://github.com/sosy-lab/sv-benchmarks/issues/1296 *) ("__assert_rtn", special [drop "func" [r]; drop "file" [r]; drop "line" []; drop "exp" [r]] @@ Abort); (* MacOS's built-in assert *) ("__assert_fail", special [drop "assertion" [r]; drop "file" [r]; drop "line" []; drop "function" [r]] @@ Abort); (* gcc's built-in assert *) + ("__assert", special [drop "assertion" [r]; drop "file" [r]; drop "line" []] @@ Abort); (* header says: The following is not at all used here but needed for standard compliance. *) ("__builtin_return_address", unknown [drop "level" []]); ("__builtin___sprintf_chk", unknown (drop "s" [w] :: drop "flag" [] :: drop "os" [] :: drop "fmt" [r] :: VarArgs (drop' [r]))); ("__builtin_add_overflow", unknown [drop "a" []; drop "b" []; drop "c" [w]]); @@ -576,6 +580,10 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__fgets_chk", unknown [drop "__s" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); ("__fread_alias", unknown [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); ("__fread_chk", unknown [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("fread_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "buffer" [w]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); + ("__fread_unlocked_alias", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("__fread_unlocked_chk", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("__fread_unlocked_chk_warn", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); ("__read_chk", unknown [drop "__fd" []; drop "__buf" [w]; drop "__nbytes" []; drop "__buflen" []]); ("__read_alias", unknown [drop "__fd" []; drop "__buf" [w]; drop "__nbytes" []]); ("__readlink_chk", unknown [drop "path" [r]; drop "buf" [w]; drop "len" []; drop "buflen" []]); @@ -972,6 +980,7 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__VERIFIER_atomic_end", special [] @@ Unlock verifier_atomic); ("__VERIFIER_nondet_loff_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *) ("__VERIFIER_nondet_int", unknown []); (* declare invalidate actions to prevent invalidating globals when extern in regression tests *) + ("__VERIFIER_nondet_size_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *) ] let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index fc015f458b..90fcb6c24d 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -14,9 +14,10 @@ struct let name () = "memLeak" module D = ToppedVarInfoSet - module C = Lattice.Unit + module C = D + module P = IdentityP (D) - let context _ _ = () + let context _ d = d (* HELPER FUNCTIONS *) let get_global_vars () = @@ -117,4 +118,4 @@ struct end let _ = - MCP.register_analysis (module Spec : MCPSpec) \ No newline at end of file + MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/autoTune.ml b/src/autoTune.ml index 06347f3190..7ddc1aee43 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -227,8 +227,8 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) = | ValidMemcleanup -> (* Enable the memLeak analysis *) let memLeakAna = ["memLeak"] in if (get_int "ana.malloc.unique_address_count") < 1 then ( - print_endline "Setting \"ana.malloc.unique_address_count\" to 1"; - set_int "ana.malloc.unique_address_count" 1; + print_endline "Setting \"ana.malloc.unique_address_count\" to 5"; + set_int "ana.malloc.unique_address_count" 5; ); print_endline @@ "Specification: ValidMemtrack and ValidMemcleanup -> enabling memLeak analysis \"" ^ (String.concat ", " memLeakAna) ^ "\""; enableAnalyses memLeakAna diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 40669ff729..4e282b19a4 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -352,7 +352,7 @@ "description": "List of path-sensitive analyses", "type": "array", "items": { "type": "string" }, - "default": [ "mutex", "malloc_null", "uninit", "expsplit","activeSetjmp" ] + "default": [ "mutex", "malloc_null", "uninit", "expsplit","activeSetjmp","memLeak" ] }, "ctx_insens": { "title": "ana.ctx_insens", diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml index 068aed7a22..373a66d3d6 100644 --- a/src/witness/myARG.ml +++ b/src/witness/myARG.ml @@ -141,7 +141,7 @@ struct let equal_node_context _ _ = failwith "StackNode: equal_node_context" end -module Stack (Cfg:CfgForward) (Arg: S): +module Stack (Arg: S with module Edge = InlineEdge): S with module Node = StackNode (Arg.Node) and module Edge = Arg.Edge = struct module Node = StackNode (Arg.Node) @@ -156,45 +156,30 @@ struct | n :: stack -> let cfgnode = Arg.Node.cfgnode n in match cfgnode with - | Function _ -> (* TODO: can this be done without Cfg? *) + | Function _ -> (* TODO: can this be done without cfgnode? *) begin match stack with (* | [] -> failwith "StackArg.next: return stack empty" *) | [] -> [] (* main return *) | call_n :: call_stack -> - let call_cfgnode = Arg.Node.cfgnode call_n in let call_next = - Cfg.next call_cfgnode + Arg.next call_n (* filter because infinite loops starting with function call will have another Neg(1) edge from the head *) - |> List.filter (fun (locedges, to_node) -> - List.exists (function - | (_, Proc _) -> true - | (_, _) -> false - ) locedges + |> List.filter_map (fun (edge, to_n) -> + match edge with + | InlinedEdge _ -> Some to_n + | _ -> None ) in - begin match call_next with - | [] -> failwith "StackArg.next: call next empty" - | [(_, return_node)] -> - begin match Arg.Node.move_opt call_n return_node with - (* TODO: Is it possible to have a calling node without a returning node? *) - (* | None -> [] *) - | None -> failwith "StackArg.next: no return node" - | Some return_n -> - (* TODO: Instead of next & filter, construct unique return_n directly. Currently edge missing. *) - Arg.next n - |> List.filter (fun (edge, to_n) -> - (* let to_cfgnode = Arg.Node.cfgnode to_n in - MyCFG.Node.equal to_cfgnode return_node *) - Arg.Node.equal_node_context to_n return_n - ) - |> List.map (fun (edge, to_n) -> - let to_n' = to_n :: call_stack in - (edge, to_n') - ) - end - | _ :: _ :: _ -> failwith "StackArg.next: call next ambiguous" - end + Arg.next n + |> List.filter_map (fun (edge, to_n) -> + if BatList.mem_cmp Arg.Node.compare to_n call_next then ( + let to_n' = to_n :: call_stack in + Some (edge, to_n') + ) + else + None + ) end | _ -> let+ (edge, to_n) = Arg.next n in diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index eae97b1199..89487ea8d4 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -76,9 +76,9 @@ sig val is_sink: Arg.Node.t -> bool end -module StackTaskResult (Cfg:MyCFG.CfgForward) (TaskResult: TaskResult) = +module StackTaskResult (TaskResult: TaskResult with module Arg.Edge = MyARG.InlineEdge) = struct - module Arg = MyARG.Stack (Cfg) (TaskResult.Arg) + module Arg = MyARG.Stack (TaskResult.Arg) let result = TaskResult.result diff --git a/src/witness/witness.ml b/src/witness/witness.ml index d94960d542..235461c348 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -14,7 +14,7 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult) let module TaskResult = (val if get_bool "witness.graphml.stack" then - (module StackTaskResult (Task.Cfg) (TaskResult) : WitnessTaskResult) + (module StackTaskResult (TaskResult) : WitnessTaskResult) else (module TaskResult) ) diff --git a/tests/regression/56-witness/52-witness-lifter-ps2.c b/tests/regression/56-witness/52-witness-lifter-ps2.c new file mode 100644 index 0000000000..bcb7c1410c --- /dev/null +++ b/tests/regression/56-witness/52-witness-lifter-ps2.c @@ -0,0 +1,35 @@ +// PARAM: --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --enable witness.graphml.enabled --set ana.specification 'CHECK( init(main()), LTL(G valid-memtrack) )' --set ana.activated[+] memLeak --set ana.path_sens[+] memLeak --set ana.malloc.unique_address_count 1 +struct _twoIntsStruct { + int intOne ; + int intTwo ; +}; + +typedef struct _twoIntsStruct twoIntsStruct; + +void printStructLine(twoIntsStruct const *structTwoIntsStruct) +{ + return; +} + + +int main(int argc, char **argv) +{ + twoIntsStruct *data; + int tmp_1; + + + if (tmp_1 != 0) { + twoIntsStruct *dataBuffer = malloc(800UL); + data = dataBuffer; + } + else { + + twoIntsStruct *dataBuffer_0 = malloc(800UL); + data = dataBuffer_0; + } + + printStructLine((twoIntsStruct const *)data); + free((void *)data); + + return; +} diff --git a/tests/regression/56-witness/53-witness-lifter-ps3.c b/tests/regression/56-witness/53-witness-lifter-ps3.c new file mode 100644 index 0000000000..06b73b3888 --- /dev/null +++ b/tests/regression/56-witness/53-witness-lifter-ps3.c @@ -0,0 +1,39 @@ +// PARAM: --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --enable witness.graphml.enabled --set ana.specification 'CHECK( init(main()), LTL(G valid-memtrack) )' --set ana.activated[+] memLeak --set ana.path_sens[+] memLeak --set ana.malloc.unique_address_count 1 +struct _twoIntsStruct { + int intOne ; + int intTwo ; +}; + +typedef struct _twoIntsStruct twoIntsStruct; + +void printStructLine(twoIntsStruct const *structTwoIntsStruct) +{ + return; +} + +twoIntsStruct *foo() { + twoIntsStruct *data; + int tmp_1; + + if (tmp_1 != 0) { + twoIntsStruct *dataBuffer = malloc(800UL); + data = dataBuffer; + } + else { + + twoIntsStruct *dataBuffer_0 = malloc(800UL); + data = dataBuffer_0; + } + return data; +} + +int main(int argc, char **argv) +{ + twoIntsStruct *data; + data = foo(); + + printStructLine((twoIntsStruct const *)data); + free((void *)data); + + return; +}