1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.BitPrecise.BitTricks
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Checks the correctness of a few tricks from the large collection found in:
-- <http://graphics.stanford.edu/~seander/bithacks.html>
-----------------------------------------------------------------------------
{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.BitPrecise.BitTricks where
import Data.SBV
-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>
fastMinCorrect :: SInt32 -> SInt32 -> SBool
fastMinCorrect x y = m .== fm
where m = ite (x .< y) x y
fm = y `xor` ((x `xor` y) .&. (-(oneIf (x .< y))));
-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax>
fastMaxCorrect :: SInt32 -> SInt32 -> SBool
fastMaxCorrect x y = m .== fm
where m = ite (x .< y) y x
fm = x `xor` ((x `xor` y) .&. (-(oneIf (x .< y))));
-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns>
oppositeSignsCorrect :: SInt32 -> SInt32 -> SBool
oppositeSignsCorrect x y = r .== os
where r = (x .< 0 .&& y .>= 0) .|| (x .>= 0 .&& y .< 0)
os = (x `xor` y) .< 0
-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching>
conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool
conditionalSetClearCorrect f m w = r .== r'
where r = ite f (w .|. m) (w .&. complement m)
r' = w `xor` ((-(oneIf f) `xor` w) .&. m);
-- | Formalizes <http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>
powerOfTwoCorrect :: SWord32 -> SBool
powerOfTwoCorrect v = f .== s
where f = (v ./= 0) .&& ((v .&. (v-1)) .== 0);
powers :: [Word32]
powers = map ((2::Word32)^) [(0::Word32) .. 31]
s = sAny (v .==) $ map literal powers
-- | Collection of queries
queries :: IO ()
queries =
let check w t = do putStr $ "Proving " ++ show w ++ ": "
print =<< prove t
in do check "Fast min " fastMinCorrect
check "Fast max " fastMaxCorrect
check "Opposite signs " oppositeSignsCorrect
check "Conditional set/clear" conditionalSetClearCorrect
check "PowerOfTwo " powerOfTwoCorrect
|
