Remove duplicate binop handling from memOutOfBounds

src/analyses/memOutOfBounds.ml

@@ -116,19 +116,6 @@ struct
     | TPtr (t, _) -> Some t
     | _ -> None
 
-  let eval_ptr_offset_in_binop man exp ptr_contents_typ =
-    let eval_offset = man.ask (Queries.EvalInt exp) in
-    match eval_offset with
-    | `Lifted eo ->
-      let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in
-      let casted_eo = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) eo in (* TODO: proper castkind *)
-      begin
-        try `Lifted (ID.mul casted_eo ptr_contents_typ_size_in_bytes)
-        with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
-      end
-    | `Top -> `Top
-    | `Bot -> `Bot
-
   let rec offs_to_idx typ offs =
     match offs with
     | `NoOffset -> intdom_of_int 0
@@ -222,14 +209,7 @@ struct
                 Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs
             end
         end;
-        begin match e with
-          | Lval (Var v, _) as lval_exp -> check_no_binop_deref man lval_exp
-          | BinOp (binop, e1, e2, t) when binop = PlusPI || binop = MinusPI || binop = IndexPI ->
-            check_binop_exp man binop e1 e2 t;
-            check_exp_for_oob_access man ~is_implicitly_derefed e1;
-            check_exp_for_oob_access man ~is_implicitly_derefed e2
-          | _ -> check_exp_for_oob_access man ~is_implicitly_derefed e
-        end
+        check_no_binop_deref man e
 
   and check_no_binop_deref man lval_exp =
     let behavior = Undefined MemoryOutOfBoundsAccess in
@@ -293,72 +273,6 @@ struct
     | StartOf lval
     | AddrOf lval -> check_lval_for_oob_access man ~is_implicitly_derefed lval
 
-  and check_binop_exp man binop e1 e2 t =
-    let binopexp = BinOp (binop, e1, e2, t) in
-    let behavior = Undefined MemoryOutOfBoundsAccess in
-    let cwe_number = 823 in
-    match binop with
-    | PlusPI
-    | IndexPI
-    | MinusPI ->
-      let ptr_type = typeOf e1 in
-      let ptr_contents_type = get_ptr_deref_type ptr_type in
-      begin match ptr_contents_type with
-        | Some t ->
-          let offset_size = eval_ptr_offset_in_binop man e2 t in
-          let* addr = man.ask (Queries.MayPointTo e1) in
-          let ptr_size = get_addr_size man addr in
-          let addr_offs = get_addr_offset t addr in
-          (* Make sure to add the address offset to the binop offset *)
-          let offset_size_with_addr_size = match offset_size with
-            | `Lifted os ->
-              let casted_os = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) os in (* TODO: proper castkind *)
-              let casted_ao = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) addr_offs in (* TODO: proper castkind *)
-              begin
-                try `Lifted (ID.add casted_os casted_ao)
-                with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
-              end
-            | `Top -> `Top
-            | `Bot -> `Bot
-          in
-          begin match ptr_size, offset_size_with_addr_size with
-            | `Top, _ ->
-              set_mem_safety_flag InvalidDeref;
-              M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp;
-              Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp
-            | _, `Top ->
-              set_mem_safety_flag InvalidDeref;
-              M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp;
-              Checks.warn Checks.Category.InvalidMemoryAccess "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp
-            | `Bot, _ ->
-              set_mem_safety_flag InvalidDeref;
-              M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp;
-              Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp
-            | _, `Bot ->
-              set_mem_safety_flag InvalidDeref;
-              M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp;
-              Checks.warn Checks.Category.InvalidMemoryAccess "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp
-            | `Lifted ps, `Lifted o ->
-              let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *)
-              let casted_o = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) o in (* TODO: proper castkind *)
-              begin match check_offset_bounds casted_ps casted_o with
-                | Some true, _
-                | _, Some true ->
-                  set_mem_safety_flag InvalidDeref;
-                  M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o;
-                  Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o
-                | Some false, Some false ->
-                  Checks.safe Checks.Category.InvalidMemoryAccess
-                | _ ->
-                  set_mem_safety_flag InvalidDeref;
-                  M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o;
-                  Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o
-              end
-          end
-        | _ -> M.error "Binary expression %a doesn't have a pointer" d_exp binopexp
-      end
-    | _ -> ()
-
   (* For memset() and memcpy() *)
   let check_count man fun_name ptr n =
     let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in

tests/regression/74-invalid_deref/01-oob-heap-simple.t

@@ -1,7 +1,7 @@
   $ goblint --set ana.activated[+] memOutOfBounds --enable ana.int.interval 01-oob-heap-simple.c 2>&1 | tee default-output.txt
   [Warning] The memOutOfBounds analysis enables cil.addNestedScopeAttr.
-  [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is 5 (in bytes). It is offset by 10 (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22)
-  [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (5) with offset (⊤). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21)
+  [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 5 (in bytes). It is offset by 10 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22)
+  [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (5) (in bytes) with offset by (⊤) (in bytes). Memory out-of-bounds access might occur (01-oob-heap-simple.c:11:5-11:21)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 8
     dead: 0
@@ -11,9 +11,9 @@
 
   $ diff default-output.txt full-output.txt
   2,3c2,3
-  < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is 5 (in bytes). It is offset by 10 (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22)
-  < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (5) with offset (⊤). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21)
+  < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 5 (in bytes). It is offset by 10 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22)
+  < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (5) (in bytes) with offset by (⊤) (in bytes). Memory out-of-bounds access might occur (01-oob-heap-simple.c:11:5-11:21)
   ---
-  > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is (5,[5,5]) (in bytes). It is offset by (10,[10,10]) (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22)
-  > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size ((5,[5,5])) with offset ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21)
+  > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is (5,[5,5]) (in bytes). It is offset by (10,[10,10]) (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22)
+  > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer ((5,[5,5])) (in bytes) with offset by ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])) (in bytes). Memory out-of-bounds access might occur (01-oob-heap-simple.c:11:5-11:21)
   [1]

tests/regression/74-invalid_deref/40-oob-deref-cast.c

@@ -0,0 +1,9 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+#include <stdlib.h>
+
+int main() {
+  char* s = malloc(10);
+  s += 10; // NOWARN
+  unsigned char ch = (*(unsigned char *) s); // WARN!
+  return 0;
+}

tests/regression/74-invalid_deref/41-oob-coreutils-seq-incr.c

@@ -0,0 +1,37 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
+#include <stdlib.h>
+#include <string.h>
+
+// This is some wild C code from coreutils seq.
+static void
+incr (char **s0, size_t *s_len)
+{
+  char *s = *s0; // NOWARN
+  char *endp = s + *s_len - 1; // NOWARN
+  do
+    {
+      if ((*endp)++ < '9') // TODO NOWARN
+        return;
+      *endp-- = '0'; // TODO NOWARN
+    }
+  while (endp >= s);
+  *--(*s0) = '1'; // WARN!
+  ++*s_len; // NOWARN
+}
+
+int main() {
+  char* s = malloc(10);
+  memset(s, '0', 10); // NOWARN
+
+  char* s2 = s + 9;
+  size_t len = 1;
+  incr(&s2, &len); // everything in this should be in bounds
+
+  memset(s, '9', 10); // NOWARN
+
+  s2 = s;
+  len = 10;
+  incr(&s2, &len); // something in this could be out of bounds
+
+  return 0;
+}