Changeset 3039


Ignore:
Timestamp:
Mar 29, 2013, 5:45:14 PM (4 years ago)
Author:
tranquil
Message:
  • merged and extended MovSuccessor? and Mov in one instruction (Mov dst

ident offset)

  • JMP now correctly uses ACCDPTR argument
  • LINToASM: ADDRESS now translate to a symbolical Mov (now a preamble

is generated), and globals initialization is fixed accordingly

Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2999 r3039  
    562562| RETI: preinstruction A
    563563| NOP: preinstruction A
    564 | JMP: [[indirect_dptr]] → preinstruction A.
     564| JMP: [[acc_dptr]] → preinstruction A.
    565565
    566566definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
     
    979979  | Jmp: Identifier → pseudo_instruction
    980980  | Jnz : [[acc_a]] → Identifier → Identifier → pseudo_instruction
    981   | MovSuccessor : [[ acc_a ; direct ; registr ]] → word_side → Identifier → pseudo_instruction
    982981  | Call: Identifier → pseudo_instruction
    983   | Mov: [[dptr]] → Identifier → pseudo_instruction.
     982  | Mov: ([[dptr]] ⊎ ([[ acc_a ; direct ; registr ]] × word_side)) →
     983    Identifier → Word → pseudo_instruction.
    984984
    985985definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
  • src/ASM/Assembly.ma

    r3034 r3039  
    538538      let address ≝ ADDR16 lookup_address in
    539539        [ LCALL address ]
    540   | Mov d trgt ⇒
    541     let address ≝ DATA16 (lookup_datalabels trgt) in
     540  | Mov d trgt off ⇒
     541    let addr ≝ \fst (add_16_with_carry … (lookup_datalabels trgt) off false) in
     542    match d with
     543    [ inl _ ⇒
     544      let address ≝ DATA16 addr in
    542545      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
     546    | inr pr ⇒
     547      let v ≝ DATA (match \snd pr with
     548        [ LOW ⇒ \snd (vsplit … 8 8 addr)
     549        | HIGH ⇒ \fst (vsplit … 8 8 addr)
     550        ]) in
     551     match \fst pr return λx. bool_to_Prop (is_in ? [[acc_a;direct;registr]] x) → ? with
     552     [ ACC_A ⇒ λ_.
     553        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, v〉))))))]     
     554     | DIRECT b1 ⇒ λ_.
     555        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT b1, v〉)))))]
     556     | REGISTER r ⇒ λ_.
     557        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, v〉))))))]
     558     | _ ⇒ Ⓧ ] (subaddressing_modein …)]
    543559  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma policy ppc instr
    544560  | Jmp jmp ⇒
     
    566582        LJMP (ADDR16 lookup_address2);
    567583        LJMP (ADDR16 lookup_address1) ]
    568   | MovSuccessor dst ws lbl ⇒
     584  (*| MovSuccessor dst ws lbl ⇒
    569585     let addr ≝ lookup_labels lbl in
    570586     let 〈high, low〉 ≝ vsplit ? 8 8 addr in
     
    576592        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT b1, v〉)))))]
    577593     | REGISTER r ⇒ λ_.
    578         [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, v〉))))))]     | _ ⇒ λK. match K in False with [ ] ] (subaddressing_modein … dst)
     594        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, v〉))))))]     | _ ⇒ λK. match K in False with [ ] ] (subaddressing_modein … dst)*)
    579595  ].
    580596  try %
     
    648664    let labels ≝ \fst (create_label_cost_map instr_list) in
    649665    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    650     let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x (zero …) in
     666    let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x (lookup_labels x) in
    651667    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    652668    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
     
    668684   \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi).
    669685#lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2
    670 cases pi //
     686cases pi // * [ #addr #Id #off % ] * #addr * @(subaddressing_mode_elim … addr) //
    671687qed.
    672688
     
    791807  [2: @pair_elim #x #y #_ cases (?∧?)]
    792808  normalize in ⊢ (?%?); //
    793 |7: #label whd in match (assembly_1_pseudoinstruction ??????);
     809|6: #label whd in match (assembly_1_pseudoinstruction ??????);
    794810  whd in match (expand_pseudo_instruction ??????);
    795811  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
    796812  normalize in ⊢ (?%?); //
    797 |8: #dptr #id normalize in ⊢ (?%?); //
    798813|5: #acc #dst1 #dst2 normalize in ⊢ (?%?); //
    799 |6: #dst #ws #lbl whd in match (assembly_1_pseudoinstruction ??????);
     814|7: * [ #dptr #id #offset normalize in ⊢ (?%?); //]
     815    * #dst @(subaddressing_mode_elim … dst) [2,3: #w] * #lbl #off
     816    whd in match (assembly_1_pseudoinstruction ??????);
    800817    whd in match (expand_pseudo_instruction ??????);
    801     @pair_elim #high #low #EQ @(subaddressing_mode_elim … dst)
    802     normalize nodelta [2,3: #w] normalize in ⊢ (?%?); //
     818    lapply (vsplit bool 8 8 ?) * #high #low
     819    normalize in ⊢ (?%?); //
    803820]
    804821qed.
     
    820837       let datalabels ≝ construct_datalabels preamble in
    821838       let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    822        let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
     839       let lookup_datalabels ≝ λx.lookup_def … datalabels x (lookup_labels x) in
    823840       ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < |instr_list|.
    824841         let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc ppc_ok in
     
    839856  let datalabels ≝ construct_datalabels preamble in
    840857  let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
    841   let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
     858  let lookup_datalabels ≝ λx.lookup_def … datalabels x (lookup_labels x) in
    842859  let 〈next_pc,revcode〉 ≝ pi1 … (
    843860     foldl_strong
     
    10721089          else
    10731090            〈4, 4〉
    1074       | JMP _ ⇒ ? (*CSC: To be implemented*)
     1091      | JMP _ ⇒ 〈2, 2〉
    10751092      | JNC lbl ⇒
    10761093        let lookup_address ≝ sigma (lookup_labels lbl) in
     
    12261243       let ticks ≝ ticks_of_instruction (NOP ?) in
    12271244         〈ticks, ticks〉
    1228     | Jnz _ _ _ ⇒ ? (*CSC: To be implemented*)
    1229     | MovSuccessor _ _ _ ⇒ ? (*CSC: To be implemented *)
     1245    | Jnz _ _ _ ⇒ 〈4, 4〉
    12301246    | Jmp jmp ⇒
    12311247      let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
     
    12511267      else
    12521268        〈2, 2〉 (* LCALL *)
    1253     | Mov dptr tgt ⇒ 〈2, 2〉
    1254     ].
    1255 cases daemon (*CSC: The three new pseudoinstruction cases*)
    1256 qed.
     1269    | Mov dst lbl off ⇒
     1270      match dst with
     1271      [ inl _ ⇒ 〈2, 2〉
     1272      | inr pr ⇒
     1273        match \fst pr return λx.is_in … [[ acc_a; direct; registr]] x → ? with
     1274        [ REGISTER r ⇒ λ_.〈1, 1〉
     1275        | DIRECT d ⇒ λ_.〈2, 2〉
     1276        | ACC_A ⇒ λ_.〈1, 1〉
     1277        | _ ⇒ Ⓧ] (subaddressing_modein …)]
     1278     ].
    12571279
    12581280definition ticks_of:
  • src/ASM/Fetch.ma

    r2999 r3039  
    400400         let 〈b,v〉≝  head … v in if b then
    401401          let 〈b,v〉≝  head … v in if b then
    402            〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
     402           〈〈JMP … ACC_DPTR, pc〉, 2〉
    403403          else
    404404           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
  • src/ASM/Interpret.ma

    r2906 r3039  
    11911191qed-.
    11921192
    1193 definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝
    1194   λticks,cm,s,instr,pc.
     1193definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm.
     1194  (Identifier → Word) →
     1195  (Identifier → Word) →
     1196  PseudoStatus cm → ? → ? → PseudoStatus cm ≝
     1197  λticks,cm,addr_of_label,addr_of_symbol,s,instr,pc.
    11951198  let s ≝ set_program_counter ?? s pc in
    11961199  let s ≝
     
    12011204    | Jmp jmp ⇒
    12021205       let s ≝ set_clock … s (\fst ticks + clock … s) in
    1203         set_program_counter … s (address_of_word_labels (code cm) jmp)
     1206        set_program_counter … s (addr_of_label jmp)
    12041207    | Jnz acc dst1 dst2 ⇒
    12051208       if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
    12061209        let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1207          set_program_counter … s (address_of_word_labels (code cm) dst1)
     1210         set_program_counter … s (addr_of_label dst1)
    12081211       else
    12091212        let s ≝ set_clock ?? s (\snd ticks + clock … s) in
    1210          set_program_counter … s (address_of_word_labels (code cm) dst2)
    1211     | MovSuccessor dst ws lbl ⇒
    1212       let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1213       let addr ≝ address_of_word_labels (code cm) lbl in
    1214       let 〈high, low〉 ≝ vsplit ? 8 8 addr in
    1215       let v ≝ match ws with [ HIGH ⇒ high | LOW ⇒ low ] in
    1216        set_arg_8 … s dst v     
     1213         set_program_counter … s (addr_of_label dst2)
    12171214    | Call call ⇒
    12181215      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1219       let a ≝ address_of_word_labels (code cm) call in
     1216      let a ≝ addr_of_label call in
    12201217      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    12211218      let s ≝ set_8051_sfr … s SFR_SP new_sp in
     
    12261223      let s ≝ write_at_stack_pointer … s pc_bu in
    12271224        set_program_counter … s a
    1228     | Mov dptr ident
     1225    | Mov dst ident off
    12291226      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
    1230       let the_preamble ≝ preamble cm in
    1231       let data_labels ≝ construct_datalabels the_preamble in
    1232         set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
     1227      let v ≝ addr_of_symbol ident in
     1228      match dst with
     1229      [ inl dptr ⇒ set_arg_16 … s v dptr
     1230      | inr pr ⇒
     1231        let v' ≝ match \snd pr with
     1232        [ LOW ⇒ \snd (vsplit … 8 8 v)
     1233        | HIGH ⇒ \fst (vsplit … 8 8 v)
     1234        ] in
     1235        set_arg_8 ?? s (\fst pr) v'
     1236      ]
    12331237    ]
    12341238  in
    12351239    s.
    1236   [2: % | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
     1240  @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    12371241qed.
    12381242
    12391243definition execute_1_pseudo_instruction:
    1240  ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |code cm| → nat × nat) → ∀s:PseudoStatus cm.
     1244 ∀cm.(∀ppc:Word. nat_of_bitvector … ppc < |code cm| → nat × nat) →
     1245  (Identifier → Word) →
     1246  (Identifier → Word) →
     1247 ∀s:PseudoStatus cm.
    12411248   nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|code cm| →
    12421249    PseudoStatus cm
    12431250
    1244   λcm,ticks_of,s,pc_ok.
     1251  λcm,ticks_of,addr_of_label,addr_of_symbol,s,pc_ok.
    12451252  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (code cm) (program_counter … s) pc_ok in
    12461253  let ticks ≝ ticks_of (program_counter … s) pc_ok in
    1247    execute_1_pseudo_instruction0 ticks cm s instr pc.
     1254   execute_1_pseudo_instruction0 ticks cm addr_of_label addr_of_symbol s instr pc.
    12481255
    12491256let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝
  • src/ASM/Interpret2.ma

    r2999 r3039  
    5151(* Move next function in interpret? *)
    5252definition execute_1_pseudo_instruction':
    53  ∀cm. ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
    54  λcm,sigma,policy,status.
     53 ∀cm.(Identifier → Word) → (Identifier → Word) →
     54 ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
     55 λcm,addr_of_label,addr_of_symbol,sigma,policy,status.
    5556  execute_1_pseudo_instruction cm
    56    (ticks_of cm  sigma policy) status ….
     57   (ticks_of cm  sigma policy) addr_of_label addr_of_symbol status ….
    5758cases daemon (*CSC: we need to prove that we remain inside the program
    5859 (code closed), which is impossible in case of function pointers.
     
    6869  | Jmp _ ⇒ cl_other
    6970  | Jnz _ _ _ ⇒ cl_jump
    70   | MovSuccessor _ _ _ ⇒ cl_other
    7171  | Call _ ⇒ cl_call
    72   | Mov _ _ ⇒ cl_other ].
     72  | Mov _ _ _ ⇒ cl_other ].
    7373
    7474definition ASM_classify: ∀cm. PseudoStatus cm → status_class ≝
     
    108108
    109109definition ASM_as_call_ident:
    110  ∀prog,sigma,policy.(Σs:PseudoStatus prog. ASM_classify … s = cl_call) → ident
     110 ∀prog.(Identifier → Word) → (Identifier → Word) →
     111 ∀sigma,policy.(Σs:PseudoStatus prog. ASM_classify … s = cl_call) → ident
    111112
    112  λprog,sigma,policy,s0.
    113   let st ≝ execute_1_pseudo_instruction' prog sigma policy s0 in
     113 λprog,addr_of_label,addr_of_symbol,sigma,policy,s0.
     114  let st ≝ execute_1_pseudo_instruction' prog addr_of_label addr_of_symbol
     115    sigma policy s0 in
    114116  let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? (program_counter … st)) … (code prog) ? in
    115117  match lbl with
     
    122124
    123125definition ASM_abstract_status:
    124  ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
    125   λprog,sigma,policy.
     126 ∀prog:pseudo_assembly_program.
     127  (Identifier → Word) →
     128  (Identifier → Word) →
     129 ∀sigma,policy.abstract_status ≝
     130  λprog,addr_of_label,addr_of_symbol,sigma,policy.
    126131    mk_abstract_status
    127132      (PseudoStatus prog)
    128       (λs1,s2. execute_1_pseudo_instruction' … sigma policy s1 = s2)
     133      (λs1,s2. execute_1_pseudo_instruction' … addr_of_label addr_of_symbol
     134        sigma policy s1 = s2)
    129135      word_deqset
    130136      (program_counter …)
     
    133139      (ASM_next_instruction_properly_relates_program_counters prog)
    134140      (ASM_as_result …)
    135       (ASM_as_call_ident prog sigma policy …)
     141      (ASM_as_call_ident prog addr_of_label addr_of_symbol sigma policy …)
    136142      ?.
    137143 * #st whd in ⊢ (??%? → ?); cases (\fst (fetch_pseudo_instruction ???)) [*]
     
    142148 pseudo_assembly_program → ∀sigma,policy. preclassified_system ≝
    143149 λc,sigma,policy.
     150  let label_map ≝ \fst (create_label_cost_map (code … c)) in
     151  let symbol_map ≝ construct_datalabels (preamble … c) in
     152  let addr_of_label ≝ λx.bitvector_of_nat ? (lookup_def … label_map x 0) in
     153  let addr_of_symbol ≝ λx.lookup_def … symbol_map x (addr_of_label x) in
    144154  mk_preclassified_system_of_abstract_status
    145155   (pseudo_assembly_program × (Word → Word) × (Word → bool))
    146    (ASM_abstract_status c sigma policy)
    147    (λst. return (execute_1_pseudo_instruction' … sigma policy st))
     156   (ASM_abstract_status c addr_of_label addr_of_symbol sigma policy)
     157   (λst. return (execute_1_pseudo_instruction' … addr_of_label addr_of_symbol sigma policy st))
    148158   (initialise_status … c).
  • src/ASM/PolicyFront.ma

    r3034 r3039  
    145145    | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ]
    146146    ]
    147   | Mov d trgt ⇒
    148      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]
     147  | Mov d trgt off ⇒
     148    match d with
     149    [ inl _ ⇒
     150      let address ≝ DATA16 (bv_zero 16) in
     151      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
     152    | inr pr ⇒
     153      let v ≝ DATA (bv_zero 8) in
     154     match \fst pr return λx. bool_to_Prop (is_in ? [[acc_a;direct;registr]] x) → ? with
     155     [ ACC_A ⇒ λ_.
     156        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, v〉))))))]     
     157     | DIRECT b1 ⇒ λ_.
     158        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT b1, v〉)))))]
     159     | REGISTER r ⇒ λ_.
     160        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, v〉))))))]
     161     | _ ⇒ Ⓧ ] (subaddressing_modein …)]
    149162  | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr
    150163  | Jnz acc dst1 dst2 ⇒
     
    152165        LJMP (ADDR16 (zero ?));
    153166        LJMP (ADDR16 (zero ?)) ]
    154   | MovSuccessor dst ws lbl ⇒
    155      let v ≝ DATA (zero …) in
    156      match dst return λx. bool_to_Prop (is_in ? [[acc_a;direct;registr]] x) → ? with
    157      [ ACC_A ⇒ λ_.
    158         [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈
    159 ACC_A, v〉))))))]
    160      | DIRECT b1 ⇒ λ_.
    161         [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT b1, v〉)))))]
    162      | REGISTER r ⇒ λ_.
    163         [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈
    164 REGISTER r, v〉))))))]
    165      | _ ⇒ λK. match K in False with [ ] ] (subaddressing_modein … dst)
    166167  | Jmp jmp ⇒
    167168    match jmp_len with
     
    605606   #EQ normalize in EQ; destruct(EQ)
    606607  |2,3,8: #x [3: #y] #H cases H
    607   |4,7: #id #_ cases a cases b #H try % normalize in H; destruct(H)
    608   |5,6: #x #y #z #H normalize in H; cases H
     608  |4,6: #id #_ cases a cases b #H try % normalize in H; destruct(H)
     609  |5,7: #x #y #z #H normalize in H; cases H
    609610 ]
    610611qed.
     
    614615 #a #b #i cases i
    615616 [2,3,8: #x [3: #y] #H cases H
    616  |4,7: #id #_ cases a cases b @leb_true_to_le / by refl/
     617 |4,6: #id #_ cases a cases b @leb_true_to_le / by refl/
    617618 |1: #pi cases pi
    618619    try (#x #y #H) try (#x #H) try (#H) cases H
     
    621622    cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
    622623    @(subaddressing_mode_elim … a1) #w %
    623  |5,6: #x #y #z #H cases H
     624 |5,7: #x #y #z #H cases H
    624625 ]
    625626qed.
     
    659660              try (#x #id #Hnth_eq #Hsafe) try (#id #Hnth_eq #Hsafe) try (#Hnth_eq #Hsafe)
    660661              try % lapply Hsafe -Hsafe lapply Hnth_eq -Hnth_eq lapply id -id
    661           |2,3,5,8: #x [3: #y #z | 4: #y] normalize nodelta #_ #_ %
    662           |6: #x #y #z normalize nodelta #_ #_ @pair_elim #w1 #w2 #_
    663               @(subaddressing_mode_elim … x) try #k % ]
     662          |2,3,5: #x [3: #y #z | 4: #y] normalize nodelta #_ #_ %
     663          |7: * [ #x normalize nodelta #y #z #_ #_ % ]
     664            * #x @(subaddressing_mode_elim … x) [2,3: #y] * #lbl #off
     665            normalize nodelta #_ #_ lapply (vsplit ? 8 8 ?) * #w1 #w2 % ]
    664666            #id lapply (Hpc_equal i (le_S_to_le … Hi))
    665667            lapply (Hpc_equal (S i) Hi)
     
    772774  ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i.
    773775 #i cases i
    774  [2,3,8: #x [3: #y] #Hj #j1 #j2 %
    775  |5,6: #x #y #z #_ #j1 #j2 %
    776  |4,7: #x #Hi cases Hi
     776 [2,3: #x [3: #y] #Hj #j1 #j2 %
     777 |5,7: #x #y #z #_ #j1 #j2 %
     778 |4,6: #x #Hi cases Hi
    777779 |1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2)
    778780     try % cases Hj ]
  • src/ASM/PolicyStep.ma

    r2714 r3039  
    7171 | <Heq2 >Hi >lookup_insert_miss
    7272   [ >lookup_insert_hit cases instr in Heq1;
    73      [2,3,8: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    74      |5,6: #x #y #z normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ %
    75      |4,7: #x normalize nodelta #Heq1 >nth_append_second try %
     73     [2,3: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
     74     |5,7: #x #y #z normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ %
     75     |4,6: #x normalize nodelta #Heq1 >nth_append_second try %
    7676           <minus_n_n #abs cases abs
    7777     |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
     
    148148   |Cost (_:costlabel)⇒None jump_length
    149149   |Jnz _ _ _ ⇒ None ?
    150    |MovSuccessor _ _ _ ⇒ None ?
    151150   |Jmp (j:Identifier)⇒
    152151    Some jump_length
     
    155154    Some jump_length
    156155    (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
    157    |Mov (_:[[dptr]]) (_:Identifier)⇒None jump_length]
     156   |Mov _ _ _ ⇒ None jump_length]
    158157    in option
    159158    return λ_:(option jump_length).(jump_length×ℕ)
     
    206205        [ >lookup_insert_hit normalize nodelta
    207206          inversion instr in Heq1; normalize nodelta
    208           [4,7: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
     207          [4,6: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    209208          | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta
    210209            lapply (destination_of_None_to_is_jump_false pi)
     
    214213            | #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
    215214            ]
    216           |5,6: #x #y #z #Heqi
    217           |2,3,8: #x [3: #y] #Heqi ]
     215          |5,7: #x #y #z #Heqi
     216          |2,3: #x [3: #y] #Heqi ]
    218217          #Hj <(proj1 ?? (pair_destruct ?????? Hj))
    219218          lapply (pi2 ?? old_sigma (|prefix|) ??) try assumption
     
    266265   |Cost (_:costlabel)⇒None jump_length
    267266   |Jnz _ _ _ ⇒ None ?
    268    |MovSuccessor _ _ _ ⇒ None ?
    269267   |Jmp (j:Identifier)⇒
    270268    Some jump_length
     
    273271    Some jump_length
    274272    (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
    275    |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
     273   |Mov _ _ _⇒None jump_length]
    276274    in option
    277275    return λ_:(option jump_length).(jump_length×ℕ)
     
    432430    >Hpolicy1
    433431    [ cases instr in Heq1 Heq;
    434       [2,3,8: #x [3: #y] normalize nodelta #_ #_ %
    435       |5,6: #x #y #z #_ #_ %
     432      [2,3: #x [3: #y] normalize nodelta #_ #_ %
     433      |5,7: #x #y #z #_ #_ %
    436434      |1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
    437435          normalize nodelta cases (destination_of ?) normalize nodelta [#_ #_ %]]
     
    585583            try (#x #y #Heq1 #Hadded #X) try (#x #Heq1 #Hadded #X) try (#Heq1 #Hadded #X)
    586584            <(proj2 ?? (pair_destruct ?????? Heq1)) >X @plus_left_monotone
    587             [1,3,4,6,7,9: @instruction_size_irrelevant try %
     585            [1,3,4,6,8: @instruction_size_irrelevant try %
    588586              whd in match is_jump; normalize nodelta >dest_None %
    589587            |*: >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ'
     
    738736    (* USE[pass]: lookup p = lookup old_sigma + added *)
    739737    >Hpolicy2
    740     [1,3,4,6,7,9:
     738    [1,3,4,6,8:
    741739      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
    742740      -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
     
    746744      @plus_right_monotone @instruction_size_irrelevant try %
    747745      whd in match is_jump; normalize nodelta >y %
    748     |2,5,6,8:
     746    |*:
    749747      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H
    750748      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; #EQ
     
    828826   Some jump_length
    829827   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    830   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]*)
     828  |Mov _ _ _⇒None jump_length] *)
    831829 ∀inc_pc : ℕ.
    832830 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
     
    869867   |Cost (_:costlabel)⇒None jump_length
    870868   |Jnz _ _ _ ⇒ None ?
    871    |MovSuccessor _ _ _ ⇒ None ?
    872869   |Jmp (j:Identifier)⇒
    873870    Some jump_length
     
    876873    Some jump_length
    877874    (select_call_length labels old_sigma 〈inc_pc,inc_sigma〉 (|prefix|) c)
    878    |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
     875   |Mov _ _ _⇒None jump_length]
    879876    in option
    880877    return λ_:(option jump_length).(jump_length×ℕ)
     
    904901    Some jump_length
    905902    (select_call_length labels old_sigma inc_pc_sigma (|prefix|) c)
    906    |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
     903   |Mov _ _ _⇒None jump_length]
    907904    in option
    908905    return λ_:(option jump_length).ℕ
     
    1002999      ]
    10031000      normalize nodelta cases instr in Hjump Heq1;
    1004       [1,9: #pi normalize nodelta cases pi
     1001      [1,8: #pi normalize nodelta cases pi
    10051002        try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1)
    10061003        try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id
    1007       |2,3,8,10,11,16: #y [3,6: #id] normalize nodelta #abs cases abs
    1008       |5,6,13,14: #x #y #z #abs cases abs
     1004      |2,3,7,9,10,14: #y [3,6: #id #off] normalize nodelta #abs cases abs
     1005      |5,12: #x #y #z #abs cases abs
    10091006      ]
    10101007      #id #Hjump normalize nodelta #Heq1
     
    10521049          #Holdeq >prf >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
    10531050          >p1 cases instr in Hjump Heq1;
    1054           [1,9: #pi normalize nodelta cases pi
     1051          [1,8: #pi normalize nodelta cases pi
    10551052            try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1)
    10561053            try (cases Hjump) lapply Heq1 -Heq1 lapply Hjump -Hjump lapply id -id
    1057           |2,3,8,10,11,16: #y [3,6: #id] normalize nodelta #abs cases abs
    1058           |5,6,13,14: #x #y #z #abs cases abs
     1054          |2,3,7,9,10,14: #y [3,6: #id #off] normalize nodelta #abs cases abs
     1055          |5,12: #x #y #z #abs cases abs
    10591056          ]
    10601057          #id #Hjump normalize nodelta <Hjump #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1))
  • src/LIN/LINToASM.ma

    r3028 r3039  
    88
    99(* utilities to provide Identifier's and addresses  *)
    10 record ASM_universe (globals : list ident) : Type[0] :=
     10record ASM_universe : Type[0] :=
    1111{ id_univ : universe ASMTag
    1212; current_funct : ident
    1313; ident_map : identifier_map SymbolTag Identifier
    1414; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier)
    15 ; address_map : identifier_map SymbolTag Word
    16 ; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map
    1715; fresh_cost_label: Pos
    1816}.
    1917
    2018definition report_cost:
    21  ∀globals. costlabel → state_monad (ASM_universe globals) unit ≝
    22  λglobals,cl,u.
     19 costlabel → state_monad ASM_universe unit ≝
     20 λcl,u.
    2321  let clw ≝ word_of_identifier … cl in
    2422  if leb (fresh_cost_label … u) clw then
    2523   〈mk_ASM_universe … (id_univ … u) (current_funct … u) (ident_map … u)
    26     (label_map … u) (address_map … u) (globals_are_in … u) (succ clw), it〉 
     24    (label_map … u) (succ clw), it〉 
    2725  else
    2826   〈u,it〉.
    2927
    30 definition new_ASM_universe :
    31 ∀p : joint_program LIN.ASM_universe (prog_var_names … p) ≝
    32 λp.
    33   let globals_addr_internal ≝
    34    λres_offset : identifier_map SymbolTag Word × Z.
    35    λx_size: ident × region × (list init_data).
    36     let 〈res, offset〉 ≝ res_offset in
    37     let 〈x, region, data〉 ≝ x_size in
    38       〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat (size_init_data_list data)〉 in
    39       (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
    40   let addresses ≝ foldl ?? globals_addr_internal 〈empty_map …, -(S (globals_stacksize … p))〉 (prog_vars ?? p) in
    41 mk_ASM_universe ? (mk_universe … one)
    42   (an_identifier … one (* dummy *))
    43   (empty_map …) (empty_map …)
    44   (\fst addresses) ? one.
    45 @hide_prf
    46 normalize nodelta
    47 cases p -p * #vars #functs #main #cost_init
    48 #i #H
    49 letin init_val ≝ (〈empty_map ? Word, -(S (globals_stacksize ??))〉)
    50 cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
    51 [ %2{H} ] -H
    52 lapply i -i lapply init_val -init_val elim vars -vars
    53 [2: ** #id #r #v #tl #IH ] #init_val #i
    54 [2: * [2: * ] #H @H ]
    55 * [2: #H cases (orb_Prop_true … H) -H ] #H
    56 @IH
    57 [ %1 cases init_val normalize nodelta #init_map #off
    58   >(proj1 ?? (eqb_true ???) H) @mem_set_add_id
    59 | %2{H}
    60 | %1 cases init_val in H; normalize nodelta #init_map #off #H
    61   >mem_set_add @orb_Prop_r @H
    62 ]
    63 qed.
    64 
    6528definition Identifier_of_label :
    66   ∀globals.label → state_monad (ASM_universe globals) Identifier ≝
    67 λg,l,u.
     29  label → state_monad ASM_universe Identifier ≝
     30λl,u.
    6831let current ≝ current_funct … u in
    6932let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in
     
    7639  ] in
    7740〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
    78   (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
     41  (fresh_cost_label … u), id〉.
    7942
    8043definition Identifier_of_ident :
    81   ∀globals.ident → state_monad (ASM_universe globals) Identifier ≝
    82 λg,i,u.
     44  ident → state_monad ASM_universe Identifier ≝
     45λi,u.
    8346let imap ≝ ident_map … u in
    84 let 〈id, univ, imap〉 ≝
    85   match lookup … imap i with
     47let res ≝ match lookup … imap i with
    8648  [ Some id ⇒ 〈id, id_univ … u, imap〉
    8749  | None ⇒
     
    8951    〈id, univ, add … imap i id〉
    9052  ] in
     53let id ≝ \fst (\fst res) in
     54let univ ≝ \snd (\fst res) in
     55let imap ≝ \snd res in
    9156〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
    92   (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
     57  (fresh_cost_label … u), id〉.
     58
     59definition new_ASM_universe :
     60∀p : joint_program LIN.ASM_universe ≝
     61λp.
     62mk_ASM_universe (mk_universe … one)
     63  (an_identifier … one (* dummy *))
     64  (empty_map …) (empty_map …) one.
     65(*@hide_prf normalize nodelta
     66cases p -p * #vars #functs #main #cost_init
     67#i #H
     68normalize nodelta
     69letin init_val ≝ (〈empty_map SymbolTag Identifier, mk_universe ASMTag one〉)
     70cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
     71[ %2{H} ] -H
     72lapply i -i lapply init_val -init_val
     73whd in match prog_var_names; normalize nodelta
     74elim vars -vars
     75[2: ** #id #r #v #tl #IH ] #init_val #i
     76[2: * [2: * ] #H @H ]
     77* [2: #H cases (orb_Prop_true … H) -H ] #H
     78@IH
     79[ %1 cases init_val normalize nodelta #init_map #off
     80  >(proj1 ?? (eqb_true ???) H) @pair_elim #lft #rgt #_ @mem_set_add_id
     81| %2{H}
     82| %1 cases init_val in H; normalize nodelta #init_map #off #H
     83  @pair_elim #lft #rgt #_
     84  >mem_set_add @orb_Prop_r @H
     85]
     86qed.
     87*)
    9388
    9489definition start_funct_translation :
    9590  ∀globals.(ident × (joint_function LIN globals)) →
    96     state_monad (ASM_universe globals) unit ≝
     91    state_monad ASM_universe unit ≝
    9792  λg,id_f,u.
    9893    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
    99       (address_map … u) (globals_are_in … u) (fresh_cost_label … u), it〉.
    100 
    101 definition address_of_ident :
    102   ∀globals,i.i ∈ globals → state_monad (ASM_universe globals) [[ data16 ]] ≝
    103 λglobals,i,prf,u.
    104 〈u, DATA16 (lookup_safe … (globals_are_in … u … prf))〉. @I qed.
     94      (fresh_cost_label … u), it〉.
    10595
    10696definition ASM_fresh :
    107   ∀globals.state_monad (ASM_universe globals) Identifier ≝
    108 λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
     97  state_monad ASM_universe Identifier ≝
     98λu.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
    10999〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
    110   (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
     100  (fresh_cost_label … u), id〉.
    111101
    112102definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     
    161151(* TODO: check and change to free bit *)
    162152definition asm_other_bit ≝ BIT_ADDR (zero_byte).
     153definition one_word : Word ≝ bv_zero 15 @@ [[ true ]].
    163154
    164155definition translate_statements :
    165156  ∀globals.
    166157  joint_statement LIN globals →
    167   state_monad (ASM_universe globals) pseudo_instruction ≝
     158  state_monad ASM_universe pseudo_instruction ≝
    168159  λglobals,statement.
    169160  match statement with
     
    188179          | LOW_ADDRESS lbl ⇒
    189180            ! lbl' ← Identifier_of_label … lbl ;
    190             return MovSuccessor (register_address RegisterA) LOW lbl'
     181            return Mov (inr ?? 〈register_address RegisterA, LOW〉) lbl' one_word
    191182          | HIGH_ADDRESS lbl ⇒
    192183            ! lbl' ← Identifier_of_label … lbl ;
    193             return MovSuccessor (register_address RegisterA) HIGH lbl'
     184            return Mov (inr ?? 〈register_address RegisterA, HIGH〉) lbl' one_word
    194185          ]
    195186        | COMMENT comment ⇒ return Comment comment
     
    253244        | LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    254245        | STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    255         | ADDRESS addr proof _ _ ⇒
    256           ! addr' ← address_of_ident … proof ;
    257           return Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, addr'〉)))))
     246        | ADDRESS id proof _ _ ⇒
     247          ! Id ← Identifier_of_ident … id ;
     248          return (Mov (inl ?? DPTR) Id (bv_zero ?))
    258249        | SET_CARRY ⇒
    259250          return Instruction (SETB ? CARRY)
     
    312303          return Call (toASM_ident ? id')
    313304        | inr _ ⇒
    314           return Instruction (JMP … INDIRECT_DPTR)
     305          return Instruction (JMP … ACC_DPTR)
    315306        ]
    316307      | COST_LABEL lbl ⇒
     
    336327  match \fst statement with
    337328  [ Some lbl ⇒
    338     ! lbl' ← Identifier_of_label globals lbl ;
     329    ! lbl' ← Identifier_of_label lbl ;
    339330    return 〈Some ? lbl', stmt〉
    340331  | None ⇒
     
    371362{ virtual_dptr : Z
    372363; actual_dptr : Z
    373 ; built : list labelled_instruction
     364; built_code : list (list labelled_instruction)
     365; built_preamble : list (Identifier × Word)
    374366}.
    375367
    376 definition store_byte : Byte → init_mutable → init_mutable ≝
     368definition store_byte_or_Identifier :
     369  (Byte ⊎ (word_side × Identifier)) → init_mutable → init_mutable ≝
    377370λby,mut.
    378371match mut with
    379 [ mk_init_mutable virt act acc
     372[ mk_init_mutable virt act acc1 acc2
    380373  let off ≝ virt - act in
    381374  let pre ≝
     
    384377    else [ 〈None ?, Instruction (MOV ? (inl … (inl … (inr …
    385378        〈DPTR, DATA16 (bitvector_of_Z … virt)〉))))〉 ] in
     379  let post ≝ match by with
     380    [ inl by ⇒
     381      〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ?
     382                               〈ACC_A, DATA by〉))))))〉
     383    | inr si_id ⇒
     384      〈None ?, Mov (inr ?? 〈ACC_A, \fst si_id〉) (\snd si_id) (bv_zero ?)〉
     385    ] in
    386386  mk_init_mutable (Zsucc virt) virt
    387     (pre @
    388      [ 〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ?
    389                              〈ACC_A, DATA by〉))))))〉 ;
    390        〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ])
     387    ((pre @
     388      [ post ;
     389       〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ]) ::
     390     acc1)
     391    acc2 
    391392]. @I qed.
    392393
     394
    393395definition do_store_init_data :
    394   ∀globals.ASM_universe globals → init_data → init_mutable → init_mutable ≝
    395 λglobals,u,data.
     396  init_data → state_monad ASM_universe init_mutable →
     397  state_monad ASM_universe init_mutable ≝
     398λdata,m_mut.
     399! mut ← m_mut ;
     400let store_byte ≝ λby.store_byte_or_Identifier (inl … by) in
     401let store_Identifier ≝ λside,id.store_byte_or_Identifier (inr … 〈side, id〉) in
    396402match data with
    397403[ Init_int8 n ⇒
    398   store_byte n
     404  return store_byte n mut
    399405| Init_int16 n ⇒
    400406  let 〈by0, by1〉 ≝ vsplit ? 8 8 n in
    401   store_byte by1 ∘ store_byte by0
     407  return store_byte by1 (store_byte by0 mut)
    402408| Init_int32 n ⇒
    403409  let 〈by0, n〉 ≝ vsplit ? 8 24 n in
    404410  let 〈by1, n〉 ≝ vsplit ? 8 16 n in
    405411  let 〈by2, by3〉 ≝ vsplit ? 8 8 n in
    406   store_byte by3 ∘ store_byte by2 ∘ store_byte by1 ∘ store_byte by0
     412  return store_byte by3 (store_byte by2 (store_byte by1 (store_byte by0 mut)))
    407413| Init_addrof symb ofs ⇒
    408   let addr : Word ≝
    409     match lookup … (address_map … u) symb with
    410     [ Some x ⇒ bitvector_of_Z ? (Z_of_unsigned_bitvector … x + ofs)
    411     | None ⇒ bv_zero ?
    412     ] in
    413   let 〈by1, by0〉 ≝ vsplit ? 8 8 addr in
    414   store_byte by1 ∘ store_byte by0
     414  ! id ← Identifier_of_ident … symb ;
     415  return store_Identifier HIGH id (store_Identifier LOW id mut)
    415416| Init_space n ⇒
    416   λmut.mk_init_mutable (n + virtual_dptr mut) (actual_dptr mut) (built mut)
     417  return mk_init_mutable (n + virtual_dptr mut) (actual_dptr mut)
     418    (built_code mut) (built_preamble mut)
    417419| Init_null ⇒
    418420  let z ≝ bv_zero ? in
    419   store_byte z ∘ store_byte z
     421  return store_byte z (store_byte z mut)
    420422].
    421423
    422 definition do_store_init_data_list :
    423   ∀globals.ASM_universe globals → Z → list init_data → list labelled_instruction ≝
    424   λglobals,u,start_dptr,data.
    425   let init ≝ mk_init_mutable start_dptr OZ [ ] in
    426   built (foldr … (do_store_init_data … u) init data).
    427 
    428 definition translate_premain : ∀p : lin_program.
    429   Identifier → state_monad (ASM_universe (prog_var_names … p)) (list labelled_instruction) ≝
     424definition do_store_global :
     425  (ident × region × (list init_data)) →
     426    state_monad ASM_universe init_mutable →
     427    state_monad ASM_universe init_mutable ≝
     428  λid_reg_data,m_mut.! mut ← m_mut ;
     429  let 〈id, reg, data〉 ≝ id_reg_data in
     430  ! Id ← Identifier_of_ident … id ;
     431  let mut ≝ mk_init_mutable (virtual_dptr mut) (actual_dptr mut) (built_code mut)
     432      (〈Id, bitvector_of_Z … (virtual_dptr mut)〉 :: built_preamble mut) in
     433  foldr … do_store_init_data (return mut) data.
     434
     435let rec reversed_flatten_aux A acc (l : list (list A)) on l : list A ≝
     436match l with
     437[ nil ⇒ acc
     438| cons hd tl ⇒ reversed_flatten_aux … (hd @ acc) tl
     439].
     440
     441definition translate_premain : ∀p : lin_program.Identifier →
     442  state_monad ASM_universe (list labelled_instruction × (list (Identifier × Word))) ≝
    430443  λp : lin_program.λexit_label.
    431444  ! main ← Identifier_of_ident … (prog_main … p) ;
     
    433446  (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
    434447  let start_sp : Z ≝ -(S (globals_stacksize … p)) in
     448  let mut ≝ mk_init_mutable start_sp OZ [ ] [ ] in
     449  ! globals_init ← foldr … do_store_global (return mut) (prog_vars … p) ;
    435450  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
    436   let data ≝ flatten ? (map ?? (λx.\snd x) (prog_vars … p)) in
    437451  let init_isp ≝
    438452    (* initial stack pointer set to 2Fh in order to use addressable bits *)
     
    443457  let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in
    444458  let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in
    445   return ([
     459  return [
    446460    〈None ?, Cost (init_cost_label … p)〉 ;
    447461    (* initialize the internal stack pointer past the addressable bits *)
     
    456470    (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
    457471      〈reg_sph, DATA sph〉))))))〉 ] @
    458   do_store_init_data_list ? u start_sp data @
     472  reversed_flatten_aux … [ ] (built_code globals_init) @
    459473  [ 〈None ?, Call main〉 ;
    460474    〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ;
    461     〈None ?, Jmp exit_label〉]). @I qed.
     475    〈None ?, Jmp exit_label〉], built_preamble globals_init〉. @I qed.
    462476
    463477definition get_symboltable :
    464   ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝
    465   λglobals,u.
     478  state_monad ASM_universe (list (Identifier × ident)) ≝
     479  λu.
    466480  let imap ≝ ident_map … u in
    467481  let f ≝ λiold,inew.cons ? 〈inew, iold〉 in
     
    479493     ! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
    480494     ! symboltable ← get_symboltable … ;
    481      ! init ← translate_premain p exit_label;
     495     ! 〈init, preamble〉 ← translate_premain p exit_label;
    482496     return
    483497       (
     
    487501        (* atm no data identifier is used in the code, so preamble must be empty *)
    488502        return
    489           (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))).
     503          (mk_pseudo_assembly_program preamble code code_ok symboltable exit_label ? ?))).
    490504cases daemon
    491505qed.
Note: See TracChangeset for help on using the changeset viewer.