sys/src/cmd/spin/spin.h

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