[purity] Refactor global writes and get rid of BottomLifting

Reviewed By: mbouaziz, ngorogiannis

Differential Revision: D13878260

fbshipit-source-id: bafd3cfbe

infer/src/checkers/loopInvariant.ml

@@ -177,19 +177,20 @@ let get_invalidated_vars_in_loop tenv loop_head ~is_inv_by_default loop_nodes =
       Procdesc.Node.get_instrs node
       |> Instrs.fold ~init:acc ~f:(fun acc instr ->
              match instr with
-             | Sil.Call ((id, _), Const (Cfun callee_pname), args, _, _) ->
+             | Sil.Call ((id, _), Const (Cfun callee_pname), args, _, _) -> (
                  let purity = get_purity tenv ~is_inv_by_default callee_pname args in
-                 Option.value_map (PurityDomain.get_modified_params purity) ~default:acc
-                   ~f:(fun modified_params ->
-                     let acc' =
-                       get_vars_to_invalidate node loop_head args modified_params
-                         (InvalidatedVars.add (Var.of_id id) acc)
-                     in
-                     (* if one of the callees modifies a global static
-                        variable, invalidate all the function calls *)
-                     if PurityDomain.contains_global modified_params then
-                       InvalidatedVars.union acc' (force all_modified)
-                     else acc' )
+                 PurityDomain.(
+                   match purity with
+                   | AbstractDomain.Types.Top ->
+                       (* modified global *)
+                       (* if one of the callees modifies a global static
+                          variable, invalidate all the function calls *)
+                       InvalidatedVars.union acc (force all_modified)
+                   | AbstractDomain.Types.NonTop modified_params ->
+                       if ModifiedParamIndices.is_empty modified_params then (*pure*) acc
+                       else
+                         get_vars_to_invalidate node loop_head args modified_params
+                           (InvalidatedVars.add (Var.of_id id) acc)) )
              | _ ->
                  acc ) )
     loop_nodes InvalidatedVars.empty

infer/src/checkers/purity.ml

@@ -59,14 +59,12 @@ module TransferFunctions = struct
     let base_var, _ = HilExp.AccessExpression.get_base ae in
     (* treat writes to global (static) variables separately since they
        are not considered to be explicit parameters. *)
-    let modified_params =
-      if Var.is_global base_var then Domain.ModifiedParamIndices.singleton Domain.global
-      else
-        get_modified_params formals ~f:(fun var ->
-            Var.equal var base_var || ModifiedVarSet.mem var (get_alias_set inferbo_mem base_var)
-        )
-    in
-    Domain.impure modified_params
+    if Var.is_global base_var then Domain.impure_global
+    else
+      let alias_set = lazy (get_alias_set inferbo_mem base_var) in
+      get_modified_params formals ~f:(fun var ->
+          Var.equal var base_var || ModifiedVarSet.mem var (Lazy.force alias_set) )
+      |> Domain.impure_params
 
 
   let rec is_heap_access ae =
@@ -115,21 +113,21 @@ module TransferFunctions = struct
       get_modified_params formals ~f:(fun formal_var ->
           ModifiedVarSet.mem formal_var vars_of_modified_args )
     in
-    (* if callee modified global, caller also indirectly does so*)
-    if Domain.contains_global callee_modified_params then
-      Domain.ModifiedParamIndices.add Domain.global caller_modified_params
-    else caller_modified_params
+    caller_modified_params
 
 
   (* if the callee is impure, find the parameters that have been modified by the callee *)
   let find_modified_if_impure inferbo_mem formals args callee_summary =
-    match Domain.get_modified_params callee_summary with
-    | Some callee_modified_params ->
-        debug "Callee modified params %a \n" Domain.ModifiedParamIndices.pp callee_modified_params ;
-        Domain.impure
-          (find_params_matching_modified_args inferbo_mem formals args callee_modified_params)
-    | None ->
-        Domain.pure
+    match callee_summary with
+    | AbstractDomain.Types.Top ->
+        Domain.impure_global
+    | AbstractDomain.Types.NonTop callee_modified_params ->
+        Domain.(
+          debug "Callee modified params %a \n" ModifiedParamIndices.pp callee_modified_params ;
+          if ModifiedParamIndices.is_empty callee_modified_params then pure
+          else
+            impure_params
+              (find_params_matching_modified_args inferbo_mem formals args callee_modified_params))
 
 
   let exec_instr (astate : Domain.t)
@@ -146,18 +144,21 @@ module TransferFunctions = struct
         track_modified_params inferbo_mem formals ae |> Domain.join astate
     | Call (_, Direct called_pname, args, _, _) ->
         let matching_modified =
-          find_params_matching_modified_args inferbo_mem formals args
-            (Domain.all_params_modified args)
+          lazy
+            (find_params_matching_modified_args inferbo_mem formals args
+               (Domain.all_params_modified args))
         in
         Domain.join astate
           ( match InvariantModels.Call.dispatch tenv called_pname [] with
           | Some inv ->
-              Domain.with_purity (InvariantModels.is_invariant inv) matching_modified
-          | None ->
-              Payload.read pdesc called_pname
-              |> Option.value_map ~default:(Domain.impure matching_modified) ~f:(fun summary ->
-                     debug "Reading from %a \n" Typ.Procname.pp called_pname ;
-                     find_modified_if_impure inferbo_mem formals args summary ) )
+              Domain.with_purity (InvariantModels.is_invariant inv) (Lazy.force matching_modified)
+          | None -> (
+            match Payload.read pdesc called_pname with
+            | Some summary ->
+                debug "Reading from %a \n" Typ.Procname.pp called_pname ;
+                find_modified_if_impure inferbo_mem formals args summary
+            | None ->
+                Domain.impure_params (Lazy.force matching_modified) ) )
     | Call (_, Indirect _, _, _, _) ->
         (* This should never happen in Java. Fail if it does. *)
         L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr
@@ -200,16 +201,8 @@ let checker {Callbacks.tenv; summary; proc_desc; integer_type_widths} : Summary.
   in
   match Analyzer.compute_post proc_data ~initial:PurityDomain.pure with
   | Some astate ->
-      let astate' =
-        PurityDomain.get_modified_params astate
-        |> Option.value_map ~default:astate ~f:(fun modified_params ->
-               debug "Modified parameter indices of %a: %a \n" Typ.Procname.pp proc_name
-                 PurityDomain.ModifiedParamIndices.pp modified_params ;
-               if PurityDomain.ModifiedParamIndices.is_empty modified_params then PurityDomain.pure
-               else astate )
-      in
-      if should_report proc_desc && PurityDomain.is_pure astate' then report_pure () ;
-      Payload.update_summary astate' summary
+      if should_report proc_desc && PurityDomain.is_pure astate then report_pure () ;
+      Payload.update_summary astate summary
   | None ->
       L.internal_error "Analyzer failed to compute purity information for %a@." Typ.Procname.pp
         proc_name ;

infer/src/checkers/purityDomain.ml

@@ -7,22 +7,24 @@
 open! IStd
 module F = Format
 module ModifiedParamIndices = AbstractDomain.FiniteSet (Int)
-module Domain = AbstractDomain.BottomLifted (ModifiedParamIndices)
+module Domain = AbstractDomain.TopLifted (ModifiedParamIndices)
 include Domain
 
-let global = -1
+let pure = AbstractDomain.Types.NonTop ModifiedParamIndices.empty
 
-let contains_global modified_params = ModifiedParamIndices.mem global modified_params
+let impure_global = AbstractDomain.Types.Top
 
-let pure = AbstractDomain.Types.Bottom
-
-let is_pure = Domain.is_bottom
+let is_pure astate =
+  match astate with
+  | AbstractDomain.Types.Top ->
+      false
+  | AbstractDomain.Types.NonTop modified_params ->
+      ModifiedParamIndices.is_empty modified_params
 
-let impure modified_args = AbstractDomain.Types.NonBottom modified_args
 
-let with_purity is_pure modified_args =
-  if is_pure then AbstractDomain.Types.Bottom else impure modified_args
+let impure_params modified_params = AbstractDomain.Types.NonTop modified_params
 
+let with_purity is_pure modified_params = if is_pure then pure else impure_params modified_params
 
 let all_params_modified args =
   List.foldi ~init:ModifiedParamIndices.empty
@@ -30,14 +32,6 @@ let all_params_modified args =
     args
 
 
-let get_modified_params astate =
-  match astate with
-  | AbstractDomain.Types.NonBottom modified_args ->
-      Some modified_args
-  | AbstractDomain.Types.Bottom ->
-      None
-
-
 type summary = Domain.t
 
 let pp_summary fmt astate = F.fprintf fmt "@\n Purity summary: %a @\n" Domain.pp astate