Ptr.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Runtime.Monad
2
3/-!
4# Runtime: pointers into arrays
5
6Trusted base of every translation; see `docs/trusted-base.md`.
7
8A pointer is `Ptr R`: null, or an array (where it lives is the reference `R`: a heap block, an array inside a struct,
9a static table) and an index. Every primitive is written once, for every `R`, through the class `Space`. Each one
10says which C operation it models and when it faults. Byte pointers are `BPtr = Ptr BRef` (see `Schema.lean`), and
11`load8`, `index8` and `store8` are their names in the translation. The functions of the C library (`memcpy`,
12`memset`, `strlen`, `malloc`, `free`) are in `Libc.lean`.
13-/
14
15namespace C
16
17section generic
18variable {R T : Type} [Space Heap R T]
19
20/-- `p + k`. Faults unless the result is an index of the array or one past its end. `NULL + 0` is `NULL` (allowed
21by decision, although C17 leaves it undefined; see `docs/trusted-base.md`); the pointer must point to a live array.
22It checks the result only: a pointer built by hand outside its array (`Ptr.ref r off` with `off` beyond the end) is
23not caught here. The translations obtain pointers from `Ptr.add` and from the schema, which never form one. -/
24def Ptr.add (p : Ptr R) (k : Int) : M (Ptr R) := fun h =>
25  match p with
26  | .null => if k = 0 then .ok (.null, h) else .error (.ub "arithmetic on a null pointer")
27  | .ref r off =>
28    match Space.get h r with
29    | none => .error (.ub "arithmetic on a dangling pointer")
30    | some a =>
31      if 0 ≤ (off : Int) + k ∧ (off : Int) + k ≤ (a.size : Int) then .ok (.ref r ((off : Int) + k).toNat, h)
32      else .error (.ub "pointer arithmetic outside its object")
33
34/-- `*p`. Faults if `p` is null, dangling, or outside its array (one past the end is not readable). -/
35def Ptr.load (p : Ptr R) : M T := fun h =>
36  match p with
37  | .null => .error (.ub "null dereference")
38  | .ref r off =>
39    match Space.get h r with
40    | none => .error (.ub "read through a dangling pointer")
41    | some a => if hk : off < a.size then .ok (a[off], h) else .error (.ub "read outside its object")
42
43/-- `p[i]`, that is `*(p + i)`. -/
44def Ptr.index (p : Ptr R) (i : Int) : M T := do
45  Ptr.load (← p.add i)
46
47/-- `*p = v`. Faults if `p` is null, dangling, outside its array, or the array is read-only. -/
48def Ptr.store (p : Ptr R) (v : T) : M Unit := fun h =>
49  match p with
50  | .null => .error (.ub "null store")
51  | .ref r off =>
52    match Space.get h r with
53    | none => .error (.ub "store through a dangling pointer")
54    | some a =>
55      if Space.ro h r then .error (.ub "store into a read-only object")
56      else if off < a.size then .ok ((), Space.modify h r (fun a => a.set! off v))
57      else .error (.ub "store outside its object")
58
59/-- `p - q` (a `ptrdiff_t`). Faults unless both point into the same live array and the difference is a `ptrdiff_t`
60(`NULL - NULL` is a fault although C23 defines it as 0). -/
61def Ptr.diff [DecidableEq R] (p q : Ptr R) : M Int64 := fun h =>
62  match p, q with
63  | .ref r1 o1, .ref r2 o2 =>
64    if r1 = r2 then
65      match Space.get h r1 with
66      | some a =>
67        if o1 ≤ a.size ∧ o2 ≤ a.size then
68          if -(2 ^ 63 : Int) ≤ (o1 : Int) - (o2 : Int) ∧ (o1 : Int) - (o2 : Int) < 2 ^ 63 then
69            .ok (Int64.ofInt ((o1 : Int) - (o2 : Int)), h)
70          else .error (.ub "pointer difference is not a ptrdiff_t")
71        else .error (.ub "pointer outside its object")
72      | none => .error (.ub "difference of dangling pointers")
73    else .error (.ub "difference of pointers into different objects")
74  | _, _ => .error (.ub "difference of null pointers")
75
76/-- `p < q`. Faults unless both point into the same live array (relational comparison of unrelated pointers is
77undefined). -/
78def Ptr.lt [DecidableEq R] (p q : Ptr R) : M Bool := fun h =>
79  match p, q with
80  | .ref r1 o1, .ref r2 o2 =>
81    if r1 = r2 then
82      match Space.get h r1 with
83      | some a =>
84        if o1 ≤ a.size ∧ o2 ≤ a.size then .ok (decide (o1 < o2), h)
85        else .error (.ub "pointer outside its object")
86      | none => .error (.ub "comparison of dangling pointers")
87    else .error (.ub "comparison of pointers into different objects")
88  | _, _ => .error (.ub "comparison of null pointers")
89
90/-- `p <= q`; the same faults as `Ptr.lt`. -/
91def Ptr.le [DecidableEq R] (p q : Ptr R) : M Bool := do
92  return !(← Ptr.lt q p)
93
94/-! ### Rules -/
95
96theorem Ptr.add_ok {h : Heap} {r : R} {a : Array T} {off : Nat} {k : Int}
97    (hg : Space.get h r = some a) (h0 : 0 ≤ (off : Int) + k) (h1 : (off : Int) + k ≤ (a.size : Int)) :
98    OkOn h (Ptr.add (Ptr.ref r off) k) (Ptr.ref r ((off : Int) + k).toNat) := by
99  unfold OkOn Ptr.add; simp [hg, h0, h1]
100
101theorem Ptr.add_nat_ok {h : Heap} {r : R} {a : Array T} {off n : Nat}
102    (hg : Space.get h r = some a) (h1 : off + n ≤ a.size) :
103    OkOn h (Ptr.add (Ptr.ref r off) (n : Int)) (Ptr.ref r (off + n)) := by
104  have := Ptr.add_ok (a := a) (off := off) (k := (n : Int)) hg (by omega) (by omega)
105  have e : ((off : Int) + (n : Int)).toNat = off + n := by omega
106  rwa [e] at this
107
108theorem Ptr.sub_nat_ok {h : Heap} {r : R} {a : Array T} {off n : Nat}
109    (hg : Space.get h r = some a) (hn : n ≤ off) (h1 : off ≤ a.size) :
110    OkOn h (Ptr.add (Ptr.ref r off) (-(n : Int))) (Ptr.ref r (off - n)) := by
111  have := Ptr.add_ok (a := a) (off := off) (k := -(n : Int)) hg (by omega) (by omega)
112  have e : ((off : Int) + -(n : Int)).toNat = off - n := by omega
113  rwa [e] at this
114
115theorem Ptr.add_null_zero {h : Heap} : OkOn h (Ptr.add (Ptr.null : Ptr R) 0) Ptr.null := by
116  unfold OkOn Ptr.add; simp
117
118theorem Ptr.load_ok {h : Heap} {r : R} {a : Array T} {off : Nat}
119    (hg : Space.get h r = some a) (hlt : off < a.size) :
120    OkOn h (Ptr.load (Ptr.ref r off)) a[off] := by
121  unfold OkOn Ptr.load; simp [hg, hlt]
122
123theorem Ptr.index_ok {h : Heap} {r : R} {a : Array T} {off i : Nat}
124    (hg : Space.get h r = some a) (hlt : off + i < a.size) :
125    OkOn h (Ptr.index (Ptr.ref r off) (i : Int)) a[off + i] := by
126  unfold Ptr.index
127  refine OkOn.bind (Ptr.add_nat_ok hg (by omega)) ?_
128  exact Ptr.load_ok hg hlt
129
130theorem Ptr.store_ok {h : Heap} {r : R} {a : Array T} {off : Nat} {v : T}
131    (hg : Space.get h r = some a) (hro : Space.ro h r = false) (hlt : off < a.size) :
132    Ptr.store (Ptr.ref r off) v h = .ok ((), Space.put h r (a.set! off v)) := by
133  simp [Ptr.store, hg, hro, hlt, Space.modify_eq _ _ _ _ hg]
134
135theorem Ptr.diff_ok [DecidableEq R] {h : Heap} {r : R} {a : Array T} {o1 o2 : Nat}
136    (hg : Space.get h r = some a) (h1 : o1 ≤ a.size) (h2 : o2 ≤ a.size)
137    (hr : -(2 ^ 63 : Int) ≤ (o1 : Int) - (o2 : Int) ∧ (o1 : Int) - (o2 : Int) < 2 ^ 63) :
138    OkOn h (Ptr.diff (Ptr.ref r o1) (Ptr.ref r o2)) (Int64.ofInt ((o1 : Int) - (o2 : Int))) := by
139  unfold OkOn Ptr.diff; simp [hg, h1, h2]; omega
140
141theorem Ptr.lt_ok [DecidableEq R] {h : Heap} {r : R} {a : Array T} {o1 o2 : Nat}
142    (hg : Space.get h r = some a) (h1 : o1 ≤ a.size) (h2 : o2 ≤ a.size) :
143    OkOn h (Ptr.lt (Ptr.ref r o1) (Ptr.ref r o2)) (decide (o1 < o2)) := by
144  unfold OkOn Ptr.lt; simp [hg, h1, h2]
145end generic
146
147/-! ## Byte pointers -/
148
149/-- `*p` for an `unsigned char *`. -/
150abbrev load8 (p : BPtr) : M UInt8 := Ptr.load p
151/-- `p[i]` for an `unsigned char *`. -/
152abbrev index8 (p : BPtr) (i : Int) : M UInt8 := Ptr.index p i
153/-- `*p = v` for an `unsigned char *`. -/
154abbrev store8 (p : BPtr) (v : UInt8) : M Unit := Ptr.store p v
155theorem load8_ok {h : Heap} {blk off : Nat} {bytes : Array UInt8} (hb : h.bytes blk = some bytes)
156    (hlt : off < bytes.size) : OkOn h (load8 (.ref (.blk blk) off)) bytes[off] :=
157  Ptr.load_ok hb hlt
158
159theorem index8_ok {h : Heap} {blk off i : Nat} {bytes : Array UInt8} (hb : h.bytes blk = some bytes)
160    (hlt : off + i < bytes.size) : OkOn h (index8 (.ref (.blk blk) off) i) bytes[off + i] :=
161  Ptr.index_ok hb hlt
162
163/-- A store into a read-only block is a fault. -/
164theorem store_readonly {h : Heap} {b off : Nat} {a : Array UInt8} {v : UInt8} (hb : h.bytes b = some a) (hro : h.ro b = true) :
165    store8 (.ref (.blk b) off) v h = .error (.ub "store into a read-only object") := by
166  simp [store8, Ptr.store, hb, hro]
167
168end C