projects / lttv.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
update verif
[lttv.git] / trunk / verif / examples / pan.h
CommitLineData
0b55f123 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
10char *TrailFile = PanSource; /* default */
11char *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
2eb837fb 26#ifndef HASH32
27#define HASH64
28#endif
0b55f123 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
55typedef struct S_F_MAP {
56 char *fnm; int from; int upto;
57} S_F_MAP;
58
2eb837fb 59#define nstates4 57 /* :init: */
60#define endstate4 56
0b55f123 61short src_ln4 [] = {
2eb837fb 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, };
0b55f123 70S_F_MAP src_file4 [] = {
71 { "-", 0, 0 },
2eb837fb 72 { "buffer.spin", 1, 56 },
73 { "-", 57, 58 }
0b55f123 74};
75uchar reached4 [] = {
2eb837fb 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,
0b55f123 79 0, 0, 1, 1, 0, 1, 1, 0,
2eb837fb 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, };
0b55f123 84uchar *loopstate4;
85
86#define nstates3 10 /* cleaner */
87#define endstate3 9
88short src_ln3 [] = {
2eb837fb 89 0, 211, 212, 213, 214, 210, 216, 210,
90 209, 217, 0, };
0b55f123 91S_F_MAP src_file3 [] = {
92 { "-", 0, 0 },
93 { "buffer.spin", 1, 9 },
94 { "-", 10, 11 }
95};
96uchar reached3 [] = {
97 0, 1, 0, 0, 1, 0, 1, 1,
98 0, 0, 0, };
99uchar *loopstate3;
100
2eb837fb 101#define nstates2 30 /* reader */
102#define endstate2 29
0b55f123 103short src_ln2 [] = {
2eb837fb 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, };
0b55f123 108S_F_MAP src_file2 [] = {
109 { "-", 0, 0 },
2eb837fb 110 { "buffer.spin", 1, 29 },
111 { "-", 30, 31 }
0b55f123 112};
113uchar 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,
2eb837fb 117 1, 1, 0, 1, 1, 0, 0, };
0b55f123 118uchar *loopstate2;
119
120#define nstates1 51 /* tracer */
121#define endstate1 50
122short src_ln1 [] = {
2eb837fb 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, };
0b55f123 130S_F_MAP src_file1 [] = {
131 { "-", 0, 0 },
132 { "buffer.spin", 1, 50 },
133 { "-", 51, 52 }
134};
135uchar 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, };
143uchar *loopstate1;
144
145#define nstates0 31 /* switcher */
146#define endstate0 30
147short src_ln0 [] = {
2eb837fb 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, };
0b55f123 152S_F_MAP src_file0 [] = {
153 { "-", 0, 0 },
154 { "buffer.spin", 1, 30 },
155 { "-", 31, 32 }
156};
157uchar 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, };
162uchar *loopstate0;
163struct {
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};
173short *frm_st0;
174struct {
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
194char *procname[] = {
195 "switcher",
196 "tracer",
197 "reader",
198 "cleaner",
199 ":init:",
200 ":np_:",
201};
202
203#define Pinit ((P4 *)this)
204typedef 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)
215typedef 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)
222typedef 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;
0b55f123 228} P2;
2eb837fb 229#define Air2 (sizeof(P2) - Offsetof(P2, j) - 1*sizeof(uchar))
0b55f123 230#define Ptracer ((P1 *)this)
231typedef 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)
244typedef 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))
254typedef 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
268typedef 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])
290extern 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)
361unsigned long *ncomps; /* in shared memory */
362#else
363unsigned 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 */
369typedef 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
390typedef 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
407Trans ***trans; /* 1 ptr per state per proctype */
408
409struct H_el *Lstate;
410int depthfound = -1; /* loop detection */
411#if VECTORSZ>32000
412int proc_offset[MAXPROC];
413int q_offset[MAXQ];
414#else
415short proc_offset[MAXPROC];
416short q_offset[MAXQ];
417#endif
418uchar proc_skip[MAXPROC];
419uchar q_skip[MAXQ];
420unsigned long vsize; /* vector size in bytes */
421#ifdef SVDUMP
422int vprefix=0, svfd; /* runtime option -pN */
423#endif
424char *tprefix = "trail"; /* runtime option -tsuffix */
425short boq = -1; /* blocked_on_queue status */
426typedef 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;
0b55f123 454 uchar events_lost;
455 uchar refcount;
456 uchar sv[VECTORSZ];
457} State;
458
459#define HAS_TRACK 0
460/* hidden variable: */ uchar deliver;
461int _; /* 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
467uchar reached5[3]; /* np_ */
468uchar *loopstate5; /* np_ */
469#define nstates5 3 /* np_ */
470#define endstate5 2 /* np_ */
471
472#define start5 0 /* np_ */
2eb837fb 473#define start4 41
0b55f123 474#define start3 8
2eb837fb 475#define start2 26
0b55f123 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 */
510uchar *accpstate[6];
511uchar *progstate[6];
512uchar *loopstate[6];
513uchar *reached[6];
514uchar *stopstate[6];
515uchar *visstate[6];
516short *mapstate[6];
517#ifdef HAS_CODE
518int NrStates[6];
519#endif
520#define NQS 0
521short q_flds[1];
522short q_max[1];
523typedef struct Q0 { /* generic q */
524 uchar Qlen; /* q_size */
525 uchar _t;
526} Q0;
527
528/** function prototypes **/
529char *emalloc(unsigned long);
530char *Malloc(unsigned long);
531int Boundcheck(int, int, int, int, Trans *);
532int addqueue(int, int);
533/* int atoi(char *); */
534/* int abort(void); */
535int close(int);
536int delproc(int, int);
537int endstate(void);
538int hstore(char *, int);
539#ifdef MA
540int gstore(char *, int, uchar);
541#endif
542int q_cond(short, Trans *);
543int q_full(int);
544int q_len(int);
545int q_zero(int);
546int qrecv(int, int, int, int);
547int unsend(int);
548/* void *sbrk(int); */
549void Uerror(char *);
550void assert(int, char *, int, int, Trans *);
551void c_chandump(int);
552void c_globals(void);
553void c_locals(int, int);
554void checkcycles(void);
555void crack(int, int, Trans *, short *);
556void d_sfh(const char *, int);
557void sfh(const char *, int);
558void d_hash(uchar *, int);
559void s_hash(uchar *, int);
560void r_hash(uchar *, int);
561void delq(int);
562void do_reach(void);
563void pan_exit(int);
564void exit(int);
565void hinit(void);
566void imed(Trans *, int, int, int);
567void new_state(void);
568void p_restor(int);
569void putpeg(int, int);
570void putrail(void);
571void q_restor(void);
572void retrans(int, int, int, short *, uchar *, uchar *);
573void settable(void);
574void setq_claim(int, int, char *, int, char *);
575void sv_restor(void);
576void sv_save(void);
577void tagtable(int, int, int, short *, uchar *);
578void do_dfs(int, int, int, short *, uchar *, uchar *);
579void uerror(char *);
580void unrecv(int, int, int, int, int);
581void usage(FILE *);
582void wrap_stats(void);
583#if defined(FULLSTACK) && defined(BITSTATE)
584int onstack_now(void);
585void onstack_init(void);
586void onstack_put(void);
587void onstack_zap(void);
588#endif
589#ifndef XUSAFE
590int q_S_check(int, int);
591int q_R_check(int, int);
592uchar q_claim[MAXQ+1];
593char *q_name[MAXQ+1];
594char *p_name[MAXPROC+1];
595#endif
596void 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
609long peg[NTRANS];
610#endif
LTTng 2.x Viewer (LTTV)
This page took 0.044104 seconds and 4 git commands to generate.