From 5a2b285fffe0e0ab65fcede7018f8a12e1a2c5ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 8 Apr 2020 03:18:30 -0700 Subject: [PATCH] [pulse] Distinguish exit state at top level Summary: This diff lifts the `PulseAbductiveDomain.t` in `PulseExecutionState` by tracking whether the program continues the analysis normally or exits unusually (e.g. by calling `exit` or `throw`): ``` type exec_state = | ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *) | ExitProgram of PulseAbductiveDomain.t (** represents the state originating at exit/divergence. *) ``` Now, Pulse's actual domain is tracked by `PulseExecutionState` and as soon as we try to analyze an instruction at `ExitProgram`, we simply return its state. The aim is to recover the state at the time of the exit, rather than simply ignoring them (i.e. returning empty disjuncts). This allows us to get rid of some FNs that we were not able to detect before. Moreover, it also allows the impurity analysis to be more precise since we will know how the state changed up to exit. TODO: - Impurity analysis needs to be improved to consider functions that simply exit as impure. - The next goal is to handle error state similarly so that when pulse finds an error, we recover the state at the error location (and potentially continue to analyze?). Disclaimer: currently, we handle throw statements like exit (as was the case before). However, this is not correct. Ideally, control flow from throw nodes follows catch nodes rather than exiting the program entirely. Reviewed By: jvillard Differential Revision: D20791747 fbshipit-source-id: df9e5445a --- infer/src/checkers/impurity.ml | 37 +- infer/src/pulse/Pulse.ml | 133 +- infer/src/pulse/PulseAbductiveDomain.ml | 1368 ++++++++--------- infer/src/pulse/PulseAbductiveDomain.mli | 36 +- infer/src/pulse/PulseExecutionState.ml | 43 + infer/src/pulse/PulseExecutionState.mli | 20 + infer/src/pulse/PulseModels.ml | 92 +- infer/src/pulse/PulseModels.mli | 2 +- infer/src/pulse/PulseOperations.ml | 54 +- infer/src/pulse/PulseOperations.mli | 4 +- infer/src/pulse/PulseSummary.ml | 7 +- infer/src/pulse/PulseSummary.mli | 4 +- .../codetoanalyze/cpp/impurity/exit_test.cpp | 20 + .../codetoanalyze/cpp/pulse/exit_test.cpp | 29 + .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + .../codetoanalyze/cpp/pulse/throw_test.cpp | 35 + .../codetoanalyze/java/impurity/Test.java | 11 +- .../codetoanalyze/java/impurity/issues.exp | 2 +- 18 files changed, 1045 insertions(+), 853 deletions(-) create mode 100644 infer/src/pulse/PulseExecutionState.ml create mode 100644 infer/src/pulse/PulseExecutionState.mli create mode 100644 infer/tests/codetoanalyze/cpp/impurity/exit_test.cpp create mode 100644 infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp create mode 100644 infer/tests/codetoanalyze/cpp/pulse/throw_test.cpp diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 5429457bf..554be4d71 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -138,21 +138,24 @@ let is_modeled_pure tenv pname = (** Given Pulse summary, extract impurity info, i.e. parameters and global variables that are modified by the function and skipped functions. *) -let extract_impurity tenv pdesc pre_post : ImpurityDomain.t = - let pre_heap = (AbductiveDomain.PrePost.get_pre pre_post).BaseDomain.heap in - let post = AbductiveDomain.PrePost.get_post pre_post in - let post_stack = post.BaseDomain.stack in - let pname = Procdesc.get_proc_name pdesc in - let modified_params = - Procdesc.get_formals pdesc |> get_modified_params pname post_stack pre_heap post - in - let modified_globals = get_modified_globals pre_heap post post_stack in - let skipped_calls = - AbductiveDomain.PrePost.get_skipped_calls pre_post - |> PulseAbductiveDomain.SkippedCalls.filter (fun proc_name _ -> - Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) ) - in - {modified_globals; modified_params; skipped_calls} +let extract_impurity tenv pdesc (exec_state : PulseExecutionState.t) : ImpurityDomain.t = + match exec_state with + | ExitProgram astate | ContinueProgram astate -> + (* TODO: consider impure even though the program only exits with pre=post *) + let pre_heap = (PulseAbductiveDomain.get_pre astate).BaseDomain.heap in + let post = PulseAbductiveDomain.get_post astate in + let post_stack = post.BaseDomain.stack in + let pname = Procdesc.get_proc_name pdesc in + let modified_params = + Procdesc.get_formals pdesc |> get_modified_params pname post_stack pre_heap post + in + let modified_globals = get_modified_globals pre_heap post post_stack in + let skipped_calls = + PulseAbductiveDomain.get_skipped_calls astate + |> PulseAbductiveDomain.SkippedCalls.filter (fun proc_name _ -> + Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) ) + in + {modified_globals; modified_params; skipped_calls} let checker {exe_env; Callbacks.summary} : Summary.t = @@ -177,8 +180,8 @@ let checker {exe_env; Callbacks.summary} : Summary.t = impure_fun_desc | Some pre_posts -> let (ImpurityDomain.{modified_globals; modified_params; skipped_calls} as impurity_astate) = - List.fold pre_posts ~init:ImpurityDomain.pure ~f:(fun acc pre_post -> - let modified = extract_impurity tenv pdesc pre_post in + List.fold pre_posts ~init:ImpurityDomain.pure ~f:(fun acc exec_state -> + let modified = extract_impurity tenv pdesc exec_state in ImpurityDomain.join acc modified ) in if Purity.should_report proc_name && not (ImpurityDomain.is_pure impurity_astate) then diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 4ce60489b..2075ad407 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -27,6 +27,10 @@ let check_error summary = function raise_notrace AbstractDomain.Stop_analysis +let check_error_continue summary result = + PulseExecutionState.ContinueProgram (check_error summary result) + + let proc_name_of_call call_exp = match (call_exp : Exp.t) with | Const (Cfun proc_name) | Closure {name= proc_name} -> @@ -39,7 +43,7 @@ type get_formals = Procname.t -> (Pvar.t * Typ.t) list option module PulseTransferFunctions = struct module CFG = ProcCfg.Normal - module Domain = PulseAbductiveDomain + module Domain = PulseExecutionState type extras = get_formals @@ -50,9 +54,9 @@ module PulseTransferFunctions = struct PulseOperations.call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt astate | _ -> L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; - Ok - [ PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals - ~formals_opt:None astate ] + PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals + ~formals_opt:None astate + |> PulseOperations.ok_continue (** has an object just gone out of scope? *) @@ -70,11 +74,16 @@ module PulseTransferFunctions = struct (** [out_of_scope_access_expr] has just gone out of scope and in now invalid *) - let exec_object_out_of_scope call_loc (pvar, typ) astate = - let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in - (* invalidate [&x] *) - let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in - PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate + let exec_object_out_of_scope call_loc (pvar, typ) exec_state = + match exec_state with + | PulseExecutionState.ContinueProgram astate -> + let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in + let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in + (* invalidate [&x] *) + PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate + >>| PulseExecutionState.continue + | PulseExecutionState.ExitProgram _ -> + Ok exec_state let dispatch_call tenv summary ret call_exp actuals call_loc flags get_formals astate = @@ -99,7 +108,7 @@ module PulseTransferFunctions = struct None in (* do interprocedural call then destroy objects going out of scope *) - let posts = + let exec_state_res = match model with | Some (model, callee_procname) -> L.d_printfln "Found model for call@\n" ; @@ -121,59 +130,67 @@ module PulseTransferFunctions = struct match get_out_of_scope_object call_exp actuals flags with | Some pvar_typ -> L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ; - let* posts = posts in - List.map posts ~f:(fun astate -> exec_object_out_of_scope call_loc pvar_typ astate) + let* exec_states = exec_state_res in + List.map exec_states ~f:(fun exec_state -> + exec_object_out_of_scope call_loc pvar_typ exec_state ) |> Result.all | None -> - posts + exec_state_res let exec_instr (astate : Domain.t) {tenv; ProcData.summary; extras= get_formals} _cfg_node - (instr : Sil.instr) = - match instr with - | Load {id= lhs_id; e= rhs_exp; loc} -> - (* [lhs_id := *rhs_exp] *) - let result = - let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in - PulseOperations.write_id lhs_id rhs_addr_hist astate - in - [check_error summary 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) = PulseOperations.eval loc rhs_exp astate in - let* astate, lhs_addr_hist = PulseOperations.eval loc lhs_exp astate in - let* astate = - PulseOperations.write_deref loc ~ref:lhs_addr_hist - ~obj:(rhs_addr, event :: rhs_history) - astate - in - match lhs_exp with - | Lvar pvar when Pvar.is_return pvar -> - PulseOperations.check_address_escape loc summary.Summary.proc_desc rhs_addr - rhs_history astate - | _ -> - Ok astate - in - [check_error summary result] - | Prune (condition, loc, is_then_branch, if_kind) -> - let post, cond_satisfiable = - PulseOperations.prune ~is_then_branch if_kind loc ~condition astate |> check_error summary - in - if cond_satisfiable then (* [condition] is true or unknown value: go into the branch *) - [post] - else (* [condition] is known to be unsatisfiable: prune path *) [] - | Call (ret, call_exp, actuals, loc, call_flags) -> - dispatch_call tenv summary ret call_exp actuals loc call_flags get_formals astate - |> check_error summary - | Metadata (ExitScope (vars, location)) -> - let astate = PulseOperations.remove_vars vars location astate in - [check_error summary astate] - | Metadata (VariableLifetimeBegins (pvar, _, location)) -> - [PulseOperations.realloc_pvar pvar location astate] - | Metadata (Abstract _ | Nullify _ | Skip) -> + (instr : Sil.instr) : Domain.t list = + match astate with + | ExitProgram _ -> + (* program already exited, simply propagate the exited state upwards *) [astate] + | ContinueProgram astate -> ( + match instr with + | Load {id= lhs_id; e= rhs_exp; loc} -> + (* [lhs_id := *rhs_exp] *) + let result = + let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in + PulseOperations.write_id lhs_id rhs_addr_hist astate + in + [check_error_continue summary 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) = PulseOperations.eval loc rhs_exp astate in + let* astate, lhs_addr_hist = PulseOperations.eval loc lhs_exp astate in + let* astate = + PulseOperations.write_deref loc ~ref:lhs_addr_hist + ~obj:(rhs_addr, event :: rhs_history) + astate + in + match lhs_exp with + | Lvar pvar when Pvar.is_return pvar -> + PulseOperations.check_address_escape loc summary.Summary.proc_desc rhs_addr + rhs_history astate + | _ -> + Ok astate + in + [check_error_continue summary result] + | Prune (condition, loc, is_then_branch, if_kind) -> + let exec_state, cond_satisfiable = + PulseOperations.prune ~is_then_branch if_kind loc ~condition astate + |> check_error summary + in + if cond_satisfiable then + (* [condition] is true or unknown value: go into the branch *) + [Domain.continue exec_state] + else (* [condition] is known to be unsatisfiable: prune path *) [] + | Call (ret, call_exp, actuals, loc, call_flags) -> + dispatch_call tenv summary ret call_exp actuals loc call_flags get_formals astate + |> check_error summary + | Metadata (ExitScope (vars, location)) -> + let astate = PulseOperations.remove_vars vars location astate in + [check_error_continue summary astate] + | Metadata (VariableLifetimeBegins (pvar, _, location)) -> + [PulseOperations.realloc_pvar pvar location astate |> Domain.continue] + | Metadata (Abstract _ | Nullify _ | Skip) -> + [Domain.ContinueProgram astate] ) let pp_session_name _node fmt = F.pp_print_string fmt "Pulse" @@ -197,7 +214,7 @@ let checker {Callbacks.exe_env; summary} = AbstractValue.init () ; let pdesc = Summary.get_proc_desc summary in let initial = - DisjunctiveTransferFunctions.Disjuncts.singleton (PulseAbductiveDomain.mk_initial pdesc) + DisjunctiveTransferFunctions.Disjuncts.singleton (PulseExecutionState.mk_initial pdesc) in let get_formals callee_pname = Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 22d922b38..610a7beb6 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -362,741 +362,725 @@ let set_post_cell (addr, history) (edges_map, attr_set) location astate = |> BaseAddressAttributes.add addr attr_set ) -module PrePost = struct - type domain_t = t +let filter_for_summary astate = + let post_stack = + BaseStack.filter + (fun var _ -> Var.appears_in_source_code var && not (is_local var astate)) + (astate.post :> BaseDomain.t).stack + in + (* deregister empty edges *) + let deregister_empty heap = + BaseMemory.filter (fun _addr edges -> not (BaseMemory.Edges.is_empty edges)) heap + in + let pre_heap = deregister_empty (astate.pre :> base_domain).heap in + let post_heap = deregister_empty (astate.post :> base_domain).heap in + { astate with + pre= PreDomain.update astate.pre ~heap:pre_heap + ; post= Domain.update ~stack:post_stack ~heap:post_heap astate.post } - type t = domain_t - let filter_for_summary astate = - let post_stack = - BaseStack.filter - (fun var _ -> Var.appears_in_source_code var && not (is_local var astate)) - (astate.post :> BaseDomain.t).stack - in - (* deregister empty edges *) - let deregister_empty heap = - BaseMemory.filter (fun _addr edges -> not (BaseMemory.Edges.is_empty edges)) heap - in - let pre_heap = deregister_empty (astate.pre :> base_domain).heap in - let post_heap = deregister_empty (astate.post :> base_domain).heap in - { astate with - pre= PreDomain.update astate.pre ~heap:pre_heap - ; post= Domain.update ~stack:post_stack ~heap:post_heap astate.post } - - - let add_out_of_scope_attribute addr pvar location history heap typ = - BaseAddressAttributes.add_one addr - (Invalid (GoneOutOfScope (pvar, typ), Immediate {location; history})) - heap - - - (** invalidate local variables going out of scope *) - let invalidate_locals pdesc astate : t = - let attrs : BaseAddressAttributes.t = (astate.post :> BaseDomain.t).attrs in - let attrs' = - BaseAddressAttributes.fold - (fun addr attrs acc -> - Attributes.get_address_of_stack_variable attrs - |> Option.value_map ~default:acc ~f:(fun (var, location, history) -> - let get_local_typ_opt pvar = - Procdesc.get_locals pdesc - |> List.find_map ~f:(fun ProcAttributes.{name; typ} -> - if Mangled.equal name (Pvar.get_name pvar) then Some typ else None ) - in - match var with - | Var.ProgramVar pvar -> - get_local_typ_opt pvar - |> Option.value_map ~default:acc - ~f:(add_out_of_scope_attribute addr pvar location history acc) - | _ -> - acc ) ) - attrs attrs - in - if phys_equal attrs attrs' then astate - else {astate with pre= astate.pre; post= Domain.update astate.post ~attrs:attrs'} - - - let of_post pdesc astate = - let domain = filter_for_summary astate in - let domain, _ = discard_unreachable domain in - invalidate_locals pdesc domain - - - (* {2 machinery to apply a pre/post pair corresponding to a function's summary in a function call - to the current state} *) - - module AddressSet = AbstractValue.Set - module AddressMap = AbstractValue.Map - - (** stuff we carry around when computing the result of applying one pre/post pair *) - type call_state = - { astate: domain_t (** caller's abstract state computed so far *) - ; subst: (AbstractValue.t * ValueHistory.t) AddressMap.t - (** translation from callee addresses to caller addresses and their caller histories *) - ; rev_subst: AbstractValue.t AddressMap.t - (** the inverse translation from [subst] from caller addresses to callee addresses *) - ; visited: AddressSet.t - (** set of callee addresses that have been visited already - - NOTE: this is not always equal to the domain of [rev_subst]: when applying the post we - visit each subgraph from each formal independently so we reset [visited] between the - visit of each formal *) } - - let pp_call_state fmt {astate; subst; rev_subst; visited} = - F.fprintf fmt - "@[{ astate=@[%a@];@,\ - \ subst=@[%a@];@,\ - \ rev_subst=@[%a@];@,\ - \ visited=@[%a@]@,\ - \ }@]" pp astate - (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr)) - subst - (AddressMap.pp ~pp_value:AbstractValue.pp) - rev_subst AddressSet.pp visited - - - type contradiction = - | Aliasing of - { addr_caller: AbstractValue.t - ; addr_callee: AbstractValue.t - ; addr_callee': AbstractValue.t - ; call_state: call_state } - (** raised when the precondition and the current state disagree on the aliasing, i.e. some - addresses [callee_addr] and [callee_addr'] that are distinct in the pre are aliased to a - single address [caller_addr] in the caller's current state. Typically raised when - calling [foo(z,z)] where the spec for [foo(x,y)] says that [x] and [y] are disjoint. *) - | CItv of - { addr_caller: AbstractValue.t - ; addr_callee: AbstractValue.t - ; arith_caller: CItv.t option - ; arith_callee: CItv.t option - ; call_state: call_state } - (** raised when the pre asserts arithmetic facts that are demonstrably false in the caller - state *) - | ArithmeticBo of - { addr_caller: AbstractValue.t - ; addr_callee: AbstractValue.t - ; arith_callee: Itv.ItvPure.t - ; call_state: call_state } - (** raised when the pre asserts arithmetic facts that are demonstrably false in the caller - state *) - | FormalActualLength of - {formals: Var.t list; actuals: ((AbstractValue.t * ValueHistory.t) * Typ.t) list} - - let pp_contradiction fmt = function - | Aliasing {addr_caller; addr_callee; addr_callee'; call_state} -> - F.fprintf fmt - "address %a in caller already bound to %a, not %a@\nnote: current call state was %a" - AbstractValue.pp addr_caller AbstractValue.pp addr_callee' AbstractValue.pp addr_callee - pp_call_state call_state - | CItv {addr_caller; addr_callee; arith_caller; arith_callee; call_state} -> - F.fprintf fmt - "caller addr %a%a but callee addr %a%a; %a=%a is unsatisfiable@\n\ - note: current call state was %a" AbstractValue.pp addr_caller (Pp.option CItv.pp) - arith_caller AbstractValue.pp addr_callee (Pp.option CItv.pp) arith_callee - AbstractValue.pp addr_caller AbstractValue.pp addr_callee pp_call_state call_state - | ArithmeticBo {addr_caller; addr_callee; arith_callee; call_state} -> - F.fprintf fmt - "callee addr %a%a is incompatible with caller addr %a's arithmetic constraints@\n\ - note: current call state was %a" AbstractValue.pp addr_callee Itv.ItvPure.pp arith_callee - AbstractValue.pp addr_caller pp_call_state call_state - | FormalActualLength {formals; actuals} -> - F.fprintf fmt "formals have length %d but actuals have length %d" (List.length formals) - (List.length actuals) - - - exception Contradiction of contradiction - - let fold_globals_of_stack call_loc stack call_state ~f = - Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:BaseStack.fold) - stack ~init:call_state ~f:(fun call_state (var, stack_value) -> - match var with - | Var.ProgramVar pvar when Pvar.is_global pvar -> - let call_state, addr_hist_caller = - let astate, var_value = - Stack.eval [ValueHistory.VariableAccessed (pvar, call_loc)] var call_state.astate - in - if phys_equal astate call_state.astate then (call_state, var_value) - else ({call_state with astate}, var_value) +let add_out_of_scope_attribute addr pvar location history heap typ = + BaseAddressAttributes.add_one addr + (Invalid (GoneOutOfScope (pvar, typ), Immediate {location; history})) + heap + + +(** invalidate local variables going out of scope *) +let invalidate_locals pdesc astate : t = + let attrs : BaseAddressAttributes.t = (astate.post :> BaseDomain.t).attrs in + let attrs' = + BaseAddressAttributes.fold + (fun addr attrs acc -> + Attributes.get_address_of_stack_variable attrs + |> Option.value_map ~default:acc ~f:(fun (var, location, history) -> + let get_local_typ_opt pvar = + Procdesc.get_locals pdesc + |> List.find_map ~f:(fun ProcAttributes.{name; typ} -> + if Mangled.equal name (Pvar.get_name pvar) then Some typ else None ) + in + match var with + | Var.ProgramVar pvar -> + get_local_typ_opt pvar + |> Option.value_map ~default:acc + ~f:(add_out_of_scope_attribute addr pvar location history acc) + | _ -> + acc ) ) + attrs attrs + in + if phys_equal attrs attrs' then astate + else {astate with pre= astate.pre; post= Domain.update astate.post ~attrs:attrs'} + + +let of_post pdesc astate = + let domain = filter_for_summary astate in + let domain, _ = discard_unreachable domain in + invalidate_locals pdesc domain + + +(* {2 machinery to apply a pre/post pair corresponding to a function's summary in a function call + to the current state} *) + +module AddressSet = AbstractValue.Set +module AddressMap = AbstractValue.Map + +(** stuff we carry around when computing the result of applying one pre/post pair *) +type call_state = + { astate: t (** caller's abstract state computed so far *) + ; subst: (AbstractValue.t * ValueHistory.t) AddressMap.t + (** translation from callee addresses to caller addresses and their caller histories *) + ; rev_subst: AbstractValue.t AddressMap.t + (** the inverse translation from [subst] from caller addresses to callee addresses *) + ; visited: AddressSet.t + (** set of callee addresses that have been visited already + + NOTE: this is not always equal to the domain of [rev_subst]: when applying the post we + visit each subgraph from each formal independently so we reset [visited] between the + visit of each formal *) } + +let pp_call_state fmt {astate; subst; rev_subst; visited} = + F.fprintf fmt + "@[{ astate=@[%a@];@,\ + \ subst=@[%a@];@,\ + \ rev_subst=@[%a@];@,\ + \ visited=@[%a@]@,\ + \ }@]" pp astate + (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr)) + subst + (AddressMap.pp ~pp_value:AbstractValue.pp) + rev_subst AddressSet.pp visited + + +type contradiction = + | Aliasing of + { addr_caller: AbstractValue.t + ; addr_callee: AbstractValue.t + ; addr_callee': AbstractValue.t + ; call_state: call_state } + (** raised when the precondition and the current state disagree on the aliasing, i.e. some + addresses [callee_addr] and [callee_addr'] that are distinct in the pre are aliased to a + single address [caller_addr] in the caller's current state. Typically raised when calling + [foo(z,z)] where the spec for [foo(x,y)] says that [x] and [y] are disjoint. *) + | CItv of + { addr_caller: AbstractValue.t + ; addr_callee: AbstractValue.t + ; arith_caller: CItv.t option + ; arith_callee: CItv.t option + ; call_state: call_state } + (** raised when the pre asserts arithmetic facts that are demonstrably false in the caller + state *) + | ArithmeticBo of + { addr_caller: AbstractValue.t + ; addr_callee: AbstractValue.t + ; arith_callee: Itv.ItvPure.t + ; call_state: call_state } + (** raised when the pre asserts arithmetic facts that are demonstrably false in the caller + state *) + | FormalActualLength of + {formals: Var.t list; actuals: ((AbstractValue.t * ValueHistory.t) * Typ.t) list} + +let pp_contradiction fmt = function + | Aliasing {addr_caller; addr_callee; addr_callee'; call_state} -> + F.fprintf fmt + "address %a in caller already bound to %a, not %a@\nnote: current call state was %a" + AbstractValue.pp addr_caller AbstractValue.pp addr_callee' AbstractValue.pp addr_callee + pp_call_state call_state + | CItv {addr_caller; addr_callee; arith_caller; arith_callee; call_state} -> + F.fprintf fmt + "caller addr %a%a but callee addr %a%a; %a=%a is unsatisfiable@\n\ + note: current call state was %a" AbstractValue.pp addr_caller (Pp.option CItv.pp) + arith_caller AbstractValue.pp addr_callee (Pp.option CItv.pp) arith_callee AbstractValue.pp + addr_caller AbstractValue.pp addr_callee pp_call_state call_state + | ArithmeticBo {addr_caller; addr_callee; arith_callee; call_state} -> + F.fprintf fmt + "callee addr %a%a is incompatible with caller addr %a's arithmetic constraints@\n\ + note: current call state was %a" AbstractValue.pp addr_callee Itv.ItvPure.pp arith_callee + AbstractValue.pp addr_caller pp_call_state call_state + | FormalActualLength {formals; actuals} -> + F.fprintf fmt "formals have length %d but actuals have length %d" (List.length formals) + (List.length actuals) + + +exception Contradiction of contradiction + +let fold_globals_of_stack call_loc stack call_state ~f = + Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:BaseStack.fold) + stack ~init:call_state ~f:(fun call_state (var, stack_value) -> + match var with + | Var.ProgramVar pvar when Pvar.is_global pvar -> + let call_state, addr_hist_caller = + let astate, var_value = + Stack.eval [ValueHistory.VariableAccessed (pvar, call_loc)] var call_state.astate in - f pvar ~stack_value ~addr_hist_caller call_state - | _ -> - Ok call_state ) - - - let visit call_state ~addr_callee ~addr_hist_caller = - let addr_caller = fst addr_hist_caller in - ( match AddressMap.find_opt addr_caller call_state.rev_subst with - | Some addr_callee' when not (AbstractValue.equal addr_callee addr_callee') -> - raise (Contradiction (Aliasing {addr_caller; addr_callee; addr_callee'; call_state})) - | _ -> - () ) ; - if AddressSet.mem addr_callee call_state.visited then (`AlreadyVisited, call_state) - else - ( `NotAlreadyVisited - , { call_state with - visited= AddressSet.add addr_callee call_state.visited - ; subst= AddressMap.add addr_callee addr_hist_caller call_state.subst - ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } ) - - - let pp f {pre; post; skipped_calls} = - F.fprintf f "PRE:@\n @[%a@]@\n" BaseDomain.pp (pre :> BaseDomain.t) ; - F.fprintf f "POST:@\n @[%a@]@\n" BaseDomain.pp (post :> BaseDomain.t) ; - F.fprintf f "SKIPPED_CALLS:@ @[%a@]@\n" SkippedCalls.pp skipped_calls - - - (* {3 reading the pre from the current state} *) - - let add_call_to_trace proc_name call_location caller_history in_call = - Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call} - - - (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in - [call_state.astate] starting from address [addr_caller]. Report an error if some invalid - addresses are traversed in the process. *) - let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre - ~addr_hist_caller call_state = - match visit call_state ~addr_callee:addr_pre ~addr_hist_caller with - | `AlreadyVisited, call_state -> - Ok call_state - | `NotAlreadyVisited, call_state -> ( - match BaseMemory.find_opt addr_pre pre.BaseDomain.heap with - | None -> - Ok call_state - | Some edges_pre -> - Container.fold_result - ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) - ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) -> - let astate, addr_hist_dest_caller = - Memory.eval_edge addr_hist_caller access call_state.astate - in - let call_state = {call_state with astate} in - materialize_pre_from_address callee_proc_name call_location ~pre - ~addr_pre:addr_pre_dest ~addr_hist_caller:addr_hist_dest_caller call_state ) ) - - - (** materialize subgraph of [pre] rooted at the address represented by a [formal] parameter that - has been instantiated with the corresponding [actual] into the current state - [call_state.astate] *) - let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state = - L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractValue.pp (fst actual) ; - (let open IOption.Let_syntax in - let* addr_formal_pre, _ = BaseStack.find_opt formal pre.BaseDomain.stack in - let+ formal_pre, _ = BaseMemory.find_edge_opt addr_formal_pre Dereference pre.BaseDomain.heap in - materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:formal_pre - ~addr_hist_caller:actual call_state) - |> function Some result -> result | None -> Ok call_state - - - let is_cell_read_only ~edges_pre_opt ~cell_post:(edges_post, attrs_post) = - match edges_pre_opt with + if phys_equal astate call_state.astate then (call_state, var_value) + else ({call_state with astate}, var_value) + in + f pvar ~stack_value ~addr_hist_caller call_state + | _ -> + Ok call_state ) + + +let visit call_state ~addr_callee ~addr_hist_caller = + let addr_caller = fst addr_hist_caller in + ( match AddressMap.find_opt addr_caller call_state.rev_subst with + | Some addr_callee' when not (AbstractValue.equal addr_callee addr_callee') -> + raise (Contradiction (Aliasing {addr_caller; addr_callee; addr_callee'; call_state})) + | _ -> + () ) ; + if AddressSet.mem addr_callee call_state.visited then (`AlreadyVisited, call_state) + else + ( `NotAlreadyVisited + , { call_state with + visited= AddressSet.add addr_callee call_state.visited + ; subst= AddressMap.add addr_callee addr_hist_caller call_state.subst + ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } ) + + +let pp f {pre; post; skipped_calls} = + F.fprintf f "PRE:@\n @[%a@]@\n" BaseDomain.pp (pre :> BaseDomain.t) ; + F.fprintf f "POST:@\n @[%a@]@\n" BaseDomain.pp (post :> BaseDomain.t) ; + F.fprintf f "SKIPPED_CALLS:@ @[%a@]@\n" SkippedCalls.pp skipped_calls + + +(* {3 reading the pre from the current state} *) + +let add_call_to_trace proc_name call_location caller_history in_call = + Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call} + + +(** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in + [call_state.astate] starting from address [addr_caller]. Report an error if some invalid + addresses are traversed in the process. *) +let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre ~addr_hist_caller + call_state = + match visit call_state ~addr_callee:addr_pre ~addr_hist_caller with + | `AlreadyVisited, call_state -> + Ok call_state + | `NotAlreadyVisited, call_state -> ( + match BaseMemory.find_opt addr_pre pre.BaseDomain.heap with | None -> - false - | Some edges_pre when not (Attributes.is_modified attrs_post) -> - let are_edges_equal = - BaseMemory.Edges.equal - (fun (addr_dest_pre, _) (addr_dest_post, _) -> - (* NOTE: ignores traces - - TODO: can the traces be leveraged here? maybe easy to detect writes by looking at - the post trace *) - AbstractValue.equal addr_dest_pre addr_dest_post ) - edges_pre edges_post - in - if CommandLineOption.strict_mode then assert are_edges_equal ; - are_edges_equal - | _ -> - false + Ok call_state + | Some edges_pre -> + Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) + ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) -> + let astate, addr_hist_dest_caller = + Memory.eval_edge addr_hist_caller access call_state.astate + in + let call_state = {call_state with astate} in + materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:addr_pre_dest + ~addr_hist_caller:addr_hist_dest_caller call_state ) ) + + +(** materialize subgraph of [pre] rooted at the address represented by a [formal] parameter that has + been instantiated with the corresponding [actual] into the current state [call_state.astate] *) +let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state = + L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractValue.pp (fst actual) ; + (let open IOption.Let_syntax in + let* addr_formal_pre, _ = BaseStack.find_opt formal pre.BaseDomain.stack in + let+ formal_pre, _ = BaseMemory.find_edge_opt addr_formal_pre Dereference pre.BaseDomain.heap in + materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:formal_pre + ~addr_hist_caller:actual call_state) + |> function Some result -> result | None -> Ok call_state + + +let is_cell_read_only ~edges_pre_opt ~cell_post:(edges_post, attrs_post) = + match edges_pre_opt with + | None -> + false + | Some edges_pre when not (Attributes.is_modified attrs_post) -> + let are_edges_equal = + BaseMemory.Edges.equal + (fun (addr_dest_pre, _) (addr_dest_post, _) -> + (* NOTE: ignores traces + + TODO: can the traces be leveraged here? maybe easy to detect writes by looking at + the post trace *) + AbstractValue.equal addr_dest_pre addr_dest_post ) + edges_pre edges_post + in + if CommandLineOption.strict_mode then assert are_edges_equal ; + are_edges_equal + | _ -> + false - let materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals - call_state = - (* For each [(formal, actual)] pair, resolve them to addresses in their respective states then - call [materialize_pre_from] on them. Give up if calling the function introduces aliasing. - *) +let materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals + call_state = + (* For each [(formal, actual)] pair, resolve them to addresses in their respective states then + call [materialize_pre_from] on them. Give up if calling the function introduces aliasing. + *) + match + IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal (actual, _) -> + materialize_pre_from_actual callee_proc_name call_location + ~pre:(pre_post.pre :> BaseDomain.t) + ~formal ~actual call_state ) + with + | Unequal_lengths -> + raise (Contradiction (FormalActualLength {formals; actuals})) + | Ok result -> + result + + +let materialize_pre_for_globals callee_proc_name call_location pre_post call_state = + fold_globals_of_stack call_location (pre_post.pre :> BaseDomain.t).stack call_state + ~f:(fun _var ~stack_value:(addr_pre, _) ~addr_hist_caller call_state -> + materialize_pre_from_address callee_proc_name call_location + ~pre:(pre_post.pre :> BaseDomain.t) + ~addr_pre ~addr_hist_caller call_state ) + + +let eval_sym_of_subst astate subst s bound_end = + let v = Symb.Symbol.get_pulse_value_exn s in + match PulseAbstractValue.Map.find_opt v !subst with + | Some (v', _) -> + Itv.ItvPure.get_bound (AddressAttributes.get_bo_itv v' astate) bound_end + | None -> + let v' = PulseAbstractValue.mk_fresh () in + subst := PulseAbstractValue.Map.add v (v', []) !subst ; + Bounds.Bound.of_pulse_value v' + + +let subst_attribute call_state subst_ref astate ~addr_caller attr ~addr_callee = + match (attr : Attribute.t) with + | CItv (arith_callee, hist) -> ( + let arith_caller_opt = AddressAttributes.get_citv addr_caller astate |> Option.map ~f:fst in + match CItv.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) with + | Unsatisfiable -> + raise + (Contradiction + (CItv + { addr_caller + ; addr_callee + ; arith_caller= arith_caller_opt + ; arith_callee= Some arith_callee + ; call_state })) + | Satisfiable (Some abduce_caller, _abduce_callee) -> + Attribute.CItv (abduce_caller, hist) + | Satisfiable (None, _) -> + attr ) + | BoItv itv -> ( match - IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal (actual, _) -> - materialize_pre_from_actual callee_proc_name call_location - ~pre:(pre_post.pre :> BaseDomain.t) - ~formal ~actual call_state ) + Itv.ItvPure.subst itv (fun symb bound -> + AbstractDomain.Types.NonBottom (eval_sym_of_subst astate subst_ref symb bound) ) with - | Unequal_lengths -> - raise (Contradiction (FormalActualLength {formals; actuals})) - | Ok result -> - result - - - let materialize_pre_for_globals callee_proc_name call_location pre_post call_state = - fold_globals_of_stack call_location (pre_post.pre :> BaseDomain.t).stack call_state - ~f:(fun _var ~stack_value:(addr_pre, _) ~addr_hist_caller call_state -> - materialize_pre_from_address callee_proc_name call_location - ~pre:(pre_post.pre :> BaseDomain.t) - ~addr_pre ~addr_hist_caller call_state ) - - - let eval_sym_of_subst astate subst s bound_end = - let v = Symb.Symbol.get_pulse_value_exn s in - match PulseAbstractValue.Map.find_opt v !subst with - | Some (v', _) -> - Itv.ItvPure.get_bound (AddressAttributes.get_bo_itv v' astate) bound_end - | None -> - let v' = PulseAbstractValue.mk_fresh () in - subst := PulseAbstractValue.Map.add v (v', []) !subst ; - Bounds.Bound.of_pulse_value v' - - - let subst_attribute call_state subst_ref astate ~addr_caller attr ~addr_callee = + | NonBottom itv' -> + Attribute.BoItv itv' + | Bottom -> + raise + (Contradiction (ArithmeticBo {addr_callee; addr_caller; arith_callee= itv; call_state})) ) + | AddressOfCppTemporary _ + | AddressOfStackVariable _ + | Allocated _ + | Closure _ + | Invalid _ + | MustBeValid _ + | StdVectorReserve + | WrittenTo _ -> + (* non-relational attributes *) + attr + + +let add_call_to_attributes proc_name call_location ~addr_callee ~addr_caller caller_history attrs + call_state = + let add_call_to_attribute attr = match (attr : Attribute.t) with - | CItv (arith_callee, hist) -> ( - let arith_caller_opt = AddressAttributes.get_citv addr_caller astate |> Option.map ~f:fst in - match CItv.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) with - | Unsatisfiable -> - raise - (Contradiction - (CItv - { addr_caller - ; addr_callee - ; arith_caller= arith_caller_opt - ; arith_callee= Some arith_callee - ; call_state })) - | Satisfiable (Some abduce_caller, _abduce_callee) -> - Attribute.CItv (abduce_caller, hist) - | Satisfiable (None, _) -> - attr ) - | BoItv itv -> ( - match - Itv.ItvPure.subst itv (fun symb bound -> - AbstractDomain.Types.NonBottom (eval_sym_of_subst astate subst_ref symb bound) ) - with - | NonBottom itv' -> - Attribute.BoItv itv' - | Bottom -> - raise - (Contradiction (ArithmeticBo {addr_callee; addr_caller; arith_callee= itv; call_state})) - ) + | Invalid (invalidation, trace) -> + Attribute.Invalid + (invalidation, add_call_to_trace proc_name call_location caller_history trace) + | CItv (arith, trace) -> + Attribute.CItv (arith, add_call_to_trace proc_name call_location caller_history trace) + | Allocated (procname, trace) -> + Attribute.Allocated + (procname, add_call_to_trace proc_name call_location caller_history trace) | AddressOfCppTemporary _ | AddressOfStackVariable _ - | Allocated _ + | BoItv _ | Closure _ - | Invalid _ | MustBeValid _ | StdVectorReserve | WrittenTo _ -> - (* non-relational attributes *) attr + in + let subst_ref = ref call_state.subst in + let attrs = + Attributes.map attrs ~f:(fun attr -> + let attr = + subst_attribute call_state subst_ref call_state.astate ~addr_callee ~addr_caller attr + in + add_call_to_attribute attr ) + in + (!subst_ref, attrs) - let add_call_to_attributes proc_name call_location ~addr_callee ~addr_caller caller_history attrs - call_state = - let add_call_to_attribute attr = - match (attr : Attribute.t) with - | Invalid (invalidation, trace) -> - Attribute.Invalid - (invalidation, add_call_to_trace proc_name call_location caller_history trace) - | CItv (arith, trace) -> - Attribute.CItv (arith, add_call_to_trace proc_name call_location caller_history trace) - | Allocated (procname, trace) -> - Attribute.Allocated - (procname, add_call_to_trace proc_name call_location caller_history trace) - | AddressOfCppTemporary _ - | AddressOfStackVariable _ - | BoItv _ - | Closure _ - | MustBeValid _ - | StdVectorReserve - | WrittenTo _ -> - attr - in - let subst_ref = ref call_state.subst in - let attrs = - Attributes.map attrs ~f:(fun attr -> - let attr = - subst_attribute call_state subst_ref call_state.astate ~addr_callee ~addr_caller attr - in - add_call_to_attribute attr ) - in - (!subst_ref, attrs) - - - let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state = - let one_address_sat addr_callee callee_attrs (addr_caller, caller_history) call_state = - let subst, attrs_caller = - add_call_to_attributes callee_proc_name call_location ~addr_callee ~addr_caller - caller_history callee_attrs call_state - in - let astate = AddressAttributes.abduce_and_add addr_caller attrs_caller call_state.astate in - if phys_equal subst call_state.subst && phys_equal astate call_state.astate then call_state - else {call_state with subst; astate} - in - (* check all callee addresses that make sense for the caller, i.e. the domain of [call_state.subst] *) - AddressMap.fold - (fun addr_callee addr_hist_caller call_state -> - match BaseAddressAttributes.find_opt addr_callee (pre_post.pre :> BaseDomain.t).attrs with - | None -> - call_state - | Some callee_attrs -> - one_address_sat addr_callee callee_attrs addr_hist_caller call_state ) - call_state.subst call_state - - - let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state = - PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ; - let r = - let open IResult.Let_syntax in - (* first make as large a mapping as we can between callee values and caller values... *) - materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals - call_state - >>= materialize_pre_for_globals callee_proc_name call_location pre_post - >>| (* ...then relational arithmetic constraints in the callee's attributes will make sense in - terms of the caller's values *) - apply_arithmetic_constraints callee_proc_name call_location pre_post +let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state = + let one_address_sat addr_callee callee_attrs (addr_caller, caller_history) call_state = + let subst, attrs_caller = + add_call_to_attributes callee_proc_name call_location ~addr_callee ~addr_caller caller_history + callee_attrs call_state in - PerfEvent.(log (fun logger -> log_end_event logger ())) ; - r + let astate = AddressAttributes.abduce_and_add addr_caller attrs_caller call_state.astate in + if phys_equal subst call_state.subst && phys_equal astate call_state.astate then call_state + else {call_state with subst; astate} + in + (* check all callee addresses that make sense for the caller, i.e. the domain of [call_state.subst] *) + AddressMap.fold + (fun addr_callee addr_hist_caller call_state -> + match BaseAddressAttributes.find_opt addr_callee (pre_post.pre :> BaseDomain.t).attrs with + | None -> + call_state + | Some callee_attrs -> + one_address_sat addr_callee callee_attrs addr_hist_caller call_state ) + call_state.subst call_state + + +let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state = + PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ; + let r = + let open IResult.Let_syntax in + (* first make as large a mapping as we can between callee values and caller values... *) + materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals + call_state + >>= materialize_pre_for_globals callee_proc_name call_location pre_post + >>| (* ...then relational arithmetic constraints in the callee's attributes will make sense in + terms of the caller's values *) + apply_arithmetic_constraints callee_proc_name call_location pre_post + in + PerfEvent.(log (fun logger -> log_end_event logger ())) ; + r - (* {3 applying the post to the current state} *) +(* {3 applying the post to the current state} *) - let subst_find_or_new subst addr_callee ~default_hist_caller = - match AddressMap.find_opt addr_callee subst with - | None -> - let addr_hist_fresh = (AbstractValue.mk_fresh (), default_hist_caller) in - (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh) - | Some addr_hist_caller -> - (subst, addr_hist_caller) +let subst_find_or_new subst addr_callee ~default_hist_caller = + match AddressMap.find_opt addr_callee subst with + | None -> + let addr_hist_fresh = (AbstractValue.mk_fresh (), default_hist_caller) in + (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh) + | Some addr_hist_caller -> + (subst, addr_hist_caller) - let call_state_subst_find_or_new call_state addr_callee ~default_hist_caller = - let new_subst, addr_hist_caller = - subst_find_or_new call_state.subst addr_callee ~default_hist_caller - in - if phys_equal new_subst call_state.subst then (call_state, addr_hist_caller) - else ({call_state with subst= new_subst}, addr_hist_caller) +let call_state_subst_find_or_new call_state addr_callee ~default_hist_caller = + let new_subst, addr_hist_caller = + subst_find_or_new call_state.subst addr_callee ~default_hist_caller + in + if phys_equal new_subst call_state.subst then (call_state, addr_hist_caller) + else ({call_state with subst= new_subst}, addr_hist_caller) - let delete_edges_in_callee_pre_from_caller ~addr_callee:_ ~edges_pre_opt ~addr_caller call_state = - match BaseMemory.find_opt addr_caller (call_state.astate.post :> base_domain).heap with +let delete_edges_in_callee_pre_from_caller ~addr_callee:_ ~edges_pre_opt ~addr_caller call_state = + match BaseMemory.find_opt addr_caller (call_state.astate.post :> base_domain).heap with + | None -> + BaseMemory.Edges.empty + | Some old_post_edges -> ( + match edges_pre_opt with | None -> - BaseMemory.Edges.empty - | Some old_post_edges -> ( - match edges_pre_opt with - | None -> - old_post_edges - | Some edges_pre -> - BaseMemory.Edges.merge - (fun _access old_opt pre_opt -> - (* TODO: should apply [call_state.subst] to [_access]! Actually, should rewrite the - whole [cell_pre] beforehand so that [Edges.merge] makes sense. *) - if Option.is_some pre_opt then - (* delete edge if some edge for the same access exists in the pre *) - None - else (* keep old edge if it exists *) old_opt ) - old_post_edges edges_pre ) - - - let record_post_cell callee_proc_name call_loc ~addr_callee ~edges_pre_opt - ~cell_post:(edges_post, attrs_post) ~addr_hist_caller:(addr_caller, hist_caller) call_state = - let post_edges_minus_pre = - delete_edges_in_callee_pre_from_caller ~addr_callee ~edges_pre_opt ~addr_caller call_state - in - let call_state = - let subst, attrs_post_caller = - add_call_to_attributes ~addr_callee ~addr_caller callee_proc_name call_loc hist_caller - attrs_post call_state - in - let astate = - AddressAttributes.abduce_and_add addr_caller attrs_post_caller call_state.astate - in - {call_state with subst; astate} - in - let heap = (call_state.astate.post :> base_domain).heap in - let attrs = (call_state.astate.post :> base_domain).attrs in - let subst, translated_post_edges = - BaseMemory.Edges.fold_map ~init:call_state.subst edges_post - ~f:(fun subst (addr_callee, trace_post) -> - let subst, (addr_curr, hist_curr) = - subst_find_or_new subst addr_callee ~default_hist_caller:hist_caller - in - ( subst - , ( addr_curr - , ValueHistory.Call {f= Call callee_proc_name; location= call_loc; in_call= trace_post} - :: hist_curr ) ) ) + old_post_edges + | Some edges_pre -> + BaseMemory.Edges.merge + (fun _access old_opt pre_opt -> + (* TODO: should apply [call_state.subst] to [_access]! Actually, should rewrite the + whole [cell_pre] beforehand so that [Edges.merge] makes sense. *) + if Option.is_some pre_opt then + (* delete edge if some edge for the same access exists in the pre *) + None + else (* keep old edge if it exists *) old_opt ) + old_post_edges edges_pre ) + + +let record_post_cell callee_proc_name call_loc ~addr_callee ~edges_pre_opt + ~cell_post:(edges_post, attrs_post) ~addr_hist_caller:(addr_caller, hist_caller) call_state = + let post_edges_minus_pre = + delete_edges_in_callee_pre_from_caller ~addr_callee ~edges_pre_opt ~addr_caller call_state + in + let call_state = + let subst, attrs_post_caller = + add_call_to_attributes ~addr_callee ~addr_caller callee_proc_name call_loc hist_caller + attrs_post call_state in - let heap = - let edges_post_caller = - BaseMemory.Edges.union - (fun _ _ post_cell -> Some post_cell) - post_edges_minus_pre translated_post_edges - in - BaseMemory.add addr_caller edges_post_caller heap + let astate = AddressAttributes.abduce_and_add addr_caller attrs_post_caller call_state.astate in + {call_state with subst; astate} + in + let heap = (call_state.astate.post :> base_domain).heap in + let attrs = (call_state.astate.post :> base_domain).attrs in + let subst, translated_post_edges = + BaseMemory.Edges.fold_map ~init:call_state.subst edges_post + ~f:(fun subst (addr_callee, trace_post) -> + let subst, (addr_curr, hist_curr) = + subst_find_or_new subst addr_callee ~default_hist_caller:hist_caller + in + ( subst + , ( addr_curr + , ValueHistory.Call {f= Call callee_proc_name; location= call_loc; in_call= trace_post} + :: hist_curr ) ) ) + in + let heap = + let edges_post_caller = + BaseMemory.Edges.union + (fun _ _ post_cell -> Some post_cell) + post_edges_minus_pre translated_post_edges in - let attrs = - let written_to_callee_opt = - let open IOption.Let_syntax in - let* attrs = BaseAddressAttributes.find_opt addr_caller attrs in - Attributes.get_written_to attrs - in - match written_to_callee_opt with - | None -> - attrs - | Some callee_trace -> - let written_to = - Attribute.WrittenTo - (ViaCall - { in_call= callee_trace - ; f= Call callee_proc_name - ; location= call_loc - ; history= hist_caller }) - in - BaseAddressAttributes.add_one addr_caller written_to attrs + BaseMemory.add addr_caller edges_post_caller heap + in + let attrs = + let written_to_callee_opt = + let open IOption.Let_syntax in + let* attrs = BaseAddressAttributes.find_opt addr_caller attrs in + Attributes.get_written_to attrs in - let caller_post = Domain.update ~heap ~attrs call_state.astate.post in - {call_state with subst; astate= {call_state.astate with post= caller_post}} + match written_to_callee_opt with + | None -> + attrs + | Some callee_trace -> + let written_to = + Attribute.WrittenTo + (ViaCall + { in_call= callee_trace + ; f= Call callee_proc_name + ; location= call_loc + ; history= hist_caller }) + in + BaseAddressAttributes.add_one addr_caller written_to attrs + in + let caller_post = Domain.update ~heap ~attrs call_state.astate.post in + {call_state with subst; astate= {call_state.astate with post= caller_post}} + + +let rec record_post_for_address callee_proc_name call_loc ({pre} as pre_post) ~addr_callee + ~addr_hist_caller call_state = + L.d_printfln "%a<->%a" AbstractValue.pp addr_callee AbstractValue.pp (fst addr_hist_caller) ; + match visit call_state ~addr_callee ~addr_hist_caller with + | `AlreadyVisited, call_state -> + call_state + | `NotAlreadyVisited, call_state -> ( + match find_post_cell_opt addr_callee pre_post with + | None -> + call_state + | Some ((edges_post, _attrs_post) as cell_post) -> + let edges_pre_opt = BaseMemory.find_opt addr_callee (pre :> BaseDomain.t).BaseDomain.heap in + let call_state_after_post = + if is_cell_read_only ~edges_pre_opt ~cell_post then call_state + else + record_post_cell callee_proc_name call_loc ~addr_callee ~edges_pre_opt ~addr_hist_caller + ~cell_post call_state + in + IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold ~init:call_state_after_post + edges_post ~f:(fun call_state (_access, (addr_callee_dest, _)) -> + let call_state, addr_hist_curr_dest = + call_state_subst_find_or_new call_state addr_callee_dest + ~default_hist_caller:(snd addr_hist_caller) + in + record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:addr_callee_dest + ~addr_hist_caller:addr_hist_curr_dest call_state ) ) - let rec record_post_for_address callee_proc_name call_loc ({pre} as pre_post) ~addr_callee - ~addr_hist_caller call_state = - L.d_printfln "%a<->%a" AbstractValue.pp addr_callee AbstractValue.pp (fst addr_hist_caller) ; - match visit call_state ~addr_callee ~addr_hist_caller with - | `AlreadyVisited, call_state -> - call_state - | `NotAlreadyVisited, call_state -> ( - match find_post_cell_opt addr_callee pre_post with - | None -> - call_state - | Some ((edges_post, _attrs_post) as cell_post) -> - let edges_pre_opt = - BaseMemory.find_opt addr_callee (pre :> BaseDomain.t).BaseDomain.heap - in - let call_state_after_post = - if is_cell_read_only ~edges_pre_opt ~cell_post then call_state - else - record_post_cell callee_proc_name call_loc ~addr_callee ~edges_pre_opt - ~addr_hist_caller ~cell_post call_state - in - IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold ~init:call_state_after_post - edges_post ~f:(fun call_state (_access, (addr_callee_dest, _)) -> - let call_state, addr_hist_curr_dest = - call_state_subst_find_or_new call_state addr_callee_dest - ~default_hist_caller:(snd addr_hist_caller) - in - record_post_for_address callee_proc_name call_loc pre_post - ~addr_callee:addr_callee_dest ~addr_hist_caller:addr_hist_curr_dest call_state ) ) - - - let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state = - L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractValue.pp - (fst actual) ; +let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state = + L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractValue.pp (fst actual) ; + match + let open IOption.Let_syntax in + let* addr_formal_pre, _ = + BaseStack.find_opt formal (pre_post.pre :> BaseDomain.t).BaseDomain.stack + in + let+ formal_pre, _ = + BaseMemory.find_edge_opt addr_formal_pre Dereference + (pre_post.pre :> BaseDomain.t).BaseDomain.heap + in + record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre + ~addr_hist_caller:actual call_state + with + | Some call_state -> + call_state + | None -> + call_state + + +let record_post_for_return callee_proc_name call_loc pre_post call_state = + let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in + match BaseStack.find_opt return_var (pre_post.post :> BaseDomain.t).stack with + | None -> + (call_state, None) + | Some (addr_return, _) -> ( match - let open IOption.Let_syntax in - let* addr_formal_pre, _ = - BaseStack.find_opt formal (pre_post.pre :> BaseDomain.t).BaseDomain.stack - in - let+ formal_pre, _ = - BaseMemory.find_edge_opt addr_formal_pre Dereference - (pre_post.pre :> BaseDomain.t).BaseDomain.heap - in - record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre - ~addr_hist_caller:actual call_state + BaseMemory.find_edge_opt addr_return Dereference + (pre_post.post :> BaseDomain.t).BaseDomain.heap with - | Some call_state -> - call_state | None -> - call_state + (call_state, None) + | Some (return_callee, _) -> + let return_caller_addr_hist = + match AddressMap.find_opt return_callee call_state.subst with + | Some return_caller_hist -> + return_caller_hist + | None -> + ( AbstractValue.mk_fresh () + , [ (* this could maybe include an event like "returned here" *) ] ) + in + let call_state = + record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:return_callee + ~addr_hist_caller:return_caller_addr_hist call_state + in + (call_state, Some return_caller_addr_hist) ) - let record_post_for_return callee_proc_name call_loc pre_post call_state = - let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in - match BaseStack.find_opt return_var (pre_post.post :> BaseDomain.t).stack with - | None -> - (call_state, None) - | Some (addr_return, _) -> ( - match - BaseMemory.find_edge_opt addr_return Dereference - (pre_post.post :> BaseDomain.t).BaseDomain.heap - with - | None -> - (call_state, None) - | Some (return_callee, _) -> - let return_caller_addr_hist = - match AddressMap.find_opt return_callee call_state.subst with - | Some return_caller_hist -> - return_caller_hist - | None -> - ( AbstractValue.mk_fresh () - , [ (* this could maybe include an event like "returned here" *) ] ) - in - let call_state = - record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:return_callee - ~addr_hist_caller:return_caller_addr_hist call_state - in - (call_state, Some return_caller_addr_hist) ) +let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state = + (* for each [(formal_i, actual_i)] pair, do [post_i = post union subst(graph reachable from + formal_i in post)], deleting previous info when comparing pre and post shows a difference + (TODO: record in the pre when a location is written to instead of just comparing values + between pre and post since it's unreliable, eg replace value read in pre with same value in + post but nuke other fields in the meantime? is that possible?). *) + match + List.fold2 formals actuals ~init:call_state ~f:(fun call_state formal (actual, _) -> + record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual call_state ) + with + | Unequal_lengths -> + (* should have been checked before by [materialize_pre] *) + assert false + | Ok call_state -> + call_state - let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state - = - (* for each [(formal_i, actual_i)] pair, do [post_i = post union subst(graph reachable from - formal_i in post)], deleting previous info when comparing pre and post shows a difference - (TODO: record in the pre when a location is written to instead of just comparing values - between pre and post since it's unreliable, eg replace value read in pre with same value in - post but nuke other fields in the meantime? is that possible?). *) - match - List.fold2 formals actuals ~init:call_state ~f:(fun call_state formal (actual, _) -> - record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual call_state - ) - with - | Unequal_lengths -> - (* should have been checked before by [materialize_pre] *) - assert false - | Ok call_state -> - call_state +let apply_post_for_globals callee_proc_name call_location pre_post call_state = + match + fold_globals_of_stack call_location (pre_post.pre :> BaseDomain.t).stack call_state + ~f:(fun _var ~stack_value:(addr_callee, _) ~addr_hist_caller call_state -> + Ok + (record_post_for_address callee_proc_name call_location pre_post ~addr_callee + ~addr_hist_caller call_state) ) + with + | Error _ -> + (* always return [Ok _] above *) assert false + | Ok call_state -> + call_state - let apply_post_for_globals callee_proc_name call_location pre_post call_state = - match - fold_globals_of_stack call_location (pre_post.pre :> BaseDomain.t).stack call_state - ~f:(fun _var ~stack_value:(addr_callee, _) ~addr_hist_caller call_state -> - Ok - (record_post_for_address callee_proc_name call_location pre_post ~addr_callee - ~addr_hist_caller call_state) ) - with - | Error _ -> - (* always return [Ok _] above *) assert false - | Ok call_state -> +let record_post_remaining_attributes callee_proc_name call_loc pre_post call_state = + BaseAddressAttributes.fold + (fun addr_callee attrs call_state -> + if AddressSet.mem addr_callee call_state.visited then + (* already recorded the attributes when we were walking the edges map *) call_state + else + match AddressMap.find_opt addr_callee call_state.subst with + | None -> + (* callee address has no meaning for the caller *) call_state + | Some (addr_caller, history) -> + let subst, attrs' = + add_call_to_attributes callee_proc_name call_loc ~addr_callee ~addr_caller history + attrs call_state + in + let astate = AddressAttributes.abduce_and_add addr_caller attrs' call_state.astate in + {call_state with subst; astate} ) + (pre_post.post :> BaseDomain.t).attrs call_state + + +let record_skipped_calls callee_proc_name call_loc pre_post call_state = + let callee_skipped_map = pre_post.skipped_calls in + let caller_skipped_map = + SkippedCalls.map + (fun trace -> add_call_to_trace callee_proc_name call_loc [] trace) + callee_skipped_map + |> (* favor calls we already knew about somewhat arbitrarily *) + SkippedCalls.union + (fun _ orig_call _callee_call -> Some orig_call) + call_state.astate.skipped_calls + in + {call_state with astate= {call_state.astate with skipped_calls= caller_skipped_map}} + + +let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state = + PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; + let r = + apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state + |> apply_post_for_globals callee_proc_name call_location pre_post + |> record_post_for_return callee_proc_name call_location pre_post + |> fun (call_state, return_caller) -> + ( record_post_remaining_attributes callee_proc_name call_location pre_post call_state + |> record_skipped_calls callee_proc_name call_location pre_post + , return_caller ) + |> fun ({astate}, return_caller) -> (astate, return_caller) + in + PerfEvent.(log (fun logger -> log_end_event logger ())) ; + r + + +let check_all_valid callee_proc_name call_location {pre; post= _} call_state = + AddressMap.fold + (fun addr_pre (addr_caller, hist_caller) astate_result -> + match astate_result with + | Error _ -> + astate_result + | Ok astate -> ( + match BaseAddressAttributes.get_must_be_valid addr_pre (pre :> BaseDomain.t).attrs with + | None -> + astate_result + | Some callee_access_trace -> + let access_trace = + Trace.ViaCall + { in_call= callee_access_trace + ; f= Call callee_proc_name + ; location= call_location + ; history= hist_caller } + in + AddressAttributes.check_valid access_trace addr_caller astate + |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> + L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; + Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} + ) ) ) + call_state.subst (Ok call_state.astate) - let record_post_remaining_attributes callee_proc_name call_loc pre_post call_state = - BaseAddressAttributes.fold - (fun addr_callee attrs call_state -> - if AddressSet.mem addr_callee call_state.visited then - (* already recorded the attributes when we were walking the edges map *) - call_state - else - match AddressMap.find_opt addr_callee call_state.subst with - | None -> - (* callee address has no meaning for the caller *) call_state - | Some (addr_caller, history) -> - let subst, attrs' = - add_call_to_attributes callee_proc_name call_loc ~addr_callee ~addr_caller history - attrs call_state - in - let astate = AddressAttributes.abduce_and_add addr_caller attrs' call_state.astate in - {call_state with subst; astate} ) - (pre_post.post :> BaseDomain.t).attrs call_state - - - let record_skipped_calls callee_proc_name call_loc pre_post call_state = - let callee_skipped_map = pre_post.skipped_calls in - let caller_skipped_map = - SkippedCalls.map - (fun trace -> add_call_to_trace callee_proc_name call_loc [] trace) - callee_skipped_map - |> (* favor calls we already knew about somewhat arbitrarily *) - SkippedCalls.union - (fun _ orig_call _callee_call -> Some orig_call) - call_state.astate.skipped_calls - in - {call_state with astate= {call_state.astate with skipped_calls= caller_skipped_map}} - - - let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state = - PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; - let r = - apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state - |> apply_post_for_globals callee_proc_name call_location pre_post - |> record_post_for_return callee_proc_name call_location pre_post - |> fun (call_state, return_caller) -> - ( record_post_remaining_attributes callee_proc_name call_location pre_post call_state - |> record_skipped_calls callee_proc_name call_location pre_post - , return_caller ) - |> fun ({astate}, return_caller) -> (astate, return_caller) - in - PerfEvent.(log (fun logger -> log_end_event logger ())) ; - r +(* - read all the pre, assert validity of addresses and materializes *everything* (to throw stuff + in the *current* pre as appropriate so that callers of the current procedure will also know + about the deeper reads) + - for each actual, write the post for that actual - let check_all_valid callee_proc_name call_location {pre; post= _} call_state = - AddressMap.fold - (fun addr_pre (addr_caller, hist_caller) astate_result -> - match astate_result with - | Error _ -> - astate_result - | Ok astate -> ( - match BaseAddressAttributes.get_must_be_valid addr_pre (pre :> BaseDomain.t).attrs with - | None -> - astate_result - | Some callee_access_trace -> - let access_trace = - Trace.ViaCall - { in_call= callee_access_trace - ; f= Call callee_proc_name - ; location= call_location - ; history= hist_caller } - in - AddressAttributes.check_valid access_trace addr_caller astate - |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> - L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; - Diagnostic.AccessToInvalidAddress - {invalidation; invalidation_trace; access_trace} ) ) ) - call_state.subst (Ok call_state.astate) - - - (* - read all the pre, assert validity of addresses and materializes *everything* (to throw stuff - in the *current* pre as appropriate so that callers of the current procedure will also know - about the deeper reads) - - - for each actual, write the post for that actual - - - if aliasing is introduced at any time then give up - - questions: - - - what if some preconditions raise lifetime issues but others don't? Have to be careful with - the noise that this will introduce since we don't care about values. For instance, if the pre - is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is - to bake in some value analysis. *) - let apply callee_proc_name call_location pre_post ~formals ~actuals astate = - L.d_printfln "Applying pre/post for %a(%a):@\n%a" Procname.pp callee_proc_name - (Pp.seq ~sep:"," Var.pp) formals pp pre_post ; - let empty_call_state = - {astate; subst= AddressMap.empty; rev_subst= AddressMap.empty; visited= AddressSet.empty} - in - (* read the precondition *) - match - materialize_pre callee_proc_name call_location pre_post ~formals ~actuals empty_call_state - with - | exception Contradiction reason -> - (* can't make sense of the pre-condition in the current context: give up on that particular - pre/post pair *) - L.d_printfln "Cannot apply precondition: %a" pp_contradiction reason ; - Ok None - | Error _ as error -> - (* error: the function call requires to read some state known to be invalid *) - error - | Ok call_state -> ( - L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ; - match - let open IResult.Let_syntax in - let+ astate = check_all_valid callee_proc_name call_location pre_post call_state in - (* reset [visited] *) - let call_state = {call_state with astate; visited= AddressSet.empty} in - (* apply the postcondition *) - apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state - with - | Ok post -> - Ok (Some post) - | exception Contradiction reason -> - L.d_printfln "Cannot apply post-condition: %a" pp_contradiction reason ; - Ok None - | Error _ as error -> - error ) - - - let get_pre {pre} = (pre :> BaseDomain.t) - - let get_post {post} = (post :> BaseDomain.t) - - let get_skipped_calls {skipped_calls} = skipped_calls -end + - if aliasing is introduced at any time then give up + + questions: + + - what if some preconditions raise lifetime issues but others don't? Have to be careful with + the noise that this will introduce since we don't care about values. For instance, if the pre + is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is + to bake in some value analysis. *) +let apply callee_proc_name call_location pre_post ~formals ~actuals astate = + L.d_printfln "Applying pre/post for %a(%a):@\n%a" Procname.pp callee_proc_name + (Pp.seq ~sep:"," Var.pp) formals pp pre_post ; + let empty_call_state = + {astate; subst= AddressMap.empty; rev_subst= AddressMap.empty; visited= AddressSet.empty} + in + (* read the precondition *) + match + materialize_pre callee_proc_name call_location pre_post ~formals ~actuals empty_call_state + with + | exception Contradiction reason -> + (* can't make sense of the pre-condition in the current context: give up on that particular + pre/post pair *) + L.d_printfln "Cannot apply precondition: %a" pp_contradiction reason ; + Ok None + | Error _ as error -> + (* error: the function call requires to read some state known to be invalid *) + error + | Ok call_state -> ( + L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ; + match + let open IResult.Let_syntax in + let+ astate = check_all_valid callee_proc_name call_location pre_post call_state in + (* reset [visited] *) + let call_state = {call_state with astate; visited= AddressSet.empty} in + (* apply the postcondition *) + apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state + with + | Ok post -> + Ok (Some post) + | exception Contradiction reason -> + L.d_printfln "Cannot apply post-condition: %a" pp_contradiction reason ; + Ok None + | Error _ as error -> + error ) + + +let get_pre {pre} = (pre :> BaseDomain.t) + +let get_post {post} = (post :> BaseDomain.t) + +let get_skipped_calls {skipped_calls} = skipped_calls diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index decb2c4ca..542103178 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -110,29 +110,25 @@ val discard_unreachable : t -> t * BaseAddressAttributes.t val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t -module PrePost : sig - type domain_t = t +val leq : lhs:t -> rhs:t -> bool - type t = private domain_t +val pp : Format.formatter -> t -> unit - val pp : Format.formatter -> t -> unit +val of_post : Procdesc.t -> t -> t - val of_post : Procdesc.t -> domain_t -> t +val get_pre : t -> BaseDomain.t - val apply : - Procname.t - -> Location.t - -> t - -> formals:Var.t list - -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list - -> domain_t - -> ((domain_t * (AbstractValue.t * ValueHistory.t) option) option, Diagnostic.t) result - (** return the abstract state after the call along with an optional return value, or [None] if the - precondition could not be satisfied (e.g. some aliasing constraints were not satisfied) *) +val get_post : t -> BaseDomain.t - val get_pre : t -> BaseDomain.t +val get_skipped_calls : t -> SkippedCalls.t - val get_post : t -> BaseDomain.t - - val get_skipped_calls : t -> SkippedCalls.t -end +val apply : + Procname.t + -> Location.t + -> t + -> formals:Var.t list + -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list + -> t + -> ((t * (AbstractValue.t * ValueHistory.t) option) option, Diagnostic.t) result +(** return the abstract state after the call along with an optional return value, or [None] if the + precondition could not be satisfied (e.g. some aliasing constraints were not satisfied) *) diff --git a/infer/src/pulse/PulseExecutionState.ml b/infer/src/pulse/PulseExecutionState.ml new file mode 100644 index 000000000..877451446 --- /dev/null +++ b/infer/src/pulse/PulseExecutionState.ml @@ -0,0 +1,43 @@ +(* + * 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 F = Format + +type exec_state = + | ContinueProgram of PulseAbductiveDomain.t + | ExitProgram of PulseAbductiveDomain.t + +type t = exec_state + +let continue astate = ContinueProgram astate + +let mk_initial pdesc = ContinueProgram (PulseAbductiveDomain.mk_initial pdesc) + +let leq ~lhs ~rhs = + match (lhs, rhs) with + | ContinueProgram astate1, ContinueProgram astate2 | ExitProgram astate1, ExitProgram astate2 -> + PulseAbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 + | ExitProgram _, ContinueProgram _ | ContinueProgram _, ExitProgram _ -> + false + + +let pp fmt = function + | ContinueProgram astate -> + PulseAbductiveDomain.pp fmt astate + | ExitProgram astate -> + F.fprintf fmt "{ExitProgram %a}" PulseAbductiveDomain.pp astate + + +let map ~f exec_state = + match exec_state with + | ContinueProgram astate -> + ContinueProgram (f astate) + | ExitProgram astate -> + ExitProgram (f astate) + + +let of_post pdesc = map ~f:(PulseAbductiveDomain.of_post pdesc) diff --git a/infer/src/pulse/PulseExecutionState.mli b/infer/src/pulse/PulseExecutionState.mli new file mode 100644 index 000000000..6702e1f8c --- /dev/null +++ b/infer/src/pulse/PulseExecutionState.mli @@ -0,0 +1,20 @@ +(* + * 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 + +type exec_state = + | ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *) + | ExitProgram of PulseAbductiveDomain.t + (** represents the state originating at exit/divergence. *) + +include AbstractDomain.NoJoin with type t = exec_state + +val continue : PulseAbductiveDomain.t -> t + +val of_post : Procdesc.t -> t -> t + +val mk_initial : Procdesc.t -> t diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index a0a053022..7ec5b6e80 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -17,7 +17,7 @@ type model = -> Location.t -> ret:Ident.t * Typ.t -> PulseAbductiveDomain.t - -> PulseAbductiveDomain.t list PulseOperations.access_result + -> PulseExecutionState.t list PulseOperations.access_result module Misc = struct let shallow_copy model_desc dest_pointer_hist src_pointer_hist : model = @@ -30,10 +30,14 @@ module Misc = struct ~obj:(fst obj_copy, event :: snd obj_copy) astate in - [PulseOperations.havoc_id ret_id [event] astate] + let astate = PulseOperations.havoc_id ret_id [event] astate in + [PulseExecutionState.ContinueProgram astate] - let early_exit : model = fun ~caller_summary:_ ~callee_procname:_ _ ~ret:_ _ -> Ok [] + let early_exit : model = + fun ~caller_summary:_ ~callee_procname:_ _ ~ret:_ astate -> + Ok [PulseExecutionState.ExitProgram astate] + let return_int : Int64.t -> model = fun i64 ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> @@ -44,7 +48,7 @@ module Misc = struct |> AddressAttributes.add_one ret_addr (CItv (CItv.equal_to i, Immediate {location; history= []})) in - Ok [PulseOperations.write_id ret_id (ret_addr, []) astate] + PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue let return_unknown_size : model = @@ -55,20 +59,22 @@ module Misc = struct |> AddressAttributes.add_one ret_addr (CItv (CItv.zero_inf, Immediate {location; history= []})) in - Ok [PulseOperations.write_id ret_id (ret_addr, []) astate] + PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue + + let skip : model = + fun ~caller_summary:_ ~callee_procname:_ _ ~ret:_ astate -> PulseOperations.ok_continue astate - let skip : model = fun ~caller_summary:_ ~callee_procname:_ _ ~ret:_ astate -> Ok [astate] let nondet ~fn_name : model = fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model fn_name; location; in_call= []} in - Ok [PulseOperations.havoc_id ret_id [event] astate] + PulseOperations.havoc_id ret_id [event] astate |> PulseOperations.ok_continue let id_first_arg arg_access_hist : model = fun ~caller_summary:_ ~callee_procname:_ _ ~ret astate -> - Ok [PulseOperations.write_id (fst ret) arg_access_hist astate] + PulseOperations.write_id (fst ret) arg_access_hist astate |> PulseOperations.ok_continue end module C = struct @@ -82,10 +88,10 @@ module C = struct || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv (fst deleted_access) astate) in if is_known_zero then (* freeing 0 is a no-op *) - Ok [astate] + PulseOperations.ok_continue astate else let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in - [astate] + [PulseExecutionState.ContinueProgram astate] let malloc _ : model = @@ -97,6 +103,7 @@ module C = struct |> AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.pos) |> AddressAttributes.add_one ret_addr (CItv (CItv.ge_to IntLit.one, Immediate {location; history= []})) + |> PulseExecutionState.continue in let+ astate_null = AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit IntLit.zero)) astate @@ -106,23 +113,27 @@ module C = struct |> PulseOperations.invalidate location (Invalidation.ConstantDereference IntLit.zero) (ret_addr, []) in - [astate_alloc; astate_null] + [astate_alloc; PulseExecutionState.ContinueProgram astate_null] end module Cplusplus = struct let delete deleted_access : model = fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> - PulseOperations.invalidate location Invalidation.CppDelete deleted_access astate >>| List.return + let+ astate = + PulseOperations.invalidate location Invalidation.CppDelete deleted_access astate + in + [PulseExecutionState.ContinueProgram astate] let placement_new actuals : model = fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "()"; location; in_call= []} in - match List.rev actuals with + ( match List.rev actuals with | ProcnameDispatcher.Call.FuncArg.{arg_payload= address, hist} :: _ -> - Ok [PulseOperations.write_id ret_id (address, event :: hist) astate] + PulseOperations.write_id ret_id (address, event :: hist) astate | _ -> - Ok [PulseOperations.havoc_id ret_id [event] astate] + PulseOperations.havoc_id ret_id [event] astate ) + |> PulseOperations.ok_continue end module StdAtomicInteger = struct @@ -150,7 +161,7 @@ module StdAtomicInteger = struct in let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in let+ astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in - [astate] + [PulseExecutionState.ContinueProgram astate] let arith_bop prepost location event ret_id bop this operand astate = @@ -173,7 +184,7 @@ module StdAtomicInteger = struct arith_bop `Post location event ret_id (PlusA None) this (AbstractValueOperand increment) astate in - [astate] + [PulseExecutionState.ContinueProgram astate] let fetch_sub this (increment, _) _memory_ordering : model = @@ -183,7 +194,7 @@ module StdAtomicInteger = struct arith_bop `Post location event ret_id (MinusA None) this (AbstractValueOperand increment) astate in - [astate] + [PulseExecutionState.ContinueProgram astate] let operator_plus_plus_pre this : model = @@ -192,7 +203,7 @@ module StdAtomicInteger = struct let+ astate = arith_bop `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate in - [astate] + [PulseExecutionState.ContinueProgram astate] let operator_plus_plus_post this _int : model = @@ -203,7 +214,7 @@ module StdAtomicInteger = struct let+ astate = arith_bop `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate in - [astate] + [PulseExecutionState.ContinueProgram astate] let operator_minus_minus_pre this : model = @@ -212,7 +223,7 @@ module StdAtomicInteger = struct let+ astate = arith_bop `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate in - [astate] + [PulseExecutionState.ContinueProgram astate] let operator_minus_minus_post this _int : model = @@ -223,14 +234,15 @@ module StdAtomicInteger = struct let+ astate = arith_bop `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate in - [astate] + [PulseExecutionState.ContinueProgram astate] let load_instr model_desc this _memory_ordering_opt : model = fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in let+ astate, _int_addr, (int, hist) = load_backing_int location this astate in - [PulseOperations.write_id ret_id (int, event :: hist) astate] + let astate = PulseOperations.write_id ret_id (int, event :: hist) astate in + [PulseExecutionState.ContinueProgram astate] let load = load_instr "std::atomic::load()" @@ -249,7 +261,7 @@ module StdAtomicInteger = struct fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "std::atomic::store()"; location; in_call= []} in let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in - [astate] + [PulseExecutionState.ContinueProgram astate] let exchange this_address (new_value, new_hist) _memory_ordering : model = @@ -257,7 +269,8 @@ module StdAtomicInteger = struct let event = ValueHistory.Call {f= Model "std::atomic::exchange()"; location; in_call= []} in let* astate, _int_addr, (old_int, old_hist) = load_backing_int location this_address astate in let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in - [PulseOperations.write_id ret_id (old_int, event :: old_hist) astate] + let astate = PulseOperations.write_id ret_id (old_int, event :: old_hist) astate in + [PulseExecutionState.ContinueProgram astate] end module ObjectiveC = struct @@ -268,7 +281,7 @@ module ObjectiveC = struct in let ret_addr = AbstractValue.mk_fresh () in let astate = PulseOperations.allocate callee_procname location (ret_addr, []) astate in - Ok [PulseOperations.write_id ret_id (ret_addr, hist) astate] + PulseOperations.write_id ret_id (ret_addr, hist) astate |> PulseOperations.ok_continue end module JavaObject = struct @@ -278,7 +291,8 @@ module JavaObject = struct let event = ValueHistory.Call {f= Model "Object.clone"; location; in_call= []} in let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in let+ astate, obj_copy = PulseOperations.shallow_copy location obj astate in - [PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate] + let astate = PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate in + [PulseExecutionState.ContinueProgram astate] end module StdBasicString = struct @@ -301,7 +315,8 @@ module StdBasicString = struct let+ astate, (string, hist) = PulseOperations.eval_access location string_addr_hist Dereference astate in - [PulseOperations.write_id ret_id (string, event :: hist) astate] + let astate = PulseOperations.write_id ret_id (string, event :: hist) astate in + [PulseExecutionState.ContinueProgram astate] let destructor this_hist : model = @@ -312,7 +327,7 @@ module StdBasicString = struct let string_addr_hist = (string_addr, call_event :: string_hist) in let* astate = PulseOperations.invalidate_deref location CppDelete string_addr_hist astate in let+ astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in - [astate] + [PulseExecutionState.ContinueProgram astate] end module StdFunction = struct @@ -328,7 +343,8 @@ module StdFunction = struct let* astate = PulseOperations.Closures.check_captured_addresses location lambda astate in match AddressAttributes.get_closure_proc_name lambda astate with | None -> - (* we don't know what proc name this lambda resolves to *) Ok (havoc_ret ret astate) + (* we don't know what proc name this lambda resolves to *) + Ok (havoc_ret ret astate |> List.map ~f:PulseExecutionState.continue) | Some callee_proc_name -> let actuals = List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> @@ -373,14 +389,16 @@ module StdVector = struct ; location ; in_call= [] } in - reallocate_internal_array [crumb] vector vector_f location astate >>| List.return + reallocate_internal_array [crumb] vector vector_f location astate + >>| PulseExecutionState.continue >>| List.return let at ~desc vector index : model = fun ~caller_summary:_ ~callee_procname:_ location ~ret astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let+ astate, (addr, hist) = element_of_internal_array location vector (fst index) astate in - [PulseOperations.write_id (fst ret) (addr, event :: hist) astate] + let astate = PulseOperations.write_id (fst ret) (addr, event :: hist) astate in + [PulseExecutionState.ContinueProgram astate] let reserve vector : model = @@ -388,7 +406,7 @@ module StdVector = struct let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in reallocate_internal_array [crumb] vector Reserve location astate >>| AddressAttributes.std_vector_reserve (fst vector) - >>| List.return + >>| PulseExecutionState.continue >>| List.return let push_back vector : model = @@ -397,10 +415,11 @@ module StdVector = struct if AddressAttributes.is_std_vector_reserved (fst vector) astate then (* assume that any call to [push_back] is ok after one called [reserve] on the same vector (a perfect analysis would also make sure we don't exceed the reserved size) *) - Ok [astate] + PulseOperations.ok_continue astate else (* simulate a re-allocation of the underlying array every time an element is added *) - reallocate_internal_array [crumb] vector PushBack location astate >>| List.return + reallocate_internal_array [crumb] vector PushBack location astate + >>| PulseExecutionState.continue >>| List.return end module JavaCollection = struct @@ -416,7 +435,8 @@ module JavaCollection = struct astate >>= PulseOperations.invalidate_deref location (StdVector Assign) old_elem in - [PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate] + let astate = PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate in + [PulseExecutionState.ContinueProgram astate] end module StringSet = Caml.Set.Make (String) diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli index 58bf290fe..c4224148d 100644 --- a/infer/src/pulse/PulseModels.mli +++ b/infer/src/pulse/PulseModels.mli @@ -13,7 +13,7 @@ type model = -> Location.t -> ret:Ident.t * Typ.t -> PulseAbductiveDomain.t - -> PulseAbductiveDomain.t list PulseOperations.access_result + -> PulseExecutionState.t list PulseOperations.access_result val dispatch : Tenv.t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index e8aa64a52..d87fce623 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -14,6 +14,8 @@ type t = AbductiveDomain.t type 'a access_result = ('a, Diagnostic.t) result +let ok_continue post = Ok [PulseExecutionState.ContinueProgram post] + (** Check that the [address] is not known to be invalid *) let check_addr_access location (address, history) astate = let access_trace = Trace.Immediate {location; history} in @@ -570,33 +572,47 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = |> havoc_ret ret |> add_skipped_proc -let call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt astate = +let apply_callee callee_pname call_loc callee_exec_state ~ret ~formals ~actuals astate = + let apply callee_prepost ~f = + PulseAbductiveDomain.apply callee_pname call_loc callee_prepost ~formals ~actuals astate + >>| function + | None -> + (* couldn't apply pre/post pair *) None + | Some (post, return_val_opt) -> + 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 + Some (f post) + in + let open PulseExecutionState in + match callee_exec_state with + | ContinueProgram astate -> + apply astate ~f:(fun astate -> ContinueProgram astate) + | ExitProgram astate -> + apply astate ~f:(fun astate -> ExitProgram astate) + + +let call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt + (astate : PulseAbductiveDomain.t) : (PulseExecutionState.t list, Diagnostic.t) result = match PulsePayload.read_full ~caller_summary ~callee_pname with - | Some (callee_proc_desc, preposts) -> + | 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 (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *) - List.fold_result preposts ~init:[] ~f:(fun posts pre_post -> + List.fold_result exec_states ~init:[] ~f:(fun posts callee_exec_state -> (* apply all pre/post specs *) - AbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals astate + apply_callee callee_pname call_loc callee_exec_state ~formals ~actuals ~ret astate >>| function - | None -> - (* couldn't apply pre/post pair *) posts - | Some (post, return_val_opt) -> - 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 - post :: posts ) + | None -> (* couldn't apply pre/post pair *) posts | Some 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 ; - Ok [unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt astate] + unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt astate + |> ok_continue diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index c3bd60c32..b36099688 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -13,6 +13,8 @@ type t = PulseAbductiveDomain.t type 'a access_result = ('a, Diagnostic.t) result +val ok_continue : t -> (PulseExecutionState.exec_state list, 'a) result + module Closures : sig val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t) result (** assert the validity of the addresses captured by the lambda *) @@ -112,7 +114,7 @@ val call : -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> formals_opt:(Pvar.t * Typ.t) list option -> t - -> t list access_result + -> PulseExecutionState.t list access_result (** perform an interprocedural call: apply the summary for the call proc name passed as argument if it exists *) diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index f1589bd1c..3d37685d2 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -6,15 +6,14 @@ *) open! IStd module F = Format -open PulseDomainInterface -type t = AbductiveDomain.PrePost.t list +type t = PulseExecutionState.t list -let of_posts pdesc posts = List.map posts ~f:(PulseAbductiveDomain.PrePost.of_post pdesc) +let of_posts pdesc posts = List.map posts ~f:(PulseExecutionState.of_post pdesc) let pp fmt summary = F.open_vbox 0 ; F.fprintf fmt "%d pre/post(s)@;" (List.length summary) ; List.iteri summary ~f:(fun i pre_post -> - F.fprintf fmt "#%d: @[%a@]@;" i PulseAbductiveDomain.PrePost.pp pre_post ) ; + F.fprintf fmt "#%d: @[%a@]@;" i PulseExecutionState.pp pre_post ) ; F.close_box () diff --git a/infer/src/pulse/PulseSummary.mli b/infer/src/pulse/PulseSummary.mli index 94ded779c..1de0157b9 100644 --- a/infer/src/pulse/PulseSummary.mli +++ b/infer/src/pulse/PulseSummary.mli @@ -6,8 +6,8 @@ *) open! IStd -type t = PulseAbductiveDomain.PrePost.t list +type t = PulseExecutionState.t list -val of_posts : Procdesc.t -> PulseAbductiveDomain.t list -> t +val of_posts : Procdesc.t -> PulseExecutionState.t list -> t val pp : Format.formatter -> t -> unit diff --git a/infer/tests/codetoanalyze/cpp/impurity/exit_test.cpp b/infer/tests/codetoanalyze/cpp/impurity/exit_test.cpp new file mode 100644 index 000000000..278777729 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/impurity/exit_test.cpp @@ -0,0 +1,20 @@ +/* + * 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. + */ +#include + +int x; + +void exit_positive_impure_FN(int a[10], int b) { + if (b > 0) { + exit(0); + } +} + +void unreachable_impure_FN(int a[10], int b) { + exit_positive_impure_FN(a, 10); + x = 9; +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp b/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp new file mode 100644 index 000000000..9b588dd71 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/exit_test.cpp @@ -0,0 +1,29 @@ +/* + * 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. + */ +#include + +// we get two disjuncts one for each branch +void exit_positive(int a[10], int b) { + if (b < 1) { + exit(0); + } +} + +void unreachable_double_free_ok(int a[10], int b) { + exit_positive(a, 0); + free(a); + free(a); +} + +void store_exit(int* x, bool b) { + if (b) { + *x = 42; + exit(0); + } +} + +void store_exit_null_bad(bool b) { store_exit(NULL, b); } diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index c0feb5e80..31c899570 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -12,6 +12,7 @@ codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_access_ok,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `deduplication::templated_delete_function<_Bool>` here,parameter `a` of deduplication::templated_delete_function<_Bool>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<_Bool>` here,parameter `a` of deduplication::templated_access_function<_Bool>,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `deduplication::templated_delete_function` here,parameter `a` of deduplication::templated_delete_function,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,parameter `a` of deduplication::templated_access_function,invalid access occurs here] +codetoanalyze/cpp/pulse/exit_test.cpp, store_exit_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `store_exit` here,parameter `x` of store_exit,invalid access occurs here] codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,invalid access occurs here] codetoanalyze/cpp/pulse/frontend.cpp, deref_null_namespace_alias_ptr_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `some::thing::bad_ptr` here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `some::thing::bad_ptr`,return from call to `some::thing::bad_ptr`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,assigned,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/throw_test.cpp b/infer/tests/codetoanalyze/cpp/pulse/throw_test.cpp new file mode 100644 index 000000000..4d1a7c348 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/throw_test.cpp @@ -0,0 +1,35 @@ +/* + * 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. + */ +#include + +int double_free_in_catch_bad_FN(int a[10], int b) { + try { + if (b > 0) { + free(a); + throw(0); + } + } catch (...) { + free(a); + } + return 0; +} + +void throw_positive(int a[10], int b) { + if (b > 0) { + free(a); + throw(1); + } +} + +int double_free_interproc_bad_FN(int a[10], int b) { + try { + throw_positive(a, 2); + } catch (...) { + free(a); + } + return 0; +} diff --git a/infer/tests/codetoanalyze/java/impurity/Test.java b/infer/tests/codetoanalyze/java/impurity/Test.java index 06ec71e03..d558c1f1d 100644 --- a/infer/tests/codetoanalyze/java/impurity/Test.java +++ b/infer/tests/codetoanalyze/java/impurity/Test.java @@ -89,8 +89,15 @@ class Test { return System.nanoTime(); } - // In pulse, we get 0 disjuncts as a summary, hence consider this as impure - void exit_impure() { + // In pulse, we get Exited summary where pre=post + // TODO: change impurity to track exit as impure + void exit_impure_FN() { + System.exit(1); + } + + // In pulse, we get Exited summary where pre=post + void modify_exit_impure(int[] a) { + a[0] = 0; System.exit(1); } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index c280d251f..b199f6e27 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -34,9 +34,9 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():voi codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` modified here] codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter `array` modified here] codetoanalyze/java/impurity/Test.java, Test.call_impure_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.call_impure_impure(int),when calling `void Test.set_impure(int,int)` here,parameter `this` modified here] -codetoanalyze/java/impurity/Test.java, Test.exit_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.exit_impure() with empty pulse summary] codetoanalyze/java/impurity/Test.java, Test.global_array_set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.global_array_set_impure(int,int),global variable `Test` modified here] codetoanalyze/java/impurity/Test.java, Test.local_field_write_impure(Test):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.local_field_write_impure(Test),parameter `x` modified here] +codetoanalyze/java/impurity/Test.java, Test.modify_exit_impure(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.modify_exit_impure(int[]),parameter `a` modified here] codetoanalyze/java/impurity/Test.java, Test.parameter_field_write_impure(Test,boolean):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.parameter_field_write_impure(Test,boolean),parameter `test` modified here] codetoanalyze/java/impurity/Test.java, Test.set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.set_impure(int,int),parameter `this` modified here] codetoanalyze/java/impurity/Test.java, Test.swap_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.swap_impure(int[],int,int),parameter `array` modified here]