module Camfort.Specification.Units.InferenceFrontend (doInferUnits) where
import Data.Data
import Data.Char
import Data.Function
import Data.List
import Data.Matrix
import qualified Data.Map as M
import Data.Maybe
import Data.Ratio
import Data.Generics.Uniplate.Operations
import Data.Label.Monadic hiding (modify)
import Control.Monad.State.Strict hiding (gets)
import Control.Monad
import Control.Monad.Writer.Strict
import GHC.Prim
import qualified Language.Fortran.AST as F
import qualified Language.Fortran.Analysis as FA
import qualified Language.Fortran.Analysis.Types as FAT
import qualified Language.Fortran.Analysis.Renaming as FAR
import qualified Language.Fortran.Analysis.BBlocks as FAB
import qualified Language.Fortran.Analysis.DataFlow as FAD
import qualified Language.Fortran.Util.Position as FU
import qualified Language.Fortran.Util.SecondParameter as FUS
import Camfort.Analysis.CommentAnnotator
import Camfort.Analysis.Annotations hiding (Unitless)
import Camfort.Analysis.Types
import Camfort.Specification.Units.Debug
import Camfort.Specification.Units.Environment
import Camfort.Specification.Units.InferenceBackend
import Camfort.Specification.Units.Solve
import qualified Camfort.Specification.Units.Parser as Parser
import Camfort.Transformation.Syntax
import qualified Debug.Trace as D
type A1 = FA.Analysis (UnitAnnotation A)
type Params = (?criticals :: Bool,
?solver :: Solver,
?debug :: Bool,
?assumeLiterals :: AssumeLiterals,
?nameMap :: FAR.NameMap,
?argumentDecls :: Bool)
realName :: (?nameMap :: FAR.NameMap) => F.Name -> F.Name
realName v = v `fromMaybe` (v `M.lookup` ?nameMap)
plumb f x = do { f x ; return x }
onPrev :: (a -> a) -> FA.Analysis a -> FA.Analysis a
onPrev f ann = ann { FA.prevAnnotation = f (FA.prevAnnotation ann) }
instance ASTEmbeddable A1 Parser.UnitStatement where
annotateWithAST ann ast =
onPrev (\ann -> ann { unitSpec = Just ast }) ann
instance Linkable A1 where
link ann (b@(F.BlStatement _ _ _ (F.StDeclaration {}))) =
onPrev (\ann -> ann { unitBlock = Just b }) ann
link ann b = ann
doInferUnits ::
Params => F.ProgramFile A1
-> State UnitEnv ()
doInferUnits pf = do
(pf', parserReport) <- return $ runWriter (annotateComments Parser.unitParser pf)
report <<++ (intercalate "\n" parserReport)
let ?argumentDecls = False in descendBiM perProgramUnit pf'
ifDebug (report <<++ "Finished inferring prog units")
ifDebug debugGaussian
inferInterproceduralUnits pf'
return ()
perProgramUnit :: Params
=> F.ProgramUnit A1
-> State UnitEnv (F.ProgramUnit A1)
perProgramUnit p@(F.PUMain _ _ _ body subprogs) = do
resetTemps
descendBiM perBlock body
descendBiM perProgramUnit subprogs
return p
perProgramUnit p@(F.PUModule _ _ _ body subprogs) = do
resetTemps
puname =: (Just $ FA.puName p)
descendBiM perBlock p
descendBiM perProgramUnit subprogs
return p
perProgramUnit p@(F.PUSubroutine ann span rec name args body subprogs) = do
resetTemps
addProcedure rec name Nothing args body span
descendBiM perProgramUnit subprogs
return p
perProgramUnit p@(F.PUFunction ann span retTy rec name args result
body subprogs) = do
resetTemps
addProcedure rec name (Just name) args body span
descendBiM perProgramUnit subprogs
return p
perProgramUnit p = do
resetTemps
descendBiM perBlock p
return p
addProcedure :: Params
=> Bool
-> F.Name
-> Maybe F.Name
-> (Maybe (F.AList F.Expression A1))
-> [F.Block A1]
-> FU.SrcSpan
-> State UnitEnv ()
addProcedure rec name rname args body span = do
let ?argumentDecls = True in mapM_ perStatement [s | s@(F.StDeclaration {}) <- universeBi body :: [F.Statement A1]]
uenv <- gets varColEnv
resultVar <- case rname of
Just rname ->
case (lookupWithoutSrcSpanRealName rname uenv) of
Just (uvar, _) -> return $ Just uvar
Nothing -> do m <- addCol Variable
varColEnv << (VarBinder (rname, span), (VarCol m, []))
return $ (Just (VarCol m))
Nothing -> return Nothing
let argVars = fromMaybe [] (fmap (map (lookupUnitByName uenv) . F.aStrip) args)
procedureEnv << (name, (resultVar, argVars))
descendBiM perBlock body
if rec
then do descendBiM perBlock body
return ()
else return ()
ifDebug (report <<++ "Pre doing row reduce")
consistent <- solveSystemM ""
success =: consistent
linearSystem =. reduceRows 1
ifDebug (report <<++ "Post doing reduce")
ifDebug (debugGaussian)
return ()
where
lookupUnitByName uenv ve@(F.ExpValue _ _ (F.ValVariable _)) =
maybe (VarCol 1) fst $ lookupWithoutSrcSpan v uenv
where v = FA.varName ve
perBlock :: Params
=> F.Block A1
-> State UnitEnv (F.Block A1)
perBlock b@(F.BlComment ann span _) = do
case (unitSpec (FA.prevAnnotation ann), unitBlock (FA.prevAnnotation ann)) of
(Just (Parser.UnitAssignment (Just vars) unitsAST), Just block) -> do
let units = toUnitInfo unitsAST
unitsConverted <- convertUnit units
case block of
bl@(F.BlStatement ann span _ (F.StDeclaration _ _ _ _ decls)) ->
flip mapM_ vars (\var ->
mapM_ (processVar' (Just var) [unitsConverted]) (getNamesAndInits decls))
_ -> return ()
(Just (Parser.UnitAlias name unitsAST), _) -> do
let unitInfo = toUnitInfo unitsAST
learnDerivedUnit (name, unitInfo)
_ -> return ()
return b
where
processVar' varReal unitC (var, init, span) = do
if (Just (realName var) == varReal) then hasDeclaration <<++ var else return ()
processVar varReal unitC (var, init, span)
learnDerivedUnit (name, spec) =
do denv <- gets derivedUnitEnv
when (isJust $ lookup name denv) $ error "Redeclared unit of measure"
unit <- convertUnit spec
denv <- gets derivedUnitEnv
when (isJust $ lookup name denv) $ error "Recursive unit-of-measure definition"
derivedUnitEnv << (name, unit)
getNamesAndInits x =
[(FA.varName e, i, s) | (F.DeclVariable _ _ e@(F.ExpValue _ s (F.ValVariable v)) _ i) <-
(universeBi (F.aStrip x) :: [F.Declarator A1])]
++ [(FA.varName e, i, s) | (F.DeclArray _ _ e@(F.ExpValue _ s (F.ValVariable v)) _ _ i) <-
(universeBi (F.aStrip x) :: [F.Declarator A1])]
dimDeclarators x = concat
[F.aStrip dims | (F.DeclArray _ _ _ dims _ _) <-
(universeBi (F.aStrip x) :: [F.Declarator A1])]
perBlock b@(F.BlStatement _ _ _ s) = do
perStatement s
return b
perBlock b = do
mapM_ perDoSpecification (universeBi b)
mapM_ perExpr (universeBi b)
descendBiM (plumb perBlock) b
return b
processVar :: Params
=> Maybe F.Name
-> [UnitConstant]
-> (F.Name, Maybe (F.Expression A1), FU.SrcSpan)
-> State UnitEnv ()
processVar (Just dvar) units (v, initExpr, span) | dvar == (realName v) = do
system <- gets linearSystem
let m = ncols (fst system) + 1
unitVarCats <<++ (if ?argumentDecls then Argument else Variable)
extendConstraints units
varColEnv << (VarBinder (v, span), (VarCol m, []))
uv <- gets varColEnv
case initExpr of
Nothing -> return ()
Just e -> do
uv <- perExpr e
mustEqual False (VarCol m) uv
return ()
processVar dvar units (v, initExpr, span) | otherwise = return ()
perDoSpecification ::
Params
=> F.DoSpecification A1 -> State UnitEnv ()
perDoSpecification (F.DoSpecification _ _
st@(F.StExpressionAssign _ _ ei e0) en step) = do
uiv <- perExpr ei
e0v <- perExpr e0
env <- perExpr en
mustEqual True uiv e0v
mustEqual True e0v env
case step of
Nothing -> return ()
Just stepE -> do stepv <- perExpr stepE
mustEqual True env stepv
return ()
perStatement ::
Params
=> F.Statement A1 -> State UnitEnv ()
perStatement (F.StDeclaration _ span spec atr decls) = do
uenv <- gets varColEnv
mapM_ (\(v, i, s) -> if notAlreadyDeclared uenv v
then processVar (Just (realName v)) [] (v, i, s)
else return ()) (getNamesAndInits decls)
where
notAlreadyDeclared uenv v =
case lookupWithoutSrcSpan v uenv of
Nothing -> True
Just _ -> False
getNamesAndInits x =
[(FA.varName e, i, s) |
(F.DeclVariable _ _ e@(F.ExpValue _ s (F.ValVariable _)) _ i)
<- (universeBi (F.aStrip x) :: [F.Declarator A1])]
++ [(FA.varName e, i, s) |
(F.DeclArray _ _ e@(F.ExpValue _ s (F.ValVariable _)) _ _ i)
<- (universeBi (F.aStrip x) :: [F.Declarator A1])]
perStatement (F.StExpressionAssign _ span e1 e2) = do
uv1 <- perExpr e1
uv2 <- perExpr e2
mustEqual False uv1 uv2
return ()
perStatement (F.StPointerAssign _ _ e1 e2) = do
uv1 <- perExpr e1
uv2 <- perExpr e2
mustEqual False uv1 uv2
return ()
perStatement (F.StCall _ _ e@(F.ExpValue _ _ (F.ValVariable vReal)) args) = do
uvs <- fromMaybe (return []) (fmap (mapM perArgument . F.aStrip) args)
case (lookup (map toUpper vReal) intrinsicsDict) of
Just fun -> fun vReal
Nothing -> return ()
uv@(VarCol uvn) <- anyUnits Temporary
calls << (vReal, (Just uv, uvs))
perStatement s = do
mapM_ perDoSpecification (universeBi s)
descendBiM (plumb perExpr) s
return ()
inferInterproceduralUnits ::
Params => F.ProgramFile A1 -> State UnitEnv ()
inferInterproceduralUnits x =
do --reorderColumns
if ?criticals then reorderVarCols else return ()
consistent <- solveSystemM "inconsistent"
if consistent then
do system <- gets linearSystem
let dontAssumeLiterals = case ?assumeLiterals of
Poly -> True
Unitless -> False
Mixed -> False
inferInterproceduralUnits' x dontAssumeLiterals system
return ()
else
return ()
inferInterproceduralUnits' ::
Params => F.ProgramFile A1 -> Bool -> LinearSystem
-> State UnitEnv (F.ProgramFile A1)
inferInterproceduralUnits' x haveAssumedLiterals system1 =
do addInterproceduralConstraints x
consistent <- solveSystemM "inconsistent"
if not consistent then
do linearSystem =: system1
return x
else do
system2 <- gets linearSystem
if system1 == system2
then if ?criticals then nextStep else checkUnderdeterminedM >> nextStep
else inferInterproceduralUnits' x haveAssumedLiterals system2
where nextStep | haveAssumedLiterals = return x
| otherwise = do consistent <- assumeLiteralUnits
if not consistent
then return x
else do system3 <- gets linearSystem
inferInterproceduralUnits' x True system3
assumeLiteralUnits :: (?solver :: Solver, ?debug :: Bool) => State UnitEnv Bool
assumeLiteralUnits =
do system@(matrix, vector) <- gets linearSystem
mapM_ assumeLiteralUnits' [1 .. ncols matrix]
consistent <- solveSystemM "underdetermined"
when (not consistent) $ linearSystem =: system
return consistent
assumeLiteralUnits' m =
do (matrix, vector) <- gets linearSystem
ucats <- gets unitVarCats
let n = find (\n -> matrix ! (n, m) /= 0) [1 .. nrows matrix]
m' = n >>= (\n -> find (\m -> matrix ! (n, m) /= 0) [1 .. ncols matrix])
nonLiteral n m = matrix ! (n, m) /= 0 && ucats !! (m 1) /= (Literal True)
m's = n >>= (\n -> find (nonLiteral n) [1 .. ncols matrix])
when (ucats !! (m 1) == (Literal True) && (m' /= Just m || isJust m's)) $ do
n' <- addRow
modify $ liftUnitEnv $ setElem 1 (n', m)
addInterproceduralConstraints ::
(?debug :: Bool) => F.ProgramFile A1 -> State UnitEnv ()
addInterproceduralConstraints x =
do
cs <- gets calls
penv <- gets procedureEnv
mapM_ (addCall penv) cs
where
addCall penv (name, (result, args)) =
do case lookup name penv of
Just (r, as) -> let (r1, r2) = decodeResult result r
in handleArgs (args ++ r1) (as ++ r2)
Nothing -> return ()
handleArgs actualVars dummyVars =
do order <- gets reorderedCols
let actual = map (\(VarCol uv) -> uv) actualVars
dummy = map (\(VarCol uv) -> uv) dummyVars
mapM_ (handleArg $ zip dummy actual) dummy
handleArg dummyToActual dummy =
do (matrix, vector) <- gets linearSystem
ifDebug (debugGaussian)
ifDebug (report <<++ ("hArg - " ++ show dummyToActual ++ "-" ++ show dummy))
let
n = maybe 1 id $ find (\n -> matrix ! (n, dummy) /= 0) [1 .. nrows matrix]
Just m = find (\m -> matrix ! (n, m) /= 0) [1 .. ncols matrix]
ifDebug (report <<++ ("n = " ++ show n ++ ", m = " ++ show m))
if (m == dummy) then
do let
ms = filter (\m -> matrix ! (n, m) /= 0) [m .. ncols matrix]
m's = mapMaybe (flip lookup dummyToActual) ms
pairs =
--else
(zip ms m's)
ifDebug (report <<++ ("ms = " ++ show ms ++ ", m's' = "
++ show m's
++ ", their zip = " ++ show pairs
++ " dA = " ++ show dummyToActual))
if (True)
then do { newRow <- addRow' $ vector !! (n 1);
mapM_ (handleArgPair matrix n newRow) dummyToActual ; }
else return ()
else
return ()
handleArgPair matrix n newRow (m, m') = do
modify $ liftUnitEnv $ setElem (matrix ! (n, m)) (newRow, m')
decodeResult (Just r1) (Just r2) = ([r1], [r2])
decodeResult Nothing Nothing = ([], [])
decodeResult (Just _) Nothing = error "Subroutine used as a function!"
decodeResult Nothing (Just _) = error "Function used as a subroutine!"
data BinOpKind = AddOp | MulOp | DivOp | PowerOp | LogicOp | RelOp
binOpKind :: F.BinaryOp -> BinOpKind
binOpKind F.Addition = AddOp
binOpKind F.Subtraction = AddOp
binOpKind F.Multiplication = MulOp
binOpKind F.Division = DivOp
binOpKind F.Exponentiation = PowerOp
binOpKind F.Concatenation = AddOp
binOpKind F.GT = RelOp
binOpKind F.GTE = RelOp
binOpKind F.LT = RelOp
binOpKind F.LTE = RelOp
binOpKind F.EQ = RelOp
binOpKind F.NE = RelOp
binOpKind F.Or = LogicOp
binOpKind F.And = LogicOp
binOpKind F.Equivalent = RelOp
binOpKind F.NotEquivalent = RelOp
binOpKind (F.BinCustom _) = RelOp
(<**>) :: Maybe a -> Maybe a -> Maybe a
Nothing <**> x = x
(Just x) <**> y = (Just x)
perIndex :: Params => F.Name -> F.Index A1 -> State UnitEnv ()
perIndex v (F.IxSingle _ _ _ e) = return ()
perExpr :: Params => F.Expression A1 -> State UnitEnv VarCol
perExpr e@(F.ExpValue _ span (F.ValVariable _)) = do
let v = FA.varName e
uenv <- gets varColEnv
case lookupWithoutSrcSpan v uenv of
Nothing ->
case lookupWithoutSrcSpanRealName (realName v) uenv of
Nothing -> do uv@(VarCol uvn) <- anyUnits Temporary
return uv
Just (uv, _) -> return uv
Just (uv, _) -> return uv
perExpr e@(F.ExpValue _ span v) = perLiteral v
where
perLiteral :: Params => F.Value A1 -> State UnitEnv VarCol
perLiteral val = do
uv@(VarCol uvn) <- anyUnits (Literal (?assumeLiterals /= Mixed))
debugInfo << (uvn, (span, show val))
return uv
perExpr e@(F.ExpBinary _ _ op e1 e2) = do
uv1 <- perExpr e1
uv2 <- perExpr e2
(VarCol n) <- case binOpKind op of
AddOp -> mustEqual True uv1 uv2
MulOp -> mustAddUp uv1 uv2 1 1
DivOp -> mustAddUp uv1 uv2 1 (1)
PowerOp -> powerUnits uv1 e2
LogicOp -> mustEqual True uv1 uv2
RelOp -> do mustEqual True uv1 uv2
return $ VarCol 1
debugInfo << (n, (FU.getSpan e, pprint e))
return (VarCol n)
where
pprint e = ""
perExpr (F.ExpUnary _ _ _ e) = perExpr e
perExpr (F.ExpSubscript _ _ e alist) = do
descendBiM (plumb (perIndex (FA.varName e))) alist
perExpr e
perExpr f@(F.ExpFunctionCall _ span e@(F.ExpValue _ _ (F.ValVariable vReal)) args) = do
uv <- anyUnits Temporary
argsU <- fromMaybe (return []) (fmap (mapM perArgument . F.aStrip) args)
calls << (vReal, (Just uv, argsU))
return uv
perExpr f@(F.ExpDataRef _ _ e1 e2) = do
perExpr e2
perExpr e1
perExpr f@(F.ExpImpliedDo _ _ exprs spec) = do
perDoSpecification spec
uv <- anyUnits Temporary
exprsU <- mapM perExpr (F.aStrip exprs)
mapM_ (mustEqual True uv) exprsU
return uv
perExpr f@(F.ExpInitialisation _ _ exprs) = do
uv <- anyUnits Temporary
exprsU <- mapM perExpr (F.aStrip exprs)
mapM_ (mustEqual True uv) exprsU
return uv
perExpr f@(F.ExpReturnSpec _ _ e) = do
perExpr e
perArgument :: Params =>
F.Argument A1 -> State UnitEnv VarCol
perArgument (F.Argument _ _ _ expr) = perExpr expr
handleExpression :: Params
=> F.Expression A1
-> State UnitEnv (F.Expression A1)
handleExpression x = do
perExpr x
return x
powerUnits :: Params
=> VarCol -> F.Expression A1 -> State UnitEnv VarCol
powerUnits (VarCol uv) (F.ExpValue _ _ (F.ValInteger powerString)) =
case fmap (fromInteger . fst) $ listToMaybe $ reads powerString of
Just power -> do
m <- addCol Temporary
n <- addRow
modify $ liftUnitEnv $ incrElem (1) (n, m) . incrElem power (n, uv)
return $ VarCol m
Nothing -> mustEqual False (VarCol uv) (VarCol 1)
powerUnits uv e =
do mustEqual False uv (VarCol 1)
uv <- perExpr e
mustEqual False uv (VarCol 1)
lookupWithoutSrcSpanRealName :: Params => F.Name -> [(VarBinder, a)] -> Maybe a
lookupWithoutSrcSpanRealName v env = snd `fmap` find f env
where
f (VarBinder (w, _), _) = (map toUpper (realName w)) == map toUpper v