From c92d56e4add6150e308199f6187e01e98163574f Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Sun, 24 Mar 2019 18:42:21 -0700 Subject: [PATCH] [inferbo] Substitute symbolic value of unknown function call to top Summary: This diff substitutes symbolic values for unknown functions in proof obligations to top. The goal of the diff is to avoid generating too many number of proof obligations that cannot be concretized. Reviewed By: ezgicicek Differential Revision: D14537542 fbshipit-source-id: 7f8f3bb4b --- .../bufferoverrun/bufferOverrunAnalysis.ml | 3 +- .../bufferOverrunProofObligations.ml | 9 ++- .../bufferOverrunProofObligations.mli | 2 +- .../bufferoverrun/bufferOverrunSemantics.ml | 72 +++++++++++-------- .../java/bufferoverrun/.inferconfig | 3 + .../java/bufferoverrun/External.java | 20 ++++++ .../codetoanalyze/java/bufferoverrun/Makefile | 2 +- .../java/bufferoverrun/issues.exp | 2 + 8 files changed, 80 insertions(+), 33 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/bufferoverrun/.inferconfig create mode 100644 infer/tests/codetoanalyze/java/bufferoverrun/External.java diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 430566b74..68ea66b77 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -131,7 +131,8 @@ module TransferFunctions = struct 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 ~strict:false + Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem + ~mode:Sem.EvalNormal in let caller_mem = instantiate_mem_reachable ret callee_formals callee_pname ~callee_exit_mem eval_sym_trace diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 1614f0879..d606a523a 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -14,6 +14,7 @@ module Dom = BufferOverrunDomain module ItvPure = Itv.ItvPure module MF = MarkupFormatter module Relation = BufferOverrunDomainRelation +module Sem = BufferOverrunSemantics module ValTrace = BufferOverrunTrace module ConditionTrace = struct @@ -753,9 +754,13 @@ module ConditionWithTrace = struct "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 ; - match Dom.Reachability.subst cwt.reachability (eval_sym_trace ~strict:true) call_site with + match + Dom.Reachability.subst cwt.reachability + (eval_sym_trace ~mode:Sem.EvalPOReachability) + call_site + with | `Reachable reachability -> ( - let {Dom.eval_sym; trace_of_sym} = eval_sym_trace ~strict:false in + let {Dom.eval_sym; trace_of_sym} = eval_sym_trace ~mode:Sem.EvalPOCond in match Condition.subst eval_sym rel_map caller_relation cwt.cond with | None -> None diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index a99f2eaad..591bb577d 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -73,7 +73,7 @@ module ConditionSet : sig val subst : summary_t - -> (strict:bool -> BufferOverrunDomain.eval_sym_trace) + -> (mode:BufferOverrunSemantics.eval_mode -> BufferOverrunDomain.eval_sym_trace) -> Relation.SubstMap.t -> Relation.t -> Typ.Procname.t diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 55d5c2e76..5976030aa 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -363,81 +363,97 @@ module ParamBindings = struct add_binding formals actuals empty end -let rec eval_sympath_partial ~strict params p mem = +(* There are three modes of ondemand evaluations. + + EvalNormal: Given a symbolic value of an unknown function [Symb.SymbolPath.Callsite], it returns + a symbolic interval value. + + EvalPOCond: Given a symbolic value of an unknown function, it returns the top interval value. + This is used when substituting condition expressions of proof obligations. + + EvalPOReachability: This is similar to [EvalPOCond], but it returns the bottom location, instead + of the unknown location, when a location to substitute is not found. This is used when + substituting reachabilities of proof obligations. *) +type eval_mode = EvalNormal | EvalPOCond | EvalPOReachability + +let rec eval_sympath_partial ~mode params p mem = match p with | Symb.SymbolPath.Pvar x -> ( try ParamBindings.find x params with Caml.Not_found -> L.d_printfln_escaped "Symbol %a is not found in parameters." (Pvar.pp Pp.text) x ; Val.Itv.top ) - | Symb.SymbolPath.Callsite {cs} -> - L.d_printfln_escaped "Symbol for %a is not expected to be in parameters." Typ.Procname.pp - (CallSite.pname cs) ; - Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem + | Symb.SymbolPath.Callsite {cs} -> ( + match mode with + | EvalNormal -> + L.d_printfln_escaped "Symbol for %a is not expected to be in parameters." Typ.Procname.pp + (CallSite.pname cs) ; + Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem + | EvalPOCond | EvalPOReachability -> + Val.Itv.top ) | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ -> - let locs = eval_locpath ~strict params p mem in + let locs = eval_locpath ~mode params p mem in Mem.find_set locs mem -and eval_locpath ~strict params p mem = +and eval_locpath ~mode params p mem = let res = match p with | Symb.SymbolPath.Pvar _ | Symb.SymbolPath.Callsite _ -> - let v = eval_sympath_partial ~strict params p mem in + let v = eval_sympath_partial ~mode params p mem in Val.get_all_locs v | Symb.SymbolPath.Deref (_, p) -> - let v = eval_sympath_partial ~strict params p mem in + let v = eval_sympath_partial ~mode params p mem in Val.get_all_locs v | Symb.SymbolPath.Field (fn, p) -> - let locs = eval_locpath ~strict params p mem in + let locs = eval_locpath ~mode params p mem in PowLoc.append_field ~fn locs in - 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 ) + if PowLoc.is_empty res then ( + match mode with + | EvalPOReachability -> + res + | EvalNormal | EvalPOCond -> + L.d_printfln_escaped "Location value for %a is not found." Symb.SymbolPath.pp_partial p ; + PowLoc.unknown ) else res -let eval_sympath ~strict params sympath mem = +let eval_sympath ~mode params sympath mem = match sympath with | Symb.SymbolPath.Normal p -> - let v = eval_sympath_partial ~strict params p mem in + let v = eval_sympath_partial ~mode params p mem in (Val.get_itv v, Val.get_traces v) | Symb.SymbolPath.Offset p -> - let v = eval_sympath_partial ~strict params p mem in + let v = eval_sympath_partial ~mode params p mem in (ArrayBlk.offsetof (Val.get_array_blk v), Val.get_traces v) | Symb.SymbolPath.Length p -> - let v = eval_sympath_partial ~strict params p mem in + let v = eval_sympath_partial ~mode 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_formals actual_exps caller_mem = let params = let actuals = List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps in ParamBindings.make callee_formals actuals in - let eval_sym s bound_end = + let eval_sym ~mode s bound_end = let sympath = Symb.Symbol.path s in - let itv, _ = eval_sympath ~strict:false params sympath caller_mem in + let itv, _ = eval_sympath ~mode 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 ~strict:false params sympath caller_mem in + let itv, traces = eval_sympath ~mode:EvalNormal params sympath caller_mem in if Itv.eq itv Itv.bot then TraceSet.bottom else traces in - 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 eval_locpath ~mode partial = eval_locpath ~mode params partial caller_mem in + fun ~mode -> {eval_sym= eval_sym ~mode; trace_of_sym; eval_locpath= eval_locpath ~mode} 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 ~strict:false + mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem ~mode:EvalNormal in eval_sym_trace.eval_sym diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/.inferconfig b/infer/tests/codetoanalyze/java/bufferoverrun/.inferconfig new file mode 100644 index 000000000..ba2186de8 --- /dev/null +++ b/infer/tests/codetoanalyze/java/bufferoverrun/.inferconfig @@ -0,0 +1,3 @@ +{ + "external-java-packages": ["external."] +} diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/External.java b/infer/tests/codetoanalyze/java/bufferoverrun/External.java new file mode 100644 index 000000000..b69cf17ab --- /dev/null +++ b/infer/tests/codetoanalyze/java/bufferoverrun/External.java @@ -0,0 +1,20 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +import external.library.SomeExternalClass; + +public class External { + /* This function should raise deduplicated issues because the symbolic value of external method + * should be instantiated to top. */ + void external_function_Bad(SomeExternalClass v) { + int i = (int) (v.externalMethod1()) + 1 + (int) (v.externalMethod1()) + 1; + } + + /* This function should have no proof obilgation. */ + void call_external_function_Good(SomeExternalClass v) { + external_function_Bad(v); + } +} diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/Makefile b/infer/tests/codetoanalyze/java/bufferoverrun/Makefile index 0fa36e192..3f52d8a7b 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/Makefile +++ b/infer/tests/codetoanalyze/java/bufferoverrun/Makefile @@ -10,6 +10,6 @@ INFER_OPTIONS = --bufferoverrun-only --no-filtering --debug-exceptions \ INFERPRINT_OPTIONS = --issues-tests -SOURCES = $(wildcard *.java) +SOURCES = $(wildcard *.java) $(wildcard $(TESTS_DIR)/external/library/*.java) include $(TESTS_DIR)/javac.make diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 6022abfa9..06676544d 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -7,3 +7,5 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5] codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this.buf[*]`,Assignment,,Array declaration,Assignment,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10] codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `this.yy`,,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32] +codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: __cast,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: int Integer.intValue(),Assignment,,Unknown value from: int Integer.intValue(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]