diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 0bbbc5cb9..652eb49f6 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -243,7 +243,7 @@ module PulseTransferFunctions = struct [astate] | ContinueProgram astate -> dispatch_call analysis_data ret call_exp actuals location call_flags astate - |> PulseReport.report_results analysis_data ) + |> PulseReport.report_exec_results analysis_data ) in let dynamic_types_unreachable = PulseOperations.get_dynamic_type_unreachable_values vars astate @@ -279,30 +279,28 @@ module PulseTransferFunctions = struct | Load {id= lhs_id; e= rhs_exp; loc} -> (* [lhs_id := *rhs_exp] *) let result = - let+ astate_rhs_addr_hists = - if Config.pulse_isl then - let+ astate_rhs_addr_hists = PulseOperations.eval_deref_isl loc rhs_exp astate in - astate_rhs_addr_hists - else - let+ astate_rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in - [astate_rhs_addr_hist] - in - List.map astate_rhs_addr_hists ~f:(fun (astate, rhs_addr_hist) -> - PulseOperations.write_id lhs_id rhs_addr_hist astate ) + if Config.pulse_isl then + PulseOperations.eval_deref_isl loc rhs_exp astate + |> List.map ~f:(fun result -> + let+ astate, rhs_addr_hist = result in + PulseOperations.write_id lhs_id rhs_addr_hist astate ) + else + [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in + PulseOperations.write_id lhs_id rhs_addr_hist astate) ] in - PulseReport.report_list_result analysis_data result + PulseReport.report_results analysis_data result | Store {e1= lhs_exp; e2= rhs_exp; loc} -> (* [*lhs_exp := rhs_exp] *) let event = ValueHistory.Assignment loc in let result = - let* astate, (rhs_addr, rhs_history) = + let<*> astate, (rhs_addr, rhs_history) = PulseOperations.eval NoAccess loc rhs_exp astate in - let* is_structured, ls_astate_lhs_addr_hist = + let<*> is_structured, ls_astate_lhs_addr_hist = if Config.pulse_isl then PulseOperations.eval_structure_isl Write loc lhs_exp astate else - let* astate, lhs_addr_hist = PulseOperations.eval Write loc lhs_exp astate in - Ok (false, [(astate, lhs_addr_hist)]) + let+ astate, lhs_addr_hist = PulseOperations.eval Write loc lhs_exp astate in + (false, [Ok (astate, lhs_addr_hist)]) in let write_function lhs_addr_hist astate = if is_structured then @@ -310,40 +308,35 @@ module PulseTransferFunctions = struct ~obj:(rhs_addr, event :: rhs_history) astate else - let+ astate = - PulseOperations.write_deref loc ~ref:lhs_addr_hist + [ PulseOperations.write_deref loc ~ref:lhs_addr_hist ~obj:(rhs_addr, event :: rhs_history) - astate - in - [astate] + astate ] in - let* astates = - List.fold_result ls_astate_lhs_addr_hist ~init:[] - ~f:(fun acc_astates (astate, lhs_addr_hist) -> + let astates = + List.concat_map ls_astate_lhs_addr_hist ~f:(fun result -> + let<*> astate, lhs_addr_hist = result in match (Config.pulse_isl, astate.AbductiveDomain.isl_status) with | false, _ | true, ISLOk -> - let+ astates = write_function lhs_addr_hist astate in - List.rev_append astates acc_astates + write_function lhs_addr_hist astate | true, ISLError -> - Ok (astate :: acc_astates) ) + [Ok astate] ) in let astates = if Topl.is_deep_active () then - List.map astates ~f:(fun astate -> + List.map astates ~f:(fun result -> + let+ astate = result in topl_store_step loc ~lhs:lhs_exp ~rhs:rhs_exp astate ) else astates in match lhs_exp with | Lvar pvar when Pvar.is_return pvar -> - List.fold_result astates ~init:[] ~f:(fun acc astate -> - let+ astate = - PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate - in - astate :: acc ) + List.map astates ~f:(fun result -> + let* astate = result in + PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate ) | _ -> - Ok astates + astates in - PulseReport.report_list_result analysis_data result + PulseReport.report_results analysis_data result | Prune (condition, loc, _is_then_branch, _if_kind) -> (let<*> astate = PulseOperations.prune loc ~condition astate in if PulseArithmetic.is_unsat_cheap astate then @@ -352,10 +345,10 @@ module PulseTransferFunctions = struct else (* [condition] is true or unknown value: go into the branch *) [Ok (ContinueProgram astate)]) - |> PulseReport.report_results analysis_data + |> PulseReport.report_exec_results analysis_data | Call (ret, call_exp, actuals, loc, call_flags) -> dispatch_call analysis_data ret call_exp actuals loc call_flags astate - |> PulseReport.report_results analysis_data + |> PulseReport.report_exec_results analysis_data | Metadata (ExitScope (vars, location)) -> let remove_vars vars astates = List.concat_map astates ~f:(fun (astate : Domain.t) -> @@ -363,12 +356,8 @@ module PulseTransferFunctions = struct | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> [astate] | ContinueProgram astate -> - ( match PulseOperations.remove_vars tenv vars location astate with - | Ok astate -> - Ok [astate] - | Error _ as error -> - error ) - |> PulseReport.report_list_result analysis_data ) + PulseOperations.remove_vars tenv vars location astate + |> PulseReport.report_result analysis_data ) in if Procname.is_java (Procdesc.get_proc_name proc_desc) then remove_vars vars [ContinueProgram astate] diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index ffbf362f4..b5192b920 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -123,11 +123,10 @@ module Misc = struct let astates_alloc = let astate = PulseArithmetic.and_positive (fst deleted_access) astate in if Config.pulse_isl then - match PulseOperations.invalidate_biad_isl location invalidation deleted_access astate with - | Error _ as err -> - [err] - | Ok astates -> - List.map astates ~f:(fun astate -> Ok (ContinueProgram astate)) + PulseOperations.invalidate_biad_isl location invalidation deleted_access astate + |> List.map ~f:(fun result -> + let+ astate = result in + ContinueProgram astate ) else let<+> astate = PulseOperations.invalidate location invalidation deleted_access astate in astate diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index 009430fa1..0a50993a1 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -22,10 +22,7 @@ let mk_objc_method_nil_summary_aux proc_desc astate = let astate = PulseArithmetic.prune_eq_zero (fst self_value) astate in let ret_var = Procdesc.get_ret_var proc_desc in let* astate, ret_var_addr_hist = PulseOperations.eval Write location (Lvar ret_var) astate in - let+ astate = - PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:self_value astate - in - [astate] + PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:self_value astate let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_data) initial = @@ -39,7 +36,7 @@ let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_ However, there is an exception in the case where the return type is non-POD. In that case it's UB and we want to report an error. *) let result = mk_objc_method_nil_summary_aux proc_desc astate in - Some (PulseReport.report_list_result analysis_data result) + Some (PulseReport.report_result analysis_data result) | ContinueProgram _, _ | ExitProgram _, _ | AbortProgram _, _ @@ -55,10 +52,9 @@ let append_objc_self_positive ({InterproceduralAnalysis.proc_desc} as analysis_d | ContinueProgram astate -> let result = let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in - let astate = PulseArithmetic.prune_positive (fst value) astate in - [astate] + PulseArithmetic.prune_positive (fst value) astate in - PulseReport.report_list_result analysis_data result + PulseReport.report_result analysis_data result | ExitProgram _ | AbortProgram _ | LatentAbortProgram _ | ISLLatentMemoryError _ -> [astate] diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 3eff45f19..41b92b523 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -57,33 +57,29 @@ let check_addr_access access_mode location (address, history) astate = let check_and_abduce_addr_access_isl access_mode location (address, history) ?(null_noop = false) astate = let access_trace = Trace.Immediate {location; history} in - let* astates = - AddressAttributes.check_valid_isl access_trace address ~null_noop astate - |> Result.map_error ~f:(fun (invalidation, invalidation_trace, astate) -> - ( Diagnostic.AccessToInvalidAddress - {calling_context= []; invalidation; invalidation_trace; access_trace} - , astate ) ) - in - match access_mode with - | Read -> - List.fold_result astates ~init:[] ~f:(fun astates astate -> - match AddressAttributes.check_initialized access_trace address astate with - | Error _ -> - Error - ( Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace} - , AbductiveDomain.set_isl_status ISLError astate ) - | Ok ok_astate -> - Ok (ok_astate :: astates) ) - | Write -> - Ok - (List.map astates ~f:(fun astate -> - match astate.AbductiveDomain.isl_status with - | ISLOk -> - AbductiveDomain.initialize address astate - | ISLError -> - astate )) - | NoAccess -> - Ok astates + match AddressAttributes.check_valid_isl access_trace address ~null_noop astate with + | Error (invalidation, invalidation_trace, astate) -> + [ Error + ( Diagnostic.AccessToInvalidAddress + {calling_context= []; invalidation; invalidation_trace; access_trace} + , astate ) ] + | Ok astates -> ( + match access_mode with + | Read -> + List.map astates ~f:(fun astate -> + AddressAttributes.check_initialized access_trace address astate + |> Result.map_error ~f:(fun () -> + ( Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace} + , AbductiveDomain.set_isl_status ISLError astate ) ) ) + | Write -> + List.map astates ~f:(fun astate -> + match astate.AbductiveDomain.isl_status with + | ISLOk -> + Ok (AbductiveDomain.initialize address astate) + | ISLError -> + Ok astate ) + | NoAccess -> + List.map ~f:(fun astate -> Ok astate) astates ) module Closures = struct @@ -166,18 +162,17 @@ let eval_access mode location addr_hist access astate = let eval_access_biad_isl mode location addr_hist access astate = - let map_ok addr_hist access astates = - List.map - ~f:(fun astate -> + let map_ok addr_hist access results = + List.map results ~f:(fun result -> + let+ astate = result in match astate.AbductiveDomain.isl_status with | ISLOk -> Memory.eval_edge addr_hist access astate | ISLError -> (astate, addr_hist) ) - astates in - let+ astates = check_and_abduce_addr_access_isl mode location addr_hist astate in - map_ok addr_hist access astates + let results = check_and_abduce_addr_access_isl mode location addr_hist astate in + map_ok addr_hist access results let eval mode location exp0 astate = @@ -267,52 +262,47 @@ let eval_deref location exp astate = let eval_structure_isl mode loc exp astate = match (exp : Exp.t) with | Lfield (exp', field, _) -> - let* astate, addr_hist = eval mode loc exp' astate in - let+ astates = - eval_access_biad_isl mode loc addr_hist (HilExp.Access.FieldAccess field) astate - in + let+ astate, addr_hist = eval mode loc exp' astate in + let astates = eval_access_biad_isl mode loc addr_hist (FieldAccess field) astate in (false, astates) | Lindex (exp', exp_index) -> let* astate, addr_hist_index = eval mode loc exp_index astate in - let* astate, addr_hist = eval mode loc exp' astate in - let+ astates = + let+ astate, addr_hist = eval mode loc exp' astate in + let astates = eval_access_biad_isl mode loc addr_hist - (HilExp.Access.ArrayAccess (StdTyp.void, fst addr_hist_index)) + (ArrayAccess (StdTyp.void, fst addr_hist_index)) astate in (false, astates) | _ -> let+ astate, (addr, history) = eval mode loc exp astate in - (true, [(astate, (addr, history))]) + (true, [Ok (astate, (addr, history))]) let eval_deref_biad_isl location access addr_hist astate = - let+ astates = check_and_abduce_addr_access_isl Read location addr_hist astate in - List.map - ~f:(fun astate -> + let astates = check_and_abduce_addr_access_isl Read location addr_hist astate in + List.map astates ~f:(fun astate -> + let+ astate = astate in match astate.AbductiveDomain.isl_status with | ISLOk -> Memory.eval_edge addr_hist access astate | ISLError -> (astate, addr_hist) ) - astates let eval_deref_isl location exp astate = - let* is_structured, ls_astate_addr_hist = eval_structure_isl Read location exp astate in + let<*> is_structured, ls_astate_addr_hist = eval_structure_isl Read location exp astate in let eval_deref_function (astate, addr_hist) = if is_structured then eval_deref_biad_isl location Dereference addr_hist astate - else - let+ astate = eval_deref location exp astate in - [astate] + else [eval_deref location exp astate] in - List.fold_result ls_astate_addr_hist ~init:[] ~f:(fun acc_astates ((astate, _) as astate_addr) -> + List.concat_map ls_astate_addr_hist ~f:(fun result -> + let<*> ((astate, _) as astate_addr) = result in match astate.AbductiveDomain.isl_status with | ISLOk -> - let+ astates = eval_deref_function astate_addr in - acc_astates @ astates + eval_deref_function astate_addr | ISLError -> - Ok (acc_astates @ [astate_addr]) ) + [Ok astate_addr] ) let realloc_pvar tenv pvar typ location astate = @@ -338,16 +328,14 @@ let write_access location addr_trace_ref access addr_trace_obj astate = let write_access_biad_isl location addr_trace_ref access addr_trace_obj astate = - let* astates = check_and_abduce_addr_access_isl Write location addr_trace_ref astate in - List.fold_result astates ~init:[] ~f:(fun acc ast -> - let astate = - match ast.AbductiveDomain.isl_status with - | ISLOk -> - Memory.add_edge addr_trace_ref access addr_trace_obj location ast - | ISLError -> - ast - in - Ok (astate :: acc) ) + check_and_abduce_addr_access_isl Write location addr_trace_ref astate + |> List.map ~f:(fun result -> + let+ astate = result in + match astate.AbductiveDomain.isl_status with + | ISLOk -> + Memory.add_edge addr_trace_ref access addr_trace_obj location astate + | ISLError -> + astate ) let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate = @@ -385,17 +373,14 @@ let invalidate location cause addr_trace astate = let invalidate_biad_isl location cause (address, history) astate = - let+ astates = - check_and_abduce_addr_access_isl NoAccess location (address, history) ~null_noop:true astate - in - List.map - ~f:(fun astate -> - match astate.AbductiveDomain.isl_status with - | ISLOk -> - AddressAttributes.invalidate (address, history) cause location astate - | ISLError -> - astate ) - astates + check_and_abduce_addr_access_isl NoAccess location (address, history) ~null_noop:true astate + |> List.map ~f:(fun result -> + let+ astate = result in + match astate.AbductiveDomain.isl_status with + | ISLOk -> + AddressAttributes.invalidate (address, history) cause location astate + | ISLError -> + astate ) let invalidate_access location cause ref_addr_hist access astate = diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 041b55129..8c5de9dbb 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -70,7 +70,7 @@ val eval_structure_isl : -> Location.t -> Exp.t -> t - -> (bool * (t * (AbstractValue.t * ValueHistory.t)) list) access_result + -> (bool * (t * (AbstractValue.t * ValueHistory.t)) access_result list) access_result (** Similar to eval but apply to data structures and ISL abduction. Return a list of abduced states (ISLOk and ISLErs); The boolean indicates whether it is data structures or not. *) @@ -80,7 +80,7 @@ val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistor (** Like [eval] but evaluates [*exp]. *) val eval_deref_isl : - Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) list access_result + Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result list val eval_access : access_mode @@ -138,14 +138,14 @@ val write_deref_biad_isl : -> AbstractValue.t HilExp.Access.t -> obj:AbstractValue.t * ValueHistory.t -> t - -> t list access_result + -> t access_result list val invalidate : Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result (** record that the address is invalid *) val invalidate_biad_isl : - Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t list access_result + Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result list (** record that the address is invalid. If the address has not been allocated, abduce ISL specs for both invalid (null, free, unint) and allocated heap. *) diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index 49f569470..d959bf809 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -57,22 +57,6 @@ let report_error tenv proc_desc err_log access_result = ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue} ) -let exec_list_of_list_result = function - | Ok posts -> - posts - | Error Unsat -> - [] - | Error (Sat post) -> - [post] - - -let report_list_result {tenv; InterproceduralAnalysis.proc_desc; err_log} result = - let open Result.Monad_infix in - report_error tenv proc_desc err_log result - >>| List.map ~f:(fun post -> ExecutionDomain.ContinueProgram post) - |> exec_list_of_list_result - - let post_of_report_result = function | Ok post -> Some post @@ -82,6 +66,17 @@ let post_of_report_result = function Some post -let report_results {tenv; InterproceduralAnalysis.proc_desc; err_log} results = +let report_exec_results {InterproceduralAnalysis.proc_desc; tenv; err_log} results = List.filter_map results ~f:(fun exec_result -> report_error tenv proc_desc err_log exec_result |> post_of_report_result ) + + +let report_results analysis_data results = + List.map results ~f:(fun result -> + let open IResult.Let_syntax in + let+ astate = result in + ExecutionDomain.ContinueProgram astate ) + |> report_exec_results analysis_data + + +let report_result analysis_data result = report_results analysis_data [result] diff --git a/infer/src/pulse/PulseReport.mli b/infer/src/pulse/PulseReport.mli index 450d39c89..279c16892 100644 --- a/infer/src/pulse/PulseReport.mli +++ b/infer/src/pulse/PulseReport.mli @@ -11,12 +11,17 @@ open PulseDomainInterface type 'a access_result = ('a, Diagnostic.t * AbductiveDomain.t) result -val report_list_result : +val report_result : PulseSummary.t InterproceduralAnalysis.t - -> AbductiveDomain.t list access_result + -> AbductiveDomain.t access_result -> ExecutionDomain.t list val report_results : PulseSummary.t InterproceduralAnalysis.t + -> AbductiveDomain.t access_result list + -> ExecutionDomain.t list + +val report_exec_results : + PulseSummary.t InterproceduralAnalysis.t -> ExecutionDomain.t access_result list -> ExecutionDomain.t list