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