« Changelog History


sbv v8.4 Release Notes

Release Date: 2019-08-31 // over 4 years ago

    • SBV now supports arbitrary-size bit-vectors, i.e., SWord 17, SInt 9, SWord 128 etc. These work like any other bit-vector, using the DataKinds feature of GHC. Thanks to Ben Blaxill for the idea and the initial implementation. Note that SBV still supports the traditional fixed-size bit-vectors, SInt8, SWord16 etc. Support for these will not be removed; so existing programs will continue to work.

    • To convert between arbitrary sized bit-vectors and the old style equivalents, use fromSized and toSized functions. The behavior is controlled with a closed type-family so you will get a (hopefully not too horrendous) type error message if you try to convert, say, a SInt16 to SInt 22; or vice versa.

    • Added arbitrary-sized bit vector operations: extraction, extension, and joining; these use proxy arguments to determine precise size info, and are much better suited for type safety. Consequently, removed the Splittable class which provided similar operations but only on predefined types. There is a new class called ByteConverter to convert to-and-from bytes for suitable bit-vector sizes upto 512.

    • Tuple construction functions are given new types to strengthen type checking. Previously the tuple argument was ignored, causing things to be marked as tuples when they actually cannot be. (NB. The system was always type-safe, it just didn't produce helpful type-error messages before.)

    • Model validator: In the presence of universally quantified variables, SBV used to refuse to validate given models. This is the right thing to do since we would have to validate the model for all possible values of all the universally quantified variables. Obviously this is not useful. Instead, SBV now simply assumes any universally quantified variable is zero during model validation. This severely limits the validation result, but it is better than nothing. (In the verbose mode, a message to this effect will be printed.)

    • Model validator: SBV can now validate models returned from the backend solver for regular-expression match problems. We also constant fold matches against constant strings without calling the solver at all, less useful perhaps but more inline with the general SBV methodology.

    • Add implementation of SHA-2 family of functions as an example algorithm. These are good for code-generation purposes as opposed to actual verification tasks as it is hard to state any properties of these algorithms. But the SBV generated code can be quite useful in other development and verification environments. See 'Documentation.SBV.Examples.Crypto.SHA' for details.

    • Add 'cgShowU8UsingHex function, which controls if we print unsigned-8 bit values in code generation driver code in hex or not. Previously we were using decimal, but in crypto code hex is always better. Default is 'False' to keep backwards compatibility.

    • Add sObserve from: SymWord a => String -> SBV a -> Symbolic () which comes in handy in symbolic contexts, especially with quick-check uses.

    • Ramped up travis-appveyor build infrastructure. However, we no longer test on the CI, since build-times are prohibitively long and myriad issues cause instability. If you can help out regarding testing on CI, please reach out!