source: src/LTL/LTLToLIN.ma @ 2103

Last change on this file since 2103 was 2103, checked in by campbell, 7 years ago

Make transform_*program take a more general transformation to make
properties easier to state.

File size: 3.6 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  [ RETURN ⇒ RETURN ??
11  | sequential instr lbl ⇒ sequential … instr it
12  | GOTO l ⇒ 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. *)
20let rec visit
21  (globals: list ident) (g: label → option (ltl_statement globals))
22  (required: identifier_set LabelTag) (visited: identifier_set LabelTag)
23  (generated: list (lin_statement globals)) (l: label) (n: nat)
24    on n: identifier_set LabelTag × (list (lin_statement globals)) ≝
25  match n with
26  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
27  | S n' ⇒
28    if mem_set … visited l then
29     〈add_set ? required l, 〈None …, GOTO … globals l〉 :: generated〉
30    else
31     let visited' ≝ add_set ? visited l in
32     match g 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       [ sequential instr l2 ⇒
39         match instr with
40         [ COND acc_a_reg l1 ⇒
41            let 〈required', generated''〉 ≝
42             visit globals g required visited' generated' l2 n' in
43            let required'' ≝ add_set ? required' l1 in
44             if mem_set … visited' l1 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     | RETURN ⇒ 〈required, generated'〉
50     | GOTO l2 ⇒ visit globals g required visited' generated' l2 n']]].
51[1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
52qed.
53
54(* CSC: The branch compression (aka tunneling) optimization is not implemented
55   in Matita *)
56definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a.
57
58definition 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 ≝ ∅ in
65  let required ≝ { (entry) } in
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 ⇒
73          〈if mem_set … required' l then Some ? l else None ?,
74           x〉])
75    reversed.
76
77definition translate_int_fun:
78 ∀globals.
79  joint_internal_function … (ltl_params globals) →
80   joint_internal_function … (lin_params globals)
81
82 λglobals,f.
83  mk_joint_internal_function globals (lin_params globals)
84   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f)
85    (translate_graph globals (joint_if_entry ?? f) (nat_of_pos … (next_identifier … (joint_if_luniverse … f)))
86     (lookup ?? (joint_if_code … f)))
87    ??.
88cases daemon (*CSC: XXXXXXXXX Dead code produced *)
89qed.
90
91definition ltl_to_lin : ltl_program → lin_program ≝
92 λp. transform_program … p (λvarnames. transf_fundef … (translate_int_fun varnames)).
Note: See TracBrowser for help on using the repository browser.