copilot-theorem 2.2.1 → 3.0

raw patch · 7 files changed

+39/−590 lines, 7 filesdep −smtlib2dep ~ansi-terminaldep ~basedep ~bimapnew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies removed: smtlib2

Dependency ranges changed: ansi-terminal, base, bimap, containers, copilot-core, data-default, directory, mtl, parsec, pretty, process, random, transformers, xml

API changes (from Hackage documentation)

Files

• copilot-theorem.cabal +30/−27
• src/Copilot/Theorem/IL/PrettyPrint.hs +2/−0
• src/Copilot/Theorem/IL/Translate.hs +4/−9
• src/Copilot/Theorem/Prover/Z3.hs +0/−546
• src/Copilot/Theorem/TransSys/PrettyPrint.hs +2/−0
• src/Copilot/Theorem/TransSys/Spec.hs +1/−1
• src/Copilot/Theorem/TransSys/Translate.hs +0/−7

@@ -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

@@ -9,6 +9,8 @@ import Text.PrettyPrint.HughesPJ import qualified Data.Map as Map +import Prelude hiding ((<>))+ --------------------------------------------------------------------------------  prettyPrint :: IL -> String

@@ -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

@@ -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 })--

@@ -12,6 +12,8 @@ import qualified Data.Map   as Map import qualified Data.Bimap as Bimap +import Prelude hiding ((<>))+ --------------------------------------------------------------------------------  indent     = nest 4

@@ -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

@@ -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