1------------------------------------------------------------------------
2-- |
3-- Module      : What4.SWord
4-- Description : Dynamically-sized bitvector values
5-- Copyright   : Galois, Inc. 2018-2020
6-- License     : BSD3
7-- Maintainer  : rdockins@galois.com
8-- Stability   : experimental
9-- Portability : non-portable (language extensions)
10--
11-- A wrapper for What4 bitvectors so that the width is not tracked
12-- statically.
13------------------------------------------------------------------------
14
15{-# LANGUAGE ConstraintKinds #-}
16{-# LANGUAGE DataKinds #-}
17{-# LANGUAGE DeriveTraversable #-}
18{-# LANGUAGE DeriveFoldable #-}
19{-# LANGUAGE DeriveFunctor #-}
20{-# LANGUAGE DoAndIfThenElse #-}
21{-# LANGUAGE FlexibleContexts #-}
22{-# LANGUAGE FlexibleInstances #-}
23{-# LANGUAGE GADTs #-}
24{-# LANGUAGE LambdaCase #-}
25{-# LANGUAGE MultiParamTypeClasses #-}
26{-# LANGUAGE PatternGuards #-}
27{-# LANGUAGE PolyKinds #-}
28{-# LANGUAGE RankNTypes #-}
29{-# LANGUAGE ScopedTypeVariables #-}
30{-# LANGUAGE TypeFamilies #-}
31{-# LANGUAGE TypeOperators #-}
32{-# LANGUAGE TypeApplications #-}
33{-# LANGUAGE PartialTypeSignatures #-}
34
35module What4.SWord
36  ( SWord(..)
37  , bvAsSignedInteger
38  , bvAsUnsignedInteger
39  , integerToBV
40  , bvToInteger
41  , sbvToInteger
42  , freshBV
43  , bvWidth
44  , bvLit
45  , bvFill
46  , bvAtBE
47  , bvAtLE
48  , bvSetBE
49  , bvSetLE
50  , bvSliceBE
51  , bvSliceLE
52  , bvJoin
53  , bvIte
54  , bvPackBE
55  , bvPackLE
56  , bvUnpackBE
57  , bvUnpackLE
58  , bvForall
59  , unsignedBVBounds
60  , signedBVBounds
61
62    -- * Logic operations
63  , bvNot
64  , bvAnd
65  , bvOr
66  , bvXor
67
68    -- * Arithmetic operations
69  , bvNeg
70  , bvAdd
71  , bvSub
72  , bvMul
73  , bvUDiv
74  , bvURem
75  , bvSDiv
76  , bvSRem
77
78    -- * Comparison operations
79  , bvEq
80  , bvsle
81  , bvslt
82  , bvule
83  , bvult
84  , bvsge
85  , bvsgt
86  , bvuge
87  , bvugt
88  , bvIsNonzero
89
90    -- * bit-counting operations
91  , bvPopcount
92  , bvCountLeadingZeros
93  , bvCountTrailingZeros
94  , bvLg2
95
96    -- * Shift and rotates
97  , bvShl
98  , bvLshr
99  , bvAshr
100  , bvRol
101  , bvRor
102
103    -- * Zero- and sign-extend
104  , bvZext
105  , bvSext
106  ) where
107
108
109import           Data.Vector (Vector)
110import qualified Data.Vector as V
111import           Numeric.Natural
112
113import           GHC.TypeNats
114
115import qualified Data.BitVector.Sized as BV
116import           Data.Parameterized.NatRepr
117import           Data.Parameterized.Some(Some(..))
118
119import           What4.Interface(SymBV,Pred,SymInteger,IsExpr,SymExpr,IsExprBuilder,IsSymExprBuilder)
120import qualified What4.Interface as W
121import           What4.Panic (panic)
122
123-------------------------------------------------------------
124--
125-- | A What4 symbolic bitvector where the size does not appear in the type
126data SWord sym where
127
128  DBV :: (IsExpr (SymExpr sym), 1<=w) => SymBV sym w -> SWord sym
129  -- a bit-vector with positive length
130
131  ZBV :: SWord sym
132  -- a zero-length bit vector. i.e. 0
133
134
135instance Show (SWord sym) where
136  show (DBV bv) = show $ W.printSymExpr bv
137  show ZBV      = "0:[0]"
138
139-------------------------------------------------------------
140
141-- | Return the signed value if this is a constant bitvector
142bvAsSignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
143bvAsSignedInteger ZBV = Just 0
144bvAsSignedInteger (DBV (bv :: SymBV sym w)) =
145  BV.asSigned (W.bvWidth bv) <$> W.asBV bv
146
147-- | Return the unsigned value if this is a constant bitvector
148bvAsUnsignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
149bvAsUnsignedInteger ZBV = Just 0
150bvAsUnsignedInteger (DBV (bv :: SymBV sym w)) =
151  BV.asUnsigned <$> W.asBV bv
152
153
154unsignedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)
155unsignedBVBounds ZBV = Just (0, 0)
156unsignedBVBounds (DBV bv) = W.unsignedBVBounds bv
157
158signedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)
159signedBVBounds ZBV = Just (0, 0)
160signedBVBounds (DBV bv) = W.signedBVBounds bv
161
162
163-- | Convert an integer to an unsigned bitvector.
164--   The input value is reduced modulo 2^w.
165integerToBV :: forall sym width. (Show width, Integral width, IsExprBuilder sym) =>
166  sym ->  SymInteger sym -> width -> IO (SWord sym)
167integerToBV sym i w
168  | Just (Some wr) <- someNat w
169  , Just LeqProof  <- isPosNat wr
170  = DBV <$> W.integerToBV sym i wr
171  | 0 == toInteger w
172  = return ZBV
173  | otherwise
174  = panic "integerToBV" ["invalid bit-width", show w]
175
176-- | Interpret the bit-vector as an unsigned integer
177bvToInteger :: forall sym. (IsExprBuilder sym) =>
178  sym -> SWord sym -> IO (SymInteger sym)
179bvToInteger sym ZBV      = W.intLit sym 0
180bvToInteger sym (DBV bv) = W.bvToInteger sym bv
181
182-- | Interpret the bit-vector as a signed integer
183sbvToInteger :: forall sym. (IsExprBuilder sym) =>
184  sym -> SWord sym -> IO (SymInteger sym)
185sbvToInteger sym ZBV      = W.intLit sym 0
186sbvToInteger sym (DBV bv) = W.sbvToInteger sym bv
187
188
189-- | Get the width of a bitvector
190bvWidth :: forall sym. SWord sym -> Integer
191bvWidth (DBV x) = fromInteger (intValue (W.bvWidth x))
192bvWidth ZBV = 0
193
194-- | Create a bitvector with the given width and value
195bvLit :: forall sym. IsExprBuilder sym =>
196  sym -> Integer -> Integer -> IO (SWord sym)
197bvLit _ w _
198  | w == 0
199  = return ZBV
200bvLit sym w dat
201  | Just (Some rw) <- someNat w
202  , Just LeqProof <- isPosNat rw
203  = DBV <$> W.bvLit sym rw (BV.mkBV rw dat)
204  | otherwise
205  = panic "bvLit" ["size of bitvector is < 0 or >= maxInt", show w]
206
207
208freshBV :: forall sym. IsSymExprBuilder sym =>
209  sym -> W.SolverSymbol -> Integer -> IO (SWord sym)
210freshBV sym nm w
211  | w == 0
212  = return ZBV
213
214  | Just (Some rw) <- someNat w
215  , Just LeqProof <- isPosNat rw
216  = DBV <$> W.freshConstant sym nm (W.BaseBVRepr rw)
217
218  | otherwise
219  = panic "freshBV" ["size of bitvector is < 0 or >= maxInt", show w]
220
221
222bvFill :: forall sym. IsExprBuilder sym =>
223  sym -> Integer -> Pred sym -> IO (SWord sym)
224bvFill sym w p
225  | w == 0
226  = return ZBV
227
228  | Just (Some rw) <- someNat w
229  , Just LeqProof <- isPosNat rw
230  = DBV <$> W.bvFill sym rw p
231
232  | otherwise
233  = panic "bvFill" ["size of bitvector is < 0 or >= maxInt", show w]
234
235
236-- | Returns true if the corresponding bit in the bitvector is set.
237--   NOTE bits are numbered in big-endian ordering, meaning the
238--   most-significant bit is bit 0
239bvAtBE :: forall sym.
240  IsExprBuilder sym =>
241  sym ->
242  SWord sym ->
243  Integer {- ^ Index of bit (0 is the most significant bit) -} ->
244  IO (Pred sym)
245bvAtBE sym (DBV bv) i = do
246  let w   = natValue (W.bvWidth bv)
247  let idx = w - 1 - fromInteger i
248  W.testBitBV sym idx bv
249bvAtBE _ ZBV _ = panic "bvAtBE" ["cannot index into empty bitvector"]
250
251-- | Returns true if the corresponding bit in the bitvector is set.
252--   NOTE bits are numbered in little-endian ordering, meaning the
253--   least-significant bit is bit 0
254bvAtLE :: forall sym.
255  IsExprBuilder sym =>
256  sym ->
257  SWord sym ->
258  Integer {- ^ Index of bit (0 is the most significant bit) -} ->
259  IO (Pred sym)
260bvAtLE sym (DBV bv) i =
261  W.testBitBV sym (fromInteger i) bv
262bvAtLE _ ZBV _ = panic "bvAtLE" ["cannot index into empty bitvector"]
263
264-- | Set the numbered bit in the given bitvector to the given
265--   bit value.
266--   NOTE bits are numbered in big-endian ordering, meaning the
267--   most-significant bit is bit 0
268bvSetBE :: forall sym.
269  IsExprBuilder sym =>
270  sym ->
271  SWord sym ->
272  Integer {- ^ Index of bit (0 is the most significant bit) -} ->
273  Pred sym ->
274  IO (SWord sym)
275bvSetBE _ ZBV _ _ = return ZBV
276bvSetBE sym (DBV bv) i b =
277  do let w = natValue (W.bvWidth bv)
278     let idx = w - 1 - fromInteger i
279     DBV <$> W.bvSet sym bv idx b
280
281-- | Set the numbered bit in the given bitvector to the given
282--   bit value.
283--   NOTE bits are numbered in big-endian ordering, meaning the
284--   most-significant bit is bit 0
285bvSetLE :: forall sym.
286  IsExprBuilder sym =>
287  sym ->
288  SWord sym ->
289  Integer {- ^ Index of bit (0 is the most significant bit) -} ->
290  Pred sym ->
291  IO (SWord sym)
292bvSetLE _ ZBV _ _ = return ZBV
293bvSetLE sym (DBV bv) i b =
294  DBV <$> W.bvSet sym bv (fromInteger i) b
295
296
297-- | Concatenate two bitvectors.
298bvJoin  :: forall sym. IsExprBuilder sym => sym
299  -> SWord sym
300  -- ^ most significant bits
301  -> SWord sym
302  -- ^ least significant bits
303  -> IO (SWord sym)
304bvJoin _ x ZBV = return x
305bvJoin _ ZBV x = return x
306bvJoin sym (DBV bv1) (DBV bv2)
307  | LeqProof <- leqAddPos (W.bvWidth bv1) (W.bvWidth bv2)
308  = DBV <$> W.bvConcat sym bv1 bv2
309
310-- | Select a subsequence from a bitvector, with bits
311--   numbered in Big Endian order (most significant bit is 0).
312--   This fails if idx + n is >= w
313bvSliceBE :: forall sym. IsExprBuilder sym => sym
314  -> Integer
315  -- ^ Starting index, from 0 as most significant bit
316  -> Integer
317  -- ^ Number of bits to take (must be > 0)
318  -> SWord sym -> IO (SWord sym)
319bvSliceBE sym m n (DBV bv)
320  | Just (Some nr) <- someNat n,
321    Just LeqProof  <- isPosNat nr,
322    Just (Some mr) <- someNat m,
323    let wr = W.bvWidth bv,
324    Just LeqProof <- testLeq (addNat mr nr)  wr,
325    let idx = subNat wr (addNat mr nr),
326    Just LeqProof <- testLeq (addNat idx nr) wr
327  = DBV <$> W.bvSelect sym idx nr bv
328  | otherwise
329  = panic "bvSliceBE"
330      ["invalid arguments to slice: " ++ show m ++ " " ++ show n
331        ++ " from vector of length " ++ show (W.bvWidth bv)]
332bvSliceBE _ _ _ ZBV = return ZBV
333
334-- | Select a subsequence from a bitvector, with bits
335--   numbered in Little Endian order (least significant bit is 0).
336--   This fails if idx + n is >= w
337bvSliceLE :: forall sym. IsExprBuilder sym => sym
338  -> Integer
339  -- ^ Starting index, from 0 as most significant bit
340  -> Integer
341  -- ^ Number of bits to take (must be > 0)
342  -> SWord sym -> IO (SWord sym)
343bvSliceLE sym m n (DBV bv)
344  | Just (Some nr) <- someNat n,
345    Just LeqProof  <- isPosNat nr,
346    Just (Some mr) <- someNat m,
347    let wr = W.bvWidth bv,
348    Just LeqProof <- testLeq (addNat mr nr) wr
349  = DBV <$> W.bvSelect sym mr nr bv
350
351  | otherwise
352  = panic "bvSliceLE"
353      ["invalid arguments to slice: " ++ show m ++ " " ++ show n
354        ++ " from vector of length " ++ show (W.bvWidth bv)]
355bvSliceLE _ _ _ ZBV = return ZBV
356
357
358
359
360
361-- | Ceiling (log_2 x)
362-- adapted from saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
363w_bvLg2 :: forall sym w. (IsExprBuilder sym, 1 <= w) =>
364   sym -> SymBV sym w -> IO (SymBV sym w)
365w_bvLg2 sym x = go 0
366  where
367    w = W.bvWidth x
368    size :: Integer
369    size = intValue w
370    lit :: Integer -> IO (SymBV sym w)
371    -- BGS: This change could lead to some inefficency
372    lit n = W.bvLit sym w (BV.mkBV w n)
373    go :: Integer -> IO (SymBV sym w)
374    go i | i < size = do
375           x' <- lit (2 ^ i)
376           b' <- W.bvUle sym x x'
377           th <- lit i
378           el <- go (i + 1)
379           W.bvIte sym b' th el
380         | otherwise    = lit i
381
382-- | If-then-else applied to bitvectors.
383bvIte :: forall sym. IsExprBuilder sym =>
384  sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
385bvIte _ _ ZBV ZBV
386  = return ZBV
387bvIte sym p (DBV bv1) (DBV bv2)
388  | Just Refl <- testEquality (W.exprType bv1) (W.exprType bv2)
389  = DBV <$> W.bvIte sym p bv1 bv2
390bvIte _ _ x y
391  = panic "bvIte" ["bit-vectors don't have same length", show (bvWidth x), show (bvWidth y)]
392
393
394----------------------------------------------------------------------
395-- Convert to/from Vectors
396----------------------------------------------------------------------
397
398-- | Explode a bitvector into a vector of booleans in Big Endian
399--   order (most significant bit first)
400bvUnpackBE :: forall sym. IsExprBuilder sym =>
401  sym -> SWord sym -> IO (Vector (Pred sym))
402bvUnpackBE _   ZBV = return V.empty
403bvUnpackBE sym (DBV bv) = do
404  let w :: Natural
405      w = natValue (W.bvWidth bv)
406  V.generateM (fromIntegral w)
407              (\i -> W.testBitBV sym (w - 1 - fromIntegral i) bv)
408
409
410-- | Explode a bitvector into a vector of booleans in Little Endian
411--   order (least significant bit first)
412bvUnpackLE :: forall sym. IsExprBuilder sym =>
413  sym -> SWord sym -> IO (Vector (Pred sym))
414bvUnpackLE _   ZBV = return V.empty
415bvUnpackLE sym (DBV bv) = do
416  let w :: Natural
417      w = natValue (W.bvWidth bv)
418  V.generateM (fromIntegral w)
419              (\i -> W.testBitBV sym (fromIntegral i) bv)
420
421
422-- | convert a vector of booleans to a bitvector.  The input
423--   are used in Big Endian order (most significant bit first)
424bvPackBE :: forall sym. (W.IsExpr (W.SymExpr sym), IsExprBuilder sym) =>
425  sym -> Vector (Pred sym) -> IO (SWord sym)
426bvPackBE sym vec = do
427  vec' <- V.mapM (\p -> do
428                     v1 <- bvLit sym 1 1
429                     v2 <- bvLit sym 1 0
430                     bvIte sym p v1 v2) vec
431  V.foldM (\x y -> bvJoin sym x y) ZBV vec'
432
433
434-- | convert a vector of booleans to a bitvector.  The inputs
435--   are used in Little Endian order (least significant bit first)
436bvPackLE :: forall sym. (W.IsExpr (W.SymExpr sym), IsExprBuilder sym) =>
437  sym -> Vector (Pred sym) -> IO (SWord sym)
438bvPackLE sym vec = do
439  vec' <- V.mapM (\p -> do
440                     v1 <- bvLit sym 1 1
441                     v2 <- bvLit sym 1 0
442                     bvIte sym p v1 v2) vec
443  V.foldM (\x y -> bvJoin sym y x) ZBV vec'
444
445
446
447
448----------------------------------------------------------------------
449-- Generic wrapper for unary operators
450----------------------------------------------------------------------
451
452-- | Type of unary operation on bitvectors
453type SWordUn =
454  forall sym. IsExprBuilder sym =>
455  sym -> SWord sym -> IO (SWord sym)
456
457-- | Convert a unary operation on length indexed bvs to a unary operation
458-- on `SWord`
459bvUn ::  forall sym. IsExprBuilder sym =>
460   (forall w. 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)) ->
461   sym -> SWord sym -> IO (SWord sym)
462bvUn f sym (DBV bv) = DBV <$> f sym bv
463bvUn _ _  ZBV = return ZBV
464
465----------------------------------------------------------------------
466-- Generic wrapper for binary operators that take two words
467-- of the same length
468----------------------------------------------------------------------
469
470-- | type of binary operation that returns a bitvector
471type SWordBin =
472  forall sym. IsExprBuilder sym =>
473  sym -> SWord sym -> SWord sym -> IO (SWord sym)
474-- | type of binary operation that returns a boolean
475type PredBin =
476  forall sym. IsExprBuilder sym =>
477  sym -> SWord sym -> SWord sym -> IO (Pred sym)
478
479
480-- | convert binary operations that return bitvectors
481bvBin  :: forall sym. IsExprBuilder sym =>
482  (forall w. 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)) ->
483  sym -> SWord sym -> SWord sym -> IO (SWord sym)
484bvBin f sym (DBV bv1) (DBV bv2)
485  | Just Refl <- testEquality (W.exprType bv1) (W.exprType bv2)
486  = DBV <$> f sym bv1 bv2
487bvBin _ _ ZBV ZBV
488  = return ZBV
489bvBin _ _ x y
490  = panic "bvBin" ["bit-vectors don't have same length", show (bvWidth x), show (bvWidth y)]
491
492
493-- | convert binary operations that return booleans (Pred)
494bvBinPred  :: forall sym. IsExprBuilder sym =>
495  Bool {- ^ answer to give on 0-width bitvectors -} ->
496  (forall w. 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)) ->
497  sym -> SWord sym -> SWord sym -> IO (Pred sym)
498bvBinPred _ f sym x@(DBV bv1) y@(DBV bv2)
499  | Just Refl <- testEquality (W.exprType bv1) (W.exprType bv2)
500  = f sym bv1 bv2
501  | otherwise
502  = panic "bvBinPred" ["bit-vectors don't have same length", show (bvWidth x), show (bvWidth y)]
503bvBinPred b _ sym ZBV ZBV
504  = pure (W.backendPred sym b)
505bvBinPred _ _ _ x y
506  = panic "bvBinPred" ["bit-vectors don't have same length", show (bvWidth x), show (bvWidth y)]
507
508 -- Bitvector logical
509
510-- | Bitwise complement
511bvNot :: SWordUn
512bvNot = bvUn W.bvNotBits
513
514-- | Bitwise logical and.
515bvAnd :: SWordBin
516bvAnd = bvBin W.bvAndBits
517
518-- | Bitwise logical or.
519bvOr :: SWordBin
520bvOr = bvBin W.bvOrBits
521
522-- | Bitwise logical exclusive or.
523bvXor :: SWordBin
524bvXor = bvBin W.bvXorBits
525
526 -- Bitvector arithmetic
527
528-- | 2's complement negation.
529bvNeg :: SWordUn
530bvNeg = bvUn W.bvNeg
531
532-- | Add two bitvectors.
533bvAdd :: SWordBin
534bvAdd = bvBin W.bvAdd
535
536-- | Subtract one bitvector from another.
537bvSub :: SWordBin
538bvSub = bvBin W.bvSub
539
540-- | Multiply one bitvector by another.
541bvMul :: SWordBin
542bvMul = bvBin W.bvMul
543
544
545bvPopcount :: SWordUn
546bvPopcount = bvUn W.bvPopcount
547
548bvCountLeadingZeros :: SWordUn
549bvCountLeadingZeros = bvUn W.bvCountLeadingZeros
550
551bvCountTrailingZeros :: SWordUn
552bvCountTrailingZeros = bvUn W.bvCountTrailingZeros
553
554bvForall :: W.IsSymExprBuilder sym =>
555  sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym)
556bvForall sym n f =
557  case W.userSymbol "i" of
558    Left err -> panic "bvForall" [show err]
559    Right indexSymbol ->
560      case mkNatRepr n of
561        Some w
562          | Just LeqProof <- testLeq (knownNat @1) w ->
563              do i <- W.freshBoundVar sym indexSymbol $ W.BaseBVRepr w
564                 body <- f . DBV $ W.varExpr sym i
565                 W.forallPred sym i body
566          | otherwise -> f ZBV
567
568-- | Unsigned bitvector division.
569--
570--   The result is undefined when @y@ is zero,
571--   but is otherwise equal to @floor( x / y )@.
572bvUDiv :: SWordBin
573bvUDiv = bvBin W.bvUdiv
574
575
576-- | Unsigned bitvector remainder.
577--
578--   The result is undefined when @y@ is zero,
579--   but is otherwise equal to @x - (bvUdiv x y) * y@.
580bvURem :: SWordBin
581bvURem = bvBin W.bvUrem
582
583-- | Signed bitvector division.  The result is truncated to zero.
584--
585--   The result of @bvSdiv x y@ is undefined when @y@ is zero,
586--   but is equal to @floor(x/y)@ when @x@ and @y@ have the same sign,
587--   and equal to @ceiling(x/y)@ when @x@ and @y@ have opposite signs.
588--
589--   NOTE! However, that there is a corner case when dividing @MIN_INT@ by
590--   @-1@, in which case an overflow condition occurs, and the result is instead
591--   @MIN_INT@.
592bvSDiv :: SWordBin
593bvSDiv = bvBin W.bvSdiv
594
595-- | Signed bitvector remainder.
596--
597--   The result of @bvSrem x y@ is undefined when @y@ is zero, but is
598--   otherwise equal to @x - (bvSdiv x y) * y@.
599bvSRem :: SWordBin
600bvSRem = bvBin W.bvSrem
601
602bvLg2 :: SWordUn
603bvLg2 = bvUn w_bvLg2
604
605 -- Bitvector comparisons
606
607-- | Return true if bitvectors are equal.
608bvEq   :: PredBin
609bvEq = bvBinPred True W.bvEq
610
611-- | Signed less-than-or-equal.
612bvsle  :: PredBin
613bvsle = bvBinPred True W.bvSle
614
615-- | Signed less-than.
616bvslt  :: PredBin
617bvslt = bvBinPred False W.bvSlt
618
619-- | Unsigned less-than-or-equal.
620bvule  :: PredBin
621bvule = bvBinPred True W.bvUle
622
623-- | Unsigned less-than.
624bvult  :: PredBin
625bvult = bvBinPred False W.bvUlt
626
627-- | Signed greater-than-or-equal.
628bvsge  :: PredBin
629bvsge = bvBinPred True W.bvSge
630
631-- | Signed greater-than.
632bvsgt  :: PredBin
633bvsgt = bvBinPred False W.bvSgt
634
635-- | Unsigned greater-than-or-equal.
636bvuge  :: PredBin
637bvuge = bvBinPred True W.bvUge
638
639-- | Unsigned greater-than.
640bvugt  :: PredBin
641bvugt = bvBinPred False W.bvUgt
642
643bvIsNonzero :: IsExprBuilder sym => sym -> SWord sym -> IO (Pred sym)
644bvIsNonzero sym ZBV = return (W.falsePred sym)
645bvIsNonzero sym (DBV x) = W.bvIsNonzero sym x
646
647
648----------------------------------------
649-- Bitvector shifts and rotates
650----------------------------------------
651
652bvMax ::
653  (IsExprBuilder sym, 1 <= w) =>
654  sym ->
655  W.SymBV sym w ->
656  W.SymBV sym w ->
657  IO (W.SymBV sym w)
658bvMax sym x y =
659  do p <- W.bvUge sym x y
660     W.bvIte sym p x y
661
662reduceShift ::
663  IsExprBuilder sym =>
664  (forall w. (1 <= w) => sym -> W.SymBV sym w -> W.SymBV sym w -> IO (W.SymBV sym w)) ->
665  sym -> SWord sym -> SWord sym -> IO (SWord sym)
666reduceShift _wop _sym ZBV _ = return ZBV
667reduceShift _wop _sym x ZBV = return x
668reduceShift wop sym (DBV x) (DBV y) =
669  case compareNat (W.bvWidth x) (W.bvWidth y) of
670
671    -- already the same size, apply the operation
672    NatEQ -> DBV <$> wop sym x y
673
674    -- y is shorter, zero extend
675    NatGT _diff ->
676      do y' <- W.bvZext sym (W.bvWidth x) y
677         DBV <$> wop sym x y'
678
679    -- y is longer, clamp to the width of x then truncate.
680    -- Truncation is OK because the value will always fit after
681    -- clamping.
682    NatLT _diff ->
683      do wx <- W.bvLit sym (W.bvWidth y) (BV.mkBV (W.bvWidth y) (intValue (W.bvWidth x)))
684         y' <- W.bvTrunc sym (W.bvWidth x) =<< bvMax sym y wx
685         DBV <$> wop sym x y'
686
687reduceRotate ::
688  IsExprBuilder sym =>
689  (forall w. (1 <= w) => sym -> W.SymBV sym w -> W.SymBV sym w -> IO (W.SymBV sym w)) ->
690  sym -> SWord sym -> SWord sym -> IO (SWord sym)
691reduceRotate _wop _sym ZBV _ = return ZBV
692reduceRotate _wop _sym x ZBV = return x
693reduceRotate wop sym (DBV x) (DBV y) =
694  case compareNat (W.bvWidth x) (W.bvWidth y) of
695
696    -- already the same size, apply the operation
697    NatEQ -> DBV <$> wop sym x y
698
699    -- y is shorter, zero extend
700    NatGT _diff ->
701      do y' <- W.bvZext sym (W.bvWidth x) y
702         DBV <$> wop sym x y'
703
704    -- y is longer, reduce modulo the width of x, then truncate
705    -- Truncation is OK because the value will always
706    -- fit after modulo reduction
707    NatLT _diff ->
708      do wx <- W.bvLit sym (W.bvWidth y) (BV.mkBV (W.bvWidth y) (intValue (W.bvWidth x)))
709         y' <- W.bvTrunc sym (W.bvWidth x) =<< W.bvUrem sym y wx
710         DBV <$> wop sym x y'
711
712bvShl  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
713bvShl = reduceShift W.bvShl
714
715bvLshr  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
716bvLshr = reduceShift W.bvLshr
717
718bvAshr :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
719bvAshr = reduceShift W.bvAshr
720
721bvRol  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
722bvRol = reduceRotate W.bvRol
723
724bvRor  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
725bvRor = reduceRotate W.bvRor
726
727-- | Zero-extend a value, adding the specified number of bits.
728bvZext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)
729bvZext sym n sw =
730  case mkNatRepr n of
731    Some (nr :: NatRepr n) ->
732      case isPosNat nr of
733        Nothing -> pure sw
734        Just lp@LeqProof ->
735          case sw of
736            ZBV -> bvLit sym (toInteger n) 0
737            DBV (x :: W.SymBV sym w) ->
738              withLeqProof (leqAdd2 (leqRefl (W.bvWidth x)) lp :: LeqProof (w+1) (w+n)) $
739              withLeqProof (leqAdd LeqProof nr :: LeqProof 1 (w+n)) $
740              DBV <$> W.bvZext sym (addNat (W.bvWidth x) nr) x
741
742-- | Sign-extend a value, adding the specified number of bits.
743bvSext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)
744bvSext sym n sw =
745  case mkNatRepr n of
746    Some (nr :: NatRepr n) ->
747      case isPosNat nr of
748        Nothing -> pure sw
749        Just lp@LeqProof ->
750          case sw of
751            ZBV -> bvLit sym (toInteger n) 0
752            DBV (x :: W.SymBV sym w) ->
753              withLeqProof (leqAdd2 (leqRefl (W.bvWidth x)) lp :: LeqProof (w+1) (w+n)) $
754              withLeqProof (leqAdd LeqProof nr :: LeqProof 1 (w+n)) $
755              DBV <$> W.bvSext sym (addNat (W.bvWidth x) nr) x
756