diff --git a/infer/src/nullsafe/IDEnv.ml b/infer/src/nullsafe/IDEnv.ml index 12450cf84..bc2a2c5e6 100644 --- a/infer/src/nullsafe/IDEnv.ml +++ b/infer/src/nullsafe/IDEnv.ml @@ -14,7 +14,17 @@ type t = Exp.t Ident.Hash.t Lazy.t let create_ proc_desc = let map = Ident.Hash.create 1 in - let do_instr _ = function Sil.Load {id; e} -> Ident.Hash.add map id e | _ -> () in + let do_instr _ = function + | Sil.Load {id; e} -> + Ident.Hash.add map id e + | Sil.Call ((res_ident, _), Exp.Const (Const.Cfun fname), [(Exp.Var src_ident, _); _], _, _) + (* [id] = __cast([ex]) when [ex] is a frontend temporary, try to unfold it further *) + when Procname.equal fname BuiltinDecl.__cast -> + Ident.Hash.find_opt map src_ident + |> Option.iter ~f:(fun ex -> Ident.Hash.add map res_ident ex) + | _ -> + () + in Procdesc.iter_instrs do_instr proc_desc ; map diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 70180c211..6f7df7693 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -717,31 +717,43 @@ let handle_assignment_in_condition_for_sil_prune idenv node pvar = None ) +let pp_normalized_cond fmt (_, exp) = Exp.pp fmt exp + let rec normalize_cond_for_sil_prune_rec idenv ~node ~original_node cond = - match cond with - | Exp.UnOp (Unop.LNot, c, top) -> - let node', c' = normalize_cond_for_sil_prune_rec idenv ~node ~original_node c in - (node', Exp.UnOp (Unop.LNot, c', top)) - | Exp.BinOp (bop, c1, c2) -> - let node', c1' = normalize_cond_for_sil_prune_rec idenv ~node ~original_node c1 in - let node'', c2' = normalize_cond_for_sil_prune_rec idenv ~node:node' ~original_node c2 in - (node'', Exp.BinOp (bop, c1', c2')) - | Exp.Var _ -> - let c' = IDEnv.expand_expr idenv cond in - if not (Exp.equal c' cond) then normalize_cond_for_sil_prune_rec idenv ~node ~original_node c' - else (node, c') - | Exp.Lvar pvar when Pvar.is_frontend_tmp pvar -> ( - match handle_assignment_in_condition_for_sil_prune idenv original_node pvar with - | None -> ( - match Decompile.find_program_variable_assignment node pvar with - | Some (node', id) -> - (node', Exp.Var id) - | None -> - (node, cond) ) - | Some e2 -> - (node, e2) ) - | c -> - (node, c) + L.d_with_indent ~name:"normalize_cond_for_sil_prune_rec" ~pp_result:pp_normalized_cond (fun () -> + L.d_printfln "cond=%a" Exp.pp cond ; + match cond with + | Exp.UnOp (Unop.LNot, c, top) -> + L.d_printfln "UnOp" ; + let node', c' = normalize_cond_for_sil_prune_rec idenv ~node ~original_node c in + (node', Exp.UnOp (Unop.LNot, c', top)) + | Exp.BinOp (bop, c1, c2) -> + L.d_printfln "BinOp" ; + let node', c1' = normalize_cond_for_sil_prune_rec idenv ~node ~original_node c1 in + let node'', c2' = normalize_cond_for_sil_prune_rec idenv ~node:node' ~original_node c2 in + L.d_printfln "c1=%a@\nc2=%a" Exp.pp c1 Exp.pp c2 ; + (node'', Exp.BinOp (bop, c1', c2')) + | Exp.Var _ -> + L.d_printfln "Var" ; + let c' = IDEnv.expand_expr idenv cond in + L.d_printfln "c'=%a" Exp.pp c' ; + if not (Exp.equal c' cond) then + normalize_cond_for_sil_prune_rec idenv ~node ~original_node c' + else (node, c') + | Exp.Lvar pvar when Pvar.is_frontend_tmp pvar -> ( + L.d_printfln "Lvar" ; + match handle_assignment_in_condition_for_sil_prune idenv original_node pvar with + | None -> ( + match Decompile.find_program_variable_assignment node pvar with + | Some (node', id) -> + (node', Exp.Var id) + | None -> + (node, cond) ) + | Some e2 -> + (node, e2) ) + | c -> + L.d_printfln "other" ; + (node, c) ) (* Normalize the condition by resolving temp variables. *) diff --git a/infer/tests/codetoanalyze/java/nullsafe/ReturnNotNullable.java b/infer/tests/codetoanalyze/java/nullsafe/ReturnNotNullable.java index 4a0e094d3..41baa7ac1 100644 --- a/infer/tests/codetoanalyze/java/nullsafe/ReturnNotNullable.java +++ b/infer/tests/codetoanalyze/java/nullsafe/ReturnNotNullable.java @@ -233,8 +233,7 @@ public class ReturnNotNullable { // 1. The argument is a generic, // 2. The type parameter is not {@code Object}. // Both are important to trigger the behaviour we're checking (indirection via typecast in CFG). - public List nullCheckGenericAssignmentResultAsNonnullOk_FP( - BlockingQueue queue) { + public List nullCheckGenericAssignmentResultAsNonnullOk(BlockingQueue queue) { final ArrayList records = new ArrayList<>(queue.size()); try { Runnable task; @@ -258,7 +257,7 @@ public class ReturnNotNullable { } } - public void chainedCallsWithAssignmentChecksOk_FP(@Nullable NullableGetter c1) { + public void chainedCallsWithAssignmentChecksOk(@Nullable NullableGetter c1) { NullableGetter c2, c3; if (c1 != null && (c2 = c1.get()) != null && (c3 = c2.get()) != null) { diff --git a/infer/tests/codetoanalyze/java/nullsafe/issues.exp b/infer/tests/codetoanalyze/java/nullsafe/issues.exp index 4dcaebcc9..38b4b00f3 100644 --- a/infer/tests/codetoanalyze/java/nullsafe/issues.exp +++ b/infer/tests/codetoanalyze/java/nullsafe/issues.exp @@ -301,10 +301,7 @@ codetoanalyze/java/nullsafe/PropagatesNullable.java, codetoanalyze.java.nullsafe codetoanalyze/java/nullsafe/PropagatesNullable.java, codetoanalyze.java.nullsafe.TestPropagatesNullable$TestSecondParameter.test(java.lang.String,java.lang.String):void, 7, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`nullable(...)` is nullable and is not locally checked for null when calling `length()`.] codetoanalyze/java/nullsafe/PropagatesNullable.java, codetoanalyze.java.nullsafe.TestPropagatesNullable$TestSecondParameter.test(java.lang.String,java.lang.String):void, 11, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`nullable(...)` is nullable and is not locally checked for null when calling `length()`.] codetoanalyze/java/nullsafe/PropagatesNullable.java, codetoanalyze.java.nullsafe.TestPropagatesNullable$TestSecondParameter.test(java.lang.String,java.lang.String):void, 15, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`nullable(...)` is nullable and is not locally checked for null when calling `length()`.] -codetoanalyze/java/nullsafe/ReturnNotNullable.java, Linters_dummy_method, 23, ERADICATE_META_CLASS_NEEDS_IMPROVEMENT, no_bucket, INFO, [], ReturnNotNullable, codetoanalyze.java.nullsafe, issues: 12, curr_mode: "Default" -codetoanalyze/java/nullsafe/ReturnNotNullable.java, codetoanalyze.java.nullsafe.ReturnNotNullable$AssignmentResultCheck.chainedCallsWithAssignmentChecksOk_FP(codetoanalyze.java.nullsafe.ReturnNotNullable$AssignmentResultCheck$NullableGetter):void, 3, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`c2` is nullable and is not locally checked for null when calling `get()`: call to get() at line 264.] -codetoanalyze/java/nullsafe/ReturnNotNullable.java, codetoanalyze.java.nullsafe.ReturnNotNullable$AssignmentResultCheck.chainedCallsWithAssignmentChecksOk_FP(codetoanalyze.java.nullsafe.ReturnNotNullable$AssignmentResultCheck$NullableGetter):void, 4, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`c3` is nullable and is not locally checked for null when calling `get()`: call to get() at line 264.] -codetoanalyze/java/nullsafe/ReturnNotNullable.java, codetoanalyze.java.nullsafe.ReturnNotNullable$AssignmentResultCheck.nullCheckGenericAssignmentResultAsNonnullOk_FP(java.util.concurrent.BlockingQueue):java.util.List, 7, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`task` is nullable and is not locally checked for null when calling `toString()`: call to BlockingQueue.poll(...) at line 242 (declared nullable in nullsafe/third-party-signatures/java.sig at line 3).] +codetoanalyze/java/nullsafe/ReturnNotNullable.java, Linters_dummy_method, 23, ERADICATE_META_CLASS_NEEDS_IMPROVEMENT, no_bucket, INFO, [], ReturnNotNullable, codetoanalyze.java.nullsafe, issues: 9, curr_mode: "Default" codetoanalyze/java/nullsafe/ReturnNotNullable.java, codetoanalyze.java.nullsafe.ReturnNotNullable$ConditionalAssignment.test(boolean):java.lang.Object, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [`test(...)`: return type is declared non-nullable but the method returns a nullable value: field f1 at line 203.] codetoanalyze/java/nullsafe/ReturnNotNullable.java, codetoanalyze.java.nullsafe.ReturnNotNullable.constantToNullableIsOverannotated():java.lang.String, 0, ERADICATE_RETURN_OVER_ANNOTATED, no_bucket, ADVICE, [Method `constantToNullableIsOverannotated()` is annotated with `@Nullable` but never returns null.] codetoanalyze/java/nullsafe/ReturnNotNullable.java, codetoanalyze.java.nullsafe.ReturnNotNullable.getResourceNullable(java.lang.Class,java.lang.String):java.net.URL, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [`getResourceNullable(...)`: return type is declared non-nullable but the method returns a nullable value: call to Class.getResource(...) at line 181 (nullable according to nullsafe internal models).]