Module ir 

This module defines and implements functions for working with the Jib IR (intermediate representation) that is produced by Sail. It is a simple goto/conditional branch language, where each function can declare and use an arbitrary amount of variables.

All the IR types are parametric in the identifier type. They are initially parsed as e.g. Def<String> but then the names are interned into a symbol table (Symtab) and they are replaced by values of type Name, which is a wrapper around u32.

To conveniently initialize the IR for a Sail architecture specification see the crate::init module.

Modules

linearize

This module provides a function linearize() that converts IR from function bodies containing loops and other IR, into a linear sequence of instructions without any control flow.

serialize

This module provides serde-based serialization support for the IR. Note that the various Primop* instruction constructors cannot be serialized, as they are direct function pointers to the primop implementations. As such this module is intended to serialize and deserialize the AST only before the primops have been inserted.

ssa

This module provides a control flow graph type CFG for IR analysis and transforms, and additionally supports conversion of that CFG into single static assignment (SSA) form via CFG::ssa().

Structs

EnumMember

Name

SharedState

All symbolic evaluation happens over some (immutable) IR. The SharedState provides each worker that is performing symbolic evaluation with a convenient view into that IR.

Symtab

A Symtab is a symbol table that maps each u32 identifier used in the IR to it’s &str name and vice-versa.

Variables

An iterator over the Variable type for modifying variable usages and declarations.

Enums

AssertionMode

There are two ways to handle assertions in the Sail code, the first being to assume that they succeed (essentially treating them like assumptions in the SMT) - this is the optimistic mode. The other way is to assume that they might fail, and check each assertion to ensure that it can never fail - this is the pessimistic mode.

Def

Exp

Instr

LabeledInstr

By default each jump or goto just contains a usize offset into the instruction vector. This representation is efficient but hard to work with, so we support mapping this representation into one where any instruction can have an explicit label, and jumps point to those explicit labels, and then going back to the offset based representation for execution.

Loc

A Loc is a location that can be assigned to.

Op

Ty

UVal

A UVal is a potentially uninitialized Val.

Val

A value is either a symbolic value, represented as Symbolic(n) for where n is the identifier of the variable in the SMT solver, or one of the concrete values in this enum.

Variable

A reference to either the declaration of a variable or a usage location.

Constants

BITVECTOR_UPDATE

Special primitive for update_fbits

BV_BIT_LEFT

BV_BIT_LEFT is the field name for the left element of a bitvector,bit pair

BV_BIT_RIGHT

BV_BIT_RIGHT is the field name for the right element of a bitvector,bit pair

CURRENT_EXCEPTION

CURRENT_EXCEPTION is a global variable containing an exception with the sail type exception. It is only defined when HAVE_EXCEPTION is true.

ELF_ENTRY

The function id for the elf_entry function.

HAVE_EXCEPTION

HAVE_EXCEPTION is a global boolean variable which is true if an exception is being thrown.

INTERNAL_VECTOR_INIT

Special primitive that initializes a generic vector

INTERNAL_VECTOR_UPDATE

Special primitive used while initializing a generic vector

NULL

NULL is a global letbinding which contains the empty list

REG_DEREF

Is the function id of the reg_deref primop, that implements register dereferencing *R in Sail.

RESET_REGISTERS

RESET_REGISTERS is a special function that resets register values according to the ISA config

RETURN

When a function returns via the Instr::End instruction, the value returned is contained in the special RETURN variable.

SAIL_ASSERT

Function id for the primop implementing the assert construct in Sail.

SAIL_ASSUME

Function id for the assume primop, which is like a Sail assert but always corresponds to an raw SMT assert.

SAIL_EXCEPTION

SAIL_EXCEPTION is the Sail exception type

SAIL_EXIT

Function id for the primop implementing the exit construct in Sail.

THROW_LOCATION

THROW_LOCATION is a global variable which contains a string describing the location of the last thrown exeception.

TOP_LEVEL_LET

TOP_LEVEL_LET is a name used in backtraces when evaluating a top-level let definition

Functions

append_instrs

Append instructions from rhs into the lhs vector, leaving rhs empty (the same behavior as Vec::append).

label_instrs

Rewrites an instruction sequence with implicit offset based labels into a vector where the labels are explicit. Note that this just adds a label to every instruction which is equal to its offset. Use prune_labels to remove any labels which are not the target of any jump or goto instruction.

prune_labels

Remove labels which are not the targets of any jump or goto.

unlabel_instrs

Remove the explicit labels from instructions, and go back to using offset based jumps and gotos.

Type Aliases

Bindings

A map from identifers to potentially uninitialized values.

Reset

The idea behind the Reset type is we dynamically create what is essentially a Sail function consisting of: