Bitvector support - Githubissues

mpdairy commented 5 years ago

I would like to add Bitvector support to LH so that we can use bitwise operations in LH type signatures.

I made a feeble first attempt using BV from the Data.BitVector module in the bv library. Then I made a Data/BitVector.spec that had the line:

embed Data.BitVector.BV  as (_ BitVec 64)

But I'm getting the error:

 3 | embed Data.BitVector.BV  as (_ BitVec 64)
                                 ^

     unexpected "("
     expecting fTyConP

Then I was going to add bitvec ops to CoreToLogic.lg.

Of course, the problem with this, besides not currently working, is that I'd really want to embed a BV of n width to an SMT BitVec of n width, but I can't really do that without dependent types in Haskell.

Have you thought of a good way to add BitVecs to LH? Can you think of a hacky way to do it with what is currently available in LH?

ranjitjhala commented 5 years ago

No it’s not hard actually; the constraint solving backend already (in fact I wonder if we support it already...)

can you post an example of a file you’d like to have checked that uses bitvectors?

On Fri, Sep 13, 2019 at 6:04 PM Matt Parker notifications@github.com wrote:

I would like to add Bitvector support to LH so that we can use bitwise operations in LH type signatures.

I made a feeble first attempt using BV from the Data.BitVector module in the bv library. Then I made a Data/BitVector.spec that had the line:

Would that be incredibly difficult, or is it mostly a matter of adding the proper types to

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1542?email_source=notifications&email_token=AAMS4OBAFCJZ6IEG3JOR5UTQJQZ7PA5CNFSM4IWVM3PKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HLLGM7Q, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OHSN2H3KZO2TWSUQM3QJQZ7PANCNFSM4IWVM3PA .

mpdairy commented 5 years ago

Well, I don't have any particular file yet, but I want to specify a low level language, close to a lifted assembly language, and be able to type check for things like out of bounds array accesses.

So want to be able to do things like bitwise & and |, as well as zero extend and sign extend. Basically all the bitwise things that Z3 supports.

It looks like someone started making a LH spec for Data.Bits, but it was going to use int and I think would only be able to do easy things like bitshifts, which divide or multiply by 2.

Also, did you see my edited message about the problem of using the smt-lib BitVec type? I accidentally opened the issue when I was only half-way done creating it, so the version github emailed you didn't have much.

nikivazou commented 5 years ago

Since the systax of bitvector SMT-sorts is not supported, we need to hardcode the sorts in the theories supported by LH (e.g., as we did for sets: https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/Smt/Theories.hs#L68). This is not very difficult, so if you make a concrete example, I can add this support.

Regarding the n parameter, Haskell's Data.BitVector.BV is not parametric, so it is not clear how to connect this Haskell type to an SMT Bitvector with varying length. Again, starting with a concrete example would clear things up.

mpdairy commented 5 years ago

Ok, I'll make a little concrete example. If I used something like this (http://hackage.haskell.org/package/bv-sized-0.7.0/docs/Data-BitVector-Sized.html) for my bitvectors in Haskell, would the Nat size parameter allow you to create BVs in Smt? If so, I'll just use those, unless you have another recommendation.

nikivazou commented 5 years ago

Liquid Haskell knows about type literals, so I think we can use the Nat parameter to pass to the SMT the proper information.

mpdairy commented 4 years ago

Sorry I took so long! I was on vacation. Here's a demo module that uses the bv-sized library:

{-# LANGUAGE DataKinds #-}
{-@ LIQUID "--no-termination" @-}

module Demo where

import           Prelude
import qualified Data.BitVector.Sized as BV
import           Data.BitVector.Sized                   ( BitVector, bvWidth )

-- bvWidth :: BitVector w -> Int
{-@ measure bvWidth @-}

type BitVec a = BitVector a

{-@ udiv :: a:BitVec x -> {b:BitVec x | b /= 0} -> {r:BitVec x | r == a `div` b} @-}
udiv :: BitVec x -> BitVec x -> BitVec x
udiv = BV.bvQuotU

-- I don't see zeroExt in the official SMT-LIB spec, but z3 has it
-- so I'm assuming it can be done:
-- z3.zeroExt : i -> BV n -> BV (n + i)

-- zero extend to Word
{-@ zx_w :: {bv:BitVec a | bvWidth bv <= 16}  -> {r:BitVec 16 | z3.zeroExt (16 - bvWidth bv) bv} @-}
zx_w :: BitVec a -> BitVec 16
zx_w = BV.bvZext

-- zero extend to double Word
{-@ zx_d :: {bv:BitVec a | bvWidth bv <= 32}  -> {r:BitVec 32 | z3.zeroExt (16 - bvWidth bv) bv} @-}
zx_d :: BitVec a -> BitVec 32
zx_d = BV.bvZext

{-@ (&) :: bv1:BitVec x -> bv2:BitVec x  -> {r:BitVec x | r == bvand bv1 bv2} @-}
(&) :: BitVec a -> BitVec a -> BitVec a
(&) = BV.bvAnd

-- z3.extract :: BV -> high bit -> low bit -> BV
{-@ trunc_b :: {bv:BitVec x | bvWidth bv >= 8} -> {r:BitVec 8 | r == z3.extract bv 8 0 @-}
trunc_b :: BitVec x -> BitVec 8
trunc_b = BV.bvExtract 0

{-@ trunc_w :: {bv:BitVec x | bvWidth bv >= 16} -> {r:BitVec 16 | r == z3.extract bv 16 0 @-}
trunc_w :: BitVec x -> BitVec 16
trunc_w = BV.bvExtract 0

--works with 0x0020 but fails with 0x0200
bad1 :: BitVec 16 -> Maybe (BitVec 32)
bad1 bv
  | bv == 0 = Nothing
  | otherwise = Just $ udiv (0xFFFFFFFF :: BitVec 32) (zx_d $ trunc_b bv)

--fails with 0x1000
bad2 :: BitVec 16 -> Maybe (BitVec 32)
bad2 bv
  | bv == 0 = Nothing
  | otherwise = Just $ udiv (0xFFFFFFFF :: BitVec 32) (zx_d $ bv & 0xEFFF)

good :: BitVec 16 -> Maybe (BitVec 32)
good bv
  | bv == 0 = Nothing
  | otherwise = Just $ udiv (0xFFFFFFFF :: BitVec 32) (zx_d bv)

So I'm hoping that LH will be able to tell me that my bad functions could result in a divide-by-zero error. These are very contrived examples, but that's the sort of thing I would like to be able to type check.

I sort of just guessed at what the LH annotations would be. There were a couple functions I am familiar with from Z3 which I couldn't find in the SMT-LIB bitvec specification (http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml), like zero extend and sign extend, but I'm hoping those can somehow be created using SMT-LIB functions.

mpdairy commented 4 years ago

Let me know if you want me to make a little repo with my demo file and a working stack.yaml.

mpdairy commented 4 years ago

If somebody could give me a brief overview of what needs to be done to get this added, I'll take a stab at it.

ranjitjhala commented 4 years ago

Hi Matt,

Sorry have been a bit tied up with stuff; I'll try to take a look at this tonight!

You (probably) don't have to fiddle too much with Z3 because liquid-fixpoint the backend constraint solver we use to interface to SMT has some code for this to support bitvector literals and bit-wise and/or, e.g. see

https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/Smt/Theories.hs#L348-L349

One way to make progress and understand the whole picture is to figure out what it would take to verify a smaller subset of the above, e.g.

{-@ (&) :: bv1:BitVec x -> bv2:BitVec x -> {r:BitVec x | r == bvand bv1
bv2} @-}
(&) :: BitVec a -> BitVec a -> BitVec a
(&) = BV.bvAnd

zero :: BitVec 16
zero = ... -- Haskell repr. of bit-vector 0

test :: _ -> {v:_ | v = Refinement repr. of bit-vector 0}
test n = zero & n

Specifically, how to map

Haskell constants into bit-vector literals in SMT (the same way we do for string/integer literals)
Use connect FIXPOINT's bvAnd with the Haskell one.

This is mostly a matter of figuring out how all these are implemented for existing theories, e.g. Sets...

Ranjit.
Ranjit.

On Thu, Sep 26, 2019 at 7:29 PM Matt Parker notifications@github.com wrote:

If somebody could give me a brief overview of what needs to be done to get this added, I'll take a stab at it.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1542?email_source=notifications&email_token=AAMS4OF7GGIPSOVTGR2PNLDQLVVWPA5CNFSM4IWVM3PKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7XQSCY#issuecomment-535759115, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OHJI74SJK6DRPITUKLQLVVWPANCNFSM4IWVM3PA .

nmeum commented 7 months ago

I believe support for BitVector theories was added to liquid-fixpoint last year: https://github.com/ucsd-progsys/liquid-fixpoint/pull/642

I guess this just needs to be integrated with LH now?

ranjitjhala commented 7 months ago

Yes, I think it's just a matter of integrating with LH, which is rather mechanical, but rather sadly undocumented :-( The key bit is to

Either refine some existing Haskell bitvector API to track the semantics of the operations in the types,
or, define some new library Language.Haskell.Liquid.Bitvector (like Language.Haskell.Liquid.Bag) which exposes the same refined operations.

If you have some small example of the sort of thing you'd like checked, I can take a whack at writing out?

On Thu, Feb 8, 2024 at 4:25 AM Sören Tempel @.***> wrote:

I believe support for BitVector theories was added to liquid-fixpoint last year: ucsd-progsys/liquid-fixpoint#642 https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/pull/642__;!!Mih3wA!B51aHPCjjU2gEjyXFOaOXHfHU_0lKgP5mfjzgEFtlHAWyLem9GB3lQ6wPkVpZLncyS1IJDoXXmcxV51Xzqc0e5tR$

I guess this just needs to be integrated with LH now?

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1542*issuecomment-1934009207__;Iw!!Mih3wA!B51aHPCjjU2gEjyXFOaOXHfHU_0lKgP5mfjzgEFtlHAWyLem9GB3lQ6wPkVpZLncyS1IJDoXXmcxV51XzkjAg0ms$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OG24LL3E5HX56DZUM3YSS7ZRAVCNFSM4IWVM3PKU5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJTGQYDAOJSGA3Q__;!!Mih3wA!B51aHPCjjU2gEjyXFOaOXHfHU_0lKgP5mfjzgEFtlHAWyLem9GB3lQ6wPkVpZLncyS1IJDoXXmcxV51XzlcxpYfB$ . You are receiving this because you commented.Message ID: @.***>

--

Ranjit.

nmeum commented 7 months ago

I am just looking for a simple BitVector library that exposes the arithmetic and logic operations that Z3 provides on bitvectors (e.g. bvslt, bvsge, bvadd, bvmul, …). If you could show me how to define a basic BitVector type in LH and map that to the BitVec sort, then I might be able to do the more mechanical parts?

I started experimenting a bit with refining the existing bv module as proposed in the original issue:

import qualified Data.BitVector as BV

{-@ embed Data.BitVector.BV as BitVec @-}

{-@ define Data.BitVector.BV.sge = bvsge @-}
{-@ define Data.BitVector.BV.slt = bvslt @-}

{-@ measure bvsge :: BV.BV -> BV.BV -> Bool @-}
{-@ measure bvslt :: BV.BV -> BV.BV -> Bool @-}

{-@ bvSlt :: x:BV.BV -> y:BV.BV -> { v:Bool | v <=> not (x bvsge y) }  @-}
bvSlt :: BV.BV -> BV.BV -> Bool
bvSlt x y = BV.slt x y

But this gives me:

test.hs:11:14: error:
    • Illegal type specification for `Main.bvSlt`
    Main.bvSlt :: x:Data.BitVector.BV -> y:Data.BitVector.BV -> {v : GHC.Types.Bool | v <=> not (x bvsge y)}
    Sort Error in Refinement: {v : bool | v <=> not (x bvsge y)}
    The sort BitVec is not a function with at least 1 arguments

    Just
    •
   |
11 | {-@ bvSlt :: x:BV.BV -> y:BV.BV -> { v:Bool | v <=> not (x bvsge y) }  @-}
   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

Any hints on how to resolve that would be much appreciated. As you said, there is not a lot of documentation, so this is just what I came up with by grepping through the existing source. I hope it's not entirely the wrong approach...

ucsd-progsys / liquidhaskell

Bitvector support #1542