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]