File size: 5,084 Bytes
f5deffb | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 | import WordDialect.Memory
/-!
# WordDialect.Machine
Universal Word IR instruction set, machine state, and the single-step operational semantics.
This file is the authoritative semantics. Every frontend translation and every backend
lowering is correct only relative to `step` as defined here.
Stack convention: `dstack` is a list whose head is the top of stack. A binary operation
on `a b` (with `b` on top) computes `a op b`, as in Forth.
Code addresses are instruction indices (`Nat`), so control flow is ISA-neutral.
Besides the return stack of code addresses (`rstack`, used only by `call`/`ret`) there is an
auxiliary data stack (`astack`) of words, used only by `tor` (move the data-stack top onto it),
`fromr` (move its top back) and `rfetch` (copy its top). `call`/`ret` never touch it, so a value
parked there survives calls and recursion; this is what Forth's `>R`, `R>`, `R@` and `DO … LOOP`
need. Taking from an empty auxiliary stack traps `returnUnderflow`.
Registers are an unbounded file of virtual registers (`Nat → Word n`); mapping them onto
physical registers is a backend concern.
-/
namespace WordDialect
inductive Instr (n : Nat) where
| word (w : Word n)
| ptr (p : Ptr n)
| load | store
| add | sub | mul | div | sdiv
| and | or | xor | not
| shl | shr | rotl | rotr
| cmp (c : Cond)
| select
| jmp (target : Nat)
| branch (target : Nat)
| call (target : Nat)
| ret
| push (r : Nat)
| pop (r : Nat)
| dup | drop | swap | over | rot
| tor | fromr | rfetch
| halt
inductive Trap where
| stackUnderflow
| badAddress
| divideByZero
| badPc
| returnUnderflow
deriving DecidableEq, Repr
structure State (n : Nat) where
pc : Nat
dstack : List (Word n)
rstack : List Nat
astack : List (Word n)
regs : Nat → Word n
mem : Memory n
inductive Outcome (n : Nat) where
| next (s : State n)
| halted (s : State n)
| trapped (t : Trap)
abbrev Prog (n : Nat) := List (Instr n)
namespace State
/-- Continue at `pc + 1` with a new data stack. -/
def fall {n : Nat} (s : State n) (d : List (Word n)) : Outcome n :=
.next { s with pc := s.pc + 1, dstack := d }
def setReg {n : Nat} (regs : Nat → Word n) (r : Nat) (v : Word n) : Nat → Word n :=
fun i => if i = r then v else regs i
end State
/-- Semantics of one instruction in state `s` (the instruction is located at `s.pc`). -/
def exec {n : Nat} (i : Instr n) (s : State n) : Outcome n :=
match i, s.dstack with
| .word w, d => s.fall (w :: d)
| .ptr p, d => s.fall (p.toWord :: d)
| .load, a :: d =>
match s.mem.read? a with
| some v => s.fall (v :: d)
| none => .trapped .badAddress
| .store, a :: v :: d =>
match s.mem.write? a v with
| some m => .next { s with pc := s.pc + 1, dstack := d, mem := m }
| none => .trapped .badAddress
| .add, b :: a :: d => s.fall ((a + b) :: d)
| .sub, b :: a :: d => s.fall ((a - b) :: d)
| .mul, b :: a :: d => s.fall ((a * b) :: d)
| .sdiv, b :: a :: d =>
if b = 0#n then .trapped .divideByZero else s.fall (a.sdiv b :: d)
| .div, b :: a :: d =>
if b = 0#n then .trapped .divideByZero else s.fall (a.udiv b :: d)
| .and, b :: a :: d => s.fall ((a &&& b) :: d)
| .or, b :: a :: d => s.fall ((a ||| b) :: d)
| .xor, b :: a :: d => s.fall ((a ^^^ b) :: d)
| .not, a :: d => s.fall ((~~~a) :: d)
| .shl, b :: a :: d => s.fall (Word.shl a b :: d)
| .shr, b :: a :: d => s.fall (Word.shr a b :: d)
| .rotl, b :: a :: d => s.fall (Word.rotl a b :: d)
| .rotr, b :: a :: d => s.fall (Word.rotr a b :: d)
| .cmp c, b :: a :: d => s.fall (Word.ofBool (c.eval a b) :: d)
| .select, c :: y :: x :: d => s.fall ((if Word.isTrue c then x else y) :: d)
| .jmp t, _ => .next { s with pc := t }
| .branch t, c :: d =>
if Word.isTrue c then .next { s with pc := t, dstack := d }
else s.fall d
| .call t, _ => .next { s with pc := t, rstack := (s.pc + 1) :: s.rstack }
| .ret, _ =>
match s.rstack with
| a :: rs => .next { s with pc := a, rstack := rs }
| [] => .trapped .returnUnderflow
| .push r, d => s.fall (s.regs r :: d)
| .pop r, v :: d =>
.next { s with pc := s.pc + 1, dstack := d, regs := State.setReg s.regs r v }
| .dup, a :: d => s.fall (a :: a :: d)
| .drop, _ :: d => s.fall d
| .swap, b :: a :: d => s.fall (a :: b :: d)
| .over, b :: a :: d => s.fall (a :: b :: a :: d)
| .rot, c :: b :: a :: d => s.fall (a :: c :: b :: d)
| .tor, a :: d => .next { s with pc := s.pc + 1, dstack := d, astack := a :: s.astack }
| .fromr, d =>
match s.astack with
| a :: as => .next { s with pc := s.pc + 1, dstack := a :: d, astack := as }
| [] => .trapped .returnUnderflow
| .rfetch, d =>
match s.astack with
| a :: _ => s.fall (a :: d)
| [] => .trapped .returnUnderflow
| .halt, _ => .halted s
| _, _ => .trapped .stackUnderflow
def step {n : Nat} (p : Prog n) (s : State n) : Outcome n :=
match p[s.pc]? with
| none => .trapped .badPc
| some i => exec i s
end WordDialect
|