Slowbeast with concurrency

• Python SAST checker to detect possible data races in multi-threaded C programs.Uses Partial order reduction in Symbolic execution. Mgr. thesis project by Suyash Shandilya.

• Originally created by Marek Chalupa at FORMELA, Faculty of Informatics, Masaryk University, as a playground for symbolic execution, this fork extends support for multi-threaded C programs. Currently a work in progress, it focuses on data race detection, with additional properties like reachability analysis and overflow detection expected to follow soon. 🙂

Recently moved to devcontainer. To get started it should just be to clone and open a devcontainer in vscode. Don't follow the steps below. the get-started.sh script is likely moot now.

---

Get Started (UNUPDATED DON'T FOLLOW)

• Run the ./get-started.sh script. It builds the docker container and runs a container with the current directory mounted.

How to use:

• Running the ./get-started.sh creates a bash terminal inside the docker container (tagged: slowbeastnodatarace:latest). This is considered the default mode of operation.
• The sb-main is the main entrypoint of all the analysis. Simple sb-main <input-file> should default to using the right parameters. The line Data Race Found: False is the main value to be read. It will be printed regardless of the completion of analysis so the final result is only valid if there are no KILLED paths.
  • Line 500/501 has_threads variable set to True to force the interpreter to be the current intended one.
• TDD Friendly project. Refer to the testing doc to get started.

Requirements

• While docker is not mandatory, it is recommended for convenience.
• Refer the Docker image file (Dockerfile) and the install-llvmlite.sh script for replicating a local build. The latter is the script run as soon as the image is built and the current drive is mounted.