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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE LambdaCase #-}
module SymFnTests where
import Control.Monad.IO.Class ( MonadIO, liftIO )
import Data.Parameterized.Classes ( ShowF(..) )
import Data.Parameterized.Context ( pattern (:>), (!) )
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Nonce
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC
import qualified Data.String as String
import qualified Data.Text as T
import qualified Data.Map as Map
import qualified Data.Map.Ordered as OMap
import Hedgehog
import qualified LibBF as BF
import Test.Tasty
import Test.Tasty.Hedgehog hiding (testProperty)
import SerializeTestUtils
import qualified What4.Expr.Builder as S
import What4.BaseTypes
import qualified What4.Interface as WI
import qualified What4.Serialize.Printer as WOUT
import qualified What4.Serialize.Parser as WIN
import qualified What4.Serialize.FastSExpr as WSF
import Prelude
symFnTests :: [TestTree]
symFnTests = [
testGroup "SymFns" (mconcat [
testBasicArguments WIN.parseSExpr
, testFunctionCalls WIN.parseSExpr
, testExpressions WIN.parseSExpr
, testBasicArguments WSF.parseSExpr
, testFunctionCalls WSF.parseSExpr
, testExpressions WSF.parseSExpr
])
]
data BuilderData t = NoBuilderData
floatSinglePrecision :: FloatPrecisionRepr Prec32
floatSinglePrecision = knownRepr
floatSingleType :: BaseTypeRepr (BaseFloatType Prec32)
floatSingleType = BaseFloatRepr floatSinglePrecision
testBasicArguments :: (T.Text -> Either String WIN.SExpr) -> [TestTree]
testBasicArguments parseSExpr =
[ testProperty "same argument type" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseIntegerRepr :> BaseIntegerRepr) $ \sym bvs -> do
let i1 = bvs ! Ctx.i1of2
let i2 = bvs ! Ctx.i2of2
WI.intAdd sym i1 i2
, testProperty "different argument types" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr) $ \sym bvs -> do
let i1 = bvs ! Ctx.i1of2
let b1 = bvs ! Ctx.i2of2
WI.baseTypeIte sym b1 i1 i1
]
testFunctionCalls :: (T.Text -> Either String WIN.SExpr) -> [TestTree]
testFunctionCalls parseSExpr =
[ testProperty "no arguments" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do
ufn <- WI.freshTotalUninterpFn sym (WI.safeSymbol "ufn") Ctx.empty BaseBoolRepr
WI.applySymFn sym ufn Ctx.empty
, testProperty "two inner arguments" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do
i1 <- WI.intLit sym 0
let b1 = WI.truePred sym
ufn <- WI.freshTotalUninterpFn sym (WI.safeSymbol "ufn") (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr) BaseBoolRepr
WI.applySymFn sym ufn (Ctx.empty :> i1 :> b1)
, testProperty "argument passthrough" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseBoolRepr :> BaseIntegerRepr) $ \sym bvs -> do
let i1 = bvs ! Ctx.i2of2
let b1 = bvs ! Ctx.i1of2
ufn <- WI.freshTotalUninterpFn sym (WI.safeSymbol "ufn") (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr) BaseBoolRepr
WI.applySymFn sym ufn (Ctx.empty :> i1 :> b1)
]
testExpressions :: (T.Text -> Either String WIN.SExpr) -> [TestTree]
testExpressions parseSExpr =
[ testProperty "negative ints" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do
WI.intLit sym (-1)
, testProperty "float lit" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do
WI.floatLit sym floatSinglePrecision (BF.bfFromInt 100)
, testProperty "simple struct" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr Ctx.empty $ \sym _ -> do
i1 <- WI.intLit sym 0
let b1 = WI.truePred sym
WI.mkStruct sym (Ctx.empty :> i1 :> b1)
, testProperty "struct field access" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseStructRepr (Ctx.empty :> BaseIntegerRepr :> BaseBoolRepr)) $ \sym bvs -> do
let struct = bvs ! Ctx.baseIndex
i1 <- WI.structField sym struct Ctx.i1of2
b1 <- WI.structField sym struct Ctx.i2of2
WI.mkStruct sym (Ctx.empty :> b1 :> i1)
--, testProperty "simple constant array" $
-- property $ mkEquivalenceTest Ctx.empty $ \sym _ -> do
-- i1 <- WI.intLit sym 1
-- WI.constantArray sym (Ctx.empty :> BaseIntegerRepr) i1
, testProperty "array update" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseArrayRepr (Ctx.empty :> BaseIntegerRepr) BaseIntegerRepr) $ \sym bvs -> do
i1 <- WI.intLit sym 1
i2 <- WI.intLit sym 2
let arr = bvs ! Ctx.baseIndex
WI.arrayUpdate sym arr (Ctx.empty :> i1) i2
, testProperty "integer to bitvector" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr (Ctx.empty :> BaseIntegerRepr) $ \sym bvs -> do
let i1 = bvs ! Ctx.baseIndex
WI.integerToBV sym i1 (WI.knownNat @32)
, testProperty "float negate" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr (Ctx.empty :> floatSingleType ) $ \sym flts -> do
let f1 = flts ! Ctx.baseIndex
WI.floatNeg sym f1
, testProperty "float abs" $
withTests 1 $
property $ mkEquivalenceTest parseSExpr (Ctx.empty :> floatSingleType ) $ \sym flts -> do
let f1 = flts ! Ctx.baseIndex
WI.floatAbs sym f1
]
mkEquivalenceTest :: forall m args ret
. ( MonadTest m
, MonadIO m
)
=> (T.Text -> Either String WIN.SExpr)
-> Ctx.Assignment BaseTypeRepr args
-> (forall sym
. WI.IsSymExprBuilder sym
=> sym
-> Ctx.Assignment (WI.SymExpr sym) args
-> IO (WI.SymExpr sym ret))
-> m ()
mkEquivalenceTest parseSExpr argTs getExpr = do
Some r <- liftIO $ newIONonceGenerator
sym <- liftIO $ S.newExprBuilder S.FloatRealRepr NoBuilderData r
liftIO $ S.startCaching sym
bvs <- liftIO $ forFC argTs $ \repr -> do
n <- freshNonce r
let nm = "bv" ++ show (indexValue n)
WI.freshBoundVar sym (WI.safeSymbol nm) repr
e <- liftIO $ getExpr sym (fmapFC (WI.varExpr sym) bvs)
go sym bvs e
where
go :: forall sym t flgs st .
( WI.IsSymExprBuilder sym
, sym ~ S.ExprBuilder t st flgs
, ShowF (WI.SymExpr sym)
)
=> sym
-> Ctx.Assignment (WI.BoundVar sym) args
-> WI.SymExpr sym ret
-> m ()
go sym bvs expr = do
fn1 <- liftIO $ WI.definedFn sym (WI.safeSymbol "fn") bvs expr WI.NeverUnfold
let scfg = WOUT.Config { WOUT.cfgAllowFreeVars = True
, WOUT.cfgAllowFreeSymFns = True
}
res = WOUT.serializeSymFnWithConfig scfg fn1
fnText = WOUT.printSExpr mempty $ WOUT.resSExpr res
fnMap = Map.fromList $ map (\(x,y)->(y,x)) $ OMap.assocs $ WOUT.resSymFnEnv res
exprMap = Map.fromList $
map (\((Some bv),freshName) ->
(freshName, (Some (WI.varExpr sym bv))))
$ OMap.assocs
$ WOUT.resFreeVarEnv res
-- lcfg <- liftIO $ Log.mkLogCfg "rndtrip"
deser <- do
dcfg <- return $ (WIN.defaultConfig sym)
{ WIN.cSymFnLookup = \nm ->
case Map.lookup nm fnMap of
Nothing -> return Nothing
Just (WOUT.SomeExprSymFn fn) -> return $ Just (WIN.SomeSymFn fn)
, WIN.cExprLookup = \nm ->
case Map.lookup nm exprMap of
Nothing -> return Nothing
Just (Some x) -> return $ Just (Some x)
}
case parseSExpr fnText of
Left errMsg -> return $ Left errMsg
Right sexpr -> liftIO $ WIN.deserializeSymFnWithConfig sym dcfg sexpr
case deser of
Left err -> do
debugOut $ "Unexpected deserialization error: " ++ err ++ "!\n S-expression:\n"
debugOut $ (T.unpack fnText) ++ "\n"
failure
Right (WIN.SomeSymFn fn2) -> do
fn1out <- liftIO $ WI.definedFn sym (WI.safeSymbol "fn") bvs expr WI.NeverUnfold
symFnEqualityTest sym fn1out fn2
-- | Create a 'T.TestTree' from a Hedgehog 'Property'.
--
-- Note that @tasty-hedgehog@'s version of 'testProperty' has been deprecated
-- in favor of 'testPropertyNamed', whose second argument is intended to
-- represent the name of a top-level 'Property' value to run in the event that
-- the test fails. See https://github.com/qfpl/tasty-hedgehog/pull/42.
--
-- That being said, @what4-serialize@ currently does not define any of the
-- properties that it tests as top-level values. In the
-- meantime, we avoid incurring deprecation warnings by defining our own
-- version of 'testProperty'. The downside to this workaround is that if a
-- property fails, the error message it will produce will likely suggest
-- running ill-formed Haskell code, so users will have to use context clues to
-- determine how to /actually/ reproduce the error.
testProperty :: TestName -> Property -> TestTree
testProperty name = testPropertyNamed name (String.fromString name)
|
