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]