{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# OPTIONS_GHC -Wall #-} {-| = Handling primitive Fortran values symbolically. There are a few challenges that this module attempts to solve: Fortran uses fixed-width machine integers and floating point reals. Sometimes we might want to reason about these directly (which is supported by SBV and therefore feasible). However, sometimes they get in the way of the logic and we just want to pretend that they're the pure mathematical values that they approximate. For example floating point addition obeys very few algebraic laws, so most theorems about real numbers don't hold at all for floating point numbers. In addition, Fortran's boolean values are actually arbitrary signed integers. If we treat all boolean values symbolically as bit-vectors, logic can become very slow; so it might be best to pretend that all booleans are single bits. However, sometimes we might want to verify properties that rely on the actual bit-vector representation of booleans. This module deals with these problems by abstracting over the choices: the user should be able to choose which representation they want to use for each primitive data type. The user provides a 'PrimReprSpec' which specifies how each data type should be treated. Some examples are provided: 'prsPrecise' treats all values precisely as they are represented in the Fortran program. This makes logic slow and makes it very difficult to prove many things, but it is most accurate. On the other hand, 'prsIdealized' treats all values as their idealized mathematical equivalents. This makes logic fast and lots intuitive properties can be proved easily. However, these properties often will not hold in actual running Fortran programs: sometimes in weird edge cases and sometimes in sensible-seeming executions. It would be interesting future work to provide an analysis that helps to determine which of the two applies to a particular program! -} module Language.Fortran.Model.Repr.Prim where import Data.Int (Int16, Int32, Int64, Int8) import Data.Word (Word8) import Control.Lens import Control.Monad.Reader (MonadReader (..)) import qualified Data.SBV as SBV import Data.SBV.Dynamic (SVal) import Data.SBV.Internals (SBV (..)) import Language.Fortran.Model.Types -------------------------------------------------------------------------------- -- * Types data IntRepr a = MachineInt | ArbitraryInt deriving (Eq, Ord, Show) data RealRepr a = MachineFloat | ArbitraryReal deriving (Eq, Ord, Show) data BoolRepr a = IntBool | BitBool deriving (Eq, Ord, Show) data PrimReprHandler a = PrimReprHandler { _prhKind :: !SBV.Kind , _prhLiteral :: !(a -> SVal) , _prhSymbolic :: !(String -> SBV.Symbolic SVal) } data PrimReprSpec = PrimReprSpec { _prsInt8Repr :: !(IntRepr Int8) , _prsInt16Repr :: !(IntRepr Int16) , _prsInt32Repr :: !(IntRepr Int32) , _prsInt64Repr :: !(IntRepr Int64) , _prsFloatRepr :: !(RealRepr Float) , _prsDoubleRepr :: !(RealRepr Double) , _prsBool8Repr :: !(BoolRepr Bool8) , _prsBool16Repr :: !(BoolRepr Bool16) , _prsBool32Repr :: !(BoolRepr Bool32) , _prsBool64Repr :: !(BoolRepr Bool64) } -------------------------------------------------------------------------------- -- ** Lenses makeLenses ''PrimReprHandler makeLenses ''PrimReprSpec -------------------------------------------------------------------------------- -- * Standard specs prsPrecise :: PrimReprSpec prsPrecise = PrimReprSpec { _prsInt8Repr = MachineInt , _prsInt16Repr = MachineInt , _prsInt32Repr = MachineInt , _prsInt64Repr = MachineInt , _prsFloatRepr = MachineFloat , _prsDoubleRepr = MachineFloat , _prsBool8Repr = IntBool , _prsBool16Repr = IntBool , _prsBool32Repr = IntBool , _prsBool64Repr = IntBool } prsIdealized :: PrimReprSpec prsIdealized = PrimReprSpec { _prsInt8Repr = ArbitraryInt , _prsInt16Repr = ArbitraryInt , _prsInt32Repr = ArbitraryInt , _prsInt64Repr = ArbitraryInt , _prsFloatRepr = ArbitraryReal , _prsDoubleRepr = ArbitraryReal , _prsBool8Repr = BitBool , _prsBool16Repr = BitBool , _prsBool32Repr = BitBool , _prsBool64Repr = BitBool } prsWithArbitraryInts :: Bool -> PrimReprSpec -> PrimReprSpec prsWithArbitraryInts useArbitrary | useArbitrary = set prsInt8Repr ArbitraryInt . set prsInt16Repr ArbitraryInt . set prsInt32Repr ArbitraryInt . set prsInt64Repr ArbitraryInt | otherwise = set prsInt8Repr MachineInt . set prsInt16Repr MachineInt . set prsInt32Repr MachineInt . set prsInt64Repr MachineInt prsWithArbitraryReals :: Bool -> PrimReprSpec -> PrimReprSpec prsWithArbitraryReals useArbitrary | useArbitrary = set prsFloatRepr ArbitraryReal . set prsDoubleRepr ArbitraryReal | otherwise = set prsFloatRepr MachineFloat . set prsDoubleRepr MachineFloat -------------------------------------------------------------------------------- -- * Using specs makeSymRepr :: PrimReprSpec -> Prim p k a -> PrimReprHandler a makeSymRepr spec = \case PInt8 -> intRepr prsInt8Repr PInt16 -> intRepr prsInt16Repr PInt32 -> intRepr prsInt32Repr PInt64 -> intRepr prsInt64Repr PFloat -> realRepr prsFloatRepr PDouble -> realRepr prsDoubleRepr PBool8 -> boolRepr getBool8 prsBool8Repr PBool16 -> boolRepr getBool16 prsBool16Repr PBool32 -> boolRepr getBool32 prsBool32Repr PBool64 -> boolRepr getBool64 prsBool64Repr PChar -> bySymWord (0 :: Word8) getChar8 where intRepr :: (Integral a, SBV.SymWord a) => Lens' PrimReprSpec (IntRepr a) -> PrimReprHandler a intRepr l = case spec ^. l of MachineInt -> bySymWord 0 id ArbitraryInt -> bySymWord (0 :: Integer) fromIntegral realRepr :: (RealFloat a, SBV.SymWord a) => Lens' PrimReprSpec (RealRepr a) -> PrimReprHandler a realRepr l = case spec ^. l of MachineFloat -> bySymWord 0 id ArbitraryReal -> bySymWord (0 :: SBV.AlgReal) realToFrac boolRepr :: (Integral b, SBV.SymWord b) => (a -> b) -> Lens' PrimReprSpec (BoolRepr a) -> PrimReprHandler a boolRepr unwrap l = case spec ^. l of IntBool -> bySymWord 0 unwrap BitBool -> bySymWord (False :: Bool) (toBool . unwrap) bySymWord :: (SBV.SymWord b) => b -> (a -> b) -> PrimReprHandler a bySymWord (repValue :: b) fromPrim = PrimReprHandler { _prhKind = SBV.kindOf repValue , _prhLiteral = unSBV . SBV.literal . fromPrim , _prhSymbolic = fmap (unSBV :: SBV b -> SVal) . SBV.symbolic } toBool :: (Ord a, Num a) => a -> Bool toBool x = x > 0 -------------------------------------------------------------------------------- -- * Monadic Accessors class HasPrimReprHandlers r where primReprHandlers :: r -> PrimReprHandlers primReprHandlers env = PrimReprHandlers (primReprHandler env) primReprHandler :: r -> Prim p k a -> PrimReprHandler a primReprHandler = unPrimReprHandlers . primReprHandlers newtype PrimReprHandlers = PrimReprHandlers { unPrimReprHandlers :: forall p k a. Prim p k a -> PrimReprHandler a } instance HasPrimReprHandlers PrimReprHandlers where primReprHandlers = id primSBVKind :: (MonadReader r m, HasPrimReprHandlers r) => Prim p k a -> m SBV.Kind primSBVKind p = view (to (flip primReprHandler p) . prhKind) primLit :: (MonadReader r m, HasPrimReprHandlers r) => Prim p k a -> a -> m SVal primLit p a = do lit <- view (to (flip primReprHandler p) . prhLiteral) return (lit a) primSymbolic :: (MonadReader r m, HasPrimReprHandlers r) => Prim p k a -> String -> m (SBV.Symbolic SVal) primSymbolic p nm = do symbolic <- view (to (flip primReprHandler p) . prhSymbolic) return (symbolic nm)