diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs index e166d024ae..0480ba4ac9 100644 --- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs +++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs @@ -10,6 +10,7 @@ module Verifier.SAW.TypedTerm where import Control.Monad (foldM) import Data.Map (Map) import qualified Data.Map as Map +import Data.Text (Text) import Cryptol.ModuleSystem.Name (nameIdent) import qualified Cryptol.TypeCheck.AST as C @@ -62,7 +63,7 @@ applyTypedTerms :: SharedContext -> TypedTerm -> [TypedTerm] -> IO TypedTerm applyTypedTerms sc = foldM (applyTypedTerm sc) -- | Create an abstract defined constant with the specified name and body. -defineTypedTerm :: SharedContext -> String -> TypedTerm -> IO TypedTerm +defineTypedTerm :: SharedContext -> Text -> TypedTerm -> IO TypedTerm defineTypedTerm sc name (TypedTerm schema t) = do ty <- scTypeOf sc t TypedTerm schema <$> scConstant sc name t ty diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs index 90c517d667..28c366cadf 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs @@ -49,6 +49,7 @@ import Data.Ratio import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.Word(Word64) +import Data.Text (Text) import qualified Data.Text as Text import What4.BaseTypes @@ -148,7 +149,7 @@ baseSCType sym sc bt = -- | Create a new symbolic variable. sawCreateVar :: SAWCoreState n - -> String -- ^ the name of the variable + -> Text -- ^ the name of the variable -> SC.Term -> IO SC.Term sawCreateVar st nm tp = do @@ -539,7 +540,7 @@ evaluateExpr sym st sc cache = f [] B.UninterpVarKind -> do tp <- baseSCType sym sc (B.bvarType bv) SAWExpr <$> sawCreateVar st nm tp - where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv + where nm = solverSymbolAsText $ B.bvarName bv B.LatchVarKind -> unsupported sym "SAW backend does not support latch variables" B.QuantifierVarKind -> do diff --git a/saw-core/src/Verifier/SAW/Constant.hs b/saw-core/src/Verifier/SAW/Constant.hs index 8b124445bc..2b064868f3 100644 --- a/saw-core/src/Verifier/SAW/Constant.hs +++ b/saw-core/src/Verifier/SAW/Constant.hs @@ -8,11 +8,14 @@ Portability : non-portable (language extensions) -} module Verifier.SAW.Constant (scConst) where + +import Data.Text (Text) + import Verifier.SAW.SharedTerm import Verifier.SAW.Rewriter import Verifier.SAW.Conversion -scConst :: SharedContext -> String -> Term -> IO Term +scConst :: SharedContext -> Text -> Term -> IO Term scConst sc name t = do ty <- scTypeOf sc t ty' <- rewriteSharedTerm sc (addConvs natConversions emptySimpset) ty diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index 18d18a4fcf..6db48c95b0 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/saw-core/src/Verifier/SAW/Rewriter.hs @@ -68,7 +68,6 @@ import qualified Data.List as List import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set -import qualified Data.Text as Text import Control.Monad.Trans.Writer.Strict import Numeric.Natural @@ -222,7 +221,7 @@ scMatch sc pat term = let fvy = looseVars y `intersectBitSets` (completeBitSet depth) guard (fvy `unionBitSets` fvj == fvj) let fixVar t (nm, ty) = - do v <- scFreshGlobal sc (Text.unpack nm) ty + do v <- scFreshGlobal sc nm ty let Just ec = R.asExtCns v t' <- instantiateVar sc 0 v t return (t', ec) @@ -882,7 +881,7 @@ doHoistIfs sc ss hoistCache itePat = go goF _ (Pi nm tp body) = goBinder scPi nm tp body goBinder close nm tp body = do - (ec, body') <- scOpenTerm sc (Text.unpack nm) tp 0 body + (ec, body') <- scOpenTerm sc nm tp 0 body (body'', conds) <- go body' let (stuck, float) = List.partition (\(_,ecs) -> Set.member ec ecs) conds diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index 1680dc138e..165f7e4fb3 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -392,17 +392,16 @@ scShowTerm sc opts t = pure (showTermWithNames opts env t) -- | Create a global variable with the given identifier (which may be "_") and type. -scFreshEC :: SharedContext -> String -> a -> IO (ExtCns a) -scFreshEC sc x tp = do - i <- scFreshGlobalVar sc - let x' = Text.pack x - let uri = scFreshNameURI x' i - let nmi = ImportedName uri [x',Text.pack (x <> "#" <> show i)] - scRegisterName sc i nmi - pure (EC i nmi tp) +scFreshEC :: SharedContext -> Text -> a -> IO (ExtCns a) +scFreshEC sc x tp = + do i <- scFreshGlobalVar sc + let uri = scFreshNameURI x i + let nmi = ImportedName uri [x, x <> "#" <> Text.pack (show i)] + scRegisterName sc i nmi + pure (EC i nmi tp) -- | Create a global variable with the given identifier (which may be "_") and type. -scFreshGlobal :: SharedContext -> String -> Term -> IO Term +scFreshGlobal :: SharedContext -> Text -> Term -> IO Term scFreshGlobal sc x tp = scExtCns sc =<< scFreshEC sc x tp -- | Returns shared term associated with ident. @@ -1213,7 +1212,7 @@ scSort sc s = scFlatTermF sc (Sort s) scNat :: SharedContext -> Natural -> IO Term scNat sc n = scFlatTermF sc (NatLit n) --- | Create a literal term (of saw-core type @String@) from a 'String'. +-- | Create a literal term (of saw-core type @String@) from a 'Text'. scString :: SharedContext -> Text -> IO Term scString sc s = scFlatTermF sc (StringLit s) @@ -1324,7 +1323,7 @@ scFunAll :: SharedContext -> IO Term scFunAll sc argTypes resultType = foldrM (scFun sc) resultType argTypes --- | Create a lambda term from a parameter name (as a 'String'), parameter type +-- | Create a lambda term from a parameter name (as a 'LocalName'), parameter type -- (as a 'Term'), and a body. Regarding deBruijn indices, in the body of the -- function, an index of 0 refers to the bound parameter. scLambda :: SharedContext @@ -1378,7 +1377,7 @@ scLocalVar sc i = scTermF sc (LocalVar i) -- indices. If the body contains any ExtCns variables, they will be -- abstracted over and reapplied to the resulting constant. scConstant :: SharedContext - -> String -- ^ The name + -> Text -- ^ The name -> Term -- ^ The body -> Term -- ^ The type -> IO Term @@ -2337,7 +2336,7 @@ scTreeSize = fst . go (0, Map.empty) -- | `openTerm sc nm ty i body` replaces the loose deBruijn variable `i` -- with a fresh external constant (with name `nm`, and type `ty`) in `body`. scOpenTerm :: SharedContext - -> String + -> Text -> Term -> DeBruijnIndex -> Term diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index e300be4e36..99b9a9bab9 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -26,7 +26,6 @@ import Data.Foldable ( traverse_ ) import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe ( maybeToList ) -import qualified Data.Text as T import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) @@ -120,7 +119,7 @@ interpretJVMSetup fileReader bic cenv0 ss = evalStateT (traverse_ go ss) (mempty go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= jvm_return -- TODO: do we really want two names here? go (SetupFresh name@(ServerName n) debugName ty) = - do t <- lift $ jvm_fresh_var (T.unpack debugName) ty + do t <- lift $ jvm_fresh_var debugName ty (env, cenv) <- get put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv) save name (Val (MS.SetupTerm t)) diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs index 8f38d952f8..ee2cbf0d18 100644 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -25,7 +25,6 @@ import Data.Aeson (FromJSON(..), withObject, (.:)) import Data.ByteString (ByteString) import Data.Map (Map) import qualified Data.Map as Map -import qualified Data.Text as T import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) @@ -102,7 +101,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c = Nothing -> return () where setupFresh (ContractVar n dn ty) = - do t <- llvm_fresh_var (T.unpack dn) (llvmType ty) + do t <- llvm_fresh_var dn (llvmType ty) return (n, t) setupState allocs (env, cenv) vars = diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index baf2f26fde..9a38fd73fe 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -130,7 +130,7 @@ showPrim v = do opts <- fmap rwPPOpts getTopLevelRW return (SV.showsPrecValue opts 0 v "") -definePrim :: String -> TypedTerm -> TopLevel TypedTerm +definePrim :: Text -> TypedTerm -> TopLevel TypedTerm definePrim name (TypedTerm schema rhs) = do sc <- getSharedContext ty <- io $ Cryptol.importSchema sc Cryptol.emptyEnv schema @@ -526,7 +526,7 @@ goal_assume = do sc <- SV.scriptTopLevel getSharedContext execTactic (tacticAssume sc) -goal_intro :: String -> ProofScript TypedTerm +goal_intro :: Text -> ProofScript TypedTerm goal_intro s = do sc <- SV.scriptTopLevel getSharedContext execTactic (tacticIntro sc s) @@ -986,7 +986,7 @@ check_goal = fixPos :: Pos fixPos = PosInternal "FIXME" -freshSymbolicPrim :: String -> C.Schema -> TopLevel TypedTerm +freshSymbolicPrim :: Text -> C.Schema -> TopLevel TypedTerm freshSymbolicPrim x schema@(C.Forall [] [] ct) = do sc <- getSharedContext cty <- io $ Cryptol.importType sc Cryptol.emptyEnv ct diff --git a/src/SAWScript/Crucible/Common/Setup/Type.hs b/src/SAWScript/Crucible/Common/Setup/Type.hs index 8d61570a21..055ec60bd3 100644 --- a/src/SAWScript/Crucible/Common/Setup/Type.hs +++ b/src/SAWScript/Crucible/Common/Setup/Type.hs @@ -35,6 +35,7 @@ module SAWScript.Crucible.Common.Setup.Type import Control.Lens import Control.Monad.State (StateT) import Control.Monad.IO.Class (MonadIO(liftIO)) +import Data.Text (Text) import qualified Cryptol.TypeCheck.Type as Cryptol (Type) import qualified Verifier.SAW.Cryptol as Cryptol (importType, emptyEnv) @@ -101,7 +102,7 @@ addCondition cond = currentState . MS.csConditions %= (cond : ) freshTypedExtCns :: MonadIO m => SharedContext {- ^ shared context -} -> - String {- ^ variable name -} -> + Text {- ^ variable name -} -> Cryptol.Type {- ^ variable type -} -> CrucibleSetupT arch m TypedExtCns freshTypedExtCns sc name cty = @@ -116,7 +117,7 @@ freshTypedExtCns sc name cty = freshVariable :: MonadIO m => SharedContext {- ^ shared context -} -> - String {- ^ variable name -} -> + Text {- ^ variable name -} -> Cryptol.Type {- ^ variable type -} -> CrucibleSetupT arch m TypedTerm freshVariable sc name cty = diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index 3dbff7ee9e..424e820019 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -55,6 +55,7 @@ import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set import qualified Data.Sequence as Seq +import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Vector as V import Data.Void (absurd) @@ -955,7 +956,7 @@ typeOfJavaType jty = -- | Generate a fresh variable term. The name will be used when -- pretty-printing the variable in debug output. jvm_fresh_var :: - String {- ^ variable name -} -> + Text {- ^ variable name -} -> JavaType {- ^ variable type -} -> JVMSetupM TypedTerm {- ^ fresh typed term -} jvm_fresh_var name jty = diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index ceac360f54..a2f56ebfa0 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -106,6 +106,7 @@ import qualified Data.HashMap.Strict as HashMap import qualified Data.Set as Set import Data.Sequence (Seq) import qualified Data.Sequence as Seq +import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Vector as V import Prettyprinter @@ -1439,7 +1440,7 @@ setupArg sc sym ecRef tp = do freshGlobal cty sc_tp = do ecs <- readIORef ecRef let len = Seq.length ecs - ec <- scFreshEC sc ("arg_"++show len) sc_tp + ec <- scFreshEC sc ("arg_" <> Text.pack (show len)) sc_tp writeIORef ecRef (ecs Seq.|> TypedExtCns cty ec) scFlatTermF sc (ExtCns ec) @@ -1649,7 +1650,7 @@ cryptolTypeOfActual dl mt = -- | Generate a fresh variable term. The name will be used when -- pretty-printing the variable in debug output. llvm_fresh_var :: - String {- ^ variable name -} -> + Text {- ^ variable name -} -> L.Type {- ^ variable type -} -> LLVMCrucibleSetupM TypedTerm {- ^ fresh typed term -} llvm_fresh_var name lty = @@ -1665,7 +1666,7 @@ llvm_fresh_var name lty = Just cty -> Setup.freshVariable sc name cty llvm_fresh_cryptol_var :: - String -> + Text -> Cryptol.Schema -> LLVMCrucibleSetupM TypedTerm llvm_fresh_cryptol_var name s = diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 5154b621cc..f5a4f4713c 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -10,6 +10,7 @@ Stability : provisional {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} diff --git a/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs b/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs index 4f24128885..879d3ef960 100644 --- a/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs @@ -202,7 +202,7 @@ buildArg arg idx $ arg ^. argSkelType . typeSkelLLVMType pure (Just val, Nothing, arg ^. argSkelName) where - ident = maybe ("arg" <> show idx) Text.unpack $ arg ^. argSkelName + ident = maybe ("arg" <> Text.pack (show idx)) id $ arg ^. argSkelName skeleton_prestate :: FunctionSkeleton -> @@ -237,7 +237,7 @@ rebuildArg (arg, prearg) idx -> LLVM.Array (fromIntegral $ s ^. sizeGuessElems) pt | otherwise -> pt _ -> pt - ident = maybe ("arg" <> show idx) Text.unpack nm + ident = maybe ("arg" <> Text.pack (show idx)) id nm in do val' <- llvm_fresh_var ident t llvm_points_to True ptr $ anySetupTerm val' @@ -255,7 +255,7 @@ skeleton_poststate skel prestate = do case skel ^. funSkelRet . typeSkelLLVMType of LLVM.PrimType LLVM.Void -> pure () t -> do - ret <- llvm_fresh_var ("return value of " <> (Text.unpack $ skel ^. funSkelName)) t + ret <- llvm_fresh_var ("return value of " <> (skel ^. funSkelName)) t llvm_return $ anySetupTerm ret pure $ SkeletonState{..} diff --git a/src/SAWScript/JavaExpr.hs b/src/SAWScript/JavaExpr.hs index 836b3b5a89..b3846b40a5 100644 --- a/src/SAWScript/JavaExpr.hs +++ b/src/SAWScript/JavaExpr.hs @@ -68,6 +68,7 @@ import Language.JVM.Common (ppFldId) import Data.List (intercalate) import Data.List.Split +import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Vector as V import Text.Read hiding (lift) @@ -209,7 +210,7 @@ data LogicExpr = } deriving (Show) -scJavaValue :: SharedContext -> Term -> String -> IO Term +scJavaValue :: SharedContext -> Term -> Text -> IO Term scJavaValue sc ty name = do scFreshGlobal sc name ty diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index fea336a5b2..709db3b9b5 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -188,7 +188,7 @@ evalProp sc unints (Prop p) = Just t -> pure t Nothing -> fail "goal_eval: expected EqTrue" - ecs <- traverse (\(nm, ty) -> scFreshEC sc (Text.unpack nm) ty) args + ecs <- traverse (\(nm, ty) -> scFreshEC sc nm ty) args vars <- traverse (scExtCns sc) ecs t0 <- instantiateVarList sc 0 (reverse vars) body' @@ -726,7 +726,7 @@ predicateToSATQuery sc unintSet tm0 = case evalFOT mmap tp of Nothing -> fail ("predicateToSATQuery: expected first order type: " ++ showTerm tp) Just fot -> - do ec <- scFreshEC sc (Text.unpack lnm) tp + do ec <- scFreshEC sc lnm tp etm <- scExtCns sc ec body' <- instantiateVar sc 0 etm body processTerm mmap (Map.insert ec fot vars) body' @@ -779,7 +779,7 @@ propToSATQuery sc unintSet prop = case evalFOT mmap tp of Nothing -> fail ("propToSATQuery: expected first order type: " ++ showTerm tp) Just fot -> - do ec <- scFreshEC sc (Text.unpack lnm) tp + do ec <- scFreshEC sc lnm tp etm <- scExtCns sc ec body' <- instantiateVar sc 0 etm body processTerm mmap (Map.insert ec fot vars) xs body' @@ -830,12 +830,12 @@ goalApply sc rule goal = applyFirst (asPiLists (unProp rule)) -- for the binder. Return the generated fresh term. tacticIntro :: (F.MonadFail m, MonadIO m) => SharedContext -> - String {- ^ Name to give to the variable. If empty, will be chosen automatically from the goal. -} -> + Text {- ^ Name to give to the variable. If empty, will be chosen automatically from the goal. -} -> Tactic m TypedTerm tacticIntro sc usernm = Tactic \goal -> case asPi (unProp (goalProp goal)) of Just (nm, tp, body) -> - do let name = if null usernm then Text.unpack nm else usernm + do let name = if Text.null usernm then nm else usernm xv <- liftIO $ scFreshEC sc name tp x <- liftIO $ scExtCns sc xv tt <- liftIO $ mkTypedTerm sc x diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs index 41ccc8cfcd..df5c8b3160 100644 --- a/src/SAWScript/Prover/MRSolver.hs +++ b/src/SAWScript/Prover/MRSolver.hs @@ -13,7 +13,6 @@ import Control.Monad.Reader import Control.Monad.State import Control.Monad.Except import Data.Semigroup -import qualified Data.Text as Text import Prettyprinter @@ -614,7 +613,7 @@ askMRSolver sc smt_conf timeout t1 t2 = flip evalStateT init_st $ runExceptT $ do mrSolveEq (Type tp1) (Type tp2) let (pi_args, ret_tp) = asPiList tp1 - vars <- mapM (\(x, x_tp) -> liftSC2 scFreshGlobal (Text.unpack x) x_tp) pi_args + vars <- mapM (\(x, x_tp) -> liftSC2 scFreshGlobal x x_tp) pi_args case asCompMApp ret_tp of Just _ -> return () Nothing -> throwError (NotCompFunType tp1)