is_branch predicate Wiki

Overview

is_branch is a predicate used in the VAMP microprocessor test-generation case study to classify instructions for control-flow-related testing. It appears in test specifications that generate tests for branching operations, filtering either a single instruction or a list of instructions to the branch-instruction subset.

Use in single-instruction branch tests

For unit tests of individual branching operations, the predicate is used in the specification:

test_spec is_branch i =⇒ SUT σ0 i =k exec_instr σ0 i
apply (gen_test_cases 0 1 SUT)
store_test_thm branch_instr

This specification states that when instruction i satisfies is_branch, the system under test (SUT) applied to initial state σ0 and instruction i should conform to the reference execution exec_instr σ0 i under the conformance relation =k.

The cited case study says this generates unit test cases for branching operations starting from the initial state σ0. One schematic generated example shown is:

SUT σ0 (Ijalr ??X27X7) (...)

State-dependence concern

The case study notes a limitation of using a fixed initial state for these branch-operation tests: branching-operation behavior depends essentially on flag values. It suggests that a more interesting scenario would use different initial states with changed flag values for each test case.

Use in branch instruction sequences

The predicate is also used to constrain generated instruction sequences:

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

Here, list_all is_branch constrains every instruction in the list ιs to satisfy is_branch. The generated sequence is executed with mbind ιs execVAMP, and the resulting state is checked against the SUT result for the same initial state and instruction list.

The evidence gives the following concrete generated branch sequence:

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

Corresponding assembly:

IJ     1
IJALR  0

Test-data generation context

For the scenarios discussed in the case study, test data generation is performed by constraint solving and random instantiation. The authors note that additional constraints can be used to reduce the uniformity domain and improve coverage by dividing that domain into interesting sub-domains.