[714] | 1 | include "LTL/LTL.ma". |
---|
| 2 | include "LIN/LIN.ma". |
---|
[728] | 3 | include "utilities/BitVectorTrieSet.ma". |
---|
[1246] | 4 | include alias "common/Graphs.ma". |
---|
[714] | 5 | |
---|
[1246] | 6 | definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝ |
---|
[757] | 7 | λglobals: list ident. |
---|
| 8 | λs: ltl_statement globals. |
---|
[1166] | 9 | match s with |
---|
[1282] | 10 | [ RETURN ⇒ RETURN ?? |
---|
| 11 | | sequential instr lbl ⇒ sequential … instr it |
---|
| 12 | | GOTO l ⇒ GOTO lin_params_ globals l |
---|
[1166] | 13 | ]. |
---|
[728] | 14 | |
---|
[1233] | 15 | (* Invariant: l has not been visited yet the very first time the |
---|
| 16 | function is called and in the true branch of a conditional call. |
---|
| 17 | This avoid useless gotos. |
---|
| 18 | |
---|
| 19 | Note: the OCaml code contains some useful explanatory comments. *) |
---|
[1110] | 20 | let rec visit |
---|
[1236] | 21 | (globals: list ident) (g: label → option (ltl_statement globals)) |
---|
[1515] | 22 | (required: identifier_set LabelTag) (visited: identifier_set LabelTag) |
---|
[1246] | 23 | (generated: list (lin_statement globals)) (l: label) (n: nat) |
---|
[1515] | 24 | on n: identifier_set LabelTag × (list (lin_statement globals)) ≝ |
---|
[728] | 25 | match n with |
---|
[1233] | 26 | [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *) |
---|
[728] | 27 | | S n' ⇒ |
---|
[1515] | 28 | if mem_set … visited l then |
---|
| 29 | 〈add_set ? required l, 〈None …, GOTO … globals l〉 :: generated〉 |
---|
[1233] | 30 | else |
---|
[1515] | 31 | let visited' ≝ add_set ? visited l in |
---|
| 32 | match g l with |
---|
[1233] | 33 | [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *) |
---|
| 34 | | Some statement ⇒ |
---|
| 35 | let translated_statement ≝ translate_statement globals statement in |
---|
[1236] | 36 | let generated' ≝ 〈Some … l, translated_statement〉 :: generated in |
---|
[1233] | 37 | match statement with |
---|
[1282] | 38 | [ sequential instr l2 ⇒ |
---|
[1233] | 39 | match instr with |
---|
[1282] | 40 | [ COND acc_a_reg l1 ⇒ |
---|
[1233] | 41 | let 〈required', generated''〉 ≝ |
---|
| 42 | visit globals g required visited' generated' l2 n' in |
---|
[1515] | 43 | let required'' ≝ add_set ? required' l1 in |
---|
| 44 | if mem_set … visited' l1 then |
---|
[1233] | 45 | 〈required', generated''〉 |
---|
| 46 | else |
---|
| 47 | visit globals g required'' visited' generated'' l1 n' |
---|
| 48 | | _ ⇒ visit globals g required visited' generated' l2 n'] |
---|
[1282] | 49 | | RETURN ⇒ 〈required, generated'〉 |
---|
| 50 | | GOTO l2 ⇒ visit globals g required visited' generated' l2 n']]]. |
---|
[1250] | 51 | [1,2: @daemon (*CSC: impossible cases, use more dependent types *) ] |
---|
[1233] | 52 | qed. |
---|
[728] | 53 | |
---|
[1233] | 54 | (* CSC: The branch compression (aka tunneling) optimization is not implemented |
---|
| 55 | in Matita *) |
---|
[1236] | 56 | definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a. |
---|
[1233] | 57 | |
---|
[1236] | 58 | definition translate_graph: |
---|
| 59 | ∀globals. label → nat → |
---|
[1246] | 60 | (label → option (ltl_statement globals)) → codeT … (lin_params globals) |
---|
[1236] | 61 | ≝ |
---|
| 62 | λglobals,entry,labels_upper_bound,g. |
---|
| 63 | let g ≝ branch_compress ? g in |
---|
[1515] | 64 | let visited ≝ ∅ in |
---|
| 65 | let required ≝ { (entry) } in |
---|
[1236] | 66 | let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in |
---|
| 67 | let reversed ≝ rev ? translated in |
---|
| 68 | map ?? |
---|
| 69 | (λs. let 〈l,x〉 ≝ s in |
---|
| 70 | match l with |
---|
| 71 | [ None ⇒ 〈None …,x〉 |
---|
| 72 | | Some l ⇒ |
---|
[1515] | 73 | 〈if mem_set … required' l then Some ? l else None ?, |
---|
[1236] | 74 | x〉]) |
---|
[1379] | 75 | reversed. |
---|
[1236] | 76 | |
---|
| 77 | definition translate_int_fun: |
---|
| 78 | ∀globals. |
---|
[1246] | 79 | joint_internal_function … (ltl_params globals) → |
---|
| 80 | joint_internal_function … (lin_params globals) |
---|
[1236] | 81 | ≝ |
---|
| 82 | λglobals,f. |
---|
[1246] | 83 | mk_joint_internal_function globals (lin_params globals) |
---|
[1236] | 84 | (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f) |
---|
[1515] | 85 | (translate_graph globals (joint_if_entry ?? f) (nat_of_pos … (next_identifier … (joint_if_luniverse … f))) |
---|
[1246] | 86 | (lookup ?? (joint_if_code … f))) |
---|
[1236] | 87 | ??. |
---|
| 88 | cases daemon (*CSC: XXXXXXXXX Dead code produced *) |
---|
| 89 | qed. |
---|
| 90 | |
---|
| 91 | definition ltl_to_lin : ltl_program → lin_program ≝ |
---|
[2103] | 92 | λp. transform_program … p (λvarnames. transf_fundef … (translate_int_fun varnames)). |
---|