[pulse][specialization] new flag to enforce more strict incorrectness logic on call resolution failure

Summary: if specialization can not satisfy callee specialization needs, we cut exploration (if the new option is set). false by default.

Reviewed By: dulmarod

Differential Revision: D91479599

fbshipit-source-id: 2f0df8b85f8272540ca9535814dfb7dafcb2b177

Author: davidpichardie

infer/man/man1/infer-full.txt

@@ -3234,6 +3234,11 @@ INTERNAL OPTIONS
        --pulse-skip-procedures-reset
            Cancel the effect of --pulse-skip-procedures.
 
+       --pulse-specialization-abort-if-impossible
+           Activates: If a caller can not satisfy callee specialization
+           needs, abort current symbolic execution (Conversely:
+           --no-pulse-specialization-abort-if-impossible)
+
        --no-pulse-specialization-partial
            Deactivates: A caller does not wait to have a full set of
            specialization information before running a specialized analysis

infer/src/base/Config.ml

@@ -2719,6 +2719,11 @@ and pulse_skip_procedures =
     ~meta:"regex" "Regex of procedures that should not be analyzed by Pulse."
 
 
+and pulse_specialization_abort_if_impossible =
+  CLOpt.mk_bool ~long:"pulse-specialization-abort-if-impossible" ~default:false
+    "If a caller can not satisfy callee specialization needs, abort current symbolic execution"
+
+
 and pulse_specialization_iteration_limit =
   CLOpt.mk_int ~long:"pulse-specialization-iteration-limit" ~default:20
     ~in_help:InferCommand.[(Analyze, manual_pulse)]
@@ -4650,6 +4655,8 @@ and pulse_sanity_checks = !pulse_sanity_checks
 
 and pulse_skip_procedures = Option.map ~f:Str.regexp !pulse_skip_procedures
 
+and pulse_specialization_abort_if_impossible = !pulse_specialization_abort_if_impossible
+
 and pulse_specialization_iteration_limit = !pulse_specialization_iteration_limit
 
 and pulse_specialization_limit = !pulse_specialization_limit

infer/src/base/Config.mli

@@ -684,6 +684,8 @@ val pulse_sanity_checks : bool
 
 val pulse_skip_procedures : Str.regexp option
 
+val pulse_specialization_abort_if_impossible : bool
+
 val pulse_specialization_iteration_limit : int
 
 val pulse_specialization_limit : int

infer/src/pulse/PulseCallOperations.ml

@@ -836,6 +836,7 @@ let call ?disjunct_limit ({InterproceduralAnalysis.analyze_dependency} as analys
   in
   let rec iter_call ~max_iteration ~nth_iteration ~is_pulse_specialization_limit_reached
       ?(specialization = Specialization.Pulse.bottom) already_given summary astate =
+    L.d_printfln ~color:Orange "iter_call %d" nth_iteration ;
     let res, non_disj, contradiction = call_specialized specialization summary astate in
     let needs_aliasing_specialization =
       match (res, contradiction) with
@@ -927,7 +928,9 @@ let call ?disjunct_limit ({InterproceduralAnalysis.analyze_dependency} as analys
               Specialization.Pulse.pp specialization ;
           if nth_iteration >= max_iteration then
             L.d_printfln "[specialization] we have reached the maximum number of iteration" ;
-          if
+          if nth_iteration >= max_iteration && Config.pulse_specialization_abort_if_impossible then
+            case_if_specialization_is_impossible []
+          else if
             nth_iteration >= max_iteration || has_already_be_given || ask_caller_of_caller_first
             || Specialization.Pulse.is_bottom specialization
           then