sys/src/cmd/spin/main.c

   1 /***** spin: main.c *****/
   2
   3 /*
   4  * This file is part of the public release of Spin. It is subject to the
   5  * terms in the LICENSE file that is included in this source directory.
   6  * Tool documentation is available at http://spinroot.com
   7  */
   8
   9 #include <stdlib.h>
  10 #include <assert.h>
  11 #include "spin.h"
  12 #include "version.h"
  13 #include <sys/types.h>
  14 #include <sys/stat.h>
  15 #include <signal.h>
  16 #include <time.h>
  17 #ifdef PC
  18  #include <io.h>
  19 #else
  20  #include <unistd.h>
  21 #endif
  22 #include "y.tab.h"
  23
  24 extern int      DstepStart, lineno, tl_terse;
  25 extern FILE     *yyin, *yyout, *tl_out;
  26 extern Symbol   *context;
  27 extern char     *claimproc;
  28 extern void     repro_src(void);
  29 extern void     qhide(int);
  30 extern char     CurScope[MAXSCOPESZ];
  31 extern short    has_provided, has_code, has_ltl, has_accept;
  32 extern int      realread, buzzed;
  33
  34 static void     add_comptime(char *);
  35 static void     add_runtime(char *);
  36
  37 Symbol  *Fname, *oFname;
  38
  39 int     Etimeouts;      /* nr timeouts in program */
  40 int     Ntimeouts;      /* nr timeouts in never claim */
  41 int     analyze, columns, dumptab, has_remote, has_remvar;
  42 int     interactive, jumpsteps, m_loss, nr_errs, cutoff;
  43 int     s_trail, ntrail, verbose, xspin, notabs, rvopt;
  44 int     no_print, no_wrapup, Caccess, limited_vis, like_java;
  45 int     separate;       /* separate compilation */
  46 int     export_ast;     /* pangen5.c */
  47 int     norecompile;    /* main.c */
  48 int     old_scope_rules;        /* use pre 5.3.0 rules */
  49 int     old_priority_rules;     /* use pre 6.2.0 rules */
  50 int     product, Strict;
  51 short   replay;
  52
  53 int     merger = 1, deadvar = 1, implied_semis = 1;
  54 int     ccache = 0; /* oyvind teig: 5.2.0 case caching off by default */
  55
  56 static int preprocessonly, SeedUsed, itsr, itsr_n;
  57 static int seedy;       /* be verbose about chosen seed */
  58 static int inlineonly;  /* show inlined code */
  59 static int dataflow = 1;
  60
  61 #if 0
  62 meaning of flags on verbose:
  63         1       -g global variable values
  64         2       -l local variable values
  65         4       -p all process actions
  66         8       -r receives
  67         16      -s sends
  68         32      -v verbose
  69         64      -w very verbose
  70 #endif
  71
  72 static char     Operator[] = "operator: ";
  73 static char     Keyword[]  = "keyword: ";
  74 static char     Function[] = "function-name: ";
  75 static char     **add_ltl  = (char **) 0;
  76 static char     **ltl_file = (char **) 0;
  77 static char     **nvr_file = (char **) 0;
  78 static char     *ltl_claims = (char *) 0;
  79 static char     *pan_runtime = "";
  80 static char     *pan_comptime = "";
  81 static char     formula[4096];
  82 static FILE     *fd_ltl = (FILE *) 0;
  83 static char     *PreArg[64];
  84 static int      PreCnt = 0;
  85 static char     out1[64];
  86
  87 char    **trailfilename;        /* new option 'k' */
  88
  89 void    explain(int);
  90
  91 #define CPP     "/bin/cpp"      /* sometimes: "/lib/cpp" */
  92
  93 static char     PreProc[512];
  94 extern int      depth; /* at least some steps were made */
  95
  96 int
  97 WhatSeed(void)
  98 {
  99         return SeedUsed;
 100 }
 101
 102 void
 103 final_fiddle(void)
 104 {       char *has_a, *has_l, *has_f;
 105
 106         /* no -a or -l but has_accept: add -a */
 107         /* no -a or -l in pan_runtime: add -DSAFETY to pan_comptime */
 108         /* -a or -l but no -f then add -DNOFAIR */
 109
 110         has_a = strstr(pan_runtime, "-a");
 111         has_l = strstr(pan_runtime, "-l");
 112         has_f = strstr(pan_runtime, "-f");
 113
 114         if (!has_l && !has_a && strstr(pan_comptime, "-DNP"))
 115         {       add_runtime("-l");
 116                 has_l = strstr(pan_runtime, "-l");
 117         }
 118
 119         if (!has_a && !has_l
 120         &&  !strstr(pan_comptime, "-DSAFETY"))
 121         {       if (has_accept
 122                 && !strstr(pan_comptime, "-DBFS")
 123                 && !strstr(pan_comptime, "-DNOCLAIM"))
 124                 {       add_runtime("-a");
 125                         has_a = pan_runtime;
 126                 } else
 127                 {       add_comptime("-DSAFETY");
 128         }       }
 129
 130         if ((has_a || has_l) && !has_f
 131         &&  !strstr(pan_comptime, "-DNOFAIR"))
 132         {       add_comptime("-DNOFAIR");
 133         }
 134 }
 135
 136 static int
 137 change_param(char *t, char *what, int range, int bottom)
 138 {       char *ptr;
 139         int v;
 140
 141         assert(range < 1000 && range > 0);
 142         if ((ptr = strstr(t, what)) != NULL)
 143         {       ptr += strlen(what);
 144                 if (!isdigit((int) *ptr))
 145                 {       return 0;
 146                 }
 147                 v = atoi(ptr) + 1;      /* was: v = (atoi(ptr)+1)%range */
 148                 if (v >= range)
 149                 {       v = bottom;
 150                 }
 151                 if (v >= 100)
 152                 {       *ptr++ = '0' + (v/100); v %= 100;
 153                         *ptr++ = '0' + (v/10);
 154                         *ptr   = '0' + (v%10);
 155                 } else if (v >= 10)
 156                 {       *ptr++ = '0' + (v/10);
 157                         *ptr++ = '0' + (v%10);
 158                         *ptr   = ' ';
 159                 } else
 160                 {       *ptr++ = '0' + v;
 161                         *ptr++ = ' ';
 162                         *ptr   = ' ';
 163         }       }
 164         return 1;
 165 }
 166
 167 static void
 168 change_rs(char *t)
 169 {       char *ptr;
 170         int cnt = 0;
 171         long v;
 172
 173         if ((ptr = strstr(t, "-RS")) != NULL)
 174         {       ptr += 3;
 175                 /* room for at least 10 digits */
 176                 v = Rand()%1000000000L;
 177                 while (v/10 > 0)
 178                 {       *ptr++ = '0' + v%10;
 179                         v /= 10;
 180                         cnt++;
 181                 }
 182                 *ptr++ = '0' + v;
 183                 cnt++;
 184                 while (cnt++ < 10)
 185                 {       *ptr++ = ' ';
 186         }       }
 187 }
 188
 189 int
 190 omit_str(char *in, char *s)
 191 {       char *ptr = strstr(in, s);
 192         int i, nr = -1;
 193
 194         if (ptr)
 195         {       for (i = 0; i < (int) strlen(s); i++)
 196                 {       *ptr++ = ' ';
 197                 }
 198                 if (isdigit((int) *ptr))
 199                 {       nr = atoi(ptr);
 200                         while (isdigit((int) *ptr))
 201                         {       *ptr++ = ' ';
 202         }       }       }
 203         return nr;
 204 }
 205
 206 void
 207 string_trim(char *t)
 208 {       int n = strlen(t) - 1;
 209
 210         while (n > 0 && t[n] == ' ')
 211         {       t[n--] = '\0';
 212         }
 213 }
 214
 215 int
 216 e_system(int v, const char *s)
 217 {       static int count = 1;
 218         /* v == 0 : checks to find non-linked version of gcc */
 219         /* v == 1 : all other commands */
 220         /* v == 2 : preprocessing the promela input */
 221
 222         if (v == 1)
 223         {       if (verbose&(32|64))    /* -v or -w */
 224                 {       printf("cmd%02d: %s\n", count++, s);
 225                         fflush(stdout);
 226                 }
 227                 if (verbose&64)         /* only -w */
 228                 {       return 0;       /* suppress the call to system(s) */
 229         }       }
 230         return system(s);
 231 }
 232
 233 void
 234 alldone(int estatus)
 235 {       char *ptr;
 236 #if defined(WIN32) || defined(WIN64)
 237         struct _stat x;
 238 #else
 239         struct stat x;
 240 #endif
 241         if (preprocessonly == 0 &&  strlen(out1) > 0)
 242         {       (void) unlink((const char *) out1);
 243         }
 244
 245         (void) unlink(TMP_FILE1);
 246         (void) unlink(TMP_FILE2);
 247
 248         if (!buzzed && seedy && !analyze && !export_ast
 249         && !s_trail && !preprocessonly && depth > 0)
 250         {       printf("seed used: %d\n", SeedUsed);
 251         }
 252
 253         if (!buzzed && xspin && (analyze || s_trail))
 254         {       if (estatus)
 255                 {       printf("spin: %d error(s) - aborting\n",
 256                                 estatus);
 257                 } else
 258                 {       printf("Exit-Status 0\n");
 259         }       }
 260
 261         if (buzzed && replay && !has_code && !estatus)
 262         {       extern QH *qh;
 263                 QH *j;
 264                 int i;
 265                 char *tmp = (char *) emalloc(strlen("spin -t") +
 266                                 strlen(pan_runtime) + strlen(Fname->name) + 8);
 267                 pan_runtime = (char *) emalloc(2048);   /* more than enough */
 268                 sprintf(pan_runtime, "-n%d ", SeedUsed);
 269                 if (jumpsteps)
 270                 {       sprintf(&pan_runtime[strlen(pan_runtime)], "-j%d ", jumpsteps);
 271                 }
 272                 if (trailfilename)
 273                 {       sprintf(&pan_runtime[strlen(pan_runtime)], "-k%s ", *trailfilename);
 274                 }
 275                 if (cutoff)
 276                 {       sprintf(&pan_runtime[strlen(pan_runtime)], "-u%d ", cutoff);
 277                 }
 278                 for (i = 1; i <= PreCnt; i++)
 279                 {       strcat(pan_runtime, PreArg[i]);
 280                         strcat(pan_runtime, " ");
 281                 }
 282                 for (j = qh; j; j = j->nxt)
 283                 {       sprintf(&pan_runtime[strlen(pan_runtime)], "-q%d ", j->n);
 284                 }
 285                 if (strcmp(PreProc, CPP) != 0)
 286                 {       sprintf(&pan_runtime[strlen(pan_runtime)], "\"-P%s\" ", PreProc);
 287                 }
 288                 /* -oN options 1..5 are ignored in simulations */
 289                 if (old_priority_rules) strcat(pan_runtime, "-o6 ");
 290                 if (!implied_semis)  strcat(pan_runtime, "-o7 ");
 291                 if (no_print)        strcat(pan_runtime, "-b ");
 292                 if (no_wrapup)       strcat(pan_runtime, "-B ");
 293                 if (columns == 1)    strcat(pan_runtime, "-c ");
 294                 if (columns == 2)    strcat(pan_runtime, "-M ");
 295                 if (seedy == 1)      strcat(pan_runtime, "-h ");
 296                 if (like_java == 1)  strcat(pan_runtime, "-J ");
 297                 if (old_scope_rules) strcat(pan_runtime, "-O ");
 298                 if (notabs)          strcat(pan_runtime, "-T ");
 299                 if (verbose&1)       strcat(pan_runtime, "-g ");
 300                 if (verbose&2)       strcat(pan_runtime, "-l ");
 301                 if (verbose&4)       strcat(pan_runtime, "-p ");
 302                 if (verbose&8)       strcat(pan_runtime, "-r ");
 303                 if (verbose&16)      strcat(pan_runtime, "-s ");
 304                 if (verbose&32)      strcat(pan_runtime, "-v ");
 305                 if (verbose&64)      strcat(pan_runtime, "-w ");
 306                 if (m_loss)          strcat(pan_runtime, "-m ");
 307                 sprintf(tmp, "spin -t %s %s", pan_runtime, Fname->name);
 308                 estatus = e_system(1, tmp);     /* replay */
 309                 exit(estatus);  /* replay without c_code */
 310         }
 311
 312         if (buzzed && (!replay || has_code) && !estatus)
 313         {       char *tmp, *tmp2 = NULL, *P_X;
 314                 char *C_X = (buzzed == 2) ? "-O" : "";
 315
 316                 if (replay && strlen(pan_comptime) == 0)
 317                 {
 318 #if defined(WIN32) || defined(WIN64)
 319                         P_X = "pan";
 320 #else
 321                         P_X = "./pan";
 322 #endif
 323                         if (stat(P_X, (struct stat *)&x) < 0)
 324                         {       goto recompile; /* no executable pan for replay */
 325                         }
 326                         tmp = (char *) emalloc(8 + strlen(P_X) + strlen(pan_runtime) +4);
 327                         /* the final +4 is too allow adding " &" in some cases */
 328                         sprintf(tmp, "%s %s", P_X, pan_runtime);
 329                         goto runit;
 330                 }
 331 #if defined(WIN32) || defined(WIN64)
 332                 P_X = "-o pan pan.c && pan";
 333 #else
 334                 P_X = "-o pan pan.c && ./pan";
 335 #endif
 336                 /* swarm and biterate randomization additions */
 337                 if (!replay && itsr)    /* iterative search refinement */
 338                 {       if (!strstr(pan_comptime, "-DBITSTATE"))
 339                         {       add_comptime("-DBITSTATE");
 340                         }
 341                         if (!strstr(pan_comptime, "-DPUTPID"))
 342                         {       add_comptime("-DPUTPID");
 343                         }
 344                         if (!strstr(pan_comptime, "-DT_RAND")
 345                         &&  !strstr(pan_comptime, "-DT_REVERSE"))
 346                         {       add_runtime("-T0  ");   /* controls t_reverse */
 347                         }
 348                         if (!strstr(pan_runtime, "-P")  /* runtime flag */
 349                         ||   pan_runtime[2] < '0'
 350                         ||   pan_runtime[2] > '1') /* no -P0 or -P1 */
 351                         {       add_runtime("-P0  ");   /* controls p_reverse */
 352                         }
 353                         if (!strstr(pan_runtime, "-w"))
 354                         {       add_runtime("-w18 ");   /* -w18 = 256K */
 355                         } else
 356                         {       char nv[32];
 357                                 int x;
 358                                 x = omit_str(pan_runtime, "-w");
 359                                 if (x >= 0)
 360                                 {       sprintf(nv, "-w%d  ", x);
 361                                         add_runtime(nv); /* added spaces */
 362                         }       }
 363                         if (!strstr(pan_runtime, "-h"))
 364                         {       add_runtime("-h0  ");   /* 0..499 */
 365                                 /* leave 2 spaces for increments up to -h499 */
 366                         } else if (!strstr(pan_runtime, "-hash"))
 367                         {       char nv[32];
 368                                 int x;
 369                                 x = omit_str(pan_runtime, "-h");
 370                                 if (x >= 0)
 371                                 {       sprintf(nv, "-h%d  ", x%500);
 372                                         add_runtime(nv); /* added spaces */
 373                         }       }
 374                         if (!strstr(pan_runtime, "-k"))
 375                         {       add_runtime("-k1  ");   /* 1..3 */
 376                         } else
 377                         {       char nv[32];
 378                                 int x;
 379                                 x = omit_str(pan_runtime, "-k");
 380                                 if (x >= 0)
 381                                 {       sprintf(nv, "-k%d  ", x%4);
 382                                         add_runtime(nv); /* added spaces */
 383                         }       }
 384                         if (strstr(pan_runtime, "-p_rotate"))
 385                         {       char nv[32];
 386                                 int x;
 387                                 x = omit_str(pan_runtime, "-p_rotate");
 388                                 if (x < 0)
 389                                 {       x = 0;
 390                                 }
 391                                 sprintf(nv, "-p_rotate%d  ", x%256);
 392                                 add_runtime(nv); /* added spaces */
 393                         } else if (strstr(pan_runtime, "-p_permute") == 0)
 394                         {       add_runtime("-p_rotate0  ");
 395                         }
 396                         if (strstr(pan_runtime, "-RS"))
 397                         {       (void) omit_str(pan_runtime, "-RS");
 398                         }
 399                         /* need room for at least 10 digits */
 400                         add_runtime("-RS1234567890 ");
 401                         change_rs(pan_runtime);
 402                 }
 403 recompile:
 404                 if (strstr(PreProc, "cpp"))     /* unix/linux */
 405                 {       strcpy(PreProc, "gcc"); /* need compiler */
 406                 } else if ((tmp = strstr(PreProc, "-E")) != NULL)
 407                 {       *tmp = '\0'; /* strip preprocessing flags */
 408                 }
 409
 410                 final_fiddle();
 411                 tmp = (char *) emalloc(8 +      /* account for alignment */
 412                                 strlen(PreProc) +
 413                                 strlen(C_X) +
 414                                 strlen(pan_comptime) +
 415                                 strlen(P_X) +
 416                                 strlen(pan_runtime) +
 417                                 strlen(" -p_reverse & "));
 418                 tmp2 = tmp;
 419
 420                 /* P_X ends with " && ./pan " */
 421                 sprintf(tmp, "%s %s %s %s %s",
 422                         PreProc, C_X, pan_comptime, P_X, pan_runtime);
 423
 424                 if (!replay)
 425                 {       if (itsr < 0)           /* swarm only */
 426                         {       strcat(tmp, " &"); /* after ./pan */
 427                                 itsr = -itsr;   /* now same as biterate */
 428                         }
 429                         /* do compilation first
 430                          * split cc command from run command
 431                          * leave cc in tmp, and set tmp2 to run
 432                          */
 433                         if ((ptr = strstr(tmp, " && ")) != NULL)
 434                         {       tmp2 = ptr + 4; /* first run */
 435                                 *ptr = '\0';
 436                 }       }
 437
 438                 if (has_ltl)
 439                 {       (void) unlink("_spin_nvr.tmp");
 440                 }
 441                 if (!norecompile)
 442                 {
 443 #ifdef PC
 444                 /* make sure that if compilation fails we do not continue */
 445                 (void) unlink("./pan.exe");
 446 #else
 447                 (void) unlink("./pan");
 448 #endif
 449                 }
 450 runit:
 451                 if (norecompile && tmp != tmp2)
 452                 {       estatus = 0;
 453                 } else
 454                 {       if (itsr > 0)   /* else it happens below */
 455                         {       estatus = e_system(1, tmp);     /* compile or run */
 456                 }       }
 457                 if (replay || estatus < 0)
 458                 {       goto skipahead;
 459                 }
 460                 /* !replay */
 461                 if (itsr == 0)                  /* single run */
 462                 {       estatus = e_system(1, tmp2);
 463                 } else if (itsr > 0)    /* iterative search refinement */
 464                 {       int is_swarm = 0;
 465                         if (tmp2 != tmp)        /* swarm: did only compilation so far */
 466                         {       tmp = tmp2;     /* now we point to the run command */
 467                                 estatus = e_system(1, tmp);     /* first run */
 468                         }
 469                         itsr--;                 /* count down */
 470
 471                         /* the following are added back randomly later */
 472                         (void) omit_str(tmp, "-p_reverse");     /* replaced by spaces */
 473                         (void) omit_str(tmp, "-p_normal");
 474
 475                         if (strstr(tmp, " &") != NULL)
 476                         {       (void) omit_str(tmp, " &");
 477                                 is_swarm = 1;
 478                         }
 479
 480                         /* increase -w every itsr_n-th run */
 481                         if ((itsr_n > 0 && (itsr == 0 || (itsr%itsr_n) != 0))
 482                         ||  (change_param(tmp, "-w", 36, 18) >= 0))     /* max 4G bit statespace */
 483                         {       (void) change_param(tmp, "-h", 500, 0); /* hash function 0.499 */
 484                                 (void) change_param(tmp, "-p_rotate", 256, 0); /* if defined */
 485                                 (void) change_param(tmp, "-k", 4, 1);   /* nr bits per state 0->1,2,3 */
 486                                 (void) change_param(tmp, "-T", 2, 0);   /* with or without t_reverse*/
 487                                 (void) change_param(tmp, "-P", 2, 0);   /* -P 0..1 != p_reverse */
 488                                 change_rs(tmp);                 /* change random seed */
 489                                 string_trim(tmp);
 490                                 if (rand()%5 == 0)              /* 20% of all runs */
 491                                 {       strcat(tmp, " -p_reverse ");
 492                                         /* at end, so this overrides -p_rotateN, if there */
 493                                         /* but -P0..1 disable this in 50% of the cases */
 494                                         /* so its really activated in 10% of all runs */
 495                                 } else if (rand()%6 == 0) /* override p_rotate and p_reverse */
 496                                 {       strcat(tmp, " -p_normal ");
 497                                 }
 498                                 if (is_swarm)
 499                                 {       strcat(tmp, " &");
 500                                 }
 501                                 goto runit;
 502                 }       }
 503 skipahead:
 504                 (void) unlink("pan.b");
 505                 (void) unlink("pan.c");
 506                 (void) unlink("pan.h");
 507                 (void) unlink("pan.m");
 508                 (void) unlink("pan.p");
 509                 (void) unlink("pan.t");
 510         }
 511         exit(estatus);
 512 }
 513 #if 0
 514         -P0     normal active process creation
 515         -P1     reversed order for *active* process creation != p_reverse
 516
 517         -T0     normal transition exploration
 518         -T1     reversed order of transition exploration
 519
 520         -DP_RAND        (random starting point +- -DP_REVERSE)
 521         -DPERMUTED      (also enables -p_rotateN and -p_reverse)
 522         -DP_REVERSE     (same as -DPERMUTED with -p_reverse, but 7% faster)
 523
 524         -DT_RAND        (random starting point -- optionally with -T0..1)
 525         -DT_REVERSE     (superseded by -T0..1 options)
 526
 527          -hash generates new hash polynomial for -h0
 528
 529         permutation modes:
 530          -permuted (adds -DPERMUTED) -- this is also the default with -swarm
 531          -t_reverse (same as -T1)
 532          -p_reverse (similar to -P1)
 533          -p_rotateN
 534          -p_normal
 535
 536         less useful would be (since there is less non-determinism in transitions):
 537                 -t_rotateN -- a controlled version of -DT_RAND
 538
 539         compiling with -DPERMUTED enables a number of new runtime options,
 540         that -swarmN,M will also exploit:
 541                 -p_permute (default)
 542                 -p_rotateN
 543                 -p_reverse
 544 #endif
 545
 546 void
 547 preprocess(char *a, char *b, int a_tmp)
 548 {       char precmd[1024], cmd[2048];
 549         int i;
 550 #ifdef PC
 551         /* gcc is sometimes a symbolic link to gcc-4
 552            that does not work well in cygwin, so we try
 553            to use the actual executable that is used.
 554            the code below assumes we are on a cygwin-like system
 555          */
 556         if (strncmp(PreProc, "gcc ", strlen("gcc ")) == 0)
 557         {       if (e_system(0, "gcc-4 --version > pan.pre") == 0)
 558                 {       strcpy(PreProc, "gcc-4 -std=gnu99 -E -x c");
 559                 } else if (e_system(0, "gcc-3 --version > pan.pre") == 0)
 560                 {       strcpy(PreProc, "gcc-3 -std=gnu99 -E -x c");
 561         }       }
 562 #endif
 563
 564         assert(strlen(PreProc) < sizeof(precmd));
 565         strcpy(precmd, PreProc);
 566         for (i = 1; i <= PreCnt; i++)
 567         {       strcat(precmd, " ");
 568                 strcat(precmd, PreArg[i]);
 569         }
 570         if (strlen(precmd) > sizeof(precmd))
 571         {       fprintf(stdout, "spin: too many -D args, aborting\n");
 572                 alldone(1);
 573         }
 574         sprintf(cmd, "%s %s > %s", precmd, a, b);
 575         if (e_system(2, (const char *)cmd))             /* preprocessing */
 576         {       (void) unlink((const char *) b);
 577                 if (a_tmp) (void) unlink((const char *) a);
 578                 fprintf(stdout, "spin: preprocessing failed\n");        /* 4.1.2 was stderr */
 579                 alldone(1); /* no return, error exit */
 580         }
 581         if (a_tmp) (void) unlink((const char *) a);
 582 }
 583
 584 void
 585 usage(void)
 586 {
 587         printf("use: spin [-option] ... [-option] file\n");
 588         printf("\tNote: file must always be the last argument\n");
 589         printf("\t-A apply slicing algorithm\n");
 590         printf("\t-a generate a verifier in pan.c\n");
 591         printf("\t-B no final state details in simulations\n");
 592         printf("\t-b don't execute printfs in simulation\n");
 593         printf("\t-C print channel access info (combine with -g etc.)\n");
 594         printf("\t-c columnated -s -r simulation output\n");
 595         printf("\t-d produce symbol-table information\n");
 596         printf("\t-Dyyy pass -Dyyy to the preprocessor\n");
 597         printf("\t-Eyyy pass yyy to the preprocessor\n");
 598         printf("\t-e compute synchronous product of multiple never claims (modified by -L)\n");
 599         printf("\t-f \"..formula..\"  translate LTL ");
 600         printf("into never claim\n");
 601         printf("\t-F file  like -f, but with the LTL formula stored in a 1-line file\n");
 602         printf("\t-g print all global variables\n");
 603         printf("\t-h at end of run, print value of seed for random nr generator used\n");
 604         printf("\t-i interactive (random simulation)\n");
 605         printf("\t-I show result of inlining and preprocessing\n");
 606         printf("\t-J reverse eval order of nested unlesses\n");
 607         printf("\t-jN skip the first N steps ");
 608         printf("in simulation trail\n");
 609         printf("\t-k fname use the trailfile stored in file fname, see also -t\n");
 610         printf("\t-L when using -e, use strict language intersection\n");
 611         printf("\t-l print all local variables\n");
 612         printf("\t-M generate msc-flow in tcl/tk format\n");
 613         printf("\t-m lose msgs sent to full queues\n");
 614         printf("\t-N fname use never claim stored in file fname\n");
 615         printf("\t-nN seed for random nr generator\n");
 616         printf("\t-O use old scope rules (pre 5.3.0)\n");
 617         printf("\t-o1 turn off dataflow-optimizations in verifier\n");
 618         printf("\t-o2 don't hide write-only variables in verifier\n");
 619         printf("\t-o3 turn off statement merging in verifier\n");
 620         printf("\t-o4 turn on rendezvous optiomizations in verifier\n");
 621         printf("\t-o5 turn on case caching (reduces size of pan.m, but affects reachability reports)\n");
 622         printf("\t-o6 revert to the old rules for interpreting priority tags (pre version 6.2)\n");
 623         printf("\t-o7 revert to the old rules for semi-colon usage (pre version 6.3)\n");
 624         printf("\t-Pxxx use xxx for preprocessing\n");
 625         printf("\t-p print all statements\n");
 626         printf("\t-pp pretty-print (reformat) stdin, write stdout\n");
 627         printf("\t-qN suppress io for queue N in printouts\n");
 628         printf("\t-r print receive events\n");
 629         printf("\t-replay  replay an error trail-file found earlier\n");
 630         printf("\t      if the model contains embedded c-code, the ./pan executable is used\n");
 631         printf("\t      otherwise spin itself is used to replay the trailfile\n");
 632         printf("\t      note that pan recognizes different runtime options than spin itself\n");
 633         printf("\t-search  (or -run) generate a verifier, and compile and run it\n");
 634         printf("\t      options before -search are interpreted by spin to parse the input\n");
 635         printf("\t      options following a -search are used to compile and run the verifier pan\n");
 636         printf("\t          valid options that can follow a -search argument include:\n");
 637         printf("\t          -bfs        perform a breadth-first search\n");
 638         printf("\t          -bfspar     perform a parallel breadth-first search\n");
 639         printf("\t          -bcs        use the bounded-context-switching algorithm\n");
 640         printf("\t          -bitstate   or -bit, use bitstate storage\n");
 641         printf("\t          -biterate   use bitstate with iterative search refinement (-w18..-w35)\n");
 642         printf("\t          -swarmN,M like -biterate, but running all iterations in parallel\n");
 643         printf("\t                      perform N parallel runs and increment -w every M runs\n");
 644         printf("\t                      default value for N is 10, default for M is 1\n");
 645         printf("\t                      (add -w to see which commands will be executed)\n");
 646         printf("\t                      (add -W if ./pan exists and need not be recompiled)\n");
 647         printf("\t          -link file.c  link executable pan to file.c\n");
 648         printf("\t          -collapse   use collapse state compression\n");
 649         printf("\t          -hc         use hash-compact storage\n");
 650         printf("\t          -noclaim    ignore all ltl and never claims\n");
 651         printf("\t          -p_permute  use process scheduling order random permutation\n");
 652         printf("\t          -p_rotateN  use process scheduling order rotation by N\n");
 653         printf("\t          -p_reverse  use process scheduling order reversal\n");
 654         printf("\t          -ltl p      verify the ltl property named p\n");
 655         printf("\t          -safety     compile for safety properties only\n");
 656         printf("\t          -i          use the dfs iterative shortening algorithm\n");
 657         printf("\t          -a          search for acceptance cycles\n");
 658         printf("\t          -l          search for non-progress cycles\n");
 659         printf("\t      similarly, a -D... parameter can be specified to modify the compilation\n");
 660         printf("\t      and any valid runtime pan argument can be specified for the verification\n");
 661         printf("\t-S1 and -S2 separate pan source for claim and model\n");
 662         printf("\t-s print send events\n");
 663         printf("\t-T do not indent printf output\n");
 664         printf("\t-t[N] follow [Nth] simulation trail, see also -k\n");
 665         printf("\t-Uyyy pass -Uyyy to the preprocessor\n");
 666         printf("\t-uN stop a simulation run after N steps\n");
 667         printf("\t-v verbose, more warnings\n");
 668         printf("\t-w very verbose (when combined with -l or -g)\n");
 669         printf("\t-[XYZ] reserved for use by xspin interface\n");
 670         printf("\t-V print version number and exit\n");
 671         alldone(1);
 672 }
 673
 674 int
 675 optimizations(int nr)
 676 {
 677         switch (nr) {
 678         case '1':
 679                 dataflow = 1 - dataflow; /* dataflow */
 680                 if (verbose&32)
 681                 printf("spin: dataflow optimizations turned %s\n",
 682                         dataflow?"on":"off");
 683                 break;
 684         case '2':
 685                 /* dead variable elimination */
 686                 deadvar = 1 - deadvar;
 687                 if (verbose&32)
 688                 printf("spin: dead variable elimination turned %s\n",
 689                         deadvar?"on":"off");
 690                 break;
 691         case '3':
 692                 /* statement merging */
 693                 merger = 1 - merger;
 694                 if (verbose&32)
 695                 printf("spin: statement merging turned %s\n",
 696                         merger?"on":"off");
 697                 break;
 698
 699         case '4':
 700                 /* rv optimization */
 701                 rvopt = 1 - rvopt;
 702                 if (verbose&32)
 703                 printf("spin: rendezvous optimization turned %s\n",
 704                         rvopt?"on":"off");
 705                 break;
 706         case '5':
 707                 /* case caching */
 708                 ccache = 1 - ccache;
 709                 if (verbose&32)
 710                 printf("spin: case caching turned %s\n",
 711                         ccache?"on":"off");
 712                 break;
 713         case '6':
 714                 old_priority_rules = 1;
 715                 if (verbose&32)
 716                 printf("spin: using old priority rules (pre version 6.2)\n");
 717                 return 0; /* no break */
 718         case '7':
 719                 implied_semis = 0;
 720                 if (verbose&32)
 721                 printf("spin: no implied semi-colons (pre version 6.3)\n");
 722                 return 0; /* no break */
 723         default:
 724                 printf("spin: bad or missing parameter on -o\n");
 725                 usage();
 726                 break;
 727         }
 728         return 1;
 729 }
 730
 731 static void
 732 add_comptime(char *s)
 733 {       char *tmp;
 734
 735         if (!s || strstr(pan_comptime, s))
 736         {       return;
 737         }
 738
 739         tmp = (char *) emalloc(strlen(pan_comptime)+strlen(s)+2);
 740         sprintf(tmp, "%s %s", pan_comptime, s);
 741         pan_comptime = tmp;
 742 }
 743
 744 static struct {
 745         char *ifsee, *thendo;
 746         int keeparg;
 747 } pats[] = {
 748         { "-bfspar",    "-DBFS_PAR",    0 },
 749         { "-bfs",       "-DBFS",        0 },
 750         { "-bcs",       "-DBCS",        0 },
 751         { "-bitstate",  "-DBITSTATE",   0 },
 752         { "-bit",       "-DBITSTATE",   0 },
 753         { "-hc",        "-DHC4",        0 },
 754         { "-collapse",  "-DCOLLAPSE",   0 },
 755         { "-noclaim",   "-DNOCLAIM",    0 },
 756         { "-permuted",  "-DPERMUTED",   0 },
 757         { "-p_permute", "-DPERMUTED",   1 },
 758         { "-p_rotate",  "-DPERMUTED",   1 },
 759         { "-p_reverse", "-DPERMUTED",   1 },
 760         { "-safety",    "-DSAFETY",     0 },
 761         { "-i",         "-DREACH",      1 },
 762         { "-l",         "-DNP",         1 },
 763         { 0, 0 }
 764 };
 765
 766 static void
 767 set_itsr_n(char *s)     /* e.g., -swarm12,3 */
 768 {       char *tmp;
 769
 770         if ((tmp = strchr(s, ',')) != NULL)
 771         {       tmp++;
 772                 if (*tmp != '\0' && isdigit((int) *tmp))
 773                 {       itsr_n = atoi(tmp);
 774                         if (itsr_n < 2)
 775                         {       itsr_n = 0;
 776         }       }       }
 777 }
 778
 779 static void
 780 add_runtime(char *s)
 781 {       char *tmp;
 782         int i;
 783
 784         if (strncmp(s, "-biterate", strlen("-biterate")) == 0)
 785         {       itsr = 10;      /* default nr of sequential iterations */
 786                 if (isdigit((int) s[9]))
 787                 {       itsr = atoi(&s[9]);
 788                         if (itsr < 1)
 789                         {       itsr = 1;
 790                         }
 791                         set_itsr_n(s);
 792                 }
 793                 return;
 794         }
 795         if (strncmp(s, "-swarm", strlen("-swarm")) == 0)
 796         {       itsr = -10;     /* parallel iterations */
 797                 if (isdigit((int) s[6]))
 798                 {       itsr = atoi(&s[6]);
 799                         if (itsr < 1)
 800                         {       itsr = 1;
 801                         }
 802                         itsr = -itsr;
 803                         set_itsr_n(s);
 804                 }
 805                 return;
 806         }
 807
 808         for (i = 0; pats[i].ifsee; i++)
 809         {       if (strncmp(s, pats[i].ifsee, strlen(pats[i].ifsee)) == 0)
 810                 {       add_comptime(pats[i].thendo);
 811                         if (pats[i].keeparg)
 812                         {       break;
 813                         }
 814                         return;
 815         }       }
 816
 817         tmp = (char *) emalloc(strlen(pan_runtime)+strlen(s)+2);
 818         sprintf(tmp, "%s %s", pan_runtime, s);
 819         pan_runtime = tmp;
 820 }
 821
 822 int
 823 main(int argc, char *argv[])
 824 {       Symbol *s;
 825         int T = (int) time((time_t *)0);
 826         int usedopts = 0;
 827         extern void ana_src(int, int);
 828
 829         yyin  = stdin;
 830         yyout = stdout;
 831         tl_out = stdout;
 832         strcpy(CurScope, "_");
 833
 834         assert(strlen(CPP) < sizeof(PreProc));
 835         strcpy(PreProc, CPP);
 836
 837         /* unused flags: y, z, G, L, Q, R, W */
 838         while (argc > 1 && argv[1][0] == '-')
 839         {       switch (argv[1][1]) {
 840                 case 'A': export_ast = 1; break;
 841                 case 'a': analyze = 1; break;
 842                 case 'B': no_wrapup = 1; break;
 843                 case 'b': no_print = 1; break;
 844                 case 'C': Caccess = 1; break;
 845                 case 'c': columns = 1; break;
 846                 case 'D': PreArg[++PreCnt] = (char *) &argv[1][0];
 847                           break;        /* define */
 848                 case 'd': dumptab =  1; break;
 849                 case 'E': PreArg[++PreCnt] = (char *) &argv[1][2];
 850                           break;
 851                 case 'e': product++; break; /* see also 'L' */
 852                 case 'F': ltl_file = (char **) (argv+2);
 853                           argc--; argv++; break;
 854                 case 'f': add_ltl = (char **) argv;
 855                           argc--; argv++; break;
 856                 case 'g': verbose +=  1; break;
 857                 case 'h': seedy = 1; break;
 858                 case 'i': interactive = 1; break;
 859                 case 'I': inlineonly = 1; break;
 860                 case 'J': like_java = 1; break;
 861                 case 'j': jumpsteps = atoi(&argv[1][2]); break;
 862                 case 'k': s_trail = 1;
 863                           trailfilename = (char **) (argv+2);
 864                           argc--; argv++; break;
 865                 case 'L': Strict++; break; /* modified -e */
 866                 case 'l': verbose +=  2; break;
 867                 case 'M': columns = 2; break;
 868                 case 'm': m_loss   =  1; break;
 869                 case 'N': nvr_file = (char **) (argv+2);
 870                           argc--; argv++; break;
 871                 case 'n': T = atoi(&argv[1][2]); tl_terse = 1; break;
 872                 case 'O': old_scope_rules = 1; break;
 873                 case 'o': usedopts += optimizations(argv[1][2]); break;
 874                 case 'P': assert(strlen((const char *) &argv[1][2]) < sizeof(PreProc));
 875                           strcpy(PreProc, (const char *) &argv[1][2]);
 876                           break;
 877                 case 'p': if (argv[1][2] == 'p')
 878                           {     pretty_print();
 879                                 alldone(0);
 880                           }
 881                           verbose +=  4; break;
 882                 case 'q': if (isdigit((int) argv[1][2]))
 883                                 qhide(atoi(&argv[1][2]));
 884                           break;
 885                 case 'r':
 886                           if (strcmp(&argv[1][1], "run") == 0)
 887                           {     Srand((unsigned int) T);
 888 samecase:                       if (buzzed != 0)
 889                                 { fatal("cannot combine -x with -run -replay or -search", (char *)0);
 890                                 }
 891                                 buzzed  = 2;
 892                                 analyze = 1;
 893                                 argc--; argv++;
 894                                 /* process all remaining arguments as relating to pan: */
 895                                 while (argc > 1 && argv[1][0] == '-')
 896                                 { switch (argv[1][1]) {
 897                                   case 'D': /* eg -DNP */
 898                         /*        case 'E': conflicts with runtime arg */
 899                                   case 'O': /* eg -O2 */
 900                                   case 'U': /* to undefine a macro */
 901                                         add_comptime(argv[1]);
 902                                         break;
 903                                   case 'l':
 904                                         if (strcmp(&argv[1][1], "ltl") == 0)
 905                                         {       add_runtime("-N");
 906                                                 argc--; argv++;
 907                                                 add_runtime(argv[1]); /* prop name */
 908                                                 break;
 909                                         }
 910                                         if (strcmp(&argv[1][1], "link") == 0)
 911                                         {       argc--; argv++;
 912                                                 add_comptime(argv[1]);
 913                                                 break;
 914                                         }
 915                                         /* else fall through */
 916                                   default:
 917                                         add_runtime(argv[1]); /* -bfs etc. */
 918                                         break;
 919                                   }
 920                                   argc--; argv++;
 921                                 }
 922                                 argc++; argv--;
 923                           } else if (strcmp(&argv[1][1], "replay") == 0)
 924                           {     replay = 1;
 925                                 add_runtime("-r");
 926                                 goto samecase;
 927                           } else
 928                           {     verbose +=  8;
 929                           }
 930                           break;
 931                 case 'S': separate = atoi(&argv[1][2]); /* S1 or S2 */
 932                           /* generate code for separate compilation */
 933                           analyze = 1; break;
 934                 case 's':
 935                           if (strcmp(&argv[1][1], "simulate") == 0)
 936                           {     break; /* ignore */
 937                           }
 938                           if (strcmp(&argv[1][1], "search") == 0)
 939                           {     goto samecase;
 940                           }
 941                           verbose += 16; break;
 942                 case 'T': notabs = 1; break;
 943                 case 't': s_trail  =  1;
 944                           if (isdigit((int)argv[1][2]))
 945                           {     ntrail = atoi(&argv[1][2]);
 946                           }
 947                           break;
 948                 case 'U': PreArg[++PreCnt] = (char *) &argv[1][0];
 949                           break;        /* undefine */
 950                 case 'u': cutoff = atoi(&argv[1][2]); break;
 951                 case 'v': verbose += 32; break;
 952                 case 'V': printf("%s\n", SpinVersion);
 953                           alldone(0);
 954                           break;
 955                 case 'w': verbose += 64; break;
 956                 case 'W': norecompile = 1; break;       /* 6.4.7: for swarm/biterate */
 957                 case 'x': /* internal - reserved use */
 958                           if (buzzed != 0)
 959                           {     fatal("cannot combine -x with -run -search or -replay", (char *)0);
 960                           }
 961                           buzzed = 1;   /* implies also -a -o3 */
 962                           pan_runtime = "-d";
 963                           analyze = 1;
 964                           usedopts += optimizations('3');
 965                           break;
 966                 case 'X': xspin = notabs = 1;
 967 #ifndef PC
 968                           signal(SIGPIPE, alldone); /* not posix... */
 969 #endif
 970                           break;
 971                 case 'Y': limited_vis = 1; break;       /* used by xspin */
 972                 case 'Z': preprocessonly = 1; break;    /* used by xspin */
 973
 974                 default : usage(); break;
 975                 }
 976                 argc--; argv++;
 977         }
 978
 979         if (columns == 2 && !cutoff)
 980         {       cutoff = 1024;
 981         }
 982
 983         if (usedopts && !analyze)
 984                 printf("spin: warning -o[1..5] option ignored in simulations\n");
 985
 986         if (ltl_file)
 987         {       add_ltl = ltl_file-2; add_ltl[1][1] = 'f';
 988                 if (!(tl_out = fopen(*ltl_file, "r")))
 989                 {       printf("spin: cannot open %s\n", *ltl_file);
 990                         alldone(1);
 991                 }
 992                 if (!fgets(formula, 4096, tl_out))
 993                 {       printf("spin: cannot read %s\n", *ltl_file);
 994                 }
 995                 fclose(tl_out);
 996                 tl_out = stdout;
 997                 *ltl_file = (char *) formula;
 998         }
 999         if (argc > 1)
1000         {       FILE *fd = stdout;
1001                 char cmd[512], out2[512];
1002
1003                 /* must remain in current dir */
1004                 strcpy(out1, "pan.pre");
1005
1006                 if (add_ltl || nvr_file)
1007                 {       assert(strlen(argv[1]) < sizeof(out2));
1008                         sprintf(out2, "%s.nvr", argv[1]);
1009                         if ((fd = fopen(out2, MFLAGS)) == NULL)
1010                         {       printf("spin: cannot create tmp file %s\n",
1011                                         out2);
1012                                 alldone(1);
1013                         }
1014                         fprintf(fd, "#include \"%s\"\n", argv[1]);
1015                 }
1016
1017                 if (add_ltl)
1018                 {       tl_out = fd;
1019                         nr_errs = tl_main(2, add_ltl);
1020                         fclose(fd);
1021                         preprocess(out2, out1, 1);
1022                 } else if (nvr_file)
1023                 {       fprintf(fd, "#include \"%s\"\n", *nvr_file);
1024                         fclose(fd);
1025                         preprocess(out2, out1, 1);
1026                 } else
1027                 {       preprocess(argv[1], out1, 0);
1028                 }
1029
1030                 if (preprocessonly)
1031                 {       alldone(0);
1032                 }
1033
1034                 if (!(yyin = fopen(out1, "r")))
1035                 {       printf("spin: cannot open %s\n", out1);
1036                         alldone(1);
1037                 }
1038
1039                 assert(strlen(argv[1])+1 < sizeof(cmd));
1040
1041                 if (strncmp(argv[1], "progress", (size_t) 8) == 0
1042                 ||  strncmp(argv[1], "accept", (size_t) 6) == 0)
1043                 {       sprintf(cmd, "_%s", argv[1]);
1044                 } else
1045                 {       strcpy(cmd, argv[1]);
1046                 }
1047                 oFname = Fname = lookup(cmd);
1048                 if (oFname->name[0] == '\"')
1049                 {       int i = (int) strlen(oFname->name);
1050                         oFname->name[i-1] = '\0';
1051                         oFname = lookup(&oFname->name[1]);
1052                 }
1053         } else
1054         {       oFname = Fname = lookup("<stdin>");
1055                 if (add_ltl)
1056                 {       if (argc > 0)
1057                                 exit(tl_main(2, add_ltl));
1058                         printf("spin: missing argument to -f\n");
1059                         alldone(1);
1060                 }
1061                 printf("%s\n", SpinVersion);
1062                 fprintf(stderr, "spin: error, no filename specified\n");
1063                 fflush(stdout);
1064                 alldone(1);
1065         }
1066         if (columns == 2)
1067         {       extern void putprelude(void);
1068                 if (xspin || (verbose & (1|4|8|16|32)))
1069                 {       printf("spin: -c precludes all flags except -t\n");
1070                         alldone(1);
1071                 }
1072                 putprelude();
1073         }
1074         if (columns && !(verbose&8) && !(verbose&16))
1075         {       verbose += (8+16);
1076         }
1077         if (columns == 2 && limited_vis)
1078         {       verbose += (1+4);
1079         }
1080
1081         Srand((unsigned int) T);        /* defined in run.c */
1082         SeedUsed = T;
1083         s = lookup("_");        s->type = PREDEF; /* write-only global var */
1084         s = lookup("_p");       s->type = PREDEF;
1085         s = lookup("_pid");     s->type = PREDEF;
1086         s = lookup("_last");    s->type = PREDEF;
1087         s = lookup("_nr_pr");   s->type = PREDEF; /* new 3.3.10 */
1088         s = lookup("_priority"); s->type = PREDEF; /* new 6.2.0 */
1089
1090         yyparse();
1091         fclose(yyin);
1092
1093         if (ltl_claims)
1094         {       Symbol *r;
1095                 fclose(fd_ltl);
1096                 if (!(yyin = fopen(ltl_claims, "r")))
1097                 {       fatal("cannot open %s", ltl_claims);
1098                 }
1099                 r = oFname;
1100                 oFname = Fname = lookup(ltl_claims);
1101                 lineno = 0;
1102                 yyparse();
1103                 fclose(yyin);
1104                 oFname = Fname = r;
1105                 if (0)
1106                 {       (void) unlink(ltl_claims);
1107         }       }
1108
1109         loose_ends();
1110
1111         if (inlineonly)
1112         {       repro_src();
1113                 return 0;
1114         }
1115
1116         chanaccess();
1117         if (!Caccess)
1118         {       if (has_provided && merger)
1119                 {       merger = 0;     /* cannot use statement merging in this case */
1120                 }
1121                 if (!s_trail && (dataflow || merger) && (!replay || has_code))
1122                 {       ana_src(dataflow, merger);
1123                 }
1124                 sched();
1125                 alldone(nr_errs);
1126         }
1127
1128         return 0;
1129 }
1130
1131 void
1132 ltl_list(char *nm, char *fm)
1133 {
1134         if (s_trail
1135         ||  analyze
1136         ||  dumptab)    /* when generating pan.c or replaying a trace */
1137         {       if (!ltl_claims)
1138                 {       ltl_claims = "_spin_nvr.tmp";
1139                         if ((fd_ltl = fopen(ltl_claims, MFLAGS)) == NULL)
1140                         {       fatal("cannot open tmp file %s", ltl_claims);
1141                         }
1142                         tl_out = fd_ltl;
1143                 }
1144
1145                 add_ltl = (char **) emalloc(5 * sizeof(char *));
1146                 add_ltl[1] = "-c";
1147                 add_ltl[2] = nm;
1148                 add_ltl[3] = "-f";
1149                 add_ltl[4] = (char *) emalloc(strlen(fm)+4);
1150                 strcpy(add_ltl[4], "!(");
1151                 strcat(add_ltl[4], fm);
1152                 strcat(add_ltl[4], ")");
1153                 /* add_ltl[4] = fm; */
1154                 nr_errs += tl_main(4, add_ltl);
1155
1156                 fflush(tl_out);
1157                 /* should read this file after the main file is read */
1158         }
1159 }
1160
1161 void
1162 non_fatal(char *s1, char *s2)
1163 {       extern int yychar; extern char yytext[];
1164
1165         printf("spin: %s:%d, Error: ",
1166                 Fname?Fname->name:(oFname?oFname->name:"nofilename"), lineno);
1167 #if 1
1168         printf(s1, s2); /* avoids a gcc warning */
1169 #else
1170         if (s2)
1171                 printf(s1, s2);
1172         else
1173                 printf(s1);
1174         if (yychar > 0)
1175         {       if (yychar == SEMI)
1176                 {       printf(" statement separator");
1177                 } else
1178                 {       printf("        saw '");
1179                         explain(yychar);
1180                         printf("'");
1181         }       }
1182 #endif
1183
1184         if (strlen(yytext)>1)
1185                 printf(" near '%s'", yytext);
1186         printf("\n");
1187         nr_errs++;
1188 }
1189
1190 void
1191 fatal(char *s1, char *s2)
1192 {
1193         non_fatal(s1, s2);
1194         (void) unlink("pan.b");
1195         (void) unlink("pan.c");
1196         (void) unlink("pan.h");
1197         (void) unlink("pan.m");
1198         (void) unlink("pan.t");
1199         (void) unlink("pan.p");
1200         (void) unlink("pan.pre");
1201         if (!(verbose&32))
1202         {       (void) unlink("_spin_nvr.tmp");
1203         }
1204         alldone(1);
1205 }
1206
1207 char *
1208 emalloc(size_t n)
1209 {       char *tmp;
1210         static unsigned long cnt = 0;
1211
1212         if (n == 0)
1213                 return NULL;    /* robert shelton 10/20/06 */
1214
1215         if (!(tmp = (char *) malloc(n)))
1216         {       printf("spin: allocated %ld Gb, wanted %d bytes more\n",
1217                         cnt/(1024*1024*1024), (int) n);
1218                 fatal("not enough memory", (char *)0);
1219         }
1220         cnt += (unsigned long) n;
1221         memset(tmp, 0, n);
1222         return tmp;
1223 }
1224
1225 void
1226 trapwonly(Lextok *n /* , char *unused */)
1227 {       short i = (n->sym)?n->sym->type:0;
1228
1229         /* printf("%s   realread %d type %d\n", n->sym?n->sym->name:"--", realread, i); */
1230
1231         if (realread
1232         && (i == MTYPE
1233         ||  i == BIT
1234         ||  i == BYTE
1235         ||  i == SHORT
1236         ||  i == INT
1237         ||  i == UNSIGNED))
1238         {       n->sym->hidden |= 128;  /* var is read at least once */
1239         }
1240 }
1241
1242 void
1243 setaccess(Symbol *sp, Symbol *what, int cnt, int t)
1244 {       Access *a;
1245
1246         for (a = sp->access; a; a = a->lnk)
1247                 if (a->who == context
1248                 &&  a->what == what
1249                 &&  a->cnt == cnt
1250                 &&  a->typ == t)
1251                         return;
1252
1253         a = (Access *) emalloc(sizeof(Access));
1254         a->who = context;
1255         a->what = what;
1256         a->cnt = cnt;
1257         a->typ = t;
1258         a->lnk = sp->access;
1259         sp->access = a;
1260 }
1261
1262 Lextok *
1263 nn(Lextok *s, int t, Lextok *ll, Lextok *rl)
1264 {       Lextok *n = (Lextok *) emalloc(sizeof(Lextok));
1265         static int warn_nn = 0;
1266
1267         n->uiid = is_inline();  /* record origin of the statement */
1268         n->ntyp = (unsigned short) t;
1269         if (s && s->fn)
1270         {       n->ln = s->ln;
1271                 n->fn = s->fn;
1272         } else if (rl && rl->fn)
1273         {       n->ln = rl->ln;
1274                 n->fn = rl->fn;
1275         } else if (ll && ll->fn)
1276         {       n->ln = ll->ln;
1277                 n->fn = ll->fn;
1278         } else
1279         {       n->ln = lineno;
1280                 n->fn = Fname;
1281         }
1282         if (s) n->sym  = s->sym;
1283         n->lft  = ll;
1284         n->rgt  = rl;
1285         n->indstep = DstepStart;
1286
1287         if (t == TIMEOUT) Etimeouts++;
1288
1289         if (!context) return n;
1290
1291         if (t == 'r' || t == 's')
1292                 setaccess(n->sym, ZS, 0, t);
1293         if (t == 'R')
1294                 setaccess(n->sym, ZS, 0, 'P');
1295
1296         if (context->name == claimproc)
1297         {       int forbidden = separate;
1298                 switch (t) {
1299                 case ASGN:
1300                         printf("spin: Warning, never claim has side-effect\n");
1301                         break;
1302                 case 'r': case 's':
1303                         non_fatal("never claim contains i/o stmnts",(char *)0);
1304                         break;
1305                 case TIMEOUT:
1306                         /* never claim polls timeout */
1307                         if (Ntimeouts && Etimeouts)
1308                                 forbidden = 0;
1309                         Ntimeouts++; Etimeouts--;
1310                         break;
1311                 case LEN: case EMPTY: case FULL:
1312                 case 'R': case NFULL: case NEMPTY:
1313                         /* status becomes non-exclusive */
1314                         if (n->sym && !(n->sym->xu&XX))
1315                         {       n->sym->xu |= XX;
1316                                 if (separate == 2) {
1317                                 printf("spin: warning, make sure that the S1 model\n");
1318                                 printf("      also polls channel '%s' in its claim\n",
1319                                 n->sym->name);
1320                         }       }
1321                         forbidden = 0;
1322                         break;
1323                 case 'c':
1324                         AST_track(n, 0);        /* register as a slice criterion */
1325                         /* fall thru */
1326                 default:
1327                         forbidden = 0;
1328                         break;
1329                 }
1330                 if (forbidden)
1331                 {       printf("spin: never, saw "); explain(t); printf("\n");
1332                         fatal("incompatible with separate compilation",(char *)0);
1333                 }
1334         } else if ((t == ENABLED || t == PC_VAL) && !(warn_nn&t))
1335         {       printf("spin: Warning, using %s outside never claim\n",
1336                         (t == ENABLED)?"enabled()":"pc_value()");
1337                 warn_nn |= t;
1338         } else if (t == NONPROGRESS)
1339         {       fatal("spin: Error, using np_ outside never claim\n", (char *)0);
1340         }
1341         return n;
1342 }
1343
1344 Lextok *
1345 rem_lab(Symbol *a, Lextok *b, Symbol *c)        /* proctype name, pid, label name */
1346 {       Lextok *tmp1, *tmp2, *tmp3;
1347
1348         has_remote++;
1349         c->type = LABEL;        /* refered to in global context here */
1350         fix_dest(c, a);         /* in case target of rem_lab is jump */
1351         tmp1 = nn(ZN, '?',   b, ZN); tmp1->sym = a;
1352         tmp1 = nn(ZN, 'p', tmp1, ZN);
1353         tmp1->sym = lookup("_p");
1354         tmp2 = nn(ZN, NAME,  ZN, ZN); tmp2->sym = a;
1355         tmp3 = nn(ZN, 'q', tmp2, ZN); tmp3->sym = c;
1356         return nn(ZN, EQ, tmp1, tmp3);
1357 #if 0
1358               .---------------EQ-------.
1359              /                          \
1360            'p' -sym-> _p               'q' -sym-> c (label name)
1361            /                           /
1362          '?' -sym-> a (proctype)     NAME -sym-> a (proctype name)
1363          /
1364         b (pid expr)
1365 #endif
1366 }
1367
1368 Lextok *
1369 rem_var(Symbol *a, Lextok *b, Symbol *c, Lextok *ndx)
1370 {       Lextok *tmp1;
1371
1372         has_remote++;
1373         has_remvar++;
1374         dataflow = 0;   /* turn off dead variable resets 4.2.5 */
1375         tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a;
1376         tmp1 = nn(ZN, 'p', tmp1, ndx);
1377         tmp1->sym = c;
1378         return tmp1;
1379 #if 0
1380         cannot refer to struct elements
1381         only to scalars and arrays
1382
1383             'p' -sym-> c (variable name)
1384             / \______  possible arrayindex on c
1385            /
1386          '?' -sym-> a (proctype)
1387          /
1388         b (pid expr)
1389 #endif
1390 }
1391
1392 void
1393 explain(int n)
1394 {       FILE *fd = stdout;
1395         switch (n) {
1396         default:        if (n > 0 && n < 256)
1397                                 fprintf(fd, "'%c' = ", n);
1398                         fprintf(fd, "%d", n);
1399                         break;
1400         case '\b':      fprintf(fd, "\\b"); break;
1401         case '\t':      fprintf(fd, "\\t"); break;
1402         case '\f':      fprintf(fd, "\\f"); break;
1403         case '\n':      fprintf(fd, "\\n"); break;
1404         case '\r':      fprintf(fd, "\\r"); break;
1405         case 'c':       fprintf(fd, "condition"); break;
1406         case 's':       fprintf(fd, "send"); break;
1407         case 'r':       fprintf(fd, "recv"); break;
1408         case 'R':       fprintf(fd, "recv poll %s", Operator); break;
1409         case '@':       fprintf(fd, "@"); break;
1410         case '?':       fprintf(fd, "(x->y:z)"); break;
1411 #if 1
1412         case NEXT:      fprintf(fd, "X"); break;
1413         case ALWAYS:    fprintf(fd, "[]"); break;
1414         case EVENTUALLY: fprintf(fd, "<>"); break;
1415         case IMPLIES:   fprintf(fd, "->"); break;
1416         case EQUIV:     fprintf(fd, "<->"); break;
1417         case UNTIL:     fprintf(fd, "U"); break;
1418         case WEAK_UNTIL: fprintf(fd, "W"); break;
1419         case IN: fprintf(fd, "%sin", Keyword); break;
1420 #endif
1421         case ACTIVE:    fprintf(fd, "%sactive", Keyword); break;
1422         case AND:       fprintf(fd, "%s&&",     Operator); break;
1423         case ASGN:      fprintf(fd, "%s=",      Operator); break;
1424         case ASSERT:    fprintf(fd, "%sassert", Function); break;
1425         case ATOMIC:    fprintf(fd, "%satomic", Keyword); break;
1426         case BREAK:     fprintf(fd, "%sbreak",  Keyword); break;
1427         case C_CODE:    fprintf(fd, "%sc_code", Keyword); break;
1428         case C_DECL:    fprintf(fd, "%sc_decl", Keyword); break;
1429         case C_EXPR:    fprintf(fd, "%sc_expr", Keyword); break;
1430         case C_STATE:   fprintf(fd, "%sc_state",Keyword); break;
1431         case C_TRACK:   fprintf(fd, "%sc_track",Keyword); break;
1432         case CLAIM:     fprintf(fd, "%snever",  Keyword); break;
1433         case CONST:     fprintf(fd, "a constant"); break;
1434         case DECR:      fprintf(fd, "%s--",     Operator); break;
1435         case D_STEP:    fprintf(fd, "%sd_step", Keyword); break;
1436         case D_PROCTYPE: fprintf(fd, "%sd_proctype", Keyword); break;
1437         case DO:        fprintf(fd, "%sdo",     Keyword); break;
1438         case DOT:       fprintf(fd, "."); break;
1439         case ELSE:      fprintf(fd, "%selse",   Keyword); break;
1440         case EMPTY:     fprintf(fd, "%sempty",  Function); break;
1441         case ENABLED:   fprintf(fd, "%senabled",Function); break;
1442         case EQ:        fprintf(fd, "%s==",     Operator); break;
1443         case EVAL:      fprintf(fd, "%seval",   Function); break;
1444         case FI:        fprintf(fd, "%sfi",     Keyword); break;
1445         case FULL:      fprintf(fd, "%sfull",   Function); break;
1446         case GE:        fprintf(fd, "%s>=",     Operator); break;
1447         case GET_P:     fprintf(fd, "%sget_priority",Function); break;
1448         case GOTO:      fprintf(fd, "%sgoto",   Keyword); break;
1449         case GT:        fprintf(fd, "%s>",      Operator); break;
1450         case HIDDEN:    fprintf(fd, "%shidden", Keyword); break;
1451         case IF:        fprintf(fd, "%sif",     Keyword); break;
1452         case INCR:      fprintf(fd, "%s++",     Operator); break;
1453         case INAME:     fprintf(fd, "inline name"); break;
1454         case INLINE:    fprintf(fd, "%sinline", Keyword); break;
1455         case INIT:      fprintf(fd, "%sinit",   Keyword); break;
1456         case ISLOCAL:   fprintf(fd, "%slocal",  Keyword); break;
1457         case LABEL:     fprintf(fd, "a label-name"); break;
1458         case LE:        fprintf(fd, "%s<=",     Operator); break;
1459         case LEN:       fprintf(fd, "%slen",    Function); break;
1460         case LSHIFT:    fprintf(fd, "%s<<",     Operator); break;
1461         case LT:        fprintf(fd, "%s<",      Operator); break;
1462         case MTYPE:     fprintf(fd, "%smtype",  Keyword); break;
1463         case NAME:      fprintf(fd, "an identifier"); break;
1464         case NE:        fprintf(fd, "%s!=",     Operator); break;
1465         case NEG:       fprintf(fd, "%s! (not)",Operator); break;
1466         case NEMPTY:    fprintf(fd, "%snempty", Function); break;
1467         case NFULL:     fprintf(fd, "%snfull",  Function); break;
1468         case NON_ATOMIC: fprintf(fd, "sub-sequence"); break;
1469         case NONPROGRESS: fprintf(fd, "%snp_",  Function); break;
1470         case OD:        fprintf(fd, "%sod",     Keyword); break;
1471         case OF:        fprintf(fd, "%sof",     Keyword); break;
1472         case OR:        fprintf(fd, "%s||",     Operator); break;
1473         case O_SND:     fprintf(fd, "%s!!",     Operator); break;
1474         case PC_VAL:    fprintf(fd, "%spc_value",Function); break;
1475         case PNAME:     fprintf(fd, "process name"); break;
1476         case PRINT:     fprintf(fd, "%sprintf", Function); break;
1477         case PRINTM:    fprintf(fd, "%sprintm", Function); break;
1478         case PRIORITY:  fprintf(fd, "%spriority", Keyword); break;
1479         case PROCTYPE:  fprintf(fd, "%sproctype",Keyword); break;
1480         case PROVIDED:  fprintf(fd, "%sprovided",Keyword); break;
1481         case RCV:       fprintf(fd, "%s?",      Operator); break;
1482         case R_RCV:     fprintf(fd, "%s??",     Operator); break;
1483         case RSHIFT:    fprintf(fd, "%s>>",     Operator); break;
1484         case RUN:       fprintf(fd, "%srun",    Operator); break;
1485         case SEP:       fprintf(fd, "token: ::"); break;
1486         case SEMI:      fprintf(fd, ";"); break;
1487         case ARROW:     fprintf(fd, "->"); break;
1488         case SET_P:     fprintf(fd, "%sset_priority",Function); break;
1489         case SHOW:      fprintf(fd, "%sshow", Keyword); break;
1490         case SND:       fprintf(fd, "%s!",      Operator); break;
1491         case STRING:    fprintf(fd, "a string"); break;
1492         case TRACE:     fprintf(fd, "%strace", Keyword); break;
1493         case TIMEOUT:   fprintf(fd, "%stimeout",Keyword); break;
1494         case TYPE:      fprintf(fd, "data typename"); break;
1495         case TYPEDEF:   fprintf(fd, "%stypedef",Keyword); break;
1496         case XU:        fprintf(fd, "%sx[rs]",  Keyword); break;
1497         case UMIN:      fprintf(fd, "%s- (unary minus)", Operator); break;
1498         case UNAME:     fprintf(fd, "a typename"); break;
1499         case UNLESS:    fprintf(fd, "%sunless", Keyword); break;
1500         }
1501 }
1502
1503