From daf0e86329e9926f4b298ebe2757e70b3c7e7aa4 Mon Sep 17 00:00:00 2001
From: Federico Poli <fpoli@users.noreply.github.com>
Date: Fri, 1 Mar 2024 18:58:04 +0100
Subject: [PATCH] Fix signed discriminant in pure code (#1502)

---
 .../tests/verify/fail/issues/issue-1501.rs    | 46 +++++++++++++++++++
 .../mir/pure/interpreter/interpreter_poly.rs  |  6 ++-
 prusti-viper/src/encoder/mir/types/mod.rs     |  2 +-
 3 files changed, 51 insertions(+), 3 deletions(-)
 create mode 100644 prusti-tests/tests/verify/fail/issues/issue-1501.rs

diff --git a/prusti-tests/tests/verify/fail/issues/issue-1501.rs b/prusti-tests/tests/verify/fail/issues/issue-1501.rs
new file mode 100644
index 00000000000..89f3020894f
--- /dev/null
+++ 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
index 8d20ad75dbb..2c4edd0648b 100644
--- 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
index 91244066173..50e6df143ac 100644
--- 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},
 };