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

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

[Andrew Cooper]

Signed-off-by: Andrew Cooper <andrew.cooper3@citrix.com>
CC: Keir Fraser <keir@xen.org>
CC: Jan Beulich <JBeulich@suse.com>
CC: Tim Deegan <tim@xen.org>
CC: Ian Campbell <Ian.Campbell@citrix.com>
CC: Ian Jackson <Ian.Jackson@eu.citrix.com>
---
 misc/coverity_model.c |   70 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 70 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..2588adb
--- /dev/null
+++ b/misc/coverity_model.c
@@ -0,0 +1,70 @@
+/* Coverity Scan model
+ *
+ * This is a modeling file for Coverity Scan. Modeling 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 wchar_t, NULL etc.
+ * - Modeling doesn't need full structs and typedefs. Rudimentary structs
+ *   and similar types are sufficient.
+ * - An uninitialized 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.
+ */
+
+/* Definitions */
+#define NULL (void *)0
+#define PAGE_SIZE 4096UL
+#define PAGE_MASK (~(PAGE_SIZE-1))
+
+#define assert(cond) /* empty */
+#define page_to_mfn(p) (unsigned long)(p)
+
+struct page_info {};
+
+/*
+ * 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), and
+ * will only ever return page aligned addresses.
+ */
+void *map_domain_page(unsigned long mfn)
+{
+    void *p = __coverity_alloc__(PAGE_SIZE);
+
+    assert(p != NULL);
+    assert((p & ~PAGE_MASK) == 0);
+
+    return p;
+}
+
+void *__map_domain_page(struct page_info *page)
+{
+    return map_domain_page(page_to_mfn(page));
+}
+
+/*
+ * unmap_domain_page() will correctly unmap the page, given any virtual
+ * address inside the page.
+ */
+void unmap_domain_page(const void *va)
+{
+    const void *v = (const void*)((unsigned long)va & PAGE_MASK);
+
+    __coverity_free__(v);
+}
+
+/*
+ * 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] coverity: Store the modelling file in the source tree.

[Tim Deegan]

At 15:29 +0000 on 04 Dec (1386167363), Andrew Cooper wrote:
> Signed-off-by: Andrew Cooper <andrew.cooper3@citrix.com>
> CC: Keir Fraser <keir@xen.org>
> CC: Jan Beulich <JBeulich@suse.com>
> CC: Tim Deegan <tim@xen.org>
> CC: Ian Campbell <Ian.Campbell@citrix.com>
> CC: Ian Jackson <Ian.Jackson@eu.citrix.com>
> ---
>  misc/coverity_model.c |   70 +++++++++++++++++++++++++++++++++++++++++++++++++
>  1 file changed, 70 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..2588adb
> --- /dev/null
> +++ b/misc/coverity_model.c
> @@ -0,0 +1,70 @@
> +/* Coverity Scan model
> + *
> + * This is a modeling file for Coverity Scan. Modeling 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 wchar_t, NULL etc.
> + * - Modeling doesn't need full structs and typedefs. Rudimentary structs
> + *   and similar types are sufficient.
> + * - An uninitialized 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.
> + */

This is copied from the cpython model file, AFAICT.  Have you checked that
their license allows us to include it in Xen?  We might have to include
their copyright, BSD-style.

Tim.

> +
> +/* Definitions */
> +#define NULL (void *)0
> +#define PAGE_SIZE 4096UL
> +#define PAGE_MASK (~(PAGE_SIZE-1))
> +
> +#define assert(cond) /* empty */
> +#define page_to_mfn(p) (unsigned long)(p)
> +
> +struct page_info {};
> +
> +/*
> + * 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), and
> + * will only ever return page aligned addresses.
> + */
> +void *map_domain_page(unsigned long mfn)
> +{
> +    void *p = __coverity_alloc__(PAGE_SIZE);
> +
> +    assert(p != NULL);
> +    assert((p & ~PAGE_MASK) == 0);
> +
> +    return p;
> +}
> +
> +void *__map_domain_page(struct page_info *page)
> +{
> +    return map_domain_page(page_to_mfn(page));
> +}
> +
> +/*
> + * unmap_domain_page() will correctly unmap the page, given any virtual
> + * address inside the page.
> + */
> +void unmap_domain_page(const void *va)
> +{
> +    const void *v = (const void*)((unsigned long)va & PAGE_MASK);
> +
> +    __coverity_free__(v);
> +}
> +
> +/*
> + * 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] coverity: Store the modelling file in the source tree.

[Andrew Cooper]

On 04/12/13 15:37, Tim Deegan wrote:
> At 15:29 +0000 on 04 Dec (1386167363), Andrew Cooper wrote:
>> Signed-off-by: Andrew Cooper <andrew.cooper3@citrix.com>
>> CC: Keir Fraser <keir@xen.org>
>> CC: Jan Beulich <JBeulich@suse.com>
>> CC: Tim Deegan <tim@xen.org>
>> CC: Ian Campbell <Ian.Campbell@citrix.com>
>> CC: Ian Jackson <Ian.Jackson@eu.citrix.com>
>> ---
>>  misc/coverity_model.c |   70 +++++++++++++++++++++++++++++++++++++++++++++++++
>>  1 file changed, 70 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..2588adb
>> --- /dev/null
>> +++ b/misc/coverity_model.c
>> @@ -0,0 +1,70 @@
>> +/* Coverity Scan model
>> + *
>> + * This is a modeling file for Coverity Scan. Modeling 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 wchar_t, NULL etc.
>> + * - Modeling doesn't need full structs and typedefs. Rudimentary structs
>> + *   and similar types are sufficient.
>> + * - An uninitialized 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.
>> + */
> This is copied from the cpython model file, AFAICT.  Have you checked that
> their license allows us to include it in Xen?  We might have to include
> their copyright, BSD-style.
>
> Tim.

Hmm - I knew I had forgotten something.

As for Python licensing, it is a little complicated.

>From their own licence file, their coverity modelling file is
"GPL-compatible", with the qualification of

(1) GPL-compatible doesn't mean that we're distributing Python under
    the GPL.  All Python licenses, unlike the GPL, let you distribute
    a modified version without making your changes open source.  The
    GPL-compatible licenses make it possible to combine Python with
    other software that is released under the GPL; the others don't.


In addition, it was only the header which was copied, being by far and
away the best and concise description of what a modelling file is and
how it works.

>From my reading of this, we are ok.

It might be reasonable to include a note saying that we used the cpython
modelling file as a reference (even Coverity themselves recommend it as
a reference), but that all content is Xen specific?

~Andrew

>
>> +
>> +/* Definitions */
>> +#define NULL (void *)0
>> +#define PAGE_SIZE 4096UL
>> +#define PAGE_MASK (~(PAGE_SIZE-1))
>> +
>> +#define assert(cond) /* empty */
>> +#define page_to_mfn(p) (unsigned long)(p)
>> +
>> +struct page_info {};
>> +
>> +/*
>> + * 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), and
>> + * will only ever return page aligned addresses.
>> + */
>> +void *map_domain_page(unsigned long mfn)
>> +{
>> +    void *p = __coverity_alloc__(PAGE_SIZE);
>> +
>> +    assert(p != NULL);
>> +    assert((p & ~PAGE_MASK) == 0);
>> +
>> +    return p;
>> +}
>> +
>> +void *__map_domain_page(struct page_info *page)
>> +{
>> +    return map_domain_page(page_to_mfn(page));
>> +}
>> +
>> +/*
>> + * unmap_domain_page() will correctly unmap the page, given any virtual
>> + * address inside the page.
>> + */
>> +void unmap_domain_page(const void *va)
>> +{
>> +    const void *v = (const void*)((unsigned long)va & PAGE_MASK);
>> +
>> +    __coverity_free__(v);
>> +}
>> +
>> +/*
>> + * 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] coverity: Store the modelling file in the source tree.

[Tim Deegan]

At 15:48 +0000 on 04 Dec (1386168529), Andrew Cooper wrote:
> On 04/12/13 15:37, Tim Deegan wrote:
> > At 15:29 +0000 on 04 Dec (1386167363), Andrew Cooper wrote:
> >> Signed-off-by: Andrew Cooper <andrew.cooper3@citrix.com>
> >> CC: Keir Fraser <keir@xen.org>
> >> CC: Jan Beulich <JBeulich@suse.com>
> >> CC: Tim Deegan <tim@xen.org>
> >> CC: Ian Campbell <Ian.Campbell@citrix.com>
> >> CC: Ian Jackson <Ian.Jackson@eu.citrix.com>
> >> ---
> >>  misc/coverity_model.c |   70 +++++++++++++++++++++++++++++++++++++++++++++++++
> >>  1 file changed, 70 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..2588adb
> >> --- /dev/null
> >> +++ b/misc/coverity_model.c
> >> @@ -0,0 +1,70 @@
> >> +/* Coverity Scan model
> >> + *
> >> + * This is a modeling file for Coverity Scan. Modeling 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 wchar_t, NULL etc.
> >> + * - Modeling doesn't need full structs and typedefs. Rudimentary structs
> >> + *   and similar types are sufficient.
> >> + * - An uninitialized 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.
> >> + */
> > This is copied from the cpython model file, AFAICT.  Have you checked that
> > their license allows us to include it in Xen?  We might have to include
> > their copyright, BSD-style.
> >
> > Tim.
> 
> Hmm - I knew I had forgotten something.
> 
> As for Python licensing, it is a little complicated.
> 
> From their own licence file, their coverity modelling file is
> "GPL-compatible", with the qualification of
> 
> (1) GPL-compatible doesn't mean that we're distributing Python under
>     the GPL.  All Python licenses, unlike the GPL, let you distribute
>     a modified version without making your changes open source.  The
>     GPL-compatible licenses make it possible to combine Python with
>     other software that is released under the GPL; the others don't.
> 
> 
> In addition, it was only the header which was copied, being by far and
> away the best and concise description of what a modelling file is and
> how it works.
> 
> From my reading of this, we are ok.

Good.  Do we need to include their copyright line?

> It might be reasonable to include a note saying that we used the cpython
> modelling file as a reference (even Coverity themselves recommend it as
> a reference), but that all content is Xen specific?

I would be inclined just to rewrite the block comment if the rest of
the file is new code.

Tim.

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

[David Vrabel]

On 04/12/13 15:29, Andrew Cooper wrote:
> +/*
> + * unmap_domain_page() will correctly unmap the page, given any virtual
> + * address inside the page.

I think the va must be page aligned? Or am I getting mixed up with the
requirement for map_domain_page_global()?

David

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

[Andrew Cooper]

On 04/12/13 16:11, David Vrabel wrote:
> On 04/12/13 15:29, Andrew Cooper wrote:
>> +/*
>> + * unmap_domain_page() will correctly unmap the page, given any virtual
>> + * address inside the page.
> I think the va must be page aligned? Or am I getting mixed up with the
> requirement for map_domain_page_global()?
>
> David

unmap_domain_page() uses PFN_DOWN(va), which discards the bottom 12 bits.

unmap_domain_page_global() passes off to vunmap() which does appear to
want an aligned pointer.

~Andrew