Fix signed discriminant in pure code (#1502)

viperproject · Mar 1, 2024 · daf0e86 · daf0e86
1 parent 45405dc
commit daf0e86
Show file tree

Hide file tree

Showing 3 changed files with 51 additions and 3 deletions.
diff --git a/prusti-tests/tests/verify/fail/issues/issue-1501.rs b/prusti-tests/tests/verify/fail/issues/issue-1501.rs
@@ -0,0 +1,46 @@
+use prusti_contracts::prusti_assert;
+
+// An enum with *signed* and *explicit* discriminants
+enum Ordering {
+    Less = -10,
+    Equal = 0,
+    Greater = 100,
+}
+
+fn good() {
+    assert!(matches!(Ordering::Less, Ordering::Less));
+    assert!(matches!(Ordering::Equal, Ordering::Equal));
+    assert!(matches!(Ordering::Greater, Ordering::Greater));
+    prusti_assert!(matches!(Ordering::Less, Ordering::Less));
+    prusti_assert!(matches!(Ordering::Equal, Ordering::Equal));
+    prusti_assert!(matches!(Ordering::Greater, Ordering::Greater));
+
+    // Smoke test
+    assert!(false); //~ ERROR: asserted expression might not hold
+}
+
+fn bad_1() {
+    assert!(!matches!(Ordering::Less, Ordering::Less)); //~ ERROR: asserted expression might not hold
+}
+
+fn bad_2() {
+    assert!(!matches!(Ordering::Equal, Ordering::Equal)); //~ ERROR: asserted expression might not hold
+}
+
+fn bad_3() {
+    assert!(!matches!(Ordering::Greater, Ordering::Greater)); //~ ERROR: asserted expression might not hold
+}
+
+fn bad_4() {
+    prusti_assert!(!matches!(Ordering::Less, Ordering::Less)); //~ ERROR: asserted expression might not hold
+}
+
+fn bad_5() {
+    prusti_assert!(!matches!(Ordering::Equal, Ordering::Equal)); //~ ERROR: asserted expression might not hold
+}
+
+fn bad_6() {
+    prusti_assert!(!matches!(Ordering::Greater, Ordering::Greater)); //~ ERROR: asserted expression might not hold
+}
+
+fn main() {}
diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs
@@ -17,7 +17,7 @@ use crate::{
             },
             sequences::MirSequencesEncoderInterface,
             specifications::SpecificationsInterface,
-            types::MirTypeEncoderInterface,
+            types::{compute_discriminant_values, MirTypeEncoderInterface},
         },
         mir_encoder::{
             MirEncoder, PlaceEncoder, PlaceEncoding, PRECONDITION_LABEL, WAND_LHS_LABEL,
@@ -936,9 +936,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
                                 let mut encoded_lhs_variant = encoded_lhs.clone();
                                 if num_variants > 1 {
                                     let discr_field = self.encoder.encode_discriminant_field();
+                                    let discr_values = compute_discriminant_values(adt_def, tcx);
+                                    let discr_value = discr_values[variant_index.as_usize()];
                                     state.substitute_value(
                                         &encoded_lhs.clone().field(discr_field),
-                                        variant_index.index().into(),
+                                        discr_value.into(),
                                     );
                                     encoded_lhs_variant =
                                         encoded_lhs_variant.variant(variant_def.ident(tcx).as_str());

diff --git a/prusti-viper/src/encoder/mir/types/mod.rs b/prusti-viper/src/encoder/mir/types/mod.rs
@@ -7,7 +7,7 @@ mod interface;
 mod lifetimes;
 
 pub(crate) use self::{
-    helpers::compute_discriminant_bounds,
+    helpers::{compute_discriminant_bounds, compute_discriminant_values},
     interface::{MirTypeEncoderInterface, MirTypeEncoderState},
 };