diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index c0e677c4a..690d9b410 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -34,19 +34,24 @@ let proc_name_of_call call_exp = None +type get_formals = Procname.t -> (Pvar.t * Typ.t) list option + module PulseTransferFunctions = struct module CFG = ProcCfg.Normal module Domain = PulseAbductiveDomain - type extras = unit + type extras = get_formals - let interprocedural_call caller_summary ret call_exp actuals call_loc astate = + let interprocedural_call caller_summary ret call_exp actuals call_loc get_formals astate = match proc_name_of_call call_exp with | Some callee_pname -> - PulseOperations.call ~caller_summary call_loc callee_pname ~ret ~actuals astate + let formals_opt = get_formals callee_pname in + PulseOperations.call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt astate | None -> L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; - Ok [PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals astate] + Ok + [ PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals + ~formals_opt:None astate ] (** has an object just gone out of scope? *) @@ -72,7 +77,7 @@ module PulseTransferFunctions = struct PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate - let dispatch_call tenv summary ret call_exp actuals call_loc flags astate = + let dispatch_call tenv summary ret call_exp actuals call_loc flags get_formals astate = (* evaluate all actuals *) List.fold_result actuals ~init:(astate, []) ~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) -> @@ -105,7 +110,10 @@ module PulseTransferFunctions = struct ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ)) func_args in - let r = interprocedural_call summary ret call_exp only_actuals_evaled call_loc astate in + let r = + interprocedural_call summary ret call_exp only_actuals_evaled call_loc get_formals + astate + in PerfEvent.(log (fun logger -> log_end_event logger ())) ; r in @@ -120,7 +128,8 @@ module PulseTransferFunctions = struct posts - let exec_instr (astate : Domain.t) {tenv; ProcData.summary} _cfg_node (instr : Sil.instr) = + 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] *) @@ -157,7 +166,8 @@ module PulseTransferFunctions = struct [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 astate |> check_error summary + dispatch_call tenv summary ret call_exp actuals loc call_flags get_formals astate + |> check_error summary | Metadata (ExitScope (vars, location)) -> [PulseOperations.remove_vars vars location astate] | Metadata (VariableLifetimeBegins (pvar, _, location)) -> @@ -184,12 +194,15 @@ module DisjunctiveAnalyzer = AbstractInterpreter.MakeWTO (DisjunctiveTransferFun let checker {Callbacks.exe_env; summary} = let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in - let proc_data = ProcData.make summary tenv () in AbstractValue.init () ; let pdesc = Summary.get_proc_desc summary in let initial = DisjunctiveTransferFunctions.Disjuncts.singleton (PulseAbductiveDomain.mk_initial pdesc) in + let get_formals callee_pname = + Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals + in + let proc_data = ProcData.make summary tenv get_formals in match DisjunctiveAnalyzer.compute_post proc_data ~initial with | Some posts -> PulsePayload.update_summary diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 8afb9c3b1..598b3c19f 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -282,7 +282,8 @@ module StdFunction = struct List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ) ) in - PulseOperations.call ~caller_summary location callee_proc_name ~ret ~actuals astate + PulseOperations.call ~caller_summary location callee_proc_name ~ret ~actuals + ~formals_opt:None astate end module StdVector = struct diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 6bbc83675..d4443ba9c 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -481,13 +481,18 @@ let remove_vars vars location astate = if phys_equal astate' astate then astate else AbductiveDomain.discard_unreachable astate' -let unknown_call call_loc reason ~ret ~actuals astate = +let is_ptr_to_const formal_typ_opt = + Option.value_map formal_typ_opt ~default:false ~f:(fun (formal_typ : Typ.t) -> + match formal_typ.desc with Typ.Tptr (t, _) -> Typ.is_const t.quals | _ -> false ) + + +let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in let havoc_ret (ret, _) astate = havoc_id ret [event] astate in - let havoc_actual_if_ptr (actual, typ) astate = - if Typ.is_pointer typ then - (* TODO: to avoid false negatives, we should not havoc when the corresponding formal is a - pointer to const *) + let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate = + (* We should not havoc when the corresponding formal is a + pointer to const *) + if Typ.is_pointer actual_typ && not (is_ptr_to_const formal_typ_opt) then (* HACK: write through the pointer even if it is invalid. This is to avoid raising issues when havoc'ing pointer parameters (which normally causes a [check_valid] call. *) let fresh_value = AbstractValue.mk_fresh () in @@ -495,11 +500,20 @@ let unknown_call call_loc reason ~ret ~actuals astate = else astate in L.d_printfln "skipping unknown procedure@." ; - List.fold actuals ~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ astate) ~init:astate + ( match formals_opt with + | None -> + List.fold actuals + ~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ None astate) + ~init:astate + | Some formals -> + List.fold2_exn actuals formals + ~f:(fun astate actual_typ (_, formal_typ) -> + havoc_actual_if_ptr actual_typ (Some formal_typ) astate ) + ~init:astate ) |> havoc_ret ret -let call ~caller_summary call_loc callee_pname ~ret ~actuals astate = +let call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt astate = match PulsePayload.read_full ~caller_summary ~callee_pname with | Some (callee_proc_desc, preposts) -> let formals = @@ -528,4 +542,4 @@ let call ~caller_summary call_loc callee_pname ~ret ~actuals astate = | 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 astate] + Ok [unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt astate] diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 1e1e1528b..f2e827a48 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -108,6 +108,7 @@ val call : -> Procname.t -> ret:Ident.t * Typ.t -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list + -> formals_opt:(Pvar.t * Typ.t) list option -> t -> t list access_result (** perform an interprocedural call: apply the summary for the call proc name passed as argument if @@ -118,6 +119,7 @@ val unknown_call : -> CallEvent.t -> ret:Ident.t * 'a -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list + -> formals_opt:(Pvar.t * Typ.t) list option -> t -> t (** performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 5de67ac28..ba46b589d 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -46,6 +46,7 @@ codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::pre_increment_decrement_te codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,when calling `temporaries::UniquePtr::~UniquePtr` here,parameter `this` of temporaries::UniquePtr::~UniquePtr,when calling `temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr` here,parameter `this` of temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::get`,return from call to `temporaries::UniquePtr::get`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,passed as argument to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs here] codetoanalyze/cpp/pulse/unknown_functions.cpp, call_init_with_pointer_value_bad, 3, 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,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/unknown_functions.cpp, const_no_init_bad, 3, 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,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/unknown_functions.cpp b/infer/tests/codetoanalyze/cpp/pulse/unknown_functions.cpp index e41a04499..eafa8f3d3 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/unknown_functions.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/unknown_functions.cpp @@ -18,7 +18,7 @@ void init_ok() { p->foo(); } -void const_no_init_bad_FN() { +void const_no_init_bad() { X* p = nullptr; unknown_no_init_ptr(&p); p->foo();