grisette-0.5.0.0: test/Grisette/Backend/CEGISTests.hs
{-# LANGUAGE BinaryLiterals #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Grisette.Backend.CEGISTests (cegisTests) where
import Control.Monad.Except (ExceptT)
import Data.Proxy (Proxy (Proxy))
import qualified Data.SBV as SBV
import Data.String (IsString (fromString))
import GHC.Stack (HasCallStack)
import Grisette
( Apply (apply),
CEGISResult (CEGISSuccess),
EvaluateSym (evaluateSym),
ExtractSymbolics,
Function ((#)),
GrisetteSMTConfig,
ITEOp (symIte),
LogicalOp (symNot, symXor, (.&&), (.||)),
SEq ((.==)),
SOrd ((.<), (.>=)),
SizedBV (sizedBVConcat, sizedBVSelect, sizedBVSext, sizedBVZext),
Solvable (con),
UnionM,
VerificationConditions,
cegis,
cegisExceptVC,
cegisForAllExceptVC,
cegisMultiInputs,
cegisPostCond,
mrgIf,
precise,
solve,
symAssert,
symAssume,
z3,
)
import Grisette.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, SEq a) =>
GrisetteSMTConfig i ->
Bool ->
a ->
(a -> [SymBool]) ->
Assertion
testCegis config shouldSuccess inputs bs = do
cegisExceptVCResult <-
cegisExceptVC config (inputs, "internal" :: SymInteger) return $
\(cexInputs, internal) -> buildFormula internal (bs cexInputs)
case cegisExceptVCResult of
(_, CEGISSuccess m) -> do
shouldSuccess @=? True
verify "cegisExceptVC" m (bs inputs)
_ -> shouldSuccess @=? False
cegisForAllExceptVCResult <-
cegisForAllExceptVC config (inputs, "internal" :: SymInteger) return $
buildFormula "internal" (bs inputs)
case cegisForAllExceptVCResult of
(_, CEGISSuccess m) -> do
shouldSuccess @=? True
verify "cegisForAllExceptVC" m (bs inputs)
_ -> shouldSuccess @=? False
where
verify _ _ [] = return ()
verify funName m (v : vs) = do
y <- solve config (evaluateSym False m $ symNot v)
case y of
Left _ -> verify funName m vs
Right _ ->
assertFailure $
funName
++ ": Failed to verify "
++ show v
++ " with the model "
++ show m
buildFormula internal l = do
symAssume (internal .>= 0)
go l 0
where
go ::
[SymBool] -> SymInteger -> ExceptT VerificationConditions UnionM ()
go [] _ = return ()
go (x : xs) i =
mrgIf
(internal .>= i .&& internal .< (i + 1))
(symAssert x)
(go xs (i + 1))
cegisTests :: Test
cegisTests =
let unboundedConfig = precise SBV.z3
in testGroup
"CEGIS"
[ testGroup
"Regression"
[ testCase "Empty symbolic inputs makes cegis work like solve" $ do
(_, CEGISSuccess m1) <-
cegisMultiInputs
(precise z3)
[1 :: Integer, 2]
(\idx -> cegisPostCond $ fromString $ "a" ++ show idx)
Right m2 <- solve (precise z3) ("a1" .&& "a2")
m1 @=? m2,
testCase "Lowering of TabularFun" $ do
let s1 = "s1" :: SymInteger =~> SymInteger
let s2 = "s2" :: SymInteger =~> SymInteger
(_, CEGISSuccess m1) <-
cegis unboundedConfig ("cond" :: SymBool) $
\cond ->
cegisPostCond $
apply (symIte cond s1 s2) (symIte cond 1 2)
.== 10
.&& apply (symIte cond s1 s2) (symIte 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
(_, CEGISSuccess m1) <-
cegis unboundedConfig ("cond" :: SymBool) $
\cond ->
cegisPostCond $
apply (symIte cond s1 s2) (symIte cond 1 2)
.== 10
.&& apply (symIte cond s1 s2) (symIte 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 () $ const ["a", "b", "c"]
testCegis unboundedConfig False () $ const ["a", symNot "a"],
testCase "And" $ do
testCegis unboundedConfig True () $
const ["a" .&& "b", "b" .&& symNot "c", "a", "b", symNot "c"]
testCegis unboundedConfig False () $
const ["a" .&& "b", "b" .&& symNot "c", "a", "b", "c"]
testCegis unboundedConfig True ("a" :: SymBool) $
\a -> [symNot $ a .&& "b", symNot "b"]
testCegis unboundedConfig False ("a" :: SymBool) $
\a -> [symNot $ a .&& "b", "b"],
testCase "Or" $ do
testCegis unboundedConfig True () $
const ["a" .|| "b", "b" .|| symNot "c", "a", "b", symNot "c"]
testCegis unboundedConfig True () $
const ["a" .|| "b", "b" .|| symNot "c", "a", "b", "c"]
testCegis unboundedConfig True ("a" :: SymBool) $
\a -> [a .|| "b", "b"]
testCegis unboundedConfig False ("a" :: SymBool) $
\a -> [a .|| "b", symNot "b"],
testCase "And / Or should be consistent" $ do
testCegis unboundedConfig True () $
const ["a" .&& "b", "a" .|| "b"]
testCegis unboundedConfig True () $
const [symNot "a" .&& "b", "a" .|| "b"]
testCegis unboundedConfig False () $
const ["a" .&& "b", symNot $ "a" .|| "b"]
testCegis unboundedConfig True () $
const [symNot $ "a" .&& "b", symNot $ "a" .|| "b"],
testCase "Eqv" $ do
testCegis unboundedConfig True () $
const [("a" :: SymBool) .== "b", "a", "b"]
testCegis unboundedConfig True () $
const [("a" :: SymBool) .== "b", symNot "a", symNot "b"]
testCegis unboundedConfig False () $
const [("a" :: SymBool) .== "b", symNot "a", "b"]
testCegis unboundedConfig False () $
const [("a" :: SymBool) .== "b", symNot "a", "b"]
testCegis unboundedConfig True () $
const [("a" :: SymBool) .== "b", symNot "a" `symXor` "b"]
testCegis unboundedConfig False () $
const [("a" :: SymBool) .== "b", "a" `symXor` "b"],
testCase "symIte" $ do
testCegis unboundedConfig True ("c" :: SymBool) $
\c -> [symIte "a" "b" c, "a", "b"]
testCegis unboundedConfig False ("c" :: SymBool) $
\c -> [symIte "a" "b" c, symNot "a"]
testCegis unboundedConfig True ("b" :: SymBool) $
\b -> [symIte "a" b "c", symNot "a", "c"]
testCegis unboundedConfig False ("b" :: SymBool) $
\b -> [symIte "a" b "c", "a"]
testCegis unboundedConfig True () $
const [symIte "a" "b" "c", "a", "b", "c"]
testCegis unboundedConfig True () $
const [symIte "a" "b" "c", "a", "b", symNot "c"]
testCegis unboundedConfig True () $
const [symIte "a" "b" "c", symNot "a", "b", "c"]
testCegis unboundedConfig True () $
const [symIte "a" "b" "c", symNot "a", symNot "b", "c"]
testCegis unboundedConfig False () $
const [symIte "a" "b" "c", "a", symNot "b", "c"]
testCegis unboundedConfig False () $
const [symIte "a" "b" "c", "a", symNot "b", symNot "c"]
testCegis unboundedConfig False () $
const [symIte "a" "b" "c", symNot "a", "b", symNot "c"]
testCegis unboundedConfig False () $
const [symIte "a" "b" "c", symNot "a", symNot "b", symNot "c"]
],
let a = "a" :: SymIntN 5
b = "b" :: SymIntN 5
c = "c" :: SymIntN 5
d = "c" :: SymIntN 10
in testGroup
"Different sized BV"
[ testGroup
"Select"
[ testCase "sizedBVSelect" $ do
testCegis unboundedConfig True () $
const
[ sizedBVSelect (Proxy @2) (Proxy @2) a
.== (con 1 :: SymIntN 2),
a .== con 0b10101
]
testCegis unboundedConfig False () $
const
[ sizedBVSelect (Proxy @2) (Proxy @2) a
.== (con 1 :: SymIntN 2),
a .== con 0b10001
],
testCase "sizedBVSelect when lowered twice" $ do
testCegis unboundedConfig True a $
\ca ->
[ sizedBVSelect
(Proxy @2)
(Proxy @2)
(sizedBVConcat ca b)
.== (con 1 :: SymIntN 2)
]
testCegis unboundedConfig True b $
\cb ->
[ sizedBVSelect
(Proxy @7)
(Proxy @2)
(sizedBVConcat a cb)
.== (con 1 :: SymIntN 2)
]
],
testGroup
"Concat"
[ testCase "sizedBVConcat" $ do
testCegis unboundedConfig True () $
const
[ sizedBVConcat a b .== d,
a .== con 1,
b .== con 1,
d .== con 0b100001
]
testCegis unboundedConfig False () $
const
[ sizedBVConcat a b .== d,
a .== con 1,
b .== con 1,
d .== con 0b100010
],
testCase "sizedBVConcat when lowered twice" $ do
testCegis unboundedConfig True (a, c) $
\(ca, cc) ->
[ sizedBVConcat
cc
( sizedBVSelect
(Proxy @2)
(Proxy @2)
(sizedBVConcat ca b) ::
SymIntN 2
)
.== sizedBVConcat cc (con 1 :: SymIntN 2)
]
testCegis unboundedConfig True (b, c) $
\(cb, cc) ->
[ sizedBVConcat
cc
( sizedBVSelect
(Proxy @7)
(Proxy @2)
(sizedBVConcat a cb) ::
SymIntN 2
)
.== sizedBVConcat cc (con 1 :: SymIntN 2)
]
],
testGroup
"Zext"
[ testCase "sizedBVZext" $ do
testCegis unboundedConfig True () $
const
[ sizedBVZext (Proxy @10) a .== d,
a .== con 1,
d .== (con 1 :: SymIntN 10)
]
testCegis unboundedConfig True () $
const
[ sizedBVZext (Proxy @10) a .== d,
a .== con 0b11111,
d .== (con 0b11111 :: SymIntN 10)
]
testCegis unboundedConfig False () $
const
[ sizedBVZext (Proxy @10) a .== d,
d .== (con 0b111111 :: SymIntN 10)
]
testCegis unboundedConfig False () $
const
[ sizedBVZext (Proxy @10) a .== d,
d .== (con 0b1111111111 :: SymIntN 10)
],
testCase "sizedBVZext when lowered twice" $ do
testCegis unboundedConfig True a $
\ca ->
[ sizedBVZext
(Proxy @10)
( sizedBVSelect
(Proxy @2)
(Proxy @2)
(sizedBVConcat ca b) ::
SymIntN 2
)
.== (con 1 :: SymIntN 10)
]
testCegis unboundedConfig True b $
\cb ->
[ sizedBVZext
(Proxy @10)
( sizedBVSelect
(Proxy @7)
(Proxy @2)
(sizedBVConcat a cb) ::
SymIntN 2
)
.== (con 1 :: SymIntN 10)
]
],
testGroup
"Sext"
[ testCase "sizedBVSext" $ do
testCegis unboundedConfig True () $
const
[ sizedBVSext (Proxy @10) a .== d,
a .== con 1,
d .== (con 1 :: SymIntN 10)
]
testCegis unboundedConfig True () $
const
[ sizedBVSext (Proxy @10) a .== d,
a .== con 0b11111,
d .== (con 0b1111111111 :: SymIntN 10)
]
testCegis unboundedConfig False () $
const
[ sizedBVSext (Proxy @10) a .== d,
d .== (con 0b111111 :: SymIntN 10)
]
testCegis unboundedConfig False () $
const
[ sizedBVSext (Proxy @10) a .== d,
d .== (con 0b11111 :: SymIntN 10)
],
testCase "sizedBVSext when lowered twice" $ do
testCegis unboundedConfig True a $ \ca ->
[ sizedBVSext
(Proxy @10)
( sizedBVSelect
(Proxy @2)
(Proxy @2)
(sizedBVConcat ca b) ::
SymIntN 2
)
.== (con 1 :: SymIntN 10)
]
testCegis unboundedConfig True b $
\cb ->
[ sizedBVSext
(Proxy @10)
( sizedBVSelect
(Proxy @7)
(Proxy @2)
(sizedBVConcat a cb) ::
SymIntN 2
)
.== (con 1 :: SymIntN 10)
]
]
]
]