Merge pull request #6693 from tautschnig/feature/mmap

C library: add models of mmap, munmap

Author: tautschnig

regression/cbmc-library/mmap-01/main.c

@@ -0,0 +1,38 @@
+#include <sys/mman.h>
+
+#include <fcntl.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <unistd.h>
+
+void *mapmem(off_t offset, size_t length)
+{
+  int fd;
+  uint8_t *mem, *tmp;
+  const int prot = PROT_READ | PROT_WRITE;
+  const int flags = MAP_SHARED;
+
+  mem = NULL;
+  fd = open("/dev/mem", O_RDWR | O_CLOEXEC);
+  if(fd == -1)
+    goto out;
+
+  tmp = mmap(NULL, length, prot, flags, fd, offset);
+  close(fd);
+  if(tmp == MAP_FAILED)
+    goto out;
+  mem = tmp;
+out:
+  return mem;
+}
+
+int main()
+{
+  unsigned long int target = 0xffffffL;
+  uint8_t *mem;
+  mem = mapmem(target, 1024L);
+  printf("got address %p from target %p\n", mem, (void *)target);
+  mem[0] = 42;
+  munmap(mem, 1024L);
+  return 0;
+}

regression/cbmc-library/mmap-01/test.desc

@@ -0,0 +1,8 @@
+CORE unix
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/mman.c

@@ -0,0 +1,133 @@
+/* FUNCTION: mmap */
+
+#ifndef _WIN32
+
+#  ifndef __CPROVER_SYS_MMAN_H_INCLUDED
+#    include <sys/mman.h>
+#    define __CPROVER_SYS_MMAN_H_INCLUDED
+#  endif
+
+#  ifndef MAP_FIXED
+#    define MAP_FIXED 0
+#  endif
+
+#  ifndef MAP_ANONYMOUS
+#    define MAP_ANONYMOUS 0
+#  endif
+
+#  ifndef MAP_UNINITIALIZED
+#    define MAP_UNINITIALIZED 0
+#  endif
+
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+
+void *mmap(
+  void *addr,
+  __CPROVER_size_t length,
+  int prot,
+  int flags,
+  int fd,
+  off_t offset)
+{
+  (void)prot;
+  (void)fd;
+  (void)offset;
+
+  if(
+    addr == 0 ||
+    (__VERIFIER_nondet___CPROVER_bool() && (flags & MAP_FIXED) == 0))
+  {
+    if(flags & MAP_ANONYMOUS && (flags & MAP_UNINITIALIZED) == 0)
+      return __CPROVER_allocate(length, 1);
+    else
+      return __CPROVER_allocate(length, 0);
+  }
+  else
+  {
+    __CPROVER_allocated_memory((__CPROVER_size_t)addr, length);
+    return addr;
+  }
+}
+
+#endif
+
+/* FUNCTION: _mmap */
+
+#ifndef _WIN32
+
+#  ifndef __CPROVER_SYS_MMAN_H_INCLUDED
+#    include <sys/mman.h>
+#    define __CPROVER_SYS_MMAN_H_INCLUDED
+#  endif
+
+#  ifndef MAP_FIXED
+#    define MAP_FIXED 0
+#  endif
+
+#  ifndef MAP_ANONYMOUS
+#    define MAP_ANONYMOUS 0
+#  endif
+
+#  ifndef MAP_UNINITIALIZED
+#    define MAP_UNINITIALIZED 0
+#  endif
+
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+
+void *_mmap(
+  void *addr,
+  __CPROVER_size_t length,
+  int prot,
+  int flags,
+  int fd,
+  off_t offset)
+{
+  (void)prot;
+  (void)fd;
+  (void)offset;
+
+  if(
+    addr == 0 ||
+    (__VERIFIER_nondet___CPROVER_bool() && (flags & MAP_FIXED) == 0))
+  {
+    if(flags & MAP_ANONYMOUS && (flags & MAP_UNINITIALIZED) == 0)
+      return __CPROVER_allocate(length, 1);
+    else
+      return __CPROVER_allocate(length, 0);
+  }
+  else
+  {
+    __CPROVER_allocated_memory((__CPROVER_size_t)addr, length);
+    return addr;
+  }
+}
+
+#endif
+
+/* FUNCTION: munmap */
+
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+
+int munmap(void *addr, __CPROVER_size_t length)
+{
+  (void)length;
+
+  if(__VERIFIER_nondet___CPROVER_bool())
+    __CPROVER_deallocated = addr;
+
+  return 0;
+}
+
+/* FUNCTION: _munmap */
+
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+
+int _munmap(void *addr, __CPROVER_size_t length)
+{
+  (void)length;
+
+  if(__VERIFIER_nondet___CPROVER_bool())
+    __CPROVER_deallocated = addr;
+
+  return 0;
+}