diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-10 11:58:27 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-10 11:58:27 +0100 |
| commit | c657ba1f5e841224c745bbaf40dd8f6558e22365 (patch) | |
| tree | a8a534b3bdee05c137183d96251359567272add3 | |
| parent | 34fe97ee74793af82d3f2421a6e75b44ad955199 (diff) | |
| download | compcert-kvx-c657ba1f5e841224c745bbaf40dd8f6558e22365.tar.gz compcert-kvx-c657ba1f5e841224c745bbaf40dd8f6558e22365.zip | |
Update Verilog back end
31 files changed, 1092 insertions, 3411 deletions
diff --git a/verilog/Archi.v b/verilog/Archi.v index 8f1ccdef..dc5a078d 100644 --- a/verilog/Archi.v +++ b/verilog/Archi.v @@ -7,10 +7,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -56,8 +57,13 @@ Definition fma_invalid_mul_is_nan := false. Definition float_of_single_preserves_sNaN := false. +(** Which ABI to use. *) +Parameter win64: bool. (* Always false in 32 bits *) + Global Opaque ptr64 big_endian splitlong default_nan_64 choose_nan_64 default_nan_32 choose_nan_32 fma_order fma_invalid_mul_is_nan float_of_single_preserves_sNaN. + +Definition has_notrap_loads := false. diff --git a/verilog/Asm.v b/verilog/Asm.v index 64ae1c32..799b533e 100644 --- a/verilog/Asm.v +++ b/verilog/Asm.v @@ -279,6 +279,7 @@ Inductive instruction: Type := | Pmaxsd (rd: freg) (r2: freg) | Pminsd (rd: freg) (r2: freg) | Pmovb_rm (rd: ireg) (a: addrmode) + | Pmovq_rf (rd: ireg) (r1: freg) | Pmovsq_mr (a: addrmode) (rs: freg) | Pmovsq_rm (rd: freg) (a: addrmode) | Pmovsb @@ -998,6 +999,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmaxsd _ _ | Pminsd _ _ | Pmovb_rm _ _ + | Pmovq_rf _ _ | Pmovsq_rm _ _ | Pmovsq_mr _ _ | Pmovsb diff --git a/verilog/Asmexpand.ml b/verilog/Asmexpand.ml index 1b3961e0..e2c556c7 100644 --- a/verilog/Asmexpand.ml +++ b/verilog/Asmexpand.ml @@ -39,6 +39,11 @@ let _16z = Z.of_sint 16 let stack_alignment () = 16 +(* Pseudo instructions for 32/64 bit compatibility *) + +let _Plea (r, addr) = + if Archi.ptr64 then Pleaq (r, addr) else Pleal (r, addr) + (* SP adjustment to allocate or free a stack frame. *) let align n a = @@ -104,21 +109,6 @@ let offset_addressing (Addrmode(base, ofs, cst)) delta = let linear_addr reg ofs = Addrmode(Some reg, None, Coq_inl ofs) let global_addr id ofs = Addrmode(None, None, Coq_inr(id, ofs)) -(* A "leaq" instruction that does not overflow *) - -let emit_leaq r addr = - match Asmgen.normalize_addrmode_64 addr with - | (addr, None) -> - emit (Pleaq (r, addr)) - | (addr, Some delta) -> - emit (Pleaq (r, addr)); - emit (Paddq_ri (r, delta)) - -(* Pseudo "lea" instruction for 32/64 bit compatibility *) - -let emit_lea r addr = - if Archi.ptr64 then emit_leaq r addr else emit (Pleal (r, addr)) - (* Translate a builtin argument into an addressing mode *) let addressing_of_builtin_arg = function @@ -160,8 +150,8 @@ let expand_builtin_memcpy_small sz al src dst = copy (addressing_of_builtin_arg src) (addressing_of_builtin_arg dst) sz let expand_builtin_memcpy_big sz al src dst = - if src <> BA (IR RSI) then emit_lea RSI (addressing_of_builtin_arg src); - if dst <> BA (IR RDI) then emit_lea RDI (addressing_of_builtin_arg dst); + if src <> BA (IR RSI) then emit (_Plea (RSI, addressing_of_builtin_arg src)); + if dst <> BA (IR RDI) then emit (_Plea (RDI, addressing_of_builtin_arg dst)); (* TODO: movsq? *) emit (Pmovl_ri (RCX,coqint_of_camlint (Int32.of_int (sz / 4)))); emit Prep_movsl; @@ -299,9 +289,9 @@ let expand_builtin_va_start_elf64 r = emit (Pmovl_mr (linear_addr r _0z, RAX)); emit (Pmovl_ri (RAX, coqint_of_camlint fp_offset)); emit (Pmovl_mr (linear_addr r _4z, RAX)); - emit_leaq RAX (linear_addr RSP (Z.of_uint64 overflow_arg_area)); + emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 overflow_arg_area))); emit (Pmovq_mr (linear_addr r _8z, RAX)); - emit_leaq RAX (linear_addr RSP (Z.of_uint64 reg_save_area)); + emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 reg_save_area))); emit (Pmovq_mr (linear_addr r _16z, RAX)) let expand_builtin_va_start_win64 r = @@ -312,7 +302,7 @@ let expand_builtin_va_start_win64 r = let ofs = Int64.(add !current_function_stacksize (mul 8L (of_int num_args))) in - emit_leaq RAX (linear_addr RSP (Z.of_uint64 ofs)); + emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 ofs))); emit (Pmovq_mr (linear_addr r _0z, RAX)) (* FMA operations *) @@ -491,7 +481,8 @@ let expand_builtin_inline name args res = (* Vararg stuff *) | "__builtin_va_start", [BA(IR a)], _ -> assert (a = RDX); - if Archi.ptr64 then expand_builtin_va_start_elf64 a + if Archi.win64 then expand_builtin_va_start_win64 a + else if Archi.ptr64 then expand_builtin_va_start_elf64 a else expand_builtin_va_start_32 a (* Synchronization *) | "__builtin_membar", [], _ -> @@ -522,7 +513,14 @@ let fixup_funcall_elf64 sg = registers. *) -let copy_fregs_to_iregs args fr ir = +let rec copy_fregs_to_iregs args fr ir = + match (ir, fr, args) with + | (i1 :: ir, f1 :: fr, (Tfloat | Tsingle) :: args) -> + emit (Pmovq_rf (i1, f1)); + copy_fregs_to_iregs args fr ir + | (i1 :: ir, f1 :: fr, _ :: args) -> + copy_fregs_to_iregs args fr ir + | _ -> () let fixup_funcall_win64 sg = @@ -530,8 +528,10 @@ let fixup_funcall_win64 sg = copy_fregs_to_iregs sg.sig_args [XMM0; XMM1; XMM2; XMM3] [RCX; RDX; R8; R9] let fixup_funcall sg = - if Archi.ptr64 then - fixup_funcall_elf64 sg + if Archi.ptr64 + then if Archi.win64 + then fixup_funcall_win64 sg + else fixup_funcall_elf64 sg else () (* Expansion of instructions *) @@ -539,7 +539,23 @@ let fixup_funcall sg = let expand_instruction instr = match instr with | Pallocframe (sz, ofs_ra, ofs_link) -> - if Archi.ptr64 then begin + if Archi.win64 then begin + let sz = sp_adjustment_win64 sz in + if is_current_function_variadic() then + (* Save parameters passed in registers in reserved stack area *) + emit (Pcall_s (intern_string "__compcert_va_saveregs", + {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})); + (* Allocate frame *) + let sz' = Z.of_uint sz in + emit (Psubl_ri (RSP, sz')); + emit (Pcfi_adjust sz'); + (* Stack chaining *) + let addr1 = linear_addr RSP (Z.of_uint (sz + 8)) in + let addr2 = linear_addr RSP ofs_link in + emit (Pleaq (RAX,addr1)); + emit (Pmovq_mr (addr2, RAX)); + current_function_stacksize := Int64.of_int (sz + 8) + end else if Archi.ptr64 then begin let (sz, save_regs) = sp_adjustment_elf64 sz in (* Allocate frame *) let sz' = Z.of_uint sz in @@ -547,7 +563,7 @@ let expand_instruction instr = emit (Pcfi_adjust sz'); if save_regs >= 0 then begin (* Save the registers *) - emit_leaq R10 (linear_addr RSP (Z.of_uint save_regs)); + emit (Pleaq (R10, linear_addr RSP (Z.of_uint save_regs))); emit (Pcall_s (intern_string "__compcert_va_saveregs", {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})) end; @@ -555,7 +571,7 @@ let expand_instruction instr = let fullsz = sz + 8 in let addr1 = linear_addr RSP (Z.of_uint fullsz) in let addr2 = linear_addr RSP ofs_link in - emit_leaq RAX addr1; + emit (Pleaq (RAX, addr1)); emit (Pmovq_mr (addr2, RAX)); current_function_stacksize := Int64.of_int fullsz end else begin @@ -572,7 +588,10 @@ let expand_instruction instr = PrintAsmaux.current_function_stacksize := Int32.of_int sz end | Pfreeframe(sz, ofs_ra, ofs_link) -> - if Archi.ptr64 then begin + if Archi.win64 then begin + let sz = sp_adjustment_win64 sz in + emit (Paddq_ri (RSP, Z.of_uint sz)) + end else if Archi.ptr64 then begin let (sz, _) = sp_adjustment_elf64 sz in emit (Paddq_ri (RSP, Z.of_uint sz)) end else begin @@ -595,7 +614,7 @@ let expand_instruction instr = expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args | EF_annot_val(kind,txt, targ) -> expand_annot_val kind txt targ args res - | EF_annot _ | EF_debug _ | EF_inline_asm _ -> + | EF_annot _ | EF_debug _ | EF_inline_asm _ | EF_profiling _ -> emit instr | _ -> assert false diff --git a/verilog/Asmgen.v b/verilog/Asmgen.v index 73e3263e..99e9fc2b 100644 --- a/verilog/Asmgen.v +++ b/verilog/Asmgen.v @@ -636,9 +636,14 @@ Definition transl_op (** Translation of memory loads and stores *) -Definition transl_load (chunk: memory_chunk) +Definition transl_load + (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dest: mreg) (k: code) : res code := + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load x86 does not support non trapping loads") + | TRAP => do am <- transl_addressing addr args; match chunk with | Mint8unsigned => @@ -659,6 +664,7 @@ Definition transl_load (chunk: memory_chunk) do r <- freg_of dest; OK(Pmovsd_fm r am :: k) | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) @@ -699,8 +705,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) loadind RSP f.(fn_link_ofs) Tptr AX k1) | Mop op args res => transl_op op args res k - | Mload chunk addr args dst => - transl_load chunk addr args dst k + | Mload trap chunk addr args dst => + transl_load trap chunk addr args dst k | Mstore chunk addr args src => transl_store chunk addr args src k | Mcall sig (inl reg) => diff --git a/verilog/Asmgenproof.v b/verilog/Asmgenproof.v index 67c42b2b..8c28fb1b 100644 --- a/verilog/Asmgenproof.v +++ b/verilog/Asmgenproof.v @@ -235,11 +235,11 @@ Proof. Qed. Remark transl_load_label: - forall chunk addr args dest k c, - transl_load chunk addr args dest k = OK c -> + forall trap chunk addr args dest k c, + transl_load trap chunk addr args dest k = OK c -> tail_nolabel k c. Proof. - intros. monadInv H. destruct chunk; TailNoLabel. + intros. destruct trap; try discriminate. monadInv H. destruct chunk; TailNoLabel. Qed. Remark transl_store_label: @@ -567,6 +567,12 @@ Opaque loadind. split. eapply agree_set_undef_mreg; eauto. congruence. simpl; congruence. +- (* Mload notrap *) (* isn't there a nicer way? *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + +- (* Mload notrap *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + - (* Mstore *) assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. diff --git a/verilog/Asmgenproof1.v b/verilog/Asmgenproof1.v index fd88954e..7cff1047 100644 --- a/verilog/Asmgenproof1.v +++ b/verilog/Asmgenproof1.v @@ -1464,8 +1464,8 @@ Qed. (** Translation of memory loads. *) Lemma transl_load_correct: - forall chunk addr args dest k c (rs: regset) m a v, - transl_load chunk addr args dest k = OK c -> + forall trap chunk addr args dest k c (rs: regset) m a v, + transl_load trap chunk addr args dest k = OK c -> eval_addressing ge (rs#RSP) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> exists rs', @@ -1473,7 +1473,9 @@ Lemma transl_load_correct: /\ rs'#(preg_of dest) = v /\ forall r, data_preg r = true -> r <> preg_of dest -> rs'#r = rs#r. Proof. - unfold transl_load; intros. monadInv H. + unfold transl_load; intros. + destruct trap; simpl; try discriminate. + monadInv H. exploit transl_addressing_mode_correct; eauto. intro EA. assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto. set (rs2 := nextinstr_nf (rs#(preg_of dest) <- v)). diff --git a/verilog/Builtins1.v b/verilog/Builtins1.v index f1d60961..e5233ff5 100644 --- a/verilog/Builtins1.v +++ b/verilog/Builtins1.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/verilog/CBuiltins.ml b/verilog/CBuiltins.ml index 6820c089..a549cd25 100644 --- a/verilog/CBuiltins.ml +++ b/verilog/CBuiltins.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -19,8 +20,12 @@ open C let (va_list_type, va_list_scalar, size_va_list) = if Archi.ptr64 then - (* Actually a struct passed by reference; equivalent to 3 64-bit words *) - (TArray(TInt(IULong, []), Some 3L, []), false, 3*8) + if Archi.win64 then + (* Just a pointer *) + (TPtr(TVoid [], []), true, 8) + else + (* Actually a struct passed by reference; equivalent to 3 64-bit words *) + (TArray(TInt(IULong, []), Some 3L, []), false, 3*8) else (* Just a pointer *) (TPtr(TVoid [], []), true, 4) diff --git a/verilog/CSE2deps.v b/verilog/CSE2deps.v new file mode 100644 index 00000000..757966b8 --- /dev/null +++ b/verilog/CSE2deps.v @@ -0,0 +1,38 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import BoolEqual Coqlib. +Require Import AST Integers Floats. +Require Import Values Memory Globalenvs Events. +Require Import Op. + +Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw := + (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk)) + && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk)) + && ((ofsw + size_chunk chunkw <=? ofsr) || + (ofsr + size_chunk chunkr <=? ofsw)). + +Definition may_overlap chunk addr args chunk' addr' args' := + match addr, addr', args, args' with + | (Aindexed ofs), (Aindexed ofs'), + (base :: nil), (base' :: nil) => + if peq base base' + then negb (can_swap_accesses_ofs ofs' chunk' ofs chunk) + else true + | (Aglobal symb ofs), (Aglobal symb' ofs'), nil, nil => + if peq symb symb' + then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + else false + | (Ainstack ofs), (Ainstack ofs'), _, _ => + negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + | _, _, _, _ => true + end. diff --git a/verilog/CSE2depsproof.v b/verilog/CSE2depsproof.v new file mode 100644 index 00000000..e181b8f4 --- /dev/null +++ b/verilog/CSE2depsproof.v @@ -0,0 +1,339 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE2 CSE2deps. +Require Import Lia. + +Lemma ptrofs_modulus : + Ptrofs.modulus = if Archi.ptr64 + then 18446744073709551616 + else 4294967296. +Proof. + reflexivity. +Qed. + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Section STACK_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + + Variable addrw addrr valw : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + + Section INDEXED_AWAY. + Variable ofsw ofsr : ptrofs. + Hypothesis ADDRW : eval_addressing genv sp + (Ainstack ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Ainstack ofsr) nil = Some addrr. + + Lemma stack_load_store_away1 : + forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr + \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + unfold largest_size_chunk in *. + + inv ADDRR. + inv ADDRW. + + destruct sp; try discriminate. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW]; + rewrite OFSW). + all: try rewrite ptrofs_modulus in *. + all: destruct Archi.ptr64. + + all: intuition lia. + Qed. + + Theorem stack_load_store_away : + can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply stack_load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End STACK_WRITE. + +Section MEMORY_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + Variable base : val. + + Variable addrw addrr valw : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + + Section INDEXED_AWAY. + Variable ofsw ofsr : Z. + Hypothesis ADDRW : eval_addressing genv sp + (Aindexed ofsw) (base :: nil) = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aindexed ofsr) (base :: nil) = Some addrr. + + Lemma load_store_away1 : + forall RANGEW : 0 <= ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : ofsw + size_chunk chunkw <= ofsr + \/ ofsr + size_chunk chunkr <= ofsw, + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *. + try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *. + destruct addrr ; simpl in * ; trivial. + unfold eval_addressing, eval_addressing32, eval_addressing64 in *. + destruct Archi.ptr64 eqn:PTR64; destruct base; simpl in *; try discriminate. + rewrite PTR64 in *. + + inv ADDRR. + inv ADDRW. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int (Int.repr ofsr))) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int64 (Int64.repr ofsr))) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int (Int.repr ofsw))) as [OFSW | OFSW]; + rewrite OFSW). + all: try (destruct (Ptrofs.unsigned_add_either i0 + (Ptrofs.of_int64 (Int64.repr ofsw))) as [OFSW | OFSW]; + rewrite OFSW). + + all: unfold Ptrofs.of_int64. + all: unfold Ptrofs.of_int. + + + all: repeat rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia). + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 4294967295; lia). + all: repeat rewrite Int64.unsigned_repr by (change Int64.max_unsigned with 18446744073709551615; lia). + all: repeat rewrite Ptrofs.unsigned_repr by (change Ptrofs.max_unsigned with 18446744073709551615; lia). + + all: try change Ptrofs.modulus with 4294967296. + all: try change Ptrofs.modulus with 18446744073709551616. + + all: intuition lia. + Qed. + + Theorem load_store_away : + can_swap_accesses_ofs ofsr chunkr ofsw chunkw = true -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. + + Section DIFFERENT_GLOBALS. + Variable ofsw ofsr : ptrofs. + Hypothesis symw symr : ident. + Hypothesis ADDRW : eval_addressing genv sp + (Aglobal symw ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aglobal symr ofsr) nil = Some addrr. + + Lemma ptr64_cases: + forall {T : Type}, + forall b : bool, + forall x y : T, + (if b then (if b then x else y) else (if b then y else x)) = x. + Proof. + destruct b; reflexivity. + Qed. + + (* not needed + Lemma bool_cases_same: + forall {T : Type}, + forall b : bool, + forall x : T, + (if b then x else x) = x. + Proof. + destruct b; reflexivity. + Qed. + *) + + Lemma load_store_diff_globals : + symw <> symr -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intros. + unfold eval_addressing in *. + simpl in *. + rewrite ptr64_cases in ADDRR. + rewrite ptr64_cases in ADDRW. + unfold Genv.symbol_address in *. + unfold Genv.find_symbol in *. + destruct ((Genv.genv_symb genv) ! symw) as [bw |] eqn:SYMW; inv ADDRW. + 2: simpl in STORE; discriminate. + destruct ((Genv.genv_symb genv) ! symr) as [br |] eqn:SYMR; inv ADDRR. + 2: reflexivity. + assert (br <> bw). + { + intro EQ. + subst br. + assert (symr = symw). + { + eapply Genv.genv_vars_inj; eauto. + } + congruence. + } + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := bw). + - exact STORE. + - left. assumption. + Qed. + End DIFFERENT_GLOBALS. + + Section SAME_GLOBALS. + Variable ofsw ofsr : ptrofs. + Hypothesis sym : ident. + Hypothesis ADDRW : eval_addressing genv sp + (Aglobal sym ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aglobal sym ofsr) nil = Some addrr. + + Lemma load_store_glob_away1 : + forall RANGEW : 0 <= (Ptrofs.unsigned ofsw) <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= (Ptrofs.unsigned ofsr) <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : (Ptrofs.unsigned ofsw) + size_chunk chunkw <= (Ptrofs.unsigned ofsr) + \/ (Ptrofs.unsigned ofsr) + size_chunk chunkr <= (Ptrofs.unsigned ofsw), + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + unfold largest_size_chunk in size_chunkr_bounded, size_chunkw_bounded. + try change (Ptrofs.modulus - largest_size_chunk) with 4294967288 in *. + try change (Ptrofs.modulus - largest_size_chunk) with 18446744073709551608 in *. + unfold eval_addressing, eval_addressing32, eval_addressing64 in *. + + rewrite ptr64_cases in ADDRR. + rewrite ptr64_cases in ADDRW. + unfold Genv.symbol_address in *. + inv ADDRR. + inv ADDRW. + destruct (Genv.find_symbol genv sym). + 2: discriminate. + + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + tauto. + Qed. + + Lemma load_store_glob_away : + (can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw) = true -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply load_store_glob_away1. + all: tauto. + Qed. + End SAME_GLOBALS. +End MEMORY_WRITE. +End SOUNDNESS. + + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Lemma may_overlap_sound: + forall m m' : mem, + forall chunk addr args chunk' addr' args' v a a' rs, + (eval_addressing genv sp addr (rs ## args)) = Some a -> + (eval_addressing genv sp addr' (rs ## args')) = Some a' -> + (may_overlap chunk addr args chunk' addr' args') = false -> + (Mem.storev chunk m a v) = Some m' -> + (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a'). +Proof. + intros until rs. + intros ADDR ADDR' OVERLAP STORE. + destruct addr; destruct addr'; try discriminate. +- (* Aindexed / Aindexed *) + destruct args as [ | base [ | ]]. 1,3: discriminate. + destruct args' as [ | base' [ | ]]. 1,3: discriminate. + simpl in OVERLAP. + destruct (peq base base'). 2: discriminate. + subst base'. + destruct (can_swap_accesses_ofs z0 chunk' z chunk) eqn:SWAP. + 2: discriminate. + simpl in *. + eapply load_store_away; eassumption. +- (* Aglobal / Aglobal *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + simpl in *. + destruct (peq i i1). + { + subst i1. + rewrite negb_false_iff in OVERLAP. + eapply load_store_glob_away; eassumption. + } + eapply load_store_diff_globals; eassumption. +- (* Ainstack / Ainstack *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + cbn in OVERLAP. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + cbn in *. + eapply stack_load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. +Qed. + +End SOUNDNESS. diff --git a/verilog/ConstpropOp.v b/verilog/ConstpropOp.v deleted file mode 100644 index 9b9c9711..00000000 --- a/verilog/ConstpropOp.v +++ /dev/null @@ -1,899 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Strength reduction for operators and conditions. - This is the machine-dependent part of [Constprop]. *) - -Require Import Coqlib Compopts. -Require Import AST Integers Floats. -Require Import Op Registers. -Require Import ValueDomain ValueAOp. - -(** * Converting known values to constants *) - -Parameter symbol_is_external: ident -> bool. (**r See [SelectOp] *) - -Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a. - -Definition const_for_result (a: aval) : option operation := - match a with - | I n => Some(Ointconst n) - | L n => if Archi.ptr64 then Some(Olongconst n) else None - | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None - | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None - | Ptr(Gl id ofs) => - if symbol_is_external id then - if Ptrofs.eq ofs Ptrofs.zero then Some (Oindirectsymbol id) else None - else - Some (Olea_ptr (Aglobal id ofs)) - | Ptr(Stk ofs) => Some(Olea_ptr (Ainstack ofs)) - | _ => None - end. - -(** * Operator strength reduction *) - -(** We now define auxiliary functions for strength reduction of - operators and addressing modes: replacing an operator with a cheaper - one if some of its arguments are statically known. These are again - large pattern-matchings expressed in indirect style. *) - -(** Original definition: -<< -Nondetfunction cond_strength_reduction - (cond: condition) (args: list reg) (vl: list aval) := - match cond, args, vl with - | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Ccompimm (swap_comparison c) n1, r2 :: nil) - | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Ccompimm c n2, r1 :: nil) - | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Ccompuimm (swap_comparison c) n1, r2 :: nil) - | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Ccompuimm c n2, r1 :: nil) - | Ccompl c, r1 :: r2 :: nil, L n1 :: v2 :: nil => - (Ccomplimm (swap_comparison c) n1, r2 :: nil) - | Ccompl c, r1 :: r2 :: nil, v1 :: L n2 :: nil => - (Ccomplimm c n2, r1 :: nil) - | Ccomplu c, r1 :: r2 :: nil, L n1 :: v2 :: nil => - (Ccompluimm (swap_comparison c) n1, r2 :: nil) - | Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil => - (Ccompluimm c n2, r1 :: nil) - | _, _, _ => - (cond, args) - end. ->> -*) - -Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg) (vl: list aval), Type := - | cond_strength_reduction_case1: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | cond_strength_reduction_case2: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | cond_strength_reduction_case3: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccompu c) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | cond_strength_reduction_case4: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccompu c) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | cond_strength_reduction_case5: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccompl c) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | cond_strength_reduction_case6: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccompl c) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | cond_strength_reduction_case7: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccomplu c) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | cond_strength_reduction_case8: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccomplu c) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | cond_strength_reduction_default: forall (cond: condition) (args: list reg) (vl: list aval), cond_strength_reduction_cases cond args vl. - -Definition cond_strength_reduction_match (cond: condition) (args: list reg) (vl: list aval) := - match cond as zz1, args as zz2, vl as zz3 return cond_strength_reduction_cases zz1 zz2 zz3 with - | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => cond_strength_reduction_case1 c r1 r2 n1 v2 - | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case2 c r1 r2 v1 n2 - | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => cond_strength_reduction_case3 c r1 r2 n1 v2 - | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case4 c r1 r2 v1 n2 - | Ccompl c, r1 :: r2 :: nil, L n1 :: v2 :: nil => cond_strength_reduction_case5 c r1 r2 n1 v2 - | Ccompl c, r1 :: r2 :: nil, v1 :: L n2 :: nil => cond_strength_reduction_case6 c r1 r2 v1 n2 - | Ccomplu c, r1 :: r2 :: nil, L n1 :: v2 :: nil => cond_strength_reduction_case7 c r1 r2 n1 v2 - | Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil => cond_strength_reduction_case8 c r1 r2 v1 n2 - | cond, args, vl => cond_strength_reduction_default cond args vl - end. - -Definition cond_strength_reduction (cond: condition) (args: list reg) (vl: list aval) := - match cond_strength_reduction_match cond args vl with - | cond_strength_reduction_case1 c r1 r2 n1 v2 => (* Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Ccompimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case2 c r1 r2 v1 n2 => (* Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Ccompimm c n2, r1 :: nil) - | cond_strength_reduction_case3 c r1 r2 n1 v2 => (* Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Ccompuimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case4 c r1 r2 v1 n2 => (* Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Ccompuimm c n2, r1 :: nil) - | cond_strength_reduction_case5 c r1 r2 n1 v2 => (* Ccompl c, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - (Ccomplimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case6 c r1 r2 v1 n2 => (* Ccompl c, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - (Ccomplimm c n2, r1 :: nil) - | cond_strength_reduction_case7 c r1 r2 n1 v2 => (* Ccomplu c, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - (Ccompluimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case8 c r1 r2 v1 n2 => (* Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - (Ccompluimm c n2, r1 :: nil) - | cond_strength_reduction_default cond args vl => - (cond, args) - end. - - -Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) := - let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args'). - -Definition make_cmp_imm_eq (c: condition) (args: list reg) (vl: list aval) - (n: int) (r1: reg) (v1: aval) := - if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) - else make_cmp_base c args vl. - -Definition make_cmp_imm_ne (c: condition) (args: list reg) (vl: list aval) - (n: int) (r1: reg) (v1: aval) := - if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) - else make_cmp_base c args vl. - -(** Original definition: -<< -Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := - match c, args, vl with - | Ccompimm Ceq n, r1 :: nil, v1 :: nil => - make_cmp_imm_eq c args vl n r1 v1 - | Ccompimm Cne n, r1 :: nil, v1 :: nil => - make_cmp_imm_ne c args vl n r1 v1 - | Ccompuimm Ceq n, r1 :: nil, v1 :: nil => - make_cmp_imm_eq c args vl n r1 v1 - | Ccompuimm Cne n, r1 :: nil, v1 :: nil => - make_cmp_imm_ne c args vl n r1 v1 - | _, _, _ => - make_cmp_base c args vl - end. ->> -*) - -Inductive make_cmp_cases: forall (c: condition) (args: list reg) (vl: list aval), Type := - | make_cmp_case1: forall n r1 v1, make_cmp_cases (Ccompimm Ceq n) (r1 :: nil) (v1 :: nil) - | make_cmp_case2: forall n r1 v1, make_cmp_cases (Ccompimm Cne n) (r1 :: nil) (v1 :: nil) - | make_cmp_case3: forall n r1 v1, make_cmp_cases (Ccompuimm Ceq n) (r1 :: nil) (v1 :: nil) - | make_cmp_case4: forall n r1 v1, make_cmp_cases (Ccompuimm Cne n) (r1 :: nil) (v1 :: nil) - | make_cmp_default: forall (c: condition) (args: list reg) (vl: list aval), make_cmp_cases c args vl. - -Definition make_cmp_match (c: condition) (args: list reg) (vl: list aval) := - match c as zz1, args as zz2, vl as zz3 return make_cmp_cases zz1 zz2 zz3 with - | Ccompimm Ceq n, r1 :: nil, v1 :: nil => make_cmp_case1 n r1 v1 - | Ccompimm Cne n, r1 :: nil, v1 :: nil => make_cmp_case2 n r1 v1 - | Ccompuimm Ceq n, r1 :: nil, v1 :: nil => make_cmp_case3 n r1 v1 - | Ccompuimm Cne n, r1 :: nil, v1 :: nil => make_cmp_case4 n r1 v1 - | c, args, vl => make_cmp_default c args vl - end. - -Definition make_cmp (c: condition) (args: list reg) (vl: list aval) := - match make_cmp_match c args vl with - | make_cmp_case1 n r1 v1 => (* Ccompimm Ceq n, r1 :: nil, v1 :: nil *) - make_cmp_imm_eq c args vl n r1 v1 - | make_cmp_case2 n r1 v1 => (* Ccompimm Cne n, r1 :: nil, v1 :: nil *) - make_cmp_imm_ne c args vl n r1 v1 - | make_cmp_case3 n r1 v1 => (* Ccompuimm Ceq n, r1 :: nil, v1 :: nil *) - make_cmp_imm_eq c args vl n r1 v1 - | make_cmp_case4 n r1 v1 => (* Ccompuimm Cne n, r1 :: nil, v1 :: nil *) - make_cmp_imm_ne c args vl n r1 v1 - | make_cmp_default c args vl => - make_cmp_base c args vl - end. - - -Definition make_select (c: condition) (ty: typ) - (r1 r2: reg) (args: list reg) (vl: list aval) := - match resolve_branch (eval_static_condition c vl) with - | Some b => (Omove, (if b then r1 else r2) :: nil) - | None => - let (c', args') := cond_strength_reduction c args vl in - (Osel c' ty, r1 :: r2 :: args') - end. - -(** For addressing modes, we need to distinguish -- reductions that produce pointers (i.e. that produce [Aglobal], [Ainstack], [Abased] and [Abasedscaled] addressing modes), which are valid only if the pointer size is right; -- other reductions (producing [Aindexed] or [Aindexed2] modes), which are valid independently of the pointer size. -*) - -(** Original definition: -<< -Nondetfunction addr_strength_reduction_32_generic - (addr: addressing) (args: list reg) (vl: list aval) := - match addr, args, vl with - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Aindexed (Int.signed n1 + ofs), r2 :: nil) - | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Aindexed (Int.signed n2 + ofs), r1 :: nil) - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Aindexed (Int.signed n2 * sc + ofs), r1 :: nil) - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Ascaled sc (Int.signed n1 + ofs), r2 :: nil) - | _, _ => - (addr, args) - end. ->> -*) - -Inductive addr_strength_reduction_32_generic_cases: forall (addr: addressing) (args: list reg) (vl: list aval), Type := - | addr_strength_reduction_32_generic_case1: forall ofs r1 r2 n1 v2, addr_strength_reduction_32_generic_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | addr_strength_reduction_32_generic_case2: forall ofs r1 r2 v1 n2, addr_strength_reduction_32_generic_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | addr_strength_reduction_32_generic_case3: forall sc ofs r1 r2 v1 n2, addr_strength_reduction_32_generic_cases (Aindexed2scaled sc ofs) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | addr_strength_reduction_32_generic_case4: forall sc ofs r1 r2 n1 v2, addr_strength_reduction_32_generic_cases (Aindexed2scaled sc ofs) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | addr_strength_reduction_32_generic_default: forall (addr: addressing) (args: list reg) (vl: list aval), addr_strength_reduction_32_generic_cases addr args vl. - -Definition addr_strength_reduction_32_generic_match (addr: addressing) (args: list reg) (vl: list aval) := - match addr as zz1, args as zz2, vl as zz3 return addr_strength_reduction_32_generic_cases zz1 zz2 zz3 with - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil => addr_strength_reduction_32_generic_case1 ofs r1 r2 n1 v2 - | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil => addr_strength_reduction_32_generic_case2 ofs r1 r2 v1 n2 - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil => addr_strength_reduction_32_generic_case3 sc ofs r1 r2 v1 n2 - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil => addr_strength_reduction_32_generic_case4 sc ofs r1 r2 n1 v2 - | addr, args, vl => addr_strength_reduction_32_generic_default addr args vl - end. - -Definition addr_strength_reduction_32_generic (addr: addressing) (args: list reg) (vl: list aval) := - match addr_strength_reduction_32_generic_match addr args vl with - | addr_strength_reduction_32_generic_case1 ofs r1 r2 n1 v2 => (* Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Aindexed (Int.signed n1 + ofs), r2 :: nil) - | addr_strength_reduction_32_generic_case2 ofs r1 r2 v1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Aindexed (Int.signed n2 + ofs), r1 :: nil) - | addr_strength_reduction_32_generic_case3 sc ofs r1 r2 v1 n2 => (* Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Aindexed (Int.signed n2 * sc + ofs), r1 :: nil) - | addr_strength_reduction_32_generic_case4 sc ofs r1 r2 n1 v2 => (* Aindexed2scaled sc ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Ascaled sc (Int.signed n1 + ofs), r2 :: nil) - | addr_strength_reduction_32_generic_default addr args vl => - (addr, args) - end. - - -(** Original definition: -<< -Nondetfunction addr_strength_reduction_32 - (addr: addressing) (args: list reg) (vl: list aval) := - - if Archi.ptr64 then addr_strength_reduction_32_generic addr args vl else - - match addr, args, vl with - - | Aindexed ofs, r1 :: nil, Ptr(Gl symb n) :: nil => - (Aglobal symb (Ptrofs.add n (Ptrofs.repr ofs)), nil) - | Aindexed ofs, r1 :: nil, Ptr(Stk n) :: nil => - (Ainstack (Ptrofs.add n (Ptrofs.repr ofs)), nil) - - | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: I n2 :: nil => - (Aglobal symb (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int n2)) (Ptrofs.repr ofs)), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: Ptr(Gl symb n2) :: nil => - (Aglobal symb (Ptrofs.add (Ptrofs.add n2 (Ptrofs.of_int n1)) (Ptrofs.repr ofs)), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil => - (Ainstack (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int n2)) (Ptrofs.repr ofs)), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: Ptr(Stk n2) :: nil => - (Ainstack (Ptrofs.add (Ptrofs.add (Ptrofs.of_int n1) n2) (Ptrofs.repr ofs)), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: v2 :: nil => - (Abased symb (Ptrofs.add n1 (Ptrofs.repr ofs)), r2 :: nil) - | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: Ptr(Gl symb n2) :: nil => - (Abased symb (Ptrofs.add n2 (Ptrofs.repr ofs)), r1 :: nil) - - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: I n2 :: nil => - (Aglobal symb (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int (Int.mul n2 (Int.repr sc)))) (Ptrofs.repr ofs)), nil) - - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: v2 :: nil => - (Abasedscaled sc symb (Ptrofs.add n1 (Ptrofs.repr ofs)), r2 :: nil) - - | Abased id ofs, r1 :: nil, I n1 :: nil => - (Aglobal id (Ptrofs.add ofs (Ptrofs.of_int n1)), nil) - - | Abasedscaled sc id ofs, r1 :: nil, I n1 :: nil => - (Aglobal id (Ptrofs.add ofs (Ptrofs.of_int (Int.mul n1 (Int.repr sc)))), nil) - - | _, _ => - addr_strength_reduction_32_generic addr args vl - end. ->> -*) - -Inductive addr_strength_reduction_32_cases: forall (addr: addressing) (args: list reg) (vl: list aval), Type := - | addr_strength_reduction_32_case1: forall ofs r1 symb n, addr_strength_reduction_32_cases (Aindexed ofs) (r1 :: nil) (Ptr(Gl symb n) :: nil) - | addr_strength_reduction_32_case2: forall ofs r1 n, addr_strength_reduction_32_cases (Aindexed ofs) (r1 :: nil) (Ptr(Stk n) :: nil) - | addr_strength_reduction_32_case3: forall ofs r1 r2 symb n1 n2, addr_strength_reduction_32_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (Ptr(Gl symb n1) :: I n2 :: nil) - | addr_strength_reduction_32_case4: forall ofs r1 r2 n1 symb n2, addr_strength_reduction_32_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (I n1 :: Ptr(Gl symb n2) :: nil) - | addr_strength_reduction_32_case5: forall ofs r1 r2 n1 n2, addr_strength_reduction_32_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (Ptr(Stk n1) :: I n2 :: nil) - | addr_strength_reduction_32_case6: forall ofs r1 r2 n1 n2, addr_strength_reduction_32_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (I n1 :: Ptr(Stk n2) :: nil) - | addr_strength_reduction_32_case7: forall ofs r1 r2 symb n1 v2, addr_strength_reduction_32_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (Ptr(Gl symb n1) :: v2 :: nil) - | addr_strength_reduction_32_case8: forall ofs r1 r2 v1 symb n2, addr_strength_reduction_32_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (v1 :: Ptr(Gl symb n2) :: nil) - | addr_strength_reduction_32_case9: forall sc ofs r1 r2 symb n1 n2, addr_strength_reduction_32_cases (Aindexed2scaled sc ofs) (r1 :: r2 :: nil) (Ptr(Gl symb n1) :: I n2 :: nil) - | addr_strength_reduction_32_case10: forall sc ofs r1 r2 symb n1 v2, addr_strength_reduction_32_cases (Aindexed2scaled sc ofs) (r1 :: r2 :: nil) (Ptr(Gl symb n1) :: v2 :: nil) - | addr_strength_reduction_32_case11: forall id ofs r1 n1, addr_strength_reduction_32_cases (Abased id ofs) (r1 :: nil) (I n1 :: nil) - | addr_strength_reduction_32_case12: forall sc id ofs r1 n1, addr_strength_reduction_32_cases (Abasedscaled sc id ofs) (r1 :: nil) (I n1 :: nil) - | addr_strength_reduction_32_default: forall (addr: addressing) (args: list reg) (vl: list aval), addr_strength_reduction_32_cases addr args vl. - -Definition addr_strength_reduction_32_match (addr: addressing) (args: list reg) (vl: list aval) := - match addr as zz1, args as zz2, vl as zz3 return addr_strength_reduction_32_cases zz1 zz2 zz3 with - | Aindexed ofs, r1 :: nil, Ptr(Gl symb n) :: nil => addr_strength_reduction_32_case1 ofs r1 symb n - | Aindexed ofs, r1 :: nil, Ptr(Stk n) :: nil => addr_strength_reduction_32_case2 ofs r1 n - | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: I n2 :: nil => addr_strength_reduction_32_case3 ofs r1 r2 symb n1 n2 - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: Ptr(Gl symb n2) :: nil => addr_strength_reduction_32_case4 ofs r1 r2 n1 symb n2 - | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil => addr_strength_reduction_32_case5 ofs r1 r2 n1 n2 - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: Ptr(Stk n2) :: nil => addr_strength_reduction_32_case6 ofs r1 r2 n1 n2 - | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: v2 :: nil => addr_strength_reduction_32_case7 ofs r1 r2 symb n1 v2 - | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: Ptr(Gl symb n2) :: nil => addr_strength_reduction_32_case8 ofs r1 r2 v1 symb n2 - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: I n2 :: nil => addr_strength_reduction_32_case9 sc ofs r1 r2 symb n1 n2 - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: v2 :: nil => addr_strength_reduction_32_case10 sc ofs r1 r2 symb n1 v2 - | Abased id ofs, r1 :: nil, I n1 :: nil => addr_strength_reduction_32_case11 id ofs r1 n1 - | Abasedscaled sc id ofs, r1 :: nil, I n1 :: nil => addr_strength_reduction_32_case12 sc id ofs r1 n1 - | addr, args, vl => addr_strength_reduction_32_default addr args vl - end. - -Definition addr_strength_reduction_32 (addr: addressing) (args: list reg) (vl: list aval) := - if Archi.ptr64 then addr_strength_reduction_32_generic addr args vl else match addr_strength_reduction_32_match addr args vl with - | addr_strength_reduction_32_case1 ofs r1 symb n => (* Aindexed ofs, r1 :: nil, Ptr(Gl symb n) :: nil *) - (Aglobal symb (Ptrofs.add n (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_32_case2 ofs r1 n => (* Aindexed ofs, r1 :: nil, Ptr(Stk n) :: nil *) - (Ainstack (Ptrofs.add n (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_32_case3 ofs r1 r2 symb n1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: I n2 :: nil *) - (Aglobal symb (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int n2)) (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_32_case4 ofs r1 r2 n1 symb n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: Ptr(Gl symb n2) :: nil *) - (Aglobal symb (Ptrofs.add (Ptrofs.add n2 (Ptrofs.of_int n1)) (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_32_case5 ofs r1 r2 n1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil *) - (Ainstack (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int n2)) (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_32_case6 ofs r1 r2 n1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: Ptr(Stk n2) :: nil *) - (Ainstack (Ptrofs.add (Ptrofs.add (Ptrofs.of_int n1) n2) (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_32_case7 ofs r1 r2 symb n1 v2 => (* Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: v2 :: nil *) - (Abased symb (Ptrofs.add n1 (Ptrofs.repr ofs)), r2 :: nil) - | addr_strength_reduction_32_case8 ofs r1 r2 v1 symb n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, v1 :: Ptr(Gl symb n2) :: nil *) - (Abased symb (Ptrofs.add n2 (Ptrofs.repr ofs)), r1 :: nil) - | addr_strength_reduction_32_case9 sc ofs r1 r2 symb n1 n2 => (* Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: I n2 :: nil *) - (Aglobal symb (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int (Int.mul n2 (Int.repr sc)))) (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_32_case10 sc ofs r1 r2 symb n1 v2 => (* Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: v2 :: nil *) - (Abasedscaled sc symb (Ptrofs.add n1 (Ptrofs.repr ofs)), r2 :: nil) - | addr_strength_reduction_32_case11 id ofs r1 n1 => (* Abased id ofs, r1 :: nil, I n1 :: nil *) - (Aglobal id (Ptrofs.add ofs (Ptrofs.of_int n1)), nil) - | addr_strength_reduction_32_case12 sc id ofs r1 n1 => (* Abasedscaled sc id ofs, r1 :: nil, I n1 :: nil *) - (Aglobal id (Ptrofs.add ofs (Ptrofs.of_int (Int.mul n1 (Int.repr sc)))), nil) - | addr_strength_reduction_32_default addr args vl => - addr_strength_reduction_32_generic addr args vl - end. - - -(** Original definition: -<< -Nondetfunction addr_strength_reduction_64_generic - (addr: addressing) (args: list reg) (vl: list aval) := - match addr, args, vl with - | Aindexed2 ofs, r1 :: r2 :: nil, L n1 :: v2 :: nil => - (Aindexed (Int64.signed n1 + ofs), r2 :: nil) - | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: L n2 :: nil => - (Aindexed (Int64.signed n2 + ofs), r1 :: nil) - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: L n2 :: nil => - (Aindexed (Int64.signed n2 * sc + ofs), r1 :: nil) - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, L n1 :: v2 :: nil => - (Ascaled sc (Int64.signed n1 + ofs), r2 :: nil) - | _, _ => - (addr, args) - end. ->> -*) - -Inductive addr_strength_reduction_64_generic_cases: forall (addr: addressing) (args: list reg) (vl: list aval), Type := - | addr_strength_reduction_64_generic_case1: forall ofs r1 r2 n1 v2, addr_strength_reduction_64_generic_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | addr_strength_reduction_64_generic_case2: forall ofs r1 r2 v1 n2, addr_strength_reduction_64_generic_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | addr_strength_reduction_64_generic_case3: forall sc ofs r1 r2 v1 n2, addr_strength_reduction_64_generic_cases (Aindexed2scaled sc ofs) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | addr_strength_reduction_64_generic_case4: forall sc ofs r1 r2 n1 v2, addr_strength_reduction_64_generic_cases (Aindexed2scaled sc ofs) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | addr_strength_reduction_64_generic_default: forall (addr: addressing) (args: list reg) (vl: list aval), addr_strength_reduction_64_generic_cases addr args vl. - -Definition addr_strength_reduction_64_generic_match (addr: addressing) (args: list reg) (vl: list aval) := - match addr as zz1, args as zz2, vl as zz3 return addr_strength_reduction_64_generic_cases zz1 zz2 zz3 with - | Aindexed2 ofs, r1 :: r2 :: nil, L n1 :: v2 :: nil => addr_strength_reduction_64_generic_case1 ofs r1 r2 n1 v2 - | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: L n2 :: nil => addr_strength_reduction_64_generic_case2 ofs r1 r2 v1 n2 - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: L n2 :: nil => addr_strength_reduction_64_generic_case3 sc ofs r1 r2 v1 n2 - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, L n1 :: v2 :: nil => addr_strength_reduction_64_generic_case4 sc ofs r1 r2 n1 v2 - | addr, args, vl => addr_strength_reduction_64_generic_default addr args vl - end. - -Definition addr_strength_reduction_64_generic (addr: addressing) (args: list reg) (vl: list aval) := - match addr_strength_reduction_64_generic_match addr args vl with - | addr_strength_reduction_64_generic_case1 ofs r1 r2 n1 v2 => (* Aindexed2 ofs, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - (Aindexed (Int64.signed n1 + ofs), r2 :: nil) - | addr_strength_reduction_64_generic_case2 ofs r1 r2 v1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - (Aindexed (Int64.signed n2 + ofs), r1 :: nil) - | addr_strength_reduction_64_generic_case3 sc ofs r1 r2 v1 n2 => (* Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - (Aindexed (Int64.signed n2 * sc + ofs), r1 :: nil) - | addr_strength_reduction_64_generic_case4 sc ofs r1 r2 n1 v2 => (* Aindexed2scaled sc ofs, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - (Ascaled sc (Int64.signed n1 + ofs), r2 :: nil) - | addr_strength_reduction_64_generic_default addr args vl => - (addr, args) - end. - - -(** Original definition: -<< -Nondetfunction addr_strength_reduction_64 - (addr: addressing) (args: list reg) (vl: list aval) := - - if negb Archi.ptr64 then addr_strength_reduction_64_generic addr args vl else - - match addr, args, vl with - - | Aindexed ofs, r1 :: nil, Ptr(Gl symb n) :: nil => - (Aglobal symb (Ptrofs.add n (Ptrofs.repr ofs)), nil) - | Aindexed ofs, r1 :: nil, Ptr(Stk n) :: nil => - (Ainstack (Ptrofs.add n (Ptrofs.repr ofs)), nil) - - | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: L n2 :: nil => - (Aglobal symb (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int64 n2)) (Ptrofs.repr ofs)), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, L n1 :: Ptr(Gl symb n2) :: nil => - (Aglobal symb (Ptrofs.add (Ptrofs.add n2 (Ptrofs.of_int64 n1)) (Ptrofs.repr ofs)), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Stk n1) :: L n2 :: nil => - (Ainstack (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int64 n2)) (Ptrofs.repr ofs)), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, L n1 :: Ptr(Stk n2) :: nil => - (Ainstack (Ptrofs.add (Ptrofs.add (Ptrofs.of_int64 n1) n2) (Ptrofs.repr ofs)), nil) - - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: L n2 :: nil => - (Aglobal symb (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int64 (Int64.mul n2 (Int64.repr sc)))) (Ptrofs.repr ofs)), nil) - - | _, _ => - addr_strength_reduction_64_generic addr args vl - end. ->> -*) - -Inductive addr_strength_reduction_64_cases: forall (addr: addressing) (args: list reg) (vl: list aval), Type := - | addr_strength_reduction_64_case1: forall ofs r1 symb n, addr_strength_reduction_64_cases (Aindexed ofs) (r1 :: nil) (Ptr(Gl symb n) :: nil) - | addr_strength_reduction_64_case2: forall ofs r1 n, addr_strength_reduction_64_cases (Aindexed ofs) (r1 :: nil) (Ptr(Stk n) :: nil) - | addr_strength_reduction_64_case3: forall ofs r1 r2 symb n1 n2, addr_strength_reduction_64_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (Ptr(Gl symb n1) :: L n2 :: nil) - | addr_strength_reduction_64_case4: forall ofs r1 r2 n1 symb n2, addr_strength_reduction_64_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (L n1 :: Ptr(Gl symb n2) :: nil) - | addr_strength_reduction_64_case5: forall ofs r1 r2 n1 n2, addr_strength_reduction_64_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (Ptr(Stk n1) :: L n2 :: nil) - | addr_strength_reduction_64_case6: forall ofs r1 r2 n1 n2, addr_strength_reduction_64_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (L n1 :: Ptr(Stk n2) :: nil) - | addr_strength_reduction_64_case7: forall sc ofs r1 r2 symb n1 n2, addr_strength_reduction_64_cases (Aindexed2scaled sc ofs) (r1 :: r2 :: nil) (Ptr(Gl symb n1) :: L n2 :: nil) - | addr_strength_reduction_64_default: forall (addr: addressing) (args: list reg) (vl: list aval), addr_strength_reduction_64_cases addr args vl. - -Definition addr_strength_reduction_64_match (addr: addressing) (args: list reg) (vl: list aval) := - match addr as zz1, args as zz2, vl as zz3 return addr_strength_reduction_64_cases zz1 zz2 zz3 with - | Aindexed ofs, r1 :: nil, Ptr(Gl symb n) :: nil => addr_strength_reduction_64_case1 ofs r1 symb n - | Aindexed ofs, r1 :: nil, Ptr(Stk n) :: nil => addr_strength_reduction_64_case2 ofs r1 n - | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: L n2 :: nil => addr_strength_reduction_64_case3 ofs r1 r2 symb n1 n2 - | Aindexed2 ofs, r1 :: r2 :: nil, L n1 :: Ptr(Gl symb n2) :: nil => addr_strength_reduction_64_case4 ofs r1 r2 n1 symb n2 - | Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Stk n1) :: L n2 :: nil => addr_strength_reduction_64_case5 ofs r1 r2 n1 n2 - | Aindexed2 ofs, r1 :: r2 :: nil, L n1 :: Ptr(Stk n2) :: nil => addr_strength_reduction_64_case6 ofs r1 r2 n1 n2 - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: L n2 :: nil => addr_strength_reduction_64_case7 sc ofs r1 r2 symb n1 n2 - | addr, args, vl => addr_strength_reduction_64_default addr args vl - end. - -Definition addr_strength_reduction_64 (addr: addressing) (args: list reg) (vl: list aval) := - if negb Archi.ptr64 then addr_strength_reduction_64_generic addr args vl else match addr_strength_reduction_64_match addr args vl with - | addr_strength_reduction_64_case1 ofs r1 symb n => (* Aindexed ofs, r1 :: nil, Ptr(Gl symb n) :: nil *) - (Aglobal symb (Ptrofs.add n (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_64_case2 ofs r1 n => (* Aindexed ofs, r1 :: nil, Ptr(Stk n) :: nil *) - (Ainstack (Ptrofs.add n (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_64_case3 ofs r1 r2 symb n1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: L n2 :: nil *) - (Aglobal symb (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int64 n2)) (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_64_case4 ofs r1 r2 n1 symb n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, L n1 :: Ptr(Gl symb n2) :: nil *) - (Aglobal symb (Ptrofs.add (Ptrofs.add n2 (Ptrofs.of_int64 n1)) (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_64_case5 ofs r1 r2 n1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, Ptr(Stk n1) :: L n2 :: nil *) - (Ainstack (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int64 n2)) (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_64_case6 ofs r1 r2 n1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, L n1 :: Ptr(Stk n2) :: nil *) - (Ainstack (Ptrofs.add (Ptrofs.add (Ptrofs.of_int64 n1) n2) (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_64_case7 sc ofs r1 r2 symb n1 n2 => (* Aindexed2scaled sc ofs, r1 :: r2 :: nil, Ptr(Gl symb n1) :: L n2 :: nil *) - (Aglobal symb (Ptrofs.add (Ptrofs.add n1 (Ptrofs.of_int64 (Int64.mul n2 (Int64.repr sc)))) (Ptrofs.repr ofs)), nil) - | addr_strength_reduction_64_default addr args vl => - addr_strength_reduction_64_generic addr args vl - end. - - -Definition addr_strength_reduction - (addr: addressing) (args: list reg) (vl: list aval) := - let addr_args' := - if Archi.ptr64 - then addr_strength_reduction_64 addr args vl - else addr_strength_reduction_32 addr args vl in - if addressing_valid (fst addr_args') then addr_args' else (addr, args). - -Definition make_addimm (n: int) (r: reg) := - if Int.eq n Int.zero - then (Omove, r :: nil) - else (Olea (Aindexed (Int.signed n)), r :: nil). - -Definition make_shlimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int.iwordsize then (Oshlimm n, r1 :: nil) - else (Oshl, r1 :: r2 :: nil). - -Definition make_shrimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int.iwordsize then (Oshrimm n, r1 :: nil) - else (Oshr, r1 :: r2 :: nil). - -Definition make_shruimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int.iwordsize then (Oshruimm n, r1 :: nil) - else (Oshru, r1 :: r2 :: nil). - -Definition make_mulimm (n: int) (r: reg) := - if Int.eq n Int.zero then - (Ointconst Int.zero, nil) - else if Int.eq n Int.one then - (Omove, r :: nil) - else - match Int.is_power2 n with - | Some l => (Oshlimm l, r :: nil) - | None => (Omulimm n, r :: nil) - end. - -Definition make_andimm (n: int) (r: reg) (a: aval) := - if Int.eq n Int.zero then (Ointconst Int.zero, nil) - else if Int.eq n Int.mone then (Omove, r :: nil) - else if match a with Uns _ m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero - | _ => false end - then (Omove, r :: nil) - else (Oandimm n, r :: nil). - -Definition make_orimm (n: int) (r: reg) := - if Int.eq n Int.zero then (Omove, r :: nil) - else if Int.eq n Int.mone then (Ointconst Int.mone, nil) - else (Oorimm n, r :: nil). - -Definition make_xorimm (n: int) (r: reg) := - if Int.eq n Int.zero then (Omove, r :: nil) - else if Int.eq n Int.mone then (Onot, r :: nil) - else (Oxorimm n, r :: nil). - -Definition make_divimm n (r1 r2: reg) := - if Int.eq n Int.one then - (Omove, r1 :: nil) - else - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. - -Definition make_divuimm n (r1 r2: reg) := - if Int.eq n Int.one then - (Omove, r1 :: nil) - else - match Int.is_power2 n with - | Some l => (Oshruimm l, r1 :: nil) - | None => (Odivu, r1 :: r2 :: nil) - end. - -Definition make_moduimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => (Oandimm (Int.sub n Int.one), r1 :: nil) - | None => (Omodu, r1 :: r2 :: nil) - end. - -Definition make_addlimm (n: int64) (r: reg) := - if Int64.eq n Int64.zero - then (Omove, r :: nil) - else (Oleal (Aindexed (Int64.signed n)), r :: nil). - -Definition make_shllimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int64.iwordsize' then (Oshllimm n, r1 :: nil) - else (Oshll, r1 :: r2 :: nil). - -Definition make_shrlimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int64.iwordsize' then (Oshrlimm n, r1 :: nil) - else (Oshrl, r1 :: r2 :: nil). - -Definition make_shrluimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int64.iwordsize' then (Oshrluimm n, r1 :: nil) - else (Oshrlu, r1 :: r2 :: nil). - -Definition make_mullimm (n: int64) (r: reg) := - if Int64.eq n Int64.zero then - (Olongconst Int64.zero, nil) - else if Int64.eq n Int64.one then - (Omove, r :: nil) - else - match Int64.is_power2' n with - | Some l => (Oshllimm l, r :: nil) - | None => (Omullimm n, r :: nil) - end. - -Definition make_andlimm (n: int64) (r: reg) (a: aval) := - if Int64.eq n Int64.zero then (Olongconst Int64.zero, nil) - else if Int64.eq n Int64.mone then (Omove, r :: nil) - else (Oandlimm n, r :: nil). - -Definition make_orlimm (n: int64) (r: reg) := - if Int64.eq n Int64.zero then (Omove, r :: nil) - else if Int64.eq n Int64.mone then (Olongconst Int64.mone, nil) - else (Oorlimm n, r :: nil). - -Definition make_xorlimm (n: int64) (r: reg) := - if Int64.eq n Int64.zero then (Omove, r :: nil) - else if Int64.eq n Int64.mone then (Onotl, r :: nil) - else (Oxorlimm n, r :: nil). - -Definition make_divlimm n (r1 r2: reg) := - match Int64.is_power2' n with - | Some l => if Int.ltu l (Int.repr 63) - then (Oshrxlimm l, r1 :: nil) - else (Odivl, r1 :: r2 :: nil) - | None => (Odivl, r1 :: r2 :: nil) - end. - -Definition make_divluimm n (r1 r2: reg) := - match Int64.is_power2' n with - | Some l => (Oshrluimm l, r1 :: nil) - | None => (Odivlu, r1 :: r2 :: nil) - end. - -Definition make_modluimm n (r1 r2: reg) := - match Int64.is_power2 n with - | Some l => (Oandlimm (Int64.sub n Int64.one), r1 :: nil) - | None => (Omodlu, r1 :: r2 :: nil) - end. - -Definition make_mulfimm (n: float) (r r1 r2: reg) := - if Float.eq_dec n (Float.of_int (Int.repr 2)) - then (Oaddf, r :: r :: nil) - else (Omulf, r1 :: r2 :: nil). - -Definition make_mulfsimm (n: float32) (r r1 r2: reg) := - if Float32.eq_dec n (Float32.of_int (Int.repr 2)) - then (Oaddfs, r :: r :: nil) - else (Omulfs, r1 :: r2 :: nil). - -Definition make_cast8signed (r: reg) (a: aval) := - if vincl a (Sgn Ptop 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). -Definition make_cast8unsigned (r: reg) (a: aval) := - if vincl a (Uns Ptop 8) then (Omove, r :: nil) else (Ocast8unsigned, r :: nil). -Definition make_cast16signed (r: reg) (a: aval) := - if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). -Definition make_cast16unsigned (r: reg) (a: aval) := - if vincl a (Uns Ptop 16) then (Omove, r :: nil) else (Ocast16unsigned, r :: nil). - -(** Original definition: -<< -Nondetfunction op_strength_reduction - (op: operation) (args: list reg) (vl: list aval) := - match op, args, vl with - | Ocast8signed, r1 :: nil, v1 :: nil => make_cast8signed r1 v1 - | Ocast8unsigned, r1 :: nil, v1 :: nil => make_cast8unsigned r1 v1 - | Ocast16signed, r1 :: nil, v1 :: nil => make_cast16signed r1 v1 - | Ocast16unsigned, r1 :: nil, v1 :: nil => make_cast16unsigned r1 v1 - | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1 - | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2 - | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 - | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divimm n2 r1 r2 - | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divuimm n2 r1 r2 - | Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_moduimm n2 r1 r2 - | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2 v2 - | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1 v1 - | Oandimm n, r1 :: nil, v1 :: nil => make_andimm n r1 v1 - | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_orimm n1 r2 - | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1 - | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_xorimm n1 r2 - | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1 - | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2 - | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2 - | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2 - | Olea addr, args, vl => - let (addr', args') := addr_strength_reduction_32 addr args vl in - (Olea addr', args') - | Osubl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_addlimm (Int64.neg n2) r1 - | Omull, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_mullimm n1 r2 - | Omull, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_mullimm n2 r1 - | Odivl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_divlimm n2 r1 r2 - | Odivlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_divluimm n2 r1 r2 - | Omodlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_modluimm n2 r1 r2 - | Oandl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_andlimm n1 r2 v2 - | Oandl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_andlimm n2 r1 v1 - | Oandlimm n, r1 :: nil, v1 :: nil => make_andlimm n r1 v1 - | Oorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_orlimm n1 r2 - | Oorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_orlimm n2 r1 - | Oxorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_xorlimm n1 r2 - | Oxorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_xorlimm n2 r1 - | Oshll, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shllimm n2 r1 r2 - | Oshrl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrlimm n2 r1 r2 - | Oshrlu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrluimm n2 r1 r2 - | Oleal addr, args, vl => - let (addr', args') := addr_strength_reduction_64 addr args vl in - (Oleal addr', args') - | Ocmp c, args, vl => make_cmp c args vl - | Osel c ty, r1 :: r2 :: args, v1 :: v2 :: vl => make_select c ty r1 r2 args vl - | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2 - | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2 - | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => make_mulfsimm n2 r1 r1 r2 - | Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil => make_mulfsimm n1 r2 r1 r2 - | _, _, _ => (op, args) - end. ->> -*) - -Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg) (vl: list aval), Type := - | op_strength_reduction_case1: forall r1 v1, op_strength_reduction_cases (Ocast8signed) (r1 :: nil) (v1 :: nil) - | op_strength_reduction_case2: forall r1 v1, op_strength_reduction_cases (Ocast8unsigned) (r1 :: nil) (v1 :: nil) - | op_strength_reduction_case3: forall r1 v1, op_strength_reduction_cases (Ocast16signed) (r1 :: nil) (v1 :: nil) - | op_strength_reduction_case4: forall r1 v1, op_strength_reduction_cases (Ocast16unsigned) (r1 :: nil) (v1 :: nil) - | op_strength_reduction_case5: forall r1 r2 v1 n2, op_strength_reduction_cases (Osub) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case6: forall r1 r2 n1 v2, op_strength_reduction_cases (Omul) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case7: forall r1 r2 v1 n2, op_strength_reduction_cases (Omul) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case8: forall r1 r2 v1 n2, op_strength_reduction_cases (Odiv) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case9: forall r1 r2 v1 n2, op_strength_reduction_cases (Odivu) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case10: forall r1 r2 v1 n2, op_strength_reduction_cases (Omodu) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case11: forall r1 r2 n1 v2, op_strength_reduction_cases (Oand) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case12: forall r1 r2 v1 n2, op_strength_reduction_cases (Oand) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case13: forall n r1 v1, op_strength_reduction_cases (Oandimm n) (r1 :: nil) (v1 :: nil) - | op_strength_reduction_case14: forall r1 r2 n1 v2, op_strength_reduction_cases (Oor) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case15: forall r1 r2 v1 n2, op_strength_reduction_cases (Oor) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case16: forall r1 r2 n1 v2, op_strength_reduction_cases (Oxor) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case17: forall r1 r2 v1 n2, op_strength_reduction_cases (Oxor) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case18: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshl) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case19: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshr) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case20: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshru) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case21: forall addr args vl, op_strength_reduction_cases (Olea addr) (args) (vl) - | op_strength_reduction_case22: forall r1 r2 v1 n2, op_strength_reduction_cases (Osubl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case23: forall r1 r2 n1 v2, op_strength_reduction_cases (Omull) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | op_strength_reduction_case24: forall r1 r2 v1 n2, op_strength_reduction_cases (Omull) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case25: forall r1 r2 v1 n2, op_strength_reduction_cases (Odivl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case26: forall r1 r2 v1 n2, op_strength_reduction_cases (Odivlu) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case27: forall r1 r2 v1 n2, op_strength_reduction_cases (Omodlu) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case28: forall r1 r2 n1 v2, op_strength_reduction_cases (Oandl) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | op_strength_reduction_case29: forall r1 r2 v1 n2, op_strength_reduction_cases (Oandl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case30: forall n r1 v1, op_strength_reduction_cases (Oandlimm n) (r1 :: nil) (v1 :: nil) - | op_strength_reduction_case31: forall r1 r2 n1 v2, op_strength_reduction_cases (Oorl) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | op_strength_reduction_case32: forall r1 r2 v1 n2, op_strength_reduction_cases (Oorl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case33: forall r1 r2 n1 v2, op_strength_reduction_cases (Oxorl) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | op_strength_reduction_case34: forall r1 r2 v1 n2, op_strength_reduction_cases (Oxorl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case35: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshll) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case36: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshrl) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case37: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshrlu) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case38: forall addr args vl, op_strength_reduction_cases (Oleal addr) (args) (vl) - | op_strength_reduction_case39: forall c args vl, op_strength_reduction_cases (Ocmp c) (args) (vl) - | op_strength_reduction_case40: forall c ty r1 r2 args v1 v2 vl, op_strength_reduction_cases (Osel c ty) (r1 :: r2 :: args) (v1 :: v2 :: vl) - | op_strength_reduction_case41: forall r1 r2 v1 n2, op_strength_reduction_cases (Omulf) (r1 :: r2 :: nil) (v1 :: F n2 :: nil) - | op_strength_reduction_case42: forall r1 r2 n1 v2, op_strength_reduction_cases (Omulf) (r1 :: r2 :: nil) (F n1 :: v2 :: nil) - | op_strength_reduction_case43: forall r1 r2 v1 n2, op_strength_reduction_cases (Omulfs) (r1 :: r2 :: nil) (v1 :: FS n2 :: nil) - | op_strength_reduction_case44: forall r1 r2 n1 v2, op_strength_reduction_cases (Omulfs) (r1 :: r2 :: nil) (FS n1 :: v2 :: nil) - | op_strength_reduction_default: forall (op: operation) (args: list reg) (vl: list aval), op_strength_reduction_cases op args vl. - -Definition op_strength_reduction_match (op: operation) (args: list reg) (vl: list aval) := - match op as zz1, args as zz2, vl as zz3 return op_strength_reduction_cases zz1 zz2 zz3 with - | Ocast8signed, r1 :: nil, v1 :: nil => op_strength_reduction_case1 r1 v1 - | Ocast8unsigned, r1 :: nil, v1 :: nil => op_strength_reduction_case2 r1 v1 - | Ocast16signed, r1 :: nil, v1 :: nil => op_strength_reduction_case3 r1 v1 - | Ocast16unsigned, r1 :: nil, v1 :: nil => op_strength_reduction_case4 r1 v1 - | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case5 r1 r2 v1 n2 - | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case6 r1 r2 n1 v2 - | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case7 r1 r2 v1 n2 - | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case8 r1 r2 v1 n2 - | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case9 r1 r2 v1 n2 - | Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case10 r1 r2 v1 n2 - | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case11 r1 r2 n1 v2 - | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case12 r1 r2 v1 n2 - | Oandimm n, r1 :: nil, v1 :: nil => op_strength_reduction_case13 n r1 v1 - | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case14 r1 r2 n1 v2 - | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case15 r1 r2 v1 n2 - | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case16 r1 r2 n1 v2 - | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case17 r1 r2 v1 n2 - | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case18 r1 r2 v1 n2 - | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case19 r1 r2 v1 n2 - | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case20 r1 r2 v1 n2 - | Olea addr, args, vl => op_strength_reduction_case21 addr args vl - | Osubl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case22 r1 r2 v1 n2 - | Omull, r1 :: r2 :: nil, L n1 :: v2 :: nil => op_strength_reduction_case23 r1 r2 n1 v2 - | Omull, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case24 r1 r2 v1 n2 - | Odivl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case25 r1 r2 v1 n2 - | Odivlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case26 r1 r2 v1 n2 - | Omodlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case27 r1 r2 v1 n2 - | Oandl, r1 :: r2 :: nil, L n1 :: v2 :: nil => op_strength_reduction_case28 r1 r2 n1 v2 - | Oandl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case29 r1 r2 v1 n2 - | Oandlimm n, r1 :: nil, v1 :: nil => op_strength_reduction_case30 n r1 v1 - | Oorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => op_strength_reduction_case31 r1 r2 n1 v2 - | Oorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case32 r1 r2 v1 n2 - | Oxorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => op_strength_reduction_case33 r1 r2 n1 v2 - | Oxorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case34 r1 r2 v1 n2 - | Oshll, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case35 r1 r2 v1 n2 - | Oshrl, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case36 r1 r2 v1 n2 - | Oshrlu, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case37 r1 r2 v1 n2 - | Oleal addr, args, vl => op_strength_reduction_case38 addr args vl - | Ocmp c, args, vl => op_strength_reduction_case39 c args vl - | Osel c ty, r1 :: r2 :: args, v1 :: v2 :: vl => op_strength_reduction_case40 c ty r1 r2 args v1 v2 vl - | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => op_strength_reduction_case41 r1 r2 v1 n2 - | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => op_strength_reduction_case42 r1 r2 n1 v2 - | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => op_strength_reduction_case43 r1 r2 v1 n2 - | Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil => op_strength_reduction_case44 r1 r2 n1 v2 - | op, args, vl => op_strength_reduction_default op args vl - end. - -Definition op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := - match op_strength_reduction_match op args vl with - | op_strength_reduction_case1 r1 v1 => (* Ocast8signed, r1 :: nil, v1 :: nil *) - make_cast8signed r1 v1 - | op_strength_reduction_case2 r1 v1 => (* Ocast8unsigned, r1 :: nil, v1 :: nil *) - make_cast8unsigned r1 v1 - | op_strength_reduction_case3 r1 v1 => (* Ocast16signed, r1 :: nil, v1 :: nil *) - make_cast16signed r1 v1 - | op_strength_reduction_case4 r1 v1 => (* Ocast16unsigned, r1 :: nil, v1 :: nil *) - make_cast16unsigned r1 v1 - | op_strength_reduction_case5 r1 r2 v1 n2 => (* Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_addimm (Int.neg n2) r1 - | op_strength_reduction_case6 r1 r2 n1 v2 => (* Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_mulimm n1 r2 - | op_strength_reduction_case7 r1 r2 v1 n2 => (* Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_mulimm n2 r1 - | op_strength_reduction_case8 r1 r2 v1 n2 => (* Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_divimm n2 r1 r2 - | op_strength_reduction_case9 r1 r2 v1 n2 => (* Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_divuimm n2 r1 r2 - | op_strength_reduction_case10 r1 r2 v1 n2 => (* Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_moduimm n2 r1 r2 - | op_strength_reduction_case11 r1 r2 n1 v2 => (* Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_andimm n1 r2 v2 - | op_strength_reduction_case12 r1 r2 v1 n2 => (* Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_andimm n2 r1 v1 - | op_strength_reduction_case13 n r1 v1 => (* Oandimm n, r1 :: nil, v1 :: nil *) - make_andimm n r1 v1 - | op_strength_reduction_case14 r1 r2 n1 v2 => (* Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_orimm n1 r2 - | op_strength_reduction_case15 r1 r2 v1 n2 => (* Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_orimm n2 r1 - | op_strength_reduction_case16 r1 r2 n1 v2 => (* Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_xorimm n1 r2 - | op_strength_reduction_case17 r1 r2 v1 n2 => (* Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_xorimm n2 r1 - | op_strength_reduction_case18 r1 r2 v1 n2 => (* Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shlimm n2 r1 r2 - | op_strength_reduction_case19 r1 r2 v1 n2 => (* Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shrimm n2 r1 r2 - | op_strength_reduction_case20 r1 r2 v1 n2 => (* Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shruimm n2 r1 r2 - | op_strength_reduction_case21 addr args vl => (* Olea addr, args, vl *) - let (addr', args') := addr_strength_reduction_32 addr args vl in (Olea addr', args') - | op_strength_reduction_case22 r1 r2 v1 n2 => (* Osubl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_addlimm (Int64.neg n2) r1 - | op_strength_reduction_case23 r1 r2 n1 v2 => (* Omull, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - make_mullimm n1 r2 - | op_strength_reduction_case24 r1 r2 v1 n2 => (* Omull, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_mullimm n2 r1 - | op_strength_reduction_case25 r1 r2 v1 n2 => (* Odivl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_divlimm n2 r1 r2 - | op_strength_reduction_case26 r1 r2 v1 n2 => (* Odivlu, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_divluimm n2 r1 r2 - | op_strength_reduction_case27 r1 r2 v1 n2 => (* Omodlu, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_modluimm n2 r1 r2 - | op_strength_reduction_case28 r1 r2 n1 v2 => (* Oandl, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - make_andlimm n1 r2 v2 - | op_strength_reduction_case29 r1 r2 v1 n2 => (* Oandl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_andlimm n2 r1 v1 - | op_strength_reduction_case30 n r1 v1 => (* Oandlimm n, r1 :: nil, v1 :: nil *) - make_andlimm n r1 v1 - | op_strength_reduction_case31 r1 r2 n1 v2 => (* Oorl, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - make_orlimm n1 r2 - | op_strength_reduction_case32 r1 r2 v1 n2 => (* Oorl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_orlimm n2 r1 - | op_strength_reduction_case33 r1 r2 n1 v2 => (* Oxorl, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - make_xorlimm n1 r2 - | op_strength_reduction_case34 r1 r2 v1 n2 => (* Oxorl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_xorlimm n2 r1 - | op_strength_reduction_case35 r1 r2 v1 n2 => (* Oshll, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shllimm n2 r1 r2 - | op_strength_reduction_case36 r1 r2 v1 n2 => (* Oshrl, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shrlimm n2 r1 r2 - | op_strength_reduction_case37 r1 r2 v1 n2 => (* Oshrlu, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shrluimm n2 r1 r2 - | op_strength_reduction_case38 addr args vl => (* Oleal addr, args, vl *) - let (addr', args') := addr_strength_reduction_64 addr args vl in (Oleal addr', args') - | op_strength_reduction_case39 c args vl => (* Ocmp c, args, vl *) - make_cmp c args vl - | op_strength_reduction_case40 c ty r1 r2 args v1 v2 vl => (* Osel c ty, r1 :: r2 :: args, v1 :: v2 :: vl *) - make_select c ty r1 r2 args vl - | op_strength_reduction_case41 r1 r2 v1 n2 => (* Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil *) - make_mulfimm n2 r1 r1 r2 - | op_strength_reduction_case42 r1 r2 n1 v2 => (* Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil *) - make_mulfimm n1 r2 r1 r2 - | op_strength_reduction_case43 r1 r2 v1 n2 => (* Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil *) - make_mulfsimm n2 r1 r1 r2 - | op_strength_reduction_case44 r1 r2 n1 v2 => (* Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil *) - make_mulfsimm n1 r2 r1 r2 - | op_strength_reduction_default op args vl => - (op, args) - end. - diff --git a/verilog/ConstpropOp.vp b/verilog/ConstpropOp.vp index ada8d54a..dd4b839a 100644 --- a/verilog/ConstpropOp.vp +++ b/verilog/ConstpropOp.vp @@ -17,11 +17,10 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats. Require Import Op Registers. Require Import ValueDomain ValueAOp. +Require SelectOp. (** * Converting known values to constants *) -Parameter symbol_is_external: ident -> bool. (**r See [SelectOp] *) - Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a. Definition const_for_result (a: aval) : option operation := @@ -31,7 +30,7 @@ Definition const_for_result (a: aval) : option operation := | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None | Ptr(Gl id ofs) => - if symbol_is_external id then + if SelectOp.symbol_is_external id then if Ptrofs.eq ofs Ptrofs.zero then Some (Oindirectsymbol id) else None else Some (Olea_ptr (Aglobal id ofs)) diff --git a/verilog/ConstpropOpproof.v b/verilog/ConstpropOpproof.v index c0bdaa76..09c6e91b 100644 --- a/verilog/ConstpropOpproof.v +++ b/verilog/ConstpropOpproof.v @@ -107,7 +107,7 @@ Proof. - (* pointer *) destruct p; try discriminate; SimplVM. + (* global *) - destruct (symbol_is_external id). + destruct (SelectOp.symbol_is_external id). * revert H2; predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero; intros EQ; inv EQ. exists (Genv.symbol_address ge id Ptrofs.zero); auto. * inv H2. exists (Genv.symbol_address ge id ofs); split. diff --git a/verilog/Conventions1.v b/verilog/Conventions1.v index 592acd72..b6fb2620 100644 --- a/verilog/Conventions1.v +++ b/verilog/Conventions1.v @@ -15,6 +15,7 @@ Require Import Coqlib Decidableplus. Require Import AST Machregs Locations. +Require Import Errors. (** * Classification of machine registers *) @@ -26,45 +27,49 @@ Require Import AST Machregs Locations. We follow the x86-32 and x86-64 application binary interfaces (ABI) in our choice of callee- and caller-save registers. *) - + Definition is_callee_save (r: mreg) : bool := match r with | AX | CX | DX => false | BX | BP => true - | SI | DI => negb Archi.ptr64 (**r callee-save in 32 bits but not in 64 bits *) + | SI | DI => negb Archi.ptr64 || Archi.win64 (**r callee-save in ELF 64 bits *) | R8 | R9 | R10 | R11 => false | R12 | R13 | R14 | R15 => true | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => false - | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => false + | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => Archi.win64 | FP0 => false end. Definition int_caller_save_regs := if Archi.ptr64 - then AX :: CX :: DX :: SI :: DI :: R8 :: R9 :: R10 :: R11 :: nil + then if Archi.win64 + then AX :: CX :: DX :: R8 :: R9 :: R10 :: R11 :: nil + else AX :: CX :: DX :: SI :: DI :: R8 :: R9 :: R10 :: R11 :: nil else AX :: CX :: DX :: nil. Definition float_caller_save_regs := if Archi.ptr64 - then X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: - X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil + then if Archi.win64 + then X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: nil + else X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: + X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil else X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. Definition int_callee_save_regs := if Archi.ptr64 - then BX :: BP :: R12 :: R13 :: R14 :: R15 :: nil + then if Archi.win64 + then BX :: SI :: DI :: BP :: R12 :: R13 :: R14 :: R15 :: nil + else BX :: BP :: R12 :: R13 :: R14 :: R15 :: nil else BX :: SI :: DI :: BP :: nil. -Definition float_callee_save_regs : list mreg := nil. +Definition float_callee_save_regs := + if Archi.ptr64 && Archi.win64 + then X6 :: X7 :: X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil + else nil. Definition destroyed_at_call := List.filter (fun r => negb (is_callee_save r)) all_mregs. -Definition dummy_int_reg := AX. (**r Used in [Regalloc]. *) -Definition dummy_float_reg := X0. (**r Used in [Regalloc]. *) - -Definition callee_save_type := mreg_type. - Definition is_float_reg (r: mreg) := match r with | AX | BX | CX | DX | SI | DI | BP @@ -73,6 +78,11 @@ Definition is_float_reg (r: mreg) := | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 | FP0 => true end. +Definition dummy_int_reg := AX. (**r Used in [Regalloc]. *) +Definition dummy_float_reg := X0. (**r Used in [Regalloc]. *) + +Definition callee_save_type := mreg_type. + (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -181,7 +191,7 @@ Fixpoint loc_arguments_32 :: loc_arguments_32 tys (ofs + typesize ty) end. -(** In the x86-64 ABI: +(** In the x86-64 ELF ABI: - The first 6 integer arguments are passed in registers [DI], [SI], [DX], [CX], [R8], [R9]. - The first 8 floating-point arguments are passed in registers [X0] to [X7]. - Extra arguments are passed on the stack, in [Outgoing] slots. @@ -189,26 +199,62 @@ Fixpoint loc_arguments_32 of data is used in a slot. *) -Definition int_param_regs := DI :: SI :: DX :: CX :: R8 :: R9 :: nil. -Definition float_param_regs := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. +Definition int_param_regs_elf64 := DI :: SI :: DX :: CX :: R8 :: R9 :: nil. +Definition float_param_regs_elf64 := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. -Fixpoint loc_arguments_64 +Fixpoint loc_arguments_elf64 (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list (rpair loc) := match tyl with | nil => nil | (Tint | Tlong | Tany32 | Tany64) as ty :: tys => - match list_nth_z int_param_regs ir with + match list_nth_z int_param_regs_elf64 ir with + | None => + One (S Outgoing ofs ty) :: loc_arguments_elf64 tys ir fr (ofs + 2) + | Some ireg => + One (R ireg) :: loc_arguments_elf64 tys (ir + 1) fr ofs + end + | (Tfloat | Tsingle) as ty :: tys => + match list_nth_z float_param_regs_elf64 fr with + | None => + One (S Outgoing ofs ty) :: loc_arguments_elf64 tys ir fr (ofs + 2) + | Some freg => + One (R freg) :: loc_arguments_elf64 tys ir (fr + 1) ofs + end + end. + +(** In the x86-64 Win64 ABI: +- The first 4 arguments are passed in registers [RCX], [RDX], [R8], and [R9] + (for integer arguments) and [X0] to [X3] (for floating-point arguments). + Each argument "burns" both an integer register and a FP integer. +- The first 8 floating-point arguments are passed in registers [X0] to [X7]. +- Extra arguments are passed on the stack, in [Outgoing] slots. + Consecutive stack slots are separated by 8 bytes, even if only 4 bytes + of data is used in a slot. +- Four 8-byte words are always reserved at the bottom of the outgoing area + so that the callee can use them to save the registers containing the + first four arguments. This is handled in the Stacking phase. +*) + +Definition int_param_regs_win64 := CX :: DX :: R8 :: R9 :: nil. +Definition float_param_regs_win64 := X0 :: X1 :: X2 :: X3 :: nil. + +Fixpoint loc_arguments_win64 + (tyl: list typ) (r ofs: Z) {struct tyl} : list (rpair loc) := + match tyl with + | nil => nil + | (Tint | Tlong | Tany32 | Tany64) as ty :: tys => + match list_nth_z int_param_regs_win64 r with | None => - One (S Outgoing ofs ty) :: loc_arguments_64 tys ir fr (ofs + 2) + One (S Outgoing ofs ty) :: loc_arguments_win64 tys r (ofs + 2) | Some ireg => - One (R ireg) :: loc_arguments_64 tys (ir + 1) fr ofs + One (R ireg) :: loc_arguments_win64 tys (r + 1) ofs end | (Tfloat | Tsingle) as ty :: tys => - match list_nth_z float_param_regs fr with + match list_nth_z float_param_regs_win64 r with | None => - One (S Outgoing ofs ty) :: loc_arguments_64 tys ir fr (ofs + 2) + One (S Outgoing ofs ty) :: loc_arguments_win64 tys r (ofs + 2) | Some freg => - One (R freg) :: loc_arguments_64 tys ir (fr + 1) ofs + One (R freg) :: loc_arguments_win64 tys (r + 1) ofs end end. @@ -217,7 +263,9 @@ Fixpoint loc_arguments_64 Definition loc_arguments (s: signature) : list (rpair loc) := if Archi.ptr64 - then loc_arguments_64 s.(sig_args) 0 0 0 + then if Archi.win64 + then loc_arguments_win64 s.(sig_args) 0 0 + else loc_arguments_elf64 s.(sig_args) 0 0 0 else loc_arguments_32 s.(sig_args) 0. (** Argument locations are either caller-save registers or [Outgoing] @@ -236,9 +284,16 @@ Definition loc_argument_32_charact (ofs: Z) (l: loc) : Prop := | _ => False end. -Definition loc_argument_64_charact (ofs: Z) (l: loc) : Prop := +Definition loc_argument_elf64_charact (ofs: Z) (l: loc) : Prop := + match l with + | R r => In r int_param_regs_elf64 \/ In r float_param_regs_elf64 + | S Outgoing ofs' ty => ofs' >= ofs /\ (2 | ofs') + | _ => False + end. + +Definition loc_argument_win64_charact (ofs: Z) (l: loc) : Prop := match l with - | R r => In r int_param_regs \/ In r float_param_regs + | R r => In r int_param_regs_win64 \/ In r float_param_regs_win64 | S Outgoing ofs' ty => ofs' >= ofs /\ (2 | ofs') | _ => False end. @@ -258,37 +313,75 @@ Proof. * destruct H; split; eapply X; eauto; lia. Qed. -Remark loc_arguments_64_charact: +Remark loc_arguments_elf64_charact: forall tyl ir fr ofs p, - In p (loc_arguments_64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_64_charact ofs) p. + In p (loc_arguments_elf64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_elf64_charact ofs) p. +Proof. + assert (X: forall ofs1 ofs2 l, loc_argument_elf64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_elf64_charact ofs1 l). + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_elf64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_elf64_charact ofs1) p). + { destruct p; simpl; intuition eauto. } + assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). + { intros. apply Z.divide_add_r; auto. apply Z.divide_refl. } +Opaque list_nth_z. + induction tyl; simpl loc_arguments_elf64; intros. + elim H. + assert (A: forall ty, In p + match list_nth_z int_param_regs_elf64 ir with + | Some ireg => One (R ireg) :: loc_arguments_elf64 tyl (ir + 1) fr ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_elf64 tyl ir fr (ofs + 2) + end -> + forall_rpair (loc_argument_elf64_charact ofs) p). + { intros. destruct (list_nth_z int_param_regs_elf64 ir) as [r|] eqn:E; destruct H1. + subst. left. eapply list_nth_z_in; eauto. + eapply IHtyl; eauto. + subst. split. lia. assumption. + eapply Y; eauto. lia. } + assert (B: forall ty, In p + match list_nth_z float_param_regs_elf64 fr with + | Some ireg => One (R ireg) :: loc_arguments_elf64 tyl ir (fr + 1) ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_elf64 tyl ir fr (ofs + 2) + end -> + forall_rpair (loc_argument_elf64_charact ofs) p). + { intros. destruct (list_nth_z float_param_regs_elf64 fr) as [r|] eqn:E; destruct H1. + subst. right. eapply list_nth_z_in; eauto. + eapply IHtyl; eauto. + subst. split. lia. assumption. + eapply Y; eauto. lia. } + destruct a; eauto. +Qed. + +Remark loc_arguments_win64_charact: + forall tyl r ofs p, + In p (loc_arguments_win64 tyl r ofs) -> (2 | ofs) -> forall_rpair (loc_argument_win64_charact ofs) p. Proof. - assert (X: forall ofs1 ofs2 l, loc_argument_64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_64_charact ofs1 l). + assert (X: forall ofs1 ofs2 l, loc_argument_win64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_win64_charact ofs1 l). { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } - assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_64_charact ofs1) p). + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_win64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_win64_charact ofs1) p). { destruct p; simpl; intuition eauto. } assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). { intros. apply Z.divide_add_r; auto. apply Z.divide_refl. } Opaque list_nth_z. - induction tyl; simpl loc_arguments_64; intros. + induction tyl; simpl loc_arguments_win64; intros. elim H. assert (A: forall ty, In p - match list_nth_z int_param_regs ir with - | Some ireg => One (R ireg) :: loc_arguments_64 tyl (ir + 1) fr ofs - | None => One (S Outgoing ofs ty) :: loc_arguments_64 tyl ir fr (ofs + 2) + match list_nth_z int_param_regs_win64 r with + | Some ireg => One (R ireg) :: loc_arguments_win64 tyl (r + 1) ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_win64 tyl r (ofs + 2) end -> - forall_rpair (loc_argument_64_charact ofs) p). - { intros. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H1. + forall_rpair (loc_argument_win64_charact ofs) p). + { intros. destruct (list_nth_z int_param_regs_win64 r) as [r'|] eqn:E; destruct H1. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. subst. split. lia. assumption. eapply Y; eauto. lia. } assert (B: forall ty, In p - match list_nth_z float_param_regs fr with - | Some ireg => One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs - | None => One (S Outgoing ofs ty) :: loc_arguments_64 tyl ir fr (ofs + 2) + match list_nth_z float_param_regs_win64 r with + | Some ireg => One (R ireg) :: loc_arguments_win64 tyl (r + 1) ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_win64 tyl r (ofs + 2) end -> - forall_rpair (loc_argument_64_charact ofs) p). - { intros. destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H1. + forall_rpair (loc_argument_win64_charact ofs) p). + { intros. destruct (list_nth_z float_param_regs_win64 r) as [r'|] eqn:E; destruct H1. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. subst. split. lia. assumption. @@ -300,18 +393,30 @@ Lemma loc_arguments_acceptable: forall (s: signature) (p: rpair loc), In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p. Proof. - unfold loc_arguments; intros. destruct Archi.ptr64 eqn:SF. -- (* 64 bits *) - assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF; decide_goal). - assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal. - assert (X: forall l, loc_argument_64_charact 0 l -> loc_argument_acceptable l). - { unfold loc_argument_64_charact, loc_argument_acceptable. + unfold loc_arguments; intros. destruct Archi.ptr64 eqn:SF; [destruct Archi.win64 eqn:W64|]. +- (* WIN 64 bits *) + assert (A: forall r, In r int_param_regs_win64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF; decide_goal). + assert (B: forall r, In r float_param_regs_win64 -> is_callee_save r = false) by (unfold is_callee_save; decide_goal). + assert (X: forall l, loc_argument_win64_charact 0 l -> loc_argument_acceptable l). + { unfold loc_argument_win64_charact, loc_argument_acceptable. + destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto. + intros [C D]. split; auto. apply Z.divide_trans with 2; auto. + exists (2 / typealign ty); destruct ty; reflexivity. + } + exploit loc_arguments_win64_charact; eauto using Z.divide_0_r. + unfold forall_rpair; destruct p; intuition auto. +- (* ELF 64 bits *) + assert (A: forall r, In r int_param_regs_elf64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF, W64; decide_goal). + assert (B: forall r, In r float_param_regs_elf64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite W64; decide_goal). + assert (X: forall l, loc_argument_elf64_charact 0 l -> loc_argument_acceptable l). + { unfold loc_argument_elf64_charact, loc_argument_acceptable. destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto. intros [C D]. split; auto. apply Z.divide_trans with 2; auto. exists (2 / typealign ty); destruct ty; reflexivity. } - exploit loc_arguments_64_charact; eauto using Z.divide_0_r. + exploit loc_arguments_elf64_charact; eauto using Z.divide_0_r. unfold forall_rpair; destruct p; intuition auto. + - (* 32 bits *) assert (X: forall l, loc_argument_32_charact 0 l -> loc_argument_acceptable l). { destruct l as [r | [] ofs ty]; simpl; intuition auto. rewrite H2; apply Z.divide_1_l. } @@ -319,15 +424,15 @@ Proof. unfold forall_rpair; destruct p; intuition auto. Qed. -Hint Resolve loc_arguments_acceptable: locs. +Global Hint Resolve loc_arguments_acceptable: locs. Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. - unfold loc_arguments; destruct Archi.ptr64; reflexivity. + unfold loc_arguments; destruct Archi.ptr64; auto; destruct Archi.win64; auto. Qed. -(** ** Normalization of function results *) +(** ** Normalization of function results and parameters *) (** In the x86 ABI, a return value of type "char" is returned in register AL, leaving the top 24 bits of EAX unspecified. diff --git a/verilog/DuplicateOpcodeHeuristic.ml b/verilog/DuplicateOpcodeHeuristic.ml new file mode 100644 index 00000000..38702e1b --- /dev/null +++ b/verilog/DuplicateOpcodeHeuristic.ml @@ -0,0 +1,41 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +(* open Camlcoq *) +open Op +open Integers + +let opcode_heuristic code cond ifso ifnot is_loop_header = + match cond with + | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with + | Clt | Cle -> Some false + | Cgt | Cge -> Some true + | _ -> None + ) else None + | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with + | Clt | Cle -> Some false + | Cgt | Cge -> Some true + | _ -> None + ) else None + | Ccompf c | Ccompfs c -> (match c with + | Ceq -> Some false + | Cne -> Some true + | _ -> None + ) + | Cnotcompf c | Cnotcompfs c -> (match c with + | Ceq -> Some true + | Cne -> Some false + | _ -> None + ) + | _ -> None diff --git a/verilog/ExpansionOracle.ml b/verilog/ExpansionOracle.ml new file mode 100644 index 00000000..3b63b80d --- /dev/null +++ b/verilog/ExpansionOracle.ml @@ -0,0 +1,17 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +open RTLpathCommon + +let expanse (sb : superblock) code pm = (code, pm) + +let find_last_node_reg c = () diff --git a/verilog/Machregsaux.ml b/verilog/Machregsaux.ml index a48749a5..840943e7 100644 --- a/verilog/Machregsaux.ml +++ b/verilog/Machregsaux.ml @@ -13,3 +13,8 @@ (** Auxiliary functions on machine registers *) let is_scratch_register r = false + +let class_of_type = function + | AST.Tint | AST.Tlong -> 0 + | AST.Tfloat | AST.Tsingle -> 1 + | AST.Tany32 | AST.Tany64 -> assert false diff --git a/verilog/Machregsaux.mli b/verilog/Machregsaux.mli index f3d52849..01b0f9fd 100644 --- a/verilog/Machregsaux.mli +++ b/verilog/Machregsaux.mli @@ -13,3 +13,5 @@ (** Auxiliary functions on machine registers *) val is_scratch_register: string -> bool + +val class_of_type: AST.typ -> int diff --git a/verilog/Op.v b/verilog/Op.v index 16d75426..caa63235 100644 --- a/verilog/Op.v +++ b/verilog/Op.v @@ -742,6 +742,42 @@ Proof with (try exact I; try reflexivity). unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I. Qed. + +Definition is_trapping_op (op : operation) := + match op with + | Odiv | Odivl | Odivu | Odivlu + | Omod | Omodl | Omodu | Omodlu + | Oshrximm _ | Oshrxlimm _ + | Ointoffloat + | Ointofsingle + | Olongoffloat + | Olongofsingle + | Osingleofint + | Osingleoflong + | Ofloatofint + | Ofloatoflong + | Olea _ | Oleal _ (* TODO this is suboptimal *) => true + | _ => false + end. + +Definition args_of_operation op := + if eq_operation op Omove + then 1%nat + else List.length (fst (type_of_operation op)). + +Lemma is_trapping_op_sound: + forall op vl sp m, + is_trapping_op op = false -> + (List.length vl) = args_of_operation op -> + eval_operation genv sp op vl m <> None. +Proof. + unfold args_of_operation. + destruct op; destruct eq_operation; intros; simpl in *; try congruence. + all: try (destruct vl as [ | vh1 vl1]; try discriminate). + all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). + all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). + all: try (destruct vl3 as [ | vh4 vl4]; try discriminate). +Qed. End SOUNDNESS. (** * Manipulating and transforming operations *) @@ -963,7 +999,7 @@ Definition is_trivial_op (op: operation) : bool := (** Operations that depend on the memory state. *) -Definition condition_depends_on_memory (c: condition) : bool := +Definition cond_depends_on_memory (c: condition) : bool := match c with | Ccompu _ => negb Archi.ptr64 | Ccompuimm _ _ => negb Archi.ptr64 @@ -974,14 +1010,14 @@ Definition condition_depends_on_memory (c: condition) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with - | Ocmp c => condition_depends_on_memory c - | Osel c ty => condition_depends_on_memory c + | Ocmp c => cond_depends_on_memory c + | Osel c ty => cond_depends_on_memory c | _ => false end. -Lemma condition_depends_on_memory_correct: +Lemma cond_depends_on_memory_correct: forall c args m1 m2, - condition_depends_on_memory c = false -> + cond_depends_on_memory c = false -> eval_condition c args m1 = eval_condition c args m2. Proof. intros until m2. @@ -995,12 +1031,36 @@ Lemma op_depends_on_memory_correct: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence; intros C. -- f_equal; f_equal; apply condition_depends_on_memory_correct; auto. +- f_equal; f_equal; apply cond_depends_on_memory_correct; auto. - destruct args; auto. destruct args; auto. - rewrite (condition_depends_on_memory_correct c args m1 m2 C). + rewrite (cond_depends_on_memory_correct c args m1 m2 C). auto. Qed. +Lemma cond_valid_pointer_eq: + forall cond args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_condition cond args m1 = eval_condition cond args m2. +Proof. + intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence. + all: repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + +Lemma op_valid_pointer_eq: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. +Proof. + intros until m2. destruct op eqn:OP; simpl; try congruence. + - intros MEM; destruct cond; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + - intro MEM; destruct c; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + (** Global variables mentioned in an operation or addressing mode *) Definition globals_addressing (addr: addressing) : list ident := @@ -1199,6 +1259,21 @@ Proof. unfold eval_addressing; intros. destruct Archi.ptr64; eauto using eval_addressing32_inj, eval_addressing64_inj. Qed. +Lemma eval_addressing_inj_none: + forall addr sp1 vl1 sp2 vl2, + (forall id ofs, + In id (globals_addressing addr) -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> + eval_addressing ge1 sp1 addr vl1 = None -> + eval_addressing ge2 sp2 addr vl2 = None. +Proof. + intros until vl2. intros Hglobal Hinjsp Hinjvl. + destruct addr; simpl in *; + inv Hinjvl; trivial; try discriminate; inv H0; trivial; try discriminate; inv H2; trivial; try discriminate. +Qed. + Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, (forall id ofs, @@ -1425,6 +1500,19 @@ Proof. destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. +Lemma eval_addressing_lessdef_none: + forall sp addr vl1 vl2, + Val.lessdef_list vl1 vl2 -> + eval_addressing genv sp addr vl1 = None -> + eval_addressing genv sp addr vl2 = None. +Proof. + intros until vl2. intros Hlessdef Heval1. + destruct addr; simpl in *; + inv Hlessdef; trivial; try discriminate; + inv H0; trivial; try discriminate; + inv H2; trivial; try discriminate. +Qed. + End EVAL_LESSDEF. (** Compatibility of the evaluation functions with memory injections. *) @@ -1477,6 +1565,19 @@ Proof. econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. +Lemma eval_addressing_inject_none: + forall addr vl1 vl2, + Val.inject_list f vl1 vl2 -> + eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = None -> + eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = None. +Proof. + intros. + rewrite eval_shift_stack_addressing. + eapply eval_addressing_inj_none with (sp1 := Vptr sp1 Ptrofs.zero); eauto. + intros. apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. +Qed. + Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, Val.inject_list f vl1 vl2 -> diff --git a/verilog/PrepassSchedulingOracle.ml b/verilog/PrepassSchedulingOracle.ml new file mode 100644 index 00000000..42a3da23 --- /dev/null +++ b/verilog/PrepassSchedulingOracle.ml @@ -0,0 +1,6 @@ +open RTL +open Registers + +(* Do not do anything *) +let schedule_sequence (seqa : (instruction*Regset.t) array) + live_regs_entry typing reference = None diff --git a/verilog/RTLpathSE_simplify.v b/verilog/RTLpathSE_simplify.v new file mode 120000 index 00000000..55bf0e52 --- /dev/null +++ b/verilog/RTLpathSE_simplify.v @@ -0,0 +1 @@ +../aarch64/RTLpathSE_simplify.v
\ No newline at end of file diff --git a/verilog/SelectLong.v b/verilog/SelectLong.v deleted file mode 100644 index 3b9df4de..00000000 --- a/verilog/SelectLong.v +++ /dev/null @@ -1,804 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Instruction selection for 64-bit integer operations *) - -Require Import Coqlib. -Require Import Compopts. -Require Import AST Integers Floats. -Require Import Op CminorSel. -Require Import SelectOp SplitLong. - -Local Open Scope cminorsel_scope. -Local Open Scope string_scope. - -Section SELECT. - -Context {hf: helper_functions}. - -Definition longconst (n: int64) : expr := - if Archi.splitlong then SplitLong.longconst n else Eop (Olongconst n) Enil. - -Definition is_longconst (e: expr) := - if Archi.splitlong then SplitLong.is_longconst e else - match e with - | Eop (Olongconst n) Enil => Some n - | _ => None - end. - -Definition intoflong (e: expr) := - if Archi.splitlong then SplitLong.intoflong e else - match is_longconst e with - | Some n => Eop (Ointconst (Int.repr (Int64.unsigned n))) Enil - | None => Eop Olowlong (e ::: Enil) - end. - -Definition longofint (e: expr) := - if Archi.splitlong then SplitLong.longofint e else - match is_intconst e with - | Some n => longconst (Int64.repr (Int.signed n)) - | None => Eop Ocast32signed (e ::: Enil) - end. - -Definition longofintu (e: expr) := - if Archi.splitlong then SplitLong.longofintu e else - match is_intconst e with - | Some n => longconst (Int64.repr (Int.unsigned n)) - | None => Eop Ocast32unsigned (e ::: Enil) - end. - -(** Original definition: -<< -Nondetfunction notl (e: expr) := - if Archi.splitlong then SplitLong.notl e else - match e with - | Eop (Olongconst n) Enil => longconst (Int64.not n) - | Eop Onotl (t1:::Enil) => t1 - | _ => Eop Onotl (e:::Enil) - end. ->> -*) - -Inductive notl_cases: forall (e: expr), Type := - | notl_case1: forall n, notl_cases (Eop (Olongconst n) Enil) - | notl_case2: forall t1, notl_cases (Eop Onotl (t1:::Enil)) - | notl_default: forall (e: expr), notl_cases e. - -Definition notl_match (e: expr) := - match e as zz1 return notl_cases zz1 with - | Eop (Olongconst n) Enil => notl_case1 n - | Eop Onotl (t1:::Enil) => notl_case2 t1 - | e => notl_default e - end. - -Definition notl (e: expr) := - if Archi.splitlong then SplitLong.notl e else match notl_match e with - | notl_case1 n => (* Eop (Olongconst n) Enil *) - longconst (Int64.not n) - | notl_case2 t1 => (* Eop Onotl (t1:::Enil) *) - t1 - | notl_default e => - Eop Onotl (e:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction andlimm (n1: int64) (e2: expr) := - if Int64.eq n1 Int64.zero then longconst Int64.zero else - if Int64.eq n1 Int64.mone then e2 else - match e2 with - | Eop (Olongconst n2) Enil => - longconst (Int64.and n1 n2) - | Eop (Oandlimm n2) (t2:::Enil) => - Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil) - | _ => - Eop (Oandlimm n1) (e2:::Enil) - end. ->> -*) - -Inductive andlimm_cases: forall (e2: expr), Type := - | andlimm_case1: forall n2, andlimm_cases (Eop (Olongconst n2) Enil) - | andlimm_case2: forall n2 t2, andlimm_cases (Eop (Oandlimm n2) (t2:::Enil)) - | andlimm_default: forall (e2: expr), andlimm_cases e2. - -Definition andlimm_match (e2: expr) := - match e2 as zz1 return andlimm_cases zz1 with - | Eop (Olongconst n2) Enil => andlimm_case1 n2 - | Eop (Oandlimm n2) (t2:::Enil) => andlimm_case2 n2 t2 - | e2 => andlimm_default e2 - end. - -Definition andlimm (n1: int64) (e2: expr) := - if Int64.eq n1 Int64.zero then longconst Int64.zero else if Int64.eq n1 Int64.mone then e2 else match andlimm_match e2 with - | andlimm_case1 n2 => (* Eop (Olongconst n2) Enil *) - longconst (Int64.and n1 n2) - | andlimm_case2 n2 t2 => (* Eop (Oandlimm n2) (t2:::Enil) *) - Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil) - | andlimm_default e2 => - Eop (Oandlimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction andl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.andl e1 e2 else - match e1, e2 with - | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2 - | t1, Eop (Olongconst n2) Enil => andlimm n2 t1 - | _, _ => Eop Oandl (e1:::e2:::Enil) - end. ->> -*) - -Inductive andl_cases: forall (e1: expr) (e2: expr), Type := - | andl_case1: forall n1 t2, andl_cases (Eop (Olongconst n1) Enil) (t2) - | andl_case2: forall t1 n2, andl_cases (t1) (Eop (Olongconst n2) Enil) - | andl_default: forall (e1: expr) (e2: expr), andl_cases e1 e2. - -Definition andl_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return andl_cases zz1 zz2 with - | Eop (Olongconst n1) Enil, t2 => andl_case1 n1 t2 - | t1, Eop (Olongconst n2) Enil => andl_case2 t1 n2 - | e1, e2 => andl_default e1 e2 - end. - -Definition andl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.andl e1 e2 else match andl_match e1 e2 with - | andl_case1 n1 t2 => (* Eop (Olongconst n1) Enil, t2 *) - andlimm n1 t2 - | andl_case2 t1 n2 => (* t1, Eop (Olongconst n2) Enil *) - andlimm n2 t1 - | andl_default e1 e2 => - Eop Oandl (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction orlimm (n1: int64) (e2: expr) := - if Int64.eq n1 Int64.zero then e2 else - if Int64.eq n1 Int64.mone then longconst Int64.mone else - match e2 with - | Eop (Olongconst n2) Enil => longconst (Int64.or n1 n2) - | Eop (Oorlimm n2) (t2:::Enil) => Eop (Oorlimm (Int64.or n1 n2)) (t2:::Enil) - | _ => Eop (Oorlimm n1) (e2:::Enil) - end. ->> -*) - -Inductive orlimm_cases: forall (e2: expr), Type := - | orlimm_case1: forall n2, orlimm_cases (Eop (Olongconst n2) Enil) - | orlimm_case2: forall n2 t2, orlimm_cases (Eop (Oorlimm n2) (t2:::Enil)) - | orlimm_default: forall (e2: expr), orlimm_cases e2. - -Definition orlimm_match (e2: expr) := - match e2 as zz1 return orlimm_cases zz1 with - | Eop (Olongconst n2) Enil => orlimm_case1 n2 - | Eop (Oorlimm n2) (t2:::Enil) => orlimm_case2 n2 t2 - | e2 => orlimm_default e2 - end. - -Definition orlimm (n1: int64) (e2: expr) := - if Int64.eq n1 Int64.zero then e2 else if Int64.eq n1 Int64.mone then longconst Int64.mone else match orlimm_match e2 with - | orlimm_case1 n2 => (* Eop (Olongconst n2) Enil *) - longconst (Int64.or n1 n2) - | orlimm_case2 n2 t2 => (* Eop (Oorlimm n2) (t2:::Enil) *) - Eop (Oorlimm (Int64.or n1 n2)) (t2:::Enil) - | orlimm_default e2 => - Eop (Oorlimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction orl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.orl e1 e2 else - match e1, e2 with - | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2 - | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 - | Eop (Oshllimm n1) (t1:::Enil), Eop (Oshrluimm n2) (t2:::Enil) => - if Int.eq (Int.add n1 n2) Int64.iwordsize' && same_expr_pure t1 t2 - then Eop (Ororlimm n2) (t1:::Enil) - else Eop Oorl (e1:::e2:::Enil) - | Eop (Oshrluimm n2) (t2:::Enil), Eop (Oshllimm n1) (t1:::Enil) => - if Int.eq (Int.add n1 n2) Int64.iwordsize' && same_expr_pure t1 t2 - then Eop (Ororlimm n2) (t1:::Enil) - else Eop Oorl (e1:::e2:::Enil) - | _, _ => - Eop Oorl (e1:::e2:::Enil) - end. ->> -*) - -Inductive orl_cases: forall (e1: expr) (e2: expr), Type := - | orl_case1: forall n1 t2, orl_cases (Eop (Olongconst n1) Enil) (t2) - | orl_case2: forall t1 n2, orl_cases (t1) (Eop (Olongconst n2) Enil) - | orl_case3: forall n1 t1 n2 t2, orl_cases (Eop (Oshllimm n1) (t1:::Enil)) (Eop (Oshrluimm n2) (t2:::Enil)) - | orl_case4: forall n2 t2 n1 t1, orl_cases (Eop (Oshrluimm n2) (t2:::Enil)) (Eop (Oshllimm n1) (t1:::Enil)) - | orl_default: forall (e1: expr) (e2: expr), orl_cases e1 e2. - -Definition orl_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return orl_cases zz1 zz2 with - | Eop (Olongconst n1) Enil, t2 => orl_case1 n1 t2 - | t1, Eop (Olongconst n2) Enil => orl_case2 t1 n2 - | Eop (Oshllimm n1) (t1:::Enil), Eop (Oshrluimm n2) (t2:::Enil) => orl_case3 n1 t1 n2 t2 - | Eop (Oshrluimm n2) (t2:::Enil), Eop (Oshllimm n1) (t1:::Enil) => orl_case4 n2 t2 n1 t1 - | e1, e2 => orl_default e1 e2 - end. - -Definition orl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.orl e1 e2 else match orl_match e1 e2 with - | orl_case1 n1 t2 => (* Eop (Olongconst n1) Enil, t2 *) - orlimm n1 t2 - | orl_case2 t1 n2 => (* t1, Eop (Olongconst n2) Enil *) - orlimm n2 t1 - | orl_case3 n1 t1 n2 t2 => (* Eop (Oshllimm n1) (t1:::Enil), Eop (Oshrluimm n2) (t2:::Enil) *) - if Int.eq (Int.add n1 n2) Int64.iwordsize' && same_expr_pure t1 t2 then Eop (Ororlimm n2) (t1:::Enil) else Eop Oorl (e1:::e2:::Enil) - | orl_case4 n2 t2 n1 t1 => (* Eop (Oshrluimm n2) (t2:::Enil), Eop (Oshllimm n1) (t1:::Enil) *) - if Int.eq (Int.add n1 n2) Int64.iwordsize' && same_expr_pure t1 t2 then Eop (Ororlimm n2) (t1:::Enil) else Eop Oorl (e1:::e2:::Enil) - | orl_default e1 e2 => - Eop Oorl (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction xorlimm (n1: int64) (e2: expr) := - if Int64.eq n1 Int64.zero then e2 else - if Int64.eq n1 Int64.mone then notl e2 else - match e2 with - | Eop (Olongconst n2) Enil => longconst (Int64.xor n1 n2) - | Eop (Oxorlimm n2) (t2:::Enil) => Eop (Oxorlimm (Int64.xor n1 n2)) (t2:::Enil) - | Eop Onotl (t2:::Enil) => Eop (Oxorlimm (Int64.not n1)) (t2:::Enil) - | _ => Eop (Oxorlimm n1) (e2:::Enil) - end. ->> -*) - -Inductive xorlimm_cases: forall (e2: expr), Type := - | xorlimm_case1: forall n2, xorlimm_cases (Eop (Olongconst n2) Enil) - | xorlimm_case2: forall n2 t2, xorlimm_cases (Eop (Oxorlimm n2) (t2:::Enil)) - | xorlimm_case3: forall t2, xorlimm_cases (Eop Onotl (t2:::Enil)) - | xorlimm_default: forall (e2: expr), xorlimm_cases e2. - -Definition xorlimm_match (e2: expr) := - match e2 as zz1 return xorlimm_cases zz1 with - | Eop (Olongconst n2) Enil => xorlimm_case1 n2 - | Eop (Oxorlimm n2) (t2:::Enil) => xorlimm_case2 n2 t2 - | Eop Onotl (t2:::Enil) => xorlimm_case3 t2 - | e2 => xorlimm_default e2 - end. - -Definition xorlimm (n1: int64) (e2: expr) := - if Int64.eq n1 Int64.zero then e2 else if Int64.eq n1 Int64.mone then notl e2 else match xorlimm_match e2 with - | xorlimm_case1 n2 => (* Eop (Olongconst n2) Enil *) - longconst (Int64.xor n1 n2) - | xorlimm_case2 n2 t2 => (* Eop (Oxorlimm n2) (t2:::Enil) *) - Eop (Oxorlimm (Int64.xor n1 n2)) (t2:::Enil) - | xorlimm_case3 t2 => (* Eop Onotl (t2:::Enil) *) - Eop (Oxorlimm (Int64.not n1)) (t2:::Enil) - | xorlimm_default e2 => - Eop (Oxorlimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction xorl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.xorl e1 e2 else - match e1, e2 with - | Eop (Olongconst n1) Enil, t2 => xorlimm n1 t2 - | t1, Eop (Olongconst n2) Enil => xorlimm n2 t1 - | _, _ => Eop Oxorl (e1:::e2:::Enil) - end. ->> -*) - -Inductive xorl_cases: forall (e1: expr) (e2: expr), Type := - | xorl_case1: forall n1 t2, xorl_cases (Eop (Olongconst n1) Enil) (t2) - | xorl_case2: forall t1 n2, xorl_cases (t1) (Eop (Olongconst n2) Enil) - | xorl_default: forall (e1: expr) (e2: expr), xorl_cases e1 e2. - -Definition xorl_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return xorl_cases zz1 zz2 with - | Eop (Olongconst n1) Enil, t2 => xorl_case1 n1 t2 - | t1, Eop (Olongconst n2) Enil => xorl_case2 t1 n2 - | e1, e2 => xorl_default e1 e2 - end. - -Definition xorl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.xorl e1 e2 else match xorl_match e1 e2 with - | xorl_case1 n1 t2 => (* Eop (Olongconst n1) Enil, t2 *) - xorlimm n1 t2 - | xorl_case2 t1 n2 => (* t1, Eop (Olongconst n2) Enil *) - xorlimm n2 t1 - | xorl_default e1 e2 => - Eop Oxorl (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shllimm (e1: expr) (n: int) := - if Archi.splitlong then SplitLong.shllimm e1 n else - if Int.eq n Int.zero then e1 else - if negb (Int.ltu n Int64.iwordsize') then - Eop Oshll (e1:::Eop (Ointconst n) Enil:::Enil) - else - match e1 with - | Eop (Olongconst n1) Enil => - Eop (Olongconst(Int64.shl' n1 n)) Enil - | Eop (Oshllimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int64.iwordsize' - then Eop (Oshllimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshllimm n) (e1:::Enil) - | Eop (Oleal (Aindexed n1)) (t1:::Enil) => - if shift_is_scale n - then Eop (Oleal (Ascaled (Int64.unsigned (Int64.shl' Int64.one n)) - (Int64.unsigned (Int64.shl' (Int64.repr n1) n)))) (t1:::Enil) - else Eop (Oshllimm n) (e1:::Enil) - | _ => - if shift_is_scale n - then Eop (Oleal (Ascaled (Int64.unsigned (Int64.shl' Int64.one n)) 0)) (e1:::Enil) - else Eop (Oshllimm n) (e1:::Enil) - end. ->> -*) - -Inductive shllimm_cases: forall (e1: expr) , Type := - | shllimm_case1: forall n1, shllimm_cases (Eop (Olongconst n1) Enil) - | shllimm_case2: forall n1 t1, shllimm_cases (Eop (Oshllimm n1) (t1:::Enil)) - | shllimm_case3: forall n1 t1, shllimm_cases (Eop (Oleal (Aindexed n1)) (t1:::Enil)) - | shllimm_default: forall (e1: expr) , shllimm_cases e1. - -Definition shllimm_match (e1: expr) := - match e1 as zz1 return shllimm_cases zz1 with - | Eop (Olongconst n1) Enil => shllimm_case1 n1 - | Eop (Oshllimm n1) (t1:::Enil) => shllimm_case2 n1 t1 - | Eop (Oleal (Aindexed n1)) (t1:::Enil) => shllimm_case3 n1 t1 - | e1 => shllimm_default e1 - end. - -Definition shllimm (e1: expr) (n: int) := - if Archi.splitlong then SplitLong.shllimm e1 n else if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int64.iwordsize') then Eop Oshll (e1:::Eop (Ointconst n) Enil:::Enil) else match shllimm_match e1 with - | shllimm_case1 n1 => (* Eop (Olongconst n1) Enil *) - Eop (Olongconst(Int64.shl' n1 n)) Enil - | shllimm_case2 n1 t1 => (* Eop (Oshllimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int64.iwordsize' then Eop (Oshllimm (Int.add n n1)) (t1:::Enil) else Eop (Oshllimm n) (e1:::Enil) - | shllimm_case3 n1 t1 => (* Eop (Oleal (Aindexed n1)) (t1:::Enil) *) - if shift_is_scale n then Eop (Oleal (Ascaled (Int64.unsigned (Int64.shl' Int64.one n)) (Int64.unsigned (Int64.shl' (Int64.repr n1) n)))) (t1:::Enil) else Eop (Oshllimm n) (e1:::Enil) - | shllimm_default e1 => - if shift_is_scale n then Eop (Oleal (Ascaled (Int64.unsigned (Int64.shl' Int64.one n)) 0)) (e1:::Enil) else Eop (Oshllimm n) (e1:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shrluimm (e1: expr) (n: int) := - if Archi.splitlong then SplitLong.shrluimm e1 n else - if Int.eq n Int.zero then e1 else - if negb (Int.ltu n Int64.iwordsize') then - Eop Oshrlu (e1:::Eop (Ointconst n) Enil:::Enil) - else - match e1 with - | Eop (Olongconst n1) Enil => - Eop (Olongconst(Int64.shru' n1 n)) Enil - | Eop (Oshrluimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int64.iwordsize' - then Eop (Oshrluimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshrluimm n) (e1:::Enil) - | _ => - Eop (Oshrluimm n) (e1:::Enil) - end. ->> -*) - -Inductive shrluimm_cases: forall (e1: expr) , Type := - | shrluimm_case1: forall n1, shrluimm_cases (Eop (Olongconst n1) Enil) - | shrluimm_case2: forall n1 t1, shrluimm_cases (Eop (Oshrluimm n1) (t1:::Enil)) - | shrluimm_default: forall (e1: expr) , shrluimm_cases e1. - -Definition shrluimm_match (e1: expr) := - match e1 as zz1 return shrluimm_cases zz1 with - | Eop (Olongconst n1) Enil => shrluimm_case1 n1 - | Eop (Oshrluimm n1) (t1:::Enil) => shrluimm_case2 n1 t1 - | e1 => shrluimm_default e1 - end. - -Definition shrluimm (e1: expr) (n: int) := - if Archi.splitlong then SplitLong.shrluimm e1 n else if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int64.iwordsize') then Eop Oshrlu (e1:::Eop (Ointconst n) Enil:::Enil) else match shrluimm_match e1 with - | shrluimm_case1 n1 => (* Eop (Olongconst n1) Enil *) - Eop (Olongconst(Int64.shru' n1 n)) Enil - | shrluimm_case2 n1 t1 => (* Eop (Oshrluimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int64.iwordsize' then Eop (Oshrluimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrluimm n) (e1:::Enil) - | shrluimm_default e1 => - Eop (Oshrluimm n) (e1:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shrlimm (e1: expr) (n: int) := - if Archi.splitlong then SplitLong.shrlimm e1 n else - if Int.eq n Int.zero then e1 else - if negb (Int.ltu n Int64.iwordsize') then - Eop Oshrl (e1:::Eop (Ointconst n) Enil:::Enil) - else - match e1 with - | Eop (Olongconst n1) Enil => - Eop (Olongconst(Int64.shr' n1 n)) Enil - | Eop (Oshrlimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int64.iwordsize' - then Eop (Oshrlimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshrlimm n) (e1:::Enil) - | _ => - Eop (Oshrlimm n) (e1:::Enil) - end. ->> -*) - -Inductive shrlimm_cases: forall (e1: expr) , Type := - | shrlimm_case1: forall n1, shrlimm_cases (Eop (Olongconst n1) Enil) - | shrlimm_case2: forall n1 t1, shrlimm_cases (Eop (Oshrlimm n1) (t1:::Enil)) - | shrlimm_default: forall (e1: expr) , shrlimm_cases e1. - -Definition shrlimm_match (e1: expr) := - match e1 as zz1 return shrlimm_cases zz1 with - | Eop (Olongconst n1) Enil => shrlimm_case1 n1 - | Eop (Oshrlimm n1) (t1:::Enil) => shrlimm_case2 n1 t1 - | e1 => shrlimm_default e1 - end. - -Definition shrlimm (e1: expr) (n: int) := - if Archi.splitlong then SplitLong.shrlimm e1 n else if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int64.iwordsize') then Eop Oshrl (e1:::Eop (Ointconst n) Enil:::Enil) else match shrlimm_match e1 with - | shrlimm_case1 n1 => (* Eop (Olongconst n1) Enil *) - Eop (Olongconst(Int64.shr' n1 n)) Enil - | shrlimm_case2 n1 t1 => (* Eop (Oshrlimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int64.iwordsize' then Eop (Oshrlimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrlimm n) (e1:::Enil) - | shrlimm_default e1 => - Eop (Oshrlimm n) (e1:::Enil) - end. - - -Definition shll (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.shll e1 e2 else - match is_intconst e2 with - | Some n2 => shllimm e1 n2 - | None => Eop Oshll (e1:::e2:::Enil) - end. - -Definition shrl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.shrl e1 e2 else - match is_intconst e2 with - | Some n2 => shrlimm e1 n2 - | None => Eop Oshrl (e1:::e2:::Enil) - end. - -Definition shrlu (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.shrlu e1 e2 else - match is_intconst e2 with - | Some n2 => shrluimm e1 n2 - | _ => Eop Oshrlu (e1:::e2:::Enil) - end. - -(** Original definition: -<< -Nondetfunction addlimm (n: int64) (e: expr) := - if Int64.eq n Int64.zero then e else - match e with - | Eop (Olongconst m) Enil => longconst (Int64.add n m) - | Eop (Oleal addr) args => Eop (Oleal (offset_addressing_total addr (Int64.signed n))) args - | _ => Eop (Oleal (Aindexed (Int64.signed n))) (e ::: Enil) - end. ->> -*) - -Inductive addlimm_cases: forall (e: expr), Type := - | addlimm_case1: forall m, addlimm_cases (Eop (Olongconst m) Enil) - | addlimm_case2: forall addr args, addlimm_cases (Eop (Oleal addr) args) - | addlimm_default: forall (e: expr), addlimm_cases e. - -Definition addlimm_match (e: expr) := - match e as zz1 return addlimm_cases zz1 with - | Eop (Olongconst m) Enil => addlimm_case1 m - | Eop (Oleal addr) args => addlimm_case2 addr args - | e => addlimm_default e - end. - -Definition addlimm (n: int64) (e: expr) := - if Int64.eq n Int64.zero then e else match addlimm_match e with - | addlimm_case1 m => (* Eop (Olongconst m) Enil *) - longconst (Int64.add n m) - | addlimm_case2 addr args => (* Eop (Oleal addr) args *) - Eop (Oleal (offset_addressing_total addr (Int64.signed n))) args - | addlimm_default e => - Eop (Oleal (Aindexed (Int64.signed n))) (e ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction addl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.addl e1 e2 else - match e1, e2 with - | Eop (Olongconst n1) Enil, t2 => addlimm n1 t2 - | t1, Eop (Olongconst n2) Enil => addlimm n2 t1 - | Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) => - Eop (Oleal (Aindexed2 (n1 + n2))) (t1:::t2:::Enil) - | Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Ascaled sc n2)) (t2:::Enil) => - Eop (Oleal (Aindexed2scaled sc (n1 + n2))) (t1:::t2:::Enil) - | Eop (Oleal (Ascaled sc n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) => - Eop (Oleal (Aindexed2scaled sc (n1 + n2))) (t2:::t1:::Enil) - | Eop (Oleal (Ascaled sc n)) (t1:::Enil), t2 => - Eop (Oleal (Aindexed2scaled sc n)) (t2:::t1:::Enil) - | t1, Eop (Oleal (Ascaled sc n)) (t2:::Enil) => - Eop (Oleal (Aindexed2scaled sc n)) (t1:::t2:::Enil) - | Eop (Oleal (Aindexed n)) (t1:::Enil), t2 => - Eop (Oleal (Aindexed2 n)) (t1:::t2:::Enil) - | t1, Eop (Oleal (Aindexed n)) (t2:::Enil) => - Eop (Oleal (Aindexed2 n)) (t1:::t2:::Enil) - | _, _ => - Eop (Oleal (Aindexed2 0)) (e1:::e2:::Enil) - end. ->> -*) - -Inductive addl_cases: forall (e1: expr) (e2: expr), Type := - | addl_case1: forall n1 t2, addl_cases (Eop (Olongconst n1) Enil) (t2) - | addl_case2: forall t1 n2, addl_cases (t1) (Eop (Olongconst n2) Enil) - | addl_case3: forall n1 t1 n2 t2, addl_cases (Eop (Oleal (Aindexed n1)) (t1:::Enil)) (Eop (Oleal (Aindexed n2)) (t2:::Enil)) - | addl_case4: forall n1 t1 sc n2 t2, addl_cases (Eop (Oleal (Aindexed n1)) (t1:::Enil)) (Eop (Oleal (Ascaled sc n2)) (t2:::Enil)) - | addl_case5: forall sc n1 t1 n2 t2, addl_cases (Eop (Oleal (Ascaled sc n1)) (t1:::Enil)) (Eop (Oleal (Aindexed n2)) (t2:::Enil)) - | addl_case6: forall sc n t1 t2, addl_cases (Eop (Oleal (Ascaled sc n)) (t1:::Enil)) (t2) - | addl_case7: forall t1 sc n t2, addl_cases (t1) (Eop (Oleal (Ascaled sc n)) (t2:::Enil)) - | addl_case8: forall n t1 t2, addl_cases (Eop (Oleal (Aindexed n)) (t1:::Enil)) (t2) - | addl_case9: forall t1 n t2, addl_cases (t1) (Eop (Oleal (Aindexed n)) (t2:::Enil)) - | addl_default: forall (e1: expr) (e2: expr), addl_cases e1 e2. - -Definition addl_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return addl_cases zz1 zz2 with - | Eop (Olongconst n1) Enil, t2 => addl_case1 n1 t2 - | t1, Eop (Olongconst n2) Enil => addl_case2 t1 n2 - | Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) => addl_case3 n1 t1 n2 t2 - | Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Ascaled sc n2)) (t2:::Enil) => addl_case4 n1 t1 sc n2 t2 - | Eop (Oleal (Ascaled sc n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) => addl_case5 sc n1 t1 n2 t2 - | Eop (Oleal (Ascaled sc n)) (t1:::Enil), t2 => addl_case6 sc n t1 t2 - | t1, Eop (Oleal (Ascaled sc n)) (t2:::Enil) => addl_case7 t1 sc n t2 - | Eop (Oleal (Aindexed n)) (t1:::Enil), t2 => addl_case8 n t1 t2 - | t1, Eop (Oleal (Aindexed n)) (t2:::Enil) => addl_case9 t1 n t2 - | e1, e2 => addl_default e1 e2 - end. - -Definition addl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.addl e1 e2 else match addl_match e1 e2 with - | addl_case1 n1 t2 => (* Eop (Olongconst n1) Enil, t2 *) - addlimm n1 t2 - | addl_case2 t1 n2 => (* t1, Eop (Olongconst n2) Enil *) - addlimm n2 t1 - | addl_case3 n1 t1 n2 t2 => (* Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) *) - Eop (Oleal (Aindexed2 (n1 + n2))) (t1:::t2:::Enil) - | addl_case4 n1 t1 sc n2 t2 => (* Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Ascaled sc n2)) (t2:::Enil) *) - Eop (Oleal (Aindexed2scaled sc (n1 + n2))) (t1:::t2:::Enil) - | addl_case5 sc n1 t1 n2 t2 => (* Eop (Oleal (Ascaled sc n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) *) - Eop (Oleal (Aindexed2scaled sc (n1 + n2))) (t2:::t1:::Enil) - | addl_case6 sc n t1 t2 => (* Eop (Oleal (Ascaled sc n)) (t1:::Enil), t2 *) - Eop (Oleal (Aindexed2scaled sc n)) (t2:::t1:::Enil) - | addl_case7 t1 sc n t2 => (* t1, Eop (Oleal (Ascaled sc n)) (t2:::Enil) *) - Eop (Oleal (Aindexed2scaled sc n)) (t1:::t2:::Enil) - | addl_case8 n t1 t2 => (* Eop (Oleal (Aindexed n)) (t1:::Enil), t2 *) - Eop (Oleal (Aindexed2 n)) (t1:::t2:::Enil) - | addl_case9 t1 n t2 => (* t1, Eop (Oleal (Aindexed n)) (t2:::Enil) *) - Eop (Oleal (Aindexed2 n)) (t1:::t2:::Enil) - | addl_default e1 e2 => - Eop (Oleal (Aindexed2 0)) (e1:::e2:::Enil) - end. - - -Definition negl (e: expr) := - if Archi.splitlong then SplitLong.negl e else - match is_longconst e with - | Some n => longconst (Int64.neg n) - | None => Eop Onegl (e ::: Enil) - end. - -(** Original definition: -<< -Nondetfunction subl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.subl e1 e2 else - match e1, e2 with - | t1, Eop (Olongconst n2) Enil => addlimm (Int64.neg n2) t1 - | Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) => - addlimm (Int64.repr (n1 - n2)) (Eop Osubl (t1:::t2:::Enil)) - | Eop (Oleal (Aindexed n1)) (t1:::Enil), t2 => - addlimm (Int64.repr n1) (Eop Osubl (t1:::t2:::Enil)) - | t1, Eop (Oleal (Aindexed n2)) (t2:::Enil) => - addlimm (Int64.repr (- n2)) (Eop Osubl (t1:::t2:::Enil)) - | _, _ => - Eop Osubl (e1:::e2:::Enil) - end. ->> -*) - -Inductive subl_cases: forall (e1: expr) (e2: expr), Type := - | subl_case1: forall t1 n2, subl_cases (t1) (Eop (Olongconst n2) Enil) - | subl_case2: forall n1 t1 n2 t2, subl_cases (Eop (Oleal (Aindexed n1)) (t1:::Enil)) (Eop (Oleal (Aindexed n2)) (t2:::Enil)) - | subl_case3: forall n1 t1 t2, subl_cases (Eop (Oleal (Aindexed n1)) (t1:::Enil)) (t2) - | subl_case4: forall t1 n2 t2, subl_cases (t1) (Eop (Oleal (Aindexed n2)) (t2:::Enil)) - | subl_default: forall (e1: expr) (e2: expr), subl_cases e1 e2. - -Definition subl_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return subl_cases zz1 zz2 with - | t1, Eop (Olongconst n2) Enil => subl_case1 t1 n2 - | Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) => subl_case2 n1 t1 n2 t2 - | Eop (Oleal (Aindexed n1)) (t1:::Enil), t2 => subl_case3 n1 t1 t2 - | t1, Eop (Oleal (Aindexed n2)) (t2:::Enil) => subl_case4 t1 n2 t2 - | e1, e2 => subl_default e1 e2 - end. - -Definition subl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.subl e1 e2 else match subl_match e1 e2 with - | subl_case1 t1 n2 => (* t1, Eop (Olongconst n2) Enil *) - addlimm (Int64.neg n2) t1 - | subl_case2 n1 t1 n2 t2 => (* Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) *) - addlimm (Int64.repr (n1 - n2)) (Eop Osubl (t1:::t2:::Enil)) - | subl_case3 n1 t1 t2 => (* Eop (Oleal (Aindexed n1)) (t1:::Enil), t2 *) - addlimm (Int64.repr n1) (Eop Osubl (t1:::t2:::Enil)) - | subl_case4 t1 n2 t2 => (* t1, Eop (Oleal (Aindexed n2)) (t2:::Enil) *) - addlimm (Int64.repr (- n2)) (Eop Osubl (t1:::t2:::Enil)) - | subl_default e1 e2 => - Eop Osubl (e1:::e2:::Enil) - end. - - -Definition mullimm_base (n1: int64) (e2: expr) := - match Int64.one_bits' n1 with - | i :: nil => - shllimm e2 i - | i :: j :: nil => - Elet e2 (addl (shllimm (Eletvar 0) i) (shllimm (Eletvar 0) j)) - | _ => - Eop (Omullimm n1) (e2:::Enil) - end. - -(** Original definition: -<< -Nondetfunction mullimm (n1: int64) (e2: expr) := - if Archi.splitlong then SplitLong.mullimm n1 e2 - else if Int64.eq n1 Int64.zero then longconst Int64.zero - else if Int64.eq n1 Int64.one then e2 - else match e2 with - | Eop (Olongconst n2) Enil => longconst (Int64.mul n1 n2) - | Eop (Oleal (Aindexed n2)) (t2:::Enil) => addlimm (Int64.mul n1 (Int64.repr n2)) (mullimm_base n1 t2) - | _ => mullimm_base n1 e2 - end. ->> -*) - -Inductive mullimm_cases: forall (e2: expr), Type := - | mullimm_case1: forall n2, mullimm_cases (Eop (Olongconst n2) Enil) - | mullimm_case2: forall n2 t2, mullimm_cases (Eop (Oleal (Aindexed n2)) (t2:::Enil)) - | mullimm_default: forall (e2: expr), mullimm_cases e2. - -Definition mullimm_match (e2: expr) := - match e2 as zz1 return mullimm_cases zz1 with - | Eop (Olongconst n2) Enil => mullimm_case1 n2 - | Eop (Oleal (Aindexed n2)) (t2:::Enil) => mullimm_case2 n2 t2 - | e2 => mullimm_default e2 - end. - -Definition mullimm (n1: int64) (e2: expr) := - if Archi.splitlong then SplitLong.mullimm n1 e2 else if Int64.eq n1 Int64.zero then longconst Int64.zero else if Int64.eq n1 Int64.one then e2 else match mullimm_match e2 with - | mullimm_case1 n2 => (* Eop (Olongconst n2) Enil *) - longconst (Int64.mul n1 n2) - | mullimm_case2 n2 t2 => (* Eop (Oleal (Aindexed n2)) (t2:::Enil) *) - addlimm (Int64.mul n1 (Int64.repr n2)) (mullimm_base n1 t2) - | mullimm_default e2 => - mullimm_base n1 e2 - end. - - -(** Original definition: -<< -Nondetfunction mull (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.mull e1 e2 else - match e1, e2 with - | Eop (Olongconst n1) Enil, t2 => mullimm n1 t2 - | t1, Eop (Olongconst n2) Enil => mullimm n2 t1 - | _, _ => Eop Omull (e1:::e2:::Enil) - end. ->> -*) - -Inductive mull_cases: forall (e1: expr) (e2: expr), Type := - | mull_case1: forall n1 t2, mull_cases (Eop (Olongconst n1) Enil) (t2) - | mull_case2: forall t1 n2, mull_cases (t1) (Eop (Olongconst n2) Enil) - | mull_default: forall (e1: expr) (e2: expr), mull_cases e1 e2. - -Definition mull_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return mull_cases zz1 zz2 with - | Eop (Olongconst n1) Enil, t2 => mull_case1 n1 t2 - | t1, Eop (Olongconst n2) Enil => mull_case2 t1 n2 - | e1, e2 => mull_default e1 e2 - end. - -Definition mull (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.mull e1 e2 else match mull_match e1 e2 with - | mull_case1 n1 t2 => (* Eop (Olongconst n1) Enil, t2 *) - mullimm n1 t2 - | mull_case2 t1 n2 => (* t1, Eop (Olongconst n2) Enil *) - mullimm n2 t1 - | mull_default e1 e2 => - Eop Omull (e1:::e2:::Enil) - end. - - -Definition mullhu (e1: expr) (n2: int64) := - if Archi.splitlong then SplitLong.mullhu e1 n2 else - Eop Omullhu (e1 ::: longconst n2 ::: Enil). - -Definition mullhs (e1: expr) (n2: int64) := - if Archi.splitlong then SplitLong.mullhs e1 n2 else - Eop Omullhs (e1 ::: longconst n2 ::: Enil). - -Definition shrxlimm (e: expr) (n: int) := - if Archi.splitlong then SplitLong.shrxlimm e n else - if Int.eq n Int.zero then e else Eop (Oshrxlimm n) (e ::: Enil). - -Definition divlu_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.divlu_base e1 e2 else Eop Odivlu (e1:::e2:::Enil). -Definition modlu_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.modlu_base e1 e2 else Eop Omodlu (e1:::e2:::Enil). -Definition divls_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.divls_base e1 e2 else Eop Odivl (e1:::e2:::Enil). -Definition modls_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.modls_base e1 e2 else Eop Omodl (e1:::e2:::Enil). - -Definition cmplu (c: comparison) (e1 e2: expr) := - if Archi.splitlong then SplitLong.cmplu c e1 e2 else - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => - Eop (Ointconst (if Int64.cmpu c n1 n2 then Int.one else Int.zero)) Enil - | Some n1, None => Eop (Ocmp (Ccompluimm (swap_comparison c) n1)) (e2:::Enil) - | None, Some n2 => Eop (Ocmp (Ccompluimm c n2)) (e1:::Enil) - | None, None => Eop (Ocmp (Ccomplu c)) (e1:::e2:::Enil) - end. - -Definition cmpl (c: comparison) (e1 e2: expr) := - if Archi.splitlong then SplitLong.cmpl c e1 e2 else - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => - Eop (Ointconst (if Int64.cmp c n1 n2 then Int.one else Int.zero)) Enil - | Some n1, None => Eop (Ocmp (Ccomplimm (swap_comparison c) n1)) (e2:::Enil) - | None, Some n2 => Eop (Ocmp (Ccomplimm c n2)) (e1:::Enil) - | None, None => Eop (Ocmp (Ccompl c)) (e1:::e2:::Enil) - end. - -Definition longoffloat (e: expr) := - if Archi.splitlong then SplitLong.longoffloat e else - Eop Olongoffloat (e:::Enil). - -Definition floatoflong (e: expr) := - if Archi.splitlong then SplitLong.floatoflong e else - Eop Ofloatoflong (e:::Enil). - -Definition longofsingle (e: expr) := - if Archi.splitlong then SplitLong.longofsingle e else - Eop Olongofsingle (e:::Enil). - -Definition singleoflong (e: expr) := - if Archi.splitlong then SplitLong.singleoflong e else - Eop Osingleoflong (e:::Enil). - -End SELECT. diff --git a/verilog/SelectLong.vp b/verilog/SelectLong.vp index b213e23f..4f9fb518 100644 --- a/verilog/SelectLong.vp +++ b/verilog/SelectLong.vp @@ -16,7 +16,7 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. Require Import Op CminorSel. -Require Import SelectOp SplitLong. +Require Import OpHelpers SelectOp SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. diff --git a/verilog/SelectLongproof.v b/verilog/SelectLongproof.v index 3bef632d..f008f39e 100644 --- a/verilog/SelectLongproof.v +++ b/verilog/SelectLongproof.v @@ -16,6 +16,7 @@ Require Import String Coqlib Maps Integers Floats Errors. Require Archi. Require Import AST Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. diff --git a/verilog/SelectOp.v b/verilog/SelectOp.v deleted file mode 100644 index d477d7bd..00000000 --- a/verilog/SelectOp.v +++ /dev/null @@ -1,1549 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Instruction selection for operators *) - -(** The instruction selection pass recognizes opportunities for using - combined arithmetic and logical operations and addressing modes - offered by the target processor. For instance, the expression [x + 1] - can take advantage of the "immediate add" instruction of the processor, - and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned - into a "rotate and mask" instruction. - - This file defines functions for building CminorSel expressions and - statements, especially expressions consisting of operator - applications. These functions examine their arguments to choose - cheaper forms of operators whenever possible. - - For instance, [add e1 e2] will return a CminorSel expression semantically - equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a - [Oaddimm] operator if one of the arguments is an integer constant, - or suppress the addition altogether if one of the arguments is the - null integer. In passing, we perform operator reassociation - ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount - of constant propagation. - - On top of the "smart constructor" functions defined below, - module [Selection] implements the actual instruction selection pass. -*) - -Require Import Coqlib. -Require Import Compopts. -Require Import AST Integers Floats Builtins. -Require Import Op CminorSel. -Require Archi. - -Local Open Scope cminorsel_scope. - -(** ** Constants **) - -(** External oracle to determine whether a symbol should be addressed - through [Oindirectsymbol] or can be addressed via [Oleal Aglobal]. - This is to accommodate MacOS X's limitations on references to data - symbols imported from shared libraries. It can also help with PIC - code under ELF. *) - -Parameter symbol_is_external: ident -> bool. - -Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a. - -Definition addrsymbol (id: ident) (ofs: ptrofs) := - if symbol_is_external id then - if Ptrofs.eq ofs Ptrofs.zero - then Eop (Oindirectsymbol id) Enil - else Eop (Olea_ptr (Aindexed (Ptrofs.unsigned ofs))) (Eop (Oindirectsymbol id) Enil ::: Enil) - else - Eop (Olea_ptr (Aglobal id ofs)) Enil. - -Definition addrstack (ofs: ptrofs) := - Eop (Olea_ptr (Ainstack ofs)) Enil. - -(** ** Integer logical negation *) - -(** Original definition: -<< -Nondetfunction notint (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ointconst (Int.not n)) Enil - | Eop (Oxorimm n) (e1 ::: Enil) => Eop (Oxorimm (Int.not n)) (e1 ::: Enil) - | _ => Eop Onot (e ::: Enil) - end. ->> -*) - -Inductive notint_cases: forall (e: expr), Type := - | notint_case1: forall n, notint_cases (Eop (Ointconst n) Enil) - | notint_case2: forall n e1, notint_cases (Eop (Oxorimm n) (e1 ::: Enil)) - | notint_default: forall (e: expr), notint_cases e. - -Definition notint_match (e: expr) := - match e as zz1 return notint_cases zz1 with - | Eop (Ointconst n) Enil => notint_case1 n - | Eop (Oxorimm n) (e1 ::: Enil) => notint_case2 n e1 - | e => notint_default e - end. - -Definition notint (e: expr) := - match notint_match e with - | notint_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.not n)) Enil - | notint_case2 n e1 => (* Eop (Oxorimm n) (e1 ::: Enil) *) - Eop (Oxorimm (Int.not n)) (e1 ::: Enil) - | notint_default e => - Eop Onot (e ::: Enil) - end. - - -(** ** Integer addition and pointer addition *) - -(** Original definition: -<< -Nondetfunction addimm (n: int) (e: expr) := - if Int.eq n Int.zero then e else - match e with - | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil - | Eop (Olea addr) args => Eop (Olea (offset_addressing_total addr (Int.signed n))) args - | _ => Eop (Olea (Aindexed (Int.signed n))) (e ::: Enil) - end. ->> -*) - -Inductive addimm_cases: forall (e: expr), Type := - | addimm_case1: forall m, addimm_cases (Eop (Ointconst m) Enil) - | addimm_case2: forall addr args, addimm_cases (Eop (Olea addr) args) - | addimm_default: forall (e: expr), addimm_cases e. - -Definition addimm_match (e: expr) := - match e as zz1 return addimm_cases zz1 with - | Eop (Ointconst m) Enil => addimm_case1 m - | Eop (Olea addr) args => addimm_case2 addr args - | e => addimm_default e - end. - -Definition addimm (n: int) (e: expr) := - if Int.eq n Int.zero then e else match addimm_match e with - | addimm_case1 m => (* Eop (Ointconst m) Enil *) - Eop (Ointconst(Int.add n m)) Enil - | addimm_case2 addr args => (* Eop (Olea addr) args *) - Eop (Olea (offset_addressing_total addr (Int.signed n))) args - | addimm_default e => - Eop (Olea (Aindexed (Int.signed n))) (e ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction add (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 - | t1, Eop (Ointconst n2) Enil => addimm n2 t1 - | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => - Eop (Olea (Aindexed2 (n1 + n2))) (t1:::t2:::Enil) - | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Ascaled sc n2)) (t2:::Enil) => - Eop (Olea (Aindexed2scaled sc (n1 + n2))) (t1:::t2:::Enil) - | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => - Eop (Olea (Aindexed2scaled sc (n1 + n2))) (t2:::t1:::Enil) - | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil => - Eop (Olea (Abased id (Ptrofs.add ofs (Ptrofs.repr n1)))) (t1:::Enil) - | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Aindexed n2)) (t2:::Enil) => - Eop (Olea (Abased id (Ptrofs.add ofs (Ptrofs.repr n2)))) (t2:::Enil) - | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil => - Eop (Olea (Abasedscaled sc id (Ptrofs.add ofs (Ptrofs.repr n1)))) (t1:::Enil) - | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Ascaled sc n2)) (t2:::Enil) => - Eop (Olea (Abasedscaled sc id (Ptrofs.add ofs (Ptrofs.repr n2)))) (t2:::Enil) - | Eop (Olea (Ascaled sc n)) (t1:::Enil), t2 => - Eop (Olea (Aindexed2scaled sc n)) (t2:::t1:::Enil) - | t1, Eop (Olea (Ascaled sc n)) (t2:::Enil) => - Eop (Olea (Aindexed2scaled sc n)) (t1:::t2:::Enil) - | Eop (Olea (Aindexed n)) (t1:::Enil), t2 => - Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil) - | t1, Eop (Olea (Aindexed n)) (t2:::Enil) => - Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil) - | _, _ => - Eop (Olea (Aindexed2 0)) (e1:::e2:::Enil) - end. ->> -*) - -Inductive add_cases: forall (e1: expr) (e2: expr), Type := - | add_case1: forall n1 t2, add_cases (Eop (Ointconst n1) Enil) (t2) - | add_case2: forall t1 n2, add_cases (t1) (Eop (Ointconst n2) Enil) - | add_case3: forall n1 t1 n2 t2, add_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) (Eop (Olea (Aindexed n2)) (t2:::Enil)) - | add_case4: forall n1 t1 sc n2 t2, add_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) (Eop (Olea (Ascaled sc n2)) (t2:::Enil)) - | add_case5: forall sc n1 t1 n2 t2, add_cases (Eop (Olea (Ascaled sc n1)) (t1:::Enil)) (Eop (Olea (Aindexed n2)) (t2:::Enil)) - | add_case6: forall n1 t1 id ofs, add_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) (Eop (Olea (Aglobal id ofs)) Enil) - | add_case7: forall id ofs n2 t2, add_cases (Eop (Olea (Aglobal id ofs)) Enil) (Eop (Olea (Aindexed n2)) (t2:::Enil)) - | add_case8: forall sc n1 t1 id ofs, add_cases (Eop (Olea (Ascaled sc n1)) (t1:::Enil)) (Eop (Olea (Aglobal id ofs)) Enil) - | add_case9: forall id ofs sc n2 t2, add_cases (Eop (Olea (Aglobal id ofs)) Enil) (Eop (Olea (Ascaled sc n2)) (t2:::Enil)) - | add_case10: forall sc n t1 t2, add_cases (Eop (Olea (Ascaled sc n)) (t1:::Enil)) (t2) - | add_case11: forall t1 sc n t2, add_cases (t1) (Eop (Olea (Ascaled sc n)) (t2:::Enil)) - | add_case12: forall n t1 t2, add_cases (Eop (Olea (Aindexed n)) (t1:::Enil)) (t2) - | add_case13: forall t1 n t2, add_cases (t1) (Eop (Olea (Aindexed n)) (t2:::Enil)) - | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2. - -Definition add_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return add_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => add_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => add_case2 t1 n2 - | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => add_case3 n1 t1 n2 t2 - | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Ascaled sc n2)) (t2:::Enil) => add_case4 n1 t1 sc n2 t2 - | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => add_case5 sc n1 t1 n2 t2 - | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil => add_case6 n1 t1 id ofs - | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Aindexed n2)) (t2:::Enil) => add_case7 id ofs n2 t2 - | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil => add_case8 sc n1 t1 id ofs - | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Ascaled sc n2)) (t2:::Enil) => add_case9 id ofs sc n2 t2 - | Eop (Olea (Ascaled sc n)) (t1:::Enil), t2 => add_case10 sc n t1 t2 - | t1, Eop (Olea (Ascaled sc n)) (t2:::Enil) => add_case11 t1 sc n t2 - | Eop (Olea (Aindexed n)) (t1:::Enil), t2 => add_case12 n t1 t2 - | t1, Eop (Olea (Aindexed n)) (t2:::Enil) => add_case13 t1 n t2 - | e1, e2 => add_default e1 e2 - end. - -Definition add (e1: expr) (e2: expr) := - match add_match e1 e2 with - | add_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - addimm n1 t2 - | add_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - addimm n2 t1 - | add_case3 n1 t1 n2 t2 => (* Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) *) - Eop (Olea (Aindexed2 (n1 + n2))) (t1:::t2:::Enil) - | add_case4 n1 t1 sc n2 t2 => (* Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Ascaled sc n2)) (t2:::Enil) *) - Eop (Olea (Aindexed2scaled sc (n1 + n2))) (t1:::t2:::Enil) - | add_case5 sc n1 t1 n2 t2 => (* Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) *) - Eop (Olea (Aindexed2scaled sc (n1 + n2))) (t2:::t1:::Enil) - | add_case6 n1 t1 id ofs => (* Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil *) - Eop (Olea (Abased id (Ptrofs.add ofs (Ptrofs.repr n1)))) (t1:::Enil) - | add_case7 id ofs n2 t2 => (* Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Aindexed n2)) (t2:::Enil) *) - Eop (Olea (Abased id (Ptrofs.add ofs (Ptrofs.repr n2)))) (t2:::Enil) - | add_case8 sc n1 t1 id ofs => (* Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil *) - Eop (Olea (Abasedscaled sc id (Ptrofs.add ofs (Ptrofs.repr n1)))) (t1:::Enil) - | add_case9 id ofs sc n2 t2 => (* Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Ascaled sc n2)) (t2:::Enil) *) - Eop (Olea (Abasedscaled sc id (Ptrofs.add ofs (Ptrofs.repr n2)))) (t2:::Enil) - | add_case10 sc n t1 t2 => (* Eop (Olea (Ascaled sc n)) (t1:::Enil), t2 *) - Eop (Olea (Aindexed2scaled sc n)) (t2:::t1:::Enil) - | add_case11 t1 sc n t2 => (* t1, Eop (Olea (Ascaled sc n)) (t2:::Enil) *) - Eop (Olea (Aindexed2scaled sc n)) (t1:::t2:::Enil) - | add_case12 n t1 t2 => (* Eop (Olea (Aindexed n)) (t1:::Enil), t2 *) - Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil) - | add_case13 t1 n t2 => (* t1, Eop (Olea (Aindexed n)) (t2:::Enil) *) - Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil) - | add_default e1 e2 => - Eop (Olea (Aindexed2 0)) (e1:::e2:::Enil) - end. - - -(** ** Opposite *) - -(** Original definition: -<< -Nondetfunction negint (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ointconst (Int.neg n)) Enil - | _ => Eop Oneg (e ::: Enil) - end. ->> -*) - -Inductive negint_cases: forall (e: expr), Type := - | negint_case1: forall n, negint_cases (Eop (Ointconst n) Enil) - | negint_default: forall (e: expr), negint_cases e. - -Definition negint_match (e: expr) := - match e as zz1 return negint_cases zz1 with - | Eop (Ointconst n) Enil => negint_case1 n - | e => negint_default e - end. - -Definition negint (e: expr) := - match negint_match e with - | negint_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.neg n)) Enil - | negint_default e => - Eop Oneg (e ::: Enil) - end. - - -(** ** Integer and pointer subtraction *) - -(** Original definition: -<< -Nondetfunction sub (e1: expr) (e2: expr) := - match e1, e2 with - | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1 - | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => - addimm (Int.repr (n1 - n2)) (Eop Osub (t1:::t2:::Enil)) - | Eop (Olea (Aindexed n1)) (t1:::Enil), t2 => - addimm (Int.repr n1) (Eop Osub (t1:::t2:::Enil)) - | t1, Eop (Olea (Aindexed n2)) (t2:::Enil) => - addimm (Int.repr (-n2)) (Eop Osub (t1:::t2:::Enil)) - | _, _ => - Eop Osub (e1:::e2:::Enil) - end. ->> -*) - -Inductive sub_cases: forall (e1: expr) (e2: expr), Type := - | sub_case1: forall t1 n2, sub_cases (t1) (Eop (Ointconst n2) Enil) - | sub_case2: forall n1 t1 n2 t2, sub_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) (Eop (Olea (Aindexed n2)) (t2:::Enil)) - | sub_case3: forall n1 t1 t2, sub_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) (t2) - | sub_case4: forall t1 n2 t2, sub_cases (t1) (Eop (Olea (Aindexed n2)) (t2:::Enil)) - | sub_default: forall (e1: expr) (e2: expr), sub_cases e1 e2. - -Definition sub_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return sub_cases zz1 zz2 with - | t1, Eop (Ointconst n2) Enil => sub_case1 t1 n2 - | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => sub_case2 n1 t1 n2 t2 - | Eop (Olea (Aindexed n1)) (t1:::Enil), t2 => sub_case3 n1 t1 t2 - | t1, Eop (Olea (Aindexed n2)) (t2:::Enil) => sub_case4 t1 n2 t2 - | e1, e2 => sub_default e1 e2 - end. - -Definition sub (e1: expr) (e2: expr) := - match sub_match e1 e2 with - | sub_case1 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - addimm (Int.neg n2) t1 - | sub_case2 n1 t1 n2 t2 => (* Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) *) - addimm (Int.repr (n1 - n2)) (Eop Osub (t1:::t2:::Enil)) - | sub_case3 n1 t1 t2 => (* Eop (Olea (Aindexed n1)) (t1:::Enil), t2 *) - addimm (Int.repr n1) (Eop Osub (t1:::t2:::Enil)) - | sub_case4 t1 n2 t2 => (* t1, Eop (Olea (Aindexed n2)) (t2:::Enil) *) - addimm (Int.repr (-n2)) (Eop Osub (t1:::t2:::Enil)) - | sub_default e1 e2 => - Eop Osub (e1:::e2:::Enil) - end. - - -(** ** Immediate shifts *) - -Definition shift_is_scale (n: int) : bool := - Int.eq n (Int.repr 1) || Int.eq n (Int.repr 2) || Int.eq n (Int.repr 3). - -(** Original definition: -<< -Nondetfunction shlimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else - if negb (Int.ltu n Int.iwordsize) then - Eop Oshl (e1:::Eop (Ointconst n) Enil:::Enil) - else - match e1 with - | Eop (Ointconst n1) Enil => - Eop (Ointconst(Int.shl n1 n)) Enil - | Eop (Oshlimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshlimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshlimm n) (e1:::Enil) - | Eop (Olea (Aindexed n1)) (t1:::Enil) => - if shift_is_scale n - then Eop (Olea (Ascaled (Int.unsigned (Int.shl Int.one n)) - (Int.unsigned (Int.shl (Int.repr n1) n)))) (t1:::Enil) - else Eop (Oshlimm n) (e1:::Enil) - | _ => - if shift_is_scale n - then Eop (Olea (Ascaled (Int.unsigned (Int.shl Int.one n)) 0)) (e1:::Enil) - else Eop (Oshlimm n) (e1:::Enil) - end. ->> -*) - -Inductive shlimm_cases: forall (e1: expr) , Type := - | shlimm_case1: forall n1, shlimm_cases (Eop (Ointconst n1) Enil) - | shlimm_case2: forall n1 t1, shlimm_cases (Eop (Oshlimm n1) (t1:::Enil)) - | shlimm_case3: forall n1 t1, shlimm_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) - | shlimm_default: forall (e1: expr) , shlimm_cases e1. - -Definition shlimm_match (e1: expr) := - match e1 as zz1 return shlimm_cases zz1 with - | Eop (Ointconst n1) Enil => shlimm_case1 n1 - | Eop (Oshlimm n1) (t1:::Enil) => shlimm_case2 n1 t1 - | Eop (Olea (Aindexed n1)) (t1:::Enil) => shlimm_case3 n1 t1 - | e1 => shlimm_default e1 - end. - -Definition shlimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshl (e1:::Eop (Ointconst n) Enil:::Enil) else match shlimm_match e1 with - | shlimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst(Int.shl n1 n)) Enil - | shlimm_case2 n1 t1 => (* Eop (Oshlimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshlimm (Int.add n n1)) (t1:::Enil) else Eop (Oshlimm n) (e1:::Enil) - | shlimm_case3 n1 t1 => (* Eop (Olea (Aindexed n1)) (t1:::Enil) *) - if shift_is_scale n then Eop (Olea (Ascaled (Int.unsigned (Int.shl Int.one n)) (Int.unsigned (Int.shl (Int.repr n1) n)))) (t1:::Enil) else Eop (Oshlimm n) (e1:::Enil) - | shlimm_default e1 => - if shift_is_scale n then Eop (Olea (Ascaled (Int.unsigned (Int.shl Int.one n)) 0)) (e1:::Enil) else Eop (Oshlimm n) (e1:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shruimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else - if negb (Int.ltu n Int.iwordsize) then - Eop Oshru (e1:::Eop (Ointconst n) Enil:::Enil) - else - match e1 with - | Eop (Ointconst n1) Enil => - Eop (Ointconst(Int.shru n1 n)) Enil - | Eop (Oshruimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshruimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshruimm n) (e1:::Enil) - | _ => - Eop (Oshruimm n) (e1:::Enil) - end. ->> -*) - -Inductive shruimm_cases: forall (e1: expr) , Type := - | shruimm_case1: forall n1, shruimm_cases (Eop (Ointconst n1) Enil) - | shruimm_case2: forall n1 t1, shruimm_cases (Eop (Oshruimm n1) (t1:::Enil)) - | shruimm_default: forall (e1: expr) , shruimm_cases e1. - -Definition shruimm_match (e1: expr) := - match e1 as zz1 return shruimm_cases zz1 with - | Eop (Ointconst n1) Enil => shruimm_case1 n1 - | Eop (Oshruimm n1) (t1:::Enil) => shruimm_case2 n1 t1 - | e1 => shruimm_default e1 - end. - -Definition shruimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshru (e1:::Eop (Ointconst n) Enil:::Enil) else match shruimm_match e1 with - | shruimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst(Int.shru n1 n)) Enil - | shruimm_case2 n1 t1 => (* Eop (Oshruimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshruimm (Int.add n n1)) (t1:::Enil) else Eop (Oshruimm n) (e1:::Enil) - | shruimm_default e1 => - Eop (Oshruimm n) (e1:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shrimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else - if negb (Int.ltu n Int.iwordsize) then - Eop Oshr (e1:::Eop (Ointconst n) Enil:::Enil) - else - match e1 with - | Eop (Ointconst n1) Enil => - Eop (Ointconst(Int.shr n1 n)) Enil - | Eop (Oshrimm n1) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) - else Eop (Oshrimm n) (e1:::Enil) - | _ => - Eop (Oshrimm n) (e1:::Enil) - end. ->> -*) - -Inductive shrimm_cases: forall (e1: expr) , Type := - | shrimm_case1: forall n1, shrimm_cases (Eop (Ointconst n1) Enil) - | shrimm_case2: forall n1 t1, shrimm_cases (Eop (Oshrimm n1) (t1:::Enil)) - | shrimm_default: forall (e1: expr) , shrimm_cases e1. - -Definition shrimm_match (e1: expr) := - match e1 as zz1 return shrimm_cases zz1 with - | Eop (Ointconst n1) Enil => shrimm_case1 n1 - | Eop (Oshrimm n1) (t1:::Enil) => shrimm_case2 n1 t1 - | e1 => shrimm_default e1 - end. - -Definition shrimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshr (e1:::Eop (Ointconst n) Enil:::Enil) else match shrimm_match e1 with - | shrimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst(Int.shr n1 n)) Enil - | shrimm_case2 n1 t1 => (* Eop (Oshrimm n1) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil) - | shrimm_default e1 => - Eop (Oshrimm n) (e1:::Enil) - end. - - -(** ** Integer multiply *) - -Definition mulimm_base (n1: int) (e2: expr) := - match Int.one_bits n1 with - | i :: nil => - shlimm e2 i - | i :: j :: nil => - Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) - | _ => - Eop (Omulimm n1) (e2:::Enil) - end. - -(** Original definition: -<< -Nondetfunction mulimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil - else if Int.eq n1 Int.one then e2 - else match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst(Int.mul n1 n2)) Enil - | Eop (Olea (Aindexed n2)) (t2:::Enil) => addimm (Int.mul n1 (Int.repr n2)) (mulimm_base n1 t2) - | _ => mulimm_base n1 e2 - end. ->> -*) - -Inductive mulimm_cases: forall (e2: expr), Type := - | mulimm_case1: forall n2, mulimm_cases (Eop (Ointconst n2) Enil) - | mulimm_case2: forall n2 t2, mulimm_cases (Eop (Olea (Aindexed n2)) (t2:::Enil)) - | mulimm_default: forall (e2: expr), mulimm_cases e2. - -Definition mulimm_match (e2: expr) := - match e2 as zz1 return mulimm_cases zz1 with - | Eop (Ointconst n2) Enil => mulimm_case1 n2 - | Eop (Olea (Aindexed n2)) (t2:::Enil) => mulimm_case2 n2 t2 - | e2 => mulimm_default e2 - end. - -Definition mulimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.one then e2 else match mulimm_match e2 with - | mulimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst(Int.mul n1 n2)) Enil - | mulimm_case2 n2 t2 => (* Eop (Olea (Aindexed n2)) (t2:::Enil) *) - addimm (Int.mul n1 (Int.repr n2)) (mulimm_base n1 t2) - | mulimm_default e2 => - mulimm_base n1 e2 - end. - - -(** Original definition: -<< -Nondetfunction mul (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2 - | t1, Eop (Ointconst n2) Enil => mulimm n2 t1 - | _, _ => Eop Omul (e1:::e2:::Enil) - end. ->> -*) - -Inductive mul_cases: forall (e1: expr) (e2: expr), Type := - | mul_case1: forall n1 t2, mul_cases (Eop (Ointconst n1) Enil) (t2) - | mul_case2: forall t1 n2, mul_cases (t1) (Eop (Ointconst n2) Enil) - | mul_default: forall (e1: expr) (e2: expr), mul_cases e1 e2. - -Definition mul_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return mul_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => mul_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => mul_case2 t1 n2 - | e1, e2 => mul_default e1 e2 - end. - -Definition mul (e1: expr) (e2: expr) := - match mul_match e1 e2 with - | mul_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - mulimm n1 t2 - | mul_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - mulimm n2 t1 - | mul_default e1 e2 => - Eop Omul (e1:::e2:::Enil) - end. - - -Definition mulhs (e1: expr) (e2: expr) := Eop Omulhs (e1 ::: e2 ::: Enil). -Definition mulhu (e1: expr) (e2: expr) := Eop Omulhu (e1 ::: e2 ::: Enil). - -(** ** Bitwise and, or, xor *) - -(** Original definition: -<< -Nondetfunction andimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil - else if Int.eq n1 Int.mone then e2 - else match e2 with - | Eop (Ointconst n2) Enil => - Eop (Ointconst (Int.and n1 n2)) Enil - | Eop (Oandimm n2) (t2:::Enil) => - Eop (Oandimm (Int.and n1 n2)) (t2:::Enil) - | Eop Ocast8unsigned (t2:::Enil) => - Eop (Oandimm (Int.and n1 (Int.repr 255))) (t2:::Enil) - | Eop Ocast16unsigned (t2:::Enil) => - Eop (Oandimm (Int.and n1 (Int.repr 65535))) (t2:::Enil) - | _ => - Eop (Oandimm n1) (e2:::Enil) - end. ->> -*) - -Inductive andimm_cases: forall (e2: expr), Type := - | andimm_case1: forall n2, andimm_cases (Eop (Ointconst n2) Enil) - | andimm_case2: forall n2 t2, andimm_cases (Eop (Oandimm n2) (t2:::Enil)) - | andimm_case3: forall t2, andimm_cases (Eop Ocast8unsigned (t2:::Enil)) - | andimm_case4: forall t2, andimm_cases (Eop Ocast16unsigned (t2:::Enil)) - | andimm_default: forall (e2: expr), andimm_cases e2. - -Definition andimm_match (e2: expr) := - match e2 as zz1 return andimm_cases zz1 with - | Eop (Ointconst n2) Enil => andimm_case1 n2 - | Eop (Oandimm n2) (t2:::Enil) => andimm_case2 n2 t2 - | Eop Ocast8unsigned (t2:::Enil) => andimm_case3 t2 - | Eop Ocast16unsigned (t2:::Enil) => andimm_case4 t2 - | e2 => andimm_default e2 - end. - -Definition andimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match andimm_match e2 with - | andimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.and n1 n2)) Enil - | andimm_case2 n2 t2 => (* Eop (Oandimm n2) (t2:::Enil) *) - Eop (Oandimm (Int.and n1 n2)) (t2:::Enil) - | andimm_case3 t2 => (* Eop Ocast8unsigned (t2:::Enil) *) - Eop (Oandimm (Int.and n1 (Int.repr 255))) (t2:::Enil) - | andimm_case4 t2 => (* Eop Ocast16unsigned (t2:::Enil) *) - Eop (Oandimm (Int.and n1 (Int.repr 65535))) (t2:::Enil) - | andimm_default e2 => - Eop (Oandimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction and (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => andimm n1 t2 - | t1, Eop (Ointconst n2) Enil => andimm n2 t1 - | _, _ => Eop Oand (e1:::e2:::Enil) - end. ->> -*) - -Inductive and_cases: forall (e1: expr) (e2: expr), Type := - | and_case1: forall n1 t2, and_cases (Eop (Ointconst n1) Enil) (t2) - | and_case2: forall t1 n2, and_cases (t1) (Eop (Ointconst n2) Enil) - | and_default: forall (e1: expr) (e2: expr), and_cases e1 e2. - -Definition and_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return and_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => and_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => and_case2 t1 n2 - | e1, e2 => and_default e1 e2 - end. - -Definition and (e1: expr) (e2: expr) := - match and_match e1 e2 with - | and_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - andimm n1 t2 - | and_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - andimm n2 t1 - | and_default e1 e2 => - Eop Oand (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction orimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 - else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil - else match e2 with - | Eop (Ointconst n2) Enil => - Eop (Ointconst (Int.or n1 n2)) Enil - | Eop (Oorimm n2) (t2:::Enil) => - Eop (Oorimm (Int.or n1 n2)) (t2:::Enil) - | _ => - Eop (Oorimm n1) (e2:::Enil) - end. ->> -*) - -Inductive orimm_cases: forall (e2: expr), Type := - | orimm_case1: forall n2, orimm_cases (Eop (Ointconst n2) Enil) - | orimm_case2: forall n2 t2, orimm_cases (Eop (Oorimm n2) (t2:::Enil)) - | orimm_default: forall (e2: expr), orimm_cases e2. - -Definition orimm_match (e2: expr) := - match e2 as zz1 return orimm_cases zz1 with - | Eop (Ointconst n2) Enil => orimm_case1 n2 - | Eop (Oorimm n2) (t2:::Enil) => orimm_case2 n2 t2 - | e2 => orimm_default e2 - end. - -Definition orimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else match orimm_match e2 with - | orimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.or n1 n2)) Enil - | orimm_case2 n2 t2 => (* Eop (Oorimm n2) (t2:::Enil) *) - Eop (Oorimm (Int.or n1 n2)) (t2:::Enil) - | orimm_default e2 => - Eop (Oorimm n1) (e2:::Enil) - end. - - -Definition same_expr_pure (e1 e2: expr) := - match e1, e2 with - | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false - | _, _ => false - end. - -(** Original definition: -<< -Nondetfunction or (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => orimm n1 t2 - | t1, Eop (Ointconst n2) Enil => orimm n2 t1 - | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) => - if Int.eq (Int.add n1 n2) Int.iwordsize then - if same_expr_pure t1 t2 - then Eop (Ororimm n2) (t1:::Enil) - else Eop (Oshldimm n1) (t1:::t2:::Enil) - else Eop Oor (e1:::e2:::Enil) - | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) => - if Int.eq (Int.add n1 n2) Int.iwordsize then - if same_expr_pure t1 t2 - then Eop (Ororimm n2) (t1:::Enil) - else Eop (Oshldimm n1) (t1:::t2:::Enil) - else Eop Oor (e1:::e2:::Enil) - | _, _ => - Eop Oor (e1:::e2:::Enil) - end. ->> -*) - -Inductive or_cases: forall (e1: expr) (e2: expr), Type := - | or_case1: forall n1 t2, or_cases (Eop (Ointconst n1) Enil) (t2) - | or_case2: forall t1 n2, or_cases (t1) (Eop (Ointconst n2) Enil) - | or_case3: forall n1 t1 n2 t2, or_cases (Eop (Oshlimm n1) (t1:::Enil)) (Eop (Oshruimm n2) (t2:::Enil)) - | or_case4: forall n2 t2 n1 t1, or_cases (Eop (Oshruimm n2) (t2:::Enil)) (Eop (Oshlimm n1) (t1:::Enil)) - | or_default: forall (e1: expr) (e2: expr), or_cases e1 e2. - -Definition or_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return or_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => or_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => or_case2 t1 n2 - | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) => or_case3 n1 t1 n2 t2 - | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) => or_case4 n2 t2 n1 t1 - | e1, e2 => or_default e1 e2 - end. - -Definition or (e1: expr) (e2: expr) := - match or_match e1 e2 with - | or_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - orimm n1 t2 - | or_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - orimm n2 t1 - | or_case3 n1 t1 n2 t2 => (* Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) *) - if Int.eq (Int.add n1 n2) Int.iwordsize then if same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop (Oshldimm n1) (t1:::t2:::Enil) else Eop Oor (e1:::e2:::Enil) - | or_case4 n2 t2 n1 t1 => (* Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) *) - if Int.eq (Int.add n1 n2) Int.iwordsize then if same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop (Oshldimm n1) (t1:::t2:::Enil) else Eop Oor (e1:::e2:::Enil) - | or_default e1 e2 => - Eop Oor (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction xorimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 - else match e2 with - | Eop (Ointconst n2) Enil => - Eop (Ointconst (Int.xor n1 n2)) Enil - | Eop (Oxorimm n2) (t2:::Enil) => - Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil) - | Eop Onot (t2:::Enil) => - Eop (Oxorimm (Int.not n1)) (t2:::Enil) - | _ => - Eop (Oxorimm n1) (e2:::Enil) - end. ->> -*) - -Inductive xorimm_cases: forall (e2: expr), Type := - | xorimm_case1: forall n2, xorimm_cases (Eop (Ointconst n2) Enil) - | xorimm_case2: forall n2 t2, xorimm_cases (Eop (Oxorimm n2) (t2:::Enil)) - | xorimm_case3: forall t2, xorimm_cases (Eop Onot (t2:::Enil)) - | xorimm_default: forall (e2: expr), xorimm_cases e2. - -Definition xorimm_match (e2: expr) := - match e2 as zz1 return xorimm_cases zz1 with - | Eop (Ointconst n2) Enil => xorimm_case1 n2 - | Eop (Oxorimm n2) (t2:::Enil) => xorimm_case2 n2 t2 - | Eop Onot (t2:::Enil) => xorimm_case3 t2 - | e2 => xorimm_default e2 - end. - -Definition xorimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else match xorimm_match e2 with - | xorimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.xor n1 n2)) Enil - | xorimm_case2 n2 t2 => (* Eop (Oxorimm n2) (t2:::Enil) *) - Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil) - | xorimm_case3 t2 => (* Eop Onot (t2:::Enil) *) - Eop (Oxorimm (Int.not n1)) (t2:::Enil) - | xorimm_default e2 => - Eop (Oxorimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction xor (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2 - | t1, Eop (Ointconst n2) Enil => xorimm n2 t1 - | _, _ => Eop Oxor (e1:::e2:::Enil) - end. ->> -*) - -Inductive xor_cases: forall (e1: expr) (e2: expr), Type := - | xor_case1: forall n1 t2, xor_cases (Eop (Ointconst n1) Enil) (t2) - | xor_case2: forall t1 n2, xor_cases (t1) (Eop (Ointconst n2) Enil) - | xor_default: forall (e1: expr) (e2: expr), xor_cases e1 e2. - -Definition xor_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return xor_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => xor_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => xor_case2 t1 n2 - | e1, e2 => xor_default e1 e2 - end. - -Definition xor (e1: expr) (e2: expr) := - match xor_match e1 e2 with - | xor_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - xorimm n1 t2 - | xor_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - xorimm n2 t1 - | xor_default e1 e2 => - Eop Oxor (e1:::e2:::Enil) - end. - - -(** ** Integer division and modulus *) - -Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil). -Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil). -Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). -Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil). - -Definition shrximm (e1: expr) (n2: int) := - if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil). - -(** ** General shifts *) - -(** Original definition: -<< -Nondetfunction shl (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shlimm e1 n2 - | _ => Eop Oshl (e1:::e2:::Enil) - end. ->> -*) - -Inductive shl_cases: forall (e2: expr), Type := - | shl_case1: forall n2, shl_cases (Eop (Ointconst n2) Enil) - | shl_default: forall (e2: expr), shl_cases e2. - -Definition shl_match (e2: expr) := - match e2 as zz1 return shl_cases zz1 with - | Eop (Ointconst n2) Enil => shl_case1 n2 - | e2 => shl_default e2 - end. - -Definition shl (e1: expr) (e2: expr) := - match shl_match e2 with - | shl_case1 n2 => (* Eop (Ointconst n2) Enil *) - shlimm e1 n2 - | shl_default e2 => - Eop Oshl (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shr (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shrimm e1 n2 - | _ => Eop Oshr (e1:::e2:::Enil) - end. ->> -*) - -Inductive shr_cases: forall (e2: expr), Type := - | shr_case1: forall n2, shr_cases (Eop (Ointconst n2) Enil) - | shr_default: forall (e2: expr), shr_cases e2. - -Definition shr_match (e2: expr) := - match e2 as zz1 return shr_cases zz1 with - | Eop (Ointconst n2) Enil => shr_case1 n2 - | e2 => shr_default e2 - end. - -Definition shr (e1: expr) (e2: expr) := - match shr_match e2 with - | shr_case1 n2 => (* Eop (Ointconst n2) Enil *) - shrimm e1 n2 - | shr_default e2 => - Eop Oshr (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shru (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shruimm e1 n2 - | _ => Eop Oshru (e1:::e2:::Enil) - end. ->> -*) - -Inductive shru_cases: forall (e2: expr), Type := - | shru_case1: forall n2, shru_cases (Eop (Ointconst n2) Enil) - | shru_default: forall (e2: expr), shru_cases e2. - -Definition shru_match (e2: expr) := - match e2 as zz1 return shru_cases zz1 with - | Eop (Ointconst n2) Enil => shru_case1 n2 - | e2 => shru_default e2 - end. - -Definition shru (e1: expr) (e2: expr) := - match shru_match e2 with - | shru_case1 n2 => (* Eop (Ointconst n2) Enil *) - shruimm e1 n2 - | shru_default e2 => - Eop Oshru (e1:::e2:::Enil) - end. - - -(** ** Floating-point arithmetic *) - -Definition negf (e: expr) := Eop Onegf (e ::: Enil). -Definition absf (e: expr) := Eop Oabsf (e ::: Enil). -Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). -Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). -Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). - -Definition negfs (e: expr) := Eop Onegfs (e ::: Enil). -Definition absfs (e: expr) := Eop Oabsfs (e ::: Enil). -Definition addfs (e1 e2: expr) := Eop Oaddfs (e1 ::: e2 ::: Enil). -Definition subfs (e1 e2: expr) := Eop Osubfs (e1 ::: e2 ::: Enil). -Definition mulfs (e1 e2: expr) := Eop Omulfs (e1 ::: e2 ::: Enil). - -(** ** Comparisons *) - -(** Original definition: -<< -Nondetfunction compimm (default: comparison -> int -> condition) - (sem: comparison -> int -> int -> bool) - (c: comparison) (e1: expr) (n2: int) := - match c, e1 with - | c, Eop (Ointconst n1) Enil => - Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil - | Ceq, Eop (Ocmp c) el => - if Int.eq_dec n2 Int.zero then - Eop (Ocmp (negate_condition c)) el - else if Int.eq_dec n2 Int.one then - Eop (Ocmp c) el - else - Eop (Ointconst Int.zero) Enil - | Cne, Eop (Ocmp c) el => - if Int.eq_dec n2 Int.zero then - Eop (Ocmp c) el - else if Int.eq_dec n2 Int.one then - Eop (Ocmp (negate_condition c)) el - else - Eop (Ointconst Int.one) Enil - | Ceq, Eop (Oandimm n1) (t1 ::: Enil) => - if Int.eq_dec n2 Int.zero then - Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil) - else - Eop (Ocmp (default c n2)) (e1 ::: Enil) - | Cne, Eop (Oandimm n1) (t1 ::: Enil) => - if Int.eq_dec n2 Int.zero then - Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil) - else - Eop (Ocmp (default c n2)) (e1 ::: Enil) - | _, _ => - Eop (Ocmp (default c n2)) (e1 ::: Enil) - end. ->> -*) - -Inductive compimm_cases: forall (c: comparison) (e1: expr) , Type := - | compimm_case1: forall c n1, compimm_cases (c) (Eop (Ointconst n1) Enil) - | compimm_case2: forall c el, compimm_cases (Ceq) (Eop (Ocmp c) el) - | compimm_case3: forall c el, compimm_cases (Cne) (Eop (Ocmp c) el) - | compimm_case4: forall n1 t1, compimm_cases (Ceq) (Eop (Oandimm n1) (t1 ::: Enil)) - | compimm_case5: forall n1 t1, compimm_cases (Cne) (Eop (Oandimm n1) (t1 ::: Enil)) - | compimm_default: forall (c: comparison) (e1: expr) , compimm_cases c e1. - -Definition compimm_match (c: comparison) (e1: expr) := - match c as zz1, e1 as zz2 return compimm_cases zz1 zz2 with - | c, Eop (Ointconst n1) Enil => compimm_case1 c n1 - | Ceq, Eop (Ocmp c) el => compimm_case2 c el - | Cne, Eop (Ocmp c) el => compimm_case3 c el - | Ceq, Eop (Oandimm n1) (t1 ::: Enil) => compimm_case4 n1 t1 - | Cne, Eop (Oandimm n1) (t1 ::: Enil) => compimm_case5 n1 t1 - | c, e1 => compimm_default c e1 - end. - -Definition compimm (default: comparison -> int -> condition) (sem: comparison -> int -> int -> bool) (c: comparison) (e1: expr) (n2: int) := - match compimm_match c e1 with - | compimm_case1 c n1 => (* c, Eop (Ointconst n1) Enil *) - Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil - | compimm_case2 c el => (* Ceq, Eop (Ocmp c) el *) - if Int.eq_dec n2 Int.zero then Eop (Ocmp (negate_condition c)) el else if Int.eq_dec n2 Int.one then Eop (Ocmp c) el else Eop (Ointconst Int.zero) Enil - | compimm_case3 c el => (* Cne, Eop (Ocmp c) el *) - if Int.eq_dec n2 Int.zero then Eop (Ocmp c) el else if Int.eq_dec n2 Int.one then Eop (Ocmp (negate_condition c)) el else Eop (Ointconst Int.one) Enil - | compimm_case4 n1 t1 => (* Ceq, Eop (Oandimm n1) (t1 ::: Enil) *) - if Int.eq_dec n2 Int.zero then Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil) else Eop (Ocmp (default c n2)) (e1 ::: Enil) - | compimm_case5 n1 t1 => (* Cne, Eop (Oandimm n1) (t1 ::: Enil) *) - if Int.eq_dec n2 Int.zero then Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil) else Eop (Ocmp (default c n2)) (e1 ::: Enil) - | compimm_default c e1 => - Eop (Ocmp (default c n2)) (e1 ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => - compimm Ccompimm Int.cmp (swap_comparison c) t2 n1 - | t1, Eop (Ointconst n2) Enil => - compimm Ccompimm Int.cmp c t1 n2 - | _, _ => - Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil) - end. ->> -*) - -Inductive comp_cases: forall (e1: expr) (e2: expr), Type := - | comp_case1: forall n1 t2, comp_cases (Eop (Ointconst n1) Enil) (t2) - | comp_case2: forall t1 n2, comp_cases (t1) (Eop (Ointconst n2) Enil) - | comp_default: forall (e1: expr) (e2: expr), comp_cases e1 e2. - -Definition comp_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return comp_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => comp_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => comp_case2 t1 n2 - | e1, e2 => comp_default e1 e2 - end. - -Definition comp (c: comparison) (e1: expr) (e2: expr) := - match comp_match e1 e2 with - | comp_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - compimm Ccompimm Int.cmp (swap_comparison c) t2 n1 - | comp_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - compimm Ccompimm Int.cmp c t1 n2 - | comp_default e1 e2 => - Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => - compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1 - | t1, Eop (Ointconst n2) Enil => - compimm Ccompuimm Int.cmpu c t1 n2 - | _, _ => - Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) - end. ->> -*) - -Inductive compu_cases: forall (e1: expr) (e2: expr), Type := - | compu_case1: forall n1 t2, compu_cases (Eop (Ointconst n1) Enil) (t2) - | compu_case2: forall t1 n2, compu_cases (t1) (Eop (Ointconst n2) Enil) - | compu_default: forall (e1: expr) (e2: expr), compu_cases e1 e2. - -Definition compu_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return compu_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => compu_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => compu_case2 t1 n2 - | e1, e2 => compu_default e1 e2 - end. - -Definition compu (c: comparison) (e1: expr) (e2: expr) := - match compu_match e1 e2 with - | compu_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1 - | compu_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - compimm Ccompuimm Int.cmpu c t1 n2 - | compu_default e1 e2 => - Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil) - end. - - -Definition compf (c: comparison) (e1: expr) (e2: expr) := - Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). - -Definition compfs (c: comparison) (e1: expr) (e2: expr) := - Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). - -(** ** Integer conversions *) - -(** Original definition: -<< -Nondetfunction cast8unsigned (e: expr) := - match e with - | Eop (Ointconst n) Enil => - Eop (Ointconst (Int.zero_ext 8 n)) Enil - | Eop (Oandimm n) (t:::Enil) => - andimm (Int.and (Int.repr 255) n) t - | _ => - Eop Ocast8unsigned (e:::Enil) - end. ->> -*) - -Inductive cast8unsigned_cases: forall (e: expr), Type := - | cast8unsigned_case1: forall n, cast8unsigned_cases (Eop (Ointconst n) Enil) - | cast8unsigned_case2: forall n t, cast8unsigned_cases (Eop (Oandimm n) (t:::Enil)) - | cast8unsigned_default: forall (e: expr), cast8unsigned_cases e. - -Definition cast8unsigned_match (e: expr) := - match e as zz1 return cast8unsigned_cases zz1 with - | Eop (Ointconst n) Enil => cast8unsigned_case1 n - | Eop (Oandimm n) (t:::Enil) => cast8unsigned_case2 n t - | e => cast8unsigned_default e - end. - -Definition cast8unsigned (e: expr) := - match cast8unsigned_match e with - | cast8unsigned_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.zero_ext 8 n)) Enil - | cast8unsigned_case2 n t => (* Eop (Oandimm n) (t:::Enil) *) - andimm (Int.and (Int.repr 255) n) t - | cast8unsigned_default e => - Eop Ocast8unsigned (e:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction cast8signed (e: expr) := - match e with - | Eop (Ointconst n) Enil => - Eop (Ointconst (Int.sign_ext 8 n)) Enil - | _ => - Eop Ocast8signed (e ::: Enil) - end. ->> -*) - -Inductive cast8signed_cases: forall (e: expr), Type := - | cast8signed_case1: forall n, cast8signed_cases (Eop (Ointconst n) Enil) - | cast8signed_default: forall (e: expr), cast8signed_cases e. - -Definition cast8signed_match (e: expr) := - match e as zz1 return cast8signed_cases zz1 with - | Eop (Ointconst n) Enil => cast8signed_case1 n - | e => cast8signed_default e - end. - -Definition cast8signed (e: expr) := - match cast8signed_match e with - | cast8signed_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.sign_ext 8 n)) Enil - | cast8signed_default e => - Eop Ocast8signed (e ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction cast16unsigned (e: expr) := - match e with - | Eop (Ointconst n) Enil => - Eop (Ointconst (Int.zero_ext 16 n)) Enil - | Eop (Oandimm n) (t:::Enil) => - andimm (Int.and (Int.repr 65535) n) t - | _ => - Eop Ocast16unsigned (e:::Enil) - end. ->> -*) - -Inductive cast16unsigned_cases: forall (e: expr), Type := - | cast16unsigned_case1: forall n, cast16unsigned_cases (Eop (Ointconst n) Enil) - | cast16unsigned_case2: forall n t, cast16unsigned_cases (Eop (Oandimm n) (t:::Enil)) - | cast16unsigned_default: forall (e: expr), cast16unsigned_cases e. - -Definition cast16unsigned_match (e: expr) := - match e as zz1 return cast16unsigned_cases zz1 with - | Eop (Ointconst n) Enil => cast16unsigned_case1 n - | Eop (Oandimm n) (t:::Enil) => cast16unsigned_case2 n t - | e => cast16unsigned_default e - end. - -Definition cast16unsigned (e: expr) := - match cast16unsigned_match e with - | cast16unsigned_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.zero_ext 16 n)) Enil - | cast16unsigned_case2 n t => (* Eop (Oandimm n) (t:::Enil) *) - andimm (Int.and (Int.repr 65535) n) t - | cast16unsigned_default e => - Eop Ocast16unsigned (e:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction cast16signed (e: expr) := - match e with - | Eop (Ointconst n) Enil => - Eop (Ointconst (Int.sign_ext 16 n)) Enil - | _ => - Eop Ocast16signed (e ::: Enil) - end. ->> -*) - -Inductive cast16signed_cases: forall (e: expr), Type := - | cast16signed_case1: forall n, cast16signed_cases (Eop (Ointconst n) Enil) - | cast16signed_default: forall (e: expr), cast16signed_cases e. - -Definition cast16signed_match (e: expr) := - match e as zz1 return cast16signed_cases zz1 with - | Eop (Ointconst n) Enil => cast16signed_case1 n - | e => cast16signed_default e - end. - -Definition cast16signed (e: expr) := - match cast16signed_match e with - | cast16signed_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ointconst (Int.sign_ext 16 n)) Enil - | cast16signed_default e => - Eop Ocast16signed (e ::: Enil) - end. - - -(** ** Selection *) - -Definition select_supported (ty: typ) : bool := - match ty with - | Tint => true - | Tlong => Archi.ptr64 - | _ => false - end. - -(** [Asmgen.mk_sel] cannot always handle the conditions that are - implemented as a "and" of two processor flags. However it can - handle the negation of those conditions, which are implemented - as an "or". So, for the risky conditions we just take their - negation and swap the two arguments of the [select]. *) - -Definition select_swap (cond: condition) := - match cond with - | Ccompf Cne | Ccompfs Cne | Cnotcompf Ceq | Cnotcompfs Ceq => true - | _ => false - end. - -Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) := - if select_supported ty then - if select_swap cond - then Some (Eop (Osel (negate_condition cond) ty) (e2 ::: e1 ::: args)) - else Some (Eop (Osel cond ty) (e1 ::: e2 ::: args)) - else None. - -(** ** Floating-point conversions *) - -Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). -Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). - -Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). - -(** Original definition: -<< -Nondetfunction floatofint (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil - | _ => Eop Ofloatofint (e ::: Enil) - end. ->> -*) - -Inductive floatofint_cases: forall (e: expr), Type := - | floatofint_case1: forall n, floatofint_cases (Eop (Ointconst n) Enil) - | floatofint_default: forall (e: expr), floatofint_cases e. - -Definition floatofint_match (e: expr) := - match e as zz1 return floatofint_cases zz1 with - | Eop (Ointconst n) Enil => floatofint_case1 n - | e => floatofint_default e - end. - -Definition floatofint (e: expr) := - match floatofint_match e with - | floatofint_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ofloatconst (Float.of_int n)) Enil - | floatofint_default e => - Eop Ofloatofint (e ::: Enil) - end. - - -Definition intuoffloat (e: expr) := - if Archi.splitlong then - Elet e - (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) - (intoffloat (Eletvar 1)) - (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat - else - Eop Olowlong (Eop Olongoffloat (e ::: Enil) ::: Enil). - -(** Original definition: -<< -Nondetfunction floatofintu (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil - | _ => - if Archi.splitlong then - let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in - Elet e - (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) - (floatofint (Eletvar O)) - (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)) - else - Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil) - end. ->> -*) - -Inductive floatofintu_cases: forall (e: expr), Type := - | floatofintu_case1: forall n, floatofintu_cases (Eop (Ointconst n) Enil) - | floatofintu_default: forall (e: expr), floatofintu_cases e. - -Definition floatofintu_match (e: expr) := - match e as zz1 return floatofintu_cases zz1 with - | Eop (Ointconst n) Enil => floatofintu_case1 n - | e => floatofintu_default e - end. - -Definition floatofintu (e: expr) := - match floatofintu_match e with - | floatofintu_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Ofloatconst (Float.of_intu n)) Enil - | floatofintu_default e => - if Archi.splitlong then let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in Elet e (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) (floatofint (Eletvar O)) (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)) else Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil) - end. - - -Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil). - -(** Original definition: -<< -Nondetfunction singleofint (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_int n)) Enil - | _ => Eop Osingleofint (e ::: Enil) - end. ->> -*) - -Inductive singleofint_cases: forall (e: expr), Type := - | singleofint_case1: forall n, singleofint_cases (Eop (Ointconst n) Enil) - | singleofint_default: forall (e: expr), singleofint_cases e. - -Definition singleofint_match (e: expr) := - match e as zz1 return singleofint_cases zz1 with - | Eop (Ointconst n) Enil => singleofint_case1 n - | e => singleofint_default e - end. - -Definition singleofint (e: expr) := - match singleofint_match e with - | singleofint_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Osingleconst (Float32.of_int n)) Enil - | singleofint_default e => - Eop Osingleofint (e ::: Enil) - end. - - -Definition intuofsingle (e: expr) := intuoffloat (floatofsingle e). - -(** Original definition: -<< -Nondetfunction singleofintu (e: expr) := - match e with - | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_intu n)) Enil - | _ => singleoffloat (floatofintu e) - end. ->> -*) - -Inductive singleofintu_cases: forall (e: expr), Type := - | singleofintu_case1: forall n, singleofintu_cases (Eop (Ointconst n) Enil) - | singleofintu_default: forall (e: expr), singleofintu_cases e. - -Definition singleofintu_match (e: expr) := - match e as zz1 return singleofintu_cases zz1 with - | Eop (Ointconst n) Enil => singleofintu_case1 n - | e => singleofintu_default e - end. - -Definition singleofintu (e: expr) := - match singleofintu_match e with - | singleofintu_case1 n => (* Eop (Ointconst n) Enil *) - Eop (Osingleconst (Float32.of_intu n)) Enil - | singleofintu_default e => - singleoffloat (floatofintu e) - end. - - -(** ** Addressing modes *) - -(** Original definition: -<< -Nondetfunction addressing (chunk: memory_chunk) (e: expr) := - match e with - | Eop (Olea addr) args => - if (negb Archi.ptr64) && addressing_valid addr then (addr, args) else (Aindexed 0, e:::Enil) - | Eop (Oleal addr) args => - if Archi.ptr64 && addressing_valid addr then (addr, args) else (Aindexed 0, e:::Enil) - | _ => (Aindexed 0, e:::Enil) - end. ->> -*) - -Inductive addressing_cases: forall (e: expr), Type := - | addressing_case1: forall addr args, addressing_cases (Eop (Olea addr) args) - | addressing_case2: forall addr args, addressing_cases (Eop (Oleal addr) args) - | addressing_default: forall (e: expr), addressing_cases e. - -Definition addressing_match (e: expr) := - match e as zz1 return addressing_cases zz1 with - | Eop (Olea addr) args => addressing_case1 addr args - | Eop (Oleal addr) args => addressing_case2 addr args - | e => addressing_default e - end. - -Definition addressing (chunk: memory_chunk) (e: expr) := - match addressing_match e with - | addressing_case1 addr args => (* Eop (Olea addr) args *) - if (negb Archi.ptr64) && addressing_valid addr then (addr, args) else (Aindexed 0, e:::Enil) - | addressing_case2 addr args => (* Eop (Oleal addr) args *) - if Archi.ptr64 && addressing_valid addr then (addr, args) else (Aindexed 0, e:::Enil) - | addressing_default e => - (Aindexed 0, e:::Enil) - end. - - -(** ** Arguments of builtins *) - -(** Original definition: -<< -Nondetfunction builtin_arg_addr (addr: Op.addressing) (el: exprlist) := - match addr, el with - | Aindexed n, e1 ::: Enil => - BA_addptr (BA e1) (if Archi.ptr64 then BA_long (Int64.repr n) else BA_int (Int.repr n)) - | Aglobal id ofs, Enil => BA_addrglobal id ofs - | Ainstack ofs, Enil => BA_addrstack ofs - | _, _ => BA (Eop (Olea_ptr addr) el) - end. ->> -*) - -Inductive builtin_arg_addr_cases: forall (addr: Op.addressing) (el: exprlist), Type := - | builtin_arg_addr_case1: forall n e1, builtin_arg_addr_cases (Aindexed n) (e1 ::: Enil) - | builtin_arg_addr_case2: forall id ofs, builtin_arg_addr_cases (Aglobal id ofs) (Enil) - | builtin_arg_addr_case3: forall ofs, builtin_arg_addr_cases (Ainstack ofs) (Enil) - | builtin_arg_addr_default: forall (addr: Op.addressing) (el: exprlist), builtin_arg_addr_cases addr el. - -Definition builtin_arg_addr_match (addr: Op.addressing) (el: exprlist) := - match addr as zz1, el as zz2 return builtin_arg_addr_cases zz1 zz2 with - | Aindexed n, e1 ::: Enil => builtin_arg_addr_case1 n e1 - | Aglobal id ofs, Enil => builtin_arg_addr_case2 id ofs - | Ainstack ofs, Enil => builtin_arg_addr_case3 ofs - | addr, el => builtin_arg_addr_default addr el - end. - -Definition builtin_arg_addr (addr: Op.addressing) (el: exprlist) := - match builtin_arg_addr_match addr el with - | builtin_arg_addr_case1 n e1 => (* Aindexed n, e1 ::: Enil *) - BA_addptr (BA e1) (if Archi.ptr64 then BA_long (Int64.repr n) else BA_int (Int.repr n)) - | builtin_arg_addr_case2 id ofs => (* Aglobal id ofs, Enil *) - BA_addrglobal id ofs - | builtin_arg_addr_case3 ofs => (* Ainstack ofs, Enil *) - BA_addrstack ofs - | builtin_arg_addr_default addr el => - BA (Eop (Olea_ptr addr) el) - end. - - -(** Original definition: -<< -Nondetfunction builtin_arg (e: expr) := - match e with - | Eop (Ointconst n) Enil => BA_int n - | Eop (Olongconst n) Enil => BA_long n - | Eop (Olea addr) el => - if Archi.ptr64 then BA e else builtin_arg_addr addr el - | Eop (Oleal addr) el => - if Archi.ptr64 then builtin_arg_addr addr el else BA e - | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => - BA_long (Int64.ofwords h l) - | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) - | Eload chunk (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs - | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs - | _ => BA e - end. ->> -*) - -Inductive builtin_arg_cases: forall (e: expr), Type := - | builtin_arg_case1: forall n, builtin_arg_cases (Eop (Ointconst n) Enil) - | builtin_arg_case2: forall n, builtin_arg_cases (Eop (Olongconst n) Enil) - | builtin_arg_case3: forall addr el, builtin_arg_cases (Eop (Olea addr) el) - | builtin_arg_case4: forall addr el, builtin_arg_cases (Eop (Oleal addr) el) - | builtin_arg_case5: forall h l, builtin_arg_cases (Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil)) - | builtin_arg_case6: forall h l, builtin_arg_cases (Eop Omakelong (h ::: l ::: Enil)) - | builtin_arg_case7: forall chunk id ofs, builtin_arg_cases (Eload chunk (Aglobal id ofs) Enil) - | builtin_arg_case8: forall chunk ofs, builtin_arg_cases (Eload chunk (Ainstack ofs) Enil) - | builtin_arg_default: forall (e: expr), builtin_arg_cases e. - -Definition builtin_arg_match (e: expr) := - match e as zz1 return builtin_arg_cases zz1 with - | Eop (Ointconst n) Enil => builtin_arg_case1 n - | Eop (Olongconst n) Enil => builtin_arg_case2 n - | Eop (Olea addr) el => builtin_arg_case3 addr el - | Eop (Oleal addr) el => builtin_arg_case4 addr el - | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => builtin_arg_case5 h l - | Eop Omakelong (h ::: l ::: Enil) => builtin_arg_case6 h l - | Eload chunk (Aglobal id ofs) Enil => builtin_arg_case7 chunk id ofs - | Eload chunk (Ainstack ofs) Enil => builtin_arg_case8 chunk ofs - | e => builtin_arg_default e - end. - -Definition builtin_arg (e: expr) := - match builtin_arg_match e with - | builtin_arg_case1 n => (* Eop (Ointconst n) Enil *) - BA_int n - | builtin_arg_case2 n => (* Eop (Olongconst n) Enil *) - BA_long n - | builtin_arg_case3 addr el => (* Eop (Olea addr) el *) - if Archi.ptr64 then BA e else builtin_arg_addr addr el - | builtin_arg_case4 addr el => (* Eop (Oleal addr) el *) - if Archi.ptr64 then builtin_arg_addr addr el else BA e - | builtin_arg_case5 h l => (* Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) *) - BA_long (Int64.ofwords h l) - | builtin_arg_case6 h l => (* Eop Omakelong (h ::: l ::: Enil) *) - BA_splitlong (BA h) (BA l) - | builtin_arg_case7 chunk id ofs => (* Eload chunk (Aglobal id ofs) Enil *) - BA_loadglobal chunk id ofs - | builtin_arg_case8 chunk ofs => (* Eload chunk (Ainstack ofs) Enil *) - BA_loadstack chunk ofs - | builtin_arg_default e => - BA e - end. - - -(** Platform-specific known builtins *) - -Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := - None. diff --git a/verilog/SelectOp.vp b/verilog/SelectOp.vp index 31be8c32..2a09207b 100644 --- a/verilog/SelectOp.vp +++ b/verilog/SelectOp.vp @@ -40,6 +40,7 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats Builtins. Require Import Op CminorSel. +Require Import OpHelpers. Require Archi. Local Open Scope cminorsel_scope. @@ -502,7 +503,7 @@ Definition intuoffloat (e: expr) := if Archi.splitlong then Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (CEcond (Ccompf Clt) None (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat else @@ -515,7 +516,7 @@ Nondetfunction floatofintu (e: expr) := if Archi.splitlong then let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in Elet e - (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) + (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) None (Eletvar O ::: Enil)) (floatofint (Eletvar O)) (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)) else @@ -576,6 +577,13 @@ Nondetfunction builtin_arg (e: expr) := | _ => BA e end. +(* floats *) +Definition divf_base (e1: expr) (e2: expr) := + Eop Odivf (e1 ::: e2 ::: Enil). + +Definition divfs_base (e1: expr) (e2: expr) := + Eop Odivfs (e1 ::: e2 ::: Enil). + (** Platform-specific known builtins *) Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := diff --git a/verilog/SelectOpproof.v b/verilog/SelectOpproof.v index d8ab32a4..c43beb56 100644 --- a/verilog/SelectOpproof.v +++ b/verilog/SelectOpproof.v @@ -17,6 +17,8 @@ Require Import AST Integers Floats. Require Import Values Memory Builtins Globalenvs. Require Import Cminor Op CminorSel. Require Import SelectOp. +Require Import OpHelpers. +Require Import OpHelpersproof. Local Open Scope cminorsel_scope. @@ -68,8 +70,10 @@ Ltac TrivialExists := (** * Correctness of the smart constructors *) Section CMCONSTR. - -Variable ge: genv. +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. @@ -1012,6 +1016,27 @@ Proof. - constructor; auto. Qed. +(* floating-point division without HELPERS *) +Theorem eval_divf_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v. +Proof. + intros; unfold divf_base. + TrivialExists. +Qed. + +Theorem eval_divfs_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v. +Proof. + intros; unfold divfs_base. + TrivialExists. +Qed. + (** Platform-specific known builtins *) Theorem eval_platform_builtin: diff --git a/verilog/Stacklayout.v b/verilog/Stacklayout.v index de2a6f10..002b86bf 100644 --- a/verilog/Stacklayout.v +++ b/verilog/Stacklayout.v @@ -15,11 +15,13 @@ Require Import Coqlib. Require Import AST Memory Separation. Require Import Bounds. +Require Archi. Local Open Scope sep_scope. (** The general shape of activation records is as follows, from bottom (lowest offsets) to top: +- For the Win64 ABI: 32 reserved bytes - Space for outgoing arguments to function calls. - Back link to parent frame - Saved values of integer callee-save registers used by the function. @@ -29,11 +31,11 @@ Local Open Scope sep_scope. - Return address. *) -Definition fe_ofs_arg := 0. +Definition fe_ofs_arg := if Archi.win64 then 32 else 0. Definition make_env (b: bounds) : frame_env := let w := if Archi.ptr64 then 8 else 4 in - let olink := align (4 * b.(bound_outgoing)) w in (* back link *) + let olink := align (fe_ofs_arg + 4 * b.(bound_outgoing)) w in (* back link *) let ocs := olink + w in (* callee-saves *) let ol := align (size_callee_save_area b ocs) 8 in (* locals *) let ostkdata := align (ol + 4 * b.(bound_local)) 8 in (* stack data *) @@ -61,7 +63,7 @@ Proof. Local Opaque Z.add Z.mul sepconj range. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). - set (olink := align (4 * b.(bound_outgoing)) w). + set (olink := align (fe_ofs_arg + 4 * b.(bound_outgoing)) w). set (ocs := olink + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). @@ -69,8 +71,9 @@ Local Opaque Z.add Z.mul sepconj range. replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto). assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. + assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; lia). assert (0 <= 4 * b.(bound_outgoing)) by lia. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). assert (olink + w <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). @@ -87,7 +90,7 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap45. rewrite sep_swap34. (* Apply range_split and range_split2 repeatedly *) - unfold fe_ofs_arg. + apply range_drop_left with 0. lia. apply range_split_2. fold olink. lia. lia. apply range_split. lia. apply range_split_2. fold ol. lia. lia. @@ -105,15 +108,16 @@ Lemma frame_env_range: Proof. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). - set (olink := align (4 * b.(bound_outgoing)) w). + set (olink := align (fe_ofs_arg + 4 * b.(bound_outgoing)) w). set (ocs := olink + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. + assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; lia). assert (0 <= 4 * b.(bound_outgoing)) by lia. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). assert (olink + w <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). @@ -133,14 +137,14 @@ Lemma frame_env_aligned: Proof. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). - set (olink := align (4 * b.(bound_outgoing)) w). + set (olink := align (fe_ofs_arg + 4 * b.(bound_outgoing)) w). set (ocs := olink + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). - split. apply Z.divide_0_r. + split. exists (fe_ofs_arg / 8). unfold fe_ofs_arg; destruct Archi.win64; reflexivity. split. apply align_divides; lia. split. apply align_divides; lia. split. apply align_divides; lia. diff --git a/verilog/TargetPrinter.ml b/verilog/TargetPrinter.ml index 8950b8ca..00e70f65 100644 --- a/verilog/TargetPrinter.ml +++ b/verilog/TargetPrinter.ml @@ -95,9 +95,6 @@ let z oc n = output_string oc (Z.to_string n) let data_pointer = if Archi.ptr64 then ".quad" else ".long" -(* The comment deliminiter *) -let comment = "#" - (* Base-2 log of a Caml integer *) let rec log2 n = assert (n > 0); @@ -106,6 +103,7 @@ let rec log2 n = (* System dependent printer functions *) module type SYSTEM = sig + val comment: string val raw_symbol: out_channel -> string -> unit val symbol: out_channel -> P.t -> unit val label: out_channel -> int -> unit @@ -124,6 +122,9 @@ module type SYSTEM = module ELF_System : SYSTEM = struct + (* The comment delimiter *) + let comment = "#" + let raw_symbol oc s = fprintf oc "%s" s @@ -131,7 +132,27 @@ module ELF_System : SYSTEM = let label = elf_label - let name_of_section = fun _ -> assert false + let name_of_section = function + | Section_text -> ".text" + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> + variable_section ~sec:".data" ~bss:".bss" i + | Section_const i | Section_small_const i -> + variable_section ~sec:".section .rodata" i + | Section_string -> ".section .rodata" + | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",\"a%s%s\",@progbits" + s (if wr then "w" else "") (if ex then "x" else "") + | Section_debug_info _ -> ".section .debug_info,\"\",@progbits" + | Section_debug_loc -> ".section .debug_loc,\"\",@progbits" + | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" + | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" + | Section_debug_ranges -> ".section .debug_ranges,\"\",@progbits" + | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" + | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note" let stack_alignment = 16 @@ -147,7 +168,44 @@ module ELF_System : SYSTEM = let print_var_info = elf_print_var_info - let print_epilogue _ = () + let print_atexit oc to_be_called = + if Archi.ptr64 + then + begin + fprintf oc " leaq %s(%%rip), %%rdi\n" to_be_called; + fprintf oc " jmp atexit\n" + end + else + begin + fprintf oc " pushl $%s\n" to_be_called; + fprintf oc " call atexit\n"; + fprintf oc " addl $4, %%esp\n"; + fprintf oc " ret\n" + end + + let x86_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name = + if Archi.ptr64 + then + begin + fprintf oc " leaq %s(%%rip), %%rdx\n" profiling_counter_table_name; + fprintf oc " leaq %s(%%rip), %%rsi\n" profiling_id_table_name; + fprintf oc " movl $%d, %%edi\n" nr_items; + fprintf oc " jmp %s\n" profiling_write_table_helper + end + else + begin + fprintf oc " pushl $%s\n" profiling_counter_table_name; + fprintf oc " pushl $%s\n" profiling_id_table_name; + fprintf oc " pushl $%d\n" nr_items; + fprintf oc " call %s\n" profiling_write_table_helper ; + fprintf oc " addl $12, %%esp\n"; + fprintf oc " ret\n" + end;; + + let print_epilogue oc = + print_profiling_epilogue elf_text_print_fun_info (Init_atexit print_atexit) x86_profiling_stub oc;; let print_comm_decl oc name sz al = fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al @@ -162,6 +220,10 @@ module ELF_System : SYSTEM = module MacOS_System : SYSTEM = struct + (* The comment delimiter. + `##` instead of `#` to please the Clang assembler. *) + let comment = "##" + let raw_symbol oc s = fprintf oc "_%s" s @@ -171,7 +233,28 @@ module MacOS_System : SYSTEM = let label oc lbl = fprintf oc "L%d" lbl - let name_of_section = fun _ -> assert false + let name_of_section = function + | Section_text -> ".text" + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> + variable_section ~sec:".data" i + | Section_const i | Section_small_const i -> + variable_section ~sec:".const" ~reloc:".const_data" i + | Section_string -> ".const" + | Section_literal -> ".const" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\", %s, %s" + (if wr then "__DATA" else "__TEXT") s + (if ex then "regular, pure_instructions" else "regular") + | Section_debug_info _ -> ".section __DWARF,__debug_info,regular,debug" + | Section_debug_loc -> ".section __DWARF,__debug_loc,regular,debug" + | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug" + | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug" + | Section_debug_ranges -> ".section __DWARF,__debug_ranges,regular,debug" + | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" + | Section_ais_annotation -> assert false (* Not supported under MacOS *) let stack_alignment = 16 (* mandatory *) @@ -202,8 +285,14 @@ module MacOS_System : SYSTEM = module Cygwin_System : SYSTEM = struct + (* The comment delimiter *) + let comment = "#" + + let symbol_prefix = + if Archi.ptr64 then "" else "_" + let raw_symbol oc s = - fprintf oc "_%s" s + fprintf oc "%s%s" symbol_prefix s let symbol oc symb = raw_symbol oc (extern_atom symb) @@ -211,21 +300,61 @@ module Cygwin_System : SYSTEM = let label oc lbl = fprintf oc "L%d" lbl - let name_of_section = fun _ -> assert false - - let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) + let name_of_section = function + | Section_text -> ".text" + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> + variable_section ~sec:".data" ~bss:".bss" i + | Section_const i | Section_small_const i -> + variable_section ~sec:".section .rdata,\"dr\"" i + | Section_string -> ".section .rdata,\"dr\"" + | Section_literal -> ".section .rdata,\"dr\"" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section %s, \"%s\"\n" + s (if ex then "xr" else if wr then "d" else "dr") + | Section_debug_info _ -> ".section .debug_info,\"dr\"" + | Section_debug_loc -> ".section .debug_loc,\"dr\"" + | Section_debug_line _ -> ".section .debug_line,\"dr\"" + | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" + | Section_debug_ranges -> ".section .debug_ranges,\"dr\"" + | Section_debug_str-> assert false (* Should not be used *) + | Section_ais_annotation -> assert false (* Not supported for coff binaries *) + + let stack_alignment = 8 + (* minimum is 4 for 32 bits, 8 for 64 bits; 8 is better for perfs *) let print_align oc n = fprintf oc " .balign %d\n" n + let indirect_symbols : StringSet.t ref = ref StringSet.empty + let print_mov_rs oc rd id = - fprintf oc " movl $%a, %a\n" symbol id ireg rd + if Archi.ptr64 then begin + let s = extern_atom id in + indirect_symbols := StringSet.add s !indirect_symbols; + fprintf oc " movq .refptr.%s(%%rip), %a\n" s ireg rd + end else begin + fprintf oc " movl $%a, %a\n" symbol id ireg rd + end let print_fun_info _ _ = () let print_var_info _ _ = () - let print_epilogue _ = () + let declare_indirect_symbol oc s = + fprintf oc " .section .rdata$.refptr.%s, \"dr\"\n" s; + fprintf oc " .globl .refptr.%s\n" s; + fprintf oc " .linkonce discard\n"; + fprintf oc ".refptr.%s:\n" s; + fprintf oc " .quad %s\n" s + + let print_epilogue oc = + if Archi.ptr64 then begin + StringSet.iter (declare_indirect_symbol oc) !indirect_symbols; + indirect_symbols := StringSet.empty + end let print_comm_decl oc name sz al = fprintf oc " .comm %a, %s, %d\n" @@ -233,7 +362,8 @@ module Cygwin_System : SYSTEM = let print_lcomm_decl oc name sz al = fprintf oc " .lcomm %a, %s, %d\n" - symbol name (Z.to_string sz) (log2 al) + symbol name (Z.to_string sz) + (if Archi.ptr64 then al else log2 al) end @@ -322,8 +452,28 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%a(%%rip)" label lbl end - - + let print_profiling_logger oc id kind = + assert (kind >= 0); + assert (kind <= 1); + let ofs = profiling_offset id kind in + if Archi.ptr64 + then + begin + fprintf oc "%s profiling %a %d: atomic increment\n" comment + Profilingaux.pp_id id kind; + fprintf oc " lock addq $1, %s+%d(%%rip)\n" + profiling_counter_table_name ofs + end + else + begin + fprintf oc "%s begin profiling %a %d: increment\n" comment + Profilingaux.pp_id id kind; + fprintf oc " addl $1, %s+%d\n" profiling_counter_table_name ofs; + fprintf oc " adcl $1, %s+%d\n" profiling_counter_table_name (ofs+4); + fprintf oc "%s end profiling %a %d: increment\n" comment + Profilingaux.pp_id id kind; + end + (* Printing of instructions *) (* Reminder on X86 assembly syntaxes: @@ -654,7 +804,7 @@ module Target(System: SYSTEM):TARGET = | Pret -> if (not Archi.ptr64) && (!current_function_sig).sig_cc.cc_structret then begin - fprintf oc " movl 0(%%esp), %%eax\n"; + fprintf oc " movl 4(%%esp), %%eax\n"; fprintf oc " ret $4\n" end else begin fprintf oc " ret\n" @@ -714,6 +864,8 @@ module Target(System: SYSTEM):TARGET = fprintf oc " minsd %a, %a\n" freg a1 freg res | Pmovb_rm (rd,a) -> fprintf oc " movb %a, %a\n" addressing a ireg8 rd + | Pmovq_rf (rd, r1) -> + fprintf oc " movq %a, %a\n" freg r1 ireg64 rd | Pmovsq_mr(a, rs) -> fprintf oc " movq %a, %a\n" freg rs addressing a | Pmovsq_rm(rd, a) -> @@ -761,6 +913,8 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment + | EF_profiling(id, coq_kind) -> + print_profiling_logger oc id (Z.to_int coq_kind) | _ -> assert false end @@ -832,7 +986,23 @@ module Target(System: SYSTEM):TARGET = end let print_epilogue oc = - assert false + if !need_masks then begin + section oc Section_literal; + print_align oc 16; + fprintf oc "%a: .quad 0x8000000000000000, 0\n" + raw_symbol "__negd_mask"; + fprintf oc "%a: .quad 0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n" + raw_symbol "__absd_mask"; + fprintf oc "%a: .long 0x80000000, 0, 0, 0\n" + raw_symbol "__negs_mask"; + fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" + raw_symbol "__abss_mask" + end; + System.print_epilogue oc; + if !Clflags.option_g then begin + Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); + section oc Section_text; + end let comment = comment @@ -847,7 +1017,7 @@ end let sel_target () = let module S = (val (match Configuration.system with | "linux" | "bsd" -> (module ELF_System:SYSTEM) - | "macosx" -> (module MacOS_System:SYSTEM) + | "macos" -> (module MacOS_System:SYSTEM) | "cygwin" -> (module Cygwin_System:SYSTEM) | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") ):SYSTEM) in (module Target(S):TARGET) diff --git a/verilog/ValueAOp.v b/verilog/ValueAOp.v index d0b8427a..e5584b6a 100644 --- a/verilog/ValueAOp.v +++ b/verilog/ValueAOp.v @@ -261,6 +261,25 @@ Proof. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. apply select_sound; auto. eapply eval_static_condition_sound; eauto. Qed. - +(* +Theorem eval_static_addressing_sound_none: + forall addr vargs aargs, + eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = None -> + list_forall2 (vmatch bc) vargs aargs -> + (eval_static_addressing addr aargs) = Vbot. +Proof. + unfold eval_addressing, eval_static_addressing. + intros until aargs. intros Heval_none Hlist. + destruct (Archi.ptr64). + inv Hlist. + destruct addr; trivial; discriminate. + inv H0. + destruct addr; trivial; try discriminate. simpl in *. + inv H2. + destruct addr; trivial; discriminate. + inv H3; + destruct addr; trivial; discriminate. +Qed. +*) End SOUNDNESS. diff --git a/verilog/extractionMachdep.v b/verilog/extractionMachdep.v index a29553e8..26a3f0a7 100644 --- a/verilog/extractionMachdep.v +++ b/verilog/extractionMachdep.v @@ -6,24 +6,29 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) (* Additional extraction directives specific to the x86-64 port *) -Require SelectOp ConstpropOp. +Require Archi SelectOp. -(* SelectOp *) - -Extract Constant SelectOp.symbol_is_external => - "fun id -> Configuration.system = ""macosx"" && C2C.atom_is_extern id". +(* Archi *) -(* ConstpropOp *) +Extract Constant Archi.win64 => + "match Configuration.system with + | ""cygwin"" when ptr64 -> true + | _ -> false". -Extract Constant ConstpropOp.symbol_is_external => - "fun id -> Configuration.system = ""macosx"" && C2C.atom_is_extern id". +(* SelectOp *) +Extract Constant SelectOp.symbol_is_external => + "match Configuration.system with + | ""macos"" -> C2C.atom_is_extern + | ""cygwin"" when Archi.ptr64 -> C2C.atom_is_extern + | _ -> (fun _ -> false)". |