Changeset 2490 for src/LIN/LINToASM.ma


Ignore:
Timestamp:
Nov 25, 2012, 1:33:09 PM (7 years ago)
Author:
tranquil
Message:

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r2443 r2490  
    4141definition association_block ≝ association block Word eq_block.
    4242
    43 definition asm_cst_well_def :
    44   list (block × Word) → beval → bool ≝
    45 λglobals,bv.match bv with
    46 [ BVptr b _ _ ⇒ member ? eq_block b (map ?? \fst globals)
    47 | _ ⇒ true
    48 ].
    49 
    5043definition vector_cast :
    5144∀A,n,m.A → Vector A n → Vector A m ≝
     
    6255qed.
    6356
    64 definition asm_byte_of_beval :
    65   ∀globals,bv.asm_cst_well_def globals bv → Byte ≝
    66   λglobals,bv.match bv return λbv.asm_cst_well_def globals bv → Byte with
    67     [ BVByte b ⇒ λ_.b
    68     | BVundef ⇒ λ_.(* any will do *) zero_byte
    69     | BVnonzero ⇒ λ_.(* any will do *) maximum 7 @@ [[ true ]]
    70     | BVnull _ ⇒ λ_.zero_byte (* is it correct? *)
    71     | BVptr b p o ⇒ λprf.
    72       let b_inst ≝ vector_cast … (S p) zero_byte (rvsplit … 2 8 (association_block … prf)) in
    73       let 〈inst, ignore〉 ≝ op2_bytes Add … false b_inst o in
    74       head' … inst
    75     ].
    76 
    77 definition asm_arg_well_def :
    78   list (block × Word) → hdw_argument → bool ≝
    79 λglobals,a.match a with
    80 [ Imm bv ⇒ asm_cst_well_def globals bv
    81 | _ ⇒ true
    82 ].
    83 
    84 definition arg_address : ∀globals,arg.asm_arg_well_def globals arg →
     57definition arg_address : hdw_argument →
    8558  [[ acc_a ; direct ; registr ; data ]] ≝
    86   λglobals,a.
     59  λa.
    8760  match a
    88   return λa.asm_arg_well_def globals a → [[ acc_a ; direct ; registr ; data ]]
    8961  with
    90   [ Reg r ⇒ λ_.register_address r
    91   | Imm bv ⇒ λprf.DATA (asm_byte_of_beval … prf)
    92   ].
    93   [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I
    94   | @I
    95   ]
     62  [ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]])
     63  | Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]])
     64  ].
     65  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I
    9666qed.
    9767
    9868definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
    9969
    100 definition asm_stmt_well_def :
    101   list (block × Word) → ∀old_globals.joint_statement LIN old_globals → bool ≝
    102   λblocks,old_globals,stmt.
    103   match stmt with
    104   [ sequential instr _ ⇒
    105     match instr with
    106     [ step_seq instr' ⇒
    107       match instr' with
    108       [ OP2 _ _ _ arg ⇒ asm_arg_well_def blocks arg
    109       | MOVE regs ⇒
    110         match regs with
    111         [ int_to_reg _ bv ⇒ asm_cst_well_def blocks bv
    112         | int_to_acc _ bv ⇒ asm_cst_well_def blocks bv
    113         | _ ⇒ true
    114         ]
    115       | _ ⇒ true
    116       ]
    117     | _ ⇒ true
    118     ]
    119   | _ ⇒ true
    120   ].
    121  
    12270definition statement_labels ≝
    12371  λg: list ident.
     
    187135definition translate_statements ≝
    188136  λglobals: list (ident × nat).
    189   λblocks: list (block × Word).
    190137  λglobals_old: list ident.
    191138  λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).
    192139  λstatement: joint_statement LIN globals_old.
    193   match statement return λstmt.asm_stmt_well_def blocks ? stmt → ? with
    194   [ final instr ⇒ λ_.
     140  match statement with
     141  [ final instr ⇒
    195142    match instr with
    196143    [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
    197144    | RETURN ⇒ Instruction (RET ?)
    198     | tailcall abs ⇒ match abs in void with [ ]
     145    | TAILCALL abs _ _ ⇒ Ⓧabs
    199146    ]
    200147  | sequential instr _ ⇒
    201       match instr return λinstr.asm_stmt_well_def blocks ? (sequential ?? instr ?) → ? with
     148      match instr with
    202149      [ step_seq instr' ⇒
    203         match instr' return λinstr'.asm_stmt_well_def ?? (sequential ?? (step_seq ?? instr') ?) → ? with
    204         [ extension_seq ext ⇒ λ_.
     150        match instr' with
     151        [ extension_seq ext ⇒
    205152          match ext with
    206153          [ SAVE_CARRY ⇒
     
    209156            Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
    210157          ]
    211         | COMMENT comment ⇒ λ_.Comment comment
    212         | COST_LABEL lbl ⇒ λ_.Cost lbl
    213         | POP _ ⇒ λ_.Instruction (POP ? accumulator_address)
    214         | PUSH _ ⇒ λ_.Instruction (PUSH ? accumulator_address)
    215         | CLEAR_CARRY ⇒ λ_.Instruction (CLR ? CARRY)
    216         | CALL_ID f _ _ ⇒ λ_.Call (toASM_ident ? f)
    217         | extension_call abs ⇒ λ_.match abs in void with [ ]
    218         | OPACCS accs _ _ _ _ ⇒ λ_.
     158        | COMMENT comment ⇒ Comment comment
     159        | COST_LABEL lbl ⇒ Cost lbl
     160        | POP _ ⇒ Instruction (POP ? accumulator_address)
     161        | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
     162        | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
     163        | CALL f _ _ ⇒
     164          match f with
     165          [ inl f_id ⇒ Call (toASM_ident ? f_id)
     166          | inr _ ⇒ (* TODO call from ptr in DPTR *)
     167            match not_implemented in False with [ ]
     168          ]
     169        | OPACCS accs _ _ _ _ ⇒
    219170          match accs with
    220171          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    221172          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    222173          ]
    223         | OP1 op1 _ _ ⇒ λ_.
     174        | OP1 op1 _ _ ⇒
    224175          match op1 with
    225176          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
     
    227178          | Rl ⇒ Instruction (RL ? ACC_A)
    228179          ]
    229         | OP2 op2 _ _ reg ⇒ λprf'.?
    230           | _ ⇒ ?] | _ ⇒ ? ]].[12: whd in prf : (?%);
    231 
    232           match op2 with
    233           [ Add ⇒
    234             let reg' ≝ arg_address … prf' in
    235             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    236                                                            direct;
    237                                                            registr;
    238                                                            data ]] x) → ? with
    239             [ ACC_A ⇒ λacc_a: True.
    240               Instruction (ADD ? ACC_A accumulator_address)
    241             | DIRECT d ⇒ λdirect1: True.
    242               Instruction (ADD ? ACC_A (DIRECT d))
    243             | REGISTER r ⇒ λregister1: True.
    244               Instruction (ADD ? ACC_A (REGISTER r))
    245             | DATA b ⇒ λdata : True.
    246               Instruction (ADD ? ACC_A (DATA b))
    247             | _ ⇒ Ⓧ
    248             ] (subaddressing_modein … reg')
    249           | Addc ⇒
    250             let reg' ≝ arg_address … prf' in
    251             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    252                                                            direct;
    253                                                            registr;
    254                                                            data ]] x) → ? with
    255             [ ACC_A ⇒ λacc_a: True.
    256               Instruction (ADDC ? ACC_A accumulator_address)
    257             | DIRECT d ⇒ λdirect2: True.
    258               Instruction (ADDC ? ACC_A (DIRECT d))
    259             | REGISTER r ⇒ λregister2: True.
    260               Instruction (ADDC ? ACC_A (REGISTER r))
    261             | DATA b ⇒ λdata : True.
    262               Instruction (ADDC ? ACC_A (DATA b))
    263             | _ ⇒ Ⓧ
    264             ] (subaddressing_modein … reg')
    265           | Sub ⇒
    266             let reg' ≝ arg_address … prf' in
    267             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    268                                                            direct;
    269                                                            registr;
    270                                                            data ]] x) → ? with
    271             [ ACC_A ⇒ λacc_a: True.
    272               Instruction (SUBB ? ACC_A accumulator_address)
    273             | DIRECT d ⇒ λdirect3: True.
    274               Instruction (SUBB ? ACC_A (DIRECT d))
    275             | REGISTER r ⇒ λregister3: True.
    276               Instruction (SUBB ? ACC_A (REGISTER r))
    277             | DATA b ⇒ λdata : True.
    278               Instruction (SUBB ? ACC_A (DATA b))
    279             | _ ⇒ Ⓧ
    280             ] (subaddressing_modein … reg')
    281           | And ⇒
    282             let reg' ≝ arg_address … prf' in
    283             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    284                                                            direct;
    285                                                            registr;
    286                                                            data ]] x) → ? with
    287             [ ACC_A ⇒ λacc_a: True.
    288               Instruction (NOP ?)
    289             | DIRECT d ⇒ λdirect4: True.
    290               Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    291             | REGISTER r ⇒ λregister4: True.
    292               Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    293             | DATA b ⇒ λdata : True.
    294               Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
    295             | _ ⇒ Ⓧ
    296             ] (subaddressing_modein … reg')
    297           | Or ⇒
    298             let reg' ≝ arg_address … prf' in
    299             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    300                                                            direct;
    301                                                            registr ; data ]] x) → ? with
    302             [ ACC_A ⇒ λacc_a: True.
    303               Instruction (NOP ?)
    304             | DIRECT d ⇒ λdirect5: True.
    305               Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
    306             | REGISTER r ⇒ λregister5: True.
    307               Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
    308             | DATA b ⇒ λdata : True.
    309               Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
    310             | _ ⇒ Ⓧ
    311             ] (subaddressing_modein … reg')
    312           | Xor ⇒
    313             let reg' ≝ arg_address … prf' in
    314             match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    315                                                            direct;
    316                                                            registr ; data ]] x) → ? with
    317             [ ACC_A ⇒ λacc_a: True.
    318               Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉))
    319             | DIRECT d ⇒ λdirect6: True.
    320               Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
    321             | REGISTER r ⇒ λregister6: True.
    322               Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
    323             | DATA b ⇒ λdata : True.
    324               Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
    325             | _ ⇒ Ⓧ
    326             ] (subaddressing_modein … reg')
    327           ]
    328         | LOAD _ _ _ ⇒ λ_.Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    329         | STORE _ _ _ ⇒ λ_.Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    330         | ADDRESS addr proof _ _ ⇒ λ_.
     180        | OP2 op2 _ _ reg ⇒
     181          match arg_address … reg
     182          return λx.is_in … [[ acc_a;
     183                                 direct;
     184                                 registr;
     185                                 data ]] x → ? with
     186          [ ACC_A ⇒ λacc_a: True.
     187            match op2 with
     188            [ Add ⇒ Instruction (ADD ? ACC_A accumulator_address)
     189            | Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address)
     190            | Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address)
     191            | Xor ⇒ Instruction (CLR ? ACC_A)
     192            | _ ⇒ Instruction (NOP ?)
     193            ]
     194          | DIRECT d ⇒ λdirect1: True.
     195            match op2 with
     196            [ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d))
     197            | Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d))
     198            | Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d))
     199            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     200            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
     201            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
     202            ]
     203          | REGISTER r ⇒ λregister1: True.
     204            match op2 with
     205            [ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r))
     206            | Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r))
     207            | Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r))
     208            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     209            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
     210            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
     211            ]
     212          | DATA b ⇒ λdata : True.
     213            match op2 with
     214            [ Add ⇒ Instruction (ADD ? ACC_A (DATA b))
     215            | Addc ⇒ Instruction (ADDC ? ACC_A (DATA b))
     216            | Sub ⇒ Instruction (SUBB ? ACC_A (DATA b))
     217            | And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
     218            | Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
     219            | Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
     220            ]
     221          | _ ⇒ Ⓧ
     222          ] (subaddressing_modein …)
     223        | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     224        | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     225        | ADDRESS addr proof _ _ ⇒
    331226          let look ≝ association_ident addr globals (prf ? proof) in
    332227            Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    333         | SET_CARRY ⇒ λ_.
     228        | SET_CARRY ⇒
    334229          Instruction (SETB ? CARRY)
    335230        | MOVE regs ⇒
    336           match regs return λregs.asm_stmt_well_def ?? (sequential ?? (step_seq ?? (MOVE regs)) ?) → ? with
    337           [ to_acc _ reg ⇒ λ_.
    338              let reg' ≝ register_address reg in
    339                match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     231          match regs with
     232          [ to_acc _ reg ⇒
     233            match register_address reg return λx.is_in … [[ acc_a;
    340234                                                              direct;
    341                                                               registr ]] x) → ? with
    342                [ REGISTER r ⇒ λregister9: True.
    343                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    344                | DIRECT d ⇒ λdirect9: True.
    345                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
    346                | ACC_A ⇒ λacc_a: True.
    347                  Instruction (NOP ?)
    348                | _ ⇒ λother: False. ⊥
    349                ] (subaddressing_modein … reg')
    350           | from_acc reg _ ⇒ λ_.
    351              let reg' ≝ register_address reg in
    352                match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     235                                                              registr]] x → ? with
     236           [ REGISTER r ⇒ λregister9: True.
     237             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
     238           | DIRECT d ⇒ λdirect9: True.
     239             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
     240           | ACC_A ⇒ λacc_a: True.
     241             Instruction (NOP ?)
     242           | _ ⇒ Ⓧ
     243           ] (subaddressing_modein …)
     244         | from_acc reg _ ⇒
     245            match register_address reg return λx.is_in … [[ acc_a;
    353246                                                              direct;
    354                                                               registr ]] x) → ? with
    355                [ REGISTER r ⇒ λregister8: True.
    356                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
    357                | ACC_A ⇒ λacc: True.
    358                  Instruction (NOP ?)
    359                | DIRECT d ⇒ λdirect8: True.
    360                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
    361                | _ ⇒ λother: False. ⊥
    362                ] (subaddressing_modein … reg')
    363           | int_to_reg reg bv ⇒ λprf'.
    364             let b ≝ asm_byte_of_beval … prf' in
    365             let reg' ≝ register_address reg in
    366               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    367                                                              direct;
    368                                                              registr ]] x) → ? with
    369               [ REGISTER r ⇒ λregister7: True.
    370                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
    371               | ACC_A ⇒ λacc: True.
    372                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
    373               | DIRECT d ⇒ λdirect7: True.
    374                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
    375               | _ ⇒ λother: False. ⊥
    376               ] (subaddressing_modein … reg')
    377           | int_to_acc _ bv ⇒ λprf'.
    378             let b ≝ asm_byte_of_beval … prf' in
    379             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
     247                                                              registr ]] x → ? with
     248            [ REGISTER r ⇒ λregister8: True.
     249             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
     250            | ACC_A ⇒ λacc: True.
     251             Instruction (NOP ?)
     252            | DIRECT d ⇒ λdirect8: True.
     253             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
     254            | _ ⇒ Ⓧ
     255            ] (subaddressing_modein …)
     256          | int_to_reg reg b ⇒
     257            match register_address reg return λx.is_in … [[ acc_a;
     258                                                              direct;
     259                                                              registr ]] x → ? with
     260            [ REGISTER r ⇒ λregister7: True.
     261              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
     262            | ACC_A ⇒ λacc: True.
     263               if eq_bv … (bv_zero …) b then
     264                  Instruction (CLR ? ACC_A)
     265               else
     266                  Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
     267            | DIRECT d ⇒ λdirect7: True.
     268              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
     269            | _ ⇒ Ⓧ
     270            ] (subaddressing_modein …)
     271          | int_to_acc _ b ⇒
     272            if eq_bv … (bv_zero …) b then
     273              Instruction (CLR ? ACC_A)
     274            else
     275              Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
    380276          ]
    381277        ]
    382       | COND _ lbl ⇒ λ_.
     278      | COND _ lbl ⇒
    383279        (* dpm: this should be handled in translate_code! *)
    384280        Instruction (JNZ ? (toASM_ident ? lbl))
     
    386282    ].
    387283  try @I
    388   assumption
    389284qed.
    390285
     
    411306  λglobals_old.
    412307  λprf.
    413   λid_def.
     308  λid_def : ident × (joint_function LIN globals_old).
    414309    let 〈id, def〉 ≝ id_def in
    415310    match def with
     
    436331let rec flatten_fun_defs
    437332  (globals: list (ident × nat)) (globals_old: list ident) (prf: ?) (initial_pc: nat)
    438     (the_list: list ((identifier SymbolTag) × (fundef (joint_internal_function LIN globals_old))))
     333    (the_list: list ((identifier SymbolTag) × (joint_function LIN globals_old)))
    439334      on the_list: ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) ≝
    440335  match the_list return λx. ((list (option Identifier × pseudo_instruction)) × (identifier_map ? nat)) with
     
    457352  λexit_label.
    458353  λmain.
    459   λfuncts.
     354  λfuncts : list (ident × (joint_function LIN ?)).
    460355  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
    461356  let 〈flattened, map〉 ≝ flatten_fun_defs globals globals_old prf 6 (* Size of preamble above *) functs in
     
    487382  let global_addr ≝ globals_addr (prog_vars … p) in
    488383  let global_addr' ≝ map … (λx_off. let 〈x,off〉 ≝ x_off in 〈toASM_ident ? x, bitvector_of_nat 16 off〉) global_addr in
    489   let 〈translated, funct_map〉 ≝ translate_functs global_addr (prog_var_names … p) ? exit_label (toASM_ident … (prog_main … p)) (prog_funct … p) in
     384  let 〈translated, funct_map〉 ≝
     385    translate_functs global_addr (prog_var_names … p) ? exit_label
     386    (toASM_ident … (prog_main … p)) (prog_funct ?? p) in
    490387    〈〈funct_map, global_addr'〉, translated〉.
    491388 #i normalize nodelta -global_addr' -global_addr -exit_label -prog_lbls;
Note: See TracChangeset for help on using the changeset viewer.