Revert change to rustc SwitchTargets type. (rust-lang#710)

We have changed the visibility of one of the members of SwitchTargets to
have access to their values during codegen. I re-wrote the code to use
standard API so we don't need to keep using a forked version of the
compiler. Issue rust-lang#42.

The only changes left are the ones to enable rmc codegen and a a few
options we enabled. Those should be handled once we have a new driver.

Author: celinval

compiler/rustc_codegen_rmc/src/codegen/statement.rs

@@ -40,12 +40,9 @@ impl<'tcx> GotocCtx<'tcx> {
             TerminatorKind::Goto { target } => {
                 Stmt::goto(self.current_fn().find_label(target), loc)
             }
-            TerminatorKind::SwitchInt { discr, switch_ty, targets } => match targets {
-                SwitchTargets { values, .. } => {
-                    let all_targets = targets.all_targets();
-                    self.codegen_switch_int(discr, switch_ty, values, all_targets)
-                }
-            },
+            TerminatorKind::SwitchInt { discr, switch_ty, targets } => {
+                self.codegen_switch_int(discr, switch_ty, targets)
+            }
             TerminatorKind::Resume => Stmt::assert_false("resume instruction", loc),
             TerminatorKind::Abort => Stmt::assert_false("abort instruction", loc),
             TerminatorKind::Return => {
@@ -206,62 +203,48 @@ impl<'tcx> GotocCtx<'tcx> {
         &mut self,
         discr: &Operand<'tcx>,
         switch_ty: Ty<'tcx>,
-        values: &SmallVec<[u128; 1]>,
-        targets: &[BasicBlock],
+        targets: &SwitchTargets,
     ) -> Stmt {
-        assert_eq!(targets.len(), values.len() + 1);
-
         let v = self.codegen_operand(discr);
         let switch_ty = self.monomorphize(switch_ty);
-        match switch_ty.kind() {
-            //TODO, can replace with guarded goto
-            ty::Bool => {
-                let jmp: usize = values[0].try_into().unwrap();
-                let jmp2 = if jmp == 0 { 1 } else { 0 };
-                Stmt::block(
-                    vec![
-                        v.cast_to(Type::bool()).if_then_else(
+        if targets.all_targets().len() == 1 {
+            // Translate to a guarded goto
+            let first_target = targets.iter().next().unwrap();
+            Stmt::block(
+                vec![
+                    v.eq(Expr::int_constant(first_target.0, self.codegen_ty(switch_ty)))
+                        .if_then_else(
                             Stmt::goto(
-                                self.current_fn().labels()[targets[jmp2].index()].clone(),
+                                self.current_fn().labels()[first_target.1.index()].clone(),
                                 Location::none(),
                             ),
                             None,
                             Location::none(),
                         ),
-                        Stmt::goto(
-                            self.current_fn().labels()[targets[jmp].index()].clone(),
-                            Location::none(),
-                        ),
-                    ],
-                    Location::none(),
-                )
-            }
-            ty::Char | ty::Int(_) | ty::Uint(_) => {
-                let cases = values
-                    .iter()
-                    .enumerate()
-                    .map(|(i, idx)| {
-                        let bb = &targets[i];
-                        Expr::int_constant(*idx, self.codegen_ty(switch_ty)).switch_case(
-                            Stmt::goto(
-                                self.current_fn().labels()[bb.index()].clone(),
-                                Location::none(),
-                            ),
-                        )
-                    })
-                    .collect();
-                let default = Stmt::goto(
-                    self.current_fn().labels()[targets[values.len()].index()].clone(),
-                    Location::none(),
-                );
-                v.switch(cases, Some(default), Location::none())
-            }
-            x => {
-                unreachable!(
-                    "Unexpected switch_ty {:?}\n{:?}\n{:?}\n{:?}\n{:?}\n{:?}",
-                    discr, switch_ty, values, targets, v, x
-                )
-            }
+                    Stmt::goto(
+                        self.current_fn().labels()[targets.otherwise().index()].clone(),
+                        Location::none(),
+                    ),
+                ],
+                Location::none(),
+            )
+        } else {
+            // Switches with empty targets should've been eliminated already.
+            assert!(targets.all_targets().len() > 1);
+            let cases = targets
+                .iter()
+                .map(|(c, bb)| {
+                    Expr::int_constant(c, self.codegen_ty(switch_ty)).switch_case(Stmt::goto(
+                        self.current_fn().labels()[bb.index()].clone(),
+                        Location::none(),
+                    ))
+                })
+                .collect();
+            let default = Stmt::goto(
+                self.current_fn().labels()[targets.otherwise().index()].clone(),
+                Location::none(),
+            );
+            v.switch(cases, Some(default), Location::none())
         }
     }
 

compiler/rustc_middle/src/mir/terminator.rs

@@ -21,7 +21,7 @@ pub use super::query::*;
 pub struct SwitchTargets {
     /// Possible values. The locations to branch to in each case
     /// are found in the corresponding indices from the `targets` vector.
-    pub values: SmallVec<[u128; 1]>,
+    values: SmallVec<[u128; 1]>,
 
     /// Possible branch sites. The last element of this vector is used
     /// for the otherwise branch, so targets.len() == values.len() + 1

src/test/rmc/Match/match_bool.rs

@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// compile-flags: --crate-type lib
+// rmc-flags: --function match_bool
+
+#[rmc::proof]
+pub fn match_bool() {
+    let arg: bool = rmc::nondet();
+    let var = match arg {
+        true => !arg,
+        _ => arg,
+    };
+
+    let var2 = match arg {
+        _ => false,
+    };
+
+    assert!(var == var2);
+
+    let mut i = 0;
+
+    match arg {
+        true => i = 1,
+        false => i = 2,
+        _ => i = 3,
+    }
+
+    assert!(i == 1 || i == 2);
+}