summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Translator.cs43
-rw-r--r--Test/hofs/Naked.dfy10
-rw-r--r--Test/hofs/Naked.dfy.expect8
-rw-r--r--Test/hofs/Requires.dfy82
-rw-r--r--Test/hofs/Requires.dfy.expect5
-rw-r--r--Test/hofs/Simple.dfy.expect5
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 17:38:43 +0000