From b3770d0f173472afc52df7eb105f0b74c53f23cd Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 12 May 2020 02:06:51 -0700 Subject: [PATCH] [litho] Add sematics of assume null Summary: This diff adds semantics of assume null, heuristics. When `assume(x == null)`, it removes the methods called on the builder `*x` from the abstract state. ``` x -> {p} p -> {method1 called} assume(x == null) x -> {p} ``` This heuristics is unsound: Even though `x` (a pointer to builder object) points-to an builder object, which cannot imply that the object `p` does not exist in the concrete semantics. The unsoundness may appear when there is an alias (see the FP test added). Reviewed By: ezgicicek Differential Revision: D21502923 fbshipit-source-id: 2e392bd89 --- infer/src/checkers/LithoDomain.ml | 13 ++++++++ infer/src/checkers/LithoDomain.mli | 3 ++ infer/src/checkers/RequiredProps.ml | 19 +++++++++++ .../litho-required-props/RequiredProps.java | 32 +++++++++++++++++++ .../java/litho-required-props/issues.exp | 3 ++ 5 files changed, 70 insertions(+) diff --git a/infer/src/checkers/LithoDomain.ml b/infer/src/checkers/LithoDomain.ml index c60265391..2c1dba430 100644 --- a/infer/src/checkers/LithoDomain.ml +++ b/infer/src/checkers/LithoDomain.ml @@ -401,6 +401,17 @@ module Mem = struct {x with created= Created.add lhs (Created.lookup rhs created) created} + let assume_null path ({created; method_called} as x) = + match CreatedLocations.is_singleton_or_more (Created.lookup path created) with + | Singleton loc -> + let method_called = + MethodCalled.remove {created_location= loc; is_build_called= false} method_called + in + {x with method_called} + | Empty | More -> + x + + let call_create lhs typ_name location ({created} as x) = let created_location = CreatedLocation.ByCreateMethod {location; typ_name; latest_callsite= location} @@ -521,6 +532,8 @@ let map_no_return_called f x = {x with no_return_called= f x.no_return_called} let assign ~lhs ~rhs = map_no_return_called (Mem.assign ~lhs ~rhs) +let assume_null x = map_no_return_called (Mem.assume_null x) + let call_create lhs typ_name location = map_no_return_called (Mem.call_create lhs typ_name location) let call_builder ~ret ~receiver callee = diff --git a/infer/src/checkers/LithoDomain.mli b/infer/src/checkers/LithoDomain.mli index 6eb585dd8..1d67ed72b 100644 --- a/infer/src/checkers/LithoDomain.mli +++ b/infer/src/checkers/LithoDomain.mli @@ -53,6 +53,9 @@ val init : Tenv.t -> Procname.t -> (Pvar.t * Typ.t) list -> LocalAccessPath.t -> val assign : lhs:LocalAccessPath.t -> rhs:LocalAccessPath.t -> t -> t +val assume_null : LocalAccessPath.t -> t -> t +(** Semantics of null assume statement, i.e., [assume(x==null)] *) + val call_create : LocalAccessPath.t -> Typ.name -> Location.t -> t -> t (** Semantics of builder creation method *) diff --git a/infer/src/checkers/RequiredProps.ml b/infer/src/checkers/RequiredProps.ml index 20c071b82..d2e0570f6 100644 --- a/infer/src/checkers/RequiredProps.ml +++ b/infer/src/checkers/RequiredProps.ml @@ -206,6 +206,13 @@ module TransferFunctions = struct ~caller:astate ~callee:callee_summary ) + let assume_null caller_pname x astate = + let access_path = + Domain.LocalAccessPath.make (HilExp.AccessExpression.to_access_path x) caller_pname + in + Domain.assume_null access_path astate + + let exec_instr astate {interproc= {proc_desc; tenv}; get_proc_summary_and_formals} _ (instr : HilInstr.t) : Domain.t = let caller_pname = Procdesc.get_proc_name proc_desc in @@ -270,6 +277,18 @@ module TransferFunctions = struct astate in if HilExp.AccessExpression.is_return_var lhs_ae then Domain.call_return astate else astate + | Assume (BinaryOperator (Eq, AccessExpression x, null), _, _, _) + when HilExp.is_null_literal null -> + assume_null caller_pname x astate + | Assume (BinaryOperator (Eq, null, AccessExpression x), _, _, _) + when HilExp.is_null_literal null -> + assume_null caller_pname x astate + | Assume (UnaryOperator (LNot, BinaryOperator (Ne, AccessExpression x, null), _), _, _, _) + when HilExp.is_null_literal null -> + assume_null caller_pname x astate + | Assume (UnaryOperator (LNot, BinaryOperator (Ne, null, AccessExpression x), _), _, _, _) + when HilExp.is_null_literal null -> + assume_null caller_pname x astate | _ -> astate diff --git a/infer/tests/codetoanalyze/java/litho-required-props/RequiredProps.java b/infer/tests/codetoanalyze/java/litho-required-props/RequiredProps.java index 45bd50ed5..99a7a8d19 100644 --- a/infer/tests/codetoanalyze/java/litho-required-props/RequiredProps.java +++ b/infer/tests/codetoanalyze/java/litho-required-props/RequiredProps.java @@ -521,4 +521,36 @@ public class RequiredProps { builder1.prop1(new Object()).prop3(new Object()).build(); builder2.prop3(new Object()).build(); } + + public void nullableBuilderOk(boolean b) { + MyComponent.Builder builderOk = + mMyComponent.create().prop1(new Object()).prop2(new Object()).prop3(new Object()); + MyComponent.Builder builder = null; + if (b) { + builder = mMyComponent.create().prop1(new Object()).prop2(new Object()); + } + (builder == null ? builderOk : builder.prop3(new Object())).build(); + } + + public void nullableBuilderBad(boolean b) { + MyComponent.Builder builderOk = + mMyComponent.create().prop1(new Object()).prop2(new Object()).prop3(new Object()); + MyComponent.Builder builder = null; + if (b) { + builder = mMyComponent.create().prop2(new Object()); + } + (builder == null ? builderOk : builder.prop3(new Object())).build(); + } + + public void nullableBuilderAliasOk_FP(boolean b) { + MyComponent.Builder builder = + mMyComponent.create().prop1(new Object()).prop2(new Object()).prop3(new Object()); + MyComponent.Builder alias = builder; + if (b) { + builder = null; + } + if (builder == null) { + alias.build(); + } + } } diff --git a/infer/tests/codetoanalyze/java/litho-required-props/issues.exp b/infer/tests/codetoanalyze/java/litho-required-props/issues.exp index c347b81d6..1fdac41d0 100644 --- a/infer/tests/codetoanalyze/java/litho-required-props/issues.exp +++ b/infer/tests/codetoanalyze/java/litho-required-props/issues.exp @@ -26,6 +26,9 @@ codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.l codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.missingProp1InBothBranchesBeforeBuildBad(boolean):com.facebook.litho.Component, 4, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component com.facebook.litho.MyLithoComponent, but is not set before the call to build(),calls com.facebook.litho.MyLithoComponent.create(...),calls prop2(...)] codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.missingProp2InOneBranchBeforeBuildBad(boolean):com.facebook.litho.Component, 4, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop2** is required for component com.facebook.litho.MyLithoComponent, but is not set before the call to build(),calls com.facebook.litho.MyLithoComponent.create(...),calls prop1(...)] codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.missingProp3InOneBranchBeforeBuildBad(boolean):com.facebook.litho.Component, 3, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop3** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop1(...)] +codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.nullableBuilderAliasOk_FP(boolean):void, 2, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...)] +codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.nullableBuilderAliasOk_FP(boolean):void, 2, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop3** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...)] +codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.nullableBuilderBad(boolean):void, 5, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop2(...),calls prop3(...)] codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.setProp3InCalleeButForgetProp1Bad():com.facebook.litho.Component, 1, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop2(...),calls prop3(...)] codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.setRequiredOnBothBranchesMissingProp3Bad(boolean):com.facebook.litho.Component, 1, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop3** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop1(...),calls prop2(...)] codetoanalyze/java/litho-required-props/RequiredProps.java, codetoanalyze.java.litho.RequiredProps.setRequiredOnOneBothBranchesWithCreateOk_FP(boolean):com.facebook.litho.Component, 1, MISSING_REQUIRED_PROP, no_bucket, ERROR, [**@Prop prop1** is required for component codetoanalyze.java.litho.MyComponent, but is not set before the call to build(),calls codetoanalyze.java.litho.MyComponent.create(...),calls prop2(...),calls prop3(...)]