source: src/LTL/LTLToLIN.ma @ 1246

Last change on this file since 1246 was 1246, checked in by sacerdot, 8 years ago

Yet another change to Joint.ma to accomodate all passes.
The concrete memory representation for the code of internal functions is
back, at the price of more complexity in the definition of the parameters.

Note: I do not understand any more the well_formed_P invariant for LIN code.
Moreover, the invariant does not seem to hold for code produced using LTLToLin.

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