Simplify some AD conversions, add TODOs

goblint · Sep 15, 2023 · cb08d33 · cb08d33
1 parent fb1be83
commit cb08d33
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 14 deletions.
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
@@ -128,7 +128,7 @@ struct
       Lockset.empty ()
     else
       let ad = ask.f Queries.MustLockset in
-      Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ())
+      Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ()) (* TODO: use AD as Lockset *)
 
   (* TODO: reversed SetDomain.Hoare *)
   module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *)

diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
@@ -92,11 +92,8 @@ struct
         | ad when Queries.AD.is_top ad && not (VS.is_empty octx.local) ->
           M.warn ~category:(Behavior (Undefined Other)) "reading unknown memory location, may be tainted!"
         | ad ->
-          Queries.AD.iter (function
-              (* Use original access state instead of current with removed written vars. *)
-              | Queries.AD.Addr.Addr (v,o) -> check_mval octx.local (Queries.AD.Addr.Addr (v,o))
-              | _ -> ()
-            ) ad
+          (* Use original access state instead of current with removed written vars. *)
+          Queries.AD.iter (check_mval octx.local) ad
       end;
       ctx.local
     | Access {ad; kind = Write; _} ->
@@ -106,9 +103,7 @@ struct
           ctx.local
         | ad ->
           Queries.AD.fold (fun addr vs ->
-              match addr with
-              | Queries.AD.Addr.Addr _ -> rem_mval vs addr
-              | _ -> vs
+              rem_mval vs addr
             ) ad ctx.local
       end
     | _ -> ctx.local

diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
@@ -113,4 +113,4 @@ let conv_varset (addr_set : Spec.D.t) : VS.t =
   if Spec.D.is_top addr_set then
     VS.top ()
   else
-    VS.of_list (List.filter_map (fun addr -> Spec.D.Addr.to_var_may addr) (Spec.D.elements addr_set))
+    VS.of_list (Spec.D.to_var_may addr_set)
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
@@ -441,8 +441,7 @@ struct
         D.top ()
       else
         let taint_exp =
-          Queries.AD.elements tainted
-          |> List.filter_map Addr.to_mval
+          Queries.AD.to_mval tainted
           |> List.map Addr.Mval.to_cil_exp
           |> Queries.ES.of_list
         in

diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
@@ -7,7 +7,7 @@ module IdxDom = ValueDomain.IndexDomain
 
 open GoblintCil
 
-module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO HoareDomain? *)
+module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO: AD? *)
 module Simple = Lattice.Reverse (Mutexes)
 module Priorities = IntDomain.Lifted
 

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
@@ -755,7 +755,7 @@ struct
       | _ ->
         (* Depends on base for query. *)
         let ad = ctx.ask (Queries.EvalFunvar e) in
-        List.filter_map (fun addr -> Queries.AD.Addr.to_var addr) (Queries.AD.elements ad)
+        Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *)
     in
     let one_function f =
       match f.vtype with