From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CminorSel.v | 296 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 296 insertions(+) create mode 100644 backend/CminorSel.v (limited to 'backend/CminorSel.v') diff --git a/backend/CminorSel.v b/backend/CminorSel.v new file mode 100644 index 0000000..331105e --- /dev/null +++ b/backend/CminorSel.v @@ -0,0 +1,296 @@ +(** The Cminor language after instruction selection. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Events. +Require Import Values. +Require Import Mem. +Require Import Cminor. +Require Import Op. +Require Import Globalenvs. +Require Import Switch. + +(** * Abstract syntax *) + +(** CminorSel programs share the general structure of Cminor programs: + functions, statements and expressions. However, CminorSel uses + machine-dependent operations, addressing modes and conditions, + as defined in module [Op] and used in lower-level intermediate + languages ([RTL] and below). Moreover, a variant [condexpr] of [expr] + is used to represent expressions which are evaluated for their + boolean value only and not their exact value. +*) + +Inductive expr : Set := + | Evar : ident -> expr + | Eop : operation -> exprlist -> expr + | Eload : memory_chunk -> addressing -> exprlist -> expr + | Estore : memory_chunk -> addressing -> exprlist -> expr -> expr + | Ecall : signature -> expr -> exprlist -> expr + | Econdition : condexpr -> expr -> expr -> expr + | Elet : expr -> expr -> expr + | Eletvar : nat -> expr + | Ealloc : expr -> expr + +with condexpr : Set := + | CEtrue: condexpr + | CEfalse: condexpr + | CEcond: condition -> exprlist -> condexpr + | CEcondition : condexpr -> condexpr -> condexpr -> condexpr + +with exprlist : Set := + | Enil: exprlist + | Econs: expr -> exprlist -> exprlist. + +(** Statements are as in Cminor, except that the condition of an + if/then/else conditional is a [condexpr]. *) + +Inductive stmt : Set := + | Sskip: stmt + | Sexpr: expr -> stmt + | Sassign : ident -> expr -> stmt + | Sseq: stmt -> stmt -> stmt + | Sifthenelse: condexpr -> stmt -> stmt -> stmt + | Sloop: stmt -> stmt + | Sblock: stmt -> stmt + | Sexit: nat -> stmt + | Sswitch: expr -> list (int * nat) -> nat -> stmt + | Sreturn: option expr -> stmt + | Stailcall: signature -> expr -> exprlist -> stmt. + +Record function : Set := mkfunction { + fn_sig: signature; + fn_params: list ident; + fn_vars: list ident; + fn_stackspace: Z; + fn_body: stmt +}. + +Definition fundef := AST.fundef function. +Definition program := AST.program fundef unit. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => f.(fn_sig) + | External ef => ef.(ef_sig) + end. + +(** * Operational semantics *) + +(** Three kinds of evaluation environments are involved: +- [genv]: global environments, define symbols and functions; +- [env]: local environments, map local variables to values; +- [lenv]: let environments, map de Bruijn indices to values. +*) + +Definition genv := Genv.t fundef. + +Section RELSEM. + +Variable ge: genv. + +(** The evaluation predicates have the same general shape as those + of Cminor. Refer to the description of Cminor semantics for + the meaning of the parameters of the predicates. + One additional predicate is introduced: + [eval_condexpr ge sp le e m a t m' b], meaning that the conditional + expression [a] evaluates to the boolean [b]. *) + +Inductive eval_expr: + val -> letenv -> env -> + mem -> expr -> trace -> mem -> val -> Prop := + | eval_Evar: + forall sp le e m id v, + PTree.get id e = Some v -> + eval_expr sp le e m (Evar id) E0 m v + | eval_Eop: + forall sp le e m op al t m1 vl v, + eval_exprlist sp le e m al t m1 vl -> + eval_operation ge sp op vl m1 = Some v -> + eval_expr sp le e m (Eop op al) t m1 v + | eval_Eload: + forall sp le e m chunk addr al t m1 v vl a, + eval_exprlist sp le e m al t m1 vl -> + eval_addressing ge sp addr vl = Some a -> + Mem.loadv chunk m1 a = Some v -> + eval_expr sp le e m (Eload chunk addr al) t m1 v + | eval_Estore: + forall sp le e m chunk addr al b t t1 m1 vl t2 m2 m3 v a, + eval_exprlist sp le e m al t1 m1 vl -> + eval_expr sp le e m1 b t2 m2 v -> + eval_addressing ge sp addr vl = Some a -> + Mem.storev chunk m2 a v = Some m3 -> + t = t1 ** t2 -> + eval_expr sp le e m (Estore chunk addr al b) t m3 v + | eval_Ecall: + forall sp le e m sig a bl t t1 m1 t2 m2 t3 m3 vf vargs vres f, + eval_expr sp le e m a t1 m1 vf -> + eval_exprlist sp le e m1 bl t2 m2 vargs -> + Genv.find_funct ge vf = Some f -> + funsig f = sig -> + eval_funcall m2 f vargs t3 m3 vres -> + t = t1 ** t2 ** t3 -> + eval_expr sp le e m (Ecall sig a bl) t m3 vres + | eval_Econdition: + forall sp le e m a b c t t1 m1 v1 t2 m2 v2, + eval_condexpr sp le e m a t1 m1 v1 -> + eval_expr sp le e m1 (if v1 then b else c) t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr sp le e m (Econdition a b c) t m2 v2 + | eval_Elet: + forall sp le e m a b t t1 m1 v1 t2 m2 v2, + eval_expr sp le e m a t1 m1 v1 -> + eval_expr sp (v1::le) e m1 b t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr sp le e m (Elet a b) t m2 v2 + | eval_Eletvar: + forall sp le e m n v, + nth_error le n = Some v -> + eval_expr sp le e m (Eletvar n) E0 m v + | eval_Ealloc: + forall sp le e m a t m1 n m2 b, + eval_expr sp le e m a t m1 (Vint n) -> + Mem.alloc m1 0 (Int.signed n) = (m2, b) -> + eval_expr sp le e m (Ealloc a) t m2 (Vptr b Int.zero) + +with eval_condexpr: + val -> letenv -> env -> + mem -> condexpr -> trace -> mem -> bool -> Prop := + | eval_CEtrue: + forall sp le e m, + eval_condexpr sp le e m CEtrue E0 m true + | eval_CEfalse: + forall sp le e m, + eval_condexpr sp le e m CEfalse E0 m false + | eval_CEcond: + forall sp le e m cond al t1 m1 vl b, + eval_exprlist sp le e m al t1 m1 vl -> + eval_condition cond vl m1 = Some b -> + eval_condexpr sp le e m (CEcond cond al) t1 m1 b + | eval_CEcondition: + forall sp le e m a b c t t1 m1 vb1 t2 m2 vb2, + eval_condexpr sp le e m a t1 m1 vb1 -> + eval_condexpr sp le e m1 (if vb1 then b else c) t2 m2 vb2 -> + t = t1 ** t2 -> + eval_condexpr sp le e m (CEcondition a b c) t m2 vb2 + +with eval_exprlist: + val -> letenv -> env -> + mem -> exprlist -> trace -> mem -> list val -> Prop := + | eval_Enil: + forall sp le e m, + eval_exprlist sp le e m Enil E0 m nil + | eval_Econs: + forall sp le e m a bl t t1 m1 v t2 m2 vl, + eval_expr sp le e m a t1 m1 v -> + eval_exprlist sp le e m1 bl t2 m2 vl -> + t = t1 ** t2 -> + eval_exprlist sp le e m (Econs a bl) t m2 (v :: vl) + +with eval_funcall: + mem -> fundef -> list val -> trace -> + mem -> val -> Prop := + | eval_funcall_internal: + forall m f vargs m1 sp e t e2 m2 out vres, + Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) -> + set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> + exec_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t e2 m2 out -> + outcome_result_value out f.(fn_sig).(sig_res) vres -> + eval_funcall m (Internal f) vargs t (outcome_free_mem out m2 sp) vres + | eval_funcall_external: + forall ef m args t res, + event_match ef args t res -> + eval_funcall m (External ef) args t m res + +with exec_stmt: + val -> + env -> mem -> stmt -> trace -> + env -> mem -> outcome -> Prop := + | exec_Sskip: + forall sp e m, + exec_stmt sp e m Sskip E0 e m Out_normal + | exec_Sexpr: + forall sp e m a t m1 v, + eval_expr sp nil e m a t m1 v -> + exec_stmt sp e m (Sexpr a) t e m1 Out_normal + | exec_Sassign: + forall sp e m id a t m1 v, + eval_expr sp nil e m a t m1 v -> + exec_stmt sp e m (Sassign id a) t (PTree.set id v e) m1 Out_normal + | exec_Sifthenelse: + forall sp e m a s1 s2 t t1 m1 v1 t2 e2 m2 out, + eval_condexpr sp nil e m a t1 m1 v1 -> + exec_stmt sp e m1 (if v1 then s1 else s2) t2 e2 m2 out -> + t = t1 ** t2 -> + exec_stmt sp e m (Sifthenelse a s1 s2) t e2 m2 out + | exec_Sseq_continue: + forall sp e m t s1 t1 e1 m1 s2 t2 e2 m2 out, + exec_stmt sp e m s1 t1 e1 m1 Out_normal -> + exec_stmt sp e1 m1 s2 t2 e2 m2 out -> + t = t1 ** t2 -> + exec_stmt sp e m (Sseq s1 s2) t e2 m2 out + | exec_Sseq_stop: + forall sp e m t s1 s2 e1 m1 out, + exec_stmt sp e m s1 t e1 m1 out -> + out <> Out_normal -> + exec_stmt sp e m (Sseq s1 s2) t e1 m1 out + | exec_Sloop_loop: + forall sp e m s t t1 e1 m1 t2 e2 m2 out, + exec_stmt sp e m s t1 e1 m1 Out_normal -> + exec_stmt sp e1 m1 (Sloop s) t2 e2 m2 out -> + t = t1 ** t2 -> + exec_stmt sp e m (Sloop s) t e2 m2 out + | exec_Sloop_stop: + forall sp e m t s e1 m1 out, + exec_stmt sp e m s t e1 m1 out -> + out <> Out_normal -> + exec_stmt sp e m (Sloop s) t e1 m1 out + | exec_Sblock: + forall sp e m s t e1 m1 out, + exec_stmt sp e m s t e1 m1 out -> + exec_stmt sp e m (Sblock s) t e1 m1 (outcome_block out) + | exec_Sexit: + forall sp e m n, + exec_stmt sp e m (Sexit n) E0 e m (Out_exit n) + | exec_Sswitch: + forall sp e m a cases default t1 m1 n, + eval_expr sp nil e m a t1 m1 (Vint n) -> + exec_stmt sp e m (Sswitch a cases default) + t1 e m1 (Out_exit (switch_target n default cases)) + | exec_Sreturn_none: + forall sp e m, + exec_stmt sp e m (Sreturn None) E0 e m (Out_return None) + | exec_Sreturn_some: + forall sp e m a t m1 v, + eval_expr sp nil e m a t m1 v -> + exec_stmt sp e m (Sreturn (Some a)) t e m1 (Out_return (Some v)) + | exec_Stailcall: + forall sp e m sig a bl t t1 m1 t2 m2 t3 m3 vf vargs vres f, + eval_expr (Vptr sp Int.zero) nil e m a t1 m1 vf -> + eval_exprlist (Vptr sp Int.zero) nil e m1 bl t2 m2 vargs -> + Genv.find_funct ge vf = Some f -> + funsig f = sig -> + eval_funcall (Mem.free m2 sp) f vargs t3 m3 vres -> + t = t1 ** t2 ** t3 -> + exec_stmt (Vptr sp Int.zero) e m (Stailcall sig a bl) t e m3 (Out_tailcall_return vres). + +Scheme eval_expr_ind5 := Minimality for eval_expr Sort Prop + with eval_condexpr_ind5 := Minimality for eval_condexpr Sort Prop + with eval_exprlist_ind5 := Minimality for eval_exprlist Sort Prop + with eval_funcall_ind5 := Minimality for eval_funcall Sort Prop + with exec_stmt_ind5 := Minimality for exec_stmt Sort Prop. + +End RELSEM. + +Definition exec_program (p: program) (t: trace) (r: val) : Prop := + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + exists b, exists f, exists m, + Genv.find_symbol ge p.(prog_main) = Some b /\ + Genv.find_funct_ptr ge b = Some f /\ + funsig f = mksignature nil (Some Tint) /\ + eval_funcall ge m0 f nil t m r. + -- cgit v1.2.3