Fixed problem with evaluation of sizeof which would give false positive

Summary:
When calling function g_realloc(gpointer mem,gsize n_bytes) one of the spec considers the case
whereby n_bytes is  zero. In that case g_realloc would return null.

If we call with sizeof(int), infer would compare sizeof(int) with zero. But the prover would fail to
understand that sizeof(int) != 0.
This diff fix this. We try to convert expression to constant when they can be converted (eg in case of sizeof).
The method currently make a partial set of conversion. This could be extended.

Reviewed By: jberdine

Differential Revision: D4166944

fbshipit-source-id: 3ec4fd7

infer/src/backend/prover.ml

@@ -625,6 +625,11 @@ let check_disequal tenv prop e1 e2 =
         if IntLit.iszero d then not (Const.equal c1 c2) else Const.equal c1 c2
     | Exp.Lindex(Exp.Const c1, Exp.Const d1), Exp.Lindex (Exp.Const c2, Exp.Const d2) ->
         Const.equal c1 c2 && not (Const.equal d1 d2)
+    | Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21)
+    | Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult, e21, Sizeof _)
+    | Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21), Exp.Const (Const.Cint n)
+    | Exp.BinOp (Binop.Mult, e21, Exp.Sizeof _), Exp.Const (Const.Cint n) ->
+        IntLit.iszero n && not (Exp.is_zero e21)
     | _, _ -> false in
   let ineq = lazy (Inequalities.from_prop tenv prop) in
   let check_pi_implies_disequal e1 e2 =
@@ -1203,6 +1208,14 @@ let exp_imply tenv calc_missing subs e1_in e2_in : subst2 =
         do_imply subs (Exp.Var v1) (Exp.BinOp (Binop.MinusA, e2, e1))
     | Exp.BinOp (Binop.PlusPI, Exp.Lvar pv1, e1), e2 ->
         do_imply subs (Exp.Lvar pv1) (Exp.BinOp (Binop.MinusA, e2, e1))
+    | Exp.Sizeof (t1, None, st1), Exp.Sizeof (t2, None, st2)
+      when Typ.equal t1 t2 && Subtype.equal_modulo_flag st1 st2 -> subs
+    | 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)
+    | 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))))
     | e1, Exp.Const _ ->
         raise (IMPL_EXC ("lhs not constant", subs, (EXC_FALSE_EXPS (e1, e2))))
     | Exp.Lfield(e1, fd1, _), Exp.Lfield(e2, fd2, _) when fd1 == fd2 ->

infer/tests/codetoanalyze/c/errors/arithmetic/test_sizeof.c

@@ -0,0 +1,51 @@
+/*
+ * Copyright (c) 2016 - 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.
+ */
+
+#include <stddef.h>
+
+// builtin: return the size of arr
+extern size_t __get_array_length(const void* arr);
+
+// builtin: change the size of the array to size
+extern void __set_array_length(void* ptr, size_t size);
+
+void* my_realloc(void* ptr, size_t size) {
+  if (size == 0) { // return NULL and free ptr unless it is NULL
+    if (ptr)
+      free(ptr);
+    return NULL;
+  }
+  int old_size;
+  old_size = __get_array_length(ptr); // force ptr to be an array
+  int can_enlarge; // nondeterministically choose whether the current block can
+  // be enlarged
+  if (can_enlarge) {
+    __set_array_length(ptr, size); // enlarge the block
+    return ptr;
+  }
+  int* newblock = (int*)malloc(size);
+  if (newblock) {
+    free(ptr);
+    return newblock;
+  } else
+    exit(0); // assume that new allocation does not fail
+}
+
+void foo(int* p) {
+  p = my_realloc(p, 10 * sizeof(int));
+  p[0] = 42;
+  free(p);
+}
+
+int main() {
+
+  int* p;
+  p = xmalloc(sizeof(int));
+  foo(p);
+}

infer/tests/codetoanalyze/c/errors/issues.exp

@@ -1,6 +1,7 @@
 codetoanalyze/c/errors/arithmetic/array_out_of_bounds.c, bound_error, 2, ARRAY_OUT_OF_BOUNDS_L1
 codetoanalyze/c/errors/arithmetic/array_out_of_bounds.c, bound_error_nested, 2, ARRAY_OUT_OF_BOUNDS_L1
 codetoanalyze/c/errors/arithmetic/divide_by_zero.c, arith_divide_by_zero, 3, DIVIDE_BY_ZERO
+codetoanalyze/c/errors/arithmetic/test_sizeof.c, my_realloc, 10, UNINITIALIZED_VALUE
 codetoanalyze/c/errors/arithmetic/unsigned_values.c, signed_array, 3, DIVIDE_BY_ZERO
 codetoanalyze/c/errors/arithmetic/unsigned_values.c, signed_field, 3, DIVIDE_BY_ZERO
 codetoanalyze/c/errors/arithmetic/unsigned_values.c, signed_int, 3, DIVIDE_BY_ZERO