Skip to content

Commit d9ad6e1

Browse files
author
Remi Delmas
committed
Intrinsics rint, roundeven, nearbyint replaced by round_ties_even.
Propagate changes from rust-lang/rust#136543 Use `__sort_of_CPROVER_round_to_integral` to model `round_ties_even`. Update tests.
1 parent 26706b4 commit d9ad6e1

File tree

11 files changed

+82
-265
lines changed

11 files changed

+82
-265
lines changed

‎cprover_bindings/src/goto_program/builtin.rs‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use super::{Expr, Location, Symbol, Type};
66

77
use std::fmt::Display;
88

9-
#[derive(Debug, Clone, Copy)]
9+
#[derive(Debug, Clone, Copy, PartialEq)]
1010
pub enum BuiltinFn {
1111
Abort,
1212
Assert,
@@ -59,6 +59,8 @@ pub enum BuiltinFn {
5959
Rintf,
6060
Round,
6161
Roundf,
62+
RoundToIntegralF,
63+
RoundToIntegral,
6264
Sin,
6365
Sinf,
6466
Sqrt,
@@ -123,6 +125,9 @@ impl Display for BuiltinFn {
123125
Rintf => "rintf",
124126
Round => "round",
125127
Roundf => "roundf",
128+
// TODO remove the sort_of prefix once we move up from CBMC 6.4.1
129+
RoundToIntegralF => "__sort_of_CPROVER_round_to_integralf",
130+
RoundToIntegral => "__sort_of_CPROVER_round_to_integral",
126131
Sin => "sin",
127132
Sinf => "sinf",
128133
Sqrt => "sqrt",
@@ -188,6 +193,8 @@ impl BuiltinFn {
188193
Rintf => vec![Type::float()],
189194
Round => vec![Type::double()],
190195
Roundf => vec![Type::float()],
196+
RoundToIntegralF => vec![Type::c_int(), Type::float()],
197+
RoundToIntegral => vec![Type::c_int(), Type::double()],
191198
Sin => vec![Type::double()],
192199
Sinf => vec![Type::float()],
193200
Sqrt => vec![Type::double()],
@@ -252,6 +259,8 @@ impl BuiltinFn {
252259
Rintf => Type::float(),
253260
Round => Type::double(),
254261
Roundf => Type::float(),
262+
RoundToIntegralF => Type::float(),
263+
RoundToIntegral => Type::double(),
255264
Sin => Type::double(),
256265
Sinf => Type::float(),
257266
Sqrt => Type::double(),
@@ -316,6 +325,8 @@ impl BuiltinFn {
316325
Rintf,
317326
Round,
318327
Roundf,
328+
RoundToIntegralF,
329+
RoundToIntegral,
319330
Sin,
320331
Sinf,
321332
Sqrt,

‎cprover_bindings/src/machine_model.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ pub enum RoundingMode {
4545
Downward = 1,
4646
Upward = 2,
4747
TowardsZero = 3,
48+
ToAway = 4,
4849
}
4950

5051
impl From<RoundingMode> for BigInt {

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -180,8 +180,6 @@ minnumf32 | Yes | |
180180
minnumf64 | Yes | |
181181
move_val_init | No | |
182182
mul_with_overflow | Yes | |
183-
nearbyintf32 | Yes | |
184-
nearbyintf64 | Yes | |
185183
needs_drop | Yes | |
186184
nontemporal_store | No | |
187185
offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) |
@@ -198,8 +196,10 @@ ptr_guaranteed_eq | Yes | |
198196
ptr_guaranteed_ne | Yes | |
199197
ptr_offset_from | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-4) |
200198
raw_eq | Partial | Cannot detect [uninitialized memory](#uninitialized-memory) |
201-
rintf32 | Yes | |
202-
rintf64 | Yes | |
199+
round_ties_even_f16 | No | |
200+
round_ties_even_f32 | Yes | |
201+
round_ties_even_f64 | Yes | |
202+
round_ties_even_f128 | No | |
203203
rotate_left | Yes | |
204204
rotate_right | Yes | |
205205
roundf32 | Yes | |

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

Lines changed: 35 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -414,8 +414,6 @@ impl GotocCtx<'_> {
414414
Intrinsic::MulWithOverflow => {
415415
self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, place, loc)
416416
}
417-
Intrinsic::NearbyIntF32 => codegen_simple_intrinsic!(Nearbyintf),
418-
Intrinsic::NearbyIntF64 => codegen_simple_intrinsic!(Nearbyint),
419417
Intrinsic::NeedsDrop => codegen_intrinsic_const!(),
420418
Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf),
421419
Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow),
@@ -425,12 +423,24 @@ impl GotocCtx<'_> {
425423
Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc),
426424
Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
427425
Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc),
428-
Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf),
429-
Intrinsic::RintF64 => codegen_simple_intrinsic!(Rint),
430426
Intrinsic::RotateLeft => codegen_intrinsic_binop!(rol),
431427
Intrinsic::RotateRight => codegen_intrinsic_binop!(ror),
432428
Intrinsic::RoundF32 => codegen_simple_intrinsic!(Roundf),
433429
Intrinsic::RoundF64 => codegen_simple_intrinsic!(Round),
430+
Intrinsic::RoundTiesEvenF32 => self.codegen_round_to_integral(
431+
BuiltinFn::RoundToIntegralF,
432+
cbmc::RoundingMode::ToNearest,
433+
fargs,
434+
place,
435+
loc,
436+
),
437+
Intrinsic::RoundTiesEvenF64 => self.codegen_round_to_integral(
438+
BuiltinFn::RoundToIntegral,
439+
cbmc::RoundingMode::ToNearest,
440+
fargs,
441+
place,
442+
loc,
443+
),
434444
Intrinsic::SaturatingAdd => codegen_intrinsic_binop_with_mm!(saturating_add),
435445
Intrinsic::SaturatingSub => codegen_intrinsic_binop_with_mm!(saturating_sub),
436446
Intrinsic::SinF32 => codegen_simple_intrinsic!(Sinf),
@@ -638,6 +648,27 @@ impl GotocCtx<'_> {
638648
dividend_is_int_min.and(divisor_is_minus_one).not()
639649
}
640650

651+
// Builds a call to the round_to_integral CPROVER function with specified cbmc::RoundingMode.
652+
fn codegen_round_to_integral(
653+
&mut self,
654+
function: BuiltinFn,
655+
rounding_mode: cbmc::RoundingMode,
656+
mut fargs: Vec<Expr>,
657+
place: &Place,
658+
loc: Location,
659+
) -> Stmt {
660+
assert!(function == BuiltinFn::RoundToIntegralF || function == BuiltinFn::RoundToIntegral);
661+
let mm = self.symbol_table.machine_model();
662+
fargs.insert(0, Expr::int_constant(rounding_mode, Type::c_int()));
663+
let casted_fargs = Expr::cast_arguments_to_target_equivalent_function_parameter_types(
664+
&function.as_expr(),
665+
fargs,
666+
mm,
667+
);
668+
let expr = function.call(casted_fargs, loc);
669+
self.codegen_expr_to_place_stable(place, expr, loc)
670+
}
671+
641672
/// Intrinsics of the form *_with_overflow
642673
fn codegen_op_with_overflow(
643674
&mut self,

‎kani-compiler/src/intrinsics.rs‎

Lines changed: 10 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -86,8 +86,6 @@ pub enum Intrinsic {
8686
MinNumF32,
8787
MinNumF64,
8888
MulWithOverflow,
89-
NearbyIntF32,
90-
NearbyIntF64,
9189
NeedsDrop,
9290
PowF32,
9391
PowF64,
@@ -99,12 +97,12 @@ pub enum Intrinsic {
9997
PtrOffsetFromUnsigned,
10098
RawEq,
10199
RetagBoxToRaw,
102-
RintF32,
103-
RintF64,
104100
RotateLeft,
105101
RotateRight,
106102
RoundF32,
107103
RoundF64,
104+
RoundTiesEvenF32,
105+
RoundTiesEvenF64,
108106
SaturatingAdd,
109107
SaturatingSub,
110108
SinF32,
@@ -676,10 +674,6 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option<Intrinsic> {
676674
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
677675
Some(Intrinsic::MinNumF32)
678676
}
679-
"nearbyintf32" => {
680-
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
681-
Some(Intrinsic::NearbyIntF32)
682-
}
683677
"powf32" => {
684678
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
685679
Some(Intrinsic::PowF32)
@@ -688,14 +682,14 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option<Intrinsic> {
688682
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F32));
689683
Some(Intrinsic::PowIF32)
690684
}
691-
"rintf32" => {
692-
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
693-
Some(Intrinsic::RintF32)
694-
}
695685
"roundf32" => {
696686
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
697687
Some(Intrinsic::RoundF32)
698688
}
689+
"round_ties_even_f32" => {
690+
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
691+
Some(Intrinsic::RoundTiesEvenF32)
692+
}
699693
"sinf32" => {
700694
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
701695
Some(Intrinsic::SinF32)
@@ -770,10 +764,6 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option<Intrinsic> {
770764
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
771765
Some(Intrinsic::MinNumF64)
772766
}
773-
"nearbyintf64" => {
774-
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
775-
Some(Intrinsic::NearbyIntF64)
776-
}
777767
"powf64" => {
778768
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
779769
Some(Intrinsic::PowF64)
@@ -782,14 +772,14 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option<Intrinsic> {
782772
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F64));
783773
Some(Intrinsic::PowIF64)
784774
}
785-
"rintf64" => {
786-
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
787-
Some(Intrinsic::RintF64)
788-
}
789775
"roundf64" => {
790776
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
791777
Some(Intrinsic::RoundF64)
792778
}
779+
"round_ties_even_f64" => {
780+
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
781+
Some(Intrinsic::RoundTiesEvenF64)
782+
}
793783
"sinf64" => {
794784
assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
795785
Some(Intrinsic::SinF64)

‎kani-compiler/src/kani_middle/points_to/points_to_analysis.rs‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -664,8 +664,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
664664
| Intrinsic::MinNumF32
665665
| Intrinsic::MinNumF64
666666
| Intrinsic::MulWithOverflow
667-
| Intrinsic::NearbyIntF32
668-
| Intrinsic::NearbyIntF64
669667
| Intrinsic::NeedsDrop
670668
| Intrinsic::PowF32
671669
| Intrinsic::PowF64
@@ -677,8 +675,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
677675
| Intrinsic::PtrOffsetFromUnsigned
678676
| Intrinsic::RawEq
679677
| Intrinsic::RetagBoxToRaw
680-
| Intrinsic::RintF32
681-
| Intrinsic::RintF64
682678
| Intrinsic::RotateLeft
683679
| Intrinsic::RotateRight
684680
| Intrinsic::RoundF32

‎kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -625,17 +625,13 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
625625
| Intrinsic::MinNumF32
626626
| Intrinsic::MinNumF64
627627
| Intrinsic::MulWithOverflow
628-
| Intrinsic::NearbyIntF32
629-
| Intrinsic::NearbyIntF64
630628
| Intrinsic::NeedsDrop
631629
| Intrinsic::PowF32
632630
| Intrinsic::PowF64
633631
| Intrinsic::PowIF32
634632
| Intrinsic::PowIF64
635633
| Intrinsic::PrefAlignOf
636634
| Intrinsic::RawEq
637-
| Intrinsic::RintF32
638-
| Intrinsic::RintF64
639635
| Intrinsic::RotateLeft
640636
| Intrinsic::RotateRight
641637
| Intrinsic::RoundF32

‎tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs‎

Lines changed: 0 additions & 104 deletions
This file was deleted.

0 commit comments

Comments
 (0)