Changeset 2570


Ignore:
Timestamp:
Jan 5, 2013, 1:41:13 PM (7 years ago)
Author:
piccolo
Message:

ERTLtoERTLptr in place

Location:
src
Files:
2 added
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2566 r2570  
    1717include "joint/TranslateUtils.ma".
    1818
     19definition translate_step_seq :
     20∀globals.(joint_seq ERTL globals) → (joint_seq ERTLptr globals) ≝
     21λglobals,s.
     22match s with
     23[COMMENT s ⇒ COMMENT ERTLptr … s
     24|COST_LABEL c ⇒ COST_LABEL ERTLptr … c
     25|MOVE a  ⇒ MOVE ERTLptr … a
     26|POP a ⇒ POP ERTLptr … a
     27|PUSH a ⇒ PUSH ERTLptr … a
     28|ADDRESS i H reg1 reg2 ⇒ ADDRESS ERTLptr … i H reg1 reg2
     29|OPACCS op reg1 reg2 reg3 reg4 ⇒ OPACCS ERTLptr … op reg1 reg2 reg3 reg4
     30|OP1 op reg1 reg2 ⇒ OP1 ERTLptr … op reg1 reg2
     31|OP2 op reg1 reg2 arg ⇒ OP2 ERTLptr … op reg1 reg2 arg
     32|CLEAR_CARRY ⇒ CLEAR_CARRY ERTLptr ?
     33|SET_CARRY ⇒ SET_CARRY ERTLptr ?
     34|LOAD reg1 reg2 reg3 ⇒ LOAD ERTLptr … reg1 reg2 reg3
     35|STORE arg1 arg2 reg ⇒ STORE ERTLptr … arg1 arg2 reg
     36|extension_seq s ⇒ extension_seq ERTLptr … (ertlptr_ertl s)
     37].
     38
     39
    1940(* PAOLO: implement the b_graph_translate2 that expects functions that
    2041   return not (list instr * instr) but (list (label → instr) * instr) *)
     
    2445  →joint_step ERTL globals
    2546   →bind_seq_block ERTLptr globals (joint_step ERTLptr globals) ≝
    26  λglobals.λl.λs.?.
    27 cases s
    28 [ #called #args #dest cases called
    29   [ (*#_*) #id % %{[]} %1 [%1{id}] assumption
    30   | (*#pc*) #dest1 %2 #reg %1 @(〈[?;?;?;?], ?〉)
    31     [ @extension_seq @(LOW_ADDRESS reg ?(*pc*)) cases daemon
    32     | @(PUSH … (Reg … reg))
    33     | @extension_seq @(HIGH_ADDRESS reg ?(*pc*)) cases daemon
    34     | @(PUSH … (Reg … reg))
    35     | %1 [%2{dest1}] assumption
    36     ]]
    37 | (*#_*) #reg #l %{[]} %2 assumption
    38 | (*#_*) #X %1 %{[]} %3 cases X
    39   try (#a #b #c #d #e) try (#a #b #c #d) try (#a #b #c) try (#a #b) try #a
    40   [%1|%2|%3|%4|%5|%6|%7|%8|%9|%10|%11|%12|%13|%14] try assumption
    41   %1 @a ]
    42 qed.
     47 λglobals.λl.λs.
     48match s with
     49[ CALL called args dest ⇒
     50    match called with
     51    [inl id ⇒ bret … 〈[ ],CALL ERTLptr ? (inl … id) args dest〉
     52    |inr dest1 ⇒ νreg in bret … 〈[extension_seq ERTLptr ? (LOW_ADDRESS reg ?);
     53                                  PUSH … (Reg … reg);
     54                                  extension_seq ERTLptr ? (HIGH_ADDRESS reg ?);
     55                                  PUSH … (Reg … reg)],CALL ERTLptr ? (inr … dest1) args dest〉
     56    ]
     57| COND reg l ⇒ bret … 〈[],COND ERTLptr ? reg l〉
     58| step_seq x ⇒ bret … 〈[],step_seq ERTLptr ? (translate_step_seq … x)〉
     59].
     60cases daemon (*TO BE COMPLETED *)
     61qed.
    4362
    44 definition joint_fin_step_id: joint_fin_step ERTL → joint_fin_step ERTLptr.
    45  * [#l %1 @l | %2 | #H #arg #arg' %3 assumption ]
    46 qed.
     63definition joint_fin_step_id: joint_fin_step ERTL → joint_fin_step ERTLptr ≝
     64λs.
     65match s with
     66[GOTO l ⇒ GOTO ERTLptr … l
     67|RETURN  ⇒ RETURN ERTLptr
     68|TAILCALL H arg arg' ⇒ TAILCALL ERTLptr … H arg arg'
     69].
     70
    4771
    4872(*CSC: cut&paste from RTLtoERTL up to ERTLptr :-( keep just one copy*)
  • src/common/extraGlobalenvs.ma

    r2478 r2570  
    193193>(find_funct_ptr_transf … EQfunct) #EQ'' destruct %
    194194qed.
     195
     196
     197include alias "common/PositiveMap.ma".
     198
     199lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id.
     200id < (nextfunction ? ge) →
     201lookup_opt … id (functions ? ge) = None ? →
     202lookup_opt … id (functions … (add_functs F ge l)) = None ?.
     203#F #ge #l #id whd in match add_functs; normalize nodelta
     204elim l -l [ #_ normalize //]
     205* #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????);
     206>lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %]
     207#f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1)
     208| cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl))
     209[elim tl [normalize //]
     210#x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ]
     211#H2 lapply(transitive_le … H H2) @lt_to_not_eq
     212qed.
     213
     214lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l.
     215lookup_opt … id (functions ? (\fst gem)) = None ? →
     216lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?.
     217#F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H]
     218** #x1 #x2 #x3 #tl whd in match add_globals;
     219normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
     220cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
     221normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
     222#f1 #H3 <(drop_fn_lfn … f1 H3) assumption
     223qed.
     224
     225 
     226lemma globalenv_no_minus_one :
     227 ∀F,V,i,p.
     228  find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?.
     229#F #V #i #p
     230whd in match find_funct_ptr; normalize nodelta
     231whd in match globalenv;
     232whd in match globalenv_allocmem; normalize nodelta
     233@add_globals_functions_miss @add_functs_functions_miss normalize //
     234qed.
     235
     236
     237
  • src/joint/linearise.ma

    r2562 r2570  
    591591qed.
    592592
     593(* spostato in ExtraMonads.ma
    593594lemma option_bind_inverse : ∀A,B.∀m : option A.∀f : A → option B.∀r.
    594595  ! x ← m ; f x = return r →
     
    597598%{x} %{EQ} %
    598599qed.
     600*)
    599601
    600602lemma nth_opt_reverse_hit :
  • src/joint/lineariseProof.ma

    r2559 r2570  
    1717include "joint/Traces.ma".
    1818include "joint/semanticsUtils.ma".
     19include "common/ExtraMonads.ma".
     20(*
     21!!!SPOSTATO IN extraGlobalenvs.ma!!!!
    1922
    2023include alias "common/PositiveMap.ma".
     
    5659@add_globals_functions_miss @add_functs_functions_miss normalize //
    5760qed.
     61*)
     62
     63(* !!!spostato in semantics.ma ed aggiunto un include a extraGlobalenvs.ma!!!
    5864
    5965lemma fetch_internal_function_no_minus_one :
     
    6874  cases (symbol_for_block ???) normalize //
    6975qed.
    70    
     76
     77*)
     78
     79(*spostato in ExtraMonads.ma
     80
    7181lemma bind_option_inversion_star:
    7282  ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
     
    109119  ; 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
    110120  }.
     121
     122*)
    111123
    112124(*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
     
    123135qed.*)
    124136
     137(* spostato in ExtraMonads.ma
    125138definition res_preserve : MonadFunctRel Res Res ≝
    126139  mk_MonadFunctRel ??
     
    192205  FR … H
    193206    (f x y) (g (F x prf1) (G y prf2)).
     207*)
    194208
    195209definition graph_prog_params ≝
     
    340354@opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed.
    341355
     356(* spostato in ExtraMonads.ma
     357
    342358lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
    343359#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     
    351367lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
    352368#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
     369*)
    353370
    354371lemma sigma_is_pop_commute :
     
    449466      ∀z.contents bc1 z = contents bc2 z) →
    450467  nextblock m1 = nextblock m2 → m1 = m2.
     468(* spostato in ExtraMonads.ma
    451469
    452470lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
    453471#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     472*)
    454473
    455474lemma beloadv_sigma_commute:
     
    705724λp,graph_prog,f.«f, if_propagate … (pi2 … f)».
    706725*)
     726
     727(* spostato in ExtraMonads.ma
     728
    707729lemma m_list_map_All_ok :
    708730  ∀M : MonadProps.∀X,Y,f,l.
     
    717739    @m_return_bind
    718740qed.
     741*)
    719742
    720743definition helper_def_store__commute :
     
    15571580qed.
    15581581
     1582(*
     1583spostato in ExtraMonads.ma
    15591584
    15601585lemma res_eq_from_opt : ∀A,m,a.
     
    15711596]
    15721597qed.
    1573 
     1598*)
    15741599lemma sigma_pc_exit :
    15751600  ∀p,p',graph_prog,sigma,pc,prf.
     
    19862011%{H5} %{H3} %{H2} @H1
    19872012qed.
    1988 
     2013(* spostato in ExtraMonads.ma
    19892014lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
    19902015       opt_preserve X Y P F m n →
     
    20062031>EQ %
    20072032qed.
    2008 
     2033*)
    20092034lemma eval_seq_no_pc_sigma_commute :
    20102035 ∀p,p',graph_prog.
  • src/joint/semantics.ma

    r2564 r2570  
    55include "joint/Joint.ma".
    66include "ASM/I8051bis.ma".
    7 (* include "common/extraGlobalenvs.ma". *)
     7include "common/extraGlobalenvs.ma".
    88
    99(* CSC: external functions never fail (??) and always return something of the
     
    151151 | _ ⇒ Error … [MSG BadFunction]
    152152 ].
     153 
     154lemma fetch_internal_function_no_minus_one :
     155  ∀F,V,i,p,bl.
     156  block_id (pi1 … bl) = -1 →
     157  fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
     158    bl = Error … [MSG BadFunction].
     159 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     160 whd in match fetch_internal_function;
     161  whd in match fetch_function; normalize nodelta
     162  >globalenv_no_minus_one
     163  cases (symbol_for_block ???) normalize //
     164qed.
    153165
    154166inductive call_kind : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.