{- |
Module      :  Camfort.Specification.Units.Analysis.Criticals
Description :  Critical-units analysis.
Copyright   :  (c) 2017, Dominic Orchard, Andrew Rice, Mistral Contrastin, Matthew Danish
License     :  Apache-2.0

Maintainer  :  dom.orchard@gmail.com
Stability   :  experimental

This module defines an analysis for finding the 'critical' variables in a program.
These critical variables form a set of variables that, when given unit annotations,
can be used to infer the unit types of all other variables in the program.
-}

module Camfort.Specification.Units.Analysis.Criticals
  ( inferCriticalVariables
  ) where

import           Camfort.Analysis
import           Camfort.Analysis.Annotations
import           Camfort.Analysis.ModFile (withCombinedModuleMap)
import           Camfort.Specification.Units.Analysis (UnitAnalysis, runInference)
import qualified Camfort.Specification.Units.Annotation as UA
import           Camfort.Specification.Units.Environment
import           Camfort.Specification.Units.InferenceBackendSBV (criticalVariables)
import           Camfort.Specification.Units.Monad
import           Control.DeepSeq
import           Control.Monad.Reader (asks, lift)
import           Control.Monad.State (get)
import           Data.Generics.Uniplate.Operations
import qualified Data.Map.Strict as M
import           Data.Maybe (fromMaybe)
import qualified Language.Fortran.AST as F
import qualified Language.Fortran.Analysis as FA
import           Language.Fortran.Util.ModFile
import qualified Language.Fortran.Util.Position as FU

-- | An inference of variables that must be provided with
-- unit annotations before units for all variables can be
-- resolved.
data Criticals = Criticals
  {
    -- | 'ProgramFile' analysis was performed upon.
    Criticals -> ProgramFile Annotation
criticalsPf           :: F.ProgramFile Annotation
    -- | The inferred critical variables.
  , Criticals -> [UnitInfo]
criticalsVariables    :: [UnitInfo]
    -- | Map of all declarations.
  , Criticals -> Map Name (DeclContext, SrcSpan)
criticalsDeclarations :: M.Map F.Name (DeclContext, FU.SrcSpan)
    -- | Map of unique names.
  , Criticals -> Map Name Name
criticalsUniqMap      :: M.Map F.Name F.Name
    -- | Location of criticals.
  , Criticals -> Map Name Name
criticalsFromWhere    :: M.Map F.Name FilePath
  }

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

instance ExitCodeOfReport Criticals where
  exitCodeOf :: Criticals -> Int
exitCodeOf Criticals
_ = Int
0

instance Show Criticals where
  show :: Criticals -> Name
show Criticals
crits =
    case [UnitInfo]
vars of
      []   -> [Name] -> Name
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Name
"\n", Name
fname, Name
": No additional annotations are necessary.\n"]
      [UnitInfo]
_    -> [Name] -> Name
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Name
"\n", Name
fname, Name
": ", Int -> Name
forall a. Show a => a -> Name
show Int
numVars
                     , Name
" variable declarations suggested to be given a specification:\n"
                     , [Name] -> Name
unlines [ Name
"    " Name -> ShowS
forall a. [a] -> [a] -> [a]
++ (Name, (DeclContext, SrcSpan)) -> Name
forall a. (Name, (a, SrcSpan)) -> Name
declReport (Name, (DeclContext, SrcSpan))
d | (Name, (DeclContext, SrcSpan))
d <- Map Name (DeclContext, SrcSpan) -> [(Name, (DeclContext, SrcSpan))]
forall k a. Map k a -> [(k, a)]
M.toList Map Name (DeclContext, SrcSpan)
dmapSlice ]]
      where
        fname :: Name
fname        = ProgramFile Annotation -> Name
forall a. ProgramFile a -> Name
F.pfGetFilename (ProgramFile Annotation -> Name)
-> (Criticals -> ProgramFile Annotation) -> Criticals -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Criticals -> ProgramFile Annotation
criticalsPf (Criticals -> Name) -> Criticals -> Name
forall a b. (a -> b) -> a -> b
$ Criticals
crits
        dmap :: Map Name (DeclContext, SrcSpan)
dmap         = Criticals -> Map Name (DeclContext, SrcSpan)
criticalsDeclarations           Criticals
crits
        uniqnameMap :: Map Name Name
uniqnameMap  = Criticals -> Map Name Name
criticalsUniqMap                Criticals
crits
        fromWhereMap :: Map Name Name
fromWhereMap = Criticals -> Map Name Name
criticalsFromWhere              Criticals
crits
        vars :: [UnitInfo]
vars         = Criticals -> [UnitInfo]
criticalsVariables              Criticals
crits
        unitVarName :: UnitInfo -> Name
unitVarName (UnitVar (Name
v, Name
_))                 = Name
v
        unitVarName (UnitParamVarUse ((Name, Name)
_, (Name
v, Name
_), Int
_)) = Name
v
        unitVarName UnitInfo
_                                = Name
"<bad>"
        varNames :: [Name]
varNames  = (UnitInfo -> Name) -> [UnitInfo] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map UnitInfo -> Name
unitVarName [UnitInfo]
vars
        dmapSlice :: Map Name (DeclContext, SrcSpan)
dmapSlice = (Name -> (DeclContext, SrcSpan) -> Bool)
-> Map Name (DeclContext, SrcSpan)
-> Map Name (DeclContext, SrcSpan)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\ Name
k (DeclContext, SrcSpan)
_ -> Name
k Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
varNames) Map Name (DeclContext, SrcSpan)
dmap
        numVars :: Int
numVars   = Map Name (DeclContext, SrcSpan) -> Int
forall k a. Map k a -> Int
M.size Map Name (DeclContext, SrcSpan)
dmapSlice
        declReport :: (Name, (a, SrcSpan)) -> Name
declReport (Name
v, (a
_, SrcSpan
ss)) = Name
vfilename Name -> ShowS
forall a. [a] -> [a] -> [a]
++ Name
" (" Name -> ShowS
forall a. [a] -> [a] -> [a]
++ SrcSpan -> Name
showSpanStart SrcSpan
ss Name -> ShowS
forall a. [a] -> [a] -> [a]
++ Name
")    " Name -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> Maybe Name -> Name
forall a. a -> Maybe a -> a
fromMaybe Name
v (Name -> Map Name Name -> Maybe Name
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
v Map Name Name
uniqnameMap)
          where vfilename :: Name
vfilename = Name -> Maybe Name -> Name
forall a. a -> Maybe a -> a
fromMaybe Name
fname (Maybe Name -> Name) -> Maybe Name -> Name
forall a b. (a -> b) -> a -> b
$ Name -> Map Name Name -> Maybe Name
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
v Map Name Name
fromWhereMap
                showSpanStart :: SrcSpan -> Name
showSpanStart (FU.SrcSpan Position
l Position
_) = Position -> Name
forall a. Show a => a -> Name
show Position
l

instance Describe Criticals

-- | Return a list of critical variables as UnitInfo list (most likely
-- to be of the UnitVar constructor).
runCriticalVariables :: UnitSolver [UnitInfo]
runCriticalVariables :: UnitSolver [UnitInfo]
runCriticalVariables = do
  Constraints
cons <- UnitState -> Constraints
usConstraints (UnitState -> Constraints)
-> StateT UnitState UnitAnalysis UnitState
-> StateT UnitState UnitAnalysis Constraints
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` StateT UnitState UnitAnalysis UnitState
forall s (m :: * -> *). MonadState s m => m s
get
  [UnitInfo] -> UnitSolver [UnitInfo]
forall (m :: * -> *) a. Monad m => a -> m a
return ([UnitInfo] -> UnitSolver [UnitInfo])
-> [UnitInfo] -> UnitSolver [UnitInfo]
forall a b. (a -> b) -> a -> b
$ Constraints -> [UnitInfo]
criticalVariables Constraints
cons

-- | Infer one possible set of critical variables for a program.
inferCriticalVariables :: UnitAnalysis Criticals
inferCriticalVariables :: UnitAnalysis Criticals
inferCriticalVariables = do
  ProgramFile Annotation
pf <- (UnitEnv -> ProgramFile Annotation)
-> ReaderT UnitEnv (AnalysisT () () IO) (ProgramFile Annotation)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks UnitEnv -> ProgramFile Annotation
unitProgramFile
  ModFiles
mfs <- AnalysisT () () IO ModFiles
-> ReaderT UnitEnv (AnalysisT () () IO) ModFiles
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift AnalysisT () () IO ModFiles
forall e w (m :: * -> *). MonadAnalysis e w m => m ModFiles
analysisModFiles
  ([UnitInfo]
eVars, UnitState
_) <- UnitSolver [UnitInfo] -> UnitAnalysis ([UnitInfo], UnitState)
forall a. UnitSolver a -> UnitAnalysis (a, UnitState)
runInference UnitSolver [UnitInfo]
runCriticalVariables
  let
    -- Use the module map derived from all of the included Camfort Mod files.
    (ProgramFile (Analysis (UnitAnnotation Annotation))
pfRenamed, ModuleMap
mmap) = ModFiles
-> ProgramFile (Analysis (UnitAnnotation Annotation))
-> (ProgramFile (Analysis (UnitAnnotation Annotation)), ModuleMap)
forall a.
Data a =>
ModFiles
-> ProgramFile (Analysis a)
-> (ProgramFile (Analysis a), ModuleMap)
withCombinedModuleMap ModFiles
mfs (ProgramFile (Analysis (UnitAnnotation Annotation))
 -> (ProgramFile (Analysis (UnitAnnotation Annotation)), ModuleMap))
-> (ProgramFile Annotation
    -> ProgramFile (Analysis (UnitAnnotation Annotation)))
-> ProgramFile Annotation
-> (ProgramFile (Analysis (UnitAnnotation Annotation)), ModuleMap)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProgramFile (UnitAnnotation Annotation)
-> ProgramFile (Analysis (UnitAnnotation Annotation))
forall (b :: * -> *) a. Functor b => b a -> b (Analysis a)
FA.initAnalysis (ProgramFile (UnitAnnotation Annotation)
 -> ProgramFile (Analysis (UnitAnnotation Annotation)))
-> (ProgramFile Annotation
    -> ProgramFile (UnitAnnotation Annotation))
-> ProgramFile Annotation
-> ProgramFile (Analysis (UnitAnnotation Annotation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Annotation -> UnitAnnotation Annotation)
-> ProgramFile Annotation
-> ProgramFile (UnitAnnotation Annotation)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Annotation -> UnitAnnotation Annotation
forall a. a -> UnitAnnotation a
UA.mkUnitAnnotation (ProgramFile Annotation
 -> (ProgramFile (Analysis (UnitAnnotation Annotation)), ModuleMap))
-> ProgramFile Annotation
-> (ProgramFile (Analysis (UnitAnnotation Annotation)), ModuleMap)
forall a b. (a -> b) -> a -> b
$ ProgramFile Annotation
pf
    -- unique name -> src name across modules

    -- Map of all declarations
    dmap :: Map Name (DeclContext, SrcSpan)
dmap = ProgramFile (Analysis (UnitAnnotation Annotation))
-> Map Name (DeclContext, SrcSpan)
forall a.
Data a =>
ProgramFile (Analysis a) -> Map Name (DeclContext, SrcSpan)
extractDeclMap ProgramFile (Analysis (UnitAnnotation Annotation))
pfRenamed Map Name (DeclContext, SrcSpan)
-> Map Name (DeclContext, SrcSpan)
-> Map Name (DeclContext, SrcSpan)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` ModFiles -> Map Name (DeclContext, SrcSpan)
combinedDeclMap ModFiles
mfs
    uniqnameMap :: Map Name Name
uniqnameMap = [(Name, Name)] -> Map Name Name
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [
                (Expression (Analysis (UnitAnnotation Annotation)) -> Name
forall a. Expression (Analysis a) -> Name
FA.varName Expression (Analysis (UnitAnnotation Annotation))
e, Expression (Analysis (UnitAnnotation Annotation)) -> Name
forall a. Expression (Analysis a) -> Name
FA.srcName Expression (Analysis (UnitAnnotation Annotation))
e) |
                e :: Expression (Analysis (UnitAnnotation Annotation))
e@(F.ExpValue Analysis (UnitAnnotation Annotation)
_ SrcSpan
_ F.ValVariable{}) <- ProgramFile (Analysis (UnitAnnotation Annotation))
-> [Expression (Analysis (UnitAnnotation Annotation))]
forall from to. Biplate from to => from -> [to]
universeBi ProgramFile (Analysis (UnitAnnotation Annotation))
pfRenamed :: [F.Expression UA]
                -- going to ignore intrinsics here
              ] Map Name Name -> Map Name Name -> Map Name Name
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` ([Map Name Name] -> Map Name Name
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions ([Map Name Name] -> Map Name Name)
-> ([Map Name (Name, NameType)] -> [Map Name Name])
-> [Map Name (Name, NameType)]
-> Map Name Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Name (Name, NameType) -> Map Name Name)
-> [Map Name (Name, NameType)] -> [Map Name Name]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, Name)] -> Map Name Name
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Name, Name)] -> Map Name Name)
-> (Map Name (Name, NameType) -> [(Name, Name)])
-> Map Name (Name, NameType)
-> Map Name Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, (Name, NameType)) -> (Name, Name))
-> [(Name, (Name, NameType))] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
a, (Name
b, NameType
_)) -> (Name
b, Name
a)) ([(Name, (Name, NameType))] -> [(Name, Name)])
-> (Map Name (Name, NameType) -> [(Name, (Name, NameType))])
-> Map Name (Name, NameType)
-> [(Name, Name)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (Name, NameType) -> [(Name, (Name, NameType))]
forall k a. Map k a -> [(k, a)]
M.toList) ([Map Name (Name, NameType)] -> Map Name Name)
-> [Map Name (Name, NameType)] -> Map Name Name
forall a b. (a -> b) -> a -> b
$ ModuleMap -> [Map Name (Name, NameType)]
forall k a. Map k a -> [a]
M.elems ModuleMap
mmap)
    fromWhereMap :: Map Name Name
fromWhereMap = ModFiles -> Map Name Name
genUniqNameToFilenameMap ModFiles
mfs
  Criticals -> UnitAnalysis Criticals
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Criticals -> UnitAnalysis Criticals)
-> Criticals -> UnitAnalysis Criticals
forall a b. NFData a => (a -> b) -> a -> b
$!! Criticals :: ProgramFile Annotation
-> [UnitInfo]
-> Map Name (DeclContext, SrcSpan)
-> Map Name Name
-> Map Name Name
-> Criticals
Criticals { criticalsPf :: ProgramFile Annotation
criticalsPf           = ProgramFile Annotation
pf
                     , criticalsVariables :: [UnitInfo]
criticalsVariables    = [UnitInfo]
eVars
                     , criticalsDeclarations :: Map Name (DeclContext, SrcSpan)
criticalsDeclarations = Map Name (DeclContext, SrcSpan)
dmap
                     , criticalsUniqMap :: Map Name Name
criticalsUniqMap      = Map Name Name
uniqnameMap
                     , criticalsFromWhere :: Map Name Name
criticalsFromWhere    = Map Name Name
fromWhereMap
                     }