From 78a513a8525b5edcc3b1bfc0715ce507f9bf1cd3 Mon Sep 17 00:00:00 2001
From: Neil Brown <neil@twistedsquare.com>
Date: Thu, 5 Jun 2008 23:10:30 +0000
Subject: [PATCH] Implemented addBK, at least for assignments

---
 checks/Check.hs                | 23 ++++++++++++++++++-----
 checks/UsageCheckAlgorithms.hs |  9 +--------
 2 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/checks/Check.hs b/checks/Check.hs
index 3d04439..9f2fe1d 100644
--- a/checks/Check.hs
+++ b/checks/Check.hs
@@ -53,20 +53,33 @@ usageCheckPass t = do g' <- buildFlowGraph labelUsageFunctions t
                         Map.empty of
                           Left err -> dieP emptyMeta $ "findReachDef: " ++
                             err
-                          Right g -> return g
+                          Right r -> return r
                       checkPar (nodeRep . snd)
                         (joinCheckParFunctions
                           checkArrayUsage
                           (checkPlainVarUsage . transformPair id (fmap snd)))
-                          $ nmap (addBK reach g) g
+                          $ labelMapWithNodeId (addBK reach g) g
                       checkParAssignUsage t
                       checkProcCallArgsUsage t
                       mapM_ (checkInitVar (findMeta t) g) roots
                       return t
 
-addBK :: Map.Map Node (Map.Map Var (Set.Set (Maybe A.Expression))) -> FlowGraph PassM UsageLabel -> FNode
-  PassM UsageLabel -> FNode PassM (BK, UsageLabel)
-addBK _ _ = fmap ((,) []) --TODO
+addBK :: Map.Map Node (Map.Map Var (Set.Set (Maybe A.Expression))) -> FlowGraph PassM UsageLabel ->
+  Node -> FNode PassM UsageLabel -> FNode PassM (BK, UsageLabel)
+addBK mp g nid n = fmap ((,) $ map Map.fromList $ productN values) n
+  where
+    nodeInQuestion :: Map.Map Var (Set.Set (Maybe A.Expression))
+    nodeInQuestion = fromMaybe Map.empty $ Map.lookup nid mp
+    
+    -- Each list (xs) in the whole thing (xss) relates to a different variable
+    -- Each item in a list xs is a different possible constraint on that variable
+    -- (effectively joined together by OR)
+    -- The items in the list of BackgroundKnowledge are joined together with
+    -- AND
+    values :: [[(Var, [BackgroundKnowledge])]]
+    values = [ [(Var v, maybeToList $ fmap (Equal $ A.ExprVariable (findMeta v)
+      v) val)  | val <- Set.toList vals]
+             | (Var v, vals) <- Map.toList nodeInQuestion]
 
 
 filterPlain :: Set.Set Var -> Set.Set Var
diff --git a/checks/UsageCheckAlgorithms.hs b/checks/UsageCheckAlgorithms.hs
index 5f22a44..efb5bb3 100644
--- a/checks/UsageCheckAlgorithms.hs
+++ b/checks/UsageCheckAlgorithms.hs
@@ -134,8 +134,7 @@ findReachDef :: forall m. Monad m => FlowGraph m UsageLabel -> Node -> Either St
 findReachDef graph startNode
   = do r <- flowAlgorithm graphFuncs (udfs [startNode] graph) (startNode, Map.empty)
        -- These lines remove the maps where the variable is not read in that particular node:
-       let r' = Map.mapWithKey (\n -> Map.filterWithKey (readInNode' n)) r
-       return $ Map.filter (not . Map.null) r'
+       return $ Map.filter (not . Map.null) r
   where
     graphFuncs :: GraphFuncs Node EdgeLabel (Map.Map Var (Set.Set (Maybe A.Expression)))
     graphFuncs = GF
@@ -147,12 +146,6 @@ findReachDef graph startNode
         ,userErrLabel = ("for node at: " ++) . show . fmap getNodeMeta . lab graph
       }
 
-    readInNode' :: Node -> Var -> a -> Bool
-    readInNode' n v _ = readInNode v (lab graph n)
-
-    readInNode :: Var -> Maybe (FNode m UsageLabel) -> Bool
-    readInNode v (Just nd) = (Set.member v . readVars . nodeVars) (getNodeData nd)
-    
     writeNode :: FNode m UsageLabel -> Map.Map Var (Maybe A.Expression)
     writeNode nd = writtenVars $ nodeVars $ getNodeData nd