-- | This file is almost exactly the same as crucible-c/src/Model.hs

{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language Rank2Types #-}
{-# Language TypeFamilies #-}
{-# Language TypeApplications #-}
{-# Language TypeOperators #-}
{-# Language ScopedTypeVariables #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module Crux.Model where

import           Data.BitVector.Sized (BV)
import qualified Data.BitVector.Sized as BV
import           Data.Maybe (fromMaybe)
import qualified Data.Parameterized.Map as MapF
import qualified Numeric as N
import           LibBF (BigFloat)
import qualified LibBF as BF

import           Lang.Crucible.Types

import           Crux.UI.JS
import           Crux.Types


emptyModelView :: ModelView
emptyModelView :: ModelView
emptyModelView = MapF BaseTypeRepr Vals -> ModelView
ModelView (MapF BaseTypeRepr Vals -> ModelView)
-> MapF BaseTypeRepr Vals -> ModelView
forall a b. (a -> b) -> a -> b
$ MapF BaseTypeRepr Vals
forall {v} (k :: v -> *) (a :: v -> *). MapF k a
MapF.empty

--------------------------------------------------------------------------------

toDouble :: Rational -> Double
toDouble :: Rational -> Double
toDouble = Rational -> Double
forall a. Fractional a => Rational -> a
fromRational


showBVLiteral :: (1 <= w) => NatRepr w -> BV w -> String
showBVLiteral :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> String
showBVLiteral NatRepr w
w BV w
bv =
    (if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then String
"-0x" else String
"0x") String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String -> String
forall a. Integral a => a -> String -> String
N.showHex Integer
i (if NatRepr w -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
64 then String
"L" else String
"")
  where
  x :: Integer
x = NatRepr w -> BV w -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned NatRepr w
w BV w
bv
  i :: Integer
i = Integer -> Integer
forall a. Num a => a -> a
abs Integer
x

showFloatLiteral :: BigFloat -> String
showFloatLiteral :: BigFloat -> String
showFloatLiteral BigFloat
x
   | BigFloat -> Bool
BF.bfIsNaN BigFloat
x     = String
"NAN"
   | BigFloat -> Bool
BF.bfIsInf BigFloat
x     = if BigFloat -> Bool
BF.bfIsNeg BigFloat
x then String
"-INFINITY" else String
"INFINITY"
   | BigFloat -> Bool
BF.bfIsZero BigFloat
x    = if BigFloat -> Bool
BF.bfIsNeg BigFloat
x then String
"-0.0f" else String
"0.0f"
                                               -- NB, 24 bits of precision for float
   | Bool
otherwise        = Int -> ShowFmt -> BigFloat -> String
BF.bfToString Int
16 (Maybe Word -> ShowFmt
BF.showFree (Word -> Maybe Word
forall a. a -> Maybe a
Just Word
24) ShowFmt -> ShowFmt -> ShowFmt
forall a. Semigroup a => a -> a -> a
<> ShowFmt
BF.addPrefix) BigFloat
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"f"

showDoubleLiteral :: BigFloat -> String
showDoubleLiteral :: BigFloat -> String
showDoubleLiteral BigFloat
x
   | BigFloat -> Bool
BF.bfIsNaN BigFloat
x     = String
"(double) NAN"
   | BigFloat -> Bool
BF.bfIsInf BigFloat
x     = if BigFloat -> Bool
BF.bfIsNeg BigFloat
x then String
"- ((double) INFINITY)" else String
"(double) INFINITY"
   | BigFloat -> Bool
BF.bfIsZero BigFloat
x    = if BigFloat -> Bool
BF.bfIsNeg BigFloat
x then String
"-0.0" else String
"0.0"
                                               -- NB, 53 bits of precision for double
   | Bool
otherwise        = Int -> ShowFmt -> BigFloat -> String
BF.bfToString Int
16 (Maybe Word -> ShowFmt
BF.showFree (Word -> Maybe Word
forall a. a -> Maybe a
Just Word
53) ShowFmt -> ShowFmt -> ShowFmt
forall a. Semigroup a => a -> a -> a
<> ShowFmt
BF.addPrefix) BigFloat
x

valsJS :: BaseTypeRepr ty -> Vals ty -> IO [JS]
valsJS :: forall (ty :: BaseType). BaseTypeRepr ty -> Vals ty -> IO [JS]
valsJS BaseTypeRepr ty
ty (Vals [Entry (GroundValue ty)]
xs) =
  let showEnt :: Entry (GroundValue ty) -> IO JS
showEnt = case BaseTypeRepr ty
ty of
        BaseBVRepr NatRepr w
n -> (BV w -> String) -> NatRepr w -> Entry (BV w) -> IO JS
forall b a. Show b => (a -> String) -> b -> Entry a -> IO JS
showEnt' (NatRepr w -> BV w -> String
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> String
showBVLiteral NatRepr w
n) NatRepr w
n
        BaseFloatRepr (FloatingPointPrecisionRepr NatRepr eb
eb NatRepr sb
sb)
          | Just eb :~: 8
Refl <- NatRepr eb -> NatRepr 8 -> Maybe (eb :~: 8)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr eb
eb (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8)
          , Just sb :~: 24
Refl <- NatRepr sb -> NatRepr 24 -> Maybe (sb :~: 24)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr sb
sb (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @24)
          -> (BigFloat -> String) -> Int -> Entry BigFloat -> IO JS
forall b a. Show b => (a -> String) -> b -> Entry a -> IO JS
showEnt' BigFloat -> String
showFloatLiteral (Int
32 :: Int)
        BaseFloatRepr (FloatingPointPrecisionRepr NatRepr eb
eb NatRepr sb
sb)
          | Just eb :~: 11
Refl <- NatRepr eb -> NatRepr 11 -> Maybe (eb :~: 11)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr eb
eb (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @11)
          , Just sb :~: 53
Refl <- NatRepr sb -> NatRepr 53 -> Maybe (sb :~: 53)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr sb
sb (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @53)
          -> (BigFloat -> String) -> Int -> Entry BigFloat -> IO JS
forall b a. Show b => (a -> String) -> b -> Entry a -> IO JS
showEnt' BigFloat -> String
showDoubleLiteral (Int
64 :: Int)
        BaseTypeRepr ty
BaseRealRepr -> (Rational -> String) -> NatRepr 64 -> Entry Rational -> IO JS
forall b a. Show b => (a -> String) -> b -> Entry a -> IO JS
showEnt' (Double -> String
forall a. Show a => a -> String
show (Double -> String) -> (Rational -> Double) -> Rational -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
toDouble) (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64)
        BaseTypeRepr ty
_ -> String -> Entry (GroundValue ty) -> IO JS
forall a. HasCallStack => String -> a
error (String
"Type not implemented: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BaseTypeRepr ty -> String
forall a. Show a => a -> String
show BaseTypeRepr ty
ty)

  in (Entry (GroundValue ty) -> IO JS)
-> [Entry (GroundValue ty)] -> IO [JS]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Entry (GroundValue ty) -> IO JS
showEnt [Entry (GroundValue ty)]
xs

  where
  showEnt' :: Show b => (a -> String) -> b -> Entry a -> IO JS
  showEnt' :: forall b a. Show b => (a -> String) -> b -> Entry a -> IO JS
showEnt' a -> String
repr b
n Entry a
e =
    do JS
l <- JS -> Maybe JS -> JS
forall a. a -> Maybe a -> a
fromMaybe JS
jsNull (Maybe JS -> JS) -> IO (Maybe JS) -> IO JS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProgramLoc -> IO (Maybe JS)
jsLoc (Entry a -> ProgramLoc
forall a. Entry a -> ProgramLoc
entryLoc Entry a
e)
       JS -> IO JS
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (JS -> IO JS) -> JS -> IO JS
forall a b. (a -> b) -> a -> b
$ [(String, JS)] -> JS
jsObj
         [ String
"name" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> String -> JS
jsStr (Entry a -> String
forall a. Entry a -> String
entryName Entry a
e)
         , String
"loc"  String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> JS
l
         , String
"val"  String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> String -> JS
jsStr (a -> String
repr (Entry a -> a
forall a. Entry a -> a
entryValue Entry a
e))
         , String
"bits" String -> JS -> (String, JS)
forall a b. a -> b -> (a, b)
~> String -> JS
jsStr (b -> String
forall a. Show a => a -> String
show b
n)
         ]

modelJS :: ModelView -> IO JS
modelJS :: ModelView -> IO JS
modelJS ModelView
m =
  [JS] -> JS
jsList ([JS] -> JS) -> ([[JS]] -> [JS]) -> [[JS]] -> JS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[JS]] -> [JS]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[JS]] -> JS) -> IO [[JS]] -> IO JS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [IO [JS]] -> IO [[JS]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ((forall (s :: BaseType).
 BaseTypeRepr s -> Vals s -> [IO [JS]] -> [IO [JS]])
-> [IO [JS]] -> MapF BaseTypeRepr Vals -> [IO [JS]]
forall {v} (k :: v -> *) (a :: v -> *) b.
(forall (s :: v). k s -> a s -> b -> b) -> b -> MapF k a -> b
MapF.foldrWithKey (\BaseTypeRepr s
k Vals s
v [IO [JS]]
xs -> BaseTypeRepr s -> Vals s -> IO [JS]
forall (ty :: BaseType). BaseTypeRepr ty -> Vals ty -> IO [JS]
valsJS BaseTypeRepr s
k Vals s
v IO [JS] -> [IO [JS]] -> [IO [JS]]
forall a. a -> [a] -> [a]
: [IO [JS]]
xs) [] (ModelView -> MapF BaseTypeRepr Vals
modelVals ModelView
m))