diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 000000000..21e929e6c --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,66 @@ +name: build + +# Trigger the workflow on push or pull request +on: + - pull_request + - push + +jobs: + cabal: + name: ${{ matrix.os }} / ghc ${{ matrix.ghc }} / cabal ${{ matrix.cabal }} + runs-on: ${{ matrix.os }} + strategy: + matrix: + os: [ubuntu-26.04] + cabal: ["2.4", "3.2", "3.4"] + ghc: + - "8.6.5" + - "8.8.4" + - "8.10.4" + - "9.0.1" + + steps: + + - uses: haskell-actions/setup@main + id: setup-haskell-cabal + name: Setup Haskell + continue-on-error: true + with: + ghc-version: ${{ matrix.ghc }} + cabal-version: ${{ matrix.cabal }} + + - name: Prepare environment + run: | + echo "$HOME/.ghcup/bin" >> $GITHUB_PATH + echo "$HOME/.cabal/bin" >> $GITHUB_PATH + sed -i -e "s;-- \(secure.\) True;\1 False;g" $HOME/.cabal/config + cabal update + + - uses: actions/checkout@v7 + + - name: Install dependencies + run: | + sudo apt-get install -y cppcheck z3 + + - name: Format check + run: | + # Fail if the any non-binary files contain trailing spaces. + if grep -nIHre ' \+$' * ; then exit 1; fi + + # Fail if the code, Cabal files, documentation or CHANGELOGs contain tabs. + if grep -rP '\t' --include='*.hs' --include='*.cabal' --include='*.md' --include='CHANGELOG' . ; then exit 1; fi + + - name: Install copilot + run: | + cabal v2-install --lib copilot/ copilot-core/ copilot-c99/ copilot-language/ copilot-libraries/ copilot-theorem/ copilot-interpreter/ copilot-prettyprinter/ + + - name: Test packages + if: matrix.ghc == '8.10.4' + run: | + cabal v2-test -j1 copilot-core/ copilot-language/ copilot-interpreter/ copilot-c99/ copilot-theorem/ copilot-libraries/ + + - name: Check cpp + if: matrix.ghc == '8.10.4' + run: | + export GHC_ENVIRONMENT=~/.ghc/x86_64-linux-8.10.4/environments/default + runhaskell copilot/examples/Heater.hs; cppcheck --force --addon=misra.py --suppress=misra-c2012-14.4 --error-exitcode=2 heater.c diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index c7c69118d..000000000 --- a/.travis.yml +++ /dev/null @@ -1,50 +0,0 @@ -# dist should be at least focal because we need cppcheck >= 1.88. -dist: focal - -# NB: don't set `language: haskell` here - -# The following enables several GHC versions to be tested; often it's enough to -# test only against the last release in a major GHC version. Feel free to omit -# lines listings versions you don't need/want testing for. -env: - - CABALVER=2.4 GHCVER=8.6.5 - - CABALVER=3.2 GHCVER=8.8.4 - - CABALVER=3.2 GHCVER=8.10.4 - - CABALVER=3.4 GHCVER=9.0.1 -# - CABALVER=head GHCVER=head # see section about GHC HEAD snapshots - -# Note: the distinction between `before_install` and `install` is not important. -before_install: - - travis_retry sudo add-apt-repository -y ppa:hvr/ghc - - travis_retry sudo apt-get update - - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER # see note about happy/alex - - # We install z3 and cppcheck only for the tests, since they are not needed - # for normal compilation. - - if [ "${GHCVER}" == "8.10.4" ]; then travis_retry sudo apt-get install --yes z3 cppcheck; fi - - - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH - - cabal --version - - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]" - - travis_retry cabal update - - git submodule update --remote - -script: - # We explicitly install all libraries so that they are exposed and we can use - # them for tests (e.g., with runhaskell). There is no harm in doing this - # instead of installing just copilot. - - travis_wait 30 cabal v2-install --lib copilot copilot-core copilot-c99 copilot-language copilot-libraries copilot-theorem copilot-interpreter copilot-prettyprinter - - # Run tests only on GHC 8.10.4 - # - # Only libraries with tests are listed below or the v2-test command fails. - # - # Testing copilot-theorem and copilot-libraries requires z3. See above - # conditional installation, and keep GHC version numbers in both places in - # sync. - - if [ "${GHCVER}" == "8.10.4" ]; then cabal v2-test -j1 copilot-core copilot-language copilot-interpreter copilot-c99 copilot-theorem copilot-libraries; fi - - # Check that the code produced by Copilot complies with MISRA C 2012. We - # explicitly make cppcheck produce a non-zero exit code on non-compliance - # with the standard to make the CI build fail. - - if [ "${GHCVER}" == "8.10.4" ]; then runhaskell copilot/examples/Heater.hs; cppcheck --force --addon=misra.py --suppress=misra-c2012-14.4 --error-exitcode=2 heater.c; fi diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 63ea6878b..b5130fa0b 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,15 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + * Replace tabs in `DESIGN.md`. (#772) + * Remove trailing spaces. (#775) + +2026-09-07 + * Version bump (4.8.1). (#760) + * Replace tab in CHANGELOG. (#755) + +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) * Fix translation of special Float values to Bluespec. (#697) @@ -8,7 +20,7 @@ 2026-01-07 * Version bump (4.6.1). (#705) * Disable test suite via newly added manual cabal flag. (#673) - * Fix translation of constant floating-point values. (#696) + * Fix translation of constant floating-point values. (#696) 2025-11-07 * Version bump (4.6). (#679) diff --git a/copilot-bluespec/DESIGN.md b/copilot-bluespec/DESIGN.md index b5a07dd31..6cf5cd610 100644 --- a/copilot-bluespec/DESIGN.md +++ b/copilot-bluespec/DESIGN.md @@ -418,15 +418,15 @@ This generates a Verilog module `mkFibs.v` that looks like the following: ```verilog module mkFibs(CLK, - RST_N, + RST_N, - even_guard, + even_guard, - even_arg0, + even_arg0, - odd_guard, + odd_guard, - odd_arg0); + odd_arg0); input CLK; input RST_N; @@ -815,17 +815,17 @@ that looks like the following: ```verilog module mkFibs(CLK, - RST_N, + RST_N, - even_guard, + even_guard, - even_arg0, + even_arg0, - odd_guard, + odd_guard, - odd_arg0, + odd_arg0, - fibs); + fibs); input CLK; input RST_N; diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal index ffaadaca2..1d8f7b3af 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.7.1 +version : 4.8.2 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.7.1 && < 4.8 - , language-bluespec >= 0.1 && < 0.2 + , copilot-core >= 4.8.2 && < 4.9 + , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec diff --git a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs index 2b71b3957..84a9ffe7a 100644 --- a/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs +++ b/copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs @@ -627,43 +627,43 @@ constInt ty i -- | Translate a Copilot floating-point literal into a Bluespec expression. constFP :: Type ty -> Double -> BS.CExpr constFP ty d - -- Bluespec internally represents all IEEE floating-point values as structs + -- Bluespec internally represents all IEEE floating-point values as structs -- so special symbols have to be called for constructing special values, -- e.g. NaN, inf, and -0.0. See -- https://github.com/B-Lang-org/bsc/blob/main/src/Libraries/Base3-Math/FloatingPoint.bsv#L441 - | isInfinite d = BS.CApply - (BS.CVar $ BS.mkId BS.NoPos "infinity") + | isInfinite d = BS.CApply + (BS.CVar $ BS.mkId BS.NoPos "infinity") [ if d < 0 - then BS.CCon BS.idTrue [] + then BS.CCon BS.idTrue [] else BS.CCon BS.idFalse [] ] - - | isNaN d = let - cexpr = BS.CHasType + + | isNaN d = let + cexpr = BS.CHasType ( BS.CLit $ BS.CLiteral BS.NoPos $ BS.LInt $ BS.IntLit Nothing 10 cval ) - ( BS.CQType [] $ BS.TCon $ - BS.TyCon - (BS.mkId BS.NoPos ctype) - Nothing + ( BS.CQType [] $ BS.TCon $ + BS.TyCon + (BS.mkId BS.NoPos ctype) + Nothing BS.TIabstract ) - cval = case ty of - Float -> fromIntegral $ + cval = case ty of + Float -> fromIntegral $ castFloatToWord32 $ uncastDoubleNaNToFloat d - Double -> fromIntegral $ + Double -> fromIntegral $ castDoubleToWord64 d _ -> impossible "constFP" "copilot-bluespec" - ctype = case ty of + ctype = case ty of Float -> "Bit 32" Double -> "Bit 64" _ -> impossible "constFP" "copilot-bluespec" in BS.CApply (BS.CVar $ BS.mkId BS.NoPos "unpack") [cexpr] - | d == 0 = BS.CApply - (BS.CVar $ BS.mkId BS.NoPos "zero") - [ if isNegativeZero d - then BS.CCon BS.idTrue [] + | d == 0 = BS.CApply + (BS.CVar $ BS.mkId BS.NoPos "zero") + [ if isNegativeZero d + then BS.CCon BS.idTrue [] else BS.CCon BS.idFalse [] ] | d > 0 = withTypeAnnotation ty $ cLit $ BS.LReal d @@ -676,13 +676,13 @@ constFP ty d [cLit $ BS.LReal $ negate d] -- Because NaNs are specially placed as bit-representations by `constfp` and `constfp` requires Doubles as inputs, --- we need to convert NaN doubles safely into NaN floats. GHC Double2Float does not preserve signal nor payload +-- we need to convert NaN doubles safely into NaN floats. GHC Double2Float does not preserve signal nor payload -- internals of NaNs so in this case we need a special conversion. uncastDoubleNaNToFloat :: Double -> Float -uncastDoubleNaNToFloat nan = if (isSignaling nan) - then (setPayloadSignaling payload) +uncastDoubleNaNToFloat nan = if (isSignaling nan) + then (setPayloadSignaling payload) else (setPayload payload) - where + where payload = double2Float $ getPayload nan -- | Create a Bluespec expression consisting of a literal. diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 74c6c1dd4..b53dcc838 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,12 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + +2026-09-07 + * Version bump (4.8.1). (#760) + +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal index d9802bd42..7e1e3d17a 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.7.1 +version : 4.8.2 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.7.1 && < 4.8 + , copilot-core >= 4.8.2 && < 4.9 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 4a019a359..033129dbc 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,18 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + * Increase test coverage for `Copilot.Core.Type.Array`. (#767) + * Fix errors in the documentation of `Copilot.Core.Spec`. (#769) + * Replace tab in CHANGELOG. (#772) + * Fix comments for two tests in `Test.Copilot.Core.Type`. (#781) + * Fix typo in Haddock comment of test property. (#783) + * Fix test to use `typeSize` instead of `typeLength` (#784). + +2026-09-07 + * Version bump (4.8.1). (#760) + +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal index ee463977c..288399a9c 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.7.1 +version: 4.8.2 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. diff --git a/copilot-core/src/Copilot/Core/Spec.hs b/copilot-core/src/Copilot/Core/Spec.hs index 6614d0621..e8972c928 100644 --- a/copilot-core/src/Copilot/Core/Spec.hs +++ b/copilot-core/src/Copilot/Core/Spec.hs @@ -11,9 +11,9 @@ -- and their handling functions, or streams to observe, or a theorem that must -- be proved. -- --- In order to be executed, high-level Copilot Language Spec must be turned --- into Copilot Core's 'Spec'. This module defines the low-level Copilot Core --- representations for Specs and the main types of element in a spec. +-- In order to be executed, a high-level Copilot Language @Spec@ must be +-- turned into a Copilot Core 'Spec'. This module defines the low-level Copilot +-- Core representation for 'Spec' and the main types of element in a spec. module Copilot.Core.Spec ( Stream (..) , Observer (..) @@ -32,9 +32,9 @@ import Data.Typeable (Typeable) import Copilot.Core.Expr (Expr, Id, Name, UExpr) import Copilot.Core.Type (Type, Typed) --- | A stream in an infinite succession of values of the same type. +-- | A stream is an infinite succession of values of the same type. -- --- Stream can carry different types of data. Boolean streams play a special +-- Streams can carry different types of data. Boolean streams play a special -- role: they are used by other parts (e.g., 'Trigger') to detect when the -- properties being monitored are violated. data Stream = forall a . (Typeable a, Typed a) => Stream diff --git a/copilot-core/src/Copilot/Core/Type/Array.hs b/copilot-core/src/Copilot/Core/Type/Array.hs index b11e8949b..07c10ba31 100644 --- a/copilot-core/src/Copilot/Core/Type/Array.hs +++ b/copilot-core/src/Copilot/Core/Type/Array.hs @@ -37,7 +37,7 @@ array xs | datalen == typelen = Array xs | otherwise = error errmsg where datalen = length xs - typelen = fromIntegral $ natVal (Proxy :: Proxy n) + typelen = fromIntegral $ natVal $! (Proxy :: Proxy n) errmsg = "Length of data (" ++ show datalen ++ ") does not match length of type (" ++ show typelen ++ ")." diff --git a/copilot-core/tests/Test/Copilot/Core/Type.hs b/copilot-core/tests/Test/Copilot/Core/Type.hs index 9f9cb6d5e..47d8c5940 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type.hs @@ -165,7 +165,7 @@ testTypeLength1 = property $ typeLength a == 3 a :: Type (Array 3 Int8) a = Array Int8 --- | Test that the length of an multi-dimensional array is as expected. +-- | Test that the length of a multi-dimensional array is as expected. testTypeLength2 :: Property testTypeLength2 = property $ typeLength a == 3 where @@ -174,7 +174,7 @@ testTypeLength2 = property $ typeLength a == 3 -- | Test that the size of an array is as expected. testTypeSize1 :: Property -testTypeSize1 = property $ typeLength a == 3 +testTypeSize1 = property $ typeSize a == 3 where a :: Type (Array 3 Int8) a = Array Int8 @@ -350,7 +350,7 @@ testShowStruct = forAll arbitrary $ \k1 -> forAll arbitrary $ \k2 -> show (S (Field k1) (Field k2)) == "" --- | Test showing a struct. +-- | Test updating a struct. testUpdateStruct :: Property testUpdateStruct = forAll arbitrary $ \k1 -> @@ -364,7 +364,7 @@ testUpdateStruct = where unField (Field x) = x --- | Test showing a struct. +-- | Test updating a struct (should fail). testUpdateStructFail :: Property testUpdateStructFail = expectFailure $ forAll arbitrary $ \k1 -> diff --git a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs index e070f138b..0af0ffae9 100644 --- a/copilot-core/tests/Test/Copilot/Core/Type/Array.hs +++ b/copilot-core/tests/Test/Copilot/Core/Type/Array.hs @@ -11,8 +11,9 @@ import Test.Framework (Test, testGroup) import Test.Framework.Providers.QuickCheck2 (testProperty) import Test.QuickCheck (Gen, Property, arbitrary, chooseInt, expectFailure, forAll, - getNegative, getNonNegative, oneof, - property, vector, vectorOf) + getNegative, getNonNegative, + listOf, oneof, property, vector, + vectorOf) -- Internal imports: library modules being tested import Copilot.Core.Type.Array (Array, array, arrayElems, arrayUpdate) @@ -31,6 +32,10 @@ tests = testArrayElemsFail , testProperty "Show for arrays" testShowArray + , testProperty "showsPrec for arrays" + testShowsPrecArray + , testProperty "showList for arrays" + testShowListArray , testProperty "arrayElems (arrayUpdate x i v) !! i == v" (testArrayUpdateElem (Proxy :: Proxy 5)) , testProperty "arrayUpdate x i ((arrayElems x) !! i) == x" @@ -70,6 +75,17 @@ testShowArray :: Property testShowArray = forAll (vector 3) $ \l -> property $ show (array l :: Array 3 Int64) == show (l :: [Int64]) +-- | Test 'Show.showsPrec' for 'Array's. +testShowsPrecArray :: Property +testShowsPrecArray = forAll (getNonNegative <$> arbitrary) $ \prec -> + forAll (vector 3) $ \l -> property $ + showsPrec prec (array l :: Array 3 Int64) "" == show (l :: [Int64]) + +-- | Test 'Show.showList' for 'Array's. +testShowListArray :: Property +testShowListArray = forAll (listOf $ vector 3) $ \l -> property $ + showList (map array l :: [Array 3 Int64]) "" == show (l :: [[Int64]]) + -- | Test that updating an array updates the element appropriately (if we -- project that element we get the value we put in). testArrayUpdateElem :: forall n . KnownNat n => Proxy n -> Property diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 53984488e..55cdec51c 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,13 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + * Replace tab in `Copilot.Interpreter.Eval`. (#772) + +2026-09-07 + * Version bump (4.8.1). (#760) + +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal index 0303bf17b..60152a66a 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.7.1 +version: 4.8.2 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.7.1 && < 4.8 + copilot-core >= 4.8.2 && < 4.9 exposed-modules: diff --git a/copilot-interpreter/src/Copilot/Interpret/Eval.hs b/copilot-interpreter/src/Copilot/Interpret/Eval.hs index 462b5853e..9543806c9 100644 --- a/copilot-interpreter/src/Copilot/Interpret/Eval.hs +++ b/copilot-interpreter/src/Copilot/Interpret/Eval.hs @@ -19,7 +19,7 @@ module Copilot.Interpret.Eval import Copilot.Core (Expr (..), Field (..), Id, Name, Observer (..), Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..), Trigger (..), Type (..), UExpr (..), Value (..), - arrayElems, arrayUpdate, specObservers, + arrayElems, arrayUpdate, specObservers, specStreams, specTriggers, updateField) import Copilot.Interpret.Error (badUsage) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index 069d20f5d..4aacc9e2e 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,12 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + +2026-09-07 + * Version bump (4.8.1). (#760) + +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal index 2cfab8eb8..40ba65f2c 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.7.1 +version: 4.8.2 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.7.1 && < 4.8 - , copilot-interpreter >= 4.7.1 && < 4.8 - , copilot-theorem >= 4.7.1 && < 4.8 + , copilot-core >= 4.8.2 && < 4.9 + , copilot-interpreter >= 4.8.2 && < 4.9 + , copilot-theorem >= 4.8.2 && < 4.9 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 19b510a63..f84c75a48 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,13 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + * Add random stream generation module. (#766) + +2026-09-07 + * Version bump (4.8.1). (#760) + +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) * Add stream analysis module. (#726) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index 85b117f63..6e18aba84 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.7.1 +version: 4.8.2 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -41,7 +41,7 @@ library , containers >= 0.4 && < 0.9 , mtl >= 2.0 && < 2.4 , parsec >= 2.0 && < 3.2 - , copilot-language >= 4.7.1 && < 4.8 + , copilot-language >= 4.8.2 && < 4.9 exposed-modules: Copilot.Library.Analysis @@ -51,6 +51,7 @@ library , Copilot.Library.PTLTL , Copilot.Library.StateMachines , Copilot.Library.Statistics + , Copilot.Library.Random , Copilot.Library.RegExp , Copilot.Library.Utils , Copilot.Library.Voting diff --git a/copilot-libraries/src/Copilot/Library/Random.hs b/copilot-libraries/src/Copilot/Library/Random.hs new file mode 100644 index 000000000..d4828e12b --- /dev/null +++ b/copilot-libraries/src/Copilot/Library/Random.hs @@ -0,0 +1,145 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +-- | +-- Basic pseudo-random number generation. +-- +-- Information on performance of a selection of pseudo-random number generation +-- algorithms, including those implemented below, can be found at: +-- https://prng.di.unimi.it/ +-- +-- Important: these pseudo-random number generators are NOT cryptographically +-- secure generators. +module Copilot.Library.Random + ( randomW32 + , randomW64 + , boundedRandomIntegral + , proportionalRandomBool + , weightedRandomSelection + ) + where + +-- External imports +import Copilot.Language (Array, Stream, Typed, Word32, Word64, arrayElems, + constant, mod, mux, (!), (++), (.<<.), (.>>.), (.^.), + (<), (<=)) +import GHC.TypeLits (KnownNat, type (<=)) +import Prelude hiding (mod, (++), (<), (<=)) + +-- | Given two Word32 seeds, produce a pseudo-random stream of Word32 numbers, +-- which has a period of 2^32 - 1. Neither of the seeds should be zero, since +-- the underlying randomization algorithm maps zero to itself. +-- +-- This function uses an Xorshift+ algorithm. +randomW32 :: Word32 -> Word32 -> Stream Word32 +randomW32 0 _ = error "randomW32: seed cannot be zero." +randomW32 _ 0 = error "randomW32: seed cannot be zero." +randomW32 seed1 seed2 = s1 + s2 + + where + + s1 :: Stream Word32 + s1 = [seed1] ++ (xorshift32 s1) + + s2 :: Stream Word32 + s2 = [seed2] ++ (xorshift32 s2) + + -- This is a simple implementation of an Xorshift algorithm + xorshift32 :: Stream Word32 -> Stream Word32 + xorshift32 x1 = x4 -- Note: 0 maps to itself with this + where + x4 = x3 .^. (x3 .<<. (5 :: Stream Word32)) + x3 = x2 .^. (x2 .>>. (17 :: Stream Word32)) + x2 = x1 .^. (x1 .<<. (13 :: Stream Word32)) + +-- | Given two Word64 seeds, produce a pseudo-random stream of Word64 numbers, +-- which has a period of 2^128 - 1. Neither of the seeds should be zero, as +-- doing so will negatively impact the quality of the randomness. +-- +-- This function uses an Xorshiftrplus algorithm. +randomW64 :: Word64 -> Word64 -> Stream Word64 +randomW64 0 _ = error "randomW64: seed cannot be zero." +randomW64 _ 0 = error "randomW64: seed cannot be zero." +randomW64 seed1 seed2 = x + + where + + s0 :: Stream Word64 + s0 = [seed1] ++ s1 + + s1 :: Stream Word64 + s1 = [seed2] ++ (x + s1) + + x :: Stream Word64 + x = xorshiftr128plus s0 s1 + + xorshiftr128plus :: Stream Word64 -> Stream Word64 -> Stream Word64 + xorshiftr128plus x1 y = x4 + where + x4 = x3 .^. y + x3 = x2 .^. (x2 .>>. (17 :: Stream Word64)) + x2 = x1 .^. (x1 .<<. (23 :: Stream Word64)) + +-- | Given a stream of random integral numbers, a minimum value, and a maximum +-- value, produce a stream of random values greater than or equal to the +-- minimum and less than the maximum value, i.e., [@mN@, @mX@). +boundedRandomIntegral :: (Typed a, Integral a) + => Stream a -> a -> a -> Stream a +boundedRandomIntegral gen mN mX = (gen `mod` constant (mX - mN)) + constant mN + +-- | Given a stream of random integral numbers and two integers defining the +-- numerator and denominator of a rational probability, produce a boolean +-- stream that is randomly @True@ with the given probability. That is to say, +-- given a numerator @n@ and denominator @d@, then, over a sufficiently large +-- sample size, the resulting stream @s@ is @True@ @n@ out of @d@ times. +proportionalRandomBool :: (Typed a, Integral a) + => Stream a -> a -> a -> Stream Bool +proportionalRandomBool gen n d = (gen `mod` constant d) < constant n + +-- | Given a stream of random integral numbers, an array of values, and an +-- equal length array of weights, produce a stream of random values from the +-- given array with probabilities proportional to the given weights. +weightedRandomSelection :: forall a b s + . (KnownNat s, s <= MaxWord32, Typed a, Typed b, + Integral a, Bounded a) + => Stream a -> Array s b -> Array s a -> Stream b +weightedRandomSelection gen values weights + | overflow + = error "weightedRandomSelection: sum of weights overflows type" + + | signedType + = error "weightedRandomSelection: type of weights array must be unsigned" + + | otherwise + = constant values ! idx + + where + + -- Check if cumulativeSum decreases at any point. For unsigned integral + -- types, a decreasing element in this cumulative sequence corresponds to + -- an overflow. + overflow = or (zipWith (>) cumulativeSum (drop 1 cumulativeSum)) + + signedType = 0 > (minBound :: a) + + idx :: Stream Word32 + idx = countLeq cumulativeSum (gen `mod` constant totalSum) + + countLeq :: [a] -> Stream a -> Stream Word32 + countLeq xs v = sum [ mux (constant x <= v) 1 0 | x <- xs ] + -- ^ get number of elements in @xs@ less than or equal to @v@. + -- For non-decreasing @xs@, this is equal to the index of the first + -- element greater than @v@. + + cumulativeSum :: [a] + cumulativeSum = scanl1 (+) (arrayElems weights) + + totalSum :: a + totalSum = last cumulativeSum + +-- | Type-level representation of the upper bound on an unsigned 32-bit +-- integer. +type MaxWord32 = 4294967295 -- 2^32 - 1 diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index a8e6d3e12..bbe715c47 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,12 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + +2026-09-07 + * Version bump (4.8.1). (#760) + +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal index c40511c43..35c5c7d7c 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.7.1 +version: 4.8.2 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.7.1 && < 4.8 + copilot-core >= 4.8.2 && < 4.9 exposed-modules: diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 03facaf36..0207c5446 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,14 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + +2026-09-07 + * Version bump (4.8.1). (#760) + * Remove unnecessary extension. (#733) + +2026-07-07 + * Version bump (4.8). (#745) + * Extend range of versions of Kind2. (#734) + 2026-05-07 * Version bump (4.7.1). (#730) * Handle special Float values correctly for counterexamples. (#697) diff --git a/copilot-theorem/README.md b/copilot-theorem/README.md index 64cce8995..47a4b6081 100644 --- a/copilot-theorem/README.md +++ b/copilot-theorem/README.md @@ -31,7 +31,8 @@ properties on Copilot programs. It includes: * The *copilot-core* and *copilot-prettyprinter* Haskell libraries * The *Yices2* SMT-solver: `yices-smt2` must be in your `$PATH` * The *Z3* SMT-solver: `z3` must be in your `$PATH` -* The *Kind2* model checker: `kind2` must be in your `$PATH` +* The *Kind2* model checker (version 1.0 or newer): `kind2` must be in your + `$PATH` To build it, just install the Copilot library as described in the top-level README. @@ -87,7 +88,9 @@ configuration. The *Kind2* prover uses the model checker with the same name, from the University of Iowa. It translates the Copilot specification into a *modular transition system* (the Kind2 native format) and then calls the `kind2` -executable. +executable. Kind2 version 1.0 or newer is required: the native input format +and the command-line options used by this prover were introduced in Kind2 +1.0, and remain supported as of Kind2 3.0. It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prover :: Options -> Prover` where the `Options` type is defined as @@ -95,7 +98,7 @@ It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prov ```haskell data Options = Options { bmcMax :: Int } ``` -and where `bmcMax` corresponds to the `--bmc_max` option of *kind2* and is +and where `bmcMax` corresponds to the `--unroll_max` option of *kind2* and is equivalent to the `maxK` option of the K-Induction prover. Its default value is 0, which stands for infinity. @@ -335,11 +338,16 @@ process. The transition system obtained by the `TransSys.Translate` module is perfectly consistent. However, it can't be directly translated into the *Kind2 native -file format*. Indeed, it is natural to bind each node to a predicate but the -Kind2 file format requires that each predicate only uses previously defined -predicates. However, some nodes in our transition system could be mutually -recursive. Therefore, the goal of the `removeCycles :: Spec -> Spec` function, -defined in `TransSys.Transform`, is to remove such dependency cycles. +file format*. The native input format of Kind2 (version 1.0 and newer) does +not support predicate calls inside the initial state and transition relation +predicates of a node, so the modular structure of the transition system cannot +be expressed directly in it. Therefore, the system is first turned into an +equivalent non-modular transition system with only one node by the +`inline :: Spec -> Spec` function, defined in `TransSys.Transform`: +```haskell +inline :: Spec -> Spec +inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec +``` This function relies on the `mergeNodes :: [NodeId] -> Spec -> Spec` function, whose signature is self-explicit. The latter solves name conflicts by using the @@ -516,10 +524,14 @@ in the Kind2 SMT solver. #### Displaying counterexamples Counterexamples are not displayed with the Kind2 prover because Kind2 doesn't -support XML output of counterexamples. If the last feature is provided, it -should be easy to implement displaying of counterexamples in *copilot-theorem*. -For this, we recommend keeping some information about *observers* in -`TransSys.Spec` and to add one variable per observer in the Kind2 output file. +support the output of counterexamples for systems expressed in its native input +format (the counterexample printing functions in Kind2's +[`src/inputSystem.ml`](https://github.com/kind2-mc/kind2/blob/v3.0.0/src/inputSystem.ml) +fail with an internal error for native input). If Kind2 adds this feature, it +should be easy to implement displaying of counterexamples in +*copilot-theorem*. For this, we recommend keeping some information about +*observers* in `TransSys.Spec` and to add one variable per observer in the +Kind2 output file. #### Bad handling of non-linear operators and external functions @@ -569,14 +581,14 @@ architecture of Kind2. It is true that the code of `TransSys` is quite complex. In fact, it would be really straightforward to produce a flattened transition system and then a -Kind2 file with just a single *top* predicate. In fact, It would be as easy as +Kind2 file with just a single *top* node. In fact, It would be as easy as producing an *IL* specification. To be honest, I'm not sure producing a modular *Kind2* output is worth the complexity added. It's especially true at the time I write this in the sense that: -* Each predicate introduced is used only one time (which is true because +* Each node introduced is used only one time (which is true because Copilot doesn't handle functions or parameterized streams like Lustre does and everything is inlined during the reification process). * A similar form of structure could be obtained from a flattened Kind2 native diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index cd9d2e00e..da29f566a 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.7.1 +version : 4.8.2 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -51,6 +51,7 @@ library , containers >= 0.4 && < 0.9 , data-default >= 0.7 && < 0.9 , directory >= 1.3 && < 1.4 + , extra >= 1.7 && < 1.9 , fp-ieee >= 0.1 && < 0.2 , libBF >= 0.6.2 && < 0.7 , mtl >= 2.0 && < 2.4 @@ -60,11 +61,10 @@ library , process >= 1.6 && < 1.7 , random >= 1.1 && < 1.4 , transformers >= 0.5 && < 0.7 - , xml >= 1.3 && < 1.4 , what4 >= 1.3 && < 1.8 - , copilot-core >= 4.7.1 && < 4.8 - , copilot-prettyprinter >= 4.7.1 && < 4.8 + , copilot-core >= 4.8.2 && < 4.9 + , copilot-prettyprinter >= 4.8.2 && < 4.9 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs index e69cda8d0..efd493a6d 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs @@ -1,27 +1,54 @@ {-# LANGUAGE Safe #-} --- | Abstract syntax tree of Kind2 files. +-- | Abstract syntax tree of Kind2 native input files. +-- +-- This represents the native transition system input format supported by +-- Kind2 1.0 and newer (@--input_format native@), in which a file is a +-- sequence of @define-node@ forms, each declaring a state transition system +-- by means of an initial state predicate and a transition relation predicate. +-- The last node defined in a file is the top system analyzed by Kind2, and +-- the properties to check are attached to it. +-- +-- The native input format is largely undocumented, and Kind2's user +-- documentation only covers its Lustre frontend. The best available +-- references for the native format are the parser in the Kind2 sources +-- ([nativeInput.ml] +-- (https://github.com/kind2-mc/kind2/blob/v3.0.0/src/nativeInput.ml)), +-- which includes a sketch of the grammar in a comment near the end of the +-- file) and the example file +-- [two_counters.kind2] +-- (https://github.com/kind2-mc/kind2/blob/develop/examples/two_counters.kind2). module Copilot.Theorem.Kind2.AST where --- | A file is a sequence of predicates and propositions. +-- | A file is a sequence of node definitions, together with a distinguished +-- top node and a series of propositions about the top node. +-- +-- Kind2 analyzes the last node defined in a file as the top system, so the +-- top node is always printed after all the other nodes. data File = File - { filePreds :: [PredDef] - , fileProps :: [Prop] } + { fileNodes :: [Node] -- ^ Nodes other than the top node, in dependency + -- order (a node may only refer to nodes defined + -- before it). + , fileTopNode :: Node -- ^ The top node, which the propositions are + -- attached to. + , fileProps :: [Prop] -- ^ Propositions about the top node. + } -- | A proposition is defined by a term. data Prop = Prop { propName :: String , propTerm :: Term } --- | A predicate definition. -data PredDef = PredDef - { predId :: String -- ^ Identifier for the predicate. - , predStateVars :: [StateVarDef] -- ^ Variables identifying the states in the - -- underlying state transition system. - , predInit :: Term -- ^ Predicate that holds for initial +-- | A node definition. +data Node = Node + { nodeId :: String -- ^ Identifier for the node. + , nodeStateVars :: [StateVarDef] -- ^ Variables identifying the states in + -- the underlying state transition system. + , nodeInit :: Term -- ^ Predicate that holds for initial -- states. - , predTrans :: Term -- ^ Predicate that holds for two states, if - -- there is state transition between them. + , nodeTrans :: Term -- ^ Predicate that holds for two states, + -- if there is a state transition between + -- them. } -- | A definition of a state variable. diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs index f80b8170b..8a1d29c28 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs @@ -4,66 +4,97 @@ -- | Parse output of Kind2. module Copilot.Theorem.Kind2.Output (parseOutput) where -import Text.XML.Light hiding (findChild) -import Copilot.Theorem.Prove as P -import Data.Maybe (fromJust) +import Data.List.Extra (isInfixOf, splitOn, stripInfix, trim) +import Data.Maybe (mapMaybe) + +import Copilot.Theorem.Prove as P import qualified Copilot.Core as C import qualified Copilot.Theorem.Misc.Error as Err -simpleName s = QName s Nothing Nothing - -- | Parse output of Kind2. +-- +-- The output is expected to be in XML format, as produced by Kind2's @-xml@ +-- flag and documented at +-- . +-- Note that this function does not parse the output as XML: when given a +-- system in the native transition system format, Kind2 produces output that +-- is not always well-formed XML (e.g., counterexamples to invariant +-- properties cannot be printed for systems in that format -- the +-- counterexample printing functions in Kind2's @src/inputSystem.ml@ fail with +-- an internal error for native input -- and Kind2 reports the error in the +-- middle of the XML output). Instead, this function looks for the +-- @\@ tag for the given property and extracts the answers in the +-- @\@ tags it contains. parseOutput :: String -- ^ Property whose validity is being checked. -> C.Prop -- ^ The property's quantifier. -> String -- ^ XML output of Kind2 -> P.Output -parseOutput propId propQuantifier xml = fromJust $ do - root <- parseXMLDoc xml - case findAnswer . findPropTag $ root of - "valid" -> case propQuantifier of - -- We encode a universally quantified property P as - -- ∀x.P(x) in Kind2, so the original property is valid - -- iff the Kind2 property is valid. - C.Forall {} -> return (Output Valid []) - -- We encode an existentially quantified property P as - -- ¬(∀x.¬(P(x))) in Kind2, so the original property is - -- invalid iff the Kind2 property is valid. - C.Exists {} -> return (Output Invalid []) - "falsifiable" -> case propQuantifier of - -- We encode a universally quantified property P as - -- ∀x.P(x) in Kind2, so the original property is invalid - -- iff the Kind2 property is invalid. - C.Forall {} -> return (Output Invalid []) - -- We encode an existentially quantified property P as - -- ¬(∀x.¬(P(x))) in Kind2, so the original property is - -- valid iff the Kind2 property is invalid. - C.Exists {} -> return (Output Valid []) - s -> err $ "Unrecognized status : " ++ s +parseOutput propId propQuantifier xml + | "valid" `elem` answers = quantified (Output Valid []) + (Output Invalid []) + | "falsifiable" `elem` answers = quantified (Output Invalid []) + (Output Valid []) + | "unknown" `elem` answers = Output Unknown [] + | null answers = err $ "Answer for property " ++ propId ++ " not found" + | otherwise = err $ "Unrecognized status : " ++ unwords answers where - searchForRuntimeError = undefined + -- Pick an output based on the quantifier of the property. The first + -- argument is returned when the property Kind2 was asked about is valid, + -- and the second one when it is invalid. + -- + -- We encode a universally quantified property P as ∀x.P(x) in Kind2, so + -- the original property is valid iff the Kind2 property is valid. + -- + -- We encode an existentially quantified property P as ¬(∀x.¬(P(x))) in + -- Kind2, so the original property is valid iff the Kind2 property is + -- invalid. + quantified ifValid ifInvalid = case propQuantifier of + C.Forall {} -> ifValid + C.Exists {} -> ifInvalid + + -- All the answers reported for the property, in the order in which they + -- appear in the output. A conclusive answer (valid or falsifiable), if + -- any, takes precedence over inconclusive (unknown) ones, which Kind2 may + -- also report when the analysis terminates without an answer for all + -- properties. + answers = mapMaybe answerText + $ filter isRightProperty + $ propertyElems xml - findPropTag root = - let rightElement elt = - qName (elName elt) == "Property" - && lookupAttr (simpleName "name") (elAttribs elt) - == Just propId - in case filterChildren rightElement root of - tag : _ -> tag - _ -> err $ "Tag for property " ++ propId ++ " not found" + -- Substrings of the output following a @\ - case onlyText (elContent answTag) of - answ : _ -> cdData answ - _ -> err "Invalid 'Answer' attribute" - _ -> err "Attribute 'Answer' not found" + -- True if the given property element has the name of the property this + -- function looks for. + isRightProperty elem' = + ("name=\"" ++ escapeAttr propId ++ "\"") `isInfixOf` openingTag + where + openingTag = takeWhile (/= '>') elem' + + -- The contents of the first @\@ tag in the given element, if + -- any. + answerText elem' = do + (_, rest) <- stripInfix "" rest + let answer = trim $ takeWhile (/= '<') rest' + if null answer then Nothing else Just answer err :: forall a . String -> a err msg = Err.fatal $ "Parse error while reading the Kind2 XML output : \n" ++ msg ++ "\n\n" ++ xml + +-- | Escape a string for use as an XML attribute value. +escapeAttr :: String -> String +escapeAttr = concatMap escapeChar + where + escapeChar '&' = "&" + escapeChar '<' = "<" + escapeChar '>' = ">" + escapeChar '"' = """ + escapeChar c = [c] diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs index 6851d46fa..92d158a1c 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs @@ -1,6 +1,8 @@ {-# LANGUAGE Safe #-} --- | Pretty print a Kind2 file defining predicates and propositions. +-- | Pretty print a Kind2 file defining nodes and propositions, in the native +-- transition system input format supported by Kind2 1.0 and newer (see +-- "Copilot.Theorem.Kind2.AST" for pointers to references on the format). module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where import Copilot.Theorem.Misc.SExpr @@ -15,6 +17,14 @@ type SSExpr = SExpr String -- | Reserved keyword prime. kwPrime = "prime" +-- | Dummy position attached to the properties of the file. +-- +-- Kind2 requires a position (in the format @file:row-col@) for properties +-- declared with the @:user@ source annotation, and reports that position back +-- in its output. +propPosition :: String +propPosition = "copilot:1-1" + -- | Pretty print a Kind2 file. prettyPrint :: File -> String prettyPrint = @@ -29,30 +39,41 @@ shouldIndent (List [Atom a, Atom _]) = a `notElem` [kwPrime] shouldIndent _ = True -- | Convert a file into a sequence of expressions. +-- +-- The top node is printed last, since Kind2 analyzes the last node of the +-- file as the top system. The properties of the file are attached to it. ppFile :: File -> [SSExpr] -ppFile (File preds props) = map ppPredDef preds ++ ppProps props +ppFile (File nodes top props) = + map (`ppNode` []) nodes ++ [ppNode top (ppProps props)] --- | Convert a sequence of propositions into command to check each of them. +-- | Convert a sequence of propositions into a props field. ppProps :: [Prop] -> [SSExpr] -ppProps ps = [ node "check-prop" [ list $ map ppProp ps ] ] +ppProps [] = [] +ppProps ps = [ node "props" [ list $ map ppProp ps ] ] -- | Convert a proposition into an expression. ppProp :: Prop -> SSExpr -ppProp (Prop n t) = list [atom n, ppTerm t] +ppProp (Prop n t) = list [atom n, ppTerm t, atom ":user", atom propPosition] --- | Convert a predicate into an expression. -ppPredDef :: PredDef -> SSExpr -ppPredDef pd = - list [ atom "define-pred" - , atom (predId pd) - , list . map ppStateVarDef . predStateVars $ pd - , node "init" [ppTerm $ predInit pd] - , node "trans" [ppTerm $ predTrans pd] ] +-- | Convert a node, together with optional extra fields, into an expression. +ppNode :: Node -> [SSExpr] -> SSExpr +ppNode n extraFields = + list $ [ atom "define-node" + , atom (nodeId n) + , list . map ppStateVarDef . nodeStateVars $ n + , node "init" [ppTerm $ nodeInit n] + , node "trans" [ppTerm $ nodeTrans n] ] + ++ extraFields -- | Convert a state variable definition into an expression. ppStateVarDef :: StateVarDef -> SSExpr ppStateVarDef svd = - list [atom (varId svd), ppType (varType svd)] + list $ [atom (varId svd), ppType (varType svd)] + ++ map ppStateVarFlag (varFlags svd) + +-- | Convert a state variable option into an expression. +ppStateVarFlag :: StateVarFlag -> SSExpr +ppStateVarFlag FConst = atom ":const" -- | Convert a type into an expression. ppType :: Type -> SSExpr diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs index 4bb52322e..a79ede4f6 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs @@ -28,7 +28,8 @@ import qualified Copilot.Theorem.TransSys as TS -- | Options for Kind2 data Options = Options { bmcMax :: Int -- ^ Upper bound on the number of unrolling that base and - -- step will perform. A value of 0 means /unlimited/. + -- step will perform (passed to Kind2 via its + -- @--unroll_max@ option). A value of 0 means /unlimited/. } -- | Default options with unlimited unrolling for base and step. @@ -41,7 +42,10 @@ data ProverST = ProverST -- | A prover backend based on Kind2. -- --- The executable @kind2@ must exist and its location be in the @PATH@. +-- The executable @kind2@ must exist and its location be in the @PATH@. Kind2 +-- version 1.0 or newer is required: the native input format and the +-- command-line options this prover uses were introduced in Kind2 1.0, and +-- remain supported as of Kind2 3.0. kind2Prover :: Options -> Prover kind2Prover opts = Prover { proverName = "Kind2" @@ -50,24 +54,22 @@ kind2Prover opts = Prover , closeProver = const $ return () } kind2Prog = "kind2" -kind2BaseOptions = ["--input-format", "native", "-xml"] +kind2BaseOptions = ["--input_format", "native", "-xml"] askKind2 :: ProverST -> [PropId] -> [PropId] -> IO Output askKind2 (ProverST opts spec) assumptions toCheck = do - let kind2Input = prettyPrint . toKind2 Inlined assumptions toCheck $ spec + let kind2Input = prettyPrint . toKind2 assumptions toCheck $ spec (tempName, tempHandle) <- openTempFile "." "out" "kind" hPutStr tempHandle kind2Input hClose tempHandle let kind2Options = - kind2BaseOptions ++ ["--bmc_max", show $ bmcMax opts, tempName] + kind2BaseOptions ++ ["--unroll_max", show $ bmcMax opts, tempName] (_, output, _) <- readProcessWithExitCode kind2Prog kind2Options "" - putStrLn kind2Input - removeFile tempName let propId = head toCheck diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs index 123f6ed64..d59aaae24 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs @@ -1,68 +1,44 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE Safe #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE Safe #-} -- | Convert modular transition systems ('TransSys') into Kind2 file -- specifications. module Copilot.Theorem.Kind2.Translate ( toKind2 - , Style (..) ) where import Copilot.Theorem.TransSys import qualified Copilot.Theorem.Kind2.AST as K -import Control.Exception.Base (assert) - import Data.Function (on) import Data.Maybe (fromJust) -import Data.List (sort, sortBy) -import Data.Map (Map, (!)) +import Data.List (partition, sort, sortBy) +import Data.Map ((!)) import qualified Data.Map as Map import qualified Data.Bimap as Bimap --- The following properties MUST hold for the given transition system : --- * Nodes are sorted by topological order --- * Nodes are `completed`, which means the dependency graph is transitive --- and each node imports all the local variables of its dependencies --- - -type DepGraph = Map NodeId [NodeId] - --- | Style of the Kind2 files produced: modular (with multiple separate nodes), --- or all inlined (with only one node). --- --- In the modular style, the graph is simplified to remove cycles by collapsing --- all nodes participating in a strongly connected components. --- --- In the inlined style, the structure of the modular transition system is --- discarded and the graph is first turned into a /non-modular transition/ --- /system/ with only one node, which can be then converted into a Kind2 file. -data Style = Inlined | Modular - -- | Produce a Kind2 file that checks the properties specified. -toKind2 :: Style -- ^ Style of the file (modular or inlined). - -> [PropId] -- ^ Assumptions +toKind2 :: [PropId] -- ^ Assumptions -> [PropId] -- ^ Properties to be checked -> TransSys -- ^ Modular transition system holding the system spec -> K.File -toKind2 style assumptions checkedProps spec = - addAssumptions spec assumptions - $ trSpec (complete spec') predCallsGraph assumptions checkedProps +toKind2 assumptions checkedProps spec = + addAssumptions spec' assumptions $ trSpec spec' checkedProps where - predCallsGraph = specDependenciesGraph spec' - spec' = case style of - Inlined -> inline spec - Modular -> removeCycles spec + spec' = inline spec -trSpec :: TransSys -> DepGraph -> [PropId] -> [PropId] -> K.File -trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props +trSpec :: TransSys -> [PropId] -> K.File +trSpec spec checkedProps = K.File otherNodes topNode props where - preds = map (trNode spec predCallsGraph) (specNodes spec) + (topNode, otherNodes) = + case partition ((== specTopNodeId spec) . K.nodeId) nodes of + ([top], others) -> (top, others) + _ -> error $ "Kind2.Translate: top node " + ++ specTopNodeId spec ++ " not found" + nodes = map (trNode spec) (specNodes spec) props = map trProp $ filter ((`elem` checkedProps) . fst) $ Map.toList $ Map.map fst $ specProps spec @@ -70,37 +46,30 @@ trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props trProp :: (PropId, ExtVar) -> K.Prop trProp (pId, var) = K.Prop pId (trVar . extVarLocalPart $ var) -trNode :: TransSys -> DepGraph -> Node -> K.PredDef -trNode spec predCallsGraph node = - K.PredDef { K.predId, K.predStateVars, K.predInit, K.predTrans } - where - predId = nodeId node - predStateVars = gatherPredStateVars spec node - predInit = mkConj $ initLocals node - ++ map (trExpr False) (nodeConstrs node) - ++ predCalls True spec predCallsGraph node - predTrans = mkConj $ transLocals node - ++ map (trExpr True) (nodeConstrs node) - ++ predCalls False spec predCallsGraph node - +trNode :: TransSys -> Node -> K.Node +trNode spec node = K.Node + { K.nodeId = nodeId node + , K.nodeStateVars = gatherPredStateVars spec node + , K.nodeInit = mkConj $ initLocals node + ++ map (trExpr False) (nodeConstrs node) + , K.nodeTrans = mkConj $ transLocals node + ++ map (trExpr True) (nodeConstrs node) + } + +-- | Add the assumptions to the top node of the file by conjoining the +-- corresponding property variables to its initial state and transition +-- relation predicates. addAssumptions :: TransSys -> [PropId] -> K.File -> K.File -addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) = - K.File (changeTail aux filePreds) fileProps +addAssumptions spec assumptions file = + file { K.fileTopNode = aux (K.fileTopNode file) } where - changeTail f (reverse -> l) = case l of - [] -> error "impossible" - x : xs -> reverse $ f x : xs - - aux pred = - let init' = mkConj ( K.predInit pred : map K.StateVar vars ) - trans' = mkConj ( K.predTrans pred : map K.PrimedStateVar vars ) - in pred { K.predInit = init', K.predTrans = trans' } + aux node = + let init' = mkConj ( K.nodeInit node : map K.StateVar vars ) + trans' = mkConj ( K.nodeTrans node : map K.PrimedStateVar vars ) + in node { K.nodeInit = init', K.nodeTrans = trans' } - vars = - let bindings = nodeImportedVars (specTopNode spec) - toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec - toTopVar (ExtVar nId v) = assert (nId == specTopNodeId spec) v - in map (varName . toTopVar . toExtVar) assumptions + toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec + vars = map (varName . extVarLocalPart . toExtVar) assumptions -- The ordering really matters here because the variables -- have to be given in this order in a pred call @@ -169,39 +138,6 @@ transLocals node = Expr e -> [mkEquality (trPrimedVar v) (trExpr True e)] Constrs cs -> map (trExpr True) cs -predCalls :: Bool -> TransSys -> DepGraph -> Node -> [K.Term] -predCalls isInitCall spec predCallsGraph node = - map mkCall toCall - where - nid = nodeId node - toCall = predCallsGraph ! nid - nodesMap = Map.fromList [(nodeId n, n) | n <- specNodes spec] - - nodeLocals n = - map (ExtVar n) . sort . Map.keys - . nodeLocalVars $ (nodesMap ! n) - - mkCall callee - | isInitCall = - K.PredApp callee K.Init (argsSeq trVar) - | otherwise = - K.PredApp callee K.Trans (argsSeq trVar ++ argsSeq trPrimedVar) - where - - calleeLocals = nodeLocals callee - calleeImported = - (concatMap nodeLocals . sort . nodeDependencies) $ nodesMap ! callee - - localAlias trVarF ev = - case Bimap.lookupR ev $ nodeImportedVars node of - Nothing -> error $ - "This spec is not complete : " - ++ show ev ++ " should be imported in " ++ nid - Just v -> trVarF v - - argsSeq trVarF = - map (localAlias trVarF) (calleeLocals ++ calleeImported) - trExpr :: Bool -> Expr t -> K.Term trExpr primed = tr where diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs index cef4829ee..00edf8744 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs @@ -2,7 +2,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index a2b4dd530..c69ccd708 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,12 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + +2026-09-07 + * Version bump (4.8.1). (#760) + +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index 339892ec9..bcf1061bf 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.7.1 +Version: 4.8.2 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.7.1 && < 4.8, - copilot-core >= 4.7.1 && < 4.8, - copilot-theorem >= 4.7.1 && < 4.8, + copilot-c99 >= 4.8.2 && < 4.9, + copilot-core >= 4.8.2 && < 4.9, + copilot-theorem >= 4.8.2 && < 4.9, crucible >= 0.7.1 && < 0.8, crucible-llvm >= 0.7 && < 0.8, crux >= 0.7.1 && < 0.8, @@ -80,10 +80,10 @@ library copilot-verifier-examples hs-source-dirs: examples build-depends: case-insensitive, - copilot >= 4.7.1 && < 4.8, - copilot-language >= 4.7.1 && < 4.8, - copilot-libraries >= 4.7.1 && < 4.8, - copilot-prettyprinter >= 4.7.1 && < 4.8, + copilot >= 4.8.2 && < 4.9, + copilot-language >= 4.8.2 && < 4.9, + copilot-libraries >= 4.8.2 && < 4.9, + copilot-prettyprinter >= 4.8.2 && < 4.9, copilot-verifier exposed-modules: Copilot.Verifier.Examples diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 0735d51ab..b578bedb9 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,14 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + +2026-09-07 + * Version bump (4.8.1). (#760) + * Fix inconsistent version bounds for `copilot` in Cabal file. (#749) + * Relax version constraints on `ogma-extra`. (#757) + +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal index 5e8735ea4..34d2289bd 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.7.1 +version: 4.8.2 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.13, + ogma-extra >= 1.6.0 && < 1.17, text >= 1.2.3.1 && < 2.2, websockets >= 0.12.7 && < 0.14, - copilot >= 4.7.1 && < 4.8, - copilot-core >= 4.7.1 && < 4.8, - copilot-interpreter >= 4.7.1 && < 4.8, - copilot-language >= 4.7.1 && < 4.8 + copilot >= 4.8.2 && < 4.9, + copilot-core >= 4.8.2 && < 4.9, + copilot-interpreter >= 4.8.2 && < 4.9, + copilot-language >= 4.8.2 && < 4.9 exposed-modules: @@ -121,7 +121,7 @@ executable tikz-example build-depends: base >= 4.9 && < 5, - copilot >= 4.7 && < 4.8, + copilot >= 4.8.2 && < 4.9, copilot-visualizer if flag(examples) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index f58dd30e6..8b691705e 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,17 @@ +2026-11-07 + * Version bump (4.8.2). (#792) + * Adjust Travis CI script to flag presence of tabs as an error. (#774) + * Adjust Travis CI script to flag trailing space as an error. (#777) + * Update README to correct typos and improve readability. (#779) + * Replace Travis CI with Github Actions. (#790) + +2026-09-07 + * Version bump (4.8.1). (#760) + * Disable secure mode in Cabal in Travis CI. (#753) + +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) diff --git a/copilot/README.md b/copilot/README.md index 893d6a933..63a2459ef 100644 --- a/copilot/README.md +++ b/copilot/README.md @@ -2,12 +2,12 @@ # Copilot -[![Build Status](https://api.travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot) +[![Build Status](https://github.com/Copilot-Language/copilot/actions/workflows/build.yml/badge.svg?branch=master)](https://github.com/Copilot-Language/copilot/actions/workflows/build.yml) [![Version on Hackage](https://img.shields.io/hackage/v/copilot.svg)](https://hackage.haskell.org/package/copilot) Copilot is a runtime verification framework for hard real-time systems. Programs can be interpreted for testing, or translated into C99 code to be -incorporated in a project or standalone application. The C99 code generated +incorporated into a project or standalone application. The C99 code generated is constant in memory and time, making it suitable for systems with hard real-time requirements. @@ -26,7 +26,7 @@ real-time requirements. - Produce hard real-time C99 runtime monitors that run in constant memory and time. -- Catch errors in specifications early using expressive static type system. +- Catch errors in specifications early using an expressive static type system. - Prove properties about specifications using theorem proving extensions. @@ -98,7 +98,7 @@ ghci> ghci> Leaving GHCi. ### Other Linux distributions On other Linux distributions or older Debian-based distributions, to use -Copilot you must install a Haskell compiler (GHC) and the package manager +Copilot, you must install a Haskell compiler (GHC) and the package manager Cabal. We currently support all versions of GHC from 8.6.5 to modern versions (9.10 as of this writing). You can install the toolchain using [ghcup](https://www.haskell.org/ghcup/) or, if you are on Debian/Ubuntu, @@ -129,7 +129,7 @@ ghci> ghci> Leaving GHCi. ## Mac installation [(Back to top)](#table-of-contents) -To use Copilot you must have a Haskell compiler (GHC) and the package manager +To use Copilot, you must have a Haskell compiler (GHC) and the package manager Cabal. We currently support all versions of GHC from 8.6.5 to modern versions (9.6 as of this writing). You can install the toolchain using [ghcup](https://www.haskell.org/ghcup/), as well as with Homebrew: @@ -162,7 +162,7 @@ ghci> ghci> Leaving GHCi. Feel free to open an issue if you are unable to install Copilot following these instructions. -There is a TravisCI file at the root of the repository that may help with +There is a Travis CI file at the root of the repository that may help with troubleshooting the installation. Our issues often include comments with Dockerfiles listing the steps necessary to install Copilot from scratch. @@ -176,8 +176,9 @@ of the main repository. ```haskell -- This example implements a simple home heating system. The system heats --- when the temperature gets too low, and stops when it is high enough. It read --- temperature as a byte (range -50C to 100C) and translates this to Celsius. +-- when the temperature gets too low, and stops when it is high enough. It +-- reads the temperature as a byte (range -50C to 100C) and translates it to +-- Celsius. module Heater where @@ -238,13 +239,13 @@ does not constitute any form of endorsement._ built using NASA's Core Flight System or the Robot Operating System (ROS 2). - [arduino-copilot](https://hackage.haskell.org/package/arduino-copilot) - facilitates building copilot applications that run on Arduino. + facilitates building Copilot applications that run on Arduino. - [sketch-frp-copilot](https://hackage.haskell.org/package/sketch-frp-copilot) extends Copilot with an FRP-like interface. - [zephyr-copilot](https://hackage.haskell.org/package/zephyr-copilot) - facilitates building copilot applications that run on boards supported by the + facilitates building Copilot applications that run on boards supported by the Zephyr project. # Documentation @@ -390,5 +391,5 @@ https://github.com/Copilot-Language/copilot/graphs/contributors We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National Institute of Aerospace, which partially supported this work. -Additionally NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported +Additionally, NASA Langley contracts 80LARC17C0004 and NNL09AA00A supported further development of Copilot. diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index ace61023d..00a495e3f 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.7.1 +version: 4.8.2 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.7.1 && < 4.8 - , copilot-theorem >= 4.7.1 && < 4.8 - , copilot-language >= 4.7.1 && < 4.8 - , copilot-libraries >= 4.7.1 && < 4.8 - , copilot-c99 >= 4.7.1 && < 4.8 - , copilot-prettyprinter >= 4.7.1 && < 4.8 + , copilot-core >= 4.8.2 && < 4.9 + , copilot-theorem >= 4.8.2 && < 4.9 + , copilot-language >= 4.8.2 && < 4.9 + , copilot-libraries >= 4.8.2 && < 4.9 + , copilot-c99 >= 4.8.2 && < 4.9 + , copilot-prettyprinter >= 4.8.2 && < 4.9 exposed-modules: Language.Copilot, Language.Copilot.Main