diff --git a/infer/src/IR/Attributes.ml b/infer/src/IR/Attributes.ml index af108d9ff..470e46005 100644 --- a/infer/src/IR/Attributes.ml +++ b/infer/src/IR/Attributes.ml @@ -66,6 +66,8 @@ let find = let load pname = find (Procname.to_unique_id pname) +let is_no_return pname = match load pname with Some {is_no_return} -> is_no_return | _ -> false + let store ~proc_desc (attr : ProcAttributes.t) = let pname = attr.proc_name in let akind = proc_kind_of_attr attr in diff --git a/infer/src/IR/Attributes.mli b/infer/src/IR/Attributes.mli index c38d5edb0..7c3ceddbc 100644 --- a/infer/src/IR/Attributes.mli +++ b/infer/src/IR/Attributes.mli @@ -19,4 +19,6 @@ val store : proc_desc:Procdesc.t option -> ProcAttributes.t -> unit val load : Procname.t -> ProcAttributes.t option (** Load the attributes for the procedure from the attributes database. *) +val is_no_return : Procname.t -> bool + val pp_attributes_kind : Format.formatter -> attributes_kind -> unit diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 909e184bf..91a119476 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -443,12 +443,9 @@ module NoReturn = struct Procdesc.Node.get_instrs node |> Instrs.exists ~f:(fun (instr : Sil.instr) -> match instr with - | Call (_, Const (Cfun proc_name), _, _, _) -> ( - match Attributes.load proc_name with - | Some {ProcAttributes.is_no_return= true} -> - true - | _ -> - NoReturnModels.dispatch tenv proc_name |> Option.value ~default:false ) + | Call (_, Const (Cfun proc_name), _, _, _) -> + Attributes.is_no_return proc_name + || NoReturnModels.dispatch tenv proc_name |> Option.value ~default:false | _ -> false ) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index a6a451166..9a3c5c204 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -9,6 +9,7 @@ open! IStd module F = Format module L = Logging open IResult.Let_syntax +module IRAttributes = Attributes open PulseBasicInterface open PulseDomainInterface @@ -147,8 +148,8 @@ module PulseTransferFunctions = struct AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate - let dispatch_call ({InterproceduralAnalysis.tenv} as analysis_data) ret call_exp actuals call_loc - flags astate = + let dispatch_call ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) ret call_exp + actuals call_loc flags astate = (* evaluate all actuals *) let* astate, rev_func_args = List.fold_result actuals ~init:(astate, []) @@ -198,15 +199,20 @@ module PulseTransferFunctions = struct (* skip, as above for non-topl *) exec_state_res else exec_state_res in - 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* 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 -> - exec_state_res + let+ exec_state = + 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* 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 -> + exec_state_res + in + if Option.exists callee_pname ~f:IRAttributes.is_no_return then + ExecutionDomain.force_exit_program proc_desc exec_state + else exec_state (* [get_dealloc_from_dynamic_types vars_types loc] returns a dealloc procname and vars and diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index f00de15a2..30cc11dde 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -72,7 +72,7 @@ let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_st type summary = AbductiveDomain.summary base_t [@@deriving yojson_of] -let summary_of_posts pdesc posts = +let summary_of_posts_common ~continue_program pdesc posts = List.filter_mapi posts ~f:(fun i exec_state -> L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; match exec_state with @@ -81,7 +81,7 @@ let summary_of_posts pdesc posts = | Unsat -> None | Sat astate -> - Some (ContinueProgram astate) ) + Some (continue_program astate) ) (* already a summary but need to reconstruct the variants to make the type system happy *) | AbortProgram astate -> Some (AbortProgram astate) @@ -89,3 +89,11 @@ let summary_of_posts pdesc posts = Some (ExitProgram astate) | LatentAbortProgram {astate; latent_issue} -> Some (LatentAbortProgram {astate; latent_issue}) ) + + +let summary_of_posts = + summary_of_posts_common ~continue_program:(fun astate -> ContinueProgram astate) + + +let force_exit_program = + summary_of_posts_common ~continue_program:(fun astate -> ExitProgram astate) diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index cbf7e9978..e6c2bf4d7 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -32,3 +32,5 @@ val is_unsat_cheap : t -> bool type summary = AbductiveDomain.summary base_t [@@deriving yojson_of] val summary_of_posts : Procdesc.t -> t list -> summary list + +val force_exit_program : Procdesc.t -> t list -> t list diff --git a/infer/tests/codetoanalyze/c/pulse/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c index 88fd03ae1..080a7a46c 100644 --- a/infer/tests/codetoanalyze/c/pulse/nullptr.c +++ b/infer/tests/codetoanalyze/c/pulse/nullptr.c @@ -6,6 +6,7 @@ */ #include +#include int* malloc_no_check_bad() { int* p = (int*)malloc(sizeof(int)); @@ -77,3 +78,19 @@ void interproc_free_ok() { int* p = (int*)malloc(sizeof(int)); wrap_free(p); } + +noreturn void no_return(); + +void wrap_malloc(int** x) { + *x = (int*)malloc(sizeof(int)); + if (!*x) { + no_return(); + } +} + +void call_no_return_good() { + int* x = NULL; + wrap_malloc(&x); + *x = 5; + free(x); +}