From c9a2dcf7b16f7da631844815c89f434b4ce46e9f Mon Sep 17 00:00:00 2001 From: Jia Chen Date: Tue, 25 Jul 2017 10:31:25 -0700 Subject: [PATCH] Added constant-folding support for shifting Reviewed By: jeremydubreil Differential Revision: D5485475 fbshipit-source-id: 424a88a --- infer/src/IR/IntLit.ml | 18 ++++++++ infer/src/IR/IntLit.mli | 9 ++++ infer/src/backend/prop.ml | 28 ++++++++++++- .../codetoanalyze/c/biabduction/Makefile | 2 +- .../codetoanalyze/c/biabduction/issues.exp | 4 ++ .../tests/codetoanalyze/c/biabduction/shift.c | 41 +++++++++++++++++++ 6 files changed, 99 insertions(+), 3 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/biabduction/shift.c diff --git a/infer/src/IR/IntLit.ml b/infer/src/IR/IntLit.ml index ab1576b37..85d316344 100644 --- a/infer/src/IR/IntLit.ml +++ b/infer/src/IR/IntLit.ml @@ -103,6 +103,24 @@ let lognot i = lift1 Int64.bit_not i let sub i1 i2 = add i1 (neg i2) +let shift_left (unsigned1, i1, ptr1) (_, i2, _) = + match Int64.to_int i2 with + | None + -> failwithf "Shifting failed with operand %a" Int64.pp i2 + | Some i2 + -> if i2 < 0 || i2 >= 64 then failwithf "Oversized shift: %d" i2 ; + let res = Int64.shift_left i1 i2 in + (unsigned1, res, ptr1) + +let shift_right (unsigned1, i1, ptr1) (_, i2, _) = + match Int64.to_int i2 with + | None + -> failwithf "Shifting failed with operand %a" Int64.pp i2 + | Some i2 + -> if i2 < 0 || i2 >= 64 then failwithf "Oversized shift: %d" i2 ; + let res = Int64.shift_right i1 i2 in + (unsigned1, res, ptr1) + let pp f (unsigned, n, ptr) = if ptr && Int64.equal n 0L then F.fprintf f "null" else if unsigned then F.fprintf f "%Lu" n diff --git a/infer/src/IR/IntLit.mli b/infer/src/IR/IntLit.mli index d56b83041..f310edad1 100644 --- a/infer/src/IR/IntLit.mli +++ b/infer/src/IR/IntLit.mli @@ -78,6 +78,15 @@ val pp : F.formatter -> t -> unit val rem : t -> t -> t +val shift_left : t -> t -> t + +(* shift_right performs arithmetic shift, for the following reasons: *) +(* In C++, whether right shift is logical or arithmetical is implementation defined. + * Usually an arithmetic shift is implemented. *) +(* In Java, the current frontend refuses to translate logical right shift. *) + +val shift_right : t -> t -> t + val sub : t -> t -> t val to_int : t -> int diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 67258bffc..7d34a6417 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -992,9 +992,33 @@ module Normalize = struct | _ -> if abs then Exp.get_undefined false else BinOp (Mod, e1', e2') ) | BinOp (Shiftlt, e1, e2) - -> if abs then Exp.get_undefined false else BinOp (Shiftlt, eval e1, eval e2) + -> ( + if abs then Exp.get_undefined false + else + match (e1, e2) with + | Const Cint n, Const Cint m + -> Exp.int (IntLit.shift_left n m) + | _, Const Cint m when IntLit.iszero m + -> eval e1 + | _, Const Cint m when IntLit.isone m + -> eval (Exp.BinOp (PlusA, e1, e1)) + | Const Cint m, _ when IntLit.iszero m + -> e1 + | _ + -> BinOp (Shiftlt, eval e1, eval e2) ) | BinOp (Shiftrt, e1, e2) - -> if abs then Exp.get_undefined false else BinOp (Shiftrt, eval e1, eval e2) + -> ( + if abs then Exp.get_undefined false + else + match (e1, e2) with + | Const Cint n, Const Cint m + -> Exp.int (IntLit.shift_right n m) + | _, Const Cint m when IntLit.iszero m + -> eval e1 + | Const Cint m, _ when IntLit.iszero m + -> e1 + | _ + -> BinOp (Shiftrt, eval e1, eval e2) ) | BinOp (BAnd, e1, e2) -> ( let e1' = eval e1 in diff --git a/infer/tests/codetoanalyze/c/biabduction/Makefile b/infer/tests/codetoanalyze/c/biabduction/Makefile index cb42c7093..3207826df 100644 --- a/infer/tests/codetoanalyze/c/biabduction/Makefile +++ b/infer/tests/codetoanalyze/c/biabduction/Makefile @@ -9,7 +9,7 @@ TESTS_DIR = ../../.. ANALYZER = checkers CLANG_OPTIONS = -c -INFER_OPTIONS = --biabduction --project-root $(TESTS_DIR) +INFER_OPTIONS = --biabduction --debug-exceptions --project-root $(TESTS_DIR) INFERPRINT_OPTIONS = --issues-tests diff --git a/infer/tests/codetoanalyze/c/biabduction/issues.exp b/infer/tests/codetoanalyze/c/biabduction/issues.exp index 923495a13..d1496bdba 100644 --- a/infer/tests/codetoanalyze/c/biabduction/issues.exp +++ b/infer/tests/codetoanalyze/c/biabduction/issues.exp @@ -1,3 +1,7 @@ +codetoanalyze/c/biabduction/abduce.c, FN_set_ptr_param_array_get_null_bad, 3, PRECONDITION_NOT_MET, [start of procedure FN_set_ptr_param_array_get_null_bad()] +codetoanalyze/c/biabduction/example.c, bar, 2, DIVIDE_BY_ZERO, [start of procedure bar()] codetoanalyze/c/biabduction/example.c, foo, 2, NULL_DEREFERENCE, [start of procedure foo()] codetoanalyze/c/biabduction/example.c, global_addr_alias_bad, 3, NULL_DEREFERENCE, [start of procedure global_addr_alias_bad(),Condition is true] codetoanalyze/c/biabduction/example.c, local_addr_noalias_bad, 4, NULL_DEREFERENCE, [start of procedure local_addr_noalias_bad(),Condition is true] +codetoanalyze/c/biabduction/shift.c, return_null_deref1_bad, 2, NULL_DEREFERENCE, [start of procedure return_null_deref1_bad(),start of procedure return_depends_on_lshift(),Condition is true,return from a call to return_depends_on_lshift] +codetoanalyze/c/biabduction/shift.c, return_null_deref2_bad, 2, NULL_DEREFERENCE, [start of procedure return_null_deref2_bad(),start of procedure return_depends_on_rshift(),Condition is true,return from a call to return_depends_on_rshift] diff --git a/infer/tests/codetoanalyze/c/biabduction/shift.c b/infer/tests/codetoanalyze/c/biabduction/shift.c new file mode 100644 index 000000000..3b1bb512c --- /dev/null +++ b/infer/tests/codetoanalyze/c/biabduction/shift.c @@ -0,0 +1,41 @@ +/* + * 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* return_depends_on_lshift(int x, int* p) { + if (x < (1 << 7)) + return 0; + else + return p; +} + +int return_nonnull_deref1_ok() { + int y = 0; + return *return_depends_on_lshift(1000, &y); +} + +int return_null_deref1_bad() { + int y = 0; + return *return_depends_on_lshift(0, &y); +} + +int* return_depends_on_rshift(int x, int* p) { + if (x < (4 >> 2)) + return 0; + else + return p; +} + +int return_nonnull_deref2_ok() { + int y = 0; + return *return_depends_on_rshift(2, &y); +} + +int return_null_deref2_bad() { + int y = 0; + return *return_depends_on_rshift(0, &y); +}