Changeset 2756


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
Files:
6 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))).
  • src/common/Measurable.ma

    r2727 r2756  
    2424definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝
    2525λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
    26 
    27 (* For intensional_event; should separate out definition *)
    28 include "common/StatusSimulation.ma".
    2926
    3027definition intensional_event_of_event : event → list intensional_event ≝
  • src/common/StatusSimulation.ma

    r2755 r2756  
    8181    ∀st1,st1',st2.as_execute S1 st1 st1' →
    8282    sim_status_rel st1 st2 →
    83     match as_classify … st1 with
    84     [ None ⇒ True
    85     | Some cl ⇒
    86       match cl with
     83      match as_classify … st1 with
    8784      [ cl_call ⇒ ∀prf.
    8885        (*
     
    170167        sim_status_rel st1' st2' ∧
    171168        label_rel … st1' st2'
    172       ]
    173169    ].
    174170
     
    514510  lapply (sim_execute … H st1_R_st2)
    515511  (* without try it fails... why? *)
    516   try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); normalize nodelta
     512  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
    517513  [ #H lapply (H K) -H ] *
    518514  #st2' ** -st2 -st2'
     
    531527| (* tal_base_return *) whd
    532528  lapply (sim_execute … H st1_R_st2)
    533   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
     529  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
    534530  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    535531  ***** #ncost #J2 #K2
     
    540536| (* tal_base_call *) whd
    541537  lapply (sim_execute … H st1_R_st2)
    542   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
     538  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
    543539  #H elim (H G) -H
    544540  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     
    569565| (* tal_base_tailcall *) whd
    570566  lapply (sim_execute … H st1_R_st2)
    571   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
     567  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
    572568  #H elim (H G) -H
    573569  * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     
    583579| (* tal_step_call *)
    584580  lapply (sim_execute … H st1_R_st2)
    585   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?);
     581  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
    586582  #H elim (H G) -H
    587583  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
     
    632628| (* step_default *)
    633629  lapply (sim_execute … H st1_R_st2)
    634   >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
     630  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
    635631  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
    636632  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
     
    873869  [1,2: (* other/jump *)
    874870    lapply (sim_execute … ex G')
    875     try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); normalize nodelta
     871    try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
    876872    [ #H lapply (H ncost_st1') -H ] *
    877873    #st2' *#taaf ** #ncost #G'' #H''
     
    904900  |3: (* tailcall *)
    905901    lapply (sim_execute … ex G')
    906     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
     902    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
    907903    * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
    908904    * #taa2 * #taa2' ** #ex' #G'' #H''
     
    926922  |4: (* ret *)
    927923    lapply (sim_execute … ex G')
    928     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
     924    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
    929925    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
    930926    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
     
    948944  |5: (* call *)
    949945    lapply (sim_execute … ex G')
    950     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
     946    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
    951947    * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
    952948    * #taa2 * #taa2' ** #ex' #G'' #H''
  • src/common/StructuredTraces.ma

    r2755 r2756  
    1  include "basics/types.ma".
    21include "basics/bool.ma".
    32include "basics/jmeq.ma".
     
    54include "utilities/option.ma".
    65include "basics/lists/listb.ma".
    7 include "ASM/Util.ma".
    86include "common/IO.ma".
    97include "utilities/hide.ma".
     8include "ASM/Util.ma".
    109
    1110inductive status_class: Type[0] ≝
     
    1918  { as_status :> Type[0]
    2019  ; as_eval : as_status → IO io_out io_in as_status
     20  ; as_init : res as_status
    2121  ; as_pc : DeqSet
    2222  ; as_pc_of : as_status → as_pc
    23   ; as_classify : as_status → option status_class
     23  ; as_classify : as_status → status_class
    2424  ; as_label_of_pc : as_pc → option costlabel
    25   ; as_after_return : (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
     25  ; as_after_return : (Σs:as_status. as_classify s = cl_call) → as_status → Prop
    2626  ; as_result: as_status → option int
    27   ; as_call_ident : (Σs:as_status.as_classify s = Some ? cl_call) → ident
    28   ; as_tailcall_ident : (Σs:as_status.as_classify s = Some ? cl_tailcall) → ident
     27  ; as_call_ident : (Σs:as_status.as_classify s = cl_call) → ident
     28  ; as_tailcall_ident : (Σs:as_status.as_classify s = cl_tailcall) → ident
    2929  }.
    3030
    31 definition as_classifier ≝ λS,s,cl.as_classify S s = Some ? cl.
     31definition as_classifier ≝ λS,s,cl.as_classify S s = cl.
    3232definition as_call ≝ λS,s,f.as_call_ident S s = f.
    3333definition as_final ≝ λS,s.as_result S s ≠ None ?.
Note: See TracChangeset for help on using the changeset viewer.