From 6e8bb30d1e307707765e5a19f9836065d22dd8c9 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 9 Jun 2026 13:53:43 -0500 Subject: [PATCH 1/3] copilot-theorem: Extend range of versions of Kind2. Refs #734. In order to keep Copilot effectively working in the current software ecosystem, we need to extend the versions of dependencies that Copilot can be installed with. kind2 has seen release 2.3.0, but copilot-theorem requires kind2 0.7.2. This commit updates the copilot-theorem Kind2 native-format backend to produce output targeting the latest release of Kind2 (v2.3). --- copilot-theorem/README.md | 61 ++----- copilot-theorem/copilot-theorem.cabal | 1 - .../src/Copilot/Theorem/Kind2/AST.hs | 48 ++--- .../src/Copilot/Theorem/Kind2/Output.hs | 140 ++++++++++----- .../src/Copilot/Theorem/Kind2/PrettyPrint.hs | 54 ++++-- .../src/Copilot/Theorem/Kind2/Prover.hs | 16 +- .../src/Copilot/Theorem/Kind2/Translate.hs | 166 +++++------------- .../src/Copilot/Theorem/TransSys/Transform.hs | 103 +---------- 8 files changed, 228 insertions(+), 361 deletions(-) diff --git a/copilot-theorem/README.md b/copilot-theorem/README.md index 64cce8995..4c5cb6645 100644 --- a/copilot-theorem/README.md +++ b/copilot-theorem/README.md @@ -95,7 +95,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,51 +335,25 @@ 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 2.x 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` funtion, +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 `Misc.Renaming` monad. Some code complexity has been added so variable names remain as clear as possible after merging two nodes. -The function `removeCycles` computes the strongly connected components of the -dependency graph and merge each one into a single node. The complexity of this -process is high in the worst case (the square of the total size of the system -times the size of the biggest node) but good in practice as few nodes are to be -merged in most practical cases. - -After the cycles have been removed, it is useful to apply another -transformation which makes the translation from `TransSys.Spec` to `Kind2.AST` -easier. This transformation is implemented in the `complete` function. In a -nutshell, it transforms a system such that: - -* If a node depends on another, it imports *all* its variables. -* The dependency graph is transitive, that is if *A* depends of *B* which - depends of *C* then *A* depends on *C*. - After this transformation, the translation from `TransSys.Spec` to `Kind2.AST` is almost only a matter of syntax. -###### Bonus track - -Thanks to the `mergeNodes` function, we can get for free the function - -```haskell -inline :: Spec -> Spec -inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec -``` - -which discards all the structure of a *modular transition system* and turns it -into a *non-modular transition system* with only one node. In fact, when -translating a Copilot specification to a Kind2 file, two styles are available: -the `Kind2.toKind2` function takes a `Style` argument which can take the value -`Inlined` or `Modular`. The only difference is that in the first case, a call -to `removeCycles` is replaced by a call to `inline`. - ### Limitations of copilot-theorem Now, we will discuss some limitations of the *copilot-theorem* tool. These @@ -516,10 +490,11 @@ 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. 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 +544,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..369ae7b3a 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -60,7 +60,6 @@ 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 diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs index e69cda8d0..deab5bd8f 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs @@ -1,11 +1,19 @@ {-# 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 2.x (@--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. 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 series of +-- propositions about the last (top) node. data File = File - { filePreds :: [PredDef] + { fileNodes :: [Node] , fileProps :: [Prop] } -- | A proposition is defined by a term. @@ -13,23 +21,18 @@ 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. -data StateVarDef = StateVarDef - { varId :: String -- ^ Name of the variable. - , varType :: Type -- ^ Type of the variable. - , varFlags :: [StateVarFlag] } -- ^ Flags for the variable. - -- | Types used in Kind2 files to represent Copilot types. -- -- The Kind2 backend provides functions to, additionally, constrain the range @@ -39,14 +42,15 @@ data Type = Int | Real | Bool -- | Possible flags for a state variable. data StateVarFlag = FConst --- | Type of the predicate, either belonging to an initial state or a pair of --- states with a transition. -data PredType = Init | Trans - -- | Datatype to describe a term in the Kind language. data Term = ValueLiteral String | PrimedStateVar String | StateVar String | FunApp String [Term] - | PredApp String PredType [Term] + +-- | A definition of a state variable. +data StateVarDef = StateVarDef + { varId :: String -- ^ Name of the variable. + , varType :: Type -- ^ Type of the variable. + , varFlags :: [StateVarFlag] } -- ^ Options for the variable. diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs index f80b8170b..83eae95fc 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs @@ -4,66 +4,116 @@ -- | 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.Char (isSpace) +import Data.List (dropWhileEnd, isInfixOf, isPrefixOf) +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). Note that this function does not parse the output as XML: when given +-- a system in the native transition system format, Kind2 2.x produces output +-- that is not always well-formed XML (e.g., counterexamples to invariant +-- properties cannot be printed for systems in that format, and Kind2 reports +-- the internal 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 - - 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" - - findAnswer tag = - case findChildren (simpleName "Answer") tag of - answTag : _ -> - case onlyText (elContent answTag) of - answ : _ -> cdData answ - _ -> err "Invalid 'Answer' attribute" - _ -> err "Attribute 'Answer' not found" + -- 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 + + -- Substrings of the output following a @\') elem' + + -- The contents of the first @\@ tag in the given element, if + -- any. + answerText elem' = do + (_, rest) <- breakOn "" 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] + +-- | Break a string at the first occurrence of the given pattern, returning +-- the parts of the string before and after (but not including) the pattern, +-- if the pattern occurs in the string. +breakOn :: String -> String -> Maybe (String, String) +breakOn pat = go [] + where + go _ [] = Nothing + go acc s@(c:cs) + | pat `isPrefixOf` s = Just (reverse acc, drop (length pat) s) + | otherwise = go (c : acc) cs + +-- | Split a string at every occurrence of the given pattern, which is not +-- included in the resulting strings. +splitOn :: String -> String -> [String] +splitOn pat s = case breakOn pat s of + Nothing -> [s] + Just (before, after) -> before : splitOn pat after + +-- | Remove whitespace from both ends of a string. +trim :: String -> String +trim = dropWhile isSpace . dropWhileEnd isSpace diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs index 6851d46fa..3c114f91c 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs @@ -1,6 +1,7 @@ {-# 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 2.x. module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where import Copilot.Theorem.Misc.SExpr @@ -15,6 +16,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 +38,42 @@ shouldIndent (List [Atom a, Atom _]) = a `notElem` [kwPrime] shouldIndent _ = True -- | Convert a file into a sequence of expressions. +-- +-- The properties of the file are attached to the last node, which is the top +-- system analyzed by Kind2. ppFile :: File -> [SSExpr] -ppFile (File preds props) = map ppPredDef preds ++ ppProps props +ppFile (File nodes props) = case reverse nodes of + [] -> [] + topN : rest -> reverse $ ppNode topN (ppProps props) : map (`ppNode` []) rest --- | 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 @@ -66,8 +87,3 @@ ppTerm (ValueLiteral c) = atom c ppTerm (PrimedStateVar v) = list [atom kwPrime, atom v] ppTerm (StateVar v) = atom v ppTerm (FunApp f args) = node f $ map ppTerm args -ppTerm (PredApp p t args) = node (p ++ "." ++ ext) $ map ppTerm args - where - ext = case t of - Init -> "init" - Trans -> "trans" diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs index 4bb52322e..9957ce450 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,8 @@ data ProverST = ProverST -- | A prover backend based on Kind2. -- --- The executable @kind2@ must exist and its location be in the @PATH@. +-- The executable @kind2@ (version 2.x) must exist and its location be in the +-- @PATH@. kind2Prover :: Options -> Prover kind2Prover opts = Prover { proverName = "Kind2" @@ -50,24 +52,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" + (tempName, tempHandle) <- openTempFile "." "out" "kind2" 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..81e8b6ca7 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs @@ -2,67 +2,37 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Safe #-} -{-# LANGUAGE ViewPatterns #-} -- | 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 (sort) +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 nodes props where - preds = map (trNode spec predCallsGraph) (specNodes spec) + nodes = map trNode (specNodes spec) props = map trProp $ filter ((`elem` checkedProps) . fst) $ Map.toList $ Map.map fst $ specProps spec @@ -70,65 +40,52 @@ 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 :: Node -> K.Node +trNode node = K.Node + { K.nodeId = nodeId node + , K.nodeStateVars = gatherNodeStateVars 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 last node of the file, which is the top node +-- analyzed by Kind2, 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 (K.File {K.fileNodes, K.fileProps}) = + K.File (changeTail aux fileNodes) fileProps where - changeTail f (reverse -> l) = case l of + changeTail f l = case reverse 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' } - - 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 - --- The ordering really matters here because the variables --- have to be given in this order in a pred call --- Our convention : --- * First the local variables, sorted by alphabetical order --- * Then the imported variables, by alphabetical order on --- the father node then by alphabetical order on the variable name - -gatherPredStateVars :: TransSys -> Node -> [K.StateVarDef] -gatherPredStateVars spec node = locals ++ imported + 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' } + + toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec + vars = map (varName . extVarLocalPart . toExtVar) assumptions + +-- The ordering of state variables really matters here, as Kind2 numbers +-- counterexample streams in the order of declaration. We sort the local +-- variables by alphabetical order. + +-- After inlining, the single remaining node imports no variables, so the +-- state variables of the node are exactly its local variables. +gatherNodeStateVars :: Node -> [K.StateVarDef] +gatherNodeStateVars node = + map (\v -> K.StateVarDef (varName v) (varType v) []) + . sort . Map.keys $ nodeLocalVars node where - nodesMap = Map.fromList [(nodeId n, n) | n <- specNodes spec] - extVarType :: ExtVar -> K.Type - extVarType (ExtVar n v) = - case nodeLocalVars (nodesMap ! n) ! v of + varType v = + case nodeLocalVars node ! v of VarDescr Integer _ -> K.Int VarDescr Bool _ -> K.Bool VarDescr Real _ -> K.Real - locals = - map (\v -> K.StateVarDef (varName v) - (extVarType $ ExtVar (nodeId node) v) []) - . sort . Map.keys $ nodeLocalVars node - - imported = - map (\(v, ev) -> K.StateVarDef (varName v) (extVarType ev) []) - . sortBy (compare `on` snd) . Bimap.toList $ nodeImportedVars node - mkConj :: [K.Term] -> K.Term mkConj [] = trConst Bool True mkConj [x] = x @@ -169,39 +126,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/TransSys/Transform.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs index e59058496..6f135abb2 100644 --- a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs +++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs @@ -3,10 +3,7 @@ -- | Helper module to manipulate and simplify TransSys graphs. module Copilot.Theorem.TransSys.Transform - ( mergeNodes - , inline - , removeCycles - , complete + ( inline ) where import Copilot.Theorem.TransSys.Spec @@ -18,15 +15,12 @@ import Control.Monad (foldM, forM_, forM, guard) import Data.List (sort, (\\), intercalate, partition) -import Control.Exception.Base (assert) - import Data.Map (Map, (!)) import Data.Set (member) import Data.Bimap (Bimap) import qualified Data.Map as Map import qualified Data.Set as Set -import qualified Data.Graph as Graph import qualified Data.Bimap as Bimap prefix :: String -> Var -> Var @@ -179,98 +173,3 @@ redirectLocalImports toMerge = do -- into a /non-modular transition system/ with only one node. inline :: TransSys -> TransSys inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec - --- | Remove cycles by merging nodes participating in strongly connected --- components. --- --- 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 'removeCycles' is to --- remove such dependency cycles. --- --- The function 'removeCycles' computes the strongly connected components of --- the dependency graph and merge each one into a single node using --- 'mergeNodes'. The complexity of this process is high in the worst case (the --- square of the total size of the system times the size of the biggest node) --- but good in practice as few nodes are to be merged in most practical cases. -removeCycles :: TransSys -> TransSys -removeCycles spec = - topoSort $ foldr mergeComp spec (buildScc nodeId $ specNodes spec) - where - - mergeComp (Graph.AcyclicSCC _) s = s - mergeComp (Graph.CyclicSCC ids) s = mergeNodes ids s - - buildScc nrep ns = - let depGraph = map (\n -> (nrep n, nodeId n, nodeDependencies n)) ns - in Graph.stronglyConnComp depGraph - - topoSort s = s { specNodes = - map (\(Graph.AcyclicSCC n) -> n) $ buildScc id (specNodes s) } - --- | Completes each node of a specification with imported variables such that --- each node contains a copy of all its dependencies. --- --- The given specification should have its node sorted by topological order. --- --- The top nodes should have all the other nodes as its dependencies. - -complete :: TransSys -> TransSys -complete spec = - assert (isTopologicallySorted spec) $ spec { specNodes = specNodes' } - - where - - specNodes' = - reverse - . foldl completeNode [] - . specNodes - . completeTopNodeDeps - $ spec - - completeTopNodeDeps spec = spec { specNodes = map aux nodes } - where - nodes = specNodes spec - aux n - | nodeId n == specTopNodeId spec = - n { nodeDependencies = map nodeId nodes \\ [nodeId n] } - | otherwise = n - - -- Takes a list of nodes 'ns', 'n' whose dependencies are in 'ns', and - -- returns 'n2:ns' where 'n2' is 'n' completed - completeNode :: [Node] -> Node -> [Node] - completeNode ns n = (n { nodeDependencies = dependencies' - , nodeImportedVars = importedVars' }) : ns - - where - nsMap = Map.fromList [(nodeId n, n) | n <- ns] - dependencies' = - let newDeps = do - dId <- nodeDependencies n - let d = nsMap ! dId - nodeDependencies d - - in nub' $ nodeDependencies n ++ newDeps - - importedVars' = fst . runRenaming $ do - forM_ (Set.toList $ nodeVarsSet n) addReservedName - let toImportVars = nub' [ ExtVar nId v - | nId <- dependencies' - , let n' = nsMap ! nId - , v <- Map.keys (nodeLocalVars n') ] - - tryImport acc ev@(ExtVar n' v) = do - - -- To get readable names, we don't prefix variables - -- which come from merged nodes as they are already - -- decorated - let preferedName - | head ncNodeIdSep `elem` n' = v - | otherwise = n' `prefix` v - alias <- getFreshName [preferedName, n' `prefix` v] - return $ Bimap.tryInsert alias ev acc - - foldM tryImport (nodeImportedVars n) toImportVars From 1ca1fb34fc5987da321ec810819d6cd9bd25d674 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 9 Jun 2026 13:28:35 -0500 Subject: [PATCH 2/3] copilot-theorem: tests for the Kind2 backend. Refs #734. In order to keep Copilot effectively working in the current software ecosystem, we need to extend the versions of dependencies that Copilot can be installed with. kind2 has seen release 2.3.0, but copilot-theorem requires kind2 0.7.2. This commit adds a testsuite for the Kind2 copilot-theorem native-format backend. It requires Kind2 (v2.x) to be installed and can be activated using the `test-kind2` `cabal` flag (e.g., `cabal test -ftest-kind2`). --- copilot-theorem/copilot-theorem.cabal | 42 +++ copilot-theorem/tests/Kind2Main.hs | 21 ++ .../tests/Test/Copilot/Theorem/Kind2.hs | 301 ++++++++++++++++++ 3 files changed, 364 insertions(+) create mode 100644 copilot-theorem/tests/Kind2Main.hs create mode 100644 copilot-theorem/tests/Test/Copilot/Theorem/Kind2.hs diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index 369ae7b3a..751c033eb 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -35,6 +35,11 @@ source-repository head location: https://github.com/Copilot-Language/copilot.git subdir: copilot-theorem +flag test-kind2 + description: Enable tests that require the Kind2 model checker (kind2) + default: False + manual: True + library default-language : Haskell2010 hs-source-dirs : src @@ -136,3 +141,40 @@ test-suite unit-tests ghc-options: -Wall + +-- Tests of the Kind2 backend, which require the kind2 executable (version +-- 2.x) to be in the PATH. They must be explicitly enabled with the flag +-- test-kind2. +test-suite kind2-tests + type: + exitcode-stdio-1.0 + + main-is: + Kind2Main.hs + + other-modules: + Test.Copilot.Theorem.Kind2 + + build-depends: + base + , HUnit + , mtl + , test-framework + , test-framework-hunit + + , copilot-core + , copilot-theorem + + hs-source-dirs: + tests + + default-language: + Haskell2010 + + ghc-options: + -Wall + + if flag(test-kind2) + buildable: True + else + buildable: False diff --git a/copilot-theorem/tests/Kind2Main.hs b/copilot-theorem/tests/Kind2Main.hs new file mode 100644 index 000000000..28355e4e1 --- /dev/null +++ b/copilot-theorem/tests/Kind2Main.hs @@ -0,0 +1,21 @@ +-- | Test the Kind2 backend of copilot-theorem. +-- +-- These tests require the @kind2@ executable (version 2.x) to be in the +-- @PATH@. +module Main where + +-- External imports +import Test.Framework (Test, defaultMain) + +-- Internal imports +import qualified Test.Copilot.Theorem.Kind2 + +-- | Run all unit tests on the Kind2 backend of copilot-theorem. +main :: IO () +main = defaultMain tests + +-- | All unit tests on the Kind2 backend of copilot-theorem. +tests :: [Test.Framework.Test] +tests = + [ Test.Copilot.Theorem.Kind2.tests + ] diff --git a/copilot-theorem/tests/Test/Copilot/Theorem/Kind2.hs b/copilot-theorem/tests/Test/Copilot/Theorem/Kind2.hs new file mode 100644 index 000000000..97a69985e --- /dev/null +++ b/copilot-theorem/tests/Test/Copilot/Theorem/Kind2.hs @@ -0,0 +1,301 @@ +-- | Test copilot-theorem:Copilot.Theorem.Kind2. +-- +-- These tests require the @kind2@ executable (version 2.x) to be in the +-- @PATH@. +module Test.Copilot.Theorem.Kind2 where + +-- External imports +import Control.Monad.Writer (tell) +import Data.Int (Int32) +import Test.Framework (Test, testGroup) +import Test.Framework.Providers.HUnit (testCase) +import Test.HUnit (Assertion, assertEqual) + +-- External imports: Copilot +import Copilot.Core.Expr (Expr (Const, Drop, ExternVar, Op1, + Op2), Id) +import Copilot.Core.Operators (Op1 (..), Op2 (..)) +import Copilot.Core.Spec (Spec (..), Stream (..)) +import qualified Copilot.Core.Spec as Copilot +import Copilot.Core.Type (Typed (typeOf)) + +-- Internal imports: Modules being tested +import Copilot.Theorem.Kind2.Prover (def, kind2Prover) +import Copilot.Theorem.Prove (Action (..), PropId, prove) + +-- * Constants + +-- | Unit tests for copilot-theorem:Copilot.Theorem.Kind2. +tests :: Test.Framework.Test +tests = + testGroup "Copilot.Theorem.Kind2" + [ testCase "Prove that true is valid" + testTrueValid + , testCase "Prove that false is invalid" + testFalseInvalid + , testCase "Prove that an existentially quantified true is valid" + testExistsTrueValid + , testCase "Prove that an existentially quantified false is invalid" + testExistsFalseInvalid + , testCase "Prove a valid property of a recursive stream" + testCounterGt1 + , testCase "Disprove an invalid property of a recursive stream" + testCounterLt255 + , testCase "Prove a valid existential property of a recursive stream" + testCounterExistsGt3 + , testCase "Prove a valid property of an external stream" + testExternEq + , testCase "Prove a property using an assumption" + testAssumption + , testCase "Disprove a property when its assumption is not used" + testNoAssumption + , testCase "Prove a valid property of a real-valued stream" + testRealValued + , testCase "Prove a valid property of a boolean stream" + testBoolStream + ] + +-- * Individual tests + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- constant True +-- @ +testTrueValid :: Assertion +testTrueValid = + checkProve True propName spec + where + propName = "prop" + spec = forallPropSpec propName [] $ Const typeOf True + +-- | Test that Kind2 is able to prove the following property invalid: +-- @ +-- constant False +-- @ +testFalseInvalid :: Assertion +testFalseInvalid = + checkProve False propName spec + where + propName = "prop" + spec = forallPropSpec propName [] $ Const typeOf False + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- exists: constant True +-- @ +-- +-- Existentially quantified properties are encoded by asking Kind2 to check +-- the negation of the property, so this test exercises the case in which +-- Kind2 reports that a property is falsifiable. +testExistsTrueValid :: Assertion +testExistsTrueValid = + checkProve True propName spec + where + propName = "prop" + spec = existsPropSpec propName [] $ Const typeOf True + +-- | Test that Kind2 is able to prove the following property invalid: +-- @ +-- exists: constant False +-- @ +testExistsFalseInvalid :: Assertion +testExistsFalseInvalid = + checkProve False propName spec + where + propName = "prop" + spec = existsPropSpec propName [] $ Const typeOf False + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- let x = [2] ++ (x + 1) +-- in forAll (x > 1) +-- @ +testCounterGt1 :: Assertion +testCounterGt1 = + checkProve True propName spec + where + propName = "gt1" + spec = forallPropSpec propName [counterStream] $ + Op2 (Gt typeOf) counterExpr (constI32 1) + +-- | Test that Kind2 is able to prove the following property invalid: +-- @ +-- let x = [2] ++ (x + 1) +-- in forAll (x < 255) +-- @ +-- +-- This test exercises the case in which Kind2 reports that a property is +-- falsifiable, which, for systems in Kind2's native input format, also makes +-- Kind2 2.x produce output that is not well-formed XML. +testCounterLt255 :: Assertion +testCounterLt255 = + checkProve False propName spec + where + propName = "lt255" + spec = forallPropSpec propName [counterStream] $ + Op2 (Lt typeOf) counterExpr (constI32 255) + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- let x = [2] ++ (x + 1) +-- in exists (x > 3) +-- @ +testCounterExistsGt3 :: Assertion +testCounterExistsGt3 = + checkProve True propName spec + where + propName = "gt3" + spec = existsPropSpec propName [counterStream] $ + Op2 (Gt typeOf) counterExpr (constI32 3) + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- let e = extern "ext" Nothing +-- in forAll (e == e) +-- @ +testExternEq :: Assertion +testExternEq = + checkProve True propName spec + where + propName = "eq" + extECopy = ExternVar typeOf "ext" Nothing :: Expr Int32 + spec = forallPropSpec propName [] $ Op2 (Eq typeOf) extECopy extECopy + +-- | Test that Kind2 is able to prove the property @lt20@ valid when assuming +-- the property @lt10@, in the following specification: +-- @ +-- let x = [2] ++ (x + 1) +-- in forAll (x < 10) -- lt10 +-- forAll (x < 20) -- lt20 +-- @ +testAssumption :: Assertion +testAssumption = do + result <- prove spec "lt20" $ + tell [Assume "lt10", Check (kind2Prover def)] + assertEqual "proof result for lt20 (assuming lt10)" True result + where + spec = assumptionSpec + +-- | Test that Kind2 is able to prove the property @lt20@ invalid when the +-- assumption @lt10@ is not used, in the same specification as +-- 'testAssumption'. +testNoAssumption :: Assertion +testNoAssumption = do + result <- prove spec "lt20" $ + tell [Check (kind2Prover def)] + assertEqual "proof result for lt20 (without assumptions)" False result + where + spec = assumptionSpec + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- let y = [0.5] ++ y +-- in forAll (y > 0.0) +-- @ +testRealValued :: Assertion +testRealValued = + checkProve True propName spec + where + propName = "pos" + + streamId' :: Id + streamId' = 0 + + stream :: Stream + stream = Stream + { streamId = streamId' + , streamBuffer = [0.5 :: Double] + , streamExpr = Drop typeOf 0 streamId' + , streamExprType = typeOf + } + + spec = forallPropSpec propName [stream] $ + Op2 (Gt typeOf) (Drop typeOf 0 streamId' :: Expr Double) + (Const typeOf (0.0 :: Double)) + +-- | Test that Kind2 is able to prove the following property valid: +-- @ +-- let b = [True] ++ (b && constant True) +-- in forAll (not (not b)) +-- @ +testBoolStream :: Assertion +testBoolStream = + checkProve True propName spec + where + propName = "tt" + + streamId' :: Id + streamId' = 0 + + stream :: Stream + stream = Stream + { streamId = streamId' + , streamBuffer = [True] + , streamExpr = Op2 And (Drop typeOf 0 streamId') (Const typeOf True) + , streamExprType = typeOf + } + + spec = forallPropSpec propName [stream] $ + Op1 Not (Op1 Not (Drop typeOf 0 streamId')) + +-- * Auxiliary + +-- | Check that proving the given property of the given spec with the Kind2 +-- prover produces the expected result. +checkProve :: Bool -> PropId -> Spec -> Assertion +checkProve expectation propName spec = do + result <- prove spec propName $ tell [Check (kind2Prover def)] + assertEqual ("proof result for property " ++ propName) expectation result + +-- | A stream of 'Int32' defined by: +-- @ +-- x = [2] ++ (x + 1) +-- @ +counterStream :: Stream +counterStream = Stream + { streamId = counterStreamId + , streamBuffer = [2 :: Int32] + , streamExpr = Op2 (Add typeOf) counterExpr (constI32 1) + , streamExprType = typeOf + } + +-- | Id of 'counterStream'. +counterStreamId :: Id +counterStreamId = 0 + +-- | The current value of 'counterStream'. +counterExpr :: Expr Int32 +counterExpr = Drop typeOf 0 counterStreamId + +-- | A constant 'Int32' expression. +constI32 :: Int32 -> Expr Int32 +constI32 = Const typeOf + +-- | A specification with the 'counterStream' and two properties, @lt10@ and +-- @lt20@, stating that the values of the stream are smaller than 10 and 20, +-- respectively. Both properties are invalid on their own, but @lt20@ holds +-- if @lt10@ is assumed. +assumptionSpec :: Spec +assumptionSpec = Spec + [counterStream] + [] + [] + [ Copilot.Property "lt10" $ Copilot.Forall $ + Op2 (Lt typeOf) counterExpr (constI32 10) + , Copilot.Property "lt20" $ Copilot.Forall $ + Op2 (Lt typeOf) counterExpr (constI32 20) + ] + +-- | Build a 'Spec' that contains one property with the given name, which +-- contains the given streams, and is defined by the given boolean expression, +-- which is universally quantified. +forallPropSpec :: String -> [Stream] -> Expr Bool -> Spec +forallPropSpec propName propStreams propExpr = + Spec propStreams [] [] [Copilot.Property propName (Copilot.Forall propExpr)] + +-- | Build a 'Spec' that contains one property with the given name, which +-- contains the given streams, and is defined by the given boolean expression, +-- which is existentially quantified. +existsPropSpec :: String -> [Stream] -> Expr Bool -> Spec +existsPropSpec propName propStreams propExpr = + Spec propStreams [] [] [Copilot.Property propName (Copilot.Exists propExpr)] From b7d695d6dc7f1831abe0389ca522c68d9e937114 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Tue, 9 Jun 2026 13:54:17 -0500 Subject: [PATCH 3/3] copilot-theorem: Document changes in CHANGELOG. Refs #734. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 03facaf36..cfc067260 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-06-09 + * Update Kind2 backend to support Kind2 2.x. (#734) + 2026-05-07 * Version bump (4.7.1). (#730) * Handle special Float values correctly for counterexamples. (#697)