<commit_before>{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}

module SAWScript.Interpreter
  ( interpret
  , interpretMain
  , interpretModuleAtEntry
  , InterpretEnv, interpretEnvValues, interpretEnvTypes, interpretEnvShared
  , buildInterpretEnv
  , Value, isVUnit
  , IsValue(..)
  )
  where

import Control.Applicative
import Control.Monad ( foldM )
import Data.Graph.SCC ( stronglyConnComp )
import Data.Graph ( SCC(..) )
import qualified Data.Map as M
import Data.Map ( Map )
import Data.Maybe ( fromMaybe )
import qualified Data.Set as S
import Data.Set ( Set )
import Data.Traversable hiding ( mapM )

import qualified SAWScript.AST as SS
import SAWScript.Builtins hiding (evaluate)
import qualified SAWScript.MGU as MGU
import SAWScript.Options
import SAWScript.Value
import Verifier.SAW.Prelude (preludeModule)
import Verifier.SAW.Rewriter ( Simpset, emptySimpset )
import Verifier.SAW.SharedTerm
import Verifier.SAW.TypedAST hiding ( incVars )

import qualified Verifier.Java.Codebase as JCB
import qualified Verifier.Java.SAWBackend as JavaSAW

type Expression = SS.Expr SS.ResolvedName SS.Schema
type BlockStatement = SS.BlockStmt SS.ResolvedName SS.Schema
type RNameMap = Map SS.ResolvedName
data InterpretEnv s = InterpretEnv { interpretEnvValues :: RNameMap (Value s)
                                   , interpretEnvTypes :: RNameMap SS.Schema
                                   , interpretEnvShared :: RNameMap (SharedTerm s)
                                   } deriving (Show)


-- Type matching ---------------------------------------------------------------

-- | Matches a (possibly) polymorphic type @polyty@ against a
-- monomorphic type @monoty@, which must be an instance of it. The
-- function returns a list of type variable instantiations, in the
-- same order as the variables in the outermost TypAbs of @polyty@.
typeInstantiation :: SS.Schema -> SS.Type -> [SS.Type]
typeInstantiation (SS.Forall xs t1) t2 =
  [ fromMaybe (error "unbound type variable") (M.lookup x m) | x <- xs ]
    where m = fromMaybe (error "matchType failed") (matchType t1 t2)

-- | @matchType pat ty@ returns a map of variable instantiations, if
-- @ty@ is an instance of @pat@.
matchType :: SS.Type -> SS.Type -> Maybe (Map SS.Name SS.Type)
matchType (SS.TyCon c1 ts1) (SS.TyCon c2 ts2) | c1 == c2 = matchTypes ts1 ts2
matchType (SS.TyRecord m1) (SS.TyRecord m2)
    | M.keys m1 == M.keys m2 = matchTypes (M.elems m1) (M.elems m2)
matchType (SS.TyVar (SS.BoundVar x)) t2 = Just (M.singleton x t2)
matchType t1 t2 = error $ "matchType failed: " ++ show (t1, t2)

matchTypes :: [SS.Type] -> [SS.Type] -> Maybe (Map SS.Name SS.Type)
matchTypes [] [] = Just M.empty
matchTypes [] (_ : _) = Nothing
matchTypes (_ : _) [] = Nothing
matchTypes (x : xs) (y : ys) = do
  m1 <- matchType x y
  m2 <- matchTypes xs ys
  let compatible = and (M.elems (M.intersectionWith (==) m1 m2))
  if compatible then Just (M.union m1 m2) else Nothing


-- Translation to SAWCore ------------------------------------------------------

data Kind = KStar | KSize

translateKind :: SharedContext s -> Kind -> IO (SharedTerm s)
translateKind sc KStar = scSort sc (mkSort 0)
translateKind sc KSize = scNatType sc

translatableType :: SS.Type -> Bool
translatableType ty =
    case ty of
      SS.TyRecord m               -> all translatableType (M.elems m)
      SS.TyCon (SS.TupleCon _) ts -> all translatableType ts
      SS.TyCon SS.ArrayCon [l, t] -> translatableType l && translatableType t
      SS.TyCon SS.FunCon [a, b]   -> translatableType a && translatableType b
      SS.TyCon SS.BoolCon []      -> True
      SS.TyCon SS.ZCon []         -> True
      SS.TyCon (SS.NumCon _) []   -> True
      SS.TyVar (SS.BoundVar _)    -> True
      _                           -> False

-- | Precondition: translatableType ty
translateType
    :: SharedContext s
    -> Map SS.Name (Int, Kind)
    -> SS.Type -> IO (SharedTerm s)
translateType sc tenv ty =
    case ty of
      SS.TyRecord tm              -> do tm' <- traverse (translateType sc tenv) tm
                                        scRecordType sc tm'
      SS.TyCon (SS.TupleCon _) ts -> do ts' <- traverse (translateType sc tenv) ts
                                        scTupleType sc ts'
      SS.TyCon SS.ArrayCon [n, t] -> do n' <- translateType sc tenv n
                                        t' <- translateType sc tenv t
                                        scVecType sc n' t'
      SS.TyCon SS.FunCon [a, b]   -> do a' <- translateType sc tenv a
                                        b' <- translateType sc tenv b
                                        scFun sc a' b'
      SS.TyCon SS.BoolCon []      -> scBoolType sc
      SS.TyCon SS.ZCon []         -> scNatType sc
      SS.TyCon (SS.NumCon n) []   -> scNat sc (fromInteger n)
      SS.TyVar (SS.BoundVar x)    -> case M.lookup x tenv of
                                       Nothing -> fail $ "translateType: unbound type variable: " ++ x
                                       Just (i, k) -> do
                                         k' <- translateKind sc k
                                         scLocalVar sc i k'
      _                           -> fail $ "untranslatable type: " ++ show ty

translatableSchema :: SS.Schema -> Bool
translatableSchema (SS.Forall _ t) = translatableType t

translateSchema
    :: SharedContext s
    -> Map SS.Name (Int, Kind)
    -> SS.Schema -> IO (SharedTerm s)
translateSchema sc tenv0 (SS.Forall xs0 t) = go tenv0 xs0
  where
    go tenv [] = translateType sc tenv t
    go tenv (x : xs) = do
      let inc (i, k) = (i + 1, k)
      let k = KStar
      let tenv' = M.insert x (0, k) (fmap inc tenv)
      k' <- translateKind sc k
      t' <- go tenv' xs
      scPi sc x k' t'

translatableExpr :: Set SS.ResolvedName -> Expression -> Bool
translatableExpr env expr =
    case expr of
      SS.Bit _             _ -> True
      SS.Quote _           _ -> False -- We could allow strings, but I don't think we need them.
      SS.Z _               _ -> True
      SS.Array es          t -> translatableSchema t && all (translatableExpr env) es
      SS.Undefined         _ -> False
      SS.Block _           _ -> False
      SS.Tuple es          _ -> all (translatableExpr env) es
      SS.Record bs         _ -> all (translatableExpr env . snd) bs
      SS.Index e n         _ -> translatableExpr env e && translatableExpr env n
      SS.Lookup e _        _ -> translatableExpr env e
      SS.Var x             _ -> S.member x env
      SS.Function x t e    _ -> translatableSchema t && translatableExpr env' e
          where env' = S.insert (SS.LocalName x) env
      SS.Application f e   _ -> translatableExpr env f && translatableExpr env e
      SS.LetBlock bs e       -> all (translatableExpr env . snd) bs && translatableExpr env' e
          where env' = foldr S.insert env [ SS.LocalName x | (x, _) <- bs ]

translateExpr
    :: forall s. SharedContext s
    -> RNameMap SS.Schema
    -> RNameMap (SharedTerm s)
    -> Map SS.Name (Int, Kind)
    -> Expression -> IO (SharedTerm s)
translateExpr sc tm sm km expr =
    case expr of
      SS.Bit b                  _ -> scBool sc b
      SS.Quote _                _ -> fail "translateExpr Quote"
      SS.Z z                    _ -> scNat sc (fromInteger z)
      SS.Array es              ty -> do let (_, t) = destArrayT ty
                                        t' <- translateType sc km t
                                        es' <- traverse (translateExpr sc tm sm km) es
                                        scVector sc t' es'
      SS.Undefined              _ -> fail "translateExpr: undefined"
      SS.Block _                _ -> fail "translateExpr Block"
      SS.Tuple es               _ -> do es' <- traverse (translateExpr sc tm sm km) es
                                        scTuple sc es'
      SS.Record bs              _ -> do bs' <- traverse (translateExpr sc tm sm km) (M.fromList bs)<commit_msg>Translate strings from SAWScript to SAWCore.<commit_after>{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}

module SAWScript.Interpreter
  ( interpret
  , interpretMain
  , interpretModuleAtEntry
  , InterpretEnv, interpretEnvValues, interpretEnvTypes, interpretEnvShared
  , buildInterpretEnv
  , Value, isVUnit
  , IsValue(..)
  )
  where

import Control.Applicative
import Control.Monad ( foldM )
import Data.Graph.SCC ( stronglyConnComp )
import Data.Graph ( SCC(..) )
import qualified Data.Map as M
import Data.Map ( Map )
import Data.Maybe ( fromMaybe )
import qualified Data.Set as S
import Data.Set ( Set )
import Data.Traversable hiding ( mapM )

import qualified SAWScript.AST as SS
import SAWScript.Builtins hiding (evaluate)
import qualified SAWScript.MGU as MGU
import SAWScript.Options
import SAWScript.Value
import Verifier.SAW.Prelude (preludeModule)
import Verifier.SAW.Rewriter ( Simpset, emptySimpset )
import Verifier.SAW.SharedTerm
import Verifier.SAW.TypedAST hiding ( incVars )

import qualified Verifier.Java.Codebase as JCB
import qualified Verifier.Java.SAWBackend as JavaSAW

type Expression = SS.Expr SS.ResolvedName SS.Schema
type BlockStatement = SS.BlockStmt SS.ResolvedName SS.Schema
type RNameMap = Map SS.ResolvedName
data InterpretEnv s = InterpretEnv { interpretEnvValues :: RNameMap (Value s)
                                   , interpretEnvTypes :: RNameMap SS.Schema
                                   , interpretEnvShared :: RNameMap (SharedTerm s)
                                   } deriving (Show)


-- Type matching ---------------------------------------------------------------

-- | Matches a (possibly) polymorphic type @polyty@ against a
-- monomorphic type @monoty@, which must be an instance of it. The
-- function returns a list of type variable instantiations, in the
-- same order as the variables in the outermost TypAbs of @polyty@.
typeInstantiation :: SS.Schema -> SS.Type -> [SS.Type]
typeInstantiation (SS.Forall xs t1) t2 =
  [ fromMaybe (error "unbound type variable") (M.lookup x m) | x <- xs ]
    where m = fromMaybe (error "matchType failed") (matchType t1 t2)

-- | @matchType pat ty@ returns a map of variable instantiations, if
-- @ty@ is an instance of @pat@.
matchType :: SS.Type -> SS.Type -> Maybe (Map SS.Name SS.Type)
matchType (SS.TyCon c1 ts1) (SS.TyCon c2 ts2) | c1 == c2 = matchTypes ts1 ts2
matchType (SS.TyRecord m1) (SS.TyRecord m2)
    | M.keys m1 == M.keys m2 = matchTypes (M.elems m1) (M.elems m2)
matchType (SS.TyVar (SS.BoundVar x)) t2 = Just (M.singleton x t2)
matchType t1 t2 = error $ "matchType failed: " ++ show (t1, t2)

matchTypes :: [SS.Type] -> [SS.Type] -> Maybe (Map SS.Name SS.Type)
matchTypes [] [] = Just M.empty
matchTypes [] (_ : _) = Nothing
matchTypes (_ : _) [] = Nothing
matchTypes (x : xs) (y : ys) = do
  m1 <- matchType x y
  m2 <- matchTypes xs ys
  let compatible = and (M.elems (M.intersectionWith (==) m1 m2))
  if compatible then Just (M.union m1 m2) else Nothing


-- Translation to SAWCore ------------------------------------------------------

data Kind = KStar | KSize

translateKind :: SharedContext s -> Kind -> IO (SharedTerm s)
translateKind sc KStar = scSort sc (mkSort 0)
translateKind sc KSize = scNatType sc

translatableType :: SS.Type -> Bool
translatableType ty =
    case ty of
      SS.TyRecord m               -> all translatableType (M.elems m)
      SS.TyCon (SS.TupleCon _) ts -> all translatableType ts
      SS.TyCon SS.ArrayCon [l, t] -> translatableType l && translatableType t
      SS.TyCon SS.FunCon [a, b]   -> translatableType a && translatableType b
      SS.TyCon SS.BoolCon []      -> True
      SS.TyCon SS.ZCon []         -> True
      SS.TyCon (SS.NumCon _) []   -> True
      SS.TyVar (SS.BoundVar _)    -> True
      _                           -> False

-- | Precondition: translatableType ty
translateType
    :: SharedContext s
    -> Map SS.Name (Int, Kind)
    -> SS.Type -> IO (SharedTerm s)
translateType sc tenv ty =
    case ty of
      SS.TyRecord tm              -> do tm' <- traverse (translateType sc tenv) tm
                                        scRecordType sc tm'
      SS.TyCon (SS.TupleCon _) ts -> do ts' <- traverse (translateType sc tenv) ts
                                        scTupleType sc ts'
      SS.TyCon SS.ArrayCon [n, t] -> do n' <- translateType sc tenv n
                                        t' <- translateType sc tenv t
                                        scVecType sc n' t'
      SS.TyCon SS.FunCon [a, b]   -> do a' <- translateType sc tenv a
                                        b' <- translateType sc tenv b
                                        scFun sc a' b'
      SS.TyCon SS.BoolCon []      -> scBoolType sc
      SS.TyCon SS.ZCon []         -> scNatType sc
      SS.TyCon (SS.NumCon n) []   -> scNat sc (fromInteger n)
      SS.TyVar (SS.BoundVar x)    -> case M.lookup x tenv of
                                       Nothing -> fail $ "translateType: unbound type variable: " ++ x
                                       Just (i, k) -> do
                                         k' <- translateKind sc k
                                         scLocalVar sc i k'
      _                           -> fail $ "untranslatable type: " ++ show ty

translatableSchema :: SS.Schema -> Bool
translatableSchema (SS.Forall _ t) = translatableType t

translateSchema
    :: SharedContext s
    -> Map SS.Name (Int, Kind)
    -> SS.Schema -> IO (SharedTerm s)
translateSchema sc tenv0 (SS.Forall xs0 t) = go tenv0 xs0
  where
    go tenv [] = translateType sc tenv t
    go tenv (x : xs) = do
      let inc (i, k) = (i + 1, k)
      let k = KStar
      let tenv' = M.insert x (0, k) (fmap inc tenv)
      k' <- translateKind sc k
      t' <- go tenv' xs
      scPi sc x k' t'

translatableExpr :: Set SS.ResolvedName -> Expression -> Bool
translatableExpr env expr =
    case expr of
      SS.Bit _             _ -> True
      SS.Quote _           _ -> True
      SS.Z _               _ -> True
      SS.Array es          t -> translatableSchema t && all (translatableExpr env) es
      SS.Undefined         _ -> False
      SS.Block _           _ -> False
      SS.Tuple es          _ -> all (translatableExpr env) es
      SS.Record bs         _ -> all (translatableExpr env . snd) bs
      SS.Index e n         _ -> translatableExpr env e && translatableExpr env n
      SS.Lookup e _        _ -> translatableExpr env e
      SS.Var x             _ -> S.member x env
      SS.Function x t e    _ -> translatableSchema t && translatableExpr env' e
          where env' = S.insert (SS.LocalName x) env
      SS.Application f e   _ -> translatableExpr env f && translatableExpr env e
      SS.LetBlock bs e       -> all (translatableExpr env . snd) bs && translatableExpr env' e
          where env' = foldr S.insert env [ SS.LocalName x | (x, _) <- bs ]

translateExpr
    :: forall s. SharedContext s
    -> RNameMap SS.Schema
    -> RNameMap (SharedTerm s)
    -> Map SS.Name (Int, Kind)
    -> Expression -> IO (SharedTerm s)
translateExpr sc tm sm km expr =
    case expr of
      SS.Bit b                  _ -> scBool sc b
      SS.Quote s                _ -> scString sc s
      SS.Z z                    _ -> scNat sc (fromInteger z)
      SS.Array es              ty -> do let (_, t) = destArrayT ty
                                        t' <- translateType sc km t
                                        es' <- traverse (translateExpr sc tm sm km) es
                                        scVector sc t' es'
      SS.Undefined              _ -> fail "translateExpr: undefined"
      SS.Block _                _ -> fail "translateExpr Block"
      SS.Tuple es               _ -> do es' <- traverse (translateExpr sc tm sm km) es
                                        scTuple sc es'
      SS.Record bs              _ -> do bs' <- traverse (translateExpr sc tm sm km) (M.fromList bs)
{'fraction_non_alphanumeric': 0.11004549366777328, 'fraction_numerical': 0.00454936677732694, 'mean_word_length': 1.802722260509993, 'pattern_counts': {'":': 0, '<': 37, '<?xml version=': 0, '>': 133, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 52, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2461896', 'n_tokens_mistral': 4908, 'n_tokens_neox': 4773, 'n_words': 1618}