diff --git a/src/analyze.rs b/src/analyze.rs index 1f4853f..574a44b 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -210,7 +210,6 @@ impl<'tcx> Analyzer<'tcx> { .variants() .iter() .map(|variant| { - let name = refine::datatype_symbol(self.tcx, variant.def_id); // TODO: consider using TyCtxt::tag_for_variant let discr = resolve_discr(self.tcx, variant.discr); let field_tys = variant @@ -222,7 +221,7 @@ impl<'tcx> Analyzer<'tcx> { }) .collect(); rty::EnumVariantDef { - name, + name: chc::DatatypeSymbol::new(format!("{}.{}", name, variant.name)), discr, field_tys, } diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 86fa58f..0146e32 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -562,78 +562,30 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { }); } - fn is_box_new(&self, def_id: DefId) -> bool { - // TODO: stop using diagnositc item for semantic purpose - self.tcx.all_diagnostic_items(()).id_to_name.get(&def_id) - == Some(&rustc_span::symbol::sym::box_new) - } - - fn is_mem_swap(&self, def_id: DefId) -> bool { - // TODO: stop using diagnositc item for semantic purpose - self.tcx.all_diagnostic_items(()).id_to_name.get(&def_id) - == Some(&rustc_span::symbol::sym::mem_swap) - } - fn type_call(&mut self, func: Operand<'tcx>, args: I, expected_ret: &rty::RefinedType) where I: IntoIterator>, { // TODO: handle const_fn_def on Env side - let func_ty = match func.const_fn_def() { - // TODO: move this to well-known defs? - Some((def_id, args)) if self.is_box_new(def_id) => { - let inner_ty = self - .type_builder - .for_template(&mut self.ctx) - .build(args.type_at(0)) - .vacuous(); - let param = rty::RefinedType::unrefined(inner_ty.clone()); - let ret_term = - chc::Term::box_(chc::Term::var(rty::FunctionParamIdx::from(0_usize))); - let ret = rty::RefinedType::refined_with_term( - rty::PointerType::own(inner_ty).into(), - ret_term, - ); - rty::FunctionType::new([param].into_iter().collect(), ret).into() - } - Some((def_id, args)) if self.is_mem_swap(def_id) => { - let inner_ty = self.type_builder.build(args.type_at(0)).vacuous(); - let param1 = - rty::RefinedType::unrefined(rty::PointerType::mut_to(inner_ty.clone()).into()); - let param2 = - rty::RefinedType::unrefined(rty::PointerType::mut_to(inner_ty.clone()).into()); - let param1_var = rty::RefinedTypeVar::Free(rty::FunctionParamIdx::from(0_usize)); - let param2_var = rty::RefinedTypeVar::Free(rty::FunctionParamIdx::from(1_usize)); - let ret1 = chc::Term::var(param1_var) - .mut_current() - .equal_to(chc::Term::var(param2_var).mut_final()); - let ret2 = chc::Term::var(param2_var) - .mut_current() - .equal_to(chc::Term::var(param1_var).mut_final()); - let ret_formula = chc::Formula::Atom(ret1).and(chc::Formula::Atom(ret2)); - let ret = rty::RefinedType::new(rty::Type::unit(), ret_formula.into()); - rty::FunctionType::new([param1, param2].into_iter().collect(), ret).into() + let func_ty = if let Some((def_id, args)) = func.const_fn_def() { + let param_env = self.tcx.param_env(self.local_def_id); + let instance = mir_ty::Instance::resolve(self.tcx, param_env, def_id, args).unwrap(); + let resolved_def_id = if let Some(instance) = instance { + instance.def_id() + } else { + def_id + }; + if def_id != resolved_def_id { + tracing::info!(?def_id, ?resolved_def_id, "resolve",); } - Some((def_id, args)) => { - let param_env = self.tcx.param_env(self.local_def_id); - let instance = - mir_ty::Instance::resolve(self.tcx, param_env, def_id, args).unwrap(); - let resolved_def_id = if let Some(instance) = instance { - instance.def_id() - } else { - def_id - }; - if def_id != resolved_def_id { - tracing::info!(?def_id, ?resolved_def_id, "resolve",); - } - self.ctx - .def_ty_with_args(resolved_def_id, args) - .expect("unknown def") - .ty - .vacuous() - } - _ => self.operand_type(func.clone()).ty, + self.ctx + .def_ty_with_args(resolved_def_id, args) + .expect("unknown def") + .ty + .vacuous() + } else { + self.operand_type(func.clone()).ty }; let expected_args: IndexVec<_, _> = args .into_iter() diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index d556ef0..72b6ed9 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -274,8 +274,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let typeck_result = self.tcx.typeck(self.outer_def_id); if let rustc_hir::def::Res::Def(_, def_id) = typeck_result.qpath_res(qpath, hir_id) { - assert!(self.inner_def_id.is_none(), "invalid extern_spec_fn"); - self.inner_def_id = Some(def_id); + if matches!( + self.tcx.def_kind(def_id), + rustc_hir::def::DefKind::Fn | rustc_hir::def::DefKind::AssocFn + ) { + assert!(self.inner_def_id.is_none(), "invalid extern_spec_fn"); + self.inner_def_id = Some(def_id); + } } } } diff --git a/src/chc.rs b/src/chc.rs index 5543de4..7ee1a00 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -78,6 +78,10 @@ impl DatatypeSort { pub fn new(symbol: DatatypeSymbol, args: Vec) -> Self { DatatypeSort { symbol, args } } + + pub fn args_mut(&mut self) -> &mut Vec { + &mut self.args + } } /// A sort is the type of a logical term. diff --git a/src/main.rs b/src/main.rs index de276d8..4e91368 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,8 +1,11 @@ #![feature(rustc_private)] +extern crate rustc_ast; extern crate rustc_driver; extern crate rustc_interface; +extern crate rustc_parse; extern crate rustc_session; +extern crate rustc_span; use rustc_driver::{Callbacks, Compilation, RunCompiler}; use rustc_interface::interface::{Compiler, Config}; @@ -17,6 +20,29 @@ impl Callbacks for CompilerCalls { attrs.push("register_tool(thrust)".to_owned()); } + fn after_crate_root_parsing<'tcx>( + &mut self, + compiler: &Compiler, + queries: &'tcx Queries<'tcx>, + ) -> Compilation { + let mut result = queries.parse().unwrap(); + let krate = result.get_mut(); + + let injected = include_str!("../std.rs"); + let mut parser = rustc_parse::new_parser_from_source_str( + &compiler.sess.psess, + rustc_span::FileName::Custom("thrust std injected".to_string()), + injected.to_owned(), + ); + while let Some(item) = parser + .parse_item(rustc_parse::parser::ForceCollect::No) + .unwrap() + { + krate.items.push(item); + } + Compilation::Continue + } + fn after_analysis<'tcx>( &mut self, _compiler: &Compiler, diff --git a/src/refine/template.rs b/src/refine/template.rs index da8e4b6..29ff975 100644 --- a/src/refine/template.rs +++ b/src/refine/template.rs @@ -412,6 +412,8 @@ where .with_scope(&builder) .build_refined(param_ty.ty) } + } else if self.param_refinement.is_some() { + rty::RefinedType::unrefined(self.inner.build(param_ty.ty).vacuous()) } else { rty::RefinedType::unrefined( self.inner diff --git a/src/rty.rs b/src/rty.rs index 4c3d2a1..331a9a0 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -1254,6 +1254,13 @@ impl Refinement { refinement: self, } } + + pub fn subst_ty_params_in_sorts(&mut self, subst: &TypeParamSubst) { + for sort in &mut self.existentials { + subst_ty_params_in_sort(sort, subst); + } + subst_ty_params_in_body(&mut self.body, subst); + } } /// A helper type to map logical variables in a refinement at once. @@ -1445,6 +1452,7 @@ impl RefinedType { where FV: chc::Var, { + self.refinement.subst_ty_params_in_sorts(subst); match &mut self.ty { Type::Int | Type::Bool | Type::String | Type::Never => {} Type::Param(ty) => { @@ -1513,6 +1521,108 @@ impl RefinedType { } } +/// Substitutes type parameters in a sort. +fn subst_ty_params_in_sort(sort: &mut chc::Sort, subst: &TypeParamSubst) { + match sort { + chc::Sort::Null | chc::Sort::Int | chc::Sort::Bool | chc::Sort::String => {} + chc::Sort::Param(idx) => { + let type_param_idx = TypeParamIdx::from_usize(*idx); + if let Some(rty) = subst.get(type_param_idx) { + *sort = rty.ty.to_sort(); + } + } + chc::Sort::Box(s) | chc::Sort::Mut(s) => { + subst_ty_params_in_sort(s, subst); + } + chc::Sort::Tuple(sorts) => { + for s in sorts { + subst_ty_params_in_sort(s, subst); + } + } + chc::Sort::Datatype(dt_sort) => { + for s in dt_sort.args_mut() { + subst_ty_params_in_sort(s, subst); + } + } + } +} + +/// Substitutes type parameters in all sorts appearing in a body. +fn subst_ty_params_in_body(body: &mut chc::Body, subst: &TypeParamSubst) { + for atom in &mut body.atoms { + subst_ty_params_in_atom(atom, subst); + } + subst_ty_params_in_formula(&mut body.formula, subst); +} + +/// Substitutes type parameters in all sorts appearing in an atom. +fn subst_ty_params_in_atom(atom: &mut chc::Atom, subst: &TypeParamSubst) { + if let Some(guard) = &mut atom.guard { + subst_ty_params_in_formula(guard, subst); + } + for term in &mut atom.args { + subst_ty_params_in_term(term, subst); + } +} + +/// Substitutes type parameters in all sorts appearing in a formula. +fn subst_ty_params_in_formula(formula: &mut chc::Formula, subst: &TypeParamSubst) { + match formula { + chc::Formula::Atom(atom) => subst_ty_params_in_atom(atom, subst), + chc::Formula::Not(f) => subst_ty_params_in_formula(f, subst), + chc::Formula::And(fs) | chc::Formula::Or(fs) => { + for f in fs { + subst_ty_params_in_formula(f, subst); + } + } + chc::Formula::Exists(vars, f) => { + for (_, sort) in vars { + subst_ty_params_in_sort(sort, subst); + } + subst_ty_params_in_formula(f, subst); + } + } +} + +/// Substitutes type parameters in all sorts appearing in a term. +fn subst_ty_params_in_term(term: &mut chc::Term, subst: &TypeParamSubst) { + match term { + chc::Term::Null + | chc::Term::Var(_) + | chc::Term::Bool(_) + | chc::Term::Int(_) + | chc::Term::String(_) => {} + chc::Term::Box(t) + | chc::Term::BoxCurrent(t) + | chc::Term::MutCurrent(t) + | chc::Term::MutFinal(t) + | chc::Term::TupleProj(t, _) + | chc::Term::DatatypeDiscr(_, t) => { + subst_ty_params_in_term(t, subst); + } + chc::Term::Mut(t1, t2) => { + subst_ty_params_in_term(t1, subst); + subst_ty_params_in_term(t2, subst); + } + chc::Term::App(_, args) | chc::Term::Tuple(args) => { + for arg in args { + subst_ty_params_in_term(arg, subst); + } + } + chc::Term::DatatypeCtor(s, _, args) => { + for arg in s.args_mut() { + subst_ty_params_in_sort(arg, subst); + } + for arg in args { + subst_ty_params_in_term(arg, subst); + } + } + chc::Term::FormulaExistentialVar(sort, _) => { + subst_ty_params_in_sort(sort, subst); + } + } +} + pub fn unify_tys_params(tys1: I1, tys2: I2) -> TypeParamSubst where T: chc::Var, diff --git a/std.rs b/std.rs new file mode 100644 index 0000000..206d5ea --- /dev/null +++ b/std.rs @@ -0,0 +1,203 @@ +// This file is injected to source code by Thrust + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures(result == )] +fn _extern_spec_box_new(x: T) -> Box { + Box::new(x) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures(*x == ^y && *y == ^x)] +fn _extern_spec_std_mem_swap(x: &mut T, y: &mut T) { + std::mem::swap(x, y); +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures(^dest == src && result == *dest)] +fn _extern_spec_std_mem_replace(dest: &mut T, src: T) -> T { + std::mem::replace(dest, src) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(opt != std::option::Option::::None())] +#[thrust::ensures(std::option::Option::::Some(result) == opt)] +fn _extern_spec_option_unwrap(opt: Option) -> T { + Option::unwrap(opt) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (*opt == std::option::Option::::None() && result == true) + || (*opt != std::option::Option::::None() && result == false) +)] +fn _extern_spec_option_is_none(opt: &Option) -> bool { + Option::is_none(opt) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (*opt == std::option::Option::::None() && result == false) + || (*opt != std::option::Option::::None() && result == true) +)] +fn _extern_spec_option_is_some(opt: &Option) -> bool { + Option::is_some(opt) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (opt != std::option::Option::::None() && std::option::Option::::Some(result) == opt) + || (opt == std::option::Option::::None() && result == default) +)] +fn _extern_spec_option_unwrap_or(opt: Option, default: T) -> T { + Option::unwrap_or(opt, default) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (exists x:T0. opt == std::option::Option::::Some(x) && result == std::result::Result::::Ok(x)) + || (opt == std::option::Option::::None() && result == std::result::Result::::Err(err)) +)] +fn _extern_spec_option_ok_or(opt: Option, err: E) -> Result { + Option::ok_or(opt, err) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures(^opt == std::option::Option::::None() && result == *opt)] +fn _extern_spec_option_take(opt: &mut Option) -> Option { + Option::take(opt) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures(^opt == std::option::Option::::Some(src) && result == *opt)] +fn _extern_spec_option_replace(opt: &mut Option, src: T) -> Option { + Option::replace(opt, src) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (exists x:T0. opt == ::Some(x)> && result == std::option::Option::<&T0>::Some()) + || (opt == ::None()> && result == std::option::Option::<&T0>::None()) +)] +fn _extern_spec_option_as_ref(opt: &Option) -> Option<&T> { + Option::as_ref(opt) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (exists x1:T0, x2:T0. + *opt == std::option::Option::::Some(x1) && + ^opt == std::option::Option::::Some(x2) && + result == std::option::Option::<&mut T0>::Some() + ) + || ( + *opt == std::option::Option::::None() && + ^opt == std::option::Option::::None() && + result == std::option::Option::<&mut T0>::None() + ) +)] +fn _extern_spec_option_as_mut(opt: &mut Option) -> Option<&mut T> { + Option::as_mut(opt) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(exists x:T0. res == std::result::Result::::Ok(x))] +#[thrust::ensures(std::result::Result::::Ok(result) == res)] +fn _extern_spec_result_unwrap(res: Result) -> T { + Result::unwrap(res) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(exists x:T1. res == std::result::Result::::Err(x))] +#[thrust::ensures(std::result::Result::::Err(result) == res)] +fn _extern_spec_result_unwrap_err(res: Result) -> E { + Result::unwrap_err(res) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (exists x:T0. res == std::result::Result::::Ok(x) && result == std::option::Option::::Some(x)) + || (exists x:T1. res == std::result::Result::::Err(x) && result == std::option::Option::::None()) +)] +fn _extern_spec_result_ok(res: Result) -> Option { + Result::ok(res) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (exists x:T0. res == std::result::Result::::Ok(x) && result == std::option::Option::::None()) + || (exists x:T1. res == std::result::Result::::Err(x) && result == std::option::Option::::Some(x)) +)] +fn _extern_spec_result_err(res: Result) -> Option { + Result::err(res) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (exists x:T0. *res == std::result::Result::::Ok(x) && result == true) + || (exists x:T1. *res == std::result::Result::::Err(x) && result == false) +)] +fn _extern_spec_result_is_ok(res: &Result) -> bool { + Result::is_ok(res) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (exists x:T0. *res == std::result::Result::::Ok(x) && result == false) + || (exists x:T1. *res == std::result::Result::::Err(x) && result == true) +)] +fn _extern_spec_result_is_err(res: &Result) -> bool { + Result::is_err(res) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] // TODO: require x != i32::MIN +#[thrust::ensures(result >= 0 && (result == x || result == -x))] +fn _extern_spec_i32_abs(x: i32) -> i32 { + i32::abs(x) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures( + (x >= y && result == (x - y)) + || (x < y && result == (y - x)) +)] +fn _extern_spec_i32_abs_diff(x: i32, y: i32) -> u32 { + i32::abs_diff(x, y) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))] +fn _extern_spec_i32_signum(x: i32) -> i32 { + i32::signum(x) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures((x < 0 && result == false) || (x >= 0 && result == true))] +fn _extern_spec_i32_is_positive(x: i32) -> bool { + i32::is_positive(x) +} + +#[thrust::extern_spec_fn] +#[thrust::requires(true)] +#[thrust::ensures((x <= 0 && result == true) || (x > 0 && result == false))] +fn _extern_spec_i32_is_negative(x: i32) -> bool { + i32::is_negative(x) +}