1 /***** spin: spin.h *****/
3 /* Copyright (c) 1989-2003 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 */
19 typedef struct Lextok {
20 unsigned short ntyp; /* node type */
21 short ismtyp; /* CONST derived from MTYP */
22 int val; /* value attribute */
23 int ln; /* line number */
24 int indstep; /* part of d_step sequence */
25 struct Symbol *fn; /* file name */
26 struct Symbol *sym; /* symbol reference */
27 struct Sequence *sq; /* sequence */
28 struct SeqList *sl; /* sequence list */
29 struct Lextok *lft, *rgt; /* children in parse tree */
32 typedef struct Slicer {
33 Lextok *n; /* global var, usable as slice criterion */
34 short code; /* type of use: DEREF_USE or normal USE */
35 short used; /* set when handled */
36 struct Slicer *nxt; /* linked list */
39 typedef struct Access {
40 struct Symbol *who; /* proctype name of accessor */
41 struct Symbol *what; /* proctype name of accessed */
42 int cnt, typ; /* parameter nr and, e.g., 's' or 'r' */
43 struct Access *lnk; /* linked list */
46 typedef struct Symbol {
48 int Nid; /* unique number for the name */
49 unsigned short type; /* bit,short,.., chan,struct */
50 unsigned char hidden; /* bit-flags:
52 4=bit-equiv, 8=byte-equiv,
53 16=formal par, 32=inline par,
54 64=treat as if local; 128=read at least once
56 unsigned char colnr; /* for use with xspin during simulation */
57 int nbits; /* optional width specifier */
58 int nel; /* 1 if scalar, >1 if array */
59 int setat; /* last depth value changed */
60 int *val; /* runtime value(s), initl 0 */
61 Lextok **Sval; /* values for structures */
63 int xu; /* exclusive r or w by 1 pid */
64 struct Symbol *xup[2]; /* xr or xs proctype */
65 struct Access *access;/* e.g., senders and receives of chan */
66 Lextok *ini; /* initial value, or chan-def */
67 Lextok *Slst; /* template for structure if struct */
68 struct Symbol *Snm; /* name of the defining struct */
69 struct Symbol *owner; /* set for names of subfields in typedefs */
70 struct Symbol *context; /* 0 if global, or procname */
71 struct Symbol *next; /* linked list */
74 typedef struct Ordered { /* links all names in Symbol table */
79 typedef struct Queue {
80 short qid; /* runtime q index */
81 int qlen; /* nr messages stored */
82 int nslots, nflds; /* capacity, flds/slot */
83 int setat; /* last depth value changed */
84 int *fld_width; /* type of each field */
85 int *contents; /* the values stored */
86 int *stepnr; /* depth when each msg was sent */
87 struct Queue *nxt; /* linked list */
90 typedef struct FSM_state { /* used in pangen5.c - dataflow */
91 int from; /* state number */
92 int seen; /* used for dfs */
93 int in; /* nr of incoming edges */
94 int cr; /* has reachable 1-relevant successor */
96 unsigned long *dom, *mod; /* to mark dominant nodes */
97 struct FSM_trans *t; /* outgoing edges */
98 struct FSM_trans *p; /* incoming edges, predecessors */
99 struct FSM_state *nxt; /* linked list of all states */
102 typedef struct FSM_trans { /* used in pangen5.c - dataflow */
104 short relevant; /* when sliced */
105 short round; /* ditto: iteration when marked */
106 struct FSM_use *Val[2]; /* 0=reads, 1=writes */
107 struct Element *step;
108 struct FSM_trans *nxt;
111 typedef struct FSM_use { /* used in pangen5.c - dataflow */
118 typedef struct Element {
119 Lextok *n; /* defines the type & contents */
120 int Seqno; /* identifies this el within system */
121 int seqno; /* identifies this el within a proc */
122 int merge; /* set by -O if step can be merged */
125 short merge_in; /* nr of incoming edges */
126 short merge_mark; /* state was generated in merge sequence */
127 unsigned char status; /* used by analyzer generator */
128 struct FSM_use *dead; /* optional dead variable list */
129 struct SeqList *sub; /* subsequences, for compounds */
130 struct SeqList *esc; /* zero or more escape sequences */
131 struct Element *Nxt; /* linked list - for global lookup */
132 struct Element *nxt; /* linked list - program structure */
135 typedef struct Sequence {
137 Element *last; /* links onto continuations */
138 Element *extent; /* last element in original */
139 int maxel; /* 1+largest id in sequence */
142 typedef struct SeqList {
143 Sequence *this; /* one sequence */
144 struct SeqList *nxt; /* linked list */
147 typedef struct Label {
151 int visible; /* label referenced in claim (slice relevant) */
155 typedef struct Lbreak {
160 typedef struct RunList {
161 Symbol *n; /* name */
162 int tn; /* ordinal of type */
163 int pid; /* process id */
164 int priority; /* for simulations only */
165 Element *pc; /* current stmnt */
166 Sequence *ps; /* used by analyzer generator */
167 Lextok *prov; /* provided clause */
168 Symbol *symtab; /* local variables */
169 struct RunList *nxt; /* linked list */
172 typedef struct ProcList {
173 Symbol *n; /* name */
174 Lextok *p; /* parameters */
175 Sequence *s; /* body */
176 Lextok *prov; /* provided clause */
177 short tn; /* ordinal number */
178 short det; /* deterministic */
179 struct ProcList *nxt; /* linked list */
182 typedef Lextok *Lexptr;
184 #define YYSTYPE Lexptr
186 #define ZN (Lextok *)0
187 #define ZS (Symbol *)0
188 #define ZE (Element *)0
190 #define DONE 1 /* status bits of elements */
191 #define ATOM 2 /* part of an atomic chain */
192 #define L_ATOM 4 /* last element in a chain */
193 #define I_GLOB 8 /* inherited global ref */
194 #define DONE2 16 /* used in putcode and main*/
195 #define D_ATOM 32 /* deterministic atomic */
196 #define ENDSTATE 64 /* normal endstate */
199 #define Nhash 255 /* slots in symbol hash-table */
201 #define XR 1 /* non-shared receive-only */
202 #define XS 2 /* non-shared send-only */
203 #define XX 4 /* overrides XR or XS tag */
205 #define CODE_FRAG 2 /* auto-numbered code-fragment */
206 #define CODE_DECL 4 /* auto-numbered c_decl */
207 #define PREDEF 3 /* predefined name: _p, _last */
209 #define UNSIGNED 5 /* val defines width in bits */
210 #define BIT 1 /* also equal to width in bits */
211 #define BYTE 8 /* ditto */
212 #define SHORT 16 /* ditto */
213 #define INT 32 /* ditto */
214 #define CHAN 64 /* not */
215 #define STRUCT 128 /* user defined structure name */
217 #define SOMETHINGBIG 65536
218 #define RATHERSMALL 512
221 #define max(a,b) (((a)<(b)) ? (b) : (a))
224 enum { INIV, PUTV, LOGV }; /* for pangen[14].c */
226 /***** prototype definitions *****/
227 Element *eval_sub(Element *);
228 Element *get_lab(Lextok *, int);
229 Element *huntele(Element *, int, int);
230 Element *huntstart(Element *);
231 Element *target(Element *);
233 Lextok *do_unless(Lextok *, Lextok *);
234 Lextok *expand(Lextok *, int);
235 Lextok *getuname(Symbol *);
236 Lextok *mk_explicit(Lextok *, int, int);
237 Lextok *nn(Lextok *, int, Lextok *, Lextok *);
238 Lextok *rem_lab(Symbol *, Lextok *, Symbol *);
239 Lextok *rem_var(Symbol *, Lextok *, Symbol *, Lextok *);
240 Lextok *tail_add(Lextok *, Lextok *);
242 ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *);
244 SeqList *seqlist(Sequence *, SeqList *);
245 Sequence *close_seq(int);
247 Symbol *break_dest(void);
248 Symbol *findloc(Symbol *);
249 Symbol *has_lab(Element *, int);
250 Symbol *lookup(char *);
251 Symbol *prep_inline(Symbol *, Lextok *);
256 int any_oper(Lextok *, int);
257 int any_undo(Lextok *);
258 int c_add_sv(FILE *);
259 int cast_val(int, int, int);
260 int checkvar(Symbol *, int);
261 int Cnt_flds(Lextok *);
262 int cnt_mpars(Lextok *);
263 int complete_rendez(void);
264 int enable(Lextok *);
265 int Enabled0(Element *);
267 int find_lab(Symbol *, Symbol *, int);
268 int find_maxel(Symbol *);
269 int full_name(FILE *, Lextok *, Symbol *, int);
270 int getlocal(Lextok *);
271 int getval(Lextok *);
272 int glob_inline(char *);
273 int has_typ(Lextok *, int);
274 int in_bound(Symbol *, int);
275 int interprint(FILE *, Lextok *);
276 int printm(FILE *, Lextok *);
278 int isproctype(char *);
280 int Lval_struct(Lextok *, Symbol *, int, int);
281 int main(int, char **);
282 int pc_value(Lextok *);
283 int proper_enabler(Lextok *);
284 int putcode(FILE *, Sequence *, Element *, int, int, int);
285 int q_is_sync(Lextok *);
289 int qrecv(Lextok *, int);
291 int remotelab(Lextok *);
292 int remotevar(Lextok *);
293 int Rval_struct(Lextok *, Symbol *, int);
294 int setlocal(Lextok *, int);
295 int setval(Lextok *, int);
296 int sputtype(char *, int);
297 int Sym_typ(Lextok *);
298 int tl_main(int, char *[]);
299 int Width_set(int *, int, Lextok *);
304 void AST_track(Lextok *, int);
305 void add_seq(Lextok *);
307 void announce(char *);
308 void c_state(Symbol *, Symbol *, Symbol *);
309 void c_add_def(FILE *);
310 void c_add_loc(FILE *, char *);
311 void c_add_locinit(FILE *, int, char *);
312 void c_add_use(FILE *);
313 void c_chandump(FILE *);
314 void c_preview(void);
315 void c_struct(FILE *, char *, Symbol *);
316 void c_track(Symbol *, Symbol *, Symbol *);
317 void c_var(FILE *, char *, Symbol *);
318 void c_wrapper(FILE *);
319 void chanaccess(void);
320 void check_param_count(int, Lextok *);
321 void checkrun(Symbol *, int);
322 void comment(FILE *, Lextok *, int);
323 void cross_dsteps(Lextok *, Lextok *);
324 void doq(Symbol *, int, RunList *);
325 void dotag(FILE *, char *);
326 void do_locinits(FILE *);
327 void do_var(FILE *, int, char *, Symbol *, char *, char *, char *);
328 void dump_struct(Symbol *, char *, RunList *);
329 void dumpclaims(FILE *, int, char *);
330 void dumpglobals(void);
331 void dumplabels(void);
332 void dumplocal(RunList *);
333 void dumpsrc(int, int);
334 void fatal(char *, char *);
335 void fix_dest(Symbol *, Symbol *);
336 void genaddproc(void);
337 void genaddqueue(void);
338 void gencodetable(FILE *);
339 void genheader(void);
344 void ini_struct(Symbol *);
345 void loose_ends(void);
346 void make_atomic(Sequence *, int);
347 void match_trail(void);
348 void no_side_effects(char *);
349 void nochan_manip(Lextok *, Lextok *, int);
350 void non_fatal(char *, char *);
351 void ntimes(FILE *, int, int, char *c[]);
353 void p_talk(Element *, int);
354 void pickup_inline(Symbol *, Lextok *);
355 void plunk_c_decls(FILE *);
356 void plunk_c_fcts(FILE *);
357 void plunk_expr(FILE *, char *);
358 void plunk_inline(FILE *, char *, int);
359 void prehint(Symbol *);
360 void preruse(FILE *, Lextok *);
361 void prune_opts(Lextok *);
362 void pstext(int, char *);
363 void pushbreak(void);
364 void putname(FILE *, char *, Lextok *, int, char *);
365 void putremote(FILE *, Lextok *, int);
367 void putsrc(Element *);
368 void putstmnt(FILE *, Lextok *, int);
369 void putunames(FILE *);
371 void runnable(ProcList *, int, int);
373 void setaccess(Symbol *, Symbol *, int, int);
374 void set_lab(Symbol *, Element *);
375 void setmtype(Lextok *);
376 void setpname(Lextok *);
377 void setptype(Lextok *, int, Lextok *);
378 void setuname(Lextok *);
379 void setutype(Lextok *, Symbol *, Lextok *);
380 void setxus(Lextok *, int);
381 void Srand(unsigned);
382 void start_claim(int);
383 void struct_name(Lextok *, Symbol *, int, char *);
385 void symvar(Symbol *);
386 void trackchanuse(Lextok *, Lextok *, int);
387 void trackvar(Lextok *, Lextok *);
388 void trackrun(Lextok *);
389 void trapwonly(Lextok *, char *); /* spin.y and main.c */
390 void typ2c(Symbol *);
391 void typ_ck(int, int, char *);
392 void undostmnt(Lextok *, int);
393 void unrem_Seq(void);
395 void varcheck(Element *, Element *);
398 void yyerror(char *, ...);