Subversion Repositories planix.SVN

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

/* Copyright (c) 1989-2009 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>

enum	    { INIV, PUTV, LOGV };	/* for pangen[14].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	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	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 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 */

	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

#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 *, 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 *, 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	*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	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	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	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	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, 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	show_lab(void);

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	varcheck(Element *, Element *);

void	whoruns(int);

void	wrapup(int);

void	yyerror(char *, ...);

#endif