Dafny: let verifier, not the resolver, check for missing cases in match expressions/statements

7 files changed, 208 insertions, 25 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index f1a649ee..800585bd 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -795,21 +795,22 @@ namespace Microsoft.Dafny {
         // } else if (true) {

         //   ...

         // }

+        if (s.Cases.Count != 0) {

+          string source = "_source" + tmpVarCount;

+          tmpVarCount++;

+          Indent(indent);

+          wr.Write("{0} {1} = ", TypeName(cce.NonNull(s.Source.Type)), source);

+          TrExpr(s.Source);

+          wr.WriteLine(";");

 

-        string source = "_source" + tmpVarCount;

-        tmpVarCount++;

-        Indent(indent);

-        wr.Write("{0} {1} = ", TypeName(cce.NonNull(s.Source.Type)), source);

-        TrExpr(s.Source);

-        wr.WriteLine(";");

-        

-        int i = 0;

-        foreach (MatchCaseStmt mc in s.Cases) {

-          MatchCasePrelude(source, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent);

-          TrStmtList(mc.Body, indent);

-          i++;

+          int i = 0;

+          foreach (MatchCaseStmt mc in s.Cases) {

+            MatchCasePrelude(source, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent);

+            TrStmtList(mc.Body, indent);

+            i++;

+          }

+          Indent(indent); wr.WriteLine("}");

         }

-        Indent(indent);  wr.WriteLine("}");

 

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index d83560e0..04d92539 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1642,10 +1642,12 @@ namespace Microsoft.Dafny {
     void ObjectInvariant() {

       Contract.Invariant(Source != null);

       Contract.Invariant(cce.NonNullElements(Cases));

+      Contract.Invariant(cce.NonNullElements(MissingCases));

     }

 

     public readonly Expression Source;

     public readonly List<MatchCaseStmt/*!*/>/*!*/ Cases;

+    public readonly List<DatatypeCtor/*!*/> MissingCases = new List<DatatypeCtor>();  // filled in during resolution

 

     public MatchStmt(IToken tok, Expression source, [Captured] List<MatchCaseStmt/*!*/>/*!*/ cases)

       : base(tok) {

@@ -2490,10 +2492,13 @@ namespace Microsoft.Dafny {
   public class MatchExpr : Expression {  // a MatchExpr is an "extended expression" and is only allowed in certain places

     public readonly Expression Source;

     public readonly List<MatchCaseExpr/*!*/>/*!*/ Cases;

+    public readonly List<DatatypeCtor/*!*/> MissingCases = new List<DatatypeCtor>();  // filled in during resolution

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Source != null);

       Contract.Invariant(cce.NonNullElements(Cases));

+      Contract.Invariant(cce.NonNullElements(MissingCases));

     }

 

     public MatchExpr(IToken tok, Expression source, [Captured] List<MatchCaseExpr/*!*/>/*!*/ cases)

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index d8ca3448..eb40ac82 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1473,7 +1473,16 @@ namespace Microsoft.Dafny {
           scope.PopMarker();

         }

         if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {

-          Error(stmt, "match expression does not cover all constructors");

+          // We could complain about the syntactic omission of constructors:

+          //   Error(stmt, "match statement does not cover all constructors");

+          // but instead we let the verifier do a semantic check.

+          // So, for now, record the missing constructors:

+          foreach (var ctr in dtd.Ctors) {

+            if (!memberNamesUsed.ContainsKey(ctr.Name)) {

+              s.MissingCases.Add(ctr);

+            }

+          }

+          Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);

         }

         

         

@@ -2390,7 +2399,16 @@ namespace Microsoft.Dafny {
           scope.PopMarker();

         }

         if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {

-          Error(expr, "match expression does not cover all constructors");

+          // We could complain about the syntactic omission of constructors:

+          //   Error(expr, "match expression does not cover all constructors");

+          // but instead we let the verifier do a semantic check.

+          // So, for now, record the missing constructors:

+          foreach (var ctr in dtd.Ctors) {

+            if (!memberNamesUsed.ContainsKey(ctr.Name)) {

+              me.MissingCases.Add(ctr);

+            }

+          }

+          Contract.Assert(memberNamesUsed.Count + me.MissingCases.Count == dtd.Ctors.Count);

         }

         

       } else {

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index bba7b734..b529b984 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -1371,8 +1371,26 @@ namespace Microsoft.Dafny {
       Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(mc.tok, mc.Ctor.FullName, predef.DatatypeType);

       return new Bpl.NAryExpr(mc.tok, new Bpl.FunctionCall(id), args);

     }

-    

-    Bpl.Expr IsTotal(Expression expr, ExpressionTranslator etran){

+

+    Bpl.Expr CtorInvocation(IToken tok, DatatypeCtor ctor, ExpressionTranslator etran, Bpl.VariableSeq locals, StmtListBuilder localTypeAssumptions) {

+      Contract.Requires(tok != null);

+      Contract.Requires(ctor != null);

+      Contract.Requires(etran != null);

+      Contract.Requires(locals != null);

+      Contract.Requires(localTypeAssumptions != null);

+      Contract.Requires(predef != null);

+      Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+

+      VariableSeq bvars;

+      List<Bpl.Expr> args;

+      CreateBoundVariables(ctor.Formals, out bvars, out args);

+      locals.AddRange(bvars);

+

+      Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(tok, ctor.FullName, predef.DatatypeType);

+      return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(id), new ExprSeq(args.ToArray()));

+    }

+

+    Bpl.Expr IsTotal(Expression expr, ExpressionTranslator etran) {

       Contract.Requires(expr != null);Contract.Requires(etran != null);

       Contract.Requires(predef != null);

       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

@@ -2030,20 +2048,40 @@ namespace Microsoft.Dafny {
         MatchExpr me = (MatchExpr)expr;

         CheckWellformed(me.Source, options, locals, builder, etran);

         Bpl.Expr src = etran.TrExpr(me.Source);

-        Bpl.IfCmd ifcmd = null;

+        Bpl.IfCmd ifCmd = null;

         StmtListBuilder elsBldr = new StmtListBuilder();

         elsBldr.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.False));

         StmtList els = elsBldr.Collect(expr.tok);

+        foreach (var missingCtor in me.MissingCases) {

+          // havoc all bound variables

+          var b = new Bpl.StmtListBuilder();

+          VariableSeq newLocals = new VariableSeq();

+          Bpl.Expr r = CtorInvocation(me.tok, missingCtor, etran, newLocals, b);

+          locals.AddRange(newLocals);

+

+          if (newLocals.Length != 0) {

+            Bpl.IdentifierExprSeq havocIds = new Bpl.IdentifierExprSeq();

+            foreach (Variable local in newLocals) {

+              havocIds.Add(new Bpl.IdentifierExpr(local.tok, local));

+            }

+            builder.Add(new Bpl.HavocCmd(me.tok, havocIds));

+          }

+          b.Add(Assert(me.tok, Bpl.Expr.False, "missing case in case statement: " + missingCtor.Name));

+

+          Bpl.Expr guard = Bpl.Expr.Eq(src, r);

+          ifCmd = new Bpl.IfCmd(me.tok, guard, b.Collect(me.tok), ifCmd, els);

+          els = null;

+        }

         for (int i = me.Cases.Count; 0 <= --i; ) {

           MatchCaseExpr mc = me.Cases[i];

           Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();

           Bpl.Expr ct = CtorInvocation(mc, etran, locals, b);

           // generate:  if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ...

           CheckWellformedWithResult(mc.Body, options, result, resultType, locals, b, etran);

-          ifcmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifcmd, els);

+          ifCmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifCmd, els);

           els = null;

         }

-        builder.Add(ifcmd);

+        builder.Add(ifCmd);

         result = null;

         

       } else {

@@ -3233,16 +3271,36 @@ namespace Microsoft.Dafny {
         builder.Add(CaptureState(stmt.Tok));

         

       } else if (stmt is MatchStmt) {

-        MatchStmt s = (MatchStmt)stmt;

+        var s = (MatchStmt)stmt;

         TrStmt_CheckWellformed(s.Source, builder, locals, etran, true);

         Bpl.Expr source = etran.TrExpr(s.Source);

         

-        Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();

+        var b = new Bpl.StmtListBuilder();

         b.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));

         Bpl.StmtList els = b.Collect(stmt.Tok);

         Bpl.IfCmd ifCmd = null;

+        foreach (var missingCtor in s.MissingCases) {

+          // havoc all bound variables

+          b = new Bpl.StmtListBuilder();

+          VariableSeq newLocals = new VariableSeq();

+          Bpl.Expr r = CtorInvocation(s.Tok, missingCtor, etran, newLocals, b);

+          locals.AddRange(newLocals);

+

+          if (newLocals.Length != 0) {

+            Bpl.IdentifierExprSeq havocIds = new Bpl.IdentifierExprSeq();

+            foreach (Variable local in newLocals) {

+              havocIds.Add(new Bpl.IdentifierExpr(local.tok, local));

+            }

+            builder.Add(new Bpl.HavocCmd(s.Tok, havocIds));

+          }

+          b.Add(Assert(s.Tok, Bpl.Expr.False, "missing case in case statement: " + missingCtor.Name));

+

+          Bpl.Expr guard = Bpl.Expr.Eq(source, r);

+          ifCmd = new Bpl.IfCmd(s.Tok, guard, b.Collect(s.Tok), ifCmd, els);

+          els = null;

+        }

         for (int i = s.Cases.Count; 0 <= --i; ) {

-          MatchCaseStmt mc = (MatchCaseStmt)s.Cases[i];

+          var mc = (MatchCaseStmt)s.Cases[i];

           // havoc all bound variables

           b = new Bpl.StmtListBuilder();

           VariableSeq newLocals = new VariableSeq();

@@ -3266,7 +3324,7 @@ namespace Microsoft.Dafny {
           ifCmd = new Bpl.IfCmd(mc.tok, guard, b.Collect(mc.tok), ifCmd, els);

           els = null;

         }

-        Contract.Assert(ifCmd != null);  // follows from the fact that s.Cases.Count != 0.

+        Contract.Assert(ifCmd != null);  // follows from the fact that s.Cases.Count + s.MissingCases.Count != 0.

         builder.Add(ifCmd);

 

       } else {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 34aea30b..28f438af 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -540,6 +540,42 @@ Execution trace:
 

 Dafny program verifier finished with 6 verified, 1 error

 

+-------------------- ControlStructures.dfy --------------------

+ControlStructures.dfy(5,3): Error: missing case in case statement: Blue

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon7_Else

+    (0,0): anon8_Else

+    (0,0): anon9_Then

+ControlStructures.dfy(5,3): Error: missing case in case statement: Purple

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+ControlStructures.dfy(14,3): Error: missing case in case statement: Purple

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+    (0,0): anon7_Else

+    (0,0): anon8_Then

+ControlStructures.dfy(43,5): Error: missing case in case statement: Red

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon9_Else

+    (0,0): anon10_Then

+ControlStructures.dfy(51,3): Error: missing case in case statement: Red

+Execution trace:

+    (0,0): anon8_Else

+    (0,0): anon9_Else

+    (0,0): anon10_Else

+    (0,0): anon11_Else

+    (0,0): anon12_Then

+

+Dafny program verifier finished with 8 verified, 5 errors

+

 -------------------- Termination.dfy --------------------

 Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy
new file mode 100644
index 00000000..eed74634
--- /dev/null
+++ b/Test/dafny0/ControlStructures.dfy
@@ -0,0 +1,65 @@
+datatype D = Green | Blue | Red | Purple;

+

+method M0(d: D)

+{

+  match (d) {  // error: two missing cases: Blue and Purple

+    case Green =>

+    case Red =>

+  }

+}

+

+method M1(d: D)

+  requires d != #D.Blue;

+{

+  match (d) {  // error: missing case: Purple

+    case Green =>

+    case Red =>

+  }

+}

+

+method M2(d: D)

+  requires d != #D.Blue && d != #D.Purple;

+{

+  match (d) {

+    case Green =>

+    case Red =>

+  }

+}

+

+method M3(d: D)

+  requires d == #D.Green;

+{

+  if (d != #D.Green) {

+    match (d) {

+      // nothing here

+    }

+  }

+}

+

+method M4(d: D)

+  requires d == #D.Green || d == #D.Red;

+{

+  if (d != #D.Green) {

+    match (d) {  // error: missing case Red

+      // nothing here

+    }

+  }

+}

+

+function F0(d: D): int

+{

+  match (d)  // error: missing cases Red

+  case Purple => 80

+  case Green => 0

+  case Blue => 2

+}

+

+function F1(d: D, x: int): int

+  requires x < 100;

+  requires d == #D.Red ==> x == 200;  // (an impossibility, given the first precondition, so d != Red)

+{

+  match (d)

+  case Purple => 80

+  case Green => 0

+  case Blue => 2

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index f67429d2..16bc0e2b 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -15,7 +15,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             FunctionSpecifications.dfy ResolutionErrors.dfy

             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

-            Comprehensions.dfy

+            Comprehensions.dfy ControlStructures.dfy

             Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy) do (