Fix using assert_eq

prusti-contracts/prusti-contracts/src/core_spec/mod.rs

@@ -22,6 +22,18 @@ pub(super) mod type_eq {
 #[pure]
 fn panic(expr: &'static str) -> !;
 
+#[extern_spec(core::panicking)]
+#[requires(false)]
+pub fn assert_failed<T, U>(
+    kind: core::panicking::AssertKind,
+    left: &T,
+    right: &U,
+    args: Option<core::fmt::Arguments<'_>>,
+) -> !
+where
+    T: core::fmt::Debug + ?Sized,
+    U: core::fmt::Debug + ?Sized;
+
 #[extern_spec]
 impl<T> [T] {
     #[pure]

prusti-encoder/src/encoders/addr.rs

@@ -0,0 +1,49 @@
+use task_encoder::TaskEncoder;
+use vir::{Function, FunctionIdn, ViperIdent};
+
+/// Encodes the `Int` to `Ref` function to construct a reference from an address. In
+/// the future this will also likely include a second `Int` tag argument
+/// (from SB or TB) and inverse functions for both.
+pub struct RefDataEnc;
+
+#[derive(Debug, Clone)]
+pub struct RefData<'vir> {
+    pub addr_to_ref: vir::FunctionIdn<'vir, vir::Int, vir::Ref>,
+}
+
+#[derive(Debug, Clone)]
+pub struct RefDataLocal<'vir> {
+    addr_to_ref_fn: Function<'vir>,
+}
+
+impl TaskEncoder for RefDataEnc {
+    task_encoder::encoder_cache!(RefDataEnc);
+    type TaskDescription<'vir> = ();
+    type OutputFullLocal<'vir> = RefDataLocal<'vir>;
+    type OutputFullDependency<'vir> = RefData<'vir>;
+
+    type TaskKey<'vir> = Self::TaskDescription<'vir>;
+
+    fn task_to_key<'vir>(_task: &Self::TaskDescription<'vir>) -> Self::TaskKey<'vir> {}
+
+    fn do_encode_full<'vir>(
+        task_key: &Self::TaskKey<'vir>,
+        deps: &mut task_encoder::TaskEncoderDependencies<'vir, Self>,
+    ) -> task_encoder::EncodeFullResult<'vir, Self> {
+        deps.emit_output_ref(*task_key, ())?;
+        let addr_to_ref =
+            FunctionIdn::new(ViperIdent::new("addr_to_ref"), vir::TYPE_INT, vir::TYPE_REF);
+        let addr_to_ref_fn = vir::with_vcx(|vcx| {
+            let arg_decl = vcx.mk_local_decl("arg", vir::TYPE_INT);
+            vcx.mk_function(addr_to_ref, (arg_decl,), &[], &[], None, None)
+        });
+        Ok((RefDataLocal { addr_to_ref_fn }, RefData { addr_to_ref }))
+    }
+
+    fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) {
+        let outputs = RefDataEnc::all_outputs_local_no_errors();
+        for output in outputs {
+            program.add_function(output.addr_to_ref_fn);
+        }
+    }
+}

prusti-encoder/src/encoders/const.rs

@@ -1,5 +1,6 @@
-use prusti_interface::PrustiError;
 use prusti_rustc_interface::{
+    abi::HasDataLayout,
+    const_eval::interpret::AllocRange,
     middle::{
         mir::{
             self, ConstValue,
@@ -14,6 +15,7 @@ use vir::CastType;
 
 use crate::encoders::{
     MirPureEnc, MirPureEncTask, PureKind,
+    addr::RefDataEnc,
     ty::{
         RustTyDecomposition,
         generics::{GParams, GenericParamsEnc},
@@ -65,71 +67,105 @@ impl ConstEnc {
         }
     }
 
-    fn encode_const_val<'vir>(
+    fn encode_scalar<'vir>(
         deps: &mut TaskEncoderDependencies<'vir, Self>,
-        val: ConstValue,
+        val: Scalar,
         ty: ty::Ty<'vir>,
         context: GParams<'vir>,
-        span: Option<Span>,
     ) -> Result<vir::ExprCSnap<'vir>, EncodeFullError<'vir, Self>> {
+        let ty_task = RustTyDecomposition::from_ty(ty, context);
+        let kind = deps.require_dep::<TyUsePureEnc>(ty_task)?;
         vir::with_vcx(|vcx| {
-            let ty_task = RustTyDecomposition::from_ty(ty, context);
-            let kind = deps.require_dep::<TyUsePureEnc>(ty_task)?;
             Ok(match val {
-                ConstValue::Scalar(Scalar::Int(int)) => {
+                Scalar::Int(int) => {
+                    // TODO: Aggregates like structs will also show up as scalars
+                    // This means that the scalar doesn't contain all the data
+                    // and that it doesn't match the type of ty, which will lead
+                    // to a panic. We would have to encode these by looking at
+                    // the memory layout and iterating over the individual fields
                     let prim = kind.expect_primitive();
                     let val = int.to_bits(int.size());
                     let val = prim.expr_from_bits(ty, val);
                     (prim.prim_to_snap)(val)
                 }
-                ConstValue::Scalar(Scalar::Ptr(ptr, _)) => {
-                    match vcx.tcx().global_alloc(ptr.provenance.alloc_id()) {
-                        GlobalAlloc::Function { .. } => todo!(),
-                        GlobalAlloc::VTable(_, _) => todo!(),
-                        GlobalAlloc::Static(_) => todo!(),
-                        GlobalAlloc::Memory(_mem) => {
-                            // If the `unwrap` ever panics we need a different way to get the inner type
-                            // let inner_ty = ty.builtin_deref(true).map(|t| t.ty).unwrap_or(ty);
-                            let _inner_ty = ty.builtin_deref(true).unwrap();
-                            vcx.with_span(span.unwrap(), |vcx| {
-                                vcx.handle_error(
-                                    "application.precondition:assertion.false",
-                                    move |_| {
-                                        Some(vec![PrustiError::verification(
-                                            format!("unsupported const {val:?} might be reached"),
-                                            span.unwrap().into(),
-                                        )])
-                                    },
-                                );
-                                kind.unreachable_to_snap().downcast_ty()
-                            })
-                        }
-                        GlobalAlloc::TypeId { .. } => todo!(),
+                Scalar::Ptr(ptr, _) => match vcx.tcx().global_alloc(ptr.provenance.alloc_id()) {
+                    GlobalAlloc::Function { .. } => todo!(),
+                    GlobalAlloc::VTable(_, _) => todo!(),
+                    GlobalAlloc::Static(_) => todo!(),
+                    GlobalAlloc::Memory(mem) => {
+                        let (prov, offset) = ptr.prov_and_relative_offset();
+
+                        let inner_ty = ty.builtin_deref(true).unwrap();
+
+                        let size = if inner_ty.is_any_ptr() {
+                            vcx.tcx().data_layout().pointer_size()
+                        } else {
+                            mem.0.size()
+                        };
+
+                        // TODO: the unwrap can fail, e.g., for zero-sized types or empty strs/slices
+                        let bytes = mem
+                            .0
+                            .read_scalar(
+                                &vcx.tcx(),
+                                AllocRange {
+                                    start: offset,
+                                    size,
+                                },
+                                inner_ty.is_any_ptr(),
+                            )
+                            .unwrap();
+                        let alloc_id = prov.alloc_id().0;
+                        let rel_addr = ((alloc_id.get() as u128) << 64) | offset.bytes() as u128;
+
+                        let addr_to_ref = deps.require_dep::<RefDataEnc>(())?.addr_to_ref;
+                        kind.expect_immref().prim_to_snap(
+                            addr_to_ref(
+                                vcx.mk_const_expr(vir::ConstData::Int(rel_addr))
+                                    .downcast_ty(),
+                            ),
+                            Self::encode_scalar(deps, bytes, inner_ty, context)?.upcast_ty(),
+                        )
                     }
-                }
-                ConstValue::ZeroSized => {
-                    let s = kind.expect_structlike();
-                    s.field_snaps_to_snap(Vec::new())
-                }
-                // Encode `&str` constants to an opaque domain. If we ever want to perform string reasoning
-                // we will need to revisit this encoding, but for the moment this allows assertions to avoid
-                // crashing Prusti.
-                ConstValue::Slice { .. } if ty.peel_refs().is_str() => {
-                    let ref_ty = kind.expect_immref();
-                    let str_ty = ty.peel_refs();
-                    let str_ty_task = RustTyDecomposition::from_ty(str_ty, context);
-                    let str_snap = deps.require_dep::<TyUsePureEnc>(str_ty_task)?;
-                    let str_snap = str_snap.expect_opaque();
-                    // first, we create a string snapshot
-                    let snap = (str_snap.arbitrary)().upcast_ty();
-                    // wrap it in a ref
-                    vir::with_vcx(|vcx| ref_ty.prim_to_snap(vcx.mk_null(), snap))
-                }
-                ConstValue::Slice { .. } => todo!("ConstValue::Slice: {ty:?}"),
-                ConstValue::Indirect { .. } => todo!("ConstValue::Indirect"),
+                    GlobalAlloc::TypeId { .. } => todo!(),
+                },
             })
         })
     }
+
+    fn encode_const_val<'vir>(
+        deps: &mut TaskEncoderDependencies<'vir, Self>,
+        val: ConstValue,
+        ty: ty::Ty<'vir>,
+        context: GParams<'vir>,
+        _span: Option<Span>,
+    ) -> Result<vir::ExprCSnap<'vir>, EncodeFullError<'vir, Self>> {
+        let ty_task = RustTyDecomposition::from_ty(ty, context);
+        let kind = deps.require_dep::<TyUsePureEnc>(ty_task)?;
+        Ok(match val {
+            ConstValue::Scalar(scalar) => Self::encode_scalar(deps, scalar, ty, context)?,
+            ConstValue::ZeroSized => {
+                let s = kind.expect_structlike();
+                s.field_snaps_to_snap(Vec::new())
+            }
+            // Encode `&str` constants to an opaque domain. If we ever want to perform string reasoning
+            // we will need to revisit this encoding, but for the moment this allows assertions to avoid
+            // crashing Prusti.
+            ConstValue::Slice { .. } if ty.peel_refs().is_str() => {
+                let ref_ty = kind.expect_immref();
+                let str_ty = ty.peel_refs();
+                let str_ty_task = RustTyDecomposition::from_ty(str_ty, context);
+                let str_snap = deps.require_dep::<TyUsePureEnc>(str_ty_task)?;
+                let str_snap = str_snap.expect_opaque();
+                // first, we create a string snapshot
+                let snap = (str_snap.arbitrary)().upcast_ty();
+                // wrap it in a ref
+                vir::with_vcx(|vcx| ref_ty.prim_to_snap(vcx.mk_null(), snap))
+            }
+            ConstValue::Slice { .. } => todo!("ConstValue::Slice: {ty:?}"),
+            ConstValue::Indirect { .. } => todo!("ConstValue::Indirect"),
+        })
+    }
 }
 
 impl TaskEncoder for ConstEnc {

prusti-encoder/src/encoders/mod.rs

@@ -12,6 +12,7 @@ pub mod impure;
 /// Encoders for Rust functions (pure and impure)
 pub mod mir_fn;
 pub mod custom;
+pub mod addr;
 
 pub use r#const::ConstEnc;
 pub use impure::fn_wand::{WandEnc, WandEncOutput, WandEncTask};

prusti-encoder/src/lib.rs

@@ -20,6 +20,7 @@ use task_encoder::TaskEncoder;
 
 use crate::encoders::{
     Impure, Pure,
+    addr::RefDataEnc,
     custom::PairUseEnc,
     ty::{
         generics::{GArgsCastEnc, trait_impls::TraitImplEnc, traits::TraitEnc},
@@ -106,6 +107,7 @@ pub fn test_entrypoint<'tcx>(
     PairUseEnc::emit_outputs(&mut program);
     TraitEnc::emit_outputs(&mut program);
     TraitImplEnc::emit_outputs(&mut program);
+    RefDataEnc::emit_outputs(&mut program);
 
     if std::env::var("LOCAL_TESTING").is_ok() {
         std::fs::write("local-testing/simple.vpr", program.code()).unwrap();

prusti-rustc-interface/src/lib.rs

@@ -31,3 +31,5 @@ pub extern crate rustc_hir as hir;
 pub extern crate rustc_middle as middle;
 pub extern crate rustc_mir_dataflow as dataflow;
 pub extern crate rustc_trait_selection as trait_selection;
+
+pub extern crate rustc_const_eval as const_eval;

prusti-tests/tests/verify/fail/no-annotations/assert-eq.rs

@@ -0,0 +1,9 @@
+fn fail() {
+    assert_eq!(1, 8);
+}
+
+fn fail2() {
+    let x = 5;
+    let y = 4 - 1;
+    assert_eq!(x, y);
+}

prusti-tests/tests/verify/pass/no-annotations/assert-eq.rs

@@ -0,0 +1,9 @@
+fn pass() {
+    assert_eq!(1, 1);
+}
+
+fn pass2() {
+    let x = 5;
+    let y = 4 + 1;
+    assert_eq!(x, y);
+}