From a748799eef1d751463e886debe4e0bd458406b7c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 4 Jun 2024 20:55:38 +0200 Subject: [PATCH] Split off parts of single pass compiler (#5526) ### Description - Split off parts of single pass compiler, which is the refactoring part of https://github.com/dafny-lang/dafny/pull/5509 ### How has this been tested? - No additional testing needed By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../SinglePassCodeGenerator.Expression.cs | 605 ++++++++++ .../SinglePassCodeGenerator.Statement.cs | 464 ++++++++ .../SinglePassCodeGenerator.cs | 1036 +---------------- 3 files changed, 1070 insertions(+), 1035 deletions(-) create mode 100644 Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs create mode 100644 Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs rename Source/DafnyCore/Backends/{ => SinglePassCodeGenerator}/SinglePassCodeGenerator.cs (83%) diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs new file mode 100644 index 0000000000..d73d5eb7d7 --- /dev/null +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs @@ -0,0 +1,605 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Numerics; +using System.IO; +using System.Diagnostics.Contracts; +using DafnyCore; +using JetBrains.Annotations; +using Microsoft.BaseTypes; +using static Microsoft.Dafny.GeneratorErrors; + +namespace Microsoft.Dafny.Compilers { + public abstract partial class SinglePassCodeGenerator { + + public virtual void EmitExpr(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { + if (expr is LiteralExpr) { + LiteralExpr e = (LiteralExpr)expr; + EmitLiteralExpr(wr, e); + + } else if (expr is ThisExpr) { + if (thisContext != null) { + var instantiatedType = expr.Type.Subst(thisContext.ParentFormalTypeParametersToActuals); + var contextType = UserDefinedType.FromTopLevelDecl(expr.tok, thisContext); + if (contextType.ResolvedClass is ClassLikeDecl { NonNullTypeDecl: { } } cls) { + contextType = UserDefinedType.FromTopLevelDecl(expr.tok, cls.NonNullTypeDecl); + } + + wr = EmitCoercionIfNecessary(contextType, instantiatedType, expr.tok, wr); + } + EmitThis(wr); + + } else if (expr is IdentifierExpr) { + var e = (IdentifierExpr)expr; + if (inLetExprBody && !(e.Var is BoundVar)) { + // copy variable to a temp since + // - C# doesn't allow out param in letExpr body, and + // - Java doesn't allow any non-final variable in letExpr body. + var name = ProtectedFreshId("_pat_let_tv"); + EmitIdentifier(name, wr); + DeclareLocalVar(name, null, null, false, IdName(e.Var), copyInstrWriters.Peek(), e.Type); + } else { + EmitIdentifier(IdName(e.Var), wr); + } + } else if (expr is SetDisplayExpr) { + var e = (SetDisplayExpr)expr; + EmitCollectionDisplay(e.Type.NormalizeToAncestorType().AsSetType, e.tok, e.Elements, inLetExprBody, wr, wStmts); + + } else if (expr is MultiSetDisplayExpr) { + var e = (MultiSetDisplayExpr)expr; + EmitCollectionDisplay(e.Type.NormalizeToAncestorType().AsMultiSetType, e.tok, e.Elements, inLetExprBody, wr, wStmts); + + } else if (expr is SeqDisplayExpr) { + var e = (SeqDisplayExpr)expr; + EmitCollectionDisplay(e.Type.NormalizeToAncestorType().AsSeqType, e.tok, e.Elements, inLetExprBody, wr, wStmts); + + } else if (expr is MapDisplayExpr) { + var e = (MapDisplayExpr)expr; + EmitMapDisplay(e.Type.NormalizeToAncestorType().AsMapType, e.tok, e.Elements, inLetExprBody, wr, wStmts); + + } else if (expr is MemberSelectExpr) { + MemberSelectExpr e = (MemberSelectExpr)expr; + SpecialField sf = e.Member as SpecialField; + if (sf != null) { + GetSpecialFieldInfo(sf.SpecialId, sf.IdParam, e.Obj.Type, out var compiledName, out var preStr, out var postStr); + wr.Write(preStr); + + if (sf.IsStatic && !SupportsStaticsInGenericClasses && sf.EnclosingClass.TypeArgs.Count != 0) { + var typeArgs = e.TypeApplication_AtEnclosingClass; + Contract.Assert(typeArgs.Count == sf.EnclosingClass.TypeArgs.Count); + wr.Write("{0}.", TypeName_Companion(e.Obj.Type, wr, e.tok, sf)); + EmitNameAndActualTypeArgs(IdName(e.Member), typeArgs, e.tok, null, false, wr); + var tas = TypeArgumentInstantiation.ListFromClass(sf.EnclosingClass, typeArgs); + EmitTypeDescriptorsActuals(tas, e.tok, wr.ForkInParens()); + } else { + void writeObj(ConcreteSyntaxTree w) { + //Contract.Assert(!sf.IsStatic); + w = EmitCoercionIfNecessary(e.Obj.Type, UserDefinedType.UpcastToMemberEnclosingType(e.Obj.Type, e.Member), e.tok, w); + TrParenExpr(e.Obj, w, inLetExprBody, wStmts); + } + + var typeArgs = CombineAllTypeArguments(e.Member, e.TypeApplication_AtEnclosingClass, e.TypeApplication_JustMember); + EmitMemberSelect(writeObj, e.Obj.Type, e.Member, typeArgs, e.TypeArgumentSubstitutionsWithParents(), expr.Type).EmitRead(wr); + } + + wr.Write(postStr); + } else { + var typeArgs = CombineAllTypeArguments(e.Member, e.TypeApplication_AtEnclosingClass, e.TypeApplication_JustMember); + var typeMap = e.TypeArgumentSubstitutionsWithParents(); + var customReceiver = NeedsCustomReceiverNotTrait(e.Member); + if (!customReceiver && !e.Member.IsStatic) { + Action obj; + // The eta conversion here is to avoid capture of the receiver, because the call to EmitMemberSelect below may generate + // a lambda expression in the target language. + if (e.Member is Function && typeArgs.Count != 0) { + // need to eta-expand wrap the receiver + var etaReceiver = ProtectedFreshId("_eta_this"); + wr = CreateIIFE_ExprBody(etaReceiver, e.Obj.Type, e.Obj.tok, e.Obj, inLetExprBody, e.Type.Subst(typeMap), e.tok, wr, ref wStmts); + obj = w => EmitIdentifier(etaReceiver, w); + } else { + obj = w => EmitExpr(e.Obj, inLetExprBody, w, wStmts); + } + EmitMemberSelect(obj, e.Obj.Type, e.Member, typeArgs, typeMap, expr.Type).EmitRead(wr); + } else { + string customReceiverName = null; + if (customReceiver && e.Member is Function) { + // need to eta-expand wrap the receiver + customReceiverName = ProtectedFreshId("_eta_this"); + wr = CreateIIFE_ExprBody(customReceiverName, e.Obj.Type, e.Obj.tok, e.Obj, inLetExprBody, e.Type.Subst(typeMap), e.tok, wr, ref wStmts); + } + Action obj = w => EmitTypeName_Companion(e.Obj.Type, w, wr, e.tok, e.Member); + EmitMemberSelect(obj, e.Obj.Type, e.Member, typeArgs, typeMap, expr.Type, customReceiverName).EmitRead(wr); + } + } + } else if (expr is SeqSelectExpr) { + SeqSelectExpr e = (SeqSelectExpr)expr; + Contract.Assert(e.Seq.Type != null); + if (e.Seq.Type.IsArrayType) { + if (e.SelectOne) { + Contract.Assert(e.E0 != null && e.E1 == null); + var w = EmitArraySelect(new List() { e.E0 }, e.Type, inLetExprBody, wr, wStmts); + w = EmitCoercionIfNecessary( + e.Seq.Type, + e.Seq.Type.IsNonNullRefType || !e.Seq.Type.IsRefType ? null : UserDefinedType.CreateNonNullType((UserDefinedType)e.Seq.Type.NormalizeExpand()), + e.tok, + w + ); + TrParenExpr(e.Seq, w, inLetExprBody, wStmts); + } else { + EmitSeqSelectRange(e.Seq, e.E0, e.E1, true, inLetExprBody, wr, wStmts); + } + } else if (e.SelectOne) { + Contract.Assert(e.E0 != null && e.E1 == null); + EmitIndexCollectionSelect(e.Seq, e.E0, inLetExprBody, wr, wStmts); + } else { + EmitSeqSelectRange(e.Seq, e.E0, e.E1, false, inLetExprBody, wr, wStmts); + } + } else if (expr is SeqConstructionExpr) { + var e = (SeqConstructionExpr)expr; + EmitSeqConstructionExpr(e, inLetExprBody, wr, wStmts); + } else if (expr is MultiSetFormingExpr) { + var e = (MultiSetFormingExpr)expr; + EmitMultiSetFormingExpr(e, inLetExprBody, wr, wStmts); + } else if (expr is MultiSelectExpr) { + MultiSelectExpr e = (MultiSelectExpr)expr; + WriteCast(TypeName(e.Type.NormalizeExpand(), wr, e.tok), wr); + var w = EmitArraySelect(e.Indices, e.Type, inLetExprBody, wr, wStmts); + TrParenExpr(e.Array, w, inLetExprBody, wStmts); + + } else if (expr is SeqUpdateExpr) { + SeqUpdateExpr e = (SeqUpdateExpr)expr; + var collectionType = e.Type.NormalizeToAncestorType().AsCollectionType; + Contract.Assert(collectionType != null); + EmitIndexCollectionUpdate(e.Seq, e.Index, e.Value, collectionType, inLetExprBody, wr, wStmts); + } else if (expr is DatatypeUpdateExpr) { + var e = (DatatypeUpdateExpr)expr; + if (e.Members.All(member => member.IsGhost)) { + // all fields to be updated are ghost, which doesn't change the value + EmitExpr(e.Root, inLetExprBody, wr, wStmts); + return; + } + if (DatatypeWrapperEraser.IsErasableDatatypeWrapper(Options, e.Root.Type.AsDatatype, out var dtor)) { + var i = e.Members.IndexOf(dtor); + if (0 <= i) { + // the datatype is an erasable wrapper and its core destructor is part of the update (which implies everything else must be a ghost), + // so proceed as with the rhs + Contract.Assert(Enumerable.Range(0, e.Members.Count).All(j => j == i || e.Members[j].IsGhost)); + Contract.Assert(e.Members.Count == e.Updates.Count); + var rhs = e.Updates[i].Item3; + EmitExpr(rhs, inLetExprBody, wr, wStmts); + return; + } + } + // the optimized cases don't apply, so proceed according to the desugaring + EmitExpr(e.ResolvedExpression, inLetExprBody, wr, wStmts); + } else if (expr is FunctionCallExpr) { + FunctionCallExpr e = (FunctionCallExpr)expr; + + void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyntaxTree wStmts2) { + this.EmitExpr(e2, inLetExpr, wr2, wStmts2); + } + + if (e.Function is SpecialFunction) { + CompileSpecialFunctionCallExpr(e, wr, inLetExprBody, wStmts, EmitExpr); + } else { + CompileFunctionCallExpr(e, wr, inLetExprBody, wStmts, EmitExpr); + } + + } else if (expr is ApplyExpr) { + var e = expr as ApplyExpr; + EmitApplyExpr(e.Function.Type, e.tok, e.Function, e.Args, inLetExprBody, wr, wStmts); + + } else if (expr is DatatypeValue) { + var dtv = (DatatypeValue)expr; + Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved + + if (DatatypeWrapperEraser.IsErasableDatatypeWrapper(Options, dtv.Ctor.EnclosingDatatype, out var dtor)) { + var i = dtv.Ctor.Destructors.IndexOf(dtor); + Contract.Assert(0 <= i); + EmitExpr(dtv.Arguments[i], inLetExprBody, wr, wStmts); + return; + } + + var wrArgumentList = new ConcreteSyntaxTree(); + var wTypeDescriptorArguments = new ConcreteSyntaxTree(); + var typeSubst = TypeParameter.SubstitutionMap(dtv.Ctor.EnclosingDatatype.TypeArgs, dtv.InferredTypeArgs); + string sep = ""; + Contract.Assert(dtv.Ctor.EnclosingDatatype.TypeArgs.Count == dtv.InferredTypeArgs.Count); + WriteTypeDescriptors(dtv.Ctor.EnclosingDatatype, dtv.InferredTypeArgs, wTypeDescriptorArguments, ref sep); + sep = ""; + for (var i = 0; i < dtv.Arguments.Count; i++) { + var formal = dtv.Ctor.Formals[i]; + if (!formal.IsGhost) { + wrArgumentList.Write(sep); + var w = EmitCoercionIfNecessary(@from: dtv.Arguments[i].Type, to: dtv.Ctor.Formals[i].Type.Subst(typeSubst), toOrig: dtv.Ctor.Formals[i].Type, tok: dtv.tok, wr: wrArgumentList); + EmitExpr(dtv.Arguments[i], inLetExprBody, w, wStmts); + sep = ", "; + } + } + EmitDatatypeValue(dtv, wTypeDescriptorArguments.ToString(), wrArgumentList.ToString(), wr); + + } else if (expr is OldExpr) { + Contract.Assert(false); throw new cce.UnreachableException(); // 'old' is always a ghost + + } else if (expr is UnaryOpExpr) { + var e = (UnaryOpExpr)expr; + if (e.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BVNot) { + wr = EmitBitvectorTruncation(e.Type.NormalizeToAncestorType().AsBitVectorType, e.Type.AsNativeType(), true, wr); + } + EmitUnaryExpr(UnaryOpCodeMap[e.ResolvedOp], e.E, inLetExprBody, wr, wStmts); + } else if (expr is ConversionExpr) { + var e = (ConversionExpr)expr; + var fromType = e.E.Type.GetRuntimeType(); + var toType = e.ToType.GetRuntimeType(); + Contract.Assert(Options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy || toType.IsRefType == fromType.IsRefType); + if (toType.IsRefType || toType.IsTraitType || fromType.IsTraitType) { + var w = EmitCoercionIfNecessary(e.E.Type, e.ToType, e.tok, wr); + w = EmitDowncastIfNecessary(e.E.Type, e.ToType, e.tok, w); + EmitExpr(e.E, inLetExprBody, w, wStmts); + } else { + EmitConversionExpr(e.E, fromType, toType, inLetExprBody, wr, wStmts); + } + + } else if (expr is TypeTestExpr typeTestExpr) { + CompileTypeTest(typeTestExpr, inLetExprBody, wr, ref wStmts); + + } else if (expr is BinaryExpr) { + var e = (BinaryExpr)expr; + + if (IsComparisonToZero(e, out var arg, out var sign, out var negated) && + CompareZeroUsingSign(arg.Type)) { + // Transform e.g. x < BigInteger.Zero into x.Sign == -1 + var w = EmitSign(arg.Type, wr); + TrParenExpr(arg, w, inLetExprBody, wStmts); + wr.Write(negated ? " != " : " == "); + wr.Write(sign.ToString()); + } else { + CompileBinOp(e.ResolvedOp, e.E0, e.E1, e.tok, expr.Type.GetRuntimeType(), + out var opString, + out var preOpString, + out var postOpString, + out var callString, + out var staticCallString, + out var reverseArguments, + out var truncateResult, + out var convertE1_to_int, + out var coerceE1, + wr); + + if (truncateResult && e.Type.NormalizeToAncestorType().AsBitVectorType is { } bitvectorType) { + wr = EmitBitvectorTruncation(bitvectorType, e.Type.AsNativeType(), true, wr); + } + var e0 = reverseArguments ? e.E1 : e.E0; + var e1 = reverseArguments ? e.E0 : e.E1; + + var left = Expr(e0, inLetExprBody, wStmts); + ConcreteSyntaxTree right; + if (convertE1_to_int) { + right = ExprAsNativeInt(e1, inLetExprBody, wStmts); + } else { + right = Expr(e1, inLetExprBody, wStmts); + if (coerceE1) { + right = CoercionIfNecessary(e1.Type, TypeForCoercion(e1.Type), e1.tok, right); + } + } + + wr.Write(preOpString); + if (opString != null) { + var nativeType = AsNativeType(e.Type); + string nativeName = null; + bool needsCast = false; + if (nativeType != null) { + GetNativeInfo(nativeType.Sel, out nativeName, out _, out needsCast); + } + + var opResult = ConcreteSyntaxTree.Create($"{left.InParens()} {opString} {right.InParens()}"); + if (needsCast) { + opResult = Cast(new LineSegment(nativeName), opResult); + } + + wr.Append(opResult); + } else if (callString != null) { + wr.Format($"{left.InParens()}.{callString}({right})"); + } else if (staticCallString != null) { + wr.Format($"{staticCallString}({left}, {right})"); + } + wr.Write(postOpString); + } + } else if (expr is TernaryExpr) { + Contract.Assume(false); // currently, none of the ternary expressions is compilable + + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + if (e.Exact) { + // The Dafny "let" expression + // var Pattern(x,y) := G; E + // is translated into C# as: + // LamLet(G, tmp => + // LamLet(dtorX(tmp), x => + // LamLet(dtorY(tmp), y => E))) + Contract.Assert(e.LHSs.Count == e.RHSs.Count); // checked by resolution + var w = wr; + for (int i = 0; i < e.LHSs.Count; i++) { + var lhs = e.LHSs[i]; + if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) { + var rhsName = $"_pat_let{GetUniqueAstNumber(e)}_{i}"; + w = CreateIIFE_ExprBody(rhsName, e.RHSs[i].Type, e.RHSs[i].tok, e.RHSs[i], inLetExprBody, e.Body.Type, e.Body.tok, w, ref wStmts); + w = TrCasePattern(lhs, wr => EmitIdentifier(rhsName, wr), e.RHSs[i].Type, e.Body.Type, w, ref wStmts); + } + } + EmitExpr(e.Body, true, w, wStmts); + } else if (e.BoundVars.All(bv => bv.IsGhost)) { + // The Dafny "let" expression + // ghost var x,y :| Constraint; E + // is compiled just like E is, because the resolver has already checked that x,y (or other ghost variables, for that matter) don't + // occur in E (moreover, the verifier has checked that values for x,y satisfying Constraint exist). + EmitExpr(e.Body, inLetExprBody, wr, wStmts); + } else { + // The Dafny "let" expression + // var x,y :| Constraint; E + // is translated into C# as: + // LamLet(0, dummy => { // the only purpose of this construction here is to allow us to add some code inside an expression in C# + // var x,y; + // // Embark on computation that fills in x,y according to Constraint; the computation stops when the first + // // such value is found, but since the verifier checks that x,y follows uniquely from Constraint, this is + // // not a source of nondeterminancy. + // return E; + // }) + Contract.Assert(e.RHSs.Count == 1); // checked by resolution + var missingBounds = BoolBoundedPool.MissingBounds(e.BoundVars.ToList(), e.Constraint_Bounds, BoundedPool.PoolVirtues.Enumerable); + if (missingBounds.Count != 0) { + foreach (var bv in missingBounds) { + Error(ErrorId.c_let_such_that_is_too_complex, e.tok, "this let-such-that expression is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}'", wr, bv.Name); + } + } else { + var w = CreateIIFE1(0, e.Body.Type, e.Body.tok, "_let_dummy_" + GetUniqueAstNumber(e), wr, wStmts); + foreach (var bv in e.BoundVars) { + DeclareLocalVar(IdName(bv), bv.Type, bv.tok, false, ForcePlaceboValue(bv.Type, wr, bv.tok, true), w); + } + TrAssignSuchThat(new List(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0], e.Constraint_Bounds, e.tok.line, w, inLetExprBody); + EmitReturnExpr(e.Body, e.Body.Type, true, w); + } + } + } else if (expr is NestedMatchExpr nestedMatchExpr) { + EmitExpr(nestedMatchExpr.Flattened, inLetExprBody, wr, wStmts); + } else if (expr is MatchExpr matchExpr) { + EmitMatchExpr(inLetExprBody, wr, wStmts, matchExpr); + } else if (expr is QuantifierExpr) { + var e = (QuantifierExpr)expr; + + // Compilation does not check whether a quantifier was split. + + wr = CaptureFreeVariables(expr, true, out var su, inLetExprBody, wr, ref wStmts); + var logicalBody = su.Substitute(e.LogicalBody(true)); + + Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds + var n = e.BoundVars.Count; + Contract.Assert(e.Bounds.Count == n); + var wBody = wr; + for (int i = 0; i < n; i++) { + var bound = e.Bounds[i]; + var bv = e.BoundVars[i]; + + var collectionElementType = CompileCollection(bound, bv, inLetExprBody, false, su, out var collection, wStmts, e.Bounds, e.BoundVars, i); + wBody = EmitQuantifierExpr(collection, expr is ForallExpr, collectionElementType, bv, wBody); + var native = AsNativeType(e.BoundVars[i].Type); + var tmpVarName = ProtectedFreshId(e is ForallExpr ? "_forall_var_" : "_exists_var_"); + ConcreteSyntaxTree newWBody = CreateLambda(new List { collectionElementType }, e.tok, new List { tmpVarName }, Type.Bool, wBody, wStmts, untyped: true); + wStmts = newWBody.Fork(); + newWBody = MaybeInjectSubtypeConstraintWrtTraits( + tmpVarName, collectionElementType, bv.Type, + inLetExprBody, e.tok, newWBody, true, e is ForallExpr); + EmitDowncastVariableAssignment( + IdName(bv), bv.Type, tmpVarName, collectionElementType, true, e.tok, newWBody); + newWBody = MaybeInjectSubsetConstraint( + bv, bv.Type, inLetExprBody, e.tok, newWBody, isReturning: true, elseReturnValue: e is ForallExpr); + wBody = newWBody; + } + EmitExpr(logicalBody, inLetExprBody, wBody, wStmts); + + } else if (expr is SetComprehension) { + var e = (SetComprehension)expr; + // For "set i,j,k,l | R(i,j,k,l) :: Term(i,j,k,l)" where the term has type "G", emit something like: + // ((System.Func>)(() => { + // var _coll = new List(); + // foreach (var tmp_l in sq.Elements) { L l = (L)tmp_l; + // foreach (var tmp_k in st.Elements) { K k = (K)tmp_k; + // for (BigInteger j = Lo; j < Hi; j++) { + // for (bool i in Helper.AllBooleans) { + // if (R(i,j,k,l)) { + // _coll.Add(Term(i,j,k,l)); + // } + // } + // } + // } + // } + // return Dafny.Set.FromCollection(_coll); + // }))() + // We also split R(i,j,k,l) to evaluate it as early as possible. + wr = CaptureFreeVariables(e, true, out var su, inLetExprBody, wr, ref wStmts); + e = (SetComprehension)su.Substitute(e); + + Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds + var collectionName = ProtectedFreshId("_coll"); + var setType = e.Type.NormalizeToAncestorType().AsSetType; + var bwr = CreateIIFE0(setType, e.tok, wr, wStmts); + wStmts = bwr.Fork(); + wr = bwr; + EmitSetBuilder_New(wr, e, collectionName); + var n = e.BoundVars.Count; + Contract.Assert(e.Bounds.Count == n); + var processedBounds = new HashSet(); + List<(Expression conj, ISet frees)> unusedConjuncts = Expression.Conjuncts(e.Range).Select(conj => (conj, ModuleResolver.FreeVariables(conj))).ToList(); + unusedConjuncts.ForEach(entry => entry.frees.IntersectWith(e.BoundVars)); + wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr); + for (var i = 0; i < n; i++) { + var bound = e.Bounds[i]; + var bv = e.BoundVars[i]; + processedBounds.Add(bv); + var tmpVar = ProtectedFreshId("_compr_"); + var wStmtsLoop = wr.Fork(); + var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, wStmtsLoop); + wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, true, inLetExprBody, e.tok, collection, wr); + wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr); + } + + EmitSetBuilder_Add(setType, collectionName, e.Term, inLetExprBody, wr); + var returned = EmitReturnExpr(bwr); + GetCollectionBuilder_Build(setType, e.tok, collectionName, returned, wStmts); + + } else if (expr is MapComprehension) { + var e = (MapComprehension)expr; + // For "map i | R(i) :: Term(i)" where the term has type "V" and i has type "U", emit something like: + // ((System.Func>)(() => { + // var _coll = new List>(); + // foreach (L l in sq.Elements) { + // foreach (K k in st.Elements) { + // for (BigInteger j = Lo; j < Hi; j++) { + // for (bool i in Helper.AllBooleans) { + // if (R(i,j,k,l)) { + // _coll.Add(new Pair(i, Term(i)); + // } + // } + // } + // } + // } + // return Dafny.Map.FromCollection(_coll); + // }))() + // We also split R(i,j,k,l) to evaluate it as early as possible. + wr = CaptureFreeVariables(e, true, out var su, inLetExprBody, wr, ref wStmts); + e = (MapComprehension)su.Substitute(e); + + Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds + var mapType = e.Type.NormalizeToAncestorType().AsMapType; + var domtypeName = TypeName(mapType.Domain, wr, e.tok); + var rantypeName = TypeName(mapType.Range, wr, e.tok); + var collection_name = ProtectedFreshId("_coll"); + var bwr = CreateIIFE0(mapType, e.tok, wr, wStmts); + wStmts = bwr.Fork(); + wr = bwr; + EmitMapBuilder_New(wr, e, collection_name); + var n = e.BoundVars.Count; + Contract.Assert(e.Bounds.Count == n); + var processedBounds = new HashSet(); + List<(Expression conj, ISet frees)> unusedConjuncts = Expression.Conjuncts(e.Range).Select(conj => (conj, ModuleResolver.FreeVariables(conj))).ToList(); + unusedConjuncts.ForEach(entry => entry.frees.IntersectWith(e.BoundVars)); + wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr); + for (var i = 0; i < n; i++) { + var bound = e.Bounds[i]; + var bv = e.BoundVars[i]; + processedBounds.Add(bv); + var tmpVar = ProtectedFreshId("_compr_"); + var wStmtsLoop = wr.Fork(); + var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, wStmtsLoop); + wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, true, false, bv.tok, collection, wr); + wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr); + } + + var termLeftWriter = EmitMapBuilder_Add(mapType, e.tok, collection_name, e.Term, inLetExprBody, wr); + if (e.TermLeft == null) { + Contract.Assert(e.BoundVars.Count == 1); + EmitIdentifier(IdName(e.BoundVars[0]), termLeftWriter); + } else { + EmitExpr(e.TermLeft, inLetExprBody, termLeftWriter, wStmts); + } + + var returned = EmitReturnExpr(bwr); + GetCollectionBuilder_Build(mapType, e.tok, collection_name, returned, wStmts); + + } else if (expr is LambdaExpr) { + var e = (LambdaExpr)expr; + + IVariable receiver = null; + if (thisContext != null && (enclosingMethod is { IsTailRecursive: true } || enclosingFunction is { IsTailRecursive: true })) { + var name = ProtectedFreshId("_this"); + var ty = ModuleResolver.GetThisType(e.tok, thisContext); + receiver = new LocalVariable(RangeToken.NoToken, name, ty, false) { + type = ty + }; + var _this = new ThisExpr(thisContext); + wr = EmitBetaRedex(new List() { IdName(receiver) }, new List() { _this }, new List() { _this.Type }, expr.Type, expr.tok, inLetExprBody, wr, ref wStmts); + } + + wr = CaptureFreeVariables(e, false, out var su, inLetExprBody, wr, ref wStmts); + if (receiver != null) { + su = new Substituter(new IdentifierExpr(e.tok, receiver), su.substMap, su.typeMap); + } + + wr = CreateLambda(e.BoundVars.ConvertAll(bv => bv.Type), Token.NoToken, e.BoundVars.ConvertAll(IdName), e.Body.Type, wr, wStmts); + wStmts = wr.Fork(); + wr = EmitReturnExpr(wr); + // May need an upcast or boxing conversion to coerce to the generic arrow result type + wr = EmitCoercionIfNecessary(e.Body.Type, TypeForCoercion(e.Type.AsArrowType.Result), e.Body.tok, wr); + EmitExpr(su.Substitute(e.Body), inLetExprBody, wr, wStmts); + + } else if (expr is StmtExpr) { + var e = (StmtExpr)expr; + EmitExpr(e.E, inLetExprBody, wr, wStmts); + + } else if (expr is ITEExpr) { + var e = (ITEExpr)expr; + // The ghost-ITE optimization applies only to at "the top" of the expression structure of a function + // body. Those cases are handled in TrExprOpt, so we expect the be compiling both branches here. + Contract.Assert(e.HowToCompile == ITEExpr.ITECompilation.CompileBothBranches); + EmitITE(e.Test, e.Thn, e.Els, e.Type, inLetExprBody, wr, wStmts); + + } else if (expr is ConcreteSyntaxExpression) { + var e = (ConcreteSyntaxExpression)expr; + EmitExpr(e.ResolvedExpression, inLetExprBody, wr, wStmts); + + } else { + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + } + ConcreteSyntaxTree EmitGuardFragment(List<(Expression conj, ISet frees)> unusedConjuncts, HashSet processedBounds, ConcreteSyntaxTree wr) { + Expression localGuard = Expression.CreateBoolLiteral(expr.tok, true); + + foreach (var entry in unusedConjuncts.ToList().Where(entry => entry.frees.IsSubsetOf(processedBounds))) { + localGuard = Expression.CreateAnd(localGuard, entry.conj); + unusedConjuncts.Remove(entry); + } + + if (!LiteralExpr.IsTrue(localGuard)) { + wr = EmitIf(out var guardWriter, false, wr); + EmitExpr(localGuard, inLetExprBody, guardWriter, wStmts); + } + + return wr; + } + } + + private void EmitMatchExpr(bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, MatchExpr e) { + // ((System.Func)((SourceType _source) => { + // if (source.is_Ctor0) { + // FormalType f0 = ((Dt_Ctor0)source._D).a0; + // ... + // return Body0; + // } else if (...) { + // ... + // } else if (true) { + // ... + // } + // }))(src) + + EmitLambdaApply(wr, out var wLambda, out var wArg); + + string source = ProtectedFreshId("_source"); + ConcreteSyntaxTree w; + w = CreateLambda(new List() { e.Source.Type }, e.tok, new List() { source }, e.Type, wLambda, wStmts); + + if (e.Cases.Count == 0) { + // the verifier would have proved we never get here; still, we need some code that will compile + EmitAbsurd(null, w); + } else { + int i = 0; + var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand(); + foreach (MatchCaseExpr mc in e.Cases) { + var wCase = MatchCasePrelude(source, sourceType, mc.Ctor, mc.Arguments, i, e.Cases.Count, w); + TrExprOpt(mc.Body, mc.Body.Type, wCase, wStmts, inLetExprBody: true, accumulatorVar: null); + i++; + } + } + // We end with applying the source expression to the delegate we just built + EmitExpr(e.Source, inLetExprBody, wArg, wStmts); + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs new file mode 100644 index 0000000000..d9f46af9c3 --- /dev/null +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs @@ -0,0 +1,464 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Numerics; +using System.IO; +using System.Diagnostics.Contracts; +using DafnyCore; +using JetBrains.Annotations; +using Microsoft.BaseTypes; +using static Microsoft.Dafny.GeneratorErrors; + +namespace Microsoft.Dafny.Compilers { + public abstract partial class SinglePassCodeGenerator { + + + protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts = null) { + Contract.Requires(stmt != null); + Contract.Requires(wr != null); + + wStmts ??= wr.Fork(); + + if (stmt.IsGhost) { + return; + } + if (stmt is PrintStmt) { + var s = (PrintStmt)stmt; + foreach (var arg in s.Args) { + EmitPrintStmt(wr, arg); + } + } else if (stmt is BreakStmt) { + var s = (BreakStmt)stmt; + var label = s.TargetStmt.Labels.Data.AssignUniqueId(idGenerator); + if (s.IsContinue) { + EmitContinue(label, wr); + } else { + EmitBreak(label, wr); + } + } else if (stmt is ProduceStmt) { + var s = (ProduceStmt)stmt; + var isTailRecursiveResult = false; + if (s.HiddenUpdate != null) { + TrStmt(s.HiddenUpdate, wr); + var ss = s.HiddenUpdate.ResolvedStatements; + if (ss.Count == 1 && ss[0] is AssignStmt assign && assign.Rhs is ExprRhs eRhs && eRhs.Expr.Resolved is FunctionCallExpr fce && IsTailRecursiveByMethodCall(fce)) { + isTailRecursiveResult = true; + } + } + if (s is YieldStmt) { + EmitYield(wr); + } else if (!isTailRecursiveResult) { + EmitReturn(this.enclosingMethod.Outs, wr); + } + } else if (stmt is UpdateStmt) { + var s = (UpdateStmt)stmt; + var resolved = s.ResolvedStatements; + if (resolved.Count == 1) { + TrStmt(resolved[0], wr); + } else { + var assignStmts = resolved.Cast().Where(assignStmt => !assignStmt.IsGhost).ToList(); + var lhss = new List(); + var rhss = new List(); + + // multi-assignment + Contract.Assert(s.Lhss.Count == resolved.Count); + Contract.Assert(s.Rhss.Count == resolved.Count); + var lhsTypes = new List(); + var rhsTypes = new List(); + foreach (var assignStmt in assignStmts) { + var rhs = assignStmt.Rhs; + if (rhs is HavocRhs) { + if (Options.ForbidNondeterminism) { + Error(ErrorId.c_nondeterminism_forbidden, rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr); + } + } else { + var lhs = assignStmt.Lhs; + rhss.Add(rhs); + lhss.Add(lhs); + lhsTypes.Add(lhs.Type); + rhsTypes.Add(TypeOfRhs(rhs)); + } + } + + var wStmtsPre = wStmts.Fork(); + var lvalues = new List(); + foreach (Expression lhs in lhss) { + lvalues.Add(CreateLvalue(lhs, wStmts, wStmtsPre)); + } + + EmitMultiAssignment(lhss, lvalues, lhsTypes, out var wRhss, rhsTypes, wr); + for (int i = 0; i < wRhss.Count; i++) { + TrRhs(rhss[i], wRhss[i], wStmts); + } + } + } else if (stmt is AssignStmt) { + var s = (AssignStmt)stmt; + Contract.Assert(s.Lhs is not SeqSelectExpr expr || expr.SelectOne); // multi-element array assignments are not allowed + if (s.Rhs is HavocRhs) { + if (Options.ForbidNondeterminism) { + Error(ErrorId.c_nondeterminism_forbidden, s.Rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr); + } + } else if (s.Rhs is ExprRhs eRhs && eRhs.Expr.Resolved is FunctionCallExpr fce && IsTailRecursiveByMethodCall(fce)) { + TrTailCallStmt(s.Tok, fce.Function.ByMethodDecl, fce.Receiver, fce.Args, null, wr); + } else { + var lvalue = CreateLvalue(s.Lhs, wr, wStmts); + wStmts = wr.Fork(); + var wRhs = EmitAssignment(lvalue, TypeOfLhs(s.Lhs), TypeOfRhs(s.Rhs), wr, stmt.Tok); + TrRhs(s.Rhs, wRhs, wStmts); + } + + } else if (stmt is AssignSuchThatStmt) { + var s = (AssignSuchThatStmt)stmt; + if (Options.ForbidNondeterminism) { + Error(ErrorId.c_assign_such_that_forbidden, s.Tok, "assign-such-that statement forbidden by the --enforce-determinism option", wr); + } + var lhss = s.Lhss.ConvertAll(lhs => ((IdentifierExpr)lhs.Resolved).Var); // the resolver allows only IdentifierExpr left-hand sides + var missingBounds = BoundedPool.MissingBounds(lhss, s.Bounds, BoundedPool.PoolVirtues.Enumerable); + if (missingBounds.Count != 0) { + foreach (var bv in missingBounds) { + Error(ErrorId.c_assign_such_that_is_too_complex, s.Tok, "this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}'", wr, bv.Name); + } + } else { + Contract.Assert(s.Bounds != null); + TrAssignSuchThat(lhss, s.Expr, s.Bounds, s.Tok.line, wr, false); + } + } else if (stmt is AssignOrReturnStmt) { + var s = (AssignOrReturnStmt)stmt; + // TODO there's potential here to use target-language specific features such as exceptions + // to make it more target-language idiomatic and improve performance + TrStmtList(s.ResolvedStatements, wr); + + } else if (stmt is ExpectStmt) { + var s = (ExpectStmt)stmt; + // TODO there's potential here to use target-language specific features such as exceptions + // to make it more target-language idiomatic and improve performance + ConcreteSyntaxTree bodyWriter = EmitIf(out var guardWriter, false, wr); + var negated = new UnaryOpExpr(s.Tok, UnaryOpExpr.Opcode.Not, s.Expr); + negated.Type = Type.Bool; + EmitExpr(negated, false, guardWriter, wStmts); + EmitHalt(s.Tok, s.Message, bodyWriter); + + } else if (stmt is CallStmt) { + var s = (CallStmt)stmt; + var wrBefore = wr.Fork(); + var wrCall = wr.Fork(); + var wrAfter = wr; + TrCallStmt(s, null, wrCall, wrBefore, wrAfter); + + } else if (stmt is BlockStmt) { + var w = EmitBlock(wr); + TrStmtList(((BlockStmt)stmt).Body, w); + + } else if (stmt is IfStmt) { + IfStmt s = (IfStmt)stmt; + if (s.Guard == null) { + if (Options.ForbidNondeterminism) { + Error(ErrorId.c_nondeterministic_if_forbidden, s.Tok, "nondeterministic if statement forbidden by the --enforce-determinism option", wr); + } + // we can compile the branch of our choice + ConcreteSyntaxTree guardWriter; + if (s.Els == null) { + // let's compile the "else" branch, since that involves no work + // (still, let's leave a marker in the source code to indicate that this is what we did) + Coverage.UnusedInstrumentationPoint(s.Thn.Tok, "then branch"); + var notFalse = (UnaryOpExpr)Expression.CreateNot(s.Thn.Tok, Expression.CreateBoolLiteral(s.Thn.Tok, false)); + var thenWriter = EmitIf(out guardWriter, false, wr); + EmitUnaryExpr(ResolvedUnaryOp.BoolNot, notFalse.E, false, guardWriter, wStmts); + Coverage.Instrument(s.Tok, "implicit else branch", wr); + thenWriter = EmitIf(out guardWriter, false, thenWriter); + EmitUnaryExpr(ResolvedUnaryOp.BoolNot, notFalse.E, false, guardWriter, wStmts); + TrStmtList(new List(), thenWriter); + } else { + // let's compile the "then" branch + wr = EmitIf(out guardWriter, false, wr); + EmitExpr(Expression.CreateBoolLiteral(s.Thn.tok, true), false, guardWriter, wStmts); + Coverage.Instrument(s.Thn.Tok, "then branch", wr); + TrStmtList(s.Thn.Body, wr); + Coverage.UnusedInstrumentationPoint(s.Els.Tok, "else branch"); + } + } else { + if (s.IsBindingGuard && Options.ForbidNondeterminism) { + Error(ErrorId.c_binding_if_forbidden, s.Tok, "binding if statement forbidden by the --enforce-determinism option", wr); + } + + var coverageForElse = Coverage.IsRecording && !(s.Els is IfStmt); + var thenWriter = EmitIf(out var guardWriter, s.Els != null || coverageForElse, wr); + EmitExpr(s.IsBindingGuard ? ((ExistsExpr)s.Guard).AlphaRename("eg_d") : s.Guard, false, guardWriter, wStmts); + // We'd like to do "TrStmt(s.Thn, indent)", except we want the scope of any existential variables to come inside the block + if (s.IsBindingGuard) { + IntroduceAndAssignBoundVars((ExistsExpr)s.Guard, thenWriter); + } + Coverage.Instrument(s.Thn.Tok, "then branch", thenWriter); + TrStmtList(s.Thn.Body, thenWriter); + + if (coverageForElse) { + wr = EmitBlock(wr); + if (s.Els == null) { + Coverage.Instrument(s.Tok, "implicit else branch", wr); + } else { + Coverage.Instrument(s.Els.Tok, "else branch", wr); + } + } + if (s.Els != null) { + TrStmtNonempty(s.Els, wr, wStmts); + } + } + + } else if (stmt is AlternativeStmt) { + var s = (AlternativeStmt)stmt; + if (Options.ForbidNondeterminism && 2 <= s.Alternatives.Count) { + Error(ErrorId.c_case_based_if_forbidden, s.Tok, "case-based if statement forbidden by the --enforce-determinism option", wr); + } + foreach (var alternative in s.Alternatives) { + var thn = EmitIf(out var guardWriter, true, wr); + EmitExpr(alternative.IsBindingGuard ? ((ExistsExpr)alternative.Guard).AlphaRename("eg_d") : alternative.Guard, false, guardWriter, wStmts); + if (alternative.IsBindingGuard) { + IntroduceAndAssignBoundVars((ExistsExpr)alternative.Guard, thn); + } + Coverage.Instrument(alternative.Tok, "if-case branch", thn); + TrStmtList(alternative.Body, thn); + } + var wElse = EmitBlock(wr); + EmitAbsurd("unreachable alternative", wElse); + + } else if (stmt is WhileStmt) { + WhileStmt s = (WhileStmt)stmt; + if (s.Body == null) { + return; + } + if (s.Guard == null) { + if (Options.ForbidNondeterminism) { + Error(ErrorId.c_non_deterministic_loop_forbidden, s.Tok, "nondeterministic loop forbidden by the --enforce-determinism option", wr); + } + // This loop is allowed to stop iterating at any time. We choose to never iterate, but we still + // emit a loop structure. The structure "while (false) { }" comes to mind, but that results in + // an "unreachable code" error from Java, so we instead use "while (true) { break; }". + var wBody = CreateWhileLoop(out var guardWriter, wr); + EmitExpr(Expression.CreateBoolLiteral(s.Body.tok, true), false, guardWriter, wStmts); + EmitBreak(null, wBody); + Coverage.UnusedInstrumentationPoint(s.Body.Tok, "while body"); + } else { + var guardWriter = EmitWhile(s.Body.Tok, s.Body.Body, s.Labels, wr); + EmitExpr(s.Guard, false, guardWriter, wStmts); + } + + } else if (stmt is AlternativeLoopStmt loopStmt) { + if (Options.ForbidNondeterminism) { + Error(ErrorId.c_case_based_loop_forbidden, loopStmt.Tok, "case-based loop forbidden by the --enforce-determinism option", wr); + } + if (loopStmt.Alternatives.Count != 0) { + var w = CreateWhileLoop(out var whileGuardWriter, wr); + EmitExpr(Expression.CreateBoolLiteral(loopStmt.tok, true), false, whileGuardWriter, wStmts); + w = EmitContinueLabel(loopStmt.Labels, w); + foreach (var alternative in loopStmt.Alternatives) { + var thn = EmitIf(out var guardWriter, true, w); + EmitExpr(alternative.Guard, false, guardWriter, wStmts); + Coverage.Instrument(alternative.Tok, "while-case branch", thn); + TrStmtList(alternative.Body, thn); + } + var wElse = EmitBlock(w); + { + EmitBreak(null, wElse); + } + } + + } else if (stmt is ForLoopStmt) { + var s = (ForLoopStmt)stmt; + if (s.Body == null) { + return; + } + string endVarName = null; + if (s.End != null) { + // introduce a variable to hold the value of the end-expression + endVarName = ProtectedFreshId(s.GoingUp ? "_hi" : "_lo"); + wStmts = wr.Fork(); + EmitExpr(s.End, false, DeclareLocalVar(endVarName, s.End.Type, s.End.tok, wr), wStmts); + } + var startExprWriter = EmitForStmt(s.Tok, s.LoopIndex, s.GoingUp, endVarName, s.Body.Body, s.Labels, wr); + EmitExpr(s.Start, false, startExprWriter, wStmts); + + } else if (stmt is ForallStmt) { + var s = (ForallStmt)stmt; + if (s.Kind != ForallStmt.BodyKind.Assign) { + // Call and Proof have no side effects, so they can simply be optimized away. + return; + } else if (s.BoundVars.Count == 0) { + // the bound variables just spell out a single point, so the forall statement is equivalent to one execution of the body + TrStmt(s.Body, wr); + return; + } + var s0 = (AssignStmt)s.S0; + if (s0.Rhs is HavocRhs) { + if (Options.ForbidNondeterminism) { + Error(ErrorId.c_nondeterminism_forbidden, s0.Rhs.Tok, "nondeterministic assignment forbidden by --enforce-determinism", wr); + } + // The forall statement says to havoc a bunch of things. This can be efficiently compiled + // into doing nothing. + return; + } + var rhs = ((ExprRhs)s0.Rhs).Expr; + + if (CanSequentializeForall(s.BoundVars, s.Bounds, s.Range, s0.Lhs, rhs)) { + // Just put the statement inside the loops + var wLoop = CompileGuardedLoops(s.BoundVars, s.Bounds, s.Range, wr); + TrStmt(s0, wLoop); + } else { + // Compile: + // forall (w,x,y,z | Range(w,x,y,z)) { + // LHS(w,x,y,z) := RHS(w,x,y,z); + // } + // where w,x,y,z have types seq,set,int,bool and LHS has L-1 top-level subexpressions + // (that is, L denotes the number of top-level subexpressions of LHS plus 1), + // into: + // var ingredients = new List< L-Tuple >(); + // foreach (W w in sq.UniqueElements) { + // foreach (X x in st.Elements) { + // for (BigInteger y = Lo; j < Hi; j++) { + // for (bool z in Helper.AllBooleans) { + // if (Range(w,x,y,z)) { + // ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) )); + // } + // } + // } + // } + // } + // foreach (L-Tuple l in ingredients) { + // LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1); + // } + // + // Note, because the .NET Tuple class only supports up to 8 components, the compiler implementation + // here supports arrays only up to 6 dimensions. This does not seem like a serious practical limitation. + // However, it may be more noticeable if the forall statement supported forall assignments in its + // body. To support cases where tuples would need more than 8 components, .NET Tuple's would have to + // be nested. + + // Temporary names + var c = ProtectedFreshNumericId("_ingredients+_tup"); + string ingredients = "_ingredients" + c; + string tup = "_tup" + c; + + // Compute L + int L; + string tupleTypeArgs; + List tupleTypeArgsList; + if (s0.Lhs is MemberSelectExpr) { + var lhs = (MemberSelectExpr)s0.Lhs; + L = 2; + tupleTypeArgs = TypeArgumentName(lhs.Obj.Type, wr, lhs.tok); + tupleTypeArgsList = new List { lhs.Obj.Type }; + } else if (s0.Lhs is SeqSelectExpr) { + var lhs = (SeqSelectExpr)s0.Lhs; + L = 3; + // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple + tupleTypeArgs = TypeArgumentName(lhs.Seq.Type, wr, lhs.tok) + IntSelect; + tupleTypeArgsList = new List { lhs.Seq.Type, null }; + } else { + var lhs = (MultiSelectExpr)s0.Lhs; + L = 2 + lhs.Indices.Count; + if (8 < L) { + Error(ErrorId.c_no_assignments_to_seven_d_arrays, lhs.tok, "compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements", wr); + return; + } + tupleTypeArgs = TypeArgumentName(lhs.Array.Type, wr, lhs.tok); + tupleTypeArgsList = new List { lhs.Array.Type }; + for (int i = 0; i < lhs.Indices.Count; i++) { + // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple + tupleTypeArgs += IntSelect; + tupleTypeArgsList.Add(null); + } + + } + tupleTypeArgs += "," + TypeArgumentName(rhs.Type, wr, rhs.tok); + tupleTypeArgsList.Add(rhs.Type); + + // declare and construct "ingredients" + var wrOuter = EmitIngredients(wr, ingredients, L, tupleTypeArgs, s, s0, rhs); + + // foreach (L-Tuple l in ingredients) { + // LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1); + // } + TargetTupleSize = L; + wr = CreateForeachIngredientLoop(tup, L, tupleTypeArgs, out var collWriter, wrOuter); + collWriter.Write(ingredients); + { + var wTup = new ConcreteSyntaxTree(wr.RelativeIndentLevel); + var wCoerceTup = EmitCoercionToArbitraryTuple(wTup); + wCoerceTup.Write(tup); + tup = wTup.ToString(); + } + if (s0.Lhs is MemberSelectExpr) { + EmitMemberSelect(s0, tupleTypeArgsList, wr, tup); + } else if (s0.Lhs is SeqSelectExpr) { + EmitSeqSelect(s0, tupleTypeArgsList, wr, tup); + } else { + EmitMultiSelect(s0, tupleTypeArgsList, wr, tup, L); + } + } + } else if (stmt is NestedMatchStmt nestedMatchStmt) { + TrStmt(nestedMatchStmt.Flattened, wr, wStmts); + } else if (stmt is MatchStmt matchStmt) { + EmitMatchStmt(wr, matchStmt); + } else if (stmt is VarDeclStmt) { + var s = (VarDeclStmt)stmt; + var i = 0; + foreach (var local in s.Locals) { + bool hasRhs = s.Update is AssignSuchThatStmt || s.Update is AssignOrReturnStmt; + if (!hasRhs && s.Update is UpdateStmt u) { + if (i < u.Rhss.Count && u.Rhss[i] is HavocRhs) { + // there's no specific initial value + } else { + hasRhs = true; + } + } + TrLocalVar(local, !hasRhs, wr); + i++; + } + if (s.Update != null) { + TrStmt(s.Update, wr); + } + + } else if (stmt is VarDeclPattern) { + var s = (VarDeclPattern)stmt; + if (Contract.Exists(s.LHS.Vars, bv => !bv.IsGhost)) { + TrCasePatternOpt(s.LHS, s.RHS, wr, false); + } + } else if (stmt is ModifyStmt) { + var s = (ModifyStmt)stmt; + if (s.Body != null) { + TrStmt(s.Body, wr); + } else if (Options.ForbidNondeterminism) { + Error(ErrorId.c_bodyless_modify_statement_forbidden, s.Tok, "modify statement without a body forbidden by the --enforce-determinism option", wr); + } + } else if (stmt is TryRecoverStatement h) { + EmitHaltRecoveryStmt(h.TryBody, IdName(h.HaltMessageVar), h.RecoverBody, wr); + } else { + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement + } + } + + private void EmitMatchStmt(ConcreteSyntaxTree wr, MatchStmt s) { + // Type source = e; + // if (source.is_Ctor0) { + // FormalType f0 = ((Dt_Ctor0)source._D).a0; + // ... + // Body0; + // } else if (...) { + // ... + // } else if (true) { + // ... + // } + if (s.Cases.Count != 0) { + string source = ProtectedFreshId("_source"); + DeclareLocalVar(source, s.Source.Type, s.Source.tok, s.Source, false, wr); + + int i = 0; + var sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand(); + foreach (MatchCaseStmt mc in s.Cases) { + var w = MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, wr); + TrStmtList(mc.Body, w); + i++; + } + } + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs similarity index 83% rename from Source/DafnyCore/Backends/SinglePassCodeGenerator.cs rename to Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index d907e655f0..2ca16d4849 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -24,7 +24,7 @@ public static bool CanCompile(this ModuleDefinition module) { } } - public abstract class SinglePassCodeGenerator { + public abstract partial class SinglePassCodeGenerator { // Dafny names cannot start with "_". Hence, if an internal Dafny name is problematic in the target language, // we can prefix it with "_". // However, for backends such as Rust which need special internal fields, we want to clearly @@ -3273,452 +3273,6 @@ void TrStmtNonempty(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wS } } - protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts = null) { - Contract.Requires(stmt != null); - Contract.Requires(wr != null); - - wStmts ??= wr.Fork(); - - if (stmt.IsGhost) { - return; - } - if (stmt is PrintStmt) { - var s = (PrintStmt)stmt; - foreach (var arg in s.Args) { - EmitPrintStmt(wr, arg); - } - } else if (stmt is BreakStmt) { - var s = (BreakStmt)stmt; - var label = s.TargetStmt.Labels.Data.AssignUniqueId(idGenerator); - if (s.IsContinue) { - EmitContinue(label, wr); - } else { - EmitBreak(label, wr); - } - } else if (stmt is ProduceStmt) { - var s = (ProduceStmt)stmt; - var isTailRecursiveResult = false; - if (s.HiddenUpdate != null) { - TrStmt(s.HiddenUpdate, wr); - var ss = s.HiddenUpdate.ResolvedStatements; - if (ss.Count == 1 && ss[0] is AssignStmt assign && assign.Rhs is ExprRhs eRhs && eRhs.Expr.Resolved is FunctionCallExpr fce && IsTailRecursiveByMethodCall(fce)) { - isTailRecursiveResult = true; - } - } - if (s is YieldStmt) { - EmitYield(wr); - } else if (!isTailRecursiveResult) { - EmitReturn(this.enclosingMethod.Outs, wr); - } - } else if (stmt is UpdateStmt) { - var s = (UpdateStmt)stmt; - var resolved = s.ResolvedStatements; - if (resolved.Count == 1) { - TrStmt(resolved[0], wr); - } else { - var assignStmts = resolved.Cast().Where(assignStmt => !assignStmt.IsGhost).ToList(); - var lhss = new List(); - var rhss = new List(); - - // multi-assignment - Contract.Assert(s.Lhss.Count == resolved.Count); - Contract.Assert(s.Rhss.Count == resolved.Count); - var lhsTypes = new List(); - var rhsTypes = new List(); - foreach (var assignStmt in assignStmts) { - var rhs = assignStmt.Rhs; - if (rhs is HavocRhs) { - if (Options.ForbidNondeterminism) { - Error(ErrorId.c_nondeterminism_forbidden, rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr); - } - } else { - var lhs = assignStmt.Lhs; - rhss.Add(rhs); - lhss.Add(lhs); - lhsTypes.Add(lhs.Type); - rhsTypes.Add(TypeOfRhs(rhs)); - } - } - - var wStmtsPre = wStmts.Fork(); - var lvalues = new List(); - foreach (Expression lhs in lhss) { - lvalues.Add(CreateLvalue(lhs, wStmts, wStmtsPre)); - } - - EmitMultiAssignment(lhss, lvalues, lhsTypes, out var wRhss, rhsTypes, wr); - for (int i = 0; i < wRhss.Count; i++) { - TrRhs(rhss[i], wRhss[i], wStmts); - } - } - } else if (stmt is AssignStmt) { - var s = (AssignStmt)stmt; - Contract.Assert(s.Lhs is not SeqSelectExpr expr || expr.SelectOne); // multi-element array assignments are not allowed - if (s.Rhs is HavocRhs) { - if (Options.ForbidNondeterminism) { - Error(ErrorId.c_nondeterminism_forbidden, s.Rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr); - } - } else if (s.Rhs is ExprRhs eRhs && eRhs.Expr.Resolved is FunctionCallExpr fce && IsTailRecursiveByMethodCall(fce)) { - TrTailCallStmt(s.Tok, fce.Function.ByMethodDecl, fce.Receiver, fce.Args, null, wr); - } else { - var lvalue = CreateLvalue(s.Lhs, wr, wStmts); - wStmts = wr.Fork(); - var wRhs = EmitAssignment(lvalue, TypeOfLhs(s.Lhs), TypeOfRhs(s.Rhs), wr, stmt.Tok); - TrRhs(s.Rhs, wRhs, wStmts); - } - - } else if (stmt is AssignSuchThatStmt) { - var s = (AssignSuchThatStmt)stmt; - if (Options.ForbidNondeterminism) { - Error(ErrorId.c_assign_such_that_forbidden, s.Tok, "assign-such-that statement forbidden by the --enforce-determinism option", wr); - } - var lhss = s.Lhss.ConvertAll(lhs => ((IdentifierExpr)lhs.Resolved).Var); // the resolver allows only IdentifierExpr left-hand sides - var missingBounds = BoundedPool.MissingBounds(lhss, s.Bounds, BoundedPool.PoolVirtues.Enumerable); - if (missingBounds.Count != 0) { - foreach (var bv in missingBounds) { - Error(ErrorId.c_assign_such_that_is_too_complex, s.Tok, "this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}'", wr, bv.Name); - } - } else { - Contract.Assert(s.Bounds != null); - TrAssignSuchThat(lhss, s.Expr, s.Bounds, s.Tok.line, wr, false); - } - } else if (stmt is AssignOrReturnStmt) { - var s = (AssignOrReturnStmt)stmt; - // TODO there's potential here to use target-language specific features such as exceptions - // to make it more target-language idiomatic and improve performance - TrStmtList(s.ResolvedStatements, wr); - - } else if (stmt is ExpectStmt) { - var s = (ExpectStmt)stmt; - // TODO there's potential here to use target-language specific features such as exceptions - // to make it more target-language idiomatic and improve performance - ConcreteSyntaxTree bodyWriter = EmitIf(out var guardWriter, false, wr); - var negated = new UnaryOpExpr(s.Tok, UnaryOpExpr.Opcode.Not, s.Expr); - negated.Type = Type.Bool; - EmitExpr(negated, false, guardWriter, wStmts); - EmitHalt(s.Tok, s.Message, bodyWriter); - - } else if (stmt is CallStmt) { - var s = (CallStmt)stmt; - var wrBefore = wr.Fork(); - var wrCall = wr.Fork(); - var wrAfter = wr; - TrCallStmt(s, null, wrCall, wrBefore, wrAfter); - - } else if (stmt is BlockStmt) { - var w = EmitBlock(wr); - TrStmtList(((BlockStmt)stmt).Body, w); - - } else if (stmt is IfStmt) { - IfStmt s = (IfStmt)stmt; - if (s.Guard == null) { - if (Options.ForbidNondeterminism) { - Error(ErrorId.c_nondeterministic_if_forbidden, s.Tok, "nondeterministic if statement forbidden by the --enforce-determinism option", wr); - } - // we can compile the branch of our choice - ConcreteSyntaxTree guardWriter; - if (s.Els == null) { - // let's compile the "else" branch, since that involves no work - // (still, let's leave a marker in the source code to indicate that this is what we did) - Coverage.UnusedInstrumentationPoint(s.Thn.Tok, "then branch"); - var notFalse = (UnaryOpExpr)Expression.CreateNot(s.Thn.Tok, Expression.CreateBoolLiteral(s.Thn.Tok, false)); - var thenWriter = EmitIf(out guardWriter, false, wr); - EmitUnaryExpr(ResolvedUnaryOp.BoolNot, notFalse.E, false, guardWriter, wStmts); - Coverage.Instrument(s.Tok, "implicit else branch", wr); - thenWriter = EmitIf(out guardWriter, false, thenWriter); - EmitUnaryExpr(ResolvedUnaryOp.BoolNot, notFalse.E, false, guardWriter, wStmts); - TrStmtList(new List(), thenWriter); - } else { - // let's compile the "then" branch - wr = EmitIf(out guardWriter, false, wr); - EmitExpr(Expression.CreateBoolLiteral(s.Thn.tok, true), false, guardWriter, wStmts); - Coverage.Instrument(s.Thn.Tok, "then branch", wr); - TrStmtList(s.Thn.Body, wr); - Coverage.UnusedInstrumentationPoint(s.Els.Tok, "else branch"); - } - } else { - if (s.IsBindingGuard && Options.ForbidNondeterminism) { - Error(ErrorId.c_binding_if_forbidden, s.Tok, "binding if statement forbidden by the --enforce-determinism option", wr); - } - - var coverageForElse = Coverage.IsRecording && !(s.Els is IfStmt); - var thenWriter = EmitIf(out var guardWriter, s.Els != null || coverageForElse, wr); - EmitExpr(s.IsBindingGuard ? ((ExistsExpr)s.Guard).AlphaRename("eg_d") : s.Guard, false, guardWriter, wStmts); - // We'd like to do "TrStmt(s.Thn, indent)", except we want the scope of any existential variables to come inside the block - if (s.IsBindingGuard) { - IntroduceAndAssignBoundVars((ExistsExpr)s.Guard, thenWriter); - } - Coverage.Instrument(s.Thn.Tok, "then branch", thenWriter); - TrStmtList(s.Thn.Body, thenWriter); - - if (coverageForElse) { - wr = EmitBlock(wr); - if (s.Els == null) { - Coverage.Instrument(s.Tok, "implicit else branch", wr); - } else { - Coverage.Instrument(s.Els.Tok, "else branch", wr); - } - } - if (s.Els != null) { - TrStmtNonempty(s.Els, wr, wStmts); - } - } - - } else if (stmt is AlternativeStmt) { - var s = (AlternativeStmt)stmt; - if (Options.ForbidNondeterminism && 2 <= s.Alternatives.Count) { - Error(ErrorId.c_case_based_if_forbidden, s.Tok, "case-based if statement forbidden by the --enforce-determinism option", wr); - } - foreach (var alternative in s.Alternatives) { - var thn = EmitIf(out var guardWriter, true, wr); - EmitExpr(alternative.IsBindingGuard ? ((ExistsExpr)alternative.Guard).AlphaRename("eg_d") : alternative.Guard, false, guardWriter, wStmts); - if (alternative.IsBindingGuard) { - IntroduceAndAssignBoundVars((ExistsExpr)alternative.Guard, thn); - } - Coverage.Instrument(alternative.Tok, "if-case branch", thn); - TrStmtList(alternative.Body, thn); - } - var wElse = EmitBlock(wr); - EmitAbsurd("unreachable alternative", wElse); - - } else if (stmt is WhileStmt) { - WhileStmt s = (WhileStmt)stmt; - if (s.Body == null) { - return; - } - if (s.Guard == null) { - if (Options.ForbidNondeterminism) { - Error(ErrorId.c_non_deterministic_loop_forbidden, s.Tok, "nondeterministic loop forbidden by the --enforce-determinism option", wr); - } - // This loop is allowed to stop iterating at any time. We choose to never iterate, but we still - // emit a loop structure. The structure "while (false) { }" comes to mind, but that results in - // an "unreachable code" error from Java, so we instead use "while (true) { break; }". - var wBody = CreateWhileLoop(out var guardWriter, wr); - EmitExpr(Expression.CreateBoolLiteral(s.Body.tok, true), false, guardWriter, wStmts); - EmitBreak(null, wBody); - Coverage.UnusedInstrumentationPoint(s.Body.Tok, "while body"); - } else { - var guardWriter = EmitWhile(s.Body.Tok, s.Body.Body, s.Labels, wr); - EmitExpr(s.Guard, false, guardWriter, wStmts); - } - - } else if (stmt is AlternativeLoopStmt loopStmt) { - if (Options.ForbidNondeterminism) { - Error(ErrorId.c_case_based_loop_forbidden, loopStmt.Tok, "case-based loop forbidden by the --enforce-determinism option", wr); - } - if (loopStmt.Alternatives.Count != 0) { - var w = CreateWhileLoop(out var whileGuardWriter, wr); - EmitExpr(Expression.CreateBoolLiteral(loopStmt.tok, true), false, whileGuardWriter, wStmts); - w = EmitContinueLabel(loopStmt.Labels, w); - foreach (var alternative in loopStmt.Alternatives) { - var thn = EmitIf(out var guardWriter, true, w); - EmitExpr(alternative.Guard, false, guardWriter, wStmts); - Coverage.Instrument(alternative.Tok, "while-case branch", thn); - TrStmtList(alternative.Body, thn); - } - var wElse = EmitBlock(w); - { - EmitBreak(null, wElse); - } - } - - } else if (stmt is ForLoopStmt) { - var s = (ForLoopStmt)stmt; - if (s.Body == null) { - return; - } - string endVarName = null; - if (s.End != null) { - // introduce a variable to hold the value of the end-expression - endVarName = ProtectedFreshId(s.GoingUp ? "_hi" : "_lo"); - wStmts = wr.Fork(); - EmitExpr(s.End, false, DeclareLocalVar(endVarName, s.End.Type, s.End.tok, wr), wStmts); - } - var startExprWriter = EmitForStmt(s.Tok, s.LoopIndex, s.GoingUp, endVarName, s.Body.Body, s.Labels, wr); - EmitExpr(s.Start, false, startExprWriter, wStmts); - - } else if (stmt is ForallStmt) { - var s = (ForallStmt)stmt; - if (s.Kind != ForallStmt.BodyKind.Assign) { - // Call and Proof have no side effects, so they can simply be optimized away. - return; - } else if (s.BoundVars.Count == 0) { - // the bound variables just spell out a single point, so the forall statement is equivalent to one execution of the body - TrStmt(s.Body, wr); - return; - } - var s0 = (AssignStmt)s.S0; - if (s0.Rhs is HavocRhs) { - if (Options.ForbidNondeterminism) { - Error(ErrorId.c_nondeterminism_forbidden, s0.Rhs.Tok, "nondeterministic assignment forbidden by --enforce-determinism", wr); - } - // The forall statement says to havoc a bunch of things. This can be efficiently compiled - // into doing nothing. - return; - } - var rhs = ((ExprRhs)s0.Rhs).Expr; - - if (CanSequentializeForall(s.BoundVars, s.Bounds, s.Range, s0.Lhs, rhs)) { - // Just put the statement inside the loops - var wLoop = CompileGuardedLoops(s.BoundVars, s.Bounds, s.Range, wr); - TrStmt(s0, wLoop); - } else { - // Compile: - // forall (w,x,y,z | Range(w,x,y,z)) { - // LHS(w,x,y,z) := RHS(w,x,y,z); - // } - // where w,x,y,z have types seq,set,int,bool and LHS has L-1 top-level subexpressions - // (that is, L denotes the number of top-level subexpressions of LHS plus 1), - // into: - // var ingredients = new List< L-Tuple >(); - // foreach (W w in sq.UniqueElements) { - // foreach (X x in st.Elements) { - // for (BigInteger y = Lo; j < Hi; j++) { - // for (bool z in Helper.AllBooleans) { - // if (Range(w,x,y,z)) { - // ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) )); - // } - // } - // } - // } - // } - // foreach (L-Tuple l in ingredients) { - // LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1); - // } - // - // Note, because the .NET Tuple class only supports up to 8 components, the compiler implementation - // here supports arrays only up to 6 dimensions. This does not seem like a serious practical limitation. - // However, it may be more noticeable if the forall statement supported forall assignments in its - // body. To support cases where tuples would need more than 8 components, .NET Tuple's would have to - // be nested. - - // Temporary names - var c = ProtectedFreshNumericId("_ingredients+_tup"); - string ingredients = "_ingredients" + c; - string tup = "_tup" + c; - - // Compute L - int L; - string tupleTypeArgs; - List tupleTypeArgsList; - if (s0.Lhs is MemberSelectExpr) { - var lhs = (MemberSelectExpr)s0.Lhs; - L = 2; - tupleTypeArgs = TypeArgumentName(lhs.Obj.Type, wr, lhs.tok); - tupleTypeArgsList = new List { lhs.Obj.Type }; - } else if (s0.Lhs is SeqSelectExpr) { - var lhs = (SeqSelectExpr)s0.Lhs; - L = 3; - // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple - tupleTypeArgs = TypeArgumentName(lhs.Seq.Type, wr, lhs.tok) + IntSelect; - tupleTypeArgsList = new List { lhs.Seq.Type, null }; - } else { - var lhs = (MultiSelectExpr)s0.Lhs; - L = 2 + lhs.Indices.Count; - if (8 < L) { - Error(ErrorId.c_no_assignments_to_seven_d_arrays, lhs.tok, "compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements", wr); - return; - } - tupleTypeArgs = TypeArgumentName(lhs.Array.Type, wr, lhs.tok); - tupleTypeArgsList = new List { lhs.Array.Type }; - for (int i = 0; i < lhs.Indices.Count; i++) { - // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple - tupleTypeArgs += IntSelect; - tupleTypeArgsList.Add(null); - } - - } - tupleTypeArgs += "," + TypeArgumentName(rhs.Type, wr, rhs.tok); - tupleTypeArgsList.Add(rhs.Type); - - // declare and construct "ingredients" - var wrOuter = EmitIngredients(wr, ingredients, L, tupleTypeArgs, s, s0, rhs); - - // foreach (L-Tuple l in ingredients) { - // LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1); - // } - TargetTupleSize = L; - wr = CreateForeachIngredientLoop(tup, L, tupleTypeArgs, out var collWriter, wrOuter); - collWriter.Write(ingredients); - { - var wTup = new ConcreteSyntaxTree(wr.RelativeIndentLevel); - var wCoerceTup = EmitCoercionToArbitraryTuple(wTup); - wCoerceTup.Write(tup); - tup = wTup.ToString(); - } - if (s0.Lhs is MemberSelectExpr) { - EmitMemberSelect(s0, tupleTypeArgsList, wr, tup); - } else if (s0.Lhs is SeqSelectExpr) { - EmitSeqSelect(s0, tupleTypeArgsList, wr, tup); - } else { - EmitMultiSelect(s0, tupleTypeArgsList, wr, tup, L); - } - } - } else if (stmt is NestedMatchStmt nestedMatchStmt) { - TrStmt(nestedMatchStmt.Flattened, wr, wStmts); - } else if (stmt is MatchStmt) { - MatchStmt s = (MatchStmt)stmt; - // Type source = e; - // if (source.is_Ctor0) { - // FormalType f0 = ((Dt_Ctor0)source._D).a0; - // ... - // Body0; - // } else if (...) { - // ... - // } else if (true) { - // ... - // } - if (s.Cases.Count != 0) { - string source = ProtectedFreshId("_source"); - DeclareLocalVar(source, s.Source.Type, s.Source.tok, s.Source, false, wr); - - int i = 0; - var sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand(); - foreach (MatchCaseStmt mc in s.Cases) { - var w = MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, wr); - TrStmtList(mc.Body, w); - i++; - } - } - - } else if (stmt is VarDeclStmt) { - var s = (VarDeclStmt)stmt; - var i = 0; - foreach (var local in s.Locals) { - bool hasRhs = s.Update is AssignSuchThatStmt || s.Update is AssignOrReturnStmt; - if (!hasRhs && s.Update is UpdateStmt u) { - if (i < u.Rhss.Count && u.Rhss[i] is HavocRhs) { - // there's no specific initial value - } else { - hasRhs = true; - } - } - TrLocalVar(local, !hasRhs, wr); - i++; - } - if (s.Update != null) { - TrStmt(s.Update, wr); - } - - } else if (stmt is VarDeclPattern) { - var s = (VarDeclPattern)stmt; - if (Contract.Exists(s.LHS.Vars, bv => !bv.IsGhost)) { - TrCasePatternOpt(s.LHS, s.RHS, wr, false); - } - } else if (stmt is ModifyStmt) { - var s = (ModifyStmt)stmt; - if (s.Body != null) { - TrStmt(s.Body, wr); - } else if (Options.ForbidNondeterminism) { - Error(ErrorId.c_bodyless_modify_statement_forbidden, s.Tok, "modify statement without a body forbidden by the --enforce-determinism option", wr); - } - } else if (stmt is TryRecoverStatement h) { - EmitHaltRecoveryStmt(h.TryBody, IdName(h.HaltMessageVar), h.RecoverBody, wr); - } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement - } - } - protected virtual ConcreteSyntaxTree EmitIngredients(ConcreteSyntaxTree wr, string ingredients, int L, string tupleTypeArgs, ForallStmt s, AssignStmt s0, Expression rhs) { var wStmts = wr.Fork(); var wrVarInit = DeclareLocalVar(ingredients, null, null, wr); @@ -5202,594 +4756,6 @@ public virtual ConcreteSyntaxTree Expr(Expression expr, bool inLetExprBody, Conc return result; } - public virtual void EmitExpr(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - if (expr is LiteralExpr) { - LiteralExpr e = (LiteralExpr)expr; - EmitLiteralExpr(wr, e); - - } else if (expr is ThisExpr) { - if (thisContext != null) { - var instantiatedType = expr.Type.Subst(thisContext.ParentFormalTypeParametersToActuals); - var contextType = UserDefinedType.FromTopLevelDecl(expr.tok, thisContext); - if (contextType.ResolvedClass is ClassLikeDecl { NonNullTypeDecl: { } } cls) { - contextType = UserDefinedType.FromTopLevelDecl(expr.tok, cls.NonNullTypeDecl); - } - - wr = EmitCoercionIfNecessary(contextType, instantiatedType, expr.tok, wr); - } - EmitThis(wr); - - } else if (expr is IdentifierExpr) { - var e = (IdentifierExpr)expr; - if (inLetExprBody && !(e.Var is BoundVar)) { - // copy variable to a temp since - // - C# doesn't allow out param in letExpr body, and - // - Java doesn't allow any non-final variable in letExpr body. - var name = ProtectedFreshId("_pat_let_tv"); - EmitIdentifier(name, wr); - DeclareLocalVar(name, null, null, false, IdName(e.Var), copyInstrWriters.Peek(), e.Type); - } else { - EmitIdentifier(IdName(e.Var), wr); - } - } else if (expr is SetDisplayExpr) { - var e = (SetDisplayExpr)expr; - EmitCollectionDisplay(e.Type.NormalizeToAncestorType().AsSetType, e.tok, e.Elements, inLetExprBody, wr, wStmts); - - } else if (expr is MultiSetDisplayExpr) { - var e = (MultiSetDisplayExpr)expr; - EmitCollectionDisplay(e.Type.NormalizeToAncestorType().AsMultiSetType, e.tok, e.Elements, inLetExprBody, wr, wStmts); - - } else if (expr is SeqDisplayExpr) { - var e = (SeqDisplayExpr)expr; - EmitCollectionDisplay(e.Type.NormalizeToAncestorType().AsSeqType, e.tok, e.Elements, inLetExprBody, wr, wStmts); - - } else if (expr is MapDisplayExpr) { - var e = (MapDisplayExpr)expr; - EmitMapDisplay(e.Type.NormalizeToAncestorType().AsMapType, e.tok, e.Elements, inLetExprBody, wr, wStmts); - - } else if (expr is MemberSelectExpr) { - MemberSelectExpr e = (MemberSelectExpr)expr; - SpecialField sf = e.Member as SpecialField; - if (sf != null) { - GetSpecialFieldInfo(sf.SpecialId, sf.IdParam, e.Obj.Type, out var compiledName, out var preStr, out var postStr); - wr.Write(preStr); - - if (sf.IsStatic && !SupportsStaticsInGenericClasses && sf.EnclosingClass.TypeArgs.Count != 0) { - var typeArgs = e.TypeApplication_AtEnclosingClass; - Contract.Assert(typeArgs.Count == sf.EnclosingClass.TypeArgs.Count); - wr.Write("{0}.", TypeName_Companion(e.Obj.Type, wr, e.tok, sf)); - EmitNameAndActualTypeArgs(IdName(e.Member), typeArgs, e.tok, null, false, wr); - var tas = TypeArgumentInstantiation.ListFromClass(sf.EnclosingClass, typeArgs); - EmitTypeDescriptorsActuals(tas, e.tok, wr.ForkInParens()); - } else { - void writeObj(ConcreteSyntaxTree w) { - //Contract.Assert(!sf.IsStatic); - w = EmitCoercionIfNecessary(e.Obj.Type, UserDefinedType.UpcastToMemberEnclosingType(e.Obj.Type, e.Member), e.tok, w); - TrParenExpr(e.Obj, w, inLetExprBody, wStmts); - } - - var typeArgs = CombineAllTypeArguments(e.Member, e.TypeApplication_AtEnclosingClass, e.TypeApplication_JustMember); - EmitMemberSelect(writeObj, e.Obj.Type, e.Member, typeArgs, e.TypeArgumentSubstitutionsWithParents(), expr.Type).EmitRead(wr); - } - - wr.Write(postStr); - } else { - var typeArgs = CombineAllTypeArguments(e.Member, e.TypeApplication_AtEnclosingClass, e.TypeApplication_JustMember); - var typeMap = e.TypeArgumentSubstitutionsWithParents(); - var customReceiver = NeedsCustomReceiverNotTrait(e.Member); - if (!customReceiver && !e.Member.IsStatic) { - Action obj; - // The eta conversion here is to avoid capture of the receiver, because the call to EmitMemberSelect below may generate - // a lambda expression in the target language. - if (e.Member is Function && typeArgs.Count != 0) { - // need to eta-expand wrap the receiver - var etaReceiver = ProtectedFreshId("_eta_this"); - wr = CreateIIFE_ExprBody(etaReceiver, e.Obj.Type, e.Obj.tok, e.Obj, inLetExprBody, e.Type.Subst(typeMap), e.tok, wr, ref wStmts); - obj = w => EmitIdentifier(etaReceiver, w); - } else { - obj = w => EmitExpr(e.Obj, inLetExprBody, w, wStmts); - } - EmitMemberSelect(obj, e.Obj.Type, e.Member, typeArgs, typeMap, expr.Type).EmitRead(wr); - } else { - string customReceiverName = null; - if (customReceiver && e.Member is Function) { - // need to eta-expand wrap the receiver - customReceiverName = ProtectedFreshId("_eta_this"); - wr = CreateIIFE_ExprBody(customReceiverName, e.Obj.Type, e.Obj.tok, e.Obj, inLetExprBody, e.Type.Subst(typeMap), e.tok, wr, ref wStmts); - } - Action obj = w => EmitTypeName_Companion(e.Obj.Type, w, wr, e.tok, e.Member); - EmitMemberSelect(obj, e.Obj.Type, e.Member, typeArgs, typeMap, expr.Type, customReceiverName).EmitRead(wr); - } - } - } else if (expr is SeqSelectExpr) { - SeqSelectExpr e = (SeqSelectExpr)expr; - Contract.Assert(e.Seq.Type != null); - if (e.Seq.Type.IsArrayType) { - if (e.SelectOne) { - Contract.Assert(e.E0 != null && e.E1 == null); - var w = EmitArraySelect(new List() { e.E0 }, e.Type, inLetExprBody, wr, wStmts); - w = EmitCoercionIfNecessary( - e.Seq.Type, - e.Seq.Type.IsNonNullRefType || !e.Seq.Type.IsRefType ? null : UserDefinedType.CreateNonNullType((UserDefinedType)e.Seq.Type.NormalizeExpand()), - e.tok, - w - ); - TrParenExpr(e.Seq, w, inLetExprBody, wStmts); - } else { - EmitSeqSelectRange(e.Seq, e.E0, e.E1, true, inLetExprBody, wr, wStmts); - } - } else if (e.SelectOne) { - Contract.Assert(e.E0 != null && e.E1 == null); - EmitIndexCollectionSelect(e.Seq, e.E0, inLetExprBody, wr, wStmts); - } else { - EmitSeqSelectRange(e.Seq, e.E0, e.E1, false, inLetExprBody, wr, wStmts); - } - } else if (expr is SeqConstructionExpr) { - var e = (SeqConstructionExpr)expr; - EmitSeqConstructionExpr(e, inLetExprBody, wr, wStmts); - } else if (expr is MultiSetFormingExpr) { - var e = (MultiSetFormingExpr)expr; - EmitMultiSetFormingExpr(e, inLetExprBody, wr, wStmts); - } else if (expr is MultiSelectExpr) { - MultiSelectExpr e = (MultiSelectExpr)expr; - WriteCast(TypeName(e.Type.NormalizeExpand(), wr, e.tok), wr); - var w = EmitArraySelect(e.Indices, e.Type, inLetExprBody, wr, wStmts); - TrParenExpr(e.Array, w, inLetExprBody, wStmts); - - } else if (expr is SeqUpdateExpr) { - SeqUpdateExpr e = (SeqUpdateExpr)expr; - var collectionType = e.Type.NormalizeToAncestorType().AsCollectionType; - Contract.Assert(collectionType != null); - EmitIndexCollectionUpdate(e.Seq, e.Index, e.Value, collectionType, inLetExprBody, wr, wStmts); - } else if (expr is DatatypeUpdateExpr) { - var e = (DatatypeUpdateExpr)expr; - if (e.Members.All(member => member.IsGhost)) { - // all fields to be updated are ghost, which doesn't change the value - EmitExpr(e.Root, inLetExprBody, wr, wStmts); - return; - } - if (DatatypeWrapperEraser.IsErasableDatatypeWrapper(Options, e.Root.Type.AsDatatype, out var dtor)) { - var i = e.Members.IndexOf(dtor); - if (0 <= i) { - // the datatype is an erasable wrapper and its core destructor is part of the update (which implies everything else must be a ghost), - // so proceed as with the rhs - Contract.Assert(Enumerable.Range(0, e.Members.Count).All(j => j == i || e.Members[j].IsGhost)); - Contract.Assert(e.Members.Count == e.Updates.Count); - var rhs = e.Updates[i].Item3; - EmitExpr(rhs, inLetExprBody, wr, wStmts); - return; - } - } - // the optimized cases don't apply, so proceed according to the desugaring - EmitExpr(e.ResolvedExpression, inLetExprBody, wr, wStmts); - } else if (expr is FunctionCallExpr) { - FunctionCallExpr e = (FunctionCallExpr)expr; - - void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyntaxTree wStmts2) { - this.EmitExpr(e2, inLetExpr, wr2, wStmts2); - } - - if (e.Function is SpecialFunction) { - CompileSpecialFunctionCallExpr(e, wr, inLetExprBody, wStmts, EmitExpr); - } else { - CompileFunctionCallExpr(e, wr, inLetExprBody, wStmts, EmitExpr); - } - - } else if (expr is ApplyExpr) { - var e = expr as ApplyExpr; - EmitApplyExpr(e.Function.Type, e.tok, e.Function, e.Args, inLetExprBody, wr, wStmts); - - } else if (expr is DatatypeValue) { - var dtv = (DatatypeValue)expr; - Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved - - if (DatatypeWrapperEraser.IsErasableDatatypeWrapper(Options, dtv.Ctor.EnclosingDatatype, out var dtor)) { - var i = dtv.Ctor.Destructors.IndexOf(dtor); - Contract.Assert(0 <= i); - EmitExpr(dtv.Arguments[i], inLetExprBody, wr, wStmts); - return; - } - - var wrArgumentList = new ConcreteSyntaxTree(); - var wTypeDescriptorArguments = new ConcreteSyntaxTree(); - var typeSubst = TypeParameter.SubstitutionMap(dtv.Ctor.EnclosingDatatype.TypeArgs, dtv.InferredTypeArgs); - string sep = ""; - Contract.Assert(dtv.Ctor.EnclosingDatatype.TypeArgs.Count == dtv.InferredTypeArgs.Count); - WriteTypeDescriptors(dtv.Ctor.EnclosingDatatype, dtv.InferredTypeArgs, wTypeDescriptorArguments, ref sep); - sep = ""; - for (var i = 0; i < dtv.Arguments.Count; i++) { - var formal = dtv.Ctor.Formals[i]; - if (!formal.IsGhost) { - wrArgumentList.Write(sep); - var w = EmitCoercionIfNecessary(@from: dtv.Arguments[i].Type, to: dtv.Ctor.Formals[i].Type.Subst(typeSubst), toOrig: dtv.Ctor.Formals[i].Type, tok: dtv.tok, wr: wrArgumentList); - EmitExpr(dtv.Arguments[i], inLetExprBody, w, wStmts); - sep = ", "; - } - } - EmitDatatypeValue(dtv, wTypeDescriptorArguments.ToString(), wrArgumentList.ToString(), wr); - - } else if (expr is OldExpr) { - Contract.Assert(false); throw new cce.UnreachableException(); // 'old' is always a ghost - - } else if (expr is UnaryOpExpr) { - var e = (UnaryOpExpr)expr; - if (e.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BVNot) { - wr = EmitBitvectorTruncation(e.Type.NormalizeToAncestorType().AsBitVectorType, e.Type.AsNativeType(), true, wr); - } - EmitUnaryExpr(UnaryOpCodeMap[e.ResolvedOp], e.E, inLetExprBody, wr, wStmts); - } else if (expr is ConversionExpr) { - var e = (ConversionExpr)expr; - var fromType = e.E.Type.GetRuntimeType(); - var toType = e.ToType.GetRuntimeType(); - Contract.Assert(Options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy || toType.IsRefType == fromType.IsRefType); - if (toType.IsRefType || toType.IsTraitType || fromType.IsTraitType) { - var w = EmitCoercionIfNecessary(e.E.Type, e.ToType, e.tok, wr); - w = EmitDowncastIfNecessary(e.E.Type, e.ToType, e.tok, w); - EmitExpr(e.E, inLetExprBody, w, wStmts); - } else { - EmitConversionExpr(e.E, fromType, toType, inLetExprBody, wr, wStmts); - } - - } else if (expr is TypeTestExpr typeTestExpr) { - CompileTypeTest(typeTestExpr, inLetExprBody, wr, ref wStmts); - - } else if (expr is BinaryExpr) { - var e = (BinaryExpr)expr; - - if (IsComparisonToZero(e, out var arg, out var sign, out var negated) && - CompareZeroUsingSign(arg.Type)) { - // Transform e.g. x < BigInteger.Zero into x.Sign == -1 - var w = EmitSign(arg.Type, wr); - TrParenExpr(arg, w, inLetExprBody, wStmts); - wr.Write(negated ? " != " : " == "); - wr.Write(sign.ToString()); - } else { - CompileBinOp(e.ResolvedOp, e.E0, e.E1, e.tok, expr.Type.GetRuntimeType(), - out var opString, - out var preOpString, - out var postOpString, - out var callString, - out var staticCallString, - out var reverseArguments, - out var truncateResult, - out var convertE1_to_int, - out var coerceE1, - wr); - - if (truncateResult && e.Type.NormalizeToAncestorType().AsBitVectorType is { } bitvectorType) { - wr = EmitBitvectorTruncation(bitvectorType, e.Type.AsNativeType(), true, wr); - } - var e0 = reverseArguments ? e.E1 : e.E0; - var e1 = reverseArguments ? e.E0 : e.E1; - - var left = Expr(e0, inLetExprBody, wStmts); - ConcreteSyntaxTree right; - if (convertE1_to_int) { - right = ExprAsNativeInt(e1, inLetExprBody, wStmts); - } else { - right = Expr(e1, inLetExprBody, wStmts); - if (coerceE1) { - right = CoercionIfNecessary(e1.Type, TypeForCoercion(e1.Type), e1.tok, right); - } - } - - wr.Write(preOpString); - if (opString != null) { - var nativeType = AsNativeType(e.Type); - string nativeName = null; - bool needsCast = false; - if (nativeType != null) { - GetNativeInfo(nativeType.Sel, out nativeName, out _, out needsCast); - } - - var opResult = ConcreteSyntaxTree.Create($"{left.InParens()} {opString} {right.InParens()}"); - if (needsCast) { - opResult = Cast(new LineSegment(nativeName), opResult); - } - - wr.Append(opResult); - } else if (callString != null) { - wr.Format($"{left.InParens()}.{callString}({right})"); - } else if (staticCallString != null) { - wr.Format($"{staticCallString}({left}, {right})"); - } - wr.Write(postOpString); - } - } else if (expr is TernaryExpr) { - Contract.Assume(false); // currently, none of the ternary expressions is compilable - - } else if (expr is LetExpr) { - var e = (LetExpr)expr; - if (e.Exact) { - // The Dafny "let" expression - // var Pattern(x,y) := G; E - // is translated into C# as: - // LamLet(G, tmp => - // LamLet(dtorX(tmp), x => - // LamLet(dtorY(tmp), y => E))) - Contract.Assert(e.LHSs.Count == e.RHSs.Count); // checked by resolution - var w = wr; - for (int i = 0; i < e.LHSs.Count; i++) { - var lhs = e.LHSs[i]; - if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) { - var rhsName = $"_pat_let{GetUniqueAstNumber(e)}_{i}"; - w = CreateIIFE_ExprBody(rhsName, e.RHSs[i].Type, e.RHSs[i].tok, e.RHSs[i], inLetExprBody, e.Body.Type, e.Body.tok, w, ref wStmts); - w = TrCasePattern(lhs, wr => EmitIdentifier(rhsName, wr), e.RHSs[i].Type, e.Body.Type, w, ref wStmts); - } - } - EmitExpr(e.Body, true, w, wStmts); - } else if (e.BoundVars.All(bv => bv.IsGhost)) { - // The Dafny "let" expression - // ghost var x,y :| Constraint; E - // is compiled just like E is, because the resolver has already checked that x,y (or other ghost variables, for that matter) don't - // occur in E (moreover, the verifier has checked that values for x,y satisfying Constraint exist). - EmitExpr(e.Body, inLetExprBody, wr, wStmts); - } else { - // The Dafny "let" expression - // var x,y :| Constraint; E - // is translated into C# as: - // LamLet(0, dummy => { // the only purpose of this construction here is to allow us to add some code inside an expression in C# - // var x,y; - // // Embark on computation that fills in x,y according to Constraint; the computation stops when the first - // // such value is found, but since the verifier checks that x,y follows uniquely from Constraint, this is - // // not a source of nondeterminancy. - // return E; - // }) - Contract.Assert(e.RHSs.Count == 1); // checked by resolution - var missingBounds = BoolBoundedPool.MissingBounds(e.BoundVars.ToList(), e.Constraint_Bounds, BoundedPool.PoolVirtues.Enumerable); - if (missingBounds.Count != 0) { - foreach (var bv in missingBounds) { - Error(ErrorId.c_let_such_that_is_too_complex, e.tok, "this let-such-that expression is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}'", wr, bv.Name); - } - } else { - var w = CreateIIFE1(0, e.Body.Type, e.Body.tok, "_let_dummy_" + GetUniqueAstNumber(e), wr, wStmts); - foreach (var bv in e.BoundVars) { - DeclareLocalVar(IdName(bv), bv.Type, bv.tok, false, ForcePlaceboValue(bv.Type, wr, bv.tok, true), w); - } - TrAssignSuchThat(new List(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0], e.Constraint_Bounds, e.tok.line, w, inLetExprBody); - EmitReturnExpr(e.Body, e.Body.Type, true, w); - } - } - } else if (expr is NestedMatchExpr nestedMatchExpr) { - EmitExpr(nestedMatchExpr.Flattened, inLetExprBody, wr, wStmts); - } else if (expr is MatchExpr) { - var e = (MatchExpr)expr; - // ((System.Func)((SourceType _source) => { - // if (source.is_Ctor0) { - // FormalType f0 = ((Dt_Ctor0)source._D).a0; - // ... - // return Body0; - // } else if (...) { - // ... - // } else if (true) { - // ... - // } - // }))(src) - - EmitLambdaApply(wr, out var wLambda, out var wArg); - - string source = ProtectedFreshId("_source"); - ConcreteSyntaxTree w; - w = CreateLambda(new List() { e.Source.Type }, e.tok, new List() { source }, e.Type, wLambda, wStmts); - - if (e.Cases.Count == 0) { - // the verifier would have proved we never get here; still, we need some code that will compile - EmitAbsurd(null, w); - } else { - int i = 0; - var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand(); - foreach (MatchCaseExpr mc in e.Cases) { - var wCase = MatchCasePrelude(source, sourceType, mc.Ctor, mc.Arguments, i, e.Cases.Count, w); - TrExprOpt(mc.Body, mc.Body.Type, wCase, wStmts, inLetExprBody: true, accumulatorVar: null); - i++; - } - } - // We end with applying the source expression to the delegate we just built - EmitExpr(e.Source, inLetExprBody, wArg, wStmts); - - } else if (expr is QuantifierExpr) { - var e = (QuantifierExpr)expr; - - // Compilation does not check whether a quantifier was split. - - wr = CaptureFreeVariables(expr, true, out var su, inLetExprBody, wr, ref wStmts); - var logicalBody = su.Substitute(e.LogicalBody(true)); - - Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds - var n = e.BoundVars.Count; - Contract.Assert(e.Bounds.Count == n); - var wBody = wr; - for (int i = 0; i < n; i++) { - var bound = e.Bounds[i]; - var bv = e.BoundVars[i]; - - var collectionElementType = CompileCollection(bound, bv, inLetExprBody, false, su, out var collection, wStmts, e.Bounds, e.BoundVars, i); - wBody = EmitQuantifierExpr(collection, expr is ForallExpr, collectionElementType, bv, wBody); - var native = AsNativeType(e.BoundVars[i].Type); - var tmpVarName = ProtectedFreshId(e is ForallExpr ? "_forall_var_" : "_exists_var_"); - ConcreteSyntaxTree newWBody = CreateLambda(new List { collectionElementType }, e.tok, new List { tmpVarName }, Type.Bool, wBody, wStmts, untyped: true); - wStmts = newWBody.Fork(); - newWBody = MaybeInjectSubtypeConstraintWrtTraits( - tmpVarName, collectionElementType, bv.Type, - inLetExprBody, e.tok, newWBody, true, e is ForallExpr); - EmitDowncastVariableAssignment( - IdName(bv), bv.Type, tmpVarName, collectionElementType, true, e.tok, newWBody); - newWBody = MaybeInjectSubsetConstraint( - bv, bv.Type, inLetExprBody, e.tok, newWBody, isReturning: true, elseReturnValue: e is ForallExpr); - wBody = newWBody; - } - EmitExpr(logicalBody, inLetExprBody, wBody, wStmts); - - } else if (expr is SetComprehension) { - var e = (SetComprehension)expr; - // For "set i,j,k,l | R(i,j,k,l) :: Term(i,j,k,l)" where the term has type "G", emit something like: - // ((System.Func>)(() => { - // var _coll = new List(); - // foreach (var tmp_l in sq.Elements) { L l = (L)tmp_l; - // foreach (var tmp_k in st.Elements) { K k = (K)tmp_k; - // for (BigInteger j = Lo; j < Hi; j++) { - // for (bool i in Helper.AllBooleans) { - // if (R(i,j,k,l)) { - // _coll.Add(Term(i,j,k,l)); - // } - // } - // } - // } - // } - // return Dafny.Set.FromCollection(_coll); - // }))() - // We also split R(i,j,k,l) to evaluate it as early as possible. - wr = CaptureFreeVariables(e, true, out var su, inLetExprBody, wr, ref wStmts); - e = (SetComprehension)su.Substitute(e); - - Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds - var collectionName = ProtectedFreshId("_coll"); - var setType = e.Type.NormalizeToAncestorType().AsSetType; - var bwr = CreateIIFE0(setType, e.tok, wr, wStmts); - wStmts = bwr.Fork(); - wr = bwr; - EmitSetBuilder_New(wr, e, collectionName); - var n = e.BoundVars.Count; - Contract.Assert(e.Bounds.Count == n); - var processedBounds = new HashSet(); - List<(Expression conj, ISet frees)> unusedConjuncts = Expression.Conjuncts(e.Range).Select(conj => (conj, ModuleResolver.FreeVariables(conj))).ToList(); - unusedConjuncts.ForEach(entry => entry.frees.IntersectWith(e.BoundVars)); - wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr); - for (var i = 0; i < n; i++) { - var bound = e.Bounds[i]; - var bv = e.BoundVars[i]; - processedBounds.Add(bv); - var tmpVar = ProtectedFreshId("_compr_"); - var wStmtsLoop = wr.Fork(); - var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, wStmtsLoop); - wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, true, inLetExprBody, e.tok, collection, wr); - wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr); - } - - EmitSetBuilder_Add(setType, collectionName, e.Term, inLetExprBody, wr); - var returned = EmitReturnExpr(bwr); - GetCollectionBuilder_Build(setType, e.tok, collectionName, returned, wStmts); - - } else if (expr is MapComprehension) { - var e = (MapComprehension)expr; - // For "map i | R(i) :: Term(i)" where the term has type "V" and i has type "U", emit something like: - // ((System.Func>)(() => { - // var _coll = new List>(); - // foreach (L l in sq.Elements) { - // foreach (K k in st.Elements) { - // for (BigInteger j = Lo; j < Hi; j++) { - // for (bool i in Helper.AllBooleans) { - // if (R(i,j,k,l)) { - // _coll.Add(new Pair(i, Term(i)); - // } - // } - // } - // } - // } - // return Dafny.Map.FromCollection(_coll); - // }))() - // We also split R(i,j,k,l) to evaluate it as early as possible. - wr = CaptureFreeVariables(e, true, out var su, inLetExprBody, wr, ref wStmts); - e = (MapComprehension)su.Substitute(e); - - Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds - var mapType = e.Type.NormalizeToAncestorType().AsMapType; - var domtypeName = TypeName(mapType.Domain, wr, e.tok); - var rantypeName = TypeName(mapType.Range, wr, e.tok); - var collection_name = ProtectedFreshId("_coll"); - var bwr = CreateIIFE0(mapType, e.tok, wr, wStmts); - wStmts = bwr.Fork(); - wr = bwr; - EmitMapBuilder_New(wr, e, collection_name); - var n = e.BoundVars.Count; - Contract.Assert(e.Bounds.Count == n); - var processedBounds = new HashSet(); - List<(Expression conj, ISet frees)> unusedConjuncts = Expression.Conjuncts(e.Range).Select(conj => (conj, ModuleResolver.FreeVariables(conj))).ToList(); - unusedConjuncts.ForEach(entry => entry.frees.IntersectWith(e.BoundVars)); - wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr); - for (var i = 0; i < n; i++) { - var bound = e.Bounds[i]; - var bv = e.BoundVars[i]; - processedBounds.Add(bv); - var tmpVar = ProtectedFreshId("_compr_"); - var wStmtsLoop = wr.Fork(); - var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, wStmtsLoop); - wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, true, false, bv.tok, collection, wr); - wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr); - } - - var termLeftWriter = EmitMapBuilder_Add(mapType, e.tok, collection_name, e.Term, inLetExprBody, wr); - if (e.TermLeft == null) { - Contract.Assert(e.BoundVars.Count == 1); - EmitIdentifier(IdName(e.BoundVars[0]), termLeftWriter); - } else { - EmitExpr(e.TermLeft, inLetExprBody, termLeftWriter, wStmts); - } - - var returned = EmitReturnExpr(bwr); - GetCollectionBuilder_Build(mapType, e.tok, collection_name, returned, wStmts); - - } else if (expr is LambdaExpr) { - var e = (LambdaExpr)expr; - - IVariable receiver = null; - if (thisContext != null && (enclosingMethod is { IsTailRecursive: true } || enclosingFunction is { IsTailRecursive: true })) { - var name = ProtectedFreshId("_this"); - var ty = ModuleResolver.GetThisType(e.tok, thisContext); - receiver = new LocalVariable(RangeToken.NoToken, name, ty, false) { - type = ty - }; - var _this = new ThisExpr(thisContext); - wr = EmitBetaRedex(new List() { IdName(receiver) }, new List() { _this }, new List() { _this.Type }, expr.Type, expr.tok, inLetExprBody, wr, ref wStmts); - } - - wr = CaptureFreeVariables(e, false, out var su, inLetExprBody, wr, ref wStmts); - if (receiver != null) { - su = new Substituter(new IdentifierExpr(e.tok, receiver), su.substMap, su.typeMap); - } - - wr = CreateLambda(e.BoundVars.ConvertAll(bv => bv.Type), Token.NoToken, e.BoundVars.ConvertAll(IdName), e.Body.Type, wr, wStmts); - wStmts = wr.Fork(); - wr = EmitReturnExpr(wr); - // May need an upcast or boxing conversion to coerce to the generic arrow result type - wr = EmitCoercionIfNecessary(e.Body.Type, TypeForCoercion(e.Type.AsArrowType.Result), e.Body.tok, wr); - EmitExpr(su.Substitute(e.Body), inLetExprBody, wr, wStmts); - - } else if (expr is StmtExpr) { - var e = (StmtExpr)expr; - EmitExpr(e.E, inLetExprBody, wr, wStmts); - - } else if (expr is ITEExpr) { - var e = (ITEExpr)expr; - // The ghost-ITE optimization applies only to at "the top" of the expression structure of a function - // body. Those cases are handled in TrExprOpt, so we expect the be compiling both branches here. - Contract.Assert(e.HowToCompile == ITEExpr.ITECompilation.CompileBothBranches); - EmitITE(e.Test, e.Thn, e.Els, e.Type, inLetExprBody, wr, wStmts); - - } else if (expr is ConcreteSyntaxExpression) { - var e = (ConcreteSyntaxExpression)expr; - EmitExpr(e.ResolvedExpression, inLetExprBody, wr, wStmts); - - } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression - } - ConcreteSyntaxTree EmitGuardFragment(List<(Expression conj, ISet frees)> unusedConjuncts, HashSet processedBounds, ConcreteSyntaxTree wr) { - Expression localGuard = Expression.CreateBoolLiteral(expr.tok, true); - - foreach (var entry in unusedConjuncts.ToList().Where(entry => entry.frees.IsSubsetOf(processedBounds))) { - localGuard = Expression.CreateAnd(localGuard, entry.conj); - unusedConjuncts.Remove(entry); - } - - if (!LiteralExpr.IsTrue(localGuard)) { - wr = EmitIf(out var guardWriter, false, wr); - EmitExpr(localGuard, inLetExprBody, guardWriter, wStmts); - } - - return wr; - } - } - private void CompileTypeTest(TypeTestExpr expr, bool inLetExprBody, ConcreteSyntaxTree wr, ref ConcreteSyntaxTree wStmts) { var fromType = expr.E.Type; if (fromType.IsSubtypeOf(expr.ToType, false, false)) {