diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Selection.v | 72 | ||||
-rw-r--r-- | backend/Selectionproof.v | 6 |
2 files changed, 6 insertions, 72 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index d2067dab..05a06abf 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -267,68 +267,6 @@ Definition sel_switch_long := (fun arg ofs => subl arg (longconst (Int64.repr ofs))) lowlong. -Definition sel_builtin_default optid ef args := - OK (Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef))). - -Definition sel_builtin optid ef args := - match ef with - | EF_builtin name sign => - (if String.string_dec name "__builtin_ternary_uint" - || String.string_dec name "__builtin_ternary_int" - then - match optid with - | None => OK Sskip - | Some id => - match args with - | a1::a2::a3::nil => - OK (Sassign id (select (sel_expr a3) (sel_expr a2) (sel_expr a1))) - | _ => Error (msg "__builtin_ternary_(u)int: arguments") - end - end - else - if String.string_dec name "__builtin_ternary_ulong" - || String.string_dec name "__builtin_ternary_long" - then - match optid with - | None => OK Sskip - | Some id => - match args with - | a1::a2::a3::nil => - OK (Sassign id (selectl (sel_expr a3) (sel_expr a2) (sel_expr a1))) - | _ => Error (msg "__builtin_ternary_(u)long: arguments") - end - end - else - if String.string_dec name "__builtin_ternary_double" - then - match optid with - | None => OK Sskip - | Some id => - match args with - | a1::a2::a3::nil => - OK (Sassign id (selectf (sel_expr a3) (sel_expr a2) (sel_expr a1))) - | _ => Error (msg "__builtin_ternary_double: arguments") - end - end - else - if String.string_dec name "__builtin_ternary_float" - then - match optid with - | None => OK Sskip - | Some id => - match args with - | a1::a2::a3::nil => - OK (Sassign id (selectfs (sel_expr a3) (sel_expr a2) (sel_expr a1))) - | _ => Error (msg "__builtin_ternary_float: arguments") - end - end - else - sel_builtin_default optid ef args) - | _ => sel_builtin_default optid ef args - end. - (** Conversion from Cminor statements to Cminorsel statements. *) Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := @@ -337,10 +275,12 @@ Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := | Cminor.Sassign id e => OK (Sassign id (sel_expr e)) | Cminor.Sstore chunk addr rhs => OK (store chunk (sel_expr addr) (sel_expr rhs)) | Cminor.Scall optid sg fn args => - (match classify_call fn with - | Call_default => OK (Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args)) - | Call_imm id => OK (Scall optid sg (inr _ id) (sel_exprlist args)) - | Call_builtin ef => sel_builtin optid ef args + OK (match classify_call fn with + | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args) + | Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args) + | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef)) end) | Cminor.Sbuiltin optid ef args => OK (Sbuiltin (sel_builtin_res optid) ef diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index d839f22a..50ff377a 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -854,8 +854,6 @@ Remark find_label_commut: | _, _ => False end. Proof. -Admitted. -(* 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. @@ -888,7 +886,6 @@ Admitted. (* label *) destruct (ident_eq lbl l). auto. apply IHs; auto. Qed. - *) Definition measure (s: Cminor.state) : nat := match s with @@ -903,8 +900,6 @@ Lemma sel_step_correct: (exists T2, step tge T1 t T2 /\ match_states S2 T2) \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat. Proof. -Admitted. -(* induction 1; intros T1 ME; inv ME; try (monadInv TS). - (* skip seq *) inv MC. left; econstructor; split. econstructor. econstructor; eauto. @@ -1072,7 +1067,6 @@ Admitted. right; split. simpl; omega. split. auto. econstructor; eauto. apply sel_builtin_res_correct; auto. Qed. - *) Lemma sel_initial_states: forall S, Cminor.initial_state prog S -> |