Changeset 2910 for src/ASM/Interpret2.ma


Ignore:
Timestamp:
Mar 19, 2013, 11:19:32 PM (7 years ago)
Author:
sacerdot
Message:

Abstract statuses for ASM and OC completed.
A simple test program can now be run in every pass of the compiler, always
showing the same behaviour (up to initialization).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r2907 r2910  
    105105   as_result_of_finaladdr … st finaladdr.
    106106
     107include "common/AssocList.ma".
     108
     109definition ASM_as_call_ident:
     110 ∀prog,sigma,policy.(Σs:PseudoStatus prog. ASM_classify … s = cl_call) → ident
     111
     112 λprog,sigma,policy,s0.
     113  let st ≝ execute_1_pseudo_instruction' prog sigma policy s0 in
     114  let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? (program_counter … st)) … (code prog) ? in
     115  match lbl with
     116  [ None ⇒ ⊥
     117  | Some lbl' ⇒
     118     match assoc_list_lookup ?? lbl' (eq_identifier …) (renamed_symbols prog) with
     119     [ None ⇒ ⊥ | Some id ⇒ id ]].
     120cases daemon (*CSC: we need a specification of the renamed_symbols for this *)
     121qed.
     122
    107123definition ASM_abstract_status:
    108124 ∀prog:pseudo_assembly_program.∀sigma,policy.abstract_status ≝
     
    117133      (ASM_next_instruction_properly_relates_program_counters prog)
    118134      (ASM_as_result …)
    119       ?
     135      (ASM_as_call_ident prog sigma policy …)
    120136      ?.
    121   #x cases daemon (* XXX: (tail)call_ident function *)
     137 * #st whd in ⊢ (??%? → ?); cases (\fst (fetch_pseudo_instruction ???)) [*]
     138 normalize try (#x #y #abs) try (#x #abs) try #abs destruct (abs)
    122139qed.
    123140
Note: See TracChangeset for help on using the changeset viewer.