From 17ebe80cb217b8d6837f7b892fb75a3e11f0e3b0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 22 Nov 2023 09:29:30 +0100 Subject: [PATCH 1/5] Enable `mutex-meet-tid` for ValidDeref --- src/autoTune.ml | 6 +++++- .../74-invalid_deref/31-multithreaded.c | 21 +++++++++++++++++++ 2 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 tests/regression/74-invalid_deref/31-multithreaded.c diff --git a/src/autoTune.ml b/src/autoTune.ml index fefdeb32fd..dca3ee405a 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -222,7 +222,11 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) = print_endline "Setting \"cil.addNestedScopeAttr\" to true"; set_bool "cil.addNestedScopeAttr" true; print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\""; - enableAnalyses memOobAna + enableAnalyses memOobAna; + (* Set privatization to mutex-meet-tid *) + set_string "ana.base.privatization" "mutex-meet-tid"; + (* Required for mutex-meet-tid privatization *) + GobConfig.set_auto "ana.path_sens[+]" "threadflag"; | ValidMemtrack | ValidMemcleanup -> (* Enable the memLeak analysis *) let memLeakAna = ["memLeak"] in diff --git a/tests/regression/74-invalid_deref/31-multithreaded.c b/tests/regression/74-invalid_deref/31-multithreaded.c new file mode 100644 index 0000000000..e0dc146ba8 --- /dev/null +++ b/tests/regression/74-invalid_deref/31-multithreaded.c @@ -0,0 +1,21 @@ +//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins --set ana.path_sens[+] threadflag --set ana.activated[+] memOutOfBounds --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.privatization mutex-meet-tid +#include + +int data; +int *p = &data, *q; +pthread_mutex_t mutex; +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex); + *p = 8; + pthread_mutex_unlock(&mutex); + return ((void *)0); +} +int main() { + pthread_t id; + pthread_create(&id, ((void *)0), t_fun, ((void *)0)); + q = p; + pthread_mutex_lock(&mutex); + *q = 8; + pthread_mutex_unlock(&mutex); + return 0; +} From c5cda332088a48507f44b3c93733c13539189e04 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 22 Nov 2023 11:22:10 +0100 Subject: [PATCH 2/5] Move `AfterConfig.run` to after the autotuner --- src/analyses/base.ml | 8 +++++++- src/maingoblint.ml | 2 +- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 84be8c7a19..518d4d88c6 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1056,7 +1056,13 @@ struct ); (* Warn if any of the addresses contains a non-local and non-global variable *) if AD.exists (function - | AD.Addr.Addr (v, _) -> not (CPA.mem v st.cpa) && not (is_global a v) + | AD.Addr.Addr (v, _) -> + (M.tracel "wtf" "checking for %a\n" CilType.Varinfo.pretty v; + if v.vglob then + (* this is OK *) + false + else + (not (CPA.mem v st.cpa)) || WeakUpdates.mem v st.weak) | _ -> false ) adr then ( AnalysisStateUtil.set_mem_safety_flag InvalidDeref; diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 82a19aa4ae..79b0d121f6 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -191,10 +191,10 @@ let handle_flags () = let handle_options () = check_arguments (); - AfterConfig.run (); Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *) if AutoTune.isActivated "memsafetySpecification" && get_string "ana.specification" <> "" then AutoTune.focusOnMemSafetySpecification (); + AfterConfig.run (); Cilfacade.init_options (); handle_flags () From 8ae117253f84b9b419d52a318af06dc7e4518475 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 22 Nov 2023 11:53:08 +0100 Subject: [PATCH 3/5] Revert spurious changes to `base.ml` --- src/analyses/base.ml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 518d4d88c6..84be8c7a19 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1056,13 +1056,7 @@ struct ); (* Warn if any of the addresses contains a non-local and non-global variable *) if AD.exists (function - | AD.Addr.Addr (v, _) -> - (M.tracel "wtf" "checking for %a\n" CilType.Varinfo.pretty v; - if v.vglob then - (* this is OK *) - false - else - (not (CPA.mem v st.cpa)) || WeakUpdates.mem v st.weak) + | AD.Addr.Addr (v, _) -> not (CPA.mem v st.cpa) && not (is_global a v) | _ -> false ) adr then ( AnalysisStateUtil.set_mem_safety_flag InvalidDeref; From 06f543a0139b12366591f792642167e0e5ca2285 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 22 Nov 2023 13:21:19 +0100 Subject: [PATCH 4/5] Undo setting mutex-meet-tid privatization in autotuner --- src/autoTune.ml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index dca3ee405a..9627aed85f 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -223,10 +223,6 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) = set_bool "cil.addNestedScopeAttr" true; print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\""; enableAnalyses memOobAna; - (* Set privatization to mutex-meet-tid *) - set_string "ana.base.privatization" "mutex-meet-tid"; - (* Required for mutex-meet-tid privatization *) - GobConfig.set_auto "ana.path_sens[+]" "threadflag"; | ValidMemtrack | ValidMemcleanup -> (* Enable the memLeak analysis *) let memLeakAna = ["memLeak"] in From 209a5607204f960a0de6d6d7f81c754354306211 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 27 Nov 2023 15:18:49 +0100 Subject: [PATCH 5/5] Reduce activated analsyses and add test --- tests/regression/74-invalid_deref/31-multithreaded.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/74-invalid_deref/31-multithreaded.c b/tests/regression/74-invalid_deref/31-multithreaded.c index e0dc146ba8..8a0c12350b 100644 --- a/tests/regression/74-invalid_deref/31-multithreaded.c +++ b/tests/regression/74-invalid_deref/31-multithreaded.c @@ -1,4 +1,4 @@ -//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins --set ana.path_sens[+] threadflag --set ana.activated[+] memOutOfBounds --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.privatization mutex-meet-tid +//PARAM: --set ana.path_sens[+] threadflag --set ana.activated[+] memOutOfBounds --set ana.base.privatization mutex-meet-tid #include int data; @@ -15,7 +15,7 @@ int main() { pthread_create(&id, ((void *)0), t_fun, ((void *)0)); q = p; pthread_mutex_lock(&mutex); - *q = 8; + *q = 8; //NOWARN pthread_mutex_unlock(&mutex); return 0; }