Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils_paolo.ma

    r1641 r1882  
    2121(******************************** GRAPHS **************************************)
    2222
    23 definition graph_pointer_of_label0:
    24  pointer → label → Σp:pointer. ptype p = Code ≝
    25  λoldpc,l.
    26   mk_pointer Code
    27    (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))).
    28 // qed.
    29 
    30 definition graph_pointer_of_label :
    31   ∀pars : graph_params.∀globals. genv globals pars → pointer → label →
    32     res (Σp:pointer. ptype p = Code) ≝
    33  λ_.λ_.λ_.λoldpc,l.
    34   OK ? (graph_pointer_of_label0 oldpc l).
     23definition graph_pointer_of_label : cpointer → label → res cpointer ≝
     24  λoldpc,l.
     25  return (mk_pointer Code
     26   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))) : cpointer).
     27% qed.
    3528
    3629definition graph_label_of_pointer: pointer → res label ≝
    3730 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
    38 
    39 (*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    40  But I can't use it directly because this one uses a concrete definition of
    41  pointer_of_label and it is used to istantiate the more_sem_params record
    42  where the abstract version is declared as a field. Is there a better way
    43  to organize the code? *)
    44 definition graph_succ_p: label → address → res address ≝
    45  λl,old.
    46   do ptr ← pointer_of_address old ;
    47   let newptr ≝ graph_pointer_of_label0 ptr l in
    48   address_of_pointer newptr.
    4931
    5032definition graph_fetch_statement:
     
    5335 ∀globals.
    5436  genv globals pars →
    55   state sem_pars
     37  cpointer
    5638  res (joint_statement pars globals) ≝
    57  λpars,sem_pars,globals,ge,st.
    58   do p ← code_pointer_of_address (pc … st) ;
     39 λpars,sem_pars,globals,ge,p.
    5940  do f ← fetch_function … ge p ;
    6041  do l ← graph_label_of_pointer p;
     
    7152      pars
    7253      g_pars
    73       graph_succ_p
    74       (graph_pointer_of_label ?)
    75       (graph_fetch_statement ? ?)
     54      graph_pointer_of_label
     55      (λ_.λ_.graph_pointer_of_label)
     56      (graph_fetch_statement ? g_pars)
    7657    ).
    7758   
    7859(******************************** LINEAR **************************************)
    79 
    80 definition lin_succ_p: unit → address → res address :=
    81  λ_.λaddr. addr_add addr 1.
    82 
     60check mk_pointer
     61definition lin_succ_p: cpointer → unit → res cpointer :=
     62 λptr.λ_.return «mk_pointer Code (pblock ptr) ? (mk_offset (offv (poff ptr) + 1)), ?».
     63[%| cases ptr //] qed.
    8364
    8465axiom BadLabel: String.
     
    8667definition lin_pointer_of_label:
    8768 ∀pars : lin_params.
    88  ∀globals. genv globals pars → pointer → label →
    89   res (Σp:pointer. ptype p = Code) ≝
     69 ∀globals. genv globals pars → cpointer → label → res cpointer ≝
    9070 λpars,globals,ge,old,l.
    9171  do fn ← fetch_function … ge old ;
     
    9777     (joint_if_code … pars fn)) ;
    9878  OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
    99 // qed.
     79% qed.
    10080
    10181definition lin_fetch_statement:
     
    10383 ∀sem_pars : sem_state_params.
    10484 ∀globals.
    105  genv globals pars → state sem_pars → res (joint_statement pars globals) ≝
    106  λpars,sem_pars,globals,ge,st.
    107   do ppc ← pointer_of_address (pc … st) ;
     85 genv globals pars → cpointer → res (joint_statement pars globals) ≝
     86 λpars,sem_pars,globals,ge,ppc.
    10887  do fn ← fetch_function … ge ppc ;
    10988  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
     
    123102      lin_succ_p
    124103      (lin_pointer_of_label ?)
    125       (lin_fetch_statement ? ?)
     104      (lin_fetch_statement ? g_pars)
    126105    ).
    127106   
    128 
     107definition step_unbranching : ∀p,globals.joint_step p globals → bool ≝
     108  λp,globals,stp.match stp with
     109  [ COND _ _ ⇒ false
     110  | CALL_ID _ _ _ ⇒ false
     111  | extension c' ⇒ (* FIXME: does not care about calling extensions!! *)
     112    match ext_step_labels … c' with
     113    [ nil ⇒ true
     114    | _ ⇒ false
     115    ]
     116  | _ ⇒ true
     117  ].
     118
     119definition is_not_seq : ∀p,globals.joint_statement p globals → bool ≝
     120  λp,globals,stp.match stp with
     121  [ sequential _ _ ⇒ false
     122  | _ ⇒ true
     123  ].
     124
     125inductive s_block (p : params) (globals : list ident) : Type[0] ≝
     126  | Skip : s_block p globals
     127  | FinStep : (Σs.bool_to_Prop (¬step_unbranching p globals s)) → s_block p globals
     128  | FinStmt : (Σs.bool_to_Prop (is_not_seq p globals s)) → s_block p globals
     129  | Cons : (Σs.bool_to_Prop (step_unbranching p globals s)) → s_block p globals → s_block p globals.
     130
     131include "utilities/bind_new.ma".
     132
     133definition Block ≝ λp : params.λglobals.bind_new (localsT p) (s_block p globals).
     134
     135definition Bcons ≝ λp : params.λglobals.
     136    λs : Σs.bool_to_Prop (step_unbranching p globals s).
     137    λB : Block p globals.
     138    ! b ← B ; return Cons ?? s b.
     139
     140interpretation "block cons" 'vcons hd tl = (Bcons ??? hd tl).
     141
     142let rec is_unbranching p globals (b1 : s_block p globals) on b1 : bool ≝
     143  match b1 with
     144  [ Skip ⇒ true
     145  | FinStep _ ⇒ false
     146  | FinStmt _ ⇒ false
     147  | Cons _ tl ⇒ is_unbranching ?? tl
     148  ].
     149
     150let rec Is_unbranching p globals (b1 : Block p globals) on b1 : Prop ≝
     151  match b1 with
     152  [ bret b ⇒ bool_to_Prop (is_unbranching … b)
     153  | bnew f ⇒ ∀x.Is_unbranching … (f x)
     154  ].
     155
     156let rec s_block_append_aux p globals (b1 : s_block p globals) (b2 : s_block p globals) on b1 : is_unbranching … b1 → s_block p globals ≝
     157  match b1 return λx.is_unbranching ?? x → ? with
     158  [ Skip ⇒ λ_.b2
     159  | Cons x tl ⇒ λprf.Cons ?? x (s_block_append_aux ?? tl b2 prf)
     160  | _ ⇒ Ⓧ
     161  ].
     162
     163definition s_block_append ≝
     164  λp,globals.λb1 : Σb.bool_to_Prop (is_unbranching … b).λb2.
     165  match b1 with
     166  [ mk_Sig b1 prf ⇒ s_block_append_aux p globals b1 b2 prf ].
     167
     168definition Is_to_is_unbr : ∀p,globals.(ΣB.Is_unbranching p globals B) →
     169  bind_new (localsT p) (Σb.bool_to_Prop (is_unbranching p globals b)) ≝
     170  λp,globals. ?.
     171* #b elim b -b
     172[ #b #H @bret @b @H
     173| #f #IH #H @bnew #x @(IH x) @H
     174]
     175qed.
     176
     177lemma Is_to_is_unbr_OK : ∀p,globals,B.! b ← Is_to_is_unbr p globals B ; return pi1 … b = pi1 … B.
     178#p #globals * #b elim b
     179[ //
     180| #f #IH #H @bnew_proper
     181  #x @IH
     182]
     183qed.
     184 
     185definition Block_append ≝
     186  λp,globals.λB : Σb.Is_unbranching … b.λB'.
     187  ! b1 ← Is_to_is_unbr … B;
     188  ! b2 ← B';
     189  return s_block_append p globals b1 b2.
     190
     191definition all_unbranching ≝ λp,globals.All ? (λs.bool_to_Prop (step_unbranching p globals s)).
     192
     193let rec step_list_to_s_block (p : params) globals (l : list (joint_step p globals)) on l :
     194    s_block p globals ≝
     195  match l  with
     196  [ nil ⇒ Skip ??
     197  | cons hd tl ⇒
     198    If step_unbranching … hd then with prf do
     199      Cons ?? hd (step_list_to_s_block ?? tl)
     200    else with prf do
     201      FinStep ?? hd
     202  ]. [assumption | >prf % ] qed.
     203 
     204definition step_list_to_block : ∀R,p,g.? → Block R p g ≝
     205  λR,p,globals,l.bret R ? (step_list_to_s_block p globals l).
     206
     207record sem_rel (p1 : sem_params) (p2 : sem_params) (globals : list ident) : Type[0] ≝
     208  { function_rel : joint_function globals p1 → joint_function globals p2 → Prop
     209  ; genv_rel : genv globals p1 → genv globals p2 → Prop
     210  ; pc_rel : cpointer → cpointer → Prop
     211  ; st_rel : state p1 → state p2 → Prop
     212  ; stmt_rel : joint_statement p1 globals → Block
     213  (* TODO: state what do we need of genv_rel (like finding the same symbols and what relation to above rels ) *)
     214  ; st_to_pc_rel : ∀st1,st2.st_rel st1 st2 → pc_rel (pc ? st1) (pc ? st2)
     215  }.
     216 
     217(* move *)
     218definition beval_pair_of_xdata_pointer: (Σp:pointer. ptype p = XData) → beval × beval ≝
     219 λp. match p return λp. ptype p = XData → ? with [ mk_pointer pty pbl pok poff ⇒
     220  match pty return λpty. ? → pty = XData → ? with
     221   [ XData ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer XData pbl ? poff)) ?
     222   | _ ⇒ λpok'.λabs. ⊥] pok] ?.
     223[@(pi2 … p) |6: // |7: %] destruct (abs)
     224qed.
     225
     226definition safe_address_of_xdata_pointer: (Σp:pointer. ptype p = XData) → safe_address ≝ beval_pair_of_xdata_pointer.
     227cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H
     228lapply (pointer_compat_from_ind … H) -H cases b * #z * #H
     229%{«mk_pointer ? (mk_block ? z) H o,I»}
     230% [2,4: % [2,4: % [1,3: % [1,3: % ]] % |*:]|*:]
     231qed.
     232
     233definition state_rel : ∀p1,p2.∀R : sem_rel p1 p2.good_state p1 → good_state p2 → Prop ≝
     234  λp1,p2,R,st1,st2.
     235    frames_rel p1 p2 R (st_frms … st1) (st_frms … st2) ∧
     236    pc_rel p1 p2 R (pc … st1) (pc … st2) ∧
     237    sp_rel p1 p2 R
     238      (safe_address_of_xdata_pointer (sp … st1))
     239      (safe_address_of_xdata_pointer (sp … st2)) ∧
     240    isp_rel p1 p2 R
     241      (safe_address_of_xdata_pointer (isp … st1))
     242      (safe_address_of_xdata_pointer (isp … st2)) ∧
     243    sp_rel p1 p2 R
     244      (safe_address_of_xdata_pointer (sp … st1))
     245      (safe_address_of_xdata_pointer (sp … st2)) ∧
     246    carry … st1 = carry … st2 ∧
     247    regs_rel p1 p2 R (regs … st1) (regs … st2) ∧
     248    mem_rel p1 p2 R (m … st1) (m … st2).
     249elim st1 -st1 #st1 ** #good_pc1 #good_sp1 #good_isp1
     250elim st2 -st2 #st2 ** #good_pc2 #good_sp2 #good_isp2
     251assumption
     252qed.
     253 elim st2
     254-st1 -st2 #st2 ** #good_pc2 # ∧
     255    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
     256    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
     257    frames_rel … R (st_frms … st1) (st_frms … st2) ∧
     258
     259
     260
Note: See TracChangeset for help on using the changeset viewer.