From 2dd7aa0fbff6c182a23c9a4e8302f05b0501e21b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 29 Jan 2024 13:09:16 +0100 Subject: [PATCH] Get rid of custom event --- src/analyses/base.ml | 5 ----- src/analyses/mutexEventsAnalysis.ml | 10 ++++++++-- src/cdomains/apron/sharedFunctions.apron.ml | 2 +- src/domains/events.ml | 5 +---- 4 files changed, 10 insertions(+), 12 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index fbd169d1ca0..42e43b623ae 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 84190e6df4b..7f544b0ffda 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/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index e66be00ae46..4a237be1877 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -103,7 +103,7 @@ struct match exp with | UnOp (Neg, e, _) -> Unop (Neg, texpr1_expr_of_cil_exp e, Int, Near) - | BinOp (PlusA, e1, e2, _) -> + | BinOp ((PlusA|MinusA) as op, e1, e2, _) -> Binop (Add, texpr1_expr_of_cil_exp e1, texpr1_expr_of_cil_exp e2, Int, Near) | BinOp (MinusA, e1, e2, _) -> Binop (Sub, texpr1_expr_of_cil_exp e1, texpr1_expr_of_cil_exp e2, Int, Near) diff --git a/src/domains/events.ml b/src/domains/events.ml index 78fedeafa22..5442ec74803 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