From de083bc50c888b469967596333958aa064f3d2b6 Mon Sep 17 00:00:00 2001 From: Kilo <209128140+bivex@users.noreply.github.com> Date: Sun, 9 Aug 2026 22:07:47 +0300 Subject: [PATCH 1/2] docs: update README.md with comprehensive overview, setup, and usage guides --- README.md | 144 +++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 120 insertions(+), 24 deletions(-) diff --git a/README.md b/README.md index d6f02c02..3dd6f7f1 100644 --- a/README.md +++ b/README.md @@ -1,26 +1,122 @@ # Spin -## An Efficient Logic Model Checker for the Verification of Multi-threaded Code - -Spin is an open-source software verification tool that was originally -developed (starting in 1980) in the Computing Science Research Center of Bell Labs -(the Unix group). It is often considered the most widely used formal verification tool. - -Compilation and installation is trivial (see the makefile) and the only dependencies -are the use of a C compiler, yacc or byacc, and a small number of standard -unix/linux/cygwin-like tools (like make, mv, and rm). With help of a related tool -[Modex](http://spinroot.com/modex) Spin can verify C code directly, but the most -common use of the tool is to write a formal specification of the essence of an -application to be verified in a C-like meta-language called ProMeLa (Process Meta -Language). Annual Symposia and Workshops on the tool have been held since 1995. - -The main site for access to manuals, tutorials, and papers explaining the theory -behind the tool is [http://spinroot.com](http://spinroot.com). - -This repository contains the most recent version of the sources. Updates that are more -recent than the version.h files were made after the most recent release. When a new -release is issued, the version.h file is also updated. - -The tool supports a range of different verification algorithms, including depth-first, -breadth-first, parallel/multi-core, bounded depth, bitstate search (using Bloom filter -theory), partial order reduced, and swarm search (using arbitrarily many cpus). + +> **An Efficient Logic Model Checker for the Formal Verification of Multi-threaded Software** + +Spin is an open-source software verification tool originally developed starting in 1980 by Gerard J. Holzmann in the Computing Science Research Center of Bell Labs (the Unix group). It is widely considered one of the most powerful and popular formal verification tools available. + +--- + +## πŸ“Œ Overview + +Spin is designed for formal verification of multi-threaded, concurrent, and distributed software systems. + +Applications are typically specified in a high-level modeling language called **PROMELA** (*Process Meta Language*). Spin can simulate system executions or generate optimized C source code (`pan.c`) that exhaustively verifies the system for properties such as: +- **Deadlocks** (invalid end states) +- **Data Races & Invariant Violations** (assert failures) +- **Unreachable Code** +- **LTL Properties** (Linear Temporal Logic formulas for safety and liveness) + +Spin can also be used directly with C source code via the companion tool [Modex](http://spinroot.com/modex). + +--- + +## ✨ Features & Verification Algorithms + +Spin supports a broad range of formal verification algorithms and state-space reduction techniques: + +- **Depth-First Search (DFS) & Breadth-First Search (BFS)** +- **Partial Order Reduction (POR)** for state space compression +- **Bitstate Search** (using Bloom filter techniques for extremely large state spaces) +- **Multi-Core / Parallel Verification** +- **Bounded-Depth Search** +- **Swarm Search** (randomized parallel search across CPU cores) +- **LTL to BΓΌchi Automata** conversion for temporal logic checks + +--- + +## πŸ› οΈ Build and Installation + +### Prerequisites + +To compile Spin, you need standard C build tools: +- A **C Compiler** (`gcc` or `clang`) +- **`yacc`** or **`byacc`** (or `bison -y`) +- Standard Unix utilities (`make`, `mv`, `rm`) + +### Compilation + +Clone the repository and build using `make`: + +```bash +git clone https://github.com/nimble-code/Spin.git +cd Spin +make +``` + +To install the `spin` executable into standard PATH (`/usr/local/bin` by default): + +```bash +sudo make install +``` + +--- + +## πŸš€ Quick Start + +### 1. Simulation Mode + +You can run a random simulation of a PROMELA model (e.g. from the [`Examples/`](file:///Volumes/External/Code/Spin/Examples) directory): + +```bash +spin Examples/hello.pml +``` + +### 2. Verification Mode + +To perform an exhaustive verification of a specification: + +```bash +# 1. Generate the verifier source code (pan.c) +spin -a model.pml + +# 2. Compile the verifier +gcc -O2 -o pan pan.c + +# 3. Run the verifier to search for errors +./pan +``` + +If an error (e.g. deadlock or assertion failure) is found, a trace file (`model.pml.trail`) is generated. You can replay the error path with: + +```bash +spin -t -p model.pml +``` + +--- + +## πŸ–₯️ Graphical Interface (iSpin) + +Spin includes an optional Tcl/Tk-based GUI named **iSpin**, located in [`optional_gui/ispin.tcl`](file:///Volumes/External/Code/Spin/optional_gui/ispin.tcl). + +To run iSpin (requires Tcl/Tk installed): + +```bash +wish optional_gui/ispin.tcl +``` + +--- + +## πŸ“– Documentation & Links + +- **Official Website**: [http://spinroot.com](http://spinroot.com) +- **Manuals & Tutorials**: [http://spinroot.com/spin/Man/](http://spinroot.com/spin/Man/) +- **Examples**: See the [`Examples/`](file:///Volumes/External/Code/Spin/Examples) directory. +- **Documentation Papers & Books**: See the [`Doc/`](file:///Volumes/External/Code/Spin/Doc) directory. + +--- + +## πŸ“„ License + +Spin is released under a BSD 3-Clause License. See [`LICENSE`](file:///Volumes/External/Code/Spin/LICENSE) for full details. + From fd3f8d0e9437aecb6ab6779cd0fbad940d7f6581 Mon Sep 17 00:00:00 2001 From: Kilo <209128140+bivex@users.noreply.github.com> Date: Sun, 9 Aug 2026 22:11:38 +0300 Subject: [PATCH 2/2] fix(pvs): resolve all High Level (Level 1) static analyzer warnings - Fix potential buffer overflow and bounds check in main.c (preprocess) - Fix termios c_lflag bitmask truncation on 64-bit platforms in mesg.c - Fix potential null pointer dereferences in pangen2.c, pangen3.c, and run.c - Fix undefined behavior in 64-bit bit shift operations (1UL<= sizeof(precmd)) + { fprintf(stdout, "spin: too many -D args, aborting\n"); + alldone(1); + } + strcat(precmd, " "); strcat(precmd, PreArg[i]); } - if (strlen(precmd) > sizeof(precmd)) - { fprintf(stdout, "spin: too many -D args, aborting\n"); - alldone(1); - } sprintf(cmd, "%s \"%s\" > \"%s\"", precmd, a, b); if (e_system(2, (const char *)cmd)) /* preprocessing step */ { (void) unlink((const char *) b); diff --git a/Src/mesg.c b/Src/mesg.c index 662f812f..14a6af25 100644 --- a/Src/mesg.c +++ b/Src/mesg.c @@ -163,9 +163,9 @@ qsend(Lextok *n) tcgetattr(0,&initial_settings); new_settings = initial_settings; - new_settings.c_lflag &= ~ICANON; - new_settings.c_lflag &= ~ECHO; - new_settings.c_lflag &= ~ISIG; + new_settings.c_lflag &= ~(tcflag_t)ICANON; + new_settings.c_lflag &= ~(tcflag_t)ECHO; + new_settings.c_lflag &= ~(tcflag_t)ISIG; new_settings.c_cc[VMIN] = 0; new_settings.c_cc[VTIME] = 0; } diff --git a/Src/pangen2.c b/Src/pangen2.c index c8b7e8f9..fa487f34 100644 --- a/Src/pangen2.c +++ b/Src/pangen2.c @@ -3204,7 +3204,8 @@ putstmnt(FILE *fd, Lextok *now, int m) case PRINTM: { char *s = 0; - if (now->lft->sym + if (now->lft + && now->lft->sym && now->lft->sym->mtype_name) { s = now->lft->sym->mtype_name->name; } diff --git a/Src/pangen3.c b/Src/pangen3.c index 9e2a33e1..c7a732d4 100644 --- a/Src/pangen3.c +++ b/Src/pangen3.c @@ -454,10 +454,7 @@ comwork(FILE *fd, Lextok *now, int m) if (c == '\"') buf[j] = '\''; if (c == '\0') break; } - if (now->ntyp == PRINT) - fprintf(fd, "printf"); - else - fprintf(fd, "annotate"); + fprintf(fd, "printf"); fprintf(fd, "(%s", buf); } for (v = now->lft; v; v = v->rgt) @@ -467,7 +464,8 @@ comwork(FILE *fd, Lextok *now, int m) break; case PRINTM: fprintf(fd, "printm("); { char *s = 0; - if (now->lft->sym + if (now->lft + && now->lft->sym && now->lft->sym->mtype_name) { s = now->lft->sym->mtype_name->name; } diff --git a/Src/pangen6.c b/Src/pangen6.c index df8e08d8..3f2a7b0f 100644 --- a/Src/pangen6.c +++ b/Src/pangen6.c @@ -264,7 +264,7 @@ def_use(Lextok *now, int code) def_use(now->lft, DEREF_DEF|DEREF_USE|USE|code); for (v = now->rgt; v; v = v->rgt) { if (v->lft->ntyp == EVAL) - { if (v->lft->ntyp == ',') + { if (v->lft->lft && v->lft->lft->ntyp == ',') { def_use(v->lft->lft, code); /* will add USE */ } else { def_use(v->lft, code); /* will add USE */ @@ -278,7 +278,7 @@ def_use(Lextok *now, int code) def_use(now->lft, DEREF_USE|USE|code); for (v = now->rgt; v; v = v->rgt) { if (v->lft->ntyp == EVAL) - { if (v->lft->ntyp == ',') + { if (v->lft->lft && v->lft->lft->ntyp == ',') { def_use(v->lft->lft, code); /* will add USE */ } else { def_use(v->lft, code); /* will add USE */ @@ -2001,9 +2001,9 @@ subgraph(AST *a, FSM_state *f, int out) if (verbose&32) printf("possible pair %d %d -- %d\n", - f->from, h->from, (g[i]&(1<from, h->from, (g[i]&(1UL<from); /* record this pair */ } @@ -2036,7 +2036,7 @@ act_dom(AST *a) } i = cnt / BPW; j = cnt % BPW; /* assert(j <= 32); */ - if (!(f->dom[i]&(1<dom[i]&(1UL<t, i = 0; t; t = t->nxt) @@ -2186,20 +2186,20 @@ init_dom(AST *a) if (f->from == a->i_st) { i = a->i_st / BPW; j = a->i_st % BPW; /* assert(j <= 32); */ - f->dom[i] = (1<dom[i] = (1UL<nwords; i++) { f->dom[i] = (ulong) ~0; /* all 1's */ } if (a->nstates % BPW) for (i = (a->nstates % BPW); i < (int) BPW; i++) - { f->dom[a->nwords-1] &= ~(1<< ((ulong) i)); /* clear tail */ + { f->dom[a->nwords-1] &= ~(1UL<< ((ulong) i)); /* clear tail */ } for (cnt = 0; cnt < a->nstates; cnt++) { if (!fsm_tbl[cnt]->seen) { i = cnt / BPW; j = cnt % BPW; /* assert(j <= 32); */ - f->dom[i] &= ~(1<< ((ulong) j)); + f->dom[i] &= ~(1UL<< ((ulong) j)); } } } } } @@ -2229,7 +2229,7 @@ dom_perculate(AST *a, FSM_state *f) i = f->from / BPW; j = f->from % BPW; /* assert(j <= 32); */ - ndom[i] |= (1<nwords; i++) if (f->dom[i] != ndom[i]) diff --git a/Src/pangen7.c b/Src/pangen7.c index b6b492ed..38a4413f 100644 --- a/Src/pangen7.c +++ b/Src/pangen7.c @@ -834,9 +834,7 @@ set_el(int n, Element *e) e->nxt = e; g = e; mk_accepting(n, e); - } else - - if (e->n->ntyp == GOTO) + } else if (e->n->ntyp == GOTO) { g = get_lab(e->n, 1); g = huntele(g, e->status, -1); } else if (e->nxt) diff --git a/Src/run.c b/Src/run.c index ad7c8a4e..f3f56726 100644 --- a/Src/run.c +++ b/Src/run.c @@ -173,7 +173,7 @@ eval_sub(Element *e) { if (e->n && e->n->indstep >= 0) k = 0; /* select 1st executable guard */ else - k = Rand()%j; /* nondeterminism */ + k = (j > 0) ? (Rand()%j) : 0; /* nondeterminism */ } has_else = ZE; @@ -646,7 +646,9 @@ Enabled0(Element *e) if (Rvous) return 0; return 1; case UNLESS: - return Enabled0(e->sub->this->frst); + if (e->sub && e->sub->this) + return Enabled0(e->sub->this->frst); + return 0; case ATOMIC: case D_STEP: case NON_ATOMIC: