Module isla_lib::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 Definitions

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: