From 857eae7c6b89b5b6cd9c3ecab842cf89f1c6ef2c Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 11 Apr 2017 12:17:47 -0700 Subject: [PATCH] [build] address warnings 52 and 57 Summary: OCaml 4.04.0 new warnings raised a few valid points! Fixing warning 57 in two ways: - best way: introduce an auxiliary function to avoid code duplication - not-so-best way: introduce code duplication. I did that when the branches body are small. Typically the number of bound variables in the pattern is high, so an auxiliary function would need to take many arguments and the whole thing will not be readable (we'd still duplicate the arguments we pass to the function for instance). Reviewed By: jberdine Differential Revision: D4851006 fbshipit-source-id: fbf1867 --- infer/src/backend/dom.ml | 16 ++- infer/src/backend/prop.ml | 28 +++-- infer/src/backend/prover.ml | 16 ++- infer/src/backend/rearrange.ml | 2 +- infer/src/backend/symExec.ml | 4 + infer/src/base/Config.ml | 2 +- infer/src/clang/Capture.re | 15 ++- infer/src/eradicate/typeCheck.ml | 187 ++++++++++++++++--------------- 8 files changed, 152 insertions(+), 118 deletions(-) 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) *)