summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Compiler.cs40
-rw-r--r--Source/Dafny/DafnyAst.cs13
-rw-r--r--Source/Dafny/Resolver.cs49
-rw-r--r--Source/Dafny/Translator.cs139
4 files changed, 198 insertions, 43 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 13381cc7..aa4ca3ec 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1455,10 +1455,17 @@ namespace Microsoft.Dafny {
}
} else {
Indent(indent); wr.Write("if (");
- TrExpr(s.Guard);
+ TrExpr(s.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)s.Guard, "eg_d", new Translator(null)) : s.Guard);
wr.WriteLine(")");
- TrStmt(s.Thn, indent);
+ // We'd like to do "TrStmt(s.Thn, indent)", except we want the scope of any existential variables to come inside the block
+ Indent(indent); wr.WriteLine("{");
+ if (s.IsExistentialGuard) {
+ IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)s.Guard);
+ }
+ TrStmtList(s.Thn.Body, indent);
+ Indent(indent); wr.WriteLine("}");
+
if (s.Els != null) {
Indent(indent); wr.WriteLine("else");
TrStmt(s.Els, indent);
@@ -1467,13 +1474,14 @@ namespace Microsoft.Dafny {
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
- foreach (var alternative in s.Alternatives) {
- }
Indent(indent);
foreach (var alternative in s.Alternatives) {
wr.Write("if (");
- TrExpr(alternative.Guard);
+ TrExpr(alternative.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)alternative.Guard, "eg_d", new Translator(null)) : alternative.Guard);
wr.WriteLine(") {");
+ if (alternative.IsExistentialGuard) {
+ IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)alternative.Guard);
+ }
TrStmtList(alternative.Body, indent);
Indent(indent);
wr.Write("} else ");
@@ -1766,6 +1774,18 @@ namespace Microsoft.Dafny {
}
}
+ private void IntroduceAndAssignBoundVars(int indent, ExistsExpr exists) {
+ Contract.Requires(0 <= indent);
+ Contract.Requires(exists != null);
+ Contract.Assume(exists.Bounds != null); // follows from successful resolution
+ Contract.Assert(exists.Range == null); // follows from invariant of class IfStmt
+ foreach (var bv in exists.BoundVars) {
+ TrLocalVar(bv, false, indent);
+ }
+ var ivars = exists.BoundVars.ConvertAll(bv => (IVariable)bv);
+ TrAssignSuchThat(indent, ivars, exists.Term, exists.Bounds, exists.tok.line);
+ }
+
private void TrAssignSuchThat(int indent, List<IVariable> lhss, Expression constraint, List<ComprehensionExpr.BoundedPool> bounds, int debuginfoLine) {
Contract.Requires(0 <= indent);
Contract.Requires(lhss != null);
@@ -2155,18 +2175,18 @@ namespace Microsoft.Dafny {
}
}
- void TrLocalVar(LocalVariable s, bool alwaysInitialize, int indent) {
- Contract.Requires(s != null);
- if (s.IsGhost) {
+ void TrLocalVar(IVariable v, bool alwaysInitialize, int indent) {
+ Contract.Requires(v != null);
+ if (v.IsGhost) {
// only emit non-ghosts (we get here only for local variables introduced implicitly by call statements)
return;
}
Indent(indent);
- wr.Write("{0} @{1}", TypeName(s.Type), s.CompileName);
+ wr.Write("{0} @{1}", TypeName(v.Type), v.CompileName);
if (alwaysInitialize) {
// produce a default value
- wr.WriteLine(" = {0};", DefaultValue(s.Type));
+ wr.WriteLine(" = {0};", DefaultValue(v.Type));
} else {
wr.WriteLine(";");
}
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 64af1425..667f8407 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3903,7 +3903,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(Expr != null);
}
- public ExprRhs(Expression expr, Attributes attrs = null)
+ public ExprRhs(Expression expr, Attributes attrs = null) // TODO: these 'attrs' apparently aren't handled correctly in the Cloner, and perhaps not in various visitors either (for example, CheckIsCompilable should not go into attributes)
: base(expr.tok, attrs)
{
Contract.Requires(expr != null);
@@ -7175,9 +7175,16 @@ namespace Microsoft.Dafny {
public override IEnumerable<Expression> SubExpressions {
get {
if (SplitQuantifier == null) {
- return base.SubExpressions;
+ foreach (var e in base.SubExpressions) {
+ yield return e;
+ }
} else {
- return SplitQuantifier;
+ foreach (var e in Attributes.SubExpressions(Attributes)) {
+ yield return e;
+ }
+ foreach (var e in SplitQuantifier) {
+ yield return e;
+ }
}
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index bc94e491..1798243c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2264,12 +2264,14 @@ namespace Microsoft.Dafny
what = "quantifier";
whereToLookForBounds = ((QuantifierExpr)e).LogicalBody();
polarity = e is ExistsExpr;
- } else if (e is SetComprehension && ((SetComprehension)e).Finite) {
+ } else if (e is SetComprehension) {
what = "set comprehension";
whereToLookForBounds = e.Range;
- } else if (e is MapComprehension && ((MapComprehension)e).Finite) {
+ } else if (e is MapComprehension) {
what = "map comprehension";
whereToLookForBounds = e.Range;
+ } else {
+ Contract.Assume(e is LambdaExpr); // otherwise, unexpected ComprehensionExpr
}
if (whereToLookForBounds != null) {
List<BoundVar> missingBounds;
@@ -2278,9 +2280,9 @@ namespace Microsoft.Dafny
e.MissingBounds = missingBounds;
if ((e is SetComprehension && !((SetComprehension)e).Finite) || (e is MapComprehension && !((MapComprehension)e).Finite)) {
- // a possibly infinite set/map has no restrictions on its range
+ // a possibly infinite set/map has no restrictions on its range (unless it's used in a compilable context, which is checked later)
} else if (e is QuantifierExpr) {
- // don't report any errors at this time (instead, wait to see if the quantifier is used in a non-ghost context)
+ // a quantifier has no restrictions on its range (unless it's used in a compilable context, which is checked later)
} else if (e is SetComprehension && e.Type.HasFinitePossibleValues) {
// This means the set is finite, regardless of if the Range is bounded. So, we don't give any error here.
// However, if this expression is used in a non-ghost context (which is not yet known at this stage of
@@ -2341,7 +2343,6 @@ namespace Microsoft.Dafny
var bin = expr as BinaryExpr;
if (bin != null) {
bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type);
-
}
}
}
@@ -5647,7 +5648,17 @@ namespace Microsoft.Dafny
Contract.Assert(s.Guard.Type != null); // follows from postcondition of ResolveExpression
ConstrainTypes(s.Guard.Type, Type.Bool, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
}
- ResolveStatement(s.Thn, codeContext);
+
+ scope.PushMarker();
+ if (s.IsExistentialGuard) {
+ var exists = (ExistsExpr)s.Guard;
+ foreach (var v in exists.BoundVars) {
+ ScopePushAndReport(scope, v, "bound-variable");
+ }
+ }
+ ResolveBlockStatement(s.Thn, codeContext);
+ scope.PopMarker();
+
if (s.Els != null) {
ResolveStatement(s.Els, codeContext);
}
@@ -6525,7 +6536,7 @@ namespace Microsoft.Dafny
Contract.Requires(alternatives != null);
Contract.Requires(codeContext != null);
- // first, resolve the guards, which tells us whether or not the entire statement is a ghost statement
+ // first, resolve the guards
foreach (var alternative in alternatives) {
int prevErrorCount = reporter.Count(ErrorLevel.Error);
ResolveExpression(alternative.Guard, new ResolveOpts(codeContext, true));
@@ -6539,6 +6550,12 @@ namespace Microsoft.Dafny
}
foreach (var alternative in alternatives) {
scope.PushMarker();
+ if (alternative.IsExistentialGuard) {
+ var exists = (ExistsExpr)alternative.Guard;
+ foreach (var v in exists.BoundVars) {
+ ScopePushAndReport(scope, v, "bound-variable");
+ }
+ }
foreach (Statement ss in alternative.Body) {
ResolveStatement(ss, codeContext);
}
@@ -9508,9 +9525,9 @@ namespace Microsoft.Dafny
if (uncompilableBoundVars.Count != 0) {
string what;
if (e is SetComprehension) {
- what = "set comprehensions";
+ what = ((SetComprehension)e).Finite ? "set comprehensions" : "iset comprehensions";
} else if (e is MapComprehension) {
- what = "map comprehensions";
+ what = ((MapComprehension)e).Finite ? "map comprehensions" : "imap comprehensions";
} else {
Contract.Assume(e is QuantifierExpr); // otherwise, unexpected ComprehensionExpr (since LambdaExpr is handled separately above)
Contract.Assert(((QuantifierExpr)e).SplitQuantifier == null); // No split quantifiers during resolution
@@ -9521,15 +9538,11 @@ namespace Microsoft.Dafny
}
return;
}
+ // don't recurse down any attributes
+ if (e.Range != null) { CheckIsCompilable(e.Range); }
+ CheckIsCompilable(e.Term);
+ return;
- } else if (expr is MapComprehension) {
- var e = (MapComprehension)expr;
- if (e.MissingBounds != null && !e.Finite) {
- foreach (var bv in e.MissingBounds) {
- reporter.Error(MessageSource.Resolver, expr, "imaps in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
- }
- return;
- }
} else if (expr is NamedExpr) {
if (!moduleInfo.IsAbstract)
CheckIsCompilable(((NamedExpr)expr).Body);
@@ -10436,7 +10449,7 @@ namespace Microsoft.Dafny
} else if (expr is QuantifierExpr) {
var e = (QuantifierExpr)expr;
Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution
- return e.UncompilableBoundVars().Count != 0;
+ return e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.LogicalBody());
} else if (expr is SetComprehension) {
var e = (SetComprehension)expr;
return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index c84f0cec..18b50686 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4740,7 +4740,7 @@ namespace Microsoft.Dafny {
var typeMap = Util.Dict(e.TypeArgs, Map(typeArgumentCopies, tp => (Type)new UserDefinedType(tp)));
var newLocals = Map(typeArgumentCopies, tp => new Bpl.LocalVariable(tp.tok, new TypedIdent(tp.tok, nameTypeParam(tp), predef.Ty)));
locals.AddRange(newLocals);
- // Create local variables corresponding to the in-parameters:
+ // Create local variables corresponding to the bound variables:
var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran, typeMap);
// Get the body of the quantifier and suitably substitute for the type variables and bound variables
var body = Substitute(e.LogicalBody(true), null, substMap, typeMap);
@@ -7244,24 +7244,30 @@ namespace Microsoft.Dafny {
} else if (stmt is IfStmt) {
AddComment(builder, stmt, "if statement");
IfStmt s = (IfStmt)stmt;
- Bpl.Expr guard;
+ Expression guard;
if (s.Guard == null) {
guard = null;
} else {
- TrStmt_CheckWellformed(s.Guard, builder, locals, etran, true);
- guard = etran.TrExpr(s.Guard);
+ guard = s.IsExistentialGuard ? AlphaRename((ExistsExpr)s.Guard, "eg$", this) : s.Guard;
+ TrStmt_CheckWellformed(guard, builder, locals, etran, true);
}
Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
CurrentIdGenerator.Push();
+ if (s.IsExistentialGuard) {
+ var exists = (ExistsExpr)s.Guard; // the original (that is, not alpha-renamed) guard
+ IntroduceAndAssignExistentialVars(exists, b, builder, locals, etran);
+ }
Bpl.StmtList thn = TrStmt2StmtList(b, s.Thn, locals, etran);
CurrentIdGenerator.Pop();
Bpl.StmtList els;
Bpl.IfCmd elsIf = null;
+ b = new Bpl.StmtListBuilder();
+ if (s.IsExistentialGuard) {
+ b.Add(new Bpl.AssumeCmd(guard.tok, Bpl.Expr.Not(etran.TrExpr(guard))));
+ }
if (s.Els == null) {
- b = new Bpl.StmtListBuilder();
els = b.Collect(s.Tok);
} else {
- b = new Bpl.StmtListBuilder();
els = TrStmt2StmtList(b, s.Els, locals, etran);
if (els.BigBlocks.Count == 1) {
Bpl.BigBlock bb = els.BigBlocks[0];
@@ -7271,7 +7277,7 @@ namespace Microsoft.Dafny {
}
}
}
- builder.Add(new Bpl.IfCmd(stmt.Tok, guard, thn, elsIf, els));
+ builder.Add(new Bpl.IfCmd(stmt.Tok, guard == null || s.IsExistentialGuard ? null : etran.TrExpr(guard), thn, elsIf, els));
} else if (stmt is AlternativeStmt) {
AddComment(builder, stmt, "alternative statement");
@@ -7551,6 +7557,26 @@ namespace Microsoft.Dafny {
}
}
+ private void IntroduceAndAssignExistentialVars(ExistsExpr exists, Bpl.StmtListBuilder builder, Bpl.StmtListBuilder builderOutsideIfConstruct, List<Variable> locals, ExpressionTranslator etran) {
+ Contract.Requires(exists != null);
+ Contract.Requires(exists.Range == null);
+ Contract.Requires(builder != null);
+ Contract.Requires(builderOutsideIfConstruct != null);
+ Contract.Requires(locals != null);
+ Contract.Requires(etran != null);
+ // declare and havoc the bound variables of 'exists' as local variables
+ var iesForHavoc = new List<Bpl.IdentifierExpr>();
+ foreach (var bv in exists.BoundVars) {
+ Bpl.Type varType = TrType(bv.Type);
+ Bpl.Expr wh = GetWhereClause(bv.Tok, new Bpl.IdentifierExpr(bv.Tok, bv.AssignUniqueName(currentDeclaration.IdGenerator), varType), bv.Type, etran);
+ Bpl.Variable local = new Bpl.LocalVariable(bv.Tok, new Bpl.TypedIdent(bv.Tok, bv.AssignUniqueName(currentDeclaration.IdGenerator), varType, wh));
+ locals.Add(local);
+ iesForHavoc.Add(new Bpl.IdentifierExpr(local.tok, local));
+ }
+ builderOutsideIfConstruct.Add(new Bpl.HavocCmd(exists.tok, iesForHavoc));
+ builder.Add(new Bpl.AssumeCmd(exists.tok, etran.TrExpr(exists.Term)));
+ }
+
void TrStmtList(List<Statement> stmts, Bpl.StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
Contract.Requires(stmts != null);
Contract.Requires(builder != null);
@@ -7565,6 +7591,46 @@ namespace Microsoft.Dafny {
}
/// <summary>
+ /// Returns an expression like 'exists' but where the bound variables have been renamed to have
+ /// 'prefix' as a prefix to their previous names.
+ /// Assumes the expression has been resolved.
+ /// </summary>
+ public static Expression AlphaRename(ExistsExpr exists, string prefix, Translator translator) {
+ Contract.Requires(exists != null);
+ Contract.Requires(prefix != null);
+ Contract.Requires(translator != null);
+
+ if (exists.SplitQuantifier != null) {
+ // TODO: what to do? Substitute(exists.SplitQuantifierExpression);
+ }
+
+ var substMap = new Dictionary<IVariable, Expression>();
+ var var4var = new Dictionary<BoundVar, BoundVar>();
+ var bvars = new List<BoundVar>();
+ foreach (var bv in exists.BoundVars) {
+ var newBv = new BoundVar(bv.tok, prefix + bv.Name, bv.Type);
+ bvars.Add(newBv);
+ var4var.Add(bv, newBv);
+ var ie = new IdentifierExpr(newBv.tok, newBv.Name);
+ ie.Var = newBv; // resolve here
+ ie.Type = newBv.Type; // resolve here
+ substMap.Add(bv, ie);
+ }
+ var s = new Substituter(null, substMap, new Dictionary<TypeParameter, Type>(), translator);
+ var range = exists.Range == null ? null : s.Substitute(exists.Range);
+ var term = s.Substitute(exists.Term);
+ var attrs = s.SubstAttributes(exists.Attributes);
+ var ex = new ExistsExpr(exists.tok, exists.TypeArgs, bvars, range, term, attrs);
+ if (exists.Bounds != null) {
+ ex.Bounds = exists.Bounds.ConvertAll(bound => s.SubstituteBoundedPool(bound));
+ }
+ if (exists.MissingBounds != null) {
+ ex.MissingBounds = exists.MissingBounds.ConvertAll(bv => var4var[bv]);
+ }
+ return ex;
+ }
+
+ /// <summary>
/// Generate:
/// havoc Heap \ {this} \ _reads \ _new;
/// assume this.Valid();
@@ -8569,7 +8635,7 @@ namespace Microsoft.Dafny {
void TrAlternatives(List<GuardedAlternative> alternatives, Bpl.Cmd elseCase0, Bpl.StructuredCmd elseCase1,
Bpl.StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
Contract.Requires(alternatives != null);
- Contract.Requires((elseCase0 != null) == (elseCase1 == null)); // ugly way of doing a type union
+ Contract.Requires((elseCase0 == null) != (elseCase1 == null)); // ugly way of doing a type union
Contract.Requires(builder != null);
Contract.Requires(locals != null);
Contract.Requires(etran != null);
@@ -8583,10 +8649,13 @@ namespace Microsoft.Dafny {
return;
}
+ // alpha-rename any existential guards
+ var guards = alternatives.ConvertAll(alt => alt.IsExistentialGuard ? AlphaRename((ExistsExpr)alt.Guard, "eg$", this) : alt.Guard);
+
// build the negation of the disjunction of all guards (that is, the conjunction of their negations)
Bpl.Expr noGuard = Bpl.Expr.True;
- foreach (var alternative in alternatives) {
- noGuard = BplAnd(noGuard, Bpl.Expr.Not(etran.TrExpr(alternative.Guard)));
+ foreach (var g in guards) {
+ noGuard = BplAnd(noGuard, Bpl.Expr.Not(etran.TrExpr(g)));
}
var b = new Bpl.StmtListBuilder();
@@ -8605,8 +8674,13 @@ namespace Microsoft.Dafny {
CurrentIdGenerator.Push();
var alternative = alternatives[i];
b = new Bpl.StmtListBuilder();
- TrStmt_CheckWellformed(alternative.Guard, b, locals, etran, true);
- b.Add(new AssumeCmd(alternative.Guard.tok, etran.TrExpr(alternative.Guard)));
+ TrStmt_CheckWellformed(guards[i], b, locals, etran, true);
+ if (alternative.IsExistentialGuard) {
+ var exists = (ExistsExpr)alternative.Guard; // the original (that is, not alpha-renamed) guard
+ IntroduceAndAssignExistentialVars(exists, b, builder, locals, etran);
+ } else {
+ b.Add(new AssumeCmd(alternative.Guard.tok, etran.TrExpr(alternative.Guard)));
+ }
foreach (var s in alternative.Body) {
TrStmt(s, b, locals, etran);
}
@@ -13705,6 +13779,9 @@ namespace Microsoft.Dafny {
Contract.Assert(false); // unexpected ComprehensionExpr
}
}
+ if (e.Bounds != null) {
+ ((ComprehensionExpr)newExpr).Bounds = e.Bounds.ConvertAll(bound => SubstituteBoundedPool(bound));
+ }
// undo any changes to substMap (could be optimized to do this only if newBoundVars != e.BoundVars)
foreach (var bv in e.BoundVars) {
substMap.Remove(bv);
@@ -13761,6 +13838,44 @@ namespace Microsoft.Dafny {
}
}
+ public ComprehensionExpr.BoundedPool SubstituteBoundedPool(ComprehensionExpr.BoundedPool bound) {
+ if (bound == null) {
+ return null;
+ } else if (bound is ComprehensionExpr.ExactBoundedPool) {
+ var b = (ComprehensionExpr.ExactBoundedPool)bound;
+ return new ComprehensionExpr.ExactBoundedPool(Substitute(b.E));
+ } else if (bound is ComprehensionExpr.BoolBoundedPool) {
+ return bound; // nothing to substitute
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ return bound; // nothing to substitute
+ } else if (bound is ComprehensionExpr.RefBoundedPool) {
+ return bound; // nothing to substitute
+ } else if (bound is ComprehensionExpr.IntBoundedPool) {
+ var b = (ComprehensionExpr.IntBoundedPool)bound;
+ return new ComprehensionExpr.IntBoundedPool(b.LowerBound == null ? null : Substitute(b.LowerBound), b.UpperBound == null ? null : Substitute(b.UpperBound));
+ } else if (bound is ComprehensionExpr.SetBoundedPool) {
+ var b = (ComprehensionExpr.SetBoundedPool)bound;
+ return new ComprehensionExpr.SetBoundedPool(Substitute(b.Set));
+ } else if (bound is ComprehensionExpr.SubSetBoundedPool) {
+ var b = (ComprehensionExpr.SubSetBoundedPool)bound;
+ return new ComprehensionExpr.SubSetBoundedPool(Substitute(b.UpperBound));
+ } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {
+ var b = (ComprehensionExpr.SuperSetBoundedPool)bound;
+ return new ComprehensionExpr.SuperSetBoundedPool(Substitute(b.LowerBound));
+ } else if (bound is ComprehensionExpr.MapBoundedPool) {
+ var b = (ComprehensionExpr.MapBoundedPool)bound;
+ return new ComprehensionExpr.MapBoundedPool(Substitute(b.Map));
+ } else if (bound is ComprehensionExpr.SeqBoundedPool) {
+ var b = (ComprehensionExpr.SeqBoundedPool)bound;
+ return new ComprehensionExpr.SeqBoundedPool(Substitute(b.Seq));
+ } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {
+ return bound; // nothing to substitute
+ } else {
+ Contract.Assume(false); // unexpected ComprehensionExpr.BoundedPool
+ throw new cce.UnreachableException(); // to please compiler
+ }
+ }
+
/// <summary>
/// Return a list of bound variables, of the same length as 'vars' but with possible substitutions.
/// For any change necessary, update 'substMap' to reflect the new substitution; the caller is responsible for
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 09:09:44 +0000