Changeset 2764 for src/ASM/Interpret2.ma


Ignore:
Timestamp:
Mar 2, 2013, 11:59:37 PM (7 years ago)
Author:
sacerdot
Message:

preclassified_system for object code

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Interpret2.ma

    r2756 r2764  
    22include "common/Measurable.ma".
    33
    4 (*
    5 (* Transition system on the assembly code *)
    6 
    7 (*CSC: waiting for Jaap's code to compile or to be splitted from Assembly.ma *)
    8 axiom policy: pseudo_assembly_program → Type[0].
    9 (*CSC: problem here: mk_policy should be allowed to fail, but mk_fullexec does
    10   not allow make_global to fail too *)
    11 axiom mk_policy: ∀p:pseudo_assembly_program. policy p.
    12 
    13 (*CSC: already implemented in AssemblyProof.ma: move elsewhere *)
    14 axiom ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat.
    15 
    16 definition pseudo_make_global: pseudo_assembly_program → Word → nat × nat ≝
    17  λp. ticks_of … (mk_policy p).
    18 
    19 (*
    20 definition execute_1_pseudo_instruction_trace:
    21  (Word → nat × nat) → PseudoStatus → IO io_out io_in (trace × PseudoStatus) ≝
    22 λticks_of,s.
    23  let 〈instr,pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory … s)) (program_counter … s) in
    24  let s ≝ execute_1_pseudo_instruction ticks_of s in
    25  match instr with
    26  [ Cost cst ⇒ ret … 〈Echarge cst, s〉
    27  | _ ⇒ ret ? 〈E0, s〉 ].
    28 
    29 axiom pseudo_is_final: (Word → nat × nat) → PseudoStatus → option int.
    30 
    31 definition pseudo_exec: trans_system io_out io_in ≝
    32  mk_trans_system … pseudo_is_final execute_1_pseudo_instruction_trace.
    33 
    34 definition pseudo_ASM_fullexec: fullexec io_out io_in ≝
    35  mk_fullexec … pseudo_exec pseudo_make_global (λp.OK … (initialise_status … p)).
    36 
    37 (* Transition system on the object code *)
    38 
    39 definition make_global: labelled_object_code → BitVectorTrie costlabel 16 ≝ \snd.
    40 
    41 definition execute_1_instruction:
    42  BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝
    43 λcosts,s.
    44  let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
    45  let 〈instr,pc〉 ≝ instr_pc in
    46  match lookup_opt … pc costs with
    47  [ None ⇒ ret … 〈E0, s〉
    48  | Some cst ⇒ ret … 〈Echarge cst, execute_1 s〉 ].
    49 
    50 axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
    51 
    52 definition exec: trans_system io_out io_in ≝
    53  mk_trans_system … is_final execute_1_instruction.
    54 *)
    55 
    56 axiom exec: trans_system io_out io_in.
    57 
    58 definition ASM_fullexec: fullexec io_out io_in ≝
    59  mk_fullexec ??? exec make_global ?(*(λp.OK … (load (\fst p) (initialise_status … (Stub ??))))*).
    60 *)
    61 
     4(* Move where abstract_status is defined! *)
    625definition mk_trans_system_of_abstract_status:
    63  abstract_status → trans_system io_out io_in
     6 ∀S:abstract_status. (S → IOMonad io_out io_in S) → trans_system io_out io_in
    647≝
    65  λS.
     8 λS,as_eval.
    669  mk_trans_system ?? unit (λ_.as_status S) (λ_.as_result S)
    6710   (λ_.λstatus.
    … …  
    7316     return 〈 tr, status' 〉).
    7417
    75 definition 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).
     18definition mk_fullexec_of_abstract_status:
     19 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in
     20≝ λS,as_eval,as_init.
     21   mk_fullexec ?? unit (mk_trans_system_of_abstract_status S as_eval) (λ_.it)
     22    (λ_.return as_init).
    7923
    8024definition mk_preclassified_system_of_abstract_status:
    81  abstract_status → preclassified_system
    82 ≝ λS.
     25 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
     26≝ λS,as_eval,as_init.
    8327   mk_preclassified_system
    84     (mk_fullexec_of_abstract_status S) (λ_.λst. ¬(is_none … (as_label … st)))
     28    (mk_fullexec_of_abstract_status S as_eval as_init)
     29    (λ_.λst. ¬(is_none … (as_label … st)))
    8530    (λ_.as_classify S)
    8631    (λ_.λst,prf. as_call_ident S «st,?»).
    8732 @hide_prf cases (as_classify ??) in prf; normalize // *
    88 qed. 
     33qed.
    8934
    90 (*
    91 definition OC_transition_system: trans_system io_out io_in ≝
    92  mk_trans_system ?? OC_global OC_status ?
    93   execute_1_instruction.
     35(* End move *)
    9436
    95 definition OC_global ≝ BitVectorTrie Byte 16 × costlabel_map.
    96 
    97 definition OC_status ≝ λgl:OC_global. Status (\fst gl).
    98 
    99 definition 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 
    108 definition OC_transition_system: trans_system io_out io_in ≝
    109  mk_trans_system ?? OC_global OC_status ?
    110   execute_1_instruction.
    111 
    112 definition OC_fullexec: fullexec io_out io_in ≝
    113  mk_fullexec ??
    114   labelled_object_code*)
    115  
    116 
    117 definition OC_preclassified_system ≝
     37definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
    11838 λc:labelled_object_code.
    119   mk_preclassified_system_of_abstract_status (ASM_abstract_status (\fst c) (\fst (\snd c))).
     39  let cm ≝ load_code_memory (oc c) in
     40  mk_preclassified_system_of_abstract_status
     41   (ASM_abstract_status cm (costlabels c))
     42   (λst. return (execute_1 … st))
     43   (initialise_status … cm).
Note: See TracChangeset for help on using the changeset viewer.