<commit_before>{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}

{- |
Module           : $Header$
Description      :
License          : BSD3
Stability        : provisional
Point-of-contact : atomb
-}
module SAWScript.JavaUtils where

#if !MIN_VERSION_base(4,8,0)
import Control.Applicative
#endif
import Control.Lens
import Control.Monad
import Control.Monad.IO.Class
import qualified Data.Array as Array
import Data.Int
import Data.IORef
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as Set

import Verifier.Java.Simulator as JSS
import Verifier.SAW.Recognizer
import Verifier.SAW.SharedTerm

import qualified SAWScript.CongruenceClosure as CC
import SAWScript.JavaExpr
import SAWScript.TypedTerm

type SAWBackend = SharedContext
type SpecPathState = Path SharedContext
type SpecJavaValue = Value Term
type SAWJavaSim = Simulator SharedContext
type LocalMap t = Map.Map LocalVariableIndex (Value t)

boolExtend :: SharedContext -> Term -> IO Term
boolExtend sc x = do
  n31 <- scNat sc 31
  n1 <- scNat sc 1
  scBvUExt sc n31 n1 x

boolExtend' :: SharedContext -> Term -> IO Term
boolExtend' sc x = do
  bool <- scBoolType sc
  x' <- scSingle sc bool x
  boolExtend sc x'

byteExtend :: SharedContext -> Term -> IO Term
byteExtend sc x = do
  n24 <- scNat sc 24
  n8 <- scNat sc 8
  scBvSExt sc n24 n8 x

shortExtend :: SharedContext -> Term -> IO Term
shortExtend sc x = do
  n16 <- scNat sc 16
  scBvSExt sc n16 n16 x

extendToIValue :: SharedContext -> Term -> IO Term
extendToIValue sc t = do
  ty <- scWhnf sc =<< scTypeOf sc t
  case ty of
    (asBoolType -> Just ()) -> boolExtend' sc t
    (asBitvectorType -> Just 1) -> boolExtend sc t
    (asBitvectorType -> Just 8) -> byteExtend sc t
    (asBitvectorType -> Just 16) -> shortExtend sc t
    (asBitvectorType -> Just 32) -> return t
    _ -> fail $ "Invalid type passed to extendToIValue: " ++ show ty

typeOfValue :: SharedContext -> JSS.Value Term -> IO JSS.Type
typeOfValue sc (IValue t) = do
  ty <- scWhnf sc =<< scTypeOf sc t
  case ty of
    (asBoolType -> Just ()) -> return JSS.BooleanType
    (asBitvectorType -> Just 1) -> return JSS.BooleanType
    (asBitvectorType -> Just 8) -> return JSS.ByteType
    (asBitvectorType -> Just 16) -> return JSS.ShortType<commit_msg>Fix type error in small type extension for Java<commit_after>{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}

{- |
Module           : $Header$
Description      :
License          : BSD3
Stability        : provisional
Point-of-contact : atomb
-}
module SAWScript.JavaUtils where

#if !MIN_VERSION_base(4,8,0)
import Control.Applicative
#endif
import Control.Lens
import Control.Monad
import Control.Monad.IO.Class
import qualified Data.Array as Array
import Data.Int
import Data.IORef
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as Set

import Verifier.Java.Simulator as JSS
import Verifier.SAW.Recognizer
import Verifier.SAW.SharedTerm

import qualified SAWScript.CongruenceClosure as CC
import SAWScript.JavaExpr
import SAWScript.TypedTerm

type SAWBackend = SharedContext
type SpecPathState = Path SharedContext
type SpecJavaValue = Value Term
type SAWJavaSim = Simulator SharedContext
type LocalMap t = Map.Map LocalVariableIndex (Value t)

boolExtend :: SharedContext -> Term -> IO Term
boolExtend sc x = do
  n31 <- scNat sc 31
  n1 <- scNat sc 1
  scBvUExt sc n31 n1 x

boolExtend' :: SharedContext -> Term -> IO Term
boolExtend' sc x = do
  bool <- scBoolType sc
  x' <- scSingle sc bool x
  boolExtend sc x'

byteExtend :: SharedContext -> Term -> IO Term
byteExtend sc x = do
  n24 <- scNat sc 24
  n7 <- scNat sc 7
  scBvSExt sc n24 n7 x

shortExtend :: SharedContext -> Term -> IO Term
shortExtend sc x = do
  n15 <- scNat sc 15
  n16 <- scNat sc 16
  scBvSExt sc n16 n15 x

extendToIValue :: SharedContext -> Term -> IO Term
extendToIValue sc t = do
  ty <- scWhnf sc =<< scTypeOf sc t
  case ty of
    (asBoolType -> Just ()) -> boolExtend' sc t
    (asBitvectorType -> Just 1) -> boolExtend sc t
    (asBitvectorType -> Just 8) -> byteExtend sc t
    (asBitvectorType -> Just 16) -> shortExtend sc t
    (asBitvectorType -> Just 32) -> return t
    _ -> fail $ "Invalid type passed to extendToIValue: " ++ show ty

typeOfValue :: SharedContext -> JSS.Value Term -> IO JSS.Type
typeOfValue sc (IValue t) = do
  ty <- scWhnf sc =<< scTypeOf sc t
  case ty of
    (asBoolType -> Just ()) -> return JSS.BooleanType
    (asBitvectorType -> Just 1) -> return JSS.BooleanType
    (asBitvectorType -> Just 8) -> return JSS.ByteType
    (asBitvectorType -> Just 16) -> return JSS.ShortType
{'fraction_non_alphanumeric': 0.09565398211686421, 'fraction_numerical': 0.017467248908296942, 'mean_word_length': 3.3450767841011744, 'pattern_counts': {'":': 0, '<': 30, '<?xml version=': 0, '>': 65, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4091159', 'n_tokens_mistral': 1715, 'n_tokens_neox': 1603, 'n_words': 549}