[pulse] Do not havoc arguments of unknown functions that are pointers to const

Reviewed By: skcho

Differential Revision: D19331312

fbshipit-source-id: b450a819b

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

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

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]

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

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<temporaries::A>::UniquePtr`,parameter `y` of temporaries::UniquePtr<temporaries::A>::UniquePtr,assigned,return from call to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,when calling `temporaries::UniquePtr<temporaries::A>::~UniquePtr` here,parameter `this` of temporaries::UniquePtr<temporaries::A>::~UniquePtr,when calling `temporaries::UniquePtr<temporaries::A>::__infer_inner_destructor_~UniquePtr` here,parameter `this` of temporaries::UniquePtr<temporaries::A>::__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<temporaries::A>::UniquePtr`,parameter `y` of temporaries::UniquePtr<temporaries::A>::UniquePtr,assigned,return from call to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr<temporaries::A>::get`,return from call to `temporaries::UniquePtr<temporaries::A>::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]

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();