Changeset 2875 for src


Ignore:
Timestamp:
Mar 15, 2013, 1:32:50 AM (7 years ago)
Author:
sacerdot
Message:

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r2764 r2875  
    1717
    1818definition 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)
     19 ∀program: Type[0].
     20  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in
     21≝ λprogram,S,as_eval,as_init.
     22   mk_fullexec ?? program (mk_trans_system_of_abstract_status S as_eval) (λ_.it)
    2223    (λ_.return as_init).
    2324
    2425definition mk_preclassified_system_of_abstract_status:
    25  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
    26 ≝ λS,as_eval,as_init.
     26 ∀program: Type[0].
     27  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
     28≝ λprogram,S,as_eval,as_init.
    2729   mk_preclassified_system
    28     (mk_fullexec_of_abstract_status S as_eval as_init)
     30    (mk_fullexec_of_abstract_status program S as_eval as_init)
    2931    (λ_.λst. ¬(is_none … (as_label … st)))
    3032    (λ_.as_classify S)
     
    3941  let cm ≝ load_code_memory (oc c) in
    4042  mk_preclassified_system_of_abstract_status
     43   labelled_object_code
    4144   (ASM_abstract_status cm (costlabels c))
    4245   (λst. return (execute_1 … st))
  • src/compiler.ma

    r2841 r2875  
    2929 | ertlptr_pass: pass
    3030 | ltl_pass: pass
    31  | lin_pass: pass.
     31 | lin_pass: pass
     32 | assembly_pass: pass
     33 | object_code_pass: pass.
    3234
    3335definition with_stack_model : Type[0] → Type[0] ≝
     
    4850  | ertlptr_pass ⇒ with_stack_model ertlptr_program
    4951  | ltl_pass ⇒ with_stack_model ltl_program
    50   | lin_pass ⇒ with_stack_model lin_program ].
     52  | lin_pass ⇒ with_stack_model lin_program
     53  | assembly_pass ⇒ pseudo_assembly_program
     54  | object_code_pass ⇒ labelled_object_code ].
    5155
    5256definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit.
     
    109113  let st ≝ lookup_stack_cost … p in
    110114  let i ≝ observe lin_pass 〈p,st〉 in
    111    ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
     115   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
     116  let i ≝ observe assembly_pass p in
    112117   return 〈p,stack_cost,max_stack〉.
    113118
     
    115120include "ASM/Policy.ma".
    116121
    117 definition assembler : pseudo_assembly_program → res labelled_object_code ≝
    118 λp.
     122definition assembler :
     123 observe_pass → pseudo_assembly_program → res labelled_object_code ≝
     124λobserve,p.
    119125  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
    120126  let sigma ≝ λppc. \fst sigma_pol ppc in
    121127  let pol ≝ λppc. \snd sigma_pol ppc in
    122   OK ? (assembly p sigma pol).
     128  let p ≝ assembly p sigma pol in
     129  let i ≝ observe object_code_pass p in
     130  OK ? p.
    123131
    124132(* Cost lifting *)
     
    148156  ! 〈init_cost,p',p〉 ← front_end observe p;
    149157  ! 〈p,stack_cost,max_stack〉 ← back_end observe p;
    150   ! p ← assembler p;
     158  ! p ← assembler observe p;
    151159  let k ≝ ASM_cost_map p in
    152160  let k' ≝
  • src/correctness.ma

    r2852 r2875  
    109109  ∃n1,n2.
    110110   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
    111    observables (OC_preclassified_system (c_labelled_object_code … p)) it n1 n2
     111   observables (OC_preclassified_system (c_labelled_object_code … p))
     112    (c_labelled_object_code … p) n1 n2
    112113  ∧
    113114   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
  • src/semantics.ma

    r2841 r2875  
    99include "LTL/LTL_semantics.ma".
    1010include "LIN/LIN_semantics.ma".
     11include "ASM/Interpret2.ma".
    1112
    1213record preclassified_system_pass (P:pass) : Type[2] ≝
     
    1617
    1718definition preclassified_system_of_pass:
    18  ∀pass. preclassified_system_pass pass ≝
     19 ∀pass. syntax_of_pass pass → preclassified_system_pass pass ≝
    1920 λpass.
    20   match pass with
    21   [ clight_pass ⇒ mk_preclassified_system_pass … Clight_pcs …
    22   | clight_switch_removed_pass ⇒ mk_preclassified_system_pass … Clight_pcs …
    23   | clight_label_pass ⇒ mk_preclassified_system_pass … Clight_pcs …
    24   | clight_simplified_pass ⇒ mk_preclassified_system_pass … Clight_pcs …
    25   | cminor_pass ⇒ mk_preclassified_system_pass … Cminor_pcs …
    26   | rtlabs_pass ⇒ mk_preclassified_system_pass … RTLabs_pcs …
     21  match pass return λpass.syntax_of_pass pass → preclassified_system_pass pass with
     22  [ clight_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
     23  | clight_switch_removed_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
     24  | clight_label_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
     25  | clight_simplified_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
     26  | cminor_pass ⇒ λ_.mk_preclassified_system_pass … Cminor_pcs …
     27  | rtlabs_pass ⇒ λ_.mk_preclassified_system_pass … RTLabs_pcs …
    2728  | rtl_separate_pass ⇒
    28      mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) …
     29     λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) …
    2930  | rtl_uniq_pass ⇒
    30      mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …
     31     λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …
    3132  | ertl_pass ⇒
    32      mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
     33     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
    3334  | ertlptr_pass ⇒
    34      mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
     35     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
    3536  | ltl_pass ⇒
    36      mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
     37     λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
    3738  | lin_pass ⇒
    38      mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
     39     λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
     40  | assembly_pass ⇒
     41     ?
     42  | object_code_pass ⇒
     43     λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
    3944  ].
    40 %
     45try % cases daemon
    4146qed.
    4247
     
    4651
    4752 λpass,prog,n,print_pass,print_event,print_error,print_exit.
    48  let pcs ≝ preclassified_system_of_pass pass in
     53 let pcs ≝ preclassified_system_of_pass pass prog in
    4954  let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in
    5055  let g ≝ make_global … pcs prog in
Note: See TracChangeset for help on using the changeset viewer.