--- /dev/null
+/***** spin: spin.h *****/
+
+/* Copyright (c) 1989-2007 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>
+#ifndef PC
+#include <memory.h>
+#endif
+
+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 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 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 */
+ unsigned char det; /* deterministic */
+ unsigned char unsafe; /* contains global var inits */
+ 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 /* 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
+
+#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(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 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
projects / lttv.git / blobdiff