Merge branch 'model-checking:main' into check_align_to

Author: AlexLB99

.github/workflows/flux.yml

@@ -9,7 +9,7 @@ on:
 
 env:
   FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
-  FLUX_VERSION: "844e2fc0caa6aa96d72f2fcb627a27bf2495d82e"
+  FLUX_VERSION: "f6bdf90c54ad6eed51b25c125f251cac01cfe170"
 
 jobs:
   check-flux-on-core:

library/compiler-builtins/.github/workflows/main.yaml

@@ -195,6 +195,25 @@ jobs:
       run: ./ci/update-musl.sh
     - run: cargo clippy --workspace --all-targets
 
+  build-custom:
+    name: Build custom target
+    runs-on: ubuntu-24.04
+    timeout-minutes: 10
+    steps:
+    - uses: actions/checkout@v4
+    - name: Install Rust
+      run: |
+        rustup update nightly --no-self-update
+        rustup default nightly
+        rustup component add rust-src
+    - uses: Swatinem/rust-cache@v2
+    - run: |
+        # Ensure we can build with custom target.json files (these can interact
+        # poorly with build scripts)
+        cargo build -p compiler_builtins -p libm \
+          --target etc/thumbv7em-none-eabi-renamed.json \
+          -Zbuild-std=core
+
   benchmarks:
     name: Benchmarks
     timeout-minutes: 20
@@ -331,6 +350,7 @@ jobs:
   success:
     needs:
       - benchmarks
+      - build-custom
       - clippy
       - extensive
       - miri

library/compiler-builtins/builtins-test-intrinsics/build.rs

@@ -6,6 +6,5 @@ fn main() {
     println!("cargo::rerun-if-changed=../configure.rs");
 
     let target = builtins_configure::Target::from_env();
-    builtins_configure::configure_f16_f128(&target);
     builtins_configure::configure_aliases(&target);
 }

library/compiler-builtins/builtins-test/benches/float_cmp.rs

@@ -177,6 +177,7 @@ float_bench! {
     ],
 }
 
+#[cfg(f128_enabled)]
 float_bench! {
     name: cmp_f128_gt,
     sig: (a: f128, b: f128) -> CmpResult,
@@ -189,6 +190,7 @@ float_bench! {
     asm: []
 }
 
+#[cfg(f128_enabled)]
 float_bench! {
     name: cmp_f128_unord,
     sig: (a: f128, b: f128) -> CmpResult,

library/compiler-builtins/builtins-test/build.rs

@@ -116,5 +116,4 @@ fn main() {
     }
 
     builtins_configure::configure_aliases(&target);
-    builtins_configure::configure_f16_f128(&target);
 }

library/compiler-builtins/builtins-test/tests/conv.rs

@@ -118,7 +118,7 @@ mod i_to_f {
         i128, __floattidf;
     }
 
-    #[cfg(not(feature = "no-f16-f128"))]
+    #[cfg(f128_enabled)]
     #[cfg(not(any(target_arch = "powerpc", target_arch = "powerpc64")))]
     i_to_f! { f128, Quad, not(feature = "no-sys-f128-int-convert"),
         u32, __floatunsitf;
@@ -129,7 +129,7 @@ mod i_to_f {
         i128, __floattitf;
     }
 
-    #[cfg(not(feature = "no-f16-f128"))]
+    #[cfg(f128_enabled)]
     #[cfg(any(target_arch = "powerpc", target_arch = "powerpc64"))]
     i_to_f! { f128, Quad, not(feature = "no-sys-f128-int-convert"),
         u32, __floatunsikf;

library/compiler-builtins/builtins-test/tests/div_rem.rs

@@ -147,7 +147,7 @@ mod float_div {
         f64, __divdf3, Double, all();
     }
 
-    #[cfg(not(feature = "no-f16-f128"))]
+    #[cfg(f128_enabled)]
     #[cfg(not(any(target_arch = "powerpc", target_arch = "powerpc64")))]
     float! {
         f128, __divtf3, Quad,
@@ -156,7 +156,7 @@ mod float_div {
         not(any(feature = "no-sys-f128", all(target_arch = "aarch64", target_os = "linux")));
     }
 
-    #[cfg(not(feature = "no-f16-f128"))]
+    #[cfg(f128_enabled)]
     #[cfg(any(target_arch = "powerpc", target_arch = "powerpc64"))]
     float! {
         f128, __divkf3, Quad, not(feature = "no-sys-f128");

library/compiler-builtins/ci/run.sh

@@ -54,29 +54,26 @@ symcheck=(cargo run -p symbol-check --release)
 [[ "$target" = "wasm"* ]] && symcheck+=(--features wasm)
 symcheck+=(-- build-and-check)
 
-"${symcheck[@]}" -p compiler_builtins --target "$target"
-"${symcheck[@]}" -p compiler_builtins --target "$target" --release
-"${symcheck[@]}" -p compiler_builtins --target "$target" --features c
-"${symcheck[@]}" -p compiler_builtins --target "$target" --features c --release
-"${symcheck[@]}" -p compiler_builtins --target "$target" --features no-asm
-"${symcheck[@]}" -p compiler_builtins --target "$target" --features no-asm --release
-"${symcheck[@]}" -p compiler_builtins --target "$target" --features no-f16-f128
-"${symcheck[@]}" -p compiler_builtins --target "$target" --features no-f16-f128 --release
+"${symcheck[@]}" "$target" -- -p compiler_builtins
+"${symcheck[@]}" "$target" -- -p compiler_builtins --release
+"${symcheck[@]}" "$target" -- -p compiler_builtins --features c
+"${symcheck[@]}" "$target" -- -p compiler_builtins --features c --release
+"${symcheck[@]}" "$target" -- -p compiler_builtins --features no-asm
+"${symcheck[@]}" "$target" -- -p compiler_builtins --features no-asm --release
+"${symcheck[@]}" "$target" -- -p compiler_builtins --features no-f16-f128
+"${symcheck[@]}" "$target" -- -p compiler_builtins --features no-f16-f128 --release
 
 run_intrinsics_test() {
-    args=(
-        --target "$target" --verbose \
-        --manifest-path builtins-test-intrinsics/Cargo.toml
-    )
-    args+=( "$@" )
+    build_args=(--verbose --manifest-path builtins-test-intrinsics/Cargo.toml)
+    build_args+=("$@")
 
     # symcheck also checks the results of builtins-test-intrinsics
-    "${symcheck[@]}" "${args[@]}"
+    "${symcheck[@]}" "$target" -- "${build_args[@]}"
 
     # FIXME: we get access violations on Windows, our entrypoint may need to
     # be tweaked.
     if [ "${BUILD_ONLY:-}" != "1" ] && ! [[ "$target" = *"windows"* ]]; then
-        cargo run "${args[@]}"
+        cargo run --target "$target" "${build_args[@]}"
     fi
 }
 

library/compiler-builtins/compiler-builtins/Cargo.toml

@@ -19,6 +19,8 @@ links = "compiler-rt"
 bench = false
 doctest = false
 test = false
+# make sure this crate isn't included in public standard library docs
+doc = false
 
 [dependencies]
 core = { path = "../../core", optional = true }

library/compiler-builtins/compiler-builtins/build.rs

@@ -2,7 +2,7 @@ mod configure;
 
 use std::env;
 
-use configure::{Target, configure_aliases, configure_f16_f128};
+use configure::{Target, configure_aliases};
 
 fn main() {
     println!("cargo::rerun-if-changed=build.rs");
@@ -12,7 +12,6 @@ fn main() {
     let cwd = env::current_dir().unwrap();
 
     configure_check_cfg();
-    configure_f16_f128(&target);
     configure_aliases(&target);
 
     configure_libm(&target);