From bd216f320566dab07756c8a2852e3dee43c07c19 Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Tue, 6 Dec 2016 03:02:13 -0800 Subject: [PATCH] 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 | 13 +++++ .../c/errors/arithmetic/test_sizeof.c | 51 +++++++++++++++++++ infer/tests/codetoanalyze/c/errors/issues.exp | 1 + 3 files changed, 65 insertions(+) create mode 100644 infer/tests/codetoanalyze/c/errors/arithmetic/test_sizeof.c diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 0e3d40c67..f245957c8 100644 --- a/infer/src/backend/prover.ml +++ b/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 -> diff --git a/infer/tests/codetoanalyze/c/errors/arithmetic/test_sizeof.c b/infer/tests/codetoanalyze/c/errors/arithmetic/test_sizeof.c new file mode 100644 index 000000000..8e8741d14 --- /dev/null +++ b/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 + +// 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); +} diff --git a/infer/tests/codetoanalyze/c/errors/issues.exp b/infer/tests/codetoanalyze/c/errors/issues.exp index 56156838b..60f209240 100644 --- a/infer/tests/codetoanalyze/c/errors/issues.exp +++ b/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