Skip to content

Commit 61aa24e

Browse files
sim642sim642
authored
Merge pull request #2015 from goblint/patricia-tree2
Use patricia-tree library more
2 parents ef751d0 + 663ee11 commit 61aa24e

9 files changed

Lines changed: 178 additions & 96 deletions

File tree

‎src/analyses/commonPriv.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,7 @@ struct
169169

170170
module W =
171171
struct
172-
include MapDomain.MapBot_LiftTop (Basetype.Variables) (MinLocksets)
172+
include MapDomain.PatriciaMapBot_LiftTop (Basetype.Variables) (MinLocksets)
173173
let name () = "W"
174174
end
175175

@@ -178,7 +178,7 @@ struct
178178
(* Note different Map order! *)
179179
(* MapTop because default value in P must be top of MinLocksets,
180180
as opposed to bottom in W. *)
181-
include MapDomain.MapTop_LiftBot (Basetype.Variables) (MinLocksets)
181+
include MapDomain.PatriciaMapTop_LiftBot (Basetype.Variables) (MinLocksets)
182182
let name () = "P"
183183

184184
(* TODO: change MinLocksets.exists/top instead? *)

‎src/analyses/loopTermination.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ struct
3636
end
3737

3838
(** We want to record termination information of loops and use the loop statements for that. *)
39-
module G = MapDomain.MapBot (CilType.Stmt) (BoolDomain.MustBool)
39+
module G = MapDomain.PatriciaMapBot (CilType.Stmt) (BoolDomain.MustBool)
4040

4141
let startstate _ = ()
4242
let exitstate = startstate

‎src/analyses/startStateAnalysis.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ module Spec : Analyses.MCPSpec =
1212
struct
1313
let name () = "startState"
1414
module AD = ValueDomain.AD
15-
module D = MapDomain.MapBot (Basetype.Variables) (AD)
15+
module D = MapDomain.PatriciaMapBot (Basetype.Variables) (AD)
1616
module C = D
1717

1818
include Analyses.IdentitySpec

‎src/cdomains/baseDomain.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ end
2020
module PartDeps =
2121
struct
2222
module VarSet = SetDomain.Make(Basetype.Variables)
23-
include MapDomain.MapBot_LiftTop(Basetype.Variables)(VarSet)
23+
include MapDomain.PatriciaMapBot_LiftTop(Basetype.Variables)(VarSet)
2424
let name () = "array partitioning deps"
2525
end
2626

‎src/common/util/cilType.ml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -390,6 +390,7 @@ struct
390390
let equal x y = Varinfo.equal x.svar y.svar
391391
let compare x y = Varinfo.compare x.svar y.svar
392392
let hash x = Varinfo.hash x.svar
393+
let tag x = Varinfo.tag x.svar
393394

394395
(* Output *)
395396
let pretty () x = Varinfo.pretty () x.svar
@@ -512,6 +513,7 @@ struct
512513
let equal x y = x.sid = y.sid
513514
let compare x y = Stdlib.compare x.sid y.sid
514515
let hash x = x.sid
516+
let tag x = x.sid
515517

516518
(* Output *)
517519
let pretty () x = dn_stmt () x

‎src/domain/disjointDomain.ml‎

Lines changed: 86 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -98,19 +98,14 @@ struct
9898
end
9999
| None -> m
100100
let diff m1 m2 =
101-
M.merge (fun _ b1 b2 ->
102-
match b1, b2 with
103-
| Some b1, Some b2 ->
104-
begin match B.diff b1 b2 with
105-
| b' when B.is_bot b' ->
106-
None (* remove bot bucket to preserve invariant *)
107-
| exception Lattice.BotValue ->
108-
None (* remove bot bucket to preserve invariant *)
109-
| b' ->
110-
Some b'
111-
end
112-
| Some _, None -> b1
113-
| None, _ -> None
101+
M.difference (fun b1 b2 ->
102+
match B.diff b1 b2 with
103+
| b' when B.is_bot b' ->
104+
None (* remove bot bucket to preserve invariant *)
105+
| exception Lattice.BotValue ->
106+
None (* remove bot bucket to preserve invariant *)
107+
| b' ->
108+
Some b'
114109
) m1 m2
115110

116111
let of_list es = List.fold_left (fun acc e ->
@@ -127,32 +122,24 @@ struct
127122
M.widen m1 m2
128123

129124
let meet m1 m2 =
130-
M.merge (fun _ b1 b2 ->
131-
match b1, b2 with
132-
| Some b1, Some b2 ->
133-
begin match B.meet b1 b2 with
134-
| b' when B.is_bot b' ->
135-
None (* remove bot bucket to preserve invariant *)
136-
| exception Lattice.BotValue ->
137-
None (* remove bot bucket to preserve invariant *)
138-
| b' ->
139-
Some b'
140-
end
141-
| _, _ -> None
125+
M.nonidempotent_inter_filter (fun b1 b2 -> (* TODO: idempotent_inter_filter if not using int domain refinement *)
126+
match B.meet b1 b2 with
127+
| b' when B.is_bot b' ->
128+
None (* remove bot bucket to preserve invariant *)
129+
| exception Lattice.BotValue ->
130+
None (* remove bot bucket to preserve invariant *)
131+
| b' ->
132+
Some b'
142133
) m1 m2
143134
let narrow m1 m2 =
144-
M.merge (fun _ b1 b2 ->
145-
match b1, b2 with
146-
| Some b1, Some b2 ->
147-
begin match B.narrow b1 b2 with
148-
| b' when B.is_bot b' ->
149-
None (* remove bot bucket to preserve invariant *)
150-
| exception Lattice.BotValue ->
151-
None (* remove bot bucket to preserve invariant *)
152-
| b' ->
153-
Some b'
154-
end
155-
| _, _ -> None
135+
M.nonidempotent_inter_filter (fun b1 b2 -> (* TODO: idempotent_inter_filter if not using int domain refinement *)
136+
match B.narrow b1 b2 with
137+
| b' when B.is_bot b' ->
138+
None (* remove bot bucket to preserve invariant *)
139+
| exception Lattice.BotValue ->
140+
None (* remove bot bucket to preserve invariant *)
141+
| b' ->
142+
Some b'
156143
) m1 m2
157144

158145
let union = join
@@ -578,45 +565,75 @@ struct
578565
let nonidempotent_union f m1 m2 = M.nonidempotent_union (fun b1 b2 ->
579566
B.nonidempotent_union f b1 b2
580567
) m1 m2
581-
let idempotent_inter f m1 m2 = M.idempotent_inter (fun b1 b2 ->
582-
B.idempotent_inter f b1 b2
568+
let idempotent_inter f m1 m2 = M.idempotent_inter_filter (fun b1 b2 ->
569+
match B.idempotent_inter f b1 b2 with
570+
| b' when B.is_bot b' ->
571+
None (* remove bot bucket to preserve invariant *)
572+
| exception Lattice.BotValue ->
573+
None (* remove bot bucket to preserve invariant *)
574+
| b' ->
575+
Some b'
576+
) m1 m2
577+
let nonidempotent_inter f m1 m2 = M.nonidempotent_inter_filter (fun b1 b2 ->
578+
match B.nonidempotent_inter f b1 b2 with
579+
| b' when B.is_bot b' ->
580+
None (* remove bot bucket to preserve invariant *)
581+
| exception Lattice.BotValue ->
582+
None (* remove bot bucket to preserve invariant *)
583+
| b' ->
584+
Some b'
583585
) m1 m2
584-
let nonidempotent_inter f m1 m2 = M.nonidempotent_inter (fun b1 b2 ->
585-
B.nonidempotent_inter f b1 b2
586+
let idempotent_inter_filter f m1 m2 = M.idempotent_inter_filter (fun b1 b2 ->
587+
match B.idempotent_inter_filter f b1 b2 with
588+
| b' when B.is_bot b' ->
589+
None (* remove bot bucket to preserve invariant *)
590+
| exception Lattice.BotValue ->
591+
None (* remove bot bucket to preserve invariant *)
592+
| b' ->
593+
Some b'
594+
) m1 m2
595+
let nonidempotent_inter_filter f m1 m2 = M.nonidempotent_inter_filter (fun b1 b2 ->
596+
match B.nonidempotent_inter_filter f b1 b2 with
597+
| b' when B.is_bot b' ->
598+
None (* remove bot bucket to preserve invariant *)
599+
| exception Lattice.BotValue ->
600+
None (* remove bot bucket to preserve invariant *)
601+
| b' ->
602+
Some b'
603+
) m1 m2
604+
let difference f m1 m2 = M.difference (fun b1 b2 ->
605+
match B.difference f b1 b2 with
606+
| b' when B.is_bot b' ->
607+
None (* remove bot bucket to preserve invariant *)
608+
| exception Lattice.BotValue ->
609+
None (* remove bot bucket to preserve invariant *)
610+
| b' ->
611+
Some b'
586612
) m1 m2
587-
let merge f m1 m2 = failwith "ProjectiveMap.merge" (* TODO: ? *)
588613

589614
let widen m1 m2 =
590615
Lattice.assert_valid_widen ~leq ~pretty_diff m1 m2;
591616
M.widen m1 m2
592617

593618
let meet m1 m2 =
594-
M.merge (fun _ b1 b2 ->
595-
match b1, b2 with
596-
| Some b1, Some b2 ->
597-
begin match B.meet b1 b2 with
598-
| b' when B.is_bot b' ->
599-
None (* remove bot bucket to preserve invariant *)
600-
| exception Lattice.BotValue ->
601-
None (* remove bot bucket to preserve invariant *)
602-
| b' ->
603-
Some b'
604-
end
605-
| _, _ -> None
619+
M.nonidempotent_inter_filter (fun b1 b2 -> (* TODO: idempotent_inter_filter if not using int domain refinement *)
620+
match B.meet b1 b2 with
621+
| b' when B.is_bot b' ->
622+
None (* remove bot bucket to preserve invariant *)
623+
| exception Lattice.BotValue ->
624+
None (* remove bot bucket to preserve invariant *)
625+
| b' ->
626+
Some b'
606627
) m1 m2
607628
let narrow m1 m2 =
608-
M.merge (fun _ b1 b2 ->
609-
match b1, b2 with
610-
| Some b1, Some b2 ->
611-
begin match B.narrow b1 b2 with
612-
| b' when B.is_bot b' ->
613-
None (* remove bot bucket to preserve invariant *)
614-
| exception Lattice.BotValue ->
615-
None (* remove bot bucket to preserve invariant *)
616-
| b' ->
617-
Some b'
618-
end
619-
| _, _ -> None
629+
M.nonidempotent_inter_filter (fun b1 b2 -> (* TODO: idempotent_inter_filter if not using int domain refinement *)
630+
match B.narrow b1 b2 with
631+
| b' when B.is_bot b' ->
632+
None (* remove bot bucket to preserve invariant *)
633+
| exception Lattice.BotValue ->
634+
None (* remove bot bucket to preserve invariant *)
635+
| b' ->
636+
Some b'
620637
) m1 m2
621638

622639
include MapDomain.Print (E) (V) (
@@ -778,7 +795,9 @@ struct
778795
in
779796
snd (S.fold f s2 (s1, S.empty ()))
780797
let idempotent_inter _ _ _ = failwith "PairwiseMap.idempotent_inter" (* TODO: ? *)
781-
let merge f m1 m2 = failwith "PairwiseMap.merge" (* TODO: ? *)
798+
let idempotent_inter_filter _ _ _ = failwith "PairwiseMap.idempotent_inter_filter" (* TODO: ? *)
799+
let nonidempotent_inter_filter _ _ _ = failwith "PairwiseMap.nonidempotent_inter_filter" (* TODO: ? *)
800+
let difference _ _ _ = failwith "PairwiseMap.difference" (* TODO: ? *)
782801

783802
let leq s1 s2 =
784803
S.for_all (fun b1 ->

0 commit comments

Comments
 (0)