Skip to content
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.

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

Improve history thread ID may_create #1561

Open
wants to merge 18 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 17 commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
52055b1
Improve history thread ID may_create for unique threads
sim642 Aug 14, 2024
baa497a
Improve history thread ID may_create for incompatible prefixes
sim642 Aug 14, 2024
4f6a763
Improve history thread ID may_create for both non-unique threads
sim642 Aug 14, 2024
dbd4874
Improve history thread ID may_create for first unique thread extension
sim642 Aug 14, 2024
c2c596f
Improve history thread ID may_create for first unique thread prefix s…
sim642 Aug 14, 2024
bb2fa08
Remove history thread ID may_create for first unique thread prefix TODO
sim642 Aug 14, 2024
f3dda0e
Add history thread ID domain unit tests
sim642 Aug 15, 2024
be2b3e2
Add TODOs to history thread ID may_create
sim642 Aug 15, 2024
73a22d7
Do additional simplifications to history thread ID may_create
sim642 Aug 15, 2024
b6fd349
Optimize history thread IDs using GobList.remove_common_prefix
sim642 Aug 15, 2024
31d22ef
Simplify history thread ID may_create
sim642 Aug 15, 2024
5f1b296
Clean up history thread ID is_must_parent
sim642 Aug 15, 2024
9744751
Fix GobList.remove_common_prefix doc indentation
sim642 Aug 15, 2024
8e54444
Construct feasible races-mhp regression tests for improved history th…
sim642 Aug 15, 2024
cc7a76a
Fix comment in history thread ID is_must_parent
sim642 Aug 15, 2024
de117f5
Merge branch 'master' into threadid-history-may_create
sim642 Aug 20, 2024
fc9ecfc
Rename to must_be_ancestor and may_be_ancestor
sim642 Aug 20, 2024
205d2b9
Fix ThreadIdDomain comments from review
sim642 Dec 17, 2024
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
56 changes: 36 additions & 20 deletions src/cdomain/value/cdomains/threadIdDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,10 @@ sig
val is_unique: t -> bool

(** Overapproximates whether the first TID can be involved in the creation fo the second TID*)
sim642 marked this conversation as resolved.
Show resolved Hide resolved
val may_create: t -> t -> bool
val may_be_ancestor: t -> t -> bool

(** Is the first TID a must parent of the second thread. Always false if the first TID is not unique *)
sim642 marked this conversation as resolved.
Show resolved Hide resolved
val is_must_parent: t -> t -> bool
val must_be_ancestor: t -> t -> bool
end

module type Stateless =
Expand Down Expand Up @@ -87,8 +87,8 @@ struct
| _ -> false

let is_unique _ = false (* TODO: should this consider main unique? *)
michael-schwarz marked this conversation as resolved.
Show resolved Hide resolved
let may_create _ _ = true
let is_must_parent _ _ = false
let may_be_ancestor _ _ = true
let must_be_ancestor _ _ = false
end


Expand Down Expand Up @@ -140,18 +140,34 @@ struct
let is_unique (_, s) =
S.is_empty s

let is_must_parent (p,s) (p',s') =
if not (S.is_empty s) then
let must_be_ancestor ((p, s) as t) ((p', s') as t') =
if not (is_unique t) then
false
else if P.equal p' p && S.is_empty s' then (* s is already empty *)
(* We do not consider a thread its own parent *)
false
else
let cdef_ancestor = P.common_suffix p p' in
P.equal p cdef_ancestor
else if is_unique t' && P.equal p p' then (* t is already unique, so no need to compare sets *)
false (* thread is not its own parent *)
else ( (* t is already unique, so no need to check sets *)
match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with (* prefixes are stored reversed *)
| [], _ -> true (* p is prefix of p' *)
| _ :: _, _ -> false
)

let may_create (p,s) (p',s') =
S.subset (S.union (S.of_list p) s) (S.union (S.of_list p') s')
let may_be_ancestor ((p, s) as t) ((p', s') as t') =
if is_unique t' then
must_be_ancestor t t' (* unique must be created by something unique (that's a prefix) *)
else ( (* t' is already non-unique (but doesn't matter) *)
match GobList.remove_common_prefix Base.equal (List.rev p) (List.rev p') with (* prefixes are stored reversed *)
| [], dp when is_unique t -> (* p is prefix of p' *)
(* dp = elements added to prefix (reversed, but doesn't matter) *)
true (* all elements are contained: p is prefix of p' and s is empty (due to uniqueness) *)
| dp', [] -> (* p' is prefix of p *)
(* dp' = elements removed from prefix (reversed, but doesn't matter) *)
S.subset (S.of_list dp') s' && (* removed elements become part of set, must be contained, because compose can only add them *)
S.subset s s' (* set elements must be contained, because compose can only add them *)
| [], _ :: _ -> (* p is strict prefix of p' and t is non-unique *)
false (* composing to non-unique cannot lengthen prefix *)
| _ :: _, _ :: _ -> (* prefixes are incompatible *)
false (* composing cannot fix incompatibility there *)
)

let compose ((p, s) as current) ni =
if BatList.mem_cmp Base.compare ni p then (
Expand Down Expand Up @@ -242,8 +258,8 @@ struct

let is_main = unop H.is_main P.is_main
let is_unique = unop H.is_unique P.is_unique
let may_create = binop H.may_create P.may_create
let is_must_parent = binop H.is_must_parent P.is_must_parent
let may_be_ancestor = binop H.may_be_ancestor P.may_be_ancestor
let must_be_ancestor = binop H.must_be_ancestor P.must_be_ancestor

let created x d =
let lifth x' d' =
Expand Down Expand Up @@ -339,14 +355,14 @@ struct
| Thread tid -> FlagConfiguredTID.is_unique tid
| UnknownThread -> false

let may_create t1 t2 =
let may_be_ancestor t1 t2 =
match t1, t2 with
| Thread tid1, Thread tid2 -> FlagConfiguredTID.may_create tid1 tid2
| Thread tid1, Thread tid2 -> FlagConfiguredTID.may_be_ancestor tid1 tid2
| _, _ -> true

let is_must_parent t1 t2 =
let must_be_ancestor t1 t2 =
match t1, t2 with
| Thread tid1, Thread tid2 -> FlagConfiguredTID.is_must_parent tid1 tid2
| Thread tid1, Thread tid2 -> FlagConfiguredTID.must_be_ancestor tid1 tid2
| _, _ -> false

module D = FlagConfiguredTID.D
Expand Down
6 changes: 3 additions & 3 deletions src/cdomains/mHP.ml
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ let current (ask:Queries.ask) =
}

let pretty () {tid; created; must_joined} =
let tid_doc =
let tid_doc =
if GobConfig.get_bool "dbg.full-output" then
Some (Pretty.dprintf "tid=%a" ThreadIdDomain.ThreadLifted.pretty tid)
else
Expand Down Expand Up @@ -53,10 +53,10 @@ include Printable.SimplePretty (
(** Can it be excluded that the thread tid2 is running at a program point where *)
(* thread tid1 has created the threads in created1 *)
let definitely_not_started (current, created) other =
if (not (TID.is_must_parent current other)) then
if (not (TID.must_be_ancestor current other)) then
false
else
let ident_or_may_be_created creator = TID.equal creator other || TID.may_create creator other in
let ident_or_may_be_created creator = TID.equal creator other || TID.may_be_ancestor creator other in
if ConcDomain.ThreadSet.is_top created then
false
else
Expand Down
10 changes: 0 additions & 10 deletions src/common/domains/printable.ml
Original file line number Diff line number Diff line change
Expand Up @@ -631,16 +631,6 @@ struct
BatPrintf.fprintf f "<value>\n<map>\n";
loop 0 xs;
BatPrintf.fprintf f "</map>\n</value>\n"

let common_prefix x y =
let rec helper acc x y =
match x,y with
| x::xs, y::ys when Base.equal x y-> helper (x::acc) xs ys
| _ -> acc
in
List.rev (helper [] x y)

let common_suffix x y = List.rev (common_prefix (List.rev x) (List.rev y))
end

module type ChainParams = sig
Expand Down
16 changes: 16 additions & 0 deletions src/util/std/gobList.ml
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,22 @@ let rec fold_while_some (f : 'a -> 'b -> 'a option) (acc: 'a) (xs: 'b list): 'a

let equal = List.eq

(** [remove_common_prefix eq l1 l2] removes the common prefix ([p]) of [l1] and [l2] and
returns the rest of both lists a pair [(l1', l2')].
Formally, [p @ l1' = l1] and [p @ l2' = l2] such that [p] has maximal length.

This can be used to check being a prefix in both directions simultaneously:
- if [l1' = []], then [l1] is a prefix of [l2],
- if [l2' = []], then [l2] is a prefix of [l1].

In other cases, the common prefix is not returned (i.e. reconstructed) for efficiency reasons.

@param eq equality predicate for elements *)
let rec remove_common_prefix eq l1 l2 =
match l1, l2 with
| x1 :: l1', x2 :: l2' when eq x1 x2 -> remove_common_prefix eq l1' l2'
| _, _ -> (l1, l2)

(** Given a predicate and a list, returns two lists [(l1, l2)].
[l1] contains the prefix of the list until the last element that satisfies the predicate, [l2] contains all subsequent elements. The order of elements is preserved. *)
let until_last_with (pred: 'a -> bool) (xs: 'a list) =
Expand Down
25 changes: 25 additions & 0 deletions tests/regression/53-races-mhp/04-not-created2.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
#include <pthread.h>

int g;

void *b(void *arg) {
int *gp = arg;
if (gp)
(*gp)++; // NORACE
return NULL;
}

void *a(void *arg) {
pthread_t id;
pthread_create(&id, NULL, b, arg);
return NULL;
}

int main() {
pthread_t id, id2;
pthread_create(&id, NULL, b, NULL);
g++; // NORACE
pthread_create(&id2, NULL, a, &g);
return 0;
}
27 changes: 27 additions & 0 deletions tests/regression/53-races-mhp/05-not-created3.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
#include <pthread.h>

int g;

void *a(void *arg) {
int *gp = arg;
if (gp)
(*gp)++; // RACE (self-race in non-unique thread)
return NULL;
}

void *b(void *arg) {
pthread_t id, id2;
pthread_create(&id, NULL, a, NULL);
pthread_create(&id2, NULL, a, &g);
return NULL;
}


int main() {
pthread_t id, id2;
pthread_create(&id, NULL, a, NULL);
g++; // NORACE
pthread_create(&id2, NULL, b, NULL);
return 0;
}
36 changes: 36 additions & 0 deletions tests/regression/53-races-mhp/06-not-created4.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
#include <pthread.h>

int g;

void *d(void *arg) {
int *gp = arg;
if (gp)
(*gp)++; // RACE (self-race in non-unique thread)
return NULL;
}

void *c(void *arg) {
pthread_t id, id2;
pthread_create(&id, NULL, d, NULL);
pthread_create(&id2, NULL, d, &g);
return NULL;
}

void *b(void *arg) {
return NULL;
}

void *a(void *arg) {
pthread_t id, id2;
pthread_create(&id, NULL, b, NULL);
g++; // NORACE
pthread_create(&id2, NULL, c, NULL);
return NULL;
}

int main() {
pthread_t id;
pthread_create(&id, NULL, a, NULL);
return 0;
}
27 changes: 27 additions & 0 deletions tests/regression/53-races-mhp/07-not-created5.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
#include <pthread.h>

int g;

void *a(void *arg) {
int *gp = arg;
if (gp)
(*gp)++; // RACE (self-race in non-unique thread)
return NULL;
}

void *b(void *arg) {
pthread_t id, id2;
pthread_create(&id, NULL, a, NULL);
pthread_create(&id2, NULL, a, &g);
return NULL;
}

int main() {
pthread_t id, id2, id3;
pthread_create(&id, NULL, a, NULL);
pthread_create(&id, NULL, a, NULL);
g++; // NORACE
pthread_create(&id, NULL, b, NULL);
return 0;
}
31 changes: 31 additions & 0 deletions tests/regression/53-races-mhp/08-not-created6.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
#include <pthread.h>

int g;

void *b(void *arg) {
return NULL;
}

void *c(void *arg) {
int *gp = arg;
if (gp)
(*gp)++; // RACE (self-race in non-unique thread)
return NULL;
}

void *a(void *arg) {
pthread_t id, id2, id3, id4;
pthread_create(&id, NULL, b, NULL);
pthread_create(&id2, NULL, b, NULL);
g++; // NORACE
pthread_create(&id, NULL, c, NULL);
pthread_create(&id2, NULL, c, &g);
return NULL;
}

int main() {
pthread_t id;
pthread_create(&id, NULL, a, NULL);
return 0;
}
Loading
Loading