123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399 |
- /***** spin: spin.h *****/
- /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
- /* All Rights Reserved. This software is for educational purposes only. */
- /* No guarantee whatsoever is expressed or implied by the distribution of */
- /* this code. Permission is given to distribute this code provided that */
- /* this introductory message is not removed and no monies are exchanged. */
- /* Software written by Gerard J. Holzmann. For tool documentation see: */
- /* http://spinroot.com/ */
- /* Send all bug-reports and/or questions to: bugs@spinroot.com */
- #ifndef SEEN_SPIN_H
- #define SEEN_SPIN_H
- #include <stdio.h>
- #include <string.h>
- #include <ctype.h>
- typedef struct Lextok {
- unsigned short ntyp; /* node type */
- short ismtyp; /* CONST derived from MTYP */
- int val; /* value attribute */
- int ln; /* line number */
- int indstep; /* part of d_step sequence */
- struct Symbol *fn; /* file name */
- struct Symbol *sym; /* symbol reference */
- struct Sequence *sq; /* sequence */
- struct SeqList *sl; /* sequence list */
- struct Lextok *lft, *rgt; /* children in parse tree */
- } Lextok;
- typedef struct Slicer {
- Lextok *n; /* global var, usable as slice criterion */
- short code; /* type of use: DEREF_USE or normal USE */
- short used; /* set when handled */
- struct Slicer *nxt; /* linked list */
- } Slicer;
- typedef struct Access {
- struct Symbol *who; /* proctype name of accessor */
- struct Symbol *what; /* proctype name of accessed */
- int cnt, typ; /* parameter nr and, e.g., 's' or 'r' */
- struct Access *lnk; /* linked list */
- } Access;
- typedef struct Symbol {
- char *name;
- int Nid; /* unique number for the name */
- unsigned short type; /* bit,short,.., chan,struct */
- unsigned char hidden; /* bit-flags:
- 1=hide, 2=show,
- 4=bit-equiv, 8=byte-equiv,
- 16=formal par, 32=inline par,
- 64=treat as if local; 128=read at least once
- */
- unsigned char colnr; /* for use with xspin during simulation */
- int nbits; /* optional width specifier */
- int nel; /* 1 if scalar, >1 if array */
- int setat; /* last depth value changed */
- int *val; /* runtime value(s), initl 0 */
- Lextok **Sval; /* values for structures */
- int xu; /* exclusive r or w by 1 pid */
- struct Symbol *xup[2]; /* xr or xs proctype */
- struct Access *access;/* e.g., senders and receives of chan */
- Lextok *ini; /* initial value, or chan-def */
- Lextok *Slst; /* template for structure if struct */
- struct Symbol *Snm; /* name of the defining struct */
- struct Symbol *owner; /* set for names of subfields in typedefs */
- struct Symbol *context; /* 0 if global, or procname */
- struct Symbol *next; /* linked list */
- } Symbol;
- typedef struct Ordered { /* links all names in Symbol table */
- struct Symbol *entry;
- struct Ordered *next;
- } Ordered;
- typedef struct Queue {
- short qid; /* runtime q index */
- int qlen; /* nr messages stored */
- int nslots, nflds; /* capacity, flds/slot */
- int setat; /* last depth value changed */
- int *fld_width; /* type of each field */
- int *contents; /* the values stored */
- int *stepnr; /* depth when each msg was sent */
- struct Queue *nxt; /* linked list */
- } Queue;
- typedef struct FSM_state { /* used in pangen5.c - dataflow */
- int from; /* state number */
- int seen; /* used for dfs */
- int in; /* nr of incoming edges */
- int cr; /* has reachable 1-relevant successor */
- int scratch;
- unsigned long *dom, *mod; /* to mark dominant nodes */
- struct FSM_trans *t; /* outgoing edges */
- struct FSM_trans *p; /* incoming edges, predecessors */
- struct FSM_state *nxt; /* linked list of all states */
- } FSM_state;
- typedef struct FSM_trans { /* used in pangen5.c - dataflow */
- int to;
- short relevant; /* when sliced */
- short round; /* ditto: iteration when marked */
- struct FSM_use *Val[2]; /* 0=reads, 1=writes */
- struct Element *step;
- struct FSM_trans *nxt;
- } FSM_trans;
- typedef struct FSM_use { /* used in pangen5.c - dataflow */
- Lextok *n;
- Symbol *var;
- int special;
- struct FSM_use *nxt;
- } FSM_use;
- typedef struct Element {
- Lextok *n; /* defines the type & contents */
- int Seqno; /* identifies this el within system */
- int seqno; /* identifies this el within a proc */
- int merge; /* set by -O if step can be merged */
- int merge_start;
- int merge_single;
- short merge_in; /* nr of incoming edges */
- short merge_mark; /* state was generated in merge sequence */
- unsigned char status; /* used by analyzer generator */
- struct FSM_use *dead; /* optional dead variable list */
- struct SeqList *sub; /* subsequences, for compounds */
- struct SeqList *esc; /* zero or more escape sequences */
- struct Element *Nxt; /* linked list - for global lookup */
- struct Element *nxt; /* linked list - program structure */
- } Element;
- typedef struct Sequence {
- Element *frst;
- Element *last; /* links onto continuations */
- Element *extent; /* last element in original */
- int maxel; /* 1+largest id in sequence */
- } Sequence;
- typedef struct SeqList {
- Sequence *this; /* one sequence */
- struct SeqList *nxt; /* linked list */
- } SeqList;
- typedef struct Label {
- Symbol *s;
- Symbol *c;
- Element *e;
- int visible; /* label referenced in claim (slice relevant) */
- struct Label *nxt;
- } Label;
- typedef struct Lbreak {
- Symbol *l;
- struct Lbreak *nxt;
- } Lbreak;
- typedef struct RunList {
- Symbol *n; /* name */
- int tn; /* ordinal of type */
- int pid; /* process id */
- int priority; /* for simulations only */
- Element *pc; /* current stmnt */
- Sequence *ps; /* used by analyzer generator */
- Lextok *prov; /* provided clause */
- Symbol *symtab; /* local variables */
- struct RunList *nxt; /* linked list */
- } RunList;
- typedef struct ProcList {
- Symbol *n; /* name */
- Lextok *p; /* parameters */
- Sequence *s; /* body */
- Lextok *prov; /* provided clause */
- short tn; /* ordinal number */
- short det; /* deterministic */
- struct ProcList *nxt; /* linked list */
- } ProcList;
- typedef Lextok *Lexptr;
- #define YYSTYPE Lexptr
- #define ZN (Lextok *)0
- #define ZS (Symbol *)0
- #define ZE (Element *)0
- #define DONE 1 /* status bits of elements */
- #define ATOM 2 /* part of an atomic chain */
- #define L_ATOM 4 /* last element in a chain */
- #define I_GLOB 8 /* inherited global ref */
- #define DONE2 16 /* used in putcode and main*/
- #define D_ATOM 32 /* deterministic atomic */
- #define ENDSTATE 64 /* normal endstate */
- #define CHECK2 128
- #define Nhash 255 /* slots in symbol hash-table */
- #define XR 1 /* non-shared receive-only */
- #define XS 2 /* non-shared send-only */
- #define XX 4 /* overrides XR or XS tag */
- #define CODE_FRAG 2 /* auto-numbered code-fragment */
- #define CODE_DECL 4 /* auto-numbered c_decl */
- #define PREDEF 3 /* predefined name: _p, _last */
- #define UNSIGNED 5 /* val defines width in bits */
- #define BIT 1 /* also equal to width in bits */
- #define BYTE 8 /* ditto */
- #define SHORT 16 /* ditto */
- #define INT 32 /* ditto */
- #define CHAN 64 /* not */
- #define STRUCT 128 /* user defined structure name */
- #define SOMETHINGBIG 65536
- #define RATHERSMALL 512
- #ifndef max
- #define max(a,b) (((a)<(b)) ? (b) : (a))
- #endif
- enum { INIV, PUTV, LOGV }; /* for pangen[14].c */
- /***** prototype definitions *****/
- Element *eval_sub(Element *);
- Element *get_lab(Lextok *, int);
- Element *huntele(Element *, int, int);
- Element *huntstart(Element *);
- Element *target(Element *);
- Lextok *do_unless(Lextok *, Lextok *);
- Lextok *expand(Lextok *, int);
- Lextok *getuname(Symbol *);
- Lextok *mk_explicit(Lextok *, int, int);
- Lextok *nn(Lextok *, int, Lextok *, Lextok *);
- Lextok *rem_lab(Symbol *, Lextok *, Symbol *);
- Lextok *rem_var(Symbol *, Lextok *, Symbol *, Lextok *);
- Lextok *tail_add(Lextok *, Lextok *);
- ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *);
- SeqList *seqlist(Sequence *, SeqList *);
- Sequence *close_seq(int);
- Symbol *break_dest(void);
- Symbol *findloc(Symbol *);
- Symbol *has_lab(Element *, int);
- Symbol *lookup(char *);
- Symbol *prep_inline(Symbol *, Lextok *);
- char *emalloc(int);
- long Rand(void);
- int any_oper(Lextok *, int);
- int any_undo(Lextok *);
- int c_add_sv(FILE *);
- int cast_val(int, int, int);
- int checkvar(Symbol *, int);
- int Cnt_flds(Lextok *);
- int cnt_mpars(Lextok *);
- int complete_rendez(void);
- int enable(Lextok *);
- int Enabled0(Element *);
- int eval(Lextok *);
- int find_lab(Symbol *, Symbol *, int);
- int find_maxel(Symbol *);
- int full_name(FILE *, Lextok *, Symbol *, int);
- int getlocal(Lextok *);
- int getval(Lextok *);
- int glob_inline(char *);
- int has_typ(Lextok *, int);
- int in_bound(Symbol *, int);
- int interprint(FILE *, Lextok *);
- int printm(FILE *, Lextok *);
- int ismtype(char *);
- int isproctype(char *);
- int isutype(char *);
- int Lval_struct(Lextok *, Symbol *, int, int);
- int main(int, char **);
- int pc_value(Lextok *);
- int proper_enabler(Lextok *);
- int putcode(FILE *, Sequence *, Element *, int, int, int);
- int q_is_sync(Lextok *);
- int qlen(Lextok *);
- int qfull(Lextok *);
- int qmake(Symbol *);
- int qrecv(Lextok *, int);
- int qsend(Lextok *);
- int remotelab(Lextok *);
- int remotevar(Lextok *);
- int Rval_struct(Lextok *, Symbol *, int);
- int setlocal(Lextok *, int);
- int setval(Lextok *, int);
- int sputtype(char *, int);
- int Sym_typ(Lextok *);
- int tl_main(int, char *[]);
- int Width_set(int *, int, Lextok *);
- int yyparse(void);
- int yywrap(void);
- int yylex(void);
- void AST_track(Lextok *, int);
- void add_seq(Lextok *);
- void alldone(int);
- void announce(char *);
- void c_state(Symbol *, Symbol *, Symbol *);
- void c_add_def(FILE *);
- void c_add_loc(FILE *, char *);
- void c_add_locinit(FILE *, int, char *);
- void c_add_use(FILE *);
- void c_chandump(FILE *);
- void c_preview(void);
- void c_struct(FILE *, char *, Symbol *);
- void c_track(Symbol *, Symbol *, Symbol *);
- void c_var(FILE *, char *, Symbol *);
- void c_wrapper(FILE *);
- void chanaccess(void);
- void check_param_count(int, Lextok *);
- void checkrun(Symbol *, int);
- void comment(FILE *, Lextok *, int);
- void cross_dsteps(Lextok *, Lextok *);
- void doq(Symbol *, int, RunList *);
- void dotag(FILE *, char *);
- void do_locinits(FILE *);
- void do_var(FILE *, int, char *, Symbol *, char *, char *, char *);
- void dump_struct(Symbol *, char *, RunList *);
- void dumpclaims(FILE *, int, char *);
- void dumpglobals(void);
- void dumplabels(void);
- void dumplocal(RunList *);
- void dumpsrc(int, int);
- void fatal(char *, char *);
- void fix_dest(Symbol *, Symbol *);
- void genaddproc(void);
- void genaddqueue(void);
- void gencodetable(FILE *);
- void genheader(void);
- void genother(void);
- void gensrc(void);
- void gensvmap(void);
- void genunio(void);
- void ini_struct(Symbol *);
- void loose_ends(void);
- void make_atomic(Sequence *, int);
- void match_trail(void);
- void no_side_effects(char *);
- void nochan_manip(Lextok *, Lextok *, int);
- void non_fatal(char *, char *);
- void ntimes(FILE *, int, int, char *c[]);
- void open_seq(int);
- void p_talk(Element *, int);
- void pickup_inline(Symbol *, Lextok *);
- void plunk_c_decls(FILE *);
- void plunk_c_fcts(FILE *);
- void plunk_expr(FILE *, char *);
- void plunk_inline(FILE *, char *, int);
- void prehint(Symbol *);
- void preruse(FILE *, Lextok *);
- void prune_opts(Lextok *);
- void pstext(int, char *);
- void pushbreak(void);
- void putname(FILE *, char *, Lextok *, int, char *);
- void putremote(FILE *, Lextok *, int);
- void putskip(int);
- void putsrc(Element *);
- void putstmnt(FILE *, Lextok *, int);
- void putunames(FILE *);
- void rem_Seq(void);
- void runnable(ProcList *, int, int);
- void sched(void);
- void setaccess(Symbol *, Symbol *, int, int);
- void set_lab(Symbol *, Element *);
- void setmtype(Lextok *);
- void setpname(Lextok *);
- void setptype(Lextok *, int, Lextok *);
- void setuname(Lextok *);
- void setutype(Lextok *, Symbol *, Lextok *);
- void setxus(Lextok *, int);
- void Srand(unsigned);
- void start_claim(int);
- void struct_name(Lextok *, Symbol *, int, char *);
- void symdump(void);
- void symvar(Symbol *);
- void trackchanuse(Lextok *, Lextok *, int);
- void trackvar(Lextok *, Lextok *);
- void trackrun(Lextok *);
- void trapwonly(Lextok *, char *); /* spin.y and main.c */
- void typ2c(Symbol *);
- void typ_ck(int, int, char *);
- void undostmnt(Lextok *, int);
- void unrem_Seq(void);
- void unskip(int);
- void varcheck(Element *, Element *);
- void whoruns(int);
- void wrapup(int);
- void yyerror(char *, ...);
- #endif
|