Ignore:
Timestamp:
Jun 26, 2013, 2:22:28 PM (6 years ago)
Author:
piccolo
Message:

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2808 r3371  
    1818include "joint/semanticsUtils.ma".
    1919include "common/ExtraMonads.ma".
    20 (*
    21 !!!SPOSTATO IN extraGlobalenvs.ma!!!!
    22 
    23 include alias "common/PositiveMap.ma".
    24 
    25 lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id.
    26 id < (nextfunction ? ge) →
    27 lookup_opt … id (functions ? ge) = None ? →
    28 lookup_opt … id (functions … (add_functs F ge l)) = None ?.
    29 #F #ge #l #id whd in match add_functs; normalize nodelta
    30 elim l -l [ #_ normalize //]
    31 * #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????);
    32 >lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %]
    33 #f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1)
    34 | cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl))
    35 [elim tl [normalize //]
    36 #x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ]
    37 #H2 lapply(transitive_le … H H2) @lt_to_not_eq
    38 qed.
    39 
    40 lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l.
    41 lookup_opt … id (functions ? (\fst gem)) = None ? →
    42 lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?.
    43 #F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H]
    44 ** #x1 #x2 #x3 #tl whd in match add_globals;
    45 normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
    46 cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
    47 normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
    48 #f1 #H3 <(drop_fn_lfn … f1 H3) assumption
    49 qed.
    50 
    51  
    52 lemma globalenv_no_minus_one :
    53  ∀F,V,i,p.
    54   find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?.
    55 #F #V #i #p
    56 whd in match find_funct_ptr; normalize nodelta
    57 whd in match globalenv;
    58 whd in match globalenv_allocmem; normalize nodelta
    59 @add_globals_functions_miss @add_functs_functions_miss normalize //
    60 qed.
    61 *)
    62 
    63 (* !!!spostato in semantics.ma ed aggiunto un include a extraGlobalenvs.ma!!!
    64 
    65 lemma fetch_internal_function_no_minus_one :
    66   ∀F,V,i,p,bl.
    67   block_id (pi1 … bl) = -1 →
    68   fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
    69     bl = Error … [MSG BadFunction].
    70  #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
    71  whd in match fetch_internal_function;
    72   whd in match fetch_function; normalize nodelta
    73   >globalenv_no_minus_one
    74   cases (symbol_for_block ???) normalize //
    75 qed.
    76 
    77 *)
    78 
    79 (*spostato in ExtraMonads.ma
    80 
    81 lemma bind_option_inversion_star:
    82   ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
    83   (∀x.f = Some … x → g x = Some … y → P) →
    84   (! x ← f ; g x = Some … y) → P.
    85 #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.
    86 
    87 interpretation "option bind inversion" 'bind_inversion =
    88   (bind_option_inversion_star ???????).
    89 
    90 lemma bind_inversion_star : ∀X,Y.∀P : Prop.
    91 ∀m : res X.∀f : X → res Y.∀v : Y.
    92 (∀x. m = return x → f x = return v → P) →
    93 ! x ← m ; f x = return v → P.
    94 #X #Y #P #m #f #v #H #G
    95 elim (bind_inversion ????? G) #x * @H qed.
    96 
    97 interpretation "res bind inversion" 'bind_inversion =
    98   (bind_inversion_star ???????).
    99 
    100 lemma IO_bind_inversion:
    101   ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
    102   (∀x.f = return x → g x = return y → P) →
    103   (! x ← f ; g x = return y) → P.
    104 #O #I #A #B #P #f #g #y cases f normalize
    105 [ #o #f #_ #H destruct
    106 | #a #G #H @(G ? (refl …) H)
    107 | #e #_ #H destruct
    108 ] qed.
    109 
    110 interpretation "IO bind inversion" 'bind_inversion =
    111   (IO_bind_inversion ?????????).
    112 
    113 record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
    114   { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop)
    115   ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf))
    116   ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n.
    117       m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) →
    118                   m_frel ?? Q G (m_bind … m f) (m_bind … n g)
    119   ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v
    120   }.
    121 
    122 *)
    123 
    124 (*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
    125   λO,I.mk_MonadFunctRel ??
    126   (λX,Y,F,m,n.∀x.m = return x → n = return F x)
    127   ???.
    128 [ #X #Y #F #x #y whd in ⊢ (??%%→?); #EQ destruct(EQ) %
    129 | #X #Y #Z #W #F #G *
    130   [ #o #f | #u | #e ] #n #H #f #g #K #x
    131   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    132   >(H ? (refl …)) @K @EQ
    133 | #X #Y #P #Q #H #z #w #G #x #EQ >(G … EQ) >H %
    134 ]
    135 qed.*)
    136 
    137 (* spostato in ExtraMonads.ma
    138 definition res_preserve : MonadFunctRel Res Res ≝
    139   mk_MonadFunctRel ??
    140   (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
    141   ???.
    142 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    143 | #X #Y #Z #W #P #Q #F #G *
    144   [ #u | #e ] #n #H #f #g #K #x
    145   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    146   cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
    147 | #X #Y #P #F #G #H #u #v #K #x #EQ
    148   cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
    149 ]
    150 qed.
    151 
    152 definition opt_preserve : MonadFunctRel Option Option ≝
    153   mk_MonadFunctRel ??
    154   (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
    155   ???.
    156 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    157 | #X #Y #Z #W #P #Q #F #G *
    158   [ | #u ] #n #H #f #g #K #x
    159   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    160   cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
    161 | #X #Y #P #F #G #H #u #v #K #x #EQ
    162   cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
    163 ]
    164 qed.
    165 
    166 definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
    167   λO,I.mk_MonadFunctRel ??
    168   (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
    169   ???.
    170 [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
    171 | #X #Y #Z #W #P #Q #F #G *
    172   [ #o #f | #u | #e ] #n #H #f #g #K #x
    173   whd in ⊢ (??%%→?); #EQ destruct(EQ)
    174   cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
    175 | #X #Y #P #F #G #H #u #v #K #x #EQ
    176   cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
    177 ]
    178 qed.
    179 
    180 definition preserving ≝
    181   λM1,M2.λFR : MonadFunctRel M1 M2.
    182   λX,Y,A,B : Type[0].
    183   λP : X → Prop.
    184   λQ : A → Prop.
    185   λF : ∀x : X.P x → Y.
    186   λG : ∀a : A.Q a → B.
    187   λf : X → M1 A.
    188   λg : Y → M2 B.
    189   ∀x,prf.
    190   FR … G
    191     (f x) (g (F x prf)).
    192 
    193 definition preserving2 ≝
    194   λM1,M2.λFR : MonadFunctRel M1 M2.
    195   λX,Y,Z,W,A,B : Type[0].
    196   λP : X → Prop.
    197   λQ : Y → Prop.
    198   λR : A → Prop.
    199   λF : ∀x : X.P x → Z.
    200   λG : ∀y : Y.Q y → W.
    201   λH : ∀a : A.R a → B.
    202   λf : X → Y → M1 A.
    203   λg : Z → W → M2 B.
    204   ∀x,y,prf1,prf2.
    205   FR … H
    206     (f x y) (g (F x prf1) (G y prf2)).
    207 *)
     20
     21check mk_sem_graph_params
    20822
    20923definition graph_prog_params ≝
    210 λp,p',prog,stack_sizes.
    211 mk_prog_params (mk_sem_graph_params p p') prog stack_sizes.
     24λp,p',pre_main,prog,stack_sizes.
     25mk_prog_params (mk_sem_graph_params p p' pre_main) prog stack_sizes.
     26
     27check mk_sem_graph_params
    21228
    21329definition graph_abstract_status:
    214  ∀p:unserialized_params.
     30 ∀p:uns_params.
    21531  (∀F.sem_unserialized_params p F) →
     32   (∀prog : joint_program (mk_graph_params p).
     33    joint_closed_internal_function (mk_graph_params p) (prog_names … prog)) →
    21634    ∀prog : joint_program (mk_graph_params p).
    21735  (ident → option ℕ) →
    21836     abstract_status
    219  ≝
    220  λp,p',prog,stack_sizes.
    221  joint_abstract_status (graph_prog_params ? p' prog stack_sizes).
     37 ≝ 
     38 λp,p',pre_main,prog,stack_sizes.
     39 joint_abstract_status (graph_prog_params ? p' pre_main prog stack_sizes).
    22240
    22341definition lin_prog_params ≝
    224 λp,p',prog,stack_sizes.
    225 mk_prog_params (mk_sem_lin_params p p') prog stack_sizes.
     42λp,p',pre_main,prog,stack_sizes.
     43mk_prog_params (mk_sem_lin_params p p' pre_main) prog stack_sizes.
    22644
    22745definition lin_abstract_status:
    228  ∀p:unserialized_params.
     46 ∀p:uns_params.
    22947  (∀F.sem_unserialized_params p F) →
     48  (∀prog : joint_program (mk_lin_params p).
     49    joint_closed_internal_function (mk_lin_params p) (prog_names … prog)) →
    23050    ∀prog : joint_program (mk_lin_params p).
    23151  (ident → option ℕ) →
    23252     abstract_status
    23353 ≝
    234  λp,p',prog,stack_sizes.
    235  joint_abstract_status (lin_prog_params ? p' prog stack_sizes).
     54 λp,p',pre_main,prog,stack_sizes.
     55 joint_abstract_status (lin_prog_params ? p' pre_main prog stack_sizes).
    23656
    23757(*
Note: See TracChangeset for help on using the changeset viewer.