[YICES-HELP] Re: [YICES] Problems with bit-vectors

[Domagoj Babic]

Hi Bruno,

Thanks for the prompt reply, that worked.

I've just generated a pile of benchmarks from software verification, and
ran into the following problem:

None of the expensive operators (barrel shifters, udiv/sdiv/umod/smod)
seem to be supported. Is there any way to handle those precisely?

Perhaps with some predefined functions, like bv2bool...

Thanks,
         Domagoj Babic





On 2/15/07, Bruno Dutertre <bruno at csl.sri.com> wrote:
> Domagoj Babic wrote:
> > Hi,
> >
> > I'm trying to encode a number of modular arithmetic problems into
> > Yices bit vector format, and ran into a number of problems, from type
> > errors to segfaults. Could someone please tell me what's wrong with
> > these two examples (yices 1.0.3, 64-bit linux version binary):
> >
> > Yices complains about invalid bitvector operation, but I can't pinpoint
> > exactly which one it is:
> >
> > (define v11109088::(bitvector 32))
> > (define c6215268::(bitvector 32) (mk-bv 32 0))
> > (define o11059512::(bitvector 1) (/= v11109088 c6215268 ))
> > (define c6235236::(bitvector 8) (mk-bv 8 0))
> > (define v11088608::(bitvector 8))
> > (define o11099952::(bitvector 1) (= c6235236 v11088608 ))
> > (define c3967452::(bitvector 1) (mk-bv 1 1))
> > (define o11119308::(bitvector 1) (bv-and o11099952 c3967452 ))
> > (define v11092352::(bitvector 32))
> > (define v11193332::(bitvector 32))
> > (define o11235472::(bitvector 1) (= v11092352 v11193332 ))
> > (define o11047112::(bitvector 1) (bv-and o11119308 o11235472 ))
> > (define o11035456::(bitvector 1) (ite o11099952 o11047112 c3967452 ))
> > (define v4038232::(bitvector 8))
> > (define o11146936::(bitvector 1) (= v4038232 c6235236 ))
> > (define o11052636::(bitvector 1) (bv-and o11146936 c3967452 ))
> > (define o11032924::(bitvector 1) (bv-and o11035456 o11052636 ))
> > (define v5897552::(bitvector 8))
> > (define o11046636::(bitvector 1) (= c6235236 v5897552 ))
> > (define o11025980::(bitvector 1) (bv-and o11032924 o11046636 ))
> > (define o11228256::(bitvector 1) (bv-and o11059512 o11025980 ))
> > (define c3958328::(bitvector 32) (mk-bv 32 0))
> > (define v10993040::(bitvector 32))
> > (define o11244528::(bitvector 1) (/= c3958328 v10993040 ))
> > (define o11055164::(bitvector 1) (bv-or (bv-neg o11228256) o11244528))
> > (define o11227376::(bitvector 1) (bv-xor o11055164 c3967452 ))
> >
> > (assert (= o11227376 (mk-bv 1 1)))
> > (check)
> >
> > while this example causes Yices to segfault:
> >
> > (define c3967452::(bitvector 1) (mk-bv 1 1))
> > (define c6235236::(bitvector 8) (mk-bv 8 0))
> > (define v11238708::(bitvector 8))
> > (define o11096724::(bitvector 1) (= c6235236 v11238708 ))
> > (define o11025272::(bitvector 1) (bv-and o11096724 c3967452 ))
> > (define v11022668::(bitvector 32))
> > (define v11076860::(bitvector 32))
> > (define o11052260::(bitvector 1) (= v11022668 v11076860 ))
> > (define o11172524::(bitvector 1) (bv-and o11025272 o11052260 ))
> > (define o11176208::(bitvector 1) (ite o11096724 o11172524 c3967452 ))
> > (define v11111308::(bitvector 8))
> > (define o11175408::(bitvector 1) (= v11111308 c6235236 ))
> > (define o11002432::(bitvector 1) (bv-and o11175408 c3967452 ))
> > (define o11045532::(bitvector 1) (bv-and o11176208 o11002432 ))
> > (define c3958328::(bitvector 32) (mk-bv 32 0))
> > (define v11247560::(bitvector 32))
> > (define o11245476::(bitvector 1) (/= c3958328 v11247560 ))
> > (define o4247164::(bitvector 1) (bv-or (bv-neg o11045532) o11245476))
> > (define o11235472::(bitvector 1) (bv-xor c3967452 o4247164 ))
> >
> > (assert (= o11235472 (mk-bv 1 1)))
> > (check)
> >
> >
> > My guess is that = and /= require the result to be of type bool,
> > and that "bitvector 1" is not considered to be equivalent to bool.
> > If that's the problem, how do I convert values (both constants and
> > variables) between bool and "bitvector 1"?
> >
> > Thank you,
> >          Domagoj Babic
> >
>
> Hi,
>
> Your guess is right. (bitvector 1) is not the same as bool.
> To convert between both, you can define simple conversion
> functions such as
>
> (define (bv2bool v::(bitvector 1))::bool (= v 0b1))
> (define (bool2bv b::bool)::(bitvector 1) (ite b 0b1 0b0))
>
>
>
> A better method is to use bool instead of (bitvector 1)
> in the input. You could just rewrite the second example to
>
> (define c3967452::bool true)
> (define c6235236::(bitvector 8) (mk-bv 8 0))
> (define v11238708::(bitvector 8))
> (define o11096724::bool (= c6235236 v11238708 ))
> (define o11025272::bool (and o11096724 c3967452 ))
> (define v11022668::(bitvector 32))
> (define v11076860::(bitvector 32))
> (define o11052260::bool (= v11022668 v11076860 ))
> (define o11172524::bool (and o11025272 o11052260 ))
> (define o11176208::bool (ite o11096724 o11172524 c3967452 ))
> (define v11111308::(bitvector 8))
> (define o11175408::bool (= v11111308 c6235236 ))
> (define o11002432::bool (and o11175408 c3967452 ))
> (define o11045532::bool (and o11176208 o11002432 ))
> (define c3958328::(bitvector 32) (mk-bv 32 0))
> (define v11247560::(bitvector 32))
> (define o11245476::bool (/= c3958328 v11247560 ))
> (define o4247164::bool (or o11045532 o11245476))
> (define o11235472::bool (/= c3967452 o4247164 ))
>
> (assert o11235472)
> (check)
>
> Notes:
> (bv-neg x) is equal to x if x is of type (bitvector 1)
> so I've removed that. In general (bv-neg x) is the opposite of
> x in 2's-complement representation, not the bitwise
> complement (which would be (bv-not x)).
>
> (xor x y) does not exists for booleans, but it's the same as (/= x y).
>
>
> Also, try to use flag -tc to get feedback on type errors.
> This will point you to the line where things are incorrect,
> and avoid segmentation faults.
>
>
>
> Bruno
>