Bitvector bv%i is broken

[bobot]

Some offsets seems to be off in the conversion to a binary string. But more importantly it uses int_of_string which is limited to 63 bit. We need to handle any size. Two solutions:

• doing the conversion by hand, error prone but no new dependencies
• depend on zarith

What do you prefer?

[Gbury]

I thought about it when writing it but from what I understand there will be problems only if a problem make use of bitvectors whose size is strictly greater than 2 ^ 62, (in which case, I don't think parsing such a bitvector litteral will be realistic, so only symbolic manipulation may be done, but I guess this can happen ?), or am I missing something ?

[bobot]

No, just a bitvector of size 62, it is the actual value of the bitvector that goes through int_of_string not just the size.

[bobot]

(define-fun big () (_ BitVec 334) (_ bv9999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999 334))

[Gbury]

Oh, indeed that's a problem. We'll have to write a manual conversion to strings in that case (I'd rather avoid depending on zarith for now if not absolutely necessary).

[bobot]

So https://stackoverflow.com/a/11007021/1531323 for direct conversion to binary ?

[bobot]

For reference the code with zarith (for COLIBRI I fixed it that way temporarily):

    let parse_extended_lit _env _ast s n =
      assert (String.length s >= 2);
      let s' = String.sub s 2 (String.length s - 2) in
      match Z.of_string s' with
      | exception Failure _ -> None
      | z ->
        let z = Z.rem z (Z.shift_left Z.one n) in
        let s'' = Z.format (Printf.sprintf "%%0%ib" n) z in
        Some (Type.Term (T.mk_bitv s''))

[Gbury]

So https://stackoverflow.com/a/11007021/1531323 for direct conversion to binary ?

Yes, i'll try and implement it as soon as possible.