Skip to content

Commit fc9ecfc

Browse files
sim642sim642
committed
Rename to must_be_ancestor and may_be_ancestor
1 parent de117f5 commit fc9ecfc

File tree

3 files changed

+66
-66
lines changed

3 files changed

+66
-66
lines changed

‎src/cdomain/value/cdomains/threadIdDomain.ml‎

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,10 @@ sig
1313
val is_unique: t -> bool
1414

1515
(** Overapproximates whether the first TID can be involved in the creation fo the second TID*)
16-
val may_create: t -> t -> bool
16+
val may_be_ancestor: t -> t -> bool
1717

1818
(** Is the first TID a must parent of the second thread. Always false if the first TID is not unique *)
19-
val is_must_parent: t -> t -> bool
19+
val must_be_ancestor: t -> t -> bool
2020
end
2121

2222
module type Stateless =
@@ -87,8 +87,8 @@ struct
8787
| _ -> false
8888

8989
let is_unique _ = false (* TODO: should this consider main unique? *)
90-
let may_create _ _ = true
91-
let is_must_parent _ _ = false
90+
let may_be_ancestor _ _ = true
91+
let must_be_ancestor _ _ = false
9292
end
9393

9494

@@ -140,7 +140,7 @@ struct
140140
let is_unique (_, s) =
141141
S.is_empty s
142142

143-
let is_must_parent ((p, s) as t) ((p', s') as t') =
143+
let must_be_ancestor ((p, s) as t) ((p', s') as t') =
144144
if not (is_unique t) then
145145
false
146146
else if is_unique t' && P.equal p p' then (* t is already unique, so no need to compare sets *)
@@ -151,9 +151,9 @@ struct
151151
| _ :: _, _ -> false
152152
)
153153

154-
let may_create ((p, s) as t) ((p', s') as t') =
154+
let may_be_ancestor ((p, s) as t) ((p', s') as t') =
155155
if is_unique t' then
156-
is_must_parent t t' (* unique must be created by something unique (that's a prefix) *)
156+
must_be_ancestor t t' (* unique must be created by something unique (that's a prefix) *)
157157
else ( (* t' is already non-unique (but doesn't matter) *)
158158
match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with (* prefixes are stored reversed *)
159159
| [], dp when is_unique t -> (* p is prefix of p' *)
@@ -258,8 +258,8 @@ struct
258258

259259
let is_main = unop H.is_main P.is_main
260260
let is_unique = unop H.is_unique P.is_unique
261-
let may_create = binop H.may_create P.may_create
262-
let is_must_parent = binop H.is_must_parent P.is_must_parent
261+
let may_be_ancestor = binop H.may_be_ancestor P.may_be_ancestor
262+
let must_be_ancestor = binop H.must_be_ancestor P.must_be_ancestor
263263

264264
let created x d =
265265
let lifth x' d' =
@@ -355,14 +355,14 @@ struct
355355
| Thread tid -> FlagConfiguredTID.is_unique tid
356356
| UnknownThread -> false
357357

358-
let may_create t1 t2 =
358+
let may_be_ancestor t1 t2 =
359359
match t1, t2 with
360-
| Thread tid1, Thread tid2 -> FlagConfiguredTID.may_create tid1 tid2
360+
| Thread tid1, Thread tid2 -> FlagConfiguredTID.may_be_ancestor tid1 tid2
361361
| _, _ -> true
362362

363-
let is_must_parent t1 t2 =
363+
let must_be_ancestor t1 t2 =
364364
match t1, t2 with
365-
| Thread tid1, Thread tid2 -> FlagConfiguredTID.is_must_parent tid1 tid2
365+
| Thread tid1, Thread tid2 -> FlagConfiguredTID.must_be_ancestor tid1 tid2
366366
| _, _ -> false
367367

368368
module D = FlagConfiguredTID.D

‎src/cdomains/mHP.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ let current (ask:Queries.ask) =
2121
}
2222

2323
let pretty () {tid; created; must_joined} =
24-
let tid_doc =
24+
let tid_doc =
2525
if GobConfig.get_bool "dbg.full-output" then
2626
Some (Pretty.dprintf "tid=%a" ThreadIdDomain.ThreadLifted.pretty tid)
2727
else
@@ -53,10 +53,10 @@ include Printable.SimplePretty (
5353
(** Can it be excluded that the thread tid2 is running at a program point where *)
5454
(* thread tid1 has created the threads in created1 *)
5555
let definitely_not_started (current, created) other =
56-
if (not (TID.is_must_parent current other)) then
56+
if (not (TID.must_be_ancestor current other)) then
5757
false
5858
else
59-
let ident_or_may_be_created creator = TID.equal creator other || TID.may_create creator other in
59+
let ident_or_may_be_created creator = TID.equal creator other || TID.may_be_ancestor creator other in
6060
if ConcDomain.ThreadSet.is_top created then
6161
false
6262
else

‎tests/unit/cdomains/threadIdDomainTest.ml‎

Lines changed: 50 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -17,90 +17,90 @@ let (>>) (parent: History.t) (v: GoblintCil.varinfo): History.t =
1717
| [child] -> child
1818
| _ -> assert false
1919

20-
let test_history_is_must_parent _ =
20+
let test_history_must_be_ancestor _ =
2121
let open History in
2222
let assert_equal = assert_equal ~printer:string_of_bool in
2323

2424
(* non-unique is not must parent *)
25-
assert_equal false (is_must_parent (main >> a >> a) (main >> a >> a));
26-
assert_equal false (is_must_parent (main >> a >> a) (main >> a >> a >> a));
27-
assert_equal false (is_must_parent (main >> a >> a) (main >> a >> a >> b));
25+
assert_equal false (must_be_ancestor (main >> a >> a) (main >> a >> a));
26+
assert_equal false (must_be_ancestor (main >> a >> a) (main >> a >> a >> a));
27+
assert_equal false (must_be_ancestor (main >> a >> a) (main >> a >> a >> b));
2828

2929
(* unique is not self-parent *)
30-
assert_equal false (is_must_parent main main);
31-
assert_equal false (is_must_parent (main >> a) (main >> a));
32-
assert_equal false (is_must_parent (main >> a >> b) (main >> a >> b));
30+
assert_equal false (must_be_ancestor main main);
31+
assert_equal false (must_be_ancestor (main >> a) (main >> a));
32+
assert_equal false (must_be_ancestor (main >> a >> b) (main >> a >> b));
3333

3434
(* unique is must parent if prefix *)
35-
assert_equal true (is_must_parent main (main >> a));
36-
assert_equal true (is_must_parent main (main >> a >> a));
37-
assert_equal true (is_must_parent main (main >> a >> b));
38-
assert_equal true (is_must_parent (main >> a) (main >> a >> b));
39-
assert_equal false (is_must_parent (main >> a) main);
40-
assert_equal false (is_must_parent (main >> b) (main >> a >> b));
41-
assert_equal false (is_must_parent (main >> a) (main >> b >> a));
42-
assert_equal false (is_must_parent (main >> a) (main >> a >> a)); (* may be created by just main (non-uniquely) *)
35+
assert_equal true (must_be_ancestor main (main >> a));
36+
assert_equal true (must_be_ancestor main (main >> a >> a));
37+
assert_equal true (must_be_ancestor main (main >> a >> b));
38+
assert_equal true (must_be_ancestor (main >> a) (main >> a >> b));
39+
assert_equal false (must_be_ancestor (main >> a) main);
40+
assert_equal false (must_be_ancestor (main >> b) (main >> a >> b));
41+
assert_equal false (must_be_ancestor (main >> a) (main >> b >> a));
42+
assert_equal false (must_be_ancestor (main >> a) (main >> a >> a)); (* may be created by just main (non-uniquely) *)
4343
()
4444

45-
let test_history_may_create _ =
45+
let test_history_may_be_ancestor _ =
4646
let open History in
4747
let assert_equal = assert_equal ~printer:string_of_bool in
4848

4949
(* unique may only be created by unique (prefix) *)
50-
assert_equal true (may_create main (main >> a));
51-
assert_equal true (may_create main (main >> a >> b));
52-
assert_equal true (may_create (main >> a) (main >> a >> b));
53-
assert_equal false (may_create (main >> a) (main >> a)); (* infeasible for race: definitely_not_started allows equality *)
54-
assert_equal false (may_create (main >> b) (main >> a >> b)); (* 53-races-mhp/04-not-created2 *)
55-
assert_equal false (may_create (main >> a >> a) (main >> a >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique (main >> a >> b) *)
50+
assert_equal true (may_be_ancestor main (main >> a));
51+
assert_equal true (may_be_ancestor main (main >> a >> b));
52+
assert_equal true (may_be_ancestor (main >> a) (main >> a >> b));
53+
assert_equal false (may_be_ancestor (main >> a) (main >> a)); (* infeasible for race: definitely_not_started allows equality *)
54+
assert_equal false (may_be_ancestor (main >> b) (main >> a >> b)); (* 53-races-mhp/04-not-created2 *)
55+
assert_equal false (may_be_ancestor (main >> a >> a) (main >> a >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique (main >> a >> b) *)
5656

5757
(* unique creates non-unique and is prefix: added elements cannot be in prefix *)
58-
assert_equal true (may_create main (main >> a >> a));
59-
assert_equal true (may_create main (main >> a >> b >> b));
60-
assert_equal true (may_create (main >> a) (main >> a >> b >> b));
58+
assert_equal true (may_be_ancestor main (main >> a >> a));
59+
assert_equal true (may_be_ancestor main (main >> a >> b >> b));
60+
assert_equal true (may_be_ancestor (main >> a) (main >> a >> b >> b));
6161
(* TODO: added elements condition always true by construction in tests? *)
6262

6363
(* non-unique created by unique and is prefix: removed elements must be in set *)
64-
assert_equal true (may_create (main >> a) (main >> a >> a));
65-
assert_equal true (may_create (main >> a >> b) (main >> a >> b >> b));
66-
assert_equal true (may_create (main >> a >> b) (main >> a >> b >> a));
67-
assert_equal false (may_create (main >> a >> b) (main >> a >> a)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> a >> a), which it is not *)
68-
assert_equal false (may_create (main >> a >> b) (main >> b >> b)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> b), which it is not *)
64+
assert_equal true (may_be_ancestor (main >> a) (main >> a >> a));
65+
assert_equal true (may_be_ancestor (main >> a >> b) (main >> a >> b >> b));
66+
assert_equal true (may_be_ancestor (main >> a >> b) (main >> a >> b >> a));
67+
assert_equal false (may_be_ancestor (main >> a >> b) (main >> a >> a)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> a >> a), which it is not *)
68+
assert_equal false (may_be_ancestor (main >> a >> b) (main >> b >> b)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> b), which it is not *)
6969

7070
(* unique creates non-unique and prefixes are incompatible *)
71-
assert_equal false (may_create (main >> a) (main >> b >> a >> a)); (* 53-races-mhp/05-not-created3 *)
72-
assert_equal false (may_create (main >> a >> b) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
73-
assert_equal false (may_create (main >> a >> b) (main >> a >> c >> d >> d)); (* 53-races-mhp/06-not-created4, also passes with simple may_create *)
71+
assert_equal false (may_be_ancestor (main >> a) (main >> b >> a >> a)); (* 53-races-mhp/05-not-created3 *)
72+
assert_equal false (may_be_ancestor (main >> a >> b) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
73+
assert_equal false (may_be_ancestor (main >> a >> b) (main >> a >> c >> d >> d)); (* 53-races-mhp/06-not-created4, also passes with simple may_be_ancestor *)
7474

7575
(* non-unique creates non-unique: prefix must not lengthen *)
76-
assert_equal false (may_create (main >> a >> a) (main >> a >> b >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique prefix-ed (main >> a >> b >> b) *)
77-
assert_equal false (may_create (main >> a >> a) (main >> b >> a >> a)); (* 53-races-mhp/07-not-created5 *)
76+
assert_equal false (may_be_ancestor (main >> a >> a) (main >> a >> b >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique prefix-ed (main >> a >> b >> b) *)
77+
assert_equal false (may_be_ancestor (main >> a >> a) (main >> b >> a >> a)); (* 53-races-mhp/07-not-created5 *)
7878
(* non-unique creates non-unique: prefix must be compatible *)
79-
assert_equal false (may_create (main >> a >> b >> c >> c) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a >> b or main >> a >> b >> c), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
79+
assert_equal false (may_be_ancestor (main >> a >> b >> c >> c) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a >> b or main >> a >> b >> c), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
8080
(* non-unique creates non-unique: elements must not be removed *)
81-
assert_equal false (may_create (main >> a >> b >> b) (main >> a >> c >> c)); (* from set *) (* 53-races-mhp/08-not-created6, also passes with simple may_create *)
82-
assert_equal false (may_create (main >> a >> b >> b) (main >> b >> b)); (* from prefix *) (* infeasible for race: definitely_not_started requires (main >> a or main >> a >> b), where this must happen, to be must parent for (main >> b >> b), which it is not *)
81+
assert_equal false (may_be_ancestor (main >> a >> b >> b) (main >> a >> c >> c)); (* from set *) (* 53-races-mhp/08-not-created6, also passes with simple may_be_ancestor *)
82+
assert_equal false (may_be_ancestor (main >> a >> b >> b) (main >> b >> b)); (* from prefix *) (* infeasible for race: definitely_not_started requires (main >> a or main >> a >> b), where this must happen, to be must parent for (main >> b >> b), which it is not *)
8383
(* non-unique creates non-unique: removed elements and set must be in new set *)
84-
(* assert_equal false (may_create (main >> a >> b >> c >> c) (main >> a >> c >> c)); *)
84+
(* assert_equal false (may_be_ancestor (main >> a >> b >> c >> c) (main >> a >> c >> c)); *)
8585
(* TODO: cannot test due because by construction after prefix check? *)
8686
(* non-unique creates non-unique *)
87-
assert_equal true (may_create (main >> a >> a) (main >> a >> a));
88-
assert_equal true (may_create (main >> a >> a) (main >> a >> a >> b));
89-
assert_equal true (may_create (main >> a >> a) (main >> a >> b >> a));
90-
assert_equal true (may_create (main >> a >> a) (main >> a >> b >> c >> a));
91-
assert_equal true (may_create (main >> a >> b >> b) (main >> a >> b >> b));
92-
assert_equal true (may_create (main >> a >> b >> b) (main >> a >> a >> b));
93-
assert_equal true (may_create (main >> a >> b >> b) (main >> a >> b >> a));
94-
assert_equal true (may_create (main >> a >> b >> b) (main >> b >> b >> a));
95-
assert_equal true (may_create (main >> a >> b >> b) (main >> b >> a >> b));
87+
assert_equal true (may_be_ancestor (main >> a >> a) (main >> a >> a));
88+
assert_equal true (may_be_ancestor (main >> a >> a) (main >> a >> a >> b));
89+
assert_equal true (may_be_ancestor (main >> a >> a) (main >> a >> b >> a));
90+
assert_equal true (may_be_ancestor (main >> a >> a) (main >> a >> b >> c >> a));
91+
assert_equal true (may_be_ancestor (main >> a >> b >> b) (main >> a >> b >> b));
92+
assert_equal true (may_be_ancestor (main >> a >> b >> b) (main >> a >> a >> b));
93+
assert_equal true (may_be_ancestor (main >> a >> b >> b) (main >> a >> b >> a));
94+
assert_equal true (may_be_ancestor (main >> a >> b >> b) (main >> b >> b >> a));
95+
assert_equal true (may_be_ancestor (main >> a >> b >> b) (main >> b >> a >> b));
9696

9797
(* 4f6a7637b8d0dc723fe382f94bed6c822cd4a2ce passes all... *)
9898
()
9999

100100
let tests =
101101
"threadIdDomainTest" >::: [
102102
"history" >::: [
103-
"is_must_parent" >:: test_history_is_must_parent;
104-
"may_create" >:: test_history_may_create;
103+
"must_be_ancestor" >:: test_history_must_be_ancestor;
104+
"may_be_ancestor" >:: test_history_may_be_ancestor;
105105
]
106106
]

0 commit comments

Comments
 (0)