diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Allocation.v | 3 | ||||
-rw-r--r-- | backend/Allocproof.v | 5 | ||||
-rw-r--r-- | backend/Asmexpandaux.ml | 3 | ||||
-rw-r--r-- | backend/CminorSel.v | 6 | ||||
-rw-r--r-- | backend/Deadcode.v | 2 | ||||
-rw-r--r-- | backend/Deadcodeproof.v | 9 | ||||
-rw-r--r-- | backend/Inlining.v | 1 | ||||
-rw-r--r-- | backend/Inliningproof.v | 8 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 4 | ||||
-rw-r--r-- | backend/RTLgen.v | 4 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 27 | ||||
-rw-r--r-- | backend/RTLtyping.v | 2 | ||||
-rw-r--r-- | backend/Regalloc.ml | 15 | ||||
-rw-r--r-- | backend/Stacking.v | 2 | ||||
-rw-r--r-- | backend/Stackingproof.v | 4 | ||||
-rw-r--r-- | backend/Unusedglobproof.v | 4 | ||||
-rw-r--r-- | backend/ValueAnalysis.v | 5 | ||||
-rw-r--r-- | backend/XTL.ml | 1 |
18 files changed, 95 insertions, 10 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 3dd4cb09..3ac99a47 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -808,6 +808,9 @@ Fixpoint add_equations_builtin_arg | BA_splitlong hi lo, BA_splitlong hi' lo' => do e1 <- add_equations_builtin_arg env hi hi' e; add_equations_builtin_arg env lo lo' e1 + | BA_addptr a1 a2, BA_addptr a1' a2' => + do e1 <- add_equations_builtin_arg env a1 a1' e; + add_equations_builtin_arg env a2 a2' e1 | _, _ => None end. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 3b2ecd35..6c10d27f 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1560,6 +1560,11 @@ Proof. intros (v1 & A & B). exploit IHeval_builtin_arg2; eauto. intros (v2 & C & D). exists (Val.longofwords v1 v2); split; auto with barg. apply Val.longofwords_lessdef; auto. +- exploit IHeval_builtin_arg1; eauto. eapply add_equations_builtin_arg_satisf; eauto. + intros (v1' & A & B). + exploit IHeval_builtin_arg2; eauto. intros (v2' & C & D). + econstructor; split. eauto with barg. + destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef. Qed. Lemma add_equations_builtin_args_satisf: diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index 13aa71d2..07e33efa 100644 --- a/backend/Asmexpandaux.ml +++ b/backend/Asmexpandaux.ml @@ -82,7 +82,8 @@ let translate_annot sp preg_to_dwarf annot = | BA_single _ | BA_loadglobal _ | BA_addrglobal _ - | BA_loadstack _ -> None + | BA_loadstack _ + | BA_addptr _ -> None | BA_addrstack ofs -> Some (sp,BA_addrstack ofs) | BA_splitlong (hi,lo) -> begin diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 9439c269..96cb8ae6 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -272,7 +272,11 @@ Inductive eval_builtin_arg: builtin_arg expr -> val -> Prop := eval_builtin_arg (BA_addrglobal id ofs) (Genv.symbol_address ge id ofs) | eval_BA_splitlong: forall a1 a2 v1 v2, eval_expr nil a1 v1 -> eval_expr nil a2 v2 -> - eval_builtin_arg (BA_splitlong (BA a1) (BA a2)) (Val.longofwords v1 v2). + eval_builtin_arg (BA_splitlong (BA a1) (BA a2)) (Val.longofwords v1 v2) + | eval_BA_addptr: forall a1 v1 a2 v2, + eval_builtin_arg a1 v1 -> eval_builtin_arg a2 v2 -> + eval_builtin_arg (BA_addptr a1 a2) + (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2). End EVAL_EXPR. diff --git a/backend/Deadcode.v b/backend/Deadcode.v index e5b2ce3a..f491d678 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -68,6 +68,8 @@ Fixpoint transfer_builtin_arg (nv: nval) (na: NA.t) (a: builtin_arg reg) : NA.t | BA_loadglobal chunk id ofs => (ne, nmem_add nm (Gl id ofs) (size_chunk chunk)) | BA_splitlong hi lo => transfer_builtin_arg All (transfer_builtin_arg All na hi) lo + | BA_addptr hi lo => + transfer_builtin_arg All (transfer_builtin_arg All na hi) lo end. Definition transfer_builtin_args (na: NA.t) (al: list (builtin_arg reg)) : NA.t := diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 3f0c5a4c..07c3f84a 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -609,6 +609,12 @@ Proof. constructor; auto. apply vagree_lessdef. apply Val.longofwords_lessdef; apply lessdef_vagree; auto. +- destruct (transfer_builtin_arg All (ne1, nm1) a1) as [ne' nm'] eqn:TR. + exploit IHeval_builtin_arg2; eauto. intros (v2' & A & B & C & D). + exploit IHeval_builtin_arg1; eauto. intros (v1' & P & Q & R & S). + econstructor; intuition auto. + econstructor; eauto. + destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef, vagree_lessdef, lessdef_vagree. Qed. Lemma transfer_builtin_args_sound: @@ -657,6 +663,9 @@ Proof. - destruct IHeval_builtin_arg1 as (v1' & A1). destruct IHeval_builtin_arg2 as (v2' & A2). exists (Val.longofwords v1' v2'); constructor; auto. +- destruct IHeval_builtin_arg1 as (v1' & A1). + destruct IHeval_builtin_arg2 as (v2' & A2). + econstructor; econstructor; eauto. Qed. Lemma can_eval_builtin_args: diff --git a/backend/Inlining.v b/backend/Inlining.v index 61776743..17139dbd 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -203,6 +203,7 @@ Fixpoint sbuiltinarg (ctx: context) (a: builtin_arg reg) : builtin_arg reg := | BA_loadstack chunk ofs => BA_loadstack chunk (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk))) | BA_addrstack ofs => BA_addrstack (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk))) | BA_splitlong hi lo => BA_splitlong (sbuiltinarg ctx hi) (sbuiltinarg ctx lo) + | BA_addptr a1 a2 => BA_addptr (sbuiltinarg ctx a1) (sbuiltinarg ctx a2) | _ => a end. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index bc991f0f..c3b0cfc3 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -436,9 +436,13 @@ Proof. unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. inv MG. econstructor. eauto. rewrite Ptrofs.add_zero; auto. -- destruct IHeval_builtin_arg1 as (v1 & A1 & B1). - destruct IHeval_builtin_arg2 as (v2 & A2 & B2). +- destruct IHeval_builtin_arg1 as (v1' & A1 & B1). + destruct IHeval_builtin_arg2 as (v2' & A2 & B2). econstructor; split. eauto with barg. apply Val.longofwords_inject; auto. +- destruct IHeval_builtin_arg1 as (v1' & A1 & B1). + destruct IHeval_builtin_arg2 as (v2' & A2 & B2). + econstructor; split. eauto with barg. + destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject. Qed. Lemma tr_builtin_args: diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index c8f8ea82..f54c8698 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -178,6 +178,10 @@ let rec print_annot print_preg sp_reg_name oc = function fprintf oc "(%a * 0x100000000 + %a)" (print_annot print_preg sp_reg_name) hi (print_annot print_preg sp_reg_name) lo + | BA_addptr(a1, a2) -> + fprintf oc "(%a + %a)" + (print_annot print_preg sp_reg_name) a1 + (print_annot print_preg sp_reg_name) a2 let print_annot_text print_preg sp_reg_name oc txt args = let print_fragment = function diff --git a/backend/RTLgen.v b/backend/RTLgen.v index cfbf57d6..6d81f84b 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -396,6 +396,10 @@ Fixpoint convert_builtin_arg {A: Type} (a: builtin_arg expr) (rl: list A) : buil let (hi', rl1) := convert_builtin_arg hi rl in let (lo', rl2) := convert_builtin_arg lo rl1 in (BA_splitlong hi' lo', rl2) + | BA_addptr a1 a2 => + let (a1', rl1) := convert_builtin_arg a1 rl in + let (a2', rl2) := convert_builtin_arg a2 rl1 in + (BA_addptr a1' a2', rl2) end. Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list A) : list (builtin_arg A) := diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index b635fd58..93f209b7 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1010,10 +1010,18 @@ Lemma invert_eval_builtin_arg: /\ Events.eval_builtin_arg ge (fun v => v) sp m (fst (convert_builtin_arg a vl)) v /\ (forall vl', convert_builtin_arg a (vl ++ vl') = (fst (convert_builtin_arg a vl), vl')). Proof. - induction 1; simpl; econstructor; intuition eauto with evalexpr barg. - constructor. - constructor. - repeat constructor. + induction 1; simpl; try (econstructor; intuition eauto with evalexpr barg; fail). +- econstructor; split; eauto with evalexpr. split. constructor. auto. +- econstructor; split; eauto with evalexpr. split. constructor. auto. +- econstructor; split; eauto with evalexpr. split. repeat constructor. auto. +- destruct IHeval_builtin_arg1 as (vl1 & A1 & B1 & C1). + destruct IHeval_builtin_arg2 as (vl2 & A2 & B2 & C2). + destruct (convert_builtin_arg a1 vl1) as [a1' rl1] eqn:E1; simpl in *. + destruct (convert_builtin_arg a2 vl2) as [a2' rl2] eqn:E2; simpl in *. + exists (vl1 ++ vl2); split. + apply eval_exprlist_append; auto. + split. rewrite C1, E2. constructor; auto. + intros. rewrite app_ass, !C1, C2, E2. auto. Qed. Lemma invert_eval_builtin_args: @@ -1057,6 +1065,17 @@ Proof. rewrite CV2, CV4; simpl. intros (v2' & A2 & B2 & C2). exists (Val.longofwords v1' v2'); split. constructor; auto. split; auto. apply Val.longofwords_lessdef; auto. +- destruct (convert_builtin_arg a1 vl) as [a1' vl1] eqn:CV1; simpl in *. + destruct (convert_builtin_arg a2 vl1) as [a2' vl2] eqn:CV2; simpl in *. + destruct (convert_builtin_arg a1 rl) as [a1'' rl1] eqn:CV3; simpl in *. + destruct (convert_builtin_arg a2 rl1) as [a2'' rl2] eqn:CV4; simpl in *. + inv EV. + exploit IHa1; eauto. rewrite CV1; simpl; eauto. + rewrite CV1, CV3; simpl. intros (v1' & A1 & B1 & C1). + exploit IHa2. eexact C1. rewrite CV2; simpl; eauto. + rewrite CV2, CV4; simpl. intros (v2' & A2 & B2 & C2). + econstructor; split. constructor; eauto. + split; auto. destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef. Qed. Lemma transl_eval_builtin_args: diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 9992ab79..fef74706 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -77,6 +77,7 @@ Definition type_of_builtin_arg (a: builtin_arg reg) : typ := | BA_loadglobal chunk id ofs => type_of_chunk chunk | BA_addrglobal id ofs => Tptr | BA_splitlong hi lo => Tlong + | BA_addptr a1 a2 => Tptr end. Definition type_of_builtin_res (r: builtin_res reg) : typ := @@ -249,6 +250,7 @@ Definition type_builtin_arg (e: S.typenv) (a: builtin_arg reg) (ty: typ) : res S | BA_loadglobal chunk id ofs => type_expect e ty (type_of_chunk chunk) | BA_addrglobal id ofs => type_expect e ty Tptr | BA_splitlong hi lo => type_expect e ty Tlong + | BA_addptr a1 a2 => type_expect e ty Tptr end. Fixpoint type_builtin_args (e: S.typenv) (al: list (builtin_arg reg)) (tyl: list typ) : res S.typenv := diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index c14852f4..d4d7362d 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -167,6 +167,8 @@ let rec convert_builtin_arg tyenv = function | BA_addrglobal(id, ofs) -> BA_addrglobal(id, ofs) | BA_splitlong(hi, lo) -> BA_splitlong(convert_builtin_arg tyenv hi, convert_builtin_arg tyenv lo) + | BA_addptr(a1, a2) -> + BA_addptr(convert_builtin_arg tyenv a1, convert_builtin_arg tyenv a2) let convert_builtin_res tyenv = function | BR r -> @@ -185,6 +187,10 @@ let rec constrain_builtin_arg a cl = let (hi', cl1) = constrain_builtin_arg hi cl in let (lo', cl2) = constrain_builtin_arg lo cl1 in (BA_splitlong(hi', lo'), cl2) + | BA_addptr(a1, a2), _ -> + let (a1', cl1) = constrain_builtin_arg a1 cl in + let (a2', cl2) = constrain_builtin_arg a2 cl1 in + (BA_addptr(a1', a2'), cl2) | _, _ -> (a, cl) let rec constrain_builtin_args al cl = @@ -335,6 +341,7 @@ let rec vset_addarg a after = match a with | BA v -> VSet.add v after | BA_splitlong(hi, lo) -> vset_addarg hi (vset_addarg lo after) + | BA_addptr(a1, a2) -> vset_addarg a1 (vset_addarg a2 after) | _ -> after let vset_addargs al after = List.fold_right vset_addarg al after @@ -432,8 +439,8 @@ let rec dce_parmove srcs dsts after = let rec keep_builtin_arg after = function | BA v -> VSet.mem v after - | BA_splitlong(hi, lo) -> - keep_builtin_arg after hi && keep_builtin_arg after lo + | BA_splitlong(a1, a2) | BA_addptr(a1, a2) -> + keep_builtin_arg after a1 && keep_builtin_arg after a2 | _ -> true let dce_instr instr after k = @@ -855,6 +862,10 @@ let rec reload_arg tospill eqs = function let (hi', c1, eqs1) = reload_arg tospill eqs hi in let (lo', c2, eqs2) = reload_arg tospill eqs1 lo in (BA_splitlong(hi', lo'), c1 @ c2, eqs2) + | BA_addptr(a1, a2) -> + let (a1', c1, eqs1) = reload_arg tospill eqs a1 in + let (a2', c2, eqs2) = reload_arg tospill eqs1 a2 in + (BA_addptr(a1', a2'), c1 @ c2, eqs2) | a -> (a, [], eqs) let rec reload_args tospill eqs = function diff --git a/backend/Stacking.v b/backend/Stacking.v index f51848f2..7b382d05 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -97,6 +97,8 @@ Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg m | BA_addrglobal id ofs => BA_addrglobal id ofs | BA_splitlong hi lo => BA_splitlong (transl_builtin_arg fe hi) (transl_builtin_arg fe lo) + | BA_addptr a1 a2 => + BA_addptr (transl_builtin_arg fe a1) (transl_builtin_arg fe a2) end. (** Translation of a Linear instruction. Prepends the corresponding diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index b885d22c..d3d901b6 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1744,6 +1744,10 @@ Local Opaque fe. destruct IHeval_builtin_arg2 as (v2 & A2 & B2); auto using in_or_app. exists (Val.longofwords v1 v2); split; auto with barg. apply Val.longofwords_inject; auto. +- destruct IHeval_builtin_arg1 as (v1' & A1 & B1); auto using in_or_app. + destruct IHeval_builtin_arg2 as (v2' & A2 & B2); auto using in_or_app. + econstructor; split. eauto with barg. + destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject. Qed. Lemma transl_builtin_args_correct: diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index db03d0b3..446ffb7f 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -853,6 +853,10 @@ Proof. destruct IHeval_builtin_arg2 as (v2' & A2 & B2); eauto using in_or_app. exists (Val.longofwords v1' v2'); split; auto with barg. apply Val.longofwords_inject; auto. +- destruct IHeval_builtin_arg1 as (v1' & A1 & B1); eauto using in_or_app. + destruct IHeval_builtin_arg2 as (v2' & A2 & B2); eauto using in_or_app. + econstructor; split; eauto with barg. + destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject. Qed. Lemma eval_builtin_args_inject: diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 17a518cd..7c4c0525 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -59,6 +59,10 @@ Fixpoint abuiltin_arg (ae: aenv) (am: amem) (rm: romem) (ba: builtin_arg reg) : | BA_loadglobal chunk id ofs => loadv chunk rm am (Ptr (Gl id ofs)) | BA_addrglobal id ofs => Ptr (Gl id ofs) | BA_splitlong hi lo => longofwords (abuiltin_arg ae am rm hi) (abuiltin_arg ae am rm lo) + | BA_addptr ba1 ba2 => + let v1 := abuiltin_arg ae am rm ba1 in + let v2 := abuiltin_arg ae am rm ba2 in + if Archi.ptr64 then addl v1 v2 else add v1 v2 end. Definition set_builtin_res (br: builtin_res reg) (av: aval) (ae: aenv) : aenv := @@ -338,6 +342,7 @@ Proof. - simpl. rewrite Ptrofs.add_zero_l. auto with va. - eapply loadv_sound; eauto. apply symbol_address_sound; auto. - apply symbol_address_sound; auto. +- destruct Archi.ptr64; auto with va. Qed. Lemma abuiltin_args_sound: diff --git a/backend/XTL.ml b/backend/XTL.ml index a1b7f23b..f10efeed 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -133,6 +133,7 @@ let rec type_builtin_arg a ty = match a with | BA v -> set_var_type v ty | BA_splitlong(a1, a2) -> type_builtin_arg a1 Tint; type_builtin_arg a2 Tint + | BA_addptr(a1, a2) -> type_builtin_arg a1 coq_Tptr; type_builtin_arg a2 coq_Tptr | _ -> () let rec type_builtin_args al tyl = |