V# Symbolic Execution Engine

V# is a symbolic execution engine for .NET binaries, performing completely automated and unassisted test generation for .NET assemblies. It is cross-platform and supports .NET, .NET Core and .NET Framework assemblies.

Requirements

.NET 6 or greater

How to build

Clone the repository and run dotnet publish -c Release from the root directory

Testing a small function

1. Using NUnit and V# API

Create an empty NUnit test project DemoProject and insert the following code:

usingSystem;usingNUnit.Framework;namespaceDemoProject{publicstaticclassDemoClass{publicstaticintAbs(intx){inty=x;if(x<0)y=-x;if(y<0)thrownewException("What?");returny;}}publicclassTests{[Test]publicvoidTest1(){varsuccess=VSharp.TestGenerator.CoverAndRun(typeof(DemoClass));Assert.IsTrue(success);}}}

Add reference to VSharp.API.dll assembly (<V# build directory>/VSharp.API/bin/Release/netcoreapp6.0/publish/VSharp.API.dll). Set the Debug build type for DemoProject and place the break points into all then branches of conditions and return statement of Abs.

Run Test1 in debug mode. If it throws TypeInitializationException, then also copy native Z3 library to destination directory of DemoProject (this will be fixed in future versions) and rerun the test. Native Z3 library can be found in <V# build directory>/VSharp.API/bin/Release/netcoreapp6.0/publish/runtimes/<platform>/native.

The test will generate two unit tests for Abs function and run all the tests. You will sequentially see one value that gets into the then branch first of the first condition and INT_MIN value which takes the Abs function throwing the exception.

Run the test coverage measurement tool to be sure the exhaustiveness of the generated test coverage. The generated tests can be found in DemoProject working directory, in VSharp.tests.0 subfolder.

2. Using console runner

Create an empty class library project DemoProject2 and insert the following code:

namespaceDemoProject2{publicclassCustomer{publicintId{get;set;}publicstringName{get;set;}publicstringCity{get;set;}publicoverrideboolEquals(Objectother){if(otherisCustomerotherCustomer){returnotherCustomer.Id==this.Id;}returnfalse;}publicoverrideintGetHashCode(){returnHashCode.Combine(Id,Name,City);}}publicclassDemoClass2{privateCustomer_customer;publicboolIsOurCustomer(Customerother){if(other.Equals(_customer)){returntrue;}returnfalse;}}}

Compile this project. Run

dotnet VSharp.Runner/bin/Release/netcoreapp6.0/publish/VSharp.Runner.dll --public-methods-of-class DemoProject2.DemoClass2 <path to DemoProject2.dll>

The engine will generate *.vst unit tests into the fresh directory VSharp.tests.0.

To run the generated tests, print

dotnet VSharp.TestRunner/bin/Release/netcoreapp6.0/publish/VSharp.TestRunner.dll VSharp.tests.0

This command will run the IsOurCustomer function on different instances of DemoClass2 and other parameter generated by symbolic execution engine.

To measure the code coverage with JetBrains.dotCover, first install the coverage tool by running dotnet tool install JetBrains.dotCover.GlobalTool. Now you can generate the test coverage report by running

dotnet dotcover --dcFilters="-:module=Microsoft.*;-:module=FSharp.*;-:class=VSharp.*;-:module=VSharp.Utils" VSharp.TestRunner.dll VSharp.tests.0 --dcReportType=DetailedXML

The coverage report will be generated into the dotCover.Output.xml file. Enjoy the exhaustive test coverage!

3. Further exploration

Explore our integration testing programs codebase. Try V# on your programs!

Current state

The project is currently in active development stage and yet unreleased. If you encounter the problem, consider submitting the issue.

License

The project is licensed under the Apache License Version 2.0