Changeset 833


Ignore:
Timestamp:
May 24, 2011, 11:19:53 PM (8 years ago)
Author:
sacerdot
Message:

Bug fixed to make the file compile.
But the type of the assembly function is no more right.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r832 r833  
    636636  ].
    637637
    638 check lookup.
    639 
    640638definition assembly ≝
    641639  λp.
     
    653651        let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
    654652        let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
    655         let to_flatten ≝ map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels x) instr_list in
    656         (*
    657           foldr ? ? (λx. λy.
     653        let to_flatten ≝
     654         map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x)) instr_list
     655        in
     656         foldr ? ? (λx. λy.
    658657            match y with
    659658            [ None ⇒ None ?
     
    663662              | Some x ⇒ Some ? (x @ lst)
    664663              ]
    665             ]) (Some ? [ ]) to_flatten *) ?
    666       ]
    667     ].
    668    
    669 (*
    670         if  then (* 65536 *)
    671           None ?
    672         else
    673           let flat_list ≝ flatten ? (
    674             map ? ? (
    675               assembly_1_pseudoinstruction (
    676                 λx. lookup ? ? x labels (zero ?))
    677                   (λx. lookup ? ? x datalabels (zero ?))
    678                   (address_of labels)) instr_list) in
    679           Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉
    680 *)
    681 
    682 (*
    683   [2,3,4,5,6:
    684     normalize; %;
    685   | whd in ⊢ (? (? ? ? %));
    686       cases (split bool 8 8 (lookup Word 16 trgt labels (zero 16)))
    687       # high
    688       # low
    689       whd in ⊢ (? (? ? ? %))
    690       cases (eq_bv 8 high (zero 8))
    691       [ normalize
    692         %
    693       | elim not_implemented;
    694       ]
    695   ]
    696 qed. *)
    697 
    698 
     664            ]) (Some ? [ ]) to_flatten ]].
    699665
    700666definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
  • src/ASM/AssemblyProof.ma

    r832 r833  
    7979           (clock … ps)) ].
    8080
     81(* RUSSEL **)
     82
     83include "basics/jmeq.ma".
     84
     85definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
     86definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
     87
     88coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
     89coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
     90
     91(* END RUSSELL **)
     92
     93definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
     94 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
     95
     96  λticks_of.
     97  λs.
     98  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
     99  let ticks ≝ ticks_of (program_counter ? s) in
     100  let s ≝ set_clock ? s (clock ? s + ticks) in
     101  let s ≝ set_program_counter ? s pc in
     102  let s ≝
     103    match instr with
     104    [ Instruction instr ⇒
     105       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
     106    | Comment cmt ⇒ Some PseudoStatus s
     107    | Cost cst ⇒ Some PseudoStatus s
     108    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
     109    | Call call ⇒
     110      let a ≝ address_of_word_labels s call in
     111      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     112      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     113      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     114      let s ≝ write_at_stack_pointer ? s pc_bl in
     115      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     116      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     117      let s ≝ write_at_stack_pointer ? s pc_bu in
     118        Some PseudoStatus (set_program_counter ? s a)
     119    | Mov dptr ident ⇒
     120       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
     121    ]
     122  in
     123    s.
     124 [
     125 |2,3,4: %
     126 | whd % 
     127
     128  λticks_of.
     129  λs.
     130  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
     131  let ticks ≝ ticks_of (program_counter ? s) in
     132  let s ≝ set_clock ? s (clock ? s + ticks) in
     133  let s ≝ set_program_counter ? s pc in
     134  let s ≝
     135    match instr with
     136    [ Instruction instr ⇒
     137       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
     138    | Comment cmt ⇒ Some PseudoStatus s
     139    | Cost cst ⇒ Some PseudoStatus s
     140    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
     141    | Call call ⇒
     142      let a ≝ address_of_word_labels s call in
     143      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     144      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     145      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     146      let s ≝ write_at_stack_pointer ? s pc_bl in
     147      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     148      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     149      let s ≝ write_at_stack_pointer ? s pc_bu in
     150        Some PseudoStatus (set_program_counter ? s a)
     151    | Mov dptr ident ⇒
     152       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
     153    ]
     154  in
     155    s.
     156  [2: % ]
     157  normalize
     158  @ I
     159qed.
     160
     161
     162
     163definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
     164 {{ ps':PseudoStatus | code_memory … ps = code_memory … ps' }
     165
     166  λticks_of.
     167  λs.
     168  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
     169  let ticks ≝ ticks_of (program_counter ? s) in
     170  let s ≝ set_clock ? s (clock ? s + ticks) in
     171  let s ≝ set_program_counter ? s pc in
     172  let s ≝
     173    match instr with
     174    [ Instruction instr ⇒
     175       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
     176    | Comment cmt ⇒ Some PseudoStatus s
     177    | Cost cst ⇒ Some PseudoStatus s
     178    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
     179    | Call call ⇒
     180      let a ≝ address_of_word_labels s call in
     181      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     182      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     183      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     184      let s ≝ write_at_stack_pointer ? s pc_bl in
     185      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     186      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     187      let s ≝ write_at_stack_pointer ? s pc_bu in
     188        Some PseudoStatus (set_program_counter ? s a)
     189    | Mov dptr ident ⇒
     190       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
     191    ]
     192  in
     193    s.
     194  [2: % ]
     195  normalize
     196  @ I
     197qed.
     198
     199
    81200
    82201lemma execute_code_memory_unchanged:
     
    94213       cases (split ????) #z1 #z2 %
    95214     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
     215       [ #x1 whd in ⊢ (??? (??%))
    96216     | *: cases not_implemented
    97217     ]
Note: See TracChangeset for help on using the changeset viewer.