From 107838c179e92d40ec438b44972bc2876cb4361d Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Fri, 26 Jan 2024 11:10:21 -0800 Subject: [PATCH] Make things build with the `sum-types` branch of `cryptol` Co-authored-by: Ryan Scott --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 111 +++++++++++------- .../src/Verifier/SAW/CryptolEnv.hs | 19 +-- deps/cryptol | 2 +- intTests/test_cryptol_enums/Test.cry | 3 + intTests/test_cryptol_enums/test.saw | 1 + intTests/test_cryptol_enums/test.sh | 3 + saw/SAWScript/REPL/Monad.hs | 8 +- src/SAWScript/Builtins.hs | 2 +- .../Crucible/JVM/ResolveSetupValue.hs | 9 +- src/SAWScript/Crucible/LLVM/FFI.hs | 4 +- .../Crucible/LLVM/ResolveSetupValue.hs | 9 +- .../Crucible/MIR/ResolveSetupValue.hs | 9 +- 12 files changed, 105 insertions(+), 75 deletions(-) create mode 100644 intTests/test_cryptol_enums/Test.cry create mode 100644 intTests/test_cryptol_enums/test.saw create mode 100755 intTests/test_cryptol_enums/test.sh diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 7a2a621bef..efe6dc0dee 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -35,11 +35,11 @@ module Verifier.SAW.Cryptol , importSchema , defaultPrimitiveOptions - , genNewtypeConstructors + , genNominalConstructors , exportValueWithSchema ) where -import Control.Monad (foldM, join, unless) +import Control.Monad (foldM, join, unless,forM) import Control.Exception (catch, SomeException) import Data.Bifunctor (first) import qualified Data.Foldable as Fold @@ -76,7 +76,7 @@ import qualified Cryptol.Utils.Ident as C , modNameChunksText ) import qualified Cryptol.Utils.RecordMap as C -import Cryptol.TypeCheck.Type as C (Newtype(..)) +import Cryptol.TypeCheck.Type as C (NominalType(..)) import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf) import Cryptol.Utils.PP (pretty) @@ -266,10 +266,17 @@ importType sc env ty = C.TRec fm -> importType sc env (C.tTuple (map snd (C.canonicalFields fm))) - C.TNewtype nt ts -> + C.TNominal 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 + let n = C.ntName nt + case ntDef nt of + C.Struct stru -> go (plainSubst s (C.TRec (C.ntFields stru))) + C.Enum {} -> error "importType: `enum` is not yet supported" + C.Abstract + | Just prim <- C.asPrim n + , Just t <- Map.lookup prim (envPrimTypes env) -> + scApplyAllBeta sc t =<< traverse go ts + | True -> panic ("importType: unknown primitive type: " ++ show n) [] C.TCon tcon tyargs -> case tcon of @@ -290,11 +297,6 @@ importType sc env ty = b <- go (tyargs !! 1) scFun sc a b C.TCTuple _n -> scTupleType sc =<< traverse go tyargs - C.TCAbstract (C.UserTC n _) - | Just prim <- C.asPrim n - , Just t <- Map.lookup prim (envPrimTypes env) -> - scApplyAllBeta sc t =<< traverse go tyargs - | True -> panic ("importType: unknown primitive type: " ++ show n) [] C.PC pc -> case pc of C.PLiteral -> -- we omit first argument to class Literal @@ -1008,8 +1010,13 @@ importExpr sc env expr = ("Expected filed " ++ show x ++ " in normal RecordSel") (elemIndex x (map fst (C.canonicalFields fm))) scTupleSelector sc e' (i+1) (length (C.canonicalFields fm)) - C.TNewtype nt _args -> - do let fs = C.ntFields nt + C.TNominal nt _args -> + do let fs = case C.ntDef nt of + C.Struct s -> C.ntFields s + C.Enum {} -> + panic "importExpr" ["Select from enum"] + C.Abstract -> + panic "importExpr" ["Select from abstract type"] i <- the ("Expected field " ++ show x ++ " in Newtype Record Sel") (elemIndex x (map fst (C.canonicalFields fs))) scTupleSelector sc e' (i+1) (length (C.canonicalFields fs)) @@ -1134,6 +1141,9 @@ importExpr sc env expr = -- generated if-then-else Fold.foldrM (propGuardToIte typ') err arms + C.ECase {} -> panic "importExpr" + ["`case` expressions are not yet supported"] + where the :: String -> Maybe a -> IO a the what = maybe (panic "importExpr" ["internal type error", what]) return @@ -1240,6 +1250,8 @@ importExpr' sc env schema expr = C.ELocated _ e -> importExpr' sc env schema e + C.ECase {} -> panic "importExpr" ["`case` is not yet supported"] + C.EList {} -> fallback C.ESel {} -> fallback C.ESet {} -> fallback @@ -1285,7 +1297,7 @@ 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) + C.TNominal nt ts -> C.TNominal nt (fmap (plainSubst s) ts) -- | Generate a URI representing a cryptol name from a sequence of @@ -1632,14 +1644,26 @@ proveEq sc env t1 t2 (C.tIsRec -> Just tm1, C.tIsRec -> Just tm2) | map fst (C.canonicalFields tm1) == map fst (C.canonicalFields tm2) -> proveEq sc env (C.tTuple (map snd (C.canonicalFields tm1))) (C.tTuple (map snd (C.canonicalFields tm2))) + + -- XXX: add a case for `enum` + -- 1. Match constructors by names, and prove fields as tuples + -- 2. We need some way to combine the proofs of equality of + -- the fields, into a proof for equality of the whole type + -- for sums + (_, _) -> panic "proveEq" ["Internal type error:", pretty t1, pretty t2] + -- | Resolve user types (type aliases and newtypes) to their simpler SAW-compatible forms. tNoUser :: C.Type -> C.Type tNoUser initialTy = case C.tNoUser initialTy of - C.TNewtype nt _ -> C.TRec $ C.ntFields nt + C.TNominal nt params + | C.Struct fs <- C.ntDef nt -> + if null params then C.TRec (C.ntFields fs) + else panic "tNoUser" ["Nominal type with parameters"] + -- XXX: We should instantiate, see #2019 t -> t @@ -1898,13 +1922,12 @@ exportValue ty v = case ty of TV.TVFun _aty _bty -> pure $ V.VFun mempty (error "exportValue: TODO functions") - -- abstract types - TV.TVAbstract{} -> - error "exportValue: TODO abstract types" - - -- newtypes - TV.TVNewtype _ _ fields -> - exportValue (TV.TVRec fields) v + -- nominal types + TV.TVNominal _ _ fields -> + case fields of + TV.TVStruct fs -> exportValue (TV.TVRec fs) v + TV.TVEnum {} -> error "exportValue: TODO enum" + TV.TVAbstract {} -> error "exportValue: TODO abstract types" exportTupleValue :: [TV.TValue] -> SC.CValue -> [V.Eval V.Value] @@ -1980,30 +2003,38 @@ importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0) _ -> panic "importFirstOrderValue" ["Expected finite value of type:", show t, "but got", show v] --- | Generate functions to construct newtypes in the term environment. --- (I.e., make identity functions that take the record the newtype wraps.) -genNewtypeConstructors :: SharedContext -> Map C.Name Newtype -> Env -> IO Env -genNewtypeConstructors sc newtypes env0 = - foldM genConstr env0 newtypes +-- | Generate functions to construct nominal values in the term environment. +-- For structs, make identity functions that take the record the newtype wraps. +-- Abstract types do not produce any functions. +genNominalConstructors :: SharedContext -> Map C.Name NominalType -> Env -> IO Env +genNominalConstructors sc nominal env0 = + foldM genConstr env0 nominal where - genConstr :: Env -> Newtype -> IO Env + genConstr :: Env -> NominalType -> IO Env genConstr env nt = do - constr <- importExpr sc env (newtypeConstr nt) - let env' = env { envE = Map.insert (ntConName nt) (constr, 0) (envE env) - , envC = Map.insert (ntConName nt) (newtypeSchema nt) (envC env) + let conTs = C.nominalTypeConTypes nt + constrs <- forM (nominalConstrs nt) $ \(x,e) -> + do e' <- importExpr sc env e + pure (x,(e',0)) + let env' = env { envE = foldr (uncurry Map.insert) (envE env) constrs + , envC = foldr (uncurry Map.insert) (envC env) conTs } return env' - newtypeConstr :: Newtype -> C.Expr - newtypeConstr nt = foldr tFn fn (C.ntParams nt) + + nominalConstrs :: NominalType -> [(C.Name,C.Expr)] + nominalConstrs nt = + case C.ntDef nt of + C.Struct fs -> + let recTy = C.TRec (C.ntFields fs) + fn = C.EAbs paramName recTy (C.EVar paramName) + con = C.ntConName fs + paramName = C.asLocal C.NSValue con + in [(con, foldr tFn fn (C.ntParams nt))] + C.Abstract -> [] + C.Enum {} -> error "genNominalConstrurctors: `enum` is not yet supported" where - paramName = C.asLocal C.NSValue (ntConName nt) - recTy = C.TRec $ ntFields nt - fn = C.EAbs paramName recTy (C.EVar paramName) -- EAbs Name Type Expr -- ETAbs TParam Expr tFn tp body = if elem (C.tpKind tp) [C.KType, C.KNum] then C.ETAbs tp body - else panic "genNewtypeConstructors" ["illegal newtype parameter kind", show (C.tpKind tp)] - newtypeSchema :: Newtype -> C.Schema - newtypeSchema nt = C.Forall (ntParams nt) (ntConstraints nt) - $ C.TRec (ntFields nt) `C.tFun` C.TRec (ntFields nt) + else panic "genNominalConstructors" ["illegal nominal type parameter kind", show (C.tpKind tp)] diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index d8011aac0f..4276711491 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -313,8 +313,9 @@ mkCryEnv env = -- noIfaceParams because we don't support translating functors yet infInp <- MB.genInferInput P.emptyRange prims NoParams ifaceDecls let newtypeCons = Map.fromList - [ (T.ntConName nt, T.newtypeConType nt) - | nt <- Map.elems (TM.inpNewtypes infInp) + [ con + | nt <- Map.elems (TM.inpNominalTypes infInp) + , con <- T.nominalTypeConTypes nt ] pure (newtypeCons `Map.union` TM.inpVars infInp) let types' = Map.union (eExtraTypes env) types @@ -415,11 +416,11 @@ loadCryptolModule sc primOpts env path = do $ ME.meLoadedModules modEnv'' let newDeclGroups = concatMap T.mDecls newModules - let newNewtypes = Map.difference (ME.loadedNewtypes modEnv') - (ME.loadedNewtypes modEnv) + let newNominal = Map.difference (ME.loadedNominalTypes modEnv') + (ME.loadedNominalTypes modEnv) newTermEnv <- - do cEnv <- C.genNewtypeConstructors sc newNewtypes oldCryEnv + do cEnv <- C.genNominalConstructors sc newNominal oldCryEnv newCryEnv <- C.importTopLevelDeclGroups sc primOpts cEnv newDeclGroups traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv) @@ -517,11 +518,11 @@ importModule sc env src as vis imps = do $ ME.lmLoadedModules $ ME.meLoadedModules modEnv' let newDeclGroups = concatMap T.mDecls newModules - let newNewtypes = Map.difference (ME.loadedNewtypes modEnv') - (ME.loadedNewtypes modEnv) + let newNominal = Map.difference (ME.loadedNominalTypes modEnv') + (ME.loadedNominalTypes modEnv) newTermEnv <- - do cEnv <- C.genNewtypeConstructors sc newNewtypes oldCryEnv + do cEnv <- C.genNominalConstructors sc newNominal oldCryEnv newCryEnv <- C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions cEnv newDeclGroups traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv) @@ -751,7 +752,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) + T.TNominal nt ts -> T.TNominal nt (fmap typeNoUser ts) schemaNoUser :: T.Schema -> T.Schema schemaNoUser (T.Forall params props ty) = T.Forall params props (typeNoUser ty) diff --git a/deps/cryptol b/deps/cryptol index d23add7b63..9be52cc23b 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit d23add7b639c1b91ee3e8fe7824fa58fedfb0370 +Subproject commit 9be52cc23b9d052ebdb7726954df179f259e9932 diff --git a/intTests/test_cryptol_enums/Test.cry b/intTests/test_cryptol_enums/Test.cry new file mode 100644 index 0000000000..6c34f5eb10 --- /dev/null +++ b/intTests/test_cryptol_enums/Test.cry @@ -0,0 +1,3 @@ +module Test where + +enum Foo a b = Bar a | Baz b diff --git a/intTests/test_cryptol_enums/test.saw b/intTests/test_cryptol_enums/test.saw new file mode 100644 index 0000000000..2e096c447b --- /dev/null +++ b/intTests/test_cryptol_enums/test.saw @@ -0,0 +1 @@ +import "Test.cry"; diff --git a/intTests/test_cryptol_enums/test.sh b/intTests/test_cryptol_enums/test.sh new file mode 100755 index 0000000000..adf8b97c7a --- /dev/null +++ b/intTests/test_cryptol_enums/test.sh @@ -0,0 +1,3 @@ +set -e + +! $SAW test.saw diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index e75aee760b..15fc84783f 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -35,7 +35,7 @@ module SAWScript.REPL.Monad ( -- ** Environment , getCryptolEnv, modifyCryptolEnv, setCryptolEnv , getModuleEnv, setModuleEnv - , getTSyns, getNewtypes, getVars + , getTSyns, getNominalTypes, getVars , getExprNames , getTypeNames , getPropertyNames @@ -397,11 +397,11 @@ getTSyns = do let decls = getAllIfaceDecls me return (M.ifTySyns decls) -getNewtypes :: REPL (Map.Map T.Name T.Newtype) -getNewtypes = do +getNominalTypes :: REPL (Map.Map T.Name T.NominalType) +getNominalTypes = do me <- getModuleEnv let decls = getAllIfaceDecls me - return (M.ifNewtypes decls) + return (M.ifNominalTypes decls) -- | Get visible variable names. getExprNames :: REPL [String] diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index eb3ed0d806..a3de996e63 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -1945,7 +1945,7 @@ defaultTypedTerm opts sc cfg tt@(TypedTerm (TypedTermSchema schema) trm) 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) + C.TNominal nt ts -> C.TNominal nt (fmap (plainSubst s) ts) defaultTypedTerm _opts _sc _cfg tt = return tt diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs index 98f38a0d14..20791627c2 100644 --- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs @@ -251,10 +251,8 @@ resolveSAWTerm cc tp tm = fail "resolveSAWTerm: unsupported record type" Cryptol.TVFun _ _ -> fail "resolveSAWTerm: unsupported function type" - Cryptol.TVAbstract _ _ -> - fail "resolveSAWTerm: unsupported abstract type" - Cryptol.TVNewtype{} -> - fail "resolveSAWTerm: unsupported newtype" + Cryptol.TVNominal {} -> + fail "resolveSAWTerm: unsupported nominal type" where sym = cc^.jccSym @@ -302,8 +300,7 @@ toJVMType tp = Cryptol.TVTuple _tps -> Nothing Cryptol.TVRec _flds -> Nothing Cryptol.TVFun _ _ -> Nothing - Cryptol.TVAbstract _ _ -> Nothing - Cryptol.TVNewtype{} -> Nothing + Cryptol.TVNominal {} -> Nothing equalValsPred :: JVMCrucibleContext -> diff --git a/src/SAWScript/Crucible/LLVM/FFI.hs b/src/SAWScript/Crucible/LLVM/FFI.hs index fff80c5186..e6950602a8 100644 --- a/src/SAWScript/Crucible/LLVM/FFI.hs +++ b/src/SAWScript/Crucible/LLVM/FFI.hs @@ -75,7 +75,7 @@ import Verifier.SAW.CryptolEnv import Verifier.SAW.OpenTerm import Verifier.SAW.Prelude import Verifier.SAW.Recognizer -import Verifier.SAW.SharedTerm +import Verifier.SAW.SharedTerm as Term import Verifier.SAW.TypedTerm -- | Commonly used things that need to be passed around. @@ -142,7 +142,7 @@ llvm_ffi_setup TypedTerm { ttTerm = appTerm } = do cryEnv <- lll $ rwCryptol <$> getMergedEnv case asConstant funTerm of Just (ec, funDef) - | Just FFIFunType {..} <- Map.lookup (ecName ec) (eFFITypes cryEnv) -> do + | Just FFIFunType {..} <- Map.lookup (Term.ecName ec) (eFFITypes cryEnv) -> do when (isNothing funDef) do throwFFISetup "Cannot verify foreign function with no Cryptol implementation" diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index b5fd1bdbf6..a2cf5d1325 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -868,10 +868,8 @@ resolveSAWTerm cc tp tm = fail "resolveSAWTerm: unimplemented record type (FIXME)" Cryptol.TVFun _ _ -> fail "resolveSAWTerm: invalid function type" - Cryptol.TVAbstract _ _ -> - fail "resolveSAWTerm: invalid abstract type" - Cryptol.TVNewtype{} -> - fail "resolveSAWTerm: invalid newtype" + Cryptol.TVNominal {} -> + fail "resolveSAWTerm: invalid nominal type" where sym = cc^.ccSym dl = Crucible.llvmDataLayout (ccTypeCtx cc) @@ -931,8 +929,7 @@ toLLVMType dl tp = return (Crucible.StructType si) Cryptol.TVRec _flds -> Left (NotYetSupported "record") Cryptol.TVFun _ _ -> Left (Impossible "function") - Cryptol.TVAbstract _ _ -> Left (Impossible "abstract") - Cryptol.TVNewtype{} -> Left (Impossible "newtype") + Cryptol.TVNominal {} -> Left (Impossible "nominal") toLLVMStorageType :: forall w . diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index 57ce46397d..3f569699ea 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -868,10 +868,8 @@ resolveSAWTerm mcc tp tm = fail "resolveSAWTerm: unsupported record type" Cryptol.TVFun _ _ -> fail "resolveSAWTerm: unsupported function type" - Cryptol.TVAbstract _ _ -> - fail "resolveSAWTerm: unsupported abstract type" - Cryptol.TVNewtype{} -> - fail "resolveSAWTerm: unsupported newtype" + Cryptol.TVNominal {} -> + fail "resolveSAWTerm: unsupported nominal type" where sym = mcc ^. mccSym col = mcc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection @@ -942,8 +940,7 @@ toMIRType tp = Right $ Mir.TyTuple tps' Cryptol.TVRec _flds -> Left (NotYetSupported "record") Cryptol.TVFun _ _ -> Left (Impossible "function") - Cryptol.TVAbstract _ _ -> Left (Impossible "abstract") - Cryptol.TVNewtype{} -> Left (Impossible "newtype") + Cryptol.TVNominal {} -> Left (Impossible "nominal") -- | Check if two MIR references are equal. equalRefsPred ::