|
4 | 4 | use super::typ::{self, pointee_type};
|
5 | 5 | use super::PropertyClass;
|
6 | 6 | use crate::codegen_cprover_gotoc::GotocCtx;
|
| 7 | +use crate::unwrap_or_return_codegen_unimplemented_stmt; |
7 | 8 | use cbmc::goto_program::{
|
8 | 9 | ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
|
9 | 10 | };
|
@@ -408,6 +409,7 @@ impl<'tcx> GotocCtx<'tcx> {
|
408 | 409 | ),
|
409 | 410 | "ceilf32" => codegen_simple_intrinsic!(Ceilf),
|
410 | 411 | "ceilf64" => codegen_simple_intrinsic!(Ceil),
|
| 412 | + "compare_bytes" => self.codegen_compare_bytes(fargs, p, loc), |
411 | 413 | "copy" => self.codegen_copy(intrinsic, false, fargs, farg_types, Some(p), loc),
|
412 | 414 | "copy_nonoverlapping" => unreachable!(
|
413 | 415 | "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`"
|
@@ -987,6 +989,42 @@ impl<'tcx> GotocCtx<'tcx> {
|
987 | 989 | Stmt::block(vec![src_align_check, dst_align_check, overflow_check, copy_expr], loc)
|
988 | 990 | }
|
989 | 991 |
|
| 992 | + /// This is an intrinsic that was added in |
| 993 | + /// https://github.com/rust-lang/rust/pull/114382 that is essentially the |
| 994 | + /// same as memcmp: it compares two slices up to the specified length. |
| 995 | + /// The implementation is the same as the hook for `memcmp`. |
| 996 | + pub fn codegen_compare_bytes( |
| 997 | + &mut self, |
| 998 | + mut fargs: Vec<Expr>, |
| 999 | + p: &Place<'tcx>, |
| 1000 | + loc: Location, |
| 1001 | + ) -> Stmt { |
| 1002 | + let lhs = fargs.remove(0).cast_to(Type::void_pointer()); |
| 1003 | + let rhs = fargs.remove(0).cast_to(Type::void_pointer()); |
| 1004 | + let len = fargs.remove(0); |
| 1005 | + let (len_var, len_decl) = self.decl_temp_variable(len.typ().clone(), Some(len), loc); |
| 1006 | + let (lhs_var, lhs_decl) = self.decl_temp_variable(lhs.typ().clone(), Some(lhs), loc); |
| 1007 | + let (rhs_var, rhs_decl) = self.decl_temp_variable(rhs.typ().clone(), Some(rhs), loc); |
| 1008 | + let is_len_zero = len_var.clone().is_zero(); |
| 1009 | + // We have to ensure that the pointers are valid even if we're comparing zero bytes. |
| 1010 | + // According to Rust's current definition (see https://github.com/model-checking/kani/issues/1489), |
| 1011 | + // this means they have to be non-null and aligned. |
| 1012 | + // But alignment is automatically satisfied because `memcmp` takes `*const u8` pointers. |
| 1013 | + let is_lhs_ok = lhs_var.clone().is_nonnull(); |
| 1014 | + let is_rhs_ok = rhs_var.clone().is_nonnull(); |
| 1015 | + let should_skip_pointer_checks = is_len_zero.and(is_lhs_ok).and(is_rhs_ok); |
| 1016 | + let place_expr = |
| 1017 | + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(&p)).goto_expr; |
| 1018 | + let res = should_skip_pointer_checks.ternary( |
| 1019 | + Expr::int_constant(0, place_expr.typ().clone()), // zero bytes are always equal (as long as pointers are nonnull and aligned) |
| 1020 | + BuiltinFn::Memcmp |
| 1021 | + .call(vec![lhs_var, rhs_var, len_var], loc) |
| 1022 | + .cast_to(place_expr.typ().clone()), |
| 1023 | + ); |
| 1024 | + let code = place_expr.assign(res, loc).with_location(loc); |
| 1025 | + Stmt::block(vec![len_decl, lhs_decl, rhs_decl, code], loc) |
| 1026 | + } |
| 1027 | + |
990 | 1028 | // In some contexts (e.g., compilation-time evaluation),
|
991 | 1029 | // `ptr_guaranteed_cmp` compares two pointers and returns:
|
992 | 1030 | // * 2 if the result is unknown.
|
|
0 commit comments