From 26a6594b90c2d8777a128d53b9f49194c059655b Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 22 Aug 2016 06:24:42 -0700 Subject: [PATCH] detect unsigned values inside structured expressions Summary: Infer doesn't go looking into field values when looking for unsigned expressions, which could cause some unintended reports. Reviewed By: sblackshear Differential Revision: D3724232 fbshipit-source-id: 9c4cd97 --- infer/src/IR/Typ.re | 15 ++++ infer/src/IR/Typ.rei | 4 + infer/src/backend/prover.ml | 27 ++++-- infer/src/backend/rearrange.ml | 6 +- infer/src/checkers/annotations.ml | 11 --- infer/src/checkers/annotations.mli | 4 - infer/src/checkers/checkers.ml | 2 +- infer/src/eradicate/eradicateChecks.ml | 2 +- .../c/errors/arithmetic/unsigned_values.c | 85 +++++++++++++++++++ .../c/infer/UnsignedIsNonnegativeTest.java | 51 +++++++++++ 10 files changed, 179 insertions(+), 28 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/errors/arithmetic/unsigned_values.c create mode 100644 infer/tests/endtoend/c/infer/UnsignedIsNonnegativeTest.java diff --git a/infer/src/IR/Typ.re b/infer/src/IR/Typ.re index f80add569..1ebe49e4e 100644 --- a/infer/src/IR/Typ.re +++ b/infer/src/IR/Typ.re @@ -526,6 +526,21 @@ let struct_typ_fld default_opt f => { | _ => def () }; +let get_field_type_and_annotation fn => + fun + | Tptr (Tstruct struct_typ) _ + | Tstruct struct_typ => + try { + let (_, t, a) = + IList.find + (fun (f, _, _) => Ident.fieldname_equal f fn) + (struct_typ.instance_fields @ struct_typ.static_fields); + Some (t, a) + } { + | Not_found => None + } + | _ => None; + /** if [struct_typ] is a class, return its class kind (Java, CPP, or Obj-C) */ let struct_typ_get_class_kind struct_typ => diff --git a/infer/src/IR/Typ.rei b/infer/src/IR/Typ.rei index 165a94012..a38f0a57c 100644 --- a/infer/src/IR/Typ.rei +++ b/infer/src/IR/Typ.rei @@ -228,6 +228,10 @@ let get_extensible_array_element_typ: t => option t; let struct_typ_fld: option t => Ident.fieldname => t => t; +/** Return the type of the field [fn] and its annotation, None if [typ] has no field named [fn] */ +let get_field_type_and_annotation: Ident.fieldname => t => option (t, item_annotation); + + /** if [struct_typ] is a class, return its class kind (Java, CPP, or Obj-C) */ let struct_typ_get_class_kind: struct_typ => option Csu.class_kind; diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index bf5803cba..9440ff6c7 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -384,25 +384,36 @@ end = struct let lts = ref [] in let add_lt_minus1_e e = lts := (Exp.minus_one, e)::!lts in - let texp_is_unsigned = function - | Exp.Sizeof (Typ.Tint ik, _, _) -> Typ.ikind_is_unsigned ik + let type_opt_is_unsigned = function + | Some Typ.Tint ik -> Typ.ikind_is_unsigned ik | _ -> false in + let type_of_texp = function + | Exp.Sizeof (t, _, _) -> Some t + | _ -> None in + let texp_is_unsigned texp = type_opt_is_unsigned @@ type_of_texp texp in let strexp_lt_minus1 = function | Sil.Eexp (e, _) -> add_lt_minus1_e e | _ -> () in let rec strexp_extract = function - | Sil.Eexp _ -> () - | Sil.Estruct (fsel, _) -> - IList.iter (fun (_, se) -> strexp_extract se) fsel - | Sil.Earray (len, isel, _) -> + | Sil.Eexp (e, _), t -> + if type_opt_is_unsigned t then add_lt_minus1_e e + | Sil.Estruct (fsel, _), t -> + let get_field_type f = + Option.map_default + (fun t' -> Option.map fst @@ Typ.get_field_type_and_annotation f t') None t in + IList.iter (fun (f, se) -> strexp_extract (se, get_field_type f)) fsel + | Sil.Earray (len, isel, _), t -> + let elt_t = match t with + | Some Typ.Tarray (t, _) -> Some t + | _ -> None in add_lt_minus1_e len; IList.iter (fun (idx, se) -> add_lt_minus1_e idx; - strexp_extract se) isel in + strexp_extract (se, elt_t)) isel in let hpred_extract = function | Sil.Hpointsto(_, se, texp) -> if texp_is_unsigned texp then strexp_lt_minus1 se; - strexp_extract se + strexp_extract (se, type_of_texp texp) | Sil.Hlseg _ | Sil.Hdllseg _ -> () in IList.iter hpred_extract sigma; saturate { leqs = !leqs; lts = !lts; neqs = [] } diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index c3760160c..19fb0ee1c 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -655,7 +655,7 @@ let add_guarded_by_constraints prop lexp pdesc = IList.find_map_opt annot_extract_guarded_by_str item_annot in (* if [fld] is annotated with @GuardedBy("mLock"), return mLock *) let get_guarded_by_fld_str fld typ = - match Annotations.get_field_type_and_annotation fld typ with + match Typ.get_field_type_and_annotation fld typ with | Some (_, item_annot) -> begin match extract_guarded_by_str item_annot with @@ -683,7 +683,7 @@ let add_guarded_by_constraints prop lexp pdesc = try let fld, strexp = IList.find f flds in begin - match Annotations.get_field_type_and_annotation fld typ with + match Typ.get_field_type_and_annotation fld typ with | Some (fld_typ, _) -> Some (strexp, fld_typ) | None -> None end @@ -1210,7 +1210,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = is_nullable || Pvar.is_local pvar | Sil.Hpointsto (_, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) -> let fld_is_nullable fld = - match Annotations.get_field_type_and_annotation fld typ with + match Typ.get_field_type_and_annotation fld typ with | Some (_, annot) -> Annotations.ia_is_nullable annot | _ -> false in let is_strexp_pt_by_nullable_fld (fld, strexp) = diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index 7fb2aff84..cb1f2ee5a 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -36,17 +36,6 @@ let visibleForTesting = "com.google.common.annotations.VisibleForTesting" let suppressLint = "android.annotation.SuppressLint" -let get_field_type_and_annotation fn = function - | Typ.Tptr (Typ.Tstruct struct_typ, _) - | Typ.Tstruct struct_typ -> - (try - let (_, t, a) = IList.find (fun (f, _, _) -> - Ident.fieldname_equal f fn) - (struct_typ.Typ.instance_fields @ struct_typ.Typ.static_fields) in - Some (t, a) - with Not_found -> None) - | _ -> None - (** Return the annotations on the declaring class of [pname]. Only works for Java *) let get_declaring_class_annotations pname tenv = match Tenv.proc_extract_declaring_class_typ tenv pname with diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index 3dccba77c..eaa0103cf 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -53,10 +53,6 @@ val equal : annotated_signature -> annotated_signature -> bool (** Get a method signature with annotations from a proc_attributes. *) val get_annotated_signature : ProcAttributes.t -> annotated_signature -(** Return the type of the field [fn] and its annotation, None if [typ] has no field named [fn] *) -val get_field_type_and_annotation : - Ident.fieldname -> Typ.t -> (Typ.t * Typ.item_annotation) option - (** Return the annotations on the declaring class of [java_pname]. *) val get_declaring_class_annotations : Procname.java -> Tenv.t -> Typ.item_annotation option diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index 56c8b76c0..f27fa676a 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -112,7 +112,7 @@ module ST = struct let is_field_suppressed = match field_name, PatternMatch.get_this_type proc_attributes with | Some field_name, Some t -> begin - match (Annotations.get_field_type_and_annotation field_name t) with + match (Typ.get_field_type_and_annotation field_name t) with | Some (_, ia) -> Annotations.ia_has_annotation_with ia annotation_matches | None -> false end diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml index 4e9c01409..569895bbb 100644 --- a/infer/src/eradicate/eradicateChecks.ml +++ b/infer/src/eradicate/eradicateChecks.ml @@ -40,7 +40,7 @@ let check_library_calls = false let get_field_annotation fn typ = - match Annotations.get_field_type_and_annotation fn typ with + match Typ.get_field_type_and_annotation fn typ with | None -> None | Some (t, ia) -> let ia' = diff --git a/infer/tests/codetoanalyze/c/errors/arithmetic/unsigned_values.c b/infer/tests/codetoanalyze/c/errors/arithmetic/unsigned_values.c new file mode 100644 index 000000000..8c49ed18c --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/arithmetic/unsigned_values.c @@ -0,0 +1,85 @@ +/* + * 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. + */ + +// integers + +unsigned int returnUnsigned(); +void nonnegative_int() { + unsigned int x = returnUnsigned(); + if (x < 0) { + int y = x / 0; // shouldn't report + } +} + +int returnSigned(); +void signed_int() { + int x = returnSigned(); + if (x < 0) { + int y = 1 / 0; // should report + } +} + +// pointers to integers + +unsigned int* returnUnsignedPointer(); +void nonnegative_int_ptr() { + unsigned int* x = returnUnsignedPointer(); + if (*x < 0) { + int y = 1 / 0; // shouldn't report + } +} + +int* returnSignedPointer(); +void signed_int_ptr() { + int* x = returnSigned(); + if (*x < 0) { + int y = 1 / 0; // should report + } +} + +// struct with integer fields + +struct foo { + unsigned int unsigned_int; + int signed_int; +}; + +struct foo* returnFoo(); + +void nonnegative_field() { + struct foo* x = returnFoo(); + if (x->unsigned_int < 0) { + int y = 1 / 0; // shouldn't report + } +} + +void signed_field() { + struct foo* x = returnFoo(); + if (x->signed_int < 0) { + int y = 1 / 0; // should report + } +} + +// array of integers + +unsigned int* returnUnsignedArray(); +int nonnegative_array() { + unsigned int* a = returnUnsignedArray(); + if (a[0] < 0) { + int y = 1 / 0; // shouldn't report + } +} + +int* returnSignedArray(); +int signed_array() { + int* a = returnSignedArray(); + if (a[0] < 0) { + int y = 1 / 0; // should report + } +} diff --git a/infer/tests/endtoend/c/infer/UnsignedIsNonnegativeTest.java b/infer/tests/endtoend/c/infer/UnsignedIsNonnegativeTest.java new file mode 100644 index 000000000..a7a85960e --- /dev/null +++ b/infer/tests/endtoend/c/infer/UnsignedIsNonnegativeTest.java @@ -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. + */ + +package endtoend.c.infer; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; + +import org.junit.BeforeClass; +import org.junit.Test; + +import java.io.IOException; + +import utils.InferException; +import utils.InferResults; + +public class UnsignedIsNonnegativeTest { + + public static final String SOURCE_FILE = "arithmetic/unsigned_values.c"; + + public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO"; + + private static InferResults inferResults; + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferResults = InferResults.loadCInferResults(DivideByZeroTest.class, SOURCE_FILE); + } + + @Test + public void whenInferRunsOnDivideByZeroThenDivideByZeroIsFound() + throws InterruptedException, IOException, InferException { + String[] procedures = {"signed_int", "signed_int_ptr", "signed_field", "signed_array"}; + assertThat( + "Results should contain divide by zero error", + inferResults, + containsExactly( + DIVIDE_BY_ZERO, + SOURCE_FILE, + procedures + ) + ); + } + +}