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

1 files changed, 79 insertions, 81 deletions

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.