Added support for using the constraints in the background knowledge for the usage checking
This commit is contained in:
parent
2a56189d30
commit
e39ebf5962
|
@ -55,23 +55,51 @@ usageCheckPass t = do g' <- buildFlowGraph labelUsageFunctions t
|
||||||
Left err -> dieP emptyMeta $ "findReachDef: " ++
|
Left err -> dieP emptyMeta $ "findReachDef: " ++
|
||||||
err
|
err
|
||||||
Right r -> return r
|
Right r -> return r
|
||||||
|
cons <- case mapM (findConstraints g) roots
|
||||||
|
>>* foldl Map.union Map.empty of
|
||||||
|
Left err -> dieP emptyMeta $ "findConstraints:"
|
||||||
|
++ err
|
||||||
|
Right c -> return c
|
||||||
checkPar (nodeRep . snd)
|
checkPar (nodeRep . snd)
|
||||||
(joinCheckParFunctions
|
(joinCheckParFunctions
|
||||||
checkArrayUsage
|
checkArrayUsage
|
||||||
(checkPlainVarUsage . transformPair id (fmap snd)))
|
(checkPlainVarUsage . transformPair id (fmap snd)))
|
||||||
$ labelMapWithNodeId (addBK reach g) g
|
$ labelMapWithNodeId (addBK reach cons g) g
|
||||||
checkParAssignUsage t
|
checkParAssignUsage t
|
||||||
checkProcCallArgsUsage t
|
checkProcCallArgsUsage t
|
||||||
mapM_ (checkInitVar (findMeta t) g) roots
|
mapM_ (checkInitVar (findMeta t) g) roots
|
||||||
return t
|
return t
|
||||||
|
|
||||||
addBK :: Map.Map Node (Map.Map Var (Set.Set (Maybe A.Expression))) -> FlowGraph PassM UsageLabel ->
|
addBK :: Map.Map Node (Map.Map Var (Set.Set (Maybe A.Expression))) ->
|
||||||
|
Map.Map Node [A.Expression] -> FlowGraph PassM UsageLabel ->
|
||||||
Node -> FNode PassM UsageLabel -> FNode PassM (BK, UsageLabel)
|
Node -> FNode PassM UsageLabel -> FNode PassM (BK, UsageLabel)
|
||||||
addBK mp g nid n = fmap ((,) $ (map Map.fromList $ productN $ repBK ++ values)) n
|
addBK mp mp2 g nid n = fmap ((,) $ (map Map.fromList $ productN $ conBK ++
|
||||||
|
repBK ++ values)) n
|
||||||
where
|
where
|
||||||
nodeInQuestion :: Map.Map Var (Set.Set (Maybe A.Expression))
|
nodeInQuestion :: Map.Map Var (Set.Set (Maybe A.Expression))
|
||||||
nodeInQuestion = fromMaybe Map.empty $ Map.lookup nid mp
|
nodeInQuestion = fromMaybe Map.empty $ Map.lookup nid mp
|
||||||
|
|
||||||
|
consInQuestion :: [A.Expression]
|
||||||
|
consInQuestion = fromMaybe [] $ Map.lookup nid mp2
|
||||||
|
|
||||||
|
conInterMed :: [([Var], [BackgroundKnowledge])]
|
||||||
|
conInterMed = map f consInQuestion
|
||||||
|
where
|
||||||
|
f :: A.Expression -> ([Var], [BackgroundKnowledge])
|
||||||
|
f e = (map Var $ listify (const True) e, g e)
|
||||||
|
|
||||||
|
g :: A.Expression -> [BackgroundKnowledge]
|
||||||
|
g (A.Dyadic _ op lhs rhs)
|
||||||
|
| op == A.And = g lhs ++ g rhs
|
||||||
|
| op == A.Eq = [Equal lhs rhs]
|
||||||
|
| op == A.LessEq = [LessThanOrEqual lhs rhs]
|
||||||
|
| op == A.MoreEq = [LessThanOrEqual rhs lhs]
|
||||||
|
g _ = []
|
||||||
|
|
||||||
|
conBK :: [[(Var, [BackgroundKnowledge])]]
|
||||||
|
conBK = [ [(v, concatMap snd $ filter (elem v . fst) conInterMed)]
|
||||||
|
| v <- nub $ concatMap fst conInterMed]
|
||||||
|
|
||||||
-- Each list (xs) in the whole thing (xss) relates to a different variable
|
-- 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
|
-- Each item in a list xs is a different possible constraint on that variable
|
||||||
-- (effectively joined together by OR)
|
-- (effectively joined together by OR)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user