Adding support for bitvectors about smack HOT 4 CLOSED

I have studied a little bit what Boogie supports when it comes to types, and here is one simple example of how to maybe define our memory model in this case:

type ptr = bv64;
type bvtype t;
const unique type32 : bvtype bv32;
const unique type8 : bvtype bv8;

procedure main() 
{
  var M: <t>[ptr, bvtype t] t;
  M[0bv64, type32] := 10bv32;
  M[1bv64, type8] := 20bv8;

  assert M[0bv64, type32] == 10bv32;
  assert M[1bv64, type8] == 20bv8;

  return;
}

from smack.

I guess we should close this one now that bit-vectors are implemented.

from smack.

Hi guys,

There is obviously a scalability issue of SMACK when it is applied on DeviceDriver64 category of SVCOMP benchmarks that requires reasoning about bit-vectors. I think it would be good to improve our support for bit-vectors in order to fix this issue.

I manually inspected some benchmarks[1] and it seems that the number of variables requiring bit-vectors is limited (mainly flags[2]). So I think maybe a dependence analysis could allow us to use bit-vector on these variables while model others as integers though interprocedural support and pointer aliasing could be a big problem. Moreover, Akash's paper, Powering the Static Driver Verifier using Corral also provides a very reasonable solution. I remember you have tried it while it might not work well.

Please let me know your thoughts.

Thanks,
Shaobo

from smack.

This issue (support for bit-vectors) is certainly closed since SMACK supports bit-vectors now.

Improving the scalability of bit-vector support is a separate issue: #149.

from smack.