Merge branch 'releases'

cryptol.cabal

@@ -1,5 +1,5 @@
 Name:                cryptol
-Version:             2.2.2
+Version:             2.2.3
 Synopsis:            Cryptol: The Language of Cryptography
 Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>.
 License:             BSD3
@@ -23,7 +23,7 @@ source-repository head
 source-repository this
   type:     git
   location: https://github.com/GaloisInc/cryptol.git
-  tag:      v2.2.2
+  tag:      v2.2.3
 
 flag static
   default: False

src/Cryptol/TypeCheck/Solver/Smtlib.hs

@@ -0,0 +1,168 @@
+-- |
+-- Module      :  $Header$
+-- Copyright   :  (c) 2013-2015 Galois, Inc.
+-- License     :  BSD3
+-- Maintainer  :  cryptol@galois.com
+-- Stability   :  provisional
+-- Portability :  portable
+
+{-# LANGUAGE OverloadedStrings, RecordWildCards, PatternGuards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Cryptol.TypeCheck.Solver.Smtlib (simpDelayed) where
+
+import           Cryptol.TypeCheck.AST as Cry
+import           Cryptol.TypeCheck.Subst (fvs)
+import           Cryptol.TypeCheck.InferTypes(Goal(..))
+import           Cryptol.TypeCheck.Solver.FinOrd
+
+import           SMTLib2      as SMT
+import           SMTLib2.Int  as SMT
+import           SMTLib2.Core as SMT
+import qualified Control.Exception as X
+import           Data.String(fromString)
+import           Data.List(partition)
+import           Data.Maybe(mapMaybe)
+import qualified Data.Set as Set
+import           System.Directory(findExecutable)
+import           System.Environment(getExecutablePath)
+import           System.FilePath((</>), takeDirectory)
+import           System.Process(readProcessWithExitCode)
+import           System.Exit(ExitCode(..))
+
+
+simpDelayed :: [TParam] -> OrdFacts -> [Prop] -> [Goal] -> IO [Goal]
+simpDelayed _qvars ordAsmp origAsmps goals =
+  do ans <- mapM tryGoal goals
+
+     let (_natsDone,natsNot) = partition snd ans
+     -- XXX: check that `natsDone` also hold for the infinite case
+     return (map fst natsNot)
+
+  where
+  vs = map toVar (Set.toList (fvs (ordFactsToProps ordAsmp,
+                                        (origAsmps,map goal goals))))
+
+  asmps = mapMaybe toPred (ordFactsToProps ordAsmp ++ origAsmps)
+
+  tryGoal g = case toPred (goal g) of
+                Just q -> do res <- cvc4 (toScript vs asmps q)
+                             return (g, res == Unsat)
+                              -- i.e., solved for Nats, anyway
+                Nothing -> return (g, False)
+
+toTerm :: Cry.Type -> Maybe SMT.Expr
+toTerm ty =
+  case ty of
+    TCon tc ts  ->
+      do es <- mapM toTerm ts
+         case (tc, es) of
+           (TC (TCNum x), [])  -> return (SMT.num x)
+
+           (TF TCAdd, [e1,e2]) -> return (SMT.nAdd e1 e2)
+           (TF TCSub, [e1,e2]) -> return (SMT.nSub e1 e2)
+           (TF TCMul, [e1,e2]) -> return (SMT.nMul e1 e2)
+           (TF TCDiv, [e1,e2]) -> return (SMT.nDiv e1 e2)
+           (TF TCMod, [e1,e2]) -> return (SMT.nMod e1 e2)
+
+           (TF TCMin, [e1,e2]) -> return (SMT.ite (SMT.nLeq e1 e2) e1 e2)
+           (TF TCMax, [e1,e2]) -> return (SMT.ite (SMT.nLeq e1 e2) e2 e1)
+
+           (TF TCLg2,   [_])   -> Nothing
+           (TF TCExp,   [e1,e2])
+               | Lit (LitNum x) <- e2
+               , x >= 0        -> return $
+                                  if x == 0
+                                     then SMT.num (1 :: Int)
+                                     else foldr1 SMT.nMul
+                                        $ replicate (fromInteger x) e1
+               | otherwise     -> Nothing
+
+           (TF TCWidth, [_])   -> Nothing -- == lg2 (e + 1)
+
+           (TF TCLenFromThen, _) -> Nothing
+           (TF TCLenFromThenTo, _) -> Nothing
+
+           _  -> Nothing
+
+
+    Cry.TVar x      -> return (smtVar (toVar x))
+    TUser _ _ t -> toTerm t
+    TRec _      -> Nothing
+
+toVar :: TVar -> SMT.Name
+toVar (TVFree  x _ _ _) = fromString ("free"  ++ show x)
+toVar (TVBound x _) = fromString ("bound" ++ show x)
+
+smtVar :: SMT.Name -> SMT.Expr
+smtVar x = app (I x []) []
+
+toPred :: Cry.Prop -> Maybe SMT.Expr
+toPred ty =
+  case ty of
+    TCon tc ts ->
+      do es <- mapM toTerm ts
+         case (tc,es) of
+           (PC PEqual, [e1,e2])  -> return (e1 === e2)
+           (PC PGeq, [e1,e2])    -> return (SMT.nLeq e2 e1)
+
+           _                     -> Nothing
+
+    Cry.TVar {} -> Nothing
+    TUser _ _ t -> toPred t
+    TRec {}     -> Nothing
+
+toScript :: [SMT.Name] -> [SMT.Expr] -> SMT.Expr -> SMT.Script
+toScript vs pes q =
+  Script $
+    [ SMT.CmdSetLogic "QF_LIA" ] ++
+    [ SMT.CmdDeclareFun x [] SMT.tInt | x <- vs ] ++
+    [ SMT.CmdAssert (SMT.nLeq (SMT.num (0::Int)) (smtVar x)) | x <- vs ] ++
+    [ SMT.CmdAssert p | p <- pes ] ++
+    [ SMT.CmdAssert (SMT.not q) ] ++
+    [ SMT.CmdCheckSat ]
+
+data SMTResult = Sat | Unsat | Unknown
+                  deriving (Eq,Show)
+
+-- | First look for @cvc4@ in the path, but failing that, assume that it's 
+-- installed side-by-side with Cryptol.
+findCvc4 :: IO FilePath
+findCvc4 = do
+  mfp <- findExecutable "cvc4"
+  case mfp of
+    Just fp -> return fp
+    Nothing -> do
+     bindir <- takeDirectory `fmap` getExecutablePath
+     return (bindir </> "cvc4")
+
+cvc4 :: SMT.Script -> IO SMTResult
+cvc4 script =
+  X.handle (\(_::X.IOException) -> return Unknown) $
+  do let txt = show (SMT.pp script)
+     cvc4path <- findCvc4
+     (ex,out,err) <- readProcessWithExitCode cvc4path ["--lang=smtlib2","--rewrite-divk","-"] txt
+     case ex of
+       ExitFailure 10  -> return Sat
+       ExitFailure 20  -> return Unsat
+       ExitFailure 127 -> return Unknown -- cvc4 program not found
+       ExitSuccess
+         | out == "sat\n"     -> return Sat
+         | out == "unsat\n"   -> return Unsat
+         | out == "unknwon\n" -> return Unknown
+
+       -- XXX: We should not print to STDOUT here.
+       -- Report to a separate logger.
+       x -> do putStrLn "Called to CVC4 failed!!!"
+               putStrLn ("Exit code: " ++ show x)
+               putStrLn "Script"
+               putStrLn txt
+
+               putStrLn "Standard out:"
+               putStrLn out
+
+               putStrLn "Standard error:"
+               putStrLn err
+
+               return Unknown -- or error
+
+