Generate test data for C# unit

Nowadays, many projects are developed by using C#. As the projects grow bigger and bigger, the test effort becomes enormous. As a result, the need for automation testing for such projects become higher and higher. In this post, I share one of an approach for generating test data for C# projects automatically. This will dramatically increase the test effectiveness and reduce test effort for projects. The key idea of the method is to use abstract syntax tree (AST) to generate test data for a C# unit. From the generated AST, we can generate test data for test paths, do a lot of interesting things for the selected project such as calculating code coverage, making code instrumentation, etc. 

The first step of the method is to read all source code for the project we want to generate test data for. Assume that we have such source code stored in a string variable as follows.

using System;

using System.Collections.Generic;

using System.Linq;

using System.Text;

using System.Threading.Tasks;

 

namespace SampleCode

{

    class Program

    {

        static void Main(string[] args)

        {

        }

    }

 

    public class Student

    {

        Teacher _teacher;

        public Student()

        {

 

        }

        public string Name { get; set; }

        public string Age { get; set; }

        public Teacher Teacher { get => _teacher; set => _teacher = value; }

 

    }

    public class Teacher

    {

        public Teacher()

        {

 

        }

        public string Name { get; set; }

        public string Degree { get; set; }

    }

}

 The sample code below will guide you on how to get the list of classes declared in the project. Later, you can do related things such as finding methods, properties, declarations, generating test paths, test data, etc. from your code.

using Microsoft.CodeAnalysis;

using Microsoft.CodeAnalysis.CSharp;

using Microsoft.CodeAnalysis.CSharp.Syntax;

using System;

using System.Collections.Generic;

using System.ComponentModel;

using System.Data;

using System.Drawing;

using System.Linq;

using System.Text;

using System.Threading.Tasks;

using System.Windows.Forms;

 

namespace AST4CSharp

{

    public partial class Form1 : Form

    {

        public Form1()

        {

            InitializeComponent();

        }

 

        private void Form1_Load(object sender, EventArgs e)

        {

            string sourceCode =

                @"using System;

                using System.Collections.Generic;

                using System.Linq;

                using System.Text;

                using System.Threading.Tasks;

 

                namespace SampleCode

                {

                    class Program

                    {

                        static void Main(string[] args)

                        {

                        }

                    }

 

                    public class Student

                    {

                        Teacher _teacher;

                        public Student()

                        {

 

                        }

                        public string Name { get; set; }

                        public string Age { get; set; }

                        public Teacher Teacher { get => _teacher; set => _teacher = value; }

 

                    }

                    public class Teacher

                    {

                        public Teacher()

                        {

 

                        }

                        public string Name { get; set; }

                        public string Degree { get; set; }

                    }

                }";

 

            SyntaxTree tree = CSharpSyntaxTree.ParseText(sourceCode);

            CompilationUnitSyntax root = tree.GetCompilationUnitRoot();

 

            var finder = new ClassFinder();

            finder.Visit(root);

 

            foreach (var c in finder.classes)

            {

                Console.WriteLine(c.Identifier.Text);

            }

        }

 

        public class ClassFinder : CSharpSyntaxWalker

        {

            public ICollection<ClassDeclarationSyntax> classes { get; } = new List<ClassDeclarationSyntax>();

 

            public override void VisitClassDeclaration(ClassDeclarationSyntax node)

            {

 

                classes.Add(node);

 

                base.VisitClassDeclaration(node);

            }

        }

    }

}

 The result of the above source code is shown below.

Program

Student

Teacher

Java - Windows Intellij: Configure Microsoft z3

When I start configuring Microsoft Z3 solver for Java and for Intellij, I have a lot of difficulties. Here is some important points you must take care of to make it work.

• Download Microsoft Z3 and save it to your folder. e.g: C:\z3-4.8.8-x64-win. Remember the fitness of Z3 must be the same as Java virtual machine. I used the 64-bit version.
• Copy com.microsoft.z3.jar to your libs folder inside the project and add it as a library.
• I get the sample from this link: https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java

package solver;

import com.microsoft.z3.*;

public class z3solver {
    public z3solver() {

    }

    public static void main(String[] args) throws Exception {

//        System.loadLibrary("E:\\Vie" +"t" + "Data\\Th" + "ay Hung\\DSE\\libs\\z3-4.8.8-x64-win\\bin\\lib" + "z3java.dll");
        z3solver solver = new z3solver();
        solver.quantifierExample1();
    }

    public void simpleExample() {
        System.out.println("SimpleExample");
        Log.append("SimpleExample");

        {
            Context ctx = new Context();
            /* do something with the context */

            /* be kind to dispose manually and not wait for the GC. */
            ctx.close();
        }
    }

    void quantifierExample1() {
        try
        {
            Context ctx = new Context();

            System.out.println("QuantifierExample");
//            Log.append("QuantifierExample");

            Sort[] types = new Sort[3];
            IntExpr[] xs = new IntExpr[3];
            Symbol[] names = new Symbol[3];
            IntExpr[] vars = new IntExpr[3];

            for (int j = 0; j < 3; j++) {
                types[j] = ctx.getIntSort();
                names[j] = ctx.mkSymbol("x_" + Integer.toString(j));
                xs[j] = (IntExpr) ctx.mkConst(names[j], types[j]);
                vars[j] = (IntExpr) ctx.mkBound(2 - j, types[j]); // <-- vars
                // reversed!
            }

            Expr body_vars = ctx.mkAnd(
                    ctx.mkEq(ctx.mkAdd(vars[0], ctx.mkInt(1)), ctx.mkInt(2)),
                    ctx.mkEq(ctx.mkAdd(vars[1], ctx.mkInt(2)),
                            ctx.mkAdd(vars[2], ctx.mkInt(3))));

            Expr body_const = ctx.mkAnd(
                    ctx.mkEq(ctx.mkAdd(xs[0], ctx.mkInt(1)), ctx.mkInt(2)),
                    ctx.mkEq(ctx.mkAdd(xs[1], ctx.mkInt(2)),
                            ctx.mkAdd(xs[2], ctx.mkInt(3))));

            Expr x = ctx.mkForall(types, names, body_vars, 1, null, null,
                    ctx.mkSymbol("Q1"), ctx.mkSymbol("skid1"));
            System.out.println("Quantifier X: " + x.toString());

            Expr y = ctx.mkForall(xs, body_const, 1, null, null,
                    ctx.mkSymbol("Q2"), ctx.mkSymbol("skid2"));
            System.out.println("Quantifier Y: " + y.toString());

        }
        catch (Exception ex)
        {

        }
    }

    Model check(Context ctx, BoolExpr f, Status sat) throws Exception {
        Solver s = ctx.mkSolver();
        s.add(f);
        if (s.check() != sat)
            throw new Exception();
        if (sat == Status.SATISFIABLE)
            return s.getModel();
        else
            return null;
    }
}

• Build the project successfully, but then I get the error.

Connected to the target VM, address: '127.0.0.1:54691', transport: 'socket'

Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path

at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1860)

at java.lang.Runtime.loadLibrary0(Runtime.java:870)

at java.lang.System.loadLibrary(System.java:1122)

at com.microsoft.z3.Native.<clinit>(Native.java:14)

at com.microsoft.z3.Context.<init>(Context.java:41)

at solver.z3solver.quantifierExample1(z3solver.java:33)

at solver.z3solver.main(z3solver.java:14)

Disconnected from the target VM, address: '127.0.0.1:54691', transport: 'socket'

• You must understand that Java takes care of the build so using the import com.microsoft.z3.*; command is enough, but when running, you must provide java.library.path to the library of Z3 so it knows where the library is. You can do this by go to Run --> Edit Configurations --> VM options: Add this command: -Djava.library.path="C:\z3-4.8.8-x64-win\bin\". If your path have the last "\", VM still complains as follows:

Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path

at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1860)

at java.lang.Runtime.loadLibrary0(Runtime.java:870)

at java.lang.System.loadLibrary(System.java:1122)

at com.microsoft.z3.Native.<clinit>(Native.java:14)

at com.microsoft.z3.Context.<init>(Context.java:41)

at solver.z3solver.quantifierExample1(z3solver.java:33)

at solver.z3solver.main(z3solver.java:14)

Disconnected from the target VM, address: '127.0.0.1:53632', transport: 'socket'

• You must remove the last "\" from the path, VM will understand it. So the last and successful will be: -Djava.library.path="C:\z3-4.8.8-x64-win\bin". However, now you will have the following error.

Exception in thread "main" java.lang.UnsatisfiedLinkError: C:\z3-4.8.8-x64-win\bin\libz3java.dll: Can't find dependent libraries

at java.lang.ClassLoader$NativeLibrary.load(Native Method)

at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1934)

at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1850)

at java.lang.Runtime.loadLibrary0(Runtime.java:870)

at java.lang.System.loadLibrary(System.java:1122)

at com.microsoft.z3.Native.<clinit>(Native.java:14)

at com.microsoft.z3.Context.<init>(Context.java:41)

at solver.z3solver.quantifierExample1(z3solver.java:33)

at solver.z3solver.main(z3solver.java:14)

Disconnected from the target VM, address: '127.0.0.1:56441', transport: 'socket'

• Now I copy all the folder of Z3 to my libs folder. remove the previous com.microsoft.z3.jar from the libs folder. Add the new one com.microsoft.z3.jar as a library. Now I must edit the Run configurations. so it is: -Djava.library.path="My path\libs\z3-4.8.8-x64-win\bin"

• Now you can run the sample code without problem.

Connected to the target VM, address: '127.0.0.1:58074', transport: 'socket'

QuantifierExample

Quantifier X: (forall ((x_0 Int) (x_1 Int) (x_2 Int))

  (! (and (= (+ x_0 1) 2) (= (+ x_1 2) (+ x_2 3))) :skolemid skid1 :qid Q1))

Quantifier Y: (forall ((x_0 Int) (x_1 Int) (x_2 Int))

  (! (and (= (+ x_0 1) 2) (= (+ x_1 2) (+ x_2 3))) :skolemid skid1 :qid Q1))