/***** spin: pangen2.c *****/ /* 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 *//* (c) 2007: small additions for V5.0 to support multi-core verifications */ #include "spin.h"#include "version.h"#include "y.tab.h"#include "pangen2.h"#include "pangen4.h"#include "pangen5.h" #define DELTA 500 /* sets an upperbound on nr of chan names */ #define blurb(fd, e) { fprintf(fd, "\n"); if (!merger) fprintf(fd, "\t\t/* %s:%d */\n", \ e->n->fn->name, e->n->ln); }#define tr_map(m, e) { if (!merger) fprintf(tt, "\t\ttr_2_src(%d, \"%s\", %d);\n", \ m, e->n->fn->name, e->n->ln); } extern ProcList *rdy;extern RunList *run;extern Symbol *Fname, *oFname, *context;extern char *claimproc, *eventmap;extern int lineno, verbose, Npars, Mpars, nclaims;extern int m_loss, has_remote, has_remvar, merger, rvopt, separate;extern int Ntimeouts, Etimeouts, deadvar, old_scope_rules;extern int u_sync, u_async, nrRdy, Unique;extern int GenCode, IsGuard, Level, TestOnly;extern short has_stack;extern char *NextLab[]; FILE *tc, *th, *tt, *tb;static FILE *tm; int OkBreak = -1, has_hidden = 0; /* has_hidden set in sym.c and structs.c */short nocast=0; /* to turn off casts in lvalues */short terse=0; /* terse printing of varnames */short no_arrays=0;short has_last=0; /* spec refers to _last */short has_badelse=0; /* spec contains else combined with chan refs */short has_enabled=0; /* spec contains enabled() */short has_pcvalue=0; /* spec contains pc_value() */short has_np=0; /* spec contains np_ */short has_sorted=0; /* spec contains `!!' (sorted-send) operator */short has_random=0; /* spec contains `??' (random-recv) operator */short has_xu=0; /* spec contains xr or xs assertions */short has_unless=0; /* spec contains unless statements */short has_provided=0; /* spec contains PROVIDED clauses on procs */short has_code=0; /* spec contains c_code, c_expr, c_state */short evalindex=0; /* evaluate index of var names */int mst=0; /* max nr of state/process */int claimnr = -1; /* claim process, if any */int eventmapnr = -1; /* event trace, if any */int Pid; /* proc currently processed */int multi_oval; /* set in merges, used also in pangen4.c */ #define MAXMERGE 256 /* max nr of bups per merge sequence */ static short CnT[MAXMERGE];static Lextok XZ, YZ[MAXMERGE];static int didcase, YZmax, YZcnt; static Lextok *Nn[2];static int Det; /* set if deterministic */static int T_sum, T_mus, t_cyc;static int TPE[2], EPT[2];static int uniq=1;static int multi_needed, multi_undo;static short AllGlobal=0; /* set if process has provided clause */static short withprocname=0; /* prefix local varnames with procname */static short _isok=0; /* checks usage of predefined variable _ */ int has_global(Lextok *);void Fatal(char *, char *);static int getweight(Lextok *);static int scan_seq(Sequence *);static void genconditionals(void);static void mark_seq(Sequence *);static void patch_atomic(Sequence *);static void put_seq(Sequence *, int, int);static void putproc(ProcList *);static void Tpe(Lextok *);extern void spit_recvs(FILE *, FILE*); static intfproc(char *s){ ProcList *p; for (p = rdy; p; p = p->nxt) if (strcmp(p->n->name, s) == 0) return p->tn; fatal("proctype %s not found", s); return -1;} intpid_is_claim(int p) /* Pid (p->tn) to type (p->b) */{ ProcList *r; for (r = rdy; r; r = r->nxt) { if (r->tn == p) return (r->b == N_CLAIM); } printf("spin: error, cannot find pid %d\n", p); return 0;} static voidreverse_procs(RunList *q){ if (!q) return; reverse_procs(q->nxt); fprintf(tc, " Addproc(%d);\n", q->tn);} static voidforward_procs(RunList *q){ if (!q) return; fprintf(tc, " Addproc(%d);\n", q->tn); forward_procs(q->nxt);} static voidtm_predef_np(void){ fprintf(th, "#define _T5 %d\n", uniq++); fprintf(th, "#define _T2 %d\n", uniq++); if (Unique < (1 << (8*sizeof(unsigned char)) )) /* was uniq before */ { fprintf(th, "#define T_ID unsigned char\n"); } else if (Unique < (1 << (8*sizeof(unsigned short)) )) { fprintf(th, "#define T_ID unsigned short\n"); } else { fprintf(th, "#define T_ID unsigned int\n"); } fprintf(tm, "\tcase _T5:\t/* np_ */\n"); if (separate == 2) fprintf(tm, "\t\tif (!((!(o_pm&4) && !(tau&128))))\n"); else fprintf(tm, "\t\tif (!((!(trpt->o_pm&4) && !(trpt->tau&128))))\n"); fprintf(tm, "\t\t\tcontinue;\n"); fprintf(tm, "\t\t/* else fall through */\n"); fprintf(tm, "\tcase _T2:\t/* true */\n"); fprintf(tm, "\t\t_m = 3; goto P999;\n");} static voidtt_predef_np(void){ fprintf(tt, "\t/* np_ demon: */\n"); fprintf(tt, "\ttrans[_NP_] = "); fprintf(tt, "(Trans **) emalloc(2*sizeof(Trans *));\n"); fprintf(tt, "\tT = trans[_NP_][0] = "); fprintf(tt, "settr(9997,0,1,_T5,0,\"(np_)\", 1,2,0);\n"); fprintf(tt, "\t T->nxt = "); fprintf(tt, "settr(9998,0,0,_T2,0,\"(1)\", 0,2,0);\n"); fprintf(tt, "\tT = trans[_NP_][1] = "); fprintf(tt, "settr(9999,0,1,_T5,0,\"(np_)\", 1,2,0);\n");} static struct { char *nm[3];} Cfile[] = { { { "pan.c", "pan_s.c", "pan_t.c" } }, { { "pan.h", "pan_s.h", "pan_t.h" } }, { { "pan.t", "pan_s.t", "pan_t.t" } }, { { "pan.m", "pan_s.m", "pan_t.m" } }, { { "pan.b", "pan_s.b", "pan_t.b" } }}; voidgensrc(void){ ProcList *p; int i; disambiguate(); /* avoid name-clashes between scopes */ if (!(tc = fopen(Cfile[0].nm[separate], MFLAGS)) /* main routines */ || !(th = fopen(Cfile[1].nm[separate], MFLAGS)) /* header file */ || !(tt = fopen(Cfile[2].nm[separate], MFLAGS)) /* transition matrix */ || !(tm = fopen(Cfile[3].nm[separate], MFLAGS)) /* forward moves */ || !(tb = fopen(Cfile[4].nm[separate], MFLAGS))) /* backward moves */ { printf("spin: cannot create pan.[chtmfb]\n"); alldone(1); } fprintf(th, "#define SpinVersion \"%s\"\n", SpinVersion); fprintf(th, "#define PanSource \""); for (i = 0; oFname->name[i] != '\0'; i++) { char c = oFname->name[i]; if (c == '\\' || c == ' ') /* Windows path */ { fprintf(th, "\\"); } fprintf(th, "%c", c); } fprintf(th, "\"\n\n"); fprintf(th, "#define G_long %d\n", (int) sizeof(long)); fprintf(th, "#define G_int %d\n", (int) sizeof(int)); fprintf(th, "#ifdef WIN64\n"); fprintf(th, " #define ONE_L ((unsigned long) 1)\n"); fprintf(th, " #define long long long\n"); fprintf(th, "#else\n"); fprintf(th, " #define ONE_L (1L)\n"); fprintf(th, "#endif\n"); if (separate != 2) { fprintf(th, "char *TrailFile = PanSource; /* default */\n"); fprintf(th, "char *trailfilename;\n"); } fprintf(th, "#if defined(BFS)\n"); fprintf(th, " #ifndef SAFETY\n"); fprintf(th, " #define SAFETY\n"); fprintf(th, " #endif\n"); fprintf(th, " #ifndef XUSAFE\n"); fprintf(th, " #define XUSAFE\n"); fprintf(th, " #endif\n"); fprintf(th, "#endif\n"); fprintf(th, "#ifndef uchar\n"); fprintf(th, " #define uchar unsigned char\n"); fprintf(th, "#endif\n"); fprintf(th, "#ifndef uint\n"); fprintf(th, " #define uint unsigned int\n"); fprintf(th, "#endif\n"); if (sizeof(void *) > 4) /* 64 bit machine */ { fprintf(th, "#if !defined(HASH32) && !defined(HASH64)\n"); fprintf(th, " #define HASH64\n"); fprintf(th, "#endif\n"); } if (separate == 1 && !claimproc) { Symbol *n = (Symbol *) emalloc(sizeof(Symbol)); Sequence *s = (Sequence *) emalloc(sizeof(Sequence)); claimproc = n->name = "_:never_template:_"; ready(n, ZN, s, 0, ZN, N_CLAIM); } if (separate == 2) { if (has_remote) { printf("spin: warning, make sure that the S1 model\n"); printf(" includes the same remote references\n"); } fprintf(th, "#ifndef NFAIR\n"); fprintf(th, "#define NFAIR 2 /* must be >= 2 */\n"); fprintf(th, "#endif\n"); if (has_last) fprintf(th, "#define HAS_LAST %d\n", has_last); goto doless; } fprintf(th, "#define DELTA %d\n", DELTA); fprintf(th, "#ifdef MA\n"); fprintf(th, " #if NCORE>1 && !defined(SEP_STATE)\n"); fprintf(th, " #define SEP_STATE\n"); fprintf(th, " #endif\n"); fprintf(th, "#if MA==1\n"); /* user typed -DMA without size */ fprintf(th, " #undef MA\n"); fprintf(th, " #define MA 100\n"); fprintf(th, "#endif\n#endif\n"); fprintf(th, "#ifdef W_XPT\n"); fprintf(th, " #if W_XPT==1\n"); /* user typed -DW_XPT without size */ fprintf(th, " #undef W_XPT\n"); fprintf(th, " #define W_XPT 1000000\n"); fprintf(th, " #endif\n"); fprintf(th, "#endif\n"); fprintf(th, "#ifndef NFAIR\n"); fprintf(th, " #define NFAIR 2 /* must be >= 2 */\n"); fprintf(th, "#endif\n"); if (Ntimeouts) fprintf(th, "#define NTIM %d\n", Ntimeouts); if (Etimeouts) fprintf(th, "#define ETIM %d\n", Etimeouts); if (has_remvar) fprintf(th, "#define REM_VARS 1\n"); if (has_remote) fprintf(th, "#define REM_REFS %d\n", has_remote); /* not yet used */ if (has_hidden) fprintf(th, "#define HAS_HIDDEN %d\n", has_hidden); if (has_last) fprintf(th, "#define HAS_LAST %d\n", has_last); if (has_sorted) fprintf(th, "#define HAS_SORTED %d\n", has_sorted); if (m_loss) fprintf(th, "#define M_LOSS\n"); if (has_random) fprintf(th, "#define HAS_RANDOM %d\n", has_random); fprintf(th, "#define HAS_CODE\n"); /* doesn't seem to cause measurable overhead */ fprintf(th, "#if defined(RANDSTORE) && !defined(RANDSTOR)\n"); fprintf(th, " #define RANDSTOR RANDSTORE\n"); /* xspin uses RANDSTORE... */ fprintf(th, "#endif\n"); if (has_stack) fprintf(th, "#define HAS_STACK %d\n", has_stack); if (has_enabled) fprintf(th, "#define HAS_ENABLED 1\n"); if (has_unless) fprintf(th, "#define HAS_UNLESS %d\n", has_unless); if (has_provided) fprintf(th, "#define HAS_PROVIDED %d\n", has_provided); if (has_pcvalue) fprintf(th, "#define HAS_PCVALUE %d\n", has_pcvalue); if (has_badelse) fprintf(th, "#define HAS_BADELSE %d\n", has_badelse); if (has_enabled || has_pcvalue || has_badelse || has_last) { fprintf(th, "#ifndef NOREDUCE\n"); fprintf(th, " #define NOREDUCE 1\n"); fprintf(th, "#endif\n"); } if (has_np) fprintf(th, "#define HAS_NP %d\n", has_np); if (merger) fprintf(th, "#define MERGED 1\n"); doless: fprintf(th, "#if !defined(HAS_LAST) && defined(BCS)\n"); fprintf(th, " #define HAS_LAST 1 /* use it, but */\n"); fprintf(th, " #ifndef STORE_LAST\n"); /* unless the user insists */ fprintf(th, " #define NO_LAST 1 /* dont store it */\n"); fprintf(th, " #endif\n"); fprintf(th, "#endif\n"); fprintf(th, "#if defined(BCS) && defined(BITSTATE)\n"); fprintf(th, " #ifndef NO_CTX\n"); fprintf(th, " #define STORE_CTX 1\n"); fprintf(th, " #endif\n"); fprintf(th, "#endif\n"); fprintf(th, "#ifdef NP\n"); if (!has_np) fprintf(th, " #define HAS_NP 2\n"); fprintf(th, " #define VERI %d /* np_ */\n", nrRdy); fprintf(th, "#endif\n"); if (claimproc) { claimnr = fproc(claimproc); /* the default claim */ fprintf(th, "#ifndef NOCLAIM\n"); fprintf(th, " #define NCLAIMS %d\n", nclaims); fprintf(th, " #ifndef NP\n"); fprintf(th, " #define VERI %d\n", claimnr); fprintf(th, " #endif\n"); fprintf(th, "#endif\n"); } if (eventmap) { eventmapnr = fproc(eventmap); fprintf(th, "#define EVENT_TRACE %d\n", eventmapnr); fprintf(th, "#define endevent endstate%d\n", eventmapnr); if (eventmap[2] == 'o') /* ":notrace:" */ fprintf(th, "#define NEGATED_TRACE 1\n"); } fprintf(th, "typedef struct S_F_MAP {\n"); fprintf(th, " char *fnm; int from; int upto;\n"); fprintf(th, "} S_F_MAP;\n"); fprintf(tc, "/*** Generated by %s ***/\n", SpinVersion); fprintf(tc, "/*** From source: %s ***/\n\n", oFname->name); ntimes(tc, 0, 1, Pre0); plunk_c_decls(tc); /* types can be refered to in State */ switch (separate) { case 0: fprintf(tc, "#include \"pan.h\"\n"); break; case 1: fprintf(tc, "#include \"pan_s.h\"\n"); break; case 2: fprintf(tc, "#include \"pan_t.h\"\n"); break; } fprintf(tc, "#ifdef LOOPSTATE\n"); fprintf(tc, "double cnt_loops;\n"); fprintf(tc, "#endif\n"); fprintf(tc, "State A_Root; /* seed-state for cycles */\n"); fprintf(tc, "State now; /* the full state-vector */\n"); plunk_c_fcts(tc); /* State can be used in fcts */ if (separate != 2) ntimes(tc, 0, 1, Preamble); else fprintf(tc, "extern int verbose; extern long depth;\n"); fprintf(tc, "#ifndef NOBOUNDCHECK\n"); fprintf(tc, " #define Index(x, y)\tBoundcheck(x, y, II, tt, t)\n"); fprintf(tc, "#else\n"); fprintf(tc, " #define Index(x, y)\tx\n"); fprintf(tc, "#endif\n"); c_preview(); /* sets hastrack */ for (p = rdy; p; p = p->nxt) mst = max(p->s->maxel, mst); if (separate != 2) { fprintf(tt, "#ifdef PEG\n"); fprintf(tt, "struct T_SRC {\n"); fprintf(tt, " char *fl; int ln;\n"); fprintf(tt, "} T_SRC[NTRANS];\n\n"); fprintf(tt, "void\ntr_2_src(int m, char *file, int ln)\n"); fprintf(tt, "{ T_SRC[m].fl = file;\n"); fprintf(tt, " T_SRC[m].ln = ln;\n"); fprintf(tt, "}\n\n"); fprintf(tt, "void\nputpeg(int n, int m)\n"); fprintf(tt, "{ printf(\"%%5d\ttrans %%4d \", m, n);\n"); fprintf(tt, " printf(\"%%s:%%d\\n\",\n"); fprintf(tt, " T_SRC[n].fl, T_SRC[n].ln);\n"); fprintf(tt, "}\n"); if (!merger) { fprintf(tt, "#else\n"); fprintf(tt, "#define tr_2_src(m,f,l)\n"); } fprintf(tt, "#endif\n\n"); fprintf(tt, "void\nsettable(void)\n{\tTrans *T;\n"); fprintf(tt, "\tTrans *settr(int, int, int, int, int,"); fprintf(tt, " char *, int, int, int);\n\n"); fprintf(tt, "\ttrans = (Trans ***) "); fprintf(tt, "emalloc(%d*sizeof(Trans **));\n", nrRdy+1); /* +1 for np_ automaton */ if (separate == 1) { fprintf(tm, " if (II == 0)\n"); fprintf(tm, " { _m = step_claim(trpt->o_pm, trpt->tau, tt, ot, t);\n"); fprintf(tm, " if (_m) goto P999; else continue;\n"); fprintf(tm, " } else\n"); } fprintf(tm, "#define rand pan_rand\n"); fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n"); fprintf(tm, " cpu_printf(\"Pr: %%d Tr: %%d\\n\", II, t->forw);\n"); fprintf(tm, "#endif\n"); fprintf(tm, " switch (t->forw) {\n"); } else { fprintf(tt, "#ifndef PEG\n"); fprintf(tt, " #define tr_2_src(m,f,l)\n"); fprintf(tt, "#endif\n"); fprintf(tt, "void\nset_claim(void)\n{\tTrans *T;\n"); fprintf(tt, "\textern Trans ***trans;\n"); fprintf(tt, "\textern Trans *settr(int, int, int, int, int,"); fprintf(tt, " char *, int, int, int);\n\n"); fprintf(tm, "#define rand pan_rand\n"); fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n"); fprintf(tm, " cpu_printf(\"Pr: %%d Tr: %%d\\n\", II, forw);\n"); fprintf(tm, "#endif\n"); fprintf(tm, " switch (forw) {\n"); } fprintf(tm, " default: Uerror(\"bad forward move\");\n"); fprintf(tm, " case 0: /* if without executable clauses */\n"); fprintf(tm, " continue;\n"); fprintf(tm, " case 1: /* generic 'goto' or 'skip' */\n"); if (separate != 2) fprintf(tm, " IfNotBlocked\n"); fprintf(tm, " _m = 3; goto P999;\n"); fprintf(tm, " case 2: /* generic 'else' */\n"); if (separate == 2) fprintf(tm, " if (o_pm&1) continue;\n"); else { fprintf(tm, " IfNotBlocked\n"); fprintf(tm, " if (trpt->o_pm&1) continue;\n"); } fprintf(tm, " _m = 3; goto P999;\n"); uniq = 3; if (separate == 1) fprintf(tb, " if (II == 0) goto R999;\n"); fprintf(tb, " switch (t->back) {\n"); fprintf(tb, " default: Uerror(\"bad return move\");\n"); fprintf(tb, " case 0: goto R999; /* nothing to undo */\n"); for (p = rdy; p; p = p->nxt) { putproc(p); } if (separate != 2) { fprintf(th, "struct {\n"); fprintf(th, " int tp; short *src;\n"); fprintf(th, "} src_all[] = {\n"); for (p = rdy; p; p = p->nxt) fprintf(th, " { %d, &src_ln%d[0] },\n", p->tn, p->tn); fprintf(th, " { 0, (short *) 0 }\n"); fprintf(th, "};\n"); Lines 1–500 of 3193. Load more
/***** spin: pangen2.c *****/ /* 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 */ /* (c) 2007: small additions for V5.0 to support multi-core verifications */ #include "spin.h" #include "version.h" #include "y.tab.h" #include "pangen2.h" #include "pangen4.h" #include "pangen5.h" #define DELTA 500 /* sets an upperbound on nr of chan names */ #define blurb(fd, e) { fprintf(fd, "\n"); if (!merger) fprintf(fd, "\t\t/* %s:%d */\n", \ e->n->fn->name, e->n->ln); } #define tr_map(m, e) { if (!merger) fprintf(tt, "\t\ttr_2_src(%d, \"%s\", %d);\n", \ m, e->n->fn->name, e->n->ln); } extern ProcList *rdy; extern RunList *run; extern Symbol *Fname, *oFname, *context; extern char *claimproc, *eventmap; extern int lineno, verbose, Npars, Mpars, nclaims; extern int m_loss, has_remote, has_remvar, merger, rvopt, separate; extern int Ntimeouts, Etimeouts, deadvar, old_scope_rules; extern int u_sync, u_async, nrRdy, Unique; extern int GenCode, IsGuard, Level, TestOnly; extern short has_stack; extern char *NextLab[]; FILE *tc, *th, *tt, *tb; static FILE *tm; int OkBreak = -1, has_hidden = 0; /* has_hidden set in sym.c and structs.c */ short nocast=0; /* to turn off casts in lvalues */ short terse=0; /* terse printing of varnames */ short no_arrays=0; short has_last=0; /* spec refers to _last */ short has_badelse=0; /* spec contains else combined with chan refs */ short has_enabled=0; /* spec contains enabled() */ short has_pcvalue=0; /* spec contains pc_value() */ short has_np=0; /* spec contains np_ */ short has_sorted=0; /* spec contains `!!' (sorted-send) operator */ short has_random=0; /* spec contains `??' (random-recv) operator */ short has_xu=0; /* spec contains xr or xs assertions */ short has_unless=0; /* spec contains unless statements */ short has_provided=0; /* spec contains PROVIDED clauses on procs */ short has_code=0; /* spec contains c_code, c_expr, c_state */ short evalindex=0; /* evaluate index of var names */ int mst=0; /* max nr of state/process */ int claimnr = -1; /* claim process, if any */ int eventmapnr = -1; /* event trace, if any */ int Pid; /* proc currently processed */ int multi_oval; /* set in merges, used also in pangen4.c */ #define MAXMERGE 256 /* max nr of bups per merge sequence */ static short CnT[MAXMERGE]; static Lextok XZ, YZ[MAXMERGE]; static int didcase, YZmax, YZcnt; static Lextok *Nn[2]; static int Det; /* set if deterministic */ static int T_sum, T_mus, t_cyc; static int TPE[2], EPT[2]; static int uniq=1; static int multi_needed, multi_undo; static short AllGlobal=0; /* set if process has provided clause */ static short withprocname=0; /* prefix local varnames with procname */ static short _isok=0; /* checks usage of predefined variable _ */ int has_global(Lextok *); void Fatal(char *, char *); static int getweight(Lextok *); static int scan_seq(Sequence *); static void genconditionals(void); static void mark_seq(Sequence *); static void patch_atomic(Sequence *); static void put_seq(Sequence *, int, int); static void putproc(ProcList *); static void Tpe(Lextok *); extern void spit_recvs(FILE *, FILE*); static int fproc(char *s) { ProcList *p; for (p = rdy; p; p = p->nxt) if (strcmp(p->n->name, s) == 0) return p->tn; fatal("proctype %s not found", s); return -1; } int pid_is_claim(int p) /* Pid (p->tn) to type (p->b) */ { ProcList *r; for (r = rdy; r; r = r->nxt) { if (r->tn == p) return (r->b == N_CLAIM); } printf("spin: error, cannot find pid %d\n", p); return 0; } static void reverse_procs(RunList *q) { if (!q) return; reverse_procs(q->nxt); fprintf(tc, " Addproc(%d);\n", q->tn); } static void forward_procs(RunList *q) { if (!q) return; fprintf(tc, " Addproc(%d);\n", q->tn); forward_procs(q->nxt); } static void tm_predef_np(void) { fprintf(th, "#define _T5 %d\n", uniq++); fprintf(th, "#define _T2 %d\n", uniq++); if (Unique < (1 << (8*sizeof(unsigned char)) )) /* was uniq before */ { fprintf(th, "#define T_ID unsigned char\n"); } else if (Unique < (1 << (8*sizeof(unsigned short)) )) { fprintf(th, "#define T_ID unsigned short\n"); } else { fprintf(th, "#define T_ID unsigned int\n"); } fprintf(tm, "\tcase _T5:\t/* np_ */\n"); if (separate == 2) fprintf(tm, "\t\tif (!((!(o_pm&4) && !(tau&128))))\n"); else fprintf(tm, "\t\tif (!((!(trpt->o_pm&4) && !(trpt->tau&128))))\n"); fprintf(tm, "\t\t\tcontinue;\n"); fprintf(tm, "\t\t/* else fall through */\n"); fprintf(tm, "\tcase _T2:\t/* true */\n"); fprintf(tm, "\t\t_m = 3; goto P999;\n"); } static void tt_predef_np(void) { fprintf(tt, "\t/* np_ demon: */\n"); fprintf(tt, "\ttrans[_NP_] = "); fprintf(tt, "(Trans **) emalloc(2*sizeof(Trans *));\n"); fprintf(tt, "\tT = trans[_NP_][0] = "); fprintf(tt, "settr(9997,0,1,_T5,0,\"(np_)\", 1,2,0);\n"); fprintf(tt, "\t T->nxt = "); fprintf(tt, "settr(9998,0,0,_T2,0,\"(1)\", 0,2,0);\n"); fprintf(tt, "\tT = trans[_NP_][1] = "); fprintf(tt, "settr(9999,0,1,_T5,0,\"(np_)\", 1,2,0);\n"); } static struct { char *nm[3]; } Cfile[] = { { { "pan.c", "pan_s.c", "pan_t.c" } }, { { "pan.h", "pan_s.h", "pan_t.h" } }, { { "pan.t", "pan_s.t", "pan_t.t" } }, { { "pan.m", "pan_s.m", "pan_t.m" } }, { { "pan.b", "pan_s.b", "pan_t.b" } } }; void gensrc(void) { ProcList *p; int i; disambiguate(); /* avoid name-clashes between scopes */ if (!(tc = fopen(Cfile[0].nm[separate], MFLAGS)) /* main routines */ || !(th = fopen(Cfile[1].nm[separate], MFLAGS)) /* header file */ || !(tt = fopen(Cfile[2].nm[separate], MFLAGS)) /* transition matrix */ || !(tm = fopen(Cfile[3].nm[separate], MFLAGS)) /* forward moves */ || !(tb = fopen(Cfile[4].nm[separate], MFLAGS))) /* backward moves */ { printf("spin: cannot create pan.[chtmfb]\n"); alldone(1); } fprintf(th, "#define SpinVersion \"%s\"\n", SpinVersion); fprintf(th, "#define PanSource \""); for (i = 0; oFname->name[i] != '\0'; i++) { char c = oFname->name[i]; if (c == '\\' || c == ' ') /* Windows path */ { fprintf(th, "\\"); } fprintf(th, "%c", c); } fprintf(th, "\"\n\n"); fprintf(th, "#define G_long %d\n", (int) sizeof(long)); fprintf(th, "#define G_int %d\n", (int) sizeof(int)); fprintf(th, "#ifdef WIN64\n"); fprintf(th, " #define ONE_L ((unsigned long) 1)\n"); fprintf(th, " #define long long long\n"); fprintf(th, "#else\n"); fprintf(th, " #define ONE_L (1L)\n"); fprintf(th, "#endif\n"); if (separate != 2) { fprintf(th, "char *TrailFile = PanSource; /* default */\n"); fprintf(th, "char *trailfilename;\n"); } fprintf(th, "#if defined(BFS)\n"); fprintf(th, " #ifndef SAFETY\n"); fprintf(th, " #define SAFETY\n"); fprintf(th, " #endif\n"); fprintf(th, " #ifndef XUSAFE\n"); fprintf(th, " #define XUSAFE\n"); fprintf(th, " #endif\n"); fprintf(th, "#endif\n"); fprintf(th, "#ifndef uchar\n"); fprintf(th, " #define uchar unsigned char\n"); fprintf(th, "#endif\n"); fprintf(th, "#ifndef uint\n"); fprintf(th, " #define uint unsigned int\n"); fprintf(th, "#endif\n"); if (sizeof(void *) > 4) /* 64 bit machine */ { fprintf(th, "#if !defined(HASH32) && !defined(HASH64)\n"); fprintf(th, " #define HASH64\n"); fprintf(th, "#endif\n"); } if (separate == 1 && !claimproc) { Symbol *n = (Symbol *) emalloc(sizeof(Symbol)); Sequence *s = (Sequence *) emalloc(sizeof(Sequence)); claimproc = n->name = "_:never_template:_"; ready(n, ZN, s, 0, ZN, N_CLAIM); } if (separate == 2) { if (has_remote) { printf("spin: warning, make sure that the S1 model\n"); printf(" includes the same remote references\n"); } fprintf(th, "#ifndef NFAIR\n"); fprintf(th, "#define NFAIR 2 /* must be >= 2 */\n"); fprintf(th, "#endif\n"); if (has_last) fprintf(th, "#define HAS_LAST %d\n", has_last); goto doless; } fprintf(th, "#define DELTA %d\n", DELTA); fprintf(th, "#ifdef MA\n"); fprintf(th, " #if NCORE>1 && !defined(SEP_STATE)\n"); fprintf(th, " #define SEP_STATE\n"); fprintf(th, " #endif\n"); fprintf(th, "#if MA==1\n"); /* user typed -DMA without size */ fprintf(th, " #undef MA\n"); fprintf(th, " #define MA 100\n"); fprintf(th, "#endif\n#endif\n"); fprintf(th, "#ifdef W_XPT\n"); fprintf(th, " #if W_XPT==1\n"); /* user typed -DW_XPT without size */ fprintf(th, " #undef W_XPT\n"); fprintf(th, " #define W_XPT 1000000\n"); fprintf(th, " #endif\n"); fprintf(th, "#endif\n"); fprintf(th, "#ifndef NFAIR\n"); fprintf(th, " #define NFAIR 2 /* must be >= 2 */\n"); fprintf(th, "#endif\n"); if (Ntimeouts) fprintf(th, "#define NTIM %d\n", Ntimeouts); if (Etimeouts) fprintf(th, "#define ETIM %d\n", Etimeouts); if (has_remvar) fprintf(th, "#define REM_VARS 1\n"); if (has_remote) fprintf(th, "#define REM_REFS %d\n", has_remote); /* not yet used */ if (has_hidden) fprintf(th, "#define HAS_HIDDEN %d\n", has_hidden); if (has_last) fprintf(th, "#define HAS_LAST %d\n", has_last); if (has_sorted) fprintf(th, "#define HAS_SORTED %d\n", has_sorted); if (m_loss) fprintf(th, "#define M_LOSS\n"); if (has_random) fprintf(th, "#define HAS_RANDOM %d\n", has_random); fprintf(th, "#define HAS_CODE\n"); /* doesn't seem to cause measurable overhead */ fprintf(th, "#if defined(RANDSTORE) && !defined(RANDSTOR)\n"); fprintf(th, " #define RANDSTOR RANDSTORE\n"); /* xspin uses RANDSTORE... */ fprintf(th, "#endif\n"); if (has_stack) fprintf(th, "#define HAS_STACK %d\n", has_stack); if (has_enabled) fprintf(th, "#define HAS_ENABLED 1\n"); if (has_unless) fprintf(th, "#define HAS_UNLESS %d\n", has_unless); if (has_provided) fprintf(th, "#define HAS_PROVIDED %d\n", has_provided); if (has_pcvalue) fprintf(th, "#define HAS_PCVALUE %d\n", has_pcvalue); if (has_badelse) fprintf(th, "#define HAS_BADELSE %d\n", has_badelse); if (has_enabled || has_pcvalue || has_badelse || has_last) { fprintf(th, "#ifndef NOREDUCE\n"); fprintf(th, " #define NOREDUCE 1\n"); fprintf(th, "#endif\n"); } if (has_np) fprintf(th, "#define HAS_NP %d\n", has_np); if (merger) fprintf(th, "#define MERGED 1\n"); doless: fprintf(th, "#if !defined(HAS_LAST) && defined(BCS)\n"); fprintf(th, " #define HAS_LAST 1 /* use it, but */\n"); fprintf(th, " #ifndef STORE_LAST\n"); /* unless the user insists */ fprintf(th, " #define NO_LAST 1 /* dont store it */\n"); fprintf(th, " #endif\n"); fprintf(th, "#endif\n"); fprintf(th, "#if defined(BCS) && defined(BITSTATE)\n"); fprintf(th, " #ifndef NO_CTX\n"); fprintf(th, " #define STORE_CTX 1\n"); fprintf(th, " #endif\n"); fprintf(th, "#endif\n"); fprintf(th, "#ifdef NP\n"); if (!has_np) fprintf(th, " #define HAS_NP 2\n"); fprintf(th, " #define VERI %d /* np_ */\n", nrRdy); fprintf(th, "#endif\n"); if (claimproc) { claimnr = fproc(claimproc); /* the default claim */ fprintf(th, "#ifndef NOCLAIM\n"); fprintf(th, " #define NCLAIMS %d\n", nclaims); fprintf(th, " #ifndef NP\n"); fprintf(th, " #define VERI %d\n", claimnr); fprintf(th, " #endif\n"); fprintf(th, "#endif\n"); } if (eventmap) { eventmapnr = fproc(eventmap); fprintf(th, "#define EVENT_TRACE %d\n", eventmapnr); fprintf(th, "#define endevent endstate%d\n", eventmapnr); if (eventmap[2] == 'o') /* ":notrace:" */ fprintf(th, "#define NEGATED_TRACE 1\n"); } fprintf(th, "typedef struct S_F_MAP {\n"); fprintf(th, " char *fnm; int from; int upto;\n"); fprintf(th, "} S_F_MAP;\n"); fprintf(tc, "/*** Generated by %s ***/\n", SpinVersion); fprintf(tc, "/*** From source: %s ***/\n\n", oFname->name); ntimes(tc, 0, 1, Pre0); plunk_c_decls(tc); /* types can be refered to in State */ switch (separate) { case 0: fprintf(tc, "#include \"pan.h\"\n"); break; case 1: fprintf(tc, "#include \"pan_s.h\"\n"); break; case 2: fprintf(tc, "#include \"pan_t.h\"\n"); break; } fprintf(tc, "#ifdef LOOPSTATE\n"); fprintf(tc, "double cnt_loops;\n"); fprintf(tc, "#endif\n"); fprintf(tc, "State A_Root; /* seed-state for cycles */\n"); fprintf(tc, "State now; /* the full state-vector */\n"); plunk_c_fcts(tc); /* State can be used in fcts */ if (separate != 2) ntimes(tc, 0, 1, Preamble); else fprintf(tc, "extern int verbose; extern long depth;\n"); fprintf(tc, "#ifndef NOBOUNDCHECK\n"); fprintf(tc, " #define Index(x, y)\tBoundcheck(x, y, II, tt, t)\n"); fprintf(tc, "#else\n"); fprintf(tc, " #define Index(x, y)\tx\n"); fprintf(tc, "#endif\n"); c_preview(); /* sets hastrack */ for (p = rdy; p; p = p->nxt) mst = max(p->s->maxel, mst); if (separate != 2) { fprintf(tt, "#ifdef PEG\n"); fprintf(tt, "struct T_SRC {\n"); fprintf(tt, " char *fl; int ln;\n"); fprintf(tt, "} T_SRC[NTRANS];\n\n"); fprintf(tt, "void\ntr_2_src(int m, char *file, int ln)\n"); fprintf(tt, "{ T_SRC[m].fl = file;\n"); fprintf(tt, " T_SRC[m].ln = ln;\n"); fprintf(tt, "}\n\n"); fprintf(tt, "void\nputpeg(int n, int m)\n"); fprintf(tt, "{ printf(\"%%5d\ttrans %%4d \", m, n);\n"); fprintf(tt, " printf(\"%%s:%%d\\n\",\n"); fprintf(tt, " T_SRC[n].fl, T_SRC[n].ln);\n"); fprintf(tt, "}\n"); if (!merger) { fprintf(tt, "#else\n"); fprintf(tt, "#define tr_2_src(m,f,l)\n"); } fprintf(tt, "#endif\n\n"); fprintf(tt, "void\nsettable(void)\n{\tTrans *T;\n"); fprintf(tt, "\tTrans *settr(int, int, int, int, int,"); fprintf(tt, " char *, int, int, int);\n\n"); fprintf(tt, "\ttrans = (Trans ***) "); fprintf(tt, "emalloc(%d*sizeof(Trans **));\n", nrRdy+1); /* +1 for np_ automaton */ if (separate == 1) { fprintf(tm, " if (II == 0)\n"); fprintf(tm, " { _m = step_claim(trpt->o_pm, trpt->tau, tt, ot, t);\n"); fprintf(tm, " if (_m) goto P999; else continue;\n"); fprintf(tm, " } else\n"); } fprintf(tm, "#define rand pan_rand\n"); fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n"); fprintf(tm, " cpu_printf(\"Pr: %%d Tr: %%d\\n\", II, t->forw);\n"); fprintf(tm, "#endif\n"); fprintf(tm, " switch (t->forw) {\n"); } else { fprintf(tt, "#ifndef PEG\n"); fprintf(tt, " #define tr_2_src(m,f,l)\n"); fprintf(tt, "#endif\n"); fprintf(tt, "void\nset_claim(void)\n{\tTrans *T;\n"); fprintf(tt, "\textern Trans ***trans;\n"); fprintf(tt, "\textern Trans *settr(int, int, int, int, int,"); fprintf(tt, " char *, int, int, int);\n\n"); fprintf(tm, "#define rand pan_rand\n"); fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n"); fprintf(tm, " cpu_printf(\"Pr: %%d Tr: %%d\\n\", II, forw);\n"); fprintf(tm, "#endif\n"); fprintf(tm, " switch (forw) {\n"); } fprintf(tm, " default: Uerror(\"bad forward move\");\n"); fprintf(tm, " case 0: /* if without executable clauses */\n"); fprintf(tm, " continue;\n"); fprintf(tm, " case 1: /* generic 'goto' or 'skip' */\n"); if (separate != 2) fprintf(tm, " IfNotBlocked\n"); fprintf(tm, " _m = 3; goto P999;\n"); fprintf(tm, " case 2: /* generic 'else' */\n"); if (separate == 2) fprintf(tm, " if (o_pm&1) continue;\n"); else { fprintf(tm, " IfNotBlocked\n"); fprintf(tm, " if (trpt->o_pm&1) continue;\n"); } fprintf(tm, " _m = 3; goto P999;\n"); uniq = 3; if (separate == 1) fprintf(tb, " if (II == 0) goto R999;\n"); fprintf(tb, " switch (t->back) {\n"); fprintf(tb, " default: Uerror(\"bad return move\");\n"); fprintf(tb, " case 0: goto R999; /* nothing to undo */\n"); for (p = rdy; p; p = p->nxt) { putproc(p); } if (separate != 2) { fprintf(th, "struct {\n"); fprintf(th, " int tp; short *src;\n"); fprintf(th, "} src_all[] = {\n"); for (p = rdy; p; p = p->nxt) fprintf(th, " { %d, &src_ln%d[0] },\n", p->tn, p->tn); fprintf(th, " { 0, (short *) 0 }\n"); fprintf(th, "};\n");