diff options
| -rw-r--r-- | backend/Constprop.v | 11 | ||||
| -rw-r--r-- | extraction/extraction.v | 4 | ||||
| -rw-r--r-- | ia32/Asm.v | 3 | ||||
| -rw-r--r-- | ia32/Asmgen.v | 3 | ||||
| -rw-r--r-- | ia32/ConstpropOp.vp | 15 | ||||
| -rw-r--r-- | ia32/Op.v | 7 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 20 | ||||
| -rw-r--r-- | ia32/SelectOp.vp | 21 | ||||
| -rw-r--r-- | ia32/SelectOpproof.v | 53 | ||||
| -rw-r--r-- | ia32/extractionMachdep.v | 6 |
10 files changed, 102 insertions, 41 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index 19e5d1a..bc6a647 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -251,17 +251,6 @@ Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident := | inr s => ros end. -Parameter generate_float_constants : unit -> bool. - -Definition const_for_result (a: approx) : option operation := - match a with - | I n => Some(Ointconst n) - | F n => if generate_float_constants tt then Some(Ofloatconst n) else None - | G symb ofs => Some(Oaddrsymbol symb ofs) - | S ofs => Some(Oaddrstack ofs) - | _ => None - end. - Definition transf_instr (gapp: global_approx) (app: D.t) (instr: instruction) := match instr with | Iop op args res s => diff --git a/extraction/extraction.v b/extraction/extraction.v index 81cf53b..02bdb60 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -15,7 +15,7 @@ Require Iteration. Require Floats. Require RTLgen. Require Inlining. -Require Constprop. +Require ConstpropOp. Require Coloring. Require Allocation. Require Compiler. @@ -59,7 +59,7 @@ Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_en (* Constprop *) Extract Constant ConstpropOp.propagate_float_constants => "fun _ -> !Clflags.option_ffloatconstprop >= 1". -Extract Constant Constprop.generate_float_constants => +Extract Constant ConstpropOp.generate_float_constants => "fun _ -> !Clflags.option_ffloatconstprop >= 2". (* Coloring *) @@ -108,6 +108,7 @@ Inductive instruction: Type := (** Moves *) | Pmov_rr (rd: ireg) (r1: ireg) (**r [mov] (32-bit int) *) | Pmov_ri (rd: ireg) (n: int) + | Pmov_raddr (rd: ireg) (id: ident) | Pmov_rm (rd: ireg) (a: addrmode) | Pmov_mr (a: addrmode) (rs: ireg) | Pmovd_fr (rd: freg) (r1: ireg) (**r [movd] (32-bit int) *) @@ -458,6 +459,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome Next (nextinstr (rs#rd <- (rs r1))) m | Pmov_ri rd n => Next (nextinstr_nf (rs#rd <- (Vint n))) m + | Pmov_raddr rd id => + Next (nextinstr_nf (rs#rd <- (symbol_offset id Int.zero))) m | Pmov_rm rd a => exec_load Mint32 m a rs rd | Pmov_mr a r1 => diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 478cdf5..5603d85 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -322,6 +322,9 @@ Definition transl_op | Ofloatconst f, nil => do r <- freg_of res; OK ((if Float.eq_dec f Float.zero then Pxorpd_f r else Pmovsd_fi r f) :: k) + | Oaddrsymbol id, nil => + do r <- ireg_of res; + OK (Pmov_raddr r id :: k) | Ocast8signed, a1 :: nil => do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsb_rr r r1 k | Ocast8unsigned, a1 :: nil => diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index a5e4e0d..0643296 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -145,6 +145,19 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) := | _, _ => Unknown end. +(** * Generation of constants *) + +Parameter generate_float_constants : unit -> bool. + +Definition const_for_result (a: approx) : option operation := + match a with + | I n => Some(Ointconst n) + | F n => if generate_float_constants tt then Some(Ofloatconst n) else None + | G symb ofs => Some(Olea (Aglobal symb ofs)) + | S ofs => Some(Olea (Ainstack ofs)) + | _ => None + end. + (** * Operator strength reduction *) (** We now define auxiliary functions for strength reduction of @@ -217,7 +230,7 @@ Nondetfunction addr_strength_reduction Definition make_addimm (n: int) (r: reg) := if Int.eq n Int.zero then (Omove, r :: nil) - else (Oaddimm n, r :: nil). + else (Olea (Aindexed n), r :: nil). Definition make_shlimm (n: int) (r: reg) := if Int.eq n Int.zero @@ -69,6 +69,7 @@ Inductive operation : Type := | Omove: operation (**r [rd = r1] *) | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) | Ofloatconst: float -> operation (**r [rd] is set to the given float constant *) + | Oaddrsymbol: ident -> operation (**r [rd] is set to the address of the symbol *) (*c Integer arithmetic: *) | Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *) | Ocast8unsigned: operation (**r [rd] is 8-bit zero extension of [r1] *) @@ -113,7 +114,6 @@ Inductive operation : Type := (** Derived operators. *) -Definition Oaddrsymbol (id: ident) (ofs: int) : operation := Olea (Aglobal id ofs). Definition Oaddrstack (ofs: int) : operation := Olea (Ainstack ofs). Definition Oaddimm (n: int) : operation := Olea (Aindexed n). @@ -193,6 +193,7 @@ Definition eval_operation | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) | Ofloatconst n, nil => Some (Vfloat n) + | Oaddrsymbol id, nil => Some (symbol_address genv id Int.zero) | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1) | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1) | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1) @@ -276,6 +277,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Omove => (nil, Tint) (* treated specially *) | Ointconst _ => (nil, Tint) | Ofloatconst _ => (nil, Tfloat) + | Oaddrsymbol _ => (nil, Tint) | Ocast8signed => (Tint :: nil, Tint) | Ocast8unsigned => (Tint :: nil, Tint) | Ocast16signed => (Tint :: nil, Tint) @@ -353,6 +355,7 @@ Proof with (try exact I). congruence. exact I. exact I. + unfold symbol_address; destruct (Genv.find_symbol genv i)... destruct v0... destruct v0... destruct v0... @@ -539,6 +542,7 @@ Definition two_address_op (op: operation) : bool := | Omove => false | Ointconst _ => false | Ofloatconst _ => false + | Oaddrsymbol _ => false | Ocast8signed => false | Ocast8unsigned => false | Ocast16signed => false @@ -691,6 +695,7 @@ Lemma eval_operation_preserved: Proof. intros. unfold eval_operation; destruct op; auto. + unfold symbol_address. rewrite agree_on_symbols. auto. apply eval_addressing_preserved. Qed. diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 80b752d..ec3cf2a 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -20,6 +20,8 @@ open AST open Memdata open Asm +module StringSet = Set.Make(String) + (* Recognition of target ABI and asm syntax *) type target = ELF | MacOS | Cygwin @@ -499,6 +501,7 @@ let print_builtin_inline oc name args res = let float_literals : (int * int64) list ref = ref [] let jumptables : (int * label list) list ref = ref [] +let indirect_symbols : StringSet.t ref = ref StringSet.empty (* Reminder on AT&T syntax: op source, dest *) @@ -508,6 +511,13 @@ let print_instruction oc = function fprintf oc " movl %a, %a\n" ireg r1 ireg rd | Pmov_ri(rd, n) -> fprintf oc " movl $%ld, %a\n" (camlint_of_coqint n) ireg rd + | Pmov_raddr(rd, id) -> + if target = MacOS then begin + let id = extern_atom id in + indirect_symbols := StringSet.add id !indirect_symbols; + fprintf oc " movl L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd + end else + fprintf oc " movl $%a, %a\n" symbol id ireg rd | Pmov_rm(rd, a) -> fprintf oc " movl %a, %a\n" addressing a ireg rd | Pmov_mr(a, r1) -> @@ -822,6 +832,7 @@ let print_var oc (name, v) = let print_program oc p = need_masks := false; + indirect_symbols := StringSet.empty; List.iter (print_var oc) p.prog_vars; List.iter (print_fundef oc) p.prog_funct; if !need_masks then begin @@ -831,4 +842,13 @@ let print_program oc p = raw_symbol "__negd_mask"; fprintf oc "%a: .quad 0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n" raw_symbol "__absd_mask" + end; + if target = MacOS then begin + fprintf oc " .section __IMPORT,__pointers,non_lazy_symbol_pointers\n"; + StringSet.iter + (fun s -> + fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s; + fprintf oc " .indirect_symbol %a\n" raw_symbol s; + fprintf oc " .long 0\n") + !indirect_symbols end diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 62de4ce..19e64cc 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -52,8 +52,20 @@ Open Local Scope cminorsel_scope. (** ** Constants **) +(** External oracle to determine whether a symbol is external and must + be addressed through [Oaddrsymbol], or is local and can be addressed + through [Olea Aglobal]. This is to accommodate MacOS X's limitations + on references to data symbols imported from shared libraries. *) + +Parameter symbol_is_external: ident -> bool. + Definition addrsymbol (id: ident) (ofs: int) := - Eop (Olea (Aglobal id ofs)) Enil. + if symbol_is_external id then + if Int.eq ofs Int.zero + then Eop (Oaddrsymbol id) Enil + else Eop (Olea (Aindexed ofs)) (Eop (Oaddrsymbol id) Enil ::: Enil) + else + Eop (Olea (Aglobal id ofs)) Enil. Definition addrstack (ofs: int) := Eop (Olea (Ainstack ofs)) Enil. @@ -410,9 +422,10 @@ Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). Definition intuoffloat (e: expr) := let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in Elet e - (Econdition (CEcond (Ccompf Clt) (Eletvar O ::: f ::: Enil)) - (intoffloat (Eletvar O)) - (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar O) f)))). + (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil) + (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (intoffloat (Eletvar 1)) + (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. Definition floatofintu (e: expr) := let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 9b1cd89..f30bb88 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -119,9 +119,14 @@ Theorem eval_addrsymbol: forall le id ofs, exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (symbol_address ge id ofs) v. Proof. - intros. unfold addrsymbol. econstructor; split. - EvalOp. simpl; eauto. - auto. + intros. unfold addrsymbol. exists (symbol_address ge id ofs); split; auto. + destruct (symbol_is_external id). + predSpec Int.eq Int.eq_spec ofs Int.zero. + subst. EvalOp. + EvalOp. econstructor. EvalOp. simpl; eauto. econstructor. simpl. + unfold symbol_address. destruct (Genv.find_symbol ge id); auto. + simpl. rewrite Int.add_commut. rewrite Int.add_zero. auto. + EvalOp. Qed. Theorem eval_addrstack: @@ -679,32 +684,36 @@ Theorem eval_intuoffloat: Val.intuoffloat x = Some y -> exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v. Proof. - intros. destruct x; simpl in H0; try discriminate. + intros. destruct x; simpl in H0; try discriminate. destruct (Float.intuoffloat f) as [n|]_eqn; simpl in H0; inv H0. - exists (Vint n); split; auto. - unfold intuoffloat. - econstructor. eauto. + exists (Vint n); split; auto. unfold intuoffloat. set (im := Int.repr Int.half_modulus). set (fm := Float.floatofintu im). - assert (eval_expr ge sp e m (Vfloat f :: le) (Eletvar O) (Vfloat f)). - constructor. auto. + assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). + constructor. auto. + assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar O) (Vfloat fm)). + constructor. auto. + econstructor. eauto. + econstructor. instantiate (1 := Vfloat fm). EvalOp. apply eval_Econdition with (v1 := Float.cmp Clt f fm). - econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. - simpl. auto. + econstructor. eauto with evalexpr. auto. destruct (Float.cmp Clt f fm) as []_eqn. exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. - exploit Float.intuoffloat_intoffloat_2; eauto. intro EQ. - replace n with (Int.add (Int.sub n Float.ox8000_0000) Float.ox8000_0000). - exploit (eval_addimm Float.ox8000_0000 (Vfloat f :: le) - (intoffloat - (subf (Eletvar 0) - (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil)))). - unfold intoffloat, subf. - EvalOp. constructor. EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. - simpl. eauto. constructor. simpl. rewrite EQ. simpl; eauto. - intros [v [A B]]. simpl in B. inv B. auto. - rewrite Int.sub_add_opp. rewrite Int.add_assoc. apply Int.add_zero. + exploit Float.intuoffloat_intoffloat_2; eauto. + change Float.ox8000_0000 with im. fold fm. intro EQ. + set (t2 := subf (Eletvar (S O)) (Eletvar O)). + set (t3 := intoffloat t2). + exploit (eval_subf (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f) (Eletvar O)); eauto. + fold t2. intros [v2 [A2 B2]]. simpl in B2. inv B2. + exploit (eval_addimm Float.ox8000_0000 (Vfloat fm :: Vfloat f :: le) t3). + unfold t3. unfold intoffloat. EvalOp. simpl. rewrite EQ. simpl. eauto. + intros [v4 [A4 B4]]. simpl in B4. inv B4. + rewrite Int.sub_add_opp in A4. rewrite Int.add_assoc in A4. + rewrite (Int.add_commut (Int.neg im)) in A4. + rewrite Int.add_neg_zero in A4. + rewrite Int.add_zero in A4. + auto. Qed. Theorem eval_floatofintu: diff --git a/ia32/extractionMachdep.v b/ia32/extractionMachdep.v index 435dce2..3c6ee2e 100644 --- a/ia32/extractionMachdep.v +++ b/ia32/extractionMachdep.v @@ -12,3 +12,9 @@ (* Additional extraction directives specific to the IA32 port *) +Require SelectOp. + +(* SelectOp *) + +Extract Constant SelectOp.symbol_is_external => + "fun id -> Configuration.system = ""macosx"" && C2C.atom_is_extern id". |