From e8127be72ffc16f91de51c0b8dca3df0d3bd4745 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 6 Oct 2015 12:37:31 +0200 Subject: Push the linker args separate. --- driver/Driver.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 9b1a6e70..c7d9984e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -572,8 +572,10 @@ let cmdline_actions = Prefix "-L", Self push_linker_arg; Exact "-T", String (fun s -> if Configuration.system = "diab" then push_linker_arg ("-Wm"^s) - else - push_linker_arg ("-T "^s)); + else begin + push_linker_arg ("-T"); + push_linker_arg(s) + end); Prefix "-Wl,", Self push_linker_arg; (* Tracing options *) Exact "-dparse", Set option_dparse; -- cgit From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 11 Oct 2015 17:43:59 +0200 Subject: Use Coq strings instead of idents to name external and builtin functions. The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables. --- driver/Interp.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index f453af95..579b936d 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -59,7 +59,7 @@ let print_eventval_list p = function let print_event p = function | Event_syscall(id, args, res) -> fprintf p "extcall %s(%a) -> %a" - (extern_atom id) + (camlstring_of_coqstring id) print_eventval_list args print_eventval res | Event_vload(chunk, id, ofs, res) -> @@ -74,7 +74,7 @@ let print_event p = function print_eventval arg | Event_annot(text, args) -> fprintf p "annotation \"%s\" %a" - (extern_atom text) + (camlstring_of_coqstring text) print_eventval_list args (* Printing states *) @@ -387,7 +387,7 @@ let rec convert_external_args ge vl tl = | _, _ -> None let do_external_function id sg ge w args m = - match extern_atom id, args with + match camlstring_of_coqstring id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> print_string (do_printf m fmt args'); -- cgit From 60ab550a952c3d9719b2a91ec90c9b58769f6717 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:07:48 +0200 Subject: bug 17392: remove trailing whitespace in source files --- driver/Clflags.ml | 2 +- driver/Configuration.ml | 12 ++++++------ driver/Configuration.mli | 2 +- driver/Driver.ml | 8 ++++---- driver/Interp.ml | 12 ++++++------ 5 files changed, 18 insertions(+), 18 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index d9c21a9c..9d3697bd 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -52,7 +52,7 @@ let option_S = ref false let option_c = ref false let option_v = ref false let option_interp = ref false -let option_small_data = +let option_small_data = ref (if Configuration.arch = "powerpc" && Configuration.abi = "eabi" && Configuration.system = "diab" diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 41325368..1f05afd8 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -30,7 +30,7 @@ let ini_file_name = try List.find Sys.file_exists files with Not_found -> - begin + begin eprintf "Cannot find compcert.ini configuration file.\n"; exit 2 end @@ -73,19 +73,19 @@ let get_config_list key = let prepro = get_config_list "prepro" let asm = get_config_list "asm" let linker = get_config_list "linker" -let arch = +let arch = match get_config_string "arch" with | "powerpc"|"arm"|"ia32" as a -> a | v -> bad_config "arch" [v] let model = get_config_string "model" let abi = get_config_string "abi" let system = get_config_string "system" -let has_runtime_lib = +let has_runtime_lib = match get_config_string "has_runtime_lib" with | "true" -> true | "false" -> false | v -> bad_config "has_runtime_lib" [v] -let has_standard_headers = +let has_standard_headers = match get_config_string "has_standard_headers" with | "true" -> true | "false" -> false @@ -95,7 +95,7 @@ let stdlib_path = get_config_string "stdlib_path" else "" -let asm_supports_cfi = +let asm_supports_cfi = match get_config_string "asm_supports_cfi" with | "true" -> true | "false" -> false @@ -117,7 +117,7 @@ type struct_return_style = | SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *) | SR_int1to4 (* return by content if size is <= 4 *) | SR_int1to8 (* return by content if size is <= 8 *) - | SR_ref (* always return by assignment to a reference + | SR_ref (* always return by assignment to a reference given as extra argument *) let struct_passing_style = diff --git a/driver/Configuration.mli b/driver/Configuration.mli index f82ce213..1d048ac4 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -46,7 +46,7 @@ type struct_return_style = | SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *) | SR_int1to4 (* return by content if size is <= 4 *) | SR_int1to8 (* return by content if size is <= 8 *) - | SR_ref (* always return by assignment to a reference + | SR_ref (* always return by assignment to a reference given as extra argument *) val struct_passing_style: struct_passing_style diff --git a/driver/Driver.ml b/driver/Driver.ml index c7d9984e..4b58fb4d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -188,7 +188,7 @@ let compile_c_ast sourcename csyntax ofile debug = | Errors.Error msg -> eprintf "%s: %a" sourcename print_error msg; exit 2 in - (* Dump Asm in binary and JSON format *) + (* Dump Asm in binary and JSON format *) if !option_sdump then begin dump_asm asm (output_filename sourcename ".c" ".sdump"); @@ -518,7 +518,7 @@ let unset_all opts = List.iter (fun r -> r := false) opts let num_source_files = ref 0 let num_input_files = ref 0 - + let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in @@ -570,8 +570,8 @@ let cmdline_actions = (* Linking options *) Prefix "-l", Self push_linker_arg; Prefix "-L", Self push_linker_arg; - Exact "-T", String (fun s -> if Configuration.system = "diab" then - push_linker_arg ("-Wm"^s) + 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) diff --git a/driver/Interp.ml b/driver/Interp.ml index f453af95..b3bdc883 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -98,7 +98,7 @@ let name_of_function prog fn = in find_name prog.prog_defs let invert_local_variable e b = - Maps.PTree.fold + Maps.PTree.fold (fun res id (b', _) -> if b = b' then Some id else res) e None @@ -176,7 +176,7 @@ let rec compare_cont k1 k2 = match k1, k2 with | Kstop, Kstop -> 0 | Kdo k1, Kdo k2 -> compare_cont k1 k2 - | Kseq(s1, k1), Kseq(s2, k2) -> + | Kseq(s1, k1), Kseq(s2, k2) -> let c = compare s1 s2 in if c <> 0 then c else compare_cont k1 k2 | Kifthenelse(s1, s1', k1), Kifthenelse(s2, s2', k2) -> let c = compare (s1,s1') (s2,s2') in @@ -273,7 +273,7 @@ let extract_string m blk ofs = if c = '\000' then begin Some(Buffer.contents b) end else begin - Buffer.add_char b c; + Buffer.add_char b c; extract blk (Z.succ ofs) end | _ -> @@ -325,7 +325,7 @@ let format_value m flags length conv arg = | 'p', "", _ -> "" | _, _, _ -> - "" + "" let do_printf m fmt args = @@ -374,7 +374,7 @@ let convert_external_arg ge v t = | Vfloat f, AST.Tfloat -> Some (EVfloat f) | Vsingle f, AST.Tsingle -> Some (EVsingle f) | Vlong n, AST.Tlong -> Some (EVlong n) - | Vptr(b, ofs), AST.Tint -> + | Vptr(b, ofs), AST.Tint -> Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) | _, _ -> None @@ -565,7 +565,7 @@ let rec explore_all p prog ge time states = if nextstates <> [] then explore_all p prog ge (time + 1) nextstates (* The variant of the source program used to build the world for - executing events. + executing events. Volatile variables are turned into non-volatile ones, so that reads and writes can be performed. Other variables are turned into empty vars, so that -- cgit From f5bb397acd12292f6b41438778f2df7391d6f2fe Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:26:56 +0200 Subject: bug 17392: remove trailing whitespace in source files --- driver/Compiler.v | 48 ++++++++++++++++++++++++------------------------ driver/Complements.v | 24 ++++++++++++------------ 2 files changed, 36 insertions(+), 36 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 3920665e..ea5849ec 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -159,7 +159,7 @@ Definition transf_cminor_program (p: Cminor.program) : res Asm.program := @@@ transf_rtl_program. Definition transf_clight_program (p: Clight.program) : res Asm.program := - OK p + OK p @@ print print_Clight @@@ time "Simplification of locals" SimplLocals.transf_program @@@ time "C#minor generation" Cshmgen.transl_program @@ -167,7 +167,7 @@ Definition transf_clight_program (p: Clight.program) : res Asm.program := @@@ transf_cminor_program. Definition transf_c_program (p: Csyntax.program) : res Asm.program := - OK p + OK p @@@ time "Clight generation" SimplExpr.transl_program @@@ transf_clight_program. @@ -182,14 +182,14 @@ Lemma print_identity: forall (A: Type) (printer: A -> unit) (prog: A), print printer prog = prog. Proof. - intros; unfold print. destruct (printer prog); auto. + intros; unfold print. destruct (printer prog); auto. Qed. Lemma compose_print_identity: - forall (A: Type) (x: res A) (f: A -> unit), + forall (A: Type) (x: res A) (f: A -> unit), x @@ print f = x. Proof. - intros. destruct x; simpl. rewrite print_identity. auto. auto. + intros. destruct x; simpl. rewrite print_identity. auto. auto. Qed. Remark forward_simulation_identity: @@ -199,8 +199,8 @@ Proof. - auto. - exists s1; auto. - subst s2; auto. -- subst s2. exists s1'; auto. -Qed. +- subst s2. exists s1'; auto. +Qed. Lemma total_if_simulation: forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> A) (prog: A), @@ -259,15 +259,15 @@ Proof. destruct (partial_if debug Debugvar.transf_program p7) as [p71|] eqn:?; simpl in H; try discriminate. destruct (Stacking.transf_program p71) as [p8|] eqn:?; simpl in H; try discriminate. apply compose_forward_simulation with (RTL.semantics p1). - apply total_if_simulation. apply Tailcallproof.transf_program_correct. + apply total_if_simulation. apply Tailcallproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p11). apply Inliningproof.transf_program_correct; auto. apply compose_forward_simulation with (RTL.semantics p12). - apply Renumberproof.transf_program_correct. + apply Renumberproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p2). apply total_if_simulation. apply Constpropproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p21). - apply total_if_simulation. apply Renumberproof.transf_program_correct. + apply total_if_simulation. apply Renumberproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p3). eapply partial_if_simulation; eauto. apply CSEproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p31). @@ -281,7 +281,7 @@ Proof. apply compose_forward_simulation with (Linear.semantics p6). apply Linearizeproof.transf_program_correct; auto. apply compose_forward_simulation with (Linear.semantics p7). - apply CleanupLabelsproof.transf_program_correct. + apply CleanupLabelsproof.transf_program_correct. apply compose_forward_simulation with (Linear.semantics p71). eapply partial_if_simulation; eauto. apply Debugvarproof.transf_program_correct. apply compose_forward_simulation with (Mach.semantics Asmgenproof0.return_address_offset p8). @@ -289,8 +289,8 @@ Proof. exact Asmgenproof.return_address_exists. auto. apply Asmgenproof.transf_program_correct; eauto. - split. auto. - apply forward_to_backward_simulation. auto. + split. auto. + apply forward_to_backward_simulation. auto. apply RTL.semantics_receptive. apply Asm.semantics_determinate. Qed. @@ -305,15 +305,15 @@ Proof. assert (F: forward_simulation (Cminor.semantics p) (Asm.semantics tp)). unfold transf_cminor_program, time in H. repeat rewrite compose_print_identity in H. - simpl in H. + simpl in H. destruct (Selection.sel_program p) as [p1|] eqn:?; simpl in H; try discriminate. destruct (RTLgen.transl_program p1) as [p2|] eqn:?; simpl in H; try discriminate. eapply compose_forward_simulation. apply Selectionproof.transf_program_correct. eauto. eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption. exact (fst (transf_rtl_program_correct _ _ H)). - split. auto. - apply forward_to_backward_simulation. auto. + split. auto. + apply forward_to_backward_simulation. auto. apply Cminor.semantics_receptive. apply Asm.semantics_determinate. Qed. @@ -324,7 +324,7 @@ Theorem transf_clight_program_correct: forward_simulation (Clight.semantics1 p) (Asm.semantics tp) * backward_simulation (Clight.semantics1 p) (Asm.semantics tp). Proof. - intros. + intros. assert (F: forward_simulation (Clight.semantics1 p) (Asm.semantics tp)). revert H; unfold transf_clight_program, time; simpl. rewrite print_identity. @@ -335,10 +335,10 @@ Proof. eapply compose_forward_simulation. apply SimplLocalsproof.transf_program_correct. eauto. eapply compose_forward_simulation. apply Cshmgenproof.transl_program_correct. eauto. eapply compose_forward_simulation. apply Cminorgenproof.transl_program_correct. eauto. - exact (fst (transf_cminor_program_correct _ _ EQ3)). + exact (fst (transf_cminor_program_correct _ _ EQ3)). - split. auto. - apply forward_to_backward_simulation. auto. + split. auto. + apply forward_to_backward_simulation. auto. apply Clight.semantics_receptive. apply Asm.semantics_determinate. Qed. @@ -355,9 +355,9 @@ Proof. caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0. intros EQ1. eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto. - exact (fst (transf_clight_program_correct _ _ EQ1)). + exact (fst (transf_clight_program_correct _ _ EQ1)). - split. auto. + split. auto. apply forward_to_backward_simulation. apply factor_forward_simulation. auto. eapply sd_traces. eapply Asm.semantics_determinate. apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive. @@ -369,10 +369,10 @@ Theorem transf_c_program_correct: transf_c_program p = OK tp -> backward_simulation (Csem.semantics p) (Asm.semantics tp). Proof. - intros. + intros. apply compose_backward_simulation with (atomic (Cstrategy.semantics p)). eapply sd_traces; eapply Asm.semantics_determinate. - apply factor_backward_simulation. + apply factor_backward_simulation. apply Cstrategy.strategy_simulation. apply Csem.semantics_single_events. eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive. diff --git a/driver/Complements.v b/driver/Complements.v index 57351a2a..8651f2ff 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -44,7 +44,7 @@ Theorem transf_c_program_preservation: program_behaves (Asm.semantics tp) beh -> exists beh', program_behaves (Csem.semantics p) beh' /\ behavior_improves beh' beh. Proof. - intros. eapply backward_simulation_behavior_improves; eauto. + intros. eapply backward_simulation_behavior_improves; eauto. apply transf_c_program_correct; auto. Qed. @@ -81,7 +81,7 @@ Proof. assert (WBT: forall p, well_behaved_traces (Cstrategy.semantics p)). intros. eapply ssr_well_behaved. apply Cstrategy.semantics_strongly_receptive. intros. intuition. - eapply forward_simulation_behavior_improves; eauto. + eapply forward_simulation_behavior_improves; eauto. apply (fst (transf_cstrategy_program_correct _ _ H)). exploit backward_simulation_behavior_improves. apply (snd (transf_cstrategy_program_correct _ _ H)). @@ -92,7 +92,7 @@ Proof. exploit backward_simulation_same_safe_behavior. apply (snd (transf_cstrategy_program_correct _ _ H)). intros. rewrite <- atomic_behaviors in H2; eauto. eauto. - intros. rewrite atomic_behaviors; auto. + intros. rewrite atomic_behaviors; auto. Qed. (** We can also use the alternate big-step semantics for [Cstrategy] @@ -114,7 +114,7 @@ Proof. apply behavior_bigstep_terminates with (Cstrategy.bigstep_semantics p); auto. apply Cstrategy.bigstep_semantics_sound. exploit (behavior_bigstep_diverges (Cstrategy.bigstep_semantics_sound p)). eassumption. - intros [A | [t [A B]]]. + intros [A | [t [A B]]]. left. apply transf_cstrategy_program_preservation with p; auto. red; auto. right; exists t; split; auto. apply transf_cstrategy_program_preservation with p; auto. red; auto. Qed. @@ -125,10 +125,10 @@ Qed. 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. + this specification as well. We first show this result for specifications that are stable - under the [behavior_improves] relation. *) + under the [behavior_improves] relation. *) Section SPECS_PRESERVED. @@ -145,7 +145,7 @@ Theorem transf_c_program_preserves_spec: Proof. intros. exploit transf_c_program_preservation; eauto. intros [beh' [A B]]. - apply spec_stable with beh'; auto. + apply spec_stable with beh'; auto. Qed. End SPECS_PRESERVED. @@ -166,9 +166,9 @@ Theorem transf_c_program_preserves_safety_spec: (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) -> (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh). Proof. - intros. eapply transf_c_program_preserves_spec; eauto. - intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]]. - subst beh1. elim (spec_safety _ H3). + intros. eapply transf_c_program_preserves_spec; eauto. + intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]]. + subst beh1. elim (spec_safety _ H3). Qed. End SAFETY_PRESERVED. @@ -196,8 +196,8 @@ Proof. destruct H2 as [t [C D]]. subst. destruct A as [b1 E]. destruct D as [b2 F]. destruct b1; simpl in E; inv E. - exists t1; split; auto. - exists (behavior_app t0 b2); apply behavior_app_assoc. + exists t1; split; auto. + exists (behavior_app t0 b2); apply behavior_app_assoc. Qed. End LIVENESS_PRESERVED. -- cgit From 24b4159b6a29328c529e0e59405e03ea192aa99e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 13:06:09 +0200 Subject: Implemented the usage of DW_AT_ranges for non-contiguous address ranges. The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392. --- driver/Clflags.ml | 1 + driver/Driver.ml | 8 +++++++- 2 files changed, 8 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 9d3697bd..b0c24f08 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -46,6 +46,7 @@ let option_dmach = ref false let option_dasm = ref false let option_sdump = ref false let option_g = ref false +let option_gdwarf = ref 2 let option_o = ref (None: string option) let option_E = ref false let option_S = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index 4b58fb4d..7459e030 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -444,6 +444,7 @@ Language support options (use -fno- to turn off -f) : -fnone Turn off all language support options above Debugging options: -g Generate debugging information + -gdwarf- (GCC only) Generate debug information in DWARF v2 or DWARF v3 -frename-static Rename static functions and declarations Optimization options: (use -fno- to turn off -f) -O Optimize the compiled code [on by default] @@ -549,7 +550,12 @@ let cmdline_actions = Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun s -> option_g := true); + Exact "-g", Self (fun s -> option_g := true; + option_gdwarf := 3); + 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); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); -- cgit From 8a95c3e07fd02eaa87f8cca447bc7d7c2642eb22 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 15:19:24 +0200 Subject: Do not dump the .sdump files. Bug 16529. --- driver/Driver.ml | 17 ++--------------- 1 file changed, 2 insertions(+), 15 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 7459e030..8fe6b07d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -144,17 +144,7 @@ let parse_c_file sourcename ifile = end; csyntax,None -(* Dump Asm code in binary format for the validator *) - -let sdump_magic_number = "CompCertSDUMP" ^ Version.version - -let dump_asm asm destfile = - let oc = open_out_bin destfile in - output_string oc sdump_magic_number; - output_value oc asm; - output_value oc Camlcoq.string_of_atom; - output_value oc C2C.decl_atom; - close_out oc +(* Dump Asm code in asm format for the validator *) let jdump_magic_number = "CompCertJDUMP" ^ Version.version @@ -190,10 +180,7 @@ let compile_c_ast sourcename csyntax ofile debug = exit 2 in (* Dump Asm in binary and JSON format *) if !option_sdump then - begin - dump_asm asm (output_filename sourcename ".c" ".sdump"); - dump_jasm asm (output_filename sourcename ".c" ".json") - end; + dump_jasm asm (output_filename sourcename ".c" ".json"); (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm debug; -- cgit From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- driver/Clflags.ml | 2 +- driver/Compiler.v | 48 ++++++++++++++++++++++++------------------------ driver/Complements.v | 24 ++++++++++++------------ driver/Configuration.ml | 12 ++++++------ driver/Configuration.mli | 2 +- driver/Driver.ml | 8 ++++---- driver/Interp.ml | 12 ++++++------ 7 files changed, 54 insertions(+), 54 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index d9c21a9c..9d3697bd 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -52,7 +52,7 @@ let option_S = ref false let option_c = ref false let option_v = ref false let option_interp = ref false -let option_small_data = +let option_small_data = ref (if Configuration.arch = "powerpc" && Configuration.abi = "eabi" && Configuration.system = "diab" diff --git a/driver/Compiler.v b/driver/Compiler.v index 3920665e..ea5849ec 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -159,7 +159,7 @@ Definition transf_cminor_program (p: Cminor.program) : res Asm.program := @@@ transf_rtl_program. Definition transf_clight_program (p: Clight.program) : res Asm.program := - OK p + OK p @@ print print_Clight @@@ time "Simplification of locals" SimplLocals.transf_program @@@ time "C#minor generation" Cshmgen.transl_program @@ -167,7 +167,7 @@ Definition transf_clight_program (p: Clight.program) : res Asm.program := @@@ transf_cminor_program. Definition transf_c_program (p: Csyntax.program) : res Asm.program := - OK p + OK p @@@ time "Clight generation" SimplExpr.transl_program @@@ transf_clight_program. @@ -182,14 +182,14 @@ Lemma print_identity: forall (A: Type) (printer: A -> unit) (prog: A), print printer prog = prog. Proof. - intros; unfold print. destruct (printer prog); auto. + intros; unfold print. destruct (printer prog); auto. Qed. Lemma compose_print_identity: - forall (A: Type) (x: res A) (f: A -> unit), + forall (A: Type) (x: res A) (f: A -> unit), x @@ print f = x. Proof. - intros. destruct x; simpl. rewrite print_identity. auto. auto. + intros. destruct x; simpl. rewrite print_identity. auto. auto. Qed. Remark forward_simulation_identity: @@ -199,8 +199,8 @@ Proof. - auto. - exists s1; auto. - subst s2; auto. -- subst s2. exists s1'; auto. -Qed. +- subst s2. exists s1'; auto. +Qed. Lemma total_if_simulation: forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> A) (prog: A), @@ -259,15 +259,15 @@ Proof. destruct (partial_if debug Debugvar.transf_program p7) as [p71|] eqn:?; simpl in H; try discriminate. destruct (Stacking.transf_program p71) as [p8|] eqn:?; simpl in H; try discriminate. apply compose_forward_simulation with (RTL.semantics p1). - apply total_if_simulation. apply Tailcallproof.transf_program_correct. + apply total_if_simulation. apply Tailcallproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p11). apply Inliningproof.transf_program_correct; auto. apply compose_forward_simulation with (RTL.semantics p12). - apply Renumberproof.transf_program_correct. + apply Renumberproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p2). apply total_if_simulation. apply Constpropproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p21). - apply total_if_simulation. apply Renumberproof.transf_program_correct. + apply total_if_simulation. apply Renumberproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p3). eapply partial_if_simulation; eauto. apply CSEproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p31). @@ -281,7 +281,7 @@ Proof. apply compose_forward_simulation with (Linear.semantics p6). apply Linearizeproof.transf_program_correct; auto. apply compose_forward_simulation with (Linear.semantics p7). - apply CleanupLabelsproof.transf_program_correct. + apply CleanupLabelsproof.transf_program_correct. apply compose_forward_simulation with (Linear.semantics p71). eapply partial_if_simulation; eauto. apply Debugvarproof.transf_program_correct. apply compose_forward_simulation with (Mach.semantics Asmgenproof0.return_address_offset p8). @@ -289,8 +289,8 @@ Proof. exact Asmgenproof.return_address_exists. auto. apply Asmgenproof.transf_program_correct; eauto. - split. auto. - apply forward_to_backward_simulation. auto. + split. auto. + apply forward_to_backward_simulation. auto. apply RTL.semantics_receptive. apply Asm.semantics_determinate. Qed. @@ -305,15 +305,15 @@ Proof. assert (F: forward_simulation (Cminor.semantics p) (Asm.semantics tp)). unfold transf_cminor_program, time in H. repeat rewrite compose_print_identity in H. - simpl in H. + simpl in H. destruct (Selection.sel_program p) as [p1|] eqn:?; simpl in H; try discriminate. destruct (RTLgen.transl_program p1) as [p2|] eqn:?; simpl in H; try discriminate. eapply compose_forward_simulation. apply Selectionproof.transf_program_correct. eauto. eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption. exact (fst (transf_rtl_program_correct _ _ H)). - split. auto. - apply forward_to_backward_simulation. auto. + split. auto. + apply forward_to_backward_simulation. auto. apply Cminor.semantics_receptive. apply Asm.semantics_determinate. Qed. @@ -324,7 +324,7 @@ Theorem transf_clight_program_correct: forward_simulation (Clight.semantics1 p) (Asm.semantics tp) * backward_simulation (Clight.semantics1 p) (Asm.semantics tp). Proof. - intros. + intros. assert (F: forward_simulation (Clight.semantics1 p) (Asm.semantics tp)). revert H; unfold transf_clight_program, time; simpl. rewrite print_identity. @@ -335,10 +335,10 @@ Proof. eapply compose_forward_simulation. apply SimplLocalsproof.transf_program_correct. eauto. eapply compose_forward_simulation. apply Cshmgenproof.transl_program_correct. eauto. eapply compose_forward_simulation. apply Cminorgenproof.transl_program_correct. eauto. - exact (fst (transf_cminor_program_correct _ _ EQ3)). + exact (fst (transf_cminor_program_correct _ _ EQ3)). - split. auto. - apply forward_to_backward_simulation. auto. + split. auto. + apply forward_to_backward_simulation. auto. apply Clight.semantics_receptive. apply Asm.semantics_determinate. Qed. @@ -355,9 +355,9 @@ Proof. caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0. intros EQ1. eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto. - exact (fst (transf_clight_program_correct _ _ EQ1)). + exact (fst (transf_clight_program_correct _ _ EQ1)). - split. auto. + split. auto. apply forward_to_backward_simulation. apply factor_forward_simulation. auto. eapply sd_traces. eapply Asm.semantics_determinate. apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive. @@ -369,10 +369,10 @@ Theorem transf_c_program_correct: transf_c_program p = OK tp -> backward_simulation (Csem.semantics p) (Asm.semantics tp). Proof. - intros. + intros. apply compose_backward_simulation with (atomic (Cstrategy.semantics p)). eapply sd_traces; eapply Asm.semantics_determinate. - apply factor_backward_simulation. + apply factor_backward_simulation. apply Cstrategy.strategy_simulation. apply Csem.semantics_single_events. eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive. diff --git a/driver/Complements.v b/driver/Complements.v index 57351a2a..8651f2ff 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -44,7 +44,7 @@ Theorem transf_c_program_preservation: program_behaves (Asm.semantics tp) beh -> exists beh', program_behaves (Csem.semantics p) beh' /\ behavior_improves beh' beh. Proof. - intros. eapply backward_simulation_behavior_improves; eauto. + intros. eapply backward_simulation_behavior_improves; eauto. apply transf_c_program_correct; auto. Qed. @@ -81,7 +81,7 @@ Proof. assert (WBT: forall p, well_behaved_traces (Cstrategy.semantics p)). intros. eapply ssr_well_behaved. apply Cstrategy.semantics_strongly_receptive. intros. intuition. - eapply forward_simulation_behavior_improves; eauto. + eapply forward_simulation_behavior_improves; eauto. apply (fst (transf_cstrategy_program_correct _ _ H)). exploit backward_simulation_behavior_improves. apply (snd (transf_cstrategy_program_correct _ _ H)). @@ -92,7 +92,7 @@ Proof. exploit backward_simulation_same_safe_behavior. apply (snd (transf_cstrategy_program_correct _ _ H)). intros. rewrite <- atomic_behaviors in H2; eauto. eauto. - intros. rewrite atomic_behaviors; auto. + intros. rewrite atomic_behaviors; auto. Qed. (** We can also use the alternate big-step semantics for [Cstrategy] @@ -114,7 +114,7 @@ Proof. apply behavior_bigstep_terminates with (Cstrategy.bigstep_semantics p); auto. apply Cstrategy.bigstep_semantics_sound. exploit (behavior_bigstep_diverges (Cstrategy.bigstep_semantics_sound p)). eassumption. - intros [A | [t [A B]]]. + intros [A | [t [A B]]]. left. apply transf_cstrategy_program_preservation with p; auto. red; auto. right; exists t; split; auto. apply transf_cstrategy_program_preservation with p; auto. red; auto. Qed. @@ -125,10 +125,10 @@ Qed. 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. + this specification as well. We first show this result for specifications that are stable - under the [behavior_improves] relation. *) + under the [behavior_improves] relation. *) Section SPECS_PRESERVED. @@ -145,7 +145,7 @@ Theorem transf_c_program_preserves_spec: Proof. intros. exploit transf_c_program_preservation; eauto. intros [beh' [A B]]. - apply spec_stable with beh'; auto. + apply spec_stable with beh'; auto. Qed. End SPECS_PRESERVED. @@ -166,9 +166,9 @@ Theorem transf_c_program_preserves_safety_spec: (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) -> (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh). Proof. - intros. eapply transf_c_program_preserves_spec; eauto. - intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]]. - subst beh1. elim (spec_safety _ H3). + intros. eapply transf_c_program_preserves_spec; eauto. + intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]]. + subst beh1. elim (spec_safety _ H3). Qed. End SAFETY_PRESERVED. @@ -196,8 +196,8 @@ Proof. destruct H2 as [t [C D]]. subst. destruct A as [b1 E]. destruct D as [b2 F]. destruct b1; simpl in E; inv E. - exists t1; split; auto. - exists (behavior_app t0 b2); apply behavior_app_assoc. + exists t1; split; auto. + exists (behavior_app t0 b2); apply behavior_app_assoc. Qed. End LIVENESS_PRESERVED. diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 41325368..1f05afd8 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -30,7 +30,7 @@ let ini_file_name = try List.find Sys.file_exists files with Not_found -> - begin + begin eprintf "Cannot find compcert.ini configuration file.\n"; exit 2 end @@ -73,19 +73,19 @@ let get_config_list key = let prepro = get_config_list "prepro" let asm = get_config_list "asm" let linker = get_config_list "linker" -let arch = +let arch = match get_config_string "arch" with | "powerpc"|"arm"|"ia32" as a -> a | v -> bad_config "arch" [v] let model = get_config_string "model" let abi = get_config_string "abi" let system = get_config_string "system" -let has_runtime_lib = +let has_runtime_lib = match get_config_string "has_runtime_lib" with | "true" -> true | "false" -> false | v -> bad_config "has_runtime_lib" [v] -let has_standard_headers = +let has_standard_headers = match get_config_string "has_standard_headers" with | "true" -> true | "false" -> false @@ -95,7 +95,7 @@ let stdlib_path = get_config_string "stdlib_path" else "" -let asm_supports_cfi = +let asm_supports_cfi = match get_config_string "asm_supports_cfi" with | "true" -> true | "false" -> false @@ -117,7 +117,7 @@ type struct_return_style = | SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *) | SR_int1to4 (* return by content if size is <= 4 *) | SR_int1to8 (* return by content if size is <= 8 *) - | SR_ref (* always return by assignment to a reference + | SR_ref (* always return by assignment to a reference given as extra argument *) let struct_passing_style = diff --git a/driver/Configuration.mli b/driver/Configuration.mli index f82ce213..1d048ac4 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -46,7 +46,7 @@ type struct_return_style = | SR_int1248 (* return by content if size is 1, 2, 4 or 8 bytes *) | SR_int1to4 (* return by content if size is <= 4 *) | SR_int1to8 (* return by content if size is <= 8 *) - | SR_ref (* always return by assignment to a reference + | SR_ref (* always return by assignment to a reference given as extra argument *) val struct_passing_style: struct_passing_style diff --git a/driver/Driver.ml b/driver/Driver.ml index c7d9984e..4b58fb4d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -188,7 +188,7 @@ let compile_c_ast sourcename csyntax ofile debug = | Errors.Error msg -> eprintf "%s: %a" sourcename print_error msg; exit 2 in - (* Dump Asm in binary and JSON format *) + (* Dump Asm in binary and JSON format *) if !option_sdump then begin dump_asm asm (output_filename sourcename ".c" ".sdump"); @@ -518,7 +518,7 @@ let unset_all opts = List.iter (fun r -> r := false) opts let num_source_files = ref 0 let num_input_files = ref 0 - + let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in @@ -570,8 +570,8 @@ let cmdline_actions = (* Linking options *) Prefix "-l", Self push_linker_arg; Prefix "-L", Self push_linker_arg; - Exact "-T", String (fun s -> if Configuration.system = "diab" then - push_linker_arg ("-Wm"^s) + 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) diff --git a/driver/Interp.ml b/driver/Interp.ml index 579b936d..fb1c85f0 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -98,7 +98,7 @@ let name_of_function prog fn = in find_name prog.prog_defs let invert_local_variable e b = - Maps.PTree.fold + Maps.PTree.fold (fun res id (b', _) -> if b = b' then Some id else res) e None @@ -176,7 +176,7 @@ let rec compare_cont k1 k2 = match k1, k2 with | Kstop, Kstop -> 0 | Kdo k1, Kdo k2 -> compare_cont k1 k2 - | Kseq(s1, k1), Kseq(s2, k2) -> + | Kseq(s1, k1), Kseq(s2, k2) -> let c = compare s1 s2 in if c <> 0 then c else compare_cont k1 k2 | Kifthenelse(s1, s1', k1), Kifthenelse(s2, s2', k2) -> let c = compare (s1,s1') (s2,s2') in @@ -273,7 +273,7 @@ let extract_string m blk ofs = if c = '\000' then begin Some(Buffer.contents b) end else begin - Buffer.add_char b c; + Buffer.add_char b c; extract blk (Z.succ ofs) end | _ -> @@ -325,7 +325,7 @@ let format_value m flags length conv arg = | 'p', "", _ -> "" | _, _, _ -> - "" + "" let do_printf m fmt args = @@ -374,7 +374,7 @@ let convert_external_arg ge v t = | Vfloat f, AST.Tfloat -> Some (EVfloat f) | Vsingle f, AST.Tsingle -> Some (EVsingle f) | Vlong n, AST.Tlong -> Some (EVlong n) - | Vptr(b, ofs), AST.Tint -> + | Vptr(b, ofs), AST.Tint -> Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) | _, _ -> None @@ -565,7 +565,7 @@ let rec explore_all p prog ge time states = if nextstates <> [] then explore_all p prog ge (time + 1) nextstates (* The variant of the source program used to build the world for - executing events. + executing events. Volatile variables are turned into non-volatile ones, so that reads and writes can be performed. Other variables are turned into empty vars, so that -- cgit From 94163429293cef7410320f79fc5964fc546fccef Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 23 Oct 2015 17:38:54 +0200 Subject: Added additional option for the renaming of the suffix of the sdump file. The new option -sdump-suffix allows it to specify another suffix for the sdump file. Bug 17326 --- driver/Driver.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 8fe6b07d..a0d742c2 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -20,6 +20,9 @@ open Timing let stdlib_path = ref Configuration.stdlib_path +(* Optional sdump suffix *) +let sdump_suffix = ref ".json" + (* Invocation of external tools *) let command ?stdout args = @@ -180,7 +183,7 @@ let compile_c_ast sourcename csyntax ofile debug = exit 2 in (* Dump Asm in binary and JSON format *) if !option_sdump then - dump_jasm asm (output_filename sourcename ".c" ".json"); + dump_jasm asm (output_filename sourcename ".c" !sdump_suffix); (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm debug; @@ -470,7 +473,7 @@ Tracing options: -dltl Save LTL after register allocation in .ltl -dmach Save generated Mach code in .mach -dasm Save generated assembly in .s - -sdump Save info for post-linking validation in .sdump + -sdump Save info for post-linking validation in .json General options: -stdlib Set the path of the Compcert run-time library -v Print external commands before invoking them @@ -581,6 +584,7 @@ let cmdline_actions = Exact "-dmach", Set option_dmach; Exact "-dasm", Set option_dasm; Exact "-sdump", Set option_sdump; + Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); (* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); -- cgit