From 08c59959b06bc5e8c30aed17dcc9b28f7432d4aa Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 15 Apr 2021 10:58:30 -0700 Subject: [PATCH] Updates flowing from cryptol PRs GaloisInc/cryptol#1048 GaloisInc/cryptol#1136 GaloisInc/cryptol#1165 GaloisInc/cryptol#1171 --- cryptol-saw-core/saw/Cryptol.sawcore | 37 ++++++--- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 83 ++++++++++--------- .../src/Verifier/SAW/CryptolEnv.hs | 33 ++------ saw/SAWScript/REPL/Monad.hs | 5 +- src/SAWScript/AutoMatch/Cryptol.hs | 3 + src/SAWScript/Builtins.hs | 2 + src/SAWScript/Interpreter.hs | 1 + src/SAWScript/Value.hs | 2 +- src/SAWScript/VerificationCheck.hs | 4 +- src/SAWScript/X86Spec.hs | 4 +- 10 files changed, 95 insertions(+), 79 deletions(-) diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore index 6a1487d8c2..6d081c5158 100644 --- a/cryptol-saw-core/saw/Cryptol.sawcore +++ b/cryptol-saw-core/saw/Cryptol.sawcore @@ -1208,22 +1208,37 @@ ecCat = -- Case for (TCNum m, TCInf) (\ (a:sort 0) -> streamAppend a m)); -ecSplitAt : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> - #(seq m a, seq n a); -ecSplitAt = +ecTake : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq m a; +ecTake = + Num_rec + (\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> seq m a) + + (\ (m:Nat) -> + Num_rec + (\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> Vec m a) + -- The case (TCNum m, TCNum n) + (\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> take a m n xs) + -- The case (TCNum m, infinity) + (\ (a:sort 0) -> \ (xs: Stream a) -> streamTake a m xs)) + + (Num_rec + (\ (n:Num) -> (a:sort 0) -> seq (tcAdd TCInf n) a -> Stream a) + -- The case (TCInf, TCNum n) + (\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs) + -- The case (TCInf, TCInf) + (\ (a:sort 0) -> \ (xs:Stream a) -> xs)); + +ecDrop : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq n a; +ecDrop = finNumRec - (\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> - #(seq m a, seq n a)) + (\ (m:Num) -> (n:Num) -> (a:sort 0) -> seq (tcAdd m n) a -> seq n a) (\ (m:Nat) -> Num_rec - (\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> - #(Vec m a, seq n a)) + (\ (n:Num) -> (a:sort 0) -> seq (tcAdd (TCNum m) n) a -> seq n a) -- The case (TCNum n, TCNum m) - (\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> - (take a m n xs, drop a m n xs)) + (\ (n:Nat) -> \ (a:sort 0) -> \ (xs: Vec (addNat m n) a) -> drop a m n xs) -- The case (TCNum m, infinity) - (\ (a:sort 0) -> \ (xs: Stream a) -> - (streamTake a m xs, streamDrop a m xs))); + (\ (a:sort 0) -> \ (xs: Stream a) -> streamDrop a m xs)); ecJoin : (m n : Num) -> (a : sort 0) -> seq m (seq n a) -> seq (tcMul m n) a; ecJoin m = diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 3814999b86..087e128f9e 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -35,6 +35,8 @@ import Text.URI import qualified Cryptol.Eval.Type as TV import qualified Cryptol.Backend.Monad as V +import qualified Cryptol.Backend.SeqMap as V +import qualified Cryptol.Backend.WordValue as V import qualified Cryptol.Eval.Value as V import qualified Cryptol.Eval.Concrete as V import Cryptol.Eval.Type (evalValType) @@ -45,6 +47,7 @@ import qualified Cryptol.ModuleSystem.Name as C import qualified Cryptol.Utils.Ident as C ( Ident, PrimIdent(..), mkIdent, prelPrim, floatPrim, arrayPrim , ModName, modNameToText, identText, interactiveName + , ModPath(..), modPathSplit ) import qualified Cryptol.Utils.RecordMap as C import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf) @@ -740,7 +743,8 @@ prelPrims = -- -- Sequences primitives , ("#", flip scGlobalDef "Cryptol.ecCat") -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d - , ("splitAt", flip scGlobalDef "Cryptol.ecSplitAt") -- {a,b,c} (fin a) => [a+b] c -> ([a]c,[b]c) + , ("take", flip scGlobalDef "Cryptol.ecTake") -- {front, back, a} [front + back]a -> [front]a + , ("drop", flip scGlobalDef "Cryptol.ecDrop") -- {front, back, a} (fin front) => [front + back]a -> [back]a , ("join", flip scGlobalDef "Cryptol.ecJoin") -- {a,b,c} (fin b) => [a][b]c -> [a * b]c , ("split", flip scGlobalDef "Cryptol.ecSplit") -- {a,b,c} (fin b) => [a * b] c -> [a][b] c , ("reverse", flip scGlobalDef "Cryptol.ecReverse") -- {a,b} (fin a) => [a] b -> [a] b @@ -1231,18 +1235,20 @@ importName cnm = case C.nameInfo cnm of C.Parameter -> fail ("Cannot import non-top-level name: " ++ show cnm) C.Declared modNm _ - | modNm == C.interactiveName -> + | modNm == C.TopModule C.interactiveName -> let shortNm = C.identText (C.nameIdent cnm) aliases = [shortNm] uri = cryptolURI [shortNm] (Just (C.nameUnique cnm)) in pure (ImportedName uri aliases) | otherwise -> - let modNmTxt = C.modNameToText modNm - modNms = Text.splitOn "::" modNmTxt - shortNm = C.identText (C.nameIdent cnm) - aliases = [shortNm, modNmTxt <> "::" <> shortNm] - uri = cryptolURI (modNms ++ [shortNm]) Nothing + let (topMod, nested) = C.modPathSplit modNm + modNmTxt = C.modNameToText topMod + modNms = (Text.splitOn "::" modNmTxt) ++ map C.identText nested + shortNm = C.identText (C.nameIdent cnm) + longNm = Text.intercalate "::" ([modNmTxt] ++ map C.identText nested ++ [shortNm]) + aliases = [shortNm, longNm] + uri = cryptolURI (modNms ++ [shortNm]) Nothing in pure (ImportedName uri aliases) -- | Currently this imports declaration groups by inlining all the @@ -1646,22 +1652,22 @@ scCryptolEq sc x y = -- | Convert from SAWCore's Value type to Cryptol's, guided by the -- Cryptol type schema. -exportValueWithSchema :: C.Schema -> SC.CValue -> V.Value +exportValueWithSchema :: C.Schema -> SC.CValue -> V.Eval V.Value exportValueWithSchema (C.Forall [] [] ty) v = exportValue (evalValType mempty ty) v -exportValueWithSchema _ _ = V.VPoly mempty (error "exportValueWithSchema") +exportValueWithSchema _ _ = pure (V.VPoly mempty (error "exportValueWithSchema")) -- TODO: proper support for polymorphic values -exportValue :: TV.TValue -> SC.CValue -> V.Value +exportValue :: TV.TValue -> SC.CValue -> V.Eval V.Value exportValue ty v = case ty of TV.TVBit -> - V.VBit (SC.toBool v) + pure (V.VBit (SC.toBool v)) TV.TVInteger -> - V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer") + pure (V.VInteger (case v of SC.VInt x -> x; _ -> error "exportValue: expected integer")) TV.TVIntMod _modulus -> - V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod") + pure (V.VInteger (case v of SC.VIntMod _ x -> x; _ -> error "exportValue: expected intmod")) TV.TVArray{} -> error $ "exportValue: (on array type " ++ show ty ++ ")" @@ -1673,28 +1679,29 @@ exportValue ty v = case ty of case v of SC.VWord w -> V.word V.Concrete (toInteger (width w)) (unsigned w) SC.VVector xs - | TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) (V.ready (V.LargeBitsVal (fromIntegral (Vector.length xs)) - (V.finiteSeqMap . map (V.ready . V.VBit . SC.toBool . SC.runIdentity . force) $ Fold.toList xs))) - | otherwise -> V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap $ - map (V.ready . exportValue e . SC.runIdentity . force) $ Vector.toList xs + | TV.isTBit e -> V.VWord (toInteger (Vector.length xs)) <$> + V.bitmapWordVal V.Concrete (toInteger (Vector.length xs)) + (V.finiteSeqMap V.Concrete . map (V.ready . SC.toBool . SC.runIdentity . force) $ Fold.toList xs) + | otherwise -> pure . V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap V.Concrete $ + map (\x -> exportValue e (SC.runIdentity (force x))) (Vector.toList xs) _ -> error $ "exportValue (on seq type " ++ show ty ++ ")" -- infinite streams TV.TVStream e -> case v of - SC.VExtra (SC.CStream trie) -> V.VStream (V.IndexSeqMap $ \i -> V.ready $ exportValue e (IntTrie.apply trie i)) + SC.VExtra (SC.CStream trie) -> pure $ V.VStream (V.indexSeqMap $ \i -> exportValue e (IntTrie.apply trie i)) _ -> error $ "exportValue (on seq type " ++ show ty ++ ")" -- tuples - TV.TVTuple etys -> V.VTuple (exportTupleValue etys v) + TV.TVTuple etys -> pure $ V.VTuple $ exportTupleValue etys v -- records TV.TVRec fields -> - V.VRecord (C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v) + pure . V.VRecord . C.recordFromFieldsWithDisplay (C.displayOrder fields) $ exportRecordValue (C.canonicalFields fields) v -- functions TV.TVFun _aty _bty -> - V.VFun mempty (error "exportValue: TODO functions") + pure $ V.VFun mempty (error "exportValue: TODO functions") -- abstract types TV.TVAbstract{} -> @@ -1709,8 +1716,8 @@ exportTupleValue :: [TV.TValue] -> SC.CValue -> [V.Eval V.Value] exportTupleValue tys v = case (tys, v) of ([] , SC.VUnit ) -> [] - ([t] , _ ) -> [V.ready $ exportValue t v] - (t : ts, SC.VPair x y) -> (V.ready $ exportValue t (run x)) : exportTupleValue ts (run y) + ([t] , _ ) -> [exportValue t v] + (t : ts, SC.VPair x y) -> (exportValue t (run x)) : exportTupleValue ts (run y) _ -> error $ "exportValue: expected tuple" where run = SC.runIdentity . force @@ -1719,12 +1726,11 @@ exportRecordValue :: [(C.Ident, TV.TValue)] -> SC.CValue -> [(C.Ident, V.Eval V. exportRecordValue fields v = case (fields, v) of ([] , SC.VUnit ) -> [] - ([(n, t)] , _ ) -> [(n, V.ready $ exportValue t v)] - ((n, t) : ts, SC.VPair x y) -> - (n, V.ready $ exportValue t (run x)) : exportRecordValue ts (run y) + ([(n, t)] , _ ) -> [(n, exportValue t v)] + ((n, t) : ts, SC.VPair x y) -> (n, exportValue t (run x)) : exportRecordValue ts (run y) (_, SC.VRecordValue (alistAllFields (map (C.identText . fst) fields) -> Just ths)) -> - zipWith (\(n,t) x -> (n, V.ready $ exportValue t (run x))) fields ths + zipWith (\(n,t) x -> (n, exportValue t (run x))) fields ths _ -> error $ "exportValue: expected record" where run = SC.runIdentity . force @@ -1733,20 +1739,23 @@ fvAsBool :: FirstOrderValue -> Bool fvAsBool (FOVBit b) = b fvAsBool _ = error "fvAsBool: expected FOVBit value" -exportFirstOrderValue :: FirstOrderValue -> V.Value +exportFirstOrderValue :: FirstOrderValue -> V.Eval V.Value exportFirstOrderValue fv = case fv of - FOVBit b -> V.VBit b - FOVInt i -> V.VInteger i - FOVIntMod _ i -> V.VInteger i - FOVWord w x -> V.word V.Concrete (toInteger w) x + FOVBit b -> pure (V.VBit b) + FOVInt i -> pure (V.VInteger i) + FOVIntMod _ i -> pure (V.VInteger i) + FOVWord w x -> V.word V.Concrete (toInteger w) x FOVVec t vs - | t == FOTBit -> V.VWord len (V.ready (V.LargeBitsVal len (V.finiteSeqMap . map (V.ready . V.VBit . fvAsBool) $ vs))) - | otherwise -> V.VSeq len (V.finiteSeqMap (map (V.ready . exportFirstOrderValue) vs)) + | t == FOTBit -> V.VWord len <$> (V.bitmapWordVal V.Concrete len + (V.finiteSeqMap V.Concrete . map (V.ready . fvAsBool) $ vs)) + | otherwise -> pure (V.VSeq len (V.finiteSeqMap V.Concrete (map exportFirstOrderValue vs))) where len = toInteger (length vs) FOVArray{} -> error $ "exportFirstOrderValue: unsupported FOT Array" - FOVTuple vs -> V.VTuple (map (V.ready . exportFirstOrderValue) vs) - FOVRec vm -> V.VRecord $ C.recordFromFields [ (C.mkIdent n, V.ready $ exportFirstOrderValue v) | (n, v) <- Map.assocs vm ] + FOVTuple vs -> pure $ V.VTuple $ map exportFirstOrderValue vs + FOVRec vm -> + do let vm' = fmap exportFirstOrderValue vm + pure $ V.VRecord $ C.recordFromFields [ (C.mkIdent n, v) | (n, v) <- Map.assocs vm' ] importFirstOrderValue :: FirstOrderType -> V.Value -> IO FirstOrderValue importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0) @@ -1755,7 +1764,7 @@ importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0) go t v = case (t,v) of (FOTBit , V.VBit b) -> return (FOVBit b) (FOTInt , V.VInteger i) -> return (FOVInt i) - (FOTVec _ FOTBit, V.VWord w wv) -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete =<< wv) + (FOTVec _ FOTBit, V.VWord w wv) -> FOVWord (fromIntegral w) . V.bvVal <$> (V.asWordVal V.Concrete wv) (FOTVec _ ty , V.VSeq len xs) -> FOVVec ty <$> traverse (go ty =<<) (V.enumerateSeqMap len xs) (FOTTuple tys , V.VTuple xs) -> FOVTuple <$> traverse (\(ty, x) -> go ty =<< x) (zip tys xs) (FOTRec fs , V.VRecord xs) -> diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index 5bde4dbd26..5f3e0b9e5f 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -153,7 +153,7 @@ nameMatcher xs = case modNameChunks (textToModName (pack xs)) of [] -> const False [x] -> (packIdent x ==) . MN.nameIdent - cs -> let m = MN.Declared (packModName (map pack (init cs))) MN.UserName + cs -> let m = MN.Declared (C.TopModule (packModName (map pack (init cs)))) MN.UserName i = packIdent (last cs) in \n -> MN.nameIdent n == i && MN.nameInfo n == m @@ -253,7 +253,7 @@ getNamingEnv env = eExtraNames env `MR.shadowing` nameEnv syms = case vis of OnlyPublic -> MI.ifPublic ifc PublicAndPrivate -> MI.ifPublic ifc `mappend` M.ifPrivate ifc - return $ MN.interpImport i syms + return $ MN.interpImportIface i syms getAllIfaceDecls :: ME.ModuleEnv -> M.IfaceDecls getAllIfaceDecls me = mconcat (map (both . ME.lmInterface) (ME.getLoadedModules (ME.meLoadedModules me))) @@ -364,13 +364,13 @@ loadCryptolModule sc env path = do newCryEnv <- C.importTopLevelDeclGroups sc oldCryEnv newDeclGroups newTermEnv <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv) - let names = MEx.eBinds (T.mExports m) -- :: Set T.Name + let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name let tm' = Map.filterWithKey (\k _ -> Set.member k names) $ Map.intersectionWith TypedTerm types newTermEnv let env' = env { eModuleEnv = modEnv'' , eTermEnv = newTermEnv } - let sm' = Map.filterWithKey (\k _ -> Set.member k (MEx.eTypes (T.mExports m))) (T.mTySyns m) + let sm' = Map.filterWithKey (\k _ -> Set.member k (MEx.exported C.NSType (T.mExports m))) (T.mTySyns m) return (CryptolModule sm' tm', env') bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv @@ -430,7 +430,7 @@ bindIdent ident env = (name, env') modEnv = eModuleEnv env supply = ME.meSupply modEnv fixity = Nothing - (name, supply') = MN.mkDeclared interactiveName MN.UserName ident fixity P.emptyRange supply + (name, supply') = MN.mkDeclared C.NSValue (C.TopModule interactiveName) MN.UserName ident fixity P.emptyRange supply modEnv' = modEnv { ME.meSupply = supply' } env' = env { eModuleEnv = modEnv' } @@ -467,17 +467,8 @@ bindInteger (ident, n) env = -------------------------------------------------------------------------------- --- FIXME: This definition was copied from a local declaration inside --- function 'defaultRW' in module 'Cryptol.REPL.Monad'. The cryptol --- package should probably export it so we don't have to copy it. meSolverConfig :: ME.ModuleEnv -> TM.SolverConfig -meSolverConfig env = - TM.SolverConfig - { TM.solverPath = "z3" - , TM.solverArgs = [ "-smt2", "-in" ] - , TM.solverVerbose = 0 - , TM.solverPreludePath = ME.meSearchPath env - } +meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env) resolveIdentifier :: (?fileReader :: FilePath -> IO ByteString) => @@ -496,7 +487,7 @@ resolveIdentifier env nm = SMT.withSolver (meSolverConfig modEnv) $ \s -> do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader modEnv (res, _ws) <- MM.runModuleM (minp s) $ - MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar pnm)) + MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar MR.NameUse pnm)) case res of Left _ -> pure Nothing Right (x,_) -> pure (Just x) @@ -557,18 +548,12 @@ parseDecls sc env input = do -- Convert from 'Decl' to 'TopDecl' so that types will be generalized let topdecls = [ P.Decl (P.TopLevel P.Public Nothing d) | d <- npdecls ] - -- Label each TopDecl with the "interactive" module for unique name generation - let (mdecls :: [MN.InModule (P.TopDecl P.PName)]) = map (MN.InModule interactiveName) topdecls - nameEnv1 <- MN.liftSupply (MN.namingEnv' mdecls) - -- Resolve names - let nameEnv = nameEnv1 `MR.shadowing` getNamingEnv env - (rdecls :: [P.TopDecl T.Name]) <- MM.interactive (MB.rename interactiveName nameEnv (traverse MR.rename topdecls)) + (_nenv, rdecls) <- MM.interactive (MB.rename interactiveName (getNamingEnv env) (MR.renameTopDecls interactiveName topdecls)) -- Create a Module to contain the declarations let rmodule = P.Module { P.mName = P.Located P.emptyRange interactiveName , P.mInstance = Nothing - , P.mImports = [] , P.mDecls = rdecls } @@ -636,7 +621,7 @@ declareName env mname input = do let modEnv = eModuleEnv env (cname, modEnv') <- liftModuleM modEnv $ MM.interactive $ - MN.liftSupply (MN.mkDeclared mname MN.UserName (P.getIdent pname) Nothing P.emptyRange) + MN.liftSupply (MN.mkDeclared C.NSValue (C.TopModule mname) MN.UserName (P.getIdent pname) Nothing P.emptyRange) let env' = env { eModuleEnv = modEnv' } return (cname, env') diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index 3e7f425a23..b2e6d02ba8 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -55,6 +55,7 @@ import Cryptol.Parser (ParseError,ppError) import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError) import Cryptol.Parser.NoPat (Error) import qualified Cryptol.TypeCheck.AST as T +import Cryptol.Utils.Ident (Namespace(..)) import Cryptol.Utils.PP #if !MIN_VERSION_base(4,8,0) @@ -297,13 +298,13 @@ getNewtypes = do getExprNames :: REPL [String] getExprNames = do fNames <- fmap getNamingEnv getCryptolEnv - return (map (show . pp) (Map.keys (MN.neExprs fNames))) + return (map (show . pp) (Map.keys (MN.namespaceMap NSValue fNames))) -- | Get visible type signature names. getTypeNames :: REPL [String] getTypeNames = do fNames <- fmap getNamingEnv getCryptolEnv - return (map (show . pp) (Map.keys (MN.neTypes fNames))) + return (map (show . pp) (Map.keys (MN.namespaceMap NSType fNames))) getPropertyNames :: REPL [String] getPropertyNames = diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs index 97de1ef35a..e61139b409 100644 --- a/src/SAWScript/AutoMatch/Cryptol.hs +++ b/src/SAWScript/AutoMatch/Cryptol.hs @@ -27,6 +27,9 @@ import qualified Cryptol.TypeCheck.AST as AST import qualified Cryptol.TypeCheck.Solver.SMT as SMT import Cryptol.Utils.PP +import Verifier.SAW.CryptolEnv( meSolverConfig ) + + -- | Parse a Cryptol module into a list of declarations -- Yields an Interaction so that we can talk to the user about what went wrong getDeclsCryptol :: FilePath -> IO (Interaction (Maybe [Decl])) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 4dc754678d..e6a9702cba 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -125,6 +125,8 @@ import qualified SAWScript.Prover.Exporter as Prover import qualified SAWScript.Prover.MRSolver as Prover import SAWScript.VerificationSummary +import Verifier.SAW.CryptolEnv( meSolverConfig ) + showPrim :: SV.Value -> TopLevel String showPrim v = do opts <- fmap rwPPOpts getTopLevelRW diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index d2b86f6ea9..e1b662ecd2 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -89,6 +89,7 @@ import SAWScript.Crucible.LLVM.Skeleton.Builtins import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CIR -- Cryptol +import Verifier.SAW.CryptolEnv (meSolverConfig) import qualified Cryptol.Eval as V (PPOpts(..)) import qualified Cryptol.Backend.Monad as V (runEval) import qualified Cryptol.Eval.Value as V (defaultPPOpts, ppValue) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 0c3e9f6068..eeed97aa45 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -340,7 +340,7 @@ evaluate sc t = evaluateTypedTerm :: SharedContext -> TypedTerm -> IO C.Value evaluateTypedTerm sc (TypedTerm schema trm) = - exportValueWithSchema schema <$> evaluate sc trm + C.runEval mempty . exportValueWithSchema schema =<< evaluate sc trm applyValue :: Value -> Value -> TopLevel Value applyValue (VLambda f) x = f x diff --git a/src/SAWScript/VerificationCheck.hs b/src/SAWScript/VerificationCheck.hs index 58fc679308..2bd4694259 100644 --- a/src/SAWScript/VerificationCheck.hs +++ b/src/SAWScript/VerificationCheck.hs @@ -61,8 +61,8 @@ vcCounterexample sc opts (EqualityCheck nm impNode specNode) evalFn = sv = exportValueWithSchema sschema sn opts' = SV.cryptolPPOpts opts -- Grr. Different pretty-printers. - lv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' lv) - sv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' sv) + lv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' =<< lv) + sv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' =<< sv) return $ vcat diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index c34f195981..1c53e145d8 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -135,7 +135,7 @@ import Cryptol.ModuleSystem.Name(Name) import Cryptol.ModuleSystem.Interface(ifTySyns) import Cryptol.TypeCheck.AST(TySyn(tsDef)) import Cryptol.TypeCheck.TypePat(aNat) -import Cryptol.Utils.PP(alwaysQualify,runDoc,pp) +import Cryptol.Utils.PP(render,pp) import Cryptol.Utils.Patterns(matchMaybe) import SAWScript.Crucible.Common (Sym, sawCoreState) @@ -1249,7 +1249,7 @@ lookupCry x mp = ) Right a -> Right a - where ppName = show . runDoc alwaysQualify . pp + where ppName = render . pp