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

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

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;
 

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
+    let type_opt_is_unsigned = function
-      | Exp.Sizeof (Typ.Tint ik, _, _) -> Typ.ikind_is_unsigned ik
+      | 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.Eexp (e, _), t ->
-      | Sil.Estruct (fsel, _) ->
+          if type_opt_is_unsigned t then add_lt_minus1_e e
-          IList.iter (fun (_, se) -> strexp_extract se) fsel
+      | Sil.Estruct (fsel, _), t ->
-      | Sil.Earray (len, isel, _) ->
+          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 = [] }

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) =

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

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
 

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

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' =

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

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