[specialization][pulse] propagate specialization needs to the caller …

…of the caller

Summary:
when a caller does not have enough information to please the callee
specialization needs, he can marked himself as needed specialization.

Beware: this interprocedural technique is still active for all frontends. But I've made measures on Java and did not see performance impacts.

Reviewed By: dulmarod

Differential Revision: D45692224

fbshipit-source-id: d55e93f9fb175b2b9f535564c216ed04594f3f3b

infer/src/pulse/PulseAbductiveDomain.ml

@@ -1590,6 +1590,9 @@ module Summary = struct
 
 
   let with_need_closure_specialization summary = {summary with need_closure_specialization= true}
+
+  let add_need_dynamic_type_specialization proc_desc receiver_addr summary =
+    add_need_dynamic_type_specialization proc_desc receiver_addr summary
 end
 
 module Topl = struct

infer/src/pulse/PulseAbductiveDomain.mli

@@ -295,6 +295,8 @@ module Summary : sig
 
   val with_need_closure_specialization : summary -> summary
 
+  val add_need_dynamic_type_specialization : Procdesc.t -> AbstractValue.t -> summary -> summary
+
   val of_post :
        Tenv.t
     -> Procname.t

infer/src/pulse/PulseCallOperations.ml

@@ -478,36 +478,72 @@ let mk_actuals_map actuals formals =
       Some map
 
 
-let maybe_dynamic_type_specialization_is_needed run_analysis formals_opt actuals contradiction
-    astate =
-  let open IOption.Let_syntax in
-  let* contradiction in
-  let* pvars = PulseInterproc.is_dynamic_type_needed_contradiction contradiction in
-  let make_dynamic_type_specialization pvars =
+let maybe_dynamic_type_specialization_is_needed formals_opt actuals contradiction astate =
+  let make_dynamic_type_specialization =
     (* we try to find a dynamic type name for each pvar in the [pvars] set in order to devirtualize all
-             calls in the callee (and its own callees) *)
+       calls in the callee (and its own callees). If we do not find a dynanmic type, we record the
+       address in a set [need_specialization_from_caller] in order to propagate the need to the caller
+       state *)
     let open IOption.Let_syntax in
+    let* contradiction in
+    let* pvars = PulseInterproc.is_dynamic_type_needed_contradiction contradiction in
     let* formals = formals_opt in
-    let* actuals_map = mk_actuals_map actuals formals in
+    let+ actuals_map = mk_actuals_map actuals formals in
     Pvar.Set.fold
-      (fun pvar opt_map ->
-        let* map = opt_map in
-        let* (addr, _), _ = Pvar.Map.find_opt pvar actuals_map in
-        let* dynamic_type = AbductiveDomain.AddressAttributes.get_dynamic_type addr astate in
-        let+ dynamic_type_name = Typ.name dynamic_type in
-        Pvar.Map.add pvar dynamic_type_name map )
-      pvars (Some Pvar.Map.empty)
+      (fun pvar (dyntypes_map, need_specialization_from_caller) ->
+        let (addr, _), _ = Pvar.Map.find pvar actuals_map in
+        (* will succeed thanks to [mk_actuals_map] *)
+        let ( let** ) opt f =
+          Option.value_map opt ~f
+            ~default:(dyntypes_map, AbstractValue.Set.add addr need_specialization_from_caller)
+        in
+        let** dynamic_type = AbductiveDomain.AddressAttributes.get_dynamic_type addr astate in
+        let** dynamic_type_name = Typ.name dynamic_type in
+        (Pvar.Map.add pvar dynamic_type_name dyntypes_map, need_specialization_from_caller) )
+      pvars
+      (Pvar.Map.empty, AbstractValue.Set.empty)
   in
-  match make_dynamic_type_specialization pvars with
-  | Some map ->
-      let specialization = Specialization.Pulse.DynamicTypes map in
+  match make_dynamic_type_specialization with
+  | Some (dyntypes_map, need_specialization_from_caller)
+    when AbstractValue.Set.is_empty need_specialization_from_caller ->
+      let specialization = Specialization.Pulse.DynamicTypes dyntypes_map in
       L.d_printfln "requesting dyntypes specialization %a" Specialization.Pulse.pp specialization ;
-      let res, contradiction = run_analysis specialization in
-      Some (res, contradiction, `KnownCall)
-  | None ->
+      `RequestSpecializedAnalysis dyntypes_map
+  | Some (_, need_specialization_from_caller) ->
       L.d_printfln "[specialization] not enough dyntypes information in the caller context" ;
-      (* TODO: not implemented yet *)
-      None
+      let add_need_dynamic_type_specialization caller_proc_desc execution_state =
+        let update_astate astate =
+          AbstractValue.Set.fold
+            (fun addr astate ->
+              AbductiveDomain.add_need_dynamic_type_specialization caller_proc_desc addr astate )
+            need_specialization_from_caller astate
+        in
+        let update_summary summary =
+          AbstractValue.Set.fold
+            (fun addr summary ->
+              AbductiveDomain.Summary.add_need_dynamic_type_specialization caller_proc_desc addr
+                summary )
+            need_specialization_from_caller summary
+        in
+        match (execution_state : ExecutionDomain.t) with
+        | ExceptionRaised astate ->
+            ExceptionRaised (update_astate astate)
+        | ContinueProgram astate ->
+            ContinueProgram (update_astate astate)
+        | ExitProgram summary ->
+            ExitProgram (update_summary summary)
+        | AbortProgram summary ->
+            AbortProgram (update_summary summary)
+        | LatentAbortProgram latent_abort_program ->
+            let astate = update_summary latent_abort_program.astate in
+            LatentAbortProgram {latent_abort_program with astate}
+        | LatentInvalidAccess latent_invalid_access ->
+            let astate = update_summary latent_invalid_access.astate in
+            LatentInvalidAccess {latent_invalid_access with astate}
+      in
+      `NeedCallerSpecialization add_need_dynamic_type_specialization
+  | None ->
+      `AbortAndUseMainSummary
 
 
 let call tenv path ~caller_proc_desc
@@ -532,7 +568,7 @@ let call tenv path ~caller_proc_desc
     else results
   in
   match (analyze_dependency callee_pname : PulseSummary.t option) with
-  | Some summary ->
+  | Some summary -> (
       let call_aux exec_states =
         let results, contradiction =
           call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals call_kind
@@ -588,10 +624,23 @@ let call tenv path ~caller_proc_desc
               (res, contradiction, `KnownCall) )
         else (res, contradiction, `UnknownCall)
       else
-        maybe_dynamic_type_specialization_is_needed
-          (fun specialization -> request_specialization specialization |> call_aux)
-          formals_opt actuals contradiction astate
-        |> Option.value ~default:(res, contradiction, `KnownCall)
+        match
+          maybe_dynamic_type_specialization_is_needed formals_opt actuals contradiction astate
+        with
+        | `RequestSpecializedAnalysis dyntypes_map ->
+            let specialization = Specialization.Pulse.DynamicTypes dyntypes_map in
+            let res, contradiction = request_specialization specialization |> call_aux in
+            (* TODO: maybe this specialized summary still require specialization *)
+            (res, contradiction, `KnownCall)
+        | `NeedCallerSpecialization add_need_dynamic_type_specialization ->
+            let f exec_state = add_need_dynamic_type_specialization caller_proc_desc exec_state in
+            (* remark: we could also run an analysis of the callee with the partial information we have,
+               but here we chose to keep the default summary and wait for a full specialization.
+               Advantage: we only store specialized summary that are *sound* while the main summary
+               is a best effort computation that can be *unsound* *)
+            (List.map res ~f:(PulseResult.map ~f), contradiction, `KnownCall)
+        | `AbortAndUseMainSummary ->
+            (res, contradiction, `KnownCall) )
   | None ->
       (* no spec found for some reason (unknown function, ...) *)
       L.d_printfln_escaped "No spec found for %a@\n" Procname.pp callee_pname ;

infer/tests/codetoanalyze/hack/pulse/issues.exp

@@ -19,7 +19,7 @@ intra_file_flow.hack, IntraFileFlow.explicitSinkMethodDerivedDynamicBad, 7, TAIN
 intra_file_flow.hack, IntraFileFlow.explicitSinkClassDirectBad, 0, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value passed as argument `#1` to `IntraFileFlow.explicitSinkClassDirectBad` with kind `Simple`,when calling `IntraFileFlow$static.explicitSinkClassDirectBad` here,value passed as argument `#1` to `Logger$static.someLogMethod` with kind `Simple`], source: IntraFileFlow.explicitSinkClassDirectBad, sink: Logger$static.someLogMethod, tainted expression: $sc
 intra_file_flow.hack, IntraFileFlow$static.explicitSinkClassDirectBad, 3, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value passed as argument `#1` to `IntraFileFlow$static.explicitSinkClassDirectBad` with kind `Simple`,value passed as argument `#1` to `Logger$static.someLogMethod` with kind `Simple`], source: IntraFileFlow$static.explicitSinkClassDirectBad, sink: Logger$static.someLogMethod, tainted expression: $sc
 late_binding.hack, LateBinding::Main.call_caller_bad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
-late_binding.hack, LateBinding::Main.FP_call_parent_caller_good, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
+late_binding.hack, LateBinding::Main.call_parent_caller_bad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
 level1.hack, $root.Level1::basicFlowBad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
 level1_with_extends.hack, ExtendsTests::Main.fromABad, 2, TAINT_ERROR, no_bucket, ERROR, [in call to `ExtendsTests::A.sourceIfA`,source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,return from call to `ExtendsTests::A.sourceIfA`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
 level1_with_extends.hack, ExtendsTests::Main.fromBBad, 2, TAINT_ERROR, no_bucket, ERROR, [in call to `ExtendsTests::A.sourceIfA`,source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,return from call to `ExtendsTests::A.sourceIfA`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted

infer/tests/codetoanalyze/hack/pulse/late_binding.hack

@@ -54,15 +54,15 @@ class Main {
     }
   }
 
-  public function FN_call_parent_caller_bad(): void {
+  public function call_parent_caller_bad(): void {
     $tainted = \Level1\taintSource();
     $i = C::parent_caller();
     if ($i == 0) {
       \Level1\taintSink($tainted);
     }
   }
 
-  public function FP_call_parent_caller_good(): void {
+  public function call_parent_caller_good(): void {
     $tainted = \Level1\taintSource();
     $i = C::parent_caller();
     if ($i != 0) {

infer/tests/codetoanalyze/sil/pulse/issues.exp

@@ -22,6 +22,5 @@ to_sil_bug.sil, use_get_next_on_program_var_bad, 3, NULLPTR_DEREFERENCE, no_buck
 virt.sil, plusBad, -36, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,when calling `plus` here,when calling `Int.value` here,invalid access occurs here]
 virt.sil, test_dyntype_specialization_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 virt.sil, test_dyntype_specialization_from_caller_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
-virt.sil, FP_test_dyntype_specialization_from_caller_good, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 virt.sil, devirtualize_with_final_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]
 virt.sil, devirtualize_with_static_call_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here]

infer/tests/codetoanalyze/sil/pulse/virt.sil

@@ -97,7 +97,7 @@ define test_dyntype_specialization_from_caller_bad(x: *Int) : void {
     ret null
 }
 
-define FP_test_dyntype_specialization_from_caller_good(x: *Int) : void {
+define test_dyntype_specialization_from_caller_good(x: *Int) : void {
   #entry:
     n0 = __sil_eq(call_num_value_caller_on_allocated_int(), 42)
     prune !n0