From e89a291bdb29860d1dfc6954d275ebab7714ad5e Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 21 Feb 2018 10:24:46 -0800 Subject: [PATCH] Add saw-script `String` variables to cryptol context with type `String n`. --- src/SAWScript/Interpreter.hs | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 5264769c43..db90432f3b 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -38,6 +38,7 @@ import qualified Data.Map as Map import Data.Map ( Map ) import qualified Data.Set as Set import Data.Text (pack) +import qualified Data.Vector as Vector import System.Directory (getCurrentDirectory, setCurrentDirectory, canonicalizePath) import System.FilePath (takeDirectory) import System.Process (readProcess) @@ -80,6 +81,7 @@ import qualified Cryptol.Utils.Ident as T (packIdent, packModName) import qualified Cryptol.Eval as V (PPOpts(..)) import qualified Cryptol.Eval.Monad as V (runEval) import qualified Cryptol.Eval.Value as V (defaultPPOpts, ppValue) +import qualified Cryptol.TypeCheck.AST as C import qualified Text.PrettyPrint.ANSI.Leijen as PP @@ -126,8 +128,29 @@ extendEnv x mt md v rw = -> CEnv.bindInteger (ident, n) ce VCryptolModule m -> CEnv.bindCryptolModule (modname, m) ce + VString s + -> CEnv.bindTypedTerm (ident, typedTermOfString s) ce _ -> ce +typedTermOfString :: String -> TypedTerm +typedTermOfString cs = TypedTerm schema trm + where + nat :: Integer -> Term + nat n = Unshared (FTermF (NatLit n)) + bvNat :: Term + bvNat = Unshared (FTermF (GlobalDef "Prelude.bvNat")) + bvNat8 :: Term + bvNat8 = Unshared (App bvNat (nat 8)) + encodeChar :: Char -> Term + encodeChar c = Unshared (App bvNat8 (nat (toInteger (fromEnum c)))) + bitvector :: Term + bitvector = Unshared (FTermF (GlobalDef "Prelude.bitvector")) + byteT :: Term + byteT = Unshared (App bitvector (nat 8)) + trm :: Term + trm = Unshared (FTermF (ArrayValue byteT (Vector.fromList (map encodeChar cs)))) + schema = C.Forall [] [] (C.tString (length cs)) + addTypedef :: SS.Name -> SS.Type -> TopLevelRW -> TopLevelRW addTypedef name ty rw = rw { rwTypedef = Map.insert name ty (rwTypedef rw) }