Computer Laboratory

tesla.h
Go to the documentation of this file.
1 /*
2  * Copyright (c) 2012 Jonathan Anderson
3  * All rights reserved.
4  *
5  * This software was developed by SRI International and the University of
6  * Cambridge Computer Laboratory under DARPA/AFRL contract (FA8750-10-C-0237)
7  * ("CTSRD"), as part of the DARPA CRASH research programme.
8  *
9  * Redistribution and use in source and binary forms, with or without
10  * modification, are permitted provided that the following conditions
11  * are met:
12  * 1. Redistributions of source code must retain the above copyright
13  * notice, this list of conditions and the following disclaimer.
14  * 2. Redistributions in binary form must reproduce the above copyright
15  * notice, this list of conditions and the following disclaimer in the
16  * documentation and/or other materials provided with the distribution.
17  *
18  * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
19  * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
20  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
21  * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
22  * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
23  * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
24  * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
25  * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
26  * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
27  * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
28  * SUCH DAMAGE.
29  */
30 
39 #ifndef TESLA_H
40 #define TESLA_H
41 
50 typedef struct __tesla_event {} __tesla_event;
52 
54 typedef int __tesla_count;
55 
65 inline void
66 __tesla_inline_assertion(const char *filename, int line, int count,
67  __tesla_locality *loc, ...)
68 {
69 }
70 
71 
72 /* Only define the following things if doing TESLA analysis, not compiling. */
73 #ifdef __TESLA_ANALYSER__
74 
75 #include <sys/types.h>
76 
83 
86 
87 
88 /* TESLA events: */
90 struct __tesla_event* __tesla_call(void*, ...);
91 
93 struct __tesla_event* __tesla_return(void*, ...);
94 
95 
98 
101 
103 int __tesla_flags(int);
104 
106 int __tesla_mask(int);
107 
114 
127 
128 
131 
134 
136 
138 void* __tesla_any_ptr();
139 int __tesla_any_int();
140 long __tesla_any_long();
141 long long __tesla_any_longlong();
142 register_t __tesla_any_register_t();
143 
144 #define __tesla_any(type) __tesla_any_##type()
145 
146 
147 /*
148  * Structure-related automata descriptions:
149  */
150 
151 struct __tesla_automaton_description;
152 struct __tesla_automaton_usage;
153 
155 struct __tesla_automaton_description* __tesla_automaton_done();
156 
157 inline struct __tesla_automaton_usage*
159  __tesla_locality *loc, ...)
160 {
161  return 0;
162 }
163 
164 
174 #define __tesla_struct_usage(subject, automaton, loc, start, end) \
175  struct __tesla_automaton_usage* \
176  __tesla_struct_automaton_usage_##struct_name##_##automaton(subject) { \
177  return __tesla_struct_uses_automaton( \
178  #automaton, loc, start, end); \
179  }
180 
181 
187 #define __tesla_automaton(name, ...) \
188  struct __tesla_automaton_description* name(__VA_ARGS__)
189 
190 #else /* !__TESLA_ANALYSER__ */
191 
192 /*
193  * We are not doing TESLA analysis, no we don't want a lot of artefacts left
194  * behind like 'extern struct __tesla_locality* __tesla_global'.
195  *
196  * All that we do want to leave behind are the inline assertion sites, which
197  * we can translate into instrumentation calls.
198  */
199 
200 #define __tesla_global ((struct __tesla_locality*) 0)
201 #define __tesla_perthread ((struct __tesla_locality*) 0)
202 
203 #define __tesla_sequence(...) 1
204 
205 #define __tesla_struct_automaton(...)
206 #define __tesla_automaton(name, ...)
207 
208 #define __tesla_call(...) 0
209 #define __tesla_return(...) 0
210 
211 #define __tesla_callee(...) 0
212 #define __tesla_caller(...) 0
213 
214 #define __tesla_optional(...) 0
215 #define __tesla_any(...) 0
216 
217 #define __tesla_strict(...) 0
218 #define __tesla_conditional(...) 0
219 
220 #endif /* __TESLA_ANALYSER__ */
221 
224 #endif /* TESLA_H */