Changeset 1882 for src/RTLabs


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

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1644 r1882  
    2828definition local_env ≝ identifier_map RegisterTag (list register).
    2929
    30 definition mem_local_env : register → local_env → bool ≝
    31   λr,e. member … e r.
    32 
    33 definition add_local_env : register → list register → local_env → local_env ≝
    34   λr,v,e. add … e r v.
    35 
    36 definition find_local_env : register → local_env → list register ≝
    37   λr: register.λenv. lookup_def … env r [].
     30definition local_env_typed :
     31  list (register × typ) → local_env → Prop ≝
     32  λl,env.All ?
     33    (λp.let 〈r, ty〉 ≝ p in ∃regs.lookup … env r = Some ? regs ∧
     34                                 |regs| = size_of_sig_type ty) l.
     35
     36definition find_local_env ≝ λr.λlenv : local_env.
     37  λprf : r ∈ lenv.opt_safe … (lookup … lenv r) ?.
     38lapply (in_map_domain … lenv r)
     39>prf * #x #lookup_eq >lookup_eq % #ABS destruct(ABS)
     40qed.
     41
     42lemma find_local_env_elim : ∀P : list register → Prop.∀r. ∀lenv: local_env.∀prf.
     43  (∀x.lookup … lenv r = Some ? x → P x) → P (find_local_env r lenv prf).
     44#P#r#lenv#prf #H
     45change with (P (opt_safe ???))
     46@opt_safe_elim assumption
     47qed.
    3848
    3949definition find_local_env_arg ≝
    40   λr,lenv. map … Reg (find_local_env r lenv).
     50  λr,lenv,prf. map … Reg (find_local_env r lenv prf).
    4151
    4252let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
     
    4959
    5060definition initialize_local_env_internal ≝
    51   λlenv_runiverse.
     61  λlenv_runiverse : local_env × ?.
    5262  λr_sig.
    5363  let 〈lenv,runiverse〉 ≝ lenv_runiverse in
     
    5565  let size ≝ size_of_sig_type sig in
    5666  let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
    57     〈add_local_env r rs lenv,runiverse〉.
     67    〈add … lenv r rs,runiverse〉.
    5868
    5969definition initialize_local_env ≝
     
    7080
    7181definition map_list_local_env_internal ≝
    72   λlenv,res,r. res @ (find_local_env r lenv).
     82  λlenv,res,r_sig. res @ (find_local_env (pi1 … r_sig) lenv (pi2 … r_sig)).
    7383   
    7484definition map_list_local_env ≝
     
    8090  λprf: 2 = length A lst.
    8191  match lst return λx. 2 = |x| → A × A with
    82   [ nil ⇒ λlst_nil_prf. ?
     92  [ nil ⇒ λlst_nil_prf.
    8393  | cons hd tl ⇒ λprf.
    8494    match tl return λx. 1 = |x| → A × A with
    85     [ nil ⇒ λtl_nil_prf. ?
     95    [ nil ⇒ λtl_nil_prf.
    8696    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
    8797    ] ?
     
    98108
    99109definition find_and_addr ≝
    100   λr,lenv. make_addr ? (find_local_env r lenv).
     110  λr,lenv,prf. make_addr ? (find_local_env r lenv prf).
    101111
    102112definition rtl_args ≝
    103   λregs_list,lenv. flatten … (map … (λr.find_local_env_arg r lenv) regs_list).
     113  λlenv,regs_list. flatten … (map … (λr.find_local_env_arg (pi1 … r) lenv (pi2 … r)) regs_list).
    104114
    105115definition split_into_bytes:
     
    119129qed.
    120130
    121 
    122 lemma eqb_implies_eq:
    123   ∀m, n: nat.
    124     eqb m n = true → m = n.
    125     #m#n@eqb_elim // #_ #F destruct(F) qed.
    126 
    127131definition translate_op:
    128132  ∀globals. Op2 →
     
    131135  ∀srcrs2 : list rtl_argument.
    132136  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
    133   list (rtl_instruction globals)
     137  list (rtl_step globals)
    134138   ≝
    135139  λglobals: list ident.
     
    140144  λprf1,prf2.
    141145  let f_add ≝ OP2 rtl_params globals in
    142   let res : list (rtl_instruction globals) ≝
     146  let res : list (rtl_step globals) ≝
    143147    map3 ???? (f_add op) destrs srcrs1 srcrs2 ?? in
    144148  (* first, clear carry if op relies on it *)
     
    151155  (* if adding, we use a first Add op, that clear the carry, and then Addc's *)
    152156  [ Add ⇒
    153     match destrs return λx.|destrs| = |x| → list (rtl_instruction globals) with
     157    match destrs return λx.|destrs| = |x| → list (rtl_step globals) with
    154158    [ nil ⇒ λeq_destrs.[ ]
    155159    | cons destr destrs' ⇒ λeq_destrs.
    156       match srcrs1 return λy.|srcrs1| = |y| → list (rtl_instruction globals) with
     160      match srcrs1 return λy.|srcrs1| = |y| → list (rtl_step globals) with
    157161      [ nil ⇒ λeq_srcrs1.⊥
    158162      | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
    159         match srcrs2 return λz.|srcrs2| = |z| → list (rtl_instruction globals) with
     163        match srcrs2 return λz.|srcrs2| = |z| → list (rtl_step globals) with
    160164        [ nil ⇒ λeq_srcrs2.⊥
    161165        | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
     
    196200  | _ ⇒ True
    197201  ].
     202
    198203definition translate_cst :
    199204  ∀globals: list ident.
    200205  ∀cst_sig: Σcst : constant.cst_well_defd globals cst.
    201206  ∀destrs: list register.
    202   |destrs| = size_of_cst cst_sig → list (rtl_instruction globals)
     207  |destrs| = size_of_cst cst_sig → list (rtl_step globals)
    203208 ≝
    204209  λglobals,cst_sig,destrs,prf.
    205   match cst_sig return λy.cst_sig = y → list (rtl_instruction globals) with
     210  match cst_sig return λy.cst_sig = y → list (rtl_step globals) with
    206211  [ mk_Sig cst cst_good ⇒ λeqcst_sig.
    207     match cst return λx.cst = x → list (rtl_instruction globals)
     212    match cst return λx.cst = x → list (rtl_step globals)
    208213    with
    209214    [ Ointconst size const ⇒ λeqcst.
     
    218223    | Oaddrstack offset ⇒ λeqcst.
    219224      let 〈r1, r2〉 ≝ make_addr … destrs ? in
    220       [(rtl_st_ext_stack_address r1 r2 : rtl_instruction globals)]
     225      [(rtl_st_ext_stack_address r1 r2 : rtl_step globals)]
    221226    ] (refl …)
    222227  ] (refl …).
     
    235240  ∀destrs: list register.
    236241  ∀srcrs: list rtl_argument.
    237   |destrs| = |srcrs| → list (rtl_instruction globals) ≝
     242  |destrs| = |srcrs| → list (rtl_step globals) ≝
    238243  λglobals,destrs,srcrs,length_eq.
    239244  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
     
    259264qed.
    260265
    261 definition sign_mask : ∀globals.register → register → list (rtl_instruction globals) ≝
     266definition sign_mask : ∀globals.register → register → list (rtl_step globals) ≝
    262267    (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
    263268       byte in destr if srcr is: neg   |  pos
     
    275280definition translate_cast_signed :
    276281  ∀globals : list ident.
    277   list register → register → bind_list register unit (rtl_instruction globals) ≝
     282  list register → register → bind_list register (rtl_step globals) ≝
    278283  λglobals,destrs,srcr.
    279284  ν tmp in
     
    283288definition translate_cast_unsigned :
    284289  ∀globals : list ident.
    285   list register → list (rtl_instruction globals) ≝
     290  list register → list (rtl_step globals) ≝
    286291  λglobals,destrs.
    287292  match nat_to_args (|destrs|) 0 with
     
    296301  ∀globals: list ident.
    297302  signedness → list register → list register →
    298     bind_list register unit (rtl_instruction globals) ≝
     303    bind_list register (rtl_step globals) ≝
    299304  λglobals,src_sign,destrs,srcrs.
    300305  match srcrs
    301   return λy. y = srcrs → bind_list register unit (rtl_instruction globals)
     306  return λy. y = srcrs → bind_list register (rtl_step globals)
    302307  with
    303308  [ nil ⇒ λ_.translate_cast_unsigned ? destrs (* srcrs = [ ] ⇒ we fill with 0 *)
     
    306311    [ mk_Sig crl len_proof ⇒
    307312      (* move prefix of srcrs in destrs *)
    308       translate_move ? (\fst (\fst crl)) (map … Reg (\fst (\snd crl))) ? @
    309       match \snd (\snd crl) with
     313      translate_move ? (\fst (\fst crl)) (map … Reg (\fst (\snd crl))) ? @@
     314      match \snd (\snd crl) return λ_.bind_list ?? with
    310315      [ nil ⇒
    311         match src_sign return λ_.bind_list register unit (rtl_instruction globals) with
     316        match src_sign return λ_.bind_list register (rtl_step globals) with
    312317        [ Unsigned ⇒ translate_cast_unsigned ? (\snd (\fst crl))
    313318        | Signed ⇒
     
    326331  ∀destrs : list register.
    327332  ∀srcrs_arg : list register.
    328   |destrs| = |srcrs_arg| → list (rtl_instruction globals) ≝
     333  |destrs| = |srcrs_arg| → list (rtl_step globals) ≝
    329334  λglobals, destrs, srcrs, prf.
    330335  map2 ??? (OP1 rtl_params globals Cmpl) destrs srcrs prf.
    331336
    332 
    333 definition translate_negint : ∀globals.? → ? → ? → bind_list register unit (rtl_instruction globals) ≝
     337definition translate_negint : ∀globals.? → ? → ? → bind_list register (rtl_step globals) ≝
    334338  λglobals: list ident.
    335339  λdestrs: list register.
     
    346350  ∀globals : list ident.
    347351  list register → list register →
    348     bind_list register unit (rtl_instruction globals) ≝
     352    bind_list register (rtl_step globals) ≝
    349353  λglobals,destrs,srcrs.
    350354  match destrs with
    351355  [ nil ⇒ [ ]
    352356  | cons destr destrs' ⇒
    353     translate_cast_unsigned ? destrs' @ (* fill destrs' with 0 *)
     357    translate_cast_unsigned ? destrs' @@ (* fill destrs' with 0 *)
    354358    match srcrs with
    355359    [ nil ⇒ [destr ← 0]
    356360    | cons srcr srcrs' ⇒
    357       let f : register → rtl_instruction globals ≝
     361      let f : register → rtl_step globals ≝
    358362        λr. destr ← destr .Or. r in
    359       MOVE rtl_params globals 〈destr,srcr〉 ::
    360       map … f srcrs' @
     363      (destr ← srcr) ::: ? ]].
     364      map ?? f srcrs' @@
    361365      (* now destr is non-null iff srcrs was non-null *)
    362366      CLEAR_CARRY ? ? ::
     
    371375
    372376definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
    373   bind_list register unit (rtl_instruction globals) ≝
     377  bind_list register unit (rtl_step globals) ≝
    374378  λglobals.
    375379  λty, ty'.
     
    381385  match op1
    382386  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
    383     bind_list register unit (rtl_instruction globals) with
     387    bind_list register unit (rtl_step globals) with
    384388  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
    385389    translate_cast globals src_sign destrs srcrs
     
    440444  (Σi.i<S k) →
    441445  (* the accumulator *)
    442   list (rtl_instruction globals) →
    443     list (rtl_instruction globals) ≝
     446  list (rtl_step globals) →
     447    list (rtl_step globals) ≝
    444448  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
    445449    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
     
    488492] qed.
    489493
    490 definition translate_mul : ∀globals.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
     494definition translate_mul : ∀globals.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
    491495λglobals : list ident.
    492496λdestrs : list register.
     
    504508(* the step calculating all products with least significant byte going in the
    505509   k-th position of the result *)
    506 let translate_mul_k : (Σk.k<|destrs|) → list (rtl_instruction globals) →
    507   list (rtl_instruction globals) ≝
     510let translate_mul_k : (Σk.k<|destrs|) → list (rtl_step globals) →
     511  list (rtl_step globals) ≝
    508512  λk_sig,acc.match k_sig with
    509513  [ mk_Sig k k_prf ⇒
     
    528532
    529533definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
    530     bind_list register unit (rtl_instruction globals) ≝
     534    bind_list register unit (rtl_step globals) ≝
    531535  λglobals: list ident.
    532536  λdiv_not_mod: bool.
     
    536540  λsrcrs1_prf : |destrs| = |srcrs1|.
    537541  λsrcrs2_prf : |srcrs1| = |srcrs2|.
    538   let return_type ≝ bind_list register unit (rtl_instruction globals) in
     542  let return_type ≝ bind_list register unit (rtl_step globals) in
    539543  match destrs return λx.x = destrs → return_type with
    540544  [ nil ⇒ λ_.[ ]
     
    575579qed.
    576580
    577 definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
     581definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
    578582  λglobals: list ident.
    579583  λdestrs: list register.
     
    582586  λsrcrs1_prf : |destrs| = |srcrs1|.
    583587  λsrcrs2_prf : |srcrs1| = |srcrs2|.
    584   let return_type ≝ bind_list register unit (rtl_instruction globals) in
     588  let return_type ≝ bind_list register unit (rtl_step globals) in
    585589  match destrs return λx.x = destrs → return_type with
    586590  [ nil ⇒ λ_.[ ]
     
    593597      | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
    594598        νtmpr in
    595         let f : rtl_argument → rtl_argument → list (rtl_instruction globals) → list (rtl_instruction globals) ≝
     599        let f : rtl_argument → rtl_argument → list (rtl_step globals) → list (rtl_step globals) ≝
    596600          λs1,s2,acc.
    597601          tmpr  ← s1 .Xor. s2 ::
    598602          destr ← destr .Or. tmpr ::
    599603          acc in
    600         let epilogue : list (rtl_instruction globals) ≝
     604        let epilogue : list (rtl_step globals) ≝
    601605          [ CLEAR_CARRY … ;
    602606            tmpr ← 0 .Sub. destr ;
     
    613617(* if destrs is 0 or 1, it inverses it. To be used after operations that
    614618   ensure this. *)
    615 definition translate_toggle_bool : ∀globals.?→list (rtl_instruction globals) ≝
     619definition translate_toggle_bool : ∀globals.?→list (rtl_step globals) ≝
    616620  λglobals: list ident.
    617621  λdestrs: list register.
     
    628632  |destrs| = |srcrs1| →
    629633  |srcrs1| = |srcrs2| →
    630   list (rtl_instruction globals) ≝
     634  list (rtl_step globals) ≝
    631635  λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
    632636  match destrs with
     
    645649  (tmp : register)
    646650  (srcrs : list rtl_argument) on srcrs :
    647   (list rtl_argument) × (list (rtl_instruction globals)) ≝
     651  (list rtl_argument) × (list (rtl_step globals)) ≝
    648652  match srcrs with
    649653  [ nil ⇒ 〈[ ],[ ]〉
     
    674678  |destrs| = |srcrs1| →
    675679  |srcrs1| = |srcrs2| →
    676   bind_list register unit (rtl_instruction globals) ≝
     680  bind_list register unit (rtl_step globals) ≝
    677681  λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
    678682  νtmp_last_s1 in
     
    688692>shift_signed_length [2: >shift_signed_length] assumption qed.
    689693
    690 definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
     694definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
    691695  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf.
    692696  if is_unsigned then
     
    717721 
    718722definition translate_op2 :
    719   ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝
     723  ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_step globals) ≝
    720724  λglobals: list ident.
    721725  λop2.
     
    758762  cases not_implemented (* XXX: yes, really *) qed.
    759763
    760 definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_instruction globals) ≝
     764definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_step globals) ≝
    761765  λglobals: list ident.
    762766  λsrcrs: list register.
     
    766770  | cons srcr srcrs' ⇒
    767771    ν tmpr in
    768     let f : register → rtl_instruction globals ≝
     772    let f : register → rtl_step globals ≝
    769773      λr. tmpr ← tmpr .Or. r in
    770774    MOVE rtl_params globals 〈tmpr,srcr〉 ::
     
    781785  ν tmp_addr_l in
    782786  ν tmp_addr_h in
    783   let f ≝ λdestr : register.λacc : list (rtl_instruction globals).
     787  let f ≝ λdestr : register.λacc : list (rtl_step globals).
    784788    LOAD rtl_params globals destr (Reg tmp_addr_l) (Reg tmp_addr_h) ::
    785789    translate_op … Add
     
    798802  ν tmp_addr_l in
    799803  ν tmp_addr_h in
    800   let f ≝ λsrcr : rtl_argument.λacc : list (rtl_instruction globals).
     804  let f ≝ λsrcr : rtl_argument.λacc : list (rtl_step globals).
    801805    STORE rtl_params globals (Reg tmp_addr_l) (Reg tmp_addr_h) srcr ::
    802806    translate_op … Add
     
    822826
    823827definition translate_inst : ∀globals.?→?→?→
    824   (bind_list register unit (rtl_instruction globals)) × label ≝
     828  (bind_list register unit (rtl_step globals)) × label ≝
    825829  λglobals: list ident.
    826830  λlenv: local_env.
    827831  λstmt.
     832  λstmt_typed :
    828833  λstmt_prf : stmt_not_final stmt.
    829834  match stmt return λx.stmt = x →
    830     (bind_list register unit (rtl_instruction globals)) × label with
     835    (bind_list register unit (rtl_step globals)) × label with
    831836  [ St_skip lbl' ⇒ λ_.
    832837    〈[ ], lbl'〉
     
    865870    (* Paolo: no notation to avoid ambiguity *)
    866871    〈bcons … (
    867       match retr return λ_.rtl_instruction globals with
     872      match retr return λ_.rtl_step globals with
    868873      [ Some retr ⇒
    869874        rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv)
  • src/RTLabs/semantics.ma

    r1880 r1882  
    124124      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    125125      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    126       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     126      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    127127      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
    128128  | St_call_ptr frs args dst l ⇒ λH.
    129129      ! fv ← reg_retrieve (locals f) frs;
    130130      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    131       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     131      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    132132      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
    133133(*
     
    135135      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    136136      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    137       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     137      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    138138      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    139139  | St_tailcall_ptr frs args ⇒ λH.
    140140      ! fv ← reg_retrieve (locals f) frs;
    141141      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    142       ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     142      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    143143      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    144144*)
Note: See TracChangeset for help on using the changeset viewer.