diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 257bec24d8..da89aeba48 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -761,11 +761,15 @@ module type ClusterArg = functor (RD: RelationDomain.RD) -> sig module LRD: Lattice.S + module Cluster: Printable.S + val keep_only_protected_globals: Q.ask -> LockDomain.MustLock.t -> LRD.t -> LRD.t val keep_global: varinfo -> LRD.t -> LRD.t val lock: RD.t -> LRD.t -> LRD.t -> RD.t - val unlock: W.t -> RD.t -> LRD.t + val unlock: W.t -> RD.t -> LRD.t * (Cluster.t list) + + val filter_clusters: (Cluster.t -> bool) -> LRD.t -> LRD.t val name: unit -> string end @@ -775,6 +779,7 @@ module NoCluster:ClusterArg = functor (RD: RelationDomain.RD) -> struct open CommonPerMutex(RD) module LRD = RD + module Cluster = Printable.Unit let keep_only_protected_globals = keep_only_protected_globals @@ -786,7 +791,13 @@ struct RD.meet oct (RD.join local_m get_m) let unlock w oct_side = - oct_side + oct_side, [()] + + let filter_clusters f oct = + if f () then + oct + else + RD.bot () let name () = "no-clusters" end @@ -860,6 +871,8 @@ struct module VS = SetDomain.Make (CilType.Varinfo) module LRD = MapDomain.MapBot (VS) (RD) + module Cluster = VS + let keep_only_protected_globals ask m octs = (* normal (strong) mapping: contains only still fully protected *) (* must filter by protection to avoid later meeting with non-protecting *) @@ -909,7 +922,10 @@ struct let oct_side_cluster gs = RD.keep_vars oct_side (gs |> VS.elements |> List.map V.global) in - LRD.add_list_fun clusters oct_side_cluster (LRD.empty ()) + (LRD.add_list_fun clusters oct_side_cluster (LRD.empty ()), clusters) + + let filter_clusters f oct = + LRD.filter (fun gs _ -> f gs) oct let name = ClusteringArg.name end @@ -925,6 +941,8 @@ struct module LRD1 = DCCluster.LRD module LRD = Lattice.Prod (LRD1) (LRD1) (* second component is only used between keep_* and lock for additional weak mapping *) + module Cluster = DCCluster.Cluster + let name = ClusteringArg.name let filter_map' f m = @@ -986,7 +1004,11 @@ struct r let unlock w oct_side = - (DCCluster.unlock w oct_side, LRD1.bot ()) + let lad, clusters = DCCluster.unlock w oct_side in + ((lad, LRD1.bot ()), clusters) + + let filter_clusters f (lad,lad') = + (LRD1.filter (fun gs _ -> f gs) lad, LRD1.filter (fun gs _ -> f gs) lad') end (** Per-mutex meet with TIDs. *) @@ -1000,7 +1022,7 @@ struct module Cluster = NC module LRD = NC.LRD - include PerMutexTidCommon (Digest) (LRD) + include PerMutexTidCommon (Digest) (LRD) (NC.Cluster) module AV = RD.V module P = UnitP @@ -1022,13 +1044,11 @@ struct let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n get=%a" LockDomain.MustLock.pretty m LRD.pretty get_m; let r = - if not inits then - get_m - else - let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in - let get_mutex_inits' = Cluster.keep_only_protected_globals ask m get_mutex_inits in - if M.tracing then M.trace "relationpriv" "inits=%a\n inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits'; - LRD.join get_m get_mutex_inits' + let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in + let get_mutex_inits' = Cluster.keep_only_protected_globals ask m get_mutex_inits in + let get_mutex_inits' = Cluster.filter_clusters inits get_mutex_inits' in + if M.tracing then M.trace "relationpriv" "inits=%a\n inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits'; + LRD.join get_m get_mutex_inits' in if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r; r @@ -1047,13 +1067,11 @@ struct in if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n get=%a" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g; let r = - if not inits then - get_mutex_global_g - else - let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in - let get_mutex_inits' = Cluster.keep_global g get_mutex_inits in - if M.tracing then M.trace "relationpriv" "inits=%a\n inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits'; - LRD.join get_mutex_global_g get_mutex_inits' + let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in + let get_mutex_inits' = Cluster.keep_global g get_mutex_inits in + let get_mutex_inits' = Cluster.filter_clusters inits get_mutex_inits' in + if M.tracing then M.trace "relationpriv" "inits=%a\n inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits'; + LRD.join get_mutex_global_g get_mutex_inits' in if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r; r @@ -1061,11 +1079,9 @@ struct let get_mutex_global_g_with_mutex_inits_atomic inits ask getg = (* Unprotected invariant is one big relation. *) let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in - if not inits then - get_mutex_global_g - else - let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in - LRD.join get_mutex_global_g get_mutex_inits + let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in + let get_mutex_inits' = Cluster.filter_clusters inits get_mutex_inits in + LRD.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 = Param.handle_atomic && ask.f MustBeAtomic in @@ -1079,9 +1095,9 @@ struct if atomic && RD.mem_var rel (AV.global g) then rel (* Read previous unpublished unprotected write in current atomic section. *) else if atomic then - Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg) (* Read unprotected invariant as full relation. *) + Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg) (* Read unprotected invariant as full relation. *) else - Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g) + Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg g) in (* read *) let g_var = AV.global g in @@ -1113,9 +1129,9 @@ struct if atomic && RD.mem_var rel (AV.global g) then rel (* Read previous unpublished unprotected write in current atomic section. *) else if atomic then - Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg) (* Read unprotected invariant as full relation. *) + Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg) (* Read unprotected invariant as full relation. *) else - Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g) + Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg g) in (* write *) let g_var = AV.global g in @@ -1125,7 +1141,7 @@ struct (* unlock *) if not atomic then ( let rel_side = RD.keep_vars rel_local [g_var] in - let rel_side = Cluster.unlock (W.singleton g) rel_side in + let rel_side, clusters = Cluster.unlock (W.singleton g) rel_side in let digest = Digest.current ask in let sidev = GMutex.singleton digest rel_side in if Param.handle_atomic then @@ -1139,7 +1155,8 @@ struct else rel_local in - {rel = rel_local'; priv = (W.add g w,LMust.add lm lmust,l')} + let lmust' = List.fold (fun a c -> LMust.add (lm,c) a) lmust clusters in + {rel = rel_local'; priv = (W.add g w,lmust',l')} ) else (* Delay publishing unprotected write in the atomic section. *) @@ -1151,7 +1168,7 @@ struct let rel = st.rel in let _,lmust,l = st.priv in let lm = LLock.mutex m in - let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in + let get_m = get_m_with_mutex_inits (fun c -> (not (LMust.mem (lm,c) lmust))) ask getg m in let local_m = BatOption.default (LRD.bot ()) (L.find_opt lm l) in (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *) let local_m = Cluster.keep_only_protected_globals ask m local_m in @@ -1181,13 +1198,14 @@ struct {rel = rel_local; priv = (w',lmust,l)} else let rel_side = keep_only_protected_globals ask m rel in - let rel_side = Cluster.unlock w rel_side in + let rel_side, clusters = Cluster.unlock w rel_side in let digest = Digest.current ask in let sidev = GMutex.singleton digest rel_side in sideg (V.mutex m) (G.create_mutex sidev); let lm = LLock.mutex m in let l' = L.add lm rel_side l in - {rel = rel_local; priv = (w',LMust.add lm lmust,l')} + let lmust' = List.fold (fun a c -> LMust.add (lm,c) a) lmust clusters in + {rel = rel_local; priv = (w',lmust',l')} ) else ( (* Publish delayed unprotected write as if it were protected by the atomic section. *) @@ -1198,14 +1216,15 @@ struct {rel = rel_local; priv = (w',lmust,l)} else let rel_side = keep_only_globals ask m rel in - let rel_side = Cluster.unlock w rel_side in + let rel_side, clusters = Cluster.unlock w rel_side in let digest = Digest.current ask in let sidev = GMutex.singleton digest rel_side in (* Unprotected invariant is one big relation. *) sideg (V.mutex atomic_mutex) (G.create_mutex sidev); let (lmust', l') = W.fold (fun g (lmust, l) -> let lm = LLock.global g in - (LMust.add lm lmust, L.add lm rel_side l) + let lmust'' = List.fold (fun a c -> LMust.add (lm,c) a) lmust clusters in + (lmust'', L.add lm rel_side l) ) w (lmust, l) in {rel = rel_local; priv = (w',lmust',l')} @@ -1295,7 +1314,7 @@ struct ) (RD.vars rel) in let rel_side = RD.keep_vars rel g_vars in - let rel_side = Cluster.unlock (W.top ()) rel_side in (* top W to avoid any filtering *) + let rel_side, clusters = Cluster.unlock (W.top ()) rel_side in (* top W to avoid any filtering *) let digest = Digest.current ask in let sidev = GMutex.singleton digest rel_side in sideg V.mutex_inits (G.create_mutex sidev); diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 3afd758daa..96c211f084 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -476,7 +476,7 @@ module PerMutexMeetTIDPriv (Digest: Digest): S = struct open Queries.Protection include PerMutexMeetPrivBase - include PerMutexTidCommon (Digest) (CPA) + include PerMutexTidCommonNC (Digest) (CPA) let iter_sys_vars getg vq vf = match vq with diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 915b3da063..367d4eee25 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -237,7 +237,7 @@ struct | _ -> false end -module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) = +module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) (Cluster:Printable.S) = struct include ConfCheck.RequireThreadFlagPathSensInit @@ -266,9 +266,9 @@ struct let global x = `Right x end - (** Mutexes / globals to which values have been published, i.e. for which the initializers need not be read **) + (** Mutexes / clusters of globals to which values have been published, i.e., for which the initializers need not be read **) module LMust = struct - include SetDomain.Reverse (SetDomain.ToppedSet (LLock) (struct let topname = "All locks" end)) + include SetDomain.Reverse (SetDomain.ToppedSet (Printable.Prod(LLock)(Cluster)) (struct let topname = "All locks" end)) let name () = "LMust" end @@ -315,6 +315,14 @@ struct let startstate () = W.bot (), LMust.top (), L.bot () end +module PerMutexTidCommonNC (Digest: Digest) (LD:Lattice.S) = struct + include PerMutexTidCommon (Digest) (LD) (Printable.Unit) + module LMust = struct + include LMust + let mem lm lmust = mem (lm, ()) lmust + let add lm lmust = add (lm, ()) lmust + end +end let lift_lock (ask: Q.ask) f st (addr: LockDomain.Addr.t) = (* Should be in sync with: diff --git a/tests/regression/46-apron2/98-issue-1511b.c b/tests/regression/46-apron2/98-issue-1511b.c new file mode 100644 index 0000000000..cd6b8868a8 --- /dev/null +++ b/tests/regression/46-apron2/98-issue-1511b.c @@ -0,0 +1,33 @@ +// CRAM +#include +int d, j, k; + +pthread_mutex_t f; + +void nothing() {}; +void nothing2() {}; + +int top() { + int top2; + return top2; +} + +void main() { + d = top(); + if (d) { + k = 1; + pthread_t tid; + pthread_create(&tid, 0, ¬hing, NULL); + pthread_mutex_lock(&f); + j = 0; // To ensure something is published + pthread_mutex_unlock(&f); + pthread_mutex_lock(&f); + + pthread_t tid2; + pthread_create(&tid2, 0, ¬hing2, NULL); + float f = 8.0f; + } else { + pthread_t tid2; + pthread_create(&tid2, 0, ¬hing2, NULL); + } +} diff --git a/tests/regression/46-apron2/98-issue-1511b.t b/tests/regression/46-apron2/98-issue-1511b.t new file mode 100644 index 0000000000..741e80884a --- /dev/null +++ b/tests/regression/46-apron2/98-issue-1511b.t @@ -0,0 +1,44 @@ + $ goblint --disable warn.unsound --disable warn.imprecise --disable sem.unknown_function.invalidate.globals --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 98-issue-1511b.c --set witness.yaml.path 98-issue-1511b.yml + [Info][Witness] witness generation summary: + location invariants: 52 + loop invariants: 0 + flow-insensitive invariants: 2 + total generation entries: 29 + + $ goblint --disable warn.unsound --disable warn.imprecise --disable sem.unknown_function.invalidate.globals --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 98-issue-1511b.yml 98-issue-1511b.c + [Warning][Witness] cannot validate entry of type flow_insensitive_invariant + [Info][Witness] witness validation summary: + confirmed: 52 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 2 + disabled: 0 + total validation entries: 54 + [Success][Witness] invariant confirmed: (1LL + (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (1LL - (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (2147483646LL + (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (2147483646LL - (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (2147483646LL - (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (2147483649LL + (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (1LL + (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (1LL - (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (2147483646LL + (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (2147483646LL - (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (2147483646LL - (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (2147483649LL + (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:27:5) diff --git a/tests/regression/46-apron2/99-lmust-cluster-unsound.c b/tests/regression/46-apron2/99-lmust-cluster-unsound.c new file mode 100644 index 0000000000..96a727e8d8 --- /dev/null +++ b/tests/regression/46-apron2/99-lmust-cluster-unsound.c @@ -0,0 +1,35 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 +#include + +int a; +int b; + +pthread_mutex_t f; + +void nothing() {} +void nothing2() { + pthread_mutex_lock(&f); + a = 5; + b = 5; + pthread_mutex_unlock(&f); +} + + +void main() { + pthread_t tid; + int x; + pthread_create(&tid, 0, ¬hing, NULL); + + pthread_mutex_lock(&f); + b = 5; + pthread_mutex_unlock(&f); + + pthread_t tid2; + pthread_create(&tid2, 0, ¬hing2, NULL); + + pthread_mutex_lock(&f); + x = a; + pthread_mutex_unlock(&f); + + __goblint_check(x == 5); //UNKNOWN! +}