Changeset 2756 for src/ASM


Ignore:
Timestamp:
Mar 1, 2013, 1:05:21 PM (7 years ago)
Author:
sacerdot
Message:

WARNING: this commit breaks things, sorry, Paolo is going to fix compiler.ma
in a minute...

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2710 r2756  
    1414    mk_abstract_status
    1515      (Status code_memory)
    16       (λs,s'. (execute_1 … s) = s')
     16      (λs. return (execute_1 … s))
     17      ?
    1718      word_deqset
    1819      (program_counter …)
    19       (λs. Some ? (ASM_classify … s))
     20      (ASM_classify …)
    2021      (λpc.lookup_opt … pc cost_labels)
    2122      (next_instruction_properly_relates_program_counters code_memory)
     
    162163          program_counter_after_other pc instruction.
    163164  #code_memory #cost_labels #start_status #classify_assm
    164   change with (Some ? (ASM_classify0 ?) = ?) in classify_assm;
     165  change with (ASM_classify0 ? = ?) in classify_assm;
    165166  destruct (classify_assm)
    166167  @execute_1_and_program_counter_after_other_in_lockstep0 assumption.
  • src/ASM/Interpret.ma

    r2705 r2756  
    6464qed.
    6565
     66include alias "ASM/Arithmetic.ma".
    6667include alias "arithmetics/nat.ma".
    6768include alias "ASM/BitVectorTrie.ma".
  • src/ASM/Interpret2.ma

    r2754 r2756  
    1 include "ASM/Interpret.ma".
    2 include "common/SmallstepExec.ma".
    3 include "common/IO.ma".
     1include "ASM/ASMCosts.ma".
     2include "common/Measurable.ma".
    43
     4(*
    55(* Transition system on the assembly code *)
    66
     
    5858definition ASM_fullexec: fullexec io_out io_in ≝
    5959 mk_fullexec ??? exec make_global ?(*(λp.OK … (load (\fst p) (initialise_status … (Stub ??))))*).
     60*)
    6061
    61 axiom ASM_fullexec: fullexec io_out io_in.
     62definition mk_trans_system_of_abstract_status:
     63 abstract_status → trans_system io_out io_in
     64
     65 λS.
     66  mk_trans_system ?? unit (λ_.as_status S) (λ_.as_result S)
     67   (λ_.λstatus.
     68     let tr ≝
     69      match as_label … status with
     70      [ Some cst ⇒ Echarge cst
     71      | None ⇒ E0 ] in
     72     ! status' ← as_eval … status ;
     73     return 〈 tr, status' 〉).
     74
     75definition mk_fullexec_of_abstract_status: abstract_status → fullexec io_out io_in
     76≝ λS.
     77   mk_fullexec ?? unit (mk_trans_system_of_abstract_status S) (λ_.it)
     78    (λ_.as_init S).
     79
     80definition mk_preclassified_system_of_abstract_status:
     81 abstract_status → preclassified_system
     82≝ λS.
     83   mk_preclassified_system
     84    (mk_fullexec_of_abstract_status S) (λ_.λst. ¬(is_none … (as_label … st)))
     85    (λ_.as_classify S)
     86    (λ_.λst,prf. as_call_ident S «st,?»).
     87 @hide_prf cases (as_classify ??) in prf; normalize // *
     88qed.
     89
     90(*
     91definition OC_transition_system: trans_system io_out io_in ≝
     92 mk_trans_system ?? OC_global OC_status ?
     93  execute_1_instruction.
     94
     95definition OC_global ≝ BitVectorTrie Byte 16 × costlabel_map.
     96
     97definition OC_status ≝ λgl:OC_global. Status (\fst gl).
     98
     99definition execute_1_instruction:
     100 ∀g:OC_global. OC_status g → IO io_out io_in (trace × OC_status g) ≝
     101λg. let 〈cm,costs〉 ≝ g in λs.
     102 let 〈instr, pc,ticks〉 ≝ fetch cm (program_counter … s) in
     103 let s' ≝ execute_1 s in
     104 match lookup_opt … pc costs with
     105 [ None ⇒ ret … 〈E0, s'〉
     106 | Some cst ⇒ ret … 〈Echarge cst, s'〉 ].
     107
     108definition OC_transition_system: trans_system io_out io_in ≝
     109 mk_trans_system ?? OC_global OC_status ?
     110  execute_1_instruction.
     111
     112definition OC_fullexec: fullexec io_out io_in ≝
     113 mk_fullexec ??
     114  labelled_object_code*)
     115 
     116
     117definition OC_preclassified_system ≝
     118 λc:labelled_object_code.
     119  mk_preclassified_system_of_abstract_status (ASM_abstract_status (\fst c) (\fst (\snd c))).
Note: See TracChangeset for help on using the changeset viewer.