1 /* Coverity Scan model
2 *
3 * This is a modelling file for Coverity Scan. Modelling helps to avoid false
4 * positives.
5 *
6 * - A model file can't import any header files.
7 * - Therefore only some built-in primitives like int, char and void are
8 * available but not NULL etc.
9 * - Modelling doesn't need full structs and typedefs. Rudimentary structs
10 * and similar types are sufficient.
11 * - An uninitialised local pointer is not an error. It signifies that the
12 * variable could be either NULL or have some data.
13 *
14 * Coverity Scan doesn't pick up modifications automatically. The model file
15 * must be uploaded by an admin in the analysis.
16 *
17 * The Xen Coverity Scan modelling file used the cpython modelling file as a
18 * reference to get started (suggested by Coverty Scan themselves as a good
19 * example), but all content is Xen specific.
20 *
21 * Copyright (c) 2013-2014 Citrix Systems Ltd; All Right Reserved
22 *
23 * Based on:
24 * http://hg.python.org/cpython/file/tip/Misc/coverity_model.c
25 * Copyright (c) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010,
26 * 2011, 2012, 2013 Python Software Foundation; All Rights Reserved
27 *
28 */
29
30 /*
31 * Useful references:
32 * https://scan.coverity.com/models
33 */
34
35 /* Definitions */
36 #define NULL (void *)0
37 #define PAGE_SIZE 4096UL
38 #define PAGE_MASK (~(PAGE_SIZE-1))
39
40 #define assert(cond) /* empty */
41
42 struct page_info {};
43 struct pthread_mutex_t {};
44
45 struct libxl__ctx
46 {
47 struct pthread_mutex_t lock;
48 };
49 typedef struct libxl__ctx libxl_ctx;
50
51 /*
52 * Xen malloc. Behaves exactly like regular malloc(), except it also contains
53 * an alignment parameter.
54 *
55 * TODO: work out how to correctly model bad alignments as errors.
56 */
_xmalloc(unsigned long size,unsigned long align)57 void *_xmalloc(unsigned long size, unsigned long align)
58 {
59 int has_memory;
60
61 __coverity_negative_sink__(size);
62 __coverity_negative_sink__(align);
63
64 if ( has_memory )
65 return __coverity_alloc__(size);
66 else
67 return NULL;
68 }
69
70 /*
71 * Xen free. Frees a pointer allocated by _xmalloc().
72 */
xfree(void * va)73 void xfree(void *va)
74 {
75 __coverity_free__(va);
76 }
77
78
79 /*
80 * map_domain_page() takes an existing domain page and possibly maps it into
81 * the Xen pagetables, to allow for direct access. Model this as a memory
82 * allocation of exactly 1 page.
83 *
84 * map_domain_page() never fails. (It will BUG() before returning NULL)
85 */
map_domain_page(unsigned long mfn)86 void *map_domain_page(unsigned long mfn)
87 {
88 unsigned long ptr = (unsigned long)__coverity_alloc__(PAGE_SIZE);
89
90 /*
91 * Expressing the alignment of the memory allocation isn't possible. As a
92 * substitute, tell Coverity to ignore any path where ptr isn't page
93 * aligned.
94 */
95 if ( ptr & ~PAGE_MASK )
96 __coverity_panic__();
97
98 return (void *)ptr;
99 }
100
101 /*
102 * unmap_domain_page() will unmap a page. Model it as a free(). Any *va
103 * within the page is valid to pass.
104 */
unmap_domain_page(const void * va)105 void unmap_domain_page(const void *va)
106 {
107 unsigned long ptr = (unsigned long)va & PAGE_MASK;
108
109 __coverity_free__((void *)ptr);
110 }
111
112 /*
113 * Coverity appears not to understand that errx() unconditionally exits.
114 */
errx(int,const char *,...)115 void errx(int, const char*, ...)
116 {
117 __coverity_panic__();
118 }
119
120 /*
121 * Coverity doesn't appear to be certain that the libxl ctx->lock is recursive.
122 */
libxl__ctx_lock(libxl_ctx * ctx)123 void libxl__ctx_lock(libxl_ctx *ctx)
124 {
125 __coverity_recursive_lock_acquire__(&ctx->lock);
126 }
127
libxl__ctx_unlock(libxl_ctx * ctx)128 void libxl__ctx_unlock(libxl_ctx *ctx)
129 {
130 __coverity_recursive_lock_release__(&ctx->lock);
131 }
132
133 /*
134 * Coverity doesn't understand __builtin_unreachable(), which causes it to
135 * incorrectly find issues based on continuing execution along the false
136 * branch of an ASSERT().
137 */
__builtin_unreachable(void)138 void __builtin_unreachable(void)
139 {
140 __coverity_panic__();
141 }
142
143 /*
144 * Local variables:
145 * mode: C
146 * c-file-style: "BSD"
147 * c-basic-offset: 4
148 * tab-width: 4
149 * indent-tabs-mode: nil
150 * End:
151 */
152