source: src/ASM/Interpret2.ma @ 2899

Last change on this file since 2899 was 2899, checked in by sacerdot, 7 years ago
  1. some renaming ASM_xxx to OC_xxx
  2. ASM_pre_classified_system implemented (up to the same missing cases as OC_pre_classified_system) Note: the invariant that the pc is always in the program cannot be maintained in case of function pointer calls and returns. To be dropped.
File size: 4.1 KB
Line 
1include "ASM/ASMCosts.ma".
2include "common/Measurable.ma".
3
4(* Move where abstract_status is defined! *)
5definition mk_trans_system_of_abstract_status:
6 ∀S:abstract_status. (S → IOMonad io_out io_in S) → trans_system io_out io_in
7
8 λS,as_eval.
9  mk_trans_system ?? unit (λ_.as_status S) (λ_.as_result S)
10   (λ_.λstatus.
11     let tr ≝
12      match as_label … status with
13      [ Some cst ⇒ Echarge cst
14      | None ⇒ E0 ] in
15     ! status' ← as_eval … status ;
16     return 〈 tr, status' 〉).
17
18definition mk_fullexec_of_abstract_status:
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)
23    (λ_.return as_init).
24
25definition mk_preclassified_system_of_abstract_status:
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.
29   mk_preclassified_system
30    (mk_fullexec_of_abstract_status program S as_eval as_init)
31    (λ_.λst. ¬(is_none … (as_label … st)))
32    (λ_.as_classify S)
33    (λ_.λst,prf. as_call_ident S «st,?»).
34 @hide_prf cases (as_classify ??) in prf; normalize // *
35qed.
36
37(* End move *)
38
39definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
40 λc:labelled_object_code.
41  let cm ≝ load_code_memory (oc c) in
42  mk_preclassified_system_of_abstract_status
43   labelled_object_code
44   (OC_abstract_status cm (costlabels c))
45   (λst. return (execute_1 … st))
46   (initialise_status … cm).
47
48(* Pre-classified system for ASM *)
49
50include "ASM/Assembly.ma".
51
52(* Move next function in interpret? *)
53definition execute_1_pseudo_instruction':
54 ∀cm. ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
55 λcm,sigma,policy,status.
56  execute_1_pseudo_instruction cm
57   (ticks_of cm  sigma policy) status ….
58cases daemon (*CSC: we need to prove that we remain inside the program
59 (code closed), which is impossible in case of function pointers.
60 But the type does not allow to fail (yet?) *)
61qed.
62
63definition classify_pseudo_instruction: pseudo_instruction → status_class ≝
64 λinstr.
65  match instr with
66  [ Instruction pre ⇒ ASM_classify00 … pre
67  | Comment _ ⇒ cl_other
68  | Cost _ ⇒ cl_other
69  | Jmp _ ⇒ cl_other
70  | Jnz _ _ _ ⇒ cl_jump
71  | MovSuccessor _ _ _ ⇒ cl_other
72  | Call _ ⇒ cl_call
73  | Mov _ _ ⇒ cl_other ].
74
75definition ASM_classify: ∀cm. PseudoStatus cm → status_class ≝
76λcm,s.
77 classify_pseudo_instruction
78  (\fst (fetch_pseudo_instruction (code cm) (program_counter … s) ?)).
79cases daemon (*CSC: again*)
80qed.
81
82definition ASM_next_instruction_properly_relates_program_counters ≝
83  λcm.
84  λbefore: PseudoStatus cm.
85  λafter : PseudoStatus cm.
86    let 〈instruction, program_counter_after〉 ≝
87     fetch_pseudo_instruction (code cm) (program_counter … before) ?
88    in
89     program_counter ?? after = program_counter_after.
90cases daemon (*CSC: again*)
91qed.
92
93definition ASM_as_label_of_pc:
94 ∀prog:pseudo_assembly_program. Word → option costlabel
95
96 λprog,pc.
97 match \fst (fetch_pseudo_instruction (code prog) pc ?) with
98 [ Cost label ⇒ Some … label
99 | _ ⇒ None ? ].
100cases daemon (*CSC: again*)
101qed.
102
103definition ASM_abstract_status:
104 ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
105  λprog,sigma,policy.
106    mk_abstract_status
107      (PseudoStatus prog)
108      (λs1,s2. execute_1_pseudo_instruction' … sigma policy s1 = s2)
109      word_deqset
110      (program_counter …)
111      (ASM_classify …)
112      (ASM_as_label_of_pc prog …)
113      (ASM_next_instruction_properly_relates_program_counters prog)
114      ? (* (λs.False) *)
115      ?
116      ?.
117  #x cases daemon (* XXX: is_final predicate, (tail)call_ident function *)
118qed.
119
120definition ASM_preclassified_system:
121 pseudo_assembly_program → ∀sigma,policy. preclassified_system ≝
122 λc,sigma,policy.
123  mk_preclassified_system_of_abstract_status
124   pseudo_assembly_program
125   (ASM_abstract_status c sigma policy)
126   (λst. return (execute_1_pseudo_instruction' … sigma policy st))
127   (initialise_status … c).
Note: See TracBrowser for help on using the repository browser.