msakai / toysolver / 813

Committed 18 Jun 2026 03:47PM UTC coverage: 70.362% (-0.4%) from 70.748%

Build # 813

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #209 from msakai/feature/bv-zero-division

Update the semantics of zero division on bitvectors to conform to SMT-LIB >=2.6

Coverage Stats

5 of 7 new or added lines in 2 files covered. (71.43%)

127 existing lines in 10 files now uncovered.

11272 of 16020 relevant lines covered (70.36%)

0.7 hits per line

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

44.23

/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.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

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

msakai / toysolver / 813

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