From 423d22fa13c11a4a3c1e381522de6ebc403d02fd Mon Sep 17 00:00:00 2001 From: Neil Brown Date: Sun, 16 Dec 2007 14:02:45 +0000 Subject: [PATCH] Moved the ArrayUsageCheck tests to their own new file (ArrayUsageCheckTest) --- Makefile.am | 1 + TestMain.hs | 10 +- transformations/ArrayUsageCheckTest.hs | 449 +++++++++++++++++++++++++ transformations/RainUsageCheckTest.hs | 413 +---------------------- 4 files changed, 460 insertions(+), 413 deletions(-) create mode 100644 transformations/ArrayUsageCheckTest.hs diff --git a/Makefile.am b/Makefile.am index e71ff24..92cff7a 100644 --- a/Makefile.am +++ b/Makefile.am @@ -70,6 +70,7 @@ tock_SOURCES = $(tock_SOURCES_hs) frontends/LexOccam.x frontends/LexRain.x tocktest_SOURCES = $(tock_SOURCES) tocktest_SOURCES += transformations/PassTest.hs transformations/RainUsageCheckTest.hs +tocktest_SOURCES += transformations/ArrayUsageCheckTest.hs tocktest_SOURCES += backends/GenerateCTest.hs backends/BackendPassesTest.hs tocktest_SOURCES += common/TestUtils.hs common/CommonTest.hs common/FlowGraphTest.hs tocktest_SOURCES += frontends/ParseRainTest.hs frontends/RainPassesTest.hs frontends/RainTypesTest.hs diff --git a/TestMain.hs b/TestMain.hs index 25bd49a..538b6a3 100644 --- a/TestMain.hs +++ b/TestMain.hs @@ -18,6 +18,8 @@ with this program. If not, see . -- | A module containing the 'main' function for the Tock test suite. It currently runs tests from the following modules: -- +-- * "ArrayUsageCheckTest" +-- -- * "BackendPassesTest" -- -- * "CommonTest" @@ -41,6 +43,7 @@ import System.Console.GetOpt import System.Environment import Test.HUnit +import qualified ArrayUsageCheckTest (qcTests) import qualified BackendPassesTest (tests) import qualified CommonTest (tests) import qualified FlowGraphTest (qcTests) @@ -49,7 +52,7 @@ import qualified ParseRainTest (tests) import qualified PassTest (tests) import qualified RainPassesTest (tests) import qualified RainTypesTest (tests) -import qualified RainUsageCheckTest (qcTests) +import qualified RainUsageCheckTest (tests) import TestUtils import Utils @@ -88,7 +91,8 @@ main = do opts <- getArgs >>* getOpt RequireOrder options qcTests = concatMap snd tests tests = [ - noqc BackendPassesTest.tests + ArrayUsageCheckTest.qcTests + ,noqc BackendPassesTest.tests ,noqc CommonTest.tests ,FlowGraphTest.qcTests ,noqc GenerateCTest.tests @@ -96,7 +100,7 @@ main = do opts <- getArgs >>* getOpt RequireOrder options ,noqc PassTest.tests ,noqc RainPassesTest.tests ,noqc RainTypesTest.tests - ,RainUsageCheckTest.qcTests + ,noqc RainUsageCheckTest.tests ] noqc :: Test -> (Test, [QuickCheckTest]) diff --git a/transformations/ArrayUsageCheckTest.hs b/transformations/ArrayUsageCheckTest.hs new file mode 100644 index 0000000..161f0a2 --- /dev/null +++ b/transformations/ArrayUsageCheckTest.hs @@ -0,0 +1,449 @@ +{- +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 ArrayUsageCheckTest (qcTests) where + +import Control.Monad.Identity +import Data.Array.IArray +import Data.List +import qualified Data.Map as Map +import Data.Maybe +import Prelude hiding ((**),fail) +import Test.HUnit +import Test.QuickCheck + + +import ArrayUsageCheck +import PrettyShow +import TestUtils hiding (m) +import Utils + +testArrayCheck :: Test +testArrayCheck = TestList + [ + -- x_1 = 0 + pass (0, [], [[0,1]], []) + -- x_1 = 0, 3x_1 >= 0 --> 0 >= 0 + ,pass (1, [[0,0]], [[0,1]], [[0,3]]) + -- -7 + x_1 = 0 + ,pass (2, [], [[-7,1]], []) + -- x_1 = 9, 3 + 2x_1 >= 0 --> 21 >= 0 + ,pass (3, [[21,0]], [[-9,1]], [[3,2]]) + -- x_1 + x_2 = 0, 4x_1 = 8, 2x_2 = -4 + ,pass (4, [], [[0,1,1], [-8,4,0], [4,0,2]], []) + -- - x_1 + x_2 = 0, 4x_1 = 8, 2x_2 = 4 + ,pass (5, [], [[0,-1,1], [-8,4,0], [-4,0,2]], []) + -- -x_1 = -9, 3 + 2x_1 >= 0 --> 21 >= 0 + ,pass (6, [[21,0]], [[9,-1]], [[3,2]]) + + + -- From the Omega Test paper (x = x_1, y = x_2, z = x_3, sigma = x_1 (effectively)): + ,pass (100, [[11,13,0,0], [28,-13,0,0], [47,-5,0,0], [53,5,0,0]], [[-17,7,12,31], [-7,3,5,14]], + [[-1,1,0,0], [40,-1,0,0], [50,0,1,0], [50,0,-1,0]]) + + -- Impossible/inconsistent equality constraints: + + -- -7 = 0 + ,TestCase $ assertEqual "testArrayCheck 1002" (Nothing) (solveConstraints' [simpleArray [(0,7),(1,0)]] []) + -- x_1 = 3, x_1 = 4 + ,TestCase $ assertEqual "testArrayCheck 1003" (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 1004" (Nothing) (solveConstraints' [simpleArray [(0,0),(1,1),(2,1)], simpleArray [(0,3),(1,1),(2,1)]] []) + -- 4x_1 = 7 + ,TestCase $ assertEqual "testArrayCheck 1005" (Nothing) (solveConstraints' [simpleArray [(0,-7),(1,4)]] []) + ] + where + solveConstraints' = solveConstraints undefined + + pass :: (Int, [[Integer]], [[Integer]], [[Integer]]) -> Test + pass (ind, expIneq, inpEq, inpIneq) = TestCase $ assertEqual ("testArrayCheck " ++ show ind) + (Just $ map arrayise expIneq) (transformMaybe snd $ solveConstraints' (map arrayise inpEq) (map arrayise inpIneq)) + +arrayise :: [Integer] -> Array Int Integer +arrayise = simpleArray . zip [0..] + +-- Various helpers for easily creating equations. +-- Rules for writing equations: +-- * You must use the variables i, j, k in that order as you need them. +-- Never write an equation just involving i and k, or j and k. Always +-- use (i), (i and j), or (i and j and k). +-- * Constant scaling must always be on the left, and does not need the con +-- function. con 1 ** i won't compile. + +-- Useful to make sure the equation types are not mixed up: +newtype HandyEq = Eq [(Int, Integer)] deriving (Show, Eq) +newtype HandyIneq = Ineq [(Int, Integer)] deriving (Show, Eq) + +-- | The constraint for an arbitrary i,j that exist between low and high (inclusive) +-- and where i and j are distinct and i is taken to be the lower index. +i_j_constraint :: Integer -> Integer -> [HandyIneq] +i_j_constraint low high = [con low <== i, i ++ con 1 <== j, j <== con high] + +-- The easy way of writing equations is built on the following Haskell magic. +-- Essentially, everything is a list of (index, coefficient). You can scale +-- with the ** operator, and you can form equalities and inequalities with +-- the ===, <== and >== operators. The type system saves you from doing anything +-- nonsensical. The other neat thing is that + is ++. An &&& operator is defined +-- for combining inequality lists. + +leq :: [[(Int,Integer)]] -> [HandyIneq] +leq [] = [] +leq [_] = [] +leq (x:y:zs) = (x <== y) : (leq (y:zs)) + +(&&&) :: [HandyIneq] -> [HandyIneq] -> [HandyIneq] +(&&&) = (++) + +infixr 4 === +infixr 4 <== +infixr 4 >== +infix 6 ** + +(===) :: [(Int,Integer)] -> [(Int,Integer)] -> HandyEq +lhs === rhs = Eq $ lhs ++ negateVars rhs +(<==) :: [(Int,Integer)] -> [(Int,Integer)] -> HandyIneq +lhs <== rhs = Ineq $ negateVars lhs ++ rhs +(>==) :: [(Int,Integer)] -> [(Int,Integer)] -> HandyIneq +lhs >== rhs = Ineq $ lhs ++ negateVars rhs +negateVars :: [(Int,Integer)] -> [(Int,Integer)] +negateVars = map (transformPair id negate) +(**) :: Integer -> [(Int,Integer)] -> [(Int,Integer)] +n ** var = map (transformPair id (* n)) var +con :: Integer -> [(Int,Integer)] +con c = [(0,c)] +i,j,k,m,n,p :: [(Int, Integer)] +i = [(1,1)] +j = [(2,1)] +k = [(3,1)] +m = [(4,1)] +n = [(5,1)] +p = [(6,1)] + + +testIndexes :: Test +testIndexes = TestList + [ + + easilySolved (0, [i === con 7], []) + ,easilySolved (1, [2 ** i === con 12], []) + --should fail: + ,notSolveable (2, [i === con 7],[i <== con 5]) + + -- Can i = j? + ,notSolveable (3, [i === j], i_j_constraint 0 9) + + -- TODO need to run the below exampls on a better test (they are not "easily" solved): + + -- Can (j + 1 % 10 == i + 1 % 10)? + ,neverSolveable $ withKIsMod (i ++ con 1) 10 $ withNIsMod (j ++ con 1) 10 $ (4, [k === n], i_j_constraint 0 9) + -- Off by one (i + 1 % 9) + ,hardSolved $ withKIsMod (i ++ con 1) 9 $ withNIsMod (j ++ con 1) 9 $ (5, [k === n], i_j_constraint 0 9) + + -- The "nightmare" example from the Omega Test paper: + ,neverSolveable (6,[],leq [con 27, 11 ** i ++ 13 ** j, con 45] &&& leq [con (-10), 7 ** i ++ (-9) ** j, con 4]) + + ,safeParTest 100 True (0,10) [i] + ,safeParTest 120 False (0,10) [i,i ++ con 1] + ,safeParTest 140 True (0,10) [2 ** i, 2 ** i ++ con 1] + + + --TODO tidy up the tests and add this example that once failed the QuickCheck tests: + + --OMI ([array (0,3) [(0,0),(1,-1),(2,0),(3,0)],array (0,3) [(0,5),(1,0),(2,-1),(3,0)],array (0,3) [(0,4),(1,0),(2,0),(3,-1)]],([array (0,3) [(0,-32),(1,4),(2,4),(3,3)],array (0,3) [(0,-17),(1,1),(2,1),(3,3)],array (0,3) [(0,-54),(1,10),(2,10),(3,1)]],[array (0,3) [(0,-60),(1,3),(2,8),(3,5)],array (0,3) [(0,-60),(1,9),(2,4),(3,10)],array (0,3) [(0,-25),(1,5),(2,1),(3,5)]])) + + ,TestCase $ assertStuff "testIndexes makeEq" + (Right (Map.empty,(uncurry makeConsistent) (doubleEq [con 0 === con 1],leq [con 0,con 0,con 7] &&& leq [con 0,con 1,con 7]))) $ + makeEquations [intLiteral 0, intLiteral 1] (intLiteral 7) + ,TestCase $ assertStuff "testIndexes makeEq 2" + (Right (Map.singleton "i" 1,(uncurry makeConsistent) (doubleEq [i === con 3],leq [con 0,con 3,con 7] &&& leq [con 0,i,con 7]))) $ + makeEquations [exprVariable "i",intLiteral 3] (intLiteral 7) + + ,TestCase $ assertCounterExampleIs "testIndexes testVarMapping" (Map.fromList [(1,7)]) + $ makeConsistent [i === con 7] [] + ] + where + -- TODO comment these functions and rename the latter one + doubleEq = concatMap (\(Eq e) -> [Eq e,Eq $ negateVars e]) + assertStuff title x y = assertEqual title (munge x) (munge y) + where + munge = transformEither id (transformPair id (transformPair sort sort)) + + assertCounterExampleIs title counterEq (eq,ineq) + = assertCompareCustom title equivEq (Just counterEq) ((solveAndPrune eq ineq) >>* (getCounterEqs . fst)) + where + equivEq (Just xs) (Just ys) = xs == ys + equivEq Nothing Nothing = True + equivEq _ _ = False + + + -- Given some indexes using "i", this function checks whether these can + -- ever overlap within the bounds given, and matches this against + -- the expected value; True for safe, False for unsafe. + safeParTest :: Int -> Bool -> (Integer,Integer) -> [[(Int,Integer)]] -> Test + safeParTest ind expSafe (low, high) usesI = TestCase $ + (if expSafe + then assertEqual ("testIndexes " ++ show ind ++ " should be safe (unsolveable)") [] + else assertNotEqual ("testIndexes " ++ show ind ++ " should be solveable") [] + ) + $ findSolveable $ zip3 [ind..] (equalityCombinations) (repeat constraint) + where + changeItoJ (1,n) = (2,n) + changeItoJ x = x + + usesJ = map (map changeItoJ) usesI + + constraint = i_j_constraint low high + + equalityCombinations :: [[HandyEq]] + equalityCombinations = map (\(lhs,rhs) -> [lhs === rhs]) $ product2 (usesI,usesJ) + + + --TODO clear up this mess of easilySolved/hardSolved helper functions + + findSolveable :: [(Int, [HandyEq], [HandyIneq])] -> [(Int, [HandyEq], [HandyIneq])] + findSolveable = filter isSolveable + + isSolveable :: (Int, [HandyEq], [HandyIneq]) -> Bool + isSolveable (ind, eq, ineq) = isJust $ (uncurry solveAndPrune) (makeConsistent eq ineq) + + easilySolved :: (Int, [HandyEq], [HandyIneq]) -> Test + easilySolved (ind, eq, ineq) = TestCase $ + let ineq' = (uncurry solveAndPrune) (makeConsistent eq ineq) in + case ineq' of + Nothing -> assertFailure $ "testIndexes " ++ show ind ++ " expected to pass (solving+pruning) but failed; problem: " ++ show (eq,ineq) + Just (_,ineq'') -> + if numVariables ineq'' <= 1 + then return () + -- Until we put in the route from original to mapped variables, + -- we can't give a useful test failure here: + else assertFailure $ "testIndexes " ++ show ind ++ " more than one variable left after solving" + + hardSolved :: (Int, [HandyEq], [HandyIneq]) -> Test + hardSolved (ind, eq, ineq) = TestCase $ + assertBool ("testIndexes " ++ show ind) $ isJust $ + (transformMaybe snd . uncurry solveAndPrune) (makeConsistent eq ineq) >>= (pruneAndCheck . fmElimination) + + notSolveable :: (Int, [HandyEq], [HandyIneq]) -> Test + notSolveable (ind, eq, ineq) = TestCase $ assertEqual ("testIndexes " ++ show ind) Nothing $ + (transformMaybe snd . uncurry solveAndPrune) (makeConsistent eq ineq) >>* ((<= 1) . numVariables) + + + neverSolveable :: (Int, [HandyEq], [HandyIneq]) -> Test + neverSolveable (ind, eq, ineq) = TestCase $ assertEqual ("testIndexes " ++ show ind) Nothing $ + (transformMaybe snd . uncurry solveAndPrune) (makeConsistent eq ineq) >>= (pruneAndCheck . fmElimination) + + + isMod :: [(Int,Integer)] -> [(Int,Integer)] -> Integer -> ([HandyEq], [HandyIneq]) + isMod var@[(ind,1)] alpha divisor = ([alpha_minus_div_sigma === var], leq [con 0, alpha_minus_div_sigma, con $ divisor - 1]) + where + alpha_minus_div_sigma = alpha ++ (negate divisor) ** sigma + sigma = [(ind+1,1)] + + -- | Adds both k and m to the equation! + withKIsMod :: [(Int,Integer)] -> Integer -> (Int, [HandyEq], [HandyIneq]) -> (Int, [HandyEq], [HandyIneq]) + withKIsMod alpha divisor (ind,eq,ineq) = let (eq',ineq') = isMod k alpha divisor in (ind,eq ++ eq',ineq ++ ineq') + + -- | Adds both n and p to the equation! + withNIsMod :: [(Int,Integer)] -> Integer -> (Int, [HandyEq], [HandyIneq]) -> (Int, [HandyEq], [HandyIneq]) + withNIsMod alpha divisor (ind,eq,ineq) = let (eq',ineq') = isMod n alpha divisor in (ind,eq ++ eq',ineq ++ ineq') + + makeConsistent :: [HandyEq] -> [HandyIneq] -> (EqualityProblem, InequalityProblem) + makeConsistent eqs ineqs = (map ensure eqs', map ensure ineqs') + where + eqs' = map (\(Eq e) -> e) eqs + ineqs' = map (\(Ineq e) -> e) ineqs + + ensure = accumArray (+) 0 (0, largestIndex) + largestIndex = maximum $ map (maximum . map fst) $ eqs' ++ ineqs' + +-- QuickCheck tests for Omega Test: +-- The idea is to begin with a random list of integers, representing transformed y_i variables. +-- This will be the solution. Feed this into a random list of inequalities. The inequalities do +-- not have to be true; they merely have to exist. Then slowly transform + + +--TODO Allow zero coefficients (but be careful we don't +-- produce unsolveable equations, e.g. where an equation is all zeroes, or a_3 is zero in all of them) + +-- | Generates a list of random numbers of the given size, where the numbers are all co-prime. +-- This is so they can be used as normalised coefficients in a linear equation +coprimeList :: Int -> Gen [Integer] +coprimeList size = do non_normal <- replicateM size $ oneof [choose (-100,-1), choose (1,100)] + return $ map (\x -> x `div` (mygcdList non_normal)) non_normal + +-- | Generates a list of lists of co-prime numbers, where each list is distinct. +-- The returned list of lists will be square; N equations, each with N items +distinctCoprimeLists :: Int -> Gen [[Integer]] +distinctCoprimeLists size = distinctCoprimeLists' [] size + where + -- n is the number left to generate; size is still the "width" of the lists + distinctCoprimeLists' :: [[Integer]] -> Int -> Gen [[Integer]] + distinctCoprimeLists' result 0 = return result + distinctCoprimeLists' soFar n = do next <- coprimeList size + if (next `elem` soFar) + then distinctCoprimeLists' soFar n -- Try again + else distinctCoprimeLists' (soFar ++ [next]) (n - 1) + +-- | Given a solution, and the coefficients, work out the result. +-- Effectively the dot-product of the two lists. +calcUnits :: [Integer] -> [Integer] -> Integer +calcUnits a b = sum $ zipWith (*) a b + +-- | Given the solution for an equation (values of x_1 .. x_n), generates +-- equalities and inequalities. The equalities will all be true and consistent, +-- the inequalities will all turn out to be equal. That is, when the inequalities +-- are resolved, the LHS will equal 0. Therefore we can generate the inequalities +-- using the same method as equalities. Also, the equalities are assured to be +-- distinct. If they were not distinct (one could be transformed into another by scaling) +-- then the equation set would be unsolveable. +generateEqualities :: [Integer] -> Gen (EqualityProblem, InequalityProblem) +generateEqualities solution = do eqCoeffs <- distinctCoprimeLists num_vars + ineqCoeffs <- distinctCoprimeLists num_vars + return (map mkCoeffArray eqCoeffs, map mkCoeffArray ineqCoeffs) + where + num_vars = length solution + mkCoeffArray coeffs = arrayise $ (negate $ calcUnits solution coeffs) : coeffs + +-- | The input to a test that will have an exact solution after the equality problems have been +-- solved. All the inequalities will be simplified to 0 = 0. The answers to the equation are +-- in the map. +newtype OmegaTestInput = OMI (Map.Map CoeffIndex Integer,(EqualityProblem, InequalityProblem)) deriving (Show) + +-- | Generates an Omega test problem with between 1 and 10 variables (incl), where the solutions +-- are numbers between -20 and + 20 (incl). +generateProblem :: Gen (Map.Map CoeffIndex Integer,(EqualityProblem, InequalityProblem)) +generateProblem = choose (1,10) >>= (\n -> replicateM n $ choose (-20,20)) >>= + (\ans -> seqPair (return $ makeAns (zip [1..] ans),generateEqualities ans)) + where + makeAns :: [(Int, Integer)] -> Map.Map CoeffIndex Integer + makeAns = Map.fromList + +instance Arbitrary OmegaTestInput where + arbitrary = generateProblem >>* OMI + +qcOmegaEquality :: [QuickCheckTest] +qcOmegaEquality = [scaleQC (40,200,2000,10000) prop] + where + prop (OMI (ans,(eq,ineq))) = omegaCheck actAnswer + where + actAnswer = solveConstraints (defaultMapping $ Map.size ans) eq ineq + -- We use Map.assocs because pshow doesn't work on Maps + omegaCheck (Just (vm,ineqs)) = (True *==* all (all (== 0) . elems) ineqs) + *&&* ((Map.assocs ans) *==* (Map.assocs $ getCounterEqs vm)) + omegaCheck Nothing = mkFailResult ("Found Nothing while expecting answer: " ++ show (eq,ineq)) + +-- | A randomly mutated problem ready for testing the inequality pruning. +-- The first part is the input to the pruning, and the second part is the expected result; +-- the remaining inequalities, preceding by a list of equalities. +type MutatedProblem = + (InequalityProblem + ,Maybe ([EqualityConstraintEquation],InequalityProblem)) + +-- | The type for inside the function; easier to work with since it can't be +-- inconsistent until the end. +type MutatedProblem' = + (InequalityProblem + ,[EqualityConstraintEquation] + ,InequalityProblem) + +-- | Given a distinct inequality list, mutates each one at random using one of these mutations: +-- * Unchanged +-- * Generates similar but redundant equations +-- * Generates its dual (to be transformed into an equality equation) +-- * Generates an inconsistent partner (rare - 20% chance of existing in the returned problem). +-- The equations passed in do not have to be consistent, merely unique and normalised. +-- Returns the input, and the expected output. +mutateEquations :: InequalityProblem -> Gen MutatedProblem +mutateEquations ineq = do (a,b,c) <- mapM mutate ineq >>* + foldl (\(a,b,c) (x,y,z) -> (a++x,b++y,c++z)) ([],[],[]) + frequency + [ + (80,return (a,Just (b,c))) + ,(20,addInconsistent a >>* (\x -> (x,Nothing))) + ] + where + -- We take an equation like 5 + 3x - y >=0 (i.e. 3x - y >= -5) + -- and add -6 -3x + y >= 0 (i.e. -6 >= 3x - y) + -- This works for all cases, even where the unit coeff is zero; + -- 3x - y >= 0 becomes -1 -3x + y >= 0 (i.e. -1 >= 3x - y) + addInconsistent :: InequalityProblem -> Gen InequalityProblem + addInconsistent inpIneq + = do randEq <- oneof (map return inpIneq) + let negEq = amap negate randEq + let modRandEq = (negEq) // [(0, (negEq ! 0) - 1)] + return (modRandEq : inpIneq) + + mutate :: InequalityConstraintEquation -> Gen MutatedProblem' + mutate ineq = oneof + [ + return ([ineq],[],[ineq]) + ,addRedundant ineq + ,return $ addDual ineq + ] + + addDual :: InequalityConstraintEquation -> MutatedProblem' + addDual eq = ([eq,neg],[eq],[]) where neg = amap negate eq + + addRedundant :: InequalityConstraintEquation -> Gen MutatedProblem' + addRedundant ineq = do i <- choose (1,5) -- number of redundant equations to add + newIneqs <- replicateM i addRedundant' + return (ineq : newIneqs, [], [ineq]) + where + -- A redundant equation is one with a bigger unit coefficient: + addRedundant' = do n <- choose (1,100) + return $ ineq // [(0,n + (ineq ! 0))] + +-- | Puts an equality into normal form. This is where the first non-zero coefficient is positive. +-- If all coefficients are zero, it doesn't matter (it will be equal to its negation) +normaliseEquality :: EqualityConstraintEquation -> EqualityConstraintEquation +normaliseEquality eq = case listToMaybe $ filter (/= 0) $ elems eq of + Nothing -> eq -- all zeroes + Just x -> amap (* (signum x)) eq + +newtype OmegaPruneInput = OPI MutatedProblem deriving (Show) + +instance Arbitrary OmegaPruneInput where + arbitrary = ((generateProblem >>* snd) >>= (return . snd) >>= mutateEquations) >>* OPI + +qcOmegaPrune :: [QuickCheckTest] +qcOmegaPrune = [scaleQC (100,1000,10000,50000) prop] + where + --We perform the map assocs because we can't compare arrays using *==* + -- (toConstr fails in the pretty-printing!). + prop (OPI (inp,out)) = + case out of + Nothing -> Nothing *==* result + Just (expEq,expIneq) -> + case result of + Nothing -> mkFailResult $ "Expected success but got failure: " ++ pshow (inp,out) + Just (actEq,actIneq) -> + (sort (map assocs expIneq) *==* sort (map assocs actIneq)) + *&&* ((sort $ map normaliseEquality expEq) *==* (sort $ map normaliseEquality actEq)) + where + result = pruneAndCheck inp + +qcTests :: (Test, [QuickCheckTest]) +qcTests = (TestList + [ + testArrayCheck + ,testIndexes + ] + ,qcOmegaEquality ++ qcOmegaPrune) + + + diff --git a/transformations/RainUsageCheckTest.hs b/transformations/RainUsageCheckTest.hs index b83a917..c220fce 100644 --- a/transformations/RainUsageCheckTest.hs +++ b/transformations/RainUsageCheckTest.hs @@ -16,25 +16,19 @@ You should have received a copy of the GNU General Public License along with this program. If not, see . -} -module RainUsageCheckTest (qcTests) where +module RainUsageCheckTest (tests) where import Control.Monad.Identity import Data.Graph.Inductive -import Data.Array.IArray -import Data.List import qualified Data.Map as Map -import Data.Maybe import qualified Data.Set as Set import Prelude hiding (fail) import Test.HUnit -import Test.QuickCheck -import ArrayUsageCheck import qualified AST as A import FlowGraph import Metadata -import PrettyShow import RainUsageCheck import TestUtils import Utils @@ -300,412 +294,11 @@ testReachDef = TestList fst3 :: (a,b,c) -> a fst3(x,_,_) = x -testArrayCheck :: Test -testArrayCheck = TestList - [ - -- x_1 = 0 - pass (0, [], [[0,1]], []) - -- x_1 = 0, 3x_1 >= 0 --> 0 >= 0 - ,pass (1, [[0,0]], [[0,1]], [[0,3]]) - -- -7 + x_1 = 0 - ,pass (2, [], [[-7,1]], []) - -- x_1 = 9, 3 + 2x_1 >= 0 --> 21 >= 0 - ,pass (3, [[21,0]], [[-9,1]], [[3,2]]) - -- x_1 + x_2 = 0, 4x_1 = 8, 2x_2 = -4 - ,pass (4, [], [[0,1,1], [-8,4,0], [4,0,2]], []) - -- - x_1 + x_2 = 0, 4x_1 = 8, 2x_2 = 4 - ,pass (5, [], [[0,-1,1], [-8,4,0], [-4,0,2]], []) - -- -x_1 = -9, 3 + 2x_1 >= 0 --> 21 >= 0 - ,pass (6, [[21,0]], [[9,-1]], [[3,2]]) - - - -- From the Omega Test paper (x = x_1, y = x_2, z = x_3, sigma = x_1 (effectively)): - ,pass (100, [[11,13,0,0], [28,-13,0,0], [47,-5,0,0], [53,5,0,0]], [[-17,7,12,31], [-7,3,5,14]], - [[-1,1,0,0], [40,-1,0,0], [50,0,1,0], [50,0,-1,0]]) - - -- Impossible/inconsistent equality constraints: - - -- -7 = 0 - ,TestCase $ assertEqual "testArrayCheck 1002" (Nothing) (solveConstraints' [simpleArray [(0,7),(1,0)]] []) - -- x_1 = 3, x_1 = 4 - ,TestCase $ assertEqual "testArrayCheck 1003" (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 1004" (Nothing) (solveConstraints' [simpleArray [(0,0),(1,1),(2,1)], simpleArray [(0,3),(1,1),(2,1)]] []) - -- 4x_1 = 7 - ,TestCase $ assertEqual "testArrayCheck 1005" (Nothing) (solveConstraints' [simpleArray [(0,-7),(1,4)]] []) - ] - where - solveConstraints' = solveConstraints undefined - - pass :: (Int, [[Integer]], [[Integer]], [[Integer]]) -> Test - pass (ind, expIneq, inpEq, inpIneq) = TestCase $ assertEqual ("testArrayCheck " ++ show ind) - (Just $ map arrayise expIneq) (transformMaybe snd $ solveConstraints' (map arrayise inpEq) (map arrayise inpIneq)) - -arrayise :: [Integer] -> Array Int Integer -arrayise = simpleArray . zip [0..] - --- Useful to make sure the equation types are not mixed up: -newtype HandyEq = Eq [(Int, Integer)] deriving (Show, Eq) -newtype HandyIneq = Ineq [(Int, Integer)] deriving (Show, Eq) - -testIndexes :: Test -testIndexes = TestList - [ - -- Rules for writing equations: - -- You must use the variables i, j, k in that order as you need them. - -- Never write an equation just involving i and k, or j and k. Always - -- use (i), (i and j), or (i and j and k). - -- Constant scaling must always be on the left, and does not need the con - -- function. con 1 ** i won't compile. - - easilySolved (0, [i === con 7], []) - ,easilySolved (1, [2 ** i === con 12], []) - --should fail: - ,notSolveable (2, [i === con 7],[i <== con 5]) - - -- Can i = j? - ,notSolveable (3, [i === j], i_j_constraint 0 9) - - -- TODO need to run the below exampls on a better test (they are not "easily" solved): - - -- Can (j + 1 % 10 == i + 1 % 10)? - ,neverSolveable $ withKIsMod (i ++ con 1) 10 $ withNIsMod (j ++ con 1) 10 $ (4, [k === n], i_j_constraint 0 9) - -- Off by one (i + 1 % 9) - ,hardSolved $ withKIsMod (i ++ con 1) 9 $ withNIsMod (j ++ con 1) 9 $ (5, [k === n], i_j_constraint 0 9) - - -- The "nightmare" example from the Omega Test paper: - ,neverSolveable (6,[],leq [con 27, 11 ** i ++ 13 ** j, con 45] &&& leq [con (-10), 7 ** i ++ (-9) ** j, con 4]) - - ,safeParTest 100 True (0,10) [i] - ,safeParTest 120 False (0,10) [i,i ++ con 1] - ,safeParTest 140 True (0,10) [2 ** i, 2 ** i ++ con 1] - - - ,TestCase $ assertStuff "testIndexes makeEq" - (Right (Map.empty,(uncurry makeConsistent) (doubleEq [con 0 === con 1],leq [con 0,con 0,con 7] &&& leq [con 0,con 1,con 7]))) $ - makeEquations [intLiteral 0, intLiteral 1] (intLiteral 7) - ,TestCase $ assertStuff "testIndexes makeEq 2" - (Right (Map.singleton "i" 1,(uncurry makeConsistent) (doubleEq [i === con 3],leq [con 0,con 3,con 7] &&& leq [con 0,i,con 7]))) $ - makeEquations [exprVariable "i",intLiteral 3] (intLiteral 7) - - ,TestCase $ assertCounterExampleIs "testIndexes testVarMapping" (Map.fromList [(1,7)]) - $ makeConsistent [i === con 7] [] - ] - where - -- TODO comment these functions and rename the latter one - doubleEq = concatMap (\(Eq e) -> [Eq e,Eq $ negateVars e]) - assertStuff title x y = assertEqual title (munge x) (munge y) - where - munge = transformEither id (transformPair id (transformPair sort sort)) - - assertCounterExampleIs title counterEq (eq,ineq) - = assertCompareCustom title equivEq (Just counterEq) ((solveAndPrune eq ineq) >>* (getCounterEqs . fst)) - where - equivEq (Just xs) (Just ys) = xs == ys - equivEq Nothing Nothing = True - equivEq _ _ = False - - - -- Given some indexes using "i", this function checks whether these can - -- ever overlap within the bounds given, and matches this against - -- the expected value; True for safe, False for unsafe. - safeParTest :: Int -> Bool -> (Integer,Integer) -> [[(Int,Integer)]] -> Test - safeParTest ind expSafe (low, high) usesI = TestCase $ - (if expSafe - then assertEqual ("testIndexes " ++ show ind ++ " should be safe (unsolveable)") [] - else assertNotEqual ("testIndexes " ++ show ind ++ " should be solveable") [] - ) - $ findSolveable $ zip3 [ind..] (equalityCombinations) (repeat constraint) - where - changeItoJ (1,n) = (2,n) - changeItoJ x = x - - usesJ = map (map changeItoJ) usesI - - constraint = i_j_constraint low high - - equalityCombinations :: [[HandyEq]] - equalityCombinations = map (\(lhs,rhs) -> [lhs === rhs]) $ product2 (usesI,usesJ) - - - -- | The constraint for an arbitrary i,j that exist between low and high (inclusive) - -- and where i and j are distinct and i is taken to be the lower index. - i_j_constraint :: Integer -> Integer -> [HandyIneq] - i_j_constraint low high = [con low <== i, i ++ con 1 <== j, j <== con high] - - --TODO clear up this mess of easilySolved/hardSolved helper functions - - findSolveable :: [(Int, [HandyEq], [HandyIneq])] -> [(Int, [HandyEq], [HandyIneq])] - findSolveable = filter isSolveable - - isSolveable :: (Int, [HandyEq], [HandyIneq]) -> Bool - isSolveable (ind, eq, ineq) = isJust $ (uncurry solveAndPrune) (makeConsistent eq ineq) - - easilySolved :: (Int, [HandyEq], [HandyIneq]) -> Test - easilySolved (ind, eq, ineq) = TestCase $ - let ineq' = (uncurry solveAndPrune) (makeConsistent eq ineq) in - case ineq' of - Nothing -> assertFailure $ "testIndexes " ++ show ind ++ " expected to pass (solving+pruning) but failed; problem: " ++ show (eq,ineq) - Just (_,ineq'') -> - if numVariables ineq'' <= 1 - then return () - -- Until we put in the route from original to mapped variables, - -- we can't give a useful test failure here: - else assertFailure $ "testIndexes " ++ show ind ++ " more than one variable left after solving" - - hardSolved :: (Int, [HandyEq], [HandyIneq]) -> Test - hardSolved (ind, eq, ineq) = TestCase $ - assertBool ("testIndexes " ++ show ind) $ isJust $ - (transformMaybe snd . uncurry solveAndPrune) (makeConsistent eq ineq) >>= (pruneAndCheck . fmElimination) - - notSolveable :: (Int, [HandyEq], [HandyIneq]) -> Test - notSolveable (ind, eq, ineq) = TestCase $ assertEqual ("testIndexes " ++ show ind) Nothing $ - (transformMaybe snd . uncurry solveAndPrune) (makeConsistent eq ineq) >>* ((<= 1) . numVariables) - - - neverSolveable :: (Int, [HandyEq], [HandyIneq]) -> Test - neverSolveable (ind, eq, ineq) = TestCase $ assertEqual ("testIndexes " ++ show ind) Nothing $ - (transformMaybe snd . uncurry solveAndPrune) (makeConsistent eq ineq) >>= (pruneAndCheck . fmElimination) - - - -- The easy way of writing equations is built on the following Haskell magic. - -- Essentially, everything is a list of (index, coefficient). You can scale - -- with the ** operator, and you can form equalities and inequalities with - -- the ===, <== and >== operators. The type system saves you from doing anything - -- nonsensical. - - leq :: [[(Int,Integer)]] -> [HandyIneq] - leq [] = [] - leq [_] = [] - leq (x:y:zs) = (x <== y) : (leq (y:zs)) - - (&&&) = (++) - - infixr 4 === - infixr 4 <== - infixr 4 >== - infix 6 ** - - (===) :: [(Int,Integer)] -> [(Int,Integer)] -> HandyEq - lhs === rhs = Eq $ lhs ++ negateVars rhs - (<==) :: [(Int,Integer)] -> [(Int,Integer)] -> HandyIneq - lhs <== rhs = Ineq $ negateVars lhs ++ rhs - (>==) :: [(Int,Integer)] -> [(Int,Integer)] -> HandyIneq - lhs >== rhs = Ineq $ lhs ++ negateVars rhs - negateVars :: [(Int,Integer)] -> [(Int,Integer)] - negateVars = map (transformPair id negate) - (**) :: Integer -> [(Int,Integer)] -> [(Int,Integer)] - n ** var = map (transformPair id (* n)) var - con :: Integer -> [(Int,Integer)] - con c = [(0,c)] - i,j,k,m,n,p :: [(Int, Integer)] - i = [(1,1)] - j = [(2,1)] - k = [(3,1)] - m = [(4,1)] - n = [(5,1)] - p = [(6,1)] - - isMod :: [(Int,Integer)] -> [(Int,Integer)] -> Integer -> ([HandyEq], [HandyIneq]) - isMod var@[(ind,1)] alpha divisor = ([alpha_minus_div_sigma === var], leq [con 0, alpha_minus_div_sigma, con $ divisor - 1]) - where - alpha_minus_div_sigma = alpha ++ (negate divisor) ** sigma - sigma = [(ind+1,1)] - - -- | Adds both k and m to the equation! - withKIsMod :: [(Int,Integer)] -> Integer -> (Int, [HandyEq], [HandyIneq]) -> (Int, [HandyEq], [HandyIneq]) - withKIsMod alpha divisor (ind,eq,ineq) = let (eq',ineq') = isMod k alpha divisor in (ind,eq ++ eq',ineq ++ ineq') - - -- | Adds both n and p to the equation! - withNIsMod :: [(Int,Integer)] -> Integer -> (Int, [HandyEq], [HandyIneq]) -> (Int, [HandyEq], [HandyIneq]) - withNIsMod alpha divisor (ind,eq,ineq) = let (eq',ineq') = isMod n alpha divisor in (ind,eq ++ eq',ineq ++ ineq') - - makeConsistent :: [HandyEq] -> [HandyIneq] -> (EqualityProblem, InequalityProblem) - makeConsistent eqs ineqs = (map ensure eqs', map ensure ineqs') - where - eqs' = map (\(Eq e) -> e) eqs - ineqs' = map (\(Ineq e) -> e) ineqs - - ensure = accumArray (+) 0 (0, largestIndex) - largestIndex = maximum $ map (maximum . map fst) $ eqs' ++ ineqs' - --- QuickCheck tests for Omega Test: --- The idea is to begin with a random list of integers, representing transformed y_i variables. --- This will be the solution. Feed this into a random list of inequalities. The inequalities do --- not have to be true; they merely have to exist. Then slowly transform - - ---TODO Allow zero coefficients (but be careful we don't --- produce unsolveable equations, e.g. where an equation is all zeroes, or a_3 is zero in all of them) - --- | Generates a list of random numbers of the given size, where the numbers are all co-prime. --- This is so they can be used as normalised coefficients in a linear equation -coprimeList :: Int -> Gen [Integer] -coprimeList size = do non_normal <- replicateM size $ oneof [choose (-100,-1), choose (1,100)] - return $ map (\x -> x `div` (mygcdList non_normal)) non_normal - --- | Generates a list of lists of co-prime numbers, where each list is distinct. --- The returned list of lists will be square; N equations, each with N items -distinctCoprimeLists :: Int -> Gen [[Integer]] -distinctCoprimeLists size = distinctCoprimeLists' [] size - where - -- n is the number left to generate; size is still the "width" of the lists - distinctCoprimeLists' :: [[Integer]] -> Int -> Gen [[Integer]] - distinctCoprimeLists' result 0 = return result - distinctCoprimeLists' soFar n = do next <- coprimeList size - if (next `elem` soFar) - then distinctCoprimeLists' soFar n -- Try again - else distinctCoprimeLists' (soFar ++ [next]) (n - 1) - --- | Given a solution, and the coefficients, work out the result. --- Effectively the dot-product of the two lists. -calcUnits :: [Integer] -> [Integer] -> Integer -calcUnits a b = sum $ zipWith (*) a b - --- | Given the solution for an equation (values of x_1 .. x_n), generates --- equalities and inequalities. The equalities will all be true and consistent, --- the inequalities will all turn out to be equal. That is, when the inequalities --- are resolved, the LHS will equal 0. Therefore we can generate the inequalities --- using the same method as equalities. Also, the equalities are assured to be --- distinct. If they were not distinct (one could be transformed into another by scaling) --- then the equation set would be unsolveable. -generateEqualities :: [Integer] -> Gen (EqualityProblem, InequalityProblem) -generateEqualities solution = do eqCoeffs <- distinctCoprimeLists num_vars - ineqCoeffs <- distinctCoprimeLists num_vars - return (map mkCoeffArray eqCoeffs, map mkCoeffArray ineqCoeffs) - where - num_vars = length solution - mkCoeffArray coeffs = arrayise $ (negate $ calcUnits solution coeffs) : coeffs - --- | The input to a test that will have an exact solution after the equality problems have been --- solved. All the inequalities will be simplified to 0 = 0. The answers to the equation are --- in the map. -newtype OmegaTestInput = OMI (Map.Map CoeffIndex Integer,(EqualityProblem, InequalityProblem)) deriving (Show) - --- | Generates an Omega test problem with between 1 and 10 variables (incl), where the solutions --- are numbers between -20 and + 20 (incl). -generateProblem :: Gen (Map.Map CoeffIndex Integer,(EqualityProblem, InequalityProblem)) -generateProblem = choose (1,10) >>= (\n -> replicateM n $ choose (-20,20)) >>= - (\ans -> seqPair (return $ makeAns (zip [1..] ans),generateEqualities ans)) - where - makeAns :: [(Int, Integer)] -> Map.Map CoeffIndex Integer - makeAns = Map.fromList - -instance Arbitrary OmegaTestInput where - arbitrary = generateProblem >>* OMI - -qcOmegaEquality :: [QuickCheckTest] -qcOmegaEquality = [scaleQC (40,200,2000,10000) prop] - where - prop (OMI (ans,(eq,ineq))) = omegaCheck actAnswer - where - actAnswer = solveConstraints (defaultMapping $ Map.size ans) eq ineq - -- We use Map.assocs because pshow doesn't work on Maps - omegaCheck (Just (vm,ineqs)) = (True *==* all (all (== 0) . elems) ineqs) - *&&* ((Map.assocs ans) *==* (Map.assocs $ getCounterEqs vm)) - omegaCheck Nothing = mkFailResult ("Found Nothing while expecting answer: " ++ show (eq,ineq)) - --- | A randomly mutated problem ready for testing the inequality pruning. --- The first part is the input to the pruning, and the second part is the expected result; --- the remaining inequalities, preceding by a list of equalities. -type MutatedProblem = - (InequalityProblem - ,Maybe ([EqualityConstraintEquation],InequalityProblem)) - --- | The type for inside the function; easier to work with since it can't be --- inconsistent until the end. -type MutatedProblem' = - (InequalityProblem - ,[EqualityConstraintEquation] - ,InequalityProblem) - --- | Given a distinct inequality list, mutates each one at random using one of these mutations: --- * Unchanged --- * Generates similar but redundant equations --- * Generates its dual (to be transformed into an equality equation) --- * Generates an inconsistent partner (rare - 20% chance of existing in the returned problem). --- The equations passed in do not have to be consistent, merely unique and normalised. --- Returns the input, and the expected output. -mutateEquations :: InequalityProblem -> Gen MutatedProblem -mutateEquations ineq = do (a,b,c) <- mapM mutate ineq >>* - foldl (\(a,b,c) (x,y,z) -> (a++x,b++y,c++z)) ([],[],[]) - frequency - [ - (80,return (a,Just (b,c))) - ,(20,addInconsistent a >>* (\x -> (x,Nothing))) - ] - where - -- We take an equation like 5 + 3x - y >=0 (i.e. 3x - y >= -5) - -- and add -6 -3x + y >= 0 (i.e. -6 >= 3x - y) - -- This works for all cases, even where the unit coeff is zero; - -- 3x - y >= 0 becomes -1 -3x + y >= 0 (i.e. -1 >= 3x - y) - addInconsistent :: InequalityProblem -> Gen InequalityProblem - addInconsistent inpIneq - = do randEq <- oneof (map return inpIneq) - let negEq = amap negate randEq - let modRandEq = (negEq) // [(0, (negEq ! 0) - 1)] - return (modRandEq : inpIneq) - - mutate :: InequalityConstraintEquation -> Gen MutatedProblem' - mutate ineq = oneof - [ - return ([ineq],[],[ineq]) - ,addRedundant ineq - ,return $ addDual ineq - ] - - addDual :: InequalityConstraintEquation -> MutatedProblem' - addDual eq = ([eq,neg],[eq],[]) where neg = amap negate eq - - addRedundant :: InequalityConstraintEquation -> Gen MutatedProblem' - addRedundant ineq = do i <- choose (1,5) -- number of redundant equations to add - newIneqs <- replicateM i addRedundant' - return (ineq : newIneqs, [], [ineq]) - where - -- A redundant equation is one with a bigger unit coefficient: - addRedundant' = do n <- choose (1,100) - return $ ineq // [(0,n + (ineq ! 0))] - --- | Puts an equality into normal form. This is where the first non-zero coefficient is positive. --- If all coefficients are zero, it doesn't matter (it will be equal to its negation) -normaliseEquality :: EqualityConstraintEquation -> EqualityConstraintEquation -normaliseEquality eq = case listToMaybe $ filter (/= 0) $ elems eq of - Nothing -> eq -- all zeroes - Just x -> amap (* (signum x)) eq - -newtype OmegaPruneInput = OPI MutatedProblem deriving (Show) - -instance Arbitrary OmegaPruneInput where - arbitrary = ((generateProblem >>* snd) >>= (return . snd) >>= mutateEquations) >>* OPI - -qcOmegaPrune :: [QuickCheckTest] -qcOmegaPrune = [scaleQC (100,1000,10000,50000) prop] - where - --We perform the map assocs because we can't compare arrays using *==* - -- (toConstr fails in the pretty-printing!). - prop (OPI (inp,out)) = - case out of - Nothing -> Nothing *==* result - Just (expEq,expIneq) -> - case result of - Nothing -> mkFailResult $ "Expected success but got failure: " ++ pshow (inp,out) - Just (actEq,actIneq) -> - (sort (map assocs expIneq) *==* sort (map assocs actIneq)) - *&&* ((sort $ map normaliseEquality expEq) *==* (sort $ map normaliseEquality actEq)) - where - result = pruneAndCheck inp - -qcTests :: (Test, [QuickCheckTest]) -qcTests = (TestList +tests :: Test +tests = TestList [ testGetVarProc - ,testIndexes ,testInitVar -- ,testParUsageCheck ,testReachDef - ,testArrayCheck ] - ,qcOmegaEquality ++ qcOmegaPrune) - - -