Language.Boogie.Util

Various properties and transformations of Boogie program elements

Types

type TypeBinding = Map Id Type

Mapping from type variables to types

typeSubst :: TypeBinding -> Type -> Type

typeSubst binding t : Substitute all free type variables in t according to binding; all variables in the domain of bindings are considered free if not explicitly bound

renameTypeVars :: [Id] -> [Id] -> TypeBinding -> TypeBinding

renameTypeVars tv newTV binding : binding with each occurrence of one of tv replaced with corresponding newTV (in both domain and range)

fromTVNames :: [Id] -> [Id] -> TypeBinding

fromTVNames tvs tvs' : type binding that replaces type variables tvs with type variables tvs'

isFreeIn :: Id -> Type -> Bool

x isFreeIn t : does x occur free in t?

isTypeVar :: [Id] -> Id -> Bool

isTypeVar contextTypeVars v : Is v either one of contextTypeVars or a freash type variable generated by freshTVName?

unifier :: [Id] -> [Type] -> [Type] -> Maybe TypeBinding

unifier fv xs ys : most general unifier of xs and ys with shared free type variables of the context fv

freshTVName :: Show a => a -> [Char]

'freshTVName n : Fresh type variable with a unique identifier n

tupleType :: [Type] -> Type

Internal tuple type constructor (used for representing procedure returns as a single type)

Expressions

freeVarsTwoState :: Expression -> ([Id], [Id])

Free variables in an expression, referred to in current state and old state

freeVars :: Expression -> [Id]

Free variables in an expression, in current state

freeOldVars :: Expression -> [Id]

Free variables in an expression, in old state

type VarBinding = Map Id BareExpression

Mapping from variables to expressions

exprSubst :: VarBinding -> Expression -> Expression

exprSubst binding e : substitute all free variables in e according to binding; all variables in the domain of bindings are considered free if not explicitly bound

paramSubst :: PSig -> PDef -> Expression -> Expression

paramSubst sig def : Substitute parameter names from sig in an expression with their equivalents from def

freeSelections :: Expression -> [(Id, [Expression])]

freeSelections expr : all map selections that occur in expr, where the map is a free variable

applications :: Expression -> [(Id, [Expression])]

applications expr : all function applications that occur in expr

Specs

preconditions :: [Contract] -> [SpecClause]

preconditions specs : all precondition clauses in specs

postconditions :: [Contract] -> [SpecClause]

postconditions specs : all postcondition clauses in specs

modifies :: [Contract] -> [Id]

modifies specs : all modifies clauses in specs

assumePreconditions :: PSig -> PSig

Make all preconditions in contracts free

assumePostconditions :: PSig -> PSig

Make all postconditions in contracts free

Functions and procedures

data FSig

Function signature

Constructors

FSig

Fields

fsigName :: Id

Function name

fsigTypeVars :: [Id]

Type variables

fsigArgTypes :: [Type]

Argument types

fsigRetType :: Type

Return type

Instances

Eq FSig

fsigType :: FSig -> Type

Function signature as a map type

fsigFromType :: Type -> FSig

Map type as a function signature

data FDef

Function definition

Constructors

FDef

Fields

fdefName :: Id

Entity to which the definition belongs

fdefTV :: [Id]

Type variables

fdefArgs :: [IdType]

Arguments (types may be less general than in the corresponding signature)

fdefGuard :: Expression

Condition under which the definition applies

fdefBody :: Expression

Body

type ConstraintSet = ([FDef], [FDef])

Constraint set: contains a list of definitions and a list of constraints

type AbstractStore = Map Id ConstraintSet

Abstract store: maps names to their constraints

asUnion :: AbstractStore -> AbstractStore -> AbstractStore

Union of abstract stores (values at the same key are concatenated)

data PSig

Procedure signature

Constructors

PSig

Fields

psigName :: Id

Procedure name

psigTypeVars :: [Id]

Type variables

psigArgs :: [IdTypeWhere]

In-parameters

psigRets :: [IdTypeWhere]

Out-parameters

psigContracts :: [Contract]

Contracts

Instances

Eq PSig

psigParams :: PSig -> [IdTypeWhere]

All parameters of a procedure signature

psigArgTypes :: PSig -> [Type]

Types of in-parameters of a procedure signature

psigRetTypes :: PSig -> [Type]

Types of out-parameters of a procedure signature

psigModifies :: PSig -> [Id]

Modifies clauses of a procedure signature

psigRequires :: PSig -> [SpecClause]

Preconditions of a procedure signature

psigEnsures :: PSig -> [SpecClause]

Postconditions of a procedure signature

psigType :: PSig -> Type

Procedure signature as a map type

data PDef

Procedure definition; a single procedure might have multiple definitions (one per body)

Constructors

PDef

Fields

pdefIns :: [Id]

In-parameter names (in the same order as psigArgs in the corresponding signature)

pdefOuts :: [Id]

Out-parameter names (in the same order as psigRets in the corresponding signature)

pdefParamsRenamed :: Bool

Are any parameter names in this definition different for the procedure signature? (used for optimizing parameter renaming, True is a safe default)

pdefBody :: BasicBody

Body

pdefConstraints :: AbstractStore

Constraints on local names

pdefPos :: SourcePos

Location of the (first line of the) procedure definition in the source

pdefLocals :: PDef -> [Id]

All local names of a procedure definition

Code generation

num :: Integer -> Pos BareExpression

eneg :: Pos BareExpression -> Pos BareExpression

enot :: Pos BareExpression -> Pos BareExpression

(|+|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|-|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|*|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|/|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|%|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|!=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|<|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|<=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|>|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|>=|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|&|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|||) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|=>|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

(|<=>|) :: Pos BareExpression -> Pos BareExpression -> Pos BareExpression

conjunction :: [Pos BareExpression] -> Pos BareExpression

assume :: Pos BareExpression -> Pos BareStatement

Misc

interval :: Enum t => (t, t) -> [t]

interval (lo, hi) : Interval from lo to hi

fromRight :: Either a b -> b

Extract the element out of a Right and throw an error if its argument is Left

deleteAll :: Ord k => [k] -> Map k a -> Map k a

deleteAll keys m : map m with keys removed from its domain

restrictDomain :: Ord k => Set k -> Map k a -> Map k a

restrictDomain keys m : map m restricted on the set of keys keys

removeDomain :: Ord k => Set k -> Map k a -> Map k a

removeDomain keys m : map m with the set of keys keys removed from its domain

mapItwType :: (Type -> Type) -> IdTypeWhere -> IdTypeWhere

anyM :: Monad m => (a -> m Bool) -> [a] -> m Bool

Monadic version of any (executes boolean-valued computation for all arguments in a list until the first True is found)

changeState :: Monad m => (s -> t) -> (t -> s -> s) -> StateT t m a -> StateT s m a

Execute a computation with state of type t inside a computation with state of type s

withLocalState :: Monad m => (s -> t) -> StateT t m a -> StateT s m a

withLocalState localState e : Execute e in current state modified by localState, and then restore current state

internalError :: [Char] -> t