diff options
| -rw-r--r-- | backend/Deadcodeproof.v | 16 | ||||
| -rw-r--r-- | backend/Unusedglobproof.v | 11 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 3 | ||||
| -rw-r--r-- | common/Memory.v | 129 | ||||
| -rw-r--r-- | common/Separation.v | 4 | ||||
| -rw-r--r-- | driver/Assembler.ml | 47 | ||||
| -rw-r--r-- | driver/Assembler.mli | 21 | ||||
| -rw-r--r-- | driver/Driver.ml | 171 | ||||
| -rw-r--r-- | driver/Driveraux.ml | 25 | ||||
| -rw-r--r-- | driver/Driveraux.mli | 13 | ||||
| -rw-r--r-- | driver/Frontend.ml | 97 | ||||
| -rw-r--r-- | driver/Frontend.mli | 1 | ||||
| -rw-r--r-- | driver/Linker.ml | 81 | ||||
| -rw-r--r-- | driver/Linker.mli | 21 |
14 files changed, 447 insertions, 193 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 72881b94..26953479 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -39,8 +39,10 @@ Definition locset := block -> Z -> Prop. Record magree (m1 m2: mem) (P: locset) : Prop := mk_magree { ma_perm: forall b ofs k p, - Mem.perm m1 b ofs k p -> - Mem.perm m2 b ofs k p; + Mem.perm m1 b ofs k p -> Mem.perm m2 b ofs k p; + ma_perm_inv: + forall b ofs k p, + Mem.perm m2 b ofs k p -> Mem.perm m1 b ofs k p \/ ~Mem.perm m1 b ofs Max Nonempty; ma_memval: forall b ofs, Mem.perm m1 b ofs Cur Readable -> @@ -65,6 +67,7 @@ Lemma mextends_agree: Proof. intros. destruct H. destruct mext_inj. constructor; intros. - replace ofs with (ofs + 0) by omega. eapply mi_perm; eauto. auto. +- eauto. - exploit mi_memval; eauto. unfold inject_id; eauto. rewrite Zplus_0_r. auto. - auto. @@ -157,6 +160,8 @@ Proof. constructor; intros. - eapply Mem.perm_storebytes_1; eauto. eapply ma_perm; eauto. eapply Mem.perm_storebytes_2; eauto. +- exploit ma_perm_inv; eauto using Mem.perm_storebytes_2. + intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2. - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0). rewrite (Mem.storebytes_mem_contents _ _ _ _ _ ST2). rewrite ! PMap.gsspec. destruct (peq b0 b). @@ -201,6 +206,8 @@ Lemma magree_storebytes_left: Proof. intros. constructor; intros. - eapply ma_perm; eauto. eapply Mem.perm_storebytes_2; eauto. +- exploit ma_perm_inv; eauto. + intuition eauto using Mem.perm_storebytes_1, Mem.perm_storebytes_2. - rewrite (Mem.storebytes_mem_contents _ _ _ _ _ H0). rewrite PMap.gsspec. destruct (peq b0 b). + subst b0. rewrite Mem.setN_outside. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. @@ -242,6 +249,11 @@ Proof. assert (Mem.perm m2 b0 ofs k p). { eapply ma_perm; eauto. eapply Mem.perm_free_3; eauto. } exploit Mem.perm_free_inv; eauto. intros [[A B] | A]; auto. subst b0. eelim Mem.perm_free_2. eexact H0. eauto. eauto. +- (* inverse permissions *) + exploit ma_perm_inv; eauto using Mem.perm_free_3. intros [A|A]. + eapply Mem.perm_free_inv in A; eauto. destruct A as [[A B] | A]; auto. + subst b0; right; eapply Mem.perm_free_2; eauto. + right; intuition eauto using Mem.perm_free_3. - (* contents *) rewrite (Mem.free_result _ _ _ _ _ H0). rewrite (Mem.free_result _ _ _ _ _ FREE). diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index bb40a2d3..44cf1e8a 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -1178,6 +1178,17 @@ Proof. destruct (ident_eq id1 id2). congruence. left; eapply Genv.global_addresses_distinct; eauto. - exploit init_meminj_invert; eauto. intros (A & id & B & C). subst delta. split. omega. generalize (Int.unsigned_range_2 ofs). omega. +- exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F). + exploit (Genv.init_mem_characterization_gen p); eauto. + exploit (Genv.init_mem_characterization_gen tp); eauto. + destruct gd as [f|v]. ++ intros (P2 & Q2) (P1 & Q1). + apply Q2 in H0. destruct H0. subst. replace ofs with 0 by omega. + left; apply Mem.perm_cur; auto. ++ intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1). + apply Q2 in H0. destruct H0. subst. + left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. + apply P1. omega. Qed. End INIT_MEM. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 8b76f44d..3c80d733 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3766,6 +3766,9 @@ Proof. - (* overflow *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Zplus_0_r. split. omega. apply Int.unsigned_range_2. +- (* perm inv *) + intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. + rewrite Zplus_0_r in H2. auto. Qed. Lemma inj_of_bc_preserves_globals: diff --git a/common/Memory.v b/common/Memory.v index 0ea9e3b0..f32d21c7 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -2823,7 +2823,10 @@ Qed. Record extends' (m1 m2: mem) : Prop := mk_extends { mext_next: nextblock m1 = nextblock m2; - mext_inj: mem_inj inject_id m1 m2 + mext_inj: mem_inj inject_id m1 m2; + mext_perm_inv: forall b ofs k p, + perm m2 b ofs k p -> + perm m1 b ofs k p \/ ~perm m1 b ofs Max Nonempty }. Definition extends := extends'. @@ -2836,6 +2839,7 @@ Proof. intros. unfold inject_id in H; inv H. apply Z.divide_0_r. intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. apply memval_lessdef_refl. + tauto. Qed. Theorem load_extends: @@ -2890,10 +2894,11 @@ Proof. intros [m2' [A B]]. exists m2'; split. replace (ofs + 0) with ofs in A by omega. auto. - split; auto. + constructor; auto. rewrite (nextblock_store _ _ _ _ _ _ H0). rewrite (nextblock_store _ _ _ _ _ _ A). auto. + intros. exploit mext_perm_inv0; intuition eauto using perm_store_1, perm_store_2. Qed. Theorem store_outside_extends: @@ -2907,6 +2912,7 @@ Proof. rewrite (nextblock_store _ _ _ _ _ _ H0). auto. eapply store_outside_inj; eauto. unfold inject_id; intros. inv H2. eapply H1; eauto. omega. + intros. eauto using perm_store_2. Qed. Theorem storev_extends: @@ -2940,10 +2946,11 @@ Proof. intros [m2' [A B]]. exists m2'; split. replace (ofs + 0) with ofs in A by omega. auto. - split; auto. + constructor; auto. rewrite (nextblock_storebytes _ _ _ _ _ H0). rewrite (nextblock_storebytes _ _ _ _ _ A). auto. + intros. exploit mext_perm_inv0; intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. Theorem storebytes_outside_extends: @@ -2957,6 +2964,7 @@ Proof. rewrite (nextblock_storebytes _ _ _ _ _ H0). auto. eapply storebytes_outside_inj; eauto. unfold inject_id; intros. inv H2. eapply H1; eauto. omega. + intros. eauto using perm_storebytes_2. Qed. Theorem alloc_extends: @@ -2988,6 +2996,15 @@ Proof. eapply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. omega. + intros. eapply perm_alloc_inv in H; eauto. + generalize (perm_alloc_inv _ _ _ _ _ H0 b0 ofs Max Nonempty); intros PERM. + destruct (eq_block b0 b). + subst b0. + assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by omega. + destruct EITHER. + left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. + right; tauto. + exploit mext_perm_inv0; intuition eauto using perm_alloc_1, perm_alloc_4. Qed. Theorem free_left_extends: @@ -2999,6 +3016,10 @@ Proof. intros. inv H. constructor. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_left_inj; eauto. + intros. exploit mext_perm_inv0; eauto. intros [A|A]. + eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto. + subst b0. right; eapply perm_free_2; eauto. + intuition eauto using perm_free_3. Qed. Theorem free_right_extends: @@ -3012,6 +3033,7 @@ Proof. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_right_inj; eauto. unfold inject_id; intros. inv H. eapply H1; eauto. omega. + intros. eauto using perm_free_3. Qed. Theorem free_parallel_extends: @@ -3029,13 +3051,17 @@ Proof. eapply perm_inj with (b1 := b); eauto. eapply free_range_perm; eauto. destruct X as [m2' FREE]. exists m2'; split; auto. - inv H. constructor. + constructor. rewrite (nextblock_free _ _ _ _ _ H0). rewrite (nextblock_free _ _ _ _ _ FREE). auto. eapply free_right_inj with (m1 := m1'); eauto. eapply free_left_inj; eauto. - unfold inject_id; intros. inv H. + unfold inject_id; intros. inv H1. eapply perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto. + intros. exploit mext_perm_inv0; eauto using perm_free_3. intros [A|A]. + eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto. + subst b0. right; eapply perm_free_2; eauto. + right; intuition eauto using perm_free_3. Qed. Theorem valid_block_extends: @@ -3054,6 +3080,13 @@ Proof. eapply perm_inj; eauto. Qed. +Theorem perm_extends_inv: + forall m1 m2 b ofs k p, + extends m1 m2 -> perm m2 b ofs k p -> perm m1 b ofs k p \/ ~perm m1 b ofs Max Nonempty. +Proof. + intros. inv H; eauto. +Qed. + Theorem valid_access_extends: forall m1 m2 chunk b ofs p, extends m1 m2 -> valid_access m1 chunk b ofs p -> valid_access m2 chunk b ofs p. @@ -3110,7 +3143,12 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop := forall b b' delta ofs, f b = Some(b', delta) -> perm m1 b (Int.unsigned ofs) Max Nonempty \/ perm m1 b (Int.unsigned ofs - 1) Max Nonempty -> - delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned + delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned; + mi_perm_inv: + forall b1 ofs b2 delta k p, + f b1 = Some(b2, delta) -> + perm m2 b2 (ofs + delta) k p -> + perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty }. Definition inject := inject'. @@ -3148,6 +3186,16 @@ Proof. intros. inv H0. eapply perm_inj; eauto. Qed. +Theorem perm_inject_inv: + forall f m1 m2 b1 ofs b2 delta k p, + inject f m1 m2 -> + f b1 = Some(b2, delta) -> + perm m2 b2 (ofs + delta) k p -> + perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty. +Proof. + intros. eapply mi_perm_inv; eauto. +Qed. + Theorem range_perm_inject: forall f m1 m2 b1 b2 delta lo hi k p, f b1 = Some(b2, delta) -> @@ -3433,6 +3481,9 @@ Proof. (* representable *) intros. eapply mi_representable; try eassumption. destruct H4; eauto with mem. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto using perm_store_2. + intuition eauto using perm_store_1, perm_store_2. Qed. Theorem store_unmapped_inject: @@ -3455,6 +3506,9 @@ Proof. (* representable *) intros. eapply mi_representable; try eassumption. destruct H3; eauto with mem. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto using perm_store_2. + intuition eauto using perm_store_1, perm_store_2. Qed. Theorem store_outside_inject: @@ -3478,6 +3532,8 @@ Proof. auto. (* representable *) eauto with mem. +(* perm inv *) + intros. eauto using perm_store_2. Qed. Theorem storev_mapped_inject: @@ -3521,6 +3577,9 @@ Proof. (* representable *) intros. eapply mi_representable0; eauto. destruct H4; eauto using perm_storebytes_2. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. + intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. Theorem storebytes_unmapped_inject: @@ -3543,6 +3602,9 @@ Proof. (* representable *) intros. eapply mi_representable0; eauto. destruct H3; eauto using perm_storebytes_2. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto. + intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. Theorem storebytes_outside_inject: @@ -3566,6 +3628,8 @@ Proof. auto. (* representable *) auto. +(* perm inv *) + intros. eapply mi_perm_inv0; eauto using perm_storebytes_2. Qed. Theorem storebytes_empty_inject: @@ -3587,6 +3651,9 @@ Proof. (* representable *) intros. eapply mi_representable0; eauto. destruct H3; eauto using perm_storebytes_2. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. + intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. (* Preservation of allocations *) @@ -3609,6 +3676,10 @@ Proof. auto. (* representable *) auto. +(* perm inv *) + intros. eapply perm_alloc_inv in H2; eauto. destruct (eq_block b0 b2). + subst b0. eelim fresh_block_alloc; eauto. + eapply mi_perm_inv0; eauto. Qed. Theorem alloc_left_unmapped_inject: @@ -3652,6 +3723,10 @@ Proof. destruct (eq_block b b1); try discriminate. eapply mi_representable0; try eassumption. destruct H4; eauto using perm_alloc_4. +(* perm inv *) + intros. unfold f' in H3; destruct (eq_block b0 b1); try discriminate. + exploit mi_perm_inv0; eauto. + intuition eauto using perm_alloc_1, perm_alloc_4. (* incr *) split. auto. (* image *) @@ -3734,6 +3809,14 @@ Proof. generalize (Int.unsigned_range_2 ofs). omega. eapply mi_representable0; try eassumption. destruct H10; eauto using perm_alloc_4. +(* perm inv *) + intros. unfold f' in H9; destruct (eq_block b0 b1). + inversion H9; clear H9; subst b0 b3 delta0. + assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by omega. + destruct EITHER. + left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. + right; intros A. eapply perm_alloc_inv in A; eauto. rewrite dec_eq_true in A. tauto. + exploit mi_perm_inv0; eauto. intuition eauto using perm_alloc_1, perm_alloc_4. (* incr *) split. auto. (* image of b1 *) @@ -3790,6 +3873,10 @@ Proof. (* representable *) intros. eapply mi_representable0; try eassumption. destruct H2; eauto with mem. +(* perm inv *) + intros. exploit mi_perm_inv0; eauto. intuition eauto using perm_free_3. + eapply perm_free_inv in H4; eauto. destruct H4 as [[A B] | A]; auto. + subst b1. right; eapply perm_free_2; eauto. Qed. Lemma free_list_left_inject: @@ -3825,6 +3912,8 @@ Proof. auto. (* representable *) auto. +(* perm inv *) + intros. eauto using perm_free_3. Qed. Lemma perm_free_list: @@ -3900,6 +3989,7 @@ Proof. intros. destruct H. constructor; eauto. eapply drop_outside_inj; eauto. intros. unfold valid_block in *. erewrite nextblock_drop; eauto. + intros. eapply mi_perm_inv0; eauto using perm_drop_4. Qed. (** Composing two memory injections. *) @@ -3973,6 +4063,15 @@ Proof. ((Int.unsigned ofs - 1) + delta1) by omega. destruct H0; eauto using perm_inj. rewrite H. omega. +(* perm inv *) + intros. + destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. + destruct (f' b') as [[b'' delta''] |] eqn:?; try discriminate. + inversion H; clear H; subst b'' delta. + replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') in H0 by omega. + exploit mi_perm_inv1; eauto. intros [A|A]. + eapply mi_perm_inv0; eauto. + right; red; intros. elim A. eapply perm_inj; eauto. Qed. Lemma val_lessdef_inject_compose: @@ -4007,6 +4106,10 @@ Proof. (* representable *) eapply mi_representable0; eauto. destruct H1; eauto using perm_extends. +(* perm inv *) + exploit mi_perm_inv0; eauto. intros [A|A]. + eapply mext_perm_inv0; eauto. + right; red; intros; elim A. eapply perm_extends; eauto. Qed. Lemma inject_extends_compose: @@ -4026,19 +4129,27 @@ Proof. red; intros. eapply mi_no_overlap0; eauto. (* representable *) eapply mi_representable0; eauto. +(* perm inv *) + exploit mext_perm_inv0; eauto. intros [A|A]. + eapply mi_perm_inv0; eauto. + right; red; intros; elim A. eapply perm_inj; eauto. Qed. Lemma extends_extends_compose: forall m1 m2 m3, extends m1 m2 -> extends m2 m3 -> extends m1 m3. Proof. - intros. inv H; inv H0; constructor; intros. + intros. inversion H; subst; inv H0; constructor; intros. (* nextblock *) congruence. (* meminj *) replace inject_id with (compose_meminj inject_id inject_id). eapply mem_inj_compose; eauto. apply extensionality; intros. unfold compose_meminj, inject_id. auto. + (* perm inv *) + exploit mext_perm_inv1; eauto. intros [A|A]. + eapply mext_perm_inv0; eauto. + right; red; intros; elim A. eapply perm_extends; eauto. Qed. (** Injecting a memory into itself. *) @@ -4075,6 +4186,10 @@ Proof. (* range *) unfold flat_inj; intros. destruct (plt b (nextblock m)); inv H0. generalize (Int.unsigned_range_2 ofs); omega. +(* perm inv *) + unfold flat_inj; intros. + destruct (plt b1 (nextblock m)); inv H0. + rewrite Zplus_0_r in H1; auto. Qed. Theorem empty_inject_neutral: diff --git a/common/Separation.v b/common/Separation.v index 4d87443b..6a7ffbea 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -627,6 +627,10 @@ Next Obligation. - intros. eapply Mem.valid_block_unchanged_on; eauto. - assumption. - assumption. +- intros. destruct (Mem.perm_dec m0 b1 ofs Max Nonempty); auto. + eapply mi_perm_inv; eauto. + eapply Mem.perm_unchanged_on_2; eauto. + eapply IMG; eauto. Qed. Next Obligation. eapply Mem.valid_block_inject_2; eauto. diff --git a/driver/Assembler.ml b/driver/Assembler.ml new file mode 100644 index 00000000..52fb17d8 --- /dev/null +++ b/driver/Assembler.ml @@ -0,0 +1,47 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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 Clflags +open Commandline +open Driveraux + +(* From asm to object file *) + +let assemble ifile ofile = + let cmd = List.concat [ + Configuration.asm; + ["-o"; ofile]; + List.rev !assembler_options; + [ifile] + ] in + let exc = command cmd in + if exc <> 0 then begin + safe_remove ofile; + command_error "assembler" exc; + exit 2 + end + +let assembler_actions = + [ Prefix "-Wa,", Self (fun s -> if gnu_system then + assembler_options := s :: !assembler_options + else + assembler_options := List.rev_append (explode_comma_option s) !assembler_options); + Exact "-Xassembler", String (fun s -> if gnu_system then + assembler_options := s::"-Xassembler":: !assembler_options + else + assembler_options := s::!assembler_options );] + +let assembler_help = +"Assembling options:\n\ +\ -Wa,<opt> Pass option <opt> to the assembler\n\ +\ -Xassembler <opt> Pass <opt> as an option to the assembler\n" diff --git a/driver/Assembler.mli b/driver/Assembler.mli new file mode 100644 index 00000000..d8a4e32b --- /dev/null +++ b/driver/Assembler.mli @@ -0,0 +1,21 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +val assemble: string -> string -> unit + (** From asm to object file *) + +val assembler_actions: (Commandline.pattern * Commandline.action) list + (** Commandline optins affecting the assembler *) + +val assembler_help: string + (** Commandline help description *) diff --git a/driver/Driver.ml b/driver/Driver.ml index b8c92d6c..7311215d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -16,6 +16,8 @@ open Clflags open Timing open Driveraux open Frontend +open Assembler +open Linker let dump_options = ref false @@ -108,40 +110,6 @@ let compile_cminor_file ifile ofile = ifile msg; exit 2 -(* From asm to object file *) - -let assemble ifile ofile = - let cmd = List.concat [ - Configuration.asm; - ["-o"; ofile]; - List.rev !assembler_options; - [ifile] - ] in - let exc = command cmd in - if exc <> 0 then begin - safe_remove ofile; - command_error "assembler" exc; - exit 2 - end - -(* Linking *) - -let linker exe_name files = - let cmd = List.concat [ - Configuration.linker; - ["-o"; exe_name]; - files; - (if Configuration.has_runtime_lib - then ["-L" ^ !stdlib_path; "-lcompcert"] - else []) - ] in - let exc = command cmd in - if exc <> 0 then begin - command_error "linker" exc; - exit 2 - end - - (* Processing of a .c file *) let process_c_file sourcename = @@ -271,28 +239,33 @@ let process_h_file sourcename = exit 2 end -(* Record actions to be performed after parsing the command line *) - -let actions : ((string -> string) * string) list ref = ref [] - -let push_action fn arg = - actions := (fn, arg) :: !actions - -let push_linker_arg arg = - push_action (fun s -> s) arg - -let perform_actions () = - let rec perform = function - | [] -> [] - | (fn, arg) :: rem -> let res = fn arg in res :: perform rem - in perform (List.rev !actions) - let version_string = if Version.buildnr <> "" && Version.tag <> "" then sprintf "The CompCert C verified compiler, %s, Build: %s, Tag: %s\n" Version.version Version.buildnr Version.tag else "The CompCert C verified compiler, version "^ Version.version ^ "\n" +let gnu_system = Configuration.system <> "diab" + +let gnu_debugging_help = +" -gdwarf- Generate debug information in DWARF v2 or DWARF v3\n" + +let debugging_help = +"Debugging options:\n\ +\ -g Generate debugging information\n\ +\ -gdepth <n> Control generation of debugging information\n\ +\ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals\n\ +\ without locations, <n>=3: full;)\n" +^ (if gnu_system then gnu_debugging_help else "")^ +" -frename-static Rename static functions and declarations\n" + +let target_help = if Configuration.arch = "arm" then +"Target processor options:\n\ +\ -mthumb Use Thumb2 instruction encoding\n\ +\ -marm Use classic ARM instruction encoding\n" +else + "" + let usage_string = version_string ^ "Usage: ccomp [options] <source files>\n\ @@ -321,15 +294,9 @@ Processing options:\n\ \ -fpacked-structs Emulate packed structs [off]\n\ \ -finline-asm Support inline 'asm' statements [off]\n\ \ -fall Activate all language support options above\n\ -\ -fnone Turn off all language support options above\n\ -Debugging options:\n\ -\ -g Generate debugging information\n\ -\ -gdwarf- (GCC only) Generate debug information in DWARF v2 or DWARF v3\n\ -\ -gdepth <n> Control generation of debugging information\n\ -\ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals\n\ -\ without locations, <n>=3: full;)\n\ -\ -frename-static Rename static functions and declarations\n\ -Optimization options: (use -fno-<opt> to turn off -f<opt>)\n\ +\ -fnone Turn off all language support options above\n" ^ + debugging_help ^ +"Optimization options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -O Optimize the compiled code [on by default]\n\ \ -O0 Do not optimize the compiled code\n\ \ -O1 -O2 -O3 Synonymous for -O\n\ @@ -346,32 +313,11 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -fsmall-const <n> Set maximal size <n> for allocation in small constant area\n\ \ -falign-functions <n> Set alignment (in bytes) of function entry points\n\ \ -falign-branch-targets <n> Set alignment (in bytes) of branch targets\n\ -\ -falign-cond-branches <n> Set alignment (in bytes) of conditional branches\n\ -Target processor options:\n\ -\ -mthumb (ARM only) Use Thumb2 instruction encoding\n\ -\ -marm (ARM only) Use classic ARM instruction encoding\n\ -Assembling options:\n\ -\ -Wa,<opt> Pass option <opt> to the assembler\n\ -\ -Xassembler <opt> Pass <opt> as an option to the assembler\n\ -Linking options:\n\ -\ -l<lib> Link library <lib>\n\ -\ -L<dir> Add <dir> to search path for libraries\n\ -\ -nostartfiles (GCC only) Do not use the standard system startup files when\n\ -\ linking\n\ -\ -nodefaultlibs (GCC only) Do not use the standard system libraries when\n\ -\ linking\n\ -\ -nostdlib (GCC only) Do not use the standard system startup files or\n\ -\ libraries when linking\n\ -\ -s Remove all symbol table and relocation information from the\n\ -\ executable\n\ -\ -static Prevent linking with the shared libraries\n\ -\ -T <file> Use <file> as linker command file\n\ -\ -Wl,<opt> Pass option <opt> to the linker\n\ -\ -WUl,<opt> (GCC only) Pass option <opt> to the gcc used for linking\n\ -\ -Xlinker <opt> Pass <opt> as an option to the linker\n\ -\ -u <symb> Pretend the symbol <symb> is undefined to force linking of\n\ -\ library modules to define it.\n\ -Tracing options:\n\ +\ -falign-cond-branches <n> Set alignment (in bytes) of conditional branches\n" ^ + target_help ^ + assembler_help ^ + linker_help ^ +"Tracing options:\n\ \ -dprepro Save C file after preprocessing in <file>.i\n\ \ -dparse Save C file after parsing and elaboration in <file>.parsed.c\n\ \ -dc Save generated Compcert C in <file>.compcert.c\n\ @@ -414,10 +360,6 @@ let optimization_options = [ let set_all opts = List.iter (fun r -> r := true) opts let unset_all opts = List.iter (fun r -> r := false) opts -let gnu_linker_opt s = - if gnu_option s then - push_linker_arg s - let num_source_files = ref 0 let num_input_files = ref 0 @@ -446,12 +388,13 @@ let cmdline_actions = Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) Exact "-g", Self (fun s -> option_g := true; - option_gdwarf := 3); - Exact "-gdwarf-2", Self (fun s -> option_g:=true; + option_gdwarf := 3);] @ + (if gnu_system then + [ Exact "-gdwarf-2", Self (fun s -> option_g:=true; option_gdwarf := 2); Exact "-gdwarf-3", Self (fun s -> option_g := true; - option_gdwarf := 3); - Exact "-frename-static", Self (fun s -> option_rename_static:= true); + option_gdwarf := 3);] else []) @ + [ Exact "-frename-static", Self (fun s -> option_rename_static:= true); Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin option_g := false end else begin @@ -471,41 +414,17 @@ let cmdline_actions = Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n); (* Target processor options *) Exact "-conf", String (fun _ -> ()); (* Ignore option since it is already handled *) - Exact "-target", String (fun _ -> ()); (* Ignore option since it is already handled *) - Exact "-mthumb", Set option_mthumb; - Exact "-marm", Unset option_mthumb; + Exact "-target", String (fun _ -> ());] @ (* Ignore option since it is already handled *) + (if Configuration.arch = "arm" then + [ Exact "-mthumb", Set option_mthumb; + Exact "-marm", Unset option_mthumb; ] + else []) @ (* Assembling options *) - Prefix "-Wa,", Self (fun s -> if Configuration.system = "diab" then - assembler_options := List.rev_append (explode_comma_option s) !assembler_options - else - assembler_options := s :: !assembler_options); - Exact "-Xassembler", String (fun s -> if Configuration.system = "diab" then - assembler_options := s::!assembler_options - else - assembler_options := s::"-Xassembler":: !assembler_options); + assembler_actions @ (* Linking options *) - Prefix "-l", Self push_linker_arg; - Prefix "-L", Self push_linker_arg; - Exact "-nostartfiles", Self gnu_linker_opt; - Exact "-nodefaultlibs", Self gnu_linker_opt; - Exact "-nostdlib", Self gnu_linker_opt; - Exact "-s", Self push_linker_arg; - Exact "-static", Self push_linker_arg; - Exact "-T", String (fun s -> if Configuration.system = "diab" then - push_linker_arg ("-Wm"^s) - else begin - push_linker_arg ("-T"); - push_linker_arg(s) - end); - Exact "-Xlinker", String (fun s -> if Configuration.system = "diab" then - push_linker_arg ("-Wl,"^s) - else - push_linker_arg s); - Prefix "-Wl,", Self push_linker_arg; - Prefix "-WUl,", Self (fun s -> List.iter push_linker_arg (explode_comma_option s)); - Exact "-u", Self push_linker_arg; + linker_actions @ (* Tracing options *) - Exact "-dprepro", Set option_dprepro; + [ Exact "-dprepro", Set option_dprepro; Exact "-dparse", Set option_dparse; Exact "-dc", Set option_dcmedium; Exact "-dclight", Set option_dclight; @@ -529,7 +448,7 @@ let cmdline_actions = Exact "-trace", Self (fun _ -> Interp.trace := 2); Exact "-random", Self (fun _ -> Interp.mode := Interp.Random); Exact "-all", Self (fun _ -> Interp.mode := Interp.All) - ] + ] (* -f options: come in -f and -fno- variants *) (* Language support options *) @ f_opt "longdouble" option_flongdouble diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index b5d155d4..3fe22fac 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -94,17 +94,26 @@ let print_error oc msg = List.iter print_one_error msg; output_char oc '\n' -let gnu_option s = - if Configuration.system <> "diab" then - true - else begin - eprintf "ccomp: warning: option %s only supported for gcc backend\n" s; - false - end - +let gnu_system = Configuration.system <> "diab" (* Command-line parsing *) let explode_comma_option s = match Str.split (Str.regexp ",") s with | [] -> assert false | _ :: tl -> tl + +(* Record actions to be performed after parsing the command line *) + +let actions : ((string -> string) * string) list ref = ref [] + +let push_action fn arg = + actions := (fn, arg) :: !actions + +let push_linker_arg arg = + push_action (fun s -> s) arg + +let perform_actions () = + let rec perform = function + | [] -> [] + | (fn, arg) :: rem -> let res = fn arg in res :: perform rem + in perform (List.rev !actions) diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index 1cb219a1..60efcc80 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -36,8 +36,17 @@ val ensure_inputfile_exists: string -> unit val print_error:out_channel -> Errors.errcode list -> unit (** Printing of error messages *) -val gnu_option: string -> bool - (** Set the options for gnu systems *) +val gnu_system: bool + (** Are the target tools gnu tools? *) val explode_comma_option: string -> string list (** Split option at commas *) + +val push_action: (string -> string) -> string -> unit + (** Add an action to be performed after parsing the command line *) + +val push_linker_arg: string -> unit + (** Add a linker arguments *) + +val perform_actions: unit -> string list + (** Perform actions *) diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 44ad1700..043d4e5a 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -82,36 +82,18 @@ let parse_c_file sourcename ifile = (* Add gnu preprocessor list *) let gnu_prepro_opt_key key s = - if gnu_option s then - prepro_options := s::key::!prepro_options + prepro_options := s::key::!prepro_options (* Add gnu preprocessor option *) let gnu_prepro_opt s = - if gnu_option s then - prepro_options := s::!prepro_options + prepro_options := s::!prepro_options (* Add gnu preprocessor option s and the implict -E *) let gnu_prepro_opt_e s = - if gnu_option s then begin - prepro_options := s :: !prepro_options; - option_E := true - end + prepro_options := s :: !prepro_options; + option_E := true -let prepro_actions = [ - (* Preprocessing options *) - Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options; - assembler_options := s :: "-I" :: !assembler_options); - Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options; - assembler_options := s :: !assembler_options); - Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options); - Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options); - Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options); - Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options); - Prefix "-Wp,", Self (fun s -> - prepro_options := List.rev_append (explode_comma_option s) !prepro_options); - Exact "-Xpreprocessor", String (fun s -> - prepro_options := s :: !prepro_options); - Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options); +let gnu_prepro_actions = [ Exact "-M", Self gnu_prepro_opt_e; Exact "-MM", Self gnu_prepro_opt_e; Exact "-MF", String (gnu_prepro_opt_key "-MF"); @@ -128,36 +110,55 @@ let prepro_actions = [ Exact "-C", Self gnu_prepro_opt; Exact "-CC", Self gnu_prepro_opt;] -let prepro_help = "Preprocessing options:\n\ -\ -I<dir> Add <dir> to search path for #include files\n\ -\ -include <file> Process <file> as if #include \"<file>\" appears at the first\n\ -\ line of the primary source file.\n\ -\ -D<symb>=<val> Define preprocessor symbol\n\ -\ -U<symb> Undefine preprocessor symbol\n\ -\ -Wp,<opt> Pass option <opt> to the preprocessor\n\ -\ -Xpreprocessor <opt> Pass option <opt> to the preprocessor\n\ -\ -M (GCC only) Ouput a rule suitable for make describing the\n\ +let prepro_actions = [ + (* Preprocessing options *) + Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options; + assembler_options := s :: "-I" :: !assembler_options); + Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options; + assembler_options := s :: !assembler_options); + Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options); + Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options); + Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options); + Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options); + Prefix "-Wp,", Self (fun s -> + prepro_options := List.rev_append (explode_comma_option s) !prepro_options); + Exact "-Xpreprocessor", String (fun s -> + prepro_options := s :: !prepro_options); + Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options);] + @ (if gnu_system then gnu_prepro_actions else []) + +let gnu_prepro_help = +"\ -M Ouput a rule suitable for make describing the\n\ \ dependencies of the main source file\n\ -\ -MM (GCC only) Like -M but do not mention system header files\n\ -\ -MF <file> (GCC only) Specifies file <file> as output file for -M or -MM\n\ -\ -MG (GCC only) Assumes missing header files are generated for -M\n\ -\ -MP (GCC only) Add a phony target for each dependency other than\n\ +\ -MM Like -M but do not mention system header files\n\ +\ -MF <file> Specifies file <file> as output file for -M or -MM\n\ +\ -MG Assumes missing header files are generated for -M\n\ +\ -MP Add a phony target for each dependency other than\n\ \ the main file\n\ -\ -MT <target> (GCC only) Change the target of the rule emitted by dependency\n\ +\ -MT <target> Change the target of the rule emitted by dependency\n\ \ generation\n\ -\ -MQ <target> (GCC only) Like -MT but quotes <target>\n\ -\ -nostdinc (GCC only) Do not search the standard system directories for\n\ +\ -MQ <target> Like -MT but quotes <target>\n\ +\ -nostdinc Do not search the standard system directories for\n\ \ header files\n\ -\ -imacros <file> (GCC only) Like -include but throws output produced by\n\ +\ -imacros <file> Like -include but throws output produced by\n\ \ preprocessing of <file> away\n\ -\ -idirafter <dir> (GCC only) Search <dir> for header files after all directories\n\ +\ -idirafter <dir> Search <dir> for header files after all directories\n\ \ specified with -I and the standard system directories\n\ -\ -isystem <dir> (GCC only) Search <dir> for header files after all directories\n\ -\ +\ -isystem <dir> Search <dir> for header files after all directories\n\ \ specified by -I but before the standard system directories\n\ -\ -iquote <dir> (GCC only) Like -isystem but only for headers included with\n\ -\ quotes\n\ -\ -P (GCC only) Do not generate linemarkers\n\ -\ -C (GCC only) Do not discard comments\n\ -\ -CC (GCC only) Do not discard comments, including during macro\n\ +\ -iquote <dir> Like -isystem but only for headers included with\n\ +\ quotes\n\ +\ -P Do not generate linemarkers\n\ +\ -C Do not discard comments\n\ +\ -CC Do not discard comments, including during macro\n\ \ expansion\n" + +let prepro_help = "Preprocessing options:\n\ +\ -I<dir> Add <dir> to search path for #include files\n\ +\ -include <file> Process <file> as if #include \"<file>\" appears at the first\n\ +\ line of the primary source file.\n\ +\ -D<symb>=<val> Define preprocessor symbol\n\ +\ -U<symb> Undefine preprocessor symbol\n\ +\ -Wp,<opt> Pass option <opt> to the preprocessor\n\ +\ -Xpreprocessor <opt> Pass option <opt> to the preprocessor\n" + ^ (if gnu_system then gnu_prepro_help else "") diff --git a/driver/Frontend.mli b/driver/Frontend.mli index 689f382f..d0514d01 100644 --- a/driver/Frontend.mli +++ b/driver/Frontend.mli @@ -21,3 +21,4 @@ val prepro_actions: (Commandline.pattern * Commandline.action) list (** Commandline optins affecting the frontend *) val prepro_help: string + (** Commandline help description *) diff --git a/driver/Linker.ml b/driver/Linker.ml new file mode 100644 index 00000000..2f767023 --- /dev/null +++ b/driver/Linker.ml @@ -0,0 +1,81 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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 Clflags +open Commandline +open Driveraux + + +(* Linking *) + +let linker exe_name files = + let cmd = List.concat [ + Configuration.linker; + ["-o"; exe_name]; + files; + (if Configuration.has_runtime_lib + then ["-L" ^ !stdlib_path; "-lcompcert"] + else []) + ] in + let exc = command cmd in + if exc <> 0 then begin + command_error "linker" exc; + exit 2 + end + + +let gnu_linker_help = +" -nostartfiles Do not use the standard system startup files when\n\ +\ linking\n\ +\ -nodefaultlibs Do not use the standard system libraries when\n\ +\ linking\n\ +\ -nostdlib Do not use the standard system startup files or\n\ +\ libraries when linking\n" + +let linker_help = +"Linking options:\n\ +\ -l<lib> Link library <lib>\n\ +\ -L<dir> Add <dir> to search path for libraries\n" ^ + (if gnu_system then gnu_linker_help else "") ^ +" -s Remove all symbol table and relocation information from the\n\ +\ executable\n\ +\ -static Prevent linking with the shared libraries\n\ +\ -T <file> Use <file> as linker command file\n\ +\ -Wl,<opt> Pass option <opt> to the linker\n\ +\ -WUl,<opt> Pass option <opt> to the gcc or dcc used for linking\n\ +\ -Xlinker <opt> Pass <opt> as an option to the linker\n\ +\ -u <symb> Pretend the symbol <symb> is undefined to force linking of\n\ +\ library modules to define it.\n" + +let linker_actions = + [ Prefix "-l", Self push_linker_arg; + Prefix "-L", Self push_linker_arg; ] @ + (if gnu_system then + [ Exact "-nostartfiles", Self push_linker_arg; + Exact "-nodefaultlibs", Self push_linker_arg; + Exact "-nostdlib", Self push_linker_arg;] + else []) @ + [ Exact "-s", Self push_linker_arg; + Exact "-static", Self push_linker_arg; + Exact "-T", String (fun s -> if gnu_system then begin + push_linker_arg ("-T"); + push_linker_arg(s) + end else + push_linker_arg ("-Wm"^s)); + Exact "-Xlinker", String (fun s -> if Configuration.system = "diab" then + push_linker_arg ("-Wl,"^s) + else + push_linker_arg s); + Prefix "-Wl,", Self push_linker_arg; + Prefix "-WUl,", Self (fun s -> List.iter push_linker_arg (explode_comma_option s)); + Exact "-u", Self push_linker_arg;] diff --git a/driver/Linker.mli b/driver/Linker.mli new file mode 100644 index 00000000..3b92da05 --- /dev/null +++ b/driver/Linker.mli @@ -0,0 +1,21 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +val linker: string -> string list -> unit + (** Link files into executbale *) + +val linker_actions: (Commandline.pattern * Commandline.action) list + (** Commandline optins affecting the assembler *) + +val linker_help: string + (** Commandline help description *) |