From b2ee1152fe27520dd708ad5665c271e230b381ed Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 4 Aug 2017 04:05:34 -0700 Subject: [PATCH] [prover] do destructive normalization to prove more Summary: In some cases we normalize expressions to check some facts about them. In these cases, trying to keep as much information as possible in the expression, such as the fact it comes from a `sizeof()` expression, is not needed. Doing destructive normalization allows us to replace `sizeof()` by its statically-known value. closes #706 Reviewed By: mbouaziz Differential Revision: D5536685 fbshipit-source-id: cc3d731 --- infer/src/backend/prop.ml | 15 +++++--- infer/src/backend/prop.mli | 10 +++--- infer/src/backend/prover.ml | 34 +++++++++++-------- infer/src/backend/symExec.ml | 2 +- infer/tests/codetoanalyze/c/errors/issues.exp | 1 + .../c/errors/sizeof/sizeof_706.c | 29 ++++++++++++++++ 6 files changed, 66 insertions(+), 25 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/errors/sizeof/sizeof_706.c diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index b7e60cadc..04ba0f721 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -685,7 +685,7 @@ module Normalize = struct let ( ++ ) = IntLit.add - let sym_eval tenv abs e = + let sym_eval ?(destructive= false) tenv abs e = let lookup = Tenv.lookup tenv in let rec eval (e: Exp.t) : Exp.t = (* L.d_str " ["; Sil.d_exp e; L.d_str"] "; *) @@ -699,6 +699,8 @@ module Normalize = struct Closure {c with captured_vars} | Const _ -> e + | Sizeof {nbytes= Some n} when destructive + -> Exp.Const (Const.Cint (IntLit.of_int n)) | Sizeof {typ= {desc= Tarray ({desc= Tint ik}, _, _)}; dynamic_length= Some l} when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang -> eval l @@ -1084,9 +1086,10 @@ module Normalize = struct (* L.d_str "sym_eval "; Sil.d_exp e; L.d_str" --> "; Sil.d_exp e'; L.d_ln (); *) e' - let exp_normalize tenv sub exp = + let exp_normalize ?destructive tenv sub exp = let exp' = Sil.exp_sub sub exp in - if !Config.abs_val >= 1 then sym_eval tenv true exp' else sym_eval tenv false exp' + let abstract_expressions = !Config.abs_val >= 1 in + sym_eval ?destructive tenv abstract_expressions exp' let texp_normalize tenv sub (exp: Exp.t) : Exp.t = match exp with @@ -1675,8 +1678,10 @@ end (* End of module Normalize *) -let exp_normalize_prop tenv prop exp = - Config.run_with_abs_val_equal_zero (Normalize.exp_normalize tenv (`Exp prop.sub)) exp +let exp_normalize_prop ?destructive tenv prop exp = + Config.run_with_abs_val_equal_zero + (Normalize.exp_normalize ?destructive tenv (`Exp prop.sub)) + exp let lexp_normalize_prop tenv p lexp = let root = Exp.root_of_lexp lexp in diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index f6c238612..ce8a73ad5 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -158,10 +158,12 @@ val atom_exp_le_const : Sil.atom -> (Exp.t * IntLit.t) option val atom_const_lt_exp : Sil.atom -> (IntLit.t * Exp.t) option (** If the atom is [n 'a t -> Exp.t -> Exp.t -(** Normalize [exp] using the pure part of [prop]. Later, we should - change this such that the normalization exposes offsets of [exp] - as much as possible. *) +val exp_normalize_prop : ?destructive:bool -> Tenv.t -> 'a t -> Exp.t -> Exp.t +(** Normalize [exp] using the pure part of [prop]. Later, we should change this such that the + normalization exposes offsets of [exp] as much as possible. + + If [destructive] is true then normalize more aggressively, which may lose some useful structure + or types. *) val exp_normalize_noabs : Tenv.t -> Sil.subst -> Exp.t -> Exp.t (** Normalize the expression without abstracting complex subexpressions *) diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index aed018db9..273bd6044 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -473,11 +473,11 @@ end = struct match (e1, e2) with | Exp.Const Const.Cint n1, Exp.Const Const.Cint n2 -> IntLit.leq n1 n2 - | ( Exp.BinOp - ( Binop.MinusA - , Exp.Sizeof {typ= t1; dynamic_length= None} - , Exp.Sizeof {typ= t2; dynamic_length= None} ) + | ( Exp.BinOp (Binop.MinusA, Exp.Sizeof {nbytes= Some nb1}, Exp.Sizeof {nbytes= Some nb2}) , Exp.Const Const.Cint n2 ) + -> (* [ sizeof(t1) - sizeof(t2) <= n2 ] *) + IntLit.(leq (sub (of_int nb1) (of_int nb2)) n2) + | Exp.BinOp (Binop.MinusA, Exp.Sizeof {typ= t1}, Exp.Sizeof {typ= t2}), Exp.Const Const.Cint n2 when IntLit.isminusone n2 && type_size_comparable t1 t2 -> (* [ sizeof(t1) - sizeof(t2) <= -1 ] *) check_type_size_lt t1 t2 @@ -550,6 +550,8 @@ end = struct match e1 with | Exp.Const Const.Cint n1 -> Some (n1 -- IntLit.one) + | Exp.Sizeof {nbytes= Some n1} + -> Some (IntLit.of_int n1 -- IntLit.one) | Exp.Sizeof _ -> Some IntLit.zero | _ @@ -597,9 +599,9 @@ end (* End of module Inequalities *) (** Check [prop |- e1=e2]. Result [false] means "don't know". *) -let check_equal tenv prop e1 e2 = - let n_e1 = Prop.exp_normalize_prop tenv prop e1 in - let n_e2 = Prop.exp_normalize_prop tenv prop e2 in +let check_equal tenv prop e1_0 e2_0 = + let n_e1 = Prop.exp_normalize_prop ~destructive:true tenv prop e1_0 in + let n_e2 = Prop.exp_normalize_prop ~destructive:true tenv prop e2_0 in let check_equal () = Exp.equal n_e1 n_e2 in let check_equal_const () = match (n_e1, n_e2) with @@ -651,8 +653,8 @@ let is_root tenv prop base_exp exp = f [] exp (** Get upper and lower bounds of an expression, if any *) -let get_bounds tenv prop _e = - let e_norm = Prop.exp_normalize_prop tenv prop _e in +let get_bounds tenv prop e0 = + let e_norm = Prop.exp_normalize_prop ~destructive:true tenv prop e0 in let e_root, off = match e_norm with | Exp.BinOp (Binop.PlusA, e, Exp.Const Const.Cint n1) @@ -671,8 +673,8 @@ let get_bounds tenv prop _e = (** Check whether [prop |- e1!=e2]. *) let check_disequal tenv prop e1 e2 = let spatial_part = prop.Prop.sigma in - let n_e1 = Prop.exp_normalize_prop tenv prop e1 in - let n_e2 = Prop.exp_normalize_prop tenv prop e2 in + let n_e1 = Prop.exp_normalize_prop ~destructive:true tenv prop e1 in + let n_e2 = Prop.exp_normalize_prop ~destructive:true tenv prop e2 in let rec check_expr_disequal ce1 ce2 = match (ce1, ce2) with | Exp.Const c1, Exp.Const c2 @@ -874,7 +876,7 @@ let check_le tenv prop e1 e2 = (** Check whether [prop |- allocated(e)]. *) let check_allocatedness tenv prop e = - let n_e = Prop.exp_normalize_prop tenv prop e in + let n_e = Prop.exp_normalize_prop ~destructive:true tenv prop e in let spatial_part = prop.Prop.sigma in let f = function | Sil.Hpointsto (base, _, _) @@ -915,7 +917,7 @@ let check_inconsistency_two_hpreds tenv prop = let prop' = Prop.normalize tenv (Prop.from_sigma (sigma_seen @ sigma_rest)) in let prop_new = Prop.conjoin_eq tenv e1 e2 prop' in let sigma_new = prop_new.Prop.sigma in - let e_new = Prop.exp_normalize_prop tenv prop_new e in + let e_new = Prop.exp_normalize_prop ~destructive:true tenv prop_new e in f e_new [] sigma_new else f e (hpred :: sigma_seen) sigma_rest | (Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, Exp.Const Const.Cint i, _, _) as hpred) :: sigma_rest @@ -926,7 +928,7 @@ let check_inconsistency_two_hpreds tenv prop = let prop' = Prop.normalize tenv (Prop.from_sigma (sigma_seen @ sigma_rest)) in let prop_new = Prop.conjoin_eq tenv e1 e3 prop' in let sigma_new = prop_new.Prop.sigma in - let e_new = Prop.exp_normalize_prop tenv prop_new e in + let e_new = Prop.exp_normalize_prop ~destructive:true tenv prop_new e in f e_new [] sigma_new else f e (hpred :: sigma_seen) sigma_rest in @@ -1319,7 +1321,9 @@ let exp_imply tenv calc_missing (subs: subst2) e1_in e2_in : subst2 = -> let occurs_check v e = (* check whether [v] occurs in normalized [e] *) if Sil.fav_mem (Sil.exp_fav e) v - && Sil.fav_mem (Sil.exp_fav (Prop.exp_normalize_prop tenv Prop.prop_emp e)) v + && Sil.fav_mem + (Sil.exp_fav (Prop.exp_normalize_prop ~destructive:true tenv Prop.prop_emp e)) + v then raise (IMPL_EXC ("occurs check", subs, EXC_FALSE_EXPS (e1, e2))) in if Ident.is_primed v2 then diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 45811a14c..2ee20ee4c 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -331,7 +331,7 @@ let prune_ineq tenv ~is_strict ~positive prop e1 e2 = Propset.singleton tenv prop_with_ineq let rec prune tenv ~positive condition prop = - match condition with + match Prop.exp_normalize_prop ~destructive:true tenv prop condition with | Exp.Var _ | Exp.Lvar _ -> prune_ne tenv ~positive condition Exp.zero prop | Exp.Const Const.Cint i when IntLit.iszero i diff --git a/infer/tests/codetoanalyze/c/errors/issues.exp b/infer/tests/codetoanalyze/c/errors/issues.exp index 706ed445d..a0c7b3c49 100644 --- a/infer/tests/codetoanalyze/c/errors/issues.exp +++ b/infer/tests/codetoanalyze/c/errors/issues.exp @@ -91,6 +91,7 @@ codetoanalyze/c/errors/null_dereference/short.c, l_error, 2, NULL_DEREFERENCE codetoanalyze/c/errors/null_dereference/short.c, m, 2, NULL_TEST_AFTER_DEREFERENCE codetoanalyze/c/errors/resource_leaks/leak.c, fileNotClosed, 5, RESOURCE_LEAK codetoanalyze/c/errors/resource_leaks/leak.c, socketNotClosed, 5, RESOURCE_LEAK +codetoanalyze/c/errors/sizeof/sizeof_706.c, sentinel_bad, 0, DIVIDE_BY_ZERO codetoanalyze/c/frontend/enumeration/other_enum.c, other_enum_test, 4, DIVIDE_BY_ZERO codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c, test_offsetof_expr, 3, DIVIDE_BY_ZERO codetoanalyze/c/frontend/offsetof_expr/offsetof_expr.c, test_offsetof_expr, 5, DIVIDE_BY_ZERO diff --git a/infer/tests/codetoanalyze/c/errors/sizeof/sizeof_706.c b/infer/tests/codetoanalyze/c/errors/sizeof/sizeof_706.c new file mode 100644 index 000000000..40d15debc --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/sizeof/sizeof_706.c @@ -0,0 +1,29 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +int sizeof_eval_good(void) { + int a = 4; + int b = sizeof(a); + char c[2]; + + if (a % 4) { + return a / 0; + } + if (b % sizeof(a)) { + return a / 0; + } + if (sizeof(c) > 2) { + return a / 0; + } + if ((sizeof(c) / sizeof(c[0])) != 2) { + return a / 0; + } + return 0; +} + +void sentinel_bad(void) { return 1 / 0; }