packages feed

copilot-theorem 2.2.0 → 2.2.1

raw patch · 35 files changed

+306/−316 lines, 35 filesdep ~copilot-coredep ~smtlib2new-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: copilot-core, smtlib2

API changes (from Hackage documentation)

- Copilot.Theorem.Prove: Admit :: Action
- Copilot.Theorem.Prove: Assume :: PropId -> Action
- Copilot.Theorem.Prove: Check :: Prover -> Action
- Copilot.Theorem.Prove: Proof :: Writer [Action] b -> ProofScheme a b
- Copilot.Theorem.Prove: PropRef :: PropId -> PropRef a
+ Copilot.Theorem.Prove: [Admit] :: Action
+ Copilot.Theorem.Prove: [Assume] :: PropId -> Action
+ Copilot.Theorem.Prove: [Check] :: Prover -> Action
+ Copilot.Theorem.Prove: [Proof] :: Writer [Action] b -> ProofScheme a b
+ Copilot.Theorem.Prove: [PropRef] :: PropId -> PropRef a
+ Copilot.Theorem.Prove: combine :: Prover -> Prover -> Prover

Files

README.md view
@@ -7,7 +7,7 @@ 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 :+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@@ -26,12 +26,12 @@  ### Installation instructions -*copilot-theorem* needs the following dependencies to be installed :+*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`+* 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`@@ -53,7 +53,7 @@ boolean stream to a property name with the `prop` construct in the specification. -For instance, here is a straightforward specification declaring one property :+For instance, here is a straightforward specification declaring one property:  ```haskell spec :: Spec@@ -65,7 +65,7 @@  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 :+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.@@ -86,7 +86,7 @@  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 :+`Prover`. The latter is defined like this:  ```haskell data Cex = Cex@@ -120,13 +120,13 @@  and checks if the assumptions logically entail the conclusion. -Two provers are provided by default : `Light` and `Kind2`.+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 :+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@@ -166,7 +166,7 @@ * 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 :+`Options` is an instance of the `Data.Default` typeclass:  ```haskell instance Default Options where@@ -202,7 +202,7 @@ 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` :+As an example, the following prover is used in `Driver.hs`:  ```haskell prover =@@ -215,7 +215,7 @@  ### Proof schemes -Let's consider again this example :+Let's consider again this example:  ```haskell spec :: Spec@@ -235,7 +235,7 @@ 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 :+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.@@ -256,7 +256,7 @@ `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 :+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@@ -277,21 +277,21 @@ set of slides. You can find some additional readings in the *References* section. -### Architecture of copilot-kind+### Architecture of copilot-theorem  #### 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 :+available: -* The **IL** format : a Copilot program is translated into a list of+* 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+* 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@@ -308,7 +308,7 @@  ##### An example -The following program :+The following program:  ```haskell spec = do@@ -319,7 +319,7 @@     fib = [1, 1] ++ (fib + drop 1 fib) ``` -can be translated into this IL specification :+can be translated into this IL specification:  ``` SEQUENCES@@ -336,7 +336,7 @@     'pos' : s0[n] > 0 ``` -or this modular transition system :+or this modular transition system:  ``` NODE 's0' DEPENDS ON []@@ -399,9 +399,9 @@ #### 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 :+basic *k-induction* algorithm [1]. The `Light` directory contains three files: -* `Prover.hs` : the prover and the *k-induction* algorithm are implemented in+* `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@@ -417,16 +417,16 @@ Therefore, each stream definition directly gives us a recurrence equation and initial conditions for the associated sequence. -The translation process mostly :+The translation process mostly: -* onverts the types and operators, using uninterpreted functions to handle+* converts 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 :+sequence, we get:  ``` <step>  (set-logic QF_UFLIA)@@ -468,7 +468,7 @@ ##### Modular transition systems  Let's look at the definition of a *modular transition systems*, in the-`TransSys.Spec` module :+`TransSys.Spec` module:  ```haskell type NodeId = String@@ -513,7 +513,7 @@ 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 :+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@@ -534,12 +534,12 @@ 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 :+transformation which turns this:  ```haskell fib = [1, 1] ++ (fib + drop 1 fib) ```-into this :+into this:  ```haskell fib0 = [1] ++ fib1@@ -607,7 +607,7 @@  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 :+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`.@@ -615,7 +615,7 @@ ### 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+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. @@ -625,7 +625,7 @@ 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` :+`intCounter` function defined in the example `Grey.hs`:  ```haskell intCounter :: Stream Bool -> Stream Word64@@ -638,7 +638,7 @@ 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 :+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@@ -679,7 +679,7 @@  ##### Limitations related to the SMT solvers -The use of SMT solvers introduces two kind of limitations :+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@@ -710,7 +710,7 @@ 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` :+defined in `Copilot.Kind.Lib`:  ```haskell conj :: [Stream Bool] -> Stream Bool@@ -730,7 +730,7 @@ 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+* 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.@@ -824,7 +824,7 @@  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 :+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@@ -843,7 +843,7 @@  ## References -1. *An insight into An insight into SMT-based model checking techniques for+1. *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) @@ -853,7 +853,7 @@ 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*,+4. *Verifying safety properties of Lustre programs: an SMT-based approach*,    PhD thesis, G. Hagen  5. *Understanding IC3*, Aaron R. Bradley
copilot-theorem.cabal view
@@ -6,7 +6,7 @@   Some tools to prove properties on Copilot programs with k-induction model   checking. -version                   : 2.2.0+version                   : 2.2.1 license                   : BSD3 license-file              : LICENSE maintainer                : jonathan.laurent@ens.fr@@ -27,8 +27,19 @@                             -fno-warn-missing-signatures                             -fcontext-stack=100 +                            -fpackage-trust+                            -trust=array+                            -trust=base+                            -trust=containers+                            -trust=copilot-core+                            -trust=directory+                            -trust=exceptions+                            -trust=process+                            -trust=random+                            -trust=unix+   build-depends           : base >= 4.0 && < 5-                          , copilot-core == 2.2.0+                          , copilot-core == 2.2.1                           , mtl                           , containers                           , pretty@@ -40,7 +51,7 @@                           , xml                           , random                           , transformers-                          , smtlib2 >= 0.3+                          , smtlib2 >= 0.3 && < 1.0                           , ansi-terminal    exposed-modules         : Copilot.Theorem@@ -49,29 +60,29 @@                           , 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@@ -82,6 +93,3 @@                           , Copilot.Theorem.TransSys.Invariants                           , Copilot.Theorem.TransSys.Operators                           , Copilot.Theorem.TransSys.Type-                          --
src/Copilot/Theorem.hs view
@@ -1,5 +1,7 @@ -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-}+ module Copilot.Theorem   ( module X   , Proof
src/Copilot/Theorem/IL.hs view
@@ -1,5 +1,7 @@ -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-}+ module Copilot.Theorem.IL (module X) where  import Copilot.Theorem.IL.Spec as X
src/Copilot/Theorem/IL/PrettyPrint.hs view
@@ -1,6 +1,7 @@ ---------------------------------------------------------------------------------  {-# LANGUAGE NamedFieldPuns, GADTs #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.IL.PrettyPrint (prettyPrint, printConstraint) where
src/Copilot/Theorem/IL/Spec.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE ExistentialQuantification, GADTs, LambdaCase #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.IL.Spec   ( Type (..)
src/Copilot/Theorem/IL/Transform.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.IL.Transform ( bsimpl ) where
src/Copilot/Theorem/IL/Translate.hs view
@@ -2,8 +2,9 @@  {-# LANGUAGE RankNTypes, NamedFieldPuns, ScopedTypeVariables, GADTs,              LambdaCase #-}+{-# LANGUAGE Safe #-} -module Copilot.Theorem.IL.Translate ( translate ) where+module Copilot.Theorem.IL.Translate ( translate, translateWithBounds ) where  import Copilot.Theorem.IL.Spec @@ -11,7 +12,6 @@  import qualified Data.Map.Strict as Map -import Control.Applicative ((<$>), (<*)) import Control.Monad.State  import Data.Char@@ -48,8 +48,14 @@ -- | Translates a Copilot specification to an IL specification  translate :: C.Spec -> IL-translate (C.Spec {C.specStreams, C.specProperties}) = runTrans $ do+translate = translate' False +translateWithBounds :: C.Spec -> IL+translateWithBounds = translate' True++translate' :: Bool -> C.Spec -> IL+translate' b (C.Spec {C.specStreams, C.specProperties}) = runTrans b $ do+   let modelInit = concatMap streamInit specStreams    mainConstraints <- mapM streamRec specStreams@@ -81,7 +87,9 @@   C.Word64  -> bound' C.Word64   _         -> return ()   where bound' :: (Bounded a, Integral a) => C.Type a -> Trans ()-        bound' t = localConstraint (Op2 Bool And+        bound' t = do+          b <- addBounds <$> get+          when b $ localConstraint (Op2 Bool And             (Op2 Bool Le (trConst t minBound) s)             (Op2 Bool Ge (trConst t maxBound) s)) @@ -181,6 +189,9 @@   e2'   <- expr e2   newMux cond' (trType t) e1' e2' +expr (C.ExternStruct _ _ _ _) = undefined+expr (C.GetField _ _ _ _) = undefined+ trConst :: C.Type a -> a -> Expr trConst t v = case t of   C.Bool   -> ConstB v@@ -245,7 +256,7 @@   C.Pow t        -> (Pow, trType t)   -- C.Logb t       -> -  C.Eq t         -> (Eq, Bool)+  C.Eq _         -> (Eq, Bool)   -- C.Ne t         ->    C.Le t         -> (Le, trType t)@@ -281,6 +292,7 @@   { localConstraints :: [Expr]   , muxes            :: [(Expr, (Expr, Type, Expr, Expr))]   , nextFresh        :: Integer+  , addBounds        :: Bool   }  newMux :: Expr -> Type -> Expr -> Expr -> Trans Expr@@ -317,8 +329,8 @@ popLocalConstraints = liftM2 (++) (localConstraints <$> get) getMuxes   <* (modify $ \st -> st {localConstraints = [], muxes = []}) -runTrans :: Trans a -> a-runTrans m = evalState m $ TransST [] [] 0+runTrans :: Bool -> Trans a -> a+runTrans b m = evalState m $ TransST [] [] 0 b  --------------------------------------------------------------------------------
src/Copilot/Theorem/Kind2.hs view
@@ -1,5 +1,7 @@ -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-}+ module Copilot.Theorem.Kind2 (module X) where  import Copilot.Theorem.Kind2.AST as X
src/Copilot/Theorem/Kind2/AST.hs view
@@ -1,5 +1,7 @@ -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-}+ module Copilot.Theorem.Kind2.AST where  --------------------------------------------------------------------------------
src/Copilot/Theorem/Kind2/Output.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.Kind2.Output (parseOutput) where
src/Copilot/Theorem/Kind2/PrettyPrint.hs view
@@ -1,5 +1,7 @@ -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-}+ module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where  import Copilot.Theorem.Misc.SExpr
src/Copilot/Theorem/Kind2/Prover.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE Trustworthy #-}  module Copilot.Theorem.Kind2.Prover   ( module Data.Default
src/Copilot/Theorem/Kind2/Translate.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE RankNTypes, ViewPatterns, NamedFieldPuns, GADTs #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.Kind2.Translate   ( toKind2
src/Copilot/Theorem/Misc/Error.hs view
@@ -1,5 +1,7 @@ -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-}+ module Copilot.Theorem.Misc.Error   ( badUse   , impossible
src/Copilot/Theorem/Misc/SExpr.hs view
@@ -1,12 +1,12 @@ --------------------------------------------------------------------------------  {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE Safe #-}  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
src/Copilot/Theorem/Misc/Utils.hs view
@@ -1,5 +1,7 @@ -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-}+ module Copilot.Theorem.Misc.Utils  ( isSublistOf, nub', nubBy', nubEq  , openTempFile
src/Copilot/Theorem/Prove.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE NamedFieldPuns, ViewPatterns, ExistentialQuantification, GADTs #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.Prove   ( Output  (..)@@ -12,13 +13,13 @@   , Universal, Existential   , check   , prove+  , combine   ) where  import qualified Copilot.Core as Core  import Data.List (intercalate)-import Control.Applicative (liftA2, Applicative(..))-import Control.Monad (liftM, ap)+import Control.Applicative (liftA2) import Control.Monad.Writer  --------------------------------------------------------------------------------@@ -64,12 +65,12 @@   (<*>) = ap  instance Monad (ProofScheme a) where-  (Proof p) >>= f = Proof $ p >>= (\a -> case f a of Proof p -> p)+  (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+  Check  :: Prover -> Action+  Assume :: PropId -> Action   Admit  :: Action  --------------------------------------------------------------------------------@@ -109,9 +110,9 @@               putStrLn $ propId ++ ": unknown " ++ "(" ++ intercalate ", " infos ++ ")"               processActions context nextActions -        Assume propId -> do-          putStrLn $ propId ++ ": assumption"-          processActions (propId : context) nextActions+        Assume propId' -> do+          putStrLn $ propId' ++ ": assumption"+          processActions (propId' : context) nextActions          Admit -> do           putStrLn $ propId ++ ": admitted"@@ -148,6 +149,7 @@       closeProverR stR   } +combineOutputs :: [Char] -> [Char] -> Output -> Output -> Output combineOutputs nameL nameR (Output stL msgL) (Output stR msgR) =   Output (combineSt stL stR) infos
src/Copilot/Theorem/Prover/Backend.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.Prover.Backend (SmtFormat(..), Backend(..), SatResult(..)) where
src/Copilot/Theorem/Prover/SMT.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs #-}+{-# LANGUAGE Trustworthy #-}  module Copilot.Theorem.Prover.SMT   ( module Data.Default@@ -24,7 +25,6 @@ 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)@@ -65,7 +65,7 @@ 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.startProver = return . ProofState opts backend Map.empty . translateWithBounds   , P.askProver   = onlySat'   , P.closeProver = const $ return ()   }@@ -73,7 +73,7 @@ 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.startProver = return . ProofState opts backend Map.empty . translateWithBounds   , P.askProver   = onlyValidity'   , P.closeProver = const $ return ()   }@@ -81,7 +81,7 @@ 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.startProver = return . ProofState opts backend Map.empty . translateWithBounds   , P.askProver   = kInduction' 0 0   , P.closeProver = const $ return ()   }@@ -89,7 +89,7 @@ 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.startProver = return . ProofState opts backend Map.empty . translateWithBounds   , P.askProver   = kInduction' (startK opts) (maxK opts)   , P.closeProver = const $ return ()   }
src/Copilot/Theorem/Prover/SMTIO.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE LambdaCase, NamedFieldPuns, RankNTypes, ViewPatterns #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.Prover.SMTIO   ( Solver@@ -15,7 +16,6 @@ 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)
src/Copilot/Theorem/Prover/SMTLib.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE GADTs, FlexibleInstances #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.Prover.SMTLib (SmtLib, interpret) where
src/Copilot/Theorem/Prover/TPTP.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE GADTs, LambdaCase #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.Prover.TPTP (Tptp, interpret) where
src/Copilot/Theorem/Prover/Z3.hs view
@@ -2,6 +2,7 @@  {-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs,     MultiParamTypeClasses, FlexibleContexts #-}+{-# LANGUAGE Trustworthy #-}  module Copilot.Theorem.Prover.Z3   ( module Data.Default@@ -15,13 +16,12 @@ 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.Unit (Unit(..)) import Data.Maybe (fromJust, fromMaybe) import Data.Default (Default(..)) import Data.List (foldl')@@ -120,13 +120,12 @@ data SolverId = Base | Step   deriving (Show, Ord, Eq) -getModels :: [PropId] -> [PropId] -> ProofScript ([Expr], [Expr], [Expr], Bool)+getModels :: [PropId] -> [PropId] -> ProofScript ([Expr], [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)+  return (as ++ as', modelInit, modelRec ++ as ++ as' ++ as'', toCheck, inductive)  getSolver :: SolverId -> ProofScript Solver getSolver sid = do@@ -231,11 +230,11 @@ 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)+kInduction' startK maxK s as ps = (fromMaybe (Output P.Unknown ["proof by " ++ proofKind (toInteger maxK) ++ " failed"]) . fst)   <$> runPS (msum (map induction [(toInteger startK) .. (toInteger maxK)]) <* stopSolvers) s   where     induction k = do-      (modelInit, modelRec, toCheck, inductive) <- getModels as ps+      (assumps, 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]@@ -244,47 +243,56 @@                     ++ [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+      entailment Base assumps [ConstB False] >>= \case         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+        Unsat   -> invalid $ "inconsistent assumptions"+        Sat     -> 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+      (assumps, 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"+      entailment Base assumps [ConstB False] >>= \case+        Unknown -> unknown+        Unsat   -> invalid $ "inconsistent assumptions"+        Sat     -> 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+      (assumps, 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."+      entailment Base assumps [ConstB False] >>= \case+        Unknown -> unknown+        Unsat   -> invalid $ "inconsistent assumptions"+        Sat     -> 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 =@@ -306,6 +314,7 @@   , ratVars  :: Map String (SMTExpr Rational)   } +noVars :: TransState noVars = TransState Map.empty Map.empty Map.empty Map.empty Map.empty Map.empty  getBoolVar :: String -> Trans (SMTExpr Bool)@@ -326,234 +335,163 @@ getRatVar  :: String -> Trans (SMTExpr Rational) getRatVar  = getVar ratVars  (\v s -> s {ratVars  = v}) -getVar proj mod v = do+getVar :: (Unit (SMTAnnotation t), SMTType t) => (TransState -> Map String (SMTExpr t)) -> (Map String (SMTExpr t) -> TransState -> TransState) -> String -> Trans (SMTExpr t)+getVar proj upd v = do   vs <- proj <$> get   case Map.lookup v vs of     Nothing -> do       newVar <- lift $ varNamed v-      modify $ mod $ Map.insert v newVar vs+      modify $ upd $ 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+  ConstB b           -> return $ constant b+  Ite _ c e1 e2      -> ite <$> transB c <*> transB e1 <*> transB e2+  Op1 _ Not e        -> not' <$> transB e+  Op2 _ And e1 e2    -> (.&&.) <$> transB e1 <*> transB e2+  Op2 _ Or e1 e2     -> (.||.) <$> transB e1 <*> transB e2+  Op2 _ Eq e1 e2     -> case typeOf e1 of+    Bool   -> (.==.) <$> transB e1    <*> transB e2+    Real   -> (.==.) <$> transR e1    <*> transR e2+    BV8    -> (.==.) <$> transBV8 e1  <*> transBV8 e2+    BV16   -> (.==.) <$> transBV16 e1 <*> transBV16 e2+    BV32   -> (.==.) <$> transBV32 e1 <*> transBV32 e2+    BV64   -> (.==.) <$> transBV64 e1 <*> transBV64 e2+    SBV8   -> (.==.) <$> transBV8 e1  <*> transBV8 e2+    SBV16  -> (.==.) <$> transBV16 e1 <*> transBV16 e2+    SBV32  -> (.==.) <$> transBV32 e1 <*> transBV32 e2+    SBV64  -> (.==.) <$> transBV64 e1 <*> transBV64 e2+  e@(Op2 _ Le e1 e2) -> case typeOf e1 of+    Bool   -> error $ "Comparing Bools: " ++ show e+    Real   -> (.<=.) <$> transR e1    <*> transR e2+    BV8    -> bvule  <$> transBV8 e1  <*> transBV8 e2+    BV16   -> bvule  <$> transBV16 e1 <*> transBV16 e2+    BV32   -> bvule  <$> transBV32 e1 <*> transBV32 e2+    BV64   -> bvule  <$> transBV64 e1 <*> transBV64 e2+    SBV8   -> bvule  <$> transBV8 e1  <*> transBV8 e2+    SBV16  -> bvule  <$> transBV16 e1 <*> transBV16 e2+    SBV32  -> bvule  <$> transBV32 e1 <*> transBV32 e2+    SBV64  -> bvule  <$> transBV64 e1 <*> transBV64 e2+  e@(Op2 _ Ge e1 e2) -> case typeOf e1 of+    Bool   -> error $ "Comparing Bools: " ++ show e+    Real   -> (.>=.) <$> transR e1    <*> transR e2+    BV8    -> bvuge  <$> transBV8 e1  <*> transBV8 e2+    BV16   -> bvuge  <$> transBV16 e1 <*> transBV16 e2+    BV32   -> bvuge  <$> transBV32 e1 <*> transBV32 e2+    BV64   -> bvuge  <$> transBV64 e1 <*> transBV64 e2+    SBV8   -> bvuge  <$> transBV8 e1  <*> transBV8 e2+    SBV16  -> bvuge  <$> transBV16 e1 <*> transBV16 e2+    SBV32  -> bvuge  <$> transBV32 e1 <*> transBV32 e2+    SBV64  -> bvuge  <$> transBV64 e1 <*> transBV64 e2+  e@(Op2 _ Lt e1 e2) -> case typeOf e1 of+    Bool   -> error $ "Comparing Bools: " ++ show e+    Real   -> (.<.) <$> transR e1    <*> transR e2+    BV8    -> bvult <$> transBV8 e1  <*> transBV8 e2+    BV16   -> bvult <$> transBV16 e1 <*> transBV16 e2+    BV32   -> bvult <$> transBV32 e1 <*> transBV32 e2+    BV64   -> bvult <$> transBV64 e1 <*> transBV64 e2+    SBV8   -> bvult <$> transBV8 e1  <*> transBV8 e2+    SBV16  -> bvult <$> transBV16 e1 <*> transBV16 e2+    SBV32  -> bvult <$> transBV32 e1 <*> transBV32 e2+    SBV64  -> bvult <$> transBV64 e1 <*> transBV64 e2+  e@(Op2 _ Gt e1 e2) -> case typeOf e1 of+    Bool   -> error $ "Comparing Bools: " ++ show e+    Real   -> (.>.) <$> transR e1    <*> transR e2+    BV8    -> bvugt <$> transBV8 e1  <*> transBV8 e2+    BV16   -> bvugt <$> transBV16 e1 <*> transBV16 e2+    BV32   -> bvugt <$> transBV32 e1 <*> transBV32 e2+    BV64   -> bvugt <$> transBV64 e1 <*> transBV64 e2+    SBV8   -> bvugt <$> transBV8 e1  <*> transBV8 e2+    SBV16  -> bvugt <$> transBV16 e1 <*> transBV16 e2+    SBV32  -> bvugt <$> transBV32 e1 <*> transBV32 e2+    SBV64  -> bvugt <$> transBV64 e1 <*> transBV64 e2+  SVal _ s i         -> getBoolVar $ ncVar s i+  e                  -> error $ "Encountered unhandled expression (Bool): " ++ show e +ncVar :: [Char] -> SeqIndex -> [Char] 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)+  ConstR n         -> return $ constant $ toRational n+  Ite _ c e1 e2    -> ite <$> transB c <*> transR e1 <*> transR e2 -  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+  Op1 _ Neg e      -> app neg <$> transR e+  Op1 _ Abs e      -> app SMTAbs <$> transR e -  Op2 _ Pow e1 e2 -> do-    let pow = SMTBuiltIn "^" unit :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational-    trans2R e1 e2 $ \x y -> app pow (x, y)+  Op2 _ Add e1 e2  -> (\x y -> app plus [x, y]) <$> transR e1 <*> transR e2+  Op2 _ Sub e1 e2  -> (\x y -> app minus (x, y)) <$> transR e1 <*> transR e2+  Op2 _ Mul e1 e2  -> (\x y -> app mult [x, y]) <$> transR e1 <*> transR e2+  Op2 _ Fdiv e1 e2 -> divide <$> transR e1 <*> transR e2 -  SVal _ s i -> getRatVar $ ncVar s i+  Op2 _ Pow e1 e2  -> do+    let pow = SMTBuiltIn "^" () :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational+    (\x y -> app pow (x, y)) <$> transR e1 <*> transR e2 -  e -> error $ "Encountered unhandled expression (Rat): " ++ show e+  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+  ConstI _ n      -> return $ constant $ BitVector n+  Ite _ c e1 e2   -> ite <$> transB c <*> transBV8 e1 <*> transBV8 e2+  Op1 _ Abs e     -> abs <$> transBV8 e+  Op1 _ Neg e     -> negate <$> transBV8 e+  Op2 _ Add e1 e2 -> (+) <$> transBV8 e1 <*> transBV8 e2+  Op2 _ Sub e1 e2 -> (-) <$> transBV8 e1 <*> transBV8 e2+  Op2 _ Mul e1 e2 -> (*) <$> transBV8 e1 <*> transBV8 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+  ConstI _ n      -> return $ constant $ BitVector n+  Ite _ c e1 e2   -> ite <$> transB c <*> transBV16 e1 <*> transBV16 e2+  Op1 _ Abs e     -> abs <$> transBV16 e+  Op1 _ Neg e     -> negate <$> transBV16 e+  Op2 _ Add e1 e2 -> (+) <$> transBV16 e1 <*> transBV16 e2+  Op2 _ Sub e1 e2 -> (-) <$> transBV16 e1 <*> transBV16 e2+  Op2 _ Mul e1 e2 -> (*) <$> transBV16 e1 <*> transBV16 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+  ConstI _ n      -> return $ constant $ BitVector n+  Ite _ c e1 e2   -> ite <$> transB c <*> transBV32 e1 <*> transBV32 e2+  Op1 _ Abs e     -> abs <$> transBV32 e+  Op1 _ Neg e     -> negate <$> transBV32 e+  Op2 _ Add e1 e2 -> (+) <$> transBV32 e1 <*> transBV32 e2+  Op2 _ Sub e1 e2 -> (-) <$> transBV32 e1 <*> transBV32 e2+  Op2 _ Mul e1 e2 -> (*) <$> transBV32 e1 <*> transBV32 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'+  ConstI _ n      -> return $ constant $ BitVector n+  Ite _ c e1 e2   -> ite <$> transB c <*> transBV64 e1 <*> transBV64 e2+  Op1 _ Abs e     -> abs <$> transBV64 e+  Op1 _ Neg e     -> negate <$> transBV64 e+  Op2 _ Add e1 e2 -> (+) <$> transBV64 e1 <*> transBV64 e2+  Op2 _ Sub e1 e2 -> (-) <$> transBV64 e1 <*> transBV64 e2+  Op2 _ Mul e1 e2 -> (*) <$> transBV64 e1 <*> transBV64 e2+  SVal _ s i      -> getBV64Var $ ncVar s i+  e               -> error $ "Encountered unhandled expression (BV64): " ++ show e  ----------------------------------------------------- -- 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+  { debugBackend  :: b   , debugHandle   :: Handle   , debugLines    :: Maybe Integer   , debugPrefix   :: Maybe String@@ -562,12 +500,12 @@   }  instance (SMTBackend b m,MonadIO m) => SMTBackend (DebugBackend b) m where-  smtGetNames b = smtGetNames (debugBackend' b)-  smtNextName b = smtNextName (debugBackend' b)+  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+    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 ()@@ -603,6 +541,6 @@         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 })+    return (resp,b { debugBackend = b2 , debugLines = nline })
src/Copilot/Theorem/Tactics.hs view
@@ -1,10 +1,11 @@+{-# LANGUAGE Safe #-}+ module Copilot.Theorem.Tactics   ( instantiate, assume, admit   ) where  import Copilot.Theorem.Prove -import Data.Word import Control.Monad.Writer  instantiate :: Proof Universal -> Proof Existential
src/Copilot/Theorem/TransSys.hs view
@@ -1,5 +1,7 @@ -------------------------------------------------------------------------------- +{-# LANGUAGE Safe #-}+ module Copilot.Theorem.TransSys (module X) where  import Copilot.Theorem.TransSys.Spec as X
src/Copilot/Theorem/TransSys/Cast.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.TransSys.Cast   ( Dyn
src/Copilot/Theorem/TransSys/Invariants.hs view
@@ -1,4 +1,5 @@ {-# OPTIONS_GHC -O0 #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.TransSys.Invariants   ( HasInvariants (..)
src/Copilot/Theorem/TransSys/Operators.hs view
@@ -2,6 +2,7 @@  {-# LANGUAGE GADTs, ExistentialQuantification, LambdaCase, ScopedTypeVariables,              RankNTypes #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.TransSys.Operators where @@ -10,8 +11,6 @@ import Copilot.Theorem.TransSys.Type  import Copilot.Theorem.Misc.Error as Err--import Control.Applicative ((<$>))  --------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys/PrettyPrint.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE NamedFieldPuns, GADTs #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.TransSys.PrettyPrint ( prettyPrint ) where
src/Copilot/Theorem/TransSys/Renaming.hs view
@@ -1,6 +1,6 @@ -------------------------------------------------------------------------------- -{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.TransSys.Renaming   ( Renaming@@ -14,7 +14,6 @@ import Copilot.Theorem.TransSys.Spec  import Control.Monad.State.Lazy-import Control.Applicative  import Data.Maybe (fromMaybe) import Data.Map (Map)@@ -26,8 +25,7 @@  -------------------------------------------------------------------------------- -newtype Renaming a = Renaming (State RenamingST a)-                     deriving (Applicative, Monad, Functor)+type Renaming = State RenamingST  data RenamingST = RenamingST   { _reservedNames :: Set Var@@ -36,14 +34,12 @@ --------------------------------------------------------------------------------  addReservedName :: Var -> Renaming ()-addReservedName v =-  Renaming $ modify $ \st ->+addReservedName v = modify $ \st ->     st {_reservedNames = Set.insert v (_reservedNames st)} - getFreshName :: [Var] -> Renaming Var getFreshName vs = do-  usedNames <- _reservedNames <$> Renaming get+  usedNames <- _reservedNames <$> get   let varAppend (Var s) = Var $ s ++ "_"       applicants = vs ++ List.iterate varAppend (head vs)       v = case dropWhile (`member` usedNames) applicants of@@ -53,20 +49,19 @@   return v  rename :: NodeId -> Var -> Var -> Renaming ()-rename n v v' =-  Renaming $ modify $ \st ->+rename n v v' = modify $ \st ->     st {_renaming = Map.insert (ExtVar n v) v' (_renaming st)}  getRenamingF :: Renaming (ExtVar -> Var) getRenamingF = do-  mapping <- _renaming <$> Renaming get+  mapping <- _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+    st' = do       r <- m       f <- getRenamingF       return (r, f)
src/Copilot/Theorem/TransSys/Spec.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE ExistentialQuantification, GADTs, RankNTypes #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.TransSys.Spec   ( module Copilot.Theorem.TransSys.Operators@@ -32,7 +33,7 @@ import Control.Monad (foldM, guard)  import Data.Maybe-import Data.Monoid (Monoid, (<>), mempty, mconcat)+import Data.Monoid ((<>)) import Data.Map (Map) import Data.Set (Set, isSubsetOf, member) import Data.Bimap (Bimap)
src/Copilot/Theorem/TransSys/Transform.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.TransSys.Transform   ( mergeNodes
src/Copilot/Theorem/TransSys/Translate.hs view
@@ -2,6 +2,7 @@  {-# LANGUAGE RankNTypes, NamedFieldPuns, ViewPatterns,              ScopedTypeVariables, GADTs, FlexibleContexts #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.TransSys.Translate ( translate ) where @@ -9,7 +10,6 @@ import Copilot.Theorem.TransSys.Cast import Copilot.Theorem.Misc.Utils -import Control.Applicative ((<$>)) import Control.Monad.State.Lazy  import Data.Char (isNumber)@@ -203,9 +203,13 @@     notHandled (UnhandledOp2 _opName _ta _tb _tc) =       newUnconstrainedVar t -expr t (C.ExternFun _ta _name _args _ _mtag) = newUnconstrainedVar t+expr t (C.ExternFun _ _ _ _ _) = newUnconstrainedVar t -expr t (C.ExternArray _ _tb _name _ _ind _ _) = newUnconstrainedVar t+expr t (C.ExternArray _ _ _ _ _ _ _) = newUnconstrainedVar t++expr t (C.ExternStruct _ _ _ _) = newUnconstrainedVar t++expr t (C.GetField _ _ _ _) = undefined  newUnconstrainedVar :: Type t -> Trans (Expr t) newUnconstrainedVar t = do
src/Copilot/Theorem/TransSys/Type.hs view
@@ -1,6 +1,7 @@ --------------------------------------------------------------------------------  {-# LANGUAGE ExistentialQuantification, GADTs #-}+{-# LANGUAGE Safe #-}  module Copilot.Theorem.TransSys.Type   ( Type (..)