Merge of the clightgen branch:

- Alternate semantics for Clight where function parameters are temporaries,
  not variables
- New pass SimplLocals that turns non-addressed local variables into
  temporaries
- Simplified Csharpminor, Cshmgen and Cminorgen accordingly
- SimplExpr starts its temporaries above variable names, therefoe
  Cminorgen no longer needs to encode variable names and temps names.
- Simplified Cminor parser & printer, as well as Errors, accordingly.
- New tool clightgen to produce Clight AST in Coq-parsable .v files.
- Removed side condition "return type is void" on rules skip_seq
  in the semantics of CompCert C, Clight, C#minor, Cminor.
- Adapted RTLgenproof accordingly (now uses a memory extension).


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 22 deletions

diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 159ba99a..153f177b 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -83,8 +83,10 @@ Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
 
 Local Open Scope gensym_monad_scope.
 
-Definition initial_generator : generator := 
-  mkgenerator 1%positive nil.
+Parameter first_unused_ident: unit -> ident.
+
+Definition initial_generator (x: unit) : generator := 
+  mkgenerator (first_unused_ident x) nil.
 
 Definition gensym (ty: type): mon ident :=
   fun (g: generator) => 
@@ -397,7 +399,8 @@ Definition transl_expr_stmt (r: C.expr) : mon statement :=
 
 (*
 Definition transl_if (r: C.expr) (s1 s2: statement) : mon statement :=
-  do (sl, a) <- transl_expr (For_test nil s1 s2) r; ret (makeseq sl).
+  do (sl, a) <- transl_expr For_val r;
+  ret (makeseq (sl ++ makeif a s1 s2 :: nil)).
 *)
 
 Definition transl_if (r: C.expr) (s1 s2: statement) : mon statement :=
@@ -414,24 +417,6 @@ Proof.
   destruct s; ((left; reflexivity) || (right; congruence)).
 Defined.
 
-(** There are two possible translations for an "if then else" statement.
-  One is more efficient if the condition contains "?" constructors
-  but can duplicate the "then" and "else" branches.
-  The other produces no code duplication.  We choose between the
-  two based on the shape of the "then" and "else" branches. *)
-(*
-Fixpoint small_stmt (s: statement) : bool :=
-  match s with
-  | Sskip => true
-  | Sbreak => true
-  | Scontinue => true
-  | Sgoto _ => true
-  | Sreturn None => true
-  | Ssequence s1 s2 => small_stmt s1 && small_stmt s2
-  | _ => false
-  end.
-*)
-
 Fixpoint transl_stmt (s: C.statement) : mon statement :=
   match s with
   | C.Sskip => ret Sskip
@@ -496,7 +481,7 @@ with transl_lblstmt (ls: C.labeled_statements) : mon labeled_statements :=
 (** Translation of a function *)
 
 Definition transl_function (f: C.function) : res function :=
-  match transl_stmt f.(C.fn_body) initial_generator with
+  match transl_stmt f.(C.fn_body) (initial_generator tt) with
   | Err msg =>
       Error msg
   | Res tbody g i =>