trunk/verif/Spin/Src5.1.6/spin.h

   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