/***** spin: spin.h *****/

/*
* This file is part of the public release of Spin. It is subject to the
* terms in the LICENSE file that is included in this source directory.
* Tool documentation is available at http://spinroot.com
*/

#ifndef SEEN_SPIN_H
#define SEEN_SPIN_H

#include <stdio.h>
#include <string.h>
#include <ctype.h>
#if !defined(WIN32) && !defined(WIN64)
#include <unistd.h>
#endif
#if !defined(PC) && !defined(_PLAN9)
#include <memory.h>
#endif

enum        { INIV, PUTV, LOGV }; /* used in pangen1.c */
enum btypes { NONE, N_CLAIM, I_PROC, A_PROC, P_PROC, E_TRACE, N_TRACE };

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 */
       int     uiid;           /* inline id, if non-zero */
       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 */
       unsigned char   isarray; /* set if decl specifies array bound */
       unsigned char   *bscp;  /* block scope */
       int     sc;             /* scope seq no -- set only for proctypes */
       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 int    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     minel;          /* minimum Seqno, set and used only in guided.c */
       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     uiid;           /* non-zero if label appears in an inline */
       int     visible;        /* label referenced in claim (slice relevant) */
       struct Label    *nxt;
} Label;

typedef struct Lbreak {
       Symbol  *l;
       struct Lbreak   *nxt;
} Lbreak;

typedef struct L_List {
       Lextok *n;
       struct L_List   *nxt;
} L_List;

typedef struct RunList {
       Symbol  *n;             /* name            */
       int     tn;             /* ordinal of type */
       int     pid;            /* process id      */
       int     priority;       /* for simulations only */
       enum btypes b;          /* the type of process */
       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 */
       enum btypes b;          /* e.g., claim, trace, proc */
       short   tn;             /* ordinal number */
       unsigned char   det;    /* deterministic */
       unsigned char   unsafe; /* contains global var inits */
       unsigned char   priority; /* process priority, if any */
       struct ProcList *nxt;   /* linked list */
} ProcList;

typedef struct QH {
       int     n;
       struct  QH *nxt;
} QH;

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             /* status bits for remote ref check */
#define CHECK3  256             /* status bits for atomic jump check */

#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
#define MAXSCOPESZ      1024

#ifndef max
#define max(a,b) (((a)<(b)) ? (b) : (a))
#endif

#ifdef PC
#define MFLAGS "wb"
#else
#define MFLAGS "w"
#endif

/***** prototype definitions *****/
Element *eval_sub(Element *);
Element *get_lab(Lextok *, int);
Element *huntele(Element *, unsigned int, int);
Element *huntstart(Element *);
Element *mk_skip(void);
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 *);
Lextok  *return_statement(Lextok *);

ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *, enum btypes);

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    *put_inline(FILE *, char *);
char    *emalloc(size_t);
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     check_track(Lextok *);
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     is_inline(void);
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     pid_is_claim(int);
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     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_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    disambiguate(void);
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    mark_last(void);
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, const char *c[]);
void    open_seq(int);
void    p_talk(Element *, int);
void    pickup_inline(Symbol *, Lextok *, Lextok *);
void    plunk_c_decls(FILE *);
void    plunk_c_fcts(FILE *);
void    plunk_expr(FILE *, char *);
void    plunk_inline(FILE *, char *, int, int);
void    prehint(Symbol *);
void    preruse(FILE *, Lextok *);
void    pretty_print(void);
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    sync_product(void);
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    whoruns(int);
void    wrapup(int);
void    yyerror(char *, ...);

extern  int unlink(const char *);

#define TMP_FILE1 "._s_p_i_n_"
#define TMP_FILE2 "._n_i_p_s_"

#endif

You are viewing proxied material from sdf.org. The copyright of proxied material belongs to its original authors. Any comments or complaints in relation to proxied material should be directed to the original authors of the content concerned. Please see the disclaimer for more details.