Skip to content

Model unsigned integers as non-negative #268

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鈥檒l occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
coord-e wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Model unsigned integers as non-negative #268

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
3 changes: 0 additions & 3 deletions src/analyze.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -441,7 +441,6 @@ impl<'tcx> Analyzer<'tcx> {
generic_args
.types()
.map(|ty| type_builder.build(ty))
.map(rty::RefinedType::unrefined)
.collect(),
);
def_ty.ty.as_function().cloned()
Expand Down Expand Up @@ -484,7 +483,6 @@ impl<'tcx> Analyzer<'tcx> {
generic_args
.types()
.map(|ty| type_builder.build(ty))
.map(rty::RefinedType::unrefined)
.collect(),
);
return Some(def_ty);
Expand All @@ -508,7 +506,6 @@ impl<'tcx> Analyzer<'tcx> {
generic_args
.types()
.map(|ty| type_builder.build(ty))
.map(rty::RefinedType::unrefined)
.collect(),
);
deferred_ty_cache
Expand Down
8 changes: 8 additions & 0 deletions src/analyze/annot.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,14 @@ pub fn int_model_path() -> [Symbol; 3] {
]
}

pub fn uint_model_path() -> [Symbol; 3] {
[
Symbol::intern("thrust"),
Symbol::intern("def"),
Symbol::intern("uint_model"),
]
}

pub fn mut_model_path() -> [Symbol; 3] {
[
Symbol::intern("thrust"),
Expand Down
6 changes: 3 additions & 3 deletions src/analyze/annot_fn.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
let term = if ty.to_sort().is_singleton() {
// the analyzer don't expect params with singleton sorts to be used in formula...
// FIXME: fix the analyzer side to uniformly accept all params
Self::singleton_term_for_ty(&ty).unwrap()
Self::singleton_term_for_ty(&ty.ty).unwrap()
} else {
chc::Term::var(param_idx)
};
Expand Down Expand Up @@ -578,7 +578,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
let generic_args =
mir_ty::EarlyBinder::bind(generic_args).instantiate(self.tcx, self.generic_args);
let elem_ty = generic_args.type_at(idx);
self.type_builder.build(elem_ty)
self.type_builder.build(elem_ty).ty
}

fn adt_arg_type_at(
Expand All @@ -589,7 +589,7 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
let mir_ty::TyKind::Adt(_, args) = self.expr_ty(expr).kind() else {
panic!("expected ADT");
};
self.type_builder.build(args.type_at(idx))
self.type_builder.build(args.type_at(idx)).ty
}

fn variant_ctor_term(
Expand Down
20 changes: 9 additions & 11 deletions src/analyze/basic_block.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -549,7 +549,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
//
// TODO: Stop embedding knowledge of `<[T; N] as Model>::Ty` in the analyzer
let mut builder = PlaceTypeBuilder::default();
let elem_ty = self.type_builder.build(mir_elem_ty).vacuous();
let elem_ty = self.type_builder.build(mir_elem_ty).vacuous().ty;
let mut arr_term =
chc::Term::array_empty(chc::Sort::int(), elem_ty.to_sort());
for (i, field) in fields.iter().enumerate() {
Expand Down Expand Up @@ -583,7 +583,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
.field_tys
.clone()
.into_iter()
.map(|ty| rty::RefinedType::unrefined(ty.vacuous()));
.map(|rty| rty.vacuous());

let rty_args: IndexVec<_, _> = args
.types()
Expand Down Expand Up @@ -658,7 +658,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
) => {
// Only treat unsizing as identity when both sides resolve to the same model.
let mut op_pty = self.operand_type(operand);
let expected_ty = self.type_builder.build(ty).vacuous();
let expected_ty = self.type_builder.build(ty).vacuous().ty;
if op_pty.ty.to_sort() != expected_ty.to_sort() {
unimplemented!("unsize cast: {:?} -> {:?}", op_pty.ty, expected_ty);
}
Expand Down Expand Up @@ -1049,17 +1049,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
.expect("ghost formula function takes the ghost value as its first parameter");
let mut params: IndexVec<_, _> = param_tys
.iter()
.map(|ty| rty::RefinedType::unrefined(self.type_builder.build(*ty)).vacuous())
.map(|ty| self.type_builder.build(*ty).vacuous())
.collect();
if params.is_empty() {
// elaboration: we need at least one predicate variable in parameter
params.push(rty::RefinedType::unrefined(rty::Type::unit()).vacuous());
}
let value_ty = self.type_builder.build(*value_ty);
let func_ty = rty::FunctionType::new(
params,
rty::RefinedType::new(value_ty.vacuous(), formula_fn.to_refinement()),
);
let mut value_rty = self.type_builder.build(*value_ty).vacuous();
value_rty.refinement.push_conj(formula_fn.to_refinement());
let func_ty = rty::FunctionType::new(params, value_rty);

let args = formula_fn
.param_idents()
Expand Down Expand Up @@ -1133,7 +1131,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {

fn add_prophecy_var(&mut self, statement_index: usize, ty: mir_ty::Ty<'tcx>) {
let ty = self.type_builder.build(ty);
let temp_var = self.env.push_temp_var(ty.vacuous());
let temp_var = self.env.push_temp_var(ty.vacuous().ty);
self.prophecy_vars.insert(statement_index, temp_var);
tracing::debug!(stmt_idx = %statement_index, temp_var = ?temp_var, "add_prophecy_var");
}
Expand All @@ -1154,7 +1152,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
prophecy_ty: mir_ty::Ty<'tcx>,
) -> rty::RefinedType<Var> {
let prophecy_ty = self.type_builder.build(prophecy_ty);
let prophecy = self.env.push_temp_var(prophecy_ty.vacuous());
let prophecy = self.env.push_temp_var(prophecy_ty.vacuous().ty);
let place = self.elaborate_place_for_borrow(&referent);
self.env.borrow_place(place, prophecy).into()
}
Expand Down
8 changes: 8 additions & 0 deletions src/analyze/did_cache.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ struct DefIds {

model_ty: OnceCell<Option<DefId>>,
int_model: OnceCell<Option<DefId>>,
uint_model: OnceCell<Option<DefId>>,
mut_model: OnceCell<Option<DefId>>,
box_model: OnceCell<Option<DefId>>,
array_model: OnceCell<Option<DefId>>,
Expand Down Expand Up @@ -138,6 +139,13 @@ impl<'tcx> DefIdCache<'tcx> {
.get_or_init(|| self.annotated_def(&crate::analyze::annot::int_model_path()))
}

pub fn uint_model(&self) -> Option<DefId> {
*self
.def_ids
.uint_model
.get_or_init(|| self.annotated_def(&crate::analyze::annot::uint_model_path()))
}

pub fn mut_model(&self) -> Option<DefId> {
*self
.def_ids
Expand Down
4 changes: 4 additions & 0 deletions src/chc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1781,6 +1781,10 @@ impl<V> Body<V> {
self.formula.is_bottom() || self.atoms.iter().any(|a| a.is_bottom())
}

pub fn has_pred_var(&self) -> bool {
self.atoms.iter().any(|a| matches!(a.pred, Pred::Var(_)))
}

pub fn push_conj(&mut self, other: impl Into<Body<V>>) {
let Body { atoms, formula } = other.into();
self.atoms.extend(atoms);
Expand Down
5 changes: 3 additions & 2 deletions src/refine/basic_block.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,9 +170,10 @@ impl BasicBlockType {
};
mapping.insert(idx, mapped_idx);

// to be sure
// to be sure: only the last parameter carries the predicate variable of the
// precondition; the others carry at most what their model says about them.
if idx != last_param_idx {
assert!(param_ty.refinement.is_top());
assert!(!param_ty.refinement.has_pred_var());
}
}

Expand Down
10 changes: 4 additions & 6 deletions src/refine/env.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -422,7 +422,7 @@ impl PlaceType {
let mut field_terms = Vec::new();
let mut field_tys = Vec::new();
for field_ty in variant.field_tys.clone() {
let mut rty = rty::RefinedType::unrefined(field_ty.vacuous());
let mut rty = field_ty.vacuous();
rty.instantiate_ty_params(inner_ty.args.clone());
let (ty, field_ex_var) = builder.subsume_rty(rty.boxed());

Expand Down Expand Up @@ -766,7 +766,7 @@ where
for field_ty in &variant_def.field_tys {
let x = self.temp_vars.next_index();
fields.push(x);
let mut field_ty = rty::RefinedType::unrefined(field_ty.clone().vacuous());
let mut field_ty = field_ty.clone().vacuous();
field_ty.instantiate_ty_params(ty.args.clone());
let guarded_field_ty = field_ty.guarded(
chc::Term::var(discr_var.into())
Expand Down Expand Up @@ -977,9 +977,7 @@ where

let arg_rtys = {
let def = self.enum_defs.enum_def(sym);
let expected_tys = def
.field_tys()
.map(|ty| rty::RefinedType::unrefined(ty.clone().vacuous()).boxed());
let expected_tys = def.field_tys().map(|rty| rty.clone().vacuous().boxed());
let got_tys = field_tys.iter().map(|ty| ty.clone().into());
rty::unify_tys_params(expected_tys, got_tys).into_args(def.ty_params, |_| {
panic!("var_type: should unify all params")
Expand Down Expand Up @@ -1147,7 +1145,7 @@ where

let mut pred_args = vec![];
for field_ty in enum_def.field_tys() {
let mut field_rty = rty::RefinedType::unrefined(field_ty.clone().vacuous());
let mut field_rty = field_ty.clone().vacuous();
field_rty.instantiate_ty_params(ety.args.clone());
let field_type = field_rty.ty;

Expand Down
Loading
Loading