From f488c5d6b7be2ac8a7bfd8fc1edd306b1a9b22ed Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 7 Aug 2019 03:43:24 -0700 Subject: [PATCH] [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 | 12 +++++++----- infer/src/bufferoverrun/bufferOverrunChecker.ml | 4 +++- .../bufferoverrun/bufferOverrunProofObligations.ml | 10 +++++++--- 3 files changed, 17 insertions(+), 9 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 6f0d7c62f..b275f2f83 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 3f362795e..cd5f43251 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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 = - Sem.get_subst_map tenv integer_type_widths callee_formals params caller_mem callee_exit_mem + 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 = diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 73d895dc8..8951ec2b4 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/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 size_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp in - let relation = Relation.instantiate rel_map ~caller:caller_relation ~callee:c.relation in + let idx_sym_exp, size_sym_exp, relation = + if Option.is_none Config.bo_relational_domain then (None, None, Relation.bot) + 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