Fix unsound dereferencing of unknown pointer offset chain in DDVerify

src/analyses/base.ml

@@ -344,7 +344,7 @@ struct
    *  adding proper dependencies.
    *  For the exp argument it is always ok to put None. This means not using precise information about
    *  which part of an array is involved.  *)
-  let rec get ?(full=false) a (gs: glob_fun) (st: store) (addrs:address) (exp:exp option): value =
+  let rec get ?(top=VD.top ()) ?(full=false) a (gs: glob_fun) (st: store) (addrs:address) (exp:exp option): value =
     let at = AD.get_type addrs in
     let firstvar = if M.tracing then match AD.to_var_may addrs with [] -> "" | x :: _ -> x.vname else "" in
     if M.tracing then M.traceli "get" ~var:firstvar "Address: %a\nState: %a\n" AD.pretty addrs CPA.pretty st.cpa;
@@ -362,7 +362,7 @@ struct
       let f = function
         | Addr.Addr (x, o) -> f_addr (x, o)
         | Addr.NullPtr -> VD.bot () (* TODO: why bot? *)
-        | Addr.UnknownPtr -> VD.top ()
+        | Addr.UnknownPtr -> top (* top may be more precise than VD.top, e.g. for address sets, such that known addresses are kept for soundness *)
         | Addr.StrPtr _ -> `Int (ID.top_of IChar)
       in
       (* We form the collecting function by joining *)
@@ -720,10 +720,11 @@ struct
                   else
                     false
               end
+            | NullPtr | UnknownPtr -> true (* TODO: are these sound? *)
             | _ -> false
           in
           if AD.for_all cast_ok p then
-            get a gs st p (Some exp)  (* downcasts are safe *)
+            get ~top:(VD.top_value t) a gs st p (Some exp)  (* downcasts are safe *)
           else
             VD.top () (* upcasts not! *)
         in

tests/regression/02-base/74-pcwd-deref-unknown-fp.c

@@ -0,0 +1,70 @@
+// PARAM: --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.spawn
+// extracted from ddverify pcwd
+
+// header declarations
+
+struct file_operations {
+  void (*ioctl)();
+};
+
+struct miscdevice {
+  struct file_operations *fops;
+};
+
+struct cdev {
+  struct file_operations *ops;
+};
+
+// implementation stub
+
+struct ddv_cdev {
+  struct cdev *cdevp;
+};
+
+#define MAX_CDEV_SUPPORT 1
+
+struct cdev fixed_cdev[MAX_CDEV_SUPPORT];
+struct ddv_cdev cdev_registered[MAX_CDEV_SUPPORT];
+
+int cdev_add(struct cdev *p)
+{
+  cdev_registered[0].cdevp = p;
+  return 0;
+}
+
+int misc_register(struct miscdevice *misc) {
+  fixed_cdev[0].ops = misc->fops;
+  return cdev_add(&fixed_cdev[0]);
+}
+
+void call_cdev_functions()
+{
+  int cdev_no = 0;
+  if (cdev_registered[cdev_no].cdevp->ops->ioctl) {
+    (* cdev_registered[cdev_no].cdevp->ops->ioctl)();
+  }
+}
+
+// concrete program
+
+void pcwd_ioctl() {
+  assert(1); // reachable
+}
+
+static const struct file_operations pcwd_fops = {
+  .ioctl = pcwd_ioctl
+};
+
+static struct miscdevice pcwd_miscdev = {
+  .fops = &pcwd_fops
+};
+
+int main() {
+  misc_register(&pcwd_miscdev);
+
+  void (*fp)(struct ddv_cdev*); // unknown function pointer
+  fp(&cdev_registered); // invalidates argument!
+
+  call_cdev_functions();
+  return 0;
+}