2

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?

Nico Naus
  • 21
  • 1
  • Do you really have a `ByteString`, or do you actually have some encoded version of an `Integer`? If the latter... well, `SInteger` is already a thing. If needed you can write encoding/decoding functions between actual `ByteString`s and `Integer`s that can be run on concrete values. – Daniel Wagner Apr 29 '22 at 15:21
  • No, these `ByteString`s do not come from integers. I'm reasoning over low level code and memory containing bytes, that is where my byte strings come from. The issue is that the `ByteString`s can have arbitrary length, so they could be bigger than an `Integer` – Nico Naus Apr 29 '22 at 16:45
  • There is no upper bound to the size of an `Integer` in Haskell (unlike some other languages' default integer type). – Daniel Wagner Apr 29 '22 at 16:58
  • Thank you, this is exactly what I was looking for. The solution that I now have is: `exprToSMT _ _ d = S.svInteger (S.KBounded False ((fromEnum $ BS.length d)*8)) (bsToInteger d)` where `bsToInteger` converts the `ByteString` to the unbounded `Integer` type – Nico Naus Apr 29 '22 at 17:13

1 Answers1

0

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.

alias
  • 28,120
  • 2
  • 23
  • 40
  • 1
    I don't think that would work. If you look at my example predicate, I'm relying on the bound to cause overflow. – Nico Naus Apr 29 '22 at 16:48
  • If that's the case, why not just turn that into an integer first, and then make a 32-bit unsigned value? Of course, that can overflow, so you have to explicitly check for that. Or maybe you don't care? It's not clear to me what you're trying to achieve. – alias Apr 29 '22 at 17:35