From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CminorSel.v | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'backend/CminorSel.v') diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 84b47f3..a8e49e8 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -68,8 +68,8 @@ Inductive stmt : Type := | Sskip: stmt | Sassign : ident -> expr -> stmt | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt - | Scall : option ident -> signature -> expr -> exprlist -> stmt - | Stailcall: signature -> expr -> exprlist -> stmt + | Scall : option ident -> signature -> expr + ident -> exprlist -> stmt + | Stailcall: signature -> expr + ident -> exprlist -> stmt | Sbuiltin : option ident -> external_function -> exprlist -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt @@ -208,6 +208,14 @@ Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop. +Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop := + | eval_eos_e: forall le e v, + eval_expr le e v -> + eval_expr_or_symbol le (inl _ e) v + | eval_eos_s: forall le id b, + Genv.find_symbol ge id = Some b -> + eval_expr_or_symbol le (inr _ id) (Vptr b Int.zero). + End EVAL_EXPR. (** Pop continuation until a call or stop *) @@ -282,7 +290,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State f Sskip k sp e m') | step_call: forall f optid sig a bl k sp e m vf vargs fd, - eval_expr sp e m nil a vf -> + eval_expr_or_symbol sp e m nil a vf -> eval_exprlist sp e m nil bl vargs -> Genv.find_funct ge vf = Some fd -> funsig fd = sig -> @@ -290,7 +298,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (Callstate fd vargs (Kcall optid f sp e k) m) | step_tailcall: forall f sig a bl k sp e m vf vargs fd m', - eval_expr (Vptr sp Int.zero) e m nil a vf -> + eval_expr_or_symbol (Vptr sp Int.zero) e m nil a vf -> eval_exprlist (Vptr sp Int.zero) e m nil bl vargs -> Genv.find_funct ge vf = Some fd -> funsig fd = sig -> -- cgit v1.2.3