From 36d2932273444ef76219c7eb4b8a031e3b67e609 Mon Sep 17 00:00:00 2001 From: Santiago Arranz Olmos Date: Mon, 7 Oct 2024 22:41:02 +0100 Subject: [PATCH 1/2] Split large offset memory operations in ARM --- CHANGELOG.md | 5 + compiler/config/tests.config | 10 +- compiler/src/arm_arch_full.ml | 2 + compiler/src/compile.ml | 20 +- compiler/src/pp_arm_m4.ml | 9 + compiler/src/printer.ml | 3 - compiler/src/printer.mli | 1 - compiler/src/regalloc.ml | 28 +- compiler/src/stackAlloc.ml | 1 + compiler/src/utils.ml | 1 + compiler/src/utils.mli | 1 + .../arm-m4/large_memory_immediates/basic.jazz | 21 + .../large_memory_immediates/intrinsics.jazz | 21 + .../large_internal_array.jazz | 23 + .../too_many_stack_variables.jazz | 510 ++++++++++++++ proofs/arch/arm_expand_imm.v | 11 +- proofs/compiler/arm_extra.v | 290 +++++++- proofs/compiler/arm_params.v | 62 ++ proofs/compiler/arm_params_core_proof.v | 2 +- proofs/compiler/arm_params_proof.v | 629 +++++++++++++++++- proofs/compiler/arm_stack_zeroization.v | 33 +- proofs/compiler/arm_stack_zeroization_proof.v | 71 +- proofs/compiler/compiler.v | 1 + proofs/compiler/compiler_proof.v | 2 +- proofs/compiler/compiler_util.v | 4 +- proofs/compiler/stack_alloc.v | 47 +- proofs/compiler/stack_alloc_proof.v | 10 +- proofs/compiler/stack_alloc_proof_2.v | 43 +- proofs/compiler/x86_params.v | 1 + proofs/compiler/x86_params_proof.v | 4 + proofs/lang/fexpr.v | 32 +- proofs/lang/fexpr_facts.v | 64 +- proofs/lang/utils.v | 2 + 33 files changed, 1834 insertions(+), 130 deletions(-) create mode 100644 compiler/tests/success/arm-m4/large_memory_immediates/basic.jazz create mode 100644 compiler/tests/success/arm-m4/large_memory_immediates/intrinsics.jazz create mode 100644 compiler/tests/success/arm-m4/large_memory_immediates/large_internal_array.jazz create mode 100644 compiler/tests/success/arm-m4/large_memory_immediates/too_many_stack_variables.jazz diff --git a/CHANGELOG.md b/CHANGELOG.md index 0a24a334f..840d4d783 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -70,6 +70,11 @@ ([PR #955](https://github.com/jasmin-lang/jasmin/pull/955); fixes [#950](https://github.com/jasmin-lang/jasmin/issues/950)). +- The compiler now introduces several instructions for memory operations whose + offsets are too large for the ARM encoding + ([PR #741](https://github.com/jasmin-lang/jasmin/pull/741)). It issues a + warning in these cases. + # Jasmin 2024.07.1 — Nancy, 2024-10-03 ## New features diff --git a/compiler/config/tests.config b/compiler/config/tests.config index 822aac6a5..f0ddc9d0e 100644 --- a/compiler/config/tests.config +++ b/compiler/config/tests.config @@ -54,18 +54,18 @@ exclude = tests/success/noextract [test-arm-m4] bin = ./scripts/check-arm-m4 -okdirs = examples/**/arm-m4 tests/success/**/arm-m4 tests/success/**/common +okdirs = examples/**/arm-m4 tests/success/**/arm-m4 tests/success/**/common tests/success/arm-m4/large_memory_immediates kodirs = tests/fail/**/arm-m4 tests/fail/**/common [test-arm-m4-print] bin = ./scripts/parse-print-parse args = arm -okdirs = tests/success/**/arm-m4 tests/success/**/common +okdirs = tests/success/**/arm-m4 tests/success/**/common tests/success/arm-m4/large_memory_immediates [test-arm-m4-extraction] bin = ./scripts/extract-and-check args = arm -okdirs = examples/**/arm-m4 tests/success/**/arm-m4 tests/success/**/common +okdirs = examples/**/arm-m4 tests/success/**/arm-m4 tests/success/**/common tests/success/arm-m4/large_memory_immediates exclude = tests/success/noextract [test-x86-64-stack-zero-loop] @@ -85,7 +85,7 @@ exclude = tests/fail/warning [test-arm-m4-stack-zero-loop] bin = ./scripts/check-arm-m4 args = -stack-zero=loop -okdirs = examples/**/arm-m4 tests/success/**/arm-m4 +okdirs = examples/**/arm-m4 tests/success/**/arm-m4 tests/success/arm-m4/large_memory_immediates kodirs = tests/fail/**/arm-m4 [test-arm-m4-stack-zero-unrolled] @@ -93,4 +93,4 @@ bin = ./scripts/check-arm-m4 args = -stack-zero=unrolled okdirs = examples/**/arm-m4 tests/success/**/arm-m4 kodirs = tests/fail/**/arm-m4 -exclude = tests/success/arm-m4/large_stack +exclude = tests/success/arm-m4/large_stack tests/success/arm-m4/large_memory_immediates diff --git a/compiler/src/arm_arch_full.ml b/compiler/src/arm_arch_full.ml index 3ffe72b3e..9cfce3c5e 100644 --- a/compiler/src/arm_arch_full.ml +++ b/compiler/src/arm_arch_full.ml @@ -99,6 +99,8 @@ module Arm_core = struct | Oarm_swap _ -> true | Oarm_add_large_imm -> true | (Osmart_li _ | Osmart_li_cc _) -> true (* emit MOVT *) + | Olarge_load _ | Olarge_load_cc _ | Olarge_store _ | Olarge_store_cc _ -> + true (* emit MOV, MOVT, STR *) end diff --git a/compiler/src/compile.ml b/compiler/src/compile.ml index 5ed0c7e14..264d7062b 100644 --- a/compiler/src/compile.ml +++ b/compiler/src/compile.ml @@ -183,10 +183,22 @@ let compile (type reg regx xreg rflag cond asm_op extra_op) (fn, f) |> Conv.fdef_of_cufdef |> refresh_i_loc_f |> Conv.cufdef_of_fdef |> snd in - let warning ii msg = - (if not !Glob_options.lea then - let loc, _ = ii in - warning UseLea loc "%a" Printer.pp_warning_msg msg); + let warning ii w = + let o = + match w with + | Compiler_util.Use_lea -> + if not !Glob_options.lea + then Some (UseLea, "LEA instruction is used") + else None + | Split_memory_access -> + let msg = + "This memory immediate does not fit in one instruction, several \ + instructions were issued." + in + Some (SplitMemoryAccess, msg) + in + let loc, _ = ii in + Option.may (fun (w, msg) -> warning w loc "%s" msg) o; ii in diff --git a/compiler/src/pp_arm_m4.ml b/compiler/src/pp_arm_m4.ml index 76d97c5ca..708fab513 100644 --- a/compiler/src/pp_arm_m4.ml +++ b/compiler/src/pp_arm_m4.ml @@ -213,6 +213,13 @@ end = struct let chk_imm_w16_encoding args n opts = chk_imm args n (chk_w16_encoding opts) (chk_w16_encoding opts) + let chk_mem_immediate args n = + match List.at args n with + | _, Addr(Areg(addr)) -> + let n = Word0.wsigned Wsize.U32 addr.ad_disp in + if not (is_mem_immediate n) then exn_imm_too_big n + | _, _ -> () + let check_args (ARM_op (mn, opts)) args = match mn with | ADC | SBC | RSB -> chk_imm_accept_shift args 2 @@ -221,6 +228,8 @@ end = struct | MOV -> chk_imm_w16_encoding args 1 opts | AND | BIC | EOR | ORR -> chk_imm_reject_shift args 2 | MVN | TST -> chk_imm_reject_shift args 1 + | LDR | LDRB | LDRH -> chk_mem_immediate args 1; "" (* Should not happen. *) + | STR | STRB | STRH -> chk_mem_immediate args 1; "" (* Should not happen. *) | _ -> "" end diff --git a/compiler/src/printer.ml b/compiler/src/printer.ml index 23b8cf69b..bf26134b3 100644 --- a/compiler/src/printer.ml +++ b/compiler/src/printer.ml @@ -409,9 +409,6 @@ let pp_sprog ~debug pd asmOp fmt ((funcs, p_extra):('info, 'asm) Prog.sprog) = (* ----------------------------------------------------------------------- *) -let pp_warning_msg fmt = function - | Compiler_util.Use_lea -> Format.fprintf fmt "LEA instruction is used" - let pp_err ~debug fmt (pp_e : Compiler_util.pp_error) = let pp_var fmt v = let v = Conv.var_of_cvar v in diff --git a/compiler/src/printer.mli b/compiler/src/printer.mli index cd327db77..b02c7552b 100644 --- a/compiler/src/printer.mli +++ b/compiler/src/printer.mli @@ -1,6 +1,5 @@ open Prog -val pp_warning_msg : Format.formatter -> Compiler_util.warning_msg -> unit val pp_err : debug:bool -> Format.formatter -> Compiler_util.pp_error -> unit val pp_print_X : Format.formatter -> Z.t -> unit diff --git a/compiler/src/regalloc.ml b/compiler/src/regalloc.ml index 68822dee7..7aa4ac9e1 100644 --- a/compiler/src/regalloc.ml +++ b/compiler/src/regalloc.ml @@ -88,19 +88,23 @@ let find_equality_constraints (id: instruction_desc) : arg_position list list = | _ -> apl :: res) tbl [] -let find_var outs ins ap : _ option = - let oget = function - | Some x -> x - | None -> hierror_reg ~loc:Lnone ~internal:true "the instruction description is not correct" in +let find_var outs ins ap = + let err () = + hierror_reg + ~loc:Lnone ~internal:true "the instruction description is not correct" + in + let get_lvar = function + | Lvar v | Lmem(_, _, v, _) -> Some v + | _ -> None + in + let get_evar = function + | Pvar v when is_gkvar v -> Some v.gv + | Pload(_, _, v, _) -> Some v + | _ -> None + in match ap with - | APout n -> - Oseq.onth outs n |> oget |> - (function Lvar v -> Some v | _ -> None) - | APin n -> - Oseq.onth ins n |> oget |> - (function - | Pvar v -> if is_gkvar v then Some v.gv else None - | _ -> None) + | APout n -> Oseq.onth outs n |> Option.default_delayed err |> get_lvar + | APin n -> Oseq.onth ins n |> Option.default_delayed err |> get_evar let asm_equality_constraints ~loc pd reg_size asmOp is_move_op (int_of_var: var_i -> int option) (k: int -> int -> unit) (k': int -> int -> unit) diff --git a/compiler/src/stackAlloc.ml b/compiler/src/stackAlloc.ml index 781d9219c..77c91de67 100644 --- a/compiler/src/stackAlloc.ml +++ b/compiler/src/stackAlloc.ml @@ -190,6 +190,7 @@ let memory_analysis pp_err ~debug up = gao.gao_data cglobs get_sao + (fun ii _ -> ii) up with | Utils0.Ok sp -> sp diff --git a/compiler/src/utils.ml b/compiler/src/utils.ml index dc7781733..f3fddd45e 100644 --- a/compiler/src/utils.ml +++ b/compiler/src/utils.ml @@ -420,6 +420,7 @@ type warning = | SimplifyVectorSuffix | DuplicateVar | UnusedVar + | SplitMemoryAccess | SCTchecker | Deprecated | Experimental diff --git a/compiler/src/utils.mli b/compiler/src/utils.mli index ee03047a5..e36bef066 100644 --- a/compiler/src/utils.mli +++ b/compiler/src/utils.mli @@ -180,6 +180,7 @@ type warning = | SimplifyVectorSuffix | DuplicateVar | UnusedVar + | SplitMemoryAccess | SCTchecker | Deprecated | Experimental diff --git a/compiler/tests/success/arm-m4/large_memory_immediates/basic.jazz b/compiler/tests/success/arm-m4/large_memory_immediates/basic.jazz new file mode 100644 index 000000000..37031c341 --- /dev/null +++ b/compiler/tests/success/arm-m4/large_memory_immediates/basic.jazz @@ -0,0 +1,21 @@ +export +fn basic(reg u32 p) -> reg u32 { + [p + 4096] = p; + (u8)[p + 4096] = p; + (u16)[p + 4096] = p; + p = [p + 4096]; + p = (32u)(u8)[p + 4096]; + p = (32u)(u16)[p + 4096]; + + reg bool b; + b = p <= 3; + [p + 4096] = p if b; + (u8)[p + 4096] = p if b; + (u16)[p + 4096] = p if b; + p = [p + 4096] if b; + p = (32u)(u8)[p + 4096] if b; + p = (32u)(u16)[p + 4096] if b; + + p = p; + return p; +} diff --git a/compiler/tests/success/arm-m4/large_memory_immediates/intrinsics.jazz b/compiler/tests/success/arm-m4/large_memory_immediates/intrinsics.jazz new file mode 100644 index 000000000..abe8837e0 --- /dev/null +++ b/compiler/tests/success/arm-m4/large_memory_immediates/intrinsics.jazz @@ -0,0 +1,21 @@ +export +fn intrinsics(reg u32 p) -> reg u32 { + [p + 4096] = #STR(p); + (u8)[p + 4096] = #STRB(p); + (u16)[p + 4096] = #STRH(p); + p = #LDR([p + 4096]); + p = #LDRB((u8)[p + 4096]); + p = #LDRH((u16)[p + 4096]); + + reg bool b; + b = p <= 3; + [p + 4096] = #STRcc(p, b, [p + 4096]); + (u8)[p + 4096] = #STRBcc(p, b, (u8)[p + 4096]); + (u16)[p + 4096] = #STRHcc(p, b, (u16)[p + 4096]); + p = #LDRcc([p + 4096], b, p); + p = #LDRBcc((u8)[p + 4096], b, p); + p = #LDRHcc((u16)[p + 4096], b, p); + + p = p; + return p; +} diff --git a/compiler/tests/success/arm-m4/large_memory_immediates/large_internal_array.jazz b/compiler/tests/success/arm-m4/large_memory_immediates/large_internal_array.jazz new file mode 100644 index 000000000..a94d8ec7c --- /dev/null +++ b/compiler/tests/success/arm-m4/large_memory_immediates/large_internal_array.jazz @@ -0,0 +1,23 @@ +// Stack allocation needs to split the array set and get operations into several +// instructions to that the immediates fit in one instruction. + +// The LDR/STR instructions take an immediate of up to 12 bits. +// Since elements are 4 bytes, we the size limit for an array is 2^12 / 4. +param int LIMIT = 1024; + +export +fn large_array() -> reg u32 { + reg u32 r; + stack u32[LIMIT + 1] a; + + r = 0; + a[LIMIT] = r; + r = a[LIMIT]; + + reg bool b; + b = r <= 3; + a[LIMIT] = r if b; + r = a[LIMIT] if b; + + return r; +} diff --git a/compiler/tests/success/arm-m4/large_memory_immediates/too_many_stack_variables.jazz b/compiler/tests/success/arm-m4/large_memory_immediates/too_many_stack_variables.jazz new file mode 100644 index 000000000..eea4b1377 --- /dev/null +++ b/compiler/tests/success/arm-m4/large_memory_immediates/too_many_stack_variables.jazz @@ -0,0 +1,510 @@ +// Stack allocation needs to split the array set and get operations into several +// instructions to that the immediates fit in one instruction. + +// The LDR/STR instructions take an immediate of up to 12 bits. +// Since elements are 4 bytes, we the size limit for an array is 2^12 / 4. +export +fn too_many_stack_variables() -> reg u32 { + reg u32 z; + z = 0; + + stack u32 + s0000 s0001 s0002 s0003 s0004 s0005 s0006 s0007 s0008 s0009 s0010 s0011 + s0012 s0013 s0014 s0015 s0016 s0017 s0018 s0019 s0020 s0021 s0022 s0023 + s0024 s0025 s0026 s0027 s0028 s0029 s0030 s0031 s0032 s0033 s0034 s0035 + s0036 s0037 s0038 s0039 s0040 s0041 s0042 s0043 s0044 s0045 s0046 s0047 + s0048 s0049 s0050 s0051 s0052 s0053 s0054 s0055 s0056 s0057 s0058 s0059 + s0060 s0061 s0062 s0063 s0064 s0065 s0066 s0067 s0068 s0069 s0070 s0071 + s0072 s0073 s0074 s0075 s0076 s0077 s0078 s0079 s0080 s0081 s0082 s0083 + s0084 s0085 s0086 s0087 s0088 s0089 s0090 s0091 s0092 s0093 s0094 s0095 + s0096 s0097 s0098 s0099 s0100 s0101 s0102 s0103 s0104 s0105 s0106 s0107 + s0108 s0109 s0110 s0111 s0112 s0113 s0114 s0115 s0116 s0117 s0118 s0119 + s0120 s0121 s0122 s0123 s0124 s0125 s0126 s0127 s0128 s0129 s0130 s0131 + s0132 s0133 s0134 s0135 s0136 s0137 s0138 s0139 s0140 s0141 s0142 s0143 + s0144 s0145 s0146 s0147 s0148 s0149 s0150 s0151 s0152 s0153 s0154 s0155 + s0156 s0157 s0158 s0159 s0160 s0161 s0162 s0163 s0164 s0165 s0166 s0167 + s0168 s0169 s0170 s0171 s0172 s0173 s0174 s0175 s0176 s0177 s0178 s0179 + s0180 s0181 s0182 s0183 s0184 s0185 s0186 s0187 s0188 s0189 s0190 s0191 + s0192 s0193 s0194 s0195 s0196 s0197 s0198 s0199 s0200 s0201 s0202 s0203 + s0204 s0205 s0206 s0207 s0208 s0209 s0210 s0211 s0212 s0213 s0214 s0215 + s0216 s0217 s0218 s0219 s0220 s0221 s0222 s0223 s0224 s0225 s0226 s0227 + s0228 s0229 s0230 s0231 s0232 s0233 s0234 s0235 s0236 s0237 s0238 s0239 + s0240 s0241 s0242 s0243 s0244 s0245 s0246 s0247 s0248 s0249 s0250 s0251 + s0252 s0253 s0254 s0255 s0256 s0257 s0258 s0259 s0260 s0261 s0262 s0263 + s0264 s0265 s0266 s0267 s0268 s0269 s0270 s0271 s0272 s0273 s0274 s0275 + s0276 s0277 s0278 s0279 s0280 s0281 s0282 s0283 s0284 s0285 s0286 s0287 + s0288 s0289 s0290 s0291 s0292 s0293 s0294 s0295 s0296 s0297 s0298 s0299 + s0300 s0301 s0302 s0303 s0304 s0305 s0306 s0307 s0308 s0309 s0310 s0311 + s0312 s0313 s0314 s0315 s0316 s0317 s0318 s0319 s0320 s0321 s0322 s0323 + s0324 s0325 s0326 s0327 s0328 s0329 s0330 s0331 s0332 s0333 s0334 s0335 + s0336 s0337 s0338 s0339 s0340 s0341 s0342 s0343 s0344 s0345 s0346 s0347 + s0348 s0349 s0350 s0351 s0352 s0353 s0354 s0355 s0356 s0357 s0358 s0359 + s0360 s0361 s0362 s0363 s0364 s0365 s0366 s0367 s0368 s0369 s0370 s0371 + s0372 s0373 s0374 s0375 s0376 s0377 s0378 s0379 s0380 s0381 s0382 s0383 + s0384 s0385 s0386 s0387 s0388 s0389 s0390 s0391 s0392 s0393 s0394 s0395 + s0396 s0397 s0398 s0399 s0400 s0401 s0402 s0403 s0404 s0405 s0406 s0407 + s0408 s0409 s0410 s0411 s0412 s0413 s0414 s0415 s0416 s0417 s0418 s0419 + s0420 s0421 s0422 s0423 s0424 s0425 s0426 s0427 s0428 s0429 s0430 s0431 + s0432 s0433 s0434 s0435 s0436 s0437 s0438 s0439 s0440 s0441 s0442 s0443 + s0444 s0445 s0446 s0447 s0448 s0449 s0450 s0451 s0452 s0453 s0454 s0455 + s0456 s0457 s0458 s0459 s0460 s0461 s0462 s0463 s0464 s0465 s0466 s0467 + s0468 s0469 s0470 s0471 s0472 s0473 s0474 s0475 s0476 s0477 s0478 s0479 + s0480 s0481 s0482 s0483 s0484 s0485 s0486 s0487 s0488 s0489 s0490 s0491 + s0492 s0493 s0494 s0495 s0496 s0497 s0498 s0499 s0500 s0501 s0502 s0503 + s0504 s0505 s0506 s0507 s0508 s0509 s0510 s0511 s0512 s0513 s0514 s0515 + s0516 s0517 s0518 s0519 s0520 s0521 s0522 s0523 s0524 s0525 s0526 s0527 + s0528 s0529 s0530 s0531 s0532 s0533 s0534 s0535 s0536 s0537 s0538 s0539 + s0540 s0541 s0542 s0543 s0544 s0545 s0546 s0547 s0548 s0549 s0550 s0551 + s0552 s0553 s0554 s0555 s0556 s0557 s0558 s0559 s0560 s0561 s0562 s0563 + s0564 s0565 s0566 s0567 s0568 s0569 s0570 s0571 s0572 s0573 s0574 s0575 + s0576 s0577 s0578 s0579 s0580 s0581 s0582 s0583 s0584 s0585 s0586 s0587 + s0588 s0589 s0590 s0591 s0592 s0593 s0594 s0595 s0596 s0597 s0598 s0599 + s0600 s0601 s0602 s0603 s0604 s0605 s0606 s0607 s0608 s0609 s0610 s0611 + s0612 s0613 s0614 s0615 s0616 s0617 s0618 s0619 s0620 s0621 s0622 s0623 + s0624 s0625 s0626 s0627 s0628 s0629 s0630 s0631 s0632 s0633 s0634 s0635 + s0636 s0637 s0638 s0639 s0640 s0641 s0642 s0643 s0644 s0645 s0646 s0647 + s0648 s0649 s0650 s0651 s0652 s0653 s0654 s0655 s0656 s0657 s0658 s0659 + s0660 s0661 s0662 s0663 s0664 s0665 s0666 s0667 s0668 s0669 s0670 s0671 + s0672 s0673 s0674 s0675 s0676 s0677 s0678 s0679 s0680 s0681 s0682 s0683 + s0684 s0685 s0686 s0687 s0688 s0689 s0690 s0691 s0692 s0693 s0694 s0695 + s0696 s0697 s0698 s0699 s0700 s0701 s0702 s0703 s0704 s0705 s0706 s0707 + s0708 s0709 s0710 s0711 s0712 s0713 s0714 s0715 s0716 s0717 s0718 s0719 + s0720 s0721 s0722 s0723 s0724 s0725 s0726 s0727 s0728 s0729 s0730 s0731 + s0732 s0733 s0734 s0735 s0736 s0737 s0738 s0739 s0740 s0741 s0742 s0743 + s0744 s0745 s0746 s0747 s0748 s0749 s0750 s0751 s0752 s0753 s0754 s0755 + s0756 s0757 s0758 s0759 s0760 s0761 s0762 s0763 s0764 s0765 s0766 s0767 + s0768 s0769 s0770 s0771 s0772 s0773 s0774 s0775 s0776 s0777 s0778 s0779 + s0780 s0781 s0782 s0783 s0784 s0785 s0786 s0787 s0788 s0789 s0790 s0791 + s0792 s0793 s0794 s0795 s0796 s0797 s0798 s0799 s0800 s0801 s0802 s0803 + s0804 s0805 s0806 s0807 s0808 s0809 s0810 s0811 s0812 s0813 s0814 s0815 + s0816 s0817 s0818 s0819 s0820 s0821 s0822 s0823 s0824 s0825 s0826 s0827 + s0828 s0829 s0830 s0831 s0832 s0833 s0834 s0835 s0836 s0837 s0838 s0839 + s0840 s0841 s0842 s0843 s0844 s0845 s0846 s0847 s0848 s0849 s0850 s0851 + s0852 s0853 s0854 s0855 s0856 s0857 s0858 s0859 s0860 s0861 s0862 s0863 + s0864 s0865 s0866 s0867 s0868 s0869 s0870 s0871 s0872 s0873 s0874 s0875 + s0876 s0877 s0878 s0879 s0880 s0881 s0882 s0883 s0884 s0885 s0886 s0887 + s0888 s0889 s0890 s0891 s0892 s0893 s0894 s0895 s0896 s0897 s0898 s0899 + s0900 s0901 s0902 s0903 s0904 s0905 s0906 s0907 s0908 s0909 s0910 s0911 + s0912 s0913 s0914 s0915 s0916 s0917 s0918 s0919 s0920 s0921 s0922 s0923 + s0924 s0925 s0926 s0927 s0928 s0929 s0930 s0931 s0932 s0933 s0934 s0935 + s0936 s0937 s0938 s0939 s0940 s0941 s0942 s0943 s0944 s0945 s0946 s0947 + s0948 s0949 s0950 s0951 s0952 s0953 s0954 s0955 s0956 s0957 s0958 s0959 + s0960 s0961 s0962 s0963 s0964 s0965 s0966 s0967 s0968 s0969 s0970 s0971 + s0972 s0973 s0974 s0975 s0976 s0977 s0978 s0979 s0980 s0981 s0982 s0983 + s0984 s0985 s0986 s0987 s0988 s0989 s0990 s0991 s0992 s0993 s0994 s0995 + s0996 s0997 s0998 s0999 s1000 s1001 s1002 s1003 s1004 s1005 s1006 s1007 + s1008 s1009 s1010 s1011 s1012 s1013 s1014 s1015 s1016 s1017 s1018 s1019 + s1020 s1021 s1022 s1023 s1024; + + + s0000 = z; s0001 = z; s0002 = z; s0003 = z; s0004 = z; s0005 = z; s0006 = z; + s0007 = z; s0008 = z; s0009 = z; s0010 = z; s0011 = z; s0012 = z; s0013 = z; + s0014 = z; s0015 = z; s0016 = z; s0017 = z; s0018 = z; s0019 = z; s0020 = z; + s0021 = z; s0022 = z; s0023 = z; s0024 = z; s0025 = z; s0026 = z; s0027 = z; + s0028 = z; s0029 = z; s0030 = z; s0031 = z; s0032 = z; s0033 = z; s0034 = z; + s0035 = z; s0036 = z; s0037 = z; s0038 = z; s0039 = z; s0040 = z; s0041 = z; + s0042 = z; s0043 = z; s0044 = z; s0045 = z; s0046 = z; s0047 = z; s0048 = z; + s0049 = z; s0050 = z; s0051 = z; s0052 = z; s0053 = z; s0054 = z; s0055 = z; + s0056 = z; s0057 = z; s0058 = z; s0059 = z; s0060 = z; s0061 = z; s0062 = z; + s0063 = z; s0064 = z; s0065 = z; s0066 = z; s0067 = z; s0068 = z; s0069 = z; + s0070 = z; s0071 = z; s0072 = z; s0073 = z; s0074 = z; s0075 = z; s0076 = z; + s0077 = z; s0078 = z; s0079 = z; s0080 = z; s0081 = z; s0082 = z; s0083 = z; + s0084 = z; s0085 = z; s0086 = z; s0087 = z; s0088 = z; s0089 = z; s0090 = z; + s0091 = z; s0092 = z; s0093 = z; s0094 = z; s0095 = z; s0096 = z; s0097 = z; + s0098 = z; s0099 = z; s0100 = z; s0101 = z; s0102 = z; s0103 = z; s0104 = z; + s0105 = z; s0106 = z; s0107 = z; s0108 = z; s0109 = z; s0110 = z; s0111 = z; + s0112 = z; s0113 = z; s0114 = z; s0115 = z; s0116 = z; s0117 = z; s0118 = z; + s0119 = z; s0120 = z; s0121 = z; s0122 = z; s0123 = z; s0124 = z; s0125 = z; + s0126 = z; s0127 = z; s0128 = z; s0129 = z; s0130 = z; s0131 = z; s0132 = z; + s0133 = z; s0134 = z; s0135 = z; s0136 = z; s0137 = z; s0138 = z; s0139 = z; + s0140 = z; s0141 = z; s0142 = z; s0143 = z; s0144 = z; s0145 = z; s0146 = z; + s0147 = z; s0148 = z; s0149 = z; s0150 = z; s0151 = z; s0152 = z; s0153 = z; + s0154 = z; s0155 = z; s0156 = z; s0157 = z; s0158 = z; s0159 = z; s0160 = z; + s0161 = z; s0162 = z; s0163 = z; s0164 = z; s0165 = z; s0166 = z; s0167 = z; + s0168 = z; s0169 = z; s0170 = z; s0171 = z; s0172 = z; s0173 = z; s0174 = z; + s0175 = z; s0176 = z; s0177 = z; s0178 = z; s0179 = z; s0180 = z; s0181 = z; + s0182 = z; s0183 = z; s0184 = z; s0185 = z; s0186 = z; s0187 = z; s0188 = z; + s0189 = z; s0190 = z; s0191 = z; s0192 = z; s0193 = z; s0194 = z; s0195 = z; + s0196 = z; s0197 = z; s0198 = z; s0199 = z; s0200 = z; s0201 = z; s0202 = z; + s0203 = z; s0204 = z; s0205 = z; s0206 = z; s0207 = z; s0208 = z; s0209 = z; + s0210 = z; s0211 = z; s0212 = z; s0213 = z; s0214 = z; s0215 = z; s0216 = z; + s0217 = z; s0218 = z; s0219 = z; s0220 = z; s0221 = z; s0222 = z; s0223 = z; + s0224 = z; s0225 = z; s0226 = z; s0227 = z; s0228 = z; s0229 = z; s0230 = z; + s0231 = z; s0232 = z; s0233 = z; s0234 = z; s0235 = z; s0236 = z; s0237 = z; + s0238 = z; s0239 = z; s0240 = z; s0241 = z; s0242 = z; s0243 = z; s0244 = z; + s0245 = z; s0246 = z; s0247 = z; s0248 = z; s0249 = z; s0250 = z; s0251 = z; + s0252 = z; s0253 = z; s0254 = z; s0255 = z; s0256 = z; s0257 = z; s0258 = z; + s0259 = z; s0260 = z; s0261 = z; s0262 = z; s0263 = z; s0264 = z; s0265 = z; + s0266 = z; s0267 = z; s0268 = z; s0269 = z; s0270 = z; s0271 = z; s0272 = z; + s0273 = z; s0274 = z; s0275 = z; s0276 = z; s0277 = z; s0278 = z; s0279 = z; + s0280 = z; s0281 = z; s0282 = z; s0283 = z; s0284 = z; s0285 = z; s0286 = z; + s0287 = z; s0288 = z; s0289 = z; s0290 = z; s0291 = z; s0292 = z; s0293 = z; + s0294 = z; s0295 = z; s0296 = z; s0297 = z; s0298 = z; s0299 = z; s0300 = z; + s0301 = z; s0302 = z; s0303 = z; s0304 = z; s0305 = z; s0306 = z; s0307 = z; + s0308 = z; s0309 = z; s0310 = z; s0311 = z; s0312 = z; s0313 = z; s0314 = z; + s0315 = z; s0316 = z; s0317 = z; s0318 = z; s0319 = z; s0320 = z; s0321 = z; + s0322 = z; s0323 = z; s0324 = z; s0325 = z; s0326 = z; s0327 = z; s0328 = z; + s0329 = z; s0330 = z; s0331 = z; s0332 = z; s0333 = z; s0334 = z; s0335 = z; + s0336 = z; s0337 = z; s0338 = z; s0339 = z; s0340 = z; s0341 = z; s0342 = z; + s0343 = z; s0344 = z; s0345 = z; s0346 = z; s0347 = z; s0348 = z; s0349 = z; + s0350 = z; s0351 = z; s0352 = z; s0353 = z; s0354 = z; s0355 = z; s0356 = z; + s0357 = z; s0358 = z; s0359 = z; s0360 = z; s0361 = z; s0362 = z; s0363 = z; + s0364 = z; s0365 = z; s0366 = z; s0367 = z; s0368 = z; s0369 = z; s0370 = z; + s0371 = z; s0372 = z; s0373 = z; s0374 = z; s0375 = z; s0376 = z; s0377 = z; + s0378 = z; s0379 = z; s0380 = z; s0381 = z; s0382 = z; s0383 = z; s0384 = z; + s0385 = z; s0386 = z; s0387 = z; s0388 = z; s0389 = z; s0390 = z; s0391 = z; + s0392 = z; s0393 = z; s0394 = z; s0395 = z; s0396 = z; s0397 = z; s0398 = z; + s0399 = z; s0400 = z; s0401 = z; s0402 = z; s0403 = z; s0404 = z; s0405 = z; + s0406 = z; s0407 = z; s0408 = z; s0409 = z; s0410 = z; s0411 = z; s0412 = z; + s0413 = z; s0414 = z; s0415 = z; s0416 = z; s0417 = z; s0418 = z; s0419 = z; + s0420 = z; s0421 = z; s0422 = z; s0423 = z; s0424 = z; s0425 = z; s0426 = z; + s0427 = z; s0428 = z; s0429 = z; s0430 = z; s0431 = z; s0432 = z; s0433 = z; + s0434 = z; s0435 = z; s0436 = z; s0437 = z; s0438 = z; s0439 = z; s0440 = z; + s0441 = z; s0442 = z; s0443 = z; s0444 = z; s0445 = z; s0446 = z; s0447 = z; + s0448 = z; s0449 = z; s0450 = z; s0451 = z; s0452 = z; s0453 = z; s0454 = z; + s0455 = z; s0456 = z; s0457 = z; s0458 = z; s0459 = z; s0460 = z; s0461 = z; + s0462 = z; s0463 = z; s0464 = z; s0465 = z; s0466 = z; s0467 = z; s0468 = z; + s0469 = z; s0470 = z; s0471 = z; s0472 = z; s0473 = z; s0474 = z; s0475 = z; + s0476 = z; s0477 = z; s0478 = z; s0479 = z; s0480 = z; s0481 = z; s0482 = z; + s0483 = z; s0484 = z; s0485 = z; s0486 = z; s0487 = z; s0488 = z; s0489 = z; + s0490 = z; s0491 = z; s0492 = z; s0493 = z; s0494 = z; s0495 = z; s0496 = z; + s0497 = z; s0498 = z; s0499 = z; s0500 = z; s0501 = z; s0502 = z; s0503 = z; + s0504 = z; s0505 = z; s0506 = z; s0507 = z; s0508 = z; s0509 = z; s0510 = z; + s0511 = z; s0512 = z; s0513 = z; s0514 = z; s0515 = z; s0516 = z; s0517 = z; + s0518 = z; s0519 = z; s0520 = z; s0521 = z; s0522 = z; s0523 = z; s0524 = z; + s0525 = z; s0526 = z; s0527 = z; s0528 = z; s0529 = z; s0530 = z; s0531 = z; + s0532 = z; s0533 = z; s0534 = z; s0535 = z; s0536 = z; s0537 = z; s0538 = z; + s0539 = z; s0540 = z; s0541 = z; s0542 = z; s0543 = z; s0544 = z; s0545 = z; + s0546 = z; s0547 = z; s0548 = z; s0549 = z; s0550 = z; s0551 = z; s0552 = z; + s0553 = z; s0554 = z; s0555 = z; s0556 = z; s0557 = z; s0558 = z; s0559 = z; + s0560 = z; s0561 = z; s0562 = z; s0563 = z; s0564 = z; s0565 = z; s0566 = z; + s0567 = z; s0568 = z; s0569 = z; s0570 = z; s0571 = z; s0572 = z; s0573 = z; + s0574 = z; s0575 = z; s0576 = z; s0577 = z; s0578 = z; s0579 = z; s0580 = z; + s0581 = z; s0582 = z; s0583 = z; s0584 = z; s0585 = z; s0586 = z; s0587 = z; + s0588 = z; s0589 = z; s0590 = z; s0591 = z; s0592 = z; s0593 = z; s0594 = z; + s0595 = z; s0596 = z; s0597 = z; s0598 = z; s0599 = z; s0600 = z; s0601 = z; + s0602 = z; s0603 = z; s0604 = z; s0605 = z; s0606 = z; s0607 = z; s0608 = z; + s0609 = z; s0610 = z; s0611 = z; s0612 = z; s0613 = z; s0614 = z; s0615 = z; + s0616 = z; s0617 = z; s0618 = z; s0619 = z; s0620 = z; s0621 = z; s0622 = z; + s0623 = z; s0624 = z; s0625 = z; s0626 = z; s0627 = z; s0628 = z; s0629 = z; + s0630 = z; s0631 = z; s0632 = z; s0633 = z; s0634 = z; s0635 = z; s0636 = z; + s0637 = z; s0638 = z; s0639 = z; s0640 = z; s0641 = z; s0642 = z; s0643 = z; + s0644 = z; s0645 = z; s0646 = z; s0647 = z; s0648 = z; s0649 = z; s0650 = z; + s0651 = z; s0652 = z; s0653 = z; s0654 = z; s0655 = z; s0656 = z; s0657 = z; + s0658 = z; s0659 = z; s0660 = z; s0661 = z; s0662 = z; s0663 = z; s0664 = z; + s0665 = z; s0666 = z; s0667 = z; s0668 = z; s0669 = z; s0670 = z; s0671 = z; + s0672 = z; s0673 = z; s0674 = z; s0675 = z; s0676 = z; s0677 = z; s0678 = z; + s0679 = z; s0680 = z; s0681 = z; s0682 = z; s0683 = z; s0684 = z; s0685 = z; + s0686 = z; s0687 = z; s0688 = z; s0689 = z; s0690 = z; s0691 = z; s0692 = z; + s0693 = z; s0694 = z; s0695 = z; s0696 = z; s0697 = z; s0698 = z; s0699 = z; + s0700 = z; s0701 = z; s0702 = z; s0703 = z; s0704 = z; s0705 = z; s0706 = z; + s0707 = z; s0708 = z; s0709 = z; s0710 = z; s0711 = z; s0712 = z; s0713 = z; + s0714 = z; s0715 = z; s0716 = z; s0717 = z; s0718 = z; s0719 = z; s0720 = z; + s0721 = z; s0722 = z; s0723 = z; s0724 = z; s0725 = z; s0726 = z; s0727 = z; + s0728 = z; s0729 = z; s0730 = z; s0731 = z; s0732 = z; s0733 = z; s0734 = z; + s0735 = z; s0736 = z; s0737 = z; s0738 = z; s0739 = z; s0740 = z; s0741 = z; + s0742 = z; s0743 = z; s0744 = z; s0745 = z; s0746 = z; s0747 = z; s0748 = z; + s0749 = z; s0750 = z; s0751 = z; s0752 = z; s0753 = z; s0754 = z; s0755 = z; + s0756 = z; s0757 = z; s0758 = z; s0759 = z; s0760 = z; s0761 = z; s0762 = z; + s0763 = z; s0764 = z; s0765 = z; s0766 = z; s0767 = z; s0768 = z; s0769 = z; + s0770 = z; s0771 = z; s0772 = z; s0773 = z; s0774 = z; s0775 = z; s0776 = z; + s0777 = z; s0778 = z; s0779 = z; s0780 = z; s0781 = z; s0782 = z; s0783 = z; + s0784 = z; s0785 = z; s0786 = z; s0787 = z; s0788 = z; s0789 = z; s0790 = z; + s0791 = z; s0792 = z; s0793 = z; s0794 = z; s0795 = z; s0796 = z; s0797 = z; + s0798 = z; s0799 = z; s0800 = z; s0801 = z; s0802 = z; s0803 = z; s0804 = z; + s0805 = z; s0806 = z; s0807 = z; s0808 = z; s0809 = z; s0810 = z; s0811 = z; + s0812 = z; s0813 = z; s0814 = z; s0815 = z; s0816 = z; s0817 = z; s0818 = z; + s0819 = z; s0820 = z; s0821 = z; s0822 = z; s0823 = z; s0824 = z; s0825 = z; + s0826 = z; s0827 = z; s0828 = z; s0829 = z; s0830 = z; s0831 = z; s0832 = z; + s0833 = z; s0834 = z; s0835 = z; s0836 = z; s0837 = z; s0838 = z; s0839 = z; + s0840 = z; s0841 = z; s0842 = z; s0843 = z; s0844 = z; s0845 = z; s0846 = z; + s0847 = z; s0848 = z; s0849 = z; s0850 = z; s0851 = z; s0852 = z; s0853 = z; + s0854 = z; s0855 = z; s0856 = z; s0857 = z; s0858 = z; s0859 = z; s0860 = z; + s0861 = z; s0862 = z; s0863 = z; s0864 = z; s0865 = z; s0866 = z; s0867 = z; + s0868 = z; s0869 = z; s0870 = z; s0871 = z; s0872 = z; s0873 = z; s0874 = z; + s0875 = z; s0876 = z; s0877 = z; s0878 = z; s0879 = z; s0880 = z; s0881 = z; + s0882 = z; s0883 = z; s0884 = z; s0885 = z; s0886 = z; s0887 = z; s0888 = z; + s0889 = z; s0890 = z; s0891 = z; s0892 = z; s0893 = z; s0894 = z; s0895 = z; + s0896 = z; s0897 = z; s0898 = z; s0899 = z; s0900 = z; s0901 = z; s0902 = z; + s0903 = z; s0904 = z; s0905 = z; s0906 = z; s0907 = z; s0908 = z; s0909 = z; + s0910 = z; s0911 = z; s0912 = z; s0913 = z; s0914 = z; s0915 = z; s0916 = z; + s0917 = z; s0918 = z; s0919 = z; s0920 = z; s0921 = z; s0922 = z; s0923 = z; + s0924 = z; s0925 = z; s0926 = z; s0927 = z; s0928 = z; s0929 = z; s0930 = z; + s0931 = z; s0932 = z; s0933 = z; s0934 = z; s0935 = z; s0936 = z; s0937 = z; + s0938 = z; s0939 = z; s0940 = z; s0941 = z; s0942 = z; s0943 = z; s0944 = z; + s0945 = z; s0946 = z; s0947 = z; s0948 = z; s0949 = z; s0950 = z; s0951 = z; + s0952 = z; s0953 = z; s0954 = z; s0955 = z; s0956 = z; s0957 = z; s0958 = z; + s0959 = z; s0960 = z; s0961 = z; s0962 = z; s0963 = z; s0964 = z; s0965 = z; + s0966 = z; s0967 = z; s0968 = z; s0969 = z; s0970 = z; s0971 = z; s0972 = z; + s0973 = z; s0974 = z; s0975 = z; s0976 = z; s0977 = z; s0978 = z; s0979 = z; + s0980 = z; s0981 = z; s0982 = z; s0983 = z; s0984 = z; s0985 = z; s0986 = z; + s0987 = z; s0988 = z; s0989 = z; s0990 = z; s0991 = z; s0992 = z; s0993 = z; + s0994 = z; s0995 = z; s0996 = z; s0997 = z; s0998 = z; s0999 = z; s1000 = z; + s1001 = z; s1002 = z; s1003 = z; s1004 = z; s1005 = z; s1006 = z; s1007 = z; + s1008 = z; s1009 = z; s1010 = z; s1011 = z; s1012 = z; s1013 = z; s1014 = z; + s1015 = z; s1016 = z; s1017 = z; s1018 = z; s1019 = z; s1020 = z; s1021 = z; + s1022 = z; s1023 = z; s1024 = z; + + reg u32 r; + z = s0000; r += z; z = s0001; r += z; z = s0002; r += z; z = s0003; r += z; + z = s0004; r += z; z = s0005; r += z; z = s0006; r += z; z = s0007; r += z; + z = s0008; r += z; z = s0009; r += z; z = s0010; r += z; z = s0011; r += z; + z = s0012; r += z; z = s0013; r += z; z = s0014; r += z; z = s0015; r += z; + z = s0016; r += z; z = s0017; r += z; z = s0018; r += z; z = s0019; r += z; + z = s0020; r += z; z = s0021; r += z; z = s0022; r += z; z = s0023; r += z; + z = s0024; r += z; z = s0025; r += z; z = s0026; r += z; z = s0027; r += z; + z = s0028; r += z; z = s0029; r += z; z = s0030; r += z; z = s0031; r += z; + z = s0032; r += z; z = s0033; r += z; z = s0034; r += z; z = s0035; r += z; + z = s0036; r += z; z = s0037; r += z; z = s0038; r += z; z = s0039; r += z; + z = s0040; r += z; z = s0041; r += z; z = s0042; r += z; z = s0043; r += z; + z = s0044; r += z; z = s0045; r += z; z = s0046; r += z; z = s0047; r += z; + z = s0048; r += z; z = s0049; r += z; z = s0050; r += z; z = s0051; r += z; + z = s0052; r += z; z = s0053; r += z; z = s0054; r += z; z = s0055; r += z; + z = s0056; r += z; z = s0057; r += z; z = s0058; r += z; z = s0059; r += z; + z = s0060; r += z; z = s0061; r += z; z = s0062; r += z; z = s0063; r += z; + z = s0064; r += z; z = s0065; r += z; z = s0066; r += z; z = s0067; r += z; + z = s0068; r += z; z = s0069; r += z; z = s0070; r += z; z = s0071; r += z; + z = s0072; r += z; z = s0073; r += z; z = s0074; r += z; z = s0075; r += z; + z = s0076; r += z; z = s0077; r += z; z = s0078; r += z; z = s0079; r += z; + z = s0080; r += z; z = s0081; r += z; z = s0082; r += z; z = s0083; r += z; + z = s0084; r += z; z = s0085; r += z; z = s0086; r += z; z = s0087; r += z; + z = s0088; r += z; z = s0089; r += z; z = s0090; r += z; z = s0091; r += z; + z = s0092; r += z; z = s0093; r += z; z = s0094; r += z; z = s0095; r += z; + z = s0096; r += z; z = s0097; r += z; z = s0098; r += z; z = s0099; r += z; + z = s0100; r += z; z = s0101; r += z; z = s0102; r += z; z = s0103; r += z; + z = s0104; r += z; z = s0105; r += z; z = s0106; r += z; z = s0107; r += z; + z = s0108; r += z; z = s0109; r += z; z = s0110; r += z; z = s0111; r += z; + z = s0112; r += z; z = s0113; r += z; z = s0114; r += z; z = s0115; r += z; + z = s0116; r += z; z = s0117; r += z; z = s0118; r += z; z = s0119; r += z; + z = s0120; r += z; z = s0121; r += z; z = s0122; r += z; z = s0123; r += z; + z = s0124; r += z; z = s0125; r += z; z = s0126; r += z; z = s0127; r += z; + z = s0128; r += z; z = s0129; r += z; z = s0130; r += z; z = s0131; r += z; + z = s0132; r += z; z = s0133; r += z; z = s0134; r += z; z = s0135; r += z; + z = s0136; r += z; z = s0137; r += z; z = s0138; r += z; z = s0139; r += z; + z = s0140; r += z; z = s0141; r += z; z = s0142; r += z; z = s0143; r += z; + z = s0144; r += z; z = s0145; r += z; z = s0146; r += z; z = s0147; r += z; + z = s0148; r += z; z = s0149; r += z; z = s0150; r += z; z = s0151; r += z; + z = s0152; r += z; z = s0153; r += z; z = s0154; r += z; z = s0155; r += z; + z = s0156; r += z; z = s0157; r += z; z = s0158; r += z; z = s0159; r += z; + z = s0160; r += z; z = s0161; r += z; z = s0162; r += z; z = s0163; r += z; + z = s0164; r += z; z = s0165; r += z; z = s0166; r += z; z = s0167; r += z; + z = s0168; r += z; z = s0169; r += z; z = s0170; r += z; z = s0171; r += z; + z = s0172; r += z; z = s0173; r += z; z = s0174; r += z; z = s0175; r += z; + z = s0176; r += z; z = s0177; r += z; z = s0178; r += z; z = s0179; r += z; + z = s0180; r += z; z = s0181; r += z; z = s0182; r += z; z = s0183; r += z; + z = s0184; r += z; z = s0185; r += z; z = s0186; r += z; z = s0187; r += z; + z = s0188; r += z; z = s0189; r += z; z = s0190; r += z; z = s0191; r += z; + z = s0192; r += z; z = s0193; r += z; z = s0194; r += z; z = s0195; r += z; + z = s0196; r += z; z = s0197; r += z; z = s0198; r += z; z = s0199; r += z; + z = s0200; r += z; z = s0201; r += z; z = s0202; r += z; z = s0203; r += z; + z = s0204; r += z; z = s0205; r += z; z = s0206; r += z; z = s0207; r += z; + z = s0208; r += z; z = s0209; r += z; z = s0210; r += z; z = s0211; r += z; + z = s0212; r += z; z = s0213; r += z; z = s0214; r += z; z = s0215; r += z; + z = s0216; r += z; z = s0217; r += z; z = s0218; r += z; z = s0219; r += z; + z = s0220; r += z; z = s0221; r += z; z = s0222; r += z; z = s0223; r += z; + z = s0224; r += z; z = s0225; r += z; z = s0226; r += z; z = s0227; r += z; + z = s0228; r += z; z = s0229; r += z; z = s0230; r += z; z = s0231; r += z; + z = s0232; r += z; z = s0233; r += z; z = s0234; r += z; z = s0235; r += z; + z = s0236; r += z; z = s0237; r += z; z = s0238; r += z; z = s0239; r += z; + z = s0240; r += z; z = s0241; r += z; z = s0242; r += z; z = s0243; r += z; + z = s0244; r += z; z = s0245; r += z; z = s0246; r += z; z = s0247; r += z; + z = s0248; r += z; z = s0249; r += z; z = s0250; r += z; z = s0251; r += z; + z = s0252; r += z; z = s0253; r += z; z = s0254; r += z; z = s0255; r += z; + z = s0256; r += z; z = s0257; r += z; z = s0258; r += z; z = s0259; r += z; + z = s0260; r += z; z = s0261; r += z; z = s0262; r += z; z = s0263; r += z; + z = s0264; r += z; z = s0265; r += z; z = s0266; r += z; z = s0267; r += z; + z = s0268; r += z; z = s0269; r += z; z = s0270; r += z; z = s0271; r += z; + z = s0272; r += z; z = s0273; r += z; z = s0274; r += z; z = s0275; r += z; + z = s0276; r += z; z = s0277; r += z; z = s0278; r += z; z = s0279; r += z; + z = s0280; r += z; z = s0281; r += z; z = s0282; r += z; z = s0283; r += z; + z = s0284; r += z; z = s0285; r += z; z = s0286; r += z; z = s0287; r += z; + z = s0288; r += z; z = s0289; r += z; z = s0290; r += z; z = s0291; r += z; + z = s0292; r += z; z = s0293; r += z; z = s0294; r += z; z = s0295; r += z; + z = s0296; r += z; z = s0297; r += z; z = s0298; r += z; z = s0299; r += z; + z = s0300; r += z; z = s0301; r += z; z = s0302; r += z; z = s0303; r += z; + z = s0304; r += z; z = s0305; r += z; z = s0306; r += z; z = s0307; r += z; + z = s0308; r += z; z = s0309; r += z; z = s0310; r += z; z = s0311; r += z; + z = s0312; r += z; z = s0313; r += z; z = s0314; r += z; z = s0315; r += z; + z = s0316; r += z; z = s0317; r += z; z = s0318; r += z; z = s0319; r += z; + z = s0320; r += z; z = s0321; r += z; z = s0322; r += z; z = s0323; r += z; + z = s0324; r += z; z = s0325; r += z; z = s0326; r += z; z = s0327; r += z; + z = s0328; r += z; z = s0329; r += z; z = s0330; r += z; z = s0331; r += z; + z = s0332; r += z; z = s0333; r += z; z = s0334; r += z; z = s0335; r += z; + z = s0336; r += z; z = s0337; r += z; z = s0338; r += z; z = s0339; r += z; + z = s0340; r += z; z = s0341; r += z; z = s0342; r += z; z = s0343; r += z; + z = s0344; r += z; z = s0345; r += z; z = s0346; r += z; z = s0347; r += z; + z = s0348; r += z; z = s0349; r += z; z = s0350; r += z; z = s0351; r += z; + z = s0352; r += z; z = s0353; r += z; z = s0354; r += z; z = s0355; r += z; + z = s0356; r += z; z = s0357; r += z; z = s0358; r += z; z = s0359; r += z; + z = s0360; r += z; z = s0361; r += z; z = s0362; r += z; z = s0363; r += z; + z = s0364; r += z; z = s0365; r += z; z = s0366; r += z; z = s0367; r += z; + z = s0368; r += z; z = s0369; r += z; z = s0370; r += z; z = s0371; r += z; + z = s0372; r += z; z = s0373; r += z; z = s0374; r += z; z = s0375; r += z; + z = s0376; r += z; z = s0377; r += z; z = s0378; r += z; z = s0379; r += z; + z = s0380; r += z; z = s0381; r += z; z = s0382; r += z; z = s0383; r += z; + z = s0384; r += z; z = s0385; r += z; z = s0386; r += z; z = s0387; r += z; + z = s0388; r += z; z = s0389; r += z; z = s0390; r += z; z = s0391; r += z; + z = s0392; r += z; z = s0393; r += z; z = s0394; r += z; z = s0395; r += z; + z = s0396; r += z; z = s0397; r += z; z = s0398; r += z; z = s0399; r += z; + z = s0400; r += z; z = s0401; r += z; z = s0402; r += z; z = s0403; r += z; + z = s0404; r += z; z = s0405; r += z; z = s0406; r += z; z = s0407; r += z; + z = s0408; r += z; z = s0409; r += z; z = s0410; r += z; z = s0411; r += z; + z = s0412; r += z; z = s0413; r += z; z = s0414; r += z; z = s0415; r += z; + z = s0416; r += z; z = s0417; r += z; z = s0418; r += z; z = s0419; r += z; + z = s0420; r += z; z = s0421; r += z; z = s0422; r += z; z = s0423; r += z; + z = s0424; r += z; z = s0425; r += z; z = s0426; r += z; z = s0427; r += z; + z = s0428; r += z; z = s0429; r += z; z = s0430; r += z; z = s0431; r += z; + z = s0432; r += z; z = s0433; r += z; z = s0434; r += z; z = s0435; r += z; + z = s0436; r += z; z = s0437; r += z; z = s0438; r += z; z = s0439; r += z; + z = s0440; r += z; z = s0441; r += z; z = s0442; r += z; z = s0443; r += z; + z = s0444; r += z; z = s0445; r += z; z = s0446; r += z; z = s0447; r += z; + z = s0448; r += z; z = s0449; r += z; z = s0450; r += z; z = s0451; r += z; + z = s0452; r += z; z = s0453; r += z; z = s0454; r += z; z = s0455; r += z; + z = s0456; r += z; z = s0457; r += z; z = s0458; r += z; z = s0459; r += z; + z = s0460; r += z; z = s0461; r += z; z = s0462; r += z; z = s0463; r += z; + z = s0464; r += z; z = s0465; r += z; z = s0466; r += z; z = s0467; r += z; + z = s0468; r += z; z = s0469; r += z; z = s0470; r += z; z = s0471; r += z; + z = s0472; r += z; z = s0473; r += z; z = s0474; r += z; z = s0475; r += z; + z = s0476; r += z; z = s0477; r += z; z = s0478; r += z; z = s0479; r += z; + z = s0480; r += z; z = s0481; r += z; z = s0482; r += z; z = s0483; r += z; + z = s0484; r += z; z = s0485; r += z; z = s0486; r += z; z = s0487; r += z; + z = s0488; r += z; z = s0489; r += z; z = s0490; r += z; z = s0491; r += z; + z = s0492; r += z; z = s0493; r += z; z = s0494; r += z; z = s0495; r += z; + z = s0496; r += z; z = s0497; r += z; z = s0498; r += z; z = s0499; r += z; + z = s0500; r += z; z = s0501; r += z; z = s0502; r += z; z = s0503; r += z; + z = s0504; r += z; z = s0505; r += z; z = s0506; r += z; z = s0507; r += z; + z = s0508; r += z; z = s0509; r += z; z = s0510; r += z; z = s0511; r += z; + z = s0512; r += z; z = s0513; r += z; z = s0514; r += z; z = s0515; r += z; + z = s0516; r += z; z = s0517; r += z; z = s0518; r += z; z = s0519; r += z; + z = s0520; r += z; z = s0521; r += z; z = s0522; r += z; z = s0523; r += z; + z = s0524; r += z; z = s0525; r += z; z = s0526; r += z; z = s0527; r += z; + z = s0528; r += z; z = s0529; r += z; z = s0530; r += z; z = s0531; r += z; + z = s0532; r += z; z = s0533; r += z; z = s0534; r += z; z = s0535; r += z; + z = s0536; r += z; z = s0537; r += z; z = s0538; r += z; z = s0539; r += z; + z = s0540; r += z; z = s0541; r += z; z = s0542; r += z; z = s0543; r += z; + z = s0544; r += z; z = s0545; r += z; z = s0546; r += z; z = s0547; r += z; + z = s0548; r += z; z = s0549; r += z; z = s0550; r += z; z = s0551; r += z; + z = s0552; r += z; z = s0553; r += z; z = s0554; r += z; z = s0555; r += z; + z = s0556; r += z; z = s0557; r += z; z = s0558; r += z; z = s0559; r += z; + z = s0560; r += z; z = s0561; r += z; z = s0562; r += z; z = s0563; r += z; + z = s0564; r += z; z = s0565; r += z; z = s0566; r += z; z = s0567; r += z; + z = s0568; r += z; z = s0569; r += z; z = s0570; r += z; z = s0571; r += z; + z = s0572; r += z; z = s0573; r += z; z = s0574; r += z; z = s0575; r += z; + z = s0576; r += z; z = s0577; r += z; z = s0578; r += z; z = s0579; r += z; + z = s0580; r += z; z = s0581; r += z; z = s0582; r += z; z = s0583; r += z; + z = s0584; r += z; z = s0585; r += z; z = s0586; r += z; z = s0587; r += z; + z = s0588; r += z; z = s0589; r += z; z = s0590; r += z; z = s0591; r += z; + z = s0592; r += z; z = s0593; r += z; z = s0594; r += z; z = s0595; r += z; + z = s0596; r += z; z = s0597; r += z; z = s0598; r += z; z = s0599; r += z; + z = s0600; r += z; z = s0601; r += z; z = s0602; r += z; z = s0603; r += z; + z = s0604; r += z; z = s0605; r += z; z = s0606; r += z; z = s0607; r += z; + z = s0608; r += z; z = s0609; r += z; z = s0610; r += z; z = s0611; r += z; + z = s0612; r += z; z = s0613; r += z; z = s0614; r += z; z = s0615; r += z; + z = s0616; r += z; z = s0617; r += z; z = s0618; r += z; z = s0619; r += z; + z = s0620; r += z; z = s0621; r += z; z = s0622; r += z; z = s0623; r += z; + z = s0624; r += z; z = s0625; r += z; z = s0626; r += z; z = s0627; r += z; + z = s0628; r += z; z = s0629; r += z; z = s0630; r += z; z = s0631; r += z; + z = s0632; r += z; z = s0633; r += z; z = s0634; r += z; z = s0635; r += z; + z = s0636; r += z; z = s0637; r += z; z = s0638; r += z; z = s0639; r += z; + z = s0640; r += z; z = s0641; r += z; z = s0642; r += z; z = s0643; r += z; + z = s0644; r += z; z = s0645; r += z; z = s0646; r += z; z = s0647; r += z; + z = s0648; r += z; z = s0649; r += z; z = s0650; r += z; z = s0651; r += z; + z = s0652; r += z; z = s0653; r += z; z = s0654; r += z; z = s0655; r += z; + z = s0656; r += z; z = s0657; r += z; z = s0658; r += z; z = s0659; r += z; + z = s0660; r += z; z = s0661; r += z; z = s0662; r += z; z = s0663; r += z; + z = s0664; r += z; z = s0665; r += z; z = s0666; r += z; z = s0667; r += z; + z = s0668; r += z; z = s0669; r += z; z = s0670; r += z; z = s0671; r += z; + z = s0672; r += z; z = s0673; r += z; z = s0674; r += z; z = s0675; r += z; + z = s0676; r += z; z = s0677; r += z; z = s0678; r += z; z = s0679; r += z; + z = s0680; r += z; z = s0681; r += z; z = s0682; r += z; z = s0683; r += z; + z = s0684; r += z; z = s0685; r += z; z = s0686; r += z; z = s0687; r += z; + z = s0688; r += z; z = s0689; r += z; z = s0690; r += z; z = s0691; r += z; + z = s0692; r += z; z = s0693; r += z; z = s0694; r += z; z = s0695; r += z; + z = s0696; r += z; z = s0697; r += z; z = s0698; r += z; z = s0699; r += z; + z = s0700; r += z; z = s0701; r += z; z = s0702; r += z; z = s0703; r += z; + z = s0704; r += z; z = s0705; r += z; z = s0706; r += z; z = s0707; r += z; + z = s0708; r += z; z = s0709; r += z; z = s0710; r += z; z = s0711; r += z; + z = s0712; r += z; z = s0713; r += z; z = s0714; r += z; z = s0715; r += z; + z = s0716; r += z; z = s0717; r += z; z = s0718; r += z; z = s0719; r += z; + z = s0720; r += z; z = s0721; r += z; z = s0722; r += z; z = s0723; r += z; + z = s0724; r += z; z = s0725; r += z; z = s0726; r += z; z = s0727; r += z; + z = s0728; r += z; z = s0729; r += z; z = s0730; r += z; z = s0731; r += z; + z = s0732; r += z; z = s0733; r += z; z = s0734; r += z; z = s0735; r += z; + z = s0736; r += z; z = s0737; r += z; z = s0738; r += z; z = s0739; r += z; + z = s0740; r += z; z = s0741; r += z; z = s0742; r += z; z = s0743; r += z; + z = s0744; r += z; z = s0745; r += z; z = s0746; r += z; z = s0747; r += z; + z = s0748; r += z; z = s0749; r += z; z = s0750; r += z; z = s0751; r += z; + z = s0752; r += z; z = s0753; r += z; z = s0754; r += z; z = s0755; r += z; + z = s0756; r += z; z = s0757; r += z; z = s0758; r += z; z = s0759; r += z; + z = s0760; r += z; z = s0761; r += z; z = s0762; r += z; z = s0763; r += z; + z = s0764; r += z; z = s0765; r += z; z = s0766; r += z; z = s0767; r += z; + z = s0768; r += z; z = s0769; r += z; z = s0770; r += z; z = s0771; r += z; + z = s0772; r += z; z = s0773; r += z; z = s0774; r += z; z = s0775; r += z; + z = s0776; r += z; z = s0777; r += z; z = s0778; r += z; z = s0779; r += z; + z = s0780; r += z; z = s0781; r += z; z = s0782; r += z; z = s0783; r += z; + z = s0784; r += z; z = s0785; r += z; z = s0786; r += z; z = s0787; r += z; + z = s0788; r += z; z = s0789; r += z; z = s0790; r += z; z = s0791; r += z; + z = s0792; r += z; z = s0793; r += z; z = s0794; r += z; z = s0795; r += z; + z = s0796; r += z; z = s0797; r += z; z = s0798; r += z; z = s0799; r += z; + z = s0800; r += z; z = s0801; r += z; z = s0802; r += z; z = s0803; r += z; + z = s0804; r += z; z = s0805; r += z; z = s0806; r += z; z = s0807; r += z; + z = s0808; r += z; z = s0809; r += z; z = s0810; r += z; z = s0811; r += z; + z = s0812; r += z; z = s0813; r += z; z = s0814; r += z; z = s0815; r += z; + z = s0816; r += z; z = s0817; r += z; z = s0818; r += z; z = s0819; r += z; + z = s0820; r += z; z = s0821; r += z; z = s0822; r += z; z = s0823; r += z; + z = s0824; r += z; z = s0825; r += z; z = s0826; r += z; z = s0827; r += z; + z = s0828; r += z; z = s0829; r += z; z = s0830; r += z; z = s0831; r += z; + z = s0832; r += z; z = s0833; r += z; z = s0834; r += z; z = s0835; r += z; + z = s0836; r += z; z = s0837; r += z; z = s0838; r += z; z = s0839; r += z; + z = s0840; r += z; z = s0841; r += z; z = s0842; r += z; z = s0843; r += z; + z = s0844; r += z; z = s0845; r += z; z = s0846; r += z; z = s0847; r += z; + z = s0848; r += z; z = s0849; r += z; z = s0850; r += z; z = s0851; r += z; + z = s0852; r += z; z = s0853; r += z; z = s0854; r += z; z = s0855; r += z; + z = s0856; r += z; z = s0857; r += z; z = s0858; r += z; z = s0859; r += z; + z = s0860; r += z; z = s0861; r += z; z = s0862; r += z; z = s0863; r += z; + z = s0864; r += z; z = s0865; r += z; z = s0866; r += z; z = s0867; r += z; + z = s0868; r += z; z = s0869; r += z; z = s0870; r += z; z = s0871; r += z; + z = s0872; r += z; z = s0873; r += z; z = s0874; r += z; z = s0875; r += z; + z = s0876; r += z; z = s0877; r += z; z = s0878; r += z; z = s0879; r += z; + z = s0880; r += z; z = s0881; r += z; z = s0882; r += z; z = s0883; r += z; + z = s0884; r += z; z = s0885; r += z; z = s0886; r += z; z = s0887; r += z; + z = s0888; r += z; z = s0889; r += z; z = s0890; r += z; z = s0891; r += z; + z = s0892; r += z; z = s0893; r += z; z = s0894; r += z; z = s0895; r += z; + z = s0896; r += z; z = s0897; r += z; z = s0898; r += z; z = s0899; r += z; + z = s0900; r += z; z = s0901; r += z; z = s0902; r += z; z = s0903; r += z; + z = s0904; r += z; z = s0905; r += z; z = s0906; r += z; z = s0907; r += z; + z = s0908; r += z; z = s0909; r += z; z = s0910; r += z; z = s0911; r += z; + z = s0912; r += z; z = s0913; r += z; z = s0914; r += z; z = s0915; r += z; + z = s0916; r += z; z = s0917; r += z; z = s0918; r += z; z = s0919; r += z; + z = s0920; r += z; z = s0921; r += z; z = s0922; r += z; z = s0923; r += z; + z = s0924; r += z; z = s0925; r += z; z = s0926; r += z; z = s0927; r += z; + z = s0928; r += z; z = s0929; r += z; z = s0930; r += z; z = s0931; r += z; + z = s0932; r += z; z = s0933; r += z; z = s0934; r += z; z = s0935; r += z; + z = s0936; r += z; z = s0937; r += z; z = s0938; r += z; z = s0939; r += z; + z = s0940; r += z; z = s0941; r += z; z = s0942; r += z; z = s0943; r += z; + z = s0944; r += z; z = s0945; r += z; z = s0946; r += z; z = s0947; r += z; + z = s0948; r += z; z = s0949; r += z; z = s0950; r += z; z = s0951; r += z; + z = s0952; r += z; z = s0953; r += z; z = s0954; r += z; z = s0955; r += z; + z = s0956; r += z; z = s0957; r += z; z = s0958; r += z; z = s0959; r += z; + z = s0960; r += z; z = s0961; r += z; z = s0962; r += z; z = s0963; r += z; + z = s0964; r += z; z = s0965; r += z; z = s0966; r += z; z = s0967; r += z; + z = s0968; r += z; z = s0969; r += z; z = s0970; r += z; z = s0971; r += z; + z = s0972; r += z; z = s0973; r += z; z = s0974; r += z; z = s0975; r += z; + z = s0976; r += z; z = s0977; r += z; z = s0978; r += z; z = s0979; r += z; + z = s0980; r += z; z = s0981; r += z; z = s0982; r += z; z = s0983; r += z; + z = s0984; r += z; z = s0985; r += z; z = s0986; r += z; z = s0987; r += z; + z = s0988; r += z; z = s0989; r += z; z = s0990; r += z; z = s0991; r += z; + z = s0992; r += z; z = s0993; r += z; z = s0994; r += z; z = s0995; r += z; + z = s0996; r += z; z = s0997; r += z; z = s0998; r += z; z = s0999; r += z; + z = s1000; r += z; z = s1001; r += z; z = s1002; r += z; z = s1003; r += z; + z = s1004; r += z; z = s1005; r += z; z = s1006; r += z; z = s1007; r += z; + z = s1008; r += z; z = s1009; r += z; z = s1010; r += z; z = s1011; r += z; + z = s1012; r += z; z = s1013; r += z; z = s1014; r += z; z = s1015; r += z; + z = s1016; r += z; z = s1017; r += z; z = s1018; r += z; z = s1019; r += z; + z = s1020; r += z; z = s1021; r += z; z = s1022; r += z; z = s1023; r += z; + z = s1024; r += z; + + r += z if r == 0; + + return r; +} diff --git a/proofs/arch/arm_expand_imm.v b/proofs/arch/arm_expand_imm.v index ddd1129ae..6a5cc522b 100644 --- a/proofs/arch/arm_expand_imm.v +++ b/proofs/arch/arm_expand_imm.v @@ -85,8 +85,14 @@ Qed. HB.instance Definition _ := hasDecEq.Build expected_wencoding expected_wencoding_eq_axiom. -Definition is_w12_encoding (z : Z) : bool := (z "W12"%string | W16_encoding => "W16"%string end. - diff --git a/proofs/compiler/arm_extra.v b/proofs/compiler/arm_extra.v index c8232c100..7ab1736ce 100644 --- a/proofs/compiler/arm_extra.v +++ b/proofs/compiler/arm_extra.v @@ -26,6 +26,12 @@ Variant arm_extra_op : Type := | Oarm_add_large_imm | Osmart_li of wsize (* Load an immediate to a register. *) | Osmart_li_cc of wsize (* Conditional [Osmart_li]. *) + | Olarge_load of wsize & Z (* Same as LDR with an immediate offset, but the + offset is loaded to a register with + [Osmart_li]. *) + | Olarge_store of wsize & Z + | Olarge_load_cc of wsize & Z + | Olarge_store_cc of wsize & Z . Scheme Equality for arm_extra_op. @@ -46,7 +52,11 @@ Instance eqTC_arm_extra_op : eqTypeC arm_extra_op := (* Extra instructions descriptions. *) -Local Notation E n := (sopn.ADExplicit n None). +#[local] +Notation E := (fun n => sopn.ADExplicit n None). + +#[local] +Notation Ea := (fun n => sopn.ADExplicit n None). (* [conflicts] ensures that the returned register is distinct from the first argument. *) @@ -85,12 +95,98 @@ Definition smart_li_instr_cc (ws : wsize) : instruction_desc := (fun x b y => if b then x else y) true. +Definition large_load_instr (ws : wsize) (off : Z) : instruction_desc := + let f x := (wrepr reg_size off, zero_extend reg_size x) in + let semi x := ok (f x) in + let tin := [:: sword ws ] in + {| + str := pp_sz "large_load" ws; + tin := tin; + i_in := [:: E 0 ]; + tout := [:: sreg; sreg ]; + i_out := [:: E 1; E 2 ]; + conflicts := [:: (APout 0, APin 0) ]; + semi := semi; + semu := @values.vuincl_app_sopn_v tin [:: sreg; sreg ] semi refl_equal; + i_safe := [::]; + i_valid := true; + i_safe_wf := refl_equal; + i_semi_errty := fun _ => sem_prod_ok_error (tin := tin) f _; + i_semi_safe := fun _ => values.sem_prod_ok_safe (tin := tin) f; + |}. + +Definition large_load_instr_cc (ws : wsize) (off : Z) : instruction_desc := + let woff := wrepr reg_size off in + let f x b old_x := (woff, if b then zero_extend reg_size x else old_x) in + let semi x b o := ok (f x b o) in + let tin := [:: sword ws; sbool; sreg ] in + {| + str := pp_sz "large_load_cc" ws; + tin := [:: sword ws; sbool; sreg ]; + i_in := [:: E 0; Ea 3; E 2 ]; + tout := [:: sreg; sreg ]; + i_out := [:: E 1; E 2 ]; + conflicts := [:: (APout 0, APin 0) ]; + semi := semi; + semu := @values.vuincl_app_sopn_v tin [:: sreg; sreg ] semi refl_equal; + i_safe := [::]; + i_valid := true; + i_safe_wf := refl_equal; + i_semi_errty := fun _ => sem_prod_ok_error (tin := tin) f _; + i_semi_safe := fun _ => values.sem_prod_ok_safe (tin := tin) f; + |}. + +Definition large_store_instr (ws : wsize) (off : Z) : instruction_desc := + let f x := (wrepr reg_size off, zero_extend ws x) in + let semi x := ok (f x) in + let tin := [:: sword ws ] in + {| + str := pp_sz "large_store" ws; + tin := [:: sword ws ]; + i_in := [:: E 0 ]; + tout := [:: sreg; sword ws ]; + i_out := [:: E 1; E 2 ]; + conflicts := [:: (APout 0, APin 0) ]; + semi := semi; + semu := @values.vuincl_app_sopn_v tin [:: sreg; sword ws ] semi refl_equal; + i_safe := [::]; + i_valid := true; + i_safe_wf := refl_equal; + i_semi_errty := fun _ => sem_prod_ok_error (tin := tin) f _; + i_semi_safe := fun _ => values.sem_prod_ok_safe (tin := tin) f; + |}. + +Definition large_store_instr_cc (ws : wsize) (off : Z) : instruction_desc := + let woff := wrepr reg_size off in + let f x b old_x := (woff, if b then zero_extend ws x else old_x) in + let semi x b o := ok (f x b o) in + let tin := [:: sword ws; sbool; sword ws ] in + {| + str := pp_sz "large_store_cc" ws; + tin := tin; + i_in := [:: E 0; Ea 3; E 2 ]; + tout := [:: sreg; sword ws ]; + i_out := [:: E 1; E 2 ]; + conflicts := [:: (APout 0, APin 0) ]; + semi := semi; + semu := @values.vuincl_app_sopn_v tin [:: sreg; sword ws ] semi refl_equal; + i_safe := [::]; + i_valid := true; + i_safe_wf := refl_equal; + i_semi_errty := fun _ => sem_prod_ok_error (tin := tin) f _; + i_semi_safe := fun _ => values.sem_prod_ok_safe (tin := tin) f; + |}. + Definition get_instr_desc (o: arm_extra_op) : instruction_desc := match o with | Oarm_swap sz => Oswap_instr (sword sz) | Oarm_add_large_imm => Oarm_add_large_imm_instr | Osmart_li ws => smart_li_instr ws | Osmart_li_cc ws => smart_li_instr_cc ws + | Olarge_load ws off => large_load_instr ws off + | Olarge_store ws off => large_store_instr ws off + | Olarge_load_cc ws off => large_load_instr_cc ws off + | Olarge_store_cc ws off => large_store_instr_cc ws off end. (* Without priority 1, this instance is selected when looking for an [asmOp], @@ -130,10 +226,23 @@ Definition error (ii : instr_info) (msg : string) := pel_internal := false; |}. -Definition li_condition_modified ii := - error - ii - "assignment needs to be split but condition is modified by assignment". +Definition condition_err := "assignment needs to be split but". + +Definition condition_modified ii := + error ii (append condition_err " condition is modified by it"). + +Definition invalid_previous ii := + let msg := + [:: "conditional"; condition_err; "previous value is invalid" ] + in + error ii (concat " " msg). + +Definition previous_modified ii := + let msg := + [:: "conditional"; condition_err; "previous value is modified by it" ] + in + error ii (concat " " msg). + End E. Definition asm_args_of_opn_args @@ -151,6 +260,14 @@ Definition uncons_LLvar then ok (x, les) else Error (E.internal_error ii "invalid lvals"). +Definition uncons_Store + (ii : instr_info) + (les : seq lexpr) : + cexec (aligned * wsize * var_i * fexpr * seq lexpr) := + if les is Store al ws xbase e :: les + then ok (al, ws, xbase, e, les) + else Error (E.internal_error ii "invalid lvals"). + Definition uncons_rvar (ii : instr_info) (res : seq rexpr) : cexec (var_i * seq rexpr) := if res is Rexpr (Fvar x) :: res @@ -163,6 +280,14 @@ Definition uncons_wconst then ok (imm, res') else Error (E.internal_error ii "invalid arguments"). +Definition uncons_Load + (ii : instr_info) + (res : seq rexpr) : + (cexec (aligned * wsize * var_i * fexpr * seq rexpr)) := + if res is Load al ws xbase eoff :: res' + then ok (al, ws, xbase, eoff, res') + else Error (E.internal_error ii "invalid arguments"). + Definition smart_li_args ii ws les res := (* FIXME: This check is because [ARMFopn_core.li] only works with register size, it should not be the case. *) @@ -183,19 +308,160 @@ Definition assemble_smart_li ii ws les res := Let: (x, imm, _) := smart_li_args ii ws les res in ok (asm_args_of_opn_args (ARMFopn_core.li x imm)). +Definition cond_opn_args + (cond : rexpr) + (old : seq rexpr) + (args : ARMFopn_core.opn_args) : + asm_op_msb_t * lexprs * rexprs := + let '(les, ARM_op mn opts, res) := args in + let opts := set_is_conditional opts in + ((None, ARM_op mn opts), les, res ++ cond :: old). + Definition assemble_smart_li_cc ii ws les res : cexec (seq (asm_op_msb_t * lexprs * rexprs)) := Let: (x, imm, res) := smart_li_args ii ws les res in Let: (cond, res) := uncons ii res in Let _ := - assert (~~ Sv.mem x (free_vars_r cond)) (E.li_condition_modified ii) + assert (~~ Sv.mem x (free_vars_r cond)) (E.condition_modified ii) in Let: (oldx, _) := uncons_rvar ii res in - let mk '(les, ARM_op mn opts, res) := - let opts := set_is_conditional opts in - ok ((None, ARM_op mn opts), les, res ++ [:: cond; rvar oldx ]) + ok (map (cond_opn_args cond [:: rvar oldx ]) (ARMFopn_core.li x imm)). + +Definition chk_assemble_large_load + (err : string -> pp_error_loc) + (ws : wsize) + (woff : word reg_size) + (ws' : wsize) + (xbase tmp : var_i) + (eoff : fexpr) : + cexec unit := + Let _ := assert (ws == ws') (err "word size differs") in + let msg := "offset differs" in + Let _ := assert (is_fwconst reg_size eoff == Some woff)%CMP (err msg) in + Let _ := assert (v_var xbase != v_var tmp) (err "base and tmp clash") in + assert (vtype tmp == sword reg_size) (err "tmp is not wreg"). + +Definition assemble_large_load + (ii : instr_info) + (ws : wsize) + (off : Z) + (les : seq lexpr) + (res : seq rexpr) : + cexec (seq (asm_op_msb_t * lexprs * rexprs)) := + Let mn := o2r (E.condition_modified ii) (uload_mn_of_wsize ws) in + Let: (tmp, les) := uncons_LLvar ii les in + Let: (x, _) := uncons_LLvar ii les in + Let: (al, ws', xbase, eoff, _) := uncons_Load ii res in + let err s := + E.internal_error ii (append "invalid large_load arguments: " s) + in + Let _ := + chk_assemble_large_load err ws (wrepr reg_size off) ws' xbase tmp eoff + in + let pre := asm_args_of_opn_args (ARMFopn_core.li tmp off) in + let re := Load al ws xbase (Fvar tmp) in + let i := ((None, ARM_op mn default_opts), [:: LLvar x ], [:: re ]) in + ok (rcons pre i). + +Definition assemble_large_load_cc + (ii : instr_info) + (ws : wsize) + (off : Z) + (les : seq lexpr) + (res : seq rexpr) : + cexec (seq (asm_op_msb_t * lexprs * rexprs)) := + let err := E.internal_error ii "invalid large_load size" in + Let mn := o2r err (uload_mn_of_wsize ws) in + Let: (tmp, les) := uncons_LLvar ii les in + Let: (x, _) := uncons_LLvar ii les in + Let: (al, ws', xbase, eoff, res) := uncons_Load ii res in + Let: (cond, res) := uncons ii res in + Let _ := + assert (~~ Sv.mem tmp (free_vars_r cond)) (E.condition_modified ii) + in + Let _ := + assert (~~ Sv.mem tmp (free_vars_rs res)) (E.previous_modified ii) + in + let err s := + E.internal_error ii (append "invalid large_load arguments: " s) + in + Let _ := + chk_assemble_large_load err ws (wrepr reg_size off) ws' xbase tmp eoff + in + let pre := asm_args_of_opn_args (ARMFopn_core.li tmp off) in + let opts := set_is_conditional default_opts in + let res := [:: Load al ws xbase (Fvar tmp); cond ] ++ res in + let i := ((None, ARM_op mn opts), [:: LLvar x ], res) in + ok (rcons pre i). + +Definition chk_assemble_large_store + (err : string -> pp_error_loc) + (ws : wsize) + (woff : word reg_size) + (ws' : wsize) + (x xbase tmp : var_i) + (eoff : fexpr) : + cexec unit := + Let _ := chk_assemble_large_load err ws woff ws' xbase tmp eoff in + assert (v_var x != v_var tmp) (err "source and tmp clash"). + +Definition assemble_large_store + (ii : instr_info) + (ws : wsize) + (off : Z) + (les : seq lexpr) + (res : seq rexpr) : + cexec (seq (asm_op_msb_t * lexprs * rexprs)) := + let err := E.internal_error ii "invalid store_load size" in + Let mn := o2r err (store_mn_of_wsize ws) in + Let: (tmp, les) := uncons_LLvar ii les in + Let: (al, ws', xbase, eoff, _) := uncons_Store ii les in + Let: (x, _) := uncons_rvar ii res in + let err s := + E.internal_error ii (append "invalid large_store arguments: " s) + in + Let _ := + chk_assemble_large_store err ws (wrepr reg_size off) ws' x xbase tmp eoff + in + let pre := asm_args_of_opn_args (ARMFopn_core.li tmp off) in + let le := Store al ws xbase (Fvar tmp) in + let i := ((None, ARM_op mn default_opts), [:: le ], res) in + ok (rcons pre i). + +Definition assemble_large_store_cc + (ii : instr_info) + (ws : wsize) + (off : Z) + (les : seq lexpr) + (res : seq rexpr) : + cexec (seq (asm_op_msb_t * lexprs * rexprs)) := + let err := E.internal_error ii "invalid store_load size" in + Let mn := o2r err (store_mn_of_wsize ws) in + Let: (tmp, les) := uncons_LLvar ii les in + Let: (al, ws', xbase, eoff, _) := uncons_Store ii les in + Let: (x, res) := uncons_rvar ii res in + Let: (cond, res) := uncons ii res in + Let: (al', ws'', xbase', eoff', _) := uncons_Load ii res in + Let _ := + assert (~~ Sv.mem tmp (free_vars_r cond)) (E.condition_modified ii) + in + Let _ := + assert + [&& v_var xbase == v_var xbase' & eq_fexpr eoff eoff' ] + (E.invalid_previous ii) + in + let err s := + E.internal_error ii (append "invalid large_store arguments: " s) + in + Let _ := + chk_assemble_large_store err ws (wrepr reg_size off) ws' x xbase tmp eoff in - mapM mk (ARMFopn_core.li x imm). + let pre := asm_args_of_opn_args (ARMFopn_core.li tmp off) in + let opts := set_is_conditional default_opts in + let le := Store al ws xbase (Fvar tmp) in + let re := Load al' ws'' xbase' (Fvar tmp) in + let i := ((None, ARM_op mn opts), [:: le ], [:: rvar x; cond; re ]) in + ok (rcons pre i). Definition assemble_extra (ii: instr_info) @@ -239,6 +505,10 @@ Definition assemble_extra end | Osmart_li ws => assemble_smart_li ii ws outx inx | Osmart_li_cc ws => assemble_smart_li_cc ii ws outx inx + | Olarge_load ws off => assemble_large_load ii ws off outx inx + | Olarge_store ws off => assemble_large_store ii ws off outx inx + | Olarge_load_cc ws off => assemble_large_load_cc ii ws off outx inx + | Olarge_store_cc ws off => assemble_large_store_cc ii ws off outx inx end. #[ export ] diff --git a/proofs/compiler/arm_params.v b/proofs/compiler/arm_params.v index 77b6b5ce2..7d903835d 100644 --- a/proofs/compiler/arm_params.v +++ b/proofs/compiler/arm_params.v @@ -75,11 +75,73 @@ Definition arm_immediate (x: var_i) z := Definition arm_swap t (x y z w : var_i) := Copn [:: Lvar x; Lvar y] t (Oasm (ExtOp (Oarm_swap reg_size))) [:: Plvar z; Plvar w]. +Definition smart_mem_mn + (mn_large : Z -> arm_extra_op) + (eoff : pexpr) : + option sopn := + let%opt woff := expr.is_wconst reg_size eoff in + let off := wsigned woff in + let%opt _ := oassert (~~ is_mem_immediate off) in + Some (Oasm (ExtOp (mn_large off))). + +Definition split_mem_opn_match_lvs lvs := + if lvs is Lmem al ws vbase eoff :: lvs' + then Some (al, ws, vbase, eoff, lvs') + else None. + +Definition split_mem_opn_match_es es := + if es is Pload al ws vbase eoff :: es' + then Some (al, ws, vbase, eoff, es') + else None. + +Definition get_eop_store + (op : sopn) (ws : wsize) : option (wsize -> Z -> arm_extra_op) := + if op is Oasm (BaseOp (None, ARM_op mn opts)) + then + let%opt _ := oassert (store_mn_of_wsize ws == Some mn) in + let%opt _ := oassert [&& ~~ set_flags opts & has_shift opts == None ] in + Some (if is_conditional opts then Olarge_store_cc else Olarge_store) + else None. + +Definition get_eop_load + (op : sopn) (ws : wsize) : option (wsize -> Z -> arm_extra_op) := + if op is Oasm (BaseOp (None, ARM_op mn opts)) + then + let%opt _ := oassert (uload_mn_of_wsize ws == Some mn) in + let%opt _ := oassert [&& ~~ set_flags opts & has_shift opts == None ] in + Some (if is_conditional opts then Olarge_load_cc else Olarge_load) + else None. + +Definition split_mem_opn + (lvs : seq lval) (op : sopn) (es : seq pexpr) : option copn_args := + let lnone := Lnone dummy_var_info (sword reg_size) in + if split_mem_opn_match_lvs lvs is Some (_, ws, _, eoff, _) + then + let%opt eop := get_eop_store op ws in + let%opt op := smart_mem_mn (eop ws) eoff in + Some (lnone :: lvs, op, es) + else + if split_mem_opn_match_es es is Some (_, ws, _, eoff, _) + then + let%opt eop := get_eop_load op ws in + let%opt op := smart_mem_mn (eop ws) eoff in + Some (lnone :: lvs, op, es) + else + None. + +Definition arm_mem_opn lvs tag op es := + let '(lvs, op, es, warn) := + if split_mem_opn lvs op es is Some (lvs', op', es') + then (lvs', op', es', true) + else (lvs, op, es, false) + in (Copn lvs tag op es, warn). + Definition arm_saparams : stack_alloc_params := {| sap_mov_ofs := arm_mov_ofs; sap_immediate := arm_immediate; sap_swap := arm_swap; + sap_mem_opn := arm_mem_opn; |}. (* ------------------------------------------------------------------------ *) diff --git a/proofs/compiler/arm_params_core_proof.v b/proofs/compiler/arm_params_core_proof.v index e171a218b..214b98643 100644 --- a/proofs/compiler/arm_params_core_proof.v +++ b/proofs/compiler/arm_params_core_proof.v @@ -292,7 +292,7 @@ Proof. move=> []; first done. rewrite wbaseE /= => _ [??]. right. - by apply/ZltP. + by rewrite !zify. t_arm_op. t_get_var => /=; t_arm_op => //. eexists; split; first reflexivity. diff --git a/proofs/compiler/arm_params_proof.v b/proofs/compiler/arm_params_proof.v index 0a8d97d30..43821ca90 100644 --- a/proofs/compiler/arm_params_proof.v +++ b/proofs/compiler/arm_params_proof.v @@ -10,6 +10,7 @@ Require Import compiler_util expr fexpr + fexpr_facts fexpr_sem psem psem_facts @@ -131,6 +132,184 @@ Proof. rewrite hxty hyty //=. Qed. +Lemma smart_mem_mnP mn e op wdb gd s : + smart_mem_mn mn e = Some op -> + exists (woff : wreg), + let: off := wsigned woff in + [/\ Let x := sem_pexpr wdb gd s e in to_word reg_size x = ok woff + , ~~ is_mem_immediate off + & op = Oasm (ExtOp (mn off)) + ]. +Proof. + rewrite /smart_mem_mn. + apply: obindP => w /is_wconstP -> /oassertP [h [<-]]. + by exists w. +Qed. + +Lemma sem_sopn_smart_store + gd vi s s' al ws xbase eoff es lvs' mn opts (woff : wreg) : + let: op := Oarm (ARM_op mn opts) in + let: eop := Oasm (ExtOp (Olarge_store ws (wsigned woff))) in + let: lnone := Lnone vi (sword arm_reg_size) in + let: lvs := lnone :: Lmem al ws xbase eoff :: lvs' in + ~~ set_flags opts -> + has_shift opts = None -> + ~~ is_conditional opts -> + store_mn_of_wsize ws = Some mn -> + sem_sopn gd op s (Lmem al ws xbase eoff :: lvs') es = ok s' -> + sem_sopn gd eop s lvs es = ok s'. +Proof. + move: opts => [[] [] []] //= _ _ _. + rewrite /sem_sopn /exec_sopn /= /sopn_sem => hmn. + t_xrbindP=> res args -> /= _ _ <- w'. + case: ws hmn => //= -[?]; + subst mn; + case: args => [//|v []] /=; + t_xrbindP=> // w -> [<-] ?; + by subst res. +Qed. + +Lemma sem_sopn_smart_store_cc + gd vi s s' al ws xbase eoff es lvs' mn opts (woff : wreg) : + let: op := Oarm (ARM_op mn opts) in + let: eop := Oasm (ExtOp (Olarge_store_cc ws (wsigned woff))) in + let: lnone := Lnone vi (sword arm_reg_size) in + let: lvs := lnone :: Lmem al ws xbase eoff :: lvs' in + ~~ set_flags opts -> + has_shift opts = None -> + is_conditional opts -> + store_mn_of_wsize ws = Some mn -> + sem_sopn gd op s (Lmem al ws xbase eoff :: lvs') es = ok s' -> + sem_sopn gd eop s lvs es = ok s'. +Proof. + move: opts => [[] [] []] //= _ _ _. + rewrite /sem_sopn /exec_sopn /sopn_sem => hmn. + t_xrbindP=> res args -> /= _ _ <- w'. + case: ws hmn => // -[?]; + subst mn; + case: args => [//|v0 []] /=; + t_xrbindP=> // ? -[//|? [|??]] w -> [] ->; + t_xrbindP=> //= ? -> [?] ?; + by subst res w'. +Qed. + +Lemma smart_mem_mn_storeP gd vi s s' al ws xbase eoff es lvs' op op' eop : + let: lnone := Lnone vi (sword arm_reg_size) in + let: lvs := Lmem al ws xbase eoff :: lvs' in + get_eop_store op ws = Some eop -> + sem_sopn gd op s lvs es = ok s' -> + smart_mem_mn (eop ws) eoff = Some op' -> + sem_sopn gd op' s (lnone :: lvs) es = ok s'. +Proof using. + move=> hop hsemes hop'. + have [woff [_ _ ?]] := smart_mem_mnP true gd s hop'; subst op'. + clear hop'. + rewrite /get_eop_store in hop. + case: op hop hsemes => // -[] // [[//|] []] mn opts. + move=> /oassertP [] /eqP hmn /oassertP [] /andP [] hsft /eqP hhs. + case: (boolP (is_conditional _)) => hic [<-]. + - exact: sem_sopn_smart_store_cc. + exact: sem_sopn_smart_store. +Qed. + +Lemma sem_sopn_smart_load + gd vi s s' al ws xbase eoff lvs es' mn opts (woff : wreg) : + let: op := Oarm (ARM_op mn opts) in + let: eop := Oasm (ExtOp (Olarge_load ws (wsigned woff))) in + let: lnone := Lnone vi (sword arm_reg_size) in + ~~ set_flags opts -> + has_shift opts = None -> + ~~ is_conditional opts -> + uload_mn_of_wsize ws = Some mn -> + sem_sopn gd op s lvs (Pload al ws xbase eoff :: es') = ok s' -> + sem_sopn gd eop s (lnone :: lvs) (Pload al ws xbase eoff :: es') = ok s'. +Proof. + move: opts => [[] [] []] //= _ _ _. + rewrite /sem_sopn /exec_sopn /sopn_sem => hmn. + t_xrbindP=> res args. + case: ws hmn => // -[?]; + subst mn; + case: args => [// | v []] /=; + by t_xrbindP=> // ??? -> /= -> ?? -> /= -> ? /= -> <- ? -> <- -> ?? <- ? /= + ? -> [<-] <-. +Qed. + +Lemma sem_sopn_smart_load_cc + gd vi s s' al ws xbase eoff lvs es' mn opts (woff : wreg) : + let: op := Oarm (ARM_op mn opts) in + let: eop := Oasm (ExtOp (Olarge_load_cc ws (wsigned woff))) in + let: lnone := Lnone vi (sword arm_reg_size) in + ~~ set_flags opts -> + has_shift opts = None -> + is_conditional opts -> + uload_mn_of_wsize ws = Some mn -> + sem_sopn gd op s lvs (Pload al ws xbase eoff :: es') = ok s' -> + sem_sopn gd eop s (lnone :: lvs) (Pload al ws xbase eoff :: es') = ok s'. +Proof. + move: opts => [[] [] []] //= _ _ _. + rewrite /sem_sopn /exec_sopn /sopn_sem => hmn. + t_xrbindP=> res args. + case: ws hmn => // -[?]; + subst mn; + case: args => [// | v []] /=; + t_xrbindP=> // ? [//|? [|//]]; + by t_xrbindP=> // ??? -> /= -> ?? -> /= -> ? /= -> <- ? -> <- -> _ _ <- ?? + /= -> [] -> ? -> [<-] <- /= ->. +Qed. + +Lemma smart_mem_mn_loadP gd vi s s' lvs al ws xbase eoff es' op op' eop : + let: es := Pload al ws xbase eoff :: es' in + let: lnone := Lnone vi (sword arm_reg_size) in + get_eop_load op ws = Some eop -> + sem_sopn gd op s lvs es = ok s' -> + smart_mem_mn (eop ws) eoff = Some op' -> + sem_sopn gd op' s (lnone :: lvs) es = ok s'. +Proof using. + move=> hop hsemes hop'. + have [woff [_ _ ?]] := smart_mem_mnP true gd s hop'; subst op'. + clear hop'. + rewrite /get_eop_store in hop. + case: op hop hsemes => // -[] // [[//|] []] mn opts. + move=> /oassertP [] /eqP hmn /oassertP [] /andP [] hsft /eqP hhs. + case: (boolP (is_conditional _)) => hic [<-]. + - exact: sem_sopn_smart_load_cc. + exact: sem_sopn_smart_load. +Qed. + +Lemma split_mem_opn_match_lvsP lvs lvs' al ws xbase eoff : + split_mem_opn_match_lvs lvs = Some (al, ws, xbase, eoff, lvs') <-> + lvs = Lmem al ws xbase eoff :: lvs'. +Proof. + case: lvs => [// | lv]; case: lv => //= ????. split=> -[]; congruence. +Qed. + +Lemma split_mem_opn_match_esP es es' al ws xbase eoff : + split_mem_opn_match_es es = Some (al, ws, xbase, eoff, es') <-> + es = Pload al ws xbase eoff :: es'. +Proof. + case: es => [// | e]; case: e => //= ????. split=> -[]; congruence. +Qed. + +Lemma arm_mem_opnP : sap_mem_opn_correct (sap_mem_opn arm_saparams). +Proof. + move=> sp rip s s' lvs tag op es /psem.sem_iE h. + rewrite /= /arm_mem_opn. + case hsplit: split_mem_opn => [-[[lvs' op'] es']|]; last by constructor. + constructor. + move: hsplit. + rewrite /split_mem_opn. + case hlvs: split_mem_opn_match_lvs => [[[[[al ws] xbase] eoff] ?]|]. + - move: hlvs => /split_mem_opn_match_lvsP ?; subst lvs. + apply: obindP => eop heop. + apply: obindP => op'' hop'' [???]; subst lvs' op'' es'. + exact: (smart_mem_mn_storeP _ heop h hop''). + case hes: split_mem_opn_match_es => [[[[[al ws] xbase] eoff] ?] | //]. + move: hes => /split_mem_opn_match_esP ?; subst es. + apply: obindP => eop heop. + apply: obindP => op'' hop'' [???]; subst lvs' op'' es'. + exact: (smart_mem_mn_loadP _ heop h hop''). +Qed. + End STACK_ALLOC. Definition arm_hsaparams : @@ -139,6 +318,7 @@ Definition arm_hsaparams : mov_ofsP := arm_mov_ofsP; sap_immediateP := arm_immediateP; sap_swapP := arm_swapP; + sap_mem_opnP := arm_mem_opnP; |}. (* ------------------------------------------------------------------------ *) @@ -227,10 +407,40 @@ Lemma uload_mn_of_wsizeP ws ws' mn (w : word ws) (w' : word ws') : -> truncate_word ws w' = ok w -> exec_sopn (Oarm (ARM_op mn default_opts)) [:: Vword w' ] = ok [:: Vword (zero_extend reg_size w) ]. +Proof. case: ws w => w // [?]; subst mn; by rewrite /exec_sopn /= => ->. Qed. + +Lemma uload_mn_of_wsize_ccP + ws ws' mn opts b (w : word ws) (w' : word ws') wold vold : + ~~ set_flags opts -> + is_conditional opts -> + has_shift opts = None -> + uload_mn_of_wsize ws = Some mn -> + truncate_word ws w' = ok w -> + to_word reg_size vold = ok wold -> + exec_sopn (Oarm (ARM_op mn opts)) [:: Vword w'; Vbool b; vold ] + = ok [:: Vword (if b then zero_extend reg_size w else wold) ]. Proof. - case: ws w => w // [?]; subst mn. - all: rewrite /exec_sopn /=. - all: by move=> -> /=. + move: opts => [[] [] []] //= _ _ _. + rewrite /exec_sopn /=. + case: ws w => // w [<-] /= -> ->; by case: b. +Qed. + +Lemma store_mn_of_wsize_ccP + ws ws' mn opts b (w : word ws) (w' : word ws') wold vold : + ~~ set_flags opts -> + is_conditional opts -> + has_shift opts = None -> + store_mn_of_wsize ws = Some mn -> + truncate_word ws w' = ok w -> + to_word ws vold = ok wold -> + exec_sopn (Oarm (ARM_op mn opts)) [:: Vword w'; Vbool b; vold ] + = ok [:: Vword (if b then w else wold) ]. +Proof. + move: opts => [[] [] []] //= _ _ _. + rewrite /exec_sopn /=. + case: ws w wold => // w wold [<-] /= -> -> /=; + case: b => //=; + by rewrite zero_extend_u. Qed. Lemma arm_lmove_correct : lmove_correct arm_liparams. @@ -675,32 +885,43 @@ Lemma uncons_LLvarP ii les x les' : les = LLvar x :: les'. Proof. by case: les => [// | [// | ?] ?] [-> ->]. Qed. +Lemma uncons_StoreP ii les al ws xbase eoff les' : + uncons_Store ii les = ok (al, ws, xbase, eoff, les') -> + les = Store al ws xbase eoff :: les'. +Proof. by case: les => [// | [|//]] ????? [-> -> -> -> ->]. Qed. + Lemma uncons_rvarP ii res x res' : uncons_rvar ii res = ok (x, res') -> res = rvar x :: res'. Proof. by case: res => [// | [// | [] // ?] ?] [-> ->]. Qed. -Lemma uncons_wconstP ii les imm les' : - uncons_wconst ii les = ok (imm, les') -> - exists ws, les = rconst ws imm :: les'. +Lemma uncons_LoadP ii res al ws xbase eoff res' : + uncons_Load ii res = ok (al, ws, xbase, eoff, res') -> + res = Load al ws xbase eoff :: res'. +Proof. + by case: res => [// | [|//]] ????? [-> -> -> -> ->]. +Qed. + +Lemma uncons_wconstP ii res imm res' : + uncons_wconst ii res = ok (imm, res') -> + exists ws, res = rconst ws imm :: res'. Proof. - case: les => [// | [//|]] [] // [] // ? [] // ?? [-> ->]. by eexists. + case: res => [// | [//|]] [] // [] // ? [] // ?? [-> ->]. by eexists. Qed. Lemma smart_li_argsP ii ws les res x imm res' : smart_li_args ii ws les res = ok (x, imm, res') -> [/\ ws = reg_size - , les = [:: LLvar x ] + , exists les', les = LLvar x :: les' , vtype (v_var x) = sword reg_size & exists ws', res = rconst ws' imm :: res' ]. Proof. rewrite /smart_li_args. t_xrbindP=> /eqP -> -[??] /uncons_LLvarP ->. - t_xrbindP=> /eqP ? /nilP -> [??] /uncons_wconstP [? ->]. + t_xrbindP=> /eqP ? _ [??] /uncons_wconstP [? ->]. t_xrbindP=> ???; subst. - split=> //=. - by eexists. + split=> //=; by eexists. Qed. Lemma assemble_smart_li_correct ws : assemble_extra_correct (Osmart_li ws). @@ -708,7 +929,8 @@ Proof. move=> rip ii lvs args m xs ys m' s ops ops'. move=> hsemargs hexec hwrite. rewrite /= /assemble_smart_li. - t_xrbindP=> -[[x imm] ?] /smart_li_argsP [? ? hty [ws' ?]] [?] hops heq; + t_xrbindP=> -[[x imm] ?] /smart_li_argsP [? [les' ?] hty [ws' ?]] [?] hops + heq; subst ws lvs args ops. have [vm []] := ARMFopn_coreP.li_lsem_1 m (vname (v_var x)) (v_info x) imm. @@ -725,7 +947,8 @@ Proof. rewrite /exec_sopn /= /sopn_sem /=. t_xrbindP=> w w' /truncate_wordP [hws' ?]; subst w'. case: vs => // -[?] ?; subst w ys. - t_xrbindP=> m0 vm0 hsetx ??; subst m0 m'. + t_xrbindP=> m0 vm0 hsetx ? hwrite; subst m0. + case: les' hwrite => // -[?]; subst m'. apply: (lom_eqv_ext _ heq'). move=> y. move/get_varP: hgetx => -[/= hx _ _]. @@ -746,10 +969,10 @@ Proof. move=> rip ii lvs args m xs ys m' s ops ops'. move=> hsemargs hexec hwrite. rewrite /= /assemble_smart_li_cc. - t_xrbindP=> -[[x imm] args'] /smart_li_argsP [?? hty [ws' ?]]; + t_xrbindP=> -[[x imm] args'] /smart_li_argsP [? [lvs' ?] hty [ws' ?]]; subst lvs args ws. t_xrbindP=> -[cond args] /unconsP ?; subst args'. - t_xrbindP=> hfv_cond -[y ?] /uncons_rvarP ? hmk hops heq; subst args. + t_xrbindP=> hfv_cond -[y ?] /uncons_rvarP ? [?] hops heq; subst args ops. have [vm' []] := ARMFopn_coreP.li_lsem_1 m (vname (v_var x)) (v_info x) imm. rewrite /= -hty -var_surj -var_i_surj => hsem hvm hgetx. @@ -759,8 +982,8 @@ Proof. t_xrbindP=> w w' hw' bcond /to_boolI ? wy hwy; subst vcond. move: hw' => /to_wordI [ws [w0 []]] /Vword_inj [] ?; subst ws. rewrite /= => ? /truncate_wordP [hle1 ?]; subst w0 w'. - case: vrest hsemrest; t_xrbindP=> // hsemrest ??; subst w ys. - t_xrbindP=> _ vm hsetx <- <-. + case: vrest hsemrest; t_xrbindP=> // _ ??; subst w ys. + t_xrbindP=> _ vm hsetx <- /[dup] /size_fold2 /size0nil -> /= [?]; subst m'. (* Type of [y]. *) have := type_of_get_var hgety. @@ -792,26 +1015,22 @@ Proof. heq. all: subst vmf. - - move: hmk. - rewrite /ARMFopn_core.li. - case: ifP => [_ [<-] // | _]. - by case: ifP => _ [<-]. + - rewrite /ARMFopn_core.li. + case: ifP => //; by case: ifP. - move: hsem. rewrite ARMFopnP.sem_fopns_equiv -sem_sopns_fopns_args /=. - move: hmk. rewrite /ARMFopn_core.li. - case: ifP => _. + case: ifP => _ /=. (* Case: small immediate. *) - + move=> [<-] /=. - rewrite /exec_sopn /= /sopn_sem /= truncate_word_u /=. + + rewrite /exec_sopn /= /sopn_sem /= truncate_word_u /=. t_xrbindP=> ?? vm0 hvm' <- <- [?]; subst vm0. rewrite {}hsemcond {}hgety /= truncate_word_u {}hwy /=. case: bcond hsetx => /= [|-> //]. by rewrite hvm'. - case: ifP => _ [<-] /=. + case: ifP => _ /=. (* Case: negated immediate. *) + rewrite /exec_sopn /= /sopn_sem /= truncate_word_u /=. @@ -863,13 +1082,369 @@ Proof. by rewrite Vm.setP_eq. Qed. +Lemma ok_smart_li_args ii imm x : + let: args := ARMFopn_core.li x imm in + let: les := [:: LLvar x ] in + let: res := [:: rconst reg_size imm ] in + vtype x = sword reg_size -> + to_asm ii (Osmart_li reg_size) les res = ok (asm_args_of_opn_args args). +Proof. by rewrite /= /assemble_smart_li /smart_li_args /= => ->. Qed. + +Lemma chk_assemble_large_loadP err ws woff ws' xbase tmp eoff : + chk_assemble_large_load err ws woff ws' xbase tmp eoff = ok tt -> + [/\ ws = ws' + , forall vm, Let off := sem_fexpr vm eoff in to_word reg_size off = ok woff + , v_var xbase <> v_var tmp + , ~~ Sv.mem tmp (free_vars eoff) + & vtype tmp = sword reg_size + ]. +Proof. + rewrite /chk_assemble_large_load. + t_xrbindP=> /eqP ? /eqP /[dup] h /is_fwconstP h' /eqP ? /eqP ?. + split=> //. + case: eoff h h' => //= -[] // ? [] //=; by rewrite if_same. +Qed. + +Lemma assemble_large_load_correct ws off : + assemble_extra_correct (Olarge_load ws off). +Proof. + move=> rip ii lvs args s vargs vres s' xm ops ops' hsemargs hexec hwrite h + hops' heq. + move: h. + rewrite /= /assemble_large_load. + t_xrbindP=> mn /o2rP hmn [tmp les] /uncons_LLvarP ?; subst lvs. + t_xrbindP=> -[x les'] /uncons_LLvarP ?; subst les. + t_xrbindP=> -[[[[al ws'] xbase] eoff] args'] /uncons_LoadP ?; subst args. + t_xrbindP=> /chk_assemble_large_loadP [? hsemeoff hneq _ hty] ?; + subst ws' ops. + move: hsemargs => /=. + t_xrbindP=> _ wbase vbase hgetbase hwbase woff voff hsemeoff' hwoff w hread <- + vargs' _ ?; subst vargs. + move: (hsemeoff (evm s)). + rewrite {}hsemeoff' /= hwoff => -[?]; subst woff. + move: hops'. + rewrite -cats1 mapM_cat; t_xrbindP=> ops_li hli ops_ldr hldr ?; subst ops'. + move: hexec. + rewrite /exec_sopn /= truncate_word_le //=. + case: vargs' => //= -[?]; subst vres. + move: hwrite => /=. + rewrite zero_extend_u. + t_xrbindP=> _ vm /set_varP [_ htrunctmp ?] <- _ vm' /set_varP [_ htruncx ?] <- + hs'; subst vm vm'. + move: hs'. + rewrite with_vm_idem /=. + case: les' => // -[?]; subst s'. + + (* Load offset to [tmp]. *) + have [vmi []] := + ARMFopn_coreP.li_lsem_1 s (vname (v_var tmp)) (v_info tmp) off. + rewrite /= -hty -var_surj -var_i_surj => hsem_li hvmi hgettmp. + have [] := + assemble_opsP (m' := with_vm s vmi) arm_eval_assemble_cond hli _ _ heq. + - rewrite /ARMFopn_core.li. case: ifP => //. by case: ifP. + - move: hsem_li. + by rewrite ARMFopnP.sem_fopns_equiv -sem_sopns_fopns_args /= => ->. + move=> xmi heval_li heqi. + + (* Load from memory at address [xbase + tmp]. *) + set vmi' := vmi.[x <- Vword (zero_extend reg_size w)]. + have [|xmi' heval_ldr heqi'] := + assemble_opsP + (m' := with_vm s vmi') arm_eval_assemble_cond hldr erefl _ heqi. + - rewrite /= (get_var_eq_ex (x := xbase) _ _ hvmi); + last by apply/Sv.singleton_spec. + rewrite hgetbase /= hwbase /= hgettmp /= truncate_word_u /= hread /=. + rewrite (uload_mn_of_wsizeP hmn (truncate_word_u w)) /=. + by rewrite set_var_truncate. + subst vmi'. + + exists xmi'. + - by rewrite foldM_cat heval_li. + apply: (lom_eqv_ext _ heqi') => /= y. + case: (v_var x =P y) => [<- | /eqP ?]. + - by rewrite !Vm.setP_eq. + rewrite Vm.setP_neq // Vm.setP_neq //. + case: (v_var tmp =P y) => [<- | /eqP ?]. + - move: hgettmp => /get_varP [<- _ _]. + by rewrite Vm.setP_eq /= hty cmp_le_refl. + rewrite Vm.setP_neq //. + rewrite hvmi //. + by apply/Sv.singleton_spec/nesym/eqP. +Qed. + +Lemma assemble_large_load_cc_correct ws off : + assemble_extra_correct (Olarge_load_cc ws off). +Proof. + move=> rip ii lvs args s vargs vres s' xm ops ops' hsemargs hexec hwrite h + hops' heq. + move: h. + rewrite /= /assemble_large_load_cc. + t_xrbindP=> mn /o2rP hmn [tmp les] /uncons_LLvarP ?; subst lvs. + t_xrbindP=> -[x les'] /uncons_LLvarP ?; subst les. + t_xrbindP=> -[[[[al ws'] xbase] eoff] args'] /uncons_LoadP ?; subst args. + t_xrbindP=> -[cond res] /unconsP ?; subst args'. + t_xrbindP=> htmpcond htmpres /chk_assemble_large_loadP [? hsemeoff hneq _ hty] + ?; + subst ws' ops. + + move: hsemargs => /=. + t_xrbindP=> _ wbase vbase hgetbase hwbase woff voff hsemeoff' hwoff w hread <- + _ vcond hsemcond vold hsemold <- ?; + subst vargs. + move: (hsemeoff (evm s)). + rewrite {}hsemeoff' /= hwoff => -[?]; subst woff. + move: hops'. + rewrite -cats1 mapM_cat; t_xrbindP=> ops_li hli ops_ldr hldr ?; subst ops'. + move: hexec. + rewrite /exec_sopn /= truncate_word_le //=. + t_xrbindP=> -[/= w0 w1] b /to_boolI ?; subst vcond. + case: vold hsemold => //. + t_xrbindP=> vold [|//] hsemres wold hwold [??] ?; subst vres w0 w1. + + move: hwrite => /=. + t_xrbindP=> _ vm /set_varP [_ htrunctmp ?] <- _ vm' /set_varP [_ htruncx ?] <- + hs'; subst vm vm'. + move: hs'. + rewrite with_vm_idem /=. + case: les' => // -[?]; subst s'. + + (* Load offset to [tmp]. *) + have [vmi []] := + ARMFopn_coreP.li_lsem_1 s (vname (v_var tmp)) (v_info tmp) off. + rewrite /= -hty -var_surj -var_i_surj => hsem_li hvmi hgettmp. + have [] := + assemble_opsP (m' := with_vm s vmi) arm_eval_assemble_cond hli _ _ heq. + - rewrite /ARMFopn_core.li. case: ifP => //. by case: ifP. + - move: hsem_li. + by rewrite ARMFopnP.sem_fopns_equiv -sem_sopns_fopns_args /= => ->. + move=> xmi heval_li heqi. + + (* Load from memory at address [xbase + tmp]. *) + set w' := if b then zero_extend arm_reg_size w else wold. + set vmi' := vmi.[x <- Vword w']. + have [|xmi' heval_ldr heqi'] := + assemble_opsP + (m' := with_vm s vmi') arm_eval_assemble_cond hldr erefl _ heqi. + - rewrite /= (get_var_eq_ex (x := xbase) _ _ hvmi); + last by apply/Sv.singleton_spec. + rewrite hgetbase /= hwbase /= hgettmp /= truncate_word_u /= hread /=. + rewrite (sem_rexpr_eq_ex (emem s) _ hvmi); + last by rewrite disjoint_singleton. + rewrite hsemcond /= (sem_rexprs_eq_ex _ hvmi); + last by rewrite disjoint_singleton. + by rewrite hsemres /= + (uload_mn_of_wsize_ccP _ _ _ _ hmn (truncate_word_u w) hwold) //= + set_var_truncate. + subst vmi'. + + exists xmi'. + - by rewrite foldM_cat heval_li. + apply: (lom_eqv_ext _ heqi') => /= y. + case: (v_var x =P y) => [<- | /eqP ?]. + - rewrite !Vm.setP_eq. + subst w'. + case: b hsemcond heqi' htruncx => //= _ _ _. + by rewrite zero_extend_u. + rewrite Vm.setP_neq // Vm.setP_neq //. + case: (v_var tmp =P y) => [<- | /eqP ?]. + - move: hgettmp => /get_varP [<- _ _]. + rewrite Vm.setP_eq /= hty cmp_le_refl. + by case: b w' hsemcond heqi' htruncx => //=. + rewrite Vm.setP_neq //. + rewrite hvmi //. + by apply/Sv.singleton_spec/nesym/eqP. +Qed. + +Lemma chk_assemble_large_storeP err ws woff ws' x xbase tmp eoff : + chk_assemble_large_store err ws woff ws' x xbase tmp eoff = ok tt -> + [/\ ws = ws' + , forall vm, Let off := sem_fexpr vm eoff in to_word reg_size off = ok woff + , v_var xbase <> v_var tmp + , vtype tmp = sword reg_size + , ~~ Sv.mem tmp (free_vars eoff) + & v_var x <> v_var tmp + ]. +Proof. + rewrite /chk_assemble_large_store. + by t_xrbindP=> /chk_assemble_large_loadP [?????] /eqP. +Qed. + +Lemma assemble_large_store_correct ws off : + assemble_extra_correct (Olarge_store ws off). +Proof. + move=> rip ii lvs args s vargs vres s' xm ops ops' hsemargs hexec hwrite h + hops' heq. + move: h. + rewrite /= /assemble_large_store. + t_xrbindP=> mn /o2rP hmn [tmp les] /uncons_LLvarP ?; subst lvs. + t_xrbindP=> -[[[[al ws'] xbase] eoff] les'] /uncons_StoreP ?; subst les. + t_xrbindP=> -[x res'] /uncons_rvarP ?; subst args. + t_xrbindP=> /chk_assemble_large_storeP [? hsemeoff hneqbase hty _ hneqx] ?; + subst ws' ops. + move: hsemargs => /=. + t_xrbindP=> vx hgetx vargs' hsemres' ?; subst vargs. + move: hops'. + rewrite -cats1 mapM_cat; t_xrbindP=> ops_li hli ops_ldr hstr ?; subst ops'. + move: hexec. + rewrite /exec_sopn /=. + t_xrbindP. + case: vargs' hsemres' => // hsemres' [_ _] w /to_wordI [ws' [wx [? hwx]]] + [<- <-] ?; subst vx vres. + move: hsemres' => /size_mapM /size0nil ?; subst res'. + move: hwrite => /=. + rewrite zero_extend_u. + t_xrbindP=> _ vm /set_varP [_ htrunctmp ?] <- /= _ wbase vbase hgetbase hwbase + woff voff hsemeoff' hwoff w' hw' m hwrite <- hs'; subst vm. + rewrite get_var_neq in hgetbase; last by apply/nesym. + move: (hsemeoff (evm s).[tmp <- Vword (wrepr arm_reg_size off)]). + rewrite {}hsemeoff' /= hwoff => -[?]; subst woff. + move: hw'. + rewrite truncate_word_u => -[?]; subst w'. + move: hs'. + case: les' => // -[?]; subst s'. + + (* Load offset to [tmp]. *) + have [vmi []] := + ARMFopn_coreP.li_lsem_1 s (vname (v_var tmp)) (v_info tmp) off. + rewrite /= -hty -var_surj -var_i_surj => hsem_li hvmi hgettmp. + have [] := + assemble_opsP (m' := with_vm s vmi) arm_eval_assemble_cond hli _ _ heq. + - rewrite /ARMFopn_core.li. case: ifP => //. by case: ifP. + - move: hsem_li. + by rewrite ARMFopnP.sem_fopns_equiv -sem_sopns_fopns_args /= => ->. + move=> xmi heval_li heqi. + + set si := with_vm s vmi. + (* Store to memory at address [xbase + tmp]. *) + have [|xmi' heval_str heqi'] := + assemble_opsP + (m' := with_mem si m) arm_eval_assemble_cond hstr erefl _ heqi. + - rewrite /= (get_var_eq_ex (x := x) _ _ hvmi); + last by apply/Sv.singleton_spec. + rewrite hgetx /= (store_mn_of_wsizeP hmn hwx) /=. + rewrite (get_var_eq_ex (x := xbase) _ _ hvmi); + last by apply/Sv.singleton_spec. + by rewrite hgetbase /= hwbase /= hgettmp /= !truncate_word_u /= hwrite. + subst si. + + exists xmi'. + - by rewrite foldM_cat heval_li. + apply: (lom_eqv_ext _ heqi') => /= y. + case: (v_var tmp =P y) => [<- | /eqP ?]. + - move: hgettmp => /get_varP [<- _ _]. + by rewrite Vm.setP_eq /= hty cmp_le_refl. + rewrite Vm.setP_neq //. + rewrite hvmi //. + by apply/Sv.singleton_spec/nesym/eqP. +Qed. + +Lemma assemble_large_store_cc_correct ws off : + assemble_extra_correct (Olarge_store_cc ws off). +Proof. + move=> rip ii lvs args s vargs vres s' xm ops ops' hsemargs hexec hwrite h + hops' heq. + move: h. + rewrite /= /assemble_large_store_cc. + t_xrbindP=> mn /o2rP hmn [tmp les] /uncons_LLvarP ?; subst lvs. + t_xrbindP=> -[[[[al ws'] xbase] eoff] les'] /uncons_StoreP ?; subst les. + t_xrbindP=> -[x res'] /uncons_rvarP ?; subst args. + t_xrbindP=> -[cond res] /unconsP ?; subst res'. + t_xrbindP=> -[[[[al' ws''] xbase'] eoff'] res'] /uncons_LoadP ?; subst res. + t_xrbindP=> hcond /andP [/eqP hxbase' heoff_eoff'] /chk_assemble_large_storeP + [? hsemeoff hneqbase hty hneqoff hneqx] ?; + subst ws' ops. + + move: hsemargs => /=. + t_xrbindP=> vx hgetx _ varg hsemcond _ _ wbase' vbase' + hgetbase' hwbase' woff' voff' hsemeoff' hwoff' w'' hread <- vres' hsemres' + <- <- ?; + subst vargs. + move: hops'. + rewrite -cats1 mapM_cat; t_xrbindP=> ops_li hli ops_ldr hstr ?; subst ops'. + move: hexec. + rewrite /exec_sopn /=. + t_xrbindP. + case: vres' hsemres' => // /size_mapM /size0nil ?; subst res'. + move=> [/= w0 w] w1 /to_wordI [ws' [wx [? hwx]]] b /to_boolI ? wold + hwold [??] ?; + subst varg vres w0 w vx. + move: hwrite => /=. + rewrite truncate_word_u zero_extend_u. + t_xrbindP=> _ vm /set_varP [_ htrunctmp ?] <- /= _ wbase vbase hgetbase hwbase + woff voff hsemeoff0 hwoff _ <- m hwrite <- hs'; subst vm. + rewrite get_var_neq in hgetbase; last by apply/nesym. + move: (hsemeoff (evm s).[tmp <- Vword (wrepr arm_reg_size off)]). + rewrite hsemeoff0 /= hwoff => -[?]; subst woff. + move: hsemeoff0. + rewrite (eq_fexpr_sem_fexpr _ heoff_eoff'). + rewrite (sem_fexpr_eq_ex (vm2 := evm s) (xs := Sv.singleton tmp)); first last. + - by apply: eq_ex_set_l => // /Sv.singleton_spec. + - by rewrite -(eq_fexpr_free_vars heoff_eoff') disjoint_singleton. + rewrite hsemeoff' => -[?]; subst voff'. + move: hwoff' => /to_wordI [ws0 [woff [? hwoff']]]; subst voff. + move: hwoff' => /truncate_wordP [hws0 ?]; subst woff'. + move: hwoff => /to_wordI [ws1 [woff' [h hwoff']]]. + move: h => /Vword_inj [?]; subst ws1. + rewrite /= => ?; subst woff'. + move: hwoff' => /truncate_wordP [_ hwoff]. + rewrite -hwoff in hread. + move: hs'. + case: les' => // -[?]; subst s'. + + (* Load offset to [tmp]. *) + have [vmi []] := + ARMFopn_coreP.li_lsem_1 s (vname (v_var tmp)) (v_info tmp) off. + rewrite /= -hty -var_surj -var_i_surj => hsem_li hvmi hgettmp. + have [] := + assemble_opsP (m' := with_vm s vmi) arm_eval_assemble_cond hli _ _ heq. + - rewrite /ARMFopn_core.li. case: ifP => //. by case: ifP. + - move: hsem_li. + by rewrite ARMFopnP.sem_fopns_equiv -sem_sopns_fopns_args /= => ->. + move=> xmi heval_li heqi. + + set si := with_vm s vmi. + (* Store to memory at address [xbase + tmp]. *) + have [|xmi' heval_str heqi'] := + assemble_opsP + (m' := with_mem si m) arm_eval_assemble_cond hstr erefl _ heqi. + - rewrite /= (get_var_eq_ex (x := x) _ _ hvmi); + last by apply/Sv.singleton_spec. + rewrite hgetx /=. + rewrite (sem_rexpr_eq_ex (emem s) _ hvmi); + last by rewrite disjoint_singleton. + rewrite hsemcond /=. + rewrite (get_var_eq_ex (x := xbase) _ _ hvmi); + last by apply/Sv.singleton_spec. + rewrite hgetbase /= hwbase /= hgettmp /= truncate_word_u /=. + rewrite (get_var_eq_ex (x := xbase') _ _ hvmi); first last. + - rewrite -hxbase'. by apply/Sv.singleton_spec. + rewrite hgetbase' /= hwbase' /= hread /=. + by rewrite (store_mn_of_wsize_ccP (wold := wold) _ _ _ _ hmn hwx) //= + truncate_word_u /= hwrite. + subst si. + + exists xmi'. + - by rewrite foldM_cat heval_li. + apply: (lom_eqv_ext _ heqi') => /= y. + case: (v_var tmp =P y) => [<- | /eqP ?]. + - move: hgettmp => /get_varP [<- _ _]. + by rewrite Vm.setP_eq /= hty cmp_le_refl. + rewrite Vm.setP_neq //. + rewrite hvmi //. + by apply/Sv.singleton_spec/nesym/eqP. +Qed. + Lemma arm_assemble_extra_op op : assemble_extra_correct op. Proof. case: op. + exact: assemble_swap_correct. + exact: assemble_add_large_imm_correct. + exact: assemble_smart_li_correct. - exact: assemble_smart_li_cc_correct. + + exact: assemble_smart_li_cc_correct. + + exact: assemble_large_load_correct. + + exact: assemble_large_store_correct. + + exact: assemble_large_load_cc_correct. + exact: assemble_large_store_cc_correct. Qed. Definition arm_hagparams : h_asm_gen_params (ap_agp arm_params) := diff --git a/proofs/compiler/arm_stack_zeroization.v b/proofs/compiler/arm_stack_zeroization.v index fb4d05f53..f5ceba796 100644 --- a/proofs/compiler/arm_stack_zeroization.v +++ b/proofs/compiler/arm_stack_zeroization.v @@ -111,11 +111,26 @@ Definition stack_zero_loop_vars := (ws)[rsp + wsize_size ws] = zero (ws)[rsp + 0] = zero *) -Definition sz_unrolled : lcmd := +Definition sz_unrolled_aux : lcmd := let rn := rev (ziota 0 (stk_max / wsize_size ws)) in [seq MkLI dummy_instr_info (store_zero (fconst reg_size (off * wsize_size ws))) | off <- rn ]. -Definition stack_zero_unrolled : lcmd := sz_init ++ sz_unrolled ++ restore_sp. +Definition sz_unrolled err : cexec lcmd := + let max := (stk_max / wsize_size ws)%Z in + let e := + let s := + [:: pp_s "Stack too large for strategy ""unrolled"" (the offsets don't" + ; pp_s "fit in the instruction encoding)." + ] + in + err (pp_box s) + in + Let _ := assert (is_mem_immediate ((max - 1) * wsize_size ws)) e in + ok sz_unrolled_aux. + +Definition stack_zero_unrolled err : cexec lcmd := + Let c := sz_unrolled err in + ok (sz_init ++ c ++ restore_sp). (* [voff] is used, because it is set by [sz_init], even though it is not used in the for loop. *) @@ -131,9 +146,9 @@ Definition stack_zeroization_cmd (ws_align ws : wsize) (stk_max : Z) : cexec (lcmd * Sv.t) := - let err msg := + let err pp := {| - pel_msg := compiler_util.pp_s msg; + pel_msg := pp; pel_fn := None; pel_fi := None; pel_ii := None; @@ -142,18 +157,20 @@ Definition stack_zeroization_cmd pel_internal := false; |} in - let err_size := - err "Stack zeroization size not supported in ARMv7"%string in + let err_size := err (pp_s "Stack zeroization size not supported in ARMv7") in Let _ := assert (ws <= U32)%CMP err_size in let rsp := vid rspn in match szs with | SZSloop => ok (stack_zero_loop rsp lbl ws_align ws stk_max, stack_zero_loop_vars) | SZSloopSCT => - let err_sct := err "Strategy ""loop with SCT"" is not supported in ARMv7"%string in + let err_sct := + err (pp_s "Strategy ""loop with SCT"" is not supported in ARMv7") + in Error err_sct | SZSunrolled => - ok (stack_zero_unrolled rsp ws_align ws stk_max, stack_zero_unrolled_vars) + Let c := stack_zero_unrolled rsp ws_align ws stk_max err in + ok (c, stack_zero_unrolled_vars) end. End STACK_ZEROIZATION. diff --git a/proofs/compiler/arm_stack_zeroization_proof.v b/proofs/compiler/arm_stack_zeroization_proof.v index e1f6d892c..36f3d4234 100644 --- a/proofs/compiler/arm_stack_zeroization_proof.v +++ b/proofs/compiler/arm_stack_zeroization_proof.v @@ -491,7 +491,8 @@ Section UNROLLED. Context (hsmall : (ws <= U32)%CMP). Context (pre pos : seq linstr). -Context (hbody : is_linear_of lp fn (pre ++ sz_unrolled rspi ws stk_max ++ pos)). +Context + (hbody : is_linear_of lp fn (pre ++ sz_unrolled_aux rspi ws stk_max ++ pos)). Lemma unrolled_bodyP vars s1 s2 n : state_rel_unrolled vars s1 s2 (stk_max - Z.of_nat n * wsize_size ws) top -> @@ -586,11 +587,12 @@ Local Opaque wsize_size Z.of_nat. Local Transparent wsize_size Z.of_nat. Qed. -Lemma sz_unrolledP vars s1 s2 : +Lemma sz_unrolled_auxP vars s1 s2 : state_rel_unrolled vars s1 s2 stk_max top -> exists s3, + let c := sz_unrolled_aux rspi ws stk_max in [/\ lsem lp (of_estate s2 fn (size pre)) - (of_estate s3 fn (size pre + size (sz_unrolled rspi ws stk_max))) + (of_estate s3 fn (size pre + size c)) & state_rel_unrolled vars s1 s3 0 top]. Proof. move=> hsr. @@ -687,20 +689,36 @@ End STACK_ZERO_LOOP. Section STACK_ZERO_UNROLLED. -Context (hsmall : (ws <= U32)%CMP). -Context (pre pos : seq linstr). -Context (hbody : is_linear_of lp fn (pre ++ stack_zero_unrolled rspi ws_align ws stk_max ++ pos)). -Context (rsp_nin : ~ Sv.In rspi stack_zero_unrolled_vars). +Context + (hsmall : (ws <= U32)%CMP) + (pre csz pos : seq linstr) + (err : compiler_util.pp_error -> compiler_util.pp_error_loc) + (hcsz : stack_zero_unrolled rspi ws_align ws stk_max err = ok csz) + (hbody : is_linear_of lp fn (pre ++ csz ++ pos)) + (rsp_nin : ~ Sv.In rspi stack_zero_unrolled_vars) +. + +Lemma cszE : + csz + = sz_init rspi ws_align stk_max + ++ sz_unrolled_aux rspi ws stk_max + ++ restore_sp rspi. +Proof. + move: hcsz. + rewrite /stack_zero_unrolled /sz_unrolled. + by t_xrbindP=> lc _ ??; subst lc csz. +Qed. Lemma stack_zero_unrolledP (s1 : estate) : valid_between (emem s1) top stk_max -> (evm s1).[rspi] = Vword ptr -> exists s2, [/\ lsem lp (of_estate s1 fn (size pre)) - (of_estate s2 fn (size pre + size (stack_zero_unrolled rspi ws_align ws stk_max))) + (of_estate s2 fn (size pre + size csz)) & state_rel_unrolled stack_zero_unrolled_vars s1 s2 0 ptr]. Proof. move=> hvalid hrsp. + have ? := cszE; subst csz. move: hbody; rewrite /stack_zero_loop -!catA => hbody'. have hsubset_init: Sv.Subset sz_init_vars stack_zero_unrolled_vars. + move=> x /sv_of_listP hin. @@ -712,7 +730,7 @@ Proof. have [s2 [hsem2 hsr2]] := sz_initP hbody' rsp_nin_init hvalid hrsp. move: hbody'; rewrite catA => hbody'. have hsr2' := state_rel_unrolledI hsubset_init hsr2. - have [s3 [hsem3 hsr3]] := sz_unrolledP hsmall hbody' hsr2'. + have [s3 [hsem3 hsr3]] := sz_unrolled_auxP hsmall hbody' hsr2'. move: hbody'; rewrite catA => hbody'. have hsubset_restore: Sv.Subset restore_sp_vars stack_zero_loop_vars. + move=> x /sv_of_listP hin. @@ -753,11 +771,12 @@ Proof. + move=> [<- _]. rewrite /stack_zero_loop !label_in_lcmd_cat sz_init_no_ext_lbl. by rewrite /= store_zero_no_ext_lbl. - + move=> [<- _]. - rewrite /stack_zero_unrolled !label_in_lcmd_cat sz_init_no_ext_lbl. - rewrite /= cats0. - rewrite /sz_unrolled. - by elim: rev => [//|?? ih] /=; rewrite store_zero_no_ext_lbl. + rewrite /stack_zero_unrolled /sz_unrolled /sz_unrolled_aux. + Opaque sz_init. + t_xrbindP=> lc lc' _ ????; subst lc lc' cmd vars. + Transparent sz_init. + rewrite !label_in_lcmd_cat sz_init_no_ext_lbl /= cats0. + by elim: rev => [//|???] /=; rewrite !store_zero_no_ext_lbl. Qed. Lemma arm_stack_zero_cmdP szs rspn lbl ws_align ws stk_max cmd vars : @@ -786,16 +805,22 @@ Proof. lt_0_stk_max halign le_ws_ws_align hstack ws_small hlinear rsp_nin hlabel (s1 := to_estate _) hvalid hrsp. by rewrite -{1}hfn -{1}hpc of_estate_to_estate. - + move=> [??]; subst cmd vars. - have hlinear: [elaborate - is_linear_of lp fn - (lc - ++ stack_zero_unrolled (vid rspn) ws_align ws stk_max - ++ [::])]. + + t_xrbindP=> csz hcsz ??; subst cmd vars. + have hlinear : is_linear_of lp fn (lc ++ csz ++ [::]). + by rewrite cats0; exists lfd. - have := stack_zero_unrolledP - lt_0_stk_max halign le_ws_ws_align hstack ws_small hlinear rsp_nin - (s1 := to_estate _) hvalid hrsp. + have := + stack_zero_unrolledP + lt_0_stk_max + halign + le_ws_ws_align + hstack + ws_small + hcsz + hlinear + rsp_nin + (s1 := to_estate _) + hvalid + hrsp. by rewrite -{1}hfn -{1}hpc of_estate_to_estate. exists (emem s2), (evm s2); split=> //. diff --git a/proofs/compiler/compiler.v b/proofs/compiler/compiler.v index d8fe5d5c5..57db8d4c8 100644 --- a/proofs/compiler/compiler.v +++ b/proofs/compiler/compiler.v @@ -391,6 +391,7 @@ Definition compiler_front_end (entries: seq funname) (p: prog) : cexec sprog := (ao_globals ao) (ao_global_alloc ao) (ao_stack_alloc ao) + (warning cparams) pl in let ps : sprog := cparams.(print_sprog) StackAllocation ps in diff --git a/proofs/compiler/compiler_proof.v b/proofs/compiler/compiler_proof.v index 2b8183ac0..9ca66e685 100644 --- a/proofs/compiler/compiler_proof.v +++ b/proofs/compiler/compiler_proof.v @@ -335,7 +335,7 @@ Qed. (* TODO: move *) Remark sp_globs_stack_alloc rip rsp data ga la (p: uprog) (p': sprog) : - alloc_prog (ap_shp aparams) (ap_sap aparams) (fresh_var_ident cparams (Reg (Normal, Direct)) dummy_instr_info 0) rip rsp data ga la p = ok p' → + alloc_prog (ap_shp aparams) (ap_sap aparams) (fresh_var_ident cparams (Reg (Normal, Direct)) dummy_instr_info 0) rip rsp data ga la (warning cparams) p = ok p' → sp_globs (p_extra p') = data. Proof. by rewrite /alloc_prog; t_xrbindP => ???? _ <-. diff --git a/proofs/compiler/compiler_util.v b/proofs/compiler/compiler_util.v index ce8406fc8..6096e920f 100644 --- a/proofs/compiler/compiler_util.v +++ b/proofs/compiler/compiler_util.v @@ -12,7 +12,9 @@ Local Unset Elimination Schemes. * -------------------------------------------------------------------------- *) Variant warning_msg : Set := - | Use_lea. + | Use_lea + | Split_memory_access +. (* ** Compiler error * -------------------------------------------------------------------------- *) diff --git a/proofs/compiler/stack_alloc.v b/proofs/compiler/stack_alloc.v index 29696d6a6..c05ebe7d4 100644 --- a/proofs/compiler/stack_alloc.v +++ b/proofs/compiler/stack_alloc.v @@ -474,6 +474,9 @@ Record stack_alloc_params := (* [sap_swap t d1 d2 s1 s2] is equivalent to d1,d2 = s2, s1 *) sap_swap : assgn_tag -> var_i -> var_i -> var_i -> var_i -> instr_r; + (* Build an instruction to perform an operation with a memory operand. + Return the instruction and indicate whether we should issue a warning. *) + sap_mem_opn : seq lval -> assgn_tag -> sopn -> seq pexpr -> instr_r * bool; }. Variant mov_kind := @@ -1209,6 +1212,8 @@ Definition alloc_array_swap rmap rs t es := Error (stk_error_no_var "swap: invalid args or result, only reg ptr are accepted") end. +Context (warning : instr_info -> warning_msg -> instr_info). + Fixpoint alloc_i sao (rmap:region_map) (i: instr) : cexec (region_map * cmd) := let (ii, ir) := i in @@ -1231,9 +1236,11 @@ Fixpoint alloc_i sao (rmap:region_map) (i: instr) : cexec (region_map * cmd) := Let rs := add_iinfo ii (alloc_array_swap rmap rs t e) in ok (rs.1, [:: MkI ii rs.2]) else - Let e := add_iinfo ii (alloc_es rmap e (sopn_tin o)) in - Let rs := add_iinfo ii (alloc_lvals rmap rs (sopn_tout o)) in - ok (rs.1, [:: MkI ii (Copn rs.2 t o e)]) + Let es := add_iinfo ii (alloc_es rmap e (sopn_tin o)) in + Let: (rmap, rs) := add_iinfo ii (alloc_lvals rmap rs (sopn_tout o)) in + let '(i, warn) := sap_mem_opn saparams rs t o es in + let ii := if warn then warning ii Split_memory_access else ii in + ok (rmap, [:: MkI ii i ]) | Csyscall rs o es => alloc_syscall ii rmap rs o es @@ -1442,7 +1449,15 @@ Definition init_params mglob stack disj lmap rmap sao_params params := fmapM2 (stk_ierror_no_var "invalid function info") (init_param mglob stack) (disj, lmap, rmap) sao_params params. -Definition alloc_fd_aux p_extra mglob (fresh_reg : string -> stype -> Ident.ident) (local_alloc: funname -> stk_alloc_oracle_t) sao fd : cexec _ufundef := +Definition alloc_fd_aux + (p_extra : sprog_extra) + (mglob : Mvar.t (Z * wsize)) + (fresh_reg : string -> stype -> Ident.ident) + (local_alloc: funname -> stk_alloc_oracle_t) + (warning : instr_info -> warning_msg -> instr_info) + (sao : stk_alloc_oracle_t) + (fd : _fundef unit) : + cexec _ufundef := let vrip := {| vtype := sword Uptr; vname := p_extra.(sp_rip) |} in let vrsp := {| vtype := sword Uptr; vname := p_extra.(sp_rsp) |} in let vxlen := {| vtype := sword Uptr; vname := fresh_reg "__len__"%string (sword Uptr) |} in @@ -1472,7 +1487,7 @@ Definition alloc_fd_aux p_extra mglob (fresh_reg : string -> stype -> Ident.iden assert_check (local_size <=? sao.(sao_max_size))%Z (stk_ierror_no_var "sao_max_size too small") in - Let rbody := fmapM (alloc_i pmap local_alloc sao) rmap fd.(f_body) in + Let rbody := fmapM (alloc_i pmap local_alloc warning sao) rmap fd.(f_body) in let: (rmap, body) := rbody in Let res := check_results pmap rmap paramsi fd.(f_params) sao.(sao_return) fd.(f_res) in @@ -1485,9 +1500,17 @@ Definition alloc_fd_aux p_extra mglob (fresh_reg : string -> stype -> Ident.iden f_res := res; f_extra := f_extra fd |}. -Definition alloc_fd p_extra mglob (fresh_reg : string -> stype -> Ident.ident) (local_alloc: funname -> stk_alloc_oracle_t) fn fd := +Definition alloc_fd + (p_extra : sprog_extra) + (mglob : Mvar.t (Z * wsize)) + (fresh_reg : string -> stype -> Ident.ident) + (local_alloc: funname -> stk_alloc_oracle_t) + (warning : instr_info -> warning_msg -> instr_info) + (fn : funname) + (fd : _fundef unit) : + cexec sfundef := let: sao := local_alloc fn in - Let fd := alloc_fd_aux p_extra mglob fresh_reg local_alloc sao fd in + Let fd := alloc_fd_aux p_extra mglob fresh_reg local_alloc warning sao fd in let f_extra := {| sf_align := sao.(sao_align); sf_stk_sz := sao.(sao_size); @@ -1578,8 +1601,11 @@ Definition init_map (l:list (var * wsize * Z)) data (gd:glob_decls) : cexec (Mva (stk_ierror_no_var "missing globals") in ok mvar. -Definition alloc_prog (fresh_reg : string -> stype -> Ident.ident) - rip rsp global_data global_alloc local_alloc (P:_uprog) : cexec _sprog := +Definition alloc_prog + (fresh_reg : string -> stype -> Ident.ident) + rip rsp global_data global_alloc local_alloc warning + (P : _uprog) : + cexec _sprog := Let mglob := init_map global_alloc global_data P.(p_globs) in let p_extra := {| sp_rip := rip; @@ -1588,7 +1614,8 @@ Definition alloc_prog (fresh_reg : string -> stype -> Ident.ident) sp_glob_names := global_alloc; |} in Let _ := assert (rip != rsp) (stk_ierror_no_var "rip and rsp clash") in - Let p_funs := map_cfprog_name (alloc_fd p_extra mglob fresh_reg local_alloc) P.(p_funcs) in + let alloc := alloc_fd p_extra mglob fresh_reg local_alloc warning in + Let p_funs := map_cfprog_name alloc P.(p_funcs) in ok {| p_funcs := p_funs; p_globs := [::]; p_extra := p_extra; diff --git a/proofs/compiler/stack_alloc_proof.v b/proofs/compiler/stack_alloc_proof.v index 56c902b8e..694b233d4 100644 --- a/proofs/compiler/stack_alloc_proof.v +++ b/proofs/compiler/stack_alloc_proof.v @@ -2514,6 +2514,13 @@ Qed. (* ------------------------------------------------------------------ *) +Definition sap_mem_opn_correct + (mem_opn : seq lval -> assgn_tag -> sopn -> seq pexpr -> instr_r * bool) : + Prop := + forall (P' : sprog) rip s s' lvs tag op es, + sem_i P' rip s (Copn lvs tag op es) s' -> + sem_i P' rip s (mem_opn lvs tag op es).1 s'. + Record h_stack_alloc_params (saparams : stack_alloc_params) := { (* [mov_ofs] must behave as described in stack_alloc.v. *) @@ -2537,7 +2544,8 @@ Record h_stack_alloc_params (saparams : stack_alloc_params) := (evm s).[z] = Vword pz -> (evm s).[w] = Vword pw -> sem_i P' rip s (sap_swap saparams tag x y z w) - (with_vm s ((evm s).[x <- Vword pw]).[y <- Vword pz]) + (with_vm s ((evm s).[x <- Vword pw]).[y <- Vword pz]); + sap_mem_opnP : sap_mem_opn_correct (sap_mem_opn saparams); }. Context diff --git a/proofs/compiler/stack_alloc_proof_2.v b/proofs/compiler/stack_alloc_proof_2.v index 610f6bcd4..f51bd0709 100644 --- a/proofs/compiler/stack_alloc_proof_2.v +++ b/proofs/compiler/stack_alloc_proof_2.v @@ -1829,14 +1829,15 @@ Context (shparams : slh_lowering.sh_params) (hshparams : slh_lowering_proof.h_sh_params shparams) (saparams : stack_alloc_params) - (hsaparams : h_stack_alloc_params saparams). + (hsaparams : h_stack_alloc_params saparams) + (local_alloc : funname -> stk_alloc_oracle_t) + (fresh_reg_ : string -> stype -> Ident.ident) + (warning : instr_info -> warning_msg -> instr_info). -Variable (local_alloc : funname -> stk_alloc_oracle_t). -Variable (fresh_reg_ : string → stype → Ident.ident). Hypothesis Halloc_fd : forall fn fd, get_fundef P.(p_funcs) fn = Some fd -> - exists2 fd', alloc_fd shparams saparams P'.(p_extra) mglob fresh_reg_ local_alloc fn fd = ok fd' & - get_fundef P'.(p_funcs) fn = Some fd'. + exists2 fd', + alloc_fd shparams saparams P'.(p_extra) mglob fresh_reg_ local_alloc warning fn fd = ok fd' & get_fundef P'.(p_funcs) fn = Some fd'. (* RAnone -> export function (TODO: rename RAexport?) *) Definition enough_size m sao := @@ -1863,7 +1864,7 @@ Let Pi_r s1 (i1:instr_r) s2 := wf_pmap pmap rsp rip Slots Addr Writable Align -> wf_Slots Slots Addr Writable Align -> forall sao, - alloc_i shparams saparams pmap local_alloc sao rmap1 (MkI ii1 i1) = ok (rmap2, c2) -> + alloc_i shparams saparams pmap local_alloc warning sao rmap1 (MkI ii1 i1) = ok (rmap2, c2) -> forall m0 s1', valid_state pmap glob_size rsp rip Slots Addr Writable Align P rmap1 m0 s1 s1' -> extend_mem (emem s1) (emem s1') rip global_data -> wf_sao rsp (emem s1') sao -> @@ -1875,7 +1876,7 @@ Let Pi s1 (i1:instr) s2 := wf_pmap pmap rsp rip Slots Addr Writable Align -> wf_Slots Slots Addr Writable Align -> forall sao, - alloc_i shparams saparams pmap local_alloc sao rmap1 i1 = ok (rmap2, c2) -> + alloc_i shparams saparams pmap local_alloc warning sao rmap1 i1 = ok (rmap2, c2) -> forall m0 s1', valid_state pmap glob_size rsp rip Slots Addr Writable Align P rmap1 m0 s1 s1' -> extend_mem (emem s1) (emem s1') rip global_data -> wf_sao rsp (emem s1') sao -> @@ -1887,7 +1888,7 @@ Let Pc s1 (c1:cmd) s2 := wf_pmap pmap rsp rip Slots Addr Writable Align -> wf_Slots Slots Addr Writable Align -> forall sao, - fmapM (alloc_i shparams saparams pmap local_alloc sao) rmap1 c1 = ok (rmap2, c2) -> + fmapM (alloc_i shparams saparams pmap local_alloc warning sao) rmap1 c1 = ok (rmap2, c2) -> forall m0 s1', valid_state pmap glob_size rsp rip Slots Addr Writable Align P rmap1 m0 s1 s1' -> extend_mem (emem s1) (emem s1') rip global_data -> wf_sao rsp (emem s1') sao -> @@ -2012,10 +2013,15 @@ Proof. + subst o => -[rmap_ i] halloc /= ? <- m0 s1' hvs ??; subst rmap_. have [s2' [hsem ?]] := (alloc_array_swapP hpmap P' hsaparams hvs hes hop hw halloc). by exists s2'; split => //; apply sem_seq_ir. - move => es' he [rmap4 x'] ha /= ? <- m0 s1' hvs hext hsao; subst rmap4. + move=> es' he [rmap4 x'] ha /=. + rewrite (surjective_pairing (sap_mem_opn _ _ _ _ _)) /= => -[??] m0 s1' hvs + hext hsao; + subst rmap4 c2. have [s2' [hw' hvalid']] := alloc_lvalsP hwf.(wfsl_no_overflow) hwf.(wfsl_disjoint) hwf.(wfsl_align) hpmap ha hvs (sopn_toutP hop) hw. exists s2'; split=> //. - apply sem_seq_ir; constructor. + apply sem_seq_ir. + apply: (sap_mem_opnP hsaparams). + constructor. rewrite /sem_sopn P'_globs. have [va' [ok_va' hop']] := exec_sopn_truncate_val hop. have [vs3 [ok_vs3 htr']] := alloc_esP hwf.(wfsl_no_overflow) hwf.(wfsl_align) hpmap hvs he hes ok_va'. @@ -2132,7 +2138,7 @@ Proof. Qed. Lemma alloc_fd_max_size_ge0 pex fn fd fd' : - alloc_fd shparams saparams pex mglob fresh_reg_ local_alloc fn fd = ok fd' -> + alloc_fd shparams saparams pex mglob fresh_reg_ local_alloc warning fn fd = ok fd' -> 0 <= (local_alloc fn).(sao_max_size). Proof. rewrite /alloc_fd /alloc_fd_aux /=. @@ -2920,13 +2926,14 @@ Context (hshparams : slh_lowering_proof.h_sh_params shparams) (saparams : stack_alloc_params) (hsaparams : h_stack_alloc_params saparams) - (fresh_reg_ : string -> stype -> Ident.ident). + (fresh_reg_ : string -> stype -> Ident.ident) + (warning : instr_info -> warning_msg -> instr_info). Lemma get_alloc_fd p_extra mglob oracle fds1 fds2 : - map_cfprog_name (alloc_fd shparams saparams p_extra mglob fresh_reg_ oracle) fds1 = ok fds2 -> + map_cfprog_name (alloc_fd shparams saparams p_extra mglob fresh_reg_ oracle warning) fds1 = ok fds2 -> forall fn fd1, get_fundef fds1 fn = Some fd1 -> - exists2 fd2, alloc_fd shparams saparams p_extra mglob fresh_reg_ oracle fn fd1 = ok fd2 & + exists2 fd2, alloc_fd shparams saparams p_extra mglob fresh_reg_ oracle warning fn fd1 = ok fd2 & get_fundef fds2 fn = Some fd2. Proof. move=> hmap fn fd1. @@ -2962,7 +2969,7 @@ Qed. except for the regions pointed to by the writable [reg ptr]s given as arguments. *) Theorem alloc_progP nrip nrsp data oracle_g oracle (P: uprog) (SP: sprog) fn: - alloc_prog shparams saparams fresh_reg_ nrip nrsp data oracle_g oracle P = ok SP -> + alloc_prog shparams saparams fresh_reg_ nrip nrsp data oracle_g oracle warning P = ok SP -> forall ev scs1 m1 vargs1 scs1' m1' vres1, sem_call P ev scs1 m1 fn vargs1 scs1' m1' vres1 -> forall rip m2 vargs2, @@ -3008,13 +3015,13 @@ Proof. Qed. Lemma alloc_prog_get_fundef nrip nrsp data oracle_g oracle (P: uprog) (SP: sprog) : - alloc_prog shparams saparams fresh_reg_ nrip nrsp data oracle_g oracle P = ok SP → + alloc_prog shparams saparams fresh_reg_ nrip nrsp data oracle_g oracle warning P = ok SP → exists2 mglob, init_map oracle_g data (p_globs P) = ok mglob & ∀ fn fd, get_fundef (p_funcs P) fn = Some fd → exists2 fd', - alloc_fd shparams saparams {| sp_rsp := nrsp ; sp_rip := nrip ; sp_globs := data ; sp_glob_names := oracle_g |} mglob fresh_reg_ oracle fn fd = ok fd' & + alloc_fd shparams saparams {| sp_rsp := nrsp ; sp_rip := nrip ; sp_globs := data ; sp_glob_names := oracle_g |} mglob fresh_reg_ oracle warning fn fd = ok fd' & get_fundef (p_funcs SP) fn = Some fd'. Proof. rewrite /alloc_prog; t_xrbindP => mglob -> _ fds ok_fds <- {SP} /=. @@ -3023,7 +3030,7 @@ Proof. Qed. Lemma alloc_fd_checked_sao p_extra mglob oracle fn fd fd' : - alloc_fd shparams saparams p_extra mglob fresh_reg_ oracle fn fd = ok fd' → + alloc_fd shparams saparams p_extra mglob fresh_reg_ oracle warning fn fd = ok fd' → [/\ size (sao_params (oracle fn)) = size (f_params fd) & size (sao_return (oracle fn)) = size (f_res fd) ]. Proof. rewrite /alloc_fd/alloc_fd_aux/check_results. diff --git a/proofs/compiler/x86_params.v b/proofs/compiler/x86_params.v index 5ba60494f..ffb0c9439 100644 --- a/proofs/compiler/x86_params.v +++ b/proofs/compiler/x86_params.v @@ -67,6 +67,7 @@ Definition x86_saparams : stack_alloc_params := sap_mov_ofs := x86_mov_ofs; sap_immediate := x86_immediate; sap_swap := x86_swap; + sap_mem_opn := fun lvs tag op es => (Copn lvs tag op es, false); |}. (* ------------------------------------------------------------------------ *) diff --git a/proofs/compiler/x86_params_proof.v b/proofs/compiler/x86_params_proof.v index 2f8ca6048..6cf31bcac 100644 --- a/proofs/compiler/x86_params_proof.v +++ b/proofs/compiler/x86_params_proof.v @@ -123,6 +123,9 @@ Proof. rewrite hxty hyty //=. Qed. +Lemma x86_mem_opnP : sap_mem_opn_correct (sap_mem_opn x86_saparams). +Proof. done. Qed. + End STACK_ALLOC. Definition x86_hsaparams : h_stack_alloc_params (ap_sap x86_params) := @@ -130,6 +133,7 @@ Definition x86_hsaparams : h_stack_alloc_params (ap_sap x86_params) := mov_ofsP := x86_mov_ofsP; sap_immediateP := x86_immediateP; sap_swapP := x86_swapP; + sap_mem_opnP := x86_mem_opnP; |}. (* ------------------------------------------------------------------------ *) diff --git a/proofs/lang/fexpr.v b/proofs/lang/fexpr.v index c335e5071..c4b6cbe5b 100644 --- a/proofs/lang/fexpr.v +++ b/proofs/lang/fexpr.v @@ -1,4 +1,5 @@ -From mathcomp Require Import ssreflect ssrfun ssrbool. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg. +From mathcomp Require Import word_ssrZ. From Coq Require Import Utf8. Require Import expr. @@ -18,6 +19,20 @@ Inductive fexpr := Definition fconst (ws: wsize) (z: Z) : fexpr := Fapp1 (Oword_of_int ws) (Fconst z). +Definition is_fconst (e : fexpr) : option Z := + if e is Fconst z then Some z else None. + +Definition is_fwconst (ws : wsize) (e : fexpr) : option (word ws) := + match e with + | Fapp1 (Oword_of_int ws') e => + if (ws <= ws')%CMP + then + let%opt n := is_fconst e in + Some (wrepr ws n) + else None + | _ => None + end. + (* --------------------------------------------------------------------------- *) (* Right-expressions *) Variant rexpr := @@ -81,6 +96,21 @@ Definition free_vars_r (r:rexpr) : Sv.t := | Rexpr e => free_vars e end. +Definition free_vars_rs : seq rexpr -> Sv.t := + foldr (fun e acc => Sv.union (free_vars_r e) acc) Sv.empty. + Definition rvar (x : var_i) : rexpr := Rexpr (Fvar x). Definition rconst (ws : wsize) (z : Z) : rexpr := Rexpr (fconst ws z). Definition lstore {_ : PointerData} al ws x z := Store al ws x (fconst Uptr z). + +Fixpoint eq_fexpr (e0 e1 : fexpr) : bool := + match e0, e1 with + | Fconst n0, Fconst n1 => n0 == n1 + | Fvar x0, Fvar x1 => v_var x0 == v_var x1 + | Fapp1 op0 e0, Fapp1 op1 e1 => [&& op0 == op1 & eq_fexpr e0 e1 ] + | Fapp2 op0 e00 e01, Fapp2 op1 e10 e11 => + [&& op0 == op1, eq_fexpr e00 e10 & eq_fexpr e01 e11 ] + | Fif e00 e01 e02, Fif e10 e11 e12 => + [&& eq_fexpr e00 e10, eq_fexpr e01 e11 & eq_fexpr e02 e12 ] + | _, _ => false + end. diff --git a/proofs/lang/fexpr_facts.v b/proofs/lang/fexpr_facts.v index 09ea9bd85..5f8ddf8ed 100644 --- a/proofs/lang/fexpr_facts.v +++ b/proofs/lang/fexpr_facts.v @@ -1,6 +1,6 @@ From Coq Require Import Utf8. Require Import oseq. -From mathcomp Require Import ssreflect ssrfun ssrbool. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype. Require Import fexpr fexpr_sem. Require Import expr psem. @@ -46,6 +46,20 @@ Context (wdb : bool) (gd : glob_decls). +Lemma is_fconstP e z : + is_fconst e = Some z <-> e = Fconst z. +Proof. case: e => *; by split=> // -[->]. Qed. + +Lemma is_fwconstP vm sz e w : + is_fwconst sz e = Some w -> + Let x := sem_fexpr vm e in to_word sz x = ok w. +Proof. + case: e => // -[] //= ws e. + case: ifP => // hws. + apply: obindP => z /is_fconstP ? [?]; subst e w. + by rewrite /= truncate_word_le // zero_extend_wrepr. +Qed. + Lemma fexpr_of_pexprP s e f v : fexpr_of_pexpr e = Some f → sem_pexpr true gd s e = ok v → @@ -124,6 +138,27 @@ Proof. rewrite (free_vars_recP heq) (get_var_eq_on _ _ heq) // free_varsE; SvD.fsetdec. Qed. +Lemma sem_fexpr_eq_ex vm1 vm2 e xs : + disjoint xs (free_vars e) -> + vm1 =[\ xs ] vm2 -> + sem_fexpr vm1 e = sem_fexpr vm2 e. +Proof. move=> /eq_ex_disjoint_eq_on /[apply]. exact: free_varsP. Qed. + +Lemma sem_rexpr_eq_ex vm1 vm2 m e xs : + disjoint xs (free_vars_r e) -> + vm1 =[\ xs ] vm2 -> + sem_rexpr m vm1 e = sem_rexpr m vm2 e. +Proof. move=> /eq_ex_disjoint_eq_on /[apply]. exact: free_vars_rP. Qed. + +Lemma sem_rexprs_eq_ex s vm es xs : + disjoint xs (free_vars_rs es) -> + vm =[\ xs ] evm s -> + sem_rexprs (with_vm s vm) es = sem_rexprs s es. +Proof. + elim: es => [// | e es hind] /= => + /disjoint_sym /disjoint_union [/disjoint_sym he /disjoint_sym hes] hvm. + by rewrite (sem_rexpr_eq_ex _ he hvm) (hind hes hvm). +Qed. Lemma write_lexpr_stack_stable e v s1 s2 : write_lexpr e v s1 = ok s2 -> @@ -166,4 +201,31 @@ Proof. by move=> ???; rewrite hvalid1 hvalid2. Qed. +Lemma eq_fexpr_sem_fexpr e0 e1 vm : + eq_fexpr e0 e1 -> + sem_fexpr vm e0 = sem_fexpr vm e1. +Proof. + elim: e0 e1 => + [z0 | x0 | op e0 h | op e00 h0 e01 h1 | e00 h0 e01 h1 e02 h2] //= [^e1] //=. + - by move=> /eqP ->. + - by move=> /eqP ->. + - by move=> /andP [] /eqP -> /h ->. + - by move=> /and3P [] /eqP -> /h0 -> /h1 ->. + by move=> /and3P [] /h0 -> /h1 -> /h2 ->. +Qed. + +Lemma eq_fexpr_free_vars e0 e1 : + eq_fexpr e0 e1 -> + Sv.Equal (free_vars e0) (free_vars e1). +Proof. + rewrite /free_vars. + elim: e0 e1 => + [z0 | x0 | ? e0 h | ? e00 h0 e01 h1 | e00 h0 e01 h1 e02 h2] //= + [z1 | x1 | ? e1 | ? e10 e11 | e10 e11 e12] //=. + - by move=> /eqP ->. + - by move=> /andP [] _ /h ->. + - by rewrite !free_varsE /free_vars => /and3P [] _ /h0 -> /h1 ->. + by rewrite !free_varsE /free_vars => /and3P [] /h0 -> /h1 -> /h2 ->. +Qed. + End Section. diff --git a/proofs/lang/utils.v b/proofs/lang/utils.v index cb47c36b3..287c4aa9a 100644 --- a/proofs/lang/utils.v +++ b/proofs/lang/utils.v @@ -559,6 +559,8 @@ Section FOLD2. End FOLD2. +Arguments size_fold2 {_ _ _ _ _ _ _ _ _ _}. + (* ---------------------------------------------------------------- *) (* ALLM *) Section ALLM. From 4011b7eee0b4e0e9d7be2c43d06d74bf9e221841 Mon Sep 17 00:00:00 2001 From: Santiago Arranz Olmos Date: Mon, 7 Oct 2024 22:48:15 +0100 Subject: [PATCH 2/2] Add flag to supress warnings for splitting memory accesses --- compiler/src/compile.ml | 13 ++++++++----- compiler/src/glob_options.ml | 4 ++++ 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/compiler/src/compile.ml b/compiler/src/compile.ml index 264d7062b..2bd3fa965 100644 --- a/compiler/src/compile.ml +++ b/compiler/src/compile.ml @@ -191,11 +191,14 @@ let compile (type reg regx xreg rflag cond asm_op extra_op) then Some (UseLea, "LEA instruction is used") else None | Split_memory_access -> - let msg = - "This memory immediate does not fit in one instruction, several \ - instructions were issued." - in - Some (SplitMemoryAccess, msg) + if not !Glob_options.split_memory_access + then + let msg = + "This memory immediate does not fit in one instruction, several \ + instructions were issued." + in + Some (SplitMemoryAccess, msg) + else None in let loc, _ = ii in Option.may (fun (w, msg) -> warning w loc "%s" msg) o; diff --git a/compiler/src/glob_options.ml b/compiler/src/glob_options.ml index af4288582..d9a691dca 100644 --- a/compiler/src/glob_options.ml +++ b/compiler/src/glob_options.ml @@ -25,6 +25,7 @@ type color = | Auto | Always | Never let color = ref Auto let lea = ref false +let split_memory_access = ref false let set0 = ref false let model = ref Normal let print_stack_alloc = ref false @@ -172,6 +173,9 @@ let options = [ "-I" , Arg.String set_idirs , "[ident:path] Bind ident to path for from ident require ..."; "-lea" , Arg.Set lea , " Use lea as much as possible (default is nolea)"; "-nolea" , Arg.Clear lea , " Try to use add and mul instead of lea"; + "-split-memory-access" + , Arg.Set split_memory_access + , " Split large memory accesses in several instructions"; "-set0" , Arg.Set set0 , " Use [xor x x] to set x to 0 (default is not)"; "-noset0" , Arg.Clear set0 , " Do not use set0 option"; "-ec" , Arg.String set_ec , "[f] Extract function [f] and its dependencies to an easycrypt file (deprecated)";