Commit 7998ccfd authored by xleroy's avatar xleroy
Browse files

- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.

- Revised printing of intermediate RTL code.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 362f2f36
......@@ -16,7 +16,9 @@
- Simpler and more robust handling of calls to variadic functions.
- More tolerance for functions declared without a prototype
(option -funprototyped, on by default).
- Option -drtl.
Release 2.1, 2013-10-28
=======================
......
......@@ -615,11 +615,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pfcvtsd r1 r2 =>
Next (nextinstr (rs#r1 <- (Val.singleoffloat rs#r2))) m
| Pfldd r1 r2 n =>
exec_load Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m
exec_load Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m
| Pflds r1 r2 n =>
exec_load Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m
| Pfstd r1 r2 n =>
exec_store Mfloat64al32 (Val.add rs#r2 (Vint n)) r1 rs m
exec_store Mfloat64 (Val.add rs#r2 (Vint n)) r1 rs m
| Pfsts r1 r2 n =>
match exec_store Mfloat32 (Val.add rs#r2 (Vint n)) r1 rs m with
| Next rs' m' => Next (rs'#FR6 <- Vundef) m'
......
......@@ -542,7 +542,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
transl_memory_access_int Pldr mk_immed_mem_word dst addr args k
| Mfloat32 =>
transl_memory_access_float Pflds mk_immed_mem_float dst addr args k
| Mfloat64 | Mfloat64al32 =>
| Mfloat64 =>
transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k
| Mint64 =>
Error (msg "Asmgen.transl_load")
......@@ -563,7 +563,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
transl_memory_access_int Pstr mk_immed_mem_word src addr args k
| Mfloat32 =>
transl_memory_access_float Pfsts mk_immed_mem_float src addr args k
| Mfloat64 | Mfloat64al32 =>
| Mfloat64 =>
transl_memory_access_float Pfstd mk_immed_mem_float src addr args k
| Mint64 =>
Error (msg "Asmgen.transl_store")
......
......@@ -350,7 +350,7 @@ let print_builtin_vload_common oc chunk args res =
| Mfloat32, [IR addr], [FR res] ->
fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr;
fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2
| (Mfloat64 | Mfloat64al32), [IR addr], [FR res] ->
| Mfloat64, [IR addr], [FR res] ->
fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1
| _ ->
assert false
......@@ -381,7 +381,7 @@ let print_builtin_vstore_common oc chunk args =
| Mfloat32, [IR addr; FR src] ->
fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src;
fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2
| (Mfloat64 | Mfloat64al32), [IR addr; FR src] ->
| Mfloat64, [IR addr; FR src] ->
fprintf oc " fstd %a, [%a, #0]\n" freg src ireg addr; 1
| _ ->
assert false
......
......@@ -65,7 +65,6 @@ rule token = parse
| "float" { FLOAT }
| "float32" { FLOAT32 }
| "float64" { FLOAT64 }
| "float64al32" { FLOAT64AL32 }
| "floatofint" { FLOATOFINT }
| "floatofintu" { FLOATOFINTU }
| "floatoflong" { FLOATOFLONG }
......
......@@ -277,7 +277,6 @@ let mkmatch expr cases =
%token FLOAT
%token FLOAT32
%token FLOAT64
%token FLOAT64AL32
%token <float> FLOATLIT
%token FLOATOFINT
%token FLOATOFINTU
......@@ -687,7 +686,6 @@ memory_chunk:
| INT { Mint32 }
| FLOAT32 { Mfloat32 }
| FLOAT64 { Mfloat64 }
| FLOAT64AL32 { Mfloat64al32 }
| FLOAT { Mfloat64 }
;
......
......@@ -168,7 +168,6 @@ let type_chunk = function
| Mint64 -> tlong
| Mfloat32 -> tfloat
| Mfloat64 -> tfloat
| Mfloat64al32 -> tfloat
let name_of_chunk = PrintAST.name_of_chunk
......
......@@ -103,9 +103,8 @@ Inductive binary_operation : Type :=
| Ocmpl: comparison -> binary_operation (**r long signed comparison *)
| Ocmplu: comparison -> binary_operation. (**r long unsigned comparison *)
(** Expressions include reading local variables, constants and
arithmetic operations, reading store locations, and conditional
expressions (similar to [e1 ? e2 : e3] in C). *)
(** Expressions include reading local variables, constants,
arithmetic operations, and memory loads. *)
Inductive expr : Type :=
| Evar : ident -> expr
......
......@@ -786,7 +786,6 @@ Proof.
rewrite <- (Float.bits_of_singleoffloat f0).
congruence.
- apply encode_val_inject. rewrite val_inject_id; auto.
- apply encode_val_inject. rewrite val_inject_id; auto.
Qed.
Lemma store_argument_load_result:
......
......@@ -110,29 +110,13 @@ let print_globdef pp (id, gd) =
let print_program pp (prog: RTL.program) =
List.iter (print_globdef pp) prog.prog_defs
let print_if optdest prog =
match !optdest with
let destination : string option ref = ref None
let print_if passno prog =
match !destination with
| None -> ()
| Some f ->
let oc = open_out f in
let oc = open_out (f ^ "." ^ Z.to_string passno) in
print_program oc prog;
close_out oc
let destination_rtl : string option ref = ref None
let print_rtl = print_if destination_rtl
let destination_tailcall : string option ref = ref None
let print_tailcall = print_if destination_tailcall
let destination_inlining : string option ref = ref None
let print_inlining = print_if destination_inlining
let destination_constprop : string option ref = ref None
let print_constprop = print_if destination_constprop
let destination_cse : string option ref = ref None
let print_cse = print_if destination_cse
let destination_deadcode : string option ref = ref None
let print_deadcode = print_if destination_deadcode
......@@ -1933,7 +1933,7 @@ Definition vnormalize (chunk: memory_chunk) (v: aval) :=
| Mint64, L _ => v
| Mfloat32, F f => F (Float.singleoffloat f)
| Mfloat32, _ => Fsingle
| (Mfloat64 | Mfloat64al32), F f => v
| Mfloat64, F f => v
| _, _ => Ifptr Pbot
end.
......@@ -1987,8 +1987,6 @@ Proof.
rewrite H2. destruct v; simpl; constructor. apply Float.singleoffloat_is_single.
- (* float64 *)
destruct v; try contradiction; constructor.
- (* float64 *)
destruct v; try contradiction; constructor.
Qed.
Lemma vnormalize_monotone:
......@@ -2057,8 +2055,7 @@ Definition chunk_compat (chunk chunk': memory_chunk) : bool :=
| Mint32, Mint32 => true
| Mfloat32, Mfloat32 => true
| Mint64, Mint64 => true
| (Mfloat64 | Mfloat64al32), Mfloat64 => true
| Mfloat64al32, Mfloat64al32 => true
| Mfloat64, Mfloat64 => true
| _, _ => false
end.
......
......@@ -2493,7 +2493,7 @@ and check_builtin_vload_common ccode ecode pc chunk addr offset res fw =
>>= recur_simpl
| _ -> error
end
| (Mfloat64 | Mfloat64al32), [FR res] ->
| Mfloat64, [FR res] ->
begin match ecode with
| LFD(frD, rA, d) :: es ->
OK(fw)
......@@ -2553,7 +2553,7 @@ and check_builtin_vstore_common ccode ecode pc chunk addr offset src fw =
>>= compare_code ccode es (Int32.add pc 8l)
| _ -> error
end
| (Mfloat64 | Mfloat64al32), FR src ->
| Mfloat64, FR src ->
begin match ecode with
| STFD(frS, rA, d) :: es ->
OK(fw)
......
......@@ -133,8 +133,7 @@ Inductive memory_chunk : Type :=
| Mint32 (**r 32-bit integer, or pointer *)
| Mint64 (**r 64-bit integer *)
| Mfloat32 (**r 32-bit single-precision float *)
| Mfloat64 (**r 64-bit double-precision float *)
| Mfloat64al32. (**r 64-bit double-precision float, 4-aligned *)
| Mfloat64. (**r 64-bit double-precision float *)
Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}.
Proof. decide equality. Defined.
......@@ -152,7 +151,6 @@ Definition type_of_chunk (c: memory_chunk) : typ :=
| Mint64 => Tlong
| Mfloat32 => Tsingle
| Mfloat64 => Tfloat
| Mfloat64al32 => Tfloat
end.
Definition type_of_chunk_use (c: memory_chunk) : typ :=
......@@ -165,7 +163,6 @@ Definition type_of_chunk_use (c: memory_chunk) : typ :=
| Mint64 => Tlong
| Mfloat32 => Tfloat
| Mfloat64 => Tfloat
| Mfloat64al32 => Tfloat
end.
(** The chunk that is appropriate to store and reload a value of
......@@ -174,7 +171,7 @@ Definition type_of_chunk_use (c: memory_chunk) : typ :=
Definition chunk_of_type (ty: typ) :=
match ty with
| Tint => Mint32
| Tfloat => Mfloat64al32
| Tfloat => Mfloat64
| Tlong => Mint64
| Tsingle => Mfloat32
end.
......
......@@ -39,7 +39,6 @@ Definition size_chunk (chunk: memory_chunk) : Z :=
| Mint64 => 8
| Mfloat32 => 4
| Mfloat64 => 8
| Mfloat64al32 => 8
end.
Lemma size_chunk_pos:
......@@ -86,8 +85,7 @@ Definition align_chunk (chunk: memory_chunk) : Z :=
| Mint32 => 4
| Mint64 => 8
| Mfloat32 => 4
| Mfloat64 => 8
| Mfloat64al32 => 4
| Mfloat64 => 4
end.
Lemma align_chunk_pos:
......@@ -343,7 +341,7 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval :=
| Vptr b ofs, Mint32 => inj_pointer 4%nat b ofs
| Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n))
| Vfloat n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float.bits_of_single n)))
| Vfloat n, (Mfloat64 | Mfloat64al32) => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.bits_of_double n)))
| Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.bits_of_double n)))
| _, _ => list_repeat (size_chunk_nat chunk) Undef
end.
......@@ -358,7 +356,7 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
| Mint32 => Vint(Int.repr(decode_int bl))
| Mint64 => Vlong(Int64.repr(decode_int bl))
| Mfloat32 => Vfloat(Float.single_of_bits (Int.repr (decode_int bl)))
| Mfloat64 | Mfloat64al32 => Vfloat(Float.double_of_bits (Int64.repr (decode_int bl)))
| Mfloat64 => Vfloat(Float.double_of_bits (Int64.repr (decode_int bl)))
end
| None =>
match chunk with
......@@ -397,19 +395,19 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) :
| Vint n, Mint16unsigned, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n)
| Vint n, Mint32, Mint32 => v2 = Vint n
| Vint n, Mint32, Mfloat32 => v2 = Vfloat(Float.single_of_bits n)
| Vint n, (Mint64 | Mfloat32 | Mfloat64 | Mfloat64al32), _ => v2 = Vundef
| Vint n, (Mint64 | Mfloat32 | Mfloat64), _ => v2 = Vundef
| Vint n, _, _ => True (**r nothing meaningful to say about v2 *)
| Vptr b ofs, Mint32, Mint32 => v2 = Vptr b ofs
| Vptr b ofs, _, _ => v2 = Vundef
| Vlong n, Mint64, Mint64 => v2 = Vlong n
| Vlong n, Mint64, (Mfloat64 | Mfloat64al32) => v2 = Vfloat(Float.double_of_bits n)
| Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64|Mfloat64al32), _ => v2 = Vundef
| Vlong n, Mint64, Mfloat64 => v2 = Vfloat(Float.double_of_bits n)
| Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64), _ => v2 = Vundef
| Vlong n, _, _ => True (**r nothing meaningful to say about v2 *)
| Vfloat f, Mfloat32, Mfloat32 => v2 = Vfloat(Float.singleoffloat f)
| Vfloat f, Mfloat32, Mint32 => v2 = Vint(Float.bits_of_single f)
| Vfloat f, (Mfloat64 | Mfloat64al32), (Mfloat64 | Mfloat64al32) => v2 = Vfloat f
| Vfloat f, Mfloat64, Mfloat64 => v2 = Vfloat f
| Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mint64), _ => v2 = Vundef
| Vfloat f, (Mfloat64 | Mfloat64al32), Mint64 => v2 = Vlong(Float.bits_of_double f)
| Vfloat f, Mfloat64, Mint64 => v2 = Vlong(Float.bits_of_double f)
| Vfloat f, _, _ => True (* nothing interesting to say about v2 *)
end.
......@@ -439,15 +437,10 @@ Opaque inj_pointer.
rewrite decode_encode_int_4. auto.
rewrite decode_encode_int_8. auto.
rewrite decode_encode_int_8. auto.
rewrite decode_encode_int_8. auto.
rewrite decode_encode_int_4. auto.
rewrite decode_encode_int_4. decEq. apply Float.single_of_bits_of_single.
rewrite decode_encode_int_8. auto.
rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double.
rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double.
rewrite decode_encode_int_8. auto.
rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double.
rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double.
change (proj_bytes (inj_pointer 4 b i)) with (@None (list byte)). simpl.
unfold proj_pointer. generalize (check_inj_pointer b i 4%nat).
Transparent inj_pointer.
......
......@@ -727,6 +727,7 @@ Proof.
rewrite pred_dec_false; auto.
Qed.
(*
Theorem load_float64al32:
forall m b ofs v,
load Mfloat64 m b ofs = Some v -> load Mfloat64al32 m b ofs = Some v.
......@@ -742,6 +743,7 @@ Theorem loadv_float64al32:
Proof.
unfold loadv; intros. destruct a; auto. apply load_float64al32; auto.
Qed.
*)
(** ** Properties related to [loadbytes] *)
......@@ -1411,6 +1413,7 @@ Proof.
auto.
Qed.
(*
Theorem store_float64al32:
forall m b ofs v m',
store Mfloat64 m b ofs v = Some m' -> store Mfloat64al32 m b ofs v = Some m'.
......@@ -1428,6 +1431,7 @@ Theorem storev_float64al32:
Proof.
unfold storev; intros. destruct a; auto. apply store_float64al32; auto.
Qed.
*)
(** ** Properties related to [storebytes]. *)
......@@ -3422,7 +3426,7 @@ Proof.
destruct H0. subst; exists Mint8unsigned; auto.
destruct H0. subst; exists Mint16unsigned; auto.
destruct H0. subst; exists Mint32; auto.
subst; exists Mfloat64; auto.
subst; exists Mint64; auto.
destruct R as [chunk [A B]].
assert (valid_access m chunk b ofs Nonempty).
split. red; intros; apply H3. omega. congruence.
......
......@@ -31,7 +31,6 @@ let name_of_chunk = function
| Mint64 -> "int64"
| Mfloat32 -> "float32"
| Mfloat64 -> "float64"
| Mfloat64al32 -> "float64al32"
let name_of_external = function
| EF_external(name, sg) -> sprintf "extern %S" (extern_atom name)
......
......@@ -682,7 +682,7 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
| Mint32, Vptr b ofs => Vptr b ofs
| Mint64, Vlong n => Vlong n
| Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f)
| (Mfloat64 | Mfloat64al32), Vfloat f => Vfloat f
| Mfloat64, Vfloat f => Vfloat f
| _, _ => Vundef
end.
......
......@@ -142,7 +142,10 @@ let il32pll64 = {
(* Canned configurations for some ABIs *)
let x86_32 =
{ ilp32ll64 with name = "x86_32"; char_signed = true }
{ ilp32ll64 with name = "x86_32";
char_signed = true;
alignof_longlong = 4; alignof_double = 4;
sizeof_longdouble = 12; alignof_longdouble = 4 }
let x86_64 =
{ i32lpll64 with name = "x86_64"; char_signed = true }
let win64 =
......
......@@ -33,12 +33,7 @@ let option_dcmedium = ref false
let option_dclight = ref false
let option_dcminor = ref false
let option_drtl = ref false
let option_dtailcall = ref false
let option_dinlining = ref false
let option_dconstprop = ref false
let option_dcse = ref false
let option_ddeadcode = ref false
let option_dalloc = ref false
let option_dltl = ref false
let option_dalloctrace = ref false
let option_dmach = ref false
let option_dasm = ref false
......
......@@ -74,12 +74,7 @@ Require Asmgenproof.
(** Pretty-printers (defined in Caml). *)
Parameter print_Clight: Clight.program -> unit.
Parameter print_Cminor: Cminor.program -> unit.
Parameter print_RTL: RTL.program -> unit.
Parameter print_RTL_tailcall: RTL.program -> unit.
Parameter print_RTL_inline: RTL.program -> unit.
Parameter print_RTL_constprop: RTL.program -> unit.
Parameter print_RTL_cse: RTL.program -> unit.
Parameter print_RTL_deadcode: RTL.program -> unit.
Parameter print_RTL: Z -> RTL.program -> unit.
Parameter print_LTL: LTL.program -> unit.
Parameter print_Mach: Mach.program -> unit.
......@@ -112,19 +107,21 @@ Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
OK f
@@ print print_RTL
@@ print (print_RTL 0)
@@ Tailcall.transf_program
@@ print print_RTL_tailcall
@@ print (print_RTL 1)
@@@ Inlining.transf_program
@@ print (print_RTL 2)
@@ Renumber.transf_program
@@ print print_RTL_inline
@@ print (print_RTL 3)
@@ Constprop.transf_program
@@ print (print_RTL 4)
@@ Renumber.transf_program
@@ print print_RTL_constprop
@@ print (print_RTL 5)
@@@ CSE.transf_program
@@ print print_RTL_cse
@@ print (print_RTL 6)
@@@ Deadcode.transf_program
@@ print print_RTL_deadcode
@@ print (print_RTL 7)
@@@ Allocation.transf_program
@@ print print_LTL
@@ Tunneling.tunnel_program
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment