Documentation

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

9 files changed, 422 insertions, 211 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 23faf78..d021a63 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -26,16 +26,11 @@ Open Local Scope error_monad_scope.
   taken in the Csharpminor code can be mapped to Cminor local
   variable, since the latter do not reside in memory.  
 
-  Other tasks performed during the translation to Cminor:
-- Transformation of Csharpminor's standard set of operators and
-  trivial addressing modes to Cminor's processor-dependent operators
-  and addressing modes.  This is done using the optimizing Cminor
-  constructor functions provided in file [Cmconstr], therefore performing
-  instruction selection on the fly.
-- Insertion of truncation, zero- and sign-extension operations when
+  The other task performed during the translation to Cminor is the
+  insertion of truncation, zero- and sign-extension operations when
   assigning to a Csharpminor local variable of ``small'' type
   (e.g. [Mfloat32] or [Mint8signed]).  This is necessary to preserve
-  the ``normalize at assignment-time'' semantics of Csharpminor.
+  the ``normalize at assignment-time'' semantics of Clight and Csharpminor.
 *)
 
 (** Translation of constants. *)
@@ -62,6 +57,12 @@ Definition make_cast (chunk: memory_chunk) (e: expr): expr :=
   | Mfloat64 => e
   end.
 
+(** When the translation of an expression is stored in memory,
+  the normalization performed by [make_cast] can be redundant
+  with that implicitly performed by the memory store.
+  [store_arg] detects this case and strips away the redundant
+  normalization. *)
+
 Definition store_arg (chunk: memory_chunk) (e: expr) : expr :=
   match e with
   | Eunop Ocast8signed e1 =>
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index e24430c..385f7c6 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -1,4 +1,4 @@
-(** * Dynamic semantics for the Clight language *)
+(** Dynamic semantics for the Clight language *)
 
 Require Import Coqlib.
 Require Import Errors.
@@ -12,7 +12,12 @@ Require Import Events.
 Require Import Globalenvs.
 Require Import Csyntax.
 
-(** ** Semantics of type-dependent operations *)
+(** * Semantics of type-dependent operations *)
+
+(** Interpretation of values as truth values.
+  Non-zero integers, non-zero floats and non-null pointers are
+  considered as true.  The integer zero (which also represents
+  the null pointer) and the float 0.0 are false. *)
 
 Inductive is_false: val -> type -> Prop :=
   | is_false_int: forall sz sg,
@@ -45,6 +50,14 @@ Inductive bool_of_val : val -> type -> val -> Prop :=
         is_false v ty ->
         bool_of_val v ty Vfalse.
 
+(** The following [sem_] functions compute the result of an operator
+  application.  Since operators are overloaded, the result depends
+  both on the static types of the arguments and on their run-time values.
+  Unlike in C, automatic conversions between integers and floats
+  are not performed.  For instance, [e1 + e2] is undefined if [e1]
+  is a float and [e2] an integer.  The Clight producer must have explicitly
+  promoted [e2] to a float. *)
+
 Function sem_neg (v: val) (ty: type) : option val :=
   match ty with
   | Tint _ _ =>
@@ -111,23 +124,23 @@ end.
 
 Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   match classify_sub t1 t2 with
-  | sub_case_ii =>               (* integer subtraction *)
+  | sub_case_ii =>               (**r integer subtraction *)
       match v1,v2 with
       | Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2))
       | _,  _ => None
       end 
-  | sub_case_ff =>               (* float subtraction *)
+  | sub_case_ff =>               (**r float subtraction *)
       match v1,v2 with
       | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2))
       | _,  _ => None
       end
-  | sub_case_pi ty =>            (*array| pointer - offset *)
+  | sub_case_pi ty =>            (**r pointer minus integer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vint n2 => 
             Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
       | _,  _ => None
       end
-  | sub_case_pp ty =>          (* array|pointer - array|pointer *)
+  | sub_case_pp ty =>          (**r pointer minus pointer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vptr b2 ofs2 =>
           if zeq b1 b2 then
@@ -315,6 +328,10 @@ Definition sem_binary_operation
   | Oge => sem_cmp Cge v1 t1 v2 t2 m
   end.
 
+(** Semantic of casts.  [cast v1 t1 t2 v2] holds if value [v1],
+  viewed with static type [t1], can be cast to type [t2],
+  resulting in value [v2].  *)
+
 Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
   match sz, sg with
   | I8, Signed => Int.cast8signed i
@@ -366,25 +383,31 @@ Inductive cast : val -> type -> type -> val -> Prop :=
       neutral_for_cast t1 -> neutral_for_cast t2 ->
       cast (Vint n) t1 t2 (Vint n).
 
-(** ** Operational semantics *)
+(** * Operational semantics *)
 
-(** Global environment *)
+(** The semantics uses two environments.  The global environment
+  maps names of functions and global variables to memory block references,
+  and function pointers to their definitions.  (See module [Globalenvs].) *)
 
 Definition genv := Genv.t fundef.
 
-(** Local environment *)
+(** The local environment maps local variables to block references.
+  The current value of the variable is stored in the associated memory
+  block. *)
 
 Definition env := PTree.t block. (* map variable -> location *)
 
 Definition empty_env: env := (PTree.empty block).
 
-(** Outcomes for statements *)
+(** The execution of a statement produces an ``outcome'', indicating
+  how the execution terminated: either normally or prematurely
+  through the execution of a [break], [continue] or [return] statement. *)
 
 Inductive outcome: Set :=
-   | Out_break: outcome
-   | Out_continue: outcome
-   | Out_normal: outcome
-   | Out_return: option val -> outcome.
+   | Out_break: outcome                 (**r terminated by [break] *)
+   | Out_continue: outcome              (**r terminated by [continue] *)
+   | Out_normal: outcome                (**r terminated normally *)
+   | Out_return: option val -> outcome. (**r terminated by [return] *)
 
 Inductive out_normal_or_continue : outcome -> Prop :=
   | Out_normal_or_continue_N: out_normal_or_continue Out_normal
@@ -409,7 +432,8 @@ Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop :=
   | _, _ => False
   end. 
 
-(** Selection of the appropriate case of a [switch] *)
+(** Selection of the appropriate case of a [switch], given the value [n]
+  of the selector expression. *)
 
 Fixpoint select_switch (n: int) (sl: labeled_statements)
                        {struct sl}: labeled_statements :=
@@ -418,7 +442,11 @@ Fixpoint select_switch (n: int) (sl: labeled_statements)
   | LScase c s sl' => if Int.eq c n then sl else select_switch n sl'
   end.
 
-(** Loads and stores by type *)
+(** [load_value_of_type ty m b ofs] computes the value of a datum
+  of type [ty] residing in memory [m] at block [b], offset [ofs].
+  If the type [ty] indicates an access by value, the corresponding
+  memory load is performed.  If the type [ty] indicates an access by
+  reference, the pointer [Vptr b ofs] is returned. *)
 
 Definition load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val :=
   match access_mode ty with
@@ -427,6 +455,11 @@ Definition load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option
   | By_nothing => None
   end.
 
+(** Symmetrically, [store_value_of_type ty m b ofs v] returns the
+  memory state after storing the value [v] in the datum
+  of type [ty] residing in memory [m] at block [b], offset [ofs].
+  This is allowed only if [ty] indicates an access by value. *)
+
 Definition store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem :=
   match access_mode ty_dest with
   | By_value chunk => Mem.storev chunk m (Vptr loc ofs) v
@@ -434,7 +467,13 @@ Definition store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int)
   | By_nothing => None
   end.
 
-(** Allocation and initialization of function-local variables *)
+(** Allocation of function-local variables.
+  [alloc_variables e1 m1 vars e2 m2 bl] allocates one memory block
+  for each variable declared in [vars], and associates the variable
+  name with this block.  [e1] and [m1] are the initial local environment
+  and memory state.  [e2] and [m2] are the final local environment
+  and memory state.  The list [bl] collects the references to all
+  the blocks that were allocated. *)
 
 Inductive alloc_variables: env -> mem ->
                            list (ident * type) ->
@@ -448,6 +487,11 @@ Inductive alloc_variables: env -> mem ->
       alloc_variables (PTree.set id b1 e) m1 vars e2 m2 lb ->
       alloc_variables e m ((id, ty) :: vars) e2 m2 (b1 :: lb).
 
+(** Initialization of local variables that are parameters to a function.
+  [bind_parameters e m1 params args m2] stores the values [args]
+  in the memory blocks corresponding to the variables [params].
+  [m1] is the initial memory state and [m2] the final memory state. *)
+
 Inductive bind_parameters: env ->
                            mem -> list (ident * type) -> list val ->
                            mem -> Prop :=
@@ -465,7 +509,11 @@ Section RELSEM.
 
 Variable ge: genv.
 
-(** Evaluation of an expression in r-value position *)
+(** [eval_expr ge e m1 a t m2 v] defines the evaluation of expression [a]
+  in r-value position.  [v] is the value of the expression.
+  [m1] is the initial memory state, [m2] the final memory state.
+  [t] is the trace of input/output events performed during this
+  evaluation. *)
 
 Inductive eval_expr: env -> mem -> expr -> trace -> mem -> val -> Prop :=
   | eval_Econst_int:   forall e m i ty,
@@ -535,7 +583,11 @@ Inductive eval_expr: env -> mem -> expr -> trace -> mem -> val -> Prop :=
       eval_expr e m (Expr (Ecall a bl) ty)
                 (t1 ** t2 ** t3) m3 vres 
 
-(** Evaluation of an expression in l-value position *)
+(** [eval_lvalue ge e m1 a t m2  b ofs] defines the evaluation of
+  expression [a] in r-value position.  The result of the evaluation
+  is the block reference [b] and the byte offset [ofs] of the
+  memory location where the value of [a] resides.
+  The other parameters are as in [eval_expr]. *)
 
 with eval_lvalue: env -> mem -> expr -> trace -> mem -> block -> int -> Prop :=
   | eval_Evar_local:   forall e m id l ty,
@@ -569,7 +621,8 @@ with eval_lvalue: env -> mem -> expr -> trace -> mem -> block -> int -> Prop :=
       eval_lvalue e m (Expr (Efield a i) ty) 
                   t m1 l ofs
 
-(** Evaluation of a list of expressions *)
+(** [eval_exprlist ge e m1 al t m2 vl] evaluates a list of r-value
+  expressions [al] to their values [vl]. *)
 
 with eval_exprlist: env -> mem -> exprlist -> trace -> mem -> list val -> Prop :=
   | eval_Enil:   forall e m,
@@ -580,7 +633,11 @@ with eval_exprlist: env -> mem -> exprlist -> trace -> mem -> list val -> Prop :
       eval_exprlist e m (Econs a bl)
                     (t1 ** t2) m2 (v :: vl)
 
-(** Execution of a statement *)
+(** [exec_stmt ge e m1 s t m2 out] describes the execution of 
+  the statement [s].  [out] is the outcome for this execution.
+  [m1] is the initial memory state, [m2] the final memory state.
+  [t] is the trace of input/output events performed during this
+  evaluation. *)
 
 with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
   | exec_Sskip:   forall e m,
@@ -703,7 +760,9 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop :=
       exec_stmt e m (Sswitch a sl)
                 (t1 ** t2) m2 (outcome_switch out)
 
-(** Execution of a list of labeled statements *)
+(** [exec_lblstmts ge e m1 ls t m2 out] is a variant of [exec_stmt]
+  that executes in sequence all statements in the list of labeled
+  statements [ls]. *)
 
 with exec_lblstmts: env -> mem -> labeled_statements -> trace -> mem -> outcome -> Prop :=
   | exec_LSdefault: forall e m s t m1 out,
@@ -717,7 +776,9 @@ with exec_lblstmts: env -> mem -> labeled_statements -> trace -> mem -> outcome
      exec_stmt e m s t m1 out -> out <> Out_normal ->
      exec_lblstmts e m (LScase n s ls) t m1 out
 
-(** Evaluation of a function invocation *)
+(** [eval_funcall m1 fd args t m2 res] describes the invocation of
+  function [fd] with arguments [args].  [res] is the value returned
+  by the call.  *)
 
 with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
   | eval_funcall_internal: forall m f vargs t e m1 lb m2 m3 out vres,
@@ -739,7 +800,11 @@ Scheme eval_expr_ind6 := Minimality for eval_expr Sort Prop
 
 End RELSEM.
 
-(** Execution of a whole program *)
+(** Execution of a whole program: [exec_program p t r]
+  holds if the application of [p]'s main function to no arguments
+  in the initial memory state for [p] performs the input/output
+  operations described in the trace [t], and eventually returns value [r].
+*)
 
 Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
   let ge := Genv.globalenv p in 
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 729814e..7d805c3 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -23,7 +23,7 @@ Require Cminor.
   [Elet] construct.
 
   Unlike in Cminor (the next intermediate language of the back-end),
-  Csharpminor local variables reside in memory, and their address can
+  Csharpminor local variables reside in memory, and their addresses can
   be taken using [Eaddrof] expressions.
 *)
 
@@ -37,9 +37,9 @@ Definition binary_operation : Set := Cminor.binary_operation.
 Inductive expr : Set :=
   | Evar : ident -> expr                (**r reading a scalar variable  *)
   | Eaddrof : ident -> expr             (**r taking the address of a variable *)
-  | Econst : constant -> expr
-  | Eunop : unary_operation -> expr -> expr
-  | Ebinop : binary_operation -> expr -> expr -> expr
+  | Econst : constant -> expr           (**r constants *)
+  | Eunop : unary_operation -> expr -> expr  (**r unary operation *)
+  | Ebinop : binary_operation -> expr -> expr -> expr (**r binary operation *)
   | Eload : memory_chunk -> expr -> expr (**r memory read *)
   | Ecall : signature -> expr -> exprlist -> expr (**r function call *)
   | Econdition : expr -> expr -> expr -> expr (**r conditional expression *)
@@ -138,10 +138,12 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat))
 
 (** Four kinds of evaluation environments are involved:
 - [genv]: global environments, define symbols and functions;
-- [gvarenv]: map global variables to var info;
-- [env]: local environments, map local variables to memory blocks + var info;
+- [gvarenv]: map global variables to variable informations (type [var_kind]);
+- [env]: local environments, map local variables 
+    to memory blocks and variable informations;
 - [lenv]: let environments, map de Bruijn indices to values.
 *)
+
 Definition genv := Genv.t fundef.
 Definition gvarenv := PTree.t var_kind.
 Definition env := PTree.t (block * var_kind).
@@ -250,11 +252,12 @@ Inductive eval_var_ref: env -> ident -> block -> memory_chunk -> Prop :=
       PTree.get id (global_var_env prg) = Some (Vscalar chunk) ->
       eval_var_ref e id b chunk.
 
-(** Evaluation of an expression: [eval_expr prg le e m a m' v] states
+(** Evaluation of an expression: [eval_expr prg le e m a t m' v] states
   that expression [a], in initial memory state [m], evaluates to value
   [v].  [m'] is the final memory state, respectively, reflecting
-  memory stores possibly performed by [a].  [e] and [le] are the
-  local environment and let environment respectively. *)
+  memory stores possibly performed by [a].  [t] is the trace of input/output
+  events generated during the evaluation.
+  [e] and [le] are the local environment and let environment respectively. *)
 
 Inductive eval_expr:
          letenv -> env ->
@@ -329,7 +332,7 @@ Inductive eval_expr:
       eval_expr le e m (Ealloc a) t m2 (Vptr b Int.zero)
 
 (** Evaluation of a list of expressions:
-  [eval_exprlist prg le al m a m' vl]
+  [eval_exprlist prg le al m a t m' vl]
   states that the list [al] of expressions evaluate 
   to the list [vl] of values.
   The other parameters are as in [eval_expr].
@@ -349,7 +352,7 @@ with eval_exprlist:
       t = t1 ** t2 ->
       eval_exprlist le e m (Econs a bl) t m2 (v :: vl)
 
-(** Evaluation of a function invocation: [eval_funcall prg m f args m' res]
+(** Evaluation of a function invocation: [eval_funcall prg m f args t m' res]
   means that the function [f], applied to the arguments [args] in
   memory state [m], returns the value [res] in modified memory state [m'].
 *)
@@ -369,7 +372,7 @@ with eval_funcall:
       event_match ef vargs t vres ->
       eval_funcall m (External ef) vargs t m vres
 
-(** Execution of a statement: [exec_stmt prg e m s m' out]
+(** Execution of a statement: [exec_stmt prg e m s t m' out]
   means that statement [s] executes with outcome [out].
   The other parameters are as in [eval_expr]. *)
 
@@ -460,9 +463,10 @@ Scheme eval_expr_ind4 := Minimality for eval_expr Sort Prop
 
 End RELSEM.
 
-(** Execution of a whole program: [exec_program p r]
+(** Execution of a whole program: [exec_program p t r]
   holds if the application of [p]'s main function to no arguments
-  in the initial memory state for [p] eventually returns value [r]. *)
+  in the initial memory state for [p] performs the events described
+  in trace [t] and eventually returns value [r]. *)
 
 Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
   let ge := Genv.globalenv p in
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 5ab685d..937ea78 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -1,3 +1,13 @@
+(** Translation from Clight to Csharpminor. *)
+
+(** The main transformations performed by this first part are:
+- Resolution of all type-dependent behaviours: overloaded operators
+   are resolved, address computations for array and struct accesses
+   are made explicit, etc.
+- Translation of Clight's loops and [switch] statements into
+   Csharpminor's simpler control structures.
+*)
+
 Require Import Coqlib.
 Require Import Errors.
 Require Import Integers.
@@ -10,7 +20,7 @@ Require Import Csharpminor.
 Open Local Scope string_scope.
 Open Local Scope error_monad_scope.
 
-(** ** Operations on C types *)
+(** * Operations on C types *)
 
 Definition signature_of_function (f: Csyntax.function) : signature :=
   mksignature 
@@ -23,6 +33,9 @@ Definition chunk_of_type (ty: type): res memory_chunk :=
   | _ => Error (msg "Cshmgen.chunk_of_type")
   end.
 
+(** [var_kind_of_type ty] returns the Csharpminor ``variable kind''
+  (scalar or array) that corresponds to the given Clight type [ty]. *)
+
 Definition var_kind_of_type (ty: type): res var_kind :=
   match ty with
   | Tint I8 Signed => OK(Vscalar Mint8signed)
@@ -41,14 +54,14 @@ Definition var_kind_of_type (ty: type): res var_kind :=
   | Tcomp_ptr _ => OK(Vscalar Mint32)
 end.
   
-(** ** Csharpminor constructors *)
+(** * Csharpminor constructors *)
 
-(* The following functions build Csharpminor expressions that compute
+(** The following functions build Csharpminor expressions that compute
    the value of a C operation.  Most construction functions take
    as arguments
-   - Csharpminor subexpressions that compute the values of the
+-  Csharpminor subexpressions that compute the values of the
      arguments of the operation;
-   - The C types of the arguments of the operation.  These types
+-  The C types of the arguments of the operation.  These types
      are used to insert the necessary numeric conversions and to
      resolve operation overloading.
    Most of these functions return an [option expr], with [None] 
@@ -65,11 +78,11 @@ Definition make_floatofint (e: expr) (sg: signedness) :=
   | Unsigned => Eunop Ofloatofintu e
   end.
 
-(* [make_boolean e ty] returns a Csharpminor expression that evaluates
+(** [make_boolean e ty] returns a Csharpminor expression that evaluates
    to the boolean value of [e].  Recall that:
-     - in Csharpminor, [false] is the integer 0,
+-  in Csharpminor, [false] is the integer 0,
        [true] any non-zero integer or any pointer
-     - in C, [false] is the integer 0, the null pointer, the float 0.0
+-  in C, [false] is the integer 0, the null pointer, the float 0.0
        [true] is any non-zero integer, non-null pointer, non-null float.
 *)
 Definition make_boolean (e: expr) (ty: type) :=
@@ -186,11 +199,12 @@ Definition make_orbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
        (make_intconst Int.one)
        (make_intconst Int.zero)).
 
-(* [make_cast from to e] applies to [e] the numeric conversions needed
+(** [make_cast from to e] applies to [e] the numeric conversions needed
    to transform a result of type [from] to a result of type [to].
    It is decomposed in two functions:
-   - [make_cast1]  converts between int/pointer and float if necessary
-   - [make_cast2]  converts to a "smaller" int or float type if necessary.
+-  [make_cast1]  converts between integer and pointers, on one side,
+     and floats on the other side.
+-  [make_cast2]  converts to a "smaller" int or float type if necessary.
 *)
 
 Definition make_cast1 (from to: type) (e: expr) :=
@@ -213,7 +227,7 @@ Definition make_cast2 (from to: type) (e: expr) :=
 Definition make_cast (from to: type) (e: expr) :=
   make_cast2 from to (make_cast1 from to e).
 
-(* [make_load addr ty_res] loads a value of type [ty_res] from
+(** [make_load addr ty_res] loads a value of type [ty_res] from
    the memory location denoted by the Csharpminor expression [addr].
    If [ty_res] is an array or function type, returns [addr] instead,
    as consistent with C semantics.
@@ -226,7 +240,7 @@ Definition make_load (addr: expr) (ty_res: type) :=
   | By_nothing => Error (msg "Cshmgen.make_load")
   end.
 
-(* [make_store addr ty_res rhs ty_rhs] stores the value of the
+(** [make_store addr ty_res rhs ty_rhs] stores the value of the
    Csharpminor expression [rhs] into the memory location denoted by the
    Csharpminor expression [addr].  
    [ty] is the type of the memory location. *)
@@ -237,12 +251,12 @@ Definition make_store (addr: expr) (ty: type) (rhs: expr) :=
   | _ => Error (msg "Cshmgen.make_store")
   end.
 
-(** ** Reading and writing variables *)
+(** * Reading and writing variables *)
 
-(* [var_get id ty] builds Csharpminor code that evaluates to the
+(** [var_get id ty] returns Csharpminor code that evaluates to the
    value of C variable [id] with type [ty].  Note that 
    C variables of array or function type evaluate to the address
-   of the corresponding CabsCoq memory block, while variables of other types
+   of the corresponding Clight memory block, while variables of other types
    evaluate to the contents of the corresponding C memory block.
 *)
 
@@ -253,8 +267,8 @@ Definition var_get (id: ident) (ty: type) :=
   | _ => Error (MSG "Cshmgen.var_get " :: CTX id :: nil)
   end.
 
-(* [var_set id ty rhs] stores the value of the Csharpminor
-   expression [rhs] into the CabsCoq variable [id] of type [ty].
+(** Likewise, [var_set id ty rhs] stores the value of the Csharpminor
+   expression [rhs] into the Clight variable [id] of type [ty].
 *)
 
 Definition var_set (id: ident) (ty: type) (rhs: expr) :=
@@ -263,7 +277,7 @@ Definition var_set (id: ident) (ty: type) (rhs: expr) :=
   | _ => Error (MSG "Cshmgen.var_set " :: CTX id :: nil)
   end.
 
-(** ** Translation of operators *)
+(** * Translation of operators *)
 
 Definition transl_unop (op: Csyntax.unary_operation) (a: expr) (ta: type) : res expr :=
   match op with
@@ -294,16 +308,18 @@ Definition transl_binop (op: Csyntax.binary_operation)
   | Csyntax.Oge => make_cmp Cge a ta b tb
   end.
 
-(** ** Translation of expressions *)
+(** * Translation of expressions *)
 
-(* [transl_expr a] returns the Csharpminor code that computes the value
-   of expression [a]. The result is an option type to enable error reporting.
+(** [transl_expr a] returns the Csharpminor code that computes the value
+   of expression [a]. The computation is performed in the error monad
+   (see module [Errors]) to enable error reporting.
 
    Most cases are self-explanatory.  We outline the non-obvious cases:
-
+<<
    a && b    --->    a ? (b ? 1 : 0) : 0
 
    a || b    --->    a ? 1 : (b ? 1 : 0)
+>>
 *)
 
 Fixpoint transl_expr (a: Csyntax.expr) {struct a} : res expr :=
@@ -369,7 +385,7 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : res expr :=
       end
   end
 
-(* [transl_lvalue a] returns the Csharpminor code that evaluates
+(** [transl_lvalue a] returns the Csharpminor code that evaluates
    [a] as a lvalue, that is, code that returns the memory address
    where the value of [a] is stored.
 *)
@@ -399,7 +415,7 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : res expr :=
       Error(msg "Cshmgen.transl_lvalue")
   end
 
-(* [transl_exprlist al] returns a list of Csharpminor expressions
+(** [transl_exprlist al] returns a list of Csharpminor expressions
    that compute the values of the list [al] of Csyntax expressions.
    Used for function applications. *)
 
@@ -412,7 +428,7 @@ with transl_exprlist (al: Csyntax.exprlist): res exprlist :=
       OK (Econs ta1 ta2)
   end.
 
-(** ** Translation of statements *)
+(** * Translation of statements *)
 
 (** Determine if a C expression is a variable *)
 
@@ -422,10 +438,11 @@ Definition is_variable (e: Csyntax.expr) : option ident :=
   | _ => None
   end.
 
-(* [exit_if_false e] return the statement that tests the boolean
-   value of the CabsCoq expression [e] and performs an [exit 0] if [e]
-   evaluates to false.
-*)
+(** [exit_if_false e] return the statement that tests the boolean
+   value of the Clight expression [e].  If [e] evaluates to false,
+   an [exit 0] is performed.  If [e] evaluates to true, the generated
+   statement continues in sequence. *)
+
 Definition exit_if_false (e: Csyntax.expr) : res stmt :=
   do te <- transl_expr e;
   OK(Sifthenelse
@@ -433,7 +450,7 @@ Definition exit_if_false (e: Csyntax.expr) : res stmt :=
         Sskip
         (Sexit 0%nat)).
 
-(* [transl_statement nbrk ncnt s] returns a Csharpminor statement
+(** [transl_statement nbrk ncnt s] returns a Csharpminor statement
    that performs the same computations as the CabsCoq statement [s].
 
    If the statement [s] terminates prematurely on a [break] construct,
@@ -444,11 +461,8 @@ Definition exit_if_false (e: Csyntax.expr) : res stmt :=
    construct, the generated Csharpminor statement terminates
    prematurely on an [exit ncnt] construct.
 
-   Immediately within a loop, [nbrk = 1] and [ncnt = 0], but this 
-   changes when we're inside a [switch] construct.
-
    The general translation for loops is as follows:
-
+<<
 while (e1) s;       --->     block {
                                loop {
                                  if (!e1) exit 0;
@@ -477,13 +491,19 @@ for (e1;e2;e3) s;   --->     e1;
                                }
                              }
                              // break in s branches here
-
+>>
+   For [switch] statements, we wrap the statements associated with
+   the various cases in a cascade of nested Csharpminor blocks.
+   The multi-way branch is performed by a Csharpminor [switch]
+   statement that exits to the appropriate case.  For instance:
+<<
 switch (e) {        --->    block { block { block { block {
   case N1: s1;                switch (e) { N1: exit 0; N2: exit 1; default: exit 2; }
   case N2: s2;                } ; s1  // with break -> exit 2  and continue -> exit 3
   default: s;                 } ; s2  // with break -> exit 1  and continue -> exit 2
 }                             } ; s   // with break -> exit 0  and continue -> exit 1
                               }
+>>
 *)
 
 Fixpoint switch_table (sl: labeled_statements) (k: nat) {struct sl} : list (int * nat) :=
@@ -559,7 +579,7 @@ with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt)
       transl_lblstmts (pred nbrk) (pred ncnt) rem (Sblock (Sseq body ts))
   end.
 
-(*** Translation of functions *)
+(** * Translation of functions and programs *)
 
 Definition prefix_var_name (id: ident) : errmsg :=
   MSG "In local variable " :: CTX id :: MSG ":\n" :: nil.
@@ -583,8 +603,6 @@ Definition transl_fundef (f: Csyntax.fundef) : res fundef :=
       OK(AST.External (external_function id args res))
   end.
 
-(** ** Translation of programs *)
-
 Definition transl_globvar (ty: type) := var_kind_of_type ty.
 
 Definition transl_program (p: Csyntax.program) : res program :=
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index 7ffd156..b86b09b 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -17,7 +17,7 @@ Require Import Cminor.
 Require Import Csharpminor.
 Require Import Cshmgen.
 
-(** Operations on types *)
+(** * Properties of operations over types *)
 
 Lemma transl_fundef_sig1:
   forall f tf args res,
@@ -65,7 +65,7 @@ Proof.
   simpl; intro EQ; inversion EQ; subst vk; auto.
 Qed.
 
-(** ** Some properties of the translation functions *)
+(** * Properties of the translation functions *)
 
 Lemma map_partial_names:
   forall (A B: Set) (f: A -> res B)
@@ -162,7 +162,7 @@ Proof.
   reflexivity.
 Qed.
 
-(** Transformation of expressions and statements *)
+(** Transformation of expressions and statements. *)
 
 Lemma is_variable_correct:
   forall a id,
@@ -209,7 +209,7 @@ Proof.
   rewrite EQ1; rewrite EQ0; rewrite EQ2; auto.
 Qed.
 
-(** Properties related to switch constructs *)
+(** Properties related to [switch] constructs. *)
 
 Fixpoint lblstmts_length (sl: labeled_statements) : nat :=
   match sl with
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 8e2ce30..a75621c 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -22,7 +22,7 @@ Section CONSTRUCTORS.
 
 Variable tprog: Csharpminor.program.
 
-(** Properties of the translation of [switch] constructs. *)
+(** * Properties of the translation of [switch] constructs. *)
 
 Lemma transl_lblstmts_exit:
   forall e m1 t m2 sl body n tsl nbrk ncnt,
@@ -57,7 +57,7 @@ Proof.
 Qed.
 
 
-(** Correctness of Csharpminor construction functions *)
+(** * Correctness of Csharpminor construction functions *)
 
 Lemma make_intconst_correct:
   forall n le e m1,
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index c8b9caf..10f48f6 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -67,7 +67,11 @@ Proof.
   assumption.
 Qed.
 
-(** ** Matching between environments *)
+(** * Matching between environments *)
+
+(** In this section, we define a matching relation between
+  a Clight local environment and a Csharpminor local environment,
+  parameterized by an assignment of types to the Clight variables. *)
 
 Definition match_var_kind (ty: type) (vk: var_kind) : Prop :=
   match access_mode ty with
@@ -114,6 +118,10 @@ Proof.
   intros chunk AM. generalize (var_kind_by_value _ _ AM). congruence.
 Qed.
 
+(** The following lemmas establish the [match_env] invariant at
+  the beginning of a function invocation, after allocation of
+  local variables and initialization of the parameters. *)
+
 Lemma match_env_alloc_variables:
   forall e1 m1 vars e2 m2 lb,
   Csem.alloc_variables e1 m1 vars e2 m2 lb ->
@@ -214,6 +222,10 @@ Proof.
   intros. apply A. apply List.in_or_app. auto. 
 Qed.
 
+(** The following lemmas establish the matching property
+  between the global environments constructed at the beginning
+  of program execution. *)
+
 Definition globvarenv 
     (gv: gvarenv)
     (vars: list (ident * list init_data * var_kind)) :=
@@ -290,7 +302,9 @@ Proof.
   unfold transl_program in TRANSL. monadInv TRANSL. auto.
 Qed.
 
-(** ** Variable accessors *)
+(* ** Correctness of variable accessors *)
+
+(** Correctness of the code generated by [var_get]. *)
 
 Lemma var_get_correct:
   forall e m id ty loc ofs v tyenv code te le,
@@ -339,6 +353,8 @@ Proof.
   intros. rewrite H1 in H0; discriminate.
 Qed.
 
+(** Correctness of the code generated by [var_set]. *)
+
 Lemma var_set_correct:
   forall e m id ty m1 loc ofs t1 m2 v t2 m3 tyenv code te rhs, 
   Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) t1 m1 loc ofs ->
@@ -374,9 +390,27 @@ Proof.
   intros. rewrite H1 in H0; discriminate.
 Qed.
 
-(** ** Proof of semantic simulation *)
-
-(** Inductive properties *)
+(** * Proof of semantic simulation *)
+
+(** The proof of semantic preservation for this compiler pass relies
+  on simulation diagrams of the following form:
+<<
+         e, m1, a ------------------- te, m1, ta
+            |                           |
+           t|                           |t
+            |                           |
+            v                           v
+         e, m2, v ------------------- te, m2, v
+>>
+  Left: evaluation of expression [a] in Clight.
+  Right: evaluation of its translation [ta] in Csharpminor.
+  Top (precondition): matching between environments [e], [te], 
+    plus well-typedness of expression [a].
+  Bottom (postcondition): the result values [v] and final memory states [m2]
+    are identical in both evaluations.
+
+  We state these diagrams as the following properties, parameterized
+  by the Clight evaluation. *)
 
 Definition eval_expr_prop 
     (e: Csem.env) (m1: mem) (a: Csyntax.expr) (t: trace) (m2: mem) (v: val) : Prop :=
@@ -442,11 +476,9 @@ Definition eval_funcall_prop
     (TR: transl_fundef f = OK tf),
    Csharpminor.eval_funcall tprog m1 tf params t m2 res.
 
-(*
-Set Printing Depth 100.
-Check (Csem.eval_funcall_ind6 ge eval_expr_prop eval_lvalue_prop
-         eval_exprlist_prop exec_stmt_prop exec_lblstmts_prop eval_funcall_prop).
-*)
+(** The proof of semantic preservation is by induction on the Clight
+  evaluation derivation.  Since this proof is large, we break it
+  into one lemma for each Clight evaluation rule. *)
 
 Lemma transl_Econst_int_correct:
        (forall (e : Csem.env) (m : mem) (i : int) (ty : type),
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 6a5fcf3..3866669 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -1,4 +1,4 @@
-(** * Abstract syntax for the Clight language *)
+(** Abstract syntax for the Clight language *)
 
 Require Import Coqlib.
 Require Import Errors.
@@ -6,9 +6,15 @@ Require Import Integers.
 Require Import Floats.
 Require Import AST.
 
-(** ** Abstract syntax *)
+(** * Abstract syntax *)
 
-(** Types *)
+(** ** Types *)
+
+(** Clight types are similar to those of C.  They include numeric types,
+  pointers, arrays, function types, and composite types (struct and 
+  union).  Numeric types (integers and floats) fully specify the
+  bit size of the type.  An integer type is a pair of a signed/unsigned
+  flag and a bit size: 8, 16 or 32 bits. *)
 
 Inductive signedness : Set :=
   | Signed: signedness
@@ -19,20 +25,58 @@ Inductive intsize : Set :=
   | I16: intsize
   | I32: intsize.
 
+(** Float types come in two sizes: 32 bits (single precision)
+  and 64-bit (double precision). *)
+
 Inductive floatsize : Set :=
   | F32: floatsize
   | F64: floatsize.
 
+(** The syntax of type expressions.  Some points to note:
+- Array types [Tarray n] carry the size [n] of the array.
+  Arrays with unknown sizes are represented by pointer types.
+- Function types [Tfunction targs tres] specify the number and types
+  of the function arguments (list [targs]), and the type of the
+  function result ([tres]).  Variadic functions and old-style unprototyped
+  functions are not supported.
+- In C, struct and union types are named and compared by name.
+  This enables the definition of recursive struct types such as
+<<
+  struct s1 { int n; struct * s1 next; };
+>>
+  Note that recursion within types must go through a pointer type.
+  For instance, the following is not allowed in C.
+<<
+  struct s2 { int n; struct s2 next; };
+>>
+  In Clight, struct and union types [Tstruct id fields] and
+  [Tunion id fields] are compared by structure: the [fields]
+  argument gives the names and types of the members.  The identifier
+  [id] is a local name which can be used in conjuction with the
+  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr id]
+  stands for a pointer type to the nearest enclosing [Tstruct]
+  or [Tunion] type named [id].  For instance. the structure [s1]
+  defined above in C is expressed by
+<<
+  Tstruct "s1" (Fcons "n" (Tint I32 Signed)
+               (Fcons "next" (Tcomp_ptr "id")
+               Fnil))
+>>
+  Note that the incorrect structure [s2] above cannot be expressed at
+  all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing
+  structure or union, but not to the structure or union directly.
+*)
+
 Inductive type : Set :=
-  | Tvoid: type
-  | Tint: intsize -> signedness -> type
-  | Tfloat: floatsize -> type
-  | Tpointer: type -> type
-  | Tarray: type -> Z -> type
-  | Tfunction: typelist -> type -> type
-  | Tstruct: ident -> fieldlist -> type
-  | Tunion: ident ->fieldlist -> type
-  | Tcomp_ptr: ident -> type
+  | Tvoid: type                            (**r the [void] type *)
+  | Tint: intsize -> signedness -> type    (**r integer types *)
+  | Tfloat: floatsize -> type              (**r floating-point types *)
+  | Tpointer: type -> type                 (**r pointer types ([*ty]) *)
+  | Tarray: type -> Z -> type              (**r array types ([ty[len]]) *)
+  | Tfunction: typelist -> type -> type    (**r function types *)
+  | Tstruct: ident -> fieldlist -> type    (**r struct types *)
+  | Tunion: ident -> fieldlist -> type     (**r union types *)
+  | Tcomp_ptr: ident -> type               (**r pointer to named struct or union *)
 
 with typelist : Set :=
   | Tnil: typelist
@@ -42,51 +86,61 @@ with fieldlist : Set :=
   | Fnil: fieldlist
   | Fcons: ident -> type -> fieldlist -> fieldlist.
 
-(** Arithmetic and logical operators *)
+(** ** Expressions *)
+
+(** Arithmetic and logical operators. *)
 
 Inductive unary_operation : Set :=
-  | Onotbool : unary_operation
-  | Onotint : unary_operation
-  | Oneg : unary_operation.
+  | Onotbool : unary_operation          (**r boolean negation ([!] in C) *)
+  | Onotint : unary_operation           (**r integer complement ([~] in C) *)
+  | Oneg : unary_operation.             (**r opposite (unary [-]) *)
 
 Inductive binary_operation : Set :=
-  | Oadd : binary_operation
-  | Osub : binary_operation
-  | Omul : binary_operation
-  | Odiv : binary_operation
-  | Omod : binary_operation
-  | Oand : binary_operation
-  | Oor : binary_operation
-  | Oxor : binary_operation
-  | Oshl : binary_operation
-  | Oshr : binary_operation
-  | Oeq: binary_operation
-  | One: binary_operation
-  | Olt: binary_operation
-  | Ogt: binary_operation
-  | Ole: binary_operation
-  | Oge: binary_operation.
-
-(** Expressions *)
+  | Oadd : binary_operation             (**r addition (binary [+]) *)
+  | Osub : binary_operation             (**r subtraction (binary [-]) *)
+  | Omul : binary_operation             (**r multiplication (binary [*]) *)
+  | Odiv : binary_operation             (**r division ([/]) *)
+  | Omod : binary_operation             (**r remainder ([%]) *)
+  | Oand : binary_operation             (**r bitwise and ([&]) *)
+  | Oor : binary_operation              (**r bitwise or ([|]) *)
+  | Oxor : binary_operation             (**r bitwise xor ([^]) *)
+  | Oshl : binary_operation             (**r left shift ([<<]) *)
+  | Oshr : binary_operation             (**r right shift ([>>]) *)
+  | Oeq: binary_operation               (**r comparison ([==]) *)
+  | One: binary_operation               (**r comparison ([!=]) *)
+  | Olt: binary_operation               (**r comparison ([<]) *)
+  | Ogt: binary_operation               (**r comparison ([>]) *)
+  | Ole: binary_operation               (**r comparison ([<=]) *)
+  | Oge: binary_operation.              (**r comparison ([>=]) *)
+
+(** Clight expressions are a large subset of those of C.
+  The main omissions are string literals and assignment operators
+  ([=], [+=], [++], etc).  In Clight, assignment is a statement,
+  not an expression.  
+
+  All expressions are annotated with their types.  An expression
+  (type [expr]) is therefore a pair of a type and an expression
+  description (type [expr_descr]).
+*)
 
 Inductive expr : Set :=
   | Expr: expr_descr -> type -> expr
 
 with expr_descr : Set :=
-  | Econst_int: int -> expr_descr
-  | Econst_float: float -> expr_descr
-  | Evar: ident -> expr_descr
-  | Ederef: expr -> expr_descr
-  | Eaddrof: expr -> expr_descr
-  | Eunop: unary_operation -> expr -> expr_descr
-  | Ebinop: binary_operation -> expr -> expr -> expr_descr
-  | Ecast: type -> expr -> expr_descr
-  | Eindex: expr -> expr -> expr_descr 
-  | Ecall: expr -> exprlist -> expr_descr 
-  | Eandbool: expr -> expr -> expr_descr
-  | Eorbool: expr -> expr -> expr_descr
-  | Esizeof: type -> expr_descr
-  | Efield: expr -> ident -> expr_descr
+  | Econst_int: int -> expr_descr       (**r integer literal *)
+  | Econst_float: float -> expr_descr   (**r float literal *)
+  | Evar: ident -> expr_descr           (**r variable *)
+  | Ederef: expr -> expr_descr          (**r pointer dereference (unary [*]) *)
+  | Eaddrof: expr -> expr_descr         (**r address-of operator ([&]) *)
+  | Eunop: unary_operation -> expr -> expr_descr  (**r unary operation *)
+  | Ebinop: binary_operation -> expr -> expr -> expr_descr (**r binary operation *)
+  | Ecast: type -> expr -> expr_descr   (**r type cast ([(ty) e]) *)
+  | Eindex: expr -> expr -> expr_descr  (**r array indexing ([e1[e2]]) *)
+  | Ecall: expr -> exprlist -> expr_descr  (**r function call *)
+  | Eandbool: expr -> expr -> expr_descr (**r sequential and ([&&]) *)
+  | Eorbool: expr -> expr -> expr_descr (**r sequential or ([||]) *)
+  | Esizeof: type -> expr_descr         (**r size of a type *)
+  | Efield: expr -> ident -> expr_descr (**r access to a member of a struct or union *)
 
 with exprlist : Set :=
   | Enil: exprlist
@@ -97,27 +151,37 @@ with exprlist : Set :=
 Definition typeof (e: expr) : type :=
   match e with Expr de te => te end.
 
-(** Statements *)
+(** ** Statements *)
+
+(** Clight statements include all C statements except [goto] and labels.
+  Only structured forms of [switch] are supported; moreover,
+  the [default] case must occur last.  Blocks and block-scoped declarations
+  are not supported. *)
 
 Inductive statement : Set :=
-  | Sskip : statement
-  | Sexpr : expr -> statement
-  | Sassign : expr -> expr -> statement
-  | Ssequence : statement -> statement -> statement
-  | Sifthenelse : expr  -> statement -> statement -> statement
-  | Swhile : expr -> statement -> statement
-  | Sdowhile : expr -> statement -> statement
-  | Sfor: statement -> expr -> statement -> statement -> statement
-  | Sbreak : statement
-  | Scontinue : statement
-  | Sreturn : option expr -> statement
-  | Sswitch : expr -> labeled_statements -> statement
-
-with labeled_statements : Set :=
+  | Sskip : statement                   (**r do nothing *)
+  | Sexpr : expr -> statement           (**r evaluate expression for its side-effects *)
+  | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *)
+  | Ssequence : statement -> statement -> statement  (**r sequence *)
+  | Sifthenelse : expr  -> statement -> statement -> statement (**r conditional *)
+  | Swhile : expr -> statement -> statement   (**r [while] loop *)
+  | Sdowhile : expr -> statement -> statement (**r [do] loop *)
+  | Sfor: statement -> expr -> statement -> statement -> statement (**r [for] loop *)
+  | Sbreak : statement                      (**r [break] statement *)
+  | Scontinue : statement                   (**r [continue] statement *)
+  | Sreturn : option expr -> statement      (**r [return] statement *)
+  | Sswitch : expr -> labeled_statements -> statement  (**r [switch] statement *)
+
+with labeled_statements : Set :=            (**r cases of a [switch] *)
   | LSdefault: statement -> labeled_statements
   | LScase: int -> statement -> labeled_statements -> labeled_statements.
 
-(** Function definition *)
+(** ** Functions *)
+
+(** A function definition is composed of its return type ([fn_return]),
+  the names and types of its parameters ([fn_params]), the names
+  and types of its local variables ([fn_vars]), and the body of the
+  function (a statement, [fn_body]). *)
 
 Record function : Set := mkfunction {
   fn_return: type;
@@ -126,17 +190,24 @@ Record function : Set := mkfunction {
   fn_body: statement
 }.
 
+(** Functions can either be defined ([Internal]) or declared as
+  external functions ([External]). *)
+
 Inductive fundef : Set :=
   | Internal: function -> fundef
   | External: ident -> typelist -> type -> fundef.
 
-(** Program *)
+(** ** Programs *)
+
+(** A program is a collection of named functions, plus a collection
+  of named global variables, carrying their types and optional initialization 
+  data.  See module [AST] for more details. *)
 
 Definition program : Set := AST.program fundef type.
 
-(** ** Operations over types *)
+(** * Operations over types *)
 
-(** The type of a function definition *)
+(** The type of a function definition. *)
 
 Fixpoint type_of_params (params: list (ident * type)) : typelist :=
   match params with
@@ -153,7 +224,7 @@ Definition type_of_fundef (f: fundef) : type :=
   | External id args res => Tfunction args res
   end.
 
-(** Natural alignment of a type *)
+(** Natural alignment of a type, in bytes. *)
 
 Fixpoint alignof (t: type) : Z :=
   match t with
@@ -198,7 +269,7 @@ Proof.
   apply alignof_fields_pos.
 Qed.
 
-(** Size of a type (in bytes) *)
+(** Size of a type, in bytes. *)
 
 Fixpoint sizeof (t: type) : Z :=
   match t with
@@ -250,7 +321,9 @@ Proof.
   generalize (align_le pos (alignof t) (alignof_pos t)). omega.
 Qed.
 
-(** Byte offset for a field in a struct. *)
+(** Byte offset for a field in a struct or union.
+  Field are laid out consecutively, and padding is inserted
+  to align each field to the natural alignment for its type. *)
 
 Open Local Scope string_scope.
 
@@ -267,11 +340,14 @@ Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
 Definition field_offset (id: ident) (fld: fieldlist) : res Z :=
   field_offset_rec id fld 0.
 
-(* Describe how a variable of the given type must be accessed:
-     - by value, i.e. by loading from the address of the variable
-       with the given chunk
-     - by reference, i.e. by just returning the address of the variable
-     - not at all, e.g. the [void] type. *)
+(** The [access_mode] function describes how a variable of the given
+type must be accessed:
+- [By_value ch]: access by value, i.e. by loading from the address
+  of the variable using the memory chunk [ch];
+- [By_reference]: access by reference, i.e. by just returning
+  the address of the variable;
+- [By_nothing]: no access is possible, e.g. for the [void] type.
+*)
 
 Inductive mode: Set :=
   | By_value: memory_chunk -> mode
@@ -296,13 +372,21 @@ Definition access_mode (ty: type) : mode :=
   | Tcomp_ptr _ => By_value Mint32
 end.
 
-(** Classification of arithmetic operations and comparisons *)
+(** Classification of arithmetic operations and comparisons.
+  The following [classify_] functions take as arguments the types
+  of the arguments of an operation.  They return enough information
+  to resolve overloading for this operator applications, such as
+  ``both arguments are floats'', or ``the first is a pointer
+  and the second is an integer''.  These functions are used to resolve
+  overloading both in the dynamic semantics (module [Csem]) and in the
+  compiler (module [Cshmgen]).
+*)
 
 Inductive classify_add_cases : Set :=
-  | add_case_ii: classify_add_cases         (* int , int *)
-  | add_case_ff: classify_add_cases         (* float , float *)
-  | add_case_pi: type -> classify_add_cases (* ptr | array, int *)
-  | add_default: classify_add_cases.        (* other *)
+  | add_case_ii: classify_add_cases         (**r int , int *)
+  | add_case_ff: classify_add_cases         (**r float , float *)
+  | add_case_pi: type -> classify_add_cases (**r ptr or array, int *)
+  | add_default: classify_add_cases.        (**r other *)
 
 Definition classify_add (ty1: type) (ty2: type) :=
   match ty1, ty2 with
@@ -314,11 +398,11 @@ Definition classify_add (ty1: type) (ty2: type) :=
   end.
 
 Inductive classify_sub_cases : Set :=
-  | sub_case_ii: classify_sub_cases          (* int , int *)
-  | sub_case_ff: classify_sub_cases          (* float , float *)
-  | sub_case_pi: type -> classify_sub_cases  (* ptr | array , int *)
-  | sub_case_pp: type -> classify_sub_cases  (* ptr | array , ptr | array *)
-  | sub_default: classify_sub_cases .        (* other *)
+  | sub_case_ii: classify_sub_cases          (**r int , int *)
+  | sub_case_ff: classify_sub_cases          (**r float , float *)
+  | sub_case_pi: type -> classify_sub_cases  (**r ptr or array , int *)
+  | sub_case_pp: type -> classify_sub_cases  (**r ptr or array , ptr or array *)
+  | sub_default: classify_sub_cases .        (**r other *)
 
 Definition classify_sub (ty1: type) (ty2: type) :=
   match ty1, ty2 with
@@ -334,9 +418,9 @@ Definition classify_sub (ty1: type) (ty2: type) :=
   end.
 
 Inductive classify_mul_cases : Set:=
-  | mul_case_ii: classify_mul_cases (* int , int *)
-  | mul_case_ff: classify_mul_cases (* float , float *)
-  | mul_default: classify_mul_cases . (* other *)
+  | mul_case_ii: classify_mul_cases (**r int , int *)
+  | mul_case_ff: classify_mul_cases (**r float , float *)
+  | mul_default: classify_mul_cases . (**r other *)
 
 Definition classify_mul (ty1: type) (ty2: type) :=
   match ty1,ty2 with
@@ -346,10 +430,10 @@ Definition classify_mul (ty1: type) (ty2: type) :=
 end.
 
 Inductive classify_div_cases : Set:=
-  | div_case_I32unsi: classify_div_cases (* uns int32 , int *)
-  | div_case_ii: classify_div_cases    (* int , int *) 
-  | div_case_ff: classify_div_cases    (* float , float *)
-  | div_default: classify_div_cases. (* other *)
+  | div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *)
+  | div_case_ii: classify_div_cases    (**r int , int *) 
+  | div_case_ff: classify_div_cases    (**r float , float *)
+  | div_default: classify_div_cases. (**r other *)
 
 Definition classify_div (ty1: type) (ty2: type) :=
   match ty1,ty2 with 
@@ -361,9 +445,9 @@ Definition classify_div (ty1: type) (ty2: type) :=
 end.
 
 Inductive classify_mod_cases : Set:=
-  | mod_case_I32unsi: classify_mod_cases  (* uns I32 , int *)
-  | mod_case_ii: classify_mod_cases  (* int , int *)
-  | mod_default: classify_mod_cases . (* other *)
+  | mod_case_I32unsi: classify_mod_cases  (**r unsigned I32 , int *)
+  | mod_case_ii: classify_mod_cases  (**r int , int *)
+  | mod_default: classify_mod_cases . (**r other *)
 
 Definition classify_mod (ty1: type) (ty2: type) :=
   match ty1,ty2 with
@@ -374,9 +458,9 @@ Definition classify_mod (ty1: type) (ty2: type) :=
 end .
 
 Inductive classify_shr_cases :Set:=
-  | shr_case_I32unsi:  classify_shr_cases (* uns I32 , int *)
-  | shr_case_ii :classify_shr_cases (* int , int *)
-  | shr_default : classify_shr_cases . (* other *)
+  | shr_case_I32unsi:  classify_shr_cases (**r unsigned I32 , int *)
+  | shr_case_ii :classify_shr_cases (**r int , int *)
+  | shr_default : classify_shr_cases . (**r other *)
 
 Definition classify_shr (ty1: type) (ty2: type) :=
   match ty1,ty2 with
@@ -386,12 +470,12 @@ Definition classify_shr (ty1: type) (ty2: type) :=
   end.
 
 Inductive classify_cmp_cases : Set:=
-  | cmp_case_I32unsi: classify_cmp_cases (* uns I32 , int *)
-  | cmp_case_ii: classify_cmp_cases  (* int , int*)
-  | cmp_case_ff: classify_cmp_cases  (* float , float *)
-  | cmp_case_pi: classify_cmp_cases  (* ptr | array , int *)
-  | cmp_case_pp:classify_cmp_cases   (* ptr | array , ptr | array *)
-  | cmp_default: classify_cmp_cases . (* other *)
+  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
+  | cmp_case_ii: classify_cmp_cases  (**r int , int*)
+  | cmp_case_ff: classify_cmp_cases  (**r float , float *)
+  | cmp_case_pi: classify_cmp_cases  (**r ptr or array , int *)
+  | cmp_case_pp:classify_cmp_cases   (**r ptr or array , ptr or array *)
+  | cmp_default: classify_cmp_cases . (**r other *)
 
 Definition classify_cmp (ty1: type) (ty2: type) :=
   match ty1,ty2 with 
@@ -409,8 +493,8 @@ Definition classify_cmp (ty1: type) (ty2: type) :=
   end.
 
 Inductive classify_fun_cases : Set:=
-  | fun_case_f: typelist -> type -> classify_fun_cases   (* type fun | ptr fun*)
-  | fun_default: classify_fun_cases . (* other *)
+  | fun_case_f: typelist -> type -> classify_fun_cases   (**r (pointer to) function *)
+  | fun_default: classify_fun_cases . (**r other *)
 
 Definition classify_fun (ty: type) :=
   match ty with 
@@ -419,7 +503,8 @@ Definition classify_fun (ty: type) :=
   | _ => fun_default
   end.
 
-(** Mapping between Clight types and Cminor types and external functions *)
+(** Translating Clight types to Cminor types, function signatures,
+  and external functions. *)
 
 Definition typ_of_type (t: type) : AST.typ :=
   match t with
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 0795e1b..cb572c0 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -1,4 +1,4 @@
-(** * Type well-formedness of C programs *)
+(** * Typing constraints on C programs *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -7,11 +7,14 @@ Require Import Csyntax.
 
 (** ** Typing rules *)
 
-(** This ``type system'' is very coarse: we check only the typing properties
+(** We now define a simple, incomplete type system for the Clight language.
+  This ``type system'' is very coarse: we check only the typing properties
   that matter for the translation to be correct.  Essentially,
   we need to check that the types attached to variable references
   match the declaration types for those variables. *)
 
+(** A typing environment maps variable names to their types. *)
+
 Definition typenv := PTree.t type.
 
 Section TYPING.
@@ -165,7 +168,10 @@ Record wt_program (p: program) : Prop :=  mk_wt_program {
     exists targs, type_of_fundef fd = Tfunction targs (Tint I32 Signed)
 }.
 
-(** ** Type-checking algorithm *)
+(* ** Type-checking algorithm *)
+
+(** We now define and prove correct a type-checking algorithm
+  for the type system defined above. *)
 
 Lemma eq_signedness: forall (s1 s2: signedness), {s1=s2} + {s1<>s2}.
 Proof. decide equality. Qed.