update the version of the Spin model checker included with Plan 9 to the newest version, 4.3.0 Notes: Sun Aug 5 21:54:38 EDT 2007 geoff anybody know how to verify that the new spin works right? Reference: /n/sources/patch/applied/spin430 Date: Sun Jul 22 05:01:23 CES 2007 Signed-off-by: crd@andrew.cmu.edu Reviewed-by: geoff --- /sys/man/1/spin Sun Jul 22 05:03:46 2007 +++ /sys/man/1/spin Sun Jul 22 05:02:15 2007 @@ -271,4 +271,4 @@ --, `The model checker \*Z,' \f2IEEE Trans. on SE\f1, Vol, 23, No. 5, May 1997. .in -4 -.br +.br --- /sys/src/cmd/spin/README Sun Jul 22 04:47:13 2007 +++ /sys/src/cmd/spin/README Sun Jul 22 04:47:12 2007 @@ -2,7 +2,7 @@ available via: http://spinroot.com/spin/whatispin.html -to make the sources compile with the mkfile on plan 9 +to make the sources compile with the mkfile on Plan 9 the following changes were made: omitted memory.h from spin.h --- /sys/src/cmd/spin/dstep.c Sun Jul 22 04:47:17 2007 +++ /sys/src/cmd/spin/dstep.c Sun Jul 22 04:47:16 2007 @@ -10,11 +10,7 @@ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif #define MAXDSTEP 1024 /* was 512 */ @@ -168,7 +164,10 @@ break; case ELSE: if (inh++ > 0) fprintf(fd, " || "); - fprintf(fd, "(1 /* else */)"); +/* 4.2.5 */ if (Pid != claimnr) + fprintf(fd, "(boq == -1 /* else */)"); + else + fprintf(fd, "(1 /* else */)"); break; case 'R': if (inh++ > 0) fprintf(fd, " || "); @@ -387,7 +386,7 @@ { sprintf(NextOpt, "goto S_%.3d_%d", e->Seqno, i); NextLab[++Level] = NextOpt; - N = (e->n->ntyp == DO) ? e : e->nxt; + N = (e->n && e->n->ntyp == DO) ? e : e->nxt; putCode(fd, h->this->frst, h->this->extent, N, 1); Level--; --- /sys/src/cmd/spin/flow.c Sun Jul 22 04:47:23 2007 +++ /sys/src/cmd/spin/flow.c Sun Jul 22 04:47:22 2007 @@ -10,11 +10,7 @@ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif extern Symbol *Fname; extern int nr_errs, lineno, verbose; --- /sys/src/cmd/spin/guided.c Sun Jul 22 04:47:29 2007 +++ /sys/src/cmd/spin/guided.c Sun Jul 22 04:47:28 2007 @@ -12,11 +12,7 @@ #include "spin.h" #include #include -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif extern RunList *run, *X; extern Element *Al_El; @@ -45,7 +41,12 @@ static int newer(char *f1, char *f2) -{ struct stat x, y; +{ +#if defined(WIN32) || defined(WIN64) + struct _stat x, y; +#else + struct stat x, y; +#endif if (stat(f1, (struct stat *)&x) < 0) return 0; if (stat(f2, (struct stat *)&y) < 0) return 1; @@ -222,7 +223,9 @@ } og = g; } while (g && g != dothis->nxt); - X->pc = g?huntele(g, 0, -1):g; + if (X != NULL) + { X->pc = g?huntele(g, 0, -1):g; + } } else { keepgoing: if (dothis->merge_start) @@ -230,8 +233,10 @@ else a = dothis->merge; - X->pc = eval_sub(dothis); - if (X->pc) X->pc = huntele(X->pc, 0, a); + if (X != NULL) + { X->pc = eval_sub(dothis); + if (X->pc) X->pc = huntele(X->pc, 0, a); + } if (depth >= jumpsteps && ((verbose&32) || ((verbose&4) && not_claim()))) /* -v or -p */ @@ -247,20 +252,20 @@ if (a && (verbose&32)) printf("\t", dothis->merge, - X->pc?X->pc->seqno:-1); + (X && X->pc)?X->pc->seqno:-1); printf("\n"); } if (verbose&1) dumpglobals(); if (verbose&2) dumplocal(X); if (xspin) printf("\n"); - if (!X->pc) + if (X && !X->pc) { X->pc = dothis; printf("\ttransition failed\n"); a = 0; /* avoid inf loop */ } } - if (a && X->pc && X->pc->seqno != a) + if (a && X && X->pc && X->pc->seqno != a) { dothis = X->pc; goto keepgoing; } } --- /sys/src/cmd/spin/main.c Sun Jul 22 04:47:37 2007 +++ /sys/src/cmd/spin/main.c Sun Jul 22 04:47:35 2007 @@ -17,14 +17,11 @@ #include #ifdef PC #include -#include "y_tab.h" - extern int unlink(const char *); - #else #include -#include "y.tab.h" #endif +#include "y.tab.h" extern int DstepStart, lineno, tl_terse; extern FILE *yyin, *yyout, *tl_out; @@ -82,7 +79,7 @@ #ifdef SOLARIS #define CPP "/usr/ccs/lib/cpp" #else -#if defined(__FreeBSD__) || defined(__OpenBSD__) +#if defined(__FreeBSD__) || defined(__OpenBSD__) || defined(__NetBSD__) #define CPP "cpp" #else #define CPP "/bin/cpp" /* classic Unix systems */ @@ -356,7 +353,7 @@ default : usage(); break; } - argc--, argv++; + argc--; argv++; } if (usedopts && !analyze) printf("spin: warning -o[123] option ignored in simulations\n"); @@ -490,13 +487,6 @@ 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"); @@ -514,6 +504,9 @@ emalloc(int n) { char *tmp; + if (n == 0) + return NULL; /* robert shelton 10/20/06 */ + if (!(tmp = (char *) malloc(n))) fatal("not enough memory", (char *)0); memset(tmp, 0, n); @@ -534,7 +527,7 @@ return; if (realread) - n->sym->hidden |= 32; /* var is read at least once */ + n->sym->hidden |= 128; /* var is read at least once */ } void --- /sys/src/cmd/spin/mesg.c Sun Jul 22 04:47:45 2007 +++ /sys/src/cmd/spin/mesg.c Sun Jul 22 04:47:43 2007 @@ -10,11 +10,7 @@ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif #ifndef MAXQ #define MAXQ 2500 /* default max # queues */ @@ -538,11 +534,15 @@ void sr_buf(int v, int j) { int cnt = 1; Lextok *n; - char lbuf[256]; + char lbuf[512]; for (n = Mtype; n && j; n = n->rgt, cnt++) if (cnt == v) - { sprintf(lbuf, "%s", n->lft->sym->name); + { if(strlen(n->lft->sym->name) >= sizeof(lbuf)) + { non_fatal("mtype name %s too long", n->lft->sym->name); + break; + } + sprintf(lbuf, "%s", n->lft->sym->name); strcat(Buf, lbuf); return; } @@ -625,4 +625,20 @@ nochan_manip(p, n->lft, e); nochan_manip(p, n->rgt, 1); +} + +void +no_internals(Lextok *n) +{ char *sp; + + if (!n->sym + || !n->sym->name) + return; + + sp = n->sym->name; + + if ((strlen(sp) == strlen("_nr_pr") && strcmp(sp, "_nr_pr") == 0) + || (strlen(sp) == strlen("_p") && strcmp(sp, "_p") == 0)) + { fatal("attempt to assign value to system variable %s", sp); + } } --- /sys/src/cmd/spin/pangen1.c Sun Jul 22 04:48:03 2007 +++ /sys/src/cmd/spin/pangen1.c Sun Jul 22 04:48:02 2007 @@ -10,11 +10,7 @@ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif #include "pangen1.h" #include "pangen3.h" @@ -372,40 +368,53 @@ Symbol *sp; char buf[64], buf2[128], buf3[128]; - for (j = 0; j < 8; j++) - for (h = 0; h <= 1; h++) - for (walk = all_names; walk; walk = walk->next) - { sp = walk->entry; - if (sp->context - && !sp->owner - && sp->type == Types[j] - && ((h == 0 && sp->nel == 1) || (h == 1 && sp->nel > 1)) - && strcmp(s, sp->context->name) == 0) - { switch (dowhat) { - case LOGV: - if (sp->type == CHAN - && verbose == 0) - break; - sprintf(buf, "%s%s:", pre, s); - { sprintf(buf2, "\", ((P%d *)pptr(h))->", p); - sprintf(buf3, ");\n"); + if (dowhat == INIV) + { /* initialize in order of declaration */ + for (walk = all_names; walk; walk = walk->next) + { sp = walk->entry; + if (sp->context + && !sp->owner + && strcmp(s, sp->context->name) == 0) + { checktype(sp, s); /* fall through */ + if (!(sp->hidden&16)) + { sprintf(buf, "((P%d *)pptr(h))->", p); + do_var(ofd, dowhat, buf, sp, "", " = ", ";\n"); } - do_var(ofd, dowhat, "", sp, buf, buf2, buf3); - break; - case INIV: - checktype(sp, s); /* fall through */ - if (sp->hidden&16) { k++; break; } - case PUTV: - sprintf(buf, "((P%d *)pptr(h))->", p); - do_var(ofd, dowhat, buf, sp, "", " = ", ";\n"); k++; - break; - } - if (strcmp(s, ":never:") == 0) - { printf("error: %s defines local %s\n", - s, sp->name); - nr_errs++; - } } } + } } + } else + { for (j = 0; j < 8; j++) + for (h = 0; h <= 1; h++) + for (walk = all_names; walk; walk = walk->next) + { sp = walk->entry; + if (sp->context + && !sp->owner + && sp->type == Types[j] + && ((h == 0 && sp->nel == 1) || (h == 1 && sp->nel > 1)) + && strcmp(s, sp->context->name) == 0) + { switch (dowhat) { + case LOGV: + if (sp->type == CHAN + && verbose == 0) + break; + sprintf(buf, "%s%s:", pre, s); + { sprintf(buf2, "\", ((P%d *)pptr(h))->", p); + sprintf(buf3, ");\n"); + } + do_var(ofd, dowhat, "", sp, buf, buf2, buf3); + break; + case PUTV: + sprintf(buf, "((P%d *)pptr(h))->", p); + do_var(ofd, dowhat, buf, sp, "", " = ", ";\n"); + k++; + break; + } + if (strcmp(s, ":never:") == 0) + { printf("error: %s defines local %s\n", + s, sp->name); + nr_errs++; + } } } } + return k; } @@ -472,12 +481,17 @@ case UNSIGNED: sputtype(buf, sp->type); if (sp->nel == 1) - fprintf(fd, "\tprintf(\"\t%s %s:\t%%d\\n\", %s%s);\n", - buf, sp->name, pref, sp->name); - else - for (i = 0; i < sp->nel; i++) - fprintf(fd, "\tprintf(\"\t%s %s[%d]:\t%%d\\n\", %s%s[%d]);\n", - buf, sp->name, i, pref, sp->name, i); + { fprintf(fd, "\tprintf(\"\t%s %s:\t%%d\\n\", %s%s);\n", + buf, sp->name, pref, sp->name); + } else + { fprintf(fd, "\t{\tint l_in;\n"); + fprintf(fd, "\t\tfor (l_in = 0; l_in < %d; l_in++)\n", sp->nel); + fprintf(fd, "\t\t{\n"); + fprintf(fd, "\t\t\tprintf(\"\t%s %s[%%d]:\t%%d\\n\", l_in, %s%s[l_in]);\n", + buf, sp->name, pref, sp->name); + fprintf(fd, "\t\t}\n"); + fprintf(fd, "\t}\n"); + } break; case CHAN: if (sp->nel == 1) @@ -499,6 +513,28 @@ } } +int +c_splurge_any(ProcList *p) +{ Ordered *walk; + Symbol *sp; + + if (strcmp(p->n->name, ":never:") != 0 + && strcmp(p->n->name, ":trace:") != 0 + && strcmp(p->n->name, ":notrace:") != 0) + for (walk = all_names; walk; walk = walk->next) + { sp = walk->entry; + if (!sp->context + || sp->type == 0 + || strcmp(sp->context->name, p->n->name) != 0 + || sp->owner || (sp->hidden&1) + || (sp->type == MTYPE && ismtype(sp->name))) + continue; + + return 1; + } + return 0; +} + void c_splurge(FILE *fd, ProcList *p) { Ordered *walk; @@ -511,6 +547,7 @@ for (walk = all_names; walk; walk = walk->next) { sp = walk->entry; if (!sp->context + || sp->type == 0 || strcmp(sp->context->name, p->n->name) != 0 || sp->owner || (sp->hidden&1) || (sp->type == MTYPE && ismtype(sp->name))) @@ -548,7 +585,13 @@ { fprintf(fd, " case %d:\n", p->tn); fprintf(fd, " \tprintf(\"local vars proc %%d (%s):\\n\", pid);\n", p->n->name); - c_splurge(fd, p); + if (c_splurge_any(p)) + { fprintf(fd, " \tprintf(\"local vars proc %%d (%s):\\n\", pid);\n", + p->n->name); + c_splurge(fd, p); + } else + { fprintf(fd, " \t/* none */\n"); + } fprintf(fd, " \tbreak;\n"); } fprintf(fd, " }\n}\n"); @@ -648,16 +691,31 @@ do_init(ofd, sp); fprintf(ofd, "%s", ter); } else - for (i = 0; i < sp->nel; i++) - { fprintf(ofd, "\t\t%s%s%s[%d]%s", - pre, s, sp->name, i, sep); - if (dowhat == LOGV) - fprintf(ofd, "%s%s[%d]", - s, sp->name, i); - else - do_init(ofd, sp); - fprintf(ofd, "%s", ter); - } + { if (sp->ini && sp->ini->ntyp == CHAN) + { for (i = 0; i < sp->nel; i++) + { fprintf(ofd, "\t\t%s%s%s[%d]%s", + pre, s, sp->name, i, sep); + if (dowhat == LOGV) + fprintf(ofd, "%s%s[%d]", + s, sp->name, i); + else + do_init(ofd, sp); + fprintf(ofd, "%s", ter); + } + } else + { fprintf(ofd, "\t{\tint l_in;\n"); + fprintf(ofd, "\t\tfor (l_in = 0; l_in < %d; l_in++)\n", sp->nel); + fprintf(ofd, "\t\t{\n"); + fprintf(ofd, "\t\t\t%s%s%s[l_in]%s", + pre, s, sp->name, sep); + if (dowhat == LOGV) + fprintf(ofd, "%s%s[l_in]", s, sp->name); + else + putstmnt(ofd, sp->ini, 0); + fprintf(ofd, "%s", ter); + fprintf(ofd, "\t\t}\n"); + fprintf(ofd, "\t}\n"); + } } break; } } @@ -753,7 +811,7 @@ { int i = nrRdy; /* 1+ highest proctype nr */ fprintf(th, "#define _NP_ %d\n", i); - if (separate == 2) fprintf(th, "extern "); +/* if (separate == 2) fprintf(th, "extern "); */ fprintf(th, "uchar reached%d[3]; /* np_ */\n", i); fprintf(th, "#define nstates%d 3 /* np_ */\n", i); @@ -861,7 +919,7 @@ Element *elast = (Element *) 0; int cnt = 0; - while (elast != e && cnt++ < 20) /* new 4.0.8 */ + while (elast != e && cnt++ < 200) /* new 4.0.8 */ { elast = e; if (e->n) { if (e->n->ntyp == '.' && e->nxt) @@ -870,7 +928,7 @@ e = e->sub->this->frst; } } - if (cnt >= 20 || !e) + if (cnt >= 200 || !e) fatal("confusing control structure", (char *) 0); return e; } @@ -881,7 +939,7 @@ int cnt=0; /* a precaution against loops */ if (e) - for (cnt = 0; cnt < 20 && e->n; cnt++) + for (cnt = 0; cnt < 200 && e->n; cnt++) { if (e->seqno == stopat) break; @@ -910,7 +968,7 @@ return e; e = g; } - if (cnt >= 20 || !e) + if (cnt >= 200 || !e) fatal("confusing control structure", (char *) 0); return e; } --- /sys/src/cmd/spin/pangen1.h Sun Jul 22 04:48:19 2007 +++ /sys/src/cmd/spin/pangen1.h Sun Jul 22 04:48:15 2007 @@ -1,6 +1,6 @@ /***** spin: pangen1.h *****/ -/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */ +/* Copyright (c) 1989-2005 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 */ @@ -185,7 +185,7 @@ " static char buf[2][2048];", " int i, toggle = 0;", - " if (strlen(s) > 2047) return s;", + " if (!s || strlen(s) > 2047) return s;", " memset(buf[0], 0, 2048);", " memset(buf[1], 0, 2048);", " strcpy(buf[toggle], s);", @@ -225,7 +225,7 @@ " { printf(\"\\t\\t\");", " q = transmognify(t->tp);", - " for ( ; *q; q++)", + " for ( ; q && *q; q++)", " if (*q == '\\n')", " printf(\"\\\\n\");", " else", @@ -241,12 +241,12 @@ "", " if (wrap_in_progress++) return;", "", - " printf(\"spin: trail ends after %%d steps\\n\", depth);", + " printf(\"spin: trail ends after %%ld steps\\n\", depth);", " if (onlyproc >= 0)", " { if (onlyproc >= now._nr_pr) pan_exit(0);", " II = onlyproc;", " z = (P0 *)pptr(II);", - " printf(\"%%3d:\tproc %%d (%%s) \",", + " printf(\"%%3ld:\tproc %%d (%%s) \",", " depth, II, procname[z->_t]);", " for (i = 0; src_all[i].src; i++)", " if (src_all[i].tp == (int) z->_t)", @@ -265,7 +265,7 @@ " if (depth < 0) depth = 0;", " for (II = 0; II < now._nr_pr; II++)", " { z = (P0 *)pptr(II);", - " printf(\"%%3d:\tproc %%d (%%s) \",", + " printf(\"%%3ld:\tproc %%d (%%s) \",", " depth, II, procname[z->_t]);", " for (i = 0; src_all[i].src; i++)", " if (src_all[i].tp == (int) z->_t)", @@ -293,30 +293,34 @@ "findtrail(void)", "{ FILE *fd;", " char fnm[512], *q;", + " char MyFile[512];", + "", + " strcpy(MyFile, TrailFile);", /* avoid problem with non-writable strings */ + "", " if (whichtrail)", - " { sprintf(fnm, \"%%s%%d.%%s\", TrailFile, whichtrail, tprefix);", + " { sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);", " fd = fopen(fnm, \"r\");", - " if (fd == NULL && (q = strchr(TrailFile, \'.\')))", + " if (fd == NULL && (q = strchr(MyFile, \'.\')))", " { *q = \'\\0\';", /* e.g., strip .pml on original file */ - " sprintf(fnm, \"%%s%%d.%%s\", TrailFile, whichtrail, tprefix);", + " sprintf(fnm, \"%%s%%d.%%s\", MyFile, whichtrail, tprefix);", " *q = \'.\';", " fd = fopen(fnm, \"r\");", " if (fd == NULL)", " { printf(\"pan: cannot find %%s%%d.%%s or %%s\\n\", ", - " TrailFile, whichtrail, tprefix, fnm);", + " MyFile, whichtrail, tprefix, fnm);", " pan_exit(1);", " } }", " } else", - " { sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);", + " { sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);", " fd = fopen(fnm, \"r\");", - " if (fd == NULL && (q = strchr(TrailFile, \'.\')))", + " if (fd == NULL && (q = strchr(MyFile, \'.\')))", " { *q = \'\\0\';", /* e.g., strip .pml on original file */ - " sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);", + " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);", " *q = \'.\';", " fd = fopen(fnm, \"r\");", " if (fd == NULL)", " { printf(\"pan: cannot find %%s.%%s or %%s\\n\", ", - " TrailFile, tprefix, fnm);", + " MyFile, tprefix, fnm);", " pan_exit(1);", " } } }", " if (fd == NULL)", @@ -337,11 +341,16 @@ " P0 *z;", "", " fd = findtrail(); /* exits if unsuccessful */", - " while (fscanf(fd, \"%%d:%%d:%%d\\n\", &depth, &i, &t_id) == 3)", + " while (fscanf(fd, \"%%ld:%%d:%%d\\n\", &depth, &i, &t_id) == 3)", " { if (depth == -1)", " printf(\"<<<<>>>>\\n\");", " if (depth < 0)", " continue;", + " if (i > now._nr_pr)", + " { printf(\"pan: Error, proc %%d invalid pid \", i);", + " printf(\"transition %%d\\n\", t_id);", + " break;", + " }", " II = i;", "", " z = (P0 *)pptr(II);", @@ -382,7 +391,7 @@ " goto moveon;", " if (verbose)", - " { printf(\"depth: %%3d proc: %%3d trans: %%3d (%%d procs) \",", + " { printf(\"depth: %%3ld proc: %%3d trans: %%3d (%%d procs) \",", " depth, II, t_id, now._nr_pr);", " printf(\"forw=%%3d [%%s]\\n\", t->forw, q);", "", @@ -409,14 +418,14 @@ " {", "sameas: if (no_rck) goto moveon;", " if (coltrace)", - " { printf(\"%%d: \", depth);", + " { printf(\"%%ld: \", depth);", " for (i = 0; i < II; i++)", " printf(\"\\t\\t\");", " printf(\"%%s(%%d):\", procname[z->_t], II);", - " printf(\"[%%s]\\n\", q);", - " } else", + " printf(\"[%%s]\\n\", q?q:\"\");", + " } else if (!silent)", " { if (strlen(simvals) > 0) {", - " printf(\"%%3d: proc %%2d (%%s)\", ", + " printf(\"%%3ld: proc %%2d (%%s)\", ", " depth, II, procname[z->_t]);", " for (i = 0; src_all[i].src; i++)", " if (src_all[i].tp == (int) z->_t)", @@ -426,7 +435,7 @@ " }", " printf(\"(state %%d)\t[values: %%s]\\n\", z->_p, simvals);", " }", - " printf(\"%%3d: proc %%2d (%%s)\", ", + " printf(\"%%3ld: proc %%2d (%%s)\", ", " depth, II, procname[z->_t]);", " for (i = 0; src_all[i].src; i++)", " if (src_all[i].tp == (int) z->_t)", @@ -434,7 +443,7 @@ " src_all[i].src[z->_p]);", " break;", " }", - " printf(\"(state %%d)\t[%%s]\\n\", z->_p, q);", + " printf(\"(state %%d)\t[%%s]\\n\", z->_p, q?q:\"\");", " printf(\"\\n\");", " } }", "moveon: z->_p = t->st;", @@ -491,6 +500,9 @@ "#ifdef DEBUG", " printf(\"New bitstate\\n\");", "#endif", + " if (now._a_t&1)", + " { nShadow++;", + " }", " return 0;", "}", #endif @@ -526,6 +538,9 @@ "#ifdef DEBUG", " printf(\"New bitstate\\n\");", "#endif", + " if (now._a_t&1)", + " { nShadow++;", + " }", " return 0;", "}", "#endif", @@ -538,30 +553,35 @@ "make_trail(void)", "{ int fd;", " char *q;", + " char MyFile[512];", + "", + " q = strrchr(TrailFile, \'/\');", + " if (q == NULL) q = TrailFile; else q++;", + " strcpy(MyFile, q); /* TrailFile is not a writable string */", "", " if (iterative == 0 && Nr_Trails++ > 0)", " sprintf(fnm, \"%%s%%d.%%s\",", - " TrailFile, Nr_Trails-1, tprefix);", + " MyFile, Nr_Trails-1, tprefix);", " else", - " sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);", + " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);", "", - " if ((fd = creat(fnm, (unsigned short) TMODE)) < 0)", - " { if ((q = strchr(TrailFile, \'.\')))", + " if ((fd = creat(fnm, TMODE)) < 0)", + " { if ((q = strchr(MyFile, \'.\')))", " { *q = \'\\0\';", /* strip .pml */ " if (iterative == 0 && Nr_Trails-1 > 0)", " sprintf(fnm, \"%%s%%d.%%s\",", - " TrailFile, Nr_Trails-1, tprefix);", + " MyFile, Nr_Trails-1, tprefix);", " else", - " sprintf(fnm, \"%%s.%%s\", TrailFile, tprefix);", + " sprintf(fnm, \"%%s.%%s\", MyFile, tprefix);", " *q = \'.\';", - " fd = creat(fnm, (unsigned short) TMODE);", + " fd = creat(fnm, TMODE);", " } }", " if (fd < 0)", - " { printf(\"cannot create %%s\\n\", fnm);", + " { printf(\"pan: cannot create %%s\\n\", fnm);", " perror(\"cause\");", " } else", - " printf(\"pan: wrote %%s\\n\", fnm);", - "", + " { printf(\"pan: wrote %%s\\n\", fnm);", + " }", " return fd;", "}", 0 @@ -569,7 +589,7 @@ static char *Code2b[] = { /* breadth-first search option */ "#ifdef BFS", - "#define QPROVISO", + "#define Q_PROVISO", "#ifndef INLINE_REV", "#define INLINE_REV", "#endif", @@ -585,8 +605,13 @@ " int sz;", /* vsize */ " int nrpr;", " int nrqs;", - " int *po, *ps;", - " int *qo, *qs;", + "#if VECTORSZ>32000", + " int *po;", + "#else", + " short *po;", + "#endif", + " int *qo;", + " uchar *ps, *qs;", " struct EV_Hold *nxt;", "} EV_Hold;", "", @@ -594,7 +619,7 @@ " Trail *frame;", " SV_Hold *onow;", " EV_Hold *omask;", - "#ifdef QPROVISO", + "#ifdef Q_PROVISO", " struct H_el *lstate;", "#endif", " short boq;", @@ -647,10 +672,15 @@ " && (memcmp((char *) Mask, (char *) h->sv, n) == 0)", " && (now._nr_pr == h->nrpr)", " && (now._nr_qs == h->nrqs)", + "#if VECTORSZ>32000", " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(int)) == 0)", - " && (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(int)) == 0)", " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(int)) == 0)", - " && (memcmp((char *) q_skip, (char *) h->qs, now._nr_qs * sizeof(int)) == 0))", + "#else", + " && (memcmp((char *) proc_offset, (char *) h->po, now._nr_pr * sizeof(short)) == 0)", + " && (memcmp((char *) q_offset, (char *) h->qo, now._nr_qs * sizeof(short)) == 0)", + "#endif", + " && (memcmp((char *) proc_skip, (char *) h->ps, now._nr_pr * sizeof(uchar)) == 0)", + " && (memcmp((char *) q_skip, (char *) h->qs, now._nr_qs * sizeof(uchar)) == 0))", " break;", " if (!h)", " { h = (EV_Hold *) emalloc(sizeof(EV_Hold));", @@ -664,14 +694,22 @@ " if (now._nr_pr > 0)", " { h->po = (int *) emalloc(now._nr_pr * sizeof(int));", " h->ps = (int *) emalloc(now._nr_pr * sizeof(int));", + "#if VECTORSZ>32000", " memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(int));", - " memcpy((char *) h->ps, (char *) proc_skip, now._nr_pr * sizeof(int));", + "#else", + " memcpy((char *) h->po, (char *) proc_offset, now._nr_pr * sizeof(short));", + "#endif", + " memcpy((char *) h->ps, (char *) proc_skip, now._nr_pr * sizeof(uchar));", " }", " if (now._nr_qs > 0)", " { h->qo = (int *) emalloc(now._nr_qs * sizeof(int));", " h->qs = (int *) emalloc(now._nr_qs * sizeof(int));", + "#if VECTORSZ>32000", " memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(int));", - " memcpy((char *) h->qs, (char *) q_skip, now._nr_qs * sizeof(int));", + "#else", + " memcpy((char *) h->qo, (char *) q_offset, now._nr_qs * sizeof(short));", + "#endif", + " memcpy((char *) h->qs, (char *) q_skip, now._nr_qs * sizeof(uchar));", " }", "", " h->nxt = kept;", @@ -725,7 +763,7 @@ " t->onow = getsv(vsize);", " memcpy((char *)t->onow->sv, (char *)&now, vsize);", " t->omask = getsv_mask(vsize);", - "#if defined(FULLSTACK) && defined(QPROVISO)", + "#if defined(FULLSTACK) && defined(Q_PROVISO)", " t->lstate = Lstate;", "#endif", " if (!bfs_bot)", @@ -750,7 +788,7 @@ " bfs_trail = t->nxt;", " if (!bfs_trail)", " bfs_bot = (BFS_Trail *) 0;", - "#if defined(QPROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)", + "#if defined(Q_PROVISO) && !defined(BITSTATE) && !defined(NOREDUCE)", " if (t->lstate) t->lstate->tagged = 0;", "#endif", "", @@ -764,12 +802,20 @@ " memcpy((uchar *) Mask, (uchar *) t->omask->sv, vsize);", " if (now._nr_pr > 0)", + "#if VECTORSZ>32000", " { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(int));", - " memcpy((char *)proc_skip, (char *)t->omask->ps, now._nr_pr * sizeof(int));", + "#else", + " { memcpy((char *)proc_offset, (char *)t->omask->po, now._nr_pr * sizeof(short));", + "#endif", + " memcpy((char *)proc_skip, (char *)t->omask->ps, now._nr_pr * sizeof(uchar));", " }", " if (now._nr_qs > 0)", + "#if VECTORSZ>32000", " { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(int));", - " memcpy((uchar *)q_skip, (uchar *)t->omask->qs, now._nr_qs * sizeof(int));", + "#else", + " { memcpy((uchar *)q_offset, (uchar *)t->omask->qo, now._nr_qs * sizeof(short));", + "#endif", + " memcpy((uchar *)q_skip, (uchar *)t->omask->qs, now._nr_qs * sizeof(uchar));", " }", " freesv(t->onow); /* omask not freed */", @@ -867,7 +913,7 @@ " } else", " { truncs++;", - "#if !defined(NOREDUCE) && defined(FULLSTACK) && defined(QPROVISO)", + "#if !defined(NOREDUCE) && defined(FULLSTACK) && defined(Q_PROVISO)", "#if !defined(QLIST) && !defined(BITSTATE)", " if (Lstate && Lstate->tagged) trpt->tau |= 64;", "#else", @@ -893,9 +939,11 @@ "#endif", "}", "", + "Trail *ntrpt;", /* 4.2.8 */ + "", "void", "bfs(void)", - "{ Trans *t; Trail *ntrpt, *otrpt, *x;", + "{ Trans *t; Trail *otrpt, *x;", " uchar _n, _m, ot, nps = 0;", " int tt, E_state;", " short II, From = (short) (now._nr_pr-1), To = BASE;", @@ -1199,13 +1247,15 @@ " j = strlen(snap);", " if (write(fd, snap, j) != j)", " { printf(\"pan: error writing %%s\\n\", fnm);", - " exit(1);", + " pan_exit(1);", " } }", "}", "", "void", "nuerror(char *str)", "{ int fd = make_trail();", + " int j;", + "", " if (fd < 0) return;", "#ifdef VERI", " sprintf(snap, \"-2:%%d:-2\\n\", VERI);", @@ -1217,9 +1267,19 @@ "#endif", " trcnt = 1;", " putter(trpt, fd);", + " if (ntrpt->o_t)", /* 4.2.8 -- Alex example, missing last transition */ + " { sprintf(snap, \"%%d:%%d:%%d\\n\",", + " trcnt++, ntrpt->pr, ntrpt->o_t->t_id);", + " j = strlen(snap);", + " if (write(fd, snap, j) != j)", + " { printf(\"pan: error writing %%s\\n\", fnm);", + " pan_exit(1);", + " } }", " close(fd);", " if (errors >= upto && upto != 0)", + " {", " wrapup();", + " }", "}", "#endif", /* BFS */ 0, @@ -1398,7 +1458,7 @@ "#endif", " }", "#ifdef NEGATED_TRACE", - " now._event = start_event; /* only 1st try will count */", + " now._event = endevent; /* only 1st try will count -- fixed 4.2.6 */", "#else", "#ifndef BFS", " depth++; trpt++;", @@ -1456,7 +1516,7 @@ "stack2disk(void)", "{", " if (!stackwrite", - " && (stackwrite = creat(stackfile, 0666)) < 0)", + " && (stackwrite = creat(stackfile, TMODE)) < 0)", " Uerror(\"cannot create stackfile\");", "", " if (write(stackwrite, trail, DDD*sizeof(Trail))", @@ -1563,7 +1623,8 @@ " }", "AllOver:", "#if defined(FULLSTACK) && !defined(MA)", - " trpt->ostate = (struct H_el *) 0;", + " /* if atomic or rv move, carry forward previous state */", + " trpt->ostate = (trpt-1)->ostate;", /* was: = (struct H_el *) 0;*/ "#endif", "#ifdef VERI", " if ((trpt->tau&4) || ((trpt-1)->tau&128))", @@ -1628,8 +1689,22 @@ "#endif", "#endif", " kk = (II == 1 || II == 2);", - + /* II==0 new state */ + /* II==1 old state */ + /* II==2 on current dfs stack */ + /* II==3 on 1st dfs stack */ "#ifndef SAFETY", + + " if (!fairness && a_cycles)", + " if (II == 2 && ((trpt->o_pm&2) || ((trpt-1)->o_pm&2)))", + " { II = 3; /* Schwoon & Esparza 2005, Gastin&Moro 2004 */", + "#ifdef VERBOSE", + " printf(\"state match on dfs stack\\n\");", + "#endif", + " goto same_case;", + " }", + + "#if defined(FULLSTACK) && defined(BITSTATE)", " if (!JJ && (now._a_t&1) && depth > A_depth)", " { int oj1 = j1;", @@ -1657,12 +1732,10 @@ " } else", "#endif", " {", - "#ifdef BITSTATE", - " depthfound = Lstate->tagged - 1;", - "#else", - " depthfound = depth_of(Lstate);", + "#ifndef BITSTATE", " nShadow--;", "#endif", + "same_case: if (Lstate) depthfound = Lstate->D;", "#ifdef NP", " uerror(\"non-progress cycle\");", "#else", @@ -2736,7 +2809,6 @@ "#endif", "#endif", - " signal(SIGINT, SIG_DFL);", " printf(\"(%%s)\\n\", Version);", " if (!done) printf(\"Warning: Search not completed\\n\");", @@ -2750,7 +2822,7 @@ " printf(\" + Partial Order Reduction\\n\");", "#endif", #if 0 - "#ifdef QPROVISO", + "#ifdef Q_PROVISO", " printf(\" + Queue Proviso\\n\");", "#endif", #endif @@ -2925,7 +2997,7 @@ " { printf(\"\tState-vector as stored = %%.0f byte\",", " (tmp_nr)/(nstates-nShadow) -", " (double) (sizeof(struct H_el) - sizeof(unsigned)));", - " printf(\" + %%d byte overhead\\n\",", + " printf(\" + %%ld byte overhead\\n\",", " sizeof(struct H_el)-sizeof(unsigned));", " }", "#endif", @@ -2936,8 +3008,9 @@ "#endif", "#endif", "#ifndef BFS", - " printf(\"%%-6.3f\tmemory used for DFS stack (-m%%d)\\n\",", + " printf(\"%%-6.3f\tmemory used for DFS stack (-m%%ld)\\n\",", " nr2/1000000., maxdepth);", + " remainder = remainder - nr2;", "#endif", " if (remainder - fragment > 0.0)", " printf(\"%%-6.3f\tother (proc and chan stacks)\\n\",", @@ -2986,13 +3059,14 @@ "stopped(int arg)", "{ printf(\"Interrupted\\n\");", " wrapup();", + " pan_exit(0);", "}", "/*", " * based on Bob Jenkins hash-function from 1996", " * see: http://www.burtleburtle.net/bob/", " */", "", -"#ifdef HASH64", +"#if defined(HASH64) || defined(WIN64)", /* 64-bit Jenkins hash: http://burtleburtle.net/bob/c/lookup8.c */ "#define mix(a,b,c) \\", "{ a -= b; a -= c; a ^= (c>>43); \\", @@ -3148,6 +3222,7 @@ " case 'P': readtrail = 1; onlyproc = atoi(&argv[1][2]); break;", " case 'C': coltrace = 1; goto samething;", " case 'g': gui = 1; goto samething;", + " case 'S': silent = 1; break;", "#endif", " case 'R': Nrun = atoi(&argv[1][2]); break;", "#ifdef BITSTATE", @@ -3161,10 +3236,20 @@ " case 'w': ssize = atoi(&argv[1][2]); break;", " case 'Y': signoff = 1; break;", " case 'X': efd = stdout; break;", - " default : usage(efd); break;", + " default : fprintf(efd, \"saw option -%%c\\n\", argv[1][1]); usage(efd); break;", " }", " argc--; argv++;", " }", + " if (iterative && TMODE != 0666)", + " { TMODE = 0666;", + " fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");", + " }", + "#if defined(WIN32) || defined(WIN64)", + " if (TMODE == 0666)", + " TMODE = _S_IWRITE | _S_IREAD;", + " else", + " TMODE = _S_IREAD;", + "#endif", "#ifdef OHASH", " fprintf(efd, \"warning: -DOHASH no longer supported (directive ignored)\\n\");", "#endif", @@ -3208,10 +3293,6 @@ " }", "#endif", - " if (iterative && TMODE != 0666)", - " { TMODE = 0666;", - " fprintf(efd, \"warning: -T ignored when -i or -I is used\\n\");", - " }", "#ifdef SC", " hiwater = HHH = maxdepth-10;", " DDD = HHH/2;", @@ -3375,14 +3456,18 @@ "#endif", "#if SYNC>0 && !defined(NOREDUCE)", - "#ifdef HAS_UNLESS", + "#ifdef HAS_UNLESS", " fprintf(efd, \"warning: use of a rendezvous stmnts in the escape\\n\");", " fprintf(efd, \"\tof an unless clause, if present, could make p.o. reduction\\n\");", " fprintf(efd, \"\tinvalid (use -DNOREDUCE to avoid this)\\n\");", - "#ifdef BFS", + "#ifdef BFS", " fprintf(efd, \"\t(this type of rv is also not compatible with -DBFS)\\n\");", + "#endif", + "#endif", "#endif", - "#endif", + "#if SYNC>0 && defined(BFS)", + " fprintf(efd, \"warning: use of rendezvous in BFS mode \");", + " fprintf(efd, \"does not preserve all invalid endstates\\n\");", "#endif", "#if !defined(REACH) && !defined(BITSTATE)", " if (iterative != 0 && a_cycles == 0)", @@ -3467,7 +3552,7 @@ " nmask = mask;", "#endif", " } else if (WS != 4)", - " { fprintf(stderr, \"pan: wordsize %%d not supported\\n\", WS);", + " { fprintf(stderr, \"pan: wordsize %%ld not supported\\n\", WS);", " exit(1);", " } else /* WS == 4 and ssize < 32 */", " { mask = ((1L< 0)", " { maxdepth = (iterative == 1)?(depth-1):(depth/2);", " warned = 1;", - " printf(\"pan: reducing search depth to %%d\\n\",", + " printf(\"pan: reducing search depth to %%ld\\n\",", " maxdepth);", " } else", "#endif", @@ -3837,7 +3923,7 @@ "}\n", "int", "xrefsrc(int lno, S_F_MAP *mp, int M, int i)", - "{ Trans *T; int j;", + "{ Trans *T; int j, retval=1;", " for (T = trans[M][i]; T; T = T->nxt)", " if (T && T->tp)", " { if (strcmp(T->tp, \".(goto)\") == 0", @@ -3855,12 +3941,13 @@ " if (strcmp(T->tp, \"\") != 0)", " { char *q;", " q = transmognify(T->tp);", - " printf(\", \\\"%%s\\\"\", q);", + " printf(\", \\\"%%s\\\"\", q?q:\"\");", " } else if (stopstate[M][i])", " printf(\", -end state-\");", " printf(\"\\n\");", + " retval = 0; /* reported */", " }", - " return 0;", + " return retval;", "}\n", "void", "r_ck(uchar *which, int N, int M, short *src, S_F_MAP *mp)", @@ -3886,7 +3973,9 @@ "putrail(void)", "{ int fd; long i, j;", " Trail *trl;", + "#if defined VERI || defined(MERGED)", " char snap[64];", + "#endif", "", " fd = make_trail();", " if (fd < 0) return;", @@ -3904,7 +3993,7 @@ " trl = getframe(i);", " if (!trl->o_t) continue;", " if (trl->o_pm&128) continue;", - " sprintf(snap, \"%%d:%%d:%%d\\n\", ", + " sprintf(snap, \"%%ld:%%d:%%d\\n\", ", " i, trl->pr, trl->o_t->t_id);", " j = strlen(snap);", " if (write(fd, snap, j) != j)", @@ -3970,7 +4059,7 @@ "p_restor(int h)", "{ int i; char *z = (char *) &now;\n", " proc_offset[h] = stack->o_offset;", - " proc_skip[h] = stack->o_skip;", + " proc_skip[h] = (uchar) stack->o_skip;", "#ifndef XUSAFE", " p_name[h] = stack->o_name;", "#endif", @@ -4009,7 +4098,7 @@ " int k, k_end;", "#endif", " q_offset[now._nr_qs] = stack->o_offset;", - " q_skip[now._nr_qs] = stack->o_skip;", + " q_skip[now._nr_qs] = (uchar) stack->o_skip;", "#ifndef XUSAFE", " q_name[now._nr_qs] = stack->o_name;", "#endif", @@ -4092,7 +4181,11 @@ " }", " stack = stack->nxt;", " stack->o_offset = proc_offset[h];", - " stack->o_skip = proc_skip[h];", + "#if VECTORSZ>32000", + " stack->o_skip = (int) proc_skip[h];", + "#else", + " stack->o_skip = (short) proc_skip[h];", + "#endif", "#ifndef XUSAFE", " stack->o_name = p_name[h];", "#endif", @@ -4103,7 +4196,7 @@ " vsize = proc_offset[h];", " now._nr_pr = now._nr_pr - 1;", " memset((char *)pptr(h), 0, d);", - " vsize -= proc_skip[h];", + " vsize -= (int) proc_skip[h];", "#ifndef NOVSZ", " now._vsz = vsize;", "#endif", @@ -4131,7 +4224,11 @@ " }", " stack = stack->nxt;", " stack->o_offset = q_offset[h];", - " stack->o_skip = q_skip[h];", + "#if VECTORSZ>32000", + " stack->o_skip = (int) q_skip[h];", + "#else", + " stack->o_skip = (short) q_skip[h];", + "#endif", "#ifndef XUSAFE", " stack->o_name = q_name[h];", "#endif", @@ -4141,7 +4238,7 @@ " vsize = q_offset[h];", " now._nr_qs = now._nr_qs - 1;", " memset((char *)qptr(h), 0, d);", - " vsize -= q_skip[h];", + " vsize -= (int) q_skip[h];", "#ifndef NOVSZ", " now._vsz = vsize;", "#endif", @@ -4218,7 +4315,6 @@ " memcpy((char *)&A_Root, (char *)&now, vsize);", " A_depth = depthfound = depth;", " new_state(); /* start 2nd DFS */", - " now._a_t = o_a_t;", "#ifndef NOFAIR", " now._cnt[1] = o_cnt;", @@ -4240,13 +4336,7 @@ "struct H_el *Free_list = (struct H_el *) 0;", "void", "onstack_init(void) /* to store stack states in a bitstate search */", - "{ S_Tab = (struct H_el **)", -#if 0 - " emalloc((1L<<(ssize-3))*sizeof(struct H_el *));", - /* can lead to excessive memory use */ -#else - " emalloc(maxdepth*sizeof(struct H_el *));", -#endif + "{ S_Tab = (struct H_el **) emalloc(maxdepth*sizeof(struct H_el *));", "}", "struct H_el *", "grab_state(int n)", @@ -4582,7 +4672,7 @@ " for (w = Free_list; w; Fa++, last=w, w = w->nxt)", " { if ((int) w->tagged <= n)", " { if (last)", - " { v->nxt = w->nxt;", + " { v->nxt = w; /* was: v->nxt = w->nxt; */", " last->nxt = v;", " } else", " { v->nxt = Free_list;", @@ -4635,7 +4725,7 @@ " for (tmp = S_Tab[j1]; tmp; Zn++, tmp = tmp->nxt)", " { m = memcmp(((char *)&(tmp->state)),v,n);", " if (m <= 0)", - " { Lstate = tmp;", + " { Lstate = (struct H_el *) tmp;", " break;", " } }", " PROBE++;", @@ -4787,6 +4877,9 @@ "hstore(char *vin, int nin) /* hash table storage */", "{ struct H_el *tmp, *ntmp, *olst = (struct H_el *) 0;", " char *v; int n, m=0;", + "#ifdef HC", + " uchar rem_a;", + "#endif", "#ifdef NOCOMP", /* defined by BITSTATE */ "#if defined(BITSTATE) && defined(LC)", " if (S_Tab == H_tab)", @@ -4800,7 +4893,14 @@ "#endif", "#else", " v = (char *) &comp_now;", + " #ifdef HC", + " rem_a = now._a_t;", /* 4.3.0 */ + " now._a_t = 0;", /* for hashing/state matching to work right */ + " #endif", " n = compress(vin, nin);", /* with HC, this calls s_hash */ + " #ifdef HC", + " now._a_t = rem_a;", /* 4.3.0 */ + " #endif", "#ifndef SAFETY", " if (S_A)", " { v[0] = 0; /* _a_t */", @@ -4874,7 +4974,7 @@ "#ifdef FULLSTACK", "#ifndef SAFETY", /* or else wasnew == 0 */ " if (wasnew)", - " { Lstate = tmp;", + " { Lstate = (struct H_el *) tmp;", " tmp->tagged |= V_A;", " if ((now._a_t&1)", " && (tmp->tagged&A_V)", @@ -4897,7 +4997,7 @@ " } else", "#endif", " if ((S_A)?(tmp->tagged&V_A):tmp->tagged)", - " { Lstate = tmp;", + " { Lstate = (struct H_el *) tmp;", "#ifndef SAFETY", " /* already on current dfs stack */", " /* but may also be on 1st dfs stack */", @@ -4962,8 +5062,8 @@ " return 0;", " }", "#endif", - "#if defined(BFS) && defined(QPROVISO)", - " Lstate = tmp;", + "#if defined(BFS) && defined(Q_PROVISO)", + " Lstate = (struct H_el *) tmp;", "#endif", " return 1; /* match outside stack */", " } else if (m < 0)", @@ -4994,7 +5094,7 @@ " printf(\" New state %%d\\n\", (int) nstates);", "#endif", "#endif", - "#ifdef REACH", + "#if !defined(SAFETY) || defined(REACH)", " tmp->D = depth;", "#endif", "#ifndef SAFETY", @@ -5022,7 +5122,7 @@ "#ifdef DEBUG", " dumpstate(-1, v, n, tmp->tagged);", "#endif", - " Lstate = tmp;", + " Lstate = (struct H_el *) tmp;", "#else", "#ifdef DEBUG", " dumpstate(-1, v, n, 0);", --- /sys/src/cmd/spin/pangen2.c Sun Jul 22 04:48:33 2007 +++ /sys/src/cmd/spin/pangen2.c Sun Jul 22 04:48:30 2007 @@ -11,11 +11,7 @@ #include "spin.h" #include "version.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif #include "pangen2.h" #include "pangen4.h" #include "pangen5.h" @@ -186,15 +182,15 @@ fprintf(th, "#define uint unsigned int\n"); fprintf(th, "#endif\n"); - if (sizeof(long) > 4) /* 64 bit machine */ + if (sizeof(void *) > 4) /* 64 bit machine */ { fprintf(th, "#ifndef HASH32\n"); fprintf(th, "#define HASH64\n"); fprintf(th, "#endif\n"); } - +#if 0 if (sizeof(long)==sizeof(int)) fprintf(th, "#define long int\n"); - +#endif if (separate == 1 && !claimproc) { Symbol *n = (Symbol *) emalloc(sizeof(Symbol)); Sequence *s = (Sequence *) emalloc(sizeof(Sequence)); @@ -314,6 +310,8 @@ 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"); @@ -408,6 +406,7 @@ for (p = rdy; p; p = p->nxt) putproc(p); + if (separate != 2) { fprintf(th, "struct {\n"); fprintf(th, " int tp; short *src;\n"); @@ -417,6 +416,9 @@ p->tn, p->tn); fprintf(th, " { 0, (short *) 0 }\n"); fprintf(th, "};\n"); + fprintf(th, "short *frm_st0;\n"); /* records src states for transitions in never claim */ + } else + { fprintf(th, "extern short *frm_st0;\n"); } gencodetable(th); @@ -472,8 +474,12 @@ fprintf(th, "#define REVERSE_MOVES\t\"pan_t.b\"\n"); fprintf(th, "#define TRANSITIONS\t\"pan_t.t\"\n"); fprintf(tc, "extern int Maxbody;\n"); + fprintf(tc, "#if VECTORSZ>32000\n"); fprintf(tc, "extern int proc_offset[];\n"); - fprintf(tc, "extern int proc_skip[];\n"); + fprintf(tc, "#else\n"); + fprintf(tc, "extern short proc_offset[];\n"); + fprintf(tc, "#endif\n"); + fprintf(tc, "extern uchar proc_skip[];\n"); fprintf(tc, "extern uchar *reached[];\n"); fprintf(tc, "extern uchar *accpstate[];\n"); fprintf(tc, "extern uchar *progstate[];\n"); @@ -714,7 +720,12 @@ if (Pid == claimnr && separate == 1) { fprintf(th, "extern uchar reached%d[];\n", Pid); +#if 0 fprintf(th, "extern short nstates%d;\n", Pid); +#else + fprintf(th, "\n#define nstates%d %d\t/* %s */\n", + Pid, p->s->maxel, p->n->name); +#endif fprintf(th, "extern short src_ln%d[];\n", Pid); fprintf(th, "extern S_F_MAP src_file%d[];\n", Pid); fprintf(th, "#define endstate%d %d\n", @@ -731,7 +742,7 @@ AllGlobal = (p->prov)?1:0; /* process has provided clause */ - fprintf(th, "\nshort nstates%d=%d;\t/* %s */\n", + fprintf(th, "\n#define nstates%d %d\t/* %s */\n", Pid, p->s->maxel, p->n->name); if (Pid == claimnr) fprintf(th, "#define nstates_claim nstates%d\n", Pid); @@ -826,7 +837,8 @@ static int getNid(Lextok *n) { - if (n->sym->type == STRUCT + if (n->sym + && n->sym->type == STRUCT && n->rgt && n->rgt->lft) return getNid(n->rgt->lft); @@ -1470,6 +1482,22 @@ memset(CnT, 0, sizeof(CnT)); YZmax = YZcnt = 0; +/* NEW 4.2.6 */ + if (Pid == claimnr) + { + fprintf(tm, "\n#if defined(VERI) && !defined(NP)\n\t\t"); + fprintf(tm, "{ static int reported%d = 0;\n\t\t", e->seqno); + /* source state changes in retrans and must be looked up in frm_st0[t->forw] */ + fprintf(tm, " if (verbose && !reported%d)\n\t\t", e->seqno); + fprintf(tm, " { printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",\n\t\t"); + fprintf(tm, " depth, frm_st0[t->forw], src_claim[%d]);\n\t\t", e->seqno); + fprintf(tm, " reported%d = 1;\n\t\t", e->seqno); + fprintf(tm, " fflush(stdout);\n\t\t"); + fprintf(tm, "} }\n"); + fprintf(tm, "#endif\n\t\t"); + } +/* end */ + /* the src xrefs have the numbers in e->seqno builtin */ fprintf(tm, "reached[%d][%d] = 1;\n\t\t", Pid, e->seqno); @@ -1838,7 +1866,9 @@ break; case BREAK: if (e->nxt) - f = find_target(huntele(e->nxt, e->status, -1)); + { f = find_target(huntele(e->nxt, e->status, -1)); + break; /* 4.3.0 -- was missing */ + } /* else fall through */ default: f = e; @@ -1867,13 +1897,19 @@ || has_global(f->n)) return 1; if (f->n->ntyp == GOTO) /* may reach other atomic */ - { g = target(f); + { +#if 0 + /* if jumping from an atomic without globals into + * one with globals, this does the wrong thing + * example by Claus Traulsen, 22 June 2007 + */ + g = target(f); if (g && !(f->status & L_ATOM) && !(g->status & (ATOM|L_ATOM))) - { fprintf(tt, " /* goto mark-down, "); - fprintf(tt, "line %d - %d */\n", - f->n->ln, (g->n)?g->n->ln:0); +#endif + { fprintf(tt, " /* mark-down line %d */\n", + f->n->ln); return 1; /* assume worst case */ } } for (h = f->sub; h; h = h->nxt) @@ -2055,9 +2091,10 @@ for (v = now->lft, i = 0; v; v = v->rgt, i++) { cat2(", ", v->lft); } + check_param_count(i, now); if (i > Npars) - { printf(" %d parameters used, %d expected\n", i, Npars); + { printf("\t%d parameters used, max %d expected\n", i, Npars); fatal("too many parameters in run %s(...)", now->sym->name); } @@ -2703,7 +2740,11 @@ case C_EXPR: fprintf(fd, "("); plunk_expr(fd, now->sym->name); +#if 1 + fprintf(fd, ")"); +#else fprintf(fd, ") /* %s */ ", now->sym->name); +#endif break; case C_CODE: @@ -2943,4 +2984,13 @@ fatal("more than one run operator in expression", ""); if (runcount == 1 && opcount > 1) fatal("use of run operator in compound expression", ""); +} + +void +any_runs(Lextok *n) +{ + runcount = opcount = 0; + do_count(n, 0); + if (runcount >= 1) + fatal("run operator used in invalid context", ""); } --- /sys/src/cmd/spin/pangen2.h Sun Jul 22 04:48:46 2007 +++ /sys/src/cmd/spin/pangen2.h Sun Jul 22 04:48:45 2007 @@ -34,18 +34,22 @@ "#include ", "#include ", "#include ", -"#ifdef SC", + "#if defined(WIN32) || defined(WIN64)", + "#include ", + "#else", + "#include ", + "#include ", /* new 4.3.0 */ + "#endif", "#include ", /* defines off_t */ "#include ", "#include ", - #ifndef PC - "#include ", - #endif -"#endif", "#define Offsetof(X, Y) ((unsigned long)(&(((X *)0)->Y)))", "#ifndef max", "#define max(a,b) (((a)<(b)) ? (b) : (a))", "#endif", + "#ifndef PRINTF", + "int Printf(const char *fmt, ...); /* prototype only */", + "#endif", 0, }; @@ -89,13 +93,12 @@ " }", "#endif", "#endif", - "struct H_el {", " struct H_el *nxt;", "#ifdef FULLSTACK", - " unsigned tagged;", + " unsigned int tagged;", "#if defined(BITSTATE) && !defined(NOREDUCE) && !defined(SAFETY)", - " unsigned proviso;", /* uses just 1 bit 0/1 */ + " unsigned int proviso;", /* uses just 1 bit 0/1 */ "#endif", "#endif", "#if defined(CHECK) || (defined(COLLAPSE) && !defined(FULLSTACK))", @@ -108,8 +111,8 @@ " unsigned long ln;", /* length of vector */ "#endif", "#endif", - "#ifdef REACH", - " unsigned D;", + "#if !defined(SAFETY) || defined(REACH)", + " unsigned int D;", "#endif", " unsigned state;", "} **H_tab, **S_Tab;\n", @@ -233,7 +236,7 @@ "long Ccheck=0, Cholds=0;", "int a_cycles=0, upto=1, strict=0, verbose = 0, signoff = 0;", "#ifdef HAS_CODE", - "int gui = 0, coltrace = 0, readtrail = 0, whichtrail = 0, onlyproc = -1;", + "int gui = 0, coltrace = 0, readtrail = 0, whichtrail = 0, onlyproc = -1, silent = 0;", "#endif", "int state_tables=0, fairness=0, no_rck=0, Nr_Trails=0;", "char simvals[128];", @@ -283,7 +286,8 @@ "static long udmem;", #endif "#endif", - "static long A_depth = 0, depth = 0;", + "static long A_depth = 0;", + "long depth = 0;", /* not static to support -S2 option, but possible clash with embedded code */ "static uchar warned = 0, iterative = 0, like_java = 0, every_error = 0;", "static uchar noasserts = 0, noends = 0, bounded = 0;", "#if SYNC>0 && ASYNC==0", @@ -677,16 +681,16 @@ " for (i = 1; i < m; i++)", " { int nrelse;", " if (strcmp(procname[n], \":never:\") != 0)", - " for (T0 = trans[n][i]; T0; T0 = T0->nxt)", - " { if (T0->st == i", - " && strcmp(T0->tp, \"(1)\") == 0)", - " { printf(\"error: proctype '%%s' \",", - " procname[n]);", - " printf(\"line %%d, state %%d: has un\",", - " srcln[i], i);", - " printf(\"conditional self-loop\\n\");", - " pan_exit(1);", - " } }", + " { for (T0 = trans[n][i]; T0; T0 = T0->nxt)", + " { if (T0->st == i", + " && strcmp(T0->tp, \"(1)\") == 0)", + " { printf(\"error: proctype '%%s' \",", + " procname[n]);", + " printf(\"line %%d, state %%d: has un\",", + " srcln[i], i);", + " printf(\"conditional self-loop\\n\");", + " pan_exit(1);", + " } } }", " nrelse = 0;", " for (T0 = trans[n][i]; T0; T0 = T0->nxt)", " { if (strcmp(T0->tp, \"else\") == 0)", @@ -699,6 +703,17 @@ " printf(\" 'else' stmnts\\n\");", " pan_exit(1);", " } }", + " if (!state_tables && strcmp(procname[n], \":never:\") == 0)", + " { int h = 0;", + " for (i = 1; i < m; i++)", + " for (T0 = trans[n][i]; T0; T0 = T0->nxt)", + " if (T0->forw > h) h = T0->forw;", + " h++;", + " frm_st0 = (short *) emalloc(h * sizeof(short));", + " for (i = 1; i < m; i++)", + " for (T0 = trans[n][i]; T0; T0 = T0->nxt)", + " frm_st0[T0->forw] = i;", + " }", "}", "void", "imed(Trans *T, int v, int n, int j) /* set intermediate state */", --- /sys/src/cmd/spin/pangen3.c Sun Jul 22 04:48:59 2007 +++ /sys/src/cmd/spin/pangen3.c Sun Jul 22 04:48:57 2007 @@ -10,11 +10,7 @@ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif extern FILE *th; extern int claimnr, eventmapnr; @@ -62,7 +58,8 @@ static void putfnm_flush(int j) { - fprintf(th, "{ %s, %d, %d }\n", + if (lastfnm) + fprintf(th, "{ %s, %d, %d }\n", lastfnm->name, lastfrom, j); } --- /sys/src/cmd/spin/pangen3.h Sun Jul 22 04:49:13 2007 +++ /sys/src/cmd/spin/pangen3.h Sun Jul 22 04:49:11 2007 @@ -37,8 +37,8 @@ " int back; /* index return transition */", " struct Trans *nxt;", "} Trans;\n", - "#define qptr(x) (((uchar *)&now)+q_offset[x])", - "#define pptr(x) (((uchar *)&now)+proc_offset[x])", + "#define qptr(x) (((uchar *)&now)+(int)q_offset[x])", + "#define pptr(x) (((uchar *)&now)+(int)proc_offset[x])", /* "#define Pptr(x) ((proc_offset[x])?pptr(x):noptr)", */ "extern uchar *Pptr(int);", @@ -72,7 +72,7 @@ "#endif", "#else", "#ifdef BITSTATE", - "#ifdef SAFETY", + "#ifdef SAFETY && !defined(HASH64)", "#define CNTRSTACK", "#else", "#define FULLSTACK", @@ -163,13 +163,16 @@ "struct H_el *Lstate;", "#endif", "int depthfound = -1; /* loop detection */", - "int proc_offset[MAXPROC], proc_skip[MAXPROC];", - "int q_offset[MAXQ], q_skip[MAXQ];", - "#if VECTORSZ<65536", - " unsigned short vsize;", + "#if VECTORSZ>32000", + "int proc_offset[MAXPROC];", + "int q_offset[MAXQ];", "#else", - " unsigned long vsize; /* vector size in bytes */", + "short proc_offset[MAXPROC];", + "short q_offset[MAXQ];", "#endif", + "uchar proc_skip[MAXPROC];", + "uchar q_skip[MAXQ];", + "unsigned long vsize; /* vector size in bytes */", "#ifdef SVDUMP", "int vprefix=0, svfd; /* runtime option -pN */", "#endif", @@ -251,10 +254,10 @@ " else", " proc_skip[h] = 0;", "#ifndef NOCOMP", - " for (k = vsize + proc_skip[h]; k > vsize; k--)", + " for (k = vsize + (int) proc_skip[h]; k > vsize; k--)", " Mask[k-1] = 1; /* align */", "#endif", - " vsize += proc_skip[h];", + " vsize += (int) proc_skip[h];", " proc_offset[h] = vsize;", "#ifdef SVDUMP", " if (vprefix > 0)", @@ -262,7 +265,11 @@ " write(svfd, (uchar *) &dummy, sizeof(int)); /* mark */", " write(svfd, (uchar *) &h, sizeof(int));", " write(svfd, (uchar *) &n, sizeof(int));", + "#if VECTORSZ>32000", " write(svfd, (uchar *) &proc_offset[h], sizeof(int));", + "#else", + " write(svfd, (uchar *) &proc_offset[h], sizeof(short));", + "#endif", " write(svfd, (uchar *) &now, vprefix-4*sizeof(int)); /* padd */", " }", "#endif", @@ -326,10 +333,10 @@ "#ifndef BFS", " if (is_rv) k += j;", "#endif", - " for (k += q_skip[i]; k > vsize; k--)", + " for (k += (int) q_skip[i]; k > vsize; k--)", " Mask[k-1] = 1;", "#endif", - " vsize += q_skip[i];", + " vsize += (int) q_skip[i];", " q_offset[i] = vsize;", " now._nr_qs += 1;", " vsize += j;", @@ -536,7 +543,7 @@ "run(void)", "{ /* int i; */", " memset((char *)&now, 0, sizeof(State));", - " vsize = sizeof(State) - VECTORSZ;", + " vsize = (unsigned long) (sizeof(State) - VECTORSZ);", "#ifndef NOVSZ", " now._vsz = vsize;", "#endif", @@ -736,14 +743,16 @@ "char *emalloc(unsigned long);", "char *Malloc(unsigned long);", "int Boundcheck(int, int, int, int, Trans *);", - "/* int abort(void); */", "int addqueue(int, int);", "/* int atoi(char *); */", - "int close(int);", -"#ifndef SC", + "/* int abort(void); */", + "int close(int);", /* should probably remove this */ +#if 0 + "#ifndef SC", "int creat(char *, unsigned short);", "int write(int, void *, unsigned);", -"#endif", + "#endif", +#endif "int delproc(int, int);", "int endstate(void);", "int hstore(char *, int);", --- /sys/src/cmd/spin/pangen4.c Sun Jul 22 04:49:28 2007 +++ /sys/src/cmd/spin/pangen4.c Sun Jul 22 04:49:27 2007 @@ -10,11 +10,7 @@ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif extern FILE *tc, *tb; extern Queue *qtab; --- /sys/src/cmd/spin/pangen4.h Sun Jul 22 04:49:43 2007 +++ /sys/src/cmd/spin/pangen4.h Sun Jul 22 04:49:42 2007 @@ -27,7 +27,7 @@ "#define ushort unsigned short", "", "#define TWIDTH 256", - "#define HASH(y,n) (n)*(((int)y))", + "#define HASH(y,n) (n)*(((long)y))", "#define INRANGE(e,h) ((h>=e->From && h<=e->To)||(e->s==1 && e->S==h))", "", "extern char *emalloc(unsigned long); /* imported routine */", --- /sys/src/cmd/spin/pangen5.c Sun Jul 22 04:50:00 2007 +++ /sys/src/cmd/spin/pangen5.c Sun Jul 22 04:49:58 2007 @@ -10,11 +10,7 @@ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif typedef struct BuildStack { FSM_trans *t; --- /sys/src/cmd/spin/pangen6.c Sun Jul 22 04:50:36 2007 +++ /sys/src/cmd/spin/pangen6.c Sun Jul 22 04:50:34 2007 @@ -17,11 +17,7 @@ /* AST_criteria to process the slice criteria */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif extern Ordered *all_names; extern FSM_use *use_free; @@ -507,8 +503,7 @@ if (strcmp(as->name, bs->name) != 0) return 0; - if (as->type == STRUCT - && a && a->rgt && b && b->rgt) + if (as->type == STRUCT && a->rgt && b->rgt) return AST_mutual(a->rgt->lft, b->rgt->lft, 0); return 1; @@ -2195,7 +2190,7 @@ f->dom[i] = (ulong) ~0; /* all 1's */ if (a->nstates % BPW) - for (i = a->nstates % BPW; i < BPW; i++) + for (i = (a->nstates % BPW); i < (int) BPW; i++) f->dom[a->nwords-1] &= ~(1<nstates; cnt++) --- /sys/src/cmd/spin/pc_zpp.c Sun Jul 22 04:50:54 2007 +++ /sys/src/cmd/spin/pc_zpp.c Sun Jul 22 04:50:53 2007 @@ -376,9 +376,9 @@ { 6, "define", do_define, 1 }, { 4, "else", do_else, 0 }, { 5, "endif", do_endif, 0 }, - { 2, "if", do_if, 0 }, { 5, "ifdef", do_ifdef, 0 }, { 6, "ifndef", do_ifndef, 0 }, + { 2, "if", do_if, 0 }, { 7, "include", do_include, 1 }, { 8, "undefine", do_undefine, 1 }, }; @@ -390,7 +390,7 @@ for (p = q; *p; p++) if (*p != ' ' && *p != '\t') break; - for (i = 0; i < sizeof(s)/sizeof(struct Directives); i++) + for (i = 0; i < (int) (sizeof(s)/sizeof(struct Directives)); i++) if (!strncmp(s[i].directive, p, s[i].len)) { if (s[i].interp && !printing[if_depth]) --- /sys/src/cmd/spin/reprosrc.c Sun Jul 22 04:51:34 2007 +++ /sys/src/cmd/spin/reprosrc.c Sun Jul 22 04:51:33 2007 @@ -11,11 +11,7 @@ #include #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif static int indent = 1; --- /sys/src/cmd/spin/run.c Sun Jul 22 04:51:54 2007 +++ /sys/src/cmd/spin/run.c Sun Jul 22 04:51:53 2007 @@ -11,11 +11,7 @@ #include #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif extern RunList *X, *run; extern Symbol *Fname; @@ -441,9 +437,9 @@ interprint(FILE *fd, Lextok *n) { Lextok *tmp = n->lft; char c, *s = n->sym->name; - int i, j; char lbuf[16]; + int i, j; char lbuf[512]; extern char Buf[]; - char tBuf[1024]; + char tBuf[4096]; Buf[0] = '\0'; if (!no_print) @@ -494,7 +490,7 @@ } dotag(fd, Buf); } - if (strlen(Buf) > 1024) fatal("printf string too long", 0); + if (strlen(Buf) > 4096) fatal("printf string too long", 0); return 1; } --- /sys/src/cmd/spin/sched.c Sun Jul 22 04:52:17 2007 +++ /sys/src/cmd/spin/sched.c Sun Jul 22 04:52:15 2007 @@ -11,11 +11,7 @@ #include #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif extern int verbose, s_trail, analyze, no_wrapup; extern char *claimproc, *eventmap, Buf[]; @@ -182,6 +178,31 @@ } void +check_param_count(int i, Lextok *m) +{ ProcList *p; + Symbol *s = m->sym; /* proctype name */ + Lextok *f, *t; /* formal pars */ + int cnt = 0; + + for (p = rdy; p; p = p->nxt) + { if (strcmp(s->name, p->n->name) == 0) + { if (m->lft) /* actual param list */ + { lineno = m->lft->ln; + Fname = m->lft->fn; + } + for (f = p->p; f; f = f->rgt) /* one type at a time */ + for (t = f->lft; t; t = t->rgt) /* count formal params */ + { cnt++; + } + if (i != cnt) + { printf("spin: saw %d parameters, expected %d\n", i, cnt); + non_fatal("wrong number of parameters", ""); + } + break; + } } +} + +void start_claim(int n) { ProcList *p; RunList *r, *q = (RunList *) 0; @@ -291,6 +312,7 @@ silent_moves(Element *e) { Element *f; + if (e->n) switch (e->n->ntyp) { case GOTO: if (Rvous) break; @@ -310,29 +332,33 @@ return e; } -static void -pickproc(void) +static RunList * +pickproc(RunList *Y) { SeqList *z; Element *has_else; short Choices[256]; int j, k, nr_else = 0; if (nproc <= nstop+1) { X = run; - return; + return NULL; } if (!interactive || depth < jumpsteps) { /* was: j = (int) Rand()%(nproc-nstop); */ if (Priority_Sum < nproc-nstop) fatal("cannot happen - weights", (char *)0); j = (int) Rand()%Priority_Sum; + while (j - X->priority >= 0) { j -= X->priority; + Y = X; X = X->nxt; - if (!X) X = run; + if (!X) { Y = NULL; X = run; } } } else { int only_choice = -1; int no_choice = 0, proc_no_ch, proc_k; + + Tval = 0; /* new 4.2.6 */ try_again: printf("Select a statement\n"); try_more: for (X = run, k = 1; X; X = X->nxt) { if (X->pid > 255) break; @@ -444,7 +470,8 @@ goto try_again; } } MadeChoice = 0; - for (X = run; X; X = X->nxt) + Y = NULL; + for (X = run; X; Y = X, X = X->nxt) { if (!X->nxt || X->nxt->pid > 255 || j < Choices[X->nxt->pid]) @@ -453,12 +480,13 @@ break; } } } + return Y; } void sched(void) { Element *e; - RunList *Y=0; /* previous process in run queue */ + RunList *Y = NULL; /* previous process in run queue */ RunList *oX; int go, notbeyond = 0; #ifdef PC @@ -489,7 +517,7 @@ printf("warning: trace assertion not used in random simulation\n"); X = run; - pickproc(); + Y = pickproc(Y); while (X) { context = X->n; @@ -564,7 +592,7 @@ if (X->pc->n->ntyp == '@' && X->pid == (nproc-nstop-1)) - { if (X != run) + { if (X != run && Y != NULL) Y->nxt = X->nxt; else run = X->nxt; @@ -578,6 +606,8 @@ if (!interactive) Tval = 0; if (nproc == nstop) break; memset(is_blocked, 0, 256); + /* proc X is no longer in runlist */ + X = (X->nxt) ? X->nxt : run; } else { if (p_blocked(X->pid)) { if (Tval) break; @@ -588,8 +618,7 @@ dotag(stdout, "timeout\n"); X = oX; } } } } - Y = X; - pickproc(); + Y = pickproc(X); notbeyond = 0; } context = ZS; --- /sys/src/cmd/spin/spin.h Sun Jul 22 04:52:40 2007 +++ /sys/src/cmd/spin/spin.h Sun Jul 22 04:52:39 2007 @@ -15,8 +15,6 @@ #include #include #include -#ifndef PC -#endif typedef struct Lextok { unsigned short ntyp; /* node type */ @@ -53,7 +51,7 @@ 1=hide, 2=show, 4=bit-equiv, 8=byte-equiv, 16=formal par, 32=inline par, - 64=treat as if local + 64=treat as if local; 128=read at least once */ unsigned char colnr; /* for use with xspin during simulation */ int nbits; /* optional width specifier */ @@ -319,6 +317,7 @@ 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 *); --- /sys/src/cmd/spin/spin.y Sun Jul 22 04:53:04 2007 +++ /sys/src/cmd/spin/spin.y Sun Jul 22 04:53:02 2007 @@ -21,6 +21,8 @@ extern short has_sorted, has_random, has_enabled, has_pcvalue, has_np; extern short has_code, has_state, has_io; extern void count_runs(Lextok *); +extern void no_internals(Lextok *); +extern void any_runs(Lextok *); extern void validref(Lextok *, Lextok *); extern char yytext[]; @@ -375,7 +377,7 @@ stmnt : Special { $$ = $1; } | Stmnt { $$ = $1; if (inEventMap) - fatal("not an event", (char *)0); + non_fatal("not an event", (char *)0); } ; @@ -388,6 +390,7 @@ margs { Expand_Ok--; has_io++; $$ = nn($1, 's', $1, $4); $$->val=0; trackchanuse($4, ZN, 'S'); + any_runs($4); } | IF options FI { $$ = nn($1, IF, ZN, ZN); $$->sl = $2->sl; @@ -422,11 +425,13 @@ Stmnt : varref ASGN expr { $$ = nn($1, ASGN, $1, $3); trackvar($1, $3); nochan_manip($1, $3, 0); + no_internals($1); } | varref INCR { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1; $$ = nn(ZN, '+', $1, $$); $$ = nn($1, ASGN, $1, $$); trackvar($1, $1); + no_internals($1); if ($1->sym->type == CHAN) fatal("arithmetic on chan", (char *)0); } @@ -434,6 +439,7 @@ $$ = nn(ZN, '-', $1, $$); $$ = nn($1, ASGN, $1, $$); trackvar($1, $1); + no_internals($1); if ($1->sym->type == CHAN) fatal("arithmetic on chan id's", (char *)0); } @@ -466,6 +472,7 @@ $$ = nn($1, 's', $1, $4); $$->val = has_sorted = 1; trackchanuse($4, ZN, 'S'); + any_runs($4); } | full_expr { $$ = nn(ZN, 'c', $1, ZN); count_runs($$); } | ELSE { $$ = nn(ZN,ELSE,ZN,ZN); --- /sys/src/cmd/spin/spinlex.c Sun Jul 22 04:53:29 2007 +++ /sys/src/cmd/spin/spinlex.c Sun Jul 22 04:53:28 2007 @@ -11,11 +11,7 @@ #include #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif #define MAXINL 16 /* max recursion depth inline fcts */ #define MAXPAR 32 /* max params to an inline call */ @@ -542,7 +538,7 @@ cnt++; } - if (cnt == 0) fprintf(fd, "4"); /* can't happen */ + if (cnt == 0) fprintf(fd, "WS"); /* can't happen */ fprintf(fd, "];\n"); } @@ -614,7 +610,7 @@ } if (has_stack) - { fprintf(fd, "void\nc_stack(char *p_t_r)\n{\n"); + { fprintf(fd, "void\nc_stack(uchar *p_t_r)\n{\n"); fprintf(fd, "#ifdef VERBOSE\n"); fprintf(fd, " printf(\"c_stack %%u\\n\", p_t_r);\n"); fprintf(fd, "#endif\n"); @@ -632,7 +628,7 @@ fprintf(fd, "}\n\n"); } - fprintf(fd, "void\nc_update(char *p_t_r)\n{\n"); + fprintf(fd, "void\nc_update(uchar *p_t_r)\n{\n"); fprintf(fd, "#ifdef VERBOSE\n"); fprintf(fd, " printf(\"c_update %%u\\n\", p_t_r);\n"); fprintf(fd, "#endif\n"); @@ -662,7 +658,7 @@ fprintf(fd, "}\n"); if (has_stack) - { fprintf(fd, "void\nc_unstack(char *p_t_r)\n{\n"); + { fprintf(fd, "void\nc_unstack(uchar *p_t_r)\n{\n"); fprintf(fd, "#ifdef VERBOSE\n"); fprintf(fd, " printf(\"c_unstack %%u\\n\", p_t_r);\n"); fprintf(fd, "#endif\n"); @@ -677,7 +673,7 @@ fprintf(fd, "}\n"); } - fprintf(fd, "void\nc_revert(char *p_t_r)\n{\n"); + fprintf(fd, "void\nc_revert(uchar *p_t_r)\n{\n"); fprintf(fd, "#ifdef VERBOSE\n"); fprintf(fd, " printf(\"c_revert %%u\\n\", p_t_r);\n"); fprintf(fd, "#endif\n"); @@ -1358,7 +1354,29 @@ { sprintf(yytext, "'%c'", yylval->val); strcat(IArg_cont[IArgno], yytext); } else - { strcat(IArg_cont[IArgno], yytext); + { + switch (c) { + case SEP: strcpy(yytext, "::"); break; + case SEMI: strcpy(yytext, ";"); break; + case DECR: strcpy(yytext, "--"); break; + case INCR: strcpy(yytext, "++"); break; + case LSHIFT: strcpy(yytext, "<<"); break; + case RSHIFT: strcpy(yytext, ">>"); break; + case LE: strcpy(yytext, "<="); break; + case LT: strcpy(yytext, "<"); break; + case GE: strcpy(yytext, ">="); break; + case GT: strcpy(yytext, ">"); break; + case EQ: strcpy(yytext, "=="); break; + case ASGN: strcpy(yytext, "="); break; + case NE: strcpy(yytext, "!="); break; + case R_RCV: strcpy(yytext, "??"); break; + case RCV: strcpy(yytext, "?"); break; + case O_SND: strcpy(yytext, "!!"); break; + case SND: strcpy(yytext, "!"); break; + case AND: strcpy(yytext, "&&"); break; + case OR: strcpy(yytext, "||"); break; + } + strcat(IArg_cont[IArgno], yytext); } } --- /sys/src/cmd/spin/structs.c Sun Jul 22 04:53:54 2007 +++ /sys/src/cmd/spin/structs.c Sun Jul 22 04:53:53 2007 @@ -10,11 +10,7 @@ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif typedef struct UType { Symbol *nm; /* name of the type */ --- /sys/src/cmd/spin/sym.c Sun Jul 22 04:54:20 2007 +++ /sys/src/cmd/spin/sym.c Sun Jul 22 04:54:19 2007 @@ -10,11 +10,7 @@ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif extern Symbol *Fname, *owner; extern int lineno, depth, verbose, NamesNotAdded, deadvar; @@ -179,6 +175,7 @@ void setptype(Lextok *n, int t, Lextok *vis) /* predefined types */ { int oln = lineno, cnt = 1; extern int Expand_Ok; + while (n) { if (n->sym->type && !(n->sym->hidden&32)) { lineno = n->ln; Fname = n->fn; @@ -193,7 +190,7 @@ setaccess(n->sym, ZS, cnt, 'F'); } if (t == UNSIGNED) - { if (n->sym->nbits < 0) + { if (n->sym->nbits < 0 || n->sym->nbits >= 32) fatal("(%s) has invalid width-field", n->sym->name); if (n->sym->nbits == 0) { n->sym->nbits = 16; @@ -275,7 +272,7 @@ if (!context) { lineno = p->ln; Fname = p->fn; - non_fatal("non-local x[rs] assertion", (char *)0); + fatal("non-local x[rs] assertion", (char *)0); } for (m = p; m; m = m->rgt) { Lextok *Xu_new = (Lextok *) emalloc(sizeof(Lextok)); @@ -325,7 +322,7 @@ /* label the name */ if (n->lft->sym->type != MTYPE) - { n->lft->sym->hidden |= 32; + { n->lft->sym->hidden |= 128; /* is used */ n->lft->sym->type = MTYPE; n->lft->sym->ini = nn(ZN,CONST,ZN,ZN); n->lft->sym->ini->val = cnt; @@ -477,7 +474,7 @@ return; report: chname(sp); - for (i = d = 0; i < sizeof(xx)/sizeof(struct X); i++) + for (i = d = 0; i < (int) (sizeof(xx)/sizeof(struct X)); i++) { b = 0; for (a = sp->access; a; a = a->lnk) if (a->typ == xx[i].typ) b++; @@ -513,7 +510,7 @@ case SHORT: case INT: case UNSIGNED: - if ((walk->entry->hidden&32)) + if ((walk->entry->hidden&128)) /* was: 32 */ continue; if (!separate --- /sys/src/cmd/spin/tl_lex.c Sun Jul 22 04:56:13 2007 +++ /sys/src/cmd/spin/tl_lex.c Sun Jul 22 04:56:12 2007 @@ -28,7 +28,7 @@ tl_getword(int first, int (*tst)(int)) { int i=0; char c; - yytext[i++]= (char ) first; + yytext[i++] = (char ) first; while (tst(c = tl_Getchar())) yytext[i++] = c; yytext[i] = '\0'; --- /sys/src/cmd/spin/tl_main.c Sun Jul 22 04:56:44 2007 +++ /sys/src/cmd/spin/tl_main.c Sun Jul 22 04:56:44 2007 @@ -39,6 +39,23 @@ } void +tl_balanced(void) +{ int i; + int k = 0; + + for (i = 0; i < hasuform; i++) + { if (uform[i] == '(') + { k++; + } else if (uform[i] == ')') + { k--; + } } + if (k != 0) + { tl_errs++; + tl_yyerror("parentheses not balanced"); + } +} + +void put_uform(void) { fprintf(tl_out, "%s", uform); @@ -96,7 +113,11 @@ printf(" -n normalize tl formula and exit\n"); exit(1); } - tl_parse(); + tl_balanced(); + + if (tl_errs == 0) + tl_parse(); + if (tl_verbose) tl_stats(); return tl_errs; } --- /sys/src/cmd/spin/tl_parse.c Sun Jul 22 04:57:47 2007 +++ /sys/src/cmd/spin/tl_parse.c Sun Jul 22 04:57:46 2007 @@ -15,7 +15,7 @@ #include "tl.h" extern int tl_yylex(void); -extern int tl_verbose; +extern int tl_verbose, tl_errs; int tl_yychar = 0; YYSTYPE tl_yylval; @@ -390,6 +390,11 @@ { printf("formula: "); dump(n); printf("\n"); + } + if (tl_Getchar() != -1) + { tl_yyerror("syntax error"); + tl_errs++; + return; } trans(n); } --- /sys/src/cmd/spin/vars.c Sun Jul 22 04:59:28 2007 +++ /sys/src/cmd/spin/vars.c Sun Jul 22 04:59:27 2007 @@ -10,11 +10,7 @@ /* Send all bug-reports and/or questions to: bugs@spinroot.com */ #include "spin.h" -#ifdef PC -#include "y_tab.h" -#else #include "y.tab.h" -#endif extern Ordered *all_names; extern RunList *X, *LastX; @@ -278,8 +274,12 @@ void dumplocal(RunList *r) { static Lextok *dummy = ZN; - Symbol *z, *s = r->symtab; + Symbol *z, *s; int i; + + if (!r) return; + + s = r->symtab; if (!dummy) dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN); --- /sys/src/cmd/spin/version.h Sun Jul 22 05:00:03 2007 +++ /sys/src/cmd/spin/version.h Sun Jul 22 05:00:02 2007 @@ -1 +1 @@ -#define Version "Spin Version 4.2.5 -- 2 April 2005" +#define Version "Spin Version 4.3.0 -- 22 June 2007"