sys/src/cmd/spin/guided.c

   1 /***** spin: guided.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 "spin.h"
  10 #include <sys/types.h>
  11 #include <sys/stat.h>
  12 #include <limits.h>
  13 #include "y.tab.h"
  14
  15 extern RunList  *run, *X;
  16 extern Element  *Al_El;
  17 extern Symbol   *Fname, *oFname;
  18 extern int      verbose, lineno, xspin, jumpsteps, depth, merger, cutoff;
  19 extern int      nproc, nstop, Tval, ntrail, columns;
  20 extern short    Have_claim, Skip_claim, has_code;
  21 extern void ana_src(int, int);
  22 extern char     **trailfilename;
  23
  24 int     TstOnly = 0, pno;
  25
  26 static int      lastclaim = -1;
  27 static FILE     *fd;
  28 static void     lost_trail(void);
  29
  30 static void
  31 whichproc(int p)
  32 {       RunList *oX;
  33
  34         for (oX = run; oX; oX = oX->nxt)
  35                 if (oX->pid == p)
  36                 {       printf("(%s) ", oX->n->name);
  37                         break;
  38                 }
  39 }
  40
  41 static int
  42 newer(char *f1, char *f2)
  43 {
  44 #if defined(WIN32) || defined(WIN64)
  45         struct _stat x, y;
  46 #else
  47         struct stat x, y;
  48 #endif
  49
  50         if (stat(f1, (struct stat *)&x) < 0) return 0;
  51         if (stat(f2, (struct stat *)&y) < 0) return 1;
  52         if (x.st_mtime < y.st_mtime) return 0;
  53
  54         return 1;
  55 }
  56
  57 void
  58 hookup(void)
  59 {       Element *e;
  60
  61         for (e = Al_El; e; e = e->Nxt)
  62                 if (e->n
  63                 && (e->n->ntyp == ATOMIC
  64                 ||  e->n->ntyp == NON_ATOMIC
  65                 ||  e->n->ntyp == D_STEP))
  66                         (void) huntstart(e);
  67 }
  68
  69 int
  70 not_claim(void)
  71 {
  72         return (!Have_claim || !X || X->pid != 0);
  73 }
  74
  75 int globmin = INT_MAX;
  76 int globmax = 0;
  77
  78 int
  79 find_min(Sequence *s)
  80 {       SeqList *l;
  81         Element *e;
  82
  83         if (s->minel < 0)
  84         {       s->minel = INT_MAX;
  85                 for (e = s->frst; e; e = e->nxt)
  86                 {       if (e->status & 512)
  87                         {       continue;
  88                         }
  89                         e->status |= 512;
  90
  91                         if (e->n->ntyp == ATOMIC
  92                         ||  e->n->ntyp == NON_ATOMIC
  93                         ||  e->n->ntyp == D_STEP)
  94                         {       int n = find_min(e->n->sl->this);
  95                                 if (n < s->minel)
  96                                 {       s->minel = n;
  97                                 }
  98                         } else if (e->Seqno < s->minel)
  99                         {       s->minel = e->Seqno;
 100                         }
 101                         for (l = e->sub; l; l = l->nxt)
 102                         {       int n = find_min(l->this);
 103                                 if (n < s->minel)
 104                                 {       s->minel = n;
 105                 }       }       }
 106         }
 107         if (s->minel < globmin)
 108         {       globmin = s->minel;
 109         }
 110         return s->minel;
 111 }
 112
 113 int
 114 find_max(Sequence *s)
 115 {
 116         if (s->last->Seqno > globmax)
 117         {       globmax = s->last->Seqno;
 118         }
 119         return s->last->Seqno;
 120 }
 121
 122 void
 123 match_trail(void)
 124 {       int i, a, nst;
 125         Element *dothis;
 126         char snap[512], *q;
 127
 128         if (has_code)
 129         {       printf("spin: important:\n");
 130                 printf("  =======================================warning====\n");
 131                 printf("  this model contains embedded c code statements\n");
 132                 printf("  these statements will not be executed when the trail\n");
 133                 printf("  is replayed in this way -- they are just printed,\n");
 134                 printf("  which will likely lead to inaccurate variable values.\n");
 135                 printf("  for an accurate replay use: ./pan -r\n");
 136                 printf("  =======================================warning====\n\n");
 137         }
 138
 139         /*
 140          * if source model name is leader.pml
 141          * look for the trail file under these names:
 142          *      leader.pml.trail
 143          *      leader.pml.tra
 144          *      leader.trail
 145          *      leader.tra
 146          */
 147
 148         if (trailfilename)
 149         {       if (strlen(*trailfilename) < sizeof(snap))
 150                 {       strcpy(snap, (const char *) *trailfilename);
 151                 } else
 152                 {       fatal("filename %s too long", *trailfilename);
 153                 }
 154         } else
 155         {       if (ntrail)
 156                         sprintf(snap, "%s%d.trail", oFname->name, ntrail);
 157                 else
 158                         sprintf(snap, "%s.trail", oFname->name);
 159         }
 160
 161         if ((fd = fopen(snap, "r")) == NULL)
 162         {       snap[strlen(snap)-2] = '\0';    /* .tra */
 163                 if ((fd = fopen(snap, "r")) == NULL)
 164                 {       if ((q = strchr(oFname->name, '.')) != NULL)
 165                         {       *q = '\0';
 166                                 if (ntrail)
 167                                         sprintf(snap, "%s%d.trail",
 168                                                 oFname->name, ntrail);
 169                                 else
 170                                         sprintf(snap, "%s.trail",
 171                                                 oFname->name);
 172                                 *q = '.';
 173
 174                                 if ((fd = fopen(snap, "r")) != NULL)
 175                                         goto okay;
 176
 177                                 snap[strlen(snap)-2] = '\0';    /* last try */
 178                                 if ((fd = fopen(snap, "r")) != NULL)
 179                                         goto okay;
 180                         }
 181                         printf("spin: cannot find trail file\n");
 182                         alldone(1);
 183         }       }
 184 okay:
 185         if (xspin == 0 && newer(oFname->name, snap))
 186         {       printf("spin: warning, \"%s\" is newer than %s\n",
 187                         oFname->name, snap);
 188         }
 189         Tval = 1;
 190
 191         /*
 192          * sets Tval because timeouts may be part of trail
 193          * this used to also set m_loss to 1, but that is
 194          * better handled with the runtime -m flag
 195          */
 196
 197         hookup();
 198
 199         while (fscanf(fd, "%d:%d:%d\n", &depth, &pno, &nst) == 3)
 200         {       if (depth == -2)
 201                 {       if (verbose)
 202                         {       printf("starting claim %d\n", pno);
 203                         }
 204                         start_claim(pno);
 205                         continue;
 206                 }
 207                 if (depth == -4)
 208                 {       if (verbose)
 209                         {       printf("using statement merging\n");
 210                         }
 211                         merger = 1;
 212                         ana_src(0, 1);
 213                         continue;
 214                 }
 215                 if (depth == -1)
 216                 {       if (1 || verbose)
 217                         {       if (columns == 2)
 218                                 dotag(stdout, " CYCLE>\n");
 219                                 else
 220                                 dotag(stdout, "<<<<<START OF CYCLE>>>>>\n");
 221                         }
 222                         continue;
 223                 }
 224
 225                 if (cutoff > 0 && depth >= cutoff)
 226                 {       printf("-------------\n");
 227                         printf("depth-limit (-u%d steps) reached\n", cutoff);
 228                         break;
 229                 }
 230
 231                 if (Skip_claim && pno == 0) continue;
 232
 233                 for (dothis = Al_El; dothis; dothis = dothis->Nxt)
 234                 {       if (dothis->Seqno == nst)
 235                                 break;
 236                 }
 237                 if (!dothis)
 238                 {       printf("%3d: proc %d, no matching stmnt %d\n",
 239                                 depth, pno - Have_claim, nst);
 240                         lost_trail();
 241                 }
 242
 243                 i = nproc - nstop + Skip_claim;
 244
 245                 if (dothis->n->ntyp == '@')
 246                 {       if (pno == i-1)
 247                         {       run = run->nxt;
 248                                 nstop++;
 249                                 if (verbose&4)
 250                                 {       if (columns == 2)
 251                                         {       dotag(stdout, "<end>\n");
 252                                                 continue;
 253                                         }
 254                                         if (Have_claim && pno == 0)
 255                                         printf("%3d: claim terminates\n",
 256                                                 depth);
 257                                         else
 258                                         printf("%3d: proc %d terminates\n",
 259                                                 depth, pno - Have_claim);
 260                                 }
 261                                 continue;
 262                         }
 263                         if (pno <= 1) continue; /* init dies before never */
 264                         printf("%3d: stop error, ", depth);
 265                         printf("proc %d (i=%d) trans %d, %c\n",
 266                                 pno - Have_claim, i, nst, dothis->n->ntyp);
 267                         lost_trail();
 268                 }
 269
 270                 if (0 && !xspin && (verbose&32))
 271                 {       printf("step %d i=%d pno %d stmnt %d\n", depth, i, pno, nst);
 272                 }
 273
 274                 for (X = run; X; X = X->nxt)
 275                 {       if (--i == pno)
 276                                 break;
 277                 }
 278
 279                 if (!X)
 280                 {       if (verbose&32)
 281                         {       printf("%3d: no process %d (stmnt %d)\n", depth, pno - Have_claim, nst);
 282                                 printf(" max %d (%d - %d + %d) claim %d ",
 283                                         nproc - nstop + Skip_claim,
 284                                         nproc, nstop, Skip_claim, Have_claim);
 285                                 printf("active processes:\n");
 286                                 for (X = run; X; X = X->nxt)
 287                                 {       printf("\tpid %d\tproctype %s\n", X->pid, X->n->name);
 288                                 }
 289                                 printf("\n");
 290                                 continue;
 291                         } else
 292                         {       printf("%3d:\tproc  %d (?) ", depth, pno);
 293                                 lost_trail();
 294                         }
 295                 } else
 296                 {       int min_seq = find_min(X->ps);
 297                         int max_seq = find_max(X->ps);
 298
 299
 300                         if (nst < min_seq || nst > max_seq)
 301                         {       printf("%3d: error: invalid statement", depth);
 302                                 if (verbose&32)
 303                                 {       printf(": pid %d:%d (%s:%d:%d) stmnt %d (valid range %d .. %d)",
 304                                         pno, X->pid, X->n->name, X->tn, X->b, nst, min_seq, max_seq);
 305                                 }
 306                                 printf("\n");
 307                                 continue;
 308                                 /* lost_trail(); */
 309                         }
 310                         X->pc  = dothis;
 311                 }
 312
 313                 lineno = dothis->n->ln;
 314                 Fname  = dothis->n->fn;
 315
 316                 if (dothis->n->ntyp == D_STEP)
 317                 {       Element *g, *og = dothis;
 318                         do {
 319                                 g = eval_sub(og);
 320                                 if (g && depth >= jumpsteps
 321                                 && ((verbose&32) || ((verbose&4) && not_claim())))
 322                                 {       if (columns != 2)
 323                                         {       p_talk(og, 1);
 324
 325                                                 if (og->n->ntyp == D_STEP)
 326                                                 og = og->n->sl->this->frst;
 327
 328                                                 printf("\t[");
 329                                                 comment(stdout, og->n, 0);
 330                                                 printf("]\n");
 331                                         }
 332                                         if (verbose&1) dumpglobals();
 333                                         if (verbose&2) dumplocal(X);
 334                                         if (xspin) printf("\n");
 335                                 }
 336                                 og = g;
 337                         } while (g && g != dothis->nxt);
 338                         if (X != NULL)
 339                         {       X->pc = g?huntele(g, 0, -1):g;
 340                         }
 341                 } else
 342                 {
 343 keepgoing:              if (dothis->merge_start)
 344                                 a = dothis->merge_start;
 345                         else
 346                                 a = dothis->merge;
 347
 348                         if (X != NULL)
 349                         {       X->pc = eval_sub(dothis);
 350                                 if (X->pc) X->pc = huntele(X->pc, 0, a);
 351                         }
 352
 353                         if (depth >= jumpsteps
 354                         && ((verbose&32) || ((verbose&4) && not_claim())))      /* -v or -p */
 355                         {       if (columns != 2)
 356                                 {       p_talk(dothis, 1);
 357
 358                                         if (dothis->n->ntyp == D_STEP)
 359                                         dothis = dothis->n->sl->this->frst;
 360
 361                                         printf("\t[");
 362                                         comment(stdout, dothis->n, 0);
 363                                         printf("]");
 364                                         if (a && (verbose&32))
 365                                         printf("\t<merge %d now @%d>",
 366                                                 dothis->merge,
 367                                                 (X && X->pc)?X->pc->seqno:-1);
 368                                         printf("\n");
 369                                 }
 370                                 if (verbose&1) dumpglobals();
 371                                 if (verbose&2) dumplocal(X);
 372                                 if (xspin) printf("\n");
 373
 374                                 if (X && !X->pc)
 375                                 {       X->pc = dothis;
 376                                         printf("\ttransition failed\n");
 377                                         a = 0;  /* avoid inf loop */
 378                                 }
 379                         }
 380                         if (a && X && X->pc && X->pc->seqno != a)
 381                         {       dothis = X->pc;
 382                                 goto keepgoing;
 383                 }       }
 384
 385                 if (Have_claim && X && X->pid == 0
 386                 &&  dothis->n
 387                 &&  lastclaim != dothis->n->ln)
 388                 {       lastclaim = dothis->n->ln;
 389                         if (columns == 2)
 390                         {       char t[128];
 391                                 sprintf(t, "#%d", lastclaim);
 392                                 pstext(0, t);
 393                         } else
 394                         {
 395                                 printf("Never claim moves to line %d\t[", lastclaim);
 396                                 comment(stdout, dothis->n, 0);
 397                                 printf("]\n");
 398         }       }       }
 399         printf("spin: trail ends after %d steps\n", depth);
 400         wrapup(0);
 401 }
 402
 403 static void
 404 lost_trail(void)
 405 {       int d, p, n, l;
 406
 407         while (fscanf(fd, "%d:%d:%d:%d\n", &d, &p, &n, &l) == 4)
 408         {       printf("step %d: proc  %d ", d, p); whichproc(p);
 409                 printf("(state %d) - d %d\n", n, l);
 410         }
 411         wrapup(1);      /* no return */
 412 }
 413
 414 int
 415 pc_value(Lextok *n)
 416 {       int i = nproc - nstop;
 417         int pid = eval(n);
 418         RunList *Y;
 419
 420         for (Y = run; Y; Y = Y->nxt)
 421         {       if (--i == pid)
 422                         return Y->pc->seqno;
 423         }
 424         return 0;
 425 }