Use AddressDomain for MayPointTo and ReachableFrom queries

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

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? *)

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)
-          | _ -> 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

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

src/analyses/malloc_null.ml

@@ -99,7 +99,7 @@ struct
         | ad when not (Queries.AD.is_top ad) ->
           let to_extra addr ads =
             match addr with
-            | Queries.AD.Addr.Addr mval -> AD.of_mval mval :: ads
+            | Queries.AD.Addr.Addr mval -> AD.of_mval mval :: ads (* TODO: why list of singleton AD-s? *)
             | _ -> ads
           in
           Queries.AD.fold to_extra ad []

src/analyses/memLeak.ml

@@ -57,7 +57,7 @@ struct
             | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.singleton v
             | _ -> D.empty ()
           in
-          D.diff state unique_pointed_to_heap_vars
+          D.diff state unique_pointed_to_heap_vars (* TODO: use D.remove instead of diffing singleton *)
         | _ -> state
       end
     | Abort ->

src/analyses/mutexTypeAnalysis.ml

@@ -18,7 +18,7 @@ struct
   module O = Offset.Unit
 
   module V = struct
-    include Printable.Prod(CilType.Varinfo)(O)
+    include Printable.Prod(CilType.Varinfo)(O) (* TODO: use Mval.Unit *)
     let is_write_only _ = false
   end
 
@@ -56,7 +56,7 @@ struct
       let attr = ctx.ask (Queries.EvalMutexAttr attr) in
       let mutexes = ctx.ask (Queries.MayPointTo mutex) in
       (* It is correct to iter over these sets here, as mutexes need to be intialized before being used, and an analysis that detects usage before initialization is a different analysis. *)
-      Queries.AD.iter (function addr -> 
+      Queries.AD.iter (function addr ->
         match addr with
         | Queries.AD.Addr.Addr (v,o) -> ctx.sideg (v,O.of_offs o) attr
         | _ -> ()

src/analyses/poisonVariables.ml

@@ -103,7 +103,7 @@ struct
         | ad ->
           Queries.AD.fold (fun addr vs ->
               match addr with
-              | Queries.AD.Addr.Addr (v,o) -> rem_mval vs (v, ValueDomain.Offs.to_exp o)
+              | Queries.AD.Addr.Addr (v,o) -> rem_mval vs (v, ValueDomain.Offs.to_exp o) (* TODO: use unconverted addrs in domain? *)
               | _ -> vs
             ) ad ctx.local
       end

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 *)
 

src/analyses/taintPartialContexts.ml

@@ -12,7 +12,7 @@ let to_mvals ad =
   (* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *)
   Queries.AD.fold (fun addr mvals ->
       match addr with
-      | Queries.AD.Addr.Addr (v,o) -> D.add (v, ValueDomain.Offs.to_exp o) mvals
+      | Queries.AD.Addr.Addr (v,o) -> D.add (v, ValueDomain.Offs.to_exp o) mvals (* TODO: use unconverted addrs in domain? *)
       | _ -> mvals
     ) ad (D.empty ())
 

src/analyses/uninit.ml

@@ -198,7 +198,7 @@ struct
         | ad when not (Queries.AD.is_top ad) ->
           let to_extra ad ads =
             match ad with
-            | Queries.AD.Addr.Addr mval -> AD.of_mval mval :: ads
+            | Queries.AD.Addr.Addr mval -> AD.of_mval mval :: ads (* TODO: why list of singleton AD-s? *)
             | _ -> ads
           in
           Queries.AD.fold to_extra ad []

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]
     )
 

src/analyses/varEq.ml

@@ -258,7 +258,7 @@ struct
         if Queries.AD.is_top aad
         then false
         else Queries.AD.exists (function
-            | Addr (u,s) -> CilType.Varinfo.equal v u && oleq o (Addr.Offs.to_exp s)
+            | Addr (u,s) -> CilType.Varinfo.equal v u && oleq o (Addr.Offs.to_exp s) (* TODO: avoid conversion? *)
             | _ -> false
           ) aad
       in
@@ -298,7 +298,7 @@ struct
       else if Queries.AD.is_top bad
       then ((*Messages.warn ~category:Analyzer "No PT-set: switching to types ";*) type_may_change_apt a )
       else Queries.AD.exists (function
-          | Addr (v,o) -> lval_may_change_pt a (v, Addr.Offs.to_exp o)
+          | Addr (v,o) -> lval_may_change_pt a (v, Addr.Offs.to_exp o) (* TODO: avoid conversion? *)
           | _ -> false
         ) bad
     in

src/cdomains/addressDomain.ml

@@ -440,4 +440,6 @@ struct
     let r = narrow x y in
     if M.tracing then M.traceu "ad" "-> %a\n" pretty r;
     r
+
+  let filter f ad = fold (fun addr ad -> if f addr then add addr ad else ad) ad (empty ())
 end