From 80b3b72df749337a3b68435f45b3ff90a2a74dac Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 4 Oct 2023 11:49:49 +0300 Subject: [PATCH 01/66] Add ldv_kzalloc to svcomp malloc wrappers --- conf/svcomp.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/conf/svcomp.json b/conf/svcomp.json index 913d43784b..d6c07387a8 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -52,7 +52,8 @@ "ldv_xmalloc", "ldv_xzalloc", - "ldv_calloc" + "ldv_calloc", + "ldv_kzalloc" ] }, "base": { From 35f6d0000f61e2565e9e9ab86bf2279fd8ebce7a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 4 Oct 2023 11:54:54 +0300 Subject: [PATCH 02/66] Disable free races in svcomp They should be considered MemSafety issues instead. --- conf/svcomp.json | 3 +++ 1 file changed, 3 insertions(+) diff --git a/conf/svcomp.json b/conf/svcomp.json index d6c07387a8..16c4ef338e 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -61,6 +61,9 @@ "domain": "partitioned" } }, + "race": { + "free": false + }, "autotune": { "enabled": true, "activated": [ From b6dfb14231e30c869e9c3a139b6ce7b609960a38 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 4 Oct 2023 11:55:39 +0300 Subject: [PATCH 03/66] Make threadid path sensitive in svcomp This is required for some ldv-races/ no-data-race tasks. --- conf/svcomp.json | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/conf/svcomp.json b/conf/svcomp.json index 16c4ef338e..f51c7a52ee 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -32,6 +32,14 @@ "thread", "threadJoins" ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "threadid" + ], "context": { "widen": false }, From 11164fd7c7d709206c2e6483edd79492450af3c5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 4 Oct 2023 12:15:54 +0300 Subject: [PATCH 04/66] Use exp.architecture for SV-COMP preprocessing Avoids a large number or CIL warnings about mismatching types. --- src/maingoblint.ml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 155faa0e76..ef548fb83a 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -252,6 +252,15 @@ let preprocess_files () = (* Preprocessor flags *) let cppflags = ref (get_string_list "pre.cppflags") in + if get_bool "ana.sv-comp.enabled" then ( + let architecture_flag = match get_string "exp.architecture" with + | "32bit" -> "-m32" + | "64bit" -> "-m64" + | _ -> assert false + in + cppflags := architecture_flag :: !cppflags + ); + (* the base include directory *) (* TODO: any better way? dune executable promotion doesn't add _build sites *) let source_lib_dirs = From 94307d03c47d63621ade9b833c0be35bb23bee89 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 5 Oct 2023 17:27:55 +0300 Subject: [PATCH 05/66] Add option ana.race.call --- conf/svcomp.json | 3 ++- src/domains/access.ml | 2 ++ src/util/options.schema.json | 6 ++++++ 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/conf/svcomp.json b/conf/svcomp.json index f51c7a52ee..df624e4b83 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -70,7 +70,8 @@ } }, "race": { - "free": false + "free": false, + "call": false }, "autotune": { "enabled": true, diff --git a/src/domains/access.ml b/src/domains/access.ml index 8907ccbc32..f243b85bda 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -444,6 +444,8 @@ let may_race A.{kind; acc; _} A.{kind=kind2; acc=acc2; _} = false (* two read/read accesses do not race *) else if not (get_bool "ana.race.free") && (kind = Free || kind2 = Free) then false + else if not (get_bool "ana.race.call") && (kind = Call || kind2 = Call) then + false else if not (MCPAccess.A.may_race acc acc2) then false (* analysis-specific information excludes race *) else diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 1b9c7d3fd5..33de069b38 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1002,6 +1002,12 @@ "type": "boolean", "default": true }, + "call": { + "title": "ana.race.call", + "description": "Report races for thread-unsafe function calls.", + "type": "boolean", + "default": true + }, "direct-arithmetic": { "title": "ana.race.direct-arithmetic", "description": "Collect and distribute direct (i.e. not in a field) accesses to arithmetic types.", From 35f9323854d7e358a63b374c0bad3ced5cc1d4ed Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 1 Nov 2023 12:10:56 +0200 Subject: [PATCH 06/66] Use threadflag path-sensitivity instead of threadid in svcomp conf This is enough for ldv-races/race-2_1-container_of, etc, but cheaper. --- conf/svcomp.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/conf/svcomp.json b/conf/svcomp.json index df624e4b83..d17e1a5f1e 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -38,7 +38,7 @@ "uninit", "expsplit", "activeSetjmp", - "threadid" + "threadflag" ], "context": { "widen": false From f4b37100d7a9edd544518b434aa39950ef1edb88 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 1 Nov 2023 12:22:46 +0200 Subject: [PATCH 07/66] Copy svcomp conf to svcomp24 --- conf/svcomp24.json | 116 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 116 insertions(+) create mode 100644 conf/svcomp24.json diff --git a/conf/svcomp24.json b/conf/svcomp24.json new file mode 100644 index 0000000000..178035eb8a --- /dev/null +++ b/conf/svcomp24.json @@ -0,0 +1,116 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "threadflag" + ], + "context": { + "widen": false + }, + "malloc": { + "wrappers": [ + "kmalloc", + "__kmalloc", + "usb_alloc_urb", + "__builtin_alloca", + "kzalloc", + + "ldv_malloc", + + "kzalloc_node", + "ldv_zalloc", + "kmalloc_array", + "kcalloc", + + "ldv_xmalloc", + "ldv_xzalloc", + "ldv_calloc", + "ldv_kzalloc" + ] + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + } + }, + "pre": { + "enabled": false + } +} From 529a415a03f50dcd69ca4869b5dddf4194535638 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 1 Nov 2023 12:56:11 +0200 Subject: [PATCH 08/66] Add YAML witness generation to svcomp confs --- conf/svcomp.json | 23 +++++++++++++++++++++++ conf/svcomp24.json | 23 +++++++++++++++++++++++ 2 files changed, 46 insertions(+) diff --git a/conf/svcomp.json b/conf/svcomp.json index 178035eb8a..77f519a568 100644 --- a/conf/svcomp.json +++ b/conf/svcomp.json @@ -108,6 +108,29 @@ "enabled": true, "id": "enumerate", "unknown": false + }, + "yaml": { + "enabled": true, + "entry-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true, + "exclude-vars": [ + "tmp\\(___[0-9]+\\)?", + "cond", + "RETURN", + "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?", + ".*____CPAchecker_TMP_[0-9]+", + "__VERIFIER_assert__cond", + "__ksymtab_.*", + "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+" + ] } }, "pre": { diff --git a/conf/svcomp24.json b/conf/svcomp24.json index 178035eb8a..77f519a568 100644 --- a/conf/svcomp24.json +++ b/conf/svcomp24.json @@ -108,6 +108,29 @@ "enabled": true, "id": "enumerate", "unknown": false + }, + "yaml": { + "enabled": true, + "entry-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true, + "exclude-vars": [ + "tmp\\(___[0-9]+\\)?", + "cond", + "RETURN", + "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?", + ".*____CPAchecker_TMP_[0-9]+", + "__VERIFIER_assert__cond", + "__ksymtab_.*", + "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+" + ] } }, "pre": { From ab9eacc13ba44deea33edd146615914cdf2d544e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 1 Nov 2023 12:56:33 +0200 Subject: [PATCH 09/66] Copy svcomp24 conf to svcomp24-validate --- conf/svcomp24-validate.json | 139 ++++++++++++++++++++++++++++++++++++ 1 file changed, 139 insertions(+) create mode 100644 conf/svcomp24-validate.json diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json new file mode 100644 index 0000000000..77f519a568 --- /dev/null +++ b/conf/svcomp24-validate.json @@ -0,0 +1,139 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "threadflag" + ], + "context": { + "widen": false + }, + "malloc": { + "wrappers": [ + "kmalloc", + "__kmalloc", + "usb_alloc_urb", + "__builtin_alloca", + "kzalloc", + + "ldv_malloc", + + "kzalloc_node", + "ldv_zalloc", + "kmalloc_array", + "kcalloc", + + "ldv_xmalloc", + "ldv_xzalloc", + "ldv_calloc", + "ldv_kzalloc" + ] + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "entry-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true, + "exclude-vars": [ + "tmp\\(___[0-9]+\\)?", + "cond", + "RETURN", + "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?", + ".*____CPAchecker_TMP_[0-9]+", + "__VERIFIER_assert__cond", + "__ksymtab_.*", + "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+" + ] + } + }, + "pre": { + "enabled": false + } +} From 95ee32e6ea1bcb0a7075e9cea1f439d45f0d4965 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 1 Nov 2023 13:08:21 +0200 Subject: [PATCH 10/66] Add YAML witness validation to svcomp24-validate conf --- conf/svcomp24-validate.json | 34 +++++++++++++++------------------- 1 file changed, 15 insertions(+), 19 deletions(-) diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json index 77f519a568..3727c3e9f8 100644 --- a/conf/svcomp24-validate.json +++ b/conf/svcomp24-validate.json @@ -12,6 +12,10 @@ "float": { "interval": true }, + "apron": { + "domain": "polyhedra", + "strengthening": true + }, "activated": [ "base", "threadid", @@ -30,7 +34,9 @@ "symb_locks", "region", "thread", - "threadJoins" + "threadJoins", + "unassume", + "apron" ], "path_sens": [ "mutex", @@ -86,6 +92,9 @@ "loopUnrollHeuristic", "memsafetySpecification" ] + }, + "widen": { + "tokens": true } }, "exp": { @@ -105,32 +114,19 @@ }, "witness": { "graphml": { - "enabled": true, - "id": "enumerate", - "unknown": false + "enabled": false }, "yaml": { - "enabled": true, + "enabled": false, "entry-types": [ + "location_invariant", "loop_invariant" ] }, "invariant": { "loop-head": true, - "after-lock": false, - "other": false, - "accessed": false, - "exact": true, - "exclude-vars": [ - "tmp\\(___[0-9]+\\)?", - "cond", - "RETURN", - "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?", - ".*____CPAchecker_TMP_[0-9]+", - "__VERIFIER_assert__cond", - "__ksymtab_.*", - "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+" - ] + "after-lock": true, + "other": true } }, "pre": { From ce917e639d88c0777cd929de635c030fe060cf2b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 1 Nov 2023 13:13:52 +0200 Subject: [PATCH 11/66] Update sv-comp/archive.sh for 2024 --- sv-comp/archive.sh | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/sv-comp/archive.sh b/sv-comp/archive.sh index 9bab49f70d..87dcd75eb9 100755 --- a/sv-comp/archive.sh +++ b/sv-comp/archive.sh @@ -4,7 +4,7 @@ make clean -git tag -m "SV-COMP 2023" svcomp23 +git tag -m "SV-COMP 2024" svcomp24 dune build --profile=release src/goblint.exe rm -f goblint @@ -32,7 +32,8 @@ zip goblint/sv-comp/goblint.zip \ goblint/lib/libboxD.so \ goblint/lib/libpolkaMPQ.so \ goblint/lib/LICENSE.APRON \ - goblint/conf/svcomp23.json \ + goblint/conf/svcomp24.json \ + goblint/conf/svcomp24-validate.json \ goblint/lib/libc/stub/include/assert.h \ goblint/lib/goblint/runtime/include/goblint.h \ goblint/lib/libc/stub/src/stdlib.c \ From 6bad00c305c18578af314b3f1b83ee76aa23f8a6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 1 Nov 2023 13:22:09 +0200 Subject: [PATCH 12/66] Fix Apron license for unpinned package for SV-COMP --- sv-comp/archive.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sv-comp/archive.sh b/sv-comp/archive.sh index 87dcd75eb9..5d8605dc70 100755 --- a/sv-comp/archive.sh +++ b/sv-comp/archive.sh @@ -18,7 +18,7 @@ cp _opam/share/apron/lib/libapron.so lib/ cp _opam/share/apron/lib/liboctD.so lib/ cp _opam/share/apron/lib/libboxD.so lib/ cp _opam/share/apron/lib/libpolkaMPQ.so lib/ -cp _opam/.opam-switch/sources/apron/COPYING lib/LICENSE.APRON +wget -O lib/LICENSE.APRON https://raw.githubusercontent.com/antoinemine/apron/master/COPYING # done outside to ensure archive contains goblint/ directory cd .. From 421abcd41fa5084c3f07854b88a26a1382d253e1 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Tue, 7 Nov 2023 21:44:51 +0100 Subject: [PATCH 13/66] Warn whenever there's allocated heap memory that's unreachable from globals at program exit --- src/analyses/memLeak.ml | 32 ++++++++++++++++++++++++++++---- 1 file changed, 28 insertions(+), 4 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index dbaa2d69fc..f7f555a70a 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -19,6 +19,22 @@ struct let context _ _ = () (* HELPER FUNCTIONS *) + let get_global_vars () = + (* Filtering by GVar seems to account for declarations, as well as definitions of global vars *) + List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + + let get_reachable_mem_from_globals (global_vars:varinfo list) ctx = + global_vars + |> List.map (fun v -> Lval (Var v, NoOffset)) + |> List.filter_map (fun exp -> + match ctx.ask (Queries.MayPointTo exp) with + | a when not (Queries.AD.is_top a) && Queries.AD.cardinal a = 1 -> + begin match List.hd @@ Queries.AD.elements a with + | Queries.AD.Addr.Addr (v, _) when (ctx.ask (Queries.IsHeapVar v)) && not (ctx.ask (Queries.IsMultiple v)) -> Some v + | _ -> None + end + | _ -> None) + let warn_for_multi_threaded ctx = if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then ( set_mem_safety_flag InvalidMemTrack; @@ -27,17 +43,25 @@ struct ) let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx = - let state = ctx.local in - if not @@ D.is_empty state then + let allocated_mem = ctx.local in + if not (D.is_empty allocated_mem) then + let reachable_mem = D.of_list (get_reachable_mem_from_globals (get_global_vars ()) ctx) in + (* Check and warn if there's unreachable allocated memory at program exit *) + let allocated_and_unreachable_mem = D.diff allocated_mem reachable_mem in + if not (D.is_empty allocated_and_unreachable_mem) then ( + set_mem_safety_flag InvalidMemTrack; + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars %a\n" (Pretty.d_list ", " CilType.Varinfo.pretty) (D.elements allocated_and_unreachable_mem) + ); + (* Check and warn if some of the allocated memory is not deallocated at program exit *) match assert_exp_imprecise, exp with | true, Some exp -> set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; - M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty state + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty allocated_mem | _ -> set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; - M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty allocated_mem (* TRANSFER FUNCTIONS *) let return ctx (exp:exp option) (f:fundec) : D.t = From 9f7224ed8d6ffeaeda226b62a71d40b1dbd247f5 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Tue, 7 Nov 2023 21:45:21 +0100 Subject: [PATCH 14/66] Add test cases for unreachable heap memory from globals --- .../regression/76-memleak/08-unreachable-mem.c | 12 ++++++++++++ .../76-memleak/09-unreachable-with-local-var.c | 17 +++++++++++++++++ 2 files changed, 29 insertions(+) create mode 100644 tests/regression/76-memleak/08-unreachable-mem.c create mode 100644 tests/regression/76-memleak/09-unreachable-with-local-var.c diff --git a/tests/regression/76-memleak/08-unreachable-mem.c b/tests/regression/76-memleak/08-unreachable-mem.c new file mode 100644 index 0000000000..08e7b4e741 --- /dev/null +++ b/tests/regression/76-memleak/08-unreachable-mem.c @@ -0,0 +1,12 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +int *g; + +int main(int argc, char const *argv[]) { + g = malloc(sizeof(int)); + // Reference to g's heap contents is lost here + g = NULL; + + return 0; //WARN +} diff --git a/tests/regression/76-memleak/09-unreachable-with-local-var.c b/tests/regression/76-memleak/09-unreachable-with-local-var.c new file mode 100644 index 0000000000..1614b19132 --- /dev/null +++ b/tests/regression/76-memleak/09-unreachable-with-local-var.c @@ -0,0 +1,17 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +int *g; + +int main(int argc, char const *argv[]) { + g = malloc(sizeof(int)); + // Reference to g's heap contents is lost here + g = NULL; + // We get a false positive for p's memory being unreachable + // It's still leaked, but due to free() being commented out + // TODO: Should we only improve the error reporting for unreachable memory in this case? + int *p = malloc(sizeof(int)); + //free(p); + + return 0; //WARN +} From c056b32954f095f4ee4ab3a2fcab536eec35bdf2 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 8 Nov 2023 20:51:19 +0100 Subject: [PATCH 15/66] Remove //TODO comment from `76/09` --- tests/regression/76-memleak/09-unreachable-with-local-var.c | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/tests/regression/76-memleak/09-unreachable-with-local-var.c b/tests/regression/76-memleak/09-unreachable-with-local-var.c index 1614b19132..bc71bb560e 100644 --- a/tests/regression/76-memleak/09-unreachable-with-local-var.c +++ b/tests/regression/76-memleak/09-unreachable-with-local-var.c @@ -7,11 +7,9 @@ int main(int argc, char const *argv[]) { g = malloc(sizeof(int)); // Reference to g's heap contents is lost here g = NULL; - // We get a false positive for p's memory being unreachable - // It's still leaked, but due to free() being commented out - // TODO: Should we only improve the error reporting for unreachable memory in this case? + + // According to `valid-memtrack`, the memory of p is unreachable and we don't have a false positive int *p = malloc(sizeof(int)); - //free(p); return 0; //WARN } From 175b003aa3fae00a07052e6ae58d3cf6a8173cac Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 8 Nov 2023 21:52:45 +0200 Subject: [PATCH 16/66] Don't set `InvalidMemTrack` flag a second time Co-authored-by: Michael Schwarz --- src/analyses/memLeak.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index f7f555a70a..865ecaffc4 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -55,7 +55,6 @@ struct (* Check and warn if some of the allocated memory is not deallocated at program exit *) match assert_exp_imprecise, exp with | true, Some exp -> - set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty allocated_mem | _ -> From 05e4892feac736b520c81c151ed5b2558187e1a0 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 8 Nov 2023 21:53:56 +0200 Subject: [PATCH 17/66] Don't set `InvalidMemTrack` flag a second time Co-authored-by: Michael Schwarz --- src/analyses/memLeak.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 865ecaffc4..fc015f458b 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -58,7 +58,6 @@ struct set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty allocated_mem | _ -> - set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty allocated_mem From f343d74efa850011f6ebebf1ce819f9bc1acefb9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 8 Nov 2023 22:52:27 +0100 Subject: [PATCH 18/66] Add 3 regr. tests for trying out global struct variables --- .../76-memleak/10-global-struct-no-ptr.c | 16 ++++++++++++ .../76-memleak/11-global-struct-ptr.c | 19 ++++++++++++++ .../76-memleak/12-global-nested-struct-ptr.c | 25 +++++++++++++++++++ 3 files changed, 60 insertions(+) create mode 100644 tests/regression/76-memleak/10-global-struct-no-ptr.c create mode 100644 tests/regression/76-memleak/11-global-struct-ptr.c create mode 100644 tests/regression/76-memleak/12-global-nested-struct-ptr.c diff --git a/tests/regression/76-memleak/10-global-struct-no-ptr.c b/tests/regression/76-memleak/10-global-struct-no-ptr.c new file mode 100644 index 0000000000..490b2bb443 --- /dev/null +++ b/tests/regression/76-memleak/10-global-struct-no-ptr.c @@ -0,0 +1,16 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +typedef struct st { + int *a; + int b; +} st; + +st st_nonptr; + +int main(int argc, char const *argv[]) { + st_nonptr.a = malloc(sizeof(int)); + st_nonptr.a = NULL; + + return 0; //WARN +} diff --git a/tests/regression/76-memleak/11-global-struct-ptr.c b/tests/regression/76-memleak/11-global-struct-ptr.c new file mode 100644 index 0000000000..4ebe1c16b8 --- /dev/null +++ b/tests/regression/76-memleak/11-global-struct-ptr.c @@ -0,0 +1,19 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +typedef struct st { + int *a; + int b; +} st; + +st *st_ptr; + +int main(int argc, char const *argv[]) { + st_ptr = malloc(sizeof(st)); + st_ptr->a = malloc(sizeof(int)); + st_ptr->a = NULL; + free(st_ptr); + + // Only st_ptr->a is causing trouble here + return 0; //WARN +} diff --git a/tests/regression/76-memleak/12-global-nested-struct-ptr.c b/tests/regression/76-memleak/12-global-nested-struct-ptr.c new file mode 100644 index 0000000000..e0f5175064 --- /dev/null +++ b/tests/regression/76-memleak/12-global-nested-struct-ptr.c @@ -0,0 +1,25 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +typedef struct st { + int *a; + int b; +} st; + +typedef struct st2 { + st *st_ptr; +} st2; + +st2 *st_var; + +int main(int argc, char const *argv[]) { + st_var = malloc(sizeof(st2)); + st_var->st_ptr = malloc(sizeof(st)); + st_var->st_ptr->a = malloc(sizeof(int)); + st_var->st_ptr->a = NULL; + free(st_var->st_ptr); + free(st_var); + + // Only st_var->st_ptr->a is causing trouble here + return 0; //WARN +} From 7fc834308201ea8e7d2cd0d8c79bfe0c81833cae Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Nov 2023 13:56:10 +0200 Subject: [PATCH 19/66] Fix relation read_globals_to_locals reading untracked variables --- src/analyses/apron/relationAnalysis.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 13f549fc44..0fa26781dd 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -70,7 +70,7 @@ struct let visitor = object inherit nopCilVisitor method! vlval = function - | (Var v, NoOffset) when v.vglob || ThreadEscape.has_escaped ask v -> + | (Var v, NoOffset) when (v.vglob || ThreadEscape.has_escaped ask v) && RD.Tracked.varinfo_tracked v -> let v_in = if VH.mem v_ins v then VH.find v_ins v From fbc66e32b897891d5a00dbe47ee719df7de75772 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Nov 2023 15:18:59 +0200 Subject: [PATCH 20/66] Remove default Apron polyhedra in svcomp24-validate conf --- conf/svcomp24-validate.json | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json index 6479bd01b5..ce11af12f6 100644 --- a/conf/svcomp24-validate.json +++ b/conf/svcomp24-validate.json @@ -12,10 +12,6 @@ "float": { "interval": true }, - "apron": { - "domain": "polyhedra", - "strengthening": true - }, "activated": [ "base", "threadid", @@ -35,8 +31,7 @@ "region", "thread", "threadJoins", - "unassume", - "apron" + "unassume" ], "path_sens": [ "mutex", From 6decbddb2503a7633c73b3151df40e158417ede8 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 15 Nov 2023 23:20:11 +0100 Subject: [PATCH 21/66] Improve the detection of reachable memory through global struct vars --- src/analyses/memLeak.ml | 89 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 88 insertions(+), 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index fc015f458b..4d7e864c06 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -23,6 +23,14 @@ struct (* Filtering by GVar seems to account for declarations, as well as definitions of global vars *) List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + let get_global_struct_ptr_vars () = + List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + |> List.filter (fun v -> match v.vtype with TPtr (TComp _, _) | TPtr ((TNamed ({ttype = TComp _; _}, _)), _) -> true | _ -> false) + + let get_global_struct_non_ptr_vars () = + List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + |> List.filter (fun v -> match v.vtype with TComp (_, _) | (TNamed ({ttype = TComp _; _}, _)) -> true | _ -> false) + let get_reachable_mem_from_globals (global_vars:varinfo list) ctx = global_vars |> List.map (fun v -> Lval (Var v, NoOffset)) @@ -35,6 +43,81 @@ struct end | _ -> None) + let rec get_reachable_mem_from_str_ptr_globals (global_struct_ptr_vars:varinfo list) ctx = + let eval_value_of_heap_var heap_var = + match ctx.ask (Queries.EvalValue (Lval (Var heap_var, NoOffset))) with + | a when not (Queries.VD.is_top a) -> + begin match a with + | Struct s -> + List.fold_left (fun acc f -> + if isPointerType f.ftype then + begin match ValueDomain.Structs.get s f with + | Queries.VD.Address a -> + let reachable_from_addr_set = + List.fold_left (fun acc addr -> + match addr with + | Queries.AD.Addr.Addr (v, _) -> List.append acc (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) + | _ -> acc + ) [] (Queries.AD.elements a) + in List.append acc reachable_from_addr_set + | _ -> acc + end + else acc + ) [] (ValueDomain.Structs.keys s) + | _ -> [] + end + | _ -> [] + in + let get_pts_of_non_heap_ptr_var var = + match ctx.ask (Queries.MayPointTo (Lval (Var var, NoOffset))) with + | a when not (Queries.AD.is_top a) && Queries.AD.cardinal a = 1 -> + begin match List.hd @@ Queries.AD.elements a with + | Queries.AD.Addr.Addr (v, _) when (ctx.ask (Queries.IsHeapVar v)) && not (ctx.ask (Queries.IsMultiple v)) -> v :: (eval_value_of_heap_var v) + | Queries.AD.Addr.Addr (v, _) when not (ctx.ask (Queries.IsAllocVar v)) && isPointerType v.vtype -> get_reachable_mem_from_str_ptr_globals [v] ctx + | _ -> [] + end + | _ -> [] + in + global_struct_ptr_vars + |> List.fold_left (fun acc var -> + if ctx.ask (Queries.IsHeapVar var) then eval_value_of_heap_var var + else if not (ctx.ask (Queries.IsAllocVar var)) && isPointerType var.vtype then get_pts_of_non_heap_ptr_var var + else acc + ) [] + + let get_reachable_mem_from_str_non_ptr_globals (global_struct_non_ptr_vars:varinfo list) ctx = + global_struct_non_ptr_vars + (* Filter out global struct vars that don't have pointer fields *) + |> List.filter_map (fun v -> + match ctx.ask (Queries.EvalValue (Lval (Var v, NoOffset))) with + | a when not (Queries.VD.is_top a) -> + begin match a with + | Queries.VD.Struct s -> + let struct_fields = ValueDomain.Structs.keys s in + let ptr_struct_fields = List.filter (fun f -> isPointerType f.ftype) struct_fields in + if List.length ptr_struct_fields = 0 then None else Some (s, ptr_struct_fields) + | _ -> None + end + | _ -> None + ) + |> List.fold_left (fun acc_struct (s, fields) -> + let reachable_from_fields = + List.fold_left (fun acc_field field -> + match ValueDomain.Structs.get s field with + | Queries.VD.Address a -> + let reachable_from_addr_set = + List.fold_left (fun acc_addr addr -> + match addr with + | Queries.AD.Addr.Addr (v, _) -> List.append acc_addr (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) + | _ -> acc_addr + ) [] (Queries.AD.elements a) + in List.append acc_field reachable_from_addr_set + | _ -> acc_field + ) [] fields + in + List.append acc_struct reachable_from_fields + ) [] + let warn_for_multi_threaded ctx = if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then ( set_mem_safety_flag InvalidMemTrack; @@ -45,7 +128,11 @@ struct let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx = let allocated_mem = ctx.local in if not (D.is_empty allocated_mem) then - let reachable_mem = D.of_list (get_reachable_mem_from_globals (get_global_vars ()) ctx) in + let reachable_mem_from_non_struct_globals = D.of_list (get_reachable_mem_from_globals (get_global_vars ()) ctx) in + let reachable_mem_from_struct_ptr_globals = D.of_list (get_reachable_mem_from_str_ptr_globals (get_global_struct_ptr_vars ()) ctx) in + let reachable_mem_from_struct_non_ptr_globals = D.of_list (get_reachable_mem_from_str_non_ptr_globals (get_global_struct_non_ptr_vars ()) ctx) in + let reachable_mem_from_struct_globals = D.join reachable_mem_from_struct_ptr_globals reachable_mem_from_struct_non_ptr_globals in + let reachable_mem = D.join reachable_mem_from_non_struct_globals reachable_mem_from_struct_globals in (* Check and warn if there's unreachable allocated memory at program exit *) let allocated_and_unreachable_mem = D.diff allocated_mem reachable_mem in if not (D.is_empty allocated_and_unreachable_mem) then ( From c3804260bf8bc43ea90e76ea9f2cf0f7ebb7186f Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 15 Nov 2023 23:20:53 +0100 Subject: [PATCH 22/66] Add regr. tests for reachable memory through global struct vars --- .../13-global-nested-struct-ptr-reachable.c | 29 +++++++++++++++++++ ...4-global-nested-struct-non-ptr-reachable.c | 25 ++++++++++++++++ 2 files changed, 54 insertions(+) create mode 100644 tests/regression/76-memleak/13-global-nested-struct-ptr-reachable.c create mode 100644 tests/regression/76-memleak/14-global-nested-struct-non-ptr-reachable.c diff --git a/tests/regression/76-memleak/13-global-nested-struct-ptr-reachable.c b/tests/regression/76-memleak/13-global-nested-struct-ptr-reachable.c new file mode 100644 index 0000000000..1726625a59 --- /dev/null +++ b/tests/regression/76-memleak/13-global-nested-struct-ptr-reachable.c @@ -0,0 +1,29 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +typedef struct st { + int *a; + int b; +} st; + +typedef struct st2 { + st *st_ptr; +} st2; + +st2 *st_var; + +int main(int argc, char const *argv[]) { + st_var = malloc(sizeof(st2)); + st_var->st_ptr = malloc(sizeof(st)); + int *local_ptr = malloc(sizeof(int)); + st_var->st_ptr->a = local_ptr; + local_ptr = NULL; + + free(st_var->st_ptr); + free(st_var); + + // local_ptr's memory is reachable through st_var->st_ptr->a + // It's leaked, because we don't call free() on it + // Hence, there should be a single warning for a memory leak, but not for unreachable memory + return 0; //WARN +} diff --git a/tests/regression/76-memleak/14-global-nested-struct-non-ptr-reachable.c b/tests/regression/76-memleak/14-global-nested-struct-non-ptr-reachable.c new file mode 100644 index 0000000000..1153bd81e0 --- /dev/null +++ b/tests/regression/76-memleak/14-global-nested-struct-non-ptr-reachable.c @@ -0,0 +1,25 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +typedef struct st { + int *a; + int b; +} st; + +typedef struct st2 { + st *st_ptr; +} st2; + +st2 st_var; + +int main(int argc, char const *argv[]) { + st_var.st_ptr = malloc(sizeof(st)); + int *local_ptr = malloc(sizeof(int)); + st_var.st_ptr->a = local_ptr; + local_ptr = NULL; + free(st_var.st_ptr); + + // local_ptr's memory is reachable through st_var.st_ptr->a, but it's not freed + // Hence, there should be only a single warning for a memory leak, but not for unreachable memory + return 0; //WARN +} From 845910410bbda2f9964ccd727d63a6e7b811ac7f Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 15 Nov 2023 23:33:58 +0100 Subject: [PATCH 23/66] Fix semgrep warning for using `List.length` for an emptiness check --- src/analyses/memLeak.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index a5d357d9c8..51a5a2ff75 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -96,7 +96,7 @@ struct | Queries.VD.Struct s -> let struct_fields = ValueDomain.Structs.keys s in let ptr_struct_fields = List.filter (fun f -> isPointerType f.ftype) struct_fields in - if List.length ptr_struct_fields = 0 then None else Some (s, ptr_struct_fields) + if ptr_struct_fields = [] then None else Some (s, ptr_struct_fields) | _ -> None end | _ -> None From f209afdae5be755eeded7bb0080473fe15571b7d Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 16 Nov 2023 07:52:56 +0100 Subject: [PATCH 24/66] First attempt to improve precision for multi-threaded valid-memcleanup --- src/analyses/memLeak.ml | 72 +++++++++++++++++++++++++++++++++-------- 1 file changed, 59 insertions(+), 13 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 9c09c05cf6..c64bb95697 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -6,30 +6,50 @@ open MessageCategory open AnalysisStateUtil module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) - +module WasMallocCalled = BoolDomain.MustBool module Spec : Analyses.MCPSpec = struct include Analyses.IdentitySpec let name () = "memLeak" - module D = ToppedVarInfoSet + (* module D = ToppedVarInfoSet *) + module D = Lattice.Prod(ToppedVarInfoSet)(WasMallocCalled) module C = D module P = IdentityP (D) + module G = ToppedVarInfoSet + module V = + struct + include ThreadIdDomain.Thread + include StdV + end let context _ d = d (* HELPER FUNCTIONS *) - let warn_for_multi_threaded ctx = - if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then ( + let warn_for_multi_threaded_due_to_abort ctx = + let state = ctx.local in + if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) && snd state then ( set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; - M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program isn't running in single-threaded mode. A memory leak might occur due to multi-threading" + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program aborted while running in multi-threaded mode. A memory leak might occur" + ) + + (* If [is_return] is set to [true], then a thread return occurred, else a thread join *) + let warn_for_thread_return_or_exit current_thread ctx is_return = + let global_state = ctx.global current_thread in + if not (G.is_empty global_state) then ( + set_mem_safety_flag InvalidMemcleanup; + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s" (if is_return then "return" else "join") ) + (* if not (ToppedVarInfoSet.is_empty (fst state)) && snd state then ( + set_mem_safety_flag InvalidMemcleanup; + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s" (if is_return then "return" else "join") + ) *) let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx = let state = ctx.local in - if not @@ D.is_empty state then + if not (ToppedVarInfoSet.is_empty (fst state)) then match assert_exp_imprecise, exp with | true, Some exp -> set_mem_safety_flag InvalidMemTrack; @@ -42,6 +62,12 @@ struct (* TRANSFER FUNCTIONS *) let return ctx (exp:exp option) (f:fundec) : D.t = + (* Check for a valid-memcleanup violation in a multi-threaded setting *) + if (ctx.ask (Queries.MayBeThreadReturn)) then ( + match ctx.ask (Queries.CurrentThreadId) with + | `Lifted tid -> warn_for_thread_return_or_exit tid ctx true + | _ -> () + ); (* Returning from "main" is one possible program exit => need to check for memory leaks *) if f.svar.vname = "main" then check_for_mem_leak ctx; ctx.local @@ -53,25 +79,39 @@ struct | Malloc _ | Calloc _ | Realloc _ -> - (* Warn about multi-threaded programs as soon as we encounter a dynamic memory allocation function *) - warn_for_multi_threaded ctx; begin match ctx.ask (Queries.AllocVar {on_stack = false}) with - | `Lifted var -> D.add var state - | _ -> state + | `Lifted var -> + begin match ctx.ask (Queries.CurrentThreadId) with + | `Lifted tid -> + let current_globals = ctx.global tid in + let globals_to_side_effect = G.add var current_globals in + ctx.sideg tid globals_to_side_effect; + | _ -> () + end; + (ToppedVarInfoSet.add var (fst state), true) + | _ -> (fst state, true) end | Free ptr -> begin match ctx.ask (Queries.MayPointTo ptr) with | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 -> (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *) begin match Queries.AD.choose ad with - | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state (* Unique pointed to heap vars *) + | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> + begin match ctx.ask (Queries.CurrentThreadId) with + | `Lifted tid -> + let current_globals = ctx.global tid in + let globals_to_side_effect = G.remove v current_globals in + ctx.sideg tid globals_to_side_effect + | _ -> () + end; + (ToppedVarInfoSet.remove v (fst state), snd state) (* Unique pointed to heap vars *) | _ -> state end | _ -> state end | Abort -> - (* An "Abort" special function indicates program exit => need to check for memory leaks *) - check_for_mem_leak ctx; + (* Upon a call to the "Abort" special function, we give up and conservatively warn *) + warn_for_multi_threaded_due_to_abort ctx; state | Assert { exp; _ } -> let warn_for_assert_exp = @@ -89,6 +129,12 @@ struct in warn_for_assert_exp; state + | ThreadExit _ -> + begin match ctx.ask (Queries.CurrentThreadId) with + | `Lifted tid -> warn_for_thread_return_or_exit tid ctx false + | _ -> () + end; + state | _ -> state let startstate v = D.bot () From c0fe89e93352f530317cf1a7836684de65b216f3 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 16 Nov 2023 07:53:21 +0100 Subject: [PATCH 25/66] Add regr. test cases for multi-threaded valid-memcleanup --- .../08-invalid-memcleanup-multi-threaded.c | 33 +++++++++++++++++++ ...-invalid-memcleanup-multi-threaded-abort.c | 33 +++++++++++++++++++ 2 files changed, 66 insertions(+) create mode 100644 tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c create mode 100644 tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c diff --git a/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c b/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c new file mode 100644 index 0000000000..50b17fa65d --- /dev/null +++ b/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c @@ -0,0 +1,33 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include +#include + +int *g; +int *m1; +int *m2; + +void *f1(void *arg) { + m1 = malloc(sizeof(int)); + // Thread t1 leaks m1 here + pthread_exit(NULL); //WARN +} + +void *f2(void *arg) { + m2 = malloc(sizeof(int)); + free(m2); // No leak for thread t2, since it calls free before exiting + pthread_exit(NULL); //NOWARN +} + +int main(int argc, char const *argv[]) { + g = malloc(sizeof(int)); + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + + pthread_t t2; + pthread_create(&t2, NULL, f2, NULL); + + free(g); + + // main thread is not leaking anything + return 0; //NOWARN +} diff --git a/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c b/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c new file mode 100644 index 0000000000..9aef45198e --- /dev/null +++ b/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c @@ -0,0 +1,33 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include +#include + +int *g; +int *m1; +int *m2; + +void *f1(void *arg) { + m1 = malloc(sizeof(int)); + // Thread t1 leaks m1 here + exit(2); //WARN +} + +void *f2(void *arg) { + m2 = malloc(sizeof(int)); + free(m2); // No leak for thread t2, since it calls free before exiting + pthread_exit(NULL); //NOWARN +} + +int main(int argc, char const *argv[]) { + g = malloc(sizeof(int)); + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + + pthread_t t2; + pthread_create(&t2, NULL, f2, NULL); + + free(g); + + // main thread is not leaking anything + return 0; //NOWARN +} From 6f549915ebd3c319422e36acab66eb90c614eea5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 17 Nov 2023 12:57:05 +0200 Subject: [PATCH 26/66] Fix YAML witness invariants for unrolled loops (closes #1225) --- src/witness/yamlWitness.ml | 96 +++++++++++++++++++++++--------------- 1 file changed, 59 insertions(+), 37 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 9e8ebeff51..dc4890753d 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -145,6 +145,16 @@ struct module FCMap = BatHashtbl.Make (Printable.Prod (CilType.Fundec) (Spec.C)) type con_inv = {node: Node.t; context: Spec.C.t; invariant: Invariant.t; state: Spec.D.t} + (* TODO: fix location hack *) + module LH = BatHashtbl.Make (CilType.Location) + let location2nodes: Node.t list LH.t Lazy.t = lazy ( + let lh = LH.create 113 in + NH.iter (fun n _ -> + LH.modify_def [] (Node.location n) (List.cons n) lh + ) (Lazy.force nh); + lh + ) + let write () = let input_files = GobConfig.get_string_list "files" in let data_model = match GobConfig.get_string "exp.architecture" with @@ -208,26 +218,32 @@ struct (* Generate location invariants (without precondition) *) let entries = if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then ( - NH.fold (fun n local acc -> - let loc = Node.location n in - if is_invariant_node n then ( - let lvals = local_lvals n local in - match R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals}) with - | `Lifted inv -> - let invs = WitnessUtil.InvariantExp.process_exp inv in - List.fold_left (fun acc inv -> - let location_function = (Node.find_fundec n).svar.vname in - let location = Entry.location ~location:loc ~location_function in - let invariant = Entry.invariant (CilType.Exp.show inv) in - let entry = Entry.location_invariant ~task ~location ~invariant in - entry :: acc - ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) - acc - ) - else + LH.fold (fun loc ns acc -> + let fundec = ref None in + let inv = List.fold_left (fun acc n -> + if is_invariant_node n then ( + fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) + let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in + let lvals = local_lvals n local in + Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) + ) + else + acc + ) (Invariant.bot ()) ns + in + match inv with + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let location_function = (Option.get !fundec).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invariant = Entry.invariant (CilType.Exp.show inv) in + let entry = Entry.location_invariant ~task ~location ~invariant in + entry :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) acc - ) (Lazy.force nh) entries + ) (Lazy.force location2nodes) entries ) else entries @@ -236,25 +252,31 @@ struct (* Generate loop invariants (without precondition) *) let entries = if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then ( - NH.fold (fun n local acc -> - let loc = Node.location n in - if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then ( - match R.ask_local_node n ~local (Invariant Invariant.default_context) with - | `Lifted inv -> - let invs = WitnessUtil.InvariantExp.process_exp inv in - List.fold_left (fun acc inv -> - let location_function = (Node.find_fundec n).svar.vname in - let location = Entry.location ~location:loc ~location_function in - let invariant = Entry.invariant (CilType.Exp.show inv) in - let entry = Entry.loop_invariant ~task ~location ~invariant in - entry :: acc - ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) - acc - ) - else + LH.fold (fun loc ns acc -> + let fundec = ref None in + let inv = List.fold_left (fun acc n -> + if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then ( + fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) + let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in + Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) + ) + else + acc + ) (Invariant.bot ()) ns + in + match inv with + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let location_function = (Option.get !fundec).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invariant = Entry.invariant (CilType.Exp.show inv) in + let entry = Entry.loop_invariant ~task ~location ~invariant in + entry :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) acc - ) (Lazy.force nh) entries + ) (Lazy.force location2nodes) entries ) else entries From 952b90dbfcfd2c8ef4750abf4daca6cd5da6d8bd Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 17 Nov 2023 13:19:09 +0200 Subject: [PATCH 27/66] Fix bisect_ppx build --- src/witness/yamlWitness.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 023212fa42..22800c07dc 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -251,7 +251,7 @@ struct fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in let lvals = local_lvals n local in - Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) + Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) else acc @@ -284,7 +284,7 @@ struct if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then ( fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in - Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) + Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) else acc @@ -448,7 +448,7 @@ struct fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in let lvals = local_lvals n local in - Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) + Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) else acc @@ -481,7 +481,7 @@ struct if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then ( fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in - Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) + Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) else acc From 4ae355695675d2030b00c5df991666b8952d6357 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 17 Nov 2023 15:11:36 +0200 Subject: [PATCH 28/66] Fix missing unrolled iterations in YAML witness invariants Unrolled loop heads are different nodes, which aren't actually loop heads. For sound invariants, they must also be included if at a location if at least one is. --- src/witness/yamlWitness.ml | 152 ++++++++++++++++++------------------- 1 file changed, 76 insertions(+), 76 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 22800c07dc..1f83c8625e 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -245,29 +245,29 @@ struct let entries = if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then ( LH.fold (fun loc ns acc -> - let fundec = ref None in - let inv = List.fold_left (fun acc n -> - if is_invariant_node n then ( + if List.exists is_invariant_node ns then ( + let fundec = ref None in + let inv = List.fold_left (fun acc n -> fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in let lvals = local_lvals n local in Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) - ) - else - acc - ) (Invariant.bot ()) ns - in - match inv with - | `Lifted inv -> - let invs = WitnessUtil.InvariantExp.process_exp inv in - List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in - let invariant = Entry.invariant (CilType.Exp.show inv) in - let entry = Entry.location_invariant ~task ~location ~invariant in - entry :: acc - ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + ) (Invariant.bot ()) ns + in + match inv with + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let location_function = (Option.get !fundec).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invariant = Entry.invariant (CilType.Exp.show inv) in + let entry = Entry.location_invariant ~task ~location ~invariant in + entry :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + acc + ) + else acc ) (Lazy.force location2nodes) entries ) @@ -279,28 +279,28 @@ struct let entries = if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then ( LH.fold (fun loc ns acc -> - let fundec = ref None in - let inv = List.fold_left (fun acc n -> - if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then ( + if WitnessInvariant.emit_loop_head && List.exists (WitnessUtil.NH.mem WitnessInvariant.loop_heads) ns then ( + let fundec = ref None in + let inv = List.fold_left (fun acc n -> fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) - ) - else - acc - ) (Invariant.bot ()) ns - in - match inv with - | `Lifted inv -> - let invs = WitnessUtil.InvariantExp.process_exp inv in - List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in - let invariant = Entry.invariant (CilType.Exp.show inv) in - let entry = Entry.loop_invariant ~task ~location ~invariant in - entry :: acc - ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + ) (Invariant.bot ()) ns + in + match inv with + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let location_function = (Option.get !fundec).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invariant = Entry.invariant (CilType.Exp.show inv) in + let entry = Entry.loop_invariant ~task ~location ~invariant in + entry :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + acc + ) + else acc ) (Lazy.force location2nodes) entries ) @@ -442,29 +442,29 @@ struct let invariants = if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then ( LH.fold (fun loc ns acc -> - let fundec = ref None in - let inv = List.fold_left (fun acc n -> - if is_invariant_node n then ( + if List.exists is_invariant_node ns then ( + let fundec = ref None in + let inv = List.fold_left (fun acc n -> fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in let lvals = local_lvals n local in Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) - ) - else - acc - ) (Invariant.bot ()) ns - in - match inv with - | `Lifted inv -> - let invs = WitnessUtil.InvariantExp.process_exp inv in - List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in - let invariant = CilType.Exp.show inv in - let invariant = Entry.location_invariant' ~location ~invariant in - invariant :: acc - ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + ) (Invariant.bot ()) ns + in + match inv with + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let location_function = (Option.get !fundec).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invariant = CilType.Exp.show inv in + let invariant = Entry.location_invariant' ~location ~invariant in + invariant :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + acc + ) + else acc ) (Lazy.force location2nodes) invariants ) @@ -476,28 +476,28 @@ struct let invariants = if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then ( LH.fold (fun loc ns acc -> - let fundec = ref None in - let inv = List.fold_left (fun acc n -> - if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then ( + if WitnessInvariant.emit_loop_head && List.exists (WitnessUtil.NH.mem WitnessInvariant.loop_heads) ns then ( + let fundec = ref None in + let inv = List.fold_left (fun acc n -> fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) - ) - else - acc - ) (Invariant.bot ()) ns - in - match inv with - | `Lifted inv -> - let invs = WitnessUtil.InvariantExp.process_exp inv in - List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in - let invariant = CilType.Exp.show inv in - let invariant = Entry.loop_invariant' ~location ~invariant in - invariant :: acc - ) acc invs - | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + ) (Invariant.bot ()) ns + in + match inv with + | `Lifted inv -> + let invs = WitnessUtil.InvariantExp.process_exp inv in + List.fold_left (fun acc inv -> + let location_function = (Option.get !fundec).svar.vname in + let location = Entry.location ~location:loc ~location_function in + let invariant = CilType.Exp.show inv in + let invariant = Entry.loop_invariant' ~location ~invariant in + invariant :: acc + ) acc invs + | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *) + acc + ) + else acc ) (Lazy.force location2nodes) invariants ) From 0fb479f506c99e1e415c08d157ae09a8a768fa4c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 17 Nov 2023 15:16:48 +0200 Subject: [PATCH 29/66] Refactor YAML witness fundec lookup --- src/witness/yamlWitness.ml | 28 ++++++++++++---------------- 1 file changed, 12 insertions(+), 16 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 1f83c8625e..1f106c936e 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -246,9 +246,7 @@ struct if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then ( LH.fold (fun loc ns acc -> if List.exists is_invariant_node ns then ( - let fundec = ref None in let inv = List.fold_left (fun acc n -> - fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in let lvals = local_lvals n local in Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) @@ -256,10 +254,11 @@ struct in match inv with | `Lifted inv -> + let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in let invs = WitnessUtil.InvariantExp.process_exp inv in List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in let invariant = Entry.invariant (CilType.Exp.show inv) in let entry = Entry.location_invariant ~task ~location ~invariant in entry :: acc @@ -280,19 +279,18 @@ struct if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then ( LH.fold (fun loc ns acc -> if WitnessInvariant.emit_loop_head && List.exists (WitnessUtil.NH.mem WitnessInvariant.loop_heads) ns then ( - let fundec = ref None in let inv = List.fold_left (fun acc n -> - fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) (Invariant.bot ()) ns in match inv with | `Lifted inv -> + let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in let invs = WitnessUtil.InvariantExp.process_exp inv in List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in let invariant = Entry.invariant (CilType.Exp.show inv) in let entry = Entry.loop_invariant ~task ~location ~invariant in entry :: acc @@ -443,9 +441,7 @@ struct if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then ( LH.fold (fun loc ns acc -> if List.exists is_invariant_node ns then ( - let fundec = ref None in let inv = List.fold_left (fun acc n -> - fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in let lvals = local_lvals n local in Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) @@ -453,10 +449,11 @@ struct in match inv with | `Lifted inv -> + let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in let invs = WitnessUtil.InvariantExp.process_exp inv in List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in let invariant = CilType.Exp.show inv in let invariant = Entry.location_invariant' ~location ~invariant in invariant :: acc @@ -477,19 +474,18 @@ struct if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then ( LH.fold (fun loc ns acc -> if WitnessInvariant.emit_loop_head && List.exists (WitnessUtil.NH.mem WitnessInvariant.loop_heads) ns then ( - let fundec = ref None in let inv = List.fold_left (fun acc n -> - fundec := Some (Node.find_fundec n); (* TODO: fix location hack *) let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) (Invariant.bot ()) ns in match inv with | `Lifted inv -> + let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *) + let location_function = fundec.svar.vname in + let location = Entry.location ~location:loc ~location_function in let invs = WitnessUtil.InvariantExp.process_exp inv in List.fold_left (fun acc inv -> - let location_function = (Option.get !fundec).svar.vname in - let location = Entry.location ~location:loc ~location_function in let invariant = CilType.Exp.show inv in let invariant = Entry.loop_invariant' ~location ~invariant in invariant :: acc From 3c89ece9f7630beda3a057b1705a28ea0496dc65 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 17 Nov 2023 15:32:41 +0200 Subject: [PATCH 30/66] Fix YamlWitness indentation --- src/witness/yamlWitness.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 1f106c936e..ee370f2b6a 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -445,7 +445,7 @@ struct let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in let lvals = local_lvals n local in Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) - ) (Invariant.bot ()) ns + ) (Invariant.bot ()) ns in match inv with | `Lifted inv -> From b57e80d2f4a82102af284c6c6f3a26eba35d24b5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 17 Nov 2023 15:54:27 +0200 Subject: [PATCH 31/66] Bump YAML entry size for large unrolled invariants --- src/witness/yamlWitness.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index ee370f2b6a..c80611c83f 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -148,7 +148,7 @@ let yaml_entries_to_file ?(invariants=0) yaml_entries file = (* Yaml_unix.to_file_exn file yaml *) (* to_file/to_string uses a fixed-size buffer... *) (* estimate how big it should be + extra in case empty *) - let text = match Yaml.to_string ~len:((List.length yaml_entries + invariants) * 4096 + 2048) yaml with + let text = match Yaml.to_string ~len:((List.length yaml_entries + invariants) * 8192 + 2048) yaml with | Ok text -> text | Error (`Msg m) -> failwith ("Yaml.to_string: " ^ m) in From f70948296572a81d36f734522c1441db3fec19bb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 17 Nov 2023 16:07:37 +0200 Subject: [PATCH 32/66] Make YAML output buffer sizing exponential --- src/util/std/gobYaml.ml | 11 +++++++++++ src/witness/yamlWitness.ml | 13 ++++++------- 2 files changed, 17 insertions(+), 7 deletions(-) diff --git a/src/util/std/gobYaml.ml b/src/util/std/gobYaml.ml index a4f3e597aa..131daaaebb 100644 --- a/src/util/std/gobYaml.ml +++ b/src/util/std/gobYaml.ml @@ -1,3 +1,14 @@ +let to_string' ?(len=65535 * 4) ?encoding ?scalar_style ?layout_style v = + assert (len >= 1); + let rec aux len = + match Yaml.to_string ~len ?encoding ?scalar_style ?layout_style v with + | Ok _ as o -> o + | Error (`Msg ("scalar failed" | "doc_end failed")) when len < Sys.max_string_length / 2 -> + aux (len * 2) + | Error (`Msg _) as e -> e + in + aux len + include Yaml.Util include GobResult.Syntax diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index c80611c83f..635ba4ad72 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -143,12 +143,11 @@ struct } end -let yaml_entries_to_file ?(invariants=0) yaml_entries file = +let yaml_entries_to_file yaml_entries file = let yaml = `A yaml_entries in (* Yaml_unix.to_file_exn file yaml *) (* to_file/to_string uses a fixed-size buffer... *) - (* estimate how big it should be + extra in case empty *) - let text = match Yaml.to_string ~len:((List.length yaml_entries + invariants) * 8192 + 2048) yaml with + let text = match GobYaml.to_string' yaml with | Ok text -> text | Error (`Msg m) -> failwith ("Yaml.to_string: " ^ m) in @@ -432,7 +431,7 @@ struct in (* Generate invariant set *) - let (entries, invariants) = + let entries = if entry_type_enabled YamlWitnessType.InvariantSet.entry_type then ( let invariants = [] in @@ -503,10 +502,10 @@ struct let invariants = List.rev invariants in let entry = Entry.invariant_set ~task ~invariants in - (entry :: entries, List.length invariants) + entry :: entries ) else - (entries, 0) + entries in let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in (* reverse to make entries in file in the same order as generation messages *) @@ -515,7 +514,7 @@ struct (Pretty.dprintf "total generation entries: %d" (List.length yaml_entries), None); ]; - yaml_entries_to_file ~invariants yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path")) + yaml_entries_to_file yaml_entries (Fpath.v (GobConfig.get_string "witness.yaml.path")) let write () = Timing.wrap "yaml witness" write () From 7289ec341760ab06ce518c7520b076ca50688bb3 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 18 Nov 2023 14:38:13 +0100 Subject: [PATCH 33/66] Use solely local state for multi-threaded valid-memcleanup --- src/analyses/memLeak.ml | 61 ++++++++++++++++++----------------------- 1 file changed, 27 insertions(+), 34 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index c64bb95697..64fe7ab957 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -6,6 +6,7 @@ open MessageCategory open AnalysisStateUtil module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) +module ThreadsToHeapVarsMap = MapDomain.MapBot(ThreadIdDomain.Thread)(ToppedVarInfoSet) module WasMallocCalled = BoolDomain.MustBool module Spec : Analyses.MCPSpec = struct @@ -13,16 +14,9 @@ struct let name () = "memLeak" - (* module D = ToppedVarInfoSet *) - module D = Lattice.Prod(ToppedVarInfoSet)(WasMallocCalled) + module D = Lattice.Prod(ThreadsToHeapVarsMap)(WasMallocCalled) module C = D module P = IdentityP (D) - module G = ToppedVarInfoSet - module V = - struct - include ThreadIdDomain.Thread - include StdV - end let context _ d = d @@ -35,21 +29,18 @@ struct M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program aborted while running in multi-threaded mode. A memory leak might occur" ) - (* If [is_return] is set to [true], then a thread return occurred, else a thread join *) + (* If [is_return] is set to [true], then a thread return occurred, else a thread exit *) let warn_for_thread_return_or_exit current_thread ctx is_return = - let global_state = ctx.global current_thread in - if not (G.is_empty global_state) then ( + let state = ctx.local in + let heap_vars_of_curr_tid = ThreadsToHeapVarsMap.find current_thread (fst state) in + if not (ToppedVarInfoSet.is_empty heap_vars_of_curr_tid) then ( set_mem_safety_flag InvalidMemcleanup; - M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s" (if is_return then "return" else "join") + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s for thread %a" (if is_return then "return" else "exit") ThreadIdDomain.Thread.pretty current_thread ) - (* if not (ToppedVarInfoSet.is_empty (fst state)) && snd state then ( - set_mem_safety_flag InvalidMemcleanup; - M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s" (if is_return then "return" else "join") - ) *) let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx = let state = ctx.local in - if not (ToppedVarInfoSet.is_empty (fst state)) then + if not (ThreadsToHeapVarsMap.for_all (fun tid heap_vars -> ToppedVarInfoSet.is_empty heap_vars) (fst state)) then match assert_exp_imprecise, exp with | true, Some exp -> set_mem_safety_flag InvalidMemTrack; @@ -58,14 +49,15 @@ struct | _ -> set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; - M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables" (* TRANSFER FUNCTIONS *) let return ctx (exp:exp option) (f:fundec) : D.t = (* Check for a valid-memcleanup violation in a multi-threaded setting *) if (ctx.ask (Queries.MayBeThreadReturn)) then ( match ctx.ask (Queries.CurrentThreadId) with - | `Lifted tid -> warn_for_thread_return_or_exit tid ctx true + | `Lifted tid -> + warn_for_thread_return_or_exit tid ctx true | _ -> () ); (* Returning from "main" is one possible program exit => need to check for memory leaks *) @@ -83,34 +75,34 @@ struct | `Lifted var -> begin match ctx.ask (Queries.CurrentThreadId) with | `Lifted tid -> - let current_globals = ctx.global tid in - let globals_to_side_effect = G.add var current_globals in - ctx.sideg tid globals_to_side_effect; - | _ -> () - end; - (ToppedVarInfoSet.add var (fst state), true) + ((ThreadsToHeapVarsMap.add tid (ToppedVarInfoSet.singleton var) (fst state)), true) + | _ -> (fst state, true) + end | _ -> (fst state, true) end | Free ptr -> begin match ctx.ask (Queries.MayPointTo ptr) with - | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 -> + (* TODO: The cardinality of 1 seems to lead to the situation where only free() calls in main() are detected here (affects 76/08 and 76/09) *) + (* | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 -> *) + | ad when not (Queries.AD.is_top ad) -> (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *) begin match Queries.AD.choose ad with | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> begin match ctx.ask (Queries.CurrentThreadId) with | `Lifted tid -> - let current_globals = ctx.global tid in - let globals_to_side_effect = G.remove v current_globals in - ctx.sideg tid globals_to_side_effect - | _ -> () - end; - (ToppedVarInfoSet.remove v (fst state), snd state) (* Unique pointed to heap vars *) + let heap_vars_of_tid = ThreadsToHeapVarsMap.find tid (fst state) in + let heap_vars_of_tid_without_v = ToppedVarInfoSet.remove v heap_vars_of_tid in + let new_fst_state = ThreadsToHeapVarsMap.add tid heap_vars_of_tid_without_v (fst state) in + (new_fst_state, snd state) + | _ -> state + end | _ -> state end | _ -> state end | Abort -> - (* Upon a call to the "Abort" special function, we give up and conservatively warn *) + check_for_mem_leak ctx; + (* Upon a call to the "Abort" special function in the multi-threaded case, we give up and conservatively warn *) warn_for_multi_threaded_due_to_abort ctx; state | Assert { exp; _ } -> @@ -131,7 +123,8 @@ struct state | ThreadExit _ -> begin match ctx.ask (Queries.CurrentThreadId) with - | `Lifted tid -> warn_for_thread_return_or_exit tid ctx false + | `Lifted tid -> + warn_for_thread_return_or_exit tid ctx false | _ -> () end; state From 6cc01b5177b6bc31899c290b6ae65660bf4aa805 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 18 Nov 2023 15:22:47 +0100 Subject: [PATCH 34/66] Use `unrollType` and `GVarDecl` for global vars Also use `Queries.AD.fold` where applicable and prepend to accumulators --- src/analyses/memLeak.ml | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 51a5a2ff75..c09db2d44f 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -21,15 +21,20 @@ struct (* HELPER FUNCTIONS *) let get_global_vars () = - (* Filtering by GVar seems to account for declarations, as well as definitions of global vars *) - List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + List.filter_map (function GVar (v, _, _) | GVarDecl (v, _) -> Some v | _ -> None) !Cilfacade.current_file.globals let get_global_struct_ptr_vars () = - List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals - |> List.filter (fun v -> match v.vtype with TPtr (TComp _, _) | TPtr ((TNamed ({ttype = TComp _; _}, _)), _) -> true | _ -> false) + get_global_vars () + |> List.filter (fun v -> + match unrollType v.vtype with + | TPtr (TComp _, _) + | TPtr ((TNamed ({ttype = TComp _; _}, _)), _) -> true + | TComp (_, _) + | (TNamed ({ttype = TComp _; _}, _)) -> false + | _ -> false) let get_global_struct_non_ptr_vars () = - List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + get_global_vars () |> List.filter (fun v -> match v.vtype with TComp (_, _) | (TNamed ({ttype = TComp _; _}, _)) -> true | _ -> false) let get_reachable_mem_from_globals (global_vars:varinfo list) ctx = @@ -55,12 +60,13 @@ struct begin match ValueDomain.Structs.get s f with | Queries.VD.Address a -> let reachable_from_addr_set = - List.fold_left (fun acc addr -> + Queries.AD.fold (fun addr acc -> match addr with - | Queries.AD.Addr.Addr (v, _) -> List.append acc (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) + | Queries.AD.Addr.Addr (v, _) -> (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) @ acc | _ -> acc - ) [] (Queries.AD.elements a) - in List.append acc reachable_from_addr_set + ) a [] + in + reachable_from_addr_set @ acc | _ -> acc end else acc @@ -109,14 +115,14 @@ struct let reachable_from_addr_set = List.fold_left (fun acc_addr addr -> match addr with - | Queries.AD.Addr.Addr (v, _) -> List.append acc_addr (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) + | Queries.AD.Addr.Addr (v, _) -> (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) @ acc_addr | _ -> acc_addr ) [] (Queries.AD.elements a) - in List.append acc_field reachable_from_addr_set + in reachable_from_addr_set @ acc_field | _ -> acc_field ) [] fields in - List.append acc_struct reachable_from_fields + reachable_from_fields @ acc_struct ) [] let warn_for_multi_threaded ctx = From 80492ccd1dcad21e49a949a989d1cee42bbb6585 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 18 Nov 2023 15:26:40 +0100 Subject: [PATCH 35/66] Check that addresses in struct fields are singletons and not top --- src/analyses/memLeak.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index c09db2d44f..7e77d62a4e 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -58,7 +58,7 @@ struct List.fold_left (fun acc f -> if isPointerType f.ftype then begin match ValueDomain.Structs.get s f with - | Queries.VD.Address a -> + | Queries.VD.Address a when not (Queries.AD.is_top a) && Queries.AD.cardinal a = 1 -> let reachable_from_addr_set = Queries.AD.fold (fun addr acc -> match addr with From 720cfeebd1987bda44e4b7f4a2d545be6530025d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 19 Nov 2023 17:32:05 +0100 Subject: [PATCH 36/66] IsMallocCalled should be `may` --- src/analyses/memLeak.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 64fe7ab957..336943d407 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -7,7 +7,7 @@ open AnalysisStateUtil module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) module ThreadsToHeapVarsMap = MapDomain.MapBot(ThreadIdDomain.Thread)(ToppedVarInfoSet) -module WasMallocCalled = BoolDomain.MustBool +module WasMallocCalled = BoolDomain.MayBool module Spec : Analyses.MCPSpec = struct include Analyses.IdentitySpec From f2ca6d146e1271709259be24d5b20f9e61aab7dd Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 19 Nov 2023 17:33:24 +0100 Subject: [PATCH 37/66] Use `unrollType` for non-pointer global struct vars --- src/analyses/memLeak.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 7e77d62a4e..ab25d49cc6 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -35,7 +35,11 @@ struct let get_global_struct_non_ptr_vars () = get_global_vars () - |> List.filter (fun v -> match v.vtype with TComp (_, _) | (TNamed ({ttype = TComp _; _}, _)) -> true | _ -> false) + |> List.filter (fun v -> + match unrollType v.vtype with + | TComp (_, _) + | (TNamed ({ttype = TComp _; _}, _)) -> true + | _ -> false) let get_reachable_mem_from_globals (global_vars:varinfo list) ctx = global_vars From 0e09d099d5facf7354014319805eb53e186119d2 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 19 Nov 2023 17:36:22 +0100 Subject: [PATCH 38/66] Don't forget to prepend to `acc` when collecting globally reachable mem --- src/analyses/memLeak.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index ab25d49cc6..3079faae1f 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -91,8 +91,8 @@ struct in global_struct_ptr_vars |> List.fold_left (fun acc var -> - if ctx.ask (Queries.IsHeapVar var) then eval_value_of_heap_var var - else if not (ctx.ask (Queries.IsAllocVar var)) && isPointerType var.vtype then get_pts_of_non_heap_ptr_var var + if ctx.ask (Queries.IsHeapVar var) then (eval_value_of_heap_var var) @ acc + else if not (ctx.ask (Queries.IsAllocVar var)) && isPointerType var.vtype then (get_pts_of_non_heap_ptr_var var) @ acc else acc ) [] From af9ddc766c5b72e7bbd9d3177e1cd028e52cfc52 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 19 Nov 2023 17:36:26 +0100 Subject: [PATCH 39/66] Add unsound example --- tests/regression/76-memleak/10-leak-later.c | 25 +++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 tests/regression/76-memleak/10-leak-later.c diff --git a/tests/regression/76-memleak/10-leak-later.c b/tests/regression/76-memleak/10-leak-later.c new file mode 100644 index 0000000000..6e6e51bbdc --- /dev/null +++ b/tests/regression/76-memleak/10-leak-later.c @@ -0,0 +1,25 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include +#include + +int *g; +int *m1; +int *m2; + +void *f1(void *arg) { + int top; + + // Thread t1 leaks m0 here + exit(2); //WARN +} + +int main(int argc, char const *argv[]) { + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + + int* m0 = malloc(sizeof(int)); + free(m0); + + // main thread is not leaking anything + return 0; +} From ada84914a0da7614e023d6c0bf2ca86725d6551a Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 19 Nov 2023 18:14:50 +0100 Subject: [PATCH 40/66] Make sound by accounting for alloc in global invariant --- src/analyses/memLeak.ml | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index b1b57b6694..d2d3ce0d97 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -14,16 +14,19 @@ struct let name () = "memLeak" - module D = Lattice.Prod(ThreadsToHeapVarsMap)(WasMallocCalled) + module D = ThreadsToHeapVarsMap module C = D module P = IdentityP (D) + module V = UnitV + module G = WasMallocCalled + let context _ d = d (* HELPER FUNCTIONS *) let warn_for_multi_threaded_due_to_abort ctx = - let state = ctx.local in - if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) && snd state then ( + let malloc_called = ctx.global () in + if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) && malloc_called then ( set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program aborted while running in multi-threaded mode. A memory leak might occur" @@ -32,7 +35,7 @@ struct (* If [is_return] is set to [true], then a thread return occurred, else a thread exit *) let warn_for_thread_return_or_exit current_thread ctx is_return = let state = ctx.local in - let heap_vars_of_curr_tid = ThreadsToHeapVarsMap.find current_thread (fst state) in + let heap_vars_of_curr_tid = ThreadsToHeapVarsMap.find current_thread state in if not (ToppedVarInfoSet.is_empty heap_vars_of_curr_tid) then ( set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s for thread %a" (if is_return then "return" else "exit") ThreadIdDomain.Thread.pretty current_thread @@ -40,7 +43,7 @@ struct let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx = let state = ctx.local in - if not (ThreadsToHeapVarsMap.for_all (fun tid heap_vars -> ToppedVarInfoSet.is_empty heap_vars) (fst state)) then + if not (ThreadsToHeapVarsMap.for_all (fun tid heap_vars -> ToppedVarInfoSet.is_empty heap_vars) state) then match assert_exp_imprecise, exp with | true, Some exp -> set_mem_safety_flag InvalidMemTrack; @@ -71,14 +74,15 @@ struct | Malloc _ | Calloc _ | Realloc _ -> + ctx.sideg () true; begin match ctx.ask (Queries.AllocVar {on_stack = false}) with | `Lifted var -> begin match ctx.ask (Queries.CurrentThreadId) with | `Lifted tid -> - ((ThreadsToHeapVarsMap.add tid (ToppedVarInfoSet.singleton var) (fst state)), true) - | _ -> (fst state, true) + (ThreadsToHeapVarsMap.add tid (ToppedVarInfoSet.singleton var) state) + | _ -> state end - | _ -> (fst state, true) + | _ -> state end | Free ptr -> begin match ctx.ask (Queries.MayPointTo ptr) with @@ -90,10 +94,10 @@ struct | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> begin match ctx.ask (Queries.CurrentThreadId) with | `Lifted tid -> - let heap_vars_of_tid = ThreadsToHeapVarsMap.find tid (fst state) in + let heap_vars_of_tid = ThreadsToHeapVarsMap.find tid state in let heap_vars_of_tid_without_v = ToppedVarInfoSet.remove v heap_vars_of_tid in - let new_fst_state = ThreadsToHeapVarsMap.add tid heap_vars_of_tid_without_v (fst state) in - (new_fst_state, snd state) + let new_fst_state = ThreadsToHeapVarsMap.add tid heap_vars_of_tid_without_v state in + new_fst_state | _ -> state end | _ -> state From e7d630231d2bfce552cbb262bf3f8a4882ddd1ff Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 19 Nov 2023 18:49:03 +0100 Subject: [PATCH 41/66] Cleanup --- src/analyses/memLeak.ml | 53 +++++++------------ .../08-invalid-memcleanup-multi-threaded.c | 2 +- ...-invalid-memcleanup-multi-threaded-abort.c | 2 +- 3 files changed, 20 insertions(+), 37 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index d2d3ce0d97..0f16cec4ab 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -6,7 +6,6 @@ open MessageCategory open AnalysisStateUtil module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) -module ThreadsToHeapVarsMap = MapDomain.MapBot(ThreadIdDomain.Thread)(ToppedVarInfoSet) module WasMallocCalled = BoolDomain.MayBool module Spec : Analyses.MCPSpec = struct @@ -14,7 +13,7 @@ struct let name () = "memLeak" - module D = ThreadsToHeapVarsMap + module D = ToppedVarInfoSet module C = D module P = IdentityP (D) @@ -33,22 +32,20 @@ struct ) (* If [is_return] is set to [true], then a thread return occurred, else a thread exit *) - let warn_for_thread_return_or_exit current_thread ctx is_return = - let state = ctx.local in - let heap_vars_of_curr_tid = ThreadsToHeapVarsMap.find current_thread state in - if not (ToppedVarInfoSet.is_empty heap_vars_of_curr_tid) then ( + let warn_for_thread_return_or_exit ctx is_return = + if not (ToppedVarInfoSet.is_empty ctx.local) then ( set_mem_safety_flag InvalidMemcleanup; - M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s for thread %a" (if is_return then "return" else "exit") ThreadIdDomain.Thread.pretty current_thread + let current_thread = ctx.ask (Queries.CurrentThreadId) in + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s for thread %a" (if is_return then "return" else "exit") ThreadIdDomain.ThreadLifted.pretty current_thread ) let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx = - let state = ctx.local in - if not (ThreadsToHeapVarsMap.for_all (fun tid heap_vars -> ToppedVarInfoSet.is_empty heap_vars) state) then + if not (ToppedVarInfoSet.is_empty ctx.local) then match assert_exp_imprecise, exp with | true, Some exp -> set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; - M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty state + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty ctx.local | _ -> set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; @@ -58,10 +55,7 @@ struct let return ctx (exp:exp option) (f:fundec) : D.t = (* Check for a valid-memcleanup violation in a multi-threaded setting *) if (ctx.ask (Queries.MayBeThreadReturn)) then ( - match ctx.ask (Queries.CurrentThreadId) with - | `Lifted tid -> - warn_for_thread_return_or_exit tid ctx true - | _ -> () + warn_for_thread_return_or_exit ctx true ); (* Returning from "main" is one possible program exit => need to check for memory leaks *) if f.svar.vname = "main" then check_for_mem_leak ctx; @@ -74,35 +68,22 @@ struct | Malloc _ | Calloc _ | Realloc _ -> - ctx.sideg () true; + (ctx.sideg () true; begin match ctx.ask (Queries.AllocVar {on_stack = false}) with | `Lifted var -> - begin match ctx.ask (Queries.CurrentThreadId) with - | `Lifted tid -> - (ThreadsToHeapVarsMap.add tid (ToppedVarInfoSet.singleton var) state) - | _ -> state - end + ToppedVarInfoSet.add var state | _ -> state - end + end) | Free ptr -> begin match ctx.ask (Queries.MayPointTo ptr) with - (* TODO: The cardinality of 1 seems to lead to the situation where only free() calls in main() are detected here (affects 76/08 and 76/09) *) - (* | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 -> *) - | ad when not (Queries.AD.is_top ad) -> + | ad when (not (Queries.AD.is_top ad)) && Queries.AD.cardinal ad = 1 -> (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *) begin match Queries.AD.choose ad with | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> - begin match ctx.ask (Queries.CurrentThreadId) with - | `Lifted tid -> - let heap_vars_of_tid = ThreadsToHeapVarsMap.find tid state in - let heap_vars_of_tid_without_v = ToppedVarInfoSet.remove v heap_vars_of_tid in - let new_fst_state = ThreadsToHeapVarsMap.add tid heap_vars_of_tid_without_v state in - new_fst_state - | _ -> state - end - | _ -> state + ToppedVarInfoSet.remove v ctx.local + | _ -> ctx.local end - | _ -> state + | _ -> ctx.local end | Abort -> check_for_mem_leak ctx; @@ -128,7 +109,7 @@ struct | ThreadExit _ -> begin match ctx.ask (Queries.CurrentThreadId) with | `Lifted tid -> - warn_for_thread_return_or_exit tid ctx false + warn_for_thread_return_or_exit ctx false | _ -> () end; state @@ -136,6 +117,8 @@ struct let startstate v = D.bot () let exitstate v = D.top () + + let threadenter ctx ~multiple lval f args = [D.bot ()] end let _ = diff --git a/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c b/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c index 50b17fa65d..513a36db95 100644 --- a/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c +++ b/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c @@ -4,7 +4,6 @@ int *g; int *m1; -int *m2; void *f1(void *arg) { m1 = malloc(sizeof(int)); @@ -13,6 +12,7 @@ void *f1(void *arg) { } void *f2(void *arg) { + int *m2; m2 = malloc(sizeof(int)); free(m2); // No leak for thread t2, since it calls free before exiting pthread_exit(NULL); //NOWARN diff --git a/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c b/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c index 9aef45198e..977510b9bb 100644 --- a/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c +++ b/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c @@ -4,7 +4,6 @@ int *g; int *m1; -int *m2; void *f1(void *arg) { m1 = malloc(sizeof(int)); @@ -13,6 +12,7 @@ void *f1(void *arg) { } void *f2(void *arg) { + int *m2; m2 = malloc(sizeof(int)); free(m2); // No leak for thread t2, since it calls free before exiting pthread_exit(NULL); //NOWARN From e6cee270129731e462b31a0a75cb360d02b784c6 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 19 Nov 2023 19:01:11 +0100 Subject: [PATCH 42/66] Fix `memtrack` for multi-threaded case --- src/analyses/memLeak.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 0f16cec4ab..8a067cc80d 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -34,6 +34,7 @@ struct (* If [is_return] is set to [true], then a thread return occurred, else a thread exit *) let warn_for_thread_return_or_exit ctx is_return = if not (ToppedVarInfoSet.is_empty ctx.local) then ( + set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; let current_thread = ctx.ask (Queries.CurrentThreadId) in M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s for thread %a" (if is_return then "return" else "exit") ThreadIdDomain.ThreadLifted.pretty current_thread @@ -53,8 +54,9 @@ struct (* TRANSFER FUNCTIONS *) let return ctx (exp:exp option) (f:fundec) : D.t = - (* Check for a valid-memcleanup violation in a multi-threaded setting *) - if (ctx.ask (Queries.MayBeThreadReturn)) then ( + (* Check for a valid-memcleanup and memtrack violation in a multi-threaded setting *) + (* The check for multi-threadedness is to ensure that valid-memtrack and valid-memclenaup are treated separately for single-threaded programs *) + if (ctx.ask (Queries.MayBeThreadReturn) && not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true }))) then ( warn_for_thread_return_or_exit ctx true ); (* Returning from "main" is one possible program exit => need to check for memory leaks *) From 97eb7156d4a71fce2e84153b1a11906db5e9f2de Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 19 Nov 2023 19:23:20 +0100 Subject: [PATCH 43/66] Account for failing assertions in the multi-threaded case as well --- src/analyses/memLeak.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 8a067cc80d..8d83bcee83 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -98,12 +98,16 @@ struct | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp | a -> begin match Queries.ID.to_bool a with - | Some b -> + | Some b -> ( (* If we know for sure that the expression in "assert" is false => need to check for memory leaks *) - if b = false then - check_for_mem_leak ctx - else () - | None -> check_for_mem_leak ctx ~assert_exp_imprecise:true ~exp:(Some exp) + if b = false then ( + warn_for_multi_threaded_due_to_abort ctx; + check_for_mem_leak ctx + ) + else ()) + | None -> + (warn_for_multi_threaded_due_to_abort ctx; + check_for_mem_leak ctx ~assert_exp_imprecise:true ~exp:(Some exp)) end in warn_for_assert_exp; From 987795ec92c6e03fc9b0b659dbc396b73df41098 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 19 Nov 2023 19:26:39 +0100 Subject: [PATCH 44/66] Add a few more test cases --- .../76-memleak/11-leak-later-nested.c | 34 +++++++++++++++++++ .../76-memleak/12-multi-threaded-assert.c | 34 +++++++++++++++++++ .../13-assert-unknown-multi-threaded.c | 20 +++++++++++ 3 files changed, 88 insertions(+) create mode 100644 tests/regression/76-memleak/11-leak-later-nested.c create mode 100644 tests/regression/76-memleak/12-multi-threaded-assert.c create mode 100644 tests/regression/76-memleak/13-assert-unknown-multi-threaded.c diff --git a/tests/regression/76-memleak/11-leak-later-nested.c b/tests/regression/76-memleak/11-leak-later-nested.c new file mode 100644 index 0000000000..952dc66334 --- /dev/null +++ b/tests/regression/76-memleak/11-leak-later-nested.c @@ -0,0 +1,34 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include +#include + +int *g; +int *m1; +int *m2; + +void *f2(void *arg) { + // Thread t2 leaks m0 and t1_ptr here + quick_exit(2); //WARN +} + +void *f1(void *arg) { + pthread_t t2; + pthread_create(&t2, NULL, f2, NULL); + + int *t1_ptr = malloc(sizeof(int)); + + pthread_join(t2, NULL); + // t1_ptr is leaked, since t2 calls quick_exit() potentially before this program point + free(t1_ptr); +} + +int main(int argc, char const *argv[]) { + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + + int* m0 = malloc(sizeof(int)); + free(m0); + + // main thread is not leaking anything + return 0; +} diff --git a/tests/regression/76-memleak/12-multi-threaded-assert.c b/tests/regression/76-memleak/12-multi-threaded-assert.c new file mode 100644 index 0000000000..309a5dde75 --- /dev/null +++ b/tests/regression/76-memleak/12-multi-threaded-assert.c @@ -0,0 +1,34 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --disable warn.assert +#include +#include +#include + +int *g; +int *m1; +int *m2; + +void *f2(void *arg) { + // Thread t2 leaks m0 and t1_ptr here + assert(0); //WARN +} + +void *f1(void *arg) { + pthread_t t2; + pthread_create(&t2, NULL, f2, NULL); + + int *t1_ptr = malloc(sizeof(int)); + assert(1); //NOWARN + pthread_join(t2, NULL); + free(t1_ptr); +} + +int main(int argc, char const *argv[]) { + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + + int* m0 = malloc(sizeof(int)); + free(m0); + + // main thread is not leaking anything + return 0; +} diff --git a/tests/regression/76-memleak/13-assert-unknown-multi-threaded.c b/tests/regression/76-memleak/13-assert-unknown-multi-threaded.c new file mode 100644 index 0000000000..95eb291887 --- /dev/null +++ b/tests/regression/76-memleak/13-assert-unknown-multi-threaded.c @@ -0,0 +1,20 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --disable warn.assert +#include +#include +#include + +void *f1(void *arg) { + int top; + assert(top); //WARN +} + +int main(int argc, char const *argv[]) { + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + + int* m0 = malloc(sizeof(int)); + free(m0); + + // main thread is not leaking anything + return 0; +} From 8d55024d0580b5a4aec7bd32103d0b3f0ab84d72 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 19 Nov 2023 19:45:27 +0100 Subject: [PATCH 45/66] Add options to produce warnings only for memory leaks due to `memcleanup` or `memtrack` violations --- src/common/util/options.schema.json | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 9a6a66ee6b..5923612b5b 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -2164,6 +2164,25 @@ "description": "Output messages in deterministic order. Useful for cram testing.", "type": "boolean", "default": false + }, + "memleak": { + "title": "warn.memleak", + "type":"object", + "properties": { + "memcleanup": { + "title": "warn.memleak.memcleanup", + "description": "Enable memory leak warnings only for violations of the SV-COMP \"valid-memcleanup\" category", + "type": "boolean", + "default": false + }, + "memtrack": { + "title": "warn.memleak.memtrack", + "description": "Enable memory leak warnings only for violations of the SV-COMP \"valid-memtrack\" category", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false } }, "additionalProperties": false From ecd48aa318c0720c2f2b8b63a524635170df804e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 20 Nov 2023 10:46:35 +0200 Subject: [PATCH 46/66] Make SV-COMP validation strict --- conf/svcomp24-validate.json | 1 + src/common/util/options.schema.json | 6 ++++++ src/witness/witness.ml | 13 ++++++++++--- 3 files changed, 17 insertions(+), 3 deletions(-) diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json index ce11af12f6..2d7e988fdf 100644 --- a/conf/svcomp24-validate.json +++ b/conf/svcomp24-validate.json @@ -114,6 +114,7 @@ }, "yaml": { "enabled": false, + "strict": true, "format-version": "2.0", "entry-types": [ "location_invariant", diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 328b4f277f..0732debcc9 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -2487,6 +2487,12 @@ "type": "string", "default": "" }, + "strict": { + "title": "witness.yaml.strict", + "description": "", + "type": "boolean", + "default": false + }, "unassume": { "title": "witness.yaml.unassume", "description": "YAML witness input path", diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 235461c348..9d6a1ebe02 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -665,11 +665,18 @@ struct | Some false -> print_svcomp_result "ERROR (verify)" | _ -> if get_string "witness.yaml.validate" <> "" then ( - if !YamlWitness.cnt_refuted > 0 then + match get_bool "witness.yaml.strict" with + | true when !YamlWitness.cnt_error > 0 -> + print_svcomp_result "ERROR (witness error)" + | true when !YamlWitness.cnt_unsupported > 0 -> + print_svcomp_result "ERROR (witness unsupported)" + | true when !YamlWitness.cnt_disabled > 0 -> + print_svcomp_result "ERROR (witness disabled)" + | _ when !YamlWitness.cnt_refuted > 0 -> print_svcomp_result (Result.to_string (False None)) - else if !YamlWitness.cnt_unconfirmed > 0 then + | _ when !YamlWitness.cnt_unconfirmed > 0 -> print_svcomp_result (Result.to_string Unknown) - else + | _ -> write entrystates ) else From 6797cbb9ec941646316ffb689a12135bf1282b6a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 20 Nov 2023 12:21:32 +0200 Subject: [PATCH 47/66] Add ana.autotune.activated schema --- src/common/util/options.schema.json | 32 +++++++++++++++++++++++++++-- 1 file changed, 30 insertions(+), 2 deletions(-) diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index 745aecfb57..2b1e738196 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -542,9 +542,37 @@ "title": "ana.autotune.activated", "description": "Lists of activated tuning options.", "type": "array", - "items": { "type": "string" }, + "items": { + "type": "string", + "enum": [ + "congruence", + "singleThreaded", + "specification", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "loopUnrollHeuristic", + "forceLoopUnrollForFewLoops", + "arrayDomain", + "octagon", + "wideningThresholds", + "memsafetySpecification", + "termination" + ] + }, "default": [ - "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds", "memsafetySpecification" + "congruence", + "singleThreaded", + "specification", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "loopUnrollHeuristic", + "arrayDomain", + "octagon", + "wideningThresholds", + "memsafetySpecification", + "termination" ] } }, From 3af192da0600613de1f789e827d98b87d13c41ef Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 20 Nov 2023 13:10:40 +0200 Subject: [PATCH 48/66] Deactivate mhp and region for single-threaded programs --- src/autoTune.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 346e9d7b6f..d9a866ffc2 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -184,7 +184,7 @@ let enableAnalyses anas = (*escape is also still enabled, because otherwise we get a warning*) (*does not consider dynamic calls!*) -let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"] +let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"] let reduceThreadAnalyses () = let isThreadCreate = function | LibraryDesc.ThreadCreate _ -> true From 0ee71a02f9fe08381c94eb6704bbc42055a778fa Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 20 Nov 2023 13:48:28 +0200 Subject: [PATCH 49/66] Update SV-COMP releasing guide for 2024 --- docs/developer-guide/releasing.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md index 69ffcb2461..fc5f5f68a1 100644 --- a/docs/developer-guide/releasing.md +++ b/docs/developer-guide/releasing.md @@ -97,16 +97,17 @@ This ensures that the environment and the archive have all the correct system libraries. -6. Commit and push the archive to an SV-COMP archives repository branch (but don't open a MR yet): (SV-COMP 2023). -7. Check pushed archive via CoveriTeam-Remote: . +6. Create (or add new version) Zenodo artifact and upload the archive. - 1. Clone coveriteam repository. - 2. Locally modify `actors/goblint.yml` archive location to the raw URL of the pushed archive. - 3. Run Goblint on some sv-benchmarks and properties via CoveriTeam. +7. Open MR with Zenodo version DOI to the [fm-tools](https://gitlab.com/sosy-lab/benchmarking/fm-tools) repository. - This ensures that Goblint runs on SoSy-Lab servers. + ### After all preruns From 8b7994869c98119e50e8d19f857baccad7194628 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 21 Nov 2023 11:21:46 +0200 Subject: [PATCH 50/66] Fix invariant_set elements schema in YAML witnesses --- src/witness/yamlWitnessType.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index f9bcf3235f..de9fa151d8 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -311,13 +311,16 @@ struct } let to_yaml {invariant_type} = - `O ([ - ("type", `String (InvariantType.invariant_type invariant_type)); - ] @ InvariantType.to_yaml' invariant_type) + `O [ + ("invariant", `O ([ + ("type", `String (InvariantType.invariant_type invariant_type)); + ] @ InvariantType.to_yaml' invariant_type) + ) + ] let of_yaml y = let open GobYaml in - let+ invariant_type = y |> InvariantType.of_yaml in + let+ invariant_type = y |> find "invariant" >>= InvariantType.of_yaml in {invariant_type} end From ca61360dd19e18bba2ddeba89c3f4046cf4764ad Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 21 Nov 2023 10:21:49 +0100 Subject: [PATCH 51/66] Add example where better privatization helps --- ...alid-memcleanup-multi-threaded-betterpiv.c | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c diff --git a/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c b/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c new file mode 100644 index 0000000000..c701461cb5 --- /dev/null +++ b/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c @@ -0,0 +1,33 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.base.privatization mutex-meet-tid --set ana.path_sens[+] threadflag +#include +#include + +int *g; +int *m1; +int *m2; + +void *f1(void *arg) { + m1 = malloc(sizeof(int)); + // Thread t1 leaks m1 here + pthread_exit(NULL); //WARN +} + +void *f2(void *arg) { + m2 = malloc(sizeof(int)); + free(m2); // No leak for thread t2, since it calls free before exiting + pthread_exit(NULL); //NOWARN +} + +int main(int argc, char const *argv[]) { + g = malloc(sizeof(int)); + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + + pthread_t t2; + pthread_create(&t2, NULL, f2, NULL); + + free(g); + + // main thread is not leaking anything + return 0; //NOWARN +} From 2cc915fe1757fcd032d17b8c017f052729430d21 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 21 Nov 2023 17:16:47 +0100 Subject: [PATCH 52/66] Check at end of main thread that the program is certainly single-threaded. If other threads are not joined, they may be killed by the main thread returning. This will possibly leak memory. --- src/analyses/memLeak.ml | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 8d83bcee83..4d37992a21 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -22,10 +22,16 @@ struct let context _ d = d + let must_be_single_threaded ~since_start ctx = + ctx.ask (Queries.MustBeSingleThreaded { since_start }) + + let was_malloc_called ctx = + ctx.global () + (* HELPER FUNCTIONS *) let warn_for_multi_threaded_due_to_abort ctx = - let malloc_called = ctx.global () in - if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) && malloc_called then ( + let malloc_called = was_malloc_called ctx in + if not (must_be_single_threaded ctx ~since_start:true) && malloc_called then ( set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program aborted while running in multi-threaded mode. A memory leak might occur" @@ -56,11 +62,18 @@ struct let return ctx (exp:exp option) (f:fundec) : D.t = (* Check for a valid-memcleanup and memtrack violation in a multi-threaded setting *) (* The check for multi-threadedness is to ensure that valid-memtrack and valid-memclenaup are treated separately for single-threaded programs *) - if (ctx.ask (Queries.MayBeThreadReturn) && not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true }))) then ( - warn_for_thread_return_or_exit ctx true + if (ctx.ask (Queries.MayBeThreadReturn) && not (must_be_single_threaded ctx ~since_start:true)) then ( + warn_for_thread_return_or_exit ctx true ); (* Returning from "main" is one possible program exit => need to check for memory leaks *) - if f.svar.vname = "main" then check_for_mem_leak ctx; + if f.svar.vname = "main" then ( + check_for_mem_leak ctx; + if not (must_be_single_threaded ctx ~since_start:false) && was_malloc_called ctx then begin + set_mem_safety_flag InvalidMemTrack; + set_mem_safety_flag InvalidMemcleanup; + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Possible memory leak: Memory was allocated in a multithreaded program, but not all threads are joined." + end + ); ctx.local let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = From 45ec8a663791d3675ca05ac68355ce1b1ea2c8c1 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 21 Nov 2023 17:18:30 +0100 Subject: [PATCH 53/66] Add test case for memory leaking from a thead that is not joined, add thread_joins to other test cases. --- .../08-invalid-memcleanup-multi-threaded.c | 6 +++++- ...9-invalid-memcleanup-multi-threaded-abort.c | 7 +++++-- ...valid-memcleanup-multi-threaded-betterpiv.c | 5 ++++- .../76-memleak/15-mem-leak-not-joined-thread.c | 18 ++++++++++++++++++ 4 files changed, 32 insertions(+), 4 deletions(-) create mode 100644 tests/regression/76-memleak/15-mem-leak-not-joined-thread.c diff --git a/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c b/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c index 513a36db95..65e6e4e766 100644 --- a/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c +++ b/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread --set ana.activated[+] threadid #include #include @@ -7,6 +7,7 @@ int *m1; void *f1(void *arg) { m1 = malloc(sizeof(int)); + free(m1); // Thread t1 leaks m1 here pthread_exit(NULL); //WARN } @@ -28,6 +29,9 @@ int main(int argc, char const *argv[]) { free(g); + pthread_join(t1, NULL); + pthread_join(t2, NULL); + // main thread is not leaking anything return 0; //NOWARN } diff --git a/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c b/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c index 977510b9bb..b991433f4d 100644 --- a/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c +++ b/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread --set ana.activated[+] threadid #include #include @@ -25,9 +25,12 @@ int main(int argc, char const *argv[]) { pthread_t t2; pthread_create(&t2, NULL, f2, NULL); - + free(g); + pthread_join(t1, NULL); + pthread_join(t2, NULL); + // main thread is not leaking anything return 0; //NOWARN } diff --git a/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c b/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c index c701461cb5..7ad9194d6e 100644 --- a/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c +++ b/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.base.privatization mutex-meet-tid --set ana.path_sens[+] threadflag +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.base.privatization mutex-meet-tid --set ana.path_sens[+] threadflag --set ana.activated[+] thread --set ana.activated[+] threadid #include #include @@ -28,6 +28,9 @@ int main(int argc, char const *argv[]) { free(g); + pthread_join(t1, NULL); + pthread_join(t2, NULL); + // main thread is not leaking anything return 0; //NOWARN } diff --git a/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c b/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c new file mode 100644 index 0000000000..c60809a9f4 --- /dev/null +++ b/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c @@ -0,0 +1,18 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread --set ana.activated[+] threadid +#include +#include + +int *m1; + +void *f1(void *arg) { + m1 = malloc(sizeof(int)); + while (1); +} + +int main(int argc, char const *argv[]) { + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + + // memory from thread f1 which was not joined into main, is not freed + return 0; //WARN +} \ No newline at end of file From 56c4d620be0c7e3a3d2deb92197d3d161a850445 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 21 Nov 2023 17:40:44 +0100 Subject: [PATCH 54/66] Add test case with pthread_exit called in main, remove threadid analysis from params as it is not needed. --- .../08-invalid-memcleanup-multi-threaded.c | 4 ++-- ...-invalid-memcleanup-multi-threaded-abort.c | 3 +-- ...alid-memcleanup-multi-threaded-betterpiv.c | 2 +- .../15-mem-leak-not-joined-thread.c | 2 +- .../16-no-mem-leak-thread-exit-main.c | 23 +++++++++++++++++++ 5 files changed, 28 insertions(+), 6 deletions(-) create mode 100644 tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c diff --git a/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c b/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c index 65e6e4e766..89dc7a3416 100644 --- a/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c +++ b/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread --set ana.activated[+] threadid +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread #include #include @@ -26,7 +26,7 @@ int main(int argc, char const *argv[]) { pthread_t t2; pthread_create(&t2, NULL, f2, NULL); - + free(g); pthread_join(t1, NULL); diff --git a/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c b/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c index b991433f4d..eaba1e91b5 100644 --- a/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c +++ b/tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c @@ -1,5 +1,4 @@ -//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread --set ana.activated[+] threadid -#include +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread #include int *g; diff --git a/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c b/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c index 7ad9194d6e..9f636ab587 100644 --- a/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c +++ b/tests/regression/76-memleak/14-invalid-memcleanup-multi-threaded-betterpiv.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.base.privatization mutex-meet-tid --set ana.path_sens[+] threadflag --set ana.activated[+] thread --set ana.activated[+] threadid +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.base.privatization mutex-meet-tid --set ana.path_sens[+] threadflag --set ana.activated[+] thread #include #include diff --git a/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c b/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c index c60809a9f4..21c1992fc3 100644 --- a/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c +++ b/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread --set ana.activated[+] threadid +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread #include #include diff --git a/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c b/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c new file mode 100644 index 0000000000..5fb89113d2 --- /dev/null +++ b/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c @@ -0,0 +1,23 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread +#include +#include + +int *m1; + +void *f1(void *arg) { + m1 = malloc(sizeof(int)); + while (1); +} + +int main(int argc, char const *argv[]) { + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + + pthread_exit(NULL); + + pthread_join(t1, NULL); + + // A pthread_join called in main will wait for other threads to finish + // Therefore, no memory leak here + return 0; // NOWARN +} \ No newline at end of file From 2fef812ff9a11bebb6ac4b78ca010fde6bbfeea9 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 21 Nov 2023 17:57:07 +0100 Subject: [PATCH 55/66] Add testcases for thread return and pthread_exit in thread different from main. --- .../15-mem-leak-not-joined-thread.c | 1 + .../16-no-mem-leak-thread-exit-main.c | 3 +-- .../76-memleak/17-mem-leak-thread-return.c | 26 ++++++++++++++++++ .../76-memleak/18-mem-leak-thread-exit.c | 27 +++++++++++++++++++ 4 files changed, 55 insertions(+), 2 deletions(-) create mode 100644 tests/regression/76-memleak/17-mem-leak-thread-return.c create mode 100644 tests/regression/76-memleak/18-mem-leak-thread-exit.c diff --git a/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c b/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c index 21c1992fc3..15f249ffe1 100644 --- a/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c +++ b/tests/regression/76-memleak/15-mem-leak-not-joined-thread.c @@ -7,6 +7,7 @@ int *m1; void *f1(void *arg) { m1 = malloc(sizeof(int)); while (1); + return NULL; } int main(int argc, char const *argv[]) { diff --git a/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c b/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c index 5fb89113d2..663ea26663 100644 --- a/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c +++ b/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c @@ -7,6 +7,7 @@ int *m1; void *f1(void *arg) { m1 = malloc(sizeof(int)); while (1); + return NULL; } int main(int argc, char const *argv[]) { @@ -15,8 +16,6 @@ int main(int argc, char const *argv[]) { pthread_exit(NULL); - pthread_join(t1, NULL); - // A pthread_join called in main will wait for other threads to finish // Therefore, no memory leak here return 0; // NOWARN diff --git a/tests/regression/76-memleak/17-mem-leak-thread-return.c b/tests/regression/76-memleak/17-mem-leak-thread-return.c new file mode 100644 index 0000000000..bec64ca22f --- /dev/null +++ b/tests/regression/76-memleak/17-mem-leak-thread-return.c @@ -0,0 +1,26 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread +#include +#include + +int *m1; + +void *f2(void *arg) { + m1 = malloc(sizeof(int)); + while (1); + return NULL; +} + +void *f1(void *arg) { + pthread_t t2; + pthread_create(&t2, NULL, f2, NULL); + + return NULL; +} + +int main(int argc, char const *argv[]) { + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + pthread_join(t1, NULL); + + return 0; // WARN +} \ No newline at end of file diff --git a/tests/regression/76-memleak/18-mem-leak-thread-exit.c b/tests/regression/76-memleak/18-mem-leak-thread-exit.c new file mode 100644 index 0000000000..e98ae3f346 --- /dev/null +++ b/tests/regression/76-memleak/18-mem-leak-thread-exit.c @@ -0,0 +1,27 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread +#include +#include + +int *m1; + +void *f2(void *arg) { + m1 = malloc(sizeof(int)); + while (1); + return NULL; +} + +void *f1(void *arg) { + pthread_t t2; + pthread_create(&t2, NULL, f2, NULL); + + pthread_exit(NULL); + return NULL; +} + +int main(int argc, char const *argv[]) { + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + pthread_join(t1, NULL); + + return 0; // WARN +} \ No newline at end of file From 645b03cfa678acbf3fdc585d4ee0a7d71e8b9688 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 21 Nov 2023 20:31:00 +0100 Subject: [PATCH 56/66] ThreadAnalysis: Handle pthread_exit like return from thread. --- src/analyses/threadAnalysis.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml index 0264f4b700..d9140dbb37 100644 --- a/src/analyses/threadAnalysis.ml +++ b/src/analyses/threadAnalysis.ml @@ -22,7 +22,7 @@ struct module P = IdentityP (D) (* transfer functions *) - let return ctx (exp:exp option) (f:fundec) : D.t = + let return ctx (exp:exp option) _ : D.t = let tid = ThreadId.get_current (Analyses.ask_of_ctx ctx) in begin match tid with | `Lifted tid -> ctx.sideg tid (false, TS.bot (), not (D.is_empty ctx.local)) @@ -64,6 +64,8 @@ struct | [t] -> join_thread ctx.local t (* single thread *) | _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *) | exception SetDomain.Unsupported _ -> ctx.local) + | ThreadExit { ret_val } -> + return ctx (Some ret_val) () | _ -> ctx.local let query ctx (type a) (q: a Queries.t): a Queries.result = From 9153eb3becd5904b99aa8250e50b2cd22f74a128 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Tue, 21 Nov 2023 21:04:04 +0100 Subject: [PATCH 57/66] Use `AD.fold` instead of `List.fold_left` --- src/analyses/memLeak.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 3079faae1f..f26157fdd0 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -117,12 +117,14 @@ struct match ValueDomain.Structs.get s field with | Queries.VD.Address a -> let reachable_from_addr_set = - List.fold_left (fun acc_addr addr -> + Queries.AD.fold (fun addr acc_addr -> match addr with - | Queries.AD.Addr.Addr (v, _) -> (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) @ acc_addr + | Queries.AD.Addr.Addr (v, _) -> + let reachable_from_v = Queries.AD.of_list (List.map (fun v -> Queries.AD.Addr.Addr (v, `NoOffset)) (get_reachable_mem_from_str_ptr_globals [v] ctx)) in + Queries.AD.join (Queries.AD.add addr reachable_from_v) acc_addr | _ -> acc_addr - ) [] (Queries.AD.elements a) - in reachable_from_addr_set @ acc_field + ) a (Queries.AD.empty ()) + in (Queries.AD.to_var_may reachable_from_addr_set) @ acc_field | _ -> acc_field ) [] fields in From c6cb63e48a665e566531213bbc02b4a568f2bf79 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 22 Nov 2023 10:53:22 +0100 Subject: [PATCH 58/66] Update tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c Co-authored-by: Simmo Saan --- tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c b/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c index 663ea26663..77dd299896 100644 --- a/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c +++ b/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c @@ -16,7 +16,7 @@ int main(int argc, char const *argv[]) { pthread_exit(NULL); - // A pthread_join called in main will wait for other threads to finish + // A pthread_exit called in main will wait for other threads to finish // Therefore, no memory leak here return 0; // NOWARN } \ No newline at end of file From f12a39216068c87cc0785f1ed13f9573b8f2c08e Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 22 Nov 2023 11:02:01 +0100 Subject: [PATCH 59/66] Remove call to free. --- .../regression/76-memleak/08-invalid-memcleanup-multi-threaded.c | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c b/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c index 89dc7a3416..038801f219 100644 --- a/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c +++ b/tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c @@ -7,7 +7,6 @@ int *m1; void *f1(void *arg) { m1 = malloc(sizeof(int)); - free(m1); // Thread t1 leaks m1 here pthread_exit(NULL); //WARN } From be9171b2bf6a541358c702a4a62e31a79f3be676 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 22 Nov 2023 11:04:44 +0100 Subject: [PATCH 60/66] Add annotation of nowarn next to pthread_exit. --- .../regression/76-memleak/16-no-mem-leak-thread-exit-main.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c b/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c index 77dd299896..f7340d1d4f 100644 --- a/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c +++ b/tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c @@ -14,9 +14,9 @@ int main(int argc, char const *argv[]) { pthread_t t1; pthread_create(&t1, NULL, f1, NULL); - pthread_exit(NULL); - // A pthread_exit called in main will wait for other threads to finish // Therefore, no memory leak here - return 0; // NOWARN + pthread_exit(NULL); // NOWARN + + return 0; // NOWARN (unreachable) } \ No newline at end of file From 585a65decbf38ddfdc66ce3c544547b47877b274 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 22 Nov 2023 11:13:04 +0100 Subject: [PATCH 61/66] Check in TheadAnalysis.return whether the return is actually a threadreturn before side-effecting. --- src/analyses/threadAnalysis.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml index d9140dbb37..01c5dd87fa 100644 --- a/src/analyses/threadAnalysis.ml +++ b/src/analyses/threadAnalysis.ml @@ -22,12 +22,15 @@ struct module P = IdentityP (D) (* transfer functions *) - let return ctx (exp:exp option) _ : D.t = + let handle_thread_return ctx (exp: exp option) = let tid = ThreadId.get_current (Analyses.ask_of_ctx ctx) in - begin match tid with + match tid with | `Lifted tid -> ctx.sideg tid (false, TS.bot (), not (D.is_empty ctx.local)) | _ -> () - end; + + let return ctx (exp:exp option) _ : D.t = + if ctx.ask Queries.MayBeThreadReturn then + handle_thread_return ctx exp; ctx.local let rec is_not_unique ctx tid = @@ -65,7 +68,8 @@ struct | _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *) | exception SetDomain.Unsupported _ -> ctx.local) | ThreadExit { ret_val } -> - return ctx (Some ret_val) () + handle_thread_return ctx (Some ret_val); + ctx.local | _ -> ctx.local let query ctx (type a) (q: a Queries.t): a Queries.result = From bc7694b68b599662a11cafc0c75c259cafa68a0d Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 22 Nov 2023 11:27:04 +0100 Subject: [PATCH 62/66] Add test case that checking that analysis distinguishes between thread returns and normal returns of a thread. --- .../76-memleak/19-no-mem-leak-return.c | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 tests/regression/76-memleak/19-no-mem-leak-return.c diff --git a/tests/regression/76-memleak/19-no-mem-leak-return.c b/tests/regression/76-memleak/19-no-mem-leak-return.c new file mode 100644 index 0000000000..70e0c66216 --- /dev/null +++ b/tests/regression/76-memleak/19-no-mem-leak-return.c @@ -0,0 +1,32 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread +#include +#include + + +void *f2(void *arg) { + int* m1 = malloc(sizeof(int)); + free(m1); + return NULL; +} + +// We check here that the analysis can distinguish between thread returns and normal returns + +void startf2(pthread_t* t){ + pthread_create(t, NULL, f2, NULL); + return; //NOWARN +} + +void *f1(void *arg) { + pthread_t t2; + startf2(&t2); + pthread_join(t2, NULL); + return NULL; // NOWARN +} + +int main(int argc, char const *argv[]) { + pthread_t t1; + pthread_create(&t1, NULL, f1, NULL); + pthread_join(t1, NULL); + + return 0; // NOWARN +} \ No newline at end of file From 666795faca6dd5a20e01c78daefde8efc7fbe1de Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 22 Nov 2023 11:50:31 +0100 Subject: [PATCH 63/66] MemLeak: Do not consider unions --- src/analyses/memLeak.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index f26157fdd0..c7a044f8a6 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -27,8 +27,8 @@ struct get_global_vars () |> List.filter (fun v -> match unrollType v.vtype with - | TPtr (TComp _, _) - | TPtr ((TNamed ({ttype = TComp _; _}, _)), _) -> true + | TPtr (TComp (ci,_), _) + | TPtr ((TNamed ({ttype = TComp (ci, _); _}, _)), _) -> ci.cstruct | TComp (_, _) | (TNamed ({ttype = TComp _; _}, _)) -> false | _ -> false) @@ -37,8 +37,8 @@ struct get_global_vars () |> List.filter (fun v -> match unrollType v.vtype with - | TComp (_, _) - | (TNamed ({ttype = TComp _; _}, _)) -> true + | TComp (ci, _) + | (TNamed ({ttype = TComp (ci,_); _}, _)) -> ci.cstruct | _ -> false) let get_reachable_mem_from_globals (global_vars:varinfo list) ctx = From dd45d1960a6e72083cc2c62f4c857aa24756cb2b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Nov 2023 13:48:28 +0200 Subject: [PATCH 64/66] Add initial CHANGELOG for SV-COMP 2024 --- CHANGELOG.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 97cc399133..ab9bb8fef2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,21 @@ +## v2.3.0 (unreleased) +Functionally equivalent to Goblint in SV-COMP 2024. + +### SV-COMP 2024 +* Add termination analysis (#1093). +* Add OOB analysis (#1094, #1197). +* Add memory leak analysis (???, #1246, #1241). +* Improve multi-threaded use-after-free analysis (#1123, ). +* Support MemSafety in SV-COMP (#1201, #1199, #1262). +* YAML witnesses in SV-COMP mode (#1217, #1226, #1225, #1248). +* YAML witness version 2.0 (#1238, #1240). +* SV-COMP multi-property (#1220, #1228). +* Adapt autotuning (#912, #921, #987, #1214, #1234, #1168). +* Support `alloca` (#1179). +* Fix old thread analysis soundness (#1223, #1230). +* Add library functions (#1242, #1244, #1254, #1239). +* Fix some region escape unsoundness (#1247). + ## v2.2.1 * Bump batteries lower bound to 3.5.0. * Fix flaky dead code elimination transformation test. From bf754c06f343cbde55c4bee6a60524840fe34161 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Nov 2023 13:56:56 +0200 Subject: [PATCH 65/66] Add initial CHANGELOG for v2.3.0 --- CHANGELOG.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ab9bb8fef2..c32bf566d2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,19 +1,24 @@ ## v2.3.0 (unreleased) Functionally equivalent to Goblint in SV-COMP 2024. +* Refactor/fix race analysis (#1170, #1198). +* Add library function (#1167, #1174, #1220, #1203, #1205, #1212). +* Refactor/fix `MayPointTo` and `ReachableFrom` queries (#1142, #1176, #1144). +* Add final messages about unsound results (#1190, #1191). + ### SV-COMP 2024 * Add termination analysis (#1093). * Add OOB analysis (#1094, #1197). * Add memory leak analysis (???, #1246, #1241). * Improve multi-threaded use-after-free analysis (#1123, ). -* Support MemSafety in SV-COMP (#1201, #1199, #1262). +* Support MemSafety in SV-COMP (#1201, #1199, #1259, #1262). * YAML witnesses in SV-COMP mode (#1217, #1226, #1225, #1248). * YAML witness version 2.0 (#1238, #1240). * SV-COMP multi-property (#1220, #1228). * Adapt autotuning (#912, #921, #987, #1214, #1234, #1168). * Support `alloca` (#1179). * Fix old thread analysis soundness (#1223, #1230). -* Add library functions (#1242, #1244, #1254, #1239). +* Add library functions (#1242, #1244, #1254, #1239, #1269). * Fix some region escape unsoundness (#1247). ## v2.2.1 From 9c650571f81b5c4d0b57a466b2adf935b90ddaa4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Nov 2023 14:30:14 +0200 Subject: [PATCH 66/66] Add CHANGELOG for v2.3.0 --- CHANGELOG.md | 27 ++++++++------------------- 1 file changed, 8 insertions(+), 19 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c32bf566d2..7300c09206 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,25 +1,14 @@ ## v2.3.0 (unreleased) Functionally equivalent to Goblint in SV-COMP 2024. -* Refactor/fix race analysis (#1170, #1198). -* Add library function (#1167, #1174, #1220, #1203, #1205, #1212). -* Refactor/fix `MayPointTo` and `ReachableFrom` queries (#1142, #1176, #1144). -* Add final messages about unsound results (#1190, #1191). - -### SV-COMP 2024 -* Add termination analysis (#1093). -* Add OOB analysis (#1094, #1197). -* Add memory leak analysis (???, #1246, #1241). -* Improve multi-threaded use-after-free analysis (#1123, ). -* Support MemSafety in SV-COMP (#1201, #1199, #1259, #1262). -* YAML witnesses in SV-COMP mode (#1217, #1226, #1225, #1248). -* YAML witness version 2.0 (#1238, #1240). -* SV-COMP multi-property (#1220, #1228). -* Adapt autotuning (#912, #921, #987, #1214, #1234, #1168). -* Support `alloca` (#1179). -* Fix old thread analysis soundness (#1223, #1230). -* Add library functions (#1242, #1244, #1254, #1239, #1269). -* Fix some region escape unsoundness (#1247). +* Add termination analysis for loops (#1093). +* Add memory out-of-bounds analysis (#1094, #1197). +* Add memory leak analysis (#1127, #1241, #1246). +* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (#1220, #1228, #1201, #1199, #1259, #1262). +* Add YAML witness version 2.0 support (#1238, #1240, #1217, #1226, #1225, #1248). +* Add final warnings about unsound results (#1190, #1191). +* Add many library function specifications (#1167, #1174, #1203, #1205, #1212, #1220, #1239, #1242, #1244, #1254, #1269). +* Adapt automatic configuration tuning (#912, #921, #987, #1168, #1214, #1234). ## v2.2.1 * Bump batteries lower bound to 3.5.0.