Language.Boogie.Interpreter

Interpreter for Boogie 2

Executing programs

executeProgram :: Program -> Context -> Id -> Either RuntimeFailure Environment

executeProgram p tc entryPoint : Execute program p in type context tc starting from procedure entryPoint, and return the final environment; requires that entryPoint have no in- or out-parameters

State

data Value

Run-time value

Constructors

IntValue Integer

Integer value

BoolValue Bool

Boolean value

MapValue (Map [Value] Value)

Value of a map type

CustomValue Integer

Value of a user-defined type (values with the same code are considered equal)

Instances

Eq Value

Ord Value

Show Value

data Environment

Execution state

Constructors

Environment

Fields

envLocals :: Map Id Value

Local variable names to values

envGlobals :: Map Id Value

Global variable names to values

envOld :: Map Id Value

Global variable names to old values (in two-state contexts)

envConstants :: Map Id Expression

Constant names to expressions

envFunctions :: Map Id [FDef]

Function names to definitions

envProcedures :: Map Id [PDef]

Procedure names to definitions

envTypeContext :: Context

Type context

emptyEnv :: Environment

Empty environment

lookupFunction :: Id -> Environment -> [FDef]

lookupFunction id env : All definitions of function id in env

lookupProcedure :: Id -> Environment -> [PDef]

lookupProcedure id env : All definitions of procedure id in env

modifyTypeContext :: (Context -> Context) -> Environment -> Environment

setV :: MonadState Environment m => Id -> Value -> m ()

setV id val : set value of variable id to val; id has to be declared in the current type context

setAll :: MonadState Environment m => [Id] -> [Value] -> m ()

setAll ids vals : set values of variables ids to vals; all ids have to be declared in the current type context

Executions

type Execution a = ErrorT RuntimeFailure (State Environment) a

Computations with Environment as state, which can result in either a or RuntimeFailure

type SafeExecution a = State Environment a

Computations with Environment as state, which always result in a

execSafely :: Execution a -> (RuntimeFailure -> SafeExecution a) -> SafeExecution a

execSafely computation handler : Execute an unsafe computation in a safe environment, handling errors that occur in computation with handler

execUnsafely :: SafeExecution a -> Execution a

execUnsafely computation : Execute a safe computation in an unsafe environment

Run-time failures

data FailureSource

Constructors

SpecViolation SpecClause

Violation of user-defined specification

DivisionByZero

Division by zero

UnsupportedConstruct String

Language construct is not yet supported (should disappear in later versions)

InfiniteDomain Id Interval

Quantification over an infinite set

NoImplementation Id

Call to a procedure with no implementation

InternalFailure InternalCode

Must be cought inside the interpreter and never reach the user

Instances

Eq FailureSource

data InternalCode

Internal error codes

Instances

Eq InternalCode

data StackFrame

Information about a procedure or function call

Constructors

StackFrame

Fields

callPos :: SourcePos

Source code position of the call

callName :: Id

Name of procedure or function

Instances

Eq StackFrame

type StackTrace = [StackFrame]

data RuntimeFailure

Failures that occur during execution

Constructors

RuntimeFailure

Fields

rtfSource :: FailureSource

Source of the failure

rtfPos :: SourcePos

Location where the failure occurred

rtfEnv :: Environment

Environment at the time of failure

rtfTrace :: StackTrace

Stack trace from the program entry point to the procedure where the failure occurred

Instances

Eq RuntimeFailure

Show RuntimeFailure

Error RuntimeFailure

data FailureKind

Kinds of run-time failures

Constructors

Error

Error state reached (assertion violation)

Unreachable

Unreachable state reached (assumption violation)

Nonexecutable

The state is OK in Boogie semantics, but the execution cannot continue due to the limitations of the interpreter

Instances

Eq FailureKind

failureKind :: RuntimeFailure -> FailureKind

Kind of a run-time failure

Executing parts of programs

eval :: Expression -> Execution Value

Evaluate an expression; can have a side-effect of initializing variables that were not previously defined

exec :: Statement -> Execution ()

Execute a basic statement (no jump, if or while statements allowed)

execProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Execution [Value]

execProcedure sig def args lhss : Execute definition def of procedure sig with actual arguments args and call left-hand sides lhss

collectDefinitions :: Program -> SafeExecution ()

Collect constant, function and procedure definitions from the program

Pretty-printing

valueDoc :: Value -> Doc

Pretty-printed value

varsDoc :: Map Id Value -> Doc

Pretty-printed mapping of variables to values

functionsDoc :: Map Id [FDef] -> Doc

Pretty-printed set of function definitions

runtimeFailureDoc :: RuntimeFailure -> Doc

Pretty-printed run-time failure