Merge pull request #1144 from goblint/queries-ad-cont

Use `AddressDomain` for queries

Author: sim642

src/analyses/base.ml

@@ -1097,20 +1097,15 @@ struct
     | Int x -> ValueDomain.ID.to_int x
     | _ -> None
 
-  let eval_funvar ctx fval: varinfo list =
-    let exception OnlyUnknown in
-    try
-      let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
-      if AD.mem Addr.UnknownPtr fp then begin
-        let others = AD.to_var_may fp in
-        if others = [] then raise OnlyUnknown;
-        M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval;
-        dummyFunDec.svar :: others
-      end else
-        AD.to_var_may fp
-    with SetDomain.Unsupported _ | OnlyUnknown ->
-      M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval;
-      [dummyFunDec.svar]
+  let eval_funvar ctx fval: Queries.AD.t =
+    let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
+    if AD.is_top fp then (
+      if AD.cardinal fp = 1 then
+        M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval
+      else
+        M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval
+    );
+    fp
 
   (** Evaluate expression as address.
       Avoids expensive Apron EvalInt if the Int result would be useless to us anyway. *)
@@ -1204,10 +1199,7 @@ struct
   let query ctx (type a) (q: a Q.t): a Q.result =
     match q with
     | Q.EvalFunvar e ->
-      begin
-        let fs = eval_funvar ctx e in
-        List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs
-      end
+      eval_funvar ctx e
     | Q.EvalJumpBuf e ->
       begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
         | Address jmp_buf ->
@@ -2411,34 +2403,38 @@ struct
     in
     if get_bool "sem.noreturn.dead_code" && Cil.hasAttribute "noreturn" f.vattr then raise Deadcode else st
 
-  let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : Q.LS.t) : store =
+  let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : AD.t) : store =
     let ask = (Analyses.ask_of_ctx ctx) in
-    Q.LS.fold (fun (v, o) st ->
-        if CPA.mem v fun_st.cpa then
-          let lval = Mval.Exp.to_cil (v,o) in
-          let address = eval_lv ask ctx.global st lval in
-          let lval_type = (AD.type_of address) in
-          if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Mval.Exp.pretty (v, o) d_type lval_type;
-          match (CPA.find_opt v (fun_st.cpa)), lval_type with
-          | None, _ -> st
-          (* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *)
-          | Some (Array a), _ when (CArrays.domain_of_t a) = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa}
-          (* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *)
-          | Some voidVal, TVoid _ -> {st with cpa = CPA.add v voidVal st.cpa}
-          | _, _ -> begin
-              let new_val = get ask ctx.global fun_st address None in
-              if M.tracing then M.trace "taintPC" "update val: %a\n\n" VD.pretty new_val;
-              let st' = set_savetop ~ctx ask ctx.global st address lval_type new_val in
-              let partDep = Dep.find_opt v fun_st.deps in
-              match partDep with
-              | None -> st'
-              (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
-              | Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in
-                                                                match val_opt with
-                                                                | None -> accCPA
-                                                                | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)}
-            end
-        else st) tainted_lvs local_st
+    AD.fold (fun addr st ->
+        match addr with
+        | Addr.Addr (v,o) ->
+          if CPA.mem v fun_st.cpa then
+            let lval = Addr.Mval.to_cil (v,o) in
+            let address = eval_lv ask ctx.global st lval in
+            let lval_type = Addr.type_of addr in
+            if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Addr.Mval.pretty (v,o) d_type lval_type;
+            match (CPA.find_opt v (fun_st.cpa)), lval_type with
+            | None, _ -> st
+            (* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *)
+            | Some (Array a), _ when (CArrays.domain_of_t a) = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa}
+            (* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *)
+            | Some voidVal, TVoid _ -> {st with cpa = CPA.add v voidVal st.cpa}
+            | _, _ -> begin
+                let new_val = get ask ctx.global fun_st address None in
+                if M.tracing then M.trace "taintPC" "update val: %a\n\n" VD.pretty new_val;
+                let st' = set_savetop ~ctx ask ctx.global st address lval_type new_val in
+                let partDep = Dep.find_opt v fun_st.deps in
+                match partDep with
+                | None -> st'
+                (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
+                | Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in
+                                                                  match val_opt with
+                                                                  | None -> accCPA
+                                                                  | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)}
+              end
+          else st
+        | _ -> st
+      ) tainted_lvs local_st
 
   let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
     let combine_one (st: D.t) (fun_st: D.t) =
@@ -2453,9 +2449,9 @@ struct
         let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in
         let ask = (Analyses.ask_of_ctx ctx) in
         let tainted = f_ask.f Q.MayBeTainted in
-        if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname Q.LS.pretty tainted;
+        if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname AD.pretty tainted;
         if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
-        if Q.LS.is_top tainted then
+        if AD.is_top tainted then
           let cpa_local = CPA.filter (fun x _ -> not (is_global ask x)) st.cpa in
           let cpa' = CPA.fold CPA.add cpa_noreturn cpa_local in (* add cpa_noreturn to cpa_local *)
           if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty cpa';
@@ -2470,7 +2466,10 @@ struct
           let cpa_caller' = CPA.fold CPA.add cpa_new cpa_caller in
           if M.tracing then M.trace "taintPC" "cpa_caller': %a\n" CPA.pretty cpa_caller';
           (* remove lvals from the tainted set that correspond to variables for which we just added a new mapping from the callee*)
-          let tainted = Q.LS.filter (fun (v, _) ->  not (CPA.mem v cpa_new)) tainted in
+          let tainted = AD.filter (function
+              | Addr.Addr (v,_) -> not (CPA.mem v cpa_new)
+              | _ -> false
+            ) tainted in
           let st_combined = combine_st ctx {st with cpa = cpa_caller'} fun_st tainted in
           if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty st_combined.cpa;
           { fun_st with cpa = st_combined.cpa }

src/analyses/commonPriv.ml

@@ -60,14 +60,10 @@ struct
     ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection})
 
   let protected_vars (ask: Q.ask): varinfo list =
-    let module VS = Set.Make (CilType.Varinfo) in
-    Q.LS.fold (fun (v, _) acc ->
-        let m = ValueDomain.Addr.of_var v in (* TODO: don't ignore offsets *)
-        Q.LS.fold (fun l acc ->
-            VS.add (fst l) acc (* always `NoOffset from mutex analysis *)
-          ) (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
-      ) (ask.f Q.MustLockset) VS.empty
-    |> VS.elements
+    Q.AD.fold (fun m acc ->
+        Q.VS.join (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
+      ) (ask.f Q.MustLockset) (Q.VS.empty ())
+    |> Q.VS.elements
 end
 
 module MutexGlobals =
@@ -126,10 +122,8 @@ struct
     if !AnalysisState.global_initialization then
       Lockset.empty ()
     else
-      let ls = ask.f Queries.MustLockset in
-      Q.LS.fold (fun (var, offs) acc ->
-          Lockset.add (Lock.of_mval (var, Lock.Offs.of_exp offs)) acc
-        ) ls (Lockset.empty ())
+      let ad = ask.f Queries.MustLockset in
+      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 *)

src/analyses/modifiedSinceLongjmp.ml

@@ -23,29 +23,23 @@ struct
     (* Only checks for v.vglob on purpose, acessing espaced locals after longjmp is UB like for any local *)
     not v.vglob (* *) && not (BaseUtil.is_volatile v) && v.vstorage <> Static
 
-  let relevants_from_ls ls =
-    if Queries.LS.is_top ls then
-      VS.top ()
-    else
-      Queries.LS.fold (fun (v, _) acc -> if is_relevant v then VS.add v acc else acc) ls (VS.empty ())
-
-  let relevants_from_ad ad =
+  let relevants_from_ad ls =
     (* TODO: what about AD with both known and unknown pointers? *)
-    if Queries.AD.is_top ad then
+    if Queries.AD.is_top ls then
       VS.top ()
     else
-      Queries.AD.fold (fun addr vs ->
+      Queries.AD.fold (fun addr acc ->
           match addr with
-          | Queries.AD.Addr.Addr (v,_) -> if is_relevant v then VS.add v vs else vs
-          | _ -> vs
-        ) ad (VS.empty ())
+          | Queries.AD.Addr.Addr (v, _) when is_relevant v -> VS.add v acc
+          | _ -> acc
+        ) ls (VS.empty ())
 
   (* transfer functions *)
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, D.bot ()] (* enter with bot as opposed to IdentitySpec *)
 
   let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
-    let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTainted) in
+    let taintedcallee = relevants_from_ad (f_ask.f Queries.MayBeTainted) in
     add_to_all_defined taintedcallee ctx.local
 
   let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask) : D.t =

src/analyses/mutexAnalysis.ml

@@ -233,21 +233,15 @@ struct
       Mutexes.leq mutex_lockset protecting
     | Queries.MustLockset ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
-      let ls = Mutexes.fold (fun addr ls ->
-          match Addr.to_mval addr with
-          | Some (var, offs) -> Queries.LS.add (var, Addr.Offs.to_exp offs) ls
-          | None -> ls
-        ) held_locks (Queries.LS.empty ())
-      in
-      ls
+      Mutexes.fold (fun addr ls -> Queries.AD.add addr ls) held_locks (Queries.AD.empty ())
     | Queries.MustBeAtomic ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
       Mutexes.mem (LockDomain.Addr.of_var LF.verifier_atomic_var) held_locks
     | Queries.MustProtectedVars {mutex = m; write} ->
       let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in
       VarSet.fold (fun v acc ->
-          Queries.LS.add (v, `NoOffset) acc
-        ) protected (Queries.LS.empty ())
+          Queries.VS.add v acc
+        ) protected (Queries.VS.empty ())
     | Queries.IterSysVars (Global g, f) ->
       f (Obj.repr (V.protecting g)) (* TODO: something about V.protected? *)
     | WarnGlobal g ->

src/analyses/poisonVariables.ml

@@ -15,12 +15,16 @@ struct
 
   let context _ _ = ()
 
-  let check_mval tainted ((v, offset): Queries.LS.elt) =
-    if not v.vglob && VS.mem v tainted then
-      M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v
+  let check_mval tainted (addr: Queries.AD.elt) =
+    match addr with
+    | Queries.AD.Addr.Addr (v,_) ->
+      if not v.vglob && VS.mem v tainted then
+        M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v
+    | _ -> ()
 
-  let rem_mval tainted ((v, offset): Queries.LS.elt) = match offset with
-    | `NoOffset -> VS.remove v tainted
+  let rem_mval tainted (addr: Queries.AD.elt) =
+    match addr with
+    | Queries.AD.Addr.Addr (v,`NoOffset) -> VS.remove v tainted
     | _ -> tainted (* If there is an offset, it is a bit harder to remove, as we don't know where the indeterminate value is *)
 
 
@@ -88,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 (v, ValueDomain.Offs.to_exp 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; _} ->
@@ -102,9 +103,7 @@ struct
           ctx.local
         | 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) (* TODO: use unconverted addrs in domain? *)
-              | _ -> vs
+              rem_mval vs addr
             ) ad ctx.local
       end
     | _ -> ctx.local

src/analyses/taintPartialContexts.ml

@@ -6,31 +6,19 @@
 open GoblintCil
 open Analyses
 
-module D = SetDomain.ToppedSet (Mval.Exp) (struct let topname = "All" end)
-
-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 (* TODO: use unconverted addrs in domain? *)
-      | _ -> mvals
-    ) ad (D.empty ())
+module AD = ValueDomain.AD
 
 module Spec =
 struct
   include Analyses.IdentitySpec
 
   let name () = "taintPartialContexts"
-  module D = D
+  module D = AD
   module C = Lattice.Unit
 
   (* Add Lval or any Lval which it may point to to the set *)
   let taint_lval ctx (lval:lval) : D.t =
-    let d = ctx.local in
-    (match lval with
-     | (Var v, offs) -> D.add (v, Offset.Exp.of_cil offs) d
-     | (Mem e, _) -> D.union (to_mvals (ctx.ask (Queries.MayPointTo e))) d
-    )
+    D.union (ctx.ask (Queries.MayPointTo (AddrOf lval))) ctx.local
 
   (* this analysis is context insensitive*)
   let context _ _ = ()
@@ -45,14 +33,12 @@ struct
     let d_return =
       if D.is_top d then
         d
-      else (
+      else
         let locals = f.sformals @ f.slocals in
-        D.filter (fun (v, _) ->
-            not (List.exists (fun local ->
-                CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))
-              ) locals)
+        D.filter (function
+            | AD.Addr.Addr (v,_) -> not (List.exists (fun local -> CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))) locals)
+            | _ -> false
           ) d
-      )
     in
     if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a\n" f.svar.vname D.pretty d D.pretty d_return;
     d_return
@@ -94,9 +80,10 @@ struct
       else
         deep_addrs
     in
-    let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.MayPointTo addr)))) d shallow_addrs
+    (* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *)
+    let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.MayPointTo addr))) d shallow_addrs
     in
-    let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.ReachableFrom addr)))) d deep_addrs
+    let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.ReachableFrom addr))) d deep_addrs
     in
     d
 
@@ -111,7 +98,7 @@ struct
 
   let query ctx (type a) (q: a Queries.t) : a Queries.result =
     match q with
-    | MayBeTainted -> (ctx.local : Queries.LS.t)
+    | MayBeTainted -> (ctx.local : Queries.AD.t)
     | _ -> Queries.Result.top q
 
 end
@@ -122,5 +109,8 @@ let _ =
 module VS = SetDomain.ToppedSet(Basetype.Variables) (struct let topname = "All" end)
 
 (* Convert Lval set to (less precise) Varinfo set. *)
-let conv_varset (lval_set : Spec.D.t) : VS.t =
-  if Spec.D.is_top lval_set then VS.top () else VS.of_list (List.map (fun (v, _) -> v) (Spec.D.elements lval_set))
+let conv_varset (addr_set : Spec.D.t) : VS.t =
+  if Spec.D.is_top addr_set then
+    VS.top ()
+  else
+    VS.of_list (Spec.D.to_var_may addr_set)

src/analyses/varEq.ml

@@ -437,10 +437,14 @@ struct
     let d_local =
       (* if we are multithreaded, we run the risk, that some mutex protected variables got unlocked, so in this case caller state goes to top
          TODO: !!Unsound, this analysis does not handle this case -> regtest 63 08!! *)
-      if Queries.LS.is_top tainted || not (ctx.ask (Queries.MustBeSingleThreaded {since_start = true})) then
+      if Queries.AD.is_top tainted || not (ctx.ask (Queries.MustBeSingleThreaded {since_start = true})) then
         D.top ()
       else
-        let taint_exp = Queries.ES.of_list (List.map Mval.Exp.to_cil_exp (Queries.LS.elements tainted)) in
+        let taint_exp =
+          Queries.AD.to_mval tainted
+          |> List.map Addr.Mval.to_cil_exp
+          |> Queries.ES.of_list
+        in
         D.filter (fun exp -> not (Queries.ES.mem exp taint_exp)) ctx.local
     in
     let d = D.meet au d_local in

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