Skip to content

Commit 32018f1

Browse files
coord-ecoord-e
committed
Fix unsoundness when expanding variant of polymorphic enum
1 parent d11565d commit 32018f1

File tree

5 files changed

+96
-30
lines changed

5 files changed

+96
-30
lines changed

‎src/analyze/basic_block.rs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -511,7 +511,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
511511
F: FnOnce(&mut Self) -> T,
512512
{
513513
let old_env = self.env.clone();
514-
self.env.assume(assumption);
514+
self.env.assume(assumption, None);
515515
let result = callback(self);
516516
self.env = old_env;
517517
result
@@ -682,7 +682,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
682682
let (_, rvalue_term) = builder.subsume(rvalue_ty);
683683
builder.push_formula(local_term.mut_final().equal_to(rvalue_term));
684684
let assumption = builder.build_assumption();
685-
self.env.assume(assumption);
685+
self.env.assume(assumption, None);
686686
}
687687
}
688688

@@ -1070,7 +1070,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
10701070
assumption.existentials.extend(existentials);
10711071
}
10721072

1073-
self.env.assume(assumption);
1073+
self.env.assume(assumption, None);
10741074
}
10751075

10761076
fn unbind_atoms(&self) -> UnbindAtoms<rty::FunctionParamIdx> {

‎src/chc.rs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -371,6 +371,8 @@ impl Function {
371371
Self::LE => Sort::bool(),
372372
Self::LT => Sort::bool(),
373373
Self::NOT => Sort::bool(),
374+
Self::AND => Sort::bool(),
375+
Self::OR => Sort::bool(),
374376
Self::NEG => Sort::int(),
375377
_ => unimplemented!(),
376378
}
@@ -385,6 +387,8 @@ impl Function {
385387
pub const LE: Function = Function::infix("<=");
386388
pub const LT: Function = Function::infix("<");
387389
pub const NOT: Function = Function::new("not");
390+
pub const AND: Function = Function::new("and");
391+
pub const OR: Function = Function::new("or");
388392
pub const NEG: Function = Function::new("-");
389393
}
390394

@@ -682,6 +686,14 @@ impl<V> Term<V> {
682686
Term::App(Function::NOT, vec![self])
683687
}
684688

689+
pub fn bool_and(self, other: Self) -> Self {
690+
Term::App(Function::AND, vec![self, other])
691+
}
692+
693+
pub fn bool_or(self, other: Self) -> Self {
694+
Term::App(Function::OR, vec![self, other])
695+
}
696+
685697
pub fn neg(self) -> Self {
686698
Term::App(Function::NEG, vec![self])
687699
}

‎src/refine/env.rs‎

Lines changed: 55 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -603,6 +603,7 @@ impl Env {
603603
ty: rty::PointerType<Var>,
604604
refinement: rty::Refinement<Var>,
605605
depth: usize,
606+
guard: Option<chc::Term<Var>>,
606607
) {
607608
// note that the given var is unbound here, so be careful of using indices around temp_vars
608609
let current_refinement = refinement
@@ -623,7 +624,7 @@ impl Env {
623624
};
624625
let mut inner_ty = *ty.elem;
625626
inner_ty.extend_refinement(current_refinement);
626-
self.bind_impl(current.into(), inner_ty, depth);
627+
self.bind_impl(current.into(), inner_ty, depth, guard);
627628
}
628629

629630
fn bind_mut(
@@ -632,6 +633,7 @@ impl Env {
632633
ty: rty::PointerType<Var>,
633634
refinement: rty::Refinement<Var>,
634635
depth: usize,
636+
guard: Option<chc::Term<Var>>,
635637
) {
636638
// note that the given var is unbound here, so be careful of using indices around temp_vars
637639
let next_index = self.temp_vars.next_index();
@@ -661,7 +663,7 @@ impl Env {
661663
);
662664
let mut inner_ty = *ty.elem;
663665
inner_ty.extend_refinement(current_refinement);
664-
self.bind_impl(current.into(), inner_ty, depth);
666+
self.bind_impl(current.into(), inner_ty, depth, guard);
665667
}
666668

667669
fn bind_tuple(
@@ -670,6 +672,7 @@ impl Env {
670672
ty: rty::TupleType<Var>,
671673
refinement: rty::Refinement<Var>,
672674
depth: usize,
675+
guard: Option<chc::Term<Var>>,
673676
) {
674677
if let Var::Temp(temp) = var {
675678
// XXX: allocate `temp` once to invoke bind_var recursively
@@ -681,7 +684,7 @@ impl Env {
681684
for elem in &ty.elems {
682685
let x = self.temp_vars.next_index();
683686
xs.push(x);
684-
self.bind_impl(x.into(), elem.clone(), depth);
687+
self.bind_impl(x.into(), elem.clone(), depth, guard.clone());
685688
}
686689
let assumption = {
687690
let tuple_ty = PlaceType::tuple(
@@ -702,7 +705,7 @@ impl Env {
702705
existentials.extend(refinement.existentials);
703706
Assumption::new(existentials, formula)
704707
};
705-
self.assume(assumption);
708+
self.assume(assumption, guard);
706709
let binding = FlowBinding::Tuple(xs.clone());
707710
match var {
708711
Var::Local(local) => {
@@ -720,6 +723,7 @@ impl Env {
720723
ty: rty::EnumType<Var>,
721724
refinement: rty::Refinement<Var>,
722725
depth: usize,
726+
guard: Option<chc::Term<Var>>,
723727
) {
724728
if let Var::Temp(temp) = var {
725729
// XXX: allocate `temp` once to invoke bind_var recursively
@@ -730,15 +734,29 @@ impl Env {
730734
let def = self.enum_defs[&ty.symbol].clone();
731735
let matcher_pred = chc::MatcherPred::new(ty.symbol.clone(), ty.arg_sorts());
732736

737+
let discr_var = self
738+
.temp_vars
739+
.push(TempVarBinding::Type(rty::RefinedType::unrefined(
740+
rty::Type::int(),
741+
)));
742+
733743
let mut variants = IndexVec::new();
734-
for variant_def in &def.variants {
744+
for (variant_idx, variant_def) in def.variants.iter_enumerated() {
735745
let mut fields = IndexVec::new();
746+
let variant_guard = {
747+
let discr_term = chc::Term::var(discr_var.into());
748+
let condition = discr_term.eq(chc::Term::int(variant_def.discr as i64));
749+
match guard.clone() {
750+
Some(g) => g.bool_and(condition),
751+
None => condition,
752+
}
753+
};
736754
for field_ty in &variant_def.field_tys {
737755
let x = self.temp_vars.next_index();
738756
fields.push(x);
739757
let mut field_ty = rty::RefinedType::unrefined(field_ty.clone().vacuous());
740758
field_ty.instantiate_ty_params(ty.args.clone());
741-
self.bind_impl(x.into(), field_ty.boxed(), depth);
759+
self.bind_impl(x.into(), field_ty.boxed(), depth, Some(variant_guard.clone()));
742760
}
743761
variants.push(FlowBindingVariant { fields });
744762
}
@@ -773,11 +791,6 @@ impl Env {
773791
assumption
774792
.body
775793
.push_conj(chc::Atom::new(matcher_pred.into(), pred_args));
776-
let discr_var = self
777-
.temp_vars
778-
.push(TempVarBinding::Type(rty::RefinedType::unrefined(
779-
rty::Type::int(),
780-
)));
781794
assumption
782795
.body
783796
.push_conj(
@@ -786,7 +799,7 @@ impl Env {
786799
chc::Term::var(value_var_ev.into()),
787800
)),
788801
);
789-
self.assume(assumption);
802+
self.assume(assumption, guard);
790803

791804
let binding = FlowBinding::Enum {
792805
discr: discr_var,
@@ -803,7 +816,14 @@ impl Env {
803816
}
804817
}
805818

806-
fn bind_var(&mut self, var: Var, rty: rty::RefinedType<Var>) {
819+
fn bind_var(&mut self, var: Var, mut rty: rty::RefinedType<Var>, guard: Option<chc::Term<Var>>) {
820+
if let Some(guard) = guard {
821+
let guard_false = guard
822+
.equal_to(chc::Term::bool(false))
823+
.map_var(rty::RefinedTypeVar::Free);
824+
let body = std::mem::take(&mut rty.refinement.body);
825+
rty.refinement.body = chc::Formula::Or(vec![chc::Formula::Atom(guard_false), body.formula]).into();
826+
}
807827
match var {
808828
Var::Local(local) => {
809829
self.locals.insert(local, rty);
@@ -814,43 +834,51 @@ impl Env {
814834
}
815835
}
816836

817-
fn bind_impl(&mut self, var: Var, rty: rty::RefinedType<Var>, depth: usize) {
837+
fn bind_impl(&mut self, var: Var, rty: rty::RefinedType<Var>, depth: usize, guard: Option<chc::Term<Var>>) {
818838
if depth >= self.enum_expansion_depth_limit {
819-
self.bind_var(var, rty);
839+
self.bind_var(var, rty, guard);
820840
return;
821841
}
822842
match rty.ty {
823-
rty::Type::Pointer(ty) if ty.is_own() => self.bind_own(var, ty, rty.refinement, depth),
824-
rty::Type::Pointer(ty) if ty.is_mut() => self.bind_mut(var, ty, rty.refinement, depth),
843+
rty::Type::Pointer(ty) if ty.is_own() => self.bind_own(var, ty, rty.refinement, depth, guard),
844+
rty::Type::Pointer(ty) if ty.is_mut() => self.bind_mut(var, ty, rty.refinement, depth, guard),
825845
rty::Type::Tuple(ty) if !ty.is_unit() => {
826-
self.bind_tuple(var, ty, rty.refinement, depth)
846+
self.bind_tuple(var, ty, rty.refinement, depth, guard)
827847
}
828-
rty::Type::Enum(ty) => self.bind_enum(var, ty, rty.refinement, depth + 1),
829-
_ => self.bind_var(var, rty),
848+
rty::Type::Enum(ty) => self.bind_enum(var, ty, rty.refinement, depth + 1, guard),
849+
_ => self.bind_var(var, rty, guard),
830850
}
831851
}
832852

833853
pub fn mut_bind(&mut self, local: Local, rty: rty::RefinedType<Var>) {
834854
let rty_disp = rty.clone();
835-
self.bind_impl(local.into(), rty, 0);
855+
self.bind_impl(local.into(), rty, 0, None);
836856
tracing::debug!(local = ?local, rty = %rty_disp.display(), place_type = %self.local_type(local).display(), "mut_bind");
837857
}
838858

839859
pub fn immut_bind(&mut self, local: Local, rty: rty::RefinedType<Var>) {
840860
let rty_disp = rty.clone();
841-
self.bind_var(local.into(), rty);
861+
self.bind_var(local.into(), rty, None);
842862
tracing::debug!(local = ?local, rty = %rty_disp.display(), place_type = %self.local_type(local).display(), "immut_bind");
843863
}
844864

845-
pub fn assume(&mut self, assumption: impl Into<Assumption>) {
846-
let assumption = assumption.into();
865+
pub fn assume(&mut self, assumption: impl Into<Assumption>, guard: Option<chc::Term<Var>>) {
866+
let mut assumption = assumption.into();
867+
if let Some(guard) = guard {
868+
let guard_false = guard
869+
.equal_to(chc::Term::bool(false))
870+
.map_var(PlaceTypeVar::Var);
871+
let body = std::mem::take(&mut assumption.body);
872+
assumption.body = chc::Formula::Or(vec![chc::Formula::Atom(guard_false), body.formula]).into();
873+
}
847874
tracing::debug!(assumption = %assumption.display(), "assume");
848875
self.assumptions.push(assumption);
849876
}
850877

851878
pub fn extend_assumptions(&mut self, assumptions: Vec<impl Into<Assumption>>) {
852-
self.assumptions
853-
.extend(assumptions.into_iter().map(Into::into));
879+
for assumption in assumptions {
880+
self.assume(assumption, None);
881+
}
854882
}
855883

856884
pub fn dependencies(&self) -> impl Iterator<Item = (Var, chc::Sort)> + '_ {
@@ -1146,7 +1174,7 @@ impl Env {
11461174
pub fn drop_local(&mut self, local: Local) {
11471175
let assumption = self.dropping_assumption(&Path::Local(local));
11481176
if !assumption.is_top() {
1149-
self.assume(assumption);
1177+
self.assume(assumption, None);
11501178
}
11511179
}
11521180
}

‎tests/ui/fail/unused_variant_predicate.rs‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
//@error-in-other-file: Unsat
2+
3+
enum X<T> {
4+
None1,
5+
None2,
6+
Some(T),
7+
}
8+
9+
fn main() {
10+
let mut opt: X<i32> = X::None1;
11+
opt = X::None2;
12+
assert!(matches!(opt, X::None1));
13+
}

‎tests/ui/pass/unused_variant_predicate.rs‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
//@check-pass
2+
3+
enum X<T> {
4+
None1,
5+
None2,
6+
Some(T),
7+
}
8+
9+
fn main() {
10+
let mut opt: X<i32> = X::None1;
11+
opt = X::None2;
12+
assert!(matches!(opt, X::None2));
13+
}

0 commit comments

Comments
 (0)