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