From 165407527b1be7df6a376791719321c788e55149 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 18 Sep 2006 15:52:24 +0000 Subject: Simplification de Cminor: les affectations de variables locales ne sont plus des expressions mais des statements (Eassign -> Sassign). Cela simplifie les preuves et ameliore la qualite du RTL produit. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Cminor.v | 160 +++++++++++++++++++++++++++---------------------------- 1 file changed, 79 insertions(+), 81 deletions(-) (limited to 'backend/Cminor.v') diff --git a/backend/Cminor.v b/backend/Cminor.v index 6fdf602..9ed5e19 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -15,7 +15,7 @@ Require Import Globalenvs. (** Cminor is a low-level imperative language structured in expressions, statements, functions and programs. Expressions include - reading and writing local variables, reading and writing store locations, + reading local variables, reading and writing store locations, arithmetic operations, function calls, and conditional expressions (similar to [e1 ? e2 : e3] in C). The [Elet] and [Eletvar] constructs enable sharing the computations of subexpressions. De Bruijn notation @@ -28,7 +28,6 @@ Require Import Globalenvs. Inductive expr : Set := | Evar : ident -> expr - | Eassign : ident -> expr -> expr | Eop : operation -> exprlist -> expr | Eload : memory_chunk -> addressing -> exprlist -> expr | Estore : memory_chunk -> addressing -> exprlist -> expr -> expr @@ -48,14 +47,15 @@ with exprlist : Set := | Enil: exprlist | Econs: expr -> exprlist -> exprlist. -(** Statements include expression evaluation, an if/then/else conditional, - infinite loops, blocks and early block exits, and early function returns. - [Sexit n] terminates prematurely the execution of the [n+1] enclosing - [Sblock] statements. *) +(** Statements include expression evaluation, assignment to local variables, + an if/then/else conditional, infinite loops, blocks and early block + exits, and early function returns. [Sexit n] terminates prematurely + the execution of the [n+1] enclosing [Sblock] statements. *) Inductive stmt : Set := | Sskip: stmt | Sexpr: expr -> stmt + | Sassign : ident -> expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -154,126 +154,120 @@ Section RELSEM. Variable ge: genv. -(** Evaluation of an expression: [eval_expr ge sp le e m a e' m' v] +(** Evaluation of an expression: [eval_expr ge sp le e m a m' v] states that expression [a], in initial local environment [e] and - memory state [m], evaluates to value [v]. [e'] and [m'] are the final - local environment and memory state, respectively, reflecting variable - assignments and memory stores possibly performed by [a]. [ge] and - [le] are the global environment and let environment respectively, and - are unchanged during evaluation. [sp] is the pointer to the memory - block allocated for this function (stack frame). + memory state [m], evaluates to value [v]. [m'] is the final + memory state, reflecting memory stores possibly performed by [a]. + Expressions do not assign variables, therefore the local environment + [e] is unchanged. [ge] and [le] are the global environment and let + environment respectively, and are unchanged during evaluation. [sp] + is the pointer to the memory block allocated for this function + (stack frame). *) Inductive eval_expr: - val -> letenv -> - env -> mem -> expr -> trace -> - env -> mem -> val -> Prop := + 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 e m v - | eval_Eassign: - forall sp le e m id a t e1 m1 v, - eval_expr sp le e m a t e1 m1 v -> - eval_expr sp le e m (Eassign id a) t (PTree.set id v e1) m1 v + eval_expr sp le e m (Evar id) E0 m v | eval_Eop: - forall sp le e m op al t e1 m1 vl v, - eval_exprlist sp le e m al t e1 m1 vl -> + 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 = Some v -> - eval_expr sp le e m (Eop op al) t e1 m1 v + eval_expr sp le e m (Eop op al) t m1 v | eval_Eload: - forall sp le e m chunk addr al t e1 m1 v vl a, - eval_exprlist sp le e m al t e1 m1 vl -> + 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 e1 m1 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 e1 m1 vl t2 e2 m2 m3 v a, - eval_exprlist sp le e m al t1 e1 m1 vl -> - eval_expr sp le e1 m1 b t2 e2 m2 v -> + 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 e2 m3 v + 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 e1 m1 t2 e2 m2 t3 m3 vf vargs vres f, - eval_expr sp le e m a t1 e1 m1 vf -> - eval_exprlist sp le e1 m1 bl t2 e2 m2 vargs -> + 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 e2 m3 vres + 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 e1 m1 v1 t2 e2 m2 v2, - eval_condexpr sp le e m a t1 e1 m1 v1 -> - eval_expr sp le e1 m1 (if v1 then b else c) t2 e2 m2 v2 -> + 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 e2 m2 v2 + eval_expr sp le e m (Econdition a b c) t m2 v2 | eval_Elet: - forall sp le e m a b t t1 e1 m1 v1 t2 e2 m2 v2, - eval_expr sp le e m a t1 e1 m1 v1 -> - eval_expr sp (v1::le) e1 m1 b t2 e2 m2 v2 -> + 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 e2 m2 v2 + 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 e m v + eval_expr sp le e m (Eletvar n) E0 m v | eval_Ealloc: - forall sp le e m a t e1 m1 n m2 b, - eval_expr sp le e m a t e1 m1 (Vint n) -> + 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 e1 m2 (Vptr b Int.zero) + eval_expr sp le e m (Ealloc a) t m2 (Vptr b Int.zero) (** Evaluation of a condition expression: - [eval_condexpr ge sp le e m a e' m' b] + [eval_condexpr ge sp le e m a m' b] states that condition expression [a] evaluates to the boolean value [b]. The other parameters are as in [eval_expr]. *) with eval_condexpr: - val -> letenv -> - env -> mem -> condexpr -> trace -> - env -> mem -> bool -> Prop := + val -> letenv -> env -> + mem -> condexpr -> trace -> mem -> bool -> Prop := | eval_CEtrue: forall sp le e m, - eval_condexpr sp le e m CEtrue E0 e m true + 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 e m false + eval_condexpr sp le e m CEfalse E0 m false | eval_CEcond: - forall sp le e m cond al t1 e1 m1 vl b, - eval_exprlist sp le e m al t1 e1 m1 vl -> + 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 = Some b -> - eval_condexpr sp le e m (CEcond cond al) t1 e1 m1 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 e1 m1 vb1 t2 e2 m2 vb2, - eval_condexpr sp le e m a t1 e1 m1 vb1 -> - eval_condexpr sp le e1 m1 (if vb1 then b else c) t2 e2 m2 vb2 -> + 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 e2 m2 vb2 + eval_condexpr sp le e m (CEcondition a b c) t m2 vb2 (** Evaluation of a list of expressions: - [eval_exprlist ge sp le al m a e' m' vl] + [eval_exprlist ge sp le al m a m' vl] states that the list [al] of expressions evaluate to the list [vl] of values. The other parameters are as in [eval_expr]. *) with eval_exprlist: - val -> letenv -> - env -> mem -> exprlist -> trace -> - env -> mem -> list val -> Prop := + 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 e m nil + eval_exprlist sp le e m Enil E0 m nil | eval_Econs: - forall sp le e m a bl t t1 e1 m1 v t2 e2 m2 vl, - eval_expr sp le e m a t1 e1 m1 v -> - eval_exprlist sp le e1 m1 bl t2 e2 m2 vl -> + 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 e2 m2 (v :: vl) + eval_exprlist sp le e m (Econs a bl) t m2 (v :: vl) (** Evaluation of a function invocation: [eval_funcall ge m f args m' res] means that the function [f], applied to the arguments [args] in @@ -307,13 +301,17 @@ with exec_stmt: forall sp e m, exec_stmt sp e m Sskip E0 e m Out_normal | exec_Sexpr: - forall sp e m a t e1 m1 v, - eval_expr sp nil e m a t e1 m1 v -> - exec_stmt sp e m (Sexpr a) t e1 m1 Out_normal + 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 e1 m1 v1 t2 e2 m2 out, - eval_condexpr sp nil e m a t1 e1 m1 v1 -> - exec_stmt sp e1 m1 (if v1 then s1 else s2) t2 e2 m2 out -> + 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: @@ -346,17 +344,17 @@ with exec_stmt: 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 e1 m1 n, - eval_expr sp nil e m a t1 e1 m1 (Vint n) -> + 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 e1 m1 (Out_exit (switch_target n default cases)) + 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 e1 m1 v, - eval_expr sp nil e m a t e1 m1 v -> - exec_stmt sp e m (Sreturn (Some a)) t e1 m1 (Out_return (Some v)). + 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)). End RELSEM. -- cgit v1.2.3