aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c')
-rw-r--r--mppa_k1c/Asmexpand.ml1
-rw-r--r--mppa_k1c/Machregs.v1
-rw-r--r--mppa_k1c/SelectOp.vp12
-rw-r--r--mppa_k1c/SelectOpproof.v18
-rw-r--r--mppa_k1c/TargetPrinter.ml108
5 files changed, 115 insertions, 25 deletions
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 8ab10bc5..e388d2aa 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -591,6 +591,7 @@ let expand_instruction instr =
| EF_external _ -> failwith "asmexpand: external"
| EF_inline_asm _ -> emit instr
| EF_runtime _ -> failwith "asmexpand: runtime"
+ | EF_profiling _ -> emit instr
end
| _ ->
emit instr
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index 8098b5d1..cff1164c 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -171,6 +171,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
if Z.leb sz 15
then R62 :: R63 :: R61 :: nil
else R62 :: R63 :: R61 :: R60 :: nil
+ | EF_profiling _ _ => R62 :: R63 ::nil
| _ => nil
end.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 0974f872..bd481cbb 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -462,18 +462,10 @@ Definition mods_base (e1: expr) (e2: expr) :=
Eexternal i32_smod sig_ii_i (e1 ::: e2 ::: Enil).
Definition divu_base (e1: expr) (e2: expr) :=
- Eop Olowlong
- ((Eexternal i64_udiv sig_ll_l
- ((Eop Ocast32unsigned (e1 ::: Enil)):::
- (Eop Ocast32unsigned (e2 ::: Enil))::: Enil))
- :::Enil).
+ Eexternal i32_udiv sig_ii_i (e1 ::: e2 ::: Enil).
Definition modu_base (e1: expr) (e2: expr) :=
- Eop Olowlong
- ((Eexternal i64_umod sig_ll_l
- ((Eop Ocast32unsigned (e1 ::: Enil)):::
- (Eop Ocast32unsigned (e2 ::: Enil))::: Enil))
- :::Enil).
+ Eexternal i32_umod sig_ii_i (e1 ::: e2 ::: Enil).
Definition shrximm (e1: expr) (n2: int) :=
if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 660cba90..28294934 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -938,6 +938,12 @@ Theorem eval_divu_base:
Val.divu x y = Some z ->
exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
Proof.
+ intros; unfold divu_base.
+ econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+(* For using 64-bit unsigned division for 32-bit
+
intros until z.
intros Hax Hby Hdiv. unfold divu_base.
pose proof (divu_is_divlu x y) as DIVU.
@@ -957,7 +963,8 @@ Proof.
}
congruence.
Qed.
-
+ *)
+
Theorem eval_modu_base:
forall le a b x y z,
eval_expr ge sp e m le a x ->
@@ -965,6 +972,12 @@ Theorem eval_modu_base:
Val.modu x y = Some z ->
exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
Proof.
+ intros; unfold modu_base.
+ econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+(* for using 64-bit unsigned modulo for 32-bit
+
intros until z.
intros Hax Hby Hmod. unfold modu_base.
pose proof (modu_is_modlu x y) as MODU.
@@ -984,7 +997,8 @@ Proof.
}
congruence.
Qed.
-
+ *)
+
Theorem eval_shrximm:
forall le a n x z,
eval_expr ge sp e m le a x ->
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 930b1c51..01751f19 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -34,11 +34,57 @@ module Target (*: TARGET*) =
let comment = "#"
+ type idiv_function_kind =
+ | Idiv_system
+ | Idiv_stsud
+ | Idiv_fp;;
+
+ let idiv_function_kind = function
+ "stsud" -> Idiv_stsud
+ | "system" -> Idiv_system
+ | "fp" -> Idiv_fp
+ | _ -> failwith "unknown integer division kind";;
+
+ let idiv_function_kind_32bit () = idiv_function_kind !Clflags.option_div_i32;;
+ let idiv_function_kind_64bit () = idiv_function_kind !Clflags.option_div_i64;;
+
let subst_symbol = function
- "__compcert_i64_udiv" -> "__udivdi3"
- | "__compcert_i64_sdiv" -> "__divdi3"
- | "__compcert_i64_umod" -> "__umoddi3"
- | "__compcert_i64_smod" -> "__moddi3"
+ "__compcert_i64_udiv" ->
+ (match idiv_function_kind_64bit () with
+ | Idiv_system | Idiv_fp -> "__udivdi3"
+ | Idiv_stsud -> "__compcert_i64_udiv_stsud")
+ | "__compcert_i64_sdiv" ->
+ (match idiv_function_kind_64bit() with
+ | Idiv_system | Idiv_fp -> "__divdi3"
+ | Idiv_stsud -> "__compcert_i64_sdiv_stsud")
+ | "__compcert_i64_umod" ->
+ (match idiv_function_kind_64bit() with
+ | Idiv_system | Idiv_fp -> "__umoddi3"
+ | Idiv_stsud -> "__compcert_i64_umod_stsud")
+ | "__compcert_i64_smod" ->
+ (match idiv_function_kind_64bit() with
+ | Idiv_system | Idiv_fp -> "__moddi3"
+ | Idiv_stsud -> "__compcert_i64_smod_stsud")
+ | "__compcert_i32_sdiv" as s ->
+ (match idiv_function_kind_32bit() with
+ | Idiv_system -> s
+ | Idiv_fp -> "__compcert_i32_sdiv_fp"
+ | Idiv_stsud -> "__compcert_i32_sdiv_stsud")
+ | "__compcert_i32_udiv" as s ->
+ (match idiv_function_kind_32bit() with
+ | Idiv_system -> s
+ | Idiv_fp -> "__compcert_i32_udiv_fp"
+ | Idiv_stsud -> "__compcert_i32_udiv_stsud")
+ | "__compcert_i32_smod" as s ->
+ (match idiv_function_kind_32bit() with
+ | Idiv_system -> s
+ | Idiv_fp -> "__compcert_i32_smod_fp"
+ | Idiv_stsud -> "__compcert_i32_smod_stsud")
+ | "__compcert_i32_umod" as s ->
+ (match idiv_function_kind_32bit() with
+ | Idiv_system -> s
+ | Idiv_fp -> "__compcert_i32_umod_fp"
+ | Idiv_stsud -> "__compcert_i32_umod_stsud")
| "__compcert_f64_div" -> "__divdf3"
| "__compcert_f32_div" -> "__divsf3"
| x -> x;;
@@ -157,8 +203,12 @@ module Target (*: TARGET*) =
let name_of_section = function
| Section_text -> ".text"
- | Section_data i | Section_small_data i ->
- if i then ".data" else "COMM"
+ | Section_data(true, true) ->
+ ".section .tdata,\"awT\",@progbits"
+ | Section_data(false, true) ->
+ ".section .tbss,\"awT\",@nobits"
+ | Section_data(i, false) | Section_small_data(i) ->
+ (if i then ".data" else "COMM")
| Section_const i | Section_small_const i ->
if i then ".section .rodata" else "COMM"
| Section_string -> ".section .rodata"
@@ -211,14 +261,20 @@ module Target (*: TARGET*) =
(* Generate code to load the address of id + ofs in register r *)
-(* FIXME DMonniaux ugly ugly hack to get at standard __thread data *)
let loadsymbol oc r id ofs =
if Archi.pic_code () then begin
assert (ofs = Integers.Ptrofs.zero);
- fprintf oc " make %a = %s\n" ireg r (extern_atom id)
- end else begin
- if (extern_atom id) = "_impure_thread_data" then begin
- fprintf oc " addd %a = $r13, @tprel(%a)\n" ireg r symbol_offset (id, ofs)
+ if C2C.atom_is_thread_local id then begin
+ (* fprintf oc " addd %a = $r13, @tprel(%s)\n" ireg r (extern_atom id) *)
+ fprintf oc " addd %a = $r13, @tlsle(%s)\n" ireg r (extern_atom id)
+ end else begin
+ fprintf oc " make %a = %s\n" ireg r (extern_atom id)
+ end
+ end else
+ begin
+ if C2C.atom_is_thread_local id then begin
+ (* fprintf oc " addd %a = $r13, @tprel(%a)\n" ireg r symbol_offset (id, ofs) *)
+ fprintf oc " addd %a = $r13, @tlsle(%a)\n" ireg r symbol_offset (id, ofs)
end else begin
fprintf oc " make %a = %a\n" ireg r symbol_offset (id, ofs)
end
@@ -239,7 +295,20 @@ module Target (*: TARGET*) =
(*let w oc =
if Archi.ptr64 then output_string oc "w"
*)
-(* Offset part of a load or store *)
+
+ (* Profiling *)
+
+
+ let k1c_profiling_stub oc nr_items
+ profiling_id_table_name
+ profiling_counter_table_name =
+ fprintf oc " make $r0 = %d\n" nr_items;
+ fprintf oc " make $r1 = %s\n" profiling_id_table_name;
+ fprintf oc " make $r2 = %s\n" profiling_counter_table_name;
+ fprintf oc " goto %s\n" profiling_write_table_helper;
+ fprintf oc " ;;\n";;
+
+ (* Offset part of a load or store *)
let offset oc n = ptrofs oc n
@@ -328,6 +397,18 @@ module Target (*: 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) ->
+ let kind = Z.to_int coq_kind in
+ assert (kind >= 0);
+ assert (kind <= 1);
+ fprintf oc "%s profiling %a %d\n" comment
+ Profilingaux.pp_id id kind;
+ fprintf oc " make $r63 = %s\n" profiling_counter_table_name;
+ fprintf oc " make $r62 = 1\n";
+ fprintf oc " ;;\n";
+ fprintf oc " afaddd %d[$r63] = $r62\n"
+ (profiling_offset id kind);
+ fprintf oc " ;;\n"
| _ ->
assert false
end
@@ -789,8 +870,9 @@ module Target (*: TARGET*) =
if !Clflags.option_g then begin
section oc Section_text;
end
-
+
let print_epilogue oc =
+ print_profiling_epilogue elf_text_print_fun_info Dtors k1c_profiling_stub oc;
if !Clflags.option_g then begin
Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
section oc Section_text;
generated by cgit (git 2.34.1) at 2024-07-14 02:31:19 +0000