diff options
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/AsmToJSON.ml | 2 | ||||
| -rw-r--r-- | riscV/Asmexpand.ml | 8 | ||||
| -rw-r--r-- | riscV/Asmgenproof.v | 2 | ||||
| -rw-r--r-- | riscV/CBuiltins.ml | 8 | ||||
| -rw-r--r-- | riscV/Conventions1.v | 11 | ||||
| -rw-r--r-- | riscV/Machregs.v | 4 | ||||
| -rw-r--r-- | riscV/Op.v | 2 | ||||
| -rw-r--r-- | riscV/Stacklayout.v | 2 | ||||
| -rw-r--r-- | riscV/TargetPrinter.ml | 21 |
9 files changed, 35 insertions, 25 deletions
diff --git a/riscV/AsmToJSON.ml b/riscV/AsmToJSON.ml index ea22bdab..1b2f7458 100644 --- a/riscV/AsmToJSON.ml +++ b/riscV/AsmToJSON.ml @@ -16,3 +16,5 @@ let pp_program pp prog = Format.fprintf pp "null" + +let pp_mnemonics pp = () diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index d42f4d13..945974e0 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -104,8 +104,8 @@ let fixup_call sg = (* Handling of annotations *) -let expand_annot_val txt targ args res = - emit (Pbuiltin (EF_annot(txt,[targ]), args, BR_none)); +let expand_annot_val kind txt targ args res = + emit (Pbuiltin (EF_annot(kind,txt,[targ]), args, BR_none)); match args, res with | [BA(IR src)], BR(IR dst) -> if dst <> src then emit (Pmv (dst, src)) @@ -556,8 +556,8 @@ let expand_instruction instr = expand_builtin_vload chunk args res | EF_vstore chunk -> expand_builtin_vstore chunk args - | EF_annot_val (txt,targ) -> - expand_annot_val txt targ args res + | EF_annot_val (kind,txt,targ) -> + expand_annot_val kind txt targ args res | EF_memcpy(sz, al) -> expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args | EF_annot _ | EF_debug _ | EF_inline_asm _ -> diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index da444a4b..cc45a8de 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -920,7 +920,7 @@ Local Transparent destroyed_by_op. generalize EQ; intros EQ'. monadInv EQ'. destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0. unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m1' [C D]]. exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml index 385f9d13..0c981d11 100644 --- a/riscV/CBuiltins.ml +++ b/riscV/CBuiltins.ml @@ -26,14 +26,8 @@ let builtins = { "__builtin_fence", (TVoid [], [], false); (* Integer arithmetic *) - "__builtin_bswap", - (TInt(IUInt, []), [TInt(IUInt, [])], false); "__builtin_bswap64", (TInt(IULongLong, []), [TInt(IULongLong, [])], false); - "__builtin_bswap32", - (TInt(IUInt, []), [TInt(IUInt, [])], false); - "__builtin_bswap16", - (TInt(IUShort, []), [TInt(IUShort, [])], false); (* Float arithmetic *) "__builtin_fmadd", (TFloat(FDouble, []), @@ -51,8 +45,6 @@ let builtins = { (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false); - "__builtin_fsqrt", - (TFloat(FDouble, []), [TFloat(FDouble, [])], false); "__builtin_fmax", (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false); "__builtin_fmin", diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index 7ce7f7ee..df7ddfd2 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -216,7 +216,7 @@ Definition one_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ) One(R r) :: rec (rn + 1) ofs | None => let ofs := align ofs (typealign ty) in - One(S Outgoing ofs ty) :: rec rn (ofs + (if Archi.ptr64 then 2 else 1)) + One(S Outgoing ofs ty) :: rec rn (ofs + (if Archi.ptr64 then 2 else typesize ty)) end. Definition two_args (regs: list mreg) (rn: Z) (ofs: Z) @@ -310,6 +310,8 @@ Proof. omega. } assert (SK: (if Archi.ptr64 then 2 else 1) > 0). { destruct Archi.ptr64; omega. } + assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0). + { intros. destruct Archi.ptr64. omega. apply typesize_pos. } assert (A: forall regs rn ofs ty f, OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)). { intros until f; intros OR OF OO; red; unfold one_arg; intros. @@ -317,7 +319,8 @@ Proof. - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. - eapply OF; eauto. - subst p; simpl. auto using align_divides, typealign_pos. - - eapply OF; [idtac|eauto]. generalize (AL ofs ty OO); omega. + - eapply OF; [idtac|eauto]. + generalize (AL ofs ty OO) (SKK ty); omega. } assert (B: forall regs rn ofs f, OKREGS regs -> OKF f -> ofs >= 0 -> OK (two_args regs rn ofs f)). @@ -417,7 +420,7 @@ Proof. ofs + typesize ty <= max_outgoing_2 n p). { intros. destruct p; simpl in H; intuition; subst; simpl. - xomega. - - eapply Zle_trans. 2: apply A. xomega. + - eapply Z.le_trans. 2: apply A. xomega. - xomega. } assert (C: forall l n, In (S Outgoing ofs ty) (regs_of_rpairs l) -> @@ -425,7 +428,7 @@ Proof. { induction l; simpl; intros. - contradiction. - rewrite in_app_iff in H. destruct H. - + eapply Zle_trans. eapply B; eauto. apply Zge_le. apply fold_max_outgoing_above. + + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above. + apply IHl; auto. } apply C. diff --git a/riscV/Machregs.v b/riscV/Machregs.v index c7d558ed..d8bb4a4b 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -151,7 +151,7 @@ Definition register_names := ("F16", F16) :: ("F17", F17) :: ("F18", F18) :: ("F19", F19) :: ("F20", F20) :: ("F21", F21) :: ("F22", F22) :: ("F23", F23) :: ("F24", F24) :: ("F25", F25) :: ("F26", F26) :: ("F27", F27) :: - ("F27", F27) :: ("F28", F28) :: ("F29", F29) :: ("F30", F30) :: + ("F28", F28) :: ("F29", F29) :: ("F30", F30) :: ("F31", F31) :: nil. Definition register_by_name (s: string) : option mreg := @@ -247,7 +247,7 @@ Definition builtin_constraints (ef: external_function) : | EF_vload _ => OK_addressing :: nil | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil - | EF_annot txt targs => map (fun _ => OK_all) targs + | EF_annot kind txt targs => map (fun _ => OK_all) targs | EF_debug kind txt targs => map (fun _ => OK_all) targs | _ => nil end. @@ -1194,7 +1194,7 @@ Remark weak_valid_pointer_no_overflow_extends: Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. + intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: diff --git a/riscV/Stacklayout.v b/riscV/Stacklayout.v index ba116380..d0c6a526 100644 --- a/riscV/Stacklayout.v +++ b/riscV/Stacklayout.v @@ -139,7 +139,7 @@ Proof. set (ostkdata := align (ol + 4 * b.(bound_local)) 8). assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). - split. apply Zdivide_0. + split. apply Z.divide_0_r. split. apply align_divides; omega. split. apply align_divides; omega. split. apply align_divides; omega. diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 7a369832..b363b2b7 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -97,6 +97,11 @@ module Target : TARGET = | FR r -> freg oc r | _ -> assert false + let preg_annot = function + | IR r -> int_reg_name r + | FR r -> float_reg_name r + | _ -> assert false + (* Names of sections *) let name_of_section = function @@ -117,6 +122,7 @@ module Target : TARGET = | Section_user(s, wr, ex) -> sprintf ".section \"%s\",\"a%s%s\",%%progbits" s (if wr then "w" else "") (if ex then "x" else "") + | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note" let section oc sec = fprintf oc " %s\n" (name_of_section sec) @@ -584,11 +590,18 @@ module Target : TARGET = fprintf oc "%s end pseudoinstr btbl\n" comment | Pbuiltin(ef, args, res) -> begin match ef with - | EF_annot(txt, targs) -> - fprintf oc "%s annotation: " comment; - print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args + | EF_annot(kind,txt, targs) -> + let annot = + begin match (P.to_int kind) with + | 1 -> annot_text preg_annot "sp" (camlstring_of_coqstring txt) args + | 2 -> let lbl = new_label () in + fprintf oc "%a: " label lbl; + ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args + | _ -> assert false + end in + fprintf oc "%s annotation: %S\n" comment annot | EF_debug(kind, txt, targs) -> - print_debug_info comment print_file_line preg "sp" oc + print_debug_info comment print_file_line preg_annot "sp" oc (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; |