-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMapTest.hs
158 lines (127 loc) · 6.22 KB
/
MapTest.hs
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
module MapTest where
import Map
import Control.Applicative
import qualified Data.List as L
import Test.Target
--------------------------------------------------------------------
-- Target
--------------------------------------------------------------------
-- The values aren't interesting in terms of the properties we want to check,
-- so treat the Map as a Set to reduce the search space
type K = Char
type V = ()
type M = Map Char ()
prop_difference_lc :: M -> M -> M
prop_difference_lc = difference
prop_delete_lc :: K -> M -> M
prop_delete_lc = delete
-- liquidTests :: [(String, Test)]
liquidTests = [ ('insert, T (insert :: K -> V -> M -> M))
, ('delete, T (delete :: K -> M -> M))
, ('union, T (union :: M -> M -> M))
, ('difference, T (difference :: M -> M -> M))
, ('intersection, T (intersection :: M -> M -> M))
]
-- liquidTests_bad :: [(String, Test)]
liquidTests_bad = [ ('insert, T (insert_bad :: K -> V -> M -> M))
, ('delete, T (delete_bad :: K -> M -> M))
, ('union, T (union_bad :: M -> M -> M))
, ('difference, T (difference_bad :: M -> M -> M))
, ('intersection, T (intersection_bad :: M -> M -> M))
]
insert_bad = go
where
go :: Ord k => k -> a -> Map k a -> Map k a
go kx x Tip = singleton kx x
go kx x (Bin sz ky y l r) =
case compare kx ky of
-- Bin ky y (go kx x l) r
--LIQUID: swapped balanceL and balanceR to inject bug
LT -> balanceR ky y (go kx x l) r
GT -> balanceL ky y l (go kx x r)
EQ -> Bin sz kx x l r
delete_bad = go
where
go :: Ord k => k -> Map k a -> Map k a
go _ Tip = Tip
go k (Bin _ kx x l r) =
case compare k kx of
--LIQUID: swapped balanceL and balanceR to inject bug
LT -> balanceL kx x (go k l) r
GT -> balanceR kx x l (go k r)
EQ -> glue kx l r
--LIQUID: having trouble injecting bugs here..
glue_bad :: k -> Map k a -> Map k a -> Map k a
glue_bad _ Tip r = r
glue_bad _ l Tip = l
glue_bad kcut l r
| size l > size r = let (km, m, l') = deleteFindMax l in balanceR km m l' r
| otherwise = let (km, m, r') = deleteFindMin r in balanceL km m l r'
union_bad :: Ord k => Map k a -> Map k a -> Map k a
union_bad Tip t2 = t2
union_bad t1 Tip = t1
union_bad t1 t2 = hedgeUnion_bad NothingS NothingS t1 t2
hedgeUnion_bad :: Ord a => MaybeS a -> MaybeS a -> Map a b -> Map a b -> Map a b
hedgeUnion_bad _ _ t1 Tip = t1
--LIQUID: injected bug in join'
hedgeUnion_bad blo bhi Tip (Bin _ kx x l r) = join'_bad kx x (filterGt blo l) (filterLt bhi r)
hedgeUnion_bad _ _ t1 (Bin _ kx x Tip Tip) = insertR kx x t1 -- According to benchmarks, this special case increases
-- performance up to 30%. It does not help in difference or intersection.
hedgeUnion_bad blo bhi (Bin _ kx x l r) t2 = join'_bad kx x (hedgeUnion_bad blo bmi l (trim blo bmi t2))
(hedgeUnion_bad bmi bhi r (trim bmi bhi t2))
where bmi = JustS kx
join'_bad kx x Tip r = insertMin kx x r
join'_bad kx x l Tip = insertMax kx x l
join'_bad kx x l@(Bin sizeL ky y ly ry) r@(Bin sizeR kz z lz rz)
--LIQUID changed both < to > to inject bug
| delta*sizeL > sizeR = balanceL kz z (join'_bad kx x l lz) rz
| delta*sizeR > sizeL = balanceR ky y ly (join'_bad kx x ry r)
| otherwise = bin kx x l r
difference_bad :: Ord k => Map k a -> Map k b -> Map k a
difference_bad Tip _ = Tip
difference_bad t1 Tip = t1
difference_bad t1 t2 = hedgeDiff_bad NothingS NothingS t1 t2
hedgeDiff_bad :: Ord a => MaybeS a -> MaybeS a -> Map a b -> Map a c -> Map a b
hedgeDiff_bad _ _ Tip _ = Tip
hedgeDiff_bad blo bhi (Bin _ kx x l r) Tip = join'_bad kx x (filterGt blo l) (filterLt bhi r)
hedgeDiff_bad blo bhi t (Bin _ kx _ l r) = merge_bad kx (hedgeDiff_bad blo bmi (trim_bad blo bmi t) l)
(hedgeDiff_bad bmi bhi (trim_bad bmi bhi t) r)
where bmi = JustS kx
--LIQUID: having trouble injecting bug here
merge_bad _ Tip r = r
merge_bad _ l Tip = l
merge_bad kcut l@(Bin sizeL kx x lx rx) r@(Bin sizeR ky y ly ry)
| delta*sizeL > sizeR = balanceL ky y (merge_bad kcut l ly) ry
| delta*sizeR > sizeL = balanceR kx x lx (merge_bad kcut rx r)
| otherwise = glue kcut l r
intersection_bad :: Ord k => Map k a -> Map k b -> Map k a
intersection_bad Tip _ = Tip
intersection_bad _ Tip = Tip
intersection_bad t1 t2 = hedgeInt_bad NothingS NothingS t1 t2
hedgeInt_bad :: Ord k => MaybeS k -> MaybeS k -> Map k a -> Map k b -> Map k a
hedgeInt_bad _ _ _ Tip = Tip
hedgeInt_bad _ _ Tip _ = Tip
hedgeInt_bad blo bhi (Bin _ kx x l r) t2 = let l' = hedgeInt_bad blo bmi l (trim_bad blo bmi t2)
r' = hedgeInt_bad bmi bhi r (trim_bad bmi bhi t2)
in if kx `member` t2 then join' kx x l' r' else merge kx l' r'
where bmi = JustS kx
trim_bad :: Ord k => MaybeS k -> MaybeS k -> Map k a -> Map k a
trim_bad NothingS NothingS t = t
trim_bad (JustS lk) NothingS t = greater lk t
--LIQUID: change <= to >=
where greater lo t@(Bin _ k _ _ r) | k >= lo = greater lo r
| otherwise = t
greater _ t'@Tip = t'
trim_bad NothingS (JustS hk) t = lesser hk t
--LIQUID: change >= to <=
where lesser hi t'@(Bin _ k _ l _) | k <= hi = lesser hi l
| otherwise = t'
lesser _ t'@Tip = t'
trim_bad (JustS lk) (JustS hk) t = middle lk hk t
where middle lo hi t'@(Bin _ k _ l r) | k <= lo = middle lo hi r
| k >= hi = middle lo hi l
| otherwise = t'
middle _ _ t'@Tip = t'