1{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE ExistentialQuantification #-}
3{-# LANGUAGE ExplicitForAll #-}
4{-# LANGUAGE FlexibleContexts #-}
5{-# LANGUAGE GADTs #-}
6{-# LANGUAGE LambdaCase #-}
7{-# LANGUAGE OverloadedStrings #-}
8{-# LANGUAGE RankNTypes #-}
9{-# LANGUAGE RecordWildCards #-}
10{-# LANGUAGE ScopedTypeVariables #-}
11{-# LANGUAGE StandaloneDeriving #-}
12{-# LANGUAGE TemplateHaskell #-}
13{-# LANGUAGE TypeApplications #-}
14
15import Test.Tasty
16import Test.Tasty.HUnit
17
18
19import           Control.Exception (bracket, try, finally, SomeException)
20import           Control.Monad (void)
21import qualified Data.BitVector.Sized as BV
22import qualified Data.ByteString as BS
23import qualified Data.Map as Map
24import           Data.Foldable
25
26import qualified Data.Parameterized.Context as Ctx
27import           Data.Parameterized.Nonce
28import           Data.Parameterized.Some
29import           System.IO
30import           LibBF
31
32import What4.BaseTypes
33import What4.Config
34import What4.Expr
35import What4.Interface
36import What4.InterpretedFloatingPoint
37import What4.Protocol.Online
38import What4.Protocol.SMTLib2
39import What4.SatResult
40import What4.Solver.Adapter
41import qualified What4.Solver.CVC4 as CVC4
42import qualified What4.Solver.Z3 as Z3
43import qualified What4.Solver.Yices as Yices
44import What4.Utils.StringLiteral
45import What4.Utils.Versions (ver, SolverBounds(..), emptySolverBounds)
46
47data State t = State
48data SomePred = forall t . SomePred (BoolExpr t)
49deriving instance Show SomePred
50type SimpleExprBuilder t fs = ExprBuilder t State fs
51
52
53debugOutputFiles :: Bool
54debugOutputFiles = False
55--debugOutputFiles = True
56
57maybeClose :: Maybe Handle -> IO ()
58maybeClose Nothing = return ()
59maybeClose (Just h) = hClose h
60
61
62userSymbol' :: String -> SolverSymbol
63userSymbol' s = case userSymbol s of
64  Left e       -> error $ show e
65  Right symbol -> symbol
66
67withSym :: FloatModeRepr fm -> (forall t . SimpleExprBuilder t (Flags fm) -> IO a) -> IO a
68withSym floatMode pred_gen = withIONonceGenerator $ \gen ->
69  pred_gen =<< newExprBuilder floatMode State gen
70
71withYices :: (forall t. SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t Yices.Connection -> IO ()) -> IO ()
72withYices action = withSym FloatRealRepr $ \sym ->
73  do extendConfig Yices.yicesOptions (getConfiguration sym)
74     bracket
75       (do h <- if debugOutputFiles then Just <$> openFile "yices.out" WriteMode else return Nothing
76           s <- startSolverProcess Yices.yicesDefaultFeatures h sym
77           return (h,s))
78       (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))
79       (\(_,s) -> action sym s)
80
81withZ3 :: (forall t . SimpleExprBuilder t (Flags FloatIEEE) -> Session t Z3.Z3 -> IO ()) -> IO ()
82withZ3 action = withIONonceGenerator $ \nonce_gen -> do
83  sym <- newExprBuilder FloatIEEERepr State nonce_gen
84  extendConfig Z3.z3Options (getConfiguration sym)
85  Z3.withZ3 sym "z3" defaultLogData { logCallbackVerbose = (\_ -> putStrLn) } (action sym)
86
87withOnlineZ3
88  :: (forall t . SimpleExprBuilder t (Flags FloatIEEE) -> SolverProcess t (Writer Z3.Z3) -> IO a)
89  -> IO a
90withOnlineZ3 action = withSym FloatIEEERepr $ \sym -> do
91  extendConfig Z3.z3Options (getConfiguration sym)
92  bracket
93    (do h <- if debugOutputFiles then Just <$> openFile "z3.out" WriteMode else return Nothing
94        s <- startSolverProcess (defaultFeatures Z3.Z3) h sym
95        return (h,s))
96    (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))
97    (\(_,s) -> action sym s)
98
99withCVC4
100  :: (forall t . SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t (Writer CVC4.CVC4) -> IO a)
101  -> IO a
102withCVC4 action = withSym FloatRealRepr $ \sym -> do
103  extendConfig CVC4.cvc4Options (getConfiguration sym)
104  bracket
105    (do h <- if debugOutputFiles then Just <$> openFile "cvc4.out" WriteMode else return Nothing
106        s <- startSolverProcess (defaultFeatures CVC4.CVC4) h sym
107        return (h,s))
108    (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))
109    (\(_,s) -> action sym s)
110
111withModel
112  :: Session t Z3.Z3
113  -> BoolExpr t
114  -> ((forall tp . What4.Expr.Expr t tp -> IO (GroundValue tp)) -> IO ())
115  -> IO ()
116withModel s p action = do
117  assume (sessionWriter s) p
118  runCheckSat s $ \case
119    Sat (GroundEvalFn {..}, _) -> action groundEval
120    Unsat _                    -> "unsat" @?= ("sat" :: String)
121    Unknown                    -> "unknown" @?= ("sat" :: String)
122
123-- exists y . (x + 2.0) + (x + 2.0) < y
124iFloatTestPred
125  :: (  forall t
126      . (IsInterpretedFloatExprBuilder (SimpleExprBuilder t fs))
127     => SimpleExprBuilder t fs
128     -> IO SomePred
129     )
130iFloatTestPred sym = do
131  x  <- freshFloatConstant sym (userSymbol' "x") SingleFloatRepr
132  e0 <- iFloatLitSingle sym 2.0
133  e1 <- iFloatAdd @_ @SingleFloat sym RNE x e0
134  e2 <- iFloatAdd @_ @SingleFloat sym RTZ e1 e1
135  y  <- freshFloatBoundVar sym (userSymbol' "y") SingleFloatRepr
136  e3 <- iFloatLt @_ @SingleFloat sym e2 $ varExpr sym y
137  SomePred <$> existsPred sym y e3
138
139floatSinglePrecision :: FloatPrecisionRepr Prec32
140floatSinglePrecision = knownRepr
141
142floatDoublePrecision :: FloatPrecisionRepr Prec64
143floatDoublePrecision = knownRepr
144
145floatSingleType :: BaseTypeRepr (BaseFloatType Prec32)
146floatSingleType = BaseFloatRepr floatSinglePrecision
147
148floatDoubleType :: BaseTypeRepr (BaseFloatType Prec64)
149floatDoubleType = BaseFloatRepr floatDoublePrecision
150
151testInterpretedFloatReal :: TestTree
152testInterpretedFloatReal = testCase "Float interpreted as real" $ do
153  actual   <- withSym FloatRealRepr iFloatTestPred
154  expected <- withSym FloatRealRepr $ \sym -> do
155    x  <- freshConstant sym (userSymbol' "x") knownRepr
156    e0 <- realLit sym 2.0
157    e1 <- realAdd sym x e0
158    e2 <- realAdd sym e1 e1
159    y  <- freshBoundVar sym (userSymbol' "y") knownRepr
160    e3 <- realLt sym e2 $ varExpr sym y
161    SomePred <$> existsPred sym y e3
162  show actual @?= show expected
163
164testFloatUninterpreted :: TestTree
165testFloatUninterpreted = testCase "Float uninterpreted" $ do
166  actual   <- withSym FloatUninterpretedRepr iFloatTestPred
167  expected <- withSym FloatUninterpretedRepr $ \sym -> do
168    let bvtp = BaseBVRepr $ knownNat @32
169    rne_rm           <- intLit sym $ toInteger $ fromEnum RNE
170    rtz_rm           <- intLit sym $ toInteger $ fromEnum RTZ
171    x                <- freshConstant sym (userSymbol' "x") knownRepr
172
173    -- Floating point literal: 2.0
174    e1 <- bvLit sym knownRepr (BV.mkBV knownRepr (bfToBits (float32 NearEven) (bfFromInt 2)))
175
176    add_fn <- freshTotalUninterpFn
177      sym
178      (userSymbol' "uninterpreted_float_add")
179      (Ctx.empty Ctx.:> BaseIntegerRepr Ctx.:> bvtp Ctx.:> bvtp)
180      bvtp
181    e2    <- applySymFn sym add_fn $ Ctx.empty Ctx.:> rne_rm Ctx.:> x Ctx.:> e1
182    e3    <- applySymFn sym add_fn $ Ctx.empty Ctx.:> rtz_rm Ctx.:> e2 Ctx.:> e2
183    y     <- freshBoundVar sym (userSymbol' "y") knownRepr
184    lt_fn <- freshTotalUninterpFn sym
185                                  (userSymbol' "uninterpreted_float_lt")
186                                  (Ctx.empty Ctx.:> bvtp Ctx.:> bvtp)
187                                  BaseBoolRepr
188    e4 <- applySymFn sym lt_fn $ Ctx.empty Ctx.:> e3 Ctx.:> varExpr sym y
189    SomePred <$> existsPred sym y e4
190  show actual @?= show expected
191
192testInterpretedFloatIEEE :: TestTree
193testInterpretedFloatIEEE = testCase "Float interpreted as IEEE float" $ do
194  actual   <- withSym FloatIEEERepr iFloatTestPred
195  expected <- withSym FloatIEEERepr $ \sym -> do
196    x  <- freshConstant sym (userSymbol' "x") knownRepr
197    e0 <- floatLitRational sym floatSinglePrecision 2.0
198    e1 <- floatAdd sym RNE x e0
199    e2 <- floatAdd sym RTZ e1 e1
200    y  <- freshBoundVar sym (userSymbol' "y") knownRepr
201    e3 <- floatLt sym e2 $ varExpr sym y
202    SomePred <$> existsPred sym y e3
203  show actual @?= show expected
204
205-- x <= 0.5 && x >= 1.5
206testFloatUnsat0 :: TestTree
207testFloatUnsat0 = testCase "Unsat float formula" $ withZ3 $ \sym s -> do
208  x  <- freshConstant sym (userSymbol' "x") knownRepr
209  e0 <- floatLitRational sym floatSinglePrecision 0.5
210  e1 <- floatLitRational sym knownRepr 1.5
211  p0 <- floatLe sym x e0
212  p1 <- floatGe sym x e1
213  assume (sessionWriter s) p0
214  assume (sessionWriter s) p1
215  runCheckSat s $ \res -> isUnsat res @? "unsat"
216
217-- x * x < 0
218testFloatUnsat1 :: TestTree
219testFloatUnsat1 = testCase "Unsat float formula" $ withZ3 $ \sym s -> do
220  x  <- freshConstant sym (userSymbol' "x") floatSingleType
221  e0 <- floatMul sym RNE x x
222  p0 <- floatIsNeg sym e0
223  assume (sessionWriter s) p0
224  runCheckSat s $ \res -> isUnsat res @? "unsat"
225
226-- x + y >= x && x != infinity && y > 0 with rounding to +infinity
227testFloatUnsat2 :: TestTree
228testFloatUnsat2 = testCase "Sat float formula" $ withZ3 $ \sym s -> do
229  x  <- freshConstant sym (userSymbol' "x") floatSingleType
230  y  <- freshConstant sym (userSymbol' "y") knownRepr
231  p0 <- notPred sym =<< floatIsInf sym x
232  p1 <- floatIsPos sym y
233  p2 <- notPred sym =<< floatIsZero sym y
234  e0 <- floatAdd sym RTP x y
235  p3 <- floatGe sym x e0
236  p4 <- foldlM (andPred sym) (truePred sym) [p1, p2, p3]
237  assume (sessionWriter s) p4
238  runCheckSat s $ \res -> isSat res @? "sat"
239  assume (sessionWriter s) p0
240  runCheckSat s $ \res -> isUnsat res @? "unsat"
241
242-- x == 2.5 && y == +infinity
243testFloatSat0 :: TestTree
244testFloatSat0 = testCase "Sat float formula" $ withZ3 $ \sym s -> do
245  x <- freshConstant sym (userSymbol' "x") knownRepr
246  e0 <- floatLitRational sym floatSinglePrecision 2.5
247  p0 <- floatEq sym x e0
248  y <- freshConstant sym (userSymbol' "y") knownRepr
249  e1 <- floatPInf sym floatSinglePrecision
250  p1 <- floatEq sym y e1
251  p2 <- andPred sym p0 p1
252  withModel s p2 $ \groundEval -> do
253    (@?=) (bfFromDouble 2.5) =<< groundEval x
254    y_val <- groundEval y
255    assertBool ("expected y = +infinity, actual y = " ++ show y_val) $
256      bfIsInf y_val && bfIsPos y_val
257
258-- x >= 0.5 && x <= 1.5
259testFloatSat1 :: TestTree
260testFloatSat1 = testCase "Sat float formula" $ withZ3 $ \sym s -> do
261  x  <- freshConstant sym (userSymbol' "x") knownRepr
262  e0 <- floatLitRational sym floatSinglePrecision 0.5
263  e1 <- floatLitRational sym knownRepr 1.5
264  p0 <- floatGe sym x e0
265  p1 <- floatLe sym x e1
266  p2 <- andPred sym p0 p1
267  withModel s p2 $ \groundEval -> do
268    x_val <- groundEval x
269    assertBool ("expected x in [0.5, 1.5], actual x = " ++ show x_val) $
270      bfFromDouble 0.5 <= x_val && x_val <= bfFromDouble 1.5
271
272testFloatToBinary :: TestTree
273testFloatToBinary = testCase "float to binary" $ withZ3 $ \sym s -> do
274  x  <- freshConstant sym (userSymbol' "x") knownRepr
275  y  <- freshConstant sym (userSymbol' "y") knownRepr
276  e0 <- floatToBinary sym x
277  e1 <- bvAdd sym e0 y
278  e2 <- floatFromBinary sym floatSinglePrecision e1
279  p0 <- floatNe sym x e2
280  assume (sessionWriter s) p0
281  runCheckSat s $ \res -> isSat res @? "sat"
282  p1 <- notPred sym =<< bvIsNonzero sym y
283  assume (sessionWriter s) p1
284  runCheckSat s $ \res -> isUnsat res @? "unsat"
285
286testFloatFromBinary :: TestTree
287testFloatFromBinary = testCase "float from binary" $ withZ3 $ \sym s -> do
288  x  <- freshConstant sym (userSymbol' "x") knownRepr
289  e0 <- floatFromBinary sym floatSinglePrecision x
290  e1 <- floatToBinary sym e0
291  p0 <- bvNe sym x e1
292  assume (sessionWriter s) p0
293  runCheckSat s $ \res -> isSat res @? "sat"
294  p1 <- notPred sym =<< floatIsNaN sym e0
295  assume (sessionWriter s) p1
296  runCheckSat s $ \res -> isUnsat res @? "unsat"
297
298testFloatBinarySimplification :: TestTree
299testFloatBinarySimplification = testCase "float binary simplification" $
300  withSym FloatIEEERepr $ \sym -> do
301    x  <- freshConstant sym (userSymbol' "x") knownRepr
302    e0 <- floatToBinary sym x
303    e1 <- floatFromBinary sym floatSinglePrecision e0
304    e1 @?= x
305
306testRealFloatBinarySimplification :: TestTree
307testRealFloatBinarySimplification =
308  testCase "real float binary simplification" $
309    withSym FloatRealRepr $ \sym -> do
310      x  <- freshFloatConstant sym (userSymbol' "x") SingleFloatRepr
311      e0 <- iFloatToBinary sym SingleFloatRepr x
312      e1 <- iFloatFromBinary sym SingleFloatRepr e0
313      e1 @?= x
314
315testFloatCastSimplification :: TestTree
316testFloatCastSimplification = testCase "float cast simplification" $
317  withSym FloatIEEERepr $ \sym -> do
318    x  <- freshConstant sym (userSymbol' "x") floatSingleType
319    e0 <- floatCast sym floatDoublePrecision RNE x
320    e1 <- floatCast sym floatSinglePrecision RNE e0
321    e1 @?= x
322
323testFloatCastNoSimplification :: TestTree
324testFloatCastNoSimplification = testCase "float cast no simplification" $
325  withSym FloatIEEERepr $ \sym -> do
326    x  <- freshConstant sym (userSymbol' "x") floatDoubleType
327    e0 <- floatCast sym floatSinglePrecision RNE x
328    e1 <- floatCast sym floatDoublePrecision RNE e0
329    e1 /= x @? ""
330
331testBVSelectShl :: TestTree
332testBVSelectShl = testCase "select shl simplification" $
333  withSym FloatIEEERepr $ \sym -> do
334    x  <- freshConstant sym (userSymbol' "x") knownRepr
335    e0 <- bvLit sym (knownNat @64) (BV.zero knownNat)
336    e1 <- bvConcat sym e0 x
337    e2 <- bvShl sym e1 =<< bvLit sym knownRepr (BV.mkBV knownNat 64)
338    e3 <- bvSelect sym (knownNat @64) (knownNat @64) e2
339    e3 @?= x
340
341testBVSelectLshr :: TestTree
342testBVSelectLshr = testCase "select lshr simplification" $
343  withSym FloatIEEERepr $ \sym -> do
344    x  <- freshConstant sym (userSymbol' "x") knownRepr
345    e0 <- bvConcat sym x =<< bvLit sym (knownNat @64) (BV.zero knownNat)
346    e1 <- bvLshr sym e0 =<< bvLit sym knownRepr (BV.mkBV knownNat 64)
347    e2 <- bvSelect sym (knownNat @0) (knownNat @64) e1
348    e2 @?= x
349
350testBVOrShlZext :: TestTree
351testBVOrShlZext = testCase "bv or-shl-zext -> concat simplification" $
352  withSym FloatIEEERepr $ \sym -> do
353    x  <- freshConstant sym (userSymbol' "x") (BaseBVRepr $ knownNat @8)
354    y  <- freshConstant sym (userSymbol' "y") (BaseBVRepr $ knownNat @8)
355    e0 <- bvZext sym (knownNat @16) x
356    e1 <- bvShl sym e0 =<< bvLit sym knownRepr (BV.mkBV knownNat 8)
357    e2 <- bvZext sym (knownNat @16) y
358    e3 <- bvOrBits sym e1 e2
359    show e3 @?= "bvConcat cx@0:bv cy@1:bv"
360    e4 <- bvOrBits sym e2 e1
361    show e4 @?= show e3
362
363testUninterpretedFunctionScope :: TestTree
364testUninterpretedFunctionScope = testCase "uninterpreted function scope" $
365  withOnlineZ3 $ \sym s -> do
366    fn <- freshTotalUninterpFn sym (userSymbol' "f") knownRepr BaseIntegerRepr
367    x  <- freshConstant sym (userSymbol' "x") BaseIntegerRepr
368    y  <- freshConstant sym (userSymbol' "y") BaseIntegerRepr
369    e0 <- applySymFn sym fn (Ctx.empty Ctx.:> x)
370    e1 <- applySymFn sym fn (Ctx.empty Ctx.:> y)
371    p0 <- intEq sym x y
372    p1 <- notPred sym =<< intEq sym e0 e1
373    p2 <- andPred sym p0 p1
374    res1 <- checkSatisfiable s "test" p2
375    isUnsat res1 @? "unsat"
376    res2 <- checkSatisfiable s "test" p2
377    isUnsat res2 @? "unsat"
378
379testBVIteNesting :: TestTree
380testBVIteNesting = testCase "nested bitvector ites" $ withZ3 $ \sym s -> do
381  bv0 <- bvLit sym (knownNat @32) (BV.zero knownNat)
382  let setSymBit bv idx = do
383        c1 <- freshConstant sym (userSymbol' ("c1_" ++ show idx)) knownRepr
384        c2 <- freshConstant sym (userSymbol' ("c2_" ++ show idx)) knownRepr
385        c3 <- freshConstant sym (userSymbol' ("c3_" ++ show idx)) knownRepr
386        tt1 <- freshConstant sym (userSymbol' ("tt1_" ++ show idx)) knownRepr
387        tt2 <- freshConstant sym (userSymbol' ("tt2_" ++ show idx)) knownRepr
388        tt3 <- freshConstant sym (userSymbol' ("tt3_" ++ show idx)) knownRepr
389        tt4 <- freshConstant sym (userSymbol' ("tt4_" ++ show idx)) knownRepr
390        ite1 <- itePred sym c1 tt1 tt2
391        ite2 <- itePred sym c2 tt3 tt4
392        ite3 <- itePred sym c3 ite1 ite2
393        bvSet sym bv idx ite3
394  bv1 <- foldlM setSymBit bv0 [0..31]
395  p <- testBitBV sym 0 bv1
396  assume (sessionWriter s) p
397  runCheckSat s $ \res -> isSat res @? "sat"
398
399testRotate1 :: TestTree
400testRotate1 = testCase "rotate test1" $ withOnlineZ3 $ \sym s -> do
401  bv <- freshConstant sym (userSymbol' "bv") (BaseBVRepr (knownNat @32))
402
403  bv1 <- bvRol sym bv =<< bvLit sym knownNat (BV.mkBV knownNat 8)
404  bv2 <- bvRol sym bv1 =<< bvLit sym knownNat (BV.mkBV knownNat 16)
405  bv3 <- bvRol sym bv2 =<< bvLit sym knownNat (BV.mkBV knownNat 8)
406  bv4 <- bvRor sym bv2 =<< bvLit sym knownNat (BV.mkBV knownNat 24)
407  bv5 <- bvRor sym bv2 =<< bvLit sym knownNat (BV.mkBV knownNat 28)
408
409  res <- checkSatisfiable s "test" =<< notPred sym =<< bvEq sym bv bv3
410  isUnsat res @? "unsat1"
411
412  res1 <- checkSatisfiable s "test" =<< notPred sym =<< bvEq sym bv bv4
413  isUnsat res1 @? "unsat2"
414
415  res2 <- checkSatisfiable s "test" =<< notPred sym =<< bvEq sym bv bv5
416  isSat res2 @? "sat"
417
418testRotate2 :: TestTree
419testRotate2 = testCase "rotate test2" $ withOnlineZ3 $ \sym s -> do
420  bv  <- freshConstant sym (userSymbol' "bv") (BaseBVRepr (knownNat @32))
421  amt <- freshConstant sym (userSymbol' "amt") (BaseBVRepr (knownNat @32))
422
423  bv1 <- bvRol sym bv amt
424  bv2 <- bvRor sym bv1 amt
425  bv3 <- bvRol sym bv =<< bvLit sym knownNat (BV.mkBV knownNat 20)
426
427  bv == bv2 @? "syntactic equality"
428
429  res1 <- checkSatisfiable s "test" =<< notPred sym =<< bvEq sym bv bv2
430  isUnsat res1 @? "unsat"
431
432  res2 <- checkSatisfiable s "test" =<< notPred sym =<< bvEq sym bv bv3
433  isSat res2 @? "sat"
434
435testRotate3 :: TestTree
436testRotate3 = testCase "rotate test3" $ withOnlineZ3 $ \sym s -> do
437  bv  <- freshConstant sym (userSymbol' "bv") (BaseBVRepr (knownNat @7))
438  amt <- freshConstant sym (userSymbol' "amt") (BaseBVRepr (knownNat @7))
439
440  bv1 <- bvRol sym bv amt
441  bv2 <- bvRor sym bv1 amt
442  bv3 <- bvRol sym bv =<< bvLit sym knownNat (BV.mkBV knownNat 3)
443
444  -- Note, because 7 is not a power of two, this simplification doesn't quite
445  -- work out... it would probably be significant work to make it do so.
446  -- bv == bv2 @? "syntactic equality"
447
448  res1 <- checkSatisfiable s "test" =<< notPred sym =<< bvEq sym bv bv2
449  isUnsat res1 @? "unsat"
450
451  res2 <- checkSatisfiable s "test" =<< notPred sym =<< bvEq sym bv bv3
452  isSat res2 @? "sat"
453
454testSymbolPrimeCharZ3 :: TestTree
455testSymbolPrimeCharZ3 = testCase "z3 symbol prime (') char" $
456  withZ3 $ \sym s -> do
457    x <- freshConstant sym (userSymbol' "x'") knownRepr
458    y <- freshConstant sym (userSymbol' "y'") knownRepr
459    p <- intLt sym x y
460    assume (sessionWriter s) p
461    runCheckSat s $ \res -> isSat res @? "sat"
462
463expectFailure :: IO a -> IO ()
464expectFailure f = try @SomeException f >>= \case
465  Left _ -> return ()
466  Right _ -> assertFailure "expectFailure"
467
468testBoundVarAsFree :: TestTree
469testBoundVarAsFree = testCase "boundvarasfree" $ withOnlineZ3 $ \sym s -> do
470  x <- freshBoundVar sym (userSymbol' "x") BaseBoolRepr
471  y <- freshBoundVar sym (userSymbol' "y") BaseBoolRepr
472  pz <- freshConstant sym (userSymbol' "pz") BaseBoolRepr
473
474  let px = varExpr sym x
475  let py = varExpr sym y
476
477  expectFailure $ checkSatisfiable s "test" px
478  expectFailure $ checkSatisfiable s "test" py
479  checkSatisfiable s "test" pz >>= \res -> isSat res @? "sat"
480
481  inNewFrameWithVars s [Some x] $ do
482    checkSatisfiable s "test" px >>= \res -> isSat res @? "sat"
483    expectFailure $ checkSatisfiable s "test" py
484
485  -- Outside the scope of inNewFrameWithVars we can no longer
486  -- use the bound variable as free
487  expectFailure $ checkSatisfiable s "test" px
488  expectFailure $ checkSatisfiable s "test" py
489
490
491roundingTest ::
492  OnlineSolver solver =>
493  SimpleExprBuilder t fs ->
494  SolverProcess t solver ->
495  IO ()
496roundingTest sym solver =
497  do r <- freshConstant sym (userSymbol' "r") BaseRealRepr
498
499     let runErrTest nm op errOp =
500           do diff <- realAbs sym =<< realSub sym r =<< integerToReal sym =<< op sym r
501              p'   <- notPred sym =<< errOp diff
502              res  <- checkSatisfiable solver nm p'
503              isUnsat res @? nm
504
505     runErrTest "floor"   realFloor (\diff -> realLt sym diff =<< realLit sym 1)
506     runErrTest "ceiling" realCeil  (\diff -> realLt sym diff =<< realLit sym 1)
507     runErrTest "trunc"   realTrunc (\diff -> realLt sym diff =<< realLit sym 1)
508     runErrTest "rna"     realRound (\diff -> realLe sym diff =<< realLit sym 0.5)
509     runErrTest "rne"     realRoundEven (\diff -> realLe sym diff =<< realLit sym 0.5)
510
511     -- floor test
512     do ri <- integerToReal sym =<< realFloor sym r
513        p  <- realLe sym ri r
514
515        res <- checkSatisfiable solver "floorTest" =<< notPred sym p
516        isUnsat res @? "floorTest"
517
518     -- ceiling test
519     do ri <- integerToReal sym =<< realCeil sym r
520        p  <- realLe sym r ri
521
522        res <- checkSatisfiable solver "ceilingTest" =<< notPred sym p
523        isUnsat res @? "ceilingTest"
524
525     -- truncate test
526     do ri <- integerToReal sym =<< realTrunc sym r
527        rabs  <- realAbs sym r
528        riabs <- realAbs sym ri
529        p  <- realLe sym riabs rabs
530
531        res <- checkSatisfiable solver "truncateTest" =<< notPred sym p
532        isUnsat res @? "truncateTest"
533
534     -- round away test
535     do ri <- integerToReal sym =<< realRound sym r
536        diff <- realAbs sym =<< realSub sym r ri
537        ptie <- realEq sym diff =<< realLit sym 0.5
538        rabs <- realAbs sym r
539        iabs <- realAbs sym ri
540        plarge <- realGt sym iabs rabs
541
542        res <- checkSatisfiable solver "rnaTest" =<<
543                  andPred sym ptie =<< notPred sym plarge
544        isUnsat res @? "rnaTest"
545
546     -- round-to-even test
547     do i <- realRoundEven sym r
548        ri <- integerToReal sym i
549        diff <- realAbs sym =<< realSub sym r ri
550        ptie <- realEq sym diff =<< realLit sym 0.5
551        ieven <- intDivisible sym i 2
552
553        res <- checkSatisfiable solver "rneTest" =<<
554                 andPred sym ptie =<< notPred sym ieven
555        isUnsat res @? "rneTest"
556
557
558zeroTupleTest ::
559  OnlineSolver solver =>
560  SimpleExprBuilder t fs ->
561  SolverProcess t solver ->
562  IO ()
563zeroTupleTest sym solver =
564    do u <- freshConstant sym (userSymbol' "u") (BaseStructRepr Ctx.Empty)
565       s <- mkStruct sym Ctx.Empty
566
567       f <- freshTotalUninterpFn sym (userSymbol' "f")
568             (Ctx.Empty Ctx.:> BaseStructRepr Ctx.Empty)
569             BaseBoolRepr
570
571       fu <- applySymFn sym f (Ctx.Empty Ctx.:> u)
572       fs <- applySymFn sym f (Ctx.Empty Ctx.:> s)
573
574       p <- eqPred sym fu fs
575
576       res1 <- checkSatisfiable solver "test" p
577       isSat res1 @? "sat"
578
579       res2 <- checkSatisfiable solver "test" =<< notPred sym p
580       isUnsat res2 @? "unsat"
581
582oneTupleTest ::
583  OnlineSolver solver =>
584  SimpleExprBuilder t fs ->
585  SolverProcess t solver ->
586  IO ()
587oneTupleTest sym solver =
588    do u <- freshConstant sym (userSymbol' "u") (BaseStructRepr (Ctx.Empty Ctx.:> BaseBoolRepr))
589       s <- mkStruct sym (Ctx.Empty Ctx.:> backendPred sym False)
590
591       f <- freshTotalUninterpFn sym (userSymbol' "f")
592             (Ctx.Empty Ctx.:> BaseStructRepr (Ctx.Empty Ctx.:> BaseBoolRepr))
593             BaseBoolRepr
594
595       fu <- applySymFn sym f (Ctx.Empty Ctx.:> u)
596       fs <- applySymFn sym f (Ctx.Empty Ctx.:> s)
597
598       p <- eqPred sym fu fs
599
600       res1 <- checkSatisfiable solver "test" p
601       isSat res1 @? "sat"
602
603       res2 <- checkSatisfiable solver "test" =<< notPred sym p
604       isSat res2 @? "neg sat"
605
606
607pairTest ::
608  OnlineSolver solver =>
609  SimpleExprBuilder t fs ->
610  SolverProcess t solver ->
611  IO ()
612pairTest sym solver =
613    do u <- freshConstant sym (userSymbol' "u") (BaseStructRepr (Ctx.Empty Ctx.:> BaseBoolRepr Ctx.:> BaseRealRepr))
614       r <- realLit sym 42.0
615       s <- mkStruct sym (Ctx.Empty Ctx.:> backendPred sym True Ctx.:> r )
616
617       p <- structEq sym u s
618
619       res1 <- checkSatisfiable solver "test" p
620       isSat res1 @? "sat"
621
622       res2 <- checkSatisfiable solver "test" =<< notPred sym p
623       isSat res2 @? "neg sat"
624
625stringTest1 ::
626  OnlineSolver solver =>
627  SimpleExprBuilder t fs ->
628  SolverProcess t solver ->
629  IO ()
630stringTest1 sym solver =
631  do let bsx = "asdf\nasdf"
632     let bsz = "qwe\x1crty"
633     let bsw = "QQ\"QQ"
634
635     x <- stringLit sym (Char8Literal bsx)
636     y <- freshConstant sym (userSymbol' "str") (BaseStringRepr Char8Repr)
637     z <- stringLit sym (Char8Literal bsz)
638     w <- stringLit sym (Char8Literal bsw)
639
640     s <- stringConcat sym x =<< stringConcat sym y z
641     s' <- stringConcat sym s w
642
643     l <- stringLength sym s'
644
645     n <- intLit sym 25
646     p <- intEq sym n l
647
648     checkSatisfiableWithModel solver "test" p $ \case
649       Sat fn ->
650         do Char8Literal slit <- groundEval fn s'
651            llit <- groundEval fn n
652
653            (fromIntegral (BS.length slit) == llit) @? "model string length"
654            BS.isPrefixOf bsx slit @? "prefix check"
655            BS.isSuffixOf (bsz <> bsw) slit @? "suffix check"
656
657       _ -> fail "expected satisfiable model"
658
659     p2 <- intEq sym l =<< intLit sym 20
660     checkSatisfiableWithModel solver "test" p2 $ \case
661       Unsat () -> return ()
662       _ -> fail "expected unsatifiable model"
663
664
665stringTest2 ::
666  OnlineSolver solver =>
667  SimpleExprBuilder t fs ->
668  SolverProcess t solver ->
669  IO ()
670stringTest2 sym solver =
671  do let bsx = "asdf\nasdf"
672     let bsz = "qwe\x1crty"
673     let bsw = "QQ\"QQ"
674
675     q <- freshConstant sym (userSymbol' "q") BaseBoolRepr
676
677     x <- stringLit sym (Char8Literal bsx)
678     z <- stringLit sym (Char8Literal bsz)
679     w <- stringLit sym (Char8Literal bsw)
680
681     a <- freshConstant sym (userSymbol' "stra") (BaseStringRepr Char8Repr)
682     b <- freshConstant sym (userSymbol' "strb") (BaseStringRepr Char8Repr)
683
684     ax <- stringConcat sym x a
685
686     zw <- stringIte sym q z w
687     bzw <- stringConcat sym b zw
688
689     l <- stringLength sym zw
690     n <- intLit sym 7
691
692     p1 <- stringEq sym ax bzw
693     p2 <- intLt sym l n
694     p  <- andPred sym p1 p2
695
696     checkSatisfiableWithModel solver "test" p $ \case
697       Sat fn ->
698         do axlit <- groundEval fn ax
699            bzwlit <- groundEval fn bzw
700            qlit <- groundEval fn q
701
702            qlit == False @? "correct ite"
703            axlit == bzwlit @? "equal strings"
704
705       _ -> fail "expected satisfable model"
706
707stringTest3 ::
708  OnlineSolver solver =>
709  SimpleExprBuilder t fs ->
710  SolverProcess t solver ->
711  IO ()
712stringTest3 sym solver =
713  do let bsz = "qwe\x1crtyQQ\"QQ"
714     z <- stringLit sym (Char8Literal bsz)
715
716     a <- freshConstant sym (userSymbol' "stra") (BaseStringRepr Char8Repr)
717     b <- freshConstant sym (userSymbol' "strb") (BaseStringRepr Char8Repr)
718     c <- freshConstant sym (userSymbol' "strc") (BaseStringRepr Char8Repr)
719
720     pfx <- stringIsPrefixOf sym a z
721     sfx <- stringIsSuffixOf sym b z
722
723     cnt1 <- stringContains sym z c
724     cnt2 <- notPred sym =<< stringContains sym c =<< stringLit sym (Char8Literal "Q")
725     cnt3 <- notPred sym =<< stringContains sym c =<< stringLit sym (Char8Literal "q")
726     cnt  <- andPred sym cnt1 =<< andPred sym cnt2 cnt3
727
728     lena <- stringLength sym a
729     lenb <- stringLength sym b
730     lenc <- stringLength sym c
731
732     n <- intLit sym 9
733
734     rnga <- intEq sym lena n
735     rngb <- intEq sym lenb n
736     rngc <- intEq sym lenc =<< intLit sym 6
737     rng  <- andPred sym rnga =<< andPred sym rngb rngc
738
739     p <- andPred sym pfx =<<
740          andPred sym sfx =<<
741          andPred sym cnt rng
742
743     checkSatisfiableWithModel solver "test" p $ \case
744       Sat fn ->
745         do alit <- fromChar8Lit <$> groundEval fn a
746            blit <- fromChar8Lit <$> groundEval fn b
747            clit <- fromChar8Lit <$> groundEval fn c
748
749            alit == (BS.take 9 bsz) @? "correct prefix"
750            blit == (BS.drop (BS.length bsz - 9) bsz) @? "correct suffix"
751            clit == (BS.take 6 (BS.drop 1 bsz)) @? "correct middle"
752
753       _ -> fail "expected satisfable model"
754
755
756stringTest4 ::
757  OnlineSolver solver =>
758  SimpleExprBuilder t fs ->
759  SolverProcess t solver ->
760  IO ()
761stringTest4 sym solver =
762  do let bsx = "str"
763     x <- stringLit sym (Char8Literal bsx)
764     a <- freshConstant sym (userSymbol' "stra") (BaseStringRepr Char8Repr)
765     i <- stringIndexOf sym a x =<< intLit sym 5
766
767     zero <- intLit sym 0
768     p <- intLe sym zero i
769
770     checkSatisfiableWithModel solver "test" p $ \case
771       Sat fn ->
772          do alit <- fromChar8Lit <$> groundEval fn a
773             ilit <- groundEval fn i
774
775             BS.isPrefixOf bsx (BS.drop (fromIntegral ilit) alit) @? "correct index"
776             ilit >= 5 @? "index large enough"
777
778       _ -> fail "expected satisfable model"
779
780     np <- notPred sym p
781     lena <- stringLength sym a
782     fv <- intLit sym 10
783     plen <- intLe sym fv lena
784     q <- andPred sym np plen
785
786     checkSatisfiableWithModel solver "test" q $ \case
787       Sat fn ->
788          do alit <- fromChar8Lit <$> groundEval fn a
789             ilit <- groundEval fn i
790
791             not (BS.isInfixOf bsx (BS.drop 5 alit)) @? "substring not found"
792             ilit == (-1) @? "expected neg one"
793
794       _ -> fail "expected satisfable model"
795
796stringTest5 ::
797  OnlineSolver solver =>
798  SimpleExprBuilder t fs ->
799  SolverProcess t solver ->
800  IO ()
801stringTest5 sym solver =
802  do a <- freshConstant sym (userSymbol' "a") (BaseStringRepr Char8Repr)
803     off <- freshConstant sym (userSymbol' "off") BaseIntegerRepr
804     len <- freshConstant sym (userSymbol' "len") BaseIntegerRepr
805
806     n5 <- intLit sym 5
807     n20 <- intLit sym 20
808
809     let qlit = "qwerty"
810
811     sub <- stringSubstring sym a off len
812     p1 <- stringEq sym sub =<< stringLit sym (Char8Literal qlit)
813     p2 <- intLe sym n5 off
814     p3 <- intLe sym n20 =<< stringLength sym a
815
816     p <- andPred sym p1 =<< andPred sym p2 p3
817
818     checkSatisfiableWithModel solver "test" p $ \case
819       Sat fn ->
820         do alit <- fromChar8Lit <$> groundEval fn a
821            offlit <- groundEval fn off
822            lenlit <- groundEval fn len
823
824            let q = BS.take (fromIntegral lenlit) (BS.drop (fromIntegral offlit) alit)
825
826            q == qlit @? "correct substring"
827
828       _ -> fail "expected satisfable model"
829
830
831forallTest ::
832  OnlineSolver solver =>
833  SimpleExprBuilder t fs ->
834  SolverProcess t solver ->
835  IO ()
836forallTest sym solver =
837    do x <- freshConstant sym (userSymbol' "x") BaseBoolRepr
838       y <- freshBoundVar sym (userSymbol' "y") BaseBoolRepr
839       p <- forallPred sym y =<< orPred sym x (varExpr sym y)
840       np <- notPred sym p
841
842       checkSatisfiableWithModel solver "test" p $ \case
843         Sat fn ->
844           do b <- groundEval fn x
845              (b == True) @? "true result"
846
847         _ -> fail "expected satisfible model"
848
849       checkSatisfiableWithModel solver "test" np $ \case
850         Sat fn ->
851           do b <- groundEval fn x
852              (b == False) @? "false result"
853
854         _ -> fail "expected satisfible model"
855
856binderTupleTest1 ::
857  OnlineSolver solver =>
858  SimpleExprBuilder t fs ->
859  SolverProcess t solver ->
860  IO ()
861binderTupleTest1 sym solver =
862 do var <- freshBoundVar sym (safeSymbol "v")
863               (BaseStructRepr (Ctx.Empty Ctx.:> BaseBoolRepr))
864    p0 <- existsPred sym var (truePred sym)
865    res <- checkSatisfiable solver "test" p0
866    isSat res  @? "sat"
867
868binderTupleTest2 ::
869  OnlineSolver solver =>
870  SimpleExprBuilder t fs ->
871  SolverProcess t solver ->
872  IO ()
873binderTupleTest2 sym solver =
874  do x <- freshBoundVar sym (userSymbol' "x")
875              (BaseStructRepr (Ctx.Empty Ctx.:> BaseIntegerRepr Ctx.:> BaseBoolRepr))
876     p <- forallPred sym x =<< structEq sym (varExpr sym x) (varExpr sym x)
877     np <- notPred sym p
878     checkSatisfiableWithModel solver "test" np $ \case
879       Unsat _ -> return ()
880       _ -> fail "expected UNSAT"
881
882-- | These tests simply ensure that no exceptions are raised.
883testSolverInfo :: TestTree
884testSolverInfo = testGroup "solver info queries" $
885  [ testCase "test get solver version" $ withOnlineZ3 $ \_ proc -> do
886      let conn = solverConn proc
887      getVersion conn
888      _ <- versionResult conn (solverResponse proc)
889      pure ()
890  , testCase "test get solver name" $ withOnlineZ3 $ \_ proc -> do
891      let conn = solverConn proc
892      getName conn
893      nm <- nameResult conn (solverResponse proc)
894      nm @?= "Z3"
895  ]
896
897testSolverVersion :: TestTree
898testSolverVersion = testCase "test solver version bounds" $
899  withOnlineZ3 $ \_ proc -> do
900    let bnd = emptySolverBounds{ lower = Just $(ver "0") }
901    checkSolverVersion' (Map.singleton "Z3" bnd) proc >> return ()
902
903testBVDomainArithScale :: TestTree
904testBVDomainArithScale = testCase "bv domain arith scale" $
905  withSym FloatIEEERepr $ \sym -> do
906    x  <- freshConstant sym (userSymbol' "x") (BaseBVRepr $ knownNat @8)
907    e0 <- bvZext sym (knownNat @16) x
908    e1 <- bvNeg sym e0
909    e2 <- bvSub sym e1 =<< bvLit sym knownRepr (BV.mkBV knownNat 1)
910    e3 <- bvUgt sym e2 =<< bvLit sym knownRepr (BV.mkBV knownNat 256)
911    e3 @?= truePred sym
912
913testBVSwap :: TestTree
914testBVSwap = testCase "test bvSwap" $
915  withSym FloatIEEERepr $ \sym -> do
916    e0 <- bvSwap sym (knownNat @2) =<< bvLit sym knownRepr (BV.mkBV knownNat 1)
917    e1 <- bvLit sym knownRepr (BV.mkBV knownNat 256)
918    e0 @?= e1
919
920testBVBitreverse :: TestTree
921testBVBitreverse = testCase "test bvBitreverse" $
922  withSym FloatIEEERepr $ \sym -> do
923    e0 <- bvBitreverse sym =<< bvLit sym (knownNat @8) (BV.mkBV knownNat 1)
924    e1 <- bvLit sym knownRepr (BV.mkBV knownNat 128)
925    e0 @?= e1
926
927main :: IO ()
928main = defaultMain $ testGroup "Tests"
929  [ testInterpretedFloatReal
930  , testFloatUninterpreted
931  , testInterpretedFloatIEEE
932  , testFloatUnsat0
933  , testFloatUnsat1
934  , testFloatUnsat2
935  , testFloatSat0
936  , testFloatSat1
937  , testFloatToBinary
938  , testFloatFromBinary
939  , testFloatBinarySimplification
940  , testRealFloatBinarySimplification
941  , testFloatCastSimplification
942  , testFloatCastNoSimplification
943  , testBVSelectShl
944  , testBVSelectLshr
945  , testBVOrShlZext
946  , testUninterpretedFunctionScope
947  , testBVIteNesting
948  , testRotate1
949  , testRotate2
950  , testRotate3
951  , testSymbolPrimeCharZ3
952  , testBoundVarAsFree
953  , testSolverInfo
954  , testSolverVersion
955  , testBVDomainArithScale
956  , testBVSwap
957  , testBVBitreverse
958
959  , testCase "Yices 0-tuple" $ withYices zeroTupleTest
960  , testCase "Yices 1-tuple" $ withYices oneTupleTest
961  , testCase "Yices pair"    $ withYices pairTest
962
963  , testCase "Z3 0-tuple" $ withOnlineZ3 zeroTupleTest
964  , testCase "Z3 1-tuple" $ withOnlineZ3 oneTupleTest
965  , testCase "Z3 pair"    $ withOnlineZ3 pairTest
966
967  -- TODO, enable this test when we figure out why it
968  -- doesnt work...
969  --  , testCase "CVC4 0-tuple" $ withCVC4 zeroTupleTest
970  , testCase "CVC4 1-tuple" $ withCVC4 oneTupleTest
971  , testCase "CVC4 pair"    $ withCVC4 pairTest
972
973  , testCase "Z3 forall binder" $ withOnlineZ3 forallTest
974  , testCase "CVC4 forall binder" $ withCVC4 forallTest
975
976  , testCase "Z3 string1" $ withOnlineZ3 stringTest1
977  , testCase "Z3 string2" $ withOnlineZ3 stringTest2
978  , testCase "Z3 string3" $ withOnlineZ3 stringTest3
979  , testCase "Z3 string4" $ withOnlineZ3 stringTest4
980  , testCase "Z3 string5" $ withOnlineZ3 stringTest5
981
982  , testCase "CVC4 string1" $ withCVC4 stringTest1
983  , testCase "CVC4 string2" $ withCVC4 stringTest2
984
985  -- TODO, reenable this test, or a similar one, once the following is fixed
986  -- https://github.com/GaloisInc/what4/issues/56
987  -- , testCase "CVC4 string3" $ withCVC4 stringTest3
988  , testCase "CVC4 string4" $ withCVC4 stringTest4
989  , testCase "CVC4 string5" $ withCVC4 stringTest5
990
991  , testCase "Z3 binder tuple1" $ withOnlineZ3 binderTupleTest1
992  , testCase "Z3 binder tuple2" $ withOnlineZ3 binderTupleTest2
993
994  , testCase "CVC4 binder tuple1" $ withCVC4 binderTupleTest1
995  , testCase "CVC4 binder tuple2" $ withCVC4 binderTupleTest2
996
997  , testCase "Z3 rounding" $ withOnlineZ3 roundingTest
998  , testCase "Yices rounding" $ withYices roundingTest
999  , testCase "CVC4 rounding" $ withCVC4 roundingTest
1000  ]
1001