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