Changeset 2422


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

adapted joint to cl_call f

Location:
src/joint
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2286 r2422  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
    9 include "common/StructuredTraces.ma".
    109
    1110(* Here is the structure of parameter records (downward edges are coercions,
     
    169168λp,g,P,inst. All … P (step_labels … inst).
    170169
    171 definition step_classifier :
    172   ∀p.∀globals.
    173     joint_step p globals → status_class ≝ λp,g,s.
    174   match s with
    175   [ step_seq s ⇒
    176     match s with
    177     [ CALL_ID _ _ _ ⇒ cl_call
    178     | extension_call _ ⇒ cl_call
    179     | _ ⇒ cl_other
    180     ]
    181   | COND _ _ ⇒ cl_jump
    182   ].
    183 
    184170record stmt_params : Type[1] ≝
    185171  { uns_pars :> unserialized_params
     
    207193    ].
    208194
    209 definition fin_step_classifier :
    210   ∀p : stmt_params.
    211     joint_fin_step p → status_class
    212   ≝ λp,s.
    213   match s with
    214   [ GOTO _ ⇒ cl_other
    215   | _ ⇒ cl_return
    216   ].
    217 
    218195inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    219196  | sequential: joint_step p globals → succ p → joint_statement p globals
    220197  | final: joint_fin_step p → joint_statement p globals.
    221 
    222 definition stmt_classifier :
    223   ∀p : stmt_params.∀globals.
    224     joint_statement p globals → status_class
    225   ≝ λp,g,s.
    226   match s with
    227   [ sequential stp _ ⇒ step_classifier p g stp
    228   | final stp ⇒ fin_step_classifier p stp
    229   ].
    230198
    231199coercion extension_fin_to_fin_step : ∀p : stmt_params.
     
    466434definition joint_closed_internal_function ≝
    467435  λp,globals.
    468     Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
     436    Σdef : joint_internal_function p globals. code_closed … (joint_if_code … def).
    469437
    470438definition set_joint_code ≝
     
    534502    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
    535503
    536 definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
     504definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
    537505
    538506definition joint_program ≝
  • src/joint/SemanticUtils.ma

    r2286 r2422  
    151151definition make_sem_graph_params :
    152152  ∀pars : graph_params.
    153   ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
     153  ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars).
    154154  sem_params ≝
    155155  λpars,g_pars.
     
    190190definition make_sem_lin_params :
    191191  ∀pars : lin_params.
    192   ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
     192  ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars).
    193193  sem_params ≝
    194194  λpars,g_pars.
  • 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.
  • src/joint/blocks.ma

    r2286 r2422  
    239239definition seq_block_step_in_code ≝
    240240  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst.
    241   src ~❨\fst B, \fst l❩~> \snd l in c ∧ step_in_code … c (\snd l) (\snd B) dst.
     241  ∃hd,tl.l = hd @ [tl] ∧
     242  src ~❨\fst B, l❩~> tl in c ∧ step_in_code … c tl (\snd B) dst.
    242243
    243244definition seq_block_fin_step_in_code ≝
    244245  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit.
    245   src ~❨\fst B, \fst l❩~> \snd l in c ∧ fin_step_in_code … c (\snd l) (\snd B).
     246  ∃hd,tl.l = hd @ [tl] ∧
     247  src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
    246248
    247249(* generates ambiguity even if it shouldn't
  • src/joint/linearise.ma

    r2286 r2422  
    652652  ∀p : unserialized_params.
    653653  ∀globals.
    654     joint_internal_function (mk_graph_params p) globals →
    655     joint_internal_function (mk_lin_params p) globals
     654    joint_closed_internal_function (mk_graph_params p) globals →
     655    joint_closed_internal_function (mk_lin_params p) globals
    656656     (* ∃sigma : identifier_map LabelTag ℕ.
    657657        let g ≝ joint_if_code ?? (pi1 … fin) in
     
    669669                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    670670                    (stmt_implicit_label … s)) (nth_opt … n c)*) ≝
    671   λp,globals,f_in.
    672   mk_joint_internal_function (mk_lin_params p) globals
     671  λp,globals,f_sig.let f_in ≝ pi1 … f_sig in
     672  «mk_joint_internal_function (mk_lin_params p) globals
    673673   (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in)
    674674   (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in)
    675675   (joint_if_stacksize ?? f_in)
    676    (linearise_code p globals (joint_if_code … f_in)
    677    (match daemon in False with [ ])
    678    (joint_if_entry … f_in))
    679    0 0 (* exit is dummy! *).
     676   (linearise_code p globals (joint_if_code … f_in) (pi2 … f_sig) (joint_if_entry … f_in))
     677   0 0 (* exit is dummy! *), ?».
    680678elim (linearise_code ?????) #c * #code_closed
     679[3: #_ assumption ]
    681680@hide_prf
    682681* #sigma * #O_in #sigma_prop
     
    688687]
    689688qed.
     689
     690definition linearise : ∀p : unserialized_params.
     691  program (joint_function (mk_graph_params p)) ℕ →
     692  program (joint_function (mk_lin_params p)) ℕ ≝
     693  λp,pr.transform_program ??? pr
     694    (λglobals.transf_fundef ?? (linearise_int_fun p globals)).
  • src/joint/semantics.ma

    r2286 r2422  
    1717}.
    1818
    19 definition genv ≝ λp.genv_gen (joint_internal_function p).
     19definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
    2020coercion genv_to_genv_t :
    2121  ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
    2222  λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
    23 
    2423definition cpointer ≝ Σp.ptype p = Code.
    2524definition xpointer ≝ Σp.ptype p = XData.
    2625unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
    2726unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
     27unification hint 0 ≔ p,g ⊢
     28  joint_closed_internal_function p g ≡
     29  Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)).
    2830
    2931record sem_state_params : Type[1] ≝
     
    8284  genv pars globals →
    8385  block →
    84   res (joint_internal_function pars globals) ≝
     86  res (joint_closed_internal_function pars globals) ≝
    8587  λpars,globals,ge,b.
    8688  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     
    9597  genv pars globals →
    9698  cpointer →
    97   res (joint_internal_function pars globals) ≝
     99  res (joint_closed_internal_function pars globals) ≝
    98100 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
    99101
     
    149151  ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
    150152      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
     153  ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
     154      state st_pars → IO io_out io_in ident
    151155  ; eval_ext_call: ∀globals.genv_gen F globals →
    152156      ext_call uns_pars → state st_pars →
    153157      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
     158  ; ext_call_id : ∀globals.genv_gen F globals → ext_call uns_pars →
     159      state st_pars → IO io_out io_in ident
    154160  ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
    155161  (* do something more in some op2 calculations (e.g. mark a register for correction
     
    266272(* parameters that are defined by serialization *)
    267273record more_sem_params (pp : params) : Type[1] ≝
    268   { msu_pars :> more_sem_unserialized_params pp (joint_internal_function pp)
     274  { msu_pars :> more_sem_unserialized_params pp (joint_closed_internal_function pp)
    269275  ; offset_of_point : code_point pp → option offset (* can overflow *)
    270276  ; point_of_offset : offset → code_point pp
     
    347353definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
    348354  genv p globals → cpointer →
    349   res ((joint_internal_function p globals) × (joint_statement p globals)) ≝
     355  res ((joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
    350356  λp,msp,globals,ge,ptr.
    351357  let pt ≝ point_of_pointer ? msp ptr in
     
    427433
    428434definition eval_seq_no_pc :
    429  ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals →
     435 ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals →
    430436  state p → ∀s:joint_seq p globals.
    431437  IO io_out io_in (state p) ≝
     
    513519definition eval_step :
    514520 ∀p:sem_params.∀globals. genv p globals →
    515   joint_internal_function p globals → state p →
     521  joint_closed_internal_function p globals → state p →
    516522  ∀s:joint_step p globals.
    517523  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
     
    533539
    534540definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
    535   (* current function *) joint_internal_function p globals → state p → ∀s : joint_fin_step p.
     541  (* current function *) joint_closed_internal_function p globals → state p → ∀s : joint_fin_step p.
    536542  IO io_out io_in (state p) ≝
    537543 λp,globals,ge,curr_fn,st,s.
     
    544550
    545551definition eval_fin_step_pc :
    546  ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → state p →
     552 ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals → state p →
    547553  ∀s:joint_fin_step p.
    548554  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
     
    557563
    558564definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
    559   state p → Z → joint_internal_function p globals → call_args p →
     565  state p → Z → joint_closed_internal_function p globals → call_args p →
    560566  res (state_pc p) ≝
    561567  λp,globals,ge,st,id,fn,args.
     
    600606definition eval_statement :
    601607 ∀globals.∀p:sem_params.genv p globals →
    602   state_pc p → joint_internal_function p globals → joint_statement p globals →
     608  state_pc p → joint_closed_internal_function p globals → joint_statement p globals →
    603609    IO io_out io_in (state_pc p) ≝
    604610 λglobals,p,ge,st,curr_fn,stmt.
  • src/joint/semantics_blocks.ma

    r2324 r2422  
    232232  %* #H @H -H
    233233  lapply tl_other lapply rest_in_code
    234   (* BUG? cases tl causes "Ill formed pattern" *)
    235   @(match tl with [ nil ⇒ ? | cons hd' tl' ⇒ ?])
     234  cases tl [2: #hd' #tl' ]
    236235  cases rest [2,4: #mid' #rest']
    237   [1,4: * ]
     236  [2,3: * ]
    238237  [2: whd in ⊢ (%→?); #EQ' destruct(EQ') *
    239238  | ** #nxt' * #at_mid #_ #_ * #mid_other #_
Note: See TracChangeset for help on using the changeset viewer.