diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index 3dff0529270..bf2113e54e2 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -325,1227 +325,849 @@ public Boogie.Expr TrExpr(Expression expr) { Contract.Requires(Predef != null); switch (expr) { - case LiteralExpr literalExpr: { - LiteralExpr e = literalExpr; - if (e.Value == null) { - return Predef.Null; - } else if (e.Value is bool) { - return MaybeLit(new Boogie.LiteralExpr(GetToken(e), (bool)e.Value)); - } else if (e is CharLiteralExpr) { - // we expect e.Value to be a string representing exactly one char - Boogie.Expr rawElement = null; // assignment to please compiler's definite assignment rule - foreach (var ch in Util.UnescapedCharacters(options, (string)e.Value, false)) { - Contract.Assert(rawElement == null); // we should get here only once - rawElement = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.CharFromInt, null, Boogie.Expr.Literal(ch)); - } - Contract.Assert(rawElement != null); // there should have been an iteration of the loop above - return MaybeLit(rawElement, Predef.CharType); - } else if (e is StringLiteralExpr) { - var str = (StringLiteralExpr)e; - Boogie.Expr seq = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.SeqEmpty, Predef.BoxType); - foreach (var ch in Util.UnescapedCharacters(options, (string)e.Value, str.IsVerbatim)) { - var rawElement = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.CharFromInt, null, Boogie.Expr.Literal(ch)); - Boogie.Expr elt = BoxIfNecessary(GetToken(literalExpr), rawElement, Type.Char); - seq = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.SeqBuild, Predef.BoxType, seq, elt); - } - return MaybeLit(seq, BoogieGenerator.TrType(new SeqType(Type.Char))); - } else if (e.Value is BigInteger) { - var n = Microsoft.BaseTypes.BigNum.FromBigInt((BigInteger)e.Value); - if (e.Type.NormalizeToAncestorType() is BitvectorType bitvectorType) { - return MaybeLit(BoogieGenerator.BplBvLiteralExpr(GetToken(e), n, bitvectorType)); - } else if (e.Type.IsBigOrdinalType) { - var fromNat = FunctionCall(GetToken(literalExpr), "ORD#FromNat", Predef.BigOrdinalType, Boogie.Expr.Literal(n)); - return MaybeLit(fromNat, Predef.BigOrdinalType); - } else { - return MaybeLit(Boogie.Expr.Literal(n)); - } - } else if (e.Value is BaseTypes.BigDec) { - return MaybeLit(Boogie.Expr.Literal((BaseTypes.BigDec)e.Value)); - } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal - } - } + case LiteralExpr literalExpr: + return TranslateLiteralExpr(literalExpr); case ThisExpr: - return new Boogie.IdentifierExpr(GetToken(expr), This, BoogieGenerator.TrType(expr.Type)); - case IdentifierExpr identifierExpr: { - IdentifierExpr e = identifierExpr; - Contract.Assert(e.Var != null); - return BoogieGenerator.TrVar(GetToken(identifierExpr), e.Var); - } - case BoogieWrapper wrapper: { - var e = wrapper; - return e.Expr; + return new Bpl.IdentifierExpr(GetToken(expr), This, BoogieGenerator.TrType(expr.Type)); + case IdentifierExpr identifierExpr: + return BoogieGenerator.TrVar(GetToken(identifierExpr), identifierExpr.Var); + case BoogieWrapper wrapper: + return wrapper.Expr; + case BoogieFunctionCall call: + return TranslateBoogieFunctionCall(call); + case SetDisplayExpr displayExpr: + return TranslateSetDisplayExpr(displayExpr); + case MultiSetDisplayExpr displayExpr: + return TranslateMultiSetDisplayExpr(displayExpr); + case SeqDisplayExpr displayExpr: + return TranslateSeqDisplayExpr(displayExpr); + case MapDisplayExpr displayExpr: + return TranslateMapDisplayExpr(displayExpr); + case MemberSelectExpr selectExpr: + return TranslateMemberSelectExpr(selectExpr); + case SeqSelectExpr selectExpr: + return TranslateSeqSelectExpr(selectExpr); + case SeqUpdateExpr updateExpr: + return TranslateSeqUpdateExpr(updateExpr); + case MultiSelectExpr selectExpr: + return TranslateMultiSelectExpr(selectExpr); + case ApplyExpr applyExpr: + return TranslateApplyExpr(applyExpr); + case FunctionCallExpr callExpr: + return TranslateFunctionCallExpr(callExpr); + case DatatypeValue value: + return TranslateDatatypeValue(value); + case SeqConstructionExpr constructionExpr: + return TranslateSeqConstructionExpr(constructionExpr); + case MultiSetFormingExpr formingExpr: + return TranslateMultisetFormingExpr(formingExpr); + case OldExpr oldExpr: { + return OldAt(oldExpr.AtLabel).TrExpr(oldExpr.Expr); } - case BoogieFunctionCall call: { - var e = call; - var id = new Boogie.IdentifierExpr(GetToken(e), e.FunctionName, BoogieGenerator.TrType(e.Type)); - var args = new List(); - foreach (var arg in e.TyArgs) { - args.Add(BoogieGenerator.TypeToTy(arg)); - } - if (e.UsesHeap) { - args.Add(HeapExpr); - } - if (e.UsesOldHeap) { - args.Add(Old.HeapExpr); - } - foreach (var heapAtLabel in e.HeapAtLabels) { - var bv = BplBoundVar("$Heap_at_" + heapAtLabel.AssignUniqueId(BoogieGenerator.CurrentIdGenerator), BoogieGenerator.Predef.HeapType, out var ve); - args.Add(ve); - } - foreach (var arg in e.Args) { - args.Add(TrExpr(arg)); - } - return new Boogie.NAryExpr(GetToken(e), new Boogie.FunctionCall(id), args); + case UnchangedExpr unchangedExpr: { + return BoogieGenerator.FrameCondition(GetToken(unchangedExpr), unchangedExpr.Frame, false, FrameExpressionUse.Unchanged, OldAt(unchangedExpr.AtLabel), this, this, true); } - case SetDisplayExpr displayExpr: { - SetDisplayExpr e = displayExpr; - Boogie.Expr s = BoogieGenerator.FunctionCall(GetToken(displayExpr), e.Finite ? BuiltinFunction.SetEmpty : BuiltinFunction.ISetEmpty, Predef.BoxType); - var isLit = true; - foreach (Expression ee in e.Elements) { - var rawElement = TrExpr(ee); - isLit = isLit && BoogieGenerator.IsLit(rawElement); - Boogie.Expr ss = BoxIfNecessary(GetToken(displayExpr), rawElement, cce.NonNull(ee.Type)); - s = BoogieGenerator.FunctionCall(GetToken(displayExpr), e.Finite ? BuiltinFunction.SetUnionOne : BuiltinFunction.ISetUnionOne, Predef.BoxType, s, ss); - } - if (isLit) { - // Lit-lifting: All elements are lit, so the set is Lit too - s = MaybeLit(s, Predef.BoxType); - } - return s; + case UnaryOpExpr opExpr: + return TranslateUnaryOpExpression(opExpr); + case ConversionExpr conversionExpr: { + return BoogieGenerator.ConvertExpression(GetToken(conversionExpr), TrExpr(conversionExpr.E), conversionExpr.E.Type, conversionExpr.ToType); } - case MultiSetDisplayExpr displayExpr: { - MultiSetDisplayExpr e = displayExpr; - Boogie.Expr s = BoogieGenerator.FunctionCall(GetToken(displayExpr), BuiltinFunction.MultiSetEmpty, Predef.BoxType); - var isLit = true; - foreach (Expression ee in e.Elements) { - var rawElement = TrExpr(ee); - isLit = isLit && BoogieGenerator.IsLit(rawElement); - Boogie.Expr ss = BoxIfNecessary(GetToken(displayExpr), rawElement, cce.NonNull(ee.Type)); - s = BoogieGenerator.FunctionCall(GetToken(displayExpr), BuiltinFunction.MultiSetUnionOne, Predef.BoxType, s, ss); - } - if (isLit) { - // Lit-lifting: All elements are lit, so the multiset is Lit too - s = MaybeLit(s, Predef.BoxType); - } - return s; + case TypeTestExpr testExpr: { + return BoogieGenerator.GetSubrangeCheck(testExpr.Origin, TrExpr(testExpr.E), testExpr.E.Type, testExpr.ToType, testExpr.E, null, out var _) ?? Expr.True; } - case SeqDisplayExpr displayExpr: { - SeqDisplayExpr e = displayExpr; - // Note: a LiteralExpr(string) is really another kind of SeqDisplayExpr - Boogie.Expr s = BoogieGenerator.FunctionCall(GetToken(displayExpr), BuiltinFunction.SeqEmpty, Predef.BoxType); - var isLit = true; - foreach (Expression ee in e.Elements) { - var rawElement = TrExpr(ee); - isLit = isLit && BoogieGenerator.IsLit(rawElement); - Boogie.Expr elt = BoxIfNecessary(GetToken(displayExpr), rawElement, ee.Type); - s = BoogieGenerator.FunctionCall(GetToken(displayExpr), BuiltinFunction.SeqBuild, Predef.BoxType, s, elt); - } - if (isLit) { - // Lit-lifting: All elements are lit, so the sequence is Lit too - s = MaybeLit(s, Predef.BoxType); - } - return s; + case BinaryExpr binaryExpr: + return TranslateBinaryExpr(binaryExpr); + case TernaryExpr ternaryExpr: + return TranslateTernaryExpr(ternaryExpr); + case LetExpr letExpr: + return TrLetExpr(letExpr); + case QuantifierExpr quantifierExpr: + return TranslateQuantifierExpr(quantifierExpr); + case SetComprehension comprehension: + return TranslateSetComprehension(comprehension); + case MapComprehension comprehension: + return TranslateMapComprehension(comprehension); + case LambdaExpr lambdaExpr: + return TrLambdaExpr(lambdaExpr); + case StmtExpr stmtExpr: + return TrExpr(stmtExpr.E); + case ITEExpr iteExpr: + return TranslateIfThenElseExpr(iteExpr); + case MatchExpr matchExpr: + return TrExpr(DesugarMatchExpr(matchExpr)); + case ConcreteSyntaxExpression expression: + return TrExpr(expression.ResolvedExpression); + case NestedMatchExpr nestedMatchExpr: + return TrExpr(nestedMatchExpr.Flattened); + case BoxingCastExpr castExpr: + return BoogieGenerator.CondApplyBox(GetToken(castExpr), TrExpr(castExpr.E), castExpr.FromType, castExpr.ToType); + case UnboxingCastExpr castExpr: + return BoogieGenerator.CondApplyUnbox(GetToken(castExpr), TrExpr(castExpr.E), castExpr.FromType, castExpr.ToType); + case DecreasesToExpr decreasesToExpr: + return TranslateDecreasesToExpr(decreasesToExpr); + case FieldLocation fieldLocation: + return TranslateFieldLocation(expr, fieldLocation); + case IndexFieldLocation indexFieldLocation: + return GetArrayIndexFieldName(indexFieldLocation.Origin, indexFieldLocation.Indices.ToList()); + case LocalsObjectExpression: + return Predef.Locals; + default: + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + } + } + + private Expr TranslateFieldLocation(Expression expr, FieldLocation fieldLocation) { + var tok = GetToken(expr); + if (fieldLocation.Field is SpecialField { EnclosingMethod: not null }) { + Expr depthExpr = fieldLocation.AtCallSite ? + FunctionCall(tok, "+", Boogie.Type.Int, Id(tok, "depth"), One(tok)) + : Id(tok, "depth"); + return FunctionCall(tok, "local_field", Predef.FieldName(tok), + Id(tok, BoogieGenerator.GetField(fieldLocation.Field)), + depthExpr + ); + } else { + return Id(tok, BoogieGenerator.GetField(fieldLocation.Field)); + } + } + + private Expr TranslateIfThenElseExpr(ITEExpr iteExpr) { + var g = RemoveLit(TrExpr(iteExpr.Test)); + var thn = BoogieGenerator.AdaptBoxing(iteExpr.Thn.Origin, BoogieGenerator.RemoveLit(TrExpr(iteExpr.Thn)), iteExpr.Thn.Type, iteExpr.Type); + var els = BoogieGenerator.AdaptBoxing(iteExpr.Els.Origin, BoogieGenerator.RemoveLit(TrExpr(iteExpr.Els)), iteExpr.Els.Type, iteExpr.Type); + return new NAryExpr(GetToken(iteExpr), new IfThenElse(GetToken(iteExpr)), new List { g, thn, els }); + } + + private Expr TranslateDecreasesToExpr(DecreasesToExpr decreasesToExpr) { + var oldArray = decreasesToExpr.OldExpressions.ToArray(); + var newArray = decreasesToExpr.NewExpressions.ToArray(); + List newExprs = []; + List oldExprs = []; + List newExprsDafny = []; + List oldExprsDafny = []; + int N = Math.Min(oldArray.Length, newArray.Length); + for (int i = 0; i < N; i++) { + if (!CompatibleDecreasesTypes(oldArray[i].Type, newArray[i].Type)) { + N = i; + break; + } + oldExprsDafny.Add(oldArray[i]); + oldExprs.Add(TrExpr(oldArray[i])); + newExprsDafny.Add(newArray[i]); + newExprs.Add(TrExpr(newArray[i])); + } + + bool endsWithWinningTopComparison = N == oldArray.Length && N < newArray.Length; + var allowNoChange = decreasesToExpr.AllowNoChange || endsWithWinningTopComparison; + List toks = oldExprs.Zip(newExprs, (_, _) => (IOrigin)decreasesToExpr.Origin).ToList(); + var decreasesExpr = BoogieGenerator.DecreasesCheck(toks, null, + newExprsDafny, oldExprsDafny, newExprs, oldExprs, null, + null, allowNoChange, false); + return decreasesExpr; + } + + private Expr TranslateMapComprehension(MapComprehension comprehension) { + var e = comprehension; + // Translate "map x,y | R(x,y) :: F(x,y) := G(x,y)" into + // Map#Glue(lambda w: BoxType :: exists x,y :: R(x,y) && unbox(w) == F(x,y), + // lambda w: BoxType :: G(project_x(unbox(w)), project_y(unbox(w))), + // type)". + // where project_x and project_y are functions defined (elsewhere, in CanCallAssumption) by the following axiom: + // forall x,y :: R(x,y) ==> var x',y' := project_x(unbox(F(x,y))),project_y(unbox(F(x,y))); R(x',y') && F(x',y') == F(x,y) + // that is (without the let expression): + // forall x,y :: R(x,y) ==> R(project_x(unbox(F(x,y))), project_y(unbox(F(x,y)))) && F(project_x(unbox(F(x,y))), project_y(unbox(F(x,y)))) == F(x,y) + // + // In the common case where F(x,y) is omitted (in which case the list of bound variables is restricted to length 1): + // Translate "map x | R(x) :: G(x)" into + // Map#Glue(lambda w: BoxType :: R(unbox(w)), + // lambda w: BoxType :: G(unbox(w)), + // type)". + List bvars = []; + List freeOfAlloc = BoundedPool.HasBounds(e.Bounds, BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc); + + Boogie.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); + + var wVar = new Boogie.BoundVariable(GetToken(comprehension), new Boogie.TypedIdent(GetToken(comprehension), BoogieGenerator.CurrentIdGenerator.FreshId("$w#"), Predef.BoxType)); + + Boogie.Expr keys, values; + if (!e.IsGeneralMapComprehension) { + var bv = e.BoundVars[0]; + var w = new Boogie.IdentifierExpr(GetToken(comprehension), wVar); + Boogie.Expr unboxw = BoogieGenerator.UnboxUnlessInherentlyBoxed(w, bv.Type); + Boogie.Expr typeAntecedent = BoogieGenerator.MkIsBox(w, bv.Type); + if (freeOfAlloc != null && !freeOfAlloc[0]) { + var isAlloc = BoogieGenerator.MkIsAllocBox(w, bv.Type, HeapExpr); + typeAntecedent = BplAnd(typeAntecedent, isAlloc); + } + var subst = new Dictionary(); + subst.Add(bv, new BoogieWrapper(unboxw, bv.Type)); + + var ebody = BplAnd(typeAntecedent, TrExpr(BoogieGenerator.Substitute(e.Range, null, subst))); + keys = new Boogie.LambdaExpr(GetToken(e), [], [wVar], kv, ebody); + ebody = TrExpr(BoogieGenerator.Substitute(e.Term, null, subst)); + values = new Boogie.LambdaExpr(GetToken(e), [], [wVar], kv, BoxIfNecessary(GetToken(comprehension), ebody, e.Term.Type)); + } else { + var t = e.TermLeft; + var w = new Boogie.IdentifierExpr(GetToken(comprehension), wVar); + Boogie.Expr unboxw = BoogieGenerator.UnboxUnlessInherentlyBoxed(w, t.Type); + Boogie.Expr typeAntecedent = BoogieGenerator.MkIsBox(w, t.Type); + if (freeOfAlloc != null && !freeOfAlloc[0]) { + var isAlloc = BoogieGenerator.MkIsAllocBox(w, t.Type, HeapExpr); + typeAntecedent = BplAnd(typeAntecedent, isAlloc); + } + + BoogieGenerator.CreateBoundVariables(e.BoundVars, out var bvs, out var args); + Contract.Assert(e.BoundVars.Count == bvs.Count); + var subst = new Dictionary(); + for (var i = 0; i < e.BoundVars.Count; i++) { + subst.Add(e.BoundVars[i], new BoogieWrapper(args[i], e.BoundVars[i].Type)); + } + var rr = TrExpr(BoogieGenerator.Substitute(e.Range, null, subst)); + var ff = TrExpr(BoogieGenerator.Substitute(t, null, subst)); + var exst_body = BplAnd(rr, Boogie.Expr.Eq(unboxw, ff)); + var ebody = BplAnd(typeAntecedent, new Boogie.ExistsExpr(GetToken(e), bvs, exst_body)); + keys = new Boogie.LambdaExpr(GetToken(e), [], [wVar], kv, ebody); + + BoogieGenerator.CreateMapComprehensionProjectionFunctions(e); + Contract.Assert(e.ProjectionFunctions != null && e.ProjectionFunctions.Count == e.BoundVars.Count); + subst = new Dictionary(); + for (var i = 0; i < e.BoundVars.Count; i++) { + var p = new Boogie.NAryExpr(GetToken(e), new Boogie.FunctionCall(e.ProjectionFunctions[i]), new List { unboxw }); + var prj = new BoogieWrapper(p, e.BoundVars[i].Type); + subst.Add(e.BoundVars[i], prj); + } + ebody = TrExpr(BoogieGenerator.Substitute(e.Term, null, subst)); + values = new Boogie.LambdaExpr(GetToken(e), [], [wVar], kv, BoxIfNecessary(GetToken(comprehension), ebody, e.Term.Type)); + } + + return BoogieGenerator.FunctionCall(GetToken(e), + e.Finite ? BuiltinFunction.MapGlue : BuiltinFunction.IMapGlue, + null, + e.Finite ? FunctionCall(GetToken(comprehension), "Set#FromBoogieMap", Predef.SetType, keys) : keys, + values, BoogieGenerator.TypeToTy(comprehension.Type)); + } + + private Expr TranslateSetComprehension(SetComprehension comprehension) { + var e = comprehension; + List freeOfAlloc = BoundedPool.HasBounds(e.Bounds, BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc); + + // Translate "set xs | R :: T" into: + // Set#FromBoogieMap(lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))) + // or if "T" is "xs", then: + // Set#FromBoogieMap(lambda y: BoxType :: CorrectType(y) && R[xs := Unbox(y)]) + // where Set#FromBoogieMap is omitted for iset. + // FIXME: This is not a good translation, see comment in PreludeCore.bpl. It should be changed to not use a Boogie lambda expression + // but to instead do the lambda lifting here. + var yVar = new Boogie.BoundVariable(GetToken(comprehension), new Boogie.TypedIdent(GetToken(comprehension), BoogieGenerator.CurrentIdGenerator.FreshId("$y#"), Predef.BoxType)); + Boogie.Expr y = new Boogie.IdentifierExpr(GetToken(comprehension), yVar); + Boogie.Expr lbody; + if (e.TermIsSimple) { + var bv = e.BoundVars[0]; + // lambda y: BoxType :: CorrectType(y) && R[xs := yUnboxed] + Boogie.Expr typeAntecedent = BoogieGenerator.MkIsBox(new Boogie.IdentifierExpr(GetToken(comprehension), yVar), bv.Type); + if (freeOfAlloc != null && !freeOfAlloc[0]) { + var isAlloc = BoogieGenerator.MkIsAllocBox(new Boogie.IdentifierExpr(GetToken(comprehension), yVar), bv.Type, HeapExpr); + typeAntecedent = BplAnd(typeAntecedent, isAlloc); + } + var yUnboxed = BoogieGenerator.UnboxUnlessInherentlyBoxed(new Boogie.IdentifierExpr(GetToken(comprehension), yVar), bv.Type); + var range = BoogieGenerator.Substitute(e.Range, bv, new BoogieWrapper(yUnboxed, bv.Type)); + lbody = BplAnd(typeAntecedent, TrExpr(range)); + } else { + // lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T)) + List bvars = []; + Boogie.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars, false, freeOfAlloc); + + var eq = Boogie.Expr.Eq(y, BoxIfNecessary(GetToken(comprehension), TrExpr(e.Term), e.Term.Type)); + var ebody = BplAnd(BplAnd(typeAntecedent, TrExpr(e.Range)), eq); + var triggers = BoogieGenerator.TrTrigger(this, e.Attributes, GetToken(e)); + lbody = new Boogie.ExistsExpr(GetToken(comprehension), bvars, triggers, ebody); + } + Boogie.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); + var lambda = new Boogie.LambdaExpr(GetToken(comprehension), [], [yVar], kv, lbody); + return comprehension.Type.NormalizeToAncestorType().AsSetType.Finite + ? FunctionCall(GetToken(comprehension), "Set#FromBoogieMap", Predef.SetType, lambda) + : lambda; + } + + private Expr TranslateQuantifierExpr(QuantifierExpr quantifierExpr) { + QuantifierExpr e = quantifierExpr; + + if (e.SplitQuantifier != null) { + return TrExpr(e.SplitQuantifierExpression); + } else { + List bvars = []; + var bodyEtran = this; + if (e is ExistsExpr && BoogieGenerator.stmtContext == StmtType.ASSERT && BoogieGenerator.adjustFuelForExists) { + // assert exists need decrease fuel by 1 + bodyEtran = bodyEtran.DecreaseFuel(1); + // set adjustFuelForExists to false so that we don't keep decrease the fuel in cases like the expr below. + // assert exists p:int :: exists t:T :: ToInt(t) > 0; + BoogieGenerator.adjustFuelForExists = false; + } else if (e is ExistsExpr && BoogieGenerator.stmtContext == StmtType.ASSUME && BoogieGenerator.adjustFuelForExists) { + // assume exists need increase fuel by 1 + bodyEtran = bodyEtran.LayerOffset(1); + BoogieGenerator.adjustFuelForExists = false; + } + + Boogie.Expr antecedent = Boogie.Expr.True; + + List freeOfAlloc = BoundedPool.HasBounds(e.Bounds, BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc); + antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars, false, freeOfAlloc)); // initHeapForAllStmt + + Boogie.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); + Boogie.Trigger tr = BoogieGenerator.TrTrigger(bodyEtran, e.Attributes, GetToken(e), bvars, null, null); + + if (e.Range != null) { + antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range)); + } + Boogie.Expr body = bodyEtran.TrExpr(e.Term); + + if (e is ForallExpr) { + return new Boogie.ForallExpr(GetToken(quantifierExpr), [], bvars, kv, tr, BplImp(antecedent, body)); + } else { + Contract.Assert(e is ExistsExpr); + return new Boogie.ExistsExpr(GetToken(quantifierExpr), [], bvars, kv, tr, BplAnd(antecedent, body)); + } + } + } + + private Expr TranslateTernaryExpr(TernaryExpr ternaryExpr) { + var e = ternaryExpr; + var e0 = TrExpr(e.E0); + if (!e.E0.Type.IsBigOrdinalType) { + e0 = FunctionCall(e0.tok, "ORD#FromNat", Predef.BigOrdinalType, e0); + } + var e1 = TrExpr(e.E1); + var e2 = TrExpr(e.E2); + switch (e.Op) { + case TernaryExpr.Opcode.PrefixEqOp: + case TernaryExpr.Opcode.PrefixNeqOp: + var e1type = e.E1.Type.NormalizeExpand(); + var e2type = e.E2.Type.NormalizeExpand(); + var cot = e1type.AsCoDatatype; + Contract.Assert(cot != null); // the argument types of prefix equality (and prefix disequality) are codatatypes + var r = BoogieGenerator.CoEqualCall(cot, e1type.TypeArgs, e2type.TypeArgs, e0, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e1, e2); + if (e.Op == TernaryExpr.Opcode.PrefixEqOp) { + return r; + } else { + return Boogie.Expr.Unary(GetToken(ternaryExpr), UnaryOperator.Opcode.Not, r); } - case MapDisplayExpr displayExpr: { - MapDisplayExpr e = displayExpr; - Boogie.Type maptype = e.Finite ? Predef.MapType : Predef.IMapType; - Boogie.Expr s = BoogieGenerator.FunctionCall(GetToken(displayExpr), e.Finite ? BuiltinFunction.MapEmpty : BuiltinFunction.IMapEmpty, Predef.BoxType); - var isLit = true; - foreach (MapDisplayEntry p in e.Elements) { - var rawA = TrExpr(p.A); - var rawB = TrExpr(p.B); - isLit = isLit && BoogieGenerator.IsLit(rawA) && BoogieGenerator.IsLit(rawB); - Boogie.Expr elt = BoxIfNecessary(GetToken(displayExpr), rawA, cce.NonNull(p.A.Type)); - Boogie.Expr elt2 = BoxIfNecessary(GetToken(displayExpr), rawB, cce.NonNull(p.B.Type)); - s = FunctionCall(GetToken(displayExpr), e.Finite ? "Map#Build" : "IMap#Build", maptype, s, elt, elt2); - } - if (isLit) { - // Lit-lifting: All keys and values are lit, so the map is Lit too - s = MaybeLit(s, Predef.BoxType); - } - return s; + default: + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression + } + } + + private Expr TranslateUnaryOpExpression(UnaryOpExpr opExpr) { + var e = opExpr; + Boogie.Expr arg = TrExpr(e.E); + switch (e.ResolvedOp) { + case UnaryOpExpr.ResolvedOpcode.Lit: + return MaybeLit(arg); + case UnaryOpExpr.ResolvedOpcode.BVNot: + var bvWidth = opExpr.Type.NormalizeToAncestorType().AsBitVectorType.Width; + var bvType = BoogieGenerator.BplBvType(bvWidth); + Boogie.Expr r = FunctionCall(GetToken(opExpr), "not_bv" + bvWidth, bvType, arg); + if (BoogieGenerator.IsLit(arg)) { + r = MaybeLit(r, bvType); } - case MemberSelectExpr selectExpr: { - var e = selectExpr; - return e.MemberSelectCase( - field => { - var useSurrogateLocal = BoogieGenerator.inBodyInitContext && Expression.AsThis(e.Obj) != null && !field.IsInstanceIndependentConstant; - var fType = BoogieGenerator.TrType(field.Type); - if (useSurrogateLocal) { - return new Boogie.IdentifierExpr(GetToken(expr), BoogieGenerator.SurrogateName(field), fType); - } else if (field is ConstantField) { - var typeMap = e.TypeArgumentSubstitutionsWithParents(); - var args = GetTypeParams(field.EnclosingClass).ConvertAll(tp => BoogieGenerator.TypeToTy(typeMap[tp])); - Boogie.Expr result; - if (field.IsStatic) { - result = new Boogie.NAryExpr(GetToken(expr), new Boogie.FunctionCall(BoogieGenerator.GetReadonlyField(field)), args); - } else { - Boogie.Expr obj = BoogieGenerator.BoxifyForTraitParent(e.Origin, TrExpr(e.Obj), e.Member, e.Obj.Type); - args.Add(obj); - result = new Boogie.NAryExpr(GetToken(expr), new Boogie.FunctionCall(BoogieGenerator.GetReadonlyField(field)), args); - } - result = BoogieGenerator.CondApplyUnbox(GetToken(expr), result, field.Type, expr.Type); - return result; - } else { - Boogie.Expr obj = TrExpr(e.Obj); - Boogie.Expr result; - if (field.IsMutable) { - var tok = GetToken(expr); - result = BoogieGenerator.ReadHeap(tok, HeapExpr, obj, new Boogie.IdentifierExpr(GetToken(expr), BoogieGenerator.GetField(field))); - result = fType == Predef.BoxType ? result : BoogieGenerator.ApplyUnbox(tok, result, fType); - return BoogieGenerator.CondApplyUnbox(tok, result, field.Type, expr.Type); - } else { - result = new Boogie.NAryExpr(GetToken(expr), new Boogie.FunctionCall(BoogieGenerator.GetReadonlyField(field)), - new List { obj }); - result = BoogieGenerator.CondApplyUnbox(GetToken(expr), result, field.Type, expr.Type); - if (BoogieGenerator.IsLit(obj)) { - result = MaybeLit(result, BoogieGenerator.TrType(expr.Type)); - } - return result; - } - } - }, - fn => { - var typeMap = e.TypeArgumentSubstitutionsWithParents(); - var args = GetTypeParams(fn).ConvertAll(tp => BoogieGenerator.TypeToTy(typeMap[tp])); - if (fn.IsFuelAware()) { - args.Add(this.layerInterCluster.GetFunctionFuel(fn)); - } - if (fn.IsOpaque || fn.IsMadeImplicitlyOpaque(options)) { - args.Add(BoogieGenerator.GetRevealConstant(fn)); - } - if (fn is TwoStateFunction) { - args.Add(Old.HeapExpr); - } - if (!fn.IsStatic) { - Boogie.Expr obj = BoogieGenerator.BoxifyForTraitParent(e.Origin, TrExpr(e.Obj), e.Member, e.Obj.Type); - args.Add(obj); - } - return FunctionCall(GetToken(e), BoogieGenerator.FunctionHandle(fn), Predef.HandleType, args); - }); + return r; + case UnaryOpExpr.ResolvedOpcode.BoolNot: + return Boogie.Expr.Unary(GetToken(opExpr), UnaryOperator.Opcode.Not, arg); + case UnaryOpExpr.ResolvedOpcode.SeqLength: + Contract.Assert(e.E.Type.NormalizeToAncestorType() is SeqType); + return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.SeqLength, null, arg); + case UnaryOpExpr.ResolvedOpcode.SetCard: + Contract.Assert(e.E.Type.NormalizeToAncestorType() is SetType { Finite: true }); + return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.SetCard, null, arg); + case UnaryOpExpr.ResolvedOpcode.MultiSetCard: + Contract.Assert(e.E.Type.NormalizeToAncestorType() is MultiSetType); + return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.MultiSetCard, null, arg); + case UnaryOpExpr.ResolvedOpcode.MapCard: + Contract.Assert(e.E.Type.NormalizeToAncestorType() is MapType { Finite: true }); + return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.MapCard, null, arg); + case UnaryOpExpr.ResolvedOpcode.Fresh: + var freshLabel = ((FreshExpr)e).AtLabel; + var eeType = e.E.Type.NormalizeToAncestorType(); + if (eeType is SetType setType) { + // generate: (forall $o: ref :: { $o != null } X[Box($o)] ==> $o != null) && + // (forall $o: ref :: { X[Box($o)] } X[Box($o)] ==> !old($Heap)[$o,alloc]) + // OR, if X[Box($o)] is rewritten into smaller parts, use the less good trigger old($Heap)[$o,alloc] + Boogie.Variable oVar = new Boogie.BoundVariable(GetToken(opExpr), new Boogie.TypedIdent(GetToken(opExpr), "$o", Predef.RefType)); + Boogie.Expr o = new Boogie.IdentifierExpr(GetToken(opExpr), oVar); + Boogie.Expr oNotNull = Boogie.Expr.Neq(o, Predef.Null); + Boogie.Expr oInSet = TrInSet(GetToken(opExpr), o, e.E, setType.Arg, setType.Finite, true, out var performedInSetRewrite); + Boogie.Expr oNotFresh = OldAt(freshLabel).IsAlloced(GetToken(opExpr), o); + Boogie.Expr oIsFresh = Boogie.Expr.Not(oNotFresh); + Boogie.Expr notNullBody = BplImp(oInSet, oNotNull); + Boogie.Expr freshBody = BplImp(oInSet, oIsFresh); + var notNullTrigger = BplTrigger(oNotNull); + var notNullPred = new Boogie.ForallExpr(GetToken(opExpr), [oVar], notNullTrigger, notNullBody); + var freshTrigger = BplTrigger(performedInSetRewrite ? oNotFresh : oInSet); + var freshPred = new Boogie.ForallExpr(GetToken(opExpr), [oVar], freshTrigger, freshBody); + return BplAnd(notNullPred, freshPred); + } else if (eeType is SeqType) { + // generate: (forall $i: int :: 0 <= $i && $i < Seq#Length(X) ==> Unbox(Seq#Index(X,$i)) != null && !old($Heap)[Unbox(Seq#Index(X,$i)),alloc]) + Boogie.Variable iVar = new Boogie.BoundVariable(GetToken(opExpr), new Boogie.TypedIdent(GetToken(opExpr), "$i", Boogie.Type.Int)); + Boogie.Expr i = new Boogie.IdentifierExpr(GetToken(opExpr), iVar); + Boogie.Expr iBounds = BoogieGenerator.InSeqRange(GetToken(opExpr), i, Type.Int, TrExpr(e.E), true, null, false); + Boogie.Expr XsubI = BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.SeqIndex, Predef.RefType, TrExpr(e.E), i); + XsubI = BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.Unbox, Predef.RefType, XsubI); + Boogie.Expr oNotFresh = OldAt(freshLabel).IsAlloced(GetToken(opExpr), XsubI); + Boogie.Expr oIsFresh = Boogie.Expr.Not(oNotFresh); + Boogie.Expr xsubiNotNull = Boogie.Expr.Neq(XsubI, Predef.Null); + Boogie.Expr body = BplImp(iBounds, BplAnd(xsubiNotNull, oIsFresh)); + //TRIGGERS: Does this make sense? dafny0\SmallTests + // BROKEN // NEW_TRIGGER + //TRIG (forall $i: int :: 0 <= $i && $i < Seq#Length(Q#0) && $Unbox(Seq#Index(Q#0, $i)): ref != null ==> !read(old($Heap), $Unbox(Seq#Index(Q#0, $i)): ref, alloc)) + return new Boogie.ForallExpr(GetToken(opExpr), [iVar], body); + } else { + // generate: x != null && !old($Heap)[x] + Boogie.Expr oNull = Boogie.Expr.Neq(TrExpr(e.E), Predef.Null); + Boogie.Expr oIsFresh = Boogie.Expr.Not(OldAt(freshLabel).IsAlloced(GetToken(opExpr), TrExpr(e.E))); + return Boogie.Expr.Binary(GetToken(opExpr), BinaryOperator.Opcode.And, oNull, oIsFresh); } - case SeqSelectExpr selectExpr: { - SeqSelectExpr e = selectExpr; - Boogie.Expr seq = TrExpr(e.Seq); - var seqType = e.Seq.Type.NormalizeToAncestorType(); - Type elmtType = null; - Type domainType = null; - Contract.Assert(seqType != null); // the expression has been successfully resolved - if (seqType.IsArrayType) { - domainType = Type.Int; - elmtType = UserDefinedType.ArrayElementType(seqType); - } else if (seqType is SeqType) { - domainType = Type.Int; - elmtType = ((SeqType)seqType).Arg; - } else if (seqType is MapType) { - domainType = ((MapType)seqType).Domain; - elmtType = ((MapType)seqType).Range; - } else if (seqType is MultiSetType) { - domainType = ((MultiSetType)seqType).Arg; - elmtType = Type.Int; - } else { Contract.Assert(false); } - Boogie.Type elType = BoogieGenerator.TrType(elmtType); - Boogie.Type dType = BoogieGenerator.TrType(domainType); - Boogie.Expr e0 = e.E0 == null ? null : TrExpr(e.E0); - if (e0 != null && e.E0.Type.IsBitVectorType) { - e0 = BoogieGenerator.ConvertExpression(GetToken(e.E0), e0, e.E0.Type, Type.Int); - } - Boogie.Expr e1 = e.E1 == null ? null : TrExpr(e.E1); - if (e1 != null && e.E1.Type.IsBitVectorType) { - e1 = BoogieGenerator.ConvertExpression(GetToken(e.E1), e1, e.E1.Type, Type.Int); - } - if (e.SelectOne) { - Contract.Assert(e1 == null); - Boogie.Expr x; - if (seqType.IsArrayType) { - Boogie.Expr fieldName = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.IndexField, null, e0); - x = BoogieGenerator.ReadHeap(GetToken(selectExpr), HeapExpr, TrExpr(e.Seq), fieldName); - } else if (seqType is SeqType) { - x = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.SeqIndex, Predef.BoxType, seq, e0); - } else if (seqType is MapType) { - bool finite = ((MapType)seqType).Finite; - var f = finite ? BuiltinFunction.MapElements : BuiltinFunction.IMapElements; - x = BoogieGenerator.FunctionCall(GetToken(selectExpr), f, finite ? Predef.MapType : Predef.IMapType, seq); - x = Boogie.Expr.Select(x, BoxIfNecessary(GetToken(e), e0, domainType)); - } else if (seqType is MultiSetType) { - x = BoogieGenerator.MultisetMultiplicity(GetToken(selectExpr), TrExpr(e.Seq), BoxIfNecessary(GetToken(selectExpr), e0, domainType)); - } else { Contract.Assert(false); x = null; } - if (!ModeledAsBoxType(elmtType) && !(seqType is MultiSetType)) { - x = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.Unbox, elType, x); - } - return x; - } else { - if (seqType.IsArrayType) { - seq = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.SeqFromArray, elType, HeapExpr, seq); - } - var isLit = BoogieGenerator.IsLit(seq); - if (e1 != null) { - isLit = isLit && BoogieGenerator.IsLit(e1); - seq = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.SeqTake, elType, seq, e1); - } - if (e0 != null) { - isLit = isLit && BoogieGenerator.IsLit(e0); - seq = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.SeqDrop, elType, seq, e0); - } - // if e0 == null && e1 == null, then we have the identity operation seq[..] == seq; - if (isLit && (e0 != null || e1 != null)) { - // Lit-lift the expression - seq = MaybeLit(seq, BoogieGenerator.TrType(selectExpr.Type)); + case UnaryOpExpr.ResolvedOpcode.Allocated: + // Translate with $IsAllocBox, even if it requires boxing the argument. This has the effect of giving + // both the $IsAllocBox and $IsAlloc forms, because the axioms that connects these two is triggered + // by $IsAllocBox. + return BoogieGenerator.MkIsAllocBox(BoxIfNecessary(e.E.Origin, TrExpr(e.E), e.E.Type), e.E.Type, HeapExpr); + case UnaryOpExpr.ResolvedOpcode.Assigned: + string name = null; + switch (e.E.Resolved) { + case IdentifierExpr ie: + name = ie.Var.UniqueName; + break; + case MemberSelectExpr mse: + if (BoogieGenerator.inBodyInitContext && Expression.AsThis(mse.Obj) != null) { + name = BoogieGenerator.SurrogateName(mse.Member as Field); } - return seq; - } - } - case SeqUpdateExpr updateExpr: { - SeqUpdateExpr e = updateExpr; - Boogie.Expr seq = TrExpr(e.Seq); - var seqType = e.Seq.Type.NormalizeToAncestorType(); - if (seqType is SeqType) { - Boogie.Expr index = TrExpr(e.Index); - index = BoogieGenerator.ConvertExpression(GetToken(e.Index), index, e.Index.Type, Type.Int); - Boogie.Expr val = BoxIfNecessary(GetToken(updateExpr), TrExpr(e.Value), e.Value.Type); - return BoogieGenerator.FunctionCall(GetToken(updateExpr), BuiltinFunction.SeqUpdate, Predef.BoxType, seq, index, val); - } else if (seqType is MapType) { - MapType mt = (MapType)seqType; - Boogie.Type maptype = mt.Finite ? Predef.MapType : Predef.IMapType; - Boogie.Expr index = BoxIfNecessary(GetToken(updateExpr), TrExpr(e.Index), mt.Domain); - Boogie.Expr val = BoxIfNecessary(GetToken(updateExpr), TrExpr(e.Value), mt.Range); - return FunctionCall(GetToken(updateExpr), mt.Finite ? "Map#Build" : "IMap#Build", maptype, seq, index, val); - } else if (seqType is MultiSetType) { - Type elmtType = cce.NonNull((MultiSetType)seqType).Arg; - Boogie.Expr index = BoxIfNecessary(GetToken(updateExpr), TrExpr(e.Index), elmtType); - Boogie.Expr val = TrExpr(e.Value); - return BoogieGenerator.UpdateMultisetMultiplicity(GetToken(updateExpr), seq, index, val); - } else { - Contract.Assert(false); - throw new cce.UnreachableException(); - } + break; } - case MultiSelectExpr selectExpr: { - MultiSelectExpr e = selectExpr; - Type elmtType = UserDefinedType.ArrayElementType(e.Array.Type); ; - Boogie.Type elType = BoogieGenerator.TrType(elmtType); - - Boogie.Expr fieldName = GetArrayIndexFieldName(GetToken(selectExpr), e.Indices); - Boogie.Expr x = BoogieGenerator.ReadHeap(GetToken(selectExpr), HeapExpr, TrExpr(e.Array), fieldName); - if (!ModeledAsBoxType(elmtType)) { - x = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.Unbox, elType, x); - } - return x; + + if (name == null) { + return Expr.True; } - case ApplyExpr applyExpr: { - ApplyExpr e = applyExpr; - int arity = e.Args.Count; - var tt = e.Function.Type.AsArrowType; - Contract.Assert(tt != null); - Contract.Assert(tt.Arity == arity); - - { - // optimisation: if this could have just as well been a FunctionCallExpr, call it as such! - var con = e.Function as ConcreteSyntaxExpression; - var recv = con == null ? e.Function : con.Resolved; - var mem = recv as MemberSelectExpr; - var fn = mem == null ? null : mem.Member as Function; - if (fn != null) { - return TrExpr(new FunctionCallExpr(e.Origin, fn.NameNode, mem.Obj, e.Origin, e.CloseParen, e.Args) { - Function = fn, - Type = e.Type, - TypeApplication_AtEnclosingClass = mem.TypeApplicationAtEnclosingClass, - TypeApplication_JustFunction = mem.TypeApplicationJustMember - }); - } - } + BoogieGenerator.DefiniteAssignmentTrackers.TryGetValue(name, out var defass); + return defass; + default: + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression + } + } - Func TrArg = arg => BoogieGenerator.BoxIfNotNormallyBoxed(arg.Origin, TrExpr(arg), arg.Type); + private Expr TranslateMultisetFormingExpr(MultiSetFormingExpr formingExpr) { + MultiSetFormingExpr e = formingExpr; + var eType = e.E.Type.NormalizeToAncestorType(); + if (eType is SetType setType) { + return BoogieGenerator.FunctionCall(GetToken(formingExpr), BuiltinFunction.MultiSetFromSet, BoogieGenerator.TrType(setType.Arg), TrExpr(e.E)); + } else if (eType is SeqType seqType) { + return BoogieGenerator.FunctionCall(GetToken(formingExpr), BuiltinFunction.MultiSetFromSeq, BoogieGenerator.TrType(seqType.Arg), TrExpr(e.E)); + } else { + Contract.Assert(false); throw new cce.UnreachableException(); + } + } - var applied = FunctionCall(GetToken(applyExpr), BoogieGenerator.Apply(arity), Predef.BoxType, - Concat(Map(tt.TypeArgs, BoogieGenerator.TypeToTy), - Cons(HeapExprForArrow(e.Function.Type), Cons(TrExpr(e.Function), e.Args.ConvertAll(arg => TrArg(arg)))))); + private Expr TranslateSeqConstructionExpr(SeqConstructionExpr constructionExpr) { + var e = constructionExpr; + var eType = e.Type.NormalizeToAncestorType().AsSeqType.Arg.NormalizeExpand(); + var initalizerHeap = e.Initializer.Type.IsArrowType ? HeapExprForArrow(e.Initializer.Type) : HeapExpr; + return FunctionCall(GetToken(constructionExpr), "Seq#Create", Predef.SeqType, + BoogieGenerator.TypeToTy(eType), + initalizerHeap, + TrExpr(e.N), + TrExpr(e.Initializer)); + } + + private Expr TranslateDatatypeValue(DatatypeValue value) { + DatatypeValue dtv = value; + Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved + List args = []; + + bool argsAreLit = true; + for (int i = 0; i < dtv.Arguments.Count; i++) { + Expression arg = dtv.Arguments[i]; + Type t = dtv.Ctor.Formals[i].Type; + var bArg = TrExpr(arg); + argsAreLit = argsAreLit && BoogieGenerator.IsLit(bArg); + args.Add(BoogieGenerator.AdaptBoxing(GetToken(value), bArg, cce.NonNull(arg.Type), t)); + } + Boogie.IdentifierExpr id = new Boogie.IdentifierExpr(GetToken(dtv), dtv.Ctor.FullName, Predef.DatatypeType); + Boogie.Expr ret = new Boogie.NAryExpr(GetToken(dtv), new Boogie.FunctionCall(id), args); + if (argsAreLit) { + // If all arguments are Lit, so is the whole expression + ret = MaybeLit(ret, Predef.DatatypeType); + } + return ret; + } - return BoogieGenerator.UnboxUnlessInherentlyBoxed(applied, tt.Result); + private Expr TranslateFunctionCallExpr(FunctionCallExpr callExpr) { + FunctionCallExpr e = callExpr; + if (e.Function is SpecialFunction) { + return TrExprSpecialFunctionCall(e); + } else { + Boogie.Expr layerArgument; + Boogie.Expr revealArgument; + var etran = this; + if (e.Function.ContainsQuantifier && BoogieGenerator.stmtContext == StmtType.ASSUME && BoogieGenerator.adjustFuelForExists) { + // we need to increase fuel functions that contain quantifier expr in the assume context. + etran = etran.LayerOffset(1); + BoogieGenerator.adjustFuelForExists = false; + } + if (e.Function.IsFuelAware()) { + Statistics_CustomLayerFunctionCount++; + ModuleDefinition module = e.Function.EnclosingClass.EnclosingModuleDefinition; + if (etran.applyLimited_CurrentFunction != null && + etran.layerIntraCluster != null && + ModuleDefinition.InSameSCC(e.Function, applyLimited_CurrentFunction)) { + layerArgument = etran.layerIntraCluster.GetFunctionFuel(e.Function); + } else { + layerArgument = etran.layerInterCluster.GetFunctionFuel(e.Function); } - case FunctionCallExpr callExpr: { - FunctionCallExpr e = callExpr; - if (e.Function is SpecialFunction) { - return TrExprSpecialFunctionCall(e); - } else { - Boogie.Expr layerArgument; - Boogie.Expr revealArgument; - var etran = this; - if (e.Function.ContainsQuantifier && BoogieGenerator.stmtContext == StmtType.ASSUME && BoogieGenerator.adjustFuelForExists) { - // we need to increase fuel functions that contain quantifier expr in the assume context. - etran = etran.LayerOffset(1); - BoogieGenerator.adjustFuelForExists = false; - } - if (e.Function.IsFuelAware()) { - Statistics_CustomLayerFunctionCount++; - ModuleDefinition module = e.Function.EnclosingClass.EnclosingModuleDefinition; - if (etran.applyLimited_CurrentFunction != null && - etran.layerIntraCluster != null && - ModuleDefinition.InSameSCC(e.Function, applyLimited_CurrentFunction)) { - layerArgument = etran.layerIntraCluster.GetFunctionFuel(e.Function); - } else { - layerArgument = etran.layerInterCluster.GetFunctionFuel(e.Function); - } - } else { - layerArgument = null; - } + } else { + layerArgument = null; + } - if (e.Function.IsOpaque || e.Function.IsMadeImplicitlyOpaque(options)) { - revealArgument = BoogieGenerator.GetRevealConstant(e.Function); - } else { - revealArgument = null; - } + if (e.Function.IsOpaque || e.Function.IsMadeImplicitlyOpaque(options)) { + revealArgument = BoogieGenerator.GetRevealConstant(e.Function); + } else { + revealArgument = null; + } - var ty = BoogieGenerator.TrType(e.Type); - var id = new Boogie.IdentifierExpr(GetToken(e), e.Function.FullSanitizedName, ty); + var ty = BoogieGenerator.TrType(e.Type); + var id = new Boogie.IdentifierExpr(GetToken(e), e.Function.FullSanitizedName, ty); - var args = FunctionInvocationArguments(e, layerArgument, revealArgument, false, out var argsAreLit); - Expr result = new Boogie.NAryExpr(GetToken(e), new Boogie.FunctionCall(id), args); - result = BoogieGenerator.CondApplyUnbox(GetToken(e), result, e.Function.ResultType, e.Type); + var args = FunctionInvocationArguments(e, layerArgument, revealArgument, false, out var argsAreLit); + Expr result = new Boogie.NAryExpr(GetToken(e), new Boogie.FunctionCall(id), args); + result = BoogieGenerator.CondApplyUnbox(GetToken(e), result, e.Function.ResultType, e.Type); - bool callIsLit = argsAreLit - && BoogieGenerator.FunctionBodyIsAvailable(e.Function, BoogieGenerator.currentModule, BoogieGenerator.currentScope) - && !e.Function.Reads.Expressions.Any(); // Function could depend on external values - if (callIsLit) { - result = MaybeLit(result, ty); - } + bool callIsLit = argsAreLit + && BoogieGenerator.FunctionBodyIsAvailable(e.Function, BoogieGenerator.currentModule, BoogieGenerator.currentScope) + && !e.Function.Reads.Expressions.Any(); // Function could depend on external values + if (callIsLit) { + result = MaybeLit(result, ty); + } - return result; - } - } - case DatatypeValue value: { - DatatypeValue dtv = value; - Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved - List args = []; - - bool argsAreLit = true; - for (int i = 0; i < dtv.Arguments.Count; i++) { - Expression arg = dtv.Arguments[i]; - Type t = dtv.Ctor.Formals[i].Type; - var bArg = TrExpr(arg); - argsAreLit = argsAreLit && BoogieGenerator.IsLit(bArg); - args.Add(BoogieGenerator.AdaptBoxing(GetToken(value), bArg, cce.NonNull(arg.Type), t)); - } - Boogie.IdentifierExpr id = new Boogie.IdentifierExpr(GetToken(dtv), dtv.Ctor.FullName, Predef.DatatypeType); - Boogie.Expr ret = new Boogie.NAryExpr(GetToken(dtv), new Boogie.FunctionCall(id), args); - if (argsAreLit) { - // If all arguments are Lit, so is the whole expression - ret = MaybeLit(ret, Predef.DatatypeType); - } - return ret; - } - case SeqConstructionExpr constructionExpr: { - var e = constructionExpr; - var eType = e.Type.NormalizeToAncestorType().AsSeqType.Arg.NormalizeExpand(); - var initalizerHeap = e.Initializer.Type.IsArrowType ? HeapExprForArrow(e.Initializer.Type) : HeapExpr; - return FunctionCall(GetToken(constructionExpr), "Seq#Create", Predef.SeqType, - BoogieGenerator.TypeToTy(eType), - initalizerHeap, - TrExpr(e.N), - TrExpr(e.Initializer)); - } - case MultiSetFormingExpr formingExpr: { - MultiSetFormingExpr e = formingExpr; - var eType = e.E.Type.NormalizeToAncestorType(); - if (eType is SetType setType) { - return BoogieGenerator.FunctionCall(GetToken(formingExpr), BuiltinFunction.MultiSetFromSet, BoogieGenerator.TrType(setType.Arg), TrExpr(e.E)); - } else if (eType is SeqType seqType) { - return BoogieGenerator.FunctionCall(GetToken(formingExpr), BuiltinFunction.MultiSetFromSeq, BoogieGenerator.TrType(seqType.Arg), TrExpr(e.E)); - } else { - Contract.Assert(false); throw new cce.UnreachableException(); - } - } - case OldExpr oldExpr: { - var e = oldExpr; - return OldAt(e.AtLabel).TrExpr(e.Expr); - } - case UnchangedExpr unchangedExpr: { - var e = unchangedExpr; - return BoogieGenerator.FrameCondition(GetToken(e), e.Frame, false, FrameExpressionUse.Unchanged, OldAt(e.AtLabel), this, this, true); - } - case UnaryOpExpr opExpr: { - var e = opExpr; - Boogie.Expr arg = TrExpr(e.E); - switch (e.ResolvedOp) { - case UnaryOpExpr.ResolvedOpcode.Lit: - return MaybeLit(arg); - case UnaryOpExpr.ResolvedOpcode.BVNot: - var bvWidth = opExpr.Type.NormalizeToAncestorType().AsBitVectorType.Width; - var bvType = BoogieGenerator.BplBvType(bvWidth); - Boogie.Expr r = FunctionCall(GetToken(opExpr), "not_bv" + bvWidth, bvType, arg); - if (BoogieGenerator.IsLit(arg)) { - r = MaybeLit(r, bvType); - } - return r; - case UnaryOpExpr.ResolvedOpcode.BoolNot: - return Boogie.Expr.Unary(GetToken(opExpr), UnaryOperator.Opcode.Not, arg); - case UnaryOpExpr.ResolvedOpcode.SeqLength: - Contract.Assert(e.E.Type.NormalizeToAncestorType() is SeqType); - return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.SeqLength, null, arg); - case UnaryOpExpr.ResolvedOpcode.SetCard: - Contract.Assert(e.E.Type.NormalizeToAncestorType() is SetType { Finite: true }); - return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.SetCard, null, arg); - case UnaryOpExpr.ResolvedOpcode.MultiSetCard: - Contract.Assert(e.E.Type.NormalizeToAncestorType() is MultiSetType); - return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.MultiSetCard, null, arg); - case UnaryOpExpr.ResolvedOpcode.MapCard: - Contract.Assert(e.E.Type.NormalizeToAncestorType() is MapType { Finite: true }); - return BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.MapCard, null, arg); - case UnaryOpExpr.ResolvedOpcode.Fresh: - var freshLabel = ((FreshExpr)e).AtLabel; - var eeType = e.E.Type.NormalizeToAncestorType(); - if (eeType is SetType setType) { - // generate: (forall $o: ref :: { $o != null } X[Box($o)] ==> $o != null) && - // (forall $o: ref :: { X[Box($o)] } X[Box($o)] ==> !old($Heap)[$o,alloc]) - // OR, if X[Box($o)] is rewritten into smaller parts, use the less good trigger old($Heap)[$o,alloc] - Boogie.Variable oVar = new Boogie.BoundVariable(GetToken(opExpr), new Boogie.TypedIdent(GetToken(opExpr), "$o", Predef.RefType)); - Boogie.Expr o = new Boogie.IdentifierExpr(GetToken(opExpr), oVar); - Boogie.Expr oNotNull = Boogie.Expr.Neq(o, Predef.Null); - Boogie.Expr oInSet = TrInSet(GetToken(opExpr), o, e.E, setType.Arg, setType.Finite, true, out var performedInSetRewrite); - Boogie.Expr oNotFresh = OldAt(freshLabel).IsAlloced(GetToken(opExpr), o); - Boogie.Expr oIsFresh = Boogie.Expr.Not(oNotFresh); - Boogie.Expr notNullBody = BplImp(oInSet, oNotNull); - Boogie.Expr freshBody = BplImp(oInSet, oIsFresh); - var notNullTrigger = BplTrigger(oNotNull); - var notNullPred = new Boogie.ForallExpr(GetToken(opExpr), [oVar], notNullTrigger, notNullBody); - var freshTrigger = BplTrigger(performedInSetRewrite ? oNotFresh : oInSet); - var freshPred = new Boogie.ForallExpr(GetToken(opExpr), [oVar], freshTrigger, freshBody); - return BplAnd(notNullPred, freshPred); - } else if (eeType is SeqType) { - // generate: (forall $i: int :: 0 <= $i && $i < Seq#Length(X) ==> Unbox(Seq#Index(X,$i)) != null && !old($Heap)[Unbox(Seq#Index(X,$i)),alloc]) - Boogie.Variable iVar = new Boogie.BoundVariable(GetToken(opExpr), new Boogie.TypedIdent(GetToken(opExpr), "$i", Boogie.Type.Int)); - Boogie.Expr i = new Boogie.IdentifierExpr(GetToken(opExpr), iVar); - Boogie.Expr iBounds = BoogieGenerator.InSeqRange(GetToken(opExpr), i, Type.Int, TrExpr(e.E), true, null, false); - Boogie.Expr XsubI = BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.SeqIndex, Predef.RefType, TrExpr(e.E), i); - XsubI = BoogieGenerator.FunctionCall(GetToken(opExpr), BuiltinFunction.Unbox, Predef.RefType, XsubI); - Boogie.Expr oNotFresh = OldAt(freshLabel).IsAlloced(GetToken(opExpr), XsubI); - Boogie.Expr oIsFresh = Boogie.Expr.Not(oNotFresh); - Boogie.Expr xsubiNotNull = Boogie.Expr.Neq(XsubI, Predef.Null); - Boogie.Expr body = BplImp(iBounds, BplAnd(xsubiNotNull, oIsFresh)); - //TRIGGERS: Does this make sense? dafny0\SmallTests - // BROKEN // NEW_TRIGGER - //TRIG (forall $i: int :: 0 <= $i && $i < Seq#Length(Q#0) && $Unbox(Seq#Index(Q#0, $i)): ref != null ==> !read(old($Heap), $Unbox(Seq#Index(Q#0, $i)): ref, alloc)) - return new Boogie.ForallExpr(GetToken(opExpr), [iVar], body); - } else { - // generate: x != null && !old($Heap)[x] - Boogie.Expr oNull = Boogie.Expr.Neq(TrExpr(e.E), Predef.Null); - Boogie.Expr oIsFresh = Boogie.Expr.Not(OldAt(freshLabel).IsAlloced(GetToken(opExpr), TrExpr(e.E))); - return Boogie.Expr.Binary(GetToken(opExpr), BinaryOperator.Opcode.And, oNull, oIsFresh); - } - case UnaryOpExpr.ResolvedOpcode.Allocated: - // Translate with $IsAllocBox, even if it requires boxing the argument. This has the effect of giving - // both the $IsAllocBox and $IsAlloc forms, because the axioms that connects these two is triggered - // by $IsAllocBox. - return BoogieGenerator.MkIsAllocBox(BoxIfNecessary(e.E.Origin, TrExpr(e.E), e.E.Type), e.E.Type, HeapExpr); - case UnaryOpExpr.ResolvedOpcode.Assigned: - string name = null; - switch (e.E.Resolved) { - case IdentifierExpr ie: - name = ie.Var.UniqueName; - break; - case MemberSelectExpr mse: - if (BoogieGenerator.inBodyInitContext && Expression.AsThis(mse.Obj) != null) { - name = BoogieGenerator.SurrogateName(mse.Member as Field); - } - break; - } - - if (name == null) { - return Expr.True; - } - BoogieGenerator.DefiniteAssignmentTrackers.TryGetValue(name, out var defass); - return defass; - default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression - } - } - case ConversionExpr conversionExpr: { - var e = conversionExpr; - return BoogieGenerator.ConvertExpression(GetToken(e), TrExpr(e.E), e.E.Type, e.ToType); - } - case TypeTestExpr testExpr: { - var e = testExpr; - return BoogieGenerator.GetSubrangeCheck(e.Origin, TrExpr(e.E), e.E.Type, e.ToType, e.E, null, out var _) ?? Boogie.Expr.True; - } - case BinaryExpr binaryExpr: { - BinaryExpr e = binaryExpr; - var e0Type = e.E0.Type.NormalizeToAncestorType(); // used when making decisions about what Boogie operator/functions to use - bool isReal = e0Type.IsNumericBased(Type.NumericPersuasion.Real); - int bvWidth = e0Type.IsBitVectorType ? e0Type.AsBitVectorType.Width : -1; // -1 indicates "not a bitvector type" - Boogie.Expr e0 = TrExpr(e.E0); - if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) { - return TrInSet(GetToken(binaryExpr), e0, e.E1, e.E0.Type, e.E1.Type.NormalizeToAncestorType().AsSetType.Finite, false, out var pr); // let TrInSet translate e.E1 - } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSet) { - Boogie.Expr arg = TrInSet(GetToken(binaryExpr), e0, e.E1, e.E0.Type, e.E1.Type.NormalizeToAncestorType().AsSetType.Finite, false, out var pr); // let TrInSet translate e.E1 - return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, arg); - } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) { - return TrInMultiSet(GetToken(binaryExpr), e0, e.E1, e.E0.Type, false); // let TrInMultiSet translate e.E1 - } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInMultiSet) { - Boogie.Expr arg = TrInMultiSet(GetToken(binaryExpr), e0, e.E1, e.E0.Type, false); // let TrInMultiSet translate e.E1 - return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, arg); - } - Boogie.Expr e1 = TrExpr(e.E1); - BinaryOperator.Opcode bOpcode; - Boogie.Type typ; - var oe0 = e0; - var oe1 = e1; - var lit0 = BoogieGenerator.GetLit(e0); - var lit1 = BoogieGenerator.GetLit(e1); - bool liftLit = BoogieGenerator.IsLit(e0) && BoogieGenerator.IsLit(e1); - // NOTE(namin): We usually avoid keeping literals, because their presence might mess up triggers that do not expect them. - // Still for equality-related operations, it's useful to keep them instead of lifting them, so that they can be propagated. - bool keepLits = false; - if (lit0 != null) { - e0 = lit0; - } - if (lit1 != null) { - e1 = lit1; - } - switch (e.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.Iff: - typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Iff; break; - case BinaryExpr.ResolvedOpcode.Imp: - typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Imp; break; - case BinaryExpr.ResolvedOpcode.And: - typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.And; break; - case BinaryExpr.ResolvedOpcode.Or: - typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Or; break; - - case BinaryExpr.ResolvedOpcode.EqCommon: - keepLits = true; - if (ModeledAsBoxType(e.E0.Type)) { - e1 = BoxIfNecessary(expr.Origin, e1, e.E1.Type); - oe1 = BoxIfNecessary(expr.Origin, oe1, e.E1.Type); - } else if (ModeledAsBoxType(e.E1.Type)) { - e0 = BoxIfNecessary(expr.Origin, e0, e.E0.Type); - oe0 = BoxIfNecessary(expr.Origin, oe0, e.E0.Type); - } - if (e.E0.Type.IsCoDatatype && e.E1.Type.IsCoDatatype) { - var e0args = e.E0.Type.NormalizeExpand().TypeArgs; - var e1args = e.E1.Type.NormalizeExpand().TypeArgs; - return BoogieGenerator.CoEqualCall(e.E0.Type.AsCoDatatype, e0args, e1args, null, - this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr)); - } - if (e.E0.Type.IsIndDatatype && e.E1.Type.IsIndDatatype) { - return BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), e.E0.Type, e0, e1); - } - typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Eq; - break; - case BinaryExpr.ResolvedOpcode.NeqCommon: - if (ModeledAsBoxType(e.E0.Type)) { - e1 = BoxIfNecessary(expr.Origin, e1, e.E1.Type); - oe1 = BoxIfNecessary(expr.Origin, oe1, e.E1.Type); - } else if (ModeledAsBoxType(e.E1.Type)) { - e0 = BoxIfNecessary(expr.Origin, e0, e.E0.Type); - oe0 = BoxIfNecessary(expr.Origin, oe0, e.E0.Type); - } - if (e.E0.Type.IsCoDatatype && e.E1.Type.IsCoDatatype) { - var e0args = e.E0.Type.NormalizeExpand().TypeArgs; - var e1args = e.E1.Type.NormalizeExpand().TypeArgs; - var eq = BoogieGenerator.CoEqualCall(e.E0.Type.AsCoDatatype, e0args, e1args, null, - this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr)); - return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, eq); - } - if (e.E0.Type.IsIndDatatype && e.E1.Type.IsIndDatatype) { - var eq = BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), e.E0.Type, e0, e1); - return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, eq); - } - typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Neq; - break; - case BinaryExpr.ResolvedOpcode.Lt: - if (0 <= bvWidth) { - return TrToFunctionCall(GetToken(binaryExpr), "lt_bv" + bvWidth, Boogie.Type.Bool, e0, e1, liftLit); - } else if (e0Type.IsBigOrdinalType) { - return FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e0, e1); - } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) { - typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Lt; - break; - } else { - return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_lt_boogie", Boogie.Type.Bool, e0, e1, liftLit); - } - case BinaryExpr.ResolvedOpcode.LessThanLimit: - return FunctionCall(GetToken(binaryExpr), "ORD#LessThanLimit", Boogie.Type.Bool, e0, e1); - case BinaryExpr.ResolvedOpcode.Le: - keepLits = true; - if (0 <= bvWidth) { - return TrToFunctionCall(GetToken(binaryExpr), "le_bv" + bvWidth, Boogie.Type.Bool, e0, e1, false); - } else if (e0Type.IsBigOrdinalType) { - var less = FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e0, e1); - var eq = Boogie.Expr.Eq(e0, e1); - return BplOr(eq, less); - } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) { - typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Le; - break; - } else { - return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_le_boogie", Boogie.Type.Bool, e0, e1, false); - } - case BinaryExpr.ResolvedOpcode.Ge: - keepLits = true; - if (0 <= bvWidth) { - return TrToFunctionCall(GetToken(binaryExpr), "ge_bv" + bvWidth, Boogie.Type.Bool, e0, e1, false); - } else if (e0Type.IsBigOrdinalType) { - var less = FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e1, e0); - var eq = Boogie.Expr.Eq(e1, e0); - return BplOr(eq, less); - } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) { - typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Ge; - break; - } else { - return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_ge_boogie", Boogie.Type.Bool, e0, e1, false); - } - case BinaryExpr.ResolvedOpcode.Gt: - if (0 <= bvWidth) { - return TrToFunctionCall(GetToken(binaryExpr), "gt_bv" + bvWidth, Boogie.Type.Bool, e0, e1, liftLit); - } else if (e0Type.IsBigOrdinalType) { - return FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e1, e0); - } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) { - typ = Boogie.Type.Bool; - bOpcode = BinaryOperator.Opcode.Gt; - break; - } else { - return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_gt_boogie", Boogie.Type.Bool, e0, e1, liftLit); - } - - case BinaryExpr.ResolvedOpcode.Add: - if (0 <= bvWidth) { - return TrToFunctionCall(GetToken(binaryExpr), "add_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); - } else if (e0Type.IsBigOrdinalType) { - return TrToFunctionCall(GetToken(binaryExpr), "ORD#Plus", Predef.BigOrdinalType, e0, e1, liftLit); - } else if (e0Type.IsCharType) { - return TrToFunctionCall(GetToken(binaryExpr), "char#Plus", Predef.CharType, e0, e1, liftLit); - } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic) { - return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_add_boogie", Boogie.Type.Int, e0, e1, liftLit); - } else if (!isReal && (options.ArithMode == 2 || 5 <= options.ArithMode)) { - return TrToFunctionCall(GetToken(binaryExpr), "Add", Boogie.Type.Int, oe0, oe1, liftLit); - } else { - typ = isReal ? Boogie.Type.Real : Boogie.Type.Int; - bOpcode = BinaryOperator.Opcode.Add; - break; - } - case BinaryExpr.ResolvedOpcode.Sub: - if (0 <= bvWidth) { - return TrToFunctionCall(GetToken(binaryExpr), "sub_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); - } else if (e0Type.IsBigOrdinalType) { - return TrToFunctionCall(GetToken(binaryExpr), "ORD#Minus", Predef.BigOrdinalType, e0, e1, liftLit); - } else if (e0Type.IsCharType) { - return TrToFunctionCall(GetToken(binaryExpr), "char#Minus", Predef.CharType, e0, e1, liftLit); - } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic) { - return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_sub_boogie", Boogie.Type.Int, e0, e1, liftLit); - } else if (!isReal && (options.ArithMode == 2 || 5 <= options.ArithMode)) { - return TrToFunctionCall(GetToken(binaryExpr), "Sub", Boogie.Type.Int, oe0, oe1, liftLit); - } else { - typ = isReal ? Boogie.Type.Real : Boogie.Type.Int; - bOpcode = BinaryOperator.Opcode.Sub; - break; - } - case BinaryExpr.ResolvedOpcode.Mul: - if (0 <= bvWidth) { - return TrToFunctionCall(GetToken(binaryExpr), "mul_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); - } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic) { - return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_mul_boogie", Boogie.Type.Int, e0, e1, liftLit); - } else if (!isReal && options.ArithMode != 0 && options.ArithMode != 3) { - return TrToFunctionCall(GetToken(binaryExpr), "Mul", Boogie.Type.Int, oe0, oe1, liftLit); - } else { - typ = isReal ? Boogie.Type.Real : Boogie.Type.Int; - bOpcode = BinaryOperator.Opcode.Mul; - break; - } - case BinaryExpr.ResolvedOpcode.Div: - if (0 <= bvWidth) { - return TrToFunctionCall(GetToken(binaryExpr), "div_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); - } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic && !isReal) { - return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_div_boogie", Boogie.Type.Int, e0, e1, liftLit); - } else if (!isReal && options.ArithMode != 0 && options.ArithMode != 3) { - return TrToFunctionCall(GetToken(binaryExpr), "Div", Boogie.Type.Int, e0, oe1, liftLit); - } else if (isReal) { - typ = Boogie.Type.Real; - bOpcode = BinaryOperator.Opcode.RealDiv; - break; - } else { - typ = Boogie.Type.Int; - bOpcode = BinaryOperator.Opcode.Div; - break; - } - case BinaryExpr.ResolvedOpcode.Mod: - if (0 <= bvWidth) { - return TrToFunctionCall(GetToken(binaryExpr), "mod_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); - } else if (BoogieGenerator.DisableNonLinearArithmetic && !isReal) { - return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_mod_boogie", Boogie.Type.Int, e0, e1, liftLit); - } else if (!isReal && options.ArithMode != 0 && options.ArithMode != 3) { - return TrToFunctionCall(GetToken(binaryExpr), "Mod", Boogie.Type.Int, e0, oe1, liftLit); - } else { - typ = isReal ? Boogie.Type.Real : Boogie.Type.Int; - bOpcode = BinaryOperator.Opcode.Mod; - break; - } - - case BinaryExpr.ResolvedOpcode.LeftShift: { - Contract.Assert(0 <= bvWidth); - return TrToFunctionCall(GetToken(binaryExpr), "LeftShift_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, BoogieGenerator.ConvertExpression(GetToken(binaryExpr), e1, e.E1.Type, e.Type), liftLit); - } - case BinaryExpr.ResolvedOpcode.RightShift: { - Contract.Assert(0 <= bvWidth); - return TrToFunctionCall(GetToken(binaryExpr), "RightShift_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, BoogieGenerator.ConvertExpression(GetToken(binaryExpr), e1, e.E1.Type, e.Type), liftLit); - } - case BinaryExpr.ResolvedOpcode.BitwiseAnd: { - Contract.Assert(0 <= bvWidth); - return TrToFunctionCall(GetToken(binaryExpr), "and_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); - } - case BinaryExpr.ResolvedOpcode.BitwiseOr: { - Contract.Assert(0 <= bvWidth); - return TrToFunctionCall(GetToken(binaryExpr), "or_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); - } - case BinaryExpr.ResolvedOpcode.BitwiseXor: { - Contract.Assert(0 <= bvWidth); - return TrToFunctionCall(GetToken(binaryExpr), "xor_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); - } - - case BinaryExpr.ResolvedOpcode.LtChar: - case BinaryExpr.ResolvedOpcode.LeChar: - case BinaryExpr.ResolvedOpcode.GeChar: - case BinaryExpr.ResolvedOpcode.GtChar: { - // work off the original operands (that is, allow them to be lit-wrapped) - var operand0 = BoogieGenerator.FunctionCall(e0.tok, BuiltinFunction.CharToInt, null, oe0); - var operand1 = BoogieGenerator.FunctionCall(e0.tok, BuiltinFunction.CharToInt, null, oe1); - BinaryOperator.Opcode bOp; - switch (e.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.LtChar: bOp = BinaryOperator.Opcode.Lt; break; - case BinaryExpr.ResolvedOpcode.LeChar: bOp = BinaryOperator.Opcode.Le; break; - case BinaryExpr.ResolvedOpcode.GeChar: bOp = BinaryOperator.Opcode.Ge; break; - case BinaryExpr.ResolvedOpcode.GtChar: bOp = BinaryOperator.Opcode.Gt; break; - default: - Contract.Assert(false); // unexpected case - throw new cce.UnreachableException(); // to please compiler - } - return Boogie.Expr.Binary(GetToken(binaryExpr), bOp, operand0, operand1); - } - - case BinaryExpr.ResolvedOpcode.SetEq: - case BinaryExpr.ResolvedOpcode.MultiSetEq: - case BinaryExpr.ResolvedOpcode.SeqEq: - case BinaryExpr.ResolvedOpcode.MapEq: - return BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), e.E0.Type, e0, e1); - case BinaryExpr.ResolvedOpcode.SetNeq: - case BinaryExpr.ResolvedOpcode.MultiSetNeq: - case BinaryExpr.ResolvedOpcode.SeqNeq: - case BinaryExpr.ResolvedOpcode.MapNeq: - return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), e.E0.Type, e0, e1)); - - case BinaryExpr.ResolvedOpcode.ProperSubset: { - return BoogieGenerator.ProperSubset(GetToken(binaryExpr), e0, e1, e.E0.Type.NormalizeToAncestorType().AsSetType.Finite); - } - case BinaryExpr.ResolvedOpcode.Subset: { - bool finite = e.E1.Type.NormalizeToAncestorType().AsSetType.Finite; - var f = finite ? BuiltinFunction.SetSubset : BuiltinFunction.ISetSubset; - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, null, e0, e1); - } - case BinaryExpr.ResolvedOpcode.Superset: { - bool finite = e.E1.Type.NormalizeToAncestorType().AsSetType.Finite; - var f = finite ? BuiltinFunction.SetSubset : BuiltinFunction.ISetSubset; - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, null, e1, e0); - } - case BinaryExpr.ResolvedOpcode.ProperSuperset: - return BoogieGenerator.ProperSubset(GetToken(binaryExpr), e1, e0, e.E0.Type.NormalizeToAncestorType().AsSetType.Finite); - case BinaryExpr.ResolvedOpcode.Disjoint: { - bool finite = e.E1.Type.NormalizeToAncestorType().AsSetType.Finite; - var f = finite ? BuiltinFunction.SetDisjoint : BuiltinFunction.ISetDisjoint; - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, null, e0, e1); - } - case BinaryExpr.ResolvedOpcode.InSet: - Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above - case BinaryExpr.ResolvedOpcode.NotInSet: - Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above - case BinaryExpr.ResolvedOpcode.Union: { - var setType = binaryExpr.Type.NormalizeToAncestorType().AsSetType; - bool finite = setType.Finite; - var f = finite ? BuiltinFunction.SetUnion : BuiltinFunction.ISetUnion; - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, BoogieGenerator.TrType(setType.Arg), e0, e1); - } - case BinaryExpr.ResolvedOpcode.Intersection: { - var setType = binaryExpr.Type.NormalizeToAncestorType().AsSetType; - bool finite = setType.Finite; - var f = finite ? BuiltinFunction.SetIntersection : BuiltinFunction.ISetIntersection; - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, BoogieGenerator.TrType(setType.Arg), e0, e1); - } - case BinaryExpr.ResolvedOpcode.SetDifference: { - var setType = binaryExpr.Type.NormalizeToAncestorType().AsSetType; - bool finite = setType.Finite; - var f = finite ? BuiltinFunction.SetDifference : BuiltinFunction.ISetDifference; - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, BoogieGenerator.TrType(setType.Arg), e0, e1); - } - case BinaryExpr.ResolvedOpcode.ProperMultiSubset: - return BoogieGenerator.ProperMultiset(GetToken(binaryExpr), e0, e1); - case BinaryExpr.ResolvedOpcode.MultiSubset: - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetSubset, null, e0, e1); - case BinaryExpr.ResolvedOpcode.MultiSuperset: - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetSubset, null, e1, e0); - case BinaryExpr.ResolvedOpcode.ProperMultiSuperset: - return BoogieGenerator.ProperMultiset(GetToken(binaryExpr), e1, e0); - case BinaryExpr.ResolvedOpcode.MultiSetDisjoint: - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetDisjoint, null, e0, e1); - case BinaryExpr.ResolvedOpcode.InMultiSet: - Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above - case BinaryExpr.ResolvedOpcode.NotInMultiSet: - Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above - case BinaryExpr.ResolvedOpcode.MultiSetUnion: - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetUnion, - BoogieGenerator.TrType(binaryExpr.Type.NormalizeToAncestorType().AsMultiSetType.Arg), e0, e1); - case BinaryExpr.ResolvedOpcode.MultiSetIntersection: - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetIntersection, - BoogieGenerator.TrType(binaryExpr.Type.NormalizeToAncestorType().AsMultiSetType.Arg), e0, e1); - case BinaryExpr.ResolvedOpcode.MultiSetDifference: - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetDifference, - BoogieGenerator.TrType(binaryExpr.Type.NormalizeToAncestorType().AsMultiSetType.Arg), e0, e1); - - case BinaryExpr.ResolvedOpcode.ProperPrefix: - return BoogieGenerator.ProperPrefix(GetToken(binaryExpr), e0, e1); - case BinaryExpr.ResolvedOpcode.Prefix: { - Boogie.Expr len0 = BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqLength, null, e0); - Boogie.Expr len1 = BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqLength, null, e1); - return Boogie.Expr.Binary(GetToken(binaryExpr), BinaryOperator.Opcode.And, - Boogie.Expr.Le(len0, len1), - BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqSameUntil, null, e0, e1, len0)); - } - case BinaryExpr.ResolvedOpcode.Concat: - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqAppend, - BoogieGenerator.TrType(binaryExpr.Type.NormalizeToAncestorType().AsSeqType.Arg), e0, e1); - case BinaryExpr.ResolvedOpcode.InSeq: - return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqContains, null, e1, - BoxIfNecessary(GetToken(binaryExpr), e0, e.E0.Type)); - case BinaryExpr.ResolvedOpcode.NotInSeq: - Boogie.Expr arg = BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqContains, null, e1, - BoxIfNecessary(GetToken(binaryExpr), e0, e.E0.Type)); - return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, arg); - case BinaryExpr.ResolvedOpcode.InMap: { - bool finite = e.E1.Type.NormalizeToAncestorType().AsMapType.Finite; - var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain; - return BoogieGenerator.IsSetMember(GetToken(binaryExpr), - BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, finite ? Predef.MapType : Predef.IMapType, e1), - BoxIfNecessary(GetToken(binaryExpr), e0, e.E0.Type), - finite); - } - case BinaryExpr.ResolvedOpcode.NotInMap: { - bool finite = e.E1.Type.NormalizeToAncestorType().AsMapType.Finite; - var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain; - Boogie.Expr inMap = BoogieGenerator.IsSetMember(GetToken(binaryExpr), - BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, finite ? Predef.MapType : Predef.IMapType, e1), - BoxIfNecessary(GetToken(binaryExpr), e0, e.E0.Type), - finite); - return Boogie.Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, inMap); - } - case BinaryExpr.ResolvedOpcode.MapMerge: { - bool finite = e0Type.NormalizeToAncestorType().AsMapType.Finite; - var f = finite ? "Map#Merge" : "IMap#Merge"; - return FunctionCall(GetToken(binaryExpr), f, BoogieGenerator.TrType(binaryExpr.Type), e0, e1); - } - case BinaryExpr.ResolvedOpcode.MapSubtraction: { - bool finite = e0Type.NormalizeToAncestorType().AsMapType.Finite; - var f = finite ? "Map#Subtract" : "IMap#Subtract"; - return FunctionCall(GetToken(binaryExpr), f, BoogieGenerator.TrType(binaryExpr.Type), e0, e1); - } - - case BinaryExpr.ResolvedOpcode.RankLt: - return Boogie.Expr.Binary(GetToken(binaryExpr), BinaryOperator.Opcode.Lt, - BoogieGenerator.FunctionCall(GetToken(binaryExpr), e0Type.IsDatatype ? BuiltinFunction.DtRank : BuiltinFunction.BoxRank, null, e0), - BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.DtRank, null, e1)); - case BinaryExpr.ResolvedOpcode.RankGt: - return Boogie.Expr.Binary(GetToken(binaryExpr), BinaryOperator.Opcode.Gt, - BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.DtRank, null, e0), - BoogieGenerator.FunctionCall(GetToken(binaryExpr), e.E1.Type.IsDatatype ? BuiltinFunction.DtRank : BuiltinFunction.BoxRank, null, e1)); - - default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected binary expression - } - liftLit = liftLit && !keepLits; - var ae0 = keepLits ? oe0 : e0; - var ae1 = keepLits ? oe1 : e1; - Boogie.Expr re = Boogie.Expr.Binary(GetToken(binaryExpr), bOpcode, ae0, ae1); - if (liftLit) { - re = MaybeLit(re, typ); - } - return re; - } - case TernaryExpr ternaryExpr: { - var e = ternaryExpr; - var e0 = TrExpr(e.E0); - if (!e.E0.Type.IsBigOrdinalType) { - e0 = FunctionCall(e0.tok, "ORD#FromNat", Predef.BigOrdinalType, e0); - } - var e1 = TrExpr(e.E1); - var e2 = TrExpr(e.E2); - switch (e.Op) { - case TernaryExpr.Opcode.PrefixEqOp: - case TernaryExpr.Opcode.PrefixNeqOp: - var e1type = e.E1.Type.NormalizeExpand(); - var e2type = e.E2.Type.NormalizeExpand(); - var cot = e1type.AsCoDatatype; - Contract.Assert(cot != null); // the argument types of prefix equality (and prefix disequality) are codatatypes - var r = BoogieGenerator.CoEqualCall(cot, e1type.TypeArgs, e2type.TypeArgs, e0, this.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e1, e2); - if (e.Op == TernaryExpr.Opcode.PrefixEqOp) { - return r; - } else { - return Boogie.Expr.Unary(GetToken(ternaryExpr), UnaryOperator.Opcode.Not, r); - } - default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression - } - } - case LetExpr letExpr: - return TrLetExpr(letExpr); - case QuantifierExpr quantifierExpr: { - QuantifierExpr e = quantifierExpr; + return result; + } + } - if (e.SplitQuantifier != null) { - return TrExpr(e.SplitQuantifierExpression); - } else { - List bvars = []; - var bodyEtran = this; - if (e is ExistsExpr && BoogieGenerator.stmtContext == StmtType.ASSERT && BoogieGenerator.adjustFuelForExists) { - // assert exists need decrease fuel by 1 - bodyEtran = bodyEtran.DecreaseFuel(1); - // set adjustFuelForExists to false so that we don't keep decrease the fuel in cases like the expr below. - // assert exists p:int :: exists t:T :: ToInt(t) > 0; - BoogieGenerator.adjustFuelForExists = false; - } else if (e is ExistsExpr && BoogieGenerator.stmtContext == StmtType.ASSUME && BoogieGenerator.adjustFuelForExists) { - // assume exists need increase fuel by 1 - bodyEtran = bodyEtran.LayerOffset(1); - BoogieGenerator.adjustFuelForExists = false; - } + private Expr TranslateLiteralExpr(LiteralExpr literalExpr) { + LiteralExpr e = literalExpr; + if (e.Value == null) { + return Predef.Null; + } else if (e.Value is bool) { + return MaybeLit(new Boogie.LiteralExpr(GetToken(e), (bool)e.Value)); + } else if (e is CharLiteralExpr) { + // we expect e.Value to be a string representing exactly one char + Boogie.Expr rawElement = null; // assignment to please compiler's definite assignment rule + foreach (var ch in Util.UnescapedCharacters(options, (string)e.Value, false)) { + Contract.Assert(rawElement == null); // we should get here only once + rawElement = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.CharFromInt, null, Boogie.Expr.Literal(ch)); + } + Contract.Assert(rawElement != null); // there should have been an iteration of the loop above + return MaybeLit(rawElement, Predef.CharType); + } else if (e is StringLiteralExpr) { + var str = (StringLiteralExpr)e; + Boogie.Expr seq = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.SeqEmpty, Predef.BoxType); + foreach (var ch in Util.UnescapedCharacters(options, (string)e.Value, str.IsVerbatim)) { + var rawElement = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.CharFromInt, null, Boogie.Expr.Literal(ch)); + Boogie.Expr elt = BoxIfNecessary(GetToken(literalExpr), rawElement, Type.Char); + seq = BoogieGenerator.FunctionCall(GetToken(literalExpr), BuiltinFunction.SeqBuild, Predef.BoxType, seq, elt); + } + return MaybeLit(seq, BoogieGenerator.TrType(new SeqType(Type.Char))); + } else if (e.Value is BigInteger) { + var n = Microsoft.BaseTypes.BigNum.FromBigInt((BigInteger)e.Value); + if (e.Type.NormalizeToAncestorType() is BitvectorType bitvectorType) { + return MaybeLit(BoogieGenerator.BplBvLiteralExpr(GetToken(e), n, bitvectorType)); + } else if (e.Type.IsBigOrdinalType) { + var fromNat = FunctionCall(GetToken(literalExpr), "ORD#FromNat", Predef.BigOrdinalType, Boogie.Expr.Literal(n)); + return MaybeLit(fromNat, Predef.BigOrdinalType); + } else { + return MaybeLit(Boogie.Expr.Literal(n)); + } + } else if (e.Value is BaseTypes.BigDec) { + return MaybeLit(Boogie.Expr.Literal((BaseTypes.BigDec)e.Value)); + } else { + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal + } + } - Boogie.Expr antecedent = Boogie.Expr.True; + private Expr TranslateSeqDisplayExpr(SeqDisplayExpr displayExpr) { + SeqDisplayExpr e = displayExpr; + // Note: a LiteralExpr(string) is really another kind of SeqDisplayExpr + Boogie.Expr s = BoogieGenerator.FunctionCall(GetToken(displayExpr), BuiltinFunction.SeqEmpty, Predef.BoxType); + var isLit = true; + foreach (Expression ee in e.Elements) { + var rawElement = TrExpr(ee); + isLit = isLit && BoogieGenerator.IsLit(rawElement); + Boogie.Expr elt = BoxIfNecessary(GetToken(displayExpr), rawElement, ee.Type); + s = BoogieGenerator.FunctionCall(GetToken(displayExpr), BuiltinFunction.SeqBuild, Predef.BoxType, s, elt); + } + if (isLit) { + // Lit-lifting: All elements are lit, so the sequence is Lit too + s = MaybeLit(s, Predef.BoxType); + } + return s; + } + + private Expr TranslateSeqSelectExpr(SeqSelectExpr selectExpr) { + SeqSelectExpr e = selectExpr; + Boogie.Expr seq = TrExpr(e.Seq); + var seqType = e.Seq.Type.NormalizeToAncestorType(); + Type elmtType = null; + Type domainType = null; + Contract.Assert(seqType != null); // the expression has been successfully resolved + if (seqType.IsArrayType) { + domainType = Type.Int; + elmtType = UserDefinedType.ArrayElementType(seqType); + } else if (seqType is SeqType) { + domainType = Type.Int; + elmtType = ((SeqType)seqType).Arg; + } else if (seqType is MapType) { + domainType = ((MapType)seqType).Domain; + elmtType = ((MapType)seqType).Range; + } else if (seqType is MultiSetType) { + domainType = ((MultiSetType)seqType).Arg; + elmtType = Type.Int; + } else { Contract.Assert(false); } + Boogie.Type elType = BoogieGenerator.TrType(elmtType); + Boogie.Type dType = BoogieGenerator.TrType(domainType); + Boogie.Expr e0 = e.E0 == null ? null : TrExpr(e.E0); + if (e0 != null && e.E0.Type.IsBitVectorType) { + e0 = BoogieGenerator.ConvertExpression(GetToken(e.E0), e0, e.E0.Type, Type.Int); + } + Boogie.Expr e1 = e.E1 == null ? null : TrExpr(e.E1); + if (e1 != null && e.E1.Type.IsBitVectorType) { + e1 = BoogieGenerator.ConvertExpression(GetToken(e.E1), e1, e.E1.Type, Type.Int); + } + if (e.SelectOne) { + Contract.Assert(e1 == null); + Boogie.Expr x; + if (seqType.IsArrayType) { + Boogie.Expr fieldName = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.IndexField, null, e0); + x = BoogieGenerator.ReadHeap(GetToken(selectExpr), HeapExpr, TrExpr(e.Seq), fieldName); + } else if (seqType is SeqType) { + x = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.SeqIndex, Predef.BoxType, seq, e0); + } else if (seqType is MapType) { + bool finite = ((MapType)seqType).Finite; + var f = finite ? BuiltinFunction.MapElements : BuiltinFunction.IMapElements; + x = BoogieGenerator.FunctionCall(GetToken(selectExpr), f, finite ? Predef.MapType : Predef.IMapType, seq); + x = Boogie.Expr.Select(x, BoxIfNecessary(GetToken(e), e0, domainType)); + } else if (seqType is MultiSetType) { + x = BoogieGenerator.MultisetMultiplicity(GetToken(selectExpr), TrExpr(e.Seq), BoxIfNecessary(GetToken(selectExpr), e0, domainType)); + } else { Contract.Assert(false); x = null; } + if (!ModeledAsBoxType(elmtType) && !(seqType is MultiSetType)) { + x = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.Unbox, elType, x); + } + return x; + } else { + if (seqType.IsArrayType) { + seq = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.SeqFromArray, elType, HeapExpr, seq); + } + var isLit = BoogieGenerator.IsLit(seq); + if (e1 != null) { + isLit = isLit && BoogieGenerator.IsLit(e1); + seq = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.SeqTake, elType, seq, e1); + } + if (e0 != null) { + isLit = isLit && BoogieGenerator.IsLit(e0); + seq = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.SeqDrop, elType, seq, e0); + } + // if e0 == null && e1 == null, then we have the identity operation seq[..] == seq; + if (isLit && (e0 != null || e1 != null)) { + // Lit-lift the expression + seq = MaybeLit(seq, BoogieGenerator.TrType(selectExpr.Type)); + } + return seq; + } + } - List freeOfAlloc = BoundedPool.HasBounds(e.Bounds, BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc); - antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars, false, freeOfAlloc)); // initHeapForAllStmt + private Expr TranslateSeqUpdateExpr(SeqUpdateExpr updateExpr) { + SeqUpdateExpr e = updateExpr; + Boogie.Expr seq = TrExpr(e.Seq); + var seqType = e.Seq.Type.NormalizeToAncestorType(); + if (seqType is SeqType) { + Boogie.Expr index = TrExpr(e.Index); + index = BoogieGenerator.ConvertExpression(GetToken(e.Index), index, e.Index.Type, Type.Int); + Boogie.Expr val = BoxIfNecessary(GetToken(updateExpr), TrExpr(e.Value), e.Value.Type); + return BoogieGenerator.FunctionCall(GetToken(updateExpr), BuiltinFunction.SeqUpdate, Predef.BoxType, seq, index, val); + } else if (seqType is MapType) { + MapType mt = (MapType)seqType; + Boogie.Type maptype = mt.Finite ? Predef.MapType : Predef.IMapType; + Boogie.Expr index = BoxIfNecessary(GetToken(updateExpr), TrExpr(e.Index), mt.Domain); + Boogie.Expr val = BoxIfNecessary(GetToken(updateExpr), TrExpr(e.Value), mt.Range); + return FunctionCall(GetToken(updateExpr), mt.Finite ? "Map#Build" : "IMap#Build", maptype, seq, index, val); + } else if (seqType is MultiSetType) { + Type elmtType = cce.NonNull((MultiSetType)seqType).Arg; + Boogie.Expr index = BoxIfNecessary(GetToken(updateExpr), TrExpr(e.Index), elmtType); + Boogie.Expr val = TrExpr(e.Value); + return BoogieGenerator.UpdateMultisetMultiplicity(GetToken(updateExpr), seq, index, val); + } else { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } - Boogie.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); - Boogie.Trigger tr = BoogieGenerator.TrTrigger(bodyEtran, e.Attributes, GetToken(e), bvars, null, null); + private Expr TranslateMultiSelectExpr(MultiSelectExpr selectExpr) { + MultiSelectExpr e = selectExpr; + Type elmtType = UserDefinedType.ArrayElementType(e.Array.Type); ; + Boogie.Type elType = BoogieGenerator.TrType(elmtType); - if (e.Range != null) { - antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range)); - } - Boogie.Expr body = bodyEtran.TrExpr(e.Term); + Boogie.Expr fieldName = GetArrayIndexFieldName(GetToken(selectExpr), e.Indices); + Boogie.Expr x = BoogieGenerator.ReadHeap(GetToken(selectExpr), HeapExpr, TrExpr(e.Array), fieldName); + if (!ModeledAsBoxType(elmtType)) { + x = BoogieGenerator.FunctionCall(GetToken(selectExpr), BuiltinFunction.Unbox, elType, x); + } + return x; + } + + private Expr TranslateApplyExpr(ApplyExpr applyExpr) { + int arity = applyExpr.Args.Count; + var tt = applyExpr.Function.Type.AsArrowType; + Contract.Assert(tt != null); + Contract.Assert(tt.Arity == arity); + + { + // optimisation: if this could have just as well been a FunctionCallExpr, call it as such! + var con = applyExpr.Function as ConcreteSyntaxExpression; + var recv = con == null ? applyExpr.Function : con.Resolved; + var mem = recv as MemberSelectExpr; + var fn = mem == null ? null : mem.Member as Function; + if (fn != null) { + return TrExpr(new FunctionCallExpr(applyExpr.Origin, fn.NameNode, mem.Obj, applyExpr.Origin, applyExpr.CloseParen, applyExpr.Args) { + Function = fn, + Type = applyExpr.Type, + TypeApplication_AtEnclosingClass = mem.TypeApplicationAtEnclosingClass, + TypeApplication_JustFunction = mem.TypeApplicationJustMember + }); + } + } - if (e is ForallExpr) { - return new Boogie.ForallExpr(GetToken(quantifierExpr), [], bvars, kv, tr, BplImp(antecedent, body)); - } else { - Contract.Assert(e is ExistsExpr); - return new Boogie.ExistsExpr(GetToken(quantifierExpr), [], bvars, kv, tr, BplAnd(antecedent, body)); - } - } - } - case SetComprehension comprehension: { - var e = comprehension; - List freeOfAlloc = BoundedPool.HasBounds(e.Bounds, BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc); - - // Translate "set xs | R :: T" into: - // Set#FromBoogieMap(lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))) - // or if "T" is "xs", then: - // Set#FromBoogieMap(lambda y: BoxType :: CorrectType(y) && R[xs := Unbox(y)]) - // where Set#FromBoogieMap is omitted for iset. - // FIXME: This is not a good translation, see comment in PreludeCore.bpl. It should be changed to not use a Boogie lambda expression - // but to instead do the lambda lifting here. - var yVar = new Boogie.BoundVariable(GetToken(comprehension), new Boogie.TypedIdent(GetToken(comprehension), BoogieGenerator.CurrentIdGenerator.FreshId("$y#"), Predef.BoxType)); - Boogie.Expr y = new Boogie.IdentifierExpr(GetToken(comprehension), yVar); - Boogie.Expr lbody; - if (e.TermIsSimple) { - var bv = e.BoundVars[0]; - // lambda y: BoxType :: CorrectType(y) && R[xs := yUnboxed] - Boogie.Expr typeAntecedent = BoogieGenerator.MkIsBox(new Boogie.IdentifierExpr(GetToken(comprehension), yVar), bv.Type); - if (freeOfAlloc != null && !freeOfAlloc[0]) { - var isAlloc = BoogieGenerator.MkIsAllocBox(new Boogie.IdentifierExpr(GetToken(comprehension), yVar), bv.Type, HeapExpr); - typeAntecedent = BplAnd(typeAntecedent, isAlloc); - } - var yUnboxed = BoogieGenerator.UnboxUnlessInherentlyBoxed(new Boogie.IdentifierExpr(GetToken(comprehension), yVar), bv.Type); - var range = BoogieGenerator.Substitute(e.Range, bv, new BoogieWrapper(yUnboxed, bv.Type)); - lbody = BplAnd(typeAntecedent, TrExpr(range)); + Expr TrArg(Expression arg) => BoogieGenerator.BoxIfNotNormallyBoxed(arg.Origin, TrExpr(arg), arg.Type); + + var applied = FunctionCall(GetToken(applyExpr), BoogieGenerator.Apply(arity), Predef.BoxType, + Concat(Map(tt.TypeArgs, BoogieGenerator.TypeToTy), + Cons(HeapExprForArrow(applyExpr.Function.Type), Cons(TrExpr(applyExpr.Function), applyExpr.Args.ConvertAll(arg => TrArg(arg)))))); + + return BoogieGenerator.UnboxUnlessInherentlyBoxed(applied, tt.Result); + } + + private Expr TranslateMemberSelectExpr(MemberSelectExpr selectExpr) { + return selectExpr.MemberSelectCase( + field => { + var useSurrogateLocal = BoogieGenerator.inBodyInitContext && Expression.AsThis(selectExpr.Obj) != null && !field.IsInstanceIndependentConstant; + var fType = BoogieGenerator.TrType(field.Type); + if (useSurrogateLocal) { + return new Boogie.IdentifierExpr(GetToken(selectExpr), BoogieGenerator.SurrogateName(field), fType); + } else if (field is ConstantField) { + var typeMap = selectExpr.TypeArgumentSubstitutionsWithParents(); + var args = GetTypeParams(field.EnclosingClass).ConvertAll(tp => BoogieGenerator.TypeToTy(typeMap[tp])); + Boogie.Expr result; + if (field.IsStatic) { + result = new Boogie.NAryExpr(GetToken(selectExpr), new Boogie.FunctionCall(BoogieGenerator.GetReadonlyField(field)), args); } else { - // lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T)) - List bvars = []; - Boogie.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars, false, freeOfAlloc); - - var eq = Boogie.Expr.Eq(y, BoxIfNecessary(GetToken(comprehension), TrExpr(e.Term), e.Term.Type)); - var ebody = BplAnd(BplAnd(typeAntecedent, TrExpr(e.Range)), eq); - var triggers = BoogieGenerator.TrTrigger(this, e.Attributes, GetToken(e)); - lbody = new Boogie.ExistsExpr(GetToken(comprehension), bvars, triggers, ebody); + Boogie.Expr obj = BoogieGenerator.BoxifyForTraitParent(selectExpr.Origin, TrExpr(selectExpr.Obj), selectExpr.Member, selectExpr.Obj.Type); + args.Add(obj); + result = new Boogie.NAryExpr(GetToken(selectExpr), new Boogie.FunctionCall(BoogieGenerator.GetReadonlyField(field)), args); } - Boogie.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); - var lambda = new Boogie.LambdaExpr(GetToken(comprehension), [], [yVar], kv, lbody); - return comprehension.Type.NormalizeToAncestorType().AsSetType.Finite - ? FunctionCall(GetToken(comprehension), "Set#FromBoogieMap", Predef.SetType, lambda) - : lambda; - } - case MapComprehension comprehension: { - var e = comprehension; - // Translate "map x,y | R(x,y) :: F(x,y) := G(x,y)" into - // Map#Glue(lambda w: BoxType :: exists x,y :: R(x,y) && unbox(w) == F(x,y), - // lambda w: BoxType :: G(project_x(unbox(w)), project_y(unbox(w))), - // type)". - // where project_x and project_y are functions defined (elsewhere, in CanCallAssumption) by the following axiom: - // forall x,y :: R(x,y) ==> var x',y' := project_x(unbox(F(x,y))),project_y(unbox(F(x,y))); R(x',y') && F(x',y') == F(x,y) - // that is (without the let expression): - // forall x,y :: R(x,y) ==> R(project_x(unbox(F(x,y))), project_y(unbox(F(x,y)))) && F(project_x(unbox(F(x,y))), project_y(unbox(F(x,y)))) == F(x,y) - // - // In the common case where F(x,y) is omitted (in which case the list of bound variables is restricted to length 1): - // Translate "map x | R(x) :: G(x)" into - // Map#Glue(lambda w: BoxType :: R(unbox(w)), - // lambda w: BoxType :: G(unbox(w)), - // type)". - List bvars = []; - List freeOfAlloc = BoundedPool.HasBounds(e.Bounds, BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc); - - Boogie.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); - - var wVar = new Boogie.BoundVariable(GetToken(comprehension), new Boogie.TypedIdent(GetToken(comprehension), BoogieGenerator.CurrentIdGenerator.FreshId("$w#"), Predef.BoxType)); - - Boogie.Expr keys, values; - if (!e.IsGeneralMapComprehension) { - var bv = e.BoundVars[0]; - var w = new Boogie.IdentifierExpr(GetToken(comprehension), wVar); - Boogie.Expr unboxw = BoogieGenerator.UnboxUnlessInherentlyBoxed(w, bv.Type); - Boogie.Expr typeAntecedent = BoogieGenerator.MkIsBox(w, bv.Type); - if (freeOfAlloc != null && !freeOfAlloc[0]) { - var isAlloc = BoogieGenerator.MkIsAllocBox(w, bv.Type, HeapExpr); - typeAntecedent = BplAnd(typeAntecedent, isAlloc); - } - var subst = new Dictionary(); - subst.Add(bv, new BoogieWrapper(unboxw, bv.Type)); - - var ebody = BplAnd(typeAntecedent, TrExpr(BoogieGenerator.Substitute(e.Range, null, subst))); - keys = new Boogie.LambdaExpr(GetToken(e), [], [wVar], kv, ebody); - ebody = TrExpr(BoogieGenerator.Substitute(e.Term, null, subst)); - values = new Boogie.LambdaExpr(GetToken(e), [], [wVar], kv, BoxIfNecessary(GetToken(comprehension), ebody, e.Term.Type)); + result = BoogieGenerator.CondApplyUnbox(GetToken(selectExpr), result, field.Type, selectExpr.Type); + return result; + } else { + Boogie.Expr obj = TrExpr(selectExpr.Obj); + Boogie.Expr result; + if (field.IsMutable) { + var tok = GetToken(selectExpr); + result = BoogieGenerator.ReadHeap(tok, HeapExpr, obj, new Boogie.IdentifierExpr(GetToken(selectExpr), BoogieGenerator.GetField(field))); + result = fType == Predef.BoxType ? result : BoogieGenerator.ApplyUnbox(tok, result, fType); + return BoogieGenerator.CondApplyUnbox(tok, result, field.Type, selectExpr.Type); } else { - var t = e.TermLeft; - var w = new Boogie.IdentifierExpr(GetToken(comprehension), wVar); - Boogie.Expr unboxw = BoogieGenerator.UnboxUnlessInherentlyBoxed(w, t.Type); - Boogie.Expr typeAntecedent = BoogieGenerator.MkIsBox(w, t.Type); - if (freeOfAlloc != null && !freeOfAlloc[0]) { - var isAlloc = BoogieGenerator.MkIsAllocBox(w, t.Type, HeapExpr); - typeAntecedent = BplAnd(typeAntecedent, isAlloc); + result = new Boogie.NAryExpr(GetToken(selectExpr), new Boogie.FunctionCall(BoogieGenerator.GetReadonlyField(field)), + new List { obj }); + result = BoogieGenerator.CondApplyUnbox(GetToken(selectExpr), result, field.Type, selectExpr.Type); + if (BoogieGenerator.IsLit(obj)) { + result = MaybeLit(result, BoogieGenerator.TrType(selectExpr.Type)); } - - BoogieGenerator.CreateBoundVariables(e.BoundVars, out var bvs, out var args); - Contract.Assert(e.BoundVars.Count == bvs.Count); - var subst = new Dictionary(); - for (var i = 0; i < e.BoundVars.Count; i++) { - subst.Add(e.BoundVars[i], new BoogieWrapper(args[i], e.BoundVars[i].Type)); - } - var rr = TrExpr(BoogieGenerator.Substitute(e.Range, null, subst)); - var ff = TrExpr(BoogieGenerator.Substitute(t, null, subst)); - var exst_body = BplAnd(rr, Boogie.Expr.Eq(unboxw, ff)); - var ebody = BplAnd(typeAntecedent, new Boogie.ExistsExpr(GetToken(e), bvs, exst_body)); - keys = new Boogie.LambdaExpr(GetToken(e), [], [wVar], kv, ebody); - - BoogieGenerator.CreateMapComprehensionProjectionFunctions(e); - Contract.Assert(e.ProjectionFunctions != null && e.ProjectionFunctions.Count == e.BoundVars.Count); - subst = new Dictionary(); - for (var i = 0; i < e.BoundVars.Count; i++) { - var p = new Boogie.NAryExpr(GetToken(e), new Boogie.FunctionCall(e.ProjectionFunctions[i]), new List { unboxw }); - var prj = new BoogieWrapper(p, e.BoundVars[i].Type); - subst.Add(e.BoundVars[i], prj); - } - ebody = TrExpr(BoogieGenerator.Substitute(e.Term, null, subst)); - values = new Boogie.LambdaExpr(GetToken(e), [], [wVar], kv, BoxIfNecessary(GetToken(comprehension), ebody, e.Term.Type)); + return result; } - - return BoogieGenerator.FunctionCall(GetToken(e), - e.Finite ? BuiltinFunction.MapGlue : BuiltinFunction.IMapGlue, - null, - e.Finite ? FunctionCall(GetToken(comprehension), "Set#FromBoogieMap", Predef.SetType, keys) : keys, - values, BoogieGenerator.TypeToTy(comprehension.Type)); - } - case LambdaExpr lambdaExpr: { - var e = lambdaExpr; - return TrLambdaExpr(e); - } - case StmtExpr stmtExpr: { - var e = stmtExpr; - return TrExpr(e.E); } - case ITEExpr iteExpr: { - ITEExpr e = iteExpr; - var g = BoogieGenerator.RemoveLit(TrExpr(e.Test)); - var thn = BoogieGenerator.AdaptBoxing(e.Thn.Origin, BoogieGenerator.RemoveLit(TrExpr(e.Thn)), e.Thn.Type, e.Type); - var els = BoogieGenerator.AdaptBoxing(e.Els.Origin, BoogieGenerator.RemoveLit(TrExpr(e.Els)), e.Els.Type, e.Type); - return new NAryExpr(GetToken(iteExpr), new IfThenElse(GetToken(iteExpr)), new List { g, thn, els }); + }, + fn => { + var typeMap = selectExpr.TypeArgumentSubstitutionsWithParents(); + var args = GetTypeParams(fn).ConvertAll(tp => BoogieGenerator.TypeToTy(typeMap[tp])); + if (fn.IsFuelAware()) { + args.Add(this.layerInterCluster.GetFunctionFuel(fn)); } - case MatchExpr matchExpr: { - var e = matchExpr; - var ite = DesugarMatchExpr(e); - return TrExpr(ite); + if (fn.IsOpaque || fn.IsMadeImplicitlyOpaque(options)) { + args.Add(BoogieGenerator.GetRevealConstant(fn)); } - case ConcreteSyntaxExpression expression: { - var e = expression; - return TrExpr(e.ResolvedExpression); + if (fn is TwoStateFunction) { + args.Add(Old.HeapExpr); } - case NestedMatchExpr nestedMatchExpr: - return TrExpr(nestedMatchExpr.Flattened); - case BoxingCastExpr castExpr: { - BoxingCastExpr e = castExpr; - return BoogieGenerator.CondApplyBox(GetToken(e), TrExpr(e.E), e.FromType, e.ToType); - } - case UnboxingCastExpr castExpr: { - UnboxingCastExpr e = castExpr; - return BoogieGenerator.CondApplyUnbox(GetToken(e), TrExpr(e.E), e.FromType, e.ToType); - } - case DecreasesToExpr decreasesToExpr: - var oldArray = decreasesToExpr.OldExpressions.ToArray(); - var newArray = decreasesToExpr.NewExpressions.ToArray(); - List newExprs = []; - List oldExprs = []; - List newExprsDafny = []; - List oldExprsDafny = []; - int N = Math.Min(oldArray.Length, newArray.Length); - for (int i = 0; i < N; i++) { - if (!CompatibleDecreasesTypes(oldArray[i].Type, newArray[i].Type)) { - N = i; - break; - } - oldExprsDafny.Add(oldArray[i]); - oldExprs.Add(TrExpr(oldArray[i])); - newExprsDafny.Add(newArray[i]); - newExprs.Add(TrExpr(newArray[i])); + if (!fn.IsStatic) { + Boogie.Expr obj = BoogieGenerator.BoxifyForTraitParent(selectExpr.Origin, TrExpr(selectExpr.Obj), selectExpr.Member, selectExpr.Obj.Type); + args.Add(obj); } + return FunctionCall(GetToken(selectExpr), BoogieGenerator.FunctionHandle(fn), Predef.HandleType, args); + }); + } + + private Expr TranslateMapDisplayExpr(MapDisplayExpr displayExpr) { + Boogie.Type maptype = displayExpr.Finite ? Predef.MapType : Predef.IMapType; + Boogie.Expr s = BoogieGenerator.FunctionCall(GetToken(displayExpr), displayExpr.Finite ? BuiltinFunction.MapEmpty : BuiltinFunction.IMapEmpty, Predef.BoxType); + var isLit = true; + foreach (MapDisplayEntry p in displayExpr.Elements) { + var rawA = TrExpr(p.A); + var rawB = TrExpr(p.B); + isLit = isLit && BoogieGenerator.IsLit(rawA) && BoogieGenerator.IsLit(rawB); + Boogie.Expr elt = BoxIfNecessary(GetToken(displayExpr), rawA, cce.NonNull(p.A.Type)); + Boogie.Expr elt2 = BoxIfNecessary(GetToken(displayExpr), rawB, cce.NonNull(p.B.Type)); + s = FunctionCall(GetToken(displayExpr), displayExpr.Finite ? "Map#Build" : "IMap#Build", maptype, s, elt, elt2); + } + if (isLit) { + // Lit-lifting: All keys and values are lit, so the map is Lit too + s = MaybeLit(s, Predef.BoxType); + } + return s; + } - bool endsWithWinningTopComparison = N == oldArray.Length && N < newArray.Length; - var allowNoChange = decreasesToExpr.AllowNoChange || endsWithWinningTopComparison; - List toks = oldExprs.Zip(newExprs, (_, _) => (IOrigin)decreasesToExpr.Origin).ToList(); - var decreasesExpr = BoogieGenerator.DecreasesCheck(toks, null, - newExprsDafny, oldExprsDafny, newExprs, oldExprs, null, - null, allowNoChange, false); - return decreasesExpr; - case FieldLocation fieldLocation: - var tok = GetToken(expr); - if (fieldLocation.Field is SpecialField { EnclosingMethod: not null }) { - Expr depthExpr = fieldLocation.AtCallSite ? - FunctionCall(tok, "+", Boogie.Type.Int, Id(tok, "depth"), One(tok)) - : Id(tok, "depth"); - return FunctionCall(tok, "local_field", Predef.FieldName(tok), - Id(tok, BoogieGenerator.GetField(fieldLocation.Field)), - depthExpr - ); - } else { - return Id(tok, BoogieGenerator.GetField(fieldLocation.Field)); - } - case IndexFieldLocation indexFieldLocation: - return GetArrayIndexFieldName(indexFieldLocation.Origin, indexFieldLocation.Indices.ToList()); - case LocalsObjectExpression: - return Predef.Locals; - default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + private Expr TranslateBoogieFunctionCall(BoogieFunctionCall call) { + var id = new Boogie.IdentifierExpr(GetToken(call), call.FunctionName, BoogieGenerator.TrType(call.Type)); + var args = new List(); + foreach (var arg in call.TyArgs) { + args.Add(BoogieGenerator.TypeToTy(arg)); + } + if (call.UsesHeap) { + args.Add(HeapExpr); + } + if (call.UsesOldHeap) { + args.Add(Old.HeapExpr); + } + foreach (var heapAtLabel in call.HeapAtLabels) { + var bv = BplBoundVar("$Heap_at_" + heapAtLabel.AssignUniqueId(BoogieGenerator.CurrentIdGenerator), BoogieGenerator.Predef.HeapType, out var ve); + args.Add(ve); } + foreach (var arg in call.Args) { + args.Add(TrExpr(arg)); + } + return new Boogie.NAryExpr(GetToken(call), new Boogie.FunctionCall(id), args); + } + + private Expr TranslateSetDisplayExpr(SetDisplayExpr displayExpr) { + Boogie.Expr s = BoogieGenerator.FunctionCall(GetToken(displayExpr), displayExpr.Finite ? BuiltinFunction.SetEmpty : BuiltinFunction.ISetEmpty, Predef.BoxType); + var isLit = true; + foreach (Expression ee in displayExpr.Elements) { + var rawElement = TrExpr(ee); + isLit = isLit && BoogieGenerator.IsLit(rawElement); + Boogie.Expr ss = BoxIfNecessary(GetToken(displayExpr), rawElement, cce.NonNull(ee.Type)); + s = BoogieGenerator.FunctionCall(GetToken(displayExpr), displayExpr.Finite ? BuiltinFunction.SetUnionOne : BuiltinFunction.ISetUnionOne, Predef.BoxType, s, ss); + } + if (isLit) { + // Lit-lifting: All elements are lit, so the set is Lit too + s = MaybeLit(s, Predef.BoxType); + } + return s; } + public Expr TrExprSpecialFunctionCall(FunctionCallExpr expr) { Contract.Requires(expr.Function is SpecialFunction); string name = expr.Function.Name; @@ -1805,201 +1427,6 @@ public Boogie.Expr BoxIfNecessary(IOrigin tok, Boogie.Expr e, Type fromType) { return BoogieGenerator.BoxIfNecessary(tok, e, fromType); } - /// - /// Translate like s[Box(elmt)], but try to avoid as many set functions as possible in the - /// translation, because such functions can mess up triggering. - /// - public Boogie.Expr TrInSet(IOrigin tok, Boogie.Expr elmt, Expression s, Type elmtType, bool isFiniteSet, bool aggressive, out bool performedRewrite) { - Contract.Requires(tok != null); - Contract.Requires(elmt != null); - Contract.Requires(s != null); - Contract.Requires(elmtType != null); - Contract.Ensures(Contract.Result() != null); - - var elmtBox = BoxIfNecessary(tok, elmt, elmtType); - var r = TrInSet_Aux(tok, elmt, elmtBox, s, isFiniteSet, aggressive, out performedRewrite); - Contract.Assert(performedRewrite == RewriteInExpr(s, aggressive)); // sanity check - return r; - } - /// - /// The worker routine for TrInSet. This method takes both "elmt" and "elmtBox" as parameters, - /// using the former when the unboxed form is needed and the latter when the boxed form is needed. - /// This gives the caller the flexibility to pass in either "o, Box(o)" or "Unbox(bx), bx". - /// Note: This method must be kept in synch with RewriteInExpr. - /// - public Expr TrInSet_Aux(IOrigin tok, Expr elmt, Expr elmtBox, Expression s, bool isFiniteSet, bool aggressive, - out bool performedRewrite, Func extractObjectFromMemoryLocation = null) { - Contract.Requires(tok != null); - Contract.Requires(elmt != null); - Contract.Requires(elmtBox != null); - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); - - performedRewrite = true; // assume a rewrite will happen - s = s.Resolved; - bool pr; - if (s is BinaryExpr && aggressive) { - BinaryExpr bin = (BinaryExpr)s; - switch (bin.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.Union: - return BplOr( - TrInSet_Aux(tok, elmt, elmtBox, bin.E0, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation), - TrInSet_Aux(tok, elmt, elmtBox, bin.E1, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation)); - case BinaryExpr.ResolvedOpcode.Intersection: - return BplAnd( - TrInSet_Aux(tok, elmt, elmtBox, bin.E0, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation), - TrInSet_Aux(tok, elmt, elmtBox, bin.E1, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation)); - case BinaryExpr.ResolvedOpcode.SetDifference: - return BplAnd( - TrInSet_Aux(tok, elmt, elmtBox, bin.E0, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation), - Boogie.Expr.Not(TrInSet_Aux(tok, elmt, elmtBox, bin.E1, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation))); - default: - break; - } - } else if (s is SetDisplayExpr) { - SetDisplayExpr disp = (SetDisplayExpr)s; - Boogie.Expr disjunction = null; - foreach (Expression a in disp.Elements) { - var oneElem = TrExpr(a); - oneElem = extractObjectFromMemoryLocation != null ? extractObjectFromMemoryLocation(oneElem) : oneElem; - Boogie.Expr disjunct = Boogie.Expr.Eq(elmt, oneElem); - if (disjunction == null) { - disjunction = disjunct; - } else { - disjunction = BplOr(disjunction, disjunct); - } - } - if (disjunction == null) { - return Boogie.Expr.False; - } else { - return disjunction; - } - } else if (s is SetComprehension) { - var compr = (SetComprehension)s; - // Translate "elmt in set xs | R :: T[xs]" into: - // exists xs :: CorrectType(xs) && R && elmt==T[xs] - // or if "T[xs]" is "xs", then: - // CorrectType(elmt) && R[xs := elmt] - if (compr.TermIsSimple && extractObjectFromMemoryLocation == null) { - // CorrectType(elmt) && R[xs := elmt] - // Note, we can always use NOALLOC here. - Boogie.Expr typeAntecedent = BoogieGenerator.GetWhereClause(GetToken(compr), elmt, compr.BoundVars[0].Type, this, NOALLOC) ?? Boogie.Expr.True; - var range = BoogieGenerator.Substitute(compr.Range, compr.BoundVars[0], new BoogieWrapper(elmt, compr.BoundVars[0].Type)); - return BplAnd(typeAntecedent, TrExpr(range)); - } else { - // exists xs :: CorrectType(xs) && R && elmt==T[xs] - List freeOfAlloc = BoundedPool.HasBounds(compr.Bounds, BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc); - var bvars = new List(); - Boogie.Expr typeAntecedent = TrBoundVariables(compr.BoundVars, bvars, false, freeOfAlloc) ?? Boogie.Expr.True; - var eq = Boogie.Expr.Eq(elmtBox, BoxIfNecessary(GetToken(compr), extractObjectFromMemoryLocation != null ? extractObjectFromMemoryLocation(TrExpr(compr.Term)) : TrExpr(compr.Term), compr.Term.Type)); - var ebody = BplAnd(BplAnd(typeAntecedent, TrExpr(compr.Range)), eq); - var triggers = BoogieGenerator.TrTrigger(this, compr.Attributes, GetToken(compr)); - return new Boogie.ExistsExpr(GetToken(compr), bvars, triggers, ebody); - } - } - - if (extractObjectFromMemoryLocation != null) { - // Translate "elmt in s" into "exists xs :: xs in s && elem == xs.0" - // with extractObjectFromMemoryLocation = (xs) => xs.0 - var xs = new Bpl.BoundVariable(GetToken(s), new TypedIdent(tok, "xs", BoogieGenerator.TrType(s.Type.AsSetType.Arg))); - var xsExpr = new Bpl.IdentifierExpr(xs.tok, xs); - var xsExprBoxExtract = extractObjectFromMemoryLocation(xsExpr); - // Create the trigger Set#IsMember(xs, s) - var trigger = new Trigger(tok, false, [ - BoogieGenerator.FunctionCall(tok, BuiltinFunction.SetIsMember, Bpl.Type.Bool, xsExpr, TrExpr(s)) - ]); - var ebody = Boogie.Expr.Eq(elmt, xsExprBoxExtract); - return new Boogie.ExistsExpr(GetToken(s), new List() { xs }, trigger, ebody); - } - performedRewrite = false; - - return BoogieGenerator.IsSetMember(tok, TrExpr(s), elmtBox, isFiniteSet); - } - - /// - /// Translate like 0 < s[Box(elmt)], but try to avoid as many set functions as possible in the - /// translation, because such functions can mess up triggering. - /// Note: This method must be kept in synch with RewriteInExpr. - /// - public Boogie.Expr TrInMultiSet(IOrigin tok, Boogie.Expr elmt, Expression s, Type elmtType, bool aggressive) { - Contract.Requires(tok != null); - Contract.Requires(elmt != null); - Contract.Requires(s != null); - Contract.Requires(elmtType != null); - - Contract.Ensures(Contract.Result() != null); - var elmtBox = BoxIfNecessary(tok, elmt, elmtType); - return TrInMultiSet_Aux(tok, elmt, elmtBox, s, aggressive); - } - public Boogie.Expr TrInMultiSet_Aux(IOrigin tok, Boogie.Expr elmt, Boogie.Expr elmtBox, Expression s, bool aggressive) { - Contract.Requires(tok != null); - Contract.Requires(elmt != null); - Contract.Requires(s != null); - Contract.Requires(elmtBox != null); - - Contract.Ensures(Contract.Result() != null); - - s = s.Resolved; - if (s is BinaryExpr && aggressive) { - BinaryExpr bin = (BinaryExpr)s; - switch (bin.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.MultiSetUnion: - return Boogie.Expr.Binary(tok, BinaryOperator.Opcode.Or, TrInMultiSet_Aux(tok, elmt, elmtBox, bin.E0, aggressive), TrInMultiSet_Aux(tok, elmt, elmtBox, bin.E1, aggressive)); - case BinaryExpr.ResolvedOpcode.MultiSetIntersection: - return Boogie.Expr.Binary(tok, BinaryOperator.Opcode.And, TrInMultiSet_Aux(tok, elmt, elmtBox, bin.E0, aggressive), TrInMultiSet_Aux(tok, elmt, elmtBox, bin.E1, aggressive)); - default: - break; - } - } else if (s is MultiSetDisplayExpr) { - MultiSetDisplayExpr disp = (MultiSetDisplayExpr)s; - Boogie.Expr disjunction = null; - foreach (Expression a in disp.Elements) { - Boogie.Expr disjunct = Boogie.Expr.Eq(elmt, TrExpr(a)); - if (disjunction == null) { - disjunction = disjunct; - } else { - disjunction = BplOr(disjunction, disjunct); - } - } - if (disjunction == null) { - return Boogie.Expr.False; - } else { - return disjunction; - } - } - var result = Boogie.Expr.Gt(BoogieGenerator.MultisetMultiplicity(tok, TrExpr(s), elmtBox), Boogie.Expr.Literal(0)); - result.tok = tok; - return result; - } - - /// - /// This method returns "true" iff TrInSet_Aux/TrInMultiSet_Aux will rewrite an expression "x in s". - /// Note: This method must be kept in synch with TrInSet_Aux/TrInMultiSet_Aux. - /// - public static bool RewriteInExpr(Expression s, bool aggressive) { - Contract.Requires(s != null); - - s = s.Resolved; - if (s is BinaryExpr && aggressive) { - BinaryExpr bin = (BinaryExpr)s; - switch (bin.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.Union: - case BinaryExpr.ResolvedOpcode.Intersection: - case BinaryExpr.ResolvedOpcode.SetDifference: - case BinaryExpr.ResolvedOpcode.MultiSetUnion: - case BinaryExpr.ResolvedOpcode.MultiSetIntersection: - return true; - default: - break; - } - } else if (s is SetDisplayExpr || s is MultiSetDisplayExpr) { - return true; - } else if (s is SetComprehension) { - return true; - } - return false; - } - private static readonly Dictionary NullaryAttributesToTranslate; private static readonly HashSet NullaryAttributesToCopy = [ @@ -2321,71 +1748,8 @@ [new BoogieWrapper(index, Type.Int)], } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; return CanCallAssumption(e.E, cco); - } else if (expr is BinaryExpr) { - // The short-circuiting boolean operators &&, ||, and ==> end up duplicating their - // left argument. Therefore, we first try to re-associate the expression to make - // left arguments smaller. - if (BoogieGenerator.ReAssociateToTheRight(ref expr)) { - return CanCallAssumption(expr, cco); - } - var e = (BinaryExpr)expr; - - Boogie.Expr t0 = CanCallAssumption(e.E0, cco); - Boogie.Expr t1 = CanCallAssumption(e.E1, cco); - switch (e.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.And: - case BinaryExpr.ResolvedOpcode.Imp: - t1 = BplImp(TrExpr(e.E0), t1); - break; - case BinaryExpr.ResolvedOpcode.Or: - t1 = BplImp(Boogie.Expr.Not(TrExpr(e.E0)), t1); - break; - case BinaryExpr.ResolvedOpcode.EqCommon: - case BinaryExpr.ResolvedOpcode.NeqCommon: { - Boogie.Expr r = Boogie.Expr.True; - if (cco is not { SkipIsA: true }) { - if (e.E0 is { Type: { AsDatatype: { } dt0 }, Resolved: not DatatypeValue }) { - var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.Origin, "$IsA#" + dt0.FullSanitizedName, Boogie.Type.Bool)); - r = BplAnd(r, new Boogie.NAryExpr(expr.Origin, funcID, new List { TrExpr(e.E0) })); - } - if (e.E1 is { Type: { AsDatatype: { } dt1 }, Resolved: not DatatypeValue }) { - var funcID = new Boogie.FunctionCall(new Boogie.IdentifierExpr(expr.Origin, "$IsA#" + dt1.FullSanitizedName, Boogie.Type.Bool)); - r = BplAnd(r, new Boogie.NAryExpr(expr.Origin, funcID, new List { TrExpr(e.E1) })); - } - } - return BplAnd(r, BplAnd(t0, t1)); - } - case BinaryExpr.ResolvedOpcode.Mul: - if (7 <= BoogieGenerator.options.ArithMode) { - if (e.E0.Type.IsNumericBased(Type.NumericPersuasion.Int) && !BoogieGenerator.DisableNonLinearArithmetic) { - // Produce a useful fact about the associativity of multiplication. It is a bit dicey to do as an axiom. - // Change (k*A)*B or (A*k)*B into (A*B)*k, where k is a numeric literal - var left = e.E0.Resolved as BinaryExpr; - if (left != null && left.ResolvedOp == BinaryExpr.ResolvedOpcode.Mul) { - Boogie.Expr r = Boogie.Expr.True; - if (left.E0.Resolved is LiteralExpr) { - // (K*A)*B == (A*B)*k - var y = Expression.CreateMul(Expression.CreateMul(left.E1, e.E1), left.E0); - var eq = Expression.CreateEq(e, y, e.E0.Type); - r = BplAnd(r, TrExpr(eq)); - } - if (left.E1.Resolved is LiteralExpr) { - // (A*k)*B == (A*B)*k - var y = Expression.CreateMul(Expression.CreateMul(left.E0, e.E1), left.E1); - var eq = Expression.CreateEq(e, y, e.E0.Type); - r = BplAnd(r, TrExpr(eq)); - } - if (r != Boogie.Expr.True) { - return BplAnd(BplAnd(t0, t1), r); - } - } - } - } - break; - default: - break; - } - return BplAnd(t0, t1); + } else if (expr is BinaryExpr binaryExpr) { + return BinaryExprCanCallAssumption(binaryExpr, cco); } else if (expr is TernaryExpr) { var e = (TernaryExpr)expr; return BplAnd(CanCallAssumption(e.E0, cco), BplAnd(CanCallAssumption(e.E1, cco), CanCallAssumption(e.E2, cco))); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 69978552ca3..5347e305029 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -2450,41 +2450,6 @@ void AddCasePatternVarSubstitutions(CasePattern pat, Bpl.Expr rhs, Dic } } - /// - /// If "expr" is a binary boolean operation, then try to re-associate it to make the left argument smaller. - /// If it is possible, then "true" is returned and "expr" returns as the re-associated expression (no boolean simplifications are performed). - /// If not, then "false" is returned and "expr" is unchanged. - /// - bool ReAssociateToTheRight(ref Expression expr) { - if (expr is BinaryExpr top && Expression.StripParens(top.E0) is BinaryExpr left) { - // We have an expression of the form "(A oo B) pp C" - var A = left.E0; - var oo = left.ResolvedOp; - var B = left.E1; - var pp = top.ResolvedOp; - var C = top.E1; - - if (oo == BinaryExpr.ResolvedOpcode.And && pp == BinaryExpr.ResolvedOpcode.And) { - // rewrite (A && B) && C into A && (B && C) - expr = Expression.CreateAnd(A, Expression.CreateAnd(B, C, false), false); - return true; - } else if (oo == BinaryExpr.ResolvedOpcode.And && pp == BinaryExpr.ResolvedOpcode.Imp) { - // rewrite (A && B) ==> C into A ==> (B ==> C) - expr = Expression.CreateImplies(A, Expression.CreateImplies(B, C, false), false); - return true; - } else if (oo == BinaryExpr.ResolvedOpcode.Or && pp == BinaryExpr.ResolvedOpcode.Or) { - // rewrite (A || B) || C into A || (B || C) - expr = Expression.CreateOr(A, Expression.CreateOr(B, C, false), false); - return true; - } else if (oo == BinaryExpr.ResolvedOpcode.Imp && pp == BinaryExpr.ResolvedOpcode.Or) { - // rewrite (A ==> B) || C into A ==> (B || C) - expr = Expression.CreateImplies(A, Expression.CreateOr(B, C, false), false); - return true; - } - } - return false; - } - void CheckCasePatternShape(CasePattern pat, Expression dRhs, Bpl.Expr rhs, IOrigin rhsTok, Type rhsType, BoogieStmtListBuilder builder) where VT : class, IVariable { Contract.Requires(pat != null); diff --git a/Source/DafnyCore/Verifier/Expressions/TranslateBinaryExpr.cs b/Source/DafnyCore/Verifier/Expressions/TranslateBinaryExpr.cs new file mode 100644 index 00000000000..f9f29459c65 --- /dev/null +++ b/Source/DafnyCore/Verifier/Expressions/TranslateBinaryExpr.cs @@ -0,0 +1,718 @@ +using System; +using System.Collections.Generic; + +namespace Microsoft.Dafny; + +using System.Diagnostics.Contracts; +using Boogie; + +public partial class BoogieGenerator { + public partial class ExpressionTranslator { + + private Expr TranslateBinaryExpr(BinaryExpr binaryExpr) { + var e0Type = binaryExpr.E0.Type.NormalizeToAncestorType(); // used when making decisions about what Boogie operator/functions to use + bool isReal = e0Type.IsNumericBased(Type.NumericPersuasion.Real); + int bvWidth = e0Type.IsBitVectorType ? e0Type.AsBitVectorType.Width : -1; // -1 indicates "not a bitvector type" + Expr e0 = TrExpr(binaryExpr.E0); + if (binaryExpr.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet) { + return TrInSet(GetToken(binaryExpr), e0, binaryExpr.E1, binaryExpr.E0.Type, binaryExpr.E1.Type.NormalizeToAncestorType().AsSetType.Finite, false, out var pr); // let TrInSet translate e.E1 + } else if (binaryExpr.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSet) { + Expr arg = TrInSet(GetToken(binaryExpr), e0, binaryExpr.E1, binaryExpr.E0.Type, binaryExpr.E1.Type.NormalizeToAncestorType().AsSetType.Finite, false, out var pr); // let TrInSet translate e.E1 + return Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, arg); + } else if (binaryExpr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) { + return TrInMultiSet(GetToken(binaryExpr), e0, binaryExpr.E1, binaryExpr.E0.Type, false); // let TrInMultiSet translate e.E1 + } else if (binaryExpr.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInMultiSet) { + Expr arg = TrInMultiSet(GetToken(binaryExpr), e0, binaryExpr.E1, binaryExpr.E0.Type, false); // let TrInMultiSet translate e.E1 + return Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, arg); + } + Expr e1 = TrExpr(binaryExpr.E1); + BinaryOperator.Opcode bOpcode; + Boogie.Type typ; + var oe0 = e0; + var oe1 = e1; + var lit0 = GetLit(e0); + var lit1 = GetLit(e1); + bool liftLit = BoogieGenerator.IsLit(e0) && BoogieGenerator.IsLit(e1); + // NOTE(namin): We usually avoid keeping literals, because their presence might mess up triggers that do not expect them. + // Still for equality-related operations, it's useful to keep them instead of lifting them, so that they can be propagated. + bool keepLits = false; + if (lit0 != null) { + e0 = lit0; + } + if (lit1 != null) { + e1 = lit1; + } + switch (binaryExpr.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Iff: + typ = Boogie.Type.Bool; + bOpcode = BinaryOperator.Opcode.Iff; break; + case BinaryExpr.ResolvedOpcode.Imp: + typ = Boogie.Type.Bool; + bOpcode = BinaryOperator.Opcode.Imp; break; + case BinaryExpr.ResolvedOpcode.And: + typ = Boogie.Type.Bool; + bOpcode = BinaryOperator.Opcode.And; break; + case BinaryExpr.ResolvedOpcode.Or: + typ = Boogie.Type.Bool; + bOpcode = BinaryOperator.Opcode.Or; break; + + case BinaryExpr.ResolvedOpcode.EqCommon: + keepLits = true; + if (ModeledAsBoxType(binaryExpr.E0.Type)) { + e1 = BoxIfNecessary(binaryExpr.Origin, e1, binaryExpr.E1.Type); + oe1 = BoxIfNecessary(binaryExpr.Origin, oe1, binaryExpr.E1.Type); + } else if (ModeledAsBoxType(binaryExpr.E1.Type)) { + e0 = BoxIfNecessary(binaryExpr.Origin, e0, binaryExpr.E0.Type); + oe0 = BoxIfNecessary(binaryExpr.Origin, oe0, binaryExpr.E0.Type); + } + if (binaryExpr.E0.Type.IsCoDatatype && binaryExpr.E1.Type.IsCoDatatype) { + var e0args = binaryExpr.E0.Type.NormalizeExpand().TypeArgs; + var e1args = binaryExpr.E1.Type.NormalizeExpand().TypeArgs; + return BoogieGenerator.CoEqualCall(binaryExpr.E0.Type.AsCoDatatype, e0args, e1args, null, + layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr)); + } + if (binaryExpr.E0.Type.IsIndDatatype && binaryExpr.E1.Type.IsIndDatatype) { + return BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), binaryExpr.E0.Type, e0, e1); + } + typ = Boogie.Type.Bool; + bOpcode = BinaryOperator.Opcode.Eq; + break; + case BinaryExpr.ResolvedOpcode.NeqCommon: + if (ModeledAsBoxType(binaryExpr.E0.Type)) { + e1 = BoxIfNecessary(binaryExpr.Origin, e1, binaryExpr.E1.Type); + oe1 = BoxIfNecessary(binaryExpr.Origin, oe1, binaryExpr.E1.Type); + } else if (ModeledAsBoxType(binaryExpr.E1.Type)) { + e0 = BoxIfNecessary(binaryExpr.Origin, e0, binaryExpr.E0.Type); + oe0 = BoxIfNecessary(binaryExpr.Origin, oe0, binaryExpr.E0.Type); + } + if (binaryExpr.E0.Type.IsCoDatatype && binaryExpr.E1.Type.IsCoDatatype) { + var e0args = binaryExpr.E0.Type.NormalizeExpand().TypeArgs; + var e1args = binaryExpr.E1.Type.NormalizeExpand().TypeArgs; + var eq = BoogieGenerator.CoEqualCall(binaryExpr.E0.Type.AsCoDatatype, e0args, e1args, null, + layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), e0, e1, GetToken(binaryExpr)); + return Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, eq); + } + if (binaryExpr.E0.Type.IsIndDatatype && binaryExpr.E1.Type.IsIndDatatype) { + var eq = BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), binaryExpr.E0.Type, e0, e1); + return Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, eq); + } + typ = Boogie.Type.Bool; + bOpcode = BinaryOperator.Opcode.Neq; + break; + case BinaryExpr.ResolvedOpcode.Lt: + if (0 <= bvWidth) { + return TrToFunctionCall(GetToken(binaryExpr), "lt_bv" + bvWidth, Boogie.Type.Bool, e0, e1, liftLit); + } else if (e0Type.IsBigOrdinalType) { + return FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e0, e1); + } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) { + typ = Boogie.Type.Bool; + bOpcode = BinaryOperator.Opcode.Lt; + break; + } else { + return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_lt_boogie", Boogie.Type.Bool, e0, e1, liftLit); + } + case BinaryExpr.ResolvedOpcode.LessThanLimit: + return FunctionCall(GetToken(binaryExpr), "ORD#LessThanLimit", Boogie.Type.Bool, e0, e1); + case BinaryExpr.ResolvedOpcode.Le: + keepLits = true; + if (0 <= bvWidth) { + return TrToFunctionCall(GetToken(binaryExpr), "le_bv" + bvWidth, Boogie.Type.Bool, e0, e1, false); + } else if (e0Type.IsBigOrdinalType) { + var less = FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e0, e1); + var eq = Expr.Eq(e0, e1); + return BplOr(eq, less); + } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) { + typ = Boogie.Type.Bool; + bOpcode = BinaryOperator.Opcode.Le; + break; + } else { + return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_le_boogie", Boogie.Type.Bool, e0, e1, false); + } + case BinaryExpr.ResolvedOpcode.Ge: + keepLits = true; + if (0 <= bvWidth) { + return TrToFunctionCall(GetToken(binaryExpr), "ge_bv" + bvWidth, Boogie.Type.Bool, e0, e1, false); + } else if (e0Type.IsBigOrdinalType) { + var less = FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e1, e0); + var eq = Expr.Eq(e1, e0); + return BplOr(eq, less); + } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) { + typ = Boogie.Type.Bool; + bOpcode = BinaryOperator.Opcode.Ge; + break; + } else { + return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_ge_boogie", Boogie.Type.Bool, e0, e1, false); + } + case BinaryExpr.ResolvedOpcode.Gt: + if (0 <= bvWidth) { + return TrToFunctionCall(GetToken(binaryExpr), "gt_bv" + bvWidth, Boogie.Type.Bool, e0, e1, liftLit); + } else if (e0Type.IsBigOrdinalType) { + return FunctionCall(GetToken(binaryExpr), "ORD#Less", Boogie.Type.Bool, e1, e0); + } else if (isReal || !BoogieGenerator.DisableNonLinearArithmetic) { + typ = Boogie.Type.Bool; + bOpcode = BinaryOperator.Opcode.Gt; + break; + } else { + return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_gt_boogie", Boogie.Type.Bool, e0, e1, liftLit); + } + + case BinaryExpr.ResolvedOpcode.Add: + if (0 <= bvWidth) { + return TrToFunctionCall(GetToken(binaryExpr), "add_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); + } else if (e0Type.IsBigOrdinalType) { + return TrToFunctionCall(GetToken(binaryExpr), "ORD#Plus", Predef.BigOrdinalType, e0, e1, liftLit); + } else if (e0Type.IsCharType) { + return TrToFunctionCall(GetToken(binaryExpr), "char#Plus", Predef.CharType, e0, e1, liftLit); + } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic) { + return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_add_boogie", Boogie.Type.Int, e0, e1, liftLit); + } else if (!isReal && (options.ArithMode == 2 || 5 <= options.ArithMode)) { + return TrToFunctionCall(GetToken(binaryExpr), "Add", Boogie.Type.Int, oe0, oe1, liftLit); + } else { + typ = isReal ? Boogie.Type.Real : Boogie.Type.Int; + bOpcode = BinaryOperator.Opcode.Add; + break; + } + case BinaryExpr.ResolvedOpcode.Sub: + if (0 <= bvWidth) { + return TrToFunctionCall(GetToken(binaryExpr), "sub_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); + } else if (e0Type.IsBigOrdinalType) { + return TrToFunctionCall(GetToken(binaryExpr), "ORD#Minus", Predef.BigOrdinalType, e0, e1, liftLit); + } else if (e0Type.IsCharType) { + return TrToFunctionCall(GetToken(binaryExpr), "char#Minus", Predef.CharType, e0, e1, liftLit); + } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic) { + return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_sub_boogie", Boogie.Type.Int, e0, e1, liftLit); + } else if (!isReal && (options.ArithMode == 2 || 5 <= options.ArithMode)) { + return TrToFunctionCall(GetToken(binaryExpr), "Sub", Boogie.Type.Int, oe0, oe1, liftLit); + } else { + typ = isReal ? Boogie.Type.Real : Boogie.Type.Int; + bOpcode = BinaryOperator.Opcode.Sub; + break; + } + case BinaryExpr.ResolvedOpcode.Mul: + if (0 <= bvWidth) { + return TrToFunctionCall(GetToken(binaryExpr), "mul_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); + } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic) { + return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_mul_boogie", Boogie.Type.Int, e0, e1, liftLit); + } else if (!isReal && options.ArithMode != 0 && options.ArithMode != 3) { + return TrToFunctionCall(GetToken(binaryExpr), "Mul", Boogie.Type.Int, oe0, oe1, liftLit); + } else { + typ = isReal ? Boogie.Type.Real : Boogie.Type.Int; + bOpcode = BinaryOperator.Opcode.Mul; + break; + } + case BinaryExpr.ResolvedOpcode.Div: + if (0 <= bvWidth) { + return TrToFunctionCall(GetToken(binaryExpr), "div_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); + } else if (!isReal && BoogieGenerator.DisableNonLinearArithmetic && !isReal) { + return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_div_boogie", Boogie.Type.Int, e0, e1, liftLit); + } else if (!isReal && options.ArithMode != 0 && options.ArithMode != 3) { + return TrToFunctionCall(GetToken(binaryExpr), "Div", Boogie.Type.Int, e0, oe1, liftLit); + } else if (isReal) { + typ = Boogie.Type.Real; + bOpcode = BinaryOperator.Opcode.RealDiv; + break; + } else { + typ = Boogie.Type.Int; + bOpcode = BinaryOperator.Opcode.Div; + break; + } + case BinaryExpr.ResolvedOpcode.Mod: + if (0 <= bvWidth) { + return TrToFunctionCall(GetToken(binaryExpr), "mod_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); + } else if (BoogieGenerator.DisableNonLinearArithmetic && !isReal) { + return TrToFunctionCall(GetToken(binaryExpr), "INTERNAL_mod_boogie", Boogie.Type.Int, e0, e1, liftLit); + } else if (!isReal && options.ArithMode != 0 && options.ArithMode != 3) { + return TrToFunctionCall(GetToken(binaryExpr), "Mod", Boogie.Type.Int, e0, oe1, liftLit); + } else { + typ = isReal ? Boogie.Type.Real : Boogie.Type.Int; + bOpcode = BinaryOperator.Opcode.Mod; + break; + } + + case BinaryExpr.ResolvedOpcode.LeftShift: { + Contract.Assert(0 <= bvWidth); + return TrToFunctionCall(GetToken(binaryExpr), "LeftShift_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, BoogieGenerator.ConvertExpression(GetToken(binaryExpr), e1, binaryExpr.E1.Type, binaryExpr.Type), liftLit); + } + case BinaryExpr.ResolvedOpcode.RightShift: { + Contract.Assert(0 <= bvWidth); + return TrToFunctionCall(GetToken(binaryExpr), "RightShift_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, BoogieGenerator.ConvertExpression(GetToken(binaryExpr), e1, binaryExpr.E1.Type, binaryExpr.Type), liftLit); + } + case BinaryExpr.ResolvedOpcode.BitwiseAnd: { + Contract.Assert(0 <= bvWidth); + return TrToFunctionCall(GetToken(binaryExpr), "and_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); + } + case BinaryExpr.ResolvedOpcode.BitwiseOr: { + Contract.Assert(0 <= bvWidth); + return TrToFunctionCall(GetToken(binaryExpr), "or_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); + } + case BinaryExpr.ResolvedOpcode.BitwiseXor: { + Contract.Assert(0 <= bvWidth); + return TrToFunctionCall(GetToken(binaryExpr), "xor_bv" + bvWidth, BoogieGenerator.BplBvType(bvWidth), e0, e1, liftLit); + } + + case BinaryExpr.ResolvedOpcode.LtChar: + case BinaryExpr.ResolvedOpcode.LeChar: + case BinaryExpr.ResolvedOpcode.GeChar: + case BinaryExpr.ResolvedOpcode.GtChar: { + // work off the original operands (that is, allow them to be lit-wrapped) + var operand0 = BoogieGenerator.FunctionCall(e0.tok, BuiltinFunction.CharToInt, null, oe0); + var operand1 = BoogieGenerator.FunctionCall(e0.tok, BuiltinFunction.CharToInt, null, oe1); + BinaryOperator.Opcode bOp; + switch (binaryExpr.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.LtChar: bOp = BinaryOperator.Opcode.Lt; break; + case BinaryExpr.ResolvedOpcode.LeChar: bOp = BinaryOperator.Opcode.Le; break; + case BinaryExpr.ResolvedOpcode.GeChar: bOp = BinaryOperator.Opcode.Ge; break; + case BinaryExpr.ResolvedOpcode.GtChar: bOp = BinaryOperator.Opcode.Gt; break; + default: + Contract.Assert(false); // unexpected case + throw new cce.UnreachableException(); // to please compiler + } + return Expr.Binary(GetToken(binaryExpr), bOp, operand0, operand1); + } + + case BinaryExpr.ResolvedOpcode.SetEq: + case BinaryExpr.ResolvedOpcode.MultiSetEq: + case BinaryExpr.ResolvedOpcode.SeqEq: + case BinaryExpr.ResolvedOpcode.MapEq: + return BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), binaryExpr.E0.Type, e0, e1); + case BinaryExpr.ResolvedOpcode.SetNeq: + case BinaryExpr.ResolvedOpcode.MultiSetNeq: + case BinaryExpr.ResolvedOpcode.SeqNeq: + case BinaryExpr.ResolvedOpcode.MapNeq: + return Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, BoogieGenerator.TypeSpecificEqual(GetToken(binaryExpr), binaryExpr.E0.Type, e0, e1)); + + case BinaryExpr.ResolvedOpcode.ProperSubset: { + return BoogieGenerator.ProperSubset(GetToken(binaryExpr), e0, e1, binaryExpr.E0.Type.NormalizeToAncestorType().AsSetType.Finite); + } + case BinaryExpr.ResolvedOpcode.Subset: { + bool finite = binaryExpr.E1.Type.NormalizeToAncestorType().AsSetType.Finite; + var f = finite ? BuiltinFunction.SetSubset : BuiltinFunction.ISetSubset; + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, null, e0, e1); + } + case BinaryExpr.ResolvedOpcode.Superset: { + bool finite = binaryExpr.E1.Type.NormalizeToAncestorType().AsSetType.Finite; + var f = finite ? BuiltinFunction.SetSubset : BuiltinFunction.ISetSubset; + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, null, e1, e0); + } + case BinaryExpr.ResolvedOpcode.ProperSuperset: + return BoogieGenerator.ProperSubset(GetToken(binaryExpr), e1, e0, binaryExpr.E0.Type.NormalizeToAncestorType().AsSetType.Finite); + case BinaryExpr.ResolvedOpcode.Disjoint: { + bool finite = binaryExpr.E1.Type.NormalizeToAncestorType().AsSetType.Finite; + var f = finite ? BuiltinFunction.SetDisjoint : BuiltinFunction.ISetDisjoint; + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, null, e0, e1); + } + case BinaryExpr.ResolvedOpcode.InSet: + Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above + case BinaryExpr.ResolvedOpcode.NotInSet: + Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above + case BinaryExpr.ResolvedOpcode.Union: { + var setType = binaryExpr.Type.NormalizeToAncestorType().AsSetType; + bool finite = setType.Finite; + var f = finite ? BuiltinFunction.SetUnion : BuiltinFunction.ISetUnion; + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, BoogieGenerator.TrType(setType.Arg), e0, e1); + } + case BinaryExpr.ResolvedOpcode.Intersection: { + var setType = binaryExpr.Type.NormalizeToAncestorType().AsSetType; + bool finite = setType.Finite; + var f = finite ? BuiltinFunction.SetIntersection : BuiltinFunction.ISetIntersection; + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, BoogieGenerator.TrType(setType.Arg), e0, e1); + } + case BinaryExpr.ResolvedOpcode.SetDifference: { + var setType = binaryExpr.Type.NormalizeToAncestorType().AsSetType; + bool finite = setType.Finite; + var f = finite ? BuiltinFunction.SetDifference : BuiltinFunction.ISetDifference; + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, BoogieGenerator.TrType(setType.Arg), e0, e1); + } + case BinaryExpr.ResolvedOpcode.ProperMultiSubset: + return BoogieGenerator.ProperMultiset(GetToken(binaryExpr), e0, e1); + case BinaryExpr.ResolvedOpcode.MultiSubset: + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetSubset, null, e0, e1); + case BinaryExpr.ResolvedOpcode.MultiSuperset: + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetSubset, null, e1, e0); + case BinaryExpr.ResolvedOpcode.ProperMultiSuperset: + return BoogieGenerator.ProperMultiset(GetToken(binaryExpr), e1, e0); + case BinaryExpr.ResolvedOpcode.MultiSetDisjoint: + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetDisjoint, null, e0, e1); + case BinaryExpr.ResolvedOpcode.InMultiSet: + Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above + case BinaryExpr.ResolvedOpcode.NotInMultiSet: + Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above + case BinaryExpr.ResolvedOpcode.MultiSetUnion: + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetUnion, + BoogieGenerator.TrType(binaryExpr.Type.NormalizeToAncestorType().AsMultiSetType.Arg), e0, e1); + case BinaryExpr.ResolvedOpcode.MultiSetIntersection: + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetIntersection, + BoogieGenerator.TrType(binaryExpr.Type.NormalizeToAncestorType().AsMultiSetType.Arg), e0, e1); + case BinaryExpr.ResolvedOpcode.MultiSetDifference: + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetDifference, + BoogieGenerator.TrType(binaryExpr.Type.NormalizeToAncestorType().AsMultiSetType.Arg), e0, e1); + + case BinaryExpr.ResolvedOpcode.ProperPrefix: + return BoogieGenerator.ProperPrefix(GetToken(binaryExpr), e0, e1); + case BinaryExpr.ResolvedOpcode.Prefix: { + Expr len0 = BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqLength, null, e0); + Expr len1 = BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqLength, null, e1); + return Expr.Binary(GetToken(binaryExpr), BinaryOperator.Opcode.And, + Expr.Le(len0, len1), + BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqSameUntil, null, e0, e1, len0)); + } + case BinaryExpr.ResolvedOpcode.Concat: + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqAppend, + BoogieGenerator.TrType(binaryExpr.Type.NormalizeToAncestorType().AsSeqType.Arg), e0, e1); + case BinaryExpr.ResolvedOpcode.InSeq: + return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqContains, null, e1, + BoxIfNecessary(GetToken(binaryExpr), e0, binaryExpr.E0.Type)); + case BinaryExpr.ResolvedOpcode.NotInSeq: + Expr arg = BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.SeqContains, null, e1, + BoxIfNecessary(GetToken(binaryExpr), e0, binaryExpr.E0.Type)); + return Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, arg); + case BinaryExpr.ResolvedOpcode.InMap: { + bool finite = binaryExpr.E1.Type.NormalizeToAncestorType().AsMapType.Finite; + var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain; + return BoogieGenerator.IsSetMember(GetToken(binaryExpr), + BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, finite ? Predef.MapType : Predef.IMapType, e1), + BoxIfNecessary(GetToken(binaryExpr), e0, binaryExpr.E0.Type), + finite); + } + case BinaryExpr.ResolvedOpcode.NotInMap: { + bool finite = binaryExpr.E1.Type.NormalizeToAncestorType().AsMapType.Finite; + var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain; + Expr inMap = BoogieGenerator.IsSetMember(GetToken(binaryExpr), + BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, finite ? Predef.MapType : Predef.IMapType, e1), + BoxIfNecessary(GetToken(binaryExpr), e0, binaryExpr.E0.Type), + finite); + return Expr.Unary(GetToken(binaryExpr), UnaryOperator.Opcode.Not, inMap); + } + case BinaryExpr.ResolvedOpcode.MapMerge: { + bool finite = e0Type.NormalizeToAncestorType().AsMapType.Finite; + var f = finite ? "Map#Merge" : "IMap#Merge"; + return FunctionCall(GetToken(binaryExpr), f, BoogieGenerator.TrType(binaryExpr.Type), e0, e1); + } + case BinaryExpr.ResolvedOpcode.MapSubtraction: { + bool finite = e0Type.NormalizeToAncestorType().AsMapType.Finite; + var f = finite ? "Map#Subtract" : "IMap#Subtract"; + return FunctionCall(GetToken(binaryExpr), f, BoogieGenerator.TrType(binaryExpr.Type), e0, e1); + } + + case BinaryExpr.ResolvedOpcode.RankLt: + return Expr.Binary(GetToken(binaryExpr), BinaryOperator.Opcode.Lt, + BoogieGenerator.FunctionCall(GetToken(binaryExpr), e0Type.IsDatatype ? BuiltinFunction.DtRank : BuiltinFunction.BoxRank, null, e0), + BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.DtRank, null, e1)); + case BinaryExpr.ResolvedOpcode.RankGt: + return Expr.Binary(GetToken(binaryExpr), BinaryOperator.Opcode.Gt, + BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.DtRank, null, e0), + BoogieGenerator.FunctionCall(GetToken(binaryExpr), binaryExpr.E1.Type.IsDatatype ? BuiltinFunction.DtRank : BuiltinFunction.BoxRank, null, e1)); + + default: + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected binary expression + } + liftLit = liftLit && !keepLits; + var ae0 = keepLits ? oe0 : e0; + var ae1 = keepLits ? oe1 : e1; + Expr re = Expr.Binary(GetToken(binaryExpr), bOpcode, ae0, ae1); + if (liftLit) { + re = MaybeLit(re, typ); + } + return re; + } + + /// + /// Translate like 0 < s[Box(elmt)], but try to avoid as many set functions as possible in the + /// translation, because such functions can mess up triggering. + /// Note: This method must be kept in synch with RewriteInExpr. + /// + public Expr TrInMultiSet(IOrigin tok, Expr elmt, Expression s, Type elmtType, bool aggressive) { + Contract.Requires(tok != null); + Contract.Requires(elmt != null); + Contract.Requires(s != null); + Contract.Requires(elmtType != null); + + Contract.Ensures(Contract.Result() != null); + var elmtBox = BoxIfNecessary(tok, elmt, elmtType); + return TrInMultiSet_Aux(tok, elmt, elmtBox, s, aggressive); + } + + public Expr TrInMultiSet_Aux(IOrigin tok, Expr elmt, Expr elmtBox, Expression s, bool aggressive) { + Contract.Requires(tok != null); + Contract.Requires(elmt != null); + Contract.Requires(s != null); + Contract.Requires(elmtBox != null); + + Contract.Ensures(Contract.Result() != null); + + s = s.Resolved; + if (s is BinaryExpr && aggressive) { + BinaryExpr bin = (BinaryExpr)s; + switch (bin.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.MultiSetUnion: + return Expr.Binary(tok, BinaryOperator.Opcode.Or, TrInMultiSet_Aux(tok, elmt, elmtBox, bin.E0, aggressive), TrInMultiSet_Aux(tok, elmt, elmtBox, bin.E1, aggressive)); + case BinaryExpr.ResolvedOpcode.MultiSetIntersection: + return Expr.Binary(tok, BinaryOperator.Opcode.And, TrInMultiSet_Aux(tok, elmt, elmtBox, bin.E0, aggressive), TrInMultiSet_Aux(tok, elmt, elmtBox, bin.E1, aggressive)); + default: + break; + } + } else if (s is MultiSetDisplayExpr) { + MultiSetDisplayExpr disp = (MultiSetDisplayExpr)s; + Expr disjunction = null; + foreach (Expression a in disp.Elements) { + Expr disjunct = Expr.Eq(elmt, TrExpr(a)); + if (disjunction == null) { + disjunction = disjunct; + } else { + disjunction = BplOr(disjunction, disjunct); + } + } + if (disjunction == null) { + return Expr.False; + } else { + return disjunction; + } + } + var result = Expr.Gt(BoogieGenerator.MultisetMultiplicity(tok, TrExpr(s), elmtBox), Expr.Literal(0)); + result.tok = tok; + return result; + } + + + /// + /// Translate like s[Box(elmt)], but try to avoid as many set functions as possible in the + /// translation, because such functions can mess up triggering. + /// + public Expr TrInSet(IOrigin tok, Expr elmt, Expression s, Type elmtType, bool isFiniteSet, bool aggressive, out bool performedRewrite) { + Contract.Requires(tok != null); + Contract.Requires(elmt != null); + Contract.Requires(s != null); + Contract.Requires(elmtType != null); + Contract.Ensures(Contract.Result() != null); + + var elmtBox = BoxIfNecessary(tok, elmt, elmtType); + var r = TrInSet_Aux(tok, elmt, elmtBox, s, isFiniteSet, aggressive, out performedRewrite); + Contract.Assert(performedRewrite == RewriteInExpr(s, aggressive)); // sanity check + return r; + } + /// + /// The worker routine for TrInSet. This method takes both "elmt" and "elmtBox" as parameters, + /// using the former when the unboxed form is needed and the latter when the boxed form is needed. + /// This gives the caller the flexibility to pass in either "o, Box(o)" or "Unbox(bx), bx". + /// Note: This method must be kept in synch with RewriteInExpr. + /// + public Expr TrInSet_Aux(IOrigin tok, Expr elmt, Expr elmtBox, Expression s, bool isFiniteSet, bool aggressive, + out bool performedRewrite, Func extractObjectFromMemoryLocation = null) { + Contract.Requires(tok != null); + Contract.Requires(elmt != null); + Contract.Requires(elmtBox != null); + Contract.Requires(s != null); + Contract.Ensures(Contract.Result() != null); + + performedRewrite = true; // assume a rewrite will happen + s = s.Resolved; + bool pr; + if (s is BinaryExpr && aggressive) { + BinaryExpr bin = (BinaryExpr)s; + switch (bin.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Union: + return BplOr( + TrInSet_Aux(tok, elmt, elmtBox, bin.E0, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation), + TrInSet_Aux(tok, elmt, elmtBox, bin.E1, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation)); + case BinaryExpr.ResolvedOpcode.Intersection: + return BplAnd( + TrInSet_Aux(tok, elmt, elmtBox, bin.E0, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation), + TrInSet_Aux(tok, elmt, elmtBox, bin.E1, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation)); + case BinaryExpr.ResolvedOpcode.SetDifference: + return BplAnd( + TrInSet_Aux(tok, elmt, elmtBox, bin.E0, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation), + Expr.Not(TrInSet_Aux(tok, elmt, elmtBox, bin.E1, isFiniteSet, aggressive, out pr, extractObjectFromMemoryLocation))); + default: + break; + } + } else if (s is SetDisplayExpr) { + SetDisplayExpr disp = (SetDisplayExpr)s; + Expr disjunction = null; + foreach (Expression a in disp.Elements) { + var oneElem = TrExpr(a); + oneElem = extractObjectFromMemoryLocation != null ? extractObjectFromMemoryLocation(oneElem) : oneElem; + Expr disjunct = Expr.Eq(elmt, oneElem); + if (disjunction == null) { + disjunction = disjunct; + } else { + disjunction = BplOr(disjunction, disjunct); + } + } + if (disjunction == null) { + return Expr.False; + } else { + return disjunction; + } + } else if (s is SetComprehension) { + var compr = (SetComprehension)s; + // Translate "elmt in set xs | R :: T[xs]" into: + // exists xs :: CorrectType(xs) && R && elmt==T[xs] + // or if "T[xs]" is "xs", then: + // CorrectType(elmt) && R[xs := elmt] + if (compr.TermIsSimple && extractObjectFromMemoryLocation == null) { + // CorrectType(elmt) && R[xs := elmt] + // Note, we can always use NOALLOC here. + Expr typeAntecedent = BoogieGenerator.GetWhereClause(GetToken(compr), elmt, compr.BoundVars[0].Type, this, NOALLOC) ?? Expr.True; + var range = Substitute(compr.Range, compr.BoundVars[0], new BoogieWrapper(elmt, compr.BoundVars[0].Type)); + return BplAnd(typeAntecedent, TrExpr(range)); + } else { + // exists xs :: CorrectType(xs) && R && elmt==T[xs] + List freeOfAlloc = BoundedPool.HasBounds(compr.Bounds, BoundedPool.PoolVirtues.IndependentOfAlloc_or_ExplicitAlloc); + var bvars = new List(); + Expr typeAntecedent = TrBoundVariables(compr.BoundVars, bvars, false, freeOfAlloc) ?? Expr.True; + var eq = Expr.Eq(elmtBox, BoxIfNecessary(GetToken(compr), extractObjectFromMemoryLocation != null ? extractObjectFromMemoryLocation(TrExpr(compr.Term)) : TrExpr(compr.Term), compr.Term.Type)); + var ebody = BplAnd(BplAnd(typeAntecedent, TrExpr(compr.Range)), eq); + var triggers = BoogieGenerator.TrTrigger(this, compr.Attributes, GetToken(compr)); + return new Boogie.ExistsExpr(GetToken(compr), bvars, triggers, ebody); + } + } + + if (extractObjectFromMemoryLocation != null) { + // Translate "elmt in s" into "exists xs :: xs in s && elem == xs.0" + // with extractObjectFromMemoryLocation = (xs) => xs.0 + var xs = new BoundVariable(GetToken(s), new TypedIdent(tok, "xs", BoogieGenerator.TrType(s.Type.AsSetType.Arg))); + var xsExpr = new Boogie.IdentifierExpr(xs.tok, xs); + var xsExprBoxExtract = extractObjectFromMemoryLocation(xsExpr); + // Create the trigger Set#IsMember(xs, s) + var trigger = new Trigger(tok, false, [ + BoogieGenerator.FunctionCall(tok, BuiltinFunction.SetIsMember, Boogie.Type.Bool, xsExpr, TrExpr(s)) + ]); + var ebody = Expr.Eq(elmt, xsExprBoxExtract); + return new Boogie.ExistsExpr(GetToken(s), new List() { xs }, trigger, ebody); + } + performedRewrite = false; + + return BoogieGenerator.IsSetMember(tok, TrExpr(s), elmtBox, isFiniteSet); + } + + /// + /// This method returns "true" iff TrInSet_Aux/TrInMultiSet_Aux will rewrite an expression "x in s". + /// Note: This method must be kept in synch with TrInSet_Aux/TrInMultiSet_Aux. + /// + public static bool RewriteInExpr(Expression s, bool aggressive) { + Contract.Requires(s != null); + + s = s.Resolved; + if (s is BinaryExpr && aggressive) { + BinaryExpr bin = (BinaryExpr)s; + switch (bin.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Union: + case BinaryExpr.ResolvedOpcode.Intersection: + case BinaryExpr.ResolvedOpcode.SetDifference: + case BinaryExpr.ResolvedOpcode.MultiSetUnion: + case BinaryExpr.ResolvedOpcode.MultiSetIntersection: + return true; + default: + break; + } + } else if (s is SetDisplayExpr || s is MultiSetDisplayExpr) { + return true; + } else if (s is SetComprehension) { + return true; + } + return false; + } + + + private Expr BinaryExprCanCallAssumption(BinaryExpr expr, CanCallOptions cco) { + // The short-circuiting boolean operators &&, ||, and ==> end up duplicating their + // left argument. Therefore, we first try to re-associate the expression to make + // left arguments smaller. + var newExpr = ReAssociateToTheRight(ref expr); + if (newExpr != null) { + return CanCallAssumption(newExpr, cco); + } + + var t0 = CanCallAssumption(expr.E0, cco); + var t1 = CanCallAssumption(expr.E1, cco); + switch (expr.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.And: + case BinaryExpr.ResolvedOpcode.Imp: + t1 = BplImp(TrExpr(expr.E0), t1); + break; + case BinaryExpr.ResolvedOpcode.Or: + t1 = BplImp(Expr.Not(TrExpr(expr.E0)), t1); + break; + case BinaryExpr.ResolvedOpcode.EqCommon: + case BinaryExpr.ResolvedOpcode.NeqCommon: { + Expr r = Expr.True; + if (cco is not { SkipIsA: true }) { + if (expr.E0 is { Type: { AsDatatype: { } dt0 }, Resolved: not DatatypeValue }) { + var funcId = new FunctionCall(new Boogie.IdentifierExpr(expr.Origin, "$IsA#" + dt0.FullSanitizedName, Boogie.Type.Bool)); + r = BplAnd(r, new NAryExpr(expr.Origin, funcId, new List { TrExpr(expr.E0) })); + } + if (expr.E1 is { Type: { AsDatatype: { } dt1 }, Resolved: not DatatypeValue }) { + var funcId = new FunctionCall(new Boogie.IdentifierExpr(expr.Origin, "$IsA#" + dt1.FullSanitizedName, Boogie.Type.Bool)); + r = BplAnd(r, new NAryExpr(expr.Origin, funcId, new List { TrExpr(expr.E1) })); + } + } + return BplAnd(r, BplAnd(t0, t1)); + } + case BinaryExpr.ResolvedOpcode.Mul: + if (7 <= BoogieGenerator.options.ArithMode) { + if (expr.E0.Type.IsNumericBased(Type.NumericPersuasion.Int) && !BoogieGenerator.DisableNonLinearArithmetic) { + // Produce a useful fact about the associativity of multiplication. It is a bit dicey to do as an axiom. + // Change (k*A)*B or (A*k)*B into (A*B)*k, where k is a numeric literal + if (expr.E0.Resolved is BinaryExpr left && left.ResolvedOp == BinaryExpr.ResolvedOpcode.Mul) { + Expr r = Expr.True; + if (left.E0.Resolved is LiteralExpr) { + // (K*A)*B == (A*B)*k + var y = Expression.CreateMul(Expression.CreateMul(left.E1, expr.E1), left.E0); + var eq = Expression.CreateEq(expr, y, expr.E0.Type); + r = BplAnd(r, TrExpr(eq)); + } + if (left.E1.Resolved is LiteralExpr) { + // (A*k)*B == (A*B)*k + var y = Expression.CreateMul(Expression.CreateMul(left.E0, expr.E1), left.E1); + var eq = Expression.CreateEq(expr, y, expr.E0.Type); + r = BplAnd(r, TrExpr(eq)); + } + if (r != Expr.True) { + return BplAnd(BplAnd(t0, t1), r); + } + } + } + } + break; + } + return BplAnd(t0, t1); + } + + /// + /// If "expr" is a binary boolean operation, then try to re-associate it to make the left argument smaller. + /// If it is possible, then "true" is returned and "expr" returns as the re-associated expression (no boolean simplifications are performed). + /// If not, then "false" is returned and "expr" is unchanged. + /// + Expression ReAssociateToTheRight(ref BinaryExpr top) { + if (Expression.StripParens(top.E0) is BinaryExpr left) { + // We have an expression of the form "(A oo B) pp C" + var A = left.E0; + var oo = left.ResolvedOp; + var B = left.E1; + var pp = top.ResolvedOp; + var C = top.E1; + + if (oo == BinaryExpr.ResolvedOpcode.And && pp == BinaryExpr.ResolvedOpcode.And) { + // rewrite (A && B) && C into A && (B && C) + return Expression.CreateAnd(A, Expression.CreateAnd(B, C, false), false); + } + + if (oo == BinaryExpr.ResolvedOpcode.And && pp == BinaryExpr.ResolvedOpcode.Imp) { + // rewrite (A && B) ==> C into A ==> (B ==> C) + return Expression.CreateImplies(A, Expression.CreateImplies(B, C, false), false); + } + + if (oo == BinaryExpr.ResolvedOpcode.Or && pp == BinaryExpr.ResolvedOpcode.Or) { + // rewrite (A || B) || C into A || (B || C) + return Expression.CreateOr(A, Expression.CreateOr(B, C, false), false); + } + + if (oo == BinaryExpr.ResolvedOpcode.Imp && pp == BinaryExpr.ResolvedOpcode.Or) { + // rewrite (A ==> B) || C into A ==> (B || C) + return Expression.CreateImplies(A, Expression.CreateOr(B, C, false), false); + } + } + return null; + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/Expressions/TranslateMultiSetDisplayExpr.cs b/Source/DafnyCore/Verifier/Expressions/TranslateMultiSetDisplayExpr.cs new file mode 100644 index 00000000000..45e2dac042e --- /dev/null +++ b/Source/DafnyCore/Verifier/Expressions/TranslateMultiSetDisplayExpr.cs @@ -0,0 +1,36 @@ +namespace Microsoft.Dafny; + +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using System.Numerics; +using Dafny; +using Microsoft.BaseTypes; +using Microsoft.Boogie; +using Bpl = Microsoft.Boogie; +using static Microsoft.Dafny.Util; + +public partial class BoogieGenerator { + public partial class ExpressionTranslator { + + private Expr TranslateMultiSetDisplayExpr(MultiSetDisplayExpr displayExpr) { + Expr result = BoogieGenerator.FunctionCall(GetToken(displayExpr), BuiltinFunction.MultiSetEmpty, Predef.BoxType); + var isLit = true; + foreach (Expression ee in displayExpr.Elements) { + var rawElement = TrExpr(ee); + isLit = isLit && BoogieGenerator.IsLit(rawElement); + var ss = BoxIfNecessary(GetToken(displayExpr), rawElement, cce.NonNull(ee.Type)); + result = BoogieGenerator.FunctionCall(GetToken(displayExpr), BuiltinFunction.MultiSetUnionOne, Predef.BoxType, result, + ss); + } + + if (isLit) { + // Lit-lifting: All elements are lit, so the multiset is Lit too + result = MaybeLit(result, Predef.BoxType); + } + + return result; + } + } +} \ No newline at end of file