msakai / toysolver / 767

Committed 22 May 2025 12:57PM UTC coverage: 71.847% (-0.06%) from 71.906%

Build # 767

Build Type

push

github

Committed by

web-flow

Commit Message

Merge f4d92f6d1 into c10d256d2

Run Details

11104 of 15455 relevant lines covered (71.85%)

0.72 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

44.69

/src/ToySolver/BitVector/Base.hs

{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.BitVector.Base
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.BitVector.Base
  (
  -- * BitVector values
    BV
  , bv2nat
  , nat2bv
  , fromAscBits
  , fromDescBits
  , toAscBits
  , toDescBits
  , IsBV (..)

  -- * BitVector language
  , Var (..)
  , Expr (..)
  , Op1 (..)
  , Op2 (..)
  , repeat
  , zeroExtend
  , signExtend
  , Atom (..)
  , BVComparison (..)
  , module ToySolver.Data.OrdRel
  , Model
  , evalExpr
  , evalAtom
  ) where

import Prelude hiding (repeat)
import Data.Bits
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Ord
import qualified Data.Semigroup as Semigroup
import qualified Data.Vector as V
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Unboxed as VU
import ToySolver.Data.Boolean
import ToySolver.Data.OrdRel

class Monoid a => IsBV a where
  width :: a -> Int
  extract :: Int -> Int -> a -> a
  fromBV :: BV -> a

  bvnot  :: a -> a
  bvand  :: a -> a -> a
  bvor   :: a -> a -> a
  bvxor  :: a -> a -> a
  bvnand :: a -> a -> a
  bvnor  :: a -> a -> a
  bvxnor :: a -> a -> a

  bvneg  :: a -> a
  bvadd  :: a -> a -> a
  bvsub  :: a -> a -> a
  bvmul  :: a -> a -> a
  bvudiv :: a -> a -> a
  bvurem :: a -> a -> a
  bvsdiv :: a -> a -> a
  bvsrem :: a -> a -> a
  bvsmod :: a -> a -> a
  bvshl  :: a -> a -> a
  bvlshr :: a -> a -> a
  bvashr :: a -> a -> a
  bvcomp :: a -> a -> a

  bvnand s t = bvnot (bvand s t)
  bvnor s t  = bvnot (bvor s t)
  bvxnor s t = bvnot (bvxor s t)

  bvsub s t = bvadd s (bvneg t)

repeat :: Monoid m => Int -> m -> m
repeat i x = mconcat (replicate i x)

zeroExtend :: IsBV a => Int -> a -> a
zeroExtend i s = fromAscBits (replicate i False) <> s

signExtend :: IsBV a => Int -> a -> a
signExtend i s
  | w == 0 = fromAscBits (replicate i False)
  | otherwise = repeat i (extract (w-1) (w-1) s) <> s
  where
    w = width s

class (IsBV a, IsEqRel a (ComparisonResult a), Complement (ComparisonResult a)) => BVComparison a where
  type ComparisonResult a

  bvule, bvult, bvuge, bvugt, bvsle, bvslt, bvsge, bvsgt :: a -> a -> ComparisonResult a

  bvule a b = notB (bvult b a)
  bvult a b = notB (bvule b a)
  bvuge a b = bvule b a
  bvugt a b = bvult b a

  bvsle a b = notB (bvslt b a)
  bvslt a b = notB (bvsle b a)
  bvsge a b = bvsle b a
  bvsgt a b = bvslt b a

  {-# MINIMAL (bvule | bvult), (bvsle | bvslt) #-}

-- ------------------------------------------------------------------------

newtype BV = BV (VU.Vector Bool)
  deriving (Eq)

instance Ord BV where
  compare (BV bs1) (BV bs2) =
    (comparing VG.length <> comparing VG.reverse) bs1 bs2

instance Semigroup.Semigroup BV where
  BV hi <> BV lo = BV (lo <> hi)

instance Monoid BV where
  mempty = BV VG.empty

instance Show BV where
  show bv = "0b" ++ [if b then '1' else '0' | b <- toDescBits bv]

instance Bits BV where
  (.&.) = bvand
  (.|.) = bvor
  xor = bvxor
  complement = bvnot

  shiftL x i
    | i < w = extract (w-1-i) 0 x <> nat2bv i 0
    | otherwise = nat2bv w 0
    where
      w = width x
  shiftR x i
    | i < w = nat2bv i 0 <> extract (w-1) i x
    | otherwise = nat2bv w 0
    where
      w = width x
  rotateL x i
    | w == 0 = x
    | otherwise = extract (w-1-j) 0 x <> extract (w-1) (w-j) x
    where
      w = width x
      j = i `mod` w
  rotateR x i
    | w == 0 = x
    | otherwise = extract (j-1) 0 x <> extract (w-1) j x
    where
      w = width x
      j = i `mod` w

  zeroBits = error "zeroBits is not implemented"

  bit = error "bit is not implemented"

  setBit x@(BV bs) i
    | 0 <= i && i < w = BV $ bs VG.// [(i,True)]
    | otherwise = x
    where
      w = width x
  clearBit x@(BV bs) i
    | 0 <= i && i < w = BV $ bs VG.// [(i,False)]
    | otherwise = x
    where
      w = width x
  complementBit x@(BV bs) i
    | 0 <= i && i < w = BV $ bs VG.// [(i, not (testBit x i))]
    | otherwise = x
    where
      w = width x
  testBit x@(BV bs) i
    | 0 <= i && i < w = bs VG.! i
    | otherwise = False
    where
      w = width x

  popCount x = sum [1 | b <- toAscBits x, b]

  bitSizeMaybe _ = Nothing
  bitSize _ = error "bitSize is not implemented"
  isSigned _ = False

instance IsBV BV where
  width (BV bs) = VG.length bs
  extract i j (BV bs) = BV $ VG.slice j (i - j + 1) bs
  fromBV = id

  bvnot (BV bs) = BV $ VG.map not bs

  bvand (BV bs1) (BV bs2)
    | VG.length bs1 /= VG.length bs2 = error "width mismatch"
    | otherwise = BV $ VG.zipWith (&&) bs1 bs2
  bvor (BV bs1) (BV bs2)
    | VG.length bs1 /= VG.length bs2 = error "width mismatch"
    | otherwise = BV $ VG.zipWith (||) bs1 bs2
  bvxor (BV bs1) (BV bs2)
    | VG.length bs1 /= VG.length bs2 = error "width mismatch"
    | otherwise = BV $ VG.zipWith (/=) bs1 bs2

  bvneg x = nat2bv (width x) $ 2 ^ width x - bv2nat x

  bvadd x y
    | width x /= width y = error "invalid width"
    | otherwise = nat2bv (width x) (bv2nat x + bv2nat y)

  bvmul x y
    | width x /= width y = error "invalid width"
    | otherwise = nat2bv (width x) (bv2nat x * bv2nat y)

  bvudiv x y
    | width x /= width y = error "invalid width"
    | y' == 0 = error "division by zero"
    | otherwise = nat2bv (width x) (bv2nat x `div` y')
    where
      y' :: Integer
      y' = bv2nat y

  bvurem x y
    | width x /= width y = error "invalid width"
    | y' == 0 = error "division by zero"
    | otherwise = nat2bv (width x) (bv2nat x `mod` y')
    where
      y' :: Integer
      y' = bv2nat y

  bvsdiv x y
    | width x < 1 || width y < 1 || width x /= width y = error "invalid width"
    | not msb_x && not msb_y = bvudiv x y
    | msb_x && not msb_y = bvneg $ bvudiv (bvneg x) y
    | not msb_x && msb_y = bvneg $ bvudiv x (bvneg y)
    | otherwise = bvudiv (bvneg x) (bvneg y)
    where
      msb_x = testBit x (width x - 1)
      msb_y = testBit y (width y - 1)

  bvsrem x y
    | width x < 1 || width y < 1 || width x /= width y = error "invalid width"
    | not msb_x && not msb_y = bvurem x y
    | msb_x && not msb_y = bvneg $ bvurem (bvneg x) y
    | not msb_x && msb_y = bvurem x (bvneg y)
    | otherwise = bvneg $ bvurem (bvneg x) (bvneg y)
    where
      msb_x = testBit x (width x - 1)
      msb_y = testBit y (width y - 1)

  bvsmod x y
    | width x < 1 || width y < 1 || width x /= width y = error "invalid width"
    | bv2nat u == (0::Integer) = u
    | not msb_x && not msb_y = u
    | msb_x && not msb_y = bvadd (bvneg u) y
    | not msb_x && msb_y = bvadd u y
    | otherwise = bvneg u
    where
      msb_x = testBit x (width x - 1)
      msb_y = testBit y (width y - 1)
      abs_x = if msb_x then bvneg x else x
      abs_y = if msb_y then bvneg y else y
      u = bvurem abs_x abs_y

  bvshl  x y
    | width x /= width y = error "invalid width"
    | otherwise = nat2bv (width x) (bv2nat x `shiftL` bv2nat y)

  bvlshr x y
    | width x /= width y = error "invalid width"
    | otherwise = nat2bv (width x) (bv2nat x `shiftR` bv2nat y)

  bvashr x y
    | width x /= width y = error "invalid width"
    | not msb_x = bvlshr x y
    | otherwise = bvneg $ bvlshr (bvneg x) y
    where
      msb_x = testBit x (width x - 1)

  bvcomp x y
    | width x /= width y = error "invalid width"
    | otherwise = nat2bv 1 (if x==y then 1 else 0)

instance IsEqRel BV Bool where
  (.==.) = (==)
  (./=.) = (/=)

instance BVComparison BV where
  type ComparisonResult BV = Bool

  bvule = (<=)

  bvsle bs1 bs2
    | width bs1 /= width bs2 = error ("length mismatch: " ++ show (width bs1) ++ " and " ++ show (width bs2))
    | w == 0 = true
    | otherwise = bs1_msb && not bs2_msb || (bs1_msb == bs2_msb) && bs1 <= bs2
    where
      w = width bs1
      bs1_msb = testBit bs1 (w-1)
      bs2_msb = testBit bs2 (w-1)

bv2nat :: Integral a => BV -> a
bv2nat (BV bv) = VG.ifoldl' (\r i x -> if x then r+2^i else r) 0 bv

nat2bv :: IsBV a => Int -> Integer -> a
nat2bv m x = fromBV $ BV $ VG.generate m (testBit x)

fromAscBits :: IsBV a => [Bool] -> a
fromAscBits = fromBV . BV . VG.fromList

fromDescBits :: IsBV a => [Bool] -> a
fromDescBits = fromBV . fromAscBits . reverse

toAscBits :: BV -> [Bool]
toAscBits (BV bs) = VG.toList bs

toDescBits :: BV -> [Bool]
toDescBits = reverse . toAscBits

-- ------------------------------------------------------------------------

data Var
  = Var
  { varWidth :: {-# UNPACK #-} !Int
  , varId :: {-# UNPACK #-} !Int
  }
  deriving (Eq, Ord, Show)

data Expr
  = EConst BV
  | EVar Var
  | EOp1 Op1 Expr
  | EOp2 Op2 Expr Expr
  deriving (Eq, Ord, Show)

data Op1
  = OpExtract !Int !Int
  | OpNot
  | OpNeg
  deriving (Eq, Ord, Show)

data Op2
  = OpConcat
  | OpAnd
  | OpOr
  | OpXOr
  | OpComp
  | OpAdd
  | OpMul
  | OpUDiv
  | OpURem
  | OpSDiv
  | OpSRem
  | OpSMod
  | OpShl
  | OpLShr
  | OpAShr
  deriving (Eq, Ord, Enum, Bounded, Show)

instance IsBV Expr where
  width (EConst x) = width x
  width (EVar v) = varWidth v
  width (EOp1 op arg) =
    case op of
      OpExtract i j -> i - j + 1
      _ -> width arg
  width (EOp2 op arg1 arg2) =
    case op of
      OpConcat -> width arg1 + width arg2
      OpComp -> 1
      _ -> width arg1

  extract i j = EOp1 (OpExtract i j)

  fromBV = EConst

  bvnot = EOp1 OpNot
  bvand = EOp2 OpAnd
  bvor  = EOp2 OpOr
  bvxor = EOp2 OpXOr

  bvneg  = EOp1 OpNeg
  bvadd  = EOp2 OpAdd
  bvmul  = EOp2 OpMul
  bvudiv = EOp2 OpUDiv
  bvurem = EOp2 OpURem
  bvsdiv = EOp2 OpSDiv
  bvsrem = EOp2 OpSRem
  bvsmod = EOp2 OpSMod
  bvshl  = EOp2 OpShl
  bvlshr = EOp2 OpLShr
  bvashr = EOp2 OpAShr
  bvcomp = EOp2 OpComp

instance Semigroup.Semigroup Expr where
  (<>) = EOp2 OpConcat

instance Monoid Expr where
  mempty = EConst mempty

instance Bits Expr where
  (.&.) = bvand
  (.|.) = bvor
  xor = bvxor
  complement = bvnot
  shiftL x i
    | i < w = extract (w-1-i) 0 x <> nat2bv i 0
    | otherwise = nat2bv w 0
    where
      w = width x
  shiftR x i
    | i < w = nat2bv i 0 <> extract (w-1) i x
    | otherwise = nat2bv w 0
    where
      w = width x
  rotateL x i
    | w == 0 = x
    | otherwise = extract (w-1-j) 0 x <> extract (w-1) (w-j) x
    where
      w = width x
      j = i `mod` w
  rotateR x i
    | w == 0 = x
    | otherwise = extract (j-1) 0 x <> extract (w-1) j x
    where
      w = width x
      j = i `mod` w

  zeroBits = error "zeroBits is not implemented"

  bit = error "bit is not implemented"

  setBit x i
    | 0 <= i && i < w = extract (w-1) (i+1) x <> fromDescBits [True] <> extract (i-1) 0 x
    | otherwise = x
    where
      w = width x

  clearBit x i
    | 0 <= i && i < w = extract (w-1) (i+1) x <> fromDescBits [False] <> extract (i-1) 0 x
    | otherwise = x
    where
      w = width x

  complementBit x i
    | 0 <= i && i < w = extract (w-1) (i+1) x <> bvnot (extract i i x) <> extract (i-1) 0 x
    | otherwise = x
    where
      w = width x

  testBit = error "testBit is not implemented"

  popCount = error "popCount is not implemented"

  bitSizeMaybe _ = Nothing
  bitSize _ = error "bitSize is not implemented"
  isSigned _ = False

data Atom = Rel (OrdRel Expr) Bool
  deriving (Eq, Ord, Show)

instance Complement Atom where
  notB (Rel rel signed) = Rel (notB rel) signed

instance IsEqRel Expr Atom where
  a .==. b = Rel (a .==. b) False
  a ./=. b = Rel (a ./=. b) False

instance BVComparison Expr where
  type ComparisonResult Expr = Atom

  bvule s t = Rel (s .<=. t) False
  bvult s t = Rel (s .<.  t) False
  bvuge s t = Rel (s .>=. t) False
  bvugt s t = Rel (s .>.  t) False
  bvsle s t = Rel (s .<=. t) True
  bvslt s t = Rel (s .<.  t) True
  bvsge s t = Rel (s .>=. t) True
  bvsgt s t = Rel (s .>.  t) True

-- ------------------------------------------------------------------------

type Model = (V.Vector BV, Map BV BV, Map BV BV)

evalExpr :: Model -> Expr -> BV
evalExpr (env, divTable, remTable) = f
  where
    f (EConst bv) = bv
    f (EVar v) = env VG.! varId v
    f (EOp1 op x) = evalOp1 op (f x)
    f (EOp2 op x y) = evalOp2 op (f x) (f y)

    evalOp1 (OpExtract i j) = extract i j
    evalOp1 OpNot = bvnot
    evalOp1 OpNeg = bvneg

    evalOp2 OpConcat a b = a <> b
    evalOp2 OpAnd x y = bvand x y
    evalOp2 OpOr x y = bvor x y
    evalOp2 OpXOr x y = bvxor x y
    evalOp2 OpAdd x y = bvadd x y
    evalOp2 OpMul x y = bvmul x y
    evalOp2 OpUDiv x y
      | y' /= 0 = bvudiv x y
      | otherwise =
          case Map.lookup x divTable of
            Just d -> d
            Nothing -> nat2bv (width x) 0
      where
        y' :: Integer
        y' = bv2nat y
    evalOp2 OpURem x y
      | y' /= 0 = bvurem x y
      | otherwise =
          case Map.lookup x remTable of
            Just r -> r
            Nothing -> nat2bv (width x) 0
      where
        y' :: Integer
        y' = bv2nat y
    evalOp2 OpSDiv x y
      | width x < 1 || width y < 1 || width x /= width y = error "invalid width"
      | not msb_x && not msb_y = evalOp2 OpUDiv x y
      | msb_x && not msb_y = bvneg $ evalOp2 OpUDiv (bvneg x) y
      | not msb_x && msb_y = bvneg $ evalOp2 OpUDiv x (bvneg y)
      | otherwise = evalOp2 OpUDiv (bvneg x) (bvneg y)
      where
        msb_x = testBit x (width x - 1)
        msb_y = testBit y (width y - 1)
    evalOp2 OpSRem x y
      | width x < 1 || width y < 1 || width x /= width y = error "invalid width"
      | not msb_x && not msb_y = evalOp2 OpURem x y
      | msb_x && not msb_y = bvneg $ evalOp2 OpURem (bvneg x) y
      | not msb_x && msb_y = evalOp2 OpURem x (bvneg y)
      | otherwise = bvneg $ evalOp2 OpURem (bvneg x) (bvneg y)
      where
        msb_x = testBit x (width x - 1)
        msb_y = testBit y (width y - 1)
    evalOp2 OpSMod x y
      | width x < 1 || width y < 1 || width x /= width y = error "invalid width"
      | bv2nat u == (0::Integer) = u
      | not msb_x && not msb_y = u
      | msb_x && not msb_y = bvadd (bvneg u) y
      | not msb_x && msb_y = bvadd u y
      | otherwise = bvneg u
      where
        msb_x = testBit x (width x - 1)
        msb_y = testBit y (width y - 1)
        abs_x = if msb_x then bvneg x else x
        abs_y = if msb_y then bvneg y else y
        u = evalOp2 OpURem abs_x abs_y
    evalOp2 OpShl x y = bvshl x y
    evalOp2 OpLShr x y = bvlshr x y
    evalOp2 OpAShr x y = bvashr x y
    evalOp2 OpComp x y = nat2bv 1 (if x==y then 1 else 0)

evalAtom :: Model -> Atom -> Bool
evalAtom m (Rel (OrdRel lhs op rhs) False) = evalOp op (evalExpr m lhs) (evalExpr m rhs)
evalAtom m (Rel (OrdRel lhs op rhs) True) =
  case op of
    Lt -> bvslt lhs' rhs'
    Gt -> bvslt rhs' lhs'
    Le -> bvsle lhs' rhs'
    Ge -> bvsle rhs' lhs'
    Eql -> lhs' == rhs'
    NEq -> lhs' /= rhs'
  where
    lhs' = evalExpr m lhs
    rhs' = evalExpr m rhs

1	{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE FlexibleContexts #-}
4	{-# LANGUAGE MultiParamTypeClasses #-}
5	{-# LANGUAGE TypeFamilies #-}
6	-----------------------------------------------------------------------------
7	-- \|
8	-- Module : ToySolver.BitVector.Base
9	-- Copyright : (c) Masahiro Sakai 2016
10	-- License : BSD-style
11	--
12	-- Maintainer : masahiro.sakai@gmail.com
13	-- Stability : experimental
14	-- Portability : non-portable
15	--
16	-----------------------------------------------------------------------------
17	module ToySolver.BitVector.Base
18	(
19	-- * BitVector values
20	BV
21	, bv2nat
22	, nat2bv
23	, fromAscBits
24	, fromDescBits
25	, toAscBits
26	, toDescBits
27	, IsBV (..)
28
29	-- * BitVector language
30	, Var (..)
31	, Expr (..)
32	, Op1 (..)
33	, Op2 (..)
34	, repeat
35	, zeroExtend
36	, signExtend
37	, Atom (..)
38	, BVComparison (..)
39	, module ToySolver.Data.OrdRel
40	, Model
41	, evalExpr
42	, evalAtom
43	) where
44
45	import Prelude hiding (repeat)
46	import Data.Bits
47	import Data.Map (Map)
48	import qualified Data.Map as Map
49	import Data.Ord
50	import qualified Data.Semigroup as Semigroup
51	import qualified Data.Vector as V
52	import qualified Data.Vector.Generic as VG
53	import qualified Data.Vector.Unboxed as VU
54	import ToySolver.Data.Boolean
55	import ToySolver.Data.OrdRel
56
57	class Monoid a => IsBV a where
58	width :: a -> Int
59	extract :: Int -> Int -> a -> a
60	fromBV :: BV -> a
61
62	bvnot :: a -> a
63	bvand :: a -> a -> a
64	bvor :: a -> a -> a
65	bvxor :: a -> a -> a
66	bvnand :: a -> a -> a
67	bvnor :: a -> a -> a
68	bvxnor :: a -> a -> a
69
70	bvneg :: a -> a
71	bvadd :: a -> a -> a
72	bvsub :: a -> a -> a
73	bvmul :: a -> a -> a
74	bvudiv :: a -> a -> a
75	bvurem :: a -> a -> a
76	bvsdiv :: a -> a -> a
77	bvsrem :: a -> a -> a
78	bvsmod :: a -> a -> a
79	bvshl :: a -> a -> a
80	bvlshr :: a -> a -> a
81	bvashr :: a -> a -> a
82	bvcomp :: a -> a -> a
83
84	bvnand s t = bvnot (bvand s t)	1✔
85	bvnor s t = bvnot (bvor s t)	1✔
86	bvxnor s t = bvnot (bvxor s t)	1✔
87
88	bvsub s t = bvadd s (bvneg t)	1✔
89
90	repeat :: Monoid m => Int -> m -> m
91	repeat i x = mconcat (replicate i x)	×
92
93	zeroExtend :: IsBV a => Int -> a -> a
94	zeroExtend i s = fromAscBits (replicate i False) <> s	×
95
96	signExtend :: IsBV a => Int -> a -> a
97	signExtend i s	×
98	\| w == 0 = fromAscBits (replicate i False)	×
99	\| otherwise = repeat i (extract (w-1) (w-1) s) <> s	×
100	where
101	w = width s	×
102
103	class (IsBV a, IsEqRel a (ComparisonResult a), Complement (ComparisonResult a)) => BVComparison a where
104	type ComparisonResult a
105
106	bvule, bvult, bvuge, bvugt, bvsle, bvslt, bvsge, bvsgt :: a -> a -> ComparisonResult a
107
108	bvule a b = notB (bvult b a)	×
109	bvult a b = notB (bvule b a)	1✔
110	bvuge a b = bvule b a	1✔
111	bvugt a b = bvult b a	1✔
112
113	bvsle a b = notB (bvslt b a)	×
114	bvslt a b = notB (bvsle b a)	1✔
115	bvsge a b = bvsle b a	1✔
116	bvsgt a b = bvslt b a	1✔
117
118	{-# MINIMAL (bvule \| bvult), (bvsle \| bvslt) #-}
119
120	-- ------------------------------------------------------------------------
121
122	newtype BV = BV (VU.Vector Bool)
123	deriving (Eq)	1✔
124
125	instance Ord BV where	×
126	compare (BV bs1) (BV bs2) =	1✔
127	(comparing VG.length <> comparing VG.reverse) bs1 bs2	1✔
128
129	instance Semigroup.Semigroup BV where	×
130	BV hi <> BV lo = BV (lo <> hi)	1✔
131
132	instance Monoid BV where	×
133	mempty = BV VG.empty	×
134
135	instance Show BV where	×
136	show bv = "0b" ++ [if b then '1' else '0' \| b <- toDescBits bv]	1✔
137
138	instance Bits BV where	×
139	(.&.) = bvand	×
140	(.\|.) = bvor	×
141	xor = bvxor	×
142	complement = bvnot	×
143
144	shiftL x i	×
145	\| i < w = extract (w-1-i) 0 x <> nat2bv i 0	×
146	\| otherwise = nat2bv w 0	×
147	where
148	w = width x	×
149	shiftR x i	×
150	\| i < w = nat2bv i 0 <> extract (w-1) i x	×
151	\| otherwise = nat2bv w 0	×
152	where
153	w = width x	×
154	rotateL x i	×
155	\| w == 0 = x	×
156	\| otherwise = extract (w-1-j) 0 x <> extract (w-1) (w-j) x	×
157	where
158	w = width x	×
159	j = i `mod` w	×
160	rotateR x i	×
161	\| w == 0 = x	×
162	\| otherwise = extract (j-1) 0 x <> extract (w-1) j x	×
163	where
164	w = width x	×
165	j = i `mod` w	×
166
167	zeroBits = error "zeroBits is not implemented"	×
168
169	bit = error "bit is not implemented"	×
170
171	setBit x@(BV bs) i	×
172	\| 0 <= i && i < w = BV $ bs VG.// [(i,True)]	×
173	\| otherwise = x	×
174	where
175	w = width x	×
176	clearBit x@(BV bs) i	×
177	\| 0 <= i && i < w = BV $ bs VG.// [(i,False)]	×
178	\| otherwise = x	×
179	where
180	w = width x	×
181	complementBit x@(BV bs) i	×
182	\| 0 <= i && i < w = BV $ bs VG.// [(i, not (testBit x i))]	×
183	\| otherwise = x	×
184	where
185	w = width x	×
186	testBit x@(BV bs) i	1✔
187	\| 0 <= i && i < w = bs VG.! i	×
188	\| otherwise = False	×
189	where
190	w = width x	1✔
191
192	popCount x = sum [1 \| b <- toAscBits x, b]	×
193
194	bitSizeMaybe _ = Nothing	×
195	bitSize _ = error "bitSize is not implemented"	×
196	isSigned _ = False	×
197
198	instance IsBV BV where	×
199	width (BV bs) = VG.length bs	1✔
200	extract i j (BV bs) = BV $ VG.slice j (i - j + 1) bs	1✔
201	fromBV = id	1✔
202
203	bvnot (BV bs) = BV $ VG.map not bs	1✔
204
205	bvand (BV bs1) (BV bs2)	1✔
206	\| VG.length bs1 /= VG.length bs2 = error "width mismatch"	×
207	\| otherwise = BV $ VG.zipWith (&&) bs1 bs2	×
208	bvor (BV bs1) (BV bs2)	1✔
209	\| VG.length bs1 /= VG.length bs2 = error "width mismatch"	×
210	\| otherwise = BV $ VG.zipWith (\|\|) bs1 bs2	×
211	bvxor (BV bs1) (BV bs2)	1✔
212	\| VG.length bs1 /= VG.length bs2 = error "width mismatch"	×
213	\| otherwise = BV $ VG.zipWith (/=) bs1 bs2	×
214
215	bvneg x = nat2bv (width x) $ 2 ^ width x - bv2nat x	1✔
216
217	bvadd x y	1✔
218	\| width x /= width y = error "invalid width"	×
219	\| otherwise = nat2bv (width x) (bv2nat x + bv2nat y)	×
220
221	bvmul x y	1✔
222	\| width x /= width y = error "invalid width"	×
223	\| otherwise = nat2bv (width x) (bv2nat x * bv2nat y)	×
224
225	bvudiv x y	1✔
226	\| width x /= width y = error "invalid width"	×
227	\| y' == 0 = error "division by zero"	×
228	\| otherwise = nat2bv (width x) (bv2nat x `div` y')	×
229	where
230	y' :: Integer
231	y' = bv2nat y	1✔
232
233	bvurem x y	1✔
234	\| width x /= width y = error "invalid width"	×
235	\| y' == 0 = error "division by zero"	×
236	\| otherwise = nat2bv (width x) (bv2nat x `mod` y')	×
237	where
238	y' :: Integer
239	y' = bv2nat y	1✔
240
241	bvsdiv x y	×
242	\| width x < 1 \|\| width y < 1 \|\| width x /= width y = error "invalid width"	×
243	\| not msb_x && not msb_y = bvudiv x y	×
244	\| msb_x && not msb_y = bvneg $ bvudiv (bvneg x) y	×
245	\| not msb_x && msb_y = bvneg $ bvudiv x (bvneg y)	×
246	\| otherwise = bvudiv (bvneg x) (bvneg y)	×
247	where
248	msb_x = testBit x (width x - 1)	×
249	msb_y = testBit y (width y - 1)	×
250
251	bvsrem x y	×
252	\| width x < 1 \|\| width y < 1 \|\| width x /= width y = error "invalid width"	×
253	\| not msb_x && not msb_y = bvurem x y	×
254	\| msb_x && not msb_y = bvneg $ bvurem (bvneg x) y	×
255	\| not msb_x && msb_y = bvurem x (bvneg y)	×
256	\| otherwise = bvneg $ bvurem (bvneg x) (bvneg y)	×
257	where
258	msb_x = testBit x (width x - 1)	×
259	msb_y = testBit y (width y - 1)	×
260
261	bvsmod x y	×
262	\| width x < 1 \|\| width y < 1 \|\| width x /= width y = error "invalid width"	×
263	\| bv2nat u == (0::Integer) = u	×
264	\| not msb_x && not msb_y = u	×
265	\| msb_x && not msb_y = bvadd (bvneg u) y	×
266	\| not msb_x && msb_y = bvadd u y	×
267	\| otherwise = bvneg u	×
268	where
269	msb_x = testBit x (width x - 1)	×
270	msb_y = testBit y (width y - 1)	×
271	abs_x = if msb_x then bvneg x else x	×
272	abs_y = if msb_y then bvneg y else y	×
273	u = bvurem abs_x abs_y	×
274
275	bvshl x y	1✔
276	\| width x /= width y = error "invalid width"	×
277	\| otherwise = nat2bv (width x) (bv2nat x `shiftL` bv2nat y)	×
278
279	bvlshr x y	1✔
280	\| width x /= width y = error "invalid width"	×
281	\| otherwise = nat2bv (width x) (bv2nat x `shiftR` bv2nat y)	×
282
283	bvashr x y	1✔
284	\| width x /= width y = error "invalid width"	×
285	\| not msb_x = bvlshr x y	1✔
286	\| otherwise = bvneg $ bvlshr (bvneg x) y	×
287	where
288	msb_x = testBit x (width x - 1)	1✔
289
290	bvcomp x y	×
291	\| width x /= width y = error "invalid width"	×
292	\| otherwise = nat2bv 1 (if x==y then 1 else 0)	×
293
294	instance IsEqRel BV Bool where
295	(.==.) = (==)	×
296	(./=.) = (/=)	×
297
298	instance BVComparison BV where	1✔
299	type ComparisonResult BV = Bool
300
301	bvule = (<=)	1✔
302
303	bvsle bs1 bs2	1✔
304	\| width bs1 /= width bs2 = error ("length mismatch: " ++ show (width bs1) ++ " and " ++ show (width bs2))	×
305	\| w == 0 = true	1✔
306	\| otherwise = bs1_msb && not bs2_msb \|\| (bs1_msb == bs2_msb) && bs1 <= bs2	×
307	where
308	w = width bs1	1✔
309	bs1_msb = testBit bs1 (w-1)	1✔
310	bs2_msb = testBit bs2 (w-1)	1✔
311
312	bv2nat :: Integral a => BV -> a
313	bv2nat (BV bv) = VG.ifoldl' (\r i x -> if x then r+2^i else r) 0 bv	1✔
314
315	nat2bv :: IsBV a => Int -> Integer -> a
316	nat2bv m x = fromBV $ BV $ VG.generate m (testBit x)	1✔
317
318	fromAscBits :: IsBV a => [Bool] -> a
319	fromAscBits = fromBV . BV . VG.fromList	1✔
320
321	fromDescBits :: IsBV a => [Bool] -> a
322	fromDescBits = fromBV . fromAscBits . reverse	1✔
323
324	toAscBits :: BV -> [Bool]
325	toAscBits (BV bs) = VG.toList bs	1✔
326
327	toDescBits :: BV -> [Bool]
328	toDescBits = reverse . toAscBits	1✔
329
330	-- ------------------------------------------------------------------------
331
332	data Var
333	= Var
334	{ varWidth :: {-# UNPACK #-} !Int	1✔
335	, varId :: {-# UNPACK #-} !Int	1✔
336	}
337	deriving (Eq, Ord, Show)	×
338
339	data Expr
340	= EConst BV
341	\| EVar Var
342	\| EOp1 Op1 Expr
343	\| EOp2 Op2 Expr Expr
344	deriving (Eq, Ord, Show)	×
345
346	data Op1
347	= OpExtract !Int !Int
348	\| OpNot
349	\| OpNeg
350	deriving (Eq, Ord, Show)	×
351
352	data Op2
353	= OpConcat
354	\| OpAnd
355	\| OpOr
356	\| OpXOr
357	\| OpComp
358	\| OpAdd
359	\| OpMul
360	\| OpUDiv
361	\| OpURem
362	\| OpSDiv
363	\| OpSRem
364	\| OpSMod
365	\| OpShl
366	\| OpLShr
367	\| OpAShr
368	deriving (Eq, Ord, Enum, Bounded, Show)	×
369
370	instance IsBV Expr where	1✔
371	width (EConst x) = width x	1✔
372	width (EVar v) = varWidth v	1✔
373	width (EOp1 op arg) =
374	case op of	1✔
375	OpExtract i j -> i - j + 1	1✔
376	_ -> width arg	1✔
377	width (EOp2 op arg1 arg2) =
378	case op of	1✔
379	OpConcat -> width arg1 + width arg2	1✔
380	OpComp -> 1	×
381	_ -> width arg1	1✔
382
383	extract i j = EOp1 (OpExtract i j)	1✔
384
385	fromBV = EConst	1✔
386
387	bvnot = EOp1 OpNot	1✔
388	bvand = EOp2 OpAnd	1✔
389	bvor = EOp2 OpOr	1✔
390	bvxor = EOp2 OpXOr	1✔
391
392	bvneg = EOp1 OpNeg	1✔
393	bvadd = EOp2 OpAdd	1✔
394	bvmul = EOp2 OpMul	1✔
395	bvudiv = EOp2 OpUDiv	1✔
396	bvurem = EOp2 OpURem	1✔
397	bvsdiv = EOp2 OpSDiv	1✔
398	bvsrem = EOp2 OpSRem	1✔
399	bvsmod = EOp2 OpSMod	1✔
400	bvshl = EOp2 OpShl	1✔
401	bvlshr = EOp2 OpLShr	1✔
402	bvashr = EOp2 OpAShr	1✔
403	bvcomp = EOp2 OpComp	1✔
404
405	instance Semigroup.Semigroup Expr where	×
406	(<>) = EOp2 OpConcat	1✔
407
408	instance Monoid Expr where	×
409	mempty = EConst mempty	×
410
411	instance Bits Expr where	×
412	(.&.) = bvand	×
413	(.\|.) = bvor	×
414	xor = bvxor	×
415	complement = bvnot	×
416	shiftL x i	×
417	\| i < w = extract (w-1-i) 0 x <> nat2bv i 0	×
418	\| otherwise = nat2bv w 0	×
419	where
420	w = width x	×
421	shiftR x i	×
422	\| i < w = nat2bv i 0 <> extract (w-1) i x	×
423	\| otherwise = nat2bv w 0	×
424	where
425	w = width x	×
426	rotateL x i	×
427	\| w == 0 = x	×
428	\| otherwise = extract (w-1-j) 0 x <> extract (w-1) (w-j) x	×
429	where
430	w = width x	×
431	j = i `mod` w	×
432	rotateR x i	×
433	\| w == 0 = x	×
434	\| otherwise = extract (j-1) 0 x <> extract (w-1) j x	×
435	where
436	w = width x	×
437	j = i `mod` w	×
438
439	zeroBits = error "zeroBits is not implemented"	×
440
441	bit = error "bit is not implemented"	×
442
443	setBit x i	×
444	\| 0 <= i && i < w = extract (w-1) (i+1) x <> fromDescBits [True] <> extract (i-1) 0 x	×
445	\| otherwise = x	×
446	where
447	w = width x	×
448
449	clearBit x i	×
450	\| 0 <= i && i < w = extract (w-1) (i+1) x <> fromDescBits [False] <> extract (i-1) 0 x	×
451	\| otherwise = x	×
452	where
453	w = width x	×
454
455	complementBit x i	×
456	\| 0 <= i && i < w = extract (w-1) (i+1) x <> bvnot (extract i i x) <> extract (i-1) 0 x	×
457	\| otherwise = x	×
458	where
459	w = width x	×
460
461	testBit = error "testBit is not implemented"	×
462
463	popCount = error "popCount is not implemented"	×
464
465	bitSizeMaybe _ = Nothing	×
466	bitSize _ = error "bitSize is not implemented"	×
467	isSigned _ = False	×
468
469	data Atom = Rel (OrdRel Expr) Bool
470	deriving (Eq, Ord, Show)	×
471
472	instance Complement Atom where
473	notB (Rel rel signed) = Rel (notB rel) signed	1✔
474
475	instance IsEqRel Expr Atom where
476	a .==. b = Rel (a .==. b) False	1✔
477	a ./=. b = Rel (a ./=. b) False	1✔
478
479	instance BVComparison Expr where
480	type ComparisonResult Expr = Atom
481
482	bvule s t = Rel (s .<=. t) False	1✔
483	bvult s t = Rel (s .<. t) False	1✔
484	bvuge s t = Rel (s .>=. t) False	1✔
485	bvugt s t = Rel (s .>. t) False	1✔
486	bvsle s t = Rel (s .<=. t) True	1✔
487	bvslt s t = Rel (s .<. t) True	1✔
488	bvsge s t = Rel (s .>=. t) True	1✔
489	bvsgt s t = Rel (s .>. t) True	1✔
490
491	-- ------------------------------------------------------------------------
492
493	type Model = (V.Vector BV, Map BV BV, Map BV BV)
494
495	evalExpr :: Model -> Expr -> BV
496	evalExpr (env, divTable, remTable) = f	1✔
497	where
498	f (EConst bv) = bv	1✔
499	f (EVar v) = env VG.! varId v	1✔
500	f (EOp1 op x) = evalOp1 op (f x)	1✔
501	f (EOp2 op x y) = evalOp2 op (f x) (f y)	1✔
502
503	evalOp1 (OpExtract i j) = extract i j	1✔
504	evalOp1 OpNot = bvnot	1✔
505	evalOp1 OpNeg = bvneg	1✔
506
507	evalOp2 OpConcat a b = a <> b	1✔
508	evalOp2 OpAnd x y = bvand x y	1✔
509	evalOp2 OpOr x y = bvor x y	1✔
510	evalOp2 OpXOr x y = bvxor x y	1✔
511	evalOp2 OpAdd x y = bvadd x y	1✔
512	evalOp2 OpMul x y = bvmul x y	1✔
513	evalOp2 OpUDiv x y
514	\| y' /= 0 = bvudiv x y	1✔
515	\| otherwise =	×
516	case Map.lookup x divTable of	1✔
517	Just d -> d	1✔
518	Nothing -> nat2bv (width x) 0	×
519	where
520	y' :: Integer
521	y' = bv2nat y	1✔
522	evalOp2 OpURem x y
523	\| y' /= 0 = bvurem x y	1✔
524	\| otherwise =	×
525	case Map.lookup x remTable of	1✔
526	Just r -> r	1✔
527	Nothing -> nat2bv (width x) 0	×
528	where
529	y' :: Integer
530	y' = bv2nat y	1✔
531	evalOp2 OpSDiv x y
532	\| width x < 1 \|\| width y < 1 \|\| width x /= width y = error "invalid width"	×
533	\| not msb_x && not msb_y = evalOp2 OpUDiv x y	1✔
534	\| msb_x && not msb_y = bvneg $ evalOp2 OpUDiv (bvneg x) y	1✔
535	\| not msb_x && msb_y = bvneg $ evalOp2 OpUDiv x (bvneg y)	1✔
536	\| otherwise = evalOp2 OpUDiv (bvneg x) (bvneg y)	×
537	where
538	msb_x = testBit x (width x - 1)	1✔
539	msb_y = testBit y (width y - 1)	1✔
540	evalOp2 OpSRem x y
541	\| width x < 1 \|\| width y < 1 \|\| width x /= width y = error "invalid width"	×
542	\| not msb_x && not msb_y = evalOp2 OpURem x y	1✔
543	\| msb_x && not msb_y = bvneg $ evalOp2 OpURem (bvneg x) y	1✔
544	\| not msb_x && msb_y = evalOp2 OpURem x (bvneg y)	1✔
545	\| otherwise = bvneg $ evalOp2 OpURem (bvneg x) (bvneg y)	×
546	where
547	msb_x = testBit x (width x - 1)	1✔
548	msb_y = testBit y (width y - 1)	1✔
549	evalOp2 OpSMod x y
550	\| width x < 1 \|\| width y < 1 \|\| width x /= width y = error "invalid width"	×
551	\| bv2nat u == (0::Integer) = u	1✔
552	\| not msb_x && not msb_y = u	1✔
553	\| msb_x && not msb_y = bvadd (bvneg u) y	1✔
554	\| not msb_x && msb_y = bvadd u y	×
555	\| otherwise = bvneg u	×
556	where
557	msb_x = testBit x (width x - 1)	1✔
558	msb_y = testBit y (width y - 1)	1✔
559	abs_x = if msb_x then bvneg x else x	1✔
560	abs_y = if msb_y then bvneg y else y	1✔
561	u = evalOp2 OpURem abs_x abs_y	1✔
562	evalOp2 OpShl x y = bvshl x y	1✔
563	evalOp2 OpLShr x y = bvlshr x y	1✔
564	evalOp2 OpAShr x y = bvashr x y	1✔
565	evalOp2 OpComp x y = nat2bv 1 (if x==y then 1 else 0)	×
566
567	evalAtom :: Model -> Atom -> Bool
568	evalAtom m (Rel (OrdRel lhs op rhs) False) = evalOp op (evalExpr m lhs) (evalExpr m rhs)	1✔
569	evalAtom m (Rel (OrdRel lhs op rhs) True) =
570	case op of	1✔
571	Lt -> bvslt lhs' rhs'	1✔
572	Gt -> bvslt rhs' lhs'	1✔
573	Le -> bvsle lhs' rhs'	1✔
574	Ge -> bvsle rhs' lhs'	1✔
575	Eql -> lhs' == rhs'	1✔
576	NEq -> lhs' /= rhs'	1✔
577	where
578	lhs' = evalExpr m lhs	1✔
579	rhs' = evalExpr m rhs	1✔

msakai / toysolver / 767

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous