packages feed

copilot-theorem (empty) → 2.2.0

raw patch · 37 files changed

+5169/−0 lines, 37 filesdep +ansi-terminaldep +basedep +bimapsetup-changed

Dependencies added: ansi-terminal, base, bimap, containers, copilot-core, data-default, directory, mtl, parsec, pretty, process, random, smtlib2, transformers, xml

Files

+ LICENSE view
@@ -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.
+ README.md view
@@ -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 :++```+<step>  (set-logic QF_UFLIA)+<step>  (declare-fun n () Int)+<step>  (declare-fun s0 (Int) Int)+<step>  (assert (= (s0 (+ n 2)) (+ (s0 (+ n 0)) (s0 (+ n 1)))))+<step>  (assert (= (s0 (+ n 3)) (+ (s0 (+ n 1)) (s0 (+ n 2)))))+<step>  (assert (> (s0 (+ n 0)) 0))+<step>  (push 1)+<step>  (assert (or false (not (> (s0 (+ n 1)) 0))))+<step>  (check-sat)+<step>  (pop 1)+<step>  (assert (= (s0 (+ n 4)) (+ (s0 (+ n 2)) (s0 (+ n 3)))))+<step>  (assert (> (s0 (+ n 1)) 0))+<step>  (push 1)+<step>  (assert (or false (not (> (s0 (+ n 2)) 0))))+<step>  (check-sat)+unsat+<step>  (pop 1)+```++Here, we just kept the outputs related to the `<step>` 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
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ copilot-theorem.cabal view
@@ -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+                          ++
+ src/Copilot/Theorem.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/IL.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/IL/PrettyPrint.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/IL/Spec.hs view
@@ -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)++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/IL/Transform.hs view
@@ -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+
+ src/Copilot/Theorem/IL/Translate.hs view
@@ -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++--------------------------------------------------------------------------------+
+ src/Copilot/Theorem/Kind2.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Kind2/AST.hs view
@@ -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]++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Kind2/Output.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Kind2/PrettyPrint.hs view
@@ -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"++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Kind2/Prover.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Kind2/Translate.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Misc/Error.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Misc/SExpr.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Misc/Utils.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Prove.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Prover/Backend.hs view
@@ -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+
+ src/Copilot/Theorem/Prover/SMT.hs view
@@ -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)++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Prover/SMTIO.hs view
@@ -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 }++--------------------------------------------------------------------------------+
+ src/Copilot/Theorem/Prover/SMTLib.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Prover/TPTP.hs view
@@ -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   -> "^"++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/Prover/Z3.hs view
@@ -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 })++
+ src/Copilot/Theorem/Tactics.hs view
@@ -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]
+ src/Copilot/Theorem/TransSys.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/TransSys/Cast.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/TransSys/Invariants.hs view
@@ -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 = (,)
+ src/Copilot/Theorem/TransSys/Operators.hs view
@@ -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'"++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/TransSys/PrettyPrint.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/TransSys/Renaming.hs view
@@ -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)++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/TransSys/Spec.hs view
@@ -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 ++ ")"++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/TransSys/Transform.hs view
@@ -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++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/TransSys/Translate.hs view
@@ -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 }++--------------------------------------------------------------------------------
+ src/Copilot/Theorem/TransSys/Type.hs view
@@ -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"++--------------------------------------------------------------------------------