Add tests and implement support for alloc consts

Author: ThomasMayerl

prusti-encoder/src/encoders/addr.rs

@@ -0,0 +1,53 @@
+use task_encoder::TaskEncoder;
+use vir::{Function, FunctionIdn, ViperIdent};
+
+pub struct AddrUseEnc;
+
+#[derive(Debug, Clone)]
+pub struct AddrUse<'vir> {
+    pub ref_from_addr: vir::FunctionIdn<'vir, vir::Int, vir::Ref>,
+}
+
+#[derive(Debug, Clone)]
+pub struct AddrLocal<'vir> {
+    pub ref_from_addr: Function<'vir>,
+}
+
+impl TaskEncoder for AddrUseEnc {
+    task_encoder::encoder_cache!(AddrUseEnc);
+    type TaskDescription<'vir> = ();
+    type OutputFullLocal<'vir> = AddrLocal<'vir>;
+    type OutputFullDependency<'vir> = AddrUse<'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> {
+        let ref_from_addr = FunctionIdn::new(
+            ViperIdent::new("ref_from_addr"),
+            vir::TYPE_INT,
+            vir::TYPE_REF,
+        );
+        deps.emit_output_ref(*task_key, ())?;
+        Ok((
+            AddrLocal {
+                ref_from_addr: vir::with_vcx(|vcx| {
+                    let arg_decl = vcx.mk_local_decl("arg", vir::TYPE_INT);
+                    vcx.mk_function(ref_from_addr, (arg_decl,), &[], &[], None, None)
+                }),
+            },
+            AddrUse { ref_from_addr },
+        ))
+    }
+
+    fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) {
+        let outputs = AddrUseEnc::all_outputs_local_no_errors();
+        for output in outputs {
+            program.add_function(output.ref_from_addr);
+        }
+    }
+}

prusti-encoder/src/encoders/const.rs

@@ -1,5 +1,5 @@
-use prusti_interface::PrustiError;
 use prusti_rustc_interface::{
+    const_eval::interpret::AllocRange,
     middle::{
         mir::{
             self, ConstValue,
@@ -14,6 +14,7 @@ use vir::CastType;
 
 use crate::encoders::{
     MirPureEnc, MirPureEncTask, PureKind,
+    addr::AddrUseEnc,
     ty::{
         RustTyDecomposition,
         generics::{GParams, GenericParamsEnc},
@@ -70,7 +71,7 @@ impl ConstEnc {
         val: ConstValue,
         ty: ty::Ty<'vir>,
         context: GParams<'vir>,
-        span: Option<Span>,
+        _span: Option<Span>,
     ) -> Result<vir::ExprCSnap<'vir>, EncodeFullError<'vir, Self>> {
         vir::with_vcx(|vcx| {
             let ty_task = RustTyDecomposition::from_ty(ty, vcx.tcx(), context);
@@ -87,22 +88,41 @@ impl ConstEnc {
                         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(),
-                                        )])
+                        GlobalAlloc::Memory(mem) => {
+                            let inner_ty = ty.builtin_deref(true).unwrap();
+                            let inner_ty_task =
+                                RustTyDecomposition::from_ty(inner_ty, vcx.tcx(), context);
+                            let inner_kind = deps
+                                .require_dep::<TyUsePureEnc>(inner_ty_task)?
+                                .expect_primitive();
+                            let bytes = mem
+                                .0
+                                .0
+                                .read_scalar(
+                                    &vcx.tcx(),
+                                    AllocRange {
+                                        start: ptr.prov_and_relative_offset().1,
+                                        size: mem.0.0.size(),
                                     },
-                                );
-                                kind.unreachable_to_snap().downcast_ty()
-                            })
+                                    false,
+                                )
+                                .unwrap();
+                            let addr_to_ref = deps.require_dep::<AddrUseEnc>(())?.ref_from_addr;
+                            let (prov, offset) = ptr.prov_and_relative_offset();
+                            let alloc_id = prov.alloc_id().0;
+                            let rel_addr =
+                                ((alloc_id.get() as u128) << 64) | offset.bytes() as u128;
+
+                            kind.expect_immref().prim_to_snap(
+                                (addr_to_ref)(
+                                    vcx.mk_const_expr(vir::ConstData::Int(rel_addr))
+                                        .downcast_ty(),
+                                ),
+                                ((inner_kind.prim_to_snap)(vcx.mk_const_expr(
+                                    vir::ConstData::Int(bytes.to_bits(mem.0.0.size()).unwrap()),
+                                )))
+                                .upcast_ty(),
+                            )
                         }
                         GlobalAlloc::TypeId { .. } => todo!(),
                     }

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