1 /***** spin: spin.h *****/ 2 3 /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4 /* This software is for educational purposes only. */ 5 /* Permission is given to distribute this code provided that this intro- */ 6 /* ductory message is not removed and no monies are exchanged. */ 7 /* No guarantee is expressed or implied by the distribution of this code. */ 8 /* Software written by Gerard J. Holzmann as part of the book: */ 9 /* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */ 10 /* Prentice Hall, Englewood Cliffs, NJ, 07632. */ 11 /* Send bug-reports and/or questions to: gerard@research.att.com */ 12 13 #include <stdio.h> 14 #include <string.h> 15 #define Version "Spin Version 2.2.2 -- 24 February 1995" 16 17 typedef struct Lextok { 18 unsigned short ntyp; /* node type */ 19 short ismtyp; /* CONST derived from MTYP */ 20 int val; /* value attribute */ 21 int ln; /* line number */ 22 int indstep; /* part of d_step sequence */ 23 struct Symbol *fn; /* file name */ 24 struct Symbol *sym; /* fields 1,4-7 used as union */ 25 struct Sequence *sq; /* sequence */ 26 struct SeqList *sl; /* sequence list */ 27 struct Lextok *lft, *rgt; /* children in parse tree */ 28 } Lextok; 29 30 typedef struct Symbol { 31 char *name; 32 int Nid; /* unique number for the name */ 33 short type; /* bit,short,.., chan,struct */ 34 short hidden; /* 1 if outside statevector */ 35 int nel; /* 1 if scalar, >1 if array */ 36 int setat; /* last depth value changed */ 37 int *val; /* runtime value(s), initl 0 */ 38 struct Lextok **Sval; /* values for structures */ 39 40 int xu; /* exclusive r or w by 1 pid */ 41 struct Symbol *xup[2]; /* xr or xs proctype */ 42 43 struct Lextok *ini; /* initial value, or chan-def */ 44 struct Lextok *Slst; /* template for structure if struct */ 45 struct Symbol *Snm; /* name of the defining struct */ 46 struct Symbol *owner; /* set for names of subfields in typedefs */ 47 struct Symbol *context; /* 0 if global, or procname */ 48 struct Symbol *next; /* linked list */ 49 } Symbol; 50 51 typedef struct Queue { 52 short qid; /* runtime q index */ 53 short qlen; /* nr messages stored */ 54 short nslots, nflds; /* capacity, flds/slot */ 55 int setat; /* last depth value changed */ 56 int *fld_width; /* type of each field */ 57 int *contents; /* the actual buffer */ 58 struct Queue *nxt; /* linked list */ 59 } Queue; 60 61 typedef struct Element { 62 Lextok *n; /* defines the type & contents */ 63 int Seqno; /* identifies this el within system */ 64 int seqno; /* identifies this el within a proc */ 65 unsigned char status; /* used by analyzer generator */ 66 struct SeqList *sub; /* subsequences, for compounds */ 67 struct SeqList *esc; /* zero or more escape sequences */ 68 struct Element *Nxt; /* linked list - for global lookup */ 69 struct Element *nxt; /* linked list - program structure */ 70 } Element; 71 72 typedef struct Sequence { 73 Element *frst; 74 Element *last; /* links onto continuations */ 75 Element *extent; /* last element in original */ 76 int maxel; /* 1+largest id in the sequence */ 77 } Sequence; 78 79 typedef struct SeqList { 80 Sequence *this; /* one sequence */ 81 struct SeqList *nxt; /* linked list */ 82 } SeqList; 83 84 typedef struct Label { 85 Symbol *s; 86 Symbol *c; 87 Element *e; 88 struct Label *nxt; 89 } Label; 90 91 typedef struct Lbreak { 92 Symbol *l; 93 struct Lbreak *nxt; 94 } Lbreak; 95 96 typedef struct RunList { 97 Symbol *n; /* name */ 98 int tn; /* ordinal of type */ 99 int pid; /* process id */ 100 Element *pc; /* current stmnt */ 101 Sequence *ps; /* used by analyzer generator */ 102 Symbol *symtab; /* local variables */ 103 struct RunList *nxt; /* linked list */ 104 } RunList; 105 106 typedef struct ProcList { 107 Symbol *n; /* name */ 108 Lextok *p; /* parameters */ 109 Sequence *s; /* body */ 110 int tn; /* ordinal number */ 111 struct ProcList *nxt; /* linked list */ 112 } ProcList; 113 114 typedef Lextok *Lexptr; 115 116 #define YYSTYPE Lexptr 117 118 #define ZN (Lextok *)0 119 #define ZS (Symbol *)0 120 #define ZE (Element *)0 121 122 #define DONE 1 /* status bits of elements */ 123 #define ATOM 2 /* part of an atomic chain */ 124 #define L_ATOM 4 /* last element in a chain */ 125 #define I_GLOB 8 /* inherited global ref */ 126 #define DONE2 16 /* used in putcode and main*/ 127 #define D_ATOM 32 /* deterministic atomic */ 128 #define CHECK1 64 129 #define CHECK2 128 130 131 #define Nhash 255 /* slots in symbol hash-table */ 132 133 #define XR 1 /* non-shared receive-only */ 134 #define XS 2 /* non-shared send-only */ 135 #define XX 4 /* overrides XR or XS tag */ 136 137 #define PREDEF 3 /* predefined names: _p, _last */ 138 #define BIT 1 /* also equal to width in bits */ 139 #define BYTE 8 /* ditto */ 140 #define SHORT 16 /* ditto */ 141 #define INT 32 /* ditto */ 142 #define CHAN 64 /* not */ 143 #define STRUCT 128 /* user defined structure name */ 144 145 #define max(a,b) (((a)<(b)) ? (b) : (a)) 146 147 /***** ANSI C - prototype definitions *****/ 148 Element *colons(Lextok *); 149 Element *eval_sub(Element *); 150 Element *get_lab(Lextok *, int); 151 Element *huntele(Element *, int); 152 Element *huntstart(Element *); 153 Element *if_seq(Lextok *); 154 Element *new_el(Lextok *); 155 Element *target(Element *); 156 Element *unless_seq(Lextok *); 157 158 Lextok *cpnn(Lextok *, int, int, int); 159 Lextok *do_unless(Lextok *, Lextok *); 160 Lextok *expand(Lextok *, int); 161 Lextok *getuname(Symbol *); 162 Lextok *mk_explicit(Lextok *, int, int); 163 Lextok *nn(Lextok *, int, Lextok *, Lextok *); 164 Lextok *rem_lab(Symbol *, Lextok *, Symbol *); 165 Lextok *tail_add(Lextok *, Lextok *); 166 167 ProcList *ready(Symbol *, Lextok *, Sequence *); 168 169 SeqList *seqlist(Sequence *, SeqList *); 170 Sequence *close_seq(int); 171 172 Symbol *break_dest(void); 173 Symbol *findloc(Symbol *); 174 Symbol *has_lab(Element *); 175 Symbol *lookup(char *); 176 177 char *emalloc(int); 178 long time(long *); 179 180 int a_rcv(Queue *, Lextok *, int); 181 int a_snd(Queue *, Lextok *); 182 int any_oper(Lextok *, int); 183 int any_undo(Lextok *); 184 int atoi(char *); 185 int blog(int); 186 int cast_val(int, int); 187 int check_name(char *); 188 int checkvar(Symbol *, int); 189 int Cnt_flds(Lextok *); 190 int cnt_mpars(Lextok *); 191 int complete_rendez(void); 192 int dolocal(int, int, char *); 193 int enable(Symbol *, Lextok *); 194 int Enabled0(Element *); 195 int Enabled1(Lextok *); 196 int eval(Lextok *); 197 int eval_sync(Element *); 198 int fill_struct(Symbol *, int, int, char *, Symbol **); 199 int find_lab(Symbol *, Symbol *); 200 int find_maxel(Symbol *); 201 int fproc(char *); 202 int getglobal(Lextok *); 203 int getlocal(Lextok *); 204 int getval(Lextok *); 205 int getweight(Lextok *); 206 int has_global(Lextok *); 207 int has_typ(Lextok *, int); 208 int hash(char *); 209 int interprint(Lextok *); 210 int ismtype(char *); 211 int isproctype(char *); 212 int isutype(char *); 213 int Lval_struct(Lextok *, Symbol *, int, int); 214 int newer(char *, char *); 215 int pc_value(Lextok *); 216 int putcode(FILE *, Sequence *, Element *, int); 217 int puttype(int); 218 int q_is_sync(Lextok *); 219 int qlen(Lextok *); 220 int qfull(Lextok *); 221 int qmake(Symbol *); 222 int qrecv(Lextok *, int); 223 int qsend(Lextok *); 224 int Rval_struct(Lextok *, Symbol *, int); 225 int remotelab(Lextok *); 226 int remotevar(Lextok *); 227 int sa_snd(Queue *, Lextok *); 228 int s_snd(Queue *, Lextok *); 229 int scan_seq(Sequence *); 230 int setglobal(Lextok *, int); 231 int setlocal(Lextok *, int); 232 int setval(Lextok *, int); 233 int sputtype(char *, int); 234 int Sym_typ(Lextok *); 235 int symbolic(FILE *, Lextok *); 236 int Width_set(int *, int, Lextok *); 237 int yyparse(void); 238 int yywrap(void); 239 int yylex(void); 240 long Rand(void); 241 242 void add_el(Element *, Sequence *); 243 void add_seq(Lextok *); 244 void addsymbol(RunList *, Symbol *); 245 void attach_escape(Sequence *, Sequence *); 246 void check_proc(Lextok *, int); 247 void comment(FILE *, Lextok *, int); 248 void comwork(FILE *, Lextok *, int); 249 void cross_dsteps(Lextok *, Lextok *); 250 void do_init(Symbol *); 251 void do_var(int, char *, Symbol *); 252 void doglobal(int); 253 void dohidden(void); 254 void doq(Symbol *, int, RunList *); 255 void dump_struct(Symbol *, char *, RunList *); 256 void dumpclaims(FILE *, int, char *); 257 void dumpglobals(void); 258 void dumplabels(void); 259 void dumplocal(RunList *); 260 void dumpskip(int, int); 261 void dumpsrc(int, int); 262 void end_labs(Symbol *, int); 263 void exit(int); 264 void explain(int); 265 void fatal(char *, char *); 266 void full_name(FILE *, Lextok *, Symbol *, int); 267 void fix_dest(Symbol *, Symbol *); 268 void genaddproc(void); 269 void genaddqueue(void); 270 void genconditionals(void); 271 void genheader(void); 272 void genother(void); 273 void gensrc(void); 274 void genunio(void); 275 void ini_struct(Symbol *); 276 void lost_trail(void); 277 void main(int, char **); 278 void make_atomic(Sequence *, int); 279 void mark_seq(Sequence *); 280 void match_trail(void); 281 void mov_lab(Symbol *, Element *, Element *); 282 void ncases(FILE *, int, int, int, char **); 283 void non_fatal(char *, char *); 284 void ntimes(FILE *, int, int, char *c[]); 285 void open_seq(int); 286 void p_talk(Element *, int); 287 void patch_atomic(Sequence *); 288 void pushbreak(void); 289 void put_pinit(Element *, Symbol *, Lextok *, int); 290 void put_ptype(char *, int, int, int); 291 void put_seq(Sequence *, int, int); 292 void putCode(FILE *, Element *, Element *, Element *, int); 293 void putname(FILE *, char *, Lextok *, int, char *); 294 void putnr(int); 295 void putproc(Symbol *, Sequence *, int, int, int); 296 void putremote(FILE *, Lextok *, int); 297 void putskip(int); 298 void putsrc(int, int); 299 void putstmnt(FILE *, Lextok *, int); 300 void putunames(FILE *); 301 void rem_Seq(void); 302 void runnable(ProcList *); 303 void sched(void); 304 void set_lab(Symbol *, Element *); 305 void setmtype(Lextok *); 306 void setparams(RunList *, ProcList *, Lextok *); 307 void setpname(Lextok *); 308 void setptype(Lextok *, int, Lextok *); /* predefined types */ 309 void setuname(Lextok *); /* userdefined types */ 310 void setutype(Lextok *, Symbol *, Lextok *); 311 void setxus(Lextok *, int); 312 void sr_mesg(int, int); 313 void sr_talk(Lextok *, int, char *, char *, int, Queue *); 314 void Srand(unsigned); 315 void start_claim(int); 316 void symdump(void); 317 void formdump(void); 318 void struct_name(Lextok *, Symbol *, int); 319 void symvar(Symbol *); 320 void talk(RunList *); 321 void typ_ck(int, int, char *); 322 void typ2c(Symbol *); 323 void undostmnt(Lextok *, int); 324 void unrem_Seq(void); 325 void unskip(int); 326 void varcheck(Element *, Element *); 327 void walk_atomic(Element *, Element *, int); 328 void whichproc(int); 329 void whoruns(int); 330 void wrapup(int); 331 void yyerror(char *, ...); 332