[789] | 1 | include "RTLabs/syntax.ma". |
---|
| 2 | include "RTL/RTL.ma". |
---|
| 3 | include "common/AssocList.ma". |
---|
[1071] | 4 | include "common/FrontEndOps.ma". |
---|
[789] | 5 | include "common/Graphs.ma". |
---|
[1280] | 6 | include "joint/TranslateUtils.ma". |
---|
[789] | 7 | |
---|
[1047] | 8 | let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝ |
---|
| 9 | match n with |
---|
[1281] | 10 | [ O ⇒ 〈[],runiverse〉 |
---|
| 11 | | S n' ⇒ |
---|
| 12 | let 〈r,runiverse〉 ≝ fresh … runiverse in |
---|
| 13 | let 〈res,runiverse〉 ≝ register_freshes runiverse n' in |
---|
| 14 | 〈r::res,runiverse〉 ]. |
---|
[1047] | 15 | |
---|
| 16 | definition complete_regs ≝ |
---|
[1280] | 17 | λglobals. |
---|
[1047] | 18 | λdef. |
---|
| 19 | λsrcrs1. |
---|
| 20 | λsrcrs2. |
---|
[1280] | 21 | if leb (length … srcrs2) (length … srcrs1) then |
---|
| 22 | let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs1) (length ? srcrs2)) in |
---|
| 23 | 〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉 |
---|
| 24 | else |
---|
| 25 | let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs2) (length ? srcrs1)) in |
---|
| 26 | 〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉. |
---|
[1047] | 27 | |
---|
[1280] | 28 | lemma complete_regs_length: |
---|
| 29 | ∀globals,def,left,right. |
---|
| 30 | |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|. |
---|
| 31 | #globals #def #left #right |
---|
| 32 | whd in match complete_regs normalize nodelta |
---|
| 33 | @leb_elim normalize nodelta #H |
---|
| 34 | [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right))) |
---|
| 35 | | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))] |
---|
| 36 | cases (fresh_regs ????) #def' #fresh normalize >append_length |
---|
| 37 | generalize in match H -H; |
---|
| 38 | generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh) |
---|
| 39 | [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus |
---|
| 40 | <plus_minus_m_m /2/ ] |
---|
| 41 | qed. |
---|
[1064] | 42 | |
---|
[1053] | 43 | definition size_of_sig_type ≝ |
---|
[1052] | 44 | λsig. |
---|
| 45 | match sig with |
---|
[1047] | 46 | [ ASTint isize sign ⇒ |
---|
[1053] | 47 | let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in |
---|
| 48 | isize' ÷ (nat_of_bitvector ? int_size) |
---|
| 49 | | ASTfloat _ ⇒ ? (* dpm: not implemented *) |
---|
| 50 | | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size |
---|
[1047] | 51 | ]. |
---|
[1053] | 52 | cases not_implemented; |
---|
[1052] | 53 | qed. |
---|
[1047] | 54 | |
---|
[789] | 55 | inductive register_type: Type[0] ≝ |
---|
| 56 | | register_int: register → register_type |
---|
| 57 | | register_ptr: register → register → register_type. |
---|
| 58 | |
---|
[1280] | 59 | definition local_env ≝ BitVectorTrie (list register) 16. |
---|
[789] | 60 | |
---|
[1280] | 61 | definition mem_local_env : register → local_env → bool ≝ |
---|
| 62 | λr. member … (word_of_identifier … r). |
---|
[1052] | 63 | |
---|
[1280] | 64 | definition add_local_env : register → list register → local_env → local_env ≝ |
---|
| 65 | λr. insert … (word_of_identifier … r). |
---|
[1052] | 66 | |
---|
[1280] | 67 | definition find_local_env : register → local_env → list register ≝ |
---|
| 68 | λr: register.λbvt. lookup … (word_of_identifier … r) bvt []. |
---|
[1052] | 69 | |
---|
[789] | 70 | definition initialize_local_env_internal ≝ |
---|
[1281] | 71 | λlenv_runiverse. |
---|
[1053] | 72 | λr_sig. |
---|
[1281] | 73 | let 〈lenv,runiverse〉 ≝ lenv_runiverse in |
---|
[1053] | 74 | let 〈r, sig〉 ≝ r_sig in |
---|
| 75 | let size ≝ size_of_sig_type sig in |
---|
[1281] | 76 | let 〈rs,runiverse〉 ≝ register_freshes runiverse size in |
---|
| 77 | 〈add_local_env r rs lenv,runiverse〉. |
---|
[789] | 78 | |
---|
| 79 | definition initialize_local_env ≝ |
---|
| 80 | λruniverse. |
---|
| 81 | λregisters. |
---|
[1053] | 82 | λresult. |
---|
[1050] | 83 | let registers ≝ registers @ |
---|
| 84 | match result with |
---|
| 85 | [ None ⇒ [ ] |
---|
| 86 | | Some rt ⇒ [ rt ] |
---|
| 87 | ] |
---|
| 88 | in |
---|
[1281] | 89 | foldl ? ? initialize_local_env_internal 〈Stub …,runiverse〉 registers. |
---|
[1280] | 90 | |
---|
[1050] | 91 | definition map_list_local_env_internal ≝ |
---|
[1280] | 92 | λlenv,res,r. res @ (find_local_env r lenv). |
---|
[1050] | 93 | |
---|
| 94 | definition map_list_local_env ≝ |
---|
[1280] | 95 | λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs. |
---|
[1050] | 96 | |
---|
[1053] | 97 | definition make_addr ≝ |
---|
| 98 | λA. |
---|
| 99 | λlst: list A. |
---|
[1066] | 100 | λprf: 2 ≤ length A lst. |
---|
| 101 | match lst return λx. 2 ≤ |x| → A × A with |
---|
[1053] | 102 | [ nil ⇒ λlst_nil_prf. ? |
---|
| 103 | | cons hd tl ⇒ λprf. |
---|
[1066] | 104 | match tl return λx. 1 ≤ |x| → A × A with |
---|
[1053] | 105 | [ nil ⇒ λtl_nil_prf. ? |
---|
| 106 | | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉 |
---|
| 107 | ] ? |
---|
| 108 | ] prf. |
---|
| 109 | [1: normalize in lst_nil_prf; |
---|
[1066] | 110 | cases(not_le_Sn_O 1); |
---|
| 111 | #HYP cases(HYP lst_nil_prf) |
---|
[1053] | 112 | |2: normalize in prf; |
---|
[1066] | 113 | @le_S_S_to_le |
---|
| 114 | assumption |
---|
[1053] | 115 | |3: normalize in tl_nil_prf; |
---|
[1066] | 116 | cases(not_le_Sn_O 0) |
---|
[1280] | 117 | #HYP cases(HYP tl_nil_prf)] |
---|
[1053] | 118 | qed. |
---|
[1050] | 119 | |
---|
[789] | 120 | definition find_and_addr ≝ |
---|
[1280] | 121 | λr,lenv. make_addr ? (find_local_env r lenv). |
---|
[789] | 122 | |
---|
| 123 | definition rtl_args ≝ |
---|
[1280] | 124 | λregs_list,lenv. flatten … (map … (λr. find_local_env r lenv) regs_list). |
---|
[789] | 125 | |
---|
[1057] | 126 | definition translate_cst_int_internal ≝ |
---|
[1282] | 127 | λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl. |
---|
[1057] | 128 | |
---|
[1308] | 129 | axiom split_into_bytes: |
---|
| 130 | ∀size. |
---|
| 131 | ∀int: bvint size. |
---|
| 132 | Σbytes: list Byte. |bytes| = size_intsize size. |
---|
| 133 | |
---|
| 134 | lemma eqb_implies_eq: |
---|
| 135 | ∀m, n: nat. |
---|
| 136 | eqb m n = true → m = n. |
---|
| 137 | #M |
---|
| 138 | elim M |
---|
| 139 | [1: #N normalize |
---|
| 140 | cases N |
---|
| 141 | [1: normalize // |
---|
| 142 | |2: #M' normalize #HYP destruct(HYP) |
---|
| 143 | ] |
---|
| 144 | |2: #M' #IND_HYP #N |
---|
| 145 | normalize |
---|
| 146 | cases N |
---|
| 147 | [1: normalize #HYP destruct(HYP) |
---|
| 148 | |2: #M'' normalize #HYP |
---|
| 149 | @eq_f @(IND_HYP M'') |
---|
| 150 | assumption |
---|
| 151 | ] |
---|
| 152 | ] |
---|
| 153 | qed. |
---|
| 154 | |
---|
[1307] | 155 | let rec translate_cst |
---|
| 156 | (globals: list ident) (cst: constant) (destrs: list register) |
---|
| 157 | (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals) |
---|
| 158 | on cst: rtl_internal_function globals ≝ |
---|
| 159 | match cst with |
---|
| 160 | [ Ointconst size const ⇒ |
---|
| 161 | match destrs with |
---|
[1308] | 162 | [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def |
---|
| 163 | | _ ⇒ |
---|
| 164 | let size' ≝ size_intsize size in |
---|
| 165 | match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with |
---|
| 166 | [ true ⇒ λgood_case. |
---|
| 167 | match split_into_bytes size const with |
---|
| 168 | [ dp bytes bytes_length_proof ⇒ |
---|
| 169 | let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in |
---|
| 170 | adds_graph rtl_params1 globals mapped start_lbl dest_lbl def |
---|
| 171 | ] |
---|
| 172 | | false ⇒ λbad_case. ? |
---|
| 173 | ] (refl … (eqb size' (|destrs|))) |
---|
[1307] | 174 | ] |
---|
| 175 | | Ofloatconst float ⇒ ⊥ |
---|
[1308] | 176 | | Oaddrsymbol id offset ⇒ |
---|
| 177 | let 〈r1, r2〉 ≝ make_addr … destrs ? in |
---|
| 178 | add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def |
---|
| 179 | | Oaddrstack offset ⇒ |
---|
| 180 | let 〈r1, r2〉 ≝ make_addr … destrs ? in |
---|
[1315] | 181 | ? |
---|
| 182 | (* add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def *) |
---|
[1307] | 183 | ]. |
---|
[1308] | 184 | [1: >bytes_length_proof |
---|
| 185 | cut(size' = |destrs|) |
---|
| 186 | [1: @eqb_implies_eq |
---|
| 187 | assumption |
---|
| 188 | |2: #EQ_HYP |
---|
| 189 | <EQ_HYP % |
---|
| 190 | ] |
---|
| 191 | |5: cases not_implemented (* XXX: float, error_float in o'caml *) |
---|
[1315] | 192 | |*: cases daemon |
---|
[1307] | 193 | ]. |
---|
[1315] | 194 | qed. |
---|
[1307] | 195 | |
---|
[1059] | 196 | definition translate_move_internal ≝ |
---|
[1280] | 197 | λglobals. |
---|
[1059] | 198 | λdestr: register. |
---|
| 199 | λsrcr: register. |
---|
[1283] | 200 | sequential rtl_params_ globals (MOVE … 〈destr,srcr〉). |
---|
[1057] | 201 | |
---|
[1059] | 202 | definition translate_move ≝ |
---|
[1280] | 203 | λglobals. |
---|
[1059] | 204 | λdestrs: list register. |
---|
| 205 | λsrcrs: list register. |
---|
| 206 | λstart_lbl: label. |
---|
[1071] | 207 | match reduce_strong register register destrs srcrs with |
---|
[1060] | 208 | [ dp crl_crr len_proof ⇒ |
---|
| 209 | let commonl ≝ \fst (\fst crl_crr) in |
---|
| 210 | let commonr ≝ \fst (\snd crl_crr) in |
---|
| 211 | let restl ≝ \snd (\fst crl_crr) in |
---|
| 212 | let restr ≝ \snd (\snd crl_crr) in |
---|
[1283] | 213 | let f_common ≝ translate_move_internal globals in |
---|
[1280] | 214 | let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in |
---|
| 215 | let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) |
---|
| 216 | add_translates … [ translate1 ; translate2 ] start_lbl |
---|
[1060] | 217 | ]. |
---|
| 218 | @len_proof |
---|
| 219 | qed. |
---|
| 220 | |
---|
| 221 | let rec make |
---|
| 222 | (A: Type[0]) (elt: A) (n: nat) on n ≝ |
---|
| 223 | match n with |
---|
| 224 | [ O ⇒ [ ] |
---|
| 225 | | S n' ⇒ elt :: make A elt n' |
---|
| 226 | ]. |
---|
| 227 | |
---|
| 228 | lemma make_length: |
---|
| 229 | ∀A: Type[0]. |
---|
| 230 | ∀elt: A. |
---|
| 231 | ∀n: nat. |
---|
| 232 | n = length ? (make A elt n). |
---|
| 233 | #A #ELT #N |
---|
| 234 | elim N |
---|
| 235 | [ normalize % |
---|
| 236 | | #N #IH |
---|
| 237 | normalize <IH % |
---|
| 238 | ] |
---|
| 239 | qed. |
---|
| 240 | |
---|
| 241 | definition translate_cast_unsigned ≝ |
---|
[1280] | 242 | λglobals. |
---|
[1060] | 243 | λdestrs. |
---|
| 244 | λstart_lbl. |
---|
| 245 | λdest_lbl. |
---|
[1280] | 246 | λdef: joint_internal_function … (rtl_params globals). |
---|
| 247 | let 〈def, tmp_zero〉 ≝ fresh_reg … def in |
---|
| 248 | let zeros ≝ make … tmp_zero (length … destrs) in |
---|
| 249 | add_translates … [ |
---|
| 250 | adds_graph rtl_params1 … [ |
---|
[1283] | 251 | sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) |
---|
[1060] | 252 | ]; |
---|
[1280] | 253 | translate_move globals destrs zeros |
---|
[1060] | 254 | ] start_lbl dest_lbl def. |
---|
| 255 | |
---|
[1285] | 256 | definition translate_cast_signed: |
---|
| 257 | ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ |
---|
| 258 | λglobals: list ident. |
---|
[1060] | 259 | λdestrs. |
---|
| 260 | λsrcr. |
---|
| 261 | λstart_lbl. |
---|
| 262 | λdest_lbl. |
---|
| 263 | λdef. |
---|
[1280] | 264 | let 〈def, tmp_128〉 ≝ fresh_reg … def in |
---|
| 265 | let 〈def, tmp_255〉 ≝ fresh_reg … def in |
---|
| 266 | let 〈def, tmpr〉 ≝ fresh_reg … def in |
---|
| 267 | let 〈def, dummy〉 ≝ fresh_reg … def in |
---|
[1060] | 268 | let insts ≝ [ |
---|
[1285] | 269 | sequential … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128)); |
---|
| 270 | sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr); |
---|
| 271 | sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128); |
---|
| 272 | sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255)); |
---|
| 273 | sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255) |
---|
| 274 | ] |
---|
| 275 | in |
---|
[1280] | 276 | let srcrs ≝ make … tmpr (length … destrs) in |
---|
[1285] | 277 | add_translates rtl_params1 globals [ |
---|
| 278 | adds_graph rtl_params1 globals insts; |
---|
| 279 | translate_move globals destrs srcrs |
---|
[1060] | 280 | ] start_lbl dest_lbl def. |
---|
| 281 | |
---|
| 282 | definition translate_cast ≝ |
---|
[1285] | 283 | λglobals: list ident. |
---|
| 284 | λsrc_size: nat. |
---|
| 285 | λsrc_sign: signedness. |
---|
| 286 | λdest_size: nat. |
---|
| 287 | λdestrs: list register. |
---|
| 288 | λsrcrs: list register. |
---|
[1066] | 289 | match |srcrs| return λx. |srcrs| = x → ? with |
---|
[1285] | 290 | [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ] |
---|
[1060] | 291 | | S n' ⇒ λsucc_prf. |
---|
| 292 | if ltb dest_size src_size then |
---|
[1285] | 293 | translate_move globals destrs srcrs |
---|
[1060] | 294 | else |
---|
[1071] | 295 | match reduce_strong register register destrs srcrs with |
---|
[1060] | 296 | [ dp crl len_proof ⇒ |
---|
| 297 | let commonl ≝ \fst (\fst crl) in |
---|
| 298 | let commonr ≝ \fst (\snd crl) in |
---|
| 299 | let restl ≝ \snd (\fst crl) in |
---|
| 300 | let restr ≝ \snd (\snd crl) in |
---|
[1285] | 301 | let insts_common ≝ translate_move globals commonl commonr in |
---|
[1060] | 302 | let sign_reg ≝ last_safe ? srcrs ? in |
---|
| 303 | let insts_sign ≝ |
---|
| 304 | match src_sign with |
---|
[1285] | 305 | [ Unsigned ⇒ translate_cast_unsigned globals restl |
---|
| 306 | | Signed ⇒ translate_cast_signed globals restl sign_reg |
---|
[1060] | 307 | ] |
---|
| 308 | in |
---|
[1285] | 309 | add_translates rtl_params1 globals [ insts_common; insts_sign ] |
---|
[1060] | 310 | ] |
---|
| 311 | ] (refl ? (|srcrs|)). |
---|
| 312 | >succ_prf // |
---|
| 313 | qed. |
---|
| 314 | |
---|
| 315 | definition translate_negint ≝ |
---|
[1285] | 316 | λglobals: list ident. |
---|
| 317 | λdestrs: list register. |
---|
| 318 | λsrcrs: list register. |
---|
| 319 | λstart_lbl: label. |
---|
| 320 | λdest_lbl: label. |
---|
| 321 | λdef: rtl_internal_function globals. |
---|
| 322 | λprf: |destrs| = |srcrs|. (* assert in caml code *) |
---|
| 323 | let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in |
---|
| 324 | let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in |
---|
| 325 | let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in |
---|
[1060] | 326 | let insts_init ≝ [ |
---|
[1285] | 327 | sequential … (SET_CARRY …); |
---|
| 328 | sequential … (INT rtl_params_ globals tmpr (zero ?)) |
---|
[1060] | 329 | ] in |
---|
[1285] | 330 | let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in |
---|
[1060] | 331 | let insts_add ≝ map … f_add destrs in |
---|
[1285] | 332 | adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def. |
---|
[1060] | 333 | |
---|
[1285] | 334 | definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ |
---|
| 335 | λglobals: list ident. |
---|
| 336 | λdestrs: list register. |
---|
| 337 | λsrcrs: list register. |
---|
| 338 | λstart_lbl: label. |
---|
| 339 | λdest_lbl: label. |
---|
| 340 | λdef: rtl_internal_function globals. |
---|
[1060] | 341 | match destrs with |
---|
[1285] | 342 | [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def |
---|
[1060] | 343 | | cons destr destrs ⇒ |
---|
[1285] | 344 | let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in |
---|
| 345 | let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in |
---|
| 346 | let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in |
---|
| 347 | let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in |
---|
[1060] | 348 | let f ≝ λtmp_srcr. [ |
---|
[1285] | 349 | sequential … (CLEAR_CARRY rtl_params_ globals); |
---|
| 350 | sequential … (INT rtl_params_ globals tmpr (zero ?)); |
---|
| 351 | sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr); |
---|
| 352 | sequential … (INT rtl_params_ globals tmpr (zero ?)); |
---|
| 353 | sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr); |
---|
| 354 | sequential … (OP2 rtl_params_ globals Xor destr destr tmpr) |
---|
[1060] | 355 | ] in |
---|
[1285] | 356 | let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in |
---|
| 357 | let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in |
---|
| 358 | add_translates rtl_params1 globals [ |
---|
| 359 | save_srcrs; adds_graph rtl_params1 globals insts; epilogue |
---|
[1060] | 360 | ] start_lbl dest_lbl def |
---|
| 361 | ]. |
---|
| 362 | |
---|
[1066] | 363 | (* TODO: examine this properly. This is a change from the O'caml code due |
---|
| 364 | to us dropping the explicit use of a cast destination size field. We |
---|
| 365 | instead infer the size of the cast's destination from the context. Is |
---|
| 366 | this correct? |
---|
| 367 | *) |
---|
[1064] | 368 | definition translate_op1 ≝ |
---|
[1286] | 369 | λglobals: list ident. |
---|
[1066] | 370 | λop1: unary_operation. |
---|
[1064] | 371 | λdestrs: list register. |
---|
| 372 | λsrcrs: list register. |
---|
[1062] | 373 | λprf: |destrs| = |srcrs|. |
---|
[1064] | 374 | λstart_lbl: label. |
---|
| 375 | λdest_lbl: label. |
---|
[1286] | 376 | λdef: rtl_internal_function globals. |
---|
[1060] | 377 | match op1 with |
---|
[1066] | 378 | [ Ocastint src_sign src_size ⇒ |
---|
| 379 | let dest_size ≝ |destrs| * 8 in |
---|
| 380 | let src_size ≝ bitsize_of_intsize src_size in |
---|
[1286] | 381 | translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def |
---|
[1066] | 382 | | Onegint ⇒ |
---|
[1286] | 383 | translate_negint globals destrs srcrs start_lbl dest_lbl def prf |
---|
[1066] | 384 | | Onotbool ⇒ |
---|
[1286] | 385 | translate_notbool globals destrs srcrs start_lbl dest_lbl def |
---|
[1066] | 386 | | Onotint ⇒ |
---|
[1286] | 387 | let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in |
---|
[1060] | 388 | let l ≝ map2 … f destrs srcrs prf in |
---|
[1286] | 389 | adds_graph rtl_params1 globals l start_lbl dest_lbl def |
---|
[1066] | 390 | | Optrofint r ⇒ |
---|
[1286] | 391 | translate_move globals destrs srcrs start_lbl dest_lbl def |
---|
[1066] | 392 | | Ointofptr r ⇒ |
---|
[1286] | 393 | translate_move globals destrs srcrs start_lbl dest_lbl def |
---|
[1066] | 394 | | Oid ⇒ |
---|
[1286] | 395 | translate_move globals destrs srcrs start_lbl dest_lbl def |
---|
[1066] | 396 | | _ ⇒ ? (* float operations implemented in runtime *) |
---|
[1060] | 397 | ]. |
---|
[1066] | 398 | cases not_implemented |
---|
| 399 | qed. |
---|
[1061] | 400 | |
---|
[1286] | 401 | definition translate_op: ∀globals. ? → list register → list register → list register → |
---|
| 402 | label → label → rtl_internal_function globals → rtl_internal_function globals ≝ |
---|
| 403 | λglobals: list ident. |
---|
[1061] | 404 | λop. |
---|
[1286] | 405 | λdestrs: list register. |
---|
| 406 | λsrcrs1: list register. |
---|
| 407 | λsrcrs2: list register. |
---|
| 408 | λstart_lbl: label. |
---|
| 409 | λdest_lbl: label. |
---|
| 410 | λdef: rtl_internal_function globals. |
---|
[1071] | 411 | match reduce_strong register register srcrs1 srcrs2 with |
---|
[1061] | 412 | [ dp reduced first_reduced_proof ⇒ |
---|
| 413 | let srcrsl_common ≝ \fst (\fst reduced) in |
---|
| 414 | let srcrsr_common ≝ \fst (\snd reduced) in |
---|
| 415 | let srcrsl_rest ≝ \snd (\fst reduced) in |
---|
| 416 | let srcrsr_rest ≝ \snd (\snd reduced) in |
---|
[1293] | 417 | let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in |
---|
[1071] | 418 | match reduce_strong register register destrs srcrsl_common with |
---|
[1061] | 419 | [ dp reduced second_reduced_proof ⇒ |
---|
| 420 | let destrs_common ≝ \fst (\fst reduced) in |
---|
| 421 | let destrs_rest ≝ \snd (\fst reduced) in |
---|
[1071] | 422 | match reduce_strong register register destrs_rest srcrs_rest with |
---|
[1061] | 423 | [ dp reduced third_reduced_proof ⇒ |
---|
| 424 | let destrs_cted ≝ \fst (\fst reduced) in |
---|
| 425 | let destrs_rest ≝ \snd (\fst reduced) in |
---|
| 426 | let srcrs_cted ≝ \fst (\snd reduced) in |
---|
[1286] | 427 | let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in |
---|
[1061] | 428 | let insts_init ≝ [ |
---|
[1286] | 429 | sequential … (CLEAR_CARRY …); |
---|
| 430 | sequential … (INT rtl_params_ globals tmpr (zero …)) |
---|
[1061] | 431 | ] in |
---|
[1286] | 432 | let f_add ≝ λdestr. λsrcr1. λsrcr2. sequential … (OP2 rtl_params_ globals op destr srcr1 srcr2) in |
---|
| 433 | let insts_add ≝ map3 ? ? ? ? f_add destrs_common srcrsl_common srcrsr_common ? ? in |
---|
| 434 | let f_add_cted ≝ λdestr. λsrcr. sequential … (OP2 rtl_params_ globals op destr srcr tmpr) in |
---|
| 435 | let insts_add_cted ≝ map2 … f_add_cted destrs_cted srcrs_cted ? in |
---|
| 436 | let f_rest ≝ λdestr. sequential … (OP2 rtl_params_ globals op destr tmpr tmpr) in |
---|
[1061] | 437 | let insts_rest ≝ map … f_rest destrs_rest in |
---|
[1286] | 438 | adds_graph rtl_params1 globals (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def |
---|
[1061] | 439 | ] |
---|
| 440 | ] |
---|
| 441 | ]. |
---|
[1066] | 442 | [1: @third_reduced_proof |
---|
| 443 | |3: @first_reduced_proof |
---|
[1286] | 444 | |*: cases daemon (* XXX: some of these look like they may be false *) |
---|
[1066] | 445 | ] |
---|
[1062] | 446 | qed. |
---|
[1057] | 447 | |
---|
[1062] | 448 | let rec translate_mul1 |
---|
[1286] | 449 | (globals: list ident) (dummy: register) (tmpr: register) |
---|
| 450 | (destrs: list register) (srcrs1: list register) (srcr2: register) |
---|
| 451 | (start_lbl: label) |
---|
| 452 | on srcrs1 ≝ |
---|
[1062] | 453 | match destrs with |
---|
[1286] | 454 | [ nil ⇒ adds_graph rtl_params1 globals [ GOTO … ] start_lbl |
---|
[1062] | 455 | | cons destr tl ⇒ |
---|
| 456 | match tl with |
---|
| 457 | [ nil ⇒ |
---|
| 458 | match srcrs1 with |
---|
| 459 | [ nil ⇒ |
---|
[1286] | 460 | adds_graph rtl_params1 globals [ |
---|
| 461 | sequential … (INT rtl_params_ globals tmpr (zero …)); |
---|
| 462 | sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) |
---|
[1062] | 463 | ] start_lbl |
---|
| 464 | | cons srcr1 tl' ⇒ |
---|
[1286] | 465 | adds_graph rtl_params1 globals [ |
---|
| 466 | sequential … (OPACCS rtl_params_ globals Mul tmpr dummy srcr2 srcr1); |
---|
| 467 | sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) |
---|
[1062] | 468 | ] start_lbl |
---|
| 469 | ] |
---|
| 470 | | cons destr2 destrs ⇒ |
---|
| 471 | match srcrs1 with |
---|
| 472 | [ nil ⇒ |
---|
[1286] | 473 | add_translates rtl_params1 globals [ |
---|
| 474 | adds_graph rtl_params1 globals [ |
---|
| 475 | sequential … (INT rtl_params_ globals tmpr (zero …)); |
---|
| 476 | sequential … (OP2 rtl_params_ globals Addc destr destr tmpr); |
---|
| 477 | sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr) |
---|
[1062] | 478 | ]; |
---|
[1286] | 479 | translate_cst globals (Ointconst I8 (zero …)) destrs |
---|
[1062] | 480 | ] start_lbl |
---|
| 481 | | cons srcr1 srcrs1 ⇒ |
---|
| 482 | match destrs with |
---|
| 483 | [ nil ⇒ |
---|
[1286] | 484 | add_translates rtl_params1 globals [ |
---|
| 485 | adds_graph rtl_params1 globals [ |
---|
| 486 | sequential … (INT rtl_params_ globals tmpr (zero …)); |
---|
| 487 | sequential … (OP2 rtl_params_ globals Addc destr destr tmpr); |
---|
| 488 | sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr) |
---|
[1062] | 489 | ]; |
---|
[1286] | 490 | translate_cst globals (Ointconst I8 (zero ?)) destrs |
---|
[1062] | 491 | ] start_lbl |
---|
| 492 | | cons destr2 destrs ⇒ |
---|
[1286] | 493 | add_translates rtl_params1 globals [ |
---|
| 494 | adds_graph rtl_params1 globals [ |
---|
| 495 | sequential … (OPACCS rtl_params_ globals Mul tmpr destr2 srcr2 srcr1); |
---|
| 496 | sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) |
---|
[1062] | 497 | ]; |
---|
[1286] | 498 | translate_mul1 globals dummy tmpr (destr2 :: destrs) srcrs1 srcr2 |
---|
[1062] | 499 | ] start_lbl |
---|
| 500 | ] |
---|
| 501 | ] |
---|
| 502 | ] |
---|
| 503 | ]. |
---|
| 504 | |
---|
| 505 | definition translate_muli ≝ |
---|
[1286] | 506 | λglobals: list ident. |
---|
[1062] | 507 | λdummy: register. |
---|
| 508 | λtmpr: register. |
---|
| 509 | λdestrs: list register. |
---|
| 510 | λtmp_destrs: list register. |
---|
| 511 | λsrcrs1: list register. |
---|
| 512 | λdummy_lbl: label. |
---|
| 513 | λi: nat. |
---|
[1063] | 514 | λi_prf. |
---|
| 515 | λtranslates: list ?. |
---|
| 516 | λsrcr2i: register. |
---|
[1286] | 517 | let 〈tmp_destrs1, tmp_destrs2〉 ≝ split … tmp_destrs i i_prf in |
---|
[1063] | 518 | let tmp_destrs2' ≝ |
---|
| 519 | match tmp_destrs2 with |
---|
| 520 | [ nil ⇒ [ ] |
---|
| 521 | | cons tmp_destr2 tmp_destrs2 ⇒ [ |
---|
[1286] | 522 | adds_graph rtl_params1 globals [ |
---|
| 523 | sequential rtl_params_ globals (CLEAR_CARRY …); |
---|
| 524 | sequential … (INT rtl_params_ globals tmp_destr2 (zero …)) |
---|
[1063] | 525 | ]; |
---|
[1286] | 526 | translate_mul1 globals dummy tmpr tmp_destrs2 srcrs1 srcr2i; |
---|
| 527 | translate_cst globals (Ointconst I8 (zero …)) tmp_destrs1; |
---|
| 528 | adds_graph rtl_params1 globals [ |
---|
| 529 | sequential rtl_params_ globals (CLEAR_CARRY …) |
---|
[1063] | 530 | ]; |
---|
[1286] | 531 | translate_op globals Addc destrs destrs tmp_destrs |
---|
[1063] | 532 | ] |
---|
| 533 | ] |
---|
| 534 | in |
---|
| 535 | translates @ tmp_destrs2'. |
---|
[1062] | 536 | |
---|
[1064] | 537 | axiom translate_mul: |
---|
[1286] | 538 | ∀globals: list ident. |
---|
[1064] | 539 | ∀destrs: list register. |
---|
| 540 | ∀srcrs1: list register. |
---|
| 541 | ∀srcrs2: list register. |
---|
| 542 | ∀start_lbl: label. |
---|
| 543 | ∀dest_lbl: label. |
---|
[1286] | 544 | ∀def: rtl_internal_function globals. |
---|
| 545 | rtl_internal_function globals. |
---|
[1064] | 546 | |
---|
| 547 | (* |
---|
[1063] | 548 | definition translate_mul ≝ |
---|
[1287] | 549 | λglobals: list ident. |
---|
[1063] | 550 | λdestrs: list register. |
---|
| 551 | λsrcrs1: list register. |
---|
| 552 | λsrcrs2: list register. |
---|
| 553 | λstart_lbl: label. |
---|
| 554 | λdest_lbl: label. |
---|
[1287] | 555 | λdef: rtl_internal_function globals. |
---|
| 556 | let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in |
---|
| 557 | let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in |
---|
| 558 | let 〈def, tmp_destrs〉 ≝ fresh_regs rtl_params0 globals def (|destrs|) in |
---|
| 559 | let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in |
---|
| 560 | let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in |
---|
[1063] | 561 | let insts_init ≝ [ |
---|
[1287] | 562 | translate_move globals fresh_srcrs1 srcrs1; |
---|
| 563 | translate_move globals fresh_srcrs2 srcrs2; |
---|
| 564 | translate_cst globals (Ointconst I8 (zero …)) destrs |
---|
[1063] | 565 | ] |
---|
| 566 | in |
---|
[1306] | 567 | let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in |
---|
| 568 | let insts_mul ≝ foldi … f [ ] srcrs2 in ?. |
---|
[1063] | 569 | add_translates (insts_init @ insts_mul) start_lbl dest_lbl def. |
---|
[1064] | 570 | *) |
---|
[1062] | 571 | |
---|
[1064] | 572 | definition translate_divumodu8 ≝ |
---|
[1287] | 573 | λglobals: list ident. |
---|
[1064] | 574 | λorder: bool. |
---|
| 575 | λdestrs: list register. |
---|
| 576 | λsrcr1: register. |
---|
| 577 | λsrcr2: register. |
---|
| 578 | λstart_lbl: label. |
---|
| 579 | λdest_lbl: label. |
---|
[1287] | 580 | λdef: rtl_internal_function globals. |
---|
[1064] | 581 | match destrs with |
---|
[1287] | 582 | [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def |
---|
[1064] | 583 | | cons destr destrs ⇒ |
---|
[1287] | 584 | let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in |
---|
[1064] | 585 | let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in |
---|
[1287] | 586 | let inst_div ≝ adds_graph rtl_params1 globals [ |
---|
| 587 | sequential rtl_params_ globals (OPACCS … DivuModu destr1 destr2 srcr1 srcr2) |
---|
[1064] | 588 | ] |
---|
| 589 | in |
---|
[1287] | 590 | let insts_rest ≝ translate_cst globals (Ointconst I8 (zero ?)) destrs in |
---|
| 591 | add_translates rtl_params1 globals [ inst_div; insts_rest ] start_lbl dest_lbl def |
---|
[1064] | 592 | ]. |
---|
[1063] | 593 | |
---|
[1287] | 594 | definition translate_ne: ∀globals: list ident. ? → ? → ? → ? → ? → ? → rtl_internal_function globals ≝ |
---|
| 595 | λglobals: list ident. |
---|
[1064] | 596 | λdestrs: list register. |
---|
| 597 | λsrcrs1: list register. |
---|
| 598 | λsrcrs2: list register. |
---|
| 599 | λstart_lbl: label. |
---|
| 600 | λdest_lbl: label. |
---|
[1287] | 601 | λdef: rtl_internal_function globals. |
---|
[1064] | 602 | match destrs with |
---|
[1287] | 603 | [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def |
---|
[1064] | 604 | | cons destr destrs ⇒ |
---|
[1287] | 605 | let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in |
---|
| 606 | let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params0 globals def in |
---|
| 607 | let 〈def, tmp_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in |
---|
| 608 | let save_srcrs1 ≝ translate_move globals tmp_srcrs1 srcrs1 in |
---|
| 609 | let 〈def, tmp_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in |
---|
| 610 | let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in |
---|
[1071] | 611 | match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with |
---|
[1064] | 612 | [ dp crl their_proof ⇒ |
---|
| 613 | let commonl ≝ \fst (\fst crl) in |
---|
| 614 | let commonr ≝ \fst (\snd crl) in |
---|
| 615 | let restl ≝ \snd (\snd crl) in |
---|
| 616 | let restr ≝ \snd (\snd crl) in |
---|
[1293] | 617 | let rest ≝ restl @ restr in |
---|
[1064] | 618 | let inits ≝ [ |
---|
[1287] | 619 | sequential … (INT rtl_params_ globals destr (zero …)); |
---|
| 620 | sequential … (INT rtl_params_ globals tmp_zero (zero …)) |
---|
[1064] | 621 | ] |
---|
| 622 | in |
---|
| 623 | let f_common ≝ λtmp_srcr1. λtmp_srcr2. [ |
---|
[1287] | 624 | sequential … (CLEAR_CARRY …); |
---|
| 625 | sequential … (OP2 rtl_params_ globals Sub tmpr tmp_srcr1 tmp_srcr2); |
---|
| 626 | sequential … (OP2 rtl_params_ globals Or destr destr tmpr) |
---|
[1064] | 627 | ] |
---|
| 628 | in |
---|
[1287] | 629 | let insts_common ≝ flatten … (map2 … f_common commonl commonr ?) in |
---|
[1064] | 630 | let f_rest ≝ λtmp_srcr. [ |
---|
[1287] | 631 | sequential … (CLEAR_CARRY …); |
---|
| 632 | sequential … (OP2 rtl_params_ globals Sub tmpr tmp_zero tmp_srcr); |
---|
| 633 | sequential … (OP2 rtl_params_ globals Or destr destr tmpr) |
---|
[1064] | 634 | ] |
---|
| 635 | in |
---|
[1287] | 636 | let insts_rest ≝ flatten … (map … f_rest rest) in |
---|
[1064] | 637 | let insts ≝ inits @ insts_common @ insts_rest in |
---|
[1287] | 638 | let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in |
---|
| 639 | add_translates rtl_params1 globals [ |
---|
| 640 | save_srcrs1; save_srcrs2; adds_graph rtl_params1 globals insts; epilogue |
---|
[1064] | 641 | ] start_lbl dest_lbl def |
---|
| 642 | ] |
---|
| 643 | ]. |
---|
[1293] | 644 | @their_proof |
---|
[1064] | 645 | qed. |
---|
| 646 | |
---|
| 647 | definition translate_eq_reg ≝ |
---|
[1287] | 648 | λglobals: list ident. |
---|
[1064] | 649 | λtmp_zero: register. |
---|
| 650 | λtmp_one: register. |
---|
| 651 | λtmpr1: register. |
---|
| 652 | λtmpr2: register. |
---|
| 653 | λdestr: register. |
---|
| 654 | λdummy_lbl: label. |
---|
| 655 | λsrcr12: register × register. |
---|
| 656 | let 〈srcr1, srcr2〉 ≝ srcr12 in |
---|
[1287] | 657 | [ sequential … (CLEAR_CARRY …); |
---|
| 658 | sequential rtl_params_ globals (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2); |
---|
| 659 | sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero); |
---|
| 660 | sequential … (OP2 rtl_params_ globals Sub tmpr2 srcr2 srcr1); |
---|
| 661 | sequential … (OP2 rtl_params_ globals Addc tmpr2 tmp_zero tmp_zero); |
---|
| 662 | sequential … (OP2 rtl_params_ globals Or tmpr1 tmpr1 tmpr2); |
---|
| 663 | sequential … (OP2 rtl_params_ globals Xor tmpr1 tmpr1 tmp_one); |
---|
| 664 | sequential … (OP2 rtl_params_ globals And destr destr tmpr1) ]. |
---|
[1064] | 665 | |
---|
| 666 | definition translate_eq_list ≝ |
---|
[1287] | 667 | λglobals: list ident. |
---|
[1064] | 668 | λtmp_zero: register. |
---|
| 669 | λtmp_one: register. |
---|
| 670 | λtmpr1: register. |
---|
| 671 | λtmpr2: register. |
---|
| 672 | λdestr: register. |
---|
| 673 | λleq: list (register × register). |
---|
| 674 | λdummy_lbl: label. |
---|
[1287] | 675 | let f ≝ translate_eq_reg globals tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in |
---|
| 676 | (sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1))) :: |
---|
| 677 | flatten … (map … f leq). |
---|
[1064] | 678 | |
---|
| 679 | definition translate_atom ≝ |
---|
[1287] | 680 | λglobals: list ident. |
---|
[1064] | 681 | λtmp_zero: register. |
---|
| 682 | λtmp_one: register. |
---|
| 683 | λtmpr1: register. |
---|
| 684 | λtmpr2: register. |
---|
| 685 | λtmpr3: register. |
---|
| 686 | λdestr: register. |
---|
| 687 | λdummy_lbl: label. |
---|
| 688 | λleq: list (register × register). |
---|
| 689 | λsrcr1: register. |
---|
| 690 | λsrcr2: register. |
---|
[1287] | 691 | translate_eq_list globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @ |
---|
| 692 | [ sequential … (CLEAR_CARRY …); |
---|
| 693 | sequential … (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2); |
---|
| 694 | sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero); |
---|
| 695 | sequential … (OP2 rtl_params_ globals And tmpr3 tmpr3 tmpr1); |
---|
| 696 | sequential … (OP2 rtl_params_ globals Or destr destr tmpr3) ]. |
---|
[1064] | 697 | |
---|
| 698 | definition translate_lt_main ≝ |
---|
[1287] | 699 | λglobals: list ident. |
---|
[1064] | 700 | λtmp_zero: register. |
---|
| 701 | λtmp_one: register. |
---|
| 702 | λtmpr1: register. |
---|
| 703 | λtmpr2: register. |
---|
| 704 | λtmpr3: register. |
---|
| 705 | λdestr: register. |
---|
| 706 | λdummy_lbl: label. |
---|
| 707 | λsrcrs1: list register. |
---|
| 708 | λsrcrs2: list register. |
---|
| 709 | λproof: |srcrs1| = |srcrs2|. |
---|
| 710 | let f ≝ λinsts_leq. λsrcr1. λsrcr2. |
---|
| 711 | let 〈insts, leq〉 ≝ insts_leq in |
---|
[1287] | 712 | let added_insts ≝ translate_atom globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in |
---|
[1064] | 713 | 〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉 |
---|
| 714 | in |
---|
[1287] | 715 | \fst (fold_left2 … f 〈[ ], [ ]〉 srcrs1 srcrs2 proof). |
---|
[1064] | 716 | |
---|
| 717 | definition fresh_regs_strong: |
---|
[1287] | 718 | ∀globals. rtl_internal_function globals → ∀n: nat. Σfresh: (rtl_internal_function globals) × (list register). |\snd fresh| = n ≝ |
---|
| 719 | λglobals: list ident. |
---|
[1064] | 720 | λdef. |
---|
| 721 | λn. |
---|
[1287] | 722 | fresh_regs rtl_params0 globals def n. |
---|
[1064] | 723 | @fresh_regs_length |
---|
| 724 | qed. |
---|
| 725 | |
---|
| 726 | definition complete_regs_strong: |
---|
[1287] | 727 | ∀globals: list ident. rtl_internal_function globals → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝ |
---|
| 728 | λglobals: list ident. |
---|
[1064] | 729 | λdef. |
---|
| 730 | λleft. |
---|
| 731 | λright. |
---|
[1287] | 732 | complete_regs globals def left right. |
---|
[1064] | 733 | @complete_regs_length |
---|
| 734 | qed. |
---|
| 735 | |
---|
| 736 | definition translate_lt ≝ |
---|
[1287] | 737 | λglobals: list ident. |
---|
[1064] | 738 | λdestrs: list register. |
---|
[1306] | 739 | λprf_destrs: 0 < |destrs|. |
---|
[1064] | 740 | λsrcrs1: list register. |
---|
| 741 | λsrcrs2: list register. |
---|
| 742 | λstart_lbl: label. |
---|
| 743 | λdest_lbl: label. |
---|
[1287] | 744 | λdef: rtl_internal_function globals. |
---|
[1064] | 745 | match destrs with |
---|
[1287] | 746 | [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def |
---|
[1064] | 747 | | _ ⇒ |
---|
[1287] | 748 | match fresh_regs_strong globals def (|destrs|) with |
---|
[1064] | 749 | [ dp def_tmp_destrs tmp_destrs_proof ⇒ |
---|
| 750 | let def ≝ \fst def_tmp_destrs in |
---|
| 751 | let tmp_destrs ≝ \snd def_tmp_destrs in |
---|
| 752 | let tmp_destr ≝ hd_safe ? tmp_destrs ? in |
---|
[1287] | 753 | let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params1 globals def in |
---|
| 754 | let 〈def, tmp_one〉 ≝ fresh_reg rtl_params1 globals def in |
---|
| 755 | let 〈def, tmpr1〉 ≝ fresh_reg rtl_params1 globals def in |
---|
| 756 | let 〈def, tmpr2〉 ≝ fresh_reg rtl_params1 globals def in |
---|
| 757 | let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in |
---|
| 758 | match complete_regs_strong globals def srcrs1 srcrs2 with |
---|
[1064] | 759 | [ dp srcrs12_added srcrs12_proof ⇒ |
---|
| 760 | let srcrs1 ≝ \fst (\fst srcrs12_added) in |
---|
| 761 | let srcrs2 ≝ \snd (\fst srcrs12_added) in |
---|
| 762 | let added ≝ \snd srcrs12_added in |
---|
[1287] | 763 | let srcrs1' ≝ rev … srcrs1 in |
---|
| 764 | let srcrs2' ≝ rev … srcrs2 in |
---|
[1064] | 765 | let insts_init ≝ [ |
---|
[1287] | 766 | translate_cst globals (Ointconst I8 (zero ?)) tmp_destrs; |
---|
| 767 | translate_cst globals (Ointconst I8 (zero ?)) added; |
---|
| 768 | adds_graph rtl_params1 globals [ |
---|
| 769 | sequential rtl_params_ globals (INT rtl_params_ globals tmp_zero (zero …)); |
---|
| 770 | sequential rtl_params_ globals (INT rtl_params_ globals tmp_one (bitvector_of_nat … 1)) |
---|
[1064] | 771 | ] |
---|
| 772 | ] |
---|
| 773 | in |
---|
| 774 | let insts_main ≝ |
---|
[1287] | 775 | translate_lt_main globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in |
---|
| 776 | let insts_main ≝ [ adds_graph rtl_params1 globals insts_main ] in |
---|
| 777 | let insts_exit ≝ [ translate_move globals destrs tmp_destrs ] in |
---|
| 778 | add_translates rtl_params1 globals (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def |
---|
[1064] | 779 | ] |
---|
| 780 | ] |
---|
| 781 | ]. |
---|
| 782 | [2: >tmp_destrs_proof @prf_destrs |
---|
| 783 | |1: normalize nodelta |
---|
| 784 | generalize in match srcrs12_proof |
---|
| 785 | #HYP >rev_length >rev_length @HYP |
---|
| 786 | ] |
---|
| 787 | qed. |
---|
| 788 | |
---|
| 789 | definition add_128_to_last ≝ |
---|
[1287] | 790 | λglobals: list ident. |
---|
[1064] | 791 | λtmp_128: register. |
---|
| 792 | λrs. |
---|
| 793 | λprf: 0 < |rs|. |
---|
| 794 | λstart_lbl: label. |
---|
| 795 | match rs with |
---|
[1287] | 796 | [ nil ⇒ adds_graph rtl_params1 globals [ ] start_lbl |
---|
[1064] | 797 | | _ ⇒ |
---|
[1287] | 798 | let r ≝ last_safe … rs prf in |
---|
| 799 | adds_graph rtl_params1 globals [ |
---|
| 800 | sequential rtl_params_ globals (OP2 rtl_params_ globals Add r r tmp_128) |
---|
[1064] | 801 | ] start_lbl |
---|
| 802 | ]. |
---|
| 803 | |
---|
| 804 | definition translate_lts ≝ |
---|
[1287] | 805 | λglobals: list ident. |
---|
[1064] | 806 | λdestrs: list register. |
---|
[1306] | 807 | λdestrs_prf: 0 < |destrs|. |
---|
[1064] | 808 | λsrcrs1: list register. |
---|
| 809 | λsrcrs2: list register. |
---|
| 810 | λsrcrs1_lt_prf: 0 < |srcrs1|. |
---|
[1066] | 811 | λsrcrs2_lt_prf: 0 < |srcrs2|. |
---|
[1064] | 812 | λstart_lbl: label. |
---|
| 813 | λdest_lbl: label. |
---|
[1287] | 814 | λdef: rtl_internal_function globals. |
---|
| 815 | match fresh_regs_strong globals def (|srcrs1|) with |
---|
[1064] | 816 | [ dp def_tmp_srcrs1 srcrs1_prf ⇒ |
---|
| 817 | let def ≝ \fst def_tmp_srcrs1 in |
---|
| 818 | let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in |
---|
[1287] | 819 | match fresh_regs_strong globals def (|srcrs2|) with |
---|
[1064] | 820 | [ dp def_tmp_srcrs2 srcrs2_prf ⇒ |
---|
| 821 | let def ≝ \fst def_tmp_srcrs2 in |
---|
| 822 | let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in |
---|
[1287] | 823 | let 〈def, tmp_128〉 ≝ fresh_reg rtl_params0 globals def in |
---|
| 824 | add_translates rtl_params1 globals [ |
---|
| 825 | translate_move globals tmp_srcrs1 srcrs1; |
---|
| 826 | translate_move globals tmp_srcrs2 srcrs2; |
---|
| 827 | adds_graph rtl_params1 globals [ |
---|
| 828 | sequential rtl_params_ globals (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128)) |
---|
[1064] | 829 | ]; |
---|
[1287] | 830 | add_128_to_last globals tmp_128 tmp_srcrs1 ?; |
---|
| 831 | add_128_to_last globals tmp_128 tmp_srcrs2 ?; |
---|
| 832 | translate_lt globals destrs destrs_prf tmp_srcrs1 tmp_srcrs2 |
---|
[1064] | 833 | ] start_lbl dest_lbl def |
---|
| 834 | ] |
---|
| 835 | ]. |
---|
[1066] | 836 | [1: >srcrs1_prf @srcrs1_lt_prf |
---|
| 837 | |2: >srcrs2_prf @srcrs2_lt_prf |
---|
[1064] | 838 | ] |
---|
| 839 | qed. |
---|
| 840 | |
---|
| 841 | definition translate_op2 ≝ |
---|
[1288] | 842 | λglobals: list ident. |
---|
[1064] | 843 | λop2. |
---|
| 844 | λdestrs: list register. |
---|
[1306] | 845 | λdestrs_prf: 0 < |destrs|. |
---|
[1064] | 846 | λsrcrs1: list register. |
---|
| 847 | λsrcrs2: list register. |
---|
[1306] | 848 | λsrcrs1_prf: 0 < |srcrs1|. (* XXX: can this be relaxed? i think it can |
---|
| 849 | but we need more dep. typ. in modu/divu |
---|
| 850 | cases *) |
---|
| 851 | λsrcrs2_prf: 0 < |srcrs2|. |
---|
[1064] | 852 | λstart_lbl: label. |
---|
| 853 | λdest_lbl: label. |
---|
[1288] | 854 | λdef: rtl_internal_function globals. |
---|
[1064] | 855 | match op2 with |
---|
[1066] | 856 | [ Oadd ⇒ |
---|
[1288] | 857 | translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
[1066] | 858 | | Oaddp ⇒ |
---|
[1288] | 859 | translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
[1066] | 860 | | Osub ⇒ |
---|
[1288] | 861 | translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
[1066] | 862 | | Osubpi ⇒ |
---|
[1288] | 863 | translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
[1066] | 864 | | Osubpp sz ⇒ |
---|
[1288] | 865 | translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
[1066] | 866 | | Omul ⇒ |
---|
[1288] | 867 | translate_mul globals destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
[1066] | 868 | | Odivu ⇒ |
---|
[1288] | 869 | match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with |
---|
[1066] | 870 | [ cons hd tl ⇒ λcons_prf. |
---|
| 871 | match tl with |
---|
[1288] | 872 | [ nil ⇒ translate_divumodu8 globals true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def |
---|
[1066] | 873 | | _ ⇒ ? (* not implemented *) |
---|
| 874 | ] |
---|
| 875 | | nil ⇒ λnil_absrd. ? |
---|
| 876 | ] srcrs1_prf |
---|
| 877 | | Omodu ⇒ |
---|
[1288] | 878 | match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with |
---|
[1066] | 879 | [ cons hd tl ⇒ λcons_prf. |
---|
| 880 | match tl with |
---|
[1288] | 881 | [ nil ⇒ translate_divumodu8 globals false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def |
---|
[1066] | 882 | | _ ⇒ ? (* not implemented *) |
---|
| 883 | ] |
---|
| 884 | | nil ⇒ λnil_absrd. ? |
---|
| 885 | ] srcrs1_prf |
---|
| 886 | | Oand ⇒ |
---|
[1288] | 887 | translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
[1066] | 888 | | Oor ⇒ |
---|
[1288] | 889 | translate_op globals Or destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
[1066] | 890 | | Oxor ⇒ |
---|
[1288] | 891 | translate_op globals Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
[1066] | 892 | | Ocmp c ⇒ |
---|
[1064] | 893 | match c with |
---|
[1066] | 894 | [ Ceq ⇒ |
---|
[1288] | 895 | add_translates rtl_params1 globals [ |
---|
| 896 | translate_ne globals destrs srcrs1 srcrs2; |
---|
| 897 | translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) |
---|
[1064] | 898 | ] start_lbl dest_lbl def |
---|
[1288] | 899 | | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
| 900 | | Clt ⇒ translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def |
---|
| 901 | | Cgt ⇒ translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def |
---|
[1066] | 902 | | Cle ⇒ |
---|
[1288] | 903 | add_translates rtl_params1 globals [ |
---|
| 904 | translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?; |
---|
| 905 | translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) |
---|
[1064] | 906 | ] start_lbl dest_lbl def |
---|
[1066] | 907 | | Cge ⇒ |
---|
[1288] | 908 | add_translates rtl_params1 globals [ |
---|
| 909 | translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?; |
---|
| 910 | translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) |
---|
[1064] | 911 | ] start_lbl dest_lbl def |
---|
| 912 | ] |
---|
[1066] | 913 | | Ocmpu c ⇒ |
---|
| 914 | match c with |
---|
| 915 | [ Ceq ⇒ |
---|
[1288] | 916 | add_translates rtl_params1 globals [ |
---|
| 917 | translate_ne globals destrs srcrs1 srcrs2; |
---|
| 918 | translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) |
---|
[1066] | 919 | ] start_lbl dest_lbl def |
---|
[1288] | 920 | | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
| 921 | | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def |
---|
| 922 | | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def |
---|
[1066] | 923 | | Cle ⇒ |
---|
[1288] | 924 | add_translates rtl_params1 globals [ |
---|
| 925 | translate_lt globals destrs destrs_prf srcrs2 srcrs1; |
---|
| 926 | translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) |
---|
[1066] | 927 | ] start_lbl dest_lbl def |
---|
| 928 | | Cge ⇒ |
---|
[1288] | 929 | add_translates rtl_params1 globals [ |
---|
| 930 | translate_lt globals destrs destrs_prf srcrs1 srcrs2; |
---|
| 931 | translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) |
---|
[1066] | 932 | ] start_lbl dest_lbl def |
---|
| 933 | ] |
---|
| 934 | | Ocmpp c ⇒ |
---|
| 935 | match c with |
---|
| 936 | [ Ceq ⇒ |
---|
[1288] | 937 | add_translates rtl_params1 globals [ |
---|
| 938 | translate_ne globals destrs srcrs1 srcrs2; |
---|
| 939 | translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) |
---|
[1066] | 940 | ] start_lbl dest_lbl def |
---|
[1288] | 941 | | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def |
---|
| 942 | | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def |
---|
| 943 | | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def |
---|
[1066] | 944 | | Cle ⇒ |
---|
[1288] | 945 | add_translates rtl_params1 globals [ |
---|
| 946 | translate_lt globals destrs destrs_prf srcrs2 srcrs1; |
---|
| 947 | translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) |
---|
[1066] | 948 | ] start_lbl dest_lbl def |
---|
| 949 | | Cge ⇒ |
---|
[1288] | 950 | add_translates rtl_params1 globals [ |
---|
| 951 | translate_lt globals destrs destrs_prf srcrs1 srcrs2; |
---|
| 952 | translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|)) |
---|
[1066] | 953 | ] start_lbl dest_lbl def |
---|
| 954 | ] |
---|
| 955 | | _ ⇒ ? (* assert false, implemented in run time or float op *) |
---|
| 956 | ]. |
---|
| 957 | [ 2,6: normalize in nil_absrd; |
---|
| 958 | cases(not_le_Sn_O 0) |
---|
| 959 | #HYP cases(HYP nil_absrd) |
---|
| 960 | | 3,7,12,17,13,15,18,19,20,21,14,16: |
---|
| 961 | assumption |
---|
| 962 | | *: cases not_implemented (* yes, really *) |
---|
| 963 | ] |
---|
| 964 | qed. |
---|
| 965 | |
---|
[1288] | 966 | definition translate_cond: ∀globals: list ident. list register → label → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ |
---|
| 967 | λglobals: list ident. |
---|
[1066] | 968 | λsrcrs: list register. |
---|
| 969 | λstart_lbl: label. |
---|
| 970 | λlbl_true: label. |
---|
| 971 | λlbl_false: label. |
---|
[1288] | 972 | λdef: rtl_internal_function globals. |
---|
| 973 | let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in |
---|
| 974 | let 〈tmp_lbl, def〉 ≝ fresh_label rtl_params1 globals def in |
---|
| 975 | let init ≝ sequential rtl_params_ globals (INT rtl_params_ globals tmpr (zero …)) in |
---|
| 976 | let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in |
---|
| 977 | let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in |
---|
[1290] | 978 | add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def. |
---|
[1066] | 979 | |
---|
| 980 | definition translate_load ≝ |
---|
[1292] | 981 | λglobals: list ident. |
---|
[1066] | 982 | λaddr. |
---|
| 983 | λaddr_prf: 2 ≤ |addr|. |
---|
| 984 | λdestrs: list register. |
---|
| 985 | λstart_lbl: label. |
---|
| 986 | λdest_lbl: label. |
---|
[1292] | 987 | λdef: rtl_internal_function globals. |
---|
| 988 | match fresh_regs_strong rtl_params0 globals def (|addr|) with |
---|
[1066] | 989 | [ dp def_save_addr save_addr_prf ⇒ |
---|
| 990 | let def ≝ \fst def_save_addr in |
---|
| 991 | let save_addr ≝ \snd def_save_addr in |
---|
[1292] | 992 | match fresh_regs_strong rtl_params0 globals def (|addr|) with |
---|
[1066] | 993 | [ dp def_tmp_addr tmp_addr_prf ⇒ |
---|
| 994 | let def ≝ \fst def_tmp_addr in |
---|
| 995 | let tmp_addr ≝ \snd def_tmp_addr in |
---|
[1292] | 996 | let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in |
---|
| 997 | let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in |
---|
| 998 | let insts_save_addr ≝ translate_move globals save_addr addr in |
---|
[1066] | 999 | let f ≝ λtranslates_off. λr. |
---|
| 1000 | let 〈translates, off〉 ≝ translates_off in |
---|
| 1001 | let translates ≝ translates @ [ |
---|
[1292] | 1002 | adds_graph rtl_params1 globals [ |
---|
| 1003 | sequential rtl_params_ globals (INT rtl_params_ globals tmpr off) |
---|
[1066] | 1004 | ]; |
---|
[1292] | 1005 | translate_op2 globals Oaddp tmp_addr ? save_addr [tmpr] ? ?; |
---|
| 1006 | adds_graph rtl_params1 globals [ |
---|
| 1007 | sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2) |
---|
[1066] | 1008 | ] |
---|
| 1009 | ] |
---|
| 1010 | in |
---|
[1292] | 1011 | let 〈carry, result〉 ≝ half_add … off int_size in |
---|
[1066] | 1012 | 〈translates, result〉 |
---|
| 1013 | in |
---|
[1292] | 1014 | let 〈translates, ignore〉 ≝ foldl … f 〈[ ], (zero ?)〉 destrs in |
---|
| 1015 | add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def |
---|
[1066] | 1016 | ] |
---|
| 1017 | ]. |
---|
| 1018 | [1: normalize // |
---|
| 1019 | |2: >save_addr_prf normalize |
---|
| 1020 | @(transitive_le 1 2 (|addr|)) // |
---|
| 1021 | |3: >tmp_addr_prf normalize |
---|
| 1022 | @(transitive_le 1 2 (|addr|)) // |
---|
| 1023 | |*: >tmp_addr_prf assumption |
---|
| 1024 | ] |
---|
| 1025 | qed. |
---|
| 1026 | |
---|
| 1027 | definition translate_store ≝ |
---|
[1292] | 1028 | λglobals: list ident. |
---|
[1066] | 1029 | λaddr. |
---|
| 1030 | λaddr_prf: 2 ≤ |addr|. |
---|
| 1031 | λsrcrs: list register. |
---|
| 1032 | λstart_lbl: label. |
---|
| 1033 | λdest_lbl: label. |
---|
[1292] | 1034 | λdef: rtl_internal_function globals. |
---|
| 1035 | match fresh_regs_strong rtl_params0 globals def (|addr|) with |
---|
[1066] | 1036 | [ dp def_tmp_addr tmp_addr_prf ⇒ |
---|
| 1037 | let def ≝ \fst def_tmp_addr in |
---|
| 1038 | let tmp_addr ≝ \snd def_tmp_addr in |
---|
[1292] | 1039 | let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in |
---|
| 1040 | let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in |
---|
[1066] | 1041 | let f ≝ λtranslate_off. λsrcr. |
---|
| 1042 | let 〈translates, off〉 ≝ translate_off in |
---|
| 1043 | let translates ≝ translates @ [ |
---|
[1292] | 1044 | adds_graph rtl_params1 globals [ |
---|
| 1045 | sequential rtl_params_ globals (INT rtl_params_ globals tmpr off) |
---|
[1066] | 1046 | ]; |
---|
[1306] | 1047 | translate_op2 globals Oaddp tmp_addr … addr [tmpr] ? ?; |
---|
[1292] | 1048 | adds_graph rtl_params1 globals [ |
---|
| 1049 | sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr) |
---|
[1066] | 1050 | ] |
---|
| 1051 | ] |
---|
| 1052 | in |
---|
[1292] | 1053 | let 〈carry, result〉 ≝ half_add … off int_size in |
---|
[1066] | 1054 | 〈translates, result〉 |
---|
| 1055 | in |
---|
[1306] | 1056 | let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero …〉 srcrs in |
---|
[1292] | 1057 | add_translates rtl_params1 globals translates start_lbl dest_lbl def |
---|
[1066] | 1058 | ]. |
---|
| 1059 | [1: normalize // |
---|
| 1060 | |2: >tmp_addr_prf normalize |
---|
| 1061 | @(transitive_le 1 2 (|addr|)) // |
---|
| 1062 | |3: >tmp_addr_prf normalize |
---|
| 1063 | @(transitive_le 1 2 (|addr|)) // |
---|
| 1064 | |*: >tmp_addr_prf assumption |
---|
| 1065 | ] |
---|
| 1066 | qed. |
---|
| 1067 | |
---|
[1293] | 1068 | axiom fake_label: label. |
---|
| 1069 | |
---|
| 1070 | (* XXX: following conversation with CSC about the mix up in extension statements |
---|
[1296] | 1071 | and extension instructions in RTL, use fake_label in calls to |
---|
| 1072 | tailcall_* instructions. *) |
---|
[1066] | 1073 | definition translate_stmt ≝ |
---|
[1292] | 1074 | λglobals: list ident. |
---|
[1281] | 1075 | λlenv: local_env. |
---|
[1066] | 1076 | λlbl: label. |
---|
| 1077 | λstmt. |
---|
[1292] | 1078 | λdef: rtl_internal_function globals. |
---|
[1066] | 1079 | match stmt with |
---|
[1282] | 1080 | [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def |
---|
[1293] | 1081 | | St_cost cost_lbl lbl' ⇒ add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (COST_LABEL rtl_params_ globals cost_lbl) lbl') def |
---|
[1066] | 1082 | | St_const destr cst lbl' ⇒ |
---|
[1293] | 1083 | translate_cst globals cst (find_local_env destr lenv) lbl lbl' def |
---|
[1066] | 1084 | | St_op1 op1 destr srcr lbl' ⇒ |
---|
[1293] | 1085 | translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def |
---|
[1066] | 1086 | | St_op2 op2 destr srcr1 srcr2 lbl' ⇒ |
---|
[1306] | 1087 | translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def |
---|
[1307] | 1088 | (* XXX: should we be ignoring this? *) |
---|
[1066] | 1089 | | St_load ignore addr destr lbl' ⇒ |
---|
[1306] | 1090 | translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def |
---|
[1307] | 1091 | (* XXX: should we be ignoring this? *) |
---|
[1066] | 1092 | | St_store ignore addr srcr lbl' ⇒ |
---|
[1306] | 1093 | translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def |
---|
[1066] | 1094 | | St_call_id f args retr lbl' ⇒ |
---|
| 1095 | match retr with |
---|
| 1096 | [ Some retr ⇒ |
---|
[1293] | 1097 | add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) (find_local_env retr lenv)) lbl') def |
---|
| 1098 | | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) [ ]) lbl') def |
---|
[1066] | 1099 | ] |
---|
| 1100 | | St_call_ptr f args retr lbl' ⇒ |
---|
| 1101 | match retr with |
---|
| 1102 | [ None ⇒ |
---|
| 1103 | let 〈f1, f2〉 ≝ find_and_addr f lenv ? in |
---|
[1293] | 1104 | add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])) lbl') def |
---|
[1066] | 1105 | | Some retr ⇒ |
---|
| 1106 | let 〈f1, f2〉 ≝ find_and_addr f lenv ? in |
---|
[1293] | 1107 | add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))) lbl') def |
---|
[1066] | 1108 | ] |
---|
| 1109 | | St_tailcall_id f args ⇒ |
---|
[1293] | 1110 | add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) fake_label) def |
---|
[1066] | 1111 | | St_tailcall_ptr f args ⇒ |
---|
| 1112 | let 〈f1, f2〉 ≝ find_and_addr f lenv ? in |
---|
[1293] | 1113 | add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) fake_label) def |
---|
[1066] | 1114 | | St_cond r lbl_true lbl_false ⇒ |
---|
[1292] | 1115 | translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def |
---|
[1066] | 1116 | | St_jumptable r l ⇒ ? (* assert false: not implemented yet *) |
---|
[1292] | 1117 | | St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def |
---|
[1064] | 1118 | ]. |
---|
[1067] | 1119 | [10: cases not_implemented (* jtable case *) |
---|
| 1120 | |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *) |
---|
| 1121 | ] |
---|
| 1122 | qed. |
---|
[1064] | 1123 | |
---|
[1073] | 1124 | (* XXX: we use a "hack" here to circumvent the proof obligations required to |
---|
| 1125 | create res, an empty internal_function record. we insert into our graph |
---|
| 1126 | the start and end nodes to ensure that they are in, and place dummy |
---|
| 1127 | skip instructions at these nodes. *) |
---|
[1067] | 1128 | definition translate_internal ≝ |
---|
[1293] | 1129 | λglobals: list ident. |
---|
| 1130 | λdef. |
---|
[1067] | 1131 | let runiverse ≝ f_reggen def in |
---|
[1281] | 1132 | let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse |
---|
[1068] | 1133 | (f_params def @ f_locals def) (f_result def) in |
---|
[1292] | 1134 | let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in |
---|
| 1135 | let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in |
---|
[1149] | 1136 | let result ≝ |
---|
[1068] | 1137 | match (f_result def) with |
---|
| 1138 | [ None ⇒ [ ] |
---|
| 1139 | | Some r_typ ⇒ |
---|
| 1140 | let 〈r, typ〉 ≝ r_typ in |
---|
| 1141 | find_local_env r lenv |
---|
[1053] | 1142 | ] |
---|
[1068] | 1143 | in |
---|
| 1144 | let luniverse' ≝ f_labgen def in |
---|
| 1145 | let runiverse' ≝ runiverse in |
---|
| 1146 | let result' ≝ result in |
---|
| 1147 | let params' ≝ params in |
---|
| 1148 | let locals' ≝ locals in |
---|
| 1149 | let stack_size' ≝ f_stacksize def in |
---|
| 1150 | let entry' ≝ f_entry def in |
---|
| 1151 | let exit' ≝ f_exit def in |
---|
[1293] | 1152 | let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params_ globals entry') in |
---|
| 1153 | let graph' ≝ add LabelTag ? graph' exit' (GOTO rtl_params_ globals exit') in |
---|
[1068] | 1154 | let res ≝ |
---|
[1281] | 1155 | mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params' |
---|
| 1156 | locals' stack_size' graph' ? ? in |
---|
[1293] | 1157 | foldi … (translate_stmt globals … lenv) (f_graph def) res. |
---|
[1281] | 1158 | [ % [@entry' | @graph_add_lookup @graph_add] |
---|
| 1159 | | % [@exit' | @graph_add]] |
---|
[1073] | 1160 | qed. |
---|
[1053] | 1161 | |
---|
[1239] | 1162 | (*CSC: here we are not doing any alignment on variables, like it is done in OCaml |
---|
| 1163 | because of CompCert heritage *) |
---|
[1293] | 1164 | definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝ |
---|
| 1165 | λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))). |
---|