Changeset 1082


Ignore:
Timestamp:
Jul 20, 2011, 5:17:38 PM (8 years ago)
Author:
mulligan
Message:

work from today on ertl -> ltl pass

Location:
src
Files:
1 added
7 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1077 r1082  
    66include "common/Registers.ma".
    77
    8 definition hardware_register ≝ Register.
    98definition registers ≝ list register.
    109
     
    1312  | ertl_st_comment: String → label → ertl_statement
    1413  | ertl_st_cost: costlabel → label → ertl_statement
    15   | ertl_st_get_hdw: register → hardware_register → label → ertl_statement
    16   | ertl_st_set_hdw: hardware_register → register → label → ertl_statement
    17   | ertl_st_hdw_to_hdw: hardware_register → hardware_register → label → ertl_statement
     14  | ertl_st_get_hdw: register → Register → label → ertl_statement
     15  | ertl_st_set_hdw: Register → register → label → ertl_statement
     16  | ertl_st_hdw_to_hdw: Register → Register → label → ertl_statement
    1817  | ertl_st_new_frame: label → ertl_statement
    1918  | ertl_st_del_frame: label → ertl_statement
  • src/ERTL/ERTLToLTL.ma

    r759 r1082  
    11include "ERTL/ERTL.ma".
    2 include "LTL/LTL.ma".
    3  
    4 axiom translate_ertl_func:
    5   ∀globals: list ident.
    6     list (ident × ertl_function) → list (ident × (ltl_function_definition globals)).
    7  
    8 definition translate: ∀e: ertl_program. ltl_program (ertl_pr_vars e) ≝
    9   λp.
    10     let globals ≝ map ? ? \fst (ertl_pr_vars p) in
    11     let ltl_pr_funcs ≝ map ? ? ? (ertl_pr_funcs p) in
    12       mk_ltl_program (ertl_pr_vars p) ltl_pr_funcs (ertl_pr_main p).
    13     # H1
    14     @ (translate_ertl_func globals) in ⊢ (? × %) (* dpm here *)
     2include "LTL/LTL.ma".
  • src/ERTL/Liveness.ma

    r756 r1082  
    11include "ERTL/ERTL.ma".
    2 
    3 definition statement_successors ≝
    4   λstmt: ertl_statement.
    5   match stmt with
    6   [ ertl_st_return _ ⇒ [ ]
    7   | ertl_st_skip l ⇒ [ l ]
    8   | ertl_st_comment comment l ⇒ [ l ]
    9   | ertl_st_cost cost l ⇒ [ l ]
    10   | ertl_st_set_hdw r1 r2 l ⇒ [ l ]
    11   | ertl_st_get_hdw r1 r2 l ⇒ [ l ]
    12   | ertl_st_hdw_to_hdw r1 r2 l ⇒ [ l ]
    13   | ertl_st_new_frame l ⇒ [ l ]
    14   | ertl_st_del_frame l ⇒ [ l ]
    15   | ertl_st_frame_size r l ⇒ [ l ]
    16   | ertl_st_push r l ⇒ [ l ]
    17   | ertl_st_pop r l ⇒ [ l ]
    18   | ertl_st_addr_h r l1 l2 ⇒ [ l2 ]
    19   | ertl_st_addr_l r l1 l2 ⇒ [ l2 ]
    20   | ertl_st_int r v l ⇒ [ l ]
    21   | ertl_st_move r1 r2 l ⇒ [ l ]
    22   | ertl_st_opaccs opaccs r1 r2 r3 l ⇒ [ l ]
    23   | ertl_st_op2 op2 r1 r2 r3 l ⇒ [ l ]
    24   | ertl_st_op1 op1 r1 r2 l ⇒ [ l ]
    25   | ertl_st_clear_carry l ⇒ [ l ]
    26   | ertl_st_load r1 r2 r3 l ⇒ [ l ]
    27   | ertl_st_store r1 r2 r3 l ⇒ [ l ]
    28   | ertl_st_call_id id v l ⇒ [ l ]
    29   | ertl_st_cond_acc _ l1 l2 ⇒ [ l1 ] @ [ l2 ]
    30   ].
    31  
    32 (* dpm: this needs sorting out!  just what exactly is a register? *)
    33 
    34 definition set_of_list ≝
    35   λn: nat.
    36   λl: list (BitVector n).
    37     foldr ? ? (set_insert ?) (set_empty ?) l.
    38    
    39 definition dptr ≝
    40   set_insert ? (word_of_register RegisterDPL) (set_singleton ? (word_of_register RegisterDPH)).
  • src/ERTL/Uses.ma

    r777 r1082  
    11include "ERTL/ERTL.ma".
    2 include "utilities/BitVectorTrieSet.ma".
    3 include "ASM/Arithmetic.ma".
    4 include "ASM/I8051.ma".
    52include "common/Registers.ma".
    6 
    7 definition count ≝
    8   λr: register.
    9   λuses.
    10     let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
    11       insert ? 16 l uses.
    12      
    13 definition examine_statement ≝
    14   λstatement: ertl_statement.
    15   λuses.
    16   match statement with
    17   [ ertl_st_skip _ ⇒ uses
    18   | ertl_st_comment _ _ ⇒ uses
    19   | ertl_st_cost _ _ ⇒ uses
    20   | ertl_st_hdw_to_hdw _ _ _ ⇒ uses
    21   | ertl_st_new_frame _ ⇒ uses
    22   | ertl_st_del_frame _ ⇒ uses
    23   | ertl_st_clear_carry _ ⇒ uses
    24   | ertl_st_call_id _ _ _ ⇒ uses
    25   | ertl_st_return _ ⇒ uses
    26   | ertl_st_get_hdw r _ _ ⇒ count (word_of_register r) uses
    27   | ertl_st_set_hdw _ r _ ⇒ count (word_of_register r) uses
    28   | ertl_st_frame_size ar _ ⇒
    29     match ar with [
    30       mk_abstract_register r ⇒
    31         (* dpm: shift the abstract registers above the physical registers *)
    32         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    33           count offset uses
    34     ]
    35   | ertl_st_pop ar _ ⇒
    36     match ar with [
    37       mk_abstract_register r ⇒
    38         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    39           count offset uses
    40     ]
    41   | ertl_st_push ar _ ⇒
    42     match ar with [
    43       mk_abstract_register r ⇒
    44         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    45           count offset uses
    46     ]
    47   | ertl_st_int ar _ _ ⇒
    48     match ar with [
    49       mk_abstract_register r ⇒
    50         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    51           count offset uses
    52     ]
    53   | ertl_st_addr_h ar _ _ ⇒
    54     match ar with [
    55       mk_abstract_register r ⇒
    56         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    57           count offset uses
    58     ]
    59   | ertl_st_addr_l ar _ _ ⇒
    60     match ar with [
    61       mk_abstract_register r ⇒
    62         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    63           count offset uses
    64     ]
    65   | ertl_st_cond_acc ar _ _ ⇒
    66     match ar with [
    67       mk_abstract_register r ⇒
    68         let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    69           count offset uses
    70     ]
    71   | ertl_st_move ar1 ar2 _ ⇒
    72     match ar1 with [
    73       mk_abstract_register r1 ⇒
    74       match ar2 with [
    75         mk_abstract_register r2 ⇒
    76           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    77           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    78             count offset1 (count offset2 uses)
    79       ]
    80     ]
    81   | ertl_st_op1 op1 ar1 ar2 _ ⇒
    82     match ar1 with [
    83       mk_abstract_register r1 ⇒
    84       match ar2 with [
    85         mk_abstract_register r2 ⇒
    86           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    87           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    88             count offset1 (count offset2 uses)
    89       ]
    90     ]
    91   | ertl_st_op2 op2 ar1 ar2 ar3 _ ⇒
    92     match ar1 with [
    93       mk_abstract_register r1 ⇒
    94       match ar2 with [
    95         mk_abstract_register r2 ⇒
    96         match ar3 with [
    97           mk_abstract_register r3 ⇒
    98           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    99           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    100           let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
    101             count offset1 (count offset2 (count offset3 uses))
    102         ]
    103       ]
    104     ]
    105   | ertl_st_opaccs opaccs ar1 ar2 ar3 _ ⇒
    106     match ar1 with [
    107       mk_abstract_register r1 ⇒
    108       match ar2 with [
    109         mk_abstract_register r2 ⇒
    110         match ar3 with [
    111           mk_abstract_register r3 ⇒
    112           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    113           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    114           let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
    115             count offset1 (count offset2 (count offset3 uses))
    116         ]
    117       ]
    118     ]
    119   | ertl_st_load ar1 ar2 ar3 _ ⇒
    120     match ar1 with [
    121       mk_abstract_register r1 ⇒
    122       match ar2 with [
    123         mk_abstract_register r2 ⇒
    124         match ar3 with [
    125           mk_abstract_register r3 ⇒
    126           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    127           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    128           let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
    129             count offset1 (count offset2 (count offset3 uses))
    130         ]
    131       ]
    132     ]
    133   | ertl_st_store ar1 ar2 ar3 _ ⇒
    134     match ar1 with [
    135       mk_abstract_register r1 ⇒
    136       match ar2 with [
    137         mk_abstract_register r2 ⇒
    138         match ar3 with [
    139           mk_abstract_register r3 ⇒
    140           let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    141           let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
    142           let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
    143             count offset1 (count offset2 (count offset3 uses))
    144         ]
    145       ]
    146     ]
    147   ].
    148   [*: normalize
    149       @ le_S @ le_S @ le_S @ le_S @ le_S @ le_S
    150       @ le_S @ le_S @ le_S @ le_S @ le_S @ le_n ]
    151 qed.
    152 
    153 (*
    154 definition examine_internal ≝
    155   λint_fun.
    156     let uses ≝ foldr ? ? examine_statement (Stub ? ?) (ERTL_IF_Graph int_fun) in
    157       lookup uses.
    158 *)
  • src/LIN/JointLTLLIN.ma

    r757 r1082  
    88  | joint_instr_comment: String → joint_instruction globals
    99  | joint_instr_cost_label: costlabel → joint_instruction globals
    10   | joint_instr_int: register → Byte → joint_instruction globals
     10  | joint_instr_int: Register → Byte → joint_instruction globals
    1111  | joint_instr_pop: joint_instruction globals
    1212  | joint_instr_push: joint_instruction globals
    1313  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → joint_instruction globals
    14   | joint_instr_from_acc: register → joint_instruction globals
    15   | joint_instr_to_acc: register → joint_instruction globals
     14  | joint_instr_from_acc: Register → joint_instruction globals
     15  | joint_instr_to_acc: Register → joint_instruction globals
    1616  | joint_instr_opaccs: OpAccs → joint_instruction globals
    1717  | joint_instr_op1: Op1 → joint_instruction globals
    18   | joint_instr_op2: Op2 → register → joint_instruction globals
     18  | joint_instr_op2: Op2 → Register → joint_instruction globals
    1919  | joint_instr_clear_carry: joint_instruction globals
    2020  | joint_instr_load: joint_instruction globals
  • src/LTL/LTL.ma

    r757 r1082  
    1111  ltl_if_luniverse: universe LabelTag;
    1212  ltl_if_runiverse: universe RegisterTag;
    13   ltl_if_StackSize: nat;
    14   ltl_if_Graph: ltl_statement_graph globals;
    15   ltl_if_Entry: label;
    16   ltl_if_Exit: label
     13  ltl_if_stacksize: nat;
     14  ltl_if_graph: ltl_statement_graph globals;
     15  ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?;
     16  ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?
    1717}.
    1818
  • src/common/Graphs.ma

    r1080 r1082  
    33include "ASM/BitVectorTrie.ma".
    44include "common/Identifiers.ma".
     5include "common/AST.ma".
    56
    67axiom LabelTag : String.
    78
    89definition label ≝ identifier LabelTag.
     10
     11(* o'caml compiler doesn't make distinction between idents and labels *)
     12definition label_to_ident: label → ident ≝
     13  λl.
     14  match l with
     15  [ an_identifier l ⇒ an_identifier SymbolTag l
     16  ].
    917
    1018definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
Note: See TracChangeset for help on using the changeset viewer.