From 4cd595aebd2d39407d2fc8876a0d61ea86f2d53d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 9 Jan 2020 02:01:05 -0800 Subject: [PATCH] [pulse] Add naive model for array length in Java Summary: Model array length in Java as returning an unknown interval [0, +inf] for now. Ideally, we can deal with the size in a more precise manner in the future like in InferBo. Reviewed By: skcho Differential Revision: D19312123 fbshipit-source-id: 8c51059a4 --- infer/src/bufferoverrun/itv.mli | 2 ++ infer/src/pulse/PulseArithmetic.ml | 2 ++ infer/src/pulse/PulseArithmetic.mli | 2 ++ infer/src/pulse/PulseModels.ml | 12 ++++++++++++ .../codetoanalyze/java/impurity/PurityModeled.java | 4 ++++ 5 files changed, 22 insertions(+) diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index b6db80f25..7eb70248f 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -29,6 +29,8 @@ module ItvPure : sig val zero : t + val nat : t + val of_int : int -> t val lb : t -> Bound.t diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index 737494522..7e562e111 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -416,6 +416,8 @@ let abduce_binop_constraints ~negated (bop : Binop.t) (a1 : t) (a2 : t) = Satisfiable (None, None) +let zero_inf = between (Int IntLit.zero) PlusInfinity + let abduce_binop_is_true ~negated bop v1 v2 = Logging.d_printfln "abduce_binop_is_true ~negated:%b %s (%a) (%a)" negated (Binop.str Pp.text bop) (Pp.option pp) v1 (Pp.option pp) v2 ; diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index a9365e4d4..b53d2e34a 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -35,3 +35,5 @@ val abduce_binop_is_true : negated:bool -> Binop.t -> t option -> t option -> ab val binop : Binop.t -> t -> t -> t option val unop : Unop.t -> t -> t option + +val zero_inf : t diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 736dae915..8afb9c3b1 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -48,6 +48,17 @@ module Misc = struct Ok [PulseOperations.write_id ret_id (ret_addr, []) astate] + let return_unknown_size : model = + fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> + let ret_addr = AbstractValue.mk_fresh () in + let astate = + Memory.add_attribute ret_addr (BoItv Itv.ItvPure.nat) astate + |> Memory.add_attribute ret_addr + (Arithmetic (Arithmetic.zero_inf, Immediate {location; history= []})) + in + Ok [PulseOperations.write_id ret_id (ret_addr, []) astate] + + let skip : model = fun ~caller_summary:_ _ ~ret:_ astate -> Ok [astate] let nondet ~fn_name : model = @@ -354,6 +365,7 @@ module ProcNameDispatcher = struct ; +match_builtin BuiltinDecl.__cast <>$ capt_arg_payload $+...$--> Misc.id_first_arg ; +match_builtin BuiltinDecl.abort <>--> Misc.early_exit ; +match_builtin BuiltinDecl.exit <>--> Misc.early_exit + ; +match_builtin BuiltinDecl.__get_array_length <>--> Misc.return_unknown_size ; (* consider that all fbstrings are small strings to avoid false positives due to manual ref-counting *) -"folly" &:: "fbstring_core" &:: "category" &--> Misc.return_int Int64.zero diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index facc8a335..0530f7921 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -15,4 +15,8 @@ class PurityModeled { // copies an array from the specified source array System.arraycopy(src, 0, dst, 0, 1); } + + public void array_length_loop_pure(Integer[] array) { + for (int i = 0; i < array.length; i++) {} + } }