From 41ab2d6bdeef88afa4215954698de3d1b0f9ae19 Mon Sep 17 00:00:00 2001 From: Neil Brown Date: Sat, 9 Feb 2008 17:23:49 +0000 Subject: [PATCH] Introduced scaling of Modulo and Divide items, and tweaked some of the parameters to make the tests a little shorter --- checks/ArrayUsageCheck.hs | 41 ++++++++++---------- checks/ArrayUsageCheckTest.hs | 71 ++++++++++++++++++++++------------- 2 files changed, 63 insertions(+), 49 deletions(-) diff --git a/checks/ArrayUsageCheck.hs b/checks/ArrayUsageCheck.hs index 44b54a4..62fde3a 100644 --- a/checks/ArrayUsageCheck.hs +++ b/checks/ArrayUsageCheck.hs @@ -486,11 +486,6 @@ makeEquations otherInfo accesses bound -- Note that in all these functions, the divisor should always be positive! --- Takes an expression, and transforms it into an expression like: --- (e_0 + e_1 + e_2) / d --- where d is a constant (non-zero!) integer, and each e_k --- is either a const, a var, const * var, or (const * var) % const [TODO]. --- If the expression cannot be transformed into such a format, an error is returned flatten :: A.Expression -> Either String [FlattenedExp] flatten (A.Literal _ _ (A.IntLiteral _ n)) = return [Const (read n)] flatten (A.ExprVariable _ v) = return [Scale 1 (v,0)] @@ -525,7 +520,8 @@ flatten (A.Dyadic m op lhs rhs) | op == A.Add = combine' (flatten lhs) (flatte scale :: Integer -> FlattenedExp -> Either String FlattenedExp scale sc (Const n) = return $ Const (n * sc) scale sc (Scale n v) = return $ Scale (n * sc) v - -- TODO test the other cases then write them + scale sc (Modulo n t b) = return $ Modulo (n * sc) t b + scale sc (Divide n t b) = return $ Divide (n * sc) t b -- | An easy way of applying combine to two monadic returns combine' :: Either String [FlattenedExp] -> Either String [FlattenedExp] -> Either String [FlattenedExp] @@ -696,14 +692,15 @@ makeEquation l t summedItems [([ModuloCase], Map.Map Int Integer,[Map.Map Int Integer], [Map.Map Int Integer])] makeEquation' m (Const n) = return $ add (0,n) m makeEquation' m sc@(Scale n v) = varIndex sc >>* (\ind -> add (ind, n) m) - makeEquation' m mod@(Modulo _ top bottom) -- TODO use the scale properly + makeEquation' m mod@(Modulo n top bottom) = do top' <- process (Set.toList top) >>* map (\(_,a,b,c) -> (a,b,c)) top'' <- getSingleItem "Modulo or divide not allowed in the numerator of Modulo" top' bottom' <- process (Set.toList bottom) >>* map (\(_,a,b,c) -> (a,b,c)) - topIndex <- varIndex mod + modIndex <- varIndex mod case onlyConst (Set.toList bottom) of Just bottomConst -> - let add_x_plus_my = zipMap plus top'' . zipMap plus (Map.fromList [(topIndex,bottomConst)]) in + -- Actually adds n*(x + my) + let add_x_plus_my = zipMap plus (Map.map (*n) top'') . zipMap plus (Map.fromList [(modIndex,n * bottomConst)]) in return $ -- The zero option (x = 0, x REM y = 0): ( map (transformQuad (++ [XZero]) id (++ [top'']) id) m) @@ -713,7 +710,7 @@ makeEquation l t summedItems -- x >= 1 [zipMap plus (Map.fromList [(0,-1)]) top'' -- m <= 0 - ,Map.fromList [(topIndex,-1)] + ,Map.fromList [(modIndex,-1)] -- x + my + 1 - |y| <= 0 ,Map.map negate $ add_x_plus_my $ Map.fromList [(0,1 - bottomConst)] -- x + my >= 0 @@ -724,7 +721,7 @@ makeEquation l t summedItems -- x <= -1 [add' (0,-1) $ Map.map negate top'' -- m >= 0 - ,Map.fromList [(topIndex,1)] + ,Map.fromList [(modIndex,1)] -- x + my - 1 + |y| >= 0 ,add_x_plus_my $ Map.fromList [(0,bottomConst - 1)] -- x + my <= 0 @@ -736,20 +733,20 @@ makeEquation l t summedItems -- The zero option (x = 0, x REM y = 0): (map (transformQuad (++ [XZero]) id (++ [top'']) id) m) -- The rest: - ++ twinItems True True (top'', topIndex) bottom'' - ++ twinItems True False (top'', topIndex) bottom'' - ++ twinItems False True (top'', topIndex) bottom'' - ++ twinItems False False (top'', topIndex) bottom'' + ++ twinItems True True n (top'', modIndex) bottom'' + ++ twinItems True False n (top'', modIndex) bottom'' + ++ twinItems False True n (top'', modIndex) bottom'' + ++ twinItems False False n (top'', modIndex) bottom'' where -- Each pair for modulo (variable divisor) depending on signs of x and y (in x REM y): - twinItems :: Bool -> Bool -> (Map.Map Int Integer,Int) -> Map.Map Int Integer -> + twinItems :: Bool -> Bool -> Integer -> (Map.Map Int Integer,Int) -> Map.Map Int Integer -> [([ModuloCase], Map.Map Int Integer,[Map.Map Int Integer], [Map.Map Int Integer])] - twinItems xPos yPos (top,topIndex) bottom - = (map (transformQuad (++ [findCase xPos yPos False]) (zipMap plus top) id + twinItems xPos yPos n (top,modIndex) bottom + = (map (transformQuad (++ [findCase xPos yPos False]) (zipMap plus $ Map.map (*n) top) id (++ [xEquation] ++ [xLowerBound False] ++ [xUpperBound False])) m) - ++ (map (transformQuad (++ [findCase xPos yPos True]) (zipMap plus top . add' (topIndex,1)) id + ++ (map (transformQuad (++ [findCase xPos yPos True]) (zipMap plus (Map.map (*n) top) . add' (modIndex, n)) id (++ [xEquation] ++ [xLowerBound True] ++ [xUpperBound True] @@ -760,12 +757,12 @@ makeEquation l t summedItems -- F T | a - y >= 0 -- F F | a + y >= 0 -- Therefore the sign of a is (not xPos), the sign of y is (not yPos) - ++ [add' (topIndex,if xPos then -1 else 1) (signEq (not yPos) bottom)])) m) + ++ [add' (modIndex,if xPos then -1 else 1) (signEq (not yPos) bottom)])) m) where -- x >= 1 or x <= -1 (rearranged: -1 + x >= 0 or -1 - x >= 0) xEquation = add' (0,-1) (signEq xPos top) -- We include (x [+ a] >= 0 or x [+ a] <= 0) even though they are redundant in some cases (addA = False): - xLowerBound addA = signEq xPos $ (if addA then add' (topIndex,1) else id) top + xLowerBound addA = signEq xPos $ (if addA then add' (modIndex,1) else id) top -- We want to add the bounds as follows: -- xPos yPos | Equation -- T T | y - 1 - x - a >= 0 @@ -773,7 +770,7 @@ makeEquation l t summedItems -- F T | x + a - 1 + y >= 0 -- F F | x + a - y - 1 >= 0 -- Therefore the sign of y in the equation is yPos, the sign of x and a is (not xPos) - xUpperBound addA = add' (0,-1) $ zipMap plus (signEq (not xPos) ((if addA then add' (topIndex,1) else id) top)) (signEq yPos bottom) + xUpperBound addA = add' (0,-1) $ zipMap plus (signEq (not xPos) ((if addA then add' (modIndex,1) else id) top)) (signEq yPos bottom) signEq sign eq = if sign then eq else Map.map negate eq diff --git a/checks/ArrayUsageCheckTest.hs b/checks/ArrayUsageCheckTest.hs index 4d4590c..784d78a 100644 --- a/checks/ArrayUsageCheckTest.hs +++ b/checks/ArrayUsageCheckTest.hs @@ -168,7 +168,7 @@ mylookup x = Map.findWithDefault "unknown" x lookupTable lookupTable :: Map.Map CoeffIndex String lookupTable = Map.fromList $ zip [1..] ["i","j","k","m","n","p"] - ++ [ (n,"x" ++ show n) | n <- [7..100]] -- needed for showing QuickCheck failures + ++ [ (n,"y_" ++ show n) | n <- [7..100]] -- needed for showing QuickCheck failures showInequality :: InequalityConstraintEquation -> String showInequality ineq = "0 <= " ++ zeroIfBlank (showItems ineq) @@ -574,7 +574,7 @@ genConst = do val <- lift $ choose (1, 10) genNewExp :: Bool -> StateT VarMap Gen (GenEqItems, [FlattenedExp]) genNewExp specialAllowed - = do num <- lift $ choose (1,4) + = do num <- lift $ oneof $ map return [1,1,1,1,2,2,3] -- bias towards low numbers of items items <- replicateM num $ frequency' [(20, maybeMult genConst), (80, maybeMult $ genNewItem specialAllowed)] return $ fromJust $ foldl join Nothing items where @@ -591,8 +591,8 @@ genNewExp specialAllowed scaleEq :: Integer -> FlattenedExp -> FlattenedExp scaleEq k (Const n) = Const (k * n) scaleEq k (Scale n v) = Scale (k * n) v - scaleEq k (Modulo {}) = error "TODO allow scaling of modulo" - scaleEq k (Divide {}) = error "TODO allow scaling of divide" + scaleEq k (Modulo n t b) = Modulo (k * n) t b + scaleEq k (Divide n t b) = Divide (k * n) t b join :: Maybe (GenEqItems, [FlattenedExp]) -> (GenEqItems,FlattenedExp) -> Maybe (GenEqItems, [FlattenedExp]) join Nothing (e,f) = Just (e,[f]) @@ -602,19 +602,19 @@ generateEquationInput :: Gen ([(((A.Expression,[ModuloCase]), (A.Expression,[Mod generateEquationInput = do ((items, upper),vm) <- flip runStateT Map.empty (do upper <- frequency' [(80, genConst >>* fst), (20, genNewItem False >>* fst)] - itemCount <- lift $ choose (1,6) - items <- replicateM itemCount (genNewItem True) + itemCount <- lift $ choose (1,5) + items <- replicateM itemCount (genNewExp True) return (items, upper) ) return (makeResults vm items upper, ParItems $ map (\((x,_),_) -> SeqItems [[x]]) items, fst upper) where makeResults :: VarMap -> - [(GenEqItems, FlattenedExp)] -> + [(GenEqItems, [FlattenedExp])] -> GenEqItems -> [(((A.Expression,[ModuloCase]), (A.Expression,[ModuloCase])),VarMap,[HandyEq],[HandyIneq])] makeResults vm items upper = concatMap (flip (makeResult vm) upper) (allPairs items) - makeResult :: VarMap -> ((GenEqItems, FlattenedExp), (GenEqItems, FlattenedExp)) -> GenEqItems -> + makeResult :: VarMap -> ((GenEqItems, [FlattenedExp]), (GenEqItems, [FlattenedExp])) -> GenEqItems -> [(((A.Expression,[ModuloCase]), (A.Expression,[ModuloCase])),VarMap,[HandyEq],[HandyIneq])] makeResult vm (((ex,x),fx),((ey,y),fy)) (_,u) = mkItem (ex, moduloEq vm fx) (ey, moduloEq vm fy) where @@ -631,44 +631,61 @@ generateEquationInput arrayBound :: [(CoeffIndex, Integer)] -> [(CoeffIndex, Integer)] -> [HandyIneq] arrayBound x u = leq [con 0, x, u ++ con (-1)] - moduloEq :: VarMap -> FlattenedExp -> [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])] - moduloEq vm m@(Modulo n top bottom) = - let topVar = lookupF (Set.findMin top {-TODO-} ) vm - botVar = lookupF (Set.findMin bottom {-TODO-} ) vm + moduloEq :: VarMap -> [FlattenedExp] -> [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])] + moduloEq vm es = foldl join [([],[],[],[])] (map (moduloEq' vm) es) + where + join :: [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])] -> + [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])] -> + [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])] + join xs ys = map (uncurry join') $ product2 (xs,ys) + + join' :: ([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq]) -> + ([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq]) -> + ([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq]) + join' (msx, isx, eqsx, ineqsx) (msy, isy, eqsy, ineqsy) = (msx ++ msy, isx ++ isy, eqsx ++ eqsy, ineqsx ++ ineqsy) + + moduloEq' :: VarMap -> FlattenedExp -> [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])] + moduloEq' vm m@(Modulo n top bottom) = + let topVar = lookupFS (Set.toList top) vm + botVar = lookupFS (Set.toList bottom) vm modVar = lookupF m vm in case onlyConst (Set.toList bottom) of - Just c -> let v = n**(topVar ++ (abs c)**modVar) in - - [ ([XZero], [(0,0)], [n**topVar === con 0], []) - , ([XPos], v, [], [topVar >== con 1, modVar <== con 0] &&& leq [con 0, v, con (abs c - 1)]) - , ([XNeg], v, [], [topVar <== con (-1), modVar >== con 0] &&& leq [con (1 - abs c), v, con 0]) + Just c -> let v = topVar ++ (abs c)**modVar in + [ ([XZero], [(0,0)], [topVar === con 0], []) + , ([XPos], n**v, [], [topVar >== con 1, modVar <== con 0] &&& leq [con 0, v, con (abs c - 1)]) + , ([XNeg], n**v, [], [topVar <== con (-1), modVar >== con 0] &&& leq [con (1 - abs c), v, con 0]) ] - Nothing -> let v = n**(topVar ++ modVar) in - [ ([XZero], [(0,0)], [n**topVar === con 0], []) -- TODO stop the divisor being zero + Nothing -> let v = topVar ++ modVar in + [ ([XZero], [(0,0)], [topVar === con 0], []) -- TODO stop the divisor being zero , ([XPosYPosAZero], n**topVar, [], [topVar >== con 1] &&& leq [con 0, topVar, botVar ++ con (-1)]) , ([XPosYNegAZero], n**topVar, [], [topVar >== con 1] &&& leq [con 0, topVar, (-1)**botVar ++ con (-1)]) , ([XNegYPosAZero], n**topVar, [], [topVar <== con (-1)] &&& leq [(-1)**botVar ++ con 1, topVar, con 0]) , ([XNegYNegAZero], n**topVar, [], [topVar <== con (-1)] &&& leq [botVar ++ con 1, topVar, con 0]) - , ([XPosYPosANonZero], v, [], [topVar >== con 1, modVar <== (-1)**botVar] &&& leq [con 0, v, botVar ++ con (-1)]) - , ([XPosYNegANonZero], v, [], [topVar >== con 1, modVar <== botVar] &&& leq [con 0, v, (-1)**botVar ++ con (-1)]) + , ([XPosYPosANonZero], n**v, [], [topVar >== con 1, modVar <== (-1)**botVar] &&& leq [con 0, v, botVar ++ con (-1)]) + , ([XPosYNegANonZero], n**v, [], [topVar >== con 1, modVar <== botVar] &&& leq [con 0, v, (-1)**botVar ++ con (-1)]) - , ([XNegYPosANonZero], v, [], [topVar <== con (-1), modVar >== botVar] &&& leq [(-1)**botVar ++ con 1, v, con 0]) - , ([XNegYNegANonZero], v, [], [topVar <== con (-1), modVar >== (-1)**botVar] &&& leq [botVar ++ con 1, v, con 0]) + , ([XNegYPosANonZero], n**v, [], [topVar <== con (-1), modVar >== botVar] &&& leq [(-1)**botVar ++ con 1, v, con 0]) + , ([XNegYNegANonZero], n**v, [], [topVar <== con (-1), modVar >== (-1)**botVar] &&& leq [botVar ++ con 1, v, con 0]) ] -- TODO add divide here with equations -- (for constant divisor) - moduloEq vm exp = [([], lookupF exp vm, [], [])] + moduloEq' vm exp = [([], lookupF exp vm, [], [])] + + lookupFS :: [FlattenedExp] -> VarMap -> [(CoeffIndex, Integer)] + lookupFS es vm = concatMap (flip lookupF vm) es lookupF :: FlattenedExp -> VarMap -> [(CoeffIndex, Integer)] lookupF (Const c) _ = con c lookupF f@(Scale a v) vm = [(fromJust $ Map.lookup f vm, a)] - lookupF f@(Modulo a t b) vm = [(fromJust $ Map.lookup f vm, a)] - lookupF f@(Divide a t b) vm = [(fromJust $ Map.lookup f vm, a)] + -- We don't scale modulo directly here because the modulo variable is a or m, + -- which shouldn't be scaled + lookupF f@(Modulo a t b) vm = [(fromJust $ Map.lookup f vm, 1)] + lookupF f@(Divide a t b) vm = [(fromJust $ Map.lookup f vm, 1)] qcTestMakeEquations :: [LabelledQuickCheckTest] -qcTestMakeEquations = [("Turning Code Into Equations", scaleQC (100,1000,5000,10000) prop)] +qcTestMakeEquations = [("Turning Code Into Equations", scaleQC (20,100,200,400) prop)] where prop :: MakeEquationInput -> QCProp prop (MEI mei) = testMakeEquation mei