Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/LTL/LTL.ma

    r1197 r1311  
    1 include "common/Graphs.ma".
    2 include "utilities/IdentifierTools.ma".
    31include "joint/Joint.ma".
    42
    5 definition ltl_params: params ≝
    6  mk_params
    7    unit unit unit unit registers_move Register
    8      unit unit unit unit.
     3definition ltl_params__: params__ ≝
     4 (mk_params__ unit unit unit unit registers_move Register nat unit False).
     5definition ltl_params_ : params_ ≝ graph_params_ ltl_params__.
     6definition ltl_params0 : params0 ≝ mk_params0 ltl_params__ unit unit.
     7definition ltl_params1 : params1 ≝ mk_params1 ltl_params0 unit.
     8definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params1.
    99
    10 definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.
    11  
    12 definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
    13  
    14 record ltl_internal_function (globals: list ident): Type[0] ≝
    15 {
    16   ltl_if_luniverse: universe LabelTag;
    17   ltl_if_runiverse: universe RegisterTag;
    18   ltl_if_stacksize: nat;
    19   ltl_if_graph: ltl_statement_graph globals;
    20   ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?;
    21   ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?
    22 }.
     10definition ltl_statement ≝ joint_statement ltl_params_.
    2311
    24 inductive ltl_function_definition (globals: list ident): Type[0] ≝
    25   | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals
    26   | ltl_fu_external_function: external_function → ltl_function_definition globals.
    27  
    28 record ltl_program (globals: list (ident × nat)): Type[0] ≝
    29 {
    30   ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
    31   ltl_pr_main: option ident
    32 }.
     12definition ltl_program ≝ joint_program ltl_params.
     13
     14definition ltl_internal_function ≝
     15 λglobals. joint_internal_function … (ltl_params globals).

  • Deliverables/D3.3/id-lookup-branch/LTL/LTLToLIN.ma

    r1197 r1311  
    22include "LIN/LIN.ma".
    33include "utilities/BitVectorTrieSet.ma".
    4 include "common/Graphs.ma".
    5 
    6 axiom LTLTag: String.
     4include alias "common/Graphs.ma".
    75
    86definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
    … …  
    108  λs: ltl_statement globals.
    119  match s with
    12   [ joint_st_return ⇒ joint_st_return lin_params globals
    13   | joint_st_sequential instr lbl ⇒ joint_st_sequential lin_params globals instr lbl
    14   | joint_st_goto l ⇒ joint_st_goto lin_params globals l
    15   | joint_st_extension ext ⇒ joint_st_extension lin_params globals ext
     10  [ RETURN ⇒ RETURN ??
     11  | sequential instr lbl ⇒ sequential … instr it
     12  | GOTO l ⇒ GOTO lin_params_ globals l
    1613  ].
    17    
    18 definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    19   λl: label.
    20   λg: BitVectorTrieSet 16.
    21     set_insert ? (word_of_identifier ? l) g.
    22    
    23 definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    24   λl: label.
    25   λg: BitVectorTrieSet 16.
    26     set_insert ? (word_of_identifier ? l) g.
    27    
    28 definition marked: label → BitVectorTrieSet 16 → bool ≝
    29   λl: label.
    30   λg: BitVectorTrieSet 16.
    31     set_member ? (word_of_identifier ? l) g.
    32    
    33 (* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *)
    34    
    35 definition graph_lookup ≝
    36   λglobals: list ident.
    37   λl: label.
    38   λgr: ltl_statement_graph globals.
    39     lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
    40    
    41 definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝
    42   λglobals: list ident.
    43   λl: label.
    44   λg: ltl_statement_graph globals.
    45     graph_lookup globals l g.
    4614
    47 definition foo ≝
    48   λl2, visited, required, globals, generated, g, n.
    49   λvisit:
    50   ∀globals: list ident.
    51   ∀g: ltl_statement_graph globals.
    52   ∀required: BitVectorTrieSet 16.
    53   ∀visited: BitVectorTrieSet 16.
    54   ∀generated: list (pre_lin_statement globals).
    55   ∀l: label.
    56   ∀n: nat.
    57     BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
    58   if marked l2 visited then
    59     〈require l2 required, (joint_st_goto … globals l2) :: generated〉
    60   else
    61    visit globals g required visited generated l2 n.
     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: 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 …, 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       [ 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'' ≝ 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     | 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.
    6253
    63 (* XXX: look at this.  way too complicated to understand whether it is correct,
    64    in my opinion.
    65 *)
    66 let rec visit
    67   (globals: list ident) (g: ltl_statement_graph globals)
    68   (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    69   (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
    70     on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝
    71   match n with
    72   [ O ⇒ 〈required, generated〉
    73   | S n' ⇒
    74     let visited' ≝ mark l visited in
    75     match fetch globals l g with
    76     [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
    77     | Some statement ⇒
    78       let translated_statement ≝ translate_statement globals statement in
    79       let generated'' ≝ translated_statement :: generated in
    80       match statement with
    81       [ joint_st_sequential instr l2 ⇒
    82         match instr with
    83         [ joint_instr_cond acc_a_reg l1 ⇒
    84               let required' ≝
    85                 if marked l2 visited' then
    86                   require l2 required
    87                 else
    88                   required in
    89               let 〈required', generated''〉 ≝
    90                foo l2 visited' required' globals generated'' g n' visit (*
    91                 if marked l2 visited' then
    92                   〈required', (Joint_St_Goto ? globals l2) :: generated''〉
    93                 else
    94                   visit globals g required' visited' generated'' l2 n'*) in
    95               let required'' ≝ require l1 required' in
    96                 if ¬(marked l1 visited') then
    97                   visit globals g required'' visited' generated'' l1 n'
    98                 else
    99                   〈required', generated''〉
    100           | _ ⇒
    101             let required' ≝
    102               if marked l2 visited' then
    103                 require l2 required
    104               else
    105                 required in
    106             if marked l2 visited' then
    107               〈required', joint_st_goto … globals l2 :: generated''〉
    108             else
    109               visit globals g required' visited' generated'' l2 n'
    110           ]
    111     | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    112     | joint_st_goto l ⇒
    113       let required' ≝
    114         if marked l visited' then
    115          require l required
    116         else
    117          required
    118       in
    119         if marked l visited' then
    120           〈required', joint_st_goto … globals l :: generated''〉
    121         else
    122           visit globals g required' visited' generated'' l n'
    123     | joint_st_extension ext ⇒ 〈required, generated〉
    124     ]
    125   ]
    126 ].
     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.
    12757
    128 (*
    129 definition translate_graph ≝
    130   λglobals: list Identifier.
    131   λg: LTLStatementGraph globals.
    132   λentry: Identifier.
    133     let visited ≝ set_empty ? in
    134     let required ≝ set_insert ? entry (set_empty ?) in
    135     let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
    136     let reversed ≝ rev ? translated in
    137       filter (λs: PreLINStatement globals. ?) reversed.
    138 *)
     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 ≝ 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! *)
     80cases daemon
     81qed.
     82
     83definition 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    ??.
     94cases daemon (*CSC: XXXXXXXXX Dead code produced *)
     95qed.
     96
     97definition ltl_to_lin : ltl_program → lin_program ≝
     98 λp. transform_program … p (transf_fundef … (translate_int_fun …)).
Note: See TracChangeset for help on using the changeset viewer.