Skip to content

Commit

Permalink
Don't apply *&mut simplification during typing
Browse files Browse the repository at this point in the history 
This results in imprecise rules.
  • Loading branch information
@Nadrieril
Nadrieril committed Jan 1, 2025
1 parent b0d5fa0 commit 878b9e4
Show file tree
Hide file tree
Showing 13 changed files with 29 additions and 47 deletions.
26 changes: 4 additions & 22 deletions src/solvers/typing_rules.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,13 +153,7 @@ impl<'a> TypingPredicate<'a> {
T::Ref(inner_mtbl, _) => {
rule_variant = o.inherited_ref_on_ref;
match o.inherited_ref_on_ref {
InheritedRefOnRefBehavior::EatOuter => {
if o.simplify_deref_mut && bm_mtbl == Mutable {
underlying_place
} else {
self.expr.deref(a)
}
}
InheritedRefOnRefBehavior::EatOuter => self.expr.deref(a),
InheritedRefOnRefBehavior::EatInner => {
let can_eat_inner = match (p_mtbl, *inner_mtbl) {
(Shared, Shared) => true,
Expand All @@ -175,11 +169,7 @@ impl<'a> TypingPredicate<'a> {
underlying_place.deref(a)
} else if o.fallback_to_outer {
fallback_to_outer = FallbackToOuter(true);
if o.simplify_deref_mut && bm_mtbl == Mutable {
underlying_place
} else {
self.expr.deref(a)
}
self.expr.deref(a)
} else {
return Err(TypeError::MutabilityMismatch);
}
Expand All @@ -198,11 +188,7 @@ impl<'a> TypingPredicate<'a> {
underlying_place.deref(a)
} else if o.fallback_to_outer {
fallback_to_outer = FallbackToOuter(true);
if o.simplify_deref_mut && bm_mtbl == Mutable {
underlying_place
} else {
self.expr.deref(a)
}
self.expr.deref(a)
} else {
return Err(TypeError::MutabilityMismatch);
}
Expand All @@ -215,11 +201,7 @@ impl<'a> TypingPredicate<'a> {
T::Tuple(_) | T::OtherNonRef(_) | T::AbstractNonRef(..)
if o.eat_inherited_ref_alone =>
{
if o.simplify_deref_mut && bm_mtbl == Mutable {
underlying_place
} else {
self.expr.deref(a)
}
self.expr.deref(a)
}
T::Tuple(_) | T::OtherNonRef(_) | T::AbstractNonRef(..) => {
return Err(TypeError::InheritedRefIsAlone);
Expand Down
6 changes: 3 additions & 3 deletions tests/snapshots/bundle_rules@rfc3627-Expression.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ p @ *e: T
---------------------------------------- "Deref(EatOuter)"
&mut p @ e: &mut T, e is not a reference

p @ e: T
p @ *&mut e: T
--------------------------------------------- "Deref(EatOuter)"
&mut p @ &mut e: &mut T, T is not a reference

Expand All @@ -78,7 +78,7 @@ p @ &mut *e: &mut T
--------------------------------------- "Deref(EatInner)"
&mut p @ &mut e: &mut &mut T, e mutable

p @ e: &T
p @ *&mut e: &T
------------------------ "Deref(EatInner, FallbackToOuter)"
&mut p @ &mut e: &mut &T

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

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

Expand Down
2 changes: 1 addition & 1 deletion tests/snapshots/bundle_rules@rfc3627-Sequent.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ inh, rw ⊢ p: &mut T
----------------------------- "Deref(EatInner)"
inh, rw ⊢ &mut p: &mut &mut T

r, m ⊢ p: &T
real, m ⊢ p: &T
------------------------ "Deref(EatInner, FallbackToOuter)"
inh, m ⊢ &mut p: &mut &T

Expand Down
4 changes: 2 additions & 2 deletions tests/snapshots/bundle_rules@rfc3627-SequentBindingMode.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,8 +110,8 @@ ref mut, rw ⊢ p: T
---------------------------- "Deref(EatInner)"
ref mut, rw ⊢ &mut p: &mut T

move or ref, m ⊢ p: &T or T
--------------------------- "Deref(EatInner, FallbackToOuter)"
move, m ⊢ p: &T
----------------------- "Deref(EatInner, FallbackToOuter)"
ref mut, m ⊢ &mut p: &T

ref, ro ⊢ p: T
Expand Down
6 changes: 3 additions & 3 deletions tests/snapshots/bundle_rules@rfc3627_2021-Expression.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ p @ *e: T
---------------------------------------- "Deref(EatOuter)"
&mut p @ e: &mut T, e is not a reference

p @ e: T
p @ *&mut e: T
--------------------------------------------- "Deref(EatOuter)"
&mut p @ &mut e: &mut T, T is not a reference

Expand All @@ -82,15 +82,15 @@ p @ *e: T
---------------------------- "Deref(EatBoth)"
&mut p @ &mut e: &mut &mut T

p @ e: &T
p @ *&mut e: &T
------------------------ "Deref(EatBoth, FallbackToOuter)"
&mut p @ &mut e: &mut &T

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

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

Expand Down
2 changes: 1 addition & 1 deletion tests/snapshots/bundle_rules@rfc3627_2021-Sequent.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ real, m ⊢ p: T
---------------------------- "Deref(EatBoth)"
inh, m ⊢ &mut p: &mut &mut T

r, m ⊢ p: &T
real, m ⊢ p: &T
------------------------ "Deref(EatBoth, FallbackToOuter)"
inh, m ⊢ &mut p: &mut &T

Expand Down
4 changes: 2 additions & 2 deletions tests/snapshots/bundle_rules@rfc3627_2021-SequentBindingMode.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,8 +114,8 @@ move, m ⊢ p: T
--------------------------- "Deref(EatBoth)"
ref mut, m ⊢ &mut p: &mut T

move or ref, m ⊢ p: &T or T
--------------------------- "Deref(EatBoth, FallbackToOuter)"
move, m ⊢ p: &T
----------------------- "Deref(EatBoth, FallbackToOuter)"
ref mut, m ⊢ &mut p: &T

move, ro ⊢ p: T
Expand Down
6 changes: 3 additions & 3 deletions tests/snapshots/trace_cli@13123596375905619773.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ The old ruleset is on the left, and the new one on the right.
--------------------------------------------- "Deref" | --------------------------------------------- "Deref(EatOuter)"
inh, m ⊢ &mut p: &mut T, T is not a reference | inh, m ⊢ &mut p: &mut T, T is not a reference

real, m ⊢ p: &T | r, m ⊢ p: &T
real, m ⊢ p: &T | real, m ⊢ p: &T
------------------------ "Deref" | ------------------------ "Deref(EatInner, FallbackToOuter)"
inh, m ⊢ &mut p: &mut &T | inh, m ⊢ &mut p: &mut &T

Expand Down Expand Up @@ -251,8 +251,8 @@ ref mut, rw ⊢ p: T
---------------------------- "Deref(EatInner)"
ref mut, rw ⊢ &mut p: &mut T

move or ref, m ⊢ p: &T or T
--------------------------- "Deref(EatInner, FallbackToOuter)"
move, m ⊢ p: &T
----------------------- "Deref(EatInner, FallbackToOuter)"
ref mut, m ⊢ &mut p: &T

ref, ro ⊢ p: T
Expand Down
2 changes: 1 addition & 1 deletion tests/snapshots/trace_cli@13149991652265668877.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ The old ruleset is on the left, and the new one on the right.
--------------------------------------------- "Deref" | --------------------------------------------- "Deref(EatOuter)"
inh, m ⊢ &mut p: &mut T, T is not a reference | inh, m ⊢ &mut p: &mut T, T is not a reference

real, m ⊢ p: &T | r, m ⊢ p: &T
real, m ⊢ p: &T | real, m ⊢ p: &T
------------------------ "Deref" | ------------------------ "Deref(EatInner, FallbackToOuter)"
inh, m ⊢ &mut p: &mut &T | inh, m ⊢ &mut p: &mut &T

Expand Down
4 changes: 2 additions & 2 deletions tests/snapshots/trace_solver@14494172193295975470.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,9 @@ info:
// Applying rule `ConstructorRef`
&mut x @ &mut (*s).0: &mut &T
// Applying rule `Deref(EatInner, FallbackToOuter)`
x @ (*s).0: &T
x @ *&mut (*s).0: &T
// Applying rule `Binding`
let x: &T = (*s).0
let x: &T = *&mut (*s).0

// Final bindings (simplified):
let x: &T = (*s).0;
4 changes: 2 additions & 2 deletions tests/snapshots/trace_solver@15812390388585360924.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,9 @@ info:
// Applying rule `ConstructorRef`
&mut x @ &mut (*s).0: &mut &T
// Applying rule `Deref`
x @ (*s).0: &T
x @ *&mut (*s).0: &T
// Applying rule `Binding`
let x: &T = (*s).0
let x: &T = *&mut (*s).0

// Final bindings (simplified):
let x: &T = (*s).0;
6 changes: 3 additions & 3 deletions tests/snapshots/trace_solver@16124590782743649599.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,11 @@ info:
// Applying rule `ConstructorRef`
&mut ref mut x @ &mut (*s).0: &mut &T
// Applying rule `Deref(EatInner, FallbackToOuter)`
ref mut x @ (*s).0: &T
ref mut x @ *&mut (*s).0: &T
// Applying rule `BindingBorrow`
x @ &mut (*s).0: &mut &T
x @ &mut *&mut (*s).0: &mut &T
// Applying rule `Binding`
let x: &mut &T = &mut (*s).0
let x: &mut &T = &mut *&mut (*s).0

// Final bindings (simplified):
let x: &mut &T = &mut (*s).0;
4 changes: 2 additions & 2 deletions tests/snapshots/trace_solver@3701612019380849062.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,9 @@ info:
// Applying rule `ConstructorRef`
&x @ &mut (*s).0: &mut &T
// Applying rule `DerefMutWithShared`
x @ *&(*s).0: &T
x @ *&*&mut (*s).0: &T
// Applying rule `Binding`
let x: &T = *&(*s).0
let x: &T = *&*&mut (*s).0

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

0 comments on commit 878b9e4

Please sign in to comment.