Kratos2 Python API Reference

API for Kratos2.

Basic Types

Type Objects

class Type(object)

Base class for Kratos Type objects

write

def write(out, bindings=None)

printer in K2 format

__str__

def __str__()

Get a string representation of this type in K2 format.

VoidType Objects

class VoidType(Type)

void type

LabelType Objects

class LabelType(Type)

label type

BoolType Objects

class BoolType(Type)

boolean type

IntType Objects

class IntType(Type)

integer type

RealType Objects

class RealType(Type)

real type

SymbolType Objects

class SymbolType(Type)

symbolic type

BVType Objects

class BVType(Type)

fixed-size bit-vector type.

Attributes:

• bits: number of bits
• is_signed: sign flag

FPType Objects

class FPType(Type)

IEEE floating-point type.

Attributes:

• bits: total number of bits
• exponent: number of exponent bits
• mantissa: number of mantissa bits (without the implicit 1)

MapType Objects

class MapType(Type)

map type.

Attributes:

• index: type of the index
• element: type of the element

FunctionType Objects

class FunctionType(Type)

function type.

Attributes:

• args: list of argument types
• ret: list of return types

EnumType Objects

class EnumType(Type)

symbolic enum type.

Attributes:

• values: list of enum values (as strings)

Expr Objects

class Expr(object)

Base class for Kratos expressions.

Attributes:

• type: the expression type
• annotations: if not None, a list of (key, value) pairs

write

def write(out, indent=None, bindings=None)

Generate a K2 representation of this expression.

Arguments:

• out: file-like object
• indent: (optional) indentation level
• bindings: (optional) mapping from names to expressions

__str__

def __str__()

Get a string representation of this type in K2 format.

children

def children()

Return the list of children of this expression.

VarExpr Objects

class VarExpr(Expr)

A var expression.

Attributes:

• var: the variable name

ConstExpr Objects

class ConstExpr(Expr)

A const expression.

Attributes:

• is_symbol: true if the value is a symbol
• value: the expression value

OpExpr Objects

class OpExpr(Expr)

An op expression.

Attributes:

• op: the operation tag
• args: the operation arguments

CallExpr Objects

class CallExpr(Expr)

A call expression.

Attributes:

• func: the function to call
• args: the list of call arguments
• ret: the list of return vars

AssignExpr Objects

class AssignExpr(Expr)

An assign expression.

Attributes:

• lhs: the assignment target var
• rhs: the assigned value

AssumeExpr Objects

class AssumeExpr(Expr)

An assume expression.

Attributes:

• cond: the assumption constraint

TypeCastExpr Objects

class TypeCastExpr(Expr)

A typecast expression.

Attributes:

• expr: the child expression
• is_bitcast: true if this is a bitcast

SeqExpr Objects

class SeqExpr(Expr)

A seq expression.

Attributes:

• args: the list of children

JumpExpr Objects

class JumpExpr(Expr)

A jump expression.

Attributes:

• targets: the list of targets

LabelExpr Objects

class LabelExpr(Expr)

A label expression.

Attributes:

• name: the name of the label

HavocExpr Objects

class HavocExpr(Expr)

A havoc expression.

Attributes:

• lval: the target variable

CondJumpExpr Objects

class CondJumpExpr(Expr)

A condjump expression.

Attributes:

• cond: the jump condition
• target: the jump target

ExprVisitor Objects

class ExprVisitor(object)

A generic visitor for expressions. The visitor works by calling a method visit_ClassName for visiting expression of type ClassName. If no such method exists, generic_visit is called. The methods must accept a single argument, the expression to visit. Each method should call self.visit(c) recursively on each child c that needs to be visited.

visit

def visit(expr)

visitor entry point.

Arguments:

• expr: the expression to visit

generic_visit

def generic_visit(expr)

generic visitor function, which simply visits all the children of the input expression.

Arguments:

• expr: the expression to visit

IdentityVisitor Objects

class IdentityVisitor(ExprVisitor)

A subclass of ExprVisitor that builds a copy of the input expression

InplaceIdentityVisitor Objects

class InplaceIdentityVisitor(IdentityVisitor)

A subclass of IdentityVisitor that modifies the input expression in-place.

Function Objects

class Function(object)

A Kratos function.

Attributes:

• name: the name of the function
• params: the function formal parameters (list of var expressions)
• retvars: the function return vars (list of var expressions)
• locals: the funciton local vars (list of var expressions)
• body: the function body

__str__

def __str__()

Get a string representation of this function in K2 format.

write

def write(out, bindings=None)

Write a K2 representation of the function to the file-like out.

Arguments:

• out: a file-like object
• bindings: (optional) a mapping from names to expressions

get_const

def get_const()

Get the const expression for this function.

get_type

def get_type()

Get the type of this function.

is_param

def is_param(name)

Return true if name is a name of one of the function parameters.

is_return_var

def is_return_var(name)

Return true if name is a name of one of the function return vars.

is_local

def is_local(name)

Return true if name is a name of one of the function local vars.

is_own

def is_own(name)

Return true if name is a parameter, return var or local var.

get_param

def get_param(name)

Get the parameter with the given name. Raise KeyError if not found.

get_local

def get_local(name)

Get the local var with the given name. Raise KeyError if not found.

get_return_var

def get_return_var(name)

Get the return var with the given name. Raise KeyError if not found.

get_own

def get_own(name)

Get the parameter, local var or return var with the given name. Raise KeyError if not found.

copy

def copy()

Return a copy of this function.

Program Objects

class Program(object)

A Kratos program.

Attributes:

• init: an constraint (boolean expression) on global vars, or None
• entrypoint: name of the program entry point, or None
• comment: a comment for the program, or None
• globals: the list of global variables (list of var expressions)
• functions: the list of program functions

__str__

def __str__()

Get a string representation of this program in K2 format.

write

def write(out)

Write a K2 representation of the program to the file-like out.

Arguments:

• out: a file-like object

is_global

def is_global(name)

Returns true if name is the name of a global var of this program.

get_global

def get_global(name)

Get the global var with the given name. Raise KeyError if not found.

get_function

def get_function(name)

Get the function with the given name. Raise KeyError if not found.

copy

def copy()

Return a copy of this program.

ExecutionStep Objects

class ExecutionStep(object)

A step of a Kratos execution trace.

Arguments:

• is_path: true if this step is a subpath
• stmt: the expression corresponding to this step (when is_path is false)
• path: the subpath associated to this step (when is_path is true)

write

def write(out, indent=0)

Write a K2 representation of the execution step to the file-like out.

Arguments:

• out: a file-like object

copy

def copy()

Return a copy of this execution step.

__str__

def __str__()

Get a string representation of this execution step in K2 format.

ExecutionPath Objects

class ExecutionPath(list)

A subpath of a Kratos execution trace.

write

def write(out, indent=0)

Write a K2 representation of the execution path to the file-like out.

Arguments:

• out: a file-like object

copy

def copy()

Return a copy of this execution path.

__str__

def __str__()

Get a string representation of this execution path in K2 format.

Parsing

parse_program

def parse_program(src)

Parse a Program from the given file-like object.

Arguments:

• src: a file-like object

parse_expr

def parse_expr(src)

Parse an Expr from the given file-like object.

Arguments:

• src: a file-like object

parse_execution_path

def parse_execution_path(src)

Parse an ExecutionPath from the given file-like object.

Arguments:

• src: a file-like object

Verification

RESULT_ERROR

error verification result

RESULT_UNKNOWN

unknown verification result

RESULT_SAFE

safe verification result

RESULT_UNSAFE

unsafe verification result

VERIFICATION_MODEL_CHECKING

model checking verification method

VERIFICATION_SYMBOLIC_EXECUTION

symbolic execution verification method

VERIFICATION_SIMULATION

simulation verification method

VerificationResult Objects

class VerificationResult(object)

A Kratos verification result.

Attributes:

• status: the verification status (RESULT_UNKNOWN, RESULT_SAFE, or RESULT_UNSAFE)
• trace: the counterexample trace (can be None)

encode

def encode(config, program)

Encode a Program into a symbolic transition system.

Arguments:

• config: a dictionary with the configuration settings to use for the encoding. See here for the list of configuration options.
• program: the program to encode

Returns:

• a string representation of the symbolic transition system

verify

def verify(method, config, program)

Perform verification of the given Kratos program.

Arguments:

• method: the verification method to use (VERIFICATION_MODEL_CHECKING, VERIFICATION_SYMBOLIC_EXECUTION, or VERIFICATION_SIMULATION)
• config: a dictionary with the configuration settings to use for the verification. See here for the list of configuration options.
• program: the program to verify

Returns:

• a VerificationResult

Utility Functions

get_version

def get_version()

Get the Kratos version information as a string.

VarProvider Objects

class VarProvider(object)

A provider of fresh variables and names.

Attributes:

• added: the list of added variables

__init__

def __init__(*scopes)

Constructor.

Arguments:

• scopes: sequence of lists of variables already in use

mkvar

def mkvar(tp, name='$tmp')

Generate a unique var of the given type.

Arguments:

• tp: the type of the var
• name: (optional) custom prefix for the variable name

auxvar

def auxvar(tp)

Generate an auxiliary var of the given type. If an aux var of the requested type was already created, it will be reused.

Arguments:

• tp: the type of the var

mkname

def mkname(name='$tmp')

Generate a unique name with the given prefix.

Arguments:

• name: (optional) prefix for the name to generate

get_kratos_executable

def get_kratos_executable()

Returns the full path to the kratos executable. Raises an Exception if the path cannot be determined.