# QuickChickToolThe QuickChick Command-Line Tool

# Overview

- Batch processing, compilation and execution of tests
- Mutation testing
- Sectioning of tests and mutants

quickChick -color -top Stack

Testing base...or

Testing mutant 2 (./Exp.v: line 20): Plus-copy-paste-errorLet's take a closer look at the first one.

Testing base... make -f Makefile.coq make[1]: Entering directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' COQDEP VFILES COQC Exp.v COQC Stack.v COQC QuickChickTop.v make[1]: Leaving directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' Checking Exp.optimize_correct_prop... +++ Passed 10000 tests (0 discards) Checking Stack.compiles_correctly... +++ Passed 10000 tests (0 discards)

*separate*OCaml modules, which are in turn compiled using ocamlbuild, and then run. The separate extraction into distinct ocaml modules allows us to reuse compilation effort across different mutants as well as different calls to quickChick, as we can identify whether newly extracted modules are actually different and recompile them or not accordingly!

*mutated*code. We will see exactly what mutation testing is later in this chapter.

All tests produced the expected results

# Arithmetic Expressions

*section declaration*:

(*! Section arithmetic_expressions *)

Inductive exp : Type :=

| ANum : nat → exp

| APlus : exp → exp → exp

| AMinus : exp → exp → exp

| AMult : exp → exp → exp.

| ANum : nat → exp

| APlus : exp → exp → exp

| AMinus : exp → exp → exp

| AMult : exp → exp → exp.

Since exp is a simple datatype, QuickChick can derive a generator, a
shrinker, and a printer automatically.

Derive (Arbitrary, Show) for exp.

The eval function evaluates an expression to a number.

Fixpoint eval (e : exp) : nat :=

match e with

| ANum n ⇒ n

| APlus e

| AMinus e

| AMult e

end.

match e with

| ANum n ⇒ n

| APlus e

_{1}e_{2}⇒ (eval e_{1}) + (eval e_{2})| AMinus e

_{1}e_{2}⇒ (eval e_{1}) - (eval e_{2})| AMult e

_{1}e_{2}⇒ (eval e_{1}) * (eval e_{2})end.

(The actual definition in the file Exp.v contains a few more
annotations in comments, defining a
Now let's write a simple optimization: whenever we see an
unnecessary operation (adding/subtracting 0) we optimize it
away.

*mutant*. We will discuss these annotations later in this chapter.
Fixpoint optimize (e : exp) : exp :=

match e with

| ANum n ⇒ ANum n

| APlus e (ANum 0) ⇒ optimize e

| APlus (ANum 0) e ⇒ optimize e

| APlus e

| AMinus e (ANum 0) ⇒ optimize e

| AMinus e

| AMult e

end.

match e with

| ANum n ⇒ ANum n

| APlus e (ANum 0) ⇒ optimize e

| APlus (ANum 0) e ⇒ optimize e

| APlus e

_{1}e_{2}⇒ APlus (optimize e_{1}) (optimize e_{2})| AMinus e (ANum 0) ⇒ optimize e

| AMinus e

_{1}e_{2}⇒ AMinus (optimize e_{1}) (optimize e_{2})| AMult e

_{1}e_{2}⇒ AMult (optimize e_{1}) (optimize e_{2})end.

Again, the actual definition in Exp.v contains again a few more
annotations in comments (another section annotation and another
mutant).
We can now write a simple correctness property for the optimizer,
namely that evaluating an optimized expression yields the same
number as evaluating the original one.

Definition optimize_correct_prop (e : exp) := eval (optimize e) = eval e?.

(*! QuickChick optimize_correct_prop. *)

QuickChecking optimize_correct_prop +++ Passed 10000 tests (0 discards)

# QuickChick Test Annotations

*single*extraction and compilation pass, and report the results for all tests. This is achieved with special QuickChick annotations.

*Comments that begin with an exclamation mark are special to the QuickChick command-line tool parser and signify a test, a section, or a mutant*.

*named*property, like optimize_correct_prop. That is, while inline one could successfully execute a command like the one below, the command-line tool requires a defined constant in the test annotation.

QuickChick (fun e ⇒ eval (optimize e) = eval e?).

# Sections

(*! Section arithmetic_expressions *)

The second also includes an extends clause.
(*! Section optimizations *)(*! extends arithmetic_expressions *)

This signifies that this new block (until the end of the file,
in this case, since there are no further section headers), also
contains all tests and mutants from the arithmetic_expressions
section as well.
quickChick -color -top Stack -s optimizations

Testing base... make -f Makefile.coq make[1]: Entering directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' COQDEP VFILES COQC Exp.v COQC Stack.v COQC QuickChickTop.v make[1]: Leaving directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' Checking Exp.optimize_correct_prop... +++ Passed 10000 tests (0 discards) ... etc ...

# Mutation Testing

*mutation testing*.

(*! *)

| APlus e

(*!! Plus-copy-paste-error *)

(*! | APlus e

Let's break it down into its parts.
| APlus e

_{1}e_{2}⇒ (eval e_{1}) + (eval e_{2})(*!! Plus-copy-paste-error *)

(*! | APlus e

_{1}e_{2}=> (eval e_{1}) + (eval e_{1}) *)
(*! *)

This is followed by the correct code. In our example, by the evaluation
of APlus e_{1}e

_{2}.

(*!! Plus-copy-paste-error *)

_{1}twice as both operands in an addition.

(*! *)

| AMinus e (ANum 0) ⇒ optimize e

(*!! Minus-Reverse *)

(*!

| AMinus (ANum 0) e => optimize e

*)

This bug allows the optimization of 0-e to e instead of e-0 to e.
| AMinus e (ANum 0) ⇒ optimize e

(*!! Minus-Reverse *)

(*!

| AMinus (ANum 0) e => optimize e

*)

quickChick -color -top Stack -s optimizations

Testing mutant 0 (./Exp.v: line 35): Minus-Reverse make -f Makefile.coq make[1]: Entering directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' COQDEP VFILES COQC Exp.v COQC Stack.v COQC QuickChickTop.v make[1]: Leaving directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' AMinus (ANum 0) (ANum 1) Checking Exp.optimize_correct_prop... *** Failed after 13 tests and 4 shrinks. (0 discards) Testing mutant 1 (./Exp.v: line 20): Plus-copy-paste-error make -f Makefile.coq make[1]: Entering directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' COQDEP VFILES COQC Exp.v COQC Stack.v COQC QuickChickTop.v make[1]: Leaving directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' APlus (ANum 1) (ANum 0) Checking Exp.optimize_correct_prop... *** Failed after 5 tests and 3 shrinks. (0 discards) All tests produced the expected results

*extends*the arithmetic_expressions section, the mutants from both sections will be included. As expected, the optimize property fails in both cases.

# A Low-Level Stack Machine

Inductive sinstr : Type :=

| SPush : nat → sinstr

| SPlus : sinstr

| SMinus : sinstr

| SMult : sinstr.

| SPush : nat → sinstr

| SPlus : sinstr

| SMinus : sinstr

| SMult : sinstr.

Then we describe how to execute the stack machine.

Fixpoint execute (stack : list nat) (prog : list sinstr) : list nat :=

match (prog, stack) with

| (nil, _ ) ⇒ stack

| (SPush n::prog', _ ) ⇒ execute (n::stack) prog'

| (SPlus::prog', m::n::stack') ⇒ execute ((m+n)::stack') prog'

| (SMinus::prog', m::n::stack') ⇒ execute ((m-n)::stack') prog'

| (SMult::prog', m::n::stack') ⇒ execute ((m*n)::stack') prog'

| (_::prog', _ ) ⇒ execute stack prog'

end.

match (prog, stack) with

| (nil, _ ) ⇒ stack

| (SPush n::prog', _ ) ⇒ execute (n::stack) prog'

| (SPlus::prog', m::n::stack') ⇒ execute ((m+n)::stack') prog'

| (SMinus::prog', m::n::stack') ⇒ execute ((m-n)::stack') prog'

| (SMult::prog', m::n::stack') ⇒ execute ((m*n)::stack') prog'

| (_::prog', _ ) ⇒ execute stack prog'

end.

Given the current stack (a list of natural numbers) and the
program to be executed, we will produce a resulting stack.
Now we can compile expressions to their corresponding
stack-instruction sequences.

- If prog is empty, we return the current stack.
- To Push an integer, we cons it in the front of the list and execute the remainder of the program.
- To perform an arithmetic operation, we expect two integers at the top of the stack, operate, push the result, and execute the remainder of the program.
- Finally, if such a thing is not possible (i.e. we tried to perform a binary operation with less than 2 elements on the stack), we ignore the instruction and proceed to the rest.

Fixpoint compile (e : exp) : list sinstr :=

match e with

| ANum n ⇒ [SPush n]

| APlus e

| AMinus e

| AMult e

end.

match e with

| ANum n ⇒ [SPush n]

| APlus e

_{1}e_{2}⇒ compile e_{1}++ compile e_{2}++ [SPlus]| AMinus e

_{1}e_{2}⇒ compile e_{1}++ compile e_{2}++ [SMinus]| AMult e

_{1}e_{2}⇒ compile e_{1}++ compile e_{2}++ [SMult]end.

In the compilation above we have made a rookie compiler-writer
mistake. (Can you spot it without running QuickChick?)
The property we would expect to hold is that executing the
compiled instruction sequence of a given expression e, would
result in a single element stack with eval e as its only
element.

Definition compiles_correctly (e : exp) := (execute [] (compile e)) = [eval e]?.

(*! QuickChick compiles_correctly. *)

(*! QuickChick compiles_correctly. *)

===>

QuickChecking compiles_correctly

AMinus (ANum 0) (ANum 1)

*** Failed after 3 tests and 2 shrinks. (0 discards)

QuickChecking compiles_correctly

AMinus (ANum 0) (ANum 1)

*** Failed after 3 tests and 2 shrinks. (0 discards)

Fixpoint compile (e : exp) : list sinstr :=

match e with

| ANum n ⇒ [SPush n]

(*! *)

| APlus e

| AMinus e

| AMult e

(*!! Wrong associativity *)

(*!

| APlus e

| AMinus e

| AMult e

*)

end.

match e with

| ANum n ⇒ [SPush n]

(*! *)

| APlus e

_{1}e_{2}⇒ compile e_{2}++ compile e_{1}++ [SPlus]| AMinus e

_{1}e_{2}⇒ compile e_{2}++ compile e_{1}++ [SMinus]| AMult e

_{1}e_{2}⇒ compile e_{2}++ compile e_{1}++ [SMult](*!! Wrong associativity *)

(*!

| APlus e

_{1}e_{2}=> compile e_{1}++ compile e_{2}++ SPlus| AMinus e

_{1}e_{2}=> compile e_{1}++ compile e_{2}++ SMinus| AMult e

_{1}e_{2}=> compile e_{1}++ compile e_{2}++ SMult*)

end.

quickChick -color -top Stack -s stack

Testing base... make -f Makefile.coq make[1]: Entering directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' COQDEP VFILES COQC Exp.v COQC Stack.v COQC QuickChickTop.v make[1]: Leaving directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' Checking Stack.compiles_correctly... +++ Passed 10000 tests (0 discards) Testing mutant 0 (./Stack.v: line 33): Wrong associativity make -f Makefile.coq make[1]: Entering directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' COQDEP VFILES COQC Stack.v COQC QuickChickTop.v make[1]: Leaving directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' AMinus (ANum 0) (ANum 1) Checking Stack.compiles_correctly... *** Failed after 5 tests and 6 shrinks. (0 discards) Testing mutant 1 (./Exp.v: line 20): Plus-copy-paste-error make -f Makefile.coq make[1]: Entering directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' COQDEP VFILES COQC Exp.v COQC Stack.v COQC QuickChickTop.v make[1]: Leaving directory '/home/lemonidas/sfdev/qc/_qc_stack-compiler.tmp' APlus (ANum 0) (ANum 1) Checking Stack.compiles_correctly... *** Failed after 5 tests and 2 shrinks. (0 discards) All tests produced the expected resultsWe can see that the main property succeeds, while the two mutants (the one in arithmetic_expressions that was included because of the extension and the one in stack) both fail.

# QuickChick Command-Line Tool Flags

(* Tue Oct 9 11:47:31 EDT 2018 *)