[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

@@ -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

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<e] return [n,e] *)
 
-val exp_normalize_prop : 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. *)
+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 *)

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

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

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

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; }