Language.Fortran.Model.Repr.Prim

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!

Types

data IntRepr a

Constructors

MachineInt

ArbitraryInt

Instances

Eq (IntRepr a)

Defined in Language.Fortran.Model.Repr.Prim

Methods

(==) :: IntRepr a -> IntRepr a -> Bool

(/=) :: IntRepr a -> IntRepr a -> Bool

Ord (IntRepr a)

Defined in Language.Fortran.Model.Repr.Prim

Methods

compare :: IntRepr a -> IntRepr a -> Ordering

(<) :: IntRepr a -> IntRepr a -> Bool

(<=) :: IntRepr a -> IntRepr a -> Bool

(>) :: IntRepr a -> IntRepr a -> Bool

(>=) :: IntRepr a -> IntRepr a -> Bool

max :: IntRepr a -> IntRepr a -> IntRepr a

min :: IntRepr a -> IntRepr a -> IntRepr a

Show (IntRepr a)

Defined in Language.Fortran.Model.Repr.Prim

Methods

showsPrec :: Int -> IntRepr a -> ShowS

show :: IntRepr a -> String

showList :: [IntRepr a] -> ShowS

data RealRepr a

Constructors

MachineFloat

ArbitraryReal

Instances

Eq (RealRepr a)

Defined in Language.Fortran.Model.Repr.Prim

Methods

(==) :: RealRepr a -> RealRepr a -> Bool

(/=) :: RealRepr a -> RealRepr a -> Bool

Ord (RealRepr a)

Defined in Language.Fortran.Model.Repr.Prim

Methods

compare :: RealRepr a -> RealRepr a -> Ordering

(<) :: RealRepr a -> RealRepr a -> Bool

(<=) :: RealRepr a -> RealRepr a -> Bool

(>) :: RealRepr a -> RealRepr a -> Bool

(>=) :: RealRepr a -> RealRepr a -> Bool

max :: RealRepr a -> RealRepr a -> RealRepr a

min :: RealRepr a -> RealRepr a -> RealRepr a

Show (RealRepr a)

Defined in Language.Fortran.Model.Repr.Prim

Methods

showsPrec :: Int -> RealRepr a -> ShowS

show :: RealRepr a -> String

showList :: [RealRepr a] -> ShowS

data BoolRepr a

Constructors

IntBool

BitBool

Instances

Eq (BoolRepr a)

Defined in Language.Fortran.Model.Repr.Prim

Methods

(==) :: BoolRepr a -> BoolRepr a -> Bool

(/=) :: BoolRepr a -> BoolRepr a -> Bool

Ord (BoolRepr a)

Defined in Language.Fortran.Model.Repr.Prim

Methods

compare :: BoolRepr a -> BoolRepr a -> Ordering

(<) :: BoolRepr a -> BoolRepr a -> Bool

(<=) :: BoolRepr a -> BoolRepr a -> Bool

(>) :: BoolRepr a -> BoolRepr a -> Bool

(>=) :: BoolRepr a -> BoolRepr a -> Bool

max :: BoolRepr a -> BoolRepr a -> BoolRepr a

min :: BoolRepr a -> BoolRepr a -> BoolRepr a

Show (BoolRepr a)

Defined in Language.Fortran.Model.Repr.Prim

Methods

showsPrec :: Int -> BoolRepr a -> ShowS

show :: BoolRepr a -> String

showList :: [BoolRepr a] -> ShowS

data PrimReprHandler a

Constructors

PrimReprHandler

Fields

• _prhKind :: !Kind
• _prhLiteral :: !(a -> SVal)
• _prhSymbolic :: !(String -> Symbolic SVal)

data PrimReprSpec

Constructors

PrimReprSpec

Fields

• _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

prhSymbolic :: forall a. Lens' (PrimReprHandler a) (String -> Symbolic SVal)

prhLiteral :: forall a a. Lens (PrimReprHandler a) (PrimReprHandler a) (a -> SVal) (a -> SVal)

prhKind :: forall a. Lens' (PrimReprHandler a) Kind

prsInt8Repr :: Lens' PrimReprSpec (IntRepr Int8)

prsInt64Repr :: Lens' PrimReprSpec (IntRepr Int64)

prsInt32Repr :: Lens' PrimReprSpec (IntRepr Int32)

prsInt16Repr :: Lens' PrimReprSpec (IntRepr Int16)

prsFloatRepr :: Lens' PrimReprSpec (RealRepr Float)

prsDoubleRepr :: Lens' PrimReprSpec (RealRepr Double)

prsBool8Repr :: Lens' PrimReprSpec (BoolRepr Bool8)

prsBool64Repr :: Lens' PrimReprSpec (BoolRepr Bool64)

prsBool32Repr :: Lens' PrimReprSpec (BoolRepr Bool32)

prsBool16Repr :: Lens' PrimReprSpec (BoolRepr Bool16)

Standard specs

prsPrecise :: PrimReprSpec

prsIdealized :: PrimReprSpec

prsWithArbitraryInts :: Bool -> PrimReprSpec -> PrimReprSpec

prsWithArbitraryReals :: Bool -> PrimReprSpec -> PrimReprSpec

Using specs

makeSymRepr :: PrimReprSpec -> Prim p k a -> PrimReprHandler a

Monadic Accessors

class HasPrimReprHandlers r where

Minimal complete definition

Nothing

Methods

primReprHandlers :: r -> PrimReprHandlers

primReprHandler :: r -> Prim p k a -> PrimReprHandler a

Instances

HasPrimReprHandlers PrimReprHandlers

Defined in Language.Fortran.Model.Repr.Prim

Methods

primReprHandlers :: PrimReprHandlers -> PrimReprHandlers

primReprHandler :: forall (p :: Precision) (k :: BasicType) a. PrimReprHandlers -> Prim p k a -> PrimReprHandler a

newtype PrimReprHandlers

Constructors

PrimReprHandlers

Fields

• unPrimReprHandlers :: forall p k a. Prim p k a -> PrimReprHandler a

Instances

HasPrimReprHandlers PrimReprHandlers

Defined in Language.Fortran.Model.Repr.Prim

Methods

primReprHandlers :: PrimReprHandlers -> PrimReprHandlers

primReprHandler :: forall (p :: Precision) (k :: BasicType) a. PrimReprHandlers -> Prim p k a -> PrimReprHandler a

primSBVKind :: (MonadReader r m, HasPrimReprHandlers r) => Prim p k a -> m Kind

primLit :: (MonadReader r m, HasPrimReprHandlers r) => Prim p k a -> a -> m SVal

primSymbolic :: (MonadReader r m, HasPrimReprHandlers r) => Prim p k a -> String -> m (Symbolic SVal)