Changeset 2999 for src/ASM/ASM.ma


Ignore:
Timestamp:
Mar 28, 2013, 12:47:55 PM (7 years ago)
Author:
sacerdot
Message:

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2767 r2999  
    11561156}.
    11571157
    1158 definition object_code ≝ list Byte.
     1158definition object_code ≝ list Byte.
     1159
     1160include alias "ASM/BitVectorTrie.ma".
     1161include alias "ASM/Arithmetic.ma".
     1162
     1163definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
     1164  λpmem: BitVectorTrie Byte 16.
     1165  λpc: Word.
     1166    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
     1167
     1168definition load_code_memory0:
     1169 ∀program: object_code. Σres: BitVectorTrie Byte 16.
     1170  let program_size ≝ |program| in
     1171   program_size ≤ 2^16 →
     1172    ∀pc. ∀pc_ok: pc < program_size.
     1173     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
     1174
     1175 λprogram. \snd
     1176  (foldl_strong ?
     1177   (λprefix.
     1178     Σres: nat × (BitVectorTrie Byte 16).
     1179      let 〈i,mem〉 ≝ res in
     1180      i = |prefix| ∧
     1181      (i ≤ 2^16 →
     1182        ∀pc. ∀pc_ok: pc < |prefix|.
     1183         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
     1184   program
     1185   (λprefix,v,tl,prf,i_mem.
     1186     let 〈i,mem〉 ≝ i_mem in
     1187      〈S i,insert … (bitvector_of_nat … i) v mem〉)
     1188  〈0,Stub Byte 16〉).
     1189[3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
     1190| % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
     1191| cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
     1192  [ >length_append >H1 normalize //
     1193  | #LE #pc #pc_ok
     1194    cases (le_to_or_lt_eq … pc_ok)
     1195    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
     1196      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
     1197      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
     1198      <H1 <plus_n_O whd in ⊢ (???%); //
     1199    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
     1200      >H2 [2: @(transitive_le … LE) //]
     1201      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
     1202      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
     1203      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
     1204      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
     1205qed.
     1206
     1207definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
     1208 λprogram.load_code_memory0 program.
     1209
     1210lemma load_code_memory_ok:
     1211 ∀program: object_code.
     1212  let program_size ≝ |program| in
     1213   program_size ≤ 2^16 →
     1214    ∀pc. ∀pc_ok: pc < program_size.
     1215     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
     1216whd in match load_code_memory; normalize nodelta #program @pi2
     1217qed.
     1218
     1219
    11591220definition costlabel_map ≝ BitVectorTrie costlabel 16. (* XXX *)
    11601221definition symboltable_type ≝ BitVectorTrie ident 16.  (* XXX *)
    11611222record labelled_object_code : Type[0] ≝
    11621223{ oc : object_code
     1224; cm: BitVectorTrie Byte 16
     1225; cm_def: cm = load_code_memory oc
    11631226; costlabels : costlabel_map
    11641227; symboltable : symboltable_type
     
    11681231  partial_injection … (λpc.lookup_opt … pc costlabels)
    11691232}.
    1170 
    1171 
    1172 
Note: See TracChangeset for help on using the changeset viewer.