[1635] | 1 | include "RTLabs/syntax.ma". |
---|
| 2 | include "RTL/RTL_paolo.ma". |
---|
| 3 | include "common/AssocList.ma". |
---|
| 4 | include "common/FrontEndOps.ma". |
---|
| 5 | include "common/Graphs.ma". |
---|
| 6 | include "joint/TranslateUtils_paolo.ma". |
---|
[2155] | 7 | include "utilities/bindLists.ma". |
---|
[1635] | 8 | include alias "ASM/BitVector.ma". |
---|
| 9 | include alias "arithmetics/nat.ma". |
---|
[2217] | 10 | |
---|
| 11 | definition rtl_fresh_reg: |
---|
| 12 | ∀globals.freshT RTL globals register ≝ |
---|
| 13 | λglobals,def. |
---|
| 14 | let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in |
---|
| 15 | 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉. |
---|
| 16 | |
---|
| 17 | definition rtl_fresh_reg_no_local : |
---|
| 18 | ∀globals.freshT RTL globals register ≝ |
---|
| 19 | λglobals,def. |
---|
| 20 | let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in |
---|
| 21 | 〈set_runiverse ?? def runiverse, r〉. |
---|
| 22 | |
---|
[1635] | 23 | definition size_of_sig_type ≝ |
---|
| 24 | λsig. |
---|
| 25 | match sig with |
---|
| 26 | [ ASTint isize sign ⇒ |
---|
| 27 | let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in |
---|
| 28 | isize' ÷ (nat_of_bitvector ? int_size) |
---|
| 29 | | ASTfloat _ ⇒ ? (* dpm: not implemented *) |
---|
[2208] | 30 | | ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *) |
---|
[1635] | 31 | ]. |
---|
[2208] | 32 | cases not_implemented |
---|
[1635] | 33 | qed. |
---|
| 34 | |
---|
| 35 | inductive register_type: Type[0] ≝ |
---|
| 36 | | register_int: register → register_type |
---|
| 37 | | register_ptr: register → register → register_type. |
---|
| 38 | |
---|
| 39 | definition local_env ≝ identifier_map RegisterTag (list register). |
---|
| 40 | |
---|
[1882] | 41 | definition local_env_typed : |
---|
| 42 | list (register × typ) → local_env → Prop ≝ |
---|
| 43 | λl,env.All ? |
---|
| 44 | (λp.let 〈r, ty〉 ≝ p in ∃regs.lookup … env r = Some ? regs ∧ |
---|
| 45 | |regs| = size_of_sig_type ty) l. |
---|
[1635] | 46 | |
---|
[1882] | 47 | definition find_local_env ≝ λr.λlenv : local_env. |
---|
| 48 | λprf : r ∈ lenv.opt_safe … (lookup … lenv r) ?. |
---|
| 49 | lapply (in_map_domain … lenv r) |
---|
| 50 | >prf * #x #lookup_eq >lookup_eq % #ABS destruct(ABS) |
---|
| 51 | qed. |
---|
[1635] | 52 | |
---|
[1882] | 53 | lemma find_local_env_elim : ∀P : list register → Prop.∀r. ∀lenv: local_env.∀prf. |
---|
| 54 | (∀x.lookup … lenv r = Some ? x → P x) → P (find_local_env r lenv prf). |
---|
| 55 | #P#r#lenv#prf #H |
---|
| 56 | change with (P (opt_safe ???)) |
---|
| 57 | @opt_safe_elim assumption |
---|
| 58 | qed. |
---|
[1635] | 59 | |
---|
[2208] | 60 | definition find_local_env_arg : register → local_env → ? → list psd_argument ≝ |
---|
| 61 | λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf). |
---|
[1635] | 62 | |
---|
[2155] | 63 | definition initialize_local_env_internal : |
---|
[2217] | 64 | ∀globals. |
---|
| 65 | ((joint_internal_function RTL globals) × local_env) → (register×typ) → |
---|
| 66 | ((joint_internal_function RTL globals) × local_env) ≝ |
---|
| 67 | λglobals,def_env,r_sig. |
---|
| 68 | let 〈def,lenv〉 ≝ def_env in |
---|
[1635] | 69 | let 〈r, sig〉 ≝ r_sig in |
---|
| 70 | let size ≝ size_of_sig_type sig in |
---|
[2217] | 71 | let 〈def,rs〉 ≝ repeat_fresh … (rtl_fresh_reg_no_local globals) size def in |
---|
| 72 | 〈def,add … lenv r rs〉. |
---|
[1635] | 73 | |
---|
[2155] | 74 | include alias "common/Identifiers.ma". |
---|
| 75 | let rec map_list_local_env |
---|
| 76 | lenv (regs : list (register×typ)) on regs : |
---|
| 77 | All ? (λpr.bool_to_Prop (\fst pr ∈ lenv)) regs → list register ≝ |
---|
| 78 | match regs return λx.All ?? x → ? with |
---|
| 79 | [ nil ⇒ λ_.[ ] |
---|
| 80 | | cons hd tl ⇒ λprf.find_local_env (\fst hd) lenv ? @ map_list_local_env lenv tl ? |
---|
| 81 | ].cases prf #A #B assumption qed. |
---|
[1635] | 82 | |
---|
[2217] | 83 | definition initialize_local_env : |
---|
| 84 | ∀globals. |
---|
| 85 | list (register×typ) → |
---|
| 86 | freshT RTL globals local_env ≝ |
---|
| 87 | λglobals,registers,def. |
---|
| 88 | foldl ?? (initialize_local_env_internal globals) 〈def,empty_map …〉 registers. |
---|
| 89 | |
---|
| 90 | lemma initialize_local_env_in : ∀globals,l,def,r. |
---|
| 91 | Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def). |
---|
| 92 | #globals #l #U #r @(list_elim_left … l) |
---|
| 93 | [ * |
---|
| 94 | | * #tl #sig #hd #IH #G elim (Exists_append … G) -G |
---|
| 95 | whd in match initialize_local_env; normalize nodelta |
---|
| 96 | >foldl_step change with (initialize_local_env ???) in match (foldl ?????); |
---|
| 97 | [ #H lapply (IH H) |
---|
| 98 | | * [2: *] #EQ destruct(EQ) |
---|
| 99 | ] |
---|
| 100 | cases (initialize_local_env ???) |
---|
| 101 | #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta |
---|
| 102 | elim (repeat_fresh ??????) #U'' #rs |
---|
| 103 | [ >mem_set_add @orb_Prop_r assumption |
---|
| 104 | | @mem_set_add_id |
---|
| 105 | ] |
---|
| 106 | qed. |
---|
| 107 | |
---|
| 108 | example proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr. |
---|
| 109 | // qed-. |
---|
| 110 | example proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr. |
---|
| 111 | // qed-. |
---|
| 112 | |
---|
| 113 | definition initialize_locals_params_ret : |
---|
| 114 | ∀globals. |
---|
| 115 | (* locals *) list (register×typ) → |
---|
| 116 | (* params *) list (register×typ) → |
---|
| 117 | (* return *) option (register×typ) → |
---|
| 118 | freshT RTL globals local_env ≝ |
---|
| 119 | λglobals,locals,params,ret,def. |
---|
| 120 | let 〈def',lenv〉 as EQ ≝ |
---|
| 121 | initialize_local_env globals |
---|
| 122 | ((match ret with |
---|
| 123 | [ Some r_sig ⇒ [r_sig] |
---|
| 124 | | None ⇒ [ ] |
---|
| 125 | ]) @ locals @ params) def in |
---|
| 126 | let locals' ≝ map_list_local_env lenv locals ? in |
---|
| 127 | let params' ≝ map_list_local_env lenv params ? in |
---|
| 128 | let ret' ≝ match ret return λx.ret = x → ? with |
---|
| 129 | [ Some r_sig ⇒ λprf.find_local_env (\fst r_sig) lenv ? |
---|
| 130 | | None ⇒ λ_.[ ] |
---|
| 131 | ] (refl …) in |
---|
| 132 | let def'' ≝ |
---|
| 133 | mk_joint_internal_function RTL globals |
---|
| 134 | (joint_if_luniverse … def') (joint_if_runiverse … def') ret' |
---|
| 135 | params' locals' (joint_if_stacksize … def') |
---|
| 136 | (joint_if_code … def') (joint_if_entry … def') (joint_if_exit … def') in |
---|
| 137 | 〈def'', lenv〉. @hide_prf |
---|
| 138 | [ >(proj2_rewrite ????? EQ) |
---|
| 139 | @initialize_local_env_in >prf %1 % |
---|
| 140 | |*: >(proj2_rewrite ????? EQ) |
---|
| 141 | @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr))) |
---|
| 142 | [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params)) |
---|
| 143 | [ #a #H @Exists_append_r @Exists_append_r @H |
---|
| 144 | | generalize in match params; |
---|
| 145 | ] |
---|
| 146 | | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) locals)) |
---|
| 147 | [ #a #H @Exists_append_r @Exists_append_l @H |
---|
| 148 | | generalize in match locals; |
---|
| 149 | ] |
---|
| 150 | ] |
---|
| 151 | #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G} |
---|
| 152 | ] |
---|
| 153 | qed. |
---|
| 154 | |
---|
[1635] | 155 | definition make_addr ≝ |
---|
| 156 | λA. |
---|
| 157 | λlst: list A. |
---|
[2155] | 158 | λprf: 2 = length A lst.〈nth_safe … 0 lst ?, nth_safe … 1 lst ?〉. <prf // |
---|
| 159 | qed. |
---|
[1635] | 160 | |
---|
| 161 | definition find_and_addr ≝ |
---|
[1882] | 162 | λr,lenv,prf. make_addr ? (find_local_env r lenv prf). |
---|
[1635] | 163 | |
---|
[2155] | 164 | include alias "common/Identifiers.ma". |
---|
| 165 | let rec rtl_args (args : list register) (env : local_env) on args : |
---|
[2208] | 166 | All ? (λr.bool_to_Prop (r∈env)) args → list psd_argument ≝ |
---|
[2155] | 167 | match args return λx.All ?? x → ? with |
---|
| 168 | [ nil ⇒ λ_.[ ] |
---|
| 169 | | cons hd tl ⇒ λprf.find_local_env_arg hd env ? @ rtl_args tl env ? |
---|
| 170 | ]. |
---|
| 171 | cases prf #H #G assumption |
---|
| 172 | qed. |
---|
[1635] | 173 | |
---|
[2155] | 174 | include alias "basics/lists/list.ma". |
---|
| 175 | let rec vrsplit A (m,n : nat) |
---|
| 176 | on m : Vector A (m*n) → Σs : list (Vector A n).|s| = m ≝ |
---|
| 177 | match m return λx.Vector A (x*n) → Sig (list ?) ? with |
---|
| 178 | [ O ⇒ λv.[ ] |
---|
| 179 | | S k ⇒ λv.let spl ≝ vsplit ? n … v in \fst spl :: vrsplit ? k n (\snd spl) |
---|
| 180 | ]. |
---|
| 181 | [ % |
---|
| 182 | | cases (vrsplit ????) #lst #EQ normalize >EQ % |
---|
| 183 | ] qed. |
---|
| 184 | |
---|
[1635] | 185 | definition split_into_bytes: |
---|
| 186 | ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝ |
---|
[2155] | 187 | λsize.vrsplit ? (size_intsize size) 8. |
---|
| 188 | |
---|
| 189 | let rec list_inject_All_aux A P (l : list A) on l : All A P l → list (Σx.P x) ≝ |
---|
| 190 | match l return λx.All A P x → ? with |
---|
| 191 | [ nil ⇒ λ_.[ ] |
---|
| 192 | | cons hd tl ⇒ λprf.«hd, ?» :: list_inject_All_aux A P tl ? |
---|
| 193 | ]. cases prf #H1 #H2 [@H1 | @H2] |
---|
[1635] | 194 | qed. |
---|
| 195 | |
---|
[2155] | 196 | include alias "basics/lists/list.ma". |
---|
[1635] | 197 | definition translate_op: |
---|
| 198 | ∀globals. Op2 → |
---|
| 199 | ∀dests : list register. |
---|
[2208] | 200 | ∀srcrs1 : list psd_argument. |
---|
| 201 | ∀srcrs2 : list psd_argument. |
---|
[1635] | 202 | |dests| = |srcrs1| → |srcrs1| = |srcrs2| → |
---|
[2214] | 203 | list (joint_seq RTL globals) |
---|
[2155] | 204 | ≝ |
---|
[1635] | 205 | λglobals: list ident. |
---|
| 206 | λop. |
---|
| 207 | λdestrs. |
---|
| 208 | λsrcrs1. |
---|
| 209 | λsrcrs2. |
---|
| 210 | λprf1,prf2. |
---|
| 211 | (* first, clear carry if op relies on it *) |
---|
| 212 | match op with |
---|
[1640] | 213 | [ Addc ⇒ [CLEAR_CARRY ??] |
---|
| 214 | | Sub ⇒ [CLEAR_CARRY ??] |
---|
[1635] | 215 | | _ ⇒ [ ] |
---|
[2214] | 216 | ] @ map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2. |
---|
[1635] | 217 | |
---|
[2208] | 218 | let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.|l| = size ≝ |
---|
[1635] | 219 | match size with |
---|
| 220 | [ O ⇒ [ ] |
---|
| 221 | | S size' ⇒ |
---|
[2208] | 222 | (byte_of_nat k : psd_argument) :: nat_to_args size' (k ÷ 8) |
---|
| 223 | ]. [ % | cases (nat_to_args ??) #res #EQ normalize >EQ % ] qed. |
---|
[1635] | 224 | |
---|
[2155] | 225 | definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with |
---|
| 226 | [ Ointconst size _ _ ⇒ size_intsize size |
---|
| 227 | | Ofloatconst _ _ ⇒ ? (* not implemented *) |
---|
[1635] | 228 | | _ ⇒ 2 |
---|
| 229 | ]. |
---|
| 230 | cases not_implemented qed. |
---|
| 231 | |
---|
[2155] | 232 | definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst. |
---|
[1635] | 233 | match cst with |
---|
[2208] | 234 | [ Oaddrsymbol id _ ⇒ member id (eq_identifier ?) globals |
---|
[1635] | 235 | | _ ⇒ True |
---|
| 236 | ]. |
---|
[1882] | 237 | |
---|
[1635] | 238 | definition translate_cst : |
---|
[2155] | 239 | ∀ty. |
---|
[1635] | 240 | ∀globals: list ident. |
---|
[2155] | 241 | ∀cst_sig: Σcst : constant ty.cst_well_defd ty globals cst. |
---|
[1635] | 242 | ∀destrs: list register. |
---|
[2155] | 243 | |destrs| = size_of_cst ? cst_sig → |
---|
[2214] | 244 | list (joint_seq RTL globals) |
---|
[1635] | 245 | ≝ |
---|
[2155] | 246 | λty,globals,cst_sig,destrs. |
---|
| 247 | match pi1 … cst_sig in constant return λty'.λx : constant ty'. |
---|
| 248 | cst_well_defd ty' ? x → |destrs| = size_of_cst ty' x → ? |
---|
| 249 | with |
---|
| 250 | [ Ointconst size sign const ⇒ λcst_prf,prf. |
---|
[2208] | 251 | map2 … (λr.λb : Byte.r ← b) destrs |
---|
[2155] | 252 | (split_into_bytes size const) ? |
---|
| 253 | | Ofloatconst _ _ ⇒ ? |
---|
[2208] | 254 | | Oaddrsymbol id offset ⇒ λcst_prf,prf. |
---|
[2155] | 255 | let 〈r1, r2〉 ≝ make_addr … destrs ? in |
---|
[2214] | 256 | [ADDRESS RTL globals id ? r1 r2] |
---|
[2155] | 257 | | Oaddrstack offset ⇒ λcst_prf,prf. |
---|
| 258 | let 〈r1, r2〉 ≝ make_addr … destrs ? in |
---|
[2214] | 259 | [(rtl_stack_address r1 r2 : joint_seq RTL globals)] |
---|
[2155] | 260 | ] (pi2 … cst_sig). |
---|
[1635] | 261 | [2: cases not_implemented |
---|
[2155] | 262 | |1: cases (split_into_bytes ??) #lst |
---|
| 263 | #EQ >EQ >prf whd in ⊢ (??%?); cases size % |
---|
| 264 | |3: @cst_prf |
---|
| 265 | |*: >prf % |
---|
| 266 | ] |
---|
| 267 | qed. |
---|
[1635] | 268 | |
---|
| 269 | definition translate_move : |
---|
| 270 | ∀globals. |
---|
| 271 | ∀destrs: list register. |
---|
[2208] | 272 | ∀srcrs: list psd_argument. |
---|
[2214] | 273 | |destrs| = |srcrs| → list (joint_seq RTL globals) ≝ |
---|
[1635] | 274 | λglobals,destrs,srcrs,length_eq. |
---|
[1636] | 275 | map2 … (λdst,src.dst ← src) destrs srcrs length_eq. |
---|
[1635] | 276 | |
---|
[2155] | 277 | lemma make_list_length: |
---|
[1635] | 278 | ∀A: Type[0]. |
---|
| 279 | ∀elt: A. |
---|
| 280 | ∀n: nat. |
---|
[2155] | 281 | n = length ? (make_list A elt n). |
---|
[1635] | 282 | #A #ELT #N |
---|
[2155] | 283 | elim N normalize // qed. |
---|
[1635] | 284 | |
---|
[2155] | 285 | definition sign_mask : ∀globals.register → register → |
---|
[2214] | 286 | list (joint_seq RTL globals) ≝ |
---|
[1635] | 287 | (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that: |
---|
| 288 | byte in destr if srcr is: neg | pos |
---|
| 289 | destr ← srcr | 127 11...1 | 01...1 |
---|
| 290 | destr ← destr <rot< 1 1...11 | 1...10 |
---|
| 291 | destr ← INC destr 0....0 | 1....1 |
---|
| 292 | destr ← CPL destr 1....1 | 0....0 |
---|
| 293 | *) |
---|
| 294 | λglobals,destr,srcr. |
---|
[2208] | 295 | let byte_127 : Byte ≝ false ::: maximum ? in |
---|
| 296 | [destr ← srcr .Or. byte_127 ; |
---|
[1636] | 297 | destr ← .Rl. destr ; |
---|
| 298 | destr ← .Inc. destr ; |
---|
| 299 | destr ← .Cmpl. destr ]. |
---|
[2155] | 300 | |
---|
[1635] | 301 | definition translate_cast_signed : |
---|
| 302 | ∀globals : list ident. |
---|
[2155] | 303 | list register → register → |
---|
[2214] | 304 | bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[1635] | 305 | λglobals,destrs,srcr. |
---|
| 306 | ν tmp in |
---|
| 307 | (sign_mask ? tmp srcr @ |
---|
[2208] | 308 | translate_move ? destrs (make_list ? (Reg ? tmp) (|destrs|)) (make_list_length …)). |
---|
[1635] | 309 | |
---|
[2155] | 310 | definition translate_fill_with_zero : |
---|
[1635] | 311 | ∀globals : list ident. |
---|
[2214] | 312 | list register → list (joint_seq RTL globals) ≝ |
---|
[1635] | 313 | λglobals,destrs. |
---|
| 314 | match nat_to_args (|destrs|) 0 with |
---|
| 315 | [ mk_Sig res prf ⇒ translate_move ? destrs res ?]. |
---|
| 316 | // qed. |
---|
| 317 | |
---|
[2155] | 318 | let rec last A (l : list A) on l : option A ≝ |
---|
| 319 | match l with |
---|
| 320 | [ nil ⇒ None ? |
---|
| 321 | | cons hd tl ⇒ |
---|
| 322 | match tl with |
---|
| 323 | [ nil ⇒ Some ? hd |
---|
| 324 | | _ ⇒ last A tl |
---|
| 325 | ] |
---|
| 326 | ]. |
---|
[1635] | 327 | |
---|
[2155] | 328 | lemma last_nth : ∀A,l.last A l = nth_opt A (pred (|l|)) l. |
---|
| 329 | #A #l elim l [%] |
---|
| 330 | #hd * [#_ %] |
---|
| 331 | #hd2 #tl #IH |
---|
| 332 | change with (last A (hd2 :: tl) = ?) |
---|
| 333 | >IH // |
---|
| 334 | qed. |
---|
| 335 | |
---|
[1635] | 336 | (* using size of lists as size of ints *) |
---|
| 337 | definition translate_cast : |
---|
| 338 | ∀globals: list ident. |
---|
| 339 | signedness → list register → list register → |
---|
[2214] | 340 | bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[1635] | 341 | λglobals,src_sign,destrs,srcrs. |
---|
[2155] | 342 | match reduce_strong ?? destrs srcrs with |
---|
| 343 | [ mk_Sig t prf ⇒ |
---|
| 344 | let src_common ≝ \fst (\fst t) in |
---|
| 345 | let src_rest ≝ \snd (\fst t) in |
---|
| 346 | let dst_common ≝ \fst (\snd t) in |
---|
| 347 | let dst_rest ≝ \snd (\snd t) in |
---|
| 348 | (* first, move the common part *) |
---|
[2208] | 349 | translate_move ? src_common (map … (Reg ?) dst_common) ? @@ |
---|
[2155] | 350 | match src_rest return λ_.bind_new ?? with |
---|
| 351 | [ nil ⇒ (* upcast *) |
---|
| 352 | match src_sign return λ_.bind_new ?? with |
---|
| 353 | [ Unsigned ⇒ translate_fill_with_zero ? dst_rest |
---|
| 354 | | Signed ⇒ |
---|
| 355 | match last … srcrs (* = src_common *) with |
---|
| 356 | [ Some src_last ⇒ translate_cast_signed ? dst_rest src_last |
---|
| 357 | | None ⇒ (* srcrs is empty *) translate_fill_with_zero ? dst_rest |
---|
[1635] | 358 | ] |
---|
| 359 | ] |
---|
[2155] | 360 | | _ ⇒ (* downcast, nothing else to do *) [ ] |
---|
[1635] | 361 | ] |
---|
[2155] | 362 | ]. |
---|
| 363 | >length_map @prf qed. |
---|
[1635] | 364 | |
---|
| 365 | definition translate_notint : |
---|
| 366 | ∀globals : list ident. |
---|
| 367 | ∀destrs : list register. |
---|
| 368 | ∀srcrs_arg : list register. |
---|
[2214] | 369 | |destrs| = |srcrs_arg| → list (joint_seq RTL globals) ≝ |
---|
[1635] | 370 | λglobals, destrs, srcrs, prf. |
---|
[2214] | 371 | map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf. |
---|
[1635] | 372 | |
---|
[2214] | 373 | definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[1635] | 374 | λglobals: list ident. |
---|
| 375 | λdestrs: list register. |
---|
| 376 | λsrcrs: list register. |
---|
| 377 | λprf: |destrs| = |srcrs|. (* assert in caml code *) |
---|
| 378 | translate_notint … destrs srcrs prf @ |
---|
| 379 | match nat_to_args (|destrs|) 1 with |
---|
| 380 | [ mk_Sig res prf' ⇒ |
---|
[2208] | 381 | translate_op ? Add destrs (map … (Reg ?) destrs) res ?? |
---|
[1635] | 382 | ]. |
---|
[2208] | 383 | >length_map // qed. |
---|
[1635] | 384 | |
---|
| 385 | definition translate_notbool: |
---|
| 386 | ∀globals : list ident. |
---|
| 387 | list register → list register → |
---|
[2214] | 388 | bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[1635] | 389 | λglobals,destrs,srcrs. |
---|
| 390 | match destrs with |
---|
| 391 | [ nil ⇒ [ ] |
---|
| 392 | | cons destr destrs' ⇒ |
---|
[2155] | 393 | translate_fill_with_zero ? destrs' @@ |
---|
| 394 | match srcrs return λ_.bind_new ?? with |
---|
[2208] | 395 | [ nil ⇒ [destr ← zero_byte] |
---|
[1635] | 396 | | cons srcr srcrs' ⇒ |
---|
[2155] | 397 | (destr ← srcr) ::: |
---|
[2214] | 398 | map register (joint_seq RTL globals) (λr. destr ← destr .Or. r) srcrs' @@ |
---|
[1635] | 399 | (* now destr is non-null iff srcrs was non-null *) |
---|
[2155] | 400 | CLEAR_CARRY ?? ::: |
---|
[1635] | 401 | (* many uses of 0, better not use immediates *) |
---|
| 402 | ν tmp in |
---|
[2208] | 403 | [tmp ← zero_byte ; |
---|
[1636] | 404 | destr ← tmp .Sub. tmp ; |
---|
[1635] | 405 | (* now carry bit is set iff destr was non-null *) |
---|
[1636] | 406 | destr ← tmp .Addc. tmp] |
---|
[1635] | 407 | ] |
---|
| 408 | ]. |
---|
| 409 | |
---|
| 410 | definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? → |
---|
[2214] | 411 | bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[1635] | 412 | λglobals. |
---|
| 413 | λty, ty'. |
---|
| 414 | λop1: unary_operation ty ty'. |
---|
| 415 | λdestrs: list register. |
---|
| 416 | λsrcrs: list register. |
---|
| 417 | λprf1: |destrs| = size_of_sig_type ty'. |
---|
| 418 | λprf2: |srcrs| = size_of_sig_type ty. |
---|
| 419 | match op1 |
---|
| 420 | return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' → |
---|
[2214] | 421 | bind_new (localsT RTL) (list (joint_seq RTL globals)) with |
---|
[1635] | 422 | [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2. |
---|
| 423 | translate_cast globals src_sign destrs srcrs |
---|
| 424 | | Onegint sz sg ⇒ λeq1,eq2. |
---|
| 425 | translate_negint globals destrs srcrs ? |
---|
| 426 | | Onotbool _ _ _ _ ⇒ λeq1,eq2. |
---|
| 427 | translate_notbool globals destrs srcrs |
---|
| 428 | | Onotint sz sg ⇒ λeq1,eq2. |
---|
| 429 | translate_notint globals destrs srcrs ? |
---|
[2208] | 430 | | Optrofint sz sg ⇒ λeq1,eq2. |
---|
[1635] | 431 | translate_cast globals Unsigned destrs srcrs |
---|
[2208] | 432 | | Ointofptr sz sg ⇒ λeq1,eq2. |
---|
[1635] | 433 | translate_cast globals Unsigned destrs srcrs |
---|
| 434 | | Oid t ⇒ λeq1,eq2. |
---|
[2208] | 435 | translate_move globals destrs (map … (Reg ?) srcrs) ? |
---|
[1635] | 436 | | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *) |
---|
| 437 | ] (refl …) (refl …). |
---|
[2208] | 438 | [3,4,5,6,7,8,9: (* floats *) cases not_implemented |
---|
| 439 | |*: destruct >prf1 >prf2 [3: >length_map ] // |
---|
[1635] | 440 | ] |
---|
| 441 | qed. |
---|
| 442 | |
---|
[1640] | 443 | include alias "arithmetics/nat.ma". |
---|
| 444 | |
---|
[1635] | 445 | let rec range_strong_internal (start : ℕ) (count : ℕ) |
---|
| 446 | (* Paolo: no notation to avoid ambiguity *) |
---|
| 447 | on count : list (Σn : ℕ.lt n (plus start count)) ≝ |
---|
| 448 | match count return λx.count = x → list (Σn : ℕ. n < start + count) |
---|
| 449 | with |
---|
| 450 | [ O ⇒ λ_.[ ] |
---|
| 451 | | S count' ⇒ λEQ. |
---|
| 452 | let f : (Σn : ℕ. lt n (S start + count')) → Σn : ℕ. lt n (start + count) ≝ |
---|
| 453 | λsig.match sig with [mk_Sig n prf ⇒ n] in |
---|
| 454 | start :: map … f (range_strong_internal (S start) count') |
---|
| 455 | ] (refl …). |
---|
| 456 | destruct(EQ) // qed. |
---|
| 457 | |
---|
| 458 | definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝ |
---|
| 459 | λend.range_strong_internal 0 end. |
---|
| 460 | |
---|
| 461 | definition translate_mul_i : |
---|
| 462 | ∀globals. |
---|
| 463 | register → register → |
---|
| 464 | (* size of destination and sources *) |
---|
| 465 | ∀n : ℕ. |
---|
| 466 | (* the temporary destination, with a dummy register at the end *) |
---|
| 467 | ∀tmp_destrs_dummy : list register. |
---|
[2208] | 468 | ∀srcrs1,srcrs2 : list psd_argument. |
---|
[1635] | 469 | |tmp_destrs_dummy| = S n → |
---|
| 470 | n = |srcrs1| → |
---|
| 471 | |srcrs1| = |srcrs2| → |
---|
| 472 | (* the position of the least significant byte of the result we compute at |
---|
| 473 | this stage (goes from 0 to n in the main function) *) |
---|
| 474 | ∀k : ℕ. |
---|
| 475 | lt k n → |
---|
| 476 | (* the position of the byte in the first source we will use in this stage. |
---|
| 477 | the position in the other source will be k - i *) |
---|
| 478 | (Σi.i<S k) → |
---|
| 479 | (* the accumulator *) |
---|
[2214] | 480 | list (joint_seq RTL globals) → |
---|
| 481 | list (joint_seq RTL globals) ≝ |
---|
[1635] | 482 | λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2, |
---|
| 483 | tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc. |
---|
| 484 | (* the following will expand to |
---|
| 485 | a, b ← srcrs1[i] * srcrs2[k-i] |
---|
| 486 | tmp_destrs_dummy[k] ← tmp_destrs_dummy[k] + a |
---|
| 487 | tmp_destrs_dummy[k+1] ← tmp_destrs_dummy[k+1] + b + C |
---|
| 488 | tmp_destrs_dummy[k+2] ← tmp_destrs_dummy[k+2] + 0 + C |
---|
| 489 | ... |
---|
| 490 | tmp_destrs_dummy[n] ← tmp_destrs_dummy[n] + 0 + C |
---|
| 491 | ( all calculations on tmp_destrs_dummy[n] will be eliminated with |
---|
| 492 | liveness analysis) *) |
---|
| 493 | match i_sig with |
---|
| 494 | [ mk_Sig i i_prf ⇒ |
---|
| 495 | (* we pad the result of a byte multiplication with zeros in order |
---|
| 496 | for the bit to be carried. Redundant calculations will be eliminated |
---|
| 497 | by constant propagation. *) |
---|
[2208] | 498 | let args : list psd_argument ≝ |
---|
| 499 | [Reg ? a;Reg ? b] @ make_list ? (zero_byte : psd_argument) (n - 1 - k) in |
---|
[1635] | 500 | let tmp_destrs_view : list register ≝ |
---|
| 501 | ltl ? tmp_destrs_dummy k in |
---|
[1636] | 502 | ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?) :: |
---|
[2208] | 503 | translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @ |
---|
[1635] | 504 | acc |
---|
| 505 | ]. |
---|
| 506 | [ @lt_plus_to_minus [ @le_S_S_to_le assumption | <srcrs2_prf <srcrs1_prf |
---|
| 507 | whd >(plus_n_O (S k)) @le_plus // ] |
---|
| 508 | | <srcrs1_prf |
---|
| 509 | @(transitive_le … i_prf k_prf) |
---|
| 510 | | >length_map // |
---|
| 511 | | >length_map |
---|
| 512 | >length_ltl |
---|
| 513 | >tmp_destrs_dummy_prf >length_append |
---|
[2155] | 514 | <make_list_length |
---|
[1635] | 515 | normalize in ⊢ (???(?%?)); |
---|
| 516 | >plus_minus_commutative |
---|
| 517 | [2: @le_plus_to_minus_r <plus_n_Sm <plus_n_O assumption] |
---|
| 518 | cut (S n = 2 + (n - 1)) |
---|
[2208] | 519 | [2: #EQ >EQ %] |
---|
[1635] | 520 | >plus_minus_commutative |
---|
| 521 | [2: @(transitive_le … k_prf) //] |
---|
| 522 | @sym_eq |
---|
[2208] | 523 | @plus_to_minus % |
---|
[1635] | 524 | ] qed. |
---|
| 525 | |
---|
[2214] | 526 | definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[1635] | 527 | λglobals : list ident. |
---|
| 528 | λdestrs : list register. |
---|
[2208] | 529 | λsrcrs1 : list psd_argument. |
---|
| 530 | λsrcrs2 : list psd_argument. |
---|
[1635] | 531 | λsrcrs1_prf : |destrs| = |srcrs1|. |
---|
| 532 | λsrcrs2_prf : |srcrs1| = |srcrs2|. |
---|
| 533 | (* needed fresh registers *) |
---|
| 534 | νa in |
---|
| 535 | νb in |
---|
| 536 | (* temporary registers for the result are created, so to avoid overwriting |
---|
| 537 | sources *) |
---|
[2155] | 538 | νν |destrs| as tmp_destrs with tmp_destrs_prf in |
---|
[1635] | 539 | νdummy in |
---|
| 540 | (* the step calculating all products with least significant byte going in the |
---|
| 541 | k-th position of the result *) |
---|
[2214] | 542 | let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) → |
---|
| 543 | list (joint_seq RTL globals) ≝ |
---|
[1635] | 544 | λk_sig,acc.match k_sig with |
---|
| 545 | [ mk_Sig k k_prf ⇒ |
---|
| 546 | foldr … (translate_mul_i ? a b (|destrs|) |
---|
| 547 | (tmp_destrs @ [dummy]) srcrs1 srcrs2 |
---|
| 548 | ? srcrs1_prf srcrs2_prf k k_prf) acc (range_strong (S k)) |
---|
| 549 | ] in |
---|
| 550 | (* initializing tmp_destrs to zero |
---|
| 551 | dummy is intentionally uninitialized *) |
---|
[2155] | 552 | translate_fill_with_zero … tmp_destrs @ |
---|
[1635] | 553 | (* the main body, roughly: |
---|
| 554 | for k in 0 ... n-1 do |
---|
| 555 | for i in 0 ... k do |
---|
| 556 | translate_mul_i … k … i *) |
---|
[1636] | 557 | foldr … translate_mul_k [ ] (range_strong (|destrs|)) @ |
---|
[1635] | 558 | (* epilogue: saving the result *) |
---|
[2208] | 559 | translate_move … destrs (map … (Reg ?) tmp_destrs) ?. |
---|
[1635] | 560 | [ >length_map >tmp_destrs_prf // |
---|
| 561 | | >length_append <plus_n_Sm <plus_n_O // |
---|
| 562 | ] |
---|
| 563 | qed. |
---|
| 564 | |
---|
| 565 | definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→ |
---|
[2214] | 566 | bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[1635] | 567 | λglobals: list ident. |
---|
| 568 | λdiv_not_mod: bool. |
---|
| 569 | λdestrs: list register. |
---|
[2208] | 570 | λsrcrs1: list psd_argument. |
---|
| 571 | λsrcrs2: list psd_argument. |
---|
[1635] | 572 | λsrcrs1_prf : |destrs| = |srcrs1|. |
---|
| 573 | λsrcrs2_prf : |srcrs1| = |srcrs2|. |
---|
[2155] | 574 | match destrs return λx.x = destrs → bind_new ?? with |
---|
[1635] | 575 | [ nil ⇒ λ_.[ ] |
---|
| 576 | | cons destr destrs' ⇒ λeq_destrs. |
---|
| 577 | match destrs' with |
---|
| 578 | [ nil ⇒ |
---|
[2155] | 579 | match srcrs1 return λx.x = srcrs1 → bind_new ?? with |
---|
[1635] | 580 | [ nil ⇒ λeq_srcrs1.⊥ |
---|
| 581 | | cons srcr1 srcrs1' ⇒ λeq_srcrs1. |
---|
[2155] | 582 | match srcrs2 return λx.x = srcrs2 → bind_new ?? with |
---|
[1635] | 583 | [ nil ⇒ λeq_srcrs2.⊥ |
---|
| 584 | | cons srcr2 srcrs2' ⇒ λeq_srcrs2. |
---|
| 585 | νdummy in |
---|
| 586 | let 〈destr1, destr2〉 ≝ |
---|
| 587 | if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in |
---|
[1636] | 588 | [❮destr1, destr2❯ ← srcr1 .DivuModu. srcr2] |
---|
[1635] | 589 | ] (refl …) |
---|
| 590 | ] (refl …) |
---|
| 591 | | _ ⇒ ? (* not implemented *) |
---|
| 592 | ] |
---|
| 593 | ] (refl …). |
---|
| 594 | [3: elim not_implemented] |
---|
| 595 | destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed. |
---|
| 596 | |
---|
[1636] | 597 | (* Paolo: to be moved elsewhere *) |
---|
[1635] | 598 | 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) |
---|
| 599 | (prf : |l1| = |l2|) on l1 : C ≝ |
---|
| 600 | match l1 return λx.x = l1 → C with |
---|
| 601 | [ nil ⇒ λ_.init |
---|
| 602 | | cons a l1' ⇒ λeq_l1. |
---|
| 603 | match l2 return λy.y = l2 → C with |
---|
| 604 | [ nil ⇒ λeq_l2.⊥ |
---|
| 605 | | cons b l2' ⇒ λeq_l2. |
---|
| 606 | f a b (foldr2 A B C f init l1' l2' ?) |
---|
| 607 | ] (refl …) |
---|
| 608 | ] (refl …). |
---|
[1636] | 609 | destruct normalize in prf; [destruct|//] |
---|
| 610 | qed. |
---|
[1635] | 611 | |
---|
[2155] | 612 | definition translate_ne: ∀globals: list ident.?→?→?→?→ |
---|
[2214] | 613 | bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[1635] | 614 | λglobals: list ident. |
---|
| 615 | λdestrs: list register. |
---|
[2208] | 616 | λsrcrs1: list psd_argument. |
---|
| 617 | λsrcrs2: list psd_argument. |
---|
[2155] | 618 | match destrs return λ_.|srcrs1| = |srcrs2| → bind_new ?? with |
---|
[1635] | 619 | [ nil ⇒ λ_.[ ] |
---|
[2155] | 620 | | cons destr destrs' ⇒ λEQ. |
---|
| 621 | translate_fill_with_zero … destrs' @@ |
---|
| 622 | match srcrs1 return λx.|x| = |srcrs2| → bind_new ?? with |
---|
[2208] | 623 | [ nil ⇒ λ_.[destr ← zero_byte] |
---|
[2155] | 624 | | cons srcr1 srcrs1' ⇒ |
---|
| 625 | match srcrs2 return λx.S (|srcrs1'|) = |x| → bind_new ?? with |
---|
| 626 | [ nil ⇒ λEQ.⊥ |
---|
| 627 | | cons srcr2 srcrs2' ⇒ λEQ. |
---|
[1635] | 628 | νtmpr in |
---|
[2214] | 629 | let f : psd_argument → psd_argument → list (joint_seq RTL globals) → list (joint_seq RTL globals) ≝ |
---|
[1635] | 630 | λs1,s2,acc. |
---|
[1636] | 631 | tmpr ← s1 .Xor. s2 :: |
---|
| 632 | destr ← destr .Or. tmpr :: |
---|
[1635] | 633 | acc in |
---|
[2214] | 634 | let epilogue : list (joint_seq RTL globals) ≝ |
---|
[2155] | 635 | [ CLEAR_CARRY ?? ; |
---|
[2208] | 636 | tmpr ← zero_byte .Sub. destr ; |
---|
[1635] | 637 | (* now carry bit is 1 iff destrs != 0 *) |
---|
[2208] | 638 | destr ← zero_byte .Addc. zero_byte ] in |
---|
[1636] | 639 | destr ← srcr1 .Xor. srcr2 :: |
---|
[1635] | 640 | foldr2 ??? f epilogue srcrs1' srcrs2' ? |
---|
[2155] | 641 | ] |
---|
| 642 | ] EQ |
---|
| 643 | ]. normalize in EQ; destruct(EQ) assumption qed. |
---|
[1635] | 644 | |
---|
| 645 | (* if destrs is 0 or 1, it inverses it. To be used after operations that |
---|
| 646 | ensure this. *) |
---|
[2214] | 647 | definition translate_toggle_bool : ∀globals.?→list (joint_seq RTL globals) ≝ |
---|
[1635] | 648 | λglobals: list ident. |
---|
| 649 | λdestrs: list register. |
---|
| 650 | match destrs with |
---|
| 651 | [ nil ⇒ [ ] |
---|
[1636] | 652 | | cons destr _ ⇒ [destr ← .Cmpl. destr] |
---|
[1635] | 653 | ]. |
---|
| 654 | |
---|
| 655 | definition translate_lt_unsigned : |
---|
| 656 | ∀globals. |
---|
| 657 | ∀destrs: list register. |
---|
[2208] | 658 | ∀srcrs1: list psd_argument. |
---|
| 659 | ∀srcrs2: list psd_argument. |
---|
[1635] | 660 | |srcrs1| = |srcrs2| → |
---|
[2214] | 661 | bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[2155] | 662 | λglobals,destrs,srcrs1,srcrs2,srcrs_prf. |
---|
[1635] | 663 | match destrs with |
---|
| 664 | [ nil ⇒ [ ] |
---|
| 665 | | cons destr destrs' ⇒ |
---|
[2155] | 666 | ν tmpr in |
---|
| 667 | (translate_fill_with_zero … destrs' @ |
---|
[1635] | 668 | (* I perform a subtraction, but the only interest is in the carry bit *) |
---|
[2155] | 669 | translate_op ? Sub (make_list … tmpr (|srcrs1|)) srcrs1 srcrs2 ? srcrs_prf @ |
---|
[2208] | 670 | [ destr ← zero_byte .Addc. zero_byte ]) |
---|
[1635] | 671 | ]. |
---|
[2155] | 672 | <make_list_length % qed. |
---|
[1635] | 673 | |
---|
| 674 | (* shifts signed integers by adding 128 to the most significant byte |
---|
| 675 | it replaces it with a fresh register which must be provided *) |
---|
| 676 | let rec shift_signed globals |
---|
| 677 | (tmp : register) |
---|
[2208] | 678 | (srcrs : list psd_argument) on srcrs : |
---|
[2214] | 679 | Σt : (list psd_argument) × (list (joint_seq RTL globals)).|\fst t| = |srcrs| ≝ |
---|
[2208] | 680 | let byte_128 : Byte ≝ true ::: bv_zero ? in |
---|
[1635] | 681 | match srcrs with |
---|
| 682 | [ nil ⇒ 〈[ ],[ ]〉 |
---|
| 683 | | cons srcr srcrs' ⇒ |
---|
| 684 | match srcrs' with |
---|
[2208] | 685 | [ nil ⇒ 〈[ Reg ? tmp ], [ tmp ← srcr .Add. byte_128 ]〉 |
---|
[1635] | 686 | | _ ⇒ |
---|
[2155] | 687 | let re ≝ shift_signed globals tmp srcrs' in |
---|
| 688 | 〈srcr :: \fst re, \snd re〉 |
---|
[1635] | 689 | ] |
---|
| 690 | ]. |
---|
[2155] | 691 | [1,2: % |
---|
| 692 | |*: cases re * #a #b >p1 normalize #EQ >EQ % |
---|
| 693 | ] qed. |
---|
[1635] | 694 | |
---|
| 695 | definition translate_lt_signed : |
---|
| 696 | ∀globals. |
---|
| 697 | ∀destrs: list register. |
---|
[2208] | 698 | ∀srcrs1: list psd_argument. |
---|
| 699 | ∀srcrs2: list psd_argument. |
---|
[1635] | 700 | |srcrs1| = |srcrs2| → |
---|
[2214] | 701 | bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[2155] | 702 | λglobals,destrs,srcrs1,srcrs2,srcrs_prf. |
---|
[1635] | 703 | νtmp_last_s1 in |
---|
| 704 | νtmp_last_s2 in |
---|
| 705 | let p1 ≝ shift_signed globals tmp_last_s1 srcrs1 in |
---|
| 706 | let new_srcrs1 ≝ \fst p1 in |
---|
| 707 | let shift_srcrs1 ≝ \snd p1 in |
---|
| 708 | let p2 ≝ shift_signed globals tmp_last_s2 srcrs2 in |
---|
| 709 | let new_srcrs2 ≝ \fst p2 in |
---|
| 710 | let shift_srcrs2 ≝ \snd p2 in |
---|
[2155] | 711 | shift_srcrs1 @@ shift_srcrs2 @@ |
---|
| 712 | translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ?. |
---|
| 713 | whd in match new_srcrs1; whd in match new_srcrs2; |
---|
| 714 | cases p1 |
---|
| 715 | cases p2 |
---|
| 716 | // |
---|
| 717 | qed. |
---|
[1635] | 718 | |
---|
[2214] | 719 | definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[2155] | 720 | λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf. |
---|
[1635] | 721 | if is_unsigned then |
---|
[2155] | 722 | translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs_prf |
---|
[1635] | 723 | else |
---|
[2155] | 724 | translate_lt_signed globals destrs srcrs1 srcrs2 srcrs_prf. |
---|
[1635] | 725 | |
---|
| 726 | definition translate_cmp ≝ |
---|
[2155] | 727 | λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs_prf. |
---|
[1635] | 728 | match cmp with |
---|
| 729 | [ Ceq ⇒ |
---|
[2155] | 730 | translate_ne globals destrs srcrs1 srcrs2 srcrs_prf @@ |
---|
[1635] | 731 | translate_toggle_bool globals destrs |
---|
| 732 | | Cne ⇒ |
---|
[2155] | 733 | translate_ne globals destrs srcrs1 srcrs2 srcrs_prf |
---|
[1635] | 734 | | Clt ⇒ |
---|
[2155] | 735 | translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf |
---|
[1635] | 736 | | Cgt ⇒ |
---|
[2155] | 737 | translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? |
---|
[1635] | 738 | | Cle ⇒ |
---|
[2155] | 739 | translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? @@ |
---|
[1635] | 740 | translate_toggle_bool globals destrs |
---|
| 741 | | Cge ⇒ |
---|
[2155] | 742 | translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf @@ |
---|
[1635] | 743 | translate_toggle_bool globals destrs |
---|
| 744 | ]. |
---|
| 745 | // qed. |
---|
[2155] | 746 | |
---|
[1635] | 747 | definition translate_op2 : |
---|
[2155] | 748 | ∀globals.∀ty1,ty2,ty3.∀op : binary_operation ty1 ty2 ty3. |
---|
| 749 | ∀destrs : list register. |
---|
[2208] | 750 | ∀srcrs1,srcrs2 : list psd_argument. |
---|
[2155] | 751 | |destrs| = size_of_sig_type ty3 → |
---|
| 752 | |srcrs1| = size_of_sig_type ty1 → |
---|
| 753 | |srcrs2| = size_of_sig_type ty2 → |
---|
[2214] | 754 | bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ |
---|
[2155] | 755 | λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2. |
---|
| 756 | match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3. |
---|
| 757 | ? = size_of_sig_type ty3 → ? = size_of_sig_type ty1 → ? = size_of_sig_type ty2 → |
---|
| 758 | bind_new ?? with |
---|
| 759 | [ Oadd sz sg ⇒ λprf1,prf2,prf3. |
---|
| 760 | translate_op globals Add destrs srcrs1 srcrs2 ?? |
---|
[2208] | 761 | | Oaddp sz ⇒ λprf1,prf2,prf3. |
---|
[2155] | 762 | let is_Oaddp ≝ 0 in |
---|
| 763 | translate_op globals Add destrs srcrs1 srcrs2 ?? |
---|
| 764 | | Osub sz sg ⇒ λprf1,prf2,prf2. |
---|
| 765 | translate_op globals Sub destrs srcrs1 srcrs2 ?? |
---|
[2208] | 766 | | Osubpi sz ⇒ λprf1,prf2,prf3. |
---|
[2155] | 767 | let is_Osubpi ≝ 0 in |
---|
| 768 | translate_op globals Sub destrs srcrs1 srcrs2 ?? |
---|
[2208] | 769 | | Osubpp sz ⇒ λprf1,prf2,prf3. |
---|
[2155] | 770 | let is_Osubpp ≝ 0 in |
---|
| 771 | translate_op globals Sub destrs srcrs1 srcrs2 ?? |
---|
| 772 | | Omul sz sg ⇒ λprf1,prf2,prf3. |
---|
| 773 | translate_mul globals destrs srcrs1 srcrs2 ?? |
---|
| 774 | | Odivu sz ⇒ λprf1,prf2,prf3. |
---|
| 775 | translate_divumodu8 globals true destrs srcrs1 srcrs2 ?? |
---|
| 776 | | Omodu sz ⇒ λprf1,prf2,prf3. |
---|
| 777 | translate_divumodu8 globals false destrs srcrs1 srcrs2 ?? |
---|
| 778 | | Oand sz sg ⇒ λprf1,prf2,prf3. |
---|
| 779 | translate_op globals And destrs srcrs1 srcrs2 ?? |
---|
| 780 | | Oor sz sg ⇒ λprf1,prf2,prf3. |
---|
| 781 | translate_op globals Or destrs srcrs1 srcrs2 ?? |
---|
| 782 | | Oxor sz sg ⇒ λprf1,prf2,prf3. |
---|
| 783 | translate_op globals Xor destrs srcrs1 srcrs2 ?? |
---|
| 784 | | Ocmp sz sg1 sg2 c ⇒ λprf1,prf2,prf3. |
---|
| 785 | translate_cmp false globals c destrs srcrs1 srcrs2 ? |
---|
| 786 | | Ocmpu sz sg c ⇒ λprf1,prf2,prf3. |
---|
| 787 | translate_cmp true globals c destrs srcrs1 srcrs2 ? |
---|
[2208] | 788 | | Ocmpp sg c ⇒ λprf1,prf2,prf3. |
---|
[2155] | 789 | let is_Ocmpp ≝ 0 in |
---|
| 790 | translate_cmp true globals c destrs srcrs1 srcrs2 ? |
---|
| 791 | | _ ⇒ ⊥ (* assert false, implemented in run time or float op *) |
---|
[2208] | 792 | ]. try @not_implemented // |
---|
[2155] | 793 | (* pointer arithmetics is broken at the moment *) |
---|
| 794 | cases daemon |
---|
| 795 | qed. |
---|
[1635] | 796 | |
---|
[2155] | 797 | definition translate_cond: ∀globals: list ident. list register → label → |
---|
[2214] | 798 | bind_seq_block RTL globals (joint_step RTL globals) ≝ |
---|
[1635] | 799 | λglobals: list ident. |
---|
| 800 | λsrcrs: list register. |
---|
| 801 | λlbl_true: label. |
---|
[2214] | 802 | match srcrs return λ_.bind_seq_block RTL ? (joint_step ??) with |
---|
[2155] | 803 | [ nil ⇒ bret … 〈[ ], NOOP ??〉 |
---|
[1635] | 804 | | cons srcr srcrs' ⇒ |
---|
| 805 | ν tmpr in |
---|
[2214] | 806 | let f : register → joint_seq RTL globals ≝ |
---|
[1640] | 807 | λr. tmpr ← tmpr .Or. r in |
---|
[2214] | 808 | bret … 〈MOVE RTL globals 〈tmpr,srcr〉 :: |
---|
[2162] | 809 | map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉 |
---|
[1635] | 810 | ]. |
---|
| 811 | |
---|
| 812 | (* Paolo: to be controlled (original seemed overly complex) *) |
---|
[2214] | 813 | definition translate_load : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝ |
---|
[1635] | 814 | λglobals: list ident. |
---|
[2208] | 815 | λaddr : list psd_argument. |
---|
[1635] | 816 | λaddr_prf: 2 = |addr|. |
---|
| 817 | λdestrs: list register. |
---|
| 818 | ν tmp_addr_l in |
---|
| 819 | ν tmp_addr_h in |
---|
[2214] | 820 | let f ≝ λdestr : register.λacc : list (joint_seq RTL globals). |
---|
| 821 | LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) :: |
---|
[2208] | 822 | translate_op ? Add |
---|
[1635] | 823 | [tmp_addr_l ; tmp_addr_h] |
---|
[2208] | 824 | [tmp_addr_l ; tmp_addr_h] |
---|
| 825 | [zero_byte ; (int_size : Byte)] ? ? @ acc in |
---|
[2155] | 826 | translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@ |
---|
[1635] | 827 | foldr … f [ ] destrs. |
---|
[2208] | 828 | [1: <addr_prf |
---|
| 829 | ] // qed. |
---|
[1635] | 830 | |
---|
[2214] | 831 | definition translate_store : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝ |
---|
[1635] | 832 | λglobals: list ident. |
---|
[2208] | 833 | λaddr : list psd_argument. |
---|
[1635] | 834 | λaddr_prf: 2 = |addr|. |
---|
[2208] | 835 | λsrcrs: list psd_argument. |
---|
[1635] | 836 | ν tmp_addr_l in |
---|
| 837 | ν tmp_addr_h in |
---|
[2214] | 838 | let f ≝ λsrcr : psd_argument.λacc : list (joint_seq RTL globals). |
---|
| 839 | STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr :: |
---|
[1635] | 840 | translate_op … Add |
---|
| 841 | [tmp_addr_l ; tmp_addr_h] |
---|
[2208] | 842 | [tmp_addr_l ; tmp_addr_h] |
---|
| 843 | [zero_byte ; (int_size : Byte)] ? ? @ acc in |
---|
[2155] | 844 | translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@ |
---|
[1635] | 845 | foldr … f [ ] srcrs. |
---|
| 846 | [1: <addr_prf] // qed. |
---|
| 847 | |
---|
[2155] | 848 | definition translate_statement : ∀globals.local_env → statement → |
---|
| 849 | 𝚺b : |
---|
[2214] | 850 | bind_seq_block RTL globals (joint_step RTL globals) + |
---|
| 851 | bind_seq_block RTL globals (joint_fin_step RTL). |
---|
[2155] | 852 | if is_inl … b then label else unit ≝ |
---|
| 853 | λglobals,lenv,stmt. |
---|
| 854 | (*λstmt_typed : TODO*) |
---|
| 855 | match stmt return λ_.𝚺b:bind_seq_block ???+bind_seq_block ???.if is_inl … b then label else unit with |
---|
| 856 | [ St_skip lbl' ⇒ |
---|
| 857 | ❬NOOP ??, lbl'❭ |
---|
| 858 | | St_cost cost_lbl lbl' ⇒ |
---|
| 859 | ❬COST_LABEL … cost_lbl, lbl'❭ |
---|
| 860 | | St_const ty destr cst lbl' ⇒ |
---|
| 861 | ❬translate_cst ty globals cst (find_local_env destr lenv ?) ?, lbl'❭ |
---|
| 862 | | St_op1 ty ty' op1 destr srcr lbl' ⇒ |
---|
| 863 | ❬translate_op1 globals ty' ty op1 |
---|
| 864 | (find_local_env destr lenv ?) |
---|
| 865 | (find_local_env srcr lenv ?) ??, lbl'❭ |
---|
| 866 | | St_op2 ty1 ty2 ty3 op2 destr srcr1 srcr2 lbl' ⇒ |
---|
| 867 | ❬translate_op2 globals … op2 |
---|
| 868 | (find_local_env destr lenv ?) |
---|
| 869 | (find_local_env_arg srcr1 lenv ?) |
---|
| 870 | (find_local_env_arg srcr2 lenv ?) ???, lbl'❭ |
---|
[1635] | 871 | (* XXX: should we be ignoring this? *) |
---|
[2155] | 872 | | St_load ignore addr destr lbl' ⇒ |
---|
| 873 | ❬translate_load globals |
---|
| 874 | (find_local_env_arg addr lenv ?) ? (find_local_env destr lenv ?), lbl'❭ |
---|
[1635] | 875 | (* XXX: should we be ignoring this? *) |
---|
[2155] | 876 | | St_store ignore addr srcr lbl' ⇒ |
---|
| 877 | ❬translate_store globals (find_local_env_arg addr lenv ?) ? |
---|
| 878 | (find_local_env_arg srcr lenv ?), lbl'❭ |
---|
| 879 | | St_call_id f args retr lbl' ⇒ |
---|
| 880 | ❬(match retr with |
---|
[1635] | 881 | [ Some retr ⇒ |
---|
[2214] | 882 | CALL_ID RTL ? f (rtl_args args lenv ?) (find_local_env retr lenv ?) |
---|
[1635] | 883 | | None ⇒ |
---|
[2214] | 884 | CALL_ID RTL ? f (rtl_args args lenv ?) [ ] |
---|
[2155] | 885 | ] : bind_seq_block ???), lbl'❭ |
---|
| 886 | | St_call_ptr f args retr lbl' ⇒ |
---|
| 887 | let fs ≝ find_and_addr f lenv ?? in |
---|
| 888 | ❬(rtl_call_ptr (\fst fs) (\snd fs) (rtl_args args lenv ?) |
---|
| 889 | (match retr with |
---|
| 890 | [ Some retr ⇒ |
---|
| 891 | find_local_env retr lenv ? |
---|
| 892 | | None ⇒ [ ] |
---|
| 893 | ]) : joint_step ??), lbl'❭ |
---|
| 894 | | St_cond r lbl_true lbl_false ⇒ |
---|
| 895 | ❬translate_cond globals (find_local_env r lenv ?) lbl_true, lbl_false❭ |
---|
| 896 | | St_jumptable r l ⇒ ? (* assert false: not implemented yet *) |
---|
| 897 | | St_return ⇒ ❬RETURN ?, it❭ |
---|
| 898 | ]. |
---|
| 899 | [*: cases daemon |
---|
[1635] | 900 | (* TODO: proofs regarding lengths of lists, examine! *) |
---|
| 901 | ] |
---|
| 902 | qed. |
---|
| 903 | |
---|
| 904 | (* XXX: we use a "hack" here to circumvent the proof obligations required to |
---|
| 905 | create res, an empty internal_function record. we insert into our graph |
---|
| 906 | the start and end nodes to ensure that they are in, and place dummy |
---|
| 907 | skip instructions at these nodes. *) |
---|
| 908 | definition translate_internal ≝ |
---|
| 909 | λglobals: list ident. |
---|
| 910 | λdef. |
---|
[2217] | 911 | let runiverse' ≝ f_reggen def in |
---|
[1635] | 912 | let luniverse' ≝ f_labgen def in |
---|
| 913 | let stack_size' ≝ f_stacksize def in |
---|
| 914 | let entry' ≝ f_entry def in |
---|
| 915 | let exit' ≝ f_exit def in |
---|
[2214] | 916 | let graph' ≝ empty_map LabelTag (joint_statement RTL globals) in |
---|
[1644] | 917 | let graph' ≝ add LabelTag ? graph' entry' |
---|
| 918 | (GOTO … exit') in |
---|
[1640] | 919 | let graph' ≝ add LabelTag ? graph' exit' |
---|
[1644] | 920 | (RETURN …) in |
---|
[2217] | 921 | let init ≝ |
---|
| 922 | mk_joint_internal_function RTL globals luniverse' runiverse' [ ] [ ] |
---|
| 923 | [ ] stack_size' graph' (pi1 … entry') (pi1 … exit') in |
---|
| 924 | let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals |
---|
| 925 | (f_locals def) (f_params def) (f_result def) init in |
---|
[2155] | 926 | let f_trans ≝ λlbl,stmt,def. |
---|
| 927 | let pr ≝ translate_statement … lenv stmt in |
---|
[2217] | 928 | b_adds_graph … (rtl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in |
---|
| 929 | foldi … f_trans (f_graph def) init'. |
---|
| 930 | @hide_prf |
---|
| 931 | >graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add |
---|
[1635] | 932 | qed. |
---|
| 933 | |
---|
| 934 | (*CSC: here we are not doing any alignment on variables, like it is done in OCaml |
---|
| 935 | because of CompCert heritage *) |
---|
| 936 | definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝ |
---|
[2103] | 937 | λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)). |
---|