Skip to content

Relational MM: Cluster LMust #1643

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
michael-schwarz merged 7 commits into from
Jan 14, 2025
Merged

Relational MM: Cluster LMust #1643

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
5ebc5d7
Clustered LMust
michael-schwarz Aug 6, 2024
61a4071
Add regression test
michael-schwarz Aug 6, 2024
c592373
Fix cram tests
michael-schwarz Dec 17, 2024
174b24b
Define signature directly
michael-schwarz Jan 12, 2025
020a1c7
Add soundness example
michael-schwarz Jan 12, 2025
7cef967
Swap argument order for `filter_clusters`
michael-schwarz Jan 12, 2025
15b269f
Mention clusters in comment
michael-schwarz Jan 12, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
91 changes: 55 additions & 36 deletions src/analyses/apron/relationPriv.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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 *)
Expand Down Expand Up @@ -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
Expand All @@ -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 =
Expand Down Expand Up @@ -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. *)
Expand All @@ -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
Expand All @@ -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
Expand All @@ -1047,25 +1067,21 @@ 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

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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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. *)
Expand All @@ -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
Expand Down Expand Up @@ -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. *)
Expand All @@ -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')}
Expand Down Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/basePriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
14 changes: 11 additions & 3 deletions src/analyses/commonPriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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:
Expand Down
33 changes: 33 additions & 0 deletions tests/regression/46-apron2/98-issue-1511b.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
// CRAM
#include<pthread.h>
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, &nothing, 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, &nothing2, NULL);
float f = 8.0f;
} else {
pthread_t tid2;
pthread_create(&tid2, 0, &nothing2, NULL);
}
}
44 changes: 44 additions & 0 deletions tests/regression/46-apron2/98-issue-1511b.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
Loading
Loading