content: -- | 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
    { svcompBlacklist :: [FilePath]
        -- ^ Benchmarks to skip when evaluating in SV-COMP mode
  
    , svcompArch :: f Arch
        -- ^ The architecture assumed for the verification task
  
    , svcompSpec :: f FilePath
        -- ^ The file containing the specification text used to verify the program. Likely a .prp file.
  
    , svcompWitnessOutput :: FilePath
        -- ^ Write the witness automaton to this filename
    }
  
  data Arch = Arch32 | Arch64
    deriving (Show,Eq,Ord)
  
  archSpec :: ValueSpec Arch
  archSpec =
    (Arch32 <$ atomSpec "32bit") <!>
    (Arch64 <$ atomSpec "64bit")
  
  parseArch :: (Arch -> opts -> opts) -> String -> OptSetter opts
  parseArch mk = \txt opts ->
    case txt of
      "32bit" -> Right (mk Arch32 opts)
      "64bit" -> Right (mk Arch64 opts)
      _       -> Left "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{ svcompArch, svcompSpec
                    , svcompBlacklist, svcompWitnessOutput}) = do
    svcompArch' <- process "svcomp-arch" svcompArch
    svcompSpec' <- process "svcomp-spec" svcompSpec
    pure $ SVCOMPOptions{ svcompArch = svcompArch', svcompSpec = svcompSpec'
                        , svcompBlacklist, svcompWitnessOutput }
    where
      process :: String -> Maybe a -> IO (Identity a)
      process optName = maybe (fail $ "A value for --" ++ optName ++ " must be provided") (pure . Identity)
  
  svcompOptions :: Config (SVCOMPOptions Maybe)
  svcompOptions = Config
    { cfgFile =
        do svcompBlacklist <-
             section "svcomp-blacklist" (listSpec stringSpec) []
             "SV-COMP benchmark tasks to skip"
  
           svcompArch <-
             sectionMaybe "svcomp-arch" archSpec
             "The architecture assumed for the verification task."
  
           svcompSpec <-
             sectionMaybe "svcomp-spec" fileSpec
             "The file containing the specification text used to verify the program. Likely a .prp file."
  
           svcompWitnessOutput <-
             section "svcomp-witness-output" fileSpec "witness.graphml"
             (Text.unwords [ "The file name to which the witness automaton file should be written"
                           , "(default: witness.graphml)."
                           ])
  
           return SVCOMPOptions{ .. }
  
    , cfgEnv = []
  
    , cfgCmdLineFlag =
        [ Option [] ["svcomp-arch"]
          "The architecture assumed for the verification task."
          $ ReqArg "`32bit` or `64bit`"
          $ parseArch
          $ \a opts -> opts{ svcompArch = Just a }
  
        , Option [] ["svcomp-spec"]
          "The file containing the specification text used to verify the program. Likely a .prp file."
          $ ReqArg "FILE"
          $ \f opts -> Right opts{ svcompSpec = Just f }
  
        , Option [] ["svcomp-witness-output"]
          (unwords [ "The file name to which the witness automaton file should be written"
                   , "(default: witness.graphml)."
                   ])
          $ ReqArg "FILE"
          $ \f opts -> Right opts{ svcompWitnessOutput = f }
        ]
    }
  
  propertyVerdict :: VerificationTask -> Maybe Bool
  propertyVerdict task = foldl f Nothing (verificationProperties task)
   where
   comb b Nothing  = Just b
   comb b (Just x) = Just $! b && x
  
   f v (CheckNoError _nm, Just b)  = comb b v
   f v (CheckValidFree, Just b)    = comb b v
   f v (CheckValidDeref, Just b)   = comb b v
   f v (CheckDefBehavior, Just b)  = comb b v
   f v (CheckNoOverflow, Just b)   = comb b v
   f v _ = v
  
  data ComputedVerdict
    = Verified
    | Falsified
    | Unknown
   deriving (Eq, Generic, Ord, Show, ToJSON)
  
  data BenchmarkSet =
    BenchmarkSet
    { benchmarkName :: Text
    , benchmarkTasks :: [VerificationTask]
    }
   deriving (Show,Eq,Ord)
  
  data SVCompProperty
    = CheckNoError Text
    | CheckValidFree
    | CheckValidDeref
    | CheckValidMemtrack
    | CheckValidMemCleanup
    | CheckDefBehavior
    | CheckNoOverflow
    | CheckTerminates
    | CoverageFQL Text
   deriving (Show,Eq,Ord,Generic,ToJSON)
  
  data SVCompLanguage
    = C CDataModel
    | Java
   deriving (Show,Eq,Ord)
  
  data CDataModel = ILP32 | LP64
   deriving (Show,Eq,Ord)
  
  data VerificationTask =
    VerificationTask
    { verificationSourceFile :: FilePath
    , verificationInputFiles :: [FilePath]
    , verificationProperties :: [(SVCompProperty, Maybe Bool)]
    , verificationLanguage   :: SVCompLanguage
    }
   deriving (Show,Eq,Ord)
  
  checkParse :: Atto.Parser SVCompProperty
  checkParse = Atto.skipSpace *> Atto.string "init(main())," *> Atto.skipSpace *> ltl
   where
   ltl = Atto.string "LTL(" *> Atto.skipSpace *> go <* Atto.skipSpace <* Atto.string ")" <* Atto.skipSpace
   go = Atto.choice
        [ CheckNoError <$> (Atto.string "G ! call(" *> bracketedText <* ")")
        , pure CheckTerminates      <* Atto.string "F end"
        , pure CheckValidFree       <* Atto.string "G valid-free"
        , pure CheckValidDeref      <* Atto.string "G valid-deref"
        , pure CheckValidMemtrack   <* Atto.string "G valid-memtrack"
        , pure CheckValidMemCleanup <* Atto.string "G valid-memcleanup"
        , pure CheckNoOverflow      <* Atto.string "G ! overflow"
        , pure CheckDefBehavior     <* Atto.string "G def-behavior"
        ]
  
  coverParse :: Atto.Parser SVCompProperty
  coverParse = CoverageFQL <$> (Atto.skipSpace *> Atto.string "init(main())," *> Atto.skipSpace *> bracketedText)
  
  bracketedText :: Atto.Parser Text
  bracketedText =
   do xs <- Atto.takeTill (\x -> x `elem` ['(',')'])
      (do _ <- Atto.char '('
          ys <- bracketedText
          _ <- Atto.char ')'
          zs <- bracketedText
          return (xs <> "(" <> ys <> ")" <> zs)
       ) <|> (return xs)
  
  
  propParse :: Atto.Parser SVCompProperty
  propParse = Atto.skipSpace *> Atto.choice
    [ Atto.string "CHECK(" *> checkParse <* ")"
    , Atto.string "COVER(" *> coverParse <* ")"
    ]
  
  loadVerificationTask :: FilePath -> IO VerificationTask
  loadVerificationTask fp =
     Yaml.decodeFileEither fp >>= \case
       Left err -> fail $ unlines ["Failure parsing YAML file: " ++ show fp, show err]
       Right a  -> decodeVT a
   where
   decodeVT :: Yaml.Value -> IO VerificationTask
   decodeVT (Yaml.Object o) =
    do case lookupKM "format_version" o of
         Just (Yaml.String "2.0") -> return ()
         _ -> fail $ unwords ["Expected verification task version 2.0 while parsing", show fp]
  
       fs <- case lookupKM "input_files" o of
               Just v -> getStrs v
               Nothing -> fail $ unwords ["No 'input_files' section while parsing", show fp]
  
       ps <- case lookupKM "properties" o of
               Just v -> getProps v
               Nothing -> fail $ unwords ["No 'properties' section while parsing", show fp]
  
       lang <- case lookupKM "options" o of
                 Just v -> getLang v
                 Nothing -> fail $ unwords ["No 'options' section while parsing", show fp]
  
       return VerificationTask
              { verificationSourceFile = fp
              , verificationInputFiles = fs
              , verificationProperties = ps
              , verificationLanguage   = lang
              }
   decodeVT v = fail $ unwords ["Expected Yaml object but got:", show v, "when parsing", show fp]
  
  
   decodeProp p =
     case Atto.parseOnly propParse p of
       Left msg -> fail $ unlines [ "Could not parse property:"
                                  , Text.unpack p
                                  , msg
                                  ]
  
       Right p' -> return p'
  
   getStrs (Yaml.String f) = return [Text.unpack f]
   getStrs (Yaml.Array xs) = concat <$> V.mapM getStrs xs
   getStrs v = fail $ unwords ["expected strings, but got:", show v]
  
   getProp (Yaml.Object o) =
     do propf <- case lookupKM "property_file" o of
                   Just (Yaml.String f) -> return (Text.unpack f)
                   _ -> fail $ unwords ["expected string value in 'property_file' while parsing", show fp]
  
        prop <- decodeProp =<< Text.readFile (takeDirectory fp </> propf)
  
        verdict <- case lookupKM "expected_verdict" o of
                     Nothing -> return Nothing
                     Just (Yaml.Bool b) -> return (Just b)
                     Just (Yaml.String "true") -> return (Just True)
                     Just (Yaml.String "false") -> return (Just False)
                     Just _ -> fail $ unwords ["expected boolean value in 'expected_verdict' while parsing", show fp]
  
        return (prop, verdict)
  
   getProp _v = fail $ unwords ["expected object in 'properties' section when parsing", show fp]
  
   getProps (Yaml.Array xs) = mapM getProp (V.toList xs)
   getProps _v = fail $ unwords ["expected property array in 'properties' section when parsing", show fp]
  
   getLang (Yaml.Object o) =
     case lookupKM "language" o of
       Just (Yaml.String "C")    -> getCDataModel o
       Just (Yaml.String "Java") -> return Java
       _ -> fail $ unwords ["expected 'C' or 'Java' in 'language' while parsing", show fp]
  
   getLang _v = fail $ unwords ["expected object in 'options' section when parsing", show fp]
  
   getCDataModel o =
     case lookupKM "data_model" o of
       Just (Yaml.String "ILP32") -> return (C ILP32)
       Just (Yaml.String "LP64")  -> return (C LP64)
       _ -> fail $ unwords ["expected 'ILP32' or 'LP64' in 'data_model' while parsing", show 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 = KM.lookup
  #else
   lookupKM = HM.lookup
  #endif
  
  compilePats :: [Text] -> [Glob.Pattern]
  compilePats xs =
    let xs' = filter (not . Text.null) $ map Text.strip xs
     in map (Glob.compile . Text.unpack) xs'
  
  loadSVCOMPBenchmarks :: CruxOptions -> IO [BenchmarkSet]
  loadSVCOMPBenchmarks cruxOpts = mapM loadBenchmarkSet (inputFiles cruxOpts)
  
  loadBenchmarkSet :: FilePath -> IO BenchmarkSet
  loadBenchmarkSet fp =
    do let dir  = takeDirectory fp
           base = takeBaseName fp
           set  = dir </> base <> ".set"
  
       pats <- compilePats . Text.lines <$> Text.readFile set
       fs <- concat <$> Glob.globDir pats dir
       tasks <- mapM loadVerificationTask fs
  
       return BenchmarkSet
              { benchmarkName = Text.pack base
              , benchmarkTasks = 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 = Map.unionsWith (++) . map f
    where
    f bs = Map.fromList
             [ (t, [bs]) | t <- benchmarkTasks bs ]
  