[Patch v6] coverity: Store the modelling file in the source tree.

[Patch v6] coverity: Store the modelling file in the source tree.

[Andrew Cooper]

Signed-off-by: Andrew Cooper <andrew.cooper3@citrix.com>
CC: Coverity Team <coverity@xenproject.org>

---
Changes since v5:
 * Teach Coverity about errx() and libxl_ctx_{,un}lock()
 * Move to misc/coverity/model.c
---
 misc/coverity/model.c |  131 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 131 insertions(+)
 create mode 100644 misc/coverity/model.c

diff --git a/misc/coverity/model.c b/misc/coverity/model.c
new file mode 100644
index 0000000..cae5a25
--- /dev/null
+++ b/misc/coverity/model.c
@@ -0,0 +1,131 @@
+/* Coverity Scan model
+ *
+ * This is a modelling file for Coverity Scan. Modelling helps to avoid false
+ * positives.
+ *
+ * - A model file can't import any header files.
+ * - Therefore only some built-in primitives like int, char and void are
+ *   available but not NULL etc.
+ * - Modelling doesn't need full structs and typedefs. Rudimentary structs
+ *   and similar types are sufficient.
+ * - An uninitialised local pointer is not an error. It signifies that the
+ *   variable could be either NULL or have some data.
+ *
+ * Coverity Scan doesn't pick up modifications automatically. The model file
+ * must be uploaded by an admin in the analysis.
+ *
+ * The Xen Coverity Scan modelling file used the cpython modelling file as a
+ * reference to get started (suggested by Coverty Scan themselves as a good
+ * example), but all content is Xen specific.
+ *
+ * Copyright (c) 2013-2014 Citrix Systems Ltd; All Right Reserved
+ *
+ * Based on:
+ *     http://hg.python.org/cpython/file/tip/Misc/coverity_model.c
+ * Copyright (c) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010,
+ * 2011, 2012, 2013 Python Software Foundation; All Rights Reserved
+ *
+ */
+
+/*
+ * Useful references:
+ *   https://scan.coverity.com/models
+ */
+
+/* Definitions */
+#define NULL (void *)0
+#define PAGE_SIZE 4096UL
+#define PAGE_MASK (~(PAGE_SIZE-1))
+
+#define assert(cond) /* empty */
+
+struct page_info {};
+struct pthread_mutex_t {};
+
+struct libxl__ctx
+{
+    struct pthread_mutex_t lock;
+};
+typedef struct libxl__ctx libxl_ctx;
+
+/*
+ * Xen malloc.  Behaves exactly like regular malloc(), except it also contains
+ * an alignment parameter.
+ *
+ * TODO: work out how to correctly model bad alignments as errors.
+ */
+void *_xmalloc(unsigned long size, unsigned long align)
+{
+    int has_memory;
+
+    __coverity_negative_sink__(size);
+    __coverity_negative_sink__(align);
+
+    if ( has_memory )
+        return __coverity_alloc__(size);
+    else
+        return NULL;
+}
+
+/*
+ * Xen free.  Frees a pointer allocated by _xmalloc().
+ */
+void xfree(void *va)
+{
+    __coverity_free__(va);
+}
+
+
+/*
+ * map_domain_page() takes an existing domain page and possibly maps it into
+ * the Xen pagetables, to allow for direct access.  Model this as a memory
+ * allocation of exactly 1 page.
+ *
+ * map_domain_page() never fails. (It will BUG() before returning NULL)
+ *
+ * TODO: work out how to correctly model the behaviour that this function will
+ * only ever return page aligned pointers.
+ */
+void *map_domain_page(unsigned long mfn)
+{
+    return __coverity_alloc__(PAGE_SIZE);
+}
+
+/*
+ * unmap_domain_page() will unmap a page.  Model it as a free().
+ */
+void unmap_domain_page(const void *va)
+{
+    __coverity_free__(va);
+}
+
+/*
+ * Coverity appears not to understand that errx() unconditionally exits.
+ */
+void errx(int, const char*, ...)
+{
+    __coverity_panic__();
+}
+
+/*
+ * Coverity doesn't appear to be certain that the libxl ctx->lock is recursive.
+ */
+void libxl__ctx_lock(libxl_ctx *ctx)
+{
+    __coverity_exclusive_lock_acquire__(&ctx->lock);
+}
+
+void libxl__ctx_unlock(libxl_ctx *ctx)
+{
+    __coverity_exclusive_lock_release__(&ctx->lock);
+}
+
+/*
+ * Local variables:
+ * mode: C
+ * c-file-style: "BSD"
+ * c-basic-offset: 4
+ * tab-width: 4
+ * indent-tabs-mode: nil
+ * End:
+ */
-- 
1.7.10.4

[Patch v7] coverity: Store the modelling file in the source tree.

[Andrew Cooper]

Signed-off-by: Andrew Cooper <andrew.cooper3@citrix.com>
CC: Coverity Team <coverity@xenproject.org>

---
Changes in v7:
 * Correctly state recursive locks rather than exclusive

Changes in v6:
 * Teach Coverity about errx() and libxl_ctx_{,un}lock()
 * Move to misc/coverity/model.c
---
 misc/coverity/model.c |  131 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 131 insertions(+)
 create mode 100644 misc/coverity/model.c

diff --git a/misc/coverity/model.c b/misc/coverity/model.c
new file mode 100644
index 0000000..fac2ecb
--- /dev/null
+++ b/misc/coverity/model.c
@@ -0,0 +1,131 @@
+/* Coverity Scan model
+ *
+ * This is a modelling file for Coverity Scan. Modelling helps to avoid false
+ * positives.
+ *
+ * - A model file can't import any header files.
+ * - Therefore only some built-in primitives like int, char and void are
+ *   available but not NULL etc.
+ * - Modelling doesn't need full structs and typedefs. Rudimentary structs
+ *   and similar types are sufficient.
+ * - An uninitialised local pointer is not an error. It signifies that the
+ *   variable could be either NULL or have some data.
+ *
+ * Coverity Scan doesn't pick up modifications automatically. The model file
+ * must be uploaded by an admin in the analysis.
+ *
+ * The Xen Coverity Scan modelling file used the cpython modelling file as a
+ * reference to get started (suggested by Coverty Scan themselves as a good
+ * example), but all content is Xen specific.
+ *
+ * Copyright (c) 2013-2014 Citrix Systems Ltd; All Right Reserved
+ *
+ * Based on:
+ *     http://hg.python.org/cpython/file/tip/Misc/coverity_model.c
+ * Copyright (c) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010,
+ * 2011, 2012, 2013 Python Software Foundation; All Rights Reserved
+ *
+ */
+
+/*
+ * Useful references:
+ *   https://scan.coverity.com/models
+ */
+
+/* Definitions */
+#define NULL (void *)0
+#define PAGE_SIZE 4096UL
+#define PAGE_MASK (~(PAGE_SIZE-1))
+
+#define assert(cond) /* empty */
+
+struct page_info {};
+struct pthread_mutex_t {};
+
+struct libxl__ctx
+{
+    struct pthread_mutex_t lock;
+};
+typedef struct libxl__ctx libxl_ctx;
+
+/*
+ * Xen malloc.  Behaves exactly like regular malloc(), except it also contains
+ * an alignment parameter.
+ *
+ * TODO: work out how to correctly model bad alignments as errors.
+ */
+void *_xmalloc(unsigned long size, unsigned long align)
+{
+    int has_memory;
+
+    __coverity_negative_sink__(size);
+    __coverity_negative_sink__(align);
+
+    if ( has_memory )
+        return __coverity_alloc__(size);
+    else
+        return NULL;
+}
+
+/*
+ * Xen free.  Frees a pointer allocated by _xmalloc().
+ */
+void xfree(void *va)
+{
+    __coverity_free__(va);
+}
+
+
+/*
+ * map_domain_page() takes an existing domain page and possibly maps it into
+ * the Xen pagetables, to allow for direct access.  Model this as a memory
+ * allocation of exactly 1 page.
+ *
+ * map_domain_page() never fails. (It will BUG() before returning NULL)
+ *
+ * TODO: work out how to correctly model the behaviour that this function will
+ * only ever return page aligned pointers.
+ */
+void *map_domain_page(unsigned long mfn)
+{
+    return __coverity_alloc__(PAGE_SIZE);
+}
+
+/*
+ * unmap_domain_page() will unmap a page.  Model it as a free().
+ */
+void unmap_domain_page(const void *va)
+{
+    __coverity_free__(va);
+}
+
+/*
+ * Coverity appears not to understand that errx() unconditionally exits.
+ */
+void errx(int, const char*, ...)
+{
+    __coverity_panic__();
+}
+
+/*
+ * Coverity doesn't appear to be certain that the libxl ctx->lock is recursive.
+ */
+void libxl__ctx_lock(libxl_ctx *ctx)
+{
+    __coverity_recursive_lock_acquire__(&ctx->lock);
+}
+
+void libxl__ctx_unlock(libxl_ctx *ctx)
+{
+    __coverity_recursive_lock_release__(&ctx->lock);
+}
+
+/*
+ * Local variables:
+ * mode: C
+ * c-file-style: "BSD"
+ * c-basic-offset: 4
+ * tab-width: 4
+ * indent-tabs-mode: nil
+ * End:
+ */
-- 
1.7.10.4

Re: [Patch v7] coverity: Store the modelling file in the source tree.

[Ian Campbell]

On Wed, 2014-02-19 at 17:00 +0000, Andrew Cooper wrote:
> Signed-off-by: Andrew Cooper <andrew.cooper3@citrix.com>
> CC: Coverity Team <coverity@xenproject.org>

I'm not sure whose umbrella this comes under but I'm going to argue that
the security team are effectively the maintainers. I've therefore acked
+ applied.

Thanks.