Changeset 2899 for src/ASM/Interpret2.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r2875 r2899  
    4242  mk_preclassified_system_of_abstract_status
    4343   labelled_object_code
    44    (ASM_abstract_status cm (costlabels c))
     44   (OC_abstract_status cm (costlabels c))
    4545   (λst. return (execute_1 … st))
    4646   (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 TracChangeset for help on using the changeset viewer.