Skip to content

Commit 7a855e3

Browse files
zhassan-awstedinski
authored andcommitted
Removed incorrect special case for Rust bitwise operators (rust-lang#403)
1 parent 6917306 commit 7a855e3

File tree

2 files changed

+14
-22
lines changed
  • compiler/rustc_codegen_llvm/src/gotoc
  • src/test/cbmc/BitwiseArithOperators

2 files changed

+14
-22
lines changed

compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs

Lines changed: 4 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -48,30 +48,12 @@ impl<'tcx> GotocCtx<'tcx> {
4848
let ce1 = self.codegen_operand(e1);
4949
let ce2 = self.codegen_operand(e2);
5050
match op {
51+
BinOp::BitAnd => ce1.bitand(ce2),
52+
BinOp::BitOr => ce1.bitor(ce2),
53+
BinOp::BitXor => ce1.bitxor(ce2),
5154
BinOp::Div => ce1.div(ce2),
5255
BinOp::Rem => ce1.rem(ce2),
53-
BinOp::BitXor => {
54-
if self.operand_ty(e1).is_bool() {
55-
ce1.xor(ce2)
56-
} else {
57-
ce1.bitxor(ce2)
58-
}
59-
}
60-
BinOp::BitAnd => {
61-
if self.operand_ty(e1).is_bool() {
62-
ce1.and(ce2)
63-
} else {
64-
ce1.bitand(ce2)
65-
}
66-
}
67-
BinOp::BitOr => {
68-
if self.operand_ty(e1).is_bool() {
69-
ce1.or(ce2)
70-
} else {
71-
ce1.bitor(ce2)
72-
}
73-
}
74-
_ => unreachable!(),
56+
_ => unreachable!("Unexpected {:?}", op),
7557
}
7658
}
7759

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
include!("../../rmc-prelude.rs");
4+
5+
fn main() {
6+
let a: bool = __nondet();
7+
let b: bool = __nondet();
8+
let c = a ^ b;
9+
assert!((a == b && !c) || (a != b && c));
10+
}

0 commit comments

Comments
 (0)