From 2e915afaac498209620aee7fc0f5e547d2f7d300 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 13 Jun 2024 11:09:03 +0300 Subject: [PATCH 1/4] Enable pthreadMutexType analysis by default --- conf/examples/medium-program.json | 2 ++ conf/examples/very-precise.json | 2 ++ src/config/options.schema.json | 2 +- 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/conf/examples/medium-program.json b/conf/examples/medium-program.json index 2c1e7c7346..5afc1aa2f8 100644 --- a/conf/examples/medium-program.json +++ b/conf/examples/medium-program.json @@ -9,6 +9,7 @@ "base", "threadid", "threadflag", + "threadreturn", "mallocWrapper", "mutexEvents", "mutex", @@ -18,6 +19,7 @@ "expRelation", "mhp", "assert", + "pthreadMutexType", "var_eq", "symb_locks", "region", diff --git a/conf/examples/very-precise.json b/conf/examples/very-precise.json index 2197335eaf..074d448a85 100644 --- a/conf/examples/very-precise.json +++ b/conf/examples/very-precise.json @@ -22,6 +22,7 @@ "base", "threadid", "threadflag", + "threadreturn", "mallocWrapper", "mutexEvents", "mutex", @@ -31,6 +32,7 @@ "expRelation", "mhp", "assert", + "pthreadMutexType", "var_eq", "symb_locks", "region", diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 488fc494b0..7068cce719 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -344,7 +344,7 @@ "default": [ "expRelation", "base", "threadid", "threadflag", "threadreturn", "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp", - "assert" + "assert", "pthreadMutexType" ] }, "path_sens": { From 5962aedde36fa0caadaf77123ae6bf80b90ecc28 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 13 Jun 2024 11:09:48 +0300 Subject: [PATCH 2/4] Add pthreadMutexType to single-threaded autotuner --- src/autoTune.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 434b4fb0b2..8ec77739e7 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -186,7 +186,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"; "mhp"; "region"] +let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"] let reduceThreadAnalyses () = let isThreadCreate = function | LibraryDesc.ThreadCreate _ -> true From 30aeb975856b1fe4686bd82648cbd43c15ce686c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 13 Jun 2024 11:10:19 +0300 Subject: [PATCH 3/4] Use Mval.Unit for MutexTypeAnalysis.V --- src/analyses/mutexTypeAnalysis.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml index 441f2e9953..e8edddd41e 100644 --- a/src/analyses/mutexTypeAnalysis.ml +++ b/src/analyses/mutexTypeAnalysis.ml @@ -15,8 +15,9 @@ struct (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *) module O = Offset.Unit - module V = struct - include Printable.Prod(CilType.Varinfo)(O) (* TODO: use Mval.Unit *) + module V = + struct + include Mval.Unit let is_write_only _ = false end From ecda3f734f020703b0535e578513abfd9b2d53a4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 25 Jun 2024 11:24:45 +0300 Subject: [PATCH 4/4] Move comment in MutexTypeAnalysis --- src/analyses/mutexTypeAnalysis.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml index e8edddd41e..4a993bbd7d 100644 --- a/src/analyses/mutexTypeAnalysis.ml +++ b/src/analyses/mutexTypeAnalysis.ml @@ -12,17 +12,17 @@ struct let name () = "pthreadMutexType" - (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *) - module O = Offset.Unit - module V = struct + (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *) include Mval.Unit let is_write_only _ = false end module G = MAttr + module O = Offset.Unit + (* transfer functions *) let assign ctx (lval:lval) (rval:exp) : D.t = match lval with