diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index 63ea6878..1145b7a8 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +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) diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal index ffaadaca..2cff39b3 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 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 && < 4.9 + , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 74c6c1dd..ba43b631 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +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 d9802bd4..d3defea3 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 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 && < 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 4a019a35..e37d6058 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +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 ee463977..541cad1e 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 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index 53984488..d97f4575 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +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 0303bf17..255d0400 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 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 && < 4.9 exposed-modules: diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index 069d20f5..b162f316 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +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 2cfab8eb..ca5232a8 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 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 && < 4.9 + , copilot-interpreter >= 4.8 && < 4.9 + , copilot-theorem >= 4.8 && < 4.9 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index 19b510a6..b0928604 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +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 85b117f6..dd96c07d 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 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 && < 4.9 exposed-modules: Copilot.Library.Analysis diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index a8e6d3e1..7ffd6c90 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +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 c40511c4..393ae9b3 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 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 && < 4.9 exposed-modules: diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 03facaf3..ec8dafd5 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,7 @@ +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 64cce899..47a4b608 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 cd9d2e00..28127ebd 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 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 && < 4.9 + , copilot-prettyprinter >= 4.8 && < 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 e69cda8d..efd493a6 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 f80b8170..8a1d29c2 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 6851d46f..92d158a1 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 4bb52322..a79ede4f 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 123f6ed6..d59aaae2 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-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index a2b4dd53..81d2534f 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,6 @@ +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 339892ec..aed3a0f1 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 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 && < 4.9, + copilot-core >= 4.8 && < 4.9, + copilot-theorem >= 4.8 && < 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 && < 4.9, + copilot-language >= 4.8 && < 4.9, + copilot-libraries >= 4.8 && < 4.9, + copilot-prettyprinter >= 4.8 && < 4.9, copilot-verifier exposed-modules: Copilot.Verifier.Examples diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 0735d51a..e4a74c50 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,6 @@ +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 5e8735ea..1bd88608 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 synopsis: Visualizer for Copilot. description: Visualizer for Copilot. @@ -65,10 +65,10 @@ library 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 && < 4.9, + copilot-core >= 4.8 && < 4.9, + copilot-interpreter >= 4.8 && < 4.9, + copilot-language >= 4.8 && < 4.9 exposed-modules: diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index f58dd30e..f46d51f9 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2026-07-07 + * Version bump (4.8). (#745) + 2026-05-07 * Version bump (4.7.1). (#730) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index ace61023..85dd95ab 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.7.1 +version: 4.8 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 && < 4.9 + , copilot-theorem >= 4.8 && < 4.9 + , copilot-language >= 4.8 && < 4.9 + , copilot-libraries >= 4.8 && < 4.9 + , copilot-c99 >= 4.8 && < 4.9 + , copilot-prettyprinter >= 4.8 && < 4.9 exposed-modules: Language.Copilot, Language.Copilot.Main