aa55c6f761aee423da9f0af5b743636244c82995
1 /***** spin: spin.h *****/
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 */
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 */
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 */
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 */
49 typedef struct Symbol
{
51 int Nid
; /* unique number for the name */
52 unsigned short type
; /* bit,short,.., chan,struct */
53 unsigned char hidden
; /* bit-flags:
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
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 */
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 */
77 typedef struct Ordered
{ /* links all names in Symbol table */
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 */
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 */
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 */
105 typedef struct FSM_trans
{ /* used in pangen5.c - dataflow */
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
;
114 typedef struct FSM_use
{ /* used in pangen5.c - dataflow */
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 */
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 */
138 typedef struct Sequence
{
140 Element
*last
; /* links onto continuations */
141 Element
*extent
; /* last element in original */
142 int maxel
; /* 1+largest id in sequence */
145 typedef struct SeqList
{
146 Sequence
*this; /* one sequence */
147 struct SeqList
*nxt
; /* linked list */
150 typedef struct Label
{
154 int visible
; /* label referenced in claim (slice relevant) */
158 typedef struct Lbreak
{
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 */
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 */
186 typedef Lextok
*Lexptr
;
188 #define YYSTYPE Lexptr
190 #define ZN (Lextok *)0
191 #define ZS (Symbol *)0
192 #define ZE (Element *)0
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 */
204 #define Nhash 255 /* slots in symbol hash-table */
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 */
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 */
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 */
222 #define SOMETHINGBIG 65536
223 #define RATHERSMALL 512
226 #define max(a,b) (((a)<(b)) ? (b) : (a))
229 enum { INIV
, PUTV
, LOGV
}; /* for pangen[14].c */
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
*);
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
*);
247 ProcList
*ready(Symbol
*, Lextok
*, Sequence
*, int, Lextok
*);
249 SeqList
*seqlist(Sequence
*, SeqList
*);
250 Sequence
*close_seq(int);
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
*);
258 char *emalloc(size_t);
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
*);
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
*);
283 int isproctype(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
*);
294 int qrecv(Lextok
*, int);
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
*);
309 void AST_track(Lextok
*, int);
310 void add_seq(Lextok
*);
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);
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
[]);
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);
372 void putsrc(Element
*);
373 void putstmnt(FILE *, Lextok
*, int);
374 void putunames(FILE *);
376 void runnable(ProcList
*, int, int);
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 *);
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);
400 void varcheck(Element
*, Element
*);
403 void yyerror(char *, ...);
This page took 0.039224 seconds and 3 git commands to generate.