source: src/LIN/LINToASM.ma @ 2946

Last change on this file since 2946 was 2946, checked in by tranquil, 7 years ago

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File size: 18.5 KB
Line 
1include "utilities/BitVectorTrieSet.ma".
2include "utilities/state.ma".
3
4include "ASM/Util.ma".
5include "ASM/ASM.ma".
6
7include "LIN/LIN.ma".
8
9
10
11(* utilities to provide Identifier's and addresses  *)
12record ASM_universe (globals : list ident) : Type[0] :=
13{ id_univ : universe ASMTag
14; current_funct : ident
15; ident_map : identifier_map SymbolTag Identifier
16; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier)
17; address_map : identifier_map SymbolTag Word
18; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map
19}.
20
21definition new_ASM_universe :
22∀p : joint_program LIN.ASM_universe (prog_var_names … p) ≝
23λp.
24  let globals_addr_internal ≝
25   λres_offset : identifier_map SymbolTag Word × Z.
26   λx_size: ident × region × (list init_data).
27    let 〈res, offset〉 ≝ res_offset in
28    let 〈x, region, data〉 ≝ x_size in
29      〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat (size_init_data_list data)〉 in
30  let addresses ≝ foldl ?? globals_addr_internal 〈empty_map …, -(globals_stacksize … p)〉 (prog_vars ?? p) in
31mk_ASM_universe ? (mk_universe … one)
32  (an_identifier … one (* dummy *))
33  (empty_map …) (empty_map …)
34  (\fst addresses) ?.
35@hide_prf
36normalize nodelta
37cases p -p * #vars #functs #main #cost_init
38#i #H
39letin init_val ≝ (〈empty_map ? Word, -(globals_stacksize ??)〉)
40cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
41[ %2{H} ] -H
42lapply i -i lapply init_val -init_val elim vars -vars
43[2: ** #id #r #v #tl #IH ] #init_val #i
44[2: * [2: * ] #H @H ]
45* [2: #H cases (orb_Prop_true … H) -H ] #H
46@IH
47[ %1 cases init_val normalize nodelta #init_map #off
48  >(proj1 ?? (eqb_true ???) H) @mem_set_add_id
49| %2{H}
50| %1 cases init_val in H; normalize nodelta #init_map #off #H
51  >mem_set_add @orb_Prop_r @H
52]
53qed.
54
55definition Identifier_of_label :
56  ∀globals.label → state_monad (ASM_universe globals) Identifier ≝
57λg,l,u.
58let current ≝ current_funct … u in
59let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in
60let 〈id, univ, lmap〉 ≝
61  match lookup … lmap l with
62  [ Some id ⇒ 〈id, id_univ … u, lmap〉
63  | None ⇒
64    let 〈id, univ〉 ≝ fresh … (id_univ … u) in
65    〈id, univ, add … lmap l id〉
66  ] in
67〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
68  (address_map … u) (globals_are_in … u), id〉.
69
70definition Identifier_of_ident :
71  ∀globals.ident → state_monad (ASM_universe globals) Identifier ≝
72λg,i,u.
73let imap ≝ ident_map … u in
74let 〈id, univ, imap〉 ≝
75  match lookup … imap i with
76  [ Some id ⇒ 〈id, id_univ … u, imap〉
77  | None ⇒
78    let 〈id, univ〉 ≝ fresh … (id_univ … u) in
79    〈id, univ, add … imap i id〉
80  ] in
81〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
82  (address_map … u) (globals_are_in … u), id〉.
83
84definition start_funct_translation :
85  ∀globals.(ident × (joint_function LIN globals)) →
86    state_monad (ASM_universe globals) unit ≝
87  λg,id_f,u.
88    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
89      (address_map … u) (globals_are_in … u), it〉.
90
91definition address_of_ident :
92  ∀globals,i.i ∈ globals → state_monad (ASM_universe globals) [[ data16 ]] ≝
93λglobals,i,prf,u.
94〈u, DATA16 (lookup_safe … (globals_are_in … u … prf))〉. @I qed.
95
96definition ASM_fresh :
97  ∀globals.state_monad (ASM_universe globals) Identifier ≝
98λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
99〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
100  (address_map … u) (globals_are_in … u), id〉.
101
102definition register_address: Register → [[ acc_a; direct; registr ]] ≝
103  λr: Register.
104    match r with
105    [ Register00 ⇒ REGISTER [[ false; false; false ]]
106    | Register01 ⇒ REGISTER [[ false; false; true ]]
107    | Register02 ⇒ REGISTER [[ false; true; false ]]
108    | Register03 ⇒ REGISTER [[ false; true; true ]]
109    | Register04 ⇒ REGISTER [[ true; false; false ]]
110    | Register05 ⇒ REGISTER [[ true; false; true ]]
111    | Register06 ⇒ REGISTER [[ true; true; false ]]
112    | Register07 ⇒ REGISTER [[ true; true; true ]]
113    | RegisterA ⇒ ACC_A
114    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
115    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
116    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
117    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
118    ]. @I qed.
119
120definition vector_cast :
121∀A,n,m.A → Vector A n → Vector A m ≝
122λA,n,m,dflt,v.
123If leb n m then with prf do
124  replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
125else with prf do
126  \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
127lapply prf @(leb_elim n)
128[2,3: #_ * #abs elim (abs I) ]
129#H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …))
130[ assumption ]
131@(transitive_le … (not_le_to_lt … H)) %2 %1
132qed.
133
134definition arg_address : hdw_argument →
135  [[ acc_a ; direct ; registr ; data ]] ≝
136  λa.
137  match a
138  with
139  [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]])
140  | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]])
141  ].
142  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I
143qed.
144
145definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
146
147definition data_of_int ≝ λbv. DATA bv.
148definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
149definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
150
151(* TODO: check and change to free bit *)
152definition asm_other_bit ≝ BIT_ADDR (zero_byte).
153
154definition translate_statements :
155  ∀globals.
156  joint_statement LIN globals →
157  state_monad (ASM_universe globals) pseudo_instruction ≝
158  λglobals,statement.
159  match statement with
160  [ final instr ⇒
161    match instr with
162    [ GOTO lbl ⇒
163      ! lbl' ← Identifier_of_label … lbl ;
164      return Jmp (toASM_ident ? lbl)
165    | RETURN ⇒ return Instruction (RET ?)
166    | TAILCALL abs _ _ ⇒ Ⓧabs
167    ]
168  | sequential instr _ ⇒
169      match instr with
170      [ step_seq instr' ⇒
171        match instr' with
172        [ extension_seq ext ⇒
173          match ext with
174          [ SAVE_CARRY ⇒
175            return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
176          | RESTORE_CARRY ⇒
177            return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
178          | LOW_ADDRESS reg lbl ⇒
179            ! lbl' ← Identifier_of_label … lbl ;
180            return MovSuccessor (register_address reg) LOW lbl'
181          | HIGH_ADDRESS reg lbl ⇒
182            ! lbl' ← Identifier_of_label … lbl ;
183            return MovSuccessor (register_address reg) HIGH lbl'
184          ]
185        | COMMENT comment ⇒ return Comment comment
186        | POP _ ⇒ return Instruction (POP ? accumulator_address)
187        | PUSH _ ⇒ return Instruction (PUSH ? accumulator_address)
188        | CLEAR_CARRY ⇒ return Instruction (CLR ? CARRY)
189        | OPACCS accs _ _ _ _ ⇒
190          return match accs with
191          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
192          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
193          ]
194        | OP1 op1 _ _ ⇒
195          return match op1 with
196          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
197          | Inc ⇒ Instruction (INC ? ACC_A)
198          | Rl ⇒ Instruction (RL ? ACC_A)
199          ]
200        | OP2 op2 _ _ reg ⇒
201          return match arg_address … reg
202          return λx.is_in … [[ acc_a;
203                                 direct;
204                                 registr;
205                                 data ]] x → ? with
206          [ ACC_A ⇒ λacc_a: True.
207            match op2 with
208            [ Add ⇒ Instruction (ADD ? ACC_A accumulator_address)
209            | Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address)
210            | Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address)
211            | Xor ⇒ Instruction (CLR ? ACC_A)
212            | _ ⇒ Instruction (NOP ?)
213            ]
214          | DIRECT d ⇒ λdirect1: True.
215            match op2 with
216            [ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d))
217            | Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d))
218            | Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d))
219            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
220            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
221            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
222            ]
223          | REGISTER r ⇒ λregister1: True.
224            match op2 with
225            [ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r))
226            | Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r))
227            | Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r))
228            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
229            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
230            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
231            ]
232          | DATA b ⇒ λdata : True.
233            match op2 with
234            [ Add ⇒ Instruction (ADD ? ACC_A (DATA b))
235            | Addc ⇒ Instruction (ADDC ? ACC_A (DATA b))
236            | Sub ⇒ Instruction (SUBB ? ACC_A (DATA b))
237            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
238            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
239            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
240            ]
241          | _ ⇒ Ⓧ
242          ] (subaddressing_modein …)
243        | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
244        | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
245        | ADDRESS addr proof _ _ ⇒
246          ! addr' ← address_of_ident … proof ;
247          return Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, addr'〉)))))
248        | SET_CARRY ⇒
249          return Instruction (SETB ? CARRY)
250        | MOVE regs ⇒
251          return match regs with
252          [ to_acc _ reg ⇒
253            match register_address reg return λx.is_in … [[ acc_a;
254                                                              direct;
255                                                              registr]] x → ? with
256           [ REGISTER r ⇒ λregister9: True.
257             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
258           | DIRECT d ⇒ λdirect9: True.
259             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
260           | ACC_A ⇒ λacc_a: True.
261             Instruction (NOP ?)
262           | _ ⇒ Ⓧ
263           ] (subaddressing_modein …)
264         | from_acc reg _ ⇒
265            match register_address reg return λx.is_in … [[ acc_a;
266                                                              direct;
267                                                              registr ]] x → ? with
268            [ REGISTER r ⇒ λregister8: True.
269             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
270            | ACC_A ⇒ λacc: True.
271             Instruction (NOP ?)
272            | DIRECT d ⇒ λdirect8: True.
273             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
274            | _ ⇒ Ⓧ
275            ] (subaddressing_modein …)
276          | int_to_reg reg b ⇒
277            match register_address reg return λx.is_in … [[ acc_a;
278                                                              direct;
279                                                              registr ]] x → ? with
280            [ REGISTER r ⇒ λregister7: True.
281              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
282            | ACC_A ⇒ λacc: True.
283               if eq_bv … (bv_zero …) b then
284                  Instruction (CLR ? ACC_A)
285               else
286                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
287            | DIRECT d ⇒ λdirect7: True.
288              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
289            | _ ⇒ Ⓧ
290            ] (subaddressing_modein …)
291          | int_to_acc _ b ⇒
292            if eq_bv … (bv_zero …) b then
293              Instruction (CLR ? ACC_A)
294            else
295              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
296          ]
297        ]
298      | CALL f _ _ ⇒
299        match f with
300        [ inl id ⇒
301          ! id' ← Identifier_of_ident … id ;
302          return Call (toASM_ident ? id')
303        | inr _ ⇒
304          return Instruction (JMP … INDIRECT_DPTR)
305        ]
306      | COST_LABEL lbl ⇒ return Cost lbl
307      | COND _ lbl ⇒
308        ! l ← Identifier_of_label … lbl;
309        return Instruction (JNZ ? l)
310      ]
311    | FCOND _ _ lbl_true lbl_false ⇒
312      ! l1 ← Identifier_of_label … lbl_true;
313      ! l2 ← Identifier_of_label … lbl_false;
314      return Jnz ACC_A l1 l2
315    ].
316  try @I
317qed.
318
319
320definition build_translated_statement ≝
321  λglobals.
322  λstatement: lin_statement globals.
323  ! stmt ← translate_statements globals (\snd statement) ;
324  match \fst statement with
325  [ Some lbl ⇒
326    ! lbl' ← Identifier_of_label globals lbl ;
327    return 〈Some ? lbl', stmt〉
328  | None ⇒
329    return 〈None ?, stmt〉
330  ].
331
332definition translate_code ≝
333  λglobals.
334  λcode: list (lin_statement globals).
335    m_list_map … (build_translated_statement globals) code.
336
337definition translate_fun_def ≝
338  λglobals.
339  λid_def : ident × (joint_function LIN globals).
340  !_ start_funct_translation … id_def ;
341  (* ^ modify current function id ^ *)
342  match \snd id_def with
343    [ Internal int ⇒
344      let code ≝ joint_if_code … int in
345      ! id ← Identifier_of_ident … (\fst id_def) ;
346      ! code' ← translate_code … code ;
347      match code' with
348      [ nil ⇒ return [〈Some ? id, Instruction (RET ?)〉] (* impossible, but whatever *)
349      | cons hd tl ⇒
350        match \fst hd with
351        [ None ⇒ return (〈Some ? id, \snd hd〉 :: tl)
352        | _ ⇒ return (〈Some ? id, Instruction (NOP ?)〉 :: hd :: tl) (* should never happen *)
353        ]
354      ]
355    | External _ ⇒ return [ ]
356    ].
357
358definition store_bytes : list Byte → list labelled_instruction ≝
359λbytes.
360\fold[(append ?), (nil ?)]_{by ∈ bytes}
361    [ 〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA by〉))))))〉 ;
362      〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ;
363      〈None ?, Instruction (INC ? DPTR)〉 ]. @I qed.
364
365definition do_store_init_data :
366  ∀globals.ASM_universe globals → Z → init_data → list labelled_instruction ≝
367λglobals,u,nxt_dptr,data.
368match data with
369[ Init_int8 n ⇒
370  store_bytes [ n ]
371| Init_int16 n ⇒
372  let 〈by0, by1〉 ≝ vsplit ? 8 8 n in store_bytes [ by0 ; by1 ]
373| Init_int32 n ⇒
374  let 〈by0, n〉 ≝ vsplit ? 8 24 n in
375  let 〈by1, n〉 ≝ vsplit ? 8 16 n in
376  let 〈by2, by3〉 ≝ vsplit ? 8 8 n in
377  store_bytes [ by0 ; by1 ; by2 ; by3 ]
378| Init_addrof symb ofs ⇒
379  let addr : Word ≝
380    match lookup … (address_map … u) symb with
381    [ Some x ⇒ bitvector_of_Z ? (Z_of_unsigned_bitvector … x + ofs)
382    | None ⇒ bv_zero ?
383    ] in
384  let 〈by1, by0〉 ≝ vsplit ? 8 8 addr in
385  store_bytes [by0 ; by1] 
386| Init_space n ⇒
387  (* if n = 1 it is better to use INC, ow we can set the DPTR with MOV *)
388  match n with
389  [ O ⇒ [ ]
390  | S k ⇒
391    match k with
392    [ O ⇒ [ 〈None ?, Instruction (INC ? DPTR)〉 ]
393    | _ ⇒ [ 〈None ?, Instruction (MOV ? (inl ?? (inl ?? (inr ?? 〈DPTR, DATA16 (bitvector_of_Z … nxt_dptr)〉))))〉 ]
394    ]
395  ]
396| Init_null ⇒ store_bytes [ bv_zero ? ; bv_zero ? ]
397]. @I qed.
398
399definition do_store_init_data_list :
400  ∀globals.ASM_universe globals → Z → list init_data → list labelled_instruction ≝
401λglobals,u,start_dptr,data.
402let f ≝ λdata,dptr_acc.
403  let 〈dptr, acc〉 ≝ dptr_acc in
404  let nxt_dptr ≝ dptr + size_init_data data in
405  〈nxt_dptr, do_store_init_data … u nxt_dptr data @ acc〉 in
406\snd (foldr ?? f 〈start_dptr, [ ]〉 data).
407
408definition translate_initialization : ∀p : lin_program.
409  state_monad (ASM_universe (prog_var_names … p)) (list labelled_instruction) ≝
410  λp : lin_program.λu.
411  let start_sp : Z ≝ -(globals_stacksize … p) in
412  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
413  let data ≝ flatten ? (map ?? (λx.\snd x) (prog_vars … p)) in
414  let init_isp ≝
415    (* initial stack pointer set to 2Fh in order to use addressable bits *)
416    DATA (zero 2 @@ [[true;false]] @@ maximum 4) in
417  let isp_direct ≝
418    (* 81h = 10000001b *)
419    DIRECT (true ::: bv_zero 6 @@ [[ true ]]) in
420  let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in
421  let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in
422  〈u, [
423    〈None ?, Cost (init_cost_label … p)〉 ;
424    (* initialize the internal stack pointer past the addressable bits *)
425    〈None ?, Instruction
426    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
427      〈isp_direct, init_isp〉)))))〉 ;
428    (* initialize our stack pointer past the globals *)
429    〈None ?, Instruction
430    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
431      〈reg_spl, DATA spl〉))))))〉 ;
432    〈None ?, Instruction
433    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
434      〈reg_sph, DATA sph〉))))))〉 ] @
435  do_store_init_data_list ? u start_sp data〉. @I qed.
436
437definition get_symboltable :
438  ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝
439  λglobals,u.
440  let imap ≝ ident_map … u in
441  let f ≝ λiold,inew.cons ? 〈inew, iold〉 in
442  〈u, foldi ??? f imap [ ]〉.
443
444definition lin_to_asm : lin_program → option pseudo_assembly_program ≝
445  λp.
446  state_run ?? (new_ASM_universe p)
447    (let add_translation ≝
448      λacc,id_def.
449      ! code ← translate_fun_def … id_def ;
450      ! acc ← acc ;
451      return (code @ acc) in
452     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
453     ! exit_label ← ASM_fresh … ;
454     ! main ← Identifier_of_ident … (prog_main … p) ;
455     ! symboltable ← get_symboltable … ;
456     ! init ← translate_initialization p ;
457     return
458       (let code ≝
459        init @ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
460        ! code_ok ← code_size_opt code ; 
461        (* atm no data identifier is used in the code, so preamble must be empty *)
462        return
463          (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))).
464cases daemon
465qed.
Note: See TracBrowser for help on using the repository browser.