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