Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking

                                  Shoham Shitrit                                   Sreepathi Pai
                             University of Rochester                          University of Rochester
                             sshitrit@u.rochester.edu                          sree@cs.rochester.edu

          Abstract—Formal semantics for instruction sets can be used to    both exhaustive and randomized testing do not make use of
validate implementations through formal verification. However,     the formal semantics, a point that is usually in their favour. In
testing is often the only feasible method when checking an artifact        this work, we explore how formal semantics can be used to
such as a hardware processor, a simulator, or a compiler. In this     seed an effective and automatic test generation strategies for
work, we construct a pipeline that can be used to automatically           instruction sets.
generate a test suite for an instruction set from its executable
semantics. Our method mutates the formal semantics, expressed               Our work is essentially model-based test generation with
as a C program, to introduce bugs in the semantics. Using a          the formal semantics specifying the model. The crux of our test
bounded model checker, we then check the mutated semantics           generation idea can be traced back to Carrington and Stocks [3]
to the original for equivalence. Since the mutated and original          where formal specifications expressed in Z were mutated and
semantics are usually not equivalent, this yields counterexamples      tests generated to distinguish the mutant specifications from
which can be used to construct a test suite. By combining a              the original specification. Our work in this paper is based
mutation testing engine with a bounded model checker, we obtain
a fully automatic method for constructing test suites for a given     on a similar idea, but our specifications describe instruction
formal semantics. We intend    to     instantiate this on a      formal  sets, are encoded in C, and we use model checking to verify
semantics of a portion of NVIDIA’s PTX instruction set for GPUs     equivalence. This is implemented in a fully automatic test suite
that we have developed. We will compare to our existing method           generation pipeline. Our evaluation focuses on an empirical
of testing that uses stratified random sampling and evaluate        analysis of our pipeline and its suitability in generating tests
effectiveness, cost, and feasibility.                                     for a real-world instruction set.
                           I.  INTRODUCTION                                We focus on NVIDIA’s PTX instruction set [4], a virtual
                                                                              instruction not unlike LLVM IR, but for NVIDIA’s GPUs.
Formal semantics for the instruction sets of many pro-                       NVIDIA only provides an informal description of PTX. We
cessors are now available [1, 2]. These semantics can be                have formalized this description in a custom domain-specific
used to validate processor implementations through formal                     language from which we extract the C semantics used in
verification. In         many  cases, software    interpreters that are    this work. Our method is restricted to instructions whose
correct-by-construction can be automatically extracted from               behaviour is completely defined by their inputs. More com-
these semantics. However, formal verification cannot be used              plicated instructions whose behaviour depends on internal,
or is too expensive for many implementations of instruction           implementation-specific, invisible GPU state are not supported
sets. A user who only has access to hardware processor and               by our current framework. These instructions do not consume
no access to the internals has no way of formally verifying                inputs or produce outputs in the conventional sense. Con-
it. Tools such as high-performance virtual machines, dynamic            cretely, this means instructions that enforce behaviour like
binary translators, compilers, etc. all utilize instruction set       memory consistency, synchronization, etc. are out of scope for
semantics but are very difficult to verify formally.                   our technique. These instructions are tested using orthogonal
             Exhaustive testing can be used to validate implementations   strategies like litmus tests [5].
of instruction sets and, in theory, achieve the same level of              Our contributions are as follows:
assurance as verification. However, the input space of even                •    We construct and evaluate a test generation pipeline
individual instructions is so large as to render exhaustive                       that uses mutation testing to introduce bugs in an
testing impractical. Randomized testing can be used instead                     executable specification and equivalence checking to
to achieve a high level of assurance but sampling strategies                  generate inputs to detect those bugs.
can significantly affect the quality of the test suite. Moreover,
                                                                           •   We describe an alternate method for constructing test
                                                                              suites based on stratified random sampling to serve as
International Fuzzing Workshop (FUZZING) 2022                                 a point for comparison.
27 February 2022, Virtual                                                  •     We find that our pipeline can construct inputs that
ISBN 1-891562-77-0
https://dx.doi.org/10.14722/fuzzing.2022.23xxx                                   expose bugs that are missed by stratified sampling-
www.ndss-symposium.org                                                          based method and at relatively low cost in CPU time.

f l o a ts r c 1 ,e x e c u t e a d d r m f t z s a t f 3 2 ( f l o a t Test Suite f l o a t s r c 2 ) { f l o a t t m p d s t ; f l o a t d s t ; Oracle Generate Test Mutated Tests fail s r c 1 = FTZ ( s r c 1 ) ; Semantics Mutations Semantics s r c 2 = FTZ ( s r c 2 ) ; t m p d s t = SATURATE(ADD ROUND( s r c 1 , All tests pass s r c 2 , FE DOWNWARD) ) ; t m p d s t = FTZ ( t m p d s t ) ; d s t = t m p d s t ; Extract Not Equivalent Check Equivalent r e t u r n d s t ; Counterexamples Equivalence } Fig. 1. A pipeline for generating test suites based on mutation generation Listing 1. The semantics of the PTX add.rm.ftz.sat.f32 instruction and equivalence checking. expressed as a C program.

                                                                                      equivalence. Since the semantics are expressed as C programs,
 •                                  We find some bugs in C code can introduce non-    any tool that can check equivalence of C programs can be used.
                                   determinism which makes testing for them nearly    In our work, we use CBMC [6], a bounded model checker for
     impossible without specialized instrumention.                                    C programs. The check asserts that for all inputs x and y that
 •                          We evaluate the possibility of generating a test suite    are floating point numbers, the two implementations are equal:
       fully          using  our    technique     and  find  it      to    be time    f l o a t x , y ;
                                consuming, compared to augmenting an existing test    a s s e r t ( a d d   r m f t z s a t  f 3 2 o r i g i n a l ( x , y )     ==
       suite                                                                                    a d d       r m f t z s a t  f 3 2 b u g g y ( x , y ) ) ;
                          We present preliminary data on 12 PTX instructions which                           When the two functions are not equivalent, CBMC will
                    operate on floating-point inputs and that comprise arithmetic,    yield counter-examples that cause this assertion fails. These

logical and elementary math functions. counter-examples can then be added to the test suite. II. MOTIVATING EXAMPLE We note that equivalence checking is undecidable in gen- To provide an overview of our technique, we demonstrate eral. However, several features of instruction set semantics it on Listing 1 which is a C program semantically equivalent make this less of an issue in practice. First, instruction set to the PTX add.rm.ftz.sat.f32 instruction. The instruc- semantics are usually simple, performing bitwise manipula- tion adds two 32-bit floating point numbers together rounding tions on fixed-size inputs. Second, loops if present, are almost towards negative infinity (.rm) and saturating the result to lie always bounded. Thus, checking the equivalence of instruction between [0.0, 1.0], while flushing subnormal inputs and output set semantics usually boils down to checking the equivalence floating point numbers to zero (.ftz). of small, straight-line programs, a far more tractable task. In the implementation, the FTZ function checks if a floating Given an equivalence checker and the correct semantics, point number is a subnormal and returns a zero with the sign we can now generate a test suite by creating buggy versions of the original number when it is, or the original number of the semantics and identifying the inputs that distinguish otherwise. The SATURATE function forces the output of the the buggy versions from the original semantics. This test suite rounding add (ADD_ROUND) to lie in [0.0, 1.0] by saturating can then be used to validate implementations which cannot negative values to 0.0 and positive values greater than 1.0 to be formally verified. We use mutation testing to generate the 1.0. buggy versions of the semantics. Consider now a real-life buggy implementation of these III. IMPLEMENTATION semantics in the CUDA compiler where FTZ was not applied to src1 and src2. To detect this bug, the values of src1 and Our framework for test suite generation for instruction set src2 must obviously be subnormal floats. However, their sum semantics using mutation testing and equivalence checking is must be a normal number to avoid the bug being masked by the shown in Figure 1. FTZ on tmp_dst. Using similar reasoning, it is easy to show that if a buggy implementation omitted the FTZ on the sum A. Overview (i.e. FTZ(tmp_dst) but preserved the FTZ applications on We are provided with an oracle semantics for the NVIDIA’s the inputs, the bug will only be caught if the inputs are normal PTX instruction set for its GPUs as semantically equivalent floating point values that sum to a subnormal value. Since C programs. Such C programs can be extracted from an the inputs and outputs must obey a specific relationship to existing formal semantics such as those encoded in SAIL [7] detect these bugs, existing methods such as random sampling but executable models can also be constructed from formal and even branch coverage can fail to generate inputs that will specifications written in K [8]. An existing test suite consisting unearth the bug. of input–output pairs for each instruction is also provided. This Yet, given the buggy implementation and the original test suite is not strictly necessary. When provided, however, our semantics, it is possible, in theory, to check the two for technique will only focus on mutations that are not detected

                                                                         2

by the existing test suite. Thus, our technique can improve the / * p r e c e d i n g t h i s and n o t shown i s t h e quality of an existing test suite. In the following discussion, co de from L i s t i n g 1 * / we always assume a test suite is provided since an empty test suite is acceptable as well. f l o a t m u t a t e d f u n c t i o n ( f l o a t s r c 1 , f l o a t The oracle semantics for each instruction are handed to a s r c 2 ) mutation generator. The resulting mutants can be regarded as { buggy versions of the oracle semantics, where the bugs are f l o a t t m p d s t ; the mutations that were introduced. These mutants are tested f l o a t d s t ; against the existing test suite. If tests fail for all mutations, s r c 1 = FTZ ( s r c 1 ) ; the pipeline stops, as the existing test suite is strong enough s r c 2 = FTZ ( s r c 2 ) ; to detect all introduced mutations. t m p d s t = SATURATE(ADD ROUND( s r c 1 , s r c 2 , Each mutant that survives the test suite proceeds to the ; FE DOWNWARD) ) ; equivalence checker, a step that does not usually exist in d s t = t m p d s t ; typical mutation testing scenarios. The equivalence checker r e t u r n d s t ; will consider one mutation at a time and verify equivalence } with the oracle semantics. Since a mutation–oracle pair is usually not semantically equivalent, this verification will fail. i n t main ( ) { With an appropriate tool, a counter-example can be extracted f l o a t v a r i a b l e 0 ; showing that the same inputs produce different outputs for the f l o a t v a r i a b l e 1 ; mutant and the oracle. This test case differentiates the oracle f l o a t r e s u l t = and the mutation and can be added to the test suite. e x e c u t e a d d r m f t z s a t f 3 2 ( In general, deciding when to stop this pipeline is unclear. v a r i a b l e 0 , v a r i a b l e 1 ) ; There are a finite number of functions that take two n-bit f l o a t m u t a t e d r e s u l t = m u t a t e d f u n c t i o n ( inputs, but this number is very large. We stop when we run v a r i a b l e 0 , v a r i a b l e 1 ) ; out of mutants. Thus, the quality of the pipeline is heavily a s s e r t ( r e s u l t == m u t a t e d r e s u l t ) ; dependent on the mutation generator. } r e t u r n 0 ; B. Mutation Generation and Testing Listing 2. A mutated version of add.rm.ftz.sat.f32 C semantics that omits the FTZ on the output variable tmp_dst with the code in main that The mutation framework utilized in this pipeline is MUSIC drives CBMC. (“MUtation analySIs tool with high Configurability and exten- sibility”) [9]. MUSIC mutates the AST of the oracle C program and outputs a mutated C program. This allows us to CBMC, the and the oracle semantics. Thus, either all the mutants are bounded model checker for C, which supports reasoning about semantically equivalent to the oracle semantics or the test suite floating point arithmetic. Other mutation frameworks (e.g. is incomplete. Traditional mutation testing frameworks rely on [10]) could be used if coupled with an equivalence checker the user to investigate these survivors to figure out which of that supports floating point operations. these cases a survivor falls into. MUSIC produces a number of mutant programs with each However, an equivalence checker can distinguish these mutant containing a single mutation chosen from a pre-defined two cases. In our technique, we use a model checker to library of mutations. If these mutants fail existing tests, they verify equivalence. For our purposes, model checkers are ideal are discarded. Only mutants that pass all existing tests and since they will not only verify equivalence, but also yield survive move on to the equivalence checking stage. counterexamples when the programs are not equivalent. MUSIC generates all the mutants in a single invocation. We use the C Bounded Model Checker (CMBC). CBMC However, the testing of each of these mutants can be done in converts C programs into logical models expressed in SMT- parallel since they are a collection of independent tasks. In our LIB language. Then, it discharges assertions about the C Python implementation of the pipeline, we use the facilities of program using existing SAT/SMT solvers. If the assertions fail, the built-in multiprocessing module to test mutants in CBMC will produce a trace of an execution of the program parallel. that causes the assertion to fail. From this trace, we can extract In this stage of the pipeline, we can measure the effective- the input values and use the oracle to generate the expected ness of the existing test suite by computing a mutation score output. The input–output pair can then be added to the existing – the number of killed mutations divided by the total number test suite. of mutations. The closer the mutation score is to 1.0, the more Consider as an example of this procedure, Listing 2, which mutants the test suite has killed, and thus the more resilient shows the mutated version of add.rm.ftz.sat.f32 and the test suite is to detecting bugs in the program. the main function that sets up the equivalence test. Note that since variable_0 and variable_1 are not initialized, C. Equivalence Checking and Testing their values are non-deterministic, causing CBMC to check A non-empty set of mutant survivors indicates that the the assertion over all possible values. existing test suite is incapable of differentiating between them Predictably, this mutated version fails the equivalence

3

check, and we obtain the following values from the CBMC TABLE I. SAMPLING STRATA FOR EACH TYPE OF PARAMETER TO A trace, shown here in hexadecimal float notation: PTX INSTRUCTION. b IS THE BITWIDTH OF THE INTEGER, min AND max ARE THE MINIMUM AND MAXIMUM NORMAL FLOATING POINT NUMBERS, v a r i a b l e 0 = −0x1 . d953fp −124 min AND max ARE THEIR SUBNORMAL ANALOGUES, nan IS THE v a r i a b l e 1 = 0 x1 . 0 a34p −123 IEEE754 NOT-A-NUMBER. m u t a t e d r e s u l t = 0 x1 . d8a08p −127 Type Strata Unsigned integers {0}, {1}, [2, 2b − 1), {2b − 1}, Both the input variables are normal numbers indicated by Signed Integers {−2b−1}, {0}, {1}, (−2b−1, 2b−1− 1), {2b−1 − 1} exponents greater than -127. However, their sum – the output Floats (Numbers) [−max, −min], [−max, −min], of mutated function – is clearly a subnormal number. Lacking {−0.0}, {+0.0}, [+min, +max the FTZ on tmp_dst, this subnormal escapes out as a return Float (Special) {−nan},], [+min, +max] {−∞}, {+∞}, {+nan} value. The original function would have returned 0 in this case. The procedure has generated exactly the inputs we were looking for – two normal numbers that sum to a subnormal. maximum number of test cases produced by our combinatorial Model checking is sound and exact. It produces no false strategy is 1728, for 3-input instructions whose arguments are positives unlike techniques such as abstract interpretation [11]. floating point numbers. However, this means that the primary limitation of model The strata definitions are currently ad hoc and aim to maxi- checking is state-space explosion. Therefore, like its name mize parameter coverage as well as incorporate all “boundary” implies, CBMC is limited to bounded programs. This means values. In particular, we want to elicit exceptional and un- that all loops in the program must have a fixed upper bound defined behaviour such as divide-by-zero, integer overflows, so that before model checking CBMC can unroll all loops up etc. Since we always take at least one sample from each to that bound. strata, the elements of the singleton sets in Table I will always Nevertheless, CBMC is a very good fit for our needs. The be included. Stratified sampling performed significantly better PTX instruction set semantics when expressed as C programs than a pure random sampling strategy that considered every do have loops, but all of them have finite bounds. We note that n-bit pattern equally likely. In hindsight, this is not surprising, none of the programs in this preliminary study have loops. since bit patterns representing a nan or ∞ are fewer in number They are also relatively small programs that do not make than those representing the normal numbers, for example. much use of the C standard library. CBMC also supports Unfortunately, an automatic criteria for defining strata is reasoning about IEEE floating point semantics [12, 13] which not known. This means that this is not a fully automatic is critical to generate tests for the large number of floating method, unlike the combination of mutation generation and point instructions supported by the GPU. equivalence checking. Like testing mutations, each invocation of CBMC on a V. E survived mutant can be executed in parallel. Similar to that VALUATION stage, we run equivalence checks in parallel using Python’s The goal of our evaluation is to answer the following built-in facilities. research questions. The first five questions naturally arise as observations from each stage of the pipeline. The last three IV. STRATIFIED RANDOM SAMPLING TEST SUITE questions investigate properties of our proposed method. GENERATION RQ1. How effective is mutation testing at generating mutants To compare our proposed test generation framework, we that pass our existing test suite generated by stratified random use a test suite generated using stratified random sampling. sampling? The premise of our method is that it will generate This technique uses the types of the inputs to generate test buggy versions that evade our current test suite. Effectiveness cases. Each test case is a randomly sampled value from a is measured by the count of mutants surviving our current predefined and fixed set of strata for a type. test suite that is generated by the stratified random sampling As an example, the strata for 32-bit method detailed in Section IV. unsigned integers are defined as the set RQ2. For mutants that evade the test suite, how many are {{0}, {1}, [2, UINT MAX), {UINT MAX}} where each caught later by the counter-examples generated by the equiv- element is itself a set and represents a strata. Here, there are alence checker? This evaluates if the equivalence checker can four strata, three of which are the singleton sets containing indeed generate inputs to detect the mutated versions of the 0, 1, and UINT MAX and the fourth consists all the other semantics and is measured by the increase in the number of positive numbers. For an instruction consuming a single mutants killed by the original test suite when augmented with unsigned 32-bit integer, our procedure would produce four the newly generated inputs. inputs, one from each strata. Random sampling would only RQ3. How many mutants are only caught by the equivalence be used for the set [2, UINT MAX), the test cases would checker and continue to escape being caught by the test suite always contain 0, 1, and UINT MAX. even after it has been augmented with counter-examples? For a instruction that takes n inputs, we would select the Ideally, the inputs generated by the equivalence checker should Cartesian product of the n sample sets to yield the test cases. result in the mutant being detected during testing, thus this Thus, all instructions consuming two 32-bit unsigned integers number should be zero. Surprisingly, we found this is not would have 16 test cases. Thus, only type and arity decide the always the case, pointing to a limitation of testing methods inputs used, not the semantics of the instruction per se. The that we did not fully appreciate when we started.

                                       4

RQ4. Which mutations lead to syntactic differences but are TABLE II. THE FLOW OF MUTATIONS THROUGH THE PIPELINE semantically identical? To be most useful, every syntactically Instruction Total Kill #1 Same Kill #2 Left Time (s) distinct mutant should also be semantically distinct from the abs.f32 70 65 3 0 2 1.41 ± 0.05 original program. Here, we investigate why some mutants re- add.rm.ftz.sat.f32 167 143 2 21 1 2.49 ± 0.13 add.rn.f32 24 23 0 0 1 0.72 ± 0.02 main semantically identical despite being syntactically distinct, add.sat.f32 128 125 1 0 2 1.86 ± 0.08 pointing to an additional way in which the quality of mutation set.eq.ftz.s32.f32 302 229 66 2 5 4.23 ± 0.22 generators may be evaluated using equivalence checkers. set.ge.f32.f32 333 233 79 2 19 4.75 ± 0.04 set.gt.s32.f32 212 139 66 2 5 3.27 ± 0.18 set.gt.u32.f32 212 139 66 2 5 3.25 ± 0.15 RQ5. What are the costs of this pipeline? Measured primarily setp.ge.f32 378 290 76 2 10 5.18 ± 0.16 as time consumed, we provide data on how long it takes for sqrt.rm.f32 245 127 0 11 107 3.50 ± 0.16 each stage of the pipeline. sub.rn.ftz.sat.f32 167 143 2 21 1 2.65 ± 0.10 sub.rz.ftz.sat.f32 167 143 2 21 1 2.56 ± 0.02

RQ6. What is the applicability of this pipeline? Although TABLE III. EQUIVALENCE CHECKER TEST GENERATION we provide preliminary results on 12 arithmetic and logical instructions that consume floats, we possess the semantics for Instruction Generated Unique Total Time (s) 4085 arithmetic and logic instructions that span integral and abs.f32 2 2 10 7.59 ± 0.09 add.rm.ftz.sat.f32 22 12 76 44.42 ± 0.38 floating point types of various sizes. Although, in principle, add.rn.f32 1 1 65 4.02 ± 0.04 these are supported by our pipeline, we have not yet inves- add.sat.f32 2 2 66 13.81 ± 0.08 tigated this empirically. In particular, we are concerned that set.eq.ftz.s32.f32 7 6 70 46.82 ± 0.43 set.ge.f32.f32 21 11 75 78.10 ± 0.38 some instructions, especially bit-level manipulation instruc- set.gt.s32.f32 7 6 70 47.21 ± 0.28 tions, might stress our equivalence checker. set.gt.u32.f32 7 3 67 46.48 ± 0.42 setp.ge.f32 12 8 72 61.01 ± 0.41 RQ7. How sensitive is the pipeline to the mutation generator sqrt.rm.f32 118 24 32 217.67 ± 1.72 sub.rn.ftz.sat.f32 22 12 76 43.97 ± 0.50 and the equivalence checker? Although we use MUSIC and sub.rz.ftz.sat.f32 22 12 76 44.15 ± 0.40 CBMC, there are similar tools that can be used in the pipeline. Although none of these support exactly what we want – C- level mutation and support for floating point arithmetic – it low when an existing test suite is used. Generating a test suite would still be interesting to evaluate piecemeal if additional from scratch (RQ8) is possible but consumes more time. The mutations are generated that are missed by the test suite created results for the RQ1–RQ7 are summarized in Table II and in through our pipeline. Likewise, using a symbolic execution Table III. Results for RQ8 are presented later in Table IV. like KLEE [14] for equivalence checking would provide a nice contrast to CBMC. A. RQ1: Generating Mutants RQ8. Can our pipeline replace a stratified random sampling The Total and Kill #1 columns of Table II show the number approach? Our pipeline is fully automated, in contrast to of mutants generated for an instruction and the number of those stratified sampling which requires manual specification of the mutants killed in the first round by our existing test suite. strata. Our primary metric here is cost. It is difficult to evaluate This number also includes mutants that failed to compile or coverage since that would involve finding buggy programs that did not execute to completion, though the fraction of mutants only our stratified sampling-based test suite will catch which killed by the test suite is always above 75%, except for implies those bugs cannot be induced by a mutation-based sqrt.rm.f32 where only 58% of mutants were detected method. by the test suite. Clearly, the number of mutants is related to RQ9. How effective is a state-of-the-art fuzzer compared to syntactic complexity of the original program (not evaluated equivalence checking? It is not hard to imagine replacing the here) – the abs.f32 instruction is mostly a single call to the equivalence checker with a fuzzer that attempts to discover the fabsf function, whereas all the others are more complicated. inputs that differentiate the mutants. We will use libFuzzer [15] The stratified sampling-based test suite does a remarkable job to compare to equivalence checking using CBMC. The fuzzer of eliminating a majority of mutants despite being based only will be given the same time that CBMC took. (This question on input types and arity. was suggested by a reviewer.) B. RQ2: Equivalence Checker Effectiveness In this work, we provide preliminary observations for a set of 12 instructions, all operating on floating point inputs. The Kill #2 column of Table II shows the number of MUSIC (commit 891d9ef), based on LLVM 7, was used mutants that escaped the original test suite, but were killed by to mutate programs. CBMC 5.38 was used to perform the a second round of testing when the test suite was augmented equivalence checks using the built-in MiniSAT solver. The by the new inputs produced by the equivalence checker. These timing results were obtained on a machine with AMD EPYC mutants were detected as being semantically different from the 7502P 32-core processor and 256GB of RAM running Ubuntu original program and the counter-examples generated should 18.04LTS. Each reported time is the average of 5 runs along be enough to detect them. While this is indeed the case for 8 of with its 95% confidence interval. the 11 instructions whose mutants survived, three instructions – abs.f32, add.rn.f32, and add.sat.f32 – had mutants Overall, we find that our proposed pipeline is effective at that survived the second round of testing as well. Indeed, to our accomplishing our basic goals – mutation testing does generate great surprise, there were always mutants that were detected buggy mutants that escape our existing test suite, equivalence by the equivalence checker to be different, but which always checking is able to detect semantic differences and generate evaded detection during testing. We investigate these in more the exact inputs required to distinguish them, and the cost is detail in our discussion of RQ3.

5

                    Table III shows the results of input generation by the   p r e d 2      = ( ! ( i s n a n ( s r c 1 )   % i s n a n ( s r c 2 ) ) )      &&

equivalence checker. While the Generated column shows the ( s r c 1 >= s r c 2 ) ; number of new inputs generated, a deduplication pass based on string equality results in far fewer Unique inputs being CBMC recognizes that when both src1 and src2 are not added to the test suite resulting in a final test suite containing not-a-number (NaN), the remainder operation will fail with a Total inputs. This suggests that many mutants themselves are divide by zero and it generates two normal numbers as inputs semantically identical to each other and this similarity could to provoke this behaviour. Unfortunately, when compiling the be exploited to reduce the cost of equivalence checking. For test at level -O3, the gcc 7.5.0 compiler decides to completely example, equivalence checking could be run only on a random remove the check (which is undefined if isnan(src2) == sample of mutants that survived a round of testing. The inputs 0) relying instead on the x86 SSE ucomiss instruction to generated could be used to weed out other mutants in a detect NaN, so no floating point exception for divide-by-zero substantially cheaper “mini-round” of testing to save on the is generated and the code executes normally to produce the cost of equivalence checking. same result as the oracle. Now, the C99 >= operator should raise a floating-point exception when one of the operands is a C. RQ3: Mutants that Evade Tests NaN, but the ucomiss instruction will only do so if it is a signaling NaN. Unfortunately, our test suite does not contain The Left column in Table II represents the mutants that a signaling NaN and CBMC is unaware of x86 semantics. The survive two rounds of testing, with the second round containing clang compiler does not have this “feature” and the test fails the inputs generated by the equivalence checker. This is as expected. logically possible but unexpected.1 This could be when the The compile-time exploitation of undefined behaviour equivalence checker flags a mutant as being non-equivalent means that some bugs will slip through testing non- when it is actually equivalent. This is benign and apparent, but deterministically depending on the compile-time environment. can complicate analysis. But another reason for this happening Thus, while CBMC can flag undefined behaviour, an imple- is the presence of non-determinism in the test. However, all mentation may or may not manifest the undefined behaviour. our instructions have deterministic behaviour. Nevertheless, A suggestion from a reviewer, which we plan to adopt, is we find that the mutation generation process introduces non- to instrument the tests using undefined-behaviour sanitizers. determinism in subtle ways by generating code that relies on This would increase the chances that the compiled version will undefined behaviour. detect the same undefined behaviours as CBMC. An excerpt from abs.f32 shows how a read from an Equivalence checking could be performed at the assembly- uninitialized variable is introduced into abs.f32 when an language level, which would detect this program as equivalent assignment is changed to +=: to the original except for signaling NaNs and hence produce a f l o a t t m p d s t ; signaling NaN as input. Model checkers for x86 exist including t m p d s t += f a b s f ( s r c ) ; those with support for SSE instructions [2], but we do not plan to explore them in this work. This mutation will go undetected if tmp_dst contains the D. RQ4: Syntactic Differences, Semantic Equivalence value 0.0 or if the compiler optimizes the undefined read away. The latter is the case on our test system. Equivalence checking provides insights into the limitations Although sqrt.rm.f32 contains a large number of of mutation generators. The Same column in Table II shows mutants that evade both rounds of testing, the reason is that, for some instructions, the majority of mutants that survive that it uses the C library sqrtf function. CBMC uses its the first round of tests are those that are equivalent to the own built-in implementation that is known to produce non- original program. Our limited survey of these programs shows deterministic results when the input is a subnormal because this is because the effect of the mutations is masked either IEEE subnormals have the unusual property that two numbers statically or dynamically. Some of these reasons are described can be squared to obtain them. The current implementation below, in no particular order. returns one of these numbers non-deterministically resulting a) Dead Code: Many mutations like the one introduced in spurious equivalence failures. Although a path to a possible below in abs.f32 are dead code and will never execute. fix is known [16], it has not been implemented as of writing. t m p d s t = f a b s f ( s r c 1 ) ; The set.ge.u32.f32 instruction contains a different d s t =: ( ( t m p d s t ) < 0 ? k i l l ( g e t p i d ( ) , 9 ) and more complicated instance, where the comparison: ( t m p d s t ) ) ; p r e d 2 = ( ! ( i s n a n ( s r c 1 ) i s n a n ( s r c 2 ) ) ) In the above code, the assignment is replaced by a ternary && ( s r c 1 >= s r c 2 ) ; operator, but the condition can never be true because tmp_dst is the output of fabsf. is mutated to: b) Semantic Equivalence: In contrast, mutations like 1The dual is when a mutant evades the equivalence checker but would be fabsf(-src1) will execute, but the semantics of fabsf caught by a test. This indicates a soundness bug in the equivalence checker. guarantee that the output will remain unchanged. Although This can be checked by asking for a proof of equivalence for each entry in the ternary operator replacement is hard to reason about the Same column of Table II and verifying the proof. This is a process that syntactically, fabsf can be detected syntactically and the can be automated but isn’t in our work. negation of its operands potentially skipped.

                                                     6

c) Near Semantic Equivalence: Some mutations are TABLE IV. EQUIVALENCES CHECKER TEST GENERATION FROM nearly equivalent to the original code, so there’s very little CRATCH chance they’ll change the behaviour of the program. Consider Instruction Generated Unique Time (s) this mutated code from the semantics of set.eq.u32.f32 abs.f32 67 16 123.40 ± 0.31 described previously: add.rm.ftz.sat.f32 165 93 294.08 ± 0.86 add.rn.f32 24 14 48.18 ± 0.30 add.sat.f32 127 57 222.40 ± 1.09 p r e d 2 = ( ! ( i s n a n ( s r c 1 ) << i s n a n ( s r c 2 ) ) ) set.eq.ftz.s32.f32 218 83 358.23 ± 2.16 && ( s r c 1 >= s r c 2 ) ; set.ge.f32.f32 232 93 394.51 ± 1.31 set.gt.s32.f32 128 61 269.86 ± 0.56 set.gt.u32.f32 128 54 276.26 ± 0.74 The mutation has the || replaced with <<. However, for setp.ge.f32 260 83 443.78 ± 1.84 boolean 0–1 inputs and outputs, << agrees with || 75% of sqrt.rm.f32 245 60 425.83 ± 1.64 sub.rn.ftz.sat.f32 165 91 291.80 ± 1.82 the time, disagreeing only for 0 << 1. The original program sub.rz.ftz.sat.f32 165 92 291.29 ± 1.74 would store 0 in pred2 for this case, and that’s what happens here as well, masking the effect of the mutation. This suggests that semantic equivalence should be thought of as a continuum takes milliseconds to produce inputs that can be reused across rather than a binary value to drive the search for mutations with programs. a higher probability of changing behaviour. The total number of inputs per instruction is solely the Unique number of inputs. As expected, these inputs kill the E. RQ5: Pipeline Costs same number of mutants as the sum of Kill #1 and Kill #2 The Time column in Table II contains the time it takes from Table II. However, in nearly every case, the number of for mutation generation and mutation testing per instruction. inputs is much greater than those listed in Table III. Only The testing of each mutant runs in parallel. The time includes add.rn.f32 requires significantly fewer inputs to kill all compilation, running, and checking of the outputs. Clearly, mutants than stratified sampling. Other instructions that have mutation generation and testing is not very expensive for these fewer inputs are add.sat.f32, set.gt.s32.f32 and small programs. set.gt.u32.f32. Equivalence checking (Table III) is more expensive. Even Although the costs for equivalence checking could be running in parallel, the throughput is only 1 mutant every few lowered by some form of deduplication before performing the seconds. The overall times are still relatively small, though. equivalence check, we suspect augmenting a good test suite is The most expensive checks take just a little more than a minute more cost effective than generating inputs from scratch. of wallclock time. To scale to larger instruction sets, however, Apart from cost, this method of test suite generation is the technique described at the end of Section V-B will probably sensitive to a particular mutation engine. This sensitivity can need to be used. be evaluated by using the generated test suite on mutations generated by an alternative mutation engine. F. RQ6: Applicability The instructions chosen for our preliminary tests span I. RQ9: Comparison to Fuzzing arithmetic, logic, and elementary math on floating point inputs. As of writing, our current infrastructure cannot substitute We plan to extend our pipeline to the other 4,085 instructions a fuzzer for an equivalence checker. However, to evaluate that span types from 8-bit integers to 64-bit integers and 64-bit feasibility, we instrumented the example in Listing 2 and ran floating point numbers as well. Nothing in our pipeline would it using libFuzzer (clang 10 and 12). CBMC takes around 2s restrict its applicability, however we suspect reasoning about to detect a counter example. However, libFuzzer is unable to bit-level instructions might be expensive. generate inputs that kill the mutant even when given more G. RQ7: Evaluating Alternatives time. We tried input generation strategies that ranged from 1.1M executions/s (default mutator) to 300K exec/s using a We would like to evaluate the effectiveness of the generated prototype stratified-sampling-based mutator that we continue test suite on mutations generated by Mull [10]. This could to refine. Nevertheless, we hope to confer with conference be coupled to use LLBMC [17], a bounded model checker attendees to obtain an experiment setup that will generate a for LLVM IR to perform equivalence checks on Mull output. useful comparison for the final revision. As an aside, before LLBMC does not support floating-point instructions and we this experiment, we did not appreciate the simplicity of the were unable to obtain it from its website. Alternatively, we can interface offered by equivalence checkers. use SeaHorn [18] to check equivalence, though the integration with Mull will need to be worked out. VI. RELATED WORK H. RQ8: Test Suite Generation from Scratch Hierons et al. [19] surveys a number of techniques that use formal specifications in the service of testing. Using formal Table IV shows the time taken to produce a test suite instruction set semantics to generate test cases is a form of for each program from scratch. In this case, all mutants are model-based test generation. As semantics for instructions are sent to the equivalence checker for verification. Predictably, usually embedded in instruction set simulators, past work on the time now taken is much higher, however there is no testing these simulators [20, 21, 22, 23, 24] highlight the main particular pattern that is evident. In contrast, stratified sampling approaches used.

   7

        Instructions for the x86 instruction set are encoded as                 VII.     CONCLUSION

a constraint-satisfaction problem to generate test inputs for each path [24]. The work eschews SAT solvers because CSP We have presented an automatic test generation pipeline for problems are easier to encode. DeMilli and Offutt [25] explores instruction set semantics. The pipeline uses mutation testing to how mutations can be associated with constraints that can then introduce bugs and equivalence checking to construct inputs be solved to generate test inputs. that trigger those bugs. The method can be used to augment both an existing test suite and construct a test suite. How- Martignoni et al. [23] use randomized testing by generating ever, our preliminary evaluation on 12 PTX instructions finds a stream of random bytes and testing the sequence on an that the pipeline is cost-effective only for augmentation. We actual physical CPU to identify both instructions and inputs also find mutation testing can introduce undefined behaviour randomly. Their method generates inputs randomly but is leading to non-determinism that can complicate testing of C essentially a form of differential testing. implementations. We are currently limited to particular tools to maximize the number of instruction set semantics supported. Specifications for Intel CPUs are mined from their manuals Good support for floating point would allow us to use other in [22] and used to construct test abstractions. These are equivalence checkers and mutation testing tools. instantiated with “boundary” values based on the intuition that Coupling equivalence checking to a mutation testing frame- boundary values lead to most errors. work provides a promising method to improve the quality of Wagstaff et al. [20] instrument the executable specification the mutation generation. As we observe in our evaluation, the of the ISA used in the instruction set simulator to obtain ability to detect semantically equivalent mutants also provides path coverage. This information is then used to construct path an objective metric for mutation tools. Our notion of near constraints that are solved using CVC4 to obtain test inputs semantic equivalence can be used to characterize the quality that exercise rarely-used paths. of individual mutations. Coverage-guided fuzzing is used to construct test inputs in REFERENCES [21] where mutation is used to increase code coverage in an [1] A. Armstrong, T. Bauereiss, B. Campbell, A. Reid, instruction set simulator. In constrast to these works, we mutate K. E. Gray, R. M. Norton, P. Mundkur, M. Wassell, a stand-alone semantics which is not embedded in a simulator. J. French, C. Pulte, S. Flur, I. Stark, N. Krishnaswami, We mutate the semantics to deliberately introduce bugs and use and P. Sewell, “ISA semantics for ARMv8-a, RISC- equivalence checking to surface inputs that trigger those bugs. v, and CHERI-MIPS,” Proceedings of the ACM on Coverage-based techniques would complement our method. Programming Languages, vol. 3, no. POPL, pp. 1–31, In a manner similar to our goal of using mutation testing to Jan. 2019. [Online]. Available: https://dl.acm.org/doi/10. add more tests, SpecTest [26] monitors the executable model of 1145/3290384 a language extracted from its semantics to obtain coverage of [2] S. Dasgupta, D. Park, T. Kasampalis, V. S. Adve, and small step semantics that are used by test programs. These test G. Ros¸u, “A Complete Formal Semantics of x86-64 programs are then mutated to increase coverage of language User-level Instruction Set Architecture,” in Proceedings semantics by injecting program constructs that correspond to of the 40th ACM SIGPLAN Conference on Programming unexercised semantics. Their mutation technique could be used Language Design and Implementation, ser. PLDI 2019. in our work to develop a richer set of bugs. New York, NY, USA: ACM, 2019, pp. 1133–1148. [Online]. Available: http://doi.acm.org/10.1145/3314221. Mutation-based testing tools [9, 10] have traditionally 3314601 checked if a test suite is adequate to detect randomly inserted [3] D. Carrington and P. Stocks, “A tale of two paradigms: bugs. It is usually outside the scope of mutation testing tools Formal methods and software testing,” in Z User Work- to generate test inputs. But some methods have generated tests shop, Cambridge 1994, ser. Workshops in Computing, by observing executions for state differences of (Java) objects J. P. Bowen and J. A. Hall, Eds. London: Springer, and then constructing assertions to detect these differences on 1994, pp. 51–68. this state [27]. Values are constructed randomly whereas we [4] N. Corporation, PTX: Parallel Thread Execution ISA, rely on counter-example generation using a model checker. 7th ed., 2021. [5] J. Alglave, L. Maranget, S. Sarkar, and P. Sewell, “Lit- Zhang et al. [28] drive dynamic symbolic execution to mus: Running Tests against Hardware,” in Tools and trigger mutation-detecting assertions that were introduced at Algorithms for the Construction and Analysis of Systems, the same time as the mutations, allowing inputs to be gen- ser. Lecture Notes in Computer Science, P. A. Abdulla erated. In our method, the equivalence checker also operates and K. R. M. Leino, Eds. Springer Berlin Heidelberg, symbolically but is highly decoupled from the mutation engine, 2011, pp. 41–44. and does not need to introduce additional assertions. [6] D. Kroening and M. Tautschnig, “Cbmc – c bounded model checker,” in Tools and Algorithms for the Con- Another method to generate inputs that detect differences struction and Analysis of Systems, E. Abrah´´ am and is through the use of differential symbolic execution [29]. In K. Havelund, Eds. Berlin, Heidelberg: Springer Berlin this work, Java programs are executed symbolically to generate Heidelberg, 2014, pp. 389–391. (abstract) bounded execution summaries that are then checked [7] A. Armstrong, T. Bauereiss, B. Campbell, K. E. Gray, for equivalence using CVC3. The simplicity of instruction set R. Norton-Wright, C. Pulte, S. Flur, and P. Sewell, semantics allows us to avoid the use of summaries. “The Sail instruction-set semantics specification

8

                 language,” p. 26, 2021. [Online]. Available: https://raw.    A.     J.    H.     Simons,      S.  Vilkomir,    M. R.      Woodward,
                  githubusercontent.com/rems-project/sail/sail2/manual.pdf    and        H.      Zedan,    “Using     formal    specifications    to

[8] T. F. Serbanuta, A. Arusoaie, D. Lazar, C. Ellison, support testing,” ACM Computing Surveys, vol. 41, D. Lucanu, and G. Rosu, “The K Primer (version 3.3),” no. 2, pp. 1–76, Feb. 2009. [Online]. Available: Electronic Notes in Theoretical Computer Science, vol. https://dl.acm.org/doi/10.1145/1459352.1459354 304, pp. 57–80, Jun. 2014. [Online]. Available: https:// [20] H. Wagstaff, T. Spink, and B. Franke, “Automated ISA linkinghub.elsevier.com/retrieve/pii/S1571066114000395 branch coverage analysis and test case generation for [9] D. L. Phan, Y. Kim, and M. Kim, “Music: Mutation retargetable instruction set simulators,” in Proceedings analysis tool with high configurability and extensibility,” of the 2014 International Conference on Compilers, in 2018 IEEE International Conference on Software Architecture and Synthesis for Embedded Systems, ser. Testing, Verification and Validation Workshops (ICSTW), CASES ’14. New York, NY, USA: Association for 2018, pp. 40–46. Computing Machinery, Oct. 2014, pp. 1–10. [Online]. [10] A. Denisov and S. Pankevich, “Mull it over: Mutation Available: https://doi.org/10.1145/2656106.2656113 testing based on LLVM,” 2018 IEEE International [21] V. Herdt, D. Große, H. M. Le, and R. Drechsler, “Ver- Conference on Software Testing, Verification and ifying Instruction Set Simulators using Coverage-guided Validation Workshops (ICSTW), Apr 2018. [Online]. Fuzzing*,” in 2019 Design, Automation Test in Europe Available: http://dx.doi.org/10.1109/ICSTW.2018.00024 Conference Exhibition (DATE), Mar. 2019, pp. 360–365. [11] P. Cousot and R. Cousot, “Abstract interpretation: [22] W. Ma, A. Forin, and J.-C. Liu, “Rapid prototyping a unified lattice model for static analysis of and compact testing of CPU emulators,” in Proceedings programs by construction or approximation of of 2010 21st IEEE International Symposium on Rapid fixpoints,” in Proceedings of the 4th ACM SIGACT- System Protyping, Jun. 2010, pp. 1–7. SIGPLAN symposium on Principles of programming [23] L. Martignoni, R. Paleari, G. F. Roglia, and D. Bruschi, languages - POPL ’77. Los Angeles, California: “Testing CPU emulators,” in Proceedings of the ACM Press, 1977, pp. 238–252. [Online]. Available: eighteenth international symposium on Software testing http://portal.acm.org/citation.cfm?doid=512950.512973 and analysis, ser. ISSTA ’09. New York, NY, USA: [12] “The CPROVER Manual: Floating point.” [On- Association for Computing Machinery, Jul. 2009, pp. line]. Available: http://www.cprover.org/cprover-manual/ 261–272. [Online]. Available: https://doi.org/10.1145/ modeling/floating-point/ 1572272.1572303 [13] M. Brain, F. Schanda, and Y. Sun, “Building Better [24] S. V. Kodakara, D. A. Mathaikutty, A. Dingankar, Bit-Blasting for Floating-Point Problems,” in Tools and S. Shukla, and D. Lilja, “Model Based Test Genera- Algorithms for the Construction and Analysis of Systems, tion for Microprocessor Architecture Validation,” in 20th ser. Lecture Notes in Computer Science, T. Vojnar and International Conference on VLSI Design held jointly L. Zhang, Eds. Cham: Springer International Publishing, with 6th International Conference on Embedded Systems 2019, pp. 79–98. (VLSID’07), Jan. 2007, pp. 465–472. [14] C. Cadar, D. Dunbar, and D. Engler, “KLEE: Unassisted [25] R. DeMilli and A. Offutt, “Constraint-based automatic and Automatic Generation of High-Coverage Tests for test data generation,” IEEE Transactions on Software Complex Systems Programs,” OSDI, p. 16, 2008. Engineering, vol. 17, no. 9, pp. 900–910, Sep. 1991. [15] LLVM Project, “libFuzzer – a library for coverage- [26] R. Schumi and J. Sun, “SpecTest: Specification-Based guided fuzz testing. – LLVM 15.0.0git documentation.” Compiler Testing,” in Fundamental Approaches to Soft- [Online]. Available: https://llvm.org/docs/LibFuzzer.html ware Engineering, ser. Lecture Notes in Computer Sci- [16] M. Brain, “sqrtf appears to be non-deterministic ence, E. Guerra and M. Stoelinga, Eds. Cham: Springer and throwing spurious verification failures - Issue International Publishing, 2021, pp. 269–291. #6563 - diffblue/cbmc.” [Online]. Available: https: [27] G. Fraser and A. Zeller, “Mutation-Driven Generation of //github.com/diffblue/cbmc/issues/6563 Unit Tests and Oracles,” IEEE Transactions on Software [17] F. Merz, S. Falke, and C. Sinz, “LLBMC: Bounded Engineering, vol. 38, no. 2, pp. 278–292, Mar. 2012. Model Checking of C and C++ Programs Using a [28] L. Zhang, T. Xie, L. Zhang, N. Tillmann, Compiler IR,” in Verified Software: Theories, Tools, J. de Halleux, and H. Mei, “Test generation Experiments, R. Joshi, P. M¨uller, and A. Podelski, via Dynamic Symbolic Execution for mutation Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, testing,” in 2010 IEEE International Conference 2012, vol. 7152, pp. 146–161, series Title: Lecture on Software Maintenance. Timisoara, Romania: Notes in Computer Science. [Online]. Available: http: IEEE, Sep. 2010, pp. 1–10. [Online]. Available: //link.springer.com/10.1007/978-3-642-27705-4 12 http://ieeexplore.ieee.org/document/5609672/ [18] A. Gurfinkel, T. Kahsai, A. Komuravelli, and J. A. Navas, [29] S. Person, M. B. Dwyer, S. Elbaum, and “The SeaHorn Verification Framework,” in Computer C. S. Pˇasˇareanu, “Differential symbolic execution,” Aided Verification, D. Kroening and C. S. P˘as˘areanu, in Proceedings of the 16th ACM SIGSOFT Eds. Cham: Springer International Publishing, 2015, International Symposium on Foundations of software vol. 9206, pp. 343–361, series Title: Lecture Notes engineering, ser. SIGSOFT ’08/FSE-16. New York, in Computer Science. [Online]. Available: http://link. NY, USA: Association for Computing Machinery, springer.com/10.1007/978-3-319-21690-4 20 Nov. 2008, pp. 226–237. [Online]. Available: [19] R. M. Hierons, K. Bogdanov, J. P. Bowen, https://doi.org/10.1145/1453101.1453131 R. Cleaveland, J. Derrick, J. Dick, M. Gheorghe, M. Harman, K. Kapoor, P. Krause, G. L¨uttgen,

                                                         9