diff --git a/nitta.cabal b/nitta.cabal index 84a7d6049..0c50e52b5 100644 --- a/nitta.cabal +++ b/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 diff --git a/src/NITTA/Model/IntegrityCheck.hs b/src/NITTA/Model/IntegrityCheck.hs new file mode 100644 index 000000000..48d313063 --- /dev/null +++ b/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 : aleksandr.penskoi@gmail.com +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) diff --git a/src/NITTA/Model/Networks/Bus.hs b/src/NITTA/Model/Networks/Bus.hs index 0a24638cd..e1734204b 100644 --- a/src/NITTA/Model/Networks/Bus.hs +++ b/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) diff --git a/src/NITTA/Model/ProcessorUnits/Accum.hs b/src/NITTA/Model/ProcessorUnits/Accum.hs index 0d081cdda..165e19a88 100644 --- a/src/NITTA/Model/ProcessorUnits/Accum.hs +++ b/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 diff --git a/src/NITTA/Model/ProcessorUnits/Broken.hs b/src/NITTA/Model/ProcessorUnits/Broken.hs index 73e577c00..75a9d5014 100644 --- a/src/NITTA/Model/ProcessorUnits/Broken.hs +++ b/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 } diff --git a/src/NITTA/Model/ProcessorUnits/Fram.hs b/src/NITTA/Model/ProcessorUnits/Fram.hs index bf9514ec7..dff6f9a0c 100644 --- a/src/NITTA/Model/ProcessorUnits/Fram.hs +++ b/src/NITTA/Model/ProcessorUnits/Fram.hs @@ -98,7 +98,7 @@ data Cell v x t = Cell data Job v x t = Job { function :: F v x , startAt :: Maybe t - , binds, endpoints :: [ProcessStepID] + , binds :: [ProcessStepID] } deriving (Show, Eq) @@ -107,7 +107,6 @@ defJob f = { function = f , startAt = Nothing , binds = [] - , endpoints = [] } instance WithFunctions (Cell v x t) (F v x) where @@ -259,7 +258,8 @@ instance (VarValTime v x t) => BreakLoopProblem (Fram v x t) v x where revoke <- scheduleFunctionRevoke $ recLoop bl f1 <- scheduleFunctionBind $ recLoopOut bl f2 <- scheduleFunctionBind $ recLoopIn bl - establishVerticalRelations binds (f1 ++ f2 ++ revoke) + + establishHorizontalRelations binds (f1 ++ f2 ++ revoke) return (f1, f2) iJob = (defJob $ recLoopOut bl){binds = iPid, startAt = Just 0} oJob = (defJob $ recLoopIn bl){binds = oPid} @@ -303,7 +303,7 @@ instance (VarValTime v x t) => EndpointProblem (Fram v x t) v t where -- Constant endpointDecision fram@Fram{memory} d@EndpointSt{epRole = Source vs, epAt} - | Just (addr, cell@Cell{state = DoConstant vs', job = Just Job{function, binds, endpoints}}) <- + | Just (addr, cell@Cell{state = DoConstant vs', job = Just Job{function, binds}}) <- L.find ( \case (_, Cell{state = DoConstant vs'}) -> (vs' L.\\ S.elems vs) /= vs' @@ -313,11 +313,9 @@ instance (VarValTime v x t) => EndpointProblem (Fram v x t) v t where let vsRemain = vs' L.\\ S.elems vs ((), process_') = runSchedule fram $ do updateTick (sup epAt + 1) - endpoints' <- scheduleEndpoint d $ scheduleInstruction (shiftI (-1) epAt) $ PrepareRead addr - when (null vsRemain) $ do - fPID <- scheduleFunction (0 ... sup epAt) function - establishVerticalRelations binds fPID - establishVerticalRelations fPID (endpoints ++ endpoints') + void $ scheduleEndpoint d $ scheduleInstruction (shiftI (-1) epAt) $ PrepareRead addr + when (null vsRemain) $ + scheduleFunctionFinish binds function $ 0 ... sup epAt cell' = case vsRemain of [] -> cell @@ -334,7 +332,7 @@ instance (VarValTime v x t) => EndpointProblem (Fram v x t) v t where } -- Loop endpointDecision fram@Fram{memory} d@EndpointSt{epRole = Source vs, epAt} - | Just (addr, cell@Cell{state = DoLoopSource vs' oJob, job = Just job@Job{binds, function, startAt, endpoints}}) <- + | Just (addr, cell@Cell{state = DoLoopSource vs' oJob, job = Just job@Job{binds, function, startAt}}) <- L.find ( \case (_, Cell{state = DoLoopSource vs' _}) -> (vs' L.\\ S.elems vs) /= vs' @@ -342,19 +340,17 @@ instance (VarValTime v x t) => EndpointProblem (Fram v x t) v t where ) $ A.assocs memory = let vsRemain = vs' L.\\ S.elems vs - (endpoints', process_) = runSchedule fram $ do + (_endpoints, process_) = runSchedule fram $ do updateTick (sup epAt + 1) eps <- scheduleEndpoint d $ scheduleInstruction (shiftI (-1) epAt) $ PrepareRead addr - when (null vsRemain) $ do - fPID <- scheduleFunction (0 ... sup epAt) function - establishVerticalRelations binds fPID - establishVerticalRelations fPID $ eps ++ endpoints + when (null vsRemain) $ + scheduleFunctionFinish binds function $ 0 ... sup epAt return eps cell' = if not $ null vsRemain then cell - { job = Just job{startAt = startAt <|> Just (inf epAt - 1), endpoints = endpoints' ++ endpoints} + { job = Just job{startAt = startAt <|> Just (inf epAt - 1)} , state = DoLoopSource vsRemain oJob } else @@ -364,14 +360,14 @@ instance (VarValTime v x t) => EndpointProblem (Fram v x t) v t where } in fram{process_, memory = memory A.// [(addr, cell')]} endpointDecision fram@Fram{memory} d@EndpointSt{epRole = Target v, epAt} - | Just (addr, cell@Cell{job = Just Job{function, binds, endpoints}}) <- + | Just (addr, cell@Cell{job = Just Job{function, binds}}) <- L.find (\case (_, Cell{state = DoLoopTarget v'}) -> v == v'; _ -> False) $ A.assocs memory = let ((), process_) = runSchedule fram $ do - endpoints' <- scheduleEndpoint d $ scheduleInstruction epAt $ Write addr + void $ scheduleEndpoint d $ scheduleInstruction epAt $ Write addr updateTick (sup epAt + 1) - fPID <- scheduleFunction epAt function - establishVerticalRelations binds fPID - establishVerticalRelations fPID (endpoints ++ endpoints') + + scheduleFunctionFinish binds function epAt + cell' = cell { job = Nothing @@ -385,12 +381,12 @@ instance (VarValTime v x t) => EndpointProblem (Fram v x t) v t where endpointDecision fram@Fram{memory, remainBuffers} d@EndpointSt{epRole = Target v, epAt} | Just (addr, cell@Cell{history}) <- findForBufferCell fram , ([(Buffer (I _) (O vs), j@Job{function})], remainBuffers') <- L.partition (\(Buffer (I v') (O _), _) -> v' == v) remainBuffers = - let (endpoints, process_) = runSchedule fram $ do + let (_endpoints, process_) = runSchedule fram $ do updateTick (sup epAt + 1) scheduleEndpoint d $ scheduleInstruction epAt $ Write addr cell' = cell - { job = Just j{startAt = Just $ inf epAt, endpoints} + { job = Just j{startAt = Just $ inf epAt} , state = DoBuffer $ S.elems vs , lastWrite = Just $ sup epAt , history = function : history @@ -401,7 +397,7 @@ instance (VarValTime v x t) => EndpointProblem (Fram v x t) v t where , process_ } endpointDecision fram@Fram{memory} d@EndpointSt{epRole = Source vs, epAt} - | Just (addr, cell@Cell{state = DoBuffer vs', job = Just Job{function, startAt = Just fBegin, binds, endpoints}}) <- + | Just (addr, cell@Cell{state = DoBuffer vs', job = Just Job{function, startAt = Just fBegin, binds}}) <- L.find ( \case (_, Cell{state = DoBuffer vs'}) -> (vs' L.\\ S.elems vs) /= vs' @@ -411,11 +407,9 @@ instance (VarValTime v x t) => EndpointProblem (Fram v x t) v t where let vsRemain = vs' L.\\ S.elems vs ((), process_) = runSchedule fram $ do updateTick (sup epAt + 1) - endpoints' <- scheduleEndpoint d $ scheduleInstruction (shiftI (-1) epAt) $ PrepareRead addr - when (null vsRemain) $ do - fPID <- scheduleFunction (fBegin ... sup epAt) function - establishVerticalRelations binds fPID - establishVerticalRelations fPID (endpoints ++ endpoints') + void $ scheduleEndpoint d $ scheduleInstruction (shiftI (-1) epAt) $ PrepareRead addr + when (null vsRemain) $ + scheduleFunctionFinish binds function $ fBegin ... sup epAt cell' = case vsRemain of [] -> cell diff --git a/src/NITTA/Model/ProcessorUnits/Multiplier.hs b/src/NITTA/Model/ProcessorUnits/Multiplier.hs index 06734ea75..c3f3f87d7 100644 --- a/src/NITTA/Model/ProcessorUnits/Multiplier.hs +++ b/src/NITTA/Model/ProcessorUnits/Multiplier.hs @@ -528,11 +528,12 @@ instance (VarValTime v x t) => EndpointProblem (Multiplier v x t) v t where let (_, process_') = runSchedule pu $ do endpoints <- scheduleEndpoint d $ scheduleInstruction epAt Out when (null sources') $ do - high <- scheduleFunction (a ... sup epAt) f - let low = endpoints ++ map pID (relatedEndpoints process_ $ variables f) -- Set up the vertical relantions between functional unit -- and related to that data sending. - establishVerticalRelations high low + + -- FIXME: here ([]) you can see the source of error. + -- Function don't connected to bind step. It should be fixed. + scheduleFunctionFinish [] f $ a ... sup epAt -- this is needed to correct work of automatically generated tests -- that takes time about time from Process updateTick (sup epAt) diff --git a/src/NITTA/Model/ProcessorUnits/Shift.hs b/src/NITTA/Model/ProcessorUnits/Shift.hs index ee94508cf..153ce9d8d 100644 --- a/src/NITTA/Model/ProcessorUnits/Shift.hs +++ b/src/NITTA/Model/ProcessorUnits/Shift.hs @@ -189,9 +189,9 @@ instance (VarValTime v x t) => EndpointProblem (Shift v x t) v t where updateTick (sup epAt) endpoints <- scheduleEndpoint d $ scheduleInstruction (shiftI (-1) epAt) Out when (null sources') $ do - high <- scheduleFunction (a ... sup epAt) f - let low = endpoints ++ map pID (relatedEndpoints process_ $ variables f) - establishVerticalRelations high low + -- FIXME: here ([]) you can see the source of error. + -- Function don't connected to bind step. It should be fixed. + scheduleFunctionFinish [] f $ a ... sup epAt return endpoints in pu { process_ = process_' diff --git a/src/NITTA/Model/ProcessorUnits/Types.hs b/src/NITTA/Model/ProcessorUnits/Types.hs index 9e4d83916..e353e9425 100644 --- a/src/NITTA/Model/ProcessorUnits/Types.hs +++ b/src/NITTA/Model/ProcessorUnits/Types.hs @@ -33,6 +33,8 @@ module NITTA.Model.ProcessorUnits.Types ( Step (..), StepInfo (..), Relation (..), + isVertical, + isHorizontal, descent, whatsHappen, extractInstructionAt, @@ -207,8 +209,18 @@ data Relation = -- |Vertical relationships (up and down). For example, the intermediate -- step (function execution) can be translated to a sequence of endpoint -- steps (receiving and sending variable), and process unit instructions. - Vertical ProcessStepID ProcessStepID - deriving (Show, Eq, Generic) + Vertical {vUp, vDown :: ProcessStepID} + | -- |Horizontal relationships (on one level). For example, we bind the + -- function and apply the refactoring. The binding step should be + -- connected to refactoring steps, including new binding steps. + Horizontal {hPrev, hNext :: ProcessStepID} + deriving (Show, Generic, Ord, Eq) + +isVertical Vertical{} = True +isVertical _ = False + +isHorizontal Horizontal{} = True +isHorizontal _ = False instance ToJSON Relation diff --git a/src/NITTA/Utils.hs b/src/NITTA/Utils.hs index ff766bd5a..9331e4145 100644 --- a/src/NITTA/Utils.hs +++ b/src/NITTA/Utils.hs @@ -29,6 +29,10 @@ module NITTA.Utils ( -- *Process inspection endpointAt, + getEndpoint, + getFunction, + getInstruction, + getCAD, getEndpoints, transferred, inputsPushedAt, @@ -36,6 +40,7 @@ module NITTA.Utils ( relatedEndpoints, isFB, getFBs, + isEndpoint, isInstruction, module NITTA.Utils.Base, ) where @@ -44,12 +49,12 @@ import Control.Monad.State (State, modify') import Data.Bits (setBit, testBit) import Data.List (sortOn) import Data.Maybe (isJust, mapMaybe) -import qualified Data.Set as S import qualified Data.String.Utils as S import qualified Data.Text as T import NITTA.Intermediate.Types import NITTA.Model.ProcessorUnits.Types import NITTA.Utils.Base +import NITTA.Utils.ProcessDescription import Numeric (readInt, showHex) import Numeric.Interval.NonEmpty (inf, sup, (...)) import qualified Numeric.Interval.NonEmpty as I @@ -113,9 +118,22 @@ getFB _ = Nothing getFBs p = mapMaybe getFB $ sortOn stepStart $ steps p +isEndpoint ep = isJust $ getEndpoint ep + getEndpoint Step{pDesc} | EndpointRoleStep role <- descent pDesc = Just role getEndpoint _ = Nothing +getFunction Step{pDesc} | FStep role <- descent pDesc = Just role +getFunction _ = Nothing + +isInstruction instr = isJust $ getInstruction instr + +getInstruction Step{pDesc} | role@(InstructionStep _) <- descent pDesc = Just role +getInstruction _ = Nothing + +getCAD Step{pDesc} | CADStep role <- descent pDesc = Just role +getCAD _ = Nothing + getEndpoints p = mapMaybe getEndpoint $ sortOn stepStart $ steps p transferred pu = unionsMap variables $ getEndpoints $ process pu @@ -126,15 +144,4 @@ stepsInterval ss = b = maximum $ map (sup . pInterval) ss in a ... b -relatedEndpoints process_ vs = - filter - ( \case - Step{pDesc = EndpointRoleStep role} -> not $ null (variables role `S.intersection` vs) - _ -> False - ) - $ steps process_ - -isInstruction (InstructionStep _) = True -isInstruction _ = False - stepStart Step{pInterval} = I.inf pInterval diff --git a/src/NITTA/Utils/ProcessDescription.hs b/src/NITTA/Utils/ProcessDescription.hs index cccb6601a..e04ef3b6f 100644 --- a/src/NITTA/Utils/ProcessDescription.hs +++ b/src/NITTA/Utils/ProcessDescription.hs @@ -1,4 +1,5 @@ {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE NamedFieldPuns #-} {- | @@ -25,19 +26,23 @@ module NITTA.Utils.ProcessDescription ( scheduleFunctionBind, scheduleFunctionRevoke, scheduleFunction, + scheduleFunctionFinish, scheduleInstruction, scheduleInstruction_, scheduleNestedStep, establishVerticalRelations, - establishVerticalRelation, + establishHorizontalRelations, getProcessSlice, + relatedEndpoints, castInstruction, updateTick, -- TODO: must be hidded ) where import Control.Monad.State import Data.Proxy (asProxyTypeOf) +import qualified Data.Set as S import Data.Typeable +import NITTA.Intermediate.Types import NITTA.Model.Problems import NITTA.Model.ProcessorUnits.Types import Numeric.Interval.NonEmpty (singleton) @@ -99,7 +104,7 @@ scheduleStep' mkStep = do return [nextUid] {- |Add to the process description information about vertical relations, which are defined by the - Cartesian product of high and low lists. +Cartesian product of high and low lists. -} establishVerticalRelations high low = do sch@Schedule{schProcess = p@Process{relations}} <- get @@ -111,14 +116,16 @@ establishVerticalRelations high low = do } } --- |Add to the process description information about vertical relation. -establishVerticalRelation h l = do +{- |Add to the process description information about horizontal relations (inside +level), which are defined by the Cartesian product of high and low lists. +-} +establishHorizontalRelations high low = do sch@Schedule{schProcess = p@Process{relations}} <- get put sch { schProcess = p - { relations = Vertical h l : relations + { relations = [Horizontal h l | h <- high, l <- low] ++ relations } } @@ -133,6 +140,16 @@ scheduleFunctionRevoke f = do -- |Add to the process description information about function evaluation. scheduleFunction ti f = scheduleStep ti $ FStep f +{- |Schedule function and establish vertical relations between bind step, +function step, and all related endpoints. +-} +scheduleFunctionFinish bPID function at = do + fPID <- scheduleFunction at function + establishVerticalRelations bPID fPID + process_ <- getProcessSlice + let low = map pID $ relatedEndpoints process_ $ variables function + establishVerticalRelations fPID low + {- |Add to the process description information about endpoint behaviour, and it's low-level implementation (on instruction level). Vertical relations connect endpoint level and instruction level steps. @@ -164,6 +181,14 @@ getProcessSlice = do Schedule{schProcess} <- get return schProcess +relatedEndpoints process_ vs = + filter + ( \case + Step{pDesc = EndpointRoleStep role} -> not $ null (variables role `S.intersection` vs) + _ -> False + ) + $ steps process_ + -- |Helper for instruction extraction from a rigid type variable. castInstruction :: (Typeable a, Typeable pu) => pu -> a -> Maybe (Instruction pu) castInstruction _pu i = cast i diff --git a/test/NITTA/Model/ProcessorUnits/Broken/Tests.hs b/test/NITTA/Model/ProcessorUnits/Broken/Tests.hs index 4e9e750a3..e4ca4665a 100644 --- a/test/NITTA/Model/ProcessorUnits/Broken/Tests.hs +++ b/test/NITTA/Model/ProcessorUnits/Broken/Tests.hs @@ -109,6 +109,42 @@ tests = , expectFail $ nittaCoSimTestCase "nittaCoSimTestCase lost source endpoint" (maBroken u{lostEndpointSource = True}) alg , expectFail $ typedLuaTestCase (maBroken def{lostEndpointSource = True}) pInt "typedLuaTestCase lost source endpoint" lua ] + , testGroup + "broken relations integrity check positive" + [ nittaCoSimTestCase "nittaCoSimTestCase positive test" (maBroken u) alg + , typedLuaTestCase (maBroken def) pInt "typedLuaTestCase positive test" lua + , puCoSimTestCase "puCoSimTestCase positive test" u [("a", 42)] [brokenBuffer "a" ["b"]] + , finitePUSynthesisProp "finitePUSynthesisProp relation positive test" u fsGen + , puCoSimProp "puCoSimProp relation positive test" u fsGen + ] + , testGroup + "broken relations integrity check negative base" + [ expectFail $ finitePUSynthesisProp "finitePUSynthesisProp lost instr and ep" u{lostInstructionRelation = True, lostEndpointRelation = True} fsGen + , expectFail $ finitePUSynthesisProp "finitePUSynthesisProp lost Endpoints" u{lostEndpointRelation = True} fsGen + , expectFail $ finitePUSynthesisProp "finitePUSynthesisProp lost Instruction" u{lostInstructionRelation = True} fsGen + , expectFail $ finitePUSynthesisProp "finitePUSynthesisProp lost Function" u{lostFunctionRelation = True} fsGen + , expectFail $ puCoSimProp "puCoSimProp lost Endpoints" u{lostEndpointRelation = True} fsGen + , expectFail $ puCoSimProp "puCoSimProp lost Instruction" u{lostInstructionRelation = True} fsGen + , expectFail $ puCoSimProp "puCoSimProp lost Function" u{lostFunctionRelation = True} fsGen + , expectFail $ puCoSimTestCase "puCoSimTestCase lost Endpoints" u{lostEndpointRelation = True} [("a", 42)] [brokenBuffer "a" ["b"]] + , expectFail $ puCoSimTestCase "puCoSimTestCase lost Instructions" u{lostInstructionRelation = True} [("a", 42)] [brokenBuffer "a" ["b"]] + , expectFail $ puCoSimTestCase "puCoSimTestCase lost Function" u{lostFunctionRelation = True} [("a", 42)] [brokenBuffer "a" ["b"]] + ] + , testGroup + "broken relations integrity check negative coSim" + -- nittaCoSimTestCase has isLeaf and isComplete, but Relation alright because of CAD + -- TODO: below cases ignores lost because of CAD steps and failed because simulation + [ expectFail $ nittaCoSimTestCase "nittaCoSimTestCase lost Endpoints" (maBroken u{lostEndpointRelation = True}) alg + , expectFail $ nittaCoSimTestCase "nittaCoSimTestCase lost Instruction" (maBroken u{lostInstructionRelation = True}) alg + , expectFail $ typedLuaTestCase (maBroken def{lostEndpointRelation = True}) pInt "typedLuaTestCase lost Endpoints" lua + , expectFail $ typedLuaTestCase (maBroken def{lostInstructionRelation = True}) pInt "typedLuaTestCase lost Instruction" lua + ] + , testGroup + "broken relations integrity check negative fails" + -- TODO: try lua function without break loop + [ expectFail $ nittaCoSimTestCase "nittaCoSimTestCase lost Function" (maBroken u{lostFunctionRelation = True}) alg + , expectFail $ typedLuaTestCase (maBroken def{lostFunctionRelation = True}) pInt "typedLuaTestCase lost Function" lua + ] ] where u = def :: Broken String Int Int diff --git a/test/NITTA/Model/ProcessorUnits/Tests/DSL.hs b/test/NITTA/Model/ProcessorUnits/Tests/DSL.hs index 80cd81b12..f8b625236 100644 --- a/test/NITTA/Model/ProcessorUnits/Tests/DSL.hs +++ b/test/NITTA/Model/ProcessorUnits/Tests/DSL.hs @@ -118,6 +118,7 @@ module NITTA.Model.ProcessorUnits.Tests.DSL ( assertBindFullness, assertCoSimulation, assertSynthesisDone, + assertConsistency, assertEndpoint, assertAllEndpointRoles, assertLocks, @@ -132,9 +133,11 @@ module NITTA.Model.ProcessorUnits.Tests.DSL ( import Control.Monad.Identity import Control.Monad.State.Lazy import Data.CallStack +import Data.Either import Data.List (find) import qualified Data.Set as S import NITTA.Intermediate.Types +import NITTA.Model.IntegrityCheck import NITTA.Model.Networks.Types (PUClasses) import NITTA.Model.Problems import NITTA.Model.ProcessorUnits @@ -317,6 +320,13 @@ assertSynthesisDone = do unless (isProcessComplete unit functs && null (endpointOptions unit)) $ lift $ assertFailure $ testName <> " Process is not done: " <> incompleteProcessMsg unit functs +assertConsistency :: ProcessConsistent pu => DSLStatement pu v x t () +assertConsistency = do + UnitTestState{unit, testName} <- get + let res = checkProcessСonsistent unit + when (isLeft res) $ + lift $ assertFailure $ testName <> " Process is not consistent: " <> show (fromLeft "no msg!" res) + assertLocks :: (Locks pu v) => [Lock v] -> DSLStatement pu v x t () assertLocks expectLocks = do UnitTestState{unit} <- get diff --git a/test/NITTA/Model/ProcessorUnits/Tests/Providers.hs b/test/NITTA/Model/ProcessorUnits/Tests/Providers.hs index 0ebcc8198..4bf47882c 100644 --- a/test/NITTA/Model/ProcessorUnits/Tests/Providers.hs +++ b/test/NITTA/Model/ProcessorUnits/Tests/Providers.hs @@ -34,10 +34,12 @@ import Control.Monad import Data.CallStack import Data.Data import Data.Default +import Data.Either (fromLeft, isLeft) import qualified Data.Text as T import NITTA.Intermediate.Functions import NITTA.Intermediate.Tests.Functions () import NITTA.Intermediate.Types +import NITTA.Model.IntegrityCheck import NITTA.Model.Networks.Types import NITTA.Model.Problems hiding (Bind, BreakLoop) import NITTA.Model.ProcessorUnits @@ -73,6 +75,7 @@ puCoSimTestCase name u cntxCycle alg = unitTestCase name u $ do assignsNaive alg cntxCycle decideNaiveSynthesis + assertConsistency assertCoSimulation -- *Properties @@ -81,9 +84,12 @@ puCoSimTestCase name u cntxCycle alg = finitePUSynthesisProp name pu0 fsGen = testProperty name $ do (pu, fs) <- processAlgOnEndpointGen pu0 fsGen - return $ - isProcessComplete pu fs - && null (endpointOptions pu) + case checkProcessСonsistent pu of + Left msg -> error msg + Right _ -> + return $ + isProcessComplete pu fs + && null (endpointOptions pu) {- |A computational process of functional (Haskell) and logical (Verilog) simulation should be identical for any correct algorithm. @@ -97,6 +103,8 @@ puCoSimProp name pu0 fsGen = run $ do unless (isProcessComplete pu fs) $ error $ "process is not complete: " <> incompleteProcessMsg pu fs + when (isLeft $ checkProcessСonsistent pu) $ + error $ fromLeft "Consistency check error" $ checkProcessСonsistent pu i <- incrCounter 1 externalTestCntr pwd <- getCurrentDirectory let pTargetProjectPath = "gen" (toModuleName name <> "_" <> show i)