Using SBV to show satisfiability of predicates containing byte strings in Haskell

Question

I want to use the Data.SBV library to prove satisfiability of predicates containing byte strings of arbitrary length (from Data.ByteString).

To illustrate, a predicate could be:

([0,0,1] + [255,255,255]) == [0,0,0]

In order to do so, I need to create an SVal from ByteString. My initial approach looks something like this:

exprToSMT _ _ d = case BS.length d of
  4 -> S.svInteger (S.KBounded False 32) (toInteger $ runGet $ getWord32be d)

So I would create an SVal using the svInteger, with a bounded kind that is unsigned and of the length of the ByteString in Bits. Instead of matching on length 4, I could calculate the bound by multiplying by 8, but the issues is getting the Integer value. In my domain, the ByteString can be of any length.

How can I create an SVal that represents a concrete ByteString of any length?

Answer 1

Looks like you need unbounded integers, i.e., SInteger. The kind for that is KUnbounded. (instead of KBounded False 32). Of you can simply use literal and pass the integer to it, and SBV will automatically deduce that it's an unbounded value.