Copyright	(c) Galois Inc 2014
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.Syntax

Contents

Booleans
Expression classes
Natural numbers
Real numbers
Complex real numbers
Maybe
Vector
Function handles
IdentValueMap
Structs
Multibyte operations

Description

This module provides typeclasses and combinators for constructing AST expressions.

Synopsis

class IsExpr (e :: CrucibleType -> Type) where
- type ExprExt (e :: CrucibleType -> Type)
- app :: forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp
- asApp :: forall (tp :: CrucibleType). e tp -> Maybe (App (ExprExt e) e tp)
- exprType :: forall (tp :: CrucibleType). e tp -> TypeRepr tp
eapp :: forall e (tp :: CrucibleType). IsExpr e => ExprExtension (ExprExt e) e tp -> e tp
asEapp :: forall e (tp :: CrucibleType). IsExpr e => e tp -> Maybe (ExprExtension (ExprExt e) e tp)
true :: IsExpr e => e BoolType
false :: IsExpr e => e BoolType
notExpr :: IsExpr e => e BoolType -> e BoolType
(.&&) :: IsExpr e => e BoolType -> e BoolType -> e BoolType
(.||) :: IsExpr e => e BoolType -> e BoolType -> e BoolType
class EqExpr (e :: CrucibleType -> Type) (tp :: CrucibleType) where
- (.==) :: e tp -> e tp -> e BoolType
- (./=) :: e tp -> e tp -> e BoolType
class EqExpr e tp => OrdExpr (e :: CrucibleType -> Type) (tp :: CrucibleType) where
- (.<) :: e tp -> e tp -> e BoolType
- (.<=) :: e tp -> e tp -> e BoolType
- (.>) :: e tp -> e tp -> e BoolType
- (.>=) :: e tp -> e tp -> e BoolType
class NumExpr (e :: CrucibleType -> Type) (tp :: CrucibleType) where
- (.+) :: e tp -> e tp -> e tp
- (.-) :: e tp -> e tp -> e tp
- (.*) :: e tp -> e tp -> e tp
class LitExpr (e :: CrucibleType -> Type) (tp :: CrucibleType) ty | tp -> ty where
- litExpr :: ty -> e tp
class ConvertableToNat (e :: CrucibleType -> Type) (tp :: CrucibleType) where
- toNat :: e tp -> e NatType
rationalLit :: IsExpr e => Rational -> e RealValType
natToReal :: IsExpr e => e NatType -> e RealValType
integerToReal :: IsExpr e => e IntegerType -> e RealValType
realToCplx :: IsExpr e => e RealValType -> e ComplexRealType
imagToCplx :: IsExpr e => e RealValType -> e ComplexRealType
realPart :: IsExpr e => e ComplexRealType -> e RealValType
imagPart :: IsExpr e => e ComplexRealType -> e RealValType
realLit :: IsExpr e => Rational -> e ComplexRealType
imagLit :: IsExpr e => Rational -> e ComplexRealType
natToCplx :: IsExpr e => e NatType -> e ComplexRealType
nothingValue :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e (MaybeType tp)
justValue :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e tp -> e (MaybeType tp)
vectorSize :: forall e (tp :: CrucibleType). IsExpr e => e (VectorType tp) -> e NatType
vectorLit :: forall e (tp :: CrucibleType). IsExpr e => TypeRepr tp -> Vector (e tp) -> e (VectorType tp)
vectorGetEntry :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e (VectorType tp) -> e NatType -> e tp
vectorSetEntry :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e (VectorType tp) -> e NatType -> e tp -> e (VectorType tp)
vectorIsEmpty :: forall e (tp :: CrucibleType). IsExpr e => e (VectorType tp) -> e BoolType
vecReplicate :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e NatType -> e tp -> e (VectorType tp)
closure :: forall e (tp :: CrucibleType) (ret :: CrucibleType) (args :: Ctx CrucibleType). (IsExpr e, KnownRepr TypeRepr tp, KnownRepr TypeRepr ret, KnownCtx TypeRepr args) => e (FunctionHandleType (args ::> tp) ret) -> e tp -> e (FunctionHandleType args ret)
emptyIdentValueMap :: forall (tp :: CrucibleType) e. (KnownRepr TypeRepr tp, IsExpr e) => e (StringMapType tp)
setIdentValue :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e (StringMapType tp) -> Text -> e (MaybeType tp) -> e (StringMapType tp)
mkStruct :: forall e (ctx :: Ctx CrucibleType). IsExpr e => CtxRepr ctx -> Assignment e ctx -> e (StructType ctx)
getStruct :: forall e (ctx :: Ctx CrucibleType) (tp :: CrucibleType). IsExpr e => Index ctx tp -> e (StructType ctx) -> e tp
setStruct :: forall e (ctx :: Ctx CrucibleType) (tp :: CrucibleType). IsExpr e => CtxRepr ctx -> e (StructType ctx) -> Index ctx tp -> e tp -> e (StructType ctx)
concatExprs :: forall (w :: Natural) a expr. (IsExpr expr, 1 <= w) => NatRepr w -> [expr (BVType w)] -> (forall (w' :: Natural). 1 <= w' => NatRepr w' -> expr (BVType w') -> a) -> a
bigEndianLoad :: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) => NatRepr addrWidth -> NatRepr cellWidth -> NatRepr valWidth -> Int -> expr (BVType addrWidth) -> expr (WordMapType addrWidth (BaseBVType cellWidth)) -> expr (BVType valWidth)
bigEndianLoadDef :: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) => NatRepr addrWidth -> NatRepr cellWidth -> NatRepr valWidth -> Int -> expr (BVType addrWidth) -> expr (WordMapType addrWidth (BaseBVType cellWidth)) -> expr (BVType cellWidth) -> expr (BVType valWidth)
bigEndianStore :: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) => NatRepr addrWidth -> NatRepr cellWidth -> NatRepr valWidth -> Int -> expr (BVType addrWidth) -> expr (BVType valWidth) -> expr (WordMapType addrWidth (BaseBVType cellWidth)) -> expr (WordMapType addrWidth (BaseBVType cellWidth))
littleEndianLoad :: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) => NatRepr addrWidth -> NatRepr cellWidth -> NatRepr valWidth -> Int -> expr (BVType addrWidth) -> expr (WordMapType addrWidth (BaseBVType cellWidth)) -> expr (BVType valWidth)
littleEndianLoadDef :: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) => NatRepr addrWidth -> NatRepr cellWidth -> NatRepr valWidth -> Int -> expr (BVType addrWidth) -> expr (WordMapType addrWidth (BaseBVType cellWidth)) -> expr (BVType cellWidth) -> expr (BVType valWidth)
littleEndianStore :: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth) => NatRepr addrWidth -> NatRepr cellWidth -> NatRepr valWidth -> Int -> expr (BVType addrWidth) -> expr (BVType valWidth) -> expr (WordMapType addrWidth (BaseBVType cellWidth)) -> expr (WordMapType addrWidth (BaseBVType cellWidth))

Documentation

class IsExpr (e :: CrucibleType -> Type) where Source #

A typeclass for injecting applications into expressions.

Associated Types

type ExprExt (e :: CrucibleType -> Type) Source #

Methods

app :: forall (tp :: CrucibleType). App (ExprExt e) e tp -> e tp Source #

asApp :: forall (tp :: CrucibleType). e tp -> Maybe (App (ExprExt e) e tp) Source #

exprType :: forall (tp :: CrucibleType). e tp -> TypeRepr tp Source #

Instances

Instances details

TypeApp (ExprExtension ext) => IsExpr (Expr ext s) Source #

Instance details

Defined in Lang.Crucible.CFG.Reg

Associated Types

type ExprExt (Expr ext s)
Instance details Defined in Lang.Crucible.CFG.Reg type ExprExt (Expr ext s) = ext

Methods

app :: forall (tp :: CrucibleType). App (ExprExt (Expr ext s)) (Expr ext s) tp -> Expr ext s tp Source #

asApp :: forall (tp :: CrucibleType). Expr ext s tp -> Maybe (App (ExprExt (Expr ext s)) (Expr ext s) tp) Source #

exprType :: forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp Source #

eapp :: forall e (tp :: CrucibleType). IsExpr e => ExprExtension (ExprExt e) e tp -> e tp Source #

Inject an extension app into the expression type

asEapp :: forall e (tp :: CrucibleType). IsExpr e => e tp -> Maybe (ExprExtension (ExprExt e) e tp) Source #

Test if an expression is formed from an extension app

Booleans

true :: IsExpr e => e BoolType Source #

True expression

false :: IsExpr e => e BoolType Source #

False expression

notExpr :: IsExpr e => e BoolType -> e BoolType Source #

(.&&) :: IsExpr e => e BoolType -> e BoolType -> e BoolType infixr 3 Source #

(.||) :: IsExpr e => e BoolType -> e BoolType -> e BoolType infixr 2 Source #

Expression classes

class EqExpr (e :: CrucibleType -> Type) (tp :: CrucibleType) where Source #

Minimal complete definition

(.==)

Methods

(.==) :: e tp -> e tp -> e BoolType infix 4 Source #

(./=) :: e tp -> e tp -> e BoolType infix 4 Source #

Instances

Instances details

EqExpr e NatType Source #
Instance details Defined in Lang.Crucible.Syntax Methods (.==) :: e NatType -> e NatType -> e BoolType Source # (./=) :: e NatType -> e NatType -> e BoolType Source #
EqExpr e RealValType Source #
Instance details Defined in Lang.Crucible.Syntax Methods (.==) :: e RealValType -> e RealValType -> e BoolType Source # (./=) :: e RealValType -> e RealValType -> e BoolType Source #

class EqExpr e tp => OrdExpr (e :: CrucibleType -> Type) (tp :: CrucibleType) where Source #

Minimal complete definition

(.<)

Methods

(.<) :: e tp -> e tp -> e BoolType infix 4 Source #

(.<=) :: e tp -> e tp -> e BoolType infix 4 Source #

(.>) :: e tp -> e tp -> e BoolType infix 4 Source #

(.>=) :: e tp -> e tp -> e BoolType infix 4 Source #

Instances

Instances details

OrdExpr e NatType Source #
Instance details Defined in Lang.Crucible.Syntax Methods (.<) :: e NatType -> e NatType -> e BoolType Source # (.<=) :: e NatType -> e NatType -> e BoolType Source # (.>) :: e NatType -> e NatType -> e BoolType Source # (.>=) :: e NatType -> e NatType -> e BoolType Source #
OrdExpr e RealValType Source #
Instance details Defined in Lang.Crucible.Syntax Methods (.<) :: e RealValType -> e RealValType -> e BoolType Source # (.<=) :: e RealValType -> e RealValType -> e BoolType Source # (.>) :: e RealValType -> e RealValType -> e BoolType Source # (.>=) :: e RealValType -> e RealValType -> e BoolType Source #

class NumExpr (e :: CrucibleType -> Type) (tp :: CrucibleType) where Source #

Methods

(.+) :: e tp -> e tp -> e tp Source #

(.-) :: e tp -> e tp -> e tp Source #

(.*) :: e tp -> e tp -> e tp Source #

Instances

Instances details

NumExpr e NatType Source #
Instance details Defined in Lang.Crucible.Syntax Methods (.+) :: e NatType -> e NatType -> e NatType Source # (.-) :: e NatType -> e NatType -> e NatType Source # (.*) :: e NatType -> e NatType -> e NatType Source #

class LitExpr (e :: CrucibleType -> Type) (tp :: CrucibleType) ty | tp -> ty where Source #

An expression that embeds literal values of its type.

Methods

litExpr :: ty -> e tp Source #

Instances

Instances details

LitExpr e BoolType Bool Source #
Instance details Defined in Lang.Crucible.Syntax Methods litExpr :: Bool -> e BoolType Source #
LitExpr e IntegerType Integer Source #
Instance details Defined in Lang.Crucible.Syntax Methods litExpr :: Integer -> e IntegerType Source #
LitExpr e NatType Natural Source #
Instance details Defined in Lang.Crucible.Syntax Methods litExpr :: Natural -> e NatType Source #
LitExpr e (StringType Unicode) Text Source #
Instance details Defined in Lang.Crucible.Syntax Methods litExpr :: Text -> e (StringType Unicode) Source #
LitExpr e (FunctionHandleType args ret) (FnHandle args ret) Source #
Instance details Defined in Lang.Crucible.Syntax Methods litExpr :: FnHandle args ret -> e (FunctionHandleType args ret) Source #

Natural numbers

class ConvertableToNat (e :: CrucibleType -> Type) (tp :: CrucibleType) where Source #

Methods

toNat :: e tp -> e NatType Source #

Convert value of type to Nat. This may be partial, it is the responsibility of the calling code that it is correct for this type.

Instances

Instances details

ConvertableToNat e ComplexRealType Source #
Instance details Defined in Lang.Crucible.Syntax Methods toNat :: e ComplexRealType -> e NatType Source #
ConvertableToNat e RealValType Source #
Instance details Defined in Lang.Crucible.Syntax Methods toNat :: e RealValType -> e NatType Source #

Real numbers

rationalLit :: IsExpr e => Rational -> e RealValType Source #

natToReal :: IsExpr e => e NatType -> e RealValType Source #

integerToReal :: IsExpr e => e IntegerType -> e RealValType Source #

Complex real numbers

realToCplx :: IsExpr e => e RealValType -> e ComplexRealType Source #

imagToCplx :: IsExpr e => e RealValType -> e ComplexRealType Source #

realPart :: IsExpr e => e ComplexRealType -> e RealValType Source #

imagPart :: IsExpr e => e ComplexRealType -> e RealValType Source #

realLit :: IsExpr e => Rational -> e ComplexRealType Source #

imagLit :: IsExpr e => Rational -> e ComplexRealType Source #

natToCplx :: IsExpr e => e NatType -> e ComplexRealType Source #

Maybe

nothingValue :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e (MaybeType tp) Source #

justValue :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e tp -> e (MaybeType tp) Source #

Vector

vectorSize :: forall e (tp :: CrucibleType). IsExpr e => e (VectorType tp) -> e NatType Source #

vectorLit :: forall e (tp :: CrucibleType). IsExpr e => TypeRepr tp -> Vector (e tp) -> e (VectorType tp) Source #

vectorGetEntry :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e (VectorType tp) -> e NatType -> e tp Source #

Get the entry from a zero-based index.

vectorSetEntry :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e (VectorType tp) -> e NatType -> e tp -> e (VectorType tp) Source #

vectorIsEmpty :: forall e (tp :: CrucibleType). IsExpr e => e (VectorType tp) -> e BoolType Source #

vecReplicate :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e NatType -> e tp -> e (VectorType tp) Source #

Function handles

closure :: forall e (tp :: CrucibleType) (ret :: CrucibleType) (args :: Ctx CrucibleType). (IsExpr e, KnownRepr TypeRepr tp, KnownRepr TypeRepr ret, KnownCtx TypeRepr args) => e (FunctionHandleType (args ::> tp) ret) -> e tp -> e (FunctionHandleType args ret) Source #

IdentValueMap

emptyIdentValueMap :: forall (tp :: CrucibleType) e. (KnownRepr TypeRepr tp, IsExpr e) => e (StringMapType tp) Source #

Initialize the ident value map to the given value.

setIdentValue :: forall e (tp :: CrucibleType). (IsExpr e, KnownRepr TypeRepr tp) => e (StringMapType tp) -> Text -> e (MaybeType tp) -> e (StringMapType tp) Source #

Structs

mkStruct :: forall e (ctx :: Ctx CrucibleType). IsExpr e => CtxRepr ctx -> Assignment e ctx -> e (StructType ctx) Source #

getStruct :: forall e (ctx :: Ctx CrucibleType) (tp :: CrucibleType). IsExpr e => Index ctx tp -> e (StructType ctx) -> e tp Source #

setStruct :: forall e (ctx :: Ctx CrucibleType) (tp :: CrucibleType). IsExpr e => CtxRepr ctx -> e (StructType ctx) -> Index ctx tp -> e tp -> e (StructType ctx) Source #

Multibyte operations

concatExprs :: forall (w :: Natural) a expr. (IsExpr expr, 1 <= w) => NatRepr w -> [expr (BVType w)] -> (forall (w' :: Natural). 1 <= w' => NatRepr w' -> expr (BVType w') -> a) -> a Source #

bigEndianLoad Source #

Arguments

:: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int	number of bytes to load
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType valWidth)

bigEndianLoadDef Source #

Arguments

:: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int	number of bytes to load
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType cellWidth)
-> expr (BVType valWidth)

bigEndianStore Source #

Arguments

:: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int	number of bytes to write
-> expr (BVType addrWidth)
-> expr (BVType valWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))

littleEndianLoad Source #

Arguments

:: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int	number of bytes to load
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType valWidth)

littleEndianLoadDef Source #

Arguments

:: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int	number of bytes to load
-> expr (BVType addrWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (BVType cellWidth)
-> expr (BVType valWidth)

littleEndianStore Source #

Arguments

:: forall expr (addrWidth :: Natural) (valWidth :: Natural) (cellWidth :: Natural). (IsExpr expr, 1 <= addrWidth, 1 <= valWidth, 1 <= cellWidth)
=> NatRepr addrWidth
-> NatRepr cellWidth
-> NatRepr valWidth
-> Int	number of bytes to write
-> expr (BVType addrWidth)
-> expr (BVType valWidth)
-> expr (WordMapType addrWidth (BaseBVType cellWidth))
-> expr (WordMapType addrWidth (BaseBVType cellWidth))