diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,7 @@ +2021-03-07 + * Version bump (3.2.1). (#15). + * Completed the documentation. (#11, #14). + 2020-12-06 * Version bump (3.2). * Update description, bug-reports and homepage field in cabal file diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal --- a/copilot-theorem.cabal +++ b/copilot-theorem.cabal @@ -14,7 +14,7 @@ . -version : 3.2 +version : 3.2.1 license : BSD3 license-file : LICENSE maintainer : jonathan.laurent@ens.fr @@ -55,18 +55,23 @@ build-depends : base >= 4.9 && < 5 , ansi-terminal >= 0.8 && < 0.10 , bimap >= 0.3 && < 0.4 + , bv-sized >= 1.0.2 && < 1.1 , containers >= 0.4 && < 0.7 , data-default >= 0.7 && < 0.8 , directory >= 1.3 && < 1.4 + , filepath >= 1.4.2 && < 1.5 , mtl >= 2.0 && < 2.3 + , panic >= 0.4.0 && < 0.5 , parsec >= 2.0 && < 3.2 + , parameterized-utils >= 2.1.1 && < 2.2 , pretty >= 1.0 && < 1.2 , process >= 1.6 && < 1.7 , random >= 1.1 && < 1.2 , transformers >= 0.5 && < 0.6 , xml >= 1.3 && < 1.4 + , what4 >= 1.0 && < 1.1 - , copilot-core >= 3.2 && < 3.3 + , copilot-core >= 3.2.1 && < 3.3 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove @@ -74,6 +79,7 @@ , Copilot.Theorem.Prover.SMT -- , Copilot.Theorem.Prover.Z3 , Copilot.Theorem.Kind2.Prover + , Copilot.Theorem.What4 other-modules : Copilot.Theorem.Tactics @@ -107,3 +113,4 @@ , Copilot.Theorem.TransSys.Invariants , Copilot.Theorem.TransSys.Operators , Copilot.Theorem.TransSys.Type + diff --git a/src/Copilot/Theorem.hs b/src/Copilot/Theorem.hs --- a/src/Copilot/Theorem.hs +++ b/src/Copilot/Theorem.hs @@ -2,6 +2,17 @@ {-# LANGUAGE Safe #-} +-- | 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 prover producing native inputs for the Kind2 model checker. +-- +-- * A What4 backend that uses SMT solvers to prove safety properties. + module Copilot.Theorem ( module X , Proof diff --git a/src/Copilot/Theorem/IL.hs b/src/Copilot/Theorem/IL.hs --- a/src/Copilot/Theorem/IL.hs +++ b/src/Copilot/Theorem/IL.hs @@ -2,6 +2,14 @@ {-# LANGUAGE Safe #-} +-- | Each prover first translates the Copilot specification into an +-- intermediate representation best suited for model checking. +-- +-- This module and the ones in the same namespace implement 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. + module Copilot.Theorem.IL (module X) where import Copilot.Theorem.IL.Spec as X diff --git a/src/Copilot/Theorem/IL/PrettyPrint.hs b/src/Copilot/Theorem/IL/PrettyPrint.hs --- a/src/Copilot/Theorem/IL/PrettyPrint.hs +++ b/src/Copilot/Theorem/IL/PrettyPrint.hs @@ -3,6 +3,8 @@ {-# LANGUAGE NamedFieldPuns, GADTs #-} {-# LANGUAGE Safe #-} +-- | This module implements a pretty printer for the IL format, an intermediate +-- representation used in copilot-theorem to facilitate model checking. module Copilot.Theorem.IL.PrettyPrint (prettyPrint, printConstraint) where import Copilot.Theorem.IL.Spec @@ -13,9 +15,11 @@ -------------------------------------------------------------------------------- +-- | Pretty print an IL specification. prettyPrint :: IL -> String prettyPrint = render . ppSpec +-- | Pretty print an IL constraint expression. printConstraint :: Expr -> String printConstraint = render . ppExpr diff --git a/src/Copilot/Theorem/IL/Spec.hs b/src/Copilot/Theorem/IL/Spec.hs --- a/src/Copilot/Theorem/IL/Spec.hs +++ b/src/Copilot/Theorem/IL/Spec.hs @@ -3,6 +3,18 @@ {-# LANGUAGE ExistentialQuantification, GADTs, LambdaCase #-} {-# LANGUAGE Safe #-} +-- | This module implements the specification language for the IL format, an +-- intermediate representation used in copilot-theorem to facilitate model +-- checking. +-- +-- 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 representation is partly inspired by the IL language described in +-- Hagen, G.E., /VERIFYING SAFETY PROPERTIES OF LUSTRE PROGRAMS: AN SMT-BASED/ +-- /APPROACH/, 2008. + module Copilot.Theorem.IL.Spec ( Type (..) , Op1 (..) @@ -25,11 +37,16 @@ -------------------------------------------------------------------------------- +-- | Identifier of a sequence. type SeqId = String -data SeqIndex = Fixed Integer | Var Integer +-- | Index within a sequence. +data SeqIndex = Fixed Integer -- ^ An absolute index in the sequence. + | Var Integer -- ^ An index relative to the current time-step. deriving (Eq, Ord, Show) +-- | Idealized types. These differ from Copilot types in that, notionally, +-- reals actually denote real numbers. data Type = Bool | Real | SBV8 | SBV16 | SBV32 | SBV64 | BV8 | BV16 | BV32 | BV64 @@ -48,19 +65,21 @@ BV32 -> "BV32" BV64 -> "BV64" +-- | Idealized representation of a Copilot expression. 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] + = ConstB Bool -- ^ Constant boolean. + | ConstR Double -- ^ Constant real. + | ConstI Type Integer -- ^ Constant integer. + | Ite Type Expr Expr Expr -- ^ If-then-else. + | Op1 Type Op1 Expr -- ^ Apply a unary operator. + | Op2 Type Op2 Expr Expr -- ^ Apply a binary operator. + | SVal Type SeqId SeqIndex -- ^ Refer to a value in another sequence. + | FunApp Type String [Expr] -- ^ Function application. deriving (Eq, Ord, Show) -------------------------------------------------------------------------------- +-- | A description of a variable (or function) together with its type. data VarDescr = VarDescr { varName :: String , varType :: Type @@ -75,13 +94,16 @@ -------------------------------------------------------------------------------- +-- | Identifier for a property. type PropId = String +-- | Description of a sequence. data SeqDescr = SeqDescr { seqId :: SeqId , seqType :: Type } +-- | An IL specification. data IL = IL { modelInit :: [Expr] , modelRec :: [Expr] @@ -91,10 +113,12 @@ -------------------------------------------------------------------------------- +-- | Unary operators. data Op1 = Not | Neg | Abs | Exp | Sqrt | Log | Sin | Tan | Cos | Asin | Atan | Acos | Sinh | Tanh | Cosh | Asinh | Atanh | Acosh deriving (Eq, Ord) +-- | Binary operators. data Op2 = Eq | And | Or | Le | Lt | Ge | Gt | Add | Sub | Mul | Mod | Fdiv | Pow deriving (Eq, Ord) @@ -145,6 +169,7 @@ ------------------------------------------------------------------------------- +-- | Return the type of an expression. typeOf :: Expr -> Type typeOf e = case e of ConstB _ -> Bool @@ -156,12 +181,15 @@ SVal t _ _ -> t FunApp t _ _ -> t +-- | An index to the current element of a sequence. _n_ :: SeqIndex _n_ = Var 0 +-- | An index to a future element of a sequence. _n_plus :: (Integral a) => a -> SeqIndex _n_plus d = Var (toInteger d) +-- | Evaluate an expression at specific index in the sequence. evalAt :: SeqIndex -> Expr -> Expr evalAt _ e@(ConstB _) = e evalAt _ e@(ConstR _) = e diff --git a/src/Copilot/Theorem/IL/Transform.hs b/src/Copilot/Theorem/IL/Transform.hs --- a/src/Copilot/Theorem/IL/Transform.hs +++ b/src/Copilot/Theorem/IL/Transform.hs @@ -1,11 +1,17 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE Safe #-} +-- | Simplify IL expressions by partly evaluating operations on booleans. module Copilot.Theorem.IL.Transform ( bsimpl ) where import Copilot.Theorem.IL.Spec --- | A transformation intended to remove boolean literals. +-- | Simplify IL expressions by partly evaluating operations on booleans, +-- eliminating some boolean literals. +-- +-- For example, an if-then-else in which the condition is literally the +-- constant True or the constant False can be reduced to an operation without +-- choice in which the appropriate branch of the if-then-else is used instead. bsimpl :: Expr -> Expr bsimpl = until (\x -> bsimpl' x == x) bsimpl' where diff --git a/src/Copilot/Theorem/IL/Translate.hs b/src/Copilot/Theorem/IL/Translate.hs --- a/src/Copilot/Theorem/IL/Translate.hs +++ b/src/Copilot/Theorem/IL/Translate.hs @@ -4,6 +4,7 @@ LambdaCase #-} {-# LANGUAGE Safe #-} +-- | Translate Copilot specifications into IL specifications. module Copilot.Theorem.IL.Translate ( translate, translateWithBounds ) where import Copilot.Theorem.IL.Spec @@ -44,11 +45,13 @@ -------------------------------------------------------------------------------- --- | Translates a Copilot specification to an IL specification - +-- | Translate a Copilot specification to an IL specification. translate :: C.Spec -> IL translate = translate' False +-- | Translate a Copilot specification to an IL specification, adding +-- constraints for limiting the values of numeric expressions to known bounds +-- based on their specific types (only for integers or natural numbers). translateWithBounds :: C.Spec -> IL translateWithBounds = translate' True @@ -273,6 +276,7 @@ -------------------------------------------------------------------------------- +-- | Translation state. data TransST = TransST { localConstraints :: [Expr] , muxes :: [(Expr, (Expr, Type, Expr, Expr))] @@ -299,6 +303,7 @@ , Op2 Bool Or c (Op2 Bool Eq v e2) ] +-- | A state monad over the translation state ('TransST'). type Trans = State TransST fresh :: Trans Integer diff --git a/src/Copilot/Theorem/Kind2.hs b/src/Copilot/Theorem/Kind2.hs --- a/src/Copilot/Theorem/Kind2.hs +++ b/src/Copilot/Theorem/Kind2.hs @@ -2,6 +2,9 @@ {-# LANGUAGE Safe #-} +-- | Copilot backend for the SMT +-- based model checker. + module Copilot.Theorem.Kind2 (module X) where import Copilot.Theorem.Kind2.AST as X diff --git a/src/Copilot/Theorem/Kind2/AST.hs b/src/Copilot/Theorem/Kind2/AST.hs --- a/src/Copilot/Theorem/Kind2/AST.hs +++ b/src/Copilot/Theorem/Kind2/AST.hs @@ -2,35 +2,52 @@ {-# LANGUAGE Safe #-} +-- | Abstract syntax tree of Kind2 files. module Copilot.Theorem.Kind2.AST where -------------------------------------------------------------------------------- +-- | A file is a sequence of predicates and propositions. data File = File { filePreds :: [PredDef] , fileProps :: [Prop] } +-- | A proposition is defined by a term. data Prop = Prop { propName :: String , propTerm :: Term } +-- | A predicate definition. data PredDef = PredDef - { predId :: String - , predStateVars :: [StateVarDef] - , predInit :: Term - , predTrans :: Term } + { predId :: String -- ^ Identifier for the predicate. + , predStateVars :: [StateVarDef] -- ^ Variables identifying the states in the + -- underlying state transition system. + , predInit :: Term -- ^ Predicate that holds for initial + -- states. + , predTrans :: Term -- ^ Predicate that holds for two states, if + -- there is state transition between them. + } +-- | A definition of a state variable. data StateVarDef = StateVarDef - { varId :: String - , varType :: Type - , varFlags :: [StateVarFlag] } + { varId :: String -- ^ Name of the variable. + , varType :: Type -- ^ Type of the variable. + , varFlags :: [StateVarFlag] } -- ^ Flags for the variable. +-- | Types used in Kind2 files to represent Copilot types. +-- +-- The Kind2 backend provides functions to, additionally, constrain the range +-- of numeric values depending on their Copilot type ('Int8', 'Int16', etc.). data Type = Int | Real | Bool +-- | Possible flags for a state variable. data StateVarFlag = FConst +-- | Type of the predicate, either belonging to an initial state or a pair of +-- states with a transition. data PredType = Init | Trans +-- | Datatype to describe a term in the Kind language. data Term = ValueLiteral String | PrimedStateVar String diff --git a/src/Copilot/Theorem/Kind2/Output.hs b/src/Copilot/Theorem/Kind2/Output.hs --- a/src/Copilot/Theorem/Kind2/Output.hs +++ b/src/Copilot/Theorem/Kind2/Output.hs @@ -3,6 +3,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Safe #-} +-- | Parse output of Kind2. module Copilot.Theorem.Kind2.Output (parseOutput) where import Text.XML.Light hiding (findChild) @@ -15,7 +16,10 @@ simpleName s = QName s Nothing Nothing -parseOutput :: String -> String -> P.Output +-- | Parse output of Kind2. +parseOutput :: String -- ^ Property whose validity is being checked. + -> String -- ^ XML output of Kind2 + -> P.Output parseOutput prop xml = fromJust $ do root <- parseXMLDoc xml case findAnswer . findPropTag $ root of diff --git a/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/src/Copilot/Theorem/Kind2/PrettyPrint.hs --- a/src/Copilot/Theorem/Kind2/PrettyPrint.hs +++ b/src/Copilot/Theorem/Kind2/PrettyPrint.hs @@ -2,6 +2,7 @@ {-# LANGUAGE Safe #-} +-- | Pretty print a Kind2 file defining predicates and propositions. module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where import Copilot.Theorem.Misc.SExpr @@ -12,19 +13,22 @@ -------------------------------------------------------------------------------- +-- | A tree of expressions, in which the leafs are strings. type SSExpr = SExpr String +-- | Reserved keyword prime. kwPrime = "prime" -------------------------------------------------------------------------------- +-- | Pretty print a Kind2 file. prettyPrint :: File -> String prettyPrint = intercalate "\n\n" . map (SExpr.toString shouldIndent id) . ppFile --- Defines the indentation policy of the S-Expressions +-- | Define the indentation policy of the S-Expressions shouldIndent :: SSExpr -> Bool shouldIndent (Atom _) = False shouldIndent (List [Atom a, Atom _]) = a `notElem` [kwPrime] @@ -32,15 +36,19 @@ -------------------------------------------------------------------------------- +-- | Convert a file into a sequence of expressions. ppFile :: File -> [SSExpr] ppFile (File preds props) = map ppPredDef preds ++ ppProps props +-- | Convert a sequence of propositions into command to check each of them. ppProps :: [Prop] -> [SSExpr] ppProps ps = [ node "check-prop" [ list $ map ppProp ps ] ] +-- | Convert a proposition into an expression. ppProp :: Prop -> SSExpr ppProp (Prop n t) = list [atom n, ppTerm t] +-- | Convert a predicate into an expression. ppPredDef :: PredDef -> SSExpr ppPredDef pd = list [ atom "define-pred" @@ -49,15 +57,18 @@ , node "init" [ppTerm $ predInit pd] , node "trans" [ppTerm $ predTrans pd] ] +-- | Convert a state variable definition into an expression. ppStateVarDef :: StateVarDef -> SSExpr ppStateVarDef svd = list [atom (varId svd), ppType (varType svd)] +-- | Convert a type into an expression. ppType :: Type -> SSExpr ppType Int = atom "Int" ppType Real = atom "Real" ppType Bool = atom "Bool" +-- | Convert a term into an expression. ppTerm :: Term -> SSExpr ppTerm (ValueLiteral c) = atom c ppTerm (PrimedStateVar v) = list [atom kwPrime, atom v] diff --git a/src/Copilot/Theorem/Kind2/Prover.hs b/src/Copilot/Theorem/Kind2/Prover.hs --- a/src/Copilot/Theorem/Kind2/Prover.hs +++ b/src/Copilot/Theorem/Kind2/Prover.hs @@ -3,6 +3,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE Trustworthy #-} +-- | A prover backend based on Kind2. module Copilot.Theorem.Kind2.Prover ( module Data.Default , Options (..) @@ -27,9 +28,13 @@ -------------------------------------------------------------------------------- +-- | Options for Kind2 data Options = Options - { bmcMax :: Int } + { bmcMax :: Int -- ^ Upper bound on the number of unrolling that base and + -- step will perform. A value of 0 means /unlimited/. + } +-- | Default options with unlimited unrolling for base and step. instance Default Options where def = Options { bmcMax = 0 } @@ -37,6 +42,9 @@ { options :: Options , transSys :: TS.TransSys } +-- | A prover backend based on Kind2. +-- +-- The executable @kind2@ must exist and its location be in the @PATH@. kind2Prover :: Options -> Prover kind2Prover opts = Prover { proverName = "Kind2" diff --git a/src/Copilot/Theorem/Kind2/Translate.hs b/src/Copilot/Theorem/Kind2/Translate.hs --- a/src/Copilot/Theorem/Kind2/Translate.hs +++ b/src/Copilot/Theorem/Kind2/Translate.hs @@ -3,6 +3,8 @@ {-# LANGUAGE RankNTypes, ViewPatterns, NamedFieldPuns, GADTs #-} {-# LANGUAGE Safe #-} +-- | Convert modular transition systems ('TransSys') into Kind2 file +-- specifications. module Copilot.Theorem.Kind2.Translate ( toKind2 , Style (..) @@ -36,9 +38,23 @@ -------------------------------------------------------------------------------- +-- | Style of the Kind2 files produced: modular (with multiple separate nodes), +-- or all inlined (with only one node). +-- +-- In the modular style, the graph is simplified to remove cycles by collapsing +-- all nodes participating in a strongly connected components. +-- +-- In the inlined style, the structure of the modular transition system is +-- discarded and the graph is first turned into a /non-modular transition/ +-- /system/ with only one node, which can be then converted into a Kind2 file. data Style = Inlined | Modular -toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> K.File +-- | Produce a Kind2 file that checks the properties specified. +toKind2 :: Style -- ^ Style of the file (modular or inlined). + -> [PropId] -- ^ Assumptions + -> [PropId] -- ^ Properties to be checked + -> TransSys -- ^ Modular transition system holding the system spec + -> K.File toKind2 style assumptions checkedProps spec = addAssumptions spec assumptions $ trSpec (complete spec') predCallsGraph assumptions checkedProps diff --git a/src/Copilot/Theorem/Misc/Error.hs b/src/Copilot/Theorem/Misc/Error.hs --- a/src/Copilot/Theorem/Misc/Error.hs +++ b/src/Copilot/Theorem/Misc/Error.hs @@ -2,6 +2,7 @@ {-# LANGUAGE Safe #-} +-- | Custom functions to report error messages to users. module Copilot.Theorem.Misc.Error ( badUse , impossible @@ -12,21 +13,29 @@ -------------------------------------------------------------------------------- +-- | Tag used with error messages to help users locate the component that +-- failed or reports the error. errorHeader :: String errorHeader = "[Copilot-kind ERROR] " -badUse :: String -> a +-- | Report an error due to an error detected by Copilot (e.g., user error). +badUse :: String -- ^ Description of the error. + -> a badUse s = error $ errorHeader ++ s -impossible :: String -> a +-- | Report an error due to a bug in Copilot. +impossible :: String -- ^ Error information to attach to the message. + -> a impossible s = error $ errorHeader ++ "Unexpected internal error : " ++ s +-- | Report an error due to a bug in Copilot. impossible_ :: a impossible_ = error $ errorHeader ++ "Unexpected internal error" notHandled :: String -> a notHandled s = error $ errorHeader ++ "Not handled : " ++ s +-- | Report an unrecoverable error (e.g., incorrect format). fatal :: String -> a fatal = error diff --git a/src/Copilot/Theorem/Misc/SExpr.hs b/src/Copilot/Theorem/Misc/SExpr.hs --- a/src/Copilot/Theorem/Misc/SExpr.hs +++ b/src/Copilot/Theorem/Misc/SExpr.hs @@ -3,6 +3,8 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE Safe #-} +-- | A representation for structured expression trees, with support for pretty +-- printing and for parsing. module Copilot.Theorem.Misc.SExpr where import Text.ParserCombinators.Parsec @@ -12,20 +14,34 @@ -------------------------------------------------------------------------------- +-- | A structured expression is either an atom, or a sequence of expressions, +-- where the first in the sequence denotes the tag or label of the tree. data SExpr a = Atom a | List [SExpr a] -blank = Atom "" -atom = Atom -- s -unit = List [] -- () +-- | Empty string expression. +blank = Atom "" + +-- | Atomic expression constructor. +atom = Atom -- s + +-- | Empty expression (empty list). +unit = List [] -- () + +-- | Single expression. singleton a = List [Atom a] -- (s) -list = List -- (ss) -node a l = List (Atom a : l) -- (s ss) --------------------------------------------------------------------------------- +-- | Sequence of expressions. +list = List -- (ss) --- A straightforward string representation +-- | Sequence of expressions with a root or main note, and a series of +-- additional expressions or arguments.. +node a l = List (Atom a : l) -- (s ss) +-------------------------------------------------------------------------------- + +-- A straightforward string representation for 'SExpr's of Strings that +-- parenthesizes lists of expressions. instance Show (SExpr String) where show = PP.render . show' where @@ -35,13 +51,22 @@ -- More advanced printing with some basic indentation +-- | Indent by a given number. indent = nest 1 -toString :: (SExpr a -> Bool) -> (a -> String) -> SExpr a -> String +-- | Pretty print a structured expression as a String. +toString :: (SExpr a -> Bool) -- ^ True if an expression should be indented. + -> (a -> String) -- ^ Pretty print the value inside as 'SExpr'. + -> SExpr a -- ^ Root of 'SExpr' tree. + -> String toString shouldIndent printAtom expr = PP.render (toDoc shouldIndent printAtom expr) -toDoc :: (SExpr a -> Bool) -> (a -> String) -> SExpr a -> Doc +-- | Pretty print a structured expression as a 'Doc', or set of layouts. +toDoc :: (SExpr a -> Bool) -- ^ True if an expression should be indented. + -> (a -> String) -- ^ Pretty print the value inside as 'SExpr'. + -> SExpr a -- ^ Root of 'SExpr' tree. + -> Doc toDoc shouldIndent printAtom expr = case expr of Atom a -> text (printAtom a) List l -> parens (foldl renderItem empty l) @@ -54,6 +79,11 @@ -------------------------------------------------------------------------------- +-- | Parser for strings of characters separated by spaces into a structured +-- tree. +-- +-- Parentheses are interpreted as grouping elements, that is, defining a +-- 'List', which may be empty. parser :: GenParser Char st (SExpr String) parser = choice [try unitP, nodeP, leafP] @@ -72,7 +102,11 @@ void $ char ')' return $ List st - +-- | Parser for strings of characters separated by spaces into a structured +-- tree. +-- +-- Parentheses are interpreted as grouping elements, that is, defining a +-- 'List', which may be empty. parseSExpr :: String -> Maybe (SExpr String) parseSExpr str = case parse parser "" str of Left s -> error (show s) -- Nothing diff --git a/src/Copilot/Theorem/Misc/Utils.hs b/src/Copilot/Theorem/Misc/Utils.hs --- a/src/Copilot/Theorem/Misc/Utils.hs +++ b/src/Copilot/Theorem/Misc/Utils.hs @@ -2,6 +2,7 @@ {-# LANGUAGE Safe #-} +-- | Utility / auxiliary functions. module Copilot.Theorem.Misc.Utils ( isSublistOf, nub', nubBy', nubEq , openTempFile @@ -23,22 +24,35 @@ -------------------------------------------------------------------------------- +-- | True if the given list is a subset of the second list, when both are +-- considered as sets. isSublistOf :: Ord a => [a] -> [a] -> Bool isSublistOf = Set.isSubsetOf `on` Set.fromList +-- | True if both lists contain the same elements, when both are considered as +-- sets. nubEq :: Ord a => [a] -> [a] -> Bool nubEq = (==) `on` Set.fromList --- An efficient version of 'nub' +-- | Remove duplicates from a list. +-- +-- This is an efficient version of 'Data.List.nub' that works for lists with a +-- stronger constraint on the type (i.e., 'Ord', as opposed of +-- 'Data.List.nub''s 'Eq' constraint). nub' :: Ord a => [a] -> [a] nub' = map head . group . sort +-- | Variant of 'nub'' parameterized by the comparison function. 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) +-- | Create a temporary file and open it for writing. +openTempFile :: String -- ^ Directory where the file should be created. + -> String -- ^ Base name for the file (prefix). + -> String -- ^ File extension. + -> IO (String, Handle) openTempFile loc baseName extension = do path <- freshPath diff --git a/src/Copilot/Theorem/Prove.hs b/src/Copilot/Theorem/Prove.hs --- a/src/Copilot/Theorem/Prove.hs +++ b/src/Copilot/Theorem/Prove.hs @@ -3,6 +3,7 @@ {-# LANGUAGE NamedFieldPuns, ViewPatterns, ExistentialQuantification, GADTs #-} {-# LANGUAGE Safe #-} +-- | Connection to theorem provers. module Copilot.Theorem.Prove ( Output (..) , Status (..) @@ -24,17 +25,24 @@ -------------------------------------------------------------------------------- +-- | Output produced by a prover, containing the 'Status' of the proof and +-- additional information. data Output = Output Status [String] +-- | Status returned by a prover when given a specification and a property to +-- prove. 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 --} - +-- | A connection to a prover able to check the satisfiability of +-- specifications. +-- +-- The most important is `askProver`, which takes 3 arguments : +-- +-- * The prover descriptor +-- +-- * A list of properties names which are assumptions +-- +-- * A properties that have to be deduced from these assumptions data Prover = forall r . Prover { proverName :: String , startProver :: Core.Spec -> IO r @@ -42,18 +50,28 @@ , closeProver :: r -> IO () } +-- | A unique property identifier type PropId = String +-- | Reference to a property. data PropRef a where PropRef :: PropId -> PropRef a +-- | Empty datatype to mark proofs of universally quantified predicates. data Universal + +-- | Empty datatype to mark proofs of existentially quantified predicates. data Existential +-- | A proof scheme with unit result. type Proof a = ProofScheme a () +-- | A sequence of computations that generate a trace of required prover +-- 'Action's. type UProof = Writer [Action] () +-- | A proof scheme is a sequence of computations that compute a result and +-- generate a trace of required prover 'Action's. data ProofScheme a b where Proof :: Writer [Action] b -> ProofScheme a b @@ -68,6 +86,7 @@ (Proof p) >>= f = Proof $ p >>= (\a -> case f a of Proof p' -> p') return a = Proof (return a) +-- | Prover actions. data Action where Check :: Prover -> Action Assume :: PropId -> Action @@ -75,9 +94,14 @@ -------------------------------------------------------------------------------- +-- | Record a requirement for satisfiability checking. check :: Prover -> Proof a check prover = Proof $ tell [Check prover] +-- | Try to prove a property in a specification with a given proof scheme. +-- +-- Return 'True' if a proof of satisfiability or validity is found, false +-- otherwise. prove :: Core.Spec -> PropId -> UProof -> IO Bool prove spec propId (execWriter -> actions) = do @@ -118,6 +142,13 @@ putStrLn $ propId ++ ": admitted" processActions (propId : context) nextActions +-- | Combine two provers producing a new prover that will run both provers in +-- parallel and combine their outputs. +-- +-- The results produced by the provers must be consistent. For example, if one +-- of the provers indicates that a property is 'Valid' while another indicates +-- that it is 'Invalid', the combination of both provers will return an +-- 'Error'. combine :: Prover -> Prover -> Prover combine (Prover { proverName = proverNameL diff --git a/src/Copilot/Theorem/Prover/Backend.hs b/src/Copilot/Theorem/Prover/Backend.hs --- a/src/Copilot/Theorem/Prover/Backend.hs +++ b/src/Copilot/Theorem/Prover/Backend.hs @@ -1,12 +1,26 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Safe #-} +-- | Backend to SMT solvers and theorem provers. +-- +-- This module provides three definitions: +-- +-- - A class ('SmtFormat') abstracting over the language used to communicate the +-- desired commands to an SMT solver or theorem prover. +-- +-- - A class ('Backend') abstracting over the backend, which includes the name of +-- the executable, any options and flags necessary, and functions to parse the +-- results and close the communication. +-- +-- - A type ('SatResult') representing a satisfiability result communicated by +-- the SMT solver or theorem prover. module Copilot.Theorem.Prover.Backend (SmtFormat(..), Backend(..), SatResult(..)) where import Copilot.Theorem.IL import System.IO +-- | Format of SMT-Lib commands. class Show a => SmtFormat a where push :: a pop :: a @@ -15,6 +29,7 @@ declFun :: String -> Type -> [Type] -> a assert :: Expr -> a +-- | Backend to an SMT solver or theorem prover. data Backend a = Backend { name :: String , cmd :: String @@ -25,5 +40,5 @@ , interpret :: String -> Maybe SatResult } +-- | Satisfiability result communicated by the SMT solver or theorem prover. data SatResult = Sat | Unsat | Unknown - diff --git a/src/Copilot/Theorem/Prover/SMT.hs b/src/Copilot/Theorem/Prover/SMT.hs --- a/src/Copilot/Theorem/Prover/SMT.hs +++ b/src/Copilot/Theorem/Prover/SMT.hs @@ -3,13 +3,23 @@ {-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs #-} {-# LANGUAGE Trustworthy #-} +-- | Connections to various SMT solvers and theorem provers. module Copilot.Theorem.Prover.SMT - ( module Data.Default + ( + + -- * Backends + Backend + , SmtFormat + , SmtLib + , Tptp + , yices, dReal, altErgo, metit, z3, cvc4, mathsat + + -- * Tactics , Options (..) , induction, kInduction, onlySat, onlyValidity - , yices, dReal, altErgo, metit, z3, cvc4, mathsat - , Backend, SmtFormat - , SmtLib, Tptp + + -- * Auxiliary + , module Data.Default ) where import Copilot.Theorem.IL.Translate @@ -42,19 +52,24 @@ -------------------------------------------------------------------------------- --- | Tactics +-- * Tactics +-- | Options to configure the provers. data Options = Options { startK :: Word32 - -- The maximum number of steps of the k-induction algorithm the prover runs - -- before giving up. - , maxK :: Word32 + -- ^ Initial @k@ for the k-induction algorithm. - -- If `debug` is set to `True`, the SMTLib/TPTP queries produced by the - -- prover are displayed in the standard output. - , debug :: Bool + , maxK :: Word32 + -- ^ The maximum number of steps of the k-induction algorithm the prover runs + -- before giving up. + + , debug :: Bool + -- ^ If @debug@ is set to @True@, the SMTLib/TPTP queries produced by the + -- prover are displayed in the standard output. } +-- | Default 'Options' with a @0@ @k@ and a max of @10@ steps, and that produce +-- no debugging info. instance Default Options where def = Options { startK = 0 @@ -62,6 +77,7 @@ , debug = False } +-- | Tactic to find only a proof of satisfiability. onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential onlySat opts backend = check P.Prover { P.proverName = "OnlySat" @@ -70,6 +86,7 @@ , P.closeProver = const $ return () } +-- | Tactic to find only a proof of validity. onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal onlyValidity opts backend = check P.Prover { P.proverName = "OnlyValidity" @@ -78,6 +95,9 @@ , P.closeProver = const $ return () } +-- | Tactic to find a proof by standard 1-induction. +-- +-- The values for @startK@ and @maxK@ in the options are ignored. induction :: SmtFormat a => Options -> Backend a -> Proof Universal induction opts backend = check P.Prover { P.proverName = "Induction" @@ -86,6 +106,7 @@ , P.closeProver = const $ return () } +-- | Tactic to find a proof by k-induction. kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal kInduction opts backend = check P.Prover { P.proverName = "K-Induction" @@ -96,8 +117,13 @@ ------------------------------------------------------------------------------- --- | Backends +-- * Backends +-- | Backend to the Yices 2 SMT solver. +-- +-- It enables non-linear arithmetic (@QF_NRA@), which means MCSat will be used. +-- +-- The command @yices-smt2@ must be in the user's @PATH@. yices :: Backend SmtLib yices = Backend { name = "Yices" @@ -109,6 +135,12 @@ , interpret = SMTLib.interpret } +-- | Backend to the cvc4 SMT solver. +-- +-- It enables support for uninterpreted functions and mixed nonlinear +-- arithmetic (@QF_NIRA@). +-- +-- The command @cvc4@ must be in the user's @PATH@. cvc4 :: Backend SmtLib cvc4 = Backend { name = "CVC4" @@ -120,6 +152,12 @@ , interpret = SMTLib.interpret } +-- | Backend to the Alt-Ergo SMT solver. +-- +-- It enables support for uninterpreted functions and mixed nonlinear +-- arithmetic (@QF_NIRA@). +-- +-- The command @alt-ergo.opt@ must be in the user's @PATH@. altErgo :: Backend SmtLib altErgo = Backend { name = "Alt-Ergo" @@ -131,6 +169,9 @@ , interpret = SMTLib.interpret } +-- | Backend to the Z3 theorem prover. +-- +-- The command @z3@ must be in the user's @PATH@. z3 :: Backend SmtLib z3 = Backend { name = "Z3" @@ -142,6 +183,12 @@ , interpret = SMTLib.interpret } +-- | Backend to the dReal SMT solver. +-- +-- It enables non-linear arithmetic (@QF_NRA@). +-- +-- The libraries for dReal must be installed and @perl@ must be in the user's +-- @PATH@. dReal :: Backend SmtLib dReal = Backend { name = "dReal" @@ -153,6 +200,11 @@ , interpret = SMTLib.interpret } +-- | Backend to the Mathsat SMT solver. +-- +-- It enables non-linear arithmetic (@QF_NRA@). +-- +-- The command @mathsat@ must be in the user's @PATH@. mathsat :: Backend SmtLib mathsat = Backend { name = "MathSAT" @@ -164,7 +216,11 @@ , interpret = SMTLib.interpret } --- The argument is the path to the "tptp" subdirectory of the metitarski +-- | Backend to the MetiTaski theorem prover. +-- +-- The command @metit@ must be in the user's @PATH@. +-- +-- The argument string is the path to the @tptp@ subdirectory of the metitarski -- install location. metit :: String -> Backend Tptp metit installDir = Backend diff --git a/src/Copilot/Theorem/Prover/SMTIO.hs b/src/Copilot/Theorem/Prover/SMTIO.hs --- a/src/Copilot/Theorem/Prover/SMTIO.hs +++ b/src/Copilot/Theorem/Prover/SMTIO.hs @@ -3,9 +3,13 @@ {-# LANGUAGE LambdaCase, NamedFieldPuns, RankNTypes, ViewPatterns #-} {-# LANGUAGE Safe #-} +-- | Communication with SMT solvers or theorem provers. +-- +-- A solver is a running process defined by a 'Backend'. module Copilot.Theorem.Prover.SMTIO ( Solver - , startNewSolver, assume, entailed, stop, declVars + , startNewSolver, stop + , assume, entailed, declVars ) where import Copilot.Theorem.IL @@ -21,6 +25,7 @@ -------------------------------------------------------------------------------- +-- | A connection with a running SMT solver or theorem prover. data Solver a = Solver { solverName :: String , inh :: Handle @@ -34,6 +39,7 @@ -------------------------------------------------------------------------------- +-- | Output a debugging message if debugging is enabled for the solver. debug :: Bool -> Solver a -> String -> IO () debug printName s str = when (debugMode s) $ putStrLn $ (if printName then "<" ++ solverName s ++ "> " else "") ++ str @@ -60,6 +66,10 @@ -------------------------------------------------------------------------------- +-- | Create a new solver implemented by the backend specified. +-- +-- The error handle from the backend handle is immediately closed/discarded, +-- and the logic initialized as specifiied by the backend options. 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 @@ -68,6 +78,8 @@ send s $ setLogic $ logic b return s +-- | Stop a solver, closing all communication handles and terminating the +-- process. stop :: Solver a -> IO () stop s = do hClose $ inh s @@ -76,6 +88,7 @@ -------------------------------------------------------------------------------- +-- | Register the given expressions as assumptions or axioms with the solver. assume :: SmtFormat a => Solver a -> [Expr] -> IO (Solver a) assume s@(Solver { model }) cs = do let newAxioms = elems $ fromList cs \\ model @@ -85,6 +98,8 @@ assume' :: SmtFormat a => Solver a -> [Expr] -> IO () assume' s cs = forM_ cs (send s . assert . bsimpl) +-- | Check if a series of expressions are entailed by the axioms or assumptions +-- already registered with the solver. entailed :: SmtFormat a => Solver a -> [Expr] -> IO SatResult entailed s cs = do when (incremental $ backend s) $ send s push @@ -97,6 +112,7 @@ when (incremental $ backend s) $ send s pop receive s +-- | Register the given variables with the solver. declVars :: SmtFormat a => Solver a -> [VarDescr] -> IO (Solver a) declVars s@(Solver { vars }) decls = do let newVars = elems $ fromList decls \\ vars diff --git a/src/Copilot/Theorem/Prover/SMTLib.hs b/src/Copilot/Theorem/Prover/SMTLib.hs --- a/src/Copilot/Theorem/Prover/SMTLib.hs +++ b/src/Copilot/Theorem/Prover/SMTLib.hs @@ -3,6 +3,8 @@ {-# LANGUAGE GADTs, FlexibleInstances #-} {-# LANGUAGE Safe #-} +-- | A backend to the SMT-Lib format, enabling to produce commands for SMT-Lib +-- implementing solvers, and parse results. module Copilot.Theorem.Prover.SMTLib (SmtLib, interpret) where import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..)) @@ -14,6 +16,9 @@ -------------------------------------------------------------------------------- +-- | Type used to represent SMT-lib commands. +-- +-- Use the interface in 'SmtFormat' to create such commands. newtype SmtLib = SmtLib (SExpr String) instance Show SmtLib where @@ -26,6 +31,7 @@ -------------------------------------------------------------------------------- +-- | Interface for SMT-Lib conforming backends. instance SmtFormat SmtLib where push = SmtLib $ node "push" [atom "1"] pop = SmtLib $ node "pop" [atom "1"] @@ -36,6 +42,7 @@ node "declare-fun" [atom name, (list $ map (atom . smtTy) args), atom (smtTy retTy)] assert c = SmtLib $ node "assert" [expr c] +-- | Parse a satisfiability result. interpret :: String -> Maybe SatResult interpret "sat" = Just Sat interpret "unsat" = Just Unsat diff --git a/src/Copilot/Theorem/Prover/TPTP.hs b/src/Copilot/Theorem/Prover/TPTP.hs --- a/src/Copilot/Theorem/Prover/TPTP.hs +++ b/src/Copilot/Theorem/Prover/TPTP.hs @@ -3,6 +3,8 @@ {-# LANGUAGE GADTs, LambdaCase #-} {-# LANGUAGE Safe #-} +-- | A backend to , enabling to produce assertions +-- and to parse the results from TPTP. module Copilot.Theorem.Prover.TPTP (Tptp, interpret) where import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..)) @@ -12,6 +14,10 @@ -------------------------------------------------------------------------------- +-- | Type used to represent TPTP expressions. +-- +-- Although this type implements the 'SmtFormat' interface, only 'assert' is +-- actually used. data Tptp = Ax TptpExpr | Null data TptpExpr = Bin TptpExpr String TptpExpr | Un String TptpExpr @@ -37,6 +43,7 @@ declFun = const $ const $ const Null assert c = Ax $ expr c +-- | Parse a satisfiability result. interpret :: String -> Maybe SatResult interpret str | "SZS status Unsatisfiable" `isPrefixOf` str = Just Unsat diff --git a/src/Copilot/Theorem/Tactics.hs b/src/Copilot/Theorem/Tactics.hs --- a/src/Copilot/Theorem/Tactics.hs +++ b/src/Copilot/Theorem/Tactics.hs @@ -1,5 +1,7 @@ {-# LANGUAGE Safe #-} +-- | Utility functions to help write proof tactics. + module Copilot.Theorem.Tactics ( instantiate, assume, admit ) where @@ -8,11 +10,14 @@ import Control.Monad.Writer +-- | Instantiate a universal proof into an existential proof. instantiate :: Proof Universal -> Proof Existential instantiate (Proof p) = Proof p +-- | Assume that a property, given by reference, holds. assume :: PropRef Universal -> Proof a assume (PropRef p) = Proof $ tell [Assume p] +-- | Assume that the current goal holds. admit :: Proof a admit = Proof $ tell [Admit] diff --git a/src/Copilot/Theorem/TransSys.hs b/src/Copilot/Theorem/TransSys.hs --- a/src/Copilot/Theorem/TransSys.hs +++ b/src/Copilot/Theorem/TransSys.hs @@ -2,6 +2,15 @@ {-# LANGUAGE Safe #-} +-- | Each prover first translates the Copilot specification into an +-- intermediate representation best suited for model checking. +-- +-- This module and the ones in the same namespace implement the TransSys +-- format. A Copilot program is /flattened/ and translated into a /state/ +-- /transition system/. 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. module Copilot.Theorem.TransSys (module X) where import Copilot.Theorem.TransSys.Spec as X diff --git a/src/Copilot/Theorem/TransSys/Cast.hs b/src/Copilot/Theorem/TransSys/Cast.hs --- a/src/Copilot/Theorem/TransSys/Cast.hs +++ b/src/Copilot/Theorem/TransSys/Cast.hs @@ -3,6 +3,9 @@ {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs #-} {-# LANGUAGE Safe #-} +-- | Casting of values with dynamic types and translating from Copilot core +-- types to Copilot theorem types. + module Copilot.Theorem.TransSys.Cast ( Dyn , toDyn @@ -23,8 +26,11 @@ -------------------------------------------------------------------------------- +-- | Synonym for a dynamic type in Copilot core. type Dyn = Dynamic Type +-- | Translation of a Copilot type into Copilot theorem's internal +-- representation. castedType :: Type t -> K.U K.Type castedType t = case t of Bool -> K.U K.Bool @@ -39,6 +45,7 @@ Float -> K.U K.Real Double -> K.U K.Real +-- | Cast a dynamic value to a given type. cast :: K.Type t -> Dyn -> t cast t v | K.Integer <- t, Just (vi :: Integer) <- _cast v = vi @@ -46,6 +53,8 @@ | K.Real <- t, Just (vr :: Double) <- _cast v = vr | otherwise = error "Bad type cast" +-- | Apply function to a corresponding type in Copilot theorem's internal +-- representation. casting :: Type t -> (forall t' . K.Type t' -> a) -> a casting t f = case castedType t of K.U K.Bool -> f K.Bool diff --git a/src/Copilot/Theorem/TransSys/Invariants.hs b/src/Copilot/Theorem/TransSys/Invariants.hs --- a/src/Copilot/Theorem/TransSys/Invariants.hs +++ b/src/Copilot/Theorem/TransSys/Invariants.hs @@ -1,11 +1,14 @@ {-# OPTIONS_GHC -O0 #-} {-# LANGUAGE Safe #-} +-- | Augment types with invariants. + module Copilot.Theorem.TransSys.Invariants ( HasInvariants (..) , prop ) where +-- | Type class for types with additional invariants or contraints. class HasInvariants a where invariants :: a -> [(String, Bool)] @@ -13,5 +16,6 @@ checkInvs :: a -> Bool checkInvs obj = all snd $ invariants obj +-- | Creates an invariant with a description. prop :: String -> Bool -> (String, Bool) prop = (,) diff --git a/src/Copilot/Theorem/TransSys/Operators.hs b/src/Copilot/Theorem/TransSys/Operators.hs --- a/src/Copilot/Theorem/TransSys/Operators.hs +++ b/src/Copilot/Theorem/TransSys/Operators.hs @@ -4,6 +4,7 @@ RankNTypes #-} {-# LANGUAGE Safe #-} +-- | Operators in modular transition systems and their translation. module Copilot.Theorem.TransSys.Operators where import qualified Copilot.Core as C @@ -14,6 +15,7 @@ -------------------------------------------------------------------------------- +-- | Unary operators. data Op1 a where Not :: Op1 Bool Neg :: Op1 a @@ -34,6 +36,7 @@ Atanh :: Op1 a Acosh :: Op1 a +-- | Binary operators. data Op2 a b where Eq :: Op2 a Bool And :: Op2 Bool Bool @@ -93,37 +96,50 @@ ------------------------------------------------------------------------------- --- | 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. - --------------------------------------------------------------------------------- - +-- | Unhandled unary operator. +-- +-- 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) +-- | Unhandled binary operator. +-- +-- Unhandled operators are monomorphic, and their names are labeled so that +-- each name corresponds to a unique uninterpreted function with a +-- monomorphic type. data UnhandledOp2 = forall a b c . UnhandledOp2 String (Type a) (Type b) (Type c) +-- | Translate an Op1. +-- +-- This function is parameterized so that it can be used to translate +-- in different contexts and with different targets. +-- +-- 'm' is the monad in which the computation is made +-- +-- 'resT' is the desired return type of the expression being translated 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) -> + forall m expr _a _b resT. (Functor m) - m (expr resT) + => Type resT + -- ^ The desired return type + -> (C.Op1 _a _b, C.Expr _a) + -- ^ The unary operator encountered and its argument + + -> (forall t t'. Type t -> C.Expr t' -> m (expr t)) + -- ^ The monadic function to translate an expression + + -> (UnhandledOp1 -> m (expr resT)) + -- ^ A function to deal with a operators not handled + + -> (forall t . Type t -> Op1 t -> expr t -> expr t) + -- ^ The Op1 constructor of the 'expr' type + + -> m (expr resT) + handleOp1 resT (op, e) handleExpr notHandledF mkOp = case op of C.Not -> boolOp Not (handleExpr Bool e) @@ -181,18 +197,38 @@ -------------------------------------------------------------------------------- --- See the 'handleOp1' function for documentation +-- | Translate an Op2. +-- +-- This function is parameterized so that it can be used to translate +-- in different contexts and with different targets. +-- +-- 'm' is the monad in which the computation is made +-- +-- 'resT' is the desired return type of the expression being translated 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) + forall m expr _a _b _c resT . (Monad m) + => Type resT + -- ^ The desired return type + -> (C.Op2 _a _b _c, C.Expr _a, C.Expr _b) + -- ^ The binary operator encountered and its arguments + + -> (forall t t'. Type t -> C.Expr t' -> m (expr t)) + -- ^ The monadic function to translate an expression + + -> (UnhandledOp2 -> m (expr resT)) + -- ^ A function to deal with a operators not handled + + -> (forall t a . Type t -> Op2 a t -> expr a -> expr a -> expr t) + -- ^ The Op2 constructor of the 'expr' type + + -> (expr Bool -> expr Bool) + -- ^ The Op1 for boolean negation + + -> m (expr resT) + + handleOp2 resT (op, e1, e2) handleExpr notHandledF mkOp notOp = case op of C.And -> boolConnector And @@ -294,6 +330,7 @@ -------------------------------------------------------------------------------- +-- | Error message for unexpected behavior / internal errors. typeErrMsg :: String typeErrMsg = "Unexpected type error in 'Misc.CoreOperators'" diff --git a/src/Copilot/Theorem/TransSys/PrettyPrint.hs b/src/Copilot/Theorem/TransSys/PrettyPrint.hs --- a/src/Copilot/Theorem/TransSys/PrettyPrint.hs +++ b/src/Copilot/Theorem/TransSys/PrettyPrint.hs @@ -3,6 +3,7 @@ {-# LANGUAGE NamedFieldPuns, GADTs #-} {-# LANGUAGE Safe #-} +-- | Pretty print a TransSys specification as a Kind2/Lustre specification. module Copilot.Theorem.TransSys.PrettyPrint ( prettyPrint ) where import Copilot.Theorem.TransSys.Spec @@ -19,6 +20,7 @@ indent = nest 4 emptyLine = text "" +-- | Pretty print a TransSys specification as a Kind2/Lustre specification. prettyPrint :: TransSys -> String prettyPrint = render . pSpec diff --git a/src/Copilot/Theorem/TransSys/Renaming.hs b/src/Copilot/Theorem/TransSys/Renaming.hs --- a/src/Copilot/Theorem/TransSys/Renaming.hs +++ b/src/Copilot/Theorem/TransSys/Renaming.hs @@ -2,6 +2,8 @@ {-# LANGUAGE Safe #-} +-- | A monad capable of keeping track of variable renames and of providing +-- fresh names for variables. module Copilot.Theorem.TransSys.Renaming ( Renaming , addReservedName @@ -25,18 +27,28 @@ -------------------------------------------------------------------------------- +-- | A monad capable of keeping track of variable renames and of providing +-- fresh names for variables. type Renaming = State RenamingST +-- | State needed to keep track of variable renames and reserved names. data RenamingST = RenamingST { _reservedNames :: Set Var , _renaming :: Map ExtVar Var } -------------------------------------------------------------------------------- +-- | Register a name as reserved or used. addReservedName :: Var -> Renaming () addReservedName v = modify $ \st -> st {_reservedNames = Set.insert v (_reservedNames st)} +-- | Produce a fresh new name based on the variable names provided. +-- +-- This function will try to pick a name from the given list and, if not, will +-- use one of the names in the list as a basis for new names. +-- +-- PRE: the given list cannot be empty. getFreshName :: [Var] -> Renaming Var getFreshName vs = do usedNames <- _reservedNames <$> get @@ -48,15 +60,24 @@ addReservedName v return v -rename :: NodeId -> Var -> Var -> Renaming () +-- | Map a name in the global namespace to a new variable name. +rename :: NodeId -- ^ A node Id + -> Var -- ^ A variable within that node + -> Var -- ^ A new name for the variable + -> Renaming () rename n v v' = modify $ \st -> st {_renaming = Map.insert (ExtVar n v) v' (_renaming st)} +-- | Return a function that maps variables in the global namespace to their new +-- names if any renaming has been registered. getRenamingF :: Renaming (ExtVar -> Var) getRenamingF = do mapping <- _renaming <$> get return $ \extv -> fromMaybe (extVarLocalPart extv) (Map.lookup extv mapping) +-- | Run a computation in the 'Renaming' monad, providing a result and the +-- renaming function that maps variables in the global namespace to their new +-- local names. runRenaming :: Renaming a -> (a, ExtVar -> Var) runRenaming m = evalState st' (RenamingST Set.empty Map.empty) diff --git a/src/Copilot/Theorem/TransSys/Spec.hs b/src/Copilot/Theorem/TransSys/Spec.hs --- a/src/Copilot/Theorem/TransSys/Spec.hs +++ b/src/Copilot/Theorem/TransSys/Spec.hs @@ -3,6 +3,7 @@ {-# LANGUAGE ExistentialQuantification, GADTs, RankNTypes #-} {-# LANGUAGE Safe #-} +-- | Specification of Copilot streams as modular transition systems. module Copilot.Theorem.TransSys.Spec ( module Copilot.Theorem.TransSys.Operators , module Copilot.Theorem.TransSys.Type @@ -45,35 +46,56 @@ -------------------------------------------------------------------------------- +-- | Unique name that identifies a node. type NodeId = String + +-- | Unique name that identifies a property. type PropId = String +-- | A modular transition system is defined by a graph of nodes and a series +-- of properties, each mapped to a variable. data TransSys = TransSys { specNodes :: [Node] , specTopNodeId :: NodeId , specProps :: Map PropId ExtVar } - +-- | A node is a set of variables living in a local namespace and corresponding +-- to the 'Var' type. data Node = Node { nodeId :: NodeId - , nodeDependencies :: [NodeId] - , nodeLocalVars :: Map Var VarDescr - , nodeImportedVars :: Bimap Var ExtVar + , nodeDependencies :: [NodeId] -- ^ Nodes from which variables are + -- imported. + , nodeLocalVars :: Map Var VarDescr -- ^ Locally defined variables, + -- either as the previous value of + -- another variable (using 'Pre'), + -- an expression involving + -- variables (using 'Expr') or a + -- set of constraints (using + -- 'Constrs'). + , nodeImportedVars :: Bimap Var ExtVar -- ^ Binds each imported variable to + -- its local name. , nodeConstrs :: [Expr Bool] } +-- | Identifer of a variable in the local (within one node) namespace. data Var = Var {varName :: String} deriving (Eq, Show, Ord) +-- | Identifer of a variable in the global namespace by specifying both a node +-- name and a variable. data ExtVar = ExtVar {extVarNode :: NodeId, extVarLocalPart :: Var } deriving (Eq, Ord) +-- | A description of a variable together with its type. data VarDescr = forall t . VarDescr { varType :: Type t , varDef :: VarDef t } +-- | A variable definition either as a delay, an operation on variables, or +-- a constraint. data VarDef t = Pre t Var | Expr (Expr t) | Constrs [Expr Bool] +-- | A point-wise (time-wise) expression. data Expr t where Const :: Type t -> t -> Expr t Ite :: Type t -> Expr Bool -> Expr t -> Expr t -> Expr t @@ -83,6 +105,7 @@ -------------------------------------------------------------------------------- +-- | Constructor for variables identifiers in the global namespace. mkExtVar node name = ExtVar node (Var name) foldExpr :: (Monoid m) => (forall t . Expr t -> m) -> Expr a -> m @@ -97,6 +120,7 @@ foldUExpr :: (Monoid m) => (forall t . Expr t -> m) -> U Expr -> m foldUExpr f (U e) = foldExpr f e +-- | Apply an arbitrary transformation to the leafs of an expression. transformExpr :: (forall a . Expr a -> Expr a) -> Expr t -> Expr t transformExpr f = tre where @@ -108,6 +132,8 @@ -------------------------------------------------------------------------------- +-- | The set of variables related to a node (union of the local variables and +-- the imported variables after deferencing them). nodeVarsSet :: Node -> Set Var nodeVarsSet = liftA2 Set.union nodeLocalVarsSet @@ -157,10 +183,13 @@ specNodesIds :: TransSys -> Set NodeId specNodesIds s = Set.fromList . map nodeId $ specNodes s +-- | Given a modular transition system, produce a map from each node to its +-- dependencies. specDependenciesGraph :: TransSys -> Map NodeId [NodeId] specDependenciesGraph s = Map.fromList [ (nodeId n, nodeDependencies n) | n <- specNodes s ] +-- | Return the top node of a modular transition system. specTopNode :: TransSys -> Node specTopNode spec = fromJust $ List.find ((== specTopNodeId spec) . nodeId) @@ -183,6 +212,9 @@ , prop "The nodes invariants hold" $ all checkInvs (specNodes s) ] +-- | True if the graph is topologically sorted (i.e., if the dependencies of a +-- node appear in the list of 'specNodes' before the node that depends on +-- them). isTopologicallySorted :: TransSys -> Bool isTopologicallySorted spec = isJust $ foldM inspect Set.empty (specNodes spec) diff --git a/src/Copilot/Theorem/TransSys/Transform.hs b/src/Copilot/Theorem/TransSys/Transform.hs --- a/src/Copilot/Theorem/TransSys/Transform.hs +++ b/src/Copilot/Theorem/TransSys/Transform.hs @@ -3,6 +3,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Safe #-} +-- | Helper module to manipulate and simplify TransSys graphs. module Copilot.Theorem.TransSys.Transform ( mergeNodes , inline @@ -39,6 +40,9 @@ -------------------------------------------------------------------------------- +-- | Merge all the given nodes, replacing all references to the given node Ids +-- with a reference to a fresh node id (unless the nodes given as argument +-- contain the top node), in which case its ID is chosen instead. mergeNodes :: [NodeId] -> TransSys -> TransSys mergeNodes toMergeIds spec = spec @@ -70,7 +74,9 @@ , id <- nodeDependencies n , id `notElem` toMergeIds ] - -- All the work of renaming is done in the monad with the same name + -- All the work of renaming is done in the 'Misc.Renaming' monad. Some code + -- complexity has been added so the variable names remains as clear as + -- possible after merging two nodes. (importedVars, renamingF) = runRenaming $ do renameLocalVars toMerge redirectLocalImports toMerge @@ -182,9 +188,27 @@ -------------------------------------------------------------------------------- +-- | Discard all the structure of a /modular transition system/ and turn it +-- into a /non-modular transition system/ with only one node. inline :: TransSys -> TransSys inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec +-- | Remove cycles by merging nodes participating in strongly connected +-- components. +-- +-- The transition system obtained by the 'TransSys.Translate' module is +-- perfectly consistent. However, it can't be directly translated into the +-- /Kind2 native file format/. Indeed, it is natural to bind each node to a +-- predicate but the Kind2 file format requires that each predicate only uses +-- previously defined predicates. However, some nodes in our transition system +-- could be mutually recursive. Therefore, the goal of 'removeCycles' is to +-- remove such dependency cycles. +-- +-- The function 'removeCycles' computes the strongly connected components of +-- the dependency graph and merge each one into a single node using +-- 'mergeNodes'. The complexity of this process is high in the worst case (the +-- square of the total size of the system times the size of the biggest node) +-- but good in practice as few nodes are to be merged in most practical cases. removeCycles :: TransSys -> TransSys removeCycles spec = topoSort $ foldr mergeComp spec (buildScc nodeId $ specNodes spec) @@ -202,11 +226,12 @@ -------------------------------------------------------------------------------- --- | 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 +-- | 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 = diff --git a/src/Copilot/Theorem/TransSys/Translate.hs b/src/Copilot/Theorem/TransSys/Translate.hs --- a/src/Copilot/Theorem/TransSys/Translate.hs +++ b/src/Copilot/Theorem/TransSys/Translate.hs @@ -4,6 +4,41 @@ ScopedTypeVariables, GADTs, FlexibleContexts #-} {-# LANGUAGE Safe #-} +-- | Translate Copilot specifications into a modular transition system. +-- +-- 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@. For example, for the following Fibonacci implementation in +-- Copilot: +-- +-- @ +-- fib = [1, 1] ++ (fib + drop 1 fib) +-- @ +-- +-- the translation, converts it into: +-- +-- @ +-- 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) +-- @ +-- +-- This flattening process is made easier by the fact that the @++@ Copilot +-- operator only occurs leftmost in a stream definition after the reification +-- process. module Copilot.Theorem.TransSys.Translate ( translate ) where import Copilot.Theorem.TransSys.Spec @@ -47,6 +82,7 @@ -------------------------------------------------------------------------------- +-- | Translate Copilot specifications into a modular transition system. translate :: C.Spec -> TransSys translate cspec = diff --git a/src/Copilot/Theorem/TransSys/Type.hs b/src/Copilot/Theorem/TransSys/Type.hs --- a/src/Copilot/Theorem/TransSys/Type.hs +++ b/src/Copilot/Theorem/TransSys/Type.hs @@ -3,6 +3,7 @@ {-# LANGUAGE ExistentialQuantification, GADTs #-} {-# LANGUAGE Safe #-} +-- | Types suported by the modular transition systems. module Copilot.Theorem.TransSys.Type ( Type (..) , U (..) @@ -13,11 +14,15 @@ -------------------------------------------------------------------------------- +-- | A type at both value and type level. +-- +-- Real numbers are mapped to 'Double's. data Type a where Bool :: Type Bool Integer :: Type Integer Real :: Type Double +-- | Proofs of type equality. instance EqualType Type where Bool =~= Bool = Just Refl Integer =~= Integer = Just Refl @@ -26,8 +31,9 @@ -------------------------------------------------------------------------------- +-- | Unknown types. +-- -- 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) diff --git a/src/Copilot/Theorem/What4.hs b/src/Copilot/Theorem/What4.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Theorem/What4.hs @@ -0,0 +1,942 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +-- | +-- Module : Copilot.Theorem.What4 +-- Description : Prove spec properties using What4. +-- Copyright : (c) Ben Selfridge, 2020 +-- Maintainer : benselfridge@galois.com +-- Stability : experimental +-- Portability : POSIX +-- +-- Spec properties are translated into the language of SMT solvers using +-- @What4@. A backend solver is then used to prove the property is true. The +-- technique is sound, but incomplete. If a property is proved true by this +-- technique, then it can be guaranteed to be true. However, if a property is +-- not proved true, that does not mean it isn't true. Very simple specifications +-- are unprovable by this technique, including: +-- +-- @ +-- a = True : a +-- @ +-- +-- The above specification will not be proved true. The reason is that this +-- technique does not perform any sort of induction. When proving the inner @a@ +-- expression, the technique merely allocates a fresh constant standing for +-- "@a@, one timestep in the past." Nothing is asserted about the fresh +-- constant. +-- +-- An example of a property that is provable by this approach is: +-- +-- @ +-- a = True : b +-- b = not a +-- +-- -- Property: a || b +-- @ +-- +-- By allocating a fresh constant, @b_-1@, standing for "the value of @b@ one +-- timestep in the past", the equation for @a || b@ at some arbitrary point in +-- the future reduces to @b_-1 || not b_-1@, which is always true. +-- +-- In addition to proving that the stream expression is true at some arbitrary +-- point in the future, we also prove it for the first @k@ timesteps, where @k@ +-- is the maximum buffer length of all streams in the given spec. This amounts +-- to simply interpreting the spec, although external variables are still +-- represented as constants with unknown values. + +module Copilot.Theorem.What4 + ( prove, Solver(..), SatResult(..) + ) where + +import qualified Copilot.Core.Expr as CE +import qualified Copilot.Core.Operators as CE +import qualified Copilot.Core.Spec as CS +import qualified Copilot.Core.Type as CT +import qualified Copilot.Core.Type.Array as CT + +import qualified What4.Config as WC +import qualified What4.Expr.Builder as WB +import qualified What4.Expr.GroundEval as WG +import qualified What4.Interface as WI +import qualified What4.BaseTypes as WT +import qualified What4.Solver as WS +import qualified What4.Solver.DReal as WS + +import qualified Control.Monad.Fail as Fail +import Control.Monad.State +import qualified Data.BitVector.Sized as BV +import Data.Foldable (foldrM) +import Data.List (elemIndex) +import Data.Maybe (fromJust) +import qualified Data.Map as Map +import Data.Parameterized.Classes +import Data.Parameterized.Context hiding (zipWithM) +import Data.Parameterized.NatRepr +import Data.Parameterized.Nonce +import Data.Parameterized.Some +import Data.Parameterized.SymbolRepr +import qualified Data.Parameterized.Vector as V +import Data.Word +import GHC.Float (castWord32ToFloat, castWord64ToDouble) +import GHC.TypeNats (KnownNat) +import qualified Panic as Panic + +-------------------------------------------------------------------------------- +-- 'prove' function +-- +-- To prove properties of a spec, we translate them into What4 using the TransM +-- monad (transformer on top of IO), then negate each property and ask a backend +-- solver to produce a model for the negation. + +-- | We assume round-near-even throughout, but this variable can be changed if +-- needed. +fpRM :: WI.RoundingMode +fpRM = WI.RNE + +-- | No builder state needed. +data BuilderState a = EmptyState + +-- | The solvers supported by the what4 backend. +data Solver = CVC4 | DReal | Yices | Z3 + +-- | The 'prove' function returns results of this form for each property in a +-- spec. +data SatResult = Valid | Invalid | Unknown + deriving Show + +type CounterExample = [(String, Some CopilotValue)] + +-- | Attempt to prove all of the properties in a spec via an SMT solver (which +-- must be installed locally on the host). Return an association list mapping +-- the names of each property to the result returned by the solver. +prove :: Solver + -- ^ Solver to use + -> CS.Spec + -- ^ Spec + -> IO [(CE.Name, SatResult)] +prove solver spec = do + -- Setup symbolic backend + Some ng <- newIONonceGenerator + sym <- WB.newExprBuilder WB.FloatIEEERepr EmptyState ng + + -- Solver-specific options + case solver of + CVC4 -> WC.extendConfig WS.cvc4Options (WI.getConfiguration sym) + DReal -> WC.extendConfig WS.drealOptions (WI.getConfiguration sym) + Yices -> WC.extendConfig WS.yicesOptions (WI.getConfiguration sym) + Z3 -> WC.extendConfig WS.z3Options (WI.getConfiguration sym) + + -- Build up initial translation state + let streamMap = Map.fromList $ + (\stream -> (CS.streamId stream, stream)) <$> CS.specStreams spec + pow <- WI.freshTotalUninterpFn sym (WI.safeSymbol "pow") knownRepr knownRepr + logb <- WI.freshTotalUninterpFn sym (WI.safeSymbol "logb") knownRepr knownRepr + let st = TransState Map.empty Map.empty Map.empty streamMap pow logb + + -- Define TransM action for proving properties. Doing this in TransM rather + -- than IO allows us to reuse the state for each property. + let proveProperties = forM (CS.specProperties spec) $ \pr -> do + let bufLen (CS.Stream _ buf _ _) = length buf + maxBufLen = maximum (0 : (bufLen <$> CS.specStreams spec)) + prefix <- forM [0 .. maxBufLen - 1] $ \k -> do + XBool p <- translateExprAt sym k (CS.propertyExpr pr) + return p + XBool p <- translateExpr sym 0 (CS.propertyExpr pr) + p_and_prefix <- liftIO $ foldrM (WI.andPred sym) p prefix + not_p_and_prefix <- liftIO $ WI.notPred sym p_and_prefix + + let clauses = [not_p_and_prefix] + case solver of + CVC4 -> liftIO $ WS.runCVC4InOverride sym WS.defaultLogData clauses $ \case + WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid) + WS.Unsat _ -> return (CS.propertyName pr, Valid) + WS.Unknown -> return (CS.propertyName pr, Unknown) + DReal -> liftIO $ WS.runDRealInOverride sym WS.defaultLogData clauses $ \case + WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid) + WS.Unsat _ -> return (CS.propertyName pr, Valid) + WS.Unknown -> return (CS.propertyName pr, Unknown) + Yices -> liftIO $ WS.runYicesInOverride sym WS.defaultLogData clauses $ \case + WS.Sat _ge -> return (CS.propertyName pr, Invalid) + WS.Unsat _ -> return (CS.propertyName pr, Valid) + WS.Unknown -> return (CS.propertyName pr, Unknown) + Z3 -> liftIO $ WS.runZ3InOverride sym WS.defaultLogData clauses $ \case + WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid) + WS.Unsat _ -> return (CS.propertyName pr, Valid) + WS.Unknown -> return (CS.propertyName pr, Unknown) + + -- Execute the action and return the results for each property + (res, _) <- runStateT (unTransM proveProperties) st + return res + +-------------------------------------------------------------------------------- +-- What4 translation + +-- | the state for translating Copilot expressions into What4 expressions. As we +-- translate, we generate fresh symbolic constants for external variables and +-- for stream variables. We need to only generate one constant per variable, so +-- we allocate them in a map. When we need the constant for a particular +-- variable, we check if it is already in the map, and return it if it is; if it +-- isn't, we generate a fresh constant at that point, store it in the map, and +-- return it. +-- +-- We also store three immutable fields in this state, rather than wrap them up +-- in another monad transformer layer. These are initialized prior to +-- translation and are never modified. They are the map from stream ids to the +-- core stream definitions, a symbolic uninterpreted function for "pow", and a +-- symbolic uninterpreted function for "logb". +data TransState t = TransState { + -- | Map of all external variables we encounter during translation. These are + -- just fresh constants. The offset indicates how many timesteps in the past + -- this constant represents for that stream. + externVars :: Map.Map (CE.Name, Int) (XExpr t), + -- | Map of external variables at specific indices (positive), rather than + -- offset into the past. This is for interpreting streams at specific offsets. + externVarsAt :: Map.Map (CE.Name, Int) (XExpr t), + -- | Map from (stream id, negative offset) to fresh constant. These are all + -- constants representing the values of a stream at some point in the past. + -- The offset (ALWAYS NEGATIVE) indicates how many timesteps in the past + -- this constant represents for that stream. + streamConstants :: Map.Map (CE.Id, Int) (XExpr t), + -- | Map from stream ids to the streams themselves. This value is never + -- modified, but I didn't want to make this an RWS, so it's represented as a + -- stateful value. + streams :: Map.Map CE.Id CS.Stream, + -- | Binary power operator, represented as an uninterpreted function. + pow :: WB.ExprSymFn t (WB.Expr t) + (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) + WT.BaseRealType, + -- | Binary logarithm operator, represented as an uninterpreted function. + logb :: WB.ExprSymFn t (WB.Expr t) + (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) + WT.BaseRealType + } + +newtype TransM t a = TransM { unTransM :: StateT (TransState t) IO a } + deriving ( Functor + , Applicative + , Monad + , MonadIO + , MonadState (TransState t) + ) + +instance Fail.MonadFail (TransM t) where + fail = error + +data CopilotWhat4 = CopilotWhat4 + +instance Panic.PanicComponent CopilotWhat4 where + panicComponentName _ = "Copilot/What4 translation" + panicComponentIssues _ = "https://github.com/Copilot-Language/copilot-theorem/issues" + + {-# NOINLINE Panic.panicComponentRevision #-} + panicComponentRevision = $(Panic.useGitRevision) + +-- | Use this function rather than an error monad since it indicates that +-- copilot-core's "reify" function did something incorrectly. +panic :: MonadIO m => m a +panic = Panic.panic CopilotWhat4 "Copilot.Theorem.What4" + [ "Ill-typed core expression" ] + +-- | The What4 representation of a copilot expression. We do not attempt to +-- track the type of the inner expression at the type level, but instead lump +-- everything together into the 'XExpr t' type. The only reason this is a GADT +-- is for the array case; we need to know that the array length is strictly +-- positive. +data XExpr t where + XBool :: WB.Expr t WT.BaseBoolType -> XExpr t + XInt8 :: WB.Expr t (WT.BaseBVType 8) -> XExpr t + XInt16 :: WB.Expr t (WT.BaseBVType 16) -> XExpr t + XInt32 :: WB.Expr t (WT.BaseBVType 32) -> XExpr t + XInt64 :: WB.Expr t (WT.BaseBVType 64) -> XExpr t + XWord8 :: WB.Expr t (WT.BaseBVType 8) -> XExpr t + XWord16 :: WB.Expr t (WT.BaseBVType 16) -> XExpr t + XWord32 :: WB.Expr t (WT.BaseBVType 32) -> XExpr t + XWord64 :: WB.Expr t (WT.BaseBVType 64) -> XExpr t + XFloat :: WB.Expr t (WT.BaseFloatType WT.Prec32) -> XExpr t + XDouble :: WB.Expr t (WT.BaseFloatType WT.Prec64) -> XExpr t + XEmptyArray :: XExpr t + XArray :: 1 <= n => V.Vector n (XExpr t) -> XExpr t + XStruct :: [XExpr t] -> XExpr t + -- XArray :: NatRepr n + -- -> BaseTypeRepr tp + -- -> Some (WB.Expr t) + -- XStruct :: Assignment BaseTypeRepr tps + -- -> WB.Expr t (BaseStructType tps) + -- -> XExpr t + +deriving instance Show (XExpr t) + +data CopilotValue a = CopilotValue { cvType :: CT.Type a + , cvVal :: a + } + +valFromExpr :: WG.GroundEvalFn t -> XExpr t -> IO (Some CopilotValue) +valFromExpr ge xe = case xe of + XBool e -> Some . CopilotValue CT.Bool <$> WG.groundEval ge e + XInt8 e -> Some . CopilotValue CT.Int8 . fromBV <$> WG.groundEval ge e + XInt16 e -> Some . CopilotValue CT.Int16 . fromBV <$> WG.groundEval ge e + XInt32 e -> Some . CopilotValue CT.Int32 . fromBV <$> WG.groundEval ge e + XInt64 e -> Some . CopilotValue CT.Int64 . fromBV <$> WG.groundEval ge e + XWord8 e -> Some . CopilotValue CT.Word8 . fromBV <$> WG.groundEval ge e + XWord16 e -> Some . CopilotValue CT.Word16 . fromBV <$> WG.groundEval ge e + XWord32 e -> Some . CopilotValue CT.Word32 . fromBV <$> WG.groundEval ge e + XWord64 e -> Some . CopilotValue CT.Word64 . fromBV <$> WG.groundEval ge e + XFloat e -> + Some . CopilotValue CT.Float . castWord32ToFloat . fromBV <$> WG.groundEval ge e + XDouble e -> + Some . CopilotValue CT.Double . castWord64ToDouble . fromBV <$> WG.groundEval ge e + _ -> error "valFromExpr unhandled case" + where fromBV :: forall a w . Num a => BV.BV w -> a + fromBV = fromInteger . BV.asUnsigned + +-- | A view of an XExpr as a bitvector expression, a natrepr for its width, its +-- signed/unsigned status, and the constructor used to reconstruct an XExpr from +-- it. This is a useful view for translation, as many of the operations can be +-- grouped together for all words\/ints\/floats. +data SomeBVExpr t where + SomeBVExpr :: 1 <= w + => WB.BVExpr t w + -> NatRepr w + -> BVSign + -> (WB.BVExpr t w -> XExpr t) + -> SomeBVExpr t + +-- | The sign of a bitvector -- this indicates whether it is to be interpreted +-- as a signed 'Int' or an unsigned 'Word'. +data BVSign = Signed | Unsigned + +-- | If the inner expression can be viewed as a bitvector, we project out a view +-- of it as such. +asBVExpr :: XExpr t -> Maybe (SomeBVExpr t) +asBVExpr xe = case xe of + XInt8 e -> Just (SomeBVExpr e knownNat Signed XInt8) + XInt16 e -> Just (SomeBVExpr e knownNat Signed XInt16) + XInt32 e -> Just (SomeBVExpr e knownNat Signed XInt32) + XInt64 e -> Just (SomeBVExpr e knownNat Signed XInt64) + XWord8 e -> Just (SomeBVExpr e knownNat Unsigned XWord8) + XWord16 e -> Just (SomeBVExpr e knownNat Unsigned XWord16) + XWord32 e -> Just (SomeBVExpr e knownNat Unsigned XWord32) + XWord64 e -> Just (SomeBVExpr e knownNat Unsigned XWord64) + _ -> Nothing + +-- | Translate a constant expression by creating a what4 literal and packaging +-- it up into an 'XExpr'. +translateConstExpr :: forall a t st fs . + WB.ExprBuilder t st fs + -> CT.Type a + -> a + -> IO (XExpr t) +translateConstExpr sym tp a = case tp of + CT.Bool -> case a of + True -> return $ XBool (WI.truePred sym) + False -> return $ XBool (WI.falsePred sym) + CT.Int8 -> XInt8 <$> WI.bvLit sym knownNat (BV.int8 a) + CT.Int16 -> XInt16 <$> WI.bvLit sym knownNat (BV.int16 a) + CT.Int32 -> XInt32 <$> WI.bvLit sym knownNat (BV.int32 a) + CT.Int64 -> XInt64 <$> WI.bvLit sym knownNat (BV.int64 a) + CT.Word8 -> XWord8 <$> WI.bvLit sym knownNat (BV.word8 a) + CT.Word16 -> XWord16 <$> WI.bvLit sym knownNat (BV.word16 a) + CT.Word32 -> XWord32 <$> WI.bvLit sym knownNat (BV.word32 a) + CT.Word64 -> XWord64 <$> WI.bvLit sym knownNat (BV.word64 a) + CT.Float -> XFloat <$> WI.floatLit sym knownRepr (toRational a) + CT.Double -> XDouble <$> WI.floatLit sym knownRepr (toRational a) + CT.Array tp -> do + elts <- traverse (translateConstExpr sym tp) (CT.arrayelems a) + Just (Some n) <- return $ someNat (length elts) + case isZeroOrGT1 n of + Left Refl -> return XEmptyArray + Right LeqProof -> do + let Just v = V.fromList n elts + return $ XArray v + CT.Struct _ -> do + elts <- forM (CT.toValues a) $ \(CT.Value tp (CT.Field a)) -> + translateConstExpr sym tp a + return $ XStruct elts + +arrayLen :: KnownNat n => CT.Type (CT.Array n t) -> NatRepr n +arrayLen _ = knownNat + +-- | Generate a fresh constant for a given copilot type. This will be called +-- whenever we attempt to get the constant for a given external variable or +-- stream variable, but that variable has not been accessed yet and therefore +-- has no constant allocated. +freshCPConstant :: forall t st fs a . + WB.ExprBuilder t st fs + -> String + -> CT.Type a + -> IO (XExpr t) +freshCPConstant sym nm tp = case tp of + CT.Bool -> XBool <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Int8 -> XInt8 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Int16 -> XInt16 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Int32 -> XInt32 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Int64 -> XInt64 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Word8 -> XWord8 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Word16 -> XWord16 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Word32 -> XWord32 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Word64 -> XWord64 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Float -> XFloat <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + CT.Double -> XDouble <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr + atp@(CT.Array itp) -> do + n <- return $ arrayLen atp + case isZeroOrGT1 n of + Left Refl -> return XEmptyArray + Right LeqProof -> do + Refl <- return $ minusPlusCancel n (knownNat @1) + elts :: V.Vector n (XExpr t) <- V.generateM (decNat n) (const (freshCPConstant sym "" itp)) + return $ XArray elts + CT.Struct stp -> do + elts <- forM (CT.toValues stp) $ \(CT.Value ftp _) -> freshCPConstant sym "" ftp + return $ XStruct elts + +-- | Get the constant for a given stream id and some offset into the past. This +-- should only be called with a strictly negative offset. When this function +-- gets called for the first time for a given (streamId, offset) pair, it +-- generates a fresh constant and stores it in an internal map. Thereafter, this +-- function will just return that constant when called with the same pair. +getStreamConstant :: WB.ExprBuilder t st fs -> CE.Id -> Int -> TransM t (XExpr t) +getStreamConstant sym streamId offset = do + scs <- gets streamConstants + case Map.lookup (streamId, offset) scs of + Just xe -> return xe + Nothing -> do + CS.Stream _ _ _ tp <- getStreamDef streamId + let nm = show streamId ++ "_" ++ show offset + xe <- liftIO $ freshCPConstant sym nm tp + modify (\st -> st { streamConstants = Map.insert (streamId, offset) xe scs }) + return xe + +-- | Get the constant for a given external variable and some offset into the +-- past. This should only be called with a strictly negative offset. When this +-- function gets called for the first time for a given (var, offset) pair, it +-- generates a fresh constant and stores it in an internal map. Thereafter, this +-- function will just return that constant when called with the same pair. +getExternConstant :: WB.ExprBuilder t st fs + -> CT.Type a + -> CE.Name + -> Int + -> TransM t (XExpr t) +getExternConstant sym tp var offset = do + es <- gets externVars + case Map.lookup (var, offset) es of + Just xe -> return xe + Nothing -> do + xe <- liftIO $ freshCPConstant sym var tp + modify (\st -> st { externVars = Map.insert (var, offset) xe es} ) + return xe + +-- | Get the constant for a given external variable at some specific timestep. +getExternConstantAt :: WB.ExprBuilder t st fs + -> CT.Type a + -> CE.Name + -> Int + -> TransM t (XExpr t) +getExternConstantAt sym tp var ix = do + es <- gets externVarsAt + case Map.lookup (var, ix) es of + Just xe -> return xe + Nothing -> do + xe <- liftIO $ freshCPConstant sym var tp + modify (\st -> st { externVarsAt = Map.insert (var, ix) xe es} ) + return xe + +-- | Retrieve a stream definition given its id. +getStreamDef :: CE.Id -> TransM t CS.Stream +getStreamDef streamId = fromJust <$> gets (Map.lookup streamId . streams) + +-- | Translate an expression into a what4 representation. The int offset keeps +-- track of how many timesteps into the past each variable is referring to. +-- Initially the value should be zero, but when we translate a stream, the +-- offset is recomputed based on the length of that stream's prefix (subtracted) +-- and the drop index (added). +translateExpr :: WB.ExprBuilder t st fs + -> Int + -- ^ number of timesteps in the past we are currently looking + -- (must always be <= 0) + -> CE.Expr a + -> TransM t (XExpr t) +translateExpr sym offset e = case e of + CE.Const tp a -> liftIO $ translateConstExpr sym tp a + CE.Drop _tp ix streamId + -- If we are referencing a past value of this stream, just return an + -- unconstrained constant. + | offset + fromIntegral ix < 0 -> + getStreamConstant sym streamId (offset + fromIntegral ix) + -- If we are referencing a current or future value of this stream, we need + -- to translate the stream's expression, using an offset computed based on + -- the current offset (negative or 0), the drop index (positive or 0), and + -- the length of the stream's buffer (subtracted). + | otherwise -> do + CS.Stream _ buf e _ <- getStreamDef streamId + translateExpr sym (offset + fromIntegral ix - length buf) e + CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented" + CE.Var _ _ -> error "translateExpr: Var unimplemented" + CE.ExternVar tp nm _prefix -> getExternConstant sym tp nm offset + CE.Op1 op e -> liftIO . translateOp1 sym op =<< translateExpr sym offset e + CE.Op2 op e1 e2 -> do + xe1 <- translateExpr sym offset e1 + xe2 <- translateExpr sym offset e2 + powFn <- gets pow + logbFn <- gets logb + liftIO $ translateOp2 sym powFn logbFn op xe1 xe2 + CE.Op3 op e1 e2 e3 -> do + xe1 <- translateExpr sym offset e1 + xe2 <- translateExpr sym offset e2 + xe3 <- translateExpr sym offset e3 + liftIO $ translateOp3 sym op xe1 xe2 xe3 + CE.Label _ _ _ -> error "translateExpr: Label unimplemented" + +-- | Translate an expression into a what4 representation at a /specific/ +-- timestep, rather than "at some indeterminate point in the future." +translateExprAt :: WB.ExprBuilder t st fs + -> Int + -- ^ Index of timestep + -> CE.Expr a + -- ^ stream expression + -> TransM t (XExpr t) +translateExprAt sym k e = do + case e of + CE.Const tp a -> liftIO $ translateConstExpr sym tp a + CE.Drop _tp ix streamId -> do + CS.Stream _ buf e tp <- getStreamDef streamId + if k' < length buf + then liftIO $ translateConstExpr sym tp (buf !! k') + else translateExprAt sym (k' - length buf) e + where k' = k + fromIntegral ix + CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented" + CE.Var _ _ -> error "translateExpr: Var unimplemented" + CE.ExternVar tp nm _prefix -> getExternConstantAt sym tp nm k + CE.Op1 op e -> liftIO . translateOp1 sym op =<< translateExprAt sym k e + CE.Op2 op e1 e2 -> do + xe1 <- translateExprAt sym k e1 + xe2 <- translateExprAt sym k e2 + powFn <- gets pow + logbFn <- gets logb + liftIO $ translateOp2 sym powFn logbFn op xe1 xe2 + CE.Op3 op e1 e2 e3 -> do + xe1 <- translateExprAt sym k e1 + xe2 <- translateExprAt sym k e2 + xe3 <- translateExprAt sym k e3 + liftIO $ translateOp3 sym op xe1 xe2 xe3 + CE.Label _ _ _ -> error "translateExpr: Label unimplemented" + +type BVOp1 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> IO (WB.BVExpr t w) + +type FPOp1 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp)) + +type RealOp1 t = WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType) + +fieldName :: KnownSymbol s => CT.Field s a -> SymbolRepr s +fieldName _ = knownSymbol + +valueName :: CT.Value a -> Some SymbolRepr +valueName (CT.Value _ f) = Some (fieldName f) + +translateOp1 :: forall t st fs a b . + WB.ExprBuilder t st fs + -> CE.Op1 a b + -> XExpr t + -> IO (XExpr t) +translateOp1 sym op xe = case (op, xe) of + (CE.Not, XBool e) -> XBool <$> WI.notPred sym e + (CE.Not, _) -> panic + (CE.Abs _, xe) -> numOp bvAbs fpAbs xe + where bvAbs :: BVOp1 w t + bvAbs e = do zero <- WI.bvLit sym knownNat (BV.zero knownNat) + e_neg <- WI.bvSlt sym e zero + neg_e <- WI.bvSub sym zero e + WI.bvIte sym e_neg neg_e e + fpAbs :: FPOp1 fpp t + fpAbs e = do zero <- WI.floatLit sym knownRepr 0 + e_neg <- WI.floatLt sym e zero + neg_e <- WI.floatSub sym fpRM zero e + WI.floatIte sym e_neg neg_e e + (CE.Sign _, xe) -> numOp bvSign fpSign xe + where bvSign :: BVOp1 w t + bvSign e = do zero <- WI.bvLit sym knownRepr (BV.zero knownNat) + neg_one <- WI.bvLit sym knownNat (BV.mkBV knownNat (-1)) + pos_one <- WI.bvLit sym knownNat (BV.mkBV knownNat 1) + e_zero <- WI.bvEq sym e zero + e_neg <- WI.bvSlt sym e zero + t <- WI.bvIte sym e_neg neg_one pos_one + WI.bvIte sym e_zero zero t + fpSign :: FPOp1 fpp t + fpSign e = do zero <- WI.floatLit sym knownRepr 0 + neg_one <- WI.floatLit sym knownRepr (-1) + pos_one <- WI.floatLit sym knownRepr 1 + e_zero <- WI.floatEq sym e zero + e_neg <- WI.floatLt sym e zero + t <- WI.floatIte sym e_neg neg_one pos_one + WI.floatIte sym e_zero zero t + (CE.Recip _, xe) -> fpOp recip xe + where recip :: FPOp1 fpp t + recip e = do one <- WI.floatLit sym knownRepr 1 + WI.floatDiv sym fpRM one e + (CE.Exp _, xe) -> realOp (WI.realExp sym) xe + (CE.Sqrt _, xe) -> fpOp (WI.floatSqrt sym fpRM) xe + (CE.Log _, xe) -> realOp (WI.realLog sym) xe + (CE.Sin _, xe) -> realOp (WI.realSin sym) xe + (CE.Cos _, xe) -> realOp (WI.realCos sym) xe + (CE.Tan _, xe) -> realOp (WI.realTan sym) xe + (CE.Asin _, xe) -> realOp (realRecip <=< WI.realSin sym) xe + (CE.Acos _, xe) -> realOp (realRecip <=< WI.realCos sym) xe + (CE.Atan _, xe) -> realOp (realRecip <=< WI.realTan sym) xe + (CE.Sinh _, xe) -> realOp (WI.realSinh sym) xe + (CE.Cosh _, xe) -> realOp (WI.realCosh sym) xe + (CE.Tanh _, xe) -> realOp (WI.realTanh sym) xe + (CE.Asinh _, xe) -> realOp (realRecip <=< WI.realSinh sym) xe + (CE.Acosh _, xe) -> realOp (realRecip <=< WI.realCosh sym) xe + (CE.Atanh _, xe) -> realOp (realRecip <=< WI.realTanh sym) xe + (CE.BwNot _, xe) -> case xe of + XBool e -> XBool <$> WI.notPred sym e + _ -> bvOp (WI.bvNotBits sym) xe + (CE.Cast _ tp, xe) -> case (xe, tp) of + (XBool e, CT.Bool) -> return $ XBool e + (XBool e, CT.Word8) -> XWord8 <$> WI.predToBV sym e knownNat + (XBool e, CT.Word16) -> XWord16 <$> WI.predToBV sym e knownNat + (XBool e, CT.Word32) -> XWord32 <$> WI.predToBV sym e knownNat + (XBool e, CT.Word64) -> XWord64 <$> WI.predToBV sym e knownNat + (XBool e, CT.Int8) -> XInt8 <$> WI.predToBV sym e knownNat + (XBool e, CT.Int16) -> XInt16 <$> WI.predToBV sym e knownNat + (XBool e, CT.Int32) -> XInt32 <$> WI.predToBV sym e knownNat + (XBool e, CT.Int64) -> XInt64 <$> WI.predToBV sym e knownNat + (XInt8 e, CT.Int8) -> return $ XInt8 e + (XInt8 e, CT.Int16) -> XInt16 <$> WI.bvSext sym knownNat e + (XInt8 e, CT.Int32) -> XInt32 <$> WI.bvSext sym knownNat e + (XInt8 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e + (XInt16 e, CT.Int16) -> return $ XInt16 e + (XInt16 e, CT.Int32) -> XInt32 <$> WI.bvSext sym knownNat e + (XInt16 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e + (XInt32 e, CT.Int32) -> return $ XInt32 e + (XInt32 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e + (XInt64 e, CT.Int64) -> return $ XInt64 e + (XWord8 e, CT.Int16) -> XInt16 <$> WI.bvZext sym knownNat e + (XWord8 e, CT.Int32) -> XInt32 <$> WI.bvZext sym knownNat e + (XWord8 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e + (XWord8 e, CT.Word8) -> return $ XWord8 e + (XWord8 e, CT.Word16) -> XWord16 <$> WI.bvZext sym knownNat e + (XWord8 e, CT.Word32) -> XWord32 <$> WI.bvZext sym knownNat e + (XWord8 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e + (XWord16 e, CT.Int32) -> XInt32 <$> WI.bvZext sym knownNat e + (XWord16 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e + (XWord16 e, CT.Word16) -> return $ XWord16 e + (XWord16 e, CT.Word32) -> XWord32 <$> WI.bvZext sym knownNat e + (XWord16 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e + (XWord32 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e + (XWord32 e, CT.Word32) -> return $ XWord32 e + (XWord32 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e + (XWord64 e, CT.Word64) -> return $ XWord64 e + _ -> panic + (CE.GetField (CT.Struct s) _ftp extractor, XStruct xes) -> do + let fieldNameRepr = fieldName (extractor undefined) + let structFieldNameReprs = valueName <$> CT.toValues s + let mIx = elemIndex (Some fieldNameRepr) structFieldNameReprs + case mIx of + Just ix -> return $ xes !! ix + Nothing -> panic + _ -> panic + where numOp :: (forall w . BVOp1 w t) + -> (forall fpp . FPOp1 fpp t) + -> XExpr t + -> IO (XExpr t) + numOp bvOp fpOp xe = case xe of + XInt8 e -> XInt8 <$> bvOp e + XInt16 e -> XInt16 <$> bvOp e + XInt32 e -> XInt32 <$> bvOp e + XInt64 e -> XInt64 <$> bvOp e + XWord8 e -> XWord8 <$> bvOp e + XWord16 e -> XWord16 <$> bvOp e + XWord32 e -> XWord32 <$> bvOp e + XWord64 e -> XWord64 <$> bvOp e + XFloat e -> XFloat <$> fpOp e + XDouble e -> XDouble <$> fpOp e + _ -> panic + + bvOp :: (forall w . BVOp1 w t) -> XExpr t -> IO (XExpr t) + bvOp f xe = case xe of + XInt8 e -> XInt8 <$> f e + XInt16 e -> XInt16 <$> f e + XInt32 e -> XInt32 <$> f e + XInt64 e -> XInt64 <$> f e + XWord8 e -> XWord8 <$> f e + XWord16 e -> XWord16 <$> f e + XWord32 e -> XWord32 <$> f e + XWord64 e -> XWord64 <$> f e + _ -> panic + + fpOp :: (forall fpp . FPOp1 fpp t) -> XExpr t -> IO (XExpr t) + fpOp g xe = case xe of + XFloat e -> XFloat <$> g e + XDouble e -> XDouble <$> g e + _ -> panic + + realOp :: RealOp1 t -> XExpr t -> IO (XExpr t) + realOp h xe = fpOp hf xe + where hf :: (forall fpp . FPOp1 fpp t) + hf e = do re <- WI.floatToReal sym e + hre <- h re + WI.realToFloat sym knownRepr fpRM hre + + realRecip :: RealOp1 t + realRecip e = do one <- WI.realLit sym 1 + WI.realDiv sym one e + +type BVOp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BVExpr t w) + +type FPOp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp)) + +type RealOp2 t = WB.Expr t WT.BaseRealType -> WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType) + +type BoolCmp2 t = WB.BoolExpr t -> WB.BoolExpr t -> IO (WB.BoolExpr t) + +type BVCmp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BoolExpr t) + +type FPCmp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.BoolExpr t) + +translateOp2 :: forall t st fs a b c . + WB.ExprBuilder t st fs + -> (WB.ExprSymFn t (WB.Expr t) + (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) + WT.BaseRealType) + -- ^ Pow function + -> (WB.ExprSymFn t (WB.Expr t) + (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType) + WT.BaseRealType) + -- ^ Logb function + -> CE.Op2 a b c + -> XExpr t + -> XExpr t + -> IO (XExpr t) +translateOp2 sym powFn logbFn op xe1 xe2 = case (op, xe1, xe2) of + (CE.And, XBool e1, XBool e2) -> XBool <$> WI.andPred sym e1 e2 + (CE.Or, XBool e1, XBool e2) -> XBool <$> WI.orPred sym e1 e2 + (CE.Add _, xe1, xe2) -> numOp (WI.bvAdd sym) (WI.floatAdd sym fpRM) xe1 xe2 + (CE.Sub _, xe1, xe2) -> numOp (WI.bvSub sym) (WI.floatSub sym fpRM) xe1 xe2 + (CE.Mul _, xe1, xe2) -> numOp (WI.bvMul sym) (WI.floatMul sym fpRM) xe1 xe2 + (CE.Mod _, xe1, xe2) -> bvOp (WI.bvSrem sym) (WI.bvUrem sym) xe1 xe2 + (CE.Div _, xe1, xe2) -> bvOp (WI.bvSdiv sym) (WI.bvUdiv sym) xe1 xe2 + (CE.Fdiv _, xe1, xe2) -> fpOp (WI.floatDiv sym fpRM) xe1 xe2 + (CE.Pow _, xe1, xe2) -> fpOp powFn' xe1 xe2 + where powFn' :: FPOp2 fpp t + powFn' e1 e2 = do re1 <- WI.floatToReal sym e1 + re2 <- WI.floatToReal sym e2 + let args = (Empty :> re1 :> re2) + rpow <- WI.applySymFn sym powFn args + WI.realToFloat sym knownRepr fpRM rpow + (CE.Logb _, xe1, xe2) -> fpOp logbFn' xe1 xe2 + where logbFn' :: FPOp2 fpp t + logbFn' e1 e2 = do re1 <- WI.floatToReal sym e1 + re2 <- WI.floatToReal sym e2 + let args = (Empty :> re1 :> re2) + rpow <- WI.applySymFn sym logbFn args + WI.realToFloat sym knownRepr fpRM rpow + (CE.Eq _, xe1, xe2) -> cmp (WI.eqPred sym) (WI.bvEq sym) (WI.floatEq sym) xe1 xe2 + (CE.Ne _, xe1, xe2) -> cmp neqPred bvNeq fpNeq xe1 xe2 + where neqPred :: BoolCmp2 t + neqPred e1 e2 = do e <- WI.eqPred sym e1 e2 + WI.notPred sym e + bvNeq :: forall w . BVCmp2 w t + bvNeq e1 e2 = do e <- WI.bvEq sym e1 e2 + WI.notPred sym e + fpNeq :: forall fpp . FPCmp2 fpp t + fpNeq e1 e2 = do e <- WI.floatEq sym e1 e2 + WI.notPred sym e + (CE.Le _, xe1, xe2) -> numCmp (WI.bvSle sym) (WI.bvUle sym) (WI.floatLe sym) xe1 xe2 + (CE.Ge _, xe1, xe2) -> numCmp (WI.bvSge sym) (WI.bvUge sym) (WI.floatGe sym) xe1 xe2 + (CE.Lt _, xe1, xe2) -> numCmp (WI.bvSlt sym) (WI.bvUlt sym) (WI.floatLt sym) xe1 xe2 + (CE.Gt _, xe1, xe2) -> numCmp (WI.bvSgt sym) (WI.bvUgt sym) (WI.floatGt sym) xe1 xe2 + (CE.BwAnd _, xe1, xe2) -> bvOp (WI.bvAndBits sym) (WI.bvAndBits sym) xe1 xe2 + (CE.BwOr _, xe1, xe2) -> bvOp (WI.bvOrBits sym) (WI.bvOrBits sym) xe1 xe2 + (CE.BwXor _, xe1, xe2) -> bvOp (WI.bvXorBits sym) (WI.bvXorBits sym) xe1 xe2 + -- Note: For both shift operators, we are interpreting the shifter as an + -- unsigned bitvector regardless of whether it is a word or an int. + (CE.BwShiftL _ _, xe1, xe2) -> do + Just (SomeBVExpr e1 w1 _ ctor1) <- return $ asBVExpr xe1 + Just (SomeBVExpr e2 w2 _ _ ) <- return $ asBVExpr xe2 + e2' <- case testNatCases w1 w2 of + NatCaseLT LeqProof -> WI.bvTrunc sym w1 e2 + NatCaseEQ -> return e2 + NatCaseGT LeqProof -> WI.bvZext sym w1 e2 + ctor1 <$> WI.bvShl sym e1 e2' + (CE.BwShiftR _ _, xe1, xe2) -> do + Just (SomeBVExpr e1 w1 sgn1 ctor1) <- return $ asBVExpr xe1 + Just (SomeBVExpr e2 w2 _ _ ) <- return $ asBVExpr xe2 + e2' <- case testNatCases w1 w2 of + NatCaseLT LeqProof -> WI.bvTrunc sym w1 e2 + NatCaseEQ -> return e2 + NatCaseGT LeqProof -> WI.bvZext sym w1 e2 + ctor1 <$> case sgn1 of + Signed -> WI.bvAshr sym e1 e2' + Unsigned -> WI.bvLshr sym e1 e2' + -- Note: Currently, copilot does not check if array indices are out of bounds, + -- even for constant expressions. The method of translation we are using + -- simply creates a nest of if-then-else expression to check the index + -- expression against all possible indices. If the index expression is known + -- by the solver to be out of bounds (for instance, if it is a constant 5 for + -- an array of 5 elements), then the if-then-else will trivially resolve to + -- true. + (CE.Index _, xe1, xe2) -> do + case (xe1, xe2) of + (XArray xes, XWord32 ix) -> buildIndexExpr sym 0 ix xes + _ -> panic + _ -> panic + where numOp :: (forall w . BVOp2 w t) + -> (forall fpp . FPOp2 fpp t) + -> XExpr t + -> XExpr t + -> IO (XExpr t) + numOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of + (XInt8 e1, XInt8 e2) -> XInt8 <$> bvOp e1 e2 + (XInt16 e1, XInt16 e2) -> XInt16 <$> bvOp e1 e2 + (XInt32 e1, XInt32 e2)-> XInt32 <$> bvOp e1 e2 + (XInt64 e1, XInt64 e2)-> XInt64 <$> bvOp e1 e2 + (XWord8 e1, XWord8 e2)-> XWord8 <$> bvOp e1 e2 + (XWord16 e1, XWord16 e2)-> XWord16 <$> bvOp e1 e2 + (XWord32 e1, XWord32 e2)-> XWord32 <$> bvOp e1 e2 + (XWord64 e1, XWord64 e2)-> XWord64 <$> bvOp e1 e2 + (XFloat e1, XFloat e2)-> XFloat <$> fpOp e1 e2 + (XDouble e1, XDouble e2)-> XDouble <$> fpOp e1 e2 + _ -> panic + + bvOp :: (forall w . BVOp2 w t) + -> (forall w . BVOp2 w t) + -> XExpr t + -> XExpr t + -> IO (XExpr t) + bvOp opS opU xe1 xe2 = case (xe1, xe2) of + (XInt8 e1, XInt8 e2) -> XInt8 <$> opS e1 e2 + (XInt16 e1, XInt16 e2) -> XInt16 <$> opS e1 e2 + (XInt32 e1, XInt32 e2) -> XInt32 <$> opS e1 e2 + (XInt64 e1, XInt64 e2) -> XInt64 <$> opS e1 e2 + (XWord8 e1, XWord8 e2) -> XWord8 <$> opU e1 e2 + (XWord16 e1, XWord16 e2) -> XWord16 <$> opU e1 e2 + (XWord32 e1, XWord32 e2) -> XWord32 <$> opU e1 e2 + (XWord64 e1, XWord64 e2) -> XWord64 <$> opU e1 e2 + _ -> panic + + fpOp :: (forall fpp . FPOp2 fpp t) + -> XExpr t + -> XExpr t + -> IO (XExpr t) + fpOp op xe1 xe2 = case (xe1, xe2) of + (XFloat e1, XFloat e2) -> XFloat <$> op e1 e2 + (XDouble e1, XDouble e2) -> XDouble <$> op e1 e2 + _ -> panic + + cmp :: BoolCmp2 t + -> (forall w . BVCmp2 w t) + -> (forall fpp . FPCmp2 fpp t) + -> XExpr t + -> XExpr t + -> IO (XExpr t) + cmp boolOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of + (XBool e1, XBool e2) -> XBool <$> boolOp e1 e2 + (XInt8 e1, XInt8 e2) -> XBool <$> bvOp e1 e2 + (XInt16 e1, XInt16 e2) -> XBool <$> bvOp e1 e2 + (XInt32 e1, XInt32 e2)-> XBool <$> bvOp e1 e2 + (XInt64 e1, XInt64 e2)-> XBool <$> bvOp e1 e2 + (XWord8 e1, XWord8 e2)-> XBool <$> bvOp e1 e2 + (XWord16 e1, XWord16 e2)-> XBool <$> bvOp e1 e2 + (XWord32 e1, XWord32 e2)-> XBool <$> bvOp e1 e2 + (XWord64 e1, XWord64 e2)-> XBool <$> bvOp e1 e2 + (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2 + (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2 + _ -> panic + + numCmp :: (forall w . BVCmp2 w t) + -> (forall w . BVCmp2 w t) + -> (forall fpp . FPCmp2 fpp t) + -> XExpr t + -> XExpr t + -> IO (XExpr t) + numCmp bvSOp bvUOp fpOp xe1 xe2 = case (xe1, xe2) of + (XInt8 e1, XInt8 e2) -> XBool <$> bvSOp e1 e2 + (XInt16 e1, XInt16 e2) -> XBool <$> bvSOp e1 e2 + (XInt32 e1, XInt32 e2)-> XBool <$> bvSOp e1 e2 + (XInt64 e1, XInt64 e2)-> XBool <$> bvSOp e1 e2 + (XWord8 e1, XWord8 e2)-> XBool <$> bvUOp e1 e2 + (XWord16 e1, XWord16 e2)-> XBool <$> bvUOp e1 e2 + (XWord32 e1, XWord32 e2)-> XBool <$> bvUOp e1 e2 + (XWord64 e1, XWord64 e2)-> XBool <$> bvUOp e1 e2 + (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2 + (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2 + _ -> panic + + buildIndexExpr :: 1 <= n + => WB.ExprBuilder t st fs + -> Word32 + -- ^ Index + -> WB.Expr t (WT.BaseBVType 32) + -- ^ Index + -> V.Vector n (XExpr t) + -- ^ Elements + -> IO (XExpr t) + buildIndexExpr sym curIx ix xelts = case V.uncons xelts of + (xe, Left Refl) -> return xe + (xe, Right xelts') -> do + LeqProof <- return $ V.nonEmpty xelts' + rstExpr <- buildIndexExpr sym (curIx+1) ix xelts' + curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx) + ixEq <- WI.bvEq sym curIxExpr ix + mkIte sym ixEq xe rstExpr + + mkIte :: WB.ExprBuilder t st fs + -> WB.Expr t WT.BaseBoolType + -> XExpr t + -> XExpr t + -> IO (XExpr t) + mkIte sym pred xe1 xe2 = case (xe1, xe2) of + (XBool e1, XBool e2) -> XBool <$> WI.itePred sym pred e1 e2 + (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym pred e1 e2 + (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym pred e1 e2 + (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym pred e1 e2 + (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym pred e1 e2 + (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym pred e1 e2 + (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym pred e1 e2 + (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym pred e1 e2 + (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym pred e1 e2 + (XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym pred e1 e2 + (XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym pred e1 e2 + (XStruct xes1, XStruct xes2) -> + XStruct <$> zipWithM (mkIte sym pred) xes1 xes2 + (XArray xes1, XArray xes2) -> + case V.length xes1 `testEquality` V.length xes2 of + Just Refl -> XArray <$> V.zipWithM (mkIte sym pred) xes1 xes2 + Nothing -> panic + _ -> panic + + +translateOp3 :: forall t st fs a b c d . + WB.ExprBuilder t st fs + -> CE.Op3 a b c d + -> XExpr t + -> XExpr t + -> XExpr t + -> IO (XExpr t) +translateOp3 sym (CE.Mux _) (XBool te) xe1 xe2 = case (xe1, xe2) of + (XBool e1, XBool e2) -> XBool <$> WI.itePred sym te e1 e2 + (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym te e1 e2 + (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym te e1 e2 + (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym te e1 e2 + (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym te e1 e2 + (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym te e1 e2 + (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym te e1 e2 + (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym te e1 e2 + (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym te e1 e2 + (XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym te e1 e2 + (XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym te e1 e2 + _ -> panic +translateOp3 _ _ _ _ _ = panic