From 8e5671a4763542c767a8bdba4b6ea41a2ad7691f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 17 Nov 2014 20:58:26 +0000 Subject: Introduce unit tests which use NUnit. NUnit is now a dependency so developers need to install it via NuGet. There aren't many tests yet. Just a few for Core and Basetypes but hopefully more will be added in the future. More information can be found in Source/UnitTests/README.md --- .gitignore | 2 + .hgignore | 2 + Source/.nuget/packages.config | 4 + Source/Boogie.sln | 90 ++++++- .../UnitTests/BasetypesTests/BasetypesTests.csproj | 69 ++++++ Source/UnitTests/BasetypesTests/BigDecTests.cs | 29 +++ .../BasetypesTests/Properties/AssemblyInfo.cs | 36 +++ Source/UnitTests/BasetypesTests/packages.config | 4 + Source/UnitTests/CoreTests/AbsyMetadata.cs | 101 ++++++++ Source/UnitTests/CoreTests/CoreTests.csproj | 82 +++++++ Source/UnitTests/CoreTests/Duplicator.cs | 258 +++++++++++++++++++++ Source/UnitTests/CoreTests/ExprEquality.cs | 179 ++++++++++++++ .../UnitTests/CoreTests/Properties/AssemblyInfo.cs | 36 +++ Source/UnitTests/CoreTests/packages.config | 4 + Source/UnitTests/README.md | 55 +++++ .../TestUtil/AssertionTextWriterTraceListener.cs | 27 +++ Source/UnitTests/TestUtil/BoogieTestBase.cs | 24 ++ Source/UnitTests/TestUtil/ProgramLoader.cs | 33 +++ .../UnitTests/TestUtil/Properties/AssemblyInfo.cs | 36 +++ Source/UnitTests/TestUtil/TestUtil.csproj | 71 ++++++ Source/UnitTests/TestUtil/packages.config | 4 + Source/UnitTests/run-unittests.py | 124 ++++++++++ 22 files changed, 1269 insertions(+), 1 deletion(-) create mode 100644 Source/.nuget/packages.config create mode 100644 Source/UnitTests/BasetypesTests/BasetypesTests.csproj create mode 100644 Source/UnitTests/BasetypesTests/BigDecTests.cs create mode 100644 Source/UnitTests/BasetypesTests/Properties/AssemblyInfo.cs create mode 100644 Source/UnitTests/BasetypesTests/packages.config create mode 100644 Source/UnitTests/CoreTests/AbsyMetadata.cs create mode 100644 Source/UnitTests/CoreTests/CoreTests.csproj create mode 100644 Source/UnitTests/CoreTests/Duplicator.cs create mode 100644 Source/UnitTests/CoreTests/ExprEquality.cs create mode 100644 Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs create mode 100644 Source/UnitTests/CoreTests/packages.config create mode 100644 Source/UnitTests/README.md create mode 100644 Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs create mode 100644 Source/UnitTests/TestUtil/BoogieTestBase.cs create mode 100644 Source/UnitTests/TestUtil/ProgramLoader.cs create mode 100644 Source/UnitTests/TestUtil/Properties/AssemblyInfo.cs create mode 100644 Source/UnitTests/TestUtil/TestUtil.csproj create mode 100644 Source/UnitTests/TestUtil/packages.config create mode 100644 Source/UnitTests/run-unittests.py diff --git a/.gitignore b/.gitignore index 09d82658..c54c82dd 100644 --- a/.gitignore +++ b/.gitignore @@ -10,6 +10,8 @@ Source/*/bin Source/*/obj Source/Provers/*/bin Source/Provers/*/obj +Source/packages/* +Source/UnitTests/TestResult.xml Binaries/ITaskManager.dll Binaries/ITaskManager.pdb Binaries/Microsoft.SpecSharp.Runtime.dll diff --git a/.hgignore b/.hgignore index fe35b0ed..05298dae 100644 --- a/.hgignore +++ b/.hgignore @@ -3,6 +3,7 @@ syntax: regexp ^Source/_ReSharper\.Boogie$ ^Source/.*\.(user|suo|cache|vs10x)$ ^Source/Core/(Parser|Scanner).cs.old$ +^Source/packages/.*$ ^Binaries/.*\.(dll|pdb|exe|manifest|config)$ ^.*(bin|obj)/([^/]*/)?(Debug|Release|Checked|Debug All|DEBUG ALL)/.*$ Test/.*/Output @@ -16,3 +17,4 @@ backup.diff *.exe.mdb *.pidb *.userprefs +TestResult.xml diff --git a/Source/.nuget/packages.config b/Source/.nuget/packages.config new file mode 100644 index 00000000..f0b15e98 --- /dev/null +++ b/Source/.nuget/packages.config @@ -0,0 +1,4 @@ + + + + \ No newline at end of file diff --git a/Source/Boogie.sln b/Source/Boogie.sln index ff116c50..aabaed90 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -1,7 +1,7 @@  Microsoft Visual Studio Solution File, Format Version 12.00 # Visual Studio 2013 -VisualStudioVersion = 12.0.21005.1 +VisualStudioVersion = 12.0.31101.0 MinimumVisualStudioVersion = 10.0.40219.1 Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758C1E3-824A-439F-AA2F-0BA1143E8C8D}" EndProject @@ -44,6 +44,19 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BVD", "BVD\BVD.csproj", "{8 EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "Concurrency\Concurrency.csproj", "{D07B8E38-E172-47F4-AD02-0373014A46D3}" EndProject +Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "UnitTests", "UnitTests", "{0C77D814-EC94-45D7-9F9B-213C425D0F15}" +EndProject +Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = ".nuget", ".nuget", "{83CAF6FB-75EB-422D-B341-D61E07A0FAEB}" + ProjectSection(SolutionItems) = preProject + .nuget\packages.config = .nuget\packages.config + EndProjectSection +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CoreTests", "UnitTests\CoreTests\CoreTests.csproj", "{961B3BCA-2067-43B2-8E43-23C4293F21B9}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TestUtil", "UnitTests\TestUtil\TestUtil.csproj", "{59118E35-4236-495E-AF6E-0D641302ED2C}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BasetypesTests", "UnitTests\BasetypesTests\BasetypesTests.csproj", "{D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Checked|.NET = Checked|.NET @@ -552,11 +565,86 @@ Global {D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU {D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU {D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|x86.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|.NET.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|Any CPU.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|Any CPU.Build.0 = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|Mixed Platforms.Build.0 = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|x86.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|.NET.ActiveCfg = Debug|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|Any CPU.Build.0 = Debug|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|x86.ActiveCfg = Debug|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|.NET.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|Any CPU.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|Any CPU.Build.0 = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|Mixed Platforms.Build.0 = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|x86.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|.NET.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|Any CPU.Build.0 = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|x86.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|.NET.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|Any CPU.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|Any CPU.Build.0 = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|Mixed Platforms.Build.0 = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|x86.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|.NET.ActiveCfg = Debug|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|Any CPU.Build.0 = Debug|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|x86.ActiveCfg = Debug|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|.NET.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|Any CPU.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|Any CPU.Build.0 = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|Mixed Platforms.Build.0 = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|x86.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|.NET.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|Any CPU.Build.0 = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU + {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|x86.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|.NET.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|Any CPU.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|Any CPU.Build.0 = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|Mixed Platforms.Build.0 = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|x86.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|.NET.ActiveCfg = Debug|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|Any CPU.Build.0 = Debug|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|x86.ActiveCfg = Debug|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|.NET.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|Any CPU.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|Any CPU.Build.0 = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|Mixed Platforms.Build.0 = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|x86.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|.NET.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|Any CPU.Build.0 = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|x86.ActiveCfg = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE EndGlobalSection GlobalSection(NestedProjects) = preSolution {9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D} + {961B3BCA-2067-43B2-8E43-23C4293F21B9} = {0C77D814-EC94-45D7-9F9B-213C425D0F15} + {59118E35-4236-495E-AF6E-0D641302ED2C} = {0C77D814-EC94-45D7-9F9B-213C425D0F15} + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9} = {0C77D814-EC94-45D7-9F9B-213C425D0F15} EndGlobalSection EndGlobal diff --git a/Source/UnitTests/BasetypesTests/BasetypesTests.csproj b/Source/UnitTests/BasetypesTests/BasetypesTests.csproj new file mode 100644 index 00000000..483c12c7 --- /dev/null +++ b/Source/UnitTests/BasetypesTests/BasetypesTests.csproj @@ -0,0 +1,69 @@ + + + + + Debug + AnyCPU + {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9} + Library + Properties + BasetypesTests + BasetypesTests + v4.5 + 512 + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + + ..\..\packages\NUnit.2.6.3\lib\nunit.framework.dll + + + + + + + + + + + + + + + + + + + + {43dfad18-3e35-4558-9be2-caff6b5ba8a0} + Basetypes + + + + + + + + \ No newline at end of file diff --git a/Source/UnitTests/BasetypesTests/BigDecTests.cs b/Source/UnitTests/BasetypesTests/BigDecTests.cs new file mode 100644 index 00000000..cee80216 --- /dev/null +++ b/Source/UnitTests/BasetypesTests/BigDecTests.cs @@ -0,0 +1,29 @@ +using Microsoft.Basetypes; +using NUnit.Framework; +using System.Numerics; + +namespace BasetypesTests +{ + [TestFixture()] + public class BigDecTests { + + [Test()] + public void FromStringNegative() { + // This tests for a Bug in Boogie that used to be present where BigDec + // would not parse strings with negative numbers correctly + // + // If this bug is present this test will fail when checking the mantissa + var v = BigDec.FromString("-1.5"); + Assert.AreEqual(-1, v.Exponent); + Assert.AreEqual(new BigInteger(-15.0), v.Mantissa); + } + + [Test()] + public void FromStringPositive() { + var v = BigDec.FromString("1.5"); + Assert.AreEqual(-1, v.Exponent); + Assert.AreEqual(new BigInteger(15.0), v.Mantissa); + } + } +} + diff --git a/Source/UnitTests/BasetypesTests/Properties/AssemblyInfo.cs b/Source/UnitTests/BasetypesTests/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..4ef7c05c --- /dev/null +++ b/Source/UnitTests/BasetypesTests/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("BasetypesTests")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("")] +[assembly: AssemblyProduct("BasetypesTests")] +[assembly: AssemblyCopyright("Copyright © 2014")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("0cca79cc-3251-46d9-87c1-32bc782d9fdd")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("1.0.*")] +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/Source/UnitTests/BasetypesTests/packages.config b/Source/UnitTests/BasetypesTests/packages.config new file mode 100644 index 00000000..d4e241a2 --- /dev/null +++ b/Source/UnitTests/BasetypesTests/packages.config @@ -0,0 +1,4 @@ + + + + \ No newline at end of file diff --git a/Source/UnitTests/CoreTests/AbsyMetadata.cs b/Source/UnitTests/CoreTests/AbsyMetadata.cs new file mode 100644 index 00000000..156f38b5 --- /dev/null +++ b/Source/UnitTests/CoreTests/AbsyMetadata.cs @@ -0,0 +1,101 @@ +using Microsoft.Boogie; +using NUnit.Framework; +using System; + +namespace CoreTests +{ + [TestFixture ()] + public class AbsyMetadata { + private Absy GetAbsy() { + // The choice of Absy type here is arbitary + return new AssertCmd(Token.NoToken, Expr.True); + } + + [Test(), ExpectedException(typeof(ArgumentOutOfRangeException))] + public void NoMetadata() { + var absy = GetAbsy(); + + Assert.AreEqual(0, absy.NumberedMetaDataCount); + + string willFail = absy.GetMetadata(0); + // use willFail in someway so the result is live + Assert.IsNotNullOrEmpty(willFail); + } + + [Test(), ExpectedException(typeof(ArgumentOutOfRangeException))] + public void InvalidIndex() { + var absy = GetAbsy(); + + Assert.AreEqual(0, absy.NumberedMetaDataCount); + absy.SetMetadata(0, "hello"); + + string willFail = absy.GetMetadata(1); + // use willFail in someway so the result is live + Assert.IsNotNullOrEmpty(willFail); + } + + [Test()] + public void SimpleMetadata() { + var absy = GetAbsy(); + Assert.AreEqual(0, absy.NumberedMetaDataCount); + + var string1 = "hello"; + var string2 = "hello2"; + absy.SetMetadata(0, string1); + Assert.AreEqual(1, absy.NumberedMetaDataCount); + absy.SetMetadata(1, string2); + Assert.AreEqual(2, absy.NumberedMetaDataCount); + + Assert.AreSame(string1, absy.GetMetadata(0)); + Assert.AreSame(string2, absy.GetMetadata(1)); + + // Now try iterating over the metadata + int count = 0; + foreach (var o in absy.NumberedMetadata) { + Assert.AreEqual(count, o.Key); + Assert.IsNotNull(o.Value); + ++count; + } + Assert.AreEqual(2, count); + } + + [Test(), ExpectedException(typeof(InvalidCastException))] + public void IncorrectType() { + var absy = GetAbsy(); + Assert.AreEqual(0, absy.NumberedMetaDataCount); + + var string0 = "hello world"; + absy.SetMetadata(0, string0); + + // Now try retrive wrong type + int wrongType = absy.GetMetadata(0); + // use "wrongType" is someway so the variable is live + Assert.AreEqual(0, wrongType); + } + + [Test()] + public void NullPadding() { + var absy = GetAbsy(); + Assert.AreEqual(0, absy.NumberedMetaDataCount); + + string foo = "foo"; + absy.SetMetadata(10, foo); + Assert.AreEqual(11, absy.NumberedMetaDataCount); + + // Should nulls be made accessible? Right now its impossible to access + // them as we always throw an exception if the stored item is null + for (int i = 0; i <= 9 ; ++i) { + try { + absy.GetMetadata(i); + Assert.Fail("Accesing unset metadata should of failed"); + } + catch (InvalidCastException) { + } + } + + + Assert.AreSame(foo, absy.GetMetadata(10)); + } + } +} + diff --git a/Source/UnitTests/CoreTests/CoreTests.csproj b/Source/UnitTests/CoreTests/CoreTests.csproj new file mode 100644 index 00000000..1bad6134 --- /dev/null +++ b/Source/UnitTests/CoreTests/CoreTests.csproj @@ -0,0 +1,82 @@ + + + + + Debug + AnyCPU + {961B3BCA-2067-43B2-8E43-23C4293F21B9} + Library + Properties + CoreTests + CoreTests + v4.5 + 512 + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + + ..\..\packages\NUnit.2.6.3\lib\nunit.framework.dll + + + + + + + + + + + + + + + + + + + + + {43dfad18-3e35-4558-9be2-caff6b5ba8a0} + Basetypes + + + {b230a69c-c466-4065-b9c1-84d80e76d802} + Core + + + {fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5} + ParserHelper + + + {59118e35-4236-495e-af6e-0d641302ed2c} + TestUtil + + + + + + + + \ No newline at end of file diff --git a/Source/UnitTests/CoreTests/Duplicator.cs b/Source/UnitTests/CoreTests/Duplicator.cs new file mode 100644 index 00000000..978a041b --- /dev/null +++ b/Source/UnitTests/CoreTests/Duplicator.cs @@ -0,0 +1,258 @@ +using Microsoft.Boogie.TestUtil; +using Microsoft.Boogie; +using Microsoft.Basetypes; +using NUnit.Framework; +using System; +using System.Linq; + + +namespace CoreTests +{ + [TestFixture ()] + public class DuplicatorTests : BoogieTestBase, IErrorSink { + Duplicator d; + + public void Error(IToken tok, string msg) { + Assert.Fail(msg); + } + + [SetUp] + public void Init() { + d = new Duplicator(); + } + + [Test()] + public void BVConcatExpr() { + var bv1_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 8); + var bv2_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(2), 8); + var A = new BvConcatExpr(Token.NoToken, bv1_8, bv2_8); + var B = d.Visit(A); + + // The duplicator should ensure we get new BVConcatExprs + Assert.AreNotSame(A, B); + } + + [Test()] + public void BvExtractExpr() { + var bv2_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(2), 8); + var A = new BvExtractExpr(Token.NoToken, bv2_8, 6,0); + var B = d.Visit(A); + + // The duplicator should ensure we get new BVExtractExprs + Assert.AreNotSame(A, B); + } + + [Test()] + public void NaryExpr() { + var bv1_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 8); + var bv2_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(2), 8); + var A = NAryExpr.Eq (bv1_8, bv2_8); + var B = d.Visit(A); + + Assert.AreNotSame(A, B); + } + + [Test()] + public void WholeProgram() { + var p = new Program(); + var t = new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.Bool); + var gv = new GlobalVariable(Token.NoToken, t); + p.AddTopLevelDeclaration(gv); + string metaDataString = "This is a test"; + p.SetMetadata(0, metaDataString); + + // Now try to clone + var p2 = (Program) d.Visit(p); + + // Check global is a copy + int counter = 0; + GlobalVariable gv2 = null; + foreach (var g in p2.TopLevelDeclarations) + { + ++counter; + Assert.IsInstanceOf(g); + gv2 = g as GlobalVariable; + } + Assert.AreEqual(1, counter); + Assert.AreNotSame(gv, gv2); + Assert.AreEqual(metaDataString, p2.GetMetadata(0)); + + + // Check Top level declarations list is duplicated properly + var t2 = new TypedIdent(Token.NoToken, "bar", Microsoft.Boogie.Type.Bool); + var gv3 = new GlobalVariable(Token.NoToken, t2); + p2.AddTopLevelDeclaration(gv3); + + counter = 0; + foreach (var g in p2.TopLevelDeclarations) { + ++counter; + Assert.IsInstanceOf(g); + } + Assert.AreEqual(2, counter); + + // The original program should still only have one global variable + counter = 0; + foreach (var g in p.TopLevelDeclarations) { + ++counter; + Assert.IsInstanceOf(g); + Assert.AreSame(g, gv); + } + + Assert.AreEqual(1, counter); + + // Change Metadata in p2, this shouldn't affect p + string newMetaDataString = "Another test"; + p2.SetMetadata(0, newMetaDataString); + + Assert.AreNotEqual(p2.GetMetadata(0), p.GetMetadata(0)); + } + + [Test()] + public void GotoTargets() { + Program p = TestUtil.ProgramLoader.LoadProgramFrom(@" + procedure main() + { + entry: + assume true; + goto thing1, thing2; + + thing1: + assume true; + assume true; + goto entry, thing1; + + thing2: + assume true; + assume true; + return; + } + "); + + var main = p.TopLevelDeclarations.OfType().Where(x => x.Name == "main").First(); + + // Access blocks via their labels of gotocmds + var oldEntryBlock = ( main.Blocks[1].TransferCmd as GotoCmd ).labelTargets[0]; + Assert.AreEqual("entry", oldEntryBlock.Label); + + var oldThing1Block = ( main.Blocks[1].TransferCmd as GotoCmd ).labelTargets[1]; + Assert.AreEqual("thing1", oldThing1Block.Label); + + var oldThing2Block = ( main.Blocks[0].TransferCmd as GotoCmd ).labelTargets[1]; + Assert.AreEqual("thing2", oldThing2Block.Label); + + // Now duplicate + var newProgram = (Program) d.Visit(p); + + // First lets check blocks have been duplicated + var newMain= newProgram.TopLevelDeclarations.OfType().Where(x => x.Name == "main").First(); + var newEntryBlock = newMain.Blocks[0]; + Assert.AreEqual("entry", newEntryBlock.Label); + Assert.AreNotSame(newEntryBlock, oldEntryBlock); + + var newThing1Block = newMain.Blocks[1]; + Assert.AreEqual("thing1", newThing1Block.Label); + Assert.AreNotSame(newThing1Block, oldThing1Block); + + var newThing2Block = newMain.Blocks[2]; + Assert.AreEqual("thing2", newThing2Block.Label); + Assert.AreNotSame(newThing2Block, oldThing2Block); + + // Now let's examine the gotos and make sure they point to the duplicated blocks. + var newEntryGotoCmd = newEntryBlock.TransferCmd as GotoCmd; + var newthing1GotoCmd = newThing1Block.TransferCmd as GotoCmd; + + Assert.AreNotSame(newEntryGotoCmd.labelTargets[0], oldThing1Block); + Assert.AreSame(newEntryGotoCmd.labelTargets[0], newThing1Block); + Assert.AreNotSame(newEntryGotoCmd.labelTargets[1], oldThing2Block); + Assert.AreSame(newEntryGotoCmd.labelTargets[1], newThing2Block); + + Assert.AreNotSame(newthing1GotoCmd.labelTargets[0], oldEntryBlock); + Assert.AreSame(newthing1GotoCmd.labelTargets[0], newEntryBlock); + Assert.AreNotSame(newthing1GotoCmd.labelTargets[1], oldThing1Block); + Assert.AreSame(newthing1GotoCmd.labelTargets[1], newThing1Block); + + } + + [Test()] + public void ImplementationProcedureResolving() { + Program p = TestUtil.ProgramLoader.LoadProgramFrom(@" + procedure main(a:int) returns (r:int); + requires a > 0; + ensures r > a; + + implementation main(a:int) returns (r:int) + { + r:= a + 1; + } + "); + + // Check resolved + var oldMainImpl = p.TopLevelDeclarations.OfType().Where(i => i.Name == "main").First(); + var oldMainProc = p.TopLevelDeclarations.OfType().Where(i => i.Name == "main").First(); + Assert.AreSame(oldMainImpl.Proc, oldMainProc); + + // Now duplicate the program + var newProgram = (Program) d.Visit(p); + + // Resolving doesn't seem to fix this. + var rc = new ResolutionContext(this); + newProgram.Resolve(rc); + + // Check resolved + var newMainImpl = newProgram.TopLevelDeclarations.OfType().Where(i => i.Name == "main").First(); + var newMainProc = newProgram.TopLevelDeclarations.OfType().Where(i => i.Name == "main").First(); + Assert.AreSame(newMainImpl.Proc, newMainProc); + } + + [Test()] + public void CallCmdResolving() { + Program p = TestUtil.ProgramLoader.LoadProgramFrom(@" + procedure main() + { + var x:int; + call x := foo(); + call x := bar(); + } + + procedure foo() returns(r:int) + { + r := 0; + } + + procedure bar() returns(r:int); + ensures r == 0; + "); + + // Get hold of the procedures that will be used with the CallCmd + var oldFoo = p.TopLevelDeclarations.OfType().Where(i => i.Name == "foo").First(); + var oldBar = p.TopLevelDeclarations.OfType().Where(i => i.Name == "bar").First(); + + // Get the CallCmds to foo and bar + var oldCmdsInMain = p.TopLevelDeclarations.OfType().Where(i => i.Name == "main").SelectMany(i => i.Blocks).SelectMany(b => b.Cmds); + var oldCallToFoo = oldCmdsInMain.OfType().Where(c => c.callee == "foo").First(); + var oldCallToBar = oldCmdsInMain.OfType().Where(c => c.callee == "bar").First(); + + // Check the Calls + Assert.AreSame(oldCallToFoo.Proc, oldFoo); + Assert.AreSame(oldCallToBar.Proc, oldBar); + + // Now duplicate the program and check that the calls are resolved correctly + var newProgram = (Program) d.Visit(p); + + var foo = newProgram.TopLevelDeclarations.OfType().Where(i => i.Name == "foo").First(); + var bar = newProgram.TopLevelDeclarations.OfType().Where(i => i.Name == "bar").First(); + + // Get the call to Foo + var cmdsInMain = newProgram.TopLevelDeclarations.OfType().Where(i => i.Name == "main").SelectMany(i => i.Blocks).SelectMany(b => b.Cmds); + var callToFoo = cmdsInMain.OfType().Where(c => c.callee == "foo").First(); + var callToBar = cmdsInMain.OfType().Where(c => c.callee == "bar").First(); + + // Check the Calls + Assert.AreNotSame(callToFoo.Proc, oldFoo); + Assert.AreSame(callToFoo.Proc, foo); + Assert.AreNotSame(callToBar.Proc, oldBar); + Assert.AreSame(callToBar.Proc, bar); + } + } +} + diff --git a/Source/UnitTests/CoreTests/ExprEquality.cs b/Source/UnitTests/CoreTests/ExprEquality.cs new file mode 100644 index 00000000..6bc049f5 --- /dev/null +++ b/Source/UnitTests/CoreTests/ExprEquality.cs @@ -0,0 +1,179 @@ +using Microsoft.Boogie; +using Microsoft.Basetypes; +using NUnit.Framework; +using System.Collections.Generic; +using System; + +namespace CoreTests +{ + [TestFixture()] + public class ExprEquality { + + [Test()] + public void LiteralBool() { + var constant = new LiteralExpr(Token.NoToken, false); + var constant2 = new LiteralExpr(Token.NoToken, false); + + Assert.AreNotSame(constant, constant2); // These are different references + + Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal" + Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + + [Test()] + public void LiteralBV() { + var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8; + var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8; + + Assert.AreNotSame(constant, constant2); // These are different references + + Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal" + Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + + [Test()] + public void LiteralInt() { + var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer + var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer + + Assert.AreNotSame(constant, constant2); // These are different references + + Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal" + Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + + [Test()] + public void LiteralReal() { + var constant = new LiteralExpr(Token.NoToken, BigDec.FromString("11.7")); // Real + var constant2 = new LiteralExpr(Token.NoToken, BigDec.FromString("11.7")); // Real + + Assert.AreNotSame(constant, constant2); // These are different references + + Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal" + Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + + [Test()] + public void SimpleAdd() { + var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer + var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(19)); // Integer + var add = Expr.Add(constant, constant2); + + var add2 = Expr.Add(constant, constant2); + + Assert.AreNotSame(constant, constant2); // These are different references + Assert.AreNotSame(add, add2); // These are different references + + Assert.IsTrue(add.Equals(add2)); // These are "structurally equal" + Assert.AreEqual(add.GetHashCode(), add2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + + [Test()] + public void SimpleIdentifierExprs() { + var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8))); + var idVar = new IdentifierExpr(Token.NoToken, variable); + var idVar2 = new IdentifierExpr(Token.NoToken, variable); + + Assert.AreNotSame(idVar, idVar2); // These are different references + + Assert.IsTrue(idVar.Equals(idVar2)); // These are "structurally equal" + Assert.AreEqual(idVar.GetHashCode(), idVar2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + + [Test()] + public void SimpleIdentifierVariables() { + var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8))); + var variable2 = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8))); + var idVar = new IdentifierExpr(Token.NoToken, variable); + var idVar2 = new IdentifierExpr(Token.NoToken, variable2); + + Assert.AreNotSame(idVar, idVar2); // These are different references + // These are not "structurally equal" because the Variable references are different (even though they have the same name and type) + Assert.IsFalse(idVar.Equals(idVar2)); + } + + [Test()] + public void SimpleBVConcat() { + var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8))); + var id = new IdentifierExpr(Token.NoToken, variable); + var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8; + var concat = new BvConcatExpr(Token.NoToken, id, constant); + + // Don't trust the Boogie duplicator here. Do it ourselves + var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8; + // We don't duplicate the variable because that is not an Expr and we require reference equality. + var id2 = new IdentifierExpr(Token.NoToken, variable); + var concat2 = new BvConcatExpr(Token.NoToken, id2, constant2); + + Assert.AreNotSame(concat, concat2); // These are different references + + Assert.IsTrue(concat.Equals(concat2)); // These are "structurally equal" + Assert.AreEqual(concat.GetHashCode(), concat2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + + [Test()] + public void SimpleBVExtract() { + var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8))); + var id = new IdentifierExpr(Token.NoToken, variable); + + var extract = new BvExtractExpr(Token.NoToken, id, 5, 0); // 4-bits + + var id2 = new IdentifierExpr(Token.NoToken, variable); + var extract2 = new BvExtractExpr(Token.NoToken, id2, 5, 0); + + Assert.AreNotSame(extract, extract2); + + Assert.IsTrue(extract.Equals(extract2)); + Assert.AreEqual(extract.GetHashCode(), extract2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + + [Test()] + public void SimpleForAll() { + var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool)); + var id = new IdentifierExpr(Token.NoToken, boundVar); + var forall = new ForallExpr(Token.NoToken, new List() { boundVar }, id); + + var id2 = new IdentifierExpr(Token.NoToken, boundVar); + var forall2 = new ForallExpr(Token.NoToken, new List() { boundVar }, id2); + + Assert.AreNotSame(forall, forall2); // These are different references + + Assert.IsTrue(forall.Equals(forall2)); // These are "structurally equal" + Assert.AreEqual(forall.GetHashCode(), forall2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + + + [Test()] + public void SimpleExists() { + var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool)); + var id = new IdentifierExpr(Token.NoToken, boundVar); + var exists = new ExistsExpr(Token.NoToken, new List() { boundVar }, id); + + var id2 = new IdentifierExpr(Token.NoToken, boundVar); + var exists2 = new ExistsExpr(Token.NoToken, new List() { boundVar }, id2); + + Assert.AreNotSame(exists, exists2); // These are different references + + Assert.IsTrue(exists.Equals(exists2)); // These are "structurally equal" + Assert.AreEqual(exists.GetHashCode(), exists2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + + [Test()] + public void SimpleLambda() { + var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool)); + var id = new IdentifierExpr(Token.NoToken, boundVar); + + // This is basically an Identity Map + var lambdaExpr = new LambdaExpr(Token.NoToken, new List() , new List() { boundVar }, null, id); + + var id2 = new IdentifierExpr(Token.NoToken, boundVar); + var lambdaExpr2 = new LambdaExpr(Token.NoToken, new List() , new List() { boundVar }, null, id2); + + Assert.AreNotSame(lambdaExpr, lambdaExpr2); // These are different references + + Assert.IsTrue(lambdaExpr.Equals(lambdaExpr2)); // These are "structurally equal" + Assert.AreEqual(lambdaExpr.GetHashCode(), lambdaExpr2.GetHashCode()); // If the .Equals() is true then hash codes must be the same + } + } +} + diff --git a/Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs b/Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..fb965517 --- /dev/null +++ b/Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("CoreTests")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("")] +[assembly: AssemblyProduct("CoreTests")] +[assembly: AssemblyCopyright("Copyright © 2014")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("5c6f8617-e212-4ab7-bce6-5b1a930fa2b8")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("1.0.*")] +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/Source/UnitTests/CoreTests/packages.config b/Source/UnitTests/CoreTests/packages.config new file mode 100644 index 00000000..d4e241a2 --- /dev/null +++ b/Source/UnitTests/CoreTests/packages.config @@ -0,0 +1,4 @@ + + + + \ No newline at end of file diff --git a/Source/UnitTests/README.md b/Source/UnitTests/README.md new file mode 100644 index 00000000..5e70bc18 --- /dev/null +++ b/Source/UnitTests/README.md @@ -0,0 +1,55 @@ +Unit testing infrastructure +=========================== + +Boogie uses [NUnit](http://www.nunit.org/) unit test framework. +We currently use NUnit 2.6.3, which was the latest stable +version available at the time of writing. + + +Installing NUnit +================ + +NUnit should be installed via [NuGet](https://www.nuget.org/) package manager. + +The NuGet client is available as + +* An extension to Visual Studio +* An add-in in Monodevelop +* A command line utility from the NuGet website + +Note Mono ships with an old version of NUnit (2.4.8) which will cause +compilation issues. To fix this you must install NUnit via NuGet. + + +Running the tests +================= + +Command line +------------ + +The ``run-unittests.py`` python script in the root directory of the project can be used to run the unit tests on the command line. This script is a simple wrapper for ``nunit-console.exe``. + +``` +$ python run-unittests.py Release +``` + +Run the following to see all the available options + +``` +$ python run-unittests.py --help +``` + +Monodevelop +----------- + +Monodevelop has built in support for running NUnit tests. Goto the "Unit Tests" +panel and click "Run All". + +Visual Studio +------------- + +Visual studio needs the "NUnit Test Adapter for VS2012 and VS2013" add-in to be installed (Tools > Extensions and Updates). Once that is installed you can run unit tests by going + +1. Going to the Test Explorer (TEST > Windows > Test Explorer) +2. Clicking on "Run All" in the Test Explorer. + diff --git a/Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs b/Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs new file mode 100644 index 00000000..961ed0df --- /dev/null +++ b/Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs @@ -0,0 +1,27 @@ +using NUnit.Framework; +using System; +using System.Diagnostics; + +namespace Microsoft.Boogie +{ + namespace TestUtil + { + + public class AssertionTextWriterTraceListener : TextWriterTraceListener { + public AssertionTextWriterTraceListener(System.IO.Stream stream) : base(stream) { } + + public AssertionTextWriterTraceListener(System.IO.TextWriter writer) : base(writer) { } + + public override void Fail(string message) { + base.Fail(message); + Assert.Fail(message); + } + + public override void Fail(string message, string detailMessage) { + base.Fail(message, detailMessage); + Assert.Fail(message + " : " + detailMessage); + } + } + } +} + diff --git a/Source/UnitTests/TestUtil/BoogieTestBase.cs b/Source/UnitTests/TestUtil/BoogieTestBase.cs new file mode 100644 index 00000000..2bac71a4 --- /dev/null +++ b/Source/UnitTests/TestUtil/BoogieTestBase.cs @@ -0,0 +1,24 @@ +using NUnit.Framework; +using System; +using System.Diagnostics; +using Microsoft.Boogie; + +namespace Microsoft.Boogie +{ + namespace TestUtil + { + public class BoogieTestBase { + + public BoogieTestBase() { + // Debug log output goes to standard error. + // Failing System.Diagnostics failures trigger NUnit assertion failures + Debug.Listeners.Add(new AssertionTextWriterTraceListener(Console.Error)); + + // FIXME: THIS IS A HACK. Boogie's methods + // depend on its command line parser being set! + CommandLineOptions.Install(new Microsoft.Boogie.CommandLineOptions()); + } + } + } +} + diff --git a/Source/UnitTests/TestUtil/ProgramLoader.cs b/Source/UnitTests/TestUtil/ProgramLoader.cs new file mode 100644 index 00000000..bc5f647a --- /dev/null +++ b/Source/UnitTests/TestUtil/ProgramLoader.cs @@ -0,0 +1,33 @@ +using NUnit.Framework; +using System; +using Microsoft.Boogie; + +namespace TestUtil +{ + public class ProgramLoader + { + public static Program LoadProgramFrom(string programText, string fileName="file.bpl") + { + Assert.IsNotNullOrEmpty (programText); + Assert.IsNotNullOrEmpty (fileName); + + + int errors = 0; + Program p = null; + errors = Parser.Parse(programText, fileName, out p, /*useBaseName=*/false); + Assert.AreEqual(0, errors); + Assert.IsNotNull(p); + + // Resolve + errors = p.Resolve(); + Assert.AreEqual(0, errors); + + // Type check + errors = p.Typecheck(); + Assert.AreEqual(0, errors); + + return p; + } + } +} + diff --git a/Source/UnitTests/TestUtil/Properties/AssemblyInfo.cs b/Source/UnitTests/TestUtil/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..05c9fee5 --- /dev/null +++ b/Source/UnitTests/TestUtil/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("TestUtil")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("")] +[assembly: AssemblyProduct("TestUtil")] +[assembly: AssemblyCopyright("Copyright © 2014")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("5630b725-b802-4f97-9e46-6cdfd6819269")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("1.0.*")] +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/Source/UnitTests/TestUtil/TestUtil.csproj b/Source/UnitTests/TestUtil/TestUtil.csproj new file mode 100644 index 00000000..7642b134 --- /dev/null +++ b/Source/UnitTests/TestUtil/TestUtil.csproj @@ -0,0 +1,71 @@ + + + + + Debug + AnyCPU + {59118E35-4236-495E-AF6E-0D641302ED2C} + Library + Properties + TestUtil + TestUtil + v4.5 + 512 + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + + ..\..\packages\NUnit.2.6.3\lib\nunit.framework.dll + + + + + + + + + + + + + + + + + + + + + {b230a69c-c466-4065-b9c1-84d80e76d802} + Core + + + {fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5} + ParserHelper + + + + + \ No newline at end of file diff --git a/Source/UnitTests/TestUtil/packages.config b/Source/UnitTests/TestUtil/packages.config new file mode 100644 index 00000000..d4e241a2 --- /dev/null +++ b/Source/UnitTests/TestUtil/packages.config @@ -0,0 +1,4 @@ + + + + \ No newline at end of file diff --git a/Source/UnitTests/run-unittests.py b/Source/UnitTests/run-unittests.py new file mode 100644 index 00000000..be906edd --- /dev/null +++ b/Source/UnitTests/run-unittests.py @@ -0,0 +1,124 @@ +#!/usr/bin/env python +""" +This is a simple script to invoke nunit-console.exe +on Windows or Linux on all UnitTest libraries. +""" +import argparse +import logging +import os +import subprocess +import sys + +class ReturnCode: + SUCCESS = 0 + CONFIG_ERROR = 1 + RUN_ERROR = 2 + + +def main(args): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('BuildType', choices=['Release', 'Debug'], + help='Build type of unit test libraries') + parser.add_argument('-l','--log-level', + choices=['critical', 'error', 'warning', 'info', 'debug'], + default='info', + dest='log_level', + help='Logging level. Default %(default)s') + parser.add_argument('--nunit-console-path', default='', + help='Path to nunit-console tool. If not set the script will try to guess its location', + dest='nunit_console_path' + ) + parser.add_argument('-e', '--nunit-console-extra-args', action='append', + help='Pass extra arguments to nunit-console. This can be used multiple times', + default=[], + dest='nunit_console_extra_args' + ) + parser.add_argument('--no-progress', + action='store_true', + dest='no_progress', + help='Suppress nunit-console progress information') + + + parsedArgs = parser.parse_args(args) + logging.basicConfig(level=getattr(logging, parsedArgs.log_level.upper())) + buildType=parsedArgs.BuildType + + logging.info('Build type is {}'.format(buildType)) + + if parsedArgs.no_progress: + parsedArgs.nunit_console_extra_args.append('-nodots') + + logging.info('Extra arguments to nunit-console "{}"'.format(parsedArgs.nunit_console_extra_args)) + + UnitTestDirRoot = os.path.dirname(os.path.abspath(__file__)) + + # Find nunit-console.exe + if parsedArgs.nunit_console_path == "": + # Try to guess where the tool is + nunitConsolePath = os.path.join(os.path.join(UnitTestDirRoot,'..'), + "packages", + "NUnit.Runners.2.6.3", + "tools", + "nunit-console.exe" + ) + # Mono needs the path to be absolute + nunitConsolePath = os.path.abspath(nunitConsolePath) + else: + nunitConsolePath = parsedArgs.nunit_console_path + + logging.info('Looking for NUnit console at "{}"'.format(nunitConsolePath)) + if not os.path.exists(nunitConsolePath): + logging.error('Could not find NUnit console tool') + return ReturnCode.CONFIG_ERROR + + # Find unit test libraries + unitTestLibraries = [ ] + logging.info('Searching for Unit test libraries in "{}"'.format(UnitTestDirRoot)) + for (dirpath, dirnames, filenames) in os.walk(UnitTestDirRoot): + + # Search current directory for dll with correct suffix + for filename in filenames: + if filename.endswith('Tests.dll'): + logging.debug('Found "{}" checking build type'.format(filename)) + + pathComponents = dirpath.split(os.path.sep) + fullPath = os.path.join(dirpath, filename) + try: + buildTypeIndex = pathComponents.index(buildType) + if buildTypeIndex == 0 or pathComponents[buildTypeIndex -1] != 'bin': + continue + + logging.info('Using "{}"'.format(fullPath)) + unitTestLibraries.append(fullPath) + except ValueError: + pass + + # Run Unit tests + if len(unitTestLibraries) == 0: + logging.error('No Unit test libraries were found') + return ReturnCode.CONFIG_ERROR + + cmd = [] + + if os.name == 'posix': + cmd.append('mono') + + cmd.extend([nunitConsolePath, '-nologo']) + + if len(parsedArgs.nunit_console_extra_args) > 0: + cmd.extend(parsedArgs.nunit_console_extra_args) + + cmd.extend(unitTestLibraries) + logging.info('Running "{}"'.format(cmd)) + exitCode = subprocess.call(cmd) + if exitCode != 0: + logging.error('FAILED!') + return ReturnCode.RUN_ERROR + else: + logging.info('Succeeded') + + return ReturnCode.SUCCESS + + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) -- cgit v1.2.3