diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
commit | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch) | |
tree | 4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /riscV | |
parent | 21c979fce33b068ce4b86e67d3d866b203411c6c (diff) | |
parent | 02b169b444c435b8d1aacf54969dd7de57317a5c (diff) | |
download | compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'riscV')
-rw-r--r-- | riscV/Archi.v | 9 | ||||
-rw-r--r-- | riscV/Asm.v | 4 | ||||
-rw-r--r-- | riscV/Asmexpand.ml | 188 | ||||
-rw-r--r-- | riscV/Asmgenproof.v | 18 | ||||
-rw-r--r-- | riscV/Asmgenproof1.v | 22 | ||||
-rw-r--r-- | riscV/Builtins1.v | 9 | ||||
-rw-r--r-- | riscV/CBuiltins.ml | 9 | ||||
-rw-r--r-- | riscV/ConstpropOpproof.v | 2 | ||||
-rw-r--r-- | riscV/Conventions1.v | 160 | ||||
-rw-r--r-- | riscV/ExpansionOracle.ml | 39 | ||||
-rw-r--r-- | riscV/NeedOp.v | 4 | ||||
-rw-r--r-- | riscV/RTLpathSE_simplify.v | 14 | ||||
-rw-r--r-- | riscV/SelectOpproof.v | 28 | ||||
-rw-r--r-- | riscV/Stacklayout.v | 50 | ||||
-rw-r--r-- | riscV/TargetPrinter.ml | 8 | ||||
-rw-r--r-- | riscV/ValueAOp.v | 4 | ||||
-rw-r--r-- | riscV/extractionMachdep.v | 9 |
17 files changed, 344 insertions, 233 deletions
diff --git a/riscV/Archi.v b/riscV/Archi.v index 1bb80e89..96f34276 100644 --- a/riscV/Archi.v +++ b/riscV/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. *) (* *) (* *********************************************************************) diff --git a/riscV/Asm.v b/riscV/Asm.v index a16f57b5..c80c6cc2 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -1092,7 +1092,7 @@ Inductive step: state -> trace -> state -> Prop := rs' = nextinstr (set_res res vres (undef_regs (map preg_of (destroyed_by_builtin ef)) - (rs#X31 <- Vundef))) -> + (rs #X1 <- Vundef #X31 <- Vundef))) -> step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', @@ -1173,7 +1173,7 @@ Ltac Equalities := split. auto. intros. destruct B; auto. subst. auto. - (* trace length *) red; intros. inv H; simpl. - omega. + lia. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. - (* initial states *) diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index c5cd6817..50dc20be 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -24,6 +24,7 @@ open Asmexpandaux open AST open Camlcoq open! Integers +open Locations exception Error of string @@ -50,6 +51,86 @@ let expand_addptrofs dst src n = let expand_storeind_ptr src base ofs = List.iter emit (Asmgen.storeind_ptr src base ofs []) +(* Fix-up code around function calls and function entry. + Some floating-point arguments residing in FP registers need to be + moved to integer registers or register pairs. + Symmetrically, some floating-point parameter passed in integer + registers or register pairs need to be moved to FP registers. *) + +let int_param_regs = [| X10; X11; X12; X13; X14; X15; X16; X17 |] + +let move_single_arg fr i = + emit (Pfmvxs(int_param_regs.(i), fr)) + +let move_double_arg fr i = + if Archi.ptr64 then begin + emit (Pfmvxd(int_param_regs.(i), fr)) + end else begin + emit (Paddiw(X2, X X2, Integers.Int.neg _16)); + emit (Pfsd(fr, X2, Ofsimm _0)); + emit (Plw(int_param_regs.(i), X2, Ofsimm _0)); + if i < 7 then begin + emit (Plw(int_param_regs.(i + 1), X2, Ofsimm _4)) + end else begin + emit (Plw(X31, X2, Ofsimm _4)); + emit (Psw(X31, X2, Ofsimm _16)) + end; + emit (Paddiw(X2, X X2, _16)) + end + +let move_single_param fr i = + emit (Pfmvsx(fr, int_param_regs.(i))) + +let move_double_param fr i = + if Archi.ptr64 then begin + emit (Pfmvdx(fr, int_param_regs.(i))) + end else begin + emit (Paddiw(X2, X X2, Integers.Int.neg _16)); + emit (Psw(int_param_regs.(i), X2, Ofsimm _0)); + if i < 7 then begin + emit (Psw(int_param_regs.(i + 1), X2, Ofsimm _4)) + end else begin + emit (Plw(X31, X2, Ofsimm _16)); + emit (Psw(X31, X2, Ofsimm _4)) + end; + emit (Pfld(fr, X2, Ofsimm _0)); + emit (Paddiw(X2, X X2, _16)) + end + +let float_extra_index = function + | Machregs.F0 -> Some (F0, 0) + | Machregs.F1 -> Some (F1, 1) + | Machregs.F2 -> Some (F2, 2) + | Machregs.F3 -> Some (F3, 3) + | Machregs.F4 -> Some (F4, 4) + | Machregs.F5 -> Some (F5, 5) + | Machregs.F6 -> Some (F6, 6) + | Machregs.F7 -> Some (F7, 7) + | _ -> None + +let fixup_gen single double sg = + let fixup ty loc = + match ty, loc with + | Tsingle, One (R r) -> + begin match float_extra_index r with + | Some(r, i) -> single r i + | None -> () + end + | (Tfloat | Tany64), One (R r) -> + begin match float_extra_index r with + | Some(r, i) -> double r i + | None -> () + end + | _, _ -> () + in + List.iter2 fixup sg.sig_args (Conventions1.loc_arguments sg) + +let fixup_call sg = + fixup_gen move_single_arg move_double_arg sg + +let fixup_function_entry sg = + fixup_gen move_single_param move_double_param sg + (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; @@ -57,51 +138,6 @@ let expand_storeind_ptr src base ofs = registers. *) -(* Fix-up code around calls to variadic functions. Floating-point arguments - residing in FP registers need to be moved to integer registers. *) - -let int_param_regs = [| X10; X11; X12; X13; X14; X15; X16; X17 |] -let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |] - -let rec fixup_variadic_call ri rf tyl = - if ri < 8 then - match tyl with - | [] -> - () - | (Tint | Tany32) :: tyl -> - fixup_variadic_call (ri + 1) rf tyl - | Tsingle :: tyl -> - let rs = float_param_regs.(rf) - and rd = int_param_regs.(ri) in - emit (Pfmvxs(rd, rs)); - fixup_variadic_call (ri + 1) (rf + 1) tyl - | Tlong :: tyl -> - let ri' = if Archi.ptr64 then ri + 1 else align ri 2 + 2 in - fixup_variadic_call ri' rf tyl - | (Tfloat | Tany64) :: tyl -> - if Archi.ptr64 then begin - let rs = float_param_regs.(rf) - and rd = int_param_regs.(ri) in - emit (Pfmvxd(rd, rs)); - fixup_variadic_call (ri + 1) (rf + 1) tyl - end else begin - let ri = align ri 2 in - if ri < 8 then begin - let rs = float_param_regs.(rf) - and rd1 = int_param_regs.(ri) - and rd2 = int_param_regs.(ri + 1) in - emit (Paddiw(X2, X X2, Integers.Int.neg _16)); - emit (Pfsd(rs, X2, Ofsimm _0)); - emit (Plw(rd1, X2, Ofsimm _0)); - emit (Plw(rd2, X2, Ofsimm _4)); - emit (Paddiw(X2, X X2, _16)); - fixup_variadic_call (ri + 2) (rf + 1) tyl - end - end - -let fixup_call sg = - if sg.sig_cc.cc_vararg then fixup_variadic_call 0 0 sg.sig_args - (* Handling of annotations *) let expand_annot_val kind txt targ args res = @@ -305,18 +341,53 @@ let expand_builtin_vstore chunk args = (* Handling of varargs *) -(* Size in words of the arguments to a function. This includes both - arguments passed in registers and arguments passed on stack. *) +(* Number of integer registers, FP registers, and stack words + used to pass the (fixed) arguments to a function. *) + +let arg_int_size ri rf ofs k = + if ri < 8 + then k (ri + 1) rf ofs + else k ri rf (ofs + 1) + +let arg_single_size ri rf ofs k = + if rf < 8 + then k ri (rf + 1) ofs + else arg_int_size ri rf ofs k + +let arg_long_size ri rf ofs k = + if Archi.ptr64 then + if ri < 8 + then k (ri + 1) rf ofs + else k ri rf (ofs + 1) + else + if ri < 7 then k (ri + 2) rf ofs + else if ri = 7 then k (ri + 1) rf (ofs + 1) + else k ri rf (align ofs 2 + 2) + +let arg_double_size ri rf ofs k = + if rf < 8 + then k ri (rf + 1) ofs + else arg_long_size ri rf ofs k + +let rec args_size l ri rf ofs = + match l with + | [] -> (ri, rf, ofs) + | (Tint | Tany32) :: l -> + arg_int_size ri rf ofs (args_size l) + | Tsingle :: l -> + arg_single_size ri rf ofs (args_size l) + | Tlong :: l -> + arg_long_size ri rf ofs (args_size l) + | (Tfloat | Tany64) :: l -> + arg_double_size ri rf ofs (args_size l) -let rec args_size sz = function - | [] -> sz - | (Tint | Tsingle | Tany32) :: l -> - args_size (sz + 1) l - | (Tlong | Tfloat | Tany64) :: l -> - args_size (if Archi.ptr64 then sz + 1 else align sz 2 + 2) l +(* Size in words of the arguments to a function. This includes both + arguments passed in integer registers and arguments passed on stack, + but not arguments passed in FP registers. *) let arguments_size sg = - args_size 0 sg.sig_args + let (ri, _, ofs) = args_size sg.sig_args 0 0 0 in + ri + ofs let save_arguments first_reg base_ofs = for i = first_reg to 7 do @@ -575,8 +646,12 @@ let expand_builtin_inline name args res = (fun rl -> emit (Pmulw (rl, X a, X b)); emit (Pmulhuw (rh, X a, X b))) + (* No operation *) | "__builtin_nop", [], _ -> emit Pnop + (* Optimization hint *) + | "__builtin_unreachable", [], _ -> + () (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) @@ -628,7 +703,7 @@ let expand_instruction instr = | Pallocframe (sz, ofs) -> let sg = get_current_function_sig() in emit (Pmv (X30, X2)); - if sg.sig_cc.cc_vararg then begin + if (sg.sig_cc.cc_vararg <> None) then begin let n = arguments_size sg in let extra_sz = if n >= 8 then 0 else align ((8 - n) * wordsize) 16 in let full_sz = Z.add sz (Z.of_uint extra_sz) in @@ -646,7 +721,7 @@ let expand_instruction instr = | Pfreeframe (sz, ofs) -> let sg = get_current_function_sig() in let extra_sz = - if sg.sig_cc.cc_vararg then begin + if (sg.sig_cc.cc_vararg <> None) then begin let n = arguments_size sg in if n >= 8 then 0 else align ((8 - n) * wordsize) 16 end else 0 in @@ -746,6 +821,7 @@ let preg_to_dwarf = function let expand_function id fn = try set_current_function fn; + fixup_function_entry fn.fn_sig; expand id (* sp= *) 2 preg_to_dwarf expand_instruction fn.fn_code; Errors.OK (get_current_function ()) with Error s -> diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 509eac94..e59c4535 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -67,7 +67,7 @@ Lemma transf_function_no_overflow: transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned. Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. - omega. + lia. Qed. Lemma exec_straight_exec: @@ -460,8 +460,8 @@ Proof. split. unfold goto_label. rewrite P. rewrite H1. auto. split. rewrite Pregmap.gss. constructor; auto. rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. - auto. omega. - generalize (transf_function_no_overflow _ _ H0). omega. + auto. lia. + generalize (transf_function_no_overflow _ _ H0). lia. intros. apply Pregmap.gso; auto. Qed. @@ -869,13 +869,15 @@ Local Transparent destroyed_by_op. econstructor; eauto. instantiate (2 := tf); instantiate (1 := x). unfold nextinstr. rewrite Pregmap.gss. - rewrite set_res_other. rewrite undef_regs_other_2. rewrite Pregmap.gso by congruence. + rewrite set_res_other. rewrite undef_regs_other_2. + rewrite ! Pregmap.gso by congruence. rewrite <- H1. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. rewrite preg_notin_charact. intros. auto with asmgen. auto with asmgen. apply agree_nextinstr. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. apply Pregmap.gso; auto with asmgen. + eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. + rewrite ! Pregmap.gso; auto with asmgen. congruence. - (* Mgoto *) @@ -982,10 +984,10 @@ Local Transparent destroyed_by_op. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. rewrite F. reflexivity. reflexivity. eexact U. } - exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor. + exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor. intros (ofs' & X & Y). left; exists (State rs3 m3'); split. - eapply exec_straight_steps_1; eauto. omega. constructor. + eapply exec_straight_steps_1; eauto. lia. constructor. econstructor; eauto. rewrite X; econstructor; eauto. apply agree_exten with rs2; eauto with asmgen. @@ -1014,7 +1016,7 @@ Local Transparent destroyed_at_function_entry. - (* return *) inv STACKS. simpl in *. - right. split. omega. split. auto. + right. split. lia. split. auto. rewrite <- ATPC in H5. econstructor; eauto. congruence. Qed. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 2293e001..42ab8375 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -35,7 +35,7 @@ Proof. - set (m := Int.sub n lo). assert (A: eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto). assert (B: eqmod (two_p 12) (Int.unsigned n - Int.unsigned lo) 0). - { replace 0 with (Int.unsigned n - Int.unsigned n) by omega. + { replace 0 with (Int.unsigned n - Int.unsigned n) by lia. auto using eqmod_sub, eqmod_refl. } assert (C: eqmod (two_p 12) (Int.unsigned m) 0). { apply eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto. @@ -45,7 +45,7 @@ Proof. { apply eqmod_mod_eq in C. unfold Int.modu. change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C. reflexivity. - apply two_p_gt_ZERO; omega. } + apply two_p_gt_ZERO; lia. } rewrite <- (Int.divu_pow2 m (Int.repr 4096) (Int.repr 12)) by auto. rewrite Int.shl_mul_two_p. change (two_p (Int.unsigned (Int.repr 12))) with 4096. @@ -88,7 +88,7 @@ Proof. intros. apply ireg_of_not_X31 in H. congruence. Qed. -Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen. +Global Hint Resolve ireg_of_not_X31 ireg_of_not_X31': asmgen. (** Useful simplification tactic *) @@ -821,18 +821,18 @@ Proof. unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. unfold Int.lt. rewrite zlt_false. auto. change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed. - generalize (Int.signed_range i); omega. + generalize (Int.signed_range i); lia. * exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). exists rs1; split. eexact A1. split; auto. rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto. unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int.add_signed. symmetry; apply Int.signed_repr. assert (Int.signed n <> Int.max_signed). { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. + generalize (Int.signed_range n); lia. + apply DFL. + apply DFL. Qed. @@ -919,18 +919,18 @@ Proof. unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. unfold Int64.lt. rewrite zlt_false. auto. change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed. - generalize (Int64.signed_range i); omega. + generalize (Int64.signed_range i); lia. * exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). exists rs1; split. eexact A1. split; auto. rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto. unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. assert (Int64.signed n <> Int64.max_signed). { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. + generalize (Int64.signed_range n); lia. + apply DFL. + apply DFL. Qed. diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v index 47bacffa..6691d15c 100644 --- a/riscV/Builtins1.v +++ b/riscV/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/riscV/CBuiltins.ml b/riscV/CBuiltins.ml index 00b44fd5..ca0dbc6d 100644 --- a/riscV/CBuiltins.ml +++ b/riscV/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. *) (* *) (* *********************************************************************) diff --git a/riscV/ConstpropOpproof.v b/riscV/ConstpropOpproof.v index 26a50317..74dc4a05 100644 --- a/riscV/ConstpropOpproof.v +++ b/riscV/ConstpropOpproof.v @@ -365,7 +365,7 @@ Proof. Int.bit_solve. destruct (zlt i0 n0). replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)). rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. - rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. + rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. rewrite H6 by auto. auto. econstructor; split; eauto. auto. diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index 17326139..eeaae3c4 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -172,25 +172,29 @@ Qed. (** ** Location of function arguments *) (** The RISC-V ABI states the following conventions for passing arguments - to a function: + to a function. First for non-variadic functions: -- RV64, not variadic: pass the first 8 integer arguments in - integer registers (a1...a8: int_param_regs), the first 8 FP arguments - in FP registers (fa1...fa8: float_param_regs), and the remaining - arguments on the stack, in 8-byte slots. +- RV64: pass the first 8 integer arguments in integer registers + (a1...a8: int_param_regs), the first 8 FP arguments in FP registers + (fa1...fa8: float_param_regs) then in integer registers (a1...a8), + and the remaining arguments on the stack, in 8-byte slots. -- RV32, not variadic: same, but arguments of 64-bit integer type - are passed in two consecutive integer registers (a(i), a(i+1)) - or in a(8) and on a 32-bit word on the stack. Stack-allocated - arguments are aligned to their natural alignment. +- RV32: same, but arguments of size 64 bits that must be passed in + integer registers are passed in two consecutive integer registers + (a(i), a(i+1)), or in a(8) and on a 32-bit word on the stack. + Stack-allocated arguments are aligned to their natural alignment. -- RV64, variadic: pass the first 8 arguments in integer registers - (a1...a8), including FP arguments; pass the remaining arguments on - the stack, in 8-byte slots. +For variadic functions, the fixed arguments are passed as described +above, then the variadic arguments receive special treatment: -- RV32, variadic: same, but arguments of 64-bit types (integers as well +- RV64: FP registers are not used for passing variadic arguments. + All variadic arguments, including FP arguments, are passed in the + remaining integer registers (a1...a8), then on the stack, in 8-byte + slots. + +- RV32: likewise, but arguments of 64-bit types (integers as well as floats) are passed in two consecutive aligned integer registers - (a(2i), a(2i+1)). + (a(2i), a(2i+1)), or on the stack, in aligned 8-byte slots. The passing of FP arguments to variadic functions in integer registers doesn't quite fit CompCert's model. We do our best by passing the FP @@ -204,6 +208,15 @@ Definition int_param_regs := Definition float_param_regs := F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: F16 :: F17 :: nil. +(** To evaluate FP arguments that must be passed in integer registers, + we can use any FP caller-save register that is not already used to pass + a fixed FP argument. Since there are 8 integer registers for argument + passing, we need at most 8 extra more FP registers for these FP + arguments. *) + +Definition float_extra_param_regs := + F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil. + Definition int_arg (ri rf ofs: Z) (ty: typ) (rec: Z -> Z -> Z -> list (rpair loc)) := match list_nth_z int_param_regs ri with @@ -217,26 +230,27 @@ Definition int_arg (ri rf ofs: Z) (ty: typ) Definition float_arg (va: bool) (ri rf ofs: Z) (ty: typ) (rec: Z -> Z -> Z -> list (rpair loc)) := - match list_nth_z float_param_regs rf with + match list_nth_z (if va then nil else float_param_regs) rf with | Some r => - if va then - (let ri' := (* reserve 1 or 2 aligned integer registers *) - if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2 in - if zle ri' 8 then - (* we have enough integer registers, put argument in FP reg - and fixup code will put it in one or two integer regs *) - One (R r) :: rec ri' (rf + 1) ofs - else - (* we are out of integer registers, pass argument on stack *) + One (R r) :: rec ri (rf + 1) ofs + | None => + (* We are out of FP registers, or cannot use them because vararg, + so try to put the argument in an extra FP register while + reserving an integer register or register pair into which + fixup code will move the extra FP register. *) + let regpair := negb Archi.ptr64 && zeq (typesize ty) 2 in + let ri' := if va && regpair then align ri 2 else ri in + match list_nth_z float_extra_param_regs ri' with + | Some r => + let ri'' := ri' + (if Archi.ptr64 then 1 else typesize ty) in + let ofs'' := if regpair && zeq ri' 7 then ofs + 1 else ofs in + One (R r) :: rec ri'' rf ofs'' + | None => + (* We are out of integer registers, pass argument on stack *) let ofs := align ofs (typesize ty) in One(S Outgoing ofs ty) - :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty))) - else - One (R r) :: rec ri (rf + 1) ofs - | None => - let ofs := align ofs (typesize ty) in - One(S Outgoing ofs ty) - :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty)) + :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty)) + end end. Definition split_long_arg (va: bool) (ri rf ofs: Z) @@ -253,35 +267,43 @@ Definition split_long_arg (va: bool) (ri rf ofs: Z) rec ri rf (ofs + 2) end. -Fixpoint loc_arguments_rec (va: bool) - (tyl: list typ) (ri rf ofs: Z) {struct tyl} : list (rpair loc) := +Fixpoint loc_arguments_rec + (tyl: list typ) (fixed ri rf ofs: Z) {struct tyl} : list (rpair loc) := match tyl with | nil => nil | (Tint | Tany32) as ty :: tys => (* pass in one integer register or on stack *) - int_arg ri rf ofs ty (loc_arguments_rec va tys) + int_arg ri rf ofs ty (loc_arguments_rec tys (fixed - 1)) | Tsingle as ty :: tys => (* pass in one FP register or on stack. If vararg, reserve 1 integer register. *) - float_arg va ri rf ofs ty (loc_arguments_rec va tys) + float_arg (zle fixed 0) ri rf ofs ty (loc_arguments_rec tys (fixed - 1)) | Tlong as ty :: tys => if Archi.ptr64 then (* pass in one integer register or on stack *) - int_arg ri rf ofs ty (loc_arguments_rec va tys) + int_arg ri rf ofs ty (loc_arguments_rec tys (fixed - 1)) else (* pass in register pair or on stack; align register pair if vararg *) - split_long_arg va ri rf ofs(loc_arguments_rec va tys) + split_long_arg (zle fixed 0) ri rf ofs(loc_arguments_rec tys (fixed - 1)) | (Tfloat | Tany64) as ty :: tys => (* pass in one FP register or on stack. If vararg, reserve 1 or 2 integer registers. *) - float_arg va ri rf ofs ty (loc_arguments_rec va tys) + float_arg (zle fixed 0) ri rf ofs ty (loc_arguments_rec tys (fixed - 1)) + end. + +(** Number of fixed arguments for a function with signature [s]. *) + +Definition fixed_arguments (s: signature) : Z := + match s.(sig_cc).(cc_vararg) with + | Some n => n + | None => list_length_z s.(sig_args) end. (** [loc_arguments s] returns the list of locations where to store arguments when calling a function with signature [s]. *) Definition loc_arguments (s: signature) : list (rpair loc) := - loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0 0. + loc_arguments_rec s.(sig_args) (fixed_arguments s) 0 0 0. (** Argument locations are either non-temporary registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -306,17 +328,19 @@ Proof. { decide_goal. } assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false). { decide_goal. } + assert (CSFX: forall r, In r float_extra_param_regs -> is_callee_save r = false). + { decide_goal. } assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0). { intros. assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos). - omega. } + lia. } assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))). { intros. eapply Z.divide_trans. apply typealign_typesize. apply align_divides. apply typesize_pos. } assert (SK: (if Archi.ptr64 then 2 else 1) > 0). - { destruct Archi.ptr64; omega. } + { destruct Archi.ptr64; lia. } assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0). - { intros. destruct Archi.ptr64. omega. apply typesize_pos. } + { intros. destruct Archi.ptr64. lia. apply typesize_pos. } assert (A: forall ri rf ofs ty f, OKF f -> ofs >= 0 -> OK (int_arg ri rf ofs ty f)). { intros until f; intros OF OO; red; unfold int_arg; intros. @@ -325,23 +349,22 @@ Proof. - eapply OF; eauto. - subst p; simpl. auto using align_divides, typealign_pos. - eapply OF; [idtac|eauto]. - generalize (AL ofs ty OO) (SKK ty); omega. + generalize (AL ofs ty OO) (SKK ty); lia. } assert (B: forall va ri rf ofs ty f, OKF f -> ofs >= 0 -> OK (float_arg va ri rf ofs ty f)). { intros until f; intros OF OO; red; unfold float_arg; intros. - destruct (list_nth_z float_param_regs rf) as [r|] eqn:NTH. - - set (ri' := if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2) in *. - destruct va; [destruct (zle ri' 8)|idtac]; destruct H. - + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto. - + eapply OF; eauto. - + subst p; repeat split; auto. - + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega. - + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto. - + eapply OF; eauto. + destruct (list_nth_z (if va then nil else float_param_regs) rf) as [r|] eqn:NTH. - destruct H. - + subst p; repeat split; auto. - + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega. + + subst p; simpl. apply CSF. destruct va. simpl in NTH; discriminate. eapply list_nth_z_in; eauto. + + eapply OF; eauto. + - set (regpair := negb Archi.ptr64 && zeq (typesize ty) 2) in *. + set (ri' := if va && regpair then align ri 2 else ri) in *. + destruct (list_nth_z float_extra_param_regs ri') as [r|] eqn:NTH'; destruct H. + + subst p; simpl. apply CSFX. eapply list_nth_z_in; eauto. + + eapply OF; [|eauto]. destruct (regpair && zeq ri' 7); lia. + + subst p; simpl. auto. + + eapply OF; [|eauto]. generalize (AL ofs ty OO) (SKK ty); lia. } assert (C: forall va ri rf ofs f, OKF f -> ofs >= 0 -> OK (split_long_arg va ri rf ofs f)). @@ -353,35 +376,35 @@ Proof. [destruct (list_nth_z int_param_regs (ri'+1)) as [r2|] eqn:NTH2 | idtac]. - red; simpl; intros; destruct H. + subst p; split; apply CSI; eauto using list_nth_z_in. - + eapply OF; [idtac|eauto]. omega. + + eapply OF; [idtac|eauto]. lia. - red; simpl; intros; destruct H. + subst p; split. split; auto using Z.divide_1_l. apply CSI; eauto using list_nth_z_in. - + eapply OF; [idtac|eauto]. omega. + + eapply OF; [idtac|eauto]. lia. - red; simpl; intros; destruct H. - + subst p; repeat split; auto using Z.divide_1_l. omega. - + eapply OF; [idtac|eauto]. omega. + + subst p; repeat split; auto using Z.divide_1_l. lia. + + eapply OF; [idtac|eauto]. lia. } - cut (forall va tyl ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl ri rf ofs)). + cut (forall tyl fixed ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec tyl fixed ri rf ofs)). unfold OK. eauto. induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl. - red; simpl; tauto. - destruct ty1. -+ (* int *) apply A; auto. -+ (* float *) apply B; auto. ++ (* int *) apply A; unfold OKF; auto. ++ (* float *) apply B; unfold OKF; auto. + (* long *) destruct Archi.ptr64. - apply A; auto. - apply C; auto. -+ (* single *) apply B; auto. -+ (* any32 *) apply A; auto. -+ (* any64 *) apply B; auto. + apply A; unfold OKF; auto. + apply C; unfold OKF; auto. ++ (* single *) apply B; unfold OKF; auto. ++ (* any32 *) apply A; unfold OKF; auto. ++ (* any64 *) apply B; unfold OKF; auto. Qed. 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. eapply loc_arguments_rec_charact; eauto. omega. + unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. lia. Qed. Lemma loc_arguments_main: @@ -390,8 +413,9 @@ Proof. reflexivity. Qed. -(** ** Normalization of function results *) +(** ** Normalization of function results and parameters *) (** No normalization needed. *) Definition return_value_needs_normalization (t: rettype) := false. +Definition parameter_needs_normalization (t: rettype) := false. diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 8a17217a..bbcc6807 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -695,7 +695,6 @@ let expanse (sb : superblock) code pm = was_exp := false; let inst = get_some @@ PTree.get n code in (if !Clflags.option_fexpanse_rtlcond then - debug "We are checking node %d\n" (p2i n); match inst with (* Expansion of conditions - Ocmp *) | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> @@ -825,22 +824,28 @@ let expanse (sb : superblock) code pm = | _ -> ()); (if !Clflags.option_fexpanse_others && not !was_exp then match inst with - | Iop (Ofloatconst f, nil, dest, succ) -> - debug "Iop/Ofloatconst\n"; - let r = r2pi () in - let l = loadimm64 vn r (Floats.Float.to_bits f) in - let r', l' = extract_arg l in - exp := addinst vn Ofloat_of_bits [ r' ] dest :: l'; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Osingleconst f, nil, dest, succ) -> - debug "Iop/Osingleconst\n"; - let r = r2pi () in - let l = loadimm32 vn r (Floats.Float32.to_bits f) in - let r', l' = extract_arg l in - exp := addinst vn Osingle_of_bits [ r' ] dest :: l'; - exp := extract_final vn !exp dest succ; - was_exp := true + | Iop (Ofloatconst f, nil, dest, succ) -> ( + match make_immed64 (Floats.Float.to_bits f) with + | Imm64_single _ | Imm64_large _ -> () + | Imm64_pair (hi, lo) -> + debug "Iop/Ofloatconst\n"; + let r = r2pi () in + let l = load_hilo64 vn r hi lo in + let r', l' = extract_arg l in + exp := addinst vn Ofloat_of_bits [ r' ] dest :: l'; + exp := extract_final vn !exp dest succ; + was_exp := true) + | Iop (Osingleconst f, nil, dest, succ) -> ( + match make_immed32 (Floats.Float32.to_bits f) with + | Imm32_single imm -> () + | Imm32_pair (hi, lo) -> + debug "Iop/Osingleconst\n"; + let r = r2pi () in + let l = load_hilo32 vn r hi lo in + let r', l' = extract_arg l in + exp := addinst vn Osingle_of_bits [ r' ] dest :: l'; + exp := extract_final vn !exp dest succ; + was_exp := true) | Iop (Ointconst n, nil, dest, succ) -> debug "Iop/Ointconst\n"; exp := loadimm32 vn dest n; diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 7d66cbb8..6041a34d 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -224,8 +224,8 @@ Lemma operation_is_redundant_sound: vagree v arg1' nv. Proof. intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst. -- apply sign_ext_redundant_sound; auto. omega. -- apply sign_ext_redundant_sound; auto. omega. +- apply sign_ext_redundant_sound; auto. lia. +- apply sign_ext_redundant_sound; auto. lia. - apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. Qed. diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index ca049962..2739bc5d 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -639,7 +639,7 @@ Remark ltu_12_wordsize: Proof. unfold Int.iwordsize, Int.zwordsize. simpl. unfold Int.ltu. apply zlt_true. - rewrite !Int.unsigned_repr; try cbn; try omega. + rewrite !Int.unsigned_repr; try cbn; try lia. Qed. (** ** Signed longs *) @@ -690,14 +690,14 @@ Proof. intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto. unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int.add_signed. symmetry; apply Int.signed_repr. specialize (Int.eq_spec n (Int.repr Int.max_signed)). rewrite EQMAX; simpl; intros. assert (Int.signed n <> Int.max_signed). { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. + generalize (Int.signed_range n); lia. Qed. Lemma cmpl_ltle_add_one: forall v n, @@ -708,14 +708,14 @@ Proof. intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto. unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)). rewrite EQMAX; simpl; intros. assert (Int64.signed n <> Int64.max_signed). { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. + generalize (Int64.signed_range n); lia. Qed. Remark lt_maxsgn_false_int: forall i, diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index ce80fc57..f450fe6c 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -370,20 +370,20 @@ Proof. change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl. apply Val.lessdef_same. f_equal. transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)). - unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity. + unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity. apply Int.same_bits_eq; intros n N. change Int.zwordsize with 32 in *. - assert (N1: 0 <= n < 64) by omega. + assert (N1: 0 <= n < 64) by lia. rewrite Int64.bits_loword by auto. rewrite Int64.bits_shr' by auto. change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64. - rewrite zlt_true by omega. + rewrite zlt_true by lia. rewrite Int.testbit_repr by auto. - unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega). + unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia). transitivity (Z.testbit (Int.signed i * Int.signed i0) (n + 32)). - rewrite Z.shiftr_spec by omega. auto. + rewrite Z.shiftr_spec by lia. auto. apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. - change Int64.zwordsize with 64; omega. + change Int64.zwordsize with 64; lia. - TrivialExists. Qed. @@ -398,20 +398,20 @@ Proof. change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl. apply Val.lessdef_same. f_equal. transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)). - unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity. + unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity. apply Int.same_bits_eq; intros n N. change Int.zwordsize with 32 in *. - assert (N1: 0 <= n < 64) by omega. + assert (N1: 0 <= n < 64) by lia. rewrite Int64.bits_loword by auto. rewrite Int64.bits_shru' by auto. change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64. - rewrite zlt_true by omega. + rewrite zlt_true by lia. rewrite Int.testbit_repr by auto. - unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega). + unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia). transitivity (Z.testbit (Int.unsigned i * Int.unsigned i0) (n + 32)). - rewrite Z.shiftr_spec by omega. auto. + rewrite Z.shiftr_spec by lia. auto. apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. - change Int64.zwordsize with 64; omega. + change Int64.zwordsize with 64; lia. - TrivialExists. Qed. @@ -766,7 +766,7 @@ Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. omega. + rewrite Val.zero_ext_and. apply eval_andimm. lia. Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). @@ -779,7 +779,7 @@ Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). Proof. red; intros until x. unfold cast8unsigned. - rewrite Val.zero_ext_and. apply eval_andimm. omega. + rewrite Val.zero_ext_and. apply eval_andimm. lia. Qed. Theorem eval_intoffloat: diff --git a/riscV/Stacklayout.v b/riscV/Stacklayout.v index d0c6a526..25f02aab 100644 --- a/riscV/Stacklayout.v +++ b/riscV/Stacklayout.v @@ -68,15 +68,15 @@ Local Opaque Z.add Z.mul sepconj range. set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + 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 <= 4 * b.(bound_outgoing)) by omega. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + w <= oretaddr) by (unfold oretaddr; omega). - assert (oretaddr + w <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + w <= oretaddr) by (unfold oretaddr; lia). + assert (oretaddr + 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; omega). - assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). (* Reorder as: outgoing back link @@ -89,11 +89,11 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap45. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split_2. fold olink; omega. omega. - apply range_split. omega. - apply range_split. omega. - apply range_split_2. fold ol. omega. omega. - apply range_drop_right with ostkdata. omega. + apply range_split_2. fold olink; lia. lia. + apply range_split. lia. + apply range_split. lia. + apply range_split_2. fold ol. lia. lia. + apply range_drop_right with ostkdata. lia. eapply sep_drop2. eexact H. Qed. @@ -109,16 +109,16 @@ Proof. set (ocs := oretaddr + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + 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 <= 4 * b.(bound_outgoing)) by omega. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + w <= oretaddr) by (unfold oretaddr; omega). - assert (oretaddr + w <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + w <= oretaddr) by (unfold oretaddr; lia). + assert (oretaddr + 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; omega). - assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). - split. omega. apply align_le. omega. + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). + split. lia. apply align_le. lia. Qed. Lemma frame_env_aligned: @@ -137,11 +137,11 @@ Proof. set (ocs := oretaddr + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + 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. apply align_divides; omega. - split. apply align_divides; omega. - split. apply align_divides; omega. - apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl. + split. apply align_divides; lia. + split. apply align_divides; lia. + split. apply align_divides; lia. + apply Z.divide_add_r. apply align_divides; lia. apply Z.divide_refl. Qed. diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 1f00c440..aab6b9b8 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -110,9 +110,9 @@ module Target : TARGET = | Section_data(i, true) -> failwith "_Thread_local unsupported on this platform" | Section_data(i, false) | Section_small_data i -> - if i then ".data" else common_section () + variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" + variable_section ~sec:".section .rodata" i | Section_string -> ".section .rodata" | Section_literal -> ".section .rodata" | Section_jumptable -> ".section .rodata" @@ -394,10 +394,10 @@ module Target : TARGET = fprintf oc " fmv.d %a, %a\n" freg fd freg fs | Pfmvxs (rd,fs) -> fprintf oc " fmv.x.s %a, %a\n" ireg rd freg fs - | Pfmvxd (rd,fs) -> - fprintf oc " fmv.x.d %a, %a\n" ireg rd freg fs | Pfmvsx (fd,rs) -> fprintf oc " fmv.s.x %a, %a\n" freg fd ireg rs + | Pfmvxd (rd,fs) -> + fprintf oc " fmv.x.d %a, %a\n" ireg rd freg fs | Pfmvdx (fd,rs) -> fprintf oc " fmv.d.x %a, %a\n" freg fd ireg rs diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index d29180e4..e0314c6a 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -13,7 +13,7 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op RTL ValueDomain. -Require Import Zbits. +Require Import Zbits Lia. (** Value analysis for RISC V operators *) @@ -405,7 +405,7 @@ Proof. assert (DEFAULT: vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (Uns Pbot 1)). { destruct ob; simpl; auto with va. - destruct b; constructor; try omega. + destruct b; constructor; try lia. change 1 with (usize Int.one). apply is_uns_usize. red; intros. apply Int.bits_zero. } diff --git a/riscV/extractionMachdep.v b/riscV/extractionMachdep.v index c9a1040a..890735ba 100644 --- a/riscV/extractionMachdep.v +++ b/riscV/extractionMachdep.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. *) (* *) (* *********************************************************************) |