main.c

这是一个同样来自贝尔实验室的和UNIX有着渊源的操作系统, 其简洁的设计和实现易于我们学习和理解

/***** spin: main.c *****/

/* 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: [e-mail]            */

#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"

extern int unlink(const char *);

#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	repro_src(void);
extern void	qhide(int);

Symbol	*Fname, *oFname;

int	Etimeouts;	/* nr timeouts in program */
int	Ntimeouts;	/* nr timeouts in never claim */
int	analyze, columns, dumptab, has_remote, has_remvar;
int	interactive, jumpsteps, m_loss, nr_errs, cutoff;
int	s_trail, ntrail, verbose, xspin, notabs, rvopt;
int	no_print, no_wrapup, Caccess, limited_vis, like_java;
int	separate;	/* separate compilation */
int	export_ast;	/* pangen5.c */
int	inlineonly;	/* show inlined code */
int	seedy;		/* be verbose about chosen seed */

int	dataflow = 1, merger = 1, deadvar = 1, ccache = 1;

static int preprocessonly, SeedUsed;

#if 0
meaning 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 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	"gcc -E -x c"	/* most systems have gcc anyway */
				/* else use "cpp" */
#else
#ifdef SOLARIS
#define CPP	"/usr/ccs/lib/cpp"
#else
#if defined(__FreeBSD__) || defined(__OpenBSD__)
#define CPP	"cpp"
#else
#define CPP	"/bin/cpp"	/* classic Unix systems */
#endif
#endif
#endif

#endif
static char	*PreProc = CPP;
extern int	depth; /* at least some steps were made */

void
alldone(int estatus)
{
	if (preprocessonly == 0
	&&  strlen(out1) > 0)
		(void) unlink((const char *)out1);

	if (seedy && !analyze && !export_ast
	&& !s_trail && !preprocessonly && depth > 0)
		printf("seed used: %d\n", SeedUsed);

	if (xspin && (analyze || s_trail))
	{	if (estatus)
			printf("spin: %d error(s) - aborting\n",
			estatus);
		else
			printf("Exit-Status 0\n");
	}
	exit(estatus);
}

void
preprocess(char *a, char *b, int a_tmp)
{	char precmd[512], cmd[1024]; int i;
#ifdef PC
	extern int try_zpp(char *, char *);
	if (PreCnt == 0 && 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);
		fprintf(stdout, "spin: preprocessing failed\n");	/* 4.1.2 was stderr */
		alldone(1); /* no return, error exit */
	}
#ifdef PC
out:
#endif
	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;
}

void
usage(void)
{
	printf("use: spin [-option] ... [-option] file\n");
	printf("\tNote: file must always be the last argument\n");
	printf("\t-A apply slicing algorithm\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 (combine with -g etc.)\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-h  at end of run, print value of seed for random nr generator used\n");
	printf("\t-i interactive (random simulation)\n");
	printf("\t-I show result of inlining and preprocessing\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 don't hide write-only variables 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-S1 and -S2 separate pan source for claim and model\n");
	printf("\t-s print send events\n");
	printf("\t-T do not indent printf output\n");
	printf("\t-t[N] follow [Nth] simulation trail\n");
	printf("\t-Uyyy pass -Uyyy to the preprocessor\n");
	printf("\t-uN stop a simulation run after N steps\n");
	printf("\t-v verbose, more warnings\n");
	printf("\t-w very verbose (when combined with -l or -g)\n");
	printf("\t-[XYZ] reserved for use by xspin interface\n");
	printf("\t-V print version number and exit\n");
	alldone(1);
}

void
optimizations(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;
	}
}

#if 0
static int
Rename(const char *old, char *new)
{	FILE *fo, *fn;
	char buf[1024];

	if ((fo = fopen(old, "r")) == NULL)
	{	printf("spin: cannot open %s\n", old);
		return 1;
	}
	if ((fn = fopen(new, "w")) == NULL)
	{	printf("spin: cannot create %s\n", new);
		fclose(fo);
		return 2;
	}
	while (fgets(buf, 1024, fo))
		fputs(buf, fn);

	fclose(fo);
	fclose(fn);

	return 0;	/* success */
}
#endif

int
main(int argc, char *argv[])
{	Symbol *s;
	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 'A': export_ast = 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;	/* define */
		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 'h': seedy = 1; break;
		case 'i': interactive = 1; break;
		case 'I': inlineonly = 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': notabs = 1; break;
		case 't': s_trail  =  1;
			  if (isdigit(argv[1][2]))
				ntrail = atoi(&argv[1][2]);
			  break;
		case 'U': PreArg[++PreCnt] = (char *) &argv[1][0];
			  break;	/* undefine */
		case 'u': cutoff = atoi(&argv[1][2]); break;	/* new 3.4.14 */
		case 'v': verbose += 32; break;
		case 'V': printf("%s\n", Version);
			  alldone(0);
			  break;
		case 'w': verbose += 64; break;
		case 'X': xspin = notabs = 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];

		/* must remain in current dir */
		strcpy(out1, "pan.pre");

		if (add_ltl || nvr_file)
			strcpy(out2, "pan.___");

		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)