diff options
| -rw-r--r-- | arm/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 4 | ||||
| -rw-r--r-- | backend/CMparser.mly | 12 | ||||
| -rw-r--r-- | backend/SelectLong.vp | 123 | ||||
| -rw-r--r-- | backend/SelectLongproof.v | 195 | ||||
| -rw-r--r-- | backend/Selection.v | 110 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 162 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 13 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 8 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 8 | ||||
| -rw-r--r-- | common/AST.v | 20 | ||||
| -rw-r--r-- | common/Determinism.v | 5 | ||||
| -rw-r--r-- | common/Events.v | 13 | ||||
| -rw-r--r-- | common/PrintAST.ml | 10 | ||||
| -rw-r--r-- | driver/Interp.ml | 6 | ||||
| -rw-r--r-- | exportclight/Clightdefs.v | 1 | ||||
| -rw-r--r-- | exportclight/Clightgen.ml | 2 | ||||
| -rw-r--r-- | exportclight/ExportClight.ml | 26 | ||||
| -rw-r--r-- | extraction/extraction.v | 4 | ||||
| -rw-r--r-- | ia32/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | ia32/Machregs.v | 23 | ||||
| -rw-r--r-- | ia32/TargetPrinter.ml | 4 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | powerpc/Machregs.v | 33 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 4 |
25 files changed, 431 insertions, 361 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 990f207d..fad13c9f 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -377,7 +377,7 @@ let expand_instruction instr = | Pbuiltin (ef,args,res) -> begin match ef with | EF_builtin (name,sg) -> - expand_builtin_inline (extern_atom name) args res + expand_builtin_inline (camlstring_of_coqstring name) args res | EF_vload chunk -> expand_builtin_vload chunk args res | EF_vstore chunk -> diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 2e676090..04226900 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -777,7 +777,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = begin match ef with | EF_annot(txt, targs) -> fprintf oc "%s annotation: " comment; - print_annot_text preg "sp" oc (extern_atom txt) args; + print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args; 0 | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg "sp" oc @@ -785,7 +785,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = 0 | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (extern_atom txt) sg args res; + print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment; 5 (* hoping this is an upper bound... *) | _ -> diff --git a/backend/CMparser.mly b/backend/CMparser.mly index b48a486e..41bd35a1 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -35,9 +35,9 @@ type ef_token = let mkef sg toks = match toks with | [EFT_tok "extern"; EFT_string s] -> - EF_external(intern_string s, sg) + EF_external(coqstring_of_camlstring s, sg) | [EFT_tok "builtin"; EFT_string s] -> - EF_builtin(intern_string s, sg) + EF_builtin(coqstring_of_camlstring s, sg) | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c] -> EF_vload c | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c] -> @@ -49,12 +49,12 @@ let mkef sg toks = | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] -> EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al) | [EFT_tok "annot"; EFT_string txt] -> - EF_annot(intern_string txt, sg.sig_args) + EF_annot(coqstring_of_camlstring txt, sg.sig_args) | [EFT_tok "annot_val"; EFT_string txt] -> if sg.sig_args = [] then raise Parsing.Parse_error; - EF_annot_val(intern_string txt, List.hd sg.sig_args) + EF_annot_val(coqstring_of_camlstring txt, List.hd sg.sig_args) | [EFT_tok "inline_asm"; EFT_string txt] -> - EF_inline_asm(intern_string txt, sg, []) + EF_inline_asm(coqstring_of_camlstring txt, sg, []) | _ -> raise Parsing.Parse_error @@ -473,7 +473,7 @@ proc: fn_stackspace = $8; fn_body = $10 })) } | EXTERN STRINGLIT COLON signature - { (intern_string $2, Gfun(External(EF_external(intern_string $2,$4)))) } + { (intern_string $2, Gfun(External(EF_external(coqstring_of_camlstring $2,$4)))) } | EXTERN STRINGLIT EQUAL eftoks COLON signature { (intern_string $2, Gfun(External(mkef $6 $4))) } ; diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index 970386a9..105b284c 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -12,6 +12,7 @@ (** Instruction selection for 64-bit integer operations *) +Require String. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -24,26 +25,24 @@ Local Open Scope cminorsel_scope. Local Open Scope string_scope. (** Some operations on 64-bit integers are transformed into calls to - 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". + 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_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 *) +}. Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. @@ -55,6 +54,8 @@ 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). @@ -121,28 +122,28 @@ Definition longofintu (e: expr) := Definition negl (e: expr) := match is_longconst e with | Some n => longconst (Int64.neg n) - | None => Ebuiltin (EF_builtin i64_neg sig_l_l) (e ::: Enil) + | None => Ebuiltin (EF_builtin "__builtin_negl" 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 i64_dtos sig_f_l (arg ::: Enil). + Eexternal hf.(i64_dtos) sig_f_l (arg ::: Enil). Definition longuoffloat (arg: expr) := - Eexternal i64_dtou sig_f_l (arg ::: Enil). + Eexternal hf.(i64_dtou) sig_f_l (arg ::: Enil). Definition floatoflong (arg: expr) := - Eexternal i64_stod sig_l_f (arg ::: Enil). + Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil). Definition floatoflongu (arg: expr) := - Eexternal i64_utod sig_l_f (arg ::: Enil). + Eexternal hf.(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 i64_stof sig_l_s (arg ::: Enil). + Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil). Definition singleoflongu (arg: expr) := - Eexternal i64_utof sig_l_s (arg ::: Enil). + Eexternal hf.(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)). @@ -163,7 +164,7 @@ Definition shllimm (e1: expr) (n: int) := makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize)) (Eop (Ointconst Int.zero) Enil) else - Eexternal i64_shl sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal hf.(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 @@ -175,7 +176,7 @@ Definition shrluimm (e1: expr) (n: int) := makelong (Eop (Ointconst Int.zero) Enil) (shruimm (highlong e1) (Int.sub n Int.iwordsize)) else - Eexternal i64_shr sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal hf.(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 @@ -188,7 +189,7 @@ Definition shrlimm (e1: expr) (n: int) := (makelong (shrimm (Eletvar 0) (Int.repr 31)) (shrimm (Eletvar 0) (Int.sub n Int.iwordsize))) else - Eexternal i64_sar sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). + Eexternal hf.(i64_sar) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil). Definition is_intconst (e: expr) := match e with @@ -199,23 +200,23 @@ Definition is_intconst (e: expr) := Definition shll (e1 e2: expr) := match is_intconst e2 with | Some n => shllimm e1 n - | None => Eexternal i64_shl sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal hf.(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 i64_shr sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal hf.(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 i64_sar sig_li_l (e1 ::: e2 ::: Enil) + | None => Eexternal hf.(i64_sar) sig_li_l (e1 ::: e2 ::: Enil) end. Definition addl (e1 e2: expr) := - let default := Ebuiltin (EF_builtin i64_add sig_ll_l) (e1 ::: e2 ::: Enil) in + let default := Ebuiltin (EF_builtin "__builtin_addl" 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 @@ -224,7 +225,7 @@ Definition addl (e1 e2: expr) := end. Definition subl (e1 e2: expr) := - let default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (e1 ::: e2 ::: Enil) in + let default := Ebuiltin (EF_builtin "__builtin_subl" 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 @@ -234,7 +235,7 @@ Definition subl (e1 e2: expr) := Definition mull_base (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Elet (Ebuiltin (EF_builtin i64_mul sig_ii_l) (l1 ::: l2 ::: Enil)) + Elet (Ebuiltin (EF_builtin "__builtin_mull" sig_ii_l) (l1 ::: l2 ::: Enil)) (makelong (add (add (Eop Ohighlong (Eletvar O ::: Enil)) (mul (lift l1) (lift h2))) @@ -263,11 +264,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 i64_sdiv Int64.divs. -Definition modl := binop_long i64_smod Int64.mods. +Definition divl e1 e2 := binop_long hf.(i64_sdiv) Int64.divs e1 e2. +Definition modl e1 e2 := binop_long hf.(i64_smod) Int64.mods e1 e2. Definition divlu (e1 e2: expr) := - let default := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil) in + let default := Eexternal hf.(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 => @@ -279,7 +280,7 @@ Definition divlu (e1 e2: expr) := end. Definition modlu (e1 e2: expr) := - let default := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil) in + let default := Eexternal hf.(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 => @@ -359,45 +360,3 @@ Definition cmpl (c: comparison) (e1 e2: expr) := end. End SELECT. - -(** Checking that the helper functions are available. *) - -Require Import Errors. -Require Import Globalenvs. -Local Open Scope error_monad_scope. - -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 40c11dd8..cdfb1107 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -12,6 +12,7 @@ (** Correctness of instruction selection for integer division *) +Require Import String. Require Import Coqlib. Require Import AST. Require Import Errors. @@ -29,81 +30,96 @@ Require Import SelectOpproof. Require Import SelectLong. Open Local Scope cminorsel_scope. +Open Local Scope string_scope. (** * Axiomatization of the helper functions *) -Definition external_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := +Definition external_implements (name: string) (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. + external_call (EF_external name sg) ge vargs m E0 vres m. -Definition builtin_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := +Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := forall F V (ge: Genv.t F V) m, - external_call (EF_builtin id sg) ge vargs m E0 vres m. + external_call (EF_builtin name 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 + (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 "__builtin_negl" sig_l_l (x::nil) (Val.negl x)) + /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y)) + /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y)) + /\ (forall x y, builtin_implements "__builtin_mull" 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) (id: ident) (name: string) (sg: signature) : Prop := + exists b, Genv.find_symbol ge id = Some b /\ Genv.find_funct_ptr ge b = Some (External (EF_external name sg)). +Definition helper_functions_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (hf: helper_functions) : Prop := + helper_declared ge hf.(i64_dtos) "__i64_dtos" sig_f_l + /\ helper_declared ge hf.(i64_dtou) "__i64_dtou" sig_f_l + /\ helper_declared ge hf.(i64_stod) "__i64_stod" sig_l_f + /\ helper_declared ge hf.(i64_utod) "__i64_utod" sig_l_f + /\ helper_declared ge hf.(i64_stof) "__i64_stof" sig_l_s + /\ helper_declared ge hf.(i64_utof) "__i64_utof" sig_l_s + /\ helper_declared ge hf.(i64_sdiv) "__i64_sdiv" sig_ll_l + /\ helper_declared ge hf.(i64_udiv) "__i64_udiv" sig_ll_l + /\ helper_declared ge hf.(i64_smod) "__i64_smod" sig_ll_l + /\ helper_declared ge hf.(i64_umod) "__i64_umod" sig_ll_l + /\ helper_declared ge hf.(i64_shl) "__i64_shl" sig_li_l + /\ helper_declared ge hf.(i64_shr) "__i64_shr" sig_li_l + /\ helper_declared ge hf.(i64_sar) "__i64_sar" sig_li_l. + (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. Variable ge: genv. -Hypothesis HELPERS: - forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared ge hf. Variable sp: val. Variable e: env. Variable m: mem. -Ltac UseHelper := - generalize i64_helpers_correct; intros; - repeat (eauto; match goal with | [ H: _ /\ _ |- _ ] => destruct H end). +Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto. +Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: - forall le id sg args vargs vres, + forall le id name sg args vargs vres, eval_exprlist ge sp e m le args vargs -> - In (id, sg) i64_helpers -> - external_implements id sg vargs vres -> + helper_declared ge id name sg -> + external_implements name sg vargs vres -> eval_expr ge sp e m le (Eexternal id sg args) vres. Proof. - intros. exploit HELPERS; eauto. intros (b & A & B). econstructor; eauto. + intros. destruct H0 as (b & P & Q). econstructor; eauto. Qed. Corollary eval_helper_1: - forall le id sg arg1 varg1 vres, + forall le id name sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> - In (id, sg) i64_helpers -> - external_implements id sg (varg1::nil) vres -> + helper_declared ge id name sg -> + external_implements name 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. Qed. Corollary eval_helper_2: - forall le id sg arg1 arg2 varg1 varg2 vres, + forall le id name sg arg1 arg2 varg1 varg2 vres, eval_expr ge sp e m le arg1 varg1 -> eval_expr ge sp e m le arg2 varg2 -> - In (id, sg) i64_helpers -> - external_implements id sg (varg1::varg2::nil) vres -> + helper_declared ge id name sg -> + external_implements name 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. @@ -394,51 +410,47 @@ 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longoffloat hf a) v /\ Val.lessdef y v. Proof. intros; unfold longoffloat. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longuoffloat hf a) v /\ Val.lessdef y v. Proof. intros; unfold longuoffloat. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (floatoflong hf a) v /\ Val.lessdef y v. Proof. intros; unfold floatoflong. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (floatoflongu hf a) v /\ Val.lessdef y v. Proof. intros; unfold floatoflongu. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longofsingle hf 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. @@ -452,7 +464,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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longuofsingle hf 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. @@ -466,22 +478,20 @@ 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (singleoflong hf a) v /\ Val.lessdef y v. Proof. intros; unfold singleoflong. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. 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 a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (singleoflongu hf a) v /\ Val.lessdef y v. Proof. intros; unfold singleoflongu. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_andl: binary_constructor_sound andl Val.andl. @@ -578,7 +588,7 @@ Qed. Lemma eval_shllimm: forall n, - unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)). + unary_constructor_sound (fun e => shllimm hf e n) (fun v => Val.shll v (Vint n)). Proof. unfold shllimm; red; intros. apply eval_shift_imm; intros. @@ -608,11 +618,10 @@ 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. - simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. Qed. -Theorem eval_shll: binary_constructor_sound shll Val.shll. +Theorem eval_shll: binary_constructor_sound (shll hf) Val.shll. Proof. unfold shll; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -620,12 +629,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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Lemma eval_shrluimm: forall n, - unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)). + unary_constructor_sound (fun e => shrluimm hf e n) (fun v => Val.shrlu v (Vint n)). Proof. unfold shrluimm; red; intros. apply eval_shift_imm; intros. + (* n = 0 *) @@ -654,10 +663,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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. Qed. -Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu. +Theorem eval_shrlu: binary_constructor_sound (shrlu hf) Val.shrlu. Proof. unfold shrlu; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -665,12 +674,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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Lemma eval_shrlimm: forall n, - unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)). + unary_constructor_sound (fun e => shrlimm hf e n) (fun v => Val.shrl v (Vint n)). Proof. unfold shrlimm; red; intros. apply eval_shift_imm; intros. + (* n = 0 *) @@ -703,10 +712,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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. Qed. -Theorem eval_shrl: binary_constructor_sound shrl Val.shrl. +Theorem eval_shrl: binary_constructor_sound (shrl hf) Val.shrl. Proof. unfold shrl; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -714,17 +723,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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_addl: binary_constructor_sound addl Val.addl. Proof. unfold addl; red; intros. - set (default := Ebuiltin (EF_builtin i64_add sig_ll_l) (a ::: b ::: Enil)). + set (default := Ebuiltin (EF_builtin "__builtin_addl" 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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -743,11 +752,11 @@ Qed. Theorem eval_subl: binary_constructor_sound subl Val.subl. Proof. unfold subl; red; intros. - set (default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (a ::: b ::: Enil)). + set (default := Ebuiltin (EF_builtin "__builtin_subl" 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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -778,7 +787,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. simpl; auto 20. UseHelper. + EvalOp. eapply eval_builtin_2; eauto. 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 +795,7 @@ Proof. Qed. Lemma eval_mullimm: - forall n, unary_constructor_sound (fun a => mullimm a n) (fun v => Val.mull v (Vlong n)). + forall n, unary_constructor_sound (fun a => mullimm hf 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 +825,7 @@ Proof. apply eval_mull_base; auto. apply eval_longconst. Qed. -Theorem eval_mull: binary_constructor_sound mull Val.mull. +Theorem eval_mull: binary_constructor_sound (mull hf) Val.mull. Proof. unfold mull; red; intros. destruct (is_longconst a) as [p|] eqn:LC1; @@ -834,10 +843,10 @@ Proof. Qed. Lemma eval_binop_long: - forall id sem le a b x y z, + forall id name sem le a b x y z, (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) -> - external_implements id sig_ll_l (x::y::nil) z -> - In (id, sig_ll_l) i64_helpers -> + helper_declared ge id name sig_ll_l -> + external_implements name sig_ll_l (x::y::nil) z -> 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. @@ -857,15 +866,14 @@ 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 a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divl hf a b) v /\ Val.lessdef z v. Proof. intros. eapply eval_binop_long; eauto. intros; subst; simpl in H1. destruct (Int64.eq q Int64.zero || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. auto. - UseHelper. - simpl; auto 20. + DeclHelper. UseHelper. Qed. Theorem eval_modl: @@ -873,15 +881,14 @@ 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 a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modl hf a b) v /\ Val.lessdef z v. Proof. intros. eapply eval_binop_long; eauto. intros; subst; simpl in H1. destruct (Int64.eq q Int64.zero || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. auto. - UseHelper. - simpl; auto 20. + DeclHelper. UseHelper. Qed. Theorem eval_divlu: @@ -889,14 +896,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 a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divlu hf a b) v /\ Val.lessdef z v. Proof. intros. unfold divlu. - set (default := Eexternal i64_udiv sig_ll_l (a ::: b ::: Enil)). + set (default := Eexternal hf.(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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -932,14 +939,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 a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modlu hf a b) v /\ Val.lessdef z v. Proof. intros. unfold modlu. - set (default := Eexternal i64_umod sig_ll_l (a ::: b ::: Enil)). + set (default := Eexternal hf.(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. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. 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 2e631ad2..dea8a008 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -22,7 +22,9 @@ Instruction selection proceeds by bottom-up rewriting over expressions. The source language is Cminor and the target language is CminorSel. *) +Require String. Require Import Coqlib. +Require Import Maps. Require Import AST. Require Import Errors. Require Import Integers. @@ -67,6 +69,8 @@ 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 @@ -104,14 +108,14 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := | Cminor.Ointoflong => intoflong arg | Cminor.Olongofint => longofint arg | Cminor.Olongofintu => longofintu 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 + | 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 end. Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := @@ -139,17 +143,17 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := | Cminor.Odivfs => divfs 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.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.Oandl => andl arg1 arg2 | Cminor.Oorl => orl arg1 arg2 | Cminor.Oxorl => xorl arg1 arg2 - | Cminor.Oshll => shll arg1 arg2 - | Cminor.Oshrl => shrl arg1 arg2 - | Cminor.Oshrlu => shrlu arg1 arg2 + | Cminor.Oshll => shll hf arg1 arg2 + | Cminor.Oshrl => shrl hf arg1 arg2 + | Cminor.Oshrlu => shrlu hf arg1 arg2 | Cminor.Ocmp c => comp c arg1 arg2 | Cminor.Ocmpu c => compu c arg1 arg2 | Cminor.Ocmpf c => compf c arg1 arg2 @@ -324,8 +328,6 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := | Cminor.Sgoto lbl => OK (Sgoto lbl) end. -End SELECTION. - (** Conversion of functions. *) Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function := @@ -340,10 +342,76 @@ Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function := Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : res fundef := transf_partial_fundef (sel_function ge) f. +End SELECTION. + +(** Setting up the helper functions. *) + +Definition globdef := AST.globdef Cminor.fundef unit. + +(** We build a partial mapping from global identifiers to their definitions, + restricting ourselves to the globals we are interested in, namely + the external function declarations whose name starts with "__i64_". + This ensures that the mapping remains small and that [lookup_helper] + below is efficient. *) + +Definition globdef_of_interest (gd: globdef) : bool := + match gd with + | Gfun (External (EF_external name sg)) => String.prefix "__i64_" name + | _ => false + end. + +Definition record_globdef (globs: PTree.t globdef) (id_gd: ident * globdef) := + let (id, gd) := id_gd in + if globdef_of_interest gd + then PTree.set id gd globs + else PTree.remove id globs. + +Definition record_globdefs (p: Cminor.program) : PTree.t globdef := + List.fold_left record_globdef p.(prog_defs) (PTree.empty _). + +Definition lookup_helper_aux + (name: String.string) (sg: signature) (res: option ident) + (id: ident) (gd: globdef) := + match gd with + | Gfun (External (EF_external name' sg')) => + if String.string_dec name name' && signature_eq sg sg' + then Some id + else res + | _ => res + end. + +Definition lookup_helper (globs: PTree.t globdef) + (name: String.string) (sg: signature) : res ident := + match PTree.fold (lookup_helper_aux name sg) globs None with + | Some id => OK id + | None => Error (MSG name :: MSG ": missing or incorrect declaration" :: nil) + end. + +Local Open Scope string_scope. + +Definition get_helpers (p: Cminor.program) : res helper_functions := + let globs := record_globdefs p in + do i64_dtos <- lookup_helper globs "__i64_dtos" sig_f_l ; + do i64_dtou <- lookup_helper globs "__i64_dtou" sig_f_l ; + do i64_stod <- lookup_helper globs "__i64_stod" sig_l_f ; + do i64_utod <- lookup_helper globs "__i64_utod" sig_l_f ; + do i64_stof <- lookup_helper globs "__i64_stof" sig_l_s ; + do i64_utof <- lookup_helper globs "__i64_utof" sig_l_s ; + do i64_sdiv <- lookup_helper globs "__i64_sdiv" sig_ll_l ; + do i64_udiv <- lookup_helper globs "__i64_udiv" sig_ll_l ; + do i64_smod <- lookup_helper globs "__i64_smod" sig_ll_l ; + do i64_umod <- lookup_helper globs "__i64_umod" sig_ll_l ; + do i64_shl <- lookup_helper globs "__i64_shl" sig_li_l ; + do i64_shr <- lookup_helper globs "__i64_shr" sig_li_l ; + do i64_sar <- lookup_helper globs "__i64_sar" sig_li_l ; + OK (mk_helper_functions + i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof + i64_sdiv i64_udiv i64_smod i64_umod + i64_shl i64_shr i64_sar). + (** Conversion of programs. *) Definition sel_program (p: Cminor.program) : res program := - let ge := Genv.globalenv p in - do x <- check_helpers ge; - transform_partial_program (sel_fundef ge) p. + do hf <- get_helpers p; + transform_partial_program (sel_fundef hf (Genv.globalenv p)) p. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 1d2f2b3a..8ea4c56e 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. -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. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared ge hf. +Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf 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 ge f = OK tf. + exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf 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 ge f = OK tf. + exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf 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 ge f = OK tf -> funsig tf = Cminor.funsig f. + forall f tf, sel_fundef hf 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 ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. + forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. Proof. intros. monadInv H. auto. Qed. @@ -100,17 +100,17 @@ Proof. Qed. Lemma helper_declared_preserved: - forall id sg, helper_declared ge id sg -> helper_declared tge id sg. + forall id name sg, helper_declared ge id name sg -> helper_declared tge id name sg. Proof. - intros id sg (b & A & B). + intros id name sg (b & A & B). exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q. exists b; split; auto. rewrite symbols_preserved. auto. Qed. -Let HELPERS': - forall name sg, In (name, sg) i64_helpers -> helper_declared tge name sg. +Let HELPERS': helper_functions_declared tge hf. Proof. - intros. apply helper_declared_preserved. auto. + red in HELPERS; decompose [Logic.and] HELPERS. + red. auto 20 using helper_declared_preserved. Qed. Section CMCONSTR. @@ -172,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 op a1) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_unop hf op a1) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_cast8unsigned; auto. @@ -215,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 op a1 a2) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e m le (sel_binop hf op a1 a2) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_add; auto. @@ -552,7 +552,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 a) v' /\ Val.lessdef v v'. + exists v', eval_expr tge sp e' m' le (sel_expr hf a) v' /\ Val.lessdef v v'. Proof. induction 1; intros; simpl. (* Evar *) @@ -589,7 +589,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 a) v' /\ Val.lessdef_list v v'. + exists v', eval_exprlist tge sp e' m' le (sel_exprlist hf a) v' /\ Val.lessdef_list v v'. Proof. induction 1; intros; simpl. exists (@nil val); split; auto. constructor. @@ -603,13 +603,13 @@ Lemma sel_builtin_arg_correct: env_lessdef e e' -> Mem.extends m m' -> Cminor.eval_expr ge sp e m a v -> exists v', - CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg a c) v' + CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg hf a c) v' /\ Val.lessdef v v'. Proof. intros. unfold sel_builtin_arg. exploit sel_expr_correct; eauto. intros (v1 & A & B). exists v1; split; auto. - destruct (builtin_arg_ok (builtin_arg (sel_expr a)) c). + destruct (builtin_arg_ok (builtin_arg (sel_expr hf a)) c). apply eval_builtin_arg; eauto. constructor; auto. Qed. @@ -622,7 +622,7 @@ Lemma sel_builtin_args_correct: forall cl, exists vl', list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') - (sel_builtin_args al cl) + (sel_builtin_args hf al cl) vl' /\ Val.lessdef_list vl vl'. Proof. @@ -647,21 +647,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 ge s = OK s' -> + sel_stmt hf 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 ge f = OK f' -> + sel_function hf 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 ge f = OK f') - (TS: sel_stmt ge s = OK s') + (TF: sel_function hf ge f = OK f') + (TS: sel_stmt hf ge s = OK s') (MC: match_cont k k') (LD: env_lessdef e e') (ME: Mem.extends m m'), @@ -669,7 +669,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 ge f = OK f') + (TF: sel_fundef hf ge f = OK f') (MC: match_cont k k') (LD: Val.lessdef_list args args') (ME: Mem.extends m m'), @@ -684,7 +684,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 ge f = OK f') + (TF: sel_function hf ge f = OK f') (MC: match_cont k k') (LDA: Val.lessdef_list args args') (LDE: env_lessdef e e') @@ -694,7 +694,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 (sel_builtin_res 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 ge f = OK f') + (TF: sel_function hf ge f = OK f') (MC: match_cont k k') (LDV: Val.lessdef v v') (LDE: env_lessdef e e') @@ -712,16 +712,16 @@ Qed. Remark find_label_commut: forall lbl s k s' k', match_cont k k' -> - sel_stmt ge s = OK s' -> + sel_stmt hf 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 ge s1 = OK s1' /\ match_cont k1 k1' + | Some(s1, k1), Some(s1', k1') => sel_stmt hf 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 e)); simpl; auto. + unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto. (* call *) destruct (classify_call ge e); simpl; auto. (* tailcall *) @@ -886,7 +886,7 @@ Proof. - (* Slabel *) left; econstructor; split. constructor. constructor; auto. - (* Sgoto *) - assert (sel_stmt ge (Cminor.fn_body f) = OK (fn_body f')). + assert (sel_stmt hf 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. @@ -954,39 +954,97 @@ Qed. End PRESERVATION. -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. +(** Processing of helper functions *) + +Lemma record_globdefs_sound: + forall p id fd, + (record_globdefs p)!id = Some (Gfun fd) -> + exists b, Genv.find_symbol (Genv.globalenv p) id = Some b + /\ Genv.find_funct_ptr (Genv.globalenv p) b = Some fd. +Proof. + intros until fd. + set (P := fun (m: PTree.t globdef) (ge: Genv.t Cminor.fundef unit) => + m!id = Some (Gfun fd) -> + exists b, Genv.find_symbol ge id = Some b + /\ Genv.find_funct_ptr ge b = Some fd). + assert (REC: forall gl m ge, + P m ge -> + P (fold_left record_globdef gl m) (Genv.add_globals ge gl)). + { + induction gl; simpl; intros. + - auto. + - apply IHgl. red. destruct a as [id1 gd1]; simpl; intros. + unfold Genv.find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id1). + + subst id1. exists (Genv.genv_next ge); split; auto. + replace gd1 with (@Gfun Cminor.fundef unit fd). + unfold Genv.find_funct_ptr; simpl. apply PTree.gss. + destruct (globdef_of_interest gd1). + rewrite PTree.gss in H0; congruence. + rewrite PTree.grs in H0; congruence. + + assert (m!id = Some (Gfun fd)). + { destruct (globdef_of_interest gd1). + rewrite PTree.gso in H0; auto. + rewrite PTree.gro in H0; auto. } + exploit H; eauto. intros (b & A & B). + exists b; split; auto. unfold Genv.find_funct_ptr; simpl. + destruct gd1; auto. rewrite PTree.gso; auto. + apply Plt_ne. eapply Genv.genv_symb_range; eauto. + } + eapply REC. red; intros. rewrite PTree.gempty in H; discriminate. +Qed. + +Lemma lookup_helper_correct_1: + forall globs name sg id, + lookup_helper globs name sg = OK id -> + globs!id = Some (Gfun (External (EF_external name sg))). +Proof. + intros. + set (P := fun (m: PTree.t globdef) res => res = Some id -> m!id = Some(Gfun(External (EF_external name sg)))). + assert (P globs (PTree.fold (lookup_helper_aux name sg) globs None)). + { apply PTree_Properties.fold_rec; red; intros. + - rewrite <- H0. apply H1; auto. + - discriminate. + - assert (EITHER: k = id /\ v = Gfun (External (EF_external name sg)) + \/ a = Some id). + { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto. + destruct (String.string_dec name name0); auto. + destruct (signature_eq sg sg0); auto. + inversion H3. left; split; auto. repeat f_equal; auto. } + destruct EITHER as [[X Y] | X]. + subst k v. apply PTree.gss. + apply H2 in X. rewrite PTree.gso by congruence. auto. + } + red in H0. unfold lookup_helper in H. + destruct (PTree.fold (lookup_helper_aux name sg) globs None); inv H. 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. +Lemma lookup_helper_correct: + forall p name sg id, + lookup_helper (record_globdefs p) name sg = OK id -> + helper_declared (Genv.globalenv p) id 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. + intros. apply lookup_helper_correct_1 in H. apply record_globdefs_sound in H. auto. Qed. +Theorem get_helpers_correct: + forall p hf, + get_helpers p = OK hf -> helper_functions_declared (Genv.globalenv p) hf. +Proof. + intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct. +Qed. + +(** All together *) + 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. 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). + intros. unfold sel_program in H. + destruct (get_helpers prog) as [hf|] eqn:G; simpl in H; try discriminate. + apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). eapply public_preserved; eauto. apply sel_initial_states; auto. apply sel_final_states; auto. - apply sel_step_correct; auto. eapply check_helpers_correct; eauto. + apply sel_step_correct; auto. eapply get_helpers_correct; eauto. Qed. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bd281374..9b31dfdb 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -769,7 +769,7 @@ let rec convertExpr env e = | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypArgs env [] args1 in Ebuiltin( - EF_annot(intern_string txt, typlist_of_typelist targs1), + EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; @@ -781,7 +781,7 @@ let rec convertExpr env e = | [ {edesc = C.EConst(CStr txt)}; arg ] -> let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in - Ebuiltin(EF_annot_val(intern_string txt, typ_of_type targ), + Ebuiltin(EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> @@ -822,7 +822,7 @@ let rec convertExpr env e = let sg = signature_of_type targs tres {cc_vararg = true; cc_unproto = false; cc_structret = false} in - Ebuiltin(EF_external(intern_string "printf", sg), + Ebuiltin(EF_external(coqstring_of_camlstring "printf", sg), targs, convertExprList env args, tres) | C.ECall(fn, args) -> @@ -877,7 +877,7 @@ let convertAsm loc env txt outputs inputs clobber = let e = let tinputs = convertTypArgs env [] inputs' in let toutput = convertTyp env ty_res in - Ebuiltin(EF_inline_asm(intern_string txt', + Ebuiltin(EF_inline_asm(coqstring_of_camlstring txt', signature_of_type tinputs toutput cc_default, clobber'), tinputs, @@ -1085,14 +1085,15 @@ let convertFundecl env (sto, id, ty, optinit) = | Tfunction(args, res, cconv) -> (args, res, cconv) | _ -> assert false in let id' = intern_string id.name in + let id'' = coqstring_of_camlstring id.name in let sg = signature_of_type args res cconv in let ef = if id.name = "malloc" then EF_malloc else if id.name = "free" then EF_free else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.functions - then EF_builtin(id', sg) - else EF_external(id', sg) in + then EF_builtin(id'', sg) + else EF_external(id'', sg) in (id', Gfun(External(ef, args, res, cconv))) (** Initializers *) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 16d5823b..938454c5 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -391,7 +391,7 @@ Qed. (** External calls *) Variable do_external_function: - ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). + string -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). Hypothesis do_external_function_sound: forall id sg ge vargs m t vres m' w w', @@ -405,7 +405,7 @@ Hypothesis do_external_function_complete: do_external_function id sg ge w vargs m = Some(w', t, vres, m'). Variable do_inline_assembly: - ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). + string -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). Hypothesis do_inline_assembly_sound: forall txt sg ge vargs m t vres m' w w', @@ -513,12 +513,12 @@ Definition do_ef_memcpy (sz al: Z) | _ => None end. -Definition do_ef_annot (text: ident) (targs: list typ) +Definition do_ef_annot (text: string) (targs: list typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := do args <- list_eventval_of_val vargs targs; Some(w, Event_annot text args :: E0, Vundef, m). -Definition do_ef_annot_val (text: ident) (targ: typ) +Definition do_ef_annot_val (text: string) (targ: typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match vargs with | varg :: nil => diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index d890c820..ce912a8c 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -258,12 +258,12 @@ let rec expr p (prec, e) = exprlist (true, args) | Ebuiltin(EF_annot(txt, _), _, args, _) -> fprintf p "__builtin_annot@[<hov 1>(%S%a)@]" - (extern_atom txt) exprlist (false, args) + (camlstring_of_coqstring txt) exprlist (false, args) | Ebuiltin(EF_annot_val(txt, _), _, args, _) -> fprintf p "__builtin_annot_val@[<hov 1>(%S%a)@]" - (extern_atom txt) exprlist (false, args) + (camlstring_of_coqstring txt) exprlist (false, args) | Ebuiltin(EF_external(id, sg), _, args, _) -> - fprintf p "%s@[<hov 1>(%a)@]" (extern_atom id) exprlist (true, args) + fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) -> extended_asm p txt None args clob | Ebuiltin(_, _, args, _) -> @@ -282,7 +282,7 @@ and exprlist p (first, rl) = exprlist p (false, rl) and extended_asm p txt res args clob = - fprintf p "asm volatile (@[<hv 0>%S" (extern_atom txt); + fprintf p "asm volatile (@[<hv 0>%S" (camlstring_of_coqstring txt); fprintf p "@ :"; begin match res with | None -> () diff --git a/common/AST.v b/common/AST.v index 4e02b3d4..c62b0091 100644 --- a/common/AST.v +++ b/common/AST.v @@ -16,8 +16,8 @@ (** This file defines a number of data types and operations used in the abstract syntax trees of many of the intermediate languages. *) +Require Import String. Require Import Coqlib. -Require String. Require Import Errors. Require Import Integers. Require Import Floats. @@ -33,8 +33,6 @@ Definition ident := positive. Definition ident_eq := peq. -Parameter ident_of_string : String.string -> ident. - (** The intermediate languages are weakly typed, using the following types: *) Inductive typ : Type := @@ -305,8 +303,7 @@ End TRANSF_PROGRAM_IDENT. for the case the identifier of the function is passed as additional argument *) -Open Local Scope error_monad_scope. -Open Local Scope string_scope. +Local Open Scope error_monad_scope. Section TRANSF_PROGRAM_GEN. @@ -760,10 +757,10 @@ Qed. and associated operations. *) Inductive external_function : Type := - | EF_external (name: ident) (sg: signature) + | EF_external (name: string) (sg: signature) (** A system call or library function. Produces an event in the trace. *) - | EF_builtin (name: ident) (sg: signature) + | EF_builtin (name: string) (sg: signature) (** A compiler built-in function. Behaves like an external, but can be inlined by the compiler. *) | EF_vload (chunk: memory_chunk) @@ -786,15 +783,15 @@ Inductive external_function : Type := Produces no observable event. *) | EF_memcpy (sz: Z) (al: Z) (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *) - | EF_annot (text: ident) (targs: list typ) + | EF_annot (text: string) (targs: list typ) (** A programmer-supplied annotation. Takes zero, one or several arguments, produces an event carrying the text and the values of these arguments, and returns no value. *) - | EF_annot_val (text: ident) (targ: typ) + | EF_annot_val (text: string) (targ: typ) (** Another form of annotation that takes one argument, produces an event carrying the text and the value of this argument, and returns the value of the argument. *) - | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string) + | EF_inline_asm (text: string) (sg: signature) (clobbers: list string) (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic @@ -852,9 +849,8 @@ Definition ef_reloads (ef: external_function) : bool := Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}. Proof. - generalize ident_eq signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. + generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. decide equality. - apply list_eq_dec. apply String.string_dec. Defined. Global Opaque external_function_eq. diff --git a/common/Determinism.v b/common/Determinism.v index 7ea19663..2445398c 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -13,6 +13,7 @@ (** Characterization and properties of deterministic external worlds and deterministic semantics *) +Require Import String. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -37,11 +38,11 @@ Require Import Behaviors. the world to [w]. *) CoInductive world: Type := - World (io: ident -> list eventval -> option (eventval * world)) + World (io: string -> list eventval -> option (eventval * world)) (vload: memory_chunk -> ident -> int -> option (eventval * world)) (vstore: memory_chunk -> ident -> int -> eventval -> option world). -Definition nextworld_io (w: world) (evname: ident) (evargs: list eventval) : +Definition nextworld_io (w: world) (evname: string) (evargs: list eventval) : option (eventval * world) := match w with World io vl vs => io evname evargs end. diff --git a/common/Events.v b/common/Events.v index 7cd9155e..dc38b344 100644 --- a/common/Events.v +++ b/common/Events.v @@ -15,6 +15,7 @@ (** Observable events, execution traces, and semantics of external calls. *) +Require Import String. Require Import Coqlib. Require Intv. Require Import AST. @@ -61,10 +62,10 @@ Inductive eventval: Type := | EVptr_global: ident -> int -> eventval. Inductive event: Type := - | Event_syscall: ident -> list eventval -> eventval -> event + | Event_syscall: string -> list eventval -> eventval -> event | Event_vload: memory_chunk -> ident -> int -> eventval -> event | Event_vstore: memory_chunk -> ident -> int -> eventval -> event - | Event_annot: ident -> list eventval -> event. + | Event_annot: string -> list eventval -> event. (** The dynamic semantics for programs collect traces of events. Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *) @@ -1219,7 +1220,7 @@ Qed. (** ** Semantics of annotations. *) -Inductive extcall_annot_sem (text: ident) (targs: list typ) (ge: Senv.t): +Inductive extcall_annot_sem (text: string) (targs: list typ) (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := | extcall_annot_sem_intro: forall vargs m args, eventval_list_match ge args targs vargs -> @@ -1264,7 +1265,7 @@ Proof. split. constructor. auto. Qed. -Inductive extcall_annot_val_sem (text: ident) (targ: typ) (ge: Senv.t): +Inductive extcall_annot_val_sem (text: string) (targ: typ) (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := | extcall_annot_val_sem_intro: forall varg m arg, eventval_match ge arg targ varg -> @@ -1354,14 +1355,14 @@ Qed. we do not define their semantics, but only assume that it satisfies [extcall_properties]. *) -Parameter external_functions_sem: ident -> signature -> extcall_sem. +Parameter external_functions_sem: String.string -> signature -> extcall_sem. Axiom external_functions_properties: forall id sg, extcall_properties (external_functions_sem id sg) sg. (** We treat inline assembly similarly. *) -Parameter inline_assembly_sem: ident -> signature -> extcall_sem. +Parameter inline_assembly_sem: String.string -> signature -> extcall_sem. Axiom inline_assembly_properties: forall id sg, extcall_properties (inline_assembly_sem id sg) sg. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index aea8ff0f..67b5eb9d 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -37,17 +37,17 @@ let name_of_chunk = function | Many64 -> "any64" let name_of_external = function - | EF_external(name, sg) -> sprintf "extern %S" (extern_atom name) - | EF_builtin(name, sg) -> sprintf "builtin %S" (extern_atom name) + | EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name) + | EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name) | EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk) | EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk) | EF_malloc -> "malloc" | EF_free -> "free" | EF_memcpy(sz, al) -> sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string al) - | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text) - | EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text) - | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (extern_atom text) + | EF_annot(text, targs) -> sprintf "annot %S" (camlstring_of_coqstring text) + | EF_annot_val(text, targ) -> sprintf "annot_val %S" (camlstring_of_coqstring text) + | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (camlstring_of_coqstring text) | EF_debug(kind, text, targs) -> sprintf "debug%d %S" (P.to_int kind) (extern_atom text) diff --git a/driver/Interp.ml b/driver/Interp.ml index f453af95..579b936d 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -59,7 +59,7 @@ let print_eventval_list p = function let print_event p = function | Event_syscall(id, args, res) -> fprintf p "extcall %s(%a) -> %a" - (extern_atom id) + (camlstring_of_coqstring id) print_eventval_list args print_eventval res | Event_vload(chunk, id, ofs, res) -> @@ -74,7 +74,7 @@ let print_event p = function print_eventval arg | Event_annot(text, args) -> fprintf p "annotation \"%s\" %a" - (extern_atom text) + (camlstring_of_coqstring text) print_eventval_list args (* Printing states *) @@ -387,7 +387,7 @@ let rec convert_external_args ge vl tl = | _, _ -> None let do_external_function id sg ge w args m = - match extern_atom id, args with + match camlstring_of_coqstring id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> print_string (do_printf m fmt args'); diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index a75c95a5..fda5bb55 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -15,6 +15,7 @@ (** All imports and definitions used by .v Clight files generated by clightgen *) +Require Export String. Require Export List. Require Export ZArith. Require Export Integers. diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index a1dba2d9..c1009b4f 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -112,7 +112,7 @@ let parse_c_file sourcename ifile = in (* Parsing and production of a simplified C AST *) let ast = - match fst (Parse.preprocessed_file simplifs sourcename ifile) with + match Parse.preprocessed_file simplifs sourcename ifile with | None -> exit 2 | Some p -> p in (* Save C AST if requested *) diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 82066cc9..01e9037f 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -239,13 +239,13 @@ let signatur p sg = (print_option asttype) sg.sig_res callconv sg.sig_cc -let assertions = ref ([]: (ident * typ list) list) +let assertions = ref ([]: (string * typ list) list) let external_function p = function | EF_external(name, sg) -> - fprintf p "@[<hov 2>(EF_external %a@ %a)@]" ident name signatur sg + fprintf p "@[<hov 2>(EF_external %a@ %a)@]" coqstring name signatur sg | EF_builtin(name, sg) -> - fprintf p "@[<hov 2>(EF_builtin %a@ %a)@]" ident name signatur sg + fprintf p "@[<hov 2>(EF_builtin %a@ %a)@]" coqstring name signatur sg | EF_vload chunk -> fprintf p "(EF_vload %s)" (name_of_chunk chunk) | EF_vstore chunk -> @@ -255,16 +255,16 @@ let external_function p = function | EF_memcpy(sz, al) -> fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al) | EF_annot(text, targs) -> - assertions := (text, targs) :: !assertions; - fprintf p "(EF_annot %ld%%positive %a)" (P.to_int32 text) (print_list asttype) targs + assertions := (camlstring_of_coqstring text, targs) :: !assertions; + fprintf p "(EF_annot %a %a)" coqstring text (print_list asttype) targs | EF_annot_val(text, targ) -> - assertions := (text, [targ]) :: !assertions; - fprintf p "(EF_annot_val %ld%%positive %a)" (P.to_int32 text) asttype targ + assertions := (camlstring_of_coqstring text, [targ]) :: !assertions; + fprintf p "(EF_annot_val %a %a)" coqstring text asttype targ | EF_debug(kind, text, targs) -> fprintf p "(EF_debug %ld%%positive %ld%%positive %a)" (P.to_int32 kind) (P.to_int32 text) (print_list asttype) targs | EF_inline_asm(text, sg, clob) -> - fprintf p "@[<hov 2>(EF_inline_asm %ld%%positive@ %a@ %a)@]" - (P.to_int32 text) + fprintf p "@[<hov 2>(EF_inline_asm %a@ %a@ %a)@]" + coqstring text signatur sg (print_list coqstring) clob @@ -451,14 +451,14 @@ let print_assertion p (txt, targs) = | Str.Text s -> Text s | Str.Delim "%%" -> Text "%" | Str.Delim s -> Param(int_of_string(String.sub s 1 (String.length s - 1)))) - (Str.full_split re_annot_param (extern_atom txt)) in + (Str.full_split re_annot_param txt) in let max_param = ref 0 in List.iter (function | Text _ -> () | Param n -> max_param := max n !max_param) frags; - fprintf p " | %ld%%positive, " (P.to_int32 txt); + fprintf p " | \"%s\"%%string, " txt; list_iteri (fun i targ -> fprintf p "_x%d :: " (i + 1)) targs; @@ -473,8 +473,8 @@ let print_assertion p (txt, targs) = let print_assertions p = if !assertions <> [] then begin - fprintf p "Definition assertions (id: ident) args : Prop :=@ "; - fprintf p " match id, args with@ "; + fprintf p "Definition assertions (txt: string) args : Prop :=@ "; + fprintf p " match txt, args with@ "; List.iter (print_assertion p) !assertions; fprintf p " | _, _ => False@ "; fprintf p " end.@ @ " diff --git a/extraction/extraction.v b/extraction/extraction.v index dc7522b8..aca7102d 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -42,10 +42,6 @@ Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". (* Wfsimpl *) Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. -(* AST *) -Extract Constant AST.ident_of_string => - "fun s -> Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s)". - (* Memory - work around an extraction bug. *) Extraction NoInline Memory.Mem.valid_pointer. diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index 4f02e633..99babeb4 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -368,7 +368,7 @@ let expand_instruction instr = begin match ef with | EF_builtin(name, sg) -> - expand_builtin_inline (extern_atom name) args res + expand_builtin_inline (camlstring_of_coqstring name) args res | EF_vload chunk -> expand_builtin_vload chunk args res | EF_vstore chunk -> diff --git a/ia32/Machregs.v b/ia32/Machregs.v index ace193b7..f3801900 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -129,17 +129,14 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := end end. -Definition builtin_write16_reversed := ident_of_string "__builtin_write16_reversed". -Definition builtin_write32_reversed := ident_of_string "__builtin_write32_reversed". - Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_memcpy sz al => if zle sz 32 then CX :: X7 :: nil else CX :: SI :: DI :: nil | EF_vstore (Mint8unsigned|Mint8signed) => AX :: CX :: nil - | EF_builtin id sg => - if ident_eq id builtin_write16_reversed - || ident_eq id builtin_write32_reversed + | EF_builtin name sg => + if string_dec name "__builtin_write16_reversed" + || string_dec name "__builtin_write32_reversed" then CX :: DX :: nil else nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob | _ => nil @@ -173,21 +170,17 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg | _ => (nil, None) end. -Definition builtin_negl := ident_of_string "__builtin_negl". -Definition builtin_addl := ident_of_string "__builtin_addl". -Definition builtin_subl := ident_of_string "__builtin_subl". -Definition builtin_mull := ident_of_string "__builtin_mull". - Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (option mreg) := match ef with | EF_memcpy sz al => if zle sz 32 then (Some AX :: Some DX :: nil, nil) else (Some DI :: Some SI :: nil, nil) - | EF_builtin id sg => - if ident_eq id builtin_negl then + | EF_builtin name sg => + if string_dec name "__builtin_negl" then (Some DX :: Some AX :: nil, Some DX :: Some AX :: nil) - else if ident_eq id builtin_addl || ident_eq id builtin_subl then + else if string_dec name "__builtin_addl" + || string_dec name "__builtin_subl" then (Some DX :: Some AX :: Some CX :: Some BX :: nil, Some DX :: Some AX :: nil) - else if ident_eq id builtin_mull then + else if string_dec name "__builtin_mull" then (Some AX :: Some DX :: nil, Some DX :: Some AX :: nil) else (nil, nil) diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 95de40ca..3f5e6cfe 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -656,13 +656,13 @@ module Target(System: SYSTEM):TARGET = begin match ef with | EF_annot(txt, targs) -> fprintf oc "%s annotation: " comment; - print_annot_text preg "%esp" oc (extern_atom txt) args + print_annot_text preg "%esp" oc (camlstring_of_coqstring txt) args | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg "%esp" oc (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (extern_atom txt) sg args res; + print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 00234f9b..c88f6b6d 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -620,7 +620,7 @@ let expand_instruction instr = | Pbuiltin(ef, args, res) -> begin match ef with | EF_builtin(name, sg) -> - expand_builtin_inline (extern_atom name) args res + expand_builtin_inline (camlstring_of_coqstring name) args res | EF_vload chunk -> expand_builtin_vload chunk args res | EF_vstore chunk -> diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index f94c3b64..ec721a16 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -160,15 +160,11 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg := end end. -Definition builtin_atomic_exchange := ident_of_string "__builtin_atomic_exchange". -Definition builtin_sync_and_fetch := ident_of_string "__builtin_sync_fetch_and_add". -Definition builtin_atomic_compare_exchange := ident_of_string "__builtin_atomic_compare_exchange". - Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_builtin id sg => - if ident_eq id builtin_atomic_exchange then R10::nil - else if ident_eq id builtin_atomic_compare_exchange then R10::R11::nil + if string_dec id "__builtin_atomic_exchange" then R10::nil + else if string_dec id "__builtin_atomic_compare_exchange" then R10::R11::nil else F13 :: nil | EF_vload _ => R11 :: nil | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil @@ -194,9 +190,9 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (option mreg) := match ef with | EF_builtin id sg => - if ident_eq id builtin_atomic_exchange then ((Some R3)::(Some R4)::(Some R5)::nil,nil) - else if ident_eq id builtin_sync_and_fetch then ((Some R4)::(Some R5)::nil,(Some R3)::nil) - else if ident_eq id builtin_atomic_compare_exchange then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil) + if string_dec id "__builtin_atomic_exchange" then ((Some R3)::(Some R4)::(Some R5)::nil,nil) + else if string_dec id "__builtin_sync_fetch_and_add" then ((Some R4)::(Some R5)::nil,(Some R3)::nil) + else if string_dec id "___builtin_atomic_compare_exchange" then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil) else (nil, nil) | _ => (nil, nil) end. @@ -219,23 +215,16 @@ Definition two_address_op (op: operation) : bool := (* Constraints on constant propagation for builtins *) -Definition builtin_get_spr := ident_of_string "__builtin_get_spr". -Definition builtin_set_spr := ident_of_string "__builtin_set_spr". -Definition builtin_prefetch := ident_of_string "__builtin_prefetch". -Definition builtin_dcbtls := ident_of_string "__builtin_dcbtls". -Definition builtin_icbtls := ident_of_string "__builtin_icbtls". -Definition builtin_mbar := ident_of_string "__builtin_mbar". - Definition builtin_constraints (ef: external_function) : list builtin_arg_constraint := match ef with | EF_builtin id sg => - if ident_eq id builtin_get_spr then OK_const :: nil - else if ident_eq id builtin_set_spr then OK_const :: OK_default :: nil - else if ident_eq id builtin_prefetch then OK_default :: OK_const :: OK_const :: nil - else if ident_eq id builtin_dcbtls then OK_default::OK_const::nil - else if ident_eq id builtin_icbtls then OK_default::OK_const::nil - else if ident_eq id builtin_mbar then OK_const::nil + if string_dec id "__builtin_get_spr" then OK_const :: nil + else if string_dec id "__builtin_set_spr" then OK_const :: OK_default :: nil + else if string_dec id "__builtin_prefetch" then OK_default :: OK_const :: OK_const :: nil + else if string_dec id "__builtin_dcbtls" then OK_default::OK_const::nil + else if string_dec id "__builtin_icbtls" then OK_default::OK_const::nil + else if string_dec id "__builtin_mbar" then OK_const::nil else nil | EF_vload _ => OK_addrany :: nil | EF_vstore _ => OK_addrany :: OK_default :: nil diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index e65a8934..7dbc2cf5 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -704,13 +704,13 @@ module Target (System : SYSTEM):TARGET = begin match ef with | EF_annot(txt, targs) -> fprintf oc "%s annotation: " comment; - print_annot_text preg_annot "r1" oc (extern_atom txt) args + print_annot_text preg_annot "r1" oc (camlstring_of_coqstring txt) args | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "r1" oc (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (extern_atom txt) sg args res; + print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false |