| 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 |