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) 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..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 @@ -60,7 +65,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 @@ -137,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/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 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)]