sbv-14.8: SBVTestSuite/TestSuite/Basics/String.hs
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.Basics.String
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test the string functions.
-----------------------------------------------------------------------------
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.Basics.String(tests) where
import Data.SBV.Control
import Utils.SBVTestFramework
import Prelude hiding ((!!), (++))
import qualified Prelude as P ((++))
import Data.SBV.List ((!!), (++))
import qualified Data.SBV.List as S
import qualified Data.SBV.Char as SC
import qualified Data.SBV.RegExp as R
import Control.Monad (forM, forM_, replicateM, unless, void)
import Control.Exception (ErrorCall, displayException, evaluate, try)
import Data.List (isInfixOf, nub, sort)
import Test.Tasty.HUnit (assertBool, assertEqual)
import qualified Data.Map.Strict as M
import qualified Data.Char as C
-- Test suite
tests :: TestTree
tests =
testGroup "Basics.String" [
goldenCapturedIO "strConcat" $ \rf -> checkWith z3{redirectVerbose=Just rf} strConcatSat Sat
, goldenCapturedIO "strConcatBad" $ \rf -> checkWith z3{redirectVerbose=Just rf} strConcatUnsat Unsat
, goldenCapturedIO "strIndexOf" $ \rf -> checkWith z3{redirectVerbose=Just rf} strIndexOfSat Sat
, goldenCapturedIO "strIndexOfBad" $ \rf -> checkWith z3{redirectVerbose=Just rf} strIndexOfUnsat Unsat
, goldenCapturedIO "strExamples1" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples1 Sat
, goldenCapturedIO "strExamples2" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples2 Unsat
, goldenCapturedIO "strExamples3" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples3 Sat
, goldenCapturedIO "strExamples4" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples4 Sat
, goldenCapturedIO "strExamples5" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples5 Sat
, goldenCapturedIO "strExamples6" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples6 Unsat
, goldenCapturedIO "strExamples7" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples7 Sat
, goldenCapturedIO "strExamples8" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples8 Unsat
, goldenCapturedIO "strExamples9" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples9 Sat
, goldenCapturedIO "strExamples10" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples10 Unsat
, goldenCapturedIO "strExamples11" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples11 Unsat
, goldenCapturedIO "strExamples12" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples12 Unsat
, goldenCapturedIO "strExamples13" $ \rf -> checkWith z3{redirectVerbose=Just rf} strExamples13 Unsat
, testCase "strExamples14" $ assert strExamples14
, testGroup "literal regex semantics"
[testCase (show sample P.++ " against " P.++ show regex)
(assertEqual "Literal regex membership" (Just expected) (unliteral (literal sample `R.match` regex)))
| (sample, regex, expected) <- regexLiteralCases]
, testCase "regex literal and solver agreement" regexLiteralAgreement
, testCase "invalid regex repetition bounds" regexInvalidBounds
]
-- | Regressions for continuation handling: universal matching must not
-- discard a suffix, and Boolean operations must inspect the same prefix.
-- Include nullable repetition, empty inputs, Unicode, and embedded NULs.
regexLiteralCases :: [(String, R.RegExp, Bool)]
regexLiteralCases =
[ ("", R.Conc [], True)
, ("a", R.Conc [], False)
, ("a", R.Conc [R.Conc [], "a", R.Conc []], True)
, ("", R.Loop 0 0 "a", True)
, ("a", R.Loop 0 0 "a", False)
, ("", R.Power 0 "a", True)
, ("aa", R.Loop 2 2 "a", True)
, ("a", R.Conc [R.All, "b"], False)
, ("ab", R.Conc [R.All, "b"], True)
, ("b", R.Conc [R.All, "b"], True)
, ("", R.Conc [R.All, "b"], False)
, ("", R.All, True)
, ("a", R.Conc [R.Comp "a", "b"], False)
, ("b", R.Conc [R.Comp "a", "b"], True)
, ("ab", R.Conc [R.Comp "a", "b"], False)
, ("aab", R.Conc [R.Comp "a", "b"], True)
, ("ab", R.Conc [R.Diff "ab" "a", R.Opt "b"], True)
, ("ab", R.Conc [R.Diff "a" "ab", R.Opt "b"], True)
, ("ab", R.Conc [R.Inter "a" "ab", R.All], False)
, ("ab", R.Conc [R.Inter "a" (R.Opt "a"), "b"], True)
, ("a", R.Conc [R.Diff R.All "", "a"], False)
, ("ba", R.Conc [R.Diff R.All "", "a"], True)
, ("", R.KStar (R.Opt "a"), True)
, ("aaa", R.KStar (R.Inter (R.Opt "a") (R.Comp "b")), True)
, ("b", R.KStar (R.Inter (R.Opt "a") (R.Comp "b")), False)
, ("a", R.KStar (R.Conc [R.All, "b"]), False)
, ("b", R.Conc [R.Loop 0 2 (R.Opt "a"), "b"], True)
, ("aab", R.Conc [R.Power 2 (R.Diff "a" "b"), "b"], True)
, ("a\0", R.Conc [R.Comp "b", "\0"], True)
, ("\0a", R.Conc [R.All, "\0"], False)
, ("\955b", R.Conc [R.Inter R.All (R.Comp "a"), "b"], True)
, ("\955a", R.Conc [R.All, "b"], False)
]
-- | Compare folding with actual solver evaluation over a bounded matrix of
-- regexes and strings. Keep the solver input symbolic and constrain its value
-- so the reference path cannot silently reuse literal constant folding.
regexLiteralAgreement :: Assertion
regexLiteralAgreement = do
observations <- runSMT $ do
input <- sString "input"
query $ forM samples $ \sample -> inNewAssertionStack $ do
constrain (input .== literal sample)
status <- checkSat
actual <- case status of
Sat -> getValue (S.implode [input `R.match` regex | regex <- regexes])
_ -> pure []
pure (sample, status, actual)
forM_ observations $ \(sample, status, actual) -> do
assertEqual "A concrete string assignment must be satisfiable" Sat status
assertEqual "One result per regex" (length regexes) (length actual)
forM_ (zip regexes actual) $ \(regex, expected) ->
assertEqual ("Literal/solver disagreement for " P.++ show sample P.++ " against " P.++ show regex)
(Just expected) (unliteral (literal sample `R.match` regex))
where atoms = [R.All, R.None, R.Conc [], "", "a", "ab"]
unary = [op regex | op <- [R.Comp, R.KStar, R.KPlus, R.Opt, R.Loop 0 2], regex <- atoms]
binary = [op left right | op <- [R.Inter, R.Diff, \a b -> R.Union [a, b]], left <- atoms, right <- atoms]
base = atoms P.++ unary P.++ binary
regexes = nub $ [regex | (_, regex, _) <- regexLiteralCases]
P.++ [wrapped | regex <- base, wrapped <- [regex, R.Conc [regex, "b"], R.Conc ["a", regex]]]
samples = nub $ concatMap (`replicateM` "ab") [0 .. 3] P.++ [sample | (sample, _, _) <- regexLiteralCases]
-- | Invalid bounds must fail on both literal and symbolic inputs, even when
-- matching could skip the offending branch. The printer uses the same check.
regexInvalidBounds :: Assertion
regexInvalidBounds = forM_ invalid $ \(regex, diagnostic) ->
forM_ wrappers $ \wrap -> do
let r = wrap regex
forM_ ["", "aa"] $ \sample ->
rejects diagnostic $ void $ evaluate (unliteral ((literal sample :: SString) `R.match` r))
rejects diagnostic $ void $ evaluate (length (show r))
rejects diagnostic $ runSMT $ do
input <- sString "input"
constrain (input `R.match` r)
-- Language equality bypasses match and exercises SMT serialization itself.
rejects diagnostic $ void $ sat (r .== R.All)
where invalid = [ (R.Loop 2 1 "a", "Loop with arguments: (2,1)")
, (R.Loop (-1) 2 "a", "Loop with arguments: (-1,2)")
, (R.Loop 0 (-1) "a", "Loop with arguments: (0,-1)")
, (R.Power (-1) "a", "Power with arguments: -1")
]
wrappers = [id, \r -> R.Union [R.All, r], \r -> R.Conc [R.None, r],
R.KStar, R.KPlus, R.Opt, R.Comp, R.Loop 0 0, R.Power 0,
R.Inter R.None, R.Diff R.None]
rejects diagnostic action = do
result <- try action :: IO (Either ErrorCall ())
case result of
Left err -> assertBool ("Expected diagnostic: " P.++ diagnostic) (diagnostic `isInfixOf` displayException err)
Right () -> assertFailure ("Accepted invalid regex: " P.++ diagnostic)
checkWith :: SMTConfig -> Symbolic () -> CheckSatResult -> IO ()
checkWith cfg props csExpected = runSMTWith cfg{verbose=True} $ do
_ <- props
query $ do cs <- checkSat
unless (cs == csExpected) $
case cs of
Unsat -> error "Failed! Expected Sat, got UNSAT"
DSat{} -> error "Failed! Expected Sat, got delta-sat"
Sat -> getModel >>= \r -> error $ "Failed! Expected Unsat, got SAT:\n" P.++ show (SatResult (Satisfiable cfg r))
Unk -> getUnknownReason >>= \r -> error $ "Failed! Expected Unsat, got UNK:\n" P.++ show r
strConcatSat :: Symbolic ()
strConcatSat = constrain $ "abc" ++ "def" .== ("abcdef" :: SString)
strConcatUnsat :: Symbolic ()
strConcatUnsat = constrain $ "abc" ++ "def" .== ("abcdefg" :: SString)
strIndexOfSat :: Symbolic ()
strIndexOfSat = constrain $ S.indexOf "abcabc" ("a" :: SString) .== 0
strIndexOfUnsat :: Symbolic ()
strIndexOfUnsat = constrain $ S.indexOf "abcabc" ("a" :: SString) ./= 0
-- Basic string operations
strExamples1 :: Symbolic ()
strExamples1 = constrain $ sAnd
[ S.singleton ("abc" !! 1) ++ S.singleton ("abc" !! 0) .== ("ba" :: SString)
, "abcabc" `S.indexOf` ("a" :: SString) .== 0
, S.offsetIndexOf "abcabc" ("a" :: SString) 1 .== 3
, S.subList "xxabcyy" 2 3 .== ("abc" :: SString)
]
-- A string cannot overlap with two different characters.
strExamples2 :: Symbolic ()
strExamples2 = do
a <- sString "a"
constrain $ a ++ "b" .== "a" ++ a
-- Strings a, b, c can have a non-trivial overlap.
strExamples3 :: Symbolic ()
strExamples3 = do
[a, b, c] <- sStrings ["a", "b", "c"]
constrain $ a ++ b .== "abcd"
constrain $ b ++ c .== "cdef"
constrain $ sNot $ b .== ""
-- There is a solution to a of length at most 2.
strExamples4 :: Symbolic ()
strExamples4 = do
[a, b] <- sStrings ["a", "b"]
constrain $ "abc" ++ a .== b ++ "cef"
constrain $ S.length a .<= 2
-- There is a solution to a that is not a sequence of "a"'s.
strExamples5 :: Symbolic ()
strExamples5 = do
[a, b, c] <- sStrings ["a", "b", "c"]
constrain $ a ++ "ab" ++ b .== b ++ "ba" ++ c
constrain $ c .== a ++ b
constrain $ sNot $ a ++ "a" .== "a" ++ a
-- Contains is transitive.
strExamples6 :: Symbolic ()
strExamples6 = do
[a, b, c] <- sStrings ["a", "b", "c"]
constrain $ b `S.isInfixOf` a
constrain $ c `S.isInfixOf` b
constrain $ sNot $ c `S.isInfixOf` a
-- But containment is not a linear order.
strExamples7 :: Symbolic ()
strExamples7 = do
[a, b, c] <- sStrings ["a", "b", "c"]
constrain $ b `S.isInfixOf` a
constrain $ c `S.isInfixOf` a
constrain $ sNot $ c `S.isInfixOf` b
constrain $ sNot $ b `S.isInfixOf` c
-- Any string is equal to the prefix and suffix that add up to its length.
strExamples8 :: Symbolic ()
strExamples8 = do
[a, b, c] <- sStrings ["a", "b", "c"]
constrain $ b `S.isPrefixOf` a
constrain $ c `S.isSuffixOf` a
constrain $ S.length a .== S.length b + S.length c
constrain $ sNot $ a .== b ++ c
-- The maximal length is 6 for a string of length 2 repeated at most 3 times
strExamples9 :: Symbolic ()
strExamples9 = do
a <- sString "a"
constrain $ R.match a (R.Loop 1 3 "ab")
constrain $ S.length a .== 6
-- The maximal length is 6 for a string of length 2 repeated at most 3 times
strExamples10 :: Symbolic ()
strExamples10 = do
a <- sString "a"
constrain $ R.match a (R.Loop 1 3 "ab")
constrain $ S.length a .> 6
-- Conversion from nat to string, only ground terms
strExamples11 :: Symbolic ()
strExamples11 = do
i <- sInteger "i"
constrain $ i .== 11
constrain $ sNot $ S.natToStr i .== "11"
-- Conversion from nat to string, negative values produce empty string
strExamples12 :: Symbolic ()
strExamples12 = do
i <- sInteger "i"
constrain $ i .== -2
constrain $ sNot $ S.natToStr i .== ""
-- Conversion from string to nat, only ground terms
strExamples13 :: Symbolic ()
strExamples13 = do
s <- sString "s"
constrain $ s .== "13"
constrain $ sNot $ S.strToNat s .== 13
-- Generate all length one strings consisting of letters A-Z, to enumerate all and making sure we can parse correctly
strExamples14 :: IO Bool
strExamples14 = do m <- allSat $ do s <- sString "s"
let c = SC.ord (S.head s)
constrain $ c .>= SC.ord (literal 'A')
constrain $ c .<= SC.ord (literal 'Z')
return $ S.length s .== 1
let dicts = getModelDictionaries m
vals :: [Int]
vals = map C.ord $ concat $ sort $ map (fromCV . snd) (concatMap M.assocs dicts)
case length dicts of
26 -> return $ vals == map C.ord ['A' .. 'Z']
_ -> return False