diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 6dc6e6d971..95d60321a2 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -700,6 +700,9 @@ jobs: - run: | cd tests_fmt && sh test.sh + - run: | + cd tests_property && sh test.sh + - run: | futhark doc -o prelude-docs /dev/null tar -Jcf prelude-docs.tar.xz prelude-docs diff --git a/Makefile b/Makefile index c341b9fa47..7444ee9cce 100644 --- a/Makefile +++ b/Makefile @@ -84,5 +84,8 @@ test-structure: test-literate: cd tests_literate && sh test.sh +test-property: + cd tests_property && sh test.sh + clean: cabal clean diff --git a/futhark.cabal b/futhark.cabal index b0473ec6fc..5c69c227d1 100644 --- a/futhark.cabal +++ b/futhark.cabal @@ -394,6 +394,7 @@ library Futhark.Profile.SourceRange Futhark.Script Futhark.Test + Futhark.Test.Property Futhark.Test.Spec Futhark.Test.Values Futhark.Tools diff --git a/src/Futhark/CLI/Autotune.hs b/src/Futhark/CLI/Autotune.hs index 6206be5b61..e28e9b96f5 100644 --- a/src/Futhark/CLI/Autotune.hs +++ b/src/Futhark/CLI/Autotune.hs @@ -130,7 +130,7 @@ prepare opts futhark prog = do truns <- case testAction spec of - RunCases ios _ _ | not $ null ios -> do + RunCases ios _ _ _ | not $ null ios -> do when (optVerbose opts > 1) $ putStrLn $ unwords ("Entry points:" : map (T.unpack . iosEntryPoint) ios) diff --git a/src/Futhark/CLI/Bench.hs b/src/Futhark/CLI/Bench.hs index a349ed1fd2..b175d3ba73 100644 --- a/src/Futhark/CLI/Bench.hs +++ b/src/Futhark/CLI/Bench.hs @@ -186,7 +186,7 @@ compileBenchmark :: compileBenchmark opts (program, program_spec) = do spec <- maybe (pure program_spec) testSpecFromFileOrDie $ optTestSpec opts case testAction spec of - RunCases cases _ _ + RunCases cases _ _ _ | null $ optExcludeCase opts `intersect` (testTags spec <> testTags program_spec), diff --git a/src/Futhark/CLI/Misc.hs b/src/Futhark/CLI/Misc.hs index 015950ebef..9f424b79ba 100644 --- a/src/Futhark/CLI/Misc.hs +++ b/src/Futhark/CLI/Misc.hs @@ -84,7 +84,7 @@ mainDataget = mainWithOptions () [] "program dataset" $ \args () -> testSpecRuns = testActionRuns . testAction testActionRuns CompileTimeFailure {} = [] - testActionRuns (RunCases ios _ _) = concatMap iosTestRuns ios + testActionRuns (RunCases ios _ _ _) = concatMap iosTestRuns ios -- | @futhark check-syntax@ mainCheckSyntax :: String -> [String] -> IO () diff --git a/src/Futhark/CLI/Test.hs b/src/Futhark/CLI/Test.hs index ec6003337d..45a573c217 100644 --- a/src/Futhark/CLI/Test.hs +++ b/src/Futhark/CLI/Test.hs @@ -14,8 +14,12 @@ import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad.Trans.Class (lift) import Data.ByteString qualified as SBS import Data.ByteString.Lazy qualified as LBS +import Data.Either (partitionEithers) +import Data.IORef +import Data.Int (Int32) import Data.List (delete, partition) import Data.Map.Strict qualified as M +import Data.Maybe (mapMaybe) import Data.Text qualified as T import Data.Text.Encoding qualified as T import Data.Text.IO qualified as T @@ -44,6 +48,41 @@ import Text.Regex.TDFA -- the monadic level - a test failing should be handled explicitly. type TestM = ExceptT [T.Text] IO +extractPropSpecsFromServer :: Server -> IO [PropSpec] +extractPropSpecsFromServer srv = do + epsE <- cmdEntryPoints srv + eps <- either (error . show) pure epsE + concat <$> mapM getOne eps + where + getOne entry = do + attrsE <- cmdAttributes srv entry + attrs <- either (fail . show) pure attrsE + atMostOnePropAttr entry attrs + +atMostOnePropAttr :: T.Text -> [T.Text] -> IO [PropSpec] +atMostOnePropAttr entry attrs = + case mapMaybe (parsePropSpec entry) attrs of + [] -> pure [] + [spec] -> pure [spec] + _ -> + fail $ + "Entry point '" + <> T.unpack entry + <> "' has more than one #[prop(...)] attribute." + +parsePropSpec :: T.Text -> T.Text -> Maybe PropSpec +parsePropSpec entry attr = do + argsText <- stripCall "prop" attr + let args = map T.strip $ T.splitOn "," argsText + pure + PropSpec + { psProp = entry, + psGen = lookupArgText "gen" args, + psShrink = lookupArgText "shrink" args, + psSize = fmap fromInteger $ lookupArgRead "size" args, + psPPrint = lookupArgText "pprint" args + } + -- Taken from transformers-0.5.5.0. eitherToErrors :: Either e a -> Errors e a eitherToErrors = either failure Pure @@ -92,8 +131,8 @@ pureTestResults m = do timeout :: Int timeout = 5 * 60 * 1000000 -withProgramServer :: FilePath -> FilePath -> [String] -> (Server -> IO [TestResult]) -> TestM () -withProgramServer program runner extra_options f = do +withProgramServer :: FilePath -> FilePath -> [String] -> IORef PBTPhase -> (Server -> IO [TestResult]) -> TestM () +withProgramServer program runner extra_options phaseRef f = do -- Explicitly prefixing the current directory is necessary for -- readProcessWithExitCode to find the binary when binOutputf has -- no path component. @@ -112,7 +151,23 @@ withProgramServer program runner extra_options f = do race (threadDelay timeout) (f server) >>= \case Left _ -> do abortServer server - fail $ "test timeout after " <> show timeout <> " microseconds" + st <- readIORef phaseRef + fail $ "test timeout after " <> show timeout <> " microseconds" <> case activeTest st of + Nothing -> mempty + Just activeTestName -> do + -- use annotate to make the phase name stand out in the error message, since it is the most likely place to find out what went wrong + let phaseInfo = maybe mempty (\phaseName -> " during phase " <> phaseName) (phase st) + shrinkInfo = maybe mempty (\shrinkPhase -> " while shrinking with " <> shrinkPhase) (shrinkWith st) + sizeInfo = maybe mempty (\size -> " at size " <> showText size) (phaseSize st) + seedInfo = maybe mempty (\seed -> " with seed " <> showText seed) (phaseSeed st) + tacticInfo = maybe mempty (\tactic -> " with tactic " <> showText tactic) (phaseTactic st) + ". Was evaluating property:\n" + <> T.unpack activeTestName + <> T.unpack phaseInfo + <> T.unpack shrinkInfo + <> T.unpack sizeInfo + <> T.unpack seedInfo + <> T.unpack tacticInfo Right r -> pure r data TestMode @@ -134,7 +189,8 @@ data TestCase = TestCase { _testCaseMode :: TestMode, testCaseProgram :: FilePath, testCaseTest :: ProgramTest, - _testCasePrograms :: ProgConfig + _testCasePrograms :: ProgConfig, + pbtConfig :: PBTConfig } deriving (Show) @@ -252,7 +308,7 @@ runInterpretedEntry (FutharkExe futhark) program (InputOutputs entry run_cases) in accErrors_ $ map runInterpretedCase run_cases runTestCase :: TestCase -> TestM () -runTestCase (TestCase mode program testcase progs) = do +runTestCase (TestCase mode program testcase progs pbtConfig) = do futhark <- liftIO $ maybe getExecutablePath pure $ configFuthark progs let checkctx = mconcat @@ -289,11 +345,20 @@ runTestCase (TestCase mode program testcase progs) = do ExitSuccess -> pure () ExitFailure 127 -> throwError $ progNotFound $ T.pack futhark ExitFailure _ -> throwError $ T.decodeUtf8 err - RunCases ios structures warnings -> do + RunCases ios structures warnings properties -> do -- Compile up-front and reuse same executable for several entry points. let backend = configBackend progs extra_compiler_options = configExtraCompilerOptions progs + phaseRef <- liftIO $ newIORef $ PBTPhase + { activeTest = Nothing + , phase = Nothing + , shrinkWith = Nothing + , phaseSize = Nothing + , phaseSeed = Nothing + , phaseTactic = Nothing + } + when (mode `elem` [Compiled, Interpreted]) $ context "Generating reference outputs" $ -- We probably get the concurrency at the test program level, @@ -316,9 +381,31 @@ runTestCase (TestCase mode program testcase progs) = do ++ configExtraOptions progs runner = configRunner progs context "Running compiled program" $ - withProgramServer program runner extra_options $ \server -> do + withProgramServer program runner extra_options phaseRef $ \server -> do let run = runCompiledEntry (FutharkExe futhark) server program - concat <$> mapM run ios + propSpecs <- extractPropSpecsFromServer server + + normal_test_result <- concat <$> mapM run ios + + let requestedNames = [propName | PropertyCase propName <- properties] + let diagnostics = propertyDiagnostics requestedNames propSpecs + + if null diagnostics + then do + let verifiedProps = filter (\p -> psProp p `elem` requestedNames) propSpecs + propResultsM <- runPBT pbtConfig server verifiedProps phaseRef + let (failures, outputs) = partitionEithers propResultsM + let propResults = map (\case + Just err -> Failure [err] + Nothing -> Success) outputs + -- if any properties failed, write them to a file for later inspection + when (any (\r -> case r of + Failure _ -> True + Success -> False) propResults) $ + liftIO $ propToFile program propResults + pure $ normal_test_result ++ propResults ++ diagnostics ++ [Failure failures] + else + pure $ normal_test_result ++ diagnostics when (mode == Interpreted) $ context "Interpreting" $ @@ -464,7 +551,15 @@ doTest = catching . runTestM . runTestCase makeTestCase :: TestConfig -> TestMode -> (FilePath, ProgramTest) -> TestCase makeTestCase config mode (file, spec) = - excludeCases config $ TestCase mode file spec $ configPrograms config + excludeCases config $ TestCase mode file spec (configPrograms config) pbtcfg + where + pbtcfg = + PBTConfig + { configNumTests = configNumTests $ configPBTConfig config, + configMaxSize = configMaxSize $ configPBTConfig config, + configSeed = configSeed $ configPBTConfig config, + configShrinkTries = configShrinkTries $ configPBTConfig config + } data ReportMsg = TestStarted TestCase @@ -489,8 +584,8 @@ excludeCases config tcase = where onTest (ProgramTest desc tags action) = ProgramTest desc tags $ onAction action - onAction (RunCases ios stest wtest) = - RunCases (map onIOs $ filter relevantEntry ios) stest wtest + onAction (RunCases ios stest wtest properties) = + RunCases (map onIOs $ filter relevantEntry ios) stest wtest properties onAction action = action onIOs (InputOutputs entry runs) = InputOutputs entry $ filter (not . any excluded . runTags) runs @@ -569,6 +664,7 @@ runTests config paths = do all_tests <- map (makeTestCase config mode) <$> testSpecsFromPathsOrDie paths + -- putStrLn $ "Test cases are: " ++ show (map testCaseProgram all_tests) testmvar <- newEmptyMVar reportmvar <- newEmptyMVar concurrency <- maybe getNumCapabilities pure $ configConcurrency config @@ -591,11 +687,11 @@ runTests config paths = do numTestCases tc = case testAction $ testCaseTest tc of CompileTimeFailure _ -> 1 - RunCases ios sts wts -> + RunCases ios sts wts pbts -> length (concatMap iosTestRuns ios) + length sts + length wts - + + length pbts getResults ts | null (testStatusRemain ts) = report ts >> pure ts | otherwise = do @@ -639,7 +735,6 @@ runTests config paths = do testStatusRunFail ts' + min (numTestCases test) (length s) } - when fancy spaceTable ts <- @@ -659,7 +754,12 @@ runTests config paths = do -- Removes "Now testing" output. if fancy then cursorUpLine 1 >> clearLine - else putStrLn $ show (testStatusPass ts) <> "/" <> show (testStatusTotal ts) <> " passed." + else + putStrLn $ + show (testStatusPass ts) + <> "/" + <> show (testStatusTotal ts) + <> " passed." unless (null excluded) . putStrLn $ show (length excluded) ++ " program(s) excluded." @@ -678,7 +778,8 @@ data TestConfig = TestConfig configExclude :: [T.Text], configLineOutput :: Bool, configConcurrency :: Maybe Int, - configEntryPoint :: Maybe String + configEntryPoint :: Maybe String, + configPBTConfig :: PBTConfig } defaultConfig :: TestConfig @@ -698,7 +799,14 @@ defaultConfig = }, configLineOutput = False, configConcurrency = Nothing, - configEntryPoint = Nothing + configEntryPoint = Nothing, + configPBTConfig = + PBTConfig + { configNumTests = 100, + configMaxSize = 50, + configSeed = Nothing, + configShrinkTries = 5 + } } data ProgConfig = ProgConfig @@ -716,6 +824,9 @@ data ProgConfig = ProgConfig changeProgConfig :: (ProgConfig -> ProgConfig) -> TestConfig -> TestConfig changeProgConfig f config = config {configPrograms = f $ configPrograms config} +changePBTConfig :: (PBTConfig -> PBTConfig) -> TestConfig -> TestConfig +changePBTConfig f config = config {configPBTConfig = f $ configPBTConfig config} + setBackend :: FilePath -> ProgConfig -> ProgConfig setBackend backend config = config {configBackend = backend} @@ -854,7 +965,66 @@ commandLineOptions = ) "NAME" ) - "Only run entry points with this name." + "Only run entry points with this name.", + Option + "n" + ["num-tests"] + ( ReqArg + ( \n -> + case reads n of + [(n', "")] + | n' >= 0 -> + Right $ changePBTConfig $ \pbt -> pbt {configNumTests = n'} + _ -> + Left . optionsError $ "'" ++ n ++ "' is not a non-negative integer." + ) + "NUM" + ) $ + "Number of tests to run per property (default: " <> show (configNumTests . configPBTConfig $ defaultConfig) <> ").", + Option + "m" + ["max-size"] + ( ReqArg + ( \n -> + case reads n of + [(n', "")] + | n' >= 0 -> + Right $ changePBTConfig $ \pbt -> pbt {configMaxSize = n'} + _ -> + Left . optionsError $ "'" ++ n ++ "' is not a non-negative integer." + ) + "NUM" + ) $ + "Maximum size parameter to use for generators (default: " <> show (configMaxSize . configPBTConfig $ defaultConfig) <> ").", + Option + [] + ["seed"] + ( ReqArg + ( \n -> + case (reads n :: [(Int32, String)]) of + [(n', "")] -> + Right $ changePBTConfig $ \pbt -> pbt {configSeed = Just n'} + _ -> + Left . optionsError $ "'" ++ n ++ "' is not a valid integer." + ) + "NUM" + ) + "Set seed for all tests to use for generators.", + Option + [] + ["num-tries"] + ( ReqArg + ( \n -> + case reads n of + [(n', "")] + | n' >= 0 -> + Right $ changePBTConfig $ \pbt -> pbt {configShrinkTries = n'} + _ -> + Left . optionsError $ "'" ++ n ++ "' is not a non-negative integer." + ) + "NUM" + ) $ + "The number of tries the shrinker will perform before giving up (default: " <> show (configShrinkTries . configPBTConfig $ defaultConfig) <> ")." ] excludeBackend :: TestConfig -> TestConfig @@ -871,3 +1041,55 @@ main = mainWithOptions defaultConfig commandLineOptions "options... programs..." case progs of [] -> Nothing _ -> Just $ runTests (excludeBackend config) progs + +declaredPropertyNames :: [PropSpec] -> [T.Text] +declaredPropertyNames specs = + map psProp specs + +propertyDiagnostics :: [T.Text] -> [PropSpec] -> [TestResult] +propertyDiagnostics requested specs = + missingRequested ++ missingDeclarations + where + declared = declaredPropertyNames specs + + requestedWithoutAttr = + [ name | name <- requested, name `notElem` declared ] + + declaredWithoutRequest = + [ name | name <- declared, name `notElem` requested ] + + missingRequested = + [ Failure + [ "Unknown property in test specification: " + <> name + <> "\nThere is a '-- property: " + <> name + <> "' block, but no matching #[prop(...)] attribute on that entry point." + ] + | name <- requestedWithoutAttr + ] + + missingDeclarations = + [ Failure + [ "Undeclared property test block for attribute-backed property: " + <> name + <> "\nThere is a #[prop(...)] attribute on entry point '" + <> name + <> "', but no matching '-- property: " + <> name + <> "' block in the test specification." + ] + | name <- declaredWithoutRequest + ] + +-- Save to file helper functions +propToFile :: FilePath -> [TestResult] -> IO () +propToFile testFile results = do + let fileName = testFile <> ".prop_result" + textResults = T.unlines $ concatMap resultLines results + withFile fileName WriteMode $ \h -> + T.hPutStr h textResults + where + resultLines :: TestResult -> [T.Text] + resultLines Success = [] + resultLines (Failure msgs) = msgs diff --git a/src/Futhark/Test.hs b/src/Futhark/Test.hs index 6db3fcf769..6f66438e93 100644 --- a/src/Futhark/Test.hs +++ b/src/Futhark/Test.hs @@ -2,7 +2,8 @@ -- program is an ordinary Futhark program where an initial comment -- block specifies input- and output-sets. module Futhark.Test - ( module Futhark.Test.Spec, + ( module Futhark.Test.Property, + module Futhark.Test.Spec, valuesFromByteString, FutharkExe (..), getValues, @@ -45,6 +46,7 @@ import Data.Text.IO qualified as T import Futhark.Script qualified as Script import Futhark.Server import Futhark.Server.Values +import Futhark.Test.Property import Futhark.Test.Spec import Futhark.Test.Values qualified as V import Futhark.Util (ensureCacheDirectory, isEnvVarAtLeast, pmapIO, showText) diff --git a/src/Futhark/Test/Property.hs b/src/Futhark/Test/Property.hs new file mode 100644 index 0000000000..0c727949f1 --- /dev/null +++ b/src/Futhark/Test/Property.hs @@ -0,0 +1,643 @@ +{-# LANGUAGE LambdaCase #-} + +module Futhark.Test.Property + ( runPBT, + PBTConfig (..), + PBTPhase (..), + PropSpec (..), + lookupArgRead, + lookupArgText, + stripCall, + PBTOutput, + PBTFailure, + ) +where + +import Control.Exception +import Control.Monad +import Control.Monad.IO.Class (liftIO) +import Control.Monad.Trans.Except +import Data.Char (chr) +import Data.IORef +import Data.Int (Int32, Int64) +import Data.Maybe (fromMaybe) +import Data.Text qualified as T +import Data.Vector.Storable qualified as SV +import Futhark.Data +import Futhark.Server +import Futhark.Server.Values qualified as FSV +import Futhark.Util (showText) +import System.IO.Temp (withSystemTempFile) +import System.Random (mkStdGen, random, randomIO) + +data PBTConfig = PBTConfig + { configNumTests :: Int32, + configMaxSize :: Int64, + configSeed :: Maybe Int32, + configShrinkTries :: Int + } + deriving (Show, Eq) + +data PropSpec = PropSpec + { psProp :: T.Text, + psGen :: Maybe T.Text, + psShrink :: Maybe T.Text, + psSize :: Maybe Int64, + psPPrint :: Maybe T.Text + } + deriving (Show, Eq) + +data PBTPhase = PBTPhase + { activeTest :: Maybe EntryName, -- property being tested (same for generator and shrinker phases) + phase :: Maybe EntryName, -- current entrypoint being called (property, generator, or shrinker) + shrinkWith :: Maybe EntryName, -- property or generator (only for auto) + phaseSize :: Maybe Int64, + phaseSeed :: Maybe Int32, + phaseTactic :: Maybe Int32 + -- , phaseValue :: Maybe T.Text + } + deriving (Show, Eq) + +type PBTOutput = Maybe T.Text + +type PBTFailure = T.Text + +lookupArgText :: T.Text -> [T.Text] -> Maybe T.Text +lookupArgText name = lookupArgWith name Just + +lookupArgRead :: (Read a) => T.Text -> [T.Text] -> Maybe a +lookupArgRead name = lookupArgWith name readMaybeText + +lookupArgWith :: T.Text -> (T.Text -> Maybe a) -> [T.Text] -> Maybe a +lookupArgWith name f = msum . map (stripCall name >=> f) + +stripCall :: T.Text -> T.Text -> Maybe T.Text +stripCall name = + T.stripSuffix ")" <=< T.stripPrefix (name <> "(") . T.strip + +readMaybeText :: (Read a) => T.Text -> Maybe a +readMaybeText t = + case reads (T.unpack t) of + [(x, "")] -> Just x + _ -> Nothing + +runPBT :: PBTConfig -> Server -> [PropSpec] -> IORef PBTPhase -> IO [Either PBTFailure PBTOutput] +runPBT config srv specs entryNameRef = + withSystemTempFile "pbt-scratch" $ \scratchBin _scratchHandle -> do + eps <- cmdErrorHandlerE "Failed to get entry points: " $ cmdEntryPoints srv -- error should not be reached by the user + forM specs $ \spec -> do + validation <- validateOneSpec srv eps spec + maybe (runOne spec config scratchBin srv entryNameRef) (pure . Left) validation + +validateOneSpec :: Server -> [EntryName] -> PropSpec -> IO (Maybe PBTFailure) +validateOneSpec srv eps spec = do + let prop = psProp spec + + result <- runExceptT $ do + unless (prop `elem` eps) $ + throwE $ + "Property entry point not found: " <> prop + + liftIO (validatePropTypes srv prop) >>= maybe (pure ()) throwE + + genName <- case psGen spec of + Nothing -> + throwE $ "No generator specified for " <> prop + Just g + | g `notElem` eps -> + throwE $ "Generator is not a server entry point: " <> g + Just g -> + pure g + + liftIO (validateGenTypes srv prop genName) >>= maybe (pure ()) throwE + + case psShrink spec of + Nothing -> pure () + Just "auto" -> pure () + Just sh -> do + unless (sh `elem` eps) $ + throwE $ + "Shrinker is not a server entry point: " <> sh + liftIO (validateShrinkTypes srv prop sh) >>= maybe (pure ()) throwE + + pure $ either Just (const Nothing) result + +validatePropTypes :: Server -> EntryName -> IO (Maybe PBTFailure) +validatePropTypes srv propName = fmap (either Just (const Nothing)) . runExceptT $ do + ins <- liftIO $ getInputTypes srv propName + case ins of + [_] -> pure () + [] -> throwE $ "Property " <> propName <> " has no inputs? Expected 1." + _ -> throwE $ "Property " <> propName <> " has " <> showText (length ins) <> " inputs; expected 1." + + out <- liftIO $ getOutputType srv propName + case out of + "bool" -> pure () + ty -> throwE $ "Property " <> propName <> " output must be bool, got: " <> ty + +getInputTypes :: Server -> EntryName -> IO [TypeName] +getInputTypes srv entry = do + ins <- + cmdErrorHandlerE ("Failed to get input types for " <> entry <> ": ") $ + cmdInputs srv entry + pure $ map inputType ins + +getOutputType :: Server -> EntryName -> IO TypeName +getOutputType s entry = do + out <- + cmdErrorHandlerE ("Failed to get output types for " <> entry <> ": ") $ + cmdOutput s entry + pure $ outputType out + +validateGenTypes :: Server -> EntryName -> EntryName -> IO (Maybe PBTFailure) +validateGenTypes srv propName genName = fmap (either Just (const Nothing)) . runExceptT $ do + propTy <- + liftIO (getSingleInputType srv propName) >>= \case + Left err -> throwE $ showText err + Right ty -> pure ty + + genOut <- liftIO $ getOutputType srv genName + + isMatch <- liftIO $ outsMatchType srv propTy genOut + + unless isMatch $ + throwE $ + "Generator type mismatch.\nProperty " + <> propName + <> " expects: " + <> propTy + <> "\nGenerator " + <> genName + <> " produces: " + <> showText genOut + <> "\nExpected generator outputs to equal the property input type " + <> "(possibly split for tuples/records)." + +validateShrinkTypes :: Server -> EntryName -> EntryName -> IO (Maybe PBTFailure) +validateShrinkTypes srv propName shrinkName = fmap (either Just (const Nothing)) . runExceptT $ do + propTy <- + liftIO (getSingleInputType srv propName) >>= \case + Left err -> throwE $ showText err + Right ty -> pure ty + + shrinkIns <- liftIO $ getInputTypes srv shrinkName + + case shrinkIns of + [xTy, randTy] -> do + unless (xTy == propTy) $ + throwE $ + "Shrinker input mismatch.\n property " + <> propName + <> " expects: " + <> propTy + <> "\n shrinker " + <> shrinkName + <> " takes x: " + <> xTy + <> "\nExpected shrinker's first input to be exactly the property input type." + + unless (randTy == "i32") $ + throwE $ + "Shrinker random-value type mismatch.\n shrinker " + <> shrinkName + <> " takes random value: " + <> randTy + <> "\nExpected random value to be i32." + tys -> + throwE $ + "Shrinker input arity mismatch.\n shrinker " + <> shrinkName + <> " inputs: " + <> showText tys + <> "\nExpected exactly 2 inputs: (" + <> propTy + <> ", i32)." + + shrinkOut <- liftIO $ getOutputType srv shrinkName + isMatch <- liftIO $ outsMatchType srv propTy shrinkOut + + unless isMatch $ + throwE $ + "Shrinker output mismatch.\n property " + <> propName + <> " expects: " + <> propTy + <> "\n shrinker " + <> shrinkName + <> " returns: " + <> showText shrinkOut + <> "\nExpected shrinker output to equal the property input type." + +runOne :: PropSpec -> PBTConfig -> FilePath -> Server -> IORef PBTPhase -> IO (Either PBTFailure PBTOutput) +runOne s config scratchBin srv entryNameRef = do + let propName = psProp s + genName = fromMaybe (error "missing generator") (psGen s) + size = fromMaybe (configMaxSize config) (psSize s) + numTests = configNumTests config + serverSize = "runPBT_size" + serverSeed = "runPBT_seed" + serverIn = "runPBT_input" + serverOk = "runPBT_ok" + + runExceptT $ do + let loop i + | i >= numTests = pure Nothing + | otherwise = do + randomValue <- liftIO (randomIO :: IO Int32) + let seed = fromMaybe randomValue (configSeed config) + let runUpdate ph = liftIO $ updatePhase (Just propName) (Just ph) Nothing (Just size) (Just seed) Nothing entryNameRef + + runUpdate propName + + checkIO $ sendGenInputs srv serverSize serverSeed genName size seed + + runUpdate genName + genOutE <- liftIO $ generatorPhase genName serverSize serverSeed serverIn + genOut <- either throwE pure genOutE + + runUpdate propName + + okE <- liftIO $ withCallKeepIns srv propName serverOk [serverIn] $ + \vOk -> getVal srv vOk + ok <- either (throwE . ("Property " <>)) pure okE + + if ok + then loop (i + 1) + else do + let failmsg = + "PBT FAIL: " + <> propName + <> " size=" + <> showText size + <> " seed=" + <> showText seed + <> " after " + <> showText i + <> " tests\n" + + shrinkRes <- case psShrink s of + Just "auto" -> liftIO $ autoShrinkLoop scratchBin srv propName genName serverIn size seed genOut entryNameRef + Just sh -> liftIO $ shrinkLoop scratchBin srv propName serverIn sh seed (configShrinkTries config) entryNameRef + Nothing -> pure (Right Nothing) + + case shrinkRes of + Left err -> throwE $ failmsg <> "Shrink failed: " <> err + Right (Just err) -> throwE $ failmsg <> "Shrink failed: " <> err + Right Nothing -> do + runUpdate "prettyPrint" + counterLog <- liftIO $ pPrintPhase propName serverIn + pure $ Just (failmsg <> counterLog) + loop 0 + where + generatorPhase genName serverSize serverSeed serverIn = do + let genOut = outName genName + withFreedVars srv [genOut] $ runExceptT $ do + errM <- liftIO $ callFreeIns srv genName genOut [serverSize, serverSeed] + maybe (pure ()) (throwE . (("Generator failed: " <> genName <> " has ") <>)) errM + liftIO $ copyVar scratchBin srv serverIn genOut + pure genOut + + pPrintPhase propName serverIn = do + inputTypes <- getInputTypes srv propName + case inputTypes of + (ty0 : _) -> do + prettyOutE <- case psPPrint s of + Just futPPrint -> do + let prettyOuts = outName futPPrint + withFreedVars srv [prettyOuts] $ runExceptT $ do + errM <- liftIO $ callFreeIns srv futPPrint prettyOuts [serverIn] + maybe (pure ()) (throwE . (("Pretty printer failed: " <> futPPrint <> " has ") <>)) errM + valE <- liftIO $ FSV.getValue srv prettyOuts + case valE of + Left err -> fail $ "getValue failed: " <> show err -- this is server error, not user error, so we can just fail + Right (U8Value _ bytes) -> pure $ T.pack [chr (fromIntegral b) | b <- SV.toList bytes] + Right _ -> pure $ T.pack "pretty printer returned non-u8 value" -- this is user error + Nothing -> + Right <$> prettyVar srv serverIn ty0 + case prettyOutE of + -- TODO: report necessary info like the example resulting in the counterexample and other useful information like size and seed. + Left err -> pure err -- report as user a 'regular' error/users fault + Right prettyOut -> pure $ "Minimal counterexample: " <> prettyOut + _ -> pure "Could not retrieve input types for counterexample log." + +-- Bridges IO (Maybe Error) into our ExceptT block +checkIO :: IO (Maybe e) -> ExceptT e IO () +checkIO act = liftIO act >>= maybe (pure ()) throwE + +updatePhase :: Maybe EntryName -> Maybe EntryName -> Maybe EntryName -> Maybe Int64 -> Maybe Int32 -> Maybe Int32 -> IORef PBTPhase -> IO () +updatePhase propName phase activeTest size seed tactic phaseRef = + writeIORef phaseRef $ + PBTPhase + { activeTest = propName, + phase = phase, + shrinkWith = activeTest, + phaseSize = size, + phaseSeed = seed, + phaseTactic = tactic + } + +autoShrinkLoop :: FilePath -> Server -> EntryName -> EntryName -> VarName -> Int64 -> Int32 -> VarName -> IORef PBTPhase -> IO (Either PBTFailure PBTOutput) +autoShrinkLoop scratchBin srv propName genName vIn size seed genOut phaseRef = runExceptT $ do + let autoShrinkUpdatePhase activeTest = + liftIO $ updatePhase (Just propName) (Just "autoShrinkLoop") activeTest (Just size) (Just seed) Nothing phaseRef + + vCand = "qc_try" + vOk = "qc_ok" + serverSize = "qc_size" + serverSeed = "qc_seed" + + -- 1. Validate property input arity using our Either-to-ExceptT logic + liftIO (getInputTypes srv propName) >>= \case + [_] -> pure () + [] -> throwE $ "Property " <> propName <> " has no inputs?" + tys -> throwE $ "Property " <> propName <> " has >1 input: " <> showText tys + + -- 2. The Loop + let loop i + | i <= 1 = pure Nothing + | otherwise = do + let newSize = i - 1 + + -- Use checkIO for the generator inputs + checkIO $ sendGenInputs srv serverSize serverSeed genName newSize seed + + -- Note: Since withFreedVars manages server-side resources, + -- we lift the whole block into IO then handle the result. + res <- liftIO $ withFreedVars srv [genOut, vCand] $ runExceptT $ do + liftIO $ autoShrinkUpdatePhase (Just genName) + errM <- liftIO $ callFreeIns srv genName genOut [serverSize, serverSeed] + maybe (pure ()) (throwE . (("Generator failed: " <> genName <> " has ") <>)) errM + + _ <- liftIO $ + freeOnException srv [vCand] $ + copyVar scratchBin srv vCand genOut + + liftIO $ autoShrinkUpdatePhase (Just propName) + okE <- liftIO $ withCallKeepIns srv propName vOk [vCand] $ + \vOk' -> getVal srv vOk' + ok <- either (throwE . ("Property " <>)) pure okE + + liftIO $ autoShrinkUpdatePhase Nothing + + if ok + then pure Nothing -- Shrink didn't find a smaller failure + else do + _ <- liftIO $ + freeOnException srv [vIn] $ + copyVar scratchBin srv vIn vCand + pure (Just newSize) -- Found a smaller failing size! + case res of + Left err -> throwE err + Right Nothing -> loop (i - 1) + Right (Just s) -> loop s + loop size + +data Step + = AcceptedShrink -- Property still failed with the new candidate + | NotAcceptedShrink -- Property passed with the new candidate + | ErrorInShrink T.Text -- shrinker error (including property failure in shrinker) + deriving (Eq, Show) + +shrinkLoop :: FilePath -> Server -> EntryName -> VarName -> EntryName -> Int32 -> Int -> IORef PBTPhase -> IO (Either PBTFailure PBTOutput) +shrinkLoop scratchBin srv propName vIn shrinkName seed numTries phaseRef = runExceptT $ do + -- 1. Setup Phase + oldRef <- liftIO $ readIORef phaseRef + let size = fromMaybe 0 (phaseSize oldRef) + shrinkUpdatePhase activeTest = liftIO $ updatePhase (Just propName) (Just shrinkName) activeTest (Just size) (Just seed) Nothing phaseRef + + shrinkUpdatePhase Nothing + + -- 2. Validate Types + liftIO (getSingleInputType srv propName) >>= \case + Left err -> throwE $ showText err + Right _ -> pure () + + seedTy <- + liftIO (getInputTypes srv shrinkName) >>= \case + [_, sTy] -> pure sTy + [] -> throwE $ "Shrinker " <> shrinkName <> " has no inputs?" + [_] -> throwE $ "Shrinker " <> shrinkName <> " has 1 input; expected 2 (x, random value)." + tys -> throwE $ "Shrinker " <> shrinkName <> " has " <> showText (length tys) <> " inputs; expected 2." + + unless (seedTy == "i32") $ + throwE $ + "Shrinker " <> shrinkName <> " random value must be i32, got: " <> seedTy + + let loop (pseudoRandom :: Int32) (acc :: Int) (totalCounter :: Int) + | acc >= numTries = pure Nothing + | otherwise = do + stepResultE <- liftIO $ oneStep size pseudoRandom + stepResult <- either (throwE . ("Error in shrinker: " <>)) pure stepResultE + + let branchGen = mkStdGen (fromIntegral pseudoRandom) + let (pseudoRandom', _) = random branchGen + + case stepResult of + AcceptedShrink -> + loop pseudoRandom' 0 (totalCounter + 1) -- Reset trials on success + NotAcceptedShrink -> + loop pseudoRandom' (acc + 1) (totalCounter + 1) -- Increment trials + ErrorInShrink err -> + throwE $ "Error in shrinker: " <> err + loop seed 0 0 + where + oneStep size tactic = do + -- Keeping the constants as requested + let vTry = "qc_try" + vOk = "qc_ok" + vTactic = "qc_tactic" + vInRetyped = vIn <> "_shrinktyped" + + let shrinkUpdatePhase activeTest = updatePhase (Just propName) (Just shrinkName) activeTest (Just size) (Just seed) Nothing phaseRef + + freeVars srv [vTactic] + putVal srv vTactic tactic + + _ <- + freeOnException srv [vInRetyped] $ + copyVar scratchBin srv vInRetyped vIn + + let shrinkOuts = outName shrinkName + shrinkUpdatePhase Nothing + + withFreedVars srv [shrinkOuts, vTry] $ runExceptT $ do + errE <- liftIO $ callFreeIns srv shrinkName shrinkOuts [vInRetyped, vTactic] + maybe (pure ()) (throwE . ((shrinkName <> " has ") <>)) errE + _ <- liftIO $ freeOnException srv [vTry] $ copyVar scratchBin srv vTry shrinkOuts + + liftIO $ shrinkUpdatePhase Nothing + + okE <- liftIO $ withCallKeepIns srv propName vOk [vTry] $ \vOk' -> getVal srv vOk' + ok <- either (throwE . ("Property " <>)) pure okE + + liftIO $ shrinkUpdatePhase Nothing + + case ok of + True -> pure NotAcceptedShrink + False -> do + liftIO $ freeVars srv [vIn] + _ <- liftIO $ copyVar scratchBin srv vIn vTry + pure AcceptedShrink + +sendGenInputs :: Server -> VarName -> VarName -> VarName -> Int64 -> Int32 -> IO (Maybe PBTFailure) +sendGenInputs srv sizeName seedName genName size seed = do + insE <- cmdInputs srv genName + case insE of + -- Our fault since this should not happen for the user + Left err -> fail $ show err + Right ins' -> case map inputType ins' of + [sizeTy, seedTy] + | sizeTy == "i64" && seedTy == "i32" -> do + putVal srv sizeName size + putVal srv seedName seed + pure Nothing + | otherwise -> + pure . Just $ T.pack $ "Expected size and seed to be i64 and i32, got: size type=" <> T.unpack sizeTy <> " and seed type=" <> T.unpack seedTy + tys -> + pure . Just $ T.pack $ "Expected generator to have exactly two inputs, got types: " <> show tys + +-- | Name of out-variable for this entry point. +outName :: EntryName -> VarName +outName = (<> "_out") + +putVal :: (PutValue1 a) => Server -> T.Text -> a -> IO () +putVal s name x = do + let v = putValue1 x + cmdErrorHandlerM ("putValue failed for " <> name <> ": ") $ FSV.putValue s name v + +freeVars :: Server -> [VarName] -> IO () +freeVars s vs = do + mFail <- cmdFree s vs + case mFail of + Nothing -> pure () + Just err + | any (T.isPrefixOf "Unknown variable:") (failureMsg err) -> pure () + | otherwise -> + fail $ "cmdFree failed for " <> show vs <> ": " <> show (failureMsg err) + +callFreeIns :: Server -> EntryName -> VarName -> [VarName] -> IO (Maybe PBTFailure) +callFreeIns s entry out ins = do + freeVars s [out] + r <- cmdCall s entry out ins + freeVars s ins + either (pure . handleRuntimeError entry) (const $ pure Nothing) r + +isRuntimeError :: CmdFailure -> Bool +isRuntimeError failure = any ("runtime: " `T.isPrefixOf`) (failureLog failure) + +handleRuntimeError :: EntryName -> CmdFailure -> Maybe PBTFailure +handleRuntimeError entry err + | isRuntimeError err = Just $ "Runtime error: " <> showText (failureMsg err) + | otherwise = fail . T.unpack $ "Fatal Error on " <> entry + <> ": " <> showText (failureMsg err) + +callKeepIns :: Server -> EntryName -> VarName -> [VarName] -> IO (Maybe PBTFailure) +callKeepIns s entry out ins = do + freeVars s [out] + r <- cmdCall s entry out ins + either (pure . handleRuntimeError entry) (const $ pure Nothing) r + +freeOnException :: Server -> [VarName] -> IO a -> IO a +freeOnException srv vs action = + action `onException` freeVars srv vs + +withCallKeepIns :: Server -> EntryName -> VarName -> [VarName] -> (VarName -> IO a) -> IO (Either PBTFailure a) +withCallKeepIns srv entry out ins k = do + errM <- callKeepIns srv entry out ins + maybe (Right <$> (k out `finally` freeVars srv [out])) + (pure . Left . ((entry <> " has ") <>)) + errM + +withFreedVars :: Server -> [VarName] -> IO a -> IO a +withFreedVars srv vs action = + action `finally` freeVars srv vs + +-- | Bracket a single temporary var name. +withFreedVar :: Server -> VarName -> IO a -> IO a +withFreedVar srv v = withFreedVars srv [v] + +copyVar :: FilePath -> Server -> VarName -> VarName -> IO () +copyVar scratchBin srv outVar inVar = do + typ <- cmdErrorHandlerE "cmdType failed: " $ cmdType srv inVar + cmdErrorHandlerM "cmdStore failed: " $ cmdStore srv scratchBin [inVar] + freeVars srv [outVar] + cmdErrorHandlerM "cmdRestore failed: " $ cmdRestore srv scratchBin [(outVar, typ)] + +cmdErrorHandlerM :: T.Text -> IO (Maybe CmdFailure) -> IO () +cmdErrorHandlerM msg action = action >>= maybe (pure ()) (fail . format) + where + format err = T.unpack msg <> show err + +cmdErrorHandlerE :: T.Text -> IO (Either CmdFailure a) -> IO a +cmdErrorHandlerE msg action = action >>= either (fail . format) pure + where + format err = T.unpack msg <> show err + +getVal :: (GetValue a) => Server -> VarName -> IO a +getVal srv name = do + v <- getDataVal srv name + case getValue v of + Just b -> pure b + Nothing -> fail $ "Expected " <> T.unpack name <> " to decode, got: " <> T.unpack (valueText v) + +getDataVal :: Server -> VarName -> IO Value +getDataVal s name = do + r <- FSV.getValue s name + case r of + Left msg -> fail $ "getValue failed for " <> T.unpack name <> ": " <> T.unpack msg + Right v -> pure v + +prettyVar :: Server -> VarName -> TypeName -> IO T.Text +prettyVar srv v ty = do + fieldsRes <- cmdFields srv ty + case fieldsRes of + Right fieldLines -> do + -- convert from Field to text and type pairs + + let fnames = map fieldName fieldLines + ftypes = map fieldType fieldLines + isTuple = + and + [ fname == showText i + | (fname, i) <- zip fnames [0 .. (length fnames - 1)] + ] + + rendered <- forM (zip fnames ftypes) $ \(fname, fty) -> do + let tmp = + if isTuple + then v <> "_tup_" <> fname + else v <> "_rec_" <> fname + + sField <- withFreedVar srv tmp $ do + cmdErrorHandlerM ("cmdProject failed for field " <> fname <> ": ") $ cmdProject srv tmp v fname + + prettyVar srv tmp fty + + if isTuple + then pure sField + else pure (fname <> " = " <> sField) + + if isTuple + then pure $ "(" <> T.intercalate ", " rendered <> ")" + else do + pure $ "{" <> T.intercalate ", " rendered <> "}" + Left _notARecord -> do + valRes <- FSV.getValue srv v + case valRes of + Right val -> pure (valueText val) + Left _opaqueOrFailed -> pure (" ty <> ">") + +getSingleInputType :: Server -> EntryName -> IO (Either PBTFailure TypeName) +getSingleInputType srv ep = do + tys <- getInputTypes srv ep + case tys of + [ty] -> pure $ Right ty + [] -> pure $ Left $ T.pack $ "Entrypoint " <> T.unpack ep <> " has no inputs (expected 1)." + _ -> pure $ Left $ T.pack $ "Entrypoint " <> T.unpack ep <> " has >1 input (expected 1): " <> show tys + +outsMatchType :: Server -> TypeName -> TypeName -> IO Bool +outsMatchType srv propTy out + | out == propTy = pure True + | otherwise = do + res <- cmdFields srv propTy + pure $ either (const False) (\fs -> [out] == map fieldType fs) res diff --git a/src/Futhark/Test/Spec.hs b/src/Futhark/Test/Spec.hs index f0959756c6..cc1363621b 100644 --- a/src/Futhark/Test/Spec.hs +++ b/src/Futhark/Test/Spec.hs @@ -13,6 +13,7 @@ module Futhark.Test.Spec TestAction (..), ExpectedError (..), InputOutputs (..), + PropertyCase (..), TestRun (..), ExpectedResult (..), Success (..), @@ -26,6 +27,7 @@ import Control.Applicative import Control.Exception (catch) import Control.Monad import Data.Char +import Data.Either (partitionEithers) import Data.Functor import Data.List qualified as L import Data.Map.Strict qualified as M @@ -62,7 +64,7 @@ data ProgramTest = ProgramTest -- | How to test a program. data TestAction = CompileTimeFailure ExpectedError - | RunCases [InputOutputs] [StructureTest] [WarningTest] + | RunCases [InputOutputs] [StructureTest] [WarningTest] [PropertyCase] deriving (Show) -- | Input and output pairs for some entry point(s). @@ -72,6 +74,10 @@ data InputOutputs = InputOutputs } deriving (Show) +data PropertyCase = PropertyCase + { propertyEntryPoint :: T.Text} + deriving (Show) + -- | The error expected for a negative test. data ExpectedError = AnyError @@ -217,11 +223,35 @@ parseAction :: Parser () -> Parser TestAction parseAction sep = choice [ CompileTimeFailure <$> (lexstr' "error:" *> parseExpectedError sep), + try parseAsProperty, + parseAsRunCase + ] + where + parseAsProperty = do + props <- parseProperty sep + pure $ RunCases [] [] [] props + + parseAsRunCase = RunCases <$> parseInputOutputs sep <*> many (parseExpectedStructure sep) <*> many (parseWarning sep) - ] + <*> pure [] + +parseProperty :: Parser () -> Parser [PropertyCase] +parseProperty sep = do + entrys <- parseEntryPointsProp sep + pure $ + if null entrys + then [] + else map PropertyCase entrys + +parseEntryPointsProp :: Parser () -> Parser [T.Text] +parseEntryPointsProp sep = + lexeme' "property:" *> many entry <* sep + where + constituent c = not (isSpace c) + entry = lexeme' $ takeWhile1P Nothing constituent parseInputOutputs :: Parser () -> Parser [InputOutputs] parseInputOutputs sep = do @@ -382,9 +412,17 @@ pProgramTest = do optional ("--" *> sep *> testSpec sep) <* pEndOfTestBlock <* many pNonTestLine case maybe_spec of Just spec - | RunCases old_cases structures warnings <- testAction spec -> do - cases <- many $ pInputOutputs <* many pNonTestLine - pure spec {testAction = RunCases (old_cases ++ concat cases) structures warnings} + | RunCases old_cases structures warnings old_properties <- testAction spec -> do + let pAnyBlock = (Left <$> pInputOutputs) <|> (Right <$> pPropertyCases) + restBlocks <- many (pAnyBlock <* many pNonTestLine) + let (restCases, restProperties) = partitionEithers restBlocks + pure spec + { testAction = RunCases + (old_cases ++ concat restCases) + structures + warnings + (old_properties ++ concat restProperties) + } | otherwise -> many pNonTestLine *> notFollowedBy "-- ==" @@ -396,20 +434,22 @@ pProgramTest = do sep = void $ hspace *> optional (try $ eol *> "--" *> sep) noTest = - ProgramTest mempty mempty (RunCases mempty mempty mempty) + ProgramTest mempty mempty (RunCases mempty mempty mempty mempty) pEndOfTestBlock = (void eol <|> eof) *> notFollowedBy "--" pNonTestLine = void $ notFollowedBy "-- ==" *> restOfLine - pInputOutputs = + pInputOutputs = try $ "--" *> sep *> parseDescription sep *> parseInputOutputs sep <* pEndOfTestBlock + pPropertyCases = + "--" *> sep *> parseDescription sep *> parseProperty sep <* pEndOfTestBlock validate :: FilePath -> ProgramTest -> Either String ProgramTest validate path pt = do case testAction pt of CompileTimeFailure {} -> pure pt - RunCases ios _ _ -> do + RunCases ios _ _ _ -> do mapM_ (noDups . map runDescription . iosTestRuns) ios Right pt where diff --git a/tests_property/.gitignore b/tests_property/.gitignore new file mode 100644 index 0000000000..d8c15065f9 --- /dev/null +++ b/tests_property/.gitignore @@ -0,0 +1,5 @@ +lib/ +*/** +!*/ +!**/*.fut +!**/*.out diff --git a/tests_property/ArrayTests/ArrayArray.fut b/tests_property/ArrayTests/ArrayArray.fut new file mode 100644 index 0000000000..141773735d --- /dev/null +++ b/tests_property/ArrayTests/ArrayArray.fut @@ -0,0 +1,201 @@ +-- == +-- property: prop_matrix_sums_succ + +-- == +-- property: prop_matrix_sums_fail + +-- Property target: +-- For a rectangular matrix, compute the sum of each row. +-- Check these row-sums are nondecreasing: sums[0] <= sums[1] <= ... <= sums[r-1]. + +let row_sums (xss: [][]i32) : []i32 = + map (\xs -> reduce (+) 0i32 xs) xss + +let nondecreasing (xs: []i32) : bool = + let n = length xs + in if n < 2 then true + else + map2 (<=) ((take (n-1) xs):>[n-1]i32) ((drop 1 xs):>[n-1]i32) + |> reduce (&&) true + +-- Succeeding generator: same row length everywhere, and row sums increase with row index. +entry gen_matrix_sums (size: i64) (seed: i32) : [][]i32 = + let s = if size < 0 then 0 else size + let r_i32 = if s == 0 then 0 else 1 + (i32.abs seed) % i32.i64 (s + 1) + let c_i32 = if s == 0 then 0 else 1 + (i32.abs (seed * 17 + 3)) % i32.i64 (s + 1) + let r = i64.i32 r_i32 + let c = i64.i32 c_i32 + + let base_row : [c]i32 = + iota c |> map (\j -> i32.i64 j) + + let make_row (ri: i64) : [c]i32 = + let offset = (i32.i64 ri) * 10i32 + in map (\x -> x + offset) base_row + + in tabulate r make_row + +#[prop(gen(gen_matrix_sums), shrink(shrink_matrix_sums))] +entry prop_matrix_sums_succ (input: [][]i32) : bool = + nondecreasing (row_sums input) + +-- New protocol shrinker: +-- (xss, tactic) -> (xss', status) +-- +-- tactic 0: try dropping the last row +-- tactic 1: try dropping the first row +-- tactic >= 2: stop shrinking +-- +-- status i8: +-- 0 = produced candidate (normal) +-- 1 = produced candidate but "advance tactic" hint (runner rule: if FAIL and status=1 then tactic=0 anyway, but we keep the channel) +-- 2 = stop +entry shrink_matrix_sums (xss: [][]i32) (random: i32) : [][]i32 = + let tactic = random % 2 + let r = length xss in + if r <= 1 then + xss + else if tactic == 0 then + -- drop last row + let xss' = take (r-1) xss + in xss' + else + -- drop first row + let xss' = drop 1 xss + in xss' + + +entry gen_matrix_sums_bad (size: i64) (seed: i32) : [][]i32 = + let xss = gen_matrix_sums size seed + let r = length xss + in if r < 2 then + xss + else + -- swap first two rows + let a = xss[0] + let b = xss[1] + in [b] ++ [a] ++ drop 2 xss + +-- Helper: clamp index to [0..n-1] +let clamp_index (n: i64) (i: i32) : i64 = + let ii = i64.i32 i + in if n <= 0 then 0 + else if ii < 0 then 0 + else if ii >= n then n-1 + else ii + +-- Remove element at index i from a 1D array (keeps order). +let remove_at (i: i32) (xs: []i32) : []i32 = + let n = length xs + in if n == 0 then xs + else + let ii = clamp_index n i + let pre = take ii xs + let post = drop (ii+1) xs + in pre ++ post + +-- Remove row i from a 2D array. +let remove_row (i: i32) (xss: [][]i32) : [][]i32 = + let r = length xss + in if r == 0 then xss + else + let ii = clamp_index r i + let pre = take ii xss + let post = drop (ii+1) xss + in pre ++ post + +let remove_col (j: i32) (xss: [][]i32) : [][]i32 = + let r = length xss + in if r == 0 then xss + else + let c = length xss[0] + in if c <= 1 then xss + else + let jj = clamp_index c j + let newc = c - 1 + let mk_row (row: []i32) : [newc]i32 = + tabulate newc (\k -> + let src = if k < jj then k else k + 1 + in row[src]) + in (map mk_row xss) :> [][]i32 + +-- Shrink a scalar toward 0 (simple and terminating). +-- If already 0 -> unchanged. +-- If abs <= 1 -> goes to 0. +-- Else -> halves toward 0 (keeps sign). +let shrink_i32 (v: i32) : i32 = + if v == 0i32 then 0i32 + else if i32.abs v <= 1i32 then 0i32 + else v / 2i32 + +-- Update a single cell (ri,ci) in a rectangular matrix [r][c]i32. +-- Always returns [r][c]i32 (shape-preserving). +let update_cell_rc [r][c] (ri: i64) (ci: i64) (xss: [r][c]i32) : [r][c]i32 = + let r_ok = 0 <= ri && ri < r + let c_ok = 0 <= ci && ci < c + in if !(r_ok && c_ok) then xss + else + let old = xss[ri][ci] + let new = shrink_i32 old + in if new == old then xss + else + tabulate r (\i -> + tabulate c (\j -> + if i == ri && j == ci then new else xss[i][j])) + + +entry shrink_matrix (xss: [][]i32) (random: i32) : [][]i32 = + let tactic = random % 3 + let r : i64 = length xss + let c : i64 = if r == 0 then 0 else length xss[0] + + -- rectangular check (needed for column removal + cell shrink) + let rect : bool = + if r == 0 then true + else reduce (&&) true (map (\row -> length row == c) xss) + + let rowCount : i64 = if r > 1 then r else 0 + let colCount : i64 = if rect && c > 1 then c else 0 + let scalarCount : i64 = if rect then r * c else 0 + + let t : i64 = if tactic < 0i32 then 0i64 else i64.i32 tactic + + in if t < rowCount then + -- remove row t + remove_row (i32.i64 t) xss + + else if t < rowCount + colCount then + -- remove column j = t-rowCount + let j : i32 = i32.i64 (t - rowCount) + in remove_col j xss + + else if t < rowCount + colCount + scalarCount then + -- shrink one cell k = t-rowCount-colCount + let k : i64 = t - rowCount - colCount + in if r == 0 || c == 0 then + xss + else + let ri : i64 = k / c + let ci : i64 = k % c + let xss_rc : [r][c]i32 = xss :> [r][c]i32 + let old : i32 = xss_rc[ri][ci] + let new : i32 = shrink_i32 old + in if new == old then + -- no-op: advance tactic + xss + else + let xss_rc' : [r][c]i32 = + tabulate r (\i -> + tabulate c (\j -> + if i == ri && j == ci then new else xss_rc[i][j])) + let xss' : [][]i32 = xss_rc' :> [][]i32 + in xss' + + else + -- exhausted tactics + xss + + +#[prop(gen(gen_matrix_sums_bad), shrink(shrink_matrix))] +entry prop_matrix_sums_fail (input: [][]i32) : bool = + nondecreasing (row_sums input) \ No newline at end of file diff --git a/tests_property/ArrayTests/ArrayRecord.fut b/tests_property/ArrayTests/ArrayRecord.fut new file mode 100644 index 0000000000..6954cfe387 --- /dev/null +++ b/tests_property/ArrayTests/ArrayRecord.fut @@ -0,0 +1,96 @@ +-- == +-- property: prop_record_sums_succ + +-- == +-- property: prop_record_sums_fail + +import "../libraries/toString/toString" + +type record = { s: i32, a: i32 } +type~ arr = []record + +let all_equal (r: record) : bool = + r.s == r.a + +let prop_all_equal (xs: arr) : bool = + map all_equal xs |> reduce (&&) true + +entry gen_record_sums (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + in replicate n {s=1i32, a=1i32} + +#[prop(gen(gen_record_sums))] +entry prop_record_sums_succ (input: arr) : bool = + prop_all_equal input + +entry gen_record_sums_fail (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + in tabulate n (\i -> + if i == 0i64 then {s=1i32, a=1i32} + else {s=2i32, a=1i32}) + +let shrink_i32 (x: i32) : i32 = + if x == 0i32 then 0i32 + else if i32.abs x <= 1i32 then 0i32 + else x / 2i32 + +let shrink_record_field (r: record) (field: i32) : (record, bool) = + if field == 0i32 then + let s' = shrink_i32 r.s + let r' = {s = s', a = r.a} + in (r', r' != r) + else + let a' = shrink_i32 r.a + let r' = {s = r.s, a = a'} + in (r', r' != r) + +let replace_at [n] (xs: [n]record) (idx: i64) (v: record) : [n]record = + tabulate n (\i -> if i == idx then v else xs[i]) + +entry shrink_arr_record (xs: arr) (random: i32) : arr = + let n : i64 = length xs + let tactic = random % i32.i64 n + + let field_tactics : i32 = 2i32 * i32.i64 n + let total_tactics : i32 = + if n <= 1 then field_tactics + else 2i32 + field_tactics + + let t : i32 = if tactic < 0i32 then 0i32 else tactic + in if t >= total_tactics then + xs + else if n > 1 && t == 0i32 then + let xs' = take (n - 1) xs + in xs' + else if n > 1 && t == 1i32 then + let xs' = drop 1 xs + in xs' + else + let loc : i32 = if n > 1 then t - 2i32 else t + let idx : i64 = i64.i32 (loc / 2i32) + let field : i32 = loc % 2i32 + let xsn : [n]record = xs :> [n]record + let old = xsn[idx] + let (new, changed) = shrink_record_field old field + let ysn = replace_at xsn idx new + let ys : arr = ysn :> arr + in if changed then ys else xs + +#[prop(gen(gen_record_sums_fail), shrink(shrink_arr_record), pprint(pp_arrRecord))] +entry prop_record_sums_fail (input: arr) : bool = + prop_all_equal input + +def pp_record (r: record) : []u8 = + "{" ++ + "s: " ++ i32_to_string r.s ++ + ", a: " ++ i32_to_string r.a ++ + "}" + +entry pp_arrRecord (input: arr) : []u8 = + let n = length input + let body = + loop acc = "" + for i < n do + let sep = if i == 0 then "" else ", " + in acc ++ sep ++ pp_record input[i] + in "[" ++ body ++ "]" \ No newline at end of file diff --git a/tests_property/ArrayTests/ArrayRecord.out b/tests_property/ArrayTests/ArrayRecord.out new file mode 100644 index 0000000000..24a64c3610 --- /dev/null +++ b/tests_property/ArrayTests/ArrayRecord.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_record_sums_fail size=50 seed=REDACTED after N tests +Minimal counterexample: [{s: 1, a: 0}] diff --git a/tests_property/ArrayTests/ArrayRecord2.fut b/tests_property/ArrayTests/ArrayRecord2.fut new file mode 100644 index 0000000000..2eebcaa615 --- /dev/null +++ b/tests_property/ArrayTests/ArrayRecord2.fut @@ -0,0 +1,86 @@ +-- == +-- property: prop_record_sums_succ + +-- == +-- property: prop_record_sums_fail + +-- File 2: ONLY record is a type alias (array is []record) +import "../libraries/toString/toString" + +type record = { s: i32, a: i32 } + +let all_equal (r: record) : bool = + r.s == r.a + +let prop_all_equal (xs: []record) : bool = + map all_equal xs |> reduce (&&) true + +entry gen_record_sums (size: i64) (_: i32) : []record = + let n = if size < 0 then 0 else size + in replicate n {s=1i32, a=1i32} + +#[prop(gen(gen_record_sums))] +entry prop_record_sums_succ (input: []record) : bool = + prop_all_equal input + +entry gen_record_sums_fail (size: i64) (_: i32) : []record = + let n = if size < 0 then 0 else size + in tabulate n (\i -> + if i == 0i64 then {s=1i32, a=1i32} + else {s=2i32, a=1i32}) + +let shrink_i32 (v: i32) : i32 = + if v == 0i32 then 0i32 + else if i32.abs v <= 1i32 then 0i32 + else v / 2i32 + +let update_at_n [n] (kk: i64) (xs: [n]record) : ([n]record, bool) = + let r = xs[kk] + let s' = shrink_i32 r.s + let a' = shrink_i32 r.a + let r' = + if s' != r.s then {s = s', a = r.a} + else if a' != r.a then {s = r.s, a = a'} + else r + let changed = r' != r + let xs' = tabulate n (\i -> if i == kk then r' else xs[i]) + in (xs', changed) + +entry shrink_arr_record (xs: []record) (random: i32) : []record = + let n : i64 = length xs + let tactic = random % i32.i64 n + let t : i32 = if tactic < 0i32 then 0i32 else tactic + let n_i32 : i32 = i32.i64 n + in if n == 0 then + xs + else if t < n_i32 then + let kk = + let k64 = i64.i32 t + in if k64 < 0 then 0 + else if k64 >= n then n-1 + else k64 + let xsN : [n]record = xs :> [n]record + let (xsN', changed) = update_at_n kk xsN + let out : []record = xsN' :> []record + in if changed then out else xs + else + xs + +#[prop(gen(gen_record_sums_fail), shrink(shrink_arr_record), pprint(pp_arrRecord))] +entry prop_record_sums_fail (input: []record) : bool = + prop_all_equal input + +def pp_record (r: record) : []u8 = + "{" ++ + "s: " ++ i32_to_string r.s ++ + ", a: " ++ i32_to_string r.a ++ + "}" + +entry pp_arrRecord (input: []record) : []u8 = + let n = length input + let body = + loop acc = "" + for i < n do + let sep = if i == 0 then "" else ", " + in acc ++ sep ++ pp_record input[i] + in "[" ++ body ++ "]" \ No newline at end of file diff --git a/tests_property/ArrayTests/ArrayRecord3.fut b/tests_property/ArrayTests/ArrayRecord3.fut new file mode 100644 index 0000000000..bba6727c22 --- /dev/null +++ b/tests_property/ArrayTests/ArrayRecord3.fut @@ -0,0 +1,86 @@ +-- == +-- property: prop_record_sums_succ + +-- == +-- property: prop_record_sums_fail + +-- File 3: ONLY array is a type alias (record is INLINE, arr = []{...}) +import "../libraries/toString/toString" + +type~ arr = []{ s: i32, a: i32 } + +let all_equal (r: { s: i32, a: i32 }) : bool = + r.s == r.a + +let prop_all_equal (xs: arr) : bool = + map all_equal xs |> reduce (&&) true + +entry gen_record_sums (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + in replicate n {s=1i32, a=1i32} + +#[prop(gen(gen_record_sums))] +entry prop_record_sums_succ (input: arr) : bool = + prop_all_equal input + +entry gen_record_sums_fail (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + in tabulate n (\i -> + if i == 0i64 then {s=1i32, a=1i32} + else {s=2i32, a=1i32}) + +let shrink_i32 (v: i32) : i32 = + if v == 0i32 then 0i32 + else if i32.abs v <= 1i32 then 0i32 + else v / 2i32 + +let update_at_n [n] (kk: i64) (xs: [n]{ s: i32, a: i32 }) : ([n]{ s: i32, a: i32 }, bool) = + let r = xs[kk] + let s' = shrink_i32 r.s + let a' = shrink_i32 r.a + let r' = + if s' != r.s then {s = s', a = r.a} + else if a' != r.a then {s = r.s, a = a'} + else r + let changed = r' != r + let xs' = tabulate n (\i -> if i == kk then r' else xs[i]) + in (xs', changed) + +entry shrink_arr_record (xs: arr) (random: i32) : arr = + let n : i64 = length xs + let tactic = random % i32.i64 n + let t : i32 = if tactic < 0i32 then 0i32 else tactic + let n_i32 : i32 = i32.i64 n + in if n == 0 then + xs + else if t < n_i32 then + let kk = + let k64 = i64.i32 t + in if k64 < 0 then 0 + else if k64 >= n then n-1 + else k64 + let xsN : [n]{ s: i32, a: i32 } = xs :> [n]{ s: i32, a: i32 } + let (xsN', changed) = update_at_n kk xsN + let out : arr = xsN' :> arr + in if changed then out else xs + else + xs + +#[prop(gen(gen_record_sums_fail), shrink(shrink_arr_record), pprint(pp_arrRecord))] +entry prop_record_sums_fail (input: arr) : bool = + prop_all_equal input + +def pp_record (r: { s: i32, a: i32 }) : []u8 = + "{" ++ + "s: " ++ i32_to_string r.s ++ + ", a: " ++ i32_to_string r.a ++ + "}" + +entry pp_arrRecord (input: arr) : []u8 = + let n = length input + let body = + loop acc = "" + for i < n do + let sep = if i == 0 then "" else ", " + in acc ++ sep ++ pp_record input[i] + in "[" ++ body ++ "]" \ No newline at end of file diff --git a/tests_property/ArrayTests/ArrayRecord4.fut b/tests_property/ArrayTests/ArrayRecord4.fut new file mode 100644 index 0000000000..aadb7ed00c --- /dev/null +++ b/tests_property/ArrayTests/ArrayRecord4.fut @@ -0,0 +1,94 @@ +-- == +-- property: prop_record_sums_succ + +-- == +-- property: prop_record_sums_fail + +-- File 4: NO type aliases (record inline, array is []{...}) +import "../libraries/toString/toString" + +let all_equal (r: { s: i32, a: i32 }) : bool = + r.s == r.a + +let prop_all_equal (xs: []{ s: i32, a: i32 }) : bool = + map all_equal xs |> reduce (&&) true + +entry gen_record_sums (size: i64) (_: i32) : []{ s: i32, a: i32 } = + let n = if size < 0 then 0 else size + in replicate n {s=1i32, a=1i32} + +#[prop(gen(gen_record_sums))] +entry prop_record_sums_succ (input: []{ s: i32, a: i32 }) : bool = + prop_all_equal input + +entry gen_record_sums_fail (size: i64) (_: i32) : []{ s: i32, a: i32 } = + let n = if size < 0 then 0 else size + in tabulate n (\i -> + if i == 0i64 then {s=1i32, a=1i32} + else {s=2i32, a=1i32}) + +let shrink_i32 (v: i32) : i32 = + if v == 0i32 then 0i32 + else if i32.abs v <= 1i32 then 0i32 + else v / 2i32 + +let shrink_record_field (r: { s: i32, a: i32 }) (field: i32) : ({ s: i32, a: i32 }, bool) = + if field == 0i32 then + let s' = shrink_i32 r.s + let r' = {s = s', a = r.a} + in (r', r' != r) + else + let a' = shrink_i32 r.a + let r' = {s = r.s, a = a'} + in (r', r' != r) + +let replace_at [n] (xs: [n]{ s: i32, a: i32 }) (idx: i64) (v: { s: i32, a: i32 }) : [n]{ s: i32, a: i32 } = + tabulate n (\i -> if i == idx then v else xs[i]) + +entry shrink_arr_record (xs: []{ s: i32, a: i32 }) (random: i32) : []{ s: i32, a: i32 } = + let n : i64 = length xs + let tactic = random % i32.i64 n + + let field_tactics : i32 = 2i32 * i32.i64 n + let total_tactics : i32 = + if n <= 1 then field_tactics + else 2i32 + field_tactics + + let t : i32 = if tactic < 0i32 then 0i32 else tactic + in if t >= total_tactics then + xs + else if n > 1 && t == 0i32 then + let xs' = take (n - 1) xs + in xs' + else if n > 1 && t == 1i32 then + let xs' = drop 1 xs + in xs' + else + let loc : i32 = if n > 1 then t - 2i32 else t + let idx : i64 = i64.i32 (loc / 2i32) + let field : i32 = loc % 2i32 + let xsn : [n]{ s: i32, a: i32 } = xs :> [n]{ s: i32, a: i32 } + let old = xsn[idx] + let (new, changed) = shrink_record_field old field + let ysn = replace_at xsn idx new + let ys = ysn :> [n]{ s: i32, a: i32 } + in if changed then ys else xs + +#[prop(gen(gen_record_sums_fail), shrink(shrink_arr_record), pprint(pp_arrRecord))] +entry prop_record_sums_fail (input: []{ s: i32, a: i32 }) : bool = + prop_all_equal input + +def pp_record (r: { s: i32, a: i32 }) : []u8 = + "{" ++ + "s: " ++ i32_to_string r.s ++ + ", a: " ++ i32_to_string r.a ++ + "}" + +entry pp_arrRecord (input: []{ s: i32, a: i32 }) : []u8 = + let n = length input + let body = + loop acc = "" + for i < n do + let sep = if i == 0 then "" else ", " + in acc ++ sep ++ pp_record input[i] + in "[" ++ body ++ "]" \ No newline at end of file diff --git a/tests_property/ArrayTests/ArrayRecord4.out b/tests_property/ArrayTests/ArrayRecord4.out new file mode 100644 index 0000000000..24a64c3610 --- /dev/null +++ b/tests_property/ArrayTests/ArrayRecord4.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_record_sums_fail size=50 seed=REDACTED after N tests +Minimal counterexample: [{s: 1, a: 0}] diff --git a/tests_property/ArrayTests/ArrayRecordAutoShrink.fut b/tests_property/ArrayTests/ArrayRecordAutoShrink.fut new file mode 100644 index 0000000000..5298198360 --- /dev/null +++ b/tests_property/ArrayTests/ArrayRecordAutoShrink.fut @@ -0,0 +1,67 @@ +-- == +-- property: prop_record_sums_succ + +-- == +-- property: prop_record_sums_fail + +-- File 1: BOTH are type aliases (record + array) +import "../libraries/toString/toString" + +type record = { s: i32, a: i32 } +type~ arr = []record + +let all_equal (r: record) : bool = + r.s == r.a + +let prop_all_equal (xs: arr) : bool = + map all_equal xs |> reduce (&&) true + +entry gen_record_sums (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + in replicate n {s=1i32, a=1i32} + +#[prop(gen(gen_record_sums))] +entry prop_record_sums_succ (input: arr) : bool = + prop_all_equal input + +entry gen_record_sums_fail (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + in tabulate n (\i -> + if i == 0i64 then {s=1i32, a=1i32} + else {s=2i32, a=1i32}) + +let shrink_i32 (v: i32) : i32 = + if v == 0i32 then 0i32 + else if i32.abs v <= 1i32 then 0i32 + else v / 2i32 + +let update_at_n [n] (kk: i64) (xs: [n]record) : ([n]record, bool) = + let r = xs[kk] + let s' = shrink_i32 r.s + let a' = shrink_i32 r.a + let r' = + if s' != r.s then {s = s', a = r.a} + else if a' != r.a then {s = r.s, a = a'} + else r + let changed = r' != r + let xs' = tabulate n (\i -> if i == kk then r' else xs[i]) + in (xs', changed) + +#[prop(gen(gen_record_sums_fail), shrink(auto), pprint(pp_arrRecord))] +entry prop_record_sums_fail (input: arr) : bool = + prop_all_equal input + +def pp_record (r: record) : []u8 = + "{" ++ + "s: " ++ i32_to_string r.s ++ + ", a: " ++ i32_to_string r.a ++ + "}" + +entry pp_arrRecord (input: arr) : []u8 = + let n = length input + let body = + loop acc = "" + for i < n do + let sep = if i == 0 then "" else ", " + in acc ++ sep ++ pp_record input[i] + in "[" ++ body ++ "]" \ No newline at end of file diff --git a/tests_property/ArrayTests/ArrayRecordAutoShrink.out b/tests_property/ArrayTests/ArrayRecordAutoShrink.out new file mode 100644 index 0000000000..4946c9299c --- /dev/null +++ b/tests_property/ArrayTests/ArrayRecordAutoShrink.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_record_sums_fail size=50 seed=REDACTED after N tests +Minimal counterexample: [{s: 1, a: 1}, {s: 2, a: 1}] diff --git a/tests_property/ArrayTests/Arrayi32(2).fut b/tests_property/ArrayTests/Arrayi32(2).fut new file mode 100644 index 0000000000..5f32f83a50 --- /dev/null +++ b/tests_property/ArrayTests/Arrayi32(2).fut @@ -0,0 +1,82 @@ +-- == +-- property: prop_record_sums_succ + +-- == +-- property: prop_record_sums_fail + +-- Simple array shrinking demo (new protocol: (x,tactic)->(x',status:i8)) +-- +-- We test: "all elements are 1". +-- One generator always succeeds, one generator introduces a 0 so it fails. +-- +-- Shrinker order (SWAPPED): +-- 1) shrink scalars toward 1 (set one element to 1 by index = tactic) +-- 2) remove values (drop one element by index = tactic - n) +-- +-- status i8: +-- 0 = produced candidate (use it; runner restarts tactic from 0 on FAIL) +-- 1 = no-op candidate (runner should advance tactic) +-- 2 = stop (no more tactics) + +let all_equal_1 (x: i32) : bool = + x == 1i32 + +let prop_all_ones (xs: []i32) : bool = + map all_equal_1 xs |> reduce (&&) true + +-- Succeeding generator: all 1s +entry gen_record_sums (size: i64) (_: i32) : []i32 = + let n = if size < 0 then 0 else size + in replicate n 1i32 + +#[prop(gen(gen_record_sums))] +entry prop_record_sums_succ (input: []i32) : bool = + prop_all_ones input + +-- Failing generator: first element 1, rest 0 (if size>1) +entry gen_record_sums_fail (size: i64) (_: i32) : []i32 = + let n = if size < 0 then 0 else size + let idx : []i64 = iota n + in map (\i -> if i == 0i64 then 1i32 else 0i32) idx + +-- New-protocol shrinker for []i32 (SWAPPED order) +entry shrink_arr (xs: []i32) (random: i32) : []i32 = + let tactic = random % 4 + + let n64 : i64 = length xs + let n : i32 = i32.i64 n64 + let t : i32 = if tactic < 0i32 then 0i32 else tactic + + -- ----- Phase 1: remove one element (t in [0..n-1]) ----- + in if t < n then + if n64 <= 0 then + xs + else if n64 == 1 then + -- removing would make it empty; allow it (often helps) + [] + else + let i : i64 = i64.i32 t + let pre = take i xs + let post = drop (i+1) xs + in pre ++ post + + -- ----- Phase 2: shrink scalars toward 1 (t in [n..2n-1]) ----- + else if t < 2i32 * n then + if n64 == 0 then + xs + else + let k : i32 = t - n + let ki : i64 = i64.i32 k + -- set xs[k] to 1 if it isn't already + let old = xs[ki] + in if old == 1i32 then + xs + else + tabulate n64 (\i -> if i == ki then 1i32 else xs[i]) + + else + xs + +#[prop(gen(gen_record_sums_fail), shrink(shrink_arr))] +entry prop_record_sums_fail (input: []i32) : bool = + prop_all_ones input \ No newline at end of file diff --git a/tests_property/ArrayTests/Arrayi32(2).out b/tests_property/ArrayTests/Arrayi32(2).out new file mode 100644 index 0000000000..13f156ea12 --- /dev/null +++ b/tests_property/ArrayTests/Arrayi32(2).out @@ -0,0 +1,2 @@ +PBT FAIL: prop_record_sums_fail size=50 seed=REDACTED after N tests +Minimal counterexample: [0i32] diff --git a/tests_property/ArrayTests/Arrayi32.fut b/tests_property/ArrayTests/Arrayi32.fut new file mode 100644 index 0000000000..7f077ac3a9 --- /dev/null +++ b/tests_property/ArrayTests/Arrayi32.fut @@ -0,0 +1,84 @@ +-- == +-- property: prop_record_sums_succ + +-- == +-- property: prop_record_sums_fail + +-- Simple array shrinking demo (new protocol: (x,tactic)->(x',status:i8)) +-- +-- We test: "all elements are 1". +-- One generator always succeeds, one generator introduces a 0 so it fails. +-- +-- Shrinker order: +-- 1) remove values (drop one element by index = tactic) +-- 2) shrink scalars toward 1 (set one element to 1 by index = tactic - n) +-- +-- status i8: +-- 0 = produced candidate (use it; runner restarts tactic from 0 on FAIL) +-- 1 = no-op candidate (runner should advance tactic) +-- 2 = stop (no more tactics) + +type~ arr = []i32 + +let all_equal_1 (x: i32) : bool = + x == 1i32 + +let prop_all_ones (xs: arr) : bool = + map all_equal_1 xs |> reduce (&&) true + +-- Succeeding generator: all 1s +entry gen_record_sums (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + in replicate n 1i32 + +#[prop(gen(gen_record_sums))] +entry prop_record_sums_succ (input: arr) : bool = + prop_all_ones input + +-- Failing generator: first element 1, rest 0 (if size>1) +entry gen_record_sums_fail (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + let idx = iota n |> map (\i -> i32.i64 i) + in map (\i -> if i == 0i32 then 1i32 else 0i32) idx + +-- New-protocol shrinker for []i32 +entry shrink_arr (xs: arr) (random: i32) : arr = + let tactic = random % 4 + + let n64 : i64 = length xs + let n : i32 = i32.i64 n64 + let t : i32 = if tactic < 0i32 then 0i32 else tactic + + -- ----- Phase 1: remove one element (t in [0..n-1]) ----- + in if t < n then + if n64 <= 0 then + xs + else if n64 == 1 then + -- removing would make it empty; allow it (often helps) + [] + else + let i : i64 = i64.i32 t + let pre = take i xs + let post = drop (i+1) xs + in pre ++ post + + -- ----- Phase 2: shrink scalars toward 1 (t in [n..2n-1]) ----- + else if t < 2i32 * n then + if n64 == 0 then + xs + else + let k : i32 = t - n + let ki : i64 = i64.i32 k + -- set xs[k] to 1 if it isn't already + let old = xs[ki] + in if old == 1i32 then + xs + else + tabulate n64 (\i -> if i == ki then 1i32 else xs[i]) + + else + xs + +#[prop(gen(gen_record_sums_fail), shrink(shrink_arr))] +entry prop_record_sums_fail (input: arr) : bool = + prop_all_ones input diff --git a/tests_property/ArrayTests/Arrayi32.out b/tests_property/ArrayTests/Arrayi32.out new file mode 100644 index 0000000000..13f156ea12 --- /dev/null +++ b/tests_property/ArrayTests/Arrayi32.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_record_sums_fail size=50 seed=REDACTED after N tests +Minimal counterexample: [0i32] diff --git a/tests_property/ArrayTests/Arrayi32AutoShrink.fut b/tests_property/ArrayTests/Arrayi32AutoShrink.fut new file mode 100644 index 0000000000..e7357e17dc --- /dev/null +++ b/tests_property/ArrayTests/Arrayi32AutoShrink.fut @@ -0,0 +1,46 @@ +-- == +-- property: prop_record_sums_succ + +-- == +-- property: prop_record_sums_fail + +-- Simple array shrinking demo (new protocol: (x,tactic)->(x',status:i8)) +-- +-- We test: "all elements are 1". +-- One generator always succeeds, one generator introduces a 0 so it fails. +-- +-- Shrinker order: +-- 1) remove values (drop one element by index = tactic) +-- 2) shrink scalars toward 1 (set one element to 1 by index = tactic - n) +-- +-- status i8: +-- 0 = produced candidate (use it; runner restarts tactic from 0 on FAIL) +-- 1 = no-op candidate (runner should advance tactic) +-- 2 = stop (no more tactics) + +type~ arr = []i32 + +let all_equal_1 (x: i32) : bool = + x == 1i32 + +let prop_all_ones (xs: arr) : bool = + map all_equal_1 xs |> reduce (&&) true + +-- Succeeding generator: all 1s +entry gen_record_sums (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + in replicate n 1i32 + +#[prop(gen(gen_record_sums))] +entry prop_record_sums_succ (input: arr) : bool = + prop_all_ones input + +-- Failing generator: first element 1, rest 0 (if size>1) +entry gen_record_sums_fail (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + let idx = iota n |> map (\i -> i32.i64 i) + in map (\i -> if i == 0i32 then 1i32 else 0i32) idx + +#[prop(gen(gen_record_sums_fail), shrink(auto))] +entry prop_record_sums_fail (input: arr) : bool = + prop_all_ones input diff --git a/tests_property/ArrayTests/Arrayi32AutoShrink.out b/tests_property/ArrayTests/Arrayi32AutoShrink.out new file mode 100644 index 0000000000..0bcc8882e6 --- /dev/null +++ b/tests_property/ArrayTests/Arrayi32AutoShrink.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_record_sums_fail size=50 seed=REDACTED after N tests +Minimal counterexample: [1i32, 0i32] diff --git a/tests_property/ArrayTests/Arrayi32rev.fut b/tests_property/ArrayTests/Arrayi32rev.fut new file mode 100644 index 0000000000..b762270c05 --- /dev/null +++ b/tests_property/ArrayTests/Arrayi32rev.fut @@ -0,0 +1,79 @@ +-- == +-- property: prop_record_sums_succ + +-- == +-- property: prop_record_sums_fail + +-- Simple array shrinking demo (new protocol: (x,tactic)->(x',status:i8)) +-- +-- We test: "all elements are 1". +-- One generator always succeeds, one generator introduces a 0 so it fails. +-- +-- Shrinker order (SWAPPED): +-- 1) shrink scalars toward 1 (set one element to 1 by index = tactic) +-- 2) remove values (drop one element by index = tactic - n) +-- +-- status i8: +-- 0 = produced candidate (use it; runner restarts tactic from 0 on FAIL) +-- 1 = no-op candidate (runner should advance tactic) +-- 2 = stop (no more tactics) + +type~ arr = []i32 + +let all_equal_1 (x: i32) : bool = + x == 1i32 + +let prop_all_ones (xs: arr) : bool = + map all_equal_1 xs |> reduce (&&) true + +-- Succeeding generator: all 1s +entry gen_record_sums (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + in replicate n 1i32 + +#[prop(gen(gen_record_sums))] +entry prop_record_sums_succ (input: arr) : bool = + prop_all_ones input + +-- Failing generator: first element 1, rest 0 (if size>1) +entry gen_record_sums_fail (size: i64) (_: i32) : arr = + let n = if size < 0 then 0 else size + let idx = iota n |> map (\i -> i32.i64 i) + in map (\i -> if i == 0i32 then 1i32 else 0i32) idx + +-- New-protocol shrinker for []i32 (SWAPPED order) +entry shrink_arr (xs: arr) (random: i32) : arr = + let tactic = random % 4 + let n64 : i64 = length xs + let n : i32 = i32.i64 n64 + let t : i32 = if tactic < 0i32 then 0i32 else tactic + + -- ----- Phase 1: shrink scalars toward 1 (t in [0..n-1]) ----- + in if t < n then + if n64 == 0 then + xs + else + let ki : i64 = i64.i32 t + let old = xs[ki] + in if old == 1i32 then + xs -- no-op; advance tactic + else + tabulate n64 (\i -> if i == ki then 1i32 else xs[i]) + + -- ----- Phase 2: remove one element (t in [n..2n-1]) ----- + else + if n64 <= 0 then + xs + else + let k : i32 = t - n + let i : i64 = i64.i32 k in + if n64 == 1 then + [] + else + let pre = take i xs + let post = drop (i+1) xs + in pre ++ post + +#[prop(gen(gen_record_sums_fail), shrink(shrink_arr))] +entry prop_record_sums_fail (input: arr) : bool = + prop_all_ones input \ No newline at end of file diff --git a/tests_property/ArrayTests/Deduplicate.fut b/tests_property/ArrayTests/Deduplicate.fut new file mode 100644 index 0000000000..c315e6d05f --- /dev/null +++ b/tests_property/ArrayTests/Deduplicate.fut @@ -0,0 +1,119 @@ +-- == +-- property: prop_deduplicate_succ + +-- == +-- property: prop_deduplicate_fail + +-- Deduplicate demo with NEW shrink protocol: (x,tactic)->(x',status:i8) +-- +-- Property we test: +-- after "deduplicate_*", there are no adjacent equal elements. +-- +-- Buggy version: +-- deduplicate_fail does adjacent-dedup, then decrements the last element. +-- Minimal counterexample is [0,1] because dedup=[0,1] then last-- => [0,0]. + +-- ---------- helpers ---------- + +let no_adjacent_equal (xs: []i32) : bool = + let n = length xs + in if n < 2 then true + else + map2 (!=) (take (n-1) xs :> [n-1]i32) (drop 1 xs :> [n-1]i32) + |> reduce (&&) true + +let deduplicate_succ (xs: []i32) : []i32 = + let n = length xs + in if n < 2 then xs + else + let (_, result) = + loop (i, acc) = (1i32, [xs[0]]) while (i < i32.i64 n) do + let curr = xs[i] + let last = acc[length acc - 1] + in if curr == last then + (i+1i32, acc) + else + (i+1i32, acc ++ [curr]) + in result + +let deduplicate_fail (xs: []i32) : []i32 = + let result = deduplicate_succ xs + let n = length result + in if n < 2 then result + else + -- break it: decrement the last element + tabulate n (\i -> + let x = result[i] + in if i == n-1 then x - 1i32 else x) + +-- ---------- generators ---------- + +-- Passing generator: already “safe” for the postcondition after succ dedup. +-- (Doesn't matter much; just keeps the demo complete.) +entry gen_deduplicate_ok (size: i64) (_seed: i32) : []i32 = + let n = if size < 0 then 0 else size + in tabulate n (\i -> i32.i64 i) -- strictly increasing + +#[prop(gen(gen_deduplicate_ok))] +entry prop_deduplicate_succ (input: []i32) : bool = + no_adjacent_equal (deduplicate_succ input) + +-- Failing generator: ALWAYS returns [0,1] when size>=2, else [0]. +-- So prop_deduplicate_fail will always fail when size>=2. +entry gen_deduplicate_bad (size: i64) (_seed: i32) : []i32 = + let n = if size < 0 then 0 else size + in if n < 2 then [0i32] + else [0i32, 1i32] + +-- ---------- shrinker (NEW protocol) ---------- +-- status i8: +-- 0 = changed candidate (use it; runner restarts tactic=0 on FAIL) +-- 1 = no-op for this tactic (runner should advance tactic) +-- 2 = stop (no more tactics) +-- +-- Tactic schedule (for current xs of length n): +-- Phase A (0 .. n-1): set xs[t] to a small canonical value: +-- target(0)=0, target(i>0)=1 +-- Phase B (n .. 2n-1): remove element (t-n) +-- +-- This tends to shrink toward the minimal witness [0,1]. + +entry shrink_deduplicate (xs: []i32) (random: i32) : []i32 = + let n64 : i64 = length xs + let n : i32 = i32.i64 n64 + let tactic : i32 = random % n + let t : i32 = if tactic < 0i32 then 0i32 else tactic + + -- ---- Phase A: shrink scalars toward targets ---- + in if t < n then + if n64 == 0 then + xs + else + let i : i64 = i64.i32 t + let old = xs[i] + let target = if t == 0i32 then 0i32 else 1i32 + in if old == target then + xs + else + tabulate n64 (\j -> if j == i then target else xs[j]) + + -- ---- Phase B: remove one element ---- + else if t < 2i32 * n then + if n64 == 0 then + xs + else + let k : i32 = t - n + let i : i64 = i64.i32 k + in if n64 == 1 then + [] + else + take i xs ++ drop (i+1) xs + + else + xs + +-- ---------- failing property using shrinker ---------- + +#[prop(gen(gen_deduplicate_bad), shrink(shrink_deduplicate))] +entry prop_deduplicate_fail (input: []i32) : bool = + no_adjacent_equal (deduplicate_fail input) \ No newline at end of file diff --git a/tests_property/ArrayTests/Sort.fut b/tests_property/ArrayTests/Sort.fut new file mode 100644 index 0000000000..1262eb975d --- /dev/null +++ b/tests_property/ArrayTests/Sort.fut @@ -0,0 +1,99 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/sorts/radix_sort" + +let real_sort (xs: []i32) : []i32 = + radix_sort_int i32.num_bits i32.get_bit xs + +-- Bug: after sorting, swap the first two elements (breaks sortedness when they differ). +let flaky_sort (xs: []i32) : []i32 = + let ys = real_sort xs + let n = length ys + in if n < 2 then ys + else [ys[1]] ++ [ys[0]] ++ drop 2 ys + +entry gen_simple_param (m: i64) (with_negatives: bool) (kind: i32) : []i32 = + let n = i32.i64 m + let base = iota m |> map (\i -> i32.i64 i) + let index = iota m |> map (\i -> i32.i64 i) + + let xs = + if kind == 0 then + base + else if kind == 1 then + map (\i -> (n-1) - i) base + else if kind == 2 then + replicate m 1i32 + |> map2 (\i x -> if i == n-1 then x+1 else x) index + else + base + + in if with_negatives && n > 0 + then map2 (\i x -> if i == n-1 then -x else x) index xs + else xs + +entry gen_simple (size: i64) (seed: i32) : []i32 = + let n = if size < 0 then 0 else size + let with_negatives = (seed % 2) == 0 + let kind = (i32.abs seed) % 3 + in gen_simple_param n with_negatives kind + +let nondecreasing (xs: []i32) : bool = + let n = length xs + in if n < 2 then true + else + map2 (<=) (take (n-1) xs :> [n-1]i32) (drop 1 xs :> [n-1]i32) + |> reduce (&&) true + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (input: []i32) : bool = + nondecreasing (flaky_sort input) + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (input: []i32) : bool = + nondecreasing (real_sort input) + +let shrink_i32_to_witness (v: i32) : i32 = + if v == 0i32 then 0i32 + else if v > 0i32 then 1i32 + else -1i32 + +-- status: 0=changed, 1=no-op, 2=stop +entry shrink_simple (xs: []i32) (random: i32) : []i32 = + + let n64 : i64 = length xs + let n : i32 = i32.i64 n64 + let tactic : i32 = random % n + let t : i32 = if tactic < 0i32 then 0i32 else tactic + + -- Phase 1: shrink one element into {-1,0,1} + in if t < n then + if n64 == 0 then + xs + else + let i : i64 = i64.i32 t + let old = xs[i] + let new = shrink_i32_to_witness old + in if new == old then + xs + else + tabulate n64 (\j -> if j == i then new else xs[j]) + + -- Phase 2: drop one element + else if t < 2i32 * n then + if n64 == 0 then + xs + else + let k : i32 = t - n + let i : i64 = i64.i32 k + in if n64 == 1 then + [] + else + take i xs ++ drop (i+1) xs + + else + xs \ No newline at end of file diff --git a/tests_property/ArrayTests/reverse.fut b/tests_property/ArrayTests/reverse.fut new file mode 100644 index 0000000000..ce4b2b403d --- /dev/null +++ b/tests_property/ArrayTests/reverse.fut @@ -0,0 +1,52 @@ +import "../libraries/shrinkers/integerShrinker" +import "../lib/github.com/diku-dk/cpprandom/random" + +module rnge = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rnge +module shrink_i32 = integerlShrinkers i32 + +entry gen_i32_array (size: i64) (seed: i32) : []i32 = + tabulate size (\i -> + let state = seed + (i32.i64 i) + let rng0 = rnge.rng_from_seed [state] + let (_, x) = rand_i32.rand (-i32.i64 size, i32.i64 size) rng0 in x) + + +let reverse_bad (xs: []i32) : []i32 = xs +-- == +-- property: prop_reverse_involution + +-- == +-- property: prop_reverse_involution_bad + +-- == +-- property: prop_reverse_involution_bad2 +#[prop(gen(gen_i32_array))] +entry prop_reverse_involution (xs: []i32) : bool = + and (map2 (==) (reverse (reverse xs)) xs) + +#[prop(gen(gen_i32_array), shrink(shrinker))] +entry prop_reverse_involution_bad (xs: []i32) : bool = + and (map2 (==) (reverse_bad (reverse xs)) xs) + +#[prop(gen(gen_i32_array), shrink(auto))] +entry prop_reverse_involution_bad2 (xs: []i32) : bool = + and (map2 (==) (reverse_bad (reverse xs)) xs) + +entry shrinker (xs: []i32) (random: i32) : []i32 = + let n = length xs + in if n == 0 then xs else + + let tactic = random % 2 + let i = (i32.abs random) % i32.i64 n + + in if tactic == 0 then + -- Tactic 0: Shrink a single element at index i + let newVal = shrink_i32.shrinker xs[i] random + in copy xs with [i] = newVal + + else + -- Tactic 1: Remove the element at index i (shrink length) + let front = take (i64.i32 i) xs + let back = drop (i64.i32 i + 1) xs + in concat front back \ No newline at end of file diff --git a/tests_property/ArrayTests/reverse.out b/tests_property/ArrayTests/reverse.out new file mode 100644 index 0000000000..9dad94778c --- /dev/null +++ b/tests_property/ArrayTests/reverse.out @@ -0,0 +1,4 @@ +PBT FAIL: prop_reverse_involution_bad size=50 seed=REDACTED after N tests +Minimal counterexample: [0i32, -1i32] +PBT FAIL: prop_reverse_involution_bad2 size=50 seed=REDACTED after N tests +Minimal counterexample: [-1i32, 1i32] diff --git a/tests_property/CompositeTests/Record.fut b/tests_property/CompositeTests/Record.fut new file mode 100644 index 0000000000..00a0466fc9 --- /dev/null +++ b/tests_property/CompositeTests/Record.fut @@ -0,0 +1,43 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +-- More complex test for a record with an int inside +import "../lib/github.com/diku-dk/cpprandom/random" +type record = {x: i32, y: i32} +--------------------- record tests ------------------ +-- Uniform i32 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_i32.rand (-100i32, 100i32) rng0 + in {x = x, y = x-1} + +let simple (r: record) : (i32, i32) = + (i32.abs r.x, i32.abs r.y) + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: record) : bool = + simple r == (i32.abs r.x, i32.abs r.y) + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (r: record) : bool = + simple r == (r.x, r.y) + +let step (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: record) (random: i32) : record = + let tactic = random % 2 in + if tactic == 0 then + {x = step r.x, y = r.y} + else + {x = r.x, y = step r.y} diff --git a/tests_property/CompositeTests/Record.out b/tests_property/CompositeTests/Record.out new file mode 100644 index 0000000000..6bfa68d966 --- /dev/null +++ b/tests_property/CompositeTests/Record.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {x = -1i32, y = 0i32} diff --git a/tests_property/CompositeTests/Record2.fut b/tests_property/CompositeTests/Record2.fut new file mode 100644 index 0000000000..8ef8ab8c41 --- /dev/null +++ b/tests_property/CompositeTests/Record2.fut @@ -0,0 +1,44 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +-- More complex test for a {x: i32, y: i32} with an int inside +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- {x: i32, y: i32} tests ------------------ +-- Uniform i32 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : {x: i32, y: i32} = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_i32.rand (-100i32, 100i32) rng0 + in {x = x, y = x-1} + +let simple (r: {x: i32, y: i32}) : (i32, i32) = + (i32.abs r.x, i32.abs r.y) + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: {x: i32, y: i32}) : bool = + simple r == (i32.abs r.x, i32.abs r.y) + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (r: {x: i32, y: i32}) : bool = + simple r == (r.x, r.y) + +let step (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: {x: i32, y: i32}) (random: i32) : {x: i32, y: i32} = + let tactic = random % 2 in + if tactic == 0 then + let x' = step r.x + in {x = step r.x, y = r.y} + else + let y' = step r.y + in {x = r.x, y = step r.y} diff --git a/tests_property/CompositeTests/Record2.out b/tests_property/CompositeTests/Record2.out new file mode 100644 index 0000000000..6bfa68d966 --- /dev/null +++ b/tests_property/CompositeTests/Record2.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {x = -1i32, y = 0i32} diff --git a/tests_property/CompositeTests/RecordArray.fut b/tests_property/CompositeTests/RecordArray.fut new file mode 100644 index 0000000000..68356a2a5f --- /dev/null +++ b/tests_property/CompositeTests/RecordArray.fut @@ -0,0 +1,34 @@ +-- == +-- property: prop_record_sums_succ + +-- == +-- property: prop_record_sums_fail + +type~ record = { s: []i32, a: []i32 } + +let all_equal (xs: []i32) : bool = + let n = length xs + in if n == 0 then true + else + let first = xs[0] + in map (\x -> x == first) xs + |> reduce (&&) true + +entry gen_record_sums (size: i64) (_seed: i32) : record = + let s = replicate size (i32.i64 size) + let a = replicate size (i32.i64 size * -10) + in { s, a } + +#[prop(gen(gen_record_sums))] +entry prop_record_sums_succ (input: record) : bool = + all_equal input.s && all_equal input.a + + +entry gen_record_sums_fail (size: i64) (_seed: i32) : record = + let s = map2 (\v i -> if i == 0 then 0 else v) (replicate size (i32.i64 size)) (iota size) + let a = replicate size (i32.i64 size * -10) + in { s, a } + +#[prop(gen(gen_record_sums_fail))] +entry prop_record_sums_fail (input: record) : bool = + all_equal input.s && all_equal input.a diff --git a/tests_property/CompositeTests/RecordArray.out b/tests_property/CompositeTests/RecordArray.out new file mode 100644 index 0000000000..e64375fc56 --- /dev/null +++ b/tests_property/CompositeTests/RecordArray.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_record_sums_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {a = [-500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32, -500i32], s = [0i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32, 50i32]} diff --git a/tests_property/CompositeTests/RecordIntArray.fut b/tests_property/CompositeTests/RecordIntArray.fut new file mode 100644 index 0000000000..b59be4af63 --- /dev/null +++ b/tests_property/CompositeTests/RecordIntArray.fut @@ -0,0 +1,47 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +type record = {x: i32, xs: [3]i32} + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_i32.rand (-100i32, 100i32) rng0 + in {x = x, xs = [x, x+1, x+2]} + +let add_to_all (x: i32) (xs: [3]i32) : [3]i32 = + map (\v -> v + x) xs + +let array_eq (a: [3]i32) (b: [3]i32) : bool = + reduce (&&) true (map2 (\x y -> x == y) a b) + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: record) : bool = + length (add_to_all r.x r.xs) == length r.xs + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (r: record) : bool = + let ys = add_to_all r.x r.xs + in array_eq ys r.xs + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: record) (random: i32) : record = + let tactic = random % 2 in + if tactic == 0 then + let x' = step0 r.x + in {x = x', xs = r.xs} + + else + let xs' = map step0 r.xs + in {x = r.x, xs = xs'} diff --git a/tests_property/CompositeTests/RecordIntArray.out b/tests_property/CompositeTests/RecordIntArray.out new file mode 100644 index 0000000000..e02068f032 --- /dev/null +++ b/tests_property/CompositeTests/RecordIntArray.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {x = -1i32, xs = [0i32, 0i32, 0i32]} diff --git a/tests_property/CompositeTests/RecordRecord.fut b/tests_property/CompositeTests/RecordRecord.fut new file mode 100644 index 0000000000..8513271498 --- /dev/null +++ b/tests_property/CompositeTests/RecordRecord.fut @@ -0,0 +1,78 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +type innerRecord1 = {z: i32, b: i32} +type innerRecord2 = {o: i32, p: i32} +type record = {x: innerRecord1, y: innerRecord2} + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: innerRecord1) (r2: innerRecord2) : bool = + r1.z == r2.o && r1.b == r2.p + +entry gen_simple (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = {z = v, b = v+1}, + y = {o = v, p = v+1} } + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: record) : bool = + inner_eq r.x r.y + +entry gen_simple_fail (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = {z = v, b = v+1}, + y = {o = v+1, p = v+1} } + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: record) : bool = + inner_eq r.x r.y + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: record) (random: i32) : record = + let tactic = random % 6 in + if tactic == 0 then + let z' = step0 r.x.z + let o' = step0 r.y.o + let r' = {x = {z = z', b = r.x.b}, + y = {o = o', p = r.y.p}} + in r' + + else if tactic == 1 then + let b' = step0 r.x.b + let p' = step0 r.y.p + let r' = {x = {z = r.x.z, b = b'}, + y = {o = r.y.o, p = p'}} + in r' + + else if tactic == 2 then + let z' = step0 r.x.z + let r' = {x = {z = z', b = r.x.b}, y = r.y} + in r' + + else if tactic == 3 then + let b' = step0 r.x.b + let r' = {x = {z = r.x.z, b = b'}, y = r.y} + in r' + + else if tactic == 4 then + let o' = step0 r.y.o + let r' = {x = r.x, y = {o = o', p = r.y.p}} + in r' + + else + let p' = step0 r.y.p + let r' = {x = r.x, y = {o = r.y.o, p = p'}} + in r' diff --git a/tests_property/CompositeTests/RecordRecord.out b/tests_property/CompositeTests/RecordRecord.out new file mode 100644 index 0000000000..d7faf730d5 --- /dev/null +++ b/tests_property/CompositeTests/RecordRecord.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {x = {b = 0i32, z = 0i32}, y = {o = -1i32, p = 0i32}} diff --git a/tests_property/CompositeTests/RecordRecord2.fut b/tests_property/CompositeTests/RecordRecord2.fut new file mode 100644 index 0000000000..c8c41243f0 --- /dev/null +++ b/tests_property/CompositeTests/RecordRecord2.fut @@ -0,0 +1,75 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" +type record = {x: {z: i32, b: i32}, y: {o: i32, p: i32}} + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: {z: i32, b: i32}) (r2: {o: i32, p: i32}) : bool = + r1.z == r2.o && r1.b == r2.p + +entry gen_simple (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = {z = v, b = v+1}, + y = {o = v, p = v+1} } + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: record) : bool = + inner_eq r.x r.y + +entry gen_simple_fail (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = {z = v, b = v+1}, + y = {o = v+1, p = v+1} } + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: record) : bool = + inner_eq r.x r.y + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: record) (random: i32) : record = + let tactic = random % 6 in + if tactic == 0 then + let z' = step0 r.x.z + let o' = step0 r.y.o + let r' = {x = {z = z', b = r.x.b}, + y = {o = o', p = r.y.p}} + in r' + + else if tactic == 1 then + let b' = step0 r.x.b + let p' = step0 r.y.p + let r' = {x = {z = r.x.z, b = b'}, + y = {o = r.y.o, p = p'}} + in r' + + else if tactic == 2 then + let z' = step0 r.x.z + let r' = {x = {z = z', b = r.x.b}, y = r.y} + in r' + + else if tactic == 3 then + let b' = step0 r.x.b + let r' = {x = {z = r.x.z, b = b'}, y = r.y} + in r' + + else if tactic == 4 then + let o' = step0 r.y.o + let r' = {x = r.x, y = {o = o', p = r.y.p}} + in r' + + else + let p' = step0 r.y.p + let r' = {x = r.x, y = {o = r.y.o, p = p'}} + in r' \ No newline at end of file diff --git a/tests_property/CompositeTests/RecordRecord2.out b/tests_property/CompositeTests/RecordRecord2.out new file mode 100644 index 0000000000..d7faf730d5 --- /dev/null +++ b/tests_property/CompositeTests/RecordRecord2.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {x = {b = 0i32, z = 0i32}, y = {o = -1i32, p = 0i32}} diff --git a/tests_property/CompositeTests/RecordRecord3.fut b/tests_property/CompositeTests/RecordRecord3.fut new file mode 100644 index 0000000000..dc533260c9 --- /dev/null +++ b/tests_property/CompositeTests/RecordRecord3.fut @@ -0,0 +1,74 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: {z: i32, b: i32}) (r2: {o: i32, p: i32}) : bool = + r1.z == r2.o && r1.b == r2.p + +entry gen_simple (size: i64) (seed: i32) : {x: {z: i32, b: i32}, y: {o: i32, p: i32}} = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = {z = v, b = v+1}, + y = {o = v, p = v+1} } + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: {x: {z: i32, b: i32}, y: {o: i32, p: i32}}) : bool = + inner_eq r.x r.y + +entry gen_simple_fail (size: i64) (seed: i32) : {x: {z: i32, b: i32}, y: {o: i32, p: i32}} = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = {z = v, b = v+1}, + y = {o = v+1, p = v+1} } + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: {x: {z: i32, b: i32}, y: {o: i32, p: i32}}) : bool = + inner_eq r.x r.y + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: {x: {z: i32, b: i32}, y: {o: i32, p: i32}}) (random: i32) : {x: {z: i32, b: i32}, y: {o: i32, p: i32}} = + let tactic = random % 6 in + if tactic == 0 then + let z' = step0 r.x.z + let o' = step0 r.y.o + let r' = {x = {z = z', b = r.x.b}, + y = {o = o', p = r.y.p}} + in r' + + else if tactic == 1 then + let b' = step0 r.x.b + let p' = step0 r.y.p + let r' = {x = {z = r.x.z, b = b'}, + y = {o = r.y.o, p = p'}} + in r' + + else if tactic == 2 then + let z' = step0 r.x.z + let r' = {x = {z = z', b = r.x.b}, y = r.y} + in r' + + else if tactic == 3 then + let b' = step0 r.x.b + let r' = {x = {z = r.x.z, b = b'}, y = r.y} + in r' + + else if tactic == 4 then + let o' = step0 r.y.o + let r' = {x = r.x, y = {o = o', p = r.y.p}} + in r' + + else + let p' = step0 r.y.p + let r' = {x = r.x, y = {o = r.y.o, p = p'}} + in r' \ No newline at end of file diff --git a/tests_property/CompositeTests/RecordRecord3.out b/tests_property/CompositeTests/RecordRecord3.out new file mode 100644 index 0000000000..d7faf730d5 --- /dev/null +++ b/tests_property/CompositeTests/RecordRecord3.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {x = {b = 0i32, z = 0i32}, y = {o = -1i32, p = 0i32}} diff --git a/tests_property/CompositeTests/RecordTuple.fut b/tests_property/CompositeTests/RecordTuple.fut new file mode 100644 index 0000000000..cf6047b7f5 --- /dev/null +++ b/tests_property/CompositeTests/RecordTuple.fut @@ -0,0 +1,78 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +type tupleLeft = (i32, i32) +type tupleRight = (i32, i32) +type record = {x: tupleLeft, y: tupleRight} + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: tupleLeft) (r2: tupleRight) : bool = + r1.0 == r2.0 && r1.1 == r2.1 + +entry gen_simple (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = (v, v+1), + y = (v, v+1) } + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: record) : bool = + inner_eq r.x r.y + +entry gen_simple_fail (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = (v, v+1), + y = (v+1, v+1) } + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: record) : bool = + inner_eq r.x r.y + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: record) (random: i32) : record = + let tactic = random % 6 in + if tactic == 0 then + let x0' = step0 r.x.0 + let y0' = step0 r.y.0 + let r' = {x = (x0', r.x.1), + y = (y0', r.y.1)} + in r' + + else if tactic == 1 then + let x1' = step0 r.x.1 + let y1' = step0 r.y.1 + let r' = {x = (r.x.0, x1'), + y = (r.y.0, y1')} + in r' + + else if tactic == 2 then + let x0' = step0 r.x.0 + let r' = {x = (x0', r.x.1), y = r.y} + in r' + + else if tactic == 3 then + let x1' = step0 r.x.1 + let r' = {x = (r.x.0, x1'), y = r.y} + in r' + + else if tactic == 4 then + let y0' = step0 r.y.0 + let r' = {x = r.x, y = (y0', r.y.1)} + in r' + + else + let y1' = step0 r.y.1 + let r' = {x = r.x, y = (r.y.0, y1')} + in r' \ No newline at end of file diff --git a/tests_property/CompositeTests/RecordTuple.out b/tests_property/CompositeTests/RecordTuple.out new file mode 100644 index 0000000000..6b74161a17 --- /dev/null +++ b/tests_property/CompositeTests/RecordTuple.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {x = (0i32, 0i32), y = (-1i32, 0i32)} diff --git a/tests_property/CompositeTests/RecordTuple2.fut b/tests_property/CompositeTests/RecordTuple2.fut new file mode 100644 index 0000000000..b2f063474c --- /dev/null +++ b/tests_property/CompositeTests/RecordTuple2.fut @@ -0,0 +1,76 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +type record = {x: (i32, i32), y: (i32, i32)} + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: (i32, i32)) (r2: (i32, i32)) : bool = + r1.0 == r2.0 && r1.1 == r2.1 + +entry gen_simple (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = (v, v+1), + y = (v, v+1) } + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: record) : bool = + inner_eq r.x r.y + +entry gen_simple_fail (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = (v, v+1), + y = (v+1, v+1) } + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: record) : bool = + inner_eq r.x r.y + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: record) (random: i32) : record = + let tactic = random % 6 in + if tactic == 0 then + let x0' = step0 r.x.0 + let y0' = step0 r.y.0 + let r' = {x = (x0', r.x.1), + y = (y0', r.y.1)} + in r' + + else if tactic == 1 then + let x1' = step0 r.x.1 + let y1' = step0 r.y.1 + let r' = {x = (r.x.0, x1'), + y = (r.y.0, y1')} + in r' + + else if tactic == 2 then + let x0' = step0 r.x.0 + let r' = {x = (x0', r.x.1), y = r.y} + in r' + + else if tactic == 3 then + let x1' = step0 r.x.1 + let r' = {x = (r.x.0, x1'), y = r.y} + in r' + + else if tactic == 4 then + let y0' = step0 r.y.0 + let r' = {x = r.x, y = (y0', r.y.1)} + in r' + + else + let y1' = step0 r.y.1 + let r' = {x = r.x, y = (r.y.0, y1')} + in r' \ No newline at end of file diff --git a/tests_property/CompositeTests/RecordTuple2.out b/tests_property/CompositeTests/RecordTuple2.out new file mode 100644 index 0000000000..6b74161a17 --- /dev/null +++ b/tests_property/CompositeTests/RecordTuple2.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {x = (0i32, 0i32), y = (-1i32, 0i32)} diff --git a/tests_property/CompositeTests/RecordTuple3.fut b/tests_property/CompositeTests/RecordTuple3.fut new file mode 100644 index 0000000000..9b35f9093d --- /dev/null +++ b/tests_property/CompositeTests/RecordTuple3.fut @@ -0,0 +1,77 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: (i32, i32)) (r2: (i32, i32)) : bool = + r1.0 == r2.0 && r1.1 == r2.1 + +entry gen_simple (size: i64) (seed: i32) : {x: (i32, i32), y: (i32, i32)} = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = (v, v+1), + y = (v, v+1) } + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: {x: (i32, i32), y: (i32, i32)}) : bool = + inner_eq r.x r.y + +entry gen_simple_fail (size: i64) (seed: i32) : {x: (i32, i32), y: (i32, i32)} = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in { x = (v, v+1), + y = (v+1, v+1) } + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: {x: (i32, i32), y: (i32, i32)}) : bool = + inner_eq r.x r.y + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple + (r: {x: (i32, i32), y: (i32, i32)}) + (random: i32) + : {x: (i32, i32), y: (i32, i32)} = + let tactic = random % 6 in + if tactic == 0 then + let x0' = step0 r.x.0 + let y0' = step0 r.y.0 + let r' = {x = (x0', r.x.1), + y = (y0', r.y.1)} + in r' + + else if tactic == 1 then + let x1' = step0 r.x.1 + let y1' = step0 r.y.1 + let r' = {x = (r.x.0, x1'), + y = (r.y.0, y1')} + in r' + + else if tactic == 2 then + let x0' = step0 r.x.0 + let r' = {x = (x0', r.x.1), y = r.y} + in r' + + else if tactic == 3 then + let x1' = step0 r.x.1 + let r' = {x = (r.x.0, x1'), y = r.y} + in r' + + else if tactic == 4 then + let y0' = step0 r.y.0 + let r' = {x = r.x, y = (y0', r.y.1)} + in r' + + else + let y1' = step0 r.y.1 + let r' = {x = r.x, y = (r.y.0, y1')} + in r' \ No newline at end of file diff --git a/tests_property/CompositeTests/RecordTuple3.out b/tests_property/CompositeTests/RecordTuple3.out new file mode 100644 index 0000000000..6b74161a17 --- /dev/null +++ b/tests_property/CompositeTests/RecordTuple3.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {x = (0i32, 0i32), y = (-1i32, 0i32)} diff --git a/tests_property/CompositeTests/RecordTupleArray.fut b/tests_property/CompositeTests/RecordTupleArray.fut new file mode 100644 index 0000000000..eb4910d0cb --- /dev/null +++ b/tests_property/CompositeTests/RecordTupleArray.fut @@ -0,0 +1,129 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +type inner = { xs: [4]i32, t: (i32, i32) } +type rec = { a: inner + , b: (inner, [4]i32) + , c: [4]inner + } + +let step0 (v: i32) : i32 = + if v > 0 then v-1 else if v < 0 then v+1 else v + +let mk (ok: bool) (v: rec) : []rec = + map (\t -> t.1) (filter (\t -> t.0) [(ok, v)]) + +entry gen_simple (size: i64) (seed: i32) : rec = + let rng0 = rng_engine.rng_from_seed [seed] + let (rng1, a0) = rand_i32.rand (-100i32, 100i32) rng0 + let (rng2, a1) = rand_i32.rand (-100i32, 100i32) rng1 + let (rng3, a2) = rand_i32.rand (-100i32, 100i32) rng2 + let (rng4, a3) = rand_i32.rand (-100i32, 100i32) rng3 + let (rng5, b0) = rand_i32.rand (-100i32, 100i32) rng4 + let (rng6, b1) = rand_i32.rand (-100i32, 100i32) rng5 + let (rng7, b2) = rand_i32.rand (-100i32, 100i32) rng6 + let (_, b3) = rand_i32.rand (-100i32, 100i32) rng7 + + let a_xs : [4]i32 = [a0, a1, a2, a3] + let b_xs : [4]i32 = [b0, b1, b2, b3] + + let a_inner : inner = { xs = a_xs, t = (a0, a1) } + let b_inner : inner = { xs = b_xs, t = (b0, b1) } + + let c_arr : [4]inner = + [ {xs = [a0, a1, a2, a3], t = (a2, a3)} + , {xs = [a1, a2, a3, a0], t = (a1, a2)} + , {xs = [b0, b1, b2, b3], t = (b2, b3)} + , {xs = [b1, b2, b3, b0], t = (b1, b2)} + ] + + in { a = a_inner + , b = (b_inner, [a3, a2, a1, a0]) + , c = c_arr + } + +let simple_succ (r: rec) : i32 = + i32.abs r.a.xs[0] + i32.abs r.b.0.t.0 + i32.abs r.c[0].xs[0] + +#[noprop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: rec) : bool = + simple_succ r == + (i32.abs r.a.xs[0] + i32.abs r.b.0.t.0 + i32.abs r.c[0].xs[0]) + +entry shrink_rec (r: rec) : []rec = + let a0 = r.a.xs[0] + let a1 = r.a.xs[1] + let a2 = r.a.xs[2] + let a3 = r.a.xs[3] + + let b0 = r.b.0.xs[0] + let b1 = r.b.0.xs[1] + let b2 = r.b.0.xs[2] + let b3 = r.b.0.xs[3] + + let c00 = r.c[0].xs[0] + let c10 = r.c[1].xs[0] + + let a0' = step0 a0 + let b0' = step0 b0 + let c00' = step0 c00 + let c10' = step0 c10 + + let r1 : rec = + { a = { xs = [a0', a1, a2, a3], t = r.a.t } + , b = r.b + , c = r.c + } + + let r2 : rec = + { a = r.a + , b = ({ xs = [b0', b1, b2, b3], t = r.b.0.t }, r.b.1) + , c = r.c + } + + let r3 : rec = + { a = r.a + , b = r.b + , c = [ { xs = [c00', r.c[0].xs[1], r.c[0].xs[2], r.c[0].xs[3]], t = r.c[0].t } + , r.c[1] + , r.c[2] + , r.c[3] + ] + } + + let r4 : rec = + { a = r.a + , b = r.b + , c = [ r.c[0] + , { xs = [c10', r.c[1].xs[1], r.c[1].xs[2], r.c[1].xs[3]], t = r.c[1].t } + , r.c[2] + , r.c[3] + ] + } + + in mk (a0' != a0) r1 + ++ mk (b0' != b0) r2 + ++ mk (c00' != c00) r3 + ++ mk (c10' != c10) r4 + +entry gen_simple_fail (size: i64) (seed: i32) : rec = + gen_simple size seed + +let simple_fail (r: rec) : i32 = + i32.abs r.a.xs[0] + i32.abs r.b.0.t.0 + i32.abs r.c[0].xs[0] + 1 + +#[noprop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: rec) : bool = + simple_fail r == + (i32.abs r.a.xs[0] + i32.abs r.b.0.t.0 + i32.abs r.c[0].xs[0]) + +entry shrink_simple (r: rec) : []rec = + shrink_rec r diff --git a/tests_property/CompositeTests/SimpleRecord.fut b/tests_property/CompositeTests/SimpleRecord.fut new file mode 100644 index 0000000000..36dd279f90 --- /dev/null +++ b/tests_property/CompositeTests/SimpleRecord.fut @@ -0,0 +1,41 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +-- Simple tests for a record with an int inside +import "../lib/github.com/diku-dk/cpprandom/random" +type record = {x: i32} +--------------------- record tests ------------------ +-- Uniform i32 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : record = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_i32.rand (-100i32, 100i32) rng0 + in {x = x} + +let simple_succ (r: record) : i32 = + i32.abs r.x + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: record) : bool = + simple_succ r == i32.abs r.x + +let simple_fail (r: record) : i32 = + i32.abs r.x +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (r: record) : bool = + simple_fail r == r.x + +let step (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: record) (_random: i32) : record = + let x' = step r.x + in {x = x'} \ No newline at end of file diff --git a/tests_property/CompositeTests/SimpleRecord.out b/tests_property/CompositeTests/SimpleRecord.out new file mode 100644 index 0000000000..89dcaae433 --- /dev/null +++ b/tests_property/CompositeTests/SimpleRecord.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: {x = -1i32} diff --git a/tests_property/CompositeTests/Tuple.fut b/tests_property/CompositeTests/Tuple.fut new file mode 100644 index 0000000000..63abf7a712 --- /dev/null +++ b/tests_property/CompositeTests/Tuple.fut @@ -0,0 +1,43 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +-- More complex test for a tuple with an int inside +import "../lib/github.com/diku-dk/cpprandom/random" +type tuple = (i32, i32) +--------------------- tuple tests ------------------ +-- Uniform i32 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : tuple = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_i32.rand (-100i32, 100i32) rng0 + in (x, x-1) + +let simple (r: tuple) : (i32, i32) = + (i32.abs r.0, i32.abs r.1) + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: tuple) : bool = + simple r == (i32.abs r.0, i32.abs r.1) + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (r: tuple) : bool = + simple r == (r.0, r.1) + +let step (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: tuple) (random: i32) : tuple = + let tactic = random % 2 in + if tactic == 0 then + {0 = step r.0, 1 = r.1} + else + {0 = r.0, 1 = step r.1} \ No newline at end of file diff --git a/tests_property/CompositeTests/Tuple.out b/tests_property/CompositeTests/Tuple.out new file mode 100644 index 0000000000..50a128f5fa --- /dev/null +++ b/tests_property/CompositeTests/Tuple.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: (-1i32, 0i32) diff --git a/tests_property/CompositeTests/Tuple2.fut b/tests_property/CompositeTests/Tuple2.fut new file mode 100644 index 0000000000..8ed1db29f1 --- /dev/null +++ b/tests_property/CompositeTests/Tuple2.fut @@ -0,0 +1,43 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +-- More complex test for a (i32, i32) +import "../lib/github.com/diku-dk/cpprandom/random" + +--------------------- (i32, i32) tests ------------------ +-- Uniform i32 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : (i32, i32) = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_i32.rand (-100i32, 100i32) rng0 + in (x, x-1) + +let simple (r: (i32, i32)) : (i32, i32) = + (i32.abs r.0, i32.abs r.1) + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: (i32, i32)) : bool = + simple r == (i32.abs r.0, i32.abs r.1) + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (r: (i32, i32)) : bool = + simple r == (r.0, r.1) + +let step (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: (i32, i32)) (random: i32) : (i32, i32) = + let tactic = random % 2 in + if tactic == 0 then + {0 = step r.0, 1 = r.1} + else + {0 = r.0, 1 = step r.1} \ No newline at end of file diff --git a/tests_property/CompositeTests/Tuple2.out b/tests_property/CompositeTests/Tuple2.out new file mode 100644 index 0000000000..50a128f5fa --- /dev/null +++ b/tests_property/CompositeTests/Tuple2.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: (-1i32, 0i32) diff --git a/tests_property/CompositeTests/Tuple3.fut b/tests_property/CompositeTests/Tuple3.fut new file mode 100644 index 0000000000..1d0c29a5ad --- /dev/null +++ b/tests_property/CompositeTests/Tuple3.fut @@ -0,0 +1,45 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +-- More complex test for a tuple +import "../lib/github.com/diku-dk/cpprandom/random" + +--------------------- tuple tests ------------------ +-- Uniform i32 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : (i32, i32) = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_i32.rand (-100i32, 100i32) rng0 + in (x, x-1) + +let simple (r: (i32, i32)) : (i32, i32) = + (i32.abs r.0, i32.abs r.1) + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: (i32, i32)) : bool = + simple r == (i32.abs r.0, i32.abs r.1) + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (r: (i32, i32)) : bool = + simple r == (r.0, r.1) + +let step (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple ((x: i32, y: i32)) (random: i32) : (i32, i32) = + let tactic = random % 2 in + if tactic == 0 then + let x' = step x + in {0 = x', 1 = y} + else + let y' = step y + in {0 = x, 1 = y'} diff --git a/tests_property/CompositeTests/Tuple3.out b/tests_property/CompositeTests/Tuple3.out new file mode 100644 index 0000000000..50a128f5fa --- /dev/null +++ b/tests_property/CompositeTests/Tuple3.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: (-1i32, 0i32) diff --git a/tests_property/CompositeTests/TupleRecord.fut b/tests_property/CompositeTests/TupleRecord.fut new file mode 100644 index 0000000000..f6207572c1 --- /dev/null +++ b/tests_property/CompositeTests/TupleRecord.fut @@ -0,0 +1,78 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +type left = {a: i32, b: i32} +type right = {o: i32, p: i32} +type pair = (left, right) + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: left) (r2: right) : bool = + r1.a == r2.o && r1.b == r2.p + +entry gen_simple (size: i64) (seed: i32) : pair = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ({a = v, b = v+1}, + {o = v, p = v+1}) + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: pair) : bool = + inner_eq r.0 r.1 + +entry gen_simple_fail (size: i64) (seed: i32) : pair = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ({a = v, b = v+1}, + {o = v+1, p = v+1}) + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: pair) : bool = + inner_eq r.0 r.1 + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: pair) (random: i32) : pair = + let tactic = random % 6 in + if tactic == 0 then + let a' = step0 r.0.a + let o' = step0 r.1.o + let r' = ({a = a', b = r.0.b}, + {o = o', p = r.1.p}) + in r' + + else if tactic == 1 then + let b' = step0 r.0.b + let p' = step0 r.1.p + let r' = ({a = r.0.a, b = b'}, + {o = r.1.o, p = p'}) + in r' + + else if tactic == 2 then + let a' = step0 r.0.a + let r' = ({a = a', b = r.0.b}, r.1) + in r' + + else if tactic == 3 then + let b' = step0 r.0.b + let r' = ({a = r.0.a, b = b'}, r.1) + in r' + + else if tactic == 4 then + let o' = step0 r.1.o + let r' = (r.0, {o = o', p = r.1.p}) + in r' + + else + let p' = step0 r.1.p + let r' = (r.0, {o = r.1.o, p = p'}) + in r' diff --git a/tests_property/CompositeTests/TupleRecord.out b/tests_property/CompositeTests/TupleRecord.out new file mode 100644 index 0000000000..641059c664 --- /dev/null +++ b/tests_property/CompositeTests/TupleRecord.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: ({a = 0i32, b = 0i32}, {o = -1i32, p = 0i32}) diff --git a/tests_property/CompositeTests/TupleRecord2.fut b/tests_property/CompositeTests/TupleRecord2.fut new file mode 100644 index 0000000000..c4ffb8c064 --- /dev/null +++ b/tests_property/CompositeTests/TupleRecord2.fut @@ -0,0 +1,75 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" +type pair = ({a: i32, b: i32}, {o: i32, p: i32} ) + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: {a: i32, b: i32}) (r2: {o: i32, p: i32}) : bool = + r1.a == r2.o && r1.b == r2.p + +entry gen_simple (size: i64) (seed: i32) : pair = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ({a = v, b = v+1}, + {o = v, p = v+1}) + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: pair) : bool = + inner_eq r.0 r.1 + +entry gen_simple_fail (size: i64) (seed: i32) : pair = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ({a = v, b = v+1}, + {o = v+1, p = v+1}) + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: pair) : bool = + inner_eq r.0 r.1 + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: pair) (random: i32) : pair = + let tactic = random % 6 in + if tactic == 0 then + let a' = step0 r.0.a + let o' = step0 r.1.o + let r' = ({a = a', b = r.0.b}, + {o = o', p = r.1.p}) + in r' + + else if tactic == 1 then + let b' = step0 r.0.b + let p' = step0 r.1.p + let r' = ({a = r.0.a, b = b'}, + {o = r.1.o, p = p'}) + in r' + + else if tactic == 2 then + let a' = step0 r.0.a + let r' = ({a = a', b = r.0.b}, r.1) + in r' + + else if tactic == 3 then + let b' = step0 r.0.b + let r' = ({a = r.0.a, b = b'}, r.1) + in r' + + else if tactic == 4 then + let o' = step0 r.1.o + let r' = (r.0, {o = o', p = r.1.p}) + in r' + + else + let p' = step0 r.1.p + let r' = (r.0, {o = r.1.o, p = p'}) + in r' diff --git a/tests_property/CompositeTests/TupleRecord2.out b/tests_property/CompositeTests/TupleRecord2.out new file mode 100644 index 0000000000..641059c664 --- /dev/null +++ b/tests_property/CompositeTests/TupleRecord2.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: ({a = 0i32, b = 0i32}, {o = -1i32, p = 0i32}) diff --git a/tests_property/CompositeTests/TupleRecord3.fut b/tests_property/CompositeTests/TupleRecord3.fut new file mode 100644 index 0000000000..438dc6e5cf --- /dev/null +++ b/tests_property/CompositeTests/TupleRecord3.fut @@ -0,0 +1,74 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: {a: i32, b: i32}) (r2: {o: i32, p: i32}) : bool = + r1.a == r2.o && r1.b == r2.p + +entry gen_simple (size: i64) (seed: i32) : ({a: i32, b: i32}, {o: i32, p: i32} ) = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ({a = v, b = v+1}, + {o = v, p = v+1}) + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: ({a: i32, b: i32}, {o: i32, p: i32} )) : bool = + inner_eq r.0 r.1 + +entry gen_simple_fail (size: i64) (seed: i32) : ({a: i32, b: i32}, {o: i32, p: i32} ) = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ({a = v, b = v+1}, + {o = v+1, p = v+1}) + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: ({a: i32, b: i32}, {o: i32, p: i32} )) : bool = + inner_eq r.0 r.1 + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: ({a: i32, b: i32}, {o: i32, p: i32} )) (random: i32) : ({a: i32, b: i32}, {o: i32, p: i32} ) = + let tactic = random % 6 in + if tactic == 0 then + let a' = step0 r.0.a + let o' = step0 r.1.o + let r' = ({a = a', b = r.0.b}, + {o = o', p = r.1.p}) + in r' + + else if tactic == 1 then + let b' = step0 r.0.b + let p' = step0 r.1.p + let r' = ({a = r.0.a, b = b'}, + {o = r.1.o, p = p'}) + in r' + + else if tactic == 2 then + let a' = step0 r.0.a + let r' = ({a = a', b = r.0.b}, r.1) + in r' + + else if tactic == 3 then + let b' = step0 r.0.b + let r' = ({a = r.0.a, b = b'}, r.1) + in r' + + else if tactic == 4 then + let o' = step0 r.1.o + let r' = (r.0, {o = o', p = r.1.p}) + in r' + + else + let p' = step0 r.1.p + let r' = (r.0, {o = r.1.o, p = p'}) + in r' diff --git a/tests_property/CompositeTests/TupleRecord3.out b/tests_property/CompositeTests/TupleRecord3.out new file mode 100644 index 0000000000..641059c664 --- /dev/null +++ b/tests_property/CompositeTests/TupleRecord3.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: ({a = 0i32, b = 0i32}, {o = -1i32, p = 0i32}) diff --git a/tests_property/CompositeTests/TupleTriple.fut b/tests_property/CompositeTests/TupleTriple.fut new file mode 100644 index 0000000000..8493fcc588 --- /dev/null +++ b/tests_property/CompositeTests/TupleTriple.fut @@ -0,0 +1,49 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let triple_eq (t: (i32, i32, i32)) : bool = + t.0 == t.1 && t.1 == t.2 + +entry gen_simple (size: i64) (seed: i32) : (i32, i32, i32) = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in (v, v, v) + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (t: (i32, i32, i32)) : bool = + triple_eq t + +entry gen_simple_fail (size: i64) (seed: i32) : (i32, i32, i32) = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in (v, v+1, v) + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (t: (i32, i32, i32)) : bool = + triple_eq t + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (t: (i32, i32, i32)) (random: i32) : (i32, i32, i32) = + let tactic = random % 3 in + let (a, b, c) = t in + if tactic == 0 then + let a' = step0 a + in (a', b, c) + else if tactic == 1 then + let b' = step0 b + in (a, b', c) + else + let c' = step0 c + in (a, b, c') \ No newline at end of file diff --git a/tests_property/CompositeTests/TupleTriple.out b/tests_property/CompositeTests/TupleTriple.out new file mode 100644 index 0000000000..f93eeb91b1 --- /dev/null +++ b/tests_property/CompositeTests/TupleTriple.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: (-1i32, 0i32, 0i32) diff --git a/tests_property/CompositeTests/TupleTuple.fut b/tests_property/CompositeTests/TupleTuple.fut new file mode 100644 index 0000000000..4c5e467814 --- /dev/null +++ b/tests_property/CompositeTests/TupleTuple.fut @@ -0,0 +1,74 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +type tupleLeft = (i32, i32) +type tupleRight = (i32, i32) +type tuple = (tupleLeft, tupleRight) + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: tupleLeft) (r2: tupleRight) : bool = + r1.0 == r2.0 && r1.1 == r2.1 + +entry gen_simple (size: i64) (seed: i32) : tuple = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ((v, v+1), (v, v+1)) + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: tuple) : bool = + inner_eq r.0 r.1 + +entry gen_simple_fail (size: i64) (seed: i32) : tuple = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ((v, v+1), (v+1, v+1)) + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: tuple) : bool = + inner_eq r.0 r.1 + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: tuple) (random: i32) : tuple = + let tactic = random % 6 in + if tactic == 0 then + let x0' = step0 r.0.0 + let y0' = step0 r.1.0 + let r' = ((x0', r.0.1), (y0', r.1.1)) + in r' + + else if tactic == 1 then + let x1' = step0 r.0.1 + let y1' = step0 r.1.1 + let r' = ((r.0.0, x1'), (r.1.0, y1')) + in r' + + else if tactic == 2 then + let x0' = step0 r.0.0 + let r' = ((x0', r.0.1), r.1) + in r' + + else if tactic == 3 then + let x1' = step0 r.0.1 + let r' = ((r.0.0, x1'), r.1) + in r' + + else if tactic == 4 then + let y0' = step0 r.1.0 + let r' = (r.0, (y0', r.1.1)) + in r' + + else + let y1' = step0 r.1.1 + let r' = (r.0, (r.1.0, y1')) + in r' diff --git a/tests_property/CompositeTests/TupleTuple.out b/tests_property/CompositeTests/TupleTuple.out new file mode 100644 index 0000000000..e54a083bfe --- /dev/null +++ b/tests_property/CompositeTests/TupleTuple.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: ((0i32, 0i32), (-1i32, 0i32)) diff --git a/tests_property/CompositeTests/TupleTuple2.fut b/tests_property/CompositeTests/TupleTuple2.fut new file mode 100644 index 0000000000..dcf4b78734 --- /dev/null +++ b/tests_property/CompositeTests/TupleTuple2.fut @@ -0,0 +1,71 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" +type tuple = (((i32, i32)), (i32,i32)) + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: (i32, i32)) (r2: (i32, i32)) : bool = + r1.0 == r2.0 && r1.1 == r2.1 + +entry gen_simple (size: i64) (seed: i32) : tuple = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ((v, v+1), (v, v+1)) + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: tuple) : bool = + inner_eq r.0 r.1 + +entry gen_simple_fail (size: i64) (seed: i32) : tuple = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ((v, v+1), (v+1, v+1)) + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: tuple) : bool = + inner_eq r.0 r.1 + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: tuple) (random: i32) : tuple = + let tactic = random % 6 in + if tactic == 0 then + let x0' = step0 r.0.0 + let y0' = step0 r.1.0 + let r' = ((x0', r.0.1), (y0', r.1.1)) + in r' + + else if tactic == 1 then + let x1' = step0 r.0.1 + let y1' = step0 r.1.1 + let r' = ((r.0.0, x1'), (r.1.0, y1')) + in r' + + else if tactic == 2 then + let x0' = step0 r.0.0 + let r' = ((x0', r.0.1), r.1) + in r' + + else if tactic == 3 then + let x1' = step0 r.0.1 + let r' = ((r.0.0, x1'), r.1) + in r' + + else if tactic == 4 then + let y0' = step0 r.1.0 + let r' = (r.0, (y0', r.1.1)) + in r' + + else + let y1' = step0 r.1.1 + let r' = (r.0, (r.1.0, y1')) + in r' diff --git a/tests_property/CompositeTests/TupleTuple2.out b/tests_property/CompositeTests/TupleTuple2.out new file mode 100644 index 0000000000..e54a083bfe --- /dev/null +++ b/tests_property/CompositeTests/TupleTuple2.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: ((0i32, 0i32), (-1i32, 0i32)) diff --git a/tests_property/CompositeTests/TupleTuple3.fut b/tests_property/CompositeTests/TupleTuple3.fut new file mode 100644 index 0000000000..84e020671f --- /dev/null +++ b/tests_property/CompositeTests/TupleTuple3.fut @@ -0,0 +1,70 @@ +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +import "../lib/github.com/diku-dk/cpprandom/random" + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +let inner_eq (r1: (i32, i32)) (r2: (i32, i32)) : bool = + r1.0 == r2.0 && r1.1 == r2.1 + +entry gen_simple (size: i64) (seed: i32) : ((i32, i32), (i32, i32)) = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ((v, v+1), (v, v+1)) + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (r: ((i32, i32), (i32, i32))) : bool = + inner_eq r.0 r.1 + +entry gen_simple_fail (size: i64) (seed: i32) : ((i32, i32), (i32, i32)) = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, v) = rand_i32.rand (-100i32, 100i32) rng0 + in ((v, v+1), (v+1, v+1)) + +#[prop(gen(gen_simple_fail), shrink(shrink_simple))] +entry prop_simple_fail (r: ((i32, i32), (i32, i32))) : bool = + inner_eq r.0 r.1 + +let step0 (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple ((a: i32, b: i32), (c: i32, d: i32)) (random: i32) : ((i32, i32), (i32, i32)) = + let tactic = random % 6 in + if tactic == 0 then + let x0' = step0 a + let y0' = step0 c + let r' = ((x0', b), (y0', d)) + in r' + + else if tactic == 1 then + let x1' = step0 b + let y1' = step0 d + let r' = ((a, x1'), (c, y1')) + in r' + + else if tactic == 2 then + let x0' = step0 a + let r' = ((x0', b), (c, d)) + in r' + + else if tactic == 3 then + let x1' = step0 b + let r' = ((a, x1'), (c, d)) + in r' + + else if tactic == 4 then + let y0' = step0 c + let r' = ((a, b), (y0', d)) + in r' + + else + let y1' = step0 d + let r' = ((a, b), (c, y1')) + in r' diff --git a/tests_property/CompositeTests/TupleTuple3.out b/tests_property/CompositeTests/TupleTuple3.out new file mode 100644 index 0000000000..e54a083bfe --- /dev/null +++ b/tests_property/CompositeTests/TupleTuple3.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: ((0i32, 0i32), (-1i32, 0i32)) diff --git a/tests_property/Generator/Crash.fut b/tests_property/Generator/Crash.fut new file mode 100644 index 0000000000..bbb4286c42 --- /dev/null +++ b/tests_property/Generator/Crash.fut @@ -0,0 +1,50 @@ +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- i8 tests ------------------ +-- Uniform i8 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i8 = uniform_int_distribution i8 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : i8 = + let rng0 = rng_engine.rng_from_seed [seed] + -- let (_, x) = rand_i8.rand (-100i8, 100i8) rng0 + let (_, x) = rand_i8.rand (-i8.i64 size, i8.i64 size) rng0 + in x/0 + +entry gen_simple2 (size: i64) (seed: i32) : i8 = + let rng0 = rng_engine.rng_from_seed [seed] + -- let (_, x) = rand_i8.rand (-100i8, 100i8) rng0 + let (_, x) = rand_i8.rand (-i8.i64 size, i8.i64 size) rng0 + in x + +entry gen_simple3 (size: i64) (seed: i32) : i8 = + let rng0 = rng_engine.rng_from_seed [seed] + -- let (_, x) = rand_i8.rand (-100i8, 100i8) rng0 + let (_, x) = rand_i8.rand (-i8.i64 size, i8.i64 size) rng0 + in x + +let simple_succ (x: i8) : i8 = + i8.abs x + +-- == +-- property: prop_simple_succ2 +#[prop(gen(gen_simple2), shrink(shrink_simple))] +entry prop_simple_succ2 (x: i8) : bool = + simple_succ x == i8.abs x + +-- == +-- property: prop_simple_succ +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (x: i8) : bool = + simple_succ x == i8.abs x + +-- == +-- property: prop_simple_succ3 +#[prop(gen(gen_simple3), shrink(shrink_simple))] +entry prop_simple_succ3 (x: i8) : bool = + simple_succ x == i8.abs x + +entry shrink_simple (x: i8) (_random: i32) : i8 = + if x > 0 then + x - 2 + else + x + 2 diff --git a/tests_property/Generator/Crash.out b/tests_property/Generator/Crash.out new file mode 100644 index 0000000000..c6449f10e3 --- /dev/null +++ b/tests_property/Generator/Crash.out @@ -0,0 +1 @@ +Generator failed: gen_simple has Runtime error: ["Error: division by zero","","Backtrace:","-> #0 ./Generator/Crash.fut:11:7-9",""] diff --git a/tests_property/Makefile b/tests_property/Makefile new file mode 100644 index 0000000000..e31b16d3c5 --- /dev/null +++ b/tests_property/Makefile @@ -0,0 +1,51 @@ +.PHONY: all deps test run clean concisetest +.DEFAULT_GOAL := test + +# Discover all .fut tests recursively under tests/ +TESTS := $(sort $(shell find tests -path tests/lib -prune -o -type f -name '*.fut' -print)) + +DEPS_STAMP := tests/.futhark-deps.stamp +DEPS_INPUTS := $(wildcard tests/futhark.pkg tests/futhark.lock tests/futhark.toml tests/futhark.json) + +all: test + +deps: $(DEPS_STAMP) + +$(DEPS_STAMP): $(DEPS_INPUTS) + cd tests && futhark pkg sync + @touch $@ + +run: deps + @test -n "$(file)" || (echo "Usage: make run file=tests/foo.fut" >&2; exit 2) + cabal run futhark-quickcheck -- "$(file)" + +test: deps + @echo "Building futhark-quickcheck..." + @cabal build futhark-quickcheck + @echo "Running tests..." + @set -e; \ + files="$(if $(ONLY),$(ONLY),$(TESTS))"; \ + cabal run futhark-quickcheck -- $$files + +concisetest: deps + @echo "Building futhark-quickcheck..." + @cabal build futhark-quickcheck + @echo "Running tests (concise output)..." + @set -e; \ + files="$(if $(ONLY),$(ONLY),$(TESTS))"; \ + cabal run futhark-quickcheck -- --concise $$files + +clean: + cabal clean + rm -rf tests/lib + rm -f $(DEPS_STAMP) + cd tests && rm -f *.o *.hi *.c *.so test_int test_sort_dedup + @# Sweep compiled artifacts and binaries under tests/ + @find tests -type f \( \ + -name '*.o' -o -name '*.hi' -o -name '*.c' -o -name '*.so' -o -name '*.a' -o -name '*.dylib' -o -name '*.dll' -o \ + -name '*.exe' -o -name '*.out' \ + \) -print -delete + @# Remove any remaining executables produced during tests (heuristic: executable bit set) + @find tests -type f -perm -111 \ + ! -name '*.fut' ! -name '*.txt' ! -name '*.md' ! -name '*.json' ! -name '*.toml' ! -name '*.lock' ! -name '*.pkg' \ + -print -delete \ No newline at end of file diff --git a/tests_property/NumbersTests/Stepping.fut b/tests_property/NumbersTests/Stepping.fut new file mode 100644 index 0000000000..254fe8cc96 --- /dev/null +++ b/tests_property/NumbersTests/Stepping.fut @@ -0,0 +1,38 @@ +import "../lib/github.com/diku-dk/cpprandom/random" + +type pair = (i32, i32) + +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_pair (size: i64) (seed: i32) : pair = + let rng0 = rng_engine.rng_from_seed [seed] + let (rng1, x) = rand_i32.rand (i32.lowest, i32.highest) rng0 + let (_, y) = rand_i32.rand (-i32.i64 size, i32.i64 size) rng1 + in if x > y then (x, y) else (y + 1i32, y) + +-- This is intentionally false for generated values. +-- It fails exactly when x > y and y > 0. +let bad_pair ((x, y): pair) : bool = + not (x > y && y > 0) + +-- == +-- property: prop_pair_backtrack + +#[prop(gen(gen_pair), shrink(shrink_pair))] +entry prop_pair_backtrack (p: pair) : bool = + bad_pair p + +let step_towards_zero (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_pair ((x, y): pair) (random: i32) : pair = + let tactic = random % 2 in + if tactic == 0 then + let x' = step_towards_zero x + in (x', y) + else + let y' = step_towards_zero y + in (x, y') diff --git a/tests_property/NumbersTests/Stepping.out b/tests_property/NumbersTests/Stepping.out new file mode 100644 index 0000000000..aa8840bcc5 --- /dev/null +++ b/tests_property/NumbersTests/Stepping.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_pair_backtrack size=50 seed=REDACTED after N tests +Minimal counterexample: (2i32, 1i32) diff --git a/tests_property/NumbersTests/f64.fut b/tests_property/NumbersTests/f64.fut new file mode 100644 index 0000000000..de1788aa9a --- /dev/null +++ b/tests_property/NumbersTests/f64.fut @@ -0,0 +1,37 @@ +import "../lib/github.com/diku-dk/cpprandom/random" + +------------------ f64 tests ------------------ +-- Uniform f64 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand = uniform_real_distribution f64 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : f64 = + let rng0 = rng_engine.rng_from_seed [seed] +-- let (_, x) = rand_i32.rand (i32.lowest, i32.highest) rng0 + let (_, x) = rand.rand (-f64.i64 size, f64.i64 size) rng0 + in x + +let simple_succ (x: f64) : f64 = + f64.abs x + +-- == +-- property: prop_simple_succ +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (x: f64) : bool = + simple_succ x == f64.abs x + + +let simple_fail (x: f64) : f64 = + f64.abs x + +-- == +-- property: prop_simple_fail +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (x: f64) : bool = + simple_fail x == x + +entry shrink_simple (x: f64) (_random: i32) : f64 = + if x > 0 then + x - 1 + else + x + 1 \ No newline at end of file diff --git a/tests_property/NumbersTests/f64.out b/tests_property/NumbersTests/f64.out new file mode 100644 index 0000000000..21bfbd4792 --- /dev/null +++ b/tests_property/NumbersTests/f64.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: -0.3705067640964472f64 diff --git a/tests_property/NumbersTests/i16.fut b/tests_property/NumbersTests/i16.fut new file mode 100644 index 0000000000..774fd69459 --- /dev/null +++ b/tests_property/NumbersTests/i16.fut @@ -0,0 +1,42 @@ +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- i16 tests ------------------ +-- Uniform i16 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i16 = uniform_int_distribution i16 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : i16 = + let rng0 = rng_engine.rng_from_seed [seed] +-- let (_, x) = rand_i16.rand (i32.lowest, i32.highest) rng0 + let (_, x) = rand_i16.rand (-i16.i64 size, i16.i64 size) rng0 + in x + +let simple_succ (x: i16) : i16 = + i16.abs x + +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (x: i16) : bool = + simple_succ x == i16.abs x + +let simple_fail (x: i16) : i16 = + i16.abs x + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (x: i16) : bool = + simple_fail x == x + +entry shrink_simple (x: i16) (random: i32) : i16 = + let tactic = random % 2 in + if tactic == 0 then + x//2 + else + if x > 0 then + x - 1 + else + x + 1 diff --git a/tests_property/NumbersTests/i16.out b/tests_property/NumbersTests/i16.out new file mode 100644 index 0000000000..5fd25c3d8d --- /dev/null +++ b/tests_property/NumbersTests/i16.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: -1i16 diff --git a/tests_property/NumbersTests/i32.fut b/tests_property/NumbersTests/i32.fut new file mode 100644 index 0000000000..c1626ced81 --- /dev/null +++ b/tests_property/NumbersTests/i32.fut @@ -0,0 +1,37 @@ +import "../libraries/shrinkers/integerShrinker" +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- i32 tests ------------------ +-- Uniform i32 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : i32 = + let rng0 = rng_engine.rng_from_seed [seed] +-- let (_, x) = rand_i32.rand (i32.lowest, i32.highest) rng0 + let (_, x) = rand_i32.rand (-i32.i64 size, i32.i64 size) rng0 + in x + +let simple_succ (x: i32) : i32 = + i32.abs x + +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (x: i32) : bool = + simple_succ x == i32.abs x + +let simple_fail (x: i32) : i32 = + i32.abs x + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (x: i32) : bool = + simple_fail x == x + +module shrink_i32 = integerlShrinkers i32 +entry shrink_simple (x: i32) (random: i32) : i32 = + shrink_i32.shrinker x random diff --git a/tests_property/NumbersTests/i32.out b/tests_property/NumbersTests/i32.out new file mode 100644 index 0000000000..a1d46586ce --- /dev/null +++ b/tests_property/NumbersTests/i32.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: -1i32 diff --git a/tests_property/NumbersTests/i32NoShrink.fut b/tests_property/NumbersTests/i32NoShrink.fut new file mode 100644 index 0000000000..e7b09e12b8 --- /dev/null +++ b/tests_property/NumbersTests/i32NoShrink.fut @@ -0,0 +1,32 @@ +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- i32 tests ------------------ +-- Uniform i32 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : i32 = + let rng0 = rng_engine.rng_from_seed [seed] + -- let (_, x) = rand_i32.rand (i32.lowest, i32.highest) rng0 + let (_, x) = rand_i32.rand (-i32.i64 size, i32.i64 size) rng0 + in x + +let simple_succ (x: i32) : i32 = + i32.abs x + +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +#[prop(gen(gen_simple))] +entry prop_simple_succ (x: i32) : bool = + simple_succ x == i32.abs x + +let simple_fail (x: i32) : i32 = + i32.abs x + +-- sometimes fails +#[prop(gen(gen_simple))] +entry prop_simple_fail (x: i32) : bool = + simple_fail x == x diff --git a/tests_property/NumbersTests/i32NoShrink.out b/tests_property/NumbersTests/i32NoShrink.out new file mode 100644 index 0000000000..a1d46586ce --- /dev/null +++ b/tests_property/NumbersTests/i32NoShrink.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: -1i32 diff --git a/tests_property/NumbersTests/i64.fut b/tests_property/NumbersTests/i64.fut new file mode 100644 index 0000000000..bec2a042a9 --- /dev/null +++ b/tests_property/NumbersTests/i64.fut @@ -0,0 +1,38 @@ +import "../libraries/shrinkers/integerShrinker" +import "../lib/github.com/diku-dk/cpprandom/random" + +------------------ i64 tests ------------------ +-- Uniform i64 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand = uniform_int_distribution i64 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : i64 = + let rng0 = rng_engine.rng_from_seed [seed] + -- let (_, x) = rand.rand (i64.lowest, i64.highest) rng0 + let (_, x) = rand.rand (-size, size) rng0 + in x + +let simple_succ (x: i64) : i64 = + i64.abs x + +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (x: i64) : bool = + simple_succ x == i64.abs x + +let simple_fail (x: i64) : i64 = + i64.abs x + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (x: i64) : bool = + simple_fail x == x + +module shrink_i64 = integerlShrinkers i64 +entry shrink_simple (x: i64) (random: i32) : i64 = + shrink_i64.shrinker x random diff --git a/tests_property/NumbersTests/i64.out b/tests_property/NumbersTests/i64.out new file mode 100644 index 0000000000..b9dcf5f56c --- /dev/null +++ b/tests_property/NumbersTests/i64.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: -1i64 diff --git a/tests_property/NumbersTests/i8.fut b/tests_property/NumbersTests/i8.fut new file mode 100644 index 0000000000..bfba28a797 --- /dev/null +++ b/tests_property/NumbersTests/i8.fut @@ -0,0 +1,58 @@ +import "../libraries/shrinkers/integerShrinker" +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- i8 tests ------------------ +-- Uniform i8 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i8 = uniform_int_distribution i8 u32 rng_engine +module shrink_i8 = integerlShrinkers i8 + +entry gen_simple (size: i64) (seed: i32) : i8 = + let rng0 = rng_engine.rng_from_seed [seed] + -- let (_, x) = rand_i8.rand (-100i8, 100i8) rng0 + let (_, x) = rand_i8.rand (-i8.i64 size, i8.i64 size) rng0 + in x + +let simple_succ (x: i8) : i8 = + i8.abs x + +-- Regular test case for the shrinking to fail on. +-- == +-- entry: prop_simple_succ +-- input {-10i8} +-- output {true} +-- input {10i8} +-- output {true} + +-- == +-- property: prop_simple_succ +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (x: i8) : bool = + simple_succ x == i8.abs x + +let simple_fail (x: i8) : i8 = + i8.abs x + +-- Regular test case for the shrinking to fail on. +-- == +-- entry: prop_simple_fail +-- input {10i8} +-- output {true} +-- input {-10i8} +-- output {true} + +-- this should not run but it should use num to increase number of tests +-- n== +-- property: prop_simple_fai + +-- this should run and all 3 should fail +-- == +-- property: prop_simple_fail + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (x: i8) : bool = + simple_fail x == x + +entry shrink_simple (x: i8) (random: i32) : i8 = + shrink_i8.shrinker x random + diff --git a/tests_property/NumbersTests/i8.out b/tests_property/NumbersTests/i8.out new file mode 100644 index 0000000000..ece87c6929 --- /dev/null +++ b/tests_property/NumbersTests/i8.out @@ -0,0 +1,4 @@ +Entry point: prop_simple_fail; dataset: #1 ("-10i8"): +Value #0: expected True, got False +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: -1i8 diff --git a/tests_property/NumbersTests/i8AutoShrink.fut b/tests_property/NumbersTests/i8AutoShrink.fut new file mode 100644 index 0000000000..f60e9925a1 --- /dev/null +++ b/tests_property/NumbersTests/i8AutoShrink.fut @@ -0,0 +1,33 @@ +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- i8 tests ------------------ +-- Uniform i8 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i8 = uniform_int_distribution i8 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : i8 = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_i8.rand (-i8.i64 size, i8.i64 size) rng0 + in x + +let simple_succ (x: i8) : i8 = + i8.abs x + + +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +-- suceeds +#[prop(gen(gen_simple), shrink(auto))] +entry prop_simple_succ (x: i8) : bool = + simple_succ x == i8.abs x + +let simple_fail (x: i8) : i8 = + i8.abs x + +-- sometimes fails +#[prop(gen(gen_simple), shrink(auto))] +entry prop_simple_fail (x: i8) : bool = + simple_fail x == x diff --git a/tests_property/NumbersTests/i8AutoShrink.out b/tests_property/NumbersTests/i8AutoShrink.out new file mode 100644 index 0000000000..af70830f06 --- /dev/null +++ b/tests_property/NumbersTests/i8AutoShrink.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: -1i8 diff --git a/tests_property/NumbersTests/i8WSize.fut b/tests_property/NumbersTests/i8WSize.fut new file mode 100644 index 0000000000..999dbe5fbf --- /dev/null +++ b/tests_property/NumbersTests/i8WSize.fut @@ -0,0 +1,36 @@ +import "../libraries/shrinkers/integerShrinker" +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- i8 tests ------------------ +-- Uniform i8 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i8 = uniform_int_distribution i8 u32 rng_engine +module shrink_i8 = integerlShrinkers i8 + +entry gen_simple (size: i64) (seed: i32) : i8 = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_i8.rand (-i8.i64 size, i8.i64 size) rng0 + in x + +let simple_succ (x: i8) : i8 = + i8.abs x + +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +#[prop(gen(gen_simple), shrink(shrink_simple), size(10))] +entry prop_simple_succ (x: i8) : bool = + simple_succ x == i8.abs x + +let simple_fail (x: i8) : i8 = + i8.abs x + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple), size(10))] +entry prop_simple_fail (x: i8) : bool = + simple_fail x == x + +entry shrink_simple (x: i8) (random: i32) : i8 = + shrink_i8.shrinker x random diff --git a/tests_property/NumbersTests/i8WSize.out b/tests_property/NumbersTests/i8WSize.out new file mode 100644 index 0000000000..6f978ceea3 --- /dev/null +++ b/tests_property/NumbersTests/i8WSize.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=10 seed=REDACTED after N tests +Minimal counterexample: -1i8 diff --git a/tests_property/NumbersTests/u16.fut b/tests_property/NumbersTests/u16.fut new file mode 100644 index 0000000000..42749a3d1d --- /dev/null +++ b/tests_property/NumbersTests/u16.fut @@ -0,0 +1,37 @@ +import "../libraries/shrinkers/integerShrinker" +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- u16 tests ------------------ +-- Uniform u16 distribution using minstd_rand (u16 engine) underneath. +module rng_engine = minstd_rand +module rand_u16 = uniform_int_distribution u16 u32 rng_engine +module shrink_u16 = integerlShrinkers u16 + +entry gen_simple (size: i64) (seed: i32) : u16 = + let rng0 = rng_engine.rng_from_seed [seed] +-- let (_, x) = rand_u16.rand (u16.lowest, u16.highest) rng0 + let (_, x) = rand_u16.rand (0, u16.i64 (size/2)) rng0 + in x + +let simple_succ (x: u16) : u16 = + u16.abs x + +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (x: u16) : bool = + simple_succ x == x + +let simple_fail (x: u16) : u16 = + x-(u16.highest)/2 + +-- should fail on all numbers under half of the maximum value +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (x: u16) : bool = + simple_fail x < x + +entry shrink_simple (x: u16) (random: i32) : u16 = + shrink_u16.shrinker x random diff --git a/tests_property/NumbersTests/u16.out b/tests_property/NumbersTests/u16.out new file mode 100644 index 0000000000..69922e7f72 --- /dev/null +++ b/tests_property/NumbersTests/u16.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: 0u16 diff --git a/tests_property/NumbersTests/u32.fut b/tests_property/NumbersTests/u32.fut new file mode 100644 index 0000000000..7caf7145d2 --- /dev/null +++ b/tests_property/NumbersTests/u32.fut @@ -0,0 +1,37 @@ +import "../libraries/shrinkers/integerShrinker" +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- u32 tests ------------------ +-- Uniform u32 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_u32 = uniform_int_distribution u32 u32 rng_engine +module shrink_u32 = integerlShrinkers u32 + +entry gen_simple (size: i64) (seed: i32) : u32 = + let rng0 = rng_engine.rng_from_seed [seed] +-- let (_, x) = rand_u32.rand (u32.lowest, u32.highest) rng0 + let (_, x) = rand_u32.rand (0u32, u32.i64 size) rng0 + in x + +let simple_succ (x: u32) : u32 = + u32.abs x + +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (x: u32) : bool = + simple_succ x == u32.abs x + +let simple_fail (x: u32) : u32 = + x-(u32.highest)/2 + +-- should fail on all numbers under half of the maximum value +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (x: u32) : bool = + simple_fail x < x + +entry shrink_simple (x: u32) (random: i32) : u32 = + shrink_u32.shrinker x random diff --git a/tests_property/NumbersTests/u32.out b/tests_property/NumbersTests/u32.out new file mode 100644 index 0000000000..57f31106c2 --- /dev/null +++ b/tests_property/NumbersTests/u32.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: 0u32 diff --git a/tests_property/NumbersTests/u64.fut b/tests_property/NumbersTests/u64.fut new file mode 100644 index 0000000000..99e44b2acc --- /dev/null +++ b/tests_property/NumbersTests/u64.fut @@ -0,0 +1,38 @@ +import "../libraries/shrinkers/integerShrinker" +import "../lib/github.com/diku-dk/cpprandom/random" + +------------------ u64 tests ------------------ +-- Uniform u64 distribution using minstd_rand (u32 engine) underneath. +module rng_engine_u64 = minstd_rand +module rand_u64 = uniform_int_distribution u64 u32 rng_engine_u64 +module shrink_u64 = integerlShrinkers u64 + +entry gen_simple (size: i64) (seed: i32) : u64 = + let rng0 = rng_engine_u64.rng_from_seed [seed] +-- let (_, x) = rand_u64.rand (u64.lowest, u64.highest) rng0 + let (_, x) = rand_u64.rand (0, u64.i64 size) rng0 + in x + +let simple_succ (x: u64) : u64 = + u64.abs x + +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (x: u64) : bool = + simple_succ x == u64.abs x + +let simple_fail (x: u64) : u64 = + x-(u64.highest)/2 + +-- should fail on all numbers under half of the maximum value +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (x: u64) : bool = + simple_fail x < x + +entry shrink_simple (x: u64) (random: i32) : u64 = + shrink_u64.shrinker x random diff --git a/tests_property/NumbersTests/u64.out b/tests_property/NumbersTests/u64.out new file mode 100644 index 0000000000..6c63199125 --- /dev/null +++ b/tests_property/NumbersTests/u64.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: 0u64 diff --git a/tests_property/NumbersTests/u8.fut b/tests_property/NumbersTests/u8.fut new file mode 100644 index 0000000000..1d68c93bfa --- /dev/null +++ b/tests_property/NumbersTests/u8.fut @@ -0,0 +1,37 @@ +import "../libraries/shrinkers/integerShrinker" +import "../lib/github.com/diku-dk/cpprandom/random" +--------------------- u8 tests ------------------ +-- Uniform u8 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_u8 = uniform_int_distribution u8 u32 rng_engine +module shrink_u8 = integerlShrinkers u8 + +entry gen_simple (size: i64) (seed: i32) : u8 = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_u8.rand (0u8, u8.i64 size) rng0 + in x + +let simple_succ (x: u8) : u8 = + u8.abs x + +-- == +-- property: prop_simple_succ + +-- == +-- property: prop_simple_fail + +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_succ (x: u8) : bool = + simple_succ x == u8.abs x + +let simple_fail (x: u8) : u8 = + x-(u8.highest)/2 + +-- should fail on all numbers under half of the maximum value +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (x: u8) : bool = + simple_fail x < x + + +entry shrink_simple (x: u8) (random: i32) : u8 = + shrink_u8.shrinker x random diff --git a/tests_property/NumbersTests/u8.out b/tests_property/NumbersTests/u8.out new file mode 100644 index 0000000000..26f70c59d7 --- /dev/null +++ b/tests_property/NumbersTests/u8.out @@ -0,0 +1,2 @@ +PBT FAIL: prop_simple_fail size=50 seed=REDACTED after N tests +Minimal counterexample: 0u8 diff --git a/tests_property/ShrinkerTest/InfiniteLoop.fut b/tests_property/ShrinkerTest/InfiniteLoop.fut new file mode 100644 index 0000000000..b48b812d28 --- /dev/null +++ b/tests_property/ShrinkerTest/InfiniteLoop.fut @@ -0,0 +1,34 @@ +import "../lib/github.com/diku-dk/cpprandom/random" +type tuple = (i32, i32) +--------------------- tuple tests ------------------ +-- Uniform i32 distribution using minstd_rand (u32 engine) underneath. +module rng_engine = minstd_rand +module rand_i32 = uniform_int_distribution i32 u32 rng_engine + +entry gen_simple (size: i64) (seed: i32) : tuple = + let rng0 = rng_engine.rng_from_seed [seed] + let (_, x) = rand_i32.rand (-i32.i64 size, i32.i64 size) rng0 + in (x, x-1) + +let simple (r: tuple) : (i32, i32) = + (r.0, i32.abs r.1) + +-- n== +-- property: prop_simple_fail + +-- sometimes fails +#[prop(gen(gen_simple), shrink(shrink_simple))] +entry prop_simple_fail (r: tuple) : bool = + simple r == (r.0, r.1) + +let step (v: i32) : i32 = + if v > 0 then v - 1 + else if v < 0 then v + 1 + else 0 + +entry shrink_simple (r: tuple) (random: i32) : tuple = + let tactic : i32 = random % 2 in + if tactic == 0 then + {0 = step r.0, 1 = r.1} + else + {0 = r.0, 1 = step r.1} diff --git a/tests_property/StressTest/BigArray.fut b/tests_property/StressTest/BigArray.fut new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests_property/TypeTests/PBTTypes.fut b/tests_property/TypeTests/PBTTypes.fut new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tests_property/TypeTests/PBTTypes.out b/tests_property/TypeTests/PBTTypes.out new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/tests_property/TypeTests/PBTTypes.out @@ -0,0 +1 @@ + diff --git a/tests_property/ValidationTests/GeneratorValidationTest.fut b/tests_property/ValidationTests/GeneratorValidationTest.fut new file mode 100644 index 0000000000..156dc8eb05 --- /dev/null +++ b/tests_property/ValidationTests/GeneratorValidationTest.fut @@ -0,0 +1,113 @@ +-- == +-- property: prop_ok + +-- == +-- property: prop_missing_gen + +-- == +-- property: prop_nonentry_gen + +-- == +-- property: prop_bad_output + +-- == +-- property: prop_bad_arity + +-- == +-- property: prop_bad_input_types + +-- n== +-- property: prop_div_zero + +-- == +-- property: prop_tuple_ok + + +-- GOOD PROPERTY + GOOD GENERATOR + +#[prop(gen(gen_ok), size(10))] +entry prop_ok (x: i32) : bool = + x == x + +entry gen_ok (size: i64) (seed: i32) : i32 = + i32.i64 size + seed + + +-- MISSING GENERATOR +-- Should fail validation with "No generator specified ..." + + +#[prop(size(10))] +entry prop_missing_gen (x: i32) : bool = + x == x + + +-- GENERATOR NAME EXISTS IN SOURCE BUT IS NOT AN ENTRY POINT +-- Should fail validation with "Generator is not a server entry point ..." + +let helper_not_entry (size: i64) (seed: i32) : i32 = + i32.i64 size + seed + +#[prop(gen(helper_not_entry), size(10))] +entry prop_nonentry_gen (x: i32) : bool = + x == x + + +-- BAD GENERATOR OUTPUT TYPE +-- Property expects i32, generator returns bool +-- Should fail validateGenTypes + +#[prop(gen(gen_bad_output), size(10))] +entry prop_bad_output (x: i32) : bool = + x == x + +entry gen_bad_output (size: i64) (seed: i32) : bool = + size > 0 + + +-- BAD GENERATOR ARITY +-- Current implementation does NOT catch this in validateGenTypes; +-- it is caught later by sendGenInputs at execution time. + +#[prop(gen(gen_bad_arity), size(10))] +entry prop_bad_arity (x: i32) : bool = + x == x + +entry gen_bad_arity (seed: i32) : i32 = + seed + + +-- BAD GENERATOR INPUT TYPES +-- Current implementation does NOT catch this in validateGenTypes; +-- it is caught later by sendGenInputs at execution time. + +#[prop(gen(gen_bad_input_types), size(10))] +entry prop_bad_input_types (x: i32) : bool = + x == x + +entry gen_bad_input_types (size: i32) (seed: i64) : i32 = + size + i32.i64 seed + + +-- Generator crash +-- Generator divides by zero, causing crash. + +#[nprop(gen(gen_div_zero), size(10))] +entry prop_div_zero (x: i32) : bool = + x == x + +entry gen_div_zero (size: i64) (seed: i32) : i32 = + 10/0 + + +-- VALID COMPOSITE / TUPLE MATCH +-- Property input is a tuple; generator returns matching tuple output. +-- This should be accepted. + +#[prop(gen(gen_tuple_ok), size(10))] +entry prop_tuple_ok (p: (i32, i32)) : bool = + let (x, y) = p + in x == x && y == y + +entry gen_tuple_ok (size: i64) (seed: i32) : (i32, i32) = + (i32.i64 size, seed) \ No newline at end of file diff --git a/tests_property/ValidationTests/PropertyValidationTest.fut b/tests_property/ValidationTests/PropertyValidationTest.fut new file mode 100644 index 0000000000..448fd100fb --- /dev/null +++ b/tests_property/ValidationTests/PropertyValidationTest.fut @@ -0,0 +1,60 @@ +-- == +-- property: prop_ok + + +-- == +-- property: prop_bad_output + +-- == +-- property: prop_bad_arity + +-- == +-- property: prop_div_zero + +-- == +-- property: prop_bad_arity2 + +-- == +-- property: prop_bad + + +-- GOOD PROPERTY + GOOD GENERATOR + +#[prop(gen(gen_ok), size(10))] +entry prop_ok (x: i32) : bool = + x == x + +entry gen_ok (size: i64) (seed: i32) : i32 = + i32.i64 size + seed + + +-- BAD PROPERTY OUTPUT TYPE +-- Property expects i32 returns i32 + +#[prop(gen(gen_ok), size(10))] +entry prop_bad_output (x: i32) : i32 = + 5 + +-- BAD PROPERTY ARITY + +#[prop(gen(gen_ok), size(10))] +entry prop_bad_arity (x: i32) (y: i32) : bool = + x == x + +#[prop(gen(gen_ok), size(10))] +entry prop_bad_arity2 : bool = + 1 == 1 + +#[prop(gen(gen_ok), size(10))] +#[prop(gen(gen_ok), size(10))] +entry prop_bad (x: i32) : bool = + x == x + +-- property crash +-- prop divides by zero, causing crash. +#[prop(gen(gen_ok), size(10))] +entry prop_div_zero (x: i32) : bool = + if 7/0 == 7 + then true + else false + diff --git a/tests_property/ValidationTests/PropertyValidationTest.out b/tests_property/ValidationTests/PropertyValidationTest.out new file mode 100644 index 0000000000..a37b790290 --- /dev/null +++ b/tests_property/ValidationTests/PropertyValidationTest.out @@ -0,0 +1,4 @@ +Property prop_bad_arity has 2 inputs; expected 1. +Property prop_bad_arity2 has no inputs? Expected 1. +Property prop_bad_output output must be bool, got: i32 +Property prop_div_zero has Runtime error: ["Error: division by zero","","Backtrace:","-> #0 ./ValidationTests/PropertyValidationTest.fut:57:7-9",""] diff --git a/tests_property/ValidationTests/ShrinkerValidationTests.fut b/tests_property/ValidationTests/ShrinkerValidationTests.fut new file mode 100644 index 0000000000..398ef78573 --- /dev/null +++ b/tests_property/ValidationTests/ShrinkerValidationTests.fut @@ -0,0 +1,86 @@ +-- == +-- property: prop_ok + + +-- == +-- property: prop_bad_output + +-- == +-- property: prop_bad_input + +-- == +-- property: prop_bad_arity1 + +-- == +-- property: prop_bad_arity2 + +-- n== +-- property: prop_div_zero + + + + + +-- GOOD PROPERTY + GOOD GENERATOR + +#[prop(gen(gen_ok), size(10))] +entry prop_ok (x: i32) : bool = + x == x + +entry gen_ok (size: i64) (seed: i32) : i32 = + i32.i64 size + seed + + + + +-- BAD shrinker OUTPUT TYPE + + +#[prop(gen(gen_ok), shrink(shrink_bad_output), size(10))] +entry prop_bad_output (x: i32) : bool = + x != x + +entry shrink_bad_output (x: i32) (y: i32) : i64 = + 39 + + + +-- BAD shrinker INPUT TYPE + + +#[prop(gen(gen_ok), shrink(shrink_bad_input), size(10))] +entry prop_bad_input (x: i32) : bool = + x != x + +entry shrink_bad_input (x: i32) (y: i64) : i32 = + 39 + + + +-- BAD SHRINKER ARITY + +#[prop(gen(gen_ok), shrink(shrink_bad_arity), size(10))] +entry prop_bad_arity1 (x: i32) : bool = + x != x + +entry shrink_bad_arity (x: i32) (y: i32) (z: i32) : i32 = + 39 + +#[prop(gen(gen_ok), shrink(shrink_bad_arity2), size(10))] +entry prop_bad_arity2 (x: i32) : bool = + x != x + +entry shrink_bad_arity2 : i32 = + 39 + + + +-- SHRINKER crash +-- shrink divides by zero, causing crash. +#[nprop(gen(gen_ok), shrink(shrink_div_zero), size(10))] +entry prop_div_zero (x: i32) : bool = + x != x + +entry shrink_div_zero (x: i32) (y: i32) : i32 = + x/0 + diff --git a/tests_property/ValidationTests/genEntry.fut b/tests_property/ValidationTests/genEntry.fut new file mode 100644 index 0000000000..d4cfa8e3d3 --- /dev/null +++ b/tests_property/ValidationTests/genEntry.fut @@ -0,0 +1,8 @@ +def gen (_: i64) (_: i32) : i8 = + 0 + +-- == +-- property: prop +#[prop(gen(gen))] +entry prop (x: i8) : bool = + x == 0 \ No newline at end of file diff --git a/tests_property/ValidationTests/genEntry.out b/tests_property/ValidationTests/genEntry.out new file mode 100644 index 0000000000..7484e57bf6 --- /dev/null +++ b/tests_property/ValidationTests/genEntry.out @@ -0,0 +1 @@ +Generator is not a server entry point: gen diff --git a/tests_property/ValidationTests/genSizeType.fut b/tests_property/ValidationTests/genSizeType.fut new file mode 100644 index 0000000000..483a7df446 --- /dev/null +++ b/tests_property/ValidationTests/genSizeType.fut @@ -0,0 +1,8 @@ +entry gen (_: i32) (_: i32) : i8 = + 0 + +-- == +-- property: prop +#[prop(gen(gen))] +entry prop (x: i8) : bool = + x == 0 \ No newline at end of file diff --git a/tests_property/ValidationTests/genSizeType.out b/tests_property/ValidationTests/genSizeType.out new file mode 100644 index 0000000000..1e70f39b0e --- /dev/null +++ b/tests_property/ValidationTests/genSizeType.out @@ -0,0 +1 @@ +Expected size and seed to be i64 and i32, got: size type=i32 and seed type=i32 diff --git a/tests_property/ValidationTests/noGenGiven.fut b/tests_property/ValidationTests/noGenGiven.fut new file mode 100644 index 0000000000..f070f56672 --- /dev/null +++ b/tests_property/ValidationTests/noGenGiven.fut @@ -0,0 +1,8 @@ +entry gen (_: i64) (_: i32) : i8 = + 0 + +-- == +-- property: prop +#[prop()] +entry prop (x: i8) : bool = + x == 0 \ No newline at end of file diff --git a/tests_property/ValidationTests/noGenGiven.out b/tests_property/ValidationTests/noGenGiven.out new file mode 100644 index 0000000000..0506c60bf8 --- /dev/null +++ b/tests_property/ValidationTests/noGenGiven.out @@ -0,0 +1 @@ +No generator specified for prop diff --git a/tests_property/futhark.pkg b/tests_property/futhark.pkg new file mode 100644 index 0000000000..1a85d99035 --- /dev/null +++ b/tests_property/futhark.pkg @@ -0,0 +1,4 @@ +require { + github.com/diku-dk/cpprandom 1.4.1 #c95459a4f362a56293cbefe71ef8dcb78b7a333e + github.com/diku-dk/sorts 0.7.1 #b42cfcb2d927d4192a1083f7d9efcdbfd1e5aa4d +} diff --git a/tests_property/lib/github.com/diku-dk/cpprandom/random.fut b/tests_property/lib/github.com/diku-dk/cpprandom/random.fut new file mode 100644 index 0000000000..066529e6cd --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/cpprandom/random.fut @@ -0,0 +1,589 @@ +-- | Random number generation inspired by `` in C++. +-- +-- The overall idea is that you pass a low-level `rng_engine`@mtype, +-- that knows how to generate random integers, to a parametric module +-- that maps said integers to the desired distribution. Since Futhark +-- is a pure language, the final random number function(s) will return +-- both the random number and the new state of the engine. It is the +-- programmer's responsibility to ensure that the same state is not +-- used more than once (unless that is what is desired). See the +-- [Examples](#examples) below. +-- +-- ## Examples +-- +-- This program constructs a uniform distribution of single precision +-- floats using the `minstd_rand`@term as the underlying RNG engine. +-- At the program top level the `dist` module is constructed with +-- three parameters: the real module f32 defining the output type, the +-- integral module u32 for mathematical operations on the underlying +-- random integers, and the RNG engine minstd_rand that generates the +-- raw random values. While at the expression level we use the +-- `minstd_rand` module for initialising the random number state using +-- a seed, and then we pass that state to the `rand` function in the +-- generated distribution module, along with a description of the +-- distribution we desire. We get back not just the random number, +-- but also the new state of the engine. +-- +-- ``` +-- module dist = uniform_real_distribution f32 u32 minstd_rand +-- +-- let rng = minstd_rand.rng_from_seed [123] +-- let (rng, x) = dist.rand (1,6) rng +-- ``` +-- +-- The `rand` function of `uniform_real_distribution`@term simply +-- takes a pair of numbers describing the range. In contrast, +-- `normal_distribution`@term takes a record specifying the mean and +-- standard deviation: +-- +-- ``` +-- module norm_dist = normal_distribution f32 u32 minstd_rand +-- +-- let (rng, y) = norm_dist.rand {mean=50, stddev=25} rng +-- ``` +-- +-- Since both `dist` and `norm_dist` have been initialised with the +-- same underlying `rng_engine`@mtype (`minstd_rand`@term), we can +-- re-use the same RNG state. This is often convenient when a program +-- needs to generate random numbers from several different +-- distributions, as we still only have to manage a single RNG state. +-- +-- ### Parallel random numbers +-- +-- Random number generation is inherently sequential. The `rand` +-- functions take an RNG state as input and produce a new RNG state. +-- This creates challenges when we wish to `map` a function `f` across +-- some array `xs`, and each application of the function must produce +-- some random numbers. We generally don't want to pass the exact +-- same state to every application, as that means each element will +-- see the exact same stream of random numbers. Common procedure is +-- to use `split_rng`, which creates any number of RNG states from +-- one, and then pass one to each application of `f`: +-- +-- ``` +-- let rngs = minstd_rand.split_rng n rng +-- let (rngs, ys) = unzip (map2 f rngs xs) +-- let rng = minstd_rand.join_rng rngs +-- ``` +-- +-- We assume here that the function `f` returns not just the result, +-- but also the new RNG state. Generally, all functions that accept +-- random number states should behave like this. We subsequently use +-- `join_rng` to combine all resulting states back into a single +-- state. Thus, parallel programming with random numbers involves +-- frequently splitting and re-joining RNG states. For most RNG +-- engines, these operations are generally very cheap. +-- +-- ## See also +-- +-- The `Sobol`@term@"sobol" module provides a very different +-- (and inherently parallel) way of generating random numbers, which +-- may be more suited for Monte Carlo applications. + +-- Quick and dirty hashing to mix in something that looks like entropy. +-- From http://stackoverflow.com/a/12996028 +local +def hash (x: i32) : i32 = + let x = u32.i32 x + let x = ((x >> 16) ^ x) * 0x45d9f3b + let x = ((x >> 16) ^ x) * 0x45d9f3b + let x = ((x >> 16) ^ x) + in i32.u32 x + +-- | Low-level modules that act as sources of random numbers in some +-- uniform distribution. +module type rng_engine = { + -- | The type generated by the engine. + type t + + -- | The state of the engine. + type rng + + -- | Initialise an RNG state from a seed. Even if the seed array is + -- empty, the resulting RNG should still behave reasonably. It is + -- permissible for this function to process the seed array + -- sequentially, so don't make it too large. + val rng_from_seed [n] : [n]i32 -> rng + + -- | Split an RNG state into several states. Implementations of + -- this function tend to be cryptographically unsound, so be + -- careful. + val split_rng : (n: i64) -> rng -> [n]rng + + -- | Combine several RNG states into a single state - typically done + -- with the result of `split_rng`@term. + val join_rng [n] : [n]rng -> rng + + -- | Generate a single random element, and a new RNG state. + val rand : rng -> (rng, t) + + -- | The minimum value potentially returned by the generator. + val min : t + + -- | The maximum value potentially returned by the generator. + val max : t +} + +module type rng_distribution = { + -- | The random number engine underlying this distribution. + module engine: rng_engine + + -- | A module describing the type of values produced by this random + -- distribution. + module num: numeric + + -- | The dynamic configuration of the distribution. + type distribution + + val rand : distribution -> engine.rng -> (engine.rng, num.t) +} + +-- | A linear congruential random number generator produces numbers by +-- the recurrence relation +-- +-- > X(n+1) = (a × X(n) + c) mod m +-- +-- where *X* is the sequence of pseudorandom values, and +-- +-- * *m, 0 < m* — "modulus" +-- +-- * *a, 0 < a < m* — "multiplier" +-- +-- * *c, 0 ≤ c < m* — "increment" +-- +-- * *X(0), 0 ≤ X(0) < m* — "seed" or "initial value" +module linear_congruential_engine + (T: integral) + (P: { + val a : T.t + val c : T.t + val m : T.t + }) + : rng_engine with t = T.t with rng = T.t = { + type t = T.t + type rng = t + + module int = T + + def rand (x: rng) : (rng, t) = + let rng' = (P.a T.* x T.+ P.c) T.%% P.m + in (rng', rng') + + def rng_from_seed [n] (seed: [n]i32) = + let seed' = + loop seed' = 1 + for i < n do + u32.(((seed' >> 16) ^ seed') + ^ (i32 seed[i] ^ 0b1010101010101)) + in (rand (T.u32 seed')).0 + + def split_rng (n: i64) (x: rng) : [n]rng = + let (x, _) = rand x + in tabulate n (\i -> x T.^ T.i32 (hash (i32.i64 i))) + + def join_rng [n] (xs: [n]rng) : rng = + reduce (T.^) (T.i32 0) xs + + def min = T.i32 0 + def max = P.m +} + +-- | A random number engine that uses the *subtract with carry* +-- algorithm. Presently quite slow. The size of the state is +-- proportional to the long lag. +module subtract_with_carry_engine + (T: integral) + (P: { + -- | Word size: number of bits in each word of the state sequence. + -- Should be positive and less than the number of bits in `T.t`. + val w : i32 + + -- | Long lag: distance between operand values. + val r : i32 + + -- | Short lag: number of elements between advances. Should be + -- positive and less than `r`. + val s : i32 + }) + : rng_engine with t = T.t = { + def long_lag = P.r + def word_size = P.w + def short_lag = P.s + def modulus = T.i32 (1 << word_size) + + -- We use this one for initialisation. + module e = linear_congruential_engine T { + def a = T.u32 40014u32 + def c = T.u32 0u32 + def m = T.u32 2147483563u32 + } + + def r = i64.i32 P.r + + type t = T.t + + type rng = + { x: [r]T.t + , carry: bool + , k: i32 + } + + def rand ({x, carry, k}: rng) : (rng, t) = + let short_index = k - short_lag + let short_index = + if short_index < 0 + then short_index + long_lag + else short_index + let (xi, carry) = + if T.(x[short_index] >= x[k] + bool carry) + then ( T.(x[short_index] - x[k] - bool carry) + , false + ) + else ( T.(modulus - x[k] - bool carry + x[short_index]) + , true + ) + let x = (copy x) with [k] = xi + let k = (k + 1) % long_lag + in ({x, carry, k}, xi) + + def rng_from_seed [n] (seed: [n]i32) : rng = + let rng = e.rng_from_seed seed + let (x, _) = + loop (x, rng) = (replicate r (T.i32 0), rng) + for i < P.r do + let (v, rng) = e.rand rng + in ( x with [i] = T.(v % modulus) + , rng + ) + let carry = T.(last x == i32 0) + let k = 0 + in {x, carry, k} + + def split_rng (n: i64) ({x, carry, k}: rng) : [n]rng = + tabulate n (\i -> + { x = map (T.^ (T.i32 (hash (i32.i64 i)))) x + , carry = carry && (i % 2 == 0) + , k + }) + + def join_rng [n] (xs: [n]rng) : rng = + xs[0] + + -- FIXME + + def min = T.i32 0 + def max = T.(modulus - i32 1) +} + +-- | An engine adaptor parametric module that adapts a pseudo-random +-- number generator Engine type by using only `r` elements of +-- each block of `p` elements from the sequence it produces, +-- discarding the rest. +-- +-- The adaptor keeps an internal counter of how many elements have +-- been produced in the current block. +module discard_block_engine + (K: { + -- | Block size: number of elements in each block. Must be + -- positive. + val p : i32 + + -- | Used block: number of elements in the block that are used (not + -- discarded). The rest `p-r` are discarded. This parameter should + -- be greater than zero and lower than or equal to `p`. + val r : i32 + }) + (E: rng_engine) + : rng_engine with t = E.t = { + type t = E.t + type rng = (E.rng, i32) + + def min = E.min + def max = E.max + + def rng_from_seed (xs: []i32) : rng = + (E.rng_from_seed xs, 0) + + def split_rng (n: i64) ((rng, i): rng) : [n]rng = + map (\rng' -> (rng', i)) (E.split_rng n rng) + + def join_rng (rngs: []rng) : rng = + let (rngs', is) = unzip rngs + in (E.join_rng rngs', reduce i32.max 0 is) + + def rand ((rng, i): rng) : (rng, t) = + let (rng, i) = + if i >= K.r + then (loop rng for _j < K.r - i do (E.rand rng).0, 0) + else (rng, i + 1) + let (rng, x) = E.rand rng + in ((rng, i), x) +} + +-- | An engine adaptor that adapts an `rng_engine` so that the +-- elements are delivered in a different sequence. +-- +-- The RNG keeps a buffer of `k` generated numbers internally, and +-- when requested, returns a randomly selected number within the +-- buffer, replacing it with a value obtained from its base engine. +module shuffle_order_engine (K: {val k : i32}) (I: integral) (E: rng_engine with t = I.t) + : rng_engine with t = E.t = { + def k = i64.i32 K.k + type t = E.t + type rng = (E.rng, [k]t) + + def build_table (rng: E.rng) = + let xs = replicate k (I.i32 0) + in loop (rng, xs) for i < K.k do + let (rng, x) = E.rand rng + in (rng, xs with [i] = x) + + def rng_from_seed (xs: []i32) = + build_table (E.rng_from_seed xs) + + def split_rng (n: i64) ((rng, _): rng) : [n]rng = + map build_table (E.split_rng n rng) + + def join_rng (rngs: []rng) = + let (rngs', _) = unzip rngs + in build_table (E.join_rng rngs') + + def rand ((rng, table): rng) : (rng, t) = + let (rng, x) = E.rand rng + let i = i32.i64 (I.to_i64 x) % K.k + let (rng, y) = E.rand rng + in ((rng, (copy table) with [i] = y), table[i]) + + def min = E.min + def max = E.max +} + +-- | A `linear_congruential_engine`@term producing `u32` values and +-- initialised with `a=48271`, `c=0` and +-- `m=2147483647`. This is the same configuration as in C++. +module minstd_rand : rng_engine with t = u32 = linear_congruential_engine u32 { + def a = 48271u32 + def c = 0u32 + def m = 2147483647u32 +} + +-- | A `linear_congruential_engine`@term producing `u32` values and +-- initialised with `a=16807`, `c=0` and +-- `m=2147483647`. This is the same configuration as in C++. +module minstd_rand0 : rng_engine with t = u32 = linear_congruential_engine u32 { + def a = 16807u32 + def c = 0u32 + def m = 2147483647u32 +} + +-- | A subtract-with-carry pseudo-random generator of 24-bit numbers, +-- generally used as the base engine for the `ranlux24`@term generator. +-- It is an instantiation of `subtract_with_carry_engine`@term with +-- `w=24`, `s=10`, `r=24`. +module ranlux24_base : rng_engine with t = u32 = subtract_with_carry_engine u32 { + def w : i32 = 24 + def s : i32 = 10 + def r : i32 = 24 +} + +-- | A subtract-with-carry pseudo-random generator of 48-bit numbers, +-- generally used as the base engine for the `ranlux48`@term generator. +-- It is an instantiation of `subtract_with_carry_engine`@term with +-- `w=48`, `s=5`, `r=12`. +module ranlux48_base : rng_engine with t = u64 = subtract_with_carry_engine u64 { + def w : i32 = 48 + def s : i32 = 5 + def r : i32 = 12 +} + +-- | A subtract-with-carry pseudo-random generator of 24-bit numbers +-- with accelerated advancement. +-- +-- It is an instantiation of a `discard_block_engine`@term with +-- `ranlux24_base`@term, with parameters `p=223` and `r=23`. +module ranlux24 : rng_engine with t = u32 = + discard_block_engine {def p : i32 = 223 def r : i32 = 23} ranlux24_base + +-- | A subtract-with-carry pseudo-random generator of 48-bit numbers +-- with accelerated advancement. +-- +-- It is an instantiation of a `discard_block_engine`@term with +-- `ranlux48_base`@term, with parameters `p=223` and `r=23`. +module ranlux48 : rng_engine with t = u64 = + discard_block_engine {def p : i32 = 389 def r : i32 = 11} ranlux48_base + +-- | An engine adaptor that returns shuffled sequences generated with +-- `minstd_rand0`@term. It is not a good idea to use this RNG in a +-- parallel setting, as the state size is fairly large. +module knuth_b : rng_engine with t = u32 = + shuffle_order_engine {def k : i32 = 256} u32 minstd_rand0 + +-- | The [xorshift128+](https://en.wikipedia.org/wiki/Xorshift#xorshift+) engine. Uses +-- two 64-bit words as state. +module xorshift128plus : rng_engine with t = u64 = { + type t = u64 + module int = u64 + type rng = (u64, u64) + + def rand ((x, y): rng) : (rng, u64) = + let x = x ^ (x << 23u64) + let new_x = y + let new_y = x ^ y ^ (x >> 17u64) ^ (y >> 26u64) + in ((new_x, new_y), (new_y + y)) + + -- This seeding is quite a hack to ensure that we get good results + -- even for poor seeds. The main trick is to run a couple of rounds + -- of the RNG after we're done. + def rng_from_seed [n] (seed: [n]i32) = + (loop (a, b) = (u64.i32 (hash (i32.i64 (-n))), u64.i32 (hash (i32.i64 n))) + for i < n do + if i % 2 == 0 + then (rand (a ^ u64.i32 (hash seed[i]), b)).0 + else (rand (a, b ^ u64.i32 (hash seed[i]))).0) + |> rand + |> (.0) + |> rand + |> (.0) + + def split_rng (n: i64) ((x, y): rng) : [n]rng = + tabulate n (\i -> + let (a, b) = (rand (rng_from_seed [hash (i32.i64 (i ^ n))])).0 + in (rand (rand (x ^ a, y ^ b)).0).0) + + def join_rng [n] (xs: [n]rng) : rng = + reduce (\(x1, y1) (x2, y2) -> (x1 ^ x2, y1 ^ y2)) (0u64, 0u64) xs + + def min = u64.lowest + def max = u64.highest +} + +-- | [PCG32](http://www.pcg-random.org/). Has a state space of 128 +-- bits, and produces uniformly distributed 32-bit integers. +module pcg32 : rng_engine with t = u32 = { + type t = u32 + module int = u32 + type rng = {state: u64, inc: u64} + + def rand ({state, inc}: rng) = + let oldstate = state + let state = oldstate * 6364136223846793005u64 + (inc | 1u64) + let xorshifted = u32.u64 (((oldstate >> 18u64) ^ oldstate) >> 27u64) + let rot = u32.u64 (oldstate >> 59u64) + in ( {state, inc} + , (xorshifted >> rot) | (xorshifted << ((-rot) & 31u32)) + ) + + def rng_from_seed (xs: []i32) = + let initseq = 0xda3e39cb94b95bdbu64 + -- Should expose this somehow. + let state = 0u64 + let inc = (initseq << 1u64) | 1u64 + let {state, inc} = (rand {state, inc}).0 + let state = loop state for x in xs do state + u64.i32 x + in (rand {state, inc}).0 + + def split_rng (n: i64) ({state, inc}: rng) : [n]rng = + let ith i = + let i' = hash (i32.i64 (i ^ n)) + in {state = state ^ u64.i32 i' ^ (u64.i32 i' << 32), inc} + in tabulate n ith + + def join_rng (rngs: []rng) = + let states = map (\(x: rng) -> x.state) rngs + let incs = map (\(x: rng) -> x.inc) rngs + let state = reduce (*) 1u64 states + let inc = reduce (|) 0u64 incs + in {state, inc} + + def min = 0u32 + def max = 0xFFFFFFFFu32 +} + +-- | This uniform integer distribution generates integers in a given +-- range with equal probability for each, assuming the passed +-- `rng_engine`@mtype generates uniformly distributed integers. +module uniform_int_distribution (D: integral) (I: integral) (E: rng_engine with t = I.t) + : rng_distribution + with num.t = D.t + with engine.rng = E.rng + with distribution = (D.t, D.t) = { + def to_D (x: E.t) = D.u64 (u64.i64 (I.to_i64 x)) + def to_E (x: D.t) = I.i64 (D.to_i64 x) + + module engine = E + module num = D + type distribution = (D.t, D.t) + + -- Lower and upper bounds. + def uniform (min: D.t) (max: D.t) = (min, max) + + open I + + def rand ((D_min, D_max): distribution) (rng: E.rng) = + let min = to_E D_min + let max = to_E D_max + let range = max - min + i32 1 + in if range <= i32 0 + then (rng, to_D E.min) + else -- Avoid infinite loop if range exceeds what the RNG + -- engine can supply. This does not mean that we actually + -- deliver sensible values, though. + let secure_max = E.max - E.max %% range + let (rng, x) = + loop (rng, x) = E.rand rng + while x >= secure_max do + E.rand rng + in (rng, D_min D.+ to_D (x % range)) +} + +-- | This uniform integer distribution generates floats in a given +-- range with "equal" probability for each. +module uniform_real_distribution (R: real) (I: integral) (E: rng_engine with t = I.t) + : rng_distribution + with num.t = R.t + with engine.rng = E.rng + with distribution = (R.t, R.t) = { + def to_R (x: E.t) = + R.u64 (u64.i64 (I.to_i64 x)) + + module engine = E + module num = R + type distribution = (num.t, num.t) + + -- Lower and upper bounds. + + def uniform (min: num.t) (max: num.t) = (min, max) + + def rand ((min_r, max_r): distribution) (rng: E.rng) = + let (rng', x) = E.rand rng + let x' = R.((to_R x - to_R E.min) / (to_R E.max - to_R E.min)) + in (rng', R.(min_r + x' * (max_r - min_r))) +} + +-- | Normally distributed floats. +module normal_distribution (R: real) (I: integral) (E: rng_engine with t = I.t) + : rng_distribution + with num.t = R.t + with engine.rng = E.rng + with distribution = {mean: R.t, stddev: R.t} = { + def to_R (x: E.t) = + R.u64 (u64.i64 (I.to_i64 x)) + + module engine = E + module num = R + type distribution = {mean: num.t, stddev: num.t} + + def normal (mean: num.t) (stddev: num.t) = {mean = mean, stddev = stddev} + + open R + + def rand ({mean, stddev}: distribution) (rng: E.rng) = + -- Box-Muller where we only use one of the generated points. + let (rng, u1) = E.rand rng + let (rng, u2) = E.rand rng + let u1 = (to_R u1 - to_R E.min) / (to_R E.max - to_R E.min) + let u2 = (to_R u2 - to_R E.min) / (to_R E.max - to_R E.min) + let r = sqrt (i32 (-2) * log u1) + let theta = i32 2 * pi * u2 + in (rng, mean + stddev * (r * cos theta)) +} diff --git a/tests_property/lib/github.com/diku-dk/cpprandom/random_tests.fut b/tests_property/lib/github.com/diku-dk/cpprandom/random_tests.fut new file mode 100644 index 0000000000..25f2a3ac4c --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/cpprandom/random_tests.fut @@ -0,0 +1,126 @@ +-- | ignore + +import "random" + +module mktest (dist: rng_distribution) = { + module engine = dist.engine + module num = dist.num + + def test (x: i32) (n: i64) (d: dist.distribution) = + let rng = engine.rng_from_seed [x] + let (rng, _) = dist.rand d rng + let rngs = engine.split_rng n rng + let (_, xs) = unzip (map (dist.rand d) rngs) + let mean = num.(reduce (+) (i32 0) xs / i64 n) + in mean +} + +module mktest_f (dist: rng_distribution) (R: real with t = dist.num.t) = { + module engine = dist.engine + module num = dist.num + + def test (x: i32) (n: i64) (d: dist.distribution) = + let rng = engine.rng_from_seed [x] + let (rng, _) = dist.rand d rng + let rngs = engine.split_rng n rng + let (_, xs) = unzip (map (dist.rand d) rngs) + let mean = num.(reduce (+) (i32 0) xs / i64 n) + let stddev = + R.(xs + |> map (\x -> (x - mean)) + |> map num.((** i32 2)) + |> sum + |> (/ i64 n) + |> sqrt) + in (R.round mean, R.round stddev) +} + +-- == +-- entry: test_i32_rand +-- compiled input { 0 10000i64 } output { 50 } +-- compiled input { 1 10000i64 } output { 50 } + +module test_i32_rand_m = + mktest (uniform_int_distribution i32 u32 minstd_rand) + +entry test_i32_rand (x: i32) (n: i64) = test_i32_rand_m.test x n (1, 100) + +-- Inspired by https://github.com/diku-dk/cpprandom/issues/2 +-- == +-- entry: test_i64_rand +-- compiled input { 0 10000i64 } output { -16 } +-- compiled input { 1 10000i64 } output { -15 } + +module test_i64_rand_m = + mktest (uniform_int_distribution i32 u32 minstd_rand) + +entry test_i64_rand (x: i32) (n: i64) = test_i32_rand_m.test x n (-20, -10) + +-- == +-- entry: test_i32_ranlux24_base +-- compiled input { 0 10000i64 } output { 50 } +-- compiled input { 1 10000i64 } output { 50 } + +module test_i32_ranlux24_base_m = + mktest (uniform_int_distribution i32 u32 ranlux24_base) + +entry test_i32_ranlux24_base (x: i32) (n: i64) = + test_i32_ranlux24_base_m.test x n (1, 100) + +-- == +-- entry: test_i32_ranlux24 +-- compiled input { 0 10000i64 } output { 50 } +-- compiled input { 1 10000i64 } output { 50 } + +module test_i32_ranlux24_m = + mktest (uniform_int_distribution i32 u32 ranlux24) + +entry test_i32_ranlux24 (x: i32) (n: i64) = + test_i32_ranlux24_m.test x n (1, 100) + +-- == +-- entry: test_i32_pcg32 +-- compiled input { 0 10000i64 } output { 50 } +-- compiled input { 1 10000i64 } output { 50 } + +module test_i32_pcg32_m = + mktest (uniform_int_distribution i32 u32 pcg32) + +entry test_i32_pcg32 (x: i32) (n: i64) = + test_i32_pcg32_m.test x n (1, 100) + +-- == +-- entry: test_f32_rand +-- compiled input { 0 10000i64 } output { 50.719204f32 } +-- compiled input { 1 10000i64 } output { 50.019245f32 } + +module test_f32_rand_m = + mktest (uniform_real_distribution f32 u32 minstd_rand) + +entry test_f32_rand (x: i32) (n: i64) = + test_f32_rand_m.test x n (1f32, 100f32) + +-- == +-- entry: test_f32_normal +-- compiled input { 0 10000i64 } output { 50f32 25f32 } +-- compiled input { 1 10000i64 } output { 50f32 25f32 } + +module test_f32_normal_m = + mktest_f (normal_distribution f32 u64 xorshift128plus) f32 + +entry test_f32_normal (x: i32) (n: i64) = + test_f32_normal_m.test x n {mean = 50f32, stddev = 25f32} + +-- == +-- entry: test_f32_shuffle +-- compiled input { 0 10000i64 } output { 50f32 25f32 } +-- compiled input { 1 10000i64 } output { 50f32 25f32 } + +module shuffle_m = + shuffle_order_engine {def k : i32 = 30} u32 pcg32 + +module test_f32_shuffle_m = + mktest_f (normal_distribution f32 u32 shuffle_m) f32 + +entry test_f32_shuffle (x: i32) (n: i64) = + test_f32_shuffle_m.test x n {mean = 50f32, stddev = 25f32} diff --git a/tests_property/lib/github.com/diku-dk/cpprandom/romu.fut b/tests_property/lib/github.com/diku-dk/cpprandom/romu.fut new file mode 100644 index 0000000000..2f368c1590 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/cpprandom/romu.fut @@ -0,0 +1,305 @@ +-- | A collection of `rng_engine`@term modules that implement the +-- [Romu family of random number +-- generators](http://www.romu-random.org/) by Mark Overton. While +-- the Romu generators are mostly fast on out-of-order CPUs because +-- they can be "zero latency" by fitting into otherwise unused +-- execution slots, they may also be useful on GPU. In particular, +-- the 32-bit variants run very fast. +-- +-- As usual, the seeding, splitting, and joining functions are not +-- part of the upstream Romu algorithm, but are simply best-effort +-- implementations that try to mix in a little different entropy. +-- Caveat emptor. + +open import "random" + +-- The programming style has been left similar to the upstream Romu +-- implementations in C. + +local +def ROTL64 (x: u64, n: u64) = + (x << n) | (x >> (64 - n)) + +local +def ROTL32 (x: u32, n: u32) = + (x << n) | (x >> (32 - n)) + +-- | More robust than anyone could need, but uses more registers than +-- `romu_trio`@term. +-- +-- * Est. capacity: 2⁹⁰ bytes +-- * State size: 256 bits +module romu_quad : rng_engine with t = u64 = { + type t = u64 + type rng = {w: u64, x: u64, y: u64, z: u64} + + def rng_from_seed (ss: []i32) = + loop {w, x, y, z} = {w = 1, x = 2, y = 3, z = 4} + for s in ss do + { w = w ^ u64.i32 s ^ 1 + , x = x ^ u64.i32 s ^ 1 + , y = y ^ u64.i32 s ^ 2 + , z = z ^ u64.i32 s ^ 3 + } + + def rand {w = wp, x = xp, y = yp, z = zp} = + let wState = 15241094284759029579 * zp + let xState = zp + ROTL64 (wp, 52) + let yState = yp - xp + let zState = yp + wp + let zState = ROTL64 (zState, 19) + in ({w = wState, x = xState, y = yState, z = zState}, xp) + + def split_rng (n: i64) {w, x, y, z} = + tabulate n (\i -> + rand { w = w ^ u64.i64 i + , x = x ^ u64.i64 i + , y = y ^ u64.i64 i + , z = z ^ u64.i64 i + } + |> (.0)) + + def join_rng (rngs: []rng) = + { w = reduce (^) 0 (map (.w) rngs) + , x = reduce (^) 0 (map (.x) rngs) + , y = reduce (^) 0 (map (.y) rngs) + , z = reduce (^) 0 (map (.z) rngs) + } + + def min = u64.lowest + def max = u64.highest +} + +-- | Great for general purpose work, including huge jobs. +-- +-- * Est. capacity: 2⁷⁵ bytes +-- * State size: 192 bits +module romu_trio : rng_engine with t = u64 = { + type t = u64 + type rng = {x: u64, y: u64, z: u64} + + def rng_from_seed (ss: []i32) = + loop {x, y, z} = {x = 1, y = 2, z = 3} + for s in ss do + { x = x ^ u64.i32 s ^ 1 + , y = y ^ u64.i32 s ^ 2 + , z = z ^ u64.i32 s ^ 3 + } + + def rand {x = xp, y = yp, z = zp} = + let xState = 15241094284759029579 * zp + let yState = yp - xp + let yState = ROTL64 (yState, 12) + let zState = zp - yp + let zState = ROTL64 (zState, 44) + in ({x = xState, y = yState, z = zState}, xp) + + def split_rng (n: i64) {x, y, z} = + tabulate n (\i -> + rand { x = x ^ u64.i64 i + , y = y ^ u64.i64 i + , z = z ^ u64.i64 i + } + |> (.0)) + + def join_rng (rngs: []rng) = + { x = reduce (^) 0 (map (.x) rngs) + , y = reduce (^) 0 (map (.y) rngs) + , z = reduce (^) 0 (map (.z) rngs) + } + + def min = u64.lowest + def max = u64.highest +} + +-- | Might be faster than `romu_trio`@term due to using fewer +-- registers, but might struggle with massive jobs. +-- +-- * Est. capacity: 2⁶¹ bytes +-- * State size: 128 bits +module romu_duo : rng_engine with t = u64 = { + type t = u64 + type rng = {x: u64, y: u64} + + def rng_from_seed (ss: []i32) = + loop {x, y} = {x = 1, y = 2} + for s in ss do + { x = x ^ u64.i32 s ^ 1 + , y = y ^ u64.i32 s ^ 2 + } + + def rand {x = xp, y = yp} = + let xState = 15241094284759029579 * yp + let yState = ROTL64 (yp, 36) + ROTL64 (yp, 15) - xp + in ({x = xState, y = yState}, xp) + + def split_rng (n: i64) {x, y} = + tabulate n (\i -> + rand { x = x ^ u64.i64 i + , y = y ^ u64.i64 i + } + |> (.0)) + + def join_rng (rngs: []rng) = + { x = reduce (^) 0 (map (.x) rngs) + , y = reduce (^) 0 (map (.y) rngs) + } + + def min = u64.lowest + def max = u64.highest +} + +-- | The fastest generator using 64-bit arithmetic, but not suited for +-- huge jobs. +-- +-- * Est. capacity: 2⁵¹ bytes +-- * State size: 128 bits +module romu_duo_jr : rng_engine with t = u64 = { + type t = u64 + type rng = {x: u64, y: u64} + + def rng_from_seed (ss: []i32) = + loop {x, y} = {x = 1, y = 2} + for s in ss do + { x = x ^ u64.i32 s ^ 1 + , y = y ^ u64.i32 s ^ 2 + } + + def rand {x = xp, y = yp} = + let xState = 15241094284759029579 * yp + let yState = yp - xp + let yState = ROTL64 (yState, 27) + in ({x = xState, y = yState}, xp) + + def split_rng (n: i64) {x, y} = + tabulate n (\i -> + rand { x = x ^ u64.i64 i + , y = y ^ u64.i64 i + } + |> (.0)) + + def join_rng (rngs: []rng) = + { x = reduce (^) 0 (map (.x) rngs) + , y = reduce (^) 0 (map (.y) rngs) + } + + def min = u64.lowest + def max = u64.highest +} + +-- | 32-bit arithmetic: Good for general purpose use. +-- +-- * Est. capacity: 2⁶¹ bytes +-- * State size: 128 +module romu_quad32 : rng_engine with t = u32 = { + type t = u32 + type rng = {w: u32, x: u32, y: u32, z: u32} + + def rng_from_seed (ss: []i32) = + loop {w, x, y, z} = {w = 1, x = 2, y = 3, z = 4} + for s in ss do + { w = w ^ u32.i32 s ^ 1 + , x = x ^ u32.i32 s ^ 1 + , y = y ^ u32.i32 s ^ 2 + , z = z ^ u32.i32 s ^ 3 + } + + def rand {w = wp, x = xp, y = yp, z = zp} = + let wState = 3323815723 * zp + let xState = zp + ROTL32 (wp, 26) + let yState = yp - xp + let zState = yp + wp + let zState = ROTL32 (zState, 9) + in ({w = wState, x = xState, y = yState, z = zState}, xp) + + def split_rng (n: i64) {w, x, y, z} = + tabulate n (\i -> + rand { w = w ^ u32.i64 i + , x = x ^ u32.i64 i + , y = y ^ u32.i64 i + , z = z ^ u32.i64 i + } + |> (.0)) + + def join_rng (rngs: []rng) = + { w = reduce (^) 0 (map (.w) rngs) + , x = reduce (^) 0 (map (.x) rngs) + , y = reduce (^) 0 (map (.y) rngs) + , z = reduce (^) 0 (map (.z) rngs) + } + + def min = u32.lowest + def max = u32.highest +} + +-- | 32-bit arithmetic: Good for general purpose use, except for huge jobs. +-- +-- * Est. capacity: 2⁵³ bytes +-- * State size = 96 bits. +module romu_trio32 : rng_engine with t = u32 = { + type t = u32 + type rng = {x: u32, y: u32, z: u32} + + def rng_from_seed (ss: []i32) = + loop {x, y, z} = {x = 1, y = 2, z = 3} + for s in ss do + { x = x ^ u32.i32 s ^ 1 + , y = y ^ u32.i32 s ^ 2 + , z = z ^ u32.i32 s ^ 3 + } + + def rand {x = xp, y = yp, z = zp} = + let xState = 3323815723 * zp + let yState = yp - xp + let yState = ROTL32 (yState, 6) + let zState = zp - yp + let zState = ROTL32 (zState, 22) + in ({x = xState, y = yState, z = zState}, xp) + + def split_rng (n: i64) {x, y, z} = + tabulate n (\i -> + rand { x = x ^ u32.i64 i + , y = y ^ u32.i64 i + , z = z ^ u32.i64 i + } + |> (.0)) + + def join_rng (rngs: []rng) = + { x = reduce (^) 0 (map (.x) rngs) + , y = reduce (^) 0 (map (.y) rngs) + , z = reduce (^) 0 (map (.z) rngs) + } + + def min = u32.lowest + def max = u32.highest +} + +-- | 32-bit arithmetic: Suitable only up to 2²⁶ +-- output-values. Outputs 16-bit numbers. Fixed period of +-- (2³²)-47. +-- +-- * Capacity: 2²⁷ bytes +-- * State size; 32 bits +module romu_mono32 : rng_engine with t = u16 = { + type rng = u32 + type t = u16 + + def rng_from_seed (ss: []i32) : rng = + loop acc = 0u32 + for seed in ss do + acc ^ (u32.i32 seed & 0x1fffffff) + 1156979152 + + def rand (state: u32) = + let result = u16.u32 (state >> 16) + let state = state * 3611795771 + let state = ROTL32 (state, 12) + in (state, result) + + def split_rng (n: i64) state = + tabulate n (\i -> (rand (state ^ u32.i64 i)).0) + + def join_rng = reduce (^) 0u32 + + def min = u16.lowest + def max = u16.highest +} diff --git a/tests_property/lib/github.com/diku-dk/cpprandom/romu_tests.fut b/tests_property/lib/github.com/diku-dk/cpprandom/romu_tests.fut new file mode 100644 index 0000000000..93927ea897 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/cpprandom/romu_tests.fut @@ -0,0 +1,33 @@ +-- | ignore + +import "romu" + +module util = import "random_tests" + +module test_romu_quad_m = util.mktest (uniform_int_distribution i32 u64 romu_quad) + +module test_romu_trio_m = util.mktest (uniform_int_distribution i32 u64 romu_trio) + +module test_romu_duo_m = util.mktest (uniform_int_distribution i32 u64 romu_duo) + +module test_romu_duo_jr_m = util.mktest (uniform_int_distribution i32 u64 romu_duo_jr) + +module test_romu_quad32_m = util.mktest (uniform_int_distribution i32 u32 romu_quad32) + +module test_romu_trio32_m = util.mktest (uniform_int_distribution i32 u32 romu_trio32) + +module test_romu_mono32_m = util.mktest (uniform_int_distribution i32 u16 romu_mono32) + +entry test_romu_quad (x: i32) (n: i64) = test_romu_quad_m.test x n (1, 100) +entry test_romu_trio (x: i32) (n: i64) = test_romu_trio_m.test x n (1, 100) +entry test_romu_duo (x: i32) (n: i64) = test_romu_duo_m.test x n (1, 100) +entry test_romu_duo_jr (x: i32) (n: i64) = test_romu_duo_jr_m.test x n (1, 100) + +entry test_romu_quad32 (x: i32) (n: i64) = test_romu_quad32_m.test x n (1, 100) +entry test_romu_trio32 (x: i32) (n: i64) = test_romu_trio32_m.test x n (1, 100) +entry test_romu_mono32 (x: i32) (n: i64) = test_romu_mono32_m.test x n (1, 100) + +-- == +-- entry: test_romu_quad test_romu_trio test_romu_duo test_romu_duo_jr test_romu_quad32 test_romu_trio32 test_romu_mono32 +-- compiled input { 0 1000000i64 } output { 50 } +-- compiled input { 1 1000000i64 } output { 50 } diff --git a/tests_property/lib/github.com/diku-dk/cpprandom/shuffle.fut b/tests_property/lib/github.com/diku-dk/cpprandom/shuffle.fut new file mode 100644 index 0000000000..4a1f4b03cb --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/cpprandom/shuffle.fut @@ -0,0 +1,56 @@ +-- | Random shuffling of an array in parallel. + +open import "random" + +local +module type shuffle = { + type rng + + -- | Given a source of random numbers, shuffle an array. + val shuffle [n] 't : rng -> [n]t -> (rng, [n]t) + + -- | Given `n` sources of random numbers, shuffle an `n` element array. + val shuffle' [n] 't : [n]rng -> [n]t -> ([n]rng, [n]t) +} + +module mk_shuffle (I: integral) (E: rng_engine with t = I.t) : shuffle with rng = E.rng = { + type rng = E.rng + + def radix_sort_step [n] 't + (xs: [n]t) + (get_bit: i32 -> t -> i32) + (digit_n: i32) : [n]t = + let bits = map (get_bit digit_n) xs + let bits_inv = map (1 -) bits + let ps0 = scan (+) 0 bits_inv + let ps0_clean = map2 (*) bits_inv ps0 + let ps1 = scan (+) 0 bits + let ps0_offset = reduce (+) 0 bits_inv + let ps1_clean = map (+ ps0_offset) ps1 + let ps1_clean' = map2 (*) bits ps1_clean + let ps = map2 (+) ps0_clean ps1_clean' + let ps_actual = map (\x -> x - 1) ps + in scatter (copy xs) (map i64.i32 ps_actual) xs + + def radix_sort [n] 't + (num_bits: i32) + (get_bit: i32 -> t -> i32) + (xs: [n]t) : [n]t = + loop xs for i < num_bits do radix_sort_step xs get_bit i + + module dist = uniform_int_distribution i64 I E + + def shuffle' [n] 't rngs (xs: [n]t) = + let (rngs', keys) = map (dist.rand (0, n - 1)) rngs |> unzip + let get_bit i x = i64.get_bit i keys[x] + let num_bits = i32.f64 (f64.ceil (f64.log2 (f64.i64 n))) + let xs' = + radix_sort num_bits get_bit (iota n) + |> map (\i -> xs[i]) + in (rngs', xs') + + def shuffle [n] 't rng (xs: [n]t) = + let rngs = E.split_rng n rng + let (rngs', xs') = shuffle' rngs xs + in (E.join_rng rngs', xs') +} diff --git a/tests_property/lib/github.com/diku-dk/cpprandom/shuffle_tests.fut b/tests_property/lib/github.com/diku-dk/cpprandom/shuffle_tests.fut new file mode 100644 index 0000000000..a719243f85 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/cpprandom/shuffle_tests.fut @@ -0,0 +1,15 @@ +-- | ignore + +import "shuffle" + +module shuffle = mk_shuffle u32 pcg32 + +-- == +-- entry: test_shuffle +-- input { 10i64 } output { 45i64 true } +-- input { 1000i64 } output { 499500i64 true } +entry test_shuffle (n: i64) = + let rng = pcg32.rng_from_seed [123, i32.i64 n, 42] + let (_, xs) = shuffle.shuffle rng (iota n) + let sorted = map2 (<=) xs[:n - 1] (rotate 1 xs)[:n - 1] |> and + in (i64.sum xs, !sorted) diff --git a/tests_property/lib/github.com/diku-dk/segmented/segmented.fut b/tests_property/lib/github.com/diku-dk/segmented/segmented.fut new file mode 100644 index 0000000000..6b4dbb4c9f --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/segmented/segmented.fut @@ -0,0 +1,111 @@ +-- | Irregular segmented operations, like scans and reductions. + +-- | Segmented scan. Given a binary associative operator ``op`` with +-- neutral element ``ne``, computes the inclusive prefix scan of the +-- segments of ``as`` specified by the ``flags`` array, where `true` +-- starts a segment and `false` continues a segment. +def segmented_scan [n] 't + (op: t -> t -> t) + (ne: t) + (flags: [n]bool) + (as: [n]t) : *[n]t = + (unzip (scan (\(x_flag, x) (y_flag, y) -> + ( x_flag || y_flag + , if y_flag then y else x `op` y + )) + (false, ne) + (zip flags as))).1 + +-- | Segmented reduction. Given a binary associative operator ``op`` +-- with neutral element ``ne``, computes the reduction of the segments +-- of ``as`` specified by the ``flags`` array, where `true` starts a +-- segment and `false` continues a segment. One value is returned per +-- segment. +def segmented_reduce [n] 't + (op: t -> t -> t) + (ne: t) + (flags: [n]bool) + (as: [n]t) = + segmented_scan op ne flags as + |> zip (rotate 1 flags) + |> filter (.0) + |> map (.1) + +-- | Replicated iota. Given a repetition array, the function returns +-- an array with each index (starting from 0) repeated according to +-- the repetition array. As an example, replicated_iota [2,3,1] +-- returns the array [0,0,1,1,1,2]. +def replicated_iota [n] (reps: [n]i64) : []i64 = + let offsets = scan (+) 0 reps + let size = reduce_comm (+) 0 reps + let tmp = scatter (replicate size 0) offsets (iota n |> map (+ 1)) + in scan i64.max i64.lowest tmp + +-- | Segmented iota. Given a flags array, the function returns an +-- array of index sequences, each of which is reset according to the +-- flags array. As an examples, segmented_iota +-- [false,false,false,true,false,false,false] returns the array +-- [0,1,2,0,1,2,3]. +def segmented_iota [n] (flags: [n]bool) : *[n]i64 = + let iotas = segmented_scan (+) 0 flags (replicate n 1) + in map (\x -> x - 1) iotas + +-- | Replicated and segemented iota generated together +-- in a slighly more efficient way. +-- each segment in the segmented iota corresponds to a segment +-- in the replicated iota. As an example repl_segm_iota [2,3,1] +-- returns the arrays [0,0,1,1,1,2] and [0,1,0,1,2,0]. +def repl_segm_iota [n] (reps: [n]i64) : (*[]i64, *[]i64) = + let offsets = scan (+) 0 reps + let size = reduce_comm (+) 0 reps + let tmp = scatter (rep 0) offsets (iota n |> map (+ 1)) + let repl = scan i64.max i64.lowest tmp + let segm = map2 (\i r -> i - if r == 0 then 0 else offsets[r - 1]) (iota size) repl + in (repl, segm) + +-- | Generic expansion function. The function expands a source array +-- into a target array given (1) a function that determines, for each +-- source element, how many target elements it expands to and (2) a +-- function that computes a particular target element based on a +-- source element and the target element number associated with the +-- source. As an example, the expression expand (\x->x) (*) [2,3,1] +-- returns the array [0,2,0,3,6,0]. +def expand 'a 'b (sz: a -> i64) (get: a -> i64 -> b) (arr: []a) : *[]b = + let szs = map sz arr + let (idxs, iotas) = repl_segm_iota szs + in map2 (\i j -> get arr[i] j) idxs iotas + +-- | Expansion function equivalent to performing a segmented reduction +-- to the result of a general expansion with a flags vector expressing +-- the beginning of the expanded segments. The function makes use of +-- the intermediate flags vector generated as part of the expansion +-- and the `expand_reduce` function is therefore more efficient than +-- if a segmented reduction (with an appropriate flags vector) is +-- explicitly followed by a call to expand. +def expand_reduce 'a 'b + (sz: a -> i64) + (get: a -> i64 -> b) + (op: b -> b -> b) + (ne: b) + (arr: []a) : *[]b = + let szs = map sz arr + let idxs = replicated_iota szs + let flags = map2 (!=) idxs (rotate (-1) idxs) + let iotas = segmented_iota flags + let vs = map2 (\i j -> get arr[i] j) idxs iotas + in segmented_reduce op ne flags vs + +-- | Expansion followed by an ''outer segmented reduce'' that ensures +-- that each element in the result array corresponds to expanding and +-- reducing the corresponding element in the source array. +def expand_outer_reduce 'a 'b [n] + (sz: a -> i64) + (get: a -> i64 -> b) + (op: b -> b -> b) + (ne: b) + (arr: [n]a) : *[n]b = + let sz' x = + let s = sz x + in if s == 0 then 1 else s + let get' x i = if sz x == 0 then ne else get x i + in expand_reduce sz' get' op ne arr :> [n]b diff --git a/tests_property/lib/github.com/diku-dk/segmented/segmented_tests.fut b/tests_property/lib/github.com/diku-dk/segmented/segmented_tests.fut new file mode 100644 index 0000000000..6984792730 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/segmented/segmented_tests.fut @@ -0,0 +1,74 @@ +-- | ignore + +import "segmented" + +-- == +-- entry: test_segmented_scan +-- input { [true,false,false,true,false,false,true,false,false,false] +-- [1i64,2i64,3i64,4i64,5i64,6i64,7i64,8i64,9i64,10i64] } +-- output { [1i64,3i64,6i64,4i64,9i64,15i64,7i64,15i64,24i64,34i64] } +-- input { [true] [1i64] } +-- output { [1i64] } +-- input { empty([0]bool) empty([0]i64) } +-- output { empty([0]i64) } + +entry test_segmented_scan (flags: []bool) (as: []i64) = + segmented_scan (+) 0 flags as + +-- == +-- entry: test_segmented_reduce +-- input { [true,false,false,true,false,false,true,false,false,false] +-- [1i64,2i64,3i64,4i64,5i64,6i64,7i64,8i64,9i64,10i64] } +-- output { [6i64,15i64,34i64] } +-- input { [true] [1i64] } +-- output { [1i64] } + +entry test_segmented_reduce (flags: []bool) (as: []i64) = + segmented_reduce (+) 0 flags as + +-- == +-- entry: test_replicated_iota +-- input { [2i64,3i64,1i64] } output { [0i64,0i64,1i64,1i64,1i64,2i64] } +-- input { [3i64] } output { [0i64,0i64,0i64] } +-- input { [2i64,0i64,1i64] } output { [0i64,0i64,2i64] } +-- input { empty([0]i64) } output { empty([0]i64) } +-- input { [0i64] } output { empty([0]i64) } +-- input { [0i64,0i64] } output { empty([0]i64) } + +entry test_replicated_iota (repl:[]i64) : []i64 = + replicated_iota repl + +-- == +-- entry: test_segmented_iota +-- input { [false,false,false,true,false,false,false] } +-- output { [0i64,1i64,2i64,0i64,1i64,2i64,3i64] } +-- input { [false] } output { [0i64] } +-- input { [true] } output { [0i64] } +-- input { empty([0]bool) } output { empty([0]i64) } + +entry test_segmented_iota (flags:[]bool) : []i64 = + segmented_iota flags + +-- == +-- entry: test_expand +-- input { [2i64,3i64,1i64] } +-- output { [0i64,2i64,0i64,3i64,6i64,0i64] } + +entry test_expand (arr:[]i64) : []i64 = + expand (\ x -> x) (\x i -> x*i) arr + +-- == +-- entry: test_expand_reduce +-- input { [2i64,0i64,3i64,1i64] } +-- output { [2i64,9i64,0i64] } + +entry test_expand_reduce (arr:[]i64) : []i64 = + expand_reduce (\ x -> x) (\x i -> x*i) (+) 0 arr + +-- == +-- entry: test_expand_outer_reduce +-- input { [2i64,0i64,3i64,1i64] } +-- output { [2i64,0i64,9i64,0i64] } + +entry test_expand_outer_reduce (arr:[]i64) : []i64 = + expand_outer_reduce (\ x -> x) (\x i -> x*i) (+) 0 arr diff --git a/tests_property/lib/github.com/diku-dk/sorts/.gitignore b/tests_property/lib/github.com/diku-dk/sorts/.gitignore new file mode 100644 index 0000000000..1cdd37e613 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/.gitignore @@ -0,0 +1,3 @@ +* +!*.fut +!.gitignore diff --git a/tests_property/lib/github.com/diku-dk/sorts/bitonic_sort.fut b/tests_property/lib/github.com/diku-dk/sorts/bitonic_sort.fut new file mode 100644 index 0000000000..26c5851857 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/bitonic_sort.fut @@ -0,0 +1,63 @@ +-- | Bitonic sort. +-- +-- Runs in *O(n log²(n))* work and *O(log²(n))* span. Internally pads +-- the array to the next power of two, so a poor fit for some array +-- sizes. +-- +-- ## See Also +-- +-- * `merge_sort`@term@"merge_sort" + +local +def log2 (n: i64) : i64 = + let r = 0 + let (r, _) = + loop (r, n) while 1 < n do + let n = n / 2 + let r = r + 1 + in (r, n) + in r + +local +def ensure_pow_2 [n] 't ((<=): t -> t -> bool) (xs: [n]t) : (*[]t, i64) = + if n == 0 + then (copy xs, 0) + else let d = log2 n + in if n == 2 ** d + then (copy xs, d) + else let largest = reduce (\x y -> if x <= y then y else x) xs[0] xs + in ( concat xs (replicate (2 ** (d + 1) - n) largest) + , d + 1 + ) + +local +def kernel_par [n] 't ((<=): t -> t -> bool) (a: *[n]t) (p: i64) (q: i64) : *[n]t = + let d = 1 << (p - q) + in tabulate n (\i -> + let a_i = a[i] + let up1 = ((i >> p) & 2) == 0 + in if (i & d) == 0 + then let a_iord = a[i | d] + in if a_iord <= a_i == up1 + then a_iord + else a_i + else let a_ixord = a[i ^ d] + in if a_i <= a_ixord == up1 + then a_ixord + else a_i) + +-- | Sort an array in increasing order. +def bitonic_sort [n] 't ((<=): t -> t -> bool) (xs: [n]t) : *[n]t = + -- We need to pad the array so that its size is a power of 2. We do + -- this by first finding the largest element in the input, and then + -- using that for the padding. Then we know that the padding will + -- all be at the end, so we can easily cut it off. + let (xs, d) = ensure_pow_2 (<=) xs + in (loop xs for i < d do + loop xs for j < i + 1 do kernel_par (<=) xs i j)[:n] + +-- | Like `bitonic_sort`, but sort based on key function. +def bitonic_sort_by_key [n] 't 'k (key: t -> k) ((<=): k -> k -> bool) (xs: [n]t) : [n]t = + zip (map key xs) (iota n) + |> bitonic_sort (\(x, _) (y, _) -> x <= y) + |> map (\(_, i) -> xs[i]) diff --git a/tests_property/lib/github.com/diku-dk/sorts/bitonic_sort_tests.fut b/tests_property/lib/github.com/diku-dk/sorts/bitonic_sort_tests.fut new file mode 100644 index 0000000000..2e5c5d5403 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/bitonic_sort_tests.fut @@ -0,0 +1,48 @@ +-- | ignore + +import "bitonic_sort" + +-- == +-- entry: sort_i32 +-- input { empty([0]i32) } +-- output { empty([0]i32) } +-- input { [5,4,3,2,1] } +-- output { [1,2,3,4,5] } +-- input { [5,4,3,3,2,1] } +-- output { [1,2,3,3,4,5] } + +entry sort_i32 (xs: []i32) = bitonic_sort (i32.<=) xs + +-- == +-- entry: sort_u16 +-- input { [5u16,4u16,3u16,2u16,1u16] } +-- output { [1u16,2u16,3u16,4u16,5u16] } + +entry sort_u16 (xs: []u16) = bitonic_sort (u16.<=) xs + +-- == +-- entry: sort_f32 +-- input { [5f32,4f32,3f32,2f32,1f32] } +-- output { [1f32,2f32,3f32,4f32,5f32] } + +entry sort_f32 (xs: []f32) = bitonic_sort (f32.<=) xs + +-- == +-- entry: sort_perm_i32 +-- input { [5,4,3,2,1,0,-1,-2] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_i32 [n] (xs: [n]i32) = + zip xs (iota n) + |> bitonic_sort_by_key (.0) (<=) + |> map ((.1) >-> i32.i64) + +-- == +-- entry: sort_perm_f32 +-- input { [5f32,4f32,3f32,2f32,1f32,0f32,-1f32,-2f32] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_f32 [n] (xs: [n]f32) = + zip xs (iota n) + |> bitonic_sort_by_key (.0) (<=) + |> map ((.1) >-> i32.i64) diff --git a/tests_property/lib/github.com/diku-dk/sorts/bubble_sort.fut b/tests_property/lib/github.com/diku-dk/sorts/bubble_sort.fut new file mode 100644 index 0000000000..d3e3390438 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/bubble_sort.fut @@ -0,0 +1,28 @@ +-- | Parallel bubble sort. +-- +-- This may be useful if you have almost-sorted data that you want to +-- make fully-sorted in parallel. Obviously *very* slow for +-- non-sorted data. + +-- | Parallel bubble sort. Runs with *O(n^2)* work and *O(n^2)* depth. +def bubble_sort [n] 't ((<=): t -> t -> bool) (xs: [n]t) : [n]t = + let f b xs i = + let dir = if i % 2 == 0 then b else -b + let j = i + dir + let cmp x y = + if dir == 1 + then x <= y + else !(x <= y) + in if j >= 0 && j < n && (xs[j] `cmp` xs[i]) + then (true, xs[j]) + else (false, xs[i]) + let iter xs b = + let (changed, xs) = tabulate n (f b xs) |> unzip + in (xs, -b, or changed) + in (loop (xs, b, continue) = (xs, 1, true) while continue do iter xs b).0 + +-- | Like `bubble_sort`@term, but sort based on key function. +def bubble_sort_by_key [n] 't 'k (key: t -> k) ((<=): k -> k -> bool) (xs: [n]t) : [n]t = + zip (map key xs) (iota n) + |> bubble_sort (\(x, _) (y, _) -> x <= y) + |> map (\(_, i) -> xs[i]) diff --git a/tests_property/lib/github.com/diku-dk/sorts/bubble_sort_tests.fut b/tests_property/lib/github.com/diku-dk/sorts/bubble_sort_tests.fut new file mode 100644 index 0000000000..1bb1066283 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/bubble_sort_tests.fut @@ -0,0 +1,48 @@ +-- | ignore + +import "bubble_sort" + +-- == +-- entry: sort_i32 +-- input { empty([0]i32) } +-- output { empty([0]i32) } +-- input { [5,4,3,2,1] } +-- output { [1,2,3,4,5] } +-- input { [5,4,3,3,2,1] } +-- output { [1,2,3,3,4,5] } + +entry sort_i32 (xs: []i32) = bubble_sort (i32.<=) xs + +-- == +-- entry: sort_u16 +-- input { [5u16,4u16,3u16,2u16,1u16] } +-- output { [1u16,2u16,3u16,4u16,5u16] } + +entry sort_u16 (xs: []u16) = bubble_sort (u16.<=) xs + +-- == +-- entry: sort_f32 +-- input { [5f32,4f32,3f32,2f32,1f32] } +-- output { [1f32,2f32,3f32,4f32,5f32] } + +entry sort_f32 (xs: []f32) = bubble_sort (f32.<=) xs + +-- == +-- entry: sort_perm_i32 +-- input { [5,4,3,2,1,0,-1,-2] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_i32 [n] (xs: [n]i32) = + zip xs (iota n) + |> bubble_sort_by_key (.0) (<=) + |> map ((.1) >-> i32.i64) + +-- == +-- entry: sort_perm_f32 +-- input { [5f32,4f32,3f32,2f32,1f32,0f32,-1f32,-2f32] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_f32 [n] (xs: [n]f32) = + zip xs (iota n) + |> bubble_sort_by_key (.0) (<=) + |> map ((.1) >-> i32.i64) diff --git a/tests_property/lib/github.com/diku-dk/sorts/insertion_sort.fut b/tests_property/lib/github.com/diku-dk/sorts/insertion_sort.fut new file mode 100644 index 0000000000..70274eace3 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/insertion_sort.fut @@ -0,0 +1,29 @@ +-- | A sequential implementation of insertion sort. + +local +def swap 't [n] (i: i64) (j: i64) (xs: *[n]t) : *[n]t = + -- Need copies to prevent the uniqueness checker from getting + -- cranky. + let xi = copy xs[i] + let xs[i] = copy xs[j] + let xs[j] = xi + in xs + +-- | Insertion sort. Runs with *O(n^2)* work and *O(n^2)* depth. +def insertion_sort [n] 't ((<=): t -> t -> bool) (xs: [n]t) : *[n]t = + -- Make a copy of the array so we can operate in-place. + loop xs = copy xs + for i in 1.. 0 && (xs[j - 1] `gt` xs[j]) do + (j - 1, swap j (j - 1) xs) + in xs' + +-- | Like `insertion_sort`, but sort based on key function. +def insertion_sort_by_key [n] 't 'k (key: t -> k) ((<=): k -> k -> bool) (xs: [n]t) : [n]t = + zip (map key xs) (iota n) + |> insertion_sort (\(x, _) (y, _) -> x <= y) + |> map (\(_, i) -> xs[i]) diff --git a/tests_property/lib/github.com/diku-dk/sorts/insertion_sort_tests.fut b/tests_property/lib/github.com/diku-dk/sorts/insertion_sort_tests.fut new file mode 100644 index 0000000000..713fea58f5 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/insertion_sort_tests.fut @@ -0,0 +1,48 @@ +-- | ignore + +import "insertion_sort" + +-- == +-- entry: sort_i32 +-- input { empty([0]i32) } +-- output { empty([0]i32) } +-- input { [5,4,3,2,1] } +-- output { [1,2,3,4,5] } +-- input { [5,4,3,3,2,1] } +-- output { [1,2,3,3,4,5] } + +entry sort_i32 (xs: []i32) = insertion_sort (i32.<=) xs + +-- == +-- entry: sort_u16 +-- input { [5u16,4u16,3u16,2u16,1u16] } +-- output { [1u16,2u16,3u16,4u16,5u16] } + +entry sort_u16 (xs: []u16) = insertion_sort (u16.<=) xs + +-- == +-- entry: sort_f32 +-- input { [5f32,4f32,3f32,2f32,1f32] } +-- output { [1f32,2f32,3f32,4f32,5f32] } + +entry sort_f32 (xs: []f32) = insertion_sort (f32.<=) xs + +-- == +-- entry: sort_perm_i32 +-- input { [5,4,3,2,1,0,-1,-2] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_i32 [n] (xs: [n]i32) = + zip xs (iota n) + |> insertion_sort_by_key (.0) (<=) + |> map ((.1) >-> i32.i64) + +-- == +-- entry: sort_perm_f32 +-- input { [5f32,4f32,3f32,2f32,1f32,0f32,-1f32,-2f32] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_f32 [n] (xs: [n]f32) = + zip xs (iota n) + |> insertion_sort_by_key (.0) (<=) + |> map ((.1) >-> i32.i64) diff --git a/tests_property/lib/github.com/diku-dk/sorts/merge_sort.fut b/tests_property/lib/github.com/diku-dk/sorts/merge_sort.fut new file mode 100644 index 0000000000..18f1d019f1 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/merge_sort.fut @@ -0,0 +1,256 @@ +-- | Work-efficient parallel mergesort +-- +-- Author: Sam Westrick . + +------------------------------------------------------------------------------ +-- Double binary search: +-- Split sorted sequences s and t into (s1, s2) and (t1, t2) such that the +-- largest items of s1 and t1 are smaller than the smallest items of s2 and t2. +-- The desired output size |s1|+|t1| is given as a parameter. +-- +-- Specifically, `split_count leq s t k` returns `(m, n)` where: +-- (s1, s2) = (s[:m], s[m:]) +-- (t1, t2) = (t[:n], t[n:]) +-- m+n = k +-- max(s1) <= min(t2) +-- max(t1) <= min(s2) +-- +-- Note that there are many possible solutions, so we also mandate that `m` +-- should be minimized. +-- +-- Work: O(log(|s|+|t|)) +-- Span: O(log(|s|+|t|)) + +local +def split_count 'a (leq: a -> a -> bool) (s: []a) (t: []a) k : (i64, i64) = + let normalize ((slo, shi), (tlo, thi), count) = + let slo_orig = slo + let tlo_orig = tlo + -- maybe count is small + let shi = i64.min shi (slo + count) + let thi = i64.min thi (tlo + count) + -- maybe count is large + let slack = (shi - slo) + (thi - tlo) - count + let slack = i64.min slack (shi - slo) + let slack = i64.min slack (thi - tlo) + let slo = i64.max slo (shi - slack) + let tlo = i64.max tlo (thi - slack) + let count = count - (slo - slo_orig) - (tlo - tlo_orig) + in ((slo, shi), (tlo, thi), count) + let step ((slo, shi), (tlo, thi), count) = + if shi - slo <= 0 + then ((slo, shi), (tlo + count, thi), 0) + else if thi - tlo <= 0 + then ((slo + count, shi), (tlo, thi), 0) + else if count == 1 + then if leq t[tlo] s[slo] + then ((slo, shi), (tlo + 1, thi), 0) + else ((slo + 1, shi), (tlo, thi), 0) + else let m = count / 2 + let n = count - m + -- |------|x|-------| + -- ^ ^ ^ + -- slo slo+m shi + -- + -- |------|y|-------| + -- ^ ^ ^ + -- tlo tlo+n thi + -- + + let leq_y_x = + n == 0 + || slo + m >= shi + || leq t[tlo + n - 1] s[slo + m] + in if leq_y_x + then ((slo, shi), (tlo + n, thi), count - n) + else ((slo, shi), (tlo, tlo + n), count) + let ((slo, _), (tlo, _), _) = + loop (ss, tt, count) = normalize ((0, length s), (0, length t), k) + while count > 0 do + normalize (step (ss, tt, count)) + in (slo, tlo) + +------------------------------------------------------------------------------ +-- `merge_sequential leq s t n` merges sorted sequences `s` and `t` with the +-- simple sequential algorithm, and outputs the first `n` elements. +-- +-- (Passing `n` is convenient for making the type checker confident that +-- the output is exactly size `n`.) +-- +-- Requires `s` and `t` already sorted by `leq` + +local +def merge_sequential 'a (leq: a -> a -> bool) (s: []a) (t: []a) n : *[n]a = + let dummy = if length s > 0 then head s else head t + let (_, data) = + loop (i, data) = (0, replicate n dummy) + for k < n do + let j = k - i + let (i, x) = + if j == length t || (i < length s && leq s[i] t[j]) + then (i + 1, s[i]) + else (i, t[j]) + in (i, data with [k] = x) + in data + +------------------------------------------------------------------------------ +-- `merge_adjacent leq s mid block_size` merges s[:mid] with s[mid:] +-- Requires s[:mid] and s[mid:] both individually already sorted +-- Requires n = mid+mid +-- Requires n divisible by block_size +-- +-- High-level idea is: +-- 1. Conceptually divide the **output** into blocks. +-- 2. Use `split_count` to compute, for each block starting offset i +-- (i.e., where i in {0, block_size, 2*block_size, ...}), use +-- `split_count` to count how many elements from s and t will come +-- before offset i in the output. These counts are called `splitters` +-- in the code. +-- 3. Compute the output blocks in parallel. For each block, we sequentially +-- merge one block. +-- +-- Technically, for work-efficiency, block_size should be Omega(log n), +-- because `split_count` has approx O(log n) cost, and we do n/block_size +-- calls to `split_count`. +-- +-- In other words, we should be careful to pick a block_size that is +-- **not too small**. In practice, however, it's difficult to screw this up, +-- because for feasible values of `n`, we can assume `log n` is effectively +-- constant. block_size = 8 seems to work well. +-- +-- Work: O(n) +-- Span: O(block_size + log n) + +local +def merge_adjacent 'a [n] (leq: a -> a -> bool) (s: [n]a) mid block_size : *[n]a = + if n < 10 + then merge_sequential leq s[:mid] s[mid:] n + else let num_blocks = assert (n % block_size == 0) (n / block_size) + let splitters = + tabulate (1 + num_blocks) (\i -> split_count leq s[:mid] s[mid:] (i * block_size)) + let block b: [block_size]a = + let (slo, tlo) = splitters[b] + let (shi, thi) = splitters[b + 1] + in merge_sequential leq s[slo:shi] s[mid + tlo:mid + thi] block_size + in take n (flatten (tabulate num_blocks block)) + +------------------------------------------------------------------------------ +-- `small_insertion_sort leq s` is faster than merge sort for very small +-- sequences (e.g., |s| <= 20) + +local +def small_insertion_sort 't [n] (leq: t -> t -> bool) (s: *[n]t) : *[n]t = + if n <= 1 + then s + else let gt x y = !(leq x y) + in loop s for i in 0...(n - 2) do + let (s, _) = + loop (s, j) = (s, i) + while j >= 0 && gt s[j] s[j + 1] do + let tmp = copy s[j] + let s = s with [j] = copy s[j + 1] + let s = s with [j + 1] = tmp + in (s, j - 1) + in s + +----------------------------------------------------------------------------- +-- a couple utilities + +local +def smallest_pow_2_geq_than k = + loop (x: i64) = 1 while x < k do 2 * x + +local +def greatest_divisor_leq_than upper_bound n = + -- find smallest d such that d|n and n/d <= upper_bound + let upper_bound = assert (upper_bound >= 1) upper_bound + let d = loop (d: i64) = 1 while n / d > upper_bound || n % d != 0 do d + 1 + in n / d + +-- | Work-efficient parallel mergesort: +-- `merge_sort_with_params {max_block_size, max_merge_block_size} leq s` +-- +-- Any values for {max_block_size, max_merge_block_size} are +-- acceptable, but do heavily impact performance. See +-- `merge_sort`@term below for reasonable choices that seem to work +-- well in practice. +def merge_sort_with_params [n] 't {max_block_size, max_merge_block_size} (leq: t -> t -> bool) (s: [n]t) : [n]t = + -- High-level idea is: + -- 1. Divide the input into many small blocks (of size at most max_block_size) + -- 2. Sort all the small blocks in parallel (using small_insertion_sort) + -- 3. Merge the blocks upwards (classic loopification of mergesort) + -- + -- The tricky thing is that, to make the last step most efficient, we want a + -- exactly a power-of-two number of blocks. + -- + -- We could of course just pad everything to the nearest power-of-two size, but + -- this risks incurring a ~2x work overhead in the worst case, which probably + -- will result in 2x slowdown in practice for large sequences + -- + -- So instead, we try to maximize block_size and minimize num_blocks subject to + -- the following inequalities, which guarantees that we need approximately at + -- most n/max_block_size padding in the worst case. + -- block_size <= max_block_size + -- block_size * 2^num_blocks >= n + -- + -- Finally, a small technical issue is that, when we merge, we also need to + -- select a block size for merge to use internally. We call this + -- `merge_block_size`, and similarly put a bound on it with + -- `max_merge_block_size`. We need `merge_block_size` to be a divisor of + -- every 2^i * block_size for i >= 1. So, we pick the greatest divisor of + -- 2*block_size that satisfies merge_block_size <= max_merge_block_size. + if length s <= 1 + then s + else let max_block_size = i64.max 1 max_block_size + let max_merge_block_size = i64.max 1 max_merge_block_size + let min_num_blocks = 1 + (n - 1) / max_block_size + let num_blocks = smallest_pow_2_geq_than min_num_blocks + let block_size = 1 + (n - 1) / num_blocks + let padded_n = block_size * num_blocks + let merge_block_size = + greatest_divisor_leq_than max_merge_block_size (2 * block_size) + let max_elem = reduce (\a b -> if leq a b then b else a) s[0] s + let sorted_blocks = + flatten (tabulate num_blocks (\i -> + let block = + tabulate block_size (\j -> + let k = i * block_size + j + in if k < n then s[k] else max_elem) + in small_insertion_sort leq block)) + let (data, _) = + loop (data, stride) = (sorted_blocks, block_size) + while stride < padded_n do + let next_stride = 2 * stride + let num_merges = padded_n / next_stride + let data = + flatten (tabulate num_merges (\mi -> + let start = mi * next_stride + let piece = take next_stride (drop start data) + in merge_adjacent leq piece stride merge_block_size)) + in (data, next_stride) + in take n data + +----------------------------------------------------------------------------- + +-- | Implements `merge_sort leq s` with reasonable default parameters. Here +-- `leq` is a less-than-or-equal comparison function on elements of type `t`, +-- and `s` is an array of `n` elements of type `t`. The default parameters are +-- max_block_size = 20 and max_merge_block_size = 8. +-- +-- Work: **O(n log n)** +-- +-- Span: **O(log**2 n)** +def merge_sort [n] 't (leq: t -> t -> bool) (s: [n]t) : [n]t = + -- Note: this selection of parameters seems to work well in practice, but + -- could be investigated more carefully. + merge_sort_with_params {max_block_size = 20, max_merge_block_size = 8} leq s + +def merge_sort_by_key [n] 't 'k (key: t -> k) (leq: k -> k -> bool) (s: [n]t) : [n]t = + zip (map key s) (iota n) + |> merge_sort (\(x, _) (y, _) -> leq x y) + |> map (\(_, i) -> s[i]) + +def merge_sort_with_params_by_key [n] 't 'k params (key: t -> k) (leq: k -> k -> bool) (s: [n]t) : [n]t = + zip (map key s) (iota n) + |> merge_sort_with_params params (\(x, _) (y, _) -> leq x y) + |> map (\(_, i) -> s[i]) diff --git a/tests_property/lib/github.com/diku-dk/sorts/merge_sort_tests.fut b/tests_property/lib/github.com/diku-dk/sorts/merge_sort_tests.fut new file mode 100644 index 0000000000..cc48761178 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/merge_sort_tests.fut @@ -0,0 +1,55 @@ +-- | ignore + +import "merge_sort" + +-- picking small block sizes should stress all codepaths within +-- merge_sort, even on small inputs +def params = {max_block_size = 2i64, max_merge_block_size = 2i64} + +-- == +-- entry: sort_i32 +-- input { empty([0]i32) } +-- output { empty([0]i32) } +-- input { [5,4,3,2,1] } +-- output { [1,2,3,4,5] } +-- input { [5,4,3,3,2,1] } +-- output { [1,2,3,3,4,5] } + +entry sort_i32 (xs: []i32) = + merge_sort_with_params params (i32.<=) xs + +-- == +-- entry: sort_u16 +-- input { [5u16,4u16,3u16,2u16,1u16] } +-- output { [1u16,2u16,3u16,4u16,5u16] } + +entry sort_u16 (xs: []u16) = + merge_sort_with_params params (u16.<=) xs + +-- == +-- entry: sort_f32 +-- input { [5f32,4f32,3f32,2f32,1f32] } +-- output { [1f32,2f32,3f32,4f32,5f32] } + +entry sort_f32 (xs: []f32) = + merge_sort_with_params params (f32.<=) xs + +-- == +-- entry: sort_perm_i32 +-- input { [5,4,3,2,1,0,-1,-2] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_i32 [n] (xs: [n]i32) = + zip xs (iota n) + |> merge_sort_with_params_by_key params (.0) (<=) + |> map ((.1) >-> i32.i64) + +-- == +-- entry: sort_perm_f32 +-- input { [5f32,4f32,3f32,2f32,1f32,0f32,-1f32,-2f32] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_f32 [n] (xs: [n]f32) = + zip xs (iota n) + |> merge_sort_with_params_by_key params (.0) (<=) + |> map ((.1) >-> i32.i64) diff --git a/tests_property/lib/github.com/diku-dk/sorts/quick_sort.fut b/tests_property/lib/github.com/diku-dk/sorts/quick_sort.fut new file mode 100644 index 0000000000..ce39444db7 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/quick_sort.fut @@ -0,0 +1,108 @@ +-- | Data-parallel implementation of quicksort. Note that this +-- quicksort, while parallel, is quite slow. In almost all cases you +-- should use radix- or merge sort instead. + +local import "../segmented/segmented" + +local +def segmented_replicate [n] 't (reps: [n]i64) (vs: [n]t) : []t = + let idxs = replicated_iota reps + in map (\i -> vs[i]) idxs + +local +def info 't ((<=): t -> t -> bool) (x: t) (y: t) : i64 = + if x <= y + then if y <= x then 0 else -1 + else 1 + +local +def tripit (x: i64) : (i64, i64, i64) = + if x < 0 + then (1, 0, 0) + else if x > 0 then (0, 0, 1) else (0, 1, 0) + +local +def tripadd (a1: i64, e1: i64, b1: i64) (a2, e2, b2) = + (a1 + a2, e1 + e2, b1 + b2) + +local type sgm = {start: i64, sz: i64} + +-- segment + +local +def step [n] [k] 't ((<=): t -> t -> bool) (xs: *[n]t) (sgms: [k]sgm) : (*[n]t, []sgm) = + --let _ = trace {NEW_STEP=()} + + -- find a pivot for each segment + let pivots: []t = map (\sgm -> xs[sgm.start + sgm.sz / 2]) sgms + let sgms_szs: []i64 = map (\sgm -> sgm.sz) sgms + let [m] (idxs: [m]i64) = replicated_iota sgms_szs + -- find the indexes into values in segments; after a value equal to + -- a pivot has moved, it will no longer be part of a segment (it + -- need not be moved again). + let is = + let is1 = + segmented_replicate sgms_szs (map (\x -> x.start) sgms) + :> [m]i64 + let fs = map2 (!=) is1 (rotate (-1) is1) + let is2 = segmented_iota fs + in map2 (+) is1 is2 + -- for each such value, how does it compare to the pivot associated + -- with the segment? + let infos: []i64 = + map2 (\idx i -> info (<=) xs[i] pivots[idx]) + idxs + is + let orders: [](i64, i64, i64) = map tripit infos + -- compute segment descriptor + let flags = + map3 (\i j k -> i == 0 || j != k) (indices idxs) idxs (rotate (-1) idxs) + -- compute partition sizes for each segment + let pszs = segmented_reduce tripadd (0, 0, 0) flags orders :> [k](i64, i64, i64) + -- compute the new segments + let sgms' = + map2 (\(sgm: sgm) (a, e, b) -> + [ {start = sgm.start, sz = a} + , {start = sgm.start + a + e, sz = b} + ]) + sgms + pszs + |> flatten + |> filter (\sgm -> sgm.sz > 1) + -- compute the new positions of the values in the present segments + let newpos: []i64 = + let where: [](i64, i64, i64) = segmented_scan tripadd (0, 0, 0) flags orders + in map3 (\i (a, e, b) info -> + let (x, y, _) = pszs[i] + let s = sgms[i].start + in if info < 0 + then s + a - 1 + else if info > 0 + then s + b - 1 + x + y + else s + e - 1 + x) + idxs + where + infos + let vs = map (\i -> xs[i]) is + let xs' = scatter xs newpos vs + in (xs', sgms') + +-- | Quicksort. Given a comparison function (<=) and an array of +-- elements, `qsort (<=) xs` returns an array with the elements in +-- `xs` sorted according to `<=`. The algorithm has best case work +-- complexity *O(n)* (when all elements are identical), worst case +-- work complexity *O(n^2)*, and an average case work complexity of +-- *O(n log n)*. It has best depth complexity *O(1)*, worst depth +-- complexity *O(n)* and average depth complexity *O(log n)*. +def qsort [n] 't ((<=): t -> t -> bool) (xs: [n]t) : [n]t = + if n < 2 + then xs + else (loop (xs, mms) = (copy xs, [{start = 0, sz = n}]) + while length mms > 0 do + step (<=) xs mms).0 + +-- | Like `qsort`@term, but sort based on key function. +def qsort_by_key [n] 't 'k (key: t -> k) ((<=): k -> k -> bool) (xs: [n]t) : [n]t = + zip (map key xs) (iota n) + |> qsort (\(x, _) (y, _) -> x <= y) + |> map (\(_, i) -> xs[i]) diff --git a/tests_property/lib/github.com/diku-dk/sorts/quick_sort_test.fut b/tests_property/lib/github.com/diku-dk/sorts/quick_sort_test.fut new file mode 100644 index 0000000000..4b8ccce0f4 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/quick_sort_test.fut @@ -0,0 +1,48 @@ +-- | ignore + +import "quick_sort" + +-- == +-- entry: sort_i32 +-- input { empty([0]i32) } +-- output { empty([0]i32) } +-- input { [5,4,3,2,1] } +-- output { [1,2,3,4,5] } +-- input { [5,4,3,3,2,1] } +-- output { [1,2,3,3,4,5] } + +entry sort_i32 (xs: []i32) = qsort (i32.<=) xs + +-- == +-- entry: sort_u16 +-- input { [5u16,4u16,3u16,2u16,1u16] } +-- output { [1u16,2u16,3u16,4u16,5u16] } + +entry sort_u16 (xs: []u16) = qsort (u16.<=) xs + +-- == +-- entry: sort_f32 +-- input { [5f32,4f32,3f32,2f32,1f32] } +-- output { [1f32,2f32,3f32,4f32,5f32] } + +entry sort_f32 (xs: []f32) = qsort (f32.<=) xs + +-- == +-- entry: sort_perm_i32 +-- input { [5,4,3,2,1,0,-1,-2] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_i32 [n] (xs: [n]i32) = + zip xs (iota n) + |> qsort_by_key (.0) (<=) + |> map ((.1) >-> i32.i64) + +-- == +-- entry: sort_perm_f32 +-- input { [5f32,4f32,3f32,2f32,1f32,0f32,-1f32,-2f32] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_f32 [n] (xs: [n]f32) = + zip xs (iota n) + |> qsort_by_key (.0) (<=) + |> map ((.1) >-> i32.i64) diff --git a/tests_property/lib/github.com/diku-dk/sorts/radix_sort.fut b/tests_property/lib/github.com/diku-dk/sorts/radix_sort.fut new file mode 100644 index 0000000000..e4a64727f8 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/radix_sort.fut @@ -0,0 +1,142 @@ +-- | A non-comparison-based sort that sorts an array in *O(k n)* work +-- and *O(k log(n))* span, where *k* is the number of bits in each element. +-- +-- Generally, this is the sorting function we recommend for Futhark +-- programs, but be careful about negative integers (use +-- `radix_sort_int`@term) and floating-point numbers (use +-- `radix_sort_float`@term). If you need a comparison-based sort, +-- consider `merge_sort`@term@"merge_sort". +-- +-- ## See Also +-- +-- * `merge_sort`@term@"merge_sort" + +local +def radix_sort_step [n] 't + (xs: [n]t) + (get_bit: i32 -> t -> i32) + (digit_n: i32) : [n]t = + let num x = i8.i32 <| get_bit (digit_n + 1) x * 2 + get_bit digit_n x + let pairwise op (a1, b1, c1, d1) (a2, b2, c2, d2) = (a1 `op` a2, b1 `op` b2, c1 `op` c2, d1 `op` d2) + let pairwise' op (a1, b1, c1) (a2, b2, c2) = (a1 `op` a2, b1 `op` b2, c1 `op` c2) + let bins = map num xs + let flags = + bins + |> map (\x -> (x == 0, x == 1, x == 2, x == 3)) + let flags' = + map num xs + |> map (\x -> + ( i64.bool (x == 0) + , i64.bool (x == 1) + , i64.bool (x == 2) + )) + let offsets = + flags + |> map (\(a, b, c, d) -> (i64.bool a, i64.bool b, i64.bool c, i64.bool d)) + |> scan (pairwise (+)) (0, 0, 0, 0) + let (na, nb, nc) = reduce_comm (pairwise' (+)) (0, 0, 0) flags' + let f bin (a, b, c, d) = + (-1) + + a * (i64.bool (bin == 0)) + + na * (i64.bool (bin > 0)) + + b * (i64.bool (bin == 1)) + + nb * (i64.bool (bin > 1)) + + c * (i64.bool (bin == 2)) + + nc * (i64.bool (bin > 2)) + + d * (i64.bool (bin == 3)) + let is = map2 f bins offsets + in scatter (#[scratch] copy xs) is xs + +-- | The `num_bits` and `get_bit` arguments can be taken from one of +-- the numeric modules of module type `integral`@mtype@"/prelude/math" +-- or `float`@mtype@"/prelude/math", such as `i32`@term@"/prelude/math" +-- or `f64`@term@"/prelude/math". However, if you know that +-- the input array only uses lower-order bits (say, if all integers +-- are less than 100), then you can profitably pass a smaller +-- `num_bits` value to reduce the number of sequential iterations. +-- +-- **Warning:** while radix sort can be used with numbers, the bitwise +-- representation of of both integers and floats means that negative +-- numbers are sorted as *greater* than non-negative. Negative floats +-- are further sorted according to their absolute value. For example, +-- radix-sorting `[-2.0, -1.0, 0.0, 1.0, 2.0]` will produce `[0.0, +-- 1.0, 2.0, -1.0, -2.0]`. Use `radix_sort_int`@term and +-- `radix_sort_float`@term in the (likely) cases that this is not what +-- you want. +def radix_sort [n] 't + (num_bits: i32) + (get_bit: i32 -> t -> i32) + (xs: [n]t) : [n]t = + let iters = if n == 0 then 0 else (num_bits + 2 - 1) / 2 + in loop xs for i < iters do radix_sort_step xs get_bit (i * 2) + +def with_indices [n] 'a (xs: [n]a) : [n](a, i64) = + zip xs (iota n) + +local +def by_key_wrapper [n] 't sorter key num_bits get_bit (xs: [n]t) : [n]t = + map key xs + |> with_indices + |> sorter num_bits (\i (k, _) -> get_bit i k) + |> map (\(_, i: i64) -> xs[i]) + +-- OK because '0<=i k) + (num_bits: i32) + (get_bit: i32 -> k -> i32) + (xs: [n]t) : [n]t = + by_key_wrapper radix_sort key num_bits get_bit xs + +-- | A thin wrapper around `radix_sort`@term that ensures negative +-- integers are sorted as expected. Simply pass the usual `num_bits` +-- and `get_bit` definitions from e.g. `i32`@term@"/prelude/math". +def radix_sort_int [n] 't + (num_bits: i32) + (get_bit: i32 -> t -> i32) + (xs: [n]t) : [n]t = + let get_bit' i x = + -- Flip the most significant bit. + let b = get_bit i x + in if i == num_bits - 1 then b ^ 1 else b + in radix_sort num_bits get_bit' xs + +-- | Like `radix_sort_int`, but sort based on key function. +def radix_sort_int_by_key [n] 't 'k + (key: t -> k) + (num_bits: i32) + (get_bit: i32 -> k -> i32) + (xs: [n]t) : [n]t = + by_key_wrapper radix_sort_int key num_bits get_bit xs + +-- | A thin wrapper around `radix_sort`@term that ensures floats are +-- sorted as expected. Simply pass the usual `num_bits` and `get_bit` +-- definitions from `f32`@term@"/prelude/math" and +-- `f64`@term@"/prelude/math". +def radix_sort_float [n] 't + (num_bits: i32) + (get_bit: i32 -> t -> i32) + (xs: [n]t) : [n]t = + let get_bit' i x = + -- We flip the bit returned if: + -- + -- 0) the most significant bit is set (this makes more negative + -- numbers sort before less negative numbers), or + -- + -- 1) we are asked for the most significant bit (this makes + -- negative numbers sort before positive numbers). + let b = get_bit i x + in if get_bit (num_bits - 1) x == 1 || i == num_bits - 1 + then b ^ 1 + else b + in radix_sort num_bits get_bit' xs + +-- | Like `radix_sort_float`, but sort based on key function. +def radix_sort_float_by_key [n] 't 'k + (key: t -> k) + (num_bits: i32) + (get_bit: i32 -> k -> i32) + (xs: [n]t) : [n]t = + by_key_wrapper radix_sort_float key num_bits get_bit xs diff --git a/tests_property/lib/github.com/diku-dk/sorts/radix_sort_tests.fut b/tests_property/lib/github.com/diku-dk/sorts/radix_sort_tests.fut new file mode 100644 index 0000000000..3771247a18 --- /dev/null +++ b/tests_property/lib/github.com/diku-dk/sorts/radix_sort_tests.fut @@ -0,0 +1,74 @@ +-- | ignore + +import "radix_sort" + +-- == +-- entry: sort_i32 +-- input { [5,4,3,2,1,0,-1,-2] } +-- output { [-2,-1,0,1,2,3,4,5] } +-- input { [5,4,3,3,2,1,0,-1,-2,-1] } +-- output { [-2,-1,-1,0,1,2,3,3,4,5] } + +entry sort_i32 = radix_sort_int i32.num_bits i32.get_bit + +-- == +-- entry: sort_u16 +-- input { [5u16,4u16,3u16,2u16,1u16,-1u16] } +-- output { [-1u16,1u16,2u16,3u16,4u16,5u16] } + +entry sort_u16 = radix_sort_int u16.num_bits u16.get_bit + +-- == +-- entry: sort_f32 +-- input { [5f32,4f32,3f32,2f32,-1f32,-2f32] } +-- output { [-2f32,-1f32,2f32,3f32,4f32,5f32] } + +entry sort_f32 = radix_sort_float f32.num_bits f32.get_bit + +-- == +-- entry: sort_perm_i32 +-- input { [5,4,3,2,1,0,-1,-2] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_i32 [n] (xs: [n]i32) = + zip xs (iota n) + |> radix_sort_int_by_key (.0) i32.num_bits i32.get_bit + |> map ((.1) >-> i32.i64) + +-- == +-- entry: sort_perm_f32 +-- input { [5f32,4f32,3f32,2f32,1f32,0f32,-1f32,-2f32] } +-- output { [7, 6, 5, 4, 3, 2, 1, 0] } + +entry sort_perm_f32 [n] (xs: [n]f32) = + zip xs (iota n) + |> radix_sort_float_by_key (.0) f32.num_bits f32.get_bit + |> map ((.1) >-> i32.i64) + +-- == +-- entry: is_sorted +-- random input { [10][50]u64 } +-- output { true } + +entry is_sorted [n] (arrs: [][n]u64) : bool = + all (\arr -> + let result = radix_sort u64.num_bits u64.get_bit arr + in tabulate n (\i -> i == 0 || result[i - 1] <= result[i]) + |> and) + arrs + +-- == +-- entry: is_stable +-- random input { [10][50]u8 } +-- output { true } + +entry is_stable [n] (arrs: [][n]u8) : bool = + all (\arr -> + let (keys, idx) = + map (% 5) arr + |> flip zip (iota n) + |> radix_sort_by_key (.0) u8.num_bits u8.get_bit + |> unzip + in tabulate n (\i -> i == 0 || keys[i - 1] != keys[i] || idx[i - 1] < idx[i]) + |> and) + arrs diff --git a/tests_property/libraries/shrinkers/integerShrinker.fut b/tests_property/libraries/shrinkers/integerShrinker.fut new file mode 100644 index 0000000000..12c6616742 --- /dev/null +++ b/tests_property/libraries/shrinkers/integerShrinker.fut @@ -0,0 +1,14 @@ +module integerlShrinkers (I: integral) = { + type t = I.t + + def shrinker (x: t) (random: i32): t = + let tactic = random % 2 + in if tactic == 0 then + -- Use the division function from the module I + I.(x / i32 2) + else + if I.(x >= i32 0) then + I.(x - i32 1) + else + I.(x + i32 1) +} diff --git a/tests_property/libraries/toString/toString.fut b/tests_property/libraries/toString/toString.fut new file mode 100644 index 0000000000..9c534c9fcc --- /dev/null +++ b/tests_property/libraries/toString/toString.fut @@ -0,0 +1,62 @@ +def digit_to_u8 (d: u64) : u8 = + '0' + u8.u64 d + +def pos_u64_to_string (x: u64) : []u8 = + if x == 0u64 then + "0" + else + let (_, acc) = + loop (n, acc) = (x, "") + while n > 0u64 do + let digit = n % 10u64 + let ch = digit_to_u8 digit + in (n / 10u64, [ch] ++ acc) + in acc + +-- Unsigned integers. + +def u8_to_string (x: u8) : []u8 = + pos_u64_to_string (u64.u8 x) + +def u16_to_string (x: u16) : []u8 = + pos_u64_to_string (u64.u16 x) + +def u32_to_string (x: u32) : []u8 = + pos_u64_to_string (u64.u32 x) + +def u64_to_string (x: u64) : []u8 = + pos_u64_to_string x + +-- Signed integers. + +def i8_to_string (x: i8) : []u8 = + if x >= 0i8 then + pos_u64_to_string (u64.i8 x) + else if x == -128i8 then + "-128" + else + "-" ++ pos_u64_to_string (u64.i8 (-x)) + +def i16_to_string (x: i16) : []u8 = + if x >= 0i16 then + pos_u64_to_string (u64.i16 x) + else if x == -32768i16 then + "-32768" + else + "-" ++ pos_u64_to_string (u64.i16 (-x)) + +def i32_to_string (x: i32) : []u8 = + if x >= 0i32 then + pos_u64_to_string (u64.i32 x) + else if x == -2147483648i32 then + "-2147483648" + else + "-" ++ pos_u64_to_string (u64.i32 (-x)) + +def i64_to_string (x: i64) : []u8 = + if x >= 0i64 then + pos_u64_to_string (u64.i64 x) + else if x == -9223372036854775808i64 then + "-9223372036854775808" + else + "-" ++ pos_u64_to_string (u64.i64 (-x)) \ No newline at end of file diff --git a/tests_property/test.sh b/tests_property/test.sh new file mode 100644 index 0000000000..7c82d11813 --- /dev/null +++ b/tests_property/test.sh @@ -0,0 +1,92 @@ +#!/bin/sh +set -u + +FUTHARK_BIN=futhark +TEST_DIR=. + +run_test() { + test_file="$1" + futhark_cmd="$2" + seed_flag="" + + base_name=$(basename "$test_file") + + # Special cases where output varies due to randomness. + # Use specific seeds for these tests to ensure deterministic output. + case "$base_name" in + "i8AutoShrink.fut" | "i32NoShrink.fut") + seed_flag="--seed=-1161324613" + ;; + "f64.fut") + seed_flag="--seed=-540792207" + ;; + Record* | Tuple* | "Stepping.fut") + seed_flag="--seed=-2070821161" + ;; + ArrayRecord* | "Arrayi32(2).fut") + seed_flag="--seed=976321339" + ;; + "reverse.fut") + seed_flag="--seed=885903244" + ;; + esac + + test_file_full_path="$TEST_DIR/${test_file#./}" + + expected="${test_file%.fut}.out" + actual="${test_file%.fut}.out_actual" + + ($futhark_cmd test $seed_flag "$test_file_full_path") 2>&1 | \ + grep -vE "Compiling with|Running compiled|Running .*/|^$TEST_DIR/|[0-9]+ failed|[0-9]+ passed|[0-9]+/[0-9]+ passed" | \ + sed -E -e 's/seed=-?[0-9]+/seed=REDACTED/g' \ + -e 's/after [0-9]+ tests/after N tests/g' \ + > "$actual" + + if diff -u "$expected" "$actual" > /dev/null; then + echo "✅ PASS: $test_file_full_path" + rm -f "$actual" + return 0 + else + echo "❌ FAIL: $test_file_full_path" + echo "--- Difference (-expected, +actual) ---" + diff -u "$expected" "$actual" + return 1 + fi +} + +if [ "${1:-}" = "--worker" ]; then + run_test "$3" "$2" + exit $? +fi + +echo "Starting Property Tests..." + +# 1. Find all .fut files +ALL_TESTS=$(find "." -type d \( -name "lib" -o -name "libraries" \) -prune -o -name "*.fut" -print) + +# 2. Filter to only those with a matching .out file +TESTS=$(echo "$ALL_TESTS" | while read -r test; do + if [ -f "${test%.fut}.out" ]; then + echo "$test" + fi +done) + +# 3. Get the accurate count of tests that will ACTUALLY run +NUMTESTS=$(echo "$TESTS" | grep -c .) + +if [ -z "$TESTS" ]; then + echo "No tests found." + exit 0 +fi + +CORES=$(nproc||echo 4) +echo "$TESTS" | xargs -I {} -P "$CORES" sh "$0" "--worker" "$FUTHARK_BIN" "{}" + +# Final status check +if [ $? -ne 0 ]; then + printf "\nSome tests failed out of the $NUMTESTS tests.\n" + exit 1 +else + printf "\nAll $NUMTESTS tests passed!\n" + exit 0 +fi