spin: Update to most recent version. (thanks Ori_B)

from Ori_B:

There were a small number of changes needed from the tarball
on spinroot.org:

  - The mkfile needed to be updated
  - Memory.h needed to not be included
  - It needed to invoke /bin/cpp instead of gcc -E
  - It depended on `yychar`, which our yacc doesn't
    provide.

I'm still figuring out how to use spin, but it seems to do
the right thing when testing a few of the examples:

	% cd $home/src/Spin/Examples/
	% spin -a peterson.pml
	% pcc pan.c -D_POSIX_SOURCE
	% ./6.out

	(Spin Version 6.4.7 -- 19 August 2017)
		+ Partial Order Reduction

	Full statespace search for:
		never claim         	- (none specified)
		assertion violations	+
		acceptance   cycles 	- (not selected)
		invalid end states	+

	State-vector 32 byte, depth reached 24, errors: 0
	40 states, stored
	27 states, matched
	67 transitions (= stored+matched)
		0 atomic steps
	hash conflicts:         0 (resolved)

	Stats on memory usage (in Megabytes):
	0.002	equivalent memory usage for states (stored*(State-vector + overhead))
	0.292	actual memory usage for states
	128.000	memory used for hash table (-w24)
	0.534	memory used for DFS stack (-m10000)
	128.730	total actual memory usage


	unreached in proctype user
		/tmp/Spin/Examples/peterson.pml:20, state 10, "-end-"
		(1 of 10 states)

	pan: elapsed time 1.25 seconds
	pan: rate        32 states/second

1 files changed, 118 insertions, 45 deletions

diff --git a/sys/src/cmd/spin/sym.c b/sys/src/cmd/spin/sym.c
index 0001d2f5f..6985f0a82 100644
--- a/sys/src/cmd/spin/sym.c
+++ b/sys/src/cmd/spin/sym.c
@@ -1,25 +1,27 @@
 /***** spin: sym.c *****/
 
-/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
-/* All Rights Reserved.  This software is for educational purposes only.  */
-/* No guarantee whatsoever is expressed or implied by the distribution of */
-/* this code.  Permission is given to distribute this code provided that  */
-/* this introductory message is not removed and no monies are exchanged.  */
-/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
-/*             http://spinroot.com/                                       */
-/* Send all bug-reports and/or questions to: bugs@spinroot.com            */
+/*
+ * This file is part of the public release of Spin. It is subject to the
+ * terms in the LICENSE file that is included in this source directory.
+ * Tool documentation is available at http://spinroot.com
+ */
 
 #include "spin.h"
 #include "y.tab.h"
 
 extern Symbol	*Fname, *owner;
 extern int	lineno, depth, verbose, NamesNotAdded, deadvar;
+extern int	has_hidden, m_loss, old_scope_rules;
 extern short	has_xu;
+extern char	CurScope[MAXSCOPESZ];
 
 Symbol	*context = ZS;
 Ordered	*all_names = (Ordered *)0;
 int	Nid = 0;
 
+Lextok *Mtype = (Lextok *) 0;
+Lextok *runstmnts = ZN;
+
 static Ordered	*last_name = (Ordered *)0;
 static Symbol	*symtab[Nhash+1];
 
@@ -31,12 +33,12 @@ samename(Symbol *a, Symbol *b)
 	return !strcmp(a->name, b->name);
 }
 
-int
-hash(char *s)
-{	int h=0;
+unsigned int
+hash(const char *s)
+{	unsigned int h = 0;
 
 	while (*s)
-	{	h += *s++;
+	{	h += (unsigned int) *s++;
 		h <<= 1;
 		if (h&(Nhash+1))
 			h |= 1;
@@ -44,31 +46,89 @@ hash(char *s)
 	return h&Nhash;
 }
 
+void
+disambiguate(void)
+{	Ordered *walk;
+	Symbol *sp;
+	char *n, *m;
+
+	if (old_scope_rules)
+		return;
+
+	/* prepend the scope_prefix to the names */
+
+	for (walk = all_names; walk; walk = walk->next)
+	{	sp = walk->entry;
+		if (sp->type != 0
+		&&  sp->type != LABEL
+		&&  strlen((const char *)sp->bscp) > 1)
+		{	if (sp->context)
+			{	m = (char *) emalloc(strlen((const char *)sp->bscp) + 1);
+				sprintf(m, "_%d_", sp->context->sc);
+				if (strcmp((const char *) m, (const char *) sp->bscp) == 0)
+				{	continue;
+				/* 6.2.0: only prepend scope for inner-blocks,
+				   not for top-level locals within a proctype
+				   this means that you can no longer use the same name
+				   for a global and a (top-level) local variable
+				 */
+			}	}
+
+			n = (char *) emalloc(strlen((const char *)sp->name)
+				+ strlen((const char *)sp->bscp) + 1);
+			sprintf(n, "%s%s", sp->bscp, sp->name);
+			sp->name = n;	/* discard the old memory */
+	}	}
+}
+
 Symbol *
 lookup(char *s)
 {	Symbol *sp; Ordered *no;
-	int h = hash(s);
-
-	for (sp = symtab[h]; sp; sp = sp->next)
-		if (strcmp(sp->name, s) == 0
-		&&  samename(sp->context, context)
-		&&  samename(sp->owner, owner))
-			return sp;		/* found */
-
-	if (context)				/* in proctype */
+	unsigned int h = hash(s);
+
+	if (old_scope_rules)
+	{	/* same scope - global refering to global or local to local */
+		for (sp = symtab[h]; sp; sp = sp->next)
+		{	if (strcmp(sp->name, s) == 0
+			&&  samename(sp->context, context)
+			&&  samename(sp->owner, owner))
+			{	return sp;		/* found */
+		}	}
+	} else
+	{	/* added 6.0.0: more traditional, scope rule */
+		for (sp = symtab[h]; sp; sp = sp->next)
+		{	if (strcmp(sp->name, s) == 0
+			&&  samename(sp->context, context)
+			&&  (strcmp((const char *)sp->bscp, CurScope) == 0
+			||   strncmp((const char *)sp->bscp, CurScope, strlen((const char *)sp->bscp)) == 0)
+			&&  samename(sp->owner, owner))
+			{
+				if (!samename(sp->owner, owner))
+				{	printf("spin: different container %s\n", sp->name);
+					printf("	old: %s\n", sp->owner?sp->owner->name:"--");
+					printf("	new: %s\n", owner?owner->name:"--");
+				/*	alldone(1);	*/
+				}
+				return sp;		/* found */
+	}	}	}
+
+	if (context)				/* in proctype, refers to global */
 	for (sp = symtab[h]; sp; sp = sp->next)
-		if (strcmp(sp->name, s) == 0
+	{	if (strcmp(sp->name, s) == 0
 		&& !sp->context
 		&&  samename(sp->owner, owner))
-			return sp;		/* global */
+		{	return sp;		/* global */
+	}	}
 
 	sp = (Symbol *) emalloc(sizeof(Symbol));
-	sp->name = (char *) emalloc((int) strlen(s) + 1);
+	sp->name = (char *) emalloc(strlen(s) + 1);
 	strcpy(sp->name, s);
 	sp->nel = 1;
 	sp->setat = depth;
 	sp->context = context;
 	sp->owner = owner;			/* if fld in struct */
+	sp->bscp = (unsigned char *) emalloc(strlen((const char *)CurScope)+1);
+	strcpy((char *)sp->bscp, CurScope);
 
 	if (NamesNotAdded == 0)
 	{	sp->next = symtab[h];
@@ -109,8 +169,6 @@ trackvar(Lextok *n, Lextok *m)
 	}
 }
 
-Lextok *runstmnts = ZN;
-
 void
 trackrun(Lextok *n)
 {
@@ -151,11 +209,11 @@ checkrun(Symbol *parnm, int posno)
 		strcpy(buf2, (!(res&4))?"bit":"byte");
 		sputtype(buf, parnm->type);
 		i = (int) strlen(buf);
-		while (buf[--i] == ' ') buf[i] = '\0';
-		if (strcmp(buf, buf2) == 0) return;
+		while (i > 0 && buf[--i] == ' ') buf[i] = '\0';
+		if (i == 0 || strcmp(buf, buf2) == 0) return;
 		prehint(parnm);
 		printf("proctype %s, '%s %s' could be declared",
-			parnm->context->name, buf, parnm->name);
+			parnm->context?parnm->context->name:"", buf, parnm->name);
 		printf(" '%s %s'\n", buf2, parnm->name);
 	}
 }
@@ -178,9 +236,9 @@ setptype(Lextok *n, int t, Lextok *vis)	/* predefined types */
 
 	while (n)
 	{	if (n->sym->type && !(n->sym->hidden&32))
-		{ lineno = n->ln; Fname = n->fn;
-		  non_fatal("redeclaration of '%s'", n->sym->name);
-		  lineno = oln;
+		{	lineno = n->ln; Fname = n->fn;
+			fatal("redeclaration of '%s'", n->sym->name);
+			lineno = oln;
 		}
 		n->sym->type = (short) t;
 
@@ -201,14 +259,15 @@ setptype(Lextok *n, int t, Lextok *vis)	/* predefined types */
 				n->sym->name);
 		}
 		if (vis)
-		{	if (strncmp(vis->sym->name, ":hide:", 6) == 0)
+		{	if (strncmp(vis->sym->name, ":hide:", (size_t) 6) == 0)
 			{	n->sym->hidden |= 1;
+				has_hidden++;
 				if (t == BIT)
 				fatal("bit variable (%s) cannot be hidden",
 					n->sym->name);
-			} else if (strncmp(vis->sym->name, ":show:", 6) == 0)
+			} else if (strncmp(vis->sym->name, ":show:", (size_t) 6) == 0)
 			{	n->sym->hidden |= 2;
-			} else if (strncmp(vis->sym->name, ":local:", 7) == 0)
+			} else if (strncmp(vis->sym->name, ":local:", (size_t) 7) == 0)
 			{	n->sym->hidden |= 64;
 			}
 		}
@@ -268,7 +327,13 @@ void
 setxus(Lextok *p, int t)
 {	Lextok *m, *n;
 
-	has_xu = 1; 
+	has_xu = 1;
+
+	if (m_loss && t == XS)
+	{	printf("spin: %s:%d, warning, xs tag not compatible with -m (message loss)\n",
+			(p->fn != NULL) ? p->fn->name : "stdin", p->ln);
+	}
+
 	if (!context)
 	{	lineno = p->ln;
 		Fname = p->fn;
@@ -276,6 +341,7 @@ setxus(Lextok *p, int t)
 	}
 	for (m = p; m; m = m->rgt)
 	{	Lextok *Xu_new = (Lextok *) emalloc(sizeof(Lextok));
+		Xu_new->uiid = p->uiid;
 		Xu_new->val = t;
 		Xu_new->lft = m->lft;
 		Xu_new->sym = context;
@@ -297,8 +363,6 @@ setxus(Lextok *p, int t)
 	}
 }
 
-Lextok *Mtype = (Lextok *) 0;
-
 void
 setmtype(Lextok *m)
 {	Lextok *n;
@@ -332,7 +396,7 @@ setmtype(Lextok *m)
 	}
 	lineno = oln;
 	if (cnt > 256)
-	fatal("too many mtype elements (>255)", (char *)0);
+		fatal("too many mtype elements (>255)", (char *)0);
 }
 
 int
@@ -389,11 +453,11 @@ symvar(Symbol *sp)
 	printf("\t");
 	if (sp->owner) printf("%s.", sp->owner->name);
 	printf("%s", sp->name);
-	if (sp->nel > 1) printf("[%d]", sp->nel);
+	if (sp->nel > 1 || sp->isarray == 1) printf("[%d]", sp->nel);
 
 	if (sp->type == CHAN)
 		printf("\t%d", (sp->ini)?sp->ini->val:0);
-	else if (sp->type == STRUCT) /* Frank Weil, 2.9.8 */
+	else if (sp->type == STRUCT && sp->Snm != NULL) /* Frank Weil, 2.9.8 */
 		printf("\t%s", sp->Snm->name);
 	else
 		printf("\t%d", eval(sp->ini));
@@ -408,8 +472,13 @@ symvar(Symbol *sp)
 
 	if (sp->Nid < 0)	/* formal parameter */
 		printf("\t<parameter %d>", -(sp->Nid));
+	else if (sp->type == MTYPE)
+		printf("\t<constant>");
+	else if (sp->isarray)
+		printf("\t<array>");
 	else
 		printf("\t<variable>");
+
 	if (sp->type == CHAN && sp->ini)
 	{	int i;
 		for (m = sp->ini->rgt, i = 0; m; m = m->rgt)
@@ -423,6 +492,11 @@ symvar(Symbol *sp)
 			if (m->rgt) printf("\t");
 		}
 	}
+
+	if (!old_scope_rules)
+	{	printf("\t{scope %s}", sp->bscp);
+	}
+
 	printf("\n");
 }
 
@@ -440,11 +514,10 @@ chname(Symbol *sp)
 	if (sp->context) printf("%s-", sp->context->name);
 	if (sp->owner) printf("%s.", sp->owner->name);
 	printf("%s", sp->name);
-	if (sp->nel > 1) printf("[%d]", sp->nel);
+	if (sp->nel > 1 || sp->isarray == 1) printf("[%d]", sp->nel);
 	printf("\t");
 }
 
-
 static struct X {
 	int typ; char *nm;
 } xx[] = {
@@ -521,14 +594,14 @@ chanaccess(void)
 
 			if (!(verbose&32) || has_code) continue;
 
-			printf("spin: warning, %s, ", Fname->name);
+			printf("spin: %s:0, warning, ", Fname->name);
 			sputtype(buf, walk->entry->type);
 			if (walk->entry->context)
 				printf("proctype %s",
 					walk->entry->context->name);
 			else
 				printf("global");
-			printf(", '%s%s' variable is never used\n",
+			printf(", '%s%s' variable is never used (other than in print stmnts)\n",
 				buf, walk->entry->name);
 	}	}
 }