diff --git a/copilot-bluespec/.dockerignore b/copilot-bluespec/.dockerignore new file mode 100644 index 00000000..d1a0321b --- /dev/null +++ b/copilot-bluespec/.dockerignore @@ -0,0 +1,29 @@ +dist +dist-* +cabal-dev +*.o +*.hi +*.chi +*.chs.h +*.dyn_o +*.dyn_hi +.hpc +.hsenv +.cabal-sandbox/ +cabal.sandbox.config +*.prof +*.aux +*.hp +*.eventlog +.stack-work/ +cabal.project.local +cabal.project.local~ +.HTF/ +.ghc.environment.* +copilot-profiling +.DS_Store +.log + +Dockerfile +.git +.gitignore diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG new file mode 100644 index 00000000..10f4486e --- /dev/null +++ b/copilot-bluespec/CHANGELOG @@ -0,0 +1,44 @@ +2025-05-18 + * Include `copilot-bluespec` in mainline `copilot` repo. (#623) + +2025-05-08 + * Version bump (4.4). (copilot-bluespec#43) + +2025-05-05 + * Version bump (4.3.1). (copilot-bluespec#41) + * Move Copilot.Compile.Bluespec.External out of shared directory. + (copilot-bluespec#36) + * Allow building with filepath-1.5.*. (copilot-bluespec#39) + +2025-03-10 + * Version bump (4.3). (copilot-bluespec#34) + +2025-01-20 + * Version bump (4.2). (copilot-bluespec#31) + * Implement missing floating-point operations. (copilot-bluespec#28) + * Allow using same trigger name in multiple declarations. + (copilot-bluespec#30) + +2024-11-08 + * Version bump (4.1). (copilot-bluespec#25) + +2024-09-09 + * Version bump (4.0). (copilot-bluespec#23) + * Support translating Copilot array updates to Bluespec. + (copilot-bluespec#19) + +2024-08-03 + * Test GHC 9.4 through 9.8. (copilot-bluespec#20) + +2024-07-11 + * Version bump (3.20). (copilot-bluespec#11) + * Support translating Copilot struct updates to Bluespec. + (copilot-bluespec#10) + * Fix a bug in the translation of the signum function. + (copilot-bluespec#14) + * Fix a bug in the translation of floating-point comparisons. + (copilot-bluespec#15) + +2024-03-08 + * Version bump (3.19). (copilot-bluespec#5) + * Create new library for Bluespec backend. diff --git a/copilot-bluespec/DESIGN.md b/copilot-bluespec/DESIGN.md new file mode 100644 index 00000000..dffb607a --- /dev/null +++ b/copilot-bluespec/DESIGN.md @@ -0,0 +1,928 @@ +# The design of `copilot-bluespec` + +This document provides an overview of how the `copilot-bluespec` library +compiles a Copilot specification to a Bluespec program. We assume that you +already have some familiarity with core Copilot concepts such as streams, +triggers, externs, etc. + +## Bluespec overview + +Bluespec is a high-level hardware design language (HDL). Bluespec comes with a +compiler, `bsc`, as well as its own simulator, which allows users to run +Bluespec programs easily. Bluespec also supports compiling to Verilog. + +There are two different syntaxes for the Bluespec language: Bluespec Haskell +(BH) and Bluespec SystemVerilog (BSV). Bluespec Haskell (also known as Bluespec +Classic), the older of the two syntaxes, is a more functional, high-level +syntax that is heavily inspired by the Haskell programming language. Bluespec +SystemVerilog, which was created later, more closely SystemVerilog and targets +hardware design engineers who are more familiar with SystemVerilog's syntax. +Both syntaxes are merely front-ends for the same language, and programs written +in one syntax can be converted to the other. + +The `copilot-bluespec` library compiles to Bluespec Haskell rather than +Bluespec SystemVerilog. This is primarily because BH's Haskell-like syntax is a +closer fit to how Copilot is structured, which makes the design of the compiler +simpler. + +## A small example + +To get a sense for how `copilot-bluespec` works, let us compile a simple +Copilot specification down to Bluespec. Our specification will declare a stream +containing the Fibonacci numbers, along with some triggers that will fire if a +Fibonacci number is even or odd: + +```hs +module Main (main) where + +import qualified Prelude as P () + +import Language.Copilot +import Copilot.Compile.Bluespec + +fibs :: Stream Word32 +fibs = [1, 1] ++ (fibs + drop 1 fibs) + +evenStream :: Stream Word32 -> Stream Bool +evenStream n = (n `mod` constant 2) == constant 0 + +oddStream :: Stream Word32 -> Stream Bool +oddStream n = not (evenStream n) + +spec :: Spec +spec = do + trigger "even" (evenStream fibs) [arg fibs] + trigger "odd" (oddStream fibs) [arg fibs] + +main :: IO () +main = do + spec' <- reify spec + compile "Fibs" spec' +``` + +Note that the only parts of this program that are `copilot-bluespec`–specific +are: + +1. The `import Copilot.Compile.Bluespec` statement, and +2. The call to `compile "Fibs" spec'` in `main`. This will compile the Copilot + specification to a Bluespec program named `Fibs.bs`. + +Running this program will generate five files[^1]: + +[^1]: The actual code in these files is machine-generated and somewhat +difficult to read. We have cleaned up the code slightly to make it easier to +understand. + +* `FibsTypes.bs`: If the Copilot specification contains any structs, then this + file will contain the corresponding Bluespec struct definitions. The + specification does not contain any structs, so this file is mostly empty: + + ```bluespec + package FibsTypes where + + import FloatingPoint + import Vector + ``` + + Later in this document, we will see a different example that makes use of + structs. Note that the syntax used here is much like in Haskell, with a + notable difference being that Bluespec uses the `package` keyword instead of + `module`. + +* `FibsIfc.bs`: This file defines a _module interface_ `FibsIfc`, whose methods + correspond to the names of the triggers in the Copilot spec: + + ```bluespec + package FibsIfc where + + import FloatingPoint + import Vector + + import FibsTypes + + interface FibsIfc = + even :: UInt 32 -> Action + odd :: UInt 32 -> Action + ``` + + An interface like `FibsIfc` can be thought of as a special form of data type + that describes how a module (a hardware object) interacts with the + surrounding environment. In order for an application to make use of a Copilot + monitor, it must instantiate `FibsIfc`'s methods. Each method takes a `UInt + 32` (an unsigned 32-bit integer) as an argument and return an `Action`, which + is the Bluespec type for expressions that act on the state of the circuit (at + circuit execution time). Possible `Action`s include reading from and writing + to registers, as well as printing messages. + + We will see an example of how to instantiate `FibsIfc` later. + +* `Fibs.bs`: This file defines a `mkFibs` function, which orchestrates + everything in the generated Bluespec monitor: + + ```bluespec + package Fibs where + + import FloatingPoint + import Vector + + import FibsTypes + import FibsIfc + import BluespecFP + + mkFibs :: Module FibsIfc -> Module Empty + mkFibs ifcMod = + module + ifc <- ifcMod + + s0_0 :: Reg (UInt 32) <- mkReg 1 + s0_1 :: Reg (UInt 32) <- mkReg 1 + let s0 :: Vector 2 (Reg (UInt 32)) + s0 = update (update newVector 0 s0_0) 1 s0_1 + s0_idx :: Reg (Bit 64) <- mkReg 0 + + let s0_get :: Bit 64 -> UInt 32 + s0_get x = (select s0 ((s0_idx + x) % 2))._read + + s0_gen :: UInt 32 + s0_gen = s0_get 0 + s0_get 1 + + even_guard :: Bool + even_guard = + (s0_get 0 % 2) == 0 + + odd_guard :: Bool + odd_guard = + not (s0_get 0 % 2 == 0) + + rules + "even": when even_guard ==> + ifc.even (s0_get 0) + + "odd:": when odd_guard ==> + ifc.odd (s0_get 0) + + "step": when True ==> + action + select s0 s0_idx := s0_gen + s0_idx := (s0_idx + 1) % 2 + ``` + + `mkFibs` returns a module, which can be thought of as a generator of hardware + objects. `mkFibs` takes a `FibsIfc` module as an argument and returns another + module, which is parameterized by `Empty`. `Empty` is a standard interface + with no methods, and `Empty` is typically used in top-level modules that act + as program entrypoints. + + Note that the `module` and `action` keywords can be thought of as specialized + versions of Haskell's `do`-notation, where `module` denotes the `Module` + monad, and `action` denotes the `ActionValue` monad. (Note that `Action` is + an alias for `ActionValue ()`.) The `Monad` monad describes how to elaborate + the structure of a module, whereas the `ActionValue` monad describes the + behavior of a circuit at execution time. + +* `BluespecFP.bsv`: A collection of floating-point operations that leverage BDPI + (Bluespec's foreign-function interface). We will omit the full contents of + this file for brevity, but it will look something like this: + + ```bluespec + import FloatingPoint::*; + + import "BDPI" function Float bs_fp_expf (Float x); + import "BDPI" function Double bs_fp_exp (Double x); + import "BDPI" function Float bs_fp_logf (Float x); + import "BDPI" function Double bs_fp_log (Double x); + ... + ``` + + For more information on what this file does, see the "Floating-point numbers" + section below. + +* `bs_fp.c`: A collection of floating-point operations implemented in C. These + functions are imported via BDPI in `BluespecFP.bsv`. We will omit the full + contents of this file for brevity, but it will look something like this: + + ```bluespec + #include + + union ui_float { + unsigned int i; + float f; + }; + + union ull_double { + unsigned long long i; + double f; + }; + + unsigned int bs_fp_expf(unsigned int x) { + ... + } + + unsigned long long bs_fp_exp(unsigned long long x) { + ... + } + + unsigned int bs_fp_logf(unsigned int x) { + ... + } + + unsigned long long bs_fp_log(unsigned long long x) { + ... + } + + ... + ``` + + For more information on what this file does, see the "Floating-point numbers" + section below. + +In a larger application, a Copilot user would instantiate `mkFibs` with a +`FibsIfc` module that describes what should happen when the `even` and `odd` +triggers fire. `FibsIfc` contains everything that the user must supply; +everything else is handled within the module that `mkFibs` returns. + +Here is an example of a larger application might look like: + +```bluespec +package Top where + +import Fibs +import FibsIfc +import FibsTypes + +fibsIfc :: Module FibsIfc +fibsIfc = + module + interface + even x = + $display "Even Fibonacci number: %0d" x + + odd x = + $display "Odd Fibonacci number: %0d" x + +mkTop :: Module Empty +mkTop = mkFibs fibsIfc +``` + +`mkTop` is the top-level module that we will use as a program entrypoint. The +only interesting thing that it does is instantiate `mkFibs` with a custom +`FibsIfc`, where `even` and `odd` are defined to display a custom message +whenever an even or odd Fibonacci number is encountered, respectively. + +We can run `mkTop` by using Bluespec's simulator like so: + +``` +$ bsc -sim -g mkTop -u Top.bs +checking package dependencies +compiling Top.bs +code generation for mkTop starts +Elaborated module file created: mkTop.ba +All packages are up to date. + +$ bsc -sim -e mkTop -o mkTop.exe bs_fp.c +Bluesim object created: mkTop.{h,o} +Bluesim object created: model_mkTop.{h,o} +Simulation shared library created: mkTop.exe.so +Simulation executable created: mkTop.exe + +$ ./mkTop.exe -m 10 +Odd Fibonacci number: 1 +Odd Fibonacci number: 1 +Even Fibonacci number: 2 +Odd Fibonacci number: 3 +Odd Fibonacci number: 5 +Even Fibonacci number: 8 +Odd Fibonacci number: 13 +Odd Fibonacci number: 21 +Even Fibonacci number: 34 +``` + +We pass `-m 10` to instruct Bluespec's simulator to only run for 10 clock +cycles. Note that the first clock cycle does not fire any rules. This is a +quirk of how hardware works: the reset signal is off in the first cycle, and +the values of registers do not become ready until after the reset signal is +enabled. Because all of the rules depend on registers, none of them will fire +until the second clock cycle or later. + +## Streams + +Much like in `copilot-c99`, `copilot-bluespec` translates each stream +declaration into a ring buffer. More concretely, it translates a `Stream t` +into a `Vector n (Reg t)`, where: + +* A `Vector` is an array whose length is encoded at the type level, must + like Copilot's arrays. (Note that Bluespec has a separate `Array` type, but + `Array`s are more low-level, and they are not indexed by their length at the + type level.) + +* `n` is the minimum number of elements needed to compute later values in the + stream. + +* `t` is the stream's element type. + +* `Reg` is a register, which stores a value that can be read from and written + to. As time advances, we will update the `Reg`s in the ring buffer with later + values in the stream. + +(Commentary: a ring buffer is not the only way we could translate a stream to +Bluespec. Bluespec also has a +[`MIMO`](https://github.com/B-Lang-org/bsc/blob/f00d205867eefe09c60e11b4df155bb87041799a/src/Libraries/Base3-Misc/MIMO.bsv#L52-L73) +(many-in, many-out) queue that is _almost_ suitable for our needs, but it comes +with an unusual restriction that it must have a minimum size of 2 elements. +There exist Copilot streams that only require one element of storage, so we +would have to special-case these streams if we wanted to use a `MIMO`.) + +The `Fibs.bs` example above contains exactly one stream, which is created at +the top of the `mkFibs` function: + +```bluespec + s0_0 :: Reg (UInt 32) <- mkReg 1 + s0_1 :: Reg (UInt 32) <- mkReg 1 + let s0 :: Vector 2 (Reg (UInt 32)) + s0 = update (update newVector 0 s0_0) 1 s0_1 + s0_idx :: Reg (Bit 64) <- mkReg 0 +``` + +Here, `s0_idx`, tracks the index of the next stream element to be updated. +`mkFibs` then defines several functions in terms of `s0` and `s0_idx`, which +are then used in the rules, which we will describe later. Note that `s0_idx` is +a register of type `Bit 64`, which can be thought of as a raw 64-bit value. + +In order to access an element of a stream, we make use of the `s0_get` +function: + +```bluespec + let s0_get :: Bit 64 -> UInt 32 + s0_get x = (select s0 ((s0_idx + x) % 2))._read +``` + +This will use `s0_idx` and an offset `x` to compute which `Reg` in the `Vector` +to read from. + +## Rules + +The _rules_ govern what actions are performed during each cycle. There are +three actions in the `Fibs.hs` example: + +```bluespec + rules + "even": when even_guard ==> + ifc.even (s0_get 0) + + "odd:": when odd_guard ==> + ifc.odd (s0_get 0) + + "step": when True ==> do + select s0 s0_idx := s0_gen + s0_idx := (s0_idx + 1) % 2 +``` + +Each rule consists of three parts: + +1. A label (e.g., `"even"`) that uniquely identifies the rule within the + module. + +2. An explicit condition, which is a boolean expression of the form + `when ==> ...`. In order for a rule to fire on a given clock cycle, + its explicit condition `` must hold. + +3. A rule body (e.g., `ifc.even (s0_get 0)`), which describes what action the + rule performs if it fires on a given clock cycle. + +In the example above, the `"even"` and `"odd"` rules govern the behavior of the +triggers in the Copilot specification. These rules will only fire if +`even_guard` or `odd_guard` hold, and if they fire, they will call the `even` +or `odd` method of `FibsIfcs`, respectively. The definitions of `even_guard` +and `odd_guard` are: + +```bluespec + even_guard :: Bool + even_guard = + (s0_get 0 % 2) == 0 + + odd_guard :: Bool + odd_guard = + not (s0_get 0 % 2 == 0) +``` + +The `"step"` rule is the heart of the Copilot specification, and it always runs +on each clock cycle. `"step"` does two things: + +1. It computes the next element of the `s0` stream using the `s0_gen` function, + which is defined like so: + + ```bluespec + s0_gen :: UInt 32 + s0_gen = s0_get 0 + s0_get 1 + ``` + +2. It increments `s0_idx`, making sure to wrap around to `0` if its value + exceeds `1`. + +### A note on atomicity + +Bluespec rules are _atomic_, which means that the Bluespec compiler will ensure +that the rules are executed in some logical order that ensures the absence of +race conditions. Moreover, all register updates that occur within a module's +rules are performed simultaneously at the end of a clock cycle. + +This might seem strange if you are accustomed to the execution model of a +language like C, where all statements (and their accompanying side effects) are +invoked sequentially, one after the other. This is not how Bluespec works, +however. Recall the definitions of the three rules in the example program +above: + +```bluespec + rules + "even": when even_guard ==> + ifc.even (s0_get 0) + + "odd:": when odd_guard ==> + ifc.odd (s0_get 0) + + "step": when True ==> do + select s0 s0_idx := s0_gen + s0_idx := (s0_idx + 1) % 2 +``` + +If this were a language like C, then the order in which the rules appear would +have an effect on the runtime semantics of the program, as the behavior of +`s0_get` (used in the `"even"` and `"odd"` rules) depends on the current value +of `s0` and `s0_idx`. In Bluespec, however, the order of these rules do _not_ +matter. The `"step"` rule performs side effects of updating the value of `s0` +and `s0_idx`, but these effects are performed in a single, atomic transaction +at the end of the clock cycle. This means that the values of `s0` and `s0_idx` +that `s0_get` sees will always match their values at the start of the clock +cycle, regardless of what order Bluespec uses to invoke the rules. + +Because the Bluespec compiler can pick whatever rule order it wishes to, this +can impact the order in which `$display` output is presented. This doesn't +impact the example above, as the `"even"` and `"odd"` rules will never fire on +the same clock cycle, meaning that there is always only one `$display` call per +cycle. If program fires multiple rules on a clock cycle and each one calls +`$display`, then the order in which the `$display` calls will run is not +specified. + +## External streams + +The example above sampled data from a stream that was defined within the +Copilot specification. To see what happens when a specification uses an +external stream, let's make one small change to the example: + +```diff + fibs :: Stream Word32 +-fibs = [1, 1] ++ (fibs + drop 1 fibs) ++fibs = extern "fibs" Nothing +``` + +Now let's re-run the example and inspect the resulting Bluespec program. There +are two notable changes worth commenting on. The first change is in +`FibsIfc.bs`: + +```bluespec +package FibsIfc where + +import FloatingPoint +import Vector + +import FibsTypes + +interface FibsIfc = + even :: UInt 32 -> Action + odd :: UInt 32 -> Action + fibs :: Reg (UInt 32) +``` + +This time, the `FibsIfc` interface has an additional `fibs` method of type `Reg +(UInt 32)`. This register corresponds to the external stream that we just +defined, and it is the responsibility of the application which instantiates +`FibsIfc` to dictate what values should be written to the register. + +The second change is in `Fibs.bs`: + +```bluespec +package Fibs where + +import FloatingPoint +import Vector + +import FibsTypes +import FibsIfc + +mkFibs :: Module FibsIfc -> Module Empty +mkFibs ifcMod = + module + ifc <- ifcMod + + let even_guard :: Bool + even_guard = + (ifc.fibs._read % 2) == 0 + + odd_guard :: Bool + odd_guard = + not (ifc.fibs._read % 2 == 0) + + rules + "even": when even_guard ==> + ifc.even ifc.fibs._read + + "odd:": when odd_guard ==> + ifc.odd ifc.fibs._read +``` + +This time, the only stream that is referenced is `ifc.fibs`. As a consequence, +the `s0` stream, the `s0_idx` index, and the `"step"` rule are no longer +necessary, making the code considerably simpler. + +The flip side to having the generated code be simpler is that the application +which uses `mkFibs` must now do additional work to specify what the value of +`ifc.fibs` is. For example, we can port the behavior of the previous version +of the program like so: + +```bluespec +package Top where + +import Vector + +import Fibs +import FibsIfc +import FibsTypes + +fibsIfc :: Module FibsIfc +fibsIfc = + module + s0_0 :: Reg (UInt 32) <- mkReg 1 + s0_1 :: Reg (UInt 32) <- mkReg 1 + let s0 :: Vector 2 (Reg (UInt 32)) + s0 = update (update newVector 0 s0_0) 1 s0_1 + s0_idx :: Reg (Bit 64) <- mkReg 0 + + let s0_get :: Bit 64 -> UInt 32 + s0_get x = (select s0 ((s0_idx + x) % 2))._read + + s0_gen :: UInt 32 + s0_gen = s0_get 0 + s0_get 1 + + fibs_impl :: Reg (UInt 32) <- mkReg 1 + + interface + even x = + $display "Even Fibonacci number: %0d" x + + odd x = + $display "Odd Fibonacci number: %0d" x + + fibs = fibs_impl + + rules + "fibs": when True ==> + fibs_impl := s0_get 1 + + "step": when True ==> + action + select s0 s0_idx := s0_gen + s0_idx := (s0_idx + 1) % 2 + +mkTop :: Module Empty +mkTop = mkFibs fibsIfc +``` + +The code involving `s0`, `s0_idx`, and the `"step"` rule is exactly as before. +The only notable difference is that we create an additional `fibs_impl` +register, declare `fibs = fibs_impl` when instantiating the `FibsIfc` +interface, and declare an additional `"fibs"` rule to update the value of +`fibs_impl` on each clock cycle. Note that we always set the value of +`fibs_impl` to be `s0_get 1`, which corresponds to the most recently computed +Fibonacci number. If we set `fibs_impl` to be `s0_get 0` instead, then +`fibs_impl` would lag behind by one cycle. (Try it.) + +# Notes + +## Arrays + +Copilot's `Array n t` type is translated directly to Bluespec's `Vector n t` +type, which makes life very simple. + +## Structs + +Like Copilot, Bluespec has a notion of structs, e.g., + +```bluespec +struct Coord = + x :: UInt 32 + y :: UInt 32 + +exCoord :: Coord +exCoord = Coord { x = 27, y = 42 } + +flipCoord :: Coord -> Coord +flipCoord c = Coord { x = C.y, y = C.x } +``` + +As such, it proves fairly straightforward to translate Copilot structs to +Bluespec structs. For instance, given these Copilot structs: + +```hs +data Volts = Volts + { numVolts :: Field "numVolts" Word16 + , flag :: Field "flag" Bool + } + +instance Struct Volts where + typeName _ = "Volts" + toValues volts = [ Value Word16 (numVolts volts) + , Value Bool (flag volts) + ] + +instance Typed Volts where + typeOf = Struct (Volts (Field 0) (Field False)) + +data Battery = Battery + { temp :: Field "temp" Word16 + , volts :: Field "volts" Volts + } + +instance Struct Battery where + typeName _ = "Battery" + toValues battery = [ Value typeOf (temp battery) + , Value typeOf (volts battery) + ] + +instance Typed Battery where + typeOf = Struct (Battery (Field 0) (Field undefined)) +``` + +`copilot-bluespec` will generate the following `StructsTypes.bs` file: + +```bluespec +package StructsTypes where + +import FloatingPoint +import Vector + +struct Volts = + numVolts :: UInt 16 + flag :: Bool + deriving (Bits) + +struct Vattery = + temp :: UInt 16 + volts :: BS_volts + deriving (Bits) +``` + +The purpose of the `*Types.bs` file is to define structs separately from other +parts of the generated code. Note that each struct definition derives a `Bits` +instance so that it can be stored inside a `Reg`. + +## Capitalization of generated names + +Copilot allows users to name several things which will influence the names of +generated code, including external streams, triggers, structs, and the file +names. The `copilot-c99` backend is able to turn just about any user-supplied +name into the name of a C identifier, as C is a remarkably case-insensitive +language. For instance, both "`Volts`" and "`volts`" are legal struct names in +C. + +Bluespec, on the other hand, imposes restrictions on which identifiers can +begin with an uppercase letter and which can begin with a lowercase letter. +The following identifiers must begin with an uppercase letter: + +* Struct names +* Interface names + +The following identifiers must begin with a lowercase letter: + +* Function and value names +* Interface method names + +Package names and rule names may begin with either an uppercase or lowercase +letter. + +How do we ensure that `copilot-bluespec` respects Bluespec's capitalization +requirements? As an example, suppose a Copilot specification defines a struct +named "`volts`". This name cannot be used as a Bluespec struct name on its own, +as it does not begin with an uppercase letter. To avoid issues, we prepend the +prefix "`BS_`" to this name to get "`BS_volts`", which is a valid Bluespec +identifier. Similarly, `copilot-bluespec` will prepend the prefix `bs_` to +uppercase Copilot names if it is used in a place that expects lowercase +Bluespec identifiers. + +Note that `copilot-bluespec` will only prepend prefixes if they are necessary +to prevent the generated code from being littered with `BS_`/`bs_` prefixes in +the common case. + +## Floating-point numbers + +`copilot-bluespec` supports all of Copilot's floating-point operations with +varying degrees of performance. The following floating-point operations compile +directly to relatively performant circuits: + +* Basic arithmetic (`(+)`, `(-)`, `(*)`, `(/)`) +* Equality checking (`(==)` and `(/=)`) +* Inequality checking (`(<)`, `(<=)`, `(>)`, and `(>=)`) +* `abs` +* `signum` +* `recip` + +These operations correspond to the floating-point operations that the Bluespec +standard library provides that are well tested. Unfortunately, the Bluespec +standard library does not offer well-tested versions (or even _any_ versions) +of the remainder of Copilot's floating-point operations. The rest of these +operations are instead implemented by using BDPI (Bluespec's foreign function +interface) to interface with C code: + +* `sqrt` +* `acos` +* `asin` +* `atan` +* `atan2` +* `cos` +* `sin` +* `tan` +* `acosh` +* `asinh` +* `atanh` +* `cosh` +* `sinh` +* `tanh` +* `exp` +* `pow` +* `log` +* `logb` +* `ceiling` +* `floor` + +Implementing these operations via C provides high confidence that they are +implemented correctly, but at a somewhat steep performance penalty. + +Because these operations need to be implemented via BDPI, `copilot-bluespec` +generates two additional files: `BluespecFP.bsv` (which contains the Bluespec +function stubs for each function implemented via BDPI) and `bs_fp.c` (which +contains the corresponding C function definitions). To see how this works, +let us take a look at one of the BDPI'd functions, `sqrt`: + +```bluespec +import "BDPI" function Double bs_fp_sqrt (Double x); +import "BDPI" function Float bs_fp_sqrtf (Float x); +``` + +This declares a Bluespec function `bs_fp_sqrt` that is implemented using a C +function (also of the name `bs_fp_sqrt`) under the hood. This takes a Bluespec +`Double` as an argument and also returns a `Double`. Note that `Double` is not +treated magically by the Bluespec compiler here. This is because any Bluespec +struct can be used in BDPI (provided that the struct type implements the `Bits` +class), and Bluespec's `Double` is implemented as a struct with a `Bits` +instance that exactly matches the bit layout expected by IEEE-754 +double-precision floats. (Similarly for Bluespec's `Float` type.) + +Note that at present, the `import "BDPI"` feature is only available when using +the BSV syntax, not the BH syntax. As such, this is currently the only place +where we generate BSV code. + +The corresponding C code for `bs_fp_sqrt(f)` is: + +```c +union ull_double { + unsigned long long i; + double f; +}; + +union ui_float { + unsigned int i; + float f; +}; + +unsigned long long bs_fp_sqrt(unsigned long long x) { + union ull_double x_u; + union ull_double r_u; + x_u.i = x; + r_u.f = sqrt(x_u.f); + return r_u.i; +} + +unsigned int bs_fp_sqrtf(unsigned int x) { + union ui_float x_u; + union ui_float r_u; + x_u.i = x; + r_u.f = sqrtf(x_u.f); + return r_u.i; +} +``` + +There is a lot to unpack here. Let's go through this step by step: + +1. The C version of `bs_fp_sqrt` takes and returns an `unsigned long long`. The + use of `unsigned long long` is dictated by Bluespec itself: whenever you + use a Bluespec type in BDPI that fits in exactly 64 bits, then Bluespec + expects the corresponding C type to be `unsigned long long`. (You can see + this for yourself by inspecting the generated `imported_BDPI_functions.h` + header file.) + + There is a similar story for `bs_fp_sqrtf`, which takes an `unsigned int`. + Bluespec dictates the use of `unsigned int` when the BDPI types fits in + exactly 32 bits. + +2. This poses something of a challenge for us, since we want the implementation + of `bs_fp_sqrt` to work over `double`s, not `unsigned long long`s. To make + this possible, we define a `union ull_double` type that allows easily + converting an `unsigned long long` to a `double` and vice versa. + + There is an analogous story for `ui_float`, which allows conversion to and + from the `unsigned int` and `float` types. + +3. Finally, we perform the `sqrt(f)` function on the argument, using + `ull_double`/`ui_float` as necessary to make the types work out. + +Strictly speaking, it is only necessary to compile the generated `bs_fp.c` file +if the generated Bluespec program makes use of any of the BDPI-related +floating-point operations mentioned above. That being said, it doesn't hurt to +compile it even if the generated Bluespec program _doesn't_ use any of them, so +it's generally good practice to pass `bs_fp.c` to `bsc`. + +Eventually, we would like to stop using BDPI in favor of native Bluespec code, +which would be more performant. To do so, would we need to address the +following Bluespec issues: + +* The implementation of `sqrt` in Bluespec's standard library is buggy: + https://github.com/B-Lang-org/bsc/issues/710 + +* Bluespec's standard library does not implement the remaining floating-point + operations at all: https://github.com/B-Lang-org/bsc/issues/368 + +## Warnings + +Code generated by `copilot-bluespec` should always compile, but it is not +currently guaranteed that the code will compile without warnings. This is +because unlike `gcc` or `clang`, the `bsc` compiler produces much more warnings +by default, and in rare cases, you may trigger `bsc` warnings. This section +describes some of these warnings. + +### Rule bodies with no actions (G0023) + +Let's suppose you have a trigger named `nop`, and you instantiate it like so: + +```bluespec +exampleIfc :: Module ExampleIfc +exampleIfc = + module + interface + nop :: Action + nop = return () +``` + +As a result, firing the `nop` trigger will do absolutely nothing. `bsc` takes +notice of this fact and warns you about it: + +``` +Warning: "CopilotTest.bs", line 27, column 8: (G0023) + The body of rule `nop' has no actions. Removing... +``` + +Where `G0023` is a unique code associated with this class of warning. + +### Warning suppression notification (S0080) + +If you find the warnings above to be annoying, `bsc` offers a way to suppress +them with the `-suppress-warnings ::...` flag. +For instance, you can suppress the G0023 warning code by passing: + +``` +-suppress-warnings G0023 +``` + +This does indeed suppress them, but now `bsc` produces _another_ warning: + +``` +Warning: Unknown position: (S0080) + 1 warnings were suppressed. +``` + +That's right, `bsc` warns you about the use of `-suppress-warnings`. That feels +a bit silly to me, but in any case, the new warning comes with its own warning +code, S0080. As a result, you can _really_ suppress warnings by passing this to +`bsc`: + +``` +-suppress-warnings G0023:S0080 +``` + +## `language-bluespec` + +`copilot-bluespec` uses +[`language-bluespec`](https://github.com/GaloisInc/language-bluespec) as a +library for creating Bluespec Haskell ASTs. Most of the source code from +`language-bluespec` is directly based on the code in the Bluespec compiler, +[`bsc`](https://github.com/B-Lang-org/bsc). This is because there is (to our +knowledge) no other existing Haskell library for representing Bluespec Haskell +ASTs, and adapting the code in `bsc` proves to be the most straightforward way +of achieving what `copilot-bluespec` needs. + +It is conceivable that if the Bluespec language evolves in the future, then we +will need to update `language-bluespec` accordingly. This seems somewhat +unlikely, however, as we are generating code in a very simple subset of the +Bluespec language. + +Another possibility is to split out the AST parts of `bsc` into their own +library and maintain them going forward. See +https://github.com/B-Lang-org/bsc/issues/546 for more discussion on this point. diff --git a/copilot-bluespec/Dockerfile b/copilot-bluespec/Dockerfile new file mode 100644 index 00000000..38184244 --- /dev/null +++ b/copilot-bluespec/Dockerfile @@ -0,0 +1,36 @@ +FROM ubuntu:focal + +ENV DEBIAN_FRONTEND=noninteractive +RUN apt-get update && \ + apt-get install --yes curl gcc g++ git libz-dev make libgmp3-dev libtcl8.6 libtinfo-dev wget + +ENV BSC_VER=2023.07 +RUN mkdir -p /root/bsc +RUN wget https://github.com/B-Lang-org/bsc/releases/download/$BSC_VER/bsc-$BSC_VER-ubuntu-20.04.tar.gz -O /root/bsc.tar.gz && \ + tar -xvf /root/bsc.tar.gz -C /root/bsc --strip-components=1 && \ + rm /root/bsc.tar.gz + +ENV GHCUP_VER=0.1.22.0 +RUN mkdir -p /root/.ghcup/bin +RUN wget https://downloads.haskell.org/~ghcup/$GHCUP_VER/x86_64-linux-ghcup-$GHCUP_VER -O /root/.ghcup/bin/ghcup && \ + chmod a+x /root/.ghcup/bin/ghcup + +ENV PATH=/root/bsc/bin:/root/.cabal/bin:/root/.ghcup/bin:$PATH + +ENV GHC_VER=9.4.8 +ENV CABAL_VER=3.8.1.0 +RUN ghcup install ghc $GHC_VER && \ + ghcup set ghc $GHC_VER && \ + ghcup install cabal $CABAL_VER && \ + ghcup set cabal $CABAL_VER && \ + cabal update + +COPY . /copilot-bluespec +WORKDIR /copilot-bluespec + +RUN cabal configure --enable-tests && \ + cabal build --write-ghc-environment-files=always && \ + cabal install --lib copilot . --package-env . && \ + cabal test + +ENTRYPOINT ["/usr/bin/bash"] diff --git a/copilot-bluespec/LICENSE b/copilot-bluespec/LICENSE new file mode 100644 index 00000000..d4ed5bc4 --- /dev/null +++ b/copilot-bluespec/LICENSE @@ -0,0 +1,29 @@ +2009 +BSD3 License terms + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of the developers nor the names of its contributors +may be used to endorse or promote products derived from this software +without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/copilot-bluespec/README.md b/copilot-bluespec/README.md new file mode 100644 index 00000000..e85d9e8c --- /dev/null +++ b/copilot-bluespec/README.md @@ -0,0 +1,57 @@ +[![Build Status](https://github.com/Copilot-Language/copilot-bluespec/workflows/copilot-bluespec/badge.svg)](https://github.com/Copilot-Language/copilot-bluespec/actions?query=workflow%3Acopilot-bluespec) + +# Copilot: a stream DSL +Copilot-Bluespec implements a Bluespec backend for Copilot, producing code that +is suitable for FPGAs. + +Copilot is a runtime verification framework written in Haskell. It allows the +user to write programs in a simple but powerful way using a stream-based +approach. + +Programs can be interpreted for testing, or translated Bluespec code to be +incorporated in a project, or as a standalone application. The Bluespec backend +ensures us that the output is constant in memory and time, making it suitable +for systems with hard realtime requirements. + +## Installation +Copilot-Bluespec can be found on +[Hackage](https://hackage.haskell.org/package/copilot-bluespec). It is intended +to be installed alongside a Copilot distribution by running the following +commands: + +``` +$ cabal update +$ cabal install copilot +$ cabal install copilot-bluespec +``` + +For more detailed instructions on how to install Copilot, please refer to the +[Copilot website](https://copilot-language.github.io). + +The generated Bluespec code requires `bsc` (the Bluespec compiler) in order to +be compiled. `bsc` can be downloaded +[here](https://github.com/B-Lang-org/bsc/releases). + +We also provide a [Dockerfile](Dockerfile) which automates the process of +installing Copilot, Copilot-Bluespec, and `bsc`. The Dockerfile can be built and +run using the following commands: + +``` +$ docker build -t . +$ docker run -it +``` + +Where `` is a unique name for the Docker image. + +## Further information +For further information, install instructions and documentation, please visit +the Copilot website: +[https://copilot-language.github.io](https://copilot-language.github.io) + +There is also an implementation-focused design document +[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-bluespec/DESIGN.md). + + +## License +Copilot is distributed under the BSD-3-Clause license, which can be found +[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-bluespec/LICENSE). diff --git a/copilot-bluespec/Setup.hs b/copilot-bluespec/Setup.hs new file mode 100644 index 00000000..bf689019 --- /dev/null +++ b/copilot-bluespec/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain \ No newline at end of file diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal new file mode 100644 index 00000000..6509e7e2 --- /dev/null +++ b/copilot-bluespec/copilot-bluespec.cabal @@ -0,0 +1,100 @@ +cabal-version : >= 1.10 +name : copilot-bluespec +version : 4.4 +synopsis : A compiler for Copilot targeting FPGAs. +description : + This package is a back-end from Copilot to FPGAs in Bluespec. + . + Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in + Haskell. Copilot contains an interpreter, multiple back-end compilers, and + other verification tools. + . + A tutorial, examples, and other information are available at + . + +license : BSD3 +license-file : LICENSE +maintainer : Ryan Scott +homepage : https://copilot-language.github.io +bug-reports : https://github.com/Copilot-Language/copilot-bluespec/issues +stability : Experimental +category : Language, Embedded +build-type : Simple +extra-source-files : README.md + , CHANGELOG + +author : Frank Dedden + , Alwyn Goodloe + , Ivan Perez + , Ryan Scott + +x-curation: uncurated + +source-repository head + type: git + location: https://github.com/Copilot-Language/copilot-bluespec.git + +library + default-language : Haskell2010 + hs-source-dirs : src + + ghc-options : -Wall + build-depends : base >= 4.9 && < 5 + , directory >= 1.3 && < 1.4 + , filepath >= 1.4 && < 1.6 + , pretty >= 1.1.2 && < 1.2 + + , copilot-core >= 4.4 && < 4.5 + , language-bluespec >= 0.1 && < 0.2 + + exposed-modules : Copilot.Compile.Bluespec + + other-modules : Copilot.Compile.Bluespec.CodeGen + , Copilot.Compile.Bluespec.Compile + , Copilot.Compile.Bluespec.Error + , Copilot.Compile.Bluespec.Expr + , Copilot.Compile.Bluespec.External + , Copilot.Compile.Bluespec.FloatingPoint + , Copilot.Compile.Bluespec.Name + , Copilot.Compile.Bluespec.Representation + , Copilot.Compile.Bluespec.Settings + , Copilot.Compile.Bluespec.Type + +test-suite tests + type: + exitcode-stdio-1.0 + + main-is: + Main.hs + + other-modules: + Test.Copilot.Compile.Bluespec + + Test.Copilot.Compile.Bluespec.External + + build-depends: + base + , directory + , HUnit + , QuickCheck + , extra + , ieee754 + , pretty + , process + , random + , test-framework + , test-framework-hunit + , test-framework-quickcheck2 + , unix + + , copilot-core + , copilot-bluespec + + hs-source-dirs: + tests + + default-language: + Haskell2010 + + ghc-options: + -Wall diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec.hs new file mode 100644 index 00000000..499b1cff --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec.hs @@ -0,0 +1,12 @@ +-- | Compile Copilot specifications to Bluespec code. +module Copilot.Compile.Bluespec + ( compile + , compileWith + , BluespecSettings(..) + , mkDefaultBluespecSettings + ) where + +-- Internal imports +import Copilot.Compile.Bluespec.Compile ( compile, compileWith ) +import Copilot.Compile.Bluespec.Settings ( BluespecSettings (..), + mkDefaultBluespecSettings ) diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs new file mode 100644 index 00000000..6d9fde04 --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/CodeGen.hs @@ -0,0 +1,262 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | High-level translation of Copilot Core into Bluespec. +module Copilot.Compile.Bluespec.CodeGen + ( -- * Type declarations + mkStructDecln + + -- * Ring buffers + , mkBuffDecln + , mkIndexDecln + , mkAccessDecln + + -- * Stream generators + , mkGenFun + + -- * Monitor processing + , mkStepRule + , mkTriggerRule + + -- * Module interface specifications + , mkSpecIfcFields + ) where + +-- External imports +import Data.String (IsString (..)) +import qualified Language.Bluespec.Classic.AST as BS +import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS +import qualified Language.Bluespec.Classic.AST.Builtin.Types as BS + +-- Internal imports: Copilot +import Copilot.Core + +-- Internal imports +import Copilot.Compile.Bluespec.Expr +import Copilot.Compile.Bluespec.External +import Copilot.Compile.Bluespec.Name +import Copilot.Compile.Bluespec.Representation +import Copilot.Compile.Bluespec.Type + +-- | Write a generator function for a stream. +mkGenFun :: String -> Expr a -> Type a -> BS.CDefl +mkGenFun name expr ty = + -- name :: ty + -- name = expr + BS.CLValueSign + (BS.CDef nameId (BS.CQType [] (transType ty)) [def]) + [] + where + nameId = BS.mkId BS.NoPos $ fromString $ lowercaseName name + def = BS.CClause [] [] (transExpr expr) + +-- | Bind a buffer variable and initialise it with the stream buffer. +mkBuffDecln :: forall a. Id -> Type a -> [a] -> [BS.CStmt] +mkBuffDecln sId ty xs = + initVals ++ [BS.CSletrec [initBufSig]] + where + -- sId_0 :: Reg <- mkReg xs_0 + -- ... + -- sId_(n-1) :: Reg <- mkReg xs_(n-1) + initVals = zipWith mkInitVal xs [0..] + -- sId :: Vector n (Reg ) + -- sId = update (... (update newVector 0 sId_0) ...) (n-1) sId_(n-1) + initBufSig = BS.CLValueSign + (BS.CDef nameId (BS.CQType [] vecTy) [initBufDef]) + [] + initBufDef = BS.CClause + [] + [] + (genVector + (\idx _ -> BS.CVar $ BS.mkId BS.NoPos $ + fromString $ streamElemName sId idx) + xs) + + nameId = BS.mkId BS.NoPos $ fromString $ streamName sId + bsTy = tReg `BS.TAp` transType ty + vecTy = tVector `BS.TAp` BS.cTNum numElems BS.NoPos `BS.TAp` bsTy + numElems = toInteger $ length xs + + mkInitVal :: a -> Int -> BS.CStmt + mkInitVal x elemNum = + BS.CSBindT + (BS.CPVar elemId) + Nothing + [] + (BS.CQType [] bsTy) + (BS.CApply (BS.CVar (BS.mkId BS.NoPos "mkReg")) [constTy ty x]) + where + elemName = streamElemName sId elemNum + elemId = BS.mkId BS.NoPos $ fromString elemName + +-- | Make an index variable and initialise it to 0. +mkIndexDecln :: Id -> BS.CStmt +mkIndexDecln sId = + -- sId_idx :: Reg (Bit 64) <- mkReg 0 + BS.CSBindT + (BS.CPVar nameId) + Nothing + [] + (BS.CQType [] bsTy) + (BS.CApply (BS.CVar (BS.mkId BS.NoPos "mkReg")) + [cLit $ BS.LInt $ BS.ilDec 0]) + where + nameId = BS.mkId BS.NoPos $ fromString $ indexName sId + bsTy = tReg `BS.TAp` BS.tBitN 64 BS.NoPos + +-- | Define an accessor function for the ring buffer associated with a stream +mkAccessDecln :: Id -> Type a -> [a] -> BS.CDefl +mkAccessDecln sId ty xs = + -- sId_get :: Bits 64 -> ty + -- sId_get x = (select sId ((sId_idx + x) % buffLength))._read + BS.CLValueSign (BS.CDef nameId (BS.CQType [] funTy) [def]) [] + where + def = BS.CClause [BS.CPVar argId] [] expr + argTy = BS.tBit `BS.TAp` BS.cTNum 64 BS.NoPos + retTy = transType ty + funTy = BS.tArrow `BS.TAp` argTy `BS.TAp` retTy + name = streamAccessorName sId + nameId = BS.mkId BS.NoPos $ fromString name + buffLength = cLit $ BS.LInt $ BS.ilDec $ toInteger $ length xs + argId = BS.mkId BS.NoPos "x" + index = BS.CApply (BS.CVar (BS.idPercentAt BS.NoPos)) + [ BS.CApply (BS.CVar BS.idPlus) + [ BS.CVar (BS.mkId BS.NoPos (fromString (indexName sId))) + , BS.CVar argId + ] + , buffLength + ] + indexExpr = cIndexVector + (BS.CVar (BS.mkId BS.NoPos (fromString (streamName sId)))) + index + expr = BS.CSelect indexExpr (BS.id_read BS.NoPos) + +-- | Define fields for a module interface containing a specification's trigger +-- functions and external variables. +mkSpecIfcFields :: [Trigger] -> [External] -> [BS.CField] +mkSpecIfcFields triggers exts = + map mkTriggerField triggers ++ map mkExtField exts + where + -- trigger :: args_1 -> ... -> args_n -> Action + mkTriggerField :: Trigger -> BS.CField + mkTriggerField (Trigger name _ args) = + mkField name $ + foldr + (\(UExpr arg _) res -> BS.tArrow `BS.TAp` transType arg `BS.TAp` res) + BS.tAction + args + + -- ext :: Reg ty + mkExtField :: External -> BS.CField + mkExtField (External name ty) = + mkField name $ tReg `BS.TAp` transType ty + +-- | Define a rule for a trigger function. +mkTriggerRule :: UniqueTrigger -> BS.CRule +mkTriggerRule (UniqueTrigger uniqueName (Trigger name _ args)) = + BS.CRule + [] + (Just $ cLit $ BS.LString uniqueName) + [ BS.CQFilter $ + BS.CVar $ BS.mkId BS.NoPos $ + fromString $ guardName uniqueName + ] + (BS.CApply nameExpr args') + where + ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName + -- Note that we use 'name' here instead of 'uniqueName', as 'name' is the + -- name of the actual external function. + nameId = BS.mkId BS.NoPos $ fromString $ lowercaseName name + nameExpr = BS.CSelect (BS.CVar ifcArgId) nameId + + args' = take (length args) (map argCall (argNames uniqueName)) + argCall = BS.CVar . BS.mkId BS.NoPos . fromString + +-- | Writes the @step@ rule that updates all streams. +mkStepRule :: [Stream] -> Maybe BS.CRule +mkStepRule streams + | null allUpdates + = -- If there is nothing to update, don't bother creating a step rule. + -- Doing so wouldn't harm anything, but bsc will generate a warning + -- when compiling such an empty rule. + Nothing + | otherwise + = Just $ + BS.CRule + [] + (Just $ cLit $ BS.LString "step") + [BS.CQFilter $ BS.CCon BS.idTrue []] + (BS.Caction BS.NoPos allUpdates) + where + allUpdates = bufferUpdates ++ indexUpdates + (bufferUpdates, indexUpdates) = unzip $ map mkUpdateGlobals streams + + -- Write code to update global stream buffers and index. + mkUpdateGlobals :: Stream -> (BS.CStmt, BS.CStmt) + mkUpdateGlobals (Stream sId buff _ _) = + (bufferUpdate, indexUpdate) + where + bufferUpdate = + BS.CSExpr Nothing $ + BS.Cwrite + BS.NoPos + (cIndexVector (BS.CVar buffId) (BS.CVar indexId)) + (BS.CVar genId) + + indexUpdate = + BS.CSExpr Nothing $ + BS.Cwrite + BS.NoPos + (BS.CVar indexId) + (BS.CApply (BS.CVar (BS.idPercentAt BS.NoPos)) + [incIndex, buffLength]) + where + buffLength = cLit $ BS.LInt $ BS.ilDec $ toInteger $ length buff + incIndex = BS.CApply (BS.CVar BS.idPlus) + [ BS.CVar indexId + , cLit $ BS.LInt $ BS.ilDec 1 + ] + + buffId = BS.mkId BS.NoPos $ fromString $ streamName sId + genId = BS.mkId BS.NoPos $ fromString $ generatorName sId + indexId = BS.mkId BS.NoPos $ fromString $ indexName sId + +-- | Write a struct declaration based on its definition. +mkStructDecln :: Struct a => a -> BS.CDefn +mkStructDecln x = + BS.Cstruct + True + BS.SStruct + (BS.IdK structId) + [] -- No type variables + structFields + -- Derive a Bits instance so that we can put this struct in a Reg + [BS.CTypeclass BS.idBits] + where + structId = BS.mkId BS.NoPos $ fromString $ uppercaseName $ typeName x + structFields = map mkStructField $ toValues x + + mkStructField :: Value a -> BS.CField + mkStructField (Value ty field) = + mkField (fieldName field) (transType ty) + +-- | Write a field of a struct or interface, along with its type. +mkField :: String -> BS.CType -> BS.CField +mkField name ty = + BS.CField + { BS.cf_name = BS.mkId BS.NoPos $ fromString $ lowercaseName name + , BS.cf_pragmas = Nothing + , BS.cf_type = BS.CQType [] ty + , BS.cf_default = [] + , BS.cf_orig_type = Nothing + } + +-- | The @Reg@ Bluespec interface type. +tReg :: BS.CType +tReg = BS.TCon $ + BS.TyCon + { BS.tcon_name = BS.idReg + , BS.tcon_kind = Just (BS.Kfun BS.KStar BS.KStar) + , BS.tcon_sort = BS.TIstruct (BS.SInterface []) + [BS.id_write BS.NoPos, BS.id_read BS.NoPos] + } diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Compile.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Compile.hs new file mode 100644 index 00000000..c4701eaf --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Compile.hs @@ -0,0 +1,350 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | Compile Copilot specifications to Bluespec code. +module Copilot.Compile.Bluespec.Compile + ( compile + , compileWith + ) where + +-- External imports +import Data.List (nub, nubBy, union) +import Data.Maybe (catMaybes, maybeToList) +import Data.String (IsString (..)) +import Data.Type.Equality (testEquality, (:~:)(Refl)) +import Data.Typeable (Typeable) +import qualified Language.Bluespec.Classic.AST as BS +import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS +import qualified Language.Bluespec.Classic.AST.Builtin.Types as BS +import Text.PrettyPrint.HughesPJClass (Pretty (..), render) +import System.Directory (createDirectoryIfMissing) +import System.Exit (exitFailure) +import System.FilePath (()) +import System.IO (hPutStrLn, stderr) + +-- Internal imports: Copilot +import Copilot.Core + +-- Internal imports +import Copilot.Compile.Bluespec.CodeGen +import Copilot.Compile.Bluespec.External +import Copilot.Compile.Bluespec.FloatingPoint +import Copilot.Compile.Bluespec.Name +import Copilot.Compile.Bluespec.Representation +import Copilot.Compile.Bluespec.Settings + +-- | Compile a specification to a Bluespec file. +-- +-- The first argument is the settings for the Bluespec code generated. +-- +-- The second argument is used as a module name and the prefix for the .bs files +-- that are generated. +compileWith :: BluespecSettings -> String -> Spec -> IO () +compileWith bsSettings prefix spec + | null triggers + = do hPutStrLn stderr $ + "Copilot error: attempt at compiling empty specification.\n" + ++ "You must define at least one trigger to generate Bluespec monitors." + exitFailure + + | incompatibleTriggers triggers + = do hPutStrLn stderr $ + "Copilot error: attempt at compiling specification with conflicting " + ++ "trigger definitions.\n" + ++ "Multiple triggers have the same name, but different argument " + ++ "types.\n" + exitFailure + + | otherwise + = do let typesBsFile = render $ pPrint $ compileTypesBS bsSettings prefix spec + ifcBsFile = render $ pPrint $ compileIfcBS bsSettings prefix spec + bsFile = render $ pPrint $ compileBS bsSettings prefix spec + + let dir = bluespecSettingsOutputDirectory bsSettings + createDirectoryIfMissing True dir + writeFile (dir specTypesPkgName prefix ++ ".bs") typesBsFile + writeFile (dir specIfcPkgName prefix ++ ".bs") ifcBsFile + writeFile (dir "bs_fp.c") copilotBluespecFloatingPointC + writeFile (dir "BluespecFP.bsv") copilotBluespecFloatingPointBSV + writeFile (dir prefix ++ ".bs") bsFile + where + triggers = specTriggers spec + + -- Check that two triggers do no conflict, that is: if their names are + -- equal, the types of their arguments should be equal as well. + incompatibleTriggers :: [Trigger] -> Bool + incompatibleTriggers = pairwiseAny conflict + where + conflict :: Trigger -> Trigger -> Bool + conflict t1@(Trigger name1 _ _) t2@(Trigger name2 _ _) = + name1 == name2 && not (compareTrigger t1 t2) + + -- True if the function holds for any pair of elements. We assume that + -- the function is commutative. + pairwiseAny :: (a -> a -> Bool) -> [a] -> Bool + pairwiseAny _ [] = False + pairwiseAny _ (_:[]) = False + pairwiseAny f (x:xs) = any (f x) xs || pairwiseAny f xs + +-- | Compile a specification to a Bluespec. +-- +-- The first argument is used as a prefix for the generated .bs files. +compile :: String -> Spec -> IO () +compile = compileWith mkDefaultBluespecSettings + +-- | Generate a @.bs@ file from a 'Spec'. This is the main payload of +-- the Bluespec backend. +-- +-- The generated Bluespec file will import a handful of files from the standard +-- library, as well as the following generated files: +-- +-- * @Ifc.bs@, which defines the interface containing the trigger +-- functions and external variables. +-- +-- * @Types.bs@, which defines any structs used in the 'Spec'. +-- +-- It will also generate a @mk :: Module Ifc -> Module Empty@ +-- function, which defines the module structure for this 'Spec'. The +-- @mk@ function has the following structure: +-- +-- * First, bind the argument of type @Module Ifc@ so that trigger +-- functions can be invoked and external variables can be used. +-- +-- * Next, declare stream buffers and indices. +-- +-- * Next, declare generator functions for streams, accessor functions for +-- streams, and guard functions for triggers. +-- +-- * Next, declare rules for each trigger function. +-- +-- * Finally, declare a single rule that updates the stream buffers and +-- indices. +compileBS :: BluespecSettings -> String -> Spec -> BS.CPackage +compileBS _bsSettings prefix spec = + BS.CPackage + (BS.mkId BS.NoPos (fromString prefix)) + (Right []) + (stdLibImports ++ genImports) + [] + [moduleDef] + [] + where + -- import Types + -- import Ifc + genImports :: [BS.CImport] + genImports = + [ BS.CImpId False $ BS.mkId BS.NoPos $ fromString + $ specTypesPkgName prefix + , BS.CImpId False $ BS.mkId BS.NoPos $ fromString + $ specIfcPkgName prefix + , BS.CImpId False $ BS.mkId BS.NoPos "BluespecFP" + ] + + moduleDef :: BS.CDefn + moduleDef = BS.CValueSign $ + BS.CDef + (BS.mkId BS.NoPos $ fromString $ "mk" ++ prefix) + -- :: Module Ifc -> Module Empty + (BS.CQType + [] + (BS.tArrow + `BS.TAp` (BS.tModule `BS.TAp` ifcTy) + `BS.TAp` (BS.tModule `BS.TAp` emptyTy))) + [ BS.CClause [BS.CPVar ifcModId] [] $ + BS.Cmodule BS.NoPos $ + BS.CMStmt + (BS.CSBind (BS.CPVar ifcArgId) Nothing [] (BS.CVar ifcModId)) + : map BS.CMStmt mkGlobals ++ + [ BS.CMStmt $ BS.CSletrec genFuns + , BS.CMrules $ BS.Crules [] rules + ] + ] + + ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName + ifcModId = BS.mkId BS.NoPos "ifcMod" + + rules :: [BS.CRule] + rules = map mkTriggerRule uniqueTriggers ++ maybeToList (mkStepRule streams) + + streams = specStreams spec + triggers = specTriggers spec + uniqueTriggers = mkUniqueTriggers triggers + exts = gatherExts streams triggers + + ifcId = BS.mkId BS.NoPos $ fromString $ specIfcName prefix + ifcFields = mkSpecIfcFields triggers exts + ifcTy = BS.TCon (BS.TyCon + { BS.tcon_name = ifcId + , BS.tcon_kind = Just BS.KStar + , BS.tcon_sort = BS.TIstruct + (BS.SInterface []) + (map BS.cf_name ifcFields) + }) + + emptyTy = BS.TCon (BS.TyCon + { BS.tcon_name = BS.idEmpty + , BS.tcon_kind = Just BS.KStar + , BS.tcon_sort = BS.TIstruct (BS.SInterface []) [] + }) + + -- Make buffer and index declarations for streams. + mkGlobals :: [BS.CStmt] + mkGlobals = concatMap buffDecln streams ++ map indexDecln streams + where + buffDecln (Stream sId buff _ ty) = mkBuffDecln sId ty buff + indexDecln (Stream sId _ _ _ ) = mkIndexDecln sId + + -- Make generator functions, including trigger arguments. + genFuns :: [BS.CDefl] + genFuns = map accessDecln streams + ++ map streamGen streams + ++ concatMap triggerGen uniqueTriggers + where + accessDecln :: Stream -> BS.CDefl + accessDecln (Stream sId buff _ ty) = mkAccessDecln sId ty buff + + streamGen :: Stream -> BS.CDefl + streamGen (Stream sId _ expr ty) = mkGenFun (generatorName sId) expr ty + + triggerGen :: UniqueTrigger -> [BS.CDefl] + triggerGen (UniqueTrigger uniqueName (Trigger _name guard args)) = + guardDef : argDefs + where + guardDef = mkGenFun (guardName uniqueName) guard Bool + argDefs = map argGen (zip (argNames uniqueName) args) + + argGen :: (String, UExpr) -> BS.CDefl + argGen (argName, UExpr ty expr) = mkGenFun argName expr ty + +-- | Generate a @Ifc.bs@ file from a 'Spec'. This contains the +-- definition of the @Ifc@ interface, which declares the types of all +-- trigger functions and external variables. This is put in a separate file so +-- that larger applications can use it separately. +compileIfcBS :: BluespecSettings -> String -> Spec -> BS.CPackage +compileIfcBS _bsSettings prefix spec = + BS.CPackage + ifcPkgId + (Right []) + (stdLibImports ++ genImports) + [] + [ifcDef] + [] + where + -- import Types + genImports :: [BS.CImport] + genImports = + [ BS.CImpId False $ BS.mkId BS.NoPos $ fromString + $ specTypesPkgName prefix + ] + + ifcId = BS.mkId BS.NoPos $ fromString $ specIfcName prefix + ifcPkgId = BS.mkId BS.NoPos $ fromString $ specIfcPkgName prefix + ifcFields = mkSpecIfcFields triggers exts + + streams = specStreams spec + exts = gatherExts streams triggers + + -- Remove duplicates due to multiple guards for the same trigger. + triggers = nubBy compareTrigger (specTriggers spec) + + ifcDef :: BS.CDefn + ifcDef = BS.Cstruct + True + (BS.SInterface []) + (BS.IdK ifcId) + [] -- No type variables + ifcFields + [] -- No derived instances + +-- | Generate a @Types.bs@ file from a 'Spec'. This declares the types +-- of any structs used by the Copilot specification. This is put in a separate +-- file so that larger applications can more easily substitute their own struct +-- definitions if desired. +compileTypesBS :: BluespecSettings -> String -> Spec -> BS.CPackage +compileTypesBS _bsSettings prefix spec = + BS.CPackage + typesId + (Right []) + stdLibImports + [] + structDefs + [] + where + typesId = BS.mkId BS.NoPos $ fromString $ specTypesPkgName prefix + + structDefs = mkTypeDeclns exprs + + exprs = gatherExprs streams triggers + streams = specStreams spec + + -- Remove duplicates due to multiple guards for the same trigger. + triggers = nubBy compareTrigger (specTriggers spec) + + -- Generate type declarations. + mkTypeDeclns :: [UExpr] -> [BS.CDefn] + mkTypeDeclns es = catMaybes $ map mkTypeDecln uTypes + where + uTypes = nub $ concatMap (\(UExpr _ e) -> exprTypes e) es + + mkTypeDecln (UType ty) = case ty of + Struct x -> Just $ mkStructDecln x + _ -> Nothing + +-- | Imports from the Bluespec standard library. +stdLibImports :: [BS.CImport] +stdLibImports = + [ BS.CImpId False $ BS.mkId BS.NoPos "FloatingPoint" + , BS.CImpId False $ BS.mkId BS.NoPos "Vector" + ] + +-- ** Obtain information from Copilot Core Exprs and Types. + +-- | List all types of an expression, returns items uniquely. +exprTypes :: Typeable a => Expr a -> [UType] +exprTypes e = case e of + Const ty _ -> typeTypes ty + Local ty1 ty2 _ e1 e2 -> typeTypes ty1 `union` typeTypes ty2 + `union` exprTypes e1 `union` exprTypes e2 + Var ty _ -> typeTypes ty + Drop ty _ _ -> typeTypes ty + ExternVar ty _ _ -> typeTypes ty + Op1 _ e1 -> exprTypes e1 + Op2 _ e1 e2 -> exprTypes e1 `union` exprTypes e2 + Op3 _ e1 e2 e3 -> exprTypes e1 `union` exprTypes e2 + `union` exprTypes e3 + Label ty _ _ -> typeTypes ty + +-- | List all types of a type, returns items uniquely. +typeTypes :: Typeable a => Type a -> [UType] +typeTypes ty = case ty of + Array ty' -> typeTypes ty' `union` [UType ty] + Struct x -> concatMap (\(Value ty' _) -> typeTypes ty') (toValues x) + `union` [UType ty] + _ -> [UType ty] + +-- | Collect all expression of a list of streams and triggers and wrap them +-- into an UEXpr. +gatherExprs :: [Stream] -> [Trigger] -> [UExpr] +gatherExprs streams triggers = map streamUExpr streams + ++ concatMap triggerUExpr triggers + where + streamUExpr (Stream _ _ expr ty) = UExpr ty expr + triggerUExpr (Trigger _ guard args) = UExpr Bool guard : args + +-- | We consider triggers to be equal, if their names match and the number and +-- types of arguments. +compareTrigger :: Trigger -> Trigger -> Bool +compareTrigger (Trigger name1 _ args1) (Trigger name2 _ args2) + = name1 == name2 && compareArguments args1 args2 + + where + compareArguments :: [UExpr] -> [UExpr] -> Bool + compareArguments [] [] = True + compareArguments [] _ = False + compareArguments _ [] = False + compareArguments (x:xs) (y:ys) = compareUExpr x y && compareArguments xs ys + + compareUExpr :: UExpr -> UExpr -> Bool + compareUExpr (UExpr ty1 _) (UExpr ty2 _) + | Just Refl <- testEquality ty1 ty2 = True + | otherwise = False diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Error.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Error.hs new file mode 100644 index 00000000..b3d719da --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Error.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE Safe #-} + +-- | +-- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc. +-- +-- Custom functions to report error messages to users. +module Copilot.Compile.Bluespec.Error + ( impossible ) + where + +-- | Report an error due to a bug in Copilot. +impossible :: String -- ^ Name of the function in which the error was detected. + -> String -- ^ Name of the package in which the function is located. + -> a +impossible function package = + error $ "Impossible error in function " + ++ function ++ ", in package " ++ package + ++ ". Please file an issue at " + ++ "https://github.com/Copilot-Language/copilot/issues" + ++ " or email the maintainers at " diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs new file mode 100644 index 00000000..c4978aef --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs @@ -0,0 +1,671 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | Translate Copilot Core expressions and operators to Bluespec. +module Copilot.Compile.Bluespec.Expr + ( transExpr + , cIndexVector + , cLit + , constTy + , genVector + ) where + +-- External imports +import Data.Foldable (foldl') +import Data.String (IsString (..)) +import qualified Language.Bluespec.Classic.AST as BS +import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS + +-- Internal imports: Copilot +import Copilot.Core + +-- Internal imports +import Copilot.Compile.Bluespec.Error (impossible) +import Copilot.Compile.Bluespec.Name +import Copilot.Compile.Bluespec.Type + +-- | Translates a Copilot Core expression into a Bluespec expression. +transExpr :: Expr a -> BS.CExpr +transExpr (Const ty x) = constTy ty x + +transExpr (Local ty1 _ name e1 e2) = + let nameId = BS.mkId BS.NoPos $ fromString name + e1' = transExpr e1 + ty1' = transType ty1 + e2' = transExpr e2 in + BS.Cletrec + [ BS.CLValueSign + (BS.CDef nameId (BS.CQType [] ty1') [BS.CClause [] [] e1']) + [] + ] + e2' + +transExpr (Var _ n) = BS.CVar $ BS.mkId BS.NoPos $ fromString n + +transExpr (Drop _ amount sid) = + let accessVar = streamAccessorName sid + index = BS.LInt $ BS.ilDec $ fromIntegral amount in + BS.CApply (BS.CVar $ BS.mkId BS.NoPos $ fromString accessVar) + [BS.CLit $ BS.CLiteral BS.NoPos index] + +transExpr (ExternVar _ name _) = + let ifcArgId = BS.mkId BS.NoPos $ fromString ifcArgName in + BS.CSelect + (BS.CSelect + (BS.CVar ifcArgId) + (BS.mkId BS.NoPos $ fromString $ lowercaseName name)) + (BS.id_read BS.NoPos) + +transExpr (Label _ _ e) = transExpr e -- ignore label + +transExpr (Op1 op e) = transOp1 op (transExpr e) + +transExpr (Op2 op e1 e2) = transOp2 op (transExpr e1) (transExpr e2) + +transExpr (Op3 op e1 e2 e3) = + transOp3 op (transExpr e1) (transExpr e2) (transExpr e3) + +-- | Translates a Copilot unary operator and its argument into a Bluespec +-- function. +transOp1 :: Op1 a b -> BS.CExpr -> BS.CExpr +transOp1 op e = + case op of + Not -> app BS.idNot + Abs _ty -> app $ BS.mkId BS.NoPos "abs" + Sign ty -> transSign ty e + -- Bluespec's Arith class does not have a `recip` method corresponding to + -- Haskell's `recip` in the `Fractional` class, so we implement it + -- ourselves. + Recip ty -> BS.CApply + (BS.CVar (BS.idSlashAt BS.NoPos)) + [constNumTy ty 1, e] + BwNot _ty -> app $ BS.idInvertAt BS.NoPos + + Cast fromTy toTy -> transCast fromTy toTy e + GetField (Struct _) _ f -> BS.CSelect e $ BS.mkId BS.NoPos $ + fromString $ lowercaseName $ accessorName f + GetField _ _ _ -> impossible "transOp1" "copilot-bluespec" + + -- BDPI-supported operations + Sqrt ty -> appFP ty "sqrt" + Exp ty -> appFP ty "exp" + Log ty -> appFP ty "log" + Acos ty -> appFP ty "acos" + Asin ty -> appFP ty "asin" + Atan ty -> appFP ty "atan" + Cos ty -> appFP ty "cos" + Sin ty -> appFP ty "sin" + Tan ty -> appFP ty "tan" + Acosh ty -> appFP ty "acosh" + Asinh ty -> appFP ty "asinh" + Atanh ty -> appFP ty "atanh" + Cosh ty -> appFP ty "cosh" + Sinh ty -> appFP ty "sinh" + Tanh ty -> appFP ty "tanh" + Ceiling ty -> appFP ty "ceiling" + Floor ty -> appFP ty "floor" + where + app :: BS.Id -> BS.CExpr + app i = BS.CApply (BS.CVar i) [e] + + appFP :: forall t. Type t -> String -> BS.CExpr + appFP ty funPrefix = app $ fpFunId ty funPrefix + +-- | Translates a Copilot binary operator and its arguments into a Bluespec +-- function. +transOp2 :: Op2 a b c -> BS.CExpr -> BS.CExpr -> BS.CExpr +transOp2 op e1 e2 = + case op of + And -> app BS.idAnd + Or -> app $ BS.idOrAt BS.NoPos + Add _ty -> app BS.idPlus + Sub _ty -> app BS.idMinus + Mul _ty -> app $ BS.idStarAt BS.NoPos + Mod _ty -> app $ BS.idPercentAt BS.NoPos + Div _ty -> app $ BS.idSlashAt BS.NoPos + Fdiv _ty -> app $ BS.idSlashAt BS.NoPos + Eq _ -> app BS.idEqual + Ne _ -> app BS.idNotEqual + Le ty -> transLe ty e1 e2 + Ge ty -> transGe ty e1 e2 + Lt ty -> transLt ty e1 e2 + Gt ty -> transGt ty e1 e2 + BwAnd _ -> app $ BS.idBitAndAt BS.NoPos + BwOr _ -> app $ BS.idBitOrAt BS.NoPos + BwXor _ -> app $ BS.idCaretAt BS.NoPos + BwShiftL _ _ -> app $ BS.idLshAt BS.NoPos + BwShiftR _ _ -> app $ BS.idRshAt BS.NoPos + Index _ -> cIndexVector e1 e2 + UpdateField (Struct _) _ f -> + let field :: BS.FString + field = fromString $ lowercaseName $ accessorName f in + BS.CStructUpd e1 [(BS.mkId BS.NoPos field, e2)] + UpdateField _ _ _ -> impossible "transOp2" "copilot-bluespec" + + -- BDPI-supported operations + Pow ty -> appFP ty "pow" + Logb ty -> appFP ty "logb" + Atan2 ty -> appFP ty "atan2" + where + app :: BS.Id -> BS.CExpr + app i = BS.CApply (BS.CVar i) [e1, e2] + + appFP :: forall t. Type t -> String -> BS.CExpr + appFP ty funPrefix = app $ fpFunId ty funPrefix + +-- | Translates a Copilot ternary operator and its arguments into a Bluespec +-- function. +transOp3 :: Op3 a b c d -> BS.CExpr -> BS.CExpr -> BS.CExpr -> BS.CExpr +transOp3 op e1 e2 e3 = + case op of + Mux _ -> BS.Cif BS.NoPos e1 e2 e3 + UpdateArray _ -> cUpdateVector e1 e2 e3 + +-- | Translate @'Sign' e@ in Copilot Core into a Bluespec expression. +-- +-- @signum e@ is translated as: +-- +-- @ +-- if e > 0 then 1 else (if e < 0 then negate 1 else e) +-- @ +-- +-- That is: +-- +-- 1. If @e@ is positive, return @1@. +-- +-- 2. If @e@ is negative, return @-1@. +-- +-- 3. Otherwise, return @e@. This handles the case where @e@ is @0@ when the +-- type is an integral type. If the type is a floating-point type, it also +-- handles the cases where @e@ is @-0@ or @NaN@. +-- +-- This implementation is modeled after how GHC implements 'signum' +-- . +transSign :: Type a -> BS.CExpr -> BS.CExpr +transSign ty e = positiveCase $ negativeCase e + where + -- If @e@ is positive, return @1@, otherwise fall back to the argument. + -- + -- Produces the following code, where @@ is the argument to this + -- function: + -- @ + -- if e > 0 then 1 else + -- @ + positiveCase :: BS.CExpr -- ^ Value returned if @e@ is not positive. + -> BS.CExpr + positiveCase = + BS.Cif BS.NoPos (transGt ty e (constNumTy ty 0)) (constNumTy ty 1) + + -- If @e@ is negative, return @1@, otherwise fall back to the argument. + -- + -- Produces the following code, where @@ is the argument to this + -- function: + -- @ + -- if e < 0 then negate 1 else + -- @ + negativeCase :: BS.CExpr -- ^ Value returned if @e@ is not negative. + -> BS.CExpr + negativeCase = + BS.Cif BS.NoPos (transLt ty e (constNumTy ty 0)) (constNumTy ty (-1)) + +-- | Translate a Copilot @x < y@ expression into Bluespec. We will generate +-- different code depending on whether the arguments have a floating-point type +-- or not. +transLt :: Type a + -- ^ The type of the arguments. + -> BS.CExpr -> BS.CExpr -> BS.CExpr +transLt ty e1 e2 + | typeIsFloating ty + = transLtOrGtFP (BS.mkId BS.NoPos "LT") e1 e2 + | otherwise + = BS.CApply (BS.CVar (BS.idLtAt BS.NoPos)) [e1, e2] + +-- | Translate a Copilot @x > y@ expression into Bluespec. We will generate +-- different code depending on whether the arguments have a floating-point type +-- or not. +transGt :: Type a + -- ^ The type of the arguments. + -> BS.CExpr -> BS.CExpr -> BS.CExpr +transGt ty e1 e2 + | typeIsFloating ty + = transLtOrGtFP (BS.mkId BS.NoPos "GT") e1 e2 + | otherwise + = BS.CApply (BS.CVar (BS.idGtAt BS.NoPos)) [e1, e2] + +-- | Translate a Copilot @x <= y@ expression into Bluespec. We will generate +-- different code depending on whether the arguments have a floating-point type +-- or not. +transLe :: Type a + -- ^ The type of the arguments. + -> BS.CExpr -> BS.CExpr -> BS.CExpr +transLe ty e1 e2 + | typeIsFloating ty + = transLeOrGeFP (BS.mkId BS.NoPos "LT") e1 e2 + | otherwise + = BS.CApply (BS.CVar (BS.idLtEqAt BS.NoPos)) [e1, e2] + +-- | Translate a Copilot @x >= y@ expression into Bluespec. We will generate +-- different code depending on whether the arguments have a floating-point type +-- or not. +transGe :: Type a + -- ^ The type of the arguments. + -> BS.CExpr -> BS.CExpr -> BS.CExpr +transGe ty e1 e2 + | typeIsFloating ty + = transLeOrGeFP (BS.mkId BS.NoPos "GT") e1 e2 + | otherwise + = BS.CApply (BS.CVar (BS.idGtEqAt BS.NoPos)) [e1, e2] + +-- | Translate a Copilot floating-point comparison involving @<@ or @>@ into a +-- Bluespec expression. Specifically, @x < y@ is translated to: +-- +-- @ +-- compareFP x y == LT +-- @ +-- +-- @x > y@ is translated similarly, except that @GT@ is used instead of @LT@. +-- +-- See the comments on 'compareFPExpr' for why we translate floating-point +-- comparison operators this way. +transLtOrGtFP :: BS.Id + -- ^ A @Disorder@ label, which we check against the result of + -- calling @compareFP@. This should be either @LT@ or @GT@. + -> BS.CExpr -> BS.CExpr -> BS.CExpr +transLtOrGtFP disorderLabel e1 e2 = + BS.CApply + (BS.CVar BS.idEqual) + [compareFPExpr e1 e2, BS.CCon disorderLabel []] + +-- | Translate a Copilot floating-point comparison involving @<=@ or @>=@ into +-- a Bluespec expression. Specifically, @x <= y@ is translated to: +-- +-- @ +-- let _c = compareFP x y +-- in (_c == LT) || (_c == EQ) +-- @ +-- +-- @x >= y@ is translated similarly, except that @GT@ is used instead of @LT@. +-- +-- See the comments on 'compareFPExpr' for why we translate floating-point +-- comparison operators this way. +transLeOrGeFP :: BS.Id + -- ^ A @Disorder@ label, which we check against the result of + -- calling @compareFP@. This should be either @LT@ or @GT@. + -> BS.CExpr -> BS.CExpr -> BS.CExpr +transLeOrGeFP disorderLabel e1 e2 = + BS.Cletrec + [BS.CLValue c [BS.CClause [] [] (compareFPExpr e1 e2)] []] + (BS.CApply + (BS.CVar (BS.idOrAt BS.NoPos)) + [ BS.CApply + (BS.CVar BS.idEqual) + [BS.CVar c, BS.CCon disorderLabel []] + , BS.CApply + (BS.CVar BS.idEqual) + [BS.CVar c, BS.CCon (BS.mkId BS.NoPos "EQ") []] + ]) + where + c = BS.mkId BS.NoPos "_c" + +-- | Generate an expression of the form @compareFP x y@. This is used to power +-- the translations of the Copilot @<@, @<=@, @>@, and @>=@ floating-point +-- operators to Bluespec. +-- +-- Translating these operators using @compareFP@ is a somewhat curious design +-- choice, given that Bluespec already defines its own versions of these +-- operators. Unfortunately, we cannot directly use the Bluespec versions of +-- these operators, as they are defined in such a way that they will call +-- @error@ when one of the arguments is a NaN value. This would pose two +-- problems: +-- +-- 1. This would differ from the semantics of Copilot, where @x < y@ will return +-- @False@ (instead of erroring) when one of the arguments is NaN. (Similarly +-- for the other floating-point comparison operators.) +-- +-- 2. Moreover, if you have a Bluespec program that calls @x < y@, where the +-- value of @x@ or @y@ is derived from a register, then @bsc@ will always +-- fail to compile the code. This is because Bluespec must generate hardware +-- for all possible code paths in @<@, and because one of the code paths +-- calls @error@, this will cause compilation to result in an error. (See +-- https://github.com/B-Lang-org/bsc/discussions/711#discussioncomment-10003586 +-- for a more detailed explanation.) +-- +-- As such, we avoid using Bluespec's comparison operators and instead translate +-- Copilot's comparison operators to expressions derived from @compareFP@. +-- Unlike Bluespec's other comparison operators, calling @compareFP@ will never +-- result in an error. +compareFPExpr :: BS.CExpr -> BS.CExpr -> BS.CExpr +compareFPExpr e1 e2 = + BS.CApply + (BS.CVar (BS.mkId BS.NoPos "compareFP")) + [e1, e2] + +-- | Bluespec does not have a general-purpose casting operation, so we must +-- handle casts on a case-by-case basis. +transCast :: Type a -> Type b -> BS.CExpr -> BS.CExpr +transCast fromTy toTy = + case (fromTy, toTy) of + ----- + -- "safe" casts that cannot lose information + ----- + + (Bool, Bool) -> id + (Bool, Word8) -> upcastBool + (Bool, Word16) -> upcastBool + (Bool, Word32) -> upcastBool + (Bool, Word64) -> upcastBool + (Bool, Int8) -> upcastBool + (Bool, Int16) -> upcastBool + (Bool, Int32) -> upcastBool + (Bool, Int64) -> upcastBool + + (Int8, Int8) -> id + (Int8, Int16) -> upcast + (Int8, Int32) -> upcast + (Int8, Int64) -> upcast + (Int16, Int16) -> id + (Int16, Int32) -> upcast + (Int16, Int64) -> upcast + (Int32, Int32) -> id + (Int32, Int64) -> upcast + (Int64, Int64) -> id + + (Word8, Int16) -> unpackPackUpcast Word16 + (Word8, Int32) -> unpackPackUpcast Word32 + (Word8, Int64) -> unpackPackUpcast Word64 + (Word8, Word8) -> id + (Word8, Word16) -> upcast + (Word8, Word32) -> upcast + (Word8, Word64) -> upcast + (Word16, Int32) -> unpackPackUpcast Word32 + (Word16, Int64) -> unpackPackUpcast Word64 + (Word16, Word16) -> id + (Word16, Word32) -> upcast + (Word16, Word64) -> upcast + (Word32, Int64) -> unpackPackUpcast Word64 + (Word32, Word32) -> id + (Word32, Word64) -> upcast + (Word64, Word64) -> id + + ----- + -- "unsafe" casts, which may lose information + ----- + + -- unsigned truncations + (Word64, Word32) -> downcast + (Word64, Word16) -> downcast + (Word64, Word8) -> downcast + (Word32, Word16) -> downcast + (Word32, Word8) -> downcast + (Word16, Word8) -> downcast + + -- signed truncations + (Int64, Int32) -> downcast + (Int64, Int16) -> downcast + (Int64, Int8) -> downcast + (Int32, Int16) -> downcast + (Int32, Int8) -> downcast + (Int16, Int8) -> downcast + + -- signed integer to float + (Int64, Float) -> castIntegralToFloatingPoint + (Int32, Float) -> castIntegralToFloatingPoint + (Int16, Float) -> castIntegralToFloatingPoint + (Int8, Float) -> castIntegralToFloatingPoint + + -- unsigned integer to float + (Word64, Float) -> castIntegralToFloatingPoint + (Word32, Float) -> castIntegralToFloatingPoint + (Word16, Float) -> castIntegralToFloatingPoint + (Word8, Float) -> castIntegralToFloatingPoint + + -- signed integer to double + (Int64, Double) -> castIntegralToFloatingPoint + (Int32, Double) -> castIntegralToFloatingPoint + (Int16, Double) -> castIntegralToFloatingPoint + (Int8, Double) -> castIntegralToFloatingPoint + + -- unsigned integer to double + (Word64, Double) -> castIntegralToFloatingPoint + (Word32, Double) -> castIntegralToFloatingPoint + (Word16, Double) -> castIntegralToFloatingPoint + (Word8, Double) -> castIntegralToFloatingPoint + + -- unsigned to signed conversion + (Word64, Int64) -> unpackPack + (Word32, Int32) -> unpackPack + (Word16, Int16) -> unpackPack + (Word8, Int8) -> unpackPack + + -- signed to unsigned conversion + (Int64, Word64) -> unpackPack + (Int32, Word32) -> unpackPack + (Int16, Word16) -> unpackPack + (Int8, Word8) -> unpackPack + + _ -> impossible "transCast" "copilot-bluespec" + where + -- unpackPack :: (Bits fromTy n, Bits toTy n) => fromTy -> toTy + -- unpackPack e = (unpack (pack e)) :: toTy + -- + -- The most basic cast. Used when fromTy and toTy are both integral types + -- with the same number of bits. + unpackPack :: BS.CExpr -> BS.CExpr + unpackPack e = withTypeAnnotation toTy $ + BS.CApply + (BS.CVar BS.idUnpack) + [BS.CApply (BS.CVar BS.idPack) [e]] + + -- upcastBool :: (Add k 1 n, Bits toTy n) => Bool -> toTy + -- upcastBool b = (unpack (extend (pack b))) :: toTy + -- + -- Cast a Bool to a `Bits 1` value, extend it to `Bits n`, and then + -- convert it back to an integral type. + upcastBool :: BS.CExpr -> BS.CExpr + upcastBool e = withTypeAnnotation toTy $ + BS.CApply + (BS.CVar BS.idUnpack) + [BS.CApply extendExpr [BS.CApply (BS.CVar BS.idPack) [e]]] + + -- upcast :: (BitExtend m n x) => x m -> x n + -- upcast e = (extend e) :: ty + -- + -- Convert a narrower integral type to a wider integral type (e.g., + -- `UInt 8` to `UInt 64` or `Int 8` to `Int 64`). Note that the `extend` + -- operation is smart enough to choose between sign-extension and + -- zero-extension depending on whether `x m` (i.e., fromTy) is a signed + -- or unsigned type, respectively. + upcast :: BS.CExpr -> BS.CExpr + upcast e = withTypeAnnotation toTy $ BS.CApply extendExpr [e] + + -- downcast :: (BitExtend m n x) => x n -> x m + -- downcast e = (truncate e) :: ty + -- + -- Convert a wider integral type to a narrow integral type (e.g., + -- `UInt 64` to `UInt 8` or `Int 64` to `Int 8`) by truncating the most + -- significant bits. + downcast :: BS.CExpr -> BS.CExpr + downcast e = withTypeAnnotation toTy $ BS.CApply truncateExpr [e] + + -- Apply upcast followed by unpackPack. This requires supplying the type to + -- upcast to for type disambiguation purposes. + unpackPackUpcast :: Type a -> BS.CExpr -> BS.CExpr + unpackPackUpcast upcastTy e = unpackPack $ + withTypeAnnotation upcastTy $ BS.CApply extendExpr [e] + + -- castIntegralToFloatingPoint :: (FixedFloatCVT fromTy toTy) => fromTy toTy + -- castIntegralToFloatingPoint e = + -- ((vFixedToFloat e (0 :: UInt 64) Rnd_Nearest_Even).fst) :: tfl + -- + -- While FloatingPoint does have a Bits instance, we don't want to convert + -- an integral type to a FloatingPoint type using the Bits class, as the + -- bit representation of an integral value differs quite a bit from the bit + -- representation of a FloatingPoint value. Instead, we use the + -- special-purpose FixedFloatCVT class for this task. + castIntegralToFloatingPoint :: BS.CExpr -> BS.CExpr + castIntegralToFloatingPoint e = + withTypeAnnotation toTy $ + BS.CSelect + (BS.CApply + (BS.CVar (BS.mkId BS.NoPos "vFixedToFloat")) + [ e + , constNumTy Word64 0 + , fpRM + ]) + BS.idPrimFst + + extendExpr = BS.CVar $ BS.mkId BS.NoPos "extend" + truncateExpr = BS.CVar $ BS.mkId BS.NoPos "truncate" + +-- | Transform a Copilot Core literal, based on its value and type, into a +-- Bluespec expression. +constTy :: Type a -> a -> BS.CExpr +constTy ty = + case ty of + -- The treatment of scalar types is relatively straightforward. Note that + -- Bool is an enum, so we must construct it using a CCon rather than with + -- a CLit. + Bool -> \v -> BS.CCon (if v then BS.idTrue else BS.idFalse) [] + Int8 -> constInt ty . toInteger + Int16 -> constInt ty . toInteger + Int32 -> constInt ty . toInteger + Int64 -> constInt ty . toInteger + Word8 -> constInt ty . toInteger + Word16 -> constInt ty . toInteger + Word32 -> constInt ty . toInteger + Word64 -> constInt ty . toInteger + Float -> constFP ty . realToFrac + Double -> constFP ty + + -- Translating a Copilot array literal to a Bluespec Vector is somewhat + -- involved. Given a Copilot array {x_0, ..., x_(n-1)}, the + -- corresponding Bluespec Vector will look something like: + -- + -- let arr = update (... (update newVector 0 x_0)) (n-1) x_(n-1) + -- + -- We use the `update` function instead of the := syntax (e.g., + -- { array_temp[0] := x; array_temp[1] := y; ...}) so that we can construct + -- a Vector in a pure context. + Array ty' -> constVector ty' . arrayElems + + -- Converting a Copilot struct { field_0 = x_0, ..., field_(n-1) = x_(n-1) } + -- to a Bluespec struct is quite straightforward, given Bluespec's struct + -- initialization syntax. + Struct s -> \v -> + BS.CStruct + (Just True) + (BS.mkId BS.NoPos $ fromString $ uppercaseName $ typeName s) + (map (\(Value ty'' field@(Field val)) -> + ( BS.mkId BS.NoPos $ fromString + $ lowercaseName + $ fieldName field + , constTy ty'' val + )) + (toValues v)) + +-- | Transform a list of Copilot Core expressions of a given 'Type' into a +-- Bluespec @Vector@ expression. +constVector :: Type a -> [a] -> BS.CExpr +constVector ty = genVector (\_ -> constTy ty) + +-- | Transform a list of Copilot Core expressions into a Bluespec @Vector@ +-- expression. When invoking @genVector f es@, where @es@ has length @n@, the +-- resulting @Vector@ will consist of +-- @[f 0 (es !! 0), f 1 (es !! 1), ..., f (n-1) (es !! (n-1))]@. +genVector :: (Int -> a -> BS.CExpr) -> [a] -> BS.CExpr +genVector f vec = + snd $ + foldl' + (\(!i, !v) x -> + ( i+1 + , cUpdateVector + v + (cLit (BS.LInt (BS.ilDec (toInteger i)))) + (f i x) + )) + (0, BS.CVar (BS.mkId BS.NoPos "newVector")) + vec + +-- | Translate a literal number of type @ty@ into a Bluespec expression. +-- +-- PRE: The type of PRE is numeric (integer or floating-point), that +-- is, not boolean, struct or array. +constNumTy :: Type a -> Integer -> BS.CExpr +constNumTy ty = + case ty of + Float -> constFP ty . fromInteger + Double -> constFP ty . fromInteger + _ -> constInt ty + +-- | Translate a Copilot integer literal into a Bluespec expression. +constInt :: Type a -> Integer -> BS.CExpr +constInt ty i + -- Bluespec intentionally does not support negative literal syntax (e.g., + -- -42), so we must create negative integer literals using the `negate` + -- function. + | i >= 0 = withTypeAnnotation ty $ cLit $ BS.LInt $ BS.ilDec i + | otherwise = withTypeAnnotation ty $ + BS.CApply + (BS.CVar $ BS.idNegateAt BS.NoPos) + [cLit $ BS.LInt $ BS.ilDec $ negate i] + +-- | Translate a Copilot floating-point literal into a Bluespec expression. +constFP :: Type ty -> Double -> BS.CExpr +constFP ty d + -- Bluespec intentionally does not support negative literal syntax (e.g., + -- -42.5), so we must create negative floating-point literals using the + -- `negate` function. + | d >= 0 = withTypeAnnotation ty $ cLit $ BS.LReal d + | otherwise = withTypeAnnotation ty $ + BS.CApply + (BS.CVar $ BS.idNegateAt BS.NoPos) + [cLit $ BS.LReal $ negate d] + +-- | Create a Bluespec expression consisting of a literal. +cLit :: BS.Literal -> BS.CExpr +cLit = BS.CLit . BS.CLiteral BS.NoPos + +-- | Create a Bluespec expression that indexes into a @Vector@. +cIndexVector :: BS.CExpr -> BS.CExpr -> BS.CExpr +cIndexVector vec idx = + BS.CApply (BS.CVar (BS.mkId BS.NoPos "select")) [vec, idx] + +-- | Create a Bluespec expression that updates a @Vector@ element at a +-- particular index. +cUpdateVector :: BS.CExpr -> BS.CExpr -> BS.CExpr -> BS.CExpr +cUpdateVector vec idx newElem = + BS.CApply + (BS.CVar (BS.mkId BS.NoPos "update")) + [vec, idx, newElem] + +-- | Create a Bluespec identifier for a floating-point function that Bluespec +-- imports using BDPI. +fpFunId :: Type a -> String -> BS.Id +fpFunId ty funPrefix = + BS.mkId BS.NoPos $ fromString $ "bs_fp_" ++ funName + where + funName :: String + funName = + case ty of + Float -> funPrefix ++ "f" + Double -> funPrefix + _ -> impossible "fpFunId" "copilot-bluespec" + +-- | Explicitly annotate an expression with a type signature. This is necessary +-- to prevent expressions from having ambiguous types in certain situations. +withTypeAnnotation :: Type a -> BS.CExpr -> BS.CExpr +withTypeAnnotation ty e = e `BS.CHasType` BS.CQType [] (transType ty) + +-- | True if the type given is a floating point number. +typeIsFloating :: Type a -> Bool +typeIsFloating Float = True +typeIsFloating Double = True +typeIsFloating _ = False + +-- | We assume round-near-even throughout, but this variable can be changed if +-- needed. This matches the behavior of @fpRM@ in @copilot-theorem@'s +-- @Copilot.Theorem.What4.Translate@ module. +fpRM :: BS.CExpr +fpRM = BS.CCon (BS.mkId BS.NoPos "Rnd_Nearest_Even") [] diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/External.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/External.hs new file mode 100644 index 00000000..6d42105b --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/External.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE ExistentialQuantification #-} + +-- | Represent information about externs needed in the generation of Bluespec +-- code for stream declarations and triggers. +module Copilot.Compile.Bluespec.External + ( External(..) + , gatherExts + ) where + +-- External imports +import Data.List (unionBy) + +-- Internal imports: Copilot +import Copilot.Core ( Expr (..), Stream (..), Trigger (..), Type, UExpr (..) ) + +-- | Representation of external variables. +data External = forall a. External + { extName :: String + , extType :: Type a + } + +-- | Collect all external variables from the streams and triggers. +-- +-- Although Copilot specifications can contain also properties and theorems, +-- the Bluespec backend currently only generates code for streams and triggers. +gatherExts :: [Stream] -> [Trigger] -> [External] +gatherExts streams triggers = streamsExts `extUnion` triggersExts + where + streamsExts = foldr (extUnion . streamExts) mempty streams + triggersExts = foldr (extUnion . triggerExts) mempty triggers + + streamExts :: Stream -> [External] + streamExts (Stream _ _ expr _) = exprExts expr + + triggerExts :: Trigger -> [External] + triggerExts (Trigger _ guard args) = guardExts `extUnion` argExts + where + guardExts = exprExts guard + argExts = concatMap uExprExts args + + uExprExts :: UExpr -> [External] + uExprExts (UExpr _ expr) = exprExts expr + + exprExts :: Expr a -> [External] + exprExts (Local _ _ _ e1 e2) = exprExts e1 `extUnion` exprExts e2 + exprExts (ExternVar ty name _) = [External name ty] + exprExts (Op1 _ e) = exprExts e + exprExts (Op2 _ e1 e2) = exprExts e1 `extUnion` exprExts e2 + exprExts (Op3 _ e1 e2 e3) = exprExts e1 `extUnion` exprExts e2 + `extUnion` exprExts e3 + exprExts (Label _ _ e) = exprExts e + exprExts _ = [] + + -- | Union over lists of External, we solely base the equality on the + -- extName's. + extUnion :: [External] -> [External] -> [External] + extUnion = unionBy (\a b -> extName a == extName b) diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/FloatingPoint.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/FloatingPoint.hs new file mode 100644 index 00000000..a1683f1c --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/FloatingPoint.hs @@ -0,0 +1,171 @@ +-- | Generate definitions that allow importing C implementations of +-- floating-point operations into Bluespec. +module Copilot.Compile.Bluespec.FloatingPoint + ( copilotBluespecFloatingPointBSV + , copilotBluespecFloatingPointC + ) where + +-- | The contents of the generated @BluespecFP.bsv@ file, which contains the +-- @import \"BDPI\"@ declarations needed to use imported C functions in +-- Bluespec. +copilotBluespecFloatingPointBSV :: String +copilotBluespecFloatingPointBSV = + unlines $ + [ "import FloatingPoint::*;" + , "" + ] ++ + concatMap + (\funName -> [importOp1 Float funName, importOp1 Double funName]) + unaryFloatOpNames ++ + concatMap + (\funName -> [importOp2 Float funName, importOp2 Double funName]) + [ "pow" + , "atan2" + , "logb" + ] + where + importOp1 :: FloatType -> String -> String + importOp1 ft funName = + "import \"BDPI\" function " ++ floatTypeName ft ++ " " ++ funNamePrefix + ++ funName ++ floatTypeSuffix ft ++ " (" ++ floatTypeName ft ++ " x);" + + importOp2 :: FloatType -> String -> String + importOp2 ft funName = + "import \"BDPI\" function " ++ floatTypeName ft ++ " " ++ funNamePrefix + ++ funName ++ floatTypeSuffix ft ++ " (" ++ floatTypeName ft ++ " x, " + ++ floatTypeName ft ++ " y);" + + floatTypeName :: FloatType -> String + floatTypeName Float = "Float" + floatTypeName Double = "Double" + +-- | The contents of the generated @bs_fp.c@ file, which contains the C wrapper +-- functions that Bluespec imports. +copilotBluespecFloatingPointC :: String +copilotBluespecFloatingPointC = + unlines $ + [ "#include " + , "" + , defineUnionType Float + , defineUnionType Double + ] ++ + concatMap + (\funName -> [defineOp1 Float funName, defineOp1 Double funName]) + unaryFloatOpNames ++ + concatMap + (\funName -> [defineOp2 Float funName, defineOp2 Double funName]) + [ "pow" + , "atan2" + ] ++ + -- There is no direct C counterpart to the `logb` function, so we implement + -- it in terms of `log`. + map + (\ft -> + defineOp2Skeleton ft "logb" $ + \_cFunName x y -> "log" ++ floatTypeSuffix ft ++ "(" ++ y ++ ") / log" + ++ floatTypeSuffix ft ++ "( " ++ x ++ ")") + [Float, Double] + where + defineUnionType :: FloatType -> String + defineUnionType ft = + unlines + [ "union " ++ unionTypeName ft ++ " {" + , " " ++ integerTypeName ft ++ " i;" + , " " ++ floatTypeName ft ++ " f;" + , "};" + ] + + defineOp1Skeleton :: + FloatType -> String -> (String -> String -> String) -> String + defineOp1Skeleton ft funName mkFloatOp = + let cFunName = funName ++ floatTypeSuffix ft in + unlines + [ integerTypeName ft ++ " " + ++ funNamePrefix ++ cFunName + ++ "(" ++ integerTypeName ft ++ " x) {" + , " union " ++ unionTypeName ft ++ " x_u;" + , " union " ++ unionTypeName ft ++ " r_u;" + , " x_u.i = x;" + , " r_u.f = " ++ mkFloatOp cFunName "x_u.f" ++ ";" + , " return r_u.i;" + , "}" + ] + + defineOp1 :: FloatType -> String -> String + defineOp1 ft funName = + defineOp1Skeleton ft funName $ + \cFunName x -> cFunName ++ "(" ++ x ++ ")" + + defineOp2Skeleton :: + FloatType -> String -> (String -> String -> String -> String) -> String + defineOp2Skeleton ft funName mkFloatOp = + let cFunName = funName ++ floatTypeSuffix ft in + unlines + [ integerTypeName ft ++ " " + ++ funNamePrefix ++ cFunName + ++ "(" ++ integerTypeName ft ++ " x, " ++ integerTypeName ft + ++ " y) {" + , " union " ++ unionTypeName ft ++ " x_u;" + , " union " ++ unionTypeName ft ++ " y_u;" + , " union " ++ unionTypeName ft ++ " r_u;" + , " x_u.i = x;" + , " y_u.i = y;" + , " r_u.f = " ++ mkFloatOp cFunName "x_u.f" "y_u.f" ++ ";" + , " return r_u.i;" + , "}" + ] + + defineOp2 :: FloatType -> String -> String + defineOp2 ft funName = + defineOp2Skeleton ft funName $ + \cFunName x y -> cFunName ++ "(" ++ x ++ ", " ++ y ++ ")" + + integerTypeName :: FloatType -> String + integerTypeName Float = "unsigned int" + integerTypeName Double = "unsigned long long" + + floatTypeName :: FloatType -> String + floatTypeName Float = "float" + floatTypeName Double = "double" + + unionTypeName :: FloatType -> String + unionTypeName Float = "ui_float" + unionTypeName Double = "ull_double" + +-- * Internals + +-- | Are we generating a function for a @float@ or @double@ operation? +data FloatType + = Float + | Double + +-- | The suffix to use in the generated function. +floatTypeSuffix :: FloatType -> String +floatTypeSuffix Float = "f" +floatTypeSuffix Double = "" + +-- | The prefix to use in the generated function. +funNamePrefix :: String +funNamePrefix = "bs_fp_" + +-- | The names of unary floating-point operations. +unaryFloatOpNames :: [String] +unaryFloatOpNames = + [ "exp" + , "log" + , "acos" + , "asin" + , "atan" + , "cos" + , "sin" + , "tan" + , "acosh" + , "asinh" + , "atanh" + , "cosh" + , "sinh" + , "tanh" + , "ceil" + , "floor" + , "sqrt" + ] diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs new file mode 100644 index 00000000..dbc714a3 --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Name.hs @@ -0,0 +1,95 @@ +-- | Naming of variables and functions in Bluespec. +module Copilot.Compile.Bluespec.Name + ( argNames + , generatorName + , guardName + , ifcArgName + , indexName + , lowercaseName + , specIfcName + , specIfcPkgName + , specTypesPkgName + , streamAccessorName + , streamElemName + , streamName + , uppercaseName + ) where + +-- External imports +import Data.Char (isLower, isUpper) + +-- External imports: Copilot +import Copilot.Core (Id) + +-- | Turn a specification name into the name of its module interface. +specIfcName :: String -> String +specIfcName prefix = uppercaseName (specIfcPkgName prefix) + +-- | Turn a specification name into the name of the package that declares its +-- module interface. Note that 'specIfcPkgName' is not necessarily the same name +-- as 'specIfcName', as the former does not need to begin with an uppercase +-- letter, but the latter does. +specIfcPkgName :: String -> String +specIfcPkgName prefix = prefix ++ "Ifc" + +-- | Turn a specification name into the name of the package that declares its +-- struct types. +specTypesPkgName :: String -> String +specTypesPkgName prefix = prefix ++ "Types" + +-- | Turn a stream id into a stream element name. +streamElemName :: Id -> Int -> String +streamElemName sId n = streamName sId ++ "_" ++ show n + +-- | The name of the variable of type @Ifc@. This is used to select +-- trigger functions and external variables. +ifcArgName :: String +ifcArgName = "ifc" + +-- | Create a Bluespec name that must start with an uppercase letter (e.g., a +-- struct or interface name). If the supplied name already begins with an +-- uppercase letter, this function returns the name unchanged. Otherwise, this +-- function prepends a @BS_@ prefix (short for \"Bluespec\") at the front. +uppercaseName :: String -> String +uppercaseName [] = [] +uppercaseName n@(c:_) + | isUpper c = n + | otherwise = "BS_" ++ n + +-- | Create a Bluespec name that must start with a lowercase letter (e.g., a +-- function or method name). If the supplied name already begins with a +-- lowercase letter, this function returns the name unchanged. Otherwise, this +-- function prepends a @bs_@ prefix (short for \"Bluespec\") at the front. +lowercaseName :: String -> String +lowercaseName [] = [] +lowercaseName n@(c:_) + | isLower c = n + | otherwise = "bs_" ++ n + +-- | Turn a stream id into a suitable Bluespec variable name. +streamName :: Id -> String +streamName sId = "s" ++ show sId + +-- | Turn a stream id into the global varname for indices. +indexName :: Id -> String +indexName sId = streamName sId ++ "_idx" + +-- | Turn a stream id into the name of its accessor function +streamAccessorName :: Id -> String +streamAccessorName sId = streamName sId ++ "_get" + +-- | Turn stream id into name of its generator function. +generatorName :: Id -> String +generatorName sId = streamName sId ++ "_gen" + +-- | Turn the name of a trigger into a guard generator. +guardName :: String -> String +guardName name = lowercaseName name ++ "_guard" + +-- | Turn a trigger name into a an trigger argument name. +argName :: String -> Int -> String +argName name n = lowercaseName name ++ "_arg" ++ show n + +-- | Enumerate all argument names based on trigger name. +argNames :: String -> [String] +argNames base = map (argName base) [0..] diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Representation.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Representation.hs new file mode 100644 index 00000000..d5bc4421 --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Representation.hs @@ -0,0 +1,22 @@ +-- | Bluespec backend specific versions of selected `Copilot.Core` datatypes. +module Copilot.Compile.Bluespec.Representation + ( UniqueTrigger (..) + , UniqueTriggerId + , mkUniqueTriggers + ) + where + +import Copilot.Core ( Trigger (..) ) + +-- | Internal unique name for a trigger. +type UniqueTriggerId = String + +-- | A `Copilot.Core.Trigger` with an unique name. +data UniqueTrigger = UniqueTrigger UniqueTriggerId Trigger + +-- | Given a list of triggers, make their names unique. +mkUniqueTriggers :: [Trigger] -> [UniqueTrigger] +mkUniqueTriggers ts = zipWith mkUnique ts [0..] + where + mkUnique :: Trigger -> Integer -> UniqueTrigger + mkUnique t@(Trigger name _ _) n = UniqueTrigger (name ++ "_" ++ show n) t diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Settings.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Settings.hs new file mode 100644 index 00000000..47247b60 --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Settings.hs @@ -0,0 +1,14 @@ +-- | Settings used by the code generator to customize the code. +module Copilot.Compile.Bluespec.Settings + ( BluespecSettings(..) + , mkDefaultBluespecSettings + ) where + +-- | Settings used to customize the code generated. +newtype BluespecSettings = BluespecSettings + { bluespecSettingsOutputDirectory :: FilePath + } + +-- | Default Bluespec settings. Output to the current directory. +mkDefaultBluespecSettings :: BluespecSettings +mkDefaultBluespecSettings = BluespecSettings "." diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Type.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Type.hs new file mode 100644 index 00000000..967b695b --- /dev/null +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Type.hs @@ -0,0 +1,95 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | Translate Copilot Core expressions and operators to Bluespec. +module Copilot.Compile.Bluespec.Type + ( transType + , tVector + ) where + +-- External imports +import Data.String (IsString (..)) +import qualified Language.Bluespec.Classic.AST as BS +import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS +import qualified Language.Bluespec.Classic.AST.Builtin.Types as BS + +-- Internal imports: Copilot +import Copilot.Core + +-- Internal imports +import Copilot.Compile.Bluespec.Name + +-- | Translate a Copilot type to a Bluespec type. +transType :: Type a -> BS.CType +transType ty = case ty of + Bool -> BS.tBool + Int8 -> BS.tInt `BS.TAp` BS.cTNum 8 BS.NoPos + Int16 -> BS.tInt `BS.TAp` BS.cTNum 16 BS.NoPos + Int32 -> BS.tInt `BS.TAp` BS.cTNum 32 BS.NoPos + Int64 -> BS.tInt `BS.TAp` BS.cTNum 64 BS.NoPos + Word8 -> BS.tUInt `BS.TAp` BS.cTNum 8 BS.NoPos + Word16 -> BS.tUInt `BS.TAp` BS.cTNum 16 BS.NoPos + Word32 -> BS.tUInt `BS.TAp` BS.cTNum 32 BS.NoPos + Word64 -> BS.tUInt `BS.TAp` BS.cTNum 64 BS.NoPos + + Float -> BS.TCon $ + BS.TyCon + { BS.tcon_name = BS.mkId BS.NoPos "Float" + , BS.tcon_kind = Just BS.KStar + , BS.tcon_sort = BS.TItype 0 $ tFloatingPoint `BS.TAp` + BS.cTNum 8 BS.NoPos `BS.TAp` + BS.cTNum 23 BS.NoPos + } + Double -> BS.TCon $ + BS.TyCon + { BS.tcon_name = BS.mkId BS.NoPos "Double" + , BS.tcon_kind = Just BS.KStar + , BS.tcon_sort = BS.TItype 0 $ tFloatingPoint `BS.TAp` + BS.cTNum 11 BS.NoPos `BS.TAp` + BS.cTNum 52 BS.NoPos + } + Array ty' -> tVector `BS.TAp` BS.cTNum len BS.NoPos `BS.TAp` transType ty' + where + len = toInteger $ typeLength ty + Struct s -> BS.TCon $ + BS.TyCon + { BS.tcon_name = BS.mkId BS.NoPos $ + fromString $ + uppercaseName $ + typeName s + , BS.tcon_kind = Just BS.KStar + , BS.tcon_sort = + BS.TIstruct BS.SStruct $ + map (\(Value _tu field) -> + BS.mkId BS.NoPos $ + fromString $ + lowercaseName $ + fieldName field) + (toValues s) + } + +-- | The @Vector@ Bluespec data type. +tVector :: BS.CType +tVector = BS.TCon $ + BS.TyCon + { BS.tcon_name = BS.idVector + , BS.tcon_kind = Just (BS.Kfun BS.KNum (BS.Kfun BS.KStar BS.KStar)) + , BS.tcon_sort = + BS.TIdata + { BS.tidata_cons = [BS.mkId BS.NoPos "V"] + , BS.tidata_enum = False + } + } + +-- | The @FloatingPoint@ Bluespec struct type. +tFloatingPoint :: BS.CType +tFloatingPoint = BS.TCon $ + BS.TyCon + { BS.tcon_name = BS.mkId BS.NoPos "FloatingPoint" + , BS.tcon_kind = Just (BS.Kfun BS.KNum (BS.Kfun BS.KNum BS.KStar)) + , BS.tcon_sort = + BS.TIstruct BS.SStruct [ BS.mkId BS.NoPos "sign" + , BS.mkId BS.NoPos "exp" + , BS.mkId BS.NoPos "sfd" + ] + } diff --git a/copilot-bluespec/tests/Main.hs b/copilot-bluespec/tests/Main.hs new file mode 100644 index 00000000..928da7de --- /dev/null +++ b/copilot-bluespec/tests/Main.hs @@ -0,0 +1,18 @@ +-- | Test copilot-bluespec. +module Main where + +-- External imports +import Test.Framework (Test, defaultMain) + +-- Internal library modules being tested +import qualified Test.Copilot.Compile.Bluespec + +-- | Run all @copilot-bluespec@ tests. +main :: IO () +main = defaultMain tests + +-- | All @copilot-bluespec@ tests. +tests :: [Test.Framework.Test] +tests = + [ Test.Copilot.Compile.Bluespec.tests + ] diff --git a/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec.hs b/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec.hs new file mode 100644 index 00000000..ee99c6e7 --- /dev/null +++ b/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec.hs @@ -0,0 +1,1470 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -Wno-orphans #-} +-- | Test copilot-bluespec:Copilot.Compile.Bluespec. +module Test.Copilot.Compile.Bluespec + ( tests ) + where + +-- External imports +import Control.Arrow ((&&&)) +import Control.Exception (IOException, catch) +import Control.Monad (when) +import Data.AEq (AEq (..)) +import Data.Bits (Bits, complement) +import Data.Foldable (foldl') +import Data.List (intercalate, stripPrefix) +import Data.List.Extra (stripSuffix) +import Data.Type.Equality (testEquality) +import Data.Typeable (Proxy (..), (:~:) (Refl)) +import GHC.Float (castDoubleToWord64, + castFloatToWord32, + castWord32ToFloat, + castWord64ToDouble) +import GHC.TypeLits (KnownNat, natVal) +import Numeric.IEEE (infinity, nan) +import System.Directory (doesFileExist, + getTemporaryDirectory, + removeDirectoryRecursive, + setCurrentDirectory) +import System.IO (hPutStrLn, stderr) +import System.Posix.Temp (mkdtemp) +import System.Process (callProcess, readProcess) +import System.Random (Random) +import Test.Framework (Test, testGroup) +import Test.Framework.Providers.QuickCheck2 (testProperty) +import Test.QuickCheck (Arbitrary, Gen, Property, + arbitrary, choose, elements, + forAll, forAllBlind, frequency, + getPositive, ioProperty, once, + oneof, vectorOf, withMaxSuccess, + (.&&.)) +import Test.QuickCheck.Gen (chooseAny, chooseBoundedIntegral) +import Text.ParserCombinators.ReadPrec (minPrec) + +-- External imports: Copilot +import Copilot.Core hiding (Property) + +-- External imports +import Copilot.Compile.Bluespec (bluespecSettingsOutputDirectory, compile, + compileWith, mkDefaultBluespecSettings) + +-- Internal imports +import Test.Copilot.Compile.Bluespec.External (External (extName), gatherExts) + +-- * Constants + +-- | All tests for copilot-bluespec:Copilot.Compile.Bluespec. +tests :: Test.Framework.Test +tests = + testGroup "Copilot.Compile.Bluespec" + [ testGroup "Unit tests" + [ testProperty "Compile specification" testCompile + , testProperty "Compile specification in custom dir" testCompileCustomDir + , testProperty "Run specification" testRun + , testProperty "Run and compare results" testRunCompare + ] + , testGroup "Regression tests" + [ test14 + , test15 + ] + ] + +-- * Individual tests + +-- | Test compiling a spec. +testCompile :: Property +testCompile = once $ ioProperty $ do + tmpDir <- getTemporaryDirectory + setCurrentDirectory tmpDir + + testDir <- mkdtemp "CopilotTest" + setCurrentDirectory testDir + + compile "CopilotTest" spec + r <- compileBluespec "CopilotTest" [] + + setCurrentDirectory tmpDir + removeDirectoryRecursive testDir + + return r + + where + + spec = Spec streams observers triggers properties + + streams = [] + observers = [] + triggers = [ Trigger function guard args ] + properties = [] + + function = "func" + + guard = Const Bool True + + args = [] + +-- | Test compiling a spec in a custom directory. +testCompileCustomDir :: Property +testCompileCustomDir = once $ ioProperty $ do + tmpDir <- getTemporaryDirectory + setCurrentDirectory tmpDir + + testDir <- mkdtemp "CopilotTest" + + compileWith (mkDefaultBluespecSettings + { bluespecSettingsOutputDirectory = testDir }) + "CopilotTest" + spec + + setCurrentDirectory testDir + r <- compileBluespec "CopilotTest" [] + + setCurrentDirectory tmpDir + removeDirectoryRecursive testDir + + return r + + where + + spec = Spec streams observers triggers properties + + streams = [] + observers = [] + triggers = [ Trigger function guard args ] + properties = [] + + function = "nop" + + guard = Const Bool True + + args = [] + +-- | Test compiling a spec and running the resulting program. +-- +-- The actual behavior is ignored. +testRun :: Property +testRun = once $ ioProperty $ do + tmpDir <- getTemporaryDirectory + setCurrentDirectory tmpDir + + testDir <- mkdtemp "CopilotTest" + setCurrentDirectory testDir + + let bluespecProgram = unlines + [ "package Top where" + , "" + , "import CopilotTest" + , "import CopilotTestIfc" + , "import CopilotTestTypes" + , "" + , "copilotTestIfc :: Module CopilotTestIfc" + , "copilotTestIfc =" + , " module" + , " interface" + , " nop :: Action" + , " nop = return ()" + , "" + , "mkTop :: Module Empty" + , "mkTop = mkCopilotTest copilotTestIfc" + ] + + writeFile "Top.bs" bluespecProgram + + compile "CopilotTest" spec + r <- compileBluespec "Top" ["-g", "mkTop"] + + -- Compile a main program + r2 <- compileExecutable "mkTop" + callProcess "./mkTop" ["-m", "2"] + + setCurrentDirectory tmpDir + removeDirectoryRecursive testDir + + return $ r && r2 + + where + + spec = Spec streams observers triggers properties + + streams = [] + observers = [] + triggers = [ Trigger function guard args ] + properties = [] + + function = "nop" + + guard = Const Bool True + + args = [] + +-- | Test running compiled spec and comparing the results to the +-- expectation. +testRunCompare :: Property +testRunCompare = + -- It takes a pretty long time to run these tests, so we set the maximum + -- number of successful tests to 5 instead of the default (100) for the sake + -- of making the test suite complete in a more reasonable amount of time. + withMaxSuccess 5 $ + testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int8 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int16 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int32 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int64 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word8 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word16 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word32 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word64 Bool)) + .&&. testRunCompare1 (arbitraryOpFloatingBool :: Gen (TestCase1 Float Bool)) + .&&. testRunCompare1 (arbitraryOpFloatingBool :: Gen (TestCase1 Double Bool)) + .&&. testRunCompare1 (arbitraryOpStruct :: Gen (TestCase1 MyStruct Int8)) + .&&. testRunCompare2 (arbitraryOp2Struct :: Gen (TestCase2 MyStruct Int8 MyStruct)) + .&&. testRunCompare2 (arbitraryArray2Num :: Gen (TestCase2 (Array 2 Int8) Word32 Int8)) + .&&. testRunCompare2 (arbitraryArray2Num :: Gen (TestCase2 (Array 2 Int16) Word32 Int16)) + .&&. testRunCompare3 (arbitraryArray3Num :: Gen (TestCase3 (Array 2 Int16) Word32 Int16 (Array 2 Int16))) + +-- * Regression tests + +-- | Regression tests for +-- https://github.com/Copilot-Language/copilot-bluespec/issues/14 which ensure +-- that @copilot-bluespec@ generates code for the @signum@ function that adheres +-- to Copilot's @signum@ semantics. +test14 :: Test.Framework.Test +test14 = + testGroup "#14" + [ testProperty "`signum @Int8` generates correct Bluespec code" $ + mkRegressionTest1 (Sign Int8) (fmap signum) + [-2, -1, 0, 1, 2] + , testProperty "`signum @Double` generates correct Bluespec code" $ + mkRegressionTest1 (Sign Double) (fmap signum) + [-nan, -infinity, -2, -1, -0.0, 0, 1, 2, infinity, nan] + ] + +-- | Regression tests for +-- https://github.com/Copilot-Language/copilot-bluespec/issues/15 which ensure +-- that @copilot-bluespec@ generates valid code for comparison operators (('<'), +-- ('<='), ('>'), and ('>=')) that are capable of handling NaN values. +test15 :: Test.Framework.Test +test15 = + testGroup "#15" + [ testProperty "Generates valid (<) code for NaNs" $ + mkRegressionTest2 (Lt Double) (zipWith (<)) vals + , testProperty "Generates valid (<=) code for NaNs" $ + mkRegressionTest2 (Le Double) (zipWith (<=)) vals + , testProperty "Generates valid (>) code for NaNs" $ + mkRegressionTest2 (Gt Double) (zipWith (>)) vals + , testProperty "Generates valid (>=) code for NaNs" $ + mkRegressionTest2 (Ge Double) (zipWith (>=)) vals + ] + where + vals :: [(Double, Double)] + vals = [(0, nan), (nan, 0)] + +-- | Test the behavior of a unary operation (an @'Op1' a b@ value) against its +-- expected behavior (as a Haskell function of type @[a] -> [b]@) using the +-- supplied inputs (of type @[a]@). This function is intended to be used to +-- construct regression tests. +mkRegressionTest1 :: (Typed a, Typed b, + DisplayableInBluespec b, ReadableFromBluespec b, AEq b) + => Op1 a b + -> ([a] -> [b]) + -> [a] + -> Property +mkRegressionTest1 op haskellFun vals = + let spec = alwaysTriggerArg1 (UExpr t2 appliedOp) + appliedOp = Op1 op (ExternVar t1 varName Nothing) + + len = length vals + inputs = filterOutUnusedExts + spec + [ (typeBluespec t1, + fmap (bluespecShow t1) vals, + varName) + ] + outputs = haskellFun vals in + + once $ + testRunCompareArg + inputs len outputs spec (typeBluespec t2) + + where + + t1 = typeOf + t2 = typeOf + + varName = "input" + +-- | Test the behavior of a binary operation (an @'Op2' a b c@ value) against +-- its expected behavior (as a Haskell function of type @[a] -> [b] -> [c]@) +-- using the supplied inputs (of type @[(a, b)]@). This function is intended to +-- be used to construct regression tests. +mkRegressionTest2 :: (Typed a, Typed b, Typed c, + DisplayableInBluespec c, ReadableFromBluespec c, AEq c) + => Op2 a b c + -> ([a] -> [b] -> [c]) + -> [(a, b)] + -> Property +mkRegressionTest2 op haskellFun vals = + let spec = alwaysTriggerArg1 (UExpr t3 appliedOp) + appliedOp = Op2 op (ExternVar t1 varName1 Nothing) + (ExternVar t2 varName2 Nothing) + + len = length vals + (vals1, vals2) = unzip vals + inputs = filterOutUnusedExts + spec + [ (typeBluespec t1, + fmap (bluespecShow t1) vals1, + varName1) + , (typeBluespec t2, + fmap (bluespecShow t2) vals2, + varName2) + ] + outputs = haskellFun vals1 vals2 in + + once $ + testRunCompareArg + inputs len outputs spec (typeBluespec t3) + + where + + t1 = typeOf + t2 = typeOf + t3 = typeOf + + varName1 = "input1" + varName2 = "input2" + +-- * Random generators + +-- ** Random function generators + +-- | Generator of functions that produce booleans. +arbitraryOpBool :: Typed a => Gen (Fun a Bool, [a] -> [Bool]) +arbitraryOpBool = + frequency + [ (5, arbitraryOp1Any) + , (5, funCompose1 <$> arbitraryOp1Bool <*> arbitraryOpBool) + , (2, funCompose2 <$> arbitraryOp2Bool <*> arbitraryOpBool <*> arbitraryOpBool) + , (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpBool <*> arbitraryOpBool) + ] + +-- | Generator of functions that take Bits and produce booleans. +arbitraryOpBoolBits :: (Typed a, Bits a) => Gen (Fun a Bool, [a] -> [Bool]) +arbitraryOpBoolBits = + frequency + [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpBits <*> arbitraryOpBits) + ] + +-- | Generator of functions that take Nums and produce booleans. +arbitaryOpBoolOrdEqNum :: (Typed a, Eq a, Ord a, Num a) + => Gen (Fun a Bool, [a] -> [Bool]) +arbitaryOpBoolOrdEqNum = + frequency + [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpNum <*> arbitraryOpNum) + , (1, funCompose2 <$> arbitraryOp2Ord <*> arbitraryOpNum <*> arbitraryOpNum) + ] + +-- | Generator of functions that take Floating point numbers and produce +-- booleans. +arbitraryOpBoolEqNumFloat :: (Typed t, Eq t, Num t, Floating t) + => Gen (Fun t Bool, [t] -> [Bool]) +arbitraryOpBoolEqNumFloat = + frequency + [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpNum <*> arbitraryOpFloat) + , (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpFloat <*> arbitraryOpNum) + ] + +-- | Generator of functions that take and produce Bits. +arbitraryOpBits :: (Bits t, Typed t) + => Gen (Fun t t, [t] -> [t]) +arbitraryOpBits = elements + [ (Op1 (BwNot typeOf), fmap complement) + ] + +-- | Generator of functions that take and produce Nums. +arbitraryOpNum :: (Typed t, Num t) => Gen (Fun t t, [t] -> [t]) +arbitraryOpNum = elements + [ (Op1 (Abs typeOf), fmap abs) + , (Op1 (Sign typeOf), fmap signum) + ] + +-- | Generator of functions that take an arrays and indicates and produce +-- elements from the array. +arbitraryArrayIx :: forall t n . (Typed t, KnownNat n, Num t) + => Gen ( Fun2 (Array n t) Word32 t + , [Array n t] -> [Word32] -> [t] + ) +arbitraryArrayIx = return + (Op2 (Index typeOf), zipWith (\x y -> arrayElems x !! fromIntegral y)) + +-- | Generator of functions that take arrays, indices, and values, and then +-- produce new arrays by updating the elements at the indices with the values. +arbitraryArrayUpdate :: forall t n . (Typed t, KnownNat n, Num t) + => Gen ( Fun3 (Array n t) Word32 t (Array n t) + , [Array n t] -> [Word32] -> [t] -> [Array n t] + ) +arbitraryArrayUpdate = return + (Op3 (UpdateArray typeOf), zipWith3 (\x y z -> array (updateAt y z (arrayElems x)))) + where + updateAt :: forall a. Word32 -> a -> [a] -> [a] + updateAt _ _ [] = [] + updateAt 0 x (_ : as) = x : as + updateAt n x (a : as) = a : updateAt (n-1) x as + +-- | Generator of functions that take structs produce fields of the struct. +arbitraryStructField :: Gen ( Fun MyStruct Int8 + , [MyStruct] -> [Int8] + ) +arbitraryStructField = elements + [ (Op1 (GetField typeOf typeOf myStruct1), fmap (unField . myStruct1)) + , (Op1 (GetField typeOf typeOf myStruct2), fmap (unField . myStruct2)) + ] + +-- | Generator of functions that take and produce structs, where the returned +-- structs have one field value updated. +arbitraryStructUpdate :: Gen ( Fun2 MyStruct Int8 MyStruct + , [MyStruct] -> [Int8] -> [MyStruct] + ) +arbitraryStructUpdate = elements + [ ( Op2 (UpdateField typeOf typeOf myStruct1) + , zipWith (\s i -> s { myStruct1 = Field i }) + ) + , ( Op2 (UpdateField typeOf typeOf myStruct2) + , zipWith (\s i -> s { myStruct2 = Field i }) + ) + ] + +-- | Generator of functions on Floating point numbers. +arbitraryOpFloat :: (Floating t, Typed t) => Gen (Fun t t, [t] -> [t]) +arbitraryOpFloat = elements + [ (Op1 (Recip typeOf), fmap recip) + , (Op1 (Exp typeOf), fmap exp) + , (Op1 (Sqrt typeOf), fmap sqrt) + , (Op1 (Log typeOf), fmap log) + , (Op1 (Sin typeOf), fmap sin) + , (Op1 (Tan typeOf), fmap tan) + , (Op1 (Cos typeOf), fmap cos) + , (Op1 (Asin typeOf), fmap asin) + , (Op1 (Atan typeOf), fmap atan) + , (Op1 (Acos typeOf), fmap acos) + , (Op1 (Sinh typeOf), fmap sinh) + , (Op1 (Tanh typeOf), fmap tanh) + , (Op1 (Cosh typeOf), fmap cosh) + , (Op1 (Asinh typeOf), fmap asinh) + , (Op1 (Atanh typeOf), fmap atanh) + , (Op1 (Acosh typeOf), fmap acosh) + ] + +-- | Generator of functions on that produce elements of any type. +arbitraryOp1Any :: forall a b + . (Arbitrary b, Typed a, Typed b) + => Gen (Fun a b, [a] -> [b]) +arbitraryOp1Any = oneof $ + [ (\v -> (\_ -> Const typeOf v, fmap (const v))) <$> arbitrary ] + ++ + rest + where + rest | Just Refl <- testEquality t1 t2 + = [return (id, id)] + | otherwise + = [] + + t1 :: Type a + t1 = typeOf + + t2 :: Type b + t2 = typeOf + +-- | Generator of functions on Booleans. +arbitraryOp1Bool :: Gen (Fun Bool Bool, [Bool] -> [Bool]) +arbitraryOp1Bool = elements + [ (Op1 Not, fmap not) + ] + +-- | Generator of binary functions on Booleans. +arbitraryOp2Bool :: Gen (Fun2 Bool Bool Bool, [Bool] -> [Bool] -> [Bool]) +arbitraryOp2Bool = elements + [ (Op2 And, zipWith (&&)) + , (Op2 Or, zipWith (||)) + ] + +-- | Generator of binary functions that take two Eq elements of the same type +-- and return a Bool. +arbitraryOp2Eq :: (Typed t, Eq t) + => Gen (Fun2 t t Bool, [t] -> [t] -> [Bool]) +arbitraryOp2Eq = elements + [ (Op2 (Eq typeOf), zipWith (==)) + , (Op2 (Ne typeOf), zipWith (/=)) + ] + +-- | Generator of binary functions that take two Ord elements of the same type +-- and return a Bool. +arbitraryOp2Ord :: (Typed t, Ord t) + => Gen (Fun2 t t Bool, [t] -> [t] -> [Bool]) +arbitraryOp2Ord = elements + [ (Op2 (Le typeOf), zipWith (<=)) + , (Op2 (Lt typeOf), zipWith (<)) + , (Op2 (Ge typeOf), zipWith (>=)) + , (Op2 (Gt typeOf), zipWith (>)) + ] + +-- ** Random data generators + +-- | Random array generator. +arbitraryArray :: forall n t . (KnownNat n, Random t) => Gen (Array n t) +arbitraryArray = array <$> vectorOf len chooseAny + where + len :: Int + len = fromIntegral $ natVal (Proxy :: Proxy n) + +-- | Random struct generator. +arbitraryStruct :: Gen MyStruct +arbitraryStruct = do + fld1 <- Field <$> gen + fld2 <- Field <$> gen + return $ MyStruct fld1 fld2 + where + gen :: Gen Int8 + gen = chooseBoundedIntegral (minBound, maxBound) + +-- ** Random test case generators + +-- | Generator for test cases on integral numbers that produce booleans. +arbitraryOpIntegralBool :: (Typed t, Bounded t, Integral t, Bits t) + => Gen (TestCase1 t Bool) +arbitraryOpIntegralBool = frequency + [ (5, mkTestCase1 + arbitraryOpBool + (chooseBoundedIntegral (minBound, maxBound))) + + , (2, mkTestCase1 + arbitraryOpBoolBits + (chooseBoundedIntegral (minBound, maxBound))) + + -- we need to use +1 because certain operations overflow the number + , (2, mkTestCase1 + arbitaryOpBoolOrdEqNum + (chooseBoundedIntegral (minBound + 1, maxBound))) + ] + +-- | Generator for test cases on floating-point numbers that produce booleans. +arbitraryOpFloatingBool :: (Random t, Typed t, Floating t, Eq t) + => Gen (TestCase1 t Bool) +arbitraryOpFloatingBool = oneof + [ mkTestCase1 arbitraryOpBoolEqNumFloat chooseAny + ] + +-- | Generator for test cases on Arrays selection producing values of the +-- array. +arbitraryArray2Num :: forall n a + . (KnownNat n, Num a, Random a, Typed a) + => Gen (TestCase2 (Array n a) Word32 a) +arbitraryArray2Num = oneof + [ mkTestCase2 arbitraryArrayIx arbitraryArray gen + ] + where + gen :: Gen Word32 + gen = choose (0, len - 1) + + len :: Word32 + len = fromIntegral $ natVal (Proxy :: Proxy n) + +-- | Generator for test cases on Arrays which update values of the array. +arbitraryArray3Num :: forall n a + . (KnownNat n, Num a, Random a, Typed a) + => Gen (TestCase3 (Array n a) Word32 a (Array n a)) +arbitraryArray3Num = oneof + [ mkTestCase3 arbitraryArrayUpdate arbitraryArray gen chooseAny + ] + where + gen :: Gen Word32 + gen = choose (0, len - 1) + + len :: Word32 + len = fromIntegral $ natVal (Proxy :: Proxy n) + +-- | Generator for test cases on structs that produce fields of the struct. +arbitraryOpStruct :: Gen (TestCase1 MyStruct Int8) +arbitraryOpStruct = oneof + [ mkTestCase1 + arbitraryStructField + arbitraryStruct + ] + +-- | Generator for test cases that take and produce structs, where the returned +-- structs have one field value updated. +arbitraryOp2Struct :: Gen (TestCase2 MyStruct Int8 MyStruct) +arbitraryOp2Struct = oneof + [ mkTestCase2 + arbitraryStructUpdate + arbitraryStruct + gen + ] + where + gen :: Gen Int8 + gen = chooseBoundedIntegral (minBound, maxBound) + +-- * Semantics + +-- ** Functions + +-- | Unary Copilot function. +type Fun a b = Expr a -> Expr b + +-- | Binary Copilot function. +type Fun2 a b c = Expr a -> Expr b -> Expr c + +-- | Ternary Copilot function. +type Fun3 a b c d = Expr a -> Expr b -> Expr c -> Expr d + +-- | Compose functions, paired with the Haskell functions that define their +-- idealized meaning. +funCompose1 :: (Fun b c, [b] -> [c]) + -> (Fun a b, [a] -> [b]) + -> (Fun a c, [a] -> [c]) +funCompose1 (f1, g1) (f2, g2) = (f1 . f2, g1 . g2) + +-- | Compose a binary function, with two functions, one for each argument. +funCompose2 :: (Fun2 b c d, [b] -> [c] -> [d]) + -> (Fun a b, [a] -> [b]) + -> (Fun a c, [a] -> [c]) + -> (Fun a d, [a] -> [d]) +funCompose2 (f1, g1) (f2, g2) (f3, g3) = + (uncurry f1 . (f2 &&& f3), uncurry g1 . (g2 &&& g3)) + +-- ** Test cases + +-- | Test case specification for specs with one input variable and one output. +data TestCase1 a b = TestCase1 + { wrapTC1Expr :: Spec + -- ^ Specification containing a trigger with an extern of type 'a'. + + , wrapTC1Fun :: [a] -> [b] + -- ^ Function expected to function in the same way as the Spec being + -- tested. + + , wrapTC1CopInp :: (Type a, String, Gen a) + -- ^ Input specification. + -- + -- - The first element contains the type of the input in Bluespec. + -- + -- - The second contains the variable name in Bluespec. + -- + -- - The latter contains a randomized generator for values of the given + -- type. + + , wrapTC1CopOut :: Type b + -- ^ The type of the output in Bluespec. + } + +-- | Test case specification for specs with two input variables and one output. +data TestCase2 a b c = TestCase2 + { wrapTC2Expr :: Spec + -- ^ Specification containing a trigger with an extern of type 'a' and a + -- trigger with an argument of type 'b'. + + , wrapTC2Fun :: [a] -> [b] -> [c] + -- ^ Function expected to function in the same way as the Spec being + -- tested. + + , wrapTC2CopInp1 :: (Type a, String, Gen a) + -- ^ Input specification for the first input. + -- + -- - The first element contains the type of the input in Bluespec. + -- + -- - The second contains the variable name in Bluespec. + -- + -- - The latter contains a randomized generator for values of the given + -- type. + + , wrapTC2CopInp2 :: (Type b, String, Gen b) + -- ^ Input specification for the second input. + -- + -- - The first element contains the type of the input in Bluespec. + -- + -- - The second contains the variable name in Bluespec. + -- + -- - The latter contains a randomized generator for values of the given + -- type. + + , wrapTC2CopOut :: Type c + -- ^ The type of the output in Bluespec. + } + +-- | Test case specification for specs with three input variables and one output. +data TestCase3 a b c d = TestCase3 + { wrapTC3Expr :: Spec + -- ^ Specification containing a trigger with an extern of type 'a', a + -- trigger with an argument of type 'b', and a trigger with an argument of + -- type 'c'. + + , wrapTC3Fun :: [a] -> [b] -> [c] -> [d] + -- ^ Function expected to function in the same way as the Spec being + -- tested. + + , wrapTC3CopInp1 :: (Type a, String, Gen a) + -- ^ Input specification for the first input. + -- + -- - The first element contains the type of the input in Bluespec. + -- + -- - The second contains the variable name in Bluespec. + -- + -- - The latter contains a randomized generator for values of the given + -- type. + + , wrapTC3CopInp2 :: (Type b, String, Gen b) + -- ^ Input specification for the second input. + -- + -- - The first element contains the type of the input in Bluespec. + -- + -- - The second contains the variable name in Bluespec. + -- + -- - The latter contains a randomized generator for values of the given + -- type. + + , wrapTC3CopInp3 :: (Type c, String, Gen c) + -- ^ Input specification for the second input. + -- + -- - The first element contains the type of the input in Bluespec. + -- + -- - The second contains the variable name in Bluespec. + -- + -- - The latter contains a randomized generator for values of the given + -- type. + + , wrapTC3CopOut :: Type d + -- ^ The type of the output in Bluespec. + } + +-- | Generate test cases for expressions that behave like unary functions. +mkTestCase1 :: (Typed a, Typed b) + => Gen (Fun a b, [a] -> [b]) + -> Gen a + -> Gen (TestCase1 a b) +mkTestCase1 genO gen = do + (copilotF, semF) <- genO + + let spec = alwaysTriggerArg1 (UExpr t2 appliedOp) + appliedOp = copilotF (ExternVar t1 varName Nothing) + + return $ + TestCase1 + { wrapTC1Expr = spec + , wrapTC1Fun = semF + , wrapTC1CopInp = ( t1, varName, gen ) + , wrapTC1CopOut = t2 + } + + where + + t1 = typeOf + t2 = typeOf + + varName = "input" + +-- | Generate test cases for expressions that behave like binary functions. +mkTestCase2 :: (Typed a, Typed b, Typed c) + => Gen (Fun2 a b c, [a] -> [b] -> [c]) + -> Gen a + -> Gen b + -> Gen (TestCase2 a b c) +mkTestCase2 genO genA genB = do + (copilotF, semF) <- genO + + let spec = alwaysTriggerArg1 (UExpr t3 appliedOp) + appliedOp = copilotF (ExternVar t1 varName1 Nothing) + (ExternVar t2 varName2 Nothing) + + return $ + TestCase2 + { wrapTC2Expr = spec + , wrapTC2Fun = semF + , wrapTC2CopInp1 = ( t1, varName1, genA ) + , wrapTC2CopInp2 = ( t2, varName2, genB ) + , wrapTC2CopOut = t3 + } + + where + + t1 = typeOf + t2 = typeOf + t3 = typeOf + + varName1 = "input1" + varName2 = "input2" + +-- | Generate test cases for expressions that behave like ternary functions. +mkTestCase3 :: (Typed a, Typed b, Typed c, Typed d) + => Gen (Fun3 a b c d, [a] -> [b] -> [c] -> [d]) + -> Gen a + -> Gen b + -> Gen c + -> Gen (TestCase3 a b c d) +mkTestCase3 genO genA genB genC = do + (copilotF, semF) <- genO + + let spec = alwaysTriggerArg1 (UExpr t4 appliedOp) + appliedOp = copilotF (ExternVar t1 varName1 Nothing) + (ExternVar t2 varName2 Nothing) + (ExternVar t3 varName3 Nothing) + + return $ + TestCase3 + { wrapTC3Expr = spec + , wrapTC3Fun = semF + , wrapTC3CopInp1 = ( t1, varName1, genA ) + , wrapTC3CopInp2 = ( t2, varName2, genB ) + , wrapTC3CopInp3 = ( t3, varName3, genC ) + , wrapTC3CopOut = t4 + } + + where + + t1 = typeOf + t2 = typeOf + t3 = typeOf + t4 = typeOf + + varName1 = "input1" + varName2 = "input2" + varName3 = "input3" + +-- | Test running a compiled Bluespec program and comparing the results. +testRunCompare1 :: (Show a, Typed a, + DisplayableInBluespec b, ReadableFromBluespec b, + AEq b, Typed b) + => Gen (TestCase1 a b) -> Property +testRunCompare1 ops = + forAllBlind ops $ \testCase -> + let (TestCase1 + { wrapTC1Expr = copilotSpec + , wrapTC1Fun = haskellFun + , wrapTC1CopInp = inputVar + , wrapTC1CopOut = outputType + }) = testCase + (bluespecTypeInput, bluespecInputName, gen) = inputVar + + in forAll (getPositive <$> arbitrary) $ \len -> + + forAll (vectorOf len gen) $ \vals -> do + + let inputs = filterOutUnusedExts + copilotSpec + [ (typeBluespec bluespecTypeInput, + fmap (bluespecShow bluespecTypeInput) vals, + bluespecInputName) + ] + outputs = haskellFun vals + + testRunCompareArg + inputs len outputs copilotSpec (typeBluespec outputType) + +-- | Test running a compiled Bluespec program and comparing the results. +testRunCompare2 :: (Show a1, Typed a1, Show a2, Typed a2, + DisplayableInBluespec b, ReadableFromBluespec b, + AEq b, Typed b) + => Gen (TestCase2 a1 a2 b) -> Property +testRunCompare2 ops = + forAllBlind ops $ \testCase -> + let (TestCase2 + { wrapTC2Expr = copilotSpec + , wrapTC2Fun = haskellFun + , wrapTC2CopInp1 = inputVar1 + , wrapTC2CopInp2 = inputVar2 + , wrapTC2CopOut = outputType + }) = + testCase + + (bluespecTypeInput1, bluespecInputName1, gen1) = inputVar1 + (bluespecTypeInput2, bluespecInputName2, gen2) = inputVar2 + + in forAll (getPositive <$> arbitrary) $ \len -> + forAll (vectorOf len gen1) $ \vals1 -> + forAll (vectorOf len gen2) $ \vals2 -> do + let inputs = filterOutUnusedExts + copilotSpec + [ (typeBluespec bluespecTypeInput1, + fmap (bluespecShow bluespecTypeInput1) vals1, + bluespecInputName1) + , (typeBluespec bluespecTypeInput2, + fmap (bluespecShow bluespecTypeInput2) vals2, + bluespecInputName2) + ] + outputs = haskellFun vals1 vals2 + + testRunCompareArg + inputs len outputs copilotSpec (typeBluespec outputType) + +-- | Test running a compiled Bluespec program and comparing the results. +testRunCompare3 :: (Show a1, Typed a1, Show a2, Typed a2, Show a3, Typed a3, + DisplayableInBluespec b, ReadableFromBluespec b, + AEq b, Typed b) + => Gen (TestCase3 a1 a2 a3 b) -> Property +testRunCompare3 ops = + forAllBlind ops $ \testCase -> + let (TestCase3 + { wrapTC3Expr = copilotSpec + , wrapTC3Fun = haskellFun + , wrapTC3CopInp1 = inputVar1 + , wrapTC3CopInp2 = inputVar2 + , wrapTC3CopInp3 = inputVar3 + , wrapTC3CopOut = outputType + }) = + testCase + + (bluespecTypeInput1, bluespecInputName1, gen1) = inputVar1 + (bluespecTypeInput2, bluespecInputName2, gen2) = inputVar2 + (bluespecTypeInput3, bluespecInputName3, gen3) = inputVar3 + + in forAll (getPositive <$> arbitrary) $ \len -> + forAll (vectorOf len gen1) $ \vals1 -> + forAll (vectorOf len gen2) $ \vals2 -> + forAll (vectorOf len gen3) $ \vals3 -> do + let inputs = filterOutUnusedExts + copilotSpec + [ (typeBluespec bluespecTypeInput1, + fmap (bluespecShow bluespecTypeInput1) vals1, + bluespecInputName1) + , (typeBluespec bluespecTypeInput2, + fmap (bluespecShow bluespecTypeInput2) vals2, + bluespecInputName2) + , (typeBluespec bluespecTypeInput3, + fmap (bluespecShow bluespecTypeInput3) vals3, + bluespecInputName3) + ] + outputs = haskellFun vals1 vals2 vals3 + + testRunCompareArg + inputs len outputs copilotSpec (typeBluespec outputType) + +-- | Test running a compiled Bluespec program and comparing the results, when +-- the program produces one output as an argument to a trigger that always +-- fires. +-- +-- PRE: all lists (second argument) of inputs have the length given as second +-- argument. +-- +-- PRE: the monitoring code this is linked against uses the function +-- @printBack@ with exactly one argument to pass the results. +testRunCompareArg :: forall b + . (DisplayableInBluespec b, ReadableFromBluespec b, AEq b) + => [(String, [String], String)] + -> Int + -> [b] + -> Spec + -> String + -> Property +testRunCompareArg inputs numInputs vals spec outputType = + ioProperty $ do + tmpDir <- getTemporaryDirectory + setCurrentDirectory tmpDir + + -- Operate in temporary directory + testDir <- mkdtemp "CopilotTest" + setCurrentDirectory testDir + + -- Produce wrapper program + let bluespecProgram = + testRunCompareArgBluespecProgram (Proxy :: Proxy b) inputs outputType + writeFile "Top.bs" bluespecProgram + + -- Produce copilot monitoring code + compile "CopilotTest" spec + r <- compileBluespec "Top" ["-g", "mkTop"] + + -- Compile main program + r2 <- compileExecutable "mkTop" + + -- Print result so far (for debugging purposes only) + {- + print r2 + print testDir + -} + + -- Run the program and compare the results. Note that we use (===) (using + -- the `AEq` class from the `ieee754` package) rather than (==) (using the + -- `Eq` class), as the former allows us to use exact equality comparisons + -- for floating-point types. This lets us ensure that we are handling NaN + -- and -0.0 values correctly. + out <- readProcess "./mkTop" ["-m", show (numInputs + 2)] "" + let outNums = readFromBluespec <$> lines out + comparison = outNums === vals + + -- Only clean up if the test succeeded; otherwise, we want to inspect it. + when comparison $ do + -- Remove temporary directory + setCurrentDirectory tmpDir + removeDirectoryRecursive testDir + + return $ r && r2 && comparison + +-- | Return a wrapper Bluespec program that runs for a number of clock cycles, +-- updating external stream registers on every cycle, running the monitors, and +-- publishing the results of any outputs. +testRunCompareArgBluespecProgram + :: DisplayableInBluespec b + => Proxy b + -> [(String, [String], String)] + -> String + -> String +testRunCompareArgBluespecProgram proxy inputs outputType = unlines $ + [ "package Top where" + , "" + , "import FloatingPoint" + , "import Vector" + , "" + , "import CopilotTest" + , "import CopilotTestIfc" + , "import CopilotTestTypes" + , "" + ] + ++ inputVecDecls ++ + [ "" + , "copilotTestIfc :: Module CopilotTestIfc" + , "copilotTestIfc =" + , " module" + ] + ++ inputRegs ++ + [ " i :: Reg (Bit 64) <- mkReg 0" + , " ready :: Reg Bool <- mkReg False" + , " interface" + , " printBack :: " ++ outputType ++ " -> Action" + , " printBack output = $display " ++ printBackDisplayArgs + , " when ready" + , "" + ] + ++ inputMethods ++ + [ "" + , " rules" + , " \"inputs\": when True ==> do" + ] + ++ inputUpdates ++ + [ " i := i + 1" + , " ready := True" + , "" + , "mkTop :: Module Empty" + , "mkTop = mkCopilotTest copilotTestIfc" + ] + where + printBackDisplayArgs :: String + printBackDisplayArgs = unwords (displayInBluespec proxy "output") + + inputVecDecls :: [String] + inputVecDecls = + concatMap + (\(bluespecType, _varName, _regName, inputVecName, inputVals) -> + [ inputVecName ++ " :: Vector " ++ show (length inputVals) ++ + " (" ++ bluespecType ++ ")" + , inputVecName ++ " = " ++ genVector inputVals + ]) + vars + + inputRegs :: [String] + inputRegs = + map + (\(bluespecType, _varName, regName, _inputVecName, _inputVals) -> + " " ++ regName ++ " :: Reg (" ++ bluespecType ++ ") <- mkRegU") + vars + + inputMethods :: [String] + inputMethods = + concatMap + (\(bluespecType, varName, regName, _inputVecName, _inputVals) -> + [ " " ++ varName ++ " :: Reg (" ++ bluespecType ++ ")" + , " " ++ varName ++ " = " ++ regName + ]) + vars + + inputUpdates :: [String] + inputUpdates = + map + (\(_bluespecType, _varName, regName, inputVecName, _inputVals) -> + " " ++ regName ++ " := select " ++ inputVecName ++ " i") + vars + + vars = map oneInput inputs + oneInput (bluespecTypeInput, inputVals, bluespecInputName) = + (bluespecTypeInput, inputVarName, inputRegVarName, inputVecVarName, + inputVals) + where + inputVarName = bluespecInputName + inputRegVarName = bluespecInputName ++ "Impl" + inputVecVarName = bluespecInputName ++ "Inputs" + +-- * Auxiliary functions + +-- ** Specs handling + +-- | Build a 'Spec' that triggers at every step, passing the given expression +-- as argument, and execution a function 'printBack'. +alwaysTriggerArg1 :: UExpr -> Spec +alwaysTriggerArg1 = triggerArg1 (Const Bool True) + + where + + -- | Build a 'Spec' that triggers based on a given boolean stream, passing + -- the given expression as argument, and execution a function 'printBack'. + triggerArg1 :: Expr Bool -> UExpr -> Spec + triggerArg1 guard expr = Spec streams observers triggers properties + + where + + streams = [] + observers = [] + properties = [] + + triggers = [ Trigger function guard args ] + function = "printBack" + args = [ expr ] + +-- | Filter out any elements in the input list (of type @[(a, b, String)]@) +-- whose first element (the name of an external stream) does not correspond to +-- the name of an external stream in the supplied 'Spec'. For example, a Copilot +-- source program may declare external streams, but if none of them are used in +-- the 'Spec', then the 'Spec' value itself will not contain any external stream +-- definitions. As a result, we want to ensure that the input list also does not +-- contain any external streams. +filterOutUnusedExts :: Spec -> [(a, b, String)] -> [(a, b, String)] +filterOutUnusedExts spec = filter (\(_, _, name) -> name `elem` extNames) + where + extNames = map extName $ gatherExts (specStreams spec) (specTriggers spec) + +-- ** Compilation of Bluespec programs + +-- | Compile a Bluespec file given its basename. +compileBluespec :: String -> [String] -> IO Bool +compileBluespec baseName extraArgs = do + result <- catch (do callProcess "bsc" $ extraArgs ++ + [ "-sim", "-quiet", "-u", + -- We suppress the G0023 warning, + -- which arises due to the `nop` + -- triggers defined above. See the + -- DESIGN.md document for more + -- details on what these warning + -- codes mean. + "-suppress-warnings", "G0023:S0080", + baseName ++ ".bs" ] + return True + ) + (\e -> do + hPutStrLn stderr $ + "copilot-bluespec: error: compileBluespec: " + ++ "cannot compile " ++ baseName ++ ".bs with bsc" + hPutStrLn stderr $ + "copilot-bluespec: exception: " ++ show (e :: IOException) + return False + ) + if result + then doesFileExist $ baseName ++ ".bo" + else return False + +-- | Compile a Bluespec file into an executable given its basename. +compileExecutable :: String -> IO Bool +compileExecutable topExe = do + result <- catch (do callProcess "bsc" [ "-sim", "-quiet" + , "-e", topExe + , "-o", topExe + , "bs_fp.c" + ] + return True + ) + (\e -> do + hPutStrLn stderr $ + "copilot-bluespec: error: compileExecutable: " + ++ "cannot compile " ++ topExe ++ " with bsc" + hPutStrLn stderr $ + "copilot-bluespec: exception: " + ++ show (e :: IOException) + return False + ) + if result + then doesFileExist topExe + else return False + +-- ** Interfacing between Haskell and Bluespec + +-- | Bluespec type used to store values of a given type. +typeBluespec :: Typed a => Type a -> String +typeBluespec Bool = "Bool" +typeBluespec Int8 = "Int 8" +typeBluespec Int16 = "Int 16" +typeBluespec Int32 = "Int 32" +typeBluespec Int64 = "Int 64" +typeBluespec Word8 = "UInt 8" +typeBluespec Word16 = "UInt 16" +typeBluespec Word32 = "UInt 32" +typeBluespec Word64 = "UInt 64" +typeBluespec Float = "Float" +typeBluespec Double = "Double" +typeBluespec t@(Array tE) = + "Vector " ++ show (typeLength t) ++ "(" ++ typeBluespec tE ++ ")" +typeBluespec (Struct s) = typeName s + +-- | Show a value of a given type in Bluespec. +bluespecShow :: Type a -> a -> String +bluespecShow Bool x = show x +bluespecShow Int8 x = bluespecShowIntegral x +bluespecShow Int16 x = bluespecShowIntegral x +bluespecShow Int32 x = bluespecShowIntegral x +bluespecShow Int64 x = bluespecShowIntegral x +bluespecShow Word8 x = bluespecShowIntegral x +bluespecShow Word16 x = bluespecShowIntegral x +bluespecShow Word32 x = bluespecShowIntegral x +bluespecShow Word64 x = bluespecShowIntegral x +bluespecShow Float x = bluespecShowRealFloat 32 castFloatToWord32 x +bluespecShow Double x = bluespecShowRealFloat 64 castDoubleToWord64 x +bluespecShow (Array tE) x = genVector $ map (bluespecShow tE) $ arrayElems x +bluespecShow (Struct s) x = + typeName s + ++ "{ " + ++ intercalate ";" + (map + (\(Value fldTy fld@(Field val)) -> + fieldName fld ++ " = " ++ bluespecShow fldTy val) + (toValues x)) + ++ "}" + +-- | Show a value of a integral type (e.g., 'Int8' or 'Word8'). +bluespecShowIntegral :: (Integral a, Num a, Ord a, Show a) => a -> String +bluespecShowIntegral x + | x >= 0 = show x + -- Bluespec Haskell doesn't have negative integer literals, so something like + -- "-42" won't parse. Instead, we must rely on Bluespec's `negate` function. + -- + -- We must be careful to negate an Integer literal rather than than a + -- fixed-precision literal. For instance, suppose we wanted to display + -- (-128 :: Int8). We wouldn't want to do this by displaying `negate 128`, + -- since 128 isn't a valid Int8 value—the maximum Int8 value is 127! + -- Instead, we want to display `fromInteger (negate 128)`, where 128 is an + -- Integer. This way, `negate` can turn `128` to `-128` without issues. + | otherwise = "fromInteger (negate " ++ show (abs (toInteger x)) ++ ")" + +-- | Show a value of a floating-point type (e.g., 'Float' or 'Double'). We make +-- sure to convert NaN and infinity values to the corresponding Bluespec +-- @FloatingPoint@ functions that construct these values. +bluespecShowRealFloat :: + (Num float, Ord float, RealFloat float, Show float, Show word) + => Int + -> (float -> word) + -> float + -> String +bluespecShowRealFloat floatSizeInBits castFloatToWord float + -- We want to ensure that NaN values are correctly translated to Bluespec, + -- bit by bit. We have two mechanisms to do so. On the Haskell side, we have + -- `ieee754`'s `nanWithPayload` function, and on the Bluespec side, we have + -- `FloatingPoint`'s `nanQuiet` function. Unfortunately, their arguments are + -- of different types, and it isn't quite clear how to express one function + -- in terms of the other. + -- + -- To avoid this problem, we take a more indirect approach: we first cast + -- the Haskell floating-point value to a word and then `unpack` the word to + -- a floating-point value on the Bluespec side. It's somewhat verbose, but + -- it gets the job done reliably. + | isNaN float + = "unpack (" ++ show (castFloatToWord float) ++ + " :: Bit " ++ show floatSizeInBits ++ ")" + + | isInfinite float + = "infinity " ++ show floatIsNeg + + | floatIsNeg + = "negate " ++ show (abs float) + + | otherwise + = show float + where + floatIsNeg = (float < 0) || isNegativeZero float + +-- | Given a list of elements as arguments, show a @Vector@ expression. For +-- example, @'genVector' [\"27\", \"42\"]@ will return +-- @\"updateVector (updateVector newVector 0 27) 1 42)\"@. +genVector :: [String] -> String +genVector vals = + snd $ + foldl' + (\(!i, !v) x -> + (i+1, "update (" ++ v ++ ") " ++ show i ++ " (" ++ x ++ ")")) + (0 :: Int, "newVector") + vals + +-- | Display a value of a given type in Bluespec using @$display@. +class DisplayableInBluespec a where + displayInBluespec :: + proxy a -- ^ The type of the value. + -> String -- ^ The name of the Bluespec variable. + -> [String] -- ^ All arguments that are passed to @$display@. + +-- | Most Bluespec types can be displayed using @fshow@. +fshowDisplay :: proxy a -> String -> [String] +fshowDisplay _ output = ["(fshow " ++ output ++ ")"] + +-- | We display floating-point numbers by converting them to an integer and +-- printing them in hexadecimal (using the @%x@ modifier). This somewhat unusual +-- choice is motivated by the fact that this output is easier to parse than the +-- @fshow@ output. +hexFloatDisplay :: proxy a -> String -> [String] +hexFloatDisplay _ output = ["\"%x\"", output] + +instance DisplayableInBluespec Bool where + displayInBluespec = fshowDisplay + +instance DisplayableInBluespec Int8 where + displayInBluespec = fshowDisplay + +instance DisplayableInBluespec Int16 where + displayInBluespec = fshowDisplay + +instance DisplayableInBluespec Int32 where + displayInBluespec = fshowDisplay + +instance DisplayableInBluespec Int64 where + displayInBluespec = fshowDisplay + +instance DisplayableInBluespec Word8 where + displayInBluespec = fshowDisplay + +instance DisplayableInBluespec Word16 where + displayInBluespec = fshowDisplay + +instance DisplayableInBluespec Word32 where + displayInBluespec = fshowDisplay + +instance DisplayableInBluespec Word64 where + displayInBluespec = fshowDisplay + +instance DisplayableInBluespec Float where + displayInBluespec = hexFloatDisplay + +instance DisplayableInBluespec Double where + displayInBluespec = hexFloatDisplay + +instance DisplayableInBluespec a => DisplayableInBluespec (Array n a) where + displayInBluespec = fshowDisplay + +-- | @copilot-bluespec@–generated structs currently do not have @FShow@ +-- instances. (Perhaps they should: see +-- https://github.com/Copilot-Language/copilot-bluespec/issues/12) +-- In lieu of this, we manually define the same code that would be used in a +-- derived @FShow@ instance. +instance DisplayableInBluespec MyStruct where + displayInBluespec _ output = + [ "\"MyStruct { myStruct1 = %d ; myStruct2 = %d }\"" + , output ++ ".myStruct1" + , output ++ ".myStruct2" + ] + +-- | Read a value of a given type in Bluespec. +class ReadableFromBluespec a where + readFromBluespec :: String -> a + +instance ReadableFromBluespec Bool where + readFromBluespec = read + +instance ReadableFromBluespec Int8 where + readFromBluespec = read + +instance ReadableFromBluespec Int16 where + readFromBluespec = read + +instance ReadableFromBluespec Int32 where + readFromBluespec = read + +instance ReadableFromBluespec Int64 where + readFromBluespec = read + +instance ReadableFromBluespec Word8 where + readFromBluespec = read + +instance ReadableFromBluespec Word16 where + readFromBluespec = read + +instance ReadableFromBluespec Word32 where + readFromBluespec = read + +instance ReadableFromBluespec Word64 where + readFromBluespec = read + +-- We print out floating-point values in hexadecimal (see `hexFloatDisplay` +-- above), so we parse them accordingly here. + +instance ReadableFromBluespec Float where + readFromBluespec s = castWord32ToFloat $ read $ "0x" ++ s + +instance ReadableFromBluespec Double where + readFromBluespec s = castWord64ToDouble $ read $ "0x" ++ s + +instance (KnownNat n, ReadableFromBluespec a) => ReadableFromBluespec (Array n a) where + readFromBluespec s0 + | Just s1 <- stripPrefix "" s1 + = array $ map readFromBluespec $ words s2 + | otherwise + = error $ "Unexpected Vector fshow output: " ++ s0 + +instance ReadableFromBluespec MyStruct where + readFromBluespec str = + case readsEither (readsStruct minPrec) str of + Left err -> error err + Right ms -> ms + +-- | Attempt to read a value of type @a@. If successful, return 'Right' with +-- the read value. Otherwise, return @'Left' err@, where @err@ is an error +-- message describing what went wrong. +readsEither :: ReadS a -> String -> Either String a +readsEither readIt s = + case [ x | (x,"") <- readIt s ] of + [x] -> Right x + [] -> Left $ "readsEither: no parse: " ++ s + _ -> Left $ "readsEither: ambiguous parse: " ++ s + +-- ** Orphan instances for Arrays + +instance Eq a => Eq (Array n a) where + a1 == a2 = arrayElems a1 == arrayElems a2 + +instance AEq a => AEq (Array n a) where + a1 === a2 = arrayElems a1 === arrayElems a2 + +-- ** A simple struct definition for unit testing purposes + +data MyStruct = MyStruct + { myStruct1 :: Field "myStruct1" Int8 + , myStruct2 :: Field "myStruct2" Int8 + } + +-- | Like a derived @Eq@ instance, except that this looks through 'Field's. +instance Eq MyStruct where + MyStruct (Field f1a) (Field f2a) == MyStruct (Field f1b) (Field f2b) = + f1a == f1b && f2a == f2b +instance AEq MyStruct + +-- | Like a derived @Read@ instance, except that this adds 'Field' wrappers as +-- needed. +readsStruct :: Int -> ReadS MyStruct +readsStruct p = readParen (p > 10) $ \s -> do + ("MyStruct", s1) <- lex s + ("{", s2) <- lex s1 + ("myStruct1", s3) <- lex s2 + ("=", s4) <- lex s3 + (f1, s5) <- readsPrec 0 s4 + (";", s6) <- lex s5 + ("myStruct2", s7) <- lex s6 + ("=", s8) <- lex s7 + (f2, s9) <- readsPrec 0 s8 + ("}", s10) <- lex s9 + pure (MyStruct (Field f1) (Field f2), s10) + +instance Struct MyStruct where + typeName _ = "MyStruct" + toValues ms = [ Value Int8 (myStruct1 ms) + , Value Int8 (myStruct2 ms) + ] + +instance Typed MyStruct where + typeOf = Struct (MyStruct (Field 0) (Field 0)) + +-- | Unwrap a 'Field' to obtain the underlying value. +unField :: Field s t -> t +unField (Field val) = val diff --git a/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec/External.hs b/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec/External.hs new file mode 100644 index 00000000..01b1038b --- /dev/null +++ b/copilot-bluespec/tests/Test/Copilot/Compile/Bluespec/External.hs @@ -0,0 +1,63 @@ +{-# LANGUAGE ExistentialQuantification #-} + +-- | This is a duplicate version of @Copilot.Compile.Bluespec.External@ that is +-- specific to the test suite. Ideally, we would move this into a common library +-- that is shared between both @copilot-bluespec@ and @copilot-c99@ so that we +-- can avoid this duplication. See +-- https://github.com/Copilot-Language/copilot-bluespec/issues/3. +-- +-- Represent information about externs needed in the generation of Bluespec +-- code for stream declarations and triggers. +module Test.Copilot.Compile.Bluespec.External + ( External(..) + , gatherExts + ) where + +-- External imports +import Data.List (unionBy) + +-- External imports: Copilot +import Copilot.Core ( Expr (..), Stream (..), Trigger (..), Type, UExpr (..) ) + +-- | Representation of external variables. +data External = forall a. External + { extName :: String + , extType :: Type a + } + +-- | Collect all external variables from the streams and triggers. +-- +-- Although Copilot specifications can contain also properties and theorems, +-- the Bluespec backend currently only generates code for streams and triggers. +gatherExts :: [Stream] -> [Trigger] -> [External] +gatherExts streams triggers = streamsExts `extUnion` triggersExts + where + streamsExts = foldr (extUnion . streamExts) mempty streams + triggersExts = foldr (extUnion . triggerExts) mempty triggers + + streamExts :: Stream -> [External] + streamExts (Stream _ _ expr _) = exprExts expr + + triggerExts :: Trigger -> [External] + triggerExts (Trigger _ guard args) = guardExts `extUnion` argExts + where + guardExts = exprExts guard + argExts = concatMap uExprExts args + + uExprExts :: UExpr -> [External] + uExprExts (UExpr _ expr) = exprExts expr + + exprExts :: Expr a -> [External] + exprExts (Local _ _ _ e1 e2) = exprExts e1 `extUnion` exprExts e2 + exprExts (ExternVar ty name _) = [External name ty] + exprExts (Op1 _ e) = exprExts e + exprExts (Op2 _ e1 e2) = exprExts e1 `extUnion` exprExts e2 + exprExts (Op3 _ e1 e2 e3) = exprExts e1 `extUnion` exprExts e2 + `extUnion` exprExts e3 + exprExts (Label _ _ e) = exprExts e + exprExts _ = [] + + -- | Union over lists of External, we solely base the equality on the + -- extName's. + extUnion :: [External] -> [External] -> [External] + extUnion = unionBy (\a b -> extName a == extName b)