From ed43b750c151d4c5d402d42e775a098880664619 Mon Sep 17 00:00:00 2001 From: Neil Brown Date: Tue, 11 Dec 2007 16:54:36 +0000 Subject: [PATCH] Added an initial messy implementation of the equality part of the Omega test --- Makefile.am | 2 +- transformations/ArrayUsageCheck.hs | 177 ++++++++++++++++++++++++++ transformations/RainUsageCheckTest.hs | 19 +++ 3 files changed, 197 insertions(+), 1 deletion(-) create mode 100644 transformations/ArrayUsageCheck.hs diff --git a/Makefile.am b/Makefile.am index a6e5b24..f232d96 100644 --- a/Makefile.am +++ b/Makefile.am @@ -53,7 +53,7 @@ CLEANFILES = $(BUILT_SOURCES) tock_SOURCES_hs = transformations/SimplifyExprs.hs transformations/SimplifyTypes.hs tock_SOURCES_hs += transformations/Unnest.hs transformations/RainUsageCheck.hs transformations/SimplifyProcs.hs -tock_SOURCES_hs += transformations/SimplifyComms.hs +tock_SOURCES_hs += transformations/SimplifyComms.hs transformations/ArrayUsageCheck.hs tock_SOURCES_hs += frontends/PreprocessOccam.hs frontends/ParseRain.hs frontends/StructureOccam.hs tock_SOURCES_hs += frontends/ParseOccam.hs frontends/RainTypes.hs frontends/RainPasses.hs frontends/ParseUtils.hs tock_SOURCES_hs += common/Pass.hs common/TreeUtil.hs common/Intrinsics.hs common/EvalLiterals.hs diff --git a/transformations/ArrayUsageCheck.hs b/transformations/ArrayUsageCheck.hs new file mode 100644 index 0000000..5e3dc0b --- /dev/null +++ b/transformations/ArrayUsageCheck.hs @@ -0,0 +1,177 @@ +{- +Tock: a compiler for parallel languages +Copyright (C) 2007 University of Kent + +This program is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation, either version 2 of the License, or (at your +option) any later version. + +This program is distributed in the hope that it will be useful, but +WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +General Public License for more details. + +You should have received a copy of the GNU General Public License along +with this program. If not, see . +-} + +module ArrayUsageCheck where + +import Control.Monad.State +import Data.Array.IArray +import Data.List +import Data.Maybe + +import qualified AST as A +import FlowGraph +import Utils + +--TODO fix this tangle of code to make it work with the code at the bottom of the file + +data Constraint = Equality [CoeffVar] Integer + +type Problem = [Constraint] + +data CoeffVar = CV { coeff :: Integer, var :: A.Variable } + +type CoeffExpr = [CoeffVar] + +--type IndicesUsed = Map.Map Variable [[ + +makeProblems :: [[CoeffExpr]] -> [Problem] +makeProblems indexLists = map checkEq zippedPairs + where + allPairs :: [([CoeffExpr],[CoeffExpr])] + allPairs = [(a,b) | a <- indexLists, b <- indexLists] + zippedPairs :: [[(CoeffExpr,CoeffExpr)]] + zippedPairs = map (uncurry zip) allPairs + + checkEq :: [(CoeffExpr,CoeffExpr)] -> Problem + checkEq = map checkEq' + + checkEq' :: (CoeffExpr, CoeffExpr) -> Constraint + checkEq' (cv0,cv1) = Equality (cv0 ++ map negate cv1) 0 + + negate :: CoeffVar -> CoeffVar + negate cv = cv {coeff = - (coeff cv)} + +makeProblem1Dim :: [CoeffExpr] -> [Problem] +makeProblem1Dim ces = makeProblems [[c] | c <- ces] + +type CoeffIndex = Int +type EqualityConstraintEquation = Array CoeffIndex Integer +type EqualityProblem = [EqualityConstraintEquation] + +-- Assumed to be >= 0 +type InequalityConstraintEquation = Array CoeffIndex Integer +type InequalityProblem = [InequalityConstraintEquation] + +type StIneq = State InequalityProblem + +solveConstraints :: EqualityProblem -> InequalityProblem -> Maybe InequalityProblem +solveConstraints p ineq + = case normalise p of + Nothing -> Nothing + Just p' -> case (runState (solve p') ineq) of + (Nothing,_) -> Nothing + (_,s) -> Just s + where + normalise :: EqualityProblem -> Maybe EqualityProblem + normalise = mapM normalise' --Note the mapM; if any calls to normalise' fail, so will normalise + where + normalise' :: EqualityConstraintEquation -> Maybe EqualityConstraintEquation + normalise' e = let g = foldl1 gcd (elems e) in + if (((e ! 0) `mod` g) /= 0) then Nothing else Just $ amap (\x -> x `div` g) e + + solve :: EqualityProblem -> StIneq (Maybe EqualityProblem) + solve [] = return $ Just [] + solve p = do mp <- solveUnits p >>* (checkFalsifiable . removeRedundant) + case mp of + Nothing -> return Nothing + Just p' -> solveNext p' >>= solve + + checkForUnit :: EqualityConstraintEquation -> Maybe CoeffIndex +-- checkForUnit [_] = Nothing +-- checkForUnit is = listToMaybe $ map fst $ filter (absVal1 . snd) $ zip [1..] (tail is) -- Use [1..] because we've chopped off the 0-index value + checkForUnit = listToMaybe . map fst . filter (absVal1 . snd) . tail . assocs + + + absVal1 :: Integer -> Bool + absVal1 1 = True + absVal1 (-1) = True + absVal1 _ = False + + + findFirstUnit :: EqualityProblem -> (Maybe (EqualityConstraintEquation,CoeffIndex),EqualityProblem) + findFirstUnit [] = (Nothing,[]) + findFirstUnit (e:es) = case checkForUnit e of + Just ci -> (Just (e,ci),es) + Nothing -> let (me,es') = findFirstUnit es in (me,e:es') + + + substIn :: CoeffIndex -> Array CoeffIndex Integer -> EqualityProblem -> EqualityProblem + substIn ind arr = map substIn' + where + substIn' eq = changeAllButOneDifferent (ind,0) id $ arrayZipWith (+) eq (amap (* (eq ! ind)) arr) + + solveUnits :: EqualityProblem -> StIneq EqualityProblem + solveUnits p = case findFirstUnit p of + (Nothing,p') -> return p' -- p' should equal p anyway + (Just (eq,ind),p') -> modify change >> solveUnits (change p') + where + change = substIn ind (arrayMapWithIndex (curry $ negateOthers ind) eq) + -- ata x = addToAll x $ arrayMapWithIndex (curry $ negateOthers ind) eq + + negateOthers :: CoeffIndex -> (CoeffIndex,Integer) -> Integer + negateOthers match (ind,val) = if match == ind then 0 else negate val + + findSmallestAbsCoeff :: EqualityConstraintEquation -> CoeffIndex + findSmallestAbsCoeff = fst. minimumBy (cmpAbsSnd) . tail . assocs + where + cmpAbsSnd :: (a,Integer) -> (a,Integer) -> Ordering + cmpAbsSnd (_,x) (_,y) = compare (abs x) (abs y) + + solveNext :: EqualityProblem -> StIneq EqualityProblem + solveNext [] = return [] + solveNext (e:es) = -- We transform the kth variable into sigma, effectively + -- So a_k becomes -|a_k|, and all other constraints are transformed appropriately + modify (map change) >> return (map change (e:es)) + where + change = changeAllButOneDifferent (k,-(abs a_k)) transform + + k = findSmallestAbsCoeff e + a_k = e ! k + m = (abs a_k) + 1 + + transform :: Integer -> Integer + transform a_i = (floordivplushalf a_i m) + (mymod a_i m) + + -- I think this is probably equivalent to mod, but let's follow the maths: + mymod x y = x - (y * (floordivplushalf x y)) + + -- This is floor (x/y + 1/2). Probably a way to do it without reverting to float arithmetic: + floordivplushalf :: Integer -> Integer -> Integer + floordivplushalf x y = floor ((fromInteger x / fromInteger y) + 0.5) + + changeAllButOneDifferent :: (IArray a e, IArray a e', Ix i) => (i,e') -> (e -> e') -> a i e -> a i e' + changeAllButOneDifferent (specialI,specialE) f = arrayMapWithIndex f' + where + f' i e = if i == specialI then specialE else f e + + -- Removes all equations where the coefficients are all zero + removeRedundant :: EqualityProblem -> EqualityProblem + removeRedundant = mapMaybe (boolToMaybe (not . isRedundant)) + where + isRedundant :: EqualityConstraintEquation -> Bool + isRedundant = all (== 0) . elems + + + -- Searches for all equations where only the a_0 coefficient is non-zero; this means the equation cannot be satisfied + checkFalsifiable :: EqualityProblem -> Maybe EqualityProblem + checkFalsifiable = boolToMaybe (not . any checkFalsifiable') + where + -- | Returns True if the equation is definitely unsatisfiable + checkFalsifiable' :: EqualityConstraintEquation -> Bool + checkFalsifiable' e = (e ! 0 /= 0) && (all (== 0) . tail . elems) e + diff --git a/transformations/RainUsageCheckTest.hs b/transformations/RainUsageCheckTest.hs index a65055c..832f721 100644 --- a/transformations/RainUsageCheckTest.hs +++ b/transformations/RainUsageCheckTest.hs @@ -26,6 +26,7 @@ import Prelude hiding (fail) import Test.HUnit +import ArrayUsageCheck import qualified AST as A import FlowGraph import Metadata @@ -294,6 +295,23 @@ testReachDef = TestList fst3 :: (a,b,c) -> a fst3(x,_,_) = x +testArrayCheck :: Test +testArrayCheck = TestList + [ + -- x_1 = 0 + TestCase $ assertEqual "testArrayCheck 0" (Just []) (solveConstraints [simpleArray [(0,0),(1,1)]] []) + -- x_1 = 0, 3x_1 >= 0 + ,TestCase $ assertEqual "testArrayCheck 0a" (Just [simpleArray [(0,0),(1,0)]]) (solveConstraints [simpleArray [(0,0),(1,1)]] [simpleArray [(0,0),(1,3)]]) + -- x_1 = 7 + ,TestCase $ assertEqual "testArrayCheck 1" (Just []) (solveConstraints [simpleArray [(0,-7),(1,1)]] []) + -- -7 = 0 + ,TestCase $ assertEqual "testArrayCheck 2" (Nothing) (solveConstraints [simpleArray [(0,7),(1,0)]] []) + -- x_1 = 3, x_1 = 4 + ,TestCase $ assertEqual "testArrayCheck 3" (Nothing) (solveConstraints [simpleArray [(0,-3),(1,1)], simpleArray [(0,-4),(1,1)]] []) + -- x_1 + x_2 = 0, x_1 + x_2 = -3 + ,TestCase $ assertEqual "testArrayCheck 4" (Nothing) (solveConstraints [simpleArray [(0,0),(1,1),(2,1)], simpleArray [(0,3),(1,1),(2,1)]] []) + ] + tests :: Test tests = TestList @@ -302,6 +320,7 @@ tests = TestList ,testInitVar -- ,testParUsageCheck ,testReachDef + ,testArrayCheck ]