feat_integrity: added check integrity: functions should be present in…

nitta.cabal

@@ -58,6 +58,7 @@ library
       NITTA.Intermediate.Value
       NITTA.Intermediate.Variable
       NITTA.LuaFrontend
+      NITTA.Model.IntegrityCheck
       NITTA.Model.Microarchitecture
       NITTA.Model.Networks.Bus
       NITTA.Model.Networks.Types

src/NITTA/Model/IntegrityCheck.hs

@@ -0,0 +1,222 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{- |
+Module      : NITTA.Model.IntegrityCheck
+Description : Module for checking PU model description consistency
+Copyright   : (c) Artyom Kostyuchik, 2021
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+-}
+module NITTA.Model.IntegrityCheck (
+    ProcessConsistent (..),
+) where
+
+import Control.Monad
+import Data.Data
+import Data.Either
+import qualified Data.Map.Strict as M
+import Data.Maybe
+import qualified Data.Set as S
+import NITTA.Intermediate.Functions
+import NITTA.Intermediate.Types
+import NITTA.Model.Networks.Bus (BusNetwork, Instruction (Transport))
+import NITTA.Model.ProcessorUnits
+import NITTA.Utils
+import NITTA.Utils.ProcessDescription
+
+class ProcessConsistent u where
+    checkProcessСonsistent :: u -> Either String ()
+
+instance {-# OVERLAPS #-} (ProcessorUnit (pu v x t) v x2 t2) => ProcessConsistent (pu v x t) where
+    checkProcessСonsistent pu =
+        let isConsistent =
+                [ checkEndpointToIntermidiateRelation (getEpMap pu) (getInterMap pu) M.empty pu
+                , checkInstructionToEndpointRelation (getInstrMap pu) (getEpMap pu) $ process pu
+                , checkCadToFunctionRelation (getCadFunctionsMap pu) (getCadStepsMap pu) pu
+                ]
+         in checkResult isConsistent
+
+instance {-# INCOHERENT #-} (ProcessorUnit (pu v x t) v x2 t2, UnitTag (pu v x t)) => ProcessConsistent (BusNetwork (pu v x t) v x2 t2) where
+    checkProcessСonsistent pu =
+        let isConsistent =
+                [ checkEndpointToIntermidiateRelation (getEpMap pu) (getInterMap pu) (getTransportMap pu) pu
+                , checkInstructionToEndpointRelation (getInstrMap pu) (getEpMap pu) $ process pu
+                , checkCadToFunctionRelation (getCadFunctionsMap pu) (getCadStepsMap pu) pu
+                ]
+         in checkResult isConsistent
+
+-- checkProcessСonsistent _pu =
+--     let isConsistent = [Left "Trying to run BusNetwork"]
+--      in checkResult isConsistent
+
+checkResult res =
+    if any isLeft res
+        then Left $ concat $ lefts res
+        else Right ()
+
+checkEndpointToIntermidiateRelation eps ifs trans pu =
+    let checkIfsEmpty = M.size eps > 0 && M.size ifs == 0
+        checkEpsEmpty = M.size ifs > 0 && M.size eps == 0
+        rels = S.fromList $ filter isVertical $ relations $ process pu
+        lookup' v = fromMaybe (showError "Endpoint to Intermidiate" "enpoint" v pu) $ eps M.!? v
+        makeRelationList =
+            map S.fromList $
+                concatMap
+                    ( \(h, f) ->
+                        sequence $
+                            concatMap
+                                ( \v -> [[Vertical h $ fst p | p <- lookup' v]]
+                                )
+                                $ variables f
+                    )
+                    $ M.toList ifs
+     in do
+            when checkEpsEmpty $
+                Left "endpoints are empty"
+            when checkIfsEmpty $
+                Left "functions are empty"
+            if any (`S.isSubsetOf` rels) makeRelationList
+                then Right True
+                else checkTransportToIntermidiateRelation ifs rels trans pu
+
+-- TODO: add map with endpoints (as Source) to be sure that function is connected to endpoint after all
+--       it means: Endpoint (Source) -> Transport -> Function
+-- TODO: remove pu
+checkTransportToIntermidiateRelation ifs rels transMap pu =
+    let lookup' v = fromMaybe (showError "Transport to Intermidiate" "transport" v pu) $ transMap M.!? v
+        makeRelationList =
+            map S.fromList $
+                concatMap
+                    ( \(h, f) ->
+                        concatMap
+                            ( \v -> [[Vertical h $ fst $ lookup' v]]
+                            )
+                            $ variables f
+                    )
+                    $ M.toList ifs
+     in if any (`S.isSubsetOf` rels) makeRelationList
+            then Right True
+            else Left "Endpoint and Transport to Intermideate (function) not consistent"
+
+checkInstructionToEndpointRelation ins eps pr =
+    let checkInsEmpty = M.size eps > 0 && M.size ins == 0
+        checkEpsEmpty = M.size ins > 0 && M.size eps == 0
+        eps' = M.fromList $ concat $ M.elems eps
+        rels = S.fromList $ map (\(Vertical r1 r2) -> (r1, r2)) $ filter isVertical $ relations pr
+        consistent =
+            and $
+                concatMap
+                    ( \(r1, r2) -> case eps' M.!? r1 of
+                        Just _ | Just (InstructionStep _) <- ins M.!? r2 -> [True]
+                        _ -> []
+                    )
+                    rels
+     in do
+            when checkInsEmpty $ Left "instructions are empty"
+            when checkEpsEmpty $ Left "enpoints are empty"
+            if consistent
+                then Right True
+                else Left "Instruction to Endpoint not consistent"
+
+-- now it checks LoopBegin/End
+checkCadToFunctionRelation cadFs cadSteps pu =
+    let consistent = S.isSubsetOf makeCadVertical rels
+        rels = S.fromList $ filter isVertical $ relations $ process pu
+        showLoop f = "bind " <> show f
+        -- TODO: remove pu
+        lookup' v = fromMaybe (showError "CAD" "steps" v pu) $ cadSteps M.!? v
+        makeCadVertical =
+            S.fromList $
+                concatMap
+                    ( \(h, f) ->
+                        concatMap
+                            ( \v -> [uncurry Vertical (lookup' v, h)]
+                            )
+                            [showLoop f]
+                    )
+                    $ M.toList cadFs
+     in if consistent
+            then Right True
+            else Left $ "CAD functions not consistent. Excess:" <> show (S.difference makeCadVertical rels)
+
+getInterMap pu =
+    M.fromList
+        [ (pID, f)
+        | step@Step{pID} <- steps $ process pu
+        , isFB step
+        , f <- case getFunction step of
+            Just f -> [f]
+            _ -> []
+        ]
+
+getEpMap pu =
+    M.fromListWith (++) $
+        concat
+            [ concatMap (\v -> [(v, [(pID, ep)])]) $ variables ep
+            | step@Step{pID} <- steps $ process pu
+            , isEndpoint step
+            , ep <- case getEndpoint step of
+                Just e -> [e]
+                _ -> []
+            ]
+
+getInstrMap pu =
+    M.fromList
+        [ (pID, instr)
+        | step@Step{pID} <- steps $ process pu
+        , isInstruction step
+        , instr <- case getInstruction step of
+            Just i -> [i]
+            _ -> []
+        ]
+
+getTransportMap pu =
+    let getTransport :: (Typeable a, Typeable v, Typeable x, Typeable t) => pu v x t -> a -> Maybe (Instruction (BusNetwork String v x t))
+        getTransport _ = cast
+        filterTransport pu' pid (InstructionStep ins)
+            | Just instr@(Transport v _ _) <- getTransport pu' ins = Just (v, (pid, instr))
+            | otherwise = Nothing
+        filterTransport _ _ _ = Nothing
+     in M.fromList $ mapMaybe (uncurry $ filterTransport pu) $ M.toList $ getInstrMap pu
+
+getTransportMapBus pu =
+    let filterTransport pu' (InstructionStep ins)
+            | Just (Transport v _ _) <- castInstruction pu' ins = Just v
+            | otherwise = Nothing
+        filterTransport _ _ = Nothing
+     in M.mapMaybe (filterTransport pu) $ getInstrMap pu
+
+getCadFunctionsMap pu =
+    let filterCad (_, f)
+            | Just Loop{} <- castF f = True
+            | Just (LoopBegin Loop{} _) <- castF f = True
+            | Just (LoopEnd Loop{} _) <- castF f = True
+            | otherwise = False
+     in M.fromList $ filter filterCad $ M.toList $ getInterMap pu
+
+getCadStepsMap pu =
+    M.fromList
+        [ (pDesc', pID)
+        | step@Step{pID} <- steps $ process pu
+        , pDesc' <- case getCAD step of
+            Just msg -> [msg]
+            _ -> []
+        ]
+
+showError name mapName v pu =
+    error $
+        name
+            <> " relations contain error: "
+            <> show v
+            <> " is not present in "
+            <> mapName
+            <> " map."
+            <> "proc: "
+            <> show (process pu)

src/NITTA/Model/Networks/Bus.hs

@@ -25,6 +25,7 @@ For creating BusNetwork see 'NITTA.Model.Microarchitecture'.
 -}
 module NITTA.Model.Networks.Bus (
     BusNetwork (..),
+    Instruction (..),
     Ports (..),
     IOPorts (..),
     bindedFunctions,
@@ -177,8 +178,8 @@ instance (UnitTag tag, VarValTime v x t) => ProcessorUnit (BusNetwork tag v x t)
         let v2transportStepKey =
                 M.fromList
                     [ (v, pID)
-                    | Step{pID, pDesc} <- steps bnProcess
-                    , isInstruction pDesc
+                    | step@Step{pID, pDesc} <- steps bnProcess
+                    , isInstruction step
                     , v <- case pDesc of
                         (InstructionStep ins) | Just (Transport var _ _) <- castInstruction net ins -> [var]
                         _ -> []
@@ -200,7 +201,7 @@ instance (UnitTag tag, VarValTime v x t) => ProcessorUnit (BusNetwork tag v x t)
                 mapM_
                     ( \(epKey, v) ->
                         when (v `M.member` v2transportStepKey) $
-                            establishVerticalRelation (v2transportStepKey M.! v) epKey
+                            establishVerticalRelations [v2transportStepKey M.! v] [epKey]
                     )
                     enpointStepKeyVars
 
@@ -210,7 +211,7 @@ instance (UnitTag tag, VarValTime v x t) => ProcessorUnit (BusNetwork tag v x t)
                         mapM_
                             ( \v ->
                                 when (v `M.member` v2transportStepKey) $
-                                    establishVerticalRelation pID (v2transportStepKey M.! v)
+                                    establishVerticalRelations [pID] [v2transportStepKey M.! v]
                             )
                             $ variables f
                     )
@@ -227,7 +228,12 @@ instance (UnitTag tag, VarValTime v x t) => ProcessorUnit (BusNetwork tag v x t)
                                 return (pID, pID')
                             )
                             steps
-                mapM_ (\(Vertical h l) -> establishVerticalRelation (pu2netKey M.! h) (pu2netKey M.! l)) relations
+                mapM_
+                    ( \case
+                        (Vertical h l) -> establishVerticalRelations [pu2netKey M.! h] [pu2netKey M.! l]
+                        (Horizontal h l) -> establishHorizontalRelations [pu2netKey M.! h] [pu2netKey M.! l]
+                    )
+                    relations
 
 instance Controllable (BusNetwork tag v x t) where
     data Instruction (BusNetwork tag v x t)

src/NITTA/Model/ProcessorUnits/Accum.hs

@@ -188,10 +188,9 @@ instance (VarValTime v x t, Num x) => EndpointProblem (Accum v x t) v t where
                     (_, process_') = runSchedule pu $ do
                         endpoints <- scheduleEndpoint d $ scheduleInstruction (epAt -1) Out
                         when (null tasks') $ do
-                            high <- scheduleFunction (a ... sup epAt) func
-                            let low = endpoints ++ map pID (relatedEndpoints process_ $ variables func)
-                            establishVerticalRelations high low
-
+                            -- FIXME: here ([]) you can see the source of error.
+                            -- Function don't connected to bind step. It should be fixed.
+                            scheduleFunctionFinish [] func $ a ... sup epAt
                         updateTick (sup epAt)
                         return endpoints
                  in pu

src/NITTA/Model/ProcessorUnits/Broken.hs

@@ -26,7 +26,7 @@ module NITTA.Model.ProcessorUnits.Broken (
     IOPorts (..),
 ) where
 
-import Control.Monad (when)
+import Control.Monad
 import Data.Default
 import Data.List (find, (\\))
 import Data.Set (elems, fromList, member)
@@ -64,6 +64,9 @@ data Broken v x t = Broken
     , -- |lost source endpoint due synthesis
       lostEndpointSource :: Bool
     , wrongAttr :: Bool
+    , lostFunctionRelation :: Bool
+    , lostEndpointRelation :: Bool
+    , lostInstructionRelation :: Bool
     , unknownDataOut :: Bool
     }
 
@@ -117,29 +120,47 @@ instance (VarValTime v x t) => EndpointProblem (Broken v x t) v t where
         | not $ null remain = concatMap (endpointOptions . execution pu) $ tail remain
     endpointOptions pu@Broken{remain} = concatMap (endpointOptions . execution pu) remain
 
-    endpointDecision pu@Broken{targets = [v], currentWorkEndpoints, wrongControlOnPush} d@EndpointSt{epRole = Target v', epAt}
-        | v == v'
-          , let (newEndpoints, process_') = runSchedule pu $ do
-                    updateTick (sup epAt)
-                    scheduleEndpoint d $ scheduleInstruction (shiftI (if wrongControlOnPush then 1 else 0) epAt) Load =
-            pu
-                { process_ = process_'
-                , targets = []
-                , currentWorkEndpoints = newEndpoints ++ currentWorkEndpoints
-                , doneAt = Just $ sup epAt + 3
-                }
     endpointDecision
-        pu@Broken{targets = [], sources, doneAt, currentWork = Just (a, f), currentWorkEndpoints, wrongControlOnPull}
+        pu@Broken{targets = [v], currentWorkEndpoints, wrongControlOnPush, lostInstructionRelation, lostEndpointRelation}
+        d@EndpointSt{epRole = Target v', epAt}
+            | v == v'
+              , let (newEndpoints, process_') = runSchedule pu $ do
+                        updateTick (sup epAt)
+                        let ins =
+                                if lostInstructionRelation
+                                    then return []
+                                    else scheduleInstruction (shiftI (if wrongControlOnPush then 1 else 0) epAt) Load
+                        if lostEndpointRelation then return [] else scheduleEndpoint d ins =
+                pu
+                    { process_ = process_'
+                    , targets = []
+                    , currentWorkEndpoints = newEndpoints ++ currentWorkEndpoints
+                    , doneAt = Just $ sup epAt + 3
+                    }
+    endpointDecision
+        pu@Broken{targets = [], sources, doneAt, currentWork = Just (a, f), currentWorkEndpoints, wrongControlOnPull, lostInstructionRelation, lostEndpointRelation, lostFunctionRelation}
         d@EndpointSt{epRole = Source v, epAt}
             | not $ null sources
               , let sources' = sources \\ elems v
               , sources' /= sources
               , let (newEndpoints, process_') = runSchedule pu $ do
-                        endpoints <- scheduleEndpoint d $ scheduleInstruction (shiftI (if wrongControlOnPull then 0 else -1) epAt) Out
+                        let ins =
+                                if lostInstructionRelation
+                                    then return []
+                                    else scheduleInstruction (shiftI (if wrongControlOnPull then 0 else -1) epAt) Out
+                        let res =
+                                if lostEndpointRelation
+                                    then return []
+                                    else scheduleEndpoint d ins
+                        endpoints <- res
                         when (null sources') $ do
-                            high <- scheduleFunction (a ... sup epAt) f
+                            -- TODO: migrate to scheduleFunctionFinish: unless lostFunctionRelation $ scheduleFunctionFinish low f (a ... sup epAt)
+                            high <-
+                                if lostFunctionRelation
+                                    then return []
+                                    else scheduleFunction (a ... sup epAt) f
                             let low = endpoints ++ currentWorkEndpoints
-                            establishVerticalRelations high low
+                            unless lostFunctionRelation $ uncurry establishVerticalRelations (high, low)
                         updateTick (sup epAt + 1)
                         return endpoints =
                 pu
@@ -201,6 +222,9 @@ instance (Time t) => Default (Broken v x t) where
             , lostEndpointTarget = False
             , lostEndpointSource = False
             , wrongAttr = False
+            , lostFunctionRelation = False
+            , lostEndpointRelation = False
+            , lostInstructionRelation = False
             , unknownDataOut = False
             }