<commit_before>-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Backend.SAWCore
-- Description      : Crucible interface for generating SAWCore
-- Copyright        : (c) Galois, Inc 2014-2016
-- License          : BSD3
-- Maintainer       : <NAME> <<EMAIL>>
-- Stability        : provisional
--
-- This module provides a Crucible backend that produces SAWCore terms.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}

module Verifier.SAW.Simulator.What4.ReturnTrip where

--import           Control.Exception ( bracket )
import           Control.Lens
import           Control.Monad
import qualified Data.BitVector.Sized as BV
import           Data.IORef
import           Data.List (elemIndex)
import           Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import           Data.List.NonEmpty (NonEmpty(..))
import           Data.Map ( Map )
import qualified Data.Map as Map
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Ratio
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import           Data.Word(Word64)
import qualified Data.Text as Text

import           Numeric.Natural

import           What4.BaseTypes
import           What4.Interface
import qualified What4.Expr.ArrayUpdateMap as AUM
import qualified What4.Expr.Builder as B
import qualified What4.Expr.BoolMap as BM
import qualified What4.Expr.WeightedSum as WSum
import qualified What4.SemiRing as B
import           What4.Symbol

import qualified Verifier.SAW.SharedTerm as SC
import qualified Verifier.SAW.TypedAST as SC
import           Verifier.SAW.Utils (panic)

data SAWCruciblePersonality sym = SAWCruciblePersonality

data SAWCoreState n
  = SAWCoreState
    { saw_ctx       :: SC.SharedContext                         -- ^ the main SAWCore datastructure for building shared terms
    , saw_inputs    :: IORef (Seq (SC.ExtCns SC.Term ))
      -- ^ a record of all the symbolic input variables created so far,
      --   in the order they were created

    , saw_symMap :: IORef (Map Word64 (SC.SharedContext -> [SC.Term] -> IO SC.Term))
      -- ^ What to do with uninterpreted functions.
      -- The key is the "indexValue" of the "symFunId" for the function

    , saw_elt_cache :: B.IdxCache n SAWExpr
      -- ^ cache mapping a What4 variable nonce to its corresponding SAWCore term.

    , saw_elt_cache_r :: IORef (IntMap (Some (B.Expr n)))
      -- ^ reverse cache mapping a SAWCore TermIndex to its corresponding What4 variable.
      -- 'saw_elt_cache' and 'saw_elt_cache_r' implement a bidirectional map between
      -- SAWCore terms and What4 variables.

    }

data SAWExpr (bt :: BaseType) where
  SAWExpr :: !SC.Term -> SAWExpr bt

  -- This is a term that represents an integer, but has an
  -- implicit integer-to-real conversion.
  IntToRealSAWExpr :: !(SAWExpr BaseIntegerType) -> SAWExpr BaseRealType
  -- This is a SAWCore term that represents a natural number, but has an
  -- implicit nat-to-integer conversion.
  NatToIntSAWExpr :: !(SAWExpr BaseNatType) -> SAWExpr BaseIntegerType

{-

-- | Run the given IO action with the given SAW backend.<commit_msg>Utility for creating new SAWCoreState<commit_after>-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Backend.SAWCore
-- Description      : Crucible interface for generating SAWCore
-- Copyright        : (c) Galois, Inc 2014-2016
-- License          : BSD3
-- Maintainer       : <NAME> <rdock<EMAIL>>
-- Stability        : provisional
--
-- This module provides a Crucible backend that produces SAWCore terms.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}

module Verifier.SAW.Simulator.What4.ReturnTrip where

--import           Control.Exception ( bracket )
import           Control.Lens
import           Control.Monad
import qualified Data.BitVector.Sized as BV
import           Data.IORef
import           Data.List (elemIndex)
import           Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import           Data.List.NonEmpty (NonEmpty(..))
import           Data.Map ( Map )
import qualified Data.Map as Map
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Ratio
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import           Data.Word(Word64)
import qualified Data.Text as Text

import           Numeric.Natural

import           What4.BaseTypes
import           What4.Interface
import qualified What4.Expr.ArrayUpdateMap as AUM
import qualified What4.Expr.Builder as B
import qualified What4.Expr.BoolMap as BM
import qualified What4.Expr.WeightedSum as WSum
import qualified What4.SemiRing as B
import           What4.Symbol

import qualified Verifier.SAW.SharedTerm as SC
import qualified Verifier.SAW.TypedAST as SC
import           Verifier.SAW.Utils (panic)

data SAWCoreState n
  = SAWCoreState
    { saw_ctx       :: SC.SharedContext                         -- ^ the main SAWCore datastructure for building shared terms
    , saw_inputs    :: IORef (Seq (SC.ExtCns SC.Term ))
      -- ^ a record of all the symbolic input variables created so far,
      --   in the order they were created

    , saw_symMap :: IORef (Map Word64 (SC.SharedContext -> [SC.Term] -> IO SC.Term))
      -- ^ What to do with uninterpreted functions.
      -- The key is the "indexValue" of the "symFunId" for the function

    , saw_elt_cache :: B.IdxCache n SAWExpr
      -- ^ cache mapping a What4 variable nonce to its corresponding SAWCore term.

    , saw_elt_cache_r :: IORef (IntMap (Some (B.Expr n)))
      -- ^ reverse cache mapping a SAWCore TermIndex to its corresponding What4 variable.
      -- 'saw_elt_cache' and 'saw_elt_cache_r' implement a bidirectional map between
      -- SAWCore terms and What4 variables.

    }

newSAWCoreState ::
  SC.SharedContext ->
  IO (SAWCoreState n)
newSAWCoreState sc =
  do inpr <- newIORef Seq.empty
     ch   <- B.newIdxCache
     ch_r <- newIORef IntMap.empty
     mr   <- newIORef Map.empty
     return SAWCoreState
            { saw_ctx = sc
            , saw_inputs = inpr
            , saw_symMap = mr
            , saw_elt_cache = ch
            , saw_elt_cache_r = ch_r
            }

data SAWExpr (bt :: BaseType) where
  SAWExpr :: !SC.Term -> SAWExpr bt

  -- This is a term that represents an integer, but has an
  -- implicit integer-to-real conversion.
  IntToRealSAWExpr :: !(SAWExpr BaseIntegerType) -> SAWExpr BaseRealType
  -- This is a SAWCore term that represents a natural number, but has an
  -- implicit nat-to-integer conversion.
  NatToIntSAWExpr :: !(SAWExpr BaseNatType) -> SAWExpr BaseIntegerType

{-

-- | Run the given IO action with the given SAW backend.
{'fraction_non_alphanumeric': 0.11971830985915492, 'fraction_numerical': 0.006520605112154408, 'mean_word_length': 2.298494623655914, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 20, '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': '13961', 'n_tokens_mistral': 2270, 'n_tokens_neox': 2198, 'n_words': 696}