[inferbo] Substitute conditions of proof obligations strictly

Summary:
This diff substitutes the conditions of proof obligations strictly, so that the condition of "p!=Null" becomes bottom
when callee's p is Null.

In the non-strict substitution (which is used by default), if p's location is not found it returns the unknown location.
On the other hand, in the strict substitution (which is used only in the substitution of condition of proof obligation),
it returns bottom location.

Depends on D13415366, D13414636

Reviewed By: mbouaziz, jvillard

Differential Revision: D13415377

fbshipit-source-id: 5ae1e888e

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -144,7 +144,7 @@ module TransferFunctions = struct
       Sem.get_subst_map tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem
     in
     let eval_sym_trace =
-      Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem
+      Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem ~strict:false
     in
     let caller_mem =
       instantiate_mem_reachable ret callee_pdesc callee_pname ~callee_exit_mem eval_sym_trace

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -711,16 +711,17 @@ module ConditionWithTrace = struct
         cmp
 
 
-  let subst ({Dom.eval_sym; trace_of_sym} as eval_sym_trace) rel_map caller_relation callee_pname
-      call_site cwt =
+  let subst eval_sym_trace rel_map caller_relation callee_pname call_site cwt =
     let symbols = Condition.get_symbols cwt.cond in
     if Symb.SymbolSet.is_empty symbols then
       L.(die InternalError)
         "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \
          the first place?"
         pp_summary cwt Typ.Procname.pp callee_pname Location.pp call_site ;
-    Option.find_map (Dom.LatestPrune.subst cwt.latest_prune eval_sym_trace call_site)
+    Option.find_map
+      (Dom.LatestPrune.subst cwt.latest_prune (eval_sym_trace ~strict:true) call_site)
       ~f:(fun latest_prune ->
+        let {Dom.eval_sym; trace_of_sym} = eval_sym_trace ~strict:false in
         match Condition.subst eval_sym rel_map caller_relation cwt.cond with
         | None ->
             None

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -74,7 +74,7 @@ module ConditionSet : sig
 
   val subst :
        summary_t
-    -> BufferOverrunDomain.eval_sym_trace
+    -> (strict:bool -> BufferOverrunDomain.eval_sym_trace)
     -> Relation.SubstMap.t
     -> Relation.t
     -> Typ.Procname.t

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -339,7 +339,7 @@ module ParamBindings = struct
     add_binding formals actuals empty
 end
 
-let rec eval_sympath_partial params p mem =
+let rec eval_sympath_partial ~strict params p mem =
   match p with
   | Symb.SymbolPath.Pvar x -> (
     try ParamBindings.find x params with Caml.Not_found ->
@@ -350,42 +350,47 @@ let rec eval_sympath_partial params p mem =
         (CallSite.pname cs) ;
       Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem
   | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ ->
-      let locs = eval_locpath params p mem in
+      let locs = eval_locpath ~strict params p mem in
       Mem.find_set locs mem
 
 
-and eval_locpath params p mem =
+and eval_locpath ~strict params p mem =
   let res =
     match p with
     | Symb.SymbolPath.Pvar _ | Symb.SymbolPath.Callsite _ ->
-        let v = eval_sympath_partial params p mem in
+        let v = eval_sympath_partial ~strict params p mem in
         Val.get_all_locs v
     | Symb.SymbolPath.Deref (_, p) ->
-        let v = eval_sympath_partial params p mem in
+        let v = eval_sympath_partial ~strict params p mem in
         Val.get_all_locs v
     | Symb.SymbolPath.Field (fn, p) ->
-        let locs = eval_locpath params p mem in
+        let locs = eval_locpath ~strict params p mem in
         PowLoc.append_field ~fn locs
   in
-  if PowLoc.is_empty res then (
+  if PowLoc.is_empty res && not strict then (
     L.d_printfln_escaped "Location value for %a is not found." Symb.SymbolPath.pp_partial p ;
     PowLoc.unknown )
   else res
 
 
-let eval_sympath params sympath mem =
+let eval_sympath ~strict params sympath mem =
   match sympath with
   | Symb.SymbolPath.Normal p ->
-      let v = eval_sympath_partial params p mem in
+      let v = eval_sympath_partial ~strict params p mem in
       (Val.get_itv v, Val.get_traces v)
   | Symb.SymbolPath.Offset p ->
-      let v = eval_sympath_partial params p mem in
+      let v = eval_sympath_partial ~strict params p mem in
       (ArrayBlk.offsetof (Val.get_array_blk v), Val.get_traces v)
   | Symb.SymbolPath.Length p ->
-      let v = eval_sympath_partial params p mem in
+      let v = eval_sympath_partial ~strict params p mem in
       (ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v)
 
 
+(* We have two modes (strict and non-strict) on evaluating location paths. When a location to
+   substitute is not found:
+   - non-strict mode (which is used by default): it returns the unknown location.
+   - strict mode (which is used only in the substitution of condition of proof obligation): it
+     returns the bottom location. *)
 let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem =
   let params =
     let formals = Procdesc.get_pvar_formals callee_pdesc in
@@ -394,21 +399,23 @@ let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem =
   in
   let eval_sym s bound_end =
     let sympath = Symb.Symbol.path s in
-    let itv, _ = eval_sympath params sympath caller_mem in
+    let itv, _ = eval_sympath ~strict:false params sympath caller_mem in
     Symb.Symbol.assert_bound_end s bound_end ;
     Itv.get_bound itv bound_end
   in
   let trace_of_sym s =
     let sympath = Symb.Symbol.path s in
-    let itv, traces = eval_sympath params sympath caller_mem in
+    let itv, traces = eval_sympath ~strict:false params sympath caller_mem in
     if Itv.eq itv Itv.bot then TraceSet.empty else traces
   in
-  let eval_locpath partial = eval_locpath params partial caller_mem in
-  {eval_sym; trace_of_sym; eval_locpath}
+  let eval_locpath ~strict partial = eval_locpath ~strict params partial caller_mem in
+  fun ~strict -> {eval_sym; trace_of_sym; eval_locpath= eval_locpath ~strict}
 
 
 let mk_eval_sym integer_type_widths callee_pdesc actual_exps caller_mem =
-  let eval_sym_trace = mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem in
+  let eval_sym_trace =
+    mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem ~strict:false
+  in
   eval_sym_trace.eval_sym
 
 

infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp

@@ -51,7 +51,7 @@ void conditional_minus(int* ptr, unsigned int size) {
   }
 }
 
-void call_conditional_minus_1_Good_FP() { conditional_minus(NULL, 0); }
+void call_conditional_minus_1_Good() { conditional_minus(NULL, 0); }
 
 void call_conditional_minus_2_Good() {
   int a[3];
@@ -69,7 +69,7 @@ unsigned int conditional_minus2(int* ptr, unsigned int size) {
   }
 }
 
-void call_conditional_minus2_1_Good_FP() { conditional_minus2(NULL, 0); }
+void call_conditional_minus2_1_Good() { conditional_minus2(NULL, 0); }
 
 void call_conditional_minus2_2_Good() {
   int a[3];

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -30,9 +30,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L
 codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `size`,<Length trace>,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Array access: Offset: 2 Size: 1 by call to `conditional_buffer_access` ]
-codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ]
-codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ]
 codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `__x->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64]