diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 44bc91f49..c3ce080b6 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -710,7 +710,13 @@ end = struct else begin match atom_in with - | Sil.Aneq((Exp.Var id as e), e') | Sil.Aneq(e', (Exp.Var id as e)) + | Sil.Aneq((Exp.Var id as e), e') + when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) -> + (* e' cannot also be a normal id according to the guard so we can consider the two cases + separately (this case and the next) *) + build_other_atoms (fun e0 -> Prop.mk_neq tenv e0 e') side e + + | Sil.Aneq(e', (Exp.Var id as e)) when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) -> build_other_atoms (fun e0 -> Prop.mk_neq tenv e0 e') side e @@ -722,7 +728,13 @@ end = struct when not (Ident.is_normal id) && List.for_all ~f:exp_contains_only_normal_ids es -> build_other_atoms (fun e0 -> Prop.mk_npred tenv a (e0 :: es)) side e - | Sil.Aeq((Exp.Var id as e), e') | Sil.Aeq(e', (Exp.Var id as e)) + | Sil.Aeq((Exp.Var id as e), e') + when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) -> + (* e' cannot also be a normal id according to the guard so we can consider the two cases + separately (this case and the next) *) + build_other_atoms (fun e0 -> Prop.mk_eq tenv e0 e') side e + + | Sil.Aeq(e', (Exp.Var id as e)) when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) -> build_other_atoms (fun e0 -> Prop.mk_eq tenv e0 e') side e diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index c82d17693..ecdc067c4 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1377,21 +1377,25 @@ module Normalize = struct into a strexp of the given type *) let hpred' = mk_ptsto_exp tenv Fld_init (root, size, None) inst in replace_hpred hpred' - | (Earray (BinOp (Mult, Sizeof (t, None, st1), x), esel, inst) - | Earray (BinOp (Mult, x, Sizeof (t, None, st1)), esel, inst)), - Sizeof (Tarray (elt, _) as arr, _, _) - when Typ.equal t elt -> + | Earray (BinOp (Mult, Sizeof (t, None, st1), x), esel, inst), + Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt -> let len = Some x in - let hpred' = - mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in + let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in replace_hpred (replace_array_contents hpred' esel) - | ( Earray (BinOp (Mult, Sizeof (t, Some len, st1), x), esel, inst) - | Earray (BinOp (Mult, x, Sizeof (t, Some len, st1)), esel, inst)), - Sizeof (Tarray (elt, _) as arr, _, _) - when Typ.equal t elt -> + | Earray (BinOp (Mult, x, Sizeof (t, None, st1)), esel, inst), + Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt -> + let len = Some x in + let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in + replace_hpred (replace_array_contents hpred' esel) + | Earray (BinOp (Mult, Sizeof (t, Some len, st1), x), esel, inst), + Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt -> + let len = Some (Exp.BinOp(Mult, x, len)) in + let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in + replace_hpred (replace_array_contents hpred' esel) + | Earray (BinOp (Mult, x, Sizeof (t, Some len, st1)), esel, inst), + Sizeof (Tarray (elt, _) as arr, _, _) when Typ.equal t elt -> let len = Some (Exp.BinOp(Mult, x, len)) in - let hpred' = - mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in + let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof (arr, len, st1), None) inst in replace_hpred (replace_array_contents hpred' esel) | _ -> Hpointsto (normalized_root, normalized_cnt, normalized_te) diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 5acf9319e..566956c69 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1183,11 +1183,17 @@ let exp_imply tenv calc_missing subs e1_in e2_in : subst2 = (fst subs, sub2') else raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2)))) - | e1, Exp.BinOp (Binop.PlusA, Exp.Var v2, e2) - | e1, Exp.BinOp (Binop.PlusA, e2, Exp.Var v2) + | e1, Exp.BinOp (Binop.PlusA, (Exp.Var v2 as e2), e2') when Ident.is_primed v2 || Ident.is_footprint v2 -> - let e' = Exp.BinOp (Binop.MinusA, e1, e2) in - do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') (Exp.Var v2) + (* here e2' could also be a variable that we could try to substitute (as in the next match + case), but we ignore that to avoid backtracking *) + let e' = Exp.BinOp (Binop.MinusA, e1, e2') in + do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2 + | e1, Exp.BinOp (Binop.PlusA, e2, (Exp.Var v2 as e2')) + when Ident.is_primed v2 || Ident.is_footprint v2 -> + (* symmetric of above case *) + let e' = Exp.BinOp (Binop.MinusA, e1, e2') in + do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2 | Exp.Var _, e2 -> if calc_missing then let () = ProverState.add_missing_pi (Sil.Aeq (e1_in, e2_in)) in @@ -1219,6 +1225,8 @@ let exp_imply tenv calc_missing subs e1_in e2_in : subst2 = | Exp.Sizeof (t1, Some d1, st1), Exp.Sizeof (t2, Some d2, st2) when Typ.equal t1 t2 && Exp.equal d1 d2 && Subtype.equal_modulo_flag st1 st2 -> subs | e', Exp.Const (Const.Cint n) + when IntLit.iszero n && check_disequal tenv Prop.prop_emp e' Exp.zero -> + raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2)))) | Exp.Const (Const.Cint n), e' when IntLit.iszero n && check_disequal tenv Prop.prop_emp e' Exp.zero -> raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2)))) diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 6cc3de71b..45a3cfbe4 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -762,7 +762,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc = None in List.find_map - ~f:(function + ~f:(function [@warning "-57"] (* FIXME: silenced warning may be legit *) | Sil.Hpointsto ((Const (Cclass clazz) as lhs_exp), _, Exp.Sizeof (typ, _, _)) | Sil.Hpointsto (_, Sil.Eexp (Const (Cclass clazz) as lhs_exp, _), Exp.Sizeof (typ, _, _)) when guarded_by_str_is_class guarded_by_str0 (Ident.name_to_string clazz) -> diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 1e62f4af8..6548cee09 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -323,12 +323,16 @@ let rec prune tenv ~positive condition prop = | Exp.UnOp _ -> assert false | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) + when IntLit.iszero i && not (IntLit.isnull i) -> + prune tenv ~positive:(not positive) e prop | Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), e) when IntLit.iszero i && not (IntLit.isnull i) -> prune tenv ~positive:(not positive) e prop | Exp.BinOp (Binop.Eq, e1, e2) -> prune_ne tenv ~positive:(not positive) e1 e2 prop | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) + when IntLit.iszero i && not (IntLit.isnull i) -> + prune tenv ~positive e prop | Exp.BinOp (Binop.Ne, Exp.Const (Const.Cint i), e) when IntLit.iszero i && not (IntLit.isnull i) -> prune tenv ~positive e prop diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index cf9d2ff9c..d8a1d9509 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -318,7 +318,7 @@ let ncpu = try Utils.with_process_in "getconf _NPROCESSORS_ONLN 2>/dev/null" - (fun chan -> Scanf.fscanf chan "%d" (fun n -> n)) + (fun chan -> Scanf.bscanf (Scanf.Scanning.from_channel chan) "%d" (fun n -> n)) |> fst with _ -> 1 diff --git a/infer/src/clang/Capture.re b/infer/src/clang/Capture.re index 4b4a2e0da..d71e9aa54 100644 --- a/infer/src/clang/Capture.re +++ b/infer/src/clang/Capture.re @@ -17,11 +17,16 @@ let debug_mode = Config.debug_mode || Config.frontend_stats || Config.frontend_d let buffer_len = 262143; let catch_biniou_buffer_errors f x => - try (f x) { - | Invalid_argument "Bi_inbuf.refill_from_channel" => - Logging.err "WARNING: biniou buffer too short, skipping the file@\n"; - assert false - }; + ( + try (f x) { + /* suppress warning: allow this one case because we're just reraising the error with another + error message so it doesn't really matter if this eventually fails */ + | Invalid_argument "Bi_inbuf.refill_from_channel" => + Logging.err "WARNING: biniou buffer too short, skipping the file@\n"; + assert false + } + ) + [@warning "-52"]; /* This function reads the json file in fname, validates it, and encoded in the AST data structure defined in Clang_ast_t. */ diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 70f64583e..81ff96091 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -701,18 +701,18 @@ let typecheck_instr res_typestate := pvar_apply loc (handle_pvar ann b) !res_typestate pvar in let handle_negated_condition cond_node = - let do_instr = function - | Sil.Prune (Exp.BinOp (Binop.Eq, _cond_e, Exp.Const (Const.Cint i)), _, _, _) - | Sil.Prune (Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), _cond_e), _, _, _) - when IntLit.iszero i -> - let cond_e = Idenv.expand_expr_temps idenv cond_node _cond_e in - begin - match convert_complex_exp_to_pvar cond_node false cond_e typestate' loc with - | Exp.Lvar pvar', _ -> - set_flag pvar' AnnotatedSignature.Nullable false - | _ -> () - end - | _ -> () in + let do_instr = (function + | Sil.Prune (Exp.BinOp (Binop.Eq, _cond_e, Exp.Const (Const.Cint i)), _, _, _) + | Sil.Prune (Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), _cond_e), _, _, _) + when IntLit.iszero i -> + let cond_e = Idenv.expand_expr_temps idenv cond_node _cond_e in + begin + match convert_complex_exp_to_pvar cond_node false cond_e typestate' loc with + | Exp.Lvar pvar', _ -> + set_flag pvar' AnnotatedSignature.Nullable false + | _ -> () + end + | _ -> ()) [@warning "-57"] (* FIXME: silenced warning may be legit *) in List.iter ~f:do_instr (Procdesc.Node.get_instrs cond_node) in let handle_optional_isPresent node' e = match convert_complex_exp_to_pvar node' false e typestate' loc with @@ -1028,91 +1028,92 @@ let typecheck_instr pvar_apply loc handle_pvar typestate2 pvar | _ -> typestate2 in - match c with - | Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), e) - | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> - typecheck_expr_for_errors typestate e loc; - let typestate1, e1, from_call = match from_is_true_on_null e with - | Some e1 -> - typestate, e1, EradicateChecks.From_is_true_on_null - | None -> - typestate, e, EradicateChecks.From_condition in - let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in - let (typ, ta, _) = - typecheck_expr_simple typestate2 e' Typ.Tvoid TypeOrigin.ONone loc in + begin match c with + | Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), e) + | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> + typecheck_expr_for_errors typestate e loc; + let typestate1, e1, from_call = match from_is_true_on_null e with + | Some e1 -> + typestate, e1, EradicateChecks.From_is_true_on_null + | None -> + typestate, e, EradicateChecks.From_condition in + let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in + let (typ, ta, _) = + typecheck_expr_simple typestate2 e' Typ.Tvoid TypeOrigin.ONone loc in - if checks.eradicate then - EradicateChecks.check_zero tenv - find_canonical_duplicate curr_pdesc - node' e' typ - ta true_branch EradicateChecks.From_condition - idenv linereader loc instr_ref; - begin - match from_call with - | EradicateChecks.From_is_true_on_null -> - (* if f returns true on null, then false branch implies != null *) - if TypeAnnotation.get_value AnnotatedSignature.Nullable ta - then set_flag e' AnnotatedSignature.Nullable false typestate2 - else typestate2 - | _ -> - typestate2 - end + if checks.eradicate then + EradicateChecks.check_zero tenv + find_canonical_duplicate curr_pdesc + node' e' typ + ta true_branch EradicateChecks.From_condition + idenv linereader loc instr_ref; + begin + match from_call with + | EradicateChecks.From_is_true_on_null -> + (* if f returns true on null, then false branch implies != null *) + if TypeAnnotation.get_value AnnotatedSignature.Nullable ta + then set_flag e' AnnotatedSignature.Nullable false typestate2 + else typestate2 + | _ -> + typestate2 + end - | Exp.BinOp (Binop.Ne, Exp.Const (Const.Cint i), e) - | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> - typecheck_expr_for_errors typestate e loc; - let typestate1, e1, from_call = match from_instanceof e with - | Some e1 -> (* (e1 instanceof C) implies (e1 != null) *) - typestate, e1, EradicateChecks.From_instanceof - | None -> - begin - match from_optional_isPresent e with - | Some e1 -> - typestate, e1, EradicateChecks.From_optional_isPresent - | None -> - begin - match from_is_false_on_null e with - | Some e1 -> - typestate, e1, EradicateChecks.From_is_false_on_null - | None -> - begin - match from_containsKey e with - | Some _ when ComplexExpressions.functions_idempotent () -> - handle_containsKey e - | _ -> - typestate, e, EradicateChecks.From_condition - end - end - end in - let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in - let (typ, ta, _) = - typecheck_expr_simple typestate2 e' Typ.Tvoid TypeOrigin.ONone loc in + | Exp.BinOp (Binop.Ne, Exp.Const (Const.Cint i), e) + | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> + typecheck_expr_for_errors typestate e loc; + let typestate1, e1, from_call = match from_instanceof e with + | Some e1 -> (* (e1 instanceof C) implies (e1 != null) *) + typestate, e1, EradicateChecks.From_instanceof + | None -> + begin + match from_optional_isPresent e with + | Some e1 -> + typestate, e1, EradicateChecks.From_optional_isPresent + | None -> + begin + match from_is_false_on_null e with + | Some e1 -> + typestate, e1, EradicateChecks.From_is_false_on_null + | None -> + begin + match from_containsKey e with + | Some _ when ComplexExpressions.functions_idempotent () -> + handle_containsKey e + | _ -> + typestate, e, EradicateChecks.From_condition + end + end + end in + let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in + let (typ, ta, _) = + typecheck_expr_simple typestate2 e' Typ.Tvoid TypeOrigin.ONone loc in - if checks.eradicate then - EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc - node e' typ ta true_branch from_call idenv linereader loc instr_ref; - begin - match from_call with - | EradicateChecks.From_optional_isPresent -> - if not (TypeAnnotation.get_value AnnotatedSignature.Present ta) - then set_flag e' AnnotatedSignature.Present true typestate2 - else typestate2 - | EradicateChecks.From_is_true_on_null -> - typestate2 - | EradicateChecks.From_condition - | EradicateChecks.From_containsKey - | EradicateChecks.From_instanceof - | EradicateChecks.From_is_false_on_null -> - if TypeAnnotation.get_value AnnotatedSignature.Nullable ta then - set_flag e' AnnotatedSignature.Nullable false typestate2 - else typestate2 - end + if checks.eradicate then + EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc + node e' typ ta true_branch from_call idenv linereader loc instr_ref; + begin + match from_call with + | EradicateChecks.From_optional_isPresent -> + if not (TypeAnnotation.get_value AnnotatedSignature.Present ta) + then set_flag e' AnnotatedSignature.Present true typestate2 + else typestate2 + | EradicateChecks.From_is_true_on_null -> + typestate2 + | EradicateChecks.From_condition + | EradicateChecks.From_containsKey + | EradicateChecks.From_instanceof + | EradicateChecks.From_is_false_on_null -> + if TypeAnnotation.get_value AnnotatedSignature.Nullable ta then + set_flag e' AnnotatedSignature.Nullable false typestate2 + else typestate2 + end - | Exp.UnOp (Unop.LNot, (Exp.BinOp (Binop.Eq, e1, e2)), _) -> - check_condition node' (Exp.BinOp (Binop.Ne, e1, e2)) - | Exp.UnOp (Unop.LNot, (Exp.BinOp (Binop.Ne, e1, e2)), _) -> - check_condition node' (Exp.BinOp (Binop.Eq, e1, e2)) - | _ -> typestate in + | Exp.UnOp (Unop.LNot, (Exp.BinOp (Binop.Eq, e1, e2)), _) -> + check_condition node' (Exp.BinOp (Binop.Ne, e1, e2)) + | Exp.UnOp (Unop.LNot, (Exp.BinOp (Binop.Ne, e1, e2)), _) -> + check_condition node' (Exp.BinOp (Binop.Eq, e1, e2)) + | _ -> typestate + end [@warning "-57"] (* FIXME: silenced warning may be legit *) in (* Handle assigment fron a temp pvar in a condition. This recognizes the handling of temp variables in ((x = ...) != null) *)