Language.Boogie.Interpreter

Interpreter for Boogie 2

Executing programs

executeProgramDet :: Program -> Context -> Maybe Integer -> Id -> TestCase

executeProgramDet p tc entryPoint : Execute program p deterministically in type context tc starting from procedure entryPoint and return a single outcome. Whenever a value is unspecified, a default value of the required type is used.

executeProgram :: Program -> Context -> Generator Stream -> Maybe Integer -> Id -> [TestCase]

executeProgram p tc entryPoint : Execute program p non-deterministically in type context tc starting from procedure entryPoint and return an infinite list of possible outcomes (each either runtime failure or the final variable store). Whenever a value is unspecified, all values of the required type are tried exhaustively.

executeProgramGeneric :: (Monad m, Functor m) => Program -> Context -> Generator m -> Maybe Integer -> Id -> m TestCase

executeProgramGeneric p tc generator qbound entryPoint : Execute program p in type context tc with input generator generator, starting from procedure entryPoint, and return the outcome(s) embedded into the generator's monad.

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

MapEquality Value Value

Equality of two maps cannot be determined

InternalException InternalCode

Must be cought inside the interpreter and never reach the user

Instances

Eq FailureSource

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

rtfMemory :: Memory

Memory state 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

runtimeFailureDoc :: Bool -> RuntimeFailure -> Doc

Pretty-printed run-time failure

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

Execution outcomes

data TestCase

Description of an execution

Constructors

TestCase

Fields

tcProcedure :: PSig

Root procedure (entry point) of the execution

tcMemory :: Memory

Final memory state (at the exit from the root procedure)

tcFailure :: Maybe RuntimeFailure

Failure the execution eded with, or Nothing if the execution ended in a valid state

isPass :: TestCase -> Bool

isPass tc: Does tc end in a valid state?

isInvalid :: TestCase -> Bool

isInvalid tc: Does tc and in an unreachable state?

isNonexecutable :: TestCase -> Bool

isNonexecutable tc: Does tc end in a non-executable state?

isFail :: TestCase -> Bool

isFail tc: Does tc end in an error state?

testCaseSummary :: Bool -> TestCase -> Doc

testCaseSummary debug tc : Summary of tc's inputs and outcome, displayed in user or debug format depending on debug

finalStateDoc :: Bool -> TestCase -> Doc

finalStateDoc debug tc : outputs of tc, displayed in user or debug format depending on debug

data Summary

Test session summary

Constructors

Summary

Fields

sPassCount :: Int

Number of passing test cases

sFailCount :: Int

Number of failing test cases

sInvalidCount :: Int

Number of invalid test cases

sNonExecutableCount :: Int

Number of nonexecutable test cases

sUniqueFailures :: [TestCase]

Unique failing test cases

Instances

Show Summary

testSessionSummary :: [TestCase] -> Summary

Summary of a set of test cases

summaryDoc :: Summary -> Doc

Pretty-printed test session summary

Executing parts of programs

eval :: (Monad m, Functor m) => Expression -> Execution m Value

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

exec :: (Monad m, Functor m) => Statement -> Execution m ()

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

execProcedure :: (Monad m, Functor m) => PSig -> PDef -> [Expression] -> [Expression] -> Execution m [Value]

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

preprocess :: (Monad m, Functor m) => Program -> SafeExecution m ()

Collect procedure implementations, and constantfunctionglobal variable constraints