Merge pull request #935 from goblint/issue_716

Read offsets separately in eval_rv_base for pointer dereference

src/analyses/base.ml

@@ -801,43 +801,48 @@ struct
         let b = Mem e, NoOffset in (* base pointer *)
         let t = Cilfacade.typeOfLval b in (* static type of base *)
         let p = eval_lv a gs st b in (* abstract base addresses *)
-        let v = (* abstract base value *)
+        (* pre VLA: *)
+        (* let cast_ok = function Addr a -> sizeOf t <= sizeOf (get_type_addr a) | _ -> false in *)
+        let cast_ok a =
           let open Addr in
-          (* pre VLA: *)
-          (* let cast_ok = function Addr a -> sizeOf t <= sizeOf (get_type_addr a) | _ -> false in *)
-          let cast_ok = function
-            | Addr (x, o) ->
-              begin
-                let at = get_type_addr (x, o) in
-                if M.tracing then M.tracel "evalint" "cast_ok %a %a %a\n" Addr.pretty (Addr (x, o)) CilType.Typ.pretty (Cil.unrollType x.vtype) CilType.Typ.pretty at;
-                if at = TVoid [] then (* HACK: cast from alloc variable is always fine *)
-                  true
-                else
-                  match Cil.getInteger (sizeOf t), Cil.getInteger (sizeOf at) with
-                  | Some i1, Some i2 -> Cilint.compare_cilint i1 i2 <= 0
-                  | _ ->
-                    if contains_vla t || contains_vla (get_type_addr (x, o)) then
-                      begin
-                        (* TODO: Is this ok? *)
-                        M.info ~category:Unsound "Casting involving a VLA is assumed to work";
-                        true
-                      end
-                    else
-                      false
-              end
-            | NullPtr | UnknownPtr -> true (* TODO: are these sound? *)
-            | _ -> false
+          match a with
+          | Addr (x, o) ->
+            begin
+              let at = get_type_addr (x, o) in
+              if M.tracing then M.tracel "evalint" "cast_ok %a %a %a\n" Addr.pretty (Addr (x, o)) CilType.Typ.pretty (Cil.unrollType x.vtype) CilType.Typ.pretty at;
+              if at = TVoid [] then (* HACK: cast from alloc variable is always fine *)
+                true
+              else
+                match Cil.getInteger (sizeOf t), Cil.getInteger (sizeOf at) with
+                | Some i1, Some i2 -> Cilint.compare_cilint i1 i2 <= 0
+                | _ ->
+                  if contains_vla t || contains_vla (get_type_addr (x, o)) then
+                    begin
+                      (* TODO: Is this ok? *)
+                      M.info ~category:Unsound "Casting involving a VLA is assumed to work";
+                      true
+                    end
+                  else
+                    false
+            end
+          | NullPtr | UnknownPtr -> true (* TODO: are these sound? *)
+          | _ -> false
+        in
+        (** Lookup value at base address [addr] with given offset [ofs]. *)
+        let lookup_with_offs addr =
+          let v = (* abstract base value *)
+            if cast_ok addr then
+              get ~top:(VD.top_value t) a gs st (AD.singleton addr) (Some exp)  (* downcasts are safe *)
+            else
+              VD.top () (* upcasts not! *)
           in
-          if AD.for_all cast_ok p then
-            get ~top:(VD.top_value t) a gs st p (Some exp)  (* downcasts are safe *)
-          else
-            VD.top () (* upcasts not! *)
+          let v' = VD.cast t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *)
+          if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!\n" VD.pretty v d_type t VD.pretty v';
+          let v' = VD.eval_offset a (fun x -> get a gs st x (Some exp)) v' (convert_offset a gs st ofs) (Some exp) None t in (* handle offset *)
+          let v' = do_offs v' ofs in (* handle blessed fields? *)
+          v'
         in
-        let v' = VD.cast t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *)
-        if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!\n" VD.pretty v d_type t VD.pretty v';
-        let v' = VD.eval_offset a (fun x -> get a gs st x (Some exp)) v' (convert_offset a gs st ofs) (Some exp) None t in (* handle offset *)
-        let v' = do_offs v' ofs in (* handle blessed fields? *)
-        v'
+        AD.fold (fun a acc -> VD.join acc (lookup_with_offs a)) p (VD.bot ())
       (* Binary operators *)
       (* Eq/Ne when both values are equal and casted to the same type *)
       | BinOp (op, (CastE (t1, e1) as c1), (CastE (t2, e2) as c2), typ) when typeSig t1 = typeSig t2 && (op = Eq || op = Ne) ->

src/cdomains/structDomain.ml

@@ -12,6 +12,7 @@ sig
   include Lattice.S
   val is_bot_value: t -> bool
   val is_top_value: t -> typ -> bool
+  val top_value: ?varAttr:attributes -> typ -> t
 end
 
 module type S =
@@ -49,7 +50,11 @@ struct
 
   let pretty () = M.pretty ()
   let replace s field value = M.add field value s
-  let get s field = M.find field s
+  let get s field =
+    match M.find_opt field s with
+    | Some v -> v
+    | None -> Val.top_value field.ftype
+
   let fold = M.fold
   let map = M.map
   let keys x = M.fold (fun k _ a -> k::a) x []

src/cdomains/structDomain.mli

@@ -7,6 +7,7 @@ sig
   include Lattice.S
   val is_bot_value: t -> bool
   val is_top_value: t -> typ -> bool
+  val top_value: ?varAttr:attributes -> typ -> t
 end
 
 module type S =

tests/regression/43-struct-domain/27-chrony-nameserv-sched-array.c

@@ -0,0 +1,233 @@
+// PARAM: --set ana.malloc.wrappers '["Malloc", "Realloc", "Malloc2", "Realloc2", "ARR_CreateInstance", "realloc_array", "ARR_GetNewElement"]' --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals
+// extracted from chrony
+#include <stdlib.h>
+#include <assert.h>
+#include <pthread.h>
+
+// memory.c
+
+void *
+Malloc(size_t size)
+{
+  void *r;
+
+  r = malloc(size);
+
+  return r;
+}
+
+void *
+Realloc(void *ptr, size_t size)
+{
+  void *r;
+
+  r = realloc(ptr, size);
+
+  return r;
+}
+
+static size_t
+get_array_size(size_t nmemb, size_t size)
+{
+  size_t array_size;
+
+  array_size = nmemb * size;
+
+  return array_size;
+}
+
+void *
+Realloc2(void *ptr, size_t nmemb, size_t size)
+{
+  return Realloc(ptr, get_array_size(nmemb, size));
+}
+
+#define MallocNew(T) ((T *) Malloc(sizeof(T)))
+#define MallocArray(T, n) ((T *) Malloc2(n, sizeof(T)))
+#define ReallocArray(T, n, x) ((T *) Realloc2((void *)(x), n, sizeof(T)))
+#define Free(x) free(x)
+
+// array.c
+
+struct ARR_Instance_Record {
+  void *data;
+  unsigned int elem_size;
+  unsigned int used;
+  unsigned int allocated;
+};
+
+typedef struct ARR_Instance_Record *ARR_Instance;
+
+ARR_Instance
+ARR_CreateInstance(unsigned int elem_size)
+{
+  ARR_Instance array;
+
+  assert(elem_size > 0);
+
+  array = MallocNew(struct ARR_Instance_Record);
+
+  array->data = NULL;
+  array->elem_size = elem_size;
+  array->used = 0;
+  array->allocated = 0;
+
+  return array;
+}
+
+void *
+ARR_GetElement(ARR_Instance array, unsigned int index)
+{
+  assert(index < array->used); // UNKNOWN
+  return (void *)((char *)array->data + (size_t)index * array->elem_size);
+}
+
+static void
+realloc_array(ARR_Instance array, unsigned int min_size)
+{
+  assert(min_size <= 2 * min_size); // UNKNOWN
+  if (array->allocated >= min_size && array->allocated <= 2 * min_size)
+    return;
+
+  if (array->allocated < min_size) {
+    while (array->allocated < min_size)
+      array->allocated = array->allocated ? 2 * array->allocated : 1;
+  } else {
+    array->allocated = min_size;
+  }
+
+  array->data = Realloc2(array->data, array->allocated, array->elem_size);
+}
+
+void *
+ARR_GetNewElement(ARR_Instance array)
+{
+  array->used++;
+  realloc_array(array, array->used);
+  return ARR_GetElement(array, array->used - 1);
+}
+
+unsigned int
+ARR_GetSize(ARR_Instance array)
+{
+  return array->used;
+}
+
+// sched.c
+
+typedef void* SCH_ArbitraryArgument;
+typedef void (*SCH_FileHandler)(SCH_ArbitraryArgument);
+
+typedef struct {
+  SCH_FileHandler       handler;
+  SCH_ArbitraryArgument arg;
+} FileHandlerEntry;
+
+static ARR_Instance file_handlers;
+
+void
+SCH_Initialise(void)
+{
+  file_handlers = ARR_CreateInstance(sizeof (FileHandlerEntry));
+}
+
+void
+SCH_AddFileHandler
+(SCH_FileHandler handler, SCH_ArbitraryArgument arg)
+{
+  int fd; // rand
+  FileHandlerEntry *ptr;
+
+  while (ARR_GetSize(file_handlers) <= fd) {
+    ptr = ARR_GetNewElement(file_handlers);
+    ptr->handler = NULL;
+    ptr->arg = NULL;
+  }
+
+  ptr = ARR_GetElement(file_handlers, fd);
+
+  /* Don't want to allow the same fd to register a handler more than
+     once without deleting a previous association - this suggests
+     a bug somewhere else in the program. */
+  assert(!ptr->handler); // UNKNOWN
+
+  ptr->handler = handler;
+  ptr->arg = arg;
+}
+
+static void
+dispatch_filehandlers()
+{
+  FileHandlerEntry *ptr;
+  int fd; // rand
+
+  ptr = (FileHandlerEntry *)ARR_GetElement(file_handlers, fd);
+  SCH_FileHandler stuff = *(ptr->handler);
+  if (ptr->handler)
+    (ptr->handler)(ptr->arg);
+}
+
+// nameserv_async.c
+
+typedef void (*DNS_NameResolveHandler)(void *anything);
+
+struct DNS_Async_Instance {
+  DNS_NameResolveHandler handler;
+  void *arg;
+  pthread_t thread;
+};
+
+static void *
+start_resolving(void *anything)
+{
+  struct DNS_Async_Instance *inst = (struct DNS_Async_Instance *)anything;
+
+  return NULL;
+}
+
+static void
+end_resolving(void *anything)
+{
+  struct DNS_Async_Instance *inst = (struct DNS_Async_Instance *)anything;
+
+  DNS_NameResolveHandler h = inst->handler;
+  (inst->handler)(inst->arg);
+
+  Free(inst);
+}
+
+void
+DNS_Name2IPAddressAsync(DNS_NameResolveHandler handler, void *anything)
+{
+  struct DNS_Async_Instance *inst;
+
+  inst = MallocNew(struct DNS_Async_Instance);
+  inst->handler = handler;
+  inst->arg = anything;
+
+  pthread_create(&inst->thread, NULL, start_resolving, inst);
+
+  SCH_AddFileHandler(end_resolving, inst);
+}
+
+// stub
+
+void foo(void *arg) {
+  assert(1); // reachable
+}
+
+void bar(void *arg) {
+  int *p = arg;
+  int y = *p;
+  assert(1); // reachable
+  assert(y); // TODO
+}
+
+int main() {
+  SCH_Initialise();
+  DNS_Name2IPAddressAsync(foo, NULL);
+  int x = 1;
+  DNS_Name2IPAddressAsync(bar, &x);
+  dispatch_filehandlers();
+  return 0;
+}