never executed always true always false
1 {-# LANGUAGE DeriveDataTypeable #-}
2 {-# LANGUAGE RecordWildCards #-}
3 {-# LANGUAGE ScopedTypeVariables #-}
4
5 module Conjure.ModelAllSolveAll ( tests, TestTimeLimit(..) ) where
6
7 -- conjure
8 import Conjure.Prelude
9 import Conjure.Bug
10 import Conjure.Language.Definition
11 import Conjure.Language.Pretty
12 import Conjure.Language.Type ( TypeCheckerMode(..) )
13 import Conjure.UI.IO
14 import Conjure.UI.TranslateParameter
15 import Conjure.UI.TranslateSolution
16 import Conjure.UI.ValidateSolution
17 import Conjure.UI.MainHelper ( savilerowScriptName, mainWithArgs )
18 import Conjure.Language.NameResolution ( resolveNamesMulti )
19 import Conjure.UserError ( runUserErrorT )
20 import Conjure.UI ( ui )
21
22 -- base
23 import System.Environment ( getEnvironment )
24 import System.Environment ( withArgs )
25
26 -- tasty
27 import Test.Tasty ( TestTree, testGroup )
28 import Test.Tasty.HUnit ( Assertion, testCaseSteps )
29 import Test.Tasty.Options ( IsOption(..) )
30
31 -- shelly
32 import Shelly ( run, errExit, lastStderr, lastExitCode )
33
34 -- cmdargs
35 import System.Console.CmdArgs ( cmdArgs )
36
37 -- text
38 import qualified Data.Text as T ( isInfixOf, lines, unlines )
39 import qualified Data.Text.IO as T ( readFile )
40
41 -- containers
42 import qualified Data.Set as S ( fromList, toList, empty, null, difference )
43
44 -- Diff
45 -- Diff
46 import Data.Algorithm.Diff ( getGroupedDiff, PolyDiff (..) )
47 import Data.Algorithm.DiffOutput ( ppDiff )
48
49
50 srOptionsMk :: String -> [Text]
51 srOptionsMk srExtraOptions =
52 [ "-run-solver"
53 -- , "-timelimit" , "1200000"
54 -- , "-solver-options" , "-cpulimit 1200"
55 , "-all-solutions"
56 , "-preprocess" , "None"
57 , "-S0"
58 ] ++ map stringToText (words srExtraOptions)
59
60
61 -- | Which tests are we running?
62 data TestTimeLimit = TestTimeLimit Int -- lower bound, in seconds, default 0
63 Int -- upper bound, in seconds, default 10
64 deriving (Eq, Ord, Typeable)
65
66 instance IsOption TestTimeLimit where
67 defaultValue = TestTimeLimit 0 10
68
69 parseValue inp =
70 case splitOn "-" inp of
71 [i] ->
72 case readMay i of
73 Nothing -> Nothing
74 Just u -> Just (TestTimeLimit 0 u)
75 [i,j] ->
76 case (readMay i, readMay j) of
77 (Just l, Just u) -> Just (TestTimeLimit l u)
78 _ -> Nothing
79 _ -> bug "parseValue{TestTimeLimit}"
80
81 optionName = return "limit-time"
82 optionHelp = return $ unlines [ "Select which tests to run by their expected times."
83 , "Only tests which take less than the given value will be run."
84 , "See `expected-time.txt` files in the `tests/exhaustive` directory."
85 , "Default is 10."
86 ]
87
88
89 tests ::
90 HasCallStack =>
91 (?typeCheckerMode :: TypeCheckerMode) =>
92 IO (TestTimeLimit -> TestTree)
93 tests = do
94 srExtraOptions <- do
95 env <- getEnvironment
96 return $ fromMaybe "-O0" (lookup "SR_OPTIONS" env)
97 let srOptions = srOptionsMk srExtraOptions
98 putStrLn $ "Using Savile Row options: " ++ unwords (map textToString srOptions)
99 let baseDir = "tests/exhaustive"
100 dirs <- mapM (isTestDir baseDir) =<< getAllDirs baseDir
101 let testCases tl = concatMap (testSingleDir tl srOptions) (catMaybes dirs)
102 return $ \ tl -> testGroup "exhaustive" (testCases tl)
103
104
105 data TestDirFiles = TestDirFiles
106 { name :: String -- a name for the test case
107 , expectedTime :: Int -- how long do we expect this test to run (in seconds) (default: 0)
108 , tBaseDir :: FilePath -- dir
109 , outputsDir :: FilePath -- dir
110 , expectedsDir :: FilePath -- dir
111 , essenceFile :: FilePath -- dir + filename
112 , paramFiles :: [FilePath] -- filename
113 , expectedModels :: [FilePath] -- filename
114 , expectedSols :: [FilePath] -- filename
115 }
116 deriving Show
117
118
119 -- returns True if the argument points to a directory that is not hidden
120 isTestDir :: HasCallStack => FilePath -> FilePath -> IO (Maybe TestDirFiles)
121 isTestDir baseDir dir = do
122 dirContents <- getDirectoryContents dir
123 expectedTime <-
124 if "expected-time.txt" `elem` dirContents
125 then fromMaybe 0 . readMay . textToString <$> T.readFile (dir ++ "/expected-time.txt")
126 else return 0
127 let essenceFiles = filter (".essence" `isSuffixOf`) dirContents
128 case essenceFiles of
129 [f] -> Just <$> do
130 let params = filter (".param" `isSuffixOf`) dirContents
131 expecteds <- do
132 let dirExpected = dir </> "expected"
133 isDir <- doesDirectoryExist dirExpected
134 if isDir
135 then getDirectoryContents dirExpected
136 else return []
137 return TestDirFiles
138 { name = drop (length baseDir + 1) dir
139 , tBaseDir = dir
140 , outputsDir = dir </> "outputs"
141 , expectedsDir = dir </> "expected"
142 , essenceFile = dir </> f
143 , paramFiles = params
144 , expectedModels = filter (".eprime" `isSuffixOf`) expecteds
145 , expectedSols = filter (".solution" `isSuffixOf`) expecteds
146 , expectedTime = expectedTime
147 }
148 _ -> return Nothing
149
150
151 type Step = String -> Assertion
152
153
154 -- the first FilePath is the base directory for the exhaustive tests
155 -- we know at this point that the second FilePath points to a directory D,
156 -- which contains + an Essence file D/D.essence
157 -- + D/*.param files if required
158 -- + D/expected for the expected output files
159 testSingleDir ::
160 HasCallStack =>
161 (?typeCheckerMode :: TypeCheckerMode) =>
162 TestTimeLimit -> [Text] -> TestDirFiles -> [TestTree]
163 testSingleDir (TestTimeLimit timeLimitMin timeLimitMax) srOptions t@TestDirFiles{..} =
164 if shouldRun
165 then return $ testCaseSteps (map (\ ch -> if ch == '/' then '.' else ch) name) $ \ step -> do
166 conjuring step
167 sequence_ (savileRows step)
168 validating step
169 checkExpectedAndExtraFiles step srOptions t
170 equalNumberOfSolutions step t
171 noDuplicateSolutions step t
172 else []
173 where
174
175 shouldRun = or [ timeLimitMax == 0
176 , timeLimitMin <= expectedTime && expectedTime <= timeLimitMax
177 ]
178
179 conjuring step = do
180 void (step "Conjuring")
181 removeDirectoryIfExists outputsDir
182 -- generate the eprimes
183 modelAll tBaseDir outputsDir essenceFile
184
185 savileRows step =
186 if null paramFiles
187 then [ savileRowNoParam step srOptions t m | m <- expectedModels ]
188 else [ savileRowWithParams step srOptions t m p | m <- expectedModels
189 , p <- paramFiles ]
190
191 validating step =
192 if null paramFiles
193 then validateSolutionNoParam step t expectedSols
194 else validateSolutionWithParams step t [ ( p
195 , [ s | s <- expectedSols
196 , dropExtension p `isInfixOf` dropExtension s
197 ]
198 )
199 | p <- paramFiles
200 ]
201
202
203 savileRowNoParam ::
204 HasCallStack =>
205 (?typeCheckerMode :: TypeCheckerMode) =>
206 Step -> [Text] -> TestDirFiles -> FilePath -> Assertion
207 savileRowNoParam step srOptions TestDirFiles{..} modelPath = do
208 step (unwords ["Savile Row:", modelPath])
209 let outBase = dropExtension modelPath
210 fileShouldExist (outputsDir </> outBase ++ ".eprime")
211 (stdoutSR, stderrSR, exitCodeSR) <-
212 sh $ errExit False $ do
213 stdoutSR <- run savilerowScriptName $
214 [ "-in-eprime" , stringToText $ outputsDir </> outBase ++ ".eprime"
215 , "-out-minion" , stringToText $ outputsDir </> outBase ++ ".eprime-minion"
216 , "-out-aux" , stringToText $ outputsDir </> outBase ++ ".eprime-aux"
217 , "-out-info" , stringToText $ outputsDir </> outBase ++ ".eprime-info"
218 , "-out-solution" , stringToText $ outputsDir </> outBase ++ ".eprime-solution"
219 ] ++ srOptions
220 stderrSR <- lastStderr
221 exitCodeSR <- lastExitCode
222 return (stdoutSR, stderrSR, exitCodeSR)
223 if
224 | exitCodeSR == 0 -> do
225 eprimeModel <- readModelInfoFromFile (outputsDir </> modelPath)
226 nbEprimeSolutions <- length . filter ((outBase ++ ".eprime-solution.") `isPrefixOf`)
227 <$> getDirectoryContents outputsDir
228 forM_ (take nbEprimeSolutions allNats) $ \ i -> do
229 let eprimeSolutionPath = outBase ++ ".eprime-solution." ++ padLeft 6 '0' (show i)
230 eprimeSolution <- runLoggerPipeIO LogDebug $ readParamOrSolutionFromFile eprimeModel (outputsDir </> eprimeSolutionPath)
231 res <- runUserErrorT $ ignoreLogs $ runNameGen () $
232 translateSolution eprimeModel def eprimeSolution
233 case res of
234 Left errs -> assert $ vcat errs
235 Right s -> do
236 let filename = outputsDir </> outBase ++ "-solution" ++ padLeft 6 '0' (show i) ++ ".solution"
237 writeFile filename (renderNormal s)
238
239 | T.isInfixOf "where false" (T.unlines [stdoutSR, stderrSR]) -> return ()
240 | otherwise -> assert $ vcat [ "Savile Row stdout:" <+> pretty stdoutSR
241 , "Savile Row stderr:" <+> pretty stderrSR
242 , "Savile Row exit-code:" <+> pretty exitCodeSR
243 ]
244
245
246 savileRowWithParams ::
247 HasCallStack =>
248 (?typeCheckerMode :: TypeCheckerMode) =>
249 Step -> [Text] -> TestDirFiles -> FilePath -> FilePath -> Assertion
250 savileRowWithParams step srOptions TestDirFiles{..} modelPath paramPath = do
251 step (unwords ["Savile Row:", modelPath, paramPath])
252 fileShouldExist (outputsDir </> modelPath)
253 fileShouldExist (tBaseDir </> paramPath)
254 eprimeModel <- readModelInfoFromFile (outputsDir </> modelPath)
255 param <- runLoggerPipeIO LogDebug $ readParamOrSolutionFromFile eprimeModel (tBaseDir </> paramPath)
256 eprimeParam <- ignoreLogs $ runNameGen () $ translateParameter False eprimeModel param
257 let outBase = dropExtension modelPath ++ "-" ++ dropExtension paramPath
258 writeFile (outputsDir </> outBase ++ ".eprime-param") (renderNormal eprimeParam)
259 (stdoutSR, stderrSR, exitCodeSR) <-
260 sh $ errExit False $ do
261 stdoutSR <- run savilerowScriptName $
262 [ "-in-eprime" , stringToText $ outputsDir </> modelPath
263 , "-in-param" , stringToText $ outputsDir </> outBase ++ ".eprime-param"
264 , "-out-minion" , stringToText $ outputsDir </> outBase ++ ".eprime-minion"
265 , "-out-aux" , stringToText $ outputsDir </> outBase ++ ".eprime-aux"
266 , "-out-info" , stringToText $ outputsDir </> outBase ++ ".eprime-info"
267 , "-out-solution" , stringToText $ outputsDir </> outBase ++ ".eprime-solution"
268 ] ++ srOptions
269 stderrSR <- lastStderr
270 exitCodeSR <- lastExitCode
271 return (stdoutSR, stderrSR, exitCodeSR)
272 let stdouterrSR = T.unlines [stdoutSR, stderrSR]
273 if
274 | exitCodeSR == 0 && not (T.isInfixOf "Exception" stdouterrSR) -> do
275 nbEprimeSolutions <- length . filter ((outBase ++ ".eprime-solution.") `isPrefixOf`)
276 <$> getDirectoryContents outputsDir
277 forM_ (take nbEprimeSolutions allNats) $ \ i -> do
278 let eprimeSolutionPath = outBase ++ ".eprime-solution." ++ padLeft 6 '0' (show i)
279 eprimeSolution <- runLoggerPipeIO LogDebug $ readParamOrSolutionFromFile eprimeModel (outputsDir </> eprimeSolutionPath)
280 res <- runUserErrorT $ ignoreLogs $ runNameGen () $
281 translateSolution eprimeModel param eprimeSolution
282 case res of
283 Left errs -> assert $ vcat errs
284 Right s -> do
285 let filename = outputsDir </> outBase ++ "-solution" ++ padLeft 6 '0' (show i) ++ ".solution"
286 writeFile filename (renderNormal s)
287 | T.isInfixOf "where false" stdouterrSR -> return ()
288 | otherwise -> assert $ vcat [ "Savile Row stdout:" <+> pretty stdoutSR
289 , "Savile Row stderr:" <+> pretty stderrSR
290 , "Savile Row exit-code:" <+> pretty exitCodeSR
291 ]
292
293
294 validateSolutionNoParam ::
295 HasCallStack =>
296 (?typeCheckerMode :: TypeCheckerMode) =>
297 Step -> TestDirFiles -> [FilePath] -> Assertion
298 validateSolutionNoParam step TestDirFiles{..} solutionPaths = do
299 step "Validating solutions"
300 essence <- readModelFromFile essenceFile
301 forM_ solutionPaths $ \ solutionPath -> do
302 step (unwords ["Validating solution:", solutionPath])
303 fileShouldExist (outputsDir </> solutionPath)
304 solution <- runLoggerPipeIO LogDebug $ readParamOrSolutionFromFile essence (outputsDir </> solutionPath)
305 result <- runUserErrorT $ ignoreLogs $ runNameGen () $ do
306 [essence2, param2, solution2] <- resolveNamesMulti [essence, def, solution]
307 validateSolution essence2 param2 solution2
308 case result of
309 Left errs -> assert $ vcat errs
310 Right () -> return ()
311
312
313 validateSolutionWithParams ::
314 HasCallStack =>
315 (?typeCheckerMode :: TypeCheckerMode) =>
316 Step -> TestDirFiles -> [(FilePath, [FilePath])] -> Assertion
317 validateSolutionWithParams step TestDirFiles{..} paramSolutionPaths = do
318 step "Validating solutions"
319 essence <- readModelFromFile essenceFile
320 forM_ paramSolutionPaths $ \ (paramPath, solutionPaths) -> do
321 fileShouldExist (tBaseDir </> paramPath)
322 param <- runLoggerPipeIO LogDebug $ readParamOrSolutionFromFile essence (tBaseDir </> paramPath)
323 forM_ solutionPaths $ \ solutionPath -> do
324 step (unwords ["Validating solution:", paramPath, solutionPath])
325 fileShouldExist (outputsDir </> solutionPath)
326 solution <- runLoggerPipeIO LogDebug $ readParamOrSolutionFromFile essence (outputsDir </> solutionPath)
327 result <- runUserErrorT $ ignoreLogs $ runNameGen () $ do
328 [essence2, param2, solution2] <- resolveNamesMulti [essence, param, solution]
329 validateSolution essence2 param2 solution2
330 case result of
331 Left errs -> assert $ vcat errs
332 Right () -> return ()
333
334
335 checkExpectedAndExtraFiles :: Step -> [Text] -> TestDirFiles -> Assertion
336 checkExpectedAndExtraFiles step srOptions TestDirFiles{..} = do
337 step "Checking"
338 let
339 relevantExts :: [String]
340 relevantExts = [".eprime", ".eprime-param"]
341 ++ [".solution" | "-sat" `notElem` srOptions] -- do not diff each individual solution
342 -- if we are using a sat solver
343
344 relevantFile :: FilePath -> Bool
345 relevantFile f = or [ suffix `isSuffixOf` f
346 | suffix <- relevantExts
347 ]
348 expecteds <- do
349 b <- doesDirectoryExist expectedsDir
350 if b
351 then S.fromList . filter relevantFile <$> getDirectoryContents expectedsDir
352 else return S.empty
353 outputs <- do
354 b <- doesDirectoryExist outputsDir
355 if b
356 then S.fromList . filter relevantFile <$> getDirectoryContents outputsDir
357 else return S.empty
358 let extras = S.difference outputs expecteds
359
360 step "Checking extra files"
361 unless (S.null extras) $ assert $ "Unexpected files:" <+> prettyList id ", " (S.toList extras)
362
363 step "Checking expected files"
364 forM_ expecteds $ \ item -> do
365 step (unwords ["Checking expected file:", item])
366 let expectedPath = expectedsDir </> item
367 let generatedPath = outputsDir </> item
368 isFile <- doesFileExist generatedPath
369 if isFile
370 then do
371 e <- T.lines <$> T.readFile expectedPath
372 g <- takeWhile (/= "$ Conjure's") . T.lines <$> T.readFile generatedPath
373 let
374 fmapDiff f (First x) = First (f x)
375 fmapDiff f (Second x) = Second (f x)
376 fmapDiff f (Both x y) = Both (f x) (f y)
377
378 isBoth Both{} = True
379 isBoth _ = False
380
381 diffs = filter (not . isBoth) $ getGroupedDiff e g
382 diffsString = fmap (fmapDiff (fmap textToString)) diffs
383
384 unless (null diffs) $
385 assert $ vcat ["files differ.", pretty (ppDiff diffsString)]
386 else assert $ pretty $ "file doesn't exist: " ++ generatedPath
387
388
389 equalNumberOfSolutions :: HasCallStack => Step -> TestDirFiles -> Assertion
390 equalNumberOfSolutions step TestDirFiles{..} = do
391 step "Checking number of solutions"
392 dirShouldExist outputsDir
393 models <- sort . filter (".eprime" `isSuffixOf`) <$> getDirectoryContents outputsDir
394 params <- sort . filter (".eprime-param" `isSuffixOf`) <$> getDirectoryContents outputsDir
395 solutions <- filter (".solution" `isSuffixOf`) <$> getDirectoryContents outputsDir
396 let
397 grouped :: [ ( Maybe String -- the parameter
398 , [(String, Int)] -- model, number of solutions
399 ) ]
400 grouped =
401 (if null params
402 then
403 [ (Nothing, (model, length $ filter (solnPrefix `isPrefixOf`) solutions))
404 | model' <- models
405 , let model = splitOn1 "." model'
406 , let solnPrefix = model
407 ]
408 else
409 [ (Just param, (model, length $ filter (solnPrefix `isPrefixOf`) solutions))
410 | model <- map (splitOn1 ".") models
411 , [model2,param] <- map (splitOn "-" . splitOn1 ".") params
412 , model == model2
413 , let solnPrefix = model ++ "-" ++ param
414 ])
415 |> sortBy (comparing fst)
416 |> groupBy ((==) `on` fst)
417 |> mapMaybe (\ grp -> case grp of [] -> Nothing ; ((sol, _):_) -> Just (sol, map snd grp) )
418 let
419 differentOnes :: [(Maybe String, [(String, Int)])]
420 differentOnes =
421 [ this
422 | this@(_, modelSols) <- grouped
423 , let nbSols = map snd modelSols |> nub
424 , length nbSols > 1
425 ]
426
427 unless (null differentOnes) $
428 assert $ vcat
429 [ maybe
430 id
431 (\ p -> hang ("For parameter" <+> pretty p) 4 )
432 param
433 $ vcat [ "Model" <+> pretty model <+> "has" <+> pretty nbSols <+> "solutions."
434 | (model, nbSols) <- modelSols
435 ]
436 | (param, modelSols) <- differentOnes
437 ]
438
439
440 noDuplicateSolutions :: HasCallStack =>(?typeCheckerMode :: TypeCheckerMode) => Step -> TestDirFiles -> Assertion
441 noDuplicateSolutions step TestDirFiles{..} = do
442 step "Checking duplicate solutions"
443 dirShouldExist outputsDir
444 models <- sort . filter (".eprime" `isSuffixOf`) <$> getDirectoryContents outputsDir
445 params <- sort . filter (".eprime-param" `isSuffixOf`) <$> getDirectoryContents outputsDir
446 solutions <- filter (".solution" `isSuffixOf`) <$> getDirectoryContents outputsDir
447 solutionContents <- forM solutions $ \ s -> do m <-runLoggerPipeIO LogDebug (readParamOrSolutionFromFile (def :: Model) (outputsDir </> s))
448 return (s, m)
449 let
450 grouped :: [ ( Maybe String -- the parameter
451 , [(String, [String])] -- model, duplicate solutions
452 ) ]
453 grouped =
454 (if null params
455 then
456 [ (Nothing, (model, duplicateSolutions))
457 | model' <- models
458 , let model = splitOn1 "." model'
459 , let solnPrefix = model
460 , let thisSolutions = filter ((solnPrefix `isPrefixOf`) . fst) solutionContents
461 , let duplicateSolutions =
462 [ s1name
463 | (s1name, s1) <- thisSolutions
464 , not $ null [ s2name | (s2name, s2) <- thisSolutions
465 , s1name /= s2name && s1 == s2
466 ]
467 ]
468 , not (null duplicateSolutions)
469 ]
470 else
471 [ (Just param, (model, duplicateSolutions))
472 | model <- map (splitOn1 ".") models
473 , [model2,param] <- map (splitOn "-" . splitOn1 ".") params
474 , model == model2
475 , let solnPrefix = model ++ "-" ++ param
476 , let thisSolutions = filter ((solnPrefix `isPrefixOf`) . fst) solutionContents
477 , let duplicateSolutions =
478 [ s1name
479 | (s1name, s1) <- thisSolutions
480 , not $ null [ s2name | (s2name, s2) <- thisSolutions
481 , s1name /= s2name && s1 == s2
482 ]
483 ]
484 , not (null duplicateSolutions)
485 ])
486 |> sortBy (comparing fst)
487 |> groupBy ((==) `on` fst)
488 |> mapMaybe (\ grp -> case grp of [] -> Nothing ; ((sol, _):_) -> Just (sol, map snd grp) )
489
490 unless (null grouped) $
491 assert $ vcat
492 [ case param of
493 Nothing -> "For model" <+> pretty model <++> rest
494 Just p -> "For parameter" <+> pretty p <> ", for model" <+> pretty model <++> rest
495 | (param, duplicateSols) <- grouped
496 , (model, sols) <- duplicateSols
497 , let rest = "Duplicate solutions:" <++> prettyList id "," sols
498 ]
499
500
501 assert :: HasCallStack => Doc -> Assertion
502 assert doc = error (renderNormal doc)
503
504
505 dirShouldExist :: HasCallStack => FilePath -> Assertion
506 dirShouldExist d = do
507 b <- doesDirectoryExist d
508 unless b $
509 assert $ pretty ("dir does not exist: " ++ d)
510
511 fileShouldExist :: HasCallStack => FilePath -> Assertion
512 fileShouldExist f = do
513 b <- doesFileExist f
514 unless b $
515 assert $ pretty ("file does not exist: " ++ f)
516
517
518 modelAll ::
519 HasCallStack =>
520 (?typeCheckerMode :: TypeCheckerMode) =>
521 FilePath -> FilePath -> FilePath -> IO ()
522 modelAll tBaseDir dir essenceFile = do
523 additionalArgs <- catch (words . textToString <$> T.readFile (tBaseDir ++ "/additional-arguments.txt"))
524 (\ (_ :: SomeException) -> return [] )
525 args <- withArgs (defaultArgs ++ additionalArgs) (cmdArgs ui)
526 ignoreLogs $ runNameGen () $ mainWithArgs args
527 where
528 defaultArgs = [ "modelling"
529 , essenceFile
530 , "--output-directory=" ++ dir
531 , "-qf"
532 , "-ax"
533 , "--smart-filenames"
534 , "--line-width=120"
535 , "--channelling=yes"
536 , "--representation-levels=yes"
537 ]
538