aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c')
-rw-r--r--mppa_k1c/Archi.v6
-rw-r--r--mppa_k1c/Asmexpand.ml1
-rw-r--r--mppa_k1c/Machregs.v1
-rw-r--r--mppa_k1c/Op.v11
-rw-r--r--mppa_k1c/SelectOp.vp22
-rw-r--r--mppa_k1c/SelectOpproof.v27
-rw-r--r--mppa_k1c/TargetPrinter.ml54
7 files changed, 93 insertions, 29 deletions
diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index 69b32c7c..587f768e 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/Archi.v
@@ -26,11 +26,11 @@ Definition big_endian := false.
Definition align_int64 := 8%Z.
Definition align_float64 := 8%Z.
-Definition splitlong := negb ptr64.
+Definition splitlong := false.
Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
Proof.
- unfold splitlong. destruct ptr64; simpl; congruence.
+ unfold splitlong. congruence.
Qed.
(** THIS IS NOT CHECKED ! NONE OF THIS ! *)
@@ -77,3 +77,5 @@ Global Opaque ptr64 big_endian splitlong
(** Whether to generate position-independent code or not *)
Parameter pic_code: unit -> bool.
+
+Definition has_notrap_loads := true.
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/Op.v b/mppa_k1c/Op.v
index 92061d04..4caac9e1 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -1045,14 +1045,19 @@ Definition is_trapping_op (op : operation) :=
| _ => 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,
- op <> Omove ->
is_trapping_op op = false ->
- (List.length vl) = (List.length (fst (type_of_operation op))) ->
+ (List.length vl) = args_of_operation op ->
eval_operation genv sp op vl m <> None.
Proof.
- destruct op; intros; simpl in *; try congruence.
+ 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).
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 1cac2257..bd481cbb 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -168,13 +168,21 @@ Nondetfunction add (e1: expr) (e2: expr) :=
| t1, Eop (Oaddimm n2) (t2:::Enil) =>
addimm n2 (Eop Oadd (t1:::t2:::Enil))
| t1, (Eop Omul (t2:::t3:::Enil)) =>
- Eop Omadd (t1:::t2:::t3:::Enil)
+ if Compopts.optim_madd tt
+ then Eop Omadd (t1:::t2:::t3:::Enil)
+ else Eop Oadd (e1:::e2:::Enil)
| (Eop Omul (t2:::t3:::Enil)), t1 =>
- Eop Omadd (t1:::t2:::t3:::Enil)
+ if Compopts.optim_madd tt
+ then Eop Omadd (t1:::t2:::t3:::Enil)
+ else Eop Oadd (e1:::e2:::Enil)
| t1, (Eop (Omulimm n) (t2:::Enil)) =>
- Eop (Omaddimm n) (t1:::t2:::Enil)
+ if Compopts.optim_madd tt
+ then Eop (Omaddimm n) (t1:::t2:::Enil)
+ else Eop Oadd (e1:::e2:::Enil)
| (Eop (Omulimm n) (t2:::Enil)), t1 =>
- Eop (Omaddimm n) (t1:::t2:::Enil)
+ if Compopts.optim_madd tt
+ then Eop (Omaddimm n) (t1:::t2:::Enil)
+ else Eop Oadd (e1:::e2:::Enil)
| (Eop (Oshlimm n) (t1:::Enil)), t2 =>
add_shlimm n t1 t2
| t2, (Eop (Oshlimm n) (t1:::Enil)) =>
@@ -197,7 +205,9 @@ Nondetfunction sub (e1: expr) (e2: expr) :=
| t1, (Eop Omul (t2:::t3:::Enil)) =>
Eop Omsub (t1:::t2:::t3:::Enil)
| t1, (Eop (Omulimm n) (t2:::Enil)) =>
- Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil)
+ if Compopts.optim_madd tt
+ then Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil)
+ else Eop Osub (e1:::e2:::Enil)
| _, _ => Eop Osub (e1:::e2:::Enil)
end.
@@ -704,4 +714,4 @@ End SELECT.
(* Local Variables: *)
(* mode: coq *)
-(* End: *) \ No newline at end of file
+(* End: *)
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 6dd00ad5..cbe7a814 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -350,13 +350,19 @@ Proof.
apply eval_addimm. EvalOp.
repeat rewrite Val.add_assoc. reflexivity.
- (* Omadd *)
- subst. TrivialExists.
+ subst. destruct (Compopts.optim_madd tt); TrivialExists;
+ repeat (eauto; econstructor; simpl).
- (* Omadd rev *)
- subst. rewrite Val.add_commut. TrivialExists.
+ subst. destruct (Compopts.optim_madd tt); TrivialExists;
+ repeat (eauto; econstructor; simpl).
+ simpl. rewrite Val.add_commut. reflexivity.
- (* Omaddimm *)
- subst. TrivialExists.
+ subst. destruct (Compopts.optim_madd tt); TrivialExists;
+ repeat (eauto; econstructor; simpl).
- (* Omaddimm rev *)
- subst. rewrite Val.add_commut. TrivialExists.
+ subst. destruct (Compopts.optim_madd tt); TrivialExists;
+ repeat (eauto; econstructor; simpl).
+ simpl. rewrite Val.add_commut. reflexivity.
(* Oaddx *)
- subst. pose proof eval_addx as ADDX.
unfold binary_constructor_sound in ADDX.
@@ -380,11 +386,14 @@ Proof.
- subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp.
- subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp.
- TrivialExists. simpl. subst. reflexivity.
- - TrivialExists. simpl. subst.
- rewrite sub_add_neg.
- rewrite neg_mul_distr_r.
- unfold Val.neg.
- reflexivity.
+ - destruct (Compopts.optim_madd tt).
+ + TrivialExists. simpl. subst.
+ rewrite sub_add_neg.
+ rewrite neg_mul_distr_r.
+ unfold Val.neg.
+ reflexivity.
+ + TrivialExists. repeat (eauto; econstructor).
+ simpl. subst. reflexivity.
- TrivialExists.
Qed.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 63a0bd24..01751f19 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -203,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"
@@ -257,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
@@ -285,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
@@ -374,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
@@ -835,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 04:49:50 +0000