{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# OPTIONS_GHC -Wall #-}
module Camfort.Specification.Hoare.CheckFrontend
(
invariantChecking
, 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
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 InnerHA)
parserWithAnns = SpecOrDecl A -> SpecOrDecl InnerHA
forall (b :: * -> *) a. Functor b => b a -> b (Analysis a)
F.initAnalysis (SpecOrDecl A -> SpecOrDecl InnerHA)
-> (SpecOrDecl () -> SpecOrDecl A)
-> SpecOrDecl ()
-> SpecOrDecl InnerHA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> A) -> SpecOrDecl () -> SpecOrDecl A
forall a b. (a -> b) -> SpecOrDecl a -> SpecOrDecl b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (A -> () -> A
forall a b. a -> b -> a
const A
CA.unitAnnotation) (SpecOrDecl () -> SpecOrDecl InnerHA)
-> SpecParser HoareParseError (SpecOrDecl ())
-> SpecParser HoareParseError (SpecOrDecl InnerHA)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecParser HoareParseError (SpecOrDecl ())
hoareParser
ProgramFile HA
pf' <- SpecParser HoareParseError (SpecOrDecl InnerHA)
-> (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 InnerHA)
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 a.
Spanned a =>
a -> 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))
-> (BackendAnalysis HoareCheckResult
-> AnalysisT HoareFrontendError w IO HoareCheckResult)
-> BackendAnalysis HoareCheckResult
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HoareBackendError -> HoareFrontendError)
-> (HoareBackendWarning -> w)
-> BackendAnalysis 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 HoareBackendWarning -> w
forall a. HoareBackendWarning -> a
absurd (BackendAnalysis HoareCheckResult
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult))
-> BackendAnalysis HoareCheckResult
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
forall a b. (a -> b) -> a -> b
$ AnnotatedProgramUnit
-> PrimReprSpec -> BackendAnalysis 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse AnnotatedProgramUnit
-> AnalysisT
HoareFrontendError HoareFrontendWarning IO (Maybe HoareCheckResult)
forall {w}.
Describe w =>
AnnotatedProgramUnit
-> AnalysisT HoareFrontendError w IO (Maybe HoareCheckResult)
checkAndReport [AnnotatedProgramUnit]
annotatedPUs
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 InnerHA]
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 InnerHA] -> String
forall a. Show a => a -> String
show [SpecOrDecl InnerHA]
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"
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 a.
Spanned a =>
a
-> 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)
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]
sodsByPU :: Map F.ProgramUnitName [SpecOrDecl InnerHA]
sodsByPU :: Map ProgramUnitName [SpecOrDecl InnerHA]
sodsByPU = ([SpecOrDecl InnerHA]
-> [SpecOrDecl InnerHA] -> [SpecOrDecl InnerHA])
-> [(ProgramUnitName, [SpecOrDecl InnerHA])]
-> Map ProgramUnitName [SpecOrDecl InnerHA]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [SpecOrDecl InnerHA]
-> [SpecOrDecl InnerHA] -> [SpecOrDecl InnerHA]
forall a. [a] -> [a] -> [a]
(++)
[ (ProgramUnitName
nm, [SpecOrDecl InnerHA
sod])
| HA
ann <- ProgramFile HA -> [HA]
forall from to. Biplate from to => from -> [to]
universeBi ProgramFile HA
pf :: [HA]
, ProgramUnitName
nm <- HA -> HoareAnnotation A
forall a. Analysis a -> a
F.prevAnnotation HA
ann HoareAnnotation A
-> Getting
(Endo [ProgramUnitName]) (HoareAnnotation A) ProgramUnitName
-> [ProgramUnitName]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (Maybe ProgramUnitName
-> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName))
-> HoareAnnotation A
-> Const (Endo [ProgramUnitName]) (HoareAnnotation A)
forall a (f :: * -> *).
Functor f =>
(Maybe ProgramUnitName -> f (Maybe ProgramUnitName))
-> HoareAnnotation a -> f (HoareAnnotation a)
hoarePUName ((Maybe ProgramUnitName
-> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName))
-> HoareAnnotation A
-> Const (Endo [ProgramUnitName]) (HoareAnnotation A))
-> ((ProgramUnitName
-> Const (Endo [ProgramUnitName]) ProgramUnitName)
-> Maybe ProgramUnitName
-> Const (Endo [ProgramUnitName]) (Maybe ProgramUnitName))
-> Getting
(Endo [ProgramUnitName]) (HoareAnnotation A) 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 (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe b))
_Just
, SpecOrDecl InnerHA
sod <- HA -> HoareAnnotation A
forall a. Analysis a -> a
F.prevAnnotation HA
ann HoareAnnotation A
-> Getting
(Endo [SpecOrDecl InnerHA])
(HoareAnnotation A)
(SpecOrDecl InnerHA)
-> [SpecOrDecl InnerHA]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (Maybe (SpecOrDecl InnerHA)
-> Const (Endo [SpecOrDecl InnerHA]) (Maybe (SpecOrDecl InnerHA)))
-> HoareAnnotation A
-> Const (Endo [SpecOrDecl InnerHA]) (HoareAnnotation A)
forall a (f :: * -> *).
Functor f =>
(Maybe (SpecOrDecl InnerHA) -> f (Maybe (SpecOrDecl InnerHA)))
-> HoareAnnotation a -> f (HoareAnnotation a)
hoareSod ((Maybe (SpecOrDecl InnerHA)
-> Const (Endo [SpecOrDecl InnerHA]) (Maybe (SpecOrDecl InnerHA)))
-> HoareAnnotation A
-> Const (Endo [SpecOrDecl InnerHA]) (HoareAnnotation A))
-> ((SpecOrDecl InnerHA
-> Const (Endo [SpecOrDecl InnerHA]) (SpecOrDecl InnerHA))
-> Maybe (SpecOrDecl InnerHA)
-> Const (Endo [SpecOrDecl InnerHA]) (Maybe (SpecOrDecl InnerHA)))
-> Getting
(Endo [SpecOrDecl InnerHA])
(HoareAnnotation A)
(SpecOrDecl InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecOrDecl InnerHA
-> Const (Endo [SpecOrDecl InnerHA]) (SpecOrDecl InnerHA))
-> Maybe (SpecOrDecl InnerHA)
-> Const (Endo [SpecOrDecl InnerHA]) (Maybe (SpecOrDecl InnerHA))
forall a b (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f b) -> p (Maybe a) (f (Maybe b))
_Just
]
collectUnit
:: F.ProgramUnit HA -> [SpecOrDecl InnerHA]
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
collectUnit :: ProgramUnit HA
-> [SpecOrDecl InnerHA]
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
collectUnit ProgramUnit HA
pu [SpecOrDecl InnerHA]
sods = do
let pres :: [PrimFormula InnerHA]
pres = [SpecOrDecl InnerHA]
sods [SpecOrDecl InnerHA]
-> Getting
(Endo [PrimFormula InnerHA])
[SpecOrDecl InnerHA]
(PrimFormula InnerHA)
-> [PrimFormula InnerHA]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> [SpecOrDecl InnerHA]
-> Const (Endo [PrimFormula InnerHA]) [SpecOrDecl InnerHA]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> [SpecOrDecl InnerHA]
-> Const (Endo [PrimFormula InnerHA]) [SpecOrDecl InnerHA])
-> ((PrimFormula InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> Getting
(Endo [PrimFormula InnerHA])
[SpecOrDecl InnerHA]
(PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimSpec InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA)
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (PrimSpec ann) (f (PrimSpec ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodSpec ((PrimSpec InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> ((PrimFormula InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> PrimSpec InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
-> (PrimFormula InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> PrimSpec InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA)
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f a) -> p (Specification a) (f (Specification a))
_SpecPre
posts :: [PrimFormula InnerHA]
posts = [SpecOrDecl InnerHA]
sods [SpecOrDecl InnerHA]
-> Getting
(Endo [PrimFormula InnerHA])
[SpecOrDecl InnerHA]
(PrimFormula InnerHA)
-> [PrimFormula InnerHA]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> [SpecOrDecl InnerHA]
-> Const (Endo [PrimFormula InnerHA]) [SpecOrDecl InnerHA]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> [SpecOrDecl InnerHA]
-> Const (Endo [PrimFormula InnerHA]) [SpecOrDecl InnerHA])
-> ((PrimFormula InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> Getting
(Endo [PrimFormula InnerHA])
[SpecOrDecl InnerHA]
(PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimSpec InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA)
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (PrimSpec ann) (f (PrimSpec ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodSpec ((PrimSpec InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA))
-> ((PrimFormula InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> PrimSpec InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA))
-> (PrimFormula InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [PrimFormula InnerHA]) (SpecOrDecl InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PrimFormula InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimFormula InnerHA))
-> PrimSpec InnerHA
-> Const (Endo [PrimFormula InnerHA]) (PrimSpec InnerHA)
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f a) -> p (Specification a) (f (Specification a))
_SpecPost
decls :: [AuxDecl InnerHA]
decls = [SpecOrDecl InnerHA]
sods [SpecOrDecl InnerHA]
-> Getting
(Endo [AuxDecl InnerHA]) [SpecOrDecl InnerHA] (AuxDecl InnerHA)
-> [AuxDecl InnerHA]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (SpecOrDecl InnerHA
-> Const (Endo [AuxDecl InnerHA]) (SpecOrDecl InnerHA))
-> [SpecOrDecl InnerHA]
-> Const (Endo [AuxDecl InnerHA]) [SpecOrDecl InnerHA]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((SpecOrDecl InnerHA
-> Const (Endo [AuxDecl InnerHA]) (SpecOrDecl InnerHA))
-> [SpecOrDecl InnerHA]
-> Const (Endo [AuxDecl InnerHA]) [SpecOrDecl InnerHA])
-> ((AuxDecl InnerHA
-> Const (Endo [AuxDecl InnerHA]) (AuxDecl InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [AuxDecl InnerHA]) (SpecOrDecl InnerHA))
-> Getting
(Endo [AuxDecl InnerHA]) [SpecOrDecl InnerHA] (AuxDecl InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AuxDecl InnerHA
-> Const (Endo [AuxDecl InnerHA]) (AuxDecl InnerHA))
-> SpecOrDecl InnerHA
-> Const (Endo [AuxDecl InnerHA]) (SpecOrDecl InnerHA)
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (AuxDecl ann) (f (AuxDecl ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodDecl
errors :: [SpecOrDecl InnerHA]
errors = (SpecOrDecl InnerHA -> Bool)
-> [SpecOrDecl InnerHA] -> [SpecOrDecl InnerHA]
forall a. (a -> Bool) -> [a] -> [a]
filter (APrism
(SpecOrDecl InnerHA)
(SpecOrDecl InnerHA)
(PrimFormula InnerHA)
(PrimFormula InnerHA)
-> SpecOrDecl InnerHA -> Bool
forall s t a b. APrism s t a b -> s -> Bool
isn't (Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimSpec InnerHA)
(Identity (PrimSpec InnerHA))
-> Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(SpecOrDecl InnerHA)
(Identity (SpecOrDecl InnerHA))
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (PrimSpec ann) (f (PrimSpec ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodSpec (Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimSpec InnerHA)
(Identity (PrimSpec InnerHA))
-> Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(SpecOrDecl InnerHA)
(Identity (SpecOrDecl InnerHA)))
-> (Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(Identity (PrimFormula InnerHA))
-> Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimSpec InnerHA)
(Identity (PrimSpec InnerHA)))
-> APrism
(SpecOrDecl InnerHA)
(SpecOrDecl InnerHA)
(PrimFormula InnerHA)
(PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(Identity (PrimFormula InnerHA))
-> Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimSpec InnerHA)
(Identity (PrimSpec InnerHA))
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f a) -> p (Specification a) (f (Specification a))
_SpecPre ) (SpecOrDecl InnerHA -> Bool)
-> (SpecOrDecl InnerHA -> Bool) -> SpecOrDecl InnerHA -> Bool
.&&
APrism
(SpecOrDecl InnerHA)
(SpecOrDecl InnerHA)
(PrimFormula InnerHA)
(PrimFormula InnerHA)
-> SpecOrDecl InnerHA -> Bool
forall s t a b. APrism s t a b -> s -> Bool
isn't (Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimSpec InnerHA)
(Identity (PrimSpec InnerHA))
-> Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(SpecOrDecl InnerHA)
(Identity (SpecOrDecl InnerHA))
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (PrimSpec ann) (f (PrimSpec ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodSpec (Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimSpec InnerHA)
(Identity (PrimSpec InnerHA))
-> Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(SpecOrDecl InnerHA)
(Identity (SpecOrDecl InnerHA)))
-> (Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(Identity (PrimFormula InnerHA))
-> Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimSpec InnerHA)
(Identity (PrimSpec InnerHA)))
-> APrism
(SpecOrDecl InnerHA)
(SpecOrDecl InnerHA)
(PrimFormula InnerHA)
(PrimFormula InnerHA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(Identity (PrimFormula InnerHA))
-> Market
(PrimFormula InnerHA)
(PrimFormula InnerHA)
(PrimSpec InnerHA)
(Identity (PrimSpec InnerHA))
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p a (f a) -> p (Specification a) (f (Specification a))
_SpecPost) (SpecOrDecl InnerHA -> Bool)
-> (SpecOrDecl InnerHA -> Bool) -> SpecOrDecl InnerHA -> Bool
.&&
APrism
(SpecOrDecl InnerHA)
(SpecOrDecl InnerHA)
(AuxDecl InnerHA)
(AuxDecl InnerHA)
-> SpecOrDecl InnerHA -> Bool
forall s t a b. APrism s t a b -> s -> Bool
isn't APrism
(SpecOrDecl InnerHA)
(SpecOrDecl InnerHA)
(AuxDecl InnerHA)
(AuxDecl InnerHA)
forall ann (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (AuxDecl ann) (f (AuxDecl ann))
-> p (SpecOrDecl ann) (f (SpecOrDecl ann))
_SodDecl)
[SpecOrDecl InnerHA]
sods
where .&& :: (SpecOrDecl InnerHA -> Bool)
-> (SpecOrDecl InnerHA -> Bool) -> SpecOrDecl InnerHA -> Bool
(.&&) = (Bool -> Bool -> Bool)
-> (SpecOrDecl InnerHA -> Bool)
-> (SpecOrDecl InnerHA -> Bool)
-> SpecOrDecl InnerHA
-> Bool
forall a b c.
(a -> b -> c)
-> (SpecOrDecl InnerHA -> a)
-> (SpecOrDecl InnerHA -> b)
-> SpecOrDecl InnerHA
-> c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&)
result :: AnnotatedProgramUnit
result = [PrimFormula InnerHA]
-> [PrimFormula InnerHA]
-> [AuxDecl InnerHA]
-> ProgramUnit HA
-> AnnotatedProgramUnit
AnnotatedProgramUnit [PrimFormula InnerHA]
pres [PrimFormula InnerHA]
posts [AuxDecl InnerHA]
decls ProgramUnit HA
pu
Bool
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([SpecOrDecl InnerHA] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SpecOrDecl InnerHA]
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 a.
Spanned a =>
a
-> 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 InnerHA] -> HoareFrontendError
InvalidPUConditions (ProgramUnit HA -> ProgramUnitName
forall a. ProgramUnit (Analysis a) -> ProgramUnitName
F.puName ProgramUnit HA
pu) [SpecOrDecl InnerHA]
errors)
if [PrimFormula InnerHA] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PrimFormula InnerHA]
pres Bool -> Bool -> Bool
&& [PrimFormula InnerHA] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PrimFormula InnerHA]
posts
then do
Bool
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
-> AnalysisT HoareFrontendError HoareFrontendWarning IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([AuxDecl InnerHA] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AuxDecl InnerHA]
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 a.
Spanned a =>
a
-> 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 a.
a -> AnalysisT HoareFrontendError HoareFrontendWarning IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe AnnotatedProgramUnit
forall a. Maybe a
Nothing
else Maybe AnnotatedProgramUnit
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
forall a.
a -> AnalysisT HoareFrontendError HoareFrontendWarning IO a
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 InnerHA]
-> HoareAnalysis (Maybe AnnotatedProgramUnit))
-> Map ProgramUnitName (ProgramUnit HA)
-> Map ProgramUnitName [SpecOrDecl InnerHA]
-> 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 InnerHA]
-> HoareAnalysis (Maybe AnnotatedProgramUnit)
collectUnit Map ProgramUnitName (ProgramUnit HA)
pusByName Map ProgramUnitName [SpecOrDecl InnerHA]
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)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [HoareAnalysis (Maybe AnnotatedProgramUnit)]
apus