Use MayPointToA and ReachableFromA in accessAnalysis

Co-authored-by: Simmo Saan <[email protected]>

src/analyses/accessAnalysis.ml

@@ -33,7 +33,7 @@ struct
 
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) =
     if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach;
-    let reach_or_mpt: _ Queries.t = if reach then ReachableFrom e else MayPointTo e in
+    let reach_or_mpt: _ Queries.t = if reach then ReachableFromA e else MayPointToA e in
     let ls = ctx.ask reach_or_mpt in
     ctx.emit (Access {exp=e; lvals=ls; kind; reach})
 
@@ -138,24 +138,19 @@ struct
   let event ctx e octx =
     match e with
     | Events.Access {lvals; kind; _} when !collect_local && !AnalysisState.postsolving ->
-      begin match lvals with
-        | ls when Queries.LS.is_top ls ->
-          let access: AccessDomain.Event.t = {var_opt = None; offs_opt = None; kind} in
-          ctx.sideg ctx.node (G.singleton access)
-        | ls ->
-          let events = Queries.LS.fold (fun (var, offs) acc ->
-              let coffs = Offset.Exp.to_cil offs in
-              let access: AccessDomain.Event.t =
-                if CilType.Varinfo.equal var dummyFunDec.svar then
-                  {var_opt = None; offs_opt = (Some coffs); kind}
-                else
-                  {var_opt = (Some var); offs_opt = (Some coffs); kind}
-              in
-              G.add access acc
-            ) ls (G.empty ())
-          in
-          ctx.sideg ctx.node events
-      end
+      let events = Queries.AD.fold (fun addr acc ->
+          match addr with
+          | Queries.AD.Addr.Addr (var, offs) ->
+            let coffs = Offset.Exp.to_cil (ValueDomain.Offs.to_exp offs) in
+            let access: AccessDomain.Event.t = {var_opt = (Some var); offs_opt = (Some coffs); kind} in
+            G.add access acc
+          | UnknownPtr -> 
+            let access: AccessDomain.Event.t = {var_opt = None; offs_opt = None; kind} in
+            G.add access acc
+          | _ -> acc
+        ) lvals (G.empty ())
+      in
+      ctx.sideg ctx.node events
     | _ ->
       ctx.local
 end

src/analyses/modifiedSinceLongjmp.ml

@@ -29,6 +29,17 @@ struct
     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 ls =
+    (* TODO: what about AD with both known and unknown pointers? *)
+    if Queries.AD.is_top ls then
+      VS.top ()
+    else
+      Queries.AD.fold (fun addr acc -> 
+          match addr with
+          | Queries.AD.Addr.Addr (v, _) -> if is_relevant v then VS.add v acc else 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 *)
@@ -63,7 +74,7 @@ struct
   let event ctx (e: Events.t) octx =
     match e with
     | Access {lvals; kind = Write; _} ->
-      add_to_all_defined (relevants_from_ls lvals) ctx.local
+      add_to_all_defined (relevants_from_ad lvals) ctx.local
     | _ ->
       ctx.local
 end

src/analyses/mutexAnalysis.ml

@@ -296,7 +296,7 @@ struct
     | Events.Access {exp; lvals; kind; _} when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
       let is_recovered_to_st = not (ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx)) in
       (* must use original (pre-assign, etc) ctx queries *)
-      let old_access var_opt offs_opt =
+      let old_access var_opt =
         (* TODO: this used to use ctx instead of octx, why? *)
         (*privatization*)
         match var_opt with
@@ -325,24 +325,22 @@ struct
             )
         | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound."
       in
-      let module LS = Queries.LS in
+      let module AD = Queries.AD in
       let has_escaped g = octx.ask (Queries.MayEscape g) in
-      let on_lvals ls =
-        let ls = LS.filter (fun (g,_) -> g.vglob || has_escaped g) ls in
-        let f (var, offs) =
-          let coffs = Offset.Exp.to_cil offs in
-          if CilType.Varinfo.equal var dummyFunDec.svar then
-            old_access None (Some coffs)
-          else
-            old_access (Some var) (Some coffs)
+      let on_lvals ad =
+        let f addr =
+          match addr with
+          | AD.Addr.Addr (g,o) when g.vglob || has_escaped g -> old_access (Some g)
+          | UnknownPtr -> old_access None
+          | _ -> () 
         in
-        LS.iter f ls
+        AD.iter f ad
       in
       begin match lvals with
-        | ls when not (LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) ls) ->
+        | ad when not (AD.is_top ad) ->
           (* the case where the points-to set is non top and does not contain unknown values *)
-          on_lvals ls
-        | ls when not (LS.is_top ls) ->
+          on_lvals ad
+        | ad ->
           (* the case where the points-to set is non top and contains unknown values *)
           (* now we need to access all fields that might be pointed to: is this correct? *)
           begin match octx.ask (ReachableUkTypes exp) with
@@ -354,11 +352,11 @@ struct
                 | _ -> false
               in
               if Queries.TS.exists f ts then
-                old_access None None
+                old_access None
           end;
-          on_lvals ls
-        | _ ->
-          old_access None None
+          on_lvals ad
+          (* | _ ->
+             old_access None None *)
       end;
       ctx.local
     | _ ->

src/analyses/poisonVariables.ml

@@ -80,23 +80,28 @@ struct
         ) longjmp_nodes;
       D.join modified_locals ctx.local
     | Access {lvals; kind = Read; _} ->
-      if Queries.LS.is_top lvals then (
+      (* TODO: what about AD with both known and unknown pointers? *)
+      if Queries.AD.is_top lvals then (
         if not (VS.is_empty octx.local) then
           M.warn ~category:(Behavior (Undefined Other)) "reading unknown memory location, may be tainted!"
       )
       else (
-        Queries.LS.iter (fun lv ->
+        Queries.AD.iter (function
             (* Use original access state instead of current with removed written vars. *)
-            check_lval octx.local lv
+            | Queries.AD.Addr.Addr (v,o) -> check_lval octx.local (v, ValueDomain.Offs.to_exp o)
+            | _ -> ()
           ) lvals
       );
       ctx.local
     | Access {lvals; kind = Write; _} ->
-      if Queries.LS.is_top lvals then
+      (* TODO: what about AD with both known and unknown pointers? *)
+      if Queries.AD.is_top lvals then
         ctx.local
       else (
-        Queries.LS.fold (fun lv acc ->
-            rem_lval acc lv
+        Queries.AD.fold (fun addr acc ->
+            match addr with
+            | Queries.AD.Addr.Addr (v,o) -> rem_lval acc (v, ValueDomain.Offs.to_exp o)
+            | _ -> acc
           ) lvals ctx.local
       )
     | _ -> ctx.local

src/analyses/raceAnalysis.ml

@@ -134,7 +134,7 @@ struct
     | Events.Access {exp=e; lvals; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
       (* must use original (pre-assign, etc) ctx queries *)
       let conf = 110 in
-      let module LS = Queries.LS in
+      let module AD = Queries.AD in
       let part_access (vo:varinfo option): MCPAccess.A.t =
         (*partitions & locks*)
         Obj.obj (octx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind})))
@@ -151,24 +151,24 @@ struct
       let has_escaped g = octx.ask (Queries.MayEscape g) in
       (* The following function adds accesses to the lval-set ls
          -- this is the common case if we have a sound points-to set. *)
-      let on_lvals ls includes_uk =
-        let ls = LS.filter (fun (g,_) -> g.vglob || has_escaped g) ls in
+      let on_lvals ad includes_uk =
         let conf = if reach then conf - 20 else conf in
         let conf = if includes_uk then conf - 10 else conf in
-        let f (var, offs) =
-          let coffs = Offset.Exp.to_cil offs in
-          if CilType.Varinfo.equal var dummyFunDec.svar then
-            add_access conf None
-          else
-            add_access conf (Some (var, coffs))
+        let f addr =
+          match addr with
+          | AD.Addr.Addr (g,o) when g.vglob || has_escaped g ->
+            let coffs = Offset.Exp.to_cil (ValueDomain.Offs.to_exp o) in
+            add_access conf (Some (g, coffs))
+          | UnknownPtr -> add_access conf None
+          | _ -> () 
         in
-        LS.iter f ls
+        AD.iter f ad
       in
       begin match lvals with
-        | ls when not (LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) ls) ->
+        | ad when not (AD.is_top ad) ->
           (* the case where the points-to set is non top and does not contain unknown values *)
-          on_lvals ls false
-        | ls when not (LS.is_top ls) ->
+          on_lvals ad false
+        | ad ->
           (* the case where the points-to set is non top and contains unknown values *)
           let includes_uk = ref false in
           (* now we need to access all fields that might be pointed to: is this correct? *)
@@ -185,9 +185,9 @@ struct
               in
               Queries.TS.iter f ts
           end;
-          on_lvals ls !includes_uk
-        | _ ->
-          add_access (conf - 60) None
+          on_lvals ad !includes_uk
+          (* | _ ->
+             add_access (conf - 60) None *)
       end;
       ctx.local
     | _ ->

src/domains/events.ml

@@ -10,7 +10,7 @@ type t =
   | EnterMultiThreaded
   | SplitBranch of exp * bool (** Used to simulate old branch-based split. *)
   | AssignSpawnedThread of lval * ThreadIdDomain.Thread.t (** Assign spawned thread's ID to lval. *)
-  | Access of {exp: CilType.Exp.t; lvals: Queries.LS.t; kind: AccessKind.t; reach: bool}
+  | Access of {exp: CilType.Exp.t; lvals: Queries.AD.t; kind: AccessKind.t; reach: bool}
   | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) (* TODO: unused *)
   | UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *)
   | Assert of exp
@@ -41,7 +41,7 @@ let pretty () = function
   | EnterMultiThreaded -> text "EnterMultiThreaded"
   | SplitBranch (exp, tv) -> dprintf "SplitBranch (%a, %B)" d_exp exp tv
   | AssignSpawnedThread (lval, tid) -> dprintf "AssignSpawnedThread (%a, %a)" d_lval lval ThreadIdDomain.Thread.pretty tid
-  | Access {exp; lvals; kind; reach} -> dprintf "Access {exp=%a; lvals=%a; kind=%a; reach=%B}" CilType.Exp.pretty exp Queries.LS.pretty lvals AccessKind.pretty kind reach
+  | Access {exp; lvals; kind; reach} -> dprintf "Access {exp=%a; lvals=%a; kind=%a; reach=%B}" CilType.Exp.pretty exp Queries.AD.pretty lvals AccessKind.pretty kind reach
   | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp
   | UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp
   | Assert exp -> dprintf "Assert %a" d_exp exp