From b372befee4f833f8877937ca43d38f00bb8e3b0b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Tue, 17 Mar 2020 03:36:55 -0700 Subject: [PATCH] [pulse] Add more naive Java models Summary: This diff naively models the following as `StdVector.push_back`: - `StringBuilder.append` - `String.replace` - `Queue.poll` It also adds a FN test for `Iterator.next`. Reviewed By: skcho Differential Revision: D20469786 fbshipit-source-id: 2d8e8d117 --- infer/src/pulse/PulseModels.ml | 13 +++++++++- .../java/impurity/PurityModeled.java | 26 +++++++++++++++++++ .../codetoanalyze/java/impurity/issues.exp | 3 +++ 3 files changed, 41 insertions(+), 1 deletion(-) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index dbcc755ae..758cc30fe 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -400,7 +400,9 @@ module ProcNameDispatcher = struct let dispatch : (Tenv.t, model, arg_payload) ProcnameDispatcher.Call.dispatcher = let open ProcnameDispatcher.Call in let match_builtin builtin _ s = String.equal s (Procname.get_method builtin) in - let pushback_modeled = StringSet.of_list ["add"; "put"; "addAll"; "putAll"; "remove"] in + let pushback_modeled = + StringSet.of_list ["add"; "addAll"; "append"; "remove"; "replace"; "poll"; "put"; "putAll"] + in make_dispatcher [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc @@ -470,6 +472,15 @@ module ProcNameDispatcher = struct ; +PatternMatch.implements_collection &::+ (fun _ str -> StringSet.mem str pushback_modeled) <>$ capt_arg_payload $+...$--> StdVector.push_back + ; +PatternMatch.implements_queue + &::+ (fun _ str -> StringSet.mem str pushback_modeled) + <>$ capt_arg_payload $+...$--> StdVector.push_back + ; +PatternMatch.implements_lang "StringBuilder" + &::+ (fun _ str -> StringSet.mem str pushback_modeled) + <>$ capt_arg_payload $+...$--> StdVector.push_back + ; +PatternMatch.implements_lang "String" + &::+ (fun _ str -> StringSet.mem str pushback_modeled) + <>$ capt_arg_payload $+...$--> StdVector.push_back ; +PatternMatch.implements_iterator &:: "remove" <>$ capt_arg_payload $+...$--> StdVector.push_back ; +PatternMatch.implements_map &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index 9cb67e089..2c30e5cd0 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -7,6 +7,7 @@ import java.util.ArrayList; import java.util.Enumeration; import java.util.Iterator; +import java.util.Queue; class PurityModeled { @@ -133,4 +134,29 @@ class PurityModeled { ArrayList cloned = (ArrayList) list.clone(); cloned.add(""); // no change the list } + + String replace_impure(String s) { + return s.replace('a', 'f'); + } + + void process_queue_impure(ArrayList list, Queue queue) { + for (Integer el : list) { + queue.add(el); + } + } + + void append_impure(StringBuilder strBuilder) { + strBuilder.append("JavaGuru"); + } + + void append_pure() { + StringBuilder strBuilder = new StringBuilder("Core"); + strBuilder.append("JavaGuru"); + } + + // Our model of Iterator.next is wrong. It should be modeled as + // impure. + Integer next_impure_FN(Iterator it) { + return it.next(); + } } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index afaa2d689..e3ed05e82 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -14,6 +14,7 @@ codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java. codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_first_el_impure(ArrayList),parameter `list` modified here] codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_via_call_impure(ArrayList),when calling `void Localities$Foo.inc_impure()` here,parameter `list` modified here] codetoanalyze/java/impurity/Localities.java, Localities.newHashCode_impure():int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int Localities.newHashCode_impure(),call to skipped function int Object.hashCode() occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.append_impure(java.lang.StringBuilder):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.append_impure(StringBuilder),parameter `strBuilder` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.arraycopy_pure_FP(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.arraycopy_pure_FP(int[]),call to skipped function void System.arraycopy(Object,int,Object,int,int) occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_timing_symb_unrelated_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_timing_symb_unrelated_impure(int,int),when calling `void PurityModeled.timing_call_in_loop_symb_impure(int)` here,call to skipped function long System.nanoTime() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_write_impure(),when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here] @@ -22,7 +23,9 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_addall_impure codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_set_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_set_impure(ArrayList),parameter `list` was potentially invalidated by `std::vector::assign()` here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_impure():double, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double PurityModeled.math_random_impure(),call to skipped function double Math.random() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loop_impure(int):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int PurityModeled.math_random_in_loop_impure(int),when calling `void PurityModeled.call_write_impure()` here,when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here,call to skipped function double Math.random() occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.process_queue_impure(java.util.ArrayList,java.util.Queue):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.process_queue_impure(ArrayList,Queue),parameter `queue` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure(java.util.Iterator):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure(Iterator),parameter `i` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.replace_impure(java.lang.String):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.replace_impure(String),parameter `s` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_symb_impure(int),call to skipped function long System.nanoTime() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.write_impure(),call to skipped function void PrintStream.write(byte[],int,int) occurs here] codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` modified here]