Skip to content

Commit 5cac744

Browse files
Aurel300Aurel300
committed
wip
1 parent f775cbb commit 5cac744

File tree

7 files changed

+215
-110
lines changed

7 files changed

+215
-110
lines changed

‎prusti-encoder/src/encoders/mir_builtin.rs‎

Lines changed: 100 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -4,14 +4,10 @@ use prusti_rustc_interface::{
44
};
55
use prusti_utils::config;
66
use task_encoder::{EncodeFullError, EncodeFullResult, TaskEncoder, TaskEncoderDependencies};
7-
use vir::{CallableIdn, CastType, FunctionIdn};
8-
9-
use crate::encoders::{ConstEnc, r#const::ConstEncTask, ty::{
10-
RustTyDecomposition,
11-
generics::{GParams, GenericParamsEnc},
12-
interpretation::float::FloatDomain,
13-
pure::{TyPurePrimData, TyPurePrimDataKind},
14-
use_pure::TyUsePureEnc,
7+
use vir::{CallableIdn, CastType, FunctionIdn, HasType, MethodIdn};
8+
9+
use crate::encoders::{ConstEnc, TyUseImpureEnc, r#const::ConstEncTask, ty::{
10+
RustTyDecomposition, TySpecifics, generics::{GParams, GenericParamsEnc}, interpretation::float::FloatDomain, pure::{TyPurePrimData, TyPurePrimDataKind}, use_pure::TyUsePureEnc
1511
}};
1612

1713
pub struct MirBuiltinEnc;
@@ -33,14 +29,14 @@ pub enum MirBuiltinEncTask<'tcx> {
3329

3430
#[derive(Copy, Clone, Debug)]
3531
pub enum MirBuiltinEncOutputRef<'vir> {
36-
Unsize(FunctionIdn<'vir, (vir::CSnap, vir::ManyTyVal, vir::ManyCSnap), vir::CSnap>),
32+
Unsize(MethodIdn<'vir, (vir::Ref, vir::Ref, vir::ManyTyVal, vir::ManyCSnap)>),
3733
Len(FunctionIdn<'vir, vir::CSnap, vir::CSnap>),
3834
UnOp(FunctionIdn<'vir, vir::CSnap, vir::CSnap>),
3935
BinOp(FunctionIdn<'vir, (vir::CSnap, vir::CSnap), vir::CSnap>),
4036
}
4137
impl<'vir> task_encoder::OutputRefAny for MirBuiltinEncOutputRef<'vir> {}
4238
impl<'vir> MirBuiltinEncOutputRef<'vir> {
43-
pub fn unsize(self) -> Option<FunctionIdn<'vir, (vir::CSnap, vir::ManyTyVal, vir::ManyCSnap), vir::CSnap>> {
39+
pub fn unsize(self) -> Option<MethodIdn<'vir, (vir::Ref, vir::Ref, vir::ManyTyVal, vir::ManyCSnap)>> {
4440
match self {
4541
MirBuiltinEncOutputRef::Unsize(idn) => Some(idn),
4642
_ => None,
@@ -71,7 +67,8 @@ impl<'vir> MirBuiltinEncOutputRef<'vir> {
7167

7268
#[derive(Clone, Debug)]
7369
pub struct MirBuiltinEncOutput<'vir> {
74-
pub function: vir::Function<'vir>,
70+
functions: Vec<vir::Function<'vir>>,
71+
methods: Vec<vir::Method<'vir>>,
7572
}
7673

7774
impl TaskEncoder for MirBuiltinEnc {
@@ -92,25 +89,28 @@ impl TaskEncoder for MirBuiltinEnc {
9289
task_key: &Self::TaskKey<'vir>,
9390
deps: &mut TaskEncoderDependencies<'vir, Self>,
9491
) -> EncodeFullResult<'vir, Self> {
95-
let function = vir::with_vcx(|vcx| match *task_key {
96-
MirBuiltinEncTask::Unsize(arg_ty, res_ty, def_id) => Self::handle_unsize(vcx, deps, *task_key, arg_ty, res_ty, def_id),
97-
MirBuiltinEncTask::Len(arg_ty) => Self::handle_len(vcx, deps, *task_key, arg_ty),
98-
MirBuiltinEncTask::UnOp(res_ty, op, operand_ty) => {
99-
Self::handle_un_op(vcx, deps, *task_key, op, operand_ty, res_ty)
100-
}
101-
MirBuiltinEncTask::BinOp(res_ty, op, l_ty, r_ty) => {
102-
Self::handle_bin_op(vcx, deps, *task_key, res_ty, op, l_ty, r_ty)
92+
vir::with_vcx(|vcx| {
93+
let mut functions = Vec::new();
94+
let mut methods = Vec::new();
95+
match *task_key {
96+
MirBuiltinEncTask::Unsize(arg_ty, res_ty, def_id) => methods.push(Self::handle_unsize(vcx, deps, *task_key, arg_ty, res_ty, def_id)?),
97+
MirBuiltinEncTask::Len(arg_ty) => functions.push(Self::handle_len(vcx, deps, *task_key, arg_ty)?),
98+
MirBuiltinEncTask::UnOp(res_ty, op, operand_ty) => functions.push(Self::handle_un_op(vcx, deps, *task_key, op, operand_ty, res_ty)?),
99+
MirBuiltinEncTask::BinOp(res_ty, op, l_ty, r_ty) => functions.push(Self::handle_bin_op(vcx, deps, *task_key, res_ty, op, l_ty, r_ty)?),
100+
MirBuiltinEncTask::CheckedBinOp(res_ty, op, l_ty, r_ty) => functions.push(Self::handle_checked_bin_op(vcx, deps, *task_key, res_ty, op, l_ty, r_ty)?),
103101
}
104-
MirBuiltinEncTask::CheckedBinOp(res_ty, op, l_ty, r_ty) => {
105-
Self::handle_checked_bin_op(vcx, deps, *task_key, res_ty, op, l_ty, r_ty)
106-
}
107-
})?;
108-
Ok((MirBuiltinEncOutput { function }, ()))
102+
Ok((MirBuiltinEncOutput { functions, methods, }, ()))
103+
})
109104
}
110105

111106
fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) {
112107
for output in Self::all_outputs_local_no_errors() {
113-
program.add_function(output.function);
108+
for function in output.functions {
109+
program.add_function(function);
110+
}
111+
for method in output.methods {
112+
program.add_method(method);
113+
}
114114
}
115115
}
116116
}
@@ -132,40 +132,54 @@ impl MirBuiltinEnc {
132132
vcx: &'vir vir::VirCtxt<'vir>,
133133
deps: &mut TaskEncoderDependencies<'vir, Self>,
134134
key: <Self as TaskEncoder>::TaskKey<'vir>,
135-
arg_ty: ty::Ty<'vir>,
136-
res_ty: ty::Ty<'vir>,
135+
src_ty: ty::Ty<'vir>,
136+
dst_ty: ty::Ty<'vir>,
137137
def_id: DefId,
138-
) -> Result<vir::Function<'vir>, EncodeFullError<'vir, Self>> {
139-
let name = vir::vir_format_identifier!(vcx, "mir_unsize_{arg_ty:?}_to_{res_ty:?}");
138+
) -> Result<vir::Method<'vir>, EncodeFullError<'vir, Self>> {
139+
let name = vir::vir_format_identifier!(vcx, "mir_unsize_{src_ty:?}_to_{dst_ty:?}");
140140

141141
let params = GParams::from(def_id);
142142
let generics = deps.require_dep::<GenericParamsEnc>(params)?;
143143

144-
let ty_task = RustTyDecomposition::from_ty(arg_ty.peel_refs(), vcx.tcx(), params);
145-
let arg_array_like = deps.require_dep::<TyUsePureEnc>(ty_task)?.expect_array();
146-
let ty_task = RustTyDecomposition::from_ty(arg_ty, vcx.tcx(), params);
147-
let arg_ty_out = deps.require_dep::<TyUsePureEnc>(ty_task)?;
148-
let arg_ref = arg_ty_out.expect_immref();
149-
150-
let ty_task = RustTyDecomposition::from_ty(res_ty.peel_refs(), vcx.tcx(), params);
151-
let res_array_like = deps.require_dep::<TyUsePureEnc>(ty_task)?.expect_array();
152-
let ty_task = RustTyDecomposition::from_ty(res_ty, vcx.tcx(), params);
153-
let res_ty_out = deps.require_dep::<TyUsePureEnc>(ty_task)?;
154-
let res_ref = res_ty_out.expect_immref();
155-
156-
let arg_ty_snap = arg_ty_out.snapshot.downcast_ty();
157-
let res_ty_snap = res_ty_out.snapshot.downcast_ty();
158-
let function = FunctionIdn::new(
144+
let ty_task = RustTyDecomposition::from_ty(src_ty.peel_refs(), vcx.tcx(), params);
145+
let src_array_pure = deps.require_dep::<TyUsePureEnc>(ty_task)?.expect_array();
146+
let src_array_impure = deps.require_dep::<TyUseImpureEnc>(ty_task)?;
147+
let ty_task = RustTyDecomposition::from_ty(src_ty, vcx.tcx(), params);
148+
let src_ref_pure = deps.require_dep::<TyUsePureEnc>(ty_task)?;
149+
let src_ref_impure = deps.require_dep::<TyUseImpureEnc>(ty_task)?;
150+
151+
let ty_task = RustTyDecomposition::from_ty(dst_ty.peel_refs(), vcx.tcx(), params);
152+
let dst_array_pure = deps.require_dep::<TyUsePureEnc>(ty_task)?.expect_array();
153+
let dst_array_impure = deps.require_dep::<TyUseImpureEnc>(ty_task)?;
154+
let ty_task = RustTyDecomposition::from_ty(dst_ty, vcx.tcx(), params);
155+
let dst_ref_pure = deps.require_dep::<TyUsePureEnc>(ty_task)?;
156+
let dst_ref_impure = deps.require_dep::<TyUseImpureEnc>(ty_task)?;
157+
158+
let ref_src_decl = vcx.mk_local_decl("src", vir::TYPE_REF);
159+
let ref_src_ex = vcx.mk_local_ex(ref_src_decl);
160+
let ref_dst_decl = vcx.mk_local_decl("dst", vir::TYPE_REF);
161+
let ref_dst_ex = vcx.mk_local_ex(ref_dst_decl);
162+
let method = MethodIdn::new(
159163
name,
160-
(arg_ty_snap, generics.ty_args(), generics.const_args()),
161-
res_ty_snap,
164+
(ref_src_decl.ty(), ref_dst_decl.ty(), generics.ty_args(), generics.const_args()),
162165
);
163-
deps.emit_output_ref(key, MirBuiltinEncOutputRef::Unsize(function))?;
164-
165-
let snap_arg_decl = vcx.mk_local_decl("arg", arg_ty_snap);
166-
let snap_arg_ex = vcx.mk_local_ex(snap_arg_decl);
167-
168-
let arg_len = match arg_ty.peel_refs().kind() {
166+
deps.emit_output_ref(key, MirBuiltinEncOutputRef::Unsize(method))?;
167+
168+
let snap_src = src_ref_impure.ref_to_snap(ref_src_ex);
169+
let snap_dst = dst_ref_impure.ref_to_snap(ref_dst_ex);
170+
171+
let src_value = match src_ref_pure.specifics {
172+
TySpecifics::ImmRef(data) => data.value_access(snap_src.downcast_ty()),
173+
TySpecifics::MutRef(data) => data.value_access(snap_src.downcast_ty()),
174+
_ => unreachable!(),
175+
}.downcast_ty();
176+
let dst_value = match dst_ref_pure.specifics {
177+
TySpecifics::ImmRef(data) => data.value_access(snap_dst.downcast_ty()),
178+
TySpecifics::MutRef(data) => data.value_access(snap_dst.downcast_ty()),
179+
_ => unreachable!(),
180+
}.downcast_ty();
181+
182+
let src_len = match src_ty.peel_refs().kind() {
169183
ty::TyKind::Array(_, len) => {
170184
let const_enc = deps.require_dep::<ConstEnc>(ConstEncTask::Ty {
171185
const_: *len,
@@ -176,21 +190,22 @@ impl MirBuiltinEnc {
176190
let usize_out = deps.require_dep::<TyUsePureEnc>(ty_task)?.expect_native();
177191
(usize_out.snap_to_prim)(const_enc).downcast_ty()
178192
}
179-
_ => arg_array_like.len(arg_ref.value_access(snap_arg_ex).downcast_ty()),
193+
_ => src_array_pure.len(src_value),
180194
};
181195

182-
let snap_res_ex = vcx.mk_result(res_ty_snap);
183-
Ok(vcx.mk_function(function, (snap_arg_decl, generics.ty_decls(), generics.const_decls()), &[], vcx.alloc_slice(&[
196+
Ok(vcx.mk_method(method, (ref_src_decl, ref_dst_decl, generics.ty_decls(), generics.const_decls()), &[], vcx.alloc_slice(&[
197+
src_ref_impure.ref_to_pred(vcx, ref_src_ex, None),
198+
src_array_impure.ref_to_pred(vcx, src_ref_impure.expect_mutref().deref(ref_src_ex), None),
199+
]), vcx.alloc_slice(&[
200+
dst_ref_impure.ref_to_pred(vcx, ref_dst_ex, None),
201+
dst_array_impure.ref_to_pred(vcx, dst_ref_impure.expect_mutref().deref(ref_dst_ex), None),
202+
vir::expr! { (src_len) == ([dst_array_pure.len(dst_value)]) },
184203
vir::expr! {
185-
(arg_len)
186-
== ([res_array_like.len(res_ref.value_access(snap_res_ex).downcast_ty())])
204+
forall idx: Int :: {[dst_array_pure.index(dst_value, idx)]}
205+
([dst_array_pure.index(dst_value, idx)])
206+
== (old([src_array_pure.index(src_value, idx)]))
187207
},
188-
vir::expr! {
189-
forall idx: Int :: {[res_array_like.index(res_ref.value_access(snap_res_ex).downcast_ty(), idx)]}
190-
([res_array_like.index(res_ref.value_access(snap_res_ex).downcast_ty(), idx)])
191-
== ([arg_array_like.index(arg_ref.value_access(snap_arg_ex).downcast_ty(), idx)])
192-
},
193-
]), None, None))
208+
]), None))
194209
}
195210

196211
fn handle_len<'vir>(
@@ -199,20 +214,23 @@ impl MirBuiltinEnc {
199214
key: <Self as TaskEncoder>::TaskKey<'vir>,
200215
arg_ty: ty::Ty<'vir>,
201216
) -> Result<vir::Function<'vir>, EncodeFullError<'vir, Self>> {
202-
let ty_task = RustTyDecomposition::from_prim_ty(arg_ty);
203-
let arg_ty = deps.require_dep::<TyUsePureEnc>(ty_task)?;
217+
let ty_task = RustTyDecomposition::from_ty(arg_ty, vcx.tcx(), GParams::empty()); // TODO: context ...
218+
let arg_ty_pure = deps.require_dep::<TyUsePureEnc>(ty_task)?;
204219

205220
let ty_task = RustTyDecomposition::from_prim_ty(vcx.tcx().types.usize);
206-
let res_ty = deps.require_dep::<TyUsePureEnc>(ty_task)?;
221+
let res_ty_pure = deps.require_dep::<TyUsePureEnc>(ty_task)?;
207222

208-
let name = vir::vir_format_identifier!(vcx, "mir_len"); // TODO: name (Slice or Array)
209-
let arg_ty_snap = arg_ty.snapshot.downcast_ty();
210-
let res_ty_snap = res_ty.snapshot.downcast_ty();
223+
let name = vir::vir_format_identifier!(vcx, "mir_len_{arg_ty:?}");
224+
let arg_ty_snap = arg_ty_pure.snapshot.downcast_ty();
225+
let res_ty_snap = res_ty_pure.snapshot.downcast_ty();
211226
let function = FunctionIdn::new(name, arg_ty_snap, res_ty_snap);
212227
deps.emit_output_ref(key, MirBuiltinEncOutputRef::Len(function))?;
213228

214229
let snap_arg_decl = vcx.mk_local_decl("arg", arg_ty_snap);
215-
Ok(vcx.mk_function(function, (snap_arg_decl,), &[], &[], None, None))
230+
let snap_arg_ex = vcx.mk_local_ex(snap_arg_decl);
231+
Ok(vcx.mk_function(function, (snap_arg_decl,), &[], &[], None, Some(
232+
(res_ty_pure.expect_primitive().prim_to_snap)(arg_ty_pure.expect_array().len(snap_arg_ex).upcast_ty()),
233+
)))
216234
}
217235

218236
fn handle_un_op<'vir>(
@@ -278,16 +296,21 @@ impl MirBuiltinEnc {
278296
let function = FunctionIdn::new(name, operand_ty_snap, res_ty_snap);
279297
deps.emit_output_ref(key, MirBuiltinEncOutputRef::UnOp(function))?;
280298

281-
let ref_ty_out = operand_ty_enc.expect_immref();
282-
let slice_ty_task = RustTyDecomposition::from_ty(operand_ty.peel_refs(), vcx.tcx(), GParams::empty());
283-
let slice_ty_out = deps.require_dep::<TyUsePureEnc>(slice_ty_task)?.expect_array();
299+
//let slice_ty_task = RustTyDecomposition::from_ty(operand_ty.peel_refs(), vcx.tcx(), GParams::empty());
300+
//let slice_ty_out = deps.require_dep::<TyUsePureEnc>(slice_ty_task)?.expect_array();
284301

285-
let snap_arg_decl = vcx.mk_local_decl("arg", operand_ty_snap);
302+
let snap_arg_decl = vcx.mk_local_decl("arg", operand_ty_snap);/*
286303
let snap_arg = vcx.mk_local_ex(snap_arg_decl);
287304
let prim_res_ty = res_ty_enc.expect_primitive();
288-
let val = (prim_res_ty.prim_to_snap)(slice_ty_out.len(ref_ty_out.value_access(snap_arg).downcast_ty()).upcast_ty());
289-
290-
Ok(vcx.mk_function(function, (snap_arg_decl,), &[], &[], None, Some(val)))
305+
let operand_value = match operand_ty_enc.specifics {
306+
TySpecifics::ImmRef(data) => data.value_access(snap_arg),
307+
TySpecifics::MutRef(data) => data.value_access(snap_arg),
308+
_ => unreachable!(),
309+
}.downcast_ty();
310+
let val = (prim_res_ty.prim_to_snap)(slice_ty_out.len(operand_value).upcast_ty());
311+
312+
Ok(vcx.mk_function(function, (snap_arg_decl,), &[], &[], None, Some(val)))*/
313+
Ok(vcx.mk_function(function, (snap_arg_decl,), &[], &[], None, None))
291314
}
292315
}
293316
}

0 commit comments

Comments
 (0)