File size: 7,548 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 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 | import WordDialect
import WordIR
/-!
# BCPL.Semantics
Abstract syntax and reference semantics of the supported BCPL subset. Defined directly on
word-addressed memory, with no reference to the machine or the IR; the lowering is proved
correct against this definition.
BCPL is typeless: every value is a word, a variable is a memory cell, and `!e` / `@x` are
word indirection and address-of. Variable `x` lives at address `addr x` (the global vector).
Conventions:
* Relational operators yield BCPL truth values: `-1` (true) and `0` (false).
* A condition is true iff its value is nonzero.
* `/` is signed division truncating toward zero; division by zero traps.
* `<<` and `>>` are logical shifts.
* Order of evaluation is fixed: left operand before right; in `lhs := rhs`, the right-hand
side is evaluated before an indirect left-hand side.
-/
namespace WordDialect
namespace BCPL
open IR
abbrev Var := Nat
inductive BinOp where
| add | sub | mul | div
| and | or | neqv
| shl | shr
| eq | ne | lt | gt | le | ge
inductive UnOp where
| neg | not
inductive Expr where
| num (z : Int)
| var (x : Var)
| addrOf (x : Var)
| rv (e : Expr)
| un (o : UnOp) (e : Expr)
| bin (o : BinOp) (a b : Expr)
inductive LVal where
| var (x : Var)
| rv (e : Expr)
inductive Stmt where
| skip
| assign (l : LVal) (e : Expr)
| seq (a b : Stmt)
| test (c : Expr) (t e : Stmt)
| while (c : Expr) (body : Stmt)
def readW {n : Nat} (m : Memory n) (a : Word n) : Except Trap (Word n) :=
match m.read? a with
| some v => .ok v
| none => .error .badAddress
def writeW {n : Nat} (m : Memory n) (a v : Word n) : Except Trap (Memory n) :=
match m.write? a v with
| some m' => .ok m'
| none => .error .badAddress
namespace BinOp
def sem {n : Nat} : BinOp → Word n → Word n → Except Trap (Word n)
| .add, a, b => .ok (a + b)
| .sub, a, b => .ok (a - b)
| .mul, a, b => .ok (a * b)
| .div, a, b => if b = 0#n then .error .divideByZero else .ok (a.sdiv b)
| .and, a, b => .ok (a &&& b)
| .or, a, b => .ok (a ||| b)
| .neqv, a, b => .ok (a ^^^ b)
| .shl, a, b => .ok (Word.shl a b)
| .shr, a, b => .ok (Word.shr a b)
| .eq, a, b => .ok (flag (Cond.eval .eq a b))
| .ne, a, b => .ok (flag (Cond.eval .ne a b))
| .lt, a, b => .ok (flag (Cond.eval .slt a b))
| .gt, a, b => .ok (flag (Cond.eval .sgt a b))
| .le, a, b => .ok (flag (Cond.eval .sle a b))
| .ge, a, b => .ok (flag (Cond.eval .sge a b))
end BinOp
namespace UnOp
def sem {n : Nat} : UnOp → Word n → Word n
| .neg, v => 0#n - v
| .not, v => ~~~v
end UnOp
/-- Expression evaluation. Expressions read memory but never write it. -/
def evalE {n : Nat} (addr : Var → Word n) : Expr → Memory n → Except Trap (Word n)
| .num z, _ => .ok (BitVec.ofInt n z)
| .var x, m => readW m (addr x)
| .addrOf x, _ => .ok (addr x)
| .rv e, m =>
match evalE addr e m with
| .error t => .error t
| .ok a => readW m a
| .un o e, m =>
match evalE addr e m with
| .error t => .error t
| .ok v => .ok (o.sem v)
| .bin o a b, m =>
match evalE addr a m with
| .error t => .error t
| .ok va =>
match evalE addr b m with
| .error t => .error t
| .ok vb => o.sem va vb
def assignSem {n : Nat} (addr : Var → Word n) (l : LVal) (e : Expr) (m : Memory n) :
Except Trap (Memory n) :=
match evalE addr e m with
| .error t => .error t
| .ok v =>
match l with
| .var x => writeW m (addr x) v
| .rv a =>
match evalE addr a m with
| .error t => .error t
| .ok a' => writeW m a' v
/-- Big-step statement semantics. Non-terminating runs have no derivation. -/
inductive Exec {n : Nat} (addr : Var → Word n) : Stmt → Memory n → Except Trap (Memory n) → Prop where
| skip {m} : Exec addr .skip m (.ok m)
| assign {l e m r} : assignSem addr l e m = r → Exec addr (.assign l e) m r
| seqOk {a b m m1 r} : Exec addr a m (.ok m1) → Exec addr b m1 r → Exec addr (.seq a b) m r
| seqErr {a b m t} : Exec addr a m (.error t) → Exec addr (.seq a b) m (.error t)
| testErr {c t e m x} : evalE addr c m = .error x → Exec addr (.test c t e) m (.error x)
| testTrue {c t e m v r} :
evalE addr c m = .ok v → Word.isTrue v = true → Exec addr t m r → Exec addr (.test c t e) m r
| testFalse {c t e m v r} :
evalE addr c m = .ok v → Word.isTrue v = false → Exec addr e m r → Exec addr (.test c t e) m r
| whileErr {c body m x} : evalE addr c m = .error x → Exec addr (.while c body) m (.error x)
| whileExit {c body m v} :
evalE addr c m = .ok v → Word.isTrue v = false → Exec addr (.while c body) m (.ok m)
| whileBodyErr {c body m v x} :
evalE addr c m = .ok v → Word.isTrue v = true → Exec addr body m (.error x) →
Exec addr (.while c body) m (.error x)
| whileAgain {c body m v m1 r} :
evalE addr c m = .ok v → Word.isTrue v = true → Exec addr body m (.ok m1) →
Exec addr (.while c body) m1 r → Exec addr (.while c body) m r
/-- The statement semantics is functional: a statement and a memory determine the result. -/
theorem Exec.deterministic {n : Nat} {addr : Var → Word n} {s : Stmt} {m : Memory n}
{r₁ r₂ : Except Trap (Memory n)} (h₁ : Exec addr s m r₁) (h₂ : Exec addr s m r₂) :
r₁ = r₂ := by
induction h₁ generalizing r₂ with
| skip => cases h₂; rfl
| assign hr => cases h₂ with | assign hr' => rw [← hr, ← hr']
| seqOk ha hb iha ihb =>
cases h₂ with
| seqOk ha' hb' => have := iha ha'; cases this; exact ihb hb'
| seqErr ha' => have := iha ha'; cases this
| seqErr ha iha =>
cases h₂ with
| seqOk ha' _ => have := iha ha'; cases this
| seqErr ha' => have := iha ha'; cases this; rfl
| testErr hc =>
cases h₂ with
| testErr hc' => rw [hc] at hc'; cases hc'; rfl
| testTrue hc' => rw [hc] at hc'; cases hc'
| testFalse hc' => rw [hc] at hc'; cases hc'
| testTrue hc ht _ ih =>
cases h₂ with
| testErr hc' => rw [hc] at hc'; cases hc'
| testTrue hc' _ h' => exact ih h'
| testFalse hc' hf _ => rw [hc] at hc'; cases hc'; rw [ht] at hf; cases hf
| testFalse hc hf _ ih =>
cases h₂ with
| testErr hc' => rw [hc] at hc'; cases hc'
| testTrue hc' ht _ => rw [hc] at hc'; cases hc'; rw [hf] at ht; cases ht
| testFalse hc' _ h' => exact ih h'
| whileErr hc =>
cases h₂ with
| whileErr hc' => rw [hc] at hc'; cases hc'; rfl
| whileExit hc' => rw [hc] at hc'; cases hc'
| whileBodyErr hc' => rw [hc] at hc'; cases hc'
| whileAgain hc' => rw [hc] at hc'; cases hc'
| whileExit hc hf =>
cases h₂ with
| whileErr hc' => rw [hc] at hc'; cases hc'
| whileExit => rfl
| whileBodyErr hc' ht => rw [hc] at hc'; cases hc'; rw [hf] at ht; cases ht
| whileAgain hc' ht => rw [hc] at hc'; cases hc'; rw [hf] at ht; cases ht
| whileBodyErr hc ht hb ihb =>
cases h₂ with
| whileErr hc' => rw [hc] at hc'; cases hc'
| whileExit hc' hf => rw [hc] at hc'; cases hc'; rw [ht] at hf; cases hf
| whileBodyErr _ _ hb' => have := ihb hb'; cases this; rfl
| whileAgain _ _ hb' => have := ihb hb'; cases this
| whileAgain hc ht hb hl ihb ihl =>
cases h₂ with
| whileErr hc' => rw [hc] at hc'; cases hc'
| whileExit hc' hf => rw [hc] at hc'; cases hc'; rw [ht] at hf; cases hf
| whileBodyErr _ _ hb' => have := ihb hb'; cases this
| whileAgain _ _ hb' hl' => have := ihb hb'; cases this; exact ihl hl'
end BCPL
end WordDialect
|