From 83023733e8ac5fa28893b260664f6d6527b481ab Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 15 Jan 2015 15:42:14 +0100 Subject: Added variable to the Makefile to specify additional linker commands and changed the configure script to deactivated the checklink build if needed. --- Makefile | 4 ++-- Makefile.extr | 4 ++-- configure | 7 +++++-- 3 files changed, 9 insertions(+), 6 deletions(-) diff --git a/Makefile b/Makefile index 6ed50ce2..b4db7be9 100644 --- a/Makefile +++ b/Makefile @@ -174,9 +174,9 @@ doc/coq2html.ml: doc/coq2html.mll ocamllex -q doc/coq2html.mll tools/ndfun: tools/ndfun.ml - ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml + ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml $(LINKERSPEC) tools/modorder: tools/modorder.ml - ocamlopt -o tools/modorder str.cmxa tools/modorder.ml + ocamlopt -o tools/modorder str.cmxa tools/modorder.ml $(LINKERSPEC) latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) diff --git a/Makefile.extr b/Makefile.extr index 35ae5f7b..70b0cb67 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -90,11 +90,11 @@ CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx) ccomp: $(CCOMP_OBJS) @echo "Linking $@" - @$(OCAMLOPT) -o $@ $(LIBS) $+ + @$(OCAMLOPT) -o $@ $(LIBS) $+ $(LINKERSPEC) ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" - @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ + @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ $(LINKERSPEC) ifeq ($(CCHECKLINK),true) diff --git a/configure b/configure index 10b2c2f1..820ab650 100755 --- a/configure +++ b/configure @@ -18,6 +18,7 @@ libdir='$(PREFIX)/lib/compcert' toolprefix='' target='' has_runtime_lib=true +build_checklink=true usage='Usage: ./configure [options] target @@ -64,6 +65,8 @@ while : ; do toolprefix="$2"; shift;; -no-runtime-lib) has_runtime_lib=false; shift;; + -no-checklink) + build_checklink=false; shift;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; @@ -89,7 +92,7 @@ case "$target" in casmruntime="${toolprefix}gcc -c -Wa,-mregnames" clinker="${toolprefix}gcc" libmath="-lm" - cchecklink=true;; + cchecklink=build_checklink;; powerpc-eabi-diab|ppc-eabi-diab) arch="powerpc" model="standard" @@ -101,7 +104,7 @@ case "$target" in asm_supports_cfi=false clinker="${toolprefix}dcc" libmath="-lm" - cchecklink=true;; + cchecklink=build_checklink;; arm*-*) arch="arm" case "$target" in -- cgit From 5fc6c02e6c815f9ba3348ddc49b5b1d7563ec35c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 15 Jan 2015 17:42:53 +0100 Subject: Added missing $ for build_checklink --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/configure b/configure index 820ab650..447bc0a2 100755 --- a/configure +++ b/configure @@ -92,7 +92,7 @@ case "$target" in casmruntime="${toolprefix}gcc -c -Wa,-mregnames" clinker="${toolprefix}gcc" libmath="-lm" - cchecklink=build_checklink;; + cchecklink=${build_checklink};; powerpc-eabi-diab|ppc-eabi-diab) arch="powerpc" model="standard" @@ -104,7 +104,7 @@ case "$target" in asm_supports_cfi=false clinker="${toolprefix}dcc" libmath="-lm" - cchecklink=build_checklink;; + cchecklink=${build_checklink};; arm*-*) arch="arm" case "$target" in -- cgit From b3f8438c6224f537ba7a84580f432c40a63a481c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Jan 2015 15:59:08 +0100 Subject: Added new target to just remove the cm[iox] files and the build executables. --- Makefile.extr | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Makefile.extr b/Makefile.extr index 70b0cb67..2d429f76 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -156,6 +156,10 @@ clean: rm -f $(GENERATED) for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done +cleansource: + rm -f $(EXECUTABLES) + for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done + # Generation of .depend.extr depend: $(GENERATED) -- cgit From 58f6c7b5f4935fe9aca0eceb4ce8684d9816c7b5 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Jan 2015 16:37:29 +0100 Subject: Replaced 8 spaces by tabs. --- Makefile.extr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.extr b/Makefile.extr index 2d429f76..2afd6e31 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -157,7 +157,7 @@ clean: for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done cleansource: - rm -f $(EXECUTABLES) + rm -f $(EXECUTABLES) for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done # Generation of .depend.extr -- cgit From 860e340b9a383964773d9c4523fb02a1de407e7f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Jan 2015 13:02:07 +0100 Subject: Renamed LIB into VLIB to avoid clashes with environment variables. --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index b4db7be9..d6df22f0 100644 --- a/Makefile +++ b/Makefile @@ -49,7 +49,7 @@ FLOCQ=\ # General-purpose libraries (in lib/) -LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ +VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ Iteration.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \ Parmov.v UnionFind.v Wfsimpl.v \ Postorder.v FSetAVLplus.v IntvSets.v @@ -112,7 +112,7 @@ DRIVER=Compopts.v Compiler.v Complements.v # All source files -FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ +FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ $(PARSERVALIDATOR) $(PARSER) all: -- cgit From 28d7ff1fef9a47206114773d38e04361dc49820b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 20 Jan 2015 14:07:23 +0100 Subject: Follow-up to [5aecefe]: be conservative also in the case of a "common" global const variable. --- backend/ValueAnalysis.v | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 9c7ca1f7..b446e101 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -180,13 +180,30 @@ Fixpoint store_init_data_list (ab: ablock) (p: Z) (idl: list init_data) | id :: idl' => store_init_data_list (store_init_data ab p id) (p + Genv.init_data_size id) idl' end. +(** When CompCert is used in separate compilation mode, the [gvar_init] + initializer attached to a readonly global variable may not correspond + to the actual initial value of this global. This occurs in two cases: +- an [extern const] variable, which is represented by [gvar_init = nil]; +- a [const] variable without an explicit initializer, which is treated + by the linker as a "common" symbol, and is represented by + [gvar_init = Init_space sz :: nil]. + +In both cases, the variable can be defined and initialized in another +compilation unit which is later linked with the current compilation unit. *) + +Definition definitive_initializer (init: list init_data) : bool := + match init with + | nil => false + | Init_space _ :: nil => false + | _ => true + end. + Definition alloc_global (rm: romem) (idg: ident * globdef fundef unit): romem := match idg with | (id, Gfun f) => PTree.remove id rm | (id, Gvar v) => - if v.(gvar_readonly) && negb v.(gvar_volatile) - && match v.(gvar_init) with nil => false | _ => true end + if v.(gvar_readonly) && negb v.(gvar_volatile) && definitive_initializer v.(gvar_init) then PTree.set id (store_init_data_list (ablock_init Pbot) 0 v.(gvar_init)) rm else PTree.remove id rm end. @@ -1678,15 +1695,13 @@ Proof. destruct (peq id id1). congruence. eapply H; eauto. - rewrite PTree.gsspec in H0. destruct (peq id id1). + inv H0. rewrite PTree.gss. - destruct (gvar_readonly v1 && negb (gvar_volatile v1) && - match gvar_init v1 with nil => false | _ => true end) eqn:RO. + destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)) eqn:RO. InvBooleans. rewrite negb_true_iff in H4. rewrite PTree.gss in H1. exists v1. intuition congruence. rewrite PTree.grs in H1. discriminate. + rewrite PTree.gso. eapply H; eauto. - destruct (gvar_readonly v1 && negb (gvar_volatile v1) && - match gvar_init v1 with nil => false | _ => true end). + destruct (gvar_readonly v1 && negb (gvar_volatile v1) && definitive_initializer (gvar_init v1)). rewrite PTree.gso in H1; auto. rewrite PTree.gro in H1; auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. -- cgit From 9f2ca1049957004161834090a697cd4118e2fb08 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 20 Jan 2015 14:54:48 +0100 Subject: Protect against redefinition of the __i64_xxx helper library functions. This is achieved by declaring these functions in C2C.ml, then re-checking their declarations in the global environment during the Selection pass. In passing, the "hf" parameter for SelectLong functions was removed and replaced by fixed identifiers corresponding to the actual names of the helper functions. --- backend/SelectLong.vp | 152 ++++++++++++++++++++------------------- backend/SelectLongproof.v | 177 +++++++++++++++++++++++----------------------- backend/Selection.v | 53 +++++++------- backend/Selectionproof.v | 114 ++++++++++++++--------------- cfrontend/C2C.ml | 55 +++++++++++++- extraction/extraction.v | 6 -- 6 files changed, 306 insertions(+), 251 deletions(-) diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index ab4ab8c4..970386a9 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -20,31 +20,30 @@ Require Import Op. Require Import CminorSel. Require Import SelectOp. -Open Local Scope cminorsel_scope. +Local Open Scope cminorsel_scope. +Local Open Scope string_scope. (** Some operations on 64-bit integers are transformed into calls to - runtime library functions. The following record type collects - the names of these functions. *) - -Record helper_functions : Type := mk_helper_functions { - i64_dtos: ident; (**r float64 -> signed long *) - i64_dtou: ident; (**r float64 -> unsigned long *) - i64_stod: ident; (**r signed long -> float64 *) - i64_utod: ident; (**r unsigned long -> float64 *) - i64_stof: ident; (**r signed long -> float32 *) - i64_utof: ident; (**r unsigned long -> float32 *) - i64_neg: ident; (**r opposite *) - i64_add: ident; (**r addition *) - i64_sub: ident; (**r subtraction *) - i64_mul: ident; (**r multiplication 32x32->64 *) - i64_sdiv: ident; (**r signed division *) - i64_udiv: ident; (**r unsigned division *) - i64_smod: ident; (**r signed remainder *) - i64_umod: ident; (**r unsigned remainder *) - i64_shl: ident; (**r shift left *) - i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident (**r shift right signed *) -}. + runtime library functions or built-in functions. + Here are the names and signatures of these functions. *) + +Definition i64_dtos := ident_of_string "__i64_dtos". +Definition i64_dtou := ident_of_string "__i64_dtou". +Definition i64_stod := ident_of_string "__i64_stod". +Definition i64_utod := ident_of_string "__i64_utod". +Definition i64_stof := ident_of_string "__i64_stof". +Definition i64_utof := ident_of_string "__i64_utof". +Definition i64_neg := ident_of_string "__builtin_negl". +Definition i64_add := ident_of_string "__builtin_addl". +Definition i64_sub := ident_of_string "__builtin_subl". +Definition i64_mul := ident_of_string "__builtin_mull". +Definition i64_sdiv := ident_of_string "__i64_sdiv". +Definition i64_udiv := ident_of_string "__i64_udiv". +Definition i64_smod := ident_of_string "__i64_smod". +Definition i64_umod := ident_of_string "__i64_umod". +Definition i64_shl := ident_of_string "__i64_shl". +Definition i64_shr := ident_of_string "__i64_shr". +Definition i64_sar := ident_of_string "__i64_sar". Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. @@ -56,8 +55,6 @@ Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default Section SELECT. -Variable hf: helper_functions. - Definition makelong (h l: expr): expr := Eop Omakelong (h ::: l ::: Enil). @@ -124,28 +121,28 @@ Definition longofintu (e: expr) := Definition negl (e: expr) := match is_longconst e with | Some n => longconst (Int64.neg n) - | None => Ebuiltin (EF_builtin hf.(i64_neg) sig_l_l) (e ::: Enil) + | None => Ebuiltin (EF_builtin i64_neg sig_l_l) (e ::: Enil) end. Definition notl (e: expr) := splitlong e (fun h l => makelong (notint h) (notint l)). Definition longoffloat (arg: expr) := - Eexternal hf.(i64_dtos) sig_f_l (arg ::: Enil). + Eexternal i64_dtos sig_f_l (arg ::: Enil). Definition longuoffloat (arg: expr) := - Eexternal hf.(i64_dtou) sig_f_l (arg ::: Enil). + Eexternal i64_dtou sig_f_l (arg ::: Enil). Definition floatoflong (arg: expr) := - Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil). + Eexternal i64_stod sig_l_f (arg ::: Enil). Definition floatoflongu (arg: expr) := - Eexternal hf.(i64_utod) sig_l_f (arg ::: Enil). + Eexternal i64_utod sig_l_f (arg ::: Enil). Definition longofsingle (arg: expr) := longoffloat (floatofsingle arg). Definition longuofsingle (arg: expr) := longuoffloat (floatofsingle arg). Definition singleoflong (arg: expr) := - Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil). + Eexternal i64_stof sig_l_s (arg ::: Enil). Definition singleoflongu (arg: expr) := - Eexternal hf.(i64_utof) sig_l_s (arg ::: Enil). + Eexternal i64_utof sig_l_s (arg ::: Enil). Definition andl (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (and h1 h2) (and l1 l2)). @@ -166,7 +163,7 @@ Definition shllimm (e1: expr) (n: int) := makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize)) (Eop (Ointconst Int.zero) Enil) else - Eexternal hf.(i64_shl) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal i64_shl sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). Definition shrluimm (e1: expr) (n: int) := if Int.eq n Int.zero then e1 else @@ -178,7 +175,7 @@ Definition shrluimm (e1: expr) (n: int) := makelong (Eop (Ointconst Int.zero) Enil) (shruimm (highlong e1) (Int.sub n Int.iwordsize)) else - Eexternal hf.(i64_shr) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal i64_shr sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). Definition shrlimm (e1: expr) (n: int) := if Int.eq n Int.zero then e1 else @@ -191,7 +188,7 @@ Definition shrlimm (e1: expr) (n: int) := (makelong (shrimm (Eletvar 0) (Int.repr 31)) (shrimm (Eletvar 0) (Int.sub n Int.iwordsize))) else - Eexternal hf.(i64_sar) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal i64_sar sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). Definition is_intconst (e: expr) := match e with @@ -202,23 +199,23 @@ Definition is_intconst (e: expr) := Definition shll (e1 e2: expr) := match is_intconst e2 with | Some n => shllimm e1 n - | None => Eexternal hf.(i64_shl) sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal i64_shl sig_li_l (e1 ::: e2 ::: Enil) end. Definition shrlu (e1 e2: expr) := match is_intconst e2 with | Some n => shrluimm e1 n - | None => Eexternal hf.(i64_shr) sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal i64_shr sig_li_l (e1 ::: e2 ::: Enil) end. Definition shrl (e1 e2: expr) := match is_intconst e2 with | Some n => shrlimm e1 n - | None => Eexternal hf.(i64_sar) sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal i64_sar sig_li_l (e1 ::: e2 ::: Enil) end. Definition addl (e1 e2: expr) := - let default := Ebuiltin (EF_builtin hf.(i64_add) sig_ll_l) (e1 ::: e2 ::: Enil) in + let default := Ebuiltin (EF_builtin i64_add sig_ll_l) (e1 ::: e2 ::: Enil) in match is_longconst e1, is_longconst e2 with | Some n1, Some n2 => longconst (Int64.add n1 n2) | Some n1, _ => if Int64.eq n1 Int64.zero then e2 else default @@ -227,7 +224,7 @@ Definition addl (e1 e2: expr) := end. Definition subl (e1 e2: expr) := - let default := Ebuiltin (EF_builtin hf.(i64_sub) sig_ll_l) (e1 ::: e2 ::: Enil) in + let default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (e1 ::: e2 ::: Enil) in match is_longconst e1, is_longconst e2 with | Some n1, Some n2 => longconst (Int64.sub n1 n2) | Some n1, _ => if Int64.eq n1 Int64.zero then negl e2 else default @@ -237,7 +234,7 @@ Definition subl (e1 e2: expr) := Definition mull_base (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Elet (Ebuiltin (EF_builtin hf.(i64_mul) sig_ii_l) (l1 ::: l2 ::: Enil)) + Elet (Ebuiltin (EF_builtin i64_mul sig_ii_l) (l1 ::: l2 ::: Enil)) (makelong (add (add (Eop Ohighlong (Eletvar O ::: Enil)) (mul (lift l1) (lift h2))) @@ -266,11 +263,11 @@ Definition binop_long (id: ident) (sem: int64 -> int64 -> int64) (e1 e2: expr) : | _, _ => Eexternal id sig_ll_l (e1 ::: e2 ::: Enil) end. -Definition divl := binop_long hf.(i64_sdiv) Int64.divs. -Definition modl := binop_long hf.(i64_smod) Int64.mods. +Definition divl := binop_long i64_sdiv Int64.divs. +Definition modl := binop_long i64_smod Int64.mods. Definition divlu (e1 e2: expr) := - let default := Eexternal hf.(i64_udiv) sig_ll_l (e1 ::: e2 ::: Enil) in + let default := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil) in match is_longconst e1, is_longconst e2 with | Some n1, Some n2 => longconst (Int64.divu n1 n2) | _, Some n2 => @@ -282,7 +279,7 @@ Definition divlu (e1 e2: expr) := end. Definition modlu (e1 e2: expr) := - let default := Eexternal hf.(i64_umod) sig_ll_l (e1 ::: e2 ::: Enil) in + let default := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil) in match is_longconst e1, is_longconst e2 with | Some n1, Some n2 => longconst (Int64.modu n1 n2) | _, Some n2 => @@ -363,35 +360,44 @@ Definition cmpl (c: comparison) (e1 e2: expr) := End SELECT. -(** Setting up the helper functions *) +(** Checking that the helper functions are available. *) Require Import Errors. - -Local Open Scope string_scope. +Require Import Globalenvs. Local Open Scope error_monad_scope. -Parameter get_helper: Cminor.genv -> String.string -> signature -> res ident. -Parameter get_builtin: String.string -> signature -> res ident. - -Definition get_helpers (ge: Cminor.genv): res helper_functions := - do i64_dtos <- get_helper ge "__i64_dtos" sig_f_l ; - do i64_dtou <- get_helper ge "__i64_dtou" sig_f_l ; - do i64_stod <- get_helper ge "__i64_stod" sig_l_f ; - do i64_utod <- get_helper ge "__i64_utod" sig_l_f ; - do i64_stof <- get_helper ge "__i64_stof" sig_l_s ; - do i64_utof <- get_helper ge "__i64_utof" sig_l_s ; - do i64_neg <- get_builtin "__builtin_negl" sig_l_l ; - do i64_add <- get_builtin "__builtin_addl" sig_ll_l ; - do i64_sub <- get_builtin "__builtin_subl" sig_ll_l ; - do i64_mul <- get_builtin "__builtin_mull" sig_ll_l ; - do i64_sdiv <- get_helper ge "__i64_sdiv" sig_ll_l ; - do i64_udiv <- get_helper ge "__i64_udiv" sig_ll_l ; - do i64_smod <- get_helper ge "__i64_smod" sig_ll_l ; - do i64_umod <- get_helper ge "__i64_umod" sig_ll_l ; - do i64_shl <- get_helper ge "__i64_shl" sig_li_l ; - do i64_shr <- get_helper ge "__i64_shr" sig_li_l ; - do i64_sar <- get_helper ge "__i64_sar" sig_li_l ; - OK (mk_helper_functions - i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof - i64_neg i64_add i64_sub i64_mul i64_sdiv i64_udiv i64_smod i64_umod - i64_shl i64_shr i64_sar). +Definition check_helper (ge: Cminor.genv) (name_sg: ident * signature) : res unit := + let (name, sg) := name_sg in + match Genv.find_symbol ge name with + | None => + Error (CTX name :: MSG ": not declared" :: nil) + | Some b => + match Genv.find_funct_ptr ge b with + | Some (External (EF_external name' sg')) => + if ident_eq name' name && signature_eq sg' sg + then OK tt + else Error (CTX name :: MSG ": wrong declaration" :: nil) + | _ => + Error (CTX name :: MSG ": wrong declaration" :: nil) + end + end. + +Definition i64_helpers := + (i64_dtos, sig_f_l) :: + (i64_dtou, sig_f_l) :: + (i64_stod, sig_l_f) :: + (i64_utod, sig_l_f) :: + (i64_stof, sig_l_s) :: + (i64_utof, sig_l_s) :: + (i64_sdiv, sig_ll_l) :: + (i64_udiv, sig_ll_l) :: + (i64_smod, sig_ll_l) :: + (i64_umod, sig_ll_l) :: + (i64_shl, sig_li_l) :: + (i64_shr, sig_li_l) :: + (i64_sar, sig_li_l) :: + nil. + +Definition check_helpers (ge: Cminor.genv): res unit := + do x <- mmap (check_helper ge) i64_helpers; + OK tt. diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index c7c7ab2d..40c11dd8 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -32,69 +32,67 @@ Open Local Scope cminorsel_scope. (** * Axiomatization of the helper functions *) -Section HELPERS. - -Context {F V: Type} (ge: Genv.t (AST.fundef F) V). - -Definition helper_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := - exists b, exists ef, - Genv.find_symbol ge id = Some b - /\ Genv.find_funct_ptr ge b = Some (External ef) - /\ ef_sig ef = sg - /\ forall m, external_call ef ge vargs m E0 vres m. +Definition external_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := + forall F V (ge: Genv.t F V) m, + external_call (EF_external id sg) ge vargs m E0 vres m. Definition builtin_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := - forall m, external_call (EF_builtin id sg) ge vargs m E0 vres m. - -Definition i64_helpers_correct (hf: helper_functions) : Prop := - (forall x z, Val.longoffloat x = Some z -> helper_implements hf.(i64_dtos) sig_f_l (x::nil) z) - /\(forall x z, Val.longuoffloat x = Some z -> helper_implements hf.(i64_dtou) sig_f_l (x::nil) z) - /\(forall x z, Val.floatoflong x = Some z -> helper_implements hf.(i64_stod) sig_l_f (x::nil) z) - /\(forall x z, Val.floatoflongu x = Some z -> helper_implements hf.(i64_utod) sig_l_f (x::nil) z) - /\(forall x z, Val.singleoflong x = Some z -> helper_implements hf.(i64_stof) sig_l_s (x::nil) z) - /\(forall x z, Val.singleoflongu x = Some z -> helper_implements hf.(i64_utof) sig_l_s (x::nil) z) - /\(forall x, builtin_implements hf.(i64_neg) sig_l_l (x::nil) (Val.negl x)) - /\(forall x y, builtin_implements hf.(i64_add) sig_ll_l (x::y::nil) (Val.addl x y)) - /\(forall x y, builtin_implements hf.(i64_sub) sig_ll_l (x::y::nil) (Val.subl x y)) - /\(forall x y, builtin_implements hf.(i64_mul) sig_ii_l (x::y::nil) (Val.mull' x y)) - /\(forall x y z, Val.divls x y = Some z -> helper_implements hf.(i64_sdiv) sig_ll_l (x::y::nil) z) - /\(forall x y z, Val.divlu x y = Some z -> helper_implements hf.(i64_udiv) sig_ll_l (x::y::nil) z) - /\(forall x y z, Val.modls x y = Some z -> helper_implements hf.(i64_smod) sig_ll_l (x::y::nil) z) - /\(forall x y z, Val.modlu x y = Some z -> helper_implements hf.(i64_umod) sig_ll_l (x::y::nil) z) - /\(forall x y, helper_implements hf.(i64_shl) sig_li_l (x::y::nil) (Val.shll x y)) - /\(forall x y, helper_implements hf.(i64_shr) sig_li_l (x::y::nil) (Val.shrlu x y)) - /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y)). - -End HELPERS. + forall F V (ge: Genv.t F V) m, + external_call (EF_builtin id sg) ge vargs m E0 vres m. + +Axiom i64_helpers_correct : + (forall x z, Val.longoffloat x = Some z -> external_implements i64_dtos sig_f_l (x::nil) z) + /\ (forall x z, Val.longuoffloat x = Some z -> external_implements i64_dtou sig_f_l (x::nil) z) + /\ (forall x z, Val.floatoflong x = Some z -> external_implements i64_stod sig_l_f (x::nil) z) + /\ (forall x z, Val.floatoflongu x = Some z -> external_implements i64_utod sig_l_f (x::nil) z) + /\ (forall x z, Val.singleoflong x = Some z -> external_implements i64_stof sig_l_s (x::nil) z) + /\ (forall x z, Val.singleoflongu x = Some z -> external_implements i64_utof sig_l_s (x::nil) z) + /\ (forall x, builtin_implements i64_neg sig_l_l (x::nil) (Val.negl x)) + /\ (forall x y, builtin_implements i64_add sig_ll_l (x::y::nil) (Val.addl x y)) + /\ (forall x y, builtin_implements i64_sub sig_ll_l (x::y::nil) (Val.subl x y)) + /\ (forall x y, builtin_implements i64_mul sig_ii_l (x::y::nil) (Val.mull' x y)) + /\ (forall x y z, Val.divls x y = Some z -> external_implements i64_sdiv sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.divlu x y = Some z -> external_implements i64_udiv sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.modls x y = Some z -> external_implements i64_smod sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.modlu x y = Some z -> external_implements i64_umod sig_ll_l (x::y::nil) z) + /\ (forall x y, external_implements i64_shl sig_li_l (x::y::nil) (Val.shll x y)) + /\ (forall x y, external_implements i64_shr sig_li_l (x::y::nil) (Val.shrlu x y)) + /\ (forall x y, external_implements i64_sar sig_li_l (x::y::nil) (Val.shrl x y)). + +Definition helper_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (name: ident) (sg: signature) : Prop := + exists b, Genv.find_symbol ge name = Some b + /\ Genv.find_funct_ptr ge b = Some (External (EF_external name sg)). (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. -Variable hf: helper_functions. Variable ge: genv. -Hypothesis HELPERS: i64_helpers_correct ge hf. +Hypothesis HELPERS: + forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. Variable sp: val. Variable e: env. Variable m: mem. Ltac UseHelper := - red in HELPERS; + generalize i64_helpers_correct; intros; repeat (eauto; match goal with | [ H: _ /\ _ |- _ ] => destruct H end). Lemma eval_helper: forall le id sg args vargs vres, eval_exprlist ge sp e m le args vargs -> - helper_implements ge id sg vargs vres -> + In (id, sg) i64_helpers -> + external_implements id sg vargs vres -> eval_expr ge sp e m le (Eexternal id sg args) vres. Proof. - intros. destruct H0 as (b & ef & A & B & C & D). econstructor; eauto. + intros. exploit HELPERS; eauto. intros (b & A & B). econstructor; eauto. Qed. Corollary eval_helper_1: forall le id sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> - helper_implements ge id sg (varg1::nil) vres -> + In (id, sg) i64_helpers -> + external_implements id sg (varg1::nil) vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres. Proof. intros. eapply eval_helper; eauto. constructor; auto. constructor. @@ -104,7 +102,8 @@ Corollary eval_helper_2: forall le id sg arg1 arg2 varg1 varg2 vres, eval_expr ge sp e m le arg1 varg1 -> eval_expr ge sp e m le arg2 varg2 -> - helper_implements ge id sg (varg1::varg2::nil) vres -> + In (id, sg) i64_helpers -> + external_implements id sg (varg1::varg2::nil) vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres. Proof. intros. eapply eval_helper; eauto. constructor; auto. constructor; auto. constructor. @@ -113,7 +112,7 @@ Qed. Remark eval_builtin_1: forall le id sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> - builtin_implements ge id sg (varg1::nil) vres -> + builtin_implements id sg (varg1::nil) vres -> eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: Enil)) vres. Proof. intros. econstructor. econstructor. eauto. constructor. apply H0. @@ -123,7 +122,7 @@ Remark eval_builtin_2: forall le id sg arg1 arg2 varg1 varg2 vres, eval_expr ge sp e m le arg1 varg1 -> eval_expr ge sp e m le arg2 varg2 -> - builtin_implements ge id sg (varg1::varg2::nil) vres -> + builtin_implements id sg (varg1::varg2::nil) vres -> eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: arg2 ::: Enil)) vres. Proof. intros. econstructor. constructor; eauto. constructor; eauto. constructor. apply H1. @@ -371,7 +370,7 @@ Proof. f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega. Qed. -Theorem eval_negl: unary_constructor_sound (negl hf) Val.negl. +Theorem eval_negl: unary_constructor_sound negl Val.negl. Proof. unfold negl; red; intros. destruct (is_longconst a) eqn:E. econstructor; split. apply eval_longconst. @@ -395,10 +394,10 @@ Theorem eval_longoffloat: forall le a x y, eval_expr ge sp e m le a x -> Val.longoffloat x = Some y -> - exists v, eval_expr ge sp e m le (longoffloat hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longoffloat a) v /\ Val.lessdef y v. Proof. intros; unfold longoffloat. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto. UseHelper. auto. Qed. @@ -406,10 +405,10 @@ Theorem eval_longuoffloat: forall le a x y, eval_expr ge sp e m le a x -> Val.longuoffloat x = Some y -> - exists v, eval_expr ge sp e m le (longuoffloat hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longuoffloat a) v /\ Val.lessdef y v. Proof. intros; unfold longuoffloat. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto. UseHelper. auto. Qed. @@ -417,10 +416,10 @@ Theorem eval_floatoflong: forall le a x y, eval_expr ge sp e m le a x -> Val.floatoflong x = Some y -> - exists v, eval_expr ge sp e m le (floatoflong hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (floatoflong a) v /\ Val.lessdef y v. Proof. intros; unfold floatoflong. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto. UseHelper. auto. Qed. @@ -428,10 +427,10 @@ Theorem eval_floatoflongu: forall le a x y, eval_expr ge sp e m le a x -> Val.floatoflongu x = Some y -> - exists v, eval_expr ge sp e m le (floatoflongu hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (floatoflongu a) v /\ Val.lessdef y v. Proof. intros; unfold floatoflongu. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto. UseHelper. auto. Qed. @@ -439,7 +438,7 @@ Theorem eval_longofsingle: forall le a x y, eval_expr ge sp e m le a x -> Val.longofsingle x = Some y -> - exists v, eval_expr ge sp e m le (longofsingle hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longofsingle a) v /\ Val.lessdef y v. Proof. intros; unfold longofsingle. destruct x; simpl in H0; inv H0. destruct (Float32.to_long f) as [n|] eqn:EQ; simpl in H2; inv H2. @@ -453,7 +452,7 @@ Theorem eval_longuofsingle: forall le a x y, eval_expr ge sp e m le a x -> Val.longuofsingle x = Some y -> - exists v, eval_expr ge sp e m le (longuofsingle hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longuofsingle a) v /\ Val.lessdef y v. Proof. intros; unfold longuofsingle. destruct x; simpl in H0; inv H0. destruct (Float32.to_longu f) as [n|] eqn:EQ; simpl in H2; inv H2. @@ -467,10 +466,10 @@ Theorem eval_singleoflong: forall le a x y, eval_expr ge sp e m le a x -> Val.singleoflong x = Some y -> - exists v, eval_expr ge sp e m le (singleoflong hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (singleoflong a) v /\ Val.lessdef y v. Proof. intros; unfold singleoflong. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. auto. Qed. @@ -478,10 +477,10 @@ Theorem eval_singleoflongu: forall le a x y, eval_expr ge sp e m le a x -> Val.singleoflongu x = Some y -> - exists v, eval_expr ge sp e m le (singleoflongu hf a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (singleoflongu a) v /\ Val.lessdef y v. Proof. intros; unfold singleoflongu. econstructor; split. - eapply eval_helper_1; eauto. UseHelper. + eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. auto. Qed. @@ -579,7 +578,7 @@ Qed. Lemma eval_shllimm: forall n, - unary_constructor_sound (fun e => shllimm hf e n) (fun v => Val.shll v (Vint n)). + unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)). Proof. unfold shllimm; red; intros. apply eval_shift_imm; intros. @@ -609,10 +608,11 @@ Proof. simpl. erewrite <- Int64.decompose_shl_2. instantiate (1 := Int64.hiword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. + simpl; auto 20. UseHelper. auto. Qed. -Theorem eval_shll: binary_constructor_sound (shll hf) Val.shll. +Theorem eval_shll: binary_constructor_sound shll Val.shll. Proof. unfold shll; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -620,12 +620,12 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shllimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. Qed. Lemma eval_shrluimm: forall n, - unary_constructor_sound (fun e => shrluimm hf e n) (fun v => Val.shrlu v (Vint n)). + unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)). Proof. unfold shrluimm; red; intros. apply eval_shift_imm; intros. + (* n = 0 *) @@ -654,10 +654,10 @@ Proof. simpl. erewrite <- Int64.decompose_shru_2. instantiate (1 := Int64.loword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. simpl; auto 20. UseHelper. auto. Qed. -Theorem eval_shrlu: binary_constructor_sound (shrlu hf) Val.shrlu. +Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu. Proof. unfold shrlu; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -665,12 +665,12 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shrluimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. Qed. Lemma eval_shrlimm: forall n, - unary_constructor_sound (fun e => shrlimm hf e n) (fun v => Val.shrl v (Vint n)). + unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)). Proof. unfold shrlimm; red; intros. apply eval_shift_imm; intros. + (* n = 0 *) @@ -703,10 +703,10 @@ Proof. erewrite <- Int64.decompose_shr_2. instantiate (1 := Int64.loword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. simpl; auto 20. UseHelper. auto. Qed. -Theorem eval_shrl: binary_constructor_sound (shrl hf) Val.shrl. +Theorem eval_shrl: binary_constructor_sound shrl Val.shrl. Proof. unfold shrl; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -714,17 +714,17 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shrlimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. Qed. -Theorem eval_addl: binary_constructor_sound (addl hf) Val.addl. +Theorem eval_addl: binary_constructor_sound addl Val.addl. Proof. unfold addl; red; intros. - set (default := Ebuiltin (EF_builtin (i64_add hf) sig_ll_l) (a ::: b ::: Enil)). + set (default := Ebuiltin (EF_builtin i64_add sig_ll_l) (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.addl x y) v). { - econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -740,14 +740,14 @@ Proof. - auto. Qed. -Theorem eval_subl: binary_constructor_sound (subl hf) Val.subl. +Theorem eval_subl: binary_constructor_sound subl Val.subl. Proof. unfold subl; red; intros. - set (default := Ebuiltin (EF_builtin (i64_sub hf) sig_ll_l) (a ::: b ::: Enil)). + set (default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.subl x y) v). { - econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -764,7 +764,7 @@ Proof. - auto. Qed. -Lemma eval_mull_base: binary_constructor_sound (mull_base hf) Val.mull. +Lemma eval_mull_base: binary_constructor_sound mull_base Val.mull. Proof. unfold mull_base; red; intros. apply eval_splitlong2; auto. - intros. @@ -778,7 +778,7 @@ Proof. exploit eval_add. eexact E2. eexact E3. intros [v5 [E5 L5]]. exploit eval_add. eexact E5. eexact E4. intros [v6 [E6 L6]]. exists (Val.longofwords v6 (Val.loword p)); split. - EvalOp. eapply eval_builtin_2; eauto. UseHelper. + EvalOp. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. intros. unfold le1, p in *; subst; simpl in *. inv L3. inv L4. inv L5. simpl in L6. inv L6. simpl. f_equal. symmetry. apply Int64.decompose_mul. @@ -786,7 +786,7 @@ Proof. Qed. Lemma eval_mullimm: - forall n, unary_constructor_sound (fun a => mullimm hf a n) (fun v => Val.mull v (Vlong n)). + forall n, unary_constructor_sound (fun a => mullimm a n) (fun v => Val.mull v (Vlong n)). Proof. unfold mullimm; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. @@ -816,7 +816,7 @@ Proof. apply eval_mull_base; auto. apply eval_longconst. Qed. -Theorem eval_mull: binary_constructor_sound (mull hf) Val.mull. +Theorem eval_mull: binary_constructor_sound mull Val.mull. Proof. unfold mull; red; intros. destruct (is_longconst a) as [p|] eqn:LC1; @@ -836,7 +836,8 @@ Qed. Lemma eval_binop_long: forall id sem le a b x y z, (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) -> - helper_implements ge id sig_ll_l (x::y::nil) z -> + external_implements id sig_ll_l (x::y::nil) z -> + In (id, sig_ll_l) i64_helpers -> eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> exists v, eval_expr ge sp e m le (binop_long id sem a b) v /\ Val.lessdef z v. @@ -856,7 +857,7 @@ Theorem eval_divl: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divls x y = Some z -> - exists v, eval_expr ge sp e m le (divl hf a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divl a b) v /\ Val.lessdef z v. Proof. intros. eapply eval_binop_long; eauto. intros; subst; simpl in H1. @@ -864,6 +865,7 @@ Proof. || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. auto. UseHelper. + simpl; auto 20. Qed. Theorem eval_modl: @@ -871,7 +873,7 @@ Theorem eval_modl: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.modls x y = Some z -> - exists v, eval_expr ge sp e m le (modl hf a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modl a b) v /\ Val.lessdef z v. Proof. intros. eapply eval_binop_long; eauto. intros; subst; simpl in H1. @@ -879,6 +881,7 @@ Proof. || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. auto. UseHelper. + simpl; auto 20. Qed. Theorem eval_divlu: @@ -886,14 +889,14 @@ Theorem eval_divlu: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divlu x y = Some z -> - exists v, eval_expr ge sp e m le (divlu hf a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divlu a b) v /\ Val.lessdef z v. Proof. intros. unfold divlu. - set (default := Eexternal (i64_udiv hf) sig_ll_l (a ::: b ::: Enil)). + set (default := Eexternal i64_udiv sig_ll_l (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v). { - econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -929,14 +932,14 @@ Theorem eval_modlu: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.modlu x y = Some z -> - exists v, eval_expr ge sp e m le (modlu hf a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modlu a b) v /\ Val.lessdef z v. Proof. intros. unfold modlu. - set (default := Eexternal (i64_umod hf) sig_ll_l (a ::: b ::: Enil)). + set (default := Eexternal i64_umod sig_ll_l (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v). { - econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. diff --git a/backend/Selection.v b/backend/Selection.v index cd17b9fd..11125856 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -66,8 +66,6 @@ Definition store (chunk: memory_chunk) (e1 e2: expr) := Section SELECTION. -Variable hf: helper_functions. - Definition sel_constant (cst: Cminor.constant) : expr := match cst with | Cminor.Ointconst n => Eop (Ointconst n) Enil @@ -100,19 +98,19 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := | Cminor.Ointuofsingle => intuofsingle arg | Cminor.Osingleofint => singleofint arg | Cminor.Osingleofintu => singleofintu arg - | Cminor.Onegl => negl hf arg + | Cminor.Onegl => negl arg | Cminor.Onotl => notl arg | Cminor.Ointoflong => intoflong arg | Cminor.Olongofint => longofint arg | Cminor.Olongofintu => longofintu arg - | Cminor.Olongoffloat => longoffloat hf arg - | Cminor.Olonguoffloat => longuoffloat hf arg - | Cminor.Ofloatoflong => floatoflong hf arg - | Cminor.Ofloatoflongu => floatoflongu hf arg - | Cminor.Olongofsingle => longofsingle hf arg - | Cminor.Olonguofsingle => longuofsingle hf arg - | Cminor.Osingleoflong => singleoflong hf arg - | Cminor.Osingleoflongu => singleoflongu hf arg + | Cminor.Olongoffloat => longoffloat arg + | Cminor.Olonguoffloat => longuoffloat arg + | Cminor.Ofloatoflong => floatoflong arg + | Cminor.Ofloatoflongu => floatoflongu arg + | Cminor.Olongofsingle => longofsingle arg + | Cminor.Olonguofsingle => longuofsingle arg + | Cminor.Osingleoflong => singleoflong arg + | Cminor.Osingleoflongu => singleoflongu arg end. Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := @@ -138,19 +136,19 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := | Cminor.Osubfs => subfs arg1 arg2 | Cminor.Omulfs => mulfs arg1 arg2 | Cminor.Odivfs => divfs arg1 arg2 - | Cminor.Oaddl => addl hf arg1 arg2 - | Cminor.Osubl => subl hf arg1 arg2 - | Cminor.Omull => mull hf arg1 arg2 - | Cminor.Odivl => divl hf arg1 arg2 - | Cminor.Odivlu => divlu hf arg1 arg2 - | Cminor.Omodl => modl hf arg1 arg2 - | Cminor.Omodlu => modlu hf arg1 arg2 + | Cminor.Oaddl => addl arg1 arg2 + | Cminor.Osubl => subl arg1 arg2 + | Cminor.Omull => mull arg1 arg2 + | Cminor.Odivl => divl arg1 arg2 + | Cminor.Odivlu => divlu arg1 arg2 + | Cminor.Omodl => modl arg1 arg2 + | Cminor.Omodlu => modlu arg1 arg2 | Cminor.Oandl => andl arg1 arg2 | Cminor.Oorl => orl arg1 arg2 | Cminor.Oxorl => xorl arg1 arg2 - | Cminor.Oshll => shll hf arg1 arg2 - | Cminor.Oshrl => shrl hf arg1 arg2 - | Cminor.Oshrlu => shrlu hf arg1 arg2 + | Cminor.Oshll => shll arg1 arg2 + | Cminor.Oshrl => shrl arg1 arg2 + | Cminor.Oshrlu => shrlu arg1 arg2 | Cminor.Ocmp c => comp c arg1 arg2 | Cminor.Ocmpu c => compu c arg1 arg2 | Cminor.Ocmpf c => compf c arg1 arg2 @@ -248,7 +246,7 @@ Definition sel_switch_long := sel_switch (fun arg n => cmpl Ceq arg (longconst (Int64.repr n))) (fun arg n => cmplu Clt arg (longconst (Int64.repr n))) - (fun arg ofs => subl hf arg (longconst (Int64.repr ofs))) + (fun arg ofs => subl arg (longconst (Int64.repr ofs))) lowlong. (** Conversion from Cminor statements to Cminorsel statements. *) @@ -303,8 +301,8 @@ End SELECTION. (** Conversion of functions. *) -Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.function) : res function := - do body' <- sel_stmt hf ge f.(Cminor.fn_body); +Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function := + do body' <- sel_stmt ge f.(Cminor.fn_body); OK (mkfunction f.(Cminor.fn_sig) f.(Cminor.fn_params) @@ -312,12 +310,13 @@ Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.func f.(Cminor.fn_stackspace) body'). -Definition sel_fundef (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.fundef) : res fundef := - transf_partial_fundef (sel_function hf ge) f. +Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : res fundef := + transf_partial_fundef (sel_function ge) f. (** Conversion of programs. *) Definition sel_program (p: Cminor.program) : res program := let ge := Genv.globalenv p in - do hf <- get_helpers ge; transform_partial_program (sel_fundef hf ge) p. + do x <- check_helpers ge; + transform_partial_program (sel_fundef ge) p. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 672853e3..bb9bd592 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -46,9 +46,9 @@ Variable prog: Cminor.program. Variable tprog: CminorSel.program. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Variable hf: helper_functions. -Hypothesis HELPERS: i64_helpers_correct tge hf. -Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf ge) prog = OK tprog. +Hypothesis HELPERS: + forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. +Hypothesis TRANSFPROG: transform_partial_program (sel_fundef ge) prog = OK tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -65,7 +65,7 @@ Qed. Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf ge f = OK tf. + exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef ge f = OK tf. Proof. intros. eapply Genv.find_funct_ptr_transf_partial; eauto. Qed. @@ -74,7 +74,7 @@ Lemma functions_translated: forall (v v': val) (f: Cminor.fundef), Genv.find_funct ge v = Some f -> Val.lessdef v v' -> - exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf ge f = OK tf. + exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef ge f = OK tf. Proof. intros. inv H0. eapply Genv.find_funct_transf_partial; eauto. @@ -82,13 +82,13 @@ Proof. Qed. Lemma sig_function_translated: - forall f tf, sel_fundef hf ge f = OK tf -> funsig tf = Cminor.funsig f. + forall f tf, sel_fundef ge f = OK tf -> funsig tf = Cminor.funsig f. Proof. intros. destruct f; monadInv H; auto. monadInv EQ. auto. Qed. Lemma stackspace_function_translated: - forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. + forall f tf, sel_function ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. Proof. intros. monadInv H. auto. Qed. @@ -99,38 +99,18 @@ Proof. intros; eapply Genv.find_var_info_transf_partial; eauto. Qed. -Lemma helper_implements_preserved: - forall id sg vargs vres, - helper_implements ge id sg vargs vres -> - helper_implements tge id sg vargs vres. +Lemma helper_declared_preserved: + forall id sg, helper_declared ge id sg -> helper_declared tge id sg. Proof. - intros. destruct H as (b & ef & A & B & C & D). + intros id sg (b & A & B). exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q. - exists b; exists ef. - split. rewrite symbols_preserved. auto. - split. auto. - split. auto. - intros. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. -Qed. - -Lemma builtin_implements_preserved: - forall id sg vargs vres, - builtin_implements ge id sg vargs vres -> - builtin_implements tge id sg vargs vres. -Proof. - unfold builtin_implements; intros. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + exists b; split; auto. rewrite symbols_preserved. auto. Qed. -Lemma helpers_correct_preserved: - forall h, i64_helpers_correct ge h -> i64_helpers_correct tge h. +Let HELPERS': + forall name sg, In (name, sg) i64_helpers -> helper_declared tge name sg. Proof. - unfold i64_helpers_correct; intros. - repeat (match goal with [ H: _ /\ _ |- _ /\ _ ] => destruct H; split end); - intros; try (eapply helper_implements_preserved; eauto); - try (eapply builtin_implements_preserved; eauto). + intros. apply helper_declared_preserved. auto. Qed. Section CMCONSTR. @@ -192,7 +172,7 @@ Lemma eval_sel_unop: forall le op a1 v1 v, eval_expr tge sp e m le a1 v1 -> eval_unop op v1 = Some v -> - exists v', eval_expr tge sp e m le (sel_unop hf op a1) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_cast8unsigned; auto. @@ -235,7 +215,7 @@ Lemma eval_sel_binop: eval_expr tge sp e m le a1 v1 -> eval_expr tge sp e m le a2 v2 -> eval_binop op v1 v2 m = Some v -> - exists v', eval_expr tge sp e m le (sel_binop hf op a1 a2) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_add; auto. @@ -456,7 +436,7 @@ Lemma sel_switch_long_correct: forall dfl cases arg sp e m i t le, validate_switch Int64.modulus dfl cases t = true -> eval_expr tge sp e m le arg (Vlong i) -> - eval_exitexpr tge sp e m le (XElet arg (sel_switch_long hf O t)) (switch_target (Int64.unsigned i) dfl cases). + eval_exitexpr tge sp e m le (XElet arg (sel_switch_long O t)) (switch_target (Int64.unsigned i) dfl cases). Proof. intros. eapply sel_switch_correct with (R := Rlong); eauto. - intros until n; intros EVAL R RANGE. @@ -470,7 +450,7 @@ Proof. rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. unfold Int64.max_unsigned; omega. - intros until n; intros EVAL R RANGE. - exploit eval_subl. eexact HELPERS. eexact EVAL. apply eval_longconst with (n := Int64.repr n). + exploit eval_subl. eexact EVAL. apply eval_longconst with (n := Int64.repr n). intros (vb & A & B). inv R. simpl in B. inv B. econstructor; split; eauto. replace ((Int64.unsigned n0 - n) mod Int64.modulus) @@ -564,7 +544,7 @@ Lemma sel_expr_correct: Cminor.eval_expr ge sp e m a v -> forall e' le m', env_lessdef e e' -> Mem.extends m m' -> - exists v', eval_expr tge sp e' m' le (sel_expr hf a) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'. Proof. induction 1; intros; simpl. (* Evar *) @@ -601,7 +581,7 @@ Lemma sel_exprlist_correct: Cminor.eval_exprlist ge sp e m a v -> forall e' le m', env_lessdef e e' -> Mem.extends m m' -> - exists v', eval_exprlist tge sp e' m' le (sel_exprlist hf a) v' /\ Val.lessdef_list v v'. + exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'. Proof. induction 1; intros; simpl. exists (@nil val); split; auto. constructor. @@ -616,21 +596,21 @@ Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop := | match_cont_stop: match_cont Cminor.Kstop Kstop | match_cont_seq: forall s s' k k', - sel_stmt hf ge s = OK s' -> + sel_stmt ge s = OK s' -> match_cont k k' -> match_cont (Cminor.Kseq s k) (Kseq s' k') | match_cont_block: forall k k', match_cont k k' -> match_cont (Cminor.Kblock k) (Kblock k') | match_cont_call: forall id f sp e k f' e' k', - sel_function hf ge f = OK f' -> + sel_function ge f = OK f' -> match_cont k k' -> env_lessdef e e' -> match_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k'). Inductive match_states: Cminor.state -> CminorSel.state -> Prop := | match_state: forall f f' s k s' k' sp e m e' m' - (TF: sel_function hf ge f = OK f') - (TS: sel_stmt hf ge s = OK s') + (TF: sel_function ge f = OK f') + (TS: sel_stmt ge s = OK s') (MC: match_cont k k') (LD: env_lessdef e e') (ME: Mem.extends m m'), @@ -638,7 +618,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.State f s k sp e m) (State f' s' k' sp e' m') | match_callstate: forall f f' args args' k k' m m' - (TF: sel_fundef hf ge f = OK f') + (TF: sel_fundef ge f = OK f') (MC: match_cont k k') (LD: Val.lessdef_list args args') (ME: Mem.extends m m'), @@ -653,7 +633,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.Returnstate v k m) (Returnstate v' k' m') | match_builtin_1: forall ef args args' optid f sp e k m al f' e' k' m' - (TF: sel_function hf ge f = OK f') + (TF: sel_function ge f = OK f') (MC: match_cont k k') (LDA: Val.lessdef_list args args') (LDE: env_lessdef e e') @@ -663,7 +643,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) (State f' (Sbuiltin optid ef al) k' sp e' m') | match_builtin_2: forall v v' optid f sp e k m f' e' m' k' - (TF: sel_function hf ge f = OK f') + (TF: sel_function ge f = OK f') (MC: match_cont k k') (LDV: Val.lessdef v v') (LDE: env_lessdef e e') @@ -681,16 +661,16 @@ Qed. Remark find_label_commut: forall lbl s k s' k', match_cont k k' -> - sel_stmt hf ge s = OK s' -> + sel_stmt ge s = OK s' -> match Cminor.find_label lbl s k, find_label lbl s' k' with | None, None => True - | Some(s1, k1), Some(s1', k1') => sel_stmt hf ge s1 = OK s1' /\ match_cont k1 k1' + | Some(s1, k1), Some(s1', k1') => sel_stmt ge s1 = OK s1' /\ match_cont k1 k1' | _, _ => False end. Proof. induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto. (* store *) - unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto. + unfold store. destruct (addressing m (sel_expr e)); simpl; auto. (* call *) destruct (classify_call ge e); simpl; auto. (* tailcall *) @@ -854,7 +834,7 @@ Proof. - (* Slabel *) left; econstructor; split. constructor. constructor; auto. - (* Sgoto *) - assert (sel_stmt hf ge (Cminor.fn_body f) = OK (fn_body f')). + assert (sel_stmt ge (Cminor.fn_body f) = OK (fn_body f')). { monadInv TF; simpl; auto. } exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)). apply call_cont_commut; eauto. eauto. @@ -922,19 +902,39 @@ Qed. End PRESERVATION. -Axiom get_helpers_correct: - forall ge hf, get_helpers ge = OK hf -> i64_helpers_correct ge hf. +Lemma check_helper_correct: + forall ge name sg res, + check_helper ge (name, sg) = OK res -> helper_declared ge name sg. +Proof with (try discriminate). + unfold check_helper; intros. + destruct (Genv.find_symbol ge name) as [b|] eqn:FS... + destruct (Genv.find_funct_ptr ge b) as [fd|] eqn:FP... + destruct fd... destruct e... destruct (ident_eq name0 name)... + destruct (signature_eq sg0 sg)... + subst. exists b; auto. +Qed. + +Lemma check_helpers_correct: + forall ge res, check_helpers ge = OK res -> + forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. +Proof. + unfold check_helpers; intros ge res CH name sg. + monadInv CH. generalize (mmap_inversion _ _ EQ). + generalize i64_helpers x. induction 1; simpl; intros. + contradiction. + destruct H1. subst a1. eapply check_helper_correct; eauto. eauto. +Qed. Theorem transf_program_correct: forall prog tprog, sel_program prog = OK tprog -> forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog). Proof. - intros. unfold sel_program in H. - destruct (get_helpers (Genv.globalenv prog)) as [hf|] eqn:E; simpl in H; try discriminate. - apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). + intros. unfold sel_program in H. set (ge := Genv.globalenv prog) in *. + destruct (check_helpers ge) eqn:CH; simpl in H; try discriminate. + apply forward_simulation_opt with (match_states := match_states prog tprog) (measure := measure). eapply public_preserved; eauto. apply sel_initial_states; auto. apply sel_final_states; auto. - apply sel_step_correct; auto. eapply helpers_correct_preserved; eauto. apply get_helpers_correct. auto. + apply sel_step_correct; auto. eapply check_helpers_correct; eauto. Qed. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 118b6d2d..584c265a 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -188,7 +188,60 @@ let builtins_generic = { "__compcert_va_float64", (TFloat(FDouble, []), [TPtr(TVoid [], [])], - false) + false); + (* Helper functions for int64 arithmetic *) + "__i64_dtos", + (TInt(ILongLong, []), + [TFloat(FDouble, [])], + false); + "__i64_dtou", + (TInt(IULongLong, []), + [TFloat(FDouble, [])], + false); + "__i64_stod", + (TFloat(FDouble, []), + [TInt(ILongLong, [])], + false); + "__i64_utod", + (TFloat(FDouble, []), + [TInt(IULongLong, [])], + false); + "__i64_stof", + (TFloat(FFloat, []), + [TInt(ILongLong, [])], + false); + "__i64_utof", + (TFloat(FFloat, []), + [TInt(IULongLong, [])], + false); + "__i64_sdiv", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(ILongLong, [])], + false); + "__i64_udiv", + (TInt(IULongLong, []), + [TInt(IULongLong, []); TInt(IULongLong, [])], + false); + "__i64_smod", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(ILongLong, [])], + false); + "__i64_umod", + (TInt(IULongLong, []), + [TInt(IULongLong, []); TInt(IULongLong, [])], + false); + "__i64_shl", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(IInt, [])], + false); + "__i64_shr", + (TInt(IULongLong, []), + [TInt(IULongLong, []); TInt(IInt, [])], + false); + "__i64_sar", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(IInt, [])], + false) ] } diff --git a/extraction/extraction.v b/extraction/extraction.v index ee496ffa..94ac6f52 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -57,12 +57,6 @@ Extract Constant Iteration.GenIter.iterate => (* Selection *) -Extract Constant SelectLong.get_helper => - "fun ge s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". -Extract Constant SelectLong.get_builtin => - "fun s sg -> - Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". Extract Constant Selection.compile_switch => "Switchaux.compile_switch". (* RTLgen *) -- cgit