Skip to main content

A Python re-implementation of the proven-correct symbolic executor WiSE

Project description

PyWiSE: A Python Twin of the Verified Symbolic Bug Finder WiSE

PyWiSE is a re-implementation of the (verified) Coq version of WiSE in Python. It features a command-line interface and parser to symbolically execute IMP programs. All code, with the exception of the parser and CLI code, closely mirror the Coq implementation. To demonstrate this, the original Coq code is provided as inline-comments close to the code mirroring it.

The relevant files are:

  • streams.py, mirroring streams.v—a small library for infinite streams.
  • imp.py, mirroring imp.v—the IMP programming language.
  • symex.py, mirroring symex.v—symbolic evaluation of expressions.
  • bugfinder.py, mirroring bugfinder.v—the implementation of the bug finder.

Macros

For convenience, PyWiSE supports simple macro definitions which are inlined in the IMP program. Macros must be defined at the beginning of an IMP file and are not separated by semicolons either from each other or the remaining program. They can call other macros defined before (which implies that they cannot be (mutually) recursive). An example program using a macro is:

macro subadd1(x, y)
begin
  x = x - y;
  x = x + 1
end
subadd1(a, b);
x = 17 

which expands to

a = a - b;
a = a + a;
x = 17

Note that macro "calls" are "statements," so you cannot invoke a macro inside an expression.

Installation

PyWiSE project requires Python 3.10 or higher. It is on PyPi; a simple pip install wise-se suffices to install the symbolic executor in the current Python environment.

If you want to build the project locally, we recommend using a virtual environment:

cd /path/to/PyWiSE
python3.10 -m venv venv
source venv/bin/activate
pip install .[dev,test]

Either way, the wise command should now be available on your command line. You can test it on the examples in the examples/ directory, e.g.:

$ wise examples/gcd_buggy.imp
Analyzing file examples/gcd_buggy.imp

BUG FOUND
  Path:          a <= 0
  Example Input: a := 0
  Store:         {}
BUG FOUND
  Path:          not (a <= 0) and b <= 0
  Example Input: a := 1, b := 0
  Store:         {}
BUG FOUND
  Path:          not (a <= 0) and not (b <= 0) and not (a == b) and not (a <= b) and not (0 <= (a + b) and 0 <= b and b <= 0 and not (b == 0))
  Example Input: a := 2, b := 1
  Store:         {}{old_a -> a}{old_b -> b}{a -> (a + b)}
...

The first two bugs are failing assertions on the input; the third one is a "real" bug. For some examples, you might have to increase the number of generated symbolic states, as in wise -n 100 ....

Enter wise -h for a short help text on the available options.

Copyright and License

Copyright © 2023 Arthur Correnson and Dominic Steinhöfel.

PyWiSE is released under the GNU General Public License v3.0 (see COPYING).

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

wise-se-0.0.7.tar.gz (60.1 kB view details)

Uploaded Source

Built Distribution

wise_se-0.0.7-py3-none-any.whl (46.3 kB view details)

Uploaded Python 3

File details

Details for the file wise-se-0.0.7.tar.gz.

File metadata

  • Download URL: wise-se-0.0.7.tar.gz
  • Upload date:
  • Size: 60.1 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/4.0.2 CPython/3.11.4

File hashes

Hashes for wise-se-0.0.7.tar.gz
Algorithm Hash digest
SHA256 69abcb15d901a279230987e39f2743a9577aff84d584aac56214572077c4f6d4
MD5 7a40108b465dd93fc7d3e9f4798fdfef
BLAKE2b-256 381a1e294fb0f41186c4467bc583cdf03c776f6073960eef72fcd917ed7f6a48

See more details on using hashes here.

File details

Details for the file wise_se-0.0.7-py3-none-any.whl.

File metadata

  • Download URL: wise_se-0.0.7-py3-none-any.whl
  • Upload date:
  • Size: 46.3 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/4.0.2 CPython/3.11.4

File hashes

Hashes for wise_se-0.0.7-py3-none-any.whl
Algorithm Hash digest
SHA256 bfb7a34f51410d37dca6dd4e47e5799abfccca7f59ce8f944d18bcfe7e6ee1bc
MD5 26593c678ea3136c2e7ac7bfe2569dc0
BLAKE2b-256 02e02b08ee525801520e49a98c950e18942589e55d19f5c9a372ce7d3e400763

See more details on using hashes here.

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page