Skip to content

Array encoding #69

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Aurel300 wants to merge 10 commits into from
Closed

Array encoding #69

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
3f9732c
create arrays
Aurel300 Apr 25, 2025
9eecb6e
tidy domain encoder
Aurel300 May 16, 2025
654cebf
MIR len builtin
Aurel300 May 8, 2025
c69b144
tidy predicate encoder
Aurel300 May 8, 2025
cb29716
array index fold/unfold
Aurel300 May 16, 2025
2f8b50e
vir macros fixup
Aurel300 May 17, 2025
c277bb2
index in MIR pure
Aurel300 May 21, 2025
3fe08aa
update test
Aurel300 May 21, 2025
bc12d02
fixup index in MIR pure
Aurel300 May 21, 2025
11588da
wip const generics
Aurel300 Jun 13, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions prusti-encoder/src/encoder_traits/pure_function_enc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ use crate::encoders::{
domain::DomainEnc,
lifted::{
func_def_ty_params::LiftedTyParamsEnc,
ty::{EncodeGenericsAsLifted, LiftedTy, LiftedTyEnc},
ty::{EncodeGenericsAsLifted, LiftedTy, LiftedTyEnc, LiftedTyEncTask},
},
most_generic_ty::extract_type_params,
GenericEnc, MirLocalDefEnc, MirPureEnc, MirPureEncTask, MirSpecEnc, PureKind,
Expand Down Expand Up @@ -60,7 +60,7 @@ where
ty: Ty<'vir>,
) -> Option<ExprGen<'vir, Curr, Next>> {
let lifted_ty = deps
.require_local::<LiftedTyEnc<EncodeGenericsAsLifted>>(ty)
.require_local::<LiftedTyEnc<EncodeGenericsAsLifted>>(LiftedTyEncTask::Ty(ty))
.unwrap();
match lifted_ty {
LiftedTy::Generic(generic) => {
Expand Down
168 changes: 96 additions & 72 deletions prusti-encoder/src/encoders/const.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,22 @@ use prusti_rustc_interface::{
use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies};
use vir::{Arity, CallableIdent};

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub enum ConstEncTask<'vir> {
Mir {
const_: mir::Const<'vir>,
encoding_depth: usize, // current encoding depth
def_id: DefId, // DefId of the current function
},
}

/// Encodes constants into snapshot expressions. The evaluation of a constant
/// is assumed to be side-effect free, as enforced by the compiler. This encoder
/// handles two different kinds of constants: ones coming from the MIR and ones
/// coming from the type system.
///
/// See "Representing constants" in the rustc dev guide for an overview:
/// https://rustc-dev-guide.rust-lang.org/mir/index.html#representing-constants
pub struct ConstEnc;

use crate::encoders::{mir_pure::PureKind, MirPureEnc, MirPureEncTask};
Expand All @@ -24,11 +40,7 @@ use super::{
impl TaskEncoder for ConstEnc {
task_encoder::encoder_cache!(ConstEnc);

type TaskDescription<'vir> = (
mir::Const<'vir>,
usize, // current encoding depth
DefId, // DefId of the current function
);
type TaskDescription<'vir> = ConstEncTask<'vir>;
type OutputFullLocal<'vir> = vir::Expr<'vir>;
type EncodingError = ();

Expand All @@ -41,78 +53,90 @@ impl TaskEncoder for ConstEnc {
deps: &mut TaskEncoderDependencies<'vir, Self>,
) -> EncodeFullResult<'vir, Self> {
deps.emit_output_ref(*task_key, ())?;
let (const_, encoding_depth, def_id) = *task_key;
let res = match const_ {
mir::Const::Val(val, ty) => {
let kind = deps
.require_local::<RustTySnapshotsEnc>(ty)?
.generic_snapshot
.specifics;
match val {
ConstValue::Scalar(Scalar::Int(int)) => {
let prim = kind.expect_primitive();
let val = int.to_bits(int.size());
let val = prim.expr_from_bits(ty, val);
vir::with_vcx(|vcx| prim.prim_to_snap.apply(vcx, [val]))
}
ConstValue::Scalar(Scalar::Ptr(ptr, _)) => vir::with_vcx(|vcx| {
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();
todo!()
match *task_key {
ConstEncTask::Mir { const_, encoding_depth, def_id } => {
let res = match const_ {
mir::Const::Val(val, ty) => {
let kind = deps
.require_local::<RustTySnapshotsEnc>(ty)?
.generic_snapshot
.specifics;
match val {
ConstValue::Scalar(Scalar::Int(int)) => {
let prim = kind.expect_primitive();
let val = int.to_bits(int.size());
let val = prim.expr_from_bits(ty, val);
vir::with_vcx(|vcx| prim.prim_to_snap.apply(vcx, [val]))
}
ConstValue::Scalar(Scalar::Ptr(ptr, _)) => vir::with_vcx(|vcx| {
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();
todo!()
}
}
}),
ConstValue::ZeroSized => {
let s = kind.expect_structlike();
assert_eq!(s.field_snaps_to_snap.arity().args().len(), 0);
vir::with_vcx(|vcx| s.field_snaps_to_snap.apply(vcx, &[]))
}
// 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_snap = deps
.require_local::<RustTySnapshotsEnc>(str_ty)?
.generic_snapshot
.specifics
.expect_structlike();
let cast = deps.require_local::<RustTyCastersEnc<CastTypePure>>(str_ty)?;
vir::with_vcx(|vcx| {
// first, we create a string snapshot
let snap = str_snap.field_snaps_to_snap.apply(vcx, &[]);
// upcast it to a param
let snap = cast.cast_to_generic_if_necessary(vcx, snap);
// wrap it in a ref
ref_ty.prim_to_snap.apply(vcx, [vcx.mk_null(), snap])
})
}
ConstValue::Slice { .. } => todo!("ConstValue::Slice : {:?}", const_.ty()),
ConstValue::Indirect { .. } => todo!("ConstValue::Indirect"),
}
}),
ConstValue::ZeroSized => {
let s = kind.expect_structlike();
assert_eq!(s.field_snaps_to_snap.arity().args().len(), 0);
vir::with_vcx(|vcx| s.field_snaps_to_snap.apply(vcx, &[]))
}
// 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_snap = deps
.require_local::<RustTySnapshotsEnc>(str_ty)?
mir::Const::Unevaluated(uneval, _) => vir::with_vcx(|vcx| {
let task = MirPureEncTask {
encoding_depth: encoding_depth + 1,
parent_def_id: uneval.def,
param_env: vcx.tcx().param_env(uneval.def),
substs: ty::List::identity_for_item(vcx.tcx(), uneval.def),
kind: PureKind::Constant(uneval.promoted.unwrap()),
caller_def_id: Some(def_id),
};
let expr = deps.require_local::<MirPureEnc>(task)?.expr;
use vir::Reify;
Ok(expr.reify(vcx, (uneval.def, &[])))
})?,
mir::Const::Ty(_, _) => vir::with_vcx(|vcx| {
deps
.require_local::<RustTySnapshotsEnc>(vcx.tcx().mk_ty_from_kind(ty::TyKind::Uint(ty::UintTy::Usize)))
.unwrap()
.generic_snapshot
.specifics
.expect_structlike();
let cast = deps.require_local::<RustTyCastersEnc<CastTypePure>>(str_ty)?;
vir::with_vcx(|vcx| {
// first, we create a string snapshot
let snap = str_snap.field_snaps_to_snap.apply(vcx, &[]);
// upcast it to a param
let snap = cast.cast_to_generic_if_necessary(vcx, snap);
// wrap it in a ref
ref_ty.prim_to_snap.apply(vcx, [vcx.mk_null(), snap])
})
}
ConstValue::Slice { .. } => todo!("ConstValue::Slice : {:?}", const_.ty()),
ConstValue::Indirect { .. } => todo!("ConstValue::Indirect"),
}
}
mir::Const::Unevaluated(uneval, _) => vir::with_vcx(|vcx| {
let task = MirPureEncTask {
encoding_depth: encoding_depth + 1,
parent_def_id: uneval.def,
param_env: vcx.tcx().param_env(uneval.def),
substs: ty::List::identity_for_item(vcx.tcx(), uneval.def),
kind: PureKind::Constant(uneval.promoted.unwrap()),
caller_def_id: Some(def_id),
.expect_primitive()
.prim_to_snap.apply(vcx, [vcx.mk_uint::<0>()]) // TODO
}),
};
let expr = deps.require_local::<MirPureEnc>(task)?.expr;
use vir::Reify;
Ok(expr.reify(vcx, (uneval.def, &[])))
})?,
mir::Const::Ty(_, _) => todo!("ConstantKind::Ty"),
};
Ok((res, ()))
Ok((res, ()))
}
//_ => todo!(),
}
}
}
49 changes: 40 additions & 9 deletions prusti-encoder/src/encoders/generic.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,28 @@
use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies};
use prusti_rustc_interface::{
middle::ty::{self, TyKind},
span::symbol,
};
use task_encoder::{EncodeFullError, EncodeFullResult, TaskEncoder, TaskEncoderDependencies};
use vir::{
BinaryArity, CallableIdent, DomainIdent, DomainParamData, FunctionIdent, KnownArityAny,
NullaryArity, PredicateIdent, TypeData, UnaryArity, ViperIdent,
};

use super::rust_ty_predicates::RustTyPredicatesEnc;

pub fn generic_enc_ref<'vir, E: TaskEncoder>(
deps: &mut TaskEncoderDependencies<'vir, E>,
) -> Result<GenericEncOutputRef<'vir>, EncodeFullError<'vir, E>> {
vir::with_vcx(|vcx| {
let ty_param = vcx.tcx().mk_ty_from_kind(TyKind::Param(ty::ParamTy {
index: 0u32,
name: symbol::Symbol::intern("T"),
}));
deps.require_ref::<RustTyPredicatesEnc>(ty_param)
})?;
deps.require_ref::<GenericEnc>(())
}

pub struct GenericEnc;

#[derive(Clone, Debug)]
Expand All @@ -21,6 +40,8 @@ pub struct GenericEncOutputRef<'vir> {
pub unreachable_to_snap: FunctionIdent<'vir, NullaryArity<'vir>>,
// pub domain_type_name: DomainIdent<'vir, KnownArityAny<'vir, DomainParamData<'vir>, 0>>,
pub domain_param_name: DomainIdent<'vir, KnownArityAny<'vir, DomainParamData<'vir>, 0>>,
pub const_type_function: vir::FunctionIdent<'vir, UnaryArity<'vir>>,
pub const_value_function: vir::FunctionIdent<'vir, UnaryArity<'vir>>,
}
impl<'vir> task_encoder::OutputRefAny for GenericEncOutputRef<'vir> {}

Expand Down Expand Up @@ -78,6 +99,17 @@ impl TaskEncoder for GenericEnc {
&TYP_DOMAIN,
);

let const_type_function = FunctionIdent::new(
ViperIdent::new("const_typ"),
UnaryArity::new(&[&SNAPSHOT_PARAM_DOMAIN]),
&TYP_DOMAIN,
);
let const_value_function = FunctionIdent::new(
ViperIdent::new("const_val"),
UnaryArity::new(&[&TYP_DOMAIN]),
&SNAPSHOT_PARAM_DOMAIN,
);

let output_ref = GenericEncOutputRef {
type_snapshot: &TYP_DOMAIN,
param_snapshot: &SNAPSHOT_PARAM_DOMAIN,
Expand All @@ -87,17 +119,13 @@ impl TaskEncoder for GenericEnc {
ref_to_snap,
unreachable_to_snap,
param_type_function,
const_type_function,
const_value_function,
};

#[allow(clippy::unit_arg)]
deps.emit_output_ref(*task_key, output_ref)?;

let typ = FunctionIdent::new(
ViperIdent::new("typ"),
UnaryArity::new(&[&SNAPSHOT_PARAM_DOMAIN]),
&TYP_DOMAIN,
);

vir::with_vcx(|vcx| {
let t = vcx.mk_local_ex("t", &TYP_DOMAIN);
let ref_to_snap = vcx.mk_function(
Expand All @@ -111,7 +139,7 @@ impl TaskEncoder for GenericEnc {
))]),
vcx.alloc_slice(&[vcx.mk_bin_op_expr(
vir::BinOpKind::CmpEq,
typ.apply(vcx, [vcx.mk_result(&SNAPSHOT_PARAM_DOMAIN)]),
param_type_function.apply(vcx, [vcx.mk_result(&SNAPSHOT_PARAM_DOMAIN)]),
t,
)]),
None,
Expand All @@ -125,7 +153,10 @@ impl TaskEncoder for GenericEnc {
Ok((
GenericEncOutput {
param_snapshot: vir::vir_domain! { vcx; domain s_Param {
function typ(s_Param): Type;
function param_type_function(s_Param): Type;
function const_type_function(s_Param): Type;
function const_value_function(Type): s_Param;
axiom_inverse(const_value_function, const_type_function, s_Param);
}
},
ref_to_pred: vir::vir_predicate! { vcx; predicate p_Param(self_p: Ref, t: Type) },
Expand Down
59 changes: 46 additions & 13 deletions prusti-encoder/src/encoders/mir_builtin.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ pub enum MirBuiltinEncError {
#[derive(Clone, Copy, Debug, Hash, PartialEq, Eq)]
#[allow(clippy::enum_variant_names)]
pub enum MirBuiltinEncTask<'tcx> {
Len(ty::Ty<'tcx>),
UnOp(ty::Ty<'tcx>, mir::UnOp, ty::Ty<'tcx>),
BinOp(ty::Ty<'tcx>, mir::BinOp, ty::Ty<'tcx>, ty::Ty<'tcx>),
CheckedBinOp(ty::Ty<'tcx>, mir::BinOp, ty::Ty<'tcx>, ty::Ty<'tcx>),
Expand Down Expand Up @@ -53,22 +54,16 @@ impl TaskEncoder for MirBuiltinEnc {
task_key: &Self::TaskKey<'vir>,
deps: &mut TaskEncoderDependencies<'vir, Self>,
) -> EncodeFullResult<'vir, Self> {
vir::with_vcx(|vcx| match *task_key {
let function = vir::with_vcx(|vcx| match *task_key {
MirBuiltinEncTask::Len(e_ty) => Self::handle_len(vcx, deps, *task_key, e_ty),
MirBuiltinEncTask::UnOp(res_ty, op, operand_ty) => {
assert_eq!(res_ty, operand_ty);
let function = Self::handle_un_op(vcx, deps, *task_key, op, operand_ty)?;
Ok((MirBuiltinEncOutput { function }, ()))
Self::handle_un_op(vcx, deps, *task_key, op, operand_ty)
}
MirBuiltinEncTask::BinOp(res_ty, op, l_ty, r_ty) => {
let function = Self::handle_bin_op(vcx, deps, *task_key, res_ty, op, l_ty, r_ty)?;
Ok((MirBuiltinEncOutput { function }, ()))
}
MirBuiltinEncTask::CheckedBinOp(res_ty, op, l_ty, r_ty) => {
let function =
Self::handle_checked_bin_op(vcx, deps, *task_key, res_ty, op, l_ty, r_ty)?;
Ok((MirBuiltinEncOutput { function }, ()))
}
})
MirBuiltinEncTask::BinOp(res_ty, op, l_ty, r_ty) => Self::handle_bin_op(vcx, deps, *task_key, res_ty, op, l_ty, r_ty),
MirBuiltinEncTask::CheckedBinOp(res_ty, op, l_ty, r_ty) => Self::handle_checked_bin_op(vcx, deps, *task_key, res_ty, op, l_ty, r_ty),
})?;
Ok((MirBuiltinEncOutput { function }, ()))
}
}

Expand All @@ -83,6 +78,44 @@ fn int_name(ty: ty::Ty<'_>) -> &'static str {
}

impl MirBuiltinEnc {
fn handle_len<'vir>(
vcx: &'vir vir::VirCtxt<'vir>,
deps: &mut TaskEncoderDependencies<'vir, Self>,
key: <Self as TaskEncoder>::TaskKey<'vir>,
arg_ty: ty::Ty<'vir>,
) -> Result<vir::Function<'vir>, EncodeFullError<'vir, Self>> {
let res_ty = vcx.tcx().mk_ty_from_kind(ty::TyKind::Uint(ty::UintTy::Usize));
let arg_ty_enc = deps
.require_local::<RustTySnapshotsEnc>(arg_ty)?
.generic_snapshot;
let res_ty_enc = deps
.require_local::<RustTySnapshotsEnc>(res_ty)?
.generic_snapshot;

let name = vir::vir_format_identifier!(vcx, "mir_len"); // TODO: name (Slice or Array)
let arity = UnknownArity::new(vcx.alloc_slice(&[arg_ty_enc.snapshot]));
let function = FunctionIdent::new(name, arity, res_ty_enc.snapshot);
deps.emit_output_ref(key, MirBuiltinEncOutputRef { function })?;

let prim_arg_ty = arg_ty_enc.specifics.expect_array();
let prim_res_ty = res_ty_enc.specifics.expect_primitive();
let snap_arg = vcx.mk_local_ex("arg", arg_ty_enc.snapshot);
let prim_arg = prim_arg_ty.snap_to_prim.apply(vcx, [snap_arg]);
let val = prim_res_ty.prim_to_snap.apply(
vcx,
[vcx.mk_unary_op_expr(vir::UnOpKind::SeqLen, prim_arg)],
);

Ok(vcx.mk_function(
name.to_str(),
vcx.alloc_slice(&[vcx.mk_local_decl("arg", arg_ty_enc.snapshot)]),
res_ty_enc.snapshot,
&[],
&[],
Some(val),
))
}

fn handle_un_op<'vir>(
vcx: &'vir vir::VirCtxt<'vir>,
deps: &mut TaskEncoderDependencies<'vir, Self>,
Expand Down
Loading
Loading