diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index a282076a7..40927b26c 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/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 diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 724771565..b52db7477 100644 --- a/infer/src/checkers/purity.ml +++ b/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 ; diff --git a/infer/src/checkers/purityDomain.ml b/infer/src/checkers/purityDomain.ml index 52e63063f..55d313310 100644 --- a/infer/src/checkers/purityDomain.ml +++ b/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