diff options
70 files changed, 2878 insertions, 711 deletions
diff --git a/Binaries/Boogie.vshost.exe.manifest b/Binaries/Boogie.vshost.exe.manifest new file mode 100644 index 00000000..061c9ca9 --- /dev/null +++ b/Binaries/Boogie.vshost.exe.manifest @@ -0,0 +1,11 @@ +<?xml version="1.0" encoding="UTF-8" standalone="yes"?> +<assembly xmlns="urn:schemas-microsoft-com:asm.v1" manifestVersion="1.0"> + <assemblyIdentity version="1.0.0.0" name="MyApplication.app"/> + <trustInfo xmlns="urn:schemas-microsoft-com:asm.v2"> + <security> + <requestedPrivileges xmlns="urn:schemas-microsoft-com:asm.v3"> + <requestedExecutionLevel level="asInvoker" uiAccess="false"/> + </requestedPrivileges> + </security> + </trustInfo> +</assembly> diff --git a/Binaries/PrepareBoogieZip.bat b/Binaries/PrepareBoogieZip.bat index 5a1b267f..99a7a0a6 100644 --- a/Binaries/PrepareBoogieZip.bat +++ b/Binaries/PrepareBoogieZip.bat @@ -7,22 +7,22 @@ if exist %DEST_DIR% del /q %DEST_DIR%\* if not exist %DEST_DIR% mkdir %DEST_DIR% for %%f in ( - AbsInt.dll AbsInt.pdb - Basetypes.dll Basetypes.pdb - Boogie.exe Boogie.pdb - BVD.exe BVD.pdb - CodeContractsExtender.dll CodeContractsExtender.pdb - Core.dll Core.pdb - Doomed.dll Doomed.pdb - Graph.dll Graph.pdb - Houdini.dll Houdini.pdb - Model.dll Model.pdb - ParserHelper.dll ParserHelper.pdb - Predication.dll Predication.pdb - Provers.SMTLib.dll Provers.SMTLib.pdb - UnivBackPred2.smt UnivBackPred2.smt2 - VCExpr.dll VCExpr.pdb - VCGeneration.dll VCGeneration.pdb + BoogieAbsInt.dll BoogieAbsInt.pdb + BoogieBasetypes.dll BoogieBasetypes.pdb + Boogie.exe Boogie.pdb + BVD.exe BVD.pdb + BoogieCodeContractsExtender.dll BoogieCodeContractsExtender.pdb + BoogieCore.dll BoogieCore.pdb + BoogieDoomed.dll BoogieDoomed.pdb + BoogieGraph.dll BoogieGraph.pdb + BoogieHoudini.dll BoogieHoudini.pdb + BoogieModel.dll BoogieModel.pdb + BoogieParserHelper.dll BoogieParserHelper.pdb + BoogiePredication.dll BoogiePredication.pdb + Provers.SMTLib.dll Provers.SMTLib.pdb + UnivBackPred2.smt UnivBackPred2.smt2 + BoogieVCExpr.dll BoogieVCExpr.pdb + BoogieVCGeneration.dll BoogieVCGeneration.pdb ) do ( copy %%f %DEST_DIR% ) @@ -33,9 +33,13 @@ several other institutions make the open-source Boogie tool what it is.  +More documentation can be found at http://boogie-docs.readthedocs.org/en/latest/ . + ## Language Reference -[This is Boogie2](http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf) details +See [Language reference](http://boogie-docs.readthedocs.org/en/latest/LangRef.html). + +Note: [This is Boogie2](http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf) details many aspects of the Boogie IVL but is slightly out of date. ## Getting help diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj index 47f45f58..359eb146 100644 --- a/Source/AbsInt/AbsInt.csproj +++ b/Source/AbsInt/AbsInt.csproj @@ -9,7 +9,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>AbsInt</RootNamespace> - <AssemblyName>AbsInt</AssemblyName> + <AssemblyName>BoogieAbsInt</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> @@ -34,7 +34,7 @@ <IsWebBootstrapper>false</IsWebBootstrapper> <UseApplicationTrust>false</UseApplicationTrust> <BootstrapperEnabled>true</BootstrapperEnabled> - <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> </PropertyGroup> <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> <DebugSymbols>true</DebugSymbols> diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 2fd37463..1d35b735 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -180,8 +180,7 @@ namespace Microsoft.Boogie.AbstractInterpretation } } return e; - } else { - Contract.Assert(V.TypedIdent.Type.IsReal); + } else if (V.TypedIdent.Type.IsReal){ Expr e = Expr.True; if (Lo != null && Hi != null && Lo == Hi) { // produce an equality @@ -199,6 +198,30 @@ namespace Microsoft.Boogie.AbstractInterpretation } } return e; + } else { + Contract.Assert(V.TypedIdent.Type.IsFloat); + Expr e = Expr.True; + if (Lo != null && Hi != null && Lo == Hi) + { + // produce an equality + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type))); + } + else + { + // produce a (possibly empty) conjunction of inequalities + if (Lo != null) + { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide)); + } + if (Hi != null) + { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type))); + } + } + return e; } } } @@ -208,6 +231,8 @@ namespace Microsoft.Boogie.AbstractInterpretation return null; } else if (ty.IsReal) { return Expr.Literal(Basetypes.BigDec.FromBigInt(n)); + } else if (ty.IsFloat) { + return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatSignificand)); } else { Contract.Assume(ty.IsInt); return Expr.Literal(Basetypes.BigNum.FromBigInt(n)); @@ -669,6 +694,11 @@ namespace Microsoft.Boogie.AbstractInterpretation ((BigDec)node.Val).FloorCeiling(out floor, out ceiling); Lo = floor; Hi = ceiling; + } else if (node.Val is BigFloat) { + BigInteger floor, ceiling; + ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling); + Lo = floor; + Hi = ceiling; } else if (node.Val is bool) { if ((bool)node.Val) { // true diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj index 5e46877a..5b425bc5 100644 --- a/Source/Basetypes/Basetypes.csproj +++ b/Source/Basetypes/Basetypes.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <PropertyGroup> <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> @@ -9,7 +9,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>Basetypes</RootNamespace> - <AssemblyName>Basetypes</AssemblyName> + <AssemblyName>BoogieBasetypes</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> @@ -34,7 +34,7 @@ <IsWebBootstrapper>false</IsWebBootstrapper> <UseApplicationTrust>false</UseApplicationTrust> <BootstrapperEnabled>true</BootstrapperEnabled> - <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> </PropertyGroup> <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> <DebugSymbols>true</DebugSymbols> @@ -163,6 +163,7 @@ </Compile> <Compile Include="BigDec.cs" /> <Compile Include="BigNum.cs" /> + <Compile Include="BigFloat.cs" /> <Compile Include="Rational.cs" /> <Compile Include="Set.cs" /> </ItemGroup> @@ -200,4 +201,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project> +</Project>
\ No newline at end of file diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs new file mode 100644 index 00000000..cb248340 --- /dev/null +++ b/Source/Basetypes/BigFloat.cs @@ -0,0 +1,509 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics.Contracts; +using System.Diagnostics; + +namespace Microsoft.Basetypes +{ + using BIM = System.Numerics.BigInteger; + + /// <summary> + /// A representation of a 32-bit floating point value + /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand + /// </summary> + public struct BigFloat + { + //Please note that this code outline is copy-pasted from BigDec.cs + + // the internal representation + [Rep] + internal readonly BIM significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left) + [Rep] + internal readonly int significandSize; + [Rep] + internal readonly BIM exponent; //The value of the exponent is always positive as per fp representation requirements + [Rep] + internal readonly int exponentSize; //The bit size of the exponent + [Rep] + internal readonly String value; //Only used with second syntax + [Rep] + internal readonly bool isNeg; + + public BIM Significand { + get { + return significand; + } + } + + public BIM Exponent { + get { + return exponent; + } + } + + public int SignificandSize { + get { + return significandSize; + } + } + + public int ExponentSize { + get { + return exponentSize; + } + } + + public bool IsNegative { + get { + return this.isNeg; + } + } + + public String Value { + get { + return value; + } + } + + public static BigFloat ZERO = new BigFloat(false, BIM.Zero, BIM.Zero, 24, 8); //Does not include negative zero + + private static readonly BIM two = new BIM(2); + private static readonly BIM one = new BIM(1); + private static BIM two_n(int n) { + BIM toReturn = one; + for (int i = 0; i < n; i++) + toReturn = toReturn * two; + return toReturn; + } + + + //////////////////////////////////////////////////////////////////////////// + // Constructors + + //Please note that these constructors will be called throughout boogie + //For a complete summary of where this class has been added, simply view constructor references + + [Pure] + public static BigFloat FromInt(int v) { + return new BigFloat(v.ToString(), 24, 8); + } + + public static BigFloat FromInt(int v, int significandSize, int exponentSize) + { + return new BigFloat(v.ToString(), significandSize, exponentSize); + } + + public static BigFloat FromBigInt(BIM v) { + return new BigFloat(v.ToString(), 24, 8); + } + + public static BigFloat FromBigInt(BIM v, int significandSize, int exponentSize) + { + return new BigFloat(v.ToString(), significandSize, exponentSize); + } + + public static BigFloat FromBigDec(BigDec v) + { + return new BigFloat(v.ToDecimalString(), 24, 8); + } + + public static BigFloat FromBigDec(BigDec v, int significandSize, int exponentSize) + { + return new BigFloat(v.ToDecimalString(), significandSize, exponentSize); + } + + [Pure] + public static BigFloat FromString(String s) { + /* + * String must be either of the format *e*f*e* + * or of the special value formats: 0NaN*e* 0nan*e* 0+oo*e* 0-oo*e* + * Where * indicates an integer value (digit) + */ + BIM sig, exp; + int sigSize, expSize; + bool isNeg; + + if (s.IndexOf('f') == -1) { + String val = s; + sigSize = int.Parse(s.Substring(4, s.IndexOf('e')-4)); + expSize = int.Parse(s.Substring(s.IndexOf('e') + 1)); + if (sigSize <= 0 || expSize <= 0) + throw new FormatException("Significand and Exponent sizes must be greater than 0"); + return new BigFloat(val, sigSize, expSize); + } + + sig = BIM.Parse(s.Substring(0, s.IndexOf('e'))); + exp = BIM.Parse(s.Substring(s.IndexOf('e') + 1, s.IndexOf('f') - s.IndexOf('e') - 1)); + sigSize = int.Parse(s.Substring(s.IndexOf('f') + 1, s.IndexOf('e', s.IndexOf('e') + 1) - s.IndexOf('f') - 1)); + expSize = int.Parse(s.Substring(s.IndexOf('e', s.IndexOf('e') + 1) + 1)); + isNeg = s[0] == '-'; //We do this so that -0 is parsed correctly + + if (sigSize <= 0 || expSize <= 0) + throw new FormatException("Significand and Exponent sizes must be greater than 0"); + + sigSize = sigSize - 1; //Get rid of sign bit + sig = BIM.Abs(sig); //sig must be positive + //Uncomment if you want to shift the exponent for the user (i.e. 0e-1f24e8 --> 0e126f24e8) + //exp = exp + BIM.Pow(new BIM(2), expSize-1) - BIM.One; + + if (exp < 0 || exp >= BIM.Pow(new BIM(2), expSize)) + throw new FormatException("The given exponent " + exp + " cannot fit in the bit size " + expSize); + + if (sig >= BIM.Pow(new BIM(2), sigSize)) + throw new FormatException("The given significand " + sig + " cannot fit in the bit size " + (sigSize+1)); + + return new BigFloat(isNeg, sig, exp, sigSize, expSize); + } + + public BigFloat(bool isNeg, BIM significand, BIM exponent, int significandSize, int exponentSize) { + this.exponentSize = exponentSize; + this.exponent = exponent; + this.significand = significand; + this.significandSize = significandSize+1; + this.isNeg = isNeg; + this.value = ""; + } + + public BigFloat(String value, int significandSize, int exponentSize) { + this.exponentSize = exponentSize; + this.significandSize = significandSize; + this.exponent = BIM.Zero; + this.significand = BIM.Zero; + this.value = value; + if (value.Equals("nan")) + this.value = "NaN"; + this.isNeg = value[0] == '-'; + } + + private BIM maxsignificand() + { + BIM result = one; + for (int i = 0; i < significandSize; i++) + result = result * two; + return result - one; + } + private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; } + + + + //////////////////////////////////////////////////////////////////////////// + // Basic object operations + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is BigFloat)) + return false; + + return (this == (BigFloat)obj); + } + + [Pure] + public override int GetHashCode() { + return significand.GetHashCode() * 13 + Exponent.GetHashCode(); + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result<string>() != null); + return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value; + } + + + //////////////////////////////////////////////////////////////////////////// + // Conversion operations + + /// <summary> + /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!! + /// Converts the given decimal value (provided as a string) to the nearest floating point approximation + /// the returned fp assumes the given significand and exponent size + /// </summary> + /// <param name="value"></param> + /// <param name="significandSize"></param> + /// <param name="exponentSize"></param> + /// <returns></returns> + public static BigFloat Round(String value, int exponentSize, int significandSize) + { + int i = value.IndexOf('.'); + if (i == -1) + return Round(BIM.Parse(value), BIM.Zero, exponentSize, significandSize); + return Round(i == 0 ? BIM.Zero : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize); + } + + /// <summary> + /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!! + /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize + /// Returns the result of this calculation + /// </summary> + /// <param name="value"></param> + /// <param name="power"></param> + /// <param name="significandSize"></param> + /// <param name="exponentSize"></param> + /// <returns></returns> + public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int significandSize) + { + int exp = 0; + BIM one = new BIM(1); + BIM ten = new BIM(10); + BIM dec_max = new BIM(0); //represents the order of magnitude of dec_value for carrying during calculations + + //First, determine the exponent + while (value > one) { //Divide by two, increment exponent by 1 + if (!(value % two).IsZero) { //Add "1.0" to the decimal + dec_max = new BIM(10); + while (dec_max < dec_value) + dec_max = dec_max * ten; + dec_value = dec_value + dec_max; + } + value = value / two; + if (!(dec_value % ten).IsZero) + dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division + dec_value = dec_value / two; + exp++; + } + if (value.IsZero && !dec_value.IsZero) { + dec_max = new BIM(10); + while (dec_max < dec_value) + dec_max = dec_max * ten; + while (value.IsZero) {//Multiply by two, decrement exponent by 1 + dec_value = dec_value * two; + if (dec_value >= dec_max) { + dec_value = dec_value - dec_max; + value = value + one; + } + exp--; + } + } + + //Second, calculate the significand + value = new BIM(0); //remove implicit bit + dec_max = new BIM(10); + while (dec_max < dec_value) + dec_max = dec_max * ten; + for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated + dec_value = dec_value * two; + if (dec_value >= dec_max) { + dec_value = dec_value - dec_max; + value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation + } + } + + return new BigFloat(false, BIM.Zero, BIM.Parse(value.ToString()), exponentSize, significandSize); //Sign not actually checked... + } + + // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). + /// <summary> + /// NOTE: This may give wrong results, it hasn't been tested extensively + /// If you're getting weird bugs, you may want to check this function out... + /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative + /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way. + /// </summary> + /// <param name="floor">The Floor (rounded towards negative infinity)</param> + /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param> + public void FloorCeiling(out BIM floor, out BIM ceiling) + { + BIM two = new BIM(2); + + BIM sig = Significand + BIM.Pow(two, SignificandSize); //Add hidden bit + BIM exp = Exponent - BIM.Pow(two, ExponentSize-1) + 1; + + while (exp > BIM.Zero) { + exp--; + sig = sig << 1; + } + + sig = sig >> SignificandSize; + + if (isNeg) { + ceiling = -sig + 1; + floor = -sig; + } + else { + ceiling = sig + 1; + floor = sig; + } + } + + [Pure] + public String ToDecimalString(int maxDigits) { + //TODO: fix for fp functionality + { + throw new NotImplementedException(); + } + } + + public String ToBVString(){ + if (this.IsSpecialType) { + return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize; + } + else if (this.Value == "") { + return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")"; + } + else { + return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")"; + } + } + + [Pure] + public string ToDecimalString() { + Contract.Ensures(Contract.Result<string>() != null); + return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value; + } + + [Pure] + public static string Zeros(int n) { + //TODO: fix for fp functionality + Contract.Requires(0 <= n); + if (n <= 10) { + var tenZeros = "0000000000"; + return tenZeros.Substring(0, n); + } else { + var d = n / 2; + var s = Zeros(d); + if (n % 2 == 0) { + return s + s; + } else { + return s + s + "0"; + } + } + } + + + //////////////////////////////////////////////////////////////////////////// + // Basic arithmetic operations + + [Pure] + public BigFloat Abs { + get { + return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize); + } + } + + [Pure] + public BigFloat Negate { + get { + if (value != "") + return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize); + return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize); + } + } + + [Pure] + public static BigFloat operator -(BigFloat x) { + return x.Negate; + } + + [Pure] + public static BigFloat operator +(BigFloat x, BigFloat y) { + //TODO: Modify for correct fp functionality + Contract.Requires(x.ExponentSize == y.ExponentSize); + Contract.Requires(x.significandSize == y.significandSize); + BIM m1 = x.significand; + BIM e1 = x.Exponent; + BIM m2 = y.significand; + BIM e2 = y.Exponent; + m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit + m2 = m2 + two_n(y.significandSize + 1); + if (e2 > e1) { + m1 = y.significand; + e1 = y.Exponent; + m2 = x.significand; + e2 = x.Exponent; + } + + while (e2 < e1) { + m2 = m2 / two; + e2 = e2 + one; + } + + return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize); + } + + [Pure] + public static BigFloat operator -(BigFloat x, BigFloat y) { + return x + y.Negate; + } + + [Pure] + public static BigFloat operator *(BigFloat x, BigFloat y) { + Contract.Requires(x.ExponentSize == y.ExponentSize); + Contract.Requires(x.significandSize == y.significandSize); + return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize); + } + + + //////////////////////////////////////////////////////////////////////////// + // Some basic comparison operations + + public bool IsSpecialType { + get { + if (value == "") + return false; + return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero")); + } + } + + public bool IsPositive { + get { + return !IsNegative; + } + } + + public bool IsZero { + get { + return significand.Equals(BigNum.ZERO) && Exponent == BIM.Zero; + } + } + + [Pure] + public int CompareTo(BigFloat that) { + if (this.exponent > that.exponent) + return 1; + if (this.exponent < that.exponent) + return -1; + if (this.significand == that.significand) + return 0; + return this.significand > that.significand ? 1 : -1; + } + + [Pure] + public static bool operator ==(BigFloat x, BigFloat y) { + return x.CompareTo(y) == 0; + } + + [Pure] + public static bool operator !=(BigFloat x, BigFloat y) { + return x.CompareTo(y) != 0; + } + + [Pure] + public static bool operator <(BigFloat x, BigFloat y) { + return x.CompareTo(y) < 0; + } + + [Pure] + public static bool operator >(BigFloat x, BigFloat y) { + return x.CompareTo(y) > 0; + } + + [Pure] + public static bool operator <=(BigFloat x, BigFloat y) { + return x.CompareTo(y) <= 0; + } + + [Pure] + public static bool operator >=(BigFloat x, BigFloat y) { + return x.CompareTo(y) >= 0; + } + } +} diff --git a/Source/CodeContractsExtender/CodeContractsExtender.csproj b/Source/CodeContractsExtender/CodeContractsExtender.csproj index 05701c12..38535dc4 100644 --- a/Source/CodeContractsExtender/CodeContractsExtender.csproj +++ b/Source/CodeContractsExtender/CodeContractsExtender.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <PropertyGroup> <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> @@ -9,7 +9,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>CodeContractsExtender</RootNamespace> - <AssemblyName>CodeContractsExtender</AssemblyName> + <AssemblyName>BoogieCodeContractsExtender</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <SignAssembly>true</SignAssembly> @@ -34,7 +34,7 @@ <IsWebBootstrapper>false</IsWebBootstrapper> <UseApplicationTrust>false</UseApplicationTrust> <BootstrapperEnabled>true</BootstrapperEnabled> - <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> </PropertyGroup> <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> <DebugSymbols>true</DebugSymbols> @@ -199,4 +199,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project> +</Project>
\ No newline at end of file diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj index 113019fd..ac90077c 100644 --- a/Source/Concurrency/Concurrency.csproj +++ b/Source/Concurrency/Concurrency.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" /> <PropertyGroup> @@ -8,7 +8,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>Concurrency</RootNamespace> - <AssemblyName>Concurrency</AssemblyName> + <AssemblyName>BoogieConcurrency</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> @@ -112,4 +112,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project> +</Project>
\ No newline at end of file diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 7ffd5f7f..409254d0 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -313,6 +313,13 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<NAryExpr>() != null); return Binary(BinaryOperator.Opcode.RealDiv, e1, e2); } + public static NAryExpr FloatDiv(Expr e1, Expr e2) + { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result<NAryExpr>() != null); + return Binary(BinaryOperator.Opcode.FloatDiv, e1, e2); + } public static NAryExpr Pow(Expr e1, Expr e2) { Contract.Requires(e2 != null); Contract.Requires(e1 != null); @@ -356,6 +363,11 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<LiteralExpr>() != null); return new LiteralExpr(Token.NoToken, value); } + public static LiteralExpr Literal(BigFloat value) + { + Contract.Ensures(Contract.Result<LiteralExpr>() != null); + return new LiteralExpr(Token.NoToken, value); + } private static LiteralExpr/*!*/ true_ = Literal(true); public static LiteralExpr/*!*/ True { @@ -514,7 +526,7 @@ namespace Microsoft.Boogie { } public class LiteralExpr : Expr { - public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, or a BvConst + public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, a BigFloat, or a BvConst [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Val != null); @@ -563,6 +575,21 @@ namespace Microsoft.Boogie { } /// <summary> + /// Creates a literal expression for the floating point value "v". + /// </summary> + /// <param name="tok"></param> + /// <param name="v"></param> + public LiteralExpr(IToken/*!*/ tok, BigFloat v, bool immutable = false) + : base(tok, immutable) + { + Contract.Requires(tok != null); + Val = v; + Type = Type.GetFloatType(v.SignificandSize, v.ExponentSize); + if (immutable) + CachedHashCode = ComputeHashCode(); + } + + /// <summary> /// Creates a literal expression for the bitvector value "v". /// </summary> public LiteralExpr(IToken/*!*/ tok, BigNum v, int b, bool immutable=false) @@ -633,6 +660,9 @@ namespace Microsoft.Boogie { return Type.Int; } else if (Val is BigDec) { return Type.Real; + } else if (Val is BigFloat) { + BigFloat temp = (BigFloat)Val; + return Type.GetFloatType(temp.SignificandSize, temp.ExponentSize); } else if (Val is BvConst) { return Type.GetBvType(((BvConst)Val).Bits); } else { @@ -681,6 +711,14 @@ namespace Microsoft.Boogie { } } + public bool isBigFloat + { + get + { + return Val is BigFloat; + } + } + public BigDec asBigDec { get { Contract.Assert(isBigDec); @@ -688,6 +726,13 @@ namespace Microsoft.Boogie { } } + public BigFloat asBigFloat { + get { + Contract.Assert(isBigFloat); + return (BigFloat)cce.NonNull(Val); + } + } + public bool isBool { get { return Val is bool; @@ -1355,6 +1400,9 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real)) { return Type.Real; } + //if (arg0type.Unify(Type.Float)) { + //return Type.Float; + //} goto BAD_TYPE; case Opcode.Not: if (arg0type.Unify(Type.Bool)) { @@ -1399,6 +1447,9 @@ namespace Microsoft.Boogie { if (argument is BigDec) { return -((BigDec)argument); } + if (argument is BigFloat) { + return -((BigFloat)argument); + } break; case Opcode.Not: if (argument is bool) { @@ -1431,6 +1482,7 @@ namespace Microsoft.Boogie { Div, Mod, RealDiv, + FloatDiv, Pow, Eq, Neq, @@ -1671,6 +1723,12 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { return Type.Real; } + if (arg0type.IsFloat && arg0type.Unify(arg1type)) { + return Type.GetFloatType(arg0.Type.FloatSignificand, arg0.Type.FloatExponent); + } + if (arg1type.IsFloat && arg1type.Unify(arg0type)) { + return Type.GetFloatType(arg1.Type.FloatSignificand, arg1.Type.FloatExponent); + } goto BAD_TYPE; case Opcode.Div: case Opcode.Mod: @@ -1683,6 +1741,12 @@ namespace Microsoft.Boogie { (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real))) { return Type.Real; } + if (arg0type.IsFloat && arg0type.Unify(arg1type)) { + return Type.GetFloatType(arg0.Type.FloatSignificand, arg0.Type.FloatExponent); + } + if (arg1type.IsFloat && arg1type.Unify(arg0type)) { + return Type.GetFloatType(arg1.Type.FloatSignificand, arg1.Type.FloatExponent); + } goto BAD_TYPE; case Opcode.Pow: if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { @@ -1715,6 +1779,9 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { return Type.Bool; } + if ((arg0type.IsFloat && arg0type.Unify(arg1type)) || (arg1type.IsFloat && arg1type.Unify(arg0type))) { + return Type.Bool; + } goto BAD_TYPE; case Opcode.And: case Opcode.Or: @@ -1825,6 +1892,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) + ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) + ((BigFloat)e2); + } break; case Opcode.Sub: if (e1 is BigNum && e2 is BigNum) { @@ -1833,6 +1903,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) - ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) - ((BigFloat)e2); + } break; case Opcode.Mul: if (e1 is BigNum && e2 is BigNum) { @@ -1841,6 +1914,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) * ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) * ((BigFloat)e2); + } break; case Opcode.Div: if (e1 is BigNum && e2 is BigNum) { @@ -1855,6 +1931,9 @@ namespace Microsoft.Boogie { case Opcode.RealDiv: // TODO: add partial evaluation fro real division break; + case Opcode.FloatDiv: + //TODO: add float division + break; case Opcode.Pow: // TODO: add partial evaluation fro real exponentiation break; @@ -1865,6 +1944,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) < ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) < ((BigFloat)e2); + } break; case Opcode.Le: if (e1 is BigNum && e2 is BigNum) { @@ -1873,6 +1955,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) <= ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) <= ((BigFloat)e2); + } break; case Opcode.Gt: if (e1 is BigNum && e2 is BigNum) { @@ -1881,6 +1966,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) > ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) > ((BigFloat)e2); + } break; case Opcode.Ge: if (e1 is BigNum && e2 is BigNum) { @@ -1889,6 +1977,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) >= ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) >= ((BigFloat)e2); + } break; case Opcode.And: @@ -1990,7 +2081,7 @@ namespace Microsoft.Boogie { } else { - this.name.Emit(stream, 0xF0, false); + this.name.Emit(stream, 0xF0, false); } if (stream.UseForComputingChecksums) { @@ -2177,7 +2268,8 @@ namespace Microsoft.Boogie { public class ArithmeticCoercion : IAppliable { public enum CoercionType { ToInt, - ToReal + ToReal, + ToFloat } private IToken/*!*/ tok; diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 2953f15e..ab6ef5e9 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -244,6 +244,11 @@ namespace Microsoft.Boogie { return false; } } + public virtual bool IsFloat { + get { + return false; + } + } public virtual bool IsBool { get { return false; @@ -320,6 +325,29 @@ namespace Microsoft.Boogie { } } + public virtual bool isFloat { + get { + return false; + } + } + public virtual int FloatExponent + { + get + { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.FloatExponent should never be called + } + } + public virtual int FloatSignificand { + get { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.FloatSignificand should never be called + } + } public virtual bool IsBv { get { return false; @@ -358,6 +386,14 @@ namespace Microsoft.Boogie { } } + static public FloatType GetFloatType(int sig, int exp) { + Contract.Requires(0 <= exp); + Contract.Requires(0 <= sig); + Contract.Ensures(Contract.Result<FloatType>() != null); + + return new FloatType(sig, exp); + } + //------------ Match formal argument types on actual argument types //------------ and return the resulting substitution of type variables @@ -1008,6 +1044,165 @@ namespace Microsoft.Boogie { //===================================================================== + //Note that the functions in this class were directly copied from the BV class just below + public class FloatType : Type { + public readonly int Significand; //Size of Significand in bits + public readonly int Exponent; //Size of exponent in bits + + public FloatType(IToken token, int significand, int exponent) + : base(token) { + Contract.Requires(token != null); + Significand = significand; + Exponent = exponent; + } + + public FloatType(int significand, int exponent) + : base(Token.NoToken) { + Significand = significand; + Exponent = exponent; + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively. + + public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) + { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result<Type>() != null); + // FloatTypes are immutable anyway, we do not clone + return this; + } + + public override Type CloneUnresolved() + { + Contract.Ensures(Contract.Result<Type>() != null); + return this; + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) + { + //Contract.Requires(stream != null); + // no parentheses are necessary for bitvector-types + stream.SetToken(this); + stream.Write("{0}", this); + } + + public override string ToString() + { + Contract.Ensures(Contract.Result<string>() != null); + return "float" + Significand + "e" + Exponent; + } + + //----------- Equality ---------------------------------- + + [Pure] + public override bool Equals(Type/*!*/ that, + List<TypeVariable>/*!*/ thisBoundVariables, + List<TypeVariable>/*!*/ thatBoundVariables) + { + FloatType thatFloatType = TypeProxy.FollowProxy(that.Expanded) as FloatType; + return thatFloatType != null && this.Significand == thatFloatType.Significand && this.Exponent == thatFloatType.Exponent; + } + + //----------- Unification of types ----------- + + public override bool Unify(Type/*!*/ that, + List<TypeVariable>/*!*/ unifiableVariables, + // an idempotent substitution that describes the + // unification result up to a certain point + IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) + { + //Contract.Requires(that != null); + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(cce.NonNullElements(unifier)); + that = that.Expanded; + if (that is TypeProxy || that is TypeVariable) { + return that.Unify(this, unifiableVariables, unifier); + } + else { + return this.Equals(that); + } + } + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) + { + Contract.Ensures(Contract.Result<Type>() != null); + return this; + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List<TypeVariable> boundVariables) + { + return this.Significand.GetHashCode() + this.Exponent.GetHashCode(); + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) + { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result<Type>() != null); + // nothing to resolve + return this; + } + + // determine the free variables in a type, in the order in which the variables occur + public override List<TypeVariable>/*!*/ FreeVariables + { + get + { + Contract.Ensures(Contract.Result<List<TypeVariable>>() != null); + + return new List<TypeVariable>(); // bitvector-type are closed + } + } + + public override List<TypeProxy/*!*/>/*!*/ FreeProxies + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>())); + return new List<TypeProxy/*!*/>(); + } + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsFloat { + get { + return true; + } + } + public override int FloatSignificand { + get { + return Significand; + } + } + public override int FloatExponent { + get { + return Exponent; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) + { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result<Absy>() != null); + return visitor.VisitFloatType(this); + } + + } + + //===================================================================== + public class BvType : Type { public readonly int Bits; @@ -1286,7 +1481,7 @@ Contract.Requires(that != null); public override Type ResolveType(ResolutionContext rc) { //Contract.Requires(rc != null); Contract.Ensures(Contract.Result<Type>() != null); - // first case: the type name denotes a bitvector-type + // first case: the type name denotes a bitvector-type or float-type if (Name.StartsWith("bv") && Name.Length > 2) { bool is_bv = true; for (int i = 2; i < Name.Length; ++i) { @@ -1305,6 +1500,28 @@ Contract.Requires(that != null); } } + if (Name.StartsWith("float") && Name.Length > 5) + { + bool is_float = true; + int i = 5; + for (; is_float && Name[i] != 'e'; i++) + if (i >= Name.Length-1 || !char.IsDigit(Name[i])) //There must be an e + is_float = false; + int mid = i; + i++; + for (; i < Name.Length && is_float; i++) + if (!char.IsDigit(Name[i])) + is_float = false; + if (is_float) { + if (Arguments.Count > 0) { + rc.Error(this, + "float types must not be applied to arguments: {0}", + Name); + } + return new FloatType(tok, int.Parse(Name.Substring(5, mid-5)), int.Parse(Name.Substring(mid+1))); + } + } + // second case: the identifier is resolved to a type variable TypeVariable var = rc.LookUpTypeBinder(Name); if (var != null) { @@ -1899,6 +2116,12 @@ Contract.Requires(that != null); return p != null && p.IsReal; } } + public override bool IsFloat { + get { + Type p = ProxyFor; + return p != null && p.IsFloat; + } + } public override bool IsBool { get { Type p = ProxyFor; @@ -2747,11 +2970,20 @@ Contract.Requires(that != null); return ExpandedType.IsInt; } } - public override bool IsReal { - get { + public override bool IsReal + { + get + { return ExpandedType.IsReal; } } + public override bool IsFloat + { + get + { + return ExpandedType.IsFloat; + } + } public override bool IsBool { get { return ExpandedType.IsBool; diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 091ceeb0..f74f8bff 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -144,7 +144,12 @@ TOKENS string = quote { regularStringChar | "\\\"" } quote. decimal = digit {digit} 'e' [ '-' ] digit {digit} . - float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] . + dec_float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] . + float = [ '-' ] digit {digit} 'e' [ '-' ] digit {digit} 'f' digit {digit} 'e' digit {digit} + | '0' 'N' 'a' 'N' digit {digit} 'e' digit {digit} + | '0' 'n' 'a' 'n' digit {digit} 'e' digit {digit} + | '0' '+' 'o' 'o' digit {digit} 'e' digit {digit} + | '0' '-' 'o' 'o' digit {digit} 'e' digit {digit} . COMMENTS FROM "/*" TO "*/" NESTED COMMENTS FROM "//" TO lf @@ -330,7 +335,7 @@ TypeAtom<out Bpl.Type/*!*/ ty> ( "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 */ + /* note: bitvectors and floats are handled in UnresolvedTypeIdentifier */ | "(" Type<out ty> @@ -1252,7 +1257,7 @@ ArrayExpression<out Expr/*!*/ e> /*------------------------------------------------------------------------*/ AtomExpression<out Expr/*!*/ e> -= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; += (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat bf; List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig; List<TypeVariable>/*!*/ typeParams; IdentifierExpr/*!*/ id; @@ -1265,6 +1270,7 @@ AtomExpression<out Expr/*!*/ e> | "true" (. e = new LiteralExpr(t, true); .) | Nat<out bn> (. e = new LiteralExpr(t, bn); .) | Dec<out bd> (. e = new LiteralExpr(t, bd); .) + | Float<out bf> (. e = new LiteralExpr(t, bf); .) | BvLit<out bn, out n> (. e = new LiteralExpr(t, bn, n); .) | Ident<out x> (. id = new IdentifierExpr(x, x.val); e = id; .) @@ -1290,7 +1296,7 @@ AtomExpression<out Expr/*!*/ e> Expression<out e> ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e }); .) - | "(" ( Expression<out e> (. if (e is BvBounds) + | "(" ( Expression<out e> (. if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + "are not allowed"); .) | Forall (. x = t; .) @@ -1479,7 +1485,7 @@ Dec<out BigDec n> ( decimal (. s = t.val; .) | - float (. s = t.val; .) + dec_float (. s = t.val; .) ) (. try { n = BigDec.FromString(s); @@ -1508,4 +1514,19 @@ BvLit<out BigNum n, out int m> } .) . + +Float<out BigFloat n> += (. string s = ""; .) + ( + float (. s = t.val; .) + ) + (. try { + n = BigFloat.FromString(s); + } catch (FormatException e) { + this.SemErr("incorrectly formatted floating point, " + e.Message); + n = BigFloat.ZERO; + } + .) + . + END BoogiePL. diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 36bcc6c3..7c4cb7ae 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -9,7 +9,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>Core</RootNamespace> - <AssemblyName>Core</AssemblyName> + <AssemblyName>BoogieCore</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> @@ -34,7 +34,7 @@ <IsWebBootstrapper>false</IsWebBootstrapper> <UseApplicationTrust>false</UseApplicationTrust> <BootstrapperEnabled>true</BootstrapperEnabled> - <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> </PropertyGroup> <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> <DebugSymbols>true</DebugSymbols> @@ -186,7 +186,7 @@ </ItemGroup> <ItemGroup> <ProjectReference Include="..\Basetypes\Basetypes.csproj"> - <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project> + <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project> <Name>Basetypes</Name> </ProjectReference> <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj"> diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 793bb96e..c91de177 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -23,8 +23,9 @@ public class Parser { public const int _digits = 3; public const int _string = 4; public const int _decimal = 5; - public const int _float = 6; - public const int maxT = 96; + public const int _dec_float = 6; + public const int _float = 7; + public const int maxT = 97; const bool T = true; const bool x = false; @@ -132,7 +133,8 @@ private class BvBounds : Expr { Contract.Assert(false);throw new cce.UnreachableException(); } public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); } - public override int ComputeHashCode() { + public override int ComputeHashCode() + { return base.GetHashCode(); } } @@ -219,7 +221,7 @@ private class BvBounds : Expr { while (StartOf(1)) { switch (la.kind) { - case 21: { + case 22: { Consts(out vs); foreach(Bpl.Variable/*!*/ v in vs){ Contract.Assert(v != null); @@ -228,7 +230,7 @@ private class BvBounds : Expr { break; } - case 25: { + case 26: { Function(out ds); foreach(Bpl.Declaration/*!*/ d in ds){ Contract.Assert(d != null); @@ -237,12 +239,12 @@ private class BvBounds : Expr { break; } - case 29: { + case 30: { Axiom(out ax); Pgm.AddTopLevelDeclaration(ax); break; } - case 30: { + case 31: { UserDefinedTypes(out ts); foreach(Declaration/*!*/ td in ts){ Contract.Assert(td != null); @@ -251,7 +253,7 @@ private class BvBounds : Expr { break; } - case 7: { + case 8: { GlobalVars(out vs); foreach(Bpl.Variable/*!*/ v in vs){ Contract.Assert(v != null); @@ -260,7 +262,7 @@ private class BvBounds : Expr { break; } - case 32: { + case 33: { Procedure(out pr, out im); Pgm.AddTopLevelDeclaration(pr); if (im != null) { @@ -269,7 +271,7 @@ private class BvBounds : Expr { break; } - case 33: { + case 34: { Implementation(out nnim); Pgm.AddTopLevelDeclaration(nnim); break; @@ -285,17 +287,17 @@ private class BvBounds : Expr { bool u = false; QKeyValue kv = null; bool ChildrenComplete = false; List<ConstantParent/*!*/> Parents = null; - Expect(21); + Expect(22); y = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } - if (la.kind == 22) { + if (la.kind == 23) { Get(); u = true; } IdsType(out xs); - if (la.kind == 23) { + if (la.kind == 24) { OrderSpec(out ChildrenComplete, out Parents); } bool makeClone = false; @@ -319,7 +321,7 @@ private class BvBounds : Expr { ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv)); } - Expect(8); + Expect(9); } void Function(out List<Declaration>/*!*/ ds) { @@ -336,44 +338,44 @@ private class BvBounds : Expr { Expr definition = null; Expr/*!*/ tmp; - Expect(25); - while (la.kind == 27) { + Expect(26); + while (la.kind == 28) { Attribute(ref kv); } Ident(out z); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out typeParamTok, out typeParams); } - Expect(9); + Expect(10); if (StartOf(2)) { VarOrType(out tyd, out argKv); arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); - while (la.kind == 12) { + while (la.kind == 13) { Get(); VarOrType(out tyd, out argKv); arguments.Add(new Formal(tyd.tok, tyd, true, argKv)); } } - Expect(10); + Expect(11); argKv = null; - if (la.kind == 26) { + if (la.kind == 27) { Get(); - Expect(9); - VarOrType(out retTyd, out argKv); Expect(10); - } else if (la.kind == 11) { + VarOrType(out retTyd, out argKv); + Expect(11); + } else if (la.kind == 12) { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); - } else SynErr(97); - if (la.kind == 27) { + } else SynErr(98); + if (la.kind == 28) { Get(); Expression(out tmp); definition = tmp; - Expect(28); - } else if (la.kind == 8) { + Expect(29); + } else if (la.kind == 9) { Get(); - } else SynErr(98); + } else SynErr(99); if (retTyd == null) { // construct a dummy type for the case of syntax error retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int)); @@ -428,30 +430,30 @@ private class BvBounds : Expr { void Axiom(out Axiom/*!*/ m) { Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; - Expect(29); - while (la.kind == 27) { + Expect(30); + while (la.kind == 28) { Attribute(ref kv); } IToken/*!*/ x = t; Proposition(out e); - Expect(8); + Expect(9); m = new Axiom(x,e, null, kv); } void UserDefinedTypes(out List<Declaration/*!*/>/*!*/ ts) { Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> (); - Expect(30); - while (la.kind == 27) { + Expect(31); + while (la.kind == 28) { Attribute(ref kv); } UserDefinedType(out decl, kv); ts.Add(decl); - while (la.kind == 12) { + while (la.kind == 13) { Get(); UserDefinedType(out decl, kv); ts.Add(decl); } - Expect(8); + Expect(9); } void GlobalVars(out List<Variable>/*!*/ ds) { @@ -460,12 +462,12 @@ private class BvBounds : Expr { ds = new List<Variable>(); var dsx = ds; - Expect(7); - while (la.kind == 27) { + Expect(8); + while (la.kind == 28) { Attribute(ref kv); } IdsTypeWheres(true, "global variables", delegate(TypedIdent tyd) { dsx.Add(new GlobalVariable(tyd.tok, tyd, kv)); } ); - Expect(8); + Expect(9); } void Procedure(out Procedure/*!*/ proc, out /*maybe null*/ Implementation impl) { @@ -481,9 +483,9 @@ private class BvBounds : Expr { QKeyValue kv = null; impl = null; - Expect(32); + Expect(33); ProcSignature(true, out x, out typeParams, out ins, out outs, out kv); - if (la.kind == 8) { + if (la.kind == 9) { Get(); while (StartOf(3)) { Spec(pre, mods, post); @@ -496,7 +498,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(99); + } else SynErr(100); proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); } @@ -508,7 +510,7 @@ private class BvBounds : Expr { StmtList/*!*/ stmtList; QKeyValue kv; - Expect(33); + Expect(34); 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); @@ -522,7 +524,7 @@ private class BvBounds : Expr { void IdsTypeWheres(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) { IdsTypeWhere(allowWhereClauses, context, action); - while (la.kind == 12) { + while (la.kind == 13) { Get(); IdsTypeWhere(allowWhereClauses, context, action); } @@ -532,12 +534,12 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out ds) != null); QKeyValue kv = null; - Expect(7); - while (la.kind == 27) { + Expect(8); + while (la.kind == 28) { Attribute(ref kv); } IdsTypeWheres(true, "local variables", delegate(TypedIdent tyd) { ds.Add(new LocalVariable(tyd.tok, tyd, kv)); } ); - Expect(8); + Expect(9); } void ProcFormals(bool incoming, bool allowWhereClauses, out List<Variable>/*!*/ ds) { @@ -546,16 +548,16 @@ private class BvBounds : Expr { var dsx = ds; var context = allowWhereClauses ? "procedure formals" : "the 'implementation' copies of formals"; - Expect(9); - if (la.kind == 1 || la.kind == 27) { + Expect(10); + if (la.kind == 1 || la.kind == 28) { AttrsIdsTypeWheres(allowWhereClauses, allowWhereClauses, context, delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new Formal(tyd.tok, tyd, incoming, kv)); }); } - Expect(10); + Expect(11); } void AttrsIdsTypeWheres(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) { AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action); - while (la.kind == 12) { + while (la.kind == 13) { Get(); AttributesIdsTypeWhere(allowAttributes, allowWhereClauses, context, action); } @@ -574,7 +576,7 @@ private class BvBounds : Expr { void IdsType(out List<TypedIdent>/*!*/ tyds) { Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; Idents(out ids); - Expect(11); + Expect(12); Type(out ty); tyds = new List<TypedIdent>(); foreach(Token/*!*/ id in ids){ @@ -588,7 +590,7 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); Ident(out id); xs.Add(id); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Ident(out id); xs.Add(id); @@ -606,14 +608,14 @@ private class BvBounds : Expr { TypeArgs(args); } ty = new UnresolvedTypeIdentifier (tok, tok.val, args); - } else if (la.kind == 17 || la.kind == 19) { + } else if (la.kind == 18 || la.kind == 20) { MapType(out ty); - } else SynErr(100); + } else SynErr(101); } void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) { QKeyValue kv = null; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); if (!allowAttributes) { kv = null; @@ -627,9 +629,9 @@ private class BvBounds : Expr { void IdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) { List<IToken>/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne; Idents(out ids); - Expect(11); + Expect(12); Type(out ty); - if (la.kind == 13) { + if (la.kind == 14) { Get(); Expression(out nne); if (!allowWhereClauses) { @@ -649,7 +651,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 == 55 || la.kind == 56) { + while (la.kind == 56 || la.kind == 57) { EquivOp(); x = t; ImpliesExpression(false, out e1); @@ -659,20 +661,20 @@ private class BvBounds : Expr { void TypeAtom(out Bpl.Type/*!*/ ty) { Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; - if (la.kind == 14) { + if (la.kind == 15) { Get(); ty = new BasicType(t, SimpleType.Int); - } else if (la.kind == 15) { + } else if (la.kind == 16) { Get(); ty = new BasicType(t, SimpleType.Real); - } else if (la.kind == 16) { + } else if (la.kind == 17) { Get(); ty = new BasicType(t, SimpleType.Bool); - } else if (la.kind == 9) { + } else if (la.kind == 10) { Get(); Type(out ty); - Expect(10); - } else SynErr(101); + Expect(11); + } else SynErr(102); } void Ident(out IToken/*!*/ x) { @@ -699,10 +701,10 @@ private class BvBounds : Expr { if (StartOf(6)) { TypeArgs(ts); } - } else if (la.kind == 17 || la.kind == 19) { + } else if (la.kind == 18 || la.kind == 20) { MapType(out ty); ts.Add(ty); - } else SynErr(102); + } else SynErr(103); } void MapType(out Bpl.Type/*!*/ ty) { @@ -712,16 +714,16 @@ private class BvBounds : Expr { Bpl.Type/*!*/ result; List<TypeVariable>/*!*/ typeParameters = new List<TypeVariable>(); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out nnTok, out typeParameters); tok = nnTok; } - Expect(17); + Expect(18); if (tok == null) tok = t; if (StartOf(6)) { Types(arguments); } - Expect(18); + Expect(19); Type(out result); ty = new MapType(tok, typeParameters, arguments, result); @@ -729,10 +731,10 @@ private class BvBounds : Expr { void TypeParams(out IToken/*!*/ tok, out List<TypeVariable>/*!*/ typeParams) { Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List<IToken>/*!*/ typeParamToks; - Expect(19); + Expect(20); tok = t; Idents(out typeParamToks); - Expect(20); + Expect(21); typeParams = new List<TypeVariable> (); foreach(Token/*!*/ id in typeParamToks){ Contract.Assert(id != null); @@ -744,7 +746,7 @@ private class BvBounds : Expr { Contract.Requires(ts != null); Bpl.Type/*!*/ ty; Type(out ty); ts.Add(ty); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Type(out ty); ts.Add(ty); @@ -756,21 +758,21 @@ private class BvBounds : Expr { Parents = null; bool u; IToken/*!*/ parent; - Expect(23); + Expect(24); Parents = new List<ConstantParent/*!*/> (); u = false; - if (la.kind == 1 || la.kind == 22) { - if (la.kind == 22) { + if (la.kind == 1 || la.kind == 23) { + if (la.kind == 23) { Get(); u = true; } Ident(out parent); Parents.Add(new ConstantParent ( new IdentifierExpr(parent, parent.val), u)); - while (la.kind == 12) { + while (la.kind == 13) { Get(); u = false; - if (la.kind == 22) { + if (la.kind == 23) { Get(); u = true; } @@ -779,7 +781,7 @@ private class BvBounds : Expr { new IdentifierExpr(parent, parent.val), u)); } } - if (la.kind == 24) { + if (la.kind == 25) { Get(); ChildrenComplete = true; } @@ -792,12 +794,12 @@ private class BvBounds : Expr { IToken/*!*/ tok; kv = null; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Type(out ty); tok = ty.tok; - if (la.kind == 11) { + if (la.kind == 12) { Get(); var uti = ty as UnresolvedTypeIdentifier; if (uti != null && uti.Arguments.Count == 0) { @@ -823,7 +825,7 @@ private class BvBounds : Expr { if (la.kind == 1) { WhiteSpaceIdents(out paramTokens); } - if (la.kind == 31) { + if (la.kind == 32) { Get(); Type(out body); synonym = true; @@ -855,15 +857,15 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ 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 List<TypeVariable>(); outs = new List<Variable>(); kv = null; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Ident(out name); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out typeParamTok, out typeParams); } ProcFormals(true, allowWhereClausesOnFormals, out ins); - if (la.kind == 26) { + if (la.kind == 27) { Get(); ProcFormals(false, allowWhereClausesOnFormals, out outs); } @@ -871,7 +873,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { void Spec(List<Requires>/*!*/ pre, List<IdentifierExpr>/*!*/ mods, List<Ensures>/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms; - if (la.kind == 34) { + if (la.kind == 35) { Get(); if (la.kind == 1) { Idents(out ms); @@ -881,19 +883,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } } - Expect(8); - } else if (la.kind == 35) { + Expect(9); + } else if (la.kind == 36) { Get(); SpecPrePost(true, pre, post); - } else if (la.kind == 36 || la.kind == 37) { + } else if (la.kind == 37 || la.kind == 38) { SpecPrePost(false, pre, post); - } else SynErr(103); + } else SynErr(104); } void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new List<Variable>(); - Expect(27); - while (la.kind == 7) { + Expect(28); + while (la.kind == 8) { LocalVars(locals); } StmtList(out stmtList); @@ -901,25 +903,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; - if (la.kind == 36) { + if (la.kind == 37) { Get(); tok = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); - Expect(8); + Expect(9); pre.Add(new Requires(tok, free, e, null, kv)); - } else if (la.kind == 37) { + } else if (la.kind == 38) { Get(); tok = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); - Expect(8); + Expect(9); post.Add(new Ensures(tok, free, e, null, kv)); - } else SynErr(104); + } else SynErr(105); } void StmtList(out StmtList/*!*/ stmtList) { @@ -956,7 +958,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { cs = new List<Cmd>(); } - } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) { + } else if (la.kind == 41 || la.kind == 43 || la.kind == 46) { StructuredCmd(out ecn); ec = ecn; if (startToken == null) { startToken = ec.tok; cs = new List<Cmd>(); } @@ -976,7 +978,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } } - Expect(28); + Expect(29); IToken/*!*/ endCurly = t; if (startToken == null && bigblocks.Count == 0) { startToken = t; cs = new List<Cmd>(); @@ -1004,33 +1006,33 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { LabelOrAssign(out c, out label); break; } - case 46: { + case 47: { Get(); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); c = new AssertCmd(x, e, kv); - Expect(8); + Expect(9); break; } - case 47: { + case 48: { Get(); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } Proposition(out e); c = new AssumeCmd(x, e, kv); - Expect(8); + Expect(9); break; } - case 48: { + case 49: { Get(); x = t; Idents(out xs); - Expect(8); + Expect(9); ids = new List<IdentifierExpr>(); foreach(IToken/*!*/ y in xs){ Contract.Assert(y != null); @@ -1040,25 +1042,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { break; } - case 35: case 51: case 52: { + case 36: case 52: case 53: { CallCmd(out cn); - Expect(8); + Expect(9); c = cn; break; } - case 53: { + case 54: { ParCallCmd(out cn); c = cn; break; } - case 49: { + case 50: { Get(); x = t; - Expect(8); + Expect(9); c = new YieldCmd(x); break; } - default: SynErr(105); break; + default: SynErr(106); break; } } @@ -1066,16 +1068,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec)); IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd; - if (la.kind == 40) { + if (la.kind == 41) { IfCmd(out ifcmd); ec = ifcmd; - } else if (la.kind == 42) { + } else if (la.kind == 43) { WhileCmd(out wcmd); ec = wcmd; - } else if (la.kind == 45) { + } else if (la.kind == 46) { BreakCmd(out bcmd); ec = bcmd; - } else SynErr(106); + } else SynErr(107); } void TransferCmd(out TransferCmd/*!*/ tc) { @@ -1083,7 +1085,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Token y; List<IToken>/*!*/ xs; List<String> ss = new List<String>(); - if (la.kind == 38) { + if (la.kind == 39) { Get(); y = t; Idents(out xs); @@ -1092,11 +1094,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { ss.Add(s.val); } tc = new GotoCmd(y, ss); - } else if (la.kind == 39) { + } else if (la.kind == 40) { Get(); tc = new ReturnCmd(t); - } else SynErr(107); - Expect(8); + } else SynErr(108); + Expect(9); } void IfCmd(out IfCmd/*!*/ ifcmd) { @@ -1106,21 +1108,21 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { IfCmd/*!*/ elseIf; IfCmd elseIfOption = null; StmtList/*!*/ els; StmtList elseOption = null; - Expect(40); + Expect(41); x = t; Guard(out guard); - Expect(27); + Expect(28); StmtList(out thn); - if (la.kind == 41) { + if (la.kind == 42) { Get(); - if (la.kind == 40) { + if (la.kind == 41) { IfCmd(out elseIf); elseIfOption = elseIf; - } else if (la.kind == 27) { + } else if (la.kind == 28) { Get(); StmtList(out els); elseOption = els; - } else SynErr(108); + } else SynErr(109); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); } @@ -1132,18 +1134,18 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { StmtList/*!*/ body; QKeyValue kv = null; - Expect(42); + Expect(43); x = t; Guard(out guard); Contract.Assume(guard == null || cce.Owner.None(guard)); - while (la.kind == 35 || la.kind == 43) { + while (la.kind == 36 || la.kind == 44) { isFree = false; z = la/*lookahead token*/; - if (la.kind == 35) { + if (la.kind == 36) { Get(); isFree = true; } - Expect(43); - while (la.kind == 27) { + Expect(44); + while (la.kind == 28) { Attribute(ref kv); } Expression(out e); @@ -1154,9 +1156,9 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } kv = null; - Expect(8); + Expect(9); } - Expect(27); + Expect(28); StmtList(out body); wcmd = new WhileCmd(x, guard, invariants, body); } @@ -1165,27 +1167,27 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y; string breakLabel = null; - Expect(45); + Expect(46); x = t; if (la.kind == 1) { Ident(out y); breakLabel = y.val; } - Expect(8); + Expect(9); bcmd = new BreakCmd(x, breakLabel); } void Guard(out Expr e) { Expr/*!*/ ee; e = null; - Expect(9); - if (la.kind == 44) { + Expect(10); + if (la.kind == 45) { Get(); e = null; } else if (StartOf(9)) { Expression(out ee); e = ee; - } else SynErr(109); - Expect(10); + } else SynErr(110); + Expect(11); } void LabelOrAssign(out Cmd c, out IToken label) { @@ -1198,40 +1200,40 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Ident(out id); x = t; - if (la.kind == 11) { + if (la.kind == 12) { Get(); c = null; label = x; - } else if (la.kind == 12 || la.kind == 17 || la.kind == 50) { + } else if (la.kind == 13 || la.kind == 18 || la.kind == 51) { lhss = new List<AssignLhs/*!*/>(); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 17) { + while (la.kind == 18) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); } lhss.Add(lhs); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Ident(out id); lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); - while (la.kind == 17) { + while (la.kind == 18) { MapAssignIndex(out y, out indexes); lhs = new MapAssignLhs(y, lhs, indexes); } lhss.Add(lhs); } - Expect(50); + Expect(51); x = t; /* use location of := */ Expression(out e0); rhss = new List<Expr/*!*/> (); rhss.Add(e0); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e0); rhss.Add(e0); } - Expect(8); + Expect(9); c = new AssignCmd(x, lhss, rhss); - } else SynErr(110); + } else SynErr(111); } void CallCmd(out Cmd c) { @@ -1242,17 +1244,17 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { QKeyValue kv = null; c = null; - if (la.kind == 51) { + if (la.kind == 52) { Get(); isAsync = true; } - if (la.kind == 35) { + if (la.kind == 36) { Get(); isFree = true; } - Expect(52); + Expect(53); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } CallParams(isAsync, isFree, kv, x, out c); @@ -1266,19 +1268,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Cmd c = null; List<CallCmd> callCmds = new List<CallCmd>(); - Expect(53); + Expect(54); x = t; - while (la.kind == 27) { + while (la.kind == 28) { Attribute(ref kv); } CallParams(false, false, kv, x, out c); callCmds.Add((CallCmd)c); - while (la.kind == 54) { + while (la.kind == 55) { Get(); CallParams(false, false, kv, x, out c); callCmds.Add((CallCmd)c); } - Expect(8); + Expect(9); d = new ParCallCmd(x, callCmds, kv); } @@ -1286,18 +1288,18 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> (); Expr/*!*/ e; - Expect(17); + Expect(18); x = t; if (StartOf(9)) { Expression(out e); indexes.Add(e); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e); indexes.Add(e); } } - Expect(18); + Expect(19); } void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, out Cmd c) { @@ -1309,53 +1311,53 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { c = null; Ident(out first); - if (la.kind == 9) { + if (la.kind == 10) { Get(); if (StartOf(9)) { Expression(out en); es.Add(en); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out en); es.Add(en); } } - Expect(10); + Expect(11); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else if (la.kind == 12 || la.kind == 50) { + } else if (la.kind == 13 || la.kind == 51) { ids.Add(new IdentifierExpr(first, first.val)); - if (la.kind == 12) { + if (la.kind == 13) { Get(); Ident(out p); ids.Add(new IdentifierExpr(p, p.val)); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Ident(out p); ids.Add(new IdentifierExpr(p, p.val)); } } - Expect(50); + Expect(51); Ident(out first); - Expect(9); + Expect(10); if (StartOf(9)) { Expression(out en); es.Add(en); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out en); es.Add(en); } } - Expect(10); + Expect(11); c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else SynErr(111); + } else SynErr(112); } void Expressions(out List<Expr>/*!*/ es) { Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List<Expr>(); Expression(out e); es.Add(e); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e); es.Add(e); @@ -1366,7 +1368,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; LogicalExpression(out e0); if (StartOf(10)) { - if (la.kind == 57 || la.kind == 58) { + if (la.kind == 58 || la.kind == 59) { ImpliesOp(); x = t; ImpliesExpression(true, out e1); @@ -1378,7 +1380,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { x = t; LogicalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); - while (la.kind == 59 || la.kind == 60) { + while (la.kind == 60 || la.kind == 61) { ExpliesOp(); x = t; LogicalExpression(out e1); @@ -1389,23 +1391,23 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void EquivOp() { - if (la.kind == 55) { + if (la.kind == 56) { Get(); - } else if (la.kind == 56) { + } else if (la.kind == 57) { Get(); - } else SynErr(112); + } else SynErr(113); } void LogicalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; RelationalExpression(out e0); if (StartOf(11)) { - if (la.kind == 61 || la.kind == 62) { + if (la.kind == 62 || la.kind == 63) { AndOp(); x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); - while (la.kind == 61 || la.kind == 62) { + while (la.kind == 62 || la.kind == 63) { AndOp(); x = t; RelationalExpression(out e1); @@ -1416,7 +1418,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); - while (la.kind == 63 || la.kind == 64) { + while (la.kind == 64 || la.kind == 65) { OrOp(); x = t; RelationalExpression(out e1); @@ -1427,19 +1429,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void ImpliesOp() { - if (la.kind == 57) { + if (la.kind == 58) { Get(); - } else if (la.kind == 58) { + } else if (la.kind == 59) { Get(); - } else SynErr(113); + } else SynErr(114); } void ExpliesOp() { - if (la.kind == 59) { + if (la.kind == 60) { Get(); - } else if (la.kind == 60) { + } else if (la.kind == 61) { Get(); - } else SynErr(114); + } else SynErr(115); } void RelationalExpression(out Expr/*!*/ e0) { @@ -1453,25 +1455,25 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void AndOp() { - if (la.kind == 61) { + if (la.kind == 62) { Get(); - } else if (la.kind == 62) { + } else if (la.kind == 63) { Get(); - } else SynErr(115); + } else SynErr(116); } void OrOp() { - if (la.kind == 63) { + if (la.kind == 64) { Get(); - } else if (la.kind == 64) { + } else if (la.kind == 65) { Get(); - } else SynErr(116); + } else SynErr(117); } void BvTerm(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; Term(out e0); - while (la.kind == 73) { + while (la.kind == 74) { Get(); x = t; Term(out e1); @@ -1482,64 +1484,64 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ 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 65: { + case 66: { Get(); x = t; op=BinaryOperator.Opcode.Eq; break; } - case 19: { + case 20: { Get(); x = t; op=BinaryOperator.Opcode.Lt; break; } - case 20: { + case 21: { Get(); x = t; op=BinaryOperator.Opcode.Gt; break; } - case 66: { + case 67: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 67: { + case 68: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - case 68: { + case 69: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 69: { + case 70: { Get(); x = t; op=BinaryOperator.Opcode.Subtype; break; } - case 70: { + case 71: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 71: { + case 72: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 72: { + case 73: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - default: SynErr(117); break; + default: SynErr(118); 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 == 74 || la.kind == 75) { + while (la.kind == 75 || la.kind == 76) { AddOp(out x, out op); Factor(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -1558,19 +1560,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { 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 == 74) { + if (la.kind == 75) { Get(); x = t; op=BinaryOperator.Opcode.Add; - } else if (la.kind == 75) { + } else if (la.kind == 76) { Get(); x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(118); + } else SynErr(119); } void Power(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; UnaryExpression(out e0); - if (la.kind == 79) { + if (la.kind == 80) { Get(); x = t; Power(out e1); @@ -1580,46 +1582,46 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { 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 == 44) { + if (la.kind == 45) { Get(); x = t; op=BinaryOperator.Opcode.Mul; - } else if (la.kind == 76) { + } else if (la.kind == 77) { Get(); x = t; op=BinaryOperator.Opcode.Div; - } else if (la.kind == 77) { + } else if (la.kind == 78) { Get(); x = t; op=BinaryOperator.Opcode.Mod; - } else if (la.kind == 78) { + } else if (la.kind == 79) { Get(); x = t; op=BinaryOperator.Opcode.RealDiv; - } else SynErr(119); + } else SynErr(120); } void UnaryExpression(out Expr/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; - if (la.kind == 75) { + if (la.kind == 76) { Get(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); - } else if (la.kind == 80 || la.kind == 81) { + } else if (la.kind == 81 || la.kind == 82) { NegOp(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); } else if (StartOf(14)) { CoercionExpression(out e); - } else SynErr(120); + } else SynErr(121); } void NegOp() { - if (la.kind == 80) { + if (la.kind == 81) { Get(); - } else if (la.kind == 81) { + } else if (la.kind == 82) { Get(); - } else SynErr(121); + } else SynErr(122); } void CoercionExpression(out Expr/*!*/ e) { @@ -1628,7 +1630,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { BigNum bn; ArrayExpression(out e); - while (la.kind == 11) { + while (la.kind == 12) { Get(); x = t; if (StartOf(6)) { @@ -1643,7 +1645,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(122); + } else SynErr(123); } } @@ -1654,7 +1656,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { List<Expr>/*!*/ allArgs = dummyExprSeq; AtomExpression(out e); - while (la.kind == 17) { + while (la.kind == 18) { Get(); x = t; allArgs = new List<Expr> (); allArgs.Add(e); @@ -1667,7 +1669,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { else allArgs.Add(index0); - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -1675,7 +1677,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { allArgs.Add(e1); } - if (la.kind == 50) { + if (la.kind == 51) { Get(); Expression(out e1); if (bvExtract || e1 is BvBounds) @@ -1689,7 +1691,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { allArgs.Add(e1); store = true; } } - Expect(18); + Expect(19); if (store) e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs); else if (bvExtract) @@ -1714,7 +1716,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void AtomExpression(out Expr/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat bf; List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig; List<TypeVariable>/*!*/ typeParams; IdentifierExpr/*!*/ id; @@ -1724,12 +1726,12 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { List<Block/*!*/>/*!*/ blocks; switch (la.kind) { - case 82: { + case 83: { Get(); e = new LiteralExpr(t, false); break; } - case 83: { + case 84: { Get(); e = new LiteralExpr(t, true); break; @@ -1744,6 +1746,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new LiteralExpr(t, bd); break; } + case 7: { + Float(out bf); + e = new LiteralExpr(t, bf); + break; + } case 2: { BvLit(out bn, out n); e = new LiteralExpr(t, bn, n); @@ -1752,65 +1759,65 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { case 1: { Ident(out x); id = new IdentifierExpr(x, x.val); e = id; - if (la.kind == 9) { + if (la.kind == 10) { Get(); if (StartOf(9)) { Expressions(out es); e = new NAryExpr(x, new FunctionCall(id), es); - } else if (la.kind == 10) { + } else if (la.kind == 11) { e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); - } else SynErr(123); - Expect(10); + } else SynErr(124); + Expect(11); } break; } - case 84: { + case 85: { Get(); x = t; - Expect(9); - Expression(out e); Expect(10); + Expression(out e); + Expect(11); e = new OldExpr(x, e); break; } - case 14: { + case 15: { Get(); x = t; - Expect(9); - Expression(out e); Expect(10); + Expression(out e); + Expect(11); e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List<Expr>{ e }); break; } - case 15: { + case 16: { Get(); x = t; - Expect(9); - Expression(out e); Expect(10); + Expression(out e); + Expect(11); e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e }); break; } - case 9: { + case 10: { Get(); if (StartOf(9)) { Expression(out e); if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + "are not allowed"); - } else if (la.kind == 88 || la.kind == 89) { + } else if (la.kind == 89 || la.kind == 90) { Forall(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ForallExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 90 || la.kind == 91) { + } else if (la.kind == 91 || la.kind == 92) { Exists(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ExistsExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 92 || la.kind == 93) { + } else if (la.kind == 93 || la.kind == 94) { Lambda(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); @@ -1818,20 +1825,20 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { SemErr("triggers not allowed in lambda expressions"); if (typeParams.Count + ds.Count > 0) e = new LambdaExpr(x, typeParams, ds, kv, e); - } else SynErr(124); - Expect(10); + } else SynErr(125); + Expect(11); break; } - case 40: { + case 41: { IfThenElseExpression(out e); break; } - case 85: { + case 86: { CodeExpression(out locals, out blocks); e = new CodeExpr(locals, blocks); break; } - default: SynErr(125); break; + default: SynErr(126); break; } } @@ -1843,7 +1850,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 6) { Get(); s = t.val; - } else SynErr(126); + } else SynErr(127); try { n = BigDec.FromString(s); } catch (FormatException) { @@ -1853,6 +1860,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } + void Float(out BigFloat n) { + string s = ""; + Expect(7); + s = t.val; + try { + n = BigFloat.FromString(s); + } catch (FormatException e) { + this.SemErr("incorrectly formatted floating point, " + e.Message); + n = BigFloat.ZERO; + } + + } + void BvLit(out BigNum n, out int m) { Expect(2); int pos = t.val.IndexOf("bv"); @@ -1870,11 +1890,11 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void Forall() { - if (la.kind == 88) { + if (la.kind == 89) { Get(); - } else if (la.kind == 89) { + } else if (la.kind == 90) { Get(); - } else SynErr(127); + } else SynErr(128); } void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds, @@ -1885,35 +1905,35 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { kv = null; ds = new List<Variable> (); - if (la.kind == 19) { + if (la.kind == 20) { TypeParams(out tok, out typeParams); - if (la.kind == 1 || la.kind == 27) { + if (la.kind == 1 || la.kind == 28) { BoundVars(q, out ds); } - } else if (la.kind == 1 || la.kind == 27) { + } else if (la.kind == 1 || la.kind == 28) { BoundVars(q, out ds); - } else SynErr(128); + } else SynErr(129); QSep(); - while (la.kind == 27) { + while (la.kind == 28) { AttributeOrTrigger(ref kv, ref trig); } Expression(out body); } void Exists() { - if (la.kind == 90) { + if (la.kind == 91) { Get(); - } else if (la.kind == 91) { + } else if (la.kind == 92) { Get(); - } else SynErr(129); + } else SynErr(130); } void Lambda() { - if (la.kind == 92) { + if (la.kind == 93) { Get(); - } else if (la.kind == 93) { + } else if (la.kind == 94) { Get(); - } else SynErr(130); + } else SynErr(131); } void IfThenElseExpression(out Expr/*!*/ e) { @@ -1921,12 +1941,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { IToken/*!*/ tok; Expr/*!*/ e0, e1, e2; e = dummyExpr; - Expect(40); + Expect(41); tok = t; Expression(out e0); - Expect(87); + Expect(88); Expression(out e1); - Expect(41); + Expect(42); Expression(out e2); e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 }); } @@ -1935,8 +1955,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 List<Variable>(); Block/*!*/ b; blocks = new List<Block/*!*/>(); - Expect(85); - while (la.kind == 7) { + Expect(86); + while (la.kind == 8) { LocalVars(locals); } SpecBlock(out b); @@ -1945,7 +1965,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { SpecBlock(out b); blocks.Add(b); } - Expect(86); + Expect(87); } void SpecBlock(out Block/*!*/ b) { @@ -1958,7 +1978,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Expr/*!*/ e; Ident(out x); - Expect(11); + Expect(12); while (StartOf(8)) { LabelOrCmd(out c, out label); if (c != null) { @@ -1970,7 +1990,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } } - if (la.kind == 38) { + if (la.kind == 39) { Get(); y = t; Idents(out xs); @@ -1979,12 +1999,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 == 39) { + } else if (la.kind == 40) { Get(); Expression(out e); b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); - } else SynErr(131); - Expect(8); + } else SynErr(132); + Expect(9); } void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { @@ -1992,16 +2012,16 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { string key; List<object/*!*/> parameters; object/*!*/ param; - Expect(27); + Expect(28); tok = t; - if (la.kind == 11) { + if (la.kind == 12) { Get(); Expect(1); key = t.val; parameters = new List<object/*!*/>(); if (StartOf(16)) { AttributeParameter(out param); parameters.Add(param); - while (la.kind == 12) { + while (la.kind == 13) { Get(); AttributeParameter(out param); parameters.Add(param); @@ -2029,7 +2049,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } else if (StartOf(9)) { Expression(out e); es = new List<Expr> { e }; - while (la.kind == 12) { + while (la.kind == 13) { Get(); Expression(out e); es.Add(e); @@ -2040,8 +2060,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else SynErr(132); - Expect(28); + } else SynErr(133); + Expect(29); } void AttributeParameter(out object/*!*/ o) { @@ -2055,15 +2075,15 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } else if (StartOf(9)) { Expression(out e); o = e; - } else SynErr(133); + } else SynErr(134); } void QSep() { - if (la.kind == 94) { + if (la.kind == 95) { Get(); - } else if (la.kind == 95) { + } else if (la.kind == 96) { Get(); - } else SynErr(134); + } else SynErr(135); } @@ -2079,23 +2099,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, 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,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,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,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,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,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,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,T,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,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,T,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,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,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,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,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,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,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,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,T,T,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, 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,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,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, T,T,T,T, T,T,x,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, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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, x,x,x}, + {x,T,x,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, 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,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, 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,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, x,x,x}, + {x,T,x,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,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, T,x,x,T, T,T,x,T, x,x,T,T, T,T,T,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,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, T,x,x,x, x,x,x,x, x,x,x,T, T,T,T,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,T,T,T, x,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,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,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,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, 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,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,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,T,T, 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,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, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,T,T, x,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,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,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x}, + {x,T,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,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} }; } // end Parser @@ -2126,135 +2146,136 @@ public class Errors { case 3: s = "digits expected"; break; case 4: s = "string expected"; 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 = "\"yield\" expected"; break; - case 50: s = "\":=\" expected"; break; - case 51: s = "\"async\" expected"; break; - case 52: s = "\"call\" expected"; break; - case 53: s = "\"par\" expected"; break; - case 54: s = "\"|\" expected"; break; - case 55: s = "\"<==>\" expected"; break; - case 56: s = "\"\\u21d4\" expected"; break; - case 57: s = "\"==>\" expected"; break; - case 58: s = "\"\\u21d2\" expected"; break; - case 59: s = "\"<==\" expected"; break; - case 60: s = "\"\\u21d0\" expected"; break; - case 61: s = "\"&&\" expected"; break; - case 62: s = "\"\\u2227\" expected"; break; - case 63: s = "\"||\" expected"; break; - case 64: s = "\"\\u2228\" expected"; break; - case 65: s = "\"==\" expected"; break; - case 66: s = "\"<=\" expected"; break; - case 67: s = "\">=\" expected"; break; - case 68: s = "\"!=\" expected"; break; - case 69: s = "\"<:\" expected"; break; - case 70: s = "\"\\u2260\" expected"; break; - case 71: s = "\"\\u2264\" expected"; break; - case 72: s = "\"\\u2265\" expected"; break; - case 73: s = "\"++\" expected"; break; - case 74: s = "\"+\" expected"; break; - case 75: s = "\"-\" expected"; break; - case 76: s = "\"div\" expected"; break; - case 77: s = "\"mod\" expected"; break; - case 78: s = "\"/\" expected"; break; - case 79: s = "\"**\" expected"; break; - case 80: s = "\"!\" expected"; break; - case 81: s = "\"\\u00ac\" expected"; break; - case 82: s = "\"false\" expected"; break; - case 83: s = "\"true\" expected"; break; - case 84: s = "\"old\" expected"; break; - case 85: s = "\"|{\" expected"; break; - case 86: s = "\"}|\" expected"; break; - case 87: s = "\"then\" expected"; break; - case 88: s = "\"forall\" expected"; break; - case 89: s = "\"\\u2200\" expected"; break; - case 90: s = "\"exists\" expected"; break; - case 91: s = "\"\\u2203\" expected"; break; - case 92: s = "\"lambda\" expected"; break; - case 93: s = "\"\\u03bb\" expected"; break; - case 94: s = "\"::\" expected"; break; - case 95: s = "\"\\u2022\" expected"; break; - case 96: s = "??? expected"; break; - case 97: s = "invalid Function"; break; + case 6: s = "dec_float expected"; break; + case 7: s = "float expected"; break; + case 8: s = "\"var\" 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 = "\",\" expected"; break; + case 14: s = "\"where\" expected"; break; + case 15: s = "\"int\" expected"; break; + case 16: s = "\"real\" expected"; break; + case 17: s = "\"bool\" expected"; break; + case 18: s = "\"[\" expected"; break; + case 19: s = "\"]\" expected"; break; + case 20: s = "\"<\" expected"; break; + case 21: s = "\">\" expected"; break; + case 22: s = "\"const\" expected"; break; + case 23: s = "\"unique\" expected"; break; + case 24: s = "\"extends\" expected"; break; + case 25: s = "\"complete\" expected"; break; + case 26: s = "\"function\" expected"; break; + case 27: s = "\"returns\" expected"; break; + case 28: s = "\"{\" expected"; break; + case 29: s = "\"}\" expected"; break; + case 30: s = "\"axiom\" expected"; break; + case 31: s = "\"type\" expected"; break; + case 32: s = "\"=\" expected"; break; + case 33: s = "\"procedure\" expected"; break; + case 34: s = "\"implementation\" expected"; break; + case 35: s = "\"modifies\" expected"; break; + case 36: s = "\"free\" expected"; break; + case 37: s = "\"requires\" expected"; break; + case 38: s = "\"ensures\" expected"; break; + case 39: s = "\"goto\" expected"; break; + case 40: s = "\"return\" expected"; break; + case 41: s = "\"if\" expected"; break; + case 42: s = "\"else\" expected"; break; + case 43: s = "\"while\" expected"; break; + case 44: s = "\"invariant\" expected"; break; + case 45: s = "\"*\" expected"; break; + case 46: s = "\"break\" expected"; break; + case 47: s = "\"assert\" expected"; break; + case 48: s = "\"assume\" expected"; break; + case 49: s = "\"havoc\" expected"; break; + case 50: s = "\"yield\" expected"; break; + case 51: s = "\":=\" expected"; break; + case 52: s = "\"async\" expected"; break; + case 53: s = "\"call\" expected"; break; + case 54: s = "\"par\" expected"; break; + case 55: s = "\"|\" expected"; break; + case 56: s = "\"<==>\" expected"; break; + case 57: s = "\"\\u21d4\" expected"; break; + case 58: s = "\"==>\" expected"; break; + case 59: s = "\"\\u21d2\" expected"; break; + case 60: s = "\"<==\" expected"; break; + case 61: s = "\"\\u21d0\" expected"; break; + case 62: s = "\"&&\" expected"; break; + case 63: s = "\"\\u2227\" expected"; break; + case 64: s = "\"||\" expected"; break; + case 65: s = "\"\\u2228\" expected"; break; + case 66: s = "\"==\" expected"; break; + case 67: s = "\"<=\" expected"; break; + case 68: s = "\">=\" expected"; break; + case 69: s = "\"!=\" expected"; break; + case 70: s = "\"<:\" expected"; break; + case 71: s = "\"\\u2260\" expected"; break; + case 72: s = "\"\\u2264\" expected"; break; + case 73: s = "\"\\u2265\" expected"; break; + case 74: s = "\"++\" expected"; break; + case 75: s = "\"+\" expected"; break; + case 76: s = "\"-\" expected"; break; + case 77: s = "\"div\" expected"; break; + case 78: s = "\"mod\" expected"; break; + case 79: s = "\"/\" expected"; break; + case 80: s = "\"**\" expected"; break; + case 81: s = "\"!\" expected"; break; + case 82: s = "\"\\u00ac\" expected"; break; + case 83: s = "\"false\" expected"; break; + case 84: s = "\"true\" expected"; break; + case 85: s = "\"old\" expected"; break; + case 86: s = "\"|{\" expected"; break; + case 87: s = "\"}|\" expected"; break; + case 88: s = "\"then\" expected"; break; + case 89: s = "\"forall\" expected"; break; + case 90: s = "\"\\u2200\" expected"; break; + case 91: s = "\"exists\" expected"; break; + case 92: s = "\"\\u2203\" expected"; break; + case 93: s = "\"lambda\" expected"; break; + case 94: s = "\"\\u03bb\" expected"; break; + case 95: s = "\"::\" expected"; break; + case 96: s = "\"\\u2022\" expected"; break; + case 97: s = "??? expected"; break; case 98: s = "invalid Function"; break; - case 99: s = "invalid Procedure"; break; - case 100: s = "invalid Type"; break; - case 101: s = "invalid TypeAtom"; break; - case 102: s = "invalid TypeArgs"; break; - case 103: s = "invalid Spec"; break; - case 104: s = "invalid SpecPrePost"; break; - case 105: s = "invalid LabelOrCmd"; break; - case 106: s = "invalid StructuredCmd"; break; - case 107: s = "invalid TransferCmd"; break; - case 108: s = "invalid IfCmd"; break; - case 109: s = "invalid Guard"; break; - case 110: s = "invalid LabelOrAssign"; break; - case 111: s = "invalid CallParams"; break; - case 112: s = "invalid EquivOp"; break; - case 113: s = "invalid ImpliesOp"; break; - case 114: s = "invalid ExpliesOp"; break; - case 115: s = "invalid AndOp"; break; - case 116: s = "invalid OrOp"; break; - case 117: s = "invalid RelOp"; break; - case 118: s = "invalid AddOp"; break; - case 119: s = "invalid MulOp"; break; - case 120: s = "invalid UnaryExpression"; break; - case 121: s = "invalid NegOp"; break; - case 122: s = "invalid CoercionExpression"; break; - case 123: s = "invalid AtomExpression"; break; + case 99: s = "invalid Function"; break; + case 100: s = "invalid Procedure"; break; + case 101: s = "invalid Type"; break; + case 102: s = "invalid TypeAtom"; break; + case 103: s = "invalid TypeArgs"; break; + case 104: s = "invalid Spec"; break; + case 105: s = "invalid SpecPrePost"; break; + case 106: s = "invalid LabelOrCmd"; break; + case 107: s = "invalid StructuredCmd"; break; + case 108: s = "invalid TransferCmd"; break; + case 109: s = "invalid IfCmd"; break; + case 110: s = "invalid Guard"; break; + case 111: s = "invalid LabelOrAssign"; break; + case 112: s = "invalid CallParams"; break; + case 113: s = "invalid EquivOp"; break; + case 114: s = "invalid ImpliesOp"; break; + case 115: s = "invalid ExpliesOp"; break; + case 116: s = "invalid AndOp"; break; + case 117: s = "invalid OrOp"; break; + case 118: s = "invalid RelOp"; break; + case 119: s = "invalid AddOp"; break; + case 120: s = "invalid MulOp"; break; + case 121: s = "invalid UnaryExpression"; break; + case 122: s = "invalid NegOp"; break; + case 123: s = "invalid CoercionExpression"; break; case 124: s = "invalid AtomExpression"; break; case 125: s = "invalid AtomExpression"; break; - case 126: s = "invalid Dec"; break; - case 127: s = "invalid Forall"; break; - case 128: s = "invalid QuantifierBody"; break; - case 129: s = "invalid Exists"; break; - case 130: s = "invalid Lambda"; break; - case 131: s = "invalid SpecBlock"; break; - case 132: s = "invalid AttributeOrTrigger"; break; - case 133: s = "invalid AttributeParameter"; break; - case 134: s = "invalid QSep"; break; + case 126: s = "invalid AtomExpression"; break; + case 127: s = "invalid Dec"; break; + case 128: s = "invalid Forall"; break; + case 129: s = "invalid QuantifierBody"; break; + case 130: s = "invalid Exists"; break; + case 131: s = "invalid Lambda"; break; + case 132: s = "invalid SpecBlock"; break; + case 133: s = "invalid AttributeOrTrigger"; break; + case 134: s = "invalid AttributeParameter"; break; + case 135: s = "invalid QSep"; break; default: s = "error " + n; break; } diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index e068fc4b..46a3c419 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 = 96; - const int noSym = 96; + const int maxT = 97; + const int noSym = 97; [ContractInvariantMethod] @@ -267,41 +267,42 @@ 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] = 16; + for (int i = 49; i <= 57; ++i) start[i] = 45; for (int i = 34; i <= 34; ++i) start[i] = 6; start[92] = 1; - 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[124] = 61; - start[8660] = 28; - start[8658] = 30; - start[8656] = 31; - start[38] = 32; - start[8743] = 34; - 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[45] = 87; + start[48] = 46; + start[59] = 52; + start[40] = 53; + start[41] = 54; + start[58] = 88; + start[44] = 55; + start[91] = 56; + start[93] = 57; + start[60] = 89; + start[62] = 90; + start[123] = 58; + start[125] = 91; + start[61] = 92; + start[42] = 93; + start[124] = 94; + start[8660] = 61; + start[8658] = 63; + start[8656] = 64; + start[38] = 65; + start[8743] = 67; + start[8744] = 69; + start[33] = 95; + start[8800] = 73; + start[8804] = 74; + start[8805] = 75; + start[43] = 96; + start[47] = 77; + start[172] = 79; + start[8704] = 82; + start[8707] = 83; + start[955] = 84; + start[8226] = 86; start[Buffer.EOF] = -1; } @@ -503,48 +504,48 @@ public class Scanner { void CheckLiteral() { switch (t.val) { - 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 "yield": t.kind = 49; break; - case "async": t.kind = 51; break; - case "call": t.kind = 52; break; - case "par": t.kind = 53; break; - case "div": t.kind = 76; break; - case "mod": t.kind = 77; break; - case "false": t.kind = 82; break; - case "true": t.kind = 83; break; - case "old": t.kind = 84; break; - case "then": t.kind = 87; break; - case "forall": t.kind = 88; break; - case "exists": t.kind = 90; break; - case "lambda": t.kind = 92; break; + case "var": t.kind = 8; break; + case "where": t.kind = 14; break; + case "int": t.kind = 15; break; + case "real": t.kind = 16; break; + case "bool": t.kind = 17; break; + case "const": t.kind = 22; break; + case "unique": t.kind = 23; break; + case "extends": t.kind = 24; break; + case "complete": t.kind = 25; break; + case "function": t.kind = 26; break; + case "returns": t.kind = 27; break; + case "axiom": t.kind = 30; break; + case "type": t.kind = 31; break; + case "procedure": t.kind = 33; break; + case "implementation": t.kind = 34; break; + case "modifies": t.kind = 35; break; + case "free": t.kind = 36; break; + case "requires": t.kind = 37; break; + case "ensures": t.kind = 38; break; + case "goto": t.kind = 39; break; + case "return": t.kind = 40; break; + case "if": t.kind = 41; break; + case "else": t.kind = 42; break; + case "while": t.kind = 43; break; + case "invariant": t.kind = 44; break; + case "break": t.kind = 46; break; + case "assert": t.kind = 47; break; + case "assume": t.kind = 48; break; + case "havoc": t.kind = 49; break; + case "yield": t.kind = 50; break; + case "async": t.kind = 52; break; + case "call": t.kind = 53; break; + case "par": t.kind = 54; break; + case "div": t.kind = 77; break; + case "mod": t.kind = 78; break; + case "false": t.kind = 83; break; + case "true": t.kind = 84; break; + case "old": t.kind = 85; break; + case "then": t.kind = 88; break; + case "forall": t.kind = 89; break; + case "exists": t.kind = 91; break; + case "lambda": t.kind = 93; break; default: break; } } @@ -597,182 +598,305 @@ 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 17;} + else if (ch == 92) {AddCh(); goto case 47;} 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;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;} else {goto case 0;} case 9: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} - else {goto case 0;} + recEnd = pos; recKind = 6; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;} + else if (ch == 'e') {AddCh(); goto case 10;} + else {t.kind = 6; break;} case 10: - recEnd = pos; recKind = 5; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} - else {t.kind = 5; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} + else if (ch == '-') {AddCh(); goto case 11;} + else {goto case 0;} 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;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;} + else if (ch == 'e') {AddCh(); goto case 14;} else {goto case 0;} case 14: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;} + else if (ch == '-') {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;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;} + else {goto case 0;} case 16: - recEnd = pos; recKind = 3; if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;} - else if (ch == 'b') {AddCh(); goto case 3;} - else if (ch == 'e') {AddCh(); goto case 8;} - else if (ch == '.') {AddCh(); goto case 11;} - else {t.kind = 3; break;} + else if (ch == 'f') {AddCh(); goto case 17;} + else {goto case 0;} 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 17;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;} else {goto case 0;} 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 17;} - else {t.kind = 4; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;} + else if (ch == 'e') {AddCh(); goto case 19;} + else {goto case 0;} case 19: - {t.kind = 8; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;} + else {goto case 0;} case 20: - {t.kind = 9; break;} + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;} + else {t.kind = 7; break;} case 21: - {t.kind = 10; break;} + if (ch == 'a') {AddCh(); goto case 22;} + else {goto case 0;} case 22: - {t.kind = 12; break;} + if (ch == 'N') {AddCh(); goto case 23;} + else {goto case 0;} case 23: - {t.kind = 17; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;} + else {goto case 0;} case 24: - {t.kind = 18; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;} + else if (ch == 'e') {AddCh(); goto case 25;} + else {goto case 0;} case 25: - {t.kind = 27; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 26;} + else {goto case 0;} case 26: - {t.kind = 50; break;} + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 26;} + else {t.kind = 7; break;} case 27: - {t.kind = 55; break;} + if (ch == 'a') {AddCh(); goto case 28;} + else {goto case 0;} case 28: - {t.kind = 56; break;} + if (ch == 'n') {AddCh(); goto case 29;} + else {goto case 0;} case 29: - {t.kind = 57; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;} + else {goto case 0;} case 30: - {t.kind = 58; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;} + else if (ch == 'e') {AddCh(); goto case 31;} + else {goto case 0;} case 31: - {t.kind = 60; break;} - case 32: - if (ch == '&') {AddCh(); goto case 33;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;} else {goto case 0;} + case 32: + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;} + else {t.kind = 7; break;} case 33: - {t.kind = 61; break;} + if (ch == 'o') {AddCh(); goto case 34;} + else {goto case 0;} case 34: - {t.kind = 62; break;} + if (ch == 'o') {AddCh(); goto case 35;} + else {goto case 0;} case 35: - {t.kind = 63; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;} + else {goto case 0;} case 36: - {t.kind = 64; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;} + else if (ch == 'e') {AddCh(); goto case 37;} + else {goto case 0;} case 37: - {t.kind = 67; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;} + else {goto case 0;} case 38: - {t.kind = 68; break;} + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;} + else {t.kind = 7; break;} case 39: - {t.kind = 69; break;} + if (ch == 'o') {AddCh(); goto case 40;} + else {goto case 0;} case 40: - {t.kind = 70; break;} + if (ch == 'o') {AddCh(); goto case 41;} + else {goto case 0;} case 41: - {t.kind = 71; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;} + else {goto case 0;} case 42: - {t.kind = 72; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;} + else if (ch == 'e') {AddCh(); goto case 43;} + else {goto case 0;} case 43: - {t.kind = 73; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;} + else {goto case 0;} case 44: - {t.kind = 75; break;} + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;} + else {t.kind = 7; break;} case 45: - {t.kind = 78; break;} + recEnd = pos; recKind = 3; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 45;} + else if (ch == 'b') {AddCh(); goto case 3;} + else if (ch == 'e') {AddCh(); goto case 48;} + else if (ch == '.') {AddCh(); goto case 8;} + else {t.kind = 3; break;} case 46: - {t.kind = 79; break;} + recEnd = pos; recKind = 3; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 45;} + else if (ch == 'b') {AddCh(); goto case 3;} + else if (ch == 'e') {AddCh(); goto case 48;} + else if (ch == '.') {AddCh(); goto case 8;} + else if (ch == 'N') {AddCh(); goto case 21;} + else if (ch == 'n') {AddCh(); goto case 27;} + else if (ch == '+') {AddCh(); goto case 33;} + else if (ch == '-') {AddCh(); goto case 39;} + else {t.kind = 3; break;} case 47: - {t.kind = 81; break;} + if (ch == '"') {AddCh(); goto case 49;} + 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 47;} + else {goto case 0;} case 48: - {t.kind = 85; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;} + else if (ch == '-') {AddCh(); goto case 51;} + else {goto case 0;} case 49: - {t.kind = 86; break;} + 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 47;} + else {t.kind = 4; break;} case 50: - {t.kind = 89; break;} + recEnd = pos; recKind = 5; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;} + else if (ch == 'f') {AddCh(); goto case 17;} + else {t.kind = 5; break;} case 51: - {t.kind = 91; break;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;} + else {goto case 0;} case 52: - {t.kind = 93; break;} + {t.kind = 9; break;} case 53: - {t.kind = 94; break;} + {t.kind = 10; break;} case 54: - {t.kind = 95; break;} + {t.kind = 11; break;} case 55: - recEnd = pos; recKind = 11; - if (ch == '=') {AddCh(); goto case 26;} - else if (ch == ':') {AddCh(); goto case 53;} - else {t.kind = 11; break;} + {t.kind = 13; break;} case 56: - recEnd = pos; recKind = 19; - if (ch == '=') {AddCh(); goto case 64;} - else if (ch == ':') {AddCh(); goto case 39;} - else {t.kind = 19; break;} + {t.kind = 18; break;} case 57: - recEnd = pos; recKind = 20; - if (ch == '=') {AddCh(); goto case 37;} - else {t.kind = 20; break;} + {t.kind = 19; break;} case 58: - recEnd = pos; recKind = 28; - if (ch == '|') {AddCh(); goto case 49;} - else {t.kind = 28; break;} + {t.kind = 28; break;} case 59: - recEnd = pos; recKind = 31; - if (ch == '=') {AddCh(); goto case 65;} - else {t.kind = 31; break;} + {t.kind = 51; break;} case 60: - recEnd = pos; recKind = 44; - if (ch == '*') {AddCh(); goto case 46;} - else {t.kind = 44; break;} + {t.kind = 56; break;} case 61: - recEnd = pos; recKind = 54; - if (ch == '|') {AddCh(); goto case 35;} - else if (ch == '{') {AddCh(); goto case 48;} - else {t.kind = 54; break;} + {t.kind = 57; break;} case 62: - recEnd = pos; recKind = 80; - if (ch == '=') {AddCh(); goto case 38;} - else {t.kind = 80; break;} + {t.kind = 58; break;} case 63: - recEnd = pos; recKind = 74; - if (ch == '+') {AddCh(); goto case 43;} - else {t.kind = 74; break;} + {t.kind = 59; break;} case 64: - recEnd = pos; recKind = 66; - if (ch == '=') {AddCh(); goto case 66;} - else {t.kind = 66; break;} + {t.kind = 61; break;} case 65: - recEnd = pos; recKind = 65; - if (ch == '>') {AddCh(); goto case 29;} - else {t.kind = 65; break;} + if (ch == '&') {AddCh(); goto case 66;} + else {goto case 0;} case 66: - recEnd = pos; recKind = 59; - if (ch == '>') {AddCh(); goto case 27;} - else {t.kind = 59; break;} + {t.kind = 62; break;} + case 67: + {t.kind = 63; break;} + case 68: + {t.kind = 64; break;} + case 69: + {t.kind = 65; break;} + case 70: + {t.kind = 68; break;} + case 71: + {t.kind = 69; break;} + case 72: + {t.kind = 70; break;} + case 73: + {t.kind = 71; break;} + case 74: + {t.kind = 72; break;} + case 75: + {t.kind = 73; break;} + case 76: + {t.kind = 74; break;} + case 77: + {t.kind = 79; break;} + case 78: + {t.kind = 80; break;} + case 79: + {t.kind = 82; break;} + case 80: + {t.kind = 86; break;} + case 81: + {t.kind = 87; break;} + case 82: + {t.kind = 90; break;} + case 83: + {t.kind = 92; break;} + case 84: + {t.kind = 94; break;} + case 85: + {t.kind = 95; break;} + case 86: + {t.kind = 96; break;} + case 87: + recEnd = pos; recKind = 76; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;} + else {t.kind = 76; break;} + case 88: + recEnd = pos; recKind = 12; + if (ch == '=') {AddCh(); goto case 59;} + else if (ch == ':') {AddCh(); goto case 85;} + else {t.kind = 12; break;} + case 89: + recEnd = pos; recKind = 20; + if (ch == '=') {AddCh(); goto case 97;} + else if (ch == ':') {AddCh(); goto case 72;} + else {t.kind = 20; break;} + case 90: + recEnd = pos; recKind = 21; + if (ch == '=') {AddCh(); goto case 70;} + else {t.kind = 21; break;} + case 91: + recEnd = pos; recKind = 29; + if (ch == '|') {AddCh(); goto case 81;} + else {t.kind = 29; break;} + case 92: + recEnd = pos; recKind = 32; + if (ch == '=') {AddCh(); goto case 98;} + else {t.kind = 32; break;} + case 93: + recEnd = pos; recKind = 45; + if (ch == '*') {AddCh(); goto case 78;} + else {t.kind = 45; break;} + case 94: + recEnd = pos; recKind = 55; + if (ch == '|') {AddCh(); goto case 68;} + else if (ch == '{') {AddCh(); goto case 80;} + else {t.kind = 55; break;} + case 95: + recEnd = pos; recKind = 81; + if (ch == '=') {AddCh(); goto case 71;} + else {t.kind = 81; break;} + case 96: + recEnd = pos; recKind = 75; + if (ch == '+') {AddCh(); goto case 76;} + else {t.kind = 75; break;} + case 97: + recEnd = pos; recKind = 67; + if (ch == '=') {AddCh(); goto case 99;} + else {t.kind = 67; break;} + case 98: + recEnd = pos; recKind = 66; + if (ch == '>') {AddCh(); goto case 62;} + else {t.kind = 66; break;} + case 99: + recEnd = pos; recKind = 60; + if (ch == '>') {AddCh(); goto case 60;} + else {t.kind = 60; break;} } t.val = new String(tval, 0, tlen); diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index c845a589..c3d8a672 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -103,6 +103,12 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Type>() != null); return this.VisitType(node); } + public virtual Type VisitFloatType(FloatType node) + { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result<Type>() != null); + return this.VisitType(node); + } public virtual Expr VisitBvConcatExpr(BvConcatExpr node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result<Expr>() != null); diff --git a/Source/Doomed/Doomed.csproj b/Source/Doomed/Doomed.csproj index c8fb83ad..f055d2c9 100644 --- a/Source/Doomed/Doomed.csproj +++ b/Source/Doomed/Doomed.csproj @@ -8,7 +8,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>Doomed</RootNamespace> - <AssemblyName>Doomed</AssemblyName> + <AssemblyName>BoogieDoomed</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 9bc855be..5a22cc15 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -443,6 +443,8 @@ namespace Microsoft.Boogie static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>(); + static ThreadTaskScheduler Scheduler = new ThreadTaskScheduler(16 * 1024 * 1024); + public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots = true, string programId = null) { Contract.Requires(cce.NonNullElements(fileNames)); @@ -977,7 +979,7 @@ namespace Microsoft.Boogie { break; } - tasks[j].Start(TaskScheduler.Default); + tasks[j].Start(Scheduler); } // Don't wait for tasks that haven't been started yet. diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj index b0f77125..c715a631 100644 --- a/Source/ExecutionEngine/ExecutionEngine.csproj +++ b/Source/ExecutionEngine/ExecutionEngine.csproj @@ -8,7 +8,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>ExecutionEngine</RootNamespace> - <AssemblyName>ExecutionEngine</AssemblyName> + <AssemblyName>BoogieExecutionEngine</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'"> @@ -131,6 +131,7 @@ <ItemGroup> <Compile Include="ExecutionEngine.cs" /> <Compile Include="Properties\AssemblyInfo.cs" /> + <Compile Include="ThreadTaskScheduler.cs" /> <Compile Include="VerificationResultCache.cs" /> </ItemGroup> <ItemGroup> diff --git a/Source/ExecutionEngine/ThreadTaskScheduler.cs b/Source/ExecutionEngine/ThreadTaskScheduler.cs new file mode 100644 index 00000000..58c4c6d4 --- /dev/null +++ b/Source/ExecutionEngine/ThreadTaskScheduler.cs @@ -0,0 +1,58 @@ +using System; +using System.Collections.Generic; +using System.Collections.Concurrent; +using System.Diagnostics.Contracts; +using System.Linq; +using System.Text; +using System.Threading; +using System.Threading.Tasks; + +namespace Microsoft.Boogie +{ + // Implementation of System.Threading.Tasks.TaskScheduler which creates a unique thread per + // task, and allows each thread to have its own custom stack size. The standard + // scheduler uses the .NET threadpool, which in turn inherits stack size from the EXE. + public class ThreadTaskScheduler : TaskScheduler + { + private int stackSize; + + public ThreadTaskScheduler(int StackReserveSize) + { + Contract.Requires(StackReserveSize >= 0); + + stackSize = StackReserveSize; + } + + protected override IEnumerable<Task> GetScheduledTasks() + { + // There is never a queue of scheduled, but not running, tasks. + // So return an empty list. + return new List<Task>(); + } + + protected override void QueueTask(Task task) + { + // Each queued task runs on a newly-created thread with the required + // stack size. The default .NET task scheduler is built on the .NET + // ThreadPool. Its policy allows it to create thousands of threads + // if it chooses. + // + // Boogie creates tasks which in turn create tasks and wait on them. + // So throttling tasks via a queue risks deadlock. + + Thread th = new Thread(TaskMain, stackSize); + th.Start(task); + } + + protected override bool TryExecuteTaskInline(Task task, bool taskWasPreviouslyQueued) + { + return false; + } + + private void TaskMain(object data) + { + Task t = (Task)data; + TryExecuteTask(t); + } + } +} diff --git a/Source/Graph/Graph.csproj b/Source/Graph/Graph.csproj index 66759719..7e610d46 100644 --- a/Source/Graph/Graph.csproj +++ b/Source/Graph/Graph.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <PropertyGroup> <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> @@ -9,7 +9,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>Graph</RootNamespace> - <AssemblyName>Graph</AssemblyName> + <AssemblyName>BoogieGraph</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> @@ -34,7 +34,7 @@ <IsWebBootstrapper>false</IsWebBootstrapper> <UseApplicationTrust>false</UseApplicationTrust> <BootstrapperEnabled>true</BootstrapperEnabled> - <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> </PropertyGroup> <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> <DebugSymbols>true</DebugSymbols> @@ -196,4 +196,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project> +</Project>
\ No newline at end of file diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj index 68ea62e3..43612142 100644 --- a/Source/Houdini/Houdini.csproj +++ b/Source/Houdini/Houdini.csproj @@ -9,7 +9,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>Microsoft.Boogie.Houdini</RootNamespace> - <AssemblyName>Houdini</AssemblyName> + <AssemblyName>BoogieHoudini</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode> diff --git a/Source/Model/Model.csproj b/Source/Model/Model.csproj index dc0ae5e1..c024975f 100644 --- a/Source/Model/Model.csproj +++ b/Source/Model/Model.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <PropertyGroup> <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> @@ -9,10 +9,10 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>Microsoft.Boogie</RootNamespace> - <AssemblyName>Model</AssemblyName> + <AssemblyName>BoogieModel</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> - <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode> </PropertyGroup> <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> @@ -106,4 +106,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project> +</Project>
\ No newline at end of file diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj index b6f47b00..78601afd 100644 --- a/Source/ModelViewer/ModelViewer.csproj +++ b/Source/ModelViewer/ModelViewer.csproj @@ -9,9 +9,9 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>Microsoft.Boogie.ModelViewer</RootNamespace> - <AssemblyName>ModelViewer</AssemblyName> + <AssemblyName>BoogieModelViewer</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> - <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> <FileAlignment>512</FileAlignment> <PublishUrl>publish\</PublishUrl> <Install>true</Install> diff --git a/Source/ParserHelper/ParserHelper.csproj b/Source/ParserHelper/ParserHelper.csproj index 262ca9b7..b5ed2744 100644 --- a/Source/ParserHelper/ParserHelper.csproj +++ b/Source/ParserHelper/ParserHelper.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <PropertyGroup> <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> @@ -9,10 +9,10 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>ParserHelper</RootNamespace> - <AssemblyName>ParserHelper</AssemblyName> + <AssemblyName>BoogieParserHelper</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> - <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> </PropertyGroup> <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> @@ -139,4 +139,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project> +</Project>
\ No newline at end of file diff --git a/Source/Predication/Predication.csproj b/Source/Predication/Predication.csproj index 803525b3..1319d7f7 100644 --- a/Source/Predication/Predication.csproj +++ b/Source/Predication/Predication.csproj @@ -8,7 +8,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>Predication</RootNamespace> - <AssemblyName>Predication</AssemblyName> + <AssemblyName>BoogiePredication</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> @@ -171,4 +171,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project> +</Project>
\ No newline at end of file diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 06aa5bbe..7b2525f7 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -121,7 +121,7 @@ namespace Microsoft.Boogie.SMTLib } sb.Append(']'); TypeToStringHelper(m.Result, sb); - } else if (t.IsBool || t.IsInt || t.IsReal || t.IsBv) { + } else if (t.IsBool || t.IsInt || t.IsReal || t.IsFloat || t.IsBv) { sb.Append(TypeToString(t)); } else { System.IO.StringWriter buffer = new System.IO.StringWriter(); @@ -145,6 +145,8 @@ namespace Microsoft.Boogie.SMTLib return "Int"; else if (t.IsReal) return "Real"; + else if (t.IsFloat) + return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatSignificand + ")"; else if (t.IsBv) { return "(_ BitVec " + t.BvBits + ")"; } else { @@ -204,6 +206,11 @@ namespace Microsoft.Boogie.SMTLib else wr.Write(lit.ToDecimalString()); } + else if (node is VCExprFloatLit) + { + BigFloat lit = ((VCExprFloatLit)node).Val; + wr.Write("(" + lit.ToBVString() + ")"); + } else { Contract.Assert(false); throw new cce.UnreachableException(); @@ -630,6 +637,78 @@ namespace Microsoft.Boogie.SMTLib return true; } + public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.add RNE", node, options); + return true; + } + + public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.sub RNE", node, options); + return true; + } + + public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.mul RNE", node, options); + return true; + } + + public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.div RNE", node, options); + return true; + } + + public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.rem RNE", node, options); + return true; + } + + public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.min", node, options); + return true; + } + + public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.max", node, options); + return true; + } + + public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.leq", node, options); + return true; + } + + public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.lt", node, options); + return true; + } + + public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.geq", node, options); + return true; + } + + public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.gt", node, options); + return true; + } + + public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.eq", node, options); + return true; + } + static char[] hex = { '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f' }; public bool VisitBvOp(VCExprNAry node, LineariserOptions options) { diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index eaed83e9..1d63fa5d 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -311,7 +311,7 @@ void ObjectInvariant() return; } - if (type.IsBool || type.IsInt || type.IsReal || type.IsBv) + if (type.IsBool || type.IsInt || type.IsReal || type.IsBv || type.IsFloat) return; CtorType ctorType = type as CtorType; diff --git a/Source/UnitTests/CoreTests/CoreTests.csproj b/Source/UnitTests/CoreTests/CoreTests.csproj index 61215d48..24fd8c45 100644 --- a/Source/UnitTests/CoreTests/CoreTests.csproj +++ b/Source/UnitTests/CoreTests/CoreTests.csproj @@ -54,7 +54,7 @@ </ItemGroup> <ItemGroup> <ProjectReference Include="..\..\Basetypes\Basetypes.csproj"> - <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project> + <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project> <Name>Basetypes</Name> </ProjectReference> <ProjectReference Include="..\..\Core\Core.csproj"> diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs index b83983b6..86018d9b 100644 --- a/Source/UnitTests/CoreTests/ExprImmutability.cs +++ b/Source/UnitTests/CoreTests/ExprImmutability.cs @@ -29,6 +29,9 @@ namespace CoreTests var literal4 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 8, /*immutable=*/true); Assert.AreEqual(literal4.ComputeHashCode(), literal4.GetHashCode()); + + var literal5 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigFloat.FromInt(0), /*immutable=*/true); + Assert.AreEqual(literal5.ComputeHashCode(), literal5.GetHashCode()); } [Test()] diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 0c817756..1bcb6afc 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -334,7 +334,10 @@ namespace Microsoft.Boogie.VCExprAST { return Gen.Integer(node.asBigNum); } else if (node.Val is BigDec) { return Gen.Real(node.asBigDec); - } else if (node.Val is BvConst) { + } else if (node.Val is BigFloat) { + return Gen.Float(node.asBigFloat); + } + else if (node.Val is BvConst) { return Gen.Bitvector((BvConst)node.Val); } else { System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString()); @@ -1002,9 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST { if (cce.NonNull(e.Type).IsInt) { return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e); } - else { + else {// if (cce.NonNull(e.Type).IsReal) { return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e); } + //else {//is float + //return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO(8, 23)), e); + //} } else { return Gen.Not(this.args); @@ -1070,34 +1076,48 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result<VCExpr>() != null); Contract.Assert(args.Count == 2); + Type t = cce.NonNull(cce.NonNull(args[0]).Type); switch (app.Op) { case BinaryOperator.Opcode.Add: - if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + if (t.IsInt) { return Gen.Function(VCExpressionGenerator.AddIOp, args); } - else { + else if (t.IsReal) { return Gen.Function(VCExpressionGenerator.AddROp, args); } + else { //t is float + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "+"), args); + } case BinaryOperator.Opcode.Sub: - if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + if (t.IsInt) { return Gen.Function(VCExpressionGenerator.SubIOp, args); } - else { + else if (t.IsReal) { return Gen.Function(VCExpressionGenerator.SubROp, args); } + else { //t is float + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "-"), args); + } case BinaryOperator.Opcode.Mul: - if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + if (t.IsInt) { return Gen.Function(VCExpressionGenerator.MulIOp, args); } - else { + else if (t.IsReal) { return Gen.Function(VCExpressionGenerator.MulROp, args); } + else + { //t is float + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "*"), args); + } case BinaryOperator.Opcode.Div: return Gen.Function(VCExpressionGenerator.DivIOp, args); case BinaryOperator.Opcode.Mod: return Gen.Function(VCExpressionGenerator.ModOp, args); case BinaryOperator.Opcode.RealDiv: + if (t.IsFloat) { + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "/"), args); + } VCExpr arg0 = cce.NonNull(args[0]); VCExpr arg1 = cce.NonNull(args[1]); if (cce.NonNull(arg0.Type).IsInt) { @@ -1112,16 +1132,26 @@ namespace Microsoft.Boogie.VCExprAST { case BinaryOperator.Opcode.Eq: case BinaryOperator.Opcode.Iff: // we don't distinguish between equality and equivalence at this point + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "=="), args); return Gen.Function(VCExpressionGenerator.EqOp, args); case BinaryOperator.Opcode.Neq: return Gen.Function(VCExpressionGenerator.NeqOp, args); case BinaryOperator.Opcode.Lt: + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "<"), args); return Gen.Function(VCExpressionGenerator.LtOp, args); case BinaryOperator.Opcode.Le: + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "<="), args); return Gen.Function(VCExpressionGenerator.LeOp, args); case BinaryOperator.Opcode.Ge: + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, ">="), args); return Gen.Function(VCExpressionGenerator.GeOp, args); case BinaryOperator.Opcode.Gt: + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, ">"), args); return Gen.Function(VCExpressionGenerator.GtOp, args); case BinaryOperator.Opcode.Imp: return Gen.Function(VCExpressionGenerator.ImpliesOp, args); diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index b554c331..1a4374f8 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -380,9 +380,22 @@ namespace Microsoft.Boogie.VCExprAST { internal const string realSubName = "realSub"; internal const string realMulName = "realMul"; internal const string realDivName = "realDiv"; + internal const string floatAddName = "floatAdd"; + internal const string floatSubName = "floatSub"; + internal const string floatMulName = "floatMul"; + internal const string floatDivName = "floatDiv"; + internal const string floatRemName = "floatRem"; + internal const string floatMinName = "floatMin"; + internal const string floatMaxName = "floatMax"; + internal const string floatLeqName = "floatLeq"; + internal const string floatLtName = "floatLt"; + internal const string floatGeqName = "floatGeq"; + internal const string floatGtName = "floatGt"; + internal const string floatEqName = "floatEq"; internal const string realPowName = "realPow"; internal const string toIntName = "toIntCoercion"; internal const string toRealName = "toRealCoercion"; + internal const string toFloatName = "toFloatCoercion"; internal void AssertAsTerm(string x, LineariserOptions options) { Contract.Requires(options != null); @@ -883,7 +896,104 @@ namespace Microsoft.Boogie.VCExprAST { return true; } - public bool VisitBvOp(VCExprNAry node, LineariserOptions options) { + public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatAddName, node, options); + return true; + } + + public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatSubName, node, options); + return true; + } + + public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatMulName, node, options); + return true; + } + + public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatDivName, node, options); + return true; + } + + public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatRemName, node, options); + return true; + } + + public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatMinName, node, options); + return true; + } + + public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatMaxName, node, options); + return true; + } + + public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatLeqName, node, options); + return true; + } + + public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatLtName, node, options); + return true; + } + + public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatGeqName, node, options); + return true; + } + + public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatGtName, node, options); + return true; + } + + public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatEqName, node, options); + return true; + } + + public bool VisitBvOp(VCExprNAry node, LineariserOptions options) + { //Contract.Requires(options != null); //Contract.Requires(node != null); WriteTermApplication("$make_bv" + node.Type.BvBits, node, options); @@ -955,9 +1065,12 @@ namespace Microsoft.Boogie.VCExprAST { if (node.Type.IsInt) { WriteTermApplication(intSubName, node, options); } - else { + else if (node.Type.IsReal) { WriteTermApplication(realSubName, node, options); } + else { + WriteTermApplication(floatSubName, node, options); + } return true; } @@ -967,9 +1080,12 @@ namespace Microsoft.Boogie.VCExprAST { if (node.Type.IsInt) { WriteTermApplication(intMulName, node, options); } - else { + else if (node.Type.IsReal) { WriteTermApplication(realMulName, node, options); } + else { + WriteTermApplication(floatMulName, node, options); + } return true; } @@ -1057,6 +1173,14 @@ namespace Microsoft.Boogie.VCExprAST { return true; } + public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteApplication(toFloatName, 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 76340f97..c2d99d77 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -1424,6 +1424,13 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result<VCExpr>() != null); return CastArguments(node, Type.Real, bindings, 0); } + /*public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArguments(node, Type.Float, bindings, 0); + }*/ public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); @@ -1472,6 +1479,90 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result<VCExpr>() != null); return CastArgumentsToOldType(node, bindings, 0); } + public override VCExpr VisitFloatAddOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatSubOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatMulOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatRemOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatMinOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatMaxOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatLeqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatLtOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatGeqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatGtOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatEqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != 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/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj index 1ad99bc1..efac274e 100644 --- a/Source/VCExpr/VCExpr.csproj +++ b/Source/VCExpr/VCExpr.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <PropertyGroup> <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> @@ -9,7 +9,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>VCExpr</RootNamespace> - <AssemblyName>VCExpr</AssemblyName> + <AssemblyName>BoogieVCExpr</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> @@ -34,7 +34,7 @@ <IsWebBootstrapper>false</IsWebBootstrapper> <UseApplicationTrust>false</UseApplicationTrust> <BootstrapperEnabled>true</BootstrapperEnabled> - <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> </PropertyGroup> <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> <DebugSymbols>true</DebugSymbols> @@ -220,4 +220,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project> +</Project>
\ No newline at end of file diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 2c77a252..b5d4dfb5 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -55,6 +55,13 @@ namespace Microsoft.Boogie { return new VCExprRealLit(x); } + public VCExpr/*!*/ Float(BigFloat x) + { + Contract.Ensures(Contract.Result<VCExpr>() != null); + + return new VCExprFloatLit(x); + } + public VCExpr/*!*/ Function(VCExprOp/*!*/ op, List<VCExpr/*!*/>/*!*/ arguments, List<Type/*!*/>/*!*/ typeArguments) { @@ -319,10 +326,13 @@ namespace Microsoft.Boogie { 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 SubFOp = new VCExprNAryOp(2, Type.Float); public static readonly VCExprOp MulIOp = new VCExprNAryOp(2, Type.Int); public static readonly VCExprOp MulROp = new VCExprNAryOp(2, Type.Real); + //public static readonly VCExprOp MulFOp = new VCExprNAryOp(2, Type.Float); public static readonly VCExprOp DivIOp = new VCExprNAryOp(2, Type.Int); public static readonly VCExprOp DivROp = new VCExprNAryOp(2, Type.Real); + //public static readonly VCExprOp DivFOp = new VCExprNAryOp(2, Type.Float); 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); @@ -336,6 +346,7 @@ namespace Microsoft.Boogie { 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 ToFloatOp = new VCExprNAryOp(1, Type.Float); public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool); @@ -351,6 +362,17 @@ namespace Microsoft.Boogie { return new VCExprBoogieFunctionOp(func); } + // Float nodes + + public VCExprOp BinaryFloatOp(int exp, int man, string op) + { + Contract.Requires(exp > 0); + Contract.Requires(man > 0); + Contract.Requires(op != null); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return new VCExprBinaryFloatOp(exp, man, op); + } + // Bitvector nodes public VCExpr Bitvector(BvConst bv) { @@ -406,7 +428,8 @@ namespace Microsoft.Boogie { Subtype3Op, BvConcatOp, ToIntOp, - ToRealOp + ToRealOp, + ToFloatOp }; internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict; [ContractInvariantMethod] @@ -427,10 +450,13 @@ namespace Microsoft.Boogie { SingletonOpDict.Add(AddROp, SingletonOp.AddOp); SingletonOpDict.Add(SubIOp, SingletonOp.SubOp); SingletonOpDict.Add(SubROp, SingletonOp.SubOp); + //SingletonOpDict.Add(SubFOp, SingletonOp.SubOp); SingletonOpDict.Add(MulIOp, SingletonOp.MulOp); SingletonOpDict.Add(MulROp, SingletonOp.MulOp); + //SingletonOpDict.Add(MulFOp, SingletonOp.MulOp); SingletonOpDict.Add(DivIOp, SingletonOp.DivOp); SingletonOpDict.Add(DivROp, SingletonOp.RealDivOp); + //SingletonOpDict.Add(DivFOp, SingletonOp.FloatDivOp); SingletonOpDict.Add(ModOp, SingletonOp.ModOp); SingletonOpDict.Add(PowOp, SingletonOp.PowOp); SingletonOpDict.Add(LtOp, SingletonOp.LtOp); @@ -441,6 +467,7 @@ namespace Microsoft.Boogie { SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op); SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp); SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp); + //SingletonOpDict.Add(ToFloatOp, SingletonOp.ToFloatOp); } //////////////////////////////////////////////////////////////////////////////// @@ -862,6 +889,31 @@ namespace Microsoft.Boogie.VCExprAST { } } + public class VCExprFloatLit : VCExprLiteral + { + public readonly BigFloat Val; + internal VCExprFloatLit(BigFloat val) + : base(Type.GetFloatType(val.ExponentSize, val.SignificandSize)) + { + this.Val = val; + } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object that) + { + if (Object.ReferenceEquals(this, that)) + return true; + if (that is VCExprFloatLit) + return Val == ((VCExprFloatLit)that).Val; + return false; + } + [Pure] + public override int GetHashCode() + { + return Val.GetHashCode() * 72321; + } + } + ///////////////////////////////////////////////////////////////////////////////// // Operator expressions with fixed arity [ContractClassFor(typeof(VCExprNAry))] @@ -1639,6 +1691,86 @@ namespace Microsoft.Boogie.VCExprAST { } ///////////////////////////////////////////////////////////////////////////////// + // Float operators + + public class VCExprBinaryFloatOp : VCExprOp { + public readonly int Mantissa; + public readonly int Exponent; + private string op; + + public override int Arity { + get { + return 2; + } + } + public override int TypeParamArity { + get { + return 2; + } + } + public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) { + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); + Contract.Ensures(Contract.Result<Type>() != null); + return Type.GetFloatType(Exponent, Mantissa); + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object that) { + if (Object.ReferenceEquals(this, that)) + return true; + if (that is VCExprBinaryFloatOp) + return this.Exponent == ((VCExprBinaryFloatOp)that).Exponent && this.Mantissa == ((VCExprBinaryFloatOp)that).Mantissa; + return false; + } + [Pure] + public override int GetHashCode() { + return Exponent * 81748912 + Mantissa * 67867979; + } + + internal VCExprBinaryFloatOp(int exp, int man, string op) { + this.Exponent = exp; + this.Mantissa = man; + this.op = op; + } + public override Result Accept<Result, Arg> + (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) { + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); + switch (op) { + case ("+"): + return visitor.VisitFloatAddOp(expr, arg); + case ("-"): + return visitor.VisitFloatSubOp(expr, arg); + case ("*"): + return visitor.VisitFloatMulOp(expr, arg); + case ("/"): + return visitor.VisitFloatDivOp(expr, arg); + case ("rem"): + return visitor.VisitFloatRemOp(expr, arg); + case ("min"): + return visitor.VisitFloatMinOp(expr, arg); + case ("max"): + return visitor.VisitFloatMaxOp(expr, arg); + case ("<="): + return visitor.VisitFloatLeqOp(expr, arg); + case ("<"): + return visitor.VisitFloatLtOp(expr, arg); + case (">="): + return visitor.VisitFloatGeqOp(expr, arg); + case (">"): + return visitor.VisitFloatGtOp(expr, arg); + case ("=="): + return visitor.VisitFloatEqOp(expr, arg); + default: + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + } + + ///////////////////////////////////////////////////////////////////////////////// // Bitvector operators public class VCExprBvOp : VCExprOp { diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index 2af4708d..dac9604c 100644 --- a/Source/VCExpr/VCExprASTPrinter.cs +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -242,6 +242,78 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return PrintNAry("Store", node, wr); } + public bool VisitFloatAddOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.add", node, wr); + } + public bool VisitFloatSubOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.sub", node, wr); + } + public bool VisitFloatMulOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.mul", node, wr); + } + public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.div", node, wr); + } + public bool VisitFloatRemOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.rem", node, wr); + } + public bool VisitFloatMinOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.min", node, wr); + } + public bool VisitFloatMaxOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.max", node, wr); + } + public bool VisitFloatLeqOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.leq", node, wr); + } + public bool VisitFloatLtOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.lt", node, wr); + } + public bool VisitFloatGeqOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.geq", node, wr); + } + public bool VisitFloatGtOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.gt", node, wr); + } + public bool VisitFloatEqOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.eq", node, wr); + } public bool VisitBvOp(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 fc1bdd65..a23aaf8a 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -68,6 +68,18 @@ namespace Microsoft.Boogie.VCExprAST { Result VisitLabelOp(VCExprNAry node, Arg arg); Result VisitSelectOp(VCExprNAry node, Arg arg); Result VisitStoreOp(VCExprNAry node, Arg arg); + Result VisitFloatAddOp(VCExprNAry node, Arg arg); + Result VisitFloatSubOp(VCExprNAry node, Arg arg); + Result VisitFloatMulOp(VCExprNAry node, Arg arg); + Result VisitFloatDivOp(VCExprNAry node, Arg arg); + Result VisitFloatRemOp(VCExprNAry node, Arg arg); + Result VisitFloatMinOp(VCExprNAry node, Arg arg); + Result VisitFloatMaxOp(VCExprNAry node, Arg arg); + Result VisitFloatLeqOp(VCExprNAry node, Arg arg); + Result VisitFloatLtOp(VCExprNAry node, Arg arg); + Result VisitFloatGeqOp(VCExprNAry node, Arg arg); + Result VisitFloatGtOp(VCExprNAry node, Arg arg); + Result VisitFloatEqOp(VCExprNAry node, Arg arg); Result VisitBvOp(VCExprNAry node, Arg arg); Result VisitBvExtractOp(VCExprNAry node, Arg arg); Result VisitBvConcatOp(VCExprNAry node, Arg arg); @@ -144,6 +156,78 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException(); } + public Result VisitFloatAddOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatSubOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatMulOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatDivOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatRemOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatMinOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatMaxOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatLeqOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatLtOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatGeqOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatGtOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatEqOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + public Result VisitBvOp(VCExprNAry node, Arg arg) { Contract.Requires(node != null); throw new NotImplementedException(); @@ -234,6 +318,12 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException(); } + public Result VisitToFloat(VCExprNAry node, Arg arg) //TODO: modify later + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) { Contract.Requires(node != null); throw new NotImplementedException(); @@ -1438,6 +1528,65 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return StandardResult(node, arg); } + public virtual Result VisitFloatAddOp(VCExprNAry node, Arg arg) { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatSubOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatMulOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatDivOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatRemOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatMinOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatMaxOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatLeqOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatLtOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatGeqOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatGtOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatEqOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } public virtual Result VisitBvOp(VCExprNAry node, Arg arg) { //Contract.Requires(node != null); return StandardResult(node, arg); @@ -1518,6 +1667,11 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return StandardResult(node, arg); } + public virtual Result VisitToFloatOp(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/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index 9bd3fb1a..4d4fc374 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?> +<?xml version="1.0" encoding="utf-8"?> <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> <PropertyGroup> <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> @@ -9,7 +9,7 @@ <OutputType>Library</OutputType> <AppDesignerFolder>Properties</AppDesignerFolder> <RootNamespace>VCGeneration</RootNamespace> - <AssemblyName>VCGeneration</AssemblyName> + <AssemblyName>BoogieVCGeneration</AssemblyName> <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> <FileAlignment>512</FileAlignment> <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode> @@ -34,7 +34,7 @@ <IsWebBootstrapper>false</IsWebBootstrapper> <UseApplicationTrust>false</UseApplicationTrust> <BootstrapperEnabled>true</BootstrapperEnabled> - <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile> </PropertyGroup> <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> <DebugSymbols>true</DebugSymbols> @@ -227,4 +227,4 @@ <Target Name="AfterBuild"> </Target> --> -</Project> +</Project>
\ No newline at end of file diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl index df19aae4..2e0c6cd1 100644 --- a/Test/civl/ticket.bpl +++ b/Test/civl/ticket.bpl @@ -7,7 +7,7 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x); type X; const nil: X; -var {:layer 0,2} t: int; +var {:layer 0,1} t: int; var {:layer 0,2} s: int; var {:layer 0,2} cs: X; var {:layer 0,2} T: [int]bool; @@ -41,14 +41,15 @@ ensures {:layer 1} {:layer 2} xl != nil; } procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool) -requires {:layer 2} xls' == MapConstBool(true); +requires {:layer 1} Inv1(T, t); +requires {:layer 2} xls' == MapConstBool(true) && Inv2(T, s, cs); { var {:linear "tid"} tid: X; var {:linear "tid"} xls: [X]bool; - yield; + par Yield1() | Yield2(); - call Init(xls'); + call InitAbstract(xls'); xls := xls'; par Yield1() | Yield2(); @@ -96,10 +97,20 @@ ensures {:layer 2} Inv2(T, s, cs) && cs == tid; par Yield1() | Yield2() | YieldSpec(tid); } +procedure {:yields} {:layer 1,2} InitAbstract({:linear "tid"} xls:[X]bool) +requires {:layer 1} Inv1(T, t); +ensures {:layer 1} Inv1(T, t); +ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; s := 0; T := RightOpen(0); return true; }|; +{ + par Yield1(); + call Init(xls); + par Yield1(); +} + procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int) requires {:layer 1} Inv1(T, t); ensures {:layer 1} Inv1(T, t); -ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|; +ensures {:right} |{ A: havoc m; assume !T[m]; T[m] := true; return true; }|; { par Yield1(); call m := GetTicket(tid); @@ -130,7 +141,7 @@ ensures {:layer 1} Inv1(T,t); assert {:layer 1} Inv1(T,t); } -procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool); +procedure {:yields} {:layer 0,1} Init({:linear "tid"} xls:[X]bool); ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|; procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int); @@ -140,7 +151,7 @@ procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int); ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|; procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X); -ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|; +ensures {:atomic} |{ A: assert cs == tid; s := s + 1; cs := nil; return true; }|; procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); ensures {:atomic} |{ A: assume xl != nil; return true; }|; diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect index dc45a0ee..6696bdbd 100644 --- a/Test/civl/ticket.bpl.expect +++ b/Test/civl/ticket.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 24 verified, 0 errors +Boogie program verifier finished with 26 verified, 0 errors diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl new file mode 100644 index 00000000..d7faa4b0 --- /dev/null +++ b/Test/floats/float0.bpl @@ -0,0 +1,14 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : real) returns (r : float8e24) +{ + r := 15; // Error + r := 15.0; // Error + r := 0e1f22e8; // Error + r := 1e0f23e8; // Error + r := x; // Error + r := 1e0f23e8 + 1e0f23e8; // Error + r := 1e0f24e8 + 1e0f23e8; // Error + + return; +}
\ No newline at end of file diff --git a/Test/floats/float0.bpl.expect b/Test/floats/float0.bpl.expect new file mode 100644 index 00000000..f657a846 --- /dev/null +++ b/Test/floats/float0.bpl.expect @@ -0,0 +1,8 @@ +float0.bpl(5,1): Error: mismatched types in assignment command (cannot assign int to float8e24) +float0.bpl(6,1): Error: mismatched types in assignment command (cannot assign real to float8e24) +float0.bpl(7,1): Error: mismatched types in assignment command (cannot assign float22e8 to float8e24) +float0.bpl(8,1): Error: mismatched types in assignment command (cannot assign float23e8 to float8e24) +float0.bpl(9,1): Error: mismatched types in assignment command (cannot assign real to float8e24) +float0.bpl(10,1): Error: mismatched types in assignment command (cannot assign float23e8 to float8e24) +float0.bpl(11,15): Error: invalid argument types (float24e8 and float23e8) to binary operator + +7 type checking errors detected in float0.bpl diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl new file mode 100644 index 00000000..d7fc7837 --- /dev/null +++ b/Test/floats/float1.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : float24e8) returns (r : float24e8) +{ + r := 0e128f24e8; + r := 1e127f24e8; + r := x; + r := x + 1e127f24e8; + r := 0e127f24e8 + 0e127f24e8; + assert(r == 0e128f24e8); + + return; +}
\ No newline at end of file diff --git a/Test/floats/float1.bpl.expect b/Test/floats/float1.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float1.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float10.bpl b/Test/floats/float10.bpl new file mode 100644 index 00000000..ec9b4895 --- /dev/null +++ b/Test/floats/float10.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11); + +procedure double_range_true() returns () { + var x : float53e11; + havoc x; + if (x >= TO_FLOAT64_REAL(-1e307) && x <= TO_FLOAT64_REAL(1e307)) { + assert(x==x); + } +} + +procedure double_range_false() returns () { + var x : float53e11; + havoc x; + assert(x==x); +}
\ No newline at end of file diff --git a/Test/floats/float10.bpl.expect b/Test/floats/float10.bpl.expect new file mode 100644 index 00000000..b60994d4 --- /dev/null +++ b/Test/floats/float10.bpl.expect @@ -0,0 +1,5 @@ +float10.bpl(17,2): Error BP5001: This assertion might not hold. +Execution trace: + float10.bpl(16,2): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/floats/float11.bpl b/Test/floats/float11.bpl new file mode 100644 index 00000000..de148424 --- /dev/null +++ b/Test/floats/float11.bpl @@ -0,0 +1,22 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8); + +procedure main() returns () { + var tick : float24e8; + var time : float24e8; + var i: int; + + tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10); + time := TO_FLOAT32_INT(0); + + i := 0; + while (i < 10) + { + time := time + tick; + i := i + 1; + } + assert time == TO_FLOAT32_INT(1); +}
\ No newline at end of file diff --git a/Test/floats/float11.bpl.expect b/Test/floats/float11.bpl.expect new file mode 100644 index 00000000..213345cb --- /dev/null +++ b/Test/floats/float11.bpl.expect @@ -0,0 +1,7 @@ +float11.bpl(21,2): Error BP5001: This assertion might not hold. +Execution trace: + float11.bpl(12,7): anon0 + float11.bpl(16,2): anon3_LoopHead + float11.bpl(16,2): anon3_LoopDone + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/floats/float12.bpl b/Test/floats/float12.bpl new file mode 100644 index 00000000..914286bb --- /dev/null +++ b/Test/floats/float12.bpl @@ -0,0 +1,16 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float24e8) returns (float53e11); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float53e11) returns (float24e8); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float53e11); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11); + +procedure main() returns () { + var x : float53e11; + var y : float24e8; + + x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1); + y := TO_FLOAT32_FLOAT64(x); + assert x != TO_FLOAT64_FLOAT32(y); +}
\ No newline at end of file diff --git a/Test/floats/float12.bpl.expect b/Test/floats/float12.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float12.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl new file mode 100644 index 00000000..9c99a30b --- /dev/null +++ b/Test/floats/float13.bpl @@ -0,0 +1,34 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float53e11); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float53e11); + +procedure main() returns () { + var f : float24e8; + var fc : float24e8; + var d : float53e11; + var dc : float53e11; + + f := 2097152e129f24e8; + fc := TO_FLOAT32_INT(5); + assert(f == fc); + + f := -0e126f24e8; + fc := TO_FLOAT32_REAL(-0.5); + assert(f == fc); + + f := 1048576e128f24e8; + fc := TO_FLOAT32_REAL(2.25); + assert(f == fc); + + d := 1125899906842624e1025f53e11; + dc := TO_FLOAT64_INT(5); + assert(d == dc); + + d := 562949953421312e1024f53e11; + dc := TO_FLOAT64_REAL(2.25); + assert(d == dc); +}
\ No newline at end of file diff --git a/Test/floats/float13.bpl.expect b/Test/floats/float13.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float13.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float14.bpl b/Test/floats/float14.bpl new file mode 100644 index 00000000..1752ef0d --- /dev/null +++ b/Test/floats/float14.bpl @@ -0,0 +1,22 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var f : float24e8; + var d : float53e11; + + f := 0e-1f24e8; //Error + f := 0e256f24e8; //Error + f := 0e255f24e8; //No Error + + f := 8388608e0f24e8; //Error + f := -8388608e0f24e8; //Error + f := 8388607e0f24e8; //No Error + + d := 0e-1f53e11; //Error + d := 0e2048f53e11; //Error + d := 0e2047f53e11; //No Error + + d := 4503599627370496e0f53e11; //Error + d := -4503599627370496e0f53e11; //Error + d := 4503599627370495e0f53e11; //No Error +}
\ No newline at end of file diff --git a/Test/floats/float14.bpl.expect b/Test/floats/float14.bpl.expect new file mode 100644 index 00000000..f42b0286 --- /dev/null +++ b/Test/floats/float14.bpl.expect @@ -0,0 +1,9 @@ +float14.bpl(7,7): error: incorrectly formatted floating point, The given exponent -1 cannot fit in the bit size 8 +float14.bpl(8,7): error: incorrectly formatted floating point, The given exponent 256 cannot fit in the bit size 8 +float14.bpl(11,7): error: incorrectly formatted floating point, The given significand 8388608 cannot fit in the bit size 24 +float14.bpl(12,7): error: incorrectly formatted floating point, The given significand 8388608 cannot fit in the bit size 24 +float14.bpl(15,7): error: incorrectly formatted floating point, The given exponent -1 cannot fit in the bit size 11 +float14.bpl(16,7): error: incorrectly formatted floating point, The given exponent 2048 cannot fit in the bit size 11 +float14.bpl(19,7): error: incorrectly formatted floating point, The given significand 4503599627370496 cannot fit in the bit size 53 +float14.bpl(20,7): error: incorrectly formatted floating point, The given significand 4503599627370496 cannot fit in the bit size 53 +8 parse errors detected in float14.bpl diff --git a/Test/floats/float2.bpl b/Test/floats/float2.bpl new file mode 100644 index 00000000..ed9e60f0 --- /dev/null +++ b/Test/floats/float2.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : float11e5) returns(r : float24e8) { + var y : float53e11; + var z : float113e15; + + r := x; // Error + r := y; // Error + r := z; // Error + y := x; // Error + y := z; // Error + z := x; // Error + + return; +}
\ No newline at end of file diff --git a/Test/floats/float2.bpl.expect b/Test/floats/float2.bpl.expect new file mode 100644 index 00000000..3132c514 --- /dev/null +++ b/Test/floats/float2.bpl.expect @@ -0,0 +1,7 @@ +float2.bpl(7,1): Error: mismatched types in assignment command (cannot assign float11e5 to float24e8) +float2.bpl(8,1): Error: mismatched types in assignment command (cannot assign float53e11 to float24e8) +float2.bpl(9,1): Error: mismatched types in assignment command (cannot assign float113e15 to float24e8) +float2.bpl(10,1): Error: mismatched types in assignment command (cannot assign float11e5 to float53e11) +float2.bpl(11,1): Error: mismatched types in assignment command (cannot assign float113e15 to float53e11) +float2.bpl(12,1): Error: mismatched types in assignment command (cannot assign float11e5 to float113e15) +6 type checking errors detected in float2.bpl diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl new file mode 100644 index 00000000..507c4127 --- /dev/null +++ b/Test/floats/float3.bpl @@ -0,0 +1,27 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float24e8; + var y : float24e8; + var z : float24e8; + + z := x + y; + z := x - y; + z := x * y; + assume(y != 0e0f24e8); + z := x / y; + + z := (0e127f24e8 + 0e127f24e8 + 0e0f24e8); + assert(z == 0e128f24e8); + + z := 0e128f24e8 - 0e127f24e8; + assert(z == 0e127f24e8); + + z := 0e127f24e8 * 0e127f24e8; + assert(z == 0e127f24e8); + + z := 0e127f24e8 / 0e127f24e8; + assert(z == 0e127f24e8); + + return; +}
\ No newline at end of file diff --git a/Test/floats/float3.bpl.expect b/Test/floats/float3.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float3.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl new file mode 100644 index 00000000..1c2df42e --- /dev/null +++ b/Test/floats/float4.bpl @@ -0,0 +1,19 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo() returns (r : float8e24) { + var d : float53e11; + + r := 0NaN8e24; + r := 0nan8e24; + r := 0+oo8e24; + r := 0-oo8e24; + r := -5e255f8e24; + + d := 0NaN53e11; + d := 0nan53e11; + d := 0+oo53e11; + d := 0-oo53e11; + d := -200e2000f53e11; + + return; +}
\ No newline at end of file diff --git a/Test/floats/float4.bpl.expect b/Test/floats/float4.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float4.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float5.bpl b/Test/floats/float5.bpl new file mode 100644 index 00000000..12b19cf5 --- /dev/null +++ b/Test/floats/float5.bpl @@ -0,0 +1,23 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_INT(int) returns (float23e8); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_REAL(real) returns (float23e8); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV31(bv31) returns (float23e8); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV32(bv32) returns (float23e8); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_FLOAT824(float24e8) returns (float24e8); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT823(float23e8) returns (float24e8); + +procedure foo(x : float24e8) returns (r : float24e8) { + r := TO_FLOAT823_INT(5); // Error + r := TO_FLOAT823_REAL(5.0); // Error + r := TO_FLOAT823_BV31(0bv31); // Error + r := TO_FLOAT823_BV32(0bv32); // Error + r := TO_FLOAT823_FLOAT824(0e0f24e8); // Error + r := TO_FLOAT824_FLOAT823(0e0f23e8); // Error + + r := TO_FLOAT823_FLOAT824(x); // Error + r := TO_FLOAT824_FLOAT823(x); // Error + + return; +}
\ No newline at end of file diff --git a/Test/floats/float5.bpl.expect b/Test/floats/float5.bpl.expect new file mode 100644 index 00000000..74649769 --- /dev/null +++ b/Test/floats/float5.bpl.expect @@ -0,0 +1,6 @@ +float5.bpl(12,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8) +float5.bpl(13,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8) +float5.bpl(14,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8) +float5.bpl(15,1): Error: mismatched types in assignment command (cannot assign float23e8 to float24e8) +float5.bpl(20,27): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float24e8 (expected: float23e8) +5 type checking errors detected in float5.bpl diff --git a/Test/floats/float6.bpl b/Test/floats/float6.bpl new file mode 100644 index 00000000..fecf0385 --- /dev/null +++ b/Test/floats/float6.bpl @@ -0,0 +1,30 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_BV32(bv32) returns (float24e8); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_BV64(bv64) returns (float53e11); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float53e11) returns (float24e8); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float24e8) returns (float53e11); + +procedure main() returns () { + var i : int; + var r : real; + var f32 : float24e8; + var f64 : float53e11; + + f32 := TO_FLOAT32_INT(5); + f32 := TO_FLOAT32_REAL(5.0); + + f32 := TO_FLOAT32_BV32(0bv32); + f64 := TO_FLOAT64_BV64(0bv64); + + f32 := TO_FLOAT32_FLOAT64(0e0f53e11); + f64 := TO_FLOAT64_FLOAT32(0e0f24e8); + + f32 := TO_FLOAT32_FLOAT64(f64); + f64 := TO_FLOAT64_FLOAT32(f32); + + return; +}
\ No newline at end of file diff --git a/Test/floats/float6.bpl.expect b/Test/floats/float6.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float6.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float7.bpl b/Test/floats/float7.bpl new file mode 100644 index 00000000..39fca79e --- /dev/null +++ b/Test/floats/float7.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float53e11; + var y : float53e11; + var z : float53e11; + var r : float53e11; + x := 0e1063f53e11; + y := x + 0e1023f53e11; + z := x - 0e1023f53e11; + r := y - z; + assert r == 0e1024f53e11; +}
\ No newline at end of file diff --git a/Test/floats/float7.bpl.expect b/Test/floats/float7.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float7.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl new file mode 100644 index 00000000..bfb3b9e9 --- /dev/null +++ b/Test/floats/float8.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float24e8; + var y : float24e8; + var z : float24e8; + var r : float24e8; + x := 0e167f24e8; + y := x + 0e127f24e8; + z := x - 0e127f24e8; + r := y - z; + assert r == 0e128f24e8; +}
\ No newline at end of file diff --git a/Test/floats/float8.bpl.expect b/Test/floats/float8.bpl.expect new file mode 100644 index 00000000..c55c4619 --- /dev/null +++ b/Test/floats/float8.bpl.expect @@ -0,0 +1,5 @@ +float8.bpl(12,2): Error BP5001: This assertion might not hold. +Execution trace: + float8.bpl(8,4): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/floats/float9.bpl b/Test/floats/float9.bpl new file mode 100644 index 00000000..b1e46ae4 --- /dev/null +++ b/Test/floats/float9.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float24e8); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8); + +procedure main() returns () { + var x : float24e8; + var y : float24e8; + var z : float24e8; + var r : float24e8; + x := TO_FLOAT32_REAL(1e7); + y := x + TO_FLOAT32_INT(1); + z := x - TO_FLOAT32_INT(1); + r := y - z; + assert r == TO_FLOAT32_INT(2); +}
\ No newline at end of file diff --git a/Test/floats/float9.bpl.expect b/Test/floats/float9.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float9.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors |