{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE RankNTypes                 #-}

{-# OPTIONS_GHC -Wall #-}

{-|

This module is responsible for finding annotated program units, and running the
functionality in "Camfort.Specification.Hoare.CheckBackend" on each of them.

-}
module Camfort.Specification.Hoare.CheckFrontend
  (
    -- * Invariant Checking
    invariantChecking

    -- * Analysis Types
  , HoareAnalysis
  , HoareFrontendError(..)
  , HoareFrontendWarning(..)
  ) where

import           Control.Applicative                      (liftA2)
import           Control.Exception
import           Control.Lens
import           Control.Monad.Writer.Lazy                hiding (Product)
import           Data.Generics.Uniplate.Operations
import           Data.Map                                 (Map)
import qualified Data.Map                                 as Map
import           Data.Maybe                               (catMaybes)
import           Data.Void                                (absurd)

import qualified Language.Fortran.Analysis                as F
import qualified Language.Fortran.AST                     as F
import qualified Language.Fortran.Util.Position           as F

import           Camfort.Analysis
import qualified Camfort.Analysis.Annotations             as CA
import           Camfort.Analysis.CommentAnnotator
import           Camfort.Specification.Parser             (SpecParseError)

import           Language.Fortran.Model.Repr.Prim

import           Camfort.Specification.Hoare.Annotation
import           Camfort.Specification.Hoare.CheckBackend
import           Camfort.Specification.Hoare.Parser
import           Camfort.Specification.Hoare.Parser.Types (HoareParseError)
import           Camfort.Specification.Hoare.Syntax

import           Control.DeepSeq

--------------------------------------------------------------------------------
--  Invariant Checking
--------------------------------------------------------------------------------

{-|
Runs invariant checking on every annotated program unit in the given program
file. Expects the program file to have basic block and unique analysis
information.

The 'PrimReprSpec' argument controls how Fortran data types are treated
symbolically. See the documentation in "Language.Fortran.Mode.Repr.Prim" for a
detailed explanation.
-}
invariantChecking :: PrimReprSpec -> F.ProgramFile HA -> HoareAnalysis [HoareCheckResult]
invariantChecking :: PrimReprSpec -> ProgramFile HA -> HoareAnalysis [HoareCheckResult]
invariantChecking PrimReprSpec
primSpec ProgramFile HA
pf = do
  let parserWithAnns :: SpecParser HoareParseError (SpecOrDecl (Analysis Annotation))
parserWithAnns = SpecOrDecl Annotation -> SpecOrDecl (Analysis Annotation)
forall (b :: * -> *) a. Functor b => b a -> b (Analysis a)
F.initAnalysis (SpecOrDecl Annotation -> SpecOrDecl (Analysis Annotation))
-> (SpecOrDecl () -> SpecOrDecl Annotation)
-> SpecOrDecl ()
-> SpecOrDecl (Analysis Annotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> Annotation) -> SpecOrDecl () -> SpecOrDecl Annotation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Annotation -> () -> Annotation
forall a b. a -> b -> a
const Annotation
CA.unitAnnotation) (SpecOrDecl () -> SpecOrDecl (Analysis Annotation))
-> SpecParser HoareParseError (SpecOrDecl ())
-> SpecParser HoareParseError (SpecOrDecl (Analysis Annotation))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecParser HoareParseError (SpecOrDecl ())
hoareParser

  ProgramFile HA
pf' <- SpecParser HoareParseError (SpecOrDecl (Analysis Annotation))
-> (SrcSpan
    -> SpecParseError HoareParseError
    -> AnalysisT HoareFrontendError HoareFrontendWarning IO ())
-> ProgramFile HA
-> AnalysisT
     HoareFrontendError HoareFrontendWarning IO (ProgramFile HA)
forall (m :: * -> *) e a ast.
(Monad m, Data a, Linkable a, ASTEmbeddable a ast) =>
SpecParser e ast
-> (SrcSpan -> SpecParseError e -> m ())
-> ProgramFile a
-> m (ProgramFile a)
annotateComments SpecParser HoareParseError (SpecOrDecl (Analysis Annotation))
parserWithAnns SrcSpan
-> SpecParseError HoareParseError
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
parseError ProgramFile HA
pf
  [AnnotatedProgramUnit]
annotatedPUs <- ProgramFile HA -> HoareAnalysis [AnnotatedProgramUnit]
findAnnotatedPUs ProgramFile HA
pf'

  let checkAndReport :: AnnotatedProgramUnit
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
checkAndReport AnnotatedProgramUnit
apu = do
        let nm :: ProgramUnitName
nm = ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
-> ProgramUnit HA
forall s a. s -> Getting a s a -> a
^. Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
Lens' AnnotatedProgramUnit (ProgramUnit HA)
apuPU)
            prettyName :: Text
prettyName = String -> Text
forall a. Describe a => a -> Text
describe (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ case ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puSrcName (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
-> ProgramUnit HA
forall s a. s -> Getting a s a -> a
^. Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
Lens' AnnotatedProgramUnit (ProgramUnit HA)
apuPU) of
              F.Named String
x -> String
x
              ProgramUnitName
_         -> ProgramUnitName -> String
forall a. Show a => a -> String
show ProgramUnitName
nm
        ProgramUnit HA -> Text -> AnalysisT HoareFrontendError w IO ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> Text -> m ()
logInfo' (AnnotatedProgramUnit
apu AnnotatedProgramUnit
-> Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
-> ProgramUnit HA
forall s a. s -> Getting a s a -> a
^. Getting (ProgramUnit HA) AnnotatedProgramUnit (ProgramUnit HA)
Lens' AnnotatedProgramUnit (ProgramUnit HA)
apuPU) (Text -> AnalysisT HoareFrontendError w IO ())
-> Text -> AnalysisT HoareFrontendError w IO ()
forall a b. (a -> b) -> a -> b
$ Text
"Verifying program unit: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
prettyName
        AnalysisT HoareFrontendError w IO HoareCheckResult
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
forall (m :: * -> *) w e a.
(Monad m, Describe w, Describe e) =>
AnalysisT e w m a -> AnalysisT e w m (Maybe a)
loggingAnalysisError (AnalysisT HoareFrontendError w IO HoareCheckResult
 -> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult))
-> (AnalysisT HoareBackendError Void IO HoareCheckResult
    -> AnalysisT HoareFrontendError w IO HoareCheckResult)
-> AnalysisT HoareBackendError Void IO HoareCheckResult
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HoareBackendError -> HoareFrontendError)
-> (Void -> w)
-> AnalysisT HoareBackendError Void IO HoareCheckResult
-> AnalysisT HoareFrontendError w IO HoareCheckResult
forall (m :: * -> *) e e' w w' a.
Monad m =>
(e -> e') -> (w -> w') -> AnalysisT e w m a -> AnalysisT e' w' m a
mapAnalysisT HoareBackendError -> HoareFrontendError
BackendError Void -> w
forall a. Void -> a
absurd (AnalysisT HoareBackendError Void IO HoareCheckResult
 -> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult))
-> AnalysisT HoareBackendError Void IO HoareCheckResult
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
forall a b. (a -> b) -> a -> b
$ AnnotatedProgramUnit
-> PrimReprSpec
-> AnalysisT HoareBackendError Void IO HoareCheckResult
checkPU AnnotatedProgramUnit
apu PrimReprSpec
primSpec

  [Maybe HoareCheckResult] -> [HoareCheckResult]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe HoareCheckResult] -> [HoareCheckResult])
-> AnalysisT
     HoareFrontendError HoareFrontendWarning IO [Maybe HoareCheckResult]
-> HoareAnalysis [HoareCheckResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AnnotatedProgramUnit
 -> AnalysisT
      HoareFrontendError
      HoareFrontendWarning
      IO
      (Maybe HoareCheckResult))
-> [AnnotatedProgramUnit]
-> AnalysisT
     HoareFrontendError HoareFrontendWarning IO [Maybe HoareCheckResult]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse AnnotatedProgramUnit
-> AnalysisT
     HoareFrontendError HoareFrontendWarning IO (Maybe HoareCheckResult)
forall w.
Describe w =>
AnnotatedProgramUnit
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
checkAndReport [AnnotatedProgramUnit]
annotatedPUs

--------------------------------------------------------------------------------
--  Results and errors
--------------------------------------------------------------------------------

type HoareAnalysis = AnalysisT HoareFrontendError HoareFrontendWarning IO

data HoareFrontendError
  = ParseError (SpecParseError HoareParseError)
  | InvalidPUConditions F.ProgramUnitName [SpecOrDecl InnerHA]
  | BackendError HoareBackendError

instance NFData HoareFrontendError where
  rnf :: HoareFrontendError -> ()
rnf HoareFrontendError
_ = ()

data HoareFrontendWarning
  = OrphanDecls F.ProgramUnitName

instance NFData HoareFrontendWarning where
  rnf :: HoareFrontendWarning -> ()
rnf HoareFrontendWarning
_ = ()

instance Describe HoareFrontendError where
  describeBuilder :: HoareFrontendError -> Builder
describeBuilder = \case
    ParseError SpecParseError HoareParseError
spe -> Builder
"parse error: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (SpecParseError HoareParseError -> String
forall e. Exception e => e -> String
displayException SpecParseError HoareParseError
spe)
    InvalidPUConditions ProgramUnitName
nm [SpecOrDecl (Analysis Annotation)]
conds ->
      Builder
"invalid specification types attached to PU with name " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (ProgramUnitName -> String
forall a. Show a => a -> String
show ProgramUnitName
nm) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
": " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
      String -> Builder
forall a. Describe a => a -> Builder
describeBuilder ([SpecOrDecl (Analysis Annotation)] -> String
forall a. Show a => a -> String
show [SpecOrDecl (Analysis Annotation)]
conds)
    BackendError HoareBackendError
e -> HoareBackendError -> Builder
forall a. Describe a => a -> Builder
describeBuilder HoareBackendError
e

instance Describe HoareFrontendWarning where
  describeBuilder :: HoareFrontendWarning -> Builder
describeBuilder = \case
    OrphanDecls ProgramUnitName
nm ->
      Builder
"auxiliary variable declared for a program unit with no annotations with name " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>
      String -> Builder
forall a. Describe a => a -> Builder
describeBuilder (ProgramUnitName -> String
forall a. Show a => a -> String
show ProgramUnitName
nm) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"; skipping invariant checking for this program unit"

--------------------------------------------------------------------------------
--  Internal
--------------------------------------------------------------------------------

parseError :: F.SrcSpan -> SpecParseError HoareParseError -> HoareAnalysis ()
parseError :: SrcSpan
-> SpecParseError HoareParseError
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
parseError SrcSpan
sp SpecParseError HoareParseError
err = SrcSpan
-> HoareFrontendError
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> e -> m ()
logError' SrcSpan
sp (SpecParseError HoareParseError -> HoareFrontendError
ParseError SpecParseError HoareParseError
err)

-- | Finds all annotated program units in the given program file. Throws errors
-- for program units that are incorrectly annotated. Returns a list of program
-- units which are correctly annotated at the top level.
findAnnotatedPUs :: F.ProgramFile HA -> HoareAnalysis [AnnotatedProgramUnit]
findAnnotatedPUs :: ProgramFile HA -> HoareAnalysis [AnnotatedProgramUnit]
findAnnotatedPUs ProgramFile HA
pf =
  let pusByName :: Map F.ProgramUnitName (F.ProgramUnit HA)
      pusByName :: Map ProgramUnitName (ProgramUnit HA)
pusByName = [(ProgramUnitName, ProgramUnit HA)]
-> Map ProgramUnitName (ProgramUnit HA)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName ProgramUnit HA
pu, ProgramUnit HA
pu) | ProgramUnit HA
pu <- ProgramFile HA -> [ProgramUnit HA]
forall from to. Biplate from to => from -> [to]
universeBi ProgramFile HA
pf]

      -- Each annotation may get linked with one program unit. However, for this
      -- analysis we want to collect all of the annotations that are associated
      -- with the same program unit. For this we need to do some extra work
      -- because the comment annotator can't directly deal with this situation.
      sodsByPU :: Map F.ProgramUnitName [SpecOrDecl InnerHA]
      sodsByPU :: Map ProgramUnitName [SpecOrDecl (Analysis Annotation)]
sodsByPU = ([SpecOrDecl (Analysis Annotation)]
 -> [SpecOrDecl (Analysis Annotation)]
 -> [SpecOrDecl (Analysis Annotation)])
-> [(ProgramUnitName, [SpecOrDecl (Analysis Annotation)])]
-> Map ProgramUnitName [SpecOrDecl (Analysis Annotation)]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [SpecOrDecl (Analysis Annotation)]
-> [SpecOrDecl (Analysis Annotation)]
-> [SpecOrDecl (Analysis Annotation)]
forall a. [a] -> [a] -> [a]
(++)
        [ (ProgramUnitName
nm, [SpecOrDecl (Analysis Annotation)
sod])
        | HA
ann <- ProgramFile HA -> [HA]
forall from to. Biplate from to => from -> [to]
universeBi ProgramFile HA
pf :: [HA]
        , ProgramUnitName
nm  <- HA -> HoareAnnotation Annotation
forall a. Analysis a -> a
F.prevAnnotation HA
ann HoareAnnotation Annotation
-> Getting
     (Endo [ProgramUnitName])
     (HoareAnnotation Annotation)
     ProgramUnitName
-> [ProgramUnitName]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (Maybe ProgramUnitName
 -> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName))
-> HoareAnnotation Annotation
-> Const (Endo [ProgramUnitName]) (HoareAnnotation Annotation)
forall a. Lens' (HoareAnnotation a) (Maybe ProgramUnitName)
hoarePUName ((Maybe ProgramUnitName
  -> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName))
 -> HoareAnnotation Annotation
 -> Const (Endo [ProgramUnitName]) (HoareAnnotation Annotation))
-> ((ProgramUnitName
     -> Const (Endo [ProgramUnitName]) ProgramUnitName)
    -> Maybe ProgramUnitName
    -> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName))
-> Getting
     (Endo [ProgramUnitName])
     (HoareAnnotation Annotation)
     ProgramUnitName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProgramUnitName -> Const (Endo [ProgramUnitName]) ProgramUnitName)
-> Maybe ProgramUnitName
-> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName)
forall a b. Prism (Maybe a) (Maybe b) a b
_Just
        , SpecOrDecl (Analysis Annotation)
sod <- HA -> HoareAnnotation Annotation
forall a. Analysis a -> a
F.prevAnnotation HA
ann HoareAnnotation Annotation
-> Getting
     (Endo [SpecOrDecl (Analysis Annotation)])
     (HoareAnnotation Annotation)
     (SpecOrDecl (Analysis Annotation))
-> [SpecOrDecl (Analysis Annotation)]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (Maybe (SpecOrDecl (Analysis Annotation))
 -> Const
      (Endo [SpecOrDecl (Analysis Annotation)])
      (Maybe (SpecOrDecl (Analysis Annotation))))
-> HoareAnnotation Annotation
-> Const
     (Endo [SpecOrDecl (Analysis Annotation)])
     (HoareAnnotation Annotation)
forall a.
Lens'
  (HoareAnnotation a) (Maybe (SpecOrDecl (Analysis Annotation)))
hoareSod    ((Maybe (SpecOrDecl (Analysis Annotation))
  -> Const
       (Endo [SpecOrDecl (Analysis Annotation)])
       (Maybe (SpecOrDecl (Analysis Annotation))))
 -> HoareAnnotation Annotation
 -> Const
      (Endo [SpecOrDecl (Analysis Annotation)])
      (HoareAnnotation Annotation))
-> ((SpecOrDecl (Analysis Annotation)
     -> Const
          (Endo [SpecOrDecl (Analysis Annotation)])
          (SpecOrDecl (Analysis Annotation)))
    -> Maybe (SpecOrDecl (Analysis Annotation))
    -> Const
         (Endo [SpecOrDecl (Analysis Annotation)])
         (Maybe (SpecOrDecl (Analysis Annotation))))
-> Getting
     (Endo [SpecOrDecl (Analysis Annotation)])
     (HoareAnnotation Annotation)
     (SpecOrDecl (Analysis Annotation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecOrDecl (Analysis Annotation)
 -> Const
      (Endo [SpecOrDecl (Analysis Annotation)])
      (SpecOrDecl (Analysis Annotation)))
-> Maybe (SpecOrDecl (Analysis Annotation))
-> Const
     (Endo [SpecOrDecl (Analysis Annotation)])
     (Maybe (SpecOrDecl (Analysis Annotation)))
forall a b. Prism (Maybe a) (Maybe b) a b
_Just
        ]

      -- For a given program unit and list of associated specifications, create
      -- an annotated program unit, and report an error if something is wrong.
      collectUnit
        :: F.ProgramUnit HA -> [SpecOrDecl InnerHA]
        -> HoareAnalysis (Maybe AnnotatedProgramUnit)
      collectUnit :: ProgramUnit HA
-> [SpecOrDecl (Analysis Annotation)]
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
collectUnit ProgramUnit HA
pu [SpecOrDecl (Analysis Annotation)]
sods = do
        let pres :: [PrimFormula (Analysis Annotation)]
pres  = [SpecOrDecl (Analysis Annotation)]
sods [SpecOrDecl (Analysis Annotation)]
-> Getting
     (Endo [PrimFormula (Analysis Annotation)])
     [SpecOrDecl (Analysis Annotation)]
     (PrimFormula (Analysis Annotation))
-> [PrimFormula (Analysis Annotation)]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (SpecOrDecl (Analysis Annotation)
 -> Const
      (Endo [PrimFormula (Analysis Annotation)])
      (SpecOrDecl (Analysis Annotation)))
-> [SpecOrDecl (Analysis Annotation)]
-> Const
     (Endo [PrimFormula (Analysis Annotation)])
     [SpecOrDecl (Analysis Annotation)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((SpecOrDecl (Analysis Annotation)
  -> Const
       (Endo [PrimFormula (Analysis Annotation)])
       (SpecOrDecl (Analysis Annotation)))
 -> [SpecOrDecl (Analysis Annotation)]
 -> Const
      (Endo [PrimFormula (Analysis Annotation)])
      [SpecOrDecl (Analysis Annotation)])
-> ((PrimFormula (Analysis Annotation)
     -> Const
          (Endo [PrimFormula (Analysis Annotation)])
          (PrimFormula (Analysis Annotation)))
    -> SpecOrDecl (Analysis Annotation)
    -> Const
         (Endo [PrimFormula (Analysis Annotation)])
         (SpecOrDecl (Analysis Annotation)))
-> Getting
     (Endo [PrimFormula (Analysis Annotation)])
     [SpecOrDecl (Analysis Annotation)]
     (PrimFormula (Analysis Annotation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimSpec (Analysis Annotation)
 -> Const
      (Endo [PrimFormula (Analysis Annotation)])
      (PrimSpec (Analysis Annotation)))
-> SpecOrDecl (Analysis Annotation)
-> Const
     (Endo [PrimFormula (Analysis Annotation)])
     (SpecOrDecl (Analysis Annotation))
forall ann. Prism' (SpecOrDecl ann) (PrimSpec ann)
_SodSpec ((PrimSpec (Analysis Annotation)
  -> Const
       (Endo [PrimFormula (Analysis Annotation)])
       (PrimSpec (Analysis Annotation)))
 -> SpecOrDecl (Analysis Annotation)
 -> Const
      (Endo [PrimFormula (Analysis Annotation)])
      (SpecOrDecl (Analysis Annotation)))
-> ((PrimFormula (Analysis Annotation)
     -> Const
          (Endo [PrimFormula (Analysis Annotation)])
          (PrimFormula (Analysis Annotation)))
    -> PrimSpec (Analysis Annotation)
    -> Const
         (Endo [PrimFormula (Analysis Annotation)])
         (PrimSpec (Analysis Annotation)))
-> (PrimFormula (Analysis Annotation)
    -> Const
         (Endo [PrimFormula (Analysis Annotation)])
         (PrimFormula (Analysis Annotation)))
-> SpecOrDecl (Analysis Annotation)
-> Const
     (Endo [PrimFormula (Analysis Annotation)])
     (SpecOrDecl (Analysis Annotation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula (Analysis Annotation)
 -> Const
      (Endo [PrimFormula (Analysis Annotation)])
      (PrimFormula (Analysis Annotation)))
-> PrimSpec (Analysis Annotation)
-> Const
     (Endo [PrimFormula (Analysis Annotation)])
     (PrimSpec (Analysis Annotation))
forall a. Prism' (Specification a) a
_SpecPre
            posts :: [PrimFormula (Analysis Annotation)]
posts = [SpecOrDecl (Analysis Annotation)]
sods [SpecOrDecl (Analysis Annotation)]
-> Getting
     (Endo [PrimFormula (Analysis Annotation)])
     [SpecOrDecl (Analysis Annotation)]
     (PrimFormula (Analysis Annotation))
-> [PrimFormula (Analysis Annotation)]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (SpecOrDecl (Analysis Annotation)
 -> Const
      (Endo [PrimFormula (Analysis Annotation)])
      (SpecOrDecl (Analysis Annotation)))
-> [SpecOrDecl (Analysis Annotation)]
-> Const
     (Endo [PrimFormula (Analysis Annotation)])
     [SpecOrDecl (Analysis Annotation)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((SpecOrDecl (Analysis Annotation)
  -> Const
       (Endo [PrimFormula (Analysis Annotation)])
       (SpecOrDecl (Analysis Annotation)))
 -> [SpecOrDecl (Analysis Annotation)]
 -> Const
      (Endo [PrimFormula (Analysis Annotation)])
      [SpecOrDecl (Analysis Annotation)])
-> ((PrimFormula (Analysis Annotation)
     -> Const
          (Endo [PrimFormula (Analysis Annotation)])
          (PrimFormula (Analysis Annotation)))
    -> SpecOrDecl (Analysis Annotation)
    -> Const
         (Endo [PrimFormula (Analysis Annotation)])
         (SpecOrDecl (Analysis Annotation)))
-> Getting
     (Endo [PrimFormula (Analysis Annotation)])
     [SpecOrDecl (Analysis Annotation)]
     (PrimFormula (Analysis Annotation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimSpec (Analysis Annotation)
 -> Const
      (Endo [PrimFormula (Analysis Annotation)])
      (PrimSpec (Analysis Annotation)))
-> SpecOrDecl (Analysis Annotation)
-> Const
     (Endo [PrimFormula (Analysis Annotation)])
     (SpecOrDecl (Analysis Annotation))
forall ann. Prism' (SpecOrDecl ann) (PrimSpec ann)
_SodSpec ((PrimSpec (Analysis Annotation)
  -> Const
       (Endo [PrimFormula (Analysis Annotation)])
       (PrimSpec (Analysis Annotation)))
 -> SpecOrDecl (Analysis Annotation)
 -> Const
      (Endo [PrimFormula (Analysis Annotation)])
      (SpecOrDecl (Analysis Annotation)))
-> ((PrimFormula (Analysis Annotation)
     -> Const
          (Endo [PrimFormula (Analysis Annotation)])
          (PrimFormula (Analysis Annotation)))
    -> PrimSpec (Analysis Annotation)
    -> Const
         (Endo [PrimFormula (Analysis Annotation)])
         (PrimSpec (Analysis Annotation)))
-> (PrimFormula (Analysis Annotation)
    -> Const
         (Endo [PrimFormula (Analysis Annotation)])
         (PrimFormula (Analysis Annotation)))
-> SpecOrDecl (Analysis Annotation)
-> Const
     (Endo [PrimFormula (Analysis Annotation)])
     (SpecOrDecl (Analysis Annotation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula (Analysis Annotation)
 -> Const
      (Endo [PrimFormula (Analysis Annotation)])
      (PrimFormula (Analysis Annotation)))
-> PrimSpec (Analysis Annotation)
-> Const
     (Endo [PrimFormula (Analysis Annotation)])
     (PrimSpec (Analysis Annotation))
forall a. Prism' (Specification a) a
_SpecPost
            decls :: [AuxDecl (Analysis Annotation)]
decls = [SpecOrDecl (Analysis Annotation)]
sods [SpecOrDecl (Analysis Annotation)]
-> Getting
     (Endo [AuxDecl (Analysis Annotation)])
     [SpecOrDecl (Analysis Annotation)]
     (AuxDecl (Analysis Annotation))
-> [AuxDecl (Analysis Annotation)]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (SpecOrDecl (Analysis Annotation)
 -> Const
      (Endo [AuxDecl (Analysis Annotation)])
      (SpecOrDecl (Analysis Annotation)))
-> [SpecOrDecl (Analysis Annotation)]
-> Const
     (Endo [AuxDecl (Analysis Annotation)])
     [SpecOrDecl (Analysis Annotation)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((SpecOrDecl (Analysis Annotation)
  -> Const
       (Endo [AuxDecl (Analysis Annotation)])
       (SpecOrDecl (Analysis Annotation)))
 -> [SpecOrDecl (Analysis Annotation)]
 -> Const
      (Endo [AuxDecl (Analysis Annotation)])
      [SpecOrDecl (Analysis Annotation)])
-> ((AuxDecl (Analysis Annotation)
     -> Const
          (Endo [AuxDecl (Analysis Annotation)])
          (AuxDecl (Analysis Annotation)))
    -> SpecOrDecl (Analysis Annotation)
    -> Const
         (Endo [AuxDecl (Analysis Annotation)])
         (SpecOrDecl (Analysis Annotation)))
-> Getting
     (Endo [AuxDecl (Analysis Annotation)])
     [SpecOrDecl (Analysis Annotation)]
     (AuxDecl (Analysis Annotation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AuxDecl (Analysis Annotation)
 -> Const
      (Endo [AuxDecl (Analysis Annotation)])
      (AuxDecl (Analysis Annotation)))
-> SpecOrDecl (Analysis Annotation)
-> Const
     (Endo [AuxDecl (Analysis Annotation)])
     (SpecOrDecl (Analysis Annotation))
forall ann. Prism' (SpecOrDecl ann) (AuxDecl ann)
_SodDecl

            errors :: [SpecOrDecl (Analysis Annotation)]
errors = (SpecOrDecl (Analysis Annotation) -> Bool)
-> [SpecOrDecl (Analysis Annotation)]
-> [SpecOrDecl (Analysis Annotation)]
forall a. (a -> Bool) -> [a] -> [a]
filter (APrism
  (SpecOrDecl (Analysis Annotation))
  (SpecOrDecl (Analysis Annotation))
  (PrimFormula (Analysis Annotation))
  (PrimFormula (Analysis Annotation))
-> SpecOrDecl (Analysis Annotation) -> Bool
forall s t a b. APrism s t a b -> s -> Bool
isn't (Market
  (PrimFormula (Analysis Annotation))
  (PrimFormula (Analysis Annotation))
  (PrimSpec (Analysis Annotation))
  (Identity (PrimSpec (Analysis Annotation)))
-> Market
     (PrimFormula (Analysis Annotation))
     (PrimFormula (Analysis Annotation))
     (SpecOrDecl (Analysis Annotation))
     (Identity (SpecOrDecl (Analysis Annotation)))
forall ann. Prism' (SpecOrDecl ann) (PrimSpec ann)
_SodSpec (Market
   (PrimFormula (Analysis Annotation))
   (PrimFormula (Analysis Annotation))
   (PrimSpec (Analysis Annotation))
   (Identity (PrimSpec (Analysis Annotation)))
 -> Market
      (PrimFormula (Analysis Annotation))
      (PrimFormula (Analysis Annotation))
      (SpecOrDecl (Analysis Annotation))
      (Identity (SpecOrDecl (Analysis Annotation))))
-> (Market
      (PrimFormula (Analysis Annotation))
      (PrimFormula (Analysis Annotation))
      (PrimFormula (Analysis Annotation))
      (Identity (PrimFormula (Analysis Annotation)))
    -> Market
         (PrimFormula (Analysis Annotation))
         (PrimFormula (Analysis Annotation))
         (PrimSpec (Analysis Annotation))
         (Identity (PrimSpec (Analysis Annotation))))
-> APrism
     (SpecOrDecl (Analysis Annotation))
     (SpecOrDecl (Analysis Annotation))
     (PrimFormula (Analysis Annotation))
     (PrimFormula (Analysis Annotation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Market
  (PrimFormula (Analysis Annotation))
  (PrimFormula (Analysis Annotation))
  (PrimFormula (Analysis Annotation))
  (Identity (PrimFormula (Analysis Annotation)))
-> Market
     (PrimFormula (Analysis Annotation))
     (PrimFormula (Analysis Annotation))
     (PrimSpec (Analysis Annotation))
     (Identity (PrimSpec (Analysis Annotation)))
forall a. Prism' (Specification a) a
_SpecPre ) (SpecOrDecl (Analysis Annotation) -> Bool)
-> (SpecOrDecl (Analysis Annotation) -> Bool)
-> SpecOrDecl (Analysis Annotation)
-> Bool
.&&
                             APrism
  (SpecOrDecl (Analysis Annotation))
  (SpecOrDecl (Analysis Annotation))
  (PrimFormula (Analysis Annotation))
  (PrimFormula (Analysis Annotation))
-> SpecOrDecl (Analysis Annotation) -> Bool
forall s t a b. APrism s t a b -> s -> Bool
isn't (Market
  (PrimFormula (Analysis Annotation))
  (PrimFormula (Analysis Annotation))
  (PrimSpec (Analysis Annotation))
  (Identity (PrimSpec (Analysis Annotation)))
-> Market
     (PrimFormula (Analysis Annotation))
     (PrimFormula (Analysis Annotation))
     (SpecOrDecl (Analysis Annotation))
     (Identity (SpecOrDecl (Analysis Annotation)))
forall ann. Prism' (SpecOrDecl ann) (PrimSpec ann)
_SodSpec (Market
   (PrimFormula (Analysis Annotation))
   (PrimFormula (Analysis Annotation))
   (PrimSpec (Analysis Annotation))
   (Identity (PrimSpec (Analysis Annotation)))
 -> Market
      (PrimFormula (Analysis Annotation))
      (PrimFormula (Analysis Annotation))
      (SpecOrDecl (Analysis Annotation))
      (Identity (SpecOrDecl (Analysis Annotation))))
-> (Market
      (PrimFormula (Analysis Annotation))
      (PrimFormula (Analysis Annotation))
      (PrimFormula (Analysis Annotation))
      (Identity (PrimFormula (Analysis Annotation)))
    -> Market
         (PrimFormula (Analysis Annotation))
         (PrimFormula (Analysis Annotation))
         (PrimSpec (Analysis Annotation))
         (Identity (PrimSpec (Analysis Annotation))))
-> APrism
     (SpecOrDecl (Analysis Annotation))
     (SpecOrDecl (Analysis Annotation))
     (PrimFormula (Analysis Annotation))
     (PrimFormula (Analysis Annotation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Market
  (PrimFormula (Analysis Annotation))
  (PrimFormula (Analysis Annotation))
  (PrimFormula (Analysis Annotation))
  (Identity (PrimFormula (Analysis Annotation)))
-> Market
     (PrimFormula (Analysis Annotation))
     (PrimFormula (Analysis Annotation))
     (PrimSpec (Analysis Annotation))
     (Identity (PrimSpec (Analysis Annotation)))
forall a. Prism' (Specification a) a
_SpecPost) (SpecOrDecl (Analysis Annotation) -> Bool)
-> (SpecOrDecl (Analysis Annotation) -> Bool)
-> SpecOrDecl (Analysis Annotation)
-> Bool
.&&
                             APrism
  (SpecOrDecl (Analysis Annotation))
  (SpecOrDecl (Analysis Annotation))
  (AuxDecl (Analysis Annotation))
  (AuxDecl (Analysis Annotation))
-> SpecOrDecl (Analysis Annotation) -> Bool
forall s t a b. APrism s t a b -> s -> Bool
isn't APrism
  (SpecOrDecl (Analysis Annotation))
  (SpecOrDecl (Analysis Annotation))
  (AuxDecl (Analysis Annotation))
  (AuxDecl (Analysis Annotation))
forall ann. Prism' (SpecOrDecl ann) (AuxDecl ann)
_SodDecl)
                     [SpecOrDecl (Analysis Annotation)]
sods
              where .&& :: (SpecOrDecl (Analysis Annotation) -> Bool)
-> (SpecOrDecl (Analysis Annotation) -> Bool)
-> SpecOrDecl (Analysis Annotation)
-> Bool
(.&&) = (Bool -> Bool -> Bool)
-> (SpecOrDecl (Analysis Annotation) -> Bool)
-> (SpecOrDecl (Analysis Annotation) -> Bool)
-> SpecOrDecl (Analysis Annotation)
-> Bool
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&)

            result :: AnnotatedProgramUnit
result = [PrimFormula (Analysis Annotation)]
-> [PrimFormula (Analysis Annotation)]
-> [AuxDecl (Analysis Annotation)]
-> ProgramUnit HA
-> AnnotatedProgramUnit
AnnotatedProgramUnit [PrimFormula (Analysis Annotation)]
pres [PrimFormula (Analysis Annotation)]
posts [AuxDecl (Analysis Annotation)]
decls ProgramUnit HA
pu

        Bool
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([SpecOrDecl (Analysis Annotation)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SpecOrDecl (Analysis Annotation)]
errors) (AnalysisT HoareFrontendError HoareFrontendWarning IO ()
 -> AnalysisT HoareFrontendError HoareFrontendWarning IO ())
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall a b. (a -> b) -> a -> b
$ ProgramUnit HA
-> HoareFrontendError
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> e -> m ()
logError' ProgramUnit HA
pu (ProgramUnitName
-> [SpecOrDecl (Analysis Annotation)] -> HoareFrontendError
InvalidPUConditions (ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName ProgramUnit HA
pu) [SpecOrDecl (Analysis Annotation)]
errors)

        if [PrimFormula (Analysis Annotation)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PrimFormula (Analysis Annotation)]
pres Bool -> Bool -> Bool
&& [PrimFormula (Analysis Annotation)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PrimFormula (Analysis Annotation)]
posts
          then do
            Bool
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([AuxDecl (Analysis Annotation)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AuxDecl (Analysis Annotation)]
decls) (AnalysisT HoareFrontendError HoareFrontendWarning IO ()
 -> AnalysisT HoareFrontendError HoareFrontendWarning IO ())
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall a b. (a -> b) -> a -> b
$ ProgramUnit HA
-> HoareFrontendWarning
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall e w (m :: * -> *) a.
(MonadLogger e w m, Spanned a) =>
a -> w -> m ()
logWarn' ProgramUnit HA
pu (ProgramUnitName -> HoareFrontendWarning
OrphanDecls (ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName ProgramUnit HA
pu))
            Maybe AnnotatedProgramUnit
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe AnnotatedProgramUnit
forall a. Maybe a
Nothing
          else Maybe AnnotatedProgramUnit
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe AnnotatedProgramUnit
 -> HoareAnalysis (Maybe AnnotatedProgramUnit))
-> Maybe AnnotatedProgramUnit
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
forall a b. (a -> b) -> a -> b
$ AnnotatedProgramUnit -> Maybe AnnotatedProgramUnit
forall a. a -> Maybe a
Just AnnotatedProgramUnit
result

      apus :: [HoareAnalysis (Maybe AnnotatedProgramUnit)]
      apus :: [HoareAnalysis (Maybe AnnotatedProgramUnit)]
apus = ((ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))
 -> HoareAnalysis (Maybe AnnotatedProgramUnit))
-> [(ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))]
-> [HoareAnalysis (Maybe AnnotatedProgramUnit)]
forall a b. (a -> b) -> [a] -> [b]
map (ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
forall a b. (a, b) -> b
snd ([(ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))]
 -> [HoareAnalysis (Maybe AnnotatedProgramUnit)])
-> (Map
      ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
    -> [(ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))])
-> Map ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
-> [HoareAnalysis (Maybe AnnotatedProgramUnit)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
-> [(ProgramUnitName, HoareAnalysis (Maybe AnnotatedProgramUnit))]
forall k a. Map k a -> [(k, a)]
Map.toList (Map ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
 -> [HoareAnalysis (Maybe AnnotatedProgramUnit)])
-> Map ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
-> [HoareAnalysis (Maybe AnnotatedProgramUnit)]
forall a b. (a -> b) -> a -> b
$ (ProgramUnit HA
 -> [SpecOrDecl (Analysis Annotation)]
 -> HoareAnalysis (Maybe AnnotatedProgramUnit))
-> Map ProgramUnitName (ProgramUnit HA)
-> Map ProgramUnitName [SpecOrDecl (Analysis Annotation)]
-> Map ProgramUnitName (HoareAnalysis (Maybe AnnotatedProgramUnit))
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith ProgramUnit HA
-> [SpecOrDecl (Analysis Annotation)]
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
collectUnit Map ProgramUnitName (ProgramUnit HA)
pusByName Map ProgramUnitName [SpecOrDecl (Analysis Annotation)]
sodsByPU

  in [Maybe AnnotatedProgramUnit] -> [AnnotatedProgramUnit]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe AnnotatedProgramUnit] -> [AnnotatedProgramUnit])
-> AnalysisT
     HoareFrontendError
     HoareFrontendWarning
     IO
     [Maybe AnnotatedProgramUnit]
-> HoareAnalysis [AnnotatedProgramUnit]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HoareAnalysis (Maybe AnnotatedProgramUnit)]
-> AnalysisT
     HoareFrontendError
     HoareFrontendWarning
     IO
     [Maybe AnnotatedProgramUnit]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [HoareAnalysis (Maybe AnnotatedProgramUnit)]
apus