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