diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index eb78628de..3b7b20a4b 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -48,6 +48,14 @@ let prune_binop ~negated bop lhs_op rhs_op astate = AbductiveDomain.set_path_condition phi' astate +let prune_eq_zero v astate = + prune_binop ~negated:false Eq (AbstractValueOperand v) (LiteralOperand IntLit.zero) astate + + +let prune_positive v astate = + prune_binop ~negated:false Gt (AbstractValueOperand v) (LiteralOperand IntLit.zero) astate + + let is_known_zero astate v = PathCondition.is_known_zero astate.AbductiveDomain.path_condition v let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index 807849c59..85a5fcc25 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -30,6 +30,12 @@ val eval_unop : val prune_binop : negated:bool -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t +val prune_eq_zero : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t +(** helper function wrapping [prune_binop] *) + +val prune_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t +(** helper function wrapping [prune_binop] *) + val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool val is_unsat_cheap : AbductiveDomain.t -> bool diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 0a2bf8535..19cf09671 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -132,7 +132,7 @@ module Misc = struct let<+> astate = PulseOperations.invalidate location invalidation deleted_access astate in astate in - let astate_zero = PulseArithmetic.and_eq_int (fst deleted_access) IntLit.zero astate in + let astate_zero = PulseArithmetic.prune_eq_zero (fst deleted_access) astate in Ok (ContinueProgram astate_zero) :: astates_alloc end @@ -306,10 +306,10 @@ module Optional = struct let ret_value = (ret_addr, [ValueHistory.Call {f= Model desc; location; in_call= []}]) in let<*> astate, (value_addr, _) = to_internal_value_deref Read location optional astate in let astate = PulseOperations.write_id ret_id ret_value astate in - let astate_non_empty = PulseArithmetic.and_positive value_addr astate in - let astate_true = PulseArithmetic.and_positive ret_addr astate_non_empty in - let astate_empty = PulseArithmetic.and_eq_int value_addr IntLit.zero astate in - let astate_false = PulseArithmetic.and_eq_int ret_addr IntLit.zero astate_empty in + let astate_non_empty = PulseArithmetic.prune_positive value_addr astate in + let astate_true = PulseArithmetic.prune_positive ret_addr astate_non_empty in + let astate_empty = PulseArithmetic.prune_eq_zero value_addr astate in + let astate_false = PulseArithmetic.prune_eq_zero ret_addr astate_empty in [Ok (ContinueProgram astate_false); Ok (ContinueProgram astate_true)] @@ -320,12 +320,12 @@ module Optional = struct let value_update_hist = (fst value_addr, event :: snd value_addr) in let astate_value_addr = PulseOperations.write_id ret_id value_update_hist astate - |> PulseArithmetic.and_positive (fst value_addr) + |> PulseArithmetic.prune_positive (fst value_addr) in let nullptr = (AbstractValue.mk_fresh (), [event]) in let<*> astate_null = PulseOperations.write_id ret_id nullptr astate - |> PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero + |> PulseArithmetic.prune_eq_zero (fst value_addr) |> PulseArithmetic.and_eq_int (fst nullptr) IntLit.zero |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) nullptr in @@ -336,7 +336,7 @@ module Optional = struct fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, value_addr = to_internal_value_deref Read location optional astate in - let astate_non_empty = PulseArithmetic.and_positive (fst value_addr) astate in + let astate_non_empty = PulseArithmetic.prune_positive (fst value_addr) astate in let<*> astate_non_empty, value = PulseOperations.eval_access Read location value_addr Dereference astate_non_empty in @@ -346,7 +346,7 @@ module Optional = struct PulseOperations.eval_access Read location default Dereference astate in let default_value_hist = (default_val, event :: default_hist) in - let astate_empty = PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero astate in + let astate_empty = PulseArithmetic.prune_eq_zero (fst value_addr) astate in let astate_default = PulseOperations.write_id ret_id default_value_hist astate_empty in [Ok (ContinueProgram astate_value); Ok (ContinueProgram astate_default)] end @@ -1028,13 +1028,13 @@ module JavaPreconditions = struct let check_not_null (address, hist) : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "Preconditions.checkNotNull"; location; in_call= []} in - let astate = PulseArithmetic.and_positive address astate in + let astate = PulseArithmetic.prune_positive address astate in PulseOperations.write_id ret_id (address, event :: hist) astate |> ok_continue let check_state_argument (address, _) : model = fun _ ~callee_procname:_ _ ~ret:_ astate -> - PulseArithmetic.and_positive address astate |> ok_continue + PulseArithmetic.prune_positive address astate |> ok_continue end module StringSet = Caml.Set.Make (String) diff --git a/infer/tests/codetoanalyze/java/pulse/PreconditionsExample.java b/infer/tests/codetoanalyze/java/pulse/PreconditionsExample.java index e358ac6f0..4aaf2d26c 100644 --- a/infer/tests/codetoanalyze/java/pulse/PreconditionsExample.java +++ b/infer/tests/codetoanalyze/java/pulse/PreconditionsExample.java @@ -56,7 +56,7 @@ public class PreconditionsExample { x.toString(); } - void testCheckNotNullArgBad(Object x) { + void testCheckNotNullArgLatent(Object x) { Object y = null; Preconditions.checkNotNull(x); y.toString(); diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 4143a5fa6..175e9ea23 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -58,7 +58,7 @@ codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.Nu codetoanalyze/java/pulse/NullSafeExample.java, OtherClass.buggyMethodBad():java.lang.String, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `OtherClass.()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `OtherClass.()`,assigned,return from call to `OtherClass.()`,passed as argument to `OtherClass OtherClass.canReturnNull()`,return from call to `OtherClass OtherClass.canReturnNull()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/PreconditionsExample.java, codetoanalyze.java.infer.PreconditionsExample.checkArgumentSatBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/PreconditionsExample.java, codetoanalyze.java.infer.PreconditionsExample.checkStateConditionSatBad():void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] -codetoanalyze/java/pulse/PreconditionsExample.java, codetoanalyze.java.infer.PreconditionsExample.testCheckNotNullArgBad(java.lang.Object):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/java/pulse/PreconditionsExample.java, codetoanalyze.java.infer.PreconditionsExample.testCheckNotNullArgLatent(java.lang.Object):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressAllWarnigsInTheClass.shouldNotReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.(), 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.FP_shouldNotReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]