/***** spin: main.c *****/ /* Copyright (c) 1991-2000 by Lucent Technologies - Bell Laboratories     *//* All Rights Reserved.  This software is for educational purposes only.  *//* Permission is given to distribute this code provided that this intro-  *//* ductory message is not removed and no monies are exchanged.            *//* No guarantee is expressed or implied by the distribution of this code. *//* Software written by Gerard J. Holzmann as part of the book:            *//* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4,     *//* Prentice Hall, Englewood Cliffs, NJ, 07632.                            *//* Send bug-reports and/or questions to: gerard@research.bell-labs.com    */ #include <stdlib.h>#include "spin.h"#include "version.h"#include <signal.h>/* #include <malloc.h> */#include <time.h>#ifdef PC#include <io.h>#include "y_tab.h"#else#include <unistd.h>#include "y.tab.h"#endif extern int	DstepStart, lineno, tl_terse;extern FILE	*yyin, *yyout, *tl_out;extern Symbol	*context;extern char	*claimproc;extern void	qhide(int); Symbol	*Fname, *oFname; int	Etimeouts=0;	/* nr timeouts in program */int	Ntimeouts=0;	/* nr timeouts in never claim */int	analyze=0, columns=0, dumptab=0, has_remote=0;int	interactive=0, jumpsteps=0, m_loss=0, nr_errs=0;int	s_trail=0, ntrail=0, verbose=0, xspin=0, no_print=0, no_wrapup = 0, Caccess=0;int	limited_vis=0, like_java=0;int	dataflow = 1, merger = 1, deadvar = 1, rvopt = 0, ccache = 1;int	separate = 0;	/* separate compilation option */#if 0meaning of flags on verbose:	1	-g global variable values	2	-l local variable values	4	-p all process actions	8	-r receives	16	-s sends	32	-v verbose	64	-w very verbose#endif static Element	*Same;static int	IsAsgn = 0, OrIsAsgn = 0;static char	Operator[] = "operator: ";static char	Keyword[]  = "keyword: ";static char	Function[] = "function-name: ";static char	**add_ltl  = (char **)0;static char	**ltl_file = (char **)0;static char	**nvr_file = (char **)0;static char	*PreArg[64];static int	PreCnt = 0;static char	out1[64];static void	explain(int); #ifndef CPP		/* OS2:		"spin -Picc -E/Pd+ -E/Q+"    */		/* Visual C++:	"spin -PCL  -E/E             */#ifdef PC#define CPP	"cpp"		/*  or specify a full path    */#else#ifdef SOLARIS#define CPP	"/usr/ccs/lib/cpp"#else#ifdef __FreeBSD__#define CPP	"cpp"#else#define CPP	"/bin/cpp"#endif#endif#endif #endifstatic char	*PreProc = CPP; voidalldone(int estatus){	if (strlen(out1) > 0)		(void) unlink((const char *)out1);	if (xspin && (analyze || s_trail))	{	if (estatus)			printf("spin: %d error(s) - aborting\n",			estatus);		else			printf("Exit-Status 0\n");	}	exit(estatus);} voidpreprocess(char *a, char *b, int a_tmp){	char precmd[128], cmd[256]; int i;#ifdef PC	extern int try_zpp(char *, char *);	if (try_zpp(a, b)) goto out;#endif	strcpy(precmd, PreProc);	for (i = 1; i <= PreCnt; i++)	{	strcat(precmd, " ");		strcat(precmd, PreArg[i]);	}	sprintf(cmd, "%s %s > %s", precmd, a, b);	if (system((const char *)cmd))	{	(void) unlink((const char *) b);		if (a_tmp) (void) unlink((const char *) a);		alldone(1); /* failed */	}out:	if (a_tmp) (void) unlink((const char *) a);} FILE *cpyfile(char *src, char *tgt){	FILE *inp, *out;	char buf[1024]; 	inp = fopen(src, "r");	out = fopen(tgt, "w");	if (!inp || !out)	{	printf("spin: cannot cp %s to %s\n", src, tgt);		alldone(1);	}	while (fgets(buf, 1024, inp))		fprintf(out, "%s", buf);	fclose(inp);	return out;} voidusage(void){	printf("use: spin [-option] ... [-option] file\n");	printf("\tNote: file must always be the last argument\n");	printf("\t-a generate a verifier in pan.c\n");	printf("\t-B no final state details in simulations\n");	printf("\t-b don't execute printfs in simulation\n");	printf("\t-C print channel access info (structview)\n");	printf("\t-c columnated -s -r simulation output\n");	printf("\t-d produce symbol-table information\n");	printf("\t-Dyyy pass -Dyyy to the preprocessor\n");	printf("\t-Eyyy pass yyy to the preprocessor\n");	printf("\t-f \"..formula..\"  translate LTL ");	printf("into never claim\n");	printf("\t-F file  like -f, but with the LTL ");	printf("formula stored in a 1-line file\n");	printf("\t-g print all global variables\n");	printf("\t-i interactive (random simulation)\n");	printf("\t-J reverse eval order of nested unlesses\n");	printf("\t-jN skip the first N steps ");	printf("in simulation trail\n");	printf("\t-l print all local variables\n");	printf("\t-M print msc-flow in Postscript\n");	printf("\t-m lose msgs sent to full queues\n");	printf("\t-N file use never claim stored in file\n");	printf("\t-nN seed for random nr generator\n");	printf("\t-o1 turn off dataflow-optimizations in verifier\n");	printf("\t-o2 turn off dead variables elimination in verifier\n");	printf("\t-o3 turn off statement merging in verifier\n");	printf("\t-Pxxx use xxx for preprocessing\n");	printf("\t-p print all statements\n");	printf("\t-qN suppress io for queue N in printouts\n");	printf("\t-r print receive events\n");	printf("\t-s print send events\n");	printf("\t-v verbose, more warnings\n");	printf("\t-w very verbose (when combined with -l or -g)\n");	printf("\t-t[N] follow [Nth] simulation trail\n");	printf("\t-[XYZ] reserved for use by xspin interface\n");	printf("\t-V print version number and exit\n");	alldone(1);} voidoptimizations(char nr){	switch (nr) {	case '1':		dataflow = 1 - dataflow; /* dataflow */		if (verbose&32)		printf("spin: dataflow optimizations turned %s\n",			dataflow?"on":"off");		break;	case '2':		/* dead variable elimination */		deadvar = 1 - deadvar;		if (verbose&32)		printf("spin: dead variable elimination turned %s\n",			deadvar?"on":"off");		break;	case '3':		/* statement merging */		merger = 1 - merger;		if (verbose&32)		printf("spin: statement merging turned %s\n",			merger?"on":"off");		break; 	case '4':		/* rv optimization */		rvopt = 1 - rvopt;		if (verbose&32)		printf("spin: rendezvous optimization turned %s\n",			rvopt?"on":"off");		break;	case '5':		/* case caching */		ccache = 1 - ccache;		if (verbose&32)		printf("spin: case caching turned %s\n",			ccache?"on":"off");		break;	default:		printf("spin: bad or missing parameter on -o\n");		usage();		break;	}} intmain(int argc, char *argv[]){	Symbol *s; int preprocessonly = 0;	int T = (int) time((time_t *)0);	int usedopts = 0;	extern void ana_src(int, int); 	yyin  = stdin;	yyout = stdout;	tl_out = stdout; 	/* unused flags: e, w, x, y, z, A, G, I, L, O, Q, R, S, T, W */	while (argc > 1 && argv[1][0] == '-')	{	switch (argv[1][1]) { 		/* generate code for separate compilation: S1 or S2 */		case 'S': separate = atoi(&argv[1][2]);			  /* fall through */ 		case 'a': analyze  = 1; break;		case 'B': no_wrapup = 1; break;		case 'b': no_print = 1; break;		case 'C': Caccess = 1; break;		case 'c': columns = 1; break;		case 'D': PreArg[++PreCnt] = (char *) &argv[1][0];			  break;		case 'd': dumptab =  1; break;		case 'E': PreArg[++PreCnt] = (char *) &argv[1][2];			  break;		case 'F': ltl_file = (char **) (argv+2);			  argc--; argv++; break;		case 'f': add_ltl = (char **) argv;			  argc--; argv++; break;		case 'g': verbose +=  1; break;		case 'i': interactive = 1; break;		case 'J': like_java = 1; break;		case 'j': jumpsteps = atoi(&argv[1][2]); break;		case 'l': verbose +=  2; break;		case 'M': columns = 2; break;		case 'm': m_loss   =  1; break;		case 'N': nvr_file = (char **) (argv+2);			  argc--; argv++; break;		case 'n': T = atoi(&argv[1][2]); tl_terse = 1; break;		case 'o': optimizations(argv[1][2]);			  usedopts = 1; break;		case 'P': PreProc = (char *) &argv[1][2]; break;		case 'p': verbose +=  4; break;		case 'q': if (isdigit(argv[1][2]))				qhide(atoi(&argv[1][2]));			  break;		case 'r': verbose +=  8; break;		case 's': verbose += 16; break;		case 't': s_trail  =  1;			  if (isdigit(argv[1][2]))				ntrail = atoi(&argv[1][2]);			  break;		case 'v': verbose += 32; break;		case 'V': printf("%s\n", Version);			  alldone(0);			  break;		case 'w': verbose += 64; break;		case 'X': xspin = 1;#ifndef PC			  signal(SIGPIPE, alldone); /* not posix... */#endif			  break;		case 'Y': limited_vis = 1; break;	/* used by xspin */		case 'Z': preprocessonly = 1; break;	/* used by xspin */ 		default : usage(); break;		}		argc--, argv++;	}	if (usedopts && !analyze)		printf("spin: warning -o[123] option ignored in simulations\n");		if (ltl_file)	{	char formula[4096];		add_ltl = ltl_file-2; add_ltl[1][1] = 'f';		if (!(tl_out = fopen(*ltl_file, "r")))		{	printf("spin: cannot open %s\n", *ltl_file);			alldone(1);		}		fgets(formula, 4096, tl_out);		fclose(tl_out);		tl_out = stdout;		*ltl_file = (char *) formula;	}	if (argc > 1)	{	char cmd[128], out2[64];#ifdef PC		strcpy(out1, "_tmp1_");		strcpy(out2, "_tmp2_");#else		/* extern char *tmpnam(char *);  in stdio.h */		if (add_ltl || nvr_file)		{	/* must remain in current dir */			strcpy(out1, "_tmp1_");			strcpy(out2, "_tmp2_");		} else		{	(void) tmpnam(out1);			(void) tmpnam(out2);		}#endif		if (add_ltl)		{	tl_out = cpyfile(argv[1], out2);			nr_errs = tl_main(2, add_ltl);	/* in tl_main.c */			fclose(tl_out);			preprocess(out2, out1, 1);		} else if (nvr_file)		{	FILE *fd; char buf[1024];						if ((fd = fopen(*nvr_file, "r")) == NULL)			{	printf("spin: cannot open %s\n",					*nvr_file);				alldone(1);			}			tl_out = cpyfile(argv[1], out2);			while (fgets(buf, 1024, fd))				fprintf(tl_out, "%s", buf);			fclose(tl_out);			fclose(fd);			preprocess(out2, out1, 1);		} else			preprocess(argv[1], out1, 0); 		if (preprocessonly)		{	(void) unlink("pan.pre"); /* remove old version */			if (rename((const char *) out1, "pan.pre") != 0)			{	printf("spin: rename %s failed\n", out1);				alldone(1);			}			alldone(0);		}		if (!(yyin = fopen(out1, "r")))		{	printf("spin: cannot open %s\n", out1);			alldone(1);		} 		if (strncmp(argv[1], "progress", 8) == 0		||  strncmp(argv[1], "accept", 6) == 0)			sprintf(cmd, "_%s", argv[1]);		else			strcpy(cmd, argv[1]);		oFname = Fname = lookup(cmd);		if (oFname->name[0] == '\"')		{	int i = strlen(oFname->name);			oFname->name[i-1] = '\0';			oFname = lookup(&oFname->name[1]);		}	} else	{	oFname = Fname = lookup("<stdin>");		if (add_ltl)		{	if (argc > 0)				exit(tl_main(2, add_ltl));			printf("spin: missing argument to -f\n");			alldone(1);		}		printf("%s\n", Version);		printf("reading input from stdin:\n");		fflush(stdout);	}	if (columns == 2)	{	extern void putprelude(void);		if (xspin || verbose&(1|4|8|16|32))		{	printf("spin: -c precludes all flags except -t\n");			alldone(1);		}		putprelude();	}	if (columns && !(verbose&8) && !(verbose&16))		verbose += (8+16);	if (columns == 2 && limited_vis)		verbose += (1+4);	Srand(T);	/* defined in run.c */	s = lookup("_");	s->type = PREDEF; /* a write only global var */	s = lookup("_p");	s->type = PREDEF;	s = lookup("_pid");	s->type = PREDEF;	s = lookup("_last");	s->type = PREDEF;	s = lookup("_nr_pr");	s->type = PREDEF; /* new 3.3.10 */	yyparse();	fclose(yyin);	chanaccess();	if (!s_trail && (dataflow || merger))		ana_src(dataflow, merger);	sched();	alldone(nr_errs);	return 0;	/* can't get here */} intyywrap(void)	/* dummy routine */{	return 1;} voidnon_fatal(char *s1, char *s2){	extern char yytext[]; 	printf("spin: line %3d %s, Error: ",		lineno, Fname?Fname->name:"nofilename");	if (s2)		printf(s1, s2);	else		printf(s1);#if 0	if (yychar != -1 && yychar != 0)	{	printf("	saw '");		explain(yychar);		printf("'");	}#endif	if (yytext && strlen(yytext)>1)		printf(" near '%s'", yytext);	printf("\n");	nr_errs++;} voidfatal(char *s1, char *s2){	non_fatal(s1, s2);	alldone(1);} char *emalloc(int n){	char *tmp; 	if (!(tmp = (char *) malloc(n)))		fatal("not enough memory", (char *)0);	memset(tmp, 0, n);	return tmp;} voidtrapwonly(Lextok *n, char *s){	extern int realread;	short i = (n->sym)?n->sym->type:0; 	if (i != MTYPE	&&  i != BIT	&&  i != BYTE	&&  i != SHORT	&&  i != INT	&&  i != UNSIGNED)		return; 	if (realread)	n->sym->hidden |= 32;	/* var is read at least once */} voidsetaccess(Symbol *sp, Symbol *what, int cnt, int t){	Access *a; 	for (a = sp->access; a; a = a->lnk)		if (a->who == context		&&  a->what == what		&&  a->cnt == cnt		&&  a->typ == t)			return; 	a = (Access *) emalloc(sizeof(Access));	a->who = context;	a->what = what;	a->cnt = cnt;	a->typ = t;	a->lnk = sp->access;	sp->access = a;}

Lines 1–500 of 675. Load more