[2601] | 1 | include "RTLabs/RTLabs_syntax.ma". |
---|
[789] | 2 | include "RTL/RTL.ma". |
---|
[1071] | 3 | include "common/FrontEndOps.ma". |
---|
[789] | 4 | include "common/Graphs.ma". |
---|
[1280] | 5 | include "joint/TranslateUtils.ma". |
---|
[1352] | 6 | include alias "ASM/BitVector.ma". |
---|
| 7 | include alias "arithmetics/nat.ma". |
---|
[789] | 8 | |
---|
[1053] | 9 | definition size_of_sig_type ≝ |
---|
[1052] | 10 | λsig. |
---|
| 11 | match sig with |
---|
[1047] | 12 | [ ASTint isize sign ⇒ |
---|
[2286] | 13 | match isize with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ] |
---|
| 14 | | ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *) |
---|
[1047] | 15 | ]. |
---|
| 16 | |
---|
[789] | 17 | inductive register_type: Type[0] ≝ |
---|
| 18 | | register_int: register → register_type |
---|
| 19 | | register_ptr: register → register → register_type. |
---|
| 20 | |
---|
[1515] | 21 | definition local_env ≝ identifier_map RegisterTag (list register). |
---|
[789] | 22 | |
---|
[2286] | 23 | definition local_env_typed : |
---|
| 24 | list (register × typ) → local_env → Prop ≝ |
---|
| 25 | λl,env.All ? |
---|
| 26 | (λp.let 〈r, ty〉 ≝ p in ∃regs.lookup … env r = Some ? regs ∧ |
---|
| 27 | |regs| = size_of_sig_type ty) l. |
---|
[1052] | 28 | |
---|
[2286] | 29 | definition find_local_env ≝ λr.λlenv : local_env. |
---|
| 30 | λprf : r ∈ lenv.opt_safe … (lookup … lenv r) ?. |
---|
| 31 | lapply (in_map_domain … lenv r) |
---|
| 32 | >prf * #x #lookup_eq >lookup_eq % #ABS destruct(ABS) |
---|
| 33 | qed. |
---|
[1052] | 34 | |
---|
[2286] | 35 | lemma find_local_env_elim : ∀P : list register → Prop.∀r. ∀lenv: local_env.∀prf. |
---|
| 36 | (∀x.lookup … lenv r = Some ? x → P x) → P (find_local_env r lenv prf). |
---|
| 37 | #P#r#lenv#prf #H |
---|
| 38 | change with (P (opt_safe ???)) |
---|
| 39 | @opt_safe_elim assumption |
---|
| 40 | qed. |
---|
[1052] | 41 | |
---|
[2286] | 42 | definition find_local_env_arg : register → local_env → ? → list psd_argument ≝ |
---|
| 43 | λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf). |
---|
| 44 | |
---|
[2640] | 45 | (* move *) |
---|
| 46 | let rec m_iter (M : Monad) X (f : X → M X) (n : ℕ) (m : M X) on n : M X ≝ |
---|
| 47 | match n with |
---|
| 48 | [ O ⇒ m |
---|
| 49 | | S k ⇒ |
---|
| 50 | ! v ← m ; |
---|
| 51 | m_iter … f k (f v) |
---|
| 52 | ]. |
---|
[789] | 53 | |
---|
[2640] | 54 | definition fresh_registers : ∀p,g.ℕ → state_monad (joint_internal_function p g) (list register) ≝ |
---|
| 55 | λp,g,n. |
---|
| 56 | let f ≝ λacc.! m ← fresh_register … ; return (m :: acc) in |
---|
| 57 | m_iter … f n (return [ ]). |
---|
| 58 | |
---|
[2286] | 59 | include alias "common/Identifiers.ma". |
---|
| 60 | let rec map_list_local_env |
---|
| 61 | lenv (regs : list (register×typ)) on regs : |
---|
| 62 | All ? (λpr.bool_to_Prop (\fst pr ∈ lenv)) regs → list register ≝ |
---|
| 63 | match regs return λx.All ?? x → ? with |
---|
| 64 | [ nil ⇒ λ_.[ ] |
---|
| 65 | | cons hd tl ⇒ λprf.find_local_env (\fst hd) lenv ? @ map_list_local_env lenv tl ? |
---|
| 66 | ].cases prf #A #B assumption qed. |
---|
| 67 | |
---|
| 68 | definition initialize_local_env : |
---|
| 69 | ∀globals. |
---|
| 70 | list (register×typ) → |
---|
[2640] | 71 | state_monad (joint_internal_function RTL globals) local_env ≝ |
---|
| 72 | λglobals,registers. |
---|
| 73 | let f ≝ |
---|
| 74 | λr_sig,lenv. |
---|
| 75 | let 〈r, sig〉 ≝ r_sig in |
---|
| 76 | let size ≝ size_of_sig_type sig in |
---|
| 77 | ! regs ← fresh_registers … size ; |
---|
| 78 | return add … lenv r regs in |
---|
| 79 | m_fold … f registers (empty_map …). |
---|
[2286] | 80 | |
---|
| 81 | lemma initialize_local_env_in : ∀globals,l,def,r. |
---|
| 82 | Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def). |
---|
[2640] | 83 | whd in match initialize_local_env; normalize nodelta #globals |
---|
| 84 | cut (∀l,init,def,r.(Exists ? (λx.\fst x = r) l ∨ bool_to_Prop (r ∈ init)) → |
---|
| 85 | r ∈ \snd (m_fold (state_monad ?) ??? l init def)) |
---|
| 86 | [7: #aux #l #def #r #H @aux %1{H} |*:] |
---|
| 87 | #l elim l -l |
---|
| 88 | [ #init #def #r * [*] #H @H ] |
---|
| 89 | * #hd #sig #tl #IH #init #def #r #H |
---|
| 90 | whd in ⊢ (?(???(???%)?)); normalize nodelta |
---|
| 91 | whd in ⊢ (?(???(???(match % with [ _ ⇒ ?]))?)); |
---|
| 92 | inversion (fresh_registers ????) #def' #regs #EQfresh normalize nodelta |
---|
| 93 | @IH cases H -H [*] #H |
---|
| 94 | [ destruct %2 @mem_set_add_id |
---|
| 95 | | %1{H} |
---|
| 96 | | %2 >mem_set_add @orb_Prop_r @H |
---|
| 97 | ] |
---|
[2286] | 98 | qed. |
---|
| 99 | |
---|
| 100 | example proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr. |
---|
| 101 | // qed-. |
---|
| 102 | example proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr. |
---|
| 103 | // qed-. |
---|
| 104 | |
---|
| 105 | definition initialize_locals_params_ret : |
---|
| 106 | ∀globals. |
---|
| 107 | (* locals *) list (register×typ) → |
---|
| 108 | (* params *) list (register×typ) → |
---|
| 109 | (* return *) option (register×typ) → |
---|
[2640] | 110 | state_monad (joint_internal_function RTL globals) local_env ≝ |
---|
[2286] | 111 | λglobals,locals,params,ret,def. |
---|
| 112 | let 〈def',lenv〉 as EQ ≝ |
---|
| 113 | initialize_local_env globals |
---|
| 114 | ((match ret with |
---|
| 115 | [ Some r_sig ⇒ [r_sig] |
---|
| 116 | | None ⇒ [ ] |
---|
| 117 | ]) @ locals @ params) def in |
---|
| 118 | let params' ≝ map_list_local_env lenv params ? in |
---|
| 119 | let ret' ≝ match ret return λx.ret = x → ? with |
---|
| 120 | [ Some r_sig ⇒ λprf.find_local_env (\fst r_sig) lenv ? |
---|
| 121 | | None ⇒ λ_.[ ] |
---|
| 122 | ] (refl …) in |
---|
| 123 | let def'' ≝ |
---|
| 124 | mk_joint_internal_function RTL globals |
---|
| 125 | (joint_if_luniverse … def') (joint_if_runiverse … def') ret' |
---|
[2808] | 126 | params' (joint_if_stacksize … def') (joint_if_local_stacksize … def') |
---|
[2640] | 127 | (joint_if_code … def') (joint_if_entry … def') in |
---|
[2286] | 128 | 〈def'', lenv〉. @hide_prf |
---|
| 129 | [ >(proj2_rewrite ????? EQ) |
---|
| 130 | @initialize_local_env_in >prf %1 % |
---|
| 131 | |*: >(proj2_rewrite ????? EQ) |
---|
| 132 | @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr))) |
---|
[2640] | 133 | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params)) |
---|
| 134 | [ #a #H @Exists_append_r @Exists_append_r @H |
---|
| 135 | | elim params [%] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #G %2{G} |
---|
[2286] | 136 | ] |
---|
| 137 | ] |
---|
| 138 | qed. |
---|
[1280] | 139 | |
---|
[1053] | 140 | definition make_addr ≝ |
---|
| 141 | λA. |
---|
| 142 | λlst: list A. |
---|
[2640] | 143 | λprf: 2 = length A lst.〈nth_safe … 0 lst ?, nth_safe … 1 lst ?〉. <prf [%2] %1 |
---|
[2286] | 144 | qed. |
---|
[1050] | 145 | |
---|
[789] | 146 | definition find_and_addr ≝ |
---|
[2286] | 147 | λr,lenv,prf. make_addr ? (find_local_env r lenv prf). |
---|
[789] | 148 | |
---|
[2490] | 149 | definition find_and_addr_arg ≝ |
---|
| 150 | λr,lenv,prf. make_addr ? (find_local_env_arg r lenv prf). |
---|
| 151 | |
---|
[2505] | 152 | (*include alias "common/Identifiers.ma".*) |
---|
[2286] | 153 | let rec rtl_args (args : list register) (env : local_env) on args : |
---|
| 154 | All ? (λr.bool_to_Prop (r∈env)) args → list psd_argument ≝ |
---|
| 155 | match args return λx.All ?? x → ? with |
---|
| 156 | [ nil ⇒ λ_.[ ] |
---|
| 157 | | cons hd tl ⇒ λprf.find_local_env_arg hd env ? @ rtl_args tl env ? |
---|
| 158 | ]. |
---|
| 159 | cases prf #H #G assumption |
---|
| 160 | qed. |
---|
[789] | 161 | |
---|
[2286] | 162 | include alias "basics/lists/list.ma". |
---|
| 163 | let rec vrsplit A (m,n : nat) |
---|
| 164 | on m : Vector A (m*n) → Σs : list (Vector A n).|s| = m ≝ |
---|
| 165 | match m return λx.Vector A (x*n) → Sig (list ?) ? with |
---|
| 166 | [ O ⇒ λv.[ ] |
---|
| 167 | | S k ⇒ λv.let spl ≝ vsplit ? n … v in \fst spl :: vrsplit ? k n (\snd spl) |
---|
| 168 | ]. |
---|
| 169 | [ % |
---|
| 170 | | cases (vrsplit ????) #lst #EQ normalize >EQ % |
---|
| 171 | ] qed. |
---|
[1057] | 172 | |
---|
[1354] | 173 | definition split_into_bytes: |
---|
| 174 | ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝ |
---|
[2866] | 175 | λsize,int.reverse … (vrsplit ? (size_intsize size) 8 int). |
---|
| 176 | >length_reverse @pi2 qed. |
---|
[1308] | 177 | |
---|
[2286] | 178 | let rec list_inject_All_aux A P (l : list A) on l : All A P l → list (Σx.P x) ≝ |
---|
[2640] | 179 | match l return λx.All A P x → list (Σx.P x) with |
---|
[2286] | 180 | [ nil ⇒ λ_.[ ] |
---|
[2640] | 181 | | cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_inject_All_aux A P tl (proj2 … prf) |
---|
| 182 | ]. |
---|
[1308] | 183 | |
---|
[2866] | 184 | definition translate_op_aux: |
---|
| 185 | ∀globals. Op2 → |
---|
| 186 | ∀dests : list register. |
---|
| 187 | ∀srcrs1 : list psd_argument. |
---|
| 188 | ∀srcrs2 : list psd_argument. |
---|
| 189 | |dests| = |srcrs1| → |srcrs1| = |srcrs2| → |
---|
| 190 | list (joint_seq RTL globals) |
---|
| 191 | ≝ |
---|
| 192 | λglobals: list ident. |
---|
| 193 | λop. |
---|
| 194 | λdestrs. |
---|
| 195 | λsrcrs1. |
---|
| 196 | λsrcrs2. |
---|
| 197 | λprf1,prf2. |
---|
| 198 | (* first, clear carry if op relies on it *) |
---|
| 199 | map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2. |
---|
| 200 | |
---|
[2286] | 201 | definition translate_op: |
---|
| 202 | ∀globals. Op2 → |
---|
| 203 | ∀dests : list register. |
---|
| 204 | ∀srcrs1 : list psd_argument. |
---|
| 205 | ∀srcrs2 : list psd_argument. |
---|
| 206 | |dests| = |srcrs1| → |srcrs1| = |srcrs2| → |
---|
[2917] | 207 | list (joint_seq RTL globals) |
---|
[2286] | 208 | ≝ |
---|
[1325] | 209 | λglobals: list ident. |
---|
| 210 | λop. |
---|
[2286] | 211 | λdestrs. |
---|
| 212 | λsrcrs1. |
---|
| 213 | λsrcrs2. |
---|
| 214 | match op with |
---|
[2866] | 215 | [ Add ⇒ |
---|
| 216 | match destrs return λdestrs.|destrs| = |srcrs1| → |srcrs1| = |srcrs2| → ? with |
---|
| 217 | [ nil ⇒ λ_.λ_.[ ] |
---|
| 218 | | cons destr destrs' ⇒ |
---|
| 219 | match srcrs1 return λsrcrs1.S(|destrs'|) = |srcrs1| → |srcrs1| = |srcrs2| → ? with |
---|
| 220 | [ nil ⇒ λprf1.⊥ |
---|
| 221 | | cons srcr1 srcrs1' ⇒ |
---|
| 222 | λprf1. |
---|
| 223 | match srcrs2 return λsrcrs2.S(|srcrs1'|) = |srcrs2| → ? with |
---|
| 224 | [ nil ⇒ λprf2.⊥ |
---|
| 225 | | cons srcr2 srcrs2' ⇒ |
---|
| 226 | λprf2.OP2 ?? Add destr srcr1 srcr2 :: translate_op_aux … Addc destrs' srcrs1' srcrs2' ?? |
---|
| 227 | ] |
---|
| 228 | ] |
---|
| 229 | ] |
---|
| 230 | | Sub ⇒ λprf1,prf2.[ CLEAR_CARRY ?? ] @ translate_op_aux … Sub … prf1 prf2 |
---|
| 231 | | Addc ⇒ λprf1,prf2.[ CLEAR_CARRY ?? ] @ translate_op_aux … Addc … prf1 prf2 |
---|
| 232 | | _ ⇒ translate_op_aux … op destrs srcrs1 srcrs2 |
---|
| 233 | ]. |
---|
| 234 | normalize in prf1 prf2; destruct assumption qed. |
---|
[1325] | 235 | |
---|
[2286] | 236 | definition cast_list : ∀A.A → ℕ → list A → list A ≝ |
---|
| 237 | λA,deflt,new_length,l. |
---|
| 238 | if leb (|l|) new_length then |
---|
| 239 | l @ make_list ? deflt (new_length - |l|) |
---|
| 240 | else |
---|
| 241 | lhd … l new_length. |
---|
[1057] | 242 | |
---|
[2286] | 243 | lemma length_make_list: |
---|
[1060] | 244 | ∀A: Type[0]. |
---|
| 245 | ∀elt: A. |
---|
| 246 | ∀n: nat. |
---|
[2286] | 247 | length ? (make_list A elt n) = n. |
---|
[1060] | 248 | #A #ELT #N |
---|
[2286] | 249 | elim N normalize // qed. |
---|
| 250 | |
---|
| 251 | lemma length_lhd : ∀A,l,n.|lhd A l n| = min (|l|) n. |
---|
| 252 | #A #l elim l -l |
---|
| 253 | [ * // |
---|
| 254 | | #hd #tl #IH * normalize [%] |
---|
| 255 | #n >IH normalize elim (leb ??) % |
---|
| 256 | ] |
---|
[1060] | 257 | qed. |
---|
| 258 | |
---|
[2286] | 259 | lemma length_cast_list : ∀A,dflt,n,l.|cast_list A dflt n l| = n. |
---|
| 260 | #A #dflt #n #l |
---|
| 261 | normalize @leb_elim #H normalize |
---|
| 262 | [ >length_append >length_make_list |
---|
| 263 | @sym_eq @minus_to_plus // |
---|
| 264 | | >length_lhd normalize @leb_elim |
---|
| 265 | [ #abs elim (absurd ? abs H) ] |
---|
| 266 | #_ % |
---|
| 267 | ] |
---|
| 268 | qed. |
---|
[1060] | 269 | |
---|
[2286] | 270 | definition translate_op_asym_unsigned : |
---|
| 271 | ∀globals.Op2 → list register → list psd_argument → list psd_argument → |
---|
[2917] | 272 | list (joint_seq RTL globals) ≝ |
---|
[2286] | 273 | λglobals,op,destrs,srcrs1,srcrs2. |
---|
| 274 | let l ≝ |destrs| in |
---|
| 275 | let srcrs1' ≝ cast_list ? (zero_byte : psd_argument) l srcrs1 in |
---|
| 276 | let srcrs2' ≝ cast_list ? (zero_byte : psd_argument) l srcrs2 in |
---|
| 277 | translate_op globals op destrs srcrs1' srcrs2' ??. |
---|
[2640] | 278 | @hide_prf |
---|
[2286] | 279 | normalize nodelta |
---|
| 280 | >length_cast_list [2: >length_cast_list ] % |
---|
[1060] | 281 | qed. |
---|
| 282 | |
---|
[2866] | 283 | definition zero_args : ∀size.Σl : list psd_argument.|l| = size ≝ |
---|
| 284 | λsize. |
---|
| 285 | «make_list psd_argument (zero_byte) size, length_make_list …». |
---|
[1060] | 286 | |
---|
[2866] | 287 | definition one_args : ∀size.Σl : list psd_argument.|l| = size ≝ |
---|
| 288 | λsize.match size return λsize.Σl : list psd_argument.|l| = size with |
---|
| 289 | [ O ⇒ «[ ], refl …» |
---|
| 290 | | S k ⇒ (byte_of_nat 1 : psd_argument) :: zero_args k |
---|
| 291 | ]. |
---|
| 292 | whd in ⊢ (??%?); @eq_f @pi2 qed. |
---|
| 293 | |
---|
[2286] | 294 | definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with |
---|
| 295 | [ Ointconst size _ _ ⇒ size_intsize size |
---|
| 296 | | _ ⇒ 2 |
---|
[1060] | 297 | ]. |
---|
| 298 | |
---|
[2286] | 299 | definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst. |
---|
| 300 | match cst with |
---|
[2640] | 301 | [ Oaddrsymbol id _ ⇒ bool_to_Prop (id ∈ globals) |
---|
[2286] | 302 | | _ ⇒ True |
---|
[1060] | 303 | ]. |
---|
[2917] | 304 | |
---|
[2286] | 305 | definition translate_cst : |
---|
| 306 | ∀ty. |
---|
| 307 | ∀globals: list ident. |
---|
| 308 | ∀cst_sig: Σcst : constant ty.cst_well_defd ty globals cst. |
---|
| 309 | ∀destrs: list register. |
---|
| 310 | |destrs| = size_of_cst ? cst_sig → |
---|
[2640] | 311 | bind_new register (list (joint_seq RTL globals)) |
---|
[2286] | 312 | ≝ |
---|
| 313 | λty,globals,cst_sig,destrs. |
---|
| 314 | match pi1 … cst_sig in constant return λty'.λx : constant ty'. |
---|
| 315 | cst_well_defd ty' ? x → |destrs| = size_of_cst ty' x → ? |
---|
| 316 | with |
---|
| 317 | [ Ointconst size sign const ⇒ λcst_prf,prf. |
---|
| 318 | map2 … (λr.λb : Byte.r ← b) destrs |
---|
| 319 | (split_into_bytes size const) ? |
---|
| 320 | | Oaddrsymbol id offset ⇒ λcst_prf,prf. |
---|
| 321 | let 〈r1, r2〉 ≝ make_addr … destrs ? in |
---|
[2917] | 322 | ADDRESS RTL globals id ? r1 r2 :: |
---|
| 323 | if eqb offset 0 then [ ] else |
---|
| 324 | translate_op … Add |
---|
| 325 | [r1 ; r2 ] [ r1 ; r2 ] [ byte_of_nat … offset ; zero_byte ] |
---|
| 326 | (refl …) (refl …) |
---|
[2286] | 327 | | Oaddrstack offset ⇒ λcst_prf,prf. |
---|
| 328 | let 〈r1, r2〉 ≝ make_addr … destrs ? in |
---|
[2917] | 329 | (rtl_stack_address r1 r2 : joint_seq RTL globals) :: |
---|
| 330 | if eqb offset 0 then [ ] else |
---|
| 331 | translate_op … Add |
---|
| 332 | [r1 ; r2 ] [ r1 ; r2 ] [ byte_of_nat … offset ; zero_byte ] |
---|
| 333 | (refl …) (refl …) |
---|
[2286] | 334 | ] (pi2 … cst_sig). |
---|
[2640] | 335 | @hide_prf |
---|
[2490] | 336 | [ cases (split_into_bytes ??) #lst |
---|
[2640] | 337 | #EQ >EQ >prf whd in ⊢ (??%?); cases size % |
---|
| 338 | | @cst_prf |
---|
[2286] | 339 | |*: >prf % |
---|
| 340 | ] |
---|
[1066] | 341 | qed. |
---|
[2286] | 342 | |
---|
| 343 | definition translate_move : |
---|
| 344 | ∀globals. |
---|
| 345 | ∀destrs: list register. |
---|
| 346 | ∀srcrs: list psd_argument. |
---|
| 347 | |destrs| = |srcrs| → list (joint_seq RTL globals) ≝ |
---|
| 348 | λglobals,destrs,srcrs,length_eq. |
---|
| 349 | map2 … (λdst,src.dst ← src) destrs srcrs length_eq. |
---|
[1057] | 350 | |
---|
[2286] | 351 | definition sign_mask : ∀globals.register → psd_argument → |
---|
| 352 | list (joint_seq RTL globals) ≝ |
---|
| 353 | (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that: |
---|
| 354 | byte in destr if srcr is: neg | pos |
---|
| 355 | destr ← srcr | 127 11...1 | 01...1 |
---|
| 356 | destr ← destr <rot< 1 1...11 | 1...10 |
---|
| 357 | destr ← INC destr 0....0 | 1....1 |
---|
| 358 | destr ← CPL destr 1....1 | 0....0 |
---|
| 359 | *) |
---|
| 360 | λglobals,destr,srca. |
---|
| 361 | match srca with |
---|
| 362 | [ Reg srcr ⇒ |
---|
| 363 | let byte_127 : Byte ≝ false ::: maximum ? in |
---|
| 364 | [destr ← srcr .Or. byte_127 ; |
---|
| 365 | destr ← .Rl. destr ; |
---|
| 366 | destr ← .Inc. destr ; |
---|
| 367 | destr ← .Cmpl. destr ] |
---|
[2490] | 368 | | Imm b ⇒ |
---|
| 369 | if sign_bit … b then |
---|
| 370 | [ destr ← (maximum … : Byte) ] |
---|
| 371 | else |
---|
| 372 | [ destr ← zero_byte ] |
---|
[1062] | 373 | ]. |
---|
| 374 | |
---|
[2286] | 375 | definition translate_cast_signed : |
---|
| 376 | ∀globals : list ident. |
---|
| 377 | list register → psd_argument → |
---|
[2640] | 378 | bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[2286] | 379 | λglobals,destrs,srca. |
---|
| 380 | ν tmp in |
---|
| 381 | (sign_mask ? tmp srca @ |
---|
| 382 | translate_move ? destrs (make_list ? (Reg ? tmp) (|destrs|)) ?). |
---|
| 383 | >length_make_list % qed. |
---|
[1356] | 384 | |
---|
[2286] | 385 | definition translate_fill_with_zero : |
---|
| 386 | ∀globals : list ident. |
---|
| 387 | list register → list (joint_seq RTL globals) ≝ |
---|
| 388 | λglobals,destrs. |
---|
[2866] | 389 | translate_move ? destrs (zero_args (|destrs|)) ?. |
---|
| 390 | @sym_eq @pi2 qed. |
---|
[1356] | 391 | |
---|
[2286] | 392 | let rec last A (l : list A) on l : option A ≝ |
---|
| 393 | match l with |
---|
| 394 | [ nil ⇒ None ? |
---|
| 395 | | cons hd tl ⇒ |
---|
| 396 | match tl with |
---|
| 397 | [ nil ⇒ Some ? hd |
---|
| 398 | | _ ⇒ last A tl |
---|
| 399 | ] |
---|
| 400 | ]. |
---|
[1356] | 401 | |
---|
[2640] | 402 | lemma last_def : ∀A,hd,tl.last A (hd @ [tl]) = Some ? tl. |
---|
| 403 | #A #hd elim hd -hd [ #tl % ] #hd * [ #_ #last % ] #hd' #tl #IH #last |
---|
| 404 | @IH qed. |
---|
| 405 | |
---|
| 406 | lemma last_not_empty : ∀A,l.not_empty A l → |
---|
[2286] | 407 | match last A l with |
---|
| 408 | [ None ⇒ False |
---|
| 409 | | _ ⇒ True ]. |
---|
[2674] | 410 | #A @list_elim_left [*] #pref #last #_ #_ >last_def % qed. |
---|
[2286] | 411 | |
---|
| 412 | definition translate_op_asym_signed : |
---|
| 413 | ∀globals.Op2 → list register → list psd_argument → list psd_argument → |
---|
[2640] | 414 | bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[2286] | 415 | λglobals,op,destrs,srcrs1,srcrs2. |
---|
| 416 | νtmp1,tmp2 in |
---|
| 417 | let l ≝ |destrs| in |
---|
[2640] | 418 | let cast_srcrs ≝ λsrcrs,tmp. |
---|
[2286] | 419 | let srcrs_l ≝ |srcrs| in |
---|
| 420 | if leb srcrs_l l then |
---|
[2640] | 421 | match last ? srcrs with |
---|
[2286] | 422 | [ Some last ⇒ |
---|
| 423 | 〈srcrs @ make_list … (Reg ? tmp) (l - srcrs_l), |
---|
| 424 | sign_mask … tmp last〉 |
---|
| 425 | | None ⇒ |
---|
| 426 | 〈make_list … (zero_byte : psd_argument) l, [ ]〉 |
---|
[1331] | 427 | ] |
---|
[2286] | 428 | else |
---|
| 429 | 〈lhd … srcrs l, [ ]〉 in |
---|
[2640] | 430 | let prf : ∀srcrs,tmp.|destrs| = |\fst (cast_srcrs srcrs tmp)| ≝ ? in |
---|
| 431 | let srcrs1init ≝ cast_srcrs srcrs1 tmp1 in |
---|
| 432 | let srcrs2init ≝ cast_srcrs srcrs2 tmp2 in |
---|
| 433 | \snd srcrs1init @@ \snd srcrs2init @@ |
---|
[2286] | 434 | translate_op globals op destrs (\fst srcrs1init) (\fst srcrs2init) ??. |
---|
[2640] | 435 | @hide_prf |
---|
[2286] | 436 | [ @prf | <prf @prf ] |
---|
| 437 | #srcrs #tmp normalize nodelta |
---|
| 438 | @leb_elim #H normalize nodelta |
---|
[2640] | 439 | [ cases (last ??) normalize nodelta |
---|
| 440 | [ >length_make_list % |
---|
| 441 | | #_ >length_append >length_make_list |
---|
[2286] | 442 | @minus_to_plus // |
---|
| 443 | ] |
---|
[2640] | 444 | | >length_lhd normalize >(not_le_to_leb_false … H) % |
---|
[2286] | 445 | ] |
---|
[1331] | 446 | qed. |
---|
[1062] | 447 | |
---|
[2286] | 448 | (* using size of lists as size of ints *) |
---|
| 449 | definition translate_cast : |
---|
| 450 | ∀globals: list ident. |
---|
| 451 | signedness → list register → list register → |
---|
[2640] | 452 | bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[2286] | 453 | λglobals,src_sign,destrs,srcrs. |
---|
[2911] | 454 | match reduce_strong ?? srcrs destrs with |
---|
[2286] | 455 | [ mk_Sig t prf ⇒ |
---|
| 456 | let src_common ≝ \fst (\fst t) in |
---|
| 457 | let src_rest ≝ \snd (\fst t) in |
---|
| 458 | let dst_common ≝ \fst (\snd t) in |
---|
| 459 | let dst_rest ≝ \snd (\snd t) in |
---|
| 460 | (* first, move the common part *) |
---|
[2912] | 461 | translate_move ? dst_common (map … (Reg ?) src_common) ? @@ |
---|
[2286] | 462 | match src_rest return λ_.bind_new ?? with |
---|
| 463 | [ nil ⇒ (* upcast *) |
---|
| 464 | match src_sign return λ_.bind_new ?? with |
---|
| 465 | [ Unsigned ⇒ translate_fill_with_zero ? dst_rest |
---|
| 466 | | Signed ⇒ |
---|
| 467 | match last … srcrs (* = src_common *) with |
---|
| 468 | [ Some src_last ⇒ translate_cast_signed ? dst_rest src_last |
---|
| 469 | | None ⇒ (* srcrs is empty *) translate_fill_with_zero ? dst_rest |
---|
| 470 | ] |
---|
| 471 | ] |
---|
| 472 | | _ ⇒ (* downcast, nothing else to do *) [ ] |
---|
[1064] | 473 | ] |
---|
| 474 | ]. |
---|
[2916] | 475 | >length_map >prf % qed. |
---|
[2286] | 476 | |
---|
| 477 | definition translate_notint : |
---|
| 478 | ∀globals : list ident. |
---|
| 479 | ∀destrs : list register. |
---|
| 480 | ∀srcrs_arg : list register. |
---|
| 481 | |destrs| = |srcrs_arg| → list (joint_seq RTL globals) ≝ |
---|
| 482 | λglobals, destrs, srcrs, prf. |
---|
| 483 | map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf. |
---|
[1063] | 484 | |
---|
[2917] | 485 | definition translate_negint : ∀globals.? → ? → ? → list (joint_seq RTL globals) ≝ |
---|
[1287] | 486 | λglobals: list ident. |
---|
[1064] | 487 | λdestrs: list register. |
---|
[2286] | 488 | λsrcrs: list register. |
---|
| 489 | λprf: |destrs| = |srcrs|. (* assert in caml code *) |
---|
[2917] | 490 | translate_notint … destrs srcrs prf @ |
---|
[2866] | 491 | translate_op ? Add destrs (map … (Reg ?) destrs) (one_args (|destrs|)) ??. |
---|
| 492 | @hide_prf |
---|
| 493 | >length_map [ @sym_eq @pi2 | % ] qed. |
---|
[2286] | 494 | |
---|
| 495 | definition translate_notbool: |
---|
| 496 | ∀globals : list ident. |
---|
| 497 | list register → list register → |
---|
[2640] | 498 | bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[2286] | 499 | λglobals,destrs,srcrs. |
---|
[1064] | 500 | match destrs with |
---|
[2286] | 501 | [ nil ⇒ [ ] |
---|
| 502 | | cons destr destrs' ⇒ |
---|
| 503 | translate_fill_with_zero ? destrs' @@ |
---|
| 504 | match srcrs return λ_.bind_new ?? with |
---|
| 505 | [ nil ⇒ [destr ← zero_byte] |
---|
| 506 | | cons srcr srcrs' ⇒ |
---|
| 507 | (destr ← srcr) ::: |
---|
| 508 | map register (joint_seq RTL globals) (λr. destr ← destr .Or. r) srcrs' @@ |
---|
| 509 | (* now destr is non-null iff srcrs was non-null *) |
---|
| 510 | CLEAR_CARRY ?? ::: |
---|
| 511 | (* many uses of 0, better not use immediates *) |
---|
| 512 | ν tmp in |
---|
| 513 | [tmp ← zero_byte ; |
---|
| 514 | destr ← tmp .Sub. tmp ; |
---|
| 515 | (* now carry bit is set iff destr was non-null *) |
---|
| 516 | destr ← tmp .Addc. tmp] |
---|
| 517 | ] |
---|
| 518 | ]. |
---|
| 519 | |
---|
| 520 | definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? → |
---|
[2640] | 521 | bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[2286] | 522 | λglobals. |
---|
| 523 | λty, ty'. |
---|
| 524 | λop1: unary_operation ty ty'. |
---|
| 525 | λdestrs: list register. |
---|
| 526 | λsrcrs: list register. |
---|
| 527 | λprf1: |destrs| = size_of_sig_type ty'. |
---|
| 528 | λprf2: |srcrs| = size_of_sig_type ty. |
---|
| 529 | match op1 |
---|
| 530 | return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' → |
---|
[2640] | 531 | bind_new register (list (joint_seq RTL globals)) with |
---|
[2286] | 532 | [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2. |
---|
| 533 | translate_cast globals src_sign destrs srcrs |
---|
| 534 | | Onegint sz sg ⇒ λeq1,eq2. |
---|
| 535 | translate_negint globals destrs srcrs ? |
---|
| 536 | | Onotbool _ _ _ _ ⇒ λeq1,eq2. |
---|
| 537 | translate_notbool globals destrs srcrs |
---|
| 538 | | Onotint sz sg ⇒ λeq1,eq2. |
---|
| 539 | translate_notint globals destrs srcrs ? |
---|
| 540 | | Optrofint sz sg ⇒ λeq1,eq2. |
---|
| 541 | translate_cast globals Unsigned destrs srcrs |
---|
| 542 | | Ointofptr sz sg ⇒ λeq1,eq2. |
---|
| 543 | translate_cast globals Unsigned destrs srcrs |
---|
| 544 | | Oid t ⇒ λeq1,eq2. |
---|
| 545 | translate_move globals destrs (map … (Reg ?) srcrs) ? |
---|
| 546 | | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *) |
---|
| 547 | ] (refl …) (refl …). |
---|
[2640] | 548 | @hide_prf |
---|
[2490] | 549 | destruct >prf1 >prf2 [3: >length_map ] // |
---|
[1064] | 550 | qed. |
---|
| 551 | |
---|
[2286] | 552 | include alias "arithmetics/nat.ma". |
---|
[1064] | 553 | |
---|
[2286] | 554 | definition translate_mul_i : |
---|
| 555 | ∀globals. |
---|
| 556 | register → register → |
---|
| 557 | (* size of destination and sources *) |
---|
| 558 | ∀n : ℕ. |
---|
| 559 | (* the temporary destination, with a dummy register at the end *) |
---|
| 560 | ∀tmp_destrs_dummy : list register. |
---|
| 561 | ∀srcrs1,srcrs2 : list psd_argument. |
---|
| 562 | |tmp_destrs_dummy| = S n → |
---|
| 563 | n = |srcrs1| → |
---|
| 564 | |srcrs1| = |srcrs2| → |
---|
| 565 | (* the position of the least significant byte of the result we compute at |
---|
| 566 | this stage (goes from 0 to n in the main function) *) |
---|
| 567 | ∀k : ℕ. |
---|
| 568 | lt k n → |
---|
| 569 | (* the position of the byte in the first source we will use in this stage. |
---|
| 570 | the position in the other source will be k - i *) |
---|
| 571 | (Σi.i<S k) → |
---|
| 572 | (* the accumulator *) |
---|
[2917] | 573 | list (joint_seq RTL globals) → |
---|
| 574 | list (joint_seq RTL globals) ≝ |
---|
[2286] | 575 | λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2, |
---|
| 576 | tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc. |
---|
| 577 | (* the following will expand to |
---|
| 578 | a, b ← srcrs1[i] * srcrs2[k-i] |
---|
| 579 | tmp_destrs_dummy[k] ← tmp_destrs_dummy[k] + a |
---|
| 580 | tmp_destrs_dummy[k+1] ← tmp_destrs_dummy[k+1] + b + C |
---|
| 581 | tmp_destrs_dummy[k+2] ← tmp_destrs_dummy[k+2] + 0 + C |
---|
| 582 | ... |
---|
| 583 | tmp_destrs_dummy[n] ← tmp_destrs_dummy[n] + 0 + C |
---|
| 584 | ( all calculations on tmp_destrs_dummy[n] will be eliminated with |
---|
| 585 | liveness analysis) *) |
---|
| 586 | match i_sig with |
---|
| 587 | [ mk_Sig i i_prf ⇒ |
---|
| 588 | (* we pad the result of a byte multiplication with zeros in order |
---|
| 589 | for the bit to be carried. Redundant calculations will be eliminated |
---|
| 590 | by constant propagation. *) |
---|
| 591 | let args : list psd_argument ≝ |
---|
| 592 | [Reg ? a;Reg ? b] @ make_list ? (zero_byte : psd_argument) (n - 1 - k) in |
---|
| 593 | let tmp_destrs_view : list register ≝ |
---|
| 594 | ltl ? tmp_destrs_dummy k in |
---|
[2917] | 595 | [❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?)] @ |
---|
| 596 | translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @ |
---|
[2286] | 597 | acc |
---|
| 598 | ]. |
---|
[2640] | 599 | @hide_prf |
---|
| 600 | [ <srcrs1_prf |
---|
| 601 | @(transitive_le … i_prf k_prf) |
---|
| 602 | | @lt_plus_to_minus [ @le_S_S_to_le assumption | <srcrs2_prf <srcrs1_prf |
---|
[2286] | 603 | whd >(plus_n_O (S k)) @le_plus // ] |
---|
[2640] | 604 | | >length_map % |
---|
[2286] | 605 | | >length_map |
---|
| 606 | >length_ltl |
---|
| 607 | >tmp_destrs_dummy_prf >length_append |
---|
| 608 | >length_make_list |
---|
| 609 | normalize in ⊢ (???(?%?)); |
---|
[2640] | 610 | cases n in k_prf; [ #ABS cases (absurd ? ABS ?) /2 by le_to_not_lt/ ] |
---|
| 611 | #n' #k_prf >minus_S_S <minus_n_O |
---|
| 612 | >plus_minus_commutative [%] @le_S_S_to_le assumption |
---|
[2286] | 613 | ] qed. |
---|
[1064] | 614 | |
---|
[2640] | 615 | definition translate_mul : ∀globals.?→?→?→?→?→bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[2286] | 616 | λglobals : list ident. |
---|
| 617 | λdestrs : list register. |
---|
| 618 | λsrcrs1 : list psd_argument. |
---|
| 619 | λsrcrs2 : list psd_argument. |
---|
| 620 | λsrcrs1_prf : |destrs| = |srcrs1|. |
---|
| 621 | λsrcrs2_prf : |srcrs1| = |srcrs2|. |
---|
| 622 | (* needed fresh registers *) |
---|
| 623 | νa in |
---|
| 624 | νb in |
---|
| 625 | (* temporary registers for the result are created, so to avoid overwriting |
---|
| 626 | sources *) |
---|
| 627 | νν |destrs| as tmp_destrs with tmp_destrs_prf in |
---|
| 628 | νdummy in |
---|
[2946] | 629 | (dummy ← byte_of_nat 0) ::: |
---|
[2286] | 630 | (* the step calculating all products with least significant byte going in the |
---|
| 631 | k-th position of the result *) |
---|
[2917] | 632 | let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) → |
---|
| 633 | list (joint_seq RTL globals) ≝ |
---|
[2286] | 634 | λk_sig,acc.match k_sig with |
---|
| 635 | [ mk_Sig k k_prf ⇒ |
---|
| 636 | foldr … (translate_mul_i ? a b (|destrs|) |
---|
| 637 | (tmp_destrs @ [dummy]) srcrs1 srcrs2 |
---|
| 638 | ? srcrs1_prf srcrs2_prf k k_prf) acc (range_strong (S k)) |
---|
| 639 | ] in |
---|
| 640 | (* initializing tmp_destrs to zero |
---|
| 641 | dummy is intentionally uninitialized *) |
---|
[2917] | 642 | translate_fill_with_zero … tmp_destrs @ |
---|
[2286] | 643 | (* the main body, roughly: |
---|
| 644 | for k in 0 ... n-1 do |
---|
| 645 | for i in 0 ... k do |
---|
| 646 | translate_mul_i … k … i *) |
---|
[2917] | 647 | foldr … translate_mul_k [ ] (range_strong (|destrs|)) @ |
---|
[2286] | 648 | (* epilogue: saving the result *) |
---|
| 649 | translate_move … destrs (map … (Reg ?) tmp_destrs) ?. |
---|
[2640] | 650 | @hide_prf |
---|
[2946] | 651 | [ >length_append <plus_n_Sm <plus_n_O // |
---|
| 652 | | >length_map >tmp_destrs_prf // |
---|
[2286] | 653 | ] |
---|
[1064] | 654 | qed. |
---|
| 655 | |
---|
[2286] | 656 | definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→ |
---|
[2640] | 657 | bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[1287] | 658 | λglobals: list ident. |
---|
[2286] | 659 | λdiv_not_mod: bool. |
---|
[1064] | 660 | λdestrs: list register. |
---|
[2286] | 661 | λsrcrs1: list psd_argument. |
---|
| 662 | λsrcrs2: list psd_argument. |
---|
| 663 | λsrcrs1_prf : |destrs| = |srcrs1|. |
---|
| 664 | λsrcrs2_prf : |srcrs1| = |srcrs2|. |
---|
| 665 | match destrs return λx.x = destrs → bind_new ?? with |
---|
| 666 | [ nil ⇒ λ_.[ ] |
---|
| 667 | | cons destr destrs' ⇒ λeq_destrs. |
---|
| 668 | match destrs' with |
---|
| 669 | [ nil ⇒ |
---|
| 670 | match srcrs1 return λx.x = srcrs1 → bind_new ?? with |
---|
| 671 | [ nil ⇒ λeq_srcrs1.⊥ |
---|
| 672 | | cons srcr1 srcrs1' ⇒ λeq_srcrs1. |
---|
| 673 | match srcrs2 return λx.x = srcrs2 → bind_new ?? with |
---|
| 674 | [ nil ⇒ λeq_srcrs2.⊥ |
---|
| 675 | | cons srcr2 srcrs2' ⇒ λeq_srcrs2. |
---|
| 676 | νdummy in |
---|
| 677 | let 〈destr1, destr2〉 ≝ |
---|
| 678 | if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in |
---|
| 679 | [❮destr1, destr2❯ ← srcr1 .DivuModu. srcr2] |
---|
| 680 | ] (refl …) |
---|
| 681 | ] (refl …) |
---|
| 682 | | _ ⇒ ? (* not implemented *) |
---|
[1064] | 683 | ] |
---|
[2286] | 684 | ] (refl …). |
---|
| 685 | [3: elim not_implemented] |
---|
[2640] | 686 | @hide_prf |
---|
| 687 | destruct normalize in srcrs1_prf srcrs2_prf; destruct qed. |
---|
[2286] | 688 | |
---|
| 689 | (* Paolo: to be moved elsewhere *) |
---|
| 690 | let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B) |
---|
| 691 | (prf : |l1| = |l2|) on l1 : C ≝ |
---|
| 692 | match l1 return λx.x = l1 → C with |
---|
| 693 | [ nil ⇒ λ_.init |
---|
| 694 | | cons a l1' ⇒ λeq_l1. |
---|
| 695 | match l2 return λy.y = l2 → C with |
---|
| 696 | [ nil ⇒ λeq_l2.⊥ |
---|
| 697 | | cons b l2' ⇒ λeq_l2. |
---|
| 698 | f a b (foldr2 A B C f init l1' l2' ?) |
---|
| 699 | ] (refl …) |
---|
| 700 | ] (refl …). |
---|
[2640] | 701 | @hide_prf |
---|
[2286] | 702 | destruct normalize in prf; [destruct|//] |
---|
[1064] | 703 | qed. |
---|
| 704 | |
---|
[2286] | 705 | definition translate_ne: ∀globals: list ident.?→?→?→?→ |
---|
[2640] | 706 | bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[1287] | 707 | λglobals: list ident. |
---|
[2286] | 708 | λdestrs: list register. |
---|
| 709 | λsrcrs1: list psd_argument. |
---|
| 710 | λsrcrs2: list psd_argument. |
---|
| 711 | match destrs return λ_.|srcrs1| = |srcrs2| → bind_new ?? with |
---|
| 712 | [ nil ⇒ λ_.[ ] |
---|
| 713 | | cons destr destrs' ⇒ λEQ. |
---|
| 714 | translate_fill_with_zero … destrs' @@ |
---|
| 715 | match srcrs1 return λx.|x| = |srcrs2| → bind_new ?? with |
---|
| 716 | [ nil ⇒ λ_.[destr ← zero_byte] |
---|
| 717 | | cons srcr1 srcrs1' ⇒ |
---|
| 718 | match srcrs2 return λx.S (|srcrs1'|) = |x| → bind_new ?? with |
---|
| 719 | [ nil ⇒ λEQ.⊥ |
---|
| 720 | | cons srcr2 srcrs2' ⇒ λEQ. |
---|
| 721 | νtmpr in |
---|
| 722 | let f : psd_argument → psd_argument → list (joint_seq RTL globals) → list (joint_seq RTL globals) ≝ |
---|
| 723 | λs1,s2,acc. |
---|
| 724 | tmpr ← s1 .Xor. s2 :: |
---|
| 725 | destr ← destr .Or. tmpr :: |
---|
| 726 | acc in |
---|
| 727 | let epilogue : list (joint_seq RTL globals) ≝ |
---|
| 728 | [ CLEAR_CARRY ?? ; |
---|
| 729 | tmpr ← zero_byte .Sub. destr ; |
---|
| 730 | (* now carry bit is 1 iff destrs != 0 *) |
---|
| 731 | destr ← zero_byte .Addc. zero_byte ] in |
---|
| 732 | destr ← srcr1 .Xor. srcr2 :: |
---|
| 733 | foldr2 ??? f epilogue srcrs1' srcrs2' ? |
---|
| 734 | ] |
---|
| 735 | ] EQ |
---|
[2640] | 736 | ]. |
---|
| 737 | @hide_prf normalize in EQ; destruct(EQ) assumption qed. |
---|
[1064] | 738 | |
---|
[2286] | 739 | (* if destrs is 0 or 1, it inverses it. To be used after operations that |
---|
| 740 | ensure this. *) |
---|
[2640] | 741 | definition translate_toggle_bool : ∀globals.?→bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[1287] | 742 | λglobals: list ident. |
---|
[1064] | 743 | λdestrs: list register. |
---|
[2286] | 744 | match destrs with |
---|
| 745 | [ nil ⇒ [ ] |
---|
[2925] | 746 | | cons destr _ ⇒ [destr ← destr .Xor. byte_of_nat 1] |
---|
[1064] | 747 | ]. |
---|
[2286] | 748 | |
---|
| 749 | definition translate_lt_unsigned : |
---|
| 750 | ∀globals. |
---|
| 751 | ∀destrs: list register. |
---|
| 752 | ∀srcrs1: list psd_argument. |
---|
| 753 | ∀srcrs2: list psd_argument. |
---|
| 754 | |srcrs1| = |srcrs2| → |
---|
[2640] | 755 | bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[2286] | 756 | λglobals,destrs,srcrs1,srcrs2,srcrs_prf. |
---|
| 757 | match destrs with |
---|
| 758 | [ nil ⇒ [ ] |
---|
| 759 | | cons destr destrs' ⇒ |
---|
| 760 | ν tmpr in |
---|
[2640] | 761 | (translate_fill_with_zero … destrs' @@ |
---|
[2286] | 762 | (* I perform a subtraction, but the only interest is in the carry bit *) |
---|
[2640] | 763 | translate_op ? Sub (make_list … tmpr (|srcrs1|)) srcrs1 srcrs2 ? srcrs_prf @@ |
---|
[2286] | 764 | [ destr ← zero_byte .Addc. zero_byte ]) |
---|
| 765 | ]. |
---|
[2640] | 766 | @hide_prf |
---|
[2286] | 767 | >length_make_list % qed. |
---|
[1064] | 768 | |
---|
[2286] | 769 | (* shifts signed integers by adding 128 to the most significant byte |
---|
| 770 | it replaces it with a fresh register which must be provided *) |
---|
| 771 | let rec shift_signed globals |
---|
| 772 | (tmp : register) |
---|
| 773 | (srcrs : list psd_argument) on srcrs : |
---|
| 774 | Σt : (list psd_argument) × (list (joint_seq RTL globals)).|\fst t| = |srcrs| ≝ |
---|
| 775 | let byte_128 : Byte ≝ true ::: bv_zero ? in |
---|
| 776 | match srcrs with |
---|
| 777 | [ nil ⇒ 〈[ ],[ ]〉 |
---|
| 778 | | cons srcr srcrs' ⇒ |
---|
| 779 | match srcrs' with |
---|
| 780 | [ nil ⇒ 〈[ Reg ? tmp ], [ tmp ← srcr .Add. byte_128 ]〉 |
---|
| 781 | | _ ⇒ |
---|
| 782 | let re ≝ shift_signed globals tmp srcrs' in |
---|
| 783 | 〈srcr :: \fst re, \snd re〉 |
---|
[1064] | 784 | ] |
---|
[1066] | 785 | ]. |
---|
[2640] | 786 | @hide_prf |
---|
[2286] | 787 | [1,2: % |
---|
| 788 | |*: cases re * #a #b >p1 normalize #EQ >EQ % |
---|
| 789 | ] qed. |
---|
| 790 | |
---|
| 791 | definition translate_lt_signed : |
---|
| 792 | ∀globals. |
---|
| 793 | ∀destrs: list register. |
---|
| 794 | ∀srcrs1: list psd_argument. |
---|
| 795 | ∀srcrs2: list psd_argument. |
---|
| 796 | |srcrs1| = |srcrs2| → |
---|
[2640] | 797 | bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[2286] | 798 | λglobals,destrs,srcrs1,srcrs2,srcrs_prf. |
---|
| 799 | νtmp_last_s1 in |
---|
| 800 | νtmp_last_s2 in |
---|
| 801 | let p1 ≝ shift_signed globals tmp_last_s1 srcrs1 in |
---|
| 802 | let new_srcrs1 ≝ \fst p1 in |
---|
| 803 | let shift_srcrs1 ≝ \snd p1 in |
---|
| 804 | let p2 ≝ shift_signed globals tmp_last_s2 srcrs2 in |
---|
| 805 | let new_srcrs2 ≝ \fst p2 in |
---|
| 806 | let shift_srcrs2 ≝ \snd p2 in |
---|
| 807 | shift_srcrs1 @@ shift_srcrs2 @@ |
---|
| 808 | translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ?. |
---|
[2640] | 809 | @hide_prf |
---|
[2286] | 810 | whd in match new_srcrs1; whd in match new_srcrs2; |
---|
| 811 | cases p1 |
---|
| 812 | cases p2 |
---|
| 813 | // |
---|
[1066] | 814 | qed. |
---|
| 815 | |
---|
[2640] | 816 | definition translate_lt : bool→∀globals.?→?→?→?→bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[2286] | 817 | λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf. |
---|
| 818 | if is_unsigned then |
---|
| 819 | translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs_prf |
---|
| 820 | else |
---|
| 821 | translate_lt_signed globals destrs srcrs1 srcrs2 srcrs_prf. |
---|
| 822 | |
---|
| 823 | definition translate_cmp ≝ |
---|
| 824 | λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs_prf. |
---|
| 825 | match cmp with |
---|
| 826 | [ Ceq ⇒ |
---|
| 827 | translate_ne globals destrs srcrs1 srcrs2 srcrs_prf @@ |
---|
| 828 | translate_toggle_bool globals destrs |
---|
| 829 | | Cne ⇒ |
---|
| 830 | translate_ne globals destrs srcrs1 srcrs2 srcrs_prf |
---|
| 831 | | Clt ⇒ |
---|
| 832 | translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf |
---|
| 833 | | Cgt ⇒ |
---|
| 834 | translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? |
---|
| 835 | | Cle ⇒ |
---|
| 836 | translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? @@ |
---|
| 837 | translate_toggle_bool globals destrs |
---|
| 838 | | Cge ⇒ |
---|
| 839 | translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf @@ |
---|
| 840 | translate_toggle_bool globals destrs |
---|
[2640] | 841 | ]. @sym_eq assumption qed. |
---|
[2286] | 842 | |
---|
| 843 | definition translate_op2 : |
---|
| 844 | ∀globals.∀ty1,ty2,ty3.∀op : binary_operation ty1 ty2 ty3. |
---|
| 845 | ∀destrs : list register. |
---|
| 846 | ∀srcrs1,srcrs2 : list psd_argument. |
---|
| 847 | |destrs| = size_of_sig_type ty3 → |
---|
| 848 | |srcrs1| = size_of_sig_type ty1 → |
---|
| 849 | |srcrs2| = size_of_sig_type ty2 → |
---|
[2640] | 850 | bind_new register (list (joint_seq RTL globals)) ≝ |
---|
[2286] | 851 | λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2. |
---|
| 852 | match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3. |
---|
| 853 | ? = size_of_sig_type ty3 → ? = size_of_sig_type ty1 → ? = size_of_sig_type ty2 → |
---|
| 854 | bind_new ?? with |
---|
| 855 | [ Oadd sz sg ⇒ λprf1,prf2,prf3. |
---|
| 856 | translate_op globals Add destrs srcrs1 srcrs2 ?? |
---|
[2640] | 857 | | Oaddpi sz ⇒ λprf1,prf2,prf3. |
---|
[2286] | 858 | translate_op_asym_signed globals Add destrs srcrs1 srcrs2 |
---|
[2640] | 859 | | Oaddip sz ⇒ λprf1,prf2,prf3. |
---|
| 860 | translate_op_asym_signed globals Add destrs srcrs2 srcrs1 |
---|
[2286] | 861 | | Osub sz sg ⇒ λprf1,prf2,prf2. |
---|
| 862 | translate_op globals Sub destrs srcrs1 srcrs2 ?? |
---|
| 863 | | Osubpi sz ⇒ λprf1,prf2,prf3. |
---|
| 864 | translate_op_asym_signed globals Add destrs srcrs1 srcrs2 |
---|
| 865 | | Osubpp sz ⇒ λprf1,prf2,prf3. |
---|
| 866 | translate_op_asym_unsigned globals Sub destrs srcrs1 srcrs2 |
---|
| 867 | | Omul sz sg ⇒ λprf1,prf2,prf3. |
---|
| 868 | translate_mul globals destrs srcrs1 srcrs2 ?? |
---|
| 869 | | Odivu sz ⇒ λprf1,prf2,prf3. |
---|
| 870 | translate_divumodu8 globals true destrs srcrs1 srcrs2 ?? |
---|
| 871 | | Omodu sz ⇒ λprf1,prf2,prf3. |
---|
| 872 | translate_divumodu8 globals false destrs srcrs1 srcrs2 ?? |
---|
| 873 | | Oand sz sg ⇒ λprf1,prf2,prf3. |
---|
| 874 | translate_op globals And destrs srcrs1 srcrs2 ?? |
---|
| 875 | | Oor sz sg ⇒ λprf1,prf2,prf3. |
---|
| 876 | translate_op globals Or destrs srcrs1 srcrs2 ?? |
---|
| 877 | | Oxor sz sg ⇒ λprf1,prf2,prf3. |
---|
| 878 | translate_op globals Xor destrs srcrs1 srcrs2 ?? |
---|
| 879 | | Ocmp sz sg1 sg2 c ⇒ λprf1,prf2,prf3. |
---|
| 880 | translate_cmp false globals c destrs srcrs1 srcrs2 ? |
---|
| 881 | | Ocmpu sz sg c ⇒ λprf1,prf2,prf3. |
---|
| 882 | translate_cmp true globals c destrs srcrs1 srcrs2 ? |
---|
| 883 | | Ocmpp sg c ⇒ λprf1,prf2,prf3. |
---|
| 884 | translate_cmp true globals c destrs srcrs1 srcrs2 ? |
---|
| 885 | | _ ⇒ ⊥ (* assert false, implemented in run time or float op *) |
---|
[2640] | 886 | ]. try @not_implemented @hide_prf // |
---|
[2286] | 887 | qed. |
---|
| 888 | |
---|
| 889 | definition translate_cond: ∀globals: list ident. list register → label → |
---|
[2640] | 890 | bind_step_block RTL globals ≝ |
---|
[1288] | 891 | λglobals: list ident. |
---|
[1066] | 892 | λsrcrs: list register. |
---|
| 893 | λlbl_true: label. |
---|
[2640] | 894 | match srcrs return λ_.bind_step_block RTL ? with |
---|
| 895 | [ nil ⇒ bret … [ ] |
---|
[2286] | 896 | | cons srcr srcrs' ⇒ |
---|
| 897 | ν tmpr in |
---|
[2674] | 898 | let f : register → label → joint_seq RTL globals ≝ |
---|
| 899 | λr.λ_. tmpr ← tmpr .Or. r in |
---|
| 900 | bret … |
---|
| 901 | 〈(λ_.MOVE RTL globals 〈tmpr,srcr〉) :: |
---|
| 902 | map ?? f srcrs', |
---|
| 903 | λ_.COND … tmpr lbl_true, [ ]〉 |
---|
[2286] | 904 | ]. |
---|
[1066] | 905 | |
---|
[2286] | 906 | (* Paolo: to be controlled (original seemed overly complex) *) |
---|
[2640] | 907 | definition translate_load : ∀globals.?→?→?→bind_new register ? ≝ |
---|
[1292] | 908 | λglobals: list ident. |
---|
[2286] | 909 | λaddr : list psd_argument. |
---|
[1343] | 910 | λaddr_prf: 2 = |addr|. |
---|
[1066] | 911 | λdestrs: list register. |
---|
[2286] | 912 | ν tmp_addr_l in |
---|
| 913 | ν tmp_addr_h in |
---|
[2640] | 914 | (translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@ |
---|
| 915 | let f ≝ λdestr : register.λacc : bind_new register (list (joint_seq RTL globals)). |
---|
| 916 | [LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h)] @@ |
---|
[2286] | 917 | translate_op ? Add |
---|
| 918 | [tmp_addr_l ; tmp_addr_h] |
---|
| 919 | [tmp_addr_l ; tmp_addr_h] |
---|
[2916] | 920 | [(int_size : Byte) ; zero_byte ] ? ? @@ acc in |
---|
[2640] | 921 | foldr … f [ ] destrs). |
---|
| 922 | @hide_prf |
---|
| 923 | [ <addr_prf ] % qed. |
---|
[2286] | 924 | |
---|
[2640] | 925 | definition translate_store : ∀globals.?→?→?→bind_new register ? ≝ |
---|
[1292] | 926 | λglobals: list ident. |
---|
[2286] | 927 | λaddr : list psd_argument. |
---|
[1343] | 928 | λaddr_prf: 2 = |addr|. |
---|
[2286] | 929 | λsrcrs: list psd_argument. |
---|
| 930 | ν tmp_addr_l in |
---|
| 931 | ν tmp_addr_h in |
---|
[2640] | 932 | (translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@ |
---|
| 933 | let f ≝ λsrcr : psd_argument.λacc : bind_new register (list (joint_seq RTL globals)). |
---|
| 934 | [STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr] @@ |
---|
[2286] | 935 | translate_op … Add |
---|
| 936 | [tmp_addr_l ; tmp_addr_h] |
---|
| 937 | [tmp_addr_l ; tmp_addr_h] |
---|
[2916] | 938 | [(int_size : Byte) ; zero_byte ] ? ? @@ acc in |
---|
[2640] | 939 | foldr … f [ ] srcrs). |
---|
| 940 | @hide_prf [ <addr_prf ] % qed. |
---|
[2286] | 941 | |
---|
| 942 | lemma lenv_typed_reg_typed_ok1 : |
---|
| 943 | ∀locals,env,r,ty. |
---|
| 944 | local_env_typed locals env → |
---|
| 945 | Exists ? (λx:register×typ.〈r,ty〉=x) locals → |
---|
| 946 | ∀prf. |
---|
| 947 | |find_local_env r env prf| = size_of_sig_type ty. |
---|
| 948 | #locals #env #r #ty #env_typed #r_ok |
---|
| 949 | elim (Exists_All … r_ok env_typed) |
---|
| 950 | * #r' #ty' * #EQ destruct(EQ) * #rs * #EQ1 #EQ2 #prf |
---|
| 951 | whd in match find_local_env; normalize nodelta |
---|
| 952 | @opt_safe_elim #rs' >EQ1 #EQ' destruct assumption |
---|
[1066] | 953 | qed. |
---|
| 954 | |
---|
[2286] | 955 | lemma lenv_typed_arg_typed_ok1 : |
---|
| 956 | ∀locals,env,r,ty. |
---|
| 957 | local_env_typed locals env → |
---|
| 958 | Exists ? (λx:register×typ.〈r,ty〉=x) locals → |
---|
| 959 | ∀prf. |
---|
| 960 | |find_local_env_arg r env prf| = size_of_sig_type ty. |
---|
| 961 | #locals #env #r #ty #env_typed #r_ok #prf |
---|
| 962 | whd in match find_local_env_arg; normalize nodelta |
---|
| 963 | >length_map @lenv_typed_reg_typed_ok1 assumption |
---|
| 964 | qed. |
---|
[1293] | 965 | |
---|
[2286] | 966 | lemma lenv_typed_reg_typed_ok2 : |
---|
| 967 | ∀locals,env,r,ty. |
---|
| 968 | local_env_typed locals env → |
---|
| 969 | Exists ? (λx:register×typ.〈r,ty〉=x) locals → |
---|
| 970 | r ∈ env. |
---|
| 971 | #locals #env #r #ty #env_typed #r_ok |
---|
| 972 | elim (Exists_All … r_ok env_typed) |
---|
| 973 | * #r' #ty' * #EQ destruct(EQ) * #rs * #EQ1 #EQ2 |
---|
| 974 | whd in ⊢ (?%); |
---|
| 975 | >EQ1 % |
---|
| 976 | qed. |
---|
| 977 | |
---|
| 978 | lemma cst_size_ok : ∀ty,cst.size_of_sig_type ty=size_of_cst ty cst. |
---|
| 979 | #ty * -ty [*] // |
---|
| 980 | qed. |
---|
| 981 | |
---|
[2674] | 982 | (* TODO: move it *) |
---|
[2640] | 983 | definition ensure_bind_step_block : ∀p : params.∀g. |
---|
| 984 | bind_new register (list (joint_seq p g)) → bind_step_block p g ≝ |
---|
| 985 | λp,g,b.! l ← b; bret ? (step_block p g) l. |
---|
| 986 | |
---|
| 987 | coercion bind_step_block_from_bind_list nocomposites : |
---|
| 988 | ∀p : params.∀g. |
---|
| 989 | ∀b : bind_new register (list (joint_seq p g)).bind_step_block p g ≝ |
---|
[2674] | 990 | ensure_bind_step_block on _b : bind_new register (list (joint_seq ??)) to |
---|
[2640] | 991 | bind_step_block ??. |
---|
| 992 | |
---|
[2286] | 993 | definition translate_statement : ∀globals, locals.∀env. |
---|
| 994 | local_env_typed locals env → |
---|
| 995 | ∀stmt : statement.statement_typed locals stmt → |
---|
| 996 | 𝚺b : |
---|
[2640] | 997 | bind_step_block RTL globals + |
---|
| 998 | bind_fin_block RTL globals. |
---|
| 999 | match b with [ inl _ ⇒ label | _ ⇒ unit] ≝ |
---|
[2286] | 1000 | λglobals,locals,lenv,lenv_typed,stmt. |
---|
[2640] | 1001 | match stmt return λstmt.statement_typed locals stmt → 𝚺b: bind_step_block RTL globals ⊎ bind_fin_block RTL globals.match b with [ inl _ ⇒ label | _ ⇒ unit ] with |
---|
[2286] | 1002 | [ St_skip lbl' ⇒ λstmt_typed. |
---|
[2640] | 1003 | ❬inl … (bret … [ ]), lbl'❭ |
---|
[2286] | 1004 | | St_cost cost_lbl lbl' ⇒ λstmt_typed. |
---|
[2689] | 1005 | ❬inl … (bret … 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉), lbl'❭ |
---|
[2286] | 1006 | | St_const ty destr cst lbl' ⇒ λstmt_typed. |
---|
[2640] | 1007 | ❬inl … (translate_cst ty globals cst (find_local_env destr lenv ?) ?), lbl'❭ |
---|
[2286] | 1008 | | St_op1 ty ty' op1 destr srcr lbl' ⇒ λstmt_typed. |
---|
[2640] | 1009 | ❬inl … (translate_op1 globals ty' ty op1 |
---|
[2286] | 1010 | (find_local_env destr lenv ?) |
---|
[2640] | 1011 | (find_local_env srcr lenv ?) ??), lbl'❭ |
---|
[2286] | 1012 | | St_op2 ty1 ty2 ty3 op2 destr srcr1 srcr2 lbl' ⇒ λstmt_typed. |
---|
[2640] | 1013 | ❬inl … (translate_op2 globals … op2 |
---|
[2286] | 1014 | (find_local_env destr lenv ?) |
---|
| 1015 | (find_local_env_arg srcr1 lenv ?) |
---|
[2640] | 1016 | (find_local_env_arg srcr2 lenv ?) ???), lbl'❭ |
---|
[1307] | 1017 | (* XXX: should we be ignoring this? *) |
---|
[2286] | 1018 | | St_load ignore addr destr lbl' ⇒ λstmt_typed. |
---|
[2640] | 1019 | ❬inl … (translate_load globals |
---|
| 1020 | (find_local_env_arg addr lenv ?) ? (find_local_env destr lenv ?)), lbl'❭ |
---|
[1307] | 1021 | (* XXX: should we be ignoring this? *) |
---|
[2286] | 1022 | | St_store ignore addr srcr lbl' ⇒ λstmt_typed. |
---|
[2640] | 1023 | ❬inl … (translate_store globals (find_local_env_arg addr lenv ?) ? |
---|
| 1024 | (find_local_env_arg srcr lenv ?)), lbl'❭ |
---|
[2286] | 1025 | | St_call_id f args retr lbl' ⇒ λstmt_typed. |
---|
[2674] | 1026 | ❬inl … (bret … |
---|
| 1027 | 〈[ ],λ_.CALL RTL ? (inl ?? f) (rtl_args args lenv ?) |
---|
| 1028 | (match retr with |
---|
| 1029 | [ Some retr ⇒ |
---|
| 1030 | find_local_env retr lenv ? |
---|
| 1031 | | None ⇒ [ ] |
---|
| 1032 | ]), [ ]〉), lbl'❭ |
---|
[2286] | 1033 | | St_call_ptr f args retr lbl' ⇒ λstmt_typed. |
---|
[2490] | 1034 | let fs ≝ find_and_addr_arg f lenv ?? in |
---|
[2674] | 1035 | ❬inl … (bret … |
---|
| 1036 | 〈[ ],λ_.CALL RTL ? (inr ?? fs) (rtl_args args lenv ?) |
---|
| 1037 | (match retr with |
---|
| 1038 | [ Some retr ⇒ |
---|
| 1039 | find_local_env retr lenv ? |
---|
| 1040 | | None ⇒ [ ] |
---|
| 1041 | ]), [ ]〉), lbl'❭ |
---|
[2286] | 1042 | | St_cond r lbl_true lbl_false ⇒ λstmt_typed. |
---|
[2640] | 1043 | ❬inl … (translate_cond globals (find_local_env r lenv ?) lbl_true), lbl_false❭ |
---|
| 1044 | | St_return ⇒ λ_. ❬inr … (bret … 〈[ ], RETURN ?〉),it❭ |
---|
[2286] | 1045 | ]. |
---|
[2640] | 1046 | @hide_prf |
---|
| 1047 | [ cases daemon (* needs more hypotheses *) |
---|
| 1048 | | @(lenv_typed_reg_typed_ok2 … lenv_typed stmt_typed) |
---|
| 1049 | | >(lenv_typed_reg_typed_ok1 … lenv_typed stmt_typed) |
---|
[2286] | 1050 | @cst_size_ok |
---|
| 1051 | |4,5,6,7: cases stmt_typed #dstr_typed #srcr_typed |
---|
[2640] | 1052 | [3,4: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption |
---|
| 1053 | |2: @(lenv_typed_reg_typed_ok2 … lenv_typed srcr_typed) |
---|
| 1054 | |1: @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_typed) |
---|
[1066] | 1055 | ] |
---|
[2286] | 1056 | |8,9,10,11,12,13: |
---|
| 1057 | cases stmt_typed * #srcrs1_prf #srcrs2_prf #dstr_prf |
---|
[2640] | 1058 | [5,6: @(lenv_typed_arg_typed_ok1 … lenv_typed) assumption |
---|
| 1059 | |4: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption |
---|
| 1060 | |3: @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs2_prf) |
---|
| 1061 | |2: @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs1_prf) |
---|
| 1062 | |1: @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf) |
---|
[1066] | 1063 | ] |
---|
[2490] | 1064 | |*: cases daemon (* TODO *) |
---|
[1067] | 1065 | ] |
---|
| 1066 | qed. |
---|
[1064] | 1067 | |
---|
[2490] | 1068 | definition translate_internal : |
---|
| 1069 | ∀globals.internal_function → (* insert here more properties *) |
---|
| 1070 | joint_closed_internal_function RTL globals ≝ |
---|
[1293] | 1071 | λglobals: list ident. |
---|
| 1072 | λdef. |
---|
[2286] | 1073 | let runiverse' ≝ f_reggen def in |
---|
[1068] | 1074 | let luniverse' ≝ f_labgen def in |
---|
| 1075 | let stack_size' ≝ f_stacksize def in |
---|
[2823] | 1076 | let entry' ≝ pi1 … (f_entry def) in |
---|
[2674] | 1077 | let init ≝ mk_joint_internal_function RTL globals |
---|
[2808] | 1078 | luniverse' runiverse' [ ] [ ] stack_size' stack_size' |
---|
[2823] | 1079 | (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) entry' in |
---|
[2286] | 1080 | let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals |
---|
| 1081 | (f_locals def) (f_params def) (f_result def) init in |
---|
| 1082 | let vars ≝ (f_locals def) @ (f_params def) @ |
---|
| 1083 | match f_result def with [ Some x ⇒ [x] | _ ⇒ [ ] ] in |
---|
| 1084 | let f_trans ≝ λlbl,stmt,def. |
---|
| 1085 | let pr ≝ translate_statement … vars lenv ? stmt ? in |
---|
[2640] | 1086 | match dpi1 … pr return λx.match x with [ inl _ ⇒ label | _ ⇒ unit ] → ? with |
---|
| 1087 | [ inl instrs ⇒ λlbl'.b_adds_graph … instrs lbl lbl' def |
---|
| 1088 | | inr instrs ⇒ λ_.b_fin_adds_graph … instrs lbl def |
---|
| 1089 | ] (dpi2 … pr) in |
---|
[2674] | 1090 | foldi … f_trans (f_graph def) init'. |
---|
| 1091 | (* TODO *) cases daemon |
---|
[1073] | 1092 | qed. |
---|
[1053] | 1093 | |
---|
[1239] | 1094 | (*CSC: here we are not doing any alignment on variables, like it is done in OCaml |
---|
| 1095 | because of CompCert heritage *) |
---|
[2946] | 1096 | definition rtlabs_to_rtl: (* initialization cost label *) costlabel → |
---|
| 1097 | RTLabs_program → rtl_program ≝ |
---|
| 1098 | λinit_cost, p. |
---|
| 1099 | mk_joint_program … |
---|
| 1100 | (transform_program … p (λvarnames. transf_fundef … (translate_internal varnames))) |
---|
| 1101 | init_cost. |
---|