diff options
| -rw-r--r-- | backend/Cminortyping.v | 35 | ||||
| -rw-r--r-- | backend/Selectionaux.ml | 4 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 4 |
3 files changed, 0 insertions, 43 deletions
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v index c0b7af78..fccbda27 100644 --- a/backend/Cminortyping.v +++ b/backend/Cminortyping.v @@ -139,11 +139,7 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := | Scall optid sg fn args => do e1 <- type_expr e fn Tptr; do e2 <- type_exprlist e1 args sg.(sig_args); -<<<<<<< HEAD - opt_set e2 optid sg.(sig_res) -======= opt_set e2 optid (proj_sig_res sg) ->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a | Stailcall sg fn args => assertion (opt_typ_eq sg.(sig_res) tret); do e1 <- type_expr e fn Tptr; @@ -151,11 +147,7 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := | Sbuiltin optid ef args => let sg := ef_sig ef in do e1 <- type_exprlist e args sg.(sig_args); -<<<<<<< HEAD - opt_set e1 optid sg.(sig_res) -======= opt_set e1 optid (proj_sig_res sg) ->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a | Sseq s1 s2 => do e1 <- type_stmt tret e s1; type_stmt tret e1 s2 | Sifthenelse a s1 s2 => @@ -171,15 +163,9 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := | Sswitch sz a tbl dfl => type_expr e a (if sz then Tlong else Tint) | Sreturn opta => -<<<<<<< HEAD - match tret, opta with - | None, None => OK e - | Some t, Some a => type_expr e a t -======= match opta, tret with | None, _ => OK e | Some a, Some t => type_expr e a t ->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a | _, _ => Error (msg "inconsistent return") end | Slabel lbl s1 => @@ -220,14 +206,10 @@ Inductive wt_expr: expr -> typ -> Prop := wt_expr (Eload chunk a1) (type_of_chunk chunk). Definition wt_opt_assign (optid: option ident) (optty: option typ) : Prop := -<<<<<<< HEAD - match optid with Some id => optty = Some (env id) | _ => True end. -======= match optid with | Some id => match optty with Some ty => ty | None => Tint end = env id | _ => True end. ->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a Inductive wt_stmt: stmt -> Prop := | wt_Sskip: @@ -268,10 +250,6 @@ Inductive wt_stmt: stmt -> Prop := wt_expr a (if sz then Tlong else Tint) -> wt_stmt (Sswitch sz a tbl dfl) | wt_Sreturn_none: -<<<<<<< HEAD - tret = None -> -======= ->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a wt_stmt (Sreturn None) | wt_Sreturn_some: forall a t, tret = Some t -> wt_expr a t -> @@ -382,14 +360,6 @@ Proof. Qed. Hint Resolve opt_set_incr: ty. -<<<<<<< HEAD -Lemma opt_set_sound: forall te optid optty e e', - opt_set e optid optty = OK e' -> S.satisf te e' -> wt_opt_assign te optid optty. -Proof. - unfold opt_set; intros; red. destruct optid; [destruct optty |]; try (monadInv H). -- erewrite S.set_sound by eauto. auto. -- auto. -======= Lemma opt_set_sound: forall te optid sg e e', opt_set e optid (proj_sig_res sg) = OK e' -> S.satisf te e' -> wt_opt_assign te optid sg.(sig_res). @@ -397,7 +367,6 @@ Proof. unfold opt_set; intros; red. destruct optid. - erewrite S.set_sound by eauto. auto. - inv H. auto. ->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a Qed. Lemma type_stmt_incr: forall te tret s e e', @@ -693,11 +662,7 @@ Proof. - inv WT_CONT. econstructor; eauto using wt_Sskip. inv H. - inv WT_CONT. econstructor; eauto using wt_Sexit. inv H. - econstructor; eauto using wt_Sexit. -<<<<<<< HEAD -- inv WT_STMT. econstructor; eauto using call_cont_wt. rewrite H0; exact I. -======= - inv WT_STMT. econstructor; eauto using call_cont_wt. exact I. ->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a - inv WT_STMT. econstructor; eauto using call_cont_wt. rewrite H2. eapply wt_eval_expr; eauto. - inv WT_STMT. econstructor; eauto. diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml index 818660c1..4e366564 100644 --- a/backend/Selectionaux.ml +++ b/backend/Selectionaux.ml @@ -114,9 +114,5 @@ let if_conversion_heuristic cond ifso ifnot ty = if !Clflags.option_ffavor_branchless then true else if not (fast_cmove ty) then false else let c1 = cost_expr ifso and c2 = cost_expr ifnot in -<<<<<<< HEAD - c1 + c2 <= 30 && abs (c1 - c2) <= 8 -======= c1 + c2 <= 24 && abs (c1 - c2) <= 8 ->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 01635ff1..40db5d4b 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -1102,11 +1102,7 @@ Proof. destruct (find_label lbl x (Kseq x0 k')) as [[sy ky] | ]; intuition. apply IHs2; auto. (* ifthenelse *) -<<<<<<< HEAD - destruct (if_conversion ki env e s1 s2) as [s|] eqn:IFC. -======= - destruct (if_conversion ki env e s1 s2) as [s|] eqn:IFC. ->>>>>>> ddb2c968e6c57d2117434f169471d87f643d831a inv SE. exploit if_conversion_nolabel; eauto. intros (A & B & C). rewrite A, B, C. auto. monadInv SE; simpl. |