[impurity] Change Var to Pvar

Summary: We always add Pvars to impurity domain. So let's simplify the domain to make it explicit.

Reviewed By: ngorogiannis

Differential Revision: D25220214

fbshipit-source-id: 4dc9bce4c

infer/src/checkers/impurity.ml

@@ -42,7 +42,8 @@ let ignore_array_index (access : BaseMemory.Access.t) : unit HilExp.Access.t =
       TakeAddress
 
 
-let add_invalid_and_modified ~var ~access ~check_empty attrs acc : ImpurityDomain.ModifiedVarSet.t =
+let add_invalid_and_modified ~pvar ~access ~check_empty attrs acc : ImpurityDomain.ModifiedVarSet.t
+    =
   let modified =
     Attributes.get_written_to attrs
     |> Option.value_map ~default:[] ~f:(fun modified -> [ImpurityDomain.WrittenTo modified])
@@ -59,11 +60,11 @@ let add_invalid_and_modified ~var ~access ~check_empty attrs acc : ImpurityDomai
   else
     List.fold_left ~init:acc
       ~f:(fun acc trace ->
-        ImpurityDomain.ModifiedVarSet.add {var; access= ignore_array_index access; trace} acc )
+        ImpurityDomain.ModifiedVarSet.add {pvar; access= ignore_array_index access; trace} acc )
       invalid_and_modified
 
 
-let add_to_modified ~var ~access ~addr pre_heap post modified_vars =
+let add_to_modified ~pvar ~access ~addr pre_heap post modified_vars =
   let rec aux modified_vars ~addr_to_explore ~visited : ImpurityDomain.ModifiedVarSet.t =
     match addr_to_explore with
     | [] ->
@@ -82,18 +83,19 @@ let add_to_modified ~var ~access ~addr pre_heap post modified_vars =
                 "It is unexpected to have an address which has a binding in pre but not in post!"
           | None, Some (_, attrs_post) ->
               aux
-                (add_invalid_and_modified ~var ~access ~check_empty:false attrs_post modified_vars)
+                (add_invalid_and_modified ~pvar ~access ~check_empty:false attrs_post modified_vars)
                 ~addr_to_explore ~visited
           | Some edges_pre, Some (edges_post, attrs_post) -> (
             match get_matching_dest_addr_opt ~edges_pre ~edges_post with
             | Some addr_list ->
                 aux
-                  (add_invalid_and_modified ~var ~access attrs_post ~check_empty:false
+                  (add_invalid_and_modified ~pvar ~access attrs_post ~check_empty:false
                      modified_vars)
                   ~addr_to_explore:(addr_list @ addr_to_explore) ~visited
             | None ->
                 aux
-                  (add_invalid_and_modified ~var ~access ~check_empty:true attrs_post modified_vars)
+                  (add_invalid_and_modified ~pvar ~access ~check_empty:true attrs_post
+                     modified_vars)
                   ~addr_to_explore ~visited ) )
   in
   aux modified_vars ~addr_to_explore:[(access, addr)] ~visited:AbstractValue.Set.empty
@@ -101,13 +103,13 @@ let add_to_modified ~var ~access ~addr pre_heap post modified_vars =
 
 let get_modified_params pname post_stack pre_heap post formals =
   List.fold_left formals ~init:ImpurityDomain.ModifiedVarSet.empty ~f:(fun acc (name, typ) ->
-      let var = Var.of_pvar (Pvar.mk name pname) in
-      match BaseStack.find_opt var post_stack with
+      let pvar = Pvar.mk name pname in
+      match BaseStack.find_opt (Var.of_pvar pvar) post_stack with
       | Some (addr, _) when Typ.is_pointer typ -> (
         match BaseMemory.find_opt addr pre_heap with
         | Some edges_pre ->
             BaseMemory.Edges.fold edges_pre ~init:acc ~f:(fun acc (access, (addr, _)) ->
-                add_to_modified ~var ~access ~addr pre_heap post acc )
+                add_to_modified ~pvar ~access ~addr pre_heap post acc )
         | None ->
             debug "The address is not materialized in in pre-heap." ;
             acc )
@@ -122,7 +124,9 @@ let get_modified_globals pre_heap post post_stack =
         (* since global vars are rooted in the stack, we don't have
            access here but we still want to pick up changes to
            globals. *)
-        add_to_modified ~var ~access:HilExp.Access.Dereference ~addr pre_heap post modified_globals
+        add_to_modified
+          ~pvar:(Option.value_exn (Var.get_pvar var))
+          ~access:HilExp.Access.Dereference ~addr pre_heap post modified_globals
       else modified_globals )
     post_stack ImpurityDomain.ModifiedVarSet.empty
 

infer/src/checkers/impurityDomain.ml

@@ -12,11 +12,13 @@ module SkippedCalls = PulseSkippedCalls
 type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * PulseTrace.t)
 [@@deriving compare]
 
+let pp_pvar fmt pv = F.pp_print_string fmt (Pvar.get_simplified_name pv)
+
 module ModifiedVar = struct
-  type t = {var: Var.t; access: unit HilExp.Access.t; trace: trace [@compare.ignore]}
+  type t = {pvar: Pvar.t; access: unit HilExp.Access.t; trace: trace [@compare.ignore]}
   [@@deriving compare]
 
-  let pp fmt {var} = F.fprintf fmt "@\n %a @\n" Var.pp var
+  let pp fmt {pvar} = F.fprintf fmt "@\n %a @\n" pp_pvar pvar
 end
 
 module ModifiedVarSet = AbstractDomain.FiniteSet (ModifiedVar)
@@ -65,16 +67,16 @@ let pp_param_source fmt = function
       F.pp_print_string fmt "global variable"
 
 
-let add_to_errlog ~nesting param_source ModifiedVar.{var; trace} errlog =
+let add_to_errlog ~nesting param_source ModifiedVar.{pvar; trace} errlog =
   match trace with
   | WrittenTo access_trace ->
       PulseTrace.add_to_errlog ~include_value_history:false ~nesting
         ~pp_immediate:(fun fmt ->
-          F.fprintf fmt "%a `%a` modified here" pp_param_source param_source Var.pp var )
+          F.fprintf fmt "%a `%a` modified here" pp_param_source param_source pp_pvar pvar )
         access_trace errlog
   | Invalid (invalidation, invalidation_trace) ->
       PulseTrace.add_to_errlog ~include_value_history:false ~nesting
         ~pp_immediate:(fun fmt ->
-          F.fprintf fmt "%a `%a` %a here" pp_param_source param_source Var.pp var
+          F.fprintf fmt "%a `%a` %a here" pp_param_source param_source pp_pvar pvar
             PulseInvalidation.describe invalidation )
         invalidation_trace errlog

infer/src/checkers/impurityDomain.mli

@@ -10,7 +10,7 @@ type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * Pulse
 
 module ModifiedVar : sig
   type t =
-    { var: Var.t
+    { pvar: Pvar.t
     ; access: unit HilExp.Access.t  (** accesses that are oblivious to modified array indices *)
     ; trace: trace }
 end