Skip to content

Commit b4961ef

Browse files
committed
Initial commit
0 parents  commit b4961ef

153 files changed

Lines changed: 7406 additions & 0 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

.github/workflows/python-app.yml

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
# This workflow will install Python dependencies, run tests and lint with a single version of Python
2+
# For more information see: https://help.github.com/actions/language-and-framework-guides/using-python-with-github-actions
3+
4+
name: Python application
5+
6+
on:
7+
push:
8+
branches: [ master ]
9+
pull_request:
10+
branches: [ master ]
11+
12+
jobs:
13+
build:
14+
15+
runs-on: ubuntu-latest
16+
17+
steps:
18+
- uses: actions/checkout@v2
19+
- name: Set up Python 3.8
20+
uses: actions/setup-python@v2
21+
with:
22+
python-version: 3.8
23+
- name: Install dependencies
24+
run: |
25+
python -m pip install --upgrade pip
26+
pip install flake8 pytest
27+
if [ -f requirements.txt ]; then pip install -r requirements.txt; fi
28+
- name: Lint with flake8
29+
run: |
30+
# stop the build if there are Python syntax errors or undefined names
31+
flake8 . --count --select=E9,F63,F7,F82 --show-source --statistics
32+
# exit-zero treats all errors as warnings. The GitHub editor is 127 chars wide
33+
flake8 . --count --exit-zero --max-complexity=10 --max-line-length=127 --statistics
34+
- name: Test with pytest
35+
run: |
36+
pytest
Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
# This workflow will install Python dependencies, run tests and lint with a variety of Python versions
2+
# For more information see: https://help.github.com/actions/language-and-framework-guides/using-python-with-github-actions
3+
4+
name: Python package
5+
6+
on:
7+
push:
8+
branches: [ master ]
9+
pull_request:
10+
branches: [ master ]
11+
12+
jobs:
13+
build:
14+
15+
runs-on: ubuntu-latest
16+
strategy:
17+
matrix:
18+
python-version: [3.5, 3.6, 3.7, 3.8]
19+
20+
steps:
21+
- uses: actions/checkout@v2
22+
- name: Set up Python ${{ matrix.python-version }}
23+
uses: actions/setup-python@v2
24+
with:
25+
python-version: ${{ matrix.python-version }}
26+
- name: Install dependencies
27+
run: |
28+
python -m pip install --upgrade pip
29+
pip install flake8 pytest
30+
if [ -f requirements.txt ]; then pip install -r requirements.txt; fi
31+
- name: Lint with flake8
32+
run: |
33+
# stop the build if there are Python syntax errors or undefined names
34+
flake8 . --count --select=E9,F63,F7,F82 --show-source --statistics
35+
# exit-zero treats all errors as warnings. The GitHub editor is 127 chars wide
36+
flake8 . --count --exit-zero --max-complexity=10 --max-line-length=127 --statistics
37+
- name: Test with pytest
38+
run: |
39+
pytest

.gitignore

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
.idea/*
2+
build/*
3+
dist/*
4+
storm.egg-info/*
5+
temp/*
6+
.DS_Store
7+
config.py
8+
storm/fse_repl/bug1/mutant_*
9+
storm/fse_repl/bug2/mutant_*
10+
storm/fse_repl/bug3/mutant_*
11+
storm/fse_repl/bug4/mutant_*
12+
storm/fse_repl/bug5/mutant_*
13+
storm/fse_repl/bug6/mutant_*
14+
storm/fse_repl/bug7/mutant_*
15+
storm/fse_repl/bug8/mutant_*
16+
storm/fse_repl/bug9/mutant_*
17+
storm/fse_repl/bug10/mutant_*
18+
storm/fse_repl/bug11/mutant_*
19+
storm/fse_repl/bug12/mutant_*
20+
storm/fse_repl/bug13/mutant_*
21+
storm/fse_repl/bug14/mutant_*
22+
storm/fse_repl/bug15/mutant_*
23+
storm/fse_repl/bug16/mutant_*
24+
storm/fse_repl/bug17/mutant_*
25+
storm/fse_repl/bug18/mutant_*
26+
storm/fse_repl/bug19/mutant_*
27+
storm/fse_repl/bug20/mutant_*
28+
storm/fse_repl/bug21/mutant_*

README.md

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
![logo](https://user-images.githubusercontent.com/4897599/72667625-29075e00-3a1e-11ea-8179-776e9c4c938d.png)
2+
3+
![Python application](https://github.com/Practical-Formal-Methods/storm/workflows/Python%20application/badge.svg)
4+
![Python package](https://github.com/Practical-Formal-Methods/storm/workflows/Python%20package/badge.svg)
5+
6+
## Installation:
7+
```
8+
git clone https://github.com/Practical-Formal-Methods/storm
9+
virtualenv --python=/usr/bin/python3.7 venv
10+
source venv/bin/activate
11+
cd storm
12+
python setup.py install
13+
```
14+
15+
## Usage:
16+
17+
```
18+
storm --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME]
19+
```
20+
21+
To test the solver on a particular theory, use the `--theory` flag. For example:
22+
23+
```
24+
storm --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=LIA
25+
```
26+
27+
To run `n` parallel instances of storm on `n` cores, use the `--cores` flag. For example:
28+
29+
```
30+
storm --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=LIA --cores=10
31+
```
32+
33+
To obtain a smaller SMT instance that revealed a refutational soundness bug in an SMT solver, use:
34+
```
35+
storm --min --file_path=[PATH TO SMT INSTANCE] --solver=[SOLVER NAME] --solverbin=[PATH TO SOLVER BIN] --theory=[THEORY NAME]
36+
```
37+
If the SMT instance is in incremental mode, use `--incremental` flag.
38+
39+
40+
## Soundness bugs detected so far:
41+
STORM has detected many unique and previously unknown "refutational soundness" bugs in
42+
multiple mature SMT solvers. Here is a list of issues we filed on public bug tracking systems
43+
for various SMT solvers.
44+
45+
https://github.com/SRI-CSL/yices2/issues/150 `[yices]` `[QF_UFIDL]` <br>
46+
https://github.com/SRI-CSL/yices2/issues/160 `[yices]` `[QF_UFLRA]` <br>
47+
https://github.com/SRI-CSL/yices2/issues/167 `[yices]` `[QF_UF]` <br>
48+
https://github.com/Z3Prover/z3/issues/2758 `[z3]` `[QF_S]` <br>
49+
https://github.com/Z3Prover/z3/issues/3067 `[z3str3]` `[QF_S]` <br>
50+
https://github.com/levnach/z3/issues/115 `[z3]` `[QF_NIA]` <br>
51+
https://github.com/levnach/z3/issues/116 `[z3]` `[QF_NRA]` <br>
52+
https://github.com/Z3Prover/z3/issues/2828 `[z3]` `[QF_S]` <br>
53+
https://github.com/Z3Prover/z3/issues/2871 `[z3]` `[QF_LIA]` <br>
54+
https://github.com/SRI-CSL/yices2/issues/170 `[yices]` `[QF_NRA]` <br>
55+
https://github.com/Z3Prover/z3/issues/2829 `[z3]` `[QF_LIA]` <br>
56+
https://github.com/Z3Prover/z3/issues/2835 `[z3]` `[QF_UFLIA]` <br>
57+
https://github.com/Z3Prover/z3/issues/2873 `[z3]` `[QF_BV]` <br>
58+
https://github.com/Z3Prover/z3/issues/2993 `[z3]` `[QF_S]` <br>
59+
https://github.com/levnach/z3/issues/114 `[z3]` `[AUFNIRA]` <br>
60+
https://github.com/Z3Prover/z3/issues/3052 `[z3]` `[LIA]` <br>
61+
https://github.com/Z3Prover/z3/issues/3058 `[z3]` `[QF_BVFP]` <br>
62+
https://github.com/Z3Prover/z3/issues/3068 `[z3]` `[UF]` <br>
63+
https://github.com/SRI-CSL/yices2/issues/169 `[yices]` `[QF_UFIDL]` <br>
64+
https://github.com/SRI-CSL/yices2/issues/170 `[yices]` `[QF_NRA]` <br>
65+
https://github.com/Z3Prover/z3/issues/2994 `[z3str3]` `[QF_S]` <br>
66+
https://github.com/Z3Prover/z3/issues/3031 `[z3str3]` `[QF_S]` <br>
67+
https://github.com/Z3Prover/z3/issues/2916 `[z3]` `[QF_S]` <br>
68+
https://github.com/Z3Prover/z3/issues/2925 `[z3]` `[QF_FP]` <br>
69+
https://github.com/Z3Prover/z3/issues/3040 `[z3]` `[QF_BV]` <br>
70+
https://github.com/Z3Prover/z3/issues/3096 `[z3]` `[QF_NIA]` <br>
71+
https://github.com/Z3Prover/z3/issues/3256 `[z3]` `[AUFNIRA]` <br>
72+
https://github.com/Z3Prover/z3/issues/3822 `[z3]` `[BV]` <br>
73+
https://github.com/Z3Prover/z3/issues/3948 `[z3]` `[AUFDTLIA]` <br>
74+
https://github.com/Z3Prover/z3/issues/3949 `[z3]` `[QF_UFLRA]` <br>
75+
https://github.com/Z3Prover/z3/issues/4590 `[z3str3]` `[QF_S]` <br>
76+
https://github.com/SRI-CSL/yices2/issues/280 `[yices]` `[QF_NRA]`
77+
78+
## Reproducing bugs used in the evaluation section of our ESEC/FSE 2020 paper:
79+
Please follow the instructions
80+
[here](https://github.com/Practical-Formal-Methods/storm/tree/master/storm/fse_repl).

docs/Gemfile

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
# frozen_string_literal: true
2+
3+
source 'https://rubygems.org'
4+
5+
gemspec

docs/LICENSE

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
CC0 1.0 Universal
2+
3+
Statement of Purpose
4+
5+
The laws of most jurisdictions throughout the world automatically confer
6+
exclusive Copyright and Related Rights (defined below) upon the creator and
7+
subsequent owner(s) (each and all, an "owner") of an original work of
8+
authorship and/or a database (each, a "Work").
9+
10+
Certain owners wish to permanently relinquish those rights to a Work for the
11+
purpose of contributing to a commons of creative, cultural and scientific
12+
works ("Commons") that the public can reliably and without fear of later
13+
claims of infringement build upon, modify, incorporate in other works, reuse
14+
and redistribute as freely as possible in any form whatsoever and for any
15+
purposes, including without limitation commercial purposes. These owners may
16+
contribute to the Commons to promote the ideal of a free culture and the
17+
further production of creative, cultural and scientific works, or to gain
18+
reputation or greater distribution for their Work in part through the use and
19+
efforts of others.
20+
21+
For these and/or other purposes and motivations, and without any expectation
22+
of additional consideration or compensation, the person associating CC0 with a
23+
Work (the "Affirmer"), to the extent that he or she is an owner of Copyright
24+
and Related Rights in the Work, voluntarily elects to apply CC0 to the Work
25+
and publicly distribute the Work under its terms, with knowledge of his or her
26+
Copyright and Related Rights in the Work and the meaning and intended legal
27+
effect of CC0 on those rights.
28+
29+
1. Copyright and Related Rights. A Work made available under CC0 may be
30+
protected by copyright and related or neighboring rights ("Copyright and
31+
Related Rights"). Copyright and Related Rights include, but are not limited
32+
to, the following:
33+
34+
i. the right to reproduce, adapt, distribute, perform, display, communicate,
35+
and translate a Work;
36+
37+
ii. moral rights retained by the original author(s) and/or performer(s);
38+
39+
iii. publicity and privacy rights pertaining to a person's image or likeness
40+
depicted in a Work;
41+
42+
iv. rights protecting against unfair competition in regards to a Work,
43+
subject to the limitations in paragraph 4(a), below;
44+
45+
v. rights protecting the extraction, dissemination, use and reuse of data in
46+
a Work;
47+
48+
vi. database rights (such as those arising under Directive 96/9/EC of the
49+
European Parliament and of the Council of 11 March 1996 on the legal
50+
protection of databases, and under any national implementation thereof,
51+
including any amended or successor version of such directive); and
52+
53+
vii. other similar, equivalent or corresponding rights throughout the world
54+
based on applicable law or treaty, and any national implementations thereof.
55+
56+
2. Waiver. To the greatest extent permitted by, but not in contravention of,
57+
applicable law, Affirmer hereby overtly, fully, permanently, irrevocably and
58+
unconditionally waives, abandons, and surrenders all of Affirmer's Copyright
59+
and Related Rights and associated claims and causes of action, whether now
60+
known or unknown (including existing as well as future claims and causes of
61+
action), in the Work (i) in all territories worldwide, (ii) for the maximum
62+
duration provided by applicable law or treaty (including future time
63+
extensions), (iii) in any current or future medium and for any number of
64+
copies, and (iv) for any purpose whatsoever, including without limitation
65+
commercial, advertising or promotional purposes (the "Waiver"). Affirmer makes
66+
the Waiver for the benefit of each member of the public at large and to the
67+
detriment of Affirmer's heirs and successors, fully intending that such Waiver
68+
shall not be subject to revocation, rescission, cancellation, termination, or
69+
any other legal or equitable action to disrupt the quiet enjoyment of the Work
70+
by the public as contemplated by Affirmer's express Statement of Purpose.
71+
72+
3. Public License Fallback. Should any part of the Waiver for any reason be
73+
judged legally invalid or ineffective under applicable law, then the Waiver
74+
shall be preserved to the maximum extent permitted taking into account
75+
Affirmer's express Statement of Purpose. In addition, to the extent the Waiver
76+
is so judged Affirmer hereby grants to each affected person a royalty-free,
77+
non transferable, non sublicensable, non exclusive, irrevocable and
78+
unconditional license to exercise Affirmer's Copyright and Related Rights in
79+
the Work (i) in all territories worldwide, (ii) for the maximum duration
80+
provided by applicable law or treaty (including future time extensions), (iii)
81+
in any current or future medium and for any number of copies, and (iv) for any
82+
purpose whatsoever, including without limitation commercial, advertising or
83+
promotional purposes (the "License"). The License shall be deemed effective as
84+
of the date CC0 was applied by Affirmer to the Work. Should any part of the
85+
License for any reason be judged legally invalid or ineffective under
86+
applicable law, such partial invalidity or ineffectiveness shall not
87+
invalidate the remainder of the License, and in such case Affirmer hereby
88+
affirms that he or she will not (i) exercise any of his or her remaining
89+
Copyright and Related Rights in the Work or (ii) assert any associated claims
90+
and causes of action with respect to the Work, in either case contrary to
91+
Affirmer's express Statement of Purpose.
92+
93+
4. Limitations and Disclaimers.
94+
95+
a. No trademark or patent rights held by Affirmer are waived, abandoned,
96+
surrendered, licensed or otherwise affected by this document.
97+
98+
b. Affirmer offers the Work as-is and makes no representations or warranties
99+
of any kind concerning the Work, express, implied, statutory or otherwise,
100+
including without limitation warranties of title, merchantability, fitness
101+
for a particular purpose, non infringement, or the absence of latent or
102+
other defects, accuracy, or the present or absence of errors, whether or not
103+
discoverable, all to the greatest extent permissible under applicable law.
104+
105+
c. Affirmer disclaims responsibility for clearing rights of other persons
106+
that may apply to the Work or any use thereof, including without limitation
107+
any person's Copyright and Related Rights in the Work. Further, Affirmer
108+
disclaims responsibility for obtaining any necessary consents, permissions
109+
or other rights required for any use of the Work.
110+
111+
d. Affirmer understands and acknowledges that Creative Commons is not a
112+
party to this document and has no duty or obligation with respect to this
113+
CC0 or use of the Work.
114+
115+
For more information, please see
116+
<http://creativecommons.org/publicdomain/zero/1.0/>

0 commit comments

Comments
 (0)