From 105fd3a963388983f3fd56a7e199ed98d89351ed Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Jan 2024 16:22:37 +0200 Subject: [PATCH] Separate relation mutex-meet with atomic support --- src/analyses/apron/relationPriv.apron.ml | 37 ++++++++++++------- src/common/util/options.schema.json | 2 +- tests/regression/46-apron2/58-atomic_priv.c | 2 +- .../regression/46-apron2/59-atomic_fun_priv.c | 2 +- .../46-apron2/60-atomic_priv_sound.c | 2 +- .../46-apron2/61-atomic_priv_sound2.c | 2 +- .../46-apron2/62-atomic_priv_sound3.c | 2 +- .../regression/46-apron2/63-atomic_relation.c | 2 +- .../64-case_distinction_with_ghosts.c | 2 +- .../65-case_distinction_with_ghosts-2.c | 2 +- .../66-case_distinction_with_ghosts-3.c | 2 +- .../46-apron2/67-nondet_inc_with_ghosts.c | 2 +- .../46-apron2/68-nondet_inc_with_ghosts-2.c | 2 +- .../46-apron2/69-nondet_inc_with_ghosts-3.c | 2 +- tests/regression/46-apron2/71-mutex.c | 2 +- .../46-apron2/72-mutex_with_ghosts.c | 2 +- .../46-apron2/73-mutex_with_ghosts-2.c | 2 +- 17 files changed, 39 insertions(+), 30 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index cdea217081..cab7b9285a 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -452,7 +452,7 @@ struct end (** Per-mutex meet. *) -module PerMutexMeetPriv : S = functor (RD: RelationDomain.RD) -> +module PerMutexMeetPriv (Param: AtomicParam) : S = functor (RD: RelationDomain.RD) -> struct open CommonPerMutex(RD) include MutexGlobals @@ -479,27 +479,32 @@ struct RD.join get_m get_mutex_inits' let get_mutex_global_g_with_mutex_inits ask getg g = - let get_mutex_global_g = getg (V.mutex atomic_mutex) in - let get_mutex_inits = getg V.mutex_inits in let g_var = AV.global g in - let get_mutex_global_g' = RD.keep_vars get_mutex_global_g [g_var] in + let get_mutex_global_g = + if Param.handle_atomic then ( + RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var] + ) + else + getg (V.global g) + in + let get_mutex_inits = getg V.mutex_inits in let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in - RD.join get_mutex_global_g' get_mutex_inits' + RD.join get_mutex_global_g get_mutex_inits' - let get_mutex_global_g_with_mutex_inits' ask getg = + let get_mutex_global_g_with_mutex_inits_atomic ask getg = let get_mutex_global_g = getg (V.mutex atomic_mutex) in let get_mutex_inits = getg V.mutex_inits in RD.join get_mutex_global_g get_mutex_inits let read_global (ask: Q.ask) getg (st: relation_components_t) g x: RD.t = - let atomic = ask.f MustBeAtomic in + let atomic = Param.handle_atomic && ask.f MustBeAtomic in let rel = st.rel in (* lock *) let rel = if atomic && RD.mem_var rel (AV.global g) then rel else if atomic then - RD.meet rel (get_mutex_global_g_with_mutex_inits' ask getg) + RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg) else RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g) in @@ -522,14 +527,14 @@ struct rel_local let write_global ?(invariant=false) (ask: Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t = - let atomic = ask.f MustBeAtomic in + let atomic = Param.handle_atomic && ask.f MustBeAtomic in let rel = st.rel in (* lock *) let rel = if atomic && RD.mem_var rel (AV.global g) then rel else if atomic then - RD.meet rel (get_mutex_global_g_with_mutex_inits' ask getg) + RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg) else RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g) in @@ -541,7 +546,10 @@ struct (* unlock *) if not atomic then ( let rel_side = RD.keep_vars rel_local [g_var] in - sideg (V.mutex atomic_mutex) rel_side; + if Param.handle_atomic then + sideg (V.mutex atomic_mutex) rel_side + else + sideg (V.global g) rel_side; let rel_local' = if is_unprotected ask g then RD.remove_vars rel_local [g_var] @@ -555,7 +563,7 @@ struct let lock ask getg (st: relation_components_t) m = - let atomic = LockDomain.Addr.equal m (atomic_mutex) in + let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in (* TODO: somehow actually unneeded here? *) if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then ( let rel = st.rel in @@ -569,7 +577,7 @@ struct st (* sound w.r.t. recursive lock *) let unlock ask getg sideg (st: relation_components_t) m: relation_components_t = - let atomic = LockDomain.Addr.equal m (atomic_mutex) in + let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in let rel = st.rel in if not atomic then ( let rel_side = keep_only_protected_globals ask m rel in @@ -1373,7 +1381,8 @@ let priv_module: (module S) Lazy.t = | "top" -> (module Top : S) | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end)) | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end)) - | "mutex-meet" -> (module PerMutexMeetPriv) + | "mutex-meet" -> (module PerMutexMeetPriv (struct let handle_atomic = false end)) + | "mutex-meet-atomic" -> (module PerMutexMeetPriv (struct let handle_atomic = true end)) | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoCluster)) | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (Clustering12))) | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ArbitraryCluster (Clustering2))) diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json index bb4fa194df..aacccf64a9 100644 --- a/src/common/util/options.schema.json +++ b/src/common/util/options.schema.json @@ -921,7 +921,7 @@ "description": "Which relation privatization to use? top/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power", "type": "string", - "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"], + "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-atomic", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"], "default": "mutex-meet" }, "priv": { diff --git a/tests/regression/46-apron2/58-atomic_priv.c b/tests/regression/46-apron2/58-atomic_priv.c index e8d474357b..f7c56ac515 100644 --- a/tests/regression/46-apron2/58-atomic_priv.c +++ b/tests/regression/46-apron2/58-atomic_priv.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none #include #include diff --git a/tests/regression/46-apron2/59-atomic_fun_priv.c b/tests/regression/46-apron2/59-atomic_fun_priv.c index 21df5d380f..24b3405d8f 100644 --- a/tests/regression/46-apron2/59-atomic_fun_priv.c +++ b/tests/regression/46-apron2/59-atomic_fun_priv.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none #include #include diff --git a/tests/regression/46-apron2/60-atomic_priv_sound.c b/tests/regression/46-apron2/60-atomic_priv_sound.c index 79103337c7..87ea674727 100644 --- a/tests/regression/46-apron2/60-atomic_priv_sound.c +++ b/tests/regression/46-apron2/60-atomic_priv_sound.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none #include #include diff --git a/tests/regression/46-apron2/61-atomic_priv_sound2.c b/tests/regression/46-apron2/61-atomic_priv_sound2.c index c9ecb90a1e..393e56a026 100644 --- a/tests/regression/46-apron2/61-atomic_priv_sound2.c +++ b/tests/regression/46-apron2/61-atomic_priv_sound2.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none #include #include diff --git a/tests/regression/46-apron2/62-atomic_priv_sound3.c b/tests/regression/46-apron2/62-atomic_priv_sound3.c index 7967507b65..1a8ee32581 100644 --- a/tests/regression/46-apron2/62-atomic_priv_sound3.c +++ b/tests/regression/46-apron2/62-atomic_priv_sound3.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none #include #include diff --git a/tests/regression/46-apron2/63-atomic_relation.c b/tests/regression/46-apron2/63-atomic_relation.c index 4169b1e447..d3ab987ae6 100644 --- a/tests/regression/46-apron2/63-atomic_relation.c +++ b/tests/regression/46-apron2/63-atomic_relation.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none #include #include diff --git a/tests/regression/46-apron2/64-case_distinction_with_ghosts.c b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c index 633c1192c9..b319f3e4b1 100644 --- a/tests/regression/46-apron2/64-case_distinction_with_ghosts.c +++ b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none #include #include diff --git a/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c b/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c index 89371e74fa..223734e395 100644 --- a/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c +++ b/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none #include #include diff --git a/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c b/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c index 6fc2700299..e130c68fa1 100644 --- a/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c +++ b/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none #include #include diff --git a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c index 2fc073db05..a7227e3793 100644 --- a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c +++ b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening #include #include diff --git a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c index 380821add9..e5a281ec0c 100644 --- a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c +++ b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening #include #include diff --git a/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c b/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c index 0519dbda00..b6f4f69858 100644 --- a/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c +++ b/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none #include #include diff --git a/tests/regression/46-apron2/71-mutex.c b/tests/regression/46-apron2/71-mutex.c index abcdda8c49..99148c4d77 100644 --- a/tests/regression/46-apron2/71-mutex.c +++ b/tests/regression/46-apron2/71-mutex.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none /*----------------------------------------------------------------------------- * mutex.c - Concurrent program using locking to access a shared variable *----------------------------------------------------------------------------- diff --git a/tests/regression/46-apron2/72-mutex_with_ghosts.c b/tests/regression/46-apron2/72-mutex_with_ghosts.c index 8695a6133a..ccd6eab93f 100644 --- a/tests/regression/46-apron2/72-mutex_with_ghosts.c +++ b/tests/regression/46-apron2/72-mutex_with_ghosts.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none /*----------------------------------------------------------------------------- * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for * witness validation using locking to access a shared diff --git a/tests/regression/46-apron2/73-mutex_with_ghosts-2.c b/tests/regression/46-apron2/73-mutex_with_ghosts-2.c index 48ae9a5263..84a18faa20 100644 --- a/tests/regression/46-apron2/73-mutex_with_ghosts-2.c +++ b/tests/regression/46-apron2/73-mutex_with_ghosts-2.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none /*----------------------------------------------------------------------------- * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for * witness validation using locking to access a shared