diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 9235a2a27..9072a0a43 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) * Disable test suite via newly added manual cabal flag. (#673) diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal index b727af7fa..3ac0839cf 100644 --- a/copilot-bluespec/copilot-bluespec.cabal +++ b/copilot-bluespec/copilot-bluespec.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-bluespec -version : 4.6.1 +version : 4.7 synopsis : A compiler for Copilot targeting FPGAs. description : This package is a back-end from Copilot to FPGAs in Bluespec. @@ -51,8 +51,8 @@ library , ieee754 >= 0.8.0 && < 0.9 , pretty >= 1.1.2 && < 1.2 - , copilot-core >= 4.6.1 && < 4.7 - , language-bluespec >= 0.1 && < 0.2 + , copilot-core >= 4.7 && < 4.8 + , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 7a2ef8da6..856d51497 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,7 @@ +2026-03-07 + * Version bump (4.7). (#714) + * Raise error when compiling empty arrays or structs. (#695) + 2026-01-07 * Version bump (4.6.1). (#705) diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal index 40407cec2..0567e9416 100644 --- a/copilot-c99/copilot-c99.cabal +++ b/copilot-c99/copilot-c99.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-c99 -version : 4.6.1 +version : 4.7 synopsis : A compiler for Copilot targeting C99. description : This package is a back-end from Copilot to C. @@ -45,7 +45,7 @@ library , mtl >= 2.2 && < 2.4 , pretty >= 1.1 && < 1.2 - , copilot-core >= 4.6.1 && < 4.7 + , copilot-core >= 4.7 && < 4.8 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 diff --git a/copilot-c99/src/Copilot/Compile/C99/Error.hs b/copilot-c99/src/Copilot/Compile/C99/Error.hs index f42c794de..8ab2de608 100644 --- a/copilot-c99/src/Copilot/Compile/C99/Error.hs +++ b/copilot-c99/src/Copilot/Compile/C99/Error.hs @@ -5,7 +5,10 @@ -- -- Custom functions to report error messages to users. module Copilot.Compile.C99.Error - ( impossible ) + ( impossible + , errorEmptyStruct + , errorZeroLengthArray + ) where -- | Report an error due to a bug in Copilot. @@ -18,3 +21,17 @@ impossible function package = ++ ". Please file an issue at " ++ "https://github.com/Copilot-Language/copilot/issues" ++ " or email the maintainers at " + +-- | Report an error when attempting to compile a zero-length array to C99. +-- C99 does not support zero-length arrays, so Copilot cannot compile +-- specifications that use them. +errorZeroLengthArray :: a +errorZeroLengthArray = + error "copilot-c99: Cannot compile zero-length arrays to C99.\n" + +-- | Report an error when attempting to compile an empty struct to C99. +-- C99 does not support empty structs, so Copilot cannot compile +-- specifications that use them. +errorEmptyStruct :: a +errorEmptyStruct = + error "copilot-c99: Cannot compile empty structs to C99.\n" diff --git a/copilot-c99/src/Copilot/Compile/C99/Expr.hs b/copilot-c99/src/Copilot/Compile/C99/Expr.hs index 14e129be9..fec731fbf 100644 --- a/copilot-c99/src/Copilot/Compile/C99/Expr.hs +++ b/copilot-c99/src/Copilot/Compile/C99/Expr.hs @@ -18,7 +18,7 @@ import Copilot.Core ( Array, Expr (..), Field (..), Op1 (..), Op2 (..), arrayElems, toValues, typeLength, typeSize ) -- Internal imports -import Copilot.Compile.C99.Error ( impossible ) +import Copilot.Compile.C99.Error ( impossible, errorEmptyStruct, errorZeroLengthArray ) import Copilot.Compile.C99.Name ( exCpyName, streamAccessorName ) import Copilot.Compile.C99.Type ( transLocalVarDeclType, transType, transTypeName ) @@ -371,14 +371,23 @@ constFieldInit (Value ty (Field val)) = C.InitItem Nothing $ constInit ty val -- | Transform a Copilot Struct, based on the struct fields, into a list of C99 -- initializer values. +-- +-- Raises an error if the struct is empty, as C99 does not support structs with +-- no fields. constStruct :: [Value a] -> NonEmpty.NonEmpty C.InitItem -constStruct val = NonEmpty.fromList $ map constFieldInit val +constStruct val = case val of + [] -> errorEmptyStruct + _ -> NonEmpty.fromList $ map constFieldInit val -- | Transform a Copilot Array, based on the element values and their type, -- into a list of C99 initializer values. +-- +-- Raises an error if the array is empty, as C99 does not support zero-length +-- arrays. constArray :: Type a -> [a] -> NonEmpty.NonEmpty C.InitItem -constArray ty = - NonEmpty.fromList . map (C.InitItem Nothing . constInit ty) +constArray ty xs = case xs of + [] -> errorZeroLengthArray + _ -> NonEmpty.fromList $ map (C.InitItem Nothing . constInit ty) xs -- | Explicitly cast a C99 value to a type. explicitTy :: Type a -> C.Expr -> C.Expr diff --git a/copilot-c99/src/Copilot/Compile/C99/Type.hs b/copilot-c99/src/Copilot/Compile/C99/Type.hs index 78777617b..525fccea9 100644 --- a/copilot-c99/src/Copilot/Compile/C99/Type.hs +++ b/copilot-c99/src/Copilot/Compile/C99/Type.hs @@ -12,7 +12,9 @@ module Copilot.Compile.C99.Type import qualified Language.C99.Simple as C -- Internal imports: Copilot -import Copilot.Core ( Type (..), typeLength, typeName ) +import Copilot.Core ( Struct (..), Type (..), typeLength, + typeName ) +import Copilot.Compile.C99.Error ( errorEmptyStruct, errorZeroLengthArray ) -- | Translate a Copilot type to a C99 type. transType :: Type a -> C.Type @@ -28,10 +30,12 @@ transType ty = case ty of Word64 -> C.TypeSpec $ C.TypedefName "uint64_t" Float -> C.TypeSpec C.Float Double -> C.TypeSpec C.Double - Array ty' -> C.Array (transType ty') len + Array ty' | typeLength ty == 0 -> errorZeroLengthArray + | otherwise -> C.Array (transType ty') len where len = Just $ C.LitInt $ fromIntegral $ typeLength ty - Struct s -> C.TypeSpec $ C.Struct (typeName s) + Struct s | null (toValues s) -> errorEmptyStruct + | otherwise -> C.TypeSpec $ C.Struct (typeName s) -- | Translate a Copilot type to a valid (local) variable declaration C99 type. -- diff --git a/copilot-c99/tests/Test/Copilot/Compile/C99.hs b/copilot-c99/tests/Test/Copilot/Compile/C99.hs index 60276e870..b02fc23ae 100644 --- a/copilot-c99/tests/Test/Copilot/Compile/C99.hs +++ b/copilot-c99/tests/Test/Copilot/Compile/C99.hs @@ -8,10 +8,11 @@ module Test.Copilot.Compile.C99 -- External imports import Control.Arrow ((&&&)) -import Control.Exception (IOException, catch) -import Control.Monad (when) +import Control.Exception (ErrorCall (..), IOException, catch, + try) +import Control.Monad (unless, when) import Data.Bits (Bits, complement) -import Data.List (intercalate) +import Data.List (intercalate, isSubsequenceOf) import Data.Type.Equality (testEquality) import Data.Typeable (Proxy (..), (:~:) (Refl)) import GHC.TypeLits (KnownNat, natVal) @@ -24,7 +25,9 @@ import System.Posix.Temp (mkdtemp) import System.Process (callProcess, readProcess) import System.Random (Random) import Test.Framework (Test, testGroup) +import Test.Framework.Providers.HUnit (testCase) import Test.Framework.Providers.QuickCheck2 (testProperty) +import Test.HUnit (Assertion, assertFailure) import Test.QuickCheck (Arbitrary, Gen, Property, arbitrary, choose, elements, forAll, forAllBlind, frequency, @@ -50,6 +53,7 @@ tests = , testProperty "Compile specification in custom dir" testCompileCustomDir , testProperty "Run specification" testRun , testProperty "Run and compare results" testRunCompare + , testCase "Reject empty arrays and structs" testRejectEmpties ] -- * Individual tests @@ -137,6 +141,65 @@ testCompileCustomDir = ioProperty $ do args = [] +data Empty = Empty + +instance Struct Empty where + typeName _ = "" + toValues _ = [] + +instance Typed Empty where + typeOf = Struct Empty + +-- | Test that compiling a spec with an empty array or struct raises an error. +-- C99 does not support zero-length arrays or structs without fields, so Copilot +-- should report an error during compilation. +testRejectEmpties :: Assertion +testRejectEmpties = do + tmpDir <- getTemporaryDirectory + setCurrentDirectory tmpDir + + r1 <- try (compile "copilot_test" $ spec t1) :: IO (Either ErrorCall ()) + unless (isErrZeroArray r1) $ assertFailure "Const zero-length array" + + r2 <- try (compile "copilot_test" $ spec t2) :: IO (Either ErrorCall ()) + unless (isErrZeroArray r2) $ assertFailure "Extern zero-length array" + + r3 <- try (compile "copilot_test" $ spec t3) :: IO (Either ErrorCall ()) + unless (isErrEmptyStruct r3) $ assertFailure "Const empty struct" + + r4 <- try (compile "copilot_test" $ spec t4) :: IO (Either ErrorCall ()) + unless (isErrEmptyStruct r4) $ assertFailure "Extern empty struct" + + where + + spec a = Spec streams observers (triggers a) properties + + streams = [] + observers = [] + triggers a = [ Trigger "trig" (Const Bool True) a ] + properties = [] + + t1 = [ UExpr arrTy (Const arrTy (array [])) ] + t2 = [ UExpr arrTy (ExternVar arrTy "arrs" Nothing) ] + t3 = [ UExpr structTy (Const structTy Empty) ] + t4 = [ UExpr structTy (ExternVar structTy "structs" Nothing) ] + + arrTy :: Type (Array 0 Bool) + arrTy = Array Bool + + structTy :: Type Empty + structTy = Struct Empty + + isErrZeroArray :: Either ErrorCall a -> Bool + isErrZeroArray e = case e of + Left (ErrorCall msg) -> "zero-length array" `isSubsequenceOf` msg + _ -> False + + isErrEmptyStruct :: Either ErrorCall a -> Bool + isErrEmptyStruct e = case e of + Left (ErrorCall msg) -> "empty struct" `isSubsequenceOf` msg + _ -> False + -- | Test compiling a spec and running the resulting program. -- -- The actual behavior is ignored. diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index c00db088a..671e39ef6 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal index 336db0f26..6d99e77d6 100644 --- a/copilot-core/copilot-core.cabal +++ b/copilot-core/copilot-core.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-core -version: 4.6.1 +version: 4.7 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 1827da72f..c2920d179 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal index 7395226ab..9ef09f117 100644 --- a/copilot-interpreter/copilot-interpreter.cabal +++ b/copilot-interpreter/copilot-interpreter.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-interpreter -version: 4.6.1 +version: 4.7 synopsis: Interpreter for Copilot. description: Interpreter for Copilot. @@ -44,7 +44,7 @@ library base >= 4.9 && < 5, pretty >= 1.0 && < 1.2, - copilot-core >= 4.6.1 && < 4.7 + copilot-core >= 4.7 && < 4.8 exposed-modules: diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index eca064537..4751f7061 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) * Relax version constraint on containers. (#603) diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal index 0b65b5798..740bb2b8c 100644 --- a/copilot-language/copilot-language.cabal +++ b/copilot-language/copilot-language.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-language -version: 4.6.1 +version: 4.7 synopsis: A Haskell-embedded DSL for monitoring hard real-time distributed systems. description: @@ -42,9 +42,9 @@ library , data-reify >= 0.6 && < 0.7 , mtl >= 2.0 && < 3 - , copilot-core >= 4.6.1 && < 4.7 - , copilot-interpreter >= 4.6.1 && < 4.7 - , copilot-theorem >= 4.6.1 && < 4.7 + , copilot-core >= 4.7 && < 4.8 + , copilot-interpreter >= 4.7 && < 4.8 + , copilot-theorem >= 4.7 && < 4.8 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 6ae010b91..171b9b7d7 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) * Relax version constraint on containers. (#603) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index c864c9cda..e194daf78 100644 --- a/copilot-libraries/copilot-libraries.cabal +++ b/copilot-libraries/copilot-libraries.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-libraries -version: 4.6.1 +version: 4.7 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -38,10 +38,10 @@ library build-depends: base >= 4.9 && < 5 - , containers >= 0.4 && < 0.9 - , mtl >= 2.0 && < 2.4 - , parsec >= 2.0 && < 3.2 - , copilot-language >= 4.6.1 && < 4.7 + , containers >= 0.4 && < 0.9 + , mtl >= 2.0 && < 2.4 + , parsec >= 2.0 && < 3.2 + , copilot-language >= 4.7 && < 4.8 exposed-modules: Copilot.Library.Libraries diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index ed0b61ad9..efa6ccf51 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal index b303db95f..f6f5fcc57 100644 --- a/copilot-prettyprinter/copilot-prettyprinter.cabal +++ b/copilot-prettyprinter/copilot-prettyprinter.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-prettyprinter -version: 4.6.1 +version: 4.7 synopsis: A prettyprinter of Copilot Specifications. description: A prettyprinter of Copilot specifications. @@ -45,7 +45,7 @@ library base >= 4.9 && < 5, pretty >= 1.0 && < 1.2, - copilot-core >= 4.6.1 && < 4.7 + copilot-core >= 4.7 && < 4.8 exposed-modules: diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index f3dd23d68..4aaf2cf97 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) * Relax version constraint on containers, random. (#603) diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index 173e90eca..f8b4ff57e 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.6.1 +version : 4.7 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -62,8 +62,8 @@ library , xml >= 1.3 && < 1.4 , what4 >= 1.3 && < 1.8 - , copilot-core >= 4.6.1 && < 4.7 - , copilot-prettyprinter >= 4.6.1 && < 4.7 + , copilot-core >= 4.7 && < 4.8 + , copilot-prettyprinter >= 4.7 && < 4.8 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index ca8740289..049ec2243 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,7 @@ +2026-03-07 + * Version bump (4.7). (#714) + * Relax version constraints on what4. (#716) + 2026-01-07 * Version bump (4.6.1). (#705) diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index f77ebfcaf..c7bf36a10 100644 --- a/copilot-verifier/copilot-verifier.cabal +++ b/copilot-verifier/copilot-verifier.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: copilot-verifier -Version: 4.6.1 +Version: 4.7 Author: Galois Inc. Maintainer: rscott@galois.com Copyright: (c) Galois, Inc 2021-2024 @@ -45,9 +45,9 @@ common bldflags bv-sized >= 1.0.0 && < 1.1, bytestring, containers >= 0.5.9.0, - copilot-c99 >= 4.6.1 && < 4.7, - copilot-core >= 4.6.1 && < 4.7, - copilot-theorem >= 4.6.1 && < 4.7, + copilot-c99 >= 4.7 && < 4.8, + copilot-core >= 4.7 && < 4.8, + copilot-theorem >= 4.7 && < 4.8, crucible >= 0.7.1 && < 0.8, crucible-llvm >= 0.7 && < 0.8, crux >= 0.7.1 && < 0.8, @@ -62,7 +62,7 @@ common bldflags text, transformers, vector, - what4 >= 1.6.1 && < 1.7 + what4 >= 1.6.1 && < 1.8 library import: bldflags @@ -80,10 +80,10 @@ library copilot-verifier-examples hs-source-dirs: examples build-depends: case-insensitive, - copilot >= 4.6.1 && < 4.7, - copilot-language >= 4.6.1 && < 4.7, - copilot-libraries >= 4.6.1 && < 4.7, - copilot-prettyprinter >= 4.6.1 && < 4.7, + copilot >= 4.7 && < 4.8, + copilot-language >= 4.7 && < 4.8, + copilot-libraries >= 4.7 && < 4.8, + copilot-prettyprinter >= 4.7 && < 4.8, copilot-verifier exposed-modules: Copilot.Verifier.Examples diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 85bc41739..402ec34d5 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,7 @@ +2026-03-07 + * Version bump (4.7). (#714) + * Relax version constraints on ogma-extra. (#716) + 2026-01-07 * Version bump (4.6.1). (#705) diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal index c481a8d00..0500c1b43 100644 --- a/copilot-visualizer/copilot-visualizer.cabal +++ b/copilot-visualizer/copilot-visualizer.cabal @@ -1,6 +1,6 @@ cabal-version: >= 1.10 name: copilot-visualizer -version: 4.6.1 +version: 4.7 synopsis: Visualizer for Copilot. description: Visualizer for Copilot. @@ -61,14 +61,14 @@ library filepath >= 1.4.2 && < 1.6, hint >= 0.9.0 && < 1.10, pretty >= 1.0 && < 1.2, - ogma-extra >= 1.6.0 && < 1.10, + ogma-extra >= 1.6.0 && < 1.13, text >= 1.2.3.1 && < 2.2, websockets >= 0.12.7 && < 0.14, - copilot >= 4.6.1 && < 4.7, - copilot-core >= 4.6.1 && < 4.7, - copilot-interpreter >= 4.6.1 && < 4.7, - copilot-language >= 4.6.1 && < 4.7 + copilot >= 4.7 && < 4.8, + copilot-core >= 4.7 && < 4.8, + copilot-interpreter >= 4.7 && < 4.8, + copilot-language >= 4.7 && < 4.8 exposed-modules: @@ -121,7 +121,7 @@ executable tikz-example build-depends: base >= 4.9 && < 5, - copilot >= 4.6.1 && < 4.7, + copilot >= 4.7 && < 4.8, copilot-visualizer if flag(examples) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index 15678af71..dd34bc70f 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2026-03-07 + * Version bump (4.7). (#714) + 2026-01-07 * Version bump (4.6.1). (#705) * Relax version constraint on optparse-applicative. (#603) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index 66304a0f8..68ff811ec 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.6.1 +version: 4.7 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE @@ -52,12 +52,12 @@ library , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.6 - , copilot-core >= 4.6.1 && < 4.7 - , copilot-theorem >= 4.6.1 && < 4.7 - , copilot-language >= 4.6.1 && < 4.7 - , copilot-libraries >= 4.6.1 && < 4.7 - , copilot-c99 >= 4.6.1 && < 4.7 - , copilot-prettyprinter >= 4.6.1 && < 4.7 + , copilot-core >= 4.7 && < 4.8 + , copilot-theorem >= 4.7 && < 4.8 + , copilot-language >= 4.7 && < 4.8 + , copilot-libraries >= 4.7 && < 4.8 + , copilot-c99 >= 4.7 && < 4.8 + , copilot-prettyprinter >= 4.7 && < 4.8 exposed-modules: Language.Copilot, Language.Copilot.Main