Changeset 3039 for src/ASM


Ignore:
Timestamp:
Mar 29, 2013, 5:45:14 PM (7 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/ASM
Files:
7 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))
Note: See TracChangeset for help on using the changeset viewer.