Skip to content

Commit 878b9e4

Browse files
committed
Don't apply *&mut simplification during typing
This results in imprecise rules.
1 parent b0d5fa0 commit 878b9e4

13 files changed

+29
-47
lines changed

src/solvers/typing_rules.rs

+4-22
Original file line numberDiff line numberDiff line change
@@ -153,13 +153,7 @@ impl<'a> TypingPredicate<'a> {
153153
T::Ref(inner_mtbl, _) => {
154154
rule_variant = o.inherited_ref_on_ref;
155155
match o.inherited_ref_on_ref {
156-
InheritedRefOnRefBehavior::EatOuter => {
157-
if o.simplify_deref_mut && bm_mtbl == Mutable {
158-
underlying_place
159-
} else {
160-
self.expr.deref(a)
161-
}
162-
}
156+
InheritedRefOnRefBehavior::EatOuter => self.expr.deref(a),
163157
InheritedRefOnRefBehavior::EatInner => {
164158
let can_eat_inner = match (p_mtbl, *inner_mtbl) {
165159
(Shared, Shared) => true,
@@ -175,11 +169,7 @@ impl<'a> TypingPredicate<'a> {
175169
underlying_place.deref(a)
176170
} else if o.fallback_to_outer {
177171
fallback_to_outer = FallbackToOuter(true);
178-
if o.simplify_deref_mut && bm_mtbl == Mutable {
179-
underlying_place
180-
} else {
181-
self.expr.deref(a)
182-
}
172+
self.expr.deref(a)
183173
} else {
184174
return Err(TypeError::MutabilityMismatch);
185175
}
@@ -198,11 +188,7 @@ impl<'a> TypingPredicate<'a> {
198188
underlying_place.deref(a)
199189
} else if o.fallback_to_outer {
200190
fallback_to_outer = FallbackToOuter(true);
201-
if o.simplify_deref_mut && bm_mtbl == Mutable {
202-
underlying_place
203-
} else {
204-
self.expr.deref(a)
205-
}
191+
self.expr.deref(a)
206192
} else {
207193
return Err(TypeError::MutabilityMismatch);
208194
}
@@ -215,11 +201,7 @@ impl<'a> TypingPredicate<'a> {
215201
T::Tuple(_) | T::OtherNonRef(_) | T::AbstractNonRef(..)
216202
if o.eat_inherited_ref_alone =>
217203
{
218-
if o.simplify_deref_mut && bm_mtbl == Mutable {
219-
underlying_place
220-
} else {
221-
self.expr.deref(a)
222-
}
204+
self.expr.deref(a)
223205
}
224206
T::Tuple(_) | T::OtherNonRef(_) | T::AbstractNonRef(..) => {
225207
return Err(TypeError::InheritedRefIsAlone);

tests/snapshots/[email protected]

+3-3
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ p @ *e: T
6262
---------------------------------------- "Deref(EatOuter)"
6363
&mut p @ e: &mut T, e is not a reference
6464

65-
p @ e: T
65+
p @ *&mut e: T
6666
--------------------------------------------- "Deref(EatOuter)"
6767
&mut p @ &mut e: &mut T, T is not a reference
6868

@@ -78,7 +78,7 @@ p @ &mut *e: &mut T
7878
--------------------------------------- "Deref(EatInner)"
7979
&mut p @ &mut e: &mut &mut T, e mutable
8080

81-
p @ e: &T
81+
p @ *&mut e: &T
8282
------------------------ "Deref(EatInner, FallbackToOuter)"
8383
&mut p @ &mut e: &mut &T
8484

@@ -94,7 +94,7 @@ p @ *&*e: T
9494
------------------------------------ "DerefMutWithShared(EatOuter)"
9595
&p @ e: &mut T, e is not a reference
9696

97-
p @ *&e: T
97+
p @ *&*&mut e: T
9898
----------------------------------------- "DerefMutWithShared(EatOuter)"
9999
&p @ &mut e: &mut T, T is not a reference
100100

tests/snapshots/[email protected]

+1-1
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ inh, rw ⊢ p: &mut T
7878
----------------------------- "Deref(EatInner)"
7979
inh, rw&mut p: &mut &mut T
8080

81-
r, mp: &T
81+
real, mp: &T
8282
------------------------ "Deref(EatInner, FallbackToOuter)"
8383
inh, m&mut p: &mut &T
8484

tests/snapshots/[email protected]

+2-2
Original file line numberDiff line numberDiff line change
@@ -110,8 +110,8 @@ ref mut, rw ⊢ p: T
110110
---------------------------- "Deref(EatInner)"
111111
ref mut, rw&mut p: &mut T
112112

113-
move or ref, mp: &T or T
114-
--------------------------- "Deref(EatInner, FallbackToOuter)"
113+
move, mp: &T
114+
----------------------- "Deref(EatInner, FallbackToOuter)"
115115
ref mut, m&mut p: &T
116116

117117
ref, rop: T

tests/snapshots/bundle_rules@rfc3627_2021-Expression.snap

+3-3
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ p @ *e: T
6262
---------------------------------------- "Deref(EatOuter)"
6363
&mut p @ e: &mut T, e is not a reference
6464

65-
p @ e: T
65+
p @ *&mut e: T
6666
--------------------------------------------- "Deref(EatOuter)"
6767
&mut p @ &mut e: &mut T, T is not a reference
6868

@@ -82,15 +82,15 @@ p @ *e: T
8282
---------------------------- "Deref(EatBoth)"
8383
&mut p @ &mut e: &mut &mut T
8484

85-
p @ e: &T
85+
p @ *&mut e: &T
8686
------------------------ "Deref(EatBoth, FallbackToOuter)"
8787
&mut p @ &mut e: &mut &T
8888

8989
p @ *&*e: T
9090
------------------------------------ "DerefMutWithShared(EatOuter)"
9191
&p @ e: &mut T, e is not a reference
9292

93-
p @ *&e: T
93+
p @ *&*&mut e: T
9494
----------------------------------------- "DerefMutWithShared(EatOuter)"
9595
&p @ &mut e: &mut T, T is not a reference
9696

tests/snapshots/bundle_rules@rfc3627_2021-Sequent.snap

+1-1
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ real, m ⊢ p: T
8282
---------------------------- "Deref(EatBoth)"
8383
inh, m&mut p: &mut &mut T
8484

85-
r, mp: &T
85+
real, mp: &T
8686
------------------------ "Deref(EatBoth, FallbackToOuter)"
8787
inh, m&mut p: &mut &T
8888

tests/snapshots/bundle_rules@rfc3627_2021-SequentBindingMode.snap

+2-2
Original file line numberDiff line numberDiff line change
@@ -114,8 +114,8 @@ move, m ⊢ p: T
114114
--------------------------- "Deref(EatBoth)"
115115
ref mut, m&mut p: &mut T
116116

117-
move or ref, mp: &T or T
118-
--------------------------- "Deref(EatBoth, FallbackToOuter)"
117+
move, mp: &T
118+
----------------------- "Deref(EatBoth, FallbackToOuter)"
119119
ref mut, m&mut p: &T
120120

121121
move, rop: T

tests/snapshots/[email protected]

+3-3
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ The old ruleset is on the left, and the new one on the right.
6565
--------------------------------------------- "Deref" | --------------------------------------------- "Deref(EatOuter)"
6666
inh, m&mut p: &mut T, T is not a reference | inh, m&mut p: &mut T, T is not a reference
6767

68-
real, mp: &T | r, mp: &T
68+
real, mp: &T | real, mp: &T
6969
------------------------ "Deref" | ------------------------ "Deref(EatInner, FallbackToOuter)"
7070
inh, m&mut p: &mut &T | inh, m&mut p: &mut &T
7171

@@ -251,8 +251,8 @@ ref mut, rw ⊢ p: T
251251
---------------------------- "Deref(EatInner)"
252252
ref mut, rw&mut p: &mut T
253253

254-
move or ref, mp: &T or T
255-
--------------------------- "Deref(EatInner, FallbackToOuter)"
254+
move, mp: &T
255+
----------------------- "Deref(EatInner, FallbackToOuter)"
256256
ref mut, m&mut p: &T
257257

258258
ref, rop: T

tests/snapshots/[email protected]

+1-1
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ The old ruleset is on the left, and the new one on the right.
6565
--------------------------------------------- "Deref" | --------------------------------------------- "Deref(EatOuter)"
6666
inh, m&mut p: &mut T, T is not a reference | inh, m&mut p: &mut T, T is not a reference
6767

68-
real, mp: &T | r, mp: &T
68+
real, mp: &T | real, mp: &T
6969
------------------------ "Deref" | ------------------------ "Deref(EatInner, FallbackToOuter)"
7070
inh, m&mut p: &mut &T | inh, m&mut p: &mut &T
7171

tests/snapshots/[email protected]

+2-2
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,9 @@ info:
1919
// Applying rule `ConstructorRef`
2020
&mut x @ &mut (*s).0: &mut &T
2121
// Applying rule `Deref(EatInner, FallbackToOuter)`
22-
x @ (*s).0: &T
22+
x @ *&mut (*s).0: &T
2323
// Applying rule `Binding`
24-
let x: &T = (*s).0
24+
let x: &T = *&mut (*s).0
2525

2626
// Final bindings (simplified):
2727
let x: &T = (*s).0;

tests/snapshots/[email protected]

+2-2
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,9 @@ info:
1919
// Applying rule `ConstructorRef`
2020
&mut x @ &mut (*s).0: &mut &T
2121
// Applying rule `Deref`
22-
x @ (*s).0: &T
22+
x @ *&mut (*s).0: &T
2323
// Applying rule `Binding`
24-
let x: &T = (*s).0
24+
let x: &T = *&mut (*s).0
2525

2626
// Final bindings (simplified):
2727
let x: &T = (*s).0;

tests/snapshots/[email protected]

+3-3
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,11 @@ info:
1919
// Applying rule `ConstructorRef`
2020
&mut ref mut x @ &mut (*s).0: &mut &T
2121
// Applying rule `Deref(EatInner, FallbackToOuter)`
22-
ref mut x @ (*s).0: &T
22+
ref mut x @ *&mut (*s).0: &T
2323
// Applying rule `BindingBorrow`
24-
x @ &mut (*s).0: &mut &T
24+
x @ &mut *&mut (*s).0: &mut &T
2525
// Applying rule `Binding`
26-
let x: &mut &T = &mut (*s).0
26+
let x: &mut &T = &mut *&mut (*s).0
2727

2828
// Final bindings (simplified):
2929
let x: &mut &T = &mut (*s).0;

tests/snapshots/[email protected]

+2-2
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,9 @@ info:
1919
// Applying rule `ConstructorRef`
2020
&x @ &mut (*s).0: &mut &T
2121
// Applying rule `DerefMutWithShared`
22-
x @ *&(*s).0: &T
22+
x @ *&*&mut (*s).0: &T
2323
// Applying rule `Binding`
24-
let x: &T = *&(*s).0
24+
let x: &T = *&*&mut (*s).0
2525

2626
// Final bindings (simplified):
2727
let x: &T = (*s).0;

0 commit comments

Comments
 (0)