diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,26 @@ The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/) and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html). +## [0.26.3] + +### Added + +* `futhark test` now suppports property-based testing (like QuickCheck). Work by + Matin Nafar and Simon August Mørk. + +### Fixed + +* `futhark bench`: entry points that consumed their input produced misleading + profiling information. (#2464) + +* Sometimes arrays returned from entry points would be unnecessarily copied if + the compiler could not be sure statically that they were in row-major layout. + +* The type checker would fail to reject entry points that accepted lifted + abstract types. (#2467) + +* An issue in the interpreter's handling of local opens. + ## [0.26.2] ### Added diff --git a/docs/js-api.rst b/docs/js-api.rst --- a/docs/js-api.rst +++ b/docs/js-api.rst @@ -9,7 +9,7 @@ those wrappers. The exact generated files and the top-level JavaScript interface differ -somewhat between the WASM-style backends and the WebGPU backend, so the +somewhat between the WASM backend and the WebGPU backend, so the relevant differences are described below. First a warning: **the JavaScript API is experimental**. It may @@ -40,16 +40,33 @@ The exact file set is backend-dependent and may change over time. -The module exports a function, ``newFutharkContext``, which is a factory -function that returns a Promise producing a ``FutharkContext`` -instance (see below). A simple usage example: +The generated JavaScript wrapper exposes a ``FutharkModule`` class, +which is the preferred top-level interface for using a compiled Futhark +program from JavaScript. The module is initialised with the generated +backend runtime module. +The initialisation pattern is the same for the WASM-style backend and +the WebGPU backend. The only difference is how ``Module`` is made available. +For the WASM-style backend, the generated ``.mjs`` file exports it as the +default export, so it is imported together with ``FutharkModule``: + .. code-block:: javascript - import { newFutharkContext } from './futlib.mjs'; - var fc; - newFutharkContext().then(x => fc = x); + import Module, { FutharkModule } from './futlib.mjs'; + const module = await Module(); + + const fut = new FutharkModule(); + await fut.init(module); + +For the WebGPU backend, the generated runtime module is usually loaded +before the application code, for example: + +.. code-block:: html + + + + General concerns ---------------- @@ -61,50 +78,45 @@ Top-level wrapper objects ------------------------- -The top-level JavaScript interface differs between backends. - -WASM wrapper -~~~~~~~~~~~~ - -The WASM backend exports a ``newFutharkContext()`` factory function that -asynchronously constructs a ``FutharkContext``. - -.. js:function:: newFutharkContext() - - Asynchronously create a new ``FutharkContext`` object. +The preferred top-level JavaScript interface is ``FutharkModule``. A +``FutharkModule`` object represents an instance of a compiled Futhark +program. It owns the underlying Futhark context and is used to construct +arrays, call entry points, and free resources. -.. js:class:: FutharkContext() +.. js:class:: FutharkModule() A bookkeeping class representing an instance of a compiled Futhark program. -.. js:function:: FutharkContext.free() +.. js:function:: FutharkModule.init(module) - Frees all memory created by the ``FutharkContext`` object. It is an - error to use a ``FutharkArray`` or ``FutharkOpaque`` after the - ``FutharkContext`` on which they were defined has been freed. + Asynchronously initialise the ``FutharkModule`` object. -WebGPU wrapper -~~~~~~~~~~~~~~ + For the WASM-style backend, the ``module`` argument is optional. If + omitted, the generated wrapper loads the WebAssembly module itself. -The WebGPU backend generates a ``FutharkModule`` wrapper class. This -wrapper is initialised with the generated backend runtime module. + For the WebGPU backend, ``module`` must be the generated backend + runtime module. -.. js:class:: FutharkModule() +.. js:function:: FutharkModule.free() - A bookkeeping class representing an instance of a compiled Futhark - program. + Frees the Futhark context and configuration associated with the + module. It is an error to use a ``FutharkArray`` or ``FutharkOpaque`` + after the ``FutharkModule`` on which it was created has been freed. -.. js:function:: FutharkModule.init(module) +.. js:attribute:: FutharkModule.entry - Asynchronously initialise the ``FutharkModule`` object with the - generated backend runtime module. + Object containing the generated entry point functions. For example, + an entry point named ``main`` is available as ``fut.entry.main``. -.. js:function:: FutharkModule.free() +.. js:attribute:: FutharkModule.types - Frees the Futhark context and configuration associated with the - module. + Object containing generated type information and array constructor + objects for the array types used by the program. +The backends also provides utility methods for synchronisation, +cache management, and profiling. + .. js:function:: FutharkModule.context_sync() Wait for pending backend work associated with the context to finish. @@ -125,6 +137,25 @@ Resume profiling. +WASM compatibility interface +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The WASM-style backend also keep the older ``FutharkContext`` interface +for backwards compatibility. + +.. js:function:: newFutharkContext() + + Asynchronously create a new ``FutharkContext`` object. + +.. js:class:: FutharkContext() + + Backwards-compatible wrapper class for WASM-style backend. + ``FutharkContext`` supports the same main interface as + ``FutharkModule``, including ``entry``, ``types``, array constructors, + and ``free``. + +New code should prefer ``FutharkModule``. + Values ------ @@ -138,34 +169,11 @@ FutharkArray ------------ -The exact ``FutharkArray`` API differs slightly between backends. - -WASM wrapper -~~~~~~~~~~~~ - -.. js:function:: FutharkArray.toArray() - - Returns a nested JavaScript array. - -.. js:function:: FutharkArray.toTypedArray() - - Returns a flat typed array of the underlying data. +Arrays are represented by ``FutharkArray`` objects. The common array API is +shared by the WASM backend and the WebGPU backend. .. js:function:: FutharkArray.shape() - Returns the shape of the ``FutharkArray`` as an array of ``BigInt`` values. - -.. js:function:: FutharkArray.free() - - Frees the memory used by the ``FutharkArray``. - -WebGPU wrapper -~~~~~~~~~~~~~~ - -The WebGPU backend generates per-type subclasses of ``FutharkArray``. - -.. js:function:: FutharkArray.get_shape() - Returns the shape of the array as a ``BigInt64Array``. .. js:function:: FutharkArray.values() @@ -176,32 +184,41 @@ Frees the memory used by the ``FutharkArray``. -Array construction also differs a bit between backends. +The WASM backend also provides a few older convenience methods. -For the WASM wrapper, ``FutharkContext`` contains constructor methods for -each array type that appears in an entry point. For example, for the -type ``[]i32``: +.. js:function:: FutharkArray.toArray() -.. js:function:: FutharkContext.new_i32_1d_from_jsarray(jsarray) + Returns a nested JavaScript array. - Creates and returns a one-dimensional ``i32`` ``FutharkArray`` - representing the JavaScript array ``jsarray``. +.. js:function:: FutharkArray.toTypedArray() -.. js:function:: FutharkContext.new_i32_1d(array, dim0) + Returns a flat typed array of the underlying data. - Creates and returns a one-dimensional ``i32`` ``FutharkArray`` - representing the typed array ``array``, with shape ``dim0``. +.. js:function:: FutharkArray.shape() -For the WebGPU wrapper, each generated array type is represented by its -own generated class, available through the ``FutharkModule`` object. + Returns the shape of the ``FutharkArray`` as an array of ``BigInt`` values. +Array construction +~~~~~~~~~~~~~~~~~~ + +Each array type used by an entry point is exposed through a generated +constructor object. For example, for the type ``[]i32``: + .. js:function:: fut.i32_1d.from_data(data, dim0) Creates and returns a one-dimensional ``i32`` ``FutharkArray`` from a JavaScript ``Array`` or the corresponding typed array, with the given shape. +For the WASM backend, the generated constructor object also +provides a convenience method for nested JavaScript arrays. +.. js:function:: fut.i32_1d.from_jsarray(jsarray) + + Creates and returns a one-dimensional ``i32`` ``FutharkArray`` from + a JavaScript array. For higher-dimensional arrays, the JavaScript + array is expected to be nested according to the array rank. + FutharkOpaque ------------- @@ -219,11 +236,18 @@ Entry Points ------------ -Each entry point in the compiled futhark program for the WASM wrapper has an entry point method on -the ``FutharkContext``, and for the WebGPU wrapper, each entry point is exposed through the ``entry`` field of the ``FutharkModule`` object: +Each entry point in the compiled Futhark program is exposed through the +``entry`` field of the top-level wrapper object. For example, an entry +point named ``main`` can be called as: -.. js:function:: FutharkContext.(in1, ..., inN) +.. code-block:: javascript - The entry point function taking the N arguments of the Futhark entry point - function, and returns the result. For the WASM wrapper, if the result is a tuple the return value - is an array. For the WebGPU wrapper, if there are multiple outputs, the return value is an array of outputs in order. + const res = await fut.entry.main(in1, ..., inN); + +.. js:function:: fut.entry.(in1, ..., inN) + + The entry point function takes the JavaScript representations of the + Futhark entry point arguments and returns the result. + + If the entry point has multiple outputs, the return value is an array + containing the outputs in order. diff --git a/docs/man/futhark-bench.rst b/docs/man/futhark-bench.rst --- a/docs/man/futhark-bench.rst +++ b/docs/man/futhark-bench.rst @@ -14,13 +14,13 @@ DESCRIPTION =========== -This tool is the recommended way to benchmark Futhark programs. -Programs are compiled using the specified backend (``c`` by default), -then run a number of times for each test case, and the arithmetic mean -runtime and 95% confidence interval printed on standard output. Refer -to :ref:`futhark-test(1)` for information on how to format test data. -A program will be ignored if it contains no data sets - it will not -even be compiled. +This tool is the recommended way to benchmark Futhark programs. Programs are +compiled using the specified backend (``c`` by default), then run a number of +times for each test case, and the arithmetic mean runtime and 95% confidence +interval printed on standard output. Refer to :ref:`futhark-test(1)` for +information on how to format test data. A program will be ignored if it contains +no data sets - it will not even be compiled. Property-based tests are ignored +when benchmarking. If compilation of a program fails, then ``futhark bench`` will abort immediately. If execution of a test set fails, an error message will diff --git a/docs/man/futhark-test.rst b/docs/man/futhark-test.rst --- a/docs/man/futhark-test.rst +++ b/docs/man/futhark-test.rst @@ -28,12 +28,11 @@ == cases... -The ``description`` is an arbitrary (and possibly multiline) -human-readable explanation of the test program. It is separated from -the test cases by a line containing just ``==``. Any comment starting -at the beginning of the line, and containing a line consisting of just -``==``, will be considered a test block. The format of a test case is -as follows:: +The ``description`` is an arbitrary (and possibly multiline) human-readable +explanation of the test program. It is separated from the test cases by a line +containing just ``==``. Any comment starting at the beginning of the line, and +containing a line consisting of just ``==``, will be considered a test block. +The format of a unit test case is as follows:: [tags { tags... }] [entry: names...] @@ -136,6 +135,49 @@ element. If no suffix is provided, integer arrays have element type ``i32`` and decimal arrays have type ``f64``. +PROPERTY-BASED TESTING +---------------------- + +Apart from containing input/output tests as described above, a test block may +also have the following form:: + + property: names... + +In this case, the names indicate *properties*. A property is an entry point +with this type:: + + t -> bool + +for some ``t``, which has been given a ``#[prop]`` pragma. To test a property, +``futhark test`` will randomly generate values of type ``t``, called +*candidates*, looking for a candidate that makes the property return ``false``, +called a *counterexample*. When a counterexample has been found, ``futhark +test`` will try to shrink it and finally report the smallest counterexample that +it was able construct. + +The ``#[prop]`` attribute supports various optional arguments that grant more +control over the testing process. They are passed as arguments, e.g., +``#[prop(gen(foo),shrink(bar))]``. The following are supported: + +* ``gen(f)``, where ``f`` is an entry point function with this type:: + + (size: i64) -> (seed: u64) -> t + + Instead of automatically generating candidates for the property, ``futhark + test`` will invoke ``f`` with a size and a randomly generated seed. This can + be used to generate more complicated types. + +* ``shrink(f)``, where ``f`` is an entry point function with this type:: + + t -> u64 -> t + + When shrinking a counterexample, ``futhark test`` will call ``f`` with the + candidate so far along with a random number, which is then expected to return + a smaller value. + +* ``size(N)``, where ``N`` is an integer. This sets the size of generated candidates + (or the size argument passed to generators). + OPTIONS ======= @@ -186,6 +228,11 @@ Run ``structure`` tests. These are not run by default. When this option is passed, no other testing is done. +--seed=INT + + Set random seed used to generate values for property-based tests. If unset, a + seed is randomly generated. + --futhark=program The program used to perform operations (eg. compilation). Defaults @@ -278,8 +325,16 @@ -- random input { [100]i32 [100]i32 } auto output -- random input { [1000]i32 [1000]i32 } auto output - let main xs ys = i32.product (map2 (*) xs ys) + entry main xs ys = i32.product (map2 (*) xs ys) +The following tests that reverse is an involution:: + + -- == + -- property: reverse_involution + + #[prop] + entry reverse_involution (xs: []i32) = + and (map2 (==) (reverse (reverse xs)) xs) SEE ALSO ======== diff --git a/futhark.cabal b/futhark.cabal --- a/futhark.cabal +++ b/futhark.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: futhark -version: 0.26.2 +version: 0.26.3 synopsis: An optimising compiler for a functional, array-oriented language. description: Futhark is a small programming language designed to be compiled to @@ -320,7 +320,6 @@ Futhark.Optimise.BlkRegTiling Futhark.Optimise.CSE Futhark.Optimise.DoubleBuffer - Futhark.Optimise.EntryPointMem Futhark.Optimise.Fusion Futhark.Optimise.Fusion.Composing Futhark.Optimise.Fusion.GraphRep @@ -394,6 +393,7 @@ Futhark.Profile.SourceRange Futhark.Script Futhark.Test + Futhark.Test.Property Futhark.Test.Spec Futhark.Test.Values Futhark.Tools diff --git a/rts/c/cache.h b/rts/c/cache.h --- a/rts/c/cache.h +++ b/rts/c/cache.h @@ -67,8 +67,8 @@ if (fseek(f, 0, SEEK_END) != 0) { goto error; } - int64_t f_size = (int64_t)ftell(f); - if (fseek(f, CACHE_HEADER_SIZE, SEEK_SET) != 0) { + int64_t f_size = (int64_t)ftello(f); + if (fseeko(f, CACHE_HEADER_SIZE, SEEK_SET) != 0) { goto error; } diff --git a/rts/c/server.h b/rts/c/server.h --- a/rts/c/server.h +++ b/rts/c/server.h @@ -1624,7 +1624,7 @@ // (which doesn't care if there's extra at the end), then we compute // how much space the the object actually takes in serialised form // and rewind the file to that position. The only downside is more IO. - size_t start = ftell(f); + size_t start = (size_t)ftello(f); size_t size; char *bytes = fslurp_file(f, &size); void *obj = aux->restore(ctx, bytes); @@ -1633,10 +1633,10 @@ *(void**)p = obj; size_t obj_size; (void)aux->store(ctx, obj, NULL, &obj_size); - fseek(f, start+obj_size, SEEK_SET); + fseeko(f, start+obj_size, SEEK_SET); return 0; } else { - fseek(f, start, SEEK_SET); + fseeko(f, start, SEEK_SET); return 1; } } diff --git a/rts/c/util.h b/rts/c/util.h --- a/rts/c/util.h +++ b/rts/c/util.h @@ -60,10 +60,10 @@ // Read the rest of an open file into a NUL-terminated string; returns // NULL on error. static void* fslurp_file(FILE *f, size_t *size) { - long start = ftell(f); - fseek(f, 0, SEEK_END); - long src_size = ftell(f)-start; - fseek(f, start, SEEK_SET); + off_t start = ftello(f); + fseeko(f, 0, SEEK_END); + off_t src_size = ftello(f)-start; + fseeko(f, start, SEEK_SET); unsigned char *s = (unsigned char*) malloc((size_t)src_size + 1); if (fread(s, 1, (size_t)src_size, f) != (size_t)src_size) { free(s); diff --git a/rts/javascript/wrapperclasses.js b/rts/javascript/wrapperclasses.js --- a/rts/javascript/wrapperclasses.js +++ b/rts/javascript/wrapperclasses.js @@ -32,9 +32,13 @@ shape() { this.validCheck(); var s = this.fshape(this.ctx.ctx, this.ptr) >> 3; - return Array.from(this.ctx.wasm.HEAP64.subarray(s, s + this.dim)); + return this.ctx.wasm.HEAP64.subarray(s, s + this.dim); } + // get_shape() { + // return BigInt64Array.from(this.shape()); + // } + toTypedArray(dims = this.shape()) { this.validCheck(); console.assert(dims.length === this.dim, "dim=%s,dims=%s", this.dim, dims.toString()); @@ -56,6 +60,10 @@ return Array.from(Array(d0), (x,i) => nest(offs + i * d1, ds.slice(1))); } })(0, dims); + } + + async values() { + return this.toTypedArray(); } } diff --git a/src/Futhark/Analysis/LastUse.hs b/src/Futhark/Analysis/LastUse.hs --- a/src/Futhark/Analysis/LastUse.hs +++ b/src/Futhark/Analysis/LastUse.hs @@ -301,6 +301,10 @@ let free_in_e = freeIn se <> freeIn sp (used_nms', lu_vars) <- lastUsedInNames used_nms free_in_e pure (M.empty, lu_vars, used_nms') +lastUseMemOp _ (EnsureDirect v) used_nms = do + let free_in_e = freeIn v + (used_nms', lu_vars) <- lastUsedInNames used_nms free_in_e + pure (M.empty, lu_vars, used_nms') lastUseMemOp onInner (Inner op) used_nms = onInner op used_nms lastUseSegOp :: @@ -399,6 +403,10 @@ lastUseSeqOp :: Op (Aliases SeqMem) -> Names -> LastUseM SeqMem (LUTabFun, Names, Names) lastUseSeqOp (Alloc se sp) used_nms = do let free_in_e = freeIn se <> freeIn sp + (used_nms', lu_vars) <- lastUsedInNames used_nms free_in_e + pure (mempty, lu_vars, used_nms') +lastUseSeqOp (EnsureDirect v) used_nms = do + let free_in_e = freeIn v (used_nms', lu_vars) <- lastUsedInNames used_nms free_in_e pure (mempty, lu_vars, used_nms') lastUseSeqOp (Inner NoOp) used_nms = do diff --git a/src/Futhark/Analysis/MemAlias.hs b/src/Futhark/Analysis/MemAlias.hs --- a/src/Futhark/Analysis/MemAlias.hs +++ b/src/Futhark/Analysis/MemAlias.hs @@ -85,6 +85,9 @@ MemAliasesM (inner rep) MemAliases analyzeStm m (Let (Pat [PatElem vname _]) _ (Op (Alloc _ _))) = pure $ m <> singleton vname mempty +analyzeStm m (Let (Pat (PatElem mem_name _ : _)) _ (Op (EnsureDirect _))) = + pure $ m <> singleton mem_name mempty +analyzeStm m (Let _ _ (Op (EnsureDirect _))) = pure m analyzeStm m (Let _ _ (Op (Inner inner))) = do on_inner <- asks onInner on_inner m inner diff --git a/src/Futhark/Bench.hs b/src/Futhark/Bench.hs --- a/src/Futhark/Bench.hs +++ b/src/Futhark/Bench.hs @@ -325,9 +325,11 @@ | otherwise = Nothing + maybeReload = + when (any inputConsumed input_types) reloadInput + doRun = do call_lines <- cmdEither (cmdCall server entry out ins) - when (any inputConsumed input_types) reloadInput case mapMaybe runtime call_lines of [call_runtime] -> pure (RunResult call_runtime, call_lines) [] -> throwError "Could not find runtime in output." @@ -337,9 +339,9 @@ -- First one uncounted warmup run. void $ cmdEither $ cmdCall server entry out ins - ys <- runMinimum (freeOut *> doRun) opts 0 0 mempty + ys <- runMinimum (freeOut *> doRun <* maybeReload) opts 0 0 mempty - xs <- runConvergence (freeOut *> doRun) opts ys + xs <- runConvergence (freeOut *> doRun <* maybeReload) opts ys -- Possibly a profiled run at the end. profile_log <- @@ -347,6 +349,8 @@ then pure Nothing else do cmdMaybe . liftIO $ cmdUnpauseProfiling server + -- No need to reload the input here, and it would indeed be misleading + -- in the profiling results. profile_log <- freeOut *> doRun cmdMaybe . liftIO $ cmdPauseProfiling server pure $ Just profile_log diff --git a/src/Futhark/CLI/Autotune.hs b/src/Futhark/CLI/Autotune.hs --- a/src/Futhark/CLI/Autotune.hs +++ b/src/Futhark/CLI/Autotune.hs @@ -130,7 +130,7 @@ 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 --- a/src/Futhark/CLI/Bench.hs +++ b/src/Futhark/CLI/Bench.hs @@ -186,7 +186,7 @@ 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/Dataset.hs b/src/Futhark/CLI/Dataset.hs --- a/src/Futhark/CLI/Dataset.hs +++ b/src/Futhark/CLI/Dataset.hs @@ -5,18 +5,19 @@ module Futhark.CLI.Dataset (main) where import Control.Monad -import Control.Monad.ST import Data.Binary qualified as Bin import Data.ByteString.Lazy.Char8 qualified as BS import Data.Text qualified as T import Data.Text.IO qualified as T -import Data.Vector.Generic (freeze) -import Data.Vector.Storable qualified as SVec -import Data.Vector.Storable.Mutable qualified as USVec import Data.Word import Futhark.Data qualified as V import Futhark.Data.Reader (readValues) -import Futhark.Util (convFloat) +import Futhark.Test.Values + ( RandomConfiguration (..), + Range, + initialRandomConfiguration, + randomValue, + ) import Futhark.Util.Options import Language.Futhark.Parser import Language.Futhark.Pretty () @@ -29,8 +30,6 @@ ) import System.Exit import System.IO -import System.Random (mkStdGen, uniformR) -import System.Random.Stateful (UniformRange (..)) -- | Run @futhark dataset@. main :: String -> [String] -> IO () @@ -209,23 +208,6 @@ toValueType (TEVar v _) = Left $ "Unknown type " <> prettyText v --- | Closed interval, as in @System.Random@. -type Range a = (a, a) - -data RandomConfiguration = RandomConfiguration - { i8Range :: Range Int8, - i16Range :: Range Int16, - i32Range :: Range Int32, - i64Range :: Range Int64, - u8Range :: Range Word8, - u16Range :: Range Word16, - u32Range :: Range Word32, - u64Range :: Range Word64, - f16Range :: Range Half, - f32Range :: Range Float, - f64Range :: Range Double - } - -- The following lines provide evidence about how Haskells record -- system sucks. seti8Range :: Range Int8 -> RandomConfiguration -> RandomConfiguration @@ -260,67 +242,3 @@ setf64Range :: Range Double -> RandomConfiguration -> RandomConfiguration setf64Range bounds config = config {f64Range = bounds} - -initialRandomConfiguration :: RandomConfiguration -initialRandomConfiguration = - RandomConfiguration - (minBound, maxBound) - (minBound, maxBound) - (minBound, maxBound) - (minBound, maxBound) - (minBound, maxBound) - (minBound, maxBound) - (minBound, maxBound) - (minBound, maxBound) - (0.0, 1.0) - (0.0, 1.0) - (0.0, 1.0) - -randomValue :: RandomConfiguration -> V.ValueType -> Word64 -> V.Value -randomValue conf (V.ValueType ds t) seed = - case t of - V.I8 -> gen i8Range V.I8Value - V.I16 -> gen i16Range V.I16Value - V.I32 -> gen i32Range V.I32Value - V.I64 -> gen i64Range V.I64Value - V.U8 -> gen u8Range V.U8Value - V.U16 -> gen u16Range V.U16Value - V.U32 -> gen u32Range V.U32Value - V.U64 -> gen u64Range V.U64Value - V.F16 -> gen f16Range V.F16Value - V.F32 -> gen f32Range V.F32Value - V.F64 -> gen f64Range V.F64Value - V.Bool -> gen (const (False, True)) V.BoolValue - where - gen range final = randomVector (range conf) final ds seed - -randomVector :: - (SVec.Storable v, UniformRange v) => - Range v -> - (SVec.Vector Int -> SVec.Vector v -> V.Value) -> - [Int] -> - Word64 -> - V.Value -randomVector range final ds seed = runST $ do - -- Use some nice impure computation where we can preallocate a - -- vector of the desired size, populate it via the random number - -- generator, and then finally reutrn a frozen binary vector. - arr <- USVec.new n - let fill g i - | i < n = do - let (v, g') = uniformR range g - USVec.write arr i v - g' `seq` fill g' $! i + 1 - | otherwise = - pure () - fill (mkStdGen $ fromIntegral seed) 0 - final (SVec.fromList ds) . SVec.convert <$> freeze arr - where - n = product ds - --- XXX: The following instance is an orphan. Maybe it could be --- avoided with some newtype trickery or refactoring, but it's so --- convenient this way. -instance UniformRange Half where - uniformRM (a, b) g = - (convFloat :: Float -> Half) <$> uniformRM (convFloat a, convFloat b) g diff --git a/src/Futhark/CLI/Dev.hs b/src/Futhark/CLI/Dev.hs --- a/src/Futhark/CLI/Dev.hs +++ b/src/Futhark/CLI/Dev.hs @@ -675,6 +675,11 @@ "Ignore 'unsafe'.", Option [] + ["strip-provenance"] + (NoArg $ Right $ changeFutharkConfig $ \opts -> opts {futharkStripProvenance = True}) + "Strip provenance (location information).", + Option + [] ["entry-points"] ( ReqArg ( \arg -> Right $ diff --git a/src/Futhark/CLI/Misc.hs b/src/Futhark/CLI/Misc.hs --- a/src/Futhark/CLI/Misc.hs +++ b/src/Futhark/CLI/Misc.hs @@ -84,7 +84,7 @@ 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 --- a/src/Futhark/CLI/Test.hs +++ b/src/Futhark/CLI/Test.hs @@ -14,16 +14,19 @@ import Control.Monad.Trans.Class (lift) import Data.ByteString qualified as SBS import Data.ByteString.Lazy qualified as LBS +import Data.IORef 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 import Data.Time.Clock.System (SystemTime (..), getSystemTime) +import Data.Word (Word64) import Futhark.Analysis.Metrics.Type import Futhark.Server import Futhark.Test -import Futhark.Util (atMostChars, fancyTerminal, showText) +import Futhark.Util (atMostChars, fancyTerminal, randomSeed, showText) import Futhark.Util.Options import Futhark.Util.Pretty (annotate, bgColor, bold, hardline, pretty, putDoc, vsep) import Futhark.Util.Table @@ -92,8 +95,8 @@ 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 +115,24 @@ race (threadDelay timeout) (f server) >>= \case Left _ -> do abortServer server - fail $ "test timeout after " <> show timeout <> " microseconds" + st <- readIORef phaseRef + fail . T.unpack $ + "test timeout after " <> showText 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 (" during phase " <>) (phase st) + shrinkInfo = maybe mempty (" while shrinking with " <>) (shrinkWith st) + sizeInfo = maybe mempty ((" at size=" <>) . showText) (phaseSize st) + seedInfo = maybe mempty ((" and seed=" <>) . showText) (phaseSeed st) + tacticInfo = maybe mempty ((" with tactic=" <>) . showText) (phaseRandom st) + ". Was evaluating property:\n" + <> activeTestName + <> phaseInfo + <> shrinkInfo + <> sizeInfo + <> seedInfo + <> tacticInfo Right r -> pure r data TestMode @@ -134,7 +154,8 @@ { _testCaseMode :: TestMode, testCaseProgram :: FilePath, testCaseTest :: ProgramTest, - _testCasePrograms :: ProgConfig + _testCasePrograms :: ProgConfig, + pbtConfig :: PBTConfig } deriving (Show) @@ -252,7 +273,7 @@ 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 +310,22 @@ 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, + phaseRandom = Nothing + } + when (mode `elem` [Compiled, Interpreted]) $ context "Generating reference outputs" $ -- We probably get the concurrency at the test program level, @@ -316,10 +348,29 @@ ++ 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 + liftIO (extractPropSpecs server (map propertyEntryPoint properties)) >>= \case + Left err -> pure [Failure [err]] + Right propSpecs -> liftIO $ do + normal_test_result <- concat <$> mapM run ios + let verifiedProps = selectRequestedPropSpecs properties propSpecs + pbt_resultE <- runPBT pbtConfig server verifiedProps phaseRef program + + let allResults = flip map pbt_resultE $ \case + Left err -> Failure [err] + Right (Just e) -> Failure [e] + Right Nothing -> Success + + let hasFailures = any (\case Failure _ -> True; _ -> False) allResults + + when hasFailures $ + liftIO $ + propToFile program allResults + + pure $ normal_test_result ++ allResults + when (mode == Interpreted) $ context "Interpreting" $ accErrors_ $ @@ -464,7 +515,7 @@ 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) (configPBTConfig config) data ReportMsg = TestStarted TestCase @@ -489,8 +540,8 @@ 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 +620,7 @@ 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 +643,11 @@ 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 +691,6 @@ testStatusRunFail ts' + min (numTestCases test) (length s) } - when fancy spaceTable ts <- @@ -659,7 +710,12 @@ -- 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 +734,8 @@ configExclude :: [T.Text], configLineOutput :: Bool, configConcurrency :: Maybe Int, - configEntryPoint :: Maybe String + configEntryPoint :: Maybe String, + configPBTConfig :: PBTConfig } defaultConfig :: TestConfig @@ -698,7 +755,14 @@ }, configLineOutput = False, configConcurrency = Nothing, - configEntryPoint = Nothing + configEntryPoint = Nothing, + configPBTConfig = + PBTConfig + { configNumTests = 100, + configMaxSize = 50, + configSeed = randomSeed, + configShrinkTries = 5 + } } data ProgConfig = ProgConfig @@ -716,6 +780,9 @@ 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 +921,72 @@ ) "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 :: [(Word64, String)]) of + [(n', "")] -> + Right $ changePBTConfig $ \pbt -> pbt {configSeed = 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 @@ -865,9 +997,35 @@ : configExclude config } +selectRequestedPropSpecs :: [PropertyCase] -> [PropSpec] -> [PropSpec] +selectRequestedPropSpecs properties specs = + mapMaybe lookupSpec properties + where + lookupSpec (PropertyCase name) = + firstMatching name specs + + firstMatching _ [] = + Nothing + firstMatching name (spec : rest) + | psProp spec == name = Just spec + | otherwise = firstMatching name rest + +-- Save to file helper functions +propToFile :: FilePath -> [TestResult] -> IO () +propToFile testFile results = do + let fileName = dropExtension 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 + -- | Run @futhark test@. main :: String -> [String] -> IO () -main = mainWithOptions defaultConfig commandLineOptions "options... programs..." $ \progs config -> - case progs of - [] -> Nothing - _ -> Just $ runTests (excludeBackend config) progs +main = + mainWithOptions defaultConfig commandLineOptions "options... programs..." $ \progs config -> + case progs of + [] -> Nothing + _ -> Just $ runTests (excludeBackend config) progs diff --git a/src/Futhark/CodeGen/Backends/GenericC.hs b/src/Futhark/CodeGen/Backends/GenericC.hs --- a/src/Futhark/CodeGen/Backends/GenericC.hs +++ b/src/Futhark/CodeGen/Backends/GenericC.hs @@ -314,6 +314,7 @@ #ifndef _GNU_SOURCE // Avoid possible double-definition warning. #define _GNU_SOURCE #endif +#define _FILE_OFFSET_BITS 64 |] -- We may generate variables that are never used (e.g. for diff --git a/src/Futhark/CodeGen/Backends/GenericWASM.hs b/src/Futhark/CodeGen/Backends/GenericWASM.hs --- a/src/Futhark/CodeGen/Backends/GenericWASM.hs +++ b/src/Futhark/CodeGen/Backends/GenericWASM.hs @@ -132,7 +132,12 @@ "_futhark_context_config_free", "_futhark_context_new", "_futhark_context_free", - "_futhark_context_get_error" + "_futhark_context_get_error", + "_futhark_context_sync", + "_futhark_context_clear_caches", + "_futhark_context_report", + "_futhark_context_pause_profiling", + "_futhark_context_unpause_profiling" ] where -- Include array types from both entry points and record fields. @@ -153,23 +158,28 @@ classFutharkContext entryPoints opaqueTypes ] +-- Make FutharkModule the generated primary class, but keeps FutharkContext around for backwards compatibility. classFutharkContext :: [JSEntryPoint] -> [(String, JSOpaqueType)] -> T.Text classFutharkContext entryPoints opaqueTypes = T.unlines - [ "class FutharkContext {", - constructor entryPoints opaqueTypes, + [ "class FutharkModule {", + moduleConstructor, + moduleInitFromWasm entryPoints opaqueTypes, + moduleInit, getFreeFun, getEntryPointsFun, getTypesFun, getErrorFun, + getUtilityFuns, T.unlines $ map toFutharkArray arrays, T.unlines $ concatMap (generateProjectMethods . snd) opaqueTypes, T.unlines $ map jsWrapEntryPoint entryPoints, "}", + classFutharkContextCompat, [text| - async function newFutharkContext() { + async function newFutharkContext(num_threads) { var wasm = await loadWASM(); - return new FutharkContext(wasm); + return new FutharkContext(wasm, num_threads); } |] ] @@ -180,32 +190,90 @@ entryPointTypes = concatMap (\jse -> parameters jse ++ [ret jse]) entryPoints recordFieldTypes = [jsrfType rf | (_, JSOpaqueRecord fields) <- opaqueTypes, rf <- fields] -constructor :: [JSEntryPoint] -> [(String, JSOpaqueType)] -> T.Text -constructor jses opaqueTypes = +moduleConstructor :: T.Text +moduleConstructor = [text| - constructor(wasm, num_threads) { + constructor() { + this.wasm = undefined; + this.cfg = undefined; + this.ctx = undefined; + this.entry_points = {}; + this.types = {}; + this.entry = {}; + } + |] + +moduleInitFromWasm :: [JSEntryPoint] -> [(String, JSOpaqueType)] -> T.Text +moduleInitFromWasm jses opaqueTypes = + [text| + _init_from_wasm(wasm, num_threads) { this.wasm = wasm; this.cfg = this.wasm._futhark_context_config_new(); if (num_threads) this.wasm._futhark_context_config_set_num_threads(this.cfg, num_threads); this.ctx = this.wasm._futhark_context_new(this.cfg); + this.entry_points = { ${entries} }; this.types = { ${type_entries} }; + this.entry = {}; + ${entry_aliases} + ${array_aliases} + ${array_type_aliases} } |] where entries = T.intercalate "," $ map dicEntry jses type_entries = T.intercalate "," $ map dicTypeEntry opaqueTypes + entry_aliases = T.unlines $ map entryAlias jses + array_aliases = T.unlines $ map arrayAlias arrays + array_type_aliases = T.unlines $ map arrayTypeAlias arrays + arrays = nubOrd $ filter isArray (entryPointTypes ++ recordFieldTypes) + entryPointTypes = concatMap (\jse -> parameters jse ++ [ret jse]) jses + recordFieldTypes = [jsrfType rf | (_, JSOpaqueRecord fields) <- opaqueTypes, rf <- fields] + +moduleInit :: T.Text +moduleInit = + [text| + async init(wasm, num_threads) { + if (wasm === undefined) { + throw new Error("FutharkModule.init() requires the generated backend runtime module"); + } + + this._init_from_wasm(wasm, num_threads); + } + |] + +classFutharkContextCompat :: T.Text +classFutharkContextCompat = + [text| + class FutharkContext extends FutharkModule { + constructor(wasm, num_threads) { + super(); + + if (wasm !== undefined) { + this._init_from_wasm(wasm, num_threads); + } + } + } + |] + getFreeFun :: T.Text getFreeFun = [text| free() { - this.wasm._futhark_context_free(this.ctx); - this.wasm._futhark_context_config_free(this.cfg); + if (this.ctx !== undefined) { + this.wasm._futhark_context_free(this.ctx); + this.ctx = undefined; + } + + if (this.cfg !== undefined) { + this.wasm._futhark_context_config_free(this.cfg); + this.cfg = undefined; + } } |] @@ -237,6 +305,65 @@ } |] +getUtilityFuns :: T.Text +getUtilityFuns = + [text| + async context_sync() { + return this.wasm._futhark_context_sync(this.ctx); + } + + async clear_caches() { + return this.wasm._futhark_context_clear_caches(this.ctx); + } + + async report() { + var ptr = this.wasm._futhark_context_report(this.ctx); + var len = this.wasm.HEAP8.subarray(ptr).indexOf(0); + var bytes = this.wasm.HEAPU8.subarray(ptr, ptr + len); + var str = new TextDecoder().decode(bytes); + this.wasm._free(ptr); + return str; + } + + async pause_profiling() { + return this.wasm._futhark_context_pause_profiling(this.ctx); + } + + async unpause_profiling() { + return this.wasm._futhark_context_unpause_profiling(this.ctx); + } + |] + +entryAlias :: JSEntryPoint -> T.Text +entryAlias jse = + [text|this.entry["${ename}"] = this.${fname}.bind(this);|] + where + fname = GC.escapeName $ T.pack $ name jse + ename = T.pack $ name jse + +arrayAlias :: String -> T.Text +arrayAlias typ = + [text| + this.${signature} = { + from_data: (data, ${dims}) => this.new_${signature}(data, ${dims}), + from_jsarray: (data) => this.new_${signature}_from_jsarray(data) + }; + |] + where + d = dim typ + ftype = baseType typ + signature = T.pack $ ftype ++ "_" ++ show d ++ "d" + dims = T.pack $ intercalate ", " ["d" ++ show i | i <- [0 .. d - 1]] + +arrayTypeAlias :: String -> T.Text +arrayTypeAlias typ = + [text|this.types["${typ_text}"] = this.${signature};|] + where + d = dim typ + ftype = baseType typ + signature = T.pack $ ftype ++ "_" ++ show d ++ "d" + typ_text = T.pack typ + dicEntry :: JSEntryPoint -> T.Text dicEntry jse = [text| @@ -476,4 +603,4 @@ -- | The names exported by the generated module. libraryExports :: T.Text -libraryExports = "export {newFutharkContext, FutharkContext, FutharkArray, FutharkOpaque};" +libraryExports = "export {newFutharkContext, FutharkContext, FutharkModule, FutharkArray, FutharkOpaque};" diff --git a/src/Futhark/CodeGen/ImpGen.hs b/src/Futhark/CodeGen/ImpGen.hs --- a/src/Futhark/CodeGen/ImpGen.hs +++ b/src/Futhark/CodeGen/ImpGen.hs @@ -59,6 +59,7 @@ tvVar, ToExp (..), compileAlloc, + compileEnsureDirect, everythingVolatile, compileBody, compileBody', @@ -1741,6 +1742,32 @@ Just allocator' -> allocator' (patElemName mem) e' compileAlloc pat _ _ = error $ "compileAlloc: Invalid pattern: " ++ prettyString pat + +-- | Compile an 'EnsureDirect' operation. The pattern must contain +-- two elements: a memory block and an array. If the input array is +-- already row-major with zero offset, no copy is made. Otherwise, +-- memory is allocated and the array is copied into it. +compileEnsureDirect :: + (Mem rep inner) => Pat (LetDec rep) -> VName -> ImpM rep r op () +compileEnsureDirect (Pat [mem_pe, _]) src = do + src_entry <- lookupArray src + let src_loc@(MemLoc src_mem src_shape src_lmad) = entryArrayLoc src_entry + pt = entryArrayElemType src_entry + row_major_lmad = LMAD.iota 0 (map pe64 src_shape) + is_row_major = LMAD.dynamicEqualsLMAD src_lmad row_major_lmad + src_space <- entryMemSpace <$> lookupMemory src_mem + let dest_mem = patElemName mem_pe + dest_loc = MemLoc dest_mem src_shape row_major_lmad + sIf + is_row_major + (emit $ Imp.SetMem dest_mem src_mem src_space) + ( do + let size = Imp.bytes $ primByteSize pt * product (map pe64 src_shape) + sAlloc_ dest_mem size src_space + lmadCopy pt dest_loc src_loc + ) +compileEnsureDirect pat _ = + error $ "compileEnsureDirect: Invalid pattern: " ++ prettyString pat -- | The number of bytes needed to represent the array in a -- straightforward contiguous format, as an t'Int64' expression. diff --git a/src/Futhark/CodeGen/ImpGen/GPU.hs b/src/Futhark/CodeGen/ImpGen/GPU.hs --- a/src/Futhark/CodeGen/ImpGen/GPU.hs +++ b/src/Futhark/CodeGen/ImpGen/GPU.hs @@ -115,6 +115,8 @@ CallKernelGen () opCompiler dest (Alloc e space) = compileAlloc dest e space +opCompiler dest (EnsureDirect v) = + compileEnsureDirect dest v opCompiler (Pat [pe]) (Inner (SizeOp (GetSize key size_class))) = do fname <- askFunction let key' = keyWithEntryPoint fname key diff --git a/src/Futhark/CodeGen/ImpGen/Multicore.hs b/src/Futhark/CodeGen/ImpGen/Multicore.hs --- a/src/Futhark/CodeGen/ImpGen/Multicore.hs +++ b/src/Futhark/CodeGen/ImpGen/Multicore.hs @@ -23,6 +23,7 @@ opCompiler :: OpCompiler MCMem HostEnv Imp.Multicore opCompiler dest (Alloc e space) = compileAlloc dest e space +opCompiler dest (EnsureDirect v) = compileEnsureDirect dest v opCompiler dest (Inner op) = compileMCOp dest op parallelCopy :: CopyCompiler MCMem HostEnv Imp.Multicore diff --git a/src/Futhark/CodeGen/ImpGen/Sequential.hs b/src/Futhark/CodeGen/ImpGen/Sequential.hs --- a/src/Futhark/CodeGen/ImpGen/Sequential.hs +++ b/src/Futhark/CodeGen/ImpGen/Sequential.hs @@ -19,4 +19,6 @@ ops = ImpGen.defaultOperations opCompiler opCompiler dest (Alloc e space) = ImpGen.compileAlloc dest e space + opCompiler dest (EnsureDirect v) = + ImpGen.compileEnsureDirect dest v opCompiler _ (Inner NoOp) = pure () diff --git a/src/Futhark/Compiler/Config.hs b/src/Futhark/Compiler/Config.hs --- a/src/Futhark/Compiler/Config.hs +++ b/src/Futhark/Compiler/Config.hs @@ -41,7 +41,9 @@ -- | Additional functions that should be exposed as entry points. futharkEntryPoints :: [Name], -- | If false, disable type-checking - futharkTypeCheck :: Bool + futharkTypeCheck :: Bool, + -- | If true, strip provenance from program. + futharkStripProvenance :: Bool } -- | The default compiler configuration. @@ -53,5 +55,6 @@ futharkWerror = False, futharkSafe = False, futharkEntryPoints = [], - futharkTypeCheck = True + futharkTypeCheck = True, + futharkStripProvenance = False } diff --git a/src/Futhark/IR/GPUMem.hs b/src/Futhark/IR/GPUMem.hs --- a/src/Futhark/IR/GPUMem.hs +++ b/src/Futhark/IR/GPUMem.hs @@ -52,6 +52,7 @@ TC.TypeM GPUMem () typeCheckMemoryOp _ (Alloc size _) = TC.require (Prim int64) size + typeCheckMemoryOp _ (EnsureDirect _) = pure () typeCheckMemoryOp lvl (Inner op) = typeCheckHostOp (typeCheckMemoryOp . Just) lvl (const $ pure ()) op checkFParamDec = checkMemInfo diff --git a/src/Futhark/IR/MCMem.hs b/src/Futhark/IR/MCMem.hs --- a/src/Futhark/IR/MCMem.hs +++ b/src/Futhark/IR/MCMem.hs @@ -43,6 +43,7 @@ where typeCheckMemoryOp (Alloc size _) = TC.require (Prim int64) size + typeCheckMemoryOp (EnsureDirect _) = pure () typeCheckMemoryOp (Inner op) = typeCheckMCOp (const $ pure ()) op checkFParamDec = checkMemInfo diff --git a/src/Futhark/IR/Mem.hs b/src/Futhark/IR/Mem.hs --- a/src/Futhark/IR/Mem.hs +++ b/src/Futhark/IR/Mem.hs @@ -184,6 +184,12 @@ data MemOp (inner :: Data.Kind.Type -> Data.Kind.Type) (rep :: Data.Kind.Type) = -- | Allocate a memory block. Alloc SubExp Space + | -- | If the given array has a direct index function (as 'LMAD.isDirect'), + -- returns the array unchanged. Otherwise, make a copy of the array. The + -- choice is made dynamically, and the goal is to handle cases where we must + -- return something that is direct (mostly entry point return types), but we + -- cannot statically be sure of the layout of some array. + EnsureDirect VName | Inner (inner rep) deriving (Eq, Ord, Show) @@ -193,59 +199,79 @@ OpStmsTraverser m (inner rep) rep -> OpStmsTraverser m (MemOp inner rep) rep traverseMemOpStms _ _ op@Alloc {} = pure op +traverseMemOpStms _ _ op@EnsureDirect {} = pure op traverseMemOpStms onInner f (Inner inner) = Inner <$> onInner f inner instance (RephraseOp inner) => RephraseOp (MemOp inner) where rephraseInOp _ (Alloc e space) = pure (Alloc e space) + rephraseInOp _ (EnsureDirect v) = pure (EnsureDirect v) rephraseInOp r (Inner x) = Inner <$> rephraseInOp r x instance (FreeIn (inner rep)) => FreeIn (MemOp inner rep) where freeIn' (Alloc size _) = freeIn' size + freeIn' (EnsureDirect v) = freeIn' v freeIn' (Inner k) = freeIn' k instance (TypedOp inner) => TypedOp (MemOp inner) where opType (Alloc _ space) = pure [Mem space] + opType (EnsureDirect v) = f <$> lookupType v + where + f (Array pt shape _) = + [Mem DefaultSpace, Array pt (fmap Free shape) NoUniqueness] + f _ = error $ "EnsureDirect applied to non-array: " ++ show v opType (Inner k) = opType k instance (AliasedOp inner) => AliasedOp (MemOp inner) where opAliases Alloc {} = [mempty] + -- XXX - why not mem aliases for EnsureDirect? + opAliases (EnsureDirect v) = [mempty, oneName v] opAliases (Inner k) = opAliases k consumedInOp Alloc {} = mempty + consumedInOp EnsureDirect {} = mempty consumedInOp (Inner k) = consumedInOp k instance (CanBeAliased inner) => CanBeAliased (MemOp inner) where addOpAliases _ (Alloc se space) = Alloc se space + addOpAliases _ (EnsureDirect v) = EnsureDirect v addOpAliases aliases (Inner k) = Inner $ addOpAliases aliases k instance (Rename (inner rep)) => Rename (MemOp inner rep) where rename (Alloc size space) = Alloc <$> rename size <*> pure space + rename (EnsureDirect v) = EnsureDirect <$> rename v rename (Inner k) = Inner <$> rename k instance (Substitute (inner rep)) => Substitute (MemOp inner rep) where substituteNames subst (Alloc size space) = Alloc (substituteNames subst size) space + substituteNames subst (EnsureDirect v) = EnsureDirect (substituteNames subst v) substituteNames subst (Inner k) = Inner $ substituteNames subst k instance (PP.Pretty (inner rep)) => PP.Pretty (MemOp inner rep) where pretty (Alloc e DefaultSpace) = "alloc" <> PP.apply [PP.pretty e] pretty (Alloc e s) = "alloc" <> PP.apply [PP.pretty e, PP.pretty s] + pretty (EnsureDirect v) = "ensure_direct" <> PP.apply [PP.pretty v] pretty (Inner k) = PP.pretty k instance (OpMetrics (inner rep)) => OpMetrics (MemOp inner rep) where opMetrics Alloc {} = seen "Alloc" + opMetrics EnsureDirect {} = seen "EnsureDirect" opMetrics (Inner k) = opMetrics k instance (IsOp inner) => IsOp (MemOp inner) where safeOp (Alloc (Constant (IntValue (Int64Value k))) _) = k >= 0 safeOp Alloc {} = False + safeOp EnsureDirect {} = True safeOp (Inner k) = safeOp k cheapOp (Inner k) = cheapOp k cheapOp Alloc {} = True + cheapOp EnsureDirect {} = False opDependencies (Alloc _ e) = [freeIn e] + opDependencies (EnsureDirect v) = [mempty, freeIn v] opDependencies (Inner op) = opDependencies op instance (CanBeWise inner) => CanBeWise (MemOp inner) where addOpWisdom (Alloc size space) = Alloc size space + addOpWisdom (EnsureDirect v) = EnsureDirect v addOpWisdom (Inner k) = Inner $ addOpWisdom k instance (ST.IndexOp (inner rep)) => ST.IndexOp (MemOp inner rep) where @@ -1159,6 +1185,18 @@ instance (OpReturns inner) => OpReturns (MemOp inner) where opReturns (Alloc _ space) = pure [MemMem space] + opReturns (EnsureDirect v) = do + space <- lookupMemSpace . fst =<< lookupArraySummary v + summary <- lookupMemInfo v + case summary of + MemArray et shape _ _ -> + pure + [ MemMem space, + MemArray et (fmap Free shape) NoUniqueness . Just $ + ReturnsNewBlock space 0 . LMAD.iota 0 $ + fmap (fmap Free . pe64) (shapeDims shape) + ] + _ -> error "EnsureDirect applied to non-array" opReturns (Inner op) = opReturns op instance OpReturns NoOp where diff --git a/src/Futhark/IR/Mem/Simplify.hs b/src/Futhark/IR/Mem/Simplify.hs --- a/src/Futhark/IR/Mem/Simplify.hs +++ b/src/Futhark/IR/Mem/Simplify.hs @@ -13,6 +13,7 @@ import Futhark.Analysis.UsageTable qualified as UT import Futhark.Construct import Futhark.IR.Mem +import Futhark.IR.Mem.LMAD qualified as LMAD import Futhark.IR.Prop.Aliases (AliasedOp) import Futhark.Optimise.Simplify qualified as Simplify import Futhark.Optimise.Simplify.Engine qualified as Engine @@ -112,6 +113,18 @@ Simplify $ attributing attrs $ letBind pat $ Op op decertifySafeAlloc _ _ _ _ = Skip +-- If we know by now that this array is direct, then there is no need for +-- EnsureDirect and we just remove it. +knownDirect :: (SimplifyMemory rep inner) => TopDownRuleOp (Wise rep) +knownDirect _ (Pat [PatElem mem' _, PatElem v' _]) _ (EnsureDirect v) = Simplify $ do + ~(MemArray _ _ _ (ArrayIn mem v_lmad)) <- lookupMemInfo v + if LMAD.isDirect v_lmad + then do + letBindNames [mem'] $ BasicOp $ SubExp $ Var mem + letBindNames [v'] $ BasicOp $ SubExp $ Var v + else cannotSimplify +knownDirect _ _ _ _ = Skip + -- -- copy(reshape(manifest(v0),s)) can be rewritten to just reshape(manifest(v0),s). -- @@ -141,6 +154,7 @@ standardRules <> ruleBook [ RuleOp decertifySafeAlloc, - RuleBasicOp copyManifest + RuleBasicOp copyManifest, + RuleOp knownDirect ] [] diff --git a/src/Futhark/IR/Parse.hs b/src/Futhark/IR/Parse.hs --- a/src/Futhark/IR/Parse.hs +++ b/src/Futhark/IR/Parse.hs @@ -1132,6 +1132,8 @@ [ keyword "alloc" *> parens (Alloc <$> pSubExp <*> choice [pComma *> pSpace, pure DefaultSpace]), + keyword "ensure_direct" + *> parens (EnsureDirect <$> pVName), Inner <$> pInner ] diff --git a/src/Futhark/IR/SeqMem.hs b/src/Futhark/IR/SeqMem.hs --- a/src/Futhark/IR/SeqMem.hs +++ b/src/Futhark/IR/SeqMem.hs @@ -37,6 +37,7 @@ instance TC.Checkable SeqMem where checkOp (Alloc size _) = TC.require (Prim int64) size + checkOp (EnsureDirect _) = pure () checkOp (Inner NoOp) = pure () checkFParamDec = checkMemInfo checkLParamDec = checkMemInfo diff --git a/src/Futhark/Internalise.hs b/src/Futhark/Internalise.hs --- a/src/Futhark/Internalise.hs +++ b/src/Futhark/Internalise.hs @@ -85,7 +85,11 @@ maybeLog "Defunctionalising" prog_decs5 <- Defunctionalise.transformProg prog_decs4 maybeLog "Converting to core IR" - Exps.transformProg (futharkSafe config) (visibleTypes prog) prog_decs5 + Exps.transformProg + (futharkSafe config) + (futharkStripProvenance config) + (visibleTypes prog) + prog_decs5 where verbose = fst (futharkVerbose config) > NotVerbose maybeLog s diff --git a/src/Futhark/Internalise/Exps.hs b/src/Futhark/Internalise/Exps.hs --- a/src/Futhark/Internalise/Exps.hs +++ b/src/Futhark/Internalise/Exps.hs @@ -31,10 +31,17 @@ -- | Convert a program in source Futhark to a program in the Futhark -- core language. -transformProg :: (MonadFreshNames m) => Bool -> VisibleTypes -> [E.ValBind] -> m (I.Prog SOACS) -transformProg always_safe types vbinds = do +transformProg :: + (MonadFreshNames m) => + Bool -> + Bool -> + VisibleTypes -> + [E.ValBind] -> + m (I.Prog SOACS) +transformProg always_safe strip_provenance types vbinds = do (opaques, consts, funs) <- - runInternaliseM always_safe (internaliseValBinds types vbinds) + runInternaliseM always_safe strip_provenance $ + internaliseValBinds types vbinds I.renameProg $ I.Prog opaques consts funs internaliseValBinds :: VisibleTypes -> [E.ValBind] -> InternaliseM () diff --git a/src/Futhark/Internalise/Monad.hs b/src/Futhark/Internalise/Monad.hs --- a/src/Futhark/Internalise/Monad.hs +++ b/src/Futhark/Internalise/Monad.hs @@ -51,7 +51,8 @@ envDoBoundsChecks :: Bool, envSafe :: Bool, envAttrs :: Attrs, - envLoc :: Loc + envLoc :: Loc, + envStripProvenance :: Bool } data InternaliseState = InternaliseState @@ -102,9 +103,10 @@ runInternaliseM :: (MonadFreshNames m) => Bool -> + Bool -> InternaliseM () -> m (OpaqueTypes, Stms SOACS, [FunDef SOACS]) -runInternaliseM safe (InternaliseM m) = +runInternaliseM safe strip (InternaliseM m) = modifyNameSource $ \src -> let ((_, consts), s) = runState (runReaderT (runBuilderT m mempty) newEnv) (newState src) @@ -118,7 +120,8 @@ envDoBoundsChecks = True, envSafe = safe, envAttrs = mempty, - envLoc = mempty + envLoc = mempty, + envStripProvenance = strip } newState src = InternaliseState @@ -220,9 +223,11 @@ -- | Attach the provided location to all statements produced during execution of -- this action. locating :: (Located a) => a -> InternaliseM b -> InternaliseM b -locating a - | loc == mempty || isBuiltinLoc loc = id - | otherwise = censorStms $ fmap onStm +locating a m + | loc == mempty || isBuiltinLoc loc = m + | otherwise = do + strip <- asks envStripProvenance + if strip then m else censorStms (fmap onStm) m where loc = locOf a onStm (Let pat aux e) = Let pat (aux {stmAuxLoc = Provenance mempty loc}) e diff --git a/src/Futhark/Optimise/ArrayShortCircuiting/ArrayCoalescing.hs b/src/Futhark/Optimise/ArrayShortCircuiting/ArrayCoalescing.hs --- a/src/Futhark/Optimise/ArrayShortCircuiting/ArrayCoalescing.hs +++ b/src/Futhark/Optimise/ArrayShortCircuiting/ArrayCoalescing.hs @@ -274,6 +274,7 @@ BotUpEnv -> ShortCircuitM GPUMem BotUpEnv shortCircuitGPUMem _ _ _ (Alloc _ _) _ bu_env = pure bu_env +shortCircuitGPUMem _ _ _ (EnsureDirect _) _ bu_env = pure bu_env shortCircuitGPUMem lutab pat certs (Inner (GPU.SegOp op)) td_env bu_env = shortCircuitSegOp isSegThread lutab pat certs op td_env bu_env shortCircuitGPUMem lutab pat certs (Inner (GPU.GPUBody _ body)) td_env bu_env = do @@ -308,6 +309,7 @@ BotUpEnv -> ShortCircuitM MCMem BotUpEnv shortCircuitMCMem _ _ _ (Alloc _ _) _ bu_env = pure bu_env +shortCircuitMCMem _ _ _ (EnsureDirect _) _ bu_env = pure bu_env shortCircuitMCMem _ _ _ (Inner (MC.OtherOp NoOp)) _ bu_env = pure bu_env shortCircuitMCMem lutab pat certs (Inner (MC.ParOp (Just par_op) op)) td_env bu_env = shortCircuitSegOp (const True) lutab pat certs par_op td_env bu_env @@ -1738,6 +1740,7 @@ computeScalarTableMemOp :: ComputeScalarTable rep (inner (Aliases rep)) -> ComputeScalarTable rep (MemOp inner (Aliases rep)) computeScalarTableMemOp _ _ (Alloc _ _) = pure mempty +computeScalarTableMemOp _ _ (EnsureDirect _) = pure mempty computeScalarTableMemOp onInner scope_table (Inner op) = onInner scope_table op computeScalarTableSegOp :: diff --git a/src/Futhark/Optimise/CSE.hs b/src/Futhark/Optimise/CSE.hs --- a/src/Futhark/Optimise/CSE.hs +++ b/src/Futhark/Optimise/CSE.hs @@ -324,6 +324,7 @@ instance (CSEInOp (op rep)) => CSEInOp (Memory.MemOp op rep) where cseInOp o@Memory.Alloc {} = pure o + cseInOp o@Memory.EnsureDirect {} = pure o cseInOp (Memory.Inner k) = Memory.Inner <$> subCSE (cseInOp k) instance diff --git a/src/Futhark/Optimise/EntryPointMem.hs b/src/Futhark/Optimise/EntryPointMem.hs deleted file mode 100644 --- a/src/Futhark/Optimise/EntryPointMem.hs +++ /dev/null @@ -1,76 +0,0 @@ -{-# LANGUAGE TypeFamilies #-} - --- | We require that entry points return arrays with zero offset in --- row-major order. "Futhark.Pass.ExplicitAllocations" is --- conservative and inserts copies to ensure this is the case. After --- simplification, it may turn out that those copies are redundant. --- This pass removes them. It's a pretty simple pass, as it only has --- to look at the top level of entry points. -module Futhark.Optimise.EntryPointMem - ( entryPointMemGPU, - entryPointMemMC, - entryPointMemSeq, - ) -where - -import Data.List (find) -import Data.Map.Strict qualified as M -import Futhark.IR.GPUMem (GPUMem) -import Futhark.IR.MCMem (MCMem) -import Futhark.IR.Mem -import Futhark.IR.SeqMem (SeqMem) -import Futhark.Pass -import Futhark.Pass.ExplicitAllocations.GPU () -import Futhark.Transform.Substitute - -type Table rep = M.Map VName (Stm rep) - -mkTable :: Stms rep -> Table rep -mkTable = foldMap f - where - f stm = M.fromList $ map (,stm) (patNames (stmPat stm)) - -varInfo :: (Mem rep inner) => VName -> Table rep -> Maybe (LetDecMem, Exp rep) -varInfo v table = do - Let pat _ e <- M.lookup v table - PatElem _ info <- find ((== v) . patElemName) (patElems pat) - Just (letDecMem info, e) - -optimiseFun :: (Mem rep inner) => Table rep -> FunDef rep -> FunDef rep -optimiseFun consts_table fd = - fd {funDefBody = onBody $ funDefBody fd} - where - table = consts_table <> mkTable (bodyStms (funDefBody fd)) - mkSubst (Var v0) - | Just (MemArray _ _ _ (ArrayIn mem0 lmad0), BasicOp (Manifest v1 _)) <- - varInfo v0 table, - Just (MemArray _ _ _ (ArrayIn mem1 lmad1), _) <- - varInfo v1 table, - lmad0 == lmad1 = - M.fromList [(mem0, mem1), (v0, v1)] - mkSubst _ = mempty - onBody (Body dec stms res) = - let substs = mconcat $ map (mkSubst . resSubExp) res - in Body dec stms $ substituteNames substs res - -entryPointMem :: (Mem rep inner) => Pass rep rep -entryPointMem = - Pass - { passName = "Entry point memory optimisation", - passDescription = "Remove redundant copies of entry point results.", - passFunction = intraproceduralTransformationWithConsts pure onFun - } - where - onFun consts fd = pure $ optimiseFun (mkTable consts) fd - --- | The pass for GPU representation. -entryPointMemGPU :: Pass GPUMem GPUMem -entryPointMemGPU = entryPointMem - --- | The pass for MC representation. -entryPointMemMC :: Pass MCMem MCMem -entryPointMemMC = entryPointMem - --- | The pass for Seq representation. -entryPointMemSeq :: Pass SeqMem SeqMem -entryPointMemSeq = entryPointMem diff --git a/src/Futhark/Optimise/InliningDeadFun.hs b/src/Futhark/Optimise/InliningDeadFun.hs --- a/src/Futhark/Optimise/InliningDeadFun.hs +++ b/src/Futhark/Optimise/InliningDeadFun.hs @@ -331,7 +331,13 @@ onLambda lam = lam {lambdaBody = onBody for_assert $ lambdaBody lam} onStm (Let pat aux e) = - Let pat (traceLocs p aux) $ onExp e + Let pat aux' $ onExp e + where + -- To cut down on clutter, we only propagate attributes to certain + -- expressions. + aux' = traceLocs p $ case e of + BasicOp Manifest {} -> aux {stmAuxAttrs = attrs <> stmAuxAttrs aux} + _ -> aux onExp = mapExp diff --git a/src/Futhark/Pass/ExpandAllocations.hs b/src/Futhark/Pass/ExpandAllocations.hs --- a/src/Futhark/Pass/ExpandAllocations.hs +++ b/src/Futhark/Pass/ExpandAllocations.hs @@ -896,6 +896,7 @@ Pat <$> mapM (rephrasePatElem (Right . unMem)) pes unAllocOp Alloc {} = Left "unAllocOp: unhandled Alloc" + unAllocOp EnsureDirect {} = Left "unAllocOp: unhandled EnsureDirect" unAllocOp (Inner OtherOp {}) = Left "unAllocOp: unhandled OtherOp" unAllocOp (Inner GPUBody {}) = Left "unAllocOp: unhandled GPUBody" unAllocOp (Inner (SizeOp op)) = pure $ SizeOp op diff --git a/src/Futhark/Pass/ExplicitAllocations.hs b/src/Futhark/Pass/ExplicitAllocations.hs --- a/src/Futhark/Pass/ExplicitAllocations.hs +++ b/src/Futhark/Pass/ExplicitAllocations.hs @@ -182,7 +182,7 @@ repairExpression (BasicOp (Reshape v shape)) = do v_mem <- fst <$> lookupArraySummary v space <- lookupMemSpace v_mem - v' <- snd <$> ensureDirectArray (Just space) v + v' <- snd <$> allocLinearArray space (baseName v) v pure $ BasicOp $ Reshape v' shape repairExpression e = error $ "repairExpression:\n" <> prettyString e @@ -513,7 +513,14 @@ default_space <- askDefaultSpace if LMAD.isDirect lmad && maybe True (== mem_space) space_ok then pure (mem, v) - else needCopy (fromMaybe default_space space_ok) + else + if maybe True (== mem_space) space_ok + then do + mem' <- newVName $ baseName mem <> "_direct" + v' <- newVName $ baseName v <> "_v" + letBindNames [mem', v'] $ Op $ EnsureDirect v + pure (mem', v') + else needCopy (fromMaybe default_space space_ok) where needCopy space = -- We need to do a new allocation, copy 'v', and make a new @@ -1080,6 +1087,8 @@ Engine.SimpleM rep (MemOp inner (Engine.Wise rep), Stms (Engine.Wise rep)) simplifyMemOp _ (Alloc size space) = (,) <$> (Alloc <$> Engine.simplify size <*> pure space) <*> pure mempty +simplifyMemOp _ (EnsureDirect v) = + (,) <$> (EnsureDirect <$> Engine.simplify v) <*> pure mempty simplifyMemOp onInner (Inner k) = do (k', hoisted) <- onInner k pure (Inner k', hoisted) @@ -1123,6 +1132,8 @@ opUsage (Alloc (Var size) _) = UT.sizeUsage size opUsage (Alloc _ _) = + mempty + opUsage (EnsureDirect _) = mempty opUsage (Inner inner) = innerUsage inner diff --git a/src/Futhark/Passes.hs b/src/Futhark/Passes.hs --- a/src/Futhark/Passes.hs +++ b/src/Futhark/Passes.hs @@ -22,7 +22,6 @@ import Futhark.Optimise.ArrayShortCircuiting qualified as ArrayShortCircuiting import Futhark.Optimise.CSE import Futhark.Optimise.DoubleBuffer -import Futhark.Optimise.EntryPointMem import Futhark.Optimise.Fusion import Futhark.Optimise.GenRedOpt import Futhark.Optimise.HistAccs @@ -130,7 +129,6 @@ >>> passes [ performCSE False, simplifySeqMem, - entryPointMemSeq, simplifySeqMem, LiftAllocations.liftAllocationsSeqMem, simplifySeqMem, @@ -152,7 +150,6 @@ [ simplifyGPUMem, performCSE False, simplifyGPUMem, - entryPointMemGPU, doubleBufferGPU, simplifyGPUMem, performCSE False, @@ -197,7 +194,6 @@ [ simplifyMCMem, performCSE False, simplifyMCMem, - entryPointMemMC, doubleBufferMC, simplifyMCMem, performCSE False, diff --git a/src/Futhark/Test.hs b/src/Futhark/Test.hs --- 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 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 --- /dev/null +++ b/src/Futhark/Test/Property.hs @@ -0,0 +1,1048 @@ +{-# LANGUAGE LambdaCase #-} + +module Futhark.Test.Property + ( runPBT, + PBTConfig (..), + PBTPhase (..), + PropSpec (..), + PBTOutput, + PBTFailure, + extractPropSpecs, + ) +where + +import Control.Exception +import Control.Monad +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.Trans.Except +import Data.Either (fromRight, partitionEithers) +import Data.IORef +import Data.Int +import Data.List qualified as L +import Data.Maybe (catMaybes, fromMaybe, mapMaybe) +import Data.Text qualified as T +import Data.Word (Word64) +import Futhark.Data +import Futhark.Server +import Futhark.Server.Values qualified as FSV +import Futhark.Test.Values + ( RandomConfiguration (..), + initialRandomConfiguration, + randomValue, + ) +import Futhark.Util (showText) +import System.FilePath (dropExtension) +import System.Random (StdGen, mkStdGen, random) +import System.Random.Stateful (IOGenM (..), applyIOGen, newIOGenM) + +-- | Configuration for property-based testing. +-- Includes parameters for test case generation, shrinking, and random seed management. +data PBTConfig = PBTConfig + { -- | Number of test cases to run for each property. + configNumTests :: Int32, + -- | Maximum size argument to pass to generators and shrinkers (unless + -- overridden by PropSpec). + configMaxSize :: Int64, + -- | Seed to use for the random number generator (can be overridden by PropSpec). + configSeed :: Word64, + -- | Number of shrinking attempts to make on userdefined shrinker before + -- giving up and reporting the current candidate as the final + -- counterexample. + configShrinkTries :: Int + } + deriving (Show, Eq) + +-- | Specification for a property to be tested, including the property entry point and +-- optional generator and shrinker entry points, as well as an optional size parameter. +data PropSpec = PropSpec + { -- | The property entry point to test. + psProp :: T.Text, + -- | Optional generator entry point to use instead of the default + -- auto-generator. + psGen :: Maybe T.Text, + -- | Optional shrinker entry point to use instead of the default + -- auto-shrinker. + psShrink :: Maybe T.Text, + -- | Optional size argument to pass to the generator and shrinker phases + -- (overrides 'configMaxSize'). + psSize :: Maybe Int64 + } + deriving (Show, Eq) + +-- | Information about the current phase of property-based testing, +-- used for logging and debugging. +data PBTPhase = PBTPhase + { -- | Property being tested (same for generator and shrinker phases). + activeTest :: Maybe EntryName, + -- | Current entrypoint being called (property, generator, or shrinker). + phase :: Maybe EntryName, + -- | Property or generator (only for auto). + shrinkWith :: Maybe EntryName, + -- | Size argument for generator and shrinker phases. + phaseSize :: Maybe Int64, + -- | Seed argument for generator and shrinker phases. + phaseSeed :: Maybe Word64, + -- | Random value argument for shrinker phase (used for user-defined + -- shrinker, otherwise 'Nothing'). + phaseRandom :: Maybe Word64 + } + deriving (Show, Eq) + +-- | Output of a property-based test run, which is either a failure with +-- an error message or a success. +type PBTOutput = Maybe T.Text + +-- | Failure in property-based testing, represented as an error message. +-- For example a division by zero runtime error. +type PBTFailure = T.Text + +-- | The Haskell-level random number generator that we use for generating seeds +-- passed to generators. +type PBTGen = IOGenM StdGen + +genWord64 :: (MonadIO m) => PBTGen -> m Word64 +genWord64 = applyIOGen random + +-- | For unexcpected critical errors +unexpectedFailure :: (MonadFail m) => T.Text -> m a +unexpectedFailure msg = + fail $ + "Unexpected critical error: " + <> T.unpack msg + <> "\nProbably a bug please report as issue on the GitHub repository." + +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 = + let s = T.strip t + in if s == name + then Just "" + else T.stripSuffix ")" <=< T.stripPrefix (name <> "(") $ s + +readMaybeText :: (Read a) => T.Text -> Maybe a +readMaybeText t = + case reads (T.unpack t) of + [(x, "")] -> Just x + _ -> Nothing + +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 = fromInteger <$> lookupArgRead "size" args + } + +getPropAttrs :: T.Text -> [T.Text] -> [PropSpec] +getPropAttrs entry = mapMaybe $ parsePropSpec entry + +getInputTypes :: Server -> EntryName -> IO [TypeName] +getInputTypes srv entry = + fmap (map inputType) $ + cmdErrorHandlerE ("Failed to get input types for " <> entry <> ": ") $ + cmdInputs srv entry + +getOutputType :: Server -> EntryName -> IO TypeName +getOutputType s entry = + fmap outputType $ + cmdErrorHandlerE ("Failed to get output types for " <> entry <> ": ") $ + cmdOutput s entry + +validateGenTypes :: Server -> EntryName -> Maybe EntryName -> IO (Maybe PBTFailure) +validateGenTypes _srv _prop_name Nothing = pure Nothing +validateGenTypes srv prop_name (Just gen_name) = fmap (either Just (const Nothing)) . runExceptT $ do + gen_ins <- liftIO $ getInputTypes srv gen_name + gen_out <- liftIO $ getOutputType srv gen_name + + -- check expected output type for generator matches property input type + test_ty <- + liftIO (getSingleInputType srv prop_name) >>= \case + Left err -> throwE $ showText err + Right ty -> pure ty + + let actual_tys = gen_ins ++ [gen_out] + expected_tys = ["i64", "u64", test_ty] + + unless (actual_tys == expected_tys) $ + throwE $ + ("Generator \"" <> gen_name <> "\" for property \"" <> prop_name <> "\" has invalid type.\n") + <> ("Expected: " <> T.intercalate " -> " expected_tys <> "\n") + <> ("Actual: " <> T.intercalate " -> " actual_tys) + +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 + + -- validate input + case shrinkIns of + [xTy, randTy] -> do + let errors = + [ "Property " <> propName <> " expects " <> propTy <> " but shrinker " <> shrinkName <> " takes " <> xTy + | xTy /= propTy + ] + <> [ "Shrinker " <> shrinkName <> " takes random value " <> randTy <> " but expected u64" + | randTy /= "u64" + ] + + unless (null errors) $ + throwE $ + "Shrinker Mismatch:\n" <> T.intercalate "\n---\n" errors + tys -> + throwE $ + "Shrinker input arity mismatch.\n shrinker " + <> shrinkName + <> " inputs: " + <> showText tys + <> "\nExpected exactly 2 inputs: (" + <> propTy + <> ", u64)." + + -- validate output + shrinkOut <- liftIO $ getOutputType srv shrinkName + let isMatch = propTy == shrinkOut + + unless isMatch $ + throwE $ + "Shrinker output mismatch.\nProperty " + <> propName + <> " expects: " + <> propTy + <> "\nShrinker " + <> shrinkName + <> " returns: " + <> showText shrinkOut + <> "\nExpected shrinker output to equal the property input type." + +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 + +validateOneSpec :: Server -> [EntryName] -> PropSpec -> ExceptT PBTFailure IO () +validateOneSpec srv eps spec = do + let prop = psProp spec + + unless (prop `elem` eps) $ + throwE $ + "Property entry point not found: " <> prop + + liftIO (validatePropTypes srv prop) >>= maybe (pure ()) throwE + + genName <- case psGen spec of + Nothing -> + pure Nothing + Just g + | g `notElem` eps -> + throwE $ "Generator is not a server entry point: " <> g + Just g -> + pure $ Just g + + liftIO (validateGenTypes srv prop genName) >>= maybe (pure ()) throwE + + case psShrink spec of + Nothing -> 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 + +-- | Extract property specifications from the server by looking for entry +-- points with #[prop(...)] attributes, comparing with the declared list of properties. +extractPropSpecs :: Server -> [EntryName] -> IO (Either PBTFailure [PropSpec]) +extractPropSpecs srv properties = do + eps <- either (error . show) pure <=< liftIO $ cmdEntryPoints srv + checks <- mapM (runExceptT . getOne eps) eps + let missing = do + f <- properties + guard $ f `L.notElem` eps + pure $ Left $ "Declared as property, but is not an entry point: \"" <> f <> "\"." + case partitionEithers $ checks ++ missing of + ([], specs) -> pure $ Right $ catMaybes specs + (errors, _) -> pure $ Left $ T.intercalate "\n" errors + where + getOne eps entry = do + attrs <- + either (unexpectedFailure . showText) pure <=< liftIO $ + cmdAttributes srv entry + let specs = getPropAttrs entry attrs + is_prop = entry `elem` properties + case specs of + [spec] | is_prop -> do + validateOneSpec srv eps spec + pure $ Just spec + [] + | is_prop -> + throwE $ + "Entry point \"" + <> entry + <> "\" declared as property, but has no #[prop(...)] attribute." + | otherwise -> + pure Nothing + _ + | is_prop -> + throwE $ + "Entry point \"" + <> entry + <> "\" has more than one #[prop(...)] attribute." + | otherwise -> + throwE $ + "Entry point \"" + <> entry + <> "\" not declared as property, but has #[prop(...)] attribute." + +-- | Generate a candidate automatically. +automaticGenerator :: Server -> EntryName -> TypeName -> Int64 -> PBTGen -> IO (Maybe PBTFailure) +automaticGenerator srv candidate genTy size rng = do + kRes <- cmdErrorHandlerE "automaticGenerator cmdKind failed: " $ cmdKind srv genTy + case kRes of + Record -> do + resFields <- cmdFields srv genTy + case resFields of + Right fields -> do + let fieldVarNames = [candidate <> "_$compositeVal" <> fieldName fld | fld <- fields] + + results <- forM (zip fieldVarNames fields) $ \(fVarName, fld) -> + automaticGenerator srv fVarName (fieldType fld) size rng + + case sequence results of + Just err -> pure $ Just $ T.unlines err + Nothing -> do + freeVars srv [candidate] + cmdErrorHandlerM ("Failed to pack record " <> candidate <> ": ") $ + cmdNew srv candidate genTy fieldVarNames + + freeVars srv fieldVarNames + pure Nothing + Left err -> pure $ Just $ showText err + Array -> do + (dimCount, baseTy) <- getArrayDimsAndBase srv genTy + baseKind <- cmdErrorHandlerE "automaticGenerator base cmdKind failed: " $ cmdKind srv baseTy + case baseKind of + Record -> do + resFields <- cmdFields srv baseTy + case resFields of + Right fields -> do + let fieldVarNames = [candidate <> "_$compositeArr_" <> fieldName fld | fld <- fields] + + results <- forM (zip fieldVarNames fields) $ \(fVarName, fld) -> do + (innerDimCount, innerBaseTy) <- getArrayDimsAndBase srv (fieldType fld) + let totalDimCount = dimCount + innerDimCount + fArrTy = T.replicate totalDimCount "[]" <> innerBaseTy + automaticGenerator srv fVarName fArrTy size rng + + case sequence results of + Just err -> pure $ Just $ T.unlines err + Nothing -> do + freeVars srv [candidate] + cmdErrorHandlerM ("Failed to zip array of records " <> candidate <> ": ") $ + cmdZip srv candidate genTy fieldVarNames + + freeVars srv fieldVarNames + pure Nothing + Left err -> pure $ Just $ showText err + _ -> do + let shapeList = replicate dimCount size + seed <- genWord64 rng + case makeFutPrimitiveValue baseTy shapeList seed of + Right val -> do + freeVars srv [candidate] + putRes <- FSV.putValue srv candidate val + case putRes of + Nothing -> pure Nothing + Just err -> pure $ Just $ showText err + Left err -> pure $ Just err + _ -> do + seed <- genWord64 rng + case makeFutPrimitiveValue genTy [] seed of + Right val -> do + freeVars srv [candidate] + putRes <- FSV.putValue srv candidate val + case putRes of + Nothing -> pure Nothing + Just err -> pure $ Just $ showText err + Left _ -> do + let genName = "gen_" <> genTy + szVar = candidate <> "_$size" + sdVar = candidate <> "_$seed" + + putVal srv szVar size + putVal srv sdVar seed + + callFreeIns srv genName candidate [szVar, sdVar] + +-- | Recursively unwrap arrays using the Futhark server to handle type aliases dynamically. +getArrayDimsAndBase :: Server -> TypeName -> IO (Int, TypeName) +getArrayDimsAndBase srv t + | "[]" `T.isPrefixOf` t = do + (d, base) <- getArrayDimsAndBase srv (T.drop 2 t) + pure (d + 1, base) + | otherwise = do + kRes <- cmdKind srv t + case kRes of + Right Array -> do + etRes <- cmdElemtype srv t + case etRes of + Right et -> do + (d, base) <- getArrayDimsAndBase srv et + pure (d + 1, base) + Left _ -> pure (0, t) -- Fallback if server fails to resolve elemtype + _ -> pure (0, t) + +makeFutPrimitiveValue :: TypeName -> [Int64] -> Word64 -> Either PBTFailure Value +makeFutPrimitiveValue ty shape seed = + case ty of + "i8" -> Right $ randomValue cfg (ValueType shape' I8) seed + "i16" -> Right $ randomValue cfg (ValueType shape' I16) seed + "i32" -> Right $ randomValue cfg (ValueType shape' I32) seed + "i64" -> Right $ randomValue cfg (ValueType shape' I64) seed + "u8" -> Right $ randomValue cfg (ValueType shape' U8) seed + "u16" -> Right $ randomValue cfg (ValueType shape' U16) seed + "u32" -> Right $ randomValue cfg (ValueType shape' U32) seed + "u64" -> Right $ randomValue cfg (ValueType shape' U64) seed + "f16" -> Right $ randomValue cfg (ValueType shape' F16) seed + "f32" -> Right $ randomValue cfg (ValueType shape' F32) seed + "f64" -> Right $ randomValue cfg (ValueType shape' F64) seed + "bool" -> Right $ randomValue cfg (ValueType shape' Bool) seed + _ -> Left ("Automatic generation not implemented for: " <> ty) + where + shape' = map fromIntegral shape + cfg = initialRandomConfiguration {f32Range = (-1, 1)} + +runOne :: PropSpec -> PBTConfig -> Server -> IORef PBTPhase -> FilePath -> IO (Either PBTFailure PBTOutput) +runOne s config srv entryNameRef program = runExceptT $ do + rng <- newIOGenM $ mkStdGen $ fromIntegral $ configSeed config + let loop i + | i >= numTests = pure Nothing + | otherwise = check (i + 1) + check i = do + seed <- genWord64 rng + let runUpdate ph = + liftIO $ + updatePhase + (Just propName) + (Just ph) + Nothing + (Just size) + Nothing + Nothing + entryNameRef + + generatorCandidateM <- liftIO $ generatorPhase seed + maybe (pure ()) throwE generatorCandidateM + + runUpdate propName + + okE <- + liftIO $ withCallKeepIns srv propName serverOk [serverIn] $ getVal srv + ok <- case okE of + Right b -> pure b + Left err -> do + liftIO $ + cmdErrorHandlerM "cmdStore failed to store when property crashed" $ + cmdStore srv propertyFileName [serverIn] + valuePPrint <- liftIO pPrintPhase + throwE $ + "Property " + <> propName + <> " failed with candidate=" + <> valuePPrint + <> " with error: " + <> err + if ok + then loop i + else do + let failmsg = + "PBT FAIL: " + <> propName + <> " size=" + <> showText size + <> " seed=" + <> showText (configSeed config) + <> " after " + <> showText i + <> " tests\n" + + shrinkRes <- case psShrink s of + Nothing -> + liftIO $ + autoShrinkLoop + srv + propName + genName + serverIn + size + seed + serverSize + serverSeed + entryNameRef + Just sh -> do + userShrinkRes <- + liftIO $ + shrinkLoop + srv + propName + serverIn + sh + rng + (configShrinkTries config) + entryNameRef + + case userShrinkRes of + Right Nothing -> + pure (Right Nothing) + Right (Just err) -> do + autoRes <- + liftIO $ + autoShrinkLoop + srv + propName + genName + serverIn + size + seed + serverSize + serverSeed + entryNameRef + + pure $ + Right $ + Just $ + "User shrinker failed: " + <> err + <> "\nAttempted auto-shrinker fallback." + <> formatAutoShrinkResult autoRes + Left err -> do + autoRes <- + liftIO $ + autoShrinkLoop + srv + propName + genName + serverIn + size + seed + serverSize + serverSeed + entryNameRef + + pure $ + Right $ + Just $ + "User shrinker failed: " + <> err + <> "\nAttempted auto-shrinker fallback." + <> formatAutoShrinkResult autoRes + + case shrinkRes of + Left err -> do + runUpdate "prettyPrint" + counterLog <- liftIO pPrintPhase + liftIO $ cmdErrorHandlerM "cmdStore failed to store when shrinker crashed" $ cmdStore srv propertyFileName [serverIn] + pure $ + Just $ + failmsg + <> "Shrinking failed: " + <> err + <> "\nCounterexample: " + <> counterLog + Right (Just note) -> do + runUpdate "prettyPrint" + counterLog <- liftIO pPrintPhase + pure $ + Just $ + failmsg + <> "Shrinking note: " + <> note + <> "\nCounterexample: " + <> counterLog + Right Nothing -> do + runUpdate "prettyPrint" + counterLog <- liftIO pPrintPhase + liftIO $ + cmdErrorHandlerM "cmdStore failed to store shrinker result" $ + cmdStore srv propertyFileName [serverIn] + pure $ Just $ failmsg <> "Counterexample: " <> counterLog + loop 0 + where + propName = psProp s + genName = psGen s + size = fromMaybe (configMaxSize config) (psSize s) + numTests = configNumTests config + serverSize = "runPBT_size" + serverSeed = "runPBT_seed" + serverIn = "runPBT_input" + serverOk = "runPBT_ok" + propertyFileName = + dropExtension program <> "_" <> T.unpack propName <> ".counterexample" + + generatorPhase seed = do + let runUpdate ph = + liftIO $ + updatePhase + (Just propName) + (Just ph) + Nothing + (Just size) + (Just seed) + Nothing + entryNameRef + case genName of + Nothing -> fmap (either Just (const Nothing)) . runExceptT $ do + liftIO $ freeVars srv [serverIn] + propType <- + liftIO (getSingleInputType srv propName) >>= \case + Left err -> throwE $ showText err + Right ty -> pure ty + + rng <- newIOGenM $ mkStdGen $ fromIntegral seed + errM <- liftIO $ automaticGenerator srv serverIn propType size rng + maybe (pure ()) (throwE . ("Automatic generator failed: " <>)) errM + Just gn -> fmap (either Just (const Nothing)) . runExceptT $ do + runUpdate "User Generator" + liftIO $ putVal srv serverSize size + liftIO $ putVal srv serverSeed seed + + let genOut = outName gn + + ExceptT $ withFreedVars srv [genOut] $ runExceptT $ do + liftIO (callFreeIns srv gn genOut [serverSize, serverSeed]) >>= \case + Nothing -> pure () + Just err -> do + liftIO $ putVal srv serverSize size >> putVal srv serverSeed seed + liftIO $ + cmdErrorHandlerM "cmdStore failed to store generator error: " $ + cmdStore srv propertyFileName [serverSize, serverSeed] + liftIO $ freeVars srv [serverSize, serverSeed] + throwE $ + "User Generator " + <> gn + <> " failed with size=" + <> showText size + <> " and seed=" + <> showText seed + <> " with error: " + <> err + + liftIO $ renameVar srv serverIn genOut + + pPrintPhase = do + inputTypes <- getInputTypes srv propName + case inputTypes of + [] -> pure "Could not retrieve input type for counterexample." + ty0 : _ -> prettyVar srv serverIn ty0 + +formatAutoShrinkResult :: Either PBTFailure PBTOutput -> T.Text +formatAutoShrinkResult autoRes = + case autoRes of + Right Nothing -> + "\nAuto-shrinker fallback completed." + Right (Just msg) -> + "\nAuto-shrinker fallback completed with note: " <> msg + Left autoErr -> + "\nAuto-shrinker fallback also failed: " <> autoErr + +updatePhase :: + Maybe EntryName -> + Maybe EntryName -> + Maybe EntryName -> + Maybe Int64 -> + Maybe Word64 -> + Maybe Word64 -> + IORef PBTPhase -> + IO () +updatePhase propName phase activeTest size seed rand phaseRef = + writeIORef phaseRef $ + PBTPhase + { activeTest = propName, + phase = phase, + shrinkWith = activeTest, + phaseSize = size, + phaseSeed = seed, + phaseRandom = rand + } + +-- Given a known counterexample (generated with provided size and seed), here we +-- try to find a smaller counterexample by decreasing the size (but using the +-- same seed) until the generated value stops being a counterexample. +-- +-- XXX: currently the automatic generator does not reuse the seed, but creates a +-- new PBTGen from it. +autoShrinkLoop :: + Server -> + EntryName -> + Maybe EntryName -> + VarName -> + Int64 -> + Word64 -> + VarName -> + VarName -> + IORef PBTPhase -> + IO (Either PBTFailure PBTOutput) +autoShrinkLoop srv propName genName vCounterExample size seed serverSize serverSeed phaseRef = runExceptT $ do + let loop i + | i <= 1 = pure Nothing + | otherwise = do + let newSize = i - 1 + + errM <- liftIO $ generatorPhase newSize + maybe (pure ()) (throwE . ("Auto-shrinker generator failed: " <>)) errM + + liftIO $ autoShrinkUpdatePhase (Right $ Just propName) + + ok <- + either (throwE . ("Property " <>)) pure <=< liftIO $ + withCallKeepIns srv propName vOk [vCandidate] $ + getVal srv + + liftIO $ autoShrinkUpdatePhase (Left Nothing) + + case ok of + True -> do + liftIO $ freeVars srv [vCandidate] + loop newSize + False -> do + liftIO $ + freeOnException srv [vCounterExample] $ + renameVar srv vCounterExample vCandidate + loop newSize + loop size + where + vCandidate = "auto_shrink_candidate" + vOk = "auto_shrink_ok" + autoShrinkUpdatePhase active = + liftIO $ + updatePhase + (Just propName) + (Just "autoShrinkLoop") + (fromRight (Just "Automatic generator") active) + (Just size) + (Just seed) + Nothing + phaseRef + generatorPhase size' = do + fmap (either Just (const Nothing)) . runExceptT $ + case genName of + Nothing -> do + propertyType <- do + liftIO (getSingleInputType srv propName) >>= \case + Left err -> throwE $ showText err + Right ty -> pure ty + liftIO $ freeVars srv [serverSize, serverSeed] + runExceptT $ do + rng <- newIOGenM $ mkStdGen $ fromIntegral seed + errM <- liftIO $ automaticGenerator srv vCandidate propertyType size' rng + maybe (pure ()) (throwE . ("Automatic generator failed: " <>)) errM + Just gn -> do + liftIO $ putVal srv serverSize size' >> putVal srv serverSeed seed + runExceptT $ do + errM <- liftIO $ callFreeIns srv gn vCandidate [serverSize, serverSeed] + maybe (pure ()) (\err -> throwE $ "User Generator " <> gn <> " failed: " <> err) errM + +data Step + = -- | Property still failed with the new candidate + AcceptedShrink + | -- | Property passed with the new candidate + NotAcceptedShrink + | -- | Shrinker error (including property failure in shrinker) + ErrorInShrink T.Text + deriving (Eq, Show) + +shrinkLoop :: Server -> EntryName -> VarName -> EntryName -> PBTGen -> Int -> IORef PBTPhase -> IO (Either PBTFailure PBTOutput) +shrinkLoop srv propName counterExample shrinkName rng 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) + Nothing + Nothing + phaseRef + + shrinkUpdatePhase Nothing + + let loop (acc :: Int) (totalCounter :: Int) + | acc >= numTries = pure Nothing + | otherwise = do + random_value <- genWord64 rng + stepResultE <- liftIO $ oneStep size random_value + stepResult <- + either + ( \err -> + throwE $ + "Error in shrinker " + <> shrinkName + <> " with random=" + <> showText random_value + <> ": " + <> err + ) + pure + stepResultE + + case stepResult of + AcceptedShrink -> + loop 0 (totalCounter + 1) -- Reset trials on success + NotAcceptedShrink -> + loop (acc + 1) (totalCounter + 1) -- Increment trials + ErrorInShrink err -> + throwE $ "Error in shrinker: " <> err + loop 0 0 + where + oneStep size (val :: Word64) = do + let vCandidate = "shrink_candidate" + vOk = "shrink_ok" + vRandomValue = "shrink_random" + + let shrinkUpdatePhase activeTest randomNum = + updatePhase + (Just propName) + (Just shrinkName) + activeTest + (Just size) + Nothing + randomNum + phaseRef + + freeVars srv [vRandomValue] + putVal srv vRandomValue val + + shrinkUpdatePhase Nothing $ Just val + + withFreedVar srv vCandidate $ runExceptT $ do + errE <- liftIO $ callKeepIns srv shrinkName vCandidate [counterExample, vRandomValue] + liftIO $ freeVars srv [vRandomValue] + maybe (pure ()) (throwE . ((shrinkName <> " has ") <>)) errE + + liftIO $ shrinkUpdatePhase Nothing $ Just $ fromIntegral val + + ok <- + either (throwE . ("Property " <>)) pure <=< liftIO $ + withCallKeepIns srv propName vOk [vCandidate] $ + getVal srv + + liftIO $ shrinkUpdatePhase Nothing $ Just $ fromIntegral val + + case ok of + True -> pure NotAcceptedShrink + False -> do + liftIO $ renameVar srv counterExample vCandidate + pure AcceptedShrink + +-- | 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 -> + unexpectedFailure $ + "cmdFree failed for " + <> showText vs + <> ": " + <> showText (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 = + unexpectedFailure $ + "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] + +renameVar :: Server -> VarName -> VarName -> IO () +renameVar srv new old = do + freeVars srv [new] + cmdErrorHandlerM "cmdRename failed: " $ cmdRename srv old new + +cmdErrorHandlerM :: T.Text -> IO (Maybe CmdFailure) -> IO () +cmdErrorHandlerM msg action = action >>= maybe (pure ()) (unexpectedFailure . format) + where + format err = msg <> showText err + +cmdErrorHandlerE :: T.Text -> IO (Either CmdFailure a) -> IO a +cmdErrorHandlerE msg action = action >>= either (unexpectedFailure . format) pure + where + format err = msg <> showText 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 -> + unexpectedFailure $ + "Expected " + <> name + <> " to decode, got: " + <> valueText v + +getDataVal :: Server -> VarName -> IO Value +getDataVal s name = do + r <- FSV.getValue s name + case r of + Left msg -> + unexpectedFailure $ + "getValue failed for " + <> name + <> ": " + <> msg + Right v -> pure v + +prettyVar :: Server -> VarName -> TypeName -> IO T.Text +prettyVar srv v ty = do + kRes <- cmdErrorHandlerE "cmdKind failed: " $ cmdKind srv ty + case kRes of + Record -> do + fieldsRes <- cmdFields srv ty + case fieldsRes of + Right fieldLines -> do + let fnames = map fieldName fieldLines + ftypes = map fieldType fieldLines + isTuple = all (\(n, i :: Int) -> n == showText i) (zip fnames [0 ..]) + + rendered <- forM (zip fnames ftypes) $ \(fname, fty) -> do + let tmp = v <> "_proj_" <> fname + sField <- withFreedVar srv tmp $ do + cmdErrorHandlerM "project failed: " $ cmdProject srv tmp v fname + prettyVar srv tmp fty + pure $ if isTuple then sField else fname <> " = " <> sField + + pure $ + if isTuple + then "(" <> T.intercalate ", " rendered <> ")" + else "{" <> T.intercalate ", " rendered <> "}" + Left _ -> pure "" + Array -> do + valRes <- FSV.getValue srv v + case valRes of + Right val -> pure (valueText val) + Left _ -> do + dims <- cmdErrorHandlerE "cmdShape failed: " $ cmdShape srv v + baseTy <- getBaseType ty + buildNested v baseTy dims [] + _ -> fallbackValue + where + fallbackValue = do + valRes <- FSV.getValue srv v + case valRes of + Right val -> pure (valueText val) + Left _ -> pure (" ty <> ">") + + getBaseType :: TypeName -> IO TypeName + getBaseType t = do + k <- cmdErrorHandlerE "cmdKind failed: " $ cmdKind srv t + case k of + Array -> do + et <- cmdErrorHandlerE "cmdElemtype failed: " $ cmdElemtype srv t + getBaseType et + _ -> pure t + + buildNested :: VarName -> TypeName -> [Int] -> [Int] -> IO T.Text + buildNested varName baseType dims currentPath = + case dims of + [] -> do + let pathStr = T.intercalate "_" (map showText currentPath) + tmpElem = varName <> "_elem_" <> pathStr + + withFreedVar srv tmpElem $ do + cmdErrorHandlerM "index failed: " $ cmdIndex srv tmpElem varName currentPath + prettyVar srv tmpElem baseType + (d : restDims) -> do + elements <- forM [0 .. d - 1] $ \idx -> do + buildNested varName baseType restDims (currentPath ++ [idx]) + + pure $ "[" <> T.intercalate ", " elements <> "]" + +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 + +-- | Run a list of property specifications, returning a list of results. +-- Each result is either a failure with an error message or a success. +runPBT :: PBTConfig -> Server -> [PropSpec] -> IORef PBTPhase -> FilePath -> IO [Either PBTFailure PBTOutput] +runPBT config srv specs entryNameRef program = + forM specs $ \spec -> + runOne spec config srv entryNameRef program diff --git a/src/Futhark/Test/Spec.hs b/src/Futhark/Test/Spec.hs --- a/src/Futhark/Test/Spec.hs +++ b/src/Futhark/Test/Spec.hs @@ -13,6 +13,7 @@ TestAction (..), ExpectedError (..), InputOutputs (..), + PropertyCase (..), TestRun (..), ExpectedResult (..), Success (..), @@ -26,6 +27,7 @@ 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 @@ -- | 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 @@ } deriving (Show) +newtype PropertyCase = PropertyCase + {propertyEntryPoint :: T.Text} + deriving (Show) + -- | The error expected for a negative test. data ExpectedError = AnyError @@ -217,12 +223,33 @@ 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 + entryss <- some (parseEntryPointsProp sep) + pure $ map PropertyCase (concat entryss) + +parseEntryPointsProp :: Parser () -> Parser [T.Text] +parseEntryPointsProp sep = + lexeme' "property:" *> some entry <* sep + where + constituent c = not (isSpace c) + entry = lexeme' $ takeWhile1P Nothing constituent + parseInputOutputs :: Parser () -> Parser [InputOutputs] parseInputOutputs sep = do entrys <- parseEntryPoints sep @@ -382,9 +409,19 @@ 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 +433,23 @@ 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 = - "--" *> sep *> parseDescription sep *> parseInputOutputs sep <* pEndOfTestBlock + 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/src/Futhark/Test/Values.hs b/src/Futhark/Test/Values.hs --- a/src/Futhark/Test/Values.hs +++ b/src/Futhark/Test/Values.hs @@ -11,16 +11,30 @@ CompoundValue, mkCompound, unCompound, + + -- * Random value generation + Range, + RandomConfiguration (..), + initialRandomConfiguration, + randomValue, ) where +import Control.Monad.ST +import Data.Int import Data.Map qualified as M import Data.Text qualified as T import Data.Traversable +import Data.Vector.Storable qualified as SVec +import Data.Vector.Storable.Mutable qualified as USVec +import Data.Word import Futhark.Data import Futhark.Data.Compare import Futhark.Data.Reader -import Futhark.Util.Pretty +import Futhark.Util (convFloat) +import Futhark.Util.Pretty (Pretty (..), braces, commasep, equals, parens) +import Numeric.Half +import System.Random.Stateful (UniformRange (..), mkStdGen, uniformR) instance Pretty Value where pretty = pretty . valueText @@ -70,3 +84,84 @@ -- supported by raw values. You cannot parse or read these in -- standard ways, and they cannot be elements of arrays. type CompoundValue = Compound Value + +randomVector :: + (SVec.Storable v, UniformRange v) => + Range v -> + (SVec.Vector Int -> SVec.Vector v -> Value) -> + [Int] -> + Word64 -> + Value +randomVector range final ds seed = runST $ do + -- Use some nice impure computation where we can preallocate a + -- vector of the desired size, populate it via the random number + -- generator, and then finally reutrn a frozen binary vector. + arr <- USVec.new n + let fill g i + | i < n = do + let (v, g') = uniformR range g + USVec.write arr i v + g' `seq` fill g' $! i + 1 + | otherwise = + pure () + fill (mkStdGen $ fromIntegral seed) 0 + final (SVec.fromList ds) . SVec.convert <$> SVec.freeze arr + where + n = product ds + +-- XXX: The following instance is an orphan. Maybe it could be +-- avoided with some newtype trickery or refactoring, but it's so +-- convenient this way. +instance UniformRange Half where + uniformRM (a, b) g = + (convFloat :: Float -> Half) <$> uniformRM (convFloat a, convFloat b) g + +-- | Closed interval, as in @System.Random@. +type Range a = (a, a) + +data RandomConfiguration = RandomConfiguration + { i8Range :: Range Int8, + i16Range :: Range Int16, + i32Range :: Range Int32, + i64Range :: Range Int64, + u8Range :: Range Word8, + u16Range :: Range Word16, + u32Range :: Range Word32, + u64Range :: Range Word64, + f16Range :: Range Half, + f32Range :: Range Float, + f64Range :: Range Double + } + +initialRandomConfiguration :: RandomConfiguration +initialRandomConfiguration = + RandomConfiguration + (minBound, maxBound) + (minBound, maxBound) + (minBound, maxBound) + (minBound, maxBound) + (minBound, maxBound) + (minBound, maxBound) + (minBound, maxBound) + (minBound, maxBound) + (0.0, 1.0) + (0.0, 1.0) + (0.0, 1.0) + +randomValue :: RandomConfiguration -> ValueType -> Word64 -> Value +randomValue conf (ValueType ds t) seed = + case t of + I8 -> gen i8Range I8Value + I16 -> gen i16Range I16Value + I32 -> gen i32Range I32Value + I64 -> gen i64Range I64Value + U8 -> gen u8Range U8Value + U16 -> gen u16Range U16Value + U32 -> gen u32Range U32Value + U64 -> gen u64Range U64Value + F16 -> gen f16Range F16Value + F32 -> gen f32Range F32Value + F64 -> gen f64Range F64Value + Bool -> gen (const (False, True)) BoolValue + where + gen range final = randomVector (range conf) final ds seed diff --git a/src/Futhark/Util.hs b/src/Futhark/Util.hs --- a/src/Futhark/Util.hs +++ b/src/Futhark/Util.hs @@ -31,6 +31,7 @@ showText, unixEnvironment, isEnvVarAtLeast, + randomSeed, startupTime, fancyTerminal, hFancyTerminal, @@ -81,6 +82,7 @@ import Data.Text.IO qualified as T import Data.Time.Clock (UTCTime, getCurrentTime) import Data.Tuple (swap) +import Data.Word (Word64) import Debug.Trace import Numeric import System.Directory (createDirectoryIfMissing, listDirectory) @@ -94,6 +96,7 @@ import System.IO.Error (isAlreadyInUseError, isDoesNotExistError) import System.IO.Unsafe import System.Process.ByteString +import System.Random (randomIO) import Text.Read (readMaybe) -- | Like @nub@, but without the quadratic runtime. @@ -249,6 +252,13 @@ case readMaybe =<< lookup s unixEnvironment of Just y -> y >= x _ -> False + +{-# NOINLINE randomSeed #-} + +-- | A random number generated at startup. Can be used to produce different +-- behaviour whenever the program is run. +randomSeed :: Word64 +randomSeed = unsafePerformIO randomIO {-# NOINLINE startupTime #-} diff --git a/src/Language/Futhark/Interpreter.hs b/src/Language/Futhark/Interpreter.hs --- a/src/Language/Futhark/Interpreter.hs +++ b/src/Language/Futhark/Interpreter.hs @@ -985,11 +985,9 @@ eval env (Hole (Info t) loc) = bad loc env $ "Hole of type: " <> prettyTextOneLine t eval env (Parens e _) = eval env e -eval env (QualParens (qv, _) e loc) = do - m <- evalModuleVar env qv - case m of - ModuleFun {} -> error $ "Local open of module function at " ++ locStr loc - Module m' -> eval (m' <> env) e +eval env (QualParens _ e _) = + -- Already handled by the names added by the type checker. + eval env e eval env (TupLit vs _) = toTuple <$> mapM (eval env) vs eval env (RecordLit fields _) = ValueRecord . M.fromList <$> mapM evalField fields diff --git a/src/Language/Futhark/Prop.hs b/src/Language/Futhark/Prop.hs --- a/src/Language/Futhark/Prop.hs +++ b/src/Language/Futhark/Prop.hs @@ -54,6 +54,7 @@ orderZero, unfoldFunType, foldFunType, + typeQualVars, typeVars, isAccType, @@ -553,20 +554,24 @@ [] -> retDims (unInfo (valBindRetType vb)) _ -> [] --- | The type names mentioned in a type. -typeVars :: TypeBase dim as -> S.Set VName -typeVars t = +-- | The qualified type names mentioned in a type. +typeQualVars :: TypeBase dim as -> [QualName VName] +typeQualVars t = case t of Scalar Prim {} -> mempty Scalar (TypeVar _ tn targs) -> - mconcat $ S.singleton (qualLeaf tn) : map typeArgFree targs - Scalar (Arrow _ _ _ t1 (RetType _ t2)) -> typeVars t1 <> typeVars t2 - Scalar (Record fields) -> foldMap typeVars fields - Scalar (Sum cs) -> mconcat $ (foldMap . fmap) typeVars cs - Array _ _ rt -> typeVars $ Scalar rt + tn : concatMap typeArgFree targs + Scalar (Arrow _ _ _ t1 (RetType _ t2)) -> typeQualVars t1 <> typeQualVars t2 + Scalar (Record fields) -> foldMap typeQualVars fields + Scalar (Sum cs) -> mconcat $ (foldMap . fmap) typeQualVars cs + Array _ _ rt -> typeQualVars $ Scalar rt where - typeArgFree (TypeArgType ta) = typeVars ta + typeArgFree (TypeArgType ta) = typeQualVars ta typeArgFree TypeArgDim {} = mempty + +-- | The type names mentioned in a type. +typeVars :: TypeBase dim as -> S.Set VName +typeVars = S.fromList . map qualLeaf . typeQualVars -- | @orderZero t@ is 'True' if the argument type has order 0, i.e., it is not -- a function type, does not contain a function type as a subcomponent, and may diff --git a/src/Language/Futhark/TypeChecker.hs b/src/Language/Futhark/TypeChecker.hs --- a/src/Language/Futhark/TypeChecker.hs +++ b/src/Language/Futhark/TypeChecker.hs @@ -37,6 +37,9 @@ import Language.Futhark.TypeChecker.Types import Prelude hiding (abs, mod) +importTable :: Imports -> ImportTable +importTable = M.map (\f -> (fileAbs f, fileEnv f)) . M.fromList + --- The main checker -- | Type check a program containing no type information, yielding @@ -53,7 +56,7 @@ checkProg files src name prog = runTypeM initialEnv files' name src $ checkProgM prog where - files' = M.map fileEnv $ M.fromList files + files' = importTable files -- | Type check a single expression containing no type information, -- yielding either a type error or the same expression annotated with @@ -75,7 +78,7 @@ src (checkOneExp =<< resolveExp e) where - files' = M.map fileEnv $ M.fromList files + files' = importTable files -- | Type check a single declaration containing no type information, -- yielding either a type error or the same declaration annotated with @@ -91,12 +94,12 @@ checkDec files src env name d = second (fmap massage) $ runTypeM env files' name src $ do - (_, env', d') <- checkOneDec d + (env', d') <- checkOneDec d pure (env' <> env, d') where massage ((env', d'), src') = (env', d', src') - files' = M.map fileEnv $ M.fromList files + files' = importTable files -- | Type check a single module expression containing no type information, -- yielding either a type error or the same expression annotated with @@ -109,11 +112,10 @@ ModExpBase NoInfo Name -> (Warnings, Either TypeError (MTy, ModExpBase Info VName)) checkModExp files src env me = - second (fmap fst) . runTypeM env files' (mkInitialImport "") src $ do - (_abs, mty, me') <- checkOneModExp me - pure (mty, me') + second (fmap fst) . runTypeM env files' (mkInitialImport "") src $ + checkOneModExp me where - files' = M.map fileEnv $ M.fromList files + files' = importTable files -- | An initial environment for the type checker, containing -- intrinsics and such. @@ -150,7 +152,7 @@ checkProgM :: UncheckedProg -> TypeM FileModule checkProgM (Prog doc decs) = do checkForDuplicateDecs decs - (abs, env, decs', full_env) <- checkDecs decs + ((env, decs', full_env), abs) <- collectTySet $ checkDecs decs pure (FileModule abs env (Prog doc decs') full_env) dupDefinitionError :: @@ -283,7 +285,7 @@ TypeSpec l name' ps' doc loc : specs' ) checkSpecs (ModSpec name sig doc loc : specs) = do - (_sig_abs, mty, sig') <- checkModTypeExp sig + (mty, sig') <- checkModTypeExp sig bindSpaced1 Term name loc $ \name' -> do usedName name' let senv = @@ -298,13 +300,13 @@ ModSpec name' sig' doc loc : specs' ) checkSpecs (IncludeSpec e loc : specs) = do - (e_abs, env_abs, e_env, e') <- checkModTypeExpToEnv e + (env_abs, e_env, e') <- checkModTypeExpToEnv e mapM_ warnIfShadowing $ M.keys env_abs (abstypes, env, specs') <- localEnv e_env $ checkSpecs specs pure - ( e_abs <> env_abs <> abstypes, + ( env_abs <> abstypes, env <> e_env, IncludeSpec e' loc : specs' ) @@ -315,28 +317,28 @@ warnAbout qn = warn loc $ "Inclusion shadows type" <+> dquotes (pretty qn) <> "." -checkModTypeExp :: ModTypeExpBase NoInfo Name -> TypeM (TySet, MTy, ModTypeExpBase Info VName) +checkModTypeExp :: ModTypeExpBase NoInfo Name -> TypeM (MTy, ModTypeExpBase Info VName) checkModTypeExp (ModTypeParens e loc) = do - (abs, mty, e') <- checkModTypeExp e - pure (abs, mty, ModTypeParens e' loc) + (mty, e') <- checkModTypeExp e + pure (mty, ModTypeParens e' loc) checkModTypeExp (ModTypeVar name NoInfo loc) = do (name', mty) <- lookupMTy loc name (mty', substs) <- newNamesForMTy mty - pure (mtyAbs mty', mty', ModTypeVar name' (Info substs) loc) + pure (mty', ModTypeVar name' (Info substs) loc) checkModTypeExp (ModTypeSpecs specs loc) = do checkForDuplicateSpecs specs - (abstypes, env, specs') <- checkSpecs specs - pure (abstypes, MTy abstypes $ ModEnv env, ModTypeSpecs specs' loc) + (abs, env, specs') <- checkSpecs specs + pure (MTy abs $ ModEnv env, ModTypeSpecs specs' loc) checkModTypeExp (ModTypeWith s (TypeRef tname ps te trloc) loc) = do - (abs, s_abs, s_env, s') <- checkModTypeExpToEnv s + (s_abs, s_env, s') <- checkModTypeExpToEnv s resolveTypeParams ps $ \ps' -> do (ext, te', te_t, _) <- bindingTypeParams ps' $ checkTypeDecl te (tname', s_abs', s_env') <- refineEnv loc s_abs s_env tname ps' $ RetType ext te_t - pure (abs, MTy s_abs' $ ModEnv s_env', ModTypeWith s' (TypeRef tname' ps' te' trloc) loc) + pure (MTy s_abs' $ ModEnv s_env', ModTypeWith s' (TypeRef tname' ps' te' trloc) loc) checkModTypeExp (ModTypeArrow maybe_pname e1 e2 loc) = do - (e1_abs, MTy s_abs e1_mod, e1') <- checkModTypeExp e1 - (maybe_pname', (e2_abs, e2_mod, e2')) <- + (MTy s_abs e1_mod, e1') <- checkModTypeExp e1 + (maybe_pname', (e2_mod, e2')) <- case maybe_pname of Just pname -> bindSpaced1 Term pname loc $ \pname' -> localEnv (mempty {envModTable = M.singleton pname' e1_mod}) $ @@ -344,29 +346,28 @@ Nothing -> (Nothing,) <$> checkModTypeExp e2 pure - ( e1_abs <> e2_abs, - MTy mempty $ ModFun $ FunModType s_abs e1_mod e2_mod, + ( MTy mempty $ ModFun $ FunModType s_abs e1_mod e2_mod, ModTypeArrow maybe_pname' e1' e2' loc ) checkModTypeExpToEnv :: ModTypeExpBase NoInfo Name -> - TypeM (TySet, TySet, Env, ModTypeExpBase Info VName) + TypeM (TySet, Env, ModTypeExpBase Info VName) checkModTypeExpToEnv e = do - (abs, MTy mod_abs mod, e') <- checkModTypeExp e + (MTy mod_abs mod, e') <- checkModTypeExp e case mod of - ModEnv env -> pure (abs, mod_abs, env, e') + ModEnv env -> pure (mod_abs, env, e') ModFun {} -> unappliedFunctor $ srclocOf e -checkModTypeBind :: ModTypeBindBase NoInfo Name -> TypeM (TySet, Env, ModTypeBindBase Info VName) +checkModTypeBind :: ModTypeBindBase NoInfo Name -> TypeM (Env, ModTypeBindBase Info VName) checkModTypeBind (ModTypeBind name e doc loc) = do - (abs, env, e') <- checkModTypeExp e + (mty, e') <- checkModTypeExp e + addTySet $ mtyAbs mty bindSpaced1 Signature name loc $ \name' -> do usedName name' pure - ( abs, - mempty - { envModTypeTable = M.singleton name' env, + ( mempty + { envModTypeTable = M.singleton name' mty, envNameMap = M.singleton (Signature, name) (qualName name') }, ModTypeBind name' e' doc loc @@ -374,16 +375,15 @@ checkOneModExp :: ModExpBase NoInfo Name -> - TypeM (TySet, MTy, ModExpBase Info VName) + TypeM (MTy, ModExpBase Info VName) checkOneModExp (ModParens e loc) = do - (abs, mty, e') <- checkOneModExp e - pure (abs, mty, ModParens e' loc) + (mty, e') <- checkOneModExp e + pure (mty, ModParens e' loc) checkOneModExp (ModDecs decs loc) = do checkForDuplicateDecs decs - (abstypes, env, decs', _) <- checkDecs decs + ((env, decs', _), abstypes) <- collectTySet $ checkDecs decs pure - ( abstypes, - MTy abstypes $ ModEnv env, + ( MTy abstypes $ ModEnv env, ModDecs decs' loc ) checkOneModExp (ModVar v loc) = do @@ -393,47 +393,46 @@ && isIntrinsic (qualLeaf v') ) $ typeError loc mempty "The 'intrinsics' module may not be used in module expressions." - pure (mempty, MTy mempty env, ModVar v' loc) + pure (MTy mempty env, ModVar v' loc) checkOneModExp (ModImport name NoInfo loc) = do (name', env) <- lookupImport loc name pure - ( mempty, - MTy mempty $ ModEnv env, + ( MTy mempty $ ModEnv env, ModImport name (Info name') loc ) checkOneModExp (ModApply f e NoInfo NoInfo loc) = do - (f_abs, f_mty, f') <- checkOneModExp f + (f_mty, f') <- checkOneModExp f case mtyMod f_mty of ModFun functor -> do - (e_abs, e_mty, e') <- checkOneModExp e + (e_mty, e') <- checkOneModExp e (mty, psubsts, rsubsts) <- applyFunctor (locOf loc) functor e_mty pure - ( mtyAbs mty <> f_abs <> e_abs, - mty, + ( mty, ModApply f' e' (Info psubsts) (Info rsubsts) loc ) _ -> typeError loc mempty "Cannot apply non-parametric module." checkOneModExp (ModAscript me se NoInfo loc) = do - (me_abs, me_mod, me') <- checkOneModExp me - (se_abs, se_mty, se') <- checkModTypeExp se + (me_mod, me') <- checkOneModExp me + (se_mty, se') <- checkModTypeExp se + addTySet $ mtyAbs se_mty match_subst <- badOnLeft $ matchMTys me_mod se_mty (locOf loc) - pure (se_abs <> me_abs, se_mty, ModAscript me' se' (Info match_subst) loc) + pure (se_mty, ModAscript me' se' (Info match_subst) loc) checkOneModExp (ModLambda param maybe_fsig_e body_e loc) = withModParam param $ \param' param_abs param_mod -> do - (abs, maybe_fsig_e', body_e', mty) <- + (maybe_fsig_e', body_e', mty) <- checkModBody (fst <$> maybe_fsig_e) body_e loc pure - ( abs, - MTy mempty $ ModFun $ FunModType param_abs param_mod mty, + ( MTy mempty $ ModFun $ FunModType param_abs param_mod mty, ModLambda param' maybe_fsig_e' body_e' loc ) -checkOneModExpToEnv :: ModExpBase NoInfo Name -> TypeM (TySet, Env, ModExpBase Info VName) +checkOneModExpToEnv :: ModExpBase NoInfo Name -> TypeM (Env, ModExpBase Info VName) checkOneModExpToEnv e = do - (e_abs, MTy abs mod, e') <- checkOneModExp e + (MTy abs mod, e') <- checkOneModExp e + addTySet abs case mod of - ModEnv env -> pure (e_abs <> abs, env, e') + ModEnv env -> pure (env, e') ModFun {} -> unappliedFunctor $ srclocOf e withModParam :: @@ -441,7 +440,7 @@ (ModParamBase Info VName -> TySet -> Mod -> TypeM a) -> TypeM a withModParam (ModParam pname psig_e NoInfo loc) m = do - (_abs, MTy p_abs p_mod, psig_e') <- checkModTypeExp psig_e + (MTy p_abs p_mod, psig_e') <- checkModTypeExp psig_e bindSpaced1 Term pname loc $ \pname' -> do let in_body_env = mempty {envModTable = M.singleton pname' p_mod} localEnv in_body_env $ @@ -461,54 +460,50 @@ ModExpBase NoInfo Name -> SrcLoc -> TypeM - ( TySet, - Maybe (ModTypeExp, Info (M.Map VName VName)), + ( Maybe (ModTypeExp, Info (M.Map VName VName)), ModExp, MTy ) checkModBody maybe_fsig_e body_e loc = enteringModule $ do - (body_e_abs, body_mty, body_e') <- checkOneModExp body_e + (body_mty, body_e') <- checkOneModExp body_e case maybe_fsig_e of Nothing -> pure - ( mtyAbs body_mty <> body_e_abs, - Nothing, + ( Nothing, body_e', body_mty ) Just fsig_e -> do - (fsig_abs, fsig_mty, fsig_e') <- checkModTypeExp fsig_e + (fsig_mty, fsig_e') <- checkModTypeExp fsig_e + addTySet $ mtyAbs fsig_mty fsig_subst <- badOnLeft $ matchMTys body_mty fsig_mty (locOf loc) pure - ( fsig_abs <> body_e_abs, - Just (fsig_e', Info fsig_subst), + ( Just (fsig_e', Info fsig_subst), body_e', fsig_mty ) -checkModBind :: ModBindBase NoInfo Name -> TypeM (TySet, Env, ModBindBase Info VName) +checkModBind :: ModBindBase NoInfo Name -> TypeM (Env, ModBindBase Info VName) checkModBind (ModBind name [] maybe_fsig_e e doc loc) = do - (e_abs, maybe_fsig_e', e', mty) <- checkModBody (fst <$> maybe_fsig_e) e loc + (maybe_fsig_e', e', mty) <- checkModBody (fst <$> maybe_fsig_e) e loc bindSpaced1 Term name loc $ \name' -> do usedName name' pure - ( e_abs, - mempty + ( mempty { envModTable = M.singleton name' $ mtyMod mty, envNameMap = M.singleton (Term, name) $ qualName name' }, ModBind name' [] maybe_fsig_e' e' doc loc ) checkModBind (ModBind name (p : ps) maybe_fsig_e body_e doc loc) = do - (abs, params', maybe_fsig_e', body_e', funsig) <- + (params', maybe_fsig_e', body_e', funsig) <- withModParam p $ \p' p_abs p_mod -> withModParams ps $ \params_stuff -> do let (ps', ps_abs, ps_mod) = unzip3 params_stuff - (abs, maybe_fsig_e', body_e', mty) <- checkModBody (fst <$> maybe_fsig_e) body_e loc + (maybe_fsig_e', body_e', mty) <- checkModBody (fst <$> maybe_fsig_e) body_e loc let addParam (x, y) mty' = MTy mempty $ ModFun $ FunModType x y mty' pure - ( abs, - p' : ps', + ( p' : ps', maybe_fsig_e', body_e', FunModType p_abs p_mod $ foldr addParam mty $ zip ps_abs ps_mod @@ -516,8 +511,7 @@ bindSpaced1 Term name loc $ \name' -> do usedName name' pure - ( abs, - mempty + ( mempty { envModTable = M.singleton name' $ ModFun funsig, envNameMap = @@ -633,6 +627,14 @@ onRetType te t = ([], EntryType t te) +-- | Check that a type is non-functional, looking up the liftedness of abstract +-- types in the environment. This works because entry points cannot be polymorphic, so any remaining type names must be abstract. +orderZeroM :: TypeBase dim u -> TypeM Bool +orderZeroM t = do + (orderZero t &&) . and <$> mapM isUnlifted (typeQualVars t) + where + isUnlifted qv = (< Lifted) <$> lookupAbsTy qv + checkEntryPoint :: SrcLoc -> [TypeParam] -> @@ -645,12 +647,6 @@ withIndexLink "polymorphic-entry" "Entry point functions may not be polymorphic." - | not (all orderZero param_ts) - || not (orderZero rettype') = - typeError loc mempty $ - withIndexLink - "higher-order-entry" - "Entry point functions may not be higher-order." | sizes_only_in_ret <- S.fromList (map typeParamName tparams) `S.intersection` fvVars (freeInType rettype') @@ -666,8 +662,14 @@ "Entry point size parameter " <> pretty p <> " only used non-constructively." - | otherwise = - pure () + | otherwise = do + param_ts_order_zero <- mapM orderZeroM param_ts + ret_order_zero <- orderZeroM rettype' + when (not (and param_ts_order_zero) || not ret_order_zero) $ + typeError loc mempty $ + withIndexLink + "higher-order-entry" + "Entry point functions may not be higher-order." where (RetType _ rettype_t) = rettype (rettype_params, rettype') = unfoldFunType rettype_t @@ -704,39 +706,38 @@ vb' ) -checkOneDec :: DecBase NoInfo Name -> TypeM (TySet, Env, DecBase Info VName) +checkOneDec :: DecBase NoInfo Name -> TypeM (Env, DecBase Info VName) checkOneDec (ModDec struct) = do - (abs, modenv, struct') <- checkModBind struct - pure (abs, modenv, ModDec struct') + (modenv, struct') <- checkModBind struct + pure (modenv, ModDec struct') checkOneDec (ModTypeDec sig) = do - (abs, sigenv, sig') <- checkModTypeBind sig - pure (abs, sigenv, ModTypeDec sig') + (sigenv, sig') <- checkModTypeBind sig + pure (sigenv, ModTypeDec sig') checkOneDec (TypeDec tdec) = do (tenv, tdec') <- checkTypeBind tdec - pure (mempty, tenv, TypeDec tdec') + pure (tenv, TypeDec tdec') checkOneDec (OpenDec x loc) = do - (x_abs, x_env, x') <- checkOneModExpToEnv x - pure (x_abs, x_env, OpenDec x' loc) + (x_env, x') <- checkOneModExpToEnv x + pure (x_env, OpenDec x' loc) checkOneDec (LocalDec d loc) = do - (abstypes, env, d') <- checkOneDec d - pure (abstypes, env, LocalDec d' loc) + (env, d') <- checkOneDec d + pure (env, LocalDec d' loc) checkOneDec (ImportDec name NoInfo loc) = do (name', env) <- lookupImport loc name when (isBuiltin name) $ typeError loc mempty $ pretty name <+> "may not be explicitly imported." - pure (mempty, env, ImportDec name (Info name') loc) + pure (env, ImportDec name (Info name') loc) checkOneDec (ValDec vb) = do (env, vb') <- checkValBind vb - pure (mempty, env, ValDec vb') + pure (env, ValDec vb') -checkDecs :: [DecBase NoInfo Name] -> TypeM (TySet, Env, [DecBase Info VName], Env) +checkDecs :: [DecBase NoInfo Name] -> TypeM (Env, [DecBase Info VName], Env) checkDecs (d : ds) = do - (d_abstypes, d_env, d') <- checkOneDec d - (ds_abstypes, ds_env, ds', full_env) <- localEnv d_env $ checkDecs ds + (d_env, d') <- checkOneDec d + (ds_env, ds', full_env) <- localEnv d_env $ checkDecs ds pure - ( d_abstypes <> ds_abstypes, - case d' of + ( case d' of LocalDec {} -> ds_env ImportDec {} -> ds_env _ -> ds_env <> d_env, @@ -745,4 +746,4 @@ ) checkDecs [] = do full_env <- askEnv - pure (mempty, mempty, [], full_env) + pure (mempty, [], full_env) diff --git a/src/Language/Futhark/TypeChecker/Modules.hs b/src/Language/Futhark/TypeChecker/Modules.hs --- a/src/Language/Futhark/TypeChecker/Modules.hs +++ b/src/Language/Futhark/TypeChecker/Modules.hs @@ -89,8 +89,9 @@ pure (v, v') let substs = M.fromList pairs rev_substs = M.fromList $ map (uncurry $ flip (,)) pairs - - pure (substituteInMTy substs orig_mty, rev_substs) + new_mty = substituteInMTy substs orig_mty + addTySet $ mtyAbs new_mty + pure (new_mty, rev_substs) where substituteInMTy :: M.Map VName VName -> MTy -> MTy substituteInMTy substs (MTy mty_abs mty_mod) = diff --git a/src/Language/Futhark/TypeChecker/Monad.hs b/src/Language/Futhark/TypeChecker/Monad.hs --- a/src/Language/Futhark/TypeChecker/Monad.hs +++ b/src/Language/Futhark/TypeChecker/Monad.hs @@ -14,6 +14,7 @@ lookupMTy, lookupImport, lookupMod, + lookupAbsTy, localEnv, TypeError (..), prettyTypeError, @@ -26,6 +27,8 @@ aNote, MonadTypeChecker (..), TypeState (stateNameSource), + addTySet, + collectTySet, usedName, checkName, checkAttr, @@ -76,7 +79,7 @@ import Language.Futhark.Traversals import Language.Futhark.Warnings import Paths_futhark qualified -import Prelude hiding (mapM, mod) +import Prelude hiding (abs, mapM, mod) newtype Note = Note (Doc ()) @@ -159,7 +162,7 @@ -- | A mapping from import import names to 'Env's. This is used to -- resolve @import@ declarations. -type ImportTable = M.Map ImportName Env +type ImportTable = M.Map ImportName (TySet, Env) data Context = Context { contextEnv :: Env, @@ -175,6 +178,8 @@ stateWarnings :: Warnings, -- | Which names have been used. stateUsed :: S.Set VName, + -- | Known abstract type names. + stateTySet :: TySet, stateCounter :: Int } @@ -216,7 +221,7 @@ (Warnings, Either TypeError (a, VNameSource)) runTypeM env imports fpath src (TypeM m) = do let ctx = Context env imports fpath True - s = TypeState src mempty mempty 0 + s = TypeState src mempty mempty mempty 0 case runExcept $ runStateT (runReaderT m ctx) s of Left (ws, e) -> (ws, Left e) Right (x, s') -> (stateWarnings s', Right (x, stateNameSource s')) @@ -246,6 +251,33 @@ where explode = unknownVariable Signature qn loc +-- | Add set of abstract types. +addTySet :: TySet -> TypeM () +addTySet tys = modify $ \s -> s {stateTySet = tys <> stateTySet s} + +-- | Run type checking command while accumulating (and returning) all new +-- abstract types, then reset to known abstract types afterwards. +collectTySet :: TypeM a -> TypeM (a, TySet) +collectTySet m = do + old <- gets stateTySet + x <- m + new <- gets stateTySet + modify $ \s -> s {stateTySet = old} + pure (x, new `M.difference` old) + +-- | Look up the liftedness of an abstract type. +lookupAbsTy :: QualName VName -> TypeM Liftedness +lookupAbsTy v = do + abs <- gets stateTySet + case M.lookup v abs of + Just l -> pure l + Nothing -> + error $ + unlines + [ "lookupAbsTy: " <> prettyString v, + "known: " <> show abs + ] + -- | Look up an import. lookupImport :: SrcLoc -> FilePath -> TypeM (ImportName, Env) lookupImport loc file = do @@ -259,7 +291,9 @@ <+> dquotes (pretty (includeToText canonical_import)) "Known:" <+> commasep (map (pretty . includeToText) (M.keys imports)) - Just scope -> pure (canonical_import, scope) + Just (abs, scope) -> do + addTySet abs + pure (canonical_import, scope) -- | Evaluate a 'TypeM' computation within an extended (/not/ -- replaced) environment.