aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/AsmToJSON.ml74
-rw-r--r--powerpc/AsmToJSON.mli2
-rw-r--r--powerpc/Asmexpand.ml8
-rw-r--r--powerpc/Asmgenproof.v2
-rw-r--r--powerpc/Asmgenproof1.v12
-rw-r--r--powerpc/CBuiltins.ml8
-rw-r--r--powerpc/Conventions1.v26
-rw-r--r--powerpc/Machregs.v2
-rw-r--r--powerpc/Op.v2
-rw-r--r--powerpc/Stacklayout.v4
-rw-r--r--powerpc/TargetPrinter.ml27
11 files changed, 116 insertions, 51 deletions
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 6a235742..a3e57e51 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -28,10 +28,14 @@ let pp_reg pp t n =
let pp_ireg pp reg =
pp_reg pp "r" (TargetPrinter.int_reg_name reg)
-
let pp_freg pp reg =
pp_reg pp "f" (TargetPrinter.float_reg_name reg)
+let preg_annot = function
+ | IR r -> sprintf "r%s" (TargetPrinter.int_reg_name r)
+ | FR r -> sprintf "f%s" (TargetPrinter.float_reg_name r)
+ | _ -> assert false
+
let pp_atom pp a = pp_jstring pp (extern_atom a)
let pp_atom_constant pp a = pp_jsingle_object pp "Atom" pp_atom a
@@ -82,6 +86,7 @@ type instruction_arg =
| Float32 of Floats.float32
| Float64 of Floats.float
| Atom of positive
+ | String of string
let id = ref 0
@@ -105,23 +110,49 @@ let pp_arg pp = function
| Float32 f -> pp_float32_constant pp f
| Float64 f -> pp_float64_constant pp f
| Atom a -> pp_atom_constant pp a
+ | String s -> pp_jsingle_object pp "String" pp_jstring s
+
+let mnemonic_names =["Padd"; "Paddc"; "Padde"; "Paddi"; "Paddic"; "Paddis"; "Paddze"; "Pand_";
+ "Pandc"; "Pandi_"; "Pandis_"; "Pannot"; "Pb"; "Pbctr"; "Pbctrl"; "Pbdnz";
+ "Pbf"; "Pbl"; "Pblr"; "Pbs"; "Pbt"; "Pbtbl"; "Pcmpb"; "Pcmpd"; "Pcmpdi";
+ "Pcmpld"; "Pcmpldi"; "Pcmplw"; "Pcmplwi"; "Pcmpw"; "Pcmpwi"; "Pcntlzd";
+ "Pcntlzw"; "Pcreqv"; "Pcror"; "Pcrxor"; "Pdcbf"; "Pdcbi"; "Pdcbt";
+ "Pdcbtls"; "Pdcbtst"; "Pdcbz"; "Pdivd"; "Pdivdu"; "Pdivw"; "Pdivwu";
+ "Peieio"; "Peqv"; "Pextsb"; "Pextsh"; "Pextsw"; "Pfabs"; "Pfadd"; "Pfadds";
+ "Pfcfid"; "Pfcmpu"; "Pfctidz"; "Pfctiw"; "Pfctiwz"; "Pfdiv"; "Pfdivs";
+ "Pfmadd"; "Pfmr"; "Pfmsub"; "Pfmul"; "Pfmuls"; "Pfneg"; "Pfnmadd";
+ "Pfnmsub"; "Pfres"; "Pfrsp"; "Pfrsqrte"; "Pfsel"; "Pfsqrt"; "Pfsub";
+ "Pfsubs"; "Picbi"; "Picbtls"; "Pinlineasm"; "Pisel"; "Pisync"; "Plabel";
+ "Plbz"; "Plbzx"; "Pld"; "Pldi"; "Pldx"; "Plfd"; "Plfdx"; "Plfi"; "Plfis";
+ "Plfs"; "Plfsx"; "Plha"; "Plhax"; "Plhbrx"; "Plhz"; "Plhzx"; "Plwarx";
+ "Plwbrx"; "Plwsync"; "Plwz"; "Plwzu"; "Plwzx"; "Pmbar"; "Pmfcr"; "Pmflr";
+ "Pmfspr"; "Pmr"; "Pmtctr"; "Pmtlr"; "Pmtspr"; "Pmulhd"; "Pmulhdu"; "Pmulhw";
+ "Pmulhwu"; "Pmulld"; "Pmulli"; "Pmullw"; "Pnand"; "Pnor"; "Por"; "Porc";
+ "Pori"; "Poris"; "Prldicl"; "Prldimi"; "Prldinm"; "Prlwimi"; "Prlwinm";
+ "Psld"; "Pslw"; "Psrad"; "Psradi"; "Psraw"; "Psrawi"; "Psrd"; "Psrw";
+ "Pstb"; "Pstbx"; "Pstd"; "Pstdu"; "Pstdx"; "Pstfd"; "Pstfdu"; "Pstfdx";
+ "Pstfs"; "Pstfsx"; "Psth"; "Psthbrx"; "Psthx"; "Pstw"; "Pstwbrx"; "Pstwcx_";
+ "Pstwu"; "Pstwux"; "Pstwx"; "Psubfc"; "Psubfe"; "Psubfic"; "Psubfze";
+ "Psync"; "Ptrap"; "Pxor"; "Pxori"; "Pxoris"]
let pp_instructions pp ic =
let ic = List.filter (fun s -> match s with
| Pbuiltin (ef,_,_) ->
begin match ef with
- | EF_inline_asm _ -> true
+ | EF_inline_asm _
+ | EF_annot _ -> true
| _ -> false
end
| Pcfi_adjust _ (* Only debug relevant *)
| Pcfi_rel_offset _ -> false
| _ -> true) ic in
let instruction pp n args =
+ assert (List.mem n mnemonic_names);
pp_jobject_start pp;
pp_jmember ~first:true pp "Instruction Name" pp_jstring n;
pp_jmember pp "Args" (pp_jarray pp_arg) args;
pp_jobject_end pp in
- let instruction pp = function
+ let [@ocaml.warning "+4"] instruction pp = function
| Padd (ir1,ir2,ir3)
| Padd64 (ir1,ir2,ir3) -> instruction pp "Padd" [Ireg ir1; Ireg ir2; Ireg ir3]
| Paddc (ir1,ir2,ir3) -> instruction pp "Paddc" [Ireg ir1; Ireg ir2; Ireg ir3]
@@ -331,12 +362,35 @@ let pp_instructions pp ic =
| Pxoris (ir1,ir2,c) -> instruction pp "Pxoris" [Ireg ir1; Ireg ir2; Constant c]
| Pxoris64 (ir1,ir2,n) -> instruction pp "Pxoris" [Ireg ir1; Ireg ir2; Constant (Cint n)]
| Plabel l -> instruction pp "Plabel" [ALabel l]
- | Pbuiltin (ef,_,_) ->
+ | Pbuiltin (ef,args,_) ->
begin match ef with
| EF_inline_asm _ ->
instruction pp "Pinlineasm" [Id];
Cerrors.warning ("",-10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump"
- | _ -> assert false
+ | EF_annot (kind,txt,targs) ->
+ let annot_string = PrintAsmaux.annot_text preg_annot "r1" (camlstring_of_coqstring txt) args in
+ let len = String.length annot_string in
+ let buf = Buffer.create len in
+ String.iter (fun c -> begin match c with
+ | '\\' | '"' -> Buffer.add_char buf '\\'
+ | _ -> () end;
+ Buffer.add_char buf c) annot_string;
+ let annot_string = Buffer.contents buf in
+ let kind = match P.to_int kind with
+ | 1 -> "normal"
+ | 2 -> "ais"
+ | _ -> assert false in
+ instruction pp "Pannot" [String kind;String annot_string]
+ | EF_annot_val _
+ | EF_builtin _
+ | EF_debug _
+ | EF_external _
+ | EF_free
+ | EF_malloc
+ | EF_memcpy _
+ | EF_runtime _
+ | EF_vload _
+ | EF_vstore _ -> assert false
end
| Pcfi_adjust _ (* Only debug relevant *)
| Pcfi_rel_offset _ -> assert false in (* Only debug relevant *)
@@ -366,14 +420,15 @@ let pp_section pp sec =
pp_jobject_start pp;
pp_jmember ~first:true pp "Section Name" pp_jstring s;
pp_jmember pp "Writable" pp_jbool w;
- pp_jmember pp "Writable" pp_jbool e;
+ pp_jmember pp "Executable" pp_jbool e;
pp_jobject_end pp
| Section_debug_info _
| Section_debug_abbrev
| Section_debug_line _
| Section_debug_loc
| Section_debug_ranges
- | Section_debug_str -> () (* There should be no info in the debug sections *)
+ | Section_debug_str
+ | Section_ais_annotation -> () (* There should be no info in the debug sections *)
let pp_int_opt pp = function
| None -> fprintf pp "0"
@@ -441,3 +496,8 @@ let pp_program pp prog =
pp_jmember ~first:true pp "Global Variables" (pp_jarray pp_vardef) prog_vars;
pp_jmember pp "Functions" (pp_jarray pp_fundef) prog_funs;
pp_jobject_end pp
+
+let pp_mnemonics pp =
+ let mnemonic_names = List.sort (String.compare) mnemonic_names in
+ let new_line pp () = pp_print_string pp "\n" in
+ pp_print_list ~pp_sep:new_line pp_print_string pp mnemonic_names
diff --git a/powerpc/AsmToJSON.mli b/powerpc/AsmToJSON.mli
index e4d9c39a..058a4e83 100644
--- a/powerpc/AsmToJSON.mli
+++ b/powerpc/AsmToJSON.mli
@@ -11,3 +11,5 @@
(* *********************************************************************)
val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit
+
+val pp_mnemonics: Format.formatter -> unit
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index deab7703..96b11056 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -58,8 +58,8 @@ let emit_addimm rd rs n =
(* 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));
begin match args, res with
| [BA(IR src)], BR(IR dst) ->
if dst <> src then emit (Pmr(dst, src))
@@ -869,8 +869,8 @@ let expand_instruction instr =
expand_builtin_vstore chunk args
| EF_memcpy(sz, al) ->
expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) 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_annot _ | EF_debug _ | EF_inline_asm _ ->
emit instr
| _ ->
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index bf75d2e0..9f258e3d 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -854,7 +854,7 @@ Local Transparent destroyed_by_jumptable.
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/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index e5736277..460fa670 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -39,9 +39,9 @@ Proof.
intros. unfold high_u, low_u.
rewrite Int.shl_rolm. rewrite Int.shru_rolm.
rewrite Int.rolm_rolm.
- change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16))
+ change (Int.modu (Int.add (Int.sub (Int.repr (Z.of_nat Int.wordsize)) (Int.repr 16))
(Int.repr 16))
- (Int.repr (Z_of_nat Int.wordsize)))
+ (Int.repr (Z.of_nat Int.wordsize)))
with (Int.zero).
rewrite Int.rolm_zero. rewrite <- Int.and_or_distrib.
exact (Int.and_mone n).
@@ -54,9 +54,9 @@ Proof.
intros. unfold high_u, low_u.
rewrite Int.shl_rolm. rewrite Int.shru_rolm.
rewrite Int.rolm_rolm.
- change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16))
+ change (Int.modu (Int.add (Int.sub (Int.repr (Z.of_nat Int.wordsize)) (Int.repr 16))
(Int.repr 16))
- (Int.repr (Z_of_nat Int.wordsize)))
+ (Int.repr (Z.of_nat Int.wordsize)))
with (Int.zero).
rewrite Int.rolm_zero. rewrite <- Int.and_xor_distrib.
exact (Int.and_mone n).
@@ -198,7 +198,7 @@ Hint Resolve ireg_of_not_GPR0': asmgen.
Lemma preg_of_not_LR:
forall r, LR <> preg_of r.
Proof.
- intros. auto using sym_not_equal with asmgen.
+ intros. auto using not_eq_sym with asmgen.
Qed.
Lemma preg_notin_LR:
@@ -1243,7 +1243,7 @@ Opaque Val.add.
econstructor; split. eapply exec_straight_trans.
eapply exec_straight_two; simpl; reflexivity.
eapply exec_straight_two; simpl; reflexivity.
- split. assert (GPR0 <> x0) by (apply sym_not_equal; eauto with asmgen).
+ split. assert (GPR0 <> x0) by (apply not_eq_sym; eauto with asmgen).
Simpl. rewrite ! gpr_or_zero_zero. rewrite ! gpr_or_zero_not_zero by eauto with asmgen. Simpl.
rewrite low_high_half_zero. auto.
intros; Simpl.
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index d33d6252..35d6b89f 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -40,12 +40,6 @@ let builtins = {
(TInt(IInt, []), [TInt(IULong, [])], false);
"__builtin_ctzll",
(TInt(IInt, []), [TInt(IULongLong, [])], false);
- "__builtin_bswap",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
- "__builtin_bswap32",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
- "__builtin_bswap16",
- (TInt(IUShort, []), [TInt(IUShort, [])], false);
"__builtin_cmpb",
(TInt (IUInt, []), [TInt(IUInt, []);TInt(IUInt, [])], false);
(* Float arithmetic *)
@@ -65,8 +59,6 @@ let builtins = {
(TFloat(FDouble, []),
[TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
false);
- "__builtin_fsqrt",
- (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
"__builtin_frsqrte",
(TFloat(FDouble, []), [TFloat(FDouble, [])], false);
"__builtin_fres",
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 2793fbfb..1de55c1a 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -370,30 +370,30 @@ Proof.
induction tyl; simpl; intros.
omega.
destruct a.
- destruct (list_nth_z int_param_regs ir); eauto. apply Zle_trans with (ofs0 + 1); auto; omega.
+ destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
destruct (list_nth_z float_param_regs fr); eauto.
- apply Zle_trans with (align ofs0 2). apply align_le; omega.
- apply Zle_trans with (align ofs0 2 + 2); auto; omega.
+ apply Z.le_trans with (align ofs0 2). apply align_le; omega.
+ apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
set (ir' := align ir 2).
destruct (list_nth_z int_param_regs ir'); eauto.
destruct (list_nth_z int_param_regs (ir' + 1)); eauto.
- apply Zle_trans with (align ofs0 2). apply align_le; omega.
- apply Zle_trans with (align ofs0 2 + 2); auto; omega.
- apply Zle_trans with (align ofs0 2). apply align_le; omega.
- apply Zle_trans with (align ofs0 2 + 2); auto; omega.
+ apply Z.le_trans with (align ofs0 2). apply align_le; omega.
+ apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
+ apply Z.le_trans with (align ofs0 2). apply align_le; omega.
+ apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
destruct (list_nth_z float_param_regs fr); eauto.
- apply Zle_trans with (align ofs0 2). apply align_le; omega.
- apply Zle_trans with (align ofs0 2 + 2); auto; omega.
- destruct (list_nth_z int_param_regs ir); eauto. apply Zle_trans with (ofs0 + 1); auto; omega.
+ apply Z.le_trans with (align ofs0 2). apply align_le; omega.
+ apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
+ destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
destruct (list_nth_z float_param_regs fr); eauto.
- apply Zle_trans with (align ofs0 2). apply align_le; omega.
- apply Zle_trans with (align ofs0 2 + 2); auto; omega.
+ apply Z.le_trans with (align ofs0 2). apply align_le; omega.
+ apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
Qed.
Lemma size_arguments_above:
forall s, size_arguments s >= 0.
Proof.
- intros; unfold size_arguments. apply Zle_ge.
+ intros; unfold size_arguments. apply Z.le_ge.
apply size_arguments_rec_above.
Qed.
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 8442bb52..53d99e2f 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -279,7 +279,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.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 263c1bd8..e6f942c1 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -1042,7 +1042,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/powerpc/Stacklayout.v b/powerpc/Stacklayout.v
index 17104b33..cb3806bd 100644
--- a/powerpc/Stacklayout.v
+++ b/powerpc/Stacklayout.v
@@ -138,8 +138,8 @@ Proof.
split. exists (fe_ofs_arg / 8); reflexivity.
split. apply align_divides; omega.
split. apply align_divides; omega.
- split. apply Zdivide_0.
+ split. apply Z.divide_0_r.
apply Z.divide_add_r.
- apply Zdivide_trans with 8. exists 2; auto. apply align_divides; omega.
+ apply Z.divide_trans with 8. exists 2; auto. apply align_divides; omega.
apply Z.divide_factor_l.
Qed.
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index cb5f2304..9c07b086 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -136,6 +136,7 @@ module Linux_System : SYSTEM =
| Section_debug_line _ -> ".section .debug_line,\"\",@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 section oc sec =
@@ -234,6 +235,7 @@ module Diab_System : SYSTEM =
sprintf ".section .debug_line,,n\n"
| Section_debug_ranges
| Section_debug_str -> assert false (* Should not be used *)
+ | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",,n"
let section oc sec =
let name = name_of_section sec in
@@ -335,9 +337,9 @@ module Target (System : SYSTEM):TARGET =
(* For printing annotations, use the full register names [rN] and [fN]
to avoid ambiguity with constants. *)
- let preg_annot oc = function
- | IR r -> fprintf oc "r%s" (int_reg_name r)
- | FR r -> fprintf oc "f%s" (float_reg_name r)
+ let preg_annot = function
+ | IR r -> sprintf "r%s" (int_reg_name r)
+ | FR r -> sprintf "f%s" (float_reg_name r)
| _ -> assert false
(* Encoding masks for rlwinm instructions *)
@@ -832,10 +834,17 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " .balign %d\n" !Clflags.option_falignbranchtargets;
fprintf oc "%a:\n" label (transl_label lbl)
| Pbuiltin(ef, args, res) ->
- begin match ef with
- | EF_annot(txt, targs) ->
- fprintf oc "%s annotation: " comment;
- print_annot_text preg_annot "r1" oc (camlstring_of_coqstring txt) args
+ begin match ef with
+ | 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_annot "r1" oc
(P.to_int kind) (extern_atom txt) args
@@ -990,7 +999,9 @@ module Target (System : SYSTEM):TARGET =
let section oc sec =
section oc sec;
- debug_section oc sec
+ match sec with
+ | Section_ais_annotation -> ()
+ | _ -> debug_section oc sec
end
let sel_target () =
generated by cgit (git 2.34.1) at 2024-06-29 12:24:48 +0000