Skip to content

Commit 827c750

Browse files
coord-ecoord-e
authored
Merge pull request #16 from coord-e/unused-variant-predicate
Fix unsoundness when expanding variant of polymorphic enum
2 parents d11565d + 750b03a commit 827c750

File tree

7 files changed

+150
-21
lines changed

7 files changed

+150
-21
lines changed

‎src/chc.rs‎

Lines changed: 80 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -997,6 +997,12 @@ impl Pred {
997997
/// An atom is a predicate applied to a list of terms.
998998
#[derive(Debug, Clone)]
999999
pub struct Atom<V = TermVarIdx> {
1000+
/// With `guard`, this represents `guard => pred(args)`.
1001+
///
1002+
/// As long as there is no pvar in the `guard`, it forms a valid CHC. However, in that case,
1003+
/// it becomes odd to call this an `Atom`... It is our TODO to clean this up by either
1004+
/// getting rid of the `guard` or renaming `Atom`.
1005+
pub guard: Option<Box<Formula<V>>>,
10001006
pub pred: Pred,
10011007
pub args: Vec<Term<V>>,
10021008
}
@@ -1008,7 +1014,12 @@ where
10081014
D::Doc: Clone,
10091015
{
10101016
fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
1011-
if self.pred.is_infix() {
1017+
let guard = if let Some(guard) = &self.guard {
1018+
guard.pretty(allocator).append(allocator.text(" ⇒"))
1019+
} else {
1020+
allocator.nil()
1021+
};
1022+
let atom = if self.pred.is_infix() {
10121023
self.args[0]
10131024
.pretty_atom(allocator)
10141025
.append(allocator.line())
@@ -1027,42 +1038,58 @@ where
10271038
} else {
10281039
p.append(allocator.line()).append(inner.nest(2)).group()
10291040
}
1030-
}
1041+
};
1042+
guard.append(allocator.line()).append(atom).group()
10311043
}
10321044
}
10331045

10341046
impl<V> Atom<V> {
10351047
pub fn new(pred: Pred, args: Vec<Term<V>>) -> Self {
1036-
Atom { pred, args }
1048+
Atom {
1049+
guard: None,
1050+
pred,
1051+
args,
1052+
}
10371053
}
10381054

1039-
pub fn top() -> Self {
1055+
pub fn with_guard(guard: Formula<V>, pred: Pred, args: Vec<Term<V>>) -> Self {
10401056
Atom {
1041-
pred: KnownPred::TOP.into(),
1042-
args: vec![],
1057+
guard: Some(Box::new(guard)),
1058+
pred,
1059+
args,
10431060
}
10441061
}
10451062

1063+
pub fn top() -> Self {
1064+
Atom::new(KnownPred::TOP.into(), vec![])
1065+
}
1066+
10461067
pub fn bottom() -> Self {
1047-
Atom {
1048-
pred: KnownPred::BOTTOM.into(),
1049-
args: vec![],
1050-
}
1068+
Atom::new(KnownPred::BOTTOM.into(), vec![])
10511069
}
10521070

10531071
pub fn is_top(&self) -> bool {
1054-
self.pred.is_top()
1072+
if let Some(guard) = &self.guard {
1073+
guard.is_bottom() || self.pred.is_top()
1074+
} else {
1075+
self.pred.is_top()
1076+
}
10551077
}
10561078

10571079
pub fn is_bottom(&self) -> bool {
1058-
self.pred.is_bottom()
1080+
if let Some(guard) = &self.guard {
1081+
guard.is_top() && self.pred.is_bottom()
1082+
} else {
1083+
self.pred.is_bottom()
1084+
}
10591085
}
10601086

10611087
pub fn subst_var<F, W>(self, mut f: F) -> Atom<W>
10621088
where
10631089
F: FnMut(V) -> Term<W>,
10641090
{
10651091
Atom {
1092+
guard: self.guard.map(|fo| Box::new(fo.subst_var(&mut f))),
10661093
pred: self.pred,
10671094
args: self.args.into_iter().map(|t| t.subst_var(&mut f)).collect(),
10681095
}
@@ -1073,13 +1100,37 @@ impl<V> Atom<V> {
10731100
F: FnMut(V) -> W,
10741101
{
10751102
Atom {
1103+
guard: self.guard.map(|fo| Box::new(fo.map_var(&mut f))),
10761104
pred: self.pred,
10771105
args: self.args.into_iter().map(|t| t.map_var(&mut f)).collect(),
10781106
}
10791107
}
10801108

10811109
pub fn fv(&self) -> impl Iterator<Item = &V> {
1082-
self.args.iter().flat_map(|t| t.fv())
1110+
let guard_fvs: Box<dyn Iterator<Item = &V>> = if let Some(guard) = &self.guard {
1111+
Box::new(guard.fv())
1112+
} else {
1113+
Box::new(std::iter::empty())
1114+
};
1115+
self.args.iter().flat_map(|t| t.fv()).chain(guard_fvs)
1116+
}
1117+
1118+
pub fn guarded(self, new_guard: Formula<V>) -> Atom<V> {
1119+
let Atom {
1120+
guard: self_guard,
1121+
pred,
1122+
args,
1123+
} = self;
1124+
let guard = if let Some(self_guard) = self_guard {
1125+
self_guard.and(new_guard)
1126+
} else {
1127+
new_guard
1128+
};
1129+
Atom {
1130+
guard: Some(Box::new(guard)),
1131+
pred,
1132+
args,
1133+
}
10831134
}
10841135
}
10851136

@@ -1456,6 +1507,22 @@ impl<V> Body<V> {
14561507
}
14571508
}
14581509

1510+
impl<V> Body<V>
1511+
where
1512+
V: Var,
1513+
{
1514+
pub fn guarded(self, guard: Formula<V>) -> Body<V> {
1515+
let Body { atoms, formula } = self;
1516+
Body {
1517+
atoms: atoms
1518+
.into_iter()
1519+
.map(|a| a.guarded(guard.clone()))
1520+
.collect(),
1521+
formula: guard.not().or(formula),
1522+
}
1523+
}
1524+
}
1525+
14591526
impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Body<V>
14601527
where
14611528
V: Var,

‎src/chc/smtlib2.rs‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -223,6 +223,10 @@ pub struct Atom<'ctx, 'a> {
223223

224224
impl<'ctx, 'a> std::fmt::Display for Atom<'ctx, 'a> {
225225
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
226+
if let Some(guard) = &self.inner.guard {
227+
let guard = Formula::new(self.ctx, self.clause, guard);
228+
write!(f, "(=> {} ", guard)?;
229+
}
226230
if self.inner.pred.is_negative() {
227231
write!(f, "(not ")?;
228232
}
@@ -244,6 +248,9 @@ impl<'ctx, 'a> std::fmt::Display for Atom<'ctx, 'a> {
244248
if self.inner.pred.is_negative() {
245249
write!(f, ")")?;
246250
}
251+
if self.inner.guard.is_some() {
252+
write!(f, ")")?;
253+
}
247254
Ok(())
248255
}
249256
}

‎src/chc/unbox.rs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,9 +24,10 @@ fn unbox_term(term: Term) -> Term {
2424
}
2525

2626
fn unbox_atom(atom: Atom) -> Atom {
27-
let Atom { pred, args } = atom;
27+
let Atom { guard, pred, args } = atom;
28+
let guard = guard.map(|fo| Box::new(unbox_formula(*fo)));
2829
let args = args.into_iter().map(unbox_term).collect();
29-
Atom { pred, args }
30+
Atom { guard, pred, args }
3031
}
3132

3233
fn unbox_datatype_sort(sort: DatatypeSort) -> DatatypeSort {

‎src/refine/env.rs‎

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -730,6 +730,12 @@ impl Env {
730730
let def = self.enum_defs[&ty.symbol].clone();
731731
let matcher_pred = chc::MatcherPred::new(ty.symbol.clone(), ty.arg_sorts());
732732

733+
let discr_var = self
734+
.temp_vars
735+
.push(TempVarBinding::Type(rty::RefinedType::unrefined(
736+
rty::Type::int(),
737+
)));
738+
733739
let mut variants = IndexVec::new();
734740
for variant_def in &def.variants {
735741
let mut fields = IndexVec::new();
@@ -738,7 +744,12 @@ impl Env {
738744
fields.push(x);
739745
let mut field_ty = rty::RefinedType::unrefined(field_ty.clone().vacuous());
740746
field_ty.instantiate_ty_params(ty.args.clone());
741-
self.bind_impl(x.into(), field_ty.boxed(), depth);
747+
let guarded_field_ty = field_ty.guarded(
748+
chc::Term::var(discr_var.into())
749+
.equal_to(chc::Term::int(variant_def.discr as i64))
750+
.into(),
751+
);
752+
self.bind_impl(x.into(), guarded_field_ty.boxed(), depth);
742753
}
743754
variants.push(FlowBindingVariant { fields });
744755
}
@@ -773,11 +784,6 @@ impl Env {
773784
assumption
774785
.body
775786
.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-
)));
781787
assumption
782788
.body
783789
.push_conj(

‎src/rty.rs‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1172,6 +1172,19 @@ impl<V> Formula<V> {
11721172
}
11731173
}
11741174

1175+
impl<V> Formula<V>
1176+
where
1177+
V: chc::Var,
1178+
{
1179+
pub fn guarded(self, guard: chc::Formula<V>) -> Self {
1180+
let Formula { existentials, body } = self;
1181+
Formula {
1182+
existentials,
1183+
body: body.guarded(guard),
1184+
}
1185+
}
1186+
}
1187+
11751188
impl<V> Formula<V>
11761189
where
11771190
V: ShiftExistential,
@@ -1351,6 +1364,15 @@ impl<FV> RefinedType<FV> {
13511364
RefinedType { ty, refinement }
13521365
}
13531366

1367+
pub fn guarded(self, guard: chc::Formula<FV>) -> Self
1368+
where
1369+
FV: chc::Var,
1370+
{
1371+
let RefinedType { ty, refinement } = self;
1372+
let refinement = refinement.guarded(guard.map_var(RefinedTypeVar::Free));
1373+
RefinedType { ty, refinement }
1374+
}
1375+
13541376
/// Returns a dereferenced type of the immutable reference or owned pointer.
13551377
///
13561378
/// e.g. `{ v: Box<T> | φ } --> { v: T | φ[box v/v] }`

‎tests/ui/fail/adt_variant_without_params.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/adt_variant_without_params.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)