is_arith predicate

is_arith is presented as a test-purpose predicate for arithmetic-instruction testing in the microprocessor test-program generation case study. In the unit-test scenario, it constrains the instruction under test so that generated tests cover arithmetic operations rather than other instruction classes. [C1]

Unit-test usage

The paper gives the following arithmetic-operation unit-test setup: [C2]

test_spec σ= exec_instr σ0i =⇒is_arith i =⇒SUT σ0i σ
apply (gen_test_cases 0 1 SUT)
store_test_thm  arith_instr

In this setup, is_arith i is the predicate restricting the instruction variable i to arithmetic operations. After test-case generation, the case study reports that each arithmetic operation is covered by one generated test case. One example shown is: [C3]

1. SUT σ0(Iaddi ??X277 ??X266 ??X255) (...)

The paper identifies this as a test case for the addition operation. [C3]

Sequence-test usage

The same predicate is also used in an instruction-sequence scenario. The cited specification applies is_arith to a list of instructions and executes the generated sequence with mbind over execVAMP, checking the final state with assertSE: [C4]

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

A generated concrete sequence produced by gen_test_data is shown as: [C5]

σ 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 excerpt begins with: [C5]

ISUB  2 1 0

Test granularity considerations

The paper notes that the arithmetic-operation testing granularity is fairly coarse in this setup: HOL-TestGen selects one value satisfying all constraints over an integer variable. The authors attribute this to the model representing registers as integers rather than 32 word bitvectors, and to HOL-TestGen heuristics that select one candidate per variable. [C6]

As a workaround, the paper suggests introducing more case distinctions into test-purpose definitions, such as distinguishing values including MinInt, negative ranges, zero, and positive ranges, so that test selection must find solutions for finer constraints. [C6]