gen_test_data command

Overview

gen_test_data is a command used in HOL-TestGen during the test-data instantiation phase. After symbolic or schematic test cases have been generated, gen_test_data instantiates schematic variables with concrete values to produce executable concrete test cases. In the VAMP microprocessor case study, this workflow is shown for load/store instructions, arithmetic instruction sequences, and branch instruction sequences.

Role in the HOL-TestGen workflow

The evidence describes test generation as a two-phase process for load/store unit tests:

1. gen_test_cases performs case splitting over the instruction datatype and generates symbolic test cases with schematic operands.
2. gen_test_data performs test-data instantiation by choosing concrete witness values for those schematic variables.

For example, after symbolic load/store test cases such as:

SUT σ0(Ilb ??X7 ??X6 ??X5) (...)

gen_test_data can produce a concrete test case such as:

SUT σ0(Ilb 1 0 1) σ1

where σ1 is the expected final state after executing the operation.

Use with instruction sequences

gen_test_data is also used for instruction-sequence scenarios expressed with state-exception monad combinators such as mbind and assertSE. The case study shows a schematic load/store sequence generated by gen_test_cases, followed by a concrete sequence produced by gen_test_data:

σ0 |=(s ←mbind [Isw 0 1 8, Ilbu 1 0 -3, Ilbu 3 2 8] execVAMP;
       assertSE (λσ. σ =k SUT σ0[Isw 0 1 8, Ilbu 1 0 -3, Ilbu 3 2 8]))

This corresponds to the assembly sequence:

ISW   0 1  8
LLBU  1 0 -3
LLBU  3 2  8

The paper states that such test programs can reveal errors related to read/write sequencing, including byte-alignment errors and information loss due to pipelining.

Arithmetic example

For arithmetic instruction sequences, the case study presents a sequence generated from the gen_test_data command:

σ0 |=(s ←mbind [Isub 2 1 0, Iadd 1 5 2, Iadd 1 0 4] execVAMP;
       assertSE (λσ. σ=k SUT σ0[Isub 2 1 0, Iadd 1 5 2, Iadd 1 0 4]))

The corresponding assembly code is:

ISUB  2 1 0
IADD  1 5 2
IADD  1 0 4

The sequence is described as a subtraction followed by two addition operations.

Branching example

For branch instruction sequences, the same pattern is used: a test specification constrains lists of instructions with list_all is_branch, gen_test_cases generates schematic cases, and test data generation returns concrete sequences. One example concrete sequence is:

σ0 |=(s ←mbind [Ij 1, Ijalr 0] execVAMP;
        assertSE (λσ. σ=k SUT σ0[Ij 1, Ijalr 0]))

with corresponding assembly:

IJ        1
IJALR     0

The cited text notes that branch behavior depends on flag values, so using only a fixed initial state is limited; varying initial states with different flag values would be more interesting.

Test-data generation method and limitations

The case study states that test-data generation in the considered scenarios is performed by constraint solving and random instantiation. It also notes a limitation: this can lead to test sequences with coarsely grained memory access. The authors suggest adding constraints to reduce the uniformity domain, such as bounding address ranges or constraining load operations to addresses previously written by store operations. Such constraints can also improve coverage by dividing the uniformity domain into interesting subdomains.