Changeset 2999 for src/ASM/ASMCosts.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/ASMCosts.ma

    r2993 r2999  
    3737definition OC_abstract_status: labelled_object_code → abstract_status ≝
    3838 λprog.
    39   let code_memory ≝ load_code_memory (oc prog) in
    4039    mk_abstract_status
    41       (Status code_memory)
     40      (Status (cm prog))
    4241      (λs1,s2. execute_1 … s1 = s2)
    4342      word_deqset
    44       (program_counter … code_memory)
    45       (OC_classify code_memory)
     43      (program_counter …)
     44      (OC_classify )
    4645      (λpc.lookup_opt … pc (costlabels prog))
    47       (next_instruction_properly_relates_program_counters code_memory)
    48       (λst. as_result_of_finaladdr … code_memory … st (final_pc prog))
    49       (OC_as_call_ident prog code_memory)
     46      (next_instruction_properly_relates_program_counters )
     47      (λst. as_result_of_finaladdr … st (final_pc prog))
     48      (OC_as_call_ident prog )
    5049      ?.
    5150 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
     
    5554definition trace_any_label_length ≝
    5655  λprog: labelled_object_code.
    57   let code_memory ≝ load_code_memory (oc prog) in
    5856  λtrace_ends_flag: trace_ends_with_ret.
    59   λstart_status: Status code_memory.
    60   λfinal_status: Status code_memory.
     57  λstart_status: Status (cm prog).
     58  λfinal_status: Status (cm prog).
    6159  λthe_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    6260    as_trace_any_label_length' … the_trace.
     
    178176lemma execute_1_and_program_counter_after_other_in_lockstep:
    179177  ∀prog: labelled_object_code.
    180   let code_memory ≝ load_code_memory (oc prog) in
    181   ∀start_status: Status code_memory.
     178  ∀start_status: Status (cm prog).
    182179    as_classifier (OC_abstract_status prog) start_status cl_other →
    183       let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
     180      let 〈instruction, pc, ticks〉 ≝ fetch (cm prog) (program_counter … start_status) in
    184181        program_counter ? ? (execute_1 … start_status) =
    185182          program_counter_after_other pc instruction.
     
    192189lemma sublist_tal_pc_list_all_program_counter_list:
    193190  ∀prog: labelled_object_code.
    194   let code_memory ≝ load_code_memory (oc prog) in
    195   ∀start, final: Status code_memory.
     191  ∀start, final: Status (cm prog).
    196192  ∀trace_ends_flag.
    197193  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
     
    205201corollary tal_pc_list_length_leq_total_program_size:
    206202  ∀prog: labelled_object_code.
    207   let code_memory ≝ load_code_memory (oc prog) in
    208   ∀start, final: Status code_memory.
     203  ∀start, final: Status (cm prog).
    209204  ∀trace_ends_flag.
    210205  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
     
    225220let rec compute_paid_trace_any_label
    226221  (prog: labelled_object_code) (trace_ends_flag: trace_ends_with_ret)
    227    (start_status: Status (load_code_memory (oc prog)))
    228    (final_status: Status (load_code_memory (oc prog)))
     222   (start_status: Status (cm prog))
     223   (final_status: Status (cm prog))
    229224        (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    230225       on the_trace: nat ≝
     
    250245definition compute_paid_trace_label_label ≝
    251246  λprog: labelled_object_code.
    252   let code_memory ≝ load_code_memory (oc prog) in
    253247  λtrace_ends_flag: trace_ends_with_ret.
    254   λstart_status: Status code_memory.
    255   λfinal_status: Status code_memory.
     248  λstart_status: Status (cm prog).
     249  λfinal_status: Status (cm prog).
    256250  λthe_trace: (trace_label_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
    257251  match the_trace with
     
    262256lemma trace_compute_paid_trace_cl_other:
    263257  ∀prog : labelled_object_code.
    264   let code_memory' ≝ load_code_memory (oc prog) in
    265258  ∀program_counter' : Word.
    266259  ∀program_size' : ℕ.
     
    268261  ∀instruction : instruction.
    269262  ∀program_counter'' : Word.
    270   ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
     263  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
    271264  let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
    272   ∀start_status : (Status code_memory').
    273   ∀final_status : (Status code_memory').
     265  ∀start_status : (Status (cm prog)).
     266  ∀final_status : (Status (cm prog)).
    274267  ∀trace_ends_flag : trace_ends_with_ret.
    275268  ∀the_trace : (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
     
    283276         ] 
    284277    then
    285       ∀start_status0:Status code_memory'.
    286       ∀final_status0:Status code_memory'.
     278      ∀start_status0:Status (cm prog).
     279      ∀final_status0:Status (cm prog).
    287280      ∀trace_ends_flag0:trace_ends_with_ret.
    288281      ∀the_trace0:trace_any_label (OC_abstract_status prog) trace_ends_flag0 start_status0 final_status0.
     
    341334          end_flag trace_any_label ? ?) try (>rewrite_assm %)
    342335        whd in match (current_instruction_cost … status_pre);
    343         cut(ticks = \snd (fetch (load_code_memory (oc prog))
    344            (program_counter … status_pre)))
     336        cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre)))
    345337        [1,3:
    346338          <FETCH %
     
    384376          #Some_lookup_opt_assm <Some_lookup_opt_assm
    385377          normalize nodelta #new_recursive_assm >new_recursive_assm
    386           cut(ticks = \snd (fetch (load_code_memory (oc prog))
    387              (program_counter … status_start)))
     378          cut(ticks = \snd (fetch (cm prog) (program_counter … status_start)))
    388379          [1:
    389380            <FETCH %
     
    420411lemma trace_compute_paid_trace_cl_jump:
    421412  ∀prog: labelled_object_code.
    422   let code_memory' ≝ load_code_memory (oc prog) in
    423413  ∀program_counter': Word.
    424414  ∀first_time_around: bool.
     
    427417  ∀instruction: instruction.
    428418  ∀program_counter'': Word.
    429   ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
    430   ∀start_status: (Status code_memory').
    431   ∀final_status: (Status code_memory').
     419  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch (cm prog) program_counter'.
     420  ∀start_status: (Status (cm prog)).
     421  ∀final_status: (Status (cm prog)).
    432422  ∀trace_ends_flag: trace_ends_with_ret.
    433423  ∀the_trace: (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
     
    436426    ticks
    437427     =compute_paid_trace_any_label … the_trace.
    438   #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #first_time_around
     428  #prog #program_counter' #first_time_around
    439429  #program_size' #ticks #instruction #program_counter'' #FETCH
    440430  #start_status #final_status
     
    479469lemma trace_compute_paid_trace_cl_call:
    480470  ∀prog: labelled_object_code.
    481   let code_memory' ≝ load_code_memory (oc prog) in
    482471  ∀program_counter' : Word.
    483472  ∀program_size' : ℕ.
     
    485474  ∀instruction : instruction.
    486475  ∀program_counter'' : Word.
    487   ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
    488   ∀start_status : (Status code_memory').
    489   ∀final_status : (Status code_memory').
     476  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
     477  ∀start_status : (Status (cm prog)).
     478  ∀final_status : (Status (cm prog)).
    490479  ∀trace_ends_flag : trace_ends_with_ret.
    491480  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    496485  .if match lookup_opt costlabel 16 program_counter'' (costlabels prog) with 
    497486      [None ⇒ true | Some _ ⇒ false] 
    498    then (∀start_status0:Status code_memory'
    499              .∀final_status0:Status code_memory'
     487   then (∀start_status0:Status (cm prog)
     488             .∀final_status0:Status (cm prog)
    500489              .∀trace_ends_flag0:trace_ends_with_ret
    501490               .∀the_trace0:trace_any_label
     
    511500   → ticks+pi1
    512501     =compute_paid_trace_any_label … the_trace).
    513   #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
     502  #prog #program_counter' #program_size'
    514503  #ticks #instruction #program_counter'' #FETCH
    515504  #start_status #final_status #trace_ends_flag
     
    555544        #program_counter_assm >program_counter_assm <Some_lookup_opt
    556545        normalize nodelta #new_recursive_assm >new_recursive_assm
    557         cut(ticks = \snd (fetch code_memory' (program_counter … status_pre_fun_call)))
     546        cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre_fun_call)))
    558547        [1:
    559548          <FETCH %
     
    618607lemma trace_compute_paid_trace_cl_return:
    619608  ∀prog: labelled_object_code.
    620   let code_memory' ≝ load_code_memory (oc prog) in
    621609  ∀program_counter' : Word.
    622610  ∀program_size' : ℕ.
     
    624612  ∀instruction : instruction.
    625613  ∀program_counter'' : Word.
    626   ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
    627   ∀start_status : (Status code_memory').
    628   ∀final_status : (Status code_memory').
     614  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
     615  ∀start_status : (Status (cm prog)).
     616  ∀final_status : (Status (cm prog)).
    629617  ∀trace_ends_flag : trace_ends_with_ret.
    630618  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    633621    ticks
    634622     =compute_paid_trace_any_label … the_trace.
    635   #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
     623  #prog #program_counter' #program_size'
    636624  #ticks #instruction #program_counter'' #FETCH
    637625  #start_status #final_status #trace_ends_flag
     
    686674lemma trace_any_label_length_leq_0_to_False:
    687675  ∀prog: labelled_object_code.
    688   let code_memory ≝ load_code_memory (oc prog) in
    689676  ∀trace_ends_flag: trace_ends_with_ret.
    690   ∀start_status: Status code_memory.
    691   ∀final_status: Status code_memory.
     677  ∀start_status: Status (cm prog).
     678  ∀final_status: Status (cm prog).
    692679  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    693680   trace_any_label_length … the_trace ≤ 0 → False.
     
    703690          Σcost_of_block: nat.
    704691          if (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) then
    705             ∀start_status,final_status: Status (load_code_memory (oc prog)).
     692            ∀start_status,final_status: Status (cm prog).
    706693            ∀trace_ends_flag.
    707694            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    711698          else
    712699            (cost_of_block = 0) ≝
    713   let code_memory' ≝ load_code_memory (oc prog) in
    714700  match program_size return λx. x = program_size → ? with
    715701  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
    716702  | S program_size' ⇒ λstep_case.
    717     let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (load_code_memory (oc prog)) program_counter' in
     703    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (cm prog) program_counter' in
    718704    let to_continue ≝
    719705      match lookup_opt … program_counter' (costlabels prog) with
     
    727713          match real_instruction return λx. x = real_instruction →
    728714          Σcost_of_block: nat.
    729             ∀start_status,final_status: Status code_memory'.
     715            ∀start_status,final_status: Status (cm prog).
    730716            ∀trace_ends_flag.
    731717            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    770756          match (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) with
    771757          [ true ⇒
    772             ∀start_status: Status code_memory'.
    773             ∀final_status: Status code_memory'.
     758            ∀start_status: Status (cm prog).
     759            ∀final_status: Status (cm prog).
    774760            ∀trace_ends_flag.
    775761            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
     
    832818    ∀program_counter': Word.
    833819      Σcost_of_block: nat.
    834         ∀start_status: Status (load_code_memory (oc prog)).
    835         ∀final_status: Status (load_code_memory (oc prog)).
     820        ∀start_status: Status (cm prog).
     821        ∀final_status: Status (cm prog).
    836822        ∀trace_ends_flag.
    837823        ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
Note: See TracChangeset for help on using the changeset viewer.