Skip to content
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

Run Rustfmt #23

Closed
wants to merge 1 commit into from
Closed

Run Rustfmt #23

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
87 changes: 48 additions & 39 deletions prusti-encoder/src/encoders/generic.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
use task_encoder::{
TaskEncoder,
TaskEncoderDependencies,
};
use vir::{FunctionIdent, CallableIdent, NullaryArity};
use task_encoder::{TaskEncoder, TaskEncoderDependencies};
use vir::{CallableIdent, FunctionIdent, NullaryArity};

pub struct GenericEncoder;

Expand Down Expand Up @@ -40,7 +37,8 @@ impl TaskEncoder for GenericEncoder {
type EncodingError = GenericEncoderError;

fn with_cache<'tcx: 'vir, 'vir, F, R>(f: F) -> R
where F: FnOnce(&'vir task_encoder::CacheRef<'tcx, 'vir, GenericEncoder>) -> R,
where
F: FnOnce(&'vir task_encoder::CacheRef<'tcx, 'vir, GenericEncoder>) -> R,
{
CACHE.with(|cache| {
// SAFETY: the 'vir and 'tcx given to this function will always be
Expand All @@ -59,18 +57,24 @@ impl TaskEncoder for GenericEncoder {
fn do_encode_full<'tcx: 'vir, 'vir>(
task_key: &Self::TaskKey<'tcx>,
deps: &mut TaskEncoderDependencies<'vir>,
) -> Result<(
Self::OutputFullLocal<'vir>,
Self::OutputFullDependency<'vir>,
), (
Self::EncodingError,
Option<Self::OutputFullDependency<'vir>>,
)> {
deps.emit_output_ref::<Self>(*task_key, GenericEncoderOutputRef {
snapshot_param_name: "s_Param",
predicate_param_name: "p_Param",
domain_type_name: "s_Type",
});
) -> Result<
(
Self::OutputFullLocal<'vir>,
Self::OutputFullDependency<'vir>,
),
(
Self::EncodingError,
Option<Self::OutputFullDependency<'vir>>,
),
> {
deps.emit_output_ref::<Self>(
*task_key,
GenericEncoderOutputRef {
snapshot_param_name: "s_Param",
predicate_param_name: "p_Param",
domain_type_name: "s_Type",
},
);
let s_Type_Bool = FunctionIdent::new("s_Type_Bool", NullaryArity::new([]));
let s_Type_Int_isize = FunctionIdent::new("s_Type_Int_isize", NullaryArity::new([]));
let s_Type_Int_i8 = FunctionIdent::new("s_Type_Int_i8", NullaryArity::new([]));
Expand All @@ -84,26 +88,31 @@ impl TaskEncoder for GenericEncoder {
let s_Type_Uint_u32 = FunctionIdent::new("s_Type_Uint_u32", NullaryArity::new([]));
let s_Type_Uint_u64 = FunctionIdent::new("s_Type_Uint_u64", NullaryArity::new([]));
let s_Type_Uint_u128 = FunctionIdent::new("s_Type_Uint_u128", NullaryArity::new([]));
vir::with_vcx(|vcx| Ok((GenericEncoderOutput {
snapshot_param: vir::vir_domain! { vcx; domain s_Param {} },
predicate_param: vir::vir_predicate! { vcx; predicate p_Param(self_p: Ref/*, self_s: s_Param*/) },
domain_type: vir::vir_domain! { vcx; domain s_Type {
// TODO: only emit these when the types are actually used?
// emit instead from type encoder, to be consistent with the ADT case?
unique function s_Type_Bool(): s_Type;
unique function s_Type_Int_isize(): s_Type;
unique function s_Type_Int_i8(): s_Type;
unique function s_Type_Int_i16(): s_Type;
unique function s_Type_Int_i32(): s_Type;
unique function s_Type_Int_i64(): s_Type;
unique function s_Type_Int_i128(): s_Type;
unique function s_Type_Uint_usize(): s_Type;
unique function s_Type_Uint_u8(): s_Type;
unique function s_Type_Uint_u16(): s_Type;
unique function s_Type_Uint_u32(): s_Type;
unique function s_Type_Uint_u64(): s_Type;
unique function s_Type_Uint_u128(): s_Type;
} },
}, ())))
vir::with_vcx(|vcx| {
Ok((
GenericEncoderOutput {
snapshot_param: vir::vir_domain! { vcx; domain s_Param {} },
predicate_param: vir::vir_predicate! { vcx; predicate p_Param(self_p: Ref/*, self_s: s_Param*/) },
domain_type: vir::vir_domain! { vcx; domain s_Type {
// TODO: only emit these when the types are actually used?
// emit instead from type encoder, to be consistent with the ADT case?
unique function s_Type_Bool(): s_Type;
unique function s_Type_Int_isize(): s_Type;
unique function s_Type_Int_i8(): s_Type;
unique function s_Type_Int_i16(): s_Type;
unique function s_Type_Int_i32(): s_Type;
unique function s_Type_Int_i64(): s_Type;
unique function s_Type_Int_i128(): s_Type;
unique function s_Type_Uint_usize(): s_Type;
unique function s_Type_Uint_u8(): s_Type;
unique function s_Type_Uint_u16(): s_Type;
unique function s_Type_Uint_u32(): s_Type;
unique function s_Type_Uint_u64(): s_Type;
unique function s_Type_Uint_u128(): s_Type;
} },
},
(),
))
})
}
}
72 changes: 44 additions & 28 deletions prusti-encoder/src/encoders/local_def.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
use prusti_rustc_interface::{
index::IndexVec,
middle::{mir, ty},
span::def_id::DefId
span::def_id::DefId,
};

use task_encoder::{TaskEncoder, TaskEncoderDependencies};
use std::cell::RefCell;
use task_encoder::{TaskEncoder, TaskEncoderDependencies};

use crate::encoders::TypeEncoderOutputRef;

Expand All @@ -32,9 +32,9 @@ thread_local! {

impl TaskEncoder for MirLocalDefEncoder {
type TaskDescription<'tcx> = (
DefId, // ID of the function
DefId, // ID of the function
ty::GenericArgsRef<'tcx>, // ? this should be the "signature", after applying the env/substs
Option<DefId>, // ID of the caller function, if any
Option<DefId>, // ID of the caller function, if any
);

type OutputFullLocal<'vir> = MirLocalDefEncoderOutput<'vir>;
Expand Down Expand Up @@ -73,12 +73,16 @@ impl TaskEncoder for MirLocalDefEncoder {
> {
let (def_id, substs, caller_def_id) = *task_key;
deps.emit_output_ref::<Self>(*task_key, ());
fn mk_local_def<'vir, 'tcx>(vcx: &'vir vir::VirCtxt<'tcx>, name: &'vir str, ty: TypeEncoderOutputRef<'vir>) -> LocalDef<'vir> {
fn mk_local_def<'vir, 'tcx>(
vcx: &'vir vir::VirCtxt<'tcx>,
name: &'vir str,
ty: TypeEncoderOutputRef<'vir>,
) -> LocalDef<'vir> {
let local = vcx.mk_local(name);
let local_ex = vcx.mk_local_ex_local(local);
let impure_snap = ty.ref_to_snap.apply(vcx, [local_ex]);
let impure_pred = vcx.alloc(vir::ExprData::PredicateApp(
ty.ref_to_pred.apply(vcx, [local_ex])
ty.ref_to_pred.apply(vcx, [local_ex]),
));
LocalDef {
local,
Expand All @@ -91,36 +95,48 @@ impl TaskEncoder for MirLocalDefEncoder {

vir::with_vcx(|vcx| {
let data = if let Some(local_def_id) = def_id.as_local() {
let body = vcx.body.borrow_mut().get_impure_fn_body(local_def_id, substs, caller_def_id);
let locals = IndexVec::from_fn_n(|arg: mir::Local| {
let local = vir::vir_format!(vcx, "_{}p", arg.index());
let ty = deps.require_ref::<crate::encoders::TypeEncoder>(
body.local_decls[arg].ty,
).unwrap();
mk_local_def(vcx, local, ty)
}, body.local_decls.len());
let body =
vcx.body
.borrow_mut()
.get_impure_fn_body(local_def_id, substs, caller_def_id);
let locals = IndexVec::from_fn_n(
|arg: mir::Local| {
let local = vir::vir_format!(vcx, "_{}p", arg.index());
let ty = deps
.require_ref::<crate::encoders::TypeEncoder>(body.local_decls[arg].ty)
.unwrap();
mk_local_def(vcx, local, ty)
},
body.local_decls.len(),
);
MirLocalDefEncoderOutput {
locals: vcx.alloc(locals),
arg_count: body.arg_count,
}
} else {
let param_env = vcx.tcx.param_env(caller_def_id.unwrap_or(def_id));
let sig = vcx.tcx
.subst_and_normalize_erasing_regions(substs, param_env, vcx.tcx.fn_sig(def_id));
let sig = vcx.tcx.subst_and_normalize_erasing_regions(
substs,
param_env,
vcx.tcx.fn_sig(def_id),
);
let sig = sig.skip_binder();

let locals = IndexVec::from_fn_n(|arg: mir::Local| {
let local = vir::vir_format!(vcx, "_{}p", arg.index());
let ty = if arg.index() == 0 {
sig.output()
} else {
sig.inputs()[arg.index() - 1]
};
let ty = deps.require_ref::<crate::encoders::TypeEncoder>(
ty,
).unwrap();
mk_local_def(vcx, local, ty)
}, sig.inputs_and_output.len());
let locals = IndexVec::from_fn_n(
|arg: mir::Local| {
let local = vir::vir_format!(vcx, "_{}p", arg.index());
let ty = if arg.index() == 0 {
sig.output()
} else {
sig.inputs()[arg.index() - 1]
};
let ty = deps
.require_ref::<crate::encoders::TypeEncoder>(ty)
.unwrap();
mk_local_def(vcx, local, ty)
},
sig.inputs_and_output.len(),
);

MirLocalDefEncoderOutput {
locals: vcx.alloc(locals),
Expand Down
Loading