Gz.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Zlib.«gzclose.c»
2import ZlibF.Zlib.«uncompr.c»
3import DiffTest.Common
4import DiffTest.Heap
5
6/-!
7Lean side of the differential test for `gzlib.c`, `gzread.c`, `gzwrite.c`, `gzclose.c` and `uncompr.c`. It calls
8the translations (the modules the proofs are about) and the file model `Zlib.GzFs`. The scenario language is the
9one of `c/gz.c` and `gen/gz.py`; a fault stops the line and prints `FAULT ...` (the C side cannot fault).
10-/
11
12open DiffTest C Zlib.GzFs Zlib.Gzlib Zlib.Gzread Zlib.Gzwrite Zlib.Gzclose
13
14/-- The heap of the tests: the static tables that the translations read are installed. -/
15def startHeap : Heap := DiffTest.fullHeap
16
17structure Env where
18  fs : Fs
19  h : Heap
20  hs : Array GzFilePtr
21
22def runG {α : Type} (e : Env) (x : G α) : Except Fault (α × Env) :=
23  match (x.run e.fs) e.h with
24  | .ok ((a, fs), h) => .ok (a, { e with fs, h })
25  | .error f => .error f
26
27def runM {α : Type} (e : Env) (x : M α) : Except Fault (α × Env) :=
28  match x e.h with
29  | .ok (a, h) => .ok (a, { e with h })
30  | .error f => .error f
31
32def toHex (bs : Array UInt8) : String := Id.run do
33  let d := "0123456789abcdef".toList.toArray
34  let mut s := ""
35  for b in bs do
36    s := s.push d[(b >>> 4).toNat]! |>.push d[(b &&& 15).toNat]!
37  return s
38
39def hexArg (s : String) : Except String (Array UInt8) :=
40  if s == "-" then pure #[] else parseHex s
41
42/-- The bytes of the block `p` points into (from its start). -/
43def blockBytes (e : Env) (p : BPtr) : Array UInt8 :=
44  match p with
45  | .ref (.blk b) _ => (e.h.bytes b).getD #[]
46  | _ => #[]
47
48def cstr (s : String) : Array UInt8 := s.toUTF8.data.push 0
49
50def fail {α : Type} (m : String) : Except Fault α := .error (.ub s!"BADINPUT {m}")
51
52def pI32 (s : String) : Except String Int32 := do return Int32.ofInt (← parseI64 s).toInt
53
54def printfFmt (k : Nat) : String :=
55  match k with
56  | 0 => "hello" | 1 => "%d" | 2 => "[%5d|%-5d|%05d]" | 3 => "%s=%s" | 4 => "%u %x %X %o"
57  | 5 => "%ld %lu" | 6 => "%c%c" | 7 => "%.3s|%10s|%-10s|" | 8 => "%+d % d %%" | 9 => "%s"
58  | 10 => "%#x %#o" | 11 => "%s" | _ => "%.0d|%.5d"
59
60def doOp (e : Env) (op : String) : Except Fault (String × Env) := do
61  let f := op.splitOn ":"
62  let c := f.headD ""
63  let hIdx : Nat := match c with
64    | "put" | "mkdir" | "dump" | "fsize" => 0
65    | _ => ((f.getD 1 "0").toNat?).getD 0
66  let g : GzFilePtr := e.hs.getD hIdx none
67  let bad {α : Type} (m : String) : Except Fault α := fail m
68  let pn (i : Nat) : Except Fault Nat :=
69    match (f.getD i "").toNat? with | some n => pure n | none => bad s!"number {op}"
70  let pi (i : Nat) : Except Fault Int :=
71    match (f.getD i "").toInt? with | some n => pure n | none => bad s!"number {op}"
72  let ph (i : Nat) : Except Fault (Array UInt8) :=
73    match hexArg (f.getD i "") with | .ok b => pure b | .error m => bad m
74  let setH (e : Env) (v : GzFilePtr) : Env := { e with hs := e.hs.set! hIdx v }
75  let ro (e : Env) (s : String) : Except Fault (BPtr × Env) := runM e (allocBytesRO (cstr s))
76  let nameB := (f.getD 1 "").toUTF8.data
77  match c with
78  | "put" => return ("p", { e with fs := e.fs.put nameB (← ph 2) })
79  | "mkdir" => return ("d", { e with fs := e.fs.mkdir nameB })
80  | "fsize" =>
81    let v ← pn 1
82    return ("z", { e with fs := { e.fs with fsizeLimit := if v == 0 then 2 ^ 62 else v } })
83  | "dump" =>
84    return (match e.fs.get? nameB with | none => "=-" | some d => "=" ++ toHex d, e)
85  | "open" =>
86    let (path, e) ← ro e (f.getD 2 "")
87    let (mode, e) ← ro e (f.getD 3 "")
88    let (r, e) ← runG e (gzopen path mode)
89    return (s!"o{if r.isSome then 1 else 0}", setH e r)
90  | "dopen" =>
91    let (mode, e) ← ro e (f.getD 4 "")
92    let k := f.getD 3 ""
93    let (r, e) ← runG e (do
94      let fd : Int32 ← if k == "bad" then pure (-1) else
95        fsOpen (f.getD 2 "").toUTF8.data (if k == "r" then 0 else if k == "w" then 1 ||| 64 ||| 512
96                       else if k == "a" then 1 ||| 64 ||| 1024 else 1 ||| 64)
97      gzdopen fd mode)
98    return (s!"D{if r.isSome then 1 else 0}", setH e r)
99  | "buffer" =>
100    let n ← pn 2
101    let (r, e) ← runM e (gzbuffer g (UInt32.ofNat n))
102    return (s!"b{r.toInt}", e)
103  | "write" =>
104    let d ← ph 2
105    let (p, e) ← runM e (allocBytes d)
106    let (r, e) ← runG e (gzwrite g p (UInt32.ofNat d.size))
107    return (s!"w{r.toInt}", e)
108  | "fwrite" =>
109    let sz ← pn 2
110    let d ← ph 3
111    let (p, e) ← runM e (allocBytes d)
112    let (r, e) ← runG e (gzfwrite p (UInt64.ofNat sz) (UInt64.ofNat (if sz == 0 then 0 else d.size / sz)) g)
113    return (s!"W{r.toNat}", e)
114  | "putc" =>
115    let v ← pi 2
116    let (r, e) ← runG e (gzputc g (Int32.ofInt v))
117    return (s!"c{r.toInt}", e)
118  | "puts" =>
119    let d ← ph 2
120    let (p, e) ← runM e (allocBytes (d.push 0))
121    let (r, e) ← runG e (gzputs g p)
122    return (s!"s{r.toInt}", e)
123  | "printf" =>
124    let k ← pn 2
125    let mut env := e
126    let mut args : List VaArg := []
127    for a in (f.drop 3) do
128      let t := (a.take 1).toString
129      let rest := (a.drop 1).toString
130      if t == "s" then
131        let d ← match hexArg rest with | .ok b => pure b | .error m => bad m
132        let (p, e') ← runM env (allocBytes (d.push 0))
133        env := e'
134        args := args ++ [VaArg.str p]
135      else
136        let v ← match rest.toInt? with | some n => pure n | none => bad s!"number {op}"
137        args := args ++ [match t with
138          | "i" => VaArg.int (Int32.ofInt v)
139          | "u" => VaArg.uint (UInt32.ofNat v.toNat)
140          | "l" => VaArg.long (Int64.ofInt v)
141          | _ => VaArg.ulong (UInt64.ofNat v.toNat)]
142    if k == 9 then
143      let (p0, env') ← runM env (allocBytes #[0])
144      env := env'
145      args := [VaArg.str p0]
146    let (fp, e) ← ro env (printfFmt k)
147    let (r, e) ← runG e (gzprintf g fp args)
148    return (s!"f{r.toInt}", e)
149  | "flush" =>
150    let v ← pi 2
151    let (r, e) ← runG e (gzflush g (Int32.ofInt v))
152    return (s!"F{r.toInt}", e)
153  | "setparams" =>
154    let l ← pi 2
155    let s ← pi 3
156    let (r, e) ← runG e (gzsetparams g (Int32.ofInt l) (Int32.ofInt s))
157    return (s!"P{r.toInt}", e)
158  | "read" =>
159    let n ← pn 2
160    let (p, e) ← runM e (allocBytes (Array.replicate (max n 1) 0))
161    let (r, e) ← runG e (gzread g p (UInt32.ofNat n))
162    let out := if r.toInt > 0 then (blockBytes e p).extract 0 r.toInt.toNat else #[]
163    return (s!"r{r.toInt}:{toHex out}", e)
164  | "fread" =>
165    let sz ← pn 2
166    let ni ← pn 3
167    let (p, e) ← runM e (allocBytes (Array.replicate (max ((sz * ni) % 2 ^ 64) 1) 0))
168    let (r, e) ← runG e (gzfread p (UInt64.ofNat sz) (UInt64.ofNat ni) g)
169    return (s!"R{r.toNat}:{toHex ((blockBytes e p).extract 0 (r.toNat * sz))}", e)
170  | "gets" =>
171    let len ← pi 2
172    let (p, e) ← runM e (allocBytes (Array.replicate (if len > 0 then len.toNat else 1) 0))
173    let (r, e) ← runG e (gzgets g p (Int32.ofInt len))
174    if r == .null then return ("gN", e)
175    let b := blockBytes e p
176    let n := (b.findIdx? (· == 0)).getD b.size
177    return (s!"g{toHex (b.extract 0 n)}", e)
178  | "getc" =>
179    let (r, e) ← runG e (gzgetc g)
180    return (s!"C{r.toInt}", e)
181  | "ungetc" =>
182    let v ← pi 2
183    let (r, e) ← runG e (gzungetc (Int32.ofInt v) g)
184    return (s!"u{r.toInt}", e)
185  | "seek" =>
186    let o ← pi 2
187    let w ← pi 3
188    let (r, e) ← runG e (gzseek g (Int64.ofInt o) (Int32.ofInt w))
189    return (s!"S{r.toInt}", e)
190  | "tell" =>
191    let (r, e) ← runM e (gztell g)
192    return (s!"T{r.toInt}", e)
193  | "offset" =>
194    let (r, e) ← runG e (gzoffset g)
195    return (s!"O{r.toInt}", e)
196  | "rewind" =>
197    let (r, e) ← runG e (gzrewind g)
198    return (s!"rw{r.toInt}", e)
199  | "eof" =>
200    let (r, e) ← runM e (gzeof g)
201    return (s!"E{r.toInt}", e)
202  | "direct" =>
203    let (r, e) ← runG e (gzdirect g)
204    return (s!"Di{r.toInt}", e)
205  | "error" =>
206    let (en, e) ← runM e (allocBytes (Array.replicate 4 0))
207    let (m, e) ← runM e (gzerror g en)
208    let num := (blockBytes e en)
209    let ev : Int32 := (num[0]!.toUInt32 ||| (num[1]!.toUInt32 <<< 8) ||| (num[2]!.toUInt32 <<< 16) |||
210      (num[3]!.toUInt32 <<< 24)).toInt32
211    -- gzerror sets *errnum only for a valid file; the C driver pre-sets 12345
212    if m == .null then
213      return ("e12345:", e)
214    let (s, e) ← runM e (cstring m)
215    return (s!"e{ev.toInt}:{toHex s}", e)
216  | "clearerr" =>
217    let (_, e) ← runM e (gzclearerr g)
218    return ("ce", e)
219  | "close" =>
220    let (r, e) ← runG e (gzclose g)
221    return (s!"x{r.toInt}", setH e none)
222  | "closer" =>
223    let (r, e) ← runG e (gzclose_r g)
224    return (s!"xr{r.toInt}", setH e none)
225  | "closew" =>
226    let (r, e) ← runG e (gzclose_w g)
227    return (s!"xw{r.toInt}", setH e none)
228  | _ => bad s!"unknown op {c}"
229
230def doLine (ops : List String) : String := Id.run do
231  let mut e : Env := { fs := {}, h := startHeap, hs := Array.replicate 4 none }
232  let mut out : List String := []
233  for o in ops do
234    match doOp e o with
235    | .ok (s, e') =>
236      out := out ++ [s]
237      e := e'
238    | .error f => return String.intercalate "|" out ++ (if out.isEmpty then "" else "|") ++ showFault f
239  return String.intercalate "|" out
240
241def handle (fn : String) (args : List String) : Except String String :=
242  match fn, args with
243  | "gz", ops => .ok (doLine ops)
244  | "unc", (hex :: dl :: rest) => do
245    let src ← hexArg hex
246    let dlen ← parseNat dl
247    let slen ← match rest with | [s] => parseNat s | _ => pure src.size
248    let r : Except Fault String := do
249      let e : Env := { fs := {}, h := startHeap, hs := #[] }
250      let (sp, e) ← runM e (allocBytes (if src.isEmpty then #[0] else src))
251      let (dp, e) ← runM e (allocBytes (Array.replicate (max dlen 1) 0))
252      let (dlp, e) ← runM e (allocBytes (Array.replicate 8 0))
253      let (slp, e) ← runM e (allocBytes (Array.replicate 8 0))
254      let (_, e) ← runM e (Zlib.Gzguts.store64 dlp (UInt64.ofNat dlen))
255      let (_, e) ← runM e (Zlib.Gzguts.store64 slp (UInt64.ofNat slen))
256      let (rc, e) ← runM e (Zlib.Uncompr.uncompress2 dp dlp sp slp)
257      let (dl2, e) ← runM e (Zlib.Gzguts.load64 dlp)
258      let (sl2, e) ← runM e (Zlib.Gzguts.load64 slp)
259      let out := (blockBytes e dp).extract 0 dl2.toNat
260      return s!"{rc.toInt}:{dl2.toNat}:{sl2.toNat}:{toHex out}"
261    match r with
262    | .ok s => .ok s
263    | .error f => .ok (showFault f)
264  | _, _ => throw s!"unknown function or wrong arity: {fn}"
265
266/-- `DiffTest.mainLoop` with a flush after every line (a crash then loses nothing). -/
267def mainFlush : IO UInt32 := do
268  let stdin ← IO.getStdin
269  let stdout ← IO.getStdout
270  let mut bad : UInt32 := 0
271  repeat
272    let line ← stdin.getLine
273    if line.isEmpty then break
274    let line := line.trimAscii.toString
275    if line.isEmpty then continue
276    match line.splitOn " " with
277    | [] => continue
278    | fn :: args =>
279      match handle fn args with
280      | .ok r => stdout.putStrLn r
281      | .error e =>
282        IO.eprintln s!"bad input line: {e}"
283        bad := 1
284        stdout.putStrLn s!"BADINPUT {e}"
285      stdout.flush
286  return bad
287
288def main : IO UInt32 := mainFlush