diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 03facaf36..f2a31ba76 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2026-06-09 + * Update Kind2 backend to support Kind2 1.0 and newer. (#734) + 2026-05-07 * Version bump (4.7.1). (#730) * Handle special Float values correctly for counterexamples. (#697) diff --git a/copilot-theorem/README.md b/copilot-theorem/README.md index 64cce8995..47a4b6081 100644 --- a/copilot-theorem/README.md +++ b/copilot-theorem/README.md @@ -31,7 +31,8 @@ properties on Copilot programs. It includes: * The *copilot-core* and *copilot-prettyprinter* Haskell libraries * The *Yices2* SMT-solver: `yices-smt2` must be in your `$PATH` * The *Z3* SMT-solver: `z3` must be in your `$PATH` -* The *Kind2* model checker: `kind2` must be in your `$PATH` +* The *Kind2* model checker (version 1.0 or newer): `kind2` must be in your + `$PATH` To build it, just install the Copilot library as described in the top-level README. @@ -87,7 +88,9 @@ configuration. The *Kind2* prover uses the model checker with the same name, from the University of Iowa. It translates the Copilot specification into a *modular transition system* (the Kind2 native format) and then calls the `kind2` -executable. +executable. Kind2 version 1.0 or newer is required: the native input format +and the command-line options used by this prover were introduced in Kind2 +1.0, and remain supported as of Kind2 3.0. It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prover :: Options -> Prover` where the `Options` type is defined as @@ -95,7 +98,7 @@ It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prov ```haskell data Options = Options { bmcMax :: Int } ``` -and where `bmcMax` corresponds to the `--bmc_max` option of *kind2* and is +and where `bmcMax` corresponds to the `--unroll_max` option of *kind2* and is equivalent to the `maxK` option of the K-Induction prover. Its default value is 0, which stands for infinity. @@ -335,11 +338,16 @@ process. The transition system obtained by the `TransSys.Translate` module is perfectly consistent. However, it can't be directly translated into the *Kind2 native -file format*. Indeed, it is natural to bind each node to a predicate but the -Kind2 file format requires that each predicate only uses previously defined -predicates. However, some nodes in our transition system could be mutually -recursive. Therefore, the goal of the `removeCycles :: Spec -> Spec` function, -defined in `TransSys.Transform`, is to remove such dependency cycles. +file format*. The native input format of Kind2 (version 1.0 and newer) does +not support predicate calls inside the initial state and transition relation +predicates of a node, so the modular structure of the transition system cannot +be expressed directly in it. Therefore, the system is first turned into an +equivalent non-modular transition system with only one node by the +`inline :: Spec -> Spec` function, defined in `TransSys.Transform`: +```haskell +inline :: Spec -> Spec +inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec +``` This function relies on the `mergeNodes :: [NodeId] -> Spec -> Spec` function, whose signature is self-explicit. The latter solves name conflicts by using the @@ -516,10 +524,14 @@ in the Kind2 SMT solver. #### Displaying counterexamples Counterexamples are not displayed with the Kind2 prover because Kind2 doesn't -support XML output of counterexamples. If the last feature is provided, it -should be easy to implement displaying of counterexamples in *copilot-theorem*. -For this, we recommend keeping some information about *observers* in -`TransSys.Spec` and to add one variable per observer in the Kind2 output file. +support the output of counterexamples for systems expressed in its native input +format (the counterexample printing functions in Kind2's +[`src/inputSystem.ml`](https://github.com/kind2-mc/kind2/blob/v3.0.0/src/inputSystem.ml) +fail with an internal error for native input). If Kind2 adds this feature, it +should be easy to implement displaying of counterexamples in +*copilot-theorem*. For this, we recommend keeping some information about +*observers* in `TransSys.Spec` and to add one variable per observer in the +Kind2 output file. #### Bad handling of non-linear operators and external functions @@ -569,14 +581,14 @@ architecture of Kind2. It is true that the code of `TransSys` is quite complex. In fact, it would be really straightforward to produce a flattened transition system and then a -Kind2 file with just a single *top* predicate. In fact, It would be as easy as +Kind2 file with just a single *top* node. In fact, It would be as easy as producing an *IL* specification. To be honest, I'm not sure producing a modular *Kind2* output is worth the complexity added. It's especially true at the time I write this in the sense that: -* Each predicate introduced is used only one time (which is true because +* Each node introduced is used only one time (which is true because Copilot doesn't handle functions or parameterized streams like Lustre does and everything is inlined during the reification process). * A similar form of structure could be obtained from a flattened Kind2 native diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index cd9d2e00e..28cbbba38 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 @@ -51,6 +56,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,7 +66,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 +142,40 @@ test-suite unit-tests ghc-options: -Wall + +-- Tests of the Kind2 backend, which require the kind2 executable (version +-- 1.0 or newer) 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..2ced67ca9 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/AST.hs @@ -1,27 +1,53 @@ {-# 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 +-- (, +-- which includes a sketch of the grammar in a comment near the end of the +-- file) and the example file +-- +-- distributed with Kind2. module Copilot.Theorem.Kind2.AST where --- | A file is a sequence of predicates and propositions. +-- | A file is a sequence of node definitions, together with a distinguished +-- top node and a series of propositions about the top node. +-- +-- Kind2 analyzes the last node defined in a file as the top system, so the +-- top node is always printed after all the other nodes. data File = File - { filePreds :: [PredDef] - , fileProps :: [Prop] } + { fileNodes :: [Node] -- ^ Nodes other than the top node, in dependency + -- order (a node may only refer to nodes defined + -- before it). + , fileTopNode :: Node -- ^ The top node, which the propositions are + -- attached to. + , fileProps :: [Prop] -- ^ Propositions about the top node. + } -- | A proposition is defined by a term. data Prop = Prop { propName :: String , propTerm :: Term } --- | A predicate definition. -data PredDef = PredDef - { predId :: String -- ^ Identifier for the predicate. - , predStateVars :: [StateVarDef] -- ^ Variables identifying the states in the - -- underlying state transition system. - , predInit :: Term -- ^ Predicate that holds for initial +-- | A node definition. +data Node = Node + { nodeId :: String -- ^ Identifier for the node. + , nodeStateVars :: [StateVarDef] -- ^ Variables identifying the states in + -- the underlying state transition system. + , nodeInit :: Term -- ^ Predicate that holds for initial -- states. - , predTrans :: Term -- ^ Predicate that holds for two states, if - -- there is state transition between them. + , nodeTrans :: Term -- ^ Predicate that holds for two states, + -- if there is a state transition between + -- them. } -- | A definition of a state variable. diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs index f80b8170b..8a1d29c28 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Output.hs @@ -4,66 +4,97 @@ -- | Parse output of Kind2. module Copilot.Theorem.Kind2.Output (parseOutput) where -import Text.XML.Light hiding (findChild) -import Copilot.Theorem.Prove as P -import Data.Maybe (fromJust) +import Data.List.Extra (isInfixOf, splitOn, stripInfix, trim) +import Data.Maybe (mapMaybe) + +import Copilot.Theorem.Prove as P import qualified Copilot.Core as C import qualified Copilot.Theorem.Misc.Error as Err -simpleName s = QName s Nothing Nothing - -- | Parse output of Kind2. +-- +-- The output is expected to be in XML format, as produced by Kind2's @-xml@ +-- flag and documented at +-- . +-- Note that this function does not parse the output as XML: when given a +-- system in the native transition system format, Kind2 produces output that +-- is not always well-formed XML (e.g., counterexamples to invariant +-- properties cannot be printed for systems in that format -- the +-- counterexample printing functions in Kind2's @src/inputSystem.ml@ fail with +-- an internal error for native input -- and Kind2 reports the error in the +-- middle of the XML output). Instead, this function looks for the +-- @\@ tag for the given property and extracts the answers in the +-- @\@ tags it contains. parseOutput :: String -- ^ Property whose validity is being checked. -> C.Prop -- ^ The property's quantifier. -> String -- ^ XML output of Kind2 -> P.Output -parseOutput propId propQuantifier xml = fromJust $ do - root <- parseXMLDoc xml - case findAnswer . findPropTag $ root of - "valid" -> case propQuantifier of - -- We encode a universally quantified property P as - -- ∀x.P(x) in Kind2, so the original property is valid - -- iff the Kind2 property is valid. - C.Forall {} -> return (Output Valid []) - -- We encode an existentially quantified property P as - -- ¬(∀x.¬(P(x))) in Kind2, so the original property is - -- invalid iff the Kind2 property is valid. - C.Exists {} -> return (Output Invalid []) - "falsifiable" -> case propQuantifier of - -- We encode a universally quantified property P as - -- ∀x.P(x) in Kind2, so the original property is invalid - -- iff the Kind2 property is invalid. - C.Forall {} -> return (Output Invalid []) - -- We encode an existentially quantified property P as - -- ¬(∀x.¬(P(x))) in Kind2, so the original property is - -- valid iff the Kind2 property is invalid. - C.Exists {} -> return (Output Valid []) - s -> err $ "Unrecognized status : " ++ s +parseOutput propId propQuantifier xml + | "valid" `elem` answers = quantified (Output Valid []) + (Output Invalid []) + | "falsifiable" `elem` answers = quantified (Output Invalid []) + (Output Valid []) + | "unknown" `elem` answers = Output Unknown [] + | null answers = err $ "Answer for property " ++ propId ++ " not found" + | otherwise = err $ "Unrecognized status : " ++ unwords answers where - searchForRuntimeError = undefined + -- Pick an output based on the quantifier of the property. The first + -- argument is returned when the property Kind2 was asked about is valid, + -- and the second one when it is invalid. + -- + -- We encode a universally quantified property P as ∀x.P(x) in Kind2, so + -- the original property is valid iff the Kind2 property is valid. + -- + -- We encode an existentially quantified property P as ¬(∀x.¬(P(x))) in + -- Kind2, so the original property is valid iff the Kind2 property is + -- invalid. + quantified ifValid ifInvalid = case propQuantifier of + C.Forall {} -> ifValid + C.Exists {} -> ifInvalid + + -- All the answers reported for the property, in the order in which they + -- appear in the output. A conclusive answer (valid or falsifiable), if + -- any, takes precedence over inconclusive (unknown) ones, which Kind2 may + -- also report when the analysis terminates without an answer for all + -- properties. + answers = mapMaybe answerText + $ filter isRightProperty + $ propertyElems xml - findPropTag root = - let rightElement elt = - qName (elName elt) == "Property" - && lookupAttr (simpleName "name") (elAttribs elt) - == Just propId - in case filterChildren rightElement root of - tag : _ -> tag - _ -> err $ "Tag for property " ++ propId ++ " not found" + -- Substrings of the output following a @\ - case onlyText (elContent answTag) of - answ : _ -> cdData answ - _ -> err "Invalid 'Answer' attribute" - _ -> err "Attribute 'Answer' not found" + -- True if the given property element has the name of the property this + -- function looks for. + isRightProperty elem' = + ("name=\"" ++ escapeAttr propId ++ "\"") `isInfixOf` openingTag + where + openingTag = takeWhile (/= '>') elem' + + -- The contents of the first @\@ tag in the given element, if + -- any. + answerText elem' = do + (_, rest) <- stripInfix "" rest + let answer = trim $ takeWhile (/= '<') rest' + if null answer then Nothing else Just answer err :: forall a . String -> a err msg = Err.fatal $ "Parse error while reading the Kind2 XML output : \n" ++ msg ++ "\n\n" ++ xml + +-- | Escape a string for use as an XML attribute value. +escapeAttr :: String -> String +escapeAttr = concatMap escapeChar + where + escapeChar '&' = "&" + escapeChar '<' = "<" + escapeChar '>' = ">" + escapeChar '"' = """ + escapeChar c = [c] diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs index 6851d46fa..92d158a1c 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs @@ -1,6 +1,8 @@ {-# LANGUAGE Safe #-} --- | Pretty print a Kind2 file defining predicates and propositions. +-- | Pretty print a Kind2 file defining nodes and propositions, in the native +-- transition system input format supported by Kind2 1.0 and newer (see +-- "Copilot.Theorem.Kind2.AST" for pointers to references on the format). module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where import Copilot.Theorem.Misc.SExpr @@ -15,6 +17,14 @@ type SSExpr = SExpr String -- | Reserved keyword prime. kwPrime = "prime" +-- | Dummy position attached to the properties of the file. +-- +-- Kind2 requires a position (in the format @file:row-col@) for properties +-- declared with the @:user@ source annotation, and reports that position back +-- in its output. +propPosition :: String +propPosition = "copilot:1-1" + -- | Pretty print a Kind2 file. prettyPrint :: File -> String prettyPrint = @@ -29,30 +39,41 @@ shouldIndent (List [Atom a, Atom _]) = a `notElem` [kwPrime] shouldIndent _ = True -- | Convert a file into a sequence of expressions. +-- +-- The top node is printed last, since Kind2 analyzes the last node of the +-- file as the top system. The properties of the file are attached to it. ppFile :: File -> [SSExpr] -ppFile (File preds props) = map ppPredDef preds ++ ppProps props +ppFile (File nodes top props) = + map (`ppNode` []) nodes ++ [ppNode top (ppProps props)] --- | Convert a sequence of propositions into command to check each of them. +-- | Convert a sequence of propositions into a props field. ppProps :: [Prop] -> [SSExpr] -ppProps ps = [ node "check-prop" [ list $ map ppProp ps ] ] +ppProps [] = [] +ppProps ps = [ node "props" [ list $ map ppProp ps ] ] -- | Convert a proposition into an expression. ppProp :: Prop -> SSExpr -ppProp (Prop n t) = list [atom n, ppTerm t] +ppProp (Prop n t) = list [atom n, ppTerm t, atom ":user", atom propPosition] --- | Convert a predicate into an expression. -ppPredDef :: PredDef -> SSExpr -ppPredDef pd = - list [ atom "define-pred" - , atom (predId pd) - , list . map ppStateVarDef . predStateVars $ pd - , node "init" [ppTerm $ predInit pd] - , node "trans" [ppTerm $ predTrans pd] ] +-- | Convert a node, together with optional extra fields, into an expression. +ppNode :: Node -> [SSExpr] -> SSExpr +ppNode n extraFields = + list $ [ atom "define-node" + , atom (nodeId n) + , list . map ppStateVarDef . nodeStateVars $ n + , node "init" [ppTerm $ nodeInit n] + , node "trans" [ppTerm $ nodeTrans n] ] + ++ extraFields -- | Convert a state variable definition into an expression. ppStateVarDef :: StateVarDef -> SSExpr ppStateVarDef svd = - list [atom (varId svd), ppType (varType svd)] + list $ [atom (varId svd), ppType (varType svd)] + ++ map ppStateVarFlag (varFlags svd) + +-- | Convert a state variable option into an expression. +ppStateVarFlag :: StateVarFlag -> SSExpr +ppStateVarFlag FConst = atom ":const" -- | Convert a type into an expression. ppType :: Type -> SSExpr diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs index 4bb52322e..a79ede4f6 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Prover.hs @@ -28,7 +28,8 @@ import qualified Copilot.Theorem.TransSys as TS -- | Options for Kind2 data Options = Options { bmcMax :: Int -- ^ Upper bound on the number of unrolling that base and - -- step will perform. A value of 0 means /unlimited/. + -- step will perform (passed to Kind2 via its + -- @--unroll_max@ option). A value of 0 means /unlimited/. } -- | Default options with unlimited unrolling for base and step. @@ -41,7 +42,10 @@ data ProverST = ProverST -- | A prover backend based on Kind2. -- --- The executable @kind2@ must exist and its location be in the @PATH@. +-- The executable @kind2@ must exist and its location be in the @PATH@. Kind2 +-- version 1.0 or newer is required: the native input format and the +-- command-line options this prover uses were introduced in Kind2 1.0, and +-- remain supported as of Kind2 3.0. kind2Prover :: Options -> Prover kind2Prover opts = Prover { proverName = "Kind2" @@ -50,24 +54,22 @@ kind2Prover opts = Prover , closeProver = const $ return () } kind2Prog = "kind2" -kind2BaseOptions = ["--input-format", "native", "-xml"] +kind2BaseOptions = ["--input_format", "native", "-xml"] askKind2 :: ProverST -> [PropId] -> [PropId] -> IO Output askKind2 (ProverST opts spec) assumptions toCheck = do - let kind2Input = prettyPrint . toKind2 Inlined assumptions toCheck $ spec + let kind2Input = prettyPrint . toKind2 assumptions toCheck $ spec (tempName, tempHandle) <- openTempFile "." "out" "kind" hPutStr tempHandle kind2Input hClose tempHandle let kind2Options = - kind2BaseOptions ++ ["--bmc_max", show $ bmcMax opts, tempName] + kind2BaseOptions ++ ["--unroll_max", show $ bmcMax opts, tempName] (_, output, _) <- readProcessWithExitCode kind2Prog kind2Options "" - putStrLn kind2Input - removeFile tempName let propId = head toCheck diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs index 123f6ed64..d59aaae24 100644 --- a/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/Kind2/Translate.hs @@ -1,68 +1,44 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE Safe #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE Safe #-} -- | Convert modular transition systems ('TransSys') into Kind2 file -- specifications. module Copilot.Theorem.Kind2.Translate ( toKind2 - , Style (..) ) where import Copilot.Theorem.TransSys import qualified Copilot.Theorem.Kind2.AST as K -import Control.Exception.Base (assert) - import Data.Function (on) import Data.Maybe (fromJust) -import Data.List (sort, sortBy) -import Data.Map (Map, (!)) +import Data.List (partition, sort, sortBy) +import Data.Map ((!)) import qualified Data.Map as Map import qualified Data.Bimap as Bimap --- The following properties MUST hold for the given transition system : --- * Nodes are sorted by topological order --- * Nodes are `completed`, which means the dependency graph is transitive --- and each node imports all the local variables of its dependencies --- - -type DepGraph = Map NodeId [NodeId] - --- | Style of the Kind2 files produced: modular (with multiple separate nodes), --- or all inlined (with only one node). --- --- In the modular style, the graph is simplified to remove cycles by collapsing --- all nodes participating in a strongly connected components. --- --- In the inlined style, the structure of the modular transition system is --- discarded and the graph is first turned into a /non-modular transition/ --- /system/ with only one node, which can be then converted into a Kind2 file. -data Style = Inlined | Modular - -- | Produce a Kind2 file that checks the properties specified. -toKind2 :: Style -- ^ Style of the file (modular or inlined). - -> [PropId] -- ^ Assumptions +toKind2 :: [PropId] -- ^ Assumptions -> [PropId] -- ^ Properties to be checked -> TransSys -- ^ Modular transition system holding the system spec -> K.File -toKind2 style assumptions checkedProps spec = - addAssumptions spec assumptions - $ trSpec (complete spec') predCallsGraph assumptions checkedProps +toKind2 assumptions checkedProps spec = + addAssumptions spec' assumptions $ trSpec spec' checkedProps where - predCallsGraph = specDependenciesGraph spec' - spec' = case style of - Inlined -> inline spec - Modular -> removeCycles spec + spec' = inline spec -trSpec :: TransSys -> DepGraph -> [PropId] -> [PropId] -> K.File -trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props +trSpec :: TransSys -> [PropId] -> K.File +trSpec spec checkedProps = K.File otherNodes topNode props where - preds = map (trNode spec predCallsGraph) (specNodes spec) + (topNode, otherNodes) = + case partition ((== specTopNodeId spec) . K.nodeId) nodes of + ([top], others) -> (top, others) + _ -> error $ "Kind2.Translate: top node " + ++ specTopNodeId spec ++ " not found" + nodes = map (trNode spec) (specNodes spec) props = map trProp $ filter ((`elem` checkedProps) . fst) $ Map.toList $ Map.map fst $ specProps spec @@ -70,37 +46,30 @@ trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props trProp :: (PropId, ExtVar) -> K.Prop trProp (pId, var) = K.Prop pId (trVar . extVarLocalPart $ var) -trNode :: TransSys -> DepGraph -> Node -> K.PredDef -trNode spec predCallsGraph node = - K.PredDef { K.predId, K.predStateVars, K.predInit, K.predTrans } - where - predId = nodeId node - predStateVars = gatherPredStateVars spec node - predInit = mkConj $ initLocals node - ++ map (trExpr False) (nodeConstrs node) - ++ predCalls True spec predCallsGraph node - predTrans = mkConj $ transLocals node - ++ map (trExpr True) (nodeConstrs node) - ++ predCalls False spec predCallsGraph node - +trNode :: TransSys -> Node -> K.Node +trNode spec node = K.Node + { K.nodeId = nodeId node + , K.nodeStateVars = gatherPredStateVars spec node + , K.nodeInit = mkConj $ initLocals node + ++ map (trExpr False) (nodeConstrs node) + , K.nodeTrans = mkConj $ transLocals node + ++ map (trExpr True) (nodeConstrs node) + } + +-- | Add the assumptions to the top node of the file by conjoining the +-- corresponding property variables to its initial state and transition +-- relation predicates. addAssumptions :: TransSys -> [PropId] -> K.File -> K.File -addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) = - K.File (changeTail aux filePreds) fileProps +addAssumptions spec assumptions file = + file { K.fileTopNode = aux (K.fileTopNode file) } where - changeTail f (reverse -> l) = case l of - [] -> error "impossible" - x : xs -> reverse $ f x : xs - - aux pred = - let init' = mkConj ( K.predInit pred : map K.StateVar vars ) - trans' = mkConj ( K.predTrans pred : map K.PrimedStateVar vars ) - in pred { K.predInit = init', K.predTrans = trans' } + aux node = + let init' = mkConj ( K.nodeInit node : map K.StateVar vars ) + trans' = mkConj ( K.nodeTrans node : map K.PrimedStateVar vars ) + in node { K.nodeInit = init', K.nodeTrans = trans' } - vars = - let bindings = nodeImportedVars (specTopNode spec) - toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec - toTopVar (ExtVar nId v) = assert (nId == specTopNodeId spec) v - in map (varName . toTopVar . toExtVar) assumptions + toExtVar a = fst $ fromJust $ Map.lookup a $ specProps spec + vars = map (varName . extVarLocalPart . toExtVar) assumptions -- The ordering really matters here because the variables -- have to be given in this order in a pred call @@ -169,39 +138,6 @@ transLocals node = Expr e -> [mkEquality (trPrimedVar v) (trExpr True e)] Constrs cs -> map (trExpr True) cs -predCalls :: Bool -> TransSys -> DepGraph -> Node -> [K.Term] -predCalls isInitCall spec predCallsGraph node = - map mkCall toCall - where - nid = nodeId node - toCall = predCallsGraph ! nid - nodesMap = Map.fromList [(nodeId n, n) | n <- specNodes spec] - - nodeLocals n = - map (ExtVar n) . sort . Map.keys - . nodeLocalVars $ (nodesMap ! n) - - mkCall callee - | isInitCall = - K.PredApp callee K.Init (argsSeq trVar) - | otherwise = - K.PredApp callee K.Trans (argsSeq trVar ++ argsSeq trPrimedVar) - where - - calleeLocals = nodeLocals callee - calleeImported = - (concatMap nodeLocals . sort . nodeDependencies) $ nodesMap ! callee - - localAlias trVarF ev = - case Bimap.lookupR ev $ nodeImportedVars node of - Nothing -> error $ - "This spec is not complete : " - ++ show ev ++ " should be imported in " ++ nid - Just v -> trVarF v - - argsSeq trVarF = - map (localAlias trVarF) (calleeLocals ++ calleeImported) - trExpr :: Bool -> Expr t -> K.Term trExpr primed = tr where diff --git a/copilot-theorem/tests/Kind2Main.hs b/copilot-theorem/tests/Kind2Main.hs new file mode 100644 index 000000000..657033de9 --- /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 1.0 or newer) 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..bca62dba6 --- /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 1.0 or newer) 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 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)]