AbstractSyntax

This module provides core abstract-syntax types of the MRiscX assembly language.

@[reducible, inline]

abbrev Register : Type

Purpose of this file: This file establishes the syntax of the MRiscX assembly language, encompassing the definition of instructions, labels, registers, memory and machine states. Given that the instructionsMap, labels, registers, and memory are represented as maps, it may be beneficial to review the contents of the file Maps.lean beforehand.

Next we define some Datatypes for the map keys. This is because it makes it easier to understand which map is being processed. Firstly a register, which will hold a value

Equations

• Register = UInt64

@[implicit_reducible]

instance instCoeRegisterUInt64 : Coe Register UInt64

Equations

• instCoeRegisterUInt64 = { coe := fun (c : Register) => c }

@[reducible, inline]

abbrev MemoryAddress : Type

Next, the memory address. This address will point to a certain address in the memory which holds some value

Equations

• MemoryAddress = UInt64

@[reducible, inline]

abbrev InstructionIndex : Type

The InstructionIndex is a serial number which points to a instruction in the stack

Equations

• InstructionIndex = UInt64

@[reducible, inline]

abbrev ProgramCounter : Type

The program counter: the index of the instruction currently being executed.

Equations

• ProgramCounter = UInt64

def InstructionMap : Type

A total map which holds the instructions of a program tied to a unsigned 64-bit integers as InstructionIndex. The default value of this map is the instruction Instr.Panic.

IM := {uint64_1 ↦ instr_1, uint64_2 ↦ instr_2, ..., uint64_n ↦ instr_n} / default: Instr.IPanic

Equations

• InstructionMap = TMap InstructionIndex Instr

@[implicit_reducible]

instance instReprInstructionMap : Repr InstructionMap

Equations

• instReprInstructionMap = { reprPrec := instReprInstructionMap._aux_1 }

@[implicit_reducible]

instance instInhabitedInstructionMap : Inhabited InstructionMap

Equations

• instInhabitedInstructionMap = { default := instInhabitedInstructionMap._aux_1 }

@[implicit_reducible]

instance instToStringInstructionMap : ToString InstructionMap

Equations

• instToStringInstructionMap = { toString := fun (instrMap : InstructionMap) => reprStr instrMap }

def EmptyInstructionMap : InstructionMap

Empty InstructionMap which serves as standard InstructionMap

Equations

• EmptyInstructionMap = TMap.empty Instr.Panic

def LabelMap : Type

A partial map LabelMap, which holds all the Labels as key and links these to an unsigned 64-bit integers.

LM := {l_1 ↦ uint64_1, l_2 ↦ uint64_2, ..., l_n ↦ uint64_n}

Equations

• LabelMap = PMap String UInt64

@[implicit_reducible]

instance instReprLabelMap : Repr LabelMap

Equations

• instReprLabelMap = { reprPrec := instReprLabelMap._aux_1 }

@[implicit_reducible]

instance instInhabitedLabelMap : Inhabited LabelMap

Equations

• instInhabitedLabelMap = { default := instInhabitedLabelMap._aux_1 }

@[implicit_reducible]

instance instToStringLabelMap : ToString LabelMap

Equations

• instToStringLabelMap = { toString := fun (labelMap : LabelMap) => reprStr labelMap }

def EmptyLabels : LabelMap

Empty LabelMap which serves as standard LabelMap

Equations

• EmptyLabels = PMap.empty

structure Code : Type

The InstructionMap and the LabelMap are combined into a single structure, which is refered as Code.

• instructionMap : InstructionMap

  The instruction map, associating each instruction index with an instruction.

• labels : LabelMap

  The label map, associating each label name with its target index.

def DefaultCode : Code

A default instance of Code, containing an empty InstructionMap and an empty LabelMap.

Equations

• DefaultCode = { instructionMap := EmptyInstructionMap, labels := EmptyLabels }

def Code.setCMap (m : Code) (c : InstructionMap) : Code

Replace the instruction map of a Code with c.

Equations

• m.setCMap c = { instructionMap := c, labels := m.labels }

def Code.setLabels (m : Code) (l : LabelMap) : Code

Replace the label map of a Code with l.

Equations

• m.setLabels l = { instructionMap := m.instructionMap, labels := l }

def Code.addMultipleLabels (m : Code) (l : List (String × UInt64)) : Code

Add a list of (name, index) label bindings to a Code.

Equations

• m.addMultipleLabels [] = m
• m.addMultipleLabels (h :: t) = { instructionMap := m.instructionMap, labels := p(h.fst ↦ h.snd; m.labels) }.addMultipleLabels t

def Code.addCMap (m : Code) (id : InstructionIndex) (v : Instr) : Code

Insert an instruction v at index id into the instruction map of a Code.

Equations

• m.addCMap id v = { instructionMap := (id ↦ v; m.instructionMap), labels := m.labels }

def Code.addLabels (m : Code) (id : String) (v : UInt64) : Code

Insert a label id ↦ v into the label map of a Code.

Equations

• m.addLabels id v = { instructionMap := m.instructionMap, labels := p(id ↦ v; m.labels) }

def Code.addMaps (m : Code) (id_c : InstructionIndex) (v_c : Instr) (id_l : String) (v_l : UInt64) : Code

Insert both an instruction and a label binding into a Code.

Equations

• m.addMaps id_c v_c id_l v_l = { instructionMap := (id_c ↦ v_c; m.instructionMap), labels := p(id_l ↦ v_l; m.labels) }

def Code.setMaps (m : Code) (c : InstructionMap) (l : LabelMap) : Code

Replace both the instruction map and the label map of a Code.

Equations

• m.setMaps c l = (m.setCMap c).setLabels l

def Code.getLabel (m : Code) (l : String) : Option UInt64

Look up the target index of a label in a Code.

Equations

• m.getLabel l = PMap.get m.labels l

def Code.getInstrAt (m : Code) (l : UInt64) : Instr

Look up the instruction stored at index l in a Code.

Equations

• m.getInstrAt l = TMap.get m.instructionMap l

def Registers : Type

Definiton of the registers R := {r_1 ↦ w_1, … , r_k ↦ w_k}

Equations

• Registers = TMap Register UInt64

@[implicit_reducible]

instance instReprRegisters : Repr Registers

Equations

• instReprRegisters = { reprPrec := instReprRegisters._aux_1 }

def EmptyRegisters : Registers

RegisterMap with default value 0

R := {r_1 ↦ w_1, … , r_k ↦ w_k; 0}

Equations

• EmptyRegisters = TMap.empty 0

def Memory : Type

Definiton of the memory M := {m_1 ↦ w_1, … , m_k ↦ w_k}

Equations

• Memory = TMap MemoryAddress UInt64

@[implicit_reducible]

instance instReprMemory : Repr Memory

Equations

• instReprMemory = { reprPrec := instReprMemory._aux_1 }

def EmptyMemory : Memory

MemoryMap with default value 0

M := {m_1 ↦ w_1, … , m_k ↦ w_k; 0}

Equations

• EmptyMemory = TMap.empty 0