Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (8 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/LIN/LIN.ma

    r1197 r1311  
    11include "joint/Joint.ma".
     2include "utilities/lists.ma".
    23
    3 definition lin_params: params ≝
    4  mk_params
    5    unit unit unit unit registers_move Register
    6      unit unit unit unit.
     4definition lin_params__: params__ ≝
     5 mk_params__ unit unit unit unit registers_move Register nat unit False.
     6definition lin_params_ : params_ ≝ mk_params_ lin_params__ unit.
     7definition lin_params0 : params0 ≝ mk_params0 lin_params__ unit unit.
     8definition lin_params1 : params1 ≝ mk_params1 lin_params0 unit.
    79
    8 definition pre_lin_statement ≝
    9  λglobals: list ident. joint_statement lin_params globals.
    10 
    11 definition lin_statement ≝
    12   λglobals.
    13     option ident × (pre_lin_statement globals).
     10definition pre_lin_statement ≝ joint_statement lin_params_.
    1411
    1512definition well_formed_P ≝
     
    2118      match \fst hd with
    2219      [ Some lbl ⇒ False
    23       | None ⇒ True
    24       ]
    25     ].
    26    
    27 inductive lin_function_definition (globals: list ident): Type[0] ≝
    28   lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
    29 | lin_fu_external: external_function → lin_function_definition globals.
     20      | None ⇒ True]].
    3021
    31 record lin_program: Type[0] ≝
    32 {
    33   lin_pr_vars: list (ident × nat);
    34   lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
    35   lin_pr_main: option ident
    36 }.
     22definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).
     23
     24definition lin_params: ∀globals. params globals ≝
     25 λglobals.
     26  mk_params globals unit lin_params1 (Σcode:list (lin_statement globals). well_formed_P … code)
     27   (λcode:Σcode.?. λl.
     28    find ?? (λs. let 〈l',x〉 ≝ s in
     29     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).
     30
     31definition lin_function ≝ λglobals. joint_function … (lin_params globals).
     32
     33definition lin_program ≝ joint_program lin_params.
  • Deliverables/D3.3/id-lookup-branch/LIN/LINToASM.ma

    r1197 r1311  
    11include "ASM/Util.ma".
    22include "utilities/BitVectorTrieSet.ma".
    3 include "utilities/IdentifierTools.ma".
    43include "LIN/LIN.ma".
    5  
     4
    65let rec association (i: ident) (l: list (ident × nat))
    76                    on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝
     
    3231  let generated ≝
    3332    match instr with
    34     [ joint_st_sequential instr' _ ⇒
     33    [ sequential instr' _ ⇒
    3534      match instr' with
    36       [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    37       | joint_instr_cond acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     35      [ COST_LABEL lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     36      | COND acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    3837      | _ ⇒ set_empty ?
    3938      ]
    40     | joint_st_return ⇒ set_empty ?
    41     | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    42     | joint_st_extension _ ⇒ set_empty ?
    43     ]
     39    | RETURN ⇒ set_empty ?
     40    | GOTO lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) ]
    4441  in
    4542  match label with
     
    5451    set_union ? labels (statement_labels globals statement).
    5552
     53
    5654(* dpm: A = Identifier *)
    5755definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
    5856  λA: Type[0].
    5957  λglobals: list ident.
    60   λf: A × (lin_function_definition globals).
     58  λf: A × (lin_function globals).
    6159  let 〈ignore, fun_def〉 ≝ f in
    6260  match fun_def return λ_. BitVectorTrieSet ? with
    63   [ lin_fu_internal stmts proof
    64       foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
    65   | lin_fu_external _ ⇒ set_empty ?
     61  [ Internal stmts
     62      foldl ? ? (function_labels_internal globals) (set_empty ?) (pi1 … (joint_if_code ?? stmts))
     63  | External _ ⇒ set_empty ?
    6664  ].
    6765 
     
    7068  λglobals: list ident.
    7169  λlabels: BitVectorTrieSet ?.
    72   λfunct: A × (lin_function_definition globals).
     70  λfunct: A × (lin_function globals).
    7371    set_union ? labels (function_labels ? globals funct).
    74    
     72
     73(* CSC: here we are silently throwing away the region information *)
    7574definition program_labels ≝
    76   λprogram.
    77     foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program)))
    78               (set_empty ?) (lin_pr_funcs program).
    79     
     75 λprogram: lin_program.
     76    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
     77              (set_empty …) (prog_funct … program).
     78 
    8079definition data_of_int ≝ λbv. DATA bv.
    8180definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
    8281definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
    83 
    84 axiom ImplementedInRuntime: False.
    8582
    8683definition translate_statements ≝
     
    9087  λstatement: pre_lin_statement globals_old.
    9188  match statement with
    92   [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
    93   | joint_st_extension ext ⇒ Instruction (NOP ?) (* XXX: NOP or something else? *)
    94   | joint_st_return ⇒ Instruction (RET ?)
    95   | joint_st_sequential instr _ ⇒
     89  [ GOTO lbl ⇒ Jmp (word_of_identifier ? lbl)
     90  | RETURN ⇒ Instruction (RET ?)
     91  | sequential instr _ ⇒
    9692      match instr with
    97       [ joint_instr_comment comment ⇒ Comment comment
    98       | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
    99       | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
    100       | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
    101       | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
    102       | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
    103       | joint_instr_opaccs accs ⇒
     93      [ extension ext ⇒ ⊥
     94      | COMMENT comment ⇒ Comment comment
     95      | COST_LABEL lbl ⇒ Cost (word_of_identifier ? lbl)
     96      | POP _ ⇒ Instruction (POP ? accumulator_address)
     97      | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
     98      | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
     99      | CALL_ID f _ _ ⇒ Call (word_of_identifier ? f)
     100      | OPACCS accs _ _ _ _ ⇒
    104101        match accs with
    105102        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    106103        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    107104        ]
    108       | joint_instr_op1 op1
     105      | OP1 op1 _ _
    109106        match op1 with
    110107        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    111108        | Inc ⇒ Instruction (INC ? ACC_A)
    112109        ]
    113       | joint_instr_op2 op2 reg ⇒
     110      | OP2 op2 _ _ reg ⇒
    114111        match op2 with
    115112        [ Add ⇒
     
    192189          ] (subaddressing_modein … reg')
    193190        ]
    194       | joint_instr_int reg byte ⇒
     191      | INT reg byte ⇒
    195192        let reg' ≝ register_address reg in
    196193          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    205202          | _ ⇒ λother: False. ⊥
    206203          ] (subaddressing_modein … reg')
    207       | joint_instr_from_acc reg ⇒
    208         let reg' ≝ register_address reg in
    209           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    210                                                          direct;
    211                                                          registr ]] x) → ? with
    212           [ REGISTER r ⇒ λregister8: True.
    213             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
    214           | ACC_A ⇒ λacc: True.
    215             Instruction (NOP ?)
    216           | DIRECT d ⇒ λdirect8: True.
    217             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
    218           | _ ⇒ λother: False. ⊥
    219           ] (subaddressing_modein … reg')
    220       | joint_instr_to_acc reg ⇒
    221         let reg' ≝ register_address reg in
    222           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    223                                                          direct;
    224                                                          registr ]] x) → ? with
    225           [ REGISTER r ⇒ λregister9: True.
    226             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    227           | DIRECT d ⇒ λdirect9: True.
    228             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
    229           | ACC_A ⇒ λacc_a: True.
    230             Instruction (NOP ?)
    231           | _ ⇒ λother: False. ⊥
    232           ] (subaddressing_modein … reg')
    233       | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    234       | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    235       | joint_instr_address addr proof ⇒
     204      | MOVE regs ⇒
     205         match regs with
     206          [ from_acc reg ⇒
     207             let reg' ≝ register_address reg in
     208               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     209                                                              direct;
     210                                                              registr ]] x) → ? with
     211               [ REGISTER r ⇒ λregister8: True.
     212                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
     213               | ACC_A ⇒ λacc: True.
     214                 Instruction (NOP ?)
     215               | DIRECT d ⇒ λdirect8: True.
     216                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
     217               | _ ⇒ λother: False. ⊥
     218               ] (subaddressing_modein … reg')
     219          | to_acc reg ⇒
     220             let reg' ≝ register_address reg in
     221               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     222                                                              direct;
     223                                                              registr ]] x) → ? with
     224               [ REGISTER r ⇒ λregister9: True.
     225                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
     226               | DIRECT d ⇒ λdirect9: True.
     227                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
     228               | ACC_A ⇒ λacc_a: True.
     229                 Instruction (NOP ?)
     230               | _ ⇒ λother: False. ⊥
     231               ] (subaddressing_modein … reg')]
     232      | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     233      | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     234      | ADDRESS addr proof _ _ ⇒
    236235        let look ≝ association addr globals (prf ? proof) in
    237236          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    238       | joint_instr_cond_acc lbl ⇒
     237      | COND _ lbl ⇒
    239238        (* dpm: this should be handled in translate_code! *)
    240239        Instruction (JNZ ? (word_of_identifier ? lbl))
    241       | joint_instr_set_carry
     240      | SET_CARRY
    242241        Instruction (SETB ? CARRY)
    243242      ]
     
    245244  try assumption
    246245  try @ I
    247   cases ImplementedInRuntime
    248 qed.
     246qed.
     247
     248(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
     249definition ident_of_label: label → ident ≝
     250 λl. an_identifier … (word_of_identifier … l).
    249251
    250252definition build_translated_statement ≝
     
    253255  λprf.
    254256  λstatement: lin_statement globals_old.
    255     〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
     257    〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
    256258
    257259definition translate_code ≝
     
    270272    //
    271273  | #G2 #G02 #IH (* CSC: understand here *)
    272     whd in ⊢ (% → %)
    273     normalize in ⊢ (% → %)
    274     //
    275   ]
     274    whd in ⊢ (% → %) whd in match build_translated_statement normalize nodelta
     275    cases (\fst G2) normalize // ]
    276276qed.
    277277
    278278definition translate_fun_def ≝
    279   λglobals.
     279  λglobals: list (ident × nat).
    280280  λglobals_old.
    281281  λprf.
     
    283283    let 〈id, def〉 ≝ id_def in
    284284    match def with
    285     [ lin_fu_internal code proof ⇒
    286       match translate_code globals globals_old prf code return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
     285    [ Internal int ⇒
     286      let code_proof ≝ joint_if_code … (lin_params globals_old) int in
     287      match translate_code globals globals_old prf (pi1 ?? code_proof) return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
    287288      [ nil ⇒ λprf2. ⊥
    288289      | cons hd tl ⇒ λ_.
     
    294295            | None ⇒ 〈None ?, \snd r〉
    295296            ]) rest
    296       ] (translate_code_preserves_WellFormedP globals globals_old prf code proof)
    297     | _ ⇒ [ ]
     297      ] (translate_code_preserves_WellFormedP globals globals_old prf (pi1 ?? code_proof) (pi2 ?? code_proof))
     298    | External _ ⇒ [ ]
    298299    ].
    299     @ prf2
     300@prf2
    300301qed.
    301302   
     
    307308  λmain.
    308309  λfuncts.
    309   let preamble ≝
    310     match main with
    311     [ None ⇒ [ ]
    312     | Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ]
    313     ] in
    314       preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
    315 
    316 definition globals_addr_internal ≝
    317   λres_offset.
    318   λx_size: ident × nat.
     310  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
     311   preamble @
     312    (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
     313
     314(*CSC: region silently thrown away here *)
     315definition globals_addr ≝
     316 λl.
     317  let globals_addr_internal ≝
     318   λres_offset.
     319   λx_size: ident × region × nat.
    319320    let 〈res, offset〉 ≝ res_offset in
    320     let 〈x, size〉 ≝ x_size in
    321       〈〈x, offset〉 :: res, offset + size〉.
    322 
    323 definition globals_addr ≝
    324   λl.
     321    let 〈x, region, size〉 ≝ x_size in
     322      〈〈x, offset〉 :: res, offset + size〉
     323  in
    325324    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
    326      
     325
    327326(* dpm: plays the role of the string "_exit" in the O'caml source *)
    328 axiom identifier_prefix: Identifier.
     327axiom identifier_prefix: Word.
     328(*CSC: XXXXXXX wrong anyway since labels from different functions can now
     329  clash with each other and with names of functions *)
     330axiom fresh_prefix: BitVectorTrieSet 16 → Word → Word.
    329331
    330332(* dpm: fresh prefix stuff needs unifying with brian *)
    331 
    332 (*
    333 definition translate ≝
     333definition translate : lin_program → pseudo_assembly_program ≝
    334334  λp.
    335   let prog_lbls ≝ program_labels p in
     335  let prog_lbls ≝ program_labels p in
    336336  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
    337   let global_addr ≝ globals_addr (LIN_Pr_vars p) in
    338     〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉.
    339 *)
     337  let global_addr ≝ globals_addr (prog_vars … p) in
     338  let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈word_of_identifier ? x,off〉) global_addr in
     339    〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) (prog_funct … p)〉.
     340 #i normalize nodelta -global_addr' global_addr exit_label prog_lbls;
     341 normalize in match prog_var_names normalize nodelta
     342 elim (prog_vars … p) //
     343 #hd #tl #IH whd in ⊢ (% → %)
     344 whd in match globals_addr normalize nodelta
     345 whd in match (foldl ???? (hd::tl)) normalize nodelta
     346 cases hd * #id #reg #size normalize nodelta
     347 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
     348qed.
Note: See TracChangeset for help on using the changeset viewer.