Merge branch 'master' into saw-core-heapster-final-merge

README.md

@@ -1,4 +1,4 @@
-![Build Status](https://github.com/actions/GaloisInc/saw-script/workflows/.github/workflows/nightly.yml/badge.svg)
+[![Build Status](https://github.com/GaloisInc/saw-script/workflows/Nightly%20Builds/badge.svg)](https://github.com/GaloisInc/saw-script/actions?query=event%3Aschedule)
 
 # SAWScript
 

saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs

@@ -146,7 +146,7 @@ compMModule = mkModuleName ["CompM"]
 
 sawVectorDefinitionsModule :: TranslationConfiguration -> ModuleName
 sawVectorDefinitionsModule (TranslationConfiguration {..}) =
-  mkModuleName [vectorModule]
+  mkModuleName [Text.pack vectorModule]
 
 cryptolPrimitivesModule :: ModuleName
 cryptolPrimitivesModule = mkModuleName ["CryptolPrimitivesForSAWCore"]

saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

@@ -171,7 +171,7 @@ translateIdentWithArgs i args =
     UseRename targetModule targetName ->
       Coq.App (Coq.ExplVar $ identToCoq $
                mkIdent (fromMaybe (translateModuleName $ identModule i) targetModule)
-               targetName) <$>
+               (Text.pack targetName)) <$>
       mapM translateTerm args
     UseReplaceDropArgs n replacement
       | length args >= n -> Coq.App replacement <$> mapM translateTerm (drop n args)
@@ -186,9 +186,9 @@ translateIdent i = translateIdentWithArgs i []
 translateIdentToIdent :: TermTranslationMonad m => Ident -> m (Maybe Ident)
 translateIdentToIdent i =
   (atUseSite <$> findSpecialTreatment i) >>= \case
-    UsePreserve -> return $ Just (mkIdent translatedModuleName (identName i))
+    UsePreserve -> return $ Just (mkIdent translatedModuleName (identBaseName i))
     UseRename   targetModule targetName ->
-      return $ Just $ mkIdent (fromMaybe translatedModuleName targetModule) targetName
+      return $ Just $ mkIdent (fromMaybe translatedModuleName targetModule) (Text.pack targetName)
     UseReplaceDropArgs _ _ -> return Nothing
   where
     translatedModuleName = translateModuleName (identModule i)

saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs

@@ -13,6 +13,7 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE RankNTypes #-}

saw-core/src/Verifier/SAW/Grammar.y

@@ -337,8 +337,8 @@ mkTupleProj t _ =
      return (badTerm (pos t))
 
 -- | Parse a term as a dotted list of strings
-parseModuleName :: Term -> Maybe [String]
-parseModuleName (RecordProj t str) = (++ [Text.unpack str]) <$> parseModuleName t
+parseModuleName :: Term -> Maybe [Text]
+parseModuleName (RecordProj t fname) = (++ [fname]) <$> parseModuleName t
 parseModuleName _ = Nothing
 
 -- | Parse a qualified recursor @M1.M2...Mn.d#rec@
@@ -359,7 +359,7 @@ parseTupleSelector t i =
 -- module name given first.
 mkPosModuleName :: [PosPair Text] -> PosPair ModuleName
 mkPosModuleName [] = error "internal: Unexpected empty module name"
-mkPosModuleName l = PosPair p (mkModuleName (fmap Text.unpack nms))
+mkPosModuleName l = PosPair p (mkModuleName nms)
   where nms = fmap val l
         p = pos (last l)
 }

saw-core/src/Verifier/SAW/Name.hs

@@ -25,7 +25,6 @@ module Verifier.SAW.Name
   , moduleNamePieces
    -- * Identifiers
   , Ident(identModule, identBaseName), identName, mkIdent
-  , mkIdentText
   , parseIdent
   , isIdent
   , identText
@@ -53,7 +52,6 @@ module Verifier.SAW.Name
 import           Control.Exception (assert)
 import           Data.Char
 import           Data.Hashable
-import qualified Data.List as L
 import           Data.List.NonEmpty (NonEmpty(..))
 import           Data.Map (Map)
 import qualified Data.Map as Map
@@ -91,10 +89,10 @@ moduleNamePieces (ModuleName x) = Text.splitOn (Text.pack ".") x
 
 -- | Create a module name given a list of strings with the top-most
 -- module name given first.
-mkModuleName :: [String] -> ModuleName
+mkModuleName :: [Text] -> ModuleName
 mkModuleName [] = error "internal: mkModuleName given empty module name"
-mkModuleName nms = assert (all isCtor nms) $ ModuleName (Text.pack s)
-  where s = L.intercalate "." (reverse nms)
+mkModuleName nms = assert (all (isCtor . Text.unpack) nms) $ ModuleName s
+  where s = Text.intercalate "." (reverse nms)
 
 preludeName :: ModuleName
 preludeName = mkModuleName ["Prelude"]
@@ -131,11 +129,8 @@ instance Read Ident where
     let (str1, str2) = break (not . isIdChar) str in
     [(parseIdent str1, str2)]
 
-mkIdent :: ModuleName -> String -> Ident
-mkIdent m s = Ident m (Text.pack s)
-
-mkIdentText :: ModuleName -> Text -> Ident
-mkIdentText m s = Ident m s
+mkIdent :: ModuleName -> Text -> Ident
+mkIdent m s = Ident m s
 
 -- | Parse a fully qualified identifier.
 parseIdent :: String -> Ident
@@ -146,9 +141,8 @@ parseIdent s0 =
       _ -> internalError $ "parseIdent given bad identifier " ++ show s0
   where breakEach s =
           case break (=='.') s of
-            (h,[]) -> [h]
-            (h,'.':r) -> h : breakEach r
-            _ -> internalError "parseIdent.breakEach failed"
+            (h, []) -> [Text.pack h]
+            (h, _ : r) -> Text.pack h : breakEach r
 
 instance IsString Ident where
   fromString = parseIdent

saw-core/src/Verifier/SAW/ParserUtils.hs

@@ -143,7 +143,7 @@ declareTypedNameFun sc_fun mnm nm apply_p tp =
   let th_nm = (if apply_p then "scApply" else "sc") ++ show mnm ++ "_" ++ Text.unpack nm in
   declareTermApplyFun th_nm (length $ fst $ Un.asPiList tp) $ \sc ts ->
   [| $(sc_fun) $(varE sc)
-   (mkIdent mnm $(stringE (Text.unpack nm)))
+   (mkIdent mnm (Text.pack $(stringE (Text.unpack nm))))
    $(ts) |]
 
 -- | Declare a Haskell function

saw-core/src/Verifier/SAW/Prelude/Constants.hs

@@ -7,6 +7,8 @@ Stability   : experimental
 Portability : non-portable (language extensions)
 -}
 
+{-# LANGUAGE OverloadedStrings #-}
+
 module Verifier.SAW.Prelude.Constants where
 
 import Verifier.SAW.Term.Functor

saw-core/src/Verifier/SAW/SCTypeCheck.hs

@@ -145,7 +145,7 @@ instance LiftTCM b => LiftTCM (a -> b) where
 -- | Errors that can occur during type-checking
 data TCError
   = NotSort Term
-  | NotFuncType Term
+  | NotFuncTypeInApp TypedTerm TypedTerm
   | NotTupleType Term
   | BadTupleIndex Int Term
   | NotStringLit Term
@@ -185,9 +185,14 @@ prettyTCError e = runReader (helper e) ([], Nothing) where
 
   helper :: TCError -> PPErrM [String]
   helper (NotSort ty) = ppWithPos [ return "Not a sort" , ishow ty ]
-  helper (NotFuncType ty) =
-      ppWithPos [ return "Function application with non-function type" ,
-                  ishow ty ]
+  helper (NotFuncTypeInApp f arg) =
+      ppWithPos [ return "Function application with non-function type"
+                , return "For term:"
+                , ishow (typedVal f)
+                , return "With type:"
+                , ishow (typedType f)
+                , return "To argument:"
+                , ishow (typedVal arg) ]
   helper (NotTupleType ty) =
       ppWithPos [ return "Tuple field projection with non-tuple type" ,
                   ishow ty ]
@@ -390,7 +395,8 @@ instance TypeInfer (FlatTermF Term) where
 -- its (most general) type.
 instance TypeInfer (TermF TypedTerm) where
   typeInfer (FTermF ftf) = typeInfer ftf
-  typeInfer (App (TypedTerm _ x_tp) y) = applyPiTyped x_tp y
+  typeInfer (App x@(TypedTerm _ x_tp) y) =
+    applyPiTyped (NotFuncTypeInApp x y) x_tp y
   typeInfer (Lambda x (TypedTerm a a_tp) (TypedTerm _ b)) =
     void (ensureSort a_tp) >> liftTCM scTermF (Pi x a b)
   typeInfer (Pi _ (TypedTerm _ a_tp) (TypedTerm _ b_tp)) =
@@ -451,14 +457,16 @@ instance TypeInfer (FlatTermF TypedTerm) where
        dt <- case maybe_dt of
          Just dt -> return dt
          Nothing -> throwTCError $ NoSuchDataType d
+       let err =
+             BadParamsOrArgsLength True d
+             (map typedVal params) (map typedVal args)
        if length params == length (dtParams dt) &&
           length args == length (dtIndices dt) then return () else
-         throwTCError $
-         BadParamsOrArgsLength True d (map typedVal params) (map typedVal args)
+         throwTCError err
        -- NOTE: we assume dtType is already well-typed and in WHNF
        -- _ <- inferSort t
        -- t' <- typeCheckWHNF t
-       foldM applyPiTyped (dtType dt) (params ++ args)
+       foldM (applyPiTyped err) (dtType dt) (params ++ args)
 
   typeInfer (CtorApp c params args) =
     -- Look up the Ctor structure, check the length of the params and args, and
@@ -467,14 +475,16 @@ instance TypeInfer (FlatTermF TypedTerm) where
        ctor <- case maybe_ctor of
          Just ctor -> return ctor
          Nothing -> throwTCError $ NoSuchCtor c
+       let err =
+             BadParamsOrArgsLength False c
+             (map typedVal params) (map typedVal args)
        if length params == ctorNumParams ctor &&
           length args == ctorNumArgs ctor then return () else
-         throwTCError $
-         BadParamsOrArgsLength False c (map typedVal params) (map typedVal args)
+         throwTCError err
        -- NOTE: we assume ctorType is already well-typed and in WHNF
        -- _ <- inferSort t
        -- t' <- typeCheckWHNF t
-       foldM applyPiTyped (ctorType ctor) (params ++ args)
+       foldM (applyPiTyped err) (ctorType ctor) (params ++ args)
 
   typeInfer (RecursorApp d params p_ret cs_fs ixs arg) =
     inferRecursorApp d params p_ret cs_fs ixs arg
@@ -509,16 +519,17 @@ instance TypeInfer (FlatTermF TypedTerm) where
 
 -- | Check that @fun_tp=Pi x a b@ and that @arg@ has type @a@, and return the
 -- result of substituting @arg@ for @x@ in the result type @b@, i.e.,
--- @[arg/x]b@. This substitution could create redexes, so we call the evaluator.
-applyPiTyped :: Term -> TypedTerm -> TCM Term
-applyPiTyped fun_tp arg =
+-- @[arg/x]b@. This substitution could create redexes, so we call the
+-- evaluator. If @fun_tp@ is not a pi type, raise the supplied error.
+applyPiTyped :: TCError -> Term -> TypedTerm -> TCM Term
+applyPiTyped err fun_tp arg =
   case asPi fun_tp of
     Just (_, arg_tp, ret_tp) -> do
       -- _ <- ensureSort aty -- NOTE: we assume tx is well-formed and WHNF
       -- aty' <- scTypeCheckWHNF aty
       checkSubtype arg arg_tp
       liftTCM instantiateVar 0 (typedVal arg) ret_tp >>= typeCheckWHNF
-    _ -> throwTCError (NotFuncType fun_tp)
+    _ -> throwTCError err
 
 -- | Ensure that a 'Term' is a sort, and return that sort
 ensureSort :: Term -> TCM Sort
@@ -577,7 +588,12 @@ inferRecursorApp d params p_ret cs_fs ixs arg =
      if length params == length (dtParams dt) &&
         length ixs == length (dtIndices dt) then return () else
        throwTCError $ mk_err "Incorrect number of params or indices"
-     _ <- foldM applyPiTyped (dtType dt) (params ++ ixs)
+     _ <-
+       -- applyPiTyped cannot fail, because we have already checked the number
+       -- of params and indices
+       foldM (applyPiTyped
+              (error "Internal type-checking error: unexpected non-pi type!"))
+       (dtType dt) (params ++ ixs)
 
      -- Get the type of p_ret and make sure that it is of the form
      --

saw-core/src/Verifier/SAW/Typechecker.hs

@@ -43,7 +43,6 @@ import Prettyprinter hiding (Doc)
 import Verifier.SAW.Utils (internalError)
 
 import Verifier.SAW.Module
-import Verifier.SAW.Name (mkIdentText)
 import Verifier.SAW.Position
 import Verifier.SAW.Term.Functor
 import Verifier.SAW.Term.CtxTerm
@@ -178,7 +177,7 @@ typeInferCompleteTerm (matchAppliedRecursor -> Just (maybe_mnm, str, args)) =
          Just mnm -> return mnm
          Nothing -> getModuleName
      m <- liftTCM scFindModule mnm
-     let dt_ident = mkIdentText mnm str
+     let dt_ident = mkIdent mnm str
      dt <- case findDataType m str of
        Just d -> return d
        Nothing -> throwTCError $ NoSuchDataType dt_ident
@@ -330,7 +329,7 @@ processDecls (Un.TypeDecl NoQualifier (PosPair p nm) tp :
 
      -- Step 4: add the definition to the current module
      mnm <- getModuleName
-     let ident = mkIdentText mnm nm
+     let ident = mkIdent mnm nm
      t <- liftTCM scConstant' (ModuleIdentifier ident) def_tm def_tp
      liftTCM scRegisterGlobal ident t
      liftTCM scModifyModule mnm $ \m ->
@@ -350,7 +349,7 @@ processDecls (Un.TypeDecl q (PosPair p nm) tp : rest) =
    do typed_tp <- typeInferComplete tp
       void $ ensureSort $ typedType typed_tp
       mnm <- getModuleName
-      let ident = mkIdentText mnm nm
+      let ident = mkIdent mnm nm
       let nmi = ModuleIdentifier ident
       i <- liftTCM scFreshGlobalVar
       liftTCM scRegisterName i nmi
@@ -406,7 +405,7 @@ processDecls (Un.DataDecl (PosPair p nm) param_ctx dt_tp c_decls : rest) =
 
   -- Step 4: Add d as an empty datatype, so we can typecheck the constructors
   mnm <- getModuleName
-  let dtName = mkIdentText mnm nm
+  let dtName = mkIdent mnm nm
   let dt = DataType { dtCtors = [], .. }
   liftTCM scModifyModule mnm (\m -> beginDataType m dt)
 
@@ -432,8 +431,8 @@ processDecls (Un.DataDecl (PosPair p nm) param_ctx dt_tp c_decls : rest) =
             let tp = typedVal typed_tp in
             case mkCtorArgStruct dtName p_ctx ix_ctx tp of
               Just arg_struct ->
-                liftTCM scBuildCtor dtName (mkIdentText mnm c)
-                (map (mkIdentText mnm . fst) typed_ctors)
+                liftTCM scBuildCtor dtName (mkIdent mnm c)
+                (map (mkIdent mnm . fst) typed_ctors)
                 arg_struct
               Nothing -> err ("Malformed type form constructor: " ++ show c)
 

saw-remote-api/src/SAWServer/Term.hs

@@ -16,11 +16,11 @@ instance FromJSON JSONModuleName where
     where
       literal =
         withText "module name as string" $
-        pure . JSONModuleName . mkModuleName . map T.unpack . T.splitOn "."
+        pure . JSONModuleName . mkModuleName . T.splitOn "."
       structured =
         withArray "module name as list of parts" $ \v ->
         do parts <- traverse parseJSON (V.toList v)
-           pure $ JSONModuleName $ mkModuleName $ map T.unpack parts
+           pure $ JSONModuleName $ mkModuleName parts
 
 instance ToJSON JSONModuleName where
   toJSON (JSONModuleName n) = toJSON (show n)

src/SAWScript/Builtins.hs

@@ -39,10 +39,11 @@ import Data.List (isPrefixOf, isInfixOf)
 import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
+import Data.Text (Text)
+import qualified Data.Text as Text
 import Data.Time.Clock
 import Data.Typeable
 
-import qualified Data.Text as Text
 import System.Directory
 import qualified System.Environment
 import qualified System.Exit as Exit
@@ -884,23 +885,21 @@ cryptolSimpset =
   do sc <- getSharedContext
      io $ Cryptol.mkCryptolSimpset sc
 
-addPreludeEqs :: [String] -> Simpset
-              -> TopLevel Simpset
+addPreludeEqs :: [Text] -> Simpset -> TopLevel Simpset
 addPreludeEqs names ss = do
   sc <- getSharedContext
   eqRules <- io $ mapM (scEqRewriteRule sc) (map qualify names)
   return (addRules eqRules ss)
     where qualify = mkIdent (mkModuleName ["Prelude"])
 
-addCryptolEqs :: [String] -> Simpset
-              -> TopLevel Simpset
+addCryptolEqs :: [Text] -> Simpset -> TopLevel Simpset
 addCryptolEqs names ss = do
   sc <- getSharedContext
   eqRules <- io $ mapM (scEqRewriteRule sc) (map qualify names)
   return (addRules eqRules ss)
     where qualify = mkIdent (mkModuleName ["Cryptol"])
 
-add_core_defs :: String -> [String] -> Simpset -> TopLevel Simpset
+add_core_defs :: Text -> [Text] -> Simpset -> TopLevel Simpset
 add_core_defs modname names ss =
   do sc <- getSharedContext
      defs <- io $ mapM (getDef sc) names -- FIXME: warn if not found
@@ -912,12 +911,12 @@ add_core_defs modname names ss =
       scFindDef sc (qualify n) >>= \maybe_def ->
       case maybe_def of
         Just d -> return d
-        Nothing -> fail $ modname ++ " definition " ++ n ++ " not found"
+        Nothing -> fail $ Text.unpack $ modname <> " definition " <> n <> " not found"
 
-add_prelude_defs :: [String] -> Simpset -> TopLevel Simpset
+add_prelude_defs :: [Text] -> Simpset -> TopLevel Simpset
 add_prelude_defs = add_core_defs "Prelude"
 
-add_cryptol_defs :: [String] -> Simpset -> TopLevel Simpset
+add_cryptol_defs :: [Text] -> Simpset -> TopLevel Simpset
 add_cryptol_defs = add_core_defs "Cryptol"
 
 rewritePrim :: Simpset -> TypedTerm -> TopLevel TypedTerm