Overview
exec_instr is a function exposed by the generated ML code for the VAMP processor model. Its signature is:
val exec_instr : unit aSMcore_t_ext -> instr -> unit aSMcore_t_ext
It takes a VAMP machine state and an instruction value, and returns the successor machine state after executing that instruction. The surrounding generated VAMP structure also includes the instr datatype, arithmetic/data helper functions such as int_add, int_sub, and cell2data, the initial state sigma_0, and execInstrs for executing instruction lists. [C1]
Origin in the generated model
The VAMP ML code is generated from a formal model: the instr datatype is generated from the instruction type definition, while function definitions are generated from corresponding constants and functions defined in the model. exec_instr is therefore part of the executable model used for test generation and test execution. [C1]
Role in unit instruction testing
In the described HOL-TestGen workflow, exec_instr is used as the reference semantics for single-instruction conformance tests. A general unit-test specification has the form:
test_spec pre σ ι ==> SUT σ ι =k exec_instr σ ι
Here, SUT is a free variable later replaced by the system under test, while =k is an executable conformance relation comparing registers and the top k memory cells. Each generated unit test case contains an instruction, an initial configuration, and the expected configuration after executing the instruction. Preconditions can restrict generated tests to instruction subsets. [C2]
For load/store testing, the paper defines a predicate is_load_store and uses it to restrict the unit-test domain:
test_spec is_load_store ι ==> SUT σ0 ι =k exec_instr σ0 ι
HOL-TestGen performs exhaustive case splitting over the instruction datatype and, for load/store operations, produced eight symbolic test cases corresponding to different load and store operations. A later instantiation phase can produce concrete tests such as:
SUT σ0 (Ilb 1 0 1) σ1
where σ1 is the expected final state after execution. [C3]
Lifting into sequence testing
For instruction-sequence testing, exec_instr is lifted into the state-exception monad through execVAMP:
definition execVAMP where execVAMP == (λ i σ. Some ((), exec_instr σ i))
This lifting allows sequences of instructions to be evaluated with monadic combinators such as mbind and assertions such as assertSE. Sequence tests can compare either the entire final state or a selected part of it, such as a general-purpose register. [C4]
A load/store sequence test specification uses execVAMP as the model-side executor:
test_spec list_all is_load_store (ιs::instr list) ==>
(σ0 |= (s <- mbind ιs execVAMP;
assertSE (λσ. σ =k SUT σ0 ιs)))
This constrains generated instruction sequences to load/store instructions and checks that the final state conforms to the system under test. [C3]
Use in experiments
The generated executable model containing exec_instr was used as the execution target for HOL-TestGen-generated tests. Two test scripts were generated for load/store and arithmetic operation sequences; each produced 585 test cases, which were transformed into executable testers. Running the tests against the same executable model did not reveal errors, because the same model was used for generation and execution. [C5]
To evaluate test quality, the authors modified the executable model into a mutant model by changing int_add, int_sub, and cell2data. Against this mutant, arithmetic-operation tests reported 303 successful cases and 282 failures out of 585, while load/store tests reported 54 successful cases and 531 failures out of 585. [C5]
Technical significance
Within the case study, exec_instr is the central single-step semantic function connecting the formal VAMP instruction model to executable testing. It is used directly in unit-test specifications and indirectly in sequence-test specifications through execVAMP, making it the reference transition function for checking whether a system under test behaves according to the abstract assembler-level model. [C2] [C4]