Changeset 2910 for src


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).

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2907 r2910  
    2525qed.
    2626
     27definition OC_as_call_ident:
     28 ∀prog:labelled_object_code.∀cm. (Σs:Status cm. OC_classify … s = cl_call) → ident
     29
     30 λprog,cm,s0.
     31  let pc ≝ program_counter ?? (execute_1' cm s0) in
     32  match lookup_opt ?? pc (symboltable prog) with
     33  [ None ⇒ ⊥ | Some id ⇒ id ].
     34cases daemon (*CSC: we need a specification of the symboltable for this *)
     35qed.
     36
    2737definition OC_abstract_status: labelled_object_code → abstract_status ≝
    2838 λprog.
     
    3747      (next_instruction_properly_relates_program_counters code_memory)
    3848      (λst. as_result_of_finaladdr … st (final_pc prog))
    39       ?
     49      (OC_as_call_ident prog …)
    4050      ?.
    41   #x cases daemon (* XXX: (tail)call_ident function *)
     51 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
     52 try (#x #y #abs) try (#x #abs) try #abs destruct
    4253qed.
    4354
  • 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.