Changeset 2899 for src/ASM/Interpret2.ma

Timestamp:

Mar 19, 2013, 12:33:13 AM (7 years ago)

Author:

sacerdot

Message:

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:

• src/ASM/Interpret2.ma (modified) (1 diff)

src/ASM/Interpret2.ma

@@ -42 +42 @@
   mk_preclassified_system_of_abstract_status
    labelled_object_code
-   (ASM_abstract_status cm (costlabels c))
+   (OC_abstract_status cm (costlabels c))
    (λst. return (execute_1 … st))
    (initialise_status … cm).
+
+(* Pre-classified system for ASM *)
+
+include "ASM/Assembly.ma".
+
+(* Move next function in interpret? *)
+definition execute_1_pseudo_instruction':
+ ∀cm. ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
+ λcm,sigma,policy,status.
+  execute_1_pseudo_instruction cm
+   (ticks_of cm  sigma policy) status ….
+cases daemon (*CSC: we need to prove that we remain inside the program
+ (code closed), which is impossible in case of function pointers.
+ But the type does not allow to fail (yet?) *)
+qed.
+
+definition classify_pseudo_instruction: pseudo_instruction → status_class ≝
+ λinstr.
+  match instr with
+  [ Instruction pre ⇒ ASM_classify00 … pre
+  | Comment _ ⇒ cl_other
+  | Cost _ ⇒ cl_other
+  | Jmp _ ⇒ cl_other
+  | Jnz _ _ _ ⇒ cl_jump
+  | MovSuccessor _ _ _ ⇒ cl_other
+  | Call _ ⇒ cl_call
+  | Mov _ _ ⇒ cl_other ].
+
+definition ASM_classify: ∀cm. PseudoStatus cm → status_class ≝
+λcm,s.
+ classify_pseudo_instruction
+  (\fst (fetch_pseudo_instruction (code cm) (program_counter … s) ?)).
+cases daemon (*CSC: again*)
+qed.
+
+definition ASM_next_instruction_properly_relates_program_counters ≝
+  λcm.
+  λbefore: PseudoStatus cm.
+  λafter : PseudoStatus cm.
+    let 〈instruction, program_counter_after〉 ≝
+     fetch_pseudo_instruction (code cm) (program_counter … before) ?
+    in
+     program_counter ?? after = program_counter_after.
+cases daemon (*CSC: again*)
+qed.
+
+definition ASM_as_label_of_pc:
+ ∀prog:pseudo_assembly_program. Word → option costlabel
+≝
+ λprog,pc.
+ match \fst (fetch_pseudo_instruction (code prog) pc ?) with 
+ [ Cost label ⇒ Some … label
+ | _ ⇒ None ? ].
+cases daemon (*CSC: again*)
+qed.
+
+definition ASM_abstract_status:
+ ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
+  λprog,sigma,policy.
+    mk_abstract_status
+      (PseudoStatus prog)
+      (λs1,s2. execute_1_pseudo_instruction' … sigma policy s1 = s2)
+      word_deqset
+      (program_counter …)
+      (ASM_classify …)
+      (ASM_as_label_of_pc prog …)
+      (ASM_next_instruction_properly_relates_program_counters prog)
+      ? (* (λs.False) *)
+      ?
+      ?.
+  #x cases daemon (* XXX: is_final predicate, (tail)call_ident function *)
+qed.
+
+definition ASM_preclassified_system:
+ pseudo_assembly_program → ∀sigma,policy. preclassified_system ≝
+ λc,sigma,policy.
+  mk_preclassified_system_of_abstract_status
+   pseudo_assembly_program
+   (ASM_abstract_status c sigma policy)
+   (λst. return (execute_1_pseudo_instruction' … sigma policy st))
+   (initialise_status … c).