From 5f8e6233bb702508e735e327dfab5df9ae68cf89 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Fri, 6 Mar 2020 03:16:13 -0800 Subject: [PATCH] [pulse] Take into account skipped calls for state comparison Summary: We forgot to take skipped calls into account for state comparison. This diff fixes that. Reviewed By: skcho Differential Revision: D20282739 fbshipit-source-id: 7b4d84bb0 --- infer/src/pulse/PulseAbductiveDomain.ml | 5 +++++ infer/src/pulse/PulseBaseDomain.ml | 9 ++++++++- infer/src/pulse/PulseBaseDomain.mli | 3 +-- .../tests/codetoanalyze/java/impurity/PurityModeled.java | 9 +++++++++ infer/tests/codetoanalyze/java/impurity/issues.exp | 1 + 5 files changed, 24 insertions(+), 3 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 60eb84eb8..9504c067c 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -93,6 +93,11 @@ type t = let pp f {post; pre} = F.fprintf f "@[%a@;PRE=[%a]@]" Domain.pp post InvertedDomain.pp pre let leq ~lhs ~rhs = + (* We only care about post state for skipped calls. TODO: Pull + skipped calls out of BaseDomain to here. *) + BaseDomain.SkippedCalls.leq ~lhs:(lhs.post :> BaseDomain.t).skipped_calls + ~rhs:(rhs.post :> BaseDomain.t).skipped_calls + && match BaseDomain.isograph_map BaseDomain.empty_mapping ~lhs:(rhs.pre :> BaseDomain.t) diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index 4417a3bc0..9daaa302f 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/infer/src/pulse/PulseBaseDomain.ml @@ -18,9 +18,16 @@ module SkippedTrace = struct let pp fmt = PulseTrace.pp fmt ~pp_immediate:(fun fmt -> F.pp_print_string fmt "call to skipped function occurs here" ) + + + let leq ~lhs ~rhs = phys_equal lhs rhs + + let join _ _ = assert false + + let widen ~prev:_ ~next:_ ~num_iters:_ = assert false end -module SkippedCalls = PrettyPrintable.MakePPMonoMap (Procname) (SkippedTrace) +module SkippedCalls = AbstractDomain.Map (Procname) (SkippedTrace) (* {2 Abstract domain description } *) diff --git a/infer/src/pulse/PulseBaseDomain.mli b/infer/src/pulse/PulseBaseDomain.mli index 89920a839..95b3e9256 100644 --- a/infer/src/pulse/PulseBaseDomain.mli +++ b/infer/src/pulse/PulseBaseDomain.mli @@ -13,8 +13,7 @@ module SkippedTrace : sig type t = PulseTrace.t end -module SkippedCalls : - PrettyPrintable.PPMonoMap with type key = Procname.t and type value = SkippedTrace.t +module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = SkippedTrace.t type t = { heap: PulseBaseMemory.t diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index 9ebcebff9..f7dd01313 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -82,9 +82,18 @@ class PurityModeled { list.set(0, "e"); } + // Pulse can only widen a fixed number of times, hence it thinks + // that the exit of the loop never reaches and results in empty + // post. void timing_call_in_loop_impure_FN() { for (int i = 0; i < 10; i++) { System.nanoTime(); } } + + void timing_call_in_loop_symb_impure(int n) { + for (int i = 0; i < n; i++) { + System.nanoTime(); + } + } } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index ee23a1731..de59d00da 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -22,6 +22,7 @@ codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_set_impure(ja 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.remove_impure(java.util.Iterator):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure(Iterator),parameter `i` of void PurityModeled.remove_impure(Iterator),parameter `i` 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` accessed here,global variable `Test` modified here] codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter `array` of void Test.alias_impure(int[],int,int),assigned,parameter `array` modified here]