From 623a87c132abec61b5c74a6a00a7b162073a6a8d Mon Sep 17 00:00:00 2001 From: boehmes Date: Thu, 27 Sep 2012 17:13:42 +0200 Subject: Boogie: new syntax for integer division and modulus: use div and mod instead of / and % --- Binaries/DafnyPrelude.bpl | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index ca526173..53e8e86a 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -613,15 +613,15 @@ var $Tick: TickType; // -- Arithmetic ------------------------------------------------- // --------------------------------------------------------------- -// the connection between % and / -axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y); +// the connection between mod and div +axiom (forall x:int, y:int :: {x mod y} {x div y} x mod y == x - x div y * y); // remainder is always Euclidean Modulus. -axiom (forall x:int, y:int :: {x % y} 0 < y ==> 0 <= x % y && x % y < y); -axiom (forall x:int, y:int :: {x % y} y < 0 ==> 0 <= x % y && x % y < -y); +axiom (forall x:int, y:int :: {x mod y} 0 < y ==> 0 <= x mod y && x mod y < y); +axiom (forall x:int, y:int :: {x mod y} y < 0 ==> 0 <= x mod y && x mod y < -y); -// the following axiom has some unfortunate matching, but it does state a property about % that +// the following axiom has some unfortunate matching, but it does state a property about mod that // is sometimes useful -axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b); +axiom (forall a: int, b: int, d: int :: { a mod d, b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b); // --------------------------------------------------------------- -- cgit v1.2.3 From 43b80b13bd24bb789849aac3385df6ac4a8233be Mon Sep 17 00:00:00 2001 From: boehmes Date: Thu, 27 Sep 2012 17:13:45 +0200 Subject: Boogie: added type 'real' with overloaded arithmetic operations plus real division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested) --- Binaries/UnivBackPred2.smt2 | 3 +- Source/AbsInt/IntervalDomain.cs | 33 +- Source/Basetypes/BigDec.cs | 200 ++++-- Source/Core/AbsyExpr.cs | 259 +++++++- Source/Core/AbsyType.cs | 25 + Source/Core/BoogiePL.atg | 52 +- Source/Core/Parser.cs | 980 +++++++++++++++-------------- Source/Core/Scanner.cs | 355 ++++++----- Source/Core/Util.cs | 6 + Source/Provers/SMTLib/SMTLibLineariser.cs | 39 +- Source/Provers/SMTLib/SMTLibNamer.cs | 6 +- Source/Provers/SMTLib/TypeDeclCollector.cs | 2 +- Source/Provers/Z3api/ContextLayer.cs | 38 +- Source/Provers/Z3api/TypeAdapter.cs | 9 +- Source/Provers/Z3api/VCExprVisitor.cs | 60 +- Source/VCExpr/BigLiteralAbstracter.cs | 8 +- Source/VCExpr/Boogie2VCExpr.cs | 68 +- Source/VCExpr/SimplifyLikeLineariser.cs | 63 +- Source/VCExpr/TypeErasure.cs | 48 +- Source/VCExpr/VCExprAST.cs | 74 ++- Source/VCExpr/VCExprASTPrinter.cs | 24 +- Source/VCExpr/VCExprASTVisitors.cs | 40 ++ Test/aitest1/Answer | 2 +- Test/inline/Answer | 6 +- Test/test0/Answer | 36 ++ Test/test0/ModifiedBag.bpl | 2 +- Test/test0/PrettyPrint.bpl | 22 + Test/test0/Prog0.bpl | 2 +- Test/test1/Answer | 19 + Test/test1/IntReal.bpl | 48 ++ Test/test1/runtest.bat | 1 + Test/test2/strings-no-where.bpl | 2 +- Test/test2/strings-where.bpl | 2 +- Test/test20/Answer | 8 +- Test/test20/Prog0.bpl | 2 +- Test/test20/Prog1.bpl | 2 +- Test/test21/Answer | 9 + Test/test21/Real.bpl | 17 + Test/test21/runtest.bat | 4 +- 39 files changed, 1825 insertions(+), 751 deletions(-) create mode 100644 Test/test1/IntReal.bpl create mode 100644 Test/test21/Real.bpl (limited to 'Binaries') diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2 index d3e3777f..9bb05bfb 100644 --- a/Binaries/UnivBackPred2.smt2 +++ b/Binaries/UnivBackPred2.smt2 @@ -3,7 +3,6 @@ (set-info :category "industrial") (declare-sort |T@U| 0) (declare-sort |T@T| 0) -(declare-fun int_div (Int Int) Int) -(declare-fun int_mod (Int Int) Int) +(declare-fun real_pow (Real Real) Real) (declare-fun UOrdering2 (|T@U| |T@U|) Bool) (declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool) diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 247a357d..51391105 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -632,6 +632,10 @@ namespace Microsoft.Boogie.AbstractInterpretation var n = ((BigNum)node.Val).ToBigInteger; Lo = n; Hi = n + 1; + } else if (node.Val is BigDec) { + var n = ((BigDec)node.Val).Floor(-BigInteger.Pow(10, 12), BigInteger.Pow(10, 12)); + Lo = n; + Hi = n + 1; } else if (node.Val is bool) { if ((bool)node.Val) { // true @@ -646,7 +650,7 @@ namespace Microsoft.Boogie.AbstractInterpretation return node; } public override Expr VisitIdentifierExpr(IdentifierExpr node) { - if (node.Type.IsBool || node.Type.IsInt) { + if (node.Type.IsBool || node.Type.IsInt || node.Type.IsReal) { Node.GetBounds(N, node.Decl, out Lo, out Hi); } return node; @@ -655,7 +659,18 @@ namespace Microsoft.Boogie.AbstractInterpretation if (node.Fun is UnaryOperator) { var op = (UnaryOperator)node.Fun; Contract.Assert(node.Args.Length == 1); - if (op.Op == UnaryOperator.Opcode.Not) { + if (op.Op == UnaryOperator.Opcode.Neg) { + BigInteger? lo, hi; + VisitExpr(node.Args[0]); + lo = Lo; hi = Hi; + if (hi != null) { + Lo = 1 - hi; + } + if (lo != null) { + Hi = -lo; + } + } + else if (op.Op == UnaryOperator.Opcode.Not) { VisitExpr(node.Args[0]); Contract.Assert((Lo == null && Hi == null) || (Lo == null && (BigInteger)Hi == 1) || @@ -803,6 +818,20 @@ namespace Microsoft.Boogie.AbstractInterpretation Hi = hi1; } break; + case BinaryOperator.Opcode.RealDiv: + // this uses an incomplete approximation that could be tightened up + if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { + Lo = new BigInteger(0); + Hi = hi1; + } + break; + case BinaryOperator.Opcode.Pow: + // this uses an incomplete approximation that could be tightened up + if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { + Lo = new BigInteger(0); + Hi = hi1; + } + break; default: break; } diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs index 78b19794..6059539b 100755 --- a/Source/Basetypes/BigDec.cs +++ b/Source/Basetypes/BigDec.cs @@ -19,59 +19,86 @@ namespace Microsoft.Basetypes { // the internal representation [Rep] - internal readonly BIM mantisse; + internal readonly BIM mantissa; [Rep] - internal readonly BIM exponent; + internal readonly int exponent; - private static readonly BIM ONE = BIM.One; - private static readonly BIM TEN = new BIM(10); + public BIM Mantissa { + get { + return mantissa; + } + } + + public int Exponent { + get { + return exponent; + } + } + + public static readonly BigDec ZERO = FromInt(0); + private static readonly BIM ten = new BIM(10); //////////////////////////////////////////////////////////////////////////// // Constructors + [Pure] + public static BigDec FromInt(int v) { + return new BigDec(v, 0); + } + [Pure] public static BigDec FromString(string v) { if (v == null) throw new FormatException(); BIM integral = BIM.Zero; BIM fraction = BIM.Zero; - BIM exponent = BIM.Zero; + int exponent = 0; int len = v.Length; int i = v.IndexOf('e'); if (i >= 0) { - exponent = BIM.Parse(v.Substring(i + 1, len - i)); + if (i + 1 == v.Length) throw new FormatException(); + exponent = Int32.Parse(v.Substring(i + 1, len - i - 1)); len = i; } - int fraction_len = 0; + int fractionLen = 0; i = v.IndexOf('.'); if (i >= 0) { - fraction = BIM.Parse(v.Substring(i + 1, len - i)); - fraction_len = len - i; + if (i + 1 == v.Length) throw new FormatException(); + fractionLen = len - i - 1; + fraction = BIM.Parse(v.Substring(i + 1, fractionLen)); len = i; } integral = BIM.Parse(v.Substring(0, len)); - while (fraction_len > 0) { - integral = integral * TEN; - exponent = exponent - ONE; + if (!fraction.IsZero) { + while (fractionLen > 0) { + integral = integral * ten; + exponent = exponent - 1; + fractionLen = fractionLen - 1; + } } return new BigDec(integral + fraction, exponent); } - internal BigDec(BIM mantisse, BIM exponent) { - while (mantisse % TEN == BIM.Zero) { - mantisse = mantisse / TEN; - exponent = exponent + ONE; + internal BigDec(BIM mantissa, int exponent) { + if (mantissa.IsZero) { + this.mantissa = mantissa; + this.exponent = 0; + } + else { + while (mantissa % ten == BIM.Zero) { + mantissa = mantissa / ten; + exponent = exponent + 1; + } + this.mantissa = mantissa; + this.exponent = exponent; } - - this.mantisse = mantisse; - this.exponent = exponent; } @@ -86,46 +113,125 @@ namespace Microsoft.Basetypes { if (!(obj is BigDec)) return false; - BigDec other = (BigDec)obj; - return (this.mantisse == other.mantisse && this.exponent == other.exponent); + return (this == (BigDec)obj); } [Pure] public override int GetHashCode() { - return this.mantisse.GetHashCode() * 13 + this.exponent.GetHashCode(); + return this.mantissa.GetHashCode() * 13 + this.exponent.GetHashCode(); } [Pure] public override string/*!*/ ToString() { Contract.Ensures(Contract.Result() != null); - return String.Format("%se%s", this.mantisse.ToString(), this.exponent.ToString()); + return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString()); + } + + + //////////////////////////////////////////////////////////////////////////// + // Conversion operations + + [Pure] + public BIM Floor(BIM? minimum, BIM? maximum) { + BIM n = this.mantissa; + + if (this.exponent >= 0) { + int e = this.exponent; + while (e > 0 && (minimum == null || minimum <= n) && (maximum == null || n <= maximum)) { + n = n * ten; + e = e - 1; + } + } + else { + int e = -this.exponent; + while (e > 0 && !n.IsZero) { + n = n / ten; + e = e - 1; + } + } + + if (minimum != null && n < minimum) + return (BIM)minimum; + else if (maximum != null && maximum < n) + return (BIM)maximum; + else + return n; + } + + [Pure] + public String ToDecimalString(int maxDigits) { + string s = this.mantissa.ToString(); + int digits = (this.mantissa >= 0) ? s.Length : s.Length - 1; + BIM max = BIM.Pow(10, maxDigits); + BIM min = -max; + + if (this.exponent >= 0) { + if (maxDigits < digits || maxDigits - digits < this.exponent) { + return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString()); + } + else { + return String.Format("{0}{1}.0", s, new string('0', this.exponent)); + } + } + else { + int exp = -this.exponent; + + if (exp < digits) { + int intDigits = digits - exp; + if (maxDigits < intDigits) { + return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString()); + } + else { + int fracDigits = Math.Min(maxDigits, digits - intDigits); + return String.Format("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits)); + } + } + else { + int fracDigits = Math.Min(maxDigits, digits); + return String.Format("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits)); + } + } } //////////////////////////////////////////////////////////////////////////// // Basic arithmetic operations + [Pure] + public BigDec Abs { + get { + return new BigDec(BIM.Abs(this.mantissa), this.exponent); + } + } + + [Pure] + public BigDec Negate { + get { + return new BigDec(BIM.Negate(this.mantissa), this.exponent); + } + } + [Pure] public static BigDec operator -(BigDec x) { - return new BigDec(BIM.Negate(x.mantisse), x.exponent); + return x.Negate; } [Pure] public static BigDec operator +(BigDec x, BigDec y) { - BIM m1 = x.mantisse; - BIM e1 = x.exponent; - BIM m2 = y.mantisse; - BIM e2 = y.exponent; + BIM m1 = x.mantissa; + int e1 = x.exponent; + BIM m2 = y.mantissa; + int e2 = y.exponent; if (e2 < e1) { - m1 = y.mantisse; + m1 = y.mantissa; e1 = y.exponent; - m2 = x.mantisse; + m2 = x.mantissa; e2 = x.exponent; } while (e2 > e1) { - m2 = m2 * TEN; - e2 = e2 - ONE; + m2 = m2 * ten; + e2 = e2 - 1; } return new BigDec(m1 + m2, e1); @@ -133,12 +239,12 @@ namespace Microsoft.Basetypes { [Pure] public static BigDec operator -(BigDec x, BigDec y) { - return x + (-y); + return x + y.Negate; } [Pure] public static BigDec operator *(BigDec x, BigDec y) { - return new BigDec(x.mantisse * y.mantisse, x.exponent + y.exponent); + return new BigDec(x.mantissa * y.mantissa, x.exponent + y.exponent); } @@ -147,37 +253,43 @@ namespace Microsoft.Basetypes { public bool IsPositive { get { - return (this.mantisse > BIM.Zero); + return (this.mantissa > BIM.Zero); } } public bool IsNegative { get { - return (this.mantisse < BIM.Zero); + return (this.mantissa < BIM.Zero); } } public bool IsZero { get { - return this.mantisse.IsZero; + return this.mantissa.IsZero; } } [Pure] public int CompareTo(BigDec that) { - BigDec d = this - that; - - if (d.IsZero) { + if (this.mantissa == that.mantissa && this.exponent == that.exponent) { return 0; } - else if (d.IsNegative) { - return -1; - } else { - return 1; + BigDec d = this - that; + return d.IsNegative ? -1 : 1; } } + [Pure] + public static bool operator ==(BigDec x, BigDec y) { + return x.CompareTo(y) == 0; + } + + [Pure] + public static bool operator !=(BigDec x, BigDec y) { + return x.CompareTo(y) != 0; + } + [Pure] public static bool operator <(BigDec x, BigDec y) { return x.CompareTo(y) < 0; diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index d2b8506a..61511b33 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -250,6 +250,18 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return Binary(BinaryOperator.Opcode.Mod, e1, e2); } + public static NAryExpr RealDiv(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result() != null); + return Binary(BinaryOperator.Opcode.RealDiv, e1, e2); + } + public static NAryExpr Pow(Expr e1, Expr e2) { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result() != null); + return Binary(BinaryOperator.Opcode.Pow, e1, e2); + } public static NAryExpr Subtype(Expr e1, Expr e2) { Contract.Requires(e2 != null); Contract.Requires(e1 != null); @@ -283,6 +295,10 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return new LiteralExpr(Token.NoToken, value); } + public static LiteralExpr Literal(BigDec value) { + Contract.Ensures(Contract.Result() != null); + return new LiteralExpr(Token.NoToken, value); + } private static LiteralExpr/*!*/ true_ = Literal(true); public static LiteralExpr/*!*/ True { @@ -401,7 +417,7 @@ namespace Microsoft.Boogie { } public class LiteralExpr : Expr { - public readonly object/*!*/ Val; // false, true, a BigNum, or a BvConst + public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, or a BvConst [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Val != null); @@ -418,6 +434,7 @@ namespace Microsoft.Boogie { Val = b; Type = Type.Bool; } + /// /// Creates a literal expression for the integer value "v". /// @@ -430,6 +447,18 @@ namespace Microsoft.Boogie { Type = Type.Int; } + /// + /// Creates a literal expression for the real value "v". + /// + /// + /// + public LiteralExpr(IToken/*!*/ tok, BigDec v) + : base(tok) { + Contract.Requires(tok != null); + Val = v; + Type = Type.Real; + } + /// /// Creates a literal expression for the bitvector value "v". /// @@ -487,6 +516,8 @@ namespace Microsoft.Boogie { return Type.Bool; } else if (Val is BigNum) { return Type.Int; + } else if (Val is BigDec) { + return Type.Real; } else if (Val is BvConst) { return Type.GetBvType(((BvConst)Val).Bits); } else { @@ -529,6 +560,19 @@ namespace Microsoft.Boogie { } } + public bool isBigDec { + get { + return Val is BigDec; + } + } + + public BigDec asBigDec { + get { + Contract.Assert(isBigDec); + return (BigDec)cce.NonNull(Val); + } + } + public bool isBool { get { return Val is bool; @@ -838,6 +882,7 @@ namespace Microsoft.Boogie { T Visit(MapSelect/*!*/ mapSelect); T Visit(MapStore/*!*/ mapStore); T Visit(TypeCoercion/*!*/ typeCoercion); + T Visit(ArithmeticCoercion/*!*/ arithCoercion); T Visit(IfThenElse/*!*/ ifThenElse); } [ContractClassFor(typeof(IAppliableVisitor<>))] @@ -875,6 +920,11 @@ namespace Microsoft.Boogie { throw new NotImplementedException(); } + public T Visit(ArithmeticCoercion arithCoercion) { + Contract.Requires(arithCoercion != null); + throw new NotImplementedException(); + } + public T Visit(IfThenElse ifThenElse) { Contract.Requires(ifThenElse != null); throw new NotImplementedException(); @@ -1012,6 +1062,7 @@ namespace Microsoft.Boogie { } public enum Opcode { + Neg, Not }; private Opcode op; @@ -1047,6 +1098,8 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); switch (this.op) { + case Opcode.Neg: + return "-"; case Opcode.Not: return "!"; } @@ -1061,7 +1114,7 @@ namespace Microsoft.Boogie { stream.SetToken(ref this.tok); Contract.Assert(args.Length == 1); // determine if parens are needed - int opBindingStrength = 0x60; + int opBindingStrength = 0x70; bool parensNeeded = opBindingStrength < contextBindingStrength || (fragileContext && opBindingStrength == contextBindingStrength); @@ -1099,6 +1152,14 @@ namespace Microsoft.Boogie { tpInstantiation = SimpleTypeParamInstantiation.EMPTY; Type arg0type = cce.NonNull(cce.NonNull(args[0]).Type); switch (this.op) { + case Opcode.Neg: + if (arg0type.Unify(Type.Int)) { + return Type.Int; + } + if (arg0type.Unify(Type.Real)) { + return Type.Real; + } + goto BAD_TYPE; case Opcode.Not: if (arg0type.Unify(Type.Bool)) { return Type.Bool; @@ -1119,6 +1180,8 @@ namespace Microsoft.Boogie { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); switch (this.op) { + case Opcode.Neg: + return cce.NonNull(cce.NonNull(args[0]).Type); case Opcode.Not: return Type.Bool; default: { @@ -1133,6 +1196,14 @@ namespace Microsoft.Boogie { return null; } switch (this.op) { + case Opcode.Neg: + if (argument is BigNum) { + return -((BigNum)argument); + } + if (argument is BigDec) { + return -((BigDec)argument); + } + break; case Opcode.Not: if (argument is bool) { return !((bool)argument); @@ -1161,6 +1232,8 @@ namespace Microsoft.Boogie { Mul, Div, Mod, + RealDiv, + Pow, Eq, Neq, Gt, @@ -1217,6 +1290,10 @@ namespace Microsoft.Boogie { return "div"; case Opcode.Mod: return "mod"; + case Opcode.RealDiv: + return "/"; + case Opcode.Pow: + return "**"; case Opcode.Eq: return "=="; case Opcode.Neq: @@ -1273,6 +1350,14 @@ namespace Microsoft.Boogie { opBindingStrength = 0x50; fragileRightContext = true; break; + case Opcode.RealDiv: + opBindingStrength = 0x50; + fragileRightContext = true; + break; + case Opcode.Pow: + opBindingStrength = 0x60; + fragileRightContext = true; + break; case Opcode.Eq: case Opcode.Neq: case Opcode.Gt: @@ -1326,6 +1411,8 @@ namespace Microsoft.Boogie { case Opcode.Mul: case Opcode.Div: case Opcode.Mod: + case Opcode.RealDiv: + case Opcode.Pow: case Opcode.Neq: // Neq is allowed, but not Eq case Opcode.Subtype: // These are fine @@ -1377,12 +1464,30 @@ namespace Microsoft.Boogie { case Opcode.Add: case Opcode.Sub: case Opcode.Mul: + if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) { + return Type.Int; + } + if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { + return Type.Real; + } + goto BAD_TYPE; case Opcode.Div: case Opcode.Mod: if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) { return Type.Int; } goto BAD_TYPE; + case Opcode.RealDiv: + if ((arg0type.Unify(Type.Int) || arg0type.Unify(Type.Real)) && + (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real))) { + return Type.Real; + } + goto BAD_TYPE; + case Opcode.Pow: + if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { + return Type.Real; + } + goto BAD_TYPE; case Opcode.Eq: case Opcode.Neq: // Comparison is allowed if the argument types are unifiable @@ -1406,6 +1511,9 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) { return Type.Bool; } + if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { + return Type.Bool; + } goto BAD_TYPE; case Opcode.And: case Opcode.Or: @@ -1440,10 +1548,16 @@ namespace Microsoft.Boogie { case Opcode.Add: case Opcode.Sub: case Opcode.Mul: + return cce.NonNull(args[0]).ShallowType; + case Opcode.Div: case Opcode.Mod: return Type.Int; + case Opcode.RealDiv: + case Opcode.Pow: + return Type.Real; + case Opcode.Eq: case Opcode.Neq: case Opcode.Gt: @@ -1500,16 +1614,25 @@ namespace Microsoft.Boogie { if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1) + ((BigNum)e2); } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) + ((BigDec)e2); + } break; case Opcode.Sub: if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1) - ((BigNum)e2); } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) - ((BigDec)e2); + } break; case Opcode.Mul: if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1) * ((BigNum)e2); } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) * ((BigDec)e2); + } break; case Opcode.Div: if (e1 is BigNum && e2 is BigNum) { @@ -1521,25 +1644,43 @@ namespace Microsoft.Boogie { return /* TODO: right semantics? */ ((BigNum)e1) % ((BigNum)e2); } break; + case Opcode.RealDiv: + // TODO: add partial evaluation fro real division + break; + case Opcode.Pow: + // TODO: add partial evaluation fro real exponentiation + break; case Opcode.Lt: if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1) < ((BigNum)e2); } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) < ((BigDec)e2); + } break; case Opcode.Le: if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1) <= ((BigNum)e2); } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) <= ((BigDec)e2); + } break; case Opcode.Gt: if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1) > ((BigNum)e2); } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) > ((BigDec)e2); + } break; case Opcode.Ge: if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1) >= ((BigNum)e2); } + if (e1 is BigDec && e2 is BigDec) { + return ((BigDec)e1) >= ((BigDec)e2); + } break; case Opcode.And: @@ -1724,7 +1865,7 @@ namespace Microsoft.Boogie { stream.SetToken(ref this.tok); Contract.Assert(args.Length == 1); // determine if parens are needed - int opBindingStrength = 0x70; + int opBindingStrength = 0x80; bool parensNeeded = opBindingStrength < contextBindingStrength || (fragileContext && opBindingStrength == contextBindingStrength); @@ -1782,6 +1923,114 @@ namespace Microsoft.Boogie { } + public class ArithmeticCoercion : IAppliable { + public enum CoercionType { + ToInt, + ToReal + } + + private IToken/*!*/ tok; + public readonly CoercionType Coercion; + private readonly string name; + private readonly Type type; + private readonly Type argType; + private readonly int hashCode; + + public ArithmeticCoercion(IToken tok, CoercionType coercion) { + this.tok = tok; + this.Coercion = coercion; + + switch (coercion) { + case CoercionType.ToInt: + this.name = "int"; + this.type = Type.Int; + this.argType = Type.Real; + this.hashCode = 1; + break; + case CoercionType.ToReal: + this.name = "real"; + this.type = Type.Real; + this.argType = Type.Int; + this.hashCode = 2; + break; + default: + Contract.Assert(false); + break; + } + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result() != null); + return this.name; + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) { + ArithmeticCoercion ac = other as ArithmeticCoercion; + return ac != null && this.Coercion == ac.Coercion; + } + + [Pure] + public override int GetHashCode() { + return this.hashCode; + } + + public string/*!*/ FunctionName { + get { + return this.name; + } + } + + public int ArgumentCount { + get { + return 1; + } + } + + virtual public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + //Contract.Requires(stream != null); + //Contract.Requires(args != null); + stream.Write(this.name); + stream.Write("("); + args.Emit(stream); + stream.Write(")"); + } + + public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { + //Contract.Requires(subjectForErrorReporting != null); + //Contract.Requires(rc != null); + } + + public virtual Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + //Contract.Requires(tc != null); + //Contract.Requires(args != null); + Contract.Assert(args.Length == 1); + Contract.Ensures(args != null); + Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); + + tpInstantiation = SimpleTypeParamInstantiation.EMPTY; + + if (!cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType)) { + tc.Error(this.tok, "argument type {0} does not match expected type {1}", cce.NonNull(args[0]).Type, this.argType); + } + + return this.type; + } + + public Type ShallowType(ExprSeq args) { + //Contract.Requires(args != null); + Contract.Ensures(Contract.Result() != null); + return this.type; + } + + public virtual T Dispatch(IAppliableVisitor visitor) { + //Contract.Requires(visitor != null); + return visitor.Visit(this); + } + } + public class NAryExpr : Expr { [Additive] [Peer] @@ -1949,7 +2198,7 @@ namespace Microsoft.Boogie { bool withRhs) { Contract.Requires(args != null); Contract.Requires(stream != null); - const int opBindingStrength = 0x80; + const int opBindingStrength = 0x90; bool parensNeeded = opBindingStrength < contextBindingStrength || (fragileContext && opBindingStrength == contextBindingStrength); @@ -2440,7 +2689,7 @@ namespace Microsoft.Boogie { public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); stream.SetToken(this); - int opBindingStrength = 0x80; + int opBindingStrength = 0x90; bool parensNeeded = opBindingStrength < contextBindingStrength || (fragileContext && opBindingStrength == contextBindingStrength); diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 706d6298..d78e0d34 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -239,6 +239,11 @@ namespace Microsoft.Boogie { return false; } } + public virtual bool IsReal { + get { + return false; + } + } public virtual bool IsBool { get { return false; @@ -330,6 +335,7 @@ namespace Microsoft.Boogie { } public static readonly Type/*!*/ Int = new BasicType(SimpleType.Int); + public static readonly Type/*!*/ Real = new BasicType(SimpleType.Real); public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool); private static BvType[] bvtypeCache; @@ -865,6 +871,8 @@ namespace Microsoft.Boogie { switch (T) { case SimpleType.Int: return "int"; + case SimpleType.Real: + return "real"; case SimpleType.Bool: return "bool"; } @@ -982,6 +990,11 @@ namespace Microsoft.Boogie { return this.T == SimpleType.Int; } } + public override bool IsReal { + get { + return this.T == SimpleType.Real; + } + } public override bool IsBool { get { return this.T == SimpleType.Bool; @@ -1883,6 +1896,12 @@ Contract.Requires(that != null); return p != null && p.IsInt; } } + public override bool IsReal { + get { + Type p = ProxyFor; + return p != null && p.IsReal; + } + } public override bool IsBool { get { Type p = ProxyFor; @@ -2726,6 +2745,11 @@ Contract.Requires(that != null); return ExpandedType.IsInt; } } + public override bool IsReal { + get { + return ExpandedType.IsReal; + } + } public override bool IsBool { get { return ExpandedType.IsBool; @@ -3499,6 +3523,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); public enum SimpleType { Int, + Real, Bool }; diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 26b70bd3..96ba9824 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -145,7 +145,8 @@ TOKENS string = quote { regularStringChar | "\\\"" } quote. - float = digit {digit} '.' {digit}. + decimal = digit {digit} 'e' [ '-' ] digit {digit} . + float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] . COMMENTS FROM "/*" TO "*/" NESTED COMMENTS FROM "//" TO lf @@ -313,6 +314,7 @@ TypeArgs TypeAtom = (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; .) ( "int" (. ty = new BasicType(t, SimpleType.Int); .) + | "real" (. ty = new BasicType(t, SimpleType.Real); .) | "bool" (. ty = new BasicType(t, SimpleType.Bool); .) /* note: bitvectors are handled in UnresolvedTypeIdentifier */ | @@ -1162,9 +1164,9 @@ AddOp /*------------------------------------------------------------------------*/ Factor = (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .) - UnaryExpression + Power { MulOp - UnaryExpression (. e0 = Expr.Binary(x, op, e0, e1); .) + Power (. e0 = Expr.Binary(x, op, e0, e1); .) } . @@ -1173,16 +1175,28 @@ MulOp ( "*" (. x = t; op=BinaryOperator.Opcode.Mul; .) | "div" (. x = t; op=BinaryOperator.Opcode.Div; .) | "mod" (. x = t; op=BinaryOperator.Opcode.Mod; .) + | "/" (. x = t; op=BinaryOperator.Opcode.RealDiv; .) ) . +/*------------------------------------------------------------------------*/ +Power += (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .) + UnaryExpression + [ + "**" (. x = t; .) + /* recurse because exponentation is right-associative */ + Power (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1); .) + ] + . + /*------------------------------------------------------------------------*/ UnaryExpression = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; .) ( "-" (. x = t; .) - UnaryExpression (. e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); .) + UnaryExpression (. e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); .) | NegOp (. x = t; .) UnaryExpression (. e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); .) | CoercionExpression @@ -1271,7 +1285,7 @@ ArrayExpression /*------------------------------------------------------------------------*/ AtomExpression -= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; ExprSeq/*!*/ es; VariableSeq/*!*/ ds; Trigger trig; TypeVariableSeq/*!*/ typeParams; IdentifierExpr/*!*/ id; @@ -1283,6 +1297,7 @@ AtomExpression ( "false" (. e = new LiteralExpr(t, false); .) | "true" (. e = new LiteralExpr(t, true); .) | Nat (. e = new LiteralExpr(t, bn); .) + | Dec (. e = new LiteralExpr(t, bd); .) | BvLit (. e = new LiteralExpr(t, bn, n); .) | Ident (. id = new IdentifierExpr(x, x.val); e = id; .) @@ -1298,6 +1313,16 @@ AtomExpression Expression ")" (. e = new OldExpr(x, e); .) + | "int" (. x = t; .) + "(" + Expression + ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new ExprSeq(e)); .) + + | "real" (. x = t; .) + "(" + Expression + ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new ExprSeq(e)); .) + | "(" ( Expression (. if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + "are not allowed"); .) @@ -1481,6 +1506,23 @@ Nat .) . +/*------------------------------------------------------------------------*/ +Dec += (. string s = ""; .) + ( + decimal (. s = t.val; .) + | + float (. s = t.val; .) + ) + (. try { + n = BigDec.FromString(s); + } catch (FormatException) { + this.SemErr("incorrectly formatted number"); + n = BigDec.ZERO; + } + .) + . + /*------------------------------------------------------------------------*/ BvLit = diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 8638d9c3..0a10b0a1 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -23,8 +23,9 @@ public class Parser { public const int _bvlit = 2; public const int _digits = 3; public const int _string = 4; - public const int _float = 5; - public const int maxT = 88; + public const int _decimal = 5; + public const int _float = 6; + public const int maxT = 92; const bool T = true; const bool x = false; @@ -217,7 +218,7 @@ private class BvBounds : Expr { while (StartOf(1)) { switch (la.kind) { - case 19: { + case 21: { Consts(out vs); foreach(Bpl.Variable/*!*/ v in vs){ Contract.Assert(v != null); @@ -226,7 +227,7 @@ private class BvBounds : Expr { break; } - case 23: { + case 25: { Function(out ds); foreach(Bpl.Declaration/*!*/ d in ds){ Contract.Assert(d != null); @@ -235,12 +236,12 @@ private class BvBounds : Expr { break; } - case 27: { + case 29: { Axiom(out ax); Pgm.TopLevelDeclarations.Add(ax); break; } - case 28: { + case 30: { UserDefinedTypes(out ts); foreach(Declaration/*!*/ td in ts){ Contract.Assert(td != null); @@ -249,7 +250,7 @@ private class BvBounds : Expr { break; } - case 6: { + case 7: { GlobalVars(out vs); foreach(Bpl.Variable/*!*/ v in vs){ Contract.Assert(v != null); @@ -258,7 +259,7 @@ private class BvBounds : Expr { break; } - case 30: { + case 32: { Procedure(out pr, out im); Pgm.TopLevelDeclarations.Add(pr); if (im != null) { @@ -267,7 +268,7 @@ private class BvBounds : Expr { break; } - case 31: { + case 33: { Implementation(out nnim); Pgm.TopLevelDeclarations.Add(nnim); break; @@ -283,17 +284,17 @@ private class BvBounds : Expr { bool u = false; QKeyValue kv = null; bool ChildrenComplete = false; List Parents = null; - Expect(19); + Expect(21); y = t; - while (la.kind == 25) { + while (la.kind == 27) { Attribute(ref kv); } - if (la.kind == 20) { + if (la.kind == 22) { Get(); u = true; } IdsType(out xs); - if (la.kind == 21) { + if (la.kind == 23) { OrderSpec(out ChildrenComplete, out Parents); } bool makeClone = false; @@ -317,7 +318,7 @@ private class BvBounds : Expr { ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv)); } - Expect(7); + Expect(8); } void Function(out DeclarationSeq/*!*/ ds) { @@ -333,44 +334,44 @@ private class BvBounds : Expr { Expr definition = null; Expr/*!*/ tmp; - Expect(23); - while (la.kind == 25) { + Expect(25); + while (la.kind == 27) { Attribute(ref kv); } Ident(out z); - if (la.kind == 17) { + if (la.kind == 19) { TypeParams(out typeParamTok, out typeParams); } - Expect(8); + Expect(9); if (StartOf(2)) { VarOrType(out tyd); arguments.Add(new Formal(tyd.tok, tyd, true)); - while (la.kind == 11) { + while (la.kind == 12) { Get(); VarOrType(out tyd); arguments.Add(new Formal(tyd.tok, tyd, true)); } } - Expect(9); - if (la.kind == 24) { + Expect(10); + if (la.kind == 26) { Get(); - Expect(8); - VarOrType(out tyd); Expect(9); + VarOrType(out tyd); + Expect(10); retTyd = tyd; - } else if (la.kind == 10) { + } else if (la.kind == 11) { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, "", retTy); - } else SynErr(89); - if (la.kind == 25) { + } else SynErr(93); + if (la.kind == 27) { Get(); Expression(out tmp); definition = tmp; - Expect(26); - } else if (la.kind == 7) { + Expect(28); + } else if (la.kind == 8) { Get(); - } else SynErr(90); + } else SynErr(94); if (retTyd == null) { // construct a dummy type for the case of syntax error tyd = new TypedIdent(t, "", new BasicType(t, SimpleType.Int)); @@ -451,40 +452,40 @@ private class BvBounds : Expr { void Axiom(out Axiom/*!*/ m) { Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; - Expect(27); - while (la.kind == 25) { + Expect(29); + while (la.kind == 27) { Attribute(ref kv); } IToken/*!*/ x = t; Proposition(out e); - Expect(7); + Expect(8); m = new Axiom(x,e, null, kv); } void UserDefinedTypes(out List/*!*/ ts) { Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List (); - Expect(28); - while (la.kind == 25) { + Expect(30); + while (la.kind == 27) { Attribute(ref kv); } UserDefinedType(out decl, kv); ts.Add(decl); - while (la.kind == 11) { + while (la.kind == 12) { Get(); UserDefinedType(out decl, kv); ts.Add(decl); } - Expect(7); + Expect(8); } void GlobalVars(out VariableSeq/*!*/ ds) { Contract.Ensures(Contract.ValueAtReturn(out ds) != null); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null; - Expect(6); - while (la.kind == 25) { + Expect(7); + while (la.kind == 27) { Attribute(ref kv); } IdsTypeWheres(true, tyds); - Expect(7); + Expect(8); foreach(TypedIdent/*!*/ tyd in tyds){ Contract.Assert(tyd != null); ds.Add(new GlobalVariable(tyd.tok, tyd, kv)); @@ -505,9 +506,9 @@ private class BvBounds : Expr { QKeyValue kv = null; impl = null; - Expect(30); + Expect(32); ProcSignature(true, out x, out typeParams, out ins, out outs, out kv); - if (la.kind == 7) { + if (la.kind == 8) { Get(); while (StartOf(3)) { Spec(pre, mods, post); @@ -520,7 +521,7 @@ private class BvBounds : Expr { impl = new Implementation(x, x.val, typeParams, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(91); + } else SynErr(95); proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); } @@ -532,7 +533,7 @@ private class BvBounds : Expr { StmtList/*!*/ stmtList; QKeyValue kv; - Expect(31); + Expect(33); ProcSignature(false, out x, out typeParams, out ins, out outs, out kv); ImplBody(out locals, out stmtList); impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); @@ -547,7 +548,7 @@ private class BvBounds : Expr { void IdsTypeWheres(bool allowWhereClauses, TypedIdentSeq/*!*/ tyds) { Contract.Requires(tyds != null); IdsTypeWhere(allowWhereClauses, tyds); - while (la.kind == 11) { + while (la.kind == 12) { Get(); IdsTypeWhere(allowWhereClauses, tyds); } @@ -555,12 +556,12 @@ private class BvBounds : Expr { void LocalVars(VariableSeq/*!*/ ds) { Contract.Ensures(Contract.ValueAtReturn(out ds) != null); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); QKeyValue kv = null; - Expect(6); - while (la.kind == 25) { + Expect(7); + while (la.kind == 27) { Attribute(ref kv); } IdsTypeWheres(true, tyds); - Expect(7); + Expect(8); foreach(TypedIdent/*!*/ tyd in tyds){ Contract.Assert(tyd != null); ds.Add(new LocalVariable(tyd.tok, tyd, kv)); @@ -570,11 +571,11 @@ private class BvBounds : Expr { void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq/*!*/ ds) { Contract.Ensures(Contract.ValueAtReturn(out ds) != null); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); ds = new VariableSeq(); - Expect(8); + Expect(9); if (la.kind == 1) { IdsTypeWheres(allowWhereClauses, tyds); } - Expect(9); + Expect(10); foreach(TypedIdent/*!*/ tyd in tyds){ Contract.Assert(tyd != null); ds.Add(new Formal(tyd.tok, tyd, incoming)); @@ -595,7 +596,7 @@ private class BvBounds : Expr { void IdsType(out TypedIdentSeq/*!*/ tyds) { Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); TokenSeq/*!*/ ids; Bpl.Type/*!*/ ty; Idents(out ids); - Expect(10); + Expect(11); Type(out ty); tyds = new TypedIdentSeq(); foreach(Token/*!*/ id in ids){ @@ -609,7 +610,7 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new TokenSeq(); Ident(out id); xs.Add(id); - while (la.kind == 11) { + while (la.kind == 12) { Get(); Ident(out id); xs.Add(id); @@ -618,7 +619,7 @@ private class BvBounds : Expr { void Type(out Bpl.Type/*!*/ ty) { Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType; - if (la.kind == 8 || la.kind == 13 || la.kind == 14) { + if (StartOf(5)) { TypeAtom(out ty); } else if (la.kind == 1) { Ident(out tok); @@ -627,17 +628,17 @@ private class BvBounds : Expr { TypeArgs(args); } ty = new UnresolvedTypeIdentifier (tok, tok.val, args); - } else if (la.kind == 15 || la.kind == 17) { + } else if (la.kind == 17 || la.kind == 19) { MapType(out ty); - } else SynErr(92); + } else SynErr(96); } void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq/*!*/ tyds) { Contract.Requires(tyds != null); TokenSeq/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne; Idents(out ids); - Expect(10); + Expect(11); Type(out ty); - if (la.kind == 12) { + if (la.kind == 13) { Get(); Expression(out nne); if (allowWhereClauses) { @@ -657,7 +658,7 @@ private class BvBounds : Expr { void Expression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; ImpliesExpression(false, out e0); - while (la.kind == 50 || la.kind == 51) { + while (la.kind == 52 || la.kind == 53) { EquivOp(); x = t; ImpliesExpression(false, out e1); @@ -667,17 +668,20 @@ private class BvBounds : Expr { void TypeAtom(out Bpl.Type/*!*/ ty) { Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; - if (la.kind == 13) { + if (la.kind == 14) { Get(); ty = new BasicType(t, SimpleType.Int); - } else if (la.kind == 14) { + } else if (la.kind == 15) { + Get(); + ty = new BasicType(t, SimpleType.Real); + } else if (la.kind == 16) { Get(); ty = new BasicType(t, SimpleType.Bool); - } else if (la.kind == 8) { + } else if (la.kind == 9) { Get(); Type(out ty); - Expect(9); - } else SynErr(93); + Expect(10); + } else SynErr(97); } void Ident(out IToken/*!*/ x) { @@ -691,7 +695,7 @@ private class BvBounds : Expr { void TypeArgs(TypeSeq/*!*/ ts) { Contract.Requires(ts != null); IToken/*!*/ tok; Type/*!*/ ty; - if (la.kind == 8 || la.kind == 13 || la.kind == 14) { + if (StartOf(5)) { TypeAtom(out ty); ts.Add(ty); if (StartOf(2)) { @@ -704,10 +708,10 @@ private class BvBounds : Expr { if (StartOf(2)) { TypeArgs(ts); } - } else if (la.kind == 15 || la.kind == 17) { + } else if (la.kind == 17 || la.kind == 19) { MapType(out ty); ts.Add(ty); - } else SynErr(94); + } else SynErr(98); } void MapType(out Bpl.Type/*!*/ ty) { @@ -717,16 +721,16 @@ private class BvBounds : Expr { Type/*!*/ result; TypeVariableSeq/*!*/ typeParameters = new TypeVariableSeq(); - if (la.kind == 17) { + if (la.kind == 19) { TypeParams(out nnTok, out typeParameters); tok = nnTok; } - Expect(15); + Expect(17); if (tok == null) tok = t; if (StartOf(2)) { Types(arguments); } - Expect(16); + Expect(18); Type(out result); ty = new MapType(tok, typeParameters, arguments, result); @@ -734,10 +738,10 @@ private class BvBounds : Expr { void TypeParams(out IToken/*!*/ tok, out Bpl.TypeVariableSeq/*!*/ typeParams) { Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); TokenSeq/*!*/ typeParamToks; - Expect(17); + Expect(19); tok = t; Idents(out typeParamToks); - Expect(18); + Expect(20); typeParams = new TypeVariableSeq (); foreach(Token/*!*/ id in typeParamToks){ Contract.Assert(id != null); @@ -749,7 +753,7 @@ private class BvBounds : Expr { Contract.Requires(ts != null); Bpl.Type/*!*/ ty; Type(out ty); ts.Add(ty); - while (la.kind == 11) { + while (la.kind == 12) { Get(); Type(out ty); ts.Add(ty); @@ -761,21 +765,21 @@ private class BvBounds : Expr { Parents = null; bool u; IToken/*!*/ parent; - Expect(21); + Expect(23); Parents = new List (); u = false; - if (la.kind == 1 || la.kind == 20) { - if (la.kind == 20) { + if (la.kind == 1 || la.kind == 22) { + if (la.kind == 22) { Get(); u = true; } Ident(out parent); Parents.Add(new ConstantParent ( new IdentifierExpr(parent, parent.val), u)); - while (la.kind == 11) { + while (la.kind == 12) { Get(); u = false; - if (la.kind == 20) { + if (la.kind == 22) { Get(); u = true; } @@ -784,7 +788,7 @@ private class BvBounds : Expr { new IdentifierExpr(parent, parent.val), u)); } } - if (la.kind == 22) { + if (la.kind == 24) { Get(); ChildrenComplete = true; } @@ -794,7 +798,7 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out tyd) != null); string/*!*/ varName = ""; Bpl.Type/*!*/ ty; IToken/*!*/ tok; Type(out ty); tok = ty.tok; - if (la.kind == 10) { + if (la.kind == 11) { Get(); if (ty is UnresolvedTypeIdentifier && cce.NonNull(ty as UnresolvedTypeIdentifier).Arguments.Length == 0) { @@ -820,7 +824,7 @@ private class BvBounds : Expr { if (la.kind == 1) { WhiteSpaceIdents(out paramTokens); } - if (la.kind == 29) { + if (la.kind == 31) { Get(); Type(out body); synonym = true; @@ -852,15 +856,15 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null); IToken/*!*/ typeParamTok; typeParams = new TypeVariableSeq(); outs = new VariableSeq(); kv = null; - while (la.kind == 25) { + while (la.kind == 27) { Attribute(ref kv); } Ident(out name); - if (la.kind == 17) { + if (la.kind == 19) { TypeParams(out typeParamTok, out typeParams); } ProcFormals(true, allowWhereClausesOnFormals, out ins); - if (la.kind == 24) { + if (la.kind == 26) { Get(); ProcFormals(false, allowWhereClausesOnFormals, out outs); } @@ -868,7 +872,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { void Spec(RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; - if (la.kind == 32) { + if (la.kind == 34) { Get(); if (la.kind == 1) { Idents(out ms); @@ -878,19 +882,19 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } } - Expect(7); - } else if (la.kind == 33) { + Expect(8); + } else if (la.kind == 35) { Get(); SpecPrePost(true, pre, post); - } else if (la.kind == 34 || la.kind == 35) { + } else if (la.kind == 36 || la.kind == 37) { SpecPrePost(false, pre, post); - } else SynErr(95); + } else SynErr(99); } void ImplBody(out VariableSeq/*!*/ locals, out StmtList/*!*/ stmtList) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new VariableSeq(); - Expect(25); - while (la.kind == 6) { + Expect(27); + while (la.kind == 7) { LocalVars(locals); } StmtList(out stmtList); @@ -898,25 +902,25 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { void SpecPrePost(bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; - if (la.kind == 34) { + if (la.kind == 36) { Get(); tok = t; - while (la.kind == 25) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); - Expect(7); + Expect(8); pre.Add(new Requires(tok, free, e, null, kv)); - } else if (la.kind == 35) { + } else if (la.kind == 37) { Get(); tok = t; - while (la.kind == 25) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); - Expect(7); + Expect(8); post.Add(new Ensures(tok, free, e, null, kv)); - } else SynErr(96); + } else SynErr(100); } void StmtList(out StmtList/*!*/ stmtList) { @@ -929,8 +933,8 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { StructuredCmd ec = null; StructuredCmd/*!*/ ecn; TransferCmd tc = null; TransferCmd/*!*/ tcn; - while (StartOf(5)) { - if (StartOf(6)) { + while (StartOf(6)) { + if (StartOf(7)) { LabelOrCmd(out c, out label); if (c != null) { // LabelOrCmd read a Cmd @@ -953,7 +957,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { cs = new CmdSeq(); } - } else if (la.kind == 38 || la.kind == 40 || la.kind == 43) { + } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) { StructuredCmd(out ecn); ec = ecn; if (startToken == null) { startToken = ec.tok; cs = new CmdSeq(); } @@ -973,7 +977,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } } - Expect(26); + Expect(28); IToken/*!*/ endCurly = t; if (startToken == null && bigblocks.Count == 0) { startToken = t; cs = new CmdSeq(); @@ -998,29 +1002,29 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { if (la.kind == 1) { LabelOrAssign(out c, out label); - } else if (la.kind == 44) { + } else if (la.kind == 46) { Get(); x = t; - while (la.kind == 25) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); c = new AssertCmd(x, e, kv); - Expect(7); - } else if (la.kind == 45) { + Expect(8); + } else if (la.kind == 47) { Get(); x = t; - while (la.kind == 25) { + while (la.kind == 27) { Attribute(ref kv); } Proposition(out e); c = new AssumeCmd(x, e, kv); - Expect(7); - } else if (la.kind == 46) { + Expect(8); + } else if (la.kind == 48) { Get(); x = t; Idents(out xs); - Expect(7); + Expect(8); ids = new IdentifierExprSeq(); foreach(IToken/*!*/ y in xs){ Contract.Assert(y != null); @@ -1028,27 +1032,27 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } c = new HavocCmd(x,ids); - } else if (la.kind == 33 || la.kind == 48) { + } else if (la.kind == 35 || la.kind == 50) { CallCmd(out cn); - Expect(7); + Expect(8); c = cn; - } else SynErr(97); + } else SynErr(101); } void StructuredCmd(out StructuredCmd/*!*/ ec) { Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec)); IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd; - if (la.kind == 38) { + if (la.kind == 40) { IfCmd(out ifcmd); ec = ifcmd; - } else if (la.kind == 40) { + } else if (la.kind == 42) { WhileCmd(out wcmd); ec = wcmd; - } else if (la.kind == 43) { + } else if (la.kind == 45) { BreakCmd(out bcmd); ec = bcmd; - } else SynErr(98); + } else SynErr(102); } void TransferCmd(out TransferCmd/*!*/ tc) { @@ -1056,7 +1060,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { Token y; TokenSeq/*!*/ xs; StringSeq ss = new StringSeq(); - if (la.kind == 36) { + if (la.kind == 38) { Get(); y = t; Idents(out xs); @@ -1065,11 +1069,11 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { ss.Add(s.val); } tc = new GotoCmd(y, ss); - } else if (la.kind == 37) { + } else if (la.kind == 39) { Get(); tc = new ReturnCmd(t); - } else SynErr(99); - Expect(7); + } else SynErr(103); + Expect(8); } void IfCmd(out IfCmd/*!*/ ifcmd) { @@ -1079,21 +1083,21 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { IfCmd/*!*/ elseIf; IfCmd elseIfOption = null; StmtList/*!*/ els; StmtList elseOption = null; - Expect(38); + Expect(40); x = t; Guard(out guard); - Expect(25); + Expect(27); StmtList(out thn); - if (la.kind == 39) { + if (la.kind == 41) { Get(); - if (la.kind == 38) { + if (la.kind == 40) { IfCmd(out elseIf); elseIfOption = elseIf; - } else if (la.kind == 25) { + } else if (la.kind == 27) { Get(); StmtList(out els); elseOption = els; - } else SynErr(100); + } else SynErr(104); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); } @@ -1105,18 +1109,18 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { StmtList/*!*/ body; QKeyValue kv = null; - Expect(40); + Expect(42); x = t; Guard(out guard); Contract.Assume(guard == null || cce.Owner.None(guard)); - while (la.kind == 33 || la.kind == 41) { + while (la.kind == 35 || la.kind == 43) { isFree = false; z = la/*lookahead token*/; - if (la.kind == 33) { + if (la.kind == 35) { Get(); isFree = true; } - Expect(41); - while (la.kind == 25) { + Expect(43); + while (la.kind == 27) { Attribute(ref kv); } Expression(out e); @@ -1126,9 +1130,9 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { invariants.Add(new AssertCmd(z, e, kv)); } - Expect(7); + Expect(8); } - Expect(25); + Expect(27); StmtList(out body); wcmd = new WhileCmd(x, guard, invariants, body); } @@ -1137,27 +1141,27 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y; string breakLabel = null; - Expect(43); + Expect(45); x = t; if (la.kind == 1) { Ident(out y); breakLabel = y.val; } - Expect(7); + Expect(8); bcmd = new BreakCmd(x, breakLabel); } void Guard(out Expr e) { Expr/*!*/ ee; e = null; - Expect(8); - if (la.kind == 42) { + Expect(9); + if (la.kind == 44) { Get(); e = null; - } else if (StartOf(7)) { + } else if (StartOf(8)) { Expression(out ee); e = ee; - } else SynErr(101); - Expect(9); + } else SynErr(105); + Expect(10); } void LabelOrAssign(out Cmd c, out IToken label) { @@ -1170,40 +1174,40 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { Ident(out id); x = t; - if (la.kind == 10) { + if (la.kind == 11) { Get(); c = null; label = x; - } else if (la.kind == 11 || la.kind == 15 || la.kind == 47) { + } else if (la.kind == 12 || la.kind == 17 || la.kind == 49) { lhss = new List(); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 15) { + while (la.kind == 17) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); } lhss.Add(lhs); - while (la.kind == 11) { + while (la.kind == 12) { Get(); Ident(out id); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 15) { + while (la.kind == 17) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); } lhss.Add(lhs); } - Expect(47); + Expect(49); x = t; /* use location of := */ Expression(out e0); rhss = new List (); rhss.Add(e0); - while (la.kind == 11) { + while (la.kind == 12) { Get(); Expression(out e0); rhss.Add(e0); } - Expect(7); + Expect(8); c = new AssignCmd(x, lhss, rhss); - } else SynErr(102); + } else SynErr(106); } void CallCmd(out Cmd/*!*/ c) { @@ -1215,33 +1219,33 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { c = dummyCmd; bool isFree = false; - if (la.kind == 33) { + if (la.kind == 35) { Get(); isFree = true; } - Expect(48); + Expect(50); x = t; - while (la.kind == 25) { + while (la.kind == 27) { Attribute(ref kv); } if (la.kind == 1) { Ident(out first); - if (la.kind == 8) { + if (la.kind == 9) { Get(); - if (StartOf(8)) { + if (StartOf(9)) { CallForallArg(out en); es.Add(en); - while (la.kind == 11) { + while (la.kind == 12) { Get(); CallForallArg(out en); es.Add(en); } } - Expect(9); + Expect(10); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; - } else if (la.kind == 11 || la.kind == 47) { + } else if (la.kind == 12 || la.kind == 49) { ids.Add(new IdentifierExpr(first, first.val)); - if (la.kind == 11) { + if (la.kind == 12) { Get(); CallOutIdent(out p); if (p==null) { @@ -1250,7 +1254,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { ids.Add(new IdentifierExpr(p, p.val)); } - while (la.kind == 11) { + while (la.kind == 12) { Get(); CallOutIdent(out p); if (p==null) { @@ -1261,41 +1265,41 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } } - Expect(47); + Expect(49); Ident(out first); - Expect(8); - if (StartOf(8)) { + Expect(9); + if (StartOf(9)) { CallForallArg(out en); es.Add(en); - while (la.kind == 11) { + while (la.kind == 12) { Get(); CallForallArg(out en); es.Add(en); } } - Expect(9); + Expect(10); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; - } else SynErr(103); - } else if (la.kind == 49) { + } else SynErr(107); + } else if (la.kind == 51) { Get(); Ident(out first); - Expect(8); + Expect(9); args = new List(); - if (StartOf(8)) { + if (StartOf(9)) { CallForallArg(out en); args.Add(en); - while (la.kind == 11) { + while (la.kind == 12) { Get(); CallForallArg(out en); args.Add(en); } } - Expect(9); + Expect(10); c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree; - } else if (la.kind == 42) { + } else if (la.kind == 44) { Get(); ids.Add(null); - if (la.kind == 11) { + if (la.kind == 12) { Get(); CallOutIdent(out p); if (p==null) { @@ -1304,7 +1308,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { ids.Add(new IdentifierExpr(p, p.val)); } - while (la.kind == 11) { + while (la.kind == 12) { Get(); CallOutIdent(out p); if (p==null) { @@ -1315,70 +1319,70 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } } - Expect(47); + Expect(49); Ident(out first); - Expect(8); - if (StartOf(8)) { + Expect(9); + if (StartOf(9)) { CallForallArg(out en); es.Add(en); - while (la.kind == 11) { + while (la.kind == 12) { Get(); CallForallArg(out en); es.Add(en); } } - Expect(9); + Expect(10); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; - } else SynErr(104); + } else SynErr(108); } void MapAssignIndex(out IToken/*!*/ x, out List/*!*/ indexes) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List (); Expr/*!*/ e; - Expect(15); + Expect(17); x = t; - if (StartOf(7)) { + if (StartOf(8)) { Expression(out e); indexes.Add(e); - while (la.kind == 11) { + while (la.kind == 12) { Get(); Expression(out e); indexes.Add(e); } } - Expect(16); + Expect(18); } void CallForallArg(out Expr exprOptional) { exprOptional = null; Expr/*!*/ e; - if (la.kind == 42) { + if (la.kind == 44) { Get(); - } else if (StartOf(7)) { + } else if (StartOf(8)) { Expression(out e); exprOptional = e; - } else SynErr(105); + } else SynErr(109); } void CallOutIdent(out IToken id) { id = null; IToken/*!*/ p; - if (la.kind == 42) { + if (la.kind == 44) { Get(); } else if (la.kind == 1) { Ident(out p); id = p; - } else SynErr(106); + } else SynErr(110); } void Expressions(out ExprSeq/*!*/ es) { Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new ExprSeq(); Expression(out e); es.Add(e); - while (la.kind == 11) { + while (la.kind == 12) { Get(); Expression(out e); es.Add(e); @@ -1388,8 +1392,8 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; LogicalExpression(out e0); - if (StartOf(9)) { - if (la.kind == 52 || la.kind == 53) { + if (StartOf(10)) { + if (la.kind == 54 || la.kind == 55) { ImpliesOp(); x = t; ImpliesExpression(true, out e1); @@ -1401,7 +1405,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { x = t; LogicalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); - while (la.kind == 54 || la.kind == 55) { + while (la.kind == 56 || la.kind == 57) { ExpliesOp(); x = t; LogicalExpression(out e1); @@ -1412,23 +1416,23 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } void EquivOp() { - if (la.kind == 50) { + if (la.kind == 52) { Get(); - } else if (la.kind == 51) { + } else if (la.kind == 53) { Get(); - } else SynErr(107); + } else SynErr(111); } void LogicalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; RelationalExpression(out e0); - if (StartOf(10)) { - if (la.kind == 56 || la.kind == 57) { + if (StartOf(11)) { + if (la.kind == 58 || la.kind == 59) { AndOp(); x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); - while (la.kind == 56 || la.kind == 57) { + while (la.kind == 58 || la.kind == 59) { AndOp(); x = t; RelationalExpression(out e1); @@ -1439,7 +1443,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); - while (la.kind == 58 || la.kind == 59) { + while (la.kind == 60 || la.kind == 61) { OrOp(); x = t; RelationalExpression(out e1); @@ -1450,25 +1454,25 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } void ImpliesOp() { - if (la.kind == 52) { + if (la.kind == 54) { Get(); - } else if (la.kind == 53) { + } else if (la.kind == 55) { Get(); - } else SynErr(108); + } else SynErr(112); } void ExpliesOp() { - if (la.kind == 54) { + if (la.kind == 56) { Get(); - } else if (la.kind == 55) { + } else if (la.kind == 57) { Get(); - } else SynErr(109); + } else SynErr(113); } void RelationalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; BvTerm(out e0); - if (StartOf(11)) { + if (StartOf(12)) { RelOp(out x, out op); BvTerm(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -1476,25 +1480,25 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } void AndOp() { - if (la.kind == 56) { + if (la.kind == 58) { Get(); - } else if (la.kind == 57) { + } else if (la.kind == 59) { Get(); - } else SynErr(110); + } else SynErr(114); } void OrOp() { - if (la.kind == 58) { + if (la.kind == 60) { Get(); - } else if (la.kind == 59) { + } else if (la.kind == 61) { Get(); - } else SynErr(111); + } else SynErr(115); } void BvTerm(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; Term(out e0); - while (la.kind == 68) { + while (la.kind == 70) { Get(); x = t; Term(out e1); @@ -1505,64 +1509,64 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; switch (la.kind) { - case 60: { + case 62: { Get(); x = t; op=BinaryOperator.Opcode.Eq; break; } - case 17: { + case 19: { Get(); x = t; op=BinaryOperator.Opcode.Lt; break; } - case 18: { + case 20: { Get(); x = t; op=BinaryOperator.Opcode.Gt; break; } - case 61: { + case 63: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 62: { + case 64: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - case 63: { + case 65: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 64: { + case 66: { Get(); x = t; op=BinaryOperator.Opcode.Subtype; break; } - case 65: { + case 67: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 66: { + case 68: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 67: { + case 69: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - default: SynErr(112); break; + default: SynErr(116); break; } } void Term(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; Factor(out e0); - while (la.kind == 69 || la.kind == 70) { + while (la.kind == 71 || la.kind == 72) { AddOp(out x, out op); Factor(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -1571,64 +1575,78 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { void Factor(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; - UnaryExpression(out e0); - while (la.kind == 42 || la.kind == 71 || la.kind == 72) { + Power(out e0); + while (StartOf(13)) { MulOp(out x, out op); - UnaryExpression(out e1); + Power(out e1); e0 = Expr.Binary(x, op, e0, e1); } } void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 69) { + if (la.kind == 71) { Get(); x = t; op=BinaryOperator.Opcode.Add; - } else if (la.kind == 70) { + } else if (la.kind == 72) { Get(); x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(113); + } else SynErr(117); } - void UnaryExpression(out Expr/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; - e = dummyExpr; - - if (la.kind == 70) { + void Power(out Expr/*!*/ e0) { + Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; + UnaryExpression(out e0); + if (la.kind == 76) { Get(); x = t; - UnaryExpression(out e); - e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); - } else if (la.kind == 73 || la.kind == 74) { - NegOp(); - x = t; - UnaryExpression(out e); - e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); - } else if (StartOf(12)) { - CoercionExpression(out e); - } else SynErr(114); + Power(out e1); + e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1); + } } void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 42) { + if (la.kind == 44) { Get(); x = t; op=BinaryOperator.Opcode.Mul; - } else if (la.kind == 71) { + } else if (la.kind == 73) { Get(); x = t; op=BinaryOperator.Opcode.Div; - } else if (la.kind == 72) { + } else if (la.kind == 74) { Get(); x = t; op=BinaryOperator.Opcode.Mod; - } else SynErr(115); + } else if (la.kind == 75) { + Get(); + x = t; op=BinaryOperator.Opcode.RealDiv; + } else SynErr(118); + } + + void UnaryExpression(out Expr/*!*/ e) { + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; + e = dummyExpr; + + if (la.kind == 72) { + Get(); + x = t; + UnaryExpression(out e); + e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); + } else if (la.kind == 77 || la.kind == 78) { + NegOp(); + x = t; + UnaryExpression(out e); + e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); + } else if (StartOf(14)) { + CoercionExpression(out e); + } else SynErr(119); } void NegOp() { - if (la.kind == 73) { + if (la.kind == 77) { Get(); - } else if (la.kind == 74) { + } else if (la.kind == 78) { Get(); - } else SynErr(116); + } else SynErr(120); } void CoercionExpression(out Expr/*!*/ e) { @@ -1637,7 +1655,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { BigNum bn; ArrayExpression(out e); - while (la.kind == 10) { + while (la.kind == 11) { Get(); x = t; if (StartOf(2)) { @@ -1652,7 +1670,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(117); + } else SynErr(121); } } @@ -1663,20 +1681,20 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { ExprSeq/*!*/ allArgs = dummyExprSeq; AtomExpression(out e); - while (la.kind == 15) { + while (la.kind == 17) { Get(); x = t; allArgs = new ExprSeq (); allArgs.Add(e); store = false; bvExtract = false; - if (StartOf(13)) { - if (StartOf(7)) { + if (StartOf(15)) { + if (StartOf(8)) { Expression(out index0); if (index0 is BvBounds) bvExtract = true; else allArgs.Add(index0); - while (la.kind == 11) { + while (la.kind == 12) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -1684,7 +1702,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { allArgs.Add(e1); } - if (la.kind == 47) { + if (la.kind == 49) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -1698,7 +1716,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { allArgs.Add(e1); store = true; } } - Expect(16); + Expect(18); if (store) e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs); else if (bvExtract) @@ -1723,7 +1741,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } void AtomExpression(out Expr/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; ExprSeq/*!*/ es; VariableSeq/*!*/ ds; Trigger trig; TypeVariableSeq/*!*/ typeParams; IdentifierExpr/*!*/ id; @@ -1733,12 +1751,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { List/*!*/ blocks; switch (la.kind) { - case 75: { + case 79: { Get(); e = new LiteralExpr(t, false); break; } - case 76: { + case 80: { Get(); e = new LiteralExpr(t, true); break; @@ -1748,6 +1766,11 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { e = new LiteralExpr(t, bn); break; } + case 5: case 6: { + Dec(out bd); + e = new LiteralExpr(t, bd); + break; + } case 2: { BvLit(out bn, out n); e = new LiteralExpr(t, bn, n); @@ -1756,47 +1779,65 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { case 1: { Ident(out x); id = new IdentifierExpr(x, x.val); e = id; - if (la.kind == 8) { + if (la.kind == 9) { Get(); - if (StartOf(7)) { + if (StartOf(8)) { Expressions(out es); e = new NAryExpr(x, new FunctionCall(id), es); - } else if (la.kind == 9) { + } else if (la.kind == 10) { e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); - } else SynErr(118); - Expect(9); + } else SynErr(122); + Expect(10); } break; } - case 77: { + case 81: { Get(); x = t; - Expect(8); - Expression(out e); Expect(9); + Expression(out e); + Expect(10); e = new OldExpr(x, e); break; } - case 8: { + case 14: { Get(); - if (StartOf(7)) { + x = t; + Expect(9); + Expression(out e); + Expect(10); + e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new ExprSeq(e)); + break; + } + case 15: { + Get(); + x = t; + Expect(9); + Expression(out e); + Expect(10); + e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new ExprSeq(e)); + break; + } + case 9: { + Get(); + if (StartOf(8)) { Expression(out e); if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + "are not allowed"); - } else if (la.kind == 49 || la.kind == 81) { + } else if (la.kind == 51 || la.kind == 85) { Forall(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Length + ds.Length > 0) e = new ForallExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 82 || la.kind == 83) { + } else if (la.kind == 86 || la.kind == 87) { Exists(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Length + ds.Length > 0) e = new ExistsExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 84 || la.kind == 85) { + } else if (la.kind == 88 || la.kind == 89) { Lambda(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); @@ -1804,21 +1845,39 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { SemErr("triggers not allowed in lambda expressions"); if (typeParams.Length + ds.Length > 0) e = new LambdaExpr(x, typeParams, ds, kv, e); - } else SynErr(119); - Expect(9); + } else SynErr(123); + Expect(10); break; } - case 38: { + case 40: { IfThenElseExpression(out e); break; } - case 78: { + case 82: { CodeExpression(out locals, out blocks); e = new CodeExpr(locals, blocks); break; } - default: SynErr(120); break; + default: SynErr(124); break; + } + } + + void Dec(out BigDec n) { + string s = ""; + if (la.kind == 5) { + Get(); + s = t.val; + } else if (la.kind == 6) { + Get(); + s = t.val; + } else SynErr(125); + try { + n = BigDec.FromString(s); + } catch (FormatException) { + this.SemErr("incorrectly formatted number"); + n = BigDec.ZERO; } + } void BvLit(out BigNum n, out int m) { @@ -1838,11 +1897,11 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } void Forall() { - if (la.kind == 49) { + if (la.kind == 51) { Get(); - } else if (la.kind == 81) { + } else if (la.kind == 85) { Get(); - } else SynErr(121); + } else SynErr(126); } void QuantifierBody(IToken/*!*/ q, out TypeVariableSeq/*!*/ typeParams, out VariableSeq/*!*/ ds, @@ -1853,35 +1912,35 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { kv = null; ds = new VariableSeq (); - if (la.kind == 17) { + if (la.kind == 19) { TypeParams(out tok, out typeParams); if (la.kind == 1) { BoundVars(q, out ds); } } else if (la.kind == 1) { BoundVars(q, out ds); - } else SynErr(122); + } else SynErr(127); QSep(); - while (la.kind == 25) { + while (la.kind == 27) { AttributeOrTrigger(ref kv, ref trig); } Expression(out body); } void Exists() { - if (la.kind == 82) { + if (la.kind == 86) { Get(); - } else if (la.kind == 83) { + } else if (la.kind == 87) { Get(); - } else SynErr(123); + } else SynErr(128); } void Lambda() { - if (la.kind == 84) { + if (la.kind == 88) { Get(); - } else if (la.kind == 85) { + } else if (la.kind == 89) { Get(); - } else SynErr(124); + } else SynErr(129); } void IfThenElseExpression(out Expr/*!*/ e) { @@ -1889,12 +1948,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { IToken/*!*/ tok; Expr/*!*/ e0, e1, e2; e = dummyExpr; - Expect(38); + Expect(40); tok = t; Expression(out e0); - Expect(80); + Expect(84); Expression(out e1); - Expect(39); + Expect(41); Expression(out e2); e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); } @@ -1903,8 +1962,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new VariableSeq(); Block/*!*/ b; blocks = new List(); - Expect(78); - while (la.kind == 6) { + Expect(82); + while (la.kind == 7) { LocalVars(locals); } SpecBlock(out b); @@ -1913,7 +1972,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { SpecBlock(out b); blocks.Add(b); } - Expect(79); + Expect(83); } void SpecBlock(out Block/*!*/ b) { @@ -1926,8 +1985,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Expr/*!*/ e; Ident(out x); - Expect(10); - while (StartOf(6)) { + Expect(11); + while (StartOf(7)) { LabelOrCmd(out c, out label); if (c != null) { Contract.Assert(label == null); @@ -1938,7 +1997,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } } - if (la.kind == 36) { + if (la.kind == 38) { Get(); y = t; Idents(out xs); @@ -1947,12 +2006,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { ss.Add(s.val); } b = new Block(x,x.val,cs,new GotoCmd(y,ss)); - } else if (la.kind == 37) { + } else if (la.kind == 39) { Get(); Expression(out e); b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); - } else SynErr(125); - Expect(7); + } else SynErr(130); + Expect(8); } void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { @@ -1960,16 +2019,16 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { string key; List parameters; object/*!*/ param; - Expect(25); + Expect(27); tok = t; - if (la.kind == 10) { + if (la.kind == 11) { Get(); Expect(1); key = t.val; parameters = new List(); - if (StartOf(14)) { + if (StartOf(16)) { AttributeParameter(out param); parameters.Add(param); - while (la.kind == 11) { + while (la.kind == 12) { Get(); AttributeParameter(out param); parameters.Add(param); @@ -1994,10 +2053,10 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } } - } else if (StartOf(7)) { + } else if (StartOf(8)) { Expression(out e); es = new ExprSeq(e); - while (la.kind == 11) { + while (la.kind == 12) { Get(); Expression(out e); es.Add(e); @@ -2008,8 +2067,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else SynErr(126); - Expect(26); + } else SynErr(131); + Expect(28); } void AttributeParameter(out object/*!*/ o) { @@ -2020,18 +2079,18 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { if (la.kind == 4) { Get(); o = t.val.Substring(1, t.val.Length-2); - } else if (StartOf(7)) { + } else if (StartOf(8)) { Expression(out e); o = e; - } else SynErr(127); + } else SynErr(132); } void QSep() { - if (la.kind == 86) { + if (la.kind == 90) { Get(); - } else if (la.kind == 87) { + } else if (la.kind == 91) { Get(); - } else SynErr(128); + } else SynErr(133); } @@ -2047,21 +2106,23 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } static readonly bool[,]/*!*/ set = { - {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, T,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x} + {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x} }; } // end Parser @@ -2091,130 +2152,135 @@ public class Errors { case 2: s = "bvlit expected"; break; case 3: s = "digits expected"; break; case 4: s = "string expected"; break; - case 5: s = "float expected"; break; - case 6: s = "\"var\" expected"; break; - case 7: s = "\";\" expected"; break; - case 8: s = "\"(\" expected"; break; - case 9: s = "\")\" expected"; break; - case 10: s = "\":\" expected"; break; - case 11: s = "\",\" expected"; break; - case 12: s = "\"where\" expected"; break; - case 13: s = "\"int\" expected"; break; - case 14: s = "\"bool\" expected"; break; - case 15: s = "\"[\" expected"; break; - case 16: s = "\"]\" expected"; break; - case 17: s = "\"<\" expected"; break; - case 18: s = "\">\" expected"; break; - case 19: s = "\"const\" expected"; break; - case 20: s = "\"unique\" expected"; break; - case 21: s = "\"extends\" expected"; break; - case 22: s = "\"complete\" expected"; break; - case 23: s = "\"function\" expected"; break; - case 24: s = "\"returns\" expected"; break; - case 25: s = "\"{\" expected"; break; - case 26: s = "\"}\" expected"; break; - case 27: s = "\"axiom\" expected"; break; - case 28: s = "\"type\" expected"; break; - case 29: s = "\"=\" expected"; break; - case 30: s = "\"procedure\" expected"; break; - case 31: s = "\"implementation\" expected"; break; - case 32: s = "\"modifies\" expected"; break; - case 33: s = "\"free\" expected"; break; - case 34: s = "\"requires\" expected"; break; - case 35: s = "\"ensures\" expected"; break; - case 36: s = "\"goto\" expected"; break; - case 37: s = "\"return\" expected"; break; - case 38: s = "\"if\" expected"; break; - case 39: s = "\"else\" expected"; break; - case 40: s = "\"while\" expected"; break; - case 41: s = "\"invariant\" expected"; break; - case 42: s = "\"*\" expected"; break; - case 43: s = "\"break\" expected"; break; - case 44: s = "\"assert\" expected"; break; - case 45: s = "\"assume\" expected"; break; - case 46: s = "\"havoc\" expected"; break; - case 47: s = "\":=\" expected"; break; - case 48: s = "\"call\" expected"; break; - case 49: s = "\"forall\" expected"; break; - case 50: s = "\"<==>\" expected"; break; - case 51: s = "\"\\u21d4\" expected"; break; - case 52: s = "\"==>\" expected"; break; - case 53: s = "\"\\u21d2\" expected"; break; - case 54: s = "\"<==\" expected"; break; - case 55: s = "\"\\u21d0\" expected"; break; - case 56: s = "\"&&\" expected"; break; - case 57: s = "\"\\u2227\" expected"; break; - case 58: s = "\"||\" expected"; break; - case 59: s = "\"\\u2228\" expected"; break; - case 60: s = "\"==\" expected"; break; - case 61: s = "\"<=\" expected"; break; - case 62: s = "\">=\" expected"; break; - case 63: s = "\"!=\" expected"; break; - case 64: s = "\"<:\" expected"; break; - case 65: s = "\"\\u2260\" expected"; break; - case 66: s = "\"\\u2264\" expected"; break; - case 67: s = "\"\\u2265\" expected"; break; - case 68: s = "\"++\" expected"; break; - case 69: s = "\"+\" expected"; break; - case 70: s = "\"-\" expected"; break; - case 71: s = "\"div\" expected"; break; - case 72: s = "\"mod\" expected"; break; - case 73: s = "\"!\" expected"; break; - case 74: s = "\"\\u00ac\" expected"; break; - case 75: s = "\"false\" expected"; break; - case 76: s = "\"true\" expected"; break; - case 77: s = "\"old\" expected"; break; - case 78: s = "\"|{\" expected"; break; - case 79: s = "\"}|\" expected"; break; - case 80: s = "\"then\" expected"; break; - case 81: s = "\"\\u2200\" expected"; break; - case 82: s = "\"exists\" expected"; break; - case 83: s = "\"\\u2203\" expected"; break; - case 84: s = "\"lambda\" expected"; break; - case 85: s = "\"\\u03bb\" expected"; break; - case 86: s = "\"::\" expected"; break; - case 87: s = "\"\\u2022\" expected"; break; - case 88: s = "??? expected"; break; - case 89: s = "invalid Function"; break; - case 90: s = "invalid Function"; break; - case 91: s = "invalid Procedure"; break; - case 92: s = "invalid Type"; break; - case 93: s = "invalid TypeAtom"; break; - case 94: s = "invalid TypeArgs"; break; - case 95: s = "invalid Spec"; break; - case 96: s = "invalid SpecPrePost"; break; - case 97: s = "invalid LabelOrCmd"; break; - case 98: s = "invalid StructuredCmd"; break; - case 99: s = "invalid TransferCmd"; break; - case 100: s = "invalid IfCmd"; break; - case 101: s = "invalid Guard"; break; - case 102: s = "invalid LabelOrAssign"; break; - case 103: s = "invalid CallCmd"; break; - case 104: s = "invalid CallCmd"; break; - case 105: s = "invalid CallForallArg"; break; - case 106: s = "invalid CallOutIdent"; break; - case 107: s = "invalid EquivOp"; break; - case 108: s = "invalid ImpliesOp"; break; - case 109: s = "invalid ExpliesOp"; break; - case 110: s = "invalid AndOp"; break; - case 111: s = "invalid OrOp"; break; - case 112: s = "invalid RelOp"; break; - case 113: s = "invalid AddOp"; break; - case 114: s = "invalid UnaryExpression"; break; - case 115: s = "invalid MulOp"; break; - case 116: s = "invalid NegOp"; break; - case 117: s = "invalid CoercionExpression"; break; - case 118: s = "invalid AtomExpression"; break; - case 119: s = "invalid AtomExpression"; break; - case 120: s = "invalid AtomExpression"; break; - case 121: s = "invalid Forall"; break; - case 122: s = "invalid QuantifierBody"; break; - case 123: s = "invalid Exists"; break; - case 124: s = "invalid Lambda"; break; - case 125: s = "invalid SpecBlock"; break; - case 126: s = "invalid AttributeOrTrigger"; break; - case 127: s = "invalid AttributeParameter"; break; - case 128: s = "invalid QSep"; break; + case 5: s = "decimal expected"; break; + case 6: s = "float expected"; break; + case 7: s = "\"var\" expected"; break; + case 8: s = "\";\" expected"; break; + case 9: s = "\"(\" expected"; break; + case 10: s = "\")\" expected"; break; + case 11: s = "\":\" expected"; break; + case 12: s = "\",\" expected"; break; + case 13: s = "\"where\" expected"; break; + case 14: s = "\"int\" expected"; break; + case 15: s = "\"real\" expected"; break; + case 16: s = "\"bool\" expected"; break; + case 17: s = "\"[\" expected"; break; + case 18: s = "\"]\" expected"; break; + case 19: s = "\"<\" expected"; break; + case 20: s = "\">\" expected"; break; + case 21: s = "\"const\" expected"; break; + case 22: s = "\"unique\" expected"; break; + case 23: s = "\"extends\" expected"; break; + case 24: s = "\"complete\" expected"; break; + case 25: s = "\"function\" expected"; break; + case 26: s = "\"returns\" expected"; break; + case 27: s = "\"{\" expected"; break; + case 28: s = "\"}\" expected"; break; + case 29: s = "\"axiom\" expected"; break; + case 30: s = "\"type\" expected"; break; + case 31: s = "\"=\" expected"; break; + case 32: s = "\"procedure\" expected"; break; + case 33: s = "\"implementation\" expected"; break; + case 34: s = "\"modifies\" expected"; break; + case 35: s = "\"free\" expected"; break; + case 36: s = "\"requires\" expected"; break; + case 37: s = "\"ensures\" expected"; break; + case 38: s = "\"goto\" expected"; break; + case 39: s = "\"return\" expected"; break; + case 40: s = "\"if\" expected"; break; + case 41: s = "\"else\" expected"; break; + case 42: s = "\"while\" expected"; break; + case 43: s = "\"invariant\" expected"; break; + case 44: s = "\"*\" expected"; break; + case 45: s = "\"break\" expected"; break; + case 46: s = "\"assert\" expected"; break; + case 47: s = "\"assume\" expected"; break; + case 48: s = "\"havoc\" expected"; break; + case 49: s = "\":=\" expected"; break; + case 50: s = "\"call\" expected"; break; + case 51: s = "\"forall\" expected"; break; + case 52: s = "\"<==>\" expected"; break; + case 53: s = "\"\\u21d4\" expected"; break; + case 54: s = "\"==>\" expected"; break; + case 55: s = "\"\\u21d2\" expected"; break; + case 56: s = "\"<==\" expected"; break; + case 57: s = "\"\\u21d0\" expected"; break; + case 58: s = "\"&&\" expected"; break; + case 59: s = "\"\\u2227\" expected"; break; + case 60: s = "\"||\" expected"; break; + case 61: s = "\"\\u2228\" expected"; break; + case 62: s = "\"==\" expected"; break; + case 63: s = "\"<=\" expected"; break; + case 64: s = "\">=\" expected"; break; + case 65: s = "\"!=\" expected"; break; + case 66: s = "\"<:\" expected"; break; + case 67: s = "\"\\u2260\" expected"; break; + case 68: s = "\"\\u2264\" expected"; break; + case 69: s = "\"\\u2265\" expected"; break; + case 70: s = "\"++\" expected"; break; + case 71: s = "\"+\" expected"; break; + case 72: s = "\"-\" expected"; break; + case 73: s = "\"div\" expected"; break; + case 74: s = "\"mod\" expected"; break; + case 75: s = "\"/\" expected"; break; + case 76: s = "\"**\" expected"; break; + case 77: s = "\"!\" expected"; break; + case 78: s = "\"\\u00ac\" expected"; break; + case 79: s = "\"false\" expected"; break; + case 80: s = "\"true\" expected"; break; + case 81: s = "\"old\" expected"; break; + case 82: s = "\"|{\" expected"; break; + case 83: s = "\"}|\" expected"; break; + case 84: s = "\"then\" expected"; break; + case 85: s = "\"\\u2200\" expected"; break; + case 86: s = "\"exists\" expected"; break; + case 87: s = "\"\\u2203\" expected"; break; + case 88: s = "\"lambda\" expected"; break; + case 89: s = "\"\\u03bb\" expected"; break; + case 90: s = "\"::\" expected"; break; + case 91: s = "\"\\u2022\" expected"; break; + case 92: s = "??? expected"; break; + case 93: s = "invalid Function"; break; + case 94: s = "invalid Function"; break; + case 95: s = "invalid Procedure"; break; + case 96: s = "invalid Type"; break; + case 97: s = "invalid TypeAtom"; break; + case 98: s = "invalid TypeArgs"; break; + case 99: s = "invalid Spec"; break; + case 100: s = "invalid SpecPrePost"; break; + case 101: s = "invalid LabelOrCmd"; break; + case 102: s = "invalid StructuredCmd"; break; + case 103: s = "invalid TransferCmd"; break; + case 104: s = "invalid IfCmd"; break; + case 105: s = "invalid Guard"; break; + case 106: s = "invalid LabelOrAssign"; break; + case 107: s = "invalid CallCmd"; break; + case 108: s = "invalid CallCmd"; break; + case 109: s = "invalid CallForallArg"; break; + case 110: s = "invalid CallOutIdent"; break; + case 111: s = "invalid EquivOp"; break; + case 112: s = "invalid ImpliesOp"; break; + case 113: s = "invalid ExpliesOp"; break; + case 114: s = "invalid AndOp"; break; + case 115: s = "invalid OrOp"; break; + case 116: s = "invalid RelOp"; break; + case 117: s = "invalid AddOp"; break; + case 118: s = "invalid MulOp"; break; + case 119: s = "invalid UnaryExpression"; break; + case 120: s = "invalid NegOp"; break; + case 121: s = "invalid CoercionExpression"; break; + case 122: s = "invalid AtomExpression"; break; + case 123: s = "invalid AtomExpression"; break; + case 124: s = "invalid AtomExpression"; break; + case 125: s = "invalid Dec"; break; + case 126: s = "invalid Forall"; break; + case 127: s = "invalid QuantifierBody"; break; + case 128: s = "invalid Exists"; break; + case 129: s = "invalid Lambda"; break; + case 130: s = "invalid SpecBlock"; break; + case 131: s = "invalid AttributeOrTrigger"; break; + case 132: s = "invalid AttributeParameter"; break; + case 133: s = "invalid QSep"; break; default: s = "error " + n; break; } diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index b9f4ec42..60c15b41 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner { const char EOL = '\n'; const int eofSym = 0; /* pdt */ - const int maxT = 88; - const int noSym = 88; + const int maxT = 92; + const int noSym = 92; [ContractInvariantMethod] @@ -256,40 +256,41 @@ public class Scanner { for (int i = 65; i <= 90; ++i) start[i] = 2; for (int i = 94; i <= 122; ++i) start[i] = 2; for (int i = 126; i <= 126; ++i) start[i] = 2; - for (int i = 48; i <= 57; ++i) start[i] = 9; + for (int i = 48; i <= 57; ++i) start[i] = 16; for (int i = 34; i <= 34; ++i) start[i] = 6; start[92] = 1; - start[59] = 12; - start[40] = 13; - start[41] = 14; - start[58] = 47; - start[44] = 15; - start[91] = 16; - start[93] = 17; - start[60] = 48; - start[62] = 49; - start[123] = 18; - start[125] = 50; - start[61] = 51; - start[42] = 19; - start[8660] = 22; - start[8658] = 24; - start[8656] = 25; - start[38] = 26; - start[8743] = 28; - start[124] = 52; - start[8744] = 30; - start[33] = 53; - start[8800] = 34; - start[8804] = 35; - start[8805] = 36; - start[43] = 54; - start[45] = 38; - start[172] = 39; - start[8704] = 42; - start[8707] = 43; - start[955] = 44; - start[8226] = 46; + start[59] = 19; + start[40] = 20; + start[41] = 21; + start[58] = 55; + start[44] = 22; + start[91] = 23; + start[93] = 24; + start[60] = 56; + start[62] = 57; + start[123] = 25; + start[125] = 58; + start[61] = 59; + start[42] = 60; + start[8660] = 28; + start[8658] = 30; + start[8656] = 31; + start[38] = 32; + start[8743] = 34; + start[124] = 61; + start[8744] = 36; + start[33] = 62; + start[8800] = 40; + start[8804] = 41; + start[8805] = 42; + start[43] = 63; + start[45] = 44; + start[47] = 45; + start[172] = 47; + start[8704] = 50; + start[8707] = 51; + start[955] = 52; + start[8226] = 54; start[Buffer.EOF] = -1; } @@ -487,44 +488,45 @@ public class Scanner { void CheckLiteral() { switch (t.val) { - case "var": t.kind = 6; break; - case "where": t.kind = 12; break; - case "int": t.kind = 13; break; - case "bool": t.kind = 14; break; - case "const": t.kind = 19; break; - case "unique": t.kind = 20; break; - case "extends": t.kind = 21; break; - case "complete": t.kind = 22; break; - case "function": t.kind = 23; break; - case "returns": t.kind = 24; break; - case "axiom": t.kind = 27; break; - case "type": t.kind = 28; break; - case "procedure": t.kind = 30; break; - case "implementation": t.kind = 31; break; - case "modifies": t.kind = 32; break; - case "free": t.kind = 33; break; - case "requires": t.kind = 34; break; - case "ensures": t.kind = 35; break; - case "goto": t.kind = 36; break; - case "return": t.kind = 37; break; - case "if": t.kind = 38; break; - case "else": t.kind = 39; break; - case "while": t.kind = 40; break; - case "invariant": t.kind = 41; break; - case "break": t.kind = 43; break; - case "assert": t.kind = 44; break; - case "assume": t.kind = 45; break; - case "havoc": t.kind = 46; break; - case "call": t.kind = 48; break; - case "forall": t.kind = 49; break; - case "div": t.kind = 71; break; - case "mod": t.kind = 72; break; - case "false": t.kind = 75; break; - case "true": t.kind = 76; break; - case "old": t.kind = 77; break; - case "then": t.kind = 80; break; - case "exists": t.kind = 82; break; - case "lambda": t.kind = 84; break; + case "var": t.kind = 7; break; + case "where": t.kind = 13; break; + case "int": t.kind = 14; break; + case "real": t.kind = 15; break; + case "bool": t.kind = 16; break; + case "const": t.kind = 21; break; + case "unique": t.kind = 22; break; + case "extends": t.kind = 23; break; + case "complete": t.kind = 24; break; + case "function": t.kind = 25; break; + case "returns": t.kind = 26; break; + case "axiom": t.kind = 29; break; + case "type": t.kind = 30; break; + case "procedure": t.kind = 32; break; + case "implementation": t.kind = 33; break; + case "modifies": t.kind = 34; break; + case "free": t.kind = 35; break; + case "requires": t.kind = 36; break; + case "ensures": t.kind = 37; break; + case "goto": t.kind = 38; break; + case "return": t.kind = 39; break; + case "if": t.kind = 40; break; + case "else": t.kind = 41; break; + case "while": t.kind = 42; break; + case "invariant": t.kind = 43; break; + case "break": t.kind = 45; break; + case "assert": t.kind = 46; break; + case "assume": t.kind = 47; break; + case "havoc": t.kind = 48; break; + case "call": t.kind = 50; break; + case "forall": t.kind = 51; break; + case "div": t.kind = 73; break; + case "mod": t.kind = 74; break; + case "false": t.kind = 79; break; + case "true": t.kind = 80; break; + case "old": t.kind = 81; break; + case "then": t.kind = 84; break; + case "exists": t.kind = 86; break; + case "lambda": t.kind = 88; break; default: break; } } @@ -577,148 +579,181 @@ public class Scanner { case 6: if (ch == '"') {AddCh(); goto case 7;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 10;} + else if (ch == 92) {AddCh(); goto case 17;} else {goto case 0;} case 7: {t.kind = 4; break;} case 8: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} + else if (ch == '-') {AddCh(); goto case 9;} + else {goto case 0;} + case 9: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} + else {goto case 0;} + case 10: recEnd = pos; recKind = 5; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 8;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} else {t.kind = 5; break;} - case 9: + case 11: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} + else {goto case 0;} + case 12: + recEnd = pos; recKind = 6; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} + else if (ch == 'e') {AddCh(); goto case 13;} + else {t.kind = 6; break;} + case 13: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} + else if (ch == '-') {AddCh(); goto case 14;} + else {goto case 0;} + case 14: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} + else {goto case 0;} + case 15: + recEnd = pos; recKind = 6; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} + else {t.kind = 6; break;} + case 16: recEnd = pos; recKind = 3; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;} else if (ch == 'b') {AddCh(); goto case 3;} - else if (ch == '.') {AddCh(); goto case 8;} + else if (ch == 'e') {AddCh(); goto case 8;} + else if (ch == '.') {AddCh(); goto case 11;} else {t.kind = 3; break;} - case 10: - if (ch == '"') {AddCh(); goto case 11;} + case 17: + if (ch == '"') {AddCh(); goto case 18;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 10;} + else if (ch == 92) {AddCh(); goto case 17;} else {goto case 0;} - case 11: + case 18: recEnd = pos; recKind = 4; if (ch == '"') {AddCh(); goto case 7;} else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;} - else if (ch == 92) {AddCh(); goto case 10;} + else if (ch == 92) {AddCh(); goto case 17;} else {t.kind = 4; break;} - case 12: - {t.kind = 7; break;} - case 13: - {t.kind = 8; break;} - case 14: - {t.kind = 9; break;} - case 15: - {t.kind = 11; break;} - case 16: - {t.kind = 15; break;} - case 17: - {t.kind = 16; break;} - case 18: - {t.kind = 25; break;} case 19: - {t.kind = 42; break;} + {t.kind = 8; break;} case 20: - {t.kind = 47; break;} + {t.kind = 9; break;} case 21: - {t.kind = 50; break;} + {t.kind = 10; break;} case 22: - {t.kind = 51; break;} + {t.kind = 12; break;} case 23: - {t.kind = 52; break;} + {t.kind = 17; break;} case 24: - {t.kind = 53; break;} + {t.kind = 18; break;} case 25: - {t.kind = 55; break;} + {t.kind = 27; break;} case 26: - if (ch == '&') {AddCh(); goto case 27;} - else {goto case 0;} + {t.kind = 49; break;} case 27: - {t.kind = 56; break;} + {t.kind = 52; break;} case 28: - {t.kind = 57; break;} + {t.kind = 53; break;} case 29: - {t.kind = 58; break;} + {t.kind = 54; break;} case 30: - {t.kind = 59; break;} + {t.kind = 55; break;} case 31: - {t.kind = 62; break;} + {t.kind = 57; break;} case 32: - {t.kind = 63; break;} + if (ch == '&') {AddCh(); goto case 33;} + else {goto case 0;} case 33: - {t.kind = 64; break;} + {t.kind = 58; break;} case 34: - {t.kind = 65; break;} + {t.kind = 59; break;} case 35: - {t.kind = 66; break;} + {t.kind = 60; break;} case 36: - {t.kind = 67; break;} + {t.kind = 61; break;} case 37: - {t.kind = 68; break;} + {t.kind = 64; break;} case 38: - {t.kind = 70; break;} + {t.kind = 65; break;} case 39: - {t.kind = 74; break;} + {t.kind = 66; break;} case 40: - {t.kind = 78; break;} + {t.kind = 67; break;} case 41: - {t.kind = 79; break;} + {t.kind = 68; break;} case 42: - {t.kind = 81; break;} + {t.kind = 69; break;} case 43: - {t.kind = 83; break;} + {t.kind = 70; break;} case 44: - {t.kind = 85; break;} + {t.kind = 72; break;} case 45: - {t.kind = 86; break;} + {t.kind = 75; break;} case 46: - {t.kind = 87; break;} + {t.kind = 76; break;} case 47: - recEnd = pos; recKind = 10; - if (ch == '=') {AddCh(); goto case 20;} - else if (ch == ':') {AddCh(); goto case 45;} - else {t.kind = 10; break;} + {t.kind = 78; break;} case 48: - recEnd = pos; recKind = 17; - if (ch == '=') {AddCh(); goto case 55;} - else if (ch == ':') {AddCh(); goto case 33;} - else {t.kind = 17; break;} + {t.kind = 82; break;} case 49: - recEnd = pos; recKind = 18; - if (ch == '=') {AddCh(); goto case 31;} - else {t.kind = 18; break;} + {t.kind = 83; break;} case 50: - recEnd = pos; recKind = 26; - if (ch == '|') {AddCh(); goto case 41;} - else {t.kind = 26; break;} + {t.kind = 85; break;} case 51: - recEnd = pos; recKind = 29; - if (ch == '=') {AddCh(); goto case 56;} - else {t.kind = 29; break;} + {t.kind = 87; break;} case 52: - if (ch == '|') {AddCh(); goto case 29;} - else if (ch == '{') {AddCh(); goto case 40;} - else {goto case 0;} + {t.kind = 89; break;} case 53: - recEnd = pos; recKind = 73; - if (ch == '=') {AddCh(); goto case 32;} - else {t.kind = 73; break;} + {t.kind = 90; break;} case 54: - recEnd = pos; recKind = 69; - if (ch == '+') {AddCh(); goto case 37;} - else {t.kind = 69; break;} + {t.kind = 91; break;} case 55: - recEnd = pos; recKind = 61; - if (ch == '=') {AddCh(); goto case 57;} - else {t.kind = 61; break;} + recEnd = pos; recKind = 11; + if (ch == '=') {AddCh(); goto case 26;} + else if (ch == ':') {AddCh(); goto case 53;} + else {t.kind = 11; break;} case 56: - recEnd = pos; recKind = 60; - if (ch == '>') {AddCh(); goto case 23;} - else {t.kind = 60; break;} + recEnd = pos; recKind = 19; + if (ch == '=') {AddCh(); goto case 64;} + else if (ch == ':') {AddCh(); goto case 39;} + else {t.kind = 19; break;} case 57: - recEnd = pos; recKind = 54; - if (ch == '>') {AddCh(); goto case 21;} - else {t.kind = 54; break;} + recEnd = pos; recKind = 20; + if (ch == '=') {AddCh(); goto case 37;} + else {t.kind = 20; break;} + case 58: + recEnd = pos; recKind = 28; + if (ch == '|') {AddCh(); goto case 49;} + else {t.kind = 28; break;} + case 59: + recEnd = pos; recKind = 31; + if (ch == '=') {AddCh(); goto case 65;} + else {t.kind = 31; break;} + case 60: + recEnd = pos; recKind = 44; + if (ch == '*') {AddCh(); goto case 46;} + else {t.kind = 44; break;} + case 61: + if (ch == '|') {AddCh(); goto case 35;} + else if (ch == '{') {AddCh(); goto case 48;} + else {goto case 0;} + case 62: + recEnd = pos; recKind = 77; + if (ch == '=') {AddCh(); goto case 38;} + else {t.kind = 77; break;} + case 63: + recEnd = pos; recKind = 71; + if (ch == '+') {AddCh(); goto case 43;} + else {t.kind = 71; break;} + case 64: + recEnd = pos; recKind = 63; + if (ch == '=') {AddCh(); goto case 66;} + else {t.kind = 63; break;} + case 65: + recEnd = pos; recKind = 62; + if (ch == '>') {AddCh(); goto case 29;} + else {t.kind = 62; break;} + case 66: + recEnd = pos; recKind = 56; + if (ch == '>') {AddCh(); goto case 27;} + else {t.kind = 56; break;} } t.val = new String(tval, 0, tlen); diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index f8b8b82b..9a7fec0c 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -486,6 +486,12 @@ namespace Microsoft.Boogie { case Microsoft.Boogie.BinaryOperator.Opcode.Or: op = " || "; break; + case Microsoft.Boogie.BinaryOperator.Opcode.Pow: + op = " ** "; + break; + case Microsoft.Boogie.BinaryOperator.Opcode.RealDiv: + op = " / "; + break; case Microsoft.Boogie.BinaryOperator.Opcode.Sub: op = " - "; break; diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 6a2cbb6a..cf125c76 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -115,7 +115,7 @@ namespace Microsoft.Boogie.SMTLib } sb.Append(']'); TypeToStringHelper(m.Result, sb); - } else if (t.IsBool || t.IsInt || t.IsBv) { + } else if (t.IsBool || t.IsInt || t.IsReal || t.IsBv) { sb.Append(TypeToString(t)); } else { System.IO.StringWriter buffer = new System.IO.StringWriter(); @@ -137,6 +137,8 @@ namespace Microsoft.Boogie.SMTLib return "Bool"; else if (t.IsInt) return "Int"; + else if (t.IsReal) + return "Real"; else if (t.IsBv) { return "(_ BitVec " + t.BvBits + ")"; } else { @@ -181,7 +183,16 @@ namespace Microsoft.Boogie.SMTLib wr.Write("(- 0 {0})", lit.Abs); else wr.Write(lit); - } else { + } + else if (node is VCExprRealLit) { + BigDec lit = ((VCExprRealLit)node).Val; + if (lit.IsNegative) + // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols") + wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString(20)); + else + wr.Write(lit.ToDecimalString(20)); + } + else { Contract.Assert(false); throw new cce.UnreachableException(); } @@ -609,13 +620,23 @@ namespace Microsoft.Boogie.SMTLib public bool VisitDivOp(VCExprNAry node, LineariserOptions options) { - WriteApplication("int_div", node, options); + WriteApplication("div", node, options); return true; } public bool VisitModOp(VCExprNAry node, LineariserOptions options) { - WriteApplication("int_mod", node, options); + WriteApplication("mod", node, options); + return true; + } + + public bool VisitRealDivOp(VCExprNAry node, LineariserOptions options) { + WriteApplication("/", node, options); + return true; + } + + public bool VisitPowOp(VCExprNAry node, LineariserOptions options) { + WriteApplication("real_pow", node, options); return true; } @@ -655,6 +676,16 @@ namespace Microsoft.Boogie.SMTLib return true; } + public bool VisitToIntOp(VCExprNAry node, LineariserOptions options) { + WriteApplication("to_int", node, options); + return true; + } + + public bool VisitToRealOp(VCExprNAry node, LineariserOptions options) { + WriteApplication("to_real", node, options); + return true; + } + private string ExtractDatatype(Function func) { if (func is DatatypeSelector) { DatatypeSelector selector = (DatatypeSelector) func; diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 5629c0d6..101b07a0 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -22,8 +22,8 @@ namespace Microsoft.Boogie.SMTLib // Core theory: "and", "or", "not", "iff", "true", "false", "xor", "distinct", "ite", "=", "Bool", "=>", // implies (sic!) - // Integers - "Int", "*", "/", "-", "+", "<", "<=", ">", ">=", + // Integers and reals + "Int", "Real", "*", "/", "-", "+", "<", "<=", ">", ">=", "div", "mod", // Bitvectors "extract", "concat", "bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult", @@ -48,7 +48,7 @@ namespace Microsoft.Boogie.SMTLib "lblneg", "lblpos", "lbl-lit", "if", "&&", "||", "equals", "equiv", "bool", // Boogie-defined - "int_mod", "int_div", "UOrdering2", "UOrdering3", + "real_pow", "UOrdering2", "UOrdering3", }; static HashSet reservedSmtWords; diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index a4bdee51..bff949ea 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -255,7 +255,7 @@ void ObjectInvariant() return; } - if (type.IsBool || type.IsInt || type.IsBv) + if (type.IsBool || type.IsInt || type.IsReal || type.IsBv) return; CtorType ctorType = type as CtorType; diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index df40df3d..ad0c2239 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -139,8 +139,12 @@ namespace Microsoft.Boogie.Z3 { { case TermKind.Numeral: var numstr = arg.GetNumeralString(); - var bignum = Basetypes.BigNum.FromString(numstr); - res = gen.Integer(bignum); + if (arg.GetSort().GetSortKind() == SortKind.Int) { + res = gen.Integer(Basetypes.BigNum.FromString(numstr)); + } + else { + res = gen.Real(Basetypes.BigDec.FromString(numstr)); + } break; case TermKind.App: var args = arg.GetAppArgs(); @@ -151,8 +155,14 @@ namespace Microsoft.Boogie.Z3 { switch (arg.GetAppDecl().GetKind()) { case DeclKind.Add: - if (vcargs.Length == 0) - res = gen.Integer(Basetypes.BigNum.FromInt(0)); + if (vcargs.Length == 0) { + if (arg.GetSort().GetSortKind() == SortKind.Int) { + res = gen.Integer(Basetypes.BigNum.ZERO); + } + else { + res = gen.Real(Basetypes.BigDec.ZERO); + } + } else { res = vcargs[0]; @@ -167,7 +177,7 @@ namespace Microsoft.Boogie.Z3 { break; case DeclKind.Div: Debug.Assert(vcargs.Length == 2); - res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]); + res = gen.Function(VCExpressionGenerator.RealDivOp, vcargs[0], vcargs[1]); break; case DeclKind.Eq: Debug.Assert(vcargs.Length == 2); @@ -243,8 +253,22 @@ namespace Microsoft.Boogie.Z3 { break; case DeclKind.Uminus: Debug.Assert(vcargs.Length == 1); - var bigzero = Basetypes.BigNum.FromInt(0); - res = gen.Function(VCExpressionGenerator.SubOp, gen.Integer(bigzero), vcargs[0]); + var argzero = null; + if (vcargs[0].Type.IsInt) { + argzero = gen.Integer(Basetypes.BigNum.ZERO); + } + else { + argzero = gen.Real(Basetypes.BigDec.ZERO); + } + res = gen.Function(VCExpressionGenerator.SubOp, argzero, vcargs[0]); + break; + case DeclKind.ToInt: + Debug.Assert(vcargs.Length == 1); + res = gen.Function(VCExpressionGenerator.ToIntOp, vcargs[0]); + break; + case DeclKind.ToReal: + Debug.Assert(vcargs.Length == 1); + res = gen.Function(VCExpressionGenerator.ToRealOp, vcargs[0]); break; case DeclKind.Uninterpreted: var name = arg.GetAppDecl().GetDeclName(); diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index e1c6de0b..879211f7 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -51,7 +51,8 @@ namespace Microsoft.Boogie.Z3 public bool Equals(BasicType x, BasicType y) { return (x.IsBool == y.IsBool) && - (x.IsInt == y.IsInt); + (x.IsInt == y.IsInt) && + (x.IsReal == y.IsReal); } public int GetHashCode(BasicType basicType) @@ -60,6 +61,8 @@ namespace Microsoft.Boogie.Z3 return 1; else if (basicType.IsInt) return 2; + else if (basicType.IsReal) + return 3; else throw new Exception("Basic Type " + basicType.ToString() + " is unkwown"); } @@ -175,6 +178,10 @@ namespace Microsoft.Boogie.Z3 { typeAst = z3.MkIntSort(); } + else if (basicType.IsReal) + { + typeAst = z3.MkRealSort(); + } else throw new Exception("Unknown Basic Type " + basicType.ToString()); return typeAst; diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index 0605a854..e56a7950 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -15,6 +15,8 @@ using Microsoft.Z3; namespace Microsoft.Boogie.Z3 { + using System.Numerics.BigInteger; + public class Z3apiExprLineariser : IVCExprVisitor { private Z3apiOpLineariser opLineariser = null; @@ -110,7 +112,7 @@ namespace Microsoft.Boogie.Z3 return z3.MkSub(unwrapChildren); } - if (op == VCExpressionGenerator.DivOp) { + if (op == VCExpressionGenerator.DivOp || op == VCExpressionGenerator.RealDivOp) { return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); } @@ -126,6 +128,14 @@ namespace Microsoft.Boogie.Z3 return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]); } + if (op == VCExpressionGenerator.ToIntOp) { + return z3.MkToInt(unwrapChildren[0]); + } + + if (op == VCExpressionGenerator.ToRealOp) { + return z3.MkToReal(unwrapChildren[0]); + } + throw new Exception("unhandled boogie operator"); } @@ -139,11 +149,25 @@ namespace Microsoft.Boogie.Z3 else if (node == VCExpressionGenerator.False) return cm.z3.MkFalse(); else if (node is VCExprIntLit) - return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort()); - else - { - Contract.Assert(false); - throw new cce.UnreachableException(); + return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort()); + else if (node is VCExprRealLit) { + string m = ((VCExprRealLit)node).Val.Mantissa.ToString(); + BigInteger e = ((VCExprRealLit)node).Val.Exponent; + string f = BigInteger.Pow(10, e.Abs); + + if (e == 0) { + return cm.z3.MkNumeral(m, cm.z3.MkRealSort()); + } + else if (((VCExprRealLit)node).Val.Exponent > 0) { + return cm.z3.MkMul(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort())); + } + else { + return cm.z3.MkDiv(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort())); + } + } + else { + Contract.Assert(false); + throw new cce.UnreachableException(); } } @@ -548,6 +572,18 @@ namespace Microsoft.Boogie.Z3 return WriteApplication(node.Op, node, options); } + public Term VisitRealDivOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitPowOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + public Term VisitLtOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); @@ -590,6 +626,18 @@ namespace Microsoft.Boogie.Z3 return WriteApplication(node.Op, node, options); } + public Term VisitToIntOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitToRealOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); diff --git a/Source/VCExpr/BigLiteralAbstracter.cs b/Source/VCExpr/BigLiteralAbstracter.cs index 7eb93541..879ab6d6 100644 --- a/Source/VCExpr/BigLiteralAbstracter.cs +++ b/Source/VCExpr/BigLiteralAbstracter.cs @@ -120,7 +120,7 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Ensures(Contract.Result() != null); if (lit.IsNegative) - return Gen.Function(VCExpressionGenerator.SubOp, + return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), RepresentPos(lit.Neg)); else return RepresentPos(lit); @@ -145,7 +145,7 @@ namespace Microsoft.Boogie.VCExprAST { BigNum dist = lit - Literals[index - 1].Key; if (dist < resDistance) { resDistance = dist; - res = Gen.Function(VCExpressionGenerator.AddOp, + res = Gen.Function(VCExpressionGenerator.AddIOp, Literals[index - 1].Value, Gen.Integer(dist)); } } @@ -154,7 +154,7 @@ namespace Microsoft.Boogie.VCExprAST { BigNum dist = Literals[index].Key - lit; if (dist < resDistance) { resDistance = dist; - res = Gen.Function(VCExpressionGenerator.SubOp, + res = Gen.Function(VCExpressionGenerator.SubIOp, Literals[index].Value, Gen.Integer(dist)); } } @@ -198,7 +198,7 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(bExpr != null); BigNum dist = bValue - aValue; - VCExpr distExpr = Gen.Function(VCExpressionGenerator.SubOp, bExpr, aExpr); + VCExpr distExpr = Gen.Function(VCExpressionGenerator.SubIOp, bExpr, aExpr); if (dist <= ConstantDistanceTPO) // constants that are sufficiently close to each other are put // into a precise relationship diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 1561aec0..3035c9de 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -328,6 +328,8 @@ namespace Microsoft.Boogie.VCExprAST { } } else if (node.Val is BigNum) { return Gen.Integer(node.asBigNum); + } else if (node.Val is BigDec) { + return Gen.Real(node.asBigDec); } else if (node.Val is BvConst) { return Gen.Bitvector((BvConst)node.Val); } else { @@ -961,8 +963,20 @@ namespace Microsoft.Boogie.VCExprAST { public VCExpr Visit(UnaryOperator unaryOperator) { //Contract.Requires(unaryOperator != null); Contract.Ensures(Contract.Result() != null); - Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Not && this.args.Count == 1); - return Gen.Not(this.args); + Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Neg || unaryOperator.Op == UnaryOperator.Opcode.Not); + Contract.Assert(this.args.Count == 1); + if (unaryOperator.Op == UnaryOperator.Opcode.Neg) { + VCExpr e = cce.NonNull(this.args[0]); + if (cce.NonNull(e.Type).IsInt) { + return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e); + } + else { + return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e); + } + } + else { + return Gen.Not(this.args); + } } public VCExpr Visit(BinaryOperator binaryOperator) { @@ -996,6 +1010,21 @@ namespace Microsoft.Boogie.VCExprAST { return this.args[0]; } + public VCExpr Visit(ArithmeticCoercion arithCoercion) { + //Contract.Requires(arithCoercion != null); + Contract.Ensures(Contract.Result() != null); + Contract.Assert(this.args.Count == 1); + switch (arithCoercion.Coercion) { + case ArithmeticCoercion.CoercionType.ToInt: + return Gen.Function(VCExpressionGenerator.ToIntOp, this.args); + case ArithmeticCoercion.CoercionType.ToReal: + return Gen.Function(VCExpressionGenerator.ToRealOp, this.args); + default: + Contract.Assert(false); + return null; + } + } + public VCExpr Visit(IfThenElse ite) { //Contract.Requires(ite != null); Contract.Ensures(Contract.Result() != null); @@ -1012,15 +1041,42 @@ namespace Microsoft.Boogie.VCExprAST { switch (app.Op) { case BinaryOperator.Opcode.Add: - return Gen.Function(VCExpressionGenerator.AddOp, args); + if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + return Gen.Function(VCExpressionGenerator.AddIOp, args); + } + else { + return Gen.Function(VCExpressionGenerator.AddROp, args); + } case BinaryOperator.Opcode.Sub: - return Gen.Function(VCExpressionGenerator.SubOp, args); + if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + return Gen.Function(VCExpressionGenerator.SubIOp, args); + } + else { + return Gen.Function(VCExpressionGenerator.SubROp, args); + } case BinaryOperator.Opcode.Mul: - return Gen.Function(VCExpressionGenerator.MulOp, args); + if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + return Gen.Function(VCExpressionGenerator.MulIOp, args); + } + else { + return Gen.Function(VCExpressionGenerator.MulROp, args); + } case BinaryOperator.Opcode.Div: - return Gen.Function(VCExpressionGenerator.DivOp, args); + return Gen.Function(VCExpressionGenerator.DivIOp, args); case BinaryOperator.Opcode.Mod: return Gen.Function(VCExpressionGenerator.ModOp, args); + case BinaryOperator.Opcode.RealDiv: + VCExpr arg0 = cce.NonNull(args[0]); + VCExpr arg1 = cce.NonNull(args[1]); + if (cce.NonNull(arg0.Type).IsInt) { + arg0 = Gen.Function(VCExpressionGenerator.ToRealOp, arg0); + } + if (cce.NonNull(arg1.Type).IsInt) { + arg1 = Gen.Function(VCExpressionGenerator.ToRealOp, arg1); + } + return Gen.Function(VCExpressionGenerator.DivROp, arg0, arg1); + case BinaryOperator.Opcode.Pow: + return Gen.Function(VCExpressionGenerator.PowOp, args); case BinaryOperator.Opcode.Eq: case BinaryOperator.Opcode.Iff: // we don't distinguish between equality and equivalence at this point diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index 848fafcb..02e3adda 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -376,6 +376,13 @@ namespace Microsoft.Boogie.VCExprAST { internal const string intMulName = "*"; internal const string intDivName = "/"; internal const string intModName = "%"; + internal const string realAddName = "realAdd"; + internal const string realSubName = "realSub"; + internal const string realMulName = "realMul"; + internal const string realDivName = "realDiv"; + internal const string realPowName = "realPow"; + internal const string toIntName = "toIntCoercion"; + internal const string toRealName = "toRealCoercion"; internal void AssertAsTerm(string x, LineariserOptions options) { Contract.Requires(options != null); @@ -928,10 +935,16 @@ namespace Microsoft.Boogie.VCExprAST { public bool VisitAddOp(VCExprNAry node, LineariserOptions options) { //Contract.Requires(options != null); //Contract.Requires(node != null); - if (CommandLineOptions.Clo.ReflectAdd) { - WriteTermApplication(intAddNameReflect, node, options); - } else { - WriteTermApplication(intAddName, node, options); + if (node.Type.IsInt) { + if (CommandLineOptions.Clo.ReflectAdd) { + WriteTermApplication(intAddNameReflect, node, options); + } + else { + WriteTermApplication(intAddName, node, options); + } + } + else { + WriteTermApplication(realAddName, node, options); } return true; } @@ -939,14 +952,24 @@ namespace Microsoft.Boogie.VCExprAST { public bool VisitSubOp(VCExprNAry node, LineariserOptions options) { //Contract.Requires(options != null); //Contract.Requires(node != null); - WriteTermApplication(intSubName, node, options); + if (node.Type.IsInt) { + WriteTermApplication(intSubName, node, options); + } + else { + WriteTermApplication(realSubName, node, options); + } return true; } public bool VisitMulOp(VCExprNAry node, LineariserOptions options) { //Contract.Requires(options != null); //Contract.Requires(node != null); - WriteTermApplication(intMulName, node, options); + if (node.Type.IsInt) { + WriteTermApplication(intMulName, node, options); + } + else { + WriteTermApplication(realMulName, node, options); + } return true; } @@ -964,6 +987,20 @@ namespace Microsoft.Boogie.VCExprAST { return true; } + public bool VisitRealDivOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(realDivName, node, options); + return true; + } + + public bool VisitPowOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(realPowName, node, options); + return true; + } + public bool VisitLtOp(VCExprNAry node, LineariserOptions options) { //Contract.Requires(options != null); //Contract.Requires(node != null); @@ -1006,6 +1043,20 @@ namespace Microsoft.Boogie.VCExprAST { return true; } + public bool VisitToIntOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteApplication(toIntName, node, options); + return true; + } + + public bool VisitToRealOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteApplication(toRealName, node, options); + return true; + } + public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) { //Contract.Requires(options != null); //Contract.Requires(node != null); diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index fb91d326..9d366c9f 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -524,6 +524,7 @@ namespace Microsoft.Boogie.TypeErasure { public virtual void Setup() { GetBasicTypeRepr(Type.Int); + GetBasicTypeRepr(Type.Real); GetBasicTypeRepr(Type.Bool); } @@ -625,6 +626,7 @@ namespace Microsoft.Boogie.TypeErasure { base.Setup(); GetTypeCasts(Type.Int); + GetTypeCasts(Type.Real); GetTypeCasts(Type.Bool); } @@ -730,7 +732,7 @@ namespace Microsoft.Boogie.TypeErasure { //////////////////////////////////////////////////////////////////////////// // the only types that we allow in "untyped" expressions are U, - // Type.Int, and Type.Bool + // Type.Int, Type.Real, and Type.Bool public override Type TypeAfterErasure(Type type) { //Contract.Requires(type != null); @@ -746,7 +748,7 @@ namespace Microsoft.Boogie.TypeErasure { [Pure] public override bool UnchangedType(Type type) { //Contract.Requires(type != null); - return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays); + return type.IsInt || type.IsReal || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays); } public VCExpr Cast(VCExpr expr, Type toType) { @@ -1143,7 +1145,7 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Requires(bindings != null); Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); - Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int); + Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int || node.Type == Type.Real); return node; } @@ -1360,7 +1362,7 @@ namespace Microsoft.Boogie.TypeErasure { } // Cast the arguments of the node to their old type if necessary and possible; otherwise use - // their new type (int, bool, or U) + // their new type (int, real, bool, or U) private VCExpr CastArgumentsToOldType(VCExprNAry node, VariableBindings bindings, int newPolarity) { Contract.Requires(bindings != null); Contract.Requires(node != null); @@ -1448,19 +1450,19 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArguments(node, node.Type, bindings, 0); } public override VCExpr VisitSubOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArguments(node, node.Type, bindings, 0); } public override VCExpr VisitMulOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArguments(node, node.Type, bindings, 0); } public override VCExpr VisitDivOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); @@ -1474,29 +1476,41 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result() != null); return CastArguments(node, Type.Int, bindings, 0); } + public override VCExpr VisitRealDivOp(VCExprNAry node, VariableBindings bindings) { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, Type.Real, bindings, 0); + } + public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, Type.Real, bindings, 0); + } public override VCExpr VisitLtOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArgumentsToOldType(node, bindings, 0); } public override VCExpr VisitLeOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArgumentsToOldType(node, bindings, 0); } public override VCExpr VisitGtOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArgumentsToOldType(node, bindings, 0); } public override VCExpr VisitGeOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArgumentsToOldType(node, bindings, 0); } public override VCExpr VisitSubtypeOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); @@ -1504,6 +1518,18 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result() != null); return CastArguments(node, AxBuilder.U, bindings, 0); } + public override VCExpr VisitToIntOp(VCExprNAry node, VariableBindings bindings) { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitToRealOp(VCExprNAry node, VariableBindings bindings) { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 38541881..fcfd0041 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -49,6 +49,12 @@ namespace Microsoft.Boogie { return new VCExprIntLit(x); } + public VCExpr/*!*/ Real(BigDec x) { + Contract.Ensures(Contract.Result() != null); + + return new VCExprRealLit(x); + } + public VCExpr/*!*/ Function(VCExprOp/*!*/ op, List/*!*/ arguments, List/*!*/ typeArguments) { @@ -199,7 +205,8 @@ namespace Microsoft.Boogie { Contract.Requires(e1 != null); Contract.Ensures(Contract.Result() != null); - return Function(AddOp, e0, e1); + VCExprOp op = cce.NonNull(cce.NonNull(e0).Type).IsInt ? AddIOp : AddROp; + return Function(op, e0, e1); } public VCExpr/*!*/ Or(VCExpr/*!*/ e0, VCExpr/*!*/ e1) { Contract.Requires(e0 != null); @@ -308,11 +315,16 @@ namespace Microsoft.Boogie { //////////////////////////////////////////////////////////////////////////////// // Further operators - public static readonly VCExprOp AddOp = new VCExprNAryOp(2, Type.Int); - public static readonly VCExprOp SubOp = new VCExprNAryOp(2, Type.Int); - public static readonly VCExprOp MulOp = new VCExprNAryOp(2, Type.Int); - public static readonly VCExprOp DivOp = new VCExprNAryOp(2, Type.Int); + public static readonly VCExprOp AddIOp = new VCExprNAryOp(2, Type.Int); + public static readonly VCExprOp AddROp = new VCExprNAryOp(2, Type.Real); + public static readonly VCExprOp SubIOp = new VCExprNAryOp(2, Type.Int); + public static readonly VCExprOp SubROp = new VCExprNAryOp(2, Type.Real); + public static readonly VCExprOp MulIOp = new VCExprNAryOp(2, Type.Int); + public static readonly VCExprOp MulROp = new VCExprNAryOp(2, Type.Real); + public static readonly VCExprOp DivIOp = new VCExprNAryOp(2, Type.Int); + public static readonly VCExprOp DivROp = new VCExprNAryOp(2, Type.Real); public static readonly VCExprOp ModOp = new VCExprNAryOp(2, Type.Int); + public static readonly VCExprOp PowOp = new VCExprNAryOp(2, Type.Real); public static readonly VCExprOp LtOp = new VCExprNAryOp(2, Type.Bool); public static readonly VCExprOp LeOp = new VCExprNAryOp(2, Type.Bool); public static readonly VCExprOp GtOp = new VCExprNAryOp(2, Type.Bool); @@ -322,6 +334,8 @@ namespace Microsoft.Boogie { // the type of the compared terms public static readonly VCExprOp Subtype3Op = new VCExprNAryOp(3, Type.Bool); public static readonly VCExprOp IfThenElseOp = new VCExprIfThenElseOp(); + public static readonly VCExprOp ToIntOp = new VCExprNAryOp(1, Type.Int); + public static readonly VCExprOp ToRealOp = new VCExprNAryOp(1, Type.Real); public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool); @@ -376,13 +390,17 @@ namespace Microsoft.Boogie { MulOp, DivOp, ModOp, + RealDivOp, + PowOp, LtOp, LeOp, GtOp, GeOp, SubtypeOp, Subtype3Op, - BvConcatOp + BvConcatOp, + ToIntOp, + ToRealOp }; internal static Dictionary/*!*/ SingletonOpDict; [ContractInvariantMethod] @@ -399,17 +417,24 @@ namespace Microsoft.Boogie { SingletonOpDict.Add(AndOp, SingletonOp.AndOp); SingletonOpDict.Add(OrOp, SingletonOp.OrOp); SingletonOpDict.Add(ImpliesOp, SingletonOp.ImpliesOp); - SingletonOpDict.Add(AddOp, SingletonOp.AddOp); - SingletonOpDict.Add(SubOp, SingletonOp.SubOp); - SingletonOpDict.Add(MulOp, SingletonOp.MulOp); - SingletonOpDict.Add(DivOp, SingletonOp.DivOp); + SingletonOpDict.Add(AddIOp, SingletonOp.AddOp); + SingletonOpDict.Add(AddROp, SingletonOp.AddOp); + SingletonOpDict.Add(SubIOp, SingletonOp.SubOp); + SingletonOpDict.Add(SubROp, SingletonOp.SubOp); + SingletonOpDict.Add(MulIOp, SingletonOp.MulOp); + SingletonOpDict.Add(MulROp, SingletonOp.MulOp); + SingletonOpDict.Add(DivIOp, SingletonOp.DivOp); + SingletonOpDict.Add(DivROp, SingletonOp.RealDivOp); SingletonOpDict.Add(ModOp, SingletonOp.ModOp); + SingletonOpDict.Add(PowOp, SingletonOp.PowOp); SingletonOpDict.Add(LtOp, SingletonOp.LtOp); SingletonOpDict.Add(LeOp, SingletonOp.LeOp); SingletonOpDict.Add(GtOp, SingletonOp.GtOp); SingletonOpDict.Add(GeOp, SingletonOp.GeOp); SingletonOpDict.Add(SubtypeOp, SingletonOp.SubtypeOp); SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op); + SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp); + SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp); } //////////////////////////////////////////////////////////////////////////////// @@ -810,6 +835,27 @@ namespace Microsoft.Boogie.VCExprAST { } } + public class VCExprRealLit : VCExprLiteral { + public readonly BigDec Val; + internal VCExprRealLit(BigDec val) + : base(Type.Real) { + this.Val = val; + } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object that) { + if (Object.ReferenceEquals(this, that)) + return true; + if (that is VCExprRealLit) + return Val == ((VCExprRealLit)that).Val; + return false; + } + [Pure] + public override int GetHashCode() { + return Val.GetHashCode() * 72321; + } + } + ///////////////////////////////////////////////////////////////////////////////// // Operator expressions with fixed arity [ContractClassFor(typeof(VCExprNAry))] @@ -1218,6 +1264,10 @@ namespace Microsoft.Boogie.VCExprAST { return visitor.VisitDivOp(expr, arg); case VCExpressionGenerator.SingletonOp.ModOp: return visitor.VisitModOp(expr, arg); + case VCExpressionGenerator.SingletonOp.RealDivOp: + return visitor.VisitRealDivOp(expr, arg); + case VCExpressionGenerator.SingletonOp.PowOp: + return visitor.VisitPowOp(expr, arg); case VCExpressionGenerator.SingletonOp.LtOp: return visitor.VisitLtOp(expr, arg); case VCExpressionGenerator.SingletonOp.LeOp: @@ -1232,6 +1282,10 @@ namespace Microsoft.Boogie.VCExprAST { return visitor.VisitSubtype3Op(expr, arg); case VCExpressionGenerator.SingletonOp.BvConcatOp: return visitor.VisitBvConcatOp(expr, arg); + case VCExpressionGenerator.SingletonOp.ToIntOp: + return visitor.VisitToIntOp(expr, arg); + case VCExpressionGenerator.SingletonOp.ToRealOp: + return visitor.VisitToRealOp(expr, arg); default: Contract.Assert(false); throw new cce.UnreachableException(); diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index adb3b27e..00e6fb9c 100644 --- a/Source/VCExpr/VCExprASTPrinter.cs +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -290,12 +290,22 @@ namespace Microsoft.Boogie.VCExprAST { public bool VisitDivOp(VCExprNAry node, TextWriter wr) { //Contract.Requires(wr != null); //Contract.Requires(node != null); - return PrintNAry("/", node, wr); + return PrintNAry("div", node, wr); } public bool VisitModOp(VCExprNAry node, TextWriter wr) { //Contract.Requires(wr != null); //Contract.Requires(node != null); - return PrintNAry("%", node, wr); + return PrintNAry("mod", node, wr); + } + public bool VisitRealDivOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("/", node, wr); + } + public bool VisitPowOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("**", node, wr); } public bool VisitLtOp(VCExprNAry node, TextWriter wr) { //Contract.Requires(wr != null); @@ -327,6 +337,16 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return PrintNAry("<::", node, wr); } + public bool VisitToIntOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("int", node, wr); + } + public bool VisitToRealOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("real", node, wr); + } public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) { //Contract.Requires(wr != null); //Contract.Requires(node != null); diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 1a29bbeb..1dd1cac9 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -75,12 +75,16 @@ namespace Microsoft.Boogie.VCExprAST { Result VisitMulOp(VCExprNAry node, Arg arg); Result VisitDivOp(VCExprNAry node, Arg arg); Result VisitModOp(VCExprNAry node, Arg arg); + Result VisitRealDivOp(VCExprNAry node, Arg arg); + Result VisitPowOp(VCExprNAry node, Arg arg); Result VisitLtOp(VCExprNAry node, Arg arg); Result VisitLeOp(VCExprNAry node, Arg arg); Result VisitGtOp(VCExprNAry node, Arg arg); Result VisitGeOp(VCExprNAry node, Arg arg); Result VisitSubtypeOp(VCExprNAry node, Arg arg); Result VisitSubtype3Op(VCExprNAry node, Arg arg); + Result VisitToIntOp(VCExprNAry node, Arg arg); + Result VisitToRealOp(VCExprNAry node, Arg arg); Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg); Result VisitIfThenElseOp(VCExprNAry node, Arg arg); Result VisitCustomOp(VCExprNAry node, Arg arg); @@ -179,6 +183,16 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException(); } + public Result VisitRealDivOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitPowOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + public Result VisitLtOp(VCExprNAry node, Arg arg) { Contract.Requires(node != null); throw new NotImplementedException(); @@ -209,6 +223,16 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException(); } + public Result VisitToIntOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitToRealOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) { Contract.Requires(node != null); throw new NotImplementedException(); @@ -1427,6 +1451,14 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return StandardResult(node, arg); } + public virtual Result VisitRealDivOp(VCExprNAry node, Arg arg) { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitPowOp(VCExprNAry node, Arg arg) { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } public virtual Result VisitLtOp(VCExprNAry node, Arg arg) { //Contract.Requires(node != null); return StandardResult(node, arg); @@ -1451,6 +1483,14 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return StandardResult(node, arg); } + public virtual Result VisitToIntOp(VCExprNAry node, Arg arg) { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitToRealOp(VCExprNAry node, Arg arg) { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) { //Contract.Requires(node != null); return StandardResult(node, arg); diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer index dd5bcff2..bfe185e7 100644 --- a/Test/aitest1/Answer +++ b/Test/aitest1/Answer @@ -268,7 +268,7 @@ implementation p() A: assume {:inferred} true; - assume 0 - 1 <= x; + assume -1 <= x; assume {:inferred} -1 <= x; goto B, E; diff --git a/Test/inline/Answer b/Test/inline/Answer index 655143fa..eddeb64f 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -566,7 +566,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in var b: bool; anon0: - ret := 0 - 1; + ret := -1; b := false; found := b; i := 0; @@ -659,7 +659,7 @@ implementation main(x: int) goto inline$find$0$anon0; inline$find$0$anon0: - inline$find$0$ret := 0 - 1; + inline$find$0$ret := -1; inline$find$0$b := false; inline$find$0$found := inline$find$0$b; inline$find$0$i := 0; @@ -756,7 +756,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in var inline$check$0$ret: bool; anon0: - ret := 0 - 1; + ret := -1; b := false; found := b; i := 0; diff --git a/Test/test0/Answer b/Test/test0/Answer index d57e7647..0eda9e2e 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -34,6 +34,12 @@ const y: int; const z: int; +const r: real; + +const s: real; + +const t: real; + const P: bool; const Q: bool; @@ -56,6 +62,36 @@ axiom x + y mod z == y mod z + x; axiom (x + y) mod z == x mod z + y mod z; +axiom x / y / z == x / (y / z); + +axiom x / y / (z / x) == x / y / z; + +axiom x / s / z == x / (s / z); + +axiom x / s / (z / x) == x / s / z; + +axiom r / s / t == r / (s / t); + +axiom r / s / (t / r) == r / s / t; + +axiom r * s / t == r * s / t; + +axiom r / s * t == r / s * t; + +axiom (r * s) ** t == r ** t * s ** t; + +axiom r ** (s + t) == r ** s * r ** t; + +axiom int(real(x)) == x; + +axiom r >= 0e0 ==> real(int(r)) <= r; + +axiom int(0e0 - 2e-2) == 0; + +axiom int(0e0 - 35e0) == -35; + +axiom int(27e-1) == 2; + axiom x - y - z == x - (y - z); axiom x - y - (z - x) == x - y - z; diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl index cb69aa5f..5fffc20a 100644 --- a/Test/test0/ModifiedBag.bpl +++ b/Test/test0/ModifiedBag.bpl @@ -1,5 +1,5 @@ // ----------- BEGIN PRELUDE -type real; + type elements; diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl index 955faad8..7e4a9ce7 100644 --- a/Test/test0/PrettyPrint.bpl +++ b/Test/test0/PrettyPrint.bpl @@ -1,6 +1,9 @@ const x: int; const y: int; const z: int; +const r: real; +const s: real; +const t: real; const P: bool; const Q: bool; const R: bool; @@ -17,6 +20,25 @@ axiom (x div y) div (z div x) == (x div y) div z; axiom x + y mod z == ((y mod z) + x); axiom (x + y) mod z == (x mod z) + (y mod z); +axiom x / y / z == (x / (y / z)); +axiom (x / y) / (z / x) == (x / y) / z; +axiom x / s / z == (x / (s / z)); +axiom (x / s) / (z / x) == (x / s) / z; +axiom r / s / t == (r / (s / t)); +axiom (r / s) / (t / r) == (r / s) / t; + +axiom ((r * s) / t) == r * s / t; +axiom ((r / s) * t) == (r / s) * t; + +axiom (r * s) ** t == (r ** t) * (s ** t); +axiom r ** (s + t) == r ** s * r ** t; + +axiom int(real(x)) == x; +axiom r >= 0.0 ==> real(int(r)) <= r; +axiom int(0e-3 - 0.02) == 0; +axiom int(0e2 - 3.5e1) == -35; +axiom int(27e-1) == 2; + axiom x - y - z == (x - (y - z)); axiom (x - y) - (z - x) == (x - y) - z; diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl index ac87476f..79a4d2ab 100644 --- a/Test/test0/Prog0.bpl +++ b/Test/test0/Prog0.bpl @@ -1,5 +1,5 @@ // BoogiePL Examples -type real; + type elements; var x:int; var y:real; var z:ref; // Variables diff --git a/Test/test1/Answer b/Test/test1/Answer index a8b73b53..94bf2d9a 100644 --- a/Test/test1/Answer +++ b/Test/test1/Answer @@ -145,3 +145,22 @@ Lambda.bpl(12,8): Error: the type variable T does not occur in types of the lamb Lambda.bpl(12,2): Error: mismatched types in assignment command (cannot assign [int]int to [int]int) Lambda.bpl(18,27): Error: invalid argument types (bool and int) to binary operator + 5 type checking errors detected in Lambda.bpl +IntReal.bpl(5,8): Error: invalid argument types (int and real) to binary operator >= +IntReal.bpl(6,8): Error: invalid argument types (int and real) to binary operator <= +IntReal.bpl(7,8): Error: invalid argument types (int and real) to binary operator < +IntReal.bpl(8,8): Error: invalid argument types (int and real) to binary operator > +IntReal.bpl(10,9): Error: invalid argument types (int and real) to binary operator == +IntReal.bpl(11,8): Error: invalid argument types (int and real) to binary operator + +IntReal.bpl(12,8): Error: invalid argument types (int and real) to binary operator - +IntReal.bpl(13,8): Error: invalid argument types (int and real) to binary operator * +IntReal.bpl(14,8): Error: invalid argument types (int and real) to binary operator div +IntReal.bpl(15,8): Error: invalid argument types (int and real) to binary operator mod +IntReal.bpl(17,12): Error: invalid argument types (real and int) to binary operator == +IntReal.bpl(23,8): Error: invalid argument types (int and real) to binary operator ** +IntReal.bpl(27,14): Error: invalid argument types (real and int) to binary operator == +IntReal.bpl(29,13): Error: invalid argument types (int and real) to binary operator == +IntReal.bpl(32,6): Error: argument type int does not match expected type real +IntReal.bpl(33,6): Error: argument type real does not match expected type int +IntReal.bpl(45,8): Error: invalid argument types (real and int) to binary operator div +IntReal.bpl(46,8): Error: invalid argument types (real and int) to binary operator mod +18 type checking errors detected in IntReal.bpl \ No newline at end of file diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl new file mode 100644 index 00000000..fac41d57 --- /dev/null +++ b/Test/test1/IntReal.bpl @@ -0,0 +1,48 @@ +const i: int; +const r: real; + +axiom i == 0; +axiom i >= 0.0; // type errror +axiom i <= 0.0e0; // type errror +axiom i < 0.0e-0; // type errror +axiom i > 0.0e20; // type errror + +axiom -i == r; // type errror +axiom i + r == 0.0; // type errror +axiom i - r == 0.0; // type errror +axiom i * r == 0.0; // type errror +axiom i div r == 0; // type errror +axiom i mod r == 0; // type errror + +axiom i / i == 0; // type errror +axiom i / i == 0.0; +axiom i / r == 0.0; +axiom r / i == 0.0; +axiom r / r == 0.0; + +axiom i ** r == 0.0; // type errror +axiom r ** r == 0.0; + +axiom real(i) == 0.0; +axiom real(i) == i; // type errror +axiom int(r) == 0; +axiom int(r) == r; // type errror +axiom int(real(i)) == i; +axiom real(int(r)) == r; +axiom int(int(r)) == i; // type errror +axiom real(real(i)) == r; // type errror + +axiom i == 0; +axiom real(i) >= 0.0; +axiom real(i) <= 0.0e0; +axiom r < 0.0e-0; +axiom r > 0.0e20; + +axiom -r == real(i); +axiom real(i) + r == 0.0; +axiom r - real(0) == 0.0; +axiom r * r == 0.0; +axiom r div 0 == 0; // type errror +axiom r mod 0 == 0; // type errror + +axiom r ** r == 0.0; diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat index 979c36e4..149e6dc9 100644 --- a/Test/test1/runtest.bat +++ b/Test/test1/runtest.bat @@ -19,3 +19,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe %BGEXE% %* /noVerify FunBody.bpl %BGEXE% %* /noVerify IfThenElse0.bpl %BGEXE% %* /noVerify Lambda.bpl +%BGEXE% %* /noVerify IntReal.bpl diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl index c8ef88c8..6aee18ea 100644 --- a/Test/test2/strings-no-where.bpl +++ b/Test/test2/strings-no-where.bpl @@ -1,4 +1,4 @@ -type real; + type elements; diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl index 05e392cb..f196899f 100644 --- a/Test/test2/strings-where.bpl +++ b/Test/test2/strings-where.bpl @@ -1,4 +1,4 @@ -type real; + type elements; diff --git a/Test/test20/Answer b/Test/test20/Answer index efa5bced..fa33507e 100644 --- a/Test/test20/Answer +++ b/Test/test20/Answer @@ -118,7 +118,7 @@ axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3)); const intSet1: Set int; -axiom (forall x: int :: intSet1[x] == (x == 0 - 5 || x == 3)); +axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3)); procedure P(); @@ -126,7 +126,7 @@ procedure P(); implementation P() { - assert (forall x: int :: union(intSet0, intSet1)[x] == (x == 0 - 5 || x == 0 || x == 2 || x == 3)); + assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3)); } @@ -143,7 +143,7 @@ axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3); const intSet1: Set int; -axiom (forall x: int :: intSet1[x] <==> x == 0 - 5 || x == 3); +axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3); procedure P(); @@ -151,7 +151,7 @@ procedure P(); implementation P() { - assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == 0 - 5 || x == 0 || x == 2 || x == 3); + assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3); } diff --git a/Test/test20/Prog0.bpl b/Test/test20/Prog0.bpl index ea71b8a8..8fc7b7c7 100644 --- a/Test/test20/Prog0.bpl +++ b/Test/test20/Prog0.bpl @@ -1,5 +1,5 @@ // Let's test some Boogie 2 features ... -type real; + type elements; type Field a; diff --git a/Test/test20/Prog1.bpl b/Test/test20/Prog1.bpl index 1d75805c..0e9413c1 100644 --- a/Test/test20/Prog1.bpl +++ b/Test/test20/Prog1.bpl @@ -1,5 +1,5 @@ // Let's test some Boogie 2 features ... -type real; + type elements; type Field a; diff --git a/Test/test21/Answer b/Test/test21/Answer index 914e56a1..28aa4e8b 100644 --- a/Test/test21/Answer +++ b/Test/test21/Answer @@ -278,6 +278,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0 Boogie program verifier finished with 0 verified, 1 error +--------------------- File Real.bpl ---------------------------- + +Boogie program verifier finished with 1 verified, 0 errors --------------------- File NameClash.bpl ---------------------------- Boogie program verifier finished with 1 verified, 0 errors @@ -549,6 +552,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0 Boogie program verifier finished with 0 verified, 1 error +--------------------- File Real.bpl ---------------------------- + +Boogie program verifier finished with 1 verified, 0 errors --------------------- File NameClash.bpl ---------------------------- Boogie program verifier finished with 1 verified, 0 errors @@ -826,6 +832,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0 Boogie program verifier finished with 0 verified, 1 error +--------------------- File Real.bpl ---------------------------- + +Boogie program verifier finished with 1 verified, 0 errors --------------------- File NameClash.bpl ---------------------------- Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl new file mode 100644 index 00000000..3dcf3ea3 --- /dev/null +++ b/Test/test21/Real.bpl @@ -0,0 +1,17 @@ +axiom (forall r: real :: r == 0.0 || r / r == 1.0); + +procedure P(a: real, b: real) returns () { + assume a >= b && a != 0.0 && a >= 1.3579; + + assert 2e0 * (a + 3.0) - 0.5 >= b; + assert 2e0 * (a + 3.0) - 0.5 > b; + assert b <= 2e0 * (a + 3.0) - 0.5; + assert b < 2e0 * (a + 3.0) - 0.5; + + assert 1/2 <= 0.65; + assert a > 100e-2 ==> 1 / a <= a; + assert a / 2 != a || a == 0.00; + assert a != 0.0 ==> a / a == 1.0; + + assert int(a) >= 0 ==> real(3) * a > a; +} \ No newline at end of file diff --git a/Test/test21/runtest.bat b/Test/test21/runtest.bat index d994a4da..bfdcc570 100644 --- a/Test/test21/runtest.bat +++ b/Test/test21/runtest.bat @@ -4,6 +4,7 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe rem set BGEXE=mono ..\..\Binaries\Boogie.exe + for %%m in ( n p a ) do ( @@ -16,7 +17,8 @@ for %%f in (DisjointDomains.bpl DisjointDomains2.bpl FunAxioms.bpl Keywords.bpl Casts.bpl BooleanQuantification.bpl EmptyList.bpl Boxing.bpl MapOutputTypeParams.bpl ParallelAssignment.bpl BooleanQuantification2.bpl Flattening.bpl Orderings.bpl Orderings2.bpl Orderings3.bpl Orderings4.bpl - EmptySetBug.bpl Coercions2.bpl MapAxiomsConsistency.bpl LargeLiterals0.bpl) do ( + EmptySetBug.bpl Coercions2.bpl MapAxiomsConsistency.bpl LargeLiterals0.bpl + Real.bpl) do ( echo --------------------- File %%f ---------------------------- %BGEXE% %* /typeEncoding:%%m /logPrefix:0%%m %%f ) -- cgit v1.2.3 From a9c6c8fcf205a13c759c6f09e69b01d3b144df94 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 28 Sep 2012 15:19:53 -0700 Subject: Dafny: removed div/mod axioms, since Boogie now interprets div/mod Dafny: included FloydCycleDetect again (which had been temporarily commented out) DafnyExtension: adjusted to Boogie's change in abstract-interpretation support --- Binaries/DafnyPrelude.bpl | 15 --------------- Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy | 9 --------- Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs | 3 --- 3 files changed, 27 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 53e8e86a..5530f8a7 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -610,18 +610,3 @@ type TickType; var $Tick: TickType; // --------------------------------------------------------------- -// -- Arithmetic ------------------------------------------------- -// --------------------------------------------------------------- - -// the connection between mod and div -axiom (forall x:int, y:int :: {x mod y} {x div y} x mod y == x - x div y * y); - -// remainder is always Euclidean Modulus. -axiom (forall x:int, y:int :: {x mod y} 0 < y ==> 0 <= x mod y && x mod y < y); -axiom (forall x:int, y:int :: {x mod y} y < 0 ==> 0 <= x mod y && x mod y < -y); - -// the following axiom has some unfortunate matching, but it does state a property about mod that -// is sometimes useful -axiom (forall a: int, b: int, d: int :: { a mod d, b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b); - -// --------------------------------------------------------------- diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy index 3f68ee5d..774008b8 100644 --- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy +++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy @@ -205,7 +205,6 @@ class Node { invariant forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S); decreases S - Visited; { -assume 2<2; // TEMPORARY HACK p, steps, Visited := p.next, steps + 1, Visited + {p}; } if (p == null) { @@ -219,7 +218,6 @@ assume 2<2; // TEMPORARY HACK invariant forall k :: 0 <= k < A ==> Nexxxt(k, S) != p; decreases steps - A; { -assume 2<2; // TEMPORARY HACK A := A + 1; } B := steps - A; @@ -228,13 +226,6 @@ assume 2<2; // TEMPORARY HACK } } -/** TEMPORARY - ghost method AnalyzeList_Aux(S: set, steps: int, p: Node) returns (A: int) - ensures 0 <= A < steps; - ensures forall k :: 0 <= k < A ==> Nexxxt(k, S) != p; - ensures Nexxxt(A, S) == p; -**/ - ghost method CrucialLemma(a: int, b: int, S: set) requires IsClosed(S); requires 0 <= a && 1 <= b; diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs index 9f22b887..c691d9da 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs @@ -231,9 +231,6 @@ namespace DafnyLanguage if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) { if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) { Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program); - } else if (Bpl.CommandLineOptions.Clo.Ai.AnySet) { - // run one of the old domains - Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program); } else { // use /infer:j as the default Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true; -- cgit v1.2.3 From 247a9f10e453d7ab84fd77422ccce1a021d4fc54 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Mon, 1 Oct 2012 10:04:32 +0200 Subject: Updated the 'PrepareBoogieZip.bat' script. --- Binaries/PrepareBoogieZip.bat | 41 ++++++++++++++++++----------------------- 1 file changed, 18 insertions(+), 23 deletions(-) (limited to 'Binaries') diff --git a/Binaries/PrepareBoogieZip.bat b/Binaries/PrepareBoogieZip.bat index 9edeec4a..1f64a31c 100644 --- a/Binaries/PrepareBoogieZip.bat +++ b/Binaries/PrepareBoogieZip.bat @@ -7,33 +7,28 @@ if exist %DEST_DIR% del /q %DEST_DIR%\* if not exist %DEST_DIR% mkdir %DEST_DIR% for %%f in ( - AbsInt.dll AbsInt.pdb - AIFramework.dll AIFramework.pdb - Basetypes.dll Basetypes.pdb - Boogie.exe Boogie.pdb - BVD.exe BVD.pdb - CodeContractsExtender.dll CodeContractsExtender.pdb - Core.dll Core.pdb - Dafny.exe Dafny.pdb - DafnyPipeline.dll DafnyPipeline.pdb - Graph.dll Graph.pdb - Houdini.dll Houdini.pdb - Model.dll Model.pdb - ParserHelper.dll ParserHelper.pdb - Provers.Isabelle.dll Provers.Isabelle.pdb - Provers.Simplify.dll Provers.Simplify.pdb - Provers.SMTLib.dll Provers.SMTLib.pdb - Provers.TPTP.dll Provers.TPTP.pdb - Provers.Z3.dll Provers.Z3.pdb - VCExpr.dll VCExpr.pdb - VCGeneration.dll VCGeneration.pdb - DafnyPrelude.bpl - DafnyRuntime.cs + AbsInt.dll AbsInt.pdb + Basetypes.dll Basetypes.pdb + Boogie.exe Boogie.pdb + CodeContractsExtender.dll CodeContractsExtender.pdb + Core.dll Core.pdb + Dafny.exe Dafny.pdb + DafnyPrelude.bpl DafnyRuntime.cs + DafnyPipeline.dll DafnyPipeline.pdb + Graph.dll Graph.pdb + Houdini.dll + Model.dll Model.pdb + ParserHelper.dll ParserHelper.pdb + Provers.SMTLib.dll Provers.SMTLib.pdb TypedUnivBackPred2.sx - UnivBackPred2.smt2 + UnivBackPred2.smt UnivBackPred2.smt2 UnivBackPred2.sx + VCExpr.dll VCExpr.pdb + VCGeneration.dll VCGeneration.pdb ) do ( copy %%f %DEST_DIR% ) +xcopy /E /I /Y CodeContracts "%DEST_DIR%/CodeContracts" + echo Done. Now, manually put the contents of the %DEST_DIR% directory into Boogie.zip -- cgit v1.2.3