Simplify some AddressDomain query result manipulation

goblint · Sep 11, 2023 · 7edb312 · 7edb312
1 parent c8cc6c4
commit 7edb312
Show file tree

Hide file tree

Showing 6 changed files with 22 additions and 44 deletions.
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
@@ -276,7 +276,7 @@ struct
   let reachable_from_args ctx args =
     let to_vs e =
       ctx.ask (ReachableFrom e)
-      |> LockDomain.MayLocksetNoRW.to_var_may
+      |> Queries.AD.to_var_may
       |> VS.of_list
     in
     List.fold (fun vs e -> VS.join vs (to_vs e)) (VS.empty ()) args

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -1319,8 +1319,8 @@ struct
           (* ignore @@ printf "EvalStr Address: %a -> %s (must %i, may %i)\n" d_plainexp e (VD.short 80 (Address a)) (List.length @@ AD.to_var_must a) (List.length @@ AD.to_var_may a); *)
           begin match unrollType (Cilfacade.typeOf e) with
             | TPtr(TInt(IChar, _), _) ->
-              let (v,o) = List.hd (AD.to_mval a) in
-              let lval = Mval.Exp.to_cil @@ (v, Addr.Offs.to_exp o) in
+              let mval = List.hd (AD.to_mval a) in
+              let lval = Addr.Mval.to_cil mval in
               (try `Lifted (Bytes.to_string (Hashtbl.find char_array lval))
                with Not_found -> Queries.Result.top q)
             | _ -> (* what about ISChar and IUChar? *)

diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
@@ -64,18 +64,16 @@ struct
   let (>?) = Option.bind
 
   let mayPointTo ctx exp =
-    match ctx.ask (Queries.MayPointTo exp) with
-    | ad when not (Queries.AD.is_top ad) && not (Queries.AD.is_empty ad) ->
-      let a' = if Queries.AD.mem UnknownPtr ad then (
-          M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
-          Queries.AD.remove UnknownPtr ad
-        ) else ad
-      in
-      List.filter_map (function
-          | ValueDomain.Addr.Addr (v,o) -> Some (v, ValueDomain.Addr.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *)
-          | _ -> None
-        ) (Queries.AD.elements a')
-    | _ -> []
+    let ad = ctx.ask (Queries.MayPointTo exp) in
+    let a' = if Queries.AD.mem UnknownPtr ad then (
+        M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
+        Queries.AD.remove UnknownPtr ad
+      ) else ad
+    in
+    List.filter_map (function
+        | ValueDomain.Addr.Addr (v,o) -> Some (v, ValueDomain.Addr.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *)
+        | _ -> None
+      ) (Queries.AD.elements a')
 
   let mustPointTo ctx exp = (* this is just to get Mval.Exp *)
     match mayPointTo ctx exp with

diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
@@ -877,16 +877,9 @@ module Spec : Analyses.MCPSpec = struct
 
   module ExprEval = struct
     let eval_ptr ctx exp =
-      let ad = ctx.ask (Queries.MayPointTo exp) in
-      if (not (Queries.AD.is_top ad)) && not (Queries.AD.is_empty ad) then
-        if Queries.AD.mem UnknownPtr ad
-        then (* UNSOUND *)
-          Queries.AD.remove UnknownPtr ad
-          |> Queries.AD.to_var_may
-        else
-          Queries.AD.to_var_may ad
-      else
-        []
+      ctx.ask (Queries.MayPointTo exp)
+      |> Queries.AD.remove UnknownPtr
+      |> Queries.AD.to_var_may
 
     let eval_var ctx exp =
       match exp with
@@ -1126,11 +1119,7 @@ module Spec : Analyses.MCPSpec = struct
             ad
         in
         let thread_fun =
-          Queries.AD.fold (fun addr vars ->
-              match addr with
-              | Queries.AD.Addr.Addr (v,_) -> v :: vars
-              | _ -> vars
-            ) funs_ad []
+          Queries.AD.to_var_may funs_ad
           |> List.unique ~eq:(fun a b -> a.vid = b.vid)
           |> List.hd
         in
@@ -1255,7 +1244,7 @@ module Spec : Analyses.MCPSpec = struct
     (* TODO: optimize finding *)
     let tasks_f =
       let var_in_ad ad f = Queries.AD.exists (function
-          | Queries.AD.Addr.Addr (ls_f,_) -> ls_f = f
+          | Queries.AD.Addr.Addr (ls_f,_) -> CilType.Varinfo.equal ls_f f
           | _ -> false
         ) ad
       in

diff --git a/src/analyses/pthreadSignals.ml b/src/analyses/pthreadSignals.ml
@@ -17,10 +17,8 @@ struct
   module C = MustSignals
   module G = SetDomain.ToppedSet (MHP) (struct let topname = "All Threads" end)
 
-  let eval_exp_addr (a: Queries.ask) exp = Queries.AD.elements (a.f (Queries.MayPointTo exp))
-
-  let possible_vinfos a cv_arg =
-    List.filter_map ValueDomain.Addr.to_var_may (eval_exp_addr a cv_arg)
+  let possible_vinfos (a: Queries.ask) cv_arg =
+    Queries.AD.to_var_may (a.f (Queries.MayPointTo cv_arg))
 
   (* transfer functions *)
 

diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
@@ -160,15 +160,8 @@ struct
       if Queries.AD.is_top reachable_from_args || D.is_top caller_state then
         [caller_state, caller_state]
       else
-        let reachable_vars =
-          let get_vars addr vars =
-            match addr with
-            | Queries.AD.Addr.Addr (v,_) -> v :: vars
-            | _ -> vars
-          in
-          Queries.AD.fold get_vars reachable_from_args []
-        in
-        let callee_state = D.filter (fun var -> List.mem var reachable_vars) caller_state in
+        let reachable_vars = Queries.AD.to_var_may reachable_from_args in
+        let callee_state = D.filter (fun var -> List.mem var reachable_vars) caller_state in (* TODO: use AD.mem directly *)
         [caller_state, callee_state]
     )