Merge branch 'main' into fma-intrinsics

.github/workflows/audit.yml

@@ -7,6 +7,7 @@
 name: Cargo Audit
 on:
  pull_request:
+ merge_group:
  push:
  # Run on changes to branches but not tags.
  branches:

.github/workflows/format-check.yml

@@ -3,6 +3,7 @@
 name: Kani Format Check
 on:
  pull_request:
+ merge_group:
  push:
  # Not just any push, as that includes tags.
  # We don't want to re-trigger this workflow when tagging an existing commit.

.github/workflows/kani.yml

@@ -3,6 +3,7 @@
 name: Kani CI
 on:
  pull_request:
+ merge_group:
  push:
  # Not just any push, as that includes tags.
  # We don't want to re-trigger this workflow when tagging an existing commit.

.github/workflows/release.yml

@@ -8,6 +8,7 @@
 name: Release Bundle
 on:
  pull_request:
+ merge_group:
  push:
  branches:
  - 'main'

docs/src/rust-feature-support/intrinsics.md

@@ -187,8 +187,8 @@ nontemporal_store | No | |
 offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) |
 powf32 | Partial | Results are overapproximated |
 powf64 | Partial | Results are overapproximated |
-powif32 | No | |
-powif64 | No | |
+powif32 | Partial | Results are overapproximated |
+powif64 | Partial | Results are overapproximated |
 pref_align_of | Yes | |
 prefetch_read_data | No | |
 prefetch_read_instruction | No | |

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -490,8 +490,8 @@ impl<'tcx> GotocCtx<'tcx> {
  ),
  "powf32" => codegen_simple_intrinsic!(Powf),
  "powf64" => codegen_simple_intrinsic!(Pow),
- "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)),
- "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)),
+ "powif32" => codegen_simple_intrinsic!(Powif),
+ "powif64" => codegen_simple_intrinsic!(Powi),
  "pref_align_of" => codegen_intrinsic_const!(),
  "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, place, loc),
  "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc),

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-08-01"
+channel = "nightly-2024-08-02"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs → tests/kani/Cast/cast_abstract_args_to_concrete.rs

@@ -1,9 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// https://github.com/model-checking/kani/issues/555
-// kani-flags: --no-undefined-function-checks
-
 // This regression test is in response to issue #135.
 // The type of the second parameter to powi is a `CInteger`, but
 // the type of `2` here is a `u32`. This test ensures that

tests/kani/Intrinsics/Math/Arith/powi.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn verify_powi32() {
+ let x: f32 = kani::any();
+ kani::assume(x.is_normal());
+ kani::assume(x >= 1e-19 || x <= -1e-19);
+ kani::assume(x <= 1.84e19 && x >= -1.84e19);
+ let x2 = x.powi(2);
+ assert!(x2 >= 0.0);
+}
+
+#[kani::proof]
+fn verify_powi64() {
+ let x: f64 = kani::any();
+ kani::assume(x.is_normal());
+ kani::assume(x >= 1e-153 || x <= -1e-153);
+ kani::assume(x <= 1.34e154 && x >= -1.34e154);
+ let x2 = x.powi(2);
+ assert!(x2 >= 0.0);
+}