From 4af374175d9c69599a0c1d39fe7bd631929bedbe Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Thu, 27 Jan 2022 15:55:32 -0500 Subject: [PATCH] Partial support for `bitreverse` (#779) * Support for `bitreverse` (WIP) * Add test for all types --- .../cbmc/src/goto_program/expr.rs | 11 ++++- .../symtab_transformer/transformer.rs | 1 + src/kani-compiler/cbmc/src/irep/irep_id.rs | 2 + src/kani-compiler/cbmc/src/irep/to_irep.rs | 4 ++ .../src/codegen/intrinsic.rs | 1 + tests/kani/Intrinsics/fixme_bitreverse.rs | 47 +++++++++++++++++++ 6 files changed, 64 insertions(+), 2 deletions(-) create mode 100644 tests/kani/Intrinsics/fixme_bitreverse.rs diff --git a/src/kani-compiler/cbmc/src/goto_program/expr.rs b/src/kani-compiler/cbmc/src/goto_program/expr.rs index 4f812960f391..b9a291a4d79f 100644 --- a/src/kani-compiler/cbmc/src/goto_program/expr.rs +++ b/src/kani-compiler/cbmc/src/goto_program/expr.rs @@ -203,6 +203,8 @@ pub enum SelfOperand { pub enum UnaryOperand { /// `~self` Bitnot, + /// `__builtin_bitreverse(self)` + BitReverse, /// `__builtin_bswap(self)` Bswap, /// `__CPROVER_DYNAMIC_OBJECT(self)` @@ -1086,7 +1088,7 @@ impl Expr { impl Expr { fn typecheck_unop_arg(op: UnaryOperand, arg: &Expr) -> bool { match op { - Bitnot | Bswap | Popcount => arg.typ.is_integer(), + Bitnot | BitReverse | Bswap | Popcount => arg.typ.is_integer(), CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.is_integer(), IsDynamicObject | ObjectSize | PointerObject => arg.typ().is_pointer(), PointerOffset => arg.typ == Type::void_pointer(), @@ -1097,7 +1099,7 @@ impl Expr { fn unop_return_type(op: UnaryOperand, arg: &Expr) -> Type { match op { - Bitnot | Bswap | UnaryMinus => arg.typ.clone(), + Bitnot | BitReverse | Bswap | UnaryMinus => arg.typ.clone(), CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.clone(), ObjectSize | PointerObject => Type::size_t(), PointerOffset => Type::ssize_t(), @@ -1122,6 +1124,11 @@ impl Expr { self.unop(Bswap) } + /// `__builtin_bitreverse(self)` + pub fn bitreverse(self) -> Expr { + self.unop(BitReverse) + } + /// `__CPROVER_DYNAMIC_OBJECT(self)` pub fn dynamic_object(self) -> Self { self.unop(IsDynamicObject) diff --git a/src/kani-compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs b/src/kani-compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs index 140d4dc63201..3f347e85ea6c 100644 --- a/src/kani-compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs +++ b/src/kani-compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs @@ -476,6 +476,7 @@ pub trait Transformer: Sized { let transformed_e = self.transform_expr(e); match op { UnaryOperand::Bitnot => transformed_e.bitnot(), + UnaryOperand::BitReverse => transformed_e.bitreverse(), UnaryOperand::Bswap => transformed_e.bswap(), UnaryOperand::IsDynamicObject => transformed_e.dynamic_object(), UnaryOperand::Not => transformed_e.not(), diff --git a/src/kani-compiler/cbmc/src/irep/irep_id.rs b/src/kani-compiler/cbmc/src/irep/irep_id.rs index 1ca0fb155643..dffa7f06802f 100644 --- a/src/kani-compiler/cbmc/src/irep/irep_id.rs +++ b/src/kani-compiler/cbmc/src/irep/irep_id.rs @@ -593,6 +593,7 @@ pub enum IrepId { WorkingDirectory, Section, Bswap, + BitReverse, JavaBytecodeIndex, JavaInstanceof, JavaSuperMethodCall, @@ -1431,6 +1432,7 @@ impl ToString for IrepId { IrepId::WorkingDirectory => "working_directory", IrepId::Section => "section", IrepId::Bswap => "bswap", + IrepId::BitReverse => "bitreverse", IrepId::JavaBytecodeIndex => "java_bytecode_index", IrepId::JavaInstanceof => "java_instanceof", IrepId::JavaSuperMethodCall => "java_super_method_call", diff --git a/src/kani-compiler/cbmc/src/irep/to_irep.rs b/src/kani-compiler/cbmc/src/irep/to_irep.rs index cce47e715c20..3ad1bf41f7b0 100644 --- a/src/kani-compiler/cbmc/src/irep/to_irep.rs +++ b/src/kani-compiler/cbmc/src/irep/to_irep.rs @@ -98,6 +98,7 @@ impl ToIrepId for UnaryOperand { fn to_irep_id(&self) -> IrepId { match self { UnaryOperand::Bitnot => IrepId::Bitnot, + UnaryOperand::BitReverse => IrepId::BitReverse, UnaryOperand::Bswap => IrepId::Bswap, UnaryOperand::CountLeadingZeros { .. } => IrepId::CountLeadingZeros, UnaryOperand::CountTrailingZeros { .. } => IrepId::CountTrailingZeros, @@ -277,6 +278,9 @@ impl ToIrep for ExprValue { sub: vec![e.to_irep(mm)], named_sub: vector_map![(IrepId::BitsPerByte, Irep::just_int_id(8))], }, + ExprValue::UnOp { op: UnaryOperand::BitReverse, e } => { + Irep { id: IrepId::BitReverse, sub: vec![e.to_irep(mm)], named_sub: vector_map![] } + } ExprValue::UnOp { op: UnaryOperand::CountLeadingZeros { allow_zero }, e } => Irep { id: IrepId::CountLeadingZeros, sub: vec![e.to_irep(mm)], diff --git a/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs b/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs index c86b10e36a66..29acadf54457 100644 --- a/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs +++ b/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs @@ -355,6 +355,7 @@ impl<'tcx> GotocCtx<'tcx> { "atomic_xsub_acqrel" => codegen_atomic_binop!(sub), "atomic_xsub_rel" => codegen_atomic_binop!(sub), "atomic_xsub_relaxed" => codegen_atomic_binop!(sub), + "bitreverse" => self.codegen_expr_to_place(p, fargs.remove(0).bitreverse()), // black_box is an identity function that hints to the compiler // to be maximally pessimistic to limit optimizations "black_box" => self.codegen_expr_to_place(p, fargs.remove(0)), diff --git a/tests/kani/Intrinsics/fixme_bitreverse.rs b/tests/kani/Intrinsics/fixme_bitreverse.rs new file mode 100644 index 000000000000..544e129127c2 --- /dev/null +++ b/tests/kani/Intrinsics/fixme_bitreverse.rs @@ -0,0 +1,47 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that we get the expected results for the `bitreverse` intrinsic +// https://doc.rust-lang.org/std/intrinsics/fn.bitreverse.html + +// Note: Support for `__builtin_bitreverse` in CBMC is being added in +// https://github.com/diffblue/cbmc/pull/6581 +// Tracking issue: https://github.com/model-checking/kani/issues/778 + +const BITS_PER_BYTE: usize = 8; + +macro_rules! test_bitreverse_intrinsic { + ($ty:ty, $check_name:ident, $get_bit_name:ident) => { + fn $get_bit_name(x: $ty, n: usize) -> bool { + return x & (1 << n) != 0; + } + + fn $check_name(a: $ty, b: $ty) -> bool { + let len: usize = (std::mem::size_of::<$ty>() * BITS_PER_BYTE) - 1; + for n in 0..len { + if $get_bit_name(a, n) != $get_bit_name(b, len - n) { + return false; + } + } + return true; + } + + let x: $ty = kani::any(); + let res = $check_name(x, x.reverse_bits()); + assert!(res); + }; +} + +#[allow(overflowing_literals)] +fn main() { + test_bitreverse_intrinsic!(u8, check_reverse_u8, get_bit_at_u8); + test_bitreverse_intrinsic!(u16, check_reverse_u16, get_bit_at_u16); + test_bitreverse_intrinsic!(u32, check_reverse_u32, get_bit_at_u32); + test_bitreverse_intrinsic!(u64, check_reverse_u64, get_bit_at_u64); + test_bitreverse_intrinsic!(usize, check_reverse_usize, get_bit_at_usize); + test_bitreverse_intrinsic!(i8, check_reverse_i8, get_bit_at_i8); + test_bitreverse_intrinsic!(i16, check_reverse_i16, get_bit_at_i16); + test_bitreverse_intrinsic!(i32, check_reverse_i32, get_bit_at_i32); + test_bitreverse_intrinsic!(i64, check_reverse_i64, get_bit_at_i64); + test_bitreverse_intrinsic!(isize, check_reverse_isize, get_bit_at_isize); +}