From 06162031ecc1cc5d21eff62418480740c851f053 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 27 Jan 2021 19:15:59 -0800 Subject: [PATCH 1/3] Adapt to GaloisInc/cryptol#995 "Call stacks". --- cryptol-saw-core/css/Main.hs | 6 ++++-- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 20 ++++++++++++------- .../src/Verifier/SAW/CryptolEnv.hs | 6 ++++-- 3 files changed, 21 insertions(+), 11 deletions(-) diff --git a/cryptol-saw-core/css/Main.hs b/cryptol-saw-core/css/Main.hs index c63938b4..a3ff756a 100644 --- a/cryptol-saw-core/css/Main.hs +++ b/cryptol-saw-core/css/Main.hs @@ -89,7 +89,8 @@ cssMain css [inputModule,name] | cssMode css == NormalMode = do else (output css) modEnv <- CM.initialModuleEnv - (e,warn) <- CM.loadModuleByPath inputModule (defaultEvalOpts, BS.readFile, modEnv) + let minp = CM.ModuleInput True defaultEvalOpts BS.readFile modEnv + (e,warn) <- CM.loadModuleByPath inputModule minp mapM_ (print . pp) warn case e of Left msg -> print msg >> exitFailure @@ -127,7 +128,8 @@ extractCryptol sc modEnv input = do case P.parseExpr (pack input) of Left err -> fail (show (P.ppError err)) Right x -> return x - (exprResult, exprWarnings) <- CM.checkExpr pexpr (defaultEvalOpts, BS.readFile, modEnv) + let minp = CM.ModuleInput True defaultEvalOpts BS.readFile modEnv + (exprResult, exprWarnings) <- CM.checkExpr pexpr minp mapM_ (print . pp) exprWarnings ((_, expr, schema), _modEnv') <- case exprResult of diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index a899c11f..0c7f2ad2 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -914,6 +914,9 @@ importExpr sc env expr = do env' <- importDeclGroups sc env dgs importExpr sc env' e + C.ELocated _ e -> + importExpr sc env e + where the :: Maybe a -> IO a the = maybe (panic "importExpr" ["internal type error"]) return @@ -983,6 +986,9 @@ importExpr' sc env schema expr = do env' <- importDeclGroups sc env dgs importExpr' sc env' schema e + C.ELocated _ e -> + importExpr' sc env schema e + C.EList {} -> fallback C.ESel {} -> fallback C.ESet {} -> fallback @@ -1583,7 +1589,7 @@ scCryptolEq sc x y = -- Cryptol type schema. exportValueWithSchema :: C.Schema -> SC.CValue -> V.Value exportValueWithSchema (C.Forall [] [] ty) v = exportValue (evalValType mempty ty) v -exportValueWithSchema _ _ = V.VPoly (error "exportValueWithSchema") +exportValueWithSchema _ _ = V.VPoly mempty (error "exportValueWithSchema") -- TODO: proper support for polymorphic values exportValue :: TV.TValue -> SC.CValue -> V.Value @@ -1609,8 +1615,8 @@ exportValue ty v = case ty 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 V.Concrete . map (V.ready . V.VBit . SC.toBool . SC.runIdentity . force) $ Fold.toList xs))) - | otherwise -> V.VSeq (toInteger (Vector.length xs)) $ V.finiteSeqMap V.Concrete $ + (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 _ -> error $ "exportValue (on seq type " ++ show ty ++ ")" @@ -1629,7 +1635,7 @@ exportValue ty v = case ty of -- functions TV.TVFun _aty _bty -> - V.VFun (error "exportValue: TODO functions") + V.VFun mempty (error "exportValue: TODO functions") -- abstract types TV.TVAbstract{} -> @@ -1671,15 +1677,15 @@ exportFirstOrderValue fv = FOVIntMod _ i -> 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 V.Concrete . map (V.ready . V.VBit . fvAsBool) $ vs))) - | otherwise -> V.VSeq len (V.finiteSeqMap V.Concrete (map (V.ready . exportFirstOrderValue) 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)) 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 ] importFirstOrderValue :: FirstOrderType -> V.Value -> IO FirstOrderValue -importFirstOrderValue t0 v0 = V.runEval (go t0 v0) +importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0) where go :: FirstOrderType -> V.Value -> V.Eval FirstOrderValue go t v = case (t,v) of diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index a3e18cb8..cf45bace 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -479,7 +479,8 @@ resolveIdentifier env nm = nameEnv = getNamingEnv env doResolve pnm = - do (res, _ws) <- MM.runModuleM (defaultEvalOpts, ?fileReader, modEnv) $ + do let minp = MM.ModuleInput True defaultEvalOpts ?fileReader modEnv + (res, _ws) <- MM.runModuleM minp $ MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar pnm)) case res of Left _ -> pure Nothing @@ -641,7 +642,8 @@ liftModuleM :: (?fileReader :: FilePath -> IO ByteString) => ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv) liftModuleM env m = - MM.runModuleM (defaultEvalOpts, ?fileReader, env) m >>= moduleCmdResult + do let minp = MM.ModuleInput True defaultEvalOpts ?fileReader env + MM.runModuleM minp m >>= moduleCmdResult defaultEvalOpts :: E.EvalOpts defaultEvalOpts = E.EvalOpts quietLogger E.defaultPPOpts From de21a4533ddac4aeab822ef1af4e3d94c5f27f02 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 27 Jan 2021 19:37:40 -0800 Subject: [PATCH 2/3] Adapt to GaloisInc/cryptol#993 "Refactor evopts". --- cryptol-saw-core/css/Main.hs | 4 ++-- cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/cryptol-saw-core/css/Main.hs b/cryptol-saw-core/css/Main.hs index a3ff756a..aab74398 100644 --- a/cryptol-saw-core/css/Main.hs +++ b/cryptol-saw-core/css/Main.hs @@ -89,7 +89,7 @@ cssMain css [inputModule,name] | cssMode css == NormalMode = do else (output css) modEnv <- CM.initialModuleEnv - let minp = CM.ModuleInput True defaultEvalOpts BS.readFile modEnv + let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv (e,warn) <- CM.loadModuleByPath inputModule minp mapM_ (print . pp) warn case e of @@ -128,7 +128,7 @@ extractCryptol sc modEnv input = do case P.parseExpr (pack input) of Left err -> fail (show (P.ppError err)) Right x -> return x - let minp = CM.ModuleInput True defaultEvalOpts BS.readFile modEnv + let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv (exprResult, exprWarnings) <- CM.checkExpr pexpr minp mapM_ (print . pp) exprWarnings ((_, expr, schema), _modEnv') <- diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index cf45bace..85a01436 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -479,7 +479,7 @@ resolveIdentifier env nm = nameEnv = getNamingEnv env doResolve pnm = - do let minp = MM.ModuleInput True defaultEvalOpts ?fileReader modEnv + do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader modEnv (res, _ws) <- MM.runModuleM minp $ MM.interactive (MB.rename interactiveName nameEnv (MR.renameVar pnm)) case res of @@ -642,7 +642,7 @@ liftModuleM :: (?fileReader :: FilePath -> IO ByteString) => ME.ModuleEnv -> MM.ModuleM a -> IO (a, ME.ModuleEnv) liftModuleM env m = - do let minp = MM.ModuleInput True defaultEvalOpts ?fileReader env + do let minp = MM.ModuleInput True (pure defaultEvalOpts) ?fileReader env MM.runModuleM minp m >>= moduleCmdResult defaultEvalOpts :: E.EvalOpts From 38aeb96d63fb3eb9207bdcdb109e19dbad47ab91 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 27 Jan 2021 20:42:35 -0800 Subject: [PATCH 3/3] Adapt to GaloisInc/cryptol#1015 "Newtypes". --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 16 +++++++++++++--- cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs | 1 + 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 0c7f2ad2..78366b85 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -39,7 +39,7 @@ import qualified Cryptol.Eval.Value as V import qualified Cryptol.Eval.Concrete as V import Cryptol.Eval.Type (evalValType) import qualified Cryptol.TypeCheck.AST as C -import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, singleTParamSubst) +import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, listSubst, singleTParamSubst) import qualified Cryptol.ModuleSystem.Name as C (asPrim, nameUnique, nameIdent, nameInfo, NameInfo(..)) import qualified Cryptol.Utils.Ident as C @@ -231,6 +231,11 @@ importType sc env ty = C.TRec fm -> importType sc env (C.tTuple (map snd (C.canonicalFields fm))) + C.TNewtype nt ts -> + do let s = C.listSubst (zip (map C.TVBound (C.ntParams nt)) ts) + let t = plainSubst s (C.TRec (C.ntFields nt)) + go t + C.TCon tcon tyargs -> case tcon of C.TC tc -> @@ -250,7 +255,6 @@ importType sc env ty = b <- go (tyargs !! 1) scFun sc a b C.TCTuple _n -> scTupleType sc =<< traverse go tyargs - C.TCNewtype (C.UserTC _qn _k) -> unimplemented "TCNewtype" -- user-defined, @T@ C.TCAbstract{} -> panic "importType TODO: abstract type" [] C.PC pc -> case pc of @@ -1089,9 +1093,10 @@ plainSubst s ty = C.TUser f ts t -> C.TUser f (map (plainSubst s) ts) (plainSubst s t) C.TRec fs -> C.TRec (fmap (plainSubst s) fs) C.TVar x -> C.apSubst s (C.TVar x) + C.TNewtype nt ts -> C.TNewtype nt (fmap (plainSubst s) ts) --- | Generate a URI representing a cryptol name from a sequence of +-- | Generate a URI representing a cryptol name from a sequence of -- name parts representing the fully-qualified name. If a \"unique\" -- value is given, this represents a dynamically bound name in -- the \"\\" pseudo-module, and the unique value will @@ -1641,6 +1646,11 @@ exportValue ty v = case ty of TV.TVAbstract{} -> error "exportValue: TODO abstract types" + -- newtypes + TV.TVNewtype _ _ fields -> + exportValue (TV.TVRec fields) v + + exportTupleValue :: [TV.TValue] -> SC.CValue -> [V.Eval V.Value] exportTupleValue tys v = case (tys, v) of diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index 85a01436..5f02b0fc 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -632,6 +632,7 @@ typeNoUser t = T.TVar {} -> t T.TUser _ _ ty -> typeNoUser ty T.TRec fields -> T.TRec (fmap typeNoUser fields) + T.TNewtype nt ts -> T.TNewtype nt (fmap typeNoUser ts) schemaNoUser :: T.Schema -> T.Schema schemaNoUser (T.Forall params props ty) = T.Forall params props (typeNoUser ty)