Update cryptol

cryptol-saw-core/css/Main.hs

@@ -15,6 +15,7 @@ import qualified Cryptol.TypeCheck.AST as T
 import qualified Cryptol.ModuleSystem as CM
 import qualified Cryptol.ModuleSystem.Env as CME
 import qualified Cryptol.Parser as P
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import           Cryptol.Utils.PP
 import           Cryptol.Utils.Logger (quietLogger)
 
@@ -90,7 +91,9 @@ cssMain css [inputModule,name] | cssMode css == NormalMode = do
 
     modEnv <- CM.initialModuleEnv
     let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
-    (e,warn) <- CM.loadModuleByPath inputModule minp
+    (e,warn) <-
+      SMT.withSolver (CME.meSolverConfig modEnv) $ \s ->
+      CM.loadModuleByPath inputModule (minp s)
     mapM_ (print . pp) warn
     case e of
        Left msg -> print msg >> exitFailure
@@ -129,7 +132,9 @@ extractCryptol sc modEnv input = do
       Left err -> fail (show (P.ppError err))
       Right x -> return x
   let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
-  (exprResult, exprWarnings) <- CM.checkExpr pexpr minp
+  (exprResult, exprWarnings) <-
+    SMT.withSolver (CME.meSolverConfig modEnv) $ \s ->
+    CM.checkExpr pexpr (minp s)
   mapM_ (print . pp) exprWarnings
   ((_, expr, schema), _modEnv') <-
     case exprResult of

cryptol-saw-core/saw/Cryptol.sawcore

@@ -1498,15 +1498,41 @@ ecFpMul e p _ _ _ = error (TCFloat e p) "Unimplemented: fpMul";
 ecFpDiv : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpDiv e p _ _ _ = error (TCFloat e p) "Unimplemented: fpDiv";
 
-ecFpIsFinite : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
-ecFpIsFinite e p _ = error Bool "Unimplemented: fpIsFinite";
-
 ecFpToRational : (e : Num) -> (p : Num) -> TCFloat e p -> Rational;
 ecFpToRational e p _ = error Rational "Unimplemented: fpToRational";
 
 ecFpFromRational : (e : Num) -> (p : Num) -> Vec 3 Bool -> Rational -> TCFloat e p;
 ecFpFromRational e p _ _ = error (TCFloat e p) "Unimplemented: fpFromRational";
 
+fpIsNaN : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsNaN e p x = error Bool "Unimplemented: fpIsNaN";
+
+fpIsInf : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsInf e p x = error Bool "Unimplemented: fpIsInf";
+
+fpIsZero : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsZero e p x = error Bool "Unimplemented: fpIsZero";
+
+fpIsNeg : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsNeg e p x = error Bool "Unimplemented: fpIsNeg";
+
+fpIsNormal : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsNormal e p x = error Bool "Unimplemented: fpIsNormal";
+
+fpIsSubnormal : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+fpIsSubnormal e p x = error Bool "Unimplemented: fpIsSubnormal";
+
+fpFMA :
+  (e : Num) -> (p : Num) -> Vec 3 Bool ->
+  TCFloat e p -> TCFloat e p -> TCFloat e p -> TCFloat e p;
+fpFMA e p r x y z = error (TCFloat e p) "Unimplemented: fpFMA";
+
+fpAbs : (e : Num) -> (p : Num) -> TCFloat e p -> TCFloat e p;
+fpAbs e p x = error (TCFloat e p) "Unimplemented: fpAbs";
+
+fpSqrt : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p;
+fpSqrt e p r x = error (TCFloat e p) "Unimplemented: fpSqrt";
+
 
 --------------------------------------------------------------------------------
 -- Extra primitives

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -763,9 +763,17 @@ floatPrims =
   , ("fpSub",          flip scGlobalDef "Cryptol.ecFpSub")
   , ("fpMul",          flip scGlobalDef "Cryptol.ecFpMul")
   , ("fpDiv",          flip scGlobalDef "Cryptol.ecFpDiv")
-  , ("fpIsFinite",     flip scGlobalDef "Cryptol.ecFpIsFinite")
   , ("fpToRational",   flip scGlobalDef "Cryptol.ecFpToRational")
   , ("fpFromRational", flip scGlobalDef "Cryptol.ecFpFromRational")
+  , ("fpIsNaN",        flip scGlobalDef "Cryptol.fpIsNaN")
+  , ("fpIsInf",        flip scGlobalDef "Cryptol.fpIsInf")
+  , ("fpIsZero",       flip scGlobalDef "Cryptol.fpIsZero")
+  , ("fpIsNeg",        flip scGlobalDef "Cryptol.fpIsNeg")
+  , ("fpIsNormal",     flip scGlobalDef "Cryptol.fpIsNormal")
+  , ("fpIsSubnormal",  flip scGlobalDef "Cryptol.fpIsSubnormal")
+  , ("fpFMA",          flip scGlobalDef "Cryptol.fpFMA")
+  , ("fpAbs",          flip scGlobalDef "Cryptol.fpAbs")
+  , ("fpSqrt",         flip scGlobalDef "Cryptol.fpSqrt")
   ]
 
 

cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs

@@ -67,6 +67,7 @@ import qualified Cryptol.TypeCheck.Error as TE
 import qualified Cryptol.TypeCheck.Infer as TI
 import qualified Cryptol.TypeCheck.Kind as TK
 import qualified Cryptol.TypeCheck.Monad as TM
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 --import qualified Cryptol.TypeCheck.PP as TP
 
 import qualified Cryptol.ModuleSystem as M
@@ -474,13 +475,14 @@ resolveIdentifier env nm =
     [i] -> doResolve (P.UnQual (C.mkIdent i))
     xs  -> let (qs,i) = (init xs, last xs)
             in doResolve (P.Qual (C.packModName qs) (C.mkIdent i))
- where
- modEnv = eModuleEnv env
- nameEnv = getNamingEnv env
+  where
+  modEnv = eModuleEnv env
+  nameEnv = getNamingEnv env
 
- doResolve pnm =
+  doResolve pnm =
+    SMT.withSolver (ME.meSolverConfig modEnv) $ \s ->
     do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader modEnv
-       (res, _ws) <- MM.runModuleM minp $
+       (res, _ws) <- MM.runModuleM (minp s) $
           MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar pnm))
        case res of
          Left _ -> pure Nothing
@@ -644,7 +646,8 @@ liftModuleM ::
   ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv)
 liftModuleM env m =
   do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader env
-     MM.runModuleM minp m >>= moduleCmdResult
+     SMT.withSolver (ME.meSolverConfig env) $ \s ->
+       MM.runModuleM (minp s) m >>= moduleCmdResult
 
 defaultEvalOpts :: E.EvalOpts
 defaultEvalOpts = E.EvalOpts quietLogger E.defaultPPOpts