is_load_store predicate Wiki

Definition

is_load_store is defined as a predicate of type instr ⇒ bool:

definition is_load_store :: instr ⇒ bool
where is_load_store iw ≡ is_load_store_word’ iw
        ∨ is_load_store_hword’ iw
        ∨ is_load_store_byte’ iw

This definition classifies an instruction iw as a load/store instruction when one of the word, halfword, or byte load/store sub-predicates holds. The surrounding text gives byte-level load/store constructors such as Ilb rd rs imm, Ilbu rd rs imm, and Isb rd rs imm; analogous test cases for the word and halfword sub-predicates are noted as omitted for space. [definition-and-scope]

Use in unit-test generation

The predicate is introduced in the precondition of a test specification to reduce generated tests to load/store operations. The cited unit-test specification is:

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 over the instruction datatype and generates symbolic operands for each instruction. The generation process produced 8 symbolic test cases, corresponding to the different load and store operations; the final generation state contained 8 schematic test cases and 8 associated uniformity hypotheses. The conjunction of the test cases and uniformity hypotheses is called a test theorem. [unit-test-generation]

An example symbolic case shown in the source has the form:

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

with an associated uniformity hypothesis over all operands of Ilb. The source explains that variables beginning with ??X are schematic variables representing possible witness values. [symbolic-example]

Test-data instantiation

After symbolic generation, HOL-TestGen uses gen_test_data for test-data instantiation. One concrete example given is:

SUT σ0(Ilb 1 0 1) σ1

Here, σ1 is the expected final state after executing the operation. The cited text characterizes these cases as unit-test-style tests in which each operation is tested individually; such tests can reveal design faults when the operation result is incorrect and can detect undesired state modifications such as changes to flags or registers. [test-data-instantiation]

Use for instruction sequences

The same predicate is also used to characterize load/store instruction sequences by generalizing it to lists with the HOL-library combinator list_all. The cited sequence-level specification is:

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 paper contrasts this with more difficult-to-execute automaton or extended finite-state-machine characterizations and instead uses monadic combinators of the state-exception monad directly to define valid test sequences constrained by test purposes. [sequence-characterization]

A generated length-3 sequence example includes a store word followed by two unsigned byte loads:

[Isw ??X597 ??X586 ??X575,
 Ilbu ??X557 ??X546 ??X535,
 Ilbu ??X517 ??X506 ??X595]

This example appears inside a generated subgoal comparing execution through execVAMP with the SUT result for the same instruction sequence. [sequence-example]