Non exhaustiveness of patterns #1318

gzanitti · 2024-04-25T14:10:47Z

This PR implements non-exhaustiveness check for matchs (issue #1287). Based on the usefulness implementation proposed in the rustc_pattern_analysis[1] module of the Rust compiler. A match is exhaustive iff the wildcard _ pattern is not useful with respect to the patterns in the match. The values returned by usefulness are used to tell the user which values are missing ([] where the match is exhaustive).

Still in draft until I finish analyzing some edge cases.

[1] https://doc.rust-lang.org/nightly/nightly-rustc/rustc_pattern_analysis/usefulness/index.html

…ed on rustc usefulness

…function. Some tests still failing

ast/src/parsed/mod.rs

chriseth · 2024-04-25T15:55:47Z

Ah nice! I asked because I was not sure if the other function is maybe different. One small note: I think currently an enum variant is always marked as refutable, but with this checker, I think we should be more exact: It is irrefutable if and only if it is the only variant of the enum.

gzanitti · 2024-04-25T16:12:23Z

Ah nice! I asked because I was not sure if the other function is maybe different. One small note: I think currently an enum variant is always marked as refutable, but with this checker, I think we should be more exact: It is irrefutable if and only if it is the only variant of the enum.

Cool! Just to confirm:

enum Name {
    Variant1,
    Variant2,
}

is represented as Enum(Name, [Variant1, Variant2]), right?

Btw, I need to check/fix an edge cases with respect to the use of elipsis inside arrays, and I think this PR will be ready to be reviewed :)

ast/src/parsed/mod.rs

chriseth · 2024-04-25T16:29:02Z

Cool! Just to confirm:
enum Name {
    Variant1,
    Variant2,
}
is represented as Enum(Name, [Variant1, Variant2]), right?

Not sure I understood correctly but given that enum declaration, we could use it in a pattern like this:

match x {
  Name::Variant1 => ...,
  Name::Variant2 => ...,
}

The second parameter of Pattern::Enum is the data fields of an enum if it has them, i.e. Name::Variant1(x, 2) => ....

If you consider the following enum definition:

enum SingleVarEnum {
  Var(int, int)
}

Then we could do the following because the pattern is irrefutable:

let SingleVarEnum::Var(x, y) = m;

Of course we still need to check that the inner patterns are all irrefutable, so it would not work for let SingleVar:Enum::Var(1, y) = m.

ast/src/parsed/pattern.rs

pil-analyzer/src/pil_analyzer.rs

gzanitti · 2024-04-26T13:30:58Z

Thanks for your comments @chriseth. Last night I found a small bug when specializing patterns with internal parameters (like arrays and tuples). I'll fix that and take care of all your comments. It should be ready by tonight, sorry if it's taking longer than expected.

chriseth · 2024-04-26T13:44:00Z

No worries, take your time, it's not easy navigating in a new codebase.

…rns inside tuples, arrays, etc

ast/src/parsed/pattern.rs

Co-authored-by: chriseth <chris@ethereum.org>

…tiveness_of_patterns

chriseth · 2024-04-30T09:42:29Z

ast/src/parsed/pattern.rs

+
+use super::{asm::SymbolPath, visitor::Children};
+
+/// When a pattern is specialised, in some cases the algorithm will return


Maybe it makes sense to move this a bit down so that Pattern is the first element in this file?

chriseth · 2024-04-30T09:43:10Z

ast/src/parsed/pattern.rs

+
+    /// Check for irrefutable patterns in pattern tuples. Since pattern tuples can contain
+    /// internal patterns, irrefutability only applies in cases of unique patterns (len == 1).
+


Does this work fine if you have an empty line without comment?

chriseth · 2024-04-30T09:48:13Z

ast/src/parsed/pattern.rs

+    /// If (_, _) was obtained from specialization, it is not true that the pattern is irrefutable
+    /// because having more than one element implies that the evaluation is performed on internal patterns.
+    /// If, on the other hand, the pattern tuple is `(Pattern::Tuple(_,_), )``, irrefutability applies in the standard way.
+    pub fn is_irrefutable(&self) -> bool {


Hm, I cannot find any use of this function...

chriseth · 2024-04-30T09:57:45Z

ast/src/parsed/pattern.rs

+    /// If the constructor is shared with the pattern, specialize the pattern removing
+    /// "one layer" (the constructor) and returning internal patterns.
+    /// Return None if the pattern can't be specialized with the constructor or if the pattern is empty.


I still don't really understand this routine, but maybe adding the following items to the docstring helps:

We are only interested in the outermost type-constructor of the constructor pattern and ignore the fields and the inner patterns.

And maybe also a variant of the following:

matches!(c(v_1, .., v_n), p) <=> specialize(c, p) returns something && matches!((v_1, .., v_n), specialize(c, p))

chriseth · 2024-04-30T09:58:31Z

ast/src/parsed/pattern.rs

+    }
+}
+
+impl Default for PatternTuple {


Isn't that the same as derive(Default)?

chriseth · 2024-04-30T10:02:33Z

ast/src/parsed/pattern.rs

+    /// If the constructor is shared with the pattern, specialize the pattern removing
+    /// "one layer" (the constructor) and returning internal patterns.
+    /// Return None if the pattern can't be specialized using the constructor.


Ok, I think this part I understand now. Let me rephrase it in my own words and then we can see how we want to combine the docs.

Suggested change

/// If the constructor is shared with the pattern, specialize the pattern removing

/// "one layer" (the constructor) and returning internal patterns.

/// Return None if the pattern can't be specialized using the constructor.

/// We are only interested in the type constructor part of `constructor` and ignore the inner patterns and fields.

/// If the constructor does not match the pattern, returns None.

/// If it matches, returns a vector of the inner fields of the pattern.

And then maybe add some formal statement like on https://doc.rust-lang.org/nightly/nightly-rustc/rustc_pattern_analysis/usefulness/index.html#specialization

Ok it seems I still have not understood it :)
The returned patterns correspond to the sub-items of the constructor, not of the pattern, right?
But they are taken from the pattern.

chriseth · 2024-04-30T10:03:15Z

ast/src/parsed/pattern.rs

+    pub fn specialize(&self, constructor: &Self) -> Option<PatternTuple> {
+        match (constructor, self) {
+            (_, Pattern::CatchAll) => Some(PatternTuple { patterns: vec![] }),
+            (Pattern::CatchAll, _) => None,


I'm wondering, shouldn't this panic? CatchAll is not a constructor, is it?

chriseth · 2024-04-30T10:05:48Z

ast/src/parsed/pattern.rs

+            }),
+
+            (Pattern::Enum(path1, patterns1), Pattern::Enum(path2, patterns2)) => {
+                if path1 != path2 {


Could be pulled into the match pattern

chriseth · 2024-04-30T10:06:21Z

ast/src/parsed/pattern.rs

+                if path1 != path2 {
+                    return None;
+                }
+                match (patterns1, patterns2) {


Suggested change

match (patterns1, patterns2) {

match (cons_patterns, patterns) {

chriseth · 2024-04-30T10:07:46Z

ast/src/parsed/pattern.rs

+                        let pats = patterns2.as_ref().unwrap();
+                        Some(PatternTuple {
+                            patterns: pats.clone(),
+                        })


Suggested change

let pats = patterns2.as_ref().unwrap();

Some(PatternTuple {

patterns: pats.clone(),

})

Some(PatternTuple {

patterns: patterns2.as_ref().unwrap().clone(),

})

(or maybe even .cloned() cold work here?)

Oh wait, why don't you use Some(patterns) instead of Some(_) one line above?

chriseth · 2024-04-30T10:09:17Z

ast/src/parsed/pattern.rs

+            (Pattern::Array(cons_patterns), Pattern::Array(patterns)) => {
+                let max_len = cons_patterns.len();
+                let mut constructors = Vec::new();
+                if patterns.contains(&Pattern::Ellipsis) {


Suggested change

if patterns.contains(&Pattern::Ellipsis) {

if let Some(ellipsis_inde) = patterns.iter().position(|p| p ==&Pattern::Ellipsis) {

chriseth · 2024-04-30T10:12:29Z

ast/src/parsed/pattern.rs

+                })
+            }
+            (Pattern::Array(cons_patterns), Pattern::Array(patterns)) => {
+                let max_len = cons_patterns.len();


cons_len? Also please pull it into the block where it is used.

chriseth · 2024-04-30T10:14:12Z

ast/src/parsed/pattern.rs

+            (Pattern::Array(cons_patterns), Pattern::Array(patterns)) => {
+                let max_len = cons_patterns.len();
+                let mut constructors = Vec::new();
+                if patterns.contains(&Pattern::Ellipsis) {


Can we assert that the constructor does not contain an ellipsis?

chriseth · 2024-04-30T10:15:25Z

ast/src/parsed/pattern.rs

+                let mut constructors = Vec::new();
+                if patterns.contains(&Pattern::Ellipsis) {


Suggested change

let mut constructors = Vec::new();

if patterns.contains(&Pattern::Ellipsis) {

let constructorns = if patterns.contains(&Pattern::Ellipsis) {

chriseth · 2024-04-30T10:19:07Z

pil-analyzer/src/pil_analyzer.rs

@@ -381,6 +423,61 @@ impl PILAnalyzer {
    fn driver(&self) -> Driver {
        Driver(self)
    }
+
+    /// Check if a new pattern is useful in a set of patterns.


What is the new pattern here?

gzanitti added 11 commits April 23, 2024 10:35

Basic skeleton. Exploring the basecode

d108d21

First attempt of the specialize function. Tests need to be added. Bas…

f33a435

…ed on rustc usefulness

Better implementation of specialize. Constructors are created inside …

7a0c9b3

…function. Some tests still failing

Unspecialize function: Basic skeleton. Edge cases need to be addressed.

1636221

Non-recursive specialize function

727f20b

Usefulness with basics cases working

ad09597

Exhaustiveness check: high level function

c66b3e2

Minor changes

c20fa1f

Clippy

854c0ca

More on Clippy

5b65cac

More on Clippy

2913469

chriseth reviewed Apr 25, 2024

View reviewed changes

ast/src/parsed/mod.rs Outdated Show resolved Hide resolved

Fix issue with irrefutability

a453c6d

chriseth reviewed Apr 25, 2024

View reviewed changes

ast/src/parsed/mod.rs Outdated Show resolved Hide resolved

gzanitti added 3 commits April 25, 2024 14:16

Patterns moved to a new file

f2954c5

Conflict solved

28fc7f7

Minor fixes

503a9bd