Allow discriminant reads not followed by SwitchInt

charon/src/transform/remove_read_discriminant.rs

@@ -8,6 +8,7 @@ use crate::llbc_ast::*;
 use crate::meta::combine_meta;
 use crate::translate_ctx::*;
 use crate::types::*;
+use crate::values::{Literal, ScalarValue};
 use itertools::Itertools;
 use std::collections::{HashMap, HashSet};
 
@@ -81,7 +82,7 @@ impl<'a, 'tcx, 'ctx> Visitor<'a, 'tcx, 'ctx> {
                     RawStatement::Switch(switch @ Switch::SwitchInt(..)) => {
                         Ok((st2.meta, switch, None))
                     }
-                    _ => Err(()),
+                    _ => Err(st2),
                 };
 
                 match maybe_switch {
@@ -92,18 +93,17 @@ impl<'a, 'tcx, 'ctx> Visitor<'a, 'tcx, 'ctx> {
 
                         // Convert between discriminants and variant indices. Remark: the discriminant can
                         // be of any *signed* integer type (`isize`, `i8`, etc.).
-                        let discr_to_id: HashMap<u128, VariantId::Id> = variants
+                        let discr_to_id: HashMap<ScalarValue, VariantId::Id> = variants
                             .iter_indexed_values()
                             .map(|(id, variant)| (variant.discriminant, id))
                             .collect();
-                        let mut covered_discriminants: HashSet<u128> = HashSet::default();
+                        let mut covered_discriminants: HashSet<ScalarValue> = HashSet::default();
                         let targets = targets
                             .into_iter()
                             .map(|(v, e)| {
                                 (
                                     v.into_iter()
-                                        .filter_map(|x| {
-                                            let discr = x.to_bits();
+                                        .filter_map(|discr| {
                                             covered_discriminants.insert(discr);
                                             discr_to_id.get(&discr).or_else(|| {
                                                 register_error_or_panic!(
@@ -139,20 +139,34 @@ impl<'a, 'tcx, 'ctx> Visitor<'a, 'tcx, 'ctx> {
                             switch
                         };
                     }
-                    Err(_) => {
-                        // A discriminant read must be immediately followed by a switch int.
-                        register_error_or_panic!(
-                            self.ctx,
-                            st.meta.span.rust_span_data.span(),
-                            "A discriminant read must be followed by a `SwitchInt`"
-                        );
-                        // An error occurred. We can't keep the `Rvalue::Discriminant` around so we
-                        // `Nop` the whole statement sequence.
-                        // FIXME: add `RawStatement::Error` for cases like this.
-                        *st = Statement {
-                            content: RawStatement::Nop,
-                            meta: st.meta,
+                    Err(st2) => {
+                        // The discriminant read is not followed by a `SwitchInt`. We replace `_x =
+                        // Discr(_y)` with `match _y { 0 => { _x = 0 }, 1 => { _x = 1; }, .. }`.
+                        let targets = variants
+                            .iter_indexed_values()
+                            .map(|(id, variant)| {
+                                let value = variant.discriminant;
+                                let int_ty = value.get_integer_ty();
+                                let konst = ConstantExpr {
+                                    value: RawConstantExpr::Literal(Literal::Scalar(value)),
+                                    ty: Ty::Literal(LiteralTy::Integer(int_ty)),
+                                };
+                                let statement = Statement {
+                                    meta: *meta1,
+                                    content: RawStatement::Assign(
+                                        dest.clone(),
+                                        Rvalue::Use(Operand::Const(konst)),
+                                    ),
+                                };
+                                (vec![id], statement)
+                            })
+                            .collect();
+                        let switch = RawStatement::Switch(Switch::Match(p.clone(), targets, None));
+                        let switch = Statement {
+                            meta: *meta1,
+                            content: switch,
                         };
+                        st.content = new_sequence(switch, st2).content
                     }
                 }
             }

charon/src/translate_types.rs

@@ -4,6 +4,7 @@ use crate::formatter::IntoFormatter;
 use crate::gast::*;
 use crate::translate_ctx::*;
 use crate::types::*;
+use crate::values::ScalarValue;
 use core::convert::*;
 use hax_frontend_exporter as hax;
 use hax_frontend_exporter::SInto;
@@ -542,11 +543,15 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             let var_def: hax::VariantDef = var_def.sinto(&self.hax_state);
             trace!("variant {i}: {var_def:?}");
 
-            let discriminant: u128 = if adt.is_enum() {
-                adt.discriminant_for_variant(self.t_ctx.tcx, rust_var_id)
-                    .val
+            let discriminant = if adt.is_enum() {
+                let discr = adt.discriminant_for_variant(self.t_ctx.tcx, rust_var_id);
+                let bits = discr.val;
+                let ty = discr.ty.sinto(&self.hax_state);
+                let ty = self.translate_ty(def_span, true, &ty)?;
+                let int_ty = *ty.as_literal().as_integer();
+                ScalarValue::from_bits(int_ty, bits)
             } else {
-                0
+                ScalarValue::Isize(0)
             };
 
             let mut fields: FieldId::Vector<Field> = Default::default();

charon/src/types.rs

@@ -2,7 +2,7 @@ pub use crate::gast::{FunDeclId, TraitItemName};
 use crate::meta::{ItemMeta, Meta};
 use crate::names::Name;
 pub use crate::types_utils::*;
-use crate::values::Literal;
+use crate::values::{Literal, ScalarValue};
 use derivative::Derivative;
 use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
 use serde::Serialize;
@@ -369,10 +369,10 @@ pub struct Variant {
     pub meta: Meta,
     pub name: String,
     pub fields: FieldId::Vector<Field>,
-    #[serde(skip)]
     /// The discriminant used at runtime. This is used in `remove_read_discriminant` to match up
     /// `SwitchInt` targets with the corresponding `Variant`.
-    pub discriminant: u128,
+    #[serde(skip)]
+    pub discriminant: ScalarValue,
 }
 
 #[derive(Debug, Clone, Serialize)]

charon/src/values_utils.rs

@@ -218,6 +218,9 @@ impl ScalarValue {
             ScalarValue::I128(v) => v as u128,
         }
     }
+    pub fn from_bits(ty: IntegerTy, bits: u128) -> Self {
+        Self::from_le_bytes(ty, bits.to_le_bytes())
+    }
 
     /// **Warning**: most constants are stored as u128 by rustc. When converting
     /// to i128, it is not correct to do `v as i128`, we must reinterpret the

charon/tests/ui/issue-120-bare-discriminant-read.out

@@ -1,6 +1,3 @@
-error: A discriminant read must be followed by a `SwitchInt`
- --> /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs:598:5
-
 [ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization:
 
 enum core::option::Option<T> =
@@ -13,9 +10,21 @@ fn test_crate::call_is_some<T>(@1: core::option::Option<T>) -> bool
     let @0: bool; // return
     let opt@1: core::option::Option<T>; // arg #1
     let self@2: &'_ (core::option::Option<T>); // local
+    let @3: isize; // anonymous local
 
     self@2 := &opt@1
-    nop
+    match *(self@2) {
+        0 => {
+            @3 := const (0 : isize)
+        },
+        1 => {
+            @3 := const (1 : isize)
+        }
+    }
+    @0 := copy (@3) == const (1 : isize)
+    drop self@2
+    drop opt@1
+    return
 }
 
 fn test_crate::my_is_some<T>(@1: core::option::Option<T>) -> isize
@@ -37,6 +46,3 @@ fn test_crate::my_is_some<T>(@1: core::option::Option<T>) -> isize
 
 
 
-error: aborting due to previous error
-
-[ ERROR charon_driver:180] The extraction encountered 1 errors

charon/tests/ui/issue-120-bare-discriminant-read.rs

@@ -1,4 +1,3 @@
-//@ known-failure
 //@ charon-args=--extract-opaque-bodies
 //@ charon-args=--mir_optimized
 //@ rustc-args=-C opt-level=3