Improve computations, in particular compositionality. Isolated useless literals around if-then-else as a surprising source of practical hanging.

6 files changed, 86 insertions, 33 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 756e31fc..277f9d7d 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -8061,6 +8061,9 @@ namespace Microsoft.Dafny {
             result = ReadHeap(expr.tok, HeapExpr, obj, new Bpl.IdentifierExpr(expr.tok, translator.GetField(e.Field)));

           } else {

             result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(translator.GetReadonlyField(e.Field)), new List<Bpl.Expr> { obj });

+            if (translator.IsLit(obj)) {

+              result = translator.Lit(result, translator.TrType(expr.Type));

+            }

           }

           return translator.CondApplyUnbox(expr.tok, result, e.Field.Type, cce.NonNull(expr.Type));

 

@@ -8171,24 +8174,34 @@ namespace Microsoft.Dafny {
             layerArgument = null;

           }

 

-          var id = new Bpl.IdentifierExpr(e.tok, e.Function.FullSanitizedName, translator.TrType(e.Type));

-          var args = FunctionInvocationArguments(e, layerArgument);

-          var result = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args);

+          var ty = translator.TrType(e.Type);

+          var id = new Bpl.IdentifierExpr(e.tok, e.Function.FullSanitizedName, ty);

+          bool returnLit;

+          var args = FunctionInvocationArguments(e, layerArgument, out returnLit);

+          Expr result = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args);

+          if (returnLit && !translator.IsOpaqueFunction(e.Function)) {

+            result = translator.Lit(result, ty);

+          }

           return translator.CondApplyUnbox(e.tok, result, e.Function.ResultType, e.Type);

 

         } else if (expr is DatatypeValue) {

           DatatypeValue dtv = (DatatypeValue)expr;

           Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

           List<Bpl.Expr> args = new List<Bpl.Expr>();

+          bool isLit = true;

           for (int i = 0; i < dtv.Arguments.Count; i++) {

             Expression arg = dtv.Arguments[i];

             Type t = dtv.Ctor.Formals[i].Type;

             var bArg = TrExpr(arg);

+            isLit = isLit && translator.IsLit(bArg);

             args.Add(translator.CondApplyBox(expr.tok, bArg, cce.NonNull(arg.Type), t));

           }

           Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(dtv.tok, dtv.Ctor.FullName, predef.DatatypeType);

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

-

+          Expr ret = new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args);

+          if (isLit) {

+            ret = translator.Lit(ret, predef.DatatypeType);

+          }

+          return ret;

         } else if (expr is OldExpr) {

           OldExpr e = (OldExpr)expr;

           return Old.TrExpr(e.E);

@@ -8570,9 +8583,9 @@ namespace Microsoft.Dafny {
 

         } else if (expr is ITEExpr) {

           ITEExpr e = (ITEExpr)expr;

-          Bpl.Expr g = TrExpr(e.Test);

-          Bpl.Expr thn = TrExpr(e.Thn);

-          Bpl.Expr els = TrExpr(e.Els);

+          Bpl.Expr g = translator.RemoveLit(TrExpr(e.Test));

+          Bpl.Expr thn = translator.RemoveLit(TrExpr(e.Thn));

+          Bpl.Expr els = translator.RemoveLit(TrExpr(e.Els));

           return new NAryExpr(expr.tok, new IfThenElse(expr.tok), new List<Bpl.Expr> { g, thn, els });

 

         } else if (expr is MatchExpr) {

@@ -8694,6 +8707,11 @@ namespace Microsoft.Dafny {
       }

 

       public List<Expr> FunctionInvocationArguments(FunctionCallExpr e, Bpl.Expr layerArgument) {

+        bool returnLit;

+        return FunctionInvocationArguments(e, layerArgument, out returnLit);

+      }

+

+      public List<Expr> FunctionInvocationArguments(FunctionCallExpr e, Bpl.Expr layerArgument, out bool returnLit) {

         Contract.Requires(e != null);

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

 

@@ -8705,10 +8723,13 @@ namespace Microsoft.Dafny {
         if (!e.Function.IsStatic) {

           args.Add(TrExpr(e.Receiver));

         }

+        returnLit = true;

         for (int i = 0; i < e.Args.Count; i++) {

           Expression ee = e.Args[i];

           Type t = e.Function.Formals[i].Type;

-          args.Add(translator.CondApplyBox(e.tok, TrExpr(ee), cce.NonNull(ee.Type), t));

+          Expr tr_ee = TrExpr(ee);

+          returnLit = returnLit && translator.IsLit(tr_ee);

+          args.Add(translator.CondApplyBox(e.tok, tr_ee, cce.NonNull(ee.Type), t));

         }

         return args;

       }

@@ -9091,6 +9112,10 @@ namespace Microsoft.Dafny {
       return e;

     }

 

+    bool IsLit(Bpl.Expr expr) {

+      return GetLit(expr) != null;

+    }

+

     // The "typeInstantiation" argument is passed in to help construct the result type of the function.

     Bpl.NAryExpr FunctionCall(IToken tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[] args)

     {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3b0ca15b..248355cb 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2061,14 +2061,8 @@ Execution trace:
 Dafny program verifier finished with 1 verified, 4 errors

 

 -------------------- Computations.dfy --------------------

-Computations.dfy(163,13): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Computations.dfy(168,13): Error: assertion violation

-Execution trace:

-    (0,0): anon0

 

-Dafny program verifier finished with 49 verified, 2 errors

+Dafny program verifier finished with 49 verified, 0 errors

 

 -------------------- ComputationsNeg.dfy --------------------

 ComputationsNeg.dfy(4,3): Error: failure to decrease termination measure

@@ -2083,8 +2077,14 @@ ComputationsNeg.dfy(20,1): Error BP5003: A postcondition might not hold on this
 ComputationsNeg.dfy(19,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

+ComputationsNeg.dfy(33,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+ComputationsNeg.dfy(42,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 3 verified, 3 errors

+Dafny program verifier finished with 7 verified, 5 errors

 

 -------------------- Include.dfy --------------------

 

diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy
index 4b975559..d3c42af5 100644
--- a/Test/dafny0/Computations.dfy
+++ b/Test/dafny0/Computations.dfy
@@ -151,19 +151,12 @@ ghost method copt_test()
 {

 }

 

-// The following is a test that well-typedness antecednets are included in the literal axioms

-static function StaticFact(n: nat): nat

-  ensures 0 < StaticFact(n);

+function power(b: int, n: nat): int

 {

-  if n == 0 then 1 else n * StaticFact(n - 1)

+  if (n==0) then 1 else b*power(b, n-1)

 }

-static method test_StaticFact()

-{

-  assert StaticFact(0) == 1;

-  assert 42 != 42;  // error:  this should fail

-} 

-method test_fact()

+

+ghost method test_power()

+  ensures power(power(2, 3), 1+power(2, 2))==32768;

 {

-  assert fact(0) == 1;

-  assert 42 != 42;  // error:  this should fail

-} 

+}
\ No newline at end of file
diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy
index 72e249d8..b225a210 100644
--- a/Test/dafny0/ComputationsNeg.dfy
+++ b/Test/dafny0/ComputationsNeg.dfy
@@ -19,4 +19,25 @@ ghost method test_ThProperty()
   ensures ThProperty(10, Succ(Zero), 0);

 {

 //  assert ThProperty(9, Zero, 0);

-}
\ No newline at end of file
+}

+

+// The following is a test that well-typedness antecednets are included in the literal axioms

+static function StaticFact(n: nat): nat

+  ensures 0 < StaticFact(n);

+{

+  if n == 0 then 1 else n * StaticFact(n - 1)

+}

+static method test_StaticFact()

+{

+  assert StaticFact(0) == 1;

+  assert 42 != 42;  // error:  this should fail

+} 

+function fact(n: nat): nat

+{

+  if (n==0) then 1 else n*fact(n-1)

+}

+method test_fact()

+{

+  assert fact(0) == 1;

+  assert 42 != 42;  // error:  this should fail

+} 

diff --git a/Test/dafny4/Answer b/Test/dafny4/Answer
index 61eedf16..4dd73008 100644
--- a/Test/dafny4/Answer
+++ b/Test/dafny4/Answer
@@ -24,7 +24,7 @@ SoftwareFoundations-Basics.dfy(38,12): Error: assertion violation
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 80 verified, 1 error

+Dafny program verifier finished with 82 verified, 1 error

 

 -------------------- NumberRepresentations.dfy --------------------

 

diff --git a/Test/dafny4/SoftwareFoundations-Basics.dfy b/Test/dafny4/SoftwareFoundations-Basics.dfy
index 0b695aef..9f239612 100644
--- a/Test/dafny4/SoftwareFoundations-Basics.dfy
+++ b/Test/dafny4/SoftwareFoundations-Basics.dfy
@@ -237,7 +237,21 @@ method test_factorial1()
   var n10 := S(S(S(S(n6))));

   var n12 := S(S(n10));

 

-  // proving that 5! == 10*12 takes some effort, because the computation fuel runs out

+  assert factorial(n5)==mult(n10, n12);

+}

+

+method test_factorial1_old()

+{

+  var n2 := S(S(O));

+  var n3 := S(n2);

+  var n5 := S(S(n3));

+  var n6 := S(n5);

+  assert factorial(n3) == n6;

+

+  var n10 := S(S(S(S(n6))));

+  var n12 := S(S(n10));

+

+  // proving that 5! == 10*12 _used to_ take some effort...

   calc {

     factorial(n5);

     { mult_lemma(n2, n6); }