Rollup merge of #146740 - RalfJung:miri, r=RalfJung

miri subtree update

Subtree update of `miri` to 5a14200.

Created using https://github.com/rust-lang/josh-sync.

r? ``@ghost``

Author: Zalathar

.github/workflows/ci.yml

@@ -31,21 +31,22 @@ jobs:
             os: ubuntu-24.04-arm
             multiarch: armhf
             gcc_cross: arm-linux-gnueabihf
-          - host_target: riscv64gc-unknown-linux-gnu
-            os: ubuntu-latest
-            multiarch: riscv64
-            gcc_cross: riscv64-linux-gnu
-            qemu: true
-          - host_target: s390x-unknown-linux-gnu
-            os: ubuntu-latest
-            multiarch: s390x
-            gcc_cross: s390x-linux-gnu
-            qemu: true
-          - host_target: powerpc64le-unknown-linux-gnu
-            os: ubuntu-latest
-            multiarch: ppc64el
-            gcc_cross: powerpc64le-linux-gnu
-            qemu: true
+          # Disabled due to Ubuntu repo trouble
+          # - host_target: riscv64gc-unknown-linux-gnu
+          #   os: ubuntu-latest
+          #   multiarch: riscv64
+          #   gcc_cross: riscv64-linux-gnu
+          #   qemu: true
+          # - host_target: s390x-unknown-linux-gnu
+          #   os: ubuntu-latest
+          #   multiarch: s390x
+          #   gcc_cross: s390x-linux-gnu
+          #   qemu: true
+          # - host_target: powerpc64le-unknown-linux-gnu
+          #   os: ubuntu-latest
+          #   multiarch: ppc64el
+          #   gcc_cross: powerpc64le-linux-gnu
+          #   qemu: true
           - host_target: aarch64-apple-darwin
             os: macos-latest
           - host_target: i686-pc-windows-msvc
@@ -67,7 +68,7 @@ jobs:
       - name: install multiarch
         if: ${{ matrix.multiarch != '' }}
         run: |
-          # s390x, ppc64el need Ubuntu Ports to be in the mirror list
+          # s390x, ppc64el, riscv64 need Ubuntu Ports to be in the mirror list
           sudo bash -c "echo 'https://ports.ubuntu.com/	priority:4' >> /etc/apt/apt-mirrors.txt"
           # Add architecture
           sudo dpkg --add-architecture ${{ matrix.multiarch }}

Cargo.lock

@@ -70,7 +70,7 @@ harness = false
 
 [features]
 default = ["stack-cache", "native-lib"]
-genmc = ["dep:genmc-sys"] # this enables a GPL dependency!
+genmc = ["dep:genmc-sys"]
 stack-cache = []
 stack-cache-consistency-check = ["stack-cache"]
 tracing = ["serde_json"]

Cargo.toml

@@ -220,7 +220,7 @@ degree documented below):
   - `solaris` / `illumos`: maintained by @devnexen. Supports the entire test suite.
   - `freebsd`: maintained by @YohDeadfall and @LorrensP-2158466. Supports the entire test suite.
   - `android`: **maintainer wanted**. Support very incomplete, but a basic "hello world" works.
-  - `wasi`: **maintainer wanted**. Support very incomplete, not even standard output works, but an empty `main` function works.
+  - `wasi`: **maintainer wanted**. Support very incomplete, but a basic "hello world" works.
 - For targets on other operating systems, Miri might fail before even reaching the `main` function.
 
 However, even for targets that we do support, the degree of support for accessing platform APIs

README.md

@@ -137,6 +137,7 @@ function run_tests_minimal {
 
 # In particular, fully cover all tier 1 targets.
 # We also want to run the many-seeds tests on all tier 1 targets.
+# We run GC_STRESS only once for each tier 1 OS.
 case $HOST_TARGET in
   x86_64-unknown-linux-gnu)
     # Host
@@ -147,29 +148,31 @@ case $HOST_TARGET in
     ;;
   i686-unknown-linux-gnu)
     # Host
-    # Without GC_STRESS as this is a slow runner.
     MIR_OPT=1 MANY_SEEDS=64 TEST_BENCH=1 CARGO_MIRI_ENV=1 run_tests
     # Partially supported targets (tier 2)
     BASIC="empty_main integer heap_alloc libc-mem vec string btreemap" # ensures we have the basics: pre-main code, system allocator
     UNIX="hello panic/panic panic/unwind concurrency/simple atomic libc-mem libc-misc libc-random env num_cpus" # the things that are very similar across all Unixes, and hence easily supported there
     TEST_TARGET=aarch64-linux-android  run_tests_minimal $BASIC $UNIX time hashmap random thread sync concurrency epoll eventfd
-    TEST_TARGET=wasm32-wasip2          run_tests_minimal $BASIC wasm
+    TEST_TARGET=wasm32-wasip2          run_tests_minimal $BASIC hello wasm
     TEST_TARGET=wasm32-unknown-unknown run_tests_minimal no_std empty_main wasm # this target doesn't really have std
     TEST_TARGET=thumbv7em-none-eabihf  run_tests_minimal no_std
     ;;
   aarch64-unknown-linux-gnu)
     # Host
-    GC_STRESS=1 MIR_OPT=1 MANY_SEEDS=64 TEST_BENCH=1 CARGO_MIRI_ENV=1 run_tests
+    MIR_OPT=1 MANY_SEEDS=64 TEST_BENCH=1 CARGO_MIRI_ENV=1 run_tests
     # Extra tier 2
     MANY_SEEDS=16 TEST_TARGET=arm-unknown-linux-gnueabi run_tests # 32bit ARM
     MANY_SEEDS=16 TEST_TARGET=aarch64-pc-windows-gnullvm run_tests # gnullvm ABI
     MANY_SEEDS=16 TEST_TARGET=s390x-unknown-linux-gnu run_tests # big-endian architecture of choice
-    # Custom target JSON file
-    TEST_TARGET=tests/x86_64-unknown-kernel.json MIRI_NO_STD=1 run_tests_minimal no_std
+    # Not officially supported tier 2
+    MANY_SEEDS=16 TEST_TARGET=x86_64-unknown-freebsd run_tests
+    MANY_SEEDS=16 TEST_TARGET=i686-unknown-freebsd run_tests
     ;;
   armv7-unknown-linux-gnueabihf)
     # Host
-    GC_STRESS=1 MIR_OPT=1 MANY_SEEDS=64 TEST_BENCH=1 CARGO_MIRI_ENV=1 run_tests
+    MIR_OPT=1 MANY_SEEDS=64 TEST_BENCH=1 CARGO_MIRI_ENV=1 run_tests
+    # Custom target JSON file
+    TEST_TARGET=tests/x86_64-unknown-kernel.json MIRI_NO_STD=1 run_tests_minimal no_std
     ;;
   aarch64-apple-darwin)
     # Host
@@ -181,12 +184,9 @@ case $HOST_TARGET in
     MANY_SEEDS=16 TEST_TARGET=mips-unknown-linux-gnu run_tests # a 32bit big-endian target, and also a target without 64bit atomics
     MANY_SEEDS=16 TEST_TARGET=x86_64-unknown-illumos run_tests
     MANY_SEEDS=16 TEST_TARGET=x86_64-pc-solaris run_tests
-    MANY_SEEDS=16 TEST_TARGET=x86_64-unknown-freebsd run_tests
-    MANY_SEEDS=16 TEST_TARGET=i686-unknown-freebsd run_tests
     ;;
   i686-pc-windows-msvc)
     # Host
-    # Without GC_STRESS as this is a very slow runner.
     MIR_OPT=1 MANY_SEEDS=64 TEST_BENCH=1 run_tests
     # Extra tier 1
     # We really want to ensure a Linux target works on a Windows host,
@@ -195,8 +195,7 @@ case $HOST_TARGET in
     ;;
   aarch64-pc-windows-msvc)
     # Host
-    # Without GC_STRESS as this is a very slow runner.
-    MIR_OPT=1 MANY_SEEDS=64 TEST_BENCH=1 CARGO_MIRI_ENV=1 run_tests
+    GC_STRESS=1 MIR_OPT=1 MANY_SEEDS=64 TEST_BENCH=1 CARGO_MIRI_ENV=1 run_tests
     # Extra tier 1
     MANY_SEEDS=64 TEST_TARGET=i686-unknown-linux-gnu run_tests
     ;;

ci/ci.sh

@@ -9,9 +9,7 @@ Miri-GenMC integrates that model checker into Miri.
 
 ## Usage
 
-**IMPORTANT: The license of GenMC and thus the `genmc-sys` crate in the Miri repo is currently "GPL-3.0-or-later", so a binary produced with the `genmc` feature is subject to the requirements of the GPL. As long as that remains the case, the `genmc` feature of Miri is OFF-BY-DEFAULT and must be OFF for all Miri releases.**
-
-For testing/developing Miri-GenMC (while keeping in mind the licensing issues):
+For testing/developing Miri-GenMC:
 - clone the Miri repo.
 - build Miri-GenMC with `./miri build --features=genmc`.
 - OR: install Miri-GenMC in the current system with `./miri install --features=genmc`
@@ -21,7 +19,30 @@ Basic usage:
 MIRIFLAGS="-Zmiri-genmc" cargo miri run
 ```
 
-<!-- FIXME(genmc): explain options. -->
+Note that `cargo miri test` in GenMC mode is currently not supported.
+
+### Supported Parameters
+
+- `-Zmiri-genmc`: Enable GenMC mode (not required if any other GenMC options are used).
+- `-Zmiri-genmc-estimate`: This enables estimation of the concurrent execution space and verification time, before running the full verification. This should help users detect when their program is too complex to fully verify in a reasonable time. This will explore enough executions to make a good estimation, but at least 10 and at most `estimation-max` executions.
+- `-Zmiri-genmc-estimation-max={MAX_ITERATIONS}`: Set the maximum number of executions that will be explored during estimation (default: 1000).
+- `-Zmiri-genmc-print-exec-graphs={none,explored,blocked,all}`: Make GenMC print the execution graph of the program after every explored, every blocked, or after every execution (default: None).
+- `-Zmiri-genmc-print-exec-graphs`: Shorthand for suffix `=explored`.
+- `-Zmiri-genmc-print-genmc-output`: Print the output that GenMC provides. NOTE: this output is quite verbose and the events in the printed execution graph are hard to map back to the Rust code location they originate from.
+- `-Zmiri-genmc-log=LOG_LEVEL`: Change the log level for GenMC. Default: `warning`.
+  - `quiet`:    Disable logging.
+  - `error`:    Print errors.
+  - `warning`:  Print errors and warnings.
+  - `tip`:      Print errors, warnings and tips.
+  - If Miri is built with debug assertions, there are additional log levels available (downgraded to `tip` without debug assertions):
+    - `debug1`:   Print revisits considered by GenMC.
+    - `debug2`:   Print the execution graph after every memory access.
+    - `debug3`:   Print reads-from values considered by GenMC.
+- `-Zmiri-genmc-verbose`: Show more information, such as estimated number of executions, and time taken for verification.
+
+#### Regular Miri parameters useful for GenMC mode
+
+- `-Zmiri-disable-weak-memory-emulation`: Disable any weak memory effects (effectively upgrading all atomic orderings in the program to `SeqCst`). This option may reduce the number of explored program executions, but any bugs related to weak memory effects will be missed. This option can help determine if an error is caused by weak memory effects (i.e., if it disappears with this option enabled).
 
 <!-- FIXME(genmc): explain Miri-GenMC specific functions. -->
 
@@ -57,6 +78,15 @@ The process for obtaining them is as follows:
   If you place this directory inside the Miri folder, it is recommended to call it `genmc-src` as that tells `./miri fmt` to avoid
   formatting the Rust files inside that folder.
 
+### Formatting the C++ code
+
+For formatting the C++ code we provide a `.clang-format` file in the `genmc-sys` directory.
+With `clang-format` installed, run this command to format the c++ files (replace the `-i` with `--dry-run` to just see the changes.):
+```
+find ./genmc-sys/cpp/ -name "*.cpp" -o -name "*.hpp" | xargs clang-format --style=file:"./genmc-sys/.clang-format" -i
+```
+NOTE: this is currently not done automatically on pull requests to Miri.
+
 <!-- FIXME(genmc): explain how submitting code to GenMC should be handled. -->
 
 <!-- FIXME(genmc): explain development. -->

doc/genmc.md

@@ -0,0 +1,52 @@
+# .clang-format
+
+BasedOnStyle: LLVM
+Standard: c++20
+
+ColumnLimit: 100
+AllowShortFunctionsOnASingleLine: Empty
+AllowShortIfStatementsOnASingleLine: false
+AllowShortLoopsOnASingleLine: false
+AllowShortBlocksOnASingleLine: Empty
+BreakBeforeBraces: Attach
+
+BinPackArguments: false
+BinPackParameters: false
+AllowAllParametersOfDeclarationOnNextLine: false
+AlwaysBreakAfterReturnType: None
+
+# Force parameters to break and align
+AlignAfterOpenBracket: BlockIndent
+AllowAllArgumentsOnNextLine: false
+
+# Spacing around braces and parentheses
+SpaceBeforeCtorInitializerColon: true
+SpaceBeforeInheritanceColon: true
+SpaceInEmptyBlock: false
+SpacesInContainerLiterals: true
+SpacesInParensOptions:
+  InCStyleCasts: false
+  InConditionalStatements: false
+  InEmptyParentheses: false
+  Other: false
+SpacesInSquareBrackets: false
+
+# Brace spacing for initializers
+Cpp11BracedListStyle: false
+SpaceBeforeCpp11BracedList: true
+
+# Import grouping: group standard, external, and project includes.
+IncludeBlocks: Regroup
+SortIncludes: true
+
+# Granularity: sort includes per module/file.
+IncludeIsMainRegex: '([-_](test|unittest))?$'
+
+# Miscellaneous
+SpaceAfterCStyleCast: true
+SpaceBeforeParens: ControlStatements
+PointerAlignment: Left
+IndentCaseLabels: true
+IndentWidth: 4
+TabWidth: 4
+UseTab: Never

genmc-sys/.clang-format

@@ -1,17 +1,15 @@
 [package]
 authors = ["Miri Team"]
-# The parts in this repo are MIT OR Apache-2.0, but we are linking in
-# code from https://github.com/MPI-SWS/genmc which is GPL-3.0-or-later.
-license = "(MIT OR Apache-2.0) AND GPL-3.0-or-later"
+license = "MIT OR Apache-2.0"
 name = "genmc-sys"
 version = "0.1.0"
 edition = "2024"
 
 [dependencies]
-cxx = { version = "1.0.160", features = ["c++20"] }
+cxx = { version = "1.0.173", features = ["c++20"] }
 
 [build-dependencies]
 cc = "1.2.16"
 cmake = "0.1.54"
 git2 = { version = "0.20.2", default-features = false, features = ["https"] }
-cxx-build = { version = "1.0.160", features = ["parallel"] }
+cxx-build = { version = "1.0.173", features = ["parallel"] }