diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,29 @@ +2009 +BSD3 License terms + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +Neither the name of the developers nor the names of its contributors +may be used to endorse or promote products derived from this software +without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,863 @@ +[![Build Status](https://travis-ci.org/Copilot-Language/copilot-theorem.svg?branch=master)](https://travis-ci.org/Copilot-Language/copilot-theorem) + +# Copilot Theorem + +Highly automated proof techniques are a necessary step for the widespread +adoption of formal methods in the software industry. Moreover, it could provide +a partial answer to one of its main issue which is scalability. + +*copilot-theorem* is a Copilot library aimed at checking automatically some safety +properties on Copilot programs. It includes : + +* A general interface for *provers* and a *proof scheme* mechanism aimed at + splitting the task of proving a complex property into checking a sequence of + smaller lemmas. + +* A prover implementing basic **k-induction** model checking [1], useful for + proving basic k-inductive properties and for pedagogical purposes. + +* A prover producing native inputs for the *Kind2* model checker, developed at + University of Iowa. The latter uses both the *k-induction algorithm* extended + with *path compression* and *structural abstraction* [2] and the **IC3 + algorithm** with counterexample generalization based on *approximate + quantifier elimination* [3]. + +## A Tutorial + +### Installation instructions + +*copilot-theorem* needs the following dependencies to be installed : + +* The *copilot-core* and *copilot-language* 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` + +To build it, just clone this repository and use `cabal install`. You will find +some examples in the `examples` folder, which can be built with `cabal install` +too, producing an executable `copilot-theorem-example` in your `.cabal/bin` +folder. + +### First steps + +*copilot-theorem* is aimed at checking **safety properties** on Copilot programs. +Intuitively, a safety property is a property which express the idea that +*nothing bad can happen*. In particular, any invalid safety property can be +disproved by a finite execution trace of the program called a +**counterexample**. Safety properties are often opposed to **liveness** +properties, which express the idea that *something good will eventually +happen*. The latters are out of the scope of *copilot-theorem*. + +Safety properties are simply expressed with standard boolean streams. In +addition to triggers and observers declarations, it is possible to bind a +boolean stream to a property name with the `prop` construct in the +specification. + +For instance, here is a straightforward specification declaring one property : + +```haskell +spec :: Spec +spec = do + prop "gt0" (x > 0) + where + x = [1] ++ (1 + x) +``` + +Let's say we want to check that `gt0` holds. For this, we use the `prove :: +Prover -> ProofScheme -> Spec -> IO ()` function exported by `Copilot.Theorem`. +This function takes three arguments : + +* The prover we want to use. For now, two provers are available, exported by + the `Copilot.Theorem.Light` and `Copilot.Theorem.Kind2` module. +* A *proof scheme*, which is a sequence of instructions like *check*, *assume*, + *assert*... +* The Copilot specification + +Here, we can just write + +```haskell +prove (lightProver def) (check "gt0") spec +``` + +where `lightProver def` stands for the *light prover* with default +configuration. + +### The Prover interface + +The `Copilot.Theorem.Prover` defines a general interface for provers. Therefore, +it is really easy to add a new prover by creating a new object of type +`Prover`. The latter is defined like this : + +```haskell +data Cex = Cex + +type Infos = [String] + +data Output = Output Status Infos + +data Status + = Valid + | Invalid (Maybe Cex) + | Unknown + | Error + +data Feature = GiveCex | HandleAssumptions + +data Prover = forall r . Prover + { proverName :: String + , hasFeature :: Feature -> Bool + , startProver :: Core.Spec -> IO r + , askProver :: r -> [PropId] -> PropId -> IO Output + , closeProver :: r -> IO () + } +``` + +Each prover mostly has to provide a `askProver` function which takes as an +argument +* The prover descriptor +* A list of assumptions +* A conclusion + +and checks if the assumptions logically entail the conclusion. + +Two provers are provided by default : `Light` and `Kind2`. + +#### The light prover + +The *light prover* is a really simple prover which uses the Yices SMT solver +with the `QF_UFLIA` theory and is limited to prove *k-inductive* properties, +that is properties such that there exists some *k* such that : + +* The property holds during the first *k* steps of the algorithm. +* From the hypothesis the property has held during *k* consecutive steps, we + can prove it is still true one step further. + +For instance, in this example + +```haskell +spec :: Spec +spec = do + prop "gt0" (x > 0) + prop "neq0" (x /= 0) + where + x = [1] ++ (1 + x) +``` +the property `"gt0"` is inductive (1-inductive) but the property `"neq0"` is +not. + + +The *light prover* is defined in `Copilot.Theorem.Light`. This module exports the +`lightProver :: Options -> Prover` function which builds a prover from a record +of type `Options` : + +```haskell +data Options = Options + { kTimeout :: Integer + , onlyBmc :: Bool + , debugMode :: Bool } +``` + +Here, + +* `kTimeout` is the maximum number of steps of the k-induction algorithm the + prover executes before giving up. +* If `onlyBmc` is set to `True`, the prover will only search for + counterexamples and won't try to prove the properties discharged to it. +* If `debugMode` is set to `True`, the SMTLib queries produced by the prover + are displayed in the standard output. + +`Options` is an instance of the `Data.Default` typeclass : + +```haskell +instance Default Options where + def = Options + { kTimeout = 100 + , debugMode = False + , onlyBmc = False } +``` + +Therefore, `def` stands for the default configuration. + +#### The Kind2 prover + +The *Kind2* prover uses the model checker with the same name, from Iowa +university. It translates the Copilot specification into a *modular transition +system* (the Kind2 native format) and then calls the `kind2` executable. + +It is provided by the `Copilot.Theorem.Kind2` module, which exports a `kind2Prover +:: Options -> Prover` where the `Options` type is defined as + +```haskell +data Options = Options { bmcMax :: Int } +``` +and where `bmcMax` corresponds to the `--bmc_max` option of *kind2* and is +equivalent to the `kTimeout` option of the light prover. Its default value is +0, which stands for infinity. + +#### Combining provers + +The `combine :: Prover -> Prover -> Prover` function lets you merge two provers +A and B into a prover C which launches both A and B and returns the *most +precise* output. It would be interesting to implement other merging behaviours +in the future. For instance, a *lazy* one such that C launches B only if A has +returns *unknown* or *error*. + +As an example, the following prover is used in `Driver.hs` : + +```haskell +prover = + lightProver def {onlyBmc = True, kTimeout = 5} + `combine` kind2Prover def +``` + +We will discuss the internals and the experimental results of these provers +later. + +### Proof schemes + +Let's consider again this example : + +```haskell +spec :: Spec +spec = do + prop "gt0" (x > 0) + prop "neq0" (x /= 0) + where + x = [1] ++ (1 + x) +``` + +and let's say we want to prove `"neq0"`. Currently, the two available solvers +fail at showing this non-inductive property (we will discuss this limitation +later). Therefore, we can prove the more general inductive lemma `"gt0"` and +deduce our main goal from this. For this, we use the proof scheme + +```haskell +assert "gt0" >> check "neq0" +``` +instead of just `check "neq0"`. A proof scheme is chain of primitives schemes +glued by the `>>` operator. For now, the available primitives are : + +* `check "prop"` checks whether or not a given property is true in the current + context. +* `assume "prop"` adds an assumption in the current context. +* `assert "prop"` is a shortcut for `check "prop" >> assume "prop"`. +* `assuming :: [PropId] -> ProofScheme -> ProofScheme` is such that `assuming + props scheme` assumes the list of properties *props*, executes the proof + scheme *scheme* in this context, and forgets the assumptions. +* `msg "..."` displays a string in the standard output + +We will discuss the limitations of this tool and a way to use it in practice +later. + +### Some examples + +Some examples are in the *examples* folder. The `Driver.hs` contains the `main` +function to run any example. Each other example file exports a specification +`spec` and a proof scheme `scheme`. You can change the example being run just +by changing one *import* directive in `Driver.hs`. + +These examples include : + +* `Incr.hs` : a straightforward example in the style of the previous one. +* `Grey.hs` : an example where two different implementations of a periodical + counter are shown to be equivalent. +* `BoyerMoore.hs` : a certified version of the majority vote algorithm + introduced in the Copilot tutorial. +* `SerialBoyerMoore.hs` : a *serial* version of the first step of the *Boyer + Moore algorithm*, where a new element is added to the list and the majority + candidate is updated at each clock tick. See the section *Limitations related + to the SMT solvers* for an analysis of this example. + +## Technical details + +### An introduction to SMT-based model checking + +An introduction to the model-checking techniques used by *copilot-theorem* can be +found in the `doc` folder of this repository. It consists in a self sufficient +set of slides. You can find some additional readings in the *References* +section. + +### Architecture of copilot-kind + +#### An overview of the proving process + +Each prover first translates the Copilot specification into an intermediate +representation best suited for model checking. Two representations are +available : + +* The **IL** format : a Copilot program is translated into a list of + quantifier-free equations over integer sequences, implicitly universally + quantified by a free variable *n*. Each sequence roughly corresponds to a + stream. This format is the one used in G. Hagen's thesis [4]. The *light + prover* works with this format. + +* The **TransSys** format : a Copilot program is *flattened* and translated + into a *state transition system* [1]. Moreover, in order to keep some + structure in this representation, the variables of this system are grouped by + *nodes*, each node exporting and importing variables. The *Kind2 prover* uses + this format, which can be easily translated into the native format. + +For each of these formats, there is a folder in `src/Copilot/Theorem` which +contains at least +* `Spec.hs` where the format is defined +* `PrettyPrint.hs` for pretty printing (useful for debugging) +* `Translate.hs` where the translation process from `Core.Spec` is defined. + +These three formats share a simplified set of types and operators, defined +respectively in `Misc.Type` and `Misc.Operator`. + +##### An example + +The following program : + +```haskell +spec = do + prop "pos" (fib > 0) + + where + fib :: Stream Word64 + fib = [1, 1] ++ (fib + drop 1 fib) +``` + +can be translated into this IL specification : + +``` +SEQUENCES + s0 : Int + +MODEL INIT + s0[0] = 1 + s0[1] = 1 + +MODEL REC + s0[n + 2] = s0[n] + s0[n + 1] + +PROPERTIES + 'pos' : s0[n] > 0 +``` + +or this modular transition system : + +``` +NODE 's0' DEPENDS ON [] +DEFINES + out : Int = + 1 -> pre out.1 + out.1 : Int = + 1 -> pre out.2 + out.2 : Int = + (out) + (out.1) + +NODE 'prop-pos' DEPENDS ON [s0] +IMPORTS + (s0 : out) as 's0.out' + (s0 : out.1) as 's0.out.1' + (s0 : out.2) as 's0.out.2' +DEFINES + out : Bool = + (s0.out) > (0) + +NODE 'top' DEPENDS ON [prop-pos, s0] +IMPORTS + (prop-pos : out) as 'pos' + (s0 : out) as 's0.out' + (s0 : out.1) as 's0.out.1' + (s0 : out.2) as 's0.out.2' + +PROPS +'pos' is (top : pos) + +``` + +Note that the names of the streams are lost in the Copilot *reification +process* [7] and so we have no way to keep them. + +#### Types + +In these three formats, GADTs are used to statically ensure a part of the +type-corectness of the specification, in the same spirit it is done in the +other Copilot libraries. *copilot-theorem* handles only three types which are +`Integer`, `Real` and `Bool` and which are handled by the SMTLib standard. +*copilot-theorem* works with *pure* reals and integers. Thus, it is unsafe in the +sense it ignores integer overflow problems and the loss of precision due to +floating point arithmetic. + +The rules of translation between Copilot types and *copilot-theorem* types are +defined in `Misc/Cast`. + +#### Operators + +The operators provided by `Misc.Operator` mostly consists in boolean +connectors, linear operators, equality and inequality operators. If other +operators are used in the Copilot program, they are handled using +non-determinism or uninterpreted functions. + +The file `CoreUtils/Operators` contains helper functions to translate Copilot +operators into *copilot-theorem* operators. + + +#### The Light prover + +As said in the tutorial, the *light prover* is a simple tool implementing the +basic *k-induction* algorithm [1]. The `Light` directory contains three files : + +* `Prover.hs` : the prover and the *k-induction* algorithm are implemented in + this file. +* `SMT.hs` contains some functions to interact with the Yices SMT provers. +* `SMTLib.hs` is a set of functions to output SMTLib directives. It uses the + `Misc.SExpr` module to deal with S-expressions. + +The code is both concise and simple and should be worth a look. + +The prover first translates the copilot specification into the *IL* format. +This translation is implemented in `IL.Translate`. It is straightforward as the +*IL* format does not differ a lot from the *copilot core* format. This is the +case because the reification process has transformed the copilot program such +that the `++` operator only occurs at the top of a stream definition. +Therefore, each stream definition directly gives us a recurrence equation and +initial conditions for the associated sequence. + +The translation process mostly : + +* onverts the types and operators, using uninterpreted functions to handle + non-linear operators and external functions. +* creates a sequence for each stream, local stream ands external stream. + +The reader is invited to use the *light prover* on the examples with `debugMode += true`, in order to have a look at the SMTLib code produced. For instance, if +we check the property `"pos"` on the previous example involving the Fibonacci +sequence, we get : + +``` + (set-logic QF_UFLIA) + (declare-fun n () Int) + (declare-fun s0 (Int) Int) + (assert (= (s0 (+ n 2)) (+ (s0 (+ n 0)) (s0 (+ n 1))))) + (assert (= (s0 (+ n 3)) (+ (s0 (+ n 1)) (s0 (+ n 2))))) + (assert (> (s0 (+ n 0)) 0)) + (push 1) + (assert (or false (not (> (s0 (+ n 1)) 0)))) + (check-sat) + (pop 1) + (assert (= (s0 (+ n 4)) (+ (s0 (+ n 2)) (s0 (+ n 3))))) + (assert (> (s0 (+ n 1)) 0)) + (push 1) + (assert (or false (not (> (s0 (+ n 2)) 0)))) + (check-sat) +unsat + (pop 1) +``` + +Here, we just kept the outputs related to the `` psolver, which is the +solver trying to prove the *continuation step*. + +You can see that the SMT solver is used in an incremental way (`push` and `pop` +instructions), so we don't need to restart it at each step of the algorithm +(see [2]). + + +#### The Kind2 prover + +The *Kind2 prover* first translates the copilot specification into a *modular +transition system*. Then, a chain of transformations is applied to this system +(for instance, in order to remove dependency cycles among nodes). After this, +the system is translated into the *Kind2 native format* and the `kind2` +executable is launched. The following sections will bring more details about +this process. + +##### Modular transition systems + +Let's look at the definition of a *modular transition systems*, in the +`TransSys.Spec` module : + +```haskell +type NodeId = String +type PropId = String + +data Spec = Spec + { specNodes :: [Node] + , specTopNodeId :: NodeId + , specProps :: Map PropId ExtVar } + +data Node = Node + { nodeId :: NodeId + , nodeDependencies :: [NodeId] + , nodeLocalVars :: Map Var LVarDescr + , nodeImportedVars :: Bimap Var ExtVar + , nodeConstrs :: [Expr Bool] } + +data Var = Var {varName :: String} + deriving (Eq, Show, Ord) + +data ExtVar = ExtVar {extVarNode :: NodeId, extVarLocalPart :: Var } + deriving (Eq, Ord) + +data VarDescr = forall t . VarDescr + { varType :: Type t + , varDef :: VarDef t } + +data VarDef t = + Pre t Var + | Expr (Expr t) + | Constrs [Expr Bool] + +data Expr t where + Const :: Type t -> t -> Expr t + Ite :: Type t -> Expr Bool -> Expr t -> Expr t -> Expr t + Op1 :: Type t -> Op1 x t -> Expr x -> Expr t + Op2 :: Type t -> Op2 x y t -> Expr x -> Expr y -> Expr t + VarE :: Type t -> Var -> Expr t +``` + +A transition system (`Spec` type) is mostly made of a list of nodes. A *node* +is just a set of variables living in a local namespace and corresponding to the +`Var` type. The `ExtVar` type is used to identify a variable in the global +namespace by specifying both a node name and a variable. A node contains two +types of variables : + +* Some variables imported from other nodes. The structure `nodeImportedVars` + binds each imported variable to its local name. The set of nodes from which a + node imports some variables is stored in the `nodeDependencies` field. + +* Some locally defined variables contained in the `nodeLocalVars` field. Such a + variable can be + - Defined as the previous value of another variable (`Pre` constructor of + `VarDef`) + - Defined by an expression involving other variables (`Expr` constructor) + - Defined implicitly by a set of constraints (`Constrs` constructor) + +##### The translation process + +First, a copilot specification is translated into a modular transition system. +This process is defined in the `TransSys.Translate` module. Each stream is +associated to a node. The most significant task of this translation process is +to *flatten* the copilot specification so the value of all streams at time *n* +only depends on the values of all the streams at time *n - 1*, which is not the +case in the `Fib` example shown earlier. This is done by a simple program +transformation which turns this : + +```haskell +fib = [1, 1] ++ (fib + drop 1 fib) +``` +into this : + +```haskell +fib0 = [1] ++ fib1 +fib1 = [1] ++ (fib1 + fib0) +``` + +and then into the node + +``` +NODE 'fib' DEPENDS ON [] +DEFINES + out : Int = + 1 -> pre out.1 + out.1 : Int = + 1 -> pre out.2 + out.2 : Int = + (out) + (out.1) +``` + +Once again, this flattening process is made easier by the fact that the `++` +operator only occurs leftmost in a stream definition after the reification +process. + +##### Some transformations over modular transition systems + +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. + +This function relies on the `mergeNodes :: [NodeId] -> Spec -> Spec` function +which signature is self-explicit. The latter solves name conflicts by using the +`Misc.Renaming` monad. Some code complexity has been added so the variable +names remains 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 +limitations are organized in two categories : the limitations related to the +Copilot language itself and its implementation, and the limitations related to +the model-checking techniques we are using. + +#### Limitations related to Copilot implementation + +The reification process used to build the `Core.Spec` object looses many +informations about the structure of the original Copilot program. In fact, a +stream is kept in the reified program only if it is recursively defined. +Otherwise, all its occurences will be inlined. Moreover, let's look at the +`intCounter` function defined in the example `Grey.hs` : + +```haskell +intCounter :: Stream Bool -> Stream Word64 +intCounter reset = time + where + time = if reset then 0 + else [0] ++ if time == 3 then 0 else time + 1 +``` + +If *n* counters are created with this function, the same code will be inlined +*n* times and the structure of the original code will be lost. + +There are many problems with this : + +* It makes some optimizations of the model-checking based on a static analysis + of the program more difficult (for instance *structural abstraction* - see + [2]). +* It makes the inputs given to the SMT solvers larger and repetitive. + +We can't rewrite the Copilot reification process in order to avoid these +inconvenients as these informations are lost by GHC itself before it occurs. +The only solution we can see would be to use *Template Haskell* to generate +automatically some structural annotations, which might not be worth the dirt +introduced. + +#### Limitations related to the model-checking techniques used + +##### Limitations of the IC3 algorithm + +The IC3 algorithm was shown to be a very powerful tool for hardware +certification. However, the problems encountered when verifying softwares are +much more complex. For now, very few non-inductive properties can be proved by +*Kind2* when basic integer arithmetic is involved. + +The critical point of the IC3 algorithm is the counterexample generalization +and the lemma tightening parts of it. When encountering a *counterexample to +the inductiveness* (CTI) for a property, these techniques are used to find a +lemma discarding it which is general enough so that all CTIs can be discarded +in a finite number of steps. + +The lemmas found by the current version fo *Kind2* are often too weak. Some +suggestions to enhance this are presented in [1]. We hope some progress will be +made in this area in a near future. + +A workaround to this problem would be to write kind of an interactive mode +where the user is invited to provide some additional lemmas when automatic +techniques fail. Another solution would be to make the properties being checked +quasi-inductive by hand. In this case, *copilot-theorem* is still a useful tool +(especially for finding bugs) but the verification of a program can be long and +requires a high level of technicity. + +##### Limitations related to the SMT solvers + +The use of SMT solvers introduces two kind of limitations : + +1. We are limited by the computing power needed by the SMT solvers +2. SMT solvers can't handle quantifiers efficiently + +Let's consider the first point. SMT solving is costly and its performances are +sometimes unpredictable. For instance, when running the `SerialBoyerMoore` +example with the *light prover*, Yices2 does not terminate. However, the *z3* +SMT solver used by *Kind2* solves the problem instantaneously. Note that this +performance gap is not due to the use of the IC3 algorithm because the property +to check is inductive. It could be related to the fact the SMT problem produced +by the *light prover* uses uninterpreted functions for encoding streams instead +of simple integer variables, which is the case when the copilot program is +translated into a transition system. However, this wouldn't explain why the +*light prover* still terminates instantaneously on the `BoyerMoore` example, +which seems not simpler by far. + +The second point keeps you from expressing or proving some properties +universally quantified over a stream or a constant. Sometimes, this is still +possible. For instance, in the `Grey` example, as we check a property like +`intCounter reset == greyCounter reset` with `reset` an external stream +(therefore totally unconstrained), we kind of show a universally quantified +property. This fact could be used to enhance the proof scheme system (see the +*Future work* section). However, this trick is not always possible. For +instance, in the `SerialBoyerMoore` example, the property being checked should +be quantified over all integer constants. Here, we can't just introduce an +arbitrary constant stream because it is the quantified property which is +inductive and not the property specialized for a given constant stream. That's +why we have no other solution than replacing universal quantification by +*bounded* universal quantification by assuming all the elements of the input +stream are in the finite list `allowed` and using the function `forAllCst` +defined in `Copilot.Kind.Lib` : + +```haskell +conj :: [Stream Bool] -> Stream Bool +conj = foldl (&&) true + +forAllCst ::(Typed a) => [a] -> (Stream a -> Stream Bool) -> Stream Bool +forAllCst l f = conj $ map (f . constant) l +``` + +However, this solution isn't completely satisfying because the size of the +property generated is proportionnal to the cardinal of `allowed`. + +#### Some scalability issues + +A standard way to prove large programs is to rely on its logical structure by +writing a specification for each of its functions. This very natural approach +is hard to follow in our case because of + +* The difficulty to deal with universal quantification. +* The lack of *true* functions in Copilot : the latter offers metaprogramming + facilities but no concept of functions like *Lustre* does with its *nodes*). +* The inlining policy of the reification process. This point is related to the + previous one. + +Once again, *copilot-theorem* is still a very useful tool, especially for +debugging purposes. However, we don't think it is adapted to write and check a +complete specification for large scale programs. + +## Future work + +### Missing features in the Kind2 prover + +These features are not currently provided due to the lack of important features +in the Kind2 SMT solver. + +#### Counterexamples displaying + +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 counterexamples displaying in *copilot-theorem*. For +this, we recommend to keep some informations 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 + +Non-linear Copilot operators and external functions are poorly handled because +of the lack of support of uninterpreted functions in the Kind2 native format. A +good way to handle these would be to use uninterpreted functions. With this +solution, properties like +```haskell +2 * sin x + 1 <= 3 +``` +with `x` any stream can't be proven but at least the following can be proved +```haskell +let y = x in sin x == sin y +``` +Currently, the *Kind2 prover* fail with the last example, as the results of +unknown functions are turned into fresh unconstrained variables. + +### Simple extensions + +The following extensions would be really simple to implement given the current +architecture of Kind2. + ++ If inductive proving of a property fails, giving the user a concrete CTI + (*Counterexample To The Inductiveness*, see the [1]). + ++ Use Template Haskell to declare automatically some observers with the same + names used in the original program. + +### Refactoring suggestions + ++ Implement a cleaner way to deal with arbitrary streams and arbitrary + constants by extending the `Copilot.Core.Expr type`. See the + `Copilot.Kind.Lib` module to observe how inelegant the current solution is. + ++ Use `Cnub` as an intermediary step in the translation from `Core.Spec` to + `IL.Spec` and `TransSys.Spec`. + +### More advanced enhancements + ++ Enhance the proof scheme system such that when proving a property depending + on an arbitrary stream, it is possible to assume some specialized versions of + this property for given values of the arbitrary stream. In other words, + implementing a basic way to deal with universal quantification. + ++ It could be useful to extend the Copilot language in a way it is possible to + use annotations inside the Copilot code. For instance, we could + + - Declare assumptions and invariants next to the associated code instead of + gathering all properties in a single place. + - Declare a frequent code pattern which should be factorized in the + transition problem (see the section about Copilot limitations) + +## FAQ + +### Why does the light prover not deliver counterexamples ? + +The problem is the light prover is using uninterpreted functions to represent +streams and Yices2 can't give you values for uninterpreted functions when you +ask it for a valid assignment. Maybe we could get better performances and +easily counterexample display if we rewrite the *light prover* so that it works +with *transition systems* instead of *IL*. + +### Why does the code related to transition systems look so complex ? + +It is true 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 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 + copilot doesn't handle functions or parametrized 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 + input file with some basic static analysis by producing a dependency graph + between variables. +* For now, the *Kind2* model-checker ignores these structure informations. + +However, the current code offers some nice transformation tools (node merging, +`Renaming` monad...) which could be useful if you intend to write a tool for +simplifying or factorizing transition systems. Moreover, it becomes easier to +write local transformations on transition systems as name conflicts can be +avoided more easily when introducing more variables, as there is one namespace +per node. + +## References + +1. *An insight into An insight into SMT-based model checking techniques for + formal software verification of synchronous dataflow programs*, talk, + Jonathan Laurent (see the `doc` folder of this repository) + +2. *Scaling up the formal verification of Lustre programs with SMT-based + techniques*, G. Hagen, C. Tinelli + +3. *SMT-based Unbounded Model Checking with IC3 and Approximate Quantifier + Elimination*, C. Sticksel, C. Tinelli + +4. *Verifying safety properties of Lustre programs : an SMT-based approach*, + PhD thesis, G. Hagen + +5. *Understanding IC3*, Aaron R. Bradley + +6. *IC3: Where Monolithic and Incremental Meet*, F. Somenzi, A.R. Bradley + +7. *Copilot: Monitoring Embedded Systems*, L. Pike, N. Wegmann, S. Niller diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal new file mode 100644 --- /dev/null +++ b/copilot-theorem.cabal @@ -0,0 +1,87 @@ +cabal-version : >= 1.10 +name : copilot-theorem +synopsis: k-induction for Copilot. +description: + + Some tools to prove properties on Copilot programs with k-induction model + checking. + +version : 2.2.0 +license : BSD3 +license-file : LICENSE +maintainer : jonathan.laurent@ens.fr +stability : Experimental +category : Language, Embedded +build-type : Simple +extra-source-files : README.md + +author : Jonathan Laurent + +library + default-language : Haskell2010 + hs-source-dirs : src + + ghc-options : -Wall -fwarn-tabs + -fno-warn-name-shadowing + -fno-warn-unused-binds + -fno-warn-missing-signatures + -fcontext-stack=100 + + build-depends : base >= 4.0 && < 5 + , copilot-core == 2.2.0 + , mtl + , containers + , pretty + , process + , directory + , parsec + , data-default + , bimap + , xml + , random + , transformers + , smtlib2 >= 0.3 + , ansi-terminal + + exposed-modules : Copilot.Theorem + , Copilot.Theorem.Prove + , Copilot.Theorem.Kind2 + , Copilot.Theorem.Prover.SMT + , Copilot.Theorem.Prover.Z3 + , Copilot.Theorem.Kind2.Prover + + other-modules : Copilot.Theorem.Tactics + + , Copilot.Theorem.IL + , Copilot.Theorem.IL.PrettyPrint + , Copilot.Theorem.IL.Spec + , Copilot.Theorem.IL.Translate + , Copilot.Theorem.IL.Transform + + , Copilot.Theorem.Kind2.AST + , Copilot.Theorem.Kind2.Output + , Copilot.Theorem.Kind2.PrettyPrint + , Copilot.Theorem.Kind2.Translate + + , Copilot.Theorem.Prover.SMTIO + , Copilot.Theorem.Prover.SMTLib + , Copilot.Theorem.Prover.TPTP + , Copilot.Theorem.Prover.Backend + + , Copilot.Theorem.Misc.Error + , Copilot.Theorem.Misc.SExpr + , Copilot.Theorem.Misc.Utils + + , Copilot.Theorem.TransSys + , Copilot.Theorem.TransSys.Cast + , Copilot.Theorem.TransSys.PrettyPrint + , Copilot.Theorem.TransSys.Renaming + , Copilot.Theorem.TransSys.Spec + , Copilot.Theorem.TransSys.Transform + , Copilot.Theorem.TransSys.Translate + , Copilot.Theorem.TransSys.Invariants + , Copilot.Theorem.TransSys.Operators + , Copilot.Theorem.TransSys.Type + + + diff --git a/src/Copilot/Theorem.hs b/src/Copilot/Theorem.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem.hs @@ -0,0 +1,13 @@ +-------------------------------------------------------------------------------- + +module Copilot.Theorem + ( module X + , Proof + , PropId, PropRef + , Universal, Existential + ) where + +import Copilot.Theorem.Tactics as X +import Copilot.Theorem.Prove + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/IL.hs b/src/Copilot/Theorem/IL.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/IL.hs @@ -0,0 +1,10 @@ +-------------------------------------------------------------------------------- + +module Copilot.Theorem.IL (module X) where + +import Copilot.Theorem.IL.Spec as X +import Copilot.Theorem.IL.Translate as X +import Copilot.Theorem.IL.Transform as X +import Copilot.Theorem.IL.PrettyPrint as X + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/IL/PrettyPrint.hs b/src/Copilot/Theorem/IL/PrettyPrint.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/IL/PrettyPrint.hs @@ -0,0 +1,84 @@ +--------------------------------------------------------------------------------- + +{-# LANGUAGE NamedFieldPuns, GADTs #-} + +module Copilot.Theorem.IL.PrettyPrint (prettyPrint, printConstraint) where + +import Copilot.Theorem.IL.Spec +import Text.PrettyPrint.HughesPJ +import qualified Data.Map as Map + +-------------------------------------------------------------------------------- + +prettyPrint :: IL -> String +prettyPrint = render . ppSpec + +printConstraint :: Expr -> String +printConstraint = render . ppExpr + +indent = nest 4 +emptyLine = text "" + +ppSpec :: IL -> Doc +ppSpec (IL { modelInit, modelRec, properties }) = + text "MODEL INIT" + $$ indent (foldr (($$) . ppExpr) empty modelInit) $$ emptyLine + $$ text "MODEL REC" + $$ indent (foldr (($$) . ppExpr) empty modelRec) $$ emptyLine + $$ text "PROPERTIES" + $$ indent (Map.foldrWithKey (\k -> ($$) . ppProp k) + empty properties ) + +ppProp :: PropId -> ([Expr], Expr) -> Doc +ppProp id (as, c) = (foldr (($$) . ppExpr) empty as) + $$ quotes (text id) <+> colon <+> ppExpr c + +ppSeqDescr :: SeqDescr -> Doc +ppSeqDescr (SeqDescr id ty) = text id <+> colon <+> ppType ty + +ppVarDescr :: VarDescr -> Doc +ppVarDescr (VarDescr id ret args) = + text id + <+> colon + <+> (hsep . punctuate (space <> text "->" <> space) $ map ppType args) + <+> text "->" + <+> ppType ret + +ppType :: Type -> Doc +ppType = text . show + +ppExpr :: Expr -> Doc +ppExpr (ConstB v) = text . show $ v +ppExpr (ConstR v) = text . show $ v +ppExpr (ConstI _ v) = text . show $ v + +ppExpr (Ite _ c e1 e2) = + text "if" <+> ppExpr c + <+> text "then" <+> ppExpr e1 + <+> text "else" <+> ppExpr e2 + +ppExpr (Op1 _ op e) = ppOp1 op <+> ppExpr e + +ppExpr (Op2 _ op e1 e2) = + ppExpr e1 <+> ppOp2 op <+> ppExpr e2 + +ppExpr (SVal _ s i) = text s <> brackets (ppSeqIndex i) + +ppExpr (FunApp _ name args) = + text name <> parens (hsep . punctuate (comma <> space) $ map ppExpr args) + +ppSeqIndex :: SeqIndex -> Doc +ppSeqIndex (Var i) + | i == 0 = text "n" + | i < 0 = text "n" <+> text "-" <+> integer (-i) + | otherwise = text "n" <+> text "+" <+> integer i + +ppSeqIndex (Fixed i) = integer i + +ppOp1 :: Op1 -> Doc +ppOp1 = text . show + +ppOp2 :: Op2 -> Doc +ppOp2 = text . show + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/IL/Spec.hs b/src/Copilot/Theorem/IL/Spec.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/IL/Spec.hs @@ -0,0 +1,177 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE ExistentialQuantification, GADTs, LambdaCase #-} + +module Copilot.Theorem.IL.Spec + ( Type (..) + , Op1 (..) + , Op2 (..) + , SeqId + , SeqIndex (..) + , SeqDescr (..) + , VarDescr (..) + , Expr (..) + , IL (..) + , PropId + , typeOf + , _n_ + , _n_plus + , evalAt + ) where + +import Data.Map (Map) +import Data.Function (on) + +-------------------------------------------------------------------------------- + +type SeqId = String + +data SeqIndex = Fixed Integer | Var Integer + deriving (Eq, Ord, Show) + +data Type = Bool | Real + | SBV8 | SBV16 | SBV32 | SBV64 + | BV8 | BV16 | BV32 | BV64 + deriving (Eq, Ord) + +instance Show Type where + show = \case + Bool -> "Bool" + Real -> "Real" + SBV8 -> "SBV8" + SBV16 -> "SBV16" + SBV32 -> "SBV32" + SBV64 -> "SBV64" + BV8 -> "BV8" + BV16 -> "BV16" + BV32 -> "BV32" + BV64 -> "BV64" + +data Expr + = ConstB Bool + | ConstR Double + | ConstI Type Integer + | Ite Type Expr Expr Expr + | Op1 Type Op1 Expr + | Op2 Type Op2 Expr Expr + | SVal Type SeqId SeqIndex + | FunApp Type String [Expr] + deriving (Eq, Ord, Show) + +-------------------------------------------------------------------------------- + +data VarDescr = VarDescr + { varName :: String + , varType :: Type + , args :: [Type] + } + +instance Eq VarDescr where + (==) = (==) `on` varName + +instance Ord VarDescr where + compare = compare `on` varName + +-------------------------------------------------------------------------------- + +type PropId = String + +data SeqDescr = SeqDescr + { seqId :: SeqId + , seqType :: Type + } + +data IL = IL + { modelInit :: [Expr] + , modelRec :: [Expr] + , properties :: Map PropId ([Expr], Expr) + , inductive :: Bool + } + +-------------------------------------------------------------------------------- + +data Op1 = Not | Neg | Abs | Exp | Sqrt | Log | Sin | Tan | Cos | Asin | Atan + | Acos | Sinh | Tanh | Cosh | Asinh | Atanh | Acosh + deriving (Eq, Ord) + +data Op2 = Eq | And | Or | Le | Lt | Ge | Gt | Add | Sub | Mul | Mod | Fdiv | Pow + deriving (Eq, Ord) + +------------------------------------------------------------------------------- + +instance Show Op1 where + show op = case op of + Neg -> "-" + Not -> "not" + Abs -> "abs" + Exp -> "exp" + Sqrt -> "sqrt" + Log -> "log" + Sin -> "sin" + Tan -> "tan" + Cos -> "cos" + Asin -> "asin" + Atan -> "atan" + Acos -> "acos" + Sinh -> "sinh" + Tanh -> "tanh" + Cosh -> "cosh" + Asinh -> "asinh" + Atanh -> "atanh" + Acosh -> "acosh" + +instance Show Op2 where + show op = case op of + And -> "and" + Or -> "or" + + Add -> "+" + Sub -> "-" + Mul -> "*" + + Mod -> "mod" + + Fdiv -> "/" + + Pow -> "^" + + Eq -> "=" + + Le -> "<=" + Ge -> ">=" + Lt -> "<" + Gt -> ">" + +------------------------------------------------------------------------------- + +typeOf :: Expr -> Type +typeOf e = case e of + ConstB _ -> Bool + ConstR _ -> Real + ConstI t _ -> t + Ite t _ _ _ -> t + Op1 t _ _ -> t + Op2 t _ _ _ -> t + SVal t _ _ -> t + FunApp t _ _ -> t + +_n_ :: SeqIndex +_n_ = Var 0 + +_n_plus :: (Integral a) => a -> SeqIndex +_n_plus d = Var (toInteger d) + +evalAt :: SeqIndex -> Expr -> Expr +evalAt _ e@(ConstB _) = e +evalAt _ e@(ConstR _) = e +evalAt _ e@(ConstI _ _) = e +evalAt i (Op1 t op e) = Op1 t op (evalAt i e) +evalAt i (Op2 t op e1 e2) = Op2 t op (evalAt i e1) (evalAt i e2) +evalAt i (Ite t c e1 e2) = Ite t (evalAt i c) (evalAt i e1) (evalAt i e2) +evalAt i (FunApp t name args) = FunApp t name $ map (\e -> evalAt i e) args + +evalAt _ e@(SVal _ _ (Fixed _)) = e +evalAt (Fixed n) (SVal t s (Var d)) = SVal t s (Fixed $ n + d) +evalAt (Var k) (SVal t s (Var d)) = SVal t s (Var $ k + d) + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/IL/Transform.hs b/src/Copilot/Theorem/IL/Transform.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/IL/Transform.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE LambdaCase #-} + +module Copilot.Theorem.IL.Transform ( bsimpl ) where + +import Copilot.Theorem.IL.Spec + +-- | A transformation intended to remove boolean literals. +bsimpl :: Expr -> Expr +bsimpl = until (\x -> bsimpl' x == x) bsimpl' + where + bsimpl' = \case + Ite _ (ConstB True) e _ -> bsimpl' e + Ite _ (ConstB False) _ e -> bsimpl' e + Ite t c e1 e2 -> Ite t (bsimpl' c) (bsimpl' e1) (bsimpl' e2) + + Op1 _ Not (Op1 _ Not e) -> bsimpl' e + Op1 _ Not (ConstB True) -> ConstB False + Op1 _ Not (ConstB False) -> ConstB True + Op1 t o e -> Op1 t o (bsimpl' e) + + Op2 _ Or e (ConstB False) -> bsimpl' e + Op2 _ Or (ConstB False) e -> bsimpl' e + Op2 _ Or _ (ConstB True) -> ConstB True + Op2 _ Or (ConstB True) _ -> ConstB True + + Op2 _ And _ (ConstB False) -> ConstB False + Op2 _ And (ConstB False) _ -> ConstB False + Op2 _ And e (ConstB True) -> bsimpl' e + Op2 _ And (ConstB True) e -> bsimpl' e + + Op2 _ Eq e (ConstB False) -> bsimpl' (Op1 Bool Not e) + Op2 _ Eq (ConstB False) e -> bsimpl' (Op1 Bool Not e) + Op2 _ Eq e (ConstB True) -> bsimpl' e + Op2 _ Eq (ConstB True) e -> bsimpl' e + + Op2 t o e1 e2 -> Op2 t o (bsimpl' e1) (bsimpl' e2) + + FunApp t f args -> FunApp t f (map bsimpl' args) + + e -> e + diff --git a/src/Copilot/Theorem/IL/Translate.hs b/src/Copilot/Theorem/IL/Translate.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/IL/Translate.hs @@ -0,0 +1,324 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE RankNTypes, NamedFieldPuns, ScopedTypeVariables, GADTs, + LambdaCase #-} + +module Copilot.Theorem.IL.Translate ( translate ) where + +import Copilot.Theorem.IL.Spec + +import qualified Copilot.Core as C + +import qualified Data.Map.Strict as Map + +import Control.Applicative ((<$>), (<*)) +import Control.Monad.State + +import Data.Char +import Data.List (find) + +import Text.Printf + +import GHC.Float (float2Double) + +-------------------------------------------------------------------------------- + +-- 'nc' stands for naming convention. +ncSeq :: C.Id -> SeqId +ncSeq = printf "s%d" + +-- We assume all local variables have distinct names whatever their scopes. +ncLocal :: C.Name -> SeqId +ncLocal s = "l" ++ dropWhile (not . isNumber) s + +ncExternVar :: C.Name -> SeqId +ncExternVar n = "ext_" ++ n + +ncExternFun :: C.Name -> SeqId +ncExternFun n = "_" ++ n + +ncUnhandledOp :: String -> String +ncUnhandledOp = id + +ncMux :: Integer -> SeqId +ncMux n = "mux" ++ show n + +-------------------------------------------------------------------------------- + +-- | Translates a Copilot specification to an IL specification + +translate :: C.Spec -> IL +translate (C.Spec {C.specStreams, C.specProperties}) = runTrans $ do + + let modelInit = concatMap streamInit specStreams + + mainConstraints <- mapM streamRec specStreams + + localConstraints <- popLocalConstraints + properties <- Map.fromList <$> + forM specProperties + (\(C.Property {C.propertyName, C.propertyExpr}) -> do + e' <- expr propertyExpr + propConds <- popLocalConstraints + return (propertyName, (propConds, e'))) + + return IL + { modelInit + , modelRec = mainConstraints ++ localConstraints + , properties + , inductive = not $ null specStreams + } + +bound :: Expr -> C.Type a -> Trans () +bound s t = case t of + C.Int8 -> bound' C.Int8 + C.Int16 -> bound' C.Int16 + C.Int32 -> bound' C.Int32 + C.Int64 -> bound' C.Int64 + C.Word8 -> bound' C.Word8 + C.Word16 -> bound' C.Word16 + C.Word32 -> bound' C.Word32 + C.Word64 -> bound' C.Word64 + _ -> return () + where bound' :: (Bounded a, Integral a) => C.Type a -> Trans () + bound' t = localConstraint (Op2 Bool And + (Op2 Bool Le (trConst t minBound) s) + (Op2 Bool Ge (trConst t maxBound) s)) + +streamInit :: C.Stream -> [Expr] +streamInit (C.Stream { C.streamId = id + , C.streamBuffer = b :: [val] + , C.streamExprType = t }) = + zipWith initConstraint [0..] b + where initConstraint :: Integer -> val -> Expr + initConstraint p v = Op2 Bool Eq + (SVal (trType t) (ncSeq id) (Fixed p)) + $ trConst t v + +streamRec :: C.Stream -> Trans Expr +streamRec (C.Stream { C.streamId = id + , C.streamExpr = e + , C.streamBuffer = b + , C.streamExprType = t }) + = do + let s = SVal (trType t) (ncSeq id) (_n_plus $ length b) + bound s t + e' <- expr e + return $ Op2 Bool Eq s e' + +-------------------------------------------------------------------------------- + +expr :: C.Expr a -> Trans Expr + +expr (C.Const t v) = return $ trConst t v + +expr (C.Label _ _ e) = expr e + +expr (C.Drop t k id) = return $ SVal (trType t) (ncSeq id) (_n_plus k) + +expr (C.Local ta _ name ea eb) = do + ea' <- expr ea + localConstraint (Op2 Bool Eq (SVal (trType ta) (ncLocal name) _n_) ea') + expr eb + +expr (C.Var t name) = return $ SVal (trType t) (ncLocal name) _n_ + +expr (C.ExternVar t name _) = bound s t >> return s + where s = SVal (trType t) (ncExternVar name) _n_ + +expr (C.ExternFun t name args _ _) = do + args' <- mapM trArg args + let s = FunApp (trType t) (ncExternFun name) args' + bound s t + return s + where trArg (C.UExpr {C.uExprExpr}) = expr uExprExpr + +-- Arrays and functions are treated the same way +expr (C.ExternArray ta tb name _ ind _ _) = + expr (C.ExternFun tb name [C.UExpr ta ind] Nothing Nothing) + +expr (C.Op1 (C.Sign ta) e) = case ta of + C.Int8 -> trSign ta e + C.Int16 -> trSign ta e + C.Int32 -> trSign ta e + C.Int64 -> trSign ta e + C.Float -> trSign ta e + C.Double -> trSign ta e + _ -> expr $ C.Const ta 1 + where trSign :: (Ord a, Num a) => C.Type a -> C.Expr a -> Trans Expr + trSign ta e = + expr (C.Op3 (C.Mux ta) + (C.Op2 (C.Lt ta) e (C.Const ta 0)) + (C.Const ta (-1)) + (C.Op3 (C.Mux ta) + (C.Op2 (C.Gt ta) e (C.Const ta 0)) + (C.Const ta 1) + (C.Const ta 0))) +expr (C.Op1 (C.Sqrt _) e) = do + e' <- expr e + return $ Op2 Real Pow e' (ConstR 0.5) +expr (C.Op1 (C.Cast _ _) e) = expr e +expr (C.Op1 op e) = do + e' <- expr e + return $ Op1 t' op' e' + where (op', t') = trOp1 op + +expr (C.Op2 (C.Ne t) e1 e2) = do + e1' <- expr e1 + e2' <- expr e2 + return $ Op1 Bool Not (Op2 t' Eq e1' e2') + where t' = trType t + +expr (C.Op2 op e1 e2) = do + e1' <- expr e1 + e2' <- expr e2 + return $ Op2 t' op' e1' e2' + where (op', t') = trOp2 op + +expr (C.Op3 (C.Mux t) cond e1 e2) = do + cond' <- expr cond + e1' <- expr e1 + e2' <- expr e2 + newMux cond' (trType t) e1' e2' + +trConst :: C.Type a -> a -> Expr +trConst t v = case t of + C.Bool -> ConstB v + C.Float -> negifyR (float2Double v) + C.Double -> negifyR v + t@C.Int8 -> negifyI v (trType t) + t@C.Int16 -> negifyI v (trType t) + t@C.Int32 -> negifyI v (trType t) + t@C.Int64 -> negifyI v (trType t) + t@C.Word8 -> negifyI v (trType t) + t@C.Word16 -> negifyI v (trType t) + t@C.Word32 -> negifyI v (trType t) + t@C.Word64 -> negifyI v (trType t) + where negifyR :: Double -> Expr + negifyR v + | v >= 0 = ConstR v + | otherwise = Op1 Real Neg $ ConstR $ negate $ v + negifyI :: Integral a => a -> Type -> Expr + negifyI v t + | v >= 0 = ConstI t $ toInteger v + | otherwise = Op1 t Neg $ ConstI t $ negate $ toInteger v + +trOp1 :: C.Op1 a b -> (Op1, Type) +trOp1 = \case + C.Not -> (Not, Bool) + C.Abs t -> (Abs, trType t) + -- C.Sign t -> + -- C.Recip t -> + C.Exp t -> (Exp, trType t) + -- C.Sqrt t -> + C.Log t -> (Log, trType t) + C.Sin t -> (Sin, trType t) + C.Tan t -> (Tan, trType t) + C.Cos t -> (Cos, trType t) + C.Asin t -> (Asin, trType t) + C.Atan t -> (Atan, trType t) + C.Acos t -> (Acos, trType t) + C.Sinh t -> (Sinh, trType t) + C.Tanh t -> (Tanh, trType t) + C.Cosh t -> (Cosh, trType t) + C.Asinh t -> (Asinh, trType t) + C.Atanh t -> (Atanh, trType t) + C.Acosh t -> (Acosh, trType t) + -- C.BwNot t -> + -- C.Cast t -> + _ -> error "Unsupported unary operator in input." -- TODO(chathhorn) + +trOp2 :: C.Op2 a b c -> (Op2, Type) +trOp2 = \case + C.And -> (And, Bool) + C.Or -> (Or, Bool) + + C.Add t -> (Add, trType t) + C.Sub t -> (Sub, trType t) + C.Mul t -> (Mul, trType t) + + C.Mod t -> (Mod, trType t) + -- C.Div t -> + + C.Fdiv t -> (Fdiv, trType t) + + C.Pow t -> (Pow, trType t) + -- C.Logb t -> + + C.Eq t -> (Eq, Bool) + -- C.Ne t -> + + C.Le t -> (Le, trType t) + C.Ge t -> (Ge, trType t) + C.Lt t -> (Lt, trType t) + C.Gt t -> (Gt, trType t) + + -- C.BwAnd t -> + -- C.BwOr t -> + -- C.BwXor t -> + -- C.BwShiftL t _ -> + -- C.BwShiftR t _ -> + + _ -> error "Unsupported binary operator in input." -- TODO(chathhorn) + +trType :: C.Type a -> Type +trType = \case + C.Bool -> Bool + C.Int8 -> SBV8 + C.Int16 -> SBV16 + C.Int32 -> SBV32 + C.Int64 -> SBV64 + C.Word8 -> BV8 + C.Word16 -> BV16 + C.Word32 -> BV32 + C.Word64 -> BV64 + C.Float -> Real + C.Double -> Real + +-------------------------------------------------------------------------------- + +data TransST = TransST + { localConstraints :: [Expr] + , muxes :: [(Expr, (Expr, Type, Expr, Expr))] + , nextFresh :: Integer + } + +newMux :: Expr -> Type -> Expr -> Expr -> Trans Expr +newMux c t e1 e2 = do + ms <- muxes <$> get + case find ((==mux) . snd) ms of + Nothing -> do + f <- fresh + let v = SVal t (ncMux f) _n_ + modify $ \st -> st { muxes = (v, mux) : ms } + return v + Just (v, _) -> return v + where mux = (c, t, e1, e2) + +getMuxes :: Trans [Expr] +getMuxes = muxes <$> get >>= return . concat . (map toConstraints) + where toConstraints (v, (c, _, e1, e2)) = + [ Op2 Bool Or (Op1 Bool Not c) (Op2 Bool Eq v e1) + , Op2 Bool Or c (Op2 Bool Eq v e2) + ] + +type Trans = State TransST + +fresh :: Trans Integer +fresh = do + modify $ \st -> st {nextFresh = nextFresh st + 1} + nextFresh <$> get + +localConstraint :: Expr -> Trans () +localConstraint c = + modify $ \st -> st {localConstraints = c : localConstraints st} + +popLocalConstraints :: Trans [Expr] +popLocalConstraints = liftM2 (++) (localConstraints <$> get) getMuxes + <* (modify $ \st -> st {localConstraints = [], muxes = []}) + +runTrans :: Trans a -> a +runTrans m = evalState m $ TransST [] [] 0 + +-------------------------------------------------------------------------------- + diff --git a/src/Copilot/Theorem/Kind2.hs b/src/Copilot/Theorem/Kind2.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Kind2.hs @@ -0,0 +1,10 @@ +-------------------------------------------------------------------------------- + +module Copilot.Theorem.Kind2 (module X) where + +import Copilot.Theorem.Kind2.AST as X +import Copilot.Theorem.Kind2.Translate as X +import Copilot.Theorem.Kind2.PrettyPrint as X +import Copilot.Theorem.Kind2.Prover as X + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Kind2/AST.hs b/src/Copilot/Theorem/Kind2/AST.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Kind2/AST.hs @@ -0,0 +1,39 @@ +-------------------------------------------------------------------------------- + +module Copilot.Theorem.Kind2.AST where + +-------------------------------------------------------------------------------- + +data File = File + { filePreds :: [PredDef] + , fileProps :: [Prop] } + +data Prop = Prop + { propName :: String + , propTerm :: Term } + +data PredDef = PredDef + { predId :: String + , predStateVars :: [StateVarDef] + , predInit :: Term + , predTrans :: Term } + +data StateVarDef = StateVarDef + { varId :: String + , varType :: Type + , varFlags :: [StateVarFlag] } + +data Type = Int | Real | Bool + +data StateVarFlag = FConst + +data PredType = Init | Trans + +data Term = + ValueLiteral String + | PrimedStateVar String + | StateVar String + | FunApp String [Term] + | PredApp String PredType [Term] + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Kind2/Output.hs b/src/Copilot/Theorem/Kind2/Output.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Kind2/Output.hs @@ -0,0 +1,51 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE RankNTypes #-} + +module Copilot.Theorem.Kind2.Output (parseOutput) where + +import Text.XML.Light hiding (findChild) +import Copilot.Theorem.Prove as P +import Data.Maybe (fromJust) + +import qualified Copilot.Theorem.Misc.Error as Err + +-------------------------------------------------------------------------------- + +simpleName s = QName s Nothing Nothing + +parseOutput :: String -> String -> P.Output +parseOutput prop xml = fromJust $ do + root <- parseXMLDoc xml + case findAnswer . findPropTag $ root of + "valid" -> return (Output Valid []) + "invalid" -> return (Output Invalid []) + s -> err $ "Unrecognized status : " ++ s + + where + + searchForRuntimeError = undefined + + findPropTag root = + let rightElement elt = + qName (elName elt) == "Property" + && lookupAttr (simpleName "name") (elAttribs elt) + == Just prop + in case filterChildren rightElement root of + tag : _ -> tag + _ -> err $ "Tag for property " ++ prop ++ " 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" + + err :: forall a . String -> a + err msg = Err.fatal $ + "Parse error while reading the Kind2 XML output : \n" + ++ msg ++ "\n\n" ++ xml + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/src/Copilot/Theorem/Kind2/PrettyPrint.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Kind2/PrettyPrint.hs @@ -0,0 +1,69 @@ +-------------------------------------------------------------------------------- + +module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where + +import Copilot.Theorem.Misc.SExpr +import qualified Copilot.Theorem.Misc.SExpr as SExpr +import Copilot.Theorem.Kind2.AST + +import Data.List (intercalate) + +-------------------------------------------------------------------------------- + +type SSExpr = SExpr String + +kwPrime = "prime" + +-------------------------------------------------------------------------------- + +prettyPrint :: File -> String +prettyPrint = + intercalate "\n\n" + . map (SExpr.toString shouldIndent id) + . ppFile + +-- Defines the indentation policy of the S-Expressions +shouldIndent :: SSExpr -> Bool +shouldIndent (Atom _) = False +shouldIndent (List [Atom a, Atom _]) = a `notElem` [kwPrime] +shouldIndent _ = True + +-------------------------------------------------------------------------------- + +ppFile :: File -> [SSExpr] +ppFile (File preds props) = map ppPredDef preds ++ ppProps props + +ppProps :: [Prop] -> [SSExpr] +ppProps ps = [ node "check-prop" [ list $ map ppProp ps ] ] + +ppProp :: Prop -> SSExpr +ppProp (Prop n t) = list [atom n, ppTerm t] + +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] ] + +ppStateVarDef :: StateVarDef -> SSExpr +ppStateVarDef svd = + list [atom (varId svd), ppType (varType svd)] + +ppType :: Type -> SSExpr +ppType Int = atom "Int" +ppType Real = atom "Real" +ppType Bool = atom "Bool" + +ppTerm :: Term -> SSExpr +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/src/Copilot/Theorem/Kind2/Prover.hs b/src/Copilot/Theorem/Kind2/Prover.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Kind2/Prover.hs @@ -0,0 +1,72 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE LambdaCase #-} + +module Copilot.Theorem.Kind2.Prover + ( module Data.Default + , Options (..) + , kind2Prover + ) where + +import Copilot.Theorem.Prove +import Copilot.Theorem.Kind2.Output +import Copilot.Theorem.Kind2.PrettyPrint +import Copilot.Theorem.Kind2.Translate + +-- It seems [IO.openTempFile] doesn't work on Mac OSX +import System.IO hiding (openTempFile) +import Copilot.Theorem.Misc.Utils (openTempFile) + +import System.Process + +import System.Directory +import Data.Default + +import qualified Copilot.Theorem.TransSys as TS + +-------------------------------------------------------------------------------- + +data Options = Options + { bmcMax :: Int } + +instance Default Options where + def = Options { bmcMax = 0 } + +data ProverST = ProverST + { options :: Options + , transSys :: TS.TransSys } + +kind2Prover :: Options -> Prover +kind2Prover opts = Prover + { proverName = "Kind2" + , startProver = return . ProverST opts . TS.translate + , askProver = askKind2 + , closeProver = const $ return () } + +-------------------------------------------------------------------------------- + +kind2Prog = "kind2" +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 + + (tempName, tempHandle) <- openTempFile "." "out" "kind" + hPutStr tempHandle kind2Input + hClose tempHandle + + let kind2Options = + kind2BaseOptions ++ ["--bmc_max", show $ bmcMax opts, tempName] + + (_, output, _) <- readProcessWithExitCode kind2Prog kind2Options "" + + putStrLn kind2Input + + removeFile tempName + return $ parseOutput (head toCheck) output -- TODO support multiple toCheck props + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Kind2/Translate.hs b/src/Copilot/Theorem/Kind2/Translate.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Kind2/Translate.hs @@ -0,0 +1,212 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE RankNTypes, ViewPatterns, NamedFieldPuns, GADTs #-} + +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 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] + +-------------------------------------------------------------------------------- + +data Style = Inlined | Modular + +toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> K.File +toKind2 style assumptions checkedProps spec = + addAssumptions spec assumptions + $ trSpec (complete spec') predCallsGraph assumptions checkedProps + where predCallsGraph = specDependenciesGraph spec' + spec' = case style of + Inlined -> inline spec + Modular -> removeCycles spec + +trSpec :: TransSys -> DepGraph -> [PropId] -> [PropId] -> K.File +trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props + where preds = map (trNode spec predCallsGraph) (specNodes spec) + props = map trProp $ + filter ((`elem` checkedProps) . fst) $ + Map.toList (specProps spec) + +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 + + +addAssumptions :: TransSys -> [PropId] -> K.File -> K.File +addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) = + K.File (changeTail aux filePreds) fileProps + 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' } + + vars = + let bindings = nodeImportedVars (specTopNode spec) + toExtVar a = 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 + where + nodesMap = Map.fromList [(nodeId n, n) | n <- specNodes spec] + extVarType :: ExtVar -> K.Type + extVarType (ExtVar n v) = + case nodeLocalVars (nodesMap ! n) ! 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 +mkConj xs = K.FunApp "and" xs + +mkEquality :: K.Term -> K.Term -> K.Term +mkEquality t1 t2 = K.FunApp "=" [t1, t2] + +trVar :: Var -> K.Term +trVar v = K.StateVar (varName v) + +trPrimedVar :: Var -> K.Term +trPrimedVar v = K.PrimedStateVar (varName v) + +trConst :: Type t -> t -> K.Term +trConst Integer v = K.ValueLiteral (show v) +trConst Real v = K.ValueLiteral (show v) +trConst Bool True = K.ValueLiteral "true" +trConst Bool False = K.ValueLiteral "false" + +-------------------------------------------------------------------------------- + +initLocals :: Node -> [K.Term] +initLocals node = + concatMap f (Map.toList $ nodeLocalVars node) + where + f (v, VarDescr t def) = + case def of + Pre c _ -> [mkEquality (trVar v) (trConst t c)] + Expr e -> [mkEquality (trVar v) (trExpr False e)] + Constrs cs -> map (trExpr False) cs + + +transLocals :: Node -> [K.Term] +transLocals node = + concatMap f (Map.toList $ nodeLocalVars node) + where + f (v, VarDescr _ def) = + case def of + Pre _ v' -> [mkEquality (trPrimedVar v) (trVar v')] + 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 + tr :: forall t . Expr t -> K.Term + tr (Const t c) = trConst t c + tr (Ite _ c e1 e2) = K.FunApp "ite" [tr c, tr e1, tr e2] + tr (Op1 _ op e) = K.FunApp (show op) [tr e] + tr (Op2 _ op e1 e2) = K.FunApp (show op) [tr e1, tr e2] + tr (VarE _ v) = if primed then trPrimedVar v else trVar v + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Misc/Error.hs b/src/Copilot/Theorem/Misc/Error.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Misc/Error.hs @@ -0,0 +1,31 @@ +-------------------------------------------------------------------------------- + +module Copilot.Theorem.Misc.Error + ( badUse + , impossible + , impossible_ + , notHandled + , fatal + ) where + +-------------------------------------------------------------------------------- + +errorHeader :: String +errorHeader = "[Copilot-kind ERROR] " + +badUse :: String -> a +badUse s = error $ errorHeader ++ s + +impossible :: String -> a +impossible s = error $ errorHeader ++ "Unexpected internal error : " ++ s + +impossible_ :: a +impossible_ = error $ errorHeader ++ "Unexpected internal error" + +notHandled :: String -> a +notHandled s = error $ errorHeader ++ "Not handled : " ++ s + +fatal :: String -> a +fatal = error + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Misc/SExpr.hs b/src/Copilot/Theorem/Misc/SExpr.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Misc/SExpr.hs @@ -0,0 +1,81 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE FlexibleInstances #-} + +module Copilot.Theorem.Misc.SExpr where + +import Text.ParserCombinators.Parsec +import Text.PrettyPrint.HughesPJ as PP hiding (char, Str) +import Control.Applicative hiding ((<|>), empty) + +import Control.Monad + +-------------------------------------------------------------------------------- + +data SExpr a = Atom a + | List [SExpr a] + +blank = Atom "" +atom = Atom -- s +unit = List [] -- () +singleton a = List [Atom a] -- (s) +list = List -- (ss) +node a l = List (Atom a : l) -- (s ss) + +-------------------------------------------------------------------------------- + +-- A straightforward string representation + +instance Show (SExpr String) where + show = PP.render . show' + where + show' (Atom s) = text s + show' (List ts) = parens . hsep . map show' $ ts + + +-- More advanced printing with some basic indentation + +indent = nest 1 + +toString :: (SExpr a -> Bool) -> (a -> String) -> SExpr a -> String +toString shouldIndent printAtom expr = + PP.render (toDoc shouldIndent printAtom expr) + +toDoc :: (SExpr a -> Bool) -> (a -> String) -> SExpr a -> Doc +toDoc shouldIndent printAtom expr = case expr of + Atom a -> text (printAtom a) + List l -> parens (foldl renderItem empty l) + + where renderItem doc s + | shouldIndent s = + doc $$ indent (toDoc shouldIndent printAtom s) + | otherwise = + doc <+> toDoc shouldIndent printAtom s + +-------------------------------------------------------------------------------- + +parser :: GenParser Char st (SExpr String) +parser = + choice [try unitP, nodeP, leafP] + + where symbol = oneOf "!#$%&|*+-/:<=>?@^_~." + lonelyStr = many1 (alphaNum <|> symbol) + + unitP = string "()" >> return unit + + leafP = atom <$> lonelyStr + + nodeP = do void $ char '(' + spaces + st <- sepBy parser spaces + spaces + void $ char ')' + return $ List st + + +parseSExpr :: String -> Maybe (SExpr String) +parseSExpr str = case parse parser "" str of + Left s -> error (show s) -- Nothing + Right t -> Just t + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Misc/Utils.hs b/src/Copilot/Theorem/Misc/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Misc/Utils.hs @@ -0,0 +1,60 @@ +-------------------------------------------------------------------------------- + +module Copilot.Theorem.Misc.Utils + ( isSublistOf, nub', nubBy', nubEq + , openTempFile + ) where + +-------------------------------------------------------------------------------- + +import Data.Function (on) +import Data.List (groupBy, sortBy, group, sort) + +import Control.Applicative ((<$>)) +import Control.Monad + +import qualified Data.Set as Set + +import System.IO hiding (openTempFile) +import System.Random +import System.Directory + +-------------------------------------------------------------------------------- + +isSublistOf :: Ord a => [a] -> [a] -> Bool +isSublistOf = Set.isSubsetOf `on` Set.fromList + +nubEq :: Ord a => [a] -> [a] -> Bool +nubEq = (==) `on` Set.fromList + +-- An efficient version of 'nub' +nub' :: Ord a => [a] -> [a] +nub' = map head . group . sort + +nubBy' :: (a -> a -> Ordering) -> [a] -> [a] +nubBy' f = map head . groupBy (\x y -> f x y == EQ) . sortBy f + +-------------------------------------------------------------------------------- + +openTempFile :: String -> String -> String -> IO (String, Handle) +openTempFile loc baseName extension = do + + path <- freshPath + handle <- openFile path WriteMode + return (path, handle) + + where + + freshPath :: IO FilePath + freshPath = do + path <- pathFromSuff <$> randSuff + exists <- doesFileExist path + if exists then freshPath else return path + + randSuff :: IO String + randSuff = replicateM 4 $ randomRIO ('0', '9') + + pathFromSuff :: String -> FilePath + pathFromSuff suf = loc ++ "/" ++ baseName ++ suf ++ "." ++ extension + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Prove.hs b/src/Copilot/Theorem/Prove.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Prove.hs @@ -0,0 +1,185 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE NamedFieldPuns, ViewPatterns, ExistentialQuantification, GADTs #-} + +module Copilot.Theorem.Prove + ( Output (..) + , Status (..) + , Prover (..) + , PropId, PropRef (..) + , Proof, UProof, ProofScheme (..) + , Action (..) + , Universal, Existential + , check + , prove + ) where + +import qualified Copilot.Core as Core + +import Data.List (intercalate) +import Control.Applicative (liftA2, Applicative(..)) +import Control.Monad (liftM, ap) +import Control.Monad.Writer + +-------------------------------------------------------------------------------- + +data Output = Output Status [String] + +data Status = Sat | Valid | Invalid | Unknown | Error + +{- Each prover has to provide the following five functions. + The most important is `askProver`, which takes 3 arguments : + * The prover descriptor + * A list of properties names which are assumptions + * A property name which has to be deduced from these assumptions +-} + +data Prover = forall r . Prover + { proverName :: String + , startProver :: Core.Spec -> IO r + , askProver :: r -> [PropId] -> [PropId] -> IO Output + , closeProver :: r -> IO () + } + +type PropId = String + +data PropRef a where + PropRef :: PropId -> PropRef a + +data Universal +data Existential + +type Proof a = ProofScheme a () + +type UProof = Writer [Action] () + +data ProofScheme a b where + Proof :: Writer [Action] b -> ProofScheme a b + +instance Functor (ProofScheme a) where + fmap = liftM + +instance Applicative (ProofScheme a) where + pure = return + (<*>) = ap + +instance Monad (ProofScheme a) where + (Proof p) >>= f = Proof $ p >>= (\a -> case f a of Proof p -> p) + return a = Proof (return a) + +data Action where + Check :: Prover -> Action + Assume :: PropId -> Action + Admit :: Action + +-------------------------------------------------------------------------------- + +check :: Prover -> Proof a +check prover = Proof $ tell [Check prover] + +prove :: Core.Spec -> PropId -> UProof -> IO Bool +prove spec propId (execWriter -> actions) = do + + thms <- processActions [] actions + putStr $ "Finished: " ++ propId ++ ": proof " + if (elem propId thms) then (putStrLn "checked successfully") else (putStrLn "failed") + return $ elem propId thms + + where + processActions context [] = return context + processActions context (action:nextActions) = case action of + Check (Prover { startProver, askProver, closeProver }) -> do + prover <- startProver spec + (Output status infos) <- askProver prover context [propId] + closeProver prover + case status of + Sat -> do + putStrLn $ propId ++ ": sat " ++ "(" ++ intercalate ", " infos ++ ")" + processActions (propId : context) nextActions + Valid -> do + putStrLn $ propId ++ ": valid " ++ "(" ++ intercalate ", " infos ++ ")" + processActions (propId : context) nextActions + Invalid -> do + putStrLn $ propId ++ ": invalid " ++ "(" ++ intercalate ", " infos ++ ")" + processActions context nextActions + Error -> do + putStrLn $ propId ++ ": error " ++ "(" ++ intercalate ", " infos ++ ")" + processActions context nextActions + Unknown -> do + putStrLn $ propId ++ ": unknown " ++ "(" ++ intercalate ", " infos ++ ")" + processActions context nextActions + + Assume propId -> do + putStrLn $ propId ++ ": assumption" + processActions (propId : context) nextActions + + Admit -> do + putStrLn $ propId ++ ": admitted" + processActions (propId : context) nextActions + +combine :: Prover -> Prover -> Prover +combine + (Prover { proverName = proverNameL + , startProver = startProverL + , askProver = askProverL + , closeProver = closeProverL + }) + + (Prover { proverName = proverNameR + , startProver = startProverR + , askProver = askProverR + , closeProver = closeProverR + }) + + = Prover + { proverName = proverNameL ++ "_" ++ proverNameR + , startProver = \spec -> do + proverL <- startProverL spec + proverR <- startProverR spec + return (proverL, proverR) + + , askProver = \(stL, stR) assumptions toCheck -> + liftA2 (combineOutputs proverNameL proverNameR) + (askProverL stL assumptions toCheck) + (askProverR stR assumptions toCheck) + + , closeProver = \(stL, stR) -> do + closeProverL stL + closeProverR stR + } + +combineOutputs nameL nameR (Output stL msgL) (Output stR msgR) = + Output (combineSt stL stR) infos + + where + combineSt Error _ = Error + combineSt _ Error = Error + + combineSt Valid Invalid = Error + combineSt Invalid Valid = Error + + combineSt Invalid _ = Invalid + combineSt _ Invalid = Invalid + + combineSt Valid _ = Valid + combineSt _ Valid = Valid + + combineSt Sat _ = Sat + combineSt _ Sat = Sat + + combineSt Unknown Unknown = Unknown + + prefixMsg = case (stL, stR) of + (Valid, Invalid) -> ["The two provers don't agree"] + _ -> [] + + decoName s = "<" ++ s ++ ">" + + infos = + prefixMsg + ++ [decoName nameL] + ++ msgL + ++ [decoName nameR] + ++ msgR + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Prover/Backend.hs b/src/Copilot/Theorem/Prover/Backend.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Prover/Backend.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE RankNTypes #-} + +module Copilot.Theorem.Prover.Backend (SmtFormat(..), Backend(..), SatResult(..)) where + +import Copilot.Theorem.IL + +import System.IO + +class Show a => SmtFormat a where + push :: a + pop :: a + checkSat :: a + setLogic :: String -> a + declFun :: String -> Type -> [Type] -> a + assert :: Expr -> a + +data Backend a = Backend + { name :: String + , cmd :: String + , cmdOpts :: [String] + , inputTerminator :: Handle -> IO () + , incremental :: Bool + , logic :: String + , interpret :: String -> Maybe SatResult + } + +data SatResult = Sat | Unsat | Unknown + diff --git a/src/Copilot/Theorem/Prover/SMT.hs b/src/Copilot/Theorem/Prover/SMT.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Prover/SMT.hs @@ -0,0 +1,368 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs #-} + +module Copilot.Theorem.Prover.SMT + ( module Data.Default + , Options (..) + , induction, kInduction, onlySat, onlyValidity + , yices, dReal, altErgo, metit, z3, cvc4, mathsat + , Backend, SmtFormat + , SmtLib, Tptp + ) where + +import Copilot.Theorem.IL.Translate +import Copilot.Theorem.IL +import Copilot.Theorem.Prove (Output (..), check, Proof, Universal, Existential) +import qualified Copilot.Theorem.Prove as P + +import Copilot.Theorem.Prover.Backend +import qualified Copilot.Theorem.Prover.SMTIO as SMT + +import Copilot.Theorem.Prover.SMTLib (SmtLib) +import Copilot.Theorem.Prover.TPTP (Tptp) +import qualified Copilot.Theorem.Prover.SMTLib as SMTLib +import qualified Copilot.Theorem.Prover.TPTP as TPTP + +import Control.Applicative ((<$>), (<*)) +import Control.Monad (msum, unless, mzero) +import Control.Monad.State (StateT, runStateT, lift, get, modify) +import Control.Monad.IO.Class (liftIO) +import Control.Monad.Trans.Maybe (MaybeT (..)) + +import Data.Word +import Data.Maybe (fromJust, fromMaybe) +import Data.Function (on) +import Data.Default (Default(..)) +import Data.Map (Map) +import qualified Data.Map as Map +import Copilot.Theorem.Misc.Utils + +import System.IO (hClose) + +-------------------------------------------------------------------------------- + +-- | Tactics + +data Options = Options + { startK :: Word32 + -- The maximum number of steps of the k-induction algorithm the prover runs + -- before giving up. + , maxK :: Word32 + + -- If `debug` is set to `True`, the SMTLib/TPTP queries produced by the + -- prover are displayed in the standard output. + , debug :: Bool + } + +instance Default Options where + def = Options + { startK = 0 + , maxK = 10 + , debug = False + } + +onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential +onlySat opts backend = check P.Prover + { P.proverName = "OnlySat" + , P.startProver = return . ProofState opts backend Map.empty . translate + , P.askProver = onlySat' + , P.closeProver = const $ return () + } + +onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal +onlyValidity opts backend = check P.Prover + { P.proverName = "OnlyValidity" + , P.startProver = return . ProofState opts backend Map.empty . translate + , P.askProver = onlyValidity' + , P.closeProver = const $ return () + } + +induction :: SmtFormat a => Options -> Backend a -> Proof Universal +induction opts backend = check P.Prover + { P.proverName = "Induction" + , P.startProver = return . ProofState opts backend Map.empty . translate + , P.askProver = kInduction' 0 0 + , P.closeProver = const $ return () + } + +kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal +kInduction opts backend = check P.Prover + { P.proverName = "K-Induction" + , P.startProver = return . ProofState opts backend Map.empty . translate + , P.askProver = kInduction' (startK opts) (maxK opts) + , P.closeProver = const $ return () + } + +------------------------------------------------------------------------------- + +-- | Backends + +yices :: Backend SmtLib +yices = Backend + { name = "Yices" + , cmd = "yices-smt2" + , cmdOpts = ["--incremental"] + , inputTerminator = const $ return () + , incremental = True + , logic = "QF_NRA" + , interpret = SMTLib.interpret + } + +cvc4 :: Backend SmtLib +cvc4 = Backend + { name = "CVC4" + , cmd = "cvc4" + , cmdOpts = ["--incremental", "--lang=smt2", "--tlimit-per=5000"] + , inputTerminator = const $ return () + , incremental = True + , logic = "QF_UFNIRA" + , interpret = SMTLib.interpret + } + +altErgo :: Backend SmtLib +altErgo = Backend + { name = "Alt-Ergo" + , cmd = "alt-ergo.opt" + , cmdOpts = [] + , inputTerminator = hClose + , incremental = False + , logic = "QF_UFNIRA" + , interpret = SMTLib.interpret + } + +z3 :: Backend SmtLib +z3 = Backend + { name = "Z3" + , cmd = "z3" + , cmdOpts = ["-smt2", "-in"] + , inputTerminator = const $ return () + , incremental = True + , logic = "" + , interpret = SMTLib.interpret + } + +dReal :: Backend SmtLib +dReal = Backend + { name = "dReal" + , cmd = "perl" + , cmdOpts = ["-e", "alarm 10; exec dReal"] + , inputTerminator = hClose + , incremental = False + , logic = "QF_NRA" + , interpret = SMTLib.interpret + } + +mathsat :: Backend SmtLib +mathsat = Backend + { name = "MathSAT" + , cmd = "mathsat" + , cmdOpts = [] + , inputTerminator = const $ return () + , incremental = True + , logic = "QF_NRA" + , interpret = SMTLib.interpret + } + +-- The argument is the path to the "tptp" subdirectory of the metitarski +-- install location. +metit :: String -> Backend Tptp +metit installDir = Backend + { name = "MetiTarski" + , cmd = "metit" + , cmdOpts = + [ "--time", "5" + , "--autoInclude" + , "--tptp", installDir + , "/dev/stdin" + ] + , inputTerminator = hClose + , incremental = False + , logic = "" + , interpret = TPTP.interpret + } + +------------------------------------------------------------------------------- + +-- | Checks the Copilot specification with k-induction + +type ProofScript b = MaybeT (StateT (ProofState b) IO) + +runPS :: ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b) +runPS ps = runStateT (runMaybeT ps) + +data ProofState b = ProofState + { options :: Options + , backend :: Backend b + , solvers :: Map SolverId (SMT.Solver b) + , spec :: IL + } + +data SolverId = Base | Step + deriving (Show, Ord, Eq) + +getModels :: [PropId] -> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool) +getModels assumptionIds toCheckIds = do + IL {modelInit, modelRec, properties, inductive} <- spec <$> get + let (as, as') = selectProps assumptionIds properties + (as'', toCheck) = selectProps toCheckIds properties + modelRec' = modelRec ++ as ++ as' ++ as'' + return (modelInit, modelRec', toCheck, inductive) + +getSolver :: SmtFormat b => SolverId -> ProofScript b (SMT.Solver b) +getSolver sid = do + solvers <- solvers <$> get + case Map.lookup sid solvers of + Nothing -> startNewSolver sid + Just solver -> return solver + +setSolver :: SolverId -> SMT.Solver b -> ProofScript b () +setSolver sid solver = + (lift . modify) $ \s -> s { solvers = Map.insert sid solver (solvers s) } + +deleteSolver :: SolverId -> ProofScript b () +deleteSolver sid = + (lift . modify) $ \s -> s { solvers = Map.delete sid (solvers s) } + +startNewSolver :: SmtFormat b => SolverId -> ProofScript b (SMT.Solver b) +startNewSolver sid = do + dbg <- (options <$> get >>= return . debug) + backend <- backend <$> get + s <- liftIO $ SMT.startNewSolver (show sid) dbg backend + setSolver sid s + return s + +declVars :: SmtFormat b => SolverId -> [VarDescr] -> ProofScript b () +declVars sid vs = do + s <- getSolver sid + s' <- liftIO $ SMT.declVars s vs + setSolver sid s' + +assume :: SmtFormat b => SolverId -> [Expr] -> ProofScript b () +assume sid cs = do + s <- getSolver sid + s' <- liftIO $ SMT.assume s cs + setSolver sid s' + +entailed :: SmtFormat b => SolverId -> [Expr] -> ProofScript b SatResult +entailed sid cs = do + backend <- backend <$> get + s <- getSolver sid + result <- liftIO $ SMT.entailed s cs + unless (incremental backend) $ stop sid + return result + +stop :: SmtFormat b => SolverId -> ProofScript b () +stop sid = do + s <- getSolver sid + deleteSolver sid + liftIO $ SMT.stop s + +proofKind :: Integer -> String +proofKind 0 = "induction" +proofKind k = "k-induction (k = " ++ show k ++ ")" + +stopSolvers :: SmtFormat b => ProofScript b () +stopSolvers = do + solvers <- solvers <$> get + mapM_ stop (fst <$> Map.toList solvers) + +entailment :: SmtFormat b => SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult +entailment sid assumptions props = do + declVars sid $ nub' $ getVars assumptions ++ getVars props + assume sid assumptions + entailed sid props + +getVars :: [Expr] -> [VarDescr] +getVars = nubBy' (compare `on` varName) . concatMap getVars' + where getVars' :: Expr -> [VarDescr] + getVars' = \case + ConstB _ -> [] + ConstI _ _ -> [] + ConstR _ -> [] + Ite _ e1 e2 e3 -> getVars' e1 ++ getVars' e2 ++ getVars' e3 + Op1 _ _ e -> getVars' e + Op2 _ _ e1 e2 -> getVars' e1 ++ getVars' e2 + SVal t seq (Fixed i) -> [VarDescr (seq ++ "_" ++ show i) t []] + SVal t seq (Var i) -> [VarDescr (seq ++ "_n" ++ show i) t []] + FunApp t name args -> [VarDescr name t (map typeOf args)] + ++ concatMap getVars' args + +unknown :: ProofScript b a +unknown = mzero + +unknown' :: String -> ProofScript b Output +unknown' msg = return $ Output P.Unknown [msg] + +invalid :: String -> ProofScript b Output +invalid msg = return $ Output P.Invalid [msg] + +sat :: String -> ProofScript b Output +sat msg = return $ Output P.Sat [msg] + +valid :: String -> ProofScript b Output +valid msg = return $ Output P.Valid [msg] + +kInduction' :: SmtFormat b => Word32 -> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output +kInduction' startK maxK s as ps = (fromMaybe (Output P.Unknown ["proof by k-induction failed"]) . fst) + <$> runPS (msum (map induction [(toInteger startK) .. (toInteger maxK)]) <* stopSolvers) s + where + induction k = do + (modelInit, modelRec, toCheck, inductive) <- getModels as ps + + let base = [evalAt (Fixed i) m | m <- modelRec, i <- [0 .. k]] + baseInv = [evalAt (Fixed k) m | m <- toCheck] + + let step = [evalAt (_n_plus i) m | m <- modelRec, i <- [0 .. k + 1]] + ++ [evalAt (_n_plus i) m | m <- toCheck, i <- [0 .. k]] + stepInv = [evalAt (_n_plus $ k + 1) m | m <- toCheck] + + entailment Base (modelInit ++ base) baseInv >>= \case + Sat -> invalid $ "base case failed for " ++ proofKind k + Unknown -> unknown + Unsat -> + if not inductive then valid ("proved without induction") + else entailment Step step stepInv >>= \case + Sat -> unknown + Unknown -> unknown + Unsat -> valid $ "proved with " ++ proofKind k + + +onlySat' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output +onlySat' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s + where + script = do + (modelInit, modelRec, toCheck, inductive) <- getModels as ps + + let base = map (evalAt (Fixed 0)) modelRec + baseInv = map (evalAt (Fixed 0)) toCheck + + if inductive + then unknown' "proposition requires induction to prove." + else entailment Base (modelInit ++ base) (map (Op1 Bool Not) baseInv) >>= \case + Unsat -> invalid "prop not satisfiable" + Unknown -> unknown' "failed to find a satisfying model" + Sat -> sat "prop is satisfiable" + +onlyValidity' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output +onlyValidity' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s + where + script = do + (modelInit, modelRec, toCheck, inductive) <- getModels as ps + + let base = map (evalAt (Fixed 0)) modelRec + baseInv = map (evalAt (Fixed 0)) toCheck + + if inductive + then unknown' "proposition requires induction to prove." + else entailment Base (modelInit ++ base) baseInv >>= \case + Unsat -> valid "proof by SMT solver" + Unknown -> unknown + Sat -> invalid "SMT solver found a counter-example." + +selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr]) +selectProps propIds properties = + (squash . unzip) [(as, p) | (id, (as, p)) <- Map.toList properties, id `elem` propIds] + where squash (a, b) = (concat a, b) + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Prover/SMTIO.hs b/src/Copilot/Theorem/Prover/SMTIO.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Prover/SMTIO.hs @@ -0,0 +1,108 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE LambdaCase, NamedFieldPuns, RankNTypes, ViewPatterns #-} + +module Copilot.Theorem.Prover.SMTIO + ( Solver + , startNewSolver, assume, entailed, stop, declVars + ) where + +import Copilot.Theorem.IL +import Copilot.Theorem.Prover.Backend + +import System.IO +import System.Process +import Control.Monad +import Control.Monad.Trans +import Control.Monad.Trans.Maybe +import Control.Applicative ((<$>)) +import Data.Maybe +import Data.Set ((\\), fromList, Set, union, empty, elems) + +-------------------------------------------------------------------------------- + +data Solver a = Solver + { solverName :: String + , inh :: Handle + , outh :: Handle + , process :: ProcessHandle + , debugMode :: Bool + , vars :: Set VarDescr + , model :: Set Expr + , backend :: Backend a + } + +-------------------------------------------------------------------------------- + +debug :: Bool -> Solver a -> String -> IO () +debug printName s str = when (debugMode s) $ + putStrLn $ (if printName then "<" ++ solverName s ++ "> " else "") ++ str + +send :: Show a => Solver a -> a -> IO () +send _ (show -> "") = return () +send s (show -> a) = do + hPutStr (inh s) $ a ++ "\n" + debug True s a + hFlush $ inh s + +receive :: Solver a -> IO SatResult +receive s = fromJust <$> runMaybeT (msum $ repeat line) + where + line :: MaybeT IO SatResult + line = do + eof <- liftIO $ hIsEOF $ outh s + if eof + then liftIO (debug True s "[received: EOF]") >> return Unknown + else do + ln <- liftIO $ hGetLine $ outh s + liftIO $ debug True s $ "[received: " ++ ln ++ "]" + MaybeT $ return $ (interpret $ backend s) ln + +-------------------------------------------------------------------------------- + +startNewSolver :: SmtFormat a => String -> Bool -> Backend a -> IO (Solver a) +startNewSolver name dbgMode b = do + (i, o, e, p) <- runInteractiveProcess (cmd b) (cmdOpts b) Nothing Nothing + hClose e + let s = Solver name i o p dbgMode empty empty b + send s $ setLogic $ logic b + return s + +stop :: Solver a -> IO () +stop s = do + hClose $ inh s + hClose $ outh s + terminateProcess $ process s + +-------------------------------------------------------------------------------- + +assume :: SmtFormat a => Solver a -> [Expr] -> IO (Solver a) +assume s@(Solver { model }) cs = do + let newAxioms = elems $ fromList cs \\ model + assume' s newAxioms + return s { model = model `union` fromList newAxioms } + +assume' :: SmtFormat a => Solver a -> [Expr] -> IO () +assume' s cs = forM_ cs (send s . assert . bsimpl) + +entailed :: SmtFormat a => Solver a -> [Expr] -> IO SatResult +entailed s cs = do + when (incremental $ backend s) $ send s push + case cs of + [] -> putStrLn "Warning: no proposition to prove." >> assume' s [ConstB True] + _ -> assume' s [foldl1 (Op2 Bool Or) (map (Op1 Bool Not) cs)] + send s checkSat + (inputTerminator $ backend s) (inh s) + + when (incremental $ backend s) $ send s pop + receive s + +declVars :: SmtFormat a => Solver a -> [VarDescr] -> IO (Solver a) +declVars s@(Solver { vars }) decls = do + let newVars = elems $ fromList decls \\ vars + forM_ newVars $ \(VarDescr {varName, varType, args}) -> + send s $ declFun varName varType args + return s { vars = vars `union` fromList newVars } + +-------------------------------------------------------------------------------- + diff --git a/src/Copilot/Theorem/Prover/SMTLib.hs b/src/Copilot/Theorem/Prover/SMTLib.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Prover/SMTLib.hs @@ -0,0 +1,100 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs, FlexibleInstances #-} + +module Copilot.Theorem.Prover.SMTLib (SmtLib, interpret) where + +import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..)) + +import Copilot.Theorem.IL +import Copilot.Theorem.Misc.SExpr + +import Text.Printf + +-------------------------------------------------------------------------------- + +newtype SmtLib = SmtLib (SExpr String) + +instance Show SmtLib where + show (SmtLib s) = show s + +smtTy :: Type -> String +smtTy Bool = "Bool" +smtTy Real = "Real" +smtTy _ = "Int" + +-------------------------------------------------------------------------------- + +instance SmtFormat SmtLib where + push = SmtLib $ node "push" [atom "1"] + pop = SmtLib $ node "pop" [atom "1"] + checkSat = SmtLib $ singleton "check-sat" + setLogic "" = SmtLib $ blank + setLogic l = SmtLib $ node "set-logic" [atom l] + declFun name retTy args = SmtLib $ + node "declare-fun" [atom name, (list $ map (atom . smtTy) args), atom (smtTy retTy)] + assert c = SmtLib $ node "assert" [expr c] + +interpret :: String -> Maybe SatResult +interpret "sat" = Just Sat +interpret "unsat" = Just Unsat +interpret _ = Just Unknown + +-------------------------------------------------------------------------------- + +expr :: Expr -> SExpr String + +expr (ConstB v) = atom $ if v then "true" else "false" +expr (ConstI _ v) = atom $ show v +expr (ConstR v) = atom $ printf "%f" v + +expr (Ite _ cond e1 e2) = node "ite" [expr cond, expr e1, expr e2] + +expr (FunApp _ funName args) = node funName $ map expr args + +expr (Op1 _ op e) = + node smtOp [expr e] + where + smtOp = case op of + Not -> "not" + Neg -> "-" + Abs -> "abs" + Exp -> "exp" + Sqrt -> "sqrt" + Log -> "log" + Sin -> "sin" + Tan -> "tan" + Cos -> "cos" + Asin -> "asin" + Atan -> "atan" + Acos -> "acos" + Sinh -> "sinh" + Tanh -> "tanh" + Cosh -> "cosh" + Asinh -> "asinh" + Atanh -> "atanh" + Acosh -> "acosh" + +expr (Op2 _ op e1 e2) = + node smtOp [expr e1, expr e2] + where + smtOp = case op of + Eq -> "=" + Le -> "<=" + Lt -> "<" + Ge -> ">=" + Gt -> ">" + And -> "and" + Or -> "or" + Add -> "+" + Sub -> "-" + Mul -> "*" + Mod -> "mod" + Fdiv -> "/" + Pow -> "^" + +expr (SVal _ f ix) = atom $ case ix of + Fixed i -> f ++ "_" ++ show i + Var off -> f ++ "_n" ++ show off + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Prover/TPTP.hs b/src/Copilot/Theorem/Prover/TPTP.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Prover/TPTP.hs @@ -0,0 +1,105 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs, LambdaCase #-} + +module Copilot.Theorem.Prover.TPTP (Tptp, interpret) where + +import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..)) +import Copilot.Theorem.IL + +import Data.List + +-------------------------------------------------------------------------------- + +data Tptp = Ax TptpExpr | Null + +data TptpExpr = Bin TptpExpr String TptpExpr | Un String TptpExpr + | Atom String | Fun String [TptpExpr] + +instance Show Tptp where + show (Ax e) = "fof(formula, axiom, " ++ show e ++ ")." + show Null = "" + +instance Show TptpExpr where + show (Bin e1 op e2) = "(" ++ show e1 ++ " " ++ op ++ " " ++ show e2 ++ ")" + show (Un op e) = "(" ++ op ++ " " ++ show e ++ ")" + show (Atom atom) = atom + show (Fun name args) = name ++ "(" ++ intercalate ", " (map show args) ++ ")" + +-------------------------------------------------------------------------------- + +instance SmtFormat Tptp where + push = Null + pop = Null + checkSat = Null + setLogic = const Null + declFun = const $ const $ const Null + assert c = Ax $ expr c + +interpret :: String -> Maybe SatResult +interpret str + | "SZS status Unsatisfiable" `isPrefixOf` str = Just Unsat + | "SZS status" `isPrefixOf` str = Just Unknown + | otherwise = Nothing + +-------------------------------------------------------------------------------- + +expr :: Expr -> TptpExpr +expr = \case + ConstB v -> Atom $ if v then "$true" else "$false" + ConstR v -> Atom $ show v + ConstI _ v -> Atom $ show v + + Ite _ c e1 e2 -> Bin (Bin (expr c) "=>" (expr e1)) + "&" (Bin (Un "~" (expr c)) "=>" (expr e2)) + + FunApp _ f args -> Fun f $ map expr args + + Op1 _ Not e -> Un (showOp1 Not) $ expr e + Op1 _ Neg e -> Un (showOp1 Neg) $ expr e + Op1 _ op e -> Fun (showOp1 op) [expr e] + + Op2 _ op e1 e2 -> Bin (expr e1) (showOp2 op) (expr e2) + + SVal _ f ix -> case ix of + Fixed i -> Atom $ f ++ "_" ++ show i + Var off -> Atom $ f ++ "_n" ++ show off + +showOp1 :: Op1 -> String +showOp1 = \case + Not -> "~" + Neg -> "-" + Abs -> "abs" + Exp -> "exp" + Sqrt -> "sqrt" + Log -> "log" + Sin -> "sin" + Tan -> "tan" + Cos -> "cos" + Asin -> "arcsin" + Atan -> "arctan" + Acos -> "arccos" + Sinh -> "sinh" + Tanh -> "tanh" + Cosh -> "cosh" + Asinh -> "arcsinh" + Atanh -> "arctanh" + Acosh -> "arccosh" + +showOp2 :: Op2 -> String +showOp2 = \case + Eq -> "=" + Le -> "<=" + Lt -> "<" + Ge -> ">=" + Gt -> ">" + And -> "&" + Or -> "|" + Add -> "+" + Sub -> "-" + Mul -> "*" + Mod -> "mod" + Fdiv -> "/" + Pow -> "^" + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/Prover/Z3.hs b/src/Copilot/Theorem/Prover/Z3.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Prover/Z3.hs @@ -0,0 +1,608 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs, + MultiParamTypeClasses, FlexibleContexts #-} + +module Copilot.Theorem.Prover.Z3 + ( module Data.Default + , Options (..) + , induction, kInduction, onlySat, onlyValidity + ) +where + +import Copilot.Theorem.IL.Translate +import Copilot.Theorem.IL +import Copilot.Theorem.Prove (Output (..), check, Proof, Universal, Existential) +import qualified Copilot.Theorem.Prove as P + +import Control.Applicative ((<$>), (<*)) +import Control.Monad (msum, mzero, when, void, unless) +import Control.Monad.State (StateT, runStateT, get, modify) +import Control.Monad.Trans.Maybe (MaybeT (..)) + +import Data.Word +import Data.Unit +import Data.Maybe (fromJust, fromMaybe) +import Data.Default (Default(..)) +import Data.List (foldl') + +import Data.Set (Set, (\\), union) +import qualified Data.Set as Set +import Data.Map (Map) +import qualified Data.Map as Map + +import Language.SMTLib2 +import Language.SMTLib2.Pipe +import Language.SMTLib2.Connection +import Language.SMTLib2.Strategy + +import Language.SMTLib2.Internals hiding (Var) + +import System.Console.ANSI +import System.IO +import Control.Monad.Trans + +-------------------------------------------------------------------------------- + +-- | Tactics + +data Options = Options + { nraNLSat :: Bool + , startK :: Word32 + -- The maximum number of steps of the k-induction algorithm the prover runs + -- before giving up. + , maxK :: Word32 + + -- If `debug` is set to `True`, the SMTLib/TPTP queries produced by the + -- prover are displayed in the standard output. + , debug :: Bool + } + +instance Default Options where + def = Options + { nraNLSat = True + , startK = 0 + , maxK = 10 + , debug = False + } + +onlySat :: Options -> Proof Existential +onlySat opts = check P.Prover + { P.proverName = "OnlySat" + , P.startProver = return . ProofState opts Map.empty Map.empty Map.empty . translate + , P.askProver = onlySat' + , P.closeProver = const $ return () + } + +onlyValidity :: Options -> Proof Universal +onlyValidity opts = check P.Prover + { P.proverName = "OnlyValidity" + , P.startProver = return . ProofState opts Map.empty Map.empty Map.empty . translate + , P.askProver = onlyValidity' + , P.closeProver = const $ return () + } + +induction :: Options -> Proof Universal +induction opts = check P.Prover + { P.proverName = "Induction" + , P.startProver = return . ProofState opts Map.empty Map.empty Map.empty . translate + , P.askProver = kInduction' 0 0 + , P.closeProver = const $ return () + } + +kInduction :: Options -> Proof Universal +kInduction opts = check P.Prover + { P.proverName = "K-Induction" + , P.startProver = return . ProofState opts Map.empty Map.empty Map.empty . translate + , P.askProver = kInduction' (startK opts) (maxK opts) + , P.closeProver = const $ return () + } + +------------------------------------------------------------------------------- + +-- | Checks the Copilot specification with k-induction + +type Solver = SMTConnection (DebugBackend SMTPipe) + +type ProofScript = MaybeT (StateT ProofState IO) + +runPS :: ProofScript a -> ProofState -> IO (Maybe a, ProofState) +runPS ps = runStateT (runMaybeT ps) + +data ProofState = ProofState + { options :: Options + , solvers :: Map SolverId Solver + , vars :: Map SolverId TransState + , assumps :: Map SolverId (Set Expr) + , spec :: IL + } + +data SolverId = Base | Step + deriving (Show, Ord, Eq) + +getModels :: [PropId] -> [PropId] -> ProofScript ([Expr], [Expr], [Expr], Bool) +getModels assumptionIds toCheckIds = do + IL {modelInit, modelRec, properties, inductive} <- spec <$> get + let (as, as') = selectProps assumptionIds properties + (as'', toCheck) = selectProps toCheckIds properties + modelRec' = modelRec ++ as ++ as' ++ as'' + return (modelInit, modelRec', toCheck, inductive) + +getSolver :: SolverId -> ProofScript Solver +getSolver sid = do + solvers <- solvers <$> get + case Map.lookup sid solvers of + Nothing -> startNewSolver sid + Just solver -> return solver + +setSolver :: SolverId -> Solver -> ProofScript () +setSolver sid solver = + (lift . modify) $ \s -> s { solvers = Map.insert sid solver (solvers s) } + +getVars :: SolverId -> ProofScript TransState +getVars sid = do + vars <- vars <$> get + return $ case Map.lookup sid vars of + Nothing -> noVars + Just vs -> vs + +setVars :: SolverId -> TransState -> ProofScript () +setVars sid vs = + (lift . modify) $ \s -> s { vars = Map.insert sid vs (vars s) } + +newAssumps :: SolverId -> [Expr] -> ProofScript [Expr] +newAssumps sid as' = do + assumps <- assumps <$> get + case Map.lookup sid assumps of + Nothing -> do + modify $ \s -> s { assumps = Map.insert sid (Set.fromList as') assumps } + return as' + Just as -> do + let as'' = (Set.fromList as') `union` as + modify $ \s -> s { assumps = Map.insert sid as'' assumps } + return $ Set.elems $ (Set.fromList as') \\ as + +deleteSolver :: SolverId -> ProofScript () +deleteSolver sid = + (lift . modify) $ \s -> s { solvers = Map.delete sid (solvers s) } + +startNewSolver :: SolverId -> ProofScript Solver +startNewSolver sid = do + pipe <- liftIO $ createSMTPipe "z3" ["-smt2", "-in"] + dbg <- (options <$> get >>= return . debug) + s <- liftIO $ open (namedDebugBackend (show sid) (not dbg) pipe) + setSolver sid s + return s + +stop :: SolverId -> ProofScript () +stop sid = do + s <- getSolver sid + deleteSolver sid + liftIO $ close s + +stopSolvers :: ProofScript () +stopSolvers = do + solvers <- solvers <$> get + mapM_ stop (fst <$> Map.toList solvers) + +proofKind :: Integer -> String +proofKind 0 = "induction" +proofKind k = "k-induction (k = " ++ show k ++ ")" + +entailment :: SolverId -> [Expr] -> [Expr] -> ProofScript CheckSatResult +entailment sid assumptions props = do + s <- getSolver sid + liftIO $ performSMT s $ setOption (ProduceModels True) + -- liftIO $ performSMT s $ setOption (ProduceProofs True) + -- liftIO $ performSMT s $ setOption (ProduceUnsatCores True) + vs <- getVars sid + assumps' <- newAssumps sid assumptions + (_, vs') <- liftIO $ performSMT s $ runStateT (mapM_ (\e -> transB e >>= lift . assert) assumps') vs + setVars sid vs' + liftIO $ performSMT s $ push + _ <- liftIO $ performSMT s $ runStateT + (transB (bsimpl (foldl' (Op2 Bool Or) (ConstB False) $ map (Op1 Bool Not) props)) >>= lift . assert) vs' + + nraNL <- (options <$> get >>= return . nraNLSat) + res <- if nraNL + then liftIO $ performSMT s $ checkSat' (Just (UsingParams (CustomTactic "qfnra-nlsat") [])) + (CheckSatLimits (Just 5000) Nothing) + else liftIO $ performSMT s $ checkSat' Nothing (CheckSatLimits (Just 5000) Nothing) + + when (res == Sat) $ void $ liftIO $ performSMT s $ getModel + -- when (res == Unsat) $ void $ liftIO $ performSMT s $ getProof + liftIO $ performSMT s $ pop + -- liftIO $ print model + return res + +unknown :: ProofScript a +unknown = mzero + +unknown' :: String -> ProofScript Output +unknown' msg = return $ Output P.Unknown [msg] + +invalid :: String -> ProofScript Output +invalid msg = return $ Output P.Invalid [msg] + +sat :: String -> ProofScript Output +sat msg = return $ Output P.Sat [msg] + +valid :: String -> ProofScript Output +valid msg = return $ Output P.Valid [msg] + +kInduction' :: Word32 -> Word32 -> ProofState -> [PropId] -> [PropId] -> IO Output +kInduction' startK maxK s as ps = (fromMaybe (Output P.Unknown ["proof by k-induction failed"]) . fst) + <$> runPS (msum (map induction [(toInteger startK) .. (toInteger maxK)]) <* stopSolvers) s + where + induction k = do + (modelInit, modelRec, toCheck, inductive) <- getModels as ps + + let base = [evalAt (Fixed i) m | m <- modelRec, i <- [0 .. k]] + baseInv = [evalAt (Fixed k) m | m <- toCheck] + + let step = [evalAt (_n_plus i) m | m <- modelRec, i <- [0 .. k + 1]] + ++ [evalAt (_n_plus i) m | m <- toCheck, i <- [0 .. k]] + stepInv = [evalAt (_n_plus $ k + 1) m | m <- toCheck] + + entailment Base (modelInit ++ base) baseInv >>= \case + Sat -> invalid $ "base case failed for " ++ proofKind k + Unknown -> unknown + Unsat -> + if not inductive then valid ("proved without induction") + else entailment Step step stepInv >>= \case + Sat -> unknown + Unknown -> unknown + Unsat -> valid $ "proved with " ++ proofKind k + +onlySat' :: ProofState -> [PropId] -> [PropId] -> IO Output +onlySat' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s + where + script = do + (modelInit, modelRec, toCheck, inductive) <- getModels as ps + + let base = map (evalAt (Fixed 0)) modelRec + baseInv = map (evalAt (Fixed 0)) toCheck + + if inductive + then unknown' "proposition requires induction to prove." + else entailment Base (modelInit ++ base) (map (Op1 Bool Not) baseInv) >>= \case + Unsat -> invalid "prop not satisfiable" + Unknown -> unknown' "failed to find a satisfying model" + Sat -> sat "prop is satisfiable" + +onlyValidity' :: ProofState -> [PropId] -> [PropId] -> IO Output +onlyValidity' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s + where + script = do + (modelInit, modelRec, toCheck, inductive) <- getModels as ps + + let base = map (evalAt (Fixed 0)) modelRec + baseInv = map (evalAt (Fixed 0)) toCheck + + if inductive + then unknown' "proposition requires induction to prove." + else entailment Base (modelInit ++ base) baseInv >>= \case + Unsat -> valid "proof by Z3" + Unknown -> unknown + Sat -> invalid "Z3 found a counter-example." + +selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr]) +selectProps propIds properties = + (squash . unzip) [(as, p) | (id, (as, p)) <- Map.toList properties, id `elem` propIds] + where squash (a, b) = (concat a, b) + +-------------------------------------------------------------------------------- + +-- | This is all very ugly. It might make better sense to go straight from Core to SMTExpr, or maybe use SBV instead. + +type Trans = StateT TransState SMT + +data TransState = TransState + { boolVars :: Map String (SMTExpr Bool) + , bv8Vars :: Map String (SMTExpr BV8) + , bv16Vars :: Map String (SMTExpr BV16) + , bv32Vars :: Map String (SMTExpr BV32) + , bv64Vars :: Map String (SMTExpr BV64) + , ratVars :: Map String (SMTExpr Rational) + } + +noVars = TransState Map.empty Map.empty Map.empty Map.empty Map.empty Map.empty + +getBoolVar :: String -> Trans (SMTExpr Bool) +getBoolVar = getVar boolVars (\v s -> s {boolVars = v}) + +getBV8Var :: String -> Trans (SMTExpr BV8) +getBV8Var = getVar bv8Vars (\v s -> s {bv8Vars = v}) + +getBV16Var :: String -> Trans (SMTExpr BV16) +getBV16Var = getVar bv16Vars (\v s -> s {bv16Vars = v}) + +getBV32Var :: String -> Trans (SMTExpr BV32) +getBV32Var = getVar bv32Vars (\v s -> s {bv32Vars = v}) + +getBV64Var :: String -> Trans (SMTExpr BV64) +getBV64Var = getVar bv64Vars (\v s -> s {bv64Vars = v}) + +getRatVar :: String -> Trans (SMTExpr Rational) +getRatVar = getVar ratVars (\v s -> s {ratVars = v}) + +getVar proj mod v = do + vs <- proj <$> get + case Map.lookup v vs of + Nothing -> do + newVar <- lift $ varNamed v + modify $ mod $ Map.insert v newVar vs + return newVar + Just x -> return x + +transB :: Expr -> Trans (SMTExpr Bool) +transB = \case + ConstB b -> return $ constant b + + Ite _ c e1 e2 -> do + c' <- transB c + trans2B e1 e2 (ite c') + + Op1 _ Not e -> transB e >>= return . not' + + Op2 _ And e1 e2 -> do + e1' <- transB e1 + e2' <- transB e2 + return $ e1' .&&. e2' + Op2 _ Or e1 e2 -> do + e1' <- transB e1 + e2' <- transB e2 + return $ e1' .||. e2' + + Op2 _ Eq e1 e2 -> case typeOf e1 of + Bool -> trans2B e1 e2 (.==.) + Real -> trans2R e1 e2 (.==.) + BV8 -> trans2BV8 e1 e2 (.==.) + BV16 -> trans2BV16 e1 e2 (.==.) + BV32 -> trans2BV32 e1 e2 (.==.) + BV64 -> trans2BV64 e1 e2 (.==.) + SBV8 -> trans2BV8 e1 e2 (.==.) + SBV16 -> trans2BV16 e1 e2 (.==.) + SBV32 -> trans2BV32 e1 e2 (.==.) + SBV64 -> trans2BV64 e1 e2 (.==.) + + Op2 _ Le e1 e2 -> case typeOf e1 of + Real -> trans2R e1 e2 (.<=.) + BV8 -> trans2BV8 e1 e2 bvule + BV16 -> trans2BV16 e1 e2 bvule + BV32 -> trans2BV32 e1 e2 bvule + BV64 -> trans2BV64 e1 e2 bvule + SBV8 -> trans2BV8 e1 e2 bvsle + SBV16 -> trans2BV16 e1 e2 bvsle + SBV32 -> trans2BV32 e1 e2 bvsle + SBV64 -> trans2BV64 e1 e2 bvsle + _ -> undefined + Op2 _ Ge e1 e2 -> case typeOf e1 of + Real -> trans2R e1 e2 (.>=.) + BV8 -> trans2BV8 e1 e2 bvuge + BV16 -> trans2BV16 e1 e2 bvuge + BV32 -> trans2BV32 e1 e2 bvuge + BV64 -> trans2BV64 e1 e2 bvuge + SBV8 -> trans2BV8 e1 e2 bvsge + SBV16 -> trans2BV16 e1 e2 bvsge + SBV32 -> trans2BV32 e1 e2 bvsge + SBV64 -> trans2BV64 e1 e2 bvsge + _ -> undefined + Op2 _ Lt e1 e2 -> case typeOf e1 of + Real -> trans2R e1 e2 (.<.) + BV8 -> trans2BV8 e1 e2 bvult + BV16 -> trans2BV16 e1 e2 bvult + BV32 -> trans2BV32 e1 e2 bvult + BV64 -> trans2BV64 e1 e2 bvult + SBV8 -> trans2BV8 e1 e2 bvslt + SBV16 -> trans2BV16 e1 e2 bvslt + SBV32 -> trans2BV32 e1 e2 bvslt + SBV64 -> trans2BV64 e1 e2 bvslt + _ -> undefined + Op2 _ Gt e1 e2 -> case typeOf e1 of + Real -> trans2R e1 e2 (.>.) + BV8 -> trans2BV8 e1 e2 bvugt + BV16 -> trans2BV16 e1 e2 bvugt + BV32 -> trans2BV32 e1 e2 bvugt + BV64 -> trans2BV64 e1 e2 bvugt + SBV8 -> trans2BV8 e1 e2 bvsgt + SBV16 -> trans2BV16 e1 e2 bvsgt + SBV32 -> trans2BV32 e1 e2 bvsgt + SBV64 -> trans2BV64 e1 e2 bvsgt + _ -> undefined + + SVal _ s i -> getBoolVar $ ncVar s i + + e -> error $ "Encountered unhandled expression (Bool): " ++ show e + +ncVar s (Fixed i) = s ++ "_" ++ show i +ncVar s (Var i) = s ++ "_n" ++ show i + +transR :: Expr -> Trans (SMTExpr Rational) +transR = \case + ConstR n -> return $ constant $ toRational n + Ite _ c e1 e2 -> do + c' <- transB c + trans2R e1 e2 (ite c') + + Op1 _ Neg e -> transR e >>= return . (app neg) + Op1 _ Abs e -> transR e >>= return . (app SMTAbs) + + Op2 _ Add e1 e2 -> trans2R e1 e2 $ \x y -> app plus [x, y] + Op2 _ Sub e1 e2 -> trans2R e1 e2 $ \x y -> app minus (x, y) + Op2 _ Mul e1 e2 -> trans2R e1 e2 $ \x y -> app mult [x, y] + Op2 _ Fdiv e1 e2 -> trans2R e1 e2 divide + + Op2 _ Pow e1 e2 -> do + let pow = SMTBuiltIn "^" unit :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational + trans2R e1 e2 $ \x y -> app pow (x, y) + + SVal _ s i -> getRatVar $ ncVar s i + + e -> error $ "Encountered unhandled expression (Rat): " ++ show e + +-- TODO(chathhorn): bleghh +transBV8 :: Expr -> Trans (SMTExpr BV8) +transBV8 = \case + ConstI _ n -> return $ constant $ BitVector n + Ite _ c e1 e2 -> do + c' <- transB c + trans2BV8 e1 e2 (ite c') + + Op1 _ Abs e -> transBV8 e >>= return . abs + Op1 _ Neg e -> transBV8 e >>= return . negate + Op2 _ Add e1 e2 -> trans2BV8 e1 e2 (+) + Op2 _ Sub e1 e2 -> trans2BV8 e1 e2 (-) + Op2 _ Mul e1 e2 -> trans2BV8 e1 e2 (*) + SVal _ s i -> getBV8Var $ ncVar s i + + e -> error $ "Encountered unhandled expression (BV8): " ++ show e + +transBV16 :: Expr -> Trans (SMTExpr BV16) +transBV16 = \case + ConstI _ n -> return $ constant $ BitVector n + Ite _ c e1 e2 -> do + c' <- transB c + trans2BV16 e1 e2 (ite c') + + Op1 _ Abs e -> transBV16 e >>= return . abs + Op1 _ Neg e -> transBV16 e >>= return . negate + Op2 _ Add e1 e2 -> trans2BV16 e1 e2 (+) + Op2 _ Sub e1 e2 -> trans2BV16 e1 e2 (-) + Op2 _ Mul e1 e2 -> trans2BV16 e1 e2 (*) + SVal _ s i -> getBV16Var $ ncVar s i + + e -> error $ "Encountered unhandled expression (BV16): " ++ show e + +transBV32 :: Expr -> Trans (SMTExpr BV32) +transBV32 = \case + ConstI _ n -> return $ constant $ BitVector n + Ite _ c e1 e2 -> do + c' <- transB c + trans2BV32 e1 e2 (ite c') + + Op1 _ Abs e -> transBV32 e >>= return . abs + Op1 _ Neg e -> transBV32 e >>= return . negate + Op2 _ Add e1 e2 -> trans2BV32 e1 e2 (+) + Op2 _ Sub e1 e2 -> trans2BV32 e1 e2 (-) + Op2 _ Mul e1 e2 -> trans2BV32 e1 e2 (*) + SVal _ s i -> getBV32Var $ ncVar s i + + e -> error $ "Encountered unhandled expression (BV32): " ++ show e + +transBV64 :: Expr -> Trans (SMTExpr BV64) +transBV64 = \case + ConstI _ n -> return $ constant $ BitVector n + Ite _ c e1 e2 -> do + c' <- transB c + trans2BV64 e1 e2 (ite c') + + Op1 _ Abs e -> transBV64 e >>= return . abs + Op1 _ Neg e -> transBV64 e >>= return . negate + Op2 _ Add e1 e2 -> trans2BV64 e1 e2 (+) + Op2 _ Sub e1 e2 -> trans2BV64 e1 e2 (-) + Op2 _ Mul e1 e2 -> trans2BV64 e1 e2 (*) + SVal _ s i -> getBV64Var $ ncVar s i + + e -> error $ "Encountered unhandled expression (BV64): " ++ show e + +trans2BV8 :: Expr -> Expr -> (SMTExpr BV8 -> SMTExpr BV8 -> SMTExpr a) -> Trans (SMTExpr a) +trans2BV8 e1 e2 f = do + e1' <- transBV8 e1 + e2' <- transBV8 e2 + return $ f e1' e2' + +trans2BV16 :: Expr -> Expr -> (SMTExpr BV16 -> SMTExpr BV16 -> SMTExpr a) -> Trans (SMTExpr a) +trans2BV16 e1 e2 f = do + e1' <- transBV16 e1 + e2' <- transBV16 e2 + return $ f e1' e2' + +trans2BV32 :: Expr -> Expr -> (SMTExpr BV32 -> SMTExpr BV32 -> SMTExpr a) -> Trans (SMTExpr a) +trans2BV32 e1 e2 f = do + e1' <- transBV32 e1 + e2' <- transBV32 e2 + return $ f e1' e2' + +trans2BV64 :: Expr -> Expr -> (SMTExpr BV64 -> SMTExpr BV64 -> SMTExpr a) -> Trans (SMTExpr a) +trans2BV64 e1 e2 f = do + e1' <- transBV64 e1 + e2' <- transBV64 e2 + return $ f e1' e2' + +trans2R :: Expr -> Expr -> (SMTExpr Rational -> SMTExpr Rational -> SMTExpr a) -> Trans (SMTExpr a) +trans2R e1 e2 f = do + e1' <- transR e1 + e2' <- transR e2 + return $ f e1' e2' + +trans2B :: Expr -> Expr -> (SMTExpr Bool -> SMTExpr Bool -> SMTExpr a) -> Trans (SMTExpr a) +trans2B e1 e2 f = do + e1' <- transB e1 + e2' <- transB e2 + return $ f e1' e2' + +----------------------------------------------------- +-- Debug stuff from the the smtlib2 library github -- +----------------------------------------------------- + +debugBackend :: Bool -> b -> DebugBackend b +debugBackend mute b = DebugBackend b stderr (Just 0) Nothing True mute + +namedDebugBackend :: String -> Bool -> b -> DebugBackend b +namedDebugBackend name mute b = DebugBackend b stderr (Just 0) (Just name) True mute + +data DebugBackend b = DebugBackend + { debugBackend' :: b + , debugHandle :: Handle + , debugLines :: Maybe Integer + , debugPrefix :: Maybe String + , debugUseColor :: Bool + , mute :: Bool + } + +instance (SMTBackend b m,MonadIO m) => SMTBackend (DebugBackend b) m where + smtGetNames b = smtGetNames (debugBackend' b) + smtNextName b = smtNextName (debugBackend' b) + smtHandle b req = do + getName <- smtGetNames (debugBackend' b) + nxtName <- smtNextName (debugBackend' b) + (dts,b1) <- smtHandle (debugBackend' b) SMTDeclaredDataTypes + let rendering = renderSMTRequest nxtName getName dts req + case debugPrefix b of + Nothing -> return () + Just prf -> case rendering of + Right "" -> return () + _ -> do + when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull Cyan] + liftIO $ unless (mute b) $ hPutStr (debugHandle b) prf + nline <- case rendering of + Right "" -> return (debugLines b) + _ -> do + nline <- case debugLines b of + Nothing -> return Nothing + Just line -> do + when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull Red] + let line_str = show line + line_str_len = length line_str + line_str' = replicate (4-line_str_len) ' '++line_str++" " + liftIO $ unless (mute b) $ hPutStr (debugHandle b) line_str' + return (Just (line+1)) + case rendering of + Left l -> do + when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull Green] + liftIO $ unless (mute b) $ hPutStrLn (debugHandle b) (show l) + Right msg -> do + when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull White] + liftIO $ unless (mute b) $ hPutStr (debugHandle b) $ unlines $ fmap (\xs -> ';':xs) (lines msg) + return nline + (resp,b2) <- smtHandle b1 req + case renderSMTResponse getName dts req resp of + Nothing -> return () + Just str -> do + when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull Blue] + liftIO $ unless (mute b) $ hPutStrLn (debugHandle b) str + when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset] + return (resp,b { debugBackend' = b2 , debugLines = nline }) + + diff --git a/src/Copilot/Theorem/Tactics.hs b/src/Copilot/Theorem/Tactics.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/Tactics.hs @@ -0,0 +1,17 @@ +module Copilot.Theorem.Tactics + ( instantiate, assume, admit + ) where + +import Copilot.Theorem.Prove + +import Data.Word +import Control.Monad.Writer + +instantiate :: Proof Universal -> Proof Existential +instantiate (Proof p) = Proof p + +assume :: PropRef Universal -> Proof a +assume (PropRef p) = Proof $ tell [Assume p] + +admit :: Proof a +admit = Proof $ tell [Admit] diff --git a/src/Copilot/Theorem/TransSys.hs b/src/Copilot/Theorem/TransSys.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/TransSys.hs @@ -0,0 +1,10 @@ +-------------------------------------------------------------------------------- + +module Copilot.Theorem.TransSys (module X) where + +import Copilot.Theorem.TransSys.Spec as X +import Copilot.Theorem.TransSys.PrettyPrint as X +import Copilot.Theorem.TransSys.Translate as X +import Copilot.Theorem.TransSys.Transform as X + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/TransSys/Cast.hs b/src/Copilot/Theorem/TransSys/Cast.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/TransSys/Cast.hs @@ -0,0 +1,82 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs #-} + +module Copilot.Theorem.TransSys.Cast + ( Dyn + , toDyn + , cast + , castedType + , casting + ) where + +-------------------------------------------------------------------------------- + +import Copilot.Core as C +import Copilot.Core.Type.Equality +import Copilot.Core.Type.Dynamic + +import GHC.Float + +import qualified Copilot.Theorem.TransSys.Type as K + +-------------------------------------------------------------------------------- + +type Dyn = Dynamic Type + +castedType :: Type t -> K.U K.Type +castedType t = case t of + Bool -> K.U K.Bool + Int8 -> K.U K.Integer + Int16 -> K.U K.Integer + Int32 -> K.U K.Integer + Int64 -> K.U K.Integer + Word8 -> K.U K.Integer + Word16 -> K.U K.Integer + Word32 -> K.U K.Integer + Word64 -> K.U K.Integer + Float -> K.U K.Real + Double -> K.U K.Real + +cast :: K.Type t -> Dyn -> t +cast t v + | K.Integer <- t, Just (vi :: Integer) <- _cast v = vi + | K.Bool <- t, Just (vb :: Bool) <- _cast v = vb + | K.Real <- t, Just (vr :: Double) <- _cast v = vr + | otherwise = error "Bad type cast" + +casting :: Type t -> (forall t' . K.Type t' -> a) -> a +casting t f = case castedType t of + K.U K.Bool -> f K.Bool + K.U K.Integer -> f K.Integer + K.U K.Real -> f K.Real + +-------------------------------------------------------------------------------- + +class Casted b where + _cast :: Dyn -> Maybe b + +instance Casted Integer where + _cast (Dynamic v tv) + | Just Refl <- tv =~= Int8 = Just $ toInteger v + | Just Refl <- tv =~= Int16 = Just $ toInteger v + | Just Refl <- tv =~= Int32 = Just $ toInteger v + | Just Refl <- tv =~= Int64 = Just $ toInteger v + | Just Refl <- tv =~= Word16 = Just $ toInteger v + | Just Refl <- tv =~= Word8 = Just $ toInteger v + | Just Refl <- tv =~= Word32 = Just $ toInteger v + | Just Refl <- tv =~= Word64 = Just $ toInteger v + | otherwise = Nothing + +instance Casted Bool where + _cast (Dynamic v tv) + | Just Refl <- tv =~= Bool = Just v + | otherwise = Nothing + +instance Casted Double where + _cast (Dynamic v tv) + | Just Refl <- tv =~= Float = Just $ float2Double v + | Just Refl <- tv =~= Double = Just v + | otherwise = Nothing + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/TransSys/Invariants.hs b/src/Copilot/Theorem/TransSys/Invariants.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/TransSys/Invariants.hs @@ -0,0 +1,16 @@ +{-# OPTIONS_GHC -O0 #-} + +module Copilot.Theorem.TransSys.Invariants + ( HasInvariants (..) + , prop + ) where + +class HasInvariants a where + + invariants :: a -> [(String, Bool)] + + checkInvs :: a -> Bool + checkInvs obj = all snd $ invariants obj + +prop :: String -> Bool -> (String, Bool) +prop = (,) diff --git a/src/Copilot/Theorem/TransSys/Operators.hs b/src/Copilot/Theorem/TransSys/Operators.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/TransSys/Operators.hs @@ -0,0 +1,301 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE GADTs, ExistentialQuantification, LambdaCase, ScopedTypeVariables, + RankNTypes #-} + +module Copilot.Theorem.TransSys.Operators where + +import qualified Copilot.Core as C +import Copilot.Theorem.TransSys.Cast +import Copilot.Theorem.TransSys.Type + +import Copilot.Theorem.Misc.Error as Err + +import Control.Applicative ((<$>)) + +-------------------------------------------------------------------------------- + +data Op1 a where + Not :: Op1 Bool + Neg :: Op1 a + Abs :: Op1 a + Exp :: Op1 a + Sqrt :: Op1 a + Log :: Op1 a + Sin :: Op1 a + Tan :: Op1 a + Cos :: Op1 a + Asin :: Op1 a + Atan :: Op1 a + Acos :: Op1 a + Sinh :: Op1 a + Tanh :: Op1 a + Cosh :: Op1 a + Asinh :: Op1 a + Atanh :: Op1 a + Acosh :: Op1 a + +data Op2 a b where + Eq :: Op2 a Bool + And :: Op2 Bool Bool + Or :: Op2 Bool Bool + + Le :: (Num a) => Op2 a Bool + Lt :: (Num a) => Op2 a Bool + Ge :: (Num a) => Op2 a Bool + Gt :: (Num a) => Op2 a Bool + + Add :: (Num a) => Op2 a a + Sub :: (Num a) => Op2 a a + Mul :: (Num a) => Op2 a a + Mod :: (Num a) => Op2 a a + Fdiv :: (Num a) => Op2 a a + + Pow :: (Num a) => Op2 a a + +------------------------------------------------------------------------------- + +instance Show (Op1 a) where + show op = case op of + Neg -> "-" + Not -> "not" + Abs -> "abs" + Exp -> "exp" + Sqrt -> "sqrt" + Log -> "log" + Sin -> "sin" + Tan -> "tan" + Cos -> "cos" + Asin -> "asin" + Atan -> "atan" + Acos -> "acos" + Sinh -> "sinh" + Tanh -> "tanh" + Cosh -> "cosh" + Asinh -> "asinh" + Atanh -> "atanh" + Acosh -> "acosh" + +instance Show (Op2 a b) where + show op = case op of + Eq -> "=" + Le -> "<=" + Lt -> "<" + Ge -> ">=" + Gt -> ">" + And -> "and" + Or -> "or" + Add -> "+" + Sub -> "-" + Mul -> "*" + Mod -> "mod" + Fdiv -> "/" + Pow -> "^" + +------------------------------------------------------------------------------- + +-- | Some high level utilities to translate a Copilot operator in a standard way +-- | The unhandled operators are monomorphic, and their names are labeled so +-- | that each name corresponds to a unique uninterpreted function with a +-- | monomorphic type. + +-------------------------------------------------------------------------------- + +data UnhandledOp1 = forall a b . + UnhandledOp1 String (Type a) (Type b) + +data UnhandledOp2 = forall a b c . + UnhandledOp2 String (Type a) (Type b) (Type c) + +handleOp1 :: + -- 'm' is the monad in which the computation is made + -- 'resT' is the desired return type of the expression being translated + forall m expr _a _b resT. (Functor m) => + -- The desired return type + Type resT -> + -- The unary operator encountered and its argument + (C.Op1 _a _b, C.Expr _a) -> + -- The monadic function to translate an expression + -- (for recursive calls to be mmadess) + (forall t t'. Type t -> C.Expr t' -> m (expr t)) -> + -- A function to deal with a operators not handled by copilot-kind + (UnhandledOp1 -> m (expr resT)) -> + -- The Op1 constructor of the 'expr' type + (forall t . Type t -> Op1 t -> expr t -> expr t) -> + + m (expr resT) + +handleOp1 resT (op, e) handleExpr notHandledF mkOp = case op of + + C.Not -> boolOp Not (handleExpr Bool e) + + -- Numeric operators + C.Abs _ -> numOp Abs + C.Sign ta -> notHandled ta "sign" + + -- Fractional operators + C.Recip ta -> notHandled ta "recip" + + -- Floating operators + C.Exp _ -> numOp Exp + C.Sqrt _ -> numOp Sqrt + C.Log _ -> numOp Log + C.Sin _ -> numOp Sin + C.Tan _ -> numOp Tan + C.Cos _ -> numOp Cos + C.Asin _ -> numOp Asin + C.Atan _ -> numOp Atan + C.Acos _ -> numOp Acos + C.Sinh _ -> numOp Sinh + C.Tanh _ -> numOp Tanh + C.Cosh _ -> numOp Cosh + C.Asinh _ -> numOp Asinh + C.Atanh _ -> numOp Atanh + C.Acosh _ -> numOp Acosh + + -- Bitwise operators. + C.BwNot ta -> notHandled ta "bwnot" + + -- Casting operator. + C.Cast _ tb -> castTo tb + + where + boolOp :: Op1 Bool -> m (expr Bool) -> m (expr resT) + boolOp op e = case resT of + Bool -> (mkOp resT op) <$> e + _ -> Err.impossible typeErrMsg + + numOp :: Op1 resT -> m (expr resT) + numOp op = (mkOp resT op) <$> (handleExpr resT e) + + -- Casting from Integer (Only possible solution) + castTo :: C.Type ctb -> m (expr resT) + castTo tb = casting tb $ \tb' -> case (tb', resT) of + (Integer, Integer) -> handleExpr Integer e + (Real, Real) -> handleExpr Real e + _ -> Err.impossible typeErrMsg + + notHandled :: + C.Type a -> String -> m (expr resT) + notHandled ta s = casting ta $ \ta' -> + notHandledF $ UnhandledOp1 s ta' resT + +-------------------------------------------------------------------------------- + +-- See the 'handleOp1' function for documentation +handleOp2 :: + forall m expr _a _b _c resT . (Monad m) => + Type resT -> + (C.Op2 _a _b _c, C.Expr _a, C.Expr _b) -> + (forall t t'. Type t -> C.Expr t' -> m (expr t)) -> + (UnhandledOp2 -> m (expr resT)) -> + (forall t a . Type t -> Op2 a t -> expr a -> expr a -> expr t) -> + (expr Bool -> expr Bool) -> + m (expr resT) + + +handleOp2 resT (op, e1, e2) handleExpr notHandledF mkOp notOp = case op of + + C.And -> boolConnector And + C.Or -> boolConnector Or + + -- Numeric operators + C.Add _ -> numOp Add + C.Sub _ -> numOp Sub + C.Mul _ -> numOp Mul + + -- Integral operators. + C.Mod _ -> numOp Mod + C.Div ta -> notHandled ta "div" + + -- Fractional operators. + C.Fdiv _ -> numOp Fdiv + + -- Floating operators. + C.Pow _ -> numOp Pow + C.Logb ta -> notHandled ta "logb" + + -- Equality operators. + C.Eq ta -> eqOp ta + C.Ne ta -> neqOp ta + + -- Relational operators. + C.Le ta -> numComp ta Le + C.Ge ta -> numComp ta Ge + C.Lt ta -> numComp ta Lt + C.Gt ta -> numComp ta Gt + + -- Bitwise operators. + C.BwAnd ta -> notHandled ta "bwand" + C.BwOr ta -> notHandled ta "bwor" + C.BwXor ta -> notHandled ta "bwxor" + + -- In fact, '_tb' is ignored caused it can only + -- be casted to 'Integer', like 'ta' + C.BwShiftL ta _tb -> notHandled ta "bwshiftl" + C.BwShiftR ta _tb -> notHandled ta "bwshiftr" + + where + + boolOp :: Op2 a Bool -> expr a -> expr a -> expr resT + boolOp op e1' e2' = case resT of + Bool -> mkOp resT op e1' e2' + _ -> Err.impossible typeErrMsg + + boolConnector :: Op2 Bool Bool -> m (expr resT) + boolConnector op = do + e1' <- handleExpr Bool e1 + e2' <- handleExpr Bool e2 + return $ boolOp op e1' e2' + + eqOp :: C.Type cta -> m (expr resT) + eqOp ta = casting ta $ \ta' -> do + e1' <- handleExpr ta' e1 + e2' <- handleExpr ta' e2 + return $ boolOp Eq e1' e2' + + neqOp :: C.Type cta -> m (expr resT) + neqOp ta = case resT of + Bool -> do + e <- eqOp ta + return $ notOp e + _ -> Err.impossible typeErrMsg + + numOp :: (forall num . (Num num) => Op2 num num) -> m (expr resT) + numOp op = case resT of + Integer -> do + e1' <- handleExpr Integer e1 + e2' <- handleExpr Integer e2 + return $ mkOp resT op e1' e2' + + Real -> do + e1' <- handleExpr Real e1 + e2' <- handleExpr Real e2 + return $ mkOp resT op e1' e2' + + _ -> Err.impossible typeErrMsg + + numComp :: + C.Type cta -> + (forall num . (Num num) => Op2 num Bool) -> m (expr resT) + numComp ta op = casting ta $ \case + Integer -> do + e1' <- handleExpr Integer e1 + e2' <- handleExpr Integer e2 + return $ boolOp op e1' e2' + Real -> do + e1' <- handleExpr Real e1 + e2' <- handleExpr Real e2 + return $ boolOp op e1' e2' + _ -> Err.impossible typeErrMsg + + notHandled :: forall a . C.Type a -> String -> m (expr resT) + notHandled ta s = casting ta $ \ta' -> + notHandledF (UnhandledOp2 s ta' ta' ta') + +-------------------------------------------------------------------------------- + +typeErrMsg :: String +typeErrMsg = "Unexpected type error in 'Misc.CoreOperators'" + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/TransSys/PrettyPrint.hs b/src/Copilot/Theorem/TransSys/PrettyPrint.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/TransSys/PrettyPrint.hs @@ -0,0 +1,121 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE NamedFieldPuns, GADTs #-} + +module Copilot.Theorem.TransSys.PrettyPrint ( prettyPrint ) where + +import Copilot.Theorem.TransSys.Spec + +import Text.PrettyPrint.HughesPJ + +import qualified Data.Map as Map +import qualified Data.Bimap as Bimap + +-------------------------------------------------------------------------------- + +indent = nest 4 +emptyLine = text "" + +prettyPrint :: TransSys -> String +prettyPrint = render . pSpec + +pSpec :: TransSys -> Doc +pSpec spec = items $$ props + where + items = foldr (($$) . pNode) empty (specNodes spec) + props = text "PROPS" $$ + Map.foldrWithKey (\k -> ($$) . pProp k) + empty (specProps spec) + +pProp pId extvar = quotes (text pId) <+> text "is" <+> pExtVar extvar + +pType :: Type t -> Doc +pType = text . show + +pList :: (t -> Doc) -> [t] -> Doc +pList f l = brackets (hcat . punctuate (comma <> space) $ map f l) + +pNode :: Node -> Doc +pNode n = + header $$ imported $$ local $$ constrs $$ emptyLine + where + header = + text "NODE" + <+> quotes (text $ nodeId n) + <+> text "DEPENDS ON" + <+> pList text (nodeDependencies n) + + imported + | Bimap.null (nodeImportedVars n) = empty + | otherwise = text "IMPORTS" $$ indent + (Map.foldrWithKey (\k -> ($$) . pIVar k) + empty (Bimap.toMap $ nodeImportedVars n)) + + local + | Map.null (nodeLocalVars n) = empty + | otherwise = text "DEFINES" $$ indent + (Map.foldrWithKey (\k -> ($$) . pLVar k) + empty (nodeLocalVars n)) + + constrs = case nodeConstrs n of + [] -> empty + l -> text "WITH CONSTRAINTS" $$ + foldr (($$) . pExpr) empty l + +pConst :: Type t -> t -> Doc +pConst Integer v = text $ show v +pConst Real v = text $ show v +pConst Bool v = text $ show v + +pExtVar :: ExtVar -> Doc +pExtVar (ExtVar n v) = parens (text n <+> text ":" <+> text (varName v)) + +pIVar :: Var -> ExtVar -> Doc +pIVar v ev = + pExtVar ev + <+> text "as" <+> quotes (text (varName v)) + +pLVar :: Var -> VarDescr -> Doc +pLVar l (VarDescr {varType, varDef}) = header $$ indent body + where header = + text (varName l) + <+> text ":" + <+> pType varType + <+> text "=" + + body = case varDef of + Pre val var -> + pConst varType val + <+> text "->" <+> text "pre" + <+> text (varName var) + Expr e -> pExpr e + + Constrs cs -> + text "{" + <+> (hsep . punctuate (space <> text ";" <> space)) (map pExpr cs) + <+> text "}" + + +pExpr :: Expr t -> Doc + +pExpr (Const t v) = pConst t v + +pExpr (Ite _ c e1 e2) = + text "if" <+> pExpr c + <+> text "then" <+> pExpr e1 + <+> text "else" <+> pExpr e2 + +pExpr (Op1 _ op e) = pOp1 op <+> parens (pExpr e) + +pExpr (Op2 _ op e1 e2) = + parens (pExpr e1) <+> pOp2 op <+> parens (pExpr e2) + +pExpr (VarE _ v) = text (varName v) + +pOp1 :: Op1 a -> Doc +pOp1 = text . show + +pOp2 :: Op2 a b -> Doc +pOp2 = text . show + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/TransSys/Renaming.hs b/src/Copilot/Theorem/TransSys/Renaming.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/TransSys/Renaming.hs @@ -0,0 +1,74 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +module Copilot.Theorem.TransSys.Renaming + ( Renaming + , addReservedName + , rename + , getFreshName + , runRenaming + , getRenamingF + ) where + +import Copilot.Theorem.TransSys.Spec + +import Control.Monad.State.Lazy +import Control.Applicative + +import Data.Maybe (fromMaybe) +import Data.Map (Map) +import Data.Set (Set, member) + +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified Data.List as List + +-------------------------------------------------------------------------------- + +newtype Renaming a = Renaming (State RenamingST a) + deriving (Applicative, Monad, Functor) + +data RenamingST = RenamingST + { _reservedNames :: Set Var + , _renaming :: Map ExtVar Var } + +-------------------------------------------------------------------------------- + +addReservedName :: Var -> Renaming () +addReservedName v = + Renaming $ modify $ \st -> + st {_reservedNames = Set.insert v (_reservedNames st)} + + +getFreshName :: [Var] -> Renaming Var +getFreshName vs = do + usedNames <- _reservedNames <$> Renaming get + let varAppend (Var s) = Var $ s ++ "_" + applicants = vs ++ List.iterate varAppend (head vs) + v = case dropWhile (`member` usedNames) applicants of + v:_ -> v + [] -> error "No more names available" + addReservedName v + return v + +rename :: NodeId -> Var -> Var -> Renaming () +rename n v v' = + Renaming $ modify $ \st -> + st {_renaming = Map.insert (ExtVar n v) v' (_renaming st)} + +getRenamingF :: Renaming (ExtVar -> Var) +getRenamingF = do + mapping <- _renaming <$> Renaming get + return $ \extv -> fromMaybe (extVarLocalPart extv) (Map.lookup extv mapping) + +runRenaming :: Renaming a -> (a, ExtVar -> Var) +runRenaming m = + evalState st' (RenamingST Set.empty Map.empty) + where + Renaming st' = do + r <- m + f <- getRenamingF + return (r, f) + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/TransSys/Spec.hs b/src/Copilot/Theorem/TransSys/Spec.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/TransSys/Spec.hs @@ -0,0 +1,198 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE ExistentialQuantification, GADTs, RankNTypes #-} + +module Copilot.Theorem.TransSys.Spec + ( module Copilot.Theorem.TransSys.Operators + , module Copilot.Theorem.TransSys.Type + , module Copilot.Theorem.TransSys.Invariants + , TransSys (..) + , Node (..) + , PropId + , NodeId + , Var (..) + , ExtVar (..) + , VarDef (..) + , VarDescr (..) + , Expr (..) + , mkExtVar + , transformExpr + , isTopologicallySorted + , nodeVarsSet + , specDependenciesGraph + , specTopNode ) where + +import Copilot.Theorem.TransSys.Type +import Copilot.Theorem.TransSys.Operators +import Copilot.Theorem.TransSys.Invariants + +import Copilot.Theorem.Misc.Utils + +import Control.Applicative (liftA2) +import Control.Monad (foldM, guard) + +import Data.Maybe +import Data.Monoid (Monoid, (<>), mempty, mconcat) +import Data.Map (Map) +import Data.Set (Set, isSubsetOf, member) +import Data.Bimap (Bimap) + +import qualified Data.List as List +import qualified Data.Map as Map +import qualified Data.Set as Set +import qualified Data.Bimap as Bimap + +-------------------------------------------------------------------------------- + +type NodeId = String +type PropId = String + +data TransSys = TransSys + { specNodes :: [Node] + , specTopNodeId :: NodeId + , specProps :: Map PropId ExtVar } + + +data Node = Node + { nodeId :: NodeId + , nodeDependencies :: [NodeId] + , nodeLocalVars :: Map Var VarDescr + , nodeImportedVars :: Bimap Var ExtVar + , nodeConstrs :: [Expr Bool] } + + +data Var = Var {varName :: String} + deriving (Eq, Show, Ord) + +data ExtVar = ExtVar {extVarNode :: NodeId, extVarLocalPart :: Var } + deriving (Eq, Ord) + +data VarDescr = forall t . VarDescr + { varType :: Type t + , varDef :: VarDef t } + +data VarDef t = Pre t Var | Expr (Expr t) | Constrs [Expr Bool] + +data Expr t where + Const :: Type t -> t -> Expr t + Ite :: Type t -> Expr Bool -> Expr t -> Expr t -> Expr t + Op1 :: Type t -> Op1 t -> Expr t -> Expr t + Op2 :: Type t -> Op2 a t -> Expr a -> Expr a -> Expr t + VarE :: Type t -> Var -> Expr t + +-------------------------------------------------------------------------------- + +mkExtVar node name = ExtVar node (Var name) + +foldExpr :: (Monoid m) => (forall t . Expr t -> m) -> Expr a -> m +foldExpr f expr = f expr <> fargs + where + fargs = case expr of + (Ite _ c e1 e2) -> foldExpr f c <> foldExpr f e1 <> foldExpr f e2 + (Op1 _ _ e) -> foldExpr f e + (Op2 _ _ e1 e2) -> foldExpr f e1 <> foldExpr f e2 + _ -> mempty + +foldUExpr :: (Monoid m) => (forall t . Expr t -> m) -> U Expr -> m +foldUExpr f (U e) = foldExpr f e + +transformExpr :: (forall a . Expr a -> Expr a) -> Expr t -> Expr t +transformExpr f = tre + where + tre :: forall t . Expr t -> Expr t + tre (Ite t c e1 e2) = f (Ite t (tre c) (tre e1) (tre e2)) + tre (Op1 t op e) = f (Op1 t op (tre e)) + tre (Op2 t op e1 e2) = f (Op2 t op (tre e1) (tre e2)) + tre e = f e + +-------------------------------------------------------------------------------- + +nodeVarsSet :: Node -> Set Var +nodeVarsSet = liftA2 Set.union + nodeLocalVarsSet + (Map.keysSet . Bimap.toMap . nodeImportedVars) + +nodeLocalVarsSet :: Node -> Set Var +nodeLocalVarsSet = Map.keysSet . nodeLocalVars + +nodeRhsVarsSet :: Node -> Set Var +nodeRhsVarsSet n = + let varOcc (VarE _ v) = Set.singleton v + varOcc _ = Set.empty + + descrRhsVars (VarDescr _ (Expr e)) = foldExpr varOcc e + descrRhsVars (VarDescr _ (Pre _ v)) = Set.singleton v + descrRhsVars (VarDescr _ (Constrs cs)) = + mconcat (map (foldExpr varOcc) cs) + + in Map.fold (Set.union . descrRhsVars) Set.empty (nodeLocalVars n) + +nodeImportedExtVarsSet :: Node -> Set ExtVar +nodeImportedExtVarsSet = Map.keysSet . Bimap.toMapR . nodeImportedVars + +nodeExportedExtVarsSet :: Node -> Set ExtVar +nodeExportedExtVarsSet n = Set.map (ExtVar $ nodeId n) (nodeLocalVarsSet n) + +-------------------------------------------------------------------------------- + +instance HasInvariants Node where + + invariants n = + [ prop "The dependencies declaration doesn't lie" $ + (map extVarNode . Bimap.elems $ nodeImportedVars n) + `isSublistOf` nodeDependencies n + + , prop "All local variables are declared" $ + nodeRhsVarsSet n `isSubsetOf` nodeVarsSet n + + , prop "Never apply 'pre' to an imported var" $ + let preVars = Set.fromList + [v | (VarDescr _ (Pre _ v)) <- Map.elems $ nodeLocalVars n] + in preVars `isSubsetOf` nodeLocalVarsSet n + ] + +-------------------------------------------------------------------------------- + +specNodesIds :: TransSys -> Set NodeId +specNodesIds s = Set.fromList . map nodeId $ specNodes s + +specDependenciesGraph :: TransSys -> Map NodeId [NodeId] +specDependenciesGraph s = + Map.fromList [ (nodeId n, nodeDependencies n) | n <- specNodes s ] + +specTopNode :: TransSys -> Node +specTopNode spec = fromJust $ List.find + ((== specTopNodeId spec) . nodeId) + (specNodes spec) + +-------------------------------------------------------------------------------- + +instance HasInvariants TransSys where + + invariants s = + [ prop "All mentioned nodes are declared" $ + specTopNodeId s `member` specNodesIds s + && Set.fromList [nId | n <- specNodes s, nId <- nodeDependencies n] + `isSubsetOf` specNodesIds s + + , prop "The imported vars are not broken" $ + mconcat (map nodeImportedExtVarsSet $ specNodes s) `isSubsetOf` + mconcat (map nodeExportedExtVarsSet $ specNodes s) + + , prop "The nodes invariants hold" $ all checkInvs (specNodes s) + ] + +isTopologicallySorted :: TransSys -> Bool +isTopologicallySorted spec = + isJust $ foldM inspect Set.empty (specNodes spec) + where inspect acc n = do + guard $ Set.fromList (nodeDependencies n) `isSubsetOf` acc + return . Set.insert (nodeId n) $ acc + +-------------------------------------------------------------------------------- + +-- For debugging purposes +instance Show ExtVar where + show (ExtVar n v) = "(" ++ n ++ " : " ++ show v ++ ")" + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/TransSys/Transform.hs b/src/Copilot/Theorem/TransSys/Transform.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/TransSys/Transform.hs @@ -0,0 +1,267 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE RankNTypes #-} + +module Copilot.Theorem.TransSys.Transform + ( mergeNodes + , inline + , removeCycles + , complete + ) where + +import Copilot.Theorem.TransSys.Spec +import Copilot.Theorem.TransSys.Renaming + +import Copilot.Theorem.Misc.Utils + +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 +prefix s1 (Var s2) = Var $ s1 ++ "." ++ s2 + +ncNodeIdSep = "-" + +-------------------------------------------------------------------------------- + +mergeNodes :: [NodeId] -> TransSys -> TransSys +mergeNodes toMergeIds spec = + spec + { specNodes = newNode : + map (updateOtherNode newNodeId toMergeIds renamingExtF) otherNodes + , specProps = Map.map renamingExtF (specProps spec) } + + where + nodes = specNodes spec + (toMerge, otherNodes) = partition ((`elem` toMergeIds) . nodeId) nodes + + -- Choosing the new node ID. If the top node is merged, + -- its name is kept + newNodeId + | specTopNodeId spec `elem` toMergeIds = specTopNodeId spec + | otherwise = intercalate ncNodeIdSep (sort toMergeIds) + + newNode = Node + { nodeId = newNodeId + , nodeDependencies = dependencies + , nodeImportedVars = importedVars + , nodeLocalVars = localVars + , nodeConstrs = constrs } + + -- Computing the dependencies of the new node + dependencies = nub' + [ id | + n <- toMerge + , id <- nodeDependencies n + , id `notElem` toMergeIds ] + + -- All the work of renaming is done in the monad with the same name + (importedVars, renamingF) = runRenaming $ do + renameLocalVars toMerge + redirectLocalImports toMerge + selectImportedVars toMerge otherNodes dependencies + + -- Converting the variables descriptors + localVars = mergeVarsDescrs toMerge renamingF + + -- Computing the global renaming function + renamingExtF (gv@(ExtVar nId _)) + | nId `elem` toMergeIds = ExtVar newNodeId (renamingF gv) + | otherwise = gv + + constrs = mergeConstrs toMerge renamingF + + +updateOtherNode :: NodeId -> [NodeId] -> (ExtVar -> ExtVar) -> Node -> Node +updateOtherNode newNodeId mergedNodesIds renamingF n = n + { nodeDependencies = + let ds = nodeDependencies n + ds' = ds \\ mergedNodesIds + in if length ds' < length ds then newNodeId : ds' else ds + + , nodeImportedVars = + Bimap.fromList [ (lv, renamingF gv) + | (lv, gv) <- Bimap.toList $ nodeImportedVars n ] + } + + + +updateExpr :: NodeId -> (ExtVar -> Var) -> Expr t -> Expr t +updateExpr nId renamingF = transformExpr aux + where + aux :: forall t. Expr t -> Expr t + aux (VarE t v) = VarE t (renamingF (ExtVar nId v)) + aux e = e + + +mergeVarsDescrs :: [Node] -> (ExtVar -> Var) -> Map Var VarDescr +mergeVarsDescrs toMerge renamingF = Map.fromList $ do + n <- toMerge + let nId = nodeId n + (v, VarDescr t def) <- Map.toList $ nodeLocalVars n + let d' = case def of + Pre val v' -> VarDescr t $ + Pre val $ renamingF (ExtVar nId v') + Expr e -> VarDescr t $ + Expr $ updateExpr nId renamingF e + Constrs cs -> VarDescr t $ + Constrs $ map (updateExpr nId renamingF) cs + + return (renamingF $ ExtVar nId v, d') + +mergeConstrs :: [Node] -> (ExtVar -> Var) -> [Expr Bool] +mergeConstrs toMerge renamingF = + [ updateExpr (nodeId n) renamingF c | n <- toMerge, c <- nodeConstrs n ] + +renameLocalVars :: [Node] -> Renaming () +renameLocalVars toMerge = + forM_ niVars $ \(n, v) -> do + v' <- getFreshName [n `prefix` v] + rename n v v' + where + niVars = [ (nodeId n, v) + | n <- toMerge, (v, _) <- Map.toList (nodeLocalVars n) ] + +selectImportedVars :: [Node] -> [Node] -> [NodeId] + -> Renaming (Bimap Var ExtVar) +selectImportedVars toMerge otherNodes dependencies = + foldM checkImport Bimap.empty depsVars + + where + otherNodesMap = Map.fromList [(nodeId n, n) | n <- otherNodes] + + depsVars = [ (nId, v) + | nId <- dependencies, let n = otherNodesMap ! nId + , v <- Map.keys (nodeLocalVars n)] + + checkImport acc (nId, v) = do + v' <- getFreshName [nId `prefix` v] + bmap <- forM toMerge $ \n' -> + case Bimap.lookupR (ExtVar nId v) + (nodeImportedVars n') of + + Just lv -> rename (nodeId n') lv v' >> return True + Nothing -> return False + + return $ + if True `elem` bmap + then Bimap.insert v' (ExtVar nId v) acc + else acc + + + +redirectLocalImports :: [Node] -> Renaming () +redirectLocalImports toMerge = do + renamingF <- getRenamingF + forM_ x $ \(n, alias, n', v) -> + rename n alias (renamingF (ExtVar n' v)) + + where + mergedNodesSet = Set.fromList [nodeId n | n <- toMerge] + x = do + n <- toMerge + let nId = nodeId n + (alias, ExtVar n' v) <- Bimap.toList (nodeImportedVars n) + guard $ n' `member` mergedNodesSet + return (nId, alias, n', v) + +-------------------------------------------------------------------------------- + +inline :: TransSys -> TransSys +inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec + +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/src/Copilot/Theorem/TransSys/Translate.hs b/src/Copilot/Theorem/TransSys/Translate.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/TransSys/Translate.hs @@ -0,0 +1,286 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE RankNTypes, NamedFieldPuns, ViewPatterns, + ScopedTypeVariables, GADTs, FlexibleContexts #-} + +module Copilot.Theorem.TransSys.Translate ( translate ) where + +import Copilot.Theorem.TransSys.Spec +import Copilot.Theorem.TransSys.Cast +import Copilot.Theorem.Misc.Utils + +import Control.Applicative ((<$>)) +import Control.Monad.State.Lazy + +import Data.Char (isNumber) +import Data.Function (on) + +import Data.Map (Map) +import Data.Bimap (Bimap) + +import qualified Copilot.Core as C +import qualified Data.Map as Map +import qualified Data.Bimap as Bimap + +-------------------------------------------------------------------------------- + +-- Naming conventions +-- These are important in order to avoid name conflicts + +ncSep = "." +ncMain = "out" +ncNode i = "s" ++ show i +ncPropNode s = "prop-" ++ s +ncTopNode = "top" +ncAnonInput = "in" +ncLocal s = "l" ++ dropWhile (not . isNumber) s + +ncExternVarNode name = "ext-" ++ name +ncExternFunNode name = "fun-" ++ name +ncExternArrNode name = "arr-" ++ name + +ncImported :: NodeId -> String -> String +ncImported n s = n ++ ncSep ++ s + +ncTimeAnnot :: String -> Int -> String +ncTimeAnnot s d + | d == 0 = s + | otherwise = s ++ ncSep ++ show d + +-------------------------------------------------------------------------------- + +translate :: C.Spec -> TransSys +translate cspec = + + TransSys { specNodes = [topNode] ++ modelNodes ++ propNodes ++ extVarNodes + , specTopNodeId = topNodeId + , specProps = propBindings } + + where + + topNodeId = ncTopNode + + cprops :: [C.Property] + cprops = C.specProperties cspec + + propBindings :: Map PropId ExtVar + propBindings = Map.fromList $ do + pid <- map C.propertyName cprops + return (pid, mkExtVar topNodeId pid) + + ((modelNodes, propNodes), extvarNodesNames) = runTrans $ + liftM2 (,) (mapM stream (C.specStreams cspec)) (mkPropNodes cprops) + + topNode = mkTopNode topNodeId (map nodeId propNodes) cprops + extVarNodes = map mkExtVarNode extvarNodesNames + +-------------------------------------------------------------------------------- + + +mkTopNode :: String -> [NodeId] -> [C.Property] -> Node +mkTopNode topNodeId dependencies cprops = + Node { nodeId = topNodeId + , nodeDependencies = dependencies + , nodeLocalVars = Map.empty + , nodeImportedVars = importedVars + , nodeConstrs = []} + where + importedVars = Bimap.fromList + [ (Var cp, mkExtVar (ncPropNode cp) ncMain) + | cp <- C.propertyName <$> cprops ] + + + +mkExtVarNode (name, U t) = + Node { nodeId = name + , nodeDependencies = [] + , nodeLocalVars = Map.singleton (Var ncMain) (VarDescr t $ Constrs []) + , nodeImportedVars = Bimap.empty + , nodeConstrs = []} + + +mkPropNodes :: [C.Property] -> Trans [Node] +mkPropNodes = mapM propNode + where + propNode p = do + s <- stream (streamOfProp p) + return $ s {nodeId = ncPropNode (C.propertyName p)} + +-- A dummy ID is given to this stream, which is not a problem +-- because this ID will never be used +streamOfProp :: C.Property -> C.Stream +streamOfProp prop = + C.Stream { C.streamId = 42 + , C.streamBuffer = [] + , C.streamExpr = C.propertyExpr prop + , C.streamExprType = C.Bool } + +-------------------------------------------------------------------------------- + +stream :: C.Stream -> Trans Node +stream (C.Stream { C.streamId + , C.streamBuffer + , C.streamExpr + , C.streamExprType }) + + = casting streamExprType $ \t -> do + + let nodeId = ncNode streamId + outvar i = Var (ncMain `ncTimeAnnot` i) + buf = map (cast t . toDyn streamExprType) streamBuffer + + (e, nodeAuxVars, nodeImportedVars, nodeDependencies) <- + runExprTrans t nodeId streamExpr + + let outputLocals = + let from i [] = Map.singleton (outvar i) (VarDescr t $ Expr e) + from i (b : bs) = + Map.insert (outvar i) + (VarDescr t $ Pre b $ outvar (i + 1)) + $ from (i + 1) bs + in from 0 buf + nodeLocalVars = Map.union nodeAuxVars outputLocals + nodeOutputs = map outvar [0 .. length buf - 1] + + return Node + { nodeId, nodeDependencies, nodeLocalVars + , nodeImportedVars, nodeConstrs = [] } + +-------------------------------------------------------------------------------- + +expr :: Type t -> C.Expr t' -> Trans (Expr t) + +expr t (C.Const t' v) = return $ Const t (cast t $ toDyn t' v) + +expr t (C.Drop _ (fromIntegral -> k :: Int) id) = do + let node = ncNode id + selfRef <- (== node) <$> curNode + let varName = ncMain `ncTimeAnnot` k + let var = Var $ if selfRef then varName else ncImported node varName + unless selfRef $ do + newDep node + newImportedVar var (mkExtVar node varName) + return $ VarE t var + +expr t (C.Label _ _ e) = expr t e + +expr t (C.Local tl _tr id l e) = casting tl $ \tl' -> do + l' <- expr tl' l + newLocal (Var $ ncLocal id) $ VarDescr tl' $ Expr l' + expr t e + +expr t (C.Var _t' id) = return $ VarE t (Var $ ncLocal id) + +expr t (C.Op3 (C.Mux _) cond e1 e2) = do + cond' <- expr Bool cond + e1' <- expr t e1 + e2' <- expr t e2 + return $ Ite t cond' e1' e2' + +expr t (C.ExternVar _ name _) = do + let nodeName = ncExternVarNode name + let localAlias = Var nodeName + newExtVarNode nodeName (U t) + newDep nodeName + newImportedVar localAlias (ExtVar nodeName (Var ncMain)) + return $ VarE t localAlias + +-- TODO : Use uninterpreted functions to handle +-- * Unhandled operators +-- * Extern functions +-- * Extern arrays +-- For now, the result of these operations is a new unconstrained variable + +expr t (C.Op1 op e) = handleOp1 + t (op, e) expr notHandled Op1 + where + notHandled (UnhandledOp1 _opName _ta _tb) = + newUnconstrainedVar t + +expr t (C.Op2 op e1 e2) = handleOp2 + t (op, e1, e2) expr notHandled Op2 (Op1 Bool Not) + where + notHandled (UnhandledOp2 _opName _ta _tb _tc) = + newUnconstrainedVar t + +expr t (C.ExternFun _ta _name _args _ _mtag) = newUnconstrainedVar t + +expr t (C.ExternArray _ _tb _name _ _ind _ _) = newUnconstrainedVar t + +newUnconstrainedVar :: Type t -> Trans (Expr t) +newUnconstrainedVar t = do + newNode <- getFreshNodeName + newLocal (Var newNode) $ VarDescr t $ Constrs [] + newDep newNode + return $ VarE t (Var newNode) + +-------------------------------------------------------------------------------- + +runTrans :: Trans a -> (a, [(NodeId, U Type)]) +runTrans mx = + (x, nubBy' (compare `on` fst) $ _extVarsNodes st) + where + (x, st) = runState mx initState + initState = TransSt + { _lvars = Map.empty + , _importedVars = Bimap.empty + , _dependencies = [] + , _extVarsNodes = [] + , _curNode = "" + , _nextUid = 0 } + +runExprTrans :: + Type t -> NodeId -> C.Expr a -> + Trans (Expr t, Map Var VarDescr, Bimap Var ExtVar, [NodeId]) + +runExprTrans t curNode e = do + modify $ \st -> st { _curNode = curNode } + modify $ \st -> st { _nextUid = 0 } + e' <- expr t e + (lvs, ivs, dps) <- popLocalInfos + return (e', lvs, ivs, dps) + +data TransSt = TransSt + { _lvars :: Map Var VarDescr + , _importedVars :: Bimap Var ExtVar + , _dependencies :: [NodeId] + , _extVarsNodes :: [(NodeId, U Type)] + , _curNode :: NodeId + , _nextUid :: Int } + +type Trans a = State TransSt a + +newDep d = modify $ \s -> s { _dependencies = d : _dependencies s } + +popLocalInfos :: State TransSt (Map Var VarDescr, Bimap Var ExtVar, [NodeId]) +popLocalInfos = do + lvs <- _lvars <$> get + ivs <- _importedVars <$> get + dps <- _dependencies <$> get + modify $ \st -> st + { _lvars = Map.empty + , _importedVars = Bimap.empty + , _dependencies = [] } + return (lvs, ivs, nub' dps) + + +getUid :: Trans Int +getUid = do + uid <- _nextUid <$> get + modify $ \st -> st { _nextUid = uid + 1 } + return uid + +getFreshNodeName :: Trans NodeId +getFreshNodeName = liftM (("_" ++) . show) getUid + +newImportedVar l g = modify $ + \s -> s { _importedVars = Bimap.insert l g (_importedVars s) } + +newLocal l d = modify $ \s -> s { _lvars = Map.insert l d $ _lvars s } + +curNode = _curNode <$> get + +newExtVarNode id t = + modify $ \st -> st { _extVarsNodes = (id, t) : _extVarsNodes st } + +-------------------------------------------------------------------------------- diff --git a/src/Copilot/Theorem/TransSys/Type.hs b/src/Copilot/Theorem/TransSys/Type.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/TransSys/Type.hs @@ -0,0 +1,40 @@ +-------------------------------------------------------------------------------- + +{-# LANGUAGE ExistentialQuantification, GADTs #-} + +module Copilot.Theorem.TransSys.Type + ( Type (..) + , U (..) + , U2 (..) + ) where + +import Copilot.Core.Type.Equality + +-------------------------------------------------------------------------------- + +data Type a where + Bool :: Type Bool + Integer :: Type Integer + Real :: Type Double + +instance EqualType Type where + Bool =~= Bool = Just Refl + Integer =~= Integer = Just Refl + Real =~= Real = Just Refl + _ =~= _ = Nothing + +-------------------------------------------------------------------------------- + +-- For instance, 'U Expr' is the type of an expression of unknown type + +data U f = forall t . U (f t) +data U2 f g = forall t . U2 (f t) (g t) + +-------------------------------------------------------------------------------- + +instance Show (Type t) where + show Integer = "Int" + show Bool = "Bool" + show Real = "Real" + +--------------------------------------------------------------------------------