From 880d59f91c2d47d7d6337d4edb7c0a314c753dca Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 27 Jan 2024 23:36:50 +0100 Subject: [PATCH 1/5] Refine Points-To set on locking a mutex --- src/analyses/base.ml | 5 +++++ src/analyses/mutexEventsAnalysis.ml | 4 ++-- src/domains/events.ml | 5 ++++- tests/regression/79-mutex2/01-split.c | 20 ++++++++++++++++++++ 4 files changed, 31 insertions(+), 3 deletions(-) create mode 100644 tests/regression/79-mutex2/01-split.c diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 42e43b623a..c20fb71447 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2929,6 +2929,11 @@ struct {st' with cpa = CPA.remove !longjmp_return st'.cpa} | None -> ctx.local end + | Events.RefinePointerExp {exp; ad} -> + (match exp with + | Lval lval -> + set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOf exp) (Address ad) + | _ -> ctx.local) | _ -> ctx.local end diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 162527b32b..84190e6df4 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -24,7 +24,7 @@ struct match lv_opt with | None -> Queries.AD.iter (fun e -> - ctx.split () [Events.Lock (e, rw)] + ctx.split () [Events.Lock (e, rw); Events.RefinePointerExp {exp = arg; ad = Queries.AD.singleton e}] ) (eval_exp_addr a arg); if may_fail then ctx.split () []; @@ -32,7 +32,7 @@ struct | Some lv -> let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in Queries.AD.iter (fun e -> - ctx.split () [sb; Events.Lock (e, rw)]; + ctx.split () [sb; Events.Lock (e, rw); Events.RefinePointerExp {exp = arg; ad = Queries.AD.singleton e}]; ) (eval_exp_addr a arg); if may_fail then ( let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in diff --git a/src/domains/events.ml b/src/domains/events.ml index 06561bddbe..78fedeafa2 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -16,6 +16,7 @@ type t = | Assert of exp | Unassume of {exp: CilType.Exp.t; uuids: string list} | Longjmped of {lval: CilType.Lval.t option} + | RefinePointerExp of {exp: CilType.Exp.t; ad: ValueDomain.AD.t} (** Should event be emitted after transfer function raises [Deadcode]? *) let emit_on_deadcode = function @@ -31,7 +32,8 @@ let emit_on_deadcode = function | UpdateExpSplit _ (* Pointless to split on dead. *) | Unassume _ (* Avoid spurious writes. *) | Assert _ (* Pointless to refine dead. *) - | Longjmped _ -> + | Longjmped _ + | RefinePointerExp _ -> false let pretty () = function @@ -47,3 +49,4 @@ let pretty () = function | Assert exp -> dprintf "Assert %a" d_exp exp | Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval + | RefinePointerExp {exp; ad} -> dprintf "RefinePointerExp {exp=%a; ad=%a}" CilType.Exp.pretty exp ValueDomain.AD.pretty ad \ No newline at end of file diff --git a/tests/regression/79-mutex2/01-split.c b/tests/regression/79-mutex2/01-split.c new file mode 100644 index 0000000000..0ca07f5b4d --- /dev/null +++ b/tests/regression/79-mutex2/01-split.c @@ -0,0 +1,20 @@ +#include + +pthread_mutex_t m1; +pthread_mutex_t m2; + +int main(int argc, char const *argv[]) +{ + int top; + pthread_mutex_t* ptr; + ptr = &m1; + + if(top) { + ptr = &m2; + } + + pthread_mutex_lock(ptr); + pthread_mutex_unlock(ptr); //NOWARN + + return 0; +} \ No newline at end of file From 036bbc6057efbab7cc40f93ae209a2a793a1012f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 27 Jan 2024 23:40:58 +0100 Subject: [PATCH 2/5] Indentation --- src/analyses/base.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c20fb71447..fbd169d1ca 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2931,9 +2931,9 @@ struct end | Events.RefinePointerExp {exp; ad} -> (match exp with - | Lval lval -> - set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOf exp) (Address ad) - | _ -> ctx.local) + | Lval lval -> + set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOf exp) (Address ad) + | _ -> ctx.local) | _ -> ctx.local end From 55dacde527593460dafc4fd1c41ad1b9463edd9c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 27 Jan 2024 23:45:01 +0100 Subject: [PATCH 3/5] Add multithreaded example --- tests/regression/79-mutex2/02-split-mt.c | 37 ++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 tests/regression/79-mutex2/02-split-mt.c diff --git a/tests/regression/79-mutex2/02-split-mt.c b/tests/regression/79-mutex2/02-split-mt.c new file mode 100644 index 0000000000..9e397f9c2e --- /dev/null +++ b/tests/regression/79-mutex2/02-split-mt.c @@ -0,0 +1,37 @@ +#include + +pthread_mutex_t m1; +pthread_mutex_t m2; +pthread_mutex_t* ptr; + +void other() { + int top; + ptr = &m2; + + if(top) { + ptr = &m1; + } +} + +int main(int argc, char const *argv[]) +{ + int top; + + ptr = &m1; + + if(top) { + ptr = &m2; + } + + pthread_t mischievous; + pthread_create(&mischievous, NULL, other, NULL); + + + pthread_mutex_lock(ptr); + + // This has to produce a warning, as the other thread may have changed what + // ptr points to such that it's not the same mutex being unlocked here. + pthread_mutex_unlock(ptr); //WARN + + return 0; +} \ No newline at end of file From c27f1bd6d6138d0eb4afc8692b736da5a51eeeeb Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 29 Jan 2024 13:09:16 +0100 Subject: [PATCH 4/5] Get rid of custom event --- src/analyses/base.ml | 5 ----- src/analyses/mutexEventsAnalysis.ml | 10 ++++++++-- src/domains/events.ml | 5 +---- 3 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index fbd169d1ca..42e43b623a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2929,11 +2929,6 @@ struct {st' with cpa = CPA.remove !longjmp_return st'.cpa} | None -> ctx.local end - | Events.RefinePointerExp {exp; ad} -> - (match exp with - | Lval lval -> - set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOf exp) (Address ad) - | _ -> ctx.local) | _ -> ctx.local end diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 84190e6df4..7f544b0ffd 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -21,10 +21,16 @@ struct let eval_exp_addr (a: Queries.ask) exp = a.f (Queries.MayPointTo exp) let lock ctx rw may_fail nonzero_return_when_aquired a lv_opt arg = + let compute_refine_split (e:Mutexes.elt) = match e with + | Addr a -> + let e' = BinOp(Eq, arg, AddrOf ((PreValueDomain.Mval.to_cil a)), intType) in + [Events.SplitBranch (e',true)] + | _ -> [] + in match lv_opt with | None -> Queries.AD.iter (fun e -> - ctx.split () [Events.Lock (e, rw); Events.RefinePointerExp {exp = arg; ad = Queries.AD.singleton e}] + ctx.split () (Events.Lock (e, rw) :: compute_refine_split e) ) (eval_exp_addr a arg); if may_fail then ctx.split () []; @@ -32,7 +38,7 @@ struct | Some lv -> let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in Queries.AD.iter (fun e -> - ctx.split () [sb; Events.Lock (e, rw); Events.RefinePointerExp {exp = arg; ad = Queries.AD.singleton e}]; + ctx.split () (sb :: Events.Lock (e, rw) :: compute_refine_split e); ) (eval_exp_addr a arg); if may_fail then ( let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in diff --git a/src/domains/events.ml b/src/domains/events.ml index 78fedeafa2..06561bddbe 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -16,7 +16,6 @@ type t = | Assert of exp | Unassume of {exp: CilType.Exp.t; uuids: string list} | Longjmped of {lval: CilType.Lval.t option} - | RefinePointerExp of {exp: CilType.Exp.t; ad: ValueDomain.AD.t} (** Should event be emitted after transfer function raises [Deadcode]? *) let emit_on_deadcode = function @@ -32,8 +31,7 @@ let emit_on_deadcode = function | UpdateExpSplit _ (* Pointless to split on dead. *) | Unassume _ (* Avoid spurious writes. *) | Assert _ (* Pointless to refine dead. *) - | Longjmped _ - | RefinePointerExp _ -> + | Longjmped _ -> false let pretty () = function @@ -49,4 +47,3 @@ let pretty () = function | Assert exp -> dprintf "Assert %a" d_exp exp | Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval - | RefinePointerExp {exp; ad} -> dprintf "RefinePointerExp {exp=%a; ad=%a}" CilType.Exp.pretty exp ValueDomain.AD.pretty ad \ No newline at end of file From 3e9d7f165401fcf46745a3fad3cf91c4583e01ec Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 29 Jan 2024 14:35:23 +0100 Subject: [PATCH 5/5] Move to pre-existing folder --- tests/regression/{79-mutex2/01-split.c => 04-mutex/96-split.c} | 0 .../{79-mutex2/02-split-mt.c => 04-mutex/97-split-mt.c} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/{79-mutex2/01-split.c => 04-mutex/96-split.c} (100%) rename tests/regression/{79-mutex2/02-split-mt.c => 04-mutex/97-split-mt.c} (100%) diff --git a/tests/regression/79-mutex2/01-split.c b/tests/regression/04-mutex/96-split.c similarity index 100% rename from tests/regression/79-mutex2/01-split.c rename to tests/regression/04-mutex/96-split.c diff --git a/tests/regression/79-mutex2/02-split-mt.c b/tests/regression/04-mutex/97-split-mt.c similarity index 100% rename from tests/regression/79-mutex2/02-split-mt.c rename to tests/regression/04-mutex/97-split-mt.c