Changeset 2422 for src/joint/Traces.ma


Ignore:
Timestamp:
Oct 30, 2012, 4:23:09 PM (8 years ago)
Author:
tranquil
Message:

adapted joint to cl_call f

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2286 r2422  
    11include "joint/semantics.ma".
     2include "common/StructuredTraces.ma".
    23
    34record evaluation_params : Type[1] ≝
     
    78 ; ev_genv: genv sparams globals
    89 ; io_env : state sparams → ∀o:io_out.res (io_in o)
    9  } .
     10 }.
     11 
     12record prog_params : Type[1] ≝
     13 { prog_spars : sem_params
     14 ; prog : joint_program prog_spars
     15 ; prog_io : state prog_spars → ∀o.res (io_in o)
     16 }.
    1017
    11 (*record classifier_params : Type[1] ≝
    12   { cl_pars :> evaluation_parameters
    13   ; cl_ext_step : ext_step cl_pars → status_class
    14   ; cl_ext_fin_stmt : ext_fin_stmt cl_pars → status_class
    15   }.*)
     18definition make_global : prog_params → evaluation_params
     19
     20λpars.
     21(* Invariant: a -1 block is unused in common/Globalenvs *)
     22let b ≝ mk_block Code (-1) in
     23let ptr ≝ mk_pointer b (mk_offset (bv_zero …)) in
     24let p ≝ prog pars in
     25mk_evaluation_params
     26  (prog_var_names … p)
     27  (prog_spars pars)
     28  «ptr, refl …»
     29  (mk_genv_gen ?? (globalenv_noinit ? p) ?)
     30  (prog_io pars).
     31(* TODO or TOBEFOUND *)
     32cases daemon
     33qed.
    1634
     35coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
     36≝ make_global on _p : prog_params to evaluation_params.
     37
     38
     39axiom ExternalMain : String.
     40check save_frame
     41
     42definition make_initial_state :
     43 ∀pars: prog_params.res (state_pc pars) ≝
     44λpars.let p ≝ prog pars in
     45  let sem_globals : evaluation_params ≝ pars in
     46  let ge ≝ ev_genv sem_globals in
     47  let m ≝ alloc_mem … p in
     48  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
     49  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
     50  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
     51  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
     52  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in
     53  let main ≝ prog_main … p in
     54  let st0 ≝ mk_state pars (empty_framesT …) spp ispp (BBbit false) (empty_regsT … spp) m in
     55  (* use exit sem_globals as ra and call_dest_for_main as dest *)
     56  ! st0' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
     57  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
     58  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
     59  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
     60  match main_fd with
     61  [ Internal fn ⇒
     62    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
     63  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
     64  ].
     65  [ %
     66  | cases ispb
     67  | cases spb
     68  ] normalize //
     69qed.
     70
     71definition step_flow_classifier :
     72  ∀p : evaluation_params.∀F,flows.
     73  step_flow p F flows → status_class ≝
     74  λp,F,flows,flow.match flow with
     75  [ Redirect _ _ ⇒ cl_jump
     76  | Init bl _ _ _ ⇒
     77    match symbol_for_block … (ev_genv p) (mk_block Code bl) with
     78    [ Some f ⇒ cl_call f
     79    | None ⇒ cl_other (* we don't care, as call will fail anyway *)
     80    ]
     81  | Proceed flows ⇒
     82    match flows with
     83    [ Labels lbls ⇒
     84      match lbls with
     85      [ nil ⇒ cl_other
     86      | _ ⇒ cl_jump
     87      ]
     88    | _ ⇒ cl_other
     89    ]
     90  ].
     91
     92definition fin_step_flow_classifier :
     93  ∀p : evaluation_params.∀F,flows.
     94  fin_step_flow p F flows → status_class ≝
     95  λp,F,flows,flow.match flow with
     96  [ FRedirect lbls _ ⇒
     97    match lbls with
     98    [ nil ⇒ (* not really possible, we don't care *) cl_other
     99    | cons _ tl ⇒
     100      match tl with
     101      [ nil ⇒ (* only one label *) cl_other
     102      | _ ⇒ (* fork *) cl_jump
     103      ]
     104    ]
     105  | FTailInit bl _ _ ⇒ (* not implemented for now, probably needs new class *)
     106    cl_other
     107  | _ ⇒ cl_return
     108  ].
    17109
    18110definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
     
    58150   (* as_pc_of ≝ *) (pc …)
    59151   (* as_classifier ≝ *)
    60     (λs,cl.∃fn,stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉 ∧
    61      stmt_classifier … stmt = cl)
     152    (λs,cl.∃fn,stmt.
     153      fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉 ∧
     154      match stmt with
     155      [ sequential stp nxt ⇒
     156        ∃flow,s'.
     157        io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) = return 〈flow, s'〉 ∧
     158        step_flow_classifier … flow = cl
     159      | final stp ⇒
     160        ∃flow.io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) = return flow ∧
     161        fin_step_flow_classifier … flow = cl
     162      ])
    62163   (* as_label_of_pc ≝ *)
    63164    (λpc.
Note: See TracChangeset for help on using the changeset viewer.