gen_test_cases command Wiki

Overview

gen_test_cases is a HOL-TestGen command used in proof scripts after a test_spec formula has constrained the intended test domain. In the VAMP microprocessor case study, it is shown as an apply method that generates schematic test cases for a system under test (SUT) and is followed by store_test_thm, which stores the result as a named test theorem. [c1]

Typical forms shown in the evidence include:

apply (gen_test_cases 0 1 SUT)

for unit-test-style scenarios, and:

apply (gen_test_cases SUT)

for instruction-sequence scenarios. [c1] In the sequence case, the cited paper states that the call to the automatic test case generation method declares the free variable SUT as the system under test. [c2]

Role in the test-generation workflow

The command is used after a test purpose has narrowed the input domain. For example, a load/store predicate is introduced into the precondition of the test specification to reduce generated tests to load and store operations:

test_spec is_load_store ι ⇒ SUT σ0 ι =k exec_instr σ0 ι
apply (gen_test_cases 0 1 SUT)
store_test_thm load_store_instr

In this scenario, HOL-TestGen performs exhaustive case splitting on the instruction datatype and generates symbolic operands for each instruction, producing symbolic test cases. [c3]

The generated schematic tests are not yet concrete executions. The evidence describes a second phase, performed by the gen_test_data command, that instantiates schematic variables with concrete values. [c4]

Output structure

For the load/store unit-test scenario, test generation produced eight symbolic test cases, one for each different load/store operation, together with eight uniformity hypotheses. The paper defines the conjunction of the generated test cases and their uniformity hypotheses as a test theorem. [c5]

A generated symbolic case can contain schematic variables such as ??X7, ??X6, and ??X5; the evidence states that variables beginning with ??X are schematic variables representing possible witness values. [c6]

An example symbolic load instruction test case is shown as:

1. SUT σ0(Ilb ??X7 ??X6 ??X5) (...)
2. THYP ((∃ x xa xb. SUT σ0(Ilb xb xa x) (...)) →
        (∀ x xa xb. SUT σ0(Ilb xb xa x) (...)))

The first subgoal is the schematic test case, while the second is the associated uniformity hypothesis. [c6]

Unit-test usage

Load/store instructions

When used with the is_load_store test purpose, gen_test_cases generates unit tests for load/store instructions. The cited paper says that this kind of unit test can reveal design faults when an operation result is incorrect and can also detect undesired state modifications, such as changes to flags or registers. [c7]

Arithmetic instructions

For arithmetic operations, the cited unit-test specification constrains the tested instruction with is_arith and invokes:

apply (gen_test_cases 0 1 SUT)
store_test_thm arith_instr

At that stage, each arithmetic operation is covered by one generated test case; the evidence gives an Iaddi schematic test as an example addition-operation case. [c8]

Branching instructions

For branching operations, the cited unit-test specification uses is_branch and invokes:

apply (gen_test_cases 0 1 SUT)
store_test_thm branch_instr

The evidence states that this generates unit test cases for branching operations starting from the initial state σ0. It also notes a limitation of this setup: the initial state is fixed, while branching behavior depends on flag values, so varying initial states would be more interesting for such tests. [c9]

Sequence-test usage

gen_test_cases is also used for instruction sequences. The cited paper uses the HOL list_all combinator to generalize a predicate such as is_load_store, is_arith, or is_branch across an instruction list, and then defines valid test sequences using monadic state-exception combinators such as mbind and assertSE. [c10]

A load/store sequence specification is shown as:

test_spec list_all is_load_store (ιs::instr list) ⇒
        (σ0 |=(s ←mbind ιs execVAMP; assertSE (λσ. σ=k SUT σ0ιs)))
apply (gen_test_cases SUT)
store_test_thm load_stre_instr_seq

The cited example of a generated length-3 schematic test sequence contains one Isw followed by two Ilbu instructions, with a corresponding uniformity hypothesis. [c11]

For arithmetic instruction sequences, the evidence shows:

test_spec list_all is_arith (ι::instr list) ⇒
        (σ0 |=(s ←mbind ιs execVAMP; assertSE (λσ. σ=k SUT σ0ι)))
apply (gen_test_cases SUT)
store_test_thm arith_instr_seq

After data generation, one possible concrete sequence is a subtraction followed by two additions:

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

[c12]

For branch instruction sequences, the cited paper similarly applies gen_test_cases SUT and later obtains a concrete sequence containing IJ 1 followed by IJALR 0. [c13]

Relationship to concrete test data

gen_test_cases produces schematic test cases and hypotheses; concrete values are introduced later by gen_test_data. The evidence states that gen_test_data instantiates schematic variables with concrete values, and that test data generation in the considered scenarios is performed by constraint solving and random instantiation. [c4] [c14]

Practical considerations from the case study

The cited paper notes that test data generation can lead to sequences with coarsely grained memory access. It suggests adding constraints to reduce the uniformity domain, such as bounding address ranges, defining a predicate over used addresses, or constraining load operations to addresses written by store operations. Such constraints can also improve coverage by dividing the uniformity domain into interesting subdomains. [c14]