| Safe Haskell | Safe-Inferred |
|---|
Language.Boogie.Interpreter
Contents
Description
Interpreter for Boogie 2
- executeProgram :: Program -> Context -> Id -> Either RuntimeFailure Environment
- data Value
- data Environment = Environment {
- envLocals :: Map Id Value
- envGlobals :: Map Id Value
- envOld :: Map Id Value
- envConstants :: Map Id Expression
- envFunctions :: Map Id [FDef]
- envProcedures :: Map Id [PDef]
- envTypeContext :: Context
- emptyEnv :: Environment
- lookupFunction :: Id -> Environment -> [FDef]
- lookupProcedure :: Id -> Environment -> [PDef]
- modifyTypeContext :: (Context -> Context) -> Environment -> Environment
- setV :: MonadState Environment m => Id -> Value -> m ()
- setAll :: MonadState Environment m => [Id] -> [Value] -> m ()
- type Execution a = ErrorT RuntimeFailure (State Environment) a
- type SafeExecution a = State Environment a
- execSafely :: Execution a -> (RuntimeFailure -> SafeExecution a) -> SafeExecution a
- execUnsafely :: SafeExecution a -> Execution a
- data FailureSource
- data InternalCode
- data StackFrame = StackFrame {}
- type StackTrace = [StackFrame]
- data RuntimeFailure = RuntimeFailure {}
- data FailureKind
- = Error
- | Unreachable
- | Nonexecutable
- failureKind :: RuntimeFailure -> FailureKind
- eval :: Expression -> Execution Value
- exec :: Statement -> Execution ()
- execProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Execution [Value]
- collectDefinitions :: Program -> SafeExecution ()
- valueDoc :: Value -> Doc
- varsDoc :: Map Id Value -> Doc
- functionsDoc :: Map Id [FDef] -> Doc
- runtimeFailureDoc :: RuntimeFailure -> Doc
Executing programs
executeProgram :: Program -> Context -> Id -> Either RuntimeFailure EnvironmentSource
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
Run-time value
data Environment Source
Execution state
Constructors
| Environment | |
Fields
| |
Empty environment
lookupFunction :: Id -> Environment -> [FDef]Source
lookupFunction id env : All definitions of function id in env
lookupProcedure :: Id -> Environment -> [PDef]Source
lookupProcedure id env : All definitions of procedure id in env
modifyTypeContext :: (Context -> Context) -> Environment -> EnvironmentSource
setV :: MonadState Environment m => Id -> Value -> m ()Source
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 ()Source
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) aSource
Computations with Environment as state, which can result in either a or RuntimeFailure
type SafeExecution a = State Environment aSource
Computations with Environment as state, which always result in a
execSafely :: Execution a -> (RuntimeFailure -> SafeExecution a) -> SafeExecution aSource
execSafely computation handler : Execute an unsafe computation in a safe environment, handling errors that occur in computation with handler
execUnsafely :: SafeExecution a -> Execution aSource
execUnsafely computation : Execute a safe computation in an unsafe environment
Run-time failures
data FailureSource Source
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
data StackFrame Source
Information about a procedure or function call
Constructors
| StackFrame | |
Instances
type StackTrace = [StackFrame]Source
data RuntimeFailure Source
Failures that occur during execution
Constructors
| RuntimeFailure | |
Fields
| |
Instances
data FailureKind Source
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
failureKind :: RuntimeFailure -> FailureKindSource
Kind of a run-time failure
Executing parts of programs
eval :: Expression -> Execution ValueSource
Evaluate an expression; can have a side-effect of initializing variables that were not previously defined
exec :: Statement -> Execution ()Source
Execute a basic statement (no jump, if or while statements allowed)
execProcedure :: PSig -> PDef -> [Expression] -> [Expression] -> Execution [Value]Source
execProcedure sig def args lhss :
Execute definition def of procedure sig with actual arguments args and call left-hand sides lhss
collectDefinitions :: Program -> SafeExecution ()Source
Collect constant, function and procedure definitions from the program
Pretty-printing
runtimeFailureDoc :: RuntimeFailure -> DocSource
Pretty-printed run-time failure