/***** spin: main.c *****/ /* * 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 */ #include <stdlib.h>#include <assert.h>#include "spin.h"#include "version.h"#include <sys/types.h>#include <sys/stat.h>#include <signal.h>#include <time.h>#ifdef PC #include <io.h>#else #include <unistd.h>#endif#include "y.tab.h" 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);extern char	CurScope[MAXSCOPESZ];extern short	has_provided, has_code, has_ltl, has_accept;extern int	realread, buzzed; static void	add_comptime(char *);static void	add_runtime(char *); 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	norecompile;	/* main.c */int	old_scope_rules;	/* use pre 5.3.0 rules */int	old_priority_rules;	/* use pre 6.2.0 rules */int	product, Strict;short	replay; int	merger = 1, deadvar = 1, implied_semis = 1;int	ccache = 0; /* oyvind teig: 5.2.0 case caching off by default */ static int preprocessonly, SeedUsed, itsr, itsr_n;static int seedy;	/* be verbose about chosen seed */static int inlineonly;	/* show inlined code */static int dataflow = 1; #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 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	*ltl_claims = (char *) 0;static char	*pan_runtime = "";static char	*pan_comptime = "";static char	formula[4096];static FILE	*fd_ltl = (FILE *) 0;static char	*PreArg[64];static int	PreCnt = 0;static char	out1[64]; char	**trailfilename;	/* new option 'k' */ void	explain(int); #define CPP	"/bin/cpp"	/* sometimes: "/lib/cpp" */ static char	PreProc[512];extern int	depth; /* at least some steps were made */ intWhatSeed(void){	return SeedUsed;} voidfinal_fiddle(void){	char *has_a, *has_l, *has_f; 	/* no -a or -l but has_accept: add -a */	/* no -a or -l in pan_runtime: add -DSAFETY to pan_comptime */	/* -a or -l but no -f then add -DNOFAIR */ 	has_a = strstr(pan_runtime, "-a");	has_l = strstr(pan_runtime, "-l");	has_f = strstr(pan_runtime, "-f"); 	if (!has_l && !has_a && strstr(pan_comptime, "-DNP"))	{	add_runtime("-l");		has_l = strstr(pan_runtime, "-l");	} 	if (!has_a && !has_l	&&  !strstr(pan_comptime, "-DSAFETY"))	{	if (has_accept		&& !strstr(pan_comptime, "-DBFS")		&& !strstr(pan_comptime, "-DNOCLAIM"))		{	add_runtime("-a");			has_a = pan_runtime;		} else		{	add_comptime("-DSAFETY");	}	} 	if ((has_a || has_l) && !has_f	&&  !strstr(pan_comptime, "-DNOFAIR"))	{	add_comptime("-DNOFAIR");	}} static intchange_param(char *t, char *what, int range, int bottom){	char *ptr;	int v; 	assert(range < 1000 && range > 0);	if ((ptr = strstr(t, what)) != NULL)	{	ptr += strlen(what);		if (!isdigit((int) *ptr))		{	return 0;		}		v = atoi(ptr) + 1;	/* was: v = (atoi(ptr)+1)%range */		if (v >= range)		{	v = bottom;		}		if (v >= 100)		{	*ptr++ = '0' + (v/100); v %= 100;			*ptr++ = '0' + (v/10);			*ptr   = '0' + (v%10);		} else if (v >= 10)		{	*ptr++ = '0' + (v/10);			*ptr++ = '0' + (v%10);			*ptr   = ' ';		} else		{	*ptr++ = '0' + v;			*ptr++ = ' ';			*ptr   = ' ';	}	}	return 1;} static voidchange_rs(char *t){	char *ptr;	int cnt = 0;	long v; 	if ((ptr = strstr(t, "-RS")) != NULL)	{	ptr += 3;		/* room for at least 10 digits */		v = Rand()%1000000000L;		while (v/10 > 0)		{	*ptr++ = '0' + v%10;			v /= 10;			cnt++;		}		*ptr++ = '0' + v;		cnt++;		while (cnt++ < 10)		{	*ptr++ = ' ';	}	}} intomit_str(char *in, char *s){	char *ptr = strstr(in, s);	int i, nr = -1; 	if (ptr)	{	for (i = 0; i < (int) strlen(s); i++)		{	*ptr++ = ' ';		}		if (isdigit((int) *ptr))		{	nr = atoi(ptr);			while (isdigit((int) *ptr))			{	*ptr++ = ' ';	}	}	}	return nr;} voidstring_trim(char *t){	int n = strlen(t) - 1; 	while (n > 0 && t[n] == ' ')	{	t[n--] = '\0';	}} inte_system(int v, const char *s){	static int count = 1;	/* v == 0 : checks to find non-linked version of gcc */	/* v == 1 : all other commands */	/* v == 2 : preprocessing the promela input */ 	if (v == 1)	{	if (verbose&(32|64))	/* -v or -w */		{	printf("cmd%02d: %s\n", count++, s);			fflush(stdout);		}		if (verbose&64)		/* only -w */		{	return 0;	/* suppress the call to system(s) */	}	}	return system(s);} voidalldone(int estatus){	char *ptr;#if defined(WIN32) || defined(WIN64)	struct _stat x;#else	struct stat x;#endif	if (preprocessonly == 0 &&  strlen(out1) > 0)	{	(void) unlink((const char *) out1);	} 	(void) unlink(TMP_FILE1);	(void) unlink(TMP_FILE2); 	if (!buzzed && seedy && !analyze && !export_ast	&& !s_trail && !preprocessonly && depth > 0)	{	printf("seed used: %d\n", SeedUsed);	} 	if (!buzzed && xspin && (analyze || s_trail))	{	if (estatus)		{	printf("spin: %d error(s) - aborting\n",				estatus);		} else		{	printf("Exit-Status 0\n");	}	} 	if (buzzed && replay && !has_code && !estatus)	{	extern QH *qh;		QH *j;		int i;		char *tmp = (char *) emalloc(strlen("spin -t") +				strlen(pan_runtime) + strlen(Fname->name) + 8);		pan_runtime = (char *) emalloc(2048);	/* more than enough */		sprintf(pan_runtime, "-n%d ", SeedUsed);		if (jumpsteps)		{	sprintf(&pan_runtime[strlen(pan_runtime)], "-j%d ", jumpsteps);		}		if (trailfilename)		{	sprintf(&pan_runtime[strlen(pan_runtime)], "-k%s ", *trailfilename);		}		if (cutoff)		{	sprintf(&pan_runtime[strlen(pan_runtime)], "-u%d ", cutoff);		}		for (i = 1; i <= PreCnt; i++)		{	strcat(pan_runtime, PreArg[i]);			strcat(pan_runtime, " ");		}		for (j = qh; j; j = j->nxt)		{	sprintf(&pan_runtime[strlen(pan_runtime)], "-q%d ", j->n);		}		if (strcmp(PreProc, CPP) != 0)		{	sprintf(&pan_runtime[strlen(pan_runtime)], "\"-P%s\" ", PreProc);		}		/* -oN options 1..5 are ignored in simulations */		if (old_priority_rules) strcat(pan_runtime, "-o6 ");		if (!implied_semis)  strcat(pan_runtime, "-o7 ");		if (no_print)        strcat(pan_runtime, "-b ");		if (no_wrapup)       strcat(pan_runtime, "-B ");		if (columns == 1)    strcat(pan_runtime, "-c ");		if (columns == 2)    strcat(pan_runtime, "-M ");		if (seedy == 1)      strcat(pan_runtime, "-h ");		if (like_java == 1)  strcat(pan_runtime, "-J ");		if (old_scope_rules) strcat(pan_runtime, "-O ");		if (notabs)          strcat(pan_runtime, "-T ");		if (verbose&1)       strcat(pan_runtime, "-g ");		if (verbose&2)       strcat(pan_runtime, "-l ");		if (verbose&4)       strcat(pan_runtime, "-p ");		if (verbose&8)       strcat(pan_runtime, "-r ");		if (verbose&16)      strcat(pan_runtime, "-s ");		if (verbose&32)      strcat(pan_runtime, "-v ");		if (verbose&64)      strcat(pan_runtime, "-w ");		if (m_loss)          strcat(pan_runtime, "-m ");		sprintf(tmp, "spin -t %s %s", pan_runtime, Fname->name);		estatus = e_system(1, tmp);	/* replay */		exit(estatus);	/* replay without c_code */	} 	if (buzzed && (!replay || has_code) && !estatus)	{	char *tmp, *tmp2 = NULL, *P_X;		char *C_X = (buzzed == 2) ? "-O" : ""; 		if (replay && strlen(pan_comptime) == 0)		{#if defined(WIN32) || defined(WIN64)			P_X = "pan";#else			P_X = "./pan";#endif			if (stat(P_X, (struct stat *)&x) < 0)			{	goto recompile;	/* no executable pan for replay */			}			tmp = (char *) emalloc(8 + strlen(P_X) + strlen(pan_runtime) +4);			/* the final +4 is too allow adding " &" in some cases */			sprintf(tmp, "%s %s", P_X, pan_runtime);			goto runit;		}#if defined(WIN32) || defined(WIN64)		P_X = "-o pan pan.c && pan";#else		P_X = "-o pan pan.c && ./pan";#endif		/* swarm and biterate randomization additions */		if (!replay && itsr)	/* iterative search refinement */		{	if (!strstr(pan_comptime, "-DBITSTATE"))			{	add_comptime("-DBITSTATE");			}			if (!strstr(pan_comptime, "-DPUTPID"))			{	add_comptime("-DPUTPID");			}			if (!strstr(pan_comptime, "-DT_RAND")			&&  !strstr(pan_comptime, "-DT_REVERSE"))			{	add_runtime("-T0  ");	/* controls t_reverse */			}			if (!strstr(pan_runtime, "-P")	/* runtime flag */			||   pan_runtime[2] < '0'			||   pan_runtime[2] > '1') /* no -P0 or -P1 */			{	add_runtime("-P0  ");	/* controls p_reverse */			}			if (!strstr(pan_runtime, "-w"))			{	add_runtime("-w18 ");	/* -w18 = 256K */			} else			{	char nv[32];				int x;				x = omit_str(pan_runtime, "-w");				if (x >= 0)				{	sprintf(nv, "-w%d  ", x);					add_runtime(nv); /* added spaces */			}	}			if (!strstr(pan_runtime, "-h"))			{	add_runtime("-h0  ");	/* 0..499 */				/* leave 2 spaces for increments up to -h499 */			} else if (!strstr(pan_runtime, "-hash"))			{	char nv[32];				int x;				x = omit_str(pan_runtime, "-h");				if (x >= 0)				{	sprintf(nv, "-h%d  ", x%500);					add_runtime(nv); /* added spaces */			}	}			if (!strstr(pan_runtime, "-k"))			{	add_runtime("-k1  ");	/* 1..3 */			} else			{	char nv[32];				int x;				x = omit_str(pan_runtime, "-k");				if (x >= 0)				{	sprintf(nv, "-k%d  ", x%4);					add_runtime(nv); /* added spaces */			}	}			if (strstr(pan_runtime, "-p_rotate"))			{	char nv[32];				int x;				x = omit_str(pan_runtime, "-p_rotate");				if (x < 0)				{	x = 0;				}				sprintf(nv, "-p_rotate%d  ", x%256);				add_runtime(nv); /* added spaces */			} else if (strstr(pan_runtime, "-p_permute") == 0)			{	add_runtime("-p_rotate0  ");			}			if (strstr(pan_runtime, "-RS"))			{	(void) omit_str(pan_runtime, "-RS");			}			/* need room for at least 10 digits */			add_runtime("-RS1234567890 ");			change_rs(pan_runtime);		}recompile:		if (strstr(PreProc, "cpp"))	/* unix/linux */		{	strcpy(PreProc, "gcc");	/* need compiler */		} else if ((tmp = strstr(PreProc, "-E")) != NULL)		{	*tmp = '\0'; /* strip preprocessing flags */		} 		final_fiddle();		tmp = (char *) emalloc(8 +	/* account for alignment */				strlen(PreProc) +				strlen(C_X) +				strlen(pan_comptime) +				strlen(P_X) +				strlen(pan_runtime) +				strlen(" -p_reverse & "));		tmp2 = tmp; 		/* P_X ends with " && ./pan " */		sprintf(tmp, "%s %s %s %s %s",			PreProc, C_X, pan_comptime, P_X, pan_runtime); 		if (!replay)		{	if (itsr < 0)		/* swarm only */			{	strcat(tmp, " &"); /* after ./pan */				itsr = -itsr;	/* now same as biterate */			}			/* do compilation first			 * split cc command from run command			 * leave cc in tmp, and set tmp2 to run			 */			if ((ptr = strstr(tmp, " && ")) != NULL)			{	tmp2 = ptr + 4;	/* first run */				*ptr = '\0';		}	} 		if (has_ltl)		{	(void) unlink("_spin_nvr.tmp");		}		if (!norecompile)		{#ifdef PC		/* make sure that if compilation fails we do not continue */		(void) unlink("./pan.exe");#else		(void) unlink("./pan");#endif		}runit:		if (norecompile && tmp != tmp2)		{	estatus = 0;		} else		{	if (itsr > 0)	/* else it happens below */			{	estatus = e_system(1, tmp);	/* compile or run */		}	}		if (replay || estatus < 0)		{	goto skipahead;		}		/* !replay */		if (itsr == 0)			/* single run */		{	estatus = e_system(1, tmp2);		} else if (itsr > 0)	/* iterative search refinement */		{	int is_swarm = 0;			if (tmp2 != tmp)	/* swarm: did only compilation so far */			{	tmp = tmp2;	/* now we point to the run command */				estatus = e_system(1, tmp);	/* first run */			}			itsr--;			/* count down */ 			/* the following are added back randomly later */			(void) omit_str(tmp, "-p_reverse");	/* replaced by spaces */			(void) omit_str(tmp, "-p_normal"); 			if (strstr(tmp, " &") != NULL)			{	(void) omit_str(tmp, " &");				is_swarm = 1;			} 			/* increase -w every itsr_n-th run */			if ((itsr_n > 0 && (itsr == 0 || (itsr%itsr_n) != 0))			||  (change_param(tmp, "-w", 36, 18) >= 0))	/* max 4G bit statespace */			{	(void) change_param(tmp, "-h", 500, 0);	/* hash function 0.499 */				(void) change_param(tmp, "-p_rotate", 256, 0); /* if defined */				(void) change_param(tmp, "-k", 4, 1);	/* nr bits per state 0->1,2,3 */				(void) change_param(tmp, "-T", 2, 0);	/* with or without t_reverse*/				(void) change_param(tmp, "-P", 2, 0);	/* -P 0..1 != p_reverse */				change_rs(tmp);			/* change random seed */				string_trim(tmp);				if (rand()%5 == 0)		/* 20% of all runs */				{	strcat(tmp, " -p_reverse ");					/* at end, so this overrides -p_rotateN, if there */					/* but -P0..1 disable this in 50% of the cases */					/* so its really activated in 10% of all runs */				} else if (rand()%6 == 0) /* override p_rotate and p_reverse */				{	strcat(tmp, " -p_normal ");				}				if (is_swarm)				{	strcat(tmp, " &");				}

Lines 1–500 of 1503. Load more