-- | This module provides various helper functionality
--   for participating in the SV-COMP comptetion, including
--   parsing comptetion set files, configuration data,
--   reporting results, etc.

{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
module Crux.SVCOMP where

import           Config.Schema
import           Control.Applicative
import           Data.Aeson (ToJSON)
import qualified Data.Attoparsec.Text as Atto
import           Data.Functor.Identity (Identity(..))
import           Data.Kind (Type)
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Text.IO as Text
import qualified Data.Yaml as Yaml
import           GHC.Generics (Generic)
import           System.FilePath
import qualified System.FilePath.Glob as Glob
import qualified Data.Vector as V

#if MIN_VERSION_aeson(2,0,0)
import qualified Data.Aeson.KeyMap as KM
#else
import qualified Data.HashMap.Strict as HM
#endif

import Crux.Config
import Crux.Config.Common


data SVCOMPOptions (f :: Type -> Type) = SVCOMPOptions
  { forall (f :: * -> *). SVCOMPOptions f -> [FilePath]
svcompBlacklist :: [FilePath]
      -- ^ Benchmarks to skip when evaluating in SV-COMP mode

  , forall (f :: * -> *). SVCOMPOptions f -> f Arch
svcompArch :: f Arch
      -- ^ The architecture assumed for the verification task

  , forall (f :: * -> *). SVCOMPOptions f -> f FilePath
svcompSpec :: f FilePath
      -- ^ The file containing the specification text used to verify the program. Likely a .prp file.

  , forall (f :: * -> *). SVCOMPOptions f -> FilePath
svcompWitnessOutput :: FilePath
      -- ^ Write the witness automaton to this filename
  }

data Arch = Arch32 | Arch64
  deriving (Int -> Arch -> ShowS
[Arch] -> ShowS
Arch -> FilePath
(Int -> Arch -> ShowS)
-> (Arch -> FilePath) -> ([Arch] -> ShowS) -> Show Arch
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Arch -> ShowS
showsPrec :: Int -> Arch -> ShowS
$cshow :: Arch -> FilePath
show :: Arch -> FilePath
$cshowList :: [Arch] -> ShowS
showList :: [Arch] -> ShowS
Show,Arch -> Arch -> Bool
(Arch -> Arch -> Bool) -> (Arch -> Arch -> Bool) -> Eq Arch
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Arch -> Arch -> Bool
== :: Arch -> Arch -> Bool
$c/= :: Arch -> Arch -> Bool
/= :: Arch -> Arch -> Bool
Eq,Eq Arch
Eq Arch =>
(Arch -> Arch -> Ordering)
-> (Arch -> Arch -> Bool)
-> (Arch -> Arch -> Bool)
-> (Arch -> Arch -> Bool)
-> (Arch -> Arch -> Bool)
-> (Arch -> Arch -> Arch)
-> (Arch -> Arch -> Arch)
-> Ord Arch
Arch -> Arch -> Bool
Arch -> Arch -> Ordering
Arch -> Arch -> Arch
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Arch -> Arch -> Ordering
compare :: Arch -> Arch -> Ordering
$c< :: Arch -> Arch -> Bool
< :: Arch -> Arch -> Bool
$c<= :: Arch -> Arch -> Bool
<= :: Arch -> Arch -> Bool
$c> :: Arch -> Arch -> Bool
> :: Arch -> Arch -> Bool
$c>= :: Arch -> Arch -> Bool
>= :: Arch -> Arch -> Bool
$cmax :: Arch -> Arch -> Arch
max :: Arch -> Arch -> Arch
$cmin :: Arch -> Arch -> Arch
min :: Arch -> Arch -> Arch
Ord)

archSpec :: ValueSpec Arch
archSpec :: ValueSpec Arch
archSpec =
  (Arch
Arch32 Arch -> ValueSpec () -> ValueSpec Arch
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"32bit") ValueSpec Arch -> ValueSpec Arch -> ValueSpec Arch
forall a. ValueSpec a -> ValueSpec a -> ValueSpec a
forall (f :: * -> *) a. Alt f => f a -> f a -> f a
<!>
  (Arch
Arch64 Arch -> ValueSpec () -> ValueSpec Arch
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"64bit")

parseArch :: (Arch -> opts -> opts) -> String -> OptSetter opts
parseArch :: forall opts. (Arch -> opts -> opts) -> FilePath -> OptSetter opts
parseArch Arch -> opts -> opts
mk = \FilePath
txt opts
opts ->
  case FilePath
txt of
    FilePath
"32bit" -> opts -> Either FilePath opts
forall a b. b -> Either a b
Right (Arch -> opts -> opts
mk Arch
Arch32 opts
opts)
    FilePath
"64bit" -> opts -> Either FilePath opts
forall a b. b -> Either a b
Right (Arch -> opts -> opts
mk Arch
Arch64 opts
opts)
    FilePath
_       -> FilePath -> Either FilePath opts
forall a b. a -> Either a b
Left FilePath
"Invalid architecture"

-- | We cannot verify an SV-COMP program without knowing the architecture and
-- the specification. Unfortunately, Crux's command-line argument parser makes
-- it somewhat awkward to require certain arguments (without defaults). As a
-- hacky workaround, we parse the command-line arguments for the
-- architecture/specification as if they were optional and later check here to
-- see if they were actually provided, throwing an error if they were not
-- provided.
processSVCOMPOptions :: SVCOMPOptions Maybe -> IO (SVCOMPOptions Identity)
processSVCOMPOptions :: SVCOMPOptions Maybe -> IO (SVCOMPOptions Identity)
processSVCOMPOptions
    (SVCOMPOptions{ Maybe Arch
svcompArch :: forall (f :: * -> *). SVCOMPOptions f -> f Arch
svcompArch :: Maybe Arch
svcompArch, Maybe FilePath
svcompSpec :: forall (f :: * -> *). SVCOMPOptions f -> f FilePath
svcompSpec :: Maybe FilePath
svcompSpec
                  , [FilePath]
svcompBlacklist :: forall (f :: * -> *). SVCOMPOptions f -> [FilePath]
svcompBlacklist :: [FilePath]
svcompBlacklist, FilePath
svcompWitnessOutput :: forall (f :: * -> *). SVCOMPOptions f -> FilePath
svcompWitnessOutput :: FilePath
svcompWitnessOutput}) = do
  Identity Arch
svcompArch' <- FilePath -> Maybe Arch -> IO (Identity Arch)
forall a. FilePath -> Maybe a -> IO (Identity a)
process FilePath
"svcomp-arch" Maybe Arch
svcompArch
  Identity FilePath
svcompSpec' <- FilePath -> Maybe FilePath -> IO (Identity FilePath)
forall a. FilePath -> Maybe a -> IO (Identity a)
process FilePath
"svcomp-spec" Maybe FilePath
svcompSpec
  pure $ SVCOMPOptions{ svcompArch :: Identity Arch
svcompArch = Identity Arch
svcompArch', svcompSpec :: Identity FilePath
svcompSpec = Identity FilePath
svcompSpec'
                      , [FilePath]
svcompBlacklist :: [FilePath]
svcompBlacklist :: [FilePath]
svcompBlacklist, FilePath
svcompWitnessOutput :: FilePath
svcompWitnessOutput :: FilePath
svcompWitnessOutput }
  where
    process :: String -> Maybe a -> IO (Identity a)
    process :: forall a. FilePath -> Maybe a -> IO (Identity a)
process FilePath
optName = IO (Identity a)
-> (a -> IO (Identity a)) -> Maybe a -> IO (Identity a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (FilePath -> IO (Identity a)
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO (Identity a)) -> FilePath -> IO (Identity a)
forall a b. (a -> b) -> a -> b
$ FilePath
"A value for --" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
optName FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
" must be provided") (Identity a -> IO (Identity a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Identity a -> IO (Identity a))
-> (a -> Identity a) -> a -> IO (Identity a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity a
forall a. a -> Identity a
Identity)

svcompOptions :: Config (SVCOMPOptions Maybe)
svcompOptions :: Config (SVCOMPOptions Maybe)
svcompOptions = Config
  { cfgFile :: SectionsSpec (SVCOMPOptions Maybe)
cfgFile =
      do [FilePath]
svcompBlacklist <-
           Text
-> ValueSpec [FilePath]
-> [FilePath]
-> Text
-> SectionsSpec [FilePath]
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"svcomp-blacklist" (ValueSpec FilePath -> ValueSpec [FilePath]
forall a. ValueSpec a -> ValueSpec [a]
listSpec ValueSpec FilePath
stringSpec) []
           Text
"SV-COMP benchmark tasks to skip"

         Maybe Arch
svcompArch <-
           Text -> ValueSpec Arch -> Text -> SectionsSpec (Maybe Arch)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"svcomp-arch" ValueSpec Arch
archSpec
           Text
"The architecture assumed for the verification task."

         Maybe FilePath
svcompSpec <-
           Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"svcomp-spec" ValueSpec FilePath
fileSpec
           Text
"The file containing the specification text used to verify the program. Likely a .prp file."

         FilePath
svcompWitnessOutput <-
           Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"svcomp-witness-output" ValueSpec FilePath
fileSpec FilePath
"witness.graphml"
           ([Text] -> Text
Text.unwords [ Text
"The file name to which the witness automaton file should be written"
                         , Text
"(default: witness.graphml)."
                         ])

         return SVCOMPOptions{ FilePath
[FilePath]
Maybe FilePath
Maybe Arch
svcompBlacklist :: [FilePath]
svcompArch :: Maybe Arch
svcompSpec :: Maybe FilePath
svcompWitnessOutput :: FilePath
svcompBlacklist :: [FilePath]
svcompArch :: Maybe Arch
svcompSpec :: Maybe FilePath
svcompWitnessOutput :: FilePath
.. }

  , cfgEnv :: [EnvDescr (SVCOMPOptions Maybe)]
cfgEnv = []

  , cfgCmdLineFlag :: [OptDescr (SVCOMPOptions Maybe)]
cfgCmdLineFlag =
      [ FilePath
-> [FilePath]
-> FilePath
-> ArgDescr (SVCOMPOptions Maybe)
-> OptDescr (SVCOMPOptions Maybe)
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"svcomp-arch"]
        FilePath
"The architecture assumed for the verification task."
        (ArgDescr (SVCOMPOptions Maybe) -> OptDescr (SVCOMPOptions Maybe))
-> ArgDescr (SVCOMPOptions Maybe) -> OptDescr (SVCOMPOptions Maybe)
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter (SVCOMPOptions Maybe))
-> ArgDescr (SVCOMPOptions Maybe)
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"`32bit` or `64bit`"
        ((FilePath -> OptSetter (SVCOMPOptions Maybe))
 -> ArgDescr (SVCOMPOptions Maybe))
-> (FilePath -> OptSetter (SVCOMPOptions Maybe))
-> ArgDescr (SVCOMPOptions Maybe)
forall a b. (a -> b) -> a -> b
$ (Arch -> SVCOMPOptions Maybe -> SVCOMPOptions Maybe)
-> FilePath -> OptSetter (SVCOMPOptions Maybe)
forall opts. (Arch -> opts -> opts) -> FilePath -> OptSetter opts
parseArch
        ((Arch -> SVCOMPOptions Maybe -> SVCOMPOptions Maybe)
 -> FilePath -> OptSetter (SVCOMPOptions Maybe))
-> (Arch -> SVCOMPOptions Maybe -> SVCOMPOptions Maybe)
-> FilePath
-> OptSetter (SVCOMPOptions Maybe)
forall a b. (a -> b) -> a -> b
$ \Arch
a SVCOMPOptions Maybe
opts -> SVCOMPOptions Maybe
opts{ svcompArch = Just a }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr (SVCOMPOptions Maybe)
-> OptDescr (SVCOMPOptions Maybe)
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"svcomp-spec"]
        FilePath
"The file containing the specification text used to verify the program. Likely a .prp file."
        (ArgDescr (SVCOMPOptions Maybe) -> OptDescr (SVCOMPOptions Maybe))
-> ArgDescr (SVCOMPOptions Maybe) -> OptDescr (SVCOMPOptions Maybe)
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter (SVCOMPOptions Maybe))
-> ArgDescr (SVCOMPOptions Maybe)
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"FILE"
        ((FilePath -> OptSetter (SVCOMPOptions Maybe))
 -> ArgDescr (SVCOMPOptions Maybe))
-> (FilePath -> OptSetter (SVCOMPOptions Maybe))
-> ArgDescr (SVCOMPOptions Maybe)
forall a b. (a -> b) -> a -> b
$ \FilePath
f SVCOMPOptions Maybe
opts -> OptSetter (SVCOMPOptions Maybe)
forall a b. b -> Either a b
Right SVCOMPOptions Maybe
opts{ svcompSpec = Just f }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr (SVCOMPOptions Maybe)
-> OptDescr (SVCOMPOptions Maybe)
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"svcomp-witness-output"]
        ([FilePath] -> FilePath
unwords [ FilePath
"The file name to which the witness automaton file should be written"
                 , FilePath
"(default: witness.graphml)."
                 ])
        (ArgDescr (SVCOMPOptions Maybe) -> OptDescr (SVCOMPOptions Maybe))
-> ArgDescr (SVCOMPOptions Maybe) -> OptDescr (SVCOMPOptions Maybe)
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter (SVCOMPOptions Maybe))
-> ArgDescr (SVCOMPOptions Maybe)
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"FILE"
        ((FilePath -> OptSetter (SVCOMPOptions Maybe))
 -> ArgDescr (SVCOMPOptions Maybe))
-> (FilePath -> OptSetter (SVCOMPOptions Maybe))
-> ArgDescr (SVCOMPOptions Maybe)
forall a b. (a -> b) -> a -> b
$ \FilePath
f SVCOMPOptions Maybe
opts -> OptSetter (SVCOMPOptions Maybe)
forall a b. b -> Either a b
Right SVCOMPOptions Maybe
opts{ svcompWitnessOutput = f }
      ]
  }

propertyVerdict :: VerificationTask -> Maybe Bool
propertyVerdict :: VerificationTask -> Maybe Bool
propertyVerdict VerificationTask
task = (Maybe Bool -> (SVCompProperty, Maybe Bool) -> Maybe Bool)
-> Maybe Bool -> [(SVCompProperty, Maybe Bool)] -> Maybe Bool
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Maybe Bool -> (SVCompProperty, Maybe Bool) -> Maybe Bool
f Maybe Bool
forall a. Maybe a
Nothing (VerificationTask -> [(SVCompProperty, Maybe Bool)]
verificationProperties VerificationTask
task)
 where
 comb :: Bool -> Maybe Bool -> Maybe Bool
comb Bool
b Maybe Bool
Nothing  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b
 comb Bool
b (Just Bool
x) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$! Bool
b Bool -> Bool -> Bool
&& Bool
x

 f :: Maybe Bool -> (SVCompProperty, Maybe Bool) -> Maybe Bool
f Maybe Bool
v (CheckNoError Text
_nm, Just Bool
b)  = Bool -> Maybe Bool -> Maybe Bool
comb Bool
b Maybe Bool
v
 f Maybe Bool
v (SVCompProperty
CheckValidFree, Just Bool
b)    = Bool -> Maybe Bool -> Maybe Bool
comb Bool
b Maybe Bool
v
 f Maybe Bool
v (SVCompProperty
CheckValidDeref, Just Bool
b)   = Bool -> Maybe Bool -> Maybe Bool
comb Bool
b Maybe Bool
v
 f Maybe Bool
v (SVCompProperty
CheckDefBehavior, Just Bool
b)  = Bool -> Maybe Bool -> Maybe Bool
comb Bool
b Maybe Bool
v
 f Maybe Bool
v (SVCompProperty
CheckNoOverflow, Just Bool
b)   = Bool -> Maybe Bool -> Maybe Bool
comb Bool
b Maybe Bool
v
 f Maybe Bool
v (SVCompProperty, Maybe Bool)
_ = Maybe Bool
v

data ComputedVerdict
  = Verified
  | Falsified
  | Unknown
 deriving (ComputedVerdict -> ComputedVerdict -> Bool
(ComputedVerdict -> ComputedVerdict -> Bool)
-> (ComputedVerdict -> ComputedVerdict -> Bool)
-> Eq ComputedVerdict
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ComputedVerdict -> ComputedVerdict -> Bool
== :: ComputedVerdict -> ComputedVerdict -> Bool
$c/= :: ComputedVerdict -> ComputedVerdict -> Bool
/= :: ComputedVerdict -> ComputedVerdict -> Bool
Eq, (forall x. ComputedVerdict -> Rep ComputedVerdict x)
-> (forall x. Rep ComputedVerdict x -> ComputedVerdict)
-> Generic ComputedVerdict
forall x. Rep ComputedVerdict x -> ComputedVerdict
forall x. ComputedVerdict -> Rep ComputedVerdict x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ComputedVerdict -> Rep ComputedVerdict x
from :: forall x. ComputedVerdict -> Rep ComputedVerdict x
$cto :: forall x. Rep ComputedVerdict x -> ComputedVerdict
to :: forall x. Rep ComputedVerdict x -> ComputedVerdict
Generic, Eq ComputedVerdict
Eq ComputedVerdict =>
(ComputedVerdict -> ComputedVerdict -> Ordering)
-> (ComputedVerdict -> ComputedVerdict -> Bool)
-> (ComputedVerdict -> ComputedVerdict -> Bool)
-> (ComputedVerdict -> ComputedVerdict -> Bool)
-> (ComputedVerdict -> ComputedVerdict -> Bool)
-> (ComputedVerdict -> ComputedVerdict -> ComputedVerdict)
-> (ComputedVerdict -> ComputedVerdict -> ComputedVerdict)
-> Ord ComputedVerdict
ComputedVerdict -> ComputedVerdict -> Bool
ComputedVerdict -> ComputedVerdict -> Ordering
ComputedVerdict -> ComputedVerdict -> ComputedVerdict
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ComputedVerdict -> ComputedVerdict -> Ordering
compare :: ComputedVerdict -> ComputedVerdict -> Ordering
$c< :: ComputedVerdict -> ComputedVerdict -> Bool
< :: ComputedVerdict -> ComputedVerdict -> Bool
$c<= :: ComputedVerdict -> ComputedVerdict -> Bool
<= :: ComputedVerdict -> ComputedVerdict -> Bool
$c> :: ComputedVerdict -> ComputedVerdict -> Bool
> :: ComputedVerdict -> ComputedVerdict -> Bool
$c>= :: ComputedVerdict -> ComputedVerdict -> Bool
>= :: ComputedVerdict -> ComputedVerdict -> Bool
$cmax :: ComputedVerdict -> ComputedVerdict -> ComputedVerdict
max :: ComputedVerdict -> ComputedVerdict -> ComputedVerdict
$cmin :: ComputedVerdict -> ComputedVerdict -> ComputedVerdict
min :: ComputedVerdict -> ComputedVerdict -> ComputedVerdict
Ord, Int -> ComputedVerdict -> ShowS
[ComputedVerdict] -> ShowS
ComputedVerdict -> FilePath
(Int -> ComputedVerdict -> ShowS)
-> (ComputedVerdict -> FilePath)
-> ([ComputedVerdict] -> ShowS)
-> Show ComputedVerdict
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ComputedVerdict -> ShowS
showsPrec :: Int -> ComputedVerdict -> ShowS
$cshow :: ComputedVerdict -> FilePath
show :: ComputedVerdict -> FilePath
$cshowList :: [ComputedVerdict] -> ShowS
showList :: [ComputedVerdict] -> ShowS
Show, [ComputedVerdict] -> Value
[ComputedVerdict] -> Encoding
ComputedVerdict -> Bool
ComputedVerdict -> Value
ComputedVerdict -> Encoding
(ComputedVerdict -> Value)
-> (ComputedVerdict -> Encoding)
-> ([ComputedVerdict] -> Value)
-> ([ComputedVerdict] -> Encoding)
-> (ComputedVerdict -> Bool)
-> ToJSON ComputedVerdict
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: ComputedVerdict -> Value
toJSON :: ComputedVerdict -> Value
$ctoEncoding :: ComputedVerdict -> Encoding
toEncoding :: ComputedVerdict -> Encoding
$ctoJSONList :: [ComputedVerdict] -> Value
toJSONList :: [ComputedVerdict] -> Value
$ctoEncodingList :: [ComputedVerdict] -> Encoding
toEncodingList :: [ComputedVerdict] -> Encoding
$comitField :: ComputedVerdict -> Bool
omitField :: ComputedVerdict -> Bool
ToJSON)

data BenchmarkSet =
  BenchmarkSet
  { BenchmarkSet -> Text
benchmarkName :: Text
  , BenchmarkSet -> [VerificationTask]
benchmarkTasks :: [VerificationTask]
  }
 deriving (Int -> BenchmarkSet -> ShowS
[BenchmarkSet] -> ShowS
BenchmarkSet -> FilePath
(Int -> BenchmarkSet -> ShowS)
-> (BenchmarkSet -> FilePath)
-> ([BenchmarkSet] -> ShowS)
-> Show BenchmarkSet
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BenchmarkSet -> ShowS
showsPrec :: Int -> BenchmarkSet -> ShowS
$cshow :: BenchmarkSet -> FilePath
show :: BenchmarkSet -> FilePath
$cshowList :: [BenchmarkSet] -> ShowS
showList :: [BenchmarkSet] -> ShowS
Show,BenchmarkSet -> BenchmarkSet -> Bool
(BenchmarkSet -> BenchmarkSet -> Bool)
-> (BenchmarkSet -> BenchmarkSet -> Bool) -> Eq BenchmarkSet
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BenchmarkSet -> BenchmarkSet -> Bool
== :: BenchmarkSet -> BenchmarkSet -> Bool
$c/= :: BenchmarkSet -> BenchmarkSet -> Bool
/= :: BenchmarkSet -> BenchmarkSet -> Bool
Eq,Eq BenchmarkSet
Eq BenchmarkSet =>
(BenchmarkSet -> BenchmarkSet -> Ordering)
-> (BenchmarkSet -> BenchmarkSet -> Bool)
-> (BenchmarkSet -> BenchmarkSet -> Bool)
-> (BenchmarkSet -> BenchmarkSet -> Bool)
-> (BenchmarkSet -> BenchmarkSet -> Bool)
-> (BenchmarkSet -> BenchmarkSet -> BenchmarkSet)
-> (BenchmarkSet -> BenchmarkSet -> BenchmarkSet)
-> Ord BenchmarkSet
BenchmarkSet -> BenchmarkSet -> Bool
BenchmarkSet -> BenchmarkSet -> Ordering
BenchmarkSet -> BenchmarkSet -> BenchmarkSet
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BenchmarkSet -> BenchmarkSet -> Ordering
compare :: BenchmarkSet -> BenchmarkSet -> Ordering
$c< :: BenchmarkSet -> BenchmarkSet -> Bool
< :: BenchmarkSet -> BenchmarkSet -> Bool
$c<= :: BenchmarkSet -> BenchmarkSet -> Bool
<= :: BenchmarkSet -> BenchmarkSet -> Bool
$c> :: BenchmarkSet -> BenchmarkSet -> Bool
> :: BenchmarkSet -> BenchmarkSet -> Bool
$c>= :: BenchmarkSet -> BenchmarkSet -> Bool
>= :: BenchmarkSet -> BenchmarkSet -> Bool
$cmax :: BenchmarkSet -> BenchmarkSet -> BenchmarkSet
max :: BenchmarkSet -> BenchmarkSet -> BenchmarkSet
$cmin :: BenchmarkSet -> BenchmarkSet -> BenchmarkSet
min :: BenchmarkSet -> BenchmarkSet -> BenchmarkSet
Ord)

data SVCompProperty
  = CheckNoError Text
  | CheckValidFree
  | CheckValidDeref
  | CheckValidMemtrack
  | CheckValidMemCleanup
  | CheckDefBehavior
  | CheckNoOverflow
  | CheckTerminates
  | CoverageFQL Text
 deriving (Int -> SVCompProperty -> ShowS
[SVCompProperty] -> ShowS
SVCompProperty -> FilePath
(Int -> SVCompProperty -> ShowS)
-> (SVCompProperty -> FilePath)
-> ([SVCompProperty] -> ShowS)
-> Show SVCompProperty
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SVCompProperty -> ShowS
showsPrec :: Int -> SVCompProperty -> ShowS
$cshow :: SVCompProperty -> FilePath
show :: SVCompProperty -> FilePath
$cshowList :: [SVCompProperty] -> ShowS
showList :: [SVCompProperty] -> ShowS
Show,SVCompProperty -> SVCompProperty -> Bool
(SVCompProperty -> SVCompProperty -> Bool)
-> (SVCompProperty -> SVCompProperty -> Bool) -> Eq SVCompProperty
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SVCompProperty -> SVCompProperty -> Bool
== :: SVCompProperty -> SVCompProperty -> Bool
$c/= :: SVCompProperty -> SVCompProperty -> Bool
/= :: SVCompProperty -> SVCompProperty -> Bool
Eq,Eq SVCompProperty
Eq SVCompProperty =>
(SVCompProperty -> SVCompProperty -> Ordering)
-> (SVCompProperty -> SVCompProperty -> Bool)
-> (SVCompProperty -> SVCompProperty -> Bool)
-> (SVCompProperty -> SVCompProperty -> Bool)
-> (SVCompProperty -> SVCompProperty -> Bool)
-> (SVCompProperty -> SVCompProperty -> SVCompProperty)
-> (SVCompProperty -> SVCompProperty -> SVCompProperty)
-> Ord SVCompProperty
SVCompProperty -> SVCompProperty -> Bool
SVCompProperty -> SVCompProperty -> Ordering
SVCompProperty -> SVCompProperty -> SVCompProperty
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SVCompProperty -> SVCompProperty -> Ordering
compare :: SVCompProperty -> SVCompProperty -> Ordering
$c< :: SVCompProperty -> SVCompProperty -> Bool
< :: SVCompProperty -> SVCompProperty -> Bool
$c<= :: SVCompProperty -> SVCompProperty -> Bool
<= :: SVCompProperty -> SVCompProperty -> Bool
$c> :: SVCompProperty -> SVCompProperty -> Bool
> :: SVCompProperty -> SVCompProperty -> Bool
$c>= :: SVCompProperty -> SVCompProperty -> Bool
>= :: SVCompProperty -> SVCompProperty -> Bool
$cmax :: SVCompProperty -> SVCompProperty -> SVCompProperty
max :: SVCompProperty -> SVCompProperty -> SVCompProperty
$cmin :: SVCompProperty -> SVCompProperty -> SVCompProperty
min :: SVCompProperty -> SVCompProperty -> SVCompProperty
Ord,(forall x. SVCompProperty -> Rep SVCompProperty x)
-> (forall x. Rep SVCompProperty x -> SVCompProperty)
-> Generic SVCompProperty
forall x. Rep SVCompProperty x -> SVCompProperty
forall x. SVCompProperty -> Rep SVCompProperty x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SVCompProperty -> Rep SVCompProperty x
from :: forall x. SVCompProperty -> Rep SVCompProperty x
$cto :: forall x. Rep SVCompProperty x -> SVCompProperty
to :: forall x. Rep SVCompProperty x -> SVCompProperty
Generic,[SVCompProperty] -> Value
[SVCompProperty] -> Encoding
SVCompProperty -> Bool
SVCompProperty -> Value
SVCompProperty -> Encoding
(SVCompProperty -> Value)
-> (SVCompProperty -> Encoding)
-> ([SVCompProperty] -> Value)
-> ([SVCompProperty] -> Encoding)
-> (SVCompProperty -> Bool)
-> ToJSON SVCompProperty
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: SVCompProperty -> Value
toJSON :: SVCompProperty -> Value
$ctoEncoding :: SVCompProperty -> Encoding
toEncoding :: SVCompProperty -> Encoding
$ctoJSONList :: [SVCompProperty] -> Value
toJSONList :: [SVCompProperty] -> Value
$ctoEncodingList :: [SVCompProperty] -> Encoding
toEncodingList :: [SVCompProperty] -> Encoding
$comitField :: SVCompProperty -> Bool
omitField :: SVCompProperty -> Bool
ToJSON)

data SVCompLanguage
  = C CDataModel
  | Java
 deriving (Int -> SVCompLanguage -> ShowS
[SVCompLanguage] -> ShowS
SVCompLanguage -> FilePath
(Int -> SVCompLanguage -> ShowS)
-> (SVCompLanguage -> FilePath)
-> ([SVCompLanguage] -> ShowS)
-> Show SVCompLanguage
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SVCompLanguage -> ShowS
showsPrec :: Int -> SVCompLanguage -> ShowS
$cshow :: SVCompLanguage -> FilePath
show :: SVCompLanguage -> FilePath
$cshowList :: [SVCompLanguage] -> ShowS
showList :: [SVCompLanguage] -> ShowS
Show,SVCompLanguage -> SVCompLanguage -> Bool
(SVCompLanguage -> SVCompLanguage -> Bool)
-> (SVCompLanguage -> SVCompLanguage -> Bool) -> Eq SVCompLanguage
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SVCompLanguage -> SVCompLanguage -> Bool
== :: SVCompLanguage -> SVCompLanguage -> Bool
$c/= :: SVCompLanguage -> SVCompLanguage -> Bool
/= :: SVCompLanguage -> SVCompLanguage -> Bool
Eq,Eq SVCompLanguage
Eq SVCompLanguage =>
(SVCompLanguage -> SVCompLanguage -> Ordering)
-> (SVCompLanguage -> SVCompLanguage -> Bool)
-> (SVCompLanguage -> SVCompLanguage -> Bool)
-> (SVCompLanguage -> SVCompLanguage -> Bool)
-> (SVCompLanguage -> SVCompLanguage -> Bool)
-> (SVCompLanguage -> SVCompLanguage -> SVCompLanguage)
-> (SVCompLanguage -> SVCompLanguage -> SVCompLanguage)
-> Ord SVCompLanguage
SVCompLanguage -> SVCompLanguage -> Bool
SVCompLanguage -> SVCompLanguage -> Ordering
SVCompLanguage -> SVCompLanguage -> SVCompLanguage
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SVCompLanguage -> SVCompLanguage -> Ordering
compare :: SVCompLanguage -> SVCompLanguage -> Ordering
$c< :: SVCompLanguage -> SVCompLanguage -> Bool
< :: SVCompLanguage -> SVCompLanguage -> Bool
$c<= :: SVCompLanguage -> SVCompLanguage -> Bool
<= :: SVCompLanguage -> SVCompLanguage -> Bool
$c> :: SVCompLanguage -> SVCompLanguage -> Bool
> :: SVCompLanguage -> SVCompLanguage -> Bool
$c>= :: SVCompLanguage -> SVCompLanguage -> Bool
>= :: SVCompLanguage -> SVCompLanguage -> Bool
$cmax :: SVCompLanguage -> SVCompLanguage -> SVCompLanguage
max :: SVCompLanguage -> SVCompLanguage -> SVCompLanguage
$cmin :: SVCompLanguage -> SVCompLanguage -> SVCompLanguage
min :: SVCompLanguage -> SVCompLanguage -> SVCompLanguage
Ord)

data CDataModel = ILP32 | LP64
 deriving (Int -> CDataModel -> ShowS
[CDataModel] -> ShowS
CDataModel -> FilePath
(Int -> CDataModel -> ShowS)
-> (CDataModel -> FilePath)
-> ([CDataModel] -> ShowS)
-> Show CDataModel
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CDataModel -> ShowS
showsPrec :: Int -> CDataModel -> ShowS
$cshow :: CDataModel -> FilePath
show :: CDataModel -> FilePath
$cshowList :: [CDataModel] -> ShowS
showList :: [CDataModel] -> ShowS
Show,CDataModel -> CDataModel -> Bool
(CDataModel -> CDataModel -> Bool)
-> (CDataModel -> CDataModel -> Bool) -> Eq CDataModel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CDataModel -> CDataModel -> Bool
== :: CDataModel -> CDataModel -> Bool
$c/= :: CDataModel -> CDataModel -> Bool
/= :: CDataModel -> CDataModel -> Bool
Eq,Eq CDataModel
Eq CDataModel =>
(CDataModel -> CDataModel -> Ordering)
-> (CDataModel -> CDataModel -> Bool)
-> (CDataModel -> CDataModel -> Bool)
-> (CDataModel -> CDataModel -> Bool)
-> (CDataModel -> CDataModel -> Bool)
-> (CDataModel -> CDataModel -> CDataModel)
-> (CDataModel -> CDataModel -> CDataModel)
-> Ord CDataModel
CDataModel -> CDataModel -> Bool
CDataModel -> CDataModel -> Ordering
CDataModel -> CDataModel -> CDataModel
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: CDataModel -> CDataModel -> Ordering
compare :: CDataModel -> CDataModel -> Ordering
$c< :: CDataModel -> CDataModel -> Bool
< :: CDataModel -> CDataModel -> Bool
$c<= :: CDataModel -> CDataModel -> Bool
<= :: CDataModel -> CDataModel -> Bool
$c> :: CDataModel -> CDataModel -> Bool
> :: CDataModel -> CDataModel -> Bool
$c>= :: CDataModel -> CDataModel -> Bool
>= :: CDataModel -> CDataModel -> Bool
$cmax :: CDataModel -> CDataModel -> CDataModel
max :: CDataModel -> CDataModel -> CDataModel
$cmin :: CDataModel -> CDataModel -> CDataModel
min :: CDataModel -> CDataModel -> CDataModel
Ord)

data VerificationTask =
  VerificationTask
  { VerificationTask -> FilePath
verificationSourceFile :: FilePath
  , VerificationTask -> [FilePath]
verificationInputFiles :: [FilePath]
  , VerificationTask -> [(SVCompProperty, Maybe Bool)]
verificationProperties :: [(SVCompProperty, Maybe Bool)]
  , VerificationTask -> SVCompLanguage
verificationLanguage   :: SVCompLanguage
  }
 deriving (Int -> VerificationTask -> ShowS
[VerificationTask] -> ShowS
VerificationTask -> FilePath
(Int -> VerificationTask -> ShowS)
-> (VerificationTask -> FilePath)
-> ([VerificationTask] -> ShowS)
-> Show VerificationTask
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VerificationTask -> ShowS
showsPrec :: Int -> VerificationTask -> ShowS
$cshow :: VerificationTask -> FilePath
show :: VerificationTask -> FilePath
$cshowList :: [VerificationTask] -> ShowS
showList :: [VerificationTask] -> ShowS
Show,VerificationTask -> VerificationTask -> Bool
(VerificationTask -> VerificationTask -> Bool)
-> (VerificationTask -> VerificationTask -> Bool)
-> Eq VerificationTask
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VerificationTask -> VerificationTask -> Bool
== :: VerificationTask -> VerificationTask -> Bool
$c/= :: VerificationTask -> VerificationTask -> Bool
/= :: VerificationTask -> VerificationTask -> Bool
Eq,Eq VerificationTask
Eq VerificationTask =>
(VerificationTask -> VerificationTask -> Ordering)
-> (VerificationTask -> VerificationTask -> Bool)
-> (VerificationTask -> VerificationTask -> Bool)
-> (VerificationTask -> VerificationTask -> Bool)
-> (VerificationTask -> VerificationTask -> Bool)
-> (VerificationTask -> VerificationTask -> VerificationTask)
-> (VerificationTask -> VerificationTask -> VerificationTask)
-> Ord VerificationTask
VerificationTask -> VerificationTask -> Bool
VerificationTask -> VerificationTask -> Ordering
VerificationTask -> VerificationTask -> VerificationTask
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: VerificationTask -> VerificationTask -> Ordering
compare :: VerificationTask -> VerificationTask -> Ordering
$c< :: VerificationTask -> VerificationTask -> Bool
< :: VerificationTask -> VerificationTask -> Bool
$c<= :: VerificationTask -> VerificationTask -> Bool
<= :: VerificationTask -> VerificationTask -> Bool
$c> :: VerificationTask -> VerificationTask -> Bool
> :: VerificationTask -> VerificationTask -> Bool
$c>= :: VerificationTask -> VerificationTask -> Bool
>= :: VerificationTask -> VerificationTask -> Bool
$cmax :: VerificationTask -> VerificationTask -> VerificationTask
max :: VerificationTask -> VerificationTask -> VerificationTask
$cmin :: VerificationTask -> VerificationTask -> VerificationTask
min :: VerificationTask -> VerificationTask -> VerificationTask
Ord)

checkParse :: Atto.Parser SVCompProperty
checkParse :: Parser SVCompProperty
checkParse = Parser ()
Atto.skipSpace Parser () -> Parser Text Text -> Parser Text Text
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Text -> Parser Text Text
Atto.string Text
"init(main())," Parser Text Text -> Parser () -> Parser ()
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
Atto.skipSpace Parser () -> Parser SVCompProperty -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser SVCompProperty
ltl
 where
 ltl :: Parser SVCompProperty
ltl = Text -> Parser Text Text
Atto.string Text
"LTL(" Parser Text Text -> Parser () -> Parser ()
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
Atto.skipSpace Parser () -> Parser SVCompProperty -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser SVCompProperty
go Parser SVCompProperty -> Parser () -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
Atto.skipSpace Parser SVCompProperty -> Parser Text Text -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text Text
Atto.string Text
")" Parser SVCompProperty -> Parser () -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
Atto.skipSpace
 go :: Parser SVCompProperty
go = [Parser SVCompProperty] -> Parser SVCompProperty
forall (f :: * -> *) a. Alternative f => [f a] -> f a
Atto.choice
      [ Text -> SVCompProperty
CheckNoError (Text -> SVCompProperty)
-> Parser Text Text -> Parser SVCompProperty
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text Text
Atto.string Text
"G ! call(" Parser Text Text -> Parser Text Text -> Parser Text Text
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Text Text
bracketedText Parser Text Text -> Parser Text Text -> Parser Text Text
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Text Text
")")
      , SVCompProperty -> Parser SVCompProperty
forall a. a -> Parser Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SVCompProperty
CheckTerminates      Parser SVCompProperty -> Parser Text Text -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text Text
Atto.string Text
"F end"
      , SVCompProperty -> Parser SVCompProperty
forall a. a -> Parser Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SVCompProperty
CheckValidFree       Parser SVCompProperty -> Parser Text Text -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text Text
Atto.string Text
"G valid-free"
      , SVCompProperty -> Parser SVCompProperty
forall a. a -> Parser Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SVCompProperty
CheckValidDeref      Parser SVCompProperty -> Parser Text Text -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text Text
Atto.string Text
"G valid-deref"
      , SVCompProperty -> Parser SVCompProperty
forall a. a -> Parser Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SVCompProperty
CheckValidMemtrack   Parser SVCompProperty -> Parser Text Text -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text Text
Atto.string Text
"G valid-memtrack"
      , SVCompProperty -> Parser SVCompProperty
forall a. a -> Parser Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SVCompProperty
CheckValidMemCleanup Parser SVCompProperty -> Parser Text Text -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text Text
Atto.string Text
"G valid-memcleanup"
      , SVCompProperty -> Parser SVCompProperty
forall a. a -> Parser Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SVCompProperty
CheckNoOverflow      Parser SVCompProperty -> Parser Text Text -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text Text
Atto.string Text
"G ! overflow"
      , SVCompProperty -> Parser SVCompProperty
forall a. a -> Parser Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SVCompProperty
CheckDefBehavior     Parser SVCompProperty -> Parser Text Text -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Text -> Parser Text Text
Atto.string Text
"G def-behavior"
      ]

coverParse :: Atto.Parser SVCompProperty
coverParse :: Parser SVCompProperty
coverParse = Text -> SVCompProperty
CoverageFQL (Text -> SVCompProperty)
-> Parser Text Text -> Parser SVCompProperty
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser ()
Atto.skipSpace Parser () -> Parser Text Text -> Parser Text Text
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Text -> Parser Text Text
Atto.string Text
"init(main())," Parser Text Text -> Parser () -> Parser ()
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
Atto.skipSpace Parser () -> Parser Text Text -> Parser Text Text
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Text Text
bracketedText)

bracketedText :: Atto.Parser Text
bracketedText :: Parser Text Text
bracketedText =
 do Text
xs <- (Char -> Bool) -> Parser Text Text
Atto.takeTill (\Char
x -> Char
x Char -> FilePath -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
'(',Char
')'])
    (do Char
_ <- Char -> Parser Char
Atto.char Char
'('
        Text
ys <- Parser Text Text
bracketedText
        Char
_ <- Char -> Parser Char
Atto.char Char
')'
        Text
zs <- Parser Text Text
bracketedText
        return (Text
xs Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ys Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
zs)
     ) Parser Text Text -> Parser Text Text -> Parser Text Text
forall a. Parser Text a -> Parser Text a -> Parser Text a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Text -> Parser Text Text
forall a. a -> Parser Text a
forall (m :: * -> *) a. Monad m => a -> m a
return Text
xs)


propParse :: Atto.Parser SVCompProperty
propParse :: Parser SVCompProperty
propParse = Parser ()
Atto.skipSpace Parser () -> Parser SVCompProperty -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [Parser SVCompProperty] -> Parser SVCompProperty
forall (f :: * -> *) a. Alternative f => [f a] -> f a
Atto.choice
  [ Text -> Parser Text Text
Atto.string Text
"CHECK(" Parser Text Text -> Parser SVCompProperty -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser SVCompProperty
checkParse Parser SVCompProperty -> Parser Text Text -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Text Text
")"
  , Text -> Parser Text Text
Atto.string Text
"COVER(" Parser Text Text -> Parser SVCompProperty -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser SVCompProperty
coverParse Parser SVCompProperty -> Parser Text Text -> Parser SVCompProperty
forall a b. Parser Text a -> Parser Text b -> Parser Text a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Text Text
")"
  ]

loadVerificationTask :: FilePath -> IO VerificationTask
loadVerificationTask :: FilePath -> IO VerificationTask
loadVerificationTask FilePath
fp =
   FilePath -> IO (Either ParseException Value)
forall a. FromJSON a => FilePath -> IO (Either ParseException a)
Yaml.decodeFileEither FilePath
fp IO (Either ParseException Value)
-> (Either ParseException Value -> IO VerificationTask)
-> IO VerificationTask
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
     Left ParseException
err -> FilePath -> IO VerificationTask
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO VerificationTask)
-> FilePath -> IO VerificationTask
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [FilePath
"Failure parsing YAML file: " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> FilePath
show FilePath
fp, ParseException -> FilePath
forall a. Show a => a -> FilePath
show ParseException
err]
     Right Value
a  -> Value -> IO VerificationTask
decodeVT Value
a
 where
 decodeVT :: Yaml.Value -> IO VerificationTask
 decodeVT :: Value -> IO VerificationTask
decodeVT (Yaml.Object Object
o) =
  do case Key -> Object -> Maybe Value
forall {v}. Key -> KeyMap v -> Maybe v
lookupKM Key
"format_version" Object
o of
       Just (Yaml.String Text
"2.0") -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       Maybe Value
_ -> FilePath -> IO ()
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"Expected verification task version 2.0 while parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

     [FilePath]
fs <- case Key -> Object -> Maybe Value
forall {v}. Key -> KeyMap v -> Maybe v
lookupKM Key
"input_files" Object
o of
             Just Value
v -> Value -> IO [FilePath]
forall {m :: * -> *}. MonadFail m => Value -> m [FilePath]
getStrs Value
v
             Maybe Value
Nothing -> FilePath -> IO [FilePath]
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO [FilePath]) -> FilePath -> IO [FilePath]
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"No 'input_files' section while parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

     [(SVCompProperty, Maybe Bool)]
ps <- case Key -> Object -> Maybe Value
forall {v}. Key -> KeyMap v -> Maybe v
lookupKM Key
"properties" Object
o of
             Just Value
v -> Value -> IO [(SVCompProperty, Maybe Bool)]
getProps Value
v
             Maybe Value
Nothing -> FilePath -> IO [(SVCompProperty, Maybe Bool)]
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO [(SVCompProperty, Maybe Bool)])
-> FilePath -> IO [(SVCompProperty, Maybe Bool)]
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"No 'properties' section while parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

     SVCompLanguage
lang <- case Key -> Object -> Maybe Value
forall {v}. Key -> KeyMap v -> Maybe v
lookupKM Key
"options" Object
o of
               Just Value
v -> Value -> IO SVCompLanguage
forall {m :: * -> *}. MonadFail m => Value -> m SVCompLanguage
getLang Value
v
               Maybe Value
Nothing -> FilePath -> IO SVCompLanguage
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO SVCompLanguage) -> FilePath -> IO SVCompLanguage
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"No 'options' section while parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

     return VerificationTask
            { verificationSourceFile :: FilePath
verificationSourceFile = FilePath
fp
            , verificationInputFiles :: [FilePath]
verificationInputFiles = [FilePath]
fs
            , verificationProperties :: [(SVCompProperty, Maybe Bool)]
verificationProperties = [(SVCompProperty, Maybe Bool)]
ps
            , verificationLanguage :: SVCompLanguage
verificationLanguage   = SVCompLanguage
lang
            }
 decodeVT Value
v = FilePath -> IO VerificationTask
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO VerificationTask)
-> FilePath -> IO VerificationTask
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"Expected Yaml object but got:", Value -> FilePath
forall a. Show a => a -> FilePath
show Value
v, FilePath
"when parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]


 decodeProp :: Text -> m SVCompProperty
decodeProp Text
p =
   case Parser SVCompProperty -> Text -> Either FilePath SVCompProperty
forall a. Parser a -> Text -> Either FilePath a
Atto.parseOnly Parser SVCompProperty
propParse Text
p of
     Left FilePath
msg -> FilePath -> m SVCompProperty
forall a. FilePath -> m a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> m SVCompProperty) -> FilePath -> m SVCompProperty
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [ FilePath
"Could not parse property:"
                                , Text -> FilePath
Text.unpack Text
p
                                , FilePath
msg
                                ]

     Right SVCompProperty
p' -> SVCompProperty -> m SVCompProperty
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return SVCompProperty
p'

 getStrs :: Value -> m [FilePath]
getStrs (Yaml.String Text
f) = [FilePath] -> m [FilePath]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Text -> FilePath
Text.unpack Text
f]
 getStrs (Yaml.Array Array
xs) = Vector [FilePath] -> [FilePath]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Vector [FilePath] -> [FilePath])
-> m (Vector [FilePath]) -> m [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> m [FilePath]) -> Array -> m (Vector [FilePath])
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Vector a -> m (Vector b)
V.mapM Value -> m [FilePath]
getStrs Array
xs
 getStrs Value
v = FilePath -> m [FilePath]
forall a. FilePath -> m a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> m [FilePath]) -> FilePath -> m [FilePath]
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"expected strings, but got:", Value -> FilePath
forall a. Show a => a -> FilePath
show Value
v]

 getProp :: Value -> IO (SVCompProperty, Maybe Bool)
getProp (Yaml.Object Object
o) =
   do FilePath
propf <- case Key -> Object -> Maybe Value
forall {v}. Key -> KeyMap v -> Maybe v
lookupKM Key
"property_file" Object
o of
                 Just (Yaml.String Text
f) -> FilePath -> IO FilePath
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> FilePath
Text.unpack Text
f)
                 Maybe Value
_ -> FilePath -> IO FilePath
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"expected string value in 'property_file' while parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

      SVCompProperty
prop <- Text -> IO SVCompProperty
forall {m :: * -> *}. MonadFail m => Text -> m SVCompProperty
decodeProp (Text -> IO SVCompProperty) -> IO Text -> IO SVCompProperty
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> IO Text
Text.readFile (ShowS
takeDirectory FilePath
fp FilePath -> ShowS
</> FilePath
propf)

      Maybe Bool
verdict <- case Key -> Object -> Maybe Value
forall {v}. Key -> KeyMap v -> Maybe v
lookupKM Key
"expected_verdict" Object
o of
                   Maybe Value
Nothing -> Maybe Bool -> IO (Maybe Bool)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
forall a. Maybe a
Nothing
                   Just (Yaml.Bool Bool
b) -> Maybe Bool -> IO (Maybe Bool)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b)
                   Just (Yaml.String Text
"true") -> Maybe Bool -> IO (Maybe Bool)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)
                   Just (Yaml.String Text
"false") -> Maybe Bool -> IO (Maybe Bool)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
                   Just Value
_ -> FilePath -> IO (Maybe Bool)
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO (Maybe Bool)) -> FilePath -> IO (Maybe Bool)
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"expected boolean value in 'expected_verdict' while parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

      return (SVCompProperty
prop, Maybe Bool
verdict)

 getProp Value
_v = FilePath -> IO (SVCompProperty, Maybe Bool)
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO (SVCompProperty, Maybe Bool))
-> FilePath -> IO (SVCompProperty, Maybe Bool)
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"expected object in 'properties' section when parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

 getProps :: Value -> IO [(SVCompProperty, Maybe Bool)]
getProps (Yaml.Array Array
xs) = (Value -> IO (SVCompProperty, Maybe Bool))
-> [Value] -> IO [(SVCompProperty, Maybe Bool)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Value -> IO (SVCompProperty, Maybe Bool)
getProp (Array -> [Value]
forall a. Vector a -> [a]
V.toList Array
xs)
 getProps Value
_v = FilePath -> IO [(SVCompProperty, Maybe Bool)]
forall a. FilePath -> IO a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO [(SVCompProperty, Maybe Bool)])
-> FilePath -> IO [(SVCompProperty, Maybe Bool)]
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"expected property array in 'properties' section when parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

 getLang :: Value -> m SVCompLanguage
getLang (Yaml.Object Object
o) =
   case Key -> Object -> Maybe Value
forall {v}. Key -> KeyMap v -> Maybe v
lookupKM Key
"language" Object
o of
     Just (Yaml.String Text
"C")    -> Object -> m SVCompLanguage
forall {m :: * -> *}. MonadFail m => Object -> m SVCompLanguage
getCDataModel Object
o
     Just (Yaml.String Text
"Java") -> SVCompLanguage -> m SVCompLanguage
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return SVCompLanguage
Java
     Maybe Value
_ -> FilePath -> m SVCompLanguage
forall a. FilePath -> m a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> m SVCompLanguage) -> FilePath -> m SVCompLanguage
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"expected 'C' or 'Java' in 'language' while parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

 getLang Value
_v = FilePath -> m SVCompLanguage
forall a. FilePath -> m a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> m SVCompLanguage) -> FilePath -> m SVCompLanguage
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"expected object in 'options' section when parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

 getCDataModel :: Object -> m SVCompLanguage
getCDataModel Object
o =
   case Key -> Object -> Maybe Value
forall {v}. Key -> KeyMap v -> Maybe v
lookupKM Key
"data_model" Object
o of
     Just (Yaml.String Text
"ILP32") -> SVCompLanguage -> m SVCompLanguage
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CDataModel -> SVCompLanguage
C CDataModel
ILP32)
     Just (Yaml.String Text
"LP64")  -> SVCompLanguage -> m SVCompLanguage
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CDataModel -> SVCompLanguage
C CDataModel
LP64)
     Maybe Value
_ -> FilePath -> m SVCompLanguage
forall a. FilePath -> m a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> m SVCompLanguage) -> FilePath -> m SVCompLanguage
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unwords [FilePath
"expected 'ILP32' or 'LP64' in 'data_model' while parsing", ShowS
forall a. Show a => a -> FilePath
show FilePath
fp]

 -- TODO: When the ecosystem widely uses aeson-2.0.0.0 or later, remove this CPP.
#if MIN_VERSION_aeson(2,0,0)
 lookupKM :: Key -> KeyMap v -> Maybe v
lookupKM = Key -> KeyMap v -> Maybe v
forall {v}. Key -> KeyMap v -> Maybe v
KM.lookup
#else
 lookupKM = HM.lookup
#endif

compilePats :: [Text] -> [Glob.Pattern]
compilePats :: [Text] -> [Pattern]
compilePats [Text]
xs =
  let xs' :: [Text]
xs' = (Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Text -> Bool) -> Text -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
Text.null) ([Text] -> [Text]) -> [Text] -> [Text]
forall a b. (a -> b) -> a -> b
$ (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Text
Text.strip [Text]
xs
   in (Text -> Pattern) -> [Text] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> Pattern
Glob.compile (FilePath -> Pattern) -> (Text -> FilePath) -> Text -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
Text.unpack) [Text]
xs'

loadSVCOMPBenchmarks :: CruxOptions -> IO [BenchmarkSet]
loadSVCOMPBenchmarks :: CruxOptions -> IO [BenchmarkSet]
loadSVCOMPBenchmarks CruxOptions
cruxOpts = (FilePath -> IO BenchmarkSet) -> [FilePath] -> IO [BenchmarkSet]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FilePath -> IO BenchmarkSet
loadBenchmarkSet (CruxOptions -> [FilePath]
inputFiles CruxOptions
cruxOpts)

loadBenchmarkSet :: FilePath -> IO BenchmarkSet
loadBenchmarkSet :: FilePath -> IO BenchmarkSet
loadBenchmarkSet FilePath
fp =
  do let dir :: FilePath
dir  = ShowS
takeDirectory FilePath
fp
         base :: FilePath
base = ShowS
takeBaseName FilePath
fp
         set :: FilePath
set  = FilePath
dir FilePath -> ShowS
</> FilePath
base FilePath -> ShowS
forall a. Semigroup a => a -> a -> a
<> FilePath
".set"

     [Pattern]
pats <- [Text] -> [Pattern]
compilePats ([Text] -> [Pattern]) -> (Text -> [Text]) -> Text -> [Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Text]
Text.lines (Text -> [Pattern]) -> IO Text -> IO [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO Text
Text.readFile FilePath
set
     [FilePath]
fs <- [[FilePath]] -> [FilePath]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[FilePath]] -> [FilePath]) -> IO [[FilePath]] -> IO [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pattern] -> FilePath -> IO [[FilePath]]
Glob.globDir [Pattern]
pats FilePath
dir
     [VerificationTask]
tasks <- (FilePath -> IO VerificationTask)
-> [FilePath] -> IO [VerificationTask]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FilePath -> IO VerificationTask
loadVerificationTask [FilePath]
fs

     return BenchmarkSet
            { benchmarkName :: Text
benchmarkName = FilePath -> Text
Text.pack FilePath
base
            , benchmarkTasks :: [VerificationTask]
benchmarkTasks = [VerificationTask]
tasks
            }


type TaskMap = Map VerificationTask [BenchmarkSet]

-- | There is significant overlap between the various verification tasks found in
--   different benchmark sets in the SV-COMP repository.  This operation collects
--   together all the potentially duplicated tasks found in a collection of benchmark sets
--   and places them in a map, ensuring there is at most one reference to each one.
--   The tasks are the keys of the map; the benchmark set(s) that referenced a given task
--   are stored in the elements the map.
deduplicateTasks :: [BenchmarkSet] -> TaskMap
deduplicateTasks :: [BenchmarkSet] -> TaskMap
deduplicateTasks = ([BenchmarkSet] -> [BenchmarkSet] -> [BenchmarkSet])
-> [TaskMap] -> TaskMap
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith [BenchmarkSet] -> [BenchmarkSet] -> [BenchmarkSet]
forall a. [a] -> [a] -> [a]
(++) ([TaskMap] -> TaskMap)
-> ([BenchmarkSet] -> [TaskMap]) -> [BenchmarkSet] -> TaskMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BenchmarkSet -> TaskMap) -> [BenchmarkSet] -> [TaskMap]
forall a b. (a -> b) -> [a] -> [b]
map BenchmarkSet -> TaskMap
f
  where
  f :: BenchmarkSet -> TaskMap
f BenchmarkSet
bs = [(VerificationTask, [BenchmarkSet])] -> TaskMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
           [ (VerificationTask
t, [BenchmarkSet
bs]) | VerificationTask
t <- BenchmarkSet -> [VerificationTask]
benchmarkTasks BenchmarkSet
bs ]