-- |
-- Module      :  Cryptol.Symbolic.Value
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Cryptol.Symbolic.Value
  ( SBool, SWord, SInteger
  , literalSWord
  , fromBitsLE
  , forallBV_, existsBV_
  , forallSBool_, existsSBool_
  , forallSInteger_, existsSInteger_
  , Value
  , TValue, isTBit, tvSeq
  , GenValue(..), lam, tlam, toStream, toFinSeq, toSeq
  , fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
  , fromSeq, fromVWord
  , evalPanic
  , iteSValue, mergeValue, mergeWord, mergeBit, mergeBits, mergeSeqMap
  , mergeWord'
  )
  where

import Data.Bits (bit, complement)
import Data.List (foldl')
import qualified Data.Sequence as Seq

import Data.SBV (symbolicEnv)
import Data.SBV.Dynamic

--import Cryptol.Eval.Monad
import Cryptol.Eval.Type   (TValue(..), isTBit, tvSeq)
import Cryptol.Eval.Monad  (Eval, ready)
import Cryptol.Eval.Value  ( GenValue(..), BitWord(..), lam, tlam, toStream,
                           toFinSeq, toSeq, WordValue(..),
                           fromSeq, fromVBit, fromVWord, fromVFun, fromVPoly,
                           fromVTuple, fromVRecord, lookupRecord, SeqMap(..),
                           ppBV, BV(..), integerToChar, lookupSeqMap, memoMap,
                           wordValueSize, asBitsMap)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.PP

import Control.Monad.Trans  (liftIO)

-- SBool and SWord -------------------------------------------------------------

type SBool = SVal
type SWord = SVal
type SInteger = SVal

fromBitsLE :: [SBool] -> SWord
fromBitsLE :: [SBool] -> SBool
fromBitsLE bs :: [SBool]
bs = (SBool -> SBool -> SBool) -> SBool -> [SBool] -> SBool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' SBool -> SBool -> SBool
f (Int -> Integer -> SBool
literalSWord 0 0) [SBool]
bs
  where f :: SBool -> SBool -> SBool
f w :: SBool
w b :: SBool
b = SBool -> SBool -> SBool
svJoin (SBool -> SBool
svToWord1 SBool
b) SBool
w

literalSWord :: Int -> Integer -> SWord
literalSWord :: Int -> Integer -> SBool
literalSWord w :: Int
w i :: Integer
i = Kind -> Integer -> SBool
svInteger (Bool -> Int -> Kind
KBounded Bool
False Int
w) Integer
i

forallBV_ :: Int -> Symbolic SWord
forallBV_ :: Int -> Symbolic SBool
forallBV_ w :: Int
w = SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SBool -> Symbolic SBool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBool -> Symbolic SBool)
-> (State -> IO SBool) -> State -> Symbolic SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL) (Bool -> Int -> Kind
KBounded Bool
False Int
w) Maybe String
forall a. Maybe a
Nothing

existsBV_ :: Int -> Symbolic SWord
existsBV_ :: Int -> Symbolic SBool
existsBV_ w :: Int
w = SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SBool -> Symbolic SBool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBool -> Symbolic SBool)
-> (State -> IO SBool) -> State -> Symbolic SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX) (Bool -> Int -> Kind
KBounded Bool
False Int
w) Maybe String
forall a. Maybe a
Nothing

forallSBool_ :: Symbolic SBool
forallSBool_ :: Symbolic SBool
forallSBool_ = SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SBool -> Symbolic SBool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBool -> Symbolic SBool)
-> (State -> IO SBool) -> State -> Symbolic SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL) Kind
KBool Maybe String
forall a. Maybe a
Nothing

existsSBool_ :: Symbolic SBool
existsSBool_ :: Symbolic SBool
existsSBool_ = SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SBool -> Symbolic SBool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBool -> Symbolic SBool)
-> (State -> IO SBool) -> State -> Symbolic SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX) Kind
KBool Maybe String
forall a. Maybe a
Nothing

forallSInteger_ :: Symbolic SBool
forallSInteger_ :: Symbolic SBool
forallSInteger_ = SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SBool -> Symbolic SBool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBool -> Symbolic SBool)
-> (State -> IO SBool) -> State -> Symbolic SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
ALL) Kind
KUnbounded Maybe String
forall a. Maybe a
Nothing

existsSInteger_ :: Symbolic SBool
existsSInteger_ :: Symbolic SBool
existsSInteger_ = SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv SymbolicT IO State -> (State -> Symbolic SBool) -> Symbolic SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SBool -> Symbolic SBool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBool -> Symbolic SBool)
-> (State -> IO SBool) -> State -> Symbolic SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SBool
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX) Kind
KUnbounded Maybe String
forall a. Maybe a
Nothing

-- Values ----------------------------------------------------------------------

type Value = GenValue SBool SWord SInteger

-- Symbolic Conditionals -------------------------------------------------------

iteSValue :: SBool -> Value -> Value -> Eval Value
iteSValue :: SBool -> Value -> Value -> Eval Value
iteSValue c :: SBool
c x :: Value
x y :: Value
y =
  case SBool -> Maybe Bool
svAsBool SBool
c of
    Just True  -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
x
    Just False -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
y
    Nothing    -> Bool -> SBool -> Value -> Value -> Eval Value
mergeValue Bool
True SBool
c Value
x Value
y

mergeBit :: Bool
         -> SBool
         -> SBool
         -> SBool
         -> SBool
mergeBit :: Bool -> SBool -> SBool -> SBool -> SBool
mergeBit f :: Bool
f c :: SBool
c b1 :: SBool
b1 b2 :: SBool
b2 = Kind -> Bool -> SBool -> SBool -> SBool -> SBool
svSymbolicMerge Kind
KBool Bool
f SBool
c SBool
b1 SBool
b2

mergeWord :: Bool
          -> SBool
          -> WordValue SBool SWord SInteger
          -> WordValue SBool SWord SInteger
          -> WordValue SBool SWord SInteger
mergeWord :: Bool
-> SBool
-> WordValue SBool SBool SBool
-> WordValue SBool SBool SBool
-> WordValue SBool SBool SBool
mergeWord f :: Bool
f c :: SBool
c (WordVal w1 :: SBool
w1) (WordVal w2 :: SBool
w2) =
    SBool -> WordValue SBool SBool SBool
forall b w i. w -> WordValue b w i
WordVal (SBool -> WordValue SBool SBool SBool)
-> SBool -> WordValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ Kind -> Bool -> SBool -> SBool -> SBool -> SBool
svSymbolicMerge (SBool -> Kind
forall a. HasKind a => a -> Kind
kindOf SBool
w1) Bool
f SBool
c SBool
w1 SBool
w2
mergeWord f :: Bool
f c :: SBool
c (WordVal w1 :: SBool
w1) (BitsVal ys :: Seq (Eval SBool)
ys) =
    Seq (Eval SBool) -> WordValue SBool SBool SBool
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
-> Seq (Eval SBool) -> WordValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ Bool
-> SBool
-> Seq (Eval SBool)
-> Seq (Eval SBool)
-> Seq (Eval SBool)
mergeBits Bool
f SBool
c ([Eval SBool] -> Seq (Eval SBool)
forall a. [a] -> Seq a
Seq.fromList ([Eval SBool] -> Seq (Eval SBool))
-> [Eval SBool] -> Seq (Eval SBool)
forall a b. (a -> b) -> a -> b
$ (SBool -> Eval SBool) -> [SBool] -> [Eval SBool]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> Eval SBool
forall a. a -> Eval a
ready ([SBool] -> [Eval SBool]) -> [SBool] -> [Eval SBool]
forall a b. (a -> b) -> a -> b
$ SBool -> [SBool]
forall b w i. BitWord b w i => w -> [b]
unpackWord SBool
w1) Seq (Eval SBool)
ys
mergeWord f :: Bool
f c :: SBool
c (BitsVal xs :: Seq (Eval SBool)
xs) (WordVal w2 :: SBool
w2) =
    Seq (Eval SBool) -> WordValue SBool SBool SBool
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
-> Seq (Eval SBool) -> WordValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ Bool
-> SBool
-> Seq (Eval SBool)
-> Seq (Eval SBool)
-> Seq (Eval SBool)
mergeBits Bool
f SBool
c Seq (Eval SBool)
xs ([Eval SBool] -> Seq (Eval SBool)
forall a. [a] -> Seq a
Seq.fromList ([Eval SBool] -> Seq (Eval SBool))
-> [Eval SBool] -> Seq (Eval SBool)
forall a b. (a -> b) -> a -> b
$ (SBool -> Eval SBool) -> [SBool] -> [Eval SBool]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> Eval SBool
forall a. a -> Eval a
ready ([SBool] -> [Eval SBool]) -> [SBool] -> [Eval SBool]
forall a b. (a -> b) -> a -> b
$ SBool -> [SBool]
forall b w i. BitWord b w i => w -> [b]
unpackWord SBool
w2)
mergeWord f :: Bool
f c :: SBool
c (BitsVal xs :: Seq (Eval SBool)
xs) (BitsVal ys :: Seq (Eval SBool)
ys) =
    Seq (Eval SBool) -> WordValue SBool SBool SBool
forall b w i. Seq (Eval b) -> WordValue b w i
BitsVal (Seq (Eval SBool) -> WordValue SBool SBool SBool)
-> Seq (Eval SBool) -> WordValue SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ Bool
-> SBool
-> Seq (Eval SBool)
-> Seq (Eval SBool)
-> Seq (Eval SBool)
mergeBits Bool
f SBool
c Seq (Eval SBool)
xs Seq (Eval SBool)
ys
mergeWord f :: Bool
f c :: SBool
c w1 :: WordValue SBool SBool SBool
w1 w2 :: WordValue SBool SBool SBool
w2 =
    Integer -> SeqMap SBool SBool SBool -> WordValue SBool SBool SBool
forall b w i. Integer -> SeqMap b w i -> WordValue b w i
LargeBitsVal (WordValue SBool SBool SBool -> Integer
forall b w i. BitWord b w i => WordValue b w i -> Integer
wordValueSize WordValue SBool SBool SBool
w1) (Bool
-> SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
mergeSeqMap Bool
f SBool
c (WordValue SBool SBool SBool -> SeqMap SBool SBool SBool
forall b w i. BitWord b w i => WordValue b w i -> SeqMap b w i
asBitsMap WordValue SBool SBool SBool
w1) (WordValue SBool SBool SBool -> SeqMap SBool SBool SBool
forall b w i. BitWord b w i => WordValue b w i -> SeqMap b w i
asBitsMap WordValue SBool SBool SBool
w2))

mergeWord' :: Bool
           -> SBool
           -> Eval (WordValue SBool SWord SInteger)
           -> Eval (WordValue SBool SWord SInteger)
           -> Eval (WordValue SBool SWord SInteger)
mergeWord' :: Bool
-> SBool
-> Eval (WordValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
mergeWord' f :: Bool
f c :: SBool
c x :: Eval (WordValue SBool SBool SBool)
x y :: Eval (WordValue SBool SBool SBool)
y = Bool
-> SBool
-> WordValue SBool SBool SBool
-> WordValue SBool SBool SBool
-> WordValue SBool SBool SBool
mergeWord Bool
f SBool
c (WordValue SBool SBool SBool
 -> WordValue SBool SBool SBool -> WordValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
-> Eval
     (WordValue SBool SBool SBool -> WordValue SBool SBool SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval (WordValue SBool SBool SBool)
x Eval (WordValue SBool SBool SBool -> WordValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Eval (WordValue SBool SBool SBool)
y

mergeBits :: Bool
          -> SBool
          -> Seq.Seq (Eval SBool)
          -> Seq.Seq (Eval SBool)
          -> Seq.Seq (Eval SBool)
mergeBits :: Bool
-> SBool
-> Seq (Eval SBool)
-> Seq (Eval SBool)
-> Seq (Eval SBool)
mergeBits f :: Bool
f c :: SBool
c bs1 :: Seq (Eval SBool)
bs1 bs2 :: Seq (Eval SBool)
bs2 = (Eval SBool -> Eval SBool -> Eval SBool)
-> Seq (Eval SBool) -> Seq (Eval SBool) -> Seq (Eval SBool)
forall a b c. (a -> b -> c) -> Seq a -> Seq b -> Seq c
Seq.zipWith Eval SBool -> Eval SBool -> Eval SBool
forall (f :: * -> *).
Applicative f =>
f SBool -> f SBool -> f SBool
mergeBit' Seq (Eval SBool)
bs1 Seq (Eval SBool)
bs2
 where mergeBit' :: f SBool -> f SBool -> f SBool
mergeBit' b1 :: f SBool
b1 b2 :: f SBool
b2 = Bool -> SBool -> SBool -> SBool -> SBool
mergeBit Bool
f SBool
c (SBool -> SBool -> SBool) -> f SBool -> f (SBool -> SBool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f SBool
b1 f (SBool -> SBool) -> f SBool -> f SBool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f SBool
b2

mergeInteger :: Bool
             -> SBool
             -> SInteger
             -> SInteger
             -> SInteger
mergeInteger :: Bool -> SBool -> SBool -> SBool -> SBool
mergeInteger f :: Bool
f c :: SBool
c x :: SBool
x y :: SBool
y = Kind -> Bool -> SBool -> SBool -> SBool -> SBool
svSymbolicMerge Kind
KUnbounded Bool
f SBool
c SBool
x SBool
y

mergeValue :: Bool -> SBool -> Value -> Value -> Eval Value
mergeValue :: Bool -> SBool -> Value -> Value -> Eval Value
mergeValue f :: Bool
f c :: SBool
c v1 :: Value
v1 v2 :: Value
v2 =
  case (Value
v1, Value
v2) of
    (VRecord fs1 :: [(Ident, Eval Value)]
fs1, VRecord fs2 :: [(Ident, Eval Value)]
fs2) -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [(Ident, Eval Value)] -> Value
forall b w i. [(Ident, Eval (GenValue b w i))] -> GenValue b w i
VRecord ([(Ident, Eval Value)] -> Value) -> [(Ident, Eval Value)] -> Value
forall a b. (a -> b) -> a -> b
$ ((Ident, Eval Value) -> (Ident, Eval Value) -> (Ident, Eval Value))
-> [(Ident, Eval Value)]
-> [(Ident, Eval Value)]
-> [(Ident, Eval Value)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Ident, Eval Value) -> (Ident, Eval Value) -> (Ident, Eval Value)
forall a.
Eq a =>
(a, Eval Value) -> (a, Eval Value) -> (a, Eval Value)
mergeField [(Ident, Eval Value)]
fs1 [(Ident, Eval Value)]
fs2
    (VTuple vs1 :: [Eval Value]
vs1 , VTuple vs2 :: [Eval Value]
vs2 ) -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ [Eval Value] -> Value
forall b w i. [Eval (GenValue b w i)] -> GenValue b w i
VTuple ([Eval Value] -> Value) -> [Eval Value] -> Value
forall a b. (a -> b) -> a -> b
$ (Eval Value -> Eval Value -> Eval Value)
-> [Eval Value] -> [Eval Value] -> [Eval Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
mergeValue' Bool
f SBool
c) [Eval Value]
vs1 [Eval Value]
vs2
    (VBit b1 :: SBool
b1    , VBit b2 :: SBool
b2    ) -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ SBool -> Value
forall b w i. b -> GenValue b w i
VBit (SBool -> Value) -> SBool -> Value
forall a b. (a -> b) -> a -> b
$ Bool -> SBool -> SBool -> SBool -> SBool
mergeBit Bool
f SBool
c SBool
b1 SBool
b2
    (VInteger i1 :: SBool
i1, VInteger i2 :: SBool
i2) -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ SBool -> Value
forall b w i. i -> GenValue b w i
VInteger (SBool -> Value) -> SBool -> Value
forall a b. (a -> b) -> a -> b
$ Bool -> SBool -> SBool -> SBool -> SBool
mergeInteger Bool
f SBool
c SBool
i1 SBool
i2
    (VWord n1 :: Integer
n1 w1 :: Eval (WordValue SBool SBool SBool)
w1, VWord n2 :: Integer
n2 w2 :: Eval (WordValue SBool SBool SBool)
w2 ) | Integer
n1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n2 -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Integer -> Eval (WordValue SBool SBool SBool) -> Value
forall b w i. Integer -> Eval (WordValue b w i) -> GenValue b w i
VWord Integer
n1 (Eval (WordValue SBool SBool SBool) -> Value)
-> Eval (WordValue SBool SBool SBool) -> Value
forall a b. (a -> b) -> a -> b
$ Bool
-> SBool
-> Eval (WordValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
-> Eval (WordValue SBool SBool SBool)
mergeWord' Bool
f SBool
c Eval (WordValue SBool SBool SBool)
w1 Eval (WordValue SBool SBool SBool)
w2
    (VSeq n1 :: Integer
n1 vs1 :: SeqMap SBool SBool SBool
vs1, VSeq n2 :: Integer
n2 vs2 :: SeqMap SBool SBool SBool
vs2 ) | Integer
n1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n2 -> Integer -> SeqMap SBool SBool SBool -> Value
forall b w i. Integer -> SeqMap b w i -> GenValue b w i
VSeq Integer
n1 (SeqMap SBool SBool SBool -> Value)
-> Eval (SeqMap SBool SBool SBool) -> Eval Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
memoMap (Bool
-> SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
mergeSeqMap Bool
f SBool
c SeqMap SBool SBool SBool
vs1 SeqMap SBool SBool SBool
vs2)
    (VStream vs1 :: SeqMap SBool SBool SBool
vs1, VStream vs2 :: SeqMap SBool SBool SBool
vs2) -> SeqMap SBool SBool SBool -> Value
forall b w i. SeqMap b w i -> GenValue b w i
VStream (SeqMap SBool SBool SBool -> Value)
-> Eval (SeqMap SBool SBool SBool) -> Eval Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqMap SBool SBool SBool -> Eval (SeqMap SBool SBool SBool)
forall b w i. SeqMap b w i -> Eval (SeqMap b w i)
memoMap (Bool
-> SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
mergeSeqMap Bool
f SBool
c SeqMap SBool SBool SBool
vs1 SeqMap SBool SBool SBool
vs2)
    (VFun f1 :: Eval Value -> Eval Value
f1    , VFun f2 :: Eval Value -> Eval Value
f2    ) -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ (Eval Value -> Eval Value) -> Value
forall b w i.
(Eval (GenValue b w i) -> Eval (GenValue b w i)) -> GenValue b w i
VFun ((Eval Value -> Eval Value) -> Value)
-> (Eval Value -> Eval Value) -> Value
forall a b. (a -> b) -> a -> b
$ \x :: Eval Value
x -> Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
mergeValue' Bool
f SBool
c (Eval Value -> Eval Value
f1 Eval Value
x) (Eval Value -> Eval Value
f2 Eval Value
x)
    (VPoly f1 :: TValue -> Eval Value
f1   , VPoly f2 :: TValue -> Eval Value
f2   ) -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ (TValue -> Eval Value) -> Value
forall b w i. (TValue -> Eval (GenValue b w i)) -> GenValue b w i
VPoly ((TValue -> Eval Value) -> Value)
-> (TValue -> Eval Value) -> Value
forall a b. (a -> b) -> a -> b
$ \x :: TValue
x -> Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
mergeValue' Bool
f SBool
c (TValue -> Eval Value
f1 TValue
x) (TValue -> Eval Value
f2 TValue
x)
    (_          , _          ) -> String -> [String] -> Eval Value
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.Symbolic.Value"
                                  [ "mergeValue: incompatible values" ]
  where
    mergeField :: (a, Eval Value) -> (a, Eval Value) -> (a, Eval Value)
mergeField (n1 :: a
n1, x1 :: Eval Value
x1) (n2 :: a
n2, x2 :: Eval Value
x2)
      | a
n1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n2  = (a
n1, Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
mergeValue' Bool
f SBool
c Eval Value
x1 Eval Value
x2)
      | Bool
otherwise = String -> [String] -> (a, Eval Value)
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.Symbolic.Value"
                    [ "mergeValue.mergeField: incompatible values" ]

mergeValue' :: Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
mergeValue' :: Bool -> SBool -> Eval Value -> Eval Value -> Eval Value
mergeValue' f :: Bool
f c :: SBool
c x1 :: Eval Value
x1 x2 :: Eval Value
x2 =
  do Value
v1 <- Eval Value
x1
     Value
v2 <- Eval Value
x2
     Bool -> SBool -> Value -> Value -> Eval Value
mergeValue Bool
f SBool
c Value
v1 Value
v2

mergeSeqMap :: Bool -> SBool -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger -> SeqMap SBool SWord SInteger
mergeSeqMap :: Bool
-> SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
-> SeqMap SBool SBool SBool
mergeSeqMap f :: Bool
f c :: SBool
c x :: SeqMap SBool SBool SBool
x y :: SeqMap SBool SBool SBool
y =
  (Integer -> Eval Value) -> SeqMap SBool SBool SBool
forall b w i. (Integer -> Eval (GenValue b w i)) -> SeqMap b w i
IndexSeqMap ((Integer -> Eval Value) -> SeqMap SBool SBool SBool)
-> (Integer -> Eval Value) -> SeqMap SBool SBool SBool
forall a b. (a -> b) -> a -> b
$ \i :: Integer
i ->
  do Value
xi <- SeqMap SBool SBool SBool -> Integer -> Eval Value
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap SBool SBool SBool
x Integer
i
     Value
yi <- SeqMap SBool SBool SBool -> Integer -> Eval Value
forall b w i. SeqMap b w i -> Integer -> Eval (GenValue b w i)
lookupSeqMap SeqMap SBool SBool SBool
y Integer
i
     Bool -> SBool -> Value -> Value -> Eval Value
mergeValue Bool
f SBool
c Value
xi Value
yi

-- Symbolic Big-endian Words -------------------------------------------------------

instance BitWord SBool SWord SInteger where
  wordLen :: SBool -> Integer
wordLen v :: SBool
v = Int -> Integer
forall a. Integral a => a -> Integer
toInteger (SBool -> Int
forall a. HasKind a => a -> Int
intSizeOf SBool
v)
  wordAsChar :: SBool -> Maybe Char
wordAsChar v :: SBool
v = Integer -> Char
integerToChar (Integer -> Char) -> Maybe Integer -> Maybe Char
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBool -> Maybe Integer
svAsInteger SBool
v

  ppBit :: SBool -> Doc
ppBit v :: SBool
v
     | Just b :: Bool
b <- SBool -> Maybe Bool
svAsBool SBool
v = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$! if Bool
b then "True" else "False"
     | Bool
otherwise            = String -> Doc
text "?"
  ppWord :: PPOpts -> SBool -> Doc
ppWord opts :: PPOpts
opts v :: SBool
v
     | Just x :: Integer
x <- SBool -> Maybe Integer
svAsInteger SBool
v = PPOpts -> BV -> Doc
ppBV PPOpts
opts (Integer -> Integer -> BV
BV (SBool -> Integer
forall b w i. BitWord b w i => w -> Integer
wordLen SBool
v) Integer
x)
     | Bool
otherwise               = String -> Doc
text "[?]"
  ppInteger :: PPOpts -> SBool -> Doc
ppInteger _opts :: PPOpts
_opts v :: SBool
v
     | Just x :: Integer
x <- SBool -> Maybe Integer
svAsInteger SBool
v = Integer -> Doc
integer Integer
x
     | Bool
otherwise               = String -> Doc
text "[?]"

  bitLit :: Bool -> SBool
bitLit b :: Bool
b    = Bool -> SBool
svBool Bool
b
  wordLit :: Integer -> Integer -> SBool
wordLit n :: Integer
n x :: Integer
x = Kind -> Integer -> SBool
svInteger (Bool -> Int -> Kind
KBounded Bool
False (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)) Integer
x
  integerLit :: Integer -> SBool
integerLit x :: Integer
x = Kind -> Integer -> SBool
svInteger Kind
KUnbounded Integer
x

  wordBit :: SBool -> Integer -> SBool
wordBit x :: SBool
x idx :: Integer
idx = SBool -> Int -> SBool
svTestBit SBool
x (SBool -> Int
forall a. HasKind a => a -> Int
intSizeOf SBool
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
idx)

  wordUpdate :: SBool -> Integer -> SBool -> SBool
wordUpdate x :: SBool
x idx :: Integer
idx b :: SBool
b = Kind -> Bool -> SBool -> SBool -> SBool -> SBool
svSymbolicMerge (SBool -> Kind
forall a. HasKind a => a -> Kind
kindOf SBool
x) Bool
False SBool
b SBool
wtrue SBool
wfalse
    where
     i' :: Int
i' = SBool -> Int
forall a. HasKind a => a -> Int
intSizeOf SBool
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
idx
     wtrue :: SBool
wtrue  = SBool
x SBool -> SBool -> SBool
`svOr`  Kind -> Integer -> SBool
svInteger (SBool -> Kind
forall a. HasKind a => a -> Kind
kindOf SBool
x) (Int -> Integer
forall a. Bits a => Int -> a
bit Int
i' :: Integer)
     wfalse :: SBool
wfalse = SBool
x SBool -> SBool -> SBool
`svAnd` Kind -> Integer -> SBool
svInteger (SBool -> Kind
forall a. HasKind a => a -> Kind
kindOf SBool
x) (Integer -> Integer
forall a. Bits a => a -> a
complement (Int -> Integer
forall a. Bits a => Int -> a
bit Int
i' :: Integer))

  packWord :: [SBool] -> SBool
packWord bs :: [SBool]
bs = [SBool] -> SBool
fromBitsLE ([SBool] -> [SBool]
forall a. [a] -> [a]
reverse [SBool]
bs)
  unpackWord :: SBool -> [SBool]
unpackWord x :: SBool
x = [ SBool -> Int -> SBool
svTestBit SBool
x Int
i | Int
i <- [Int] -> [Int]
forall a. [a] -> [a]
reverse [0 .. SBool -> Int
forall a. HasKind a => a -> Int
intSizeOf SBool
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1] ]

  joinWord :: SBool -> SBool -> SBool
joinWord x :: SBool
x y :: SBool
y = SBool -> SBool -> SBool
svJoin SBool
x SBool
y

  splitWord :: Integer -> Integer -> SBool -> (SBool, SBool)
splitWord _leftW :: Integer
_leftW rightW :: Integer
rightW w :: SBool
w =
    ( Int -> Int -> SBool -> SBool
svExtract (SBool -> Int
forall a. HasKind a => a -> Int
intSizeOf SBool
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
rightW) SBool
w
    , Int -> Int -> SBool -> SBool
svExtract (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
rightW Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) 0 SBool
w
    )

  extractWord :: Integer -> Integer -> SBool -> SBool
extractWord len :: Integer
len start :: Integer
start w :: SBool
w =
    Int -> Int -> SBool -> SBool
svExtract (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
start) SBool
w

  wordPlus :: SBool -> SBool -> SBool
wordPlus  = SBool -> SBool -> SBool
svPlus
  wordMinus :: SBool -> SBool -> SBool
wordMinus = SBool -> SBool -> SBool
svMinus
  wordMult :: SBool -> SBool -> SBool
wordMult  = SBool -> SBool -> SBool
svTimes

  intPlus :: SBool -> SBool -> SBool
intPlus  = SBool -> SBool -> SBool
svPlus
  intMinus :: SBool -> SBool -> SBool
intMinus = SBool -> SBool -> SBool
svMinus
  intMult :: SBool -> SBool -> SBool
intMult  = SBool -> SBool -> SBool
svTimes

  intModPlus :: Integer -> SBool -> SBool -> SBool
intModPlus  _m :: Integer
_m = SBool -> SBool -> SBool
svPlus
  intModMinus :: Integer -> SBool -> SBool -> SBool
intModMinus _m :: Integer
_m = SBool -> SBool -> SBool
svMinus
  intModMult :: Integer -> SBool -> SBool -> SBool
intModMult  _m :: Integer
_m = SBool -> SBool -> SBool
svTimes

  wordToInt :: SBool -> SBool
wordToInt = SBool -> SBool
svToInteger
  wordFromInt :: Integer -> SBool -> SBool
wordFromInt = Integer -> SBool -> SBool
svFromInteger

-- TODO: implement this properly in SBV using "bv2int"
svToInteger :: SWord -> SInteger
svToInteger :: SBool -> SBool
svToInteger w :: SBool
w =
  case SBool -> Maybe Integer
svAsInteger SBool
w of
    Nothing -> Kind -> SBool -> SBool
svFromIntegral Kind
KUnbounded SBool
w
    Just x :: Integer
x  -> Kind -> Integer -> SBool
svInteger Kind
KUnbounded Integer
x

-- TODO: implement this properly in SBV using "int2bv"
svFromInteger :: Integer -> SInteger -> SWord
svFromInteger :: Integer -> SBool -> SBool
svFromInteger 0 _ = Int -> Integer -> SBool
literalSWord 0 0
svFromInteger n :: Integer
n i :: SBool
i =
  case SBool -> Maybe Integer
svAsInteger SBool
i of
    Nothing -> Kind -> SBool -> SBool
svFromIntegral (Bool -> Int -> Kind
KBounded Bool
False (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n)) SBool
i
    Just x :: Integer
x  -> Int -> Integer -> SBool
literalSWord (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) Integer
x

-- Errors ----------------------------------------------------------------------

evalPanic :: String -> [String] -> a
evalPanic :: String -> [String] -> a
evalPanic cxt :: String
cxt = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic ("[Symbolic]" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cxt)