Fixed bugs in encoding of preconditions of function values, Issue #84.

6 files changed, 109 insertions, 44 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 4324b2b8..c98bd203 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2176,13 +2176,6 @@ namespace Microsoft.Dafny {
       foreach (Expression req in f.Req) {

         pre = BplAnd(pre, etran.TrExpr(Substitute(req, null, substMap)));

       }

-      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)

-      ModuleDefinition mod = f.EnclosingClass.Module;

-      Bpl.Expr useViaContext = visibility == FunctionAxiomVisibility.ForeignModuleOnly ? (Bpl.Expr)Bpl.Expr.True :

-        Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight());

-

-      // ante := (useViaContext && typeAnte && pre)

-      ante = BplAnd(useViaContext, BplAnd(ante, pre));

 

       // Add the precondition function and its axiom (which is equivalent to the ante)

       if (body == null || (visibility == FunctionAxiomVisibility.IntraModuleOnly && lits == null)) {

@@ -2195,14 +2188,21 @@ namespace Microsoft.Dafny {
         }

         var appl = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool,

           formals.ConvertAll(x => (Bpl.Expr)(new Bpl.IdentifierExpr(f.tok, x))));

-        sink.AddTopLevelDeclaration(new Axiom(f.tok, BplForall(formals, BplTrigger(appl), Bpl.Expr.Eq(appl, ante))));

-        // you could use it to check that it always works, but it makes VSI-Benchmarks/b3.dfy time out:

-        // ante = appl;

+        // axiom (forall params :: { f#requires(params) }  ante ==> f#requires(params) == pre);

+        sink.AddTopLevelDeclaration(new Axiom(f.tok, BplForall(formals, BplTrigger(appl),

+          BplImp(ante, Bpl.Expr.Eq(appl, pre)))));

         if (body == null) {

           return null;

         }

       }

 

+      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)

+      ModuleDefinition mod = f.EnclosingClass.Module;

+      Bpl.Expr useViaContext = visibility == FunctionAxiomVisibility.ForeignModuleOnly ? (Bpl.Expr)Bpl.Expr.True :

+        Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight());

+      // ante := (useViaContext && typeAnte && pre)

+      ante = BplAnd(useViaContext, BplAnd(ante, pre));

+

       // useViaCanCall: f#canCall(args)

       Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool);

       Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs,args));

@@ -5632,7 +5632,6 @@ namespace Microsoft.Dafny {
         {

           // Requires(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN)

           //   = F#Requires(Ty1, .., TyN, Layer, Heap, self, [Unbox] arg1, .., [Unbox] argN)

-          //   || Scramble(...)

 

           var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(args));

           var lhs = FunctionCall(f.tok, Requires(arity), Bpl.Type.Bool, Concat(tyargs, Cons(fhandle, Cons(h, lhs_args))));

@@ -5641,9 +5640,7 @@ namespace Microsoft.Dafny {
             // In case this is the /requires/ or /reads/ function, then there is no precondition

             rhs = Bpl.Expr.True;

           } else {

-            rhs = BplOr(

-              FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool, Concat(SnocSelf(Snoc(args, h)), rhs_args)),

-              MakeScrambler(f.tok, f.FullSanitizedName + "#lessReq", Concat(vars, bvars)));

+            rhs = FunctionCall(f.tok, RequiresName(f), Bpl.Type.Bool, Concat(SnocSelf(Snoc(args, h)), rhs_args));

           }

 

           sink.AddTopLevelDeclaration(new Axiom(f.tok,

@@ -5671,15 +5668,6 @@ namespace Microsoft.Dafny {
       return name;

     }

 

-    public Bpl.Expr MakeScrambler(IToken tk, string name, List<Variable> bvars) {

-      var f = new Bpl.Function(tk, name,

-        bvars.ConvertAll(bv => (Bpl.Variable)BplFormalVar(null, bv.TypedIdent.Type, true)),

-        BplFormalVar(null, Bpl.Type.Bool, false));

-

-      sink.AddTopLevelDeclaration(f);

-      return FunctionCall(tk, name, Bpl.Type.Bool, bvars.ConvertAll(bv => (Bpl.Expr)new Bpl.IdentifierExpr(tk, bv)));

-    }

-

     private void AddArrowTypeAxioms(ArrowTypeDecl ad) {

       Contract.Requires(ad != null);

       var arity = ad.Arity;

@@ -11476,11 +11464,8 @@ namespace Microsoft.Dafny {
         var rdvars = new List<Bpl.Variable>();

         var o = translator.UnboxIfBoxed(BplBoundVar(varNameGen.FreshId("#o#"), predef.BoxType, rdvars), new ObjectType());

 

-        Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), et.IsAlloced(e.tok, o));

-        Bpl.Expr consequent = translator.InRWClause(e.tok, o, null, e.Reads.ConvertAll(su.SubstFrameExpr), et, null, null);

-        Bpl.Expr rdbody =

-          new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), rdvars, null,

-            BplImp(ante, consequent));

+        Bpl.Expr rdbody = new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), rdvars, null,

+          translator.InRWClause(e.tok, o, null, e.Reads.ConvertAll(su.SubstFrameExpr), et, null, null));

 

         return translator.Lit(

           translator.FunctionCall(e.tok, BuiltinFunction.AtLayer, predef.HandleType,

@@ -14267,7 +14252,7 @@ namespace Microsoft.Dafny {
 

     /// Makes a simple trigger

     static Bpl.Trigger BplTrigger(Bpl.Expr e) {

-      return new Trigger(e.tok, true, new List<Bpl.Expr> { e });

+      return new Bpl.Trigger(e.tok, true, new List<Bpl.Expr> { e });

     }

 

     static Bpl.Axiom BplAxiom(Bpl.Expr e) {

diff --git a/Test/hofs/Naked.dfy b/Test/hofs/Naked.dfy
index fa99377f..d23eb507 100644
--- a/Test/hofs/Naked.dfy
+++ b/Test/hofs/Naked.dfy
@@ -19,17 +19,17 @@ module Functions {
 
 module Requires {
   function t(x: nat): nat
-  requires !t.requires(x);
+  requires !t.requires(x);  // error: use of naked function in its own SCC
   { x }
 
   function g(x: nat): nat
-  requires !(g).requires(x);
+  requires !(g).requires(x);  // error: use of naked function in its own SCC
   { x }
 
-  function g2(x: int): int { h(x) }
-
+  function D(x: int): int  // used so termination errors don't mask other errors
+  function g2(x: int): int decreases D(x) { h(x) }  // error: precondition violation
   function h(x: int): int
-    requires !g2.requires(x);
+    requires !g2.requires(x);  // error: use of naked function in its own SCC
   { x }
 }
 
diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect
index b4dfc561..514952a1 100644
--- a/Test/hofs/Naked.dfy.expect
+++ b/Test/hofs/Naked.dfy.expect
@@ -21,11 +21,7 @@ Execution trace:
 Naked.dfy(26,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.

 Execution trace:

     (0,0): anon0

-Naked.dfy(29,30): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Else

-Naked.dfy(29,30): Error: possible violation of function precondition

+Naked.dfy(30,45): Error: possible violation of function precondition

 Naked.dfy(32,14): Related location

 Execution trace:

     (0,0): anon0

@@ -47,4 +43,4 @@ Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possibl
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 1 verified, 12 errors

+Dafny program verifier finished with 2 verified, 11 errors

diff --git a/Test/hofs/Requires.dfy b/Test/hofs/Requires.dfy
new file mode 100644
index 00000000..68677b3e
--- /dev/null
+++ b/Test/hofs/Requires.dfy
@@ -0,0 +1,82 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+method Main()

+{

+  test0(10);

+	test5(11);

+	test6(12);

+	test1();

+	test2();

+}

+

+predicate valid(x:int) 

+{

+  x > 0

+}

+

+function ref1(y:int) : int

+  requires valid(y);

+{

+  y - 1

+}

+

+lemma assumption1()

+  ensures forall a, b :: valid(a) && valid(b) && ref1(a) == ref1(b) ==> a == b;

+{

+} 

+

+method test0(a: int)

+{

+  if ref1.requires(a) {

+    // the precondition should suffice to let us call the method

+    ghost var b := ref1(a);

+  }

+}

+method test5(a: int)

+{

+  if valid(a) {

+    // valid(a) is the precondition of ref1

+    assert ref1.requires(a);

+  }  

+} 

+method test6(a: int)

+{

+  if ref1.requires(a) {

+    // the precondition of ref1 is valid(a)

+    assert valid(a);

+  }  

+}

+

+method test1()

+{

+  if * {

+    assert forall a, b :: valid(a) && valid(b) && ref1(a) == ref1(b) ==> a == b;

+  } else {

+    assert forall a, b :: ref1.requires(a) && ref1.requires(b) && ref1(a) == ref1(b) 

+                          ==> a == b;

+  }

+}

+

+function {:opaque} ref2(y:int) : int        // Now with an opaque attribute

+  requires valid(y);

+{

+  y - 1

+}

+

+lemma assumption2()

+  ensures forall a, b :: valid(a) && valid(b) && ref2(a) == ref2(b) ==> a == b;

+{

+  reveal_ref2();

+}

+

+method test2()

+{

+  assumption2();

+  if * {

+    assert forall a, b :: valid(a) && valid(b) && ref2(a) == ref2(b) ==> a == b;

+  } else {

+    assert forall a, b :: ref2.requires(a) && ref2.requires(b) && ref2(a) == ref2(b) 

+                          ==> a == b;

+  }

+}

diff --git a/Test/hofs/Requires.dfy.expect b/Test/hofs/Requires.dfy.expect
new file mode 100644
index 00000000..b9a40d66
--- /dev/null
+++ b/Test/hofs/Requires.dfy.expect
@@ -0,0 +1,5 @@
+

+Dafny program verifier finished with 20 verified, 0 errors

+Program compiled successfully

+Running...

+

diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect
index 1a1027ae..e2f16ef3 100644
--- a/Test/hofs/Simple.dfy.expect
+++ b/Test/hofs/Simple.dfy.expect
@@ -20,13 +20,10 @@ Execution trace:
 Simple.dfy(61,10): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-Simple.dfy(61,18): Error: assertion violation

-Execution trace:

-    (0,0): anon0

 Simple.dfy(73,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

     Simple.dfy(72,38): anon5_Else

     Simple.dfy(73,38): anon6_Else

 

-Dafny program verifier finished with 14 verified, 7 errors

+Dafny program verifier finished with 14 verified, 6 errors