From 056c8abbff965ed90e19709af6c2f4c22fae5aff Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Thu, 18 Mar 2021 05:53:56 -0700 Subject: [PATCH] [pulse][refactor] Move operations related to function calls to PulseCallOperations Summary: To implement nil summaries for unknown calls I would like to reuse functionality from PulseObjectiveCSummary which already depends on PulseOperations causing circular dependencies. Reviewed By: jvillard Differential Revision: D27155092 fbshipit-source-id: 1c300ead0 --- infer/src/pulse/Pulse.ml | 8 +- infer/src/pulse/PulseCallOperations.ml | 243 ++++++++++++++++++++++++ infer/src/pulse/PulseCallOperations.mli | 40 ++++ infer/src/pulse/PulseModels.ml | 7 +- infer/src/pulse/PulseOperations.ml | 230 ---------------------- infer/src/pulse/PulseOperations.mli | 31 +-- 6 files changed, 296 insertions(+), 263 deletions(-) create mode 100644 infer/src/pulse/PulseCallOperations.ml create mode 100644 infer/src/pulse/PulseCallOperations.mli diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 0f33f7a85..0261e5f1b 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -47,17 +47,17 @@ module PulseTransferFunctions = struct | Some callee_pname when not Config.pulse_intraprocedural_only -> let formals_opt = get_pvar_formals callee_pname in let callee_data = analyze_dependency callee_pname in - PulseOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname + PulseCallOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt astate | _ -> L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; let astate = let arg_values = List.map actuals ~f:(fun ((value, _), _) -> value) in - PulseOperations.conservatively_initialize_args arg_values astate + PulseCallOperations.conservatively_initialize_args arg_values astate in [ Ok (ContinueProgram - (PulseOperations.unknown_call tenv call_loc (SkippedUnknownCall call_exp) ~ret + (PulseCallOperations.unknown_call tenv call_loc (SkippedUnknownCall call_exp) ~ret ~actuals ~formals_opt:None astate)) ] @@ -164,7 +164,7 @@ module PulseTransferFunctions = struct List.map func_args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= value, _} -> value ) in - PulseOperations.conservatively_initialize_args arg_values astate + PulseCallOperations.conservatively_initialize_args arg_values astate in model analysis_data ~callee_procname call_loc ~ret astate | None -> diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml new file mode 100644 index 000000000..0eb6c8ffb --- /dev/null +++ b/infer/src/pulse/PulseCallOperations.ml @@ -0,0 +1,243 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module L = Logging +open PulseBasicInterface +open PulseDomainInterface +open PulseOperations.Import + +type t = AbductiveDomain.t + +let is_ptr_to_const formal_typ_opt = + Option.value_map formal_typ_opt ~default:false ~f:(fun (formal_typ : Typ.t) -> + match formal_typ.desc with Typ.Tptr (t, _) -> Typ.is_const t.quals | _ -> false ) + + +let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = + let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in + let havoc_ret (ret, _) astate = PulseOperations.havoc_id ret [event] astate in + let rec havoc_fields ((_, history) as addr) typ astate = + match typ.Typ.desc with + | Tstruct struct_name -> ( + match Tenv.lookup tenv struct_name with + | Some {fields} -> + List.fold fields ~init:astate ~f:(fun acc (field, field_typ, _) -> + let fresh_value = AbstractValue.mk_fresh () in + Memory.add_edge addr (FieldAccess field) (fresh_value, [event]) call_loc acc + |> havoc_fields (fresh_value, history) field_typ ) + | None -> + astate ) + | _ -> + astate + in + let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate = + (* We should not havoc when the corresponding formal is a + pointer to const *) + match actual_typ.Typ.desc with + | Tptr (typ, _) + when (not (Language.curr_language_is Java)) && not (is_ptr_to_const formal_typ_opt) -> + (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when + havoc'ing pointer parameters (which normally causes a [check_valid] call. *) + let fresh_value = AbstractValue.mk_fresh () in + Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate + |> havoc_fields actual typ + | _ -> + astate + in + let add_skipped_proc astate = + match reason with + | CallEvent.SkippedKnownCall proc_name -> + AbductiveDomain.add_skipped_call proc_name + (Trace.Immediate {location= call_loc; history= []}) + astate + | _ -> + astate + in + L.d_printfln "skipping unknown procedure@." ; + ( match formals_opt with + | None -> + List.fold actuals + ~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ None astate) + ~init:astate + | Some formals -> ( + match + List.fold2 actuals formals + ~f:(fun astate actual_typ (_, formal_typ) -> + havoc_actual_if_ptr actual_typ (Some formal_typ) astate ) + ~init:astate + with + | Unequal_lengths -> + L.d_printfln "ERROR: formals have length %d but actuals have length %d" + (List.length formals) (List.length actuals) ; + astate + | Ok result -> + result ) ) + |> havoc_ret ret |> add_skipped_proc + + +let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret + ~captured_vars_with_actuals ~formals ~actuals astate = + let map_call_result ~is_isl_error_prepost callee_prepost ~f = + match + PulseInterproc.apply_prepost ~is_isl_error_prepost callee_pname call_loc ~callee_prepost + ~captured_vars_with_actuals ~formals ~actuals astate + with + | (Sat (Error _) | Unsat) as path_result -> + path_result + | Sat (Ok (post, return_val_opt, subst)) -> + let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in + let post = + match return_val_opt with + | Some (return_val, return_hist) -> + PulseOperations.write_id (fst ret) (return_val, event :: return_hist) post + | None -> + PulseOperations.havoc_id (fst ret) [event] post + in + f subst post + in + let open ExecutionDomain in + let open SatUnsat.Import in + match callee_exec_state with + | ContinueProgram astate -> + map_call_result ~is_isl_error_prepost:false astate ~f:(fun _subst astate -> + Sat (Ok (ContinueProgram astate)) ) + | AbortProgram astate + | ExitProgram astate + | LatentAbortProgram {astate} + | LatentInvalidAccess {astate} -> + map_call_result ~is_isl_error_prepost:false + (astate :> AbductiveDomain.t) + ~f:(fun subst astate -> + let* astate_summary_result = + AbductiveDomain.summary_of_post tenv caller_proc_desc astate + >>| AccessResult.of_abductive_result + in + match astate_summary_result with + | Error _ as error -> + Sat error + | Ok (astate_summary : AbductiveDomain.summary) -> ( + match callee_exec_state with + | ContinueProgram _ | ISLLatentMemoryError _ -> + assert false + | AbortProgram _ -> + Sat (Ok (AbortProgram astate_summary)) + | ExitProgram _ -> + Sat (Ok (ExitProgram astate_summary)) + | LatentAbortProgram {latent_issue} -> ( + let latent_issue = + LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue + in + let diagnostic = LatentIssue.to_diagnostic latent_issue in + match LatentIssue.should_report astate_summary diagnostic with + | `DelayReport latent_issue -> + Sat (Ok (LatentAbortProgram {astate= astate_summary; latent_issue})) + | `ReportNow -> + Sat + (Error + (ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)})) + | `ISLDelay astate -> + Sat (Error (ISLError (astate :> AbductiveDomain.t))) ) + | LatentInvalidAccess {address= address_callee; must_be_valid; calling_context} -> ( + match AbstractValue.Map.find_opt address_callee subst with + | None -> + (* the address became unreachable so the bug can never be reached; drop it *) + Unsat + | Some (address, _history) -> ( + let calling_context = + (CallEvent.Call callee_pname, call_loc) :: calling_context + in + match + AbductiveDomain.find_post_cell_opt address (astate_summary :> AbductiveDomain.t) + |> Option.bind ~f:(fun (_, attrs) -> Attributes.get_invalid attrs) + with + | None -> + (* still no proof that the address is invalid *) + Sat + (Ok + (LatentInvalidAccess + {astate= astate_summary; address; must_be_valid; calling_context})) + | Some (invalidation, invalidation_trace) -> + Sat + (Error + (ReportableError + { diagnostic= + AccessToInvalidAddress + { calling_context + ; invalidation + ; invalidation_trace + ; access_trace= must_be_valid } + ; astate= (astate_summary :> AbductiveDomain.t) })) ) ) ) ) + | ISLLatentMemoryError astate -> + map_call_result ~is_isl_error_prepost:true + (astate :> AbductiveDomain.t) + ~f:(fun _subst astate -> + AbductiveDomain.summary_of_post tenv caller_proc_desc astate + >>| AccessResult.of_abductive_result + >>| Result.map ~f:(fun astate_summary -> ISLLatentMemoryError astate_summary) ) + + +let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate) = + let reachable_values = BaseDomain.reachable_addresses_from arg_values (post :> BaseDomain.t) in + AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate + + +let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc + callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) = + let get_arg_values () = List.map actuals ~f:(fun ((value, _), _) -> value) in + match callee_data with + | Some (callee_proc_desc, exec_states) -> + let formals = + Procdesc.get_formals callee_proc_desc + |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar) + in + let captured_vars = + Procdesc.get_captured callee_proc_desc + |> List.map ~f:(fun {CapturedVar.name; capture_mode} -> + let pvar = Pvar.mk name callee_pname in + (Var.of_pvar pvar, capture_mode) ) + in + let<*> astate, captured_vars_with_actuals = + match actuals with + | (actual_closure, _) :: _ + when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) -> + (* Assumption: the first parameter will be a closure *) + PulseOperations.get_captured_actuals call_loc ~captured_vars ~actual_closure astate + | _ -> + Ok (astate, []) + in + let should_keep_at_most_one_disjunct = + Option.exists Config.pulse_cut_to_one_path_procedures_pattern ~f:(fun regex -> + Str.string_match regex (Procname.to_string callee_pname) 0 ) + in + if should_keep_at_most_one_disjunct then + L.d_printfln "Will keep at most one disjunct because %a is in blacklist" Procname.pp + callee_pname ; + (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *) + List.fold ~init:[] + (exec_states :> ExecutionDomain.t list) + ~f:(fun posts callee_exec_state -> + if should_keep_at_most_one_disjunct && not (List.is_empty posts) then posts + else + (* apply all pre/post specs *) + match + apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state + ~captured_vars_with_actuals ~formals ~actuals ~ret astate + with + | Unsat -> + (* couldn't apply pre/post pair *) + posts + | Sat post -> + post :: posts ) + | None -> + (* no spec found for some reason (unknown function, ...) *) + L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ; + let astate = + conservatively_initialize_args (get_arg_values ()) astate + |> unknown_call tenv call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt + in + [Ok (ContinueProgram astate)] diff --git a/infer/src/pulse/PulseCallOperations.mli b/infer/src/pulse/PulseCallOperations.mli new file mode 100644 index 000000000..af4da9ca4 --- /dev/null +++ b/infer/src/pulse/PulseCallOperations.mli @@ -0,0 +1,40 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open PulseBasicInterface +open PulseDomainInterface + +type t = AbductiveDomain.t + +val call : + Tenv.t + -> caller_proc_desc:Procdesc.t + -> callee_data:(Procdesc.t * PulseSummary.t) option + -> Location.t + -> Procname.t + -> ret:Ident.t * Typ.t + -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list + -> formals_opt:(Pvar.t * Typ.t) list option + -> t + -> ExecutionDomain.t AccessResult.t list +(** perform an interprocedural call: apply the summary for the call proc name passed as argument if + it exists *) + +val unknown_call : + Tenv.t + -> Location.t + -> CallEvent.t + -> ret:Ident.t * Typ.t + -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list + -> formals_opt:(Pvar.t * Typ.t) list option + -> t + -> t +(** performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and + the return value as appropriate *) + +val conservatively_initialize_args : AbstractValue.t list -> t -> t diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 4a8d8bafa..99e2e1f1a 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -99,7 +99,8 @@ module Misc = struct AnalysisCallbacks.proc_resolve_attributes callee_procname |> Option.map ~f:ProcAttributes.get_pvar_formals in - PulseOperations.unknown_call tenv location (Model skip_reason) ~ret ~actuals ~formals_opt astate + PulseCallOperations.unknown_call tenv location (Model skip_reason) ~ret ~actuals ~formals_opt + astate |> ok_continue @@ -246,7 +247,7 @@ module ObjC = struct | None -> ok_continue astate | Some callee_proc_name -> - PulseOperations.call tenv ~caller_proc_desc:proc_desc + PulseCallOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals:[] ~formals_opt:None astate ) end @@ -592,7 +593,7 @@ module StdFunction = struct :: List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ) ) in - PulseOperations.call tenv ~caller_proc_desc:proc_desc + PulseCallOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals ~formals_opt:None astate diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index b21ec3b3b..7acd7067e 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -548,174 +548,6 @@ let remove_vars tenv vars location orig_astate = astate -let is_ptr_to_const formal_typ_opt = - Option.value_map formal_typ_opt ~default:false ~f:(fun (formal_typ : Typ.t) -> - match formal_typ.desc with Typ.Tptr (t, _) -> Typ.is_const t.quals | _ -> false ) - - -let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = - let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in - let havoc_ret (ret, _) astate = havoc_id ret [event] astate in - let rec havoc_fields ((_, history) as addr) typ astate = - match typ.Typ.desc with - | Tstruct struct_name -> ( - match Tenv.lookup tenv struct_name with - | Some {fields} -> - List.fold fields ~init:astate ~f:(fun acc (field, field_typ, _) -> - let fresh_value = AbstractValue.mk_fresh () in - Memory.add_edge addr (FieldAccess field) (fresh_value, [event]) call_loc acc - |> havoc_fields (fresh_value, history) field_typ ) - | None -> - astate ) - | _ -> - astate - in - let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate = - (* We should not havoc when the corresponding formal is a - pointer to const *) - match actual_typ.Typ.desc with - | Tptr (typ, _) - when (not (Language.curr_language_is Java)) && not (is_ptr_to_const formal_typ_opt) -> - (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when - havoc'ing pointer parameters (which normally causes a [check_valid] call. *) - let fresh_value = AbstractValue.mk_fresh () in - Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate - |> havoc_fields actual typ - | _ -> - astate - in - let add_skipped_proc astate = - match reason with - | CallEvent.SkippedKnownCall proc_name -> - AbductiveDomain.add_skipped_call proc_name - (Trace.Immediate {location= call_loc; history= []}) - astate - | _ -> - astate - in - L.d_printfln "skipping unknown procedure@." ; - ( match formals_opt with - | None -> - List.fold actuals - ~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ None astate) - ~init:astate - | Some formals -> ( - match - List.fold2 actuals formals - ~f:(fun astate actual_typ (_, formal_typ) -> - havoc_actual_if_ptr actual_typ (Some formal_typ) astate ) - ~init:astate - with - | Unequal_lengths -> - L.d_printfln "ERROR: formals have length %d but actuals have length %d" - (List.length formals) (List.length actuals) ; - astate - | Ok result -> - result ) ) - |> havoc_ret ret |> add_skipped_proc - - -let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret - ~captured_vars_with_actuals ~formals ~actuals astate = - let map_call_result ~is_isl_error_prepost callee_prepost ~f = - match - PulseInterproc.apply_prepost ~is_isl_error_prepost callee_pname call_loc ~callee_prepost - ~captured_vars_with_actuals ~formals ~actuals astate - with - | (Sat (Error _) | Unsat) as path_result -> - path_result - | Sat (Ok (post, return_val_opt, subst)) -> - let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in - let post = - match return_val_opt with - | Some (return_val, return_hist) -> - write_id (fst ret) (return_val, event :: return_hist) post - | None -> - havoc_id (fst ret) [event] post - in - f subst post - in - let open ExecutionDomain in - let open SatUnsat.Import in - match callee_exec_state with - | ContinueProgram astate -> - map_call_result ~is_isl_error_prepost:false astate ~f:(fun _subst astate -> - Sat (Ok (ContinueProgram astate)) ) - | AbortProgram astate - | ExitProgram astate - | LatentAbortProgram {astate} - | LatentInvalidAccess {astate} -> - map_call_result ~is_isl_error_prepost:false - (astate :> AbductiveDomain.t) - ~f:(fun subst astate -> - let* astate_summary_result = - AbductiveDomain.summary_of_post tenv caller_proc_desc astate - >>| AccessResult.of_abductive_result - in - match astate_summary_result with - | Error _ as error -> - Sat error - | Ok (astate_summary : AbductiveDomain.summary) -> ( - match callee_exec_state with - | ContinueProgram _ | ISLLatentMemoryError _ -> - assert false - | AbortProgram _ -> - Sat (Ok (AbortProgram astate_summary)) - | ExitProgram _ -> - Sat (Ok (ExitProgram astate_summary)) - | LatentAbortProgram {latent_issue} -> ( - let latent_issue = - LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue - in - let diagnostic = LatentIssue.to_diagnostic latent_issue in - match LatentIssue.should_report astate_summary diagnostic with - | `DelayReport latent_issue -> - Sat (Ok (LatentAbortProgram {astate= astate_summary; latent_issue})) - | `ReportNow -> - Sat - (Error - (ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)})) - | `ISLDelay astate -> - Sat (Error (ISLError (astate :> AbductiveDomain.t))) ) - | LatentInvalidAccess {address= address_callee; must_be_valid; calling_context} -> ( - match AbstractValue.Map.find_opt address_callee subst with - | None -> - (* the address became unreachable so the bug can never be reached; drop it *) - Unsat - | Some (address, _history) -> ( - let calling_context = - (CallEvent.Call callee_pname, call_loc) :: calling_context - in - match - AbductiveDomain.find_post_cell_opt address (astate_summary :> AbductiveDomain.t) - |> Option.bind ~f:(fun (_, attrs) -> Attributes.get_invalid attrs) - with - | None -> - (* still no proof that the address is invalid *) - Sat - (Ok - (LatentInvalidAccess - {astate= astate_summary; address; must_be_valid; calling_context})) - | Some (invalidation, invalidation_trace) -> - Sat - (Error - (ReportableError - { diagnostic= - AccessToInvalidAddress - { calling_context - ; invalidation - ; invalidation_trace - ; access_trace= must_be_valid } - ; astate= (astate_summary :> AbductiveDomain.t) })) ) ) ) ) - | ISLLatentMemoryError astate -> - map_call_result ~is_isl_error_prepost:true - (astate :> AbductiveDomain.t) - ~f:(fun _subst astate -> - AbductiveDomain.summary_of_post tenv caller_proc_desc astate - >>| AccessResult.of_abductive_result - >>| Result.map ~f:(fun astate_summary -> ISLLatentMemoryError astate_summary) ) - - let get_captured_actuals location ~captured_vars ~actual_closure astate = let* astate, this_value_addr = eval_access Read location actual_closure Dereference astate in let+ _, astate, captured_vars_with_actuals = @@ -729,65 +561,3 @@ let get_captured_actuals location ~captured_vars ~actual_closure astate = (id + 1, astate, (var, captured_actual) :: captured) ) in (astate, captured_vars_with_actuals) - - -let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate) = - let reachable_values = BaseDomain.reachable_addresses_from arg_values (post :> BaseDomain.t) in - AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate - - -let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc - callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) = - let get_arg_values () = List.map actuals ~f:(fun ((value, _), _) -> value) in - match callee_data with - | Some (callee_proc_desc, exec_states) -> - let formals = - Procdesc.get_formals callee_proc_desc - |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar) - in - let captured_vars = - Procdesc.get_captured callee_proc_desc - |> List.map ~f:(fun {CapturedVar.name; capture_mode} -> - let pvar = Pvar.mk name callee_pname in - (Var.of_pvar pvar, capture_mode) ) - in - let<*> astate, captured_vars_with_actuals = - match actuals with - | (actual_closure, _) :: _ - when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) -> - (* Assumption: the first parameter will be a closure *) - get_captured_actuals call_loc ~captured_vars ~actual_closure astate - | _ -> - Ok (astate, []) - in - let should_keep_at_most_one_disjunct = - Option.exists Config.pulse_cut_to_one_path_procedures_pattern ~f:(fun regex -> - Str.string_match regex (Procname.to_string callee_pname) 0 ) - in - if should_keep_at_most_one_disjunct then - L.d_printfln "Will keep at most one disjunct because %a is in blacklist" Procname.pp - callee_pname ; - (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *) - List.fold ~init:[] - (exec_states :> ExecutionDomain.t list) - ~f:(fun posts callee_exec_state -> - if should_keep_at_most_one_disjunct && not (List.is_empty posts) then posts - else - (* apply all pre/post specs *) - match - apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state - ~captured_vars_with_actuals ~formals ~actuals ~ret astate - with - | Unsat -> - (* couldn't apply pre/post pair *) - posts - | Sat post -> - post :: posts ) - | None -> - (* no spec found for some reason (unknown function, ...) *) - L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ; - let astate = - conservatively_initialize_args (get_arg_values ()) astate - |> unknown_call tenv call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt - in - [Ok (ContinueProgram astate)] diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index e9b10ff96..7d6130180 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -197,30 +197,9 @@ val remove_vars : Tenv.t -> Var.t list -> Location.t -> t -> t AccessResult.t val check_address_escape : Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t AccessResult.t -val call : - Tenv.t - -> caller_proc_desc:Procdesc.t - -> callee_data:(Procdesc.t * PulseSummary.t) option - -> Location.t - -> Procname.t - -> ret:Ident.t * Typ.t - -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list - -> formals_opt:(Pvar.t * Typ.t) list option - -> t - -> ExecutionDomain.t AccessResult.t list -(** perform an interprocedural call: apply the summary for the call proc name passed as argument if - it exists *) - -val unknown_call : - Tenv.t - -> Location.t - -> CallEvent.t - -> ret:Ident.t * Typ.t - -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list - -> formals_opt:(Pvar.t * Typ.t) list option - -> t +val get_captured_actuals : + Location.t + -> captured_vars:(Var.t * Pvar.capture_mode) list + -> actual_closure:AbstractValue.t * ValueHistory.t -> t -(** performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and - the return value as appropriate *) - -val conservatively_initialize_args : AbstractValue.t list -> t -> t + -> (t * (Var.t * (AbstractValue.t * ValueHistory.t)) list) AccessResult.t