crucible-0.7: Crucible is a library for language-agnostic symbolic simulation
Copyright(c) Galois Inc 2014
LicenseBSD3
MaintainerJoe Hendrix <jhendrix@galois.com>
Stabilityprovisional
Safe HaskellSafe-Inferred
LanguageHaskell2010

Lang.Crucible.Syntax

Description

This module provides typeclasses and combinators for constructing AST expressions.

Synopsis

Documentation

class IsExpr e where Source #

A typeclass for injecting applications into expressions.

Associated Types

type ExprExt e :: Type Source #

Methods

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

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

exprType :: 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) Source #

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 :: IsExpr e => ExprExtension (ExprExt e) e tp -> e tp Source #

Inject an extension app into the expression type

asEapp :: 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 tp where Source #

Minimal complete definition

(.==)

Methods

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

(./=) :: IsExpr e => 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 tp where Source #

Minimal complete definition

(.<)

Methods

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

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

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

(.>=) :: IsExpr e => 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 tp where Source #

Methods

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

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

(.*) :: IsExpr e => 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 tp ty | tp -> ty where Source #

An expression that embeds literal values of its type.

Methods

litExpr :: IsExpr e => 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 tp where Source #

Methods

toNat :: IsExpr e => 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 :: (IsExpr e, KnownRepr TypeRepr tp) => e (MaybeType tp) Source #

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

Vector

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

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

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

Get the entry from a zero-based index.

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

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

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

Function handles

closure :: (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 :: KnownRepr TypeRepr tp => IsExpr e => e (StringMapType tp) Source #

Initialize the ident value map to the given value.

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

Structs

mkStruct :: IsExpr e => CtxRepr ctx -> Assignment e ctx -> e (StructType ctx) Source #

getStruct :: IsExpr e => Index ctx tp -> e (StructType ctx) -> e tp Source #

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

Multibyte operations

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

bigEndianLoad Source #

Arguments

:: (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

:: (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

:: (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

:: (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

:: (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

:: (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))