A collection of techniques for scrutinising SPIR-V control flow rules, their validation, and whether they are implemented correctly.
📦 main
├─ .gitignore
├─ .gitmodules
├─ AUTHORS
├─ AlloyModel
│  └─ StructuredDominanceCFG.als
├─ CONTRIBUTORS
├─ LICENSE
├─ README.md
├─ fleshing
│  ├─ .gitignore
│  ├─ README.md
│  ├─ amber_result.py
│  ├─ amber_runner.py
│  ├─ amber_utils.py
│  ├─ copy-libs.sh
│  ├─ cross_compilation.py
│  ├─ examples
│  │  ├─ simple-fleshed.amber
│  │  ├─ simple.asm
│  │  └─ simple.pdf
│  ├─ fleshing_runner.py
│  ├─ fleshout.py
│  ├─ run_amber_on_android.py
│  ├─ test.py
│  ├─ test_0.png
│  ├─ test_0.xml
│  └─ use_mesa.sh
├─ isCFGdeemedFeasible.py
└─ spirv-to-alloy
   ├─ CMakeLists.txt
   ├─ convert_asm_directory.py
   ├─ scrape-vulkan-cts.py
   ├─ src
   │  └─ spirv_to_alloy
   │     ├─ CMakeLists.txt
   │     └─ src
   │        └─ main.cc
   └─ third_party
      ├─ SPIRV-Headers
      └─ SPIRV-Tools
         ├─ CMakeLists.txt
         └─ SPIRV-Tools
These instructions will guide you through getting a set of tools underway for checking whether a given control flow graph is deemed feasible.
This tool turns the control flow graph of a SPIR-V function into a form ready for analysis with Alloy. This can be useful to check whether the control flow graph is deemed feasible.
After cloning the repo, enter the repo directory and do the following:
# Update and init submodules.
git submodule update --init
# Build using a recent version of CMake. Ensure `ninja` is on your PATH.
mkdir spirv-to-alloy/build
cd spirv-to-alloy/build
cmake -G Ninja .. -DCMAKE_BUILD_TYPE=Debug
cmake --build . --config DebugFrom the build directory, the tool executable will then be ./src/spirv_to_alloy/spirv-to-alloy
To run the tool, do:
/path/to/spirv-to-alloy <spirv-binary> <function-id> <alloy module name>where <spirv-binary> is a SPIR-V binary file, <function-id> is
the id of some function in that file whose control flow graph you are
interested in, and <alloy module name> is the name of an Alloy module
that you would like to appear in the output.
Our model relies on the Alloy language.
To analyse an alloy module generated by the spirv-to-alloy tool (for e.g., XXX.als below), run the Alloy GUI Analyzer, open the model, add the content of XXX.als in the editor panel and run it under the Execute menu option.
pred XXX {
some disj b1, b2, b3, b4, b5, b6, b7, b8, b9, b10 : BLOCK {
EntryPoint = b1
HeaderBlock = b1 + b4 + b6
LoopHeader = b4 + b6
SwitchBlock = none
jump = (b1 -> ((0 -> b2) + (1 -> b3)))
+ (b3 -> (0 -> b4))
+ (b4 -> (0 -> b5))
+ (b5 -> (0 -> b6))
+ (b6 -> (0 -> b7))
+ (b8 -> (0 -> b6))
+ (b9 -> (0 -> b4))
merge = (b1 -> b3)
+ (b4 -> b10)
+ (b6 -> b9)
continue = (b4 -> b9)
+ (b6 -> b8)
}
}
run { XXX && Valid } for 10 BLOCKYou may want to run Alloy from command-line in which case the Alloy* should be installed.
For example, to check the above graph (if on macOS) run the following from the command line:
java -classpath /path/to/alloystar -Xmx3g -Djava.library.path=/path/to/alloystar/x86-mac -Dout=/path/to/traces -Dquiet=false -Dsolver=minisat -Dhigherorder=true -Dcmd=0 -Diter=true edu/mit/csail/sdg/alloy4whole/RunAlloy /path/to/XXX.als
If on Linux or Windows, change the library path accordingly. For more details on the command-line parameters, see here: Java Tool Doc.
Download the latest release of SPIR-V Tools from here
and unpack it somewhere. Note the absolute paths to the spirv-as and spirv-dis tools.
glslangValidator is the tool used to compile GLSL and HLSL shaders into SPIR-V Vulkan's shader format.
To build and install glslang, do the following:
git clone https://github.com/KhronosGroup/glslang.git
mkdir -p build
cd build
cmake -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX="$(pwd)/install" </absolute/path/to/glslang>
make -j4 install
Note the absolute path to the glslangValidator tool.
Check out the Vulkan and OpenGL CTS somewhere:
cd /somewhere/sensible/
git clone git@github.com:KhronosGroup/VK-GL-CTS.git
Navigate to the root of the spirv-control-flow repo. Then do:
mkdir VulkanCTS
./spirv-to-alloy/scrape-vulkan-cts.py VulkanCTS /path/to/VK-GL-CTS /path/to/glslangValidator /path/to/spirv-as /path/to/spirv-dis /path/to/spirv-to-alloy
where /path/to/VK-GL-CTS is the path to the VK-GL-CTS repo checked out above; the other arguments are the path to glslangValidator (from the version that you built and installed), the paths to the spirv-as and spirv-dis tools (from the release you downloaded), and the path to the spirv-to-alloy tool that you built.
NOTE: (1) Make sure the file is executable:
chmod +x scrape-vulkan-cts.py(2) The script will run with the default python interpreter. Should you use some specific Python version just specify it in the shebang line to let the kernel know what interpreter to use, e.g.,#!/usr/bin/env python3.9
If this command succeeded, you should see many .als files under VulkanCTS.
The tool isCFGdeemedFeasible.py checks (in batch mode) whether the tests from the Khronos Vulkan Conformance Testing Suite (generated by the spirv-to-alloy tool) are deemed valid by the Alloy model.
Each .als module contains an “open” statement which imports the Alloy model signature into this module spec. Both the .als module and the Alloy model should be at the same level in repo hierarchy: if all the steps are performed correctly, then the contents of VulkanCTS and AlloyModel folders are already at the same level.
For all the tests deemed valid by the Alloy model, the script will generate the corresponding xml file. In addition, the generated out.csv will store tabular data about each test.
This is a fragment example of out.csv viewed as spread sheet:
| CFG | Blocks | HeaderBlocks | LoopHeaders | SelectionHeaders | SwitchBlocks | Jumps | ExitBlocks | CyclomaticComplexity | TranslationTime | SolvingTime | Vars | PrimaryVars | Clauses | Feasible |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| s000 | 1 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 0.11 | 0.03 | 291 | 13 | 590 | TRUE |
| s059 | 4 | 1 | 0 | 1 | 0 | 2 | 3 | 4 | 0.31 | 0.03 | 13517 | 136 | 41556 | TRUE |
| s008 | 3 | 1 | 0 | 1 | 0 | 2 | 2 | 3 | 0.21 | 0.03 | 6261 | 81 | 18975 | TRUE |
usage: isCFGdeemedFeasible.py [-h] -a PATH_TO_ALLOY_FILES -x PATH_TO_XML_OUTPUT_FOLDER -c PATH_TO_ALLOYSTAR
[-m MEMORY]
[-s {sat4j,cryptominisat,glucose,plingeling,lingeling,minisatprover,minisat}]
required arguments:
-a PATH_TO_ALLOY_FILES, --path_to_alloy_Files PATH_TO_ALLOY_FILES
The path to the Vulkan CTS .als files folder
-x PATH_TO_XML_OUTPUT_FOLDER, --path_to_XML_Output_Folder PATH_TO_XML_OUTPUT_FOLDER
The path to the generated instance XML files
-c PATH_TO_ALLOYSTAR, --path_to_AlloyStar PATH_TO_ALLOYSTAR
The Alloy* (https://github.com/johnwickerson/alloystar) packs the RunAlloy tool which allows
Alloy run from the command line
optional arguments:
-h, --help show this help message and exit
-m MEMORY, --memory MEMORY
Maximum memory in [GB]
-s {sat4j,cryptominisat,glucose,plingeling,lingeling,minisatprover,minisat}, --solver {sat4j,cryptominisat,glucose,plingeling,lingeling,minisatprover,minisat}
Constraint/SAT Solver: By default, the pure Java solver "SAT4J" is chosen since it runs on
every platform and operating system. If you require faster performance, you can try one of
the native solver such as MiniSat or ZChaff.
Pull requests are welcome. For major changes, please open an issue first to discuss what you would like to change. Please read CONTRIBUTORS for more details.
See the LICENSE file for details.
- A complete registry of all official SPIR-V specifications. The Khronos Group Inc. 2021. Available at: https://www.khronos.org/registry/SPIR-V/
- Software Abstractions: Logic, Language, and Analysis. By Daniel Jackson, The MIT Press, 2006, 366pp, ISBN 978-0262101141.