{-# LANGUAGE BinaryLiterals #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} module Grisette.Backend.SBV.Data.SMT.CEGISTests (cegisTests) where import Control.Monad.Except (ExceptT, runExceptT) import Data.Proxy (Proxy (Proxy)) import qualified Data.SBV as SBV import Data.String (IsString (fromString)) import GHC.Stack (HasCallStack) import Grisette.Backend.SBV (GrisetteSMTConfig, precise, z3) import Grisette.Core.Control.Exception ( VerificationConditions, symAssert, symAssume, ) import Grisette.Core.Control.Monad.UnionM (UnionM) import Grisette.Core.Data.Class.BitVector ( SizedBV (sizedBVConcat, sizedBVSelect, sizedBVSext, sizedBVZext), ) import Grisette.Core.Data.Class.Bool ( ITEOp (ites), LogicalOp (nots, xors, (&&~), (||~)), SEq ((==~)), ) import Grisette.Core.Data.Class.CEGISSolver ( CEGISSolver (cegisMultiInputs), cegis, cegisExceptVC, cegisPostCond, ) import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym)) import Grisette.Core.Data.Class.ExtractSymbolics ( ExtractSymbolics, ) import Grisette.Core.Data.Class.Function (Function ((#))) import Grisette.Core.Data.Class.SOrd (SOrd ((<~), (>=~))) import Grisette.Core.Data.Class.SimpleMergeable (mrgIf) import Grisette.Core.Data.Class.Solvable (Solvable (con, ssym)) import Grisette.Core.Data.Class.Solver (Solver (solve)) import Grisette.IR.SymPrim.Data.SymPrim ( SymBool, SymIntN, SymInteger, type (-~>), type (=~>), ) import Test.Framework (Test, testGroup) import Test.Framework.Providers.HUnit (testCase) import Test.HUnit (Assertion, assertFailure, (@=?)) testCegis :: (HasCallStack, ExtractSymbolics a, EvaluateSym a, Show a) => GrisetteSMTConfig i -> Bool -> a -> [SymBool] -> Assertion testCegis config shouldSuccess a bs = do x <- cegisExceptVC config (a, ssym "internal" :: SymInteger) return (runExceptT $ buildFormula bs) case x of (_, Left _) -> shouldSuccess @=? False (_, Right m) -> do shouldSuccess @=? True verify bs where verify [] = return () verify (v : vs) = do y <- solve config (evaluateSym False m $ nots v) case y of Left _ -> do verify vs Right _ -> assertFailure $ "Failed to verify " ++ show v ++ " with the model " ++ show m where buildFormula :: [SymBool] -> ExceptT VerificationConditions UnionM () buildFormula l = do symAssume ((ssym "internal" :: SymInteger) >=~ 0) go l 0 where go :: [SymBool] -> SymInteger -> ExceptT VerificationConditions UnionM () go [] _ = return () go (x : xs) i = mrgIf (ssym "internal" >=~ i &&~ ssym "internal" <~ (i + 1)) (symAssert x) (go xs (i + 1)) cegisTests :: Test cegisTests = let unboundedConfig = precise SBV.z3 -- {SBV.verbose=True} in testGroup "CEGISTests" [ testGroup "Regression" [ testCase "Empty symbolic inputs makes cegis work like solve" $ do (_, Right m1) <- cegisMultiInputs (precise z3) [1 :: Integer, 2] (\x -> cegisPostCond $ fromString $ "a" ++ show x) Right m2 <- solve (precise z3) (ssym "a1" &&~ ssym "a2") m1 @=? m2, testCase "Lowering of TabularFun" $ do let s1 = "s1" :: SymInteger =~> SymInteger let s2 = "s2" :: SymInteger =~> SymInteger (_, Right m1) <- cegis unboundedConfig (ssym "cond" :: SymBool) $ cegisPostCond $ ites "cond" s1 s2 # ites "cond" 1 2 ==~ 10 &&~ ites "cond" s1 s2 # ites "cond" 3 4 ==~ 100 let s1e = evaluateSym False m1 s1 let s2e = evaluateSym False m1 s2 s1e # 1 @=? 10 s1e # 3 @=? 100 s2e # 2 @=? 10 s2e # 4 @=? 100, testCase "Lowering of GeneralFun" $ do let s1 = "s1" :: SymInteger -~> SymInteger let s2 = "s2" :: SymInteger -~> SymInteger (_, Right m1) <- cegis unboundedConfig (ssym "cond" :: SymBool) $ cegisPostCond $ ites "cond" s1 s2 # ites "cond" 1 2 ==~ 10 &&~ ites "cond" s1 s2 # ites "cond" 3 4 ==~ 100 let s1e = evaluateSym False m1 s1 let s2e = evaluateSym False m1 s2 s1e # 1 @=? 10 s1e # 3 @=? 100 s2e # 2 @=? 10 s2e # 4 @=? 100 ], testGroup "Boolean" [ testCase "Basic" $ do testCegis unboundedConfig True () [ssym "a", ssym "b", ssym "c"] testCegis unboundedConfig False () [ssym "a", nots $ ssym "a"], testCase "And" $ do testCegis unboundedConfig True () [ssym "a" &&~ ssym "b", ssym "b" &&~ nots (ssym "c"), ssym "a", ssym "b", nots (ssym "c")] testCegis unboundedConfig False () [ssym "a" &&~ ssym "b", ssym "b" &&~ nots (ssym "c"), ssym "a", ssym "b", ssym "c"] testCegis unboundedConfig True (ssym "a" :: SymBool) [nots $ ssym "a" &&~ ssym "b", nots $ ssym "b"] testCegis unboundedConfig False (ssym "a" :: SymBool) [nots $ ssym "a" &&~ ssym "b", ssym "b"], testCase "Or" $ do testCegis unboundedConfig True () [ssym "a" ||~ ssym "b", ssym "b" ||~ nots (ssym "c"), ssym "a", ssym "b", nots (ssym "c")] testCegis unboundedConfig True () [ssym "a" ||~ ssym "b", ssym "b" ||~ nots (ssym "c"), ssym "a", ssym "b", ssym "c"] testCegis unboundedConfig True (ssym "a" :: SymBool) [ssym "a" ||~ ssym "b", ssym "b"] testCegis unboundedConfig False (ssym "a" :: SymBool) [ssym "a" ||~ ssym "b", nots $ ssym "b"], testCase "And / Or should be consistent" $ do testCegis unboundedConfig True () [ssym "a" &&~ ssym "b", ssym "a" ||~ ssym "b"] testCegis unboundedConfig True () [nots $ ssym "a" &&~ ssym "b", ssym "a" ||~ ssym "b"] testCegis unboundedConfig False () [ssym "a" &&~ ssym "b", nots $ ssym "a" ||~ ssym "b"] testCegis unboundedConfig True () [nots $ ssym "a" &&~ ssym "b", nots $ ssym "a" ||~ ssym "b"], testCase "Eqv" $ do testCegis unboundedConfig True () [(ssym "a" :: SymBool) ==~ ssym "b", ssym "a", ssym "b"] testCegis unboundedConfig True () [(ssym "a" :: SymBool) ==~ ssym "b", nots $ ssym "a", nots $ ssym "b"] testCegis unboundedConfig False () [(ssym "a" :: SymBool) ==~ ssym "b", nots $ ssym "a", ssym "b"] testCegis unboundedConfig False () [(ssym "a" :: SymBool) ==~ ssym "b", nots $ ssym "a", ssym "b"] testCegis unboundedConfig True () [(ssym "a" :: SymBool) ==~ ssym "b", nots (ssym "a") `xors` ssym "b"] testCegis unboundedConfig False () [(ssym "a" :: SymBool) ==~ ssym "b", ssym "a" `xors` ssym "b"], testCase "ites" $ do testCegis unboundedConfig True (ssym "c" :: SymBool) [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), ssym "a", ssym "b"] testCegis unboundedConfig False (ssym "c" :: SymBool) [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), nots $ ssym "a"] testCegis unboundedConfig True (ssym "b" :: SymBool) [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), nots $ ssym "a", ssym "c"] testCegis unboundedConfig False (ssym "b" :: SymBool) [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), ssym "a"] testCegis unboundedConfig True () [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), ssym "a", ssym "b", ssym "c"] testCegis unboundedConfig True () [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), ssym "a", ssym "b", nots $ ssym "c"] testCegis unboundedConfig True () [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), nots $ ssym "a", ssym "b", ssym "c"] testCegis unboundedConfig True () [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), nots $ ssym "a", nots $ ssym "b", ssym "c"] testCegis unboundedConfig False () [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), ssym "a", nots $ ssym "b", ssym "c"] testCegis unboundedConfig False () [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), ssym "a", nots $ ssym "b", nots $ ssym "c"] testCegis unboundedConfig False () [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), nots $ ssym "a", ssym "b", nots $ ssym "c"] testCegis unboundedConfig False () [ites (ssym "a" :: SymBool) (ssym "b") (ssym "c"), nots $ ssym "a", nots $ ssym "b", nots $ ssym "c"] ], let a = ssym "a" :: SymIntN 5 b = ssym "b" :: SymIntN 5 c = ssym "c" :: SymIntN 5 d = ssym "c" :: SymIntN 10 in testGroup "Different sized BV" [ testGroup "Select" [ testCase "sizedBVSelect" $ do testCegis unboundedConfig True () [sizedBVSelect (Proxy @2) (Proxy @2) a ==~ (con 1 :: SymIntN 2), a ==~ con 0b10101] testCegis unboundedConfig False () [sizedBVSelect (Proxy @2) (Proxy @2) a ==~ (con 1 :: SymIntN 2), a ==~ con 0b10001], testCase "sizedBVSelect when lowered twice" $ do testCegis unboundedConfig True a [sizedBVSelect (Proxy @2) (Proxy @2) (sizedBVConcat a b) ==~ (con 1 :: SymIntN 2)] testCegis unboundedConfig True b [sizedBVSelect (Proxy @7) (Proxy @2) (sizedBVConcat a b) ==~ (con 1 :: SymIntN 2)] ], testGroup "Concat" [ testCase "sizedBVConcat" $ do testCegis unboundedConfig True () [sizedBVConcat a b ==~ d, a ==~ con 1, b ==~ con 1, d ==~ con 0b100001] testCegis unboundedConfig False () [sizedBVConcat a b ==~ d, a ==~ con 1, b ==~ con 1, d ==~ con 0b100010], testCase "sizedBVConcat when lowered twice" $ do testCegis unboundedConfig True (a, c) [sizedBVConcat c (sizedBVSelect (Proxy @2) (Proxy @2) (sizedBVConcat a b) :: SymIntN 2) ==~ sizedBVConcat c (con 1 :: SymIntN 2)] testCegis unboundedConfig True (b, c) [sizedBVConcat c (sizedBVSelect (Proxy @7) (Proxy @2) (sizedBVConcat a b) :: SymIntN 2) ==~ sizedBVConcat c (con 1 :: SymIntN 2)] ], testGroup "Zext" [ testCase "sizedBVZext" $ do testCegis unboundedConfig True () [sizedBVZext (Proxy @10) a ==~ d, a ==~ con 1, d ==~ (con 1 :: SymIntN 10)] testCegis unboundedConfig True () [sizedBVZext (Proxy @10) a ==~ d, a ==~ con 0b11111, d ==~ (con 0b11111 :: SymIntN 10)] testCegis unboundedConfig False () [sizedBVZext (Proxy @10) a ==~ d, d ==~ (con 0b111111 :: SymIntN 10)] testCegis unboundedConfig False () [sizedBVZext (Proxy @10) a ==~ d, d ==~ (con 0b1111111111 :: SymIntN 10)], testCase "sizedBVZext when lowered twice" $ do testCegis unboundedConfig True a [sizedBVZext (Proxy @10) (sizedBVSelect (Proxy @2) (Proxy @2) (sizedBVConcat a b) :: SymIntN 2) ==~ (con 1 :: SymIntN 10)] testCegis unboundedConfig True b [sizedBVZext (Proxy @10) (sizedBVSelect (Proxy @7) (Proxy @2) (sizedBVConcat a b) :: SymIntN 2) ==~ (con 1 :: SymIntN 10)] ], testGroup "Sext" [ testCase "sizedBVSext" $ do testCegis unboundedConfig True () [sizedBVSext (Proxy @10) a ==~ d, a ==~ con 1, d ==~ (con 1 :: SymIntN 10)] testCegis unboundedConfig True () [sizedBVSext (Proxy @10) a ==~ d, a ==~ con 0b11111, d ==~ (con 0b1111111111 :: SymIntN 10)] testCegis unboundedConfig False () [sizedBVSext (Proxy @10) a ==~ d, d ==~ (con 0b111111 :: SymIntN 10)] testCegis unboundedConfig False () [sizedBVSext (Proxy @10) a ==~ d, d ==~ (con 0b11111 :: SymIntN 10)], testCase "sizedBVSext when lowered twice" $ do testCegis unboundedConfig True a [sizedBVSext (Proxy @10) (sizedBVSelect (Proxy @2) (Proxy @2) (sizedBVConcat a b) :: SymIntN 2) ==~ (con 1 :: SymIntN 10)] testCegis unboundedConfig True b [sizedBVSext (Proxy @10) (sizedBVSelect (Proxy @7) (Proxy @2) (sizedBVConcat a b) :: SymIntN 2) ==~ (con 1 :: SymIntN 10)] ] ] ]