From 16702d558d5610c363c0990e2371fdcb5d5d0928 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Tue, 21 Feb 2023 12:03:34 +0100 Subject: [PATCH] support unevaluated constants in specs (fix #1268) --- .../verify_overflow/pass/issues/issue-1268.rs | 13 +++++ .../mir/pure/interpreter/interpreter_poly.rs | 9 ++-- .../mir/pure/pure_functions/encoder_poly.rs | 51 ++++++++++++++++++- .../mir/pure/pure_functions/interface.rs | 19 ++++++- 4 files changed, 86 insertions(+), 6 deletions(-) create mode 100644 prusti-tests/tests/verify_overflow/pass/issues/issue-1268.rs diff --git a/prusti-tests/tests/verify_overflow/pass/issues/issue-1268.rs b/prusti-tests/tests/verify_overflow/pass/issues/issue-1268.rs new file mode 100644 index 00000000000..d928651401d --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/issues/issue-1268.rs @@ -0,0 +1,13 @@ +use prusti_contracts::*; + +enum TestEnum { + Nil, +} + +#[ensures(TestEnum::Nil === TestEnum::Nil)] +fn test() {} + +fn main() { + let foo = 5; + prusti_assert!(foo === 5); +} 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 a7b9dd82fb5..bdabbb9b795 100644 --- a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs @@ -134,9 +134,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionBackwardInterpreter<'p, 'v, 'tcx> { &mir::Operand::Move(place) | &mir::Operand::Copy(place) => { Ok((self.encode_place(place)?.0, false)) } - mir::Operand::Constant(constant) => { - Ok((self.encoder.encode_snapshot_constant(constant)?, true)) - } + mir::Operand::Constant(constant) => match constant.literal { + mir::ConstantKind::Unevaluated(c, _cty) => { + Ok((self.encoder.encode_uneval_const(c)?, true)) + } + _ => Ok((self.encoder.encode_snapshot_constant(constant)?, true)), + }, } } diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs index 0dbecf24009..37bc0a93a4d 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs @@ -67,18 +67,65 @@ pub(super) fn encode_body<'p, 'v: 'p, 'tcx: 'v>( .env() .body .get_expression_body(proc_def_id, substs, parent_def_id); - let interpreter = PureFunctionBackwardInterpreter::new( + encode_mir( encoder, &mir, proc_def_id, pure_encoding_context, parent_def_id, + ) +} + +/// Used to encode unevaluated constants. +pub(super) fn encode_promoted<'p, 'v: 'p, 'tcx: 'v>( + encoder: &'p Encoder<'v, 'tcx>, + proc_def_id: ty::WithOptConstParam, + promoted_id: mir::Promoted, + parent_def_id: DefId, + substs: SubstsRef<'tcx>, +) -> SpannedEncodingResult { + let tcx = encoder.env().tcx(); + let promoted_bodies = tcx.promoted_mir_opt_const_arg(proc_def_id); + let param_env = tcx.param_env(parent_def_id); + let mir = tcx.subst_and_normalize_erasing_regions( + substs, + param_env, + promoted_bodies[promoted_id].clone(), + ); + encode_mir( + encoder, + &mir, + proc_def_id.did, + PureEncodingContext::Code, + parent_def_id, + ) +} + +/// Backing implementation for `encode_body` and `encode_promoted`. The extra +/// `mir` argument may be the MIR body identified by `proc_def_id` (when +/// encoding a regular function), or it may be the body of a promoted constant +/// (when encoding an unevaluated constant in the MIR). The latter does not +/// have a `DefId` of its own, it is identified by the `DefId` of its +/// containing function and a promoted ID. +fn encode_mir<'p, 'v: 'p, 'tcx: 'v>( + encoder: &'p Encoder<'v, 'tcx>, + mir: &mir::Body<'tcx>, + proc_def_id: DefId, + pure_encoding_context: PureEncodingContext, + parent_def_id: DefId, +) -> SpannedEncodingResult { + let interpreter = PureFunctionBackwardInterpreter::new( + encoder, + mir, + proc_def_id, + pure_encoding_context, + parent_def_id, ); let function_name = encoder.env().name.get_absolute_item_name(proc_def_id); debug!("Encode body of pure function {}", function_name); - let state = run_backward_interpretation(&mir, &interpreter)? + let state = run_backward_interpretation(mir, &interpreter)? .unwrap_or_else(|| panic!("Procedure {proc_def_id:?} contains a loop")); let body_expr = state.into_expr().unwrap(); debug!( diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs index 581b437024a..84f1be26cbc 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs @@ -10,7 +10,7 @@ use crate::encoder::{ use log::{debug, trace}; use prusti_common::config; use prusti_interface::data::ProcedureDefId; -use prusti_rustc_interface::middle::{ty, ty::subst::SubstsRef}; +use prusti_rustc_interface::middle::{mir, ty, ty::subst::SubstsRef}; use rustc_hash::{FxHashMap, FxHashSet}; use prusti_interface::specs::typed::ProcedureSpecificationKind; @@ -123,6 +123,11 @@ pub(crate) struct FunctionDescription<'tcx> { } pub(crate) trait PureFunctionEncoderInterface<'v, 'tcx> { + fn encode_uneval_const( + &self, + c: mir::UnevaluatedConst<'tcx>, + ) -> SpannedEncodingResult; + fn encode_pure_expression( &self, proc_def_id: ProcedureDefId, @@ -239,6 +244,18 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> Ok(self.pure_function_encoder_state.bodies_high.borrow()[&key].clone()) } + fn encode_uneval_const( + &self, + mir::UnevaluatedConst { + def, + substs, + promoted, + }: mir::UnevaluatedConst<'tcx>, + ) -> SpannedEncodingResult { + let promoted_id = promoted.expect("unevaluated const should have a promoted ID"); + super::encoder_poly::encode_promoted(self, def, promoted_id, def.did, substs) + } + // FIXME: This should be refactored to depend on encode_pure_expression_high // and moved to prusti-viper/src/encoder/high/pure_functions/interface.rs fn encode_pure_expression(