0b55f123 |
1 | /***** spin: spin.h *****/ |
2 | |
3 | /* Copyright (c) 1989-2007 by Lucent Technologies, Bell Laboratories. */ |
4 | /* All Rights Reserved. This software is for educational purposes only. */ |
5 | /* No guarantee whatsoever is expressed or implied by the distribution of */ |
6 | /* this code. Permission is given to distribute this code provided that */ |
7 | /* this introductory message is not removed and no monies are exchanged. */ |
8 | /* Software written by Gerard J. Holzmann. For tool documentation see: */ |
9 | /* http://spinroot.com/ */ |
10 | /* Send all bug-reports and/or questions to: bugs@spinroot.com */ |
11 | |
12 | #ifndef SEEN_SPIN_H |
13 | #define SEEN_SPIN_H |
14 | |
15 | #include <stdio.h> |
16 | #include <string.h> |
17 | #include <ctype.h> |
18 | #ifndef PC |
19 | #include <memory.h> |
20 | #endif |
21 | |
22 | typedef struct Lextok { |
23 | unsigned short ntyp; /* node type */ |
24 | short ismtyp; /* CONST derived from MTYP */ |
25 | int val; /* value attribute */ |
26 | int ln; /* line number */ |
27 | int indstep; /* part of d_step sequence */ |
28 | struct Symbol *fn; /* file name */ |
29 | struct Symbol *sym; /* symbol reference */ |
30 | struct Sequence *sq; /* sequence */ |
31 | struct SeqList *sl; /* sequence list */ |
32 | struct Lextok *lft, *rgt; /* children in parse tree */ |
33 | } Lextok; |
34 | |
35 | typedef struct Slicer { |
36 | Lextok *n; /* global var, usable as slice criterion */ |
37 | short code; /* type of use: DEREF_USE or normal USE */ |
38 | short used; /* set when handled */ |
39 | struct Slicer *nxt; /* linked list */ |
40 | } Slicer; |
41 | |
42 | typedef struct Access { |
43 | struct Symbol *who; /* proctype name of accessor */ |
44 | struct Symbol *what; /* proctype name of accessed */ |
45 | int cnt, typ; /* parameter nr and, e.g., 's' or 'r' */ |
46 | struct Access *lnk; /* linked list */ |
47 | } Access; |
48 | |
49 | typedef struct Symbol { |
50 | char *name; |
51 | int Nid; /* unique number for the name */ |
52 | unsigned short type; /* bit,short,.., chan,struct */ |
53 | unsigned char hidden; /* bit-flags: |
54 | 1=hide, 2=show, |
55 | 4=bit-equiv, 8=byte-equiv, |
56 | 16=formal par, 32=inline par, |
57 | 64=treat as if local; 128=read at least once |
58 | */ |
59 | unsigned char colnr; /* for use with xspin during simulation */ |
60 | int nbits; /* optional width specifier */ |
61 | int nel; /* 1 if scalar, >1 if array */ |
62 | int setat; /* last depth value changed */ |
63 | int *val; /* runtime value(s), initl 0 */ |
64 | Lextok **Sval; /* values for structures */ |
65 | |
66 | int xu; /* exclusive r or w by 1 pid */ |
67 | struct Symbol *xup[2]; /* xr or xs proctype */ |
68 | struct Access *access;/* e.g., senders and receives of chan */ |
69 | Lextok *ini; /* initial value, or chan-def */ |
70 | Lextok *Slst; /* template for structure if struct */ |
71 | struct Symbol *Snm; /* name of the defining struct */ |
72 | struct Symbol *owner; /* set for names of subfields in typedefs */ |
73 | struct Symbol *context; /* 0 if global, or procname */ |
74 | struct Symbol *next; /* linked list */ |
75 | } Symbol; |
76 | |
77 | typedef struct Ordered { /* links all names in Symbol table */ |
78 | struct Symbol *entry; |
79 | struct Ordered *next; |
80 | } Ordered; |
81 | |
82 | typedef struct Queue { |
83 | short qid; /* runtime q index */ |
84 | int qlen; /* nr messages stored */ |
85 | int nslots, nflds; /* capacity, flds/slot */ |
86 | int setat; /* last depth value changed */ |
87 | int *fld_width; /* type of each field */ |
88 | int *contents; /* the values stored */ |
89 | int *stepnr; /* depth when each msg was sent */ |
90 | struct Queue *nxt; /* linked list */ |
91 | } Queue; |
92 | |
93 | typedef struct FSM_state { /* used in pangen5.c - dataflow */ |
94 | int from; /* state number */ |
95 | int seen; /* used for dfs */ |
96 | int in; /* nr of incoming edges */ |
97 | int cr; /* has reachable 1-relevant successor */ |
98 | int scratch; |
99 | unsigned long *dom, *mod; /* to mark dominant nodes */ |
100 | struct FSM_trans *t; /* outgoing edges */ |
101 | struct FSM_trans *p; /* incoming edges, predecessors */ |
102 | struct FSM_state *nxt; /* linked list of all states */ |
103 | } FSM_state; |
104 | |
105 | typedef struct FSM_trans { /* used in pangen5.c - dataflow */ |
106 | int to; |
107 | short relevant; /* when sliced */ |
108 | short round; /* ditto: iteration when marked */ |
109 | struct FSM_use *Val[2]; /* 0=reads, 1=writes */ |
110 | struct Element *step; |
111 | struct FSM_trans *nxt; |
112 | } FSM_trans; |
113 | |
114 | typedef struct FSM_use { /* used in pangen5.c - dataflow */ |
115 | Lextok *n; |
116 | Symbol *var; |
117 | int special; |
118 | struct FSM_use *nxt; |
119 | } FSM_use; |
120 | |
121 | typedef struct Element { |
122 | Lextok *n; /* defines the type & contents */ |
123 | int Seqno; /* identifies this el within system */ |
124 | int seqno; /* identifies this el within a proc */ |
125 | int merge; /* set by -O if step can be merged */ |
126 | int merge_start; |
127 | int merge_single; |
128 | short merge_in; /* nr of incoming edges */ |
129 | short merge_mark; /* state was generated in merge sequence */ |
130 | unsigned int status; /* used by analyzer generator */ |
131 | struct FSM_use *dead; /* optional dead variable list */ |
132 | struct SeqList *sub; /* subsequences, for compounds */ |
133 | struct SeqList *esc; /* zero or more escape sequences */ |
134 | struct Element *Nxt; /* linked list - for global lookup */ |
135 | struct Element *nxt; /* linked list - program structure */ |
136 | } Element; |
137 | |
138 | typedef struct Sequence { |
139 | Element *frst; |
140 | Element *last; /* links onto continuations */ |
141 | Element *extent; /* last element in original */ |
142 | int maxel; /* 1+largest id in sequence */ |
143 | } Sequence; |
144 | |
145 | typedef struct SeqList { |
146 | Sequence *this; /* one sequence */ |
147 | struct SeqList *nxt; /* linked list */ |
148 | } SeqList; |
149 | |
150 | typedef struct Label { |
151 | Symbol *s; |
152 | Symbol *c; |
153 | Element *e; |
154 | int visible; /* label referenced in claim (slice relevant) */ |
155 | struct Label *nxt; |
156 | } Label; |
157 | |
158 | typedef struct Lbreak { |
159 | Symbol *l; |
160 | struct Lbreak *nxt; |
161 | } Lbreak; |
162 | |
163 | typedef struct RunList { |
164 | Symbol *n; /* name */ |
165 | int tn; /* ordinal of type */ |
166 | int pid; /* process id */ |
167 | int priority; /* for simulations only */ |
168 | Element *pc; /* current stmnt */ |
169 | Sequence *ps; /* used by analyzer generator */ |
170 | Lextok *prov; /* provided clause */ |
171 | Symbol *symtab; /* local variables */ |
172 | struct RunList *nxt; /* linked list */ |
173 | } RunList; |
174 | |
175 | typedef struct ProcList { |
176 | Symbol *n; /* name */ |
177 | Lextok *p; /* parameters */ |
178 | Sequence *s; /* body */ |
179 | Lextok *prov; /* provided clause */ |
180 | short tn; /* ordinal number */ |
181 | unsigned char det; /* deterministic */ |
182 | unsigned char unsafe; /* contains global var inits */ |
183 | struct ProcList *nxt; /* linked list */ |
184 | } ProcList; |
185 | |
186 | typedef Lextok *Lexptr; |
187 | |
188 | #define YYSTYPE Lexptr |
189 | |
190 | #define ZN (Lextok *)0 |
191 | #define ZS (Symbol *)0 |
192 | #define ZE (Element *)0 |
193 | |
194 | #define DONE 1 /* status bits of elements */ |
195 | #define ATOM 2 /* part of an atomic chain */ |
196 | #define L_ATOM 4 /* last element in a chain */ |
197 | #define I_GLOB 8 /* inherited global ref */ |
198 | #define DONE2 16 /* used in putcode and main*/ |
199 | #define D_ATOM 32 /* deterministic atomic */ |
200 | #define ENDSTATE 64 /* normal endstate */ |
201 | #define CHECK2 128 /* status bits for remote ref check */ |
202 | #define CHECK3 256 /* status bits for atomic jump check */ |
203 | |
204 | #define Nhash 255 /* slots in symbol hash-table */ |
205 | |
206 | #define XR 1 /* non-shared receive-only */ |
207 | #define XS 2 /* non-shared send-only */ |
208 | #define XX 4 /* overrides XR or XS tag */ |
209 | |
210 | #define CODE_FRAG 2 /* auto-numbered code-fragment */ |
211 | #define CODE_DECL 4 /* auto-numbered c_decl */ |
212 | #define PREDEF 3 /* predefined name: _p, _last */ |
213 | |
214 | #define UNSIGNED 5 /* val defines width in bits */ |
215 | #define BIT 1 /* also equal to width in bits */ |
216 | #define BYTE 8 /* ditto */ |
217 | #define SHORT 16 /* ditto */ |
218 | #define INT 32 /* ditto */ |
219 | #define CHAN 64 /* not */ |
220 | #define STRUCT 128 /* user defined structure name */ |
221 | |
222 | #define SOMETHINGBIG 65536 |
223 | #define RATHERSMALL 512 |
224 | |
225 | #ifndef max |
226 | #define max(a,b) (((a)<(b)) ? (b) : (a)) |
227 | #endif |
228 | |
229 | enum { INIV, PUTV, LOGV }; /* for pangen[14].c */ |
230 | |
231 | /***** prototype definitions *****/ |
232 | Element *eval_sub(Element *); |
233 | Element *get_lab(Lextok *, int); |
234 | Element *huntele(Element *, int, int); |
235 | Element *huntstart(Element *); |
236 | Element *target(Element *); |
237 | |
238 | Lextok *do_unless(Lextok *, Lextok *); |
239 | Lextok *expand(Lextok *, int); |
240 | Lextok *getuname(Symbol *); |
241 | Lextok *mk_explicit(Lextok *, int, int); |
242 | Lextok *nn(Lextok *, int, Lextok *, Lextok *); |
243 | Lextok *rem_lab(Symbol *, Lextok *, Symbol *); |
244 | Lextok *rem_var(Symbol *, Lextok *, Symbol *, Lextok *); |
245 | Lextok *tail_add(Lextok *, Lextok *); |
246 | |
247 | ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *); |
248 | |
249 | SeqList *seqlist(Sequence *, SeqList *); |
250 | Sequence *close_seq(int); |
251 | |
252 | Symbol *break_dest(void); |
253 | Symbol *findloc(Symbol *); |
254 | Symbol *has_lab(Element *, int); |
255 | Symbol *lookup(char *); |
256 | Symbol *prep_inline(Symbol *, Lextok *); |
257 | |
258 | char *emalloc(size_t); |
259 | long Rand(void); |
260 | |
261 | int any_oper(Lextok *, int); |
262 | int any_undo(Lextok *); |
263 | int c_add_sv(FILE *); |
264 | int cast_val(int, int, int); |
265 | int checkvar(Symbol *, int); |
266 | int Cnt_flds(Lextok *); |
267 | int cnt_mpars(Lextok *); |
268 | int complete_rendez(void); |
269 | int enable(Lextok *); |
270 | int Enabled0(Element *); |
271 | int eval(Lextok *); |
272 | int find_lab(Symbol *, Symbol *, int); |
273 | int find_maxel(Symbol *); |
274 | int full_name(FILE *, Lextok *, Symbol *, int); |
275 | int getlocal(Lextok *); |
276 | int getval(Lextok *); |
277 | int glob_inline(char *); |
278 | int has_typ(Lextok *, int); |
279 | int in_bound(Symbol *, int); |
280 | int interprint(FILE *, Lextok *); |
281 | int printm(FILE *, Lextok *); |
282 | int ismtype(char *); |
283 | int isproctype(char *); |
284 | int isutype(char *); |
285 | int Lval_struct(Lextok *, Symbol *, int, int); |
286 | int main(int, char **); |
287 | int pc_value(Lextok *); |
288 | int proper_enabler(Lextok *); |
289 | int putcode(FILE *, Sequence *, Element *, int, int, int); |
290 | int q_is_sync(Lextok *); |
291 | int qlen(Lextok *); |
292 | int qfull(Lextok *); |
293 | int qmake(Symbol *); |
294 | int qrecv(Lextok *, int); |
295 | int qsend(Lextok *); |
296 | int remotelab(Lextok *); |
297 | int remotevar(Lextok *); |
298 | int Rval_struct(Lextok *, Symbol *, int); |
299 | int setlocal(Lextok *, int); |
300 | int setval(Lextok *, int); |
301 | int sputtype(char *, int); |
302 | int Sym_typ(Lextok *); |
303 | int tl_main(int, char *[]); |
304 | int Width_set(int *, int, Lextok *); |
305 | int yyparse(void); |
306 | int yywrap(void); |
307 | int yylex(void); |
308 | |
309 | void AST_track(Lextok *, int); |
310 | void add_seq(Lextok *); |
311 | void alldone(int); |
312 | void announce(char *); |
313 | void c_state(Symbol *, Symbol *, Symbol *); |
314 | void c_add_def(FILE *); |
315 | void c_add_loc(FILE *, char *); |
316 | void c_add_locinit(FILE *, int, char *); |
317 | void c_add_use(FILE *); |
318 | void c_chandump(FILE *); |
319 | void c_preview(void); |
320 | void c_struct(FILE *, char *, Symbol *); |
321 | void c_track(Symbol *, Symbol *, Symbol *); |
322 | void c_var(FILE *, char *, Symbol *); |
323 | void c_wrapper(FILE *); |
324 | void chanaccess(void); |
325 | void check_param_count(int, Lextok *); |
326 | void checkrun(Symbol *, int); |
327 | void comment(FILE *, Lextok *, int); |
328 | void cross_dsteps(Lextok *, Lextok *); |
329 | void doq(Symbol *, int, RunList *); |
330 | void dotag(FILE *, char *); |
331 | void do_locinits(FILE *); |
332 | void do_var(FILE *, int, char *, Symbol *, char *, char *, char *); |
333 | void dump_struct(Symbol *, char *, RunList *); |
334 | void dumpclaims(FILE *, int, char *); |
335 | void dumpglobals(void); |
336 | void dumplabels(void); |
337 | void dumplocal(RunList *); |
338 | void dumpsrc(int, int); |
339 | void fatal(char *, char *); |
340 | void fix_dest(Symbol *, Symbol *); |
341 | void genaddproc(void); |
342 | void genaddqueue(void); |
343 | void gencodetable(FILE *); |
344 | void genheader(void); |
345 | void genother(void); |
346 | void gensrc(void); |
347 | void gensvmap(void); |
348 | void genunio(void); |
349 | void ini_struct(Symbol *); |
350 | void loose_ends(void); |
351 | void make_atomic(Sequence *, int); |
352 | void match_trail(void); |
353 | void no_side_effects(char *); |
354 | void nochan_manip(Lextok *, Lextok *, int); |
355 | void non_fatal(char *, char *); |
356 | void ntimes(FILE *, int, int, char *c[]); |
357 | void open_seq(int); |
358 | void p_talk(Element *, int); |
359 | void pickup_inline(Symbol *, Lextok *); |
360 | void plunk_c_decls(FILE *); |
361 | void plunk_c_fcts(FILE *); |
362 | void plunk_expr(FILE *, char *); |
363 | void plunk_inline(FILE *, char *, int); |
364 | void prehint(Symbol *); |
365 | void preruse(FILE *, Lextok *); |
366 | void prune_opts(Lextok *); |
367 | void pstext(int, char *); |
368 | void pushbreak(void); |
369 | void putname(FILE *, char *, Lextok *, int, char *); |
370 | void putremote(FILE *, Lextok *, int); |
371 | void putskip(int); |
372 | void putsrc(Element *); |
373 | void putstmnt(FILE *, Lextok *, int); |
374 | void putunames(FILE *); |
375 | void rem_Seq(void); |
376 | void runnable(ProcList *, int, int); |
377 | void sched(void); |
378 | void setaccess(Symbol *, Symbol *, int, int); |
379 | void set_lab(Symbol *, Element *); |
380 | void setmtype(Lextok *); |
381 | void setpname(Lextok *); |
382 | void setptype(Lextok *, int, Lextok *); |
383 | void setuname(Lextok *); |
384 | void setutype(Lextok *, Symbol *, Lextok *); |
385 | void setxus(Lextok *, int); |
386 | void Srand(unsigned); |
387 | void start_claim(int); |
388 | void struct_name(Lextok *, Symbol *, int, char *); |
389 | void symdump(void); |
390 | void symvar(Symbol *); |
391 | void trackchanuse(Lextok *, Lextok *, int); |
392 | void trackvar(Lextok *, Lextok *); |
393 | void trackrun(Lextok *); |
394 | void trapwonly(Lextok * /* , char * */); /* spin.y and main.c */ |
395 | void typ2c(Symbol *); |
396 | void typ_ck(int, int, char *); |
397 | void undostmnt(Lextok *, int); |
398 | void unrem_Seq(void); |
399 | void unskip(int); |
400 | void varcheck(Element *, Element *); |
401 | void whoruns(int); |
402 | void wrapup(int); |
403 | void yyerror(char *, ...); |
404 | #endif |