trunk/verif/examples/pan.h

   1 #define SpinVersion     "Spin Version 5.1.6 -- 9 May 2008"
   2 #define PanSource       "buffer.spin"
   3
   4 #ifdef WIN64
   5 #define ONE_L   ((unsigned long) 1)
   6 #define long    long long
   7 #else
   8 #define ONE_L   (1L)
   9 #endif
  10 char *TrailFile = PanSource; /* default */
  11 char *trailfilename;
  12 #if defined(BFS)
  13 #ifndef SAFETY
  14 #define SAFETY
  15 #endif
  16 #ifndef XUSAFE
  17 #define XUSAFE
  18 #endif
  19 #endif
  20 #ifndef uchar
  21 #define uchar   unsigned char
  22 #endif
  23 #ifndef uint
  24 #define uint    unsigned int
  25 #endif
  26 #define DELTA   500
  27 #ifdef MA
  28         #if NCORE>1 && !defined(SEP_STATE)
  29         #define SEP_STATE
  30         #endif
  31 #if MA==1
  32 #undef MA
  33 #define MA      100
  34 #endif
  35 #endif
  36 #ifdef W_XPT
  37 #if W_XPT==1
  38 #undef W_XPT
  39 #define W_XPT 1000000
  40 #endif
  41 #endif
  42 #ifndef NFAIR
  43 #define NFAIR   2       /* must be >= 2 */
  44 #endif
  45 #define HAS_CODE
  46 #define MERGED  1
  47 #ifdef NP       /* includes np_ demon */
  48 #define HAS_NP  2
  49 #define VERI    5
  50 #define endclaim        3 /* none */
  51 #endif
  52 typedef struct S_F_MAP {
  53         char *fnm; int from; int upto;
  54 } S_F_MAP;
  55
  56 #define nstates4        59      /* :init: */
  57 #define endstate4       58
  58 short src_ln4 [] = {
  59           0, 225, 227, 228, 229, 230, 231, 231,
  60         226, 233, 226, 233, 235, 236, 237, 238,
  61         238, 234, 240, 234, 240, 241, 242, 244,
  62         245, 246, 247, 248, 248, 243, 250, 243,
  63         250, 252, 253, 254, 255, 256, 256, 251,
  64         258, 251, 224, 262, 263, 264, 266, 267,
  65         271, 272, 273, 273, 265, 278, 265, 278,
  66         282, 260, 284,   0, };
  67 S_F_MAP src_file4 [] = {
  68         { "-", 0, 0 },
  69         { "buffer.spin", 1, 58 },
  70         { "-", 59, 60 }
  71 };
  72 uchar reached4 [] = {
  73           0,   1,   1,   0,   0,   0,   1,   1,
  74           0,   1,   1,   0,   1,   0,   0,   1,
  75           1,   0,   1,   1,   0,   0,   0,   1,
  76           0,   0,   0,   1,   1,   0,   1,   1,
  77           0,   1,   0,   0,   0,   1,   1,   0,
  78           1,   1,   0,   1,   0,   0,   1,   0,
  79           0,   0,   1,   1,   0,   1,   1,   0,
  80           0,   0,   0,   0, };
  81 uchar *loopstate4;
  82
  83 #define nstates3        10      /* cleaner */
  84 #define endstate3       9
  85 short src_ln3 [] = {
  86           0, 210, 211, 212, 213, 209, 215, 209,
  87         208, 216,   0, };
  88 S_F_MAP src_file3 [] = {
  89         { "-", 0, 0 },
  90         { "buffer.spin", 1, 9 },
  91         { "-", 10, 11 }
  92 };
  93 uchar reached3 [] = {
  94           0,   1,   0,   0,   1,   0,   1,   1,
  95           0,   0,   0, };
  96 uchar *loopstate3;
  97
  98 #define nstates2        32      /* reader */
  99 #define endstate2       31
 100 short src_ln2 [] = {
 101           0, 169, 171, 173, 174, 175, 176, 177,
 102         177, 172, 179, 172, 170, 187, 189, 190,
 103         191, 192, 192, 188, 194, 188, 194, 196,
 104         197, 186, 199, 199, 164, 201, 164, 201,
 105           0, };
 106 S_F_MAP src_file2 [] = {
 107         { "-", 0, 0 },
 108         { "buffer.spin", 1, 31 },
 109         { "-", 32, 33 }
 110 };
 111 uchar reached2 [] = {
 112           0,   1,   1,   1,   0,   0,   0,   1,
 113           1,   0,   1,   1,   0,   1,   1,   0,
 114           0,   1,   1,   0,   1,   1,   0,   0,
 115           0,   0,   1,   1,   0,   1,   1,   0,
 116           0, };
 117 uchar *loopstate2;
 118
 119 #define nstates1        51      /* tracer */
 120 #define endstate1       50
 121 short src_ln1 [] = {
 122           0,  99, 100,  98, 104, 105, 106, 106,
 123         103, 108, 102, 111, 111, 112, 112, 110,
 124         114, 114, 116, 117, 118, 119, 120, 120,
 125         115, 122, 115, 109, 127, 129, 130, 131,
 126         132, 132, 128, 134, 128, 134, 135, 137,
 127         137, 138, 138, 136, 140, 126, 142, 144,
 128         146, 141, 148,   0, };
 129 S_F_MAP src_file1 [] = {
 130         { "-", 0, 0 },
 131         { "buffer.spin", 1, 50 },
 132         { "-", 51, 52 }
 133 };
 134 uchar reached1 [] = {
 135           0,   1,   0,   0,   1,   1,   1,   0,
 136           1,   1,   0,   1,   1,   1,   0,   1,
 137           1,   0,   1,   0,   0,   0,   1,   1,
 138           0,   1,   1,   0,   1,   1,   0,   0,
 139           1,   1,   0,   1,   1,   0,   0,   1,
 140           0,   1,   0,   0,   1,   0,   1,   0,
 141           0,   0,   0,   0, };
 142 uchar *loopstate1;
 143
 144 #define nstates0        31      /* switcher */
 145 #define endstate0       30
 146 short src_ln0 [] = {
 147           0,  56,  57,  58,  61,  62,  63,  64,
 148          64,  59,  66,  55,  69,  69,  70,  70,
 149          68,  72,  67,  75,  76,  78,  78,  79,
 150          79,  77,  81,  81,  74,  84,  85,   0, };
 151 S_F_MAP src_file0 [] = {
 152         { "-", 0, 0 },
 153         { "buffer.spin", 1, 30 },
 154         { "-", 31, 32 }
 155 };
 156 uchar reached0 [] = {
 157           0,   1,   0,   0,   1,   0,   1,   1,
 158           0,   0,   1,   0,   1,   1,   1,   0,
 159           1,   1,   0,   1,   0,   1,   0,   1,
 160           0,   0,   1,   0,   0,   1,   0,   0, };
 161 uchar *loopstate0;
 162 struct {
 163         int tp; short *src;
 164 } src_all[] = {
 165         { 4, &src_ln4[0] },
 166         { 3, &src_ln3[0] },
 167         { 2, &src_ln2[0] },
 168         { 1, &src_ln1[0] },
 169         { 0, &src_ln0[0] },
 170         { 0, (short *) 0 }
 171 };
 172 short *frm_st0;
 173 struct {
 174         char *c; char *t;
 175 } code_lookup[] = {
 176         { (char *) 0, "" }
 177 };
 178 #define _T5     64
 179 #define _T2     65
 180 #define T_ID    unsigned char
 181 #define SYNC    0
 182 #define ASYNC   0
 183
 184 #ifndef NCORE
 185         #ifdef DUAL_CORE
 186                 #define NCORE   2
 187         #elif QUAD_CORE
 188                 #define NCORE   4
 189         #else
 190                 #define NCORE   1
 191         #endif
 192 #endif
 193 char *procname[] = {
 194    "switcher",
 195    "tracer",
 196    "reader",
 197    "cleaner",
 198    ":init:",
 199    ":np_:",
 200 };
 201
 202 #define Pinit   ((P4 *)this)
 203 typedef struct P4 { /* :init: */
 204         unsigned _pid : 8;  /* 0..255 */
 205         unsigned _t   : 4; /* proctype */
 206         unsigned _p   : 7; /* state    */
 207         uchar i;
 208         uchar j;
 209         uchar sum;
 210         uchar commit_sum;
 211 } P4;
 212 #define Air4    (sizeof(P4) - Offsetof(P4, commit_sum) - 1*sizeof(uchar))
 213 #define Pcleaner        ((P3 *)this)
 214 typedef struct P3 { /* cleaner */
 215         unsigned _pid : 8;  /* 0..255 */
 216         unsigned _t   : 4; /* proctype */
 217         unsigned _p   : 7; /* state    */
 218 } P3;
 219 #define Air3    (sizeof(P3) - 3)
 220 #define Preader ((P2 *)this)
 221 typedef struct P2 { /* reader */
 222         unsigned _pid : 8;  /* 0..255 */
 223         unsigned _t   : 4; /* proctype */
 224         unsigned _p   : 7; /* state    */
 225         uchar i;
 226         uchar j;
 227         uchar tmp_retrieve;
 228         uchar lwrite_off;
 229         uchar lcommit_count;
 230 } P2;
 231 #define Air2    (sizeof(P2) - Offsetof(P2, lcommit_count) - 1*sizeof(uchar))
 232 #define Ptracer ((P1 *)this)
 233 typedef struct P1 { /* tracer */
 234         unsigned _pid : 8;  /* 0..255 */
 235         unsigned _t   : 4; /* proctype */
 236         unsigned _p   : 7; /* state    */
 237         uchar size;
 238         uchar prev_off;
 239         uchar new_off;
 240         uchar tmp_commit;
 241         uchar i;
 242         uchar j;
 243 } P1;
 244 #define Air1    (sizeof(P1) - Offsetof(P1, j) - 1*sizeof(uchar))
 245 #define Pswitcher       ((P0 *)this)
 246 typedef struct P0 { /* switcher */
 247         unsigned _pid : 8;  /* 0..255 */
 248         unsigned _t   : 4; /* proctype */
 249         unsigned _p   : 7; /* state    */
 250         uchar prev_off;
 251         uchar new_off;
 252         uchar tmp_commit;
 253         uchar size;
 254 } P0;
 255 #define Air0    (sizeof(P0) - Offsetof(P0, size) - 1*sizeof(uchar))
 256 typedef struct P5 { /* np_ */
 257         unsigned _pid : 8;  /* 0..255 */
 258         unsigned _t   : 4; /* proctype */
 259         unsigned _p   : 7; /* state    */
 260 } P5;
 261 #define Air5    (sizeof(P5) - 3)
 262 #if defined(BFS) && defined(REACH)
 263 #undef REACH
 264 #endif
 265 #ifdef VERI
 266 #define BASE    1
 267 #else
 268 #define BASE    0
 269 #endif
 270 typedef struct Trans {
 271         short atom;     /* if &2 = atomic trans; if &8 local */
 272 #ifdef HAS_UNLESS
 273         short escp[HAS_UNLESS]; /* lists the escape states */
 274         short e_trans;  /* if set, this is an escp-trans */
 275 #endif
 276         short tpe[2];   /* class of operation (for reduction) */
 277         short qu[6];    /* for conditional selections: qid's  */
 278         uchar ty[6];    /* ditto: type's */
 279 #ifdef NIBIS
 280         short om;       /* completion status of preselects */
 281 #endif
 282         char *tp;       /* src txt of statement */
 283         int st;         /* the nextstate */
 284         int t_id;       /* transition id, unique within proc */
 285         int forw;       /* index forward transition */
 286         int back;       /* index return  transition */
 287         struct Trans *nxt;
 288 } Trans;
 289
 290 #define qptr(x) (((uchar *)&now)+(int)q_offset[x])
 291 #define pptr(x) (((uchar *)&now)+(int)proc_offset[x])
 292 extern uchar *Pptr(int);
 293 #define q_sz(x) (((Q0 *)qptr(x))->Qlen)
 294
 295 #ifndef VECTORSZ
 296 #define VECTORSZ        1024           /* sv   size in bytes */
 297 #endif
 298
 299 #ifdef VERBOSE
 300 #ifndef CHECK
 301 #define CHECK
 302 #endif
 303 #ifndef DEBUG
 304 #define DEBUG
 305 #endif
 306 #endif
 307 #ifdef SAFETY
 308 #ifndef NOFAIR
 309 #define NOFAIR
 310 #endif
 311 #endif
 312 #ifdef NOREDUCE
 313 #ifndef XUSAFE
 314 #define XUSAFE
 315 #endif
 316 #if !defined(SAFETY) && !defined(MA)
 317 #define FULLSTACK
 318 #endif
 319 #else
 320 #ifdef BITSTATE
 321 #if defined(SAFETY) && !defined(HASH64)
 322 #define CNTRSTACK
 323 #else
 324 #define FULLSTACK
 325 #endif
 326 #else
 327 #define FULLSTACK
 328 #endif
 329 #endif
 330 #ifdef BITSTATE
 331 #ifndef NOCOMP
 332 #define NOCOMP
 333 #endif
 334 #if !defined(LC) && defined(SC)
 335 #define LC
 336 #endif
 337 #endif
 338 #if defined(COLLAPSE2) || defined(COLLAPSE3) || defined(COLLAPSE4)
 339 /* accept the above for backward compatibility */
 340 #define COLLAPSE
 341 #endif
 342 #ifdef HC
 343 #undef HC
 344 #define HC4
 345 #endif
 346 #ifdef HC0
 347 #define HC      0
 348 #endif
 349 #ifdef HC1
 350 #define HC      1
 351 #endif
 352 #ifdef HC2
 353 #define HC      2
 354 #endif
 355 #ifdef HC3
 356 #define HC      3
 357 #endif
 358 #ifdef HC4
 359 #define HC      4
 360 #endif
 361 #ifdef COLLAPSE
 362 #if NCORE>1 && !defined(SEP_STATE)
 363 unsigned long *ncomps;  /* in shared memory */
 364 #else
 365 unsigned long ncomps[256+2];
 366 #endif
 367 #endif
 368 #define MAXQ    255
 369 #define MAXPROC 255
 370 #define WS              sizeof(void *) /* word size in bytes */
 371 typedef struct Stack  {  /* for queues and processes */
 372 #if VECTORSZ>32000
 373         int o_delta;
 374         int o_offset;
 375         int o_skip;
 376         int o_delqs;
 377 #else
 378         short o_delta;
 379         short o_offset;
 380         short o_skip;
 381         short o_delqs;
 382 #endif
 383         short o_boq;
 384 #ifndef XUSAFE
 385         char *o_name;
 386 #endif
 387         char *body;
 388         struct Stack *nxt;
 389         struct Stack *lst;
 390 } Stack;
 391
 392 typedef struct Svtack { /* for complete state vector */
 393 #if VECTORSZ>32000
 394         int o_delta;
 395         int m_delta;
 396 #else
 397         short o_delta;   /* current size of frame */
 398         short m_delta;   /* maximum size of frame */
 399 #endif
 400 #if SYNC
 401         short o_boq;
 402 #endif
 403 #define StackSize       (WS)
 404         char *body;
 405         struct Svtack *nxt;
 406         struct Svtack *lst;
 407 } Svtack;
 408
 409 Trans ***trans; /* 1 ptr per state per proctype */
 410
 411 struct H_el *Lstate;
 412 int depthfound = -1;    /* loop detection */
 413 #if VECTORSZ>32000
 414 int proc_offset[MAXPROC];
 415 int q_offset[MAXQ];
 416 #else
 417 short proc_offset[MAXPROC];
 418 short q_offset[MAXQ];
 419 #endif
 420 uchar proc_skip[MAXPROC];
 421 uchar q_skip[MAXQ];
 422 unsigned long  vsize;   /* vector size in bytes */
 423 #ifdef SVDUMP
 424 int vprefix=0, svfd;            /* runtime option -pN */
 425 #endif
 426 char *tprefix = "trail";        /* runtime option -tsuffix */
 427 short boq = -1;         /* blocked_on_queue status */
 428 typedef struct State {
 429         uchar _nr_pr;
 430         uchar _nr_qs;
 431         uchar   _a_t;   /* cycle detection */
 432 #ifndef NOFAIR
 433         uchar   _cnt[NFAIR];    /* counters, weak fairness */
 434 #endif
 435 #ifndef NOVSZ
 436 #if VECTORSZ<65536
 437         unsigned short _vsz;
 438 #else
 439         unsigned long  _vsz;
 440 #endif
 441 #endif
 442 #ifdef HAS_LAST
 443         uchar  _last;   /* pid executed in last step */
 444 #endif
 445 #ifdef EVENT_TRACE
 446 #if nstates_event<256
 447         uchar _event;
 448 #else
 449         unsigned short _event;
 450 #endif
 451 #endif
 452         uchar buffer_use[4];
 453         uchar write_off;
 454         uchar commit_count[2];
 455         uchar read_off;
 456         uchar retrieve_count[2];
 457         uchar events_lost;
 458         uchar refcount;
 459         uchar sv[VECTORSZ];
 460 } State;
 461
 462 #define HAS_TRACK       0
 463 /* hidden variable: */  uchar deliver;
 464 int _; /* a predefined write-only variable */
 465
 466 #define FORWARD_MOVES   "pan.m"
 467 #define REVERSE_MOVES   "pan.b"
 468 #define TRANSITIONS     "pan.t"
 469 #define _NP_    5
 470 uchar reached5[3];  /* np_ */
 471 uchar *loopstate5;  /* np_ */
 472 #define nstates5        3 /* np_ */
 473 #define endstate5       2 /* np_ */
 474
 475 #define start5  0 /* np_ */
 476 #define start4  42
 477 #define start3  8
 478 #define start2  28
 479 #define start1  3
 480 #define start0  11
 481 #ifdef NP
 482         #define ACCEPT_LAB      1 /* at least 1 in np_ */
 483 #else
 484         #define ACCEPT_LAB      0 /* user-defined accept labels */
 485 #endif
 486 #ifdef MEMCNT
 487         #ifdef MEMLIM
 488                 #warning -DMEMLIM takes precedence over -DMEMCNT
 489                 #undef MEMCNT
 490         #else
 491                 #if MEMCNT<20
 492                         #warning using minimal value -DMEMCNT=20 (=1MB)
 493                         #define MEMLIM  (1)
 494                         #undef MEMCNT
 495                 #else
 496                         #if MEMCNT==20
 497                                 #define MEMLIM  (1)
 498                                 #undef MEMCNT
 499                         #else
 500                          #if MEMCNT>=50
 501                           #error excessive value for MEMCNT
 502                          #else
 503                                 #define MEMLIM  (1<<(MEMCNT-20))
 504                          #endif
 505                         #endif
 506                 #endif
 507         #endif
 508 #endif
 509 #if NCORE>1 && !defined(MEMLIM)
 510         #define MEMLIM  (2048)  /* need a default, using 2 GB */
 511 #endif
 512 #define PROG_LAB        0 /* progress labels */
 513 uchar *accpstate[6];
 514 uchar *progstate[6];
 515 uchar *loopstate[6];
 516 uchar *reached[6];
 517 uchar *stopstate[6];
 518 uchar *visstate[6];
 519 short *mapstate[6];
 520 #ifdef HAS_CODE
 521 int NrStates[6];
 522 #endif
 523 #define NQS     0
 524 short q_flds[1];
 525 short q_max[1];
 526 typedef struct Q0 {     /* generic q */
 527         uchar Qlen;     /* q_size */
 528         uchar _t;
 529 } Q0;
 530
 531 /** function prototypes **/
 532 char *emalloc(unsigned long);
 533 char *Malloc(unsigned long);
 534 int Boundcheck(int, int, int, int, Trans *);
 535 int addqueue(int, int);
 536 /* int atoi(char *); */
 537 /* int abort(void); */
 538 int close(int);
 539 int delproc(int, int);
 540 int endstate(void);
 541 int hstore(char *, int);
 542 #ifdef MA
 543 int gstore(char *, int, uchar);
 544 #endif
 545 int q_cond(short, Trans *);
 546 int q_full(int);
 547 int q_len(int);
 548 int q_zero(int);
 549 int qrecv(int, int, int, int);
 550 int unsend(int);
 551 /* void *sbrk(int); */
 552 void Uerror(char *);
 553 void assert(int, char *, int, int, Trans *);
 554 void c_chandump(int);
 555 void c_globals(void);
 556 void c_locals(int, int);
 557 void checkcycles(void);
 558 void crack(int, int, Trans *, short *);
 559 void d_sfh(const char *, int);
 560 void sfh(const char *, int);
 561 void d_hash(uchar *, int);
 562 void s_hash(uchar *, int);
 563 void r_hash(uchar *, int);
 564 void delq(int);
 565 void do_reach(void);
 566 void pan_exit(int);
 567 void exit(int);
 568 void hinit(void);
 569 void imed(Trans *, int, int, int);
 570 void new_state(void);
 571 void p_restor(int);
 572 void putpeg(int, int);
 573 void putrail(void);
 574 void q_restor(void);
 575 void retrans(int, int, int, short *, uchar *, uchar *);
 576 void settable(void);
 577 void setq_claim(int, int, char *, int, char *);
 578 void sv_restor(void);
 579 void sv_save(void);
 580 void tagtable(int, int, int, short *, uchar *);
 581 void do_dfs(int, int, int, short *, uchar *, uchar *);
 582 void uerror(char *);
 583 void unrecv(int, int, int, int, int);
 584 void usage(FILE *);
 585 void wrap_stats(void);
 586 #if defined(FULLSTACK) && defined(BITSTATE)
 587 int  onstack_now(void);
 588 void onstack_init(void);
 589 void onstack_put(void);
 590 void onstack_zap(void);
 591 #endif
 592 #ifndef XUSAFE
 593 int q_S_check(int, int);
 594 int q_R_check(int, int);
 595 uchar q_claim[MAXQ+1];
 596 char *q_name[MAXQ+1];
 597 char *p_name[MAXPROC+1];
 598 #endif
 599 void qsend(int, int, int);
 600 #define Addproc(x)      addproc(x)
 601 #define LOCAL   1
 602 #define Q_FULL_F        2
 603 #define Q_EMPT_F        3
 604 #define Q_EMPT_T        4
 605 #define Q_FULL_T        5
 606 #define TIMEOUT_F       6
 607 #define GLOBAL  7
 608 #define BAD     8
 609 #define ALPHA_F 9
 610 #define NTRANS  66
 611 #ifdef PEG
 612 long peg[NTRANS];
 613 #endif