diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index d3dae46e4f82..23d760473e4a 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -48,30 +48,12 @@ impl<'tcx> GotocCtx<'tcx> { let ce1 = self.codegen_operand(e1); let ce2 = self.codegen_operand(e2); match op { + BinOp::BitAnd => ce1.bitand(ce2), + BinOp::BitOr => ce1.bitor(ce2), + BinOp::BitXor => ce1.bitxor(ce2), BinOp::Div => ce1.div(ce2), BinOp::Rem => ce1.rem(ce2), - BinOp::BitXor => { - if self.operand_ty(e1).is_bool() { - ce1.xor(ce2) - } else { - ce1.bitxor(ce2) - } - } - BinOp::BitAnd => { - if self.operand_ty(e1).is_bool() { - ce1.and(ce2) - } else { - ce1.bitand(ce2) - } - } - BinOp::BitOr => { - if self.operand_ty(e1).is_bool() { - ce1.or(ce2) - } else { - ce1.bitor(ce2) - } - } - _ => unreachable!(), + _ => unreachable!("Unexpected {:?}", op), } } diff --git a/src/test/cbmc/BitwiseArithOperators/bool.rs b/src/test/cbmc/BitwiseArithOperators/bool.rs new file mode 100644 index 000000000000..01b3a979e5ad --- /dev/null +++ b/src/test/cbmc/BitwiseArithOperators/bool.rs @@ -0,0 +1,10 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +include!("../../rmc-prelude.rs"); + +fn main() { + let a: bool = __nondet(); + let b: bool = __nondet(); + let c = a ^ b; + assert!((a == b && !c) || (a != b && c)); +}