1 | include "LTL/LTL.ma". |
---|
2 | include "LIN/LIN.ma". |
---|
3 | include "utilities/BitVectorTrieSet.ma". |
---|
4 | include alias "common/Graphs.ma". |
---|
5 | |
---|
6 | definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝ |
---|
7 | λglobals: list ident. |
---|
8 | λs: ltl_statement globals. |
---|
9 | match s with |
---|
10 | [ joint_st_return ⇒ joint_st_return ?? |
---|
11 | | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it |
---|
12 | | joint_st_goto l ⇒ joint_st_goto lin_params_ globals l |
---|
13 | ]. |
---|
14 | |
---|
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. *) |
---|
20 | let rec visit |
---|
21 | (globals: list ident) (g: label → option (ltl_statement globals)) |
---|
22 | (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) |
---|
23 | (generated: list (lin_statement globals)) (l: label) (n: nat) |
---|
24 | on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝ |
---|
25 | match n with |
---|
26 | [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *) |
---|
27 | | S n' ⇒ |
---|
28 | if set_member … (word_of_identifier … l) visited then |
---|
29 | 〈set_insert ? (word_of_identifier ? l) required, 〈None …, joint_st_goto … globals l〉 :: generated〉 |
---|
30 | else |
---|
31 | let visited' ≝ set_insert ? (word_of_identifier ? l) visited in |
---|
32 | match g (an_identifier LabelTag (word_of_identifier … l)) with |
---|
33 | [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *) |
---|
34 | | Some statement ⇒ |
---|
35 | let translated_statement ≝ translate_statement globals statement in |
---|
36 | let generated' ≝ 〈Some … l, translated_statement〉 :: generated in |
---|
37 | match statement with |
---|
38 | [ joint_st_sequential instr l2 ⇒ |
---|
39 | match instr with |
---|
40 | [ joint_instr_cond acc_a_reg l1 ⇒ |
---|
41 | let 〈required', generated''〉 ≝ |
---|
42 | visit globals g required visited' generated' l2 n' in |
---|
43 | let required'' ≝ set_insert ? (word_of_identifier ? l1) required' in |
---|
44 | if set_member … (word_of_identifier … l1) visited' then |
---|
45 | 〈required', generated''〉 |
---|
46 | else |
---|
47 | visit globals g required'' visited' generated'' l1 n' |
---|
48 | | _ ⇒ visit globals g required visited' generated' l2 n'] |
---|
49 | | joint_st_return ⇒ 〈required, generated'〉 |
---|
50 | | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n']]]. |
---|
51 | [1,2: @daemon (*CSC: impossible cases, use more dependent types *) ] |
---|
52 | qed. |
---|
53 | |
---|
54 | (* CSC: The branch compression (aka tunneling) optimization is not implemented |
---|
55 | in Matita *) |
---|
56 | definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a. |
---|
57 | |
---|
58 | definition translate_graph: |
---|
59 | ∀globals. label → nat → |
---|
60 | (label → option (ltl_statement globals)) → codeT … (lin_params globals) |
---|
61 | ≝ |
---|
62 | λglobals,entry,labels_upper_bound,g. |
---|
63 | let g ≝ branch_compress ? g in |
---|
64 | let visited ≝ set_empty ? in |
---|
65 | let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in |
---|
66 | let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in |
---|
67 | let reversed ≝ rev ? translated in |
---|
68 | let final ≝ |
---|
69 | map ?? |
---|
70 | (λs. let 〈l,x〉 ≝ s in |
---|
71 | match l with |
---|
72 | [ None ⇒ 〈None …,x〉 |
---|
73 | | Some l ⇒ |
---|
74 | 〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?, |
---|
75 | x〉]) |
---|
76 | reversed |
---|
77 | in |
---|
78 | dp … final ?. |
---|
79 | (*CSC: XXXXXXX missing proof of well formedness here; but it seems false! *) |
---|
80 | cases daemon |
---|
81 | qed. |
---|
82 | |
---|
83 | definition translate_int_fun: |
---|
84 | ∀globals. |
---|
85 | joint_internal_function … (ltl_params globals) → |
---|
86 | joint_internal_function … (lin_params globals) |
---|
87 | ≝ |
---|
88 | λglobals,f. |
---|
89 | mk_joint_internal_function globals (lin_params globals) |
---|
90 | (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f) |
---|
91 | (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f))) |
---|
92 | (lookup ?? (joint_if_code … f))) |
---|
93 | ??. |
---|
94 | cases daemon (*CSC: XXXXXXXXX Dead code produced *) |
---|
95 | qed. |
---|
96 | |
---|
97 | definition ltl_to_lin : ltl_program → lin_program ≝ |
---|
98 | λp. transform_program … p (transf_fundef … (translate_int_fun …)). |
---|