Merge of branches/full-expr-4:

- Csyntax, Csem: source C language has side-effects within expressions,
  performs implicit casts, and has nondeterministic reduction semantics
  for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
  Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
  (previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
  now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
  and matching -dxxx command-line flags.



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

4 files changed, 233 insertions, 104 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index fcec4c6..e825c66 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -22,7 +22,15 @@ let option_fbitfields = ref false
 let option_fvararg_calls = ref true
 let option_fmadd = ref false
 let option_dparse = ref false
+let option_dcmedium = ref false
 let option_dclight = ref false
+let option_dcminor = ref false
+let option_drtl = ref false
+let option_dtailcall = ref false
+let option_dcastopt = ref false
+let option_dconstprop = ref false
+let option_dcse = ref false
+let option_dalloc = ref false
 let option_dasm = ref false
 let option_E = ref false
 let option_S = ref false
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 09a6c52..e57d80d 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -23,6 +23,8 @@ Require Import Smallstep.
 (** Languages (syntax and semantics). *)
 Require Csyntax.
 Require Csem.
+Require Cstrategy.
+Require Clight.
 Require Csharpminor.
 Require Cminor.
 Require CminorSel.
@@ -33,11 +35,13 @@ Require Linear.
 Require Mach.
 Require Asm.
 (** Translation passes. *)
+Require SimplExpr.
 Require Cshmgen.
 Require Cminorgen.
 Require Selection.
 Require RTLgen.
 Require Tailcall.
+Require CastOptim.
 Require Constprop.
 Require CSE.
 Require Allocation.
@@ -47,18 +51,19 @@ 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 SimplExprproof.
+Require Cshmgenproof.
 Require Cminorgenproof.
 Require Selectionproof.
 Require RTLgenproof.
 Require Tailcallproof.
+Require CastOptimproof.
 Require Constpropproof.
 Require CSEproof.
 Require Allocproof.
@@ -73,6 +78,16 @@ Require Stackingproof.
 Require Stackingtyping.
 Require Machabstr2concr.
 Require Asmgenproof.
+(** Pretty-printers (defined in Caml). *)
+Parameter print_Csyntax: Csyntax.program -> unit.
+Parameter print_Clight: Clight.program -> unit.
+Parameter print_Cminor: Cminor.program -> unit.
+Parameter print_RTL: RTL.fundef -> unit.
+Parameter print_RTL_tailcall: RTL.fundef -> unit.
+Parameter print_RTL_castopt: RTL.fundef -> unit.
+Parameter print_RTL_constprop: RTL.fundef -> unit.
+Parameter print_RTL_cse: RTL.fundef -> unit.
+Parameter print_LTLin: LTLin.fundef -> unit.
 
 Open Local Scope string_scope.
 
@@ -93,6 +108,9 @@ Notation "a @@@ b" :=
 Notation "a @@ b" :=
    (apply_total _ _ a b) (at level 50, left associativity).
 
+Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
+  match printer prog with tt => prog end.
+
 (** 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
@@ -111,12 +129,19 @@ Notation "a @@ b" :=
 
 Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef :=
    OK f
+   @@ print print_RTL
    @@ Tailcall.transf_fundef
+   @@ print print_RTL_tailcall
+   @@ CastOptim.transf_fundef
+   @@ print print_RTL_castopt
    @@ Constprop.transf_fundef
+   @@ print print_RTL_constprop
    @@ CSE.transf_fundef
+   @@ print print_RTL_cse
   @@@ Allocation.transf_fundef
    @@ Tunneling.tunnel_fundef
   @@@ Linearize.transf_fundef
+   @@ print print_LTLin
    @@ Reload.transf_fundef
   @@@ Stacking.transf_fundef
   @@@ Asmgen.transf_fundef.
@@ -135,22 +160,28 @@ Definition transf_rtl_program (p: RTL.program) : res Asm.program :=
 
 Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
    OK p
+   @@ print print_Cminor
    @@ Selection.sel_program
   @@@ transform_partial_program transf_cminorsel_fundef.
 
 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.
+  OK p 
+   @@ print print_Csyntax
+  @@@ SimplExpr.transl_program
+   @@ print print_Clight
+  @@@ Cshmgen.transl_program
+  @@@ Cminorgen.transl_program
+  @@@ transf_cminor_program.
 
 (** The following lemmas help reason over compositions of passes. *)
 
+Lemma print_identity:
+  forall (A: Type) (printer: A -> unit) (prog: A),
+  print printer prog = prog.
+Proof.
+  intros; unfold print. destruct (printer prog); auto. 
+Qed.
+
 Lemma map_partial_compose:
   forall (X A B C: Type)
          (ctx: X -> errmsg)
@@ -221,12 +252,42 @@ Proof.
   apply extensionality; auto. 
 Qed.
 
+Lemma transform_program_print_identity:
+  forall (A V: Type) (p: program A V) (f: A -> unit),
+  transform_program (print f) p = p.
+Proof.
+  intros until f. unfold transform_program, transf_program. 
+  destruct p; simpl; f_equal. 
+  transitivity (map (fun x => x) prog_funct). 
+  apply list_map_exten; intros. destruct x; simpl. rewrite print_identity. auto.
+  apply list_map_identity.
+Qed.
+
+Lemma compose_print_identity:
+  forall (A: Type) (x: res A) (f: A -> unit), 
+  x @@ print f = x.
+Proof.
+  intros. destruct x; simpl. rewrite print_identity. auto. 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! *)
 
+Ltac TransfProgInv :=
+  match goal with
+  | [ H: transform_partial_program (fun f => _ @@@ _) _ = OK _ |- _ ] =>
+      let p := fresh "p" in let X := fresh "X" in let P := fresh "P" in
+      destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p [X P]];
+      clear H
+  | [ H: transform_partial_program (fun f => _ @@ _) _ = OK _ |- _ ] =>
+      let p := fresh "p" in let X := fresh "X" in let P := fresh "P" in
+      destruct (transform_program_compose _ _ _ _ _ _ _ _ H) as [p [X P]];
+      clear H
+  end.
+
 Theorem transf_rtl_program_correct:
   forall p tp beh,
   transf_rtl_program p = OK tp ->
@@ -235,47 +296,25 @@ Theorem transf_rtl_program_correct:
   Asm.exec_program tp beh.
 Proof.
   intros. unfold transf_rtl_program, transf_rtl_fundef in H.
-  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p7 [X7 P7]].
-  clear H.
-  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X7) as [p6 [X6 P6]].
-  clear X7.
-  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X6) as [p5 [X5 P5]].
-  clear X6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5.
-  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X5) as [p4 [X4 P4]].
-  clear X5.
-  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X4) as [p3 [X3 P3]].
-  clear X4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3.
-  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X3) as [p2 [X2 P2]].
-  clear X3.
-  destruct (transform_program_compose _ _ _ _ _ _ _ _ X2) as [p1 [X1 P1]].
-  clear X2.
-  destruct (transform_program_compose _ _ _ _ _ _ _ _ X1) as [p0 [X0 P0]].
-  clear X1.
-  destruct (transform_program_compose _ _ _ _ _ _ _ _ X0) as [p00 [X00 P00]].
-  clear X0.
-  generalize (transform_partial_program_identity _ _ _ _ X00). clear X00. intro. subst p00.
-
-  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; auto.
-  apply Allocproof.transf_program_correct with p2; auto.
-  subst p2; apply CSEproof.transf_program_correct; auto.
-  subst p1; apply Constpropproof.transf_program_correct; auto.
-  subst p0; apply Tailcallproof.transf_program_correct; auto.
+  repeat TransfProgInv. 
+  repeat rewrite transform_program_print_identity in *. subst. 
+  exploit transform_partial_program_identity; eauto. intro EQ. subst.
+
+  generalize Alloctyping.program_typing_preserved Tunnelingtyping.program_typing_preserved
+             Linearizetyping.program_typing_preserved Reloadtyping.program_typing_preserved
+             Stackingtyping.program_typing_preserved; intros.
+
+  eapply Asmgenproof.transf_program_correct; eauto 6.
+  eapply Machabstr2concr.exec_program_equiv; eauto 6.
+  eapply Stackingproof.transf_program_correct; eauto.
+  eapply Reloadproof.transf_program_correct; eauto.
+  eapply Linearizeproof.transf_program_correct; eauto.
+  eapply Tunnelingproof.transf_program_correct; eauto.
+  eapply Allocproof.transf_program_correct; eauto.
+  eapply CSEproof.transf_program_correct; eauto.
+  eapply Constpropproof.transf_program_correct; eauto.
+  eapply CastOptimproof.transf_program_correct; eauto.
+  eapply Tailcallproof.transf_program_correct; eauto.
 Qed.
 
 Theorem transf_cminor_program_correct:
@@ -286,30 +325,29 @@ Theorem transf_cminor_program_correct:
   Asm.exec_program tp beh.
 Proof.
   intros. unfold transf_cminor_program, transf_cminorsel_fundef in H.
-  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [X3 P3]].
-  clear H.
-  destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X3) as [p2 [X2 P2]].
-  clear X3.
-  generalize (transform_partial_program_identity _ _ _ _ X2). clear X2. intro. subst p2.
-  apply transf_rtl_program_correct with p3; auto.
-  apply RTLgenproof.transf_program_correct with (Selection.sel_program p); auto.
-  apply Selectionproof.transf_program_correct; auto.
+  simpl in H. repeat TransfProgInv.
+  eapply transf_rtl_program_correct; eauto.
+  eapply RTLgenproof.transf_program_correct; eauto.
+  eapply Selectionproof.transf_program_correct; eauto.
+  rewrite print_identity. auto.
 Qed.
 
 Theorem transf_c_program_correct:
   forall p tp beh,
   transf_c_program p = OK tp ->
   not_wrong beh ->
-  Csem.exec_program p beh ->
+  Cstrategy.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.
+  rewrite print_identity.
+  caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0.
+  rewrite print_identity.
+  caseEq (Cshmgen.transl_program p0); simpl; try congruence; intros p1 EQ1.
   caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2.
   intros EQ3 NOTW 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.
+  eapply Cshmgenproof.transl_program_correct; eauto.
+  eapply SimplExprproof.transl_program_correct; eauto.
 Qed.
diff --git a/driver/Complements.v b/driver/Complements.v
index 3f32cc6..334b9b0 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -23,15 +23,74 @@ Require Import Smallstep.
 Require Import Determinism.
 Require Import Csyntax.
 Require Import Csem.
+Require Import Cstrategy.
 Require Import Asm.
 Require Import Compiler.
 Require Import Errors.
 
-(** * Determinism of Asm semantics *)
+(** * Integrating a deterministic external world *)
 
-(** In this section, we show that the semantics for the Asm language
-  are deterministic, provided that the program is executed against a
-  deterministic world, as formalized in module [Determinism]. *)
+(** We now integrate a deterministic external world in the semantics
+  of Compcert C and Asm. *)
+
+Section WORLD.
+
+Variable initial_world: world.
+
+Definition exec_C_program (p: Csyntax.program) (beh: program_behavior) : Prop :=
+  wprogram_behaves _ _
+      Csem.step (Csem.initial_state p) Csem.final_state
+      initial_world (Genv.globalenv p) beh.
+
+Definition exec_asm_program (p: Asm.program) (beh: program_behavior) : Prop :=
+  wprogram_behaves _ _
+      Asm.step (Asm.initial_state p) Asm.final_state
+      initial_world (Genv.globalenv p) beh.
+
+(** ** Safety of C programs. *)
+
+(** We show that a C program is safe (in the sense of [Cstrategy.safeprog])
+  if it cannot go wrong in the world-aware semantics. *)
+
+Lemma notwrong_safeprog:
+  forall p,
+  (forall beh, exec_C_program p beh -> not_wrong beh) ->
+  Cstrategy.safeprog p initial_world.
+Proof.
+  intros; red.
+  assert (exists beh1, exec_C_program p beh1).
+    unfold exec_C_program. apply program_behaves_exists. 
+  destruct H0 as [beh1 A].
+  assert (B: not_wrong beh1) by auto.
+  split.
+  inv A; simpl in B.
+  destruct H0. exists (fst s); auto.
+  destruct H0. exists (fst s); auto.
+  destruct H0. exists (fst s); auto.
+  contradiction.
+  contradiction.
+  intros; red; intros.
+  destruct (classic (exists r, Csem.final_state s' r)).
+  (* 1. Final state.  This is immsafe. *)
+  destruct H3 as [r F]. eapply immsafe_final; eauto. 
+  (* 2. Not a final state. *)
+  destruct (classic (nostep (wstep _ _ Csem.step) (Genv.globalenv p) (s', w'))).
+  (* 2.1 No step possible -> going wrong *)
+  elim (H (Goes_wrong t)). 
+  eapply program_goes_wrong.
+  instantiate (1 := (s, initial_world)). split; auto.
+  instantiate (1 := (s', w')). apply Determinism.inject_star; auto. 
+  auto.
+  intros; red; intros. elim H3. exists r; auto. 
+  (* 2.2 One step possible -> this is immsafe *)
+  unfold nostep in H4. 
+  generalize (not_all_ex_not _ _ H4). clear H4. intros [t' P].
+  generalize (not_all_ex_not _ _ P). clear P. intros [s'' Q].
+  generalize (NNPP _ Q). clear Q. intros R. destruct R as [R1 R2]. simpl in *.
+  eapply immsafe_step. eauto. eauto. 
+Qed.
+
+(** ** Determinism of Asm semantics *)
 
 Remark extcall_arguments_deterministic:
   forall rs m sg args args',
@@ -100,17 +159,20 @@ Proof.
 Qed.
 
 Theorem asm_exec_program_deterministic:
-  forall p w beh1 beh2,
-  Asm.exec_program p beh1 -> Asm.exec_program p beh2 ->
-  possible_behavior w beh1 -> possible_behavior w beh2 ->
+  forall p beh1 beh2,
+  exec_asm_program p beh1 -> exec_asm_program p beh2 ->
   beh1 = beh2.
 Proof.
-  intros. 
-  eapply (program_behaves_deterministic _ _ step (initial_state p) final_state); eauto.
-  exact step_internal_deterministic.
-  exact (initial_state_deterministic p).
-  exact final_state_deterministic.
-  exact final_state_not_step.
+  intros. hnf in H; hnf in H0.
+  eapply (program_behaves_deterministic _ _
+             (wstep _ _ step)
+             (winitial_state _ (initial_state p) initial_world)
+             (wfinal_state _ final_state));
+  eauto.
+  apply wstep_deterministic. apply step_internal_deterministic.
+  apply winitial_state_determ. apply initial_state_deterministic.
+  apply wfinal_state_determ. apply final_state_deterministic.
+  apply wfinal_state_nostep. apply final_state_not_step.
 Qed.
 
 (** * Additional semantic preservation property *)
@@ -118,28 +180,34 @@ Qed.
 (** Combining the semantic preservation theorem from module [Compiler]
   with the determinism of Asm executions, we easily obtain
   additional, stronger semantic preservation properties.
-  The first property states that, when compiling a Clight
+  The first property states that, when compiling a Compcert C
   program that has well-defined semantics, all possible executions
   of the resulting Asm code correspond to an execution of
-  the source Clight program. *)
+  the source program. *)
 
 Theorem transf_c_program_is_refinement:
-  forall p tp w,
+  forall p tp,
   transf_c_program p = OK tp ->
-  (exists b, Csem.exec_program p b /\ possible_behavior w b /\ not_wrong b) ->
-  (forall b, Asm.exec_program tp b -> possible_behavior w b -> Csem.exec_program p b).
+  (forall beh, exec_C_program p beh -> not_wrong beh) ->
+  (forall beh, exec_asm_program tp beh -> exec_C_program p beh).
 Proof.
-  intros. destruct H0 as [b0 [A [B C]]]. 
-  assert (Asm.exec_program tp b0).
+  intros. 
+  exploit Cstrategy.strategy_behavior.
+  apply notwrong_safeprog. eauto. 
+  intros [beh1 [A [B [C D]]]].
+  assert (Asm.exec_program tp beh1).
     eapply transf_c_program_correct; eauto.
-  assert (b = b0). eapply asm_exec_program_deterministic; eauto.
-  subst b0. auto.
+  assert (exec_asm_program tp beh1).
+    red. apply inject_behaviors; auto.
+  assert (beh = beh1). eapply asm_exec_program_deterministic; eauto.
+  subst beh.
+  red. apply inject_behaviors; auto.
 Qed.
 
 Section SPECS_PRESERVED.
 
 (** The second additional results shows that if one execution
-  of the source Clight program satisfies a given specification
+  of the source C 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.  *) 
@@ -149,16 +217,15 @@ Variable spec: program_behavior -> Prop.
 Hypothesis spec_not_wrong: forall b, spec b -> not_wrong b.
 
 Theorem transf_c_program_preserves_spec:
-  forall p tp w,
+  forall p tp,
   transf_c_program p = OK tp ->
-  (exists b, Csem.exec_program p b /\ possible_behavior w b /\ spec b) ->
-  (forall b, Asm.exec_program tp b -> possible_behavior w b -> spec b).
+  (forall beh, exec_C_program p beh -> spec beh) ->
+  (forall beh, exec_asm_program tp beh -> spec beh).
 Proof.
-  intros. destruct H0 as [b1 [A [B C]]].
-  assert (Asm.exec_program tp b1).
-    eapply transf_c_program_correct; eauto.
-  assert (b1 = b). eapply asm_exec_program_deterministic; eauto. 
-  subst b1. auto.
+  intros. apply H0. apply transf_c_program_is_refinement with tp; auto. 
 Qed.
 
 End SPECS_PRESERVED.
+
+End WORLD.
+
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 2776604..8afe03c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -64,7 +64,7 @@ let compile_c_file sourcename ifile ofile =
   Sections.initialize();
   (* Simplification options *)
   let simplifs =
-    "becv" (* blocks, impure exprs, implicit casts, volatiles: mandatory *)
+    "b" (* blocks: mandatory *)
   ^ (if !option_fstruct_passing then "s" else "")
   ^ (if !option_fstruct_assign then "S" else "")
   ^ (if !option_fbitfields then "f" else "") in
@@ -87,13 +87,20 @@ let compile_c_file sourcename ifile ofile =
     match C2Clight.convertProgram ast with
     | None -> exit 2
     | Some p -> p in
-  (* Save Csyntax if requested *)
-  if !option_dclight then begin
-    let ofile = Filename.chop_suffix sourcename ".c" ^ ".light.c" in
-    let oc = open_out ofile in
-    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
-    close_out oc
-  end;
+  flush stderr;
+  (* Prepare to dump Csyntax, Clight, RTL, etc, if requested *)
+  let set_dest dst opt ext =
+    dst := if !opt then Some (Filename.chop_suffix sourcename ".c" ^ ext)
+                   else None in
+  set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
+  set_dest PrintClight.destination option_dclight ".light.c";
+  set_dest PrintCminor.destination option_dcminor ".cm";
+  set_dest PrintRTL.destination_rtl option_drtl ".rtl";
+  set_dest PrintRTL.destination_tailcall option_dtailcall ".tailcall.rtl";
+  set_dest PrintRTL.destination_castopt option_dcastopt ".castopt.rtl";
+  set_dest PrintRTL.destination_constprop option_dconstprop ".constprop.rtl";
+  set_dest PrintRTL.destination_cse option_dcse ".cse.rtl";
+  set_dest PrintLTLin.destination option_dalloc ".alloc.ltl";
   (* Convert to Asm *)
   let ppc =
     match Compiler.transf_c_program csyntax with
@@ -228,6 +235,7 @@ Code generation options:
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
 Tracing options:
   -dparse        Save C file after parsing and elaboration in <file>.parse.c
+  -dcmedium      Save generated Cmedium in <file>.medium.c
   -dclight       Save generated Clight in <file>.light.c
   -dasm          Save generated assembly in <file>.s
 Linking options:
@@ -304,7 +312,15 @@ let cmdline_actions =
   "-o$", String(fun s -> exe_name := s);
   "-stdlib$", String(fun s -> stdlib_path := s);
   "-dparse$", Set option_dparse;
+  "-dcmedium$", Set option_dcmedium;
   "-dclight$", Set option_dclight;
+  "-dcminor", Set option_dcminor;
+  "-drtl$", Set option_drtl;
+  "-dtailcall$", Set option_dtailcall;
+  "-dcastopt$", Set option_dcastopt;
+  "-dconstprop$", Set option_dconstprop;
+  "-dcse$", Set option_dcse;
+  "-dalloc$", Set option_dalloc;
   "-dasm$", Set option_dasm;
   "-E$", Set option_E;
   "-S$", Set option_S;