Get rid of custom event

goblint · Jan 29, 2024 · 2dd7aa0 · 2dd7aa0
1 parent 55dacde
commit 2dd7aa0
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 12 deletions.
diff --git 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
@@ -21,18 +21,24 @@ 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 () [];
       raise Analyses.Deadcode
     | 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
@@ -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
@@ -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