camfort-1.0: src/Camfort/Specification/Units/Analysis/Criticals.hs
{- |
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.
criticalsPf :: F.ProgramFile Annotation
-- | The inferred critical variables.
, criticalsVariables :: [UnitInfo]
-- | Map of all declarations.
, criticalsDeclarations :: M.Map F.Name (DeclContext, FU.SrcSpan)
-- | Map of unique names.
, criticalsUniqMap :: M.Map F.Name F.Name
-- | Location of criticals.
, criticalsFromWhere :: M.Map F.Name FilePath
}
instance NFData Criticals where
rnf _ = ()
instance ExitCodeOfReport Criticals where
exitCodeOf _ = 0
instance Show Criticals where
show crits =
case vars of
[] -> concat ["\n", fname, ": No additional annotations are necessary.\n"]
_ -> concat ["\n", fname, ": ", show numVars
, " variable declarations suggested to be given a specification:\n"
, unlines [ " " ++ declReport d | d <- M.toList dmapSlice ]]
where
fname = F.pfGetFilename . criticalsPf $ crits
dmap = criticalsDeclarations crits
uniqnameMap = criticalsUniqMap crits
fromWhereMap = criticalsFromWhere crits
vars = criticalsVariables crits
unitVarName (UnitVar (v, _)) = v
unitVarName (UnitParamVarUse (_, (v, _), _)) = v
unitVarName _ = "<bad>"
varNames = map unitVarName vars
dmapSlice = M.filterWithKey (\ k _ -> k `elem` varNames) dmap
numVars = M.size dmapSlice
declReport (v, (_, ss)) = vfilename ++ " (" ++ showSpanStart ss ++ ") " ++ fromMaybe v (M.lookup v uniqnameMap)
where vfilename = fromMaybe fname $ M.lookup v fromWhereMap
showSpanStart (FU.SrcSpan l _) = show 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 = do
cons <- usConstraints `fmap` get
return $ criticalVariables cons
-- | Infer one possible set of critical variables for a program.
inferCriticalVariables :: UnitAnalysis Criticals
inferCriticalVariables = do
pf <- asks unitProgramFile
mfs <- lift analysisModFiles
(eVars, _) <- runInference runCriticalVariables
let
-- Use the module map derived from all of the included Camfort Mod files.
(pfRenamed, mmap) = withCombinedModuleMap mfs . FA.initAnalysis . fmap UA.mkUnitAnnotation $ pf
-- unique name -> src name across modules
-- Map of all declarations
dmap = extractDeclMap pfRenamed `M.union` combinedDeclMap mfs
uniqnameMap = M.fromList [
(FA.varName e, FA.srcName e) |
e@(F.ExpValue _ _ F.ValVariable{}) <- universeBi pfRenamed :: [F.Expression UA]
-- going to ignore intrinsics here
] `M.union` (M.unions . map (M.fromList . map (\ (a, (b, _)) -> (b, a)) . M.toList) $ M.elems mmap)
fromWhereMap = genUniqNameToFilenameMap mfs
pure $!! Criticals { criticalsPf = pf
, criticalsVariables = eVars
, criticalsDeclarations = dmap
, criticalsUniqMap = uniqnameMap
, criticalsFromWhere = fromWhereMap
}