Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

It is quite common in computer programs that some basic functionality is implemented, for efficiency reasons, using bit-wise operations. There is even a famous book, Hacker’s delight [24], which is dedicated only to this kind of smart and efficient code.

An extreme example is the following 2-line C program (a so-called “signature program” designed by Marcel van Kervinc, http://www.iwriteiam.nl/SigProgC.html).

figure a

It reads an integer n and prints another integer f(n). Assuming n is smaller than the machine word size in bits (say 32), then f(n) appears to be the number of solutions to the n-queens problem: the number of ways of placing n queens on a \(n\times n\) chessboard so that they do not threaten each other. Even more remarkable, this program implements the most efficient algorithm known so far to solve this problem.

Solving the n-queens problem was used in the past as a challenge for deductive program verification. The challenge is to attach to such code a formal specification, expressing its expected behavior at an abstract mathematical level (i.e. expressing that it really computes the number of solutions to the n-queens problem), and to prove formally that the code respects this specification. The solutions presented by Filliâtre [15], and other authors for a simplified version computing only the first solution [18], considered more abstract implementations, that do not operate directly on bits.

Deductive program verification typically proceeds by generating, from both the code and the formal specification, a set of logic formulas. These are called verification conditions because if one proves they are all tautologies, then the program is guaranteed to respect its specification. In program verification environments like Dafny [19] and Why3 [7], verification conditions are discharged using theorem provers, in particular those of the Satisfiability Modulo Theories (SMT) family such as Alt-Ergo [6], CVC4 [3], and Z3 [22]. The SMT approach is very promising for one who seeks to verify programs operating at the level of bits, because, in this context, theories for fixed-size bit vectors have been investigated for quite a long time and efficient decision procedures are known [4, 10, 12]. The SMT-LIB international initiative (http://smtlib.cs.uiowa.edu/) aims at providing standard languages and descriptions of theories for interacting with SMT solvers. SMT-LIB provides a fairly rich standard theory for fixed-size bit vectors, and decision procedures for this theory are implemented in several SMT solvers, including CVC4 and Z3.

Our objective is to add support for bit-wise operations in Why3 and its front-end SPARK2014 [21] that deals with safety-critical Ada programs. In particular, we want to exploit the bit vector decision procedures provided by SMT solvers. However, in such a context, bit-wise operations are mixed with other objects occurring in programs and specifications, such as unbounded integers, arrays, and records. We need to rely on other theories supported by SMT solvers, and also on their support for quantified axioms. Exploiting an SMT solver when several theories are mixed together with quantified axioms requires special care. This paper reports on our design choices and on some experiments we made. We start in Sect. 2 by illustrating our approach on a short (although non-trivial) example. In Sect. 3 we describe the theories for bit vectors we designed for use in Why3. In Sect. 4 we present how our Why3 theories are exploited in the SPARK2014 front-end. In Sect. 5 we illustrate our approach on a case study originating from industrial code. Our developments are distributed in SPARK Pro 16.0 and will be in the release 0.87 of Why3. More details and more case studies (including the 2-line n-queens program) are discussed in a technical report [14] and the files for the case studies are available on Toccata’s Web gallery of verified programs (http://toccata.lri.fr/gallery/bitwise.en.html).

2 Illustrative Example

We want to specify, at an abstract level, programs that directly manipulate bits. Our approach is to exploit in parallel the theory of bit vectors supported by SMT-solvers, and their support for arithmetic and quantifiers. We provide a theory that allows the use of both on the same program. In order to do so, the intended methodology to use this theory is to specify programs at an abstract level, closer to the human mind, e.g. with mathematical integers, while at the same time exploiting the bit vector theories of SMT solvers, by providing explicit hints for provers (typically under the form of extra assertions in the code) when it is necessary to help them to make the appropriate bridge between the bit vector level and the abstract level.

Let us consider an example from the Esterel compiler [5]. Each instruction returns an integer code between 1 and a fixed N. Parallel execution returns the maximum of the codes of its branches. A static analysis approximates programs by considering the set \(\overline{P}\) of all possible return codes of P. Hence \(\overline{P||Q} = \{max(p,q) | p \in \overline{P}, q \in \overline{Q}\}\). Sets of return codes are implemented as bit vectors, a 1 at position i in \(\overline{P}\) meaning that \(i\in \overline{P}\). It was suggested by Gonthier that \(\overline{P||Q}\) can be computed as \( (\overline{P}|\overline{Q}) \& (\overline{P}|-\overline{P}) \& (\overline{Q}|-\overline{Q})\).

We want to formally specify this behavior at an abstract level, not using any low-level operation like a bit-wise ‘and’. Let us consider the case where \(N=32\).

Fig. 1.
figure 1

maxUnion: formal specification

Full size image

Formal Specification. Fig. 1 presents how this code is formally specified in our setting (see [14] for details on Why3’s syntax). The declarations import the theory of 32-bit bit vectors we designed and the theory of finite set of integers from the Why3 library. From the former theory we use the type t of bit vectors, and the operator nth: nth x n is the n-th bit of x as a Boolean.

We want to relate a bit vector to its abstract view as a set of integers. We introduce a record type s with a field bv : t, and a ghost field mdl : set int a set of integers. A type invariant specifies that for each a : s the elements of a.mdl are the indexes of the 1-bits in a.bv. The precondition requires of maxUnion that the inputs are not zeros. The postcondition formalizes the former informal specification. The important point is that the formalspecification is at an abstract mathematical level which is quite far from the code in the body of the function. Proving that the code satisfies the specification is thus a difficult task.

Fig. 2.
figure 2

maxUnion: annotated code

Full size image

Proof. The code of maxUnion is split in three sub-functions shown in Fig. 2. It makes use of additional operations:

  • of_int x: integer x converted to a bit vector

  • eq_sub_bv x y i l: means that the bits of a and b between positions i and \(i+l-1\) are equal

  • bw_or, bw_and, neg, sub: bit-wise and arithmetic operators on bit vectors

  • min_elt a: the minimal element of a

  • interval i j: the set \(\{i \ldots j-1\}\)

We emphasize that the code of aboveMin contains three assertions involving only bit vectors and bit-wise operators. This form of intermediate assertion is an example of a general strategy that we explain in Sect. 3.3.

Fig. 3.
figure 3

maxUnion: proof results

Full size image

The proof results are displayed in Fig. 3. A red background indicates an unsuccessful proof, (10 m) meaning that the timeout of 10 min is reached, (6G) meaning that the memory limit of 6 GB is reached. We stress that we use CVC4 and Z3 in two different modes. The default mode exploits their native support for bit vectors, whereas the other mode, nicknamed ‘noBV’ for ‘no bit vectors’, does not. The two VCs, 2 and 3 for aboveMin, are proved using the native bit vector support. On the contrary VCs 1 and 4 for aboveMin and the VCs for union and intersection are proved only in the mode not using native support. This need for two modes for one prover shows up in all the case studies that we considered [14]. We detail the design of these two modes in Sect. 3.3.

3 The Why3 Bit Vector Theory

Our theory of bit vectors is generic with respect to the size of bit vectors. It is then instantiated for size 8, 16, 32 and 64. In Why3, such an instance is possible through the so-called cloning feature: when a theory has one or more components that are declared abstract (a type, a function symbol) then one can clone that theory while giving some instance to some or all of these abstract components. This results in a new theory containing a copy of the original theory, with all declarations appropriately instantiated.

In the following, we only describe a representative part of the theory. We refer to the report [14] for its full description as well as a discussion of its consistency and soundness, which is established through realizations in the Coq proof assistant and in Isabelle/HOL as well.

Fig. 4.
figure 4

Generic theory for bit vectors: core, bit-wise Boolean operators and shifts

Full size image

3.1 Bit-Wise Operators

The first part of the theory is shown in Fig. 4. It starts with the declaration of the (positive) parameter size, representing the number of bits of all bit vectors. The type of bit vectors is introduced as an abstract type t equipped with one uninterpreted function nth. The intended meaning is that (nth b n) gives the n-th bit of b, as a Boolean. Note the convention that bit 0 is the least significant bit, and (nth b n) returns False when n is out of the range \(0\ldots \texttt {size}-1\). We introduce two constants zeros and ones for the bit vectors that have all bits not set or set, respectively. These are axiomatized using nth.

The bit-wise operators ‘and’, ‘or’, ‘xor’ and ‘not’ come next. Their behavior is axiomatized with the help of the nth operator as seen in Fig. 4. Shift operators are also axiomatized using the nth operator. Notice that the second argument of shift operators is an integer and not a bit vector.

Fig. 5.
figure 5

Bit Vector theory: conversions and arithmetic

Full size image

3.2 Conversion To and From Integers

The second part of our theory, presented in Fig. 5, deals with conversion between bit vectors and integers. For lack of space, we only describe here the interpretation of bit vectors as non-negative integers, that interprets \(b_{n-1}\cdots b_1 b_0\) as \(\sum _{i=0}^{n-1} b_i\times 2^i\). We start by defining the maximum representable integer, and its successor: 2 to the power of size. Then we introduce two abstract functions for the conversions. These are not fully specified from nth; it would be a very involved axiomatization that is unlikely to be useful for automated provers. Instead, we provide a few useful axioms on those functions, regarding constants size, zeros and ones, and relation to equality.

Arithmetic operations do not need to distinguish between signed and unsigned variants, except for division and remainder. Their behavior is axiomatized via to_uint to express that computation is done modulo \(2^\texttt {size}\). Derived lemmas like add_bounded are added to help provers.

Fig. 6.
figure 6

Additional operators in the bit vector theory

Full size image

3.3 Strategy for Isolating Bit-Level Reasoning

The set of operators that we defined so far is expressive enough to formally specify programs. In order to discharge VCs a first idea would be to map each symbol of our theory to the corresponding symbol in the SMT-LIB theory, provided such a symbol exists, whilst keeping the other symbols uninterpreted and keeping all the axioms. However, we observed that this is not sufficient in practice: provers do not work well on VCs mixing bit-wise operators and conversions with integers (provers with native support for bit vectors have a hard time mixing bit vectors and integers, provers without it have a hard time to reason on bit-wise operators with the axioms only). Our approach to overcome this issue is two-fold. First, we provide a means for the user to isolate pure bit vector VCs from other VCs. Second, we provide to provers two alternative translations of our bit vector theory, to target specifically either provers with native support, or provers without it. The proof strategy used for the Rightmost Bit trick example (Fig. 3) exploits this approach.

Bit-Level Operator Variant. The theory is augmented with the additional operators presented in Fig. 6. We provide pure bit vector alternatives for nth and shifts. We also introduce the eq_sub operator and its bit-level variant eq_sub_bv.

Fig. 7.
figure 7

Mapping to SMT-LIB, for the case size=32

Full size image

The Two Drivers. Why3’s driver mechanism allows us to tell for each object (type, function symbol) of the Why3 theory what is the syntax for the corresponding object of the target prover. Figure 7 summarizes the two driver variants for the instance of the theory with size=32. The second column is the mapping for provers with native bit vector support, the third column is for the other provers as well as for the noBV variants of CVC4 and Z3. The driver for provers with native support maps the type t to the corresponding type in SMT-LIB. Each operator is mapped to the corresponding symbol in the SMT-LIB theory, if it exists, and is kept uninterpreted otherwise. The axioms that link the uninterpreted operators with the native ones are kept as-is. The remaining axioms are removed. There are two exceptions: nth_bv and eq_sub_bv are not in the SMT-LIB theory. Therefore, we keep the axioms that define them in term of pure bit-level operators. The driver for provers without native support keeps all symbols uninterpreted. All the axioms are kept except the ones that define the bit-wise operators, in order to prevent the provers from trying to prove bit-level properties.

4 Adding Support for Bit Vectors in SPARK2014

Ada 2012 is the latest version of the Ada language [1], a programming language targeting real-time embedded software that requires a high level of safety, security, and reliability. This version adds new features for specifying the behavior of programs, such as subprogram contracts and type invariants. SPARK is a subset of Ada targeting formal verification [11, 21]. Its restrictions ensure that the behavior of a SPARK program is unambiguously defined. The SPARK language and toolset for static verification has been applied for many years in on-board aircraft systems, control systems, cryptographic systems, and rail systems. It provides dedicated features that are not part of Ada 2012. Essential constructs for formal verification (e.g. loop invariants) have also been introduced. To formally prove a SPARK 2014 program, GNATprove uses the language WhyML as an intermediate. The SPARK program is translated into a WhyML program which can then be verified using the Why3 tool.

Modular Integer Types. Ada’s very rich type system allows us to define various kinds of integer types. There are mostly of two kinds, namely signed and modular integer types. Modular integer types are defined by specifying a modulus, and are the types on which bit-wise operations apply. For example

figure b

defines a type BV8 that contains unsigned integers between 0 and \(2^8-1\). Overflows never occur when computing with it: computations use modular arithmetic semantics. The package Interfaces from Ada’s standard library introduces predefined names Unsigned_8, Unsigned_16, Unsigned_32 and Unsigned_64, respectively for the modular types modulo \(2^8\), \(2^{16}\), \(2^{32}\) and \(2^{64}\). Bit-wise Boolean operations are written as infix operators and, or, xor, not. Ada provides, in its standard library, functions Shift_Left, Shift_Right, and Shift_Right_Arithmetic. These are defined only when the first argument is a modular type for the standard bit sizes 8, 16, 32, and 64. The second argument of these operations is not of modular type but of type Natural, that is the signed integer type of only non negative values defined in Ada’s standard library.

Handling of Modular Types in SPARK 2014. GNATprove translates each Ada variable, resp. each expression, into a Why3 variable, resp. expression, of some adequate type [17]. Variables and expressions of some modular type are translated into variables and expressions of some bit vector type of the Why3 theory described in the previous section. Their size is either 8, 16, 32, or 64, the smallest of those that can represent all the values of the original Ada type. To simplify the presentation below, we consider only the four predefined modular types Unsigned_8, Unsigned_16, Unsigned_32 and Unsigned_64 corresponding to 8, 16, 32, and 64-bits integers. The translation of the Boolean bit-wise operations is directly the equivalent introduced in our Why3 theory. The translation of shifts is just slightly more complex because their second argument in Ada is a signed type and not a modular type. For instance, we translate Shift_Left(X,Y) as .

5 The “Bitwalker” Case Study, Using SPARK2014

The original C version of the BitWalker was provided by Siemens in the context of the ITEA 2 project OpenETCS. The version presented here was rewritten by Fraunhofer FOKUS to simplify the formal verification with Frama-C/WP [16]. The formal specification relies on a theory of bit vectors designed in the Coq proof assistant, and a significant part of the proofs were done interactively within Coq.

Fig. 8.
figure 8

Schematic view of the Peek function (on 8-bit instead of 64-bit)

Full size image
Fig. 9.
figure 9

The BitWalker, C version, the Peek function

Full size image

Bitwalker is about interacting with a stream of bytes. One of the two main functions, Peek, copies a value from the byte stream to a 64-bit unsigned integer. The expected behavior of Peek, illustrated in Fig. 8, can be expressed at a high-level by saying that the integer value of the result is the value read in the byte stream starting from the bit number start and reading length bits. The most significant bits of the result, of index larger or equal to length, must be all zero. Figure 9 presents the C source code of Peek as well as one of its main auxiliary function, PokeBit64. The code of Peek does not make use of low-level bit-wise operators, but calls instead auxiliary functions. On the contrary, the code of low-level auxiliary functions PeekBit8 and PokeBit64 make use of bit-wise operators, so there is a need at some point to relate those bit-wise operations with more high-level arithmetic notions. In the following, we propose a SPARK program equivalent to the C code of Fig. 9, with appropriate formal specifications.

Specification and Verification of PokeBit64. The function PokeBit64 writes a bit in an Unsigned_64 value at the given position Left. In order to specify this we need to: first write that the mentioned bit is correctly set after the function is called, and then not to forget that all other bits remain unchanged. Its SPARK specification is given in Fig. 10. A first difference between the C and SPARK version appears in the types: in C, the first two parameters are unsigned types and the third parameter is an integer. In Ada, since the function manipulates the first parameter’s bits, it has to be of modular type. However, the parameter Left represents a position: it is not intended to be manipulated at the level of its bits and we do not want a modular arithmetic semantics, hence we set its type to Natural. This is consistent with the typing of shifts in Ada as described in Sect. 4. The last parameter, as it represents the state of a bit, is naturally given the type Boolean. Note the use of function Nth which refers to the Why3 operator nth. While the SPARK language does not have this function built in, we use the SPARK feature external axiomatization to lift it, as well as some others, to the level of SPARK language [14].

Fig. 10.
figure 10

Specifications of auxiliary functions for Peek

Full size image

The verification of PokeBit64 is not straightforward: we are in the case of a mix of bit vectors and integers. Following the proof strategy of Sect. 3.3 we introduce assertions to separate the part dischargeable by provers with native bit vector support from the rest. The code, with the assertions used to prove the specification, is given in Fig. 11. The third and last assertions reformulate the postcondition for CVC4 and Z3 at the bit level. The three other assertions deal with conversions between modulars and integers, and are proved by other provers.

Fig. 11.
figure 11

PokeBit64: annotated code and proof results

Full size image
Fig. 12.
figure 12

Ada specification and body of Peek function

Full size image

Specification and Proof of Bitwalker Peek. The SPARK specification of the main function Peek is given in Fig. 12. As for PokeBit64 there is a difference in the types: in Ada, Start and Length are naturals, by extension to what was said on PokeBit64 type. Note also the absence of the parameter size: it corresponds to Addr’Length in Ada. The precondition starts on line 13, by specifying that the first index of our byte sequence is 0, as in the C code. We then bound Length, the number of bits to copy, by 64. The last two preconditions are here to avoid any arithmetic overflow with Start, Length, and the size of Addr. The postcondition starts on line 17, and is made of two disjoint cases. First, if the last bit to copy is out of the bounds of the byte sequence the default value 0 is returned. In the other case, we specify two things: that the i-th bit of the result, for \(0\le i< \texttt {Length}\) is equal to the bit of the sequence at position \(\texttt {Start} + \texttt {Length} - i - 1\), as shown in Fig. 8. The n-th bit of a ByteSequence is specified by the auxiliary function Nth8_Stream given on line 3 of Fig. 12. Finally we specify that the other bits of the result are set to zero.

The Ada code of Peek is very close to the original C code of Fig. 9. We only add two loop invariants (lines 12–18) that are directly derived from the post-conditions. These invariants are the expected ones in presence of such a loop. Note that, following our reasoning on type assignment, Start and Length are Naturals, whereas the contents of the array Addr are 8-bit modular types, and the result of Peek is a 64-bit modular. As expected, since there is no bit-level code in Peek, there is no need for bit-level assertions and the proof does not need the provers with native bit vector support.

6 Conclusions

We designed a rich formal theory including arbitrary fixed-size bit vectors, a large set of bit-wise operations, and a large set of operations involving both bit vectors and unbounded integers. Thanks to the driver mechanism of Why3, proof obligations that make use of this theory can be discharged either by SMT solvers with bit vector support (CVC4, Z3) or by solvers that handle this theory as an axiomatic first-order theory (Alt-Ergo, and CVC4 and Z3 in non native support mode). We presented several case studies illustrating how one can specify and prove bit-level code correct with respect to a high-level specification. We emphasize that it is important for the user to understand well the respective capabilities of the provers (do they support bit vector theories or not) and to respect a refinement-like methodology when writing annotations: to prove that bit-level code satisfies a high-level postcondition, one may need to provide a hint in the form of an assertion rephrasing the postcondition at the bit-level, and help the provers with assertions to enforce them to convert bit vectors to integers when required. Fortunately, as shown by proof of Peek in BitWalker, our approach allows a good modularity principle: as soon as low-level code is given a high-level specification, the procedures calling such code do not need to be aware that the low-level code operates at the bit level. The support of Ada’s modular types via bit vectors is included since 2015 in SPARK releases. The first feedback from AdaCore’s customers is very positive: many proof obligations that were not checked automatically before are now proved by CVC4 or Z3.

About SPARK Interpretation of Signed Integers. We chose to map Ada’s signed integer types to mathematical unbounded integers. Another choice would be to map them to bit vectors and use the signed arithmetic operators provided by SMT-LIB. We tried this alternative and noticed regressions in the rate of automatically proved VCs: on the SPARK test suite the support for unbounded integer arithmetic in SMT solvers is better than the support for arithmetic operators of BV theory.

Related Tools and Experiments. Stefan Berghofer (Secunet, Germany) is using the support for bit vectors in SPARK, on the big number package of libsparkcrypto (https://bitbucket.org/sberghofer/libsparkcrypto/). He uses Isabelle/HOL to interactively discharge the VCs that cannot be proved automatically. The BitWalker case study was initially written in C and specified using the ACSL specification language of Frama-C. For that purpose a theory of bit vectors of unbounded size was designed using the Coq proof assistant, and the proofs were done with a significant amount of interaction within Coq. Thanks to the mapping of our bit vector theory to SMT-LIB we were able to prove BitWalker fully automatically. The source language, C or Ada, is not important, although the choice between signed versus unsigned types in the source makes a difference: in Ada their semantics are significantly different. The Boogie [2] verifier and its front-ends VCC [13] and Dafny [19] also use the built-in bit vector support of Z3, to model machine words. We are not aware of any work, in this context, about the problem of mixing bit vectors with high-level specifications.

Future Work. The need to use two different drivers for the same prover is somehow unsatisfactory. The decision of using the native support for bit vectors in provers could be made by an automatic analysis of the goal. A possible alternative would be to provide appropriate constructs in the specification language so that the user could indicate the intended level of abstraction in her code. For instance, in our solution to the n-queens example [14], it would have been convenient to express with a source annotation that we want to interpret a machine word into the set of positions of its bits set to 1.

There is some need to apply the same approach to floating-point numbers, in order to exploit decision procedures for floating-point arithmetic that are now available in SMT solvers [9] (http://www.cprover.org/SMT-LIB-Float/). In the past, floating-point programs were specified in terms of real numbers [8] and proved by specific solvers. As we did for bit vectors and integers, it is therefore desirable to design a theory that would allow the combination of floating-point numbers with real numbers and at the same time would make use of SMT-LIB support for floating-point arithmetic. Last but not least, there are some programs that operate on floating-point numbers at the bit-level [20]. Proving such code would be a hard challenge [23].