[inferbo] Disable function instantiation of relational domain

Summary:
This diff makes it sure that Inferbo does nothing on relational domain
at function calls when the command line option for them is not given.

Reviewed By: ezgicicek

Differential Revision: D16647903

fbshipit-source-id: 74ef251fe

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -150,19 +150,21 @@ module TransferFunctions = struct
       -> Dom.Mem.t =
    fun tenv integer_type_widths ret callee_formals callee_pname params caller_mem callee_exit_mem
        location ->
-    let rel_subst_map =
-      Sem.get_subst_map tenv integer_type_widths callee_formals params caller_mem callee_exit_mem
-    in
     let eval_sym_trace =
       Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem
         ~mode:Sem.EvalNormal
     in
-    let caller_mem =
+    let caller_mem' =
       instantiate_mem_reachable ret callee_formals callee_pname ~callee_exit_mem eval_sym_trace
         caller_mem location
       |> forget_ret_relation ret callee_pname
     in
-    Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem
+    Option.value_map Config.bo_relational_domain ~default:caller_mem' ~f:(fun _ ->
+        let rel_subst_map =
+          Sem.get_subst_map tenv integer_type_widths callee_formals params caller_mem
+            callee_exit_mem
+        in
+        Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem' ~callee:callee_exit_mem )
 
 
   let rec is_array_access_exp = function

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -253,7 +253,9 @@ let instantiate_cond :
  fun tenv integer_type_widths callee_pname callee_formals params caller_mem callee_exit_mem
      callee_cond location ->
   let rel_subst_map =
+    Option.value_map Config.bo_relational_domain ~default:Relation.SubstMap.empty ~f:(fun _ ->
         Sem.get_subst_map tenv integer_type_widths callee_formals params caller_mem callee_exit_mem
+    )
   in
   let caller_rel = Dom.Mem.get_relation caller_mem in
   let eval_sym_trace =

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -408,9 +408,13 @@ module ArrayAccessCondition = struct
       (ItvPure.subst c.offset eval_sym, ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym)
     with
     | NonBottom offset, NonBottom idx, NonBottom size ->
-        let idx_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp in
+        let idx_sym_exp, size_sym_exp, relation =
-        let size_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp in
+          if Option.is_none Config.bo_relational_domain then (None, None, Relation.bot)
-        let relation = Relation.instantiate rel_map ~caller:caller_relation ~callee:c.relation in
+          else
+            ( Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp
+            , Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp
+            , Relation.instantiate rel_map ~caller:caller_relation ~callee:c.relation )
+        in
         let void_ptr =
           c.void_ptr || ItvPure.has_void_ptr_symb offset || ItvPure.has_void_ptr_symb idx
           || ItvPure.has_void_ptr_symb size