diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal --- a/copilot-theorem.cabal +++ b/copilot-theorem.cabal @@ -6,7 +6,7 @@ Some tools to prove properties on Copilot programs with k-induction model checking. -version : 2.2.1 +version : 3.0 license : BSD3 license-file : LICENSE maintainer : jonathan.laurent@ens.fr @@ -27,38 +27,41 @@ -fno-warn-missing-signatures -fcontext-stack=100 - -fpackage-trust - -trust=array - -trust=base - -trust=containers - -trust=copilot-core - -trust=directory - -trust=exceptions - -trust=process - -trust=random - -trust=unix + -- -fpackage-trust + -- -trust=array + -- -trust=base + -- -trust=containers + -- -- -trust=copilot-core + -- -trust=directory + -- -- -trust=exceptions + -- -trust=process + -- -- -trust=random + -- -trust=unix + -- -- -trust=parsec + -- -trust=bytestring + -- -- -trust=text - build-depends : base >= 4.0 && < 5 - , copilot-core == 2.2.1 - , mtl - , containers - , pretty - , process - , directory - , parsec - , data-default - , bimap - , xml - , random - , transformers - , smtlib2 >= 0.3 && < 1.0 - , ansi-terminal + build-depends : base >= 4.9 && < 5 + , ansi-terminal >= 0.8 && < 0.10 + , bimap >= 0.3 && < 0.4 + , containers >= 0.4 && < 0.7 + , data-default >= 0.7 && < 0.8 + , directory >= 1.3 && < 1.4 + , mtl >= 2.0 && < 2.3 + , parsec >= 2.0 && < 3.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 + , copilot-core >= 3.0 && < 3.1 + exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove , Copilot.Theorem.Kind2 , Copilot.Theorem.Prover.SMT - , Copilot.Theorem.Prover.Z3 + -- , Copilot.Theorem.Prover.Z3 , Copilot.Theorem.Kind2.Prover other-modules : Copilot.Theorem.Tactics 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 @@ -9,6 +9,8 @@ import Text.PrettyPrint.HughesPJ import qualified Data.Map as Map +import Prelude hiding ((<>)) + -------------------------------------------------------------------------------- prettyPrint :: IL -> String 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 @@ -21,6 +21,8 @@ import GHC.Float (float2Double) +import Data.Typeable (Typeable) + -------------------------------------------------------------------------------- -- 'nc' stands for naming convention. @@ -116,7 +118,7 @@ -------------------------------------------------------------------------------- -expr :: C.Expr a -> Trans Expr +expr :: Typeable a => C.Expr a -> Trans Expr expr (C.Const t v) = return $ trConst t v @@ -141,10 +143,6 @@ return s where trArg (C.UExpr {C.uExprExpr}) = expr uExprExpr --- Arrays and functions are treated the same way -expr (C.ExternArray ta tb name _ ind _ _) = - expr (C.ExternFun tb name [C.UExpr ta ind] Nothing Nothing) - expr (C.Op1 (C.Sign ta) e) = case ta of C.Int8 -> trSign ta e C.Int16 -> trSign ta e @@ -153,7 +151,7 @@ C.Float -> trSign ta e C.Double -> trSign ta e _ -> expr $ C.Const ta 1 - where trSign :: (Ord a, Num a) => C.Type a -> C.Expr a -> Trans Expr + where trSign :: (Typeable a, Ord a, Num a) => C.Type a -> C.Expr a -> Trans Expr trSign ta e = expr (C.Op3 (C.Mux ta) (C.Op2 (C.Lt ta) e (C.Const ta 0)) @@ -188,9 +186,6 @@ e1' <- expr e1 e2' <- expr e2 newMux cond' (trType t) e1' e2' - -expr (C.ExternStruct _ _ _ _) = undefined -expr (C.GetField _ _ _ _) = undefined trConst :: C.Type a -> a -> Expr trConst t v = case t of diff --git a/src/Copilot/Theorem/Prover/Z3.hs b/src/Copilot/Theorem/Prover/Z3.hs deleted file mode 100644 --- a/src/Copilot/Theorem/Prover/Z3.hs +++ /dev/null @@ -1,546 +0,0 @@ --------------------------------------------------------------------------------- - -{-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs, - MultiParamTypeClasses, FlexibleContexts #-} -{-# LANGUAGE Trustworthy #-} - -module Copilot.Theorem.Prover.Z3 - ( module Data.Default - , Options (..) - , induction, kInduction, onlySat, onlyValidity - ) -where - -import Copilot.Theorem.IL.Translate -import Copilot.Theorem.IL -import Copilot.Theorem.Prove (Output (..), check, Proof, Universal, Existential) -import qualified Copilot.Theorem.Prove as P - -import Control.Monad (msum, mzero, when, void, unless) -import Control.Monad.State (StateT, runStateT, get, modify) -import Control.Monad.Trans.Maybe (MaybeT (..)) - -import Data.Word -import Data.Unit (Unit(..)) -import Data.Maybe (fromJust, fromMaybe) -import Data.Default (Default(..)) -import Data.List (foldl') - -import Data.Set (Set, (\\), union) -import qualified Data.Set as Set -import Data.Map (Map) -import qualified Data.Map as Map - -import Language.SMTLib2 -import Language.SMTLib2.Pipe -import Language.SMTLib2.Connection -import Language.SMTLib2.Strategy - -import Language.SMTLib2.Internals hiding (Var) - -import System.Console.ANSI -import System.IO -import Control.Monad.Trans - --------------------------------------------------------------------------------- - --- | Tactics - -data Options = Options - { nraNLSat :: Bool - , startK :: Word32 - -- The maximum number of steps of the k-induction algorithm the prover runs - -- before giving up. - , maxK :: Word32 - - -- If `debug` is set to `True`, the SMTLib/TPTP queries produced by the - -- prover are displayed in the standard output. - , debug :: Bool - } - -instance Default Options where - def = Options - { nraNLSat = True - , startK = 0 - , maxK = 10 - , debug = False - } - -onlySat :: Options -> Proof Existential -onlySat opts = check P.Prover - { P.proverName = "OnlySat" - , P.startProver = return . ProofState opts Map.empty Map.empty Map.empty . translate - , P.askProver = onlySat' - , P.closeProver = const $ return () - } - -onlyValidity :: Options -> Proof Universal -onlyValidity opts = check P.Prover - { P.proverName = "OnlyValidity" - , P.startProver = return . ProofState opts Map.empty Map.empty Map.empty . translate - , P.askProver = onlyValidity' - , P.closeProver = const $ return () - } - -induction :: Options -> Proof Universal -induction opts = check P.Prover - { P.proverName = "Induction" - , P.startProver = return . ProofState opts Map.empty Map.empty Map.empty . translate - , P.askProver = kInduction' 0 0 - , P.closeProver = const $ return () - } - -kInduction :: Options -> Proof Universal -kInduction opts = check P.Prover - { P.proverName = "K-Induction" - , P.startProver = return . ProofState opts Map.empty Map.empty Map.empty . translate - , P.askProver = kInduction' (startK opts) (maxK opts) - , P.closeProver = const $ return () - } - -------------------------------------------------------------------------------- - --- | Checks the Copilot specification with k-induction - -type Solver = SMTConnection (DebugBackend SMTPipe) - -type ProofScript = MaybeT (StateT ProofState IO) - -runPS :: ProofScript a -> ProofState -> IO (Maybe a, ProofState) -runPS ps = runStateT (runMaybeT ps) - -data ProofState = ProofState - { options :: Options - , solvers :: Map SolverId Solver - , vars :: Map SolverId TransState - , assumps :: Map SolverId (Set Expr) - , spec :: IL - } - -data SolverId = Base | Step - deriving (Show, Ord, Eq) - -getModels :: [PropId] -> [PropId] -> ProofScript ([Expr], [Expr], [Expr], [Expr], Bool) -getModels assumptionIds toCheckIds = do - IL {modelInit, modelRec, properties, inductive} <- spec <$> get - let (as, as') = selectProps assumptionIds properties - (as'', toCheck) = selectProps toCheckIds properties - return (as ++ as', modelInit, modelRec ++ as ++ as' ++ as'', toCheck, inductive) - -getSolver :: SolverId -> ProofScript Solver -getSolver sid = do - solvers <- solvers <$> get - case Map.lookup sid solvers of - Nothing -> startNewSolver sid - Just solver -> return solver - -setSolver :: SolverId -> Solver -> ProofScript () -setSolver sid solver = - (lift . modify) $ \s -> s { solvers = Map.insert sid solver (solvers s) } - -getVars :: SolverId -> ProofScript TransState -getVars sid = do - vars <- vars <$> get - return $ case Map.lookup sid vars of - Nothing -> noVars - Just vs -> vs - -setVars :: SolverId -> TransState -> ProofScript () -setVars sid vs = - (lift . modify) $ \s -> s { vars = Map.insert sid vs (vars s) } - -newAssumps :: SolverId -> [Expr] -> ProofScript [Expr] -newAssumps sid as' = do - assumps <- assumps <$> get - case Map.lookup sid assumps of - Nothing -> do - modify $ \s -> s { assumps = Map.insert sid (Set.fromList as') assumps } - return as' - Just as -> do - let as'' = (Set.fromList as') `union` as - modify $ \s -> s { assumps = Map.insert sid as'' assumps } - return $ Set.elems $ (Set.fromList as') \\ as - -deleteSolver :: SolverId -> ProofScript () -deleteSolver sid = - (lift . modify) $ \s -> s { solvers = Map.delete sid (solvers s) } - -startNewSolver :: SolverId -> ProofScript Solver -startNewSolver sid = do - pipe <- liftIO $ createSMTPipe "z3" ["-smt2", "-in"] - dbg <- (options <$> get >>= return . debug) - s <- liftIO $ open (namedDebugBackend (show sid) (not dbg) pipe) - setSolver sid s - return s - -stop :: SolverId -> ProofScript () -stop sid = do - s <- getSolver sid - deleteSolver sid - liftIO $ close s - -stopSolvers :: ProofScript () -stopSolvers = do - solvers <- solvers <$> get - mapM_ stop (fst <$> Map.toList solvers) - -proofKind :: Integer -> String -proofKind 0 = "induction" -proofKind k = "k-induction (k = " ++ show k ++ ")" - -entailment :: SolverId -> [Expr] -> [Expr] -> ProofScript CheckSatResult -entailment sid assumptions props = do - s <- getSolver sid - liftIO $ performSMT s $ setOption (ProduceModels True) - -- liftIO $ performSMT s $ setOption (ProduceProofs True) - -- liftIO $ performSMT s $ setOption (ProduceUnsatCores True) - vs <- getVars sid - assumps' <- newAssumps sid assumptions - (_, vs') <- liftIO $ performSMT s $ runStateT (mapM_ (\e -> transB e >>= lift . assert) assumps') vs - setVars sid vs' - liftIO $ performSMT s $ push - _ <- liftIO $ performSMT s $ runStateT - (transB (bsimpl (foldl' (Op2 Bool Or) (ConstB False) $ map (Op1 Bool Not) props)) >>= lift . assert) vs' - - nraNL <- (options <$> get >>= return . nraNLSat) - res <- if nraNL - then liftIO $ performSMT s $ checkSat' (Just (UsingParams (CustomTactic "qfnra-nlsat") [])) - (CheckSatLimits (Just 5000) Nothing) - else liftIO $ performSMT s $ checkSat' Nothing (CheckSatLimits (Just 5000) Nothing) - - when (res == Sat) $ void $ liftIO $ performSMT s $ getModel - -- when (res == Unsat) $ void $ liftIO $ performSMT s $ getProof - liftIO $ performSMT s $ pop - -- liftIO $ print model - return res - -unknown :: ProofScript a -unknown = mzero - -unknown' :: String -> ProofScript Output -unknown' msg = return $ Output P.Unknown [msg] - -invalid :: String -> ProofScript Output -invalid msg = return $ Output P.Invalid [msg] - -sat :: String -> ProofScript Output -sat msg = return $ Output P.Sat [msg] - -valid :: String -> ProofScript Output -valid msg = return $ Output P.Valid [msg] - -kInduction' :: Word32 -> Word32 -> ProofState -> [PropId] -> [PropId] -> IO Output -kInduction' startK maxK s as ps = (fromMaybe (Output P.Unknown ["proof by " ++ proofKind (toInteger maxK) ++ " failed"]) . fst) - <$> runPS (msum (map induction [(toInteger startK) .. (toInteger maxK)]) <* stopSolvers) s - where - induction k = do - (assumps, modelInit, modelRec, toCheck, inductive) <- getModels as ps - - let base = [evalAt (Fixed i) m | m <- modelRec, i <- [0 .. k]] - baseInv = [evalAt (Fixed k) m | m <- toCheck] - - let step = [evalAt (_n_plus i) m | m <- modelRec, i <- [0 .. k + 1]] - ++ [evalAt (_n_plus i) m | m <- toCheck, i <- [0 .. k]] - stepInv = [evalAt (_n_plus $ k + 1) m | m <- toCheck] - - entailment Base assumps [ConstB False] >>= \case - Unknown -> unknown - Unsat -> invalid $ "inconsistent assumptions" - Sat -> entailment Base (modelInit ++ base) baseInv >>= \case - Sat -> invalid $ "base case failed for " ++ proofKind k - Unknown -> unknown - Unsat -> - if not inductive then valid ("proved without induction") - else entailment Step step stepInv >>= \case - Sat -> unknown - Unknown -> unknown - Unsat -> valid $ "proved with " ++ proofKind k - -onlySat' :: ProofState -> [PropId] -> [PropId] -> IO Output -onlySat' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s - where - script = do - (assumps, modelInit, modelRec, toCheck, inductive) <- getModels as ps - - let base = map (evalAt (Fixed 0)) modelRec - baseInv = map (evalAt (Fixed 0)) toCheck - - entailment Base assumps [ConstB False] >>= \case - Unknown -> unknown - Unsat -> invalid $ "inconsistent assumptions" - Sat -> if inductive - then unknown' "proposition requires induction to prove." - else entailment Base (modelInit ++ base) (map (Op1 Bool Not) baseInv) >>= \case - Unsat -> invalid "prop not satisfiable" - Unknown -> unknown' "failed to find a satisfying model" - Sat -> sat "prop is satisfiable" - -onlyValidity' :: ProofState -> [PropId] -> [PropId] -> IO Output -onlyValidity' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s - where - script = do - (assumps, modelInit, modelRec, toCheck, inductive) <- getModels as ps - - let base = map (evalAt (Fixed 0)) modelRec - baseInv = map (evalAt (Fixed 0)) toCheck - - entailment Base assumps [ConstB False] >>= \case - Unknown -> unknown - Unsat -> invalid $ "inconsistent assumptions" - Sat -> if inductive - then unknown' "proposition requires induction to prove." - else entailment Base (modelInit ++ base) baseInv >>= \case - Unsat -> valid "proof by Z3" - Unknown -> unknown - Sat -> invalid "Z3 found a counter-example." - -selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr]) -selectProps propIds properties = - (squash . unzip) [(as, p) | (id, (as, p)) <- Map.toList properties, id `elem` propIds] - where squash (a, b) = (concat a, b) - --------------------------------------------------------------------------------- - --- | This is all very ugly. It might make better sense to go straight from Core to SMTExpr, or maybe use SBV instead. - -type Trans = StateT TransState SMT - -data TransState = TransState - { boolVars :: Map String (SMTExpr Bool) - , bv8Vars :: Map String (SMTExpr BV8) - , bv16Vars :: Map String (SMTExpr BV16) - , bv32Vars :: Map String (SMTExpr BV32) - , bv64Vars :: Map String (SMTExpr BV64) - , ratVars :: Map String (SMTExpr Rational) - } - -noVars :: TransState -noVars = TransState Map.empty Map.empty Map.empty Map.empty Map.empty Map.empty - -getBoolVar :: String -> Trans (SMTExpr Bool) -getBoolVar = getVar boolVars (\v s -> s {boolVars = v}) - -getBV8Var :: String -> Trans (SMTExpr BV8) -getBV8Var = getVar bv8Vars (\v s -> s {bv8Vars = v}) - -getBV16Var :: String -> Trans (SMTExpr BV16) -getBV16Var = getVar bv16Vars (\v s -> s {bv16Vars = v}) - -getBV32Var :: String -> Trans (SMTExpr BV32) -getBV32Var = getVar bv32Vars (\v s -> s {bv32Vars = v}) - -getBV64Var :: String -> Trans (SMTExpr BV64) -getBV64Var = getVar bv64Vars (\v s -> s {bv64Vars = v}) - -getRatVar :: String -> Trans (SMTExpr Rational) -getRatVar = getVar ratVars (\v s -> s {ratVars = v}) - -getVar :: (Unit (SMTAnnotation t), SMTType t) => (TransState -> Map String (SMTExpr t)) -> (Map String (SMTExpr t) -> TransState -> TransState) -> String -> Trans (SMTExpr t) -getVar proj upd v = do - vs <- proj <$> get - case Map.lookup v vs of - Nothing -> do - newVar <- lift $ varNamed v - modify $ upd $ Map.insert v newVar vs - return newVar - Just x -> return x - -transB :: Expr -> Trans (SMTExpr Bool) -transB = \case - ConstB b -> return $ constant b - Ite _ c e1 e2 -> ite <$> transB c <*> transB e1 <*> transB e2 - Op1 _ Not e -> not' <$> transB e - Op2 _ And e1 e2 -> (.&&.) <$> transB e1 <*> transB e2 - Op2 _ Or e1 e2 -> (.||.) <$> transB e1 <*> transB e2 - Op2 _ Eq e1 e2 -> case typeOf e1 of - Bool -> (.==.) <$> transB e1 <*> transB e2 - Real -> (.==.) <$> transR e1 <*> transR e2 - BV8 -> (.==.) <$> transBV8 e1 <*> transBV8 e2 - BV16 -> (.==.) <$> transBV16 e1 <*> transBV16 e2 - BV32 -> (.==.) <$> transBV32 e1 <*> transBV32 e2 - BV64 -> (.==.) <$> transBV64 e1 <*> transBV64 e2 - SBV8 -> (.==.) <$> transBV8 e1 <*> transBV8 e2 - SBV16 -> (.==.) <$> transBV16 e1 <*> transBV16 e2 - SBV32 -> (.==.) <$> transBV32 e1 <*> transBV32 e2 - SBV64 -> (.==.) <$> transBV64 e1 <*> transBV64 e2 - e@(Op2 _ Le e1 e2) -> case typeOf e1 of - Bool -> error $ "Comparing Bools: " ++ show e - Real -> (.<=.) <$> transR e1 <*> transR e2 - BV8 -> bvule <$> transBV8 e1 <*> transBV8 e2 - BV16 -> bvule <$> transBV16 e1 <*> transBV16 e2 - BV32 -> bvule <$> transBV32 e1 <*> transBV32 e2 - BV64 -> bvule <$> transBV64 e1 <*> transBV64 e2 - SBV8 -> bvule <$> transBV8 e1 <*> transBV8 e2 - SBV16 -> bvule <$> transBV16 e1 <*> transBV16 e2 - SBV32 -> bvule <$> transBV32 e1 <*> transBV32 e2 - SBV64 -> bvule <$> transBV64 e1 <*> transBV64 e2 - e@(Op2 _ Ge e1 e2) -> case typeOf e1 of - Bool -> error $ "Comparing Bools: " ++ show e - Real -> (.>=.) <$> transR e1 <*> transR e2 - BV8 -> bvuge <$> transBV8 e1 <*> transBV8 e2 - BV16 -> bvuge <$> transBV16 e1 <*> transBV16 e2 - BV32 -> bvuge <$> transBV32 e1 <*> transBV32 e2 - BV64 -> bvuge <$> transBV64 e1 <*> transBV64 e2 - SBV8 -> bvuge <$> transBV8 e1 <*> transBV8 e2 - SBV16 -> bvuge <$> transBV16 e1 <*> transBV16 e2 - SBV32 -> bvuge <$> transBV32 e1 <*> transBV32 e2 - SBV64 -> bvuge <$> transBV64 e1 <*> transBV64 e2 - e@(Op2 _ Lt e1 e2) -> case typeOf e1 of - Bool -> error $ "Comparing Bools: " ++ show e - Real -> (.<.) <$> transR e1 <*> transR e2 - BV8 -> bvult <$> transBV8 e1 <*> transBV8 e2 - BV16 -> bvult <$> transBV16 e1 <*> transBV16 e2 - BV32 -> bvult <$> transBV32 e1 <*> transBV32 e2 - BV64 -> bvult <$> transBV64 e1 <*> transBV64 e2 - SBV8 -> bvult <$> transBV8 e1 <*> transBV8 e2 - SBV16 -> bvult <$> transBV16 e1 <*> transBV16 e2 - SBV32 -> bvult <$> transBV32 e1 <*> transBV32 e2 - SBV64 -> bvult <$> transBV64 e1 <*> transBV64 e2 - e@(Op2 _ Gt e1 e2) -> case typeOf e1 of - Bool -> error $ "Comparing Bools: " ++ show e - Real -> (.>.) <$> transR e1 <*> transR e2 - BV8 -> bvugt <$> transBV8 e1 <*> transBV8 e2 - BV16 -> bvugt <$> transBV16 e1 <*> transBV16 e2 - BV32 -> bvugt <$> transBV32 e1 <*> transBV32 e2 - BV64 -> bvugt <$> transBV64 e1 <*> transBV64 e2 - SBV8 -> bvugt <$> transBV8 e1 <*> transBV8 e2 - SBV16 -> bvugt <$> transBV16 e1 <*> transBV16 e2 - SBV32 -> bvugt <$> transBV32 e1 <*> transBV32 e2 - SBV64 -> bvugt <$> transBV64 e1 <*> transBV64 e2 - SVal _ s i -> getBoolVar $ ncVar s i - e -> error $ "Encountered unhandled expression (Bool): " ++ show e - -ncVar :: [Char] -> SeqIndex -> [Char] -ncVar s (Fixed i) = s ++ "_" ++ show i -ncVar s (Var i) = s ++ "_n" ++ show i - -transR :: Expr -> Trans (SMTExpr Rational) -transR = \case - ConstR n -> return $ constant $ toRational n - Ite _ c e1 e2 -> ite <$> transB c <*> transR e1 <*> transR e2 - - Op1 _ Neg e -> app neg <$> transR e - Op1 _ Abs e -> app SMTAbs <$> transR e - - Op2 _ Add e1 e2 -> (\x y -> app plus [x, y]) <$> transR e1 <*> transR e2 - Op2 _ Sub e1 e2 -> (\x y -> app minus (x, y)) <$> transR e1 <*> transR e2 - Op2 _ Mul e1 e2 -> (\x y -> app mult [x, y]) <$> transR e1 <*> transR e2 - Op2 _ Fdiv e1 e2 -> divide <$> transR e1 <*> transR e2 - - Op2 _ Pow e1 e2 -> do - let pow = SMTBuiltIn "^" () :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational - (\x y -> app pow (x, y)) <$> transR e1 <*> transR e2 - - SVal _ s i -> getRatVar $ ncVar s i - e -> error $ "Encountered unhandled expression (Rat): " ++ show e - --- TODO(chathhorn): bleghh -transBV8 :: Expr -> Trans (SMTExpr BV8) -transBV8 = \case - ConstI _ n -> return $ constant $ BitVector n - Ite _ c e1 e2 -> ite <$> transB c <*> transBV8 e1 <*> transBV8 e2 - Op1 _ Abs e -> abs <$> transBV8 e - Op1 _ Neg e -> negate <$> transBV8 e - Op2 _ Add e1 e2 -> (+) <$> transBV8 e1 <*> transBV8 e2 - Op2 _ Sub e1 e2 -> (-) <$> transBV8 e1 <*> transBV8 e2 - Op2 _ Mul e1 e2 -> (*) <$> transBV8 e1 <*> transBV8 e2 - SVal _ s i -> getBV8Var $ ncVar s i - e -> error $ "Encountered unhandled expression (BV8): " ++ show e - -transBV16 :: Expr -> Trans (SMTExpr BV16) -transBV16 = \case - ConstI _ n -> return $ constant $ BitVector n - Ite _ c e1 e2 -> ite <$> transB c <*> transBV16 e1 <*> transBV16 e2 - Op1 _ Abs e -> abs <$> transBV16 e - Op1 _ Neg e -> negate <$> transBV16 e - Op2 _ Add e1 e2 -> (+) <$> transBV16 e1 <*> transBV16 e2 - Op2 _ Sub e1 e2 -> (-) <$> transBV16 e1 <*> transBV16 e2 - Op2 _ Mul e1 e2 -> (*) <$> transBV16 e1 <*> transBV16 e2 - SVal _ s i -> getBV16Var $ ncVar s i - e -> error $ "Encountered unhandled expression (BV16): " ++ show e - -transBV32 :: Expr -> Trans (SMTExpr BV32) -transBV32 = \case - ConstI _ n -> return $ constant $ BitVector n - Ite _ c e1 e2 -> ite <$> transB c <*> transBV32 e1 <*> transBV32 e2 - Op1 _ Abs e -> abs <$> transBV32 e - Op1 _ Neg e -> negate <$> transBV32 e - Op2 _ Add e1 e2 -> (+) <$> transBV32 e1 <*> transBV32 e2 - Op2 _ Sub e1 e2 -> (-) <$> transBV32 e1 <*> transBV32 e2 - Op2 _ Mul e1 e2 -> (*) <$> transBV32 e1 <*> transBV32 e2 - SVal _ s i -> getBV32Var $ ncVar s i - e -> error $ "Encountered unhandled expression (BV32): " ++ show e - -transBV64 :: Expr -> Trans (SMTExpr BV64) -transBV64 = \case - ConstI _ n -> return $ constant $ BitVector n - Ite _ c e1 e2 -> ite <$> transB c <*> transBV64 e1 <*> transBV64 e2 - Op1 _ Abs e -> abs <$> transBV64 e - Op1 _ Neg e -> negate <$> transBV64 e - Op2 _ Add e1 e2 -> (+) <$> transBV64 e1 <*> transBV64 e2 - Op2 _ Sub e1 e2 -> (-) <$> transBV64 e1 <*> transBV64 e2 - Op2 _ Mul e1 e2 -> (*) <$> transBV64 e1 <*> transBV64 e2 - SVal _ s i -> getBV64Var $ ncVar s i - e -> error $ "Encountered unhandled expression (BV64): " ++ show e - ------------------------------------------------------ --- Debug stuff from the the smtlib2 library github -- ------------------------------------------------------ - -namedDebugBackend :: String -> Bool -> b -> DebugBackend b -namedDebugBackend name mute b = DebugBackend b stderr (Just 0) (Just name) True mute - -data DebugBackend b = DebugBackend - { debugBackend :: b - , debugHandle :: Handle - , debugLines :: Maybe Integer - , debugPrefix :: Maybe String - , debugUseColor :: Bool - , mute :: Bool - } - -instance (SMTBackend b m,MonadIO m) => SMTBackend (DebugBackend b) m where - smtGetNames b = smtGetNames (debugBackend b) - smtNextName b = smtNextName (debugBackend b) - smtHandle b req = do - getName <- smtGetNames (debugBackend b) - nxtName <- smtNextName (debugBackend b) - (dts,b1) <- smtHandle (debugBackend b) SMTDeclaredDataTypes - let rendering = renderSMTRequest nxtName getName dts req - case debugPrefix b of - Nothing -> return () - Just prf -> case rendering of - Right "" -> return () - _ -> do - when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull Cyan] - liftIO $ unless (mute b) $ hPutStr (debugHandle b) prf - nline <- case rendering of - Right "" -> return (debugLines b) - _ -> do - nline <- case debugLines b of - Nothing -> return Nothing - Just line -> do - when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull Red] - let line_str = show line - line_str_len = length line_str - line_str' = replicate (4-line_str_len) ' '++line_str++" " - liftIO $ unless (mute b) $ hPutStr (debugHandle b) line_str' - return (Just (line+1)) - case rendering of - Left l -> do - when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull Green] - liftIO $ unless (mute b) $ hPutStrLn (debugHandle b) (show l) - Right msg -> do - when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull White] - liftIO $ unless (mute b) $ hPutStr (debugHandle b) $ unlines $ fmap (\xs -> ';':xs) (lines msg) - return nline - (resp,b2) <- smtHandle b1 req - case renderSMTResponse getName dts req resp of - Nothing -> return () - Just str -> do - when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset,SetColor Foreground Dull Blue] - liftIO $ unless (mute b) $ hPutStrLn (debugHandle b) str - when (debugUseColor b) $ liftIO $ hSetSGR (debugHandle b) [Reset] - return (resp,b { debugBackend = b2 , debugLines = nline }) - - diff --git a/src/Copilot/Theorem/TransSys/PrettyPrint.hs b/src/Copilot/Theorem/TransSys/PrettyPrint.hs --- a/src/Copilot/Theorem/TransSys/PrettyPrint.hs +++ b/src/Copilot/Theorem/TransSys/PrettyPrint.hs @@ -12,6 +12,8 @@ import qualified Data.Map as Map import qualified Data.Bimap as Bimap +import Prelude hiding ((<>)) + -------------------------------------------------------------------------------- indent = nest 4 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 @@ -126,7 +126,7 @@ descrRhsVars (VarDescr _ (Constrs cs)) = mconcat (map (foldExpr varOcc) cs) - in Map.fold (Set.union . descrRhsVars) Set.empty (nodeLocalVars n) + in Map.foldr (Set.union . descrRhsVars) Set.empty (nodeLocalVars n) nodeImportedExtVarsSet :: Node -> Set ExtVar nodeImportedExtVarsSet = Map.keysSet . Bimap.toMapR . nodeImportedVars 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 @@ -37,7 +37,6 @@ ncExternVarNode name = "ext-" ++ name ncExternFunNode name = "fun-" ++ name -ncExternArrNode name = "arr-" ++ name ncImported :: NodeId -> String -> String ncImported n s = n ++ ncSep ++ s @@ -204,12 +203,6 @@ newUnconstrainedVar t expr t (C.ExternFun _ _ _ _ _) = newUnconstrainedVar t - -expr t (C.ExternArray _ _ _ _ _ _ _) = newUnconstrainedVar t - -expr t (C.ExternStruct _ _ _ _) = newUnconstrainedVar t - -expr t (C.GetField _ _ _ _) = undefined newUnconstrainedVar :: Type t -> Trans (Expr t) newUnconstrainedVar t = do