support unevaluated constants in specs (fix #1268)

Author: Aurel300

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);
+}

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)),
+            },
         }
     }
 

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<DefId>,
+    promoted_id: mir::Promoted,
+    parent_def_id: DefId,
+    substs: SubstsRef<'tcx>,
+) -> SpannedEncodingResult<vir::Expr> {
+    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<vir::Expr> {
+    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!(

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<vir_poly::Expr>;
+
     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<vir_poly::Expr> {
+        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(