Changeset 2710 for src/ASM


Ignore:
Timestamp:
Feb 22, 2013, 7:20:24 PM (7 years ago)
Author:
sacerdot
Message:

ASMCosts.ma repaired

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2679 r2710  
    637637    change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
    638638    cases (current_instruction ??) in classifier_assm;
    639     [8:
    640       #preinstruction cases preinstruction
    641     ]
     639    [7: #preinstruction cases preinstruction ]
    642640    try(#addr1 #addr2 #absurd destruct(absurd))
    643641    try(#addr #absurd destruct(absurd))
     
    726724          | CJNE src_trgt relative ⇒ λinstr. ticks
    727725          | DJNZ src_trgt relative ⇒ λinstr. ticks
     726          | JMP   addr             ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
     727              ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
    728728          | _                      ⇒ λinstr.
    729729              ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     
    742742          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    743743            ticks + block_cost' code_memory' jump_target program_size' cost_labels false
    744         | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    745             ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
    746744        | MOVC  src trgt ⇒ λinstr.
    747745            ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     
    782780    change with (if to_continue then ? else (0 = 0))
    783781    >p normalize nodelta %
    784   |5,6:
     782  |6,7:
    785783    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    786784    @(trace_compute_paid_trace_cl_return … program_size' … FETCH … the_trace program_counter_refl)
    787785    destruct %
    788   |42,46,47:
     786  |4,46,47:
    789787    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    790788    cases(block_cost' ?????) -block_cost'
     
    797795    whd in match (program_counter_after_other ??); normalize nodelta destruct
    798796    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
    799   |24,25,26,27,28,29,30,31,32:
     797  |25,26,27,28,29,30,31,32,33:
    800798    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    801799    @(trace_compute_paid_trace_cl_jump … first_time_around program_size' … FETCH … the_trace program_counter_refl)
    802800    destruct %
     801  |4,33:
    803802  |*:
    804803    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
     
    832831  @hyp @tal_pc_list_length_leq_total_program_size try assumption
    833832qed.
    834 
  • src/ASM/Status.ma

    r2316 r2710  
    10891089      let 〈carry, sum〉 ≝ half_add … addr size in
    10901090        〈add ? ? datalabels name addr, sum〉)
    1091           〈empty_map …, zero 16〉 (\snd the_preamble)).
     1091          〈empty_map …, zero 16〉 the_preamble).
  • src/ASM/WellLabeled.ma

    r2032 r2710  
    7575        | _ ⇒ λabsurd. ⊥
    7676        ] (subaddressing_modein … sjmp)
    77       | JMP jmp ⇒ True (* XXX: check is dynamic, as we can only jump to functions *)
    7877      | MOVC _ _ ⇒ True
    7978      | RealInstruction instruction ⇒
Note: See TracChangeset for help on using the changeset viewer.