Skip to content

Commit

Permalink
Fix signed discriminant in pure code (#1502)
Browse files Browse the repository at this point in the history
  • Loading branch information
fpoli authored Mar 1, 2024
1 parent 45405dc commit daf0e86
Show file tree
Hide file tree
Showing 3 changed files with 51 additions and 3 deletions.
46 changes: 46 additions & 0 deletions prusti-tests/tests/verify/fail/issues/issue-1501.rs
Original file line number Diff line number Diff line change
@@ -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() {}
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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());
Expand Down
2 changes: 1 addition & 1 deletion prusti-viper/src/encoder/mir/types/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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},
};

Expand Down

0 comments on commit daf0e86

Please sign in to comment.