From 4f0b823bdc1be13c2589cc46f650ab57d29e7117 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Thu, 4 Feb 2016 12:35:46 -0800 Subject: Fix issue 128. Change the translation of CanCallAssumption for let-such-that expression from // CanCall[[ var b :| RHS(b,g); Body(b,g,h) ]] = // (forall b0,b1 :: typeAntecedent ==> // CanCall[[ RHS(b,g) ]] && // (RHS(b,g) ==> CanCall[[ Body(b,g,h) ]]) && // $let$canCall(b,g)) to // CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] = // $let$canCall(g) && // CanCall[[ Body($let$b0(g), $let$b1(g), h) ]] --- Source/Dafny/Printer.cs | 8 +++++--- Source/Dafny/Translator.cs | 34 ++++++++++++++++++---------------- Test/dafny4/Bug128.dfy | 13 +++++++++++++ Test/dafny4/Bug128.dfy.expect | 4 ++++ 4 files changed, 40 insertions(+), 19 deletions(-) create mode 100644 Test/dafny4/Bug128.dfy create mode 100644 Test/dafny4/Bug128.dfy.expect diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index accdb9d3..86c493f1 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1955,9 +1955,11 @@ namespace Microsoft.Dafny { var e = (BoxingCastExpr)expr; PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, keyword); } else if (expr is Translator.BoogieWrapper) { - wr.Write("[BoogieWrapper]"); // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here - } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + wr.Write("[BoogieWrapper]"); // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here + } else if (expr is Translator.BoogieFunctionCall) { + wr.Write("[BoogieFunctionCall]"); // this prevents debugger watch window crash + } else { + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression } } diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index a1fbe646..1208a83a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4413,23 +4413,25 @@ namespace Microsoft.Dafny { var canCallBody = CanCallAssumption(Substitute(e.Body, null, substMap), etran); return BplAnd(canCallRHS, canCallBody); } else { - // CanCall[[ var b :| RHS(b,g); Body(b,g,h) ]] = - // (forall b :: typeAntecedent ==> - // CanCall[[ RHS(b,g) ]] && - // (RHS(b,g) ==> CanCall[[ Body(b,g,h) ]]) && - // $let$canCall(b,g)) - var bvars = new List(); - Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars.ToList(), bvars); - Contract.Assert(e.RHSs.Count == 1); // this is true of all successfully resolved let-such-that expressions - var canCallRHS = CanCallAssumption(e.RHSs[0], etran); - var canCallBody = Bpl.Expr.Imp(etran.TrExpr(e.RHSs[0]), CanCallAssumption(e.Body, etran)); - var d = LetDesugaring(e); // call LetDesugaring to prepare the desugaring and populate letSuchThatExprInfo with something for e + // CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] = + // $let$canCall(g) && + // CanCall[[ Body($let$b0(g), $let$b1(g), h) ]] + LetDesugaring(e); // call LetDesugaring to prepare the desugaring and populate letSuchThatExprInfo with something for e var info = letSuchThatExprInfo[e]; - var canCallFunction = info.CanCallFunctionCall(this, etran); - //TRIG (forall d#0: int :: true ==> _module.__default.DividesBoth#canCall($Heap, d#0, a#0, b#0) && (_module.__default.DividesBoth($Heap, d#0, a#0, b#0) ==> (forall m#1: int :: true ==> _module.__default.DividesBoth#canCall($Heap, m#1, a#0, b#0) && (_module.__default.DividesBoth($Heap, m#1, a#0, b#0) ==> true))) && (_module.__default.DividesBoth($Heap, d#0, a#0, b#0) && (forall m#1: int :: true ==> _module.__default.DividesBoth($Heap, m#1, a#0, b#0) ==> m#1 <= d#0) ==> true) && $let#0$canCall($Heap, a#0, b#0)) - //TRIG (forall g#0: int :: true ==> (x#0 == g#0 ==> true) && $let#0$canCall($Heap, x#0)) - //TRIGGERS: Not clear what would be good here - var cc = new Bpl.ForallExpr(e.tok, bvars, Bpl.Expr.Imp(typeAntecedent, BplAnd(BplAnd(canCallRHS, canCallBody), canCallFunction))); // LL_TRIGGER + // $let$canCall(g) + //var canCall = FunctionCall(e.tok, info.CanCallFunctionName(), Bpl.Type.Bool, gExprs); + var canCall = info.CanCallFunctionCall(this, etran); + Dictionary substMap = new Dictionary(); + foreach (var bv in e.BoundVars) { + // create a call to $let$x(g) + //var call = FunctionCall(e.tok, info.SkolemFunctionName(bv), TrType(bv.Type), gExprs); + var args = info.SkolemFunctionArgs(bv, this, etran); + var call = new BoogieFunctionCall(bv.tok, info.SkolemFunctionName(bv), info.UsesHeap, info.UsesOldHeap, args.Item1, args.Item2); + call.Type = bv.Type; + substMap.Add(bv, call); + } + var p = Substitute(e.Body, null, substMap); + var cc = BplAnd(canCall, CanCallAssumption(p, etran)); return cc; } diff --git a/Test/dafny4/Bug128.dfy b/Test/dafny4/Bug128.dfy new file mode 100644 index 00000000..b7220335 --- /dev/null +++ b/Test/dafny4/Bug128.dfy @@ -0,0 +1,13 @@ +// RUN: %dafny /noNLarith /z3opt:pi.warnings=true /proverWarnings:1 /compile:0 /autoTriggers:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function GetIndexInSequence(s:seq, x:T) : int + requires x in s; + ensures 0 <= GetIndexInSequence(s, x) < |s|; + ensures s[GetIndexInSequence(s, x)] == x; { + var i :| 0 <= i < |s| && s[i] == x; + i + } + + + diff --git a/Test/dafny4/Bug128.dfy.expect b/Test/dafny4/Bug128.dfy.expect new file mode 100644 index 00000000..700ad964 --- /dev/null +++ b/Test/dafny4/Bug128.dfy.expect @@ -0,0 +1,4 @@ +Prover warning: pattern does not contain all quantified variables. +Prover warning: pattern does not contain all quantified variables. + +Dafny program verifier finished with 1 verified, 0 errors -- cgit v1.2.3