Reorganized the development, modularizing away machine-dependent parts.

Started to merge the ARM code generator.
Started to add support for PowerPC/EABI.
Use ocamlbuild to construct executable from Caml files.


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

4 files changed, 1330 insertions, 0 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
new file mode 100644
index 00000000..08e4a536
--- /dev/null
+++ b/driver/Clflags.ml
@@ -0,0 +1,25 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Command-line flags *)
+
+let prepro_options = ref ([]: string list)
+let linker_options = ref ([]: string list)
+let exe_name = ref "a.out"
+let option_flonglong = ref false
+let option_fmadd = ref false
+let option_dclight = ref false
+let option_dasm = ref false
+let option_E = ref false
+let option_S = ref false
+let option_c = ref false
+let option_v = ref false
diff --git a/driver/Compiler.v b/driver/Compiler.v
new file mode 100644
index 00000000..219fcae3
--- /dev/null
+++ b/driver/Compiler.v
@@ -0,0 +1,305 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** The whole compiler and its proof of semantic preservation *)
+
+(** Libraries. *)
+Require Import Coqlib.
+Require Import Maps.
+Require Import Errors.
+Require Import AST.
+Require Import Values.
+Require Import Smallstep.
+(** Languages (syntax and semantics). *)
+Require Csyntax.
+Require Csem.
+Require Csharpminor.
+Require Cminor.
+Require CminorSel.
+Require RTL.
+Require LTL.
+Require LTLin.
+Require Linear.
+Require Mach.
+Require Asm.
+(** Translation passes. *)
+Require Cshmgen.
+Require Cminorgen.
+Require Selection.
+Require RTLgen.
+Require Constprop.
+Require CSE.
+Require Allocation.
+Require Tunneling.
+Require Linearize.
+Require Reload.
+Require Stacking.
+Require Asmgen.
+(** Type systems. *)
+Require Ctyping.
+Require RTLtyping.
+Require LTLtyping.
+Require LTLintyping.
+Require Lineartyping.
+Require Machtyping.
+(** Proofs of semantic preservation and typing preservation. *)
+Require Cshmgenproof3.
+Require Cminorgenproof.
+Require Selectionproof.
+Require RTLgenproof.
+Require Constpropproof.
+Require CSEproof.
+Require Allocproof.
+Require Alloctyping.
+Require Tunnelingproof.
+Require Tunnelingtyping.
+Require Linearizeproof.
+Require Linearizetyping.
+Require Reloadproof.
+Require Reloadtyping.
+Require Stackingproof.
+Require Stackingtyping.
+Require Machabstr2concr.
+Require Asmgenproof.
+
+Open Local Scope string_scope.
+
+(** * Composing the translation passes *)
+
+(** We first define useful monadic composition operators,
+    along with funny (but convenient) notations. *)
+
+Definition apply_total (A B: Set) (x: res A) (f: A -> B) : res B :=
+  match x with Error msg => Error msg | OK x1 => OK (f x1) end.
+
+Definition apply_partial (A B: Set)
+                         (x: res A) (f: A -> res B) : res B :=
+  match x with Error msg => Error msg | OK x1 => f x1 end.
+
+Notation "a @@@ b" :=
+   (apply_partial _ _ a b) (at level 50, left associativity).
+Notation "a @@ b" :=
+   (apply_total _ _ a b) (at level 50, left associativity).
+
+(** We define three translation functions for whole programs: one
+  starting with a C program, one with a Cminor program, one with an
+  RTL program.  The three translations produce Asm programs ready for
+  pretty-printing and assembling.
+
+  There are two ways to compose the compiler passes.  The first
+  translates every function from the Cminor program from Cminor to
+  RTL, then to LTL, etc, all the way to Asm, and iterates this
+  transformation for every function.  The second translates the whole
+  Cminor program to a RTL program, then to an LTL program, etc. 
+  Between Cminor and Asm, we follow the first approach because it has
+  lower memory requirements.  The translation from Clight to Asm
+  follows the second approach.
+  
+  The translation of an RTL function to an Asm function is as follows. *)
+
+Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef :=
+   OK f
+   @@ Constprop.transf_fundef
+   @@ CSE.transf_fundef
+  @@@ Allocation.transf_fundef
+   @@ Tunneling.tunnel_fundef
+  @@@ Linearize.transf_fundef
+   @@ Reload.transf_fundef
+  @@@ Stacking.transf_fundef
+  @@@ Asmgen.transf_fundef.
+
+(* Here is the translation of a Cminor function to an Asm function. *)
+
+Definition transf_cminor_fundef (f: Cminor.fundef) : res Asm.fundef :=
+  OK f
+   @@ Selection.sel_fundef
+  @@@ RTLgen.transl_fundef
+  @@@ transf_rtl_fundef.
+
+(** The corresponding translations for whole program follow. *)
+
+Definition transf_rtl_program (p: RTL.program) : res Asm.program :=
+  transform_partial_program transf_rtl_fundef p.
+
+Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
+  transform_partial_program transf_cminor_fundef p.
+
+Definition transf_c_program (p: Csyntax.program) : res Asm.program :=
+  match Ctyping.typecheck_program p with
+  | false =>
+      Error (msg "Ctyping: type error")
+  | true =>
+      OK p 
+      @@@ Cshmgen.transl_program
+      @@@ Cminorgen.transl_program
+      @@@ transf_cminor_program
+  end.
+
+(** The following lemmas help reason over compositions of passes. *)
+
+Lemma map_partial_compose:
+  forall (X A B C: Set)
+         (ctx: X -> errmsg)
+         (f1: A -> res B) (f2: B -> res C)
+         (pa: list (X * A)) (pc: list (X * C)),
+  map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc ->
+  exists pb, map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc.
+Proof.
+  induction pa; simpl.
+  intros. inv H. econstructor; eauto.
+  intro pc. destruct a as [x a].
+  caseEq (f1 a); simpl; try congruence. intros b F1.
+  caseEq (f2 b); simpl; try congruence. intros c F2 EQ.
+  monadInv EQ. exploit IHpa; eauto. intros [pb [P Q]]. 
+  rewrite P; simpl.
+  exists ((x, b) :: pb); split. auto. simpl. rewrite F2. rewrite Q. auto. 
+Qed.
+
+Lemma transform_partial_program_compose:
+  forall (A B C V: Set)
+         (f1: A -> res B) (f2: B -> res C)
+         (pa: program A V) (pc: program C V),
+  transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc ->
+  exists pb, transform_partial_program f1 pa = OK pb /\
+             transform_partial_program f2 pb = OK pc.
+Proof.
+  intros. monadInv H. 
+  exploit map_partial_compose; eauto. intros [xb [P Q]].
+  exists (mkprogram xb (prog_main pa) (prog_vars pa)); split.
+  unfold transform_partial_program. rewrite P; auto. 
+  unfold transform_partial_program. simpl. rewrite Q; auto.
+Qed.
+
+Lemma transform_program_partial_program:
+  forall (A B V: Set) (f: A -> B) (p: program A V) (tp: program B V),
+  transform_partial_program (fun x => OK (f x)) p = OK tp ->
+  transform_program f p = tp.
+Proof.
+  intros until tp. unfold transform_partial_program. 
+  rewrite map_partial_total. simpl. intros. inv H. auto. 
+Qed.
+
+Lemma transform_program_compose:
+  forall (A B C V: Set)
+         (f1: A -> res B) (f2: B -> C)
+         (pa: program A V) (pc: program C V),
+  transform_partial_program (fun f => f1 f @@ f2) pa = OK pc ->
+  exists pb, transform_partial_program f1 pa = OK pb /\
+             transform_program f2 pb = pc.
+Proof.
+  intros. 
+  replace (fun f : A => f1 f @@ f2)
+     with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H.
+  exploit transform_partial_program_compose; eauto.
+  intros [pb [X Y]]. exists pb; split. auto. 
+  apply transform_program_partial_program. auto. 
+  apply extensionality; intro. destruct(f1 x); auto. 
+Qed.
+
+Lemma transform_partial_program_identity:
+  forall (A V: Set) (pa pb: program A V),
+  transform_partial_program (@OK A) pa = OK pb ->
+  pa = pb.
+Proof.
+  intros until pb. unfold transform_partial_program. 
+  replace (@OK A) with (fun b => @OK A b).
+  rewrite map_partial_identity. simpl. destruct pa; simpl; congruence.
+  apply extensionality; auto. 
+Qed.
+
+(** * Semantic preservation *)
+
+(** We prove that the [transf_program] translations preserve semantics.
+  The proof composes the semantic preservation results for each pass.
+  This establishes the correctness of the whole compiler! *)
+
+Theorem transf_rtl_program_correct:
+  forall p tp beh,
+  transf_rtl_program p = OK tp ->
+  RTL.exec_program p beh ->
+  Asm.exec_program tp beh.
+Proof.
+  intros. unfold transf_rtl_program, transf_rtl_fundef in H.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p7 [H7 P7]].
+  clear H.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H7) as [p6 [H6 P6]].
+  clear H7.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H6) as [p5 [H5 P5]].
+  clear H6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H5) as [p4 [H4 P4]].
+  clear H5.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H4) as [p3 [H3 P3]].
+  clear H4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]].
+  clear H3.
+  destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]].
+  clear H2.
+  destruct (transform_program_compose _ _ _ _ _ _ _ _ H1) as [p0 [H00 P0]].
+  clear H1.
+  generalize (transform_partial_program_identity _ _ _ _ H00). clear H00. intro. subst p0.
+
+  assert (WT3 : LTLtyping.wt_program p3).
+    apply Alloctyping.program_typing_preserved with p2. auto.
+  assert (WT4 : LTLtyping.wt_program p4).
+    subst p4. apply Tunnelingtyping.program_typing_preserved. auto.
+  assert (WT5 : LTLintyping.wt_program p5).
+    apply Linearizetyping.program_typing_preserved with p4. auto. auto.
+  assert (WT6 : Lineartyping.wt_program p6).
+    subst p6. apply Reloadtyping.program_typing_preserved. auto.
+  assert (WT7: Machtyping.wt_program p7).
+    apply Stackingtyping.program_typing_preserved with p6. auto. auto.
+
+  apply Asmgenproof.transf_program_correct with p7; auto.
+  apply Machabstr2concr.exec_program_equiv; auto.
+  apply Stackingproof.transf_program_correct with p6; auto.
+  subst p6; apply Reloadproof.transf_program_correct; auto.
+  apply Linearizeproof.transf_program_correct with p4; auto.
+  subst p4; apply Tunnelingproof.transf_program_correct. 
+  apply Allocproof.transf_program_correct with p2; auto.
+  subst p2; apply CSEproof.transf_program_correct.
+  subst p1; apply Constpropproof.transf_program_correct. auto.
+Qed.
+
+Theorem transf_cminor_program_correct:
+  forall p tp beh,
+  transf_cminor_program p = OK tp ->
+  Cminor.exec_program p beh ->
+  Asm.exec_program tp beh.
+Proof.
+  intros. unfold transf_cminor_program, transf_cminor_fundef in H.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [H3 P3]].
+  clear H.
+  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]].
+  clear H3.
+  destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]].
+  generalize (transform_partial_program_identity _ _ _ _ H1). clear H1. intro. subst p1.
+  apply transf_rtl_program_correct with p3. auto.
+  apply RTLgenproof.transf_program_correct with p2; auto.
+  rewrite <- P1. apply Selectionproof.transf_program_correct; auto.
+Qed.
+
+Theorem transf_c_program_correct:
+  forall p tp beh,
+  transf_c_program p = OK tp ->
+  Csem.exec_program p beh ->
+  Asm.exec_program tp beh.
+Proof.
+  intros until beh; unfold transf_c_program; simpl.
+  caseEq (Ctyping.typecheck_program p); try congruence; intro.
+  caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1.
+  caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. 
+  intros EQ3 SEM.
+  eapply transf_cminor_program_correct; eauto.
+  eapply Cminorgenproof.transl_program_correct; eauto. 
+  eapply Cshmgenproof3.transl_program_correct; eauto.
+  apply Ctyping.typecheck_program_correct; auto.
+Qed.
diff --git a/driver/Complements.v b/driver/Complements.v
new file mode 100644
index 00000000..fc2fa533
--- /dev/null
+++ b/driver/Complements.v
@@ -0,0 +1,648 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Corollaries of the main semantic preservation theorem. *)
+
+Require Import Classical.
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Events.
+Require Import Globalenvs.
+Require Import Smallstep.
+Require Import Csyntax.
+Require Import Csem.
+Require Import Asm.
+Require Import Compiler.
+Require Import Errors.
+
+(** * Determinism of Asm semantics *)
+
+(** In this section, we show that the semantics for the Asm language
+  are deterministic, in a sense to be made precise later.
+  There are two sources of apparent non-determinism:
+- The semantics leaves unspecified the results of calls to external 
+  functions.  Different results to e.g. a "read" operation can of
+  course lead to different behaviors for the program.
+  We address this issue by modeling a notion of deterministic
+  external world that uniquely determines the results of external calls.
+- For diverging executions, the trace of I/O events is not uniquely
+  determined: it can contain events that will never be performed
+  because the program diverges earlier.  We address this issue
+  by showing the existence of a minimal trace for diverging executions.
+
+*)
+
+(** ** Deterministic worlds *)
+
+(** An external world is a function that, given the name of an
+  external call and its arguments, returns either [None], meaning
+  that this external call gets stuck, or [Some(r,w)], meaning
+  that this external call succeeds, has result [r], and changes
+  the world to [w]. *)
+
+Inductive world: Set :=
+  World: (ident -> list eventval -> option (eventval * world)) -> world.
+
+Definition nextworld (w: world) (evname: ident) (evargs: list eventval) :
+                     option (eventval * world) :=
+  match w with World f => f evname evargs end.
+
+(** A trace is possible in a given world if all events correspond
+  to non-stuck external calls according to the given world.
+  Two predicates are defined, for finite and infinite traces respectively:
+- [possible_trace w t w'], where [w] is the initial state of the
+  world, [t] the finite trace of interest, and [w'] the state of the
+  world after performing trace [t].
+- [possible_traceinf w T], where [w] is the initial state of the
+  world and [T] the possibly infinite trace of interest.
+*)
+
+Inductive possible_trace: world -> trace -> world -> Prop :=
+  | possible_trace_nil: forall w,
+      possible_trace w E0 w
+  | possible_trace_cons: forall w0 evname evargs evres w1 t w2,
+      nextworld w0 evname evargs = Some (evres, w1) ->
+      possible_trace w1 t w2 ->
+      possible_trace w0 (mkevent evname evargs evres :: t) w2.
+
+Lemma possible_trace_app:
+  forall t2 w2 w0 t1 w1,
+  possible_trace w0 t1 w1 -> possible_trace w1 t2 w2 ->
+  possible_trace w0 (t1 ** t2) w2.
+Proof.
+  induction 1; simpl; intros.
+  auto.
+  econstructor; eauto.
+Qed.
+
+Lemma possible_trace_app_inv:
+  forall t2 w2 t1 w0,
+  possible_trace w0 (t1 ** t2) w2 ->
+  exists w1, possible_trace w0 t1 w1 /\ possible_trace w1 t2 w2.
+Proof.
+  induction t1; simpl; intros.
+  exists w0; split. constructor. auto.
+  inv H. exploit IHt1; eauto. intros [w1 [A B]]. 
+  exists w1; split. econstructor; eauto. auto.
+Qed.
+
+CoInductive possible_traceinf: world -> traceinf -> Prop :=
+  | possible_traceinf_nil: forall w0,
+      possible_traceinf w0 Enilinf
+  | possible_traceinf_cons: forall w0 evname evargs evres w1 T,
+      nextworld w0 evname evargs = Some (evres, w1) ->
+      possible_traceinf w1 T ->
+      possible_traceinf w0 (Econsinf (mkevent evname evargs evres) T).
+
+Lemma possible_traceinf_app:
+  forall t2 w0 t1 w1,
+  possible_trace w0 t1 w1 -> possible_traceinf w1 t2 ->
+  possible_traceinf w0 (t1 *** t2).
+Proof.
+  induction 1; simpl; intros.
+  auto.
+  econstructor; eauto.
+Qed.
+
+Lemma possible_traceinf_app_inv:
+  forall t2 t1 w0,
+  possible_traceinf w0 (t1 *** t2) ->
+  exists w1, possible_trace w0 t1 w1 /\ possible_traceinf w1 t2.
+Proof.
+  induction t1; simpl; intros.
+  exists w0; split. constructor. auto.
+  inv H. exploit IHt1; eauto. intros [w1 [A B]]. 
+  exists w1; split. econstructor; eauto. auto.
+Qed.
+
+Ltac possibleTraceInv :=
+  match goal with
+  | [H: possible_trace _ (_ ** _) _ |- _] =>
+      let P1 := fresh "P" in
+      let w := fresh "w" in
+      let P2 := fresh "P" in
+      elim (possible_trace_app_inv _ _ _ _ H); clear H;
+      intros w [P1 P2];
+      possibleTraceInv
+  | [H: possible_traceinf _ (_ *** _) |- _] =>
+      let P1 := fresh "P" in
+      let w := fresh "w" in
+      let P2 := fresh "P" in
+      elim (possible_traceinf_app_inv _ _ _ H); clear H;
+      intros w [P1 P2];
+      possibleTraceInv
+  | _ => idtac
+  end.
+
+(** Determinism properties of [event_match]. *)
+
+Remark eventval_match_deterministic:
+  forall ev1 ev2 ty v1 v2,
+  eventval_match ev1 ty v1 -> eventval_match ev2 ty v2 ->
+  (ev1 = ev2 <-> v1 = v2).
+Proof.
+  intros. inv H; inv H0; intuition congruence.
+Qed.
+
+Remark eventval_list_match_deterministic:
+  forall ev1 ty v, eventval_list_match ev1 ty v ->
+  forall ev2, eventval_list_match ev2 ty v -> ev1 = ev2.
+Proof.
+  induction 1; intros.
+  inv H. auto.
+  inv H1. decEq.
+  rewrite (eventval_match_deterministic _ _ _ _ _ H H6). auto.
+  eauto.
+Qed.
+
+Lemma event_match_deterministic:
+  forall w0 t1 w1 t2 w2 ef vargs vres1 vres2,
+  possible_trace w0 t1 w1 ->
+  possible_trace w0 t2 w2 ->
+  event_match ef vargs t1 vres1 ->
+  event_match ef vargs t2 vres2 ->
+  vres1 = vres2 /\ t1 = t2 /\ w1 = w2.
+Proof.
+  intros. inv H1. inv H2. 
+  assert (eargs = eargs0). eapply eventval_list_match_deterministic; eauto. subst eargs0.
+  inv H. inv H12. inv H0. inv H12.
+  rewrite H11 in H10. inv H10. intuition. 
+  rewrite <- (eventval_match_deterministic _ _ _ _ _ H4 H5). auto.
+Qed.
+
+(** ** Determinism of Asm transitions. *)
+
+Remark extcall_arguments_deterministic:
+  forall rs m sg args args',
+  extcall_arguments rs m sg args ->
+  extcall_arguments rs m sg args' -> args = args'.
+Proof.
+  assert (
+    forall rs m ll args,
+    extcall_args rs m ll args ->
+    forall args', extcall_args rs m ll args' -> args = args').
+  induction 1; intros.
+  inv H. auto.
+  inv H1. decEq; eauto.
+  inv H; inv H4; congruence.
+  unfold extcall_arguments; intros; eauto.
+Qed.
+
+Lemma step_deterministic:
+  forall ge s0 t1 s1 t2 s2 w0 w1 w2,
+  step ge s0 t1 s1 -> step ge s0 t2 s2 ->
+  possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
+  s1 = s2 /\ t1 = t2 /\ w1 = w2.
+Proof.
+  intros. inv H; inv H0.
+  assert (c0 = c) by congruence. subst c0.
+  assert (i0 = i) by congruence. subst i0.
+  split. congruence. split. auto. inv H1; inv H2; auto.
+  congruence.
+  congruence.
+  assert (ef0 = ef) by congruence. subst ef0.
+  assert (args0 = args). eapply extcall_arguments_deterministic; eauto. subst args0.
+  exploit event_match_deterministic. eexact H1. eexact H2. eauto. eauto.
+  intros [A [B C]]. intuition congruence.
+Qed.
+
+Lemma initial_state_deterministic:
+  forall p s1 s2,
+  initial_state p s1 -> initial_state p s2 -> s1 = s2.
+Proof.
+  intros. inv H; inv H0. reflexivity. 
+Qed.
+
+Lemma final_state_not_step:
+  forall ge st r t st', final_state st r -> step ge st t st' -> False.
+Proof.
+  intros. inv H. inv H0.
+  unfold Vzero in H1. congruence.
+  unfold Vzero in H1. congruence. 
+Qed.
+
+Lemma final_state_deterministic:
+  forall st r1 r2, final_state st r1 -> final_state st r2 -> r1 = r2.
+Proof.
+  intros. inv H; inv H0. congruence.
+Qed.
+
+(** ** Determinism for terminating executions. *)
+
+(*
+Lemma star_star_inv:
+  forall ge s t1 s1, star step ge s t1 s1 ->
+  forall t2 s2 w w1 w2, star step ge s t2 s2 ->
+  possible_trace w t1 w1 -> possible_trace w t2 w2 ->
+  exists t, (star step ge s1 t s2 /\ t2 = t1 ** t)
+        \/  (star step ge s2 t s1 /\ t1 = t2 ** t).
+Proof.
+  induction 1; intros.
+  exists t2; left; split; auto.
+  inv H2. exists (t1 ** t2); right; split. econstructor; eauto. auto.
+  possibleTraceInv. 
+  exploit step_deterministic. eexact H. eexact H5. eauto. eauto. 
+  intros [U [V W]]. subst s5 t3 w3. 
+  exploit IHstar; eauto. intros [t [ [Q R] | [Q R] ]].
+  subst t4. exists t; left; split. auto. traceEq.
+  subst t2. exists t; right; split. auto. traceEq.
+Qed.
+*)
+
+Lemma steps_deterministic:
+  forall ge s0 t1 s1, star step ge s0 t1 s1 -> 
+  forall r1 r2 t2 s2 w0 w1 w2, star step ge s0 t2 s2 -> 
+  final_state s1 r1 -> final_state s2 r2 ->
+  possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 ->
+  t1 = t2 /\ r1 = r2.
+Proof.
+  induction 1; intros. 
+  inv H. split. auto. eapply final_state_deterministic; eauto.
+  byContradiction. eapply final_state_not_step with (st := s); eauto.
+  inv H2. byContradiction. eapply final_state_not_step with (st := s0); eauto.
+  possibleTraceInv.
+  exploit step_deterministic. eexact H. eexact H7. eauto. eauto. 
+  intros [A [B C]]. subst s5 t3 w3.
+  exploit IHstar. eexact H8. eauto. eauto. eauto. eauto. 
+  intros [A B]. subst t4 r2. 
+  auto.
+Qed.
+
+(** ** Determinism for infinite transition sequences. *)
+
+Lemma forever_star_inv:
+  forall ge s t s', star step ge s t s' ->
+  forall T w w', forever step ge s T ->
+  possible_trace w t w' -> possible_traceinf w T ->
+  exists T',
+  forever step ge s' T' /\ possible_traceinf w' T' /\ T = t *** T'.
+Proof.
+  induction 1; intros.
+  inv H0. exists T; auto.
+  subst t. possibleTraceInv. 
+  inv H2. possibleTraceInv. 
+  exploit step_deterministic.
+    eexact H. eexact H1. eauto. eauto. intros [A [B C]]; subst s4 t1 w1.
+  exploit IHstar; eauto. intros [T' [A [B C]]]. 
+  exists T'; split. auto.
+  split. auto.
+  rewrite C. rewrite Eappinf_assoc; auto.
+Qed.
+
+Lemma star_final_not_forever:
+  forall ge s1 t s2 r T w1 w2,
+  star step ge s1 t s2 ->
+  final_state s2 r -> forever step ge s1 T ->
+  possible_trace w1 t w2 -> possible_traceinf w1 T ->
+  False.
+Proof.
+  intros. exploit forever_star_inv; eauto. intros [T' [A [B C]]]. 
+  inv A. eapply final_state_not_step; eauto.
+Qed.
+
+(** ** Minimal traces for divergence. *)
+
+(** There are two mutually exclusive way in which a program can diverge.
+  It can diverge in a reactive fashion: it performs infinitely many
+  external calls, and the internal computations between two external
+  calls are always finite.  Or it can diverge silently: after a finite
+  number of external calls, it enters an infinite sequence of internal
+  computations. *)
+
+Definition reactive (ge: genv) (s: state) (w: world) :=
+  forall t s1 w1,
+  star step ge s t s1 -> possible_trace w t w1 ->
+  exists s2, exists t', exists s3, exists w2,
+  star step ge s1 E0 s2 
+  /\ step ge s2 t' s3
+  /\ possible_trace w1 t' w2
+  /\ t' <> E0.
+
+Definition diverges_silently (ge: genv) (s: state) :=
+  forall s2, star step ge s E0 s2 -> exists s3, step ge s2 E0 s3.
+
+Definition diverges_eventually (ge: genv) (s: state) (w: world) :=
+  exists t, exists s1, exists w1,
+  star step ge s t s1 /\ possible_trace w t w1 /\ diverges_silently ge s1.
+
+(** Using classical logic, we show that any infinite sequence of transitions
+  that is possible in a deterministic world is of one of the two forms 
+  described above. *)
+
+Lemma reactive_or_diverges:
+  forall ge s T w,
+  forever step ge s T -> possible_traceinf w T ->
+  reactive ge s w \/ diverges_eventually ge s w.
+Proof.
+  intros. elim (classic (diverges_eventually ge s w)); intro.
+  right; auto.
+  left. red; intros.
+  generalize (not_ex_all_not trace _ H1 t).
+  intro. clear H1.
+  generalize (not_ex_all_not state _ H4 s1).
+  intro. clear H4.
+  generalize (not_ex_all_not world _ H1 w1).
+  intro. clear H1.
+  elim (not_and_or _ _ H4); clear H4; intro.
+  contradiction.
+  elim (not_and_or _ _ H1); clear H1; intro.
+  contradiction.
+  generalize (not_all_ex_not state _ H1). intros [s2 A]. clear H1.
+  destruct (imply_to_and _ _ A). clear A.
+  exploit forever_star_inv.
+    eapply star_trans. eexact H2. eexact H1. reflexivity.
+    eauto. rewrite E0_right. eauto. eauto. 
+  intros [T' [A [B C]]]. 
+  inv A. possibleTraceInv. 
+  exists s2; exists t0; exists s3; exists w4. intuition.
+  subst t0. apply H4. exists s3; auto.
+Qed.
+
+(** Moreover, a program cannot be both reactive and silently diverging. *)
+
+Lemma reactive_not_diverges:
+  forall ge s w,
+  reactive ge s w -> diverges_eventually ge s w -> False.
+Proof.
+  intros. destruct H0 as [t [s1 [w1 [A [B C]]]]]. 
+  destruct (H _ _ _ A B) as [s2 [t' [s3 [w2 [P [Q [R S]]]]]]].
+  destruct (C _ P) as [s4 T].
+  assert (s3 = s4 /\ t' = E0 /\ w2 = w1).
+    eapply step_deterministic; eauto. constructor.
+  intuition congruence.
+Qed.
+
+(** A program that silently diverges can be given any finite or
+  infinite trace of events.  In particular, taking [T' = Enilinf],
+  it can be given the empty trace of events. *)
+
+Lemma diverges_forever:
+  forall ge s1 T w T',
+  diverges_silently ge s1 ->
+  forever step ge s1 T ->
+  possible_traceinf w T ->
+  forever step ge s1 T'.
+Proof.
+  cofix COINDHYP; intros. inv H0. possibleTraceInv. 
+  assert (exists s3, step ge s1 E0 s3). apply H. constructor.
+  destruct H0 as [s3 C]. 
+  assert (s2 = s3 /\ t = E0 /\ w0 = w). eapply step_deterministic; eauto. constructor.
+  destruct H0 as [Q [R S]]. subst s3 t w0. 
+  change T' with (E0 *** T'). econstructor. eassumption. 
+  eapply COINDHYP; eauto. 
+  red; intros. apply H. eapply star_left; eauto. 
+Qed.
+
+(** The trace of I/O events generated by a reactive diverging program
+  is uniquely determined up to bisimilarity. *)
+
+Lemma reactive_sim:
+  forall ge s w T1 T2,
+  reactive ge s w ->
+  forever step ge s T1 ->
+  forever step ge s T2 ->
+  possible_traceinf w T1 ->
+  possible_traceinf w T2 ->
+  traceinf_sim T1 T2.
+Proof.
+  cofix COINDHYP; intros.
+  elim (H E0 s w); try constructor. 
+  intros s2 [t' [s3 [w2 [A [B [C D]]]]]].
+  assert (star step ge s t' s3). eapply star_right; eauto. 
+  destruct (forever_star_inv _ _ _ _ H4 _ _ _ H0 C H2)
+  as [T1' [P [Q R]]].
+  destruct (forever_star_inv _ _ _ _ H4 _ _ _ H1 C H3)
+  as [T2' [S [T U]]].
+  destruct t'. unfold E0 in D. congruence.
+  assert (t' = nil). inversion B. inversion H7. auto. subst t'.
+  subst T1 T2. simpl. constructor.
+  apply COINDHYP with ge s3 w2; auto.
+  red; intros. eapply H. eapply star_trans; eauto.
+  eapply possible_trace_app; eauto. 
+Qed.
+
+(** A trace is minimal for a program if it is a prefix of all possible
+  traces. *)
+
+Definition minimal_trace (ge: genv) (s: state) (w: world) (T: traceinf) :=
+  forall T',
+  forever step ge s T' -> possible_traceinf w T' ->
+  traceinf_prefix T T'.
+
+(** For any program that diverges with some possible trace [T1],
+  the set of possible traces admits a minimal element [T].
+  If the program is reactive, this trace is [T1]. 
+  If the program silently diverges, this trace is the finite trace
+  of events performed prior to silent divergence. *)
+
+Lemma forever_minimal_trace:
+  forall ge s T1 w,
+  forever step ge s T1 -> possible_traceinf w T1 ->
+  exists T,
+     forever step ge s T
+  /\ possible_traceinf w T
+  /\ minimal_trace ge s w T.
+Proof.
+  intros. 
+  destruct (reactive_or_diverges _ _ _ _ H H0).
+  (* reactive *)
+  exists T1; split. auto. split. auto. red; intros.
+  elim (reactive_or_diverges _ _ _ _ H2 H3); intro.
+  apply traceinf_sim_prefix. eapply reactive_sim; eauto. 
+  elimtype False. eapply reactive_not_diverges; eauto.
+  (* diverges *) 
+  elim H1. intros t [s1 [w1 [A [B C]]]].
+  exists (t *** Enilinf); split.
+  exploit forever_star_inv; eauto. intros [T' [P [Q R]]]. 
+  eapply star_forever. eauto. 
+  eapply diverges_forever; eauto.
+  split. eapply possible_traceinf_app. eauto. constructor. 
+  red; intros. exploit forever_star_inv. eauto. eexact H2. eauto. eauto.
+  intros [T2 [P [Q R]]].
+  subst T'. apply traceinf_prefix_app. constructor.
+Qed.
+
+(** ** Refined semantics for program executions. *)
+
+(** We now define the following variant [exec_program'] of the
+  [exec_program] predicate defined in module [Smallstep].
+  In the diverging case [Diverges T], the new predicate imposes that the
+  finite or infinite trace [T] is minimal. *)
+
+Inductive exec_program' (p: program) (w: world): program_behavior -> Prop :=
+  | program_terminates': forall s t s' w' r,
+      initial_state p s ->
+      star step (Genv.globalenv p) s t s' ->
+      possible_trace w t w' ->
+      final_state s' r ->
+      exec_program' p w (Terminates t r)
+  | program_diverges': forall s T,
+      initial_state p s ->
+      forever step (Genv.globalenv p) s T ->
+      possible_traceinf w T ->
+      minimal_trace (Genv.globalenv p) s w T ->
+      exec_program' p w (Diverges T).
+
+(** We show that any [exec_program] execution corresponds to
+  an [exec_program'] execution. *)
+
+Definition possible_behavior (w: world) (b: program_behavior) : Prop :=
+  match b with
+  | Terminates t r => exists w', possible_trace w t w'
+  | Diverges T => possible_traceinf w T
+  end.
+
+Inductive matching_behaviors: program_behavior -> program_behavior -> Prop :=
+  | matching_behaviors_terminates: forall t r,
+      matching_behaviors (Terminates t r) (Terminates t r)
+  | matching_behaviors_diverges: forall T1 T2,
+      traceinf_prefix T2 T1 ->
+      matching_behaviors (Diverges T1) (Diverges T2).
+
+Theorem exec_program_program':
+  forall p b w,
+  exec_program p b -> possible_behavior w b ->
+  exists b', exec_program' p w b' /\ matching_behaviors b b'.
+Proof.
+  intros. inv H; simpl in H0.
+  (* termination *)
+  destruct H0 as [w' A].
+  exists (Terminates t r).
+  split. econstructor; eauto. constructor.
+  (* divergence *)
+  exploit forever_minimal_trace; eauto. intros [T0 [A [B C]]].
+  exists (Diverges T0); split.
+  econstructor; eauto.
+  constructor. apply C; auto.
+Qed.
+
+(** Moreover, [exec_program'] is deterministic, in that the behavior
+  associated with a given program and external world is uniquely
+  defined up to bisimilarity between infinite traces. *)
+
+Inductive same_behaviors: program_behavior -> program_behavior -> Prop :=
+  | same_behaviors_terminates: forall t r,
+      same_behaviors (Terminates t r) (Terminates t r)
+  | same_behaviors_diverges: forall T1 T2,
+      traceinf_sim T2 T1 ->
+      same_behaviors (Diverges T1) (Diverges T2).
+
+Theorem exec_program'_deterministic:
+  forall p b1 b2 w,
+  exec_program' p w b1 -> exec_program' p w b2 ->
+  same_behaviors b1 b2.
+Proof.
+  intros. inv H; inv H0;
+  assert (s0 = s) by (eapply initial_state_deterministic; eauto); subst s0.
+  (* terminates, terminates *)
+  exploit steps_deterministic. eexact H2. eexact H5. eauto. eauto. eauto. eauto.
+  intros [A B]. subst. constructor.
+  (* terminates, diverges *)
+  byContradiction. eapply star_final_not_forever; eauto.
+  (* diverges, terminates *)
+  byContradiction. eapply star_final_not_forever; eauto.
+  (* diverges, diverges *)
+  constructor. apply traceinf_prefix_2_sim; auto.
+Qed.
+
+Lemma matching_behaviors_same:
+  forall b b1' b2',
+  matching_behaviors b b1' -> same_behaviors b1' b2' ->
+  matching_behaviors b b2'.
+Proof.
+  intros. inv H; inv H0. 
+  constructor.
+  constructor. apply traceinf_prefix_compat with T2 T1.
+  auto. apply traceinf_sim_sym; auto. apply traceinf_sim_refl.
+Qed.
+
+(** * Additional semantic preservation property *)
+
+(** Combining the semantic preservation theorem from module [Main]
+  with the determinism of Asm executions, we easily obtain
+  additional, stronger semantic preservation properties.
+  The first property states that, when compiling a Clight
+  program that has well-defined semantics, all possible executions
+  of the resulting Asm code correspond to an execution of
+  the source Clight program, in the sense of the [matching_behaviors]
+  predicate. *)
+
+Theorem transf_c_program_correct_strong:
+  forall p tp b w,
+  transf_c_program p = OK tp ->
+  Csem.exec_program p b ->
+  possible_behavior w b ->
+  (exists b', exec_program' tp w b')
+/\(forall b', exec_program' tp w b' ->
+   exists b0, Csem.exec_program p b0 /\ matching_behaviors b0 b').
+Proof.
+  intros.
+  assert (Asm.exec_program tp b).
+    eapply transf_c_program_correct; eauto.
+  exploit exec_program_program'; eauto. 
+  intros [b' [A B]].
+  split. exists b'; auto.
+  intros. exists b. split. auto.
+  apply matching_behaviors_same with b'. auto.
+  eapply exec_program'_deterministic; eauto.
+Qed.
+
+Section SPECS_PRESERVED.
+
+(** The second additional results shows that if one execution
+  of the source Clight program satisfies a given specification
+  (a predicate on the observable behavior of the program),
+  then all executions of the produced Asm program satisfy
+  this specification as well.  *) 
+
+Variable spec: program_behavior -> Prop.
+
+(* Since the execution trace for a diverging Clight program
+   is not uniquely defined (the trace can contain events that
+   the program will never perform because it loops earlier),
+   this result holds only if the specification is closed under
+   prefixes in the case of diverging executions.  This is the
+   case for all safety properties (some undesirable event never
+   occurs), but not for liveness properties (some desirable event
+   always occurs). *)
+
+Hypothesis spec_safety:
+  forall T T', traceinf_prefix T T' -> spec (Diverges T') -> spec (Diverges T).
+
+Theorem transf_c_program_preserves_spec:
+  forall p tp b w,
+  transf_c_program p = OK tp ->
+  Csem.exec_program p b ->
+  possible_behavior w b ->
+  spec b ->
+  (exists b', exec_program' tp w b')
+/\(forall b', exec_program' tp w b' -> spec b').
+Proof.
+  intros.
+  assert (Asm.exec_program tp b).
+    eapply transf_c_program_correct; eauto.
+  exploit exec_program_program'; eauto. 
+  intros [b' [A B]].
+  split. exists b'; auto.
+  intros b'' EX.
+  assert (same_behaviors b' b''). eapply exec_program'_deterministic; eauto.
+  inv B; inv H4. 
+  auto.
+  apply spec_safety with T1. 
+  eapply traceinf_prefix_compat with T2 T1. 
+  auto. apply traceinf_sim_sym; auto. apply traceinf_sim_refl.
+  auto.
+Qed.
+
+End SPECS_PRESERVED.
diff --git a/driver/Driver.ml b/driver/Driver.ml
new file mode 100644
index 00000000..8361829f
--- /dev/null
+++ b/driver/Driver.ml
@@ -0,0 +1,352 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Printf
+open Clflags
+
+(* Location of the standard library *)
+
+let stdlib_path = ref(
+  try
+    Sys.getenv "COMPCERT_LIBRARY"
+  with Not_found ->
+    Configuration.stdlib_path)
+
+let command cmd =
+  if !option_v then begin
+    prerr_string "+ "; prerr_string cmd; prerr_endline ""
+  end;
+  Sys.command cmd
+
+let quote_options opts =
+  String.concat " " (List.rev_map Filename.quote opts)
+
+let safe_remove file =
+  try Sys.remove file with Sys_error _ -> ()
+
+(* Printing of error messages *)
+
+let print_error oc msg =
+  let print_one_error = function
+  | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
+  | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
+  in List.iter print_one_error msg
+
+(* For the CIL -> Csyntax translator:
+
+  * The meaning of some type specifiers may depend on compiler options:
+      the size of an int or the default signedness of char, for instance.
+
+  * Those type conversions may be parameterized thanks to a functor.
+
+  * Remark: [None] means that the type specifier is not supported
+      (that is, an Unsupported exception will be raised if that type
+      specifier is encountered in the program).
+*)
+
+module TypeSpecifierTranslator = struct
+  
+  open Cil
+  open Csyntax
+    
+  (** Convert a Cil.ikind into an (intsize * signedness) option *)
+  let convertIkind = function
+    | IChar      -> Some (I8, Unsigned)
+    | ISChar     -> Some (I8, Signed)
+    | IUChar     -> Some (I8, Unsigned)
+    | IInt       -> Some (I32, Signed)
+    | IUInt      -> Some (I32, Unsigned)
+    | IShort     -> Some (I16, Signed)
+    | IUShort    -> Some (I16, Unsigned)
+    | ILong      -> Some (I32, Signed)
+    | IULong     -> Some (I32, Unsigned)
+    | ILongLong  -> if !option_flonglong then Some (I32, Signed) else None
+    | IULongLong -> if !option_flonglong then Some (I32, Unsigned) else None
+	
+  (** Convert a Cil.fkind into an floatsize option *)
+  let convertFkind = function
+    | FFloat      -> Some F32
+    | FDouble     -> Some F64
+    | FLongDouble -> if !option_flonglong then Some F64 else None
+	
+end
+
+module Cil2CsyntaxTranslator = Cil2Csyntax.Make(TypeSpecifierTranslator)
+
+(* From C to preprocessed C *)
+
+let preprocess ifile ofile =
+  let cmd =
+    sprintf "%s -D__COMPCERT__ -I%s %s %s > %s"
+      Configuration.prepro
+      !stdlib_path
+      (quote_options !prepro_options)
+      ifile ofile in
+  if command cmd <> 0 then begin
+    safe_remove ofile;
+    eprintf "Error during preprocessing.\n";
+    exit 2
+  end
+
+(* From preprocessed C to asm *)
+
+let compile_c_file sourcename ifile ofile =
+  (* Parsing and production of a CIL.file *)
+  let cil =
+    try
+      Frontc.parse ifile ()
+    with
+    | Frontc.ParseError msg ->
+        eprintf "Error during parsing: %s\n" msg;
+        exit 2
+    | Errormsg.Error ->
+        exit 2 in
+  (* Remove preprocessed file (always a temp file) *)
+  safe_remove ifile;
+  (* Restore original source file name *)
+  cil.Cil.fileName <- sourcename;
+  (* Cleanup in the CIL.file *)
+  Rmtmps.removeUnusedTemps ~isRoot:Rmtmps.isExportedRoot cil;
+  (* Conversion to Csyntax *)
+  let csyntax =
+    try
+      Cil2CsyntaxTranslator.convertFile cil
+    with
+    | Cil2CsyntaxTranslator.Unsupported msg ->
+        eprintf "%s\n" msg;
+        exit 2
+    | Cil2CsyntaxTranslator.Internal_error msg ->
+        eprintf "%s\nPlease report it.\n" msg;
+        exit 2 in
+  (* Save Csyntax if requested *)
+  if !option_dclight then begin
+    let targetname = Filename.chop_suffix sourcename ".c" in
+    let oc = open_out (targetname ^ ".light.c") in
+    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
+    close_out oc
+  end;
+  (* Convert to Asm *)
+  let ppc =
+    match Compiler.transf_c_program csyntax with
+    | Errors.OK x -> x
+    | Errors.Error msg ->
+        print_error stderr msg;
+        exit 2 in
+  (* Save asm *)
+  let oc = open_out ofile in
+  PrintAsm.print_program oc ppc;
+  close_out oc
+
+(* From Cminor to asm *)
+
+let compile_cminor_file ifile ofile =
+  let ic = open_in ifile in
+  let lb = Lexing.from_channel ic in
+  try
+    match Compiler.transf_cminor_program
+            (CMtypecheck.type_program
+              (CMparser.prog CMlexer.token lb)) with
+    | Errors.Error msg ->
+        print_error stderr msg;
+        exit 2
+    | Errors.OK p ->
+        let oc = open_out ofile in
+        PrintAsm.print_program oc p;
+        close_out oc
+  with Parsing.Parse_error ->
+         eprintf "File %s, character %d: Syntax error\n"
+                 ifile (Lexing.lexeme_start lb);
+         exit 2
+     | CMlexer.Error msg ->  
+         eprintf "File %s, character %d: %s\n"
+                 ifile (Lexing.lexeme_start lb) msg;
+         exit 2
+     | CMtypecheck.Error msg ->
+         eprintf "File %s, type-checking error:\n%s"
+                 ifile msg;
+         exit 2
+
+(* From asm to object file *)
+
+let assemble ifile ofile =
+  let cmd =
+    sprintf "%s -o %s %s"
+      Configuration.asm ofile ifile in
+  let retcode = command cmd in
+  if not !option_dasm then safe_remove ifile;
+  if retcode <> 0 then begin
+    safe_remove ofile;
+    eprintf "Error during assembling.\n";
+    exit 2
+  end
+
+(* Linking *)
+
+let linker exe_name files =
+  let cmd =
+    sprintf "%s -o %s %s -L%s -lcompcert"
+      Configuration.linker
+      (Filename.quote exe_name)
+      (quote_options files)
+      !stdlib_path in
+  if command cmd <> 0 then exit 2
+
+(* Processing of a .c file *)
+
+let process_c_file sourcename =
+  let prefixname = Filename.chop_suffix sourcename ".c" in
+  if !option_E then begin
+    preprocess sourcename (prefixname ^ ".i")
+  end else begin
+    let preproname = Filename.temp_file "compcert" ".i" in
+    preprocess sourcename preproname;
+    if !option_S then begin
+      compile_c_file sourcename preproname (prefixname ^ ".s")
+    end else begin
+      let asmname =
+        if !option_dasm
+        then prefixname ^ ".s"
+        else Filename.temp_file "compcert" ".s" in
+      compile_c_file sourcename preproname asmname;
+      assemble asmname (prefixname ^ ".o")
+    end
+  end;
+  prefixname ^ ".o"
+
+(* Processing of a .cm file *)
+
+let process_cminor_file sourcename =
+  let prefixname = Filename.chop_suffix sourcename ".cm" in
+  if !option_S then begin
+    compile_cminor_file sourcename (prefixname ^ ".s")
+  end else begin
+    let asmname =
+      if !option_dasm
+      then prefixname ^ ".s"
+      else Filename.temp_file "compcert" ".s" in
+    compile_cminor_file sourcename asmname;
+    assemble asmname (prefixname ^ ".o")
+  end;
+  prefixname ^ ".o"
+
+(* Command-line parsing *)
+
+let starts_with s1 s2 =
+  String.length s1 >= String.length s2 &&
+  String.sub s1 0 (String.length s2) = s2
+
+let usage_string =
+"ccomp [options] <source files>
+Recognized source files:
+  .c             C source file
+  .cm            Cminor source file
+  .o             Object file
+  .a             Library file
+Processing options:
+  -E             Preprocess only, save result in <file>.i
+  -S             Compile to assembler only, save result in <file>.s
+  -c             Compile to object file only (no linking), result in <file>.o
+Preprocessing options:
+  -I<dir>        Add <dir> to search path for #include files
+  -D<symb>=<val> Define preprocessor symbol
+  -U<symb>       Undefine preprocessor symbol
+Compilation options:
+  -flonglong     Treat 'long long' as 'long' and 'long double' as 'double'
+  -fmadd         Use fused multiply-add and multiply-sub instructions
+  -dclight       Save generated Clight in <file>.light.c
+  -dasm          Save generated assembly in <file>.s
+Linking options:
+  -l<lib>        Link library <lib>
+  -L<dir>        Add <dir> to search path for libraries
+  -o <file>      Generate executable in <file> (default: a.out)
+General options:
+  -stdlib <dir>  Set the path of the Compcert run-time library
+  -v             Print external commands before invoking them
+"
+
+let rec parse_cmdline i =
+  if i < Array.length Sys.argv then begin
+    let s = Sys.argv.(i) in
+    if starts_with s "-I" || starts_with s "-D" || starts_with s "-U"
+    then begin
+      prepro_options := s :: !prepro_options;
+      parse_cmdline (i + 1)
+    end else 
+    if starts_with s "-l" || starts_with s "-L" then begin
+      linker_options := s :: !linker_options;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-o" && i + 1 < Array.length Sys.argv then begin
+      exe_name := Sys.argv.(i + 1);
+      parse_cmdline (i + 2)
+    end else
+    if s = "-stdlib" && i + 1 < Array.length Sys.argv then begin
+      stdlib_path := Sys.argv.(i + 1);
+      parse_cmdline (i + 2)
+    end else
+    if s = "-flonglong" then begin
+      option_flonglong := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-fmadd" then begin
+      option_fmadd := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-dclight" then begin
+      option_dclight := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-dasm" then begin
+      option_dasm := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-E" then begin
+      option_E := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-S" then begin
+      option_S := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-c" then begin
+      option_c := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-v" then begin
+      option_v := true;
+      parse_cmdline (i + 1)
+    end else
+    if Filename.check_suffix s ".c" then begin
+      let objfile = process_c_file s in
+      linker_options := objfile :: !linker_options;
+      parse_cmdline (i + 1)
+    end else
+    if Filename.check_suffix s ".cm" then begin
+      let objfile = process_cminor_file s in
+      linker_options := objfile :: !linker_options;
+      parse_cmdline (i + 1)
+    end else
+    if Filename.check_suffix s ".o" || Filename.check_suffix s ".a" then begin
+      linker_options := s :: !linker_options;
+      parse_cmdline (i + 1)
+    end else begin
+      eprintf "Unknown argument `%s'\n" s;
+      eprintf "Usage: %s" usage_string;
+      exit 2
+    end
+  end
+
+let _ =
+  parse_cmdline 1;
+  if not (!option_c || !option_S || !option_E) then begin
+    linker !exe_name !linker_options
+  end