diff options
| -rw-r--r-- | Changelog | 4 | ||||
| -rw-r--r-- | arm/Asm.v | 4 | ||||
| -rw-r--r-- | arm/Asmgen.v | 4 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 4 | ||||
| -rw-r--r-- | backend/CMlexer.mll | 1 | ||||
| -rw-r--r-- | backend/CMparser.mly | 2 | ||||
| -rw-r--r-- | backend/CMtypecheck.ml | 1 | ||||
| -rw-r--r-- | backend/Cminor.v | 5 | ||||
| -rw-r--r-- | backend/NeedDomain.v | 1 | ||||
| -rw-r--r-- | backend/PrintRTL.ml | 26 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 7 | ||||
| -rw-r--r-- | checklink/Check.ml | 4 | ||||
| -rw-r--r-- | common/AST.v | 7 | ||||
| -rw-r--r-- | common/Memdata.v | 23 | ||||
| -rw-r--r-- | common/Memory.v | 6 | ||||
| -rw-r--r-- | common/PrintAST.ml | 1 | ||||
| -rw-r--r-- | common/Values.v | 2 | ||||
| -rw-r--r-- | cparser/Machine.ml | 5 | ||||
| -rw-r--r-- | driver/Clflags.ml | 7 | ||||
| -rw-r--r-- | driver/Compiler.v | 21 | ||||
| -rw-r--r-- | driver/Driver.ml | 29 | ||||
| -rw-r--r-- | exportclight/ExportClight.ml | 1 | ||||
| -rw-r--r-- | extraction/extraction.v | 12 | ||||
| -rw-r--r-- | ia32/Asm.v | 8 | ||||
| -rw-r--r-- | ia32/Asmgen.v | 4 | ||||
| -rw-r--r-- | ia32/Asmgenproof1.v | 8 | ||||
| -rw-r--r-- | ia32/Machregs.v | 2 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 4 | ||||
| -rw-r--r-- | powerpc/Asm.v | 8 | ||||
| -rw-r--r-- | powerpc/Asmgen.v | 4 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 4 |
31 files changed, 80 insertions, 139 deletions
@@ -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' diff --git a/arm/Asmgen.v b/arm/Asmgen.v index b6cb2b3..fcc5061 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -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") diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 99dfa46..01b881f 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -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 diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index c400c5e..fb9173d 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -65,7 +65,6 @@ rule token = parse | "float" { FLOAT } | "float32" { FLOAT32 } | "float64" { FLOAT64 } - | "float64al32" { FLOAT64AL32 } | "floatofint" { FLOATOFINT } | "floatofintu" { FLOATOFINTU } | "floatoflong" { FLOATOFLONG } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 5d93b84..f0f92f2 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -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 } ; diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index d0bccca..5e46d76 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -168,7 +168,6 @@ let type_chunk = function | Mint64 -> tlong | Mfloat32 -> tfloat | Mfloat64 -> tfloat - | Mfloat64al32 -> tfloat let name_of_chunk = PrintAST.name_of_chunk diff --git a/backend/Cminor.v b/backend/Cminor.v index c12c6fc..aaf7510 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -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 diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 47f6975..f050c72 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -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: diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 137f65b..5c8347c 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -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 - diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index f11cd52..eee4762 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -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. diff --git a/checklink/Check.ml b/checklink/Check.ml index 8e8afd1..6c1739c 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -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) diff --git a/common/AST.v b/common/AST.v index 5eee291..6f35be0 100644 --- a/common/AST.v +++ b/common/AST.v @@ -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. diff --git a/common/Memdata.v b/common/Memdata.v index d8d347e..1b74705 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -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. diff --git a/common/Memory.v b/common/Memory.v index 0260a89..9afdfd3 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -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. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index a3f6bcf..329c0c7 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -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) diff --git a/common/Values.v b/common/Values.v index 99a994b..5ac9f3e 100644 --- a/common/Values.v +++ b/common/Values.v @@ -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. diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 374e1bb..d8c5575 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -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 = diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 4d6e3f6..5d068b6 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -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 diff --git a/driver/Compiler.v b/driver/Compiler.v index d088bc9..d3628b5 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -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 diff --git a/driver/Driver.ml b/driver/Driver.ml index d5b99d4..c35ac1f 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -147,14 +147,9 @@ let compile_c_ast sourcename csyntax ofile = else None in set_dest PrintClight.destination option_dclight ".light.c"; set_dest PrintCminor.destination option_dcminor ".cm"; - set_dest PrintRTL.destination_rtl option_drtl ".rtl"; - set_dest PrintRTL.destination_tailcall option_dtailcall ".tailcall.rtl"; - set_dest PrintRTL.destination_inlining option_dinlining ".inlining.rtl"; - set_dest PrintRTL.destination_constprop option_dconstprop ".constprop.rtl"; - set_dest PrintRTL.destination_cse option_dcse ".cse.rtl"; - set_dest PrintRTL.destination_deadcode option_ddeadcode ".deadcode.rtl"; + set_dest PrintRTL.destination option_drtl ".rtl"; set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; - set_dest PrintLTL.destination option_dalloc ".alloc.ltl"; + set_dest PrintLTL.destination option_dltl ".ltl"; set_dest PrintMach.destination option_dmach ".mach"; (* Convert to Asm *) let asm = @@ -427,12 +422,8 @@ Tracing options: -dc Save generated Compcert C in <file>.compcert.c -dclight Save generated Clight in <file>.light.c -dcminor Save generated Cminor in <file>.cm - -drtl Save unoptimized generated RTL in <file>.rtl - -dtailcall Save RTL after tail call optimization in <file>.tailcall.rtl - -dinlining Save RTL after inlining optimization in <file>.inlining.rtl - -dconstprop Save RTL after constant propagation in <file>.constprop.rtl - -dcse Save RTL after CSE optimization in <file>.cse.rtl - -dalloc Save LTL after register allocation in <file>.alloc.ltl + -drtl Save RTL at various optimization points in <file>.rtl.<n> + -dltl Save LTL after register allocation in <file>.ltl -dmach Save generated Mach code in <file>.mach -dasm Save generated assembly in <file>.s -sdump Save info for post-linking validation in <file>.sdump @@ -476,12 +467,7 @@ let cmdline_actions = "-dclight$", Set option_dclight; "-dcminor", Set option_dcminor; "-drtl$", Set option_drtl; - "-dtailcall$", Set option_dtailcall; - "-dinlining$", Set option_dinlining; - "-dconstprop$", Set option_dconstprop; - "-dcse$", Set option_dcse; - "-ddeadcode$", Set option_ddeadcode; - "-dalloc$", Set option_dalloc; + "-dltl$", Set option_dltl; "-dalloctrace$", Set option_dalloctrace; "-dmach$", Set option_dmach; "-dasm$", Set option_dasm; @@ -534,7 +520,10 @@ let cmdline_actions = @ f_opt "sse" option_ffpu (* backward compatibility *) let _ = - Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 }; + Gc.set { (Gc.get()) with + Gc.minor_heap_size = 524288; (* 512k *) + Gc.major_heap_increment = 4194304 (* 4M *) + }; Printexc.record_backtrace true; Machine.config := begin match Configuration.arch with diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 8c83fab..fa56a01 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -217,7 +217,6 @@ let name_of_chunk = function | Mint64 -> "Mint64" | Mfloat32 -> "Mfloat32" | Mfloat64 -> "Mfloat64" - | Mfloat64al32 -> "Mfloat64al32" let signatur p sg = fprintf p "@[<hov 2>(mksignature@ %a@ %a)@]" (print_list asttype) sg.sig_args (print_option asttype) sg.sig_res diff --git a/extraction/extraction.v b/extraction/extraction.v index 6556c87..b8442a8 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -93,12 +93,7 @@ Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2. (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". -Extract Constant Compiler.print_RTL => "PrintRTL.print_rtl". -Extract Constant Compiler.print_RTL_tailcall => "PrintRTL.print_tailcall". -Extract Constant Compiler.print_RTL_inline => "PrintRTL.print_inlining". -Extract Constant Compiler.print_RTL_constprop => "PrintRTL.print_constprop". -Extract Constant Compiler.print_RTL_cse => "PrintRTL.print_cse". -Extract Constant Compiler.print_RTL_deadcode => "PrintRTL.print_deadcode". +Extract Constant Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". @@ -118,12 +113,13 @@ Extract Inlined Constant Fappli_IEEE.B2R => "fun _ -> assert false". Extract Inlined Constant Fappli_IEEE.round_mode => "fun _ -> assert false". Extract Inlined Constant Fcalc_bracket.inbetween_loc => "fun _ -> assert false". -(* Needed in Coq 4.00 to avoid problems with Function definitions. *) +(* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. (* Go! *) + Cd "extraction". -(* Recursive Extraction Library Compiler. *) + Separate Extraction Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state @@ -486,17 +486,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmovsd_fi rd n => Next (nextinstr (rs#rd <- (Vfloat n))) m | Pmovsd_fm rd a => - exec_load Mfloat64al32 m a rs rd + exec_load Mfloat64 m a rs rd | Pmovsd_mf a r1 => - exec_store Mfloat64al32 m a rs r1 nil + exec_store Mfloat64 m a rs r1 nil | Pfld_f r1 => Next (nextinstr (rs#ST0 <- (rs r1))) m | Pfld_m a => - exec_load Mfloat64al32 m a rs ST0 + exec_load Mfloat64 m a rs ST0 | Pfstp_f rd => Next (nextinstr (rs#rd <- (rs ST0) #ST0 <- Vundef)) m | Pfstp_m a => - exec_store Mfloat64al32 m a rs ST0 (ST0 :: nil) + exec_store Mfloat64 m a rs ST0 (ST0 :: nil) | Pxchg_rr r1 r2 => Next (nextinstr (rs#r1 <- (rs r2) #r2 <- (rs r1))) m (** Moves with conversion *) diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 740dff8..fa4112d 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -441,7 +441,7 @@ Definition transl_load (chunk: memory_chunk) do r <- ireg_of dest; OK(Pmov_rm r am :: k) | Mfloat32 => do r <- freg_of dest; OK(Pcvtss2sd_fm r am :: k) - | Mfloat64 | Mfloat64al32 => + | Mfloat64 => do r <- freg_of dest; OK(Pmovsd_fm r am :: k) | Mint64 => Error (msg "Asmgen.transl_load") @@ -460,7 +460,7 @@ Definition transl_store (chunk: memory_chunk) do r <- ireg_of src; OK(Pmov_mr am r :: k) | Mfloat32 => do r <- freg_of src; OK(Pcvtsd2ss_mf am r :: k) - | Mfloat64 | Mfloat64al32 => + | Mfloat64 => do r <- freg_of src; OK(Pmovsd_mf am r :: k) | Mint64 => Error (msg "Asmgen.transl_store") diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 5d3df67..6f2aee5 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -997,10 +997,6 @@ Proof. auto. decEq. apply Pregmap.gso; auto with asmgen. exists rs2. split. destruct chunk; ArgsInv; apply exec_straight_one; auto. - (* Mfloat64 -> Mfloat64al32 *) - rewrite <- H. simpl. unfold exec_load. rewrite H1. - destruct (eval_addrmode ge x rs); simpl in *; try discriminate. - erewrite Mem.load_float64al32; eauto. split. unfold rs2. rewrite nextinstr_nf_inv1. Simplifs. apply preg_of_data. intros. unfold rs2. Simplifs. Qed. @@ -1047,10 +1043,6 @@ Proof. intros. Transparent destroyed_by_store. simpl in H2. simpl. Simplifs. (* float64 *) econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. erewrite Mem.storev_float64al32; eauto. auto. - intros. Simplifs. -(* float64al32 *) - econstructor; split. apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto. intros. Simplifs. Qed. diff --git a/ia32/Machregs.v b/ia32/Machregs.v index 826dadf..47340ec 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -94,7 +94,7 @@ Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mre | Mint8signed | Mint8unsigned => AX :: CX :: nil | Mint16signed | Mint16unsigned | Mint32 | Mint64 => nil | Mfloat32 => X7 :: nil - | Mfloat64 | Mfloat64al32 => FP0 :: nil + | Mfloat64 => FP0 :: nil end. Definition destroyed_by_cond (cond: condition): list mreg := diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 0a666cb..01034f1 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -354,7 +354,7 @@ let print_builtin_vload_common oc chunk addr res = end | Mfloat32, [FR res] -> fprintf oc " cvtss2sd %a, %a\n" addressing addr freg res - | (Mfloat64 | Mfloat64al32), [FR res] -> + | Mfloat64, [FR res] -> fprintf oc " movsd %a, %a\n" addressing addr freg res | _ -> assert false @@ -396,7 +396,7 @@ let print_builtin_vstore_common oc chunk addr src tmp = | Mfloat32, [FR src] -> fprintf oc " cvtsd2ss %a, %%xmm7\n" freg src; fprintf oc " movss %%xmm7, %a\n" addressing addr - | (Mfloat64 | Mfloat64al32), [FR src] -> + | Mfloat64, [FR src] -> fprintf oc " movsd %a, %a\n" freg src addressing addr | _ -> assert false diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 4499f01..7a75d8f 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -676,9 +676,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plbzx rd r1 r2 => load2 Mint8unsigned rd r1 r2 rs m | Plfd rd cst r1 => - load1 Mfloat64al32 rd cst r1 rs m + load1 Mfloat64 rd cst r1 rs m | Plfdx rd r1 r2 => - load2 Mfloat64al32 rd r1 r2 rs m + load2 Mfloat64 rd r1 r2 rs m | Plfs rd cst r1 => load1 Mfloat32 rd cst r1 rs m | Plfsx rd r1 r2 => @@ -745,9 +745,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pstbx rd r1 r2 => store2 Mint8unsigned rd r1 r2 rs m | Pstfd rd cst r1 => - store1 Mfloat64al32 rd cst r1 rs m + store1 Mfloat64 rd cst r1 rs m | Pstfdx rd r1 r2 => - store2 Mfloat64al32 rd r1 r2 rs m + store2 Mfloat64 rd r1 r2 rs m | Pstfs rd cst r1 => match store1 Mfloat32 rd cst r1 rs m with | Next rs' m' => Next (rs'#FPR13 <- Vundef) m' diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 39c0d1b..6b66686 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -563,7 +563,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) | Mfloat32 => do r <- freg_of dst; transl_memory_access (Plfs r) (Plfsx r) addr args GPR12 k - | Mfloat64 | Mfloat64al32 => + | Mfloat64 => do r <- freg_of dst; transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k | Mint64 => @@ -586,7 +586,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) | Mfloat32 => do r <- freg_of src; transl_memory_access (Pstfs r) (Pstfsx r) addr args temp k - | Mfloat64 | Mfloat64al32 => + | Mfloat64 => do r <- freg_of src; transl_memory_access (Pstfd r) (Pstfdx r) addr args temp k | Mint64 => diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 6d0b52c..b9778c4 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -399,7 +399,7 @@ let print_builtin_vload_common oc chunk base offset res = fprintf oc " lwz %a, %a(%a)\n" ireg res constant offset ireg base | Mfloat32, FR res -> fprintf oc " lfs %a, %a(%a)\n" freg res constant offset ireg base - | (Mfloat64 | Mfloat64al32), FR res -> + | Mfloat64, FR res -> fprintf oc " lfd %a, %a(%a)\n" freg res constant offset ireg base (* Mint64 is special-cased below *) | _ -> @@ -456,7 +456,7 @@ let print_builtin_vstore_common oc chunk base offset src = | Mfloat32, FR src -> fprintf oc " frsp %a, %a\n" freg FPR13 freg src; fprintf oc " stfs %a, %a(%a)\n" freg FPR13 constant offset ireg base - | (Mfloat64 | Mfloat64al32), FR src -> + | Mfloat64, FR src -> fprintf oc " stfd %a, %a(%a)\n" freg src constant offset ireg base (* Mint64 is special-cased below *) | _ -> |