diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-01 09:57:01 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-01 09:57:01 +0200 |
| commit | 951963b380f1ff1e0b55f8303e4ae098cedb3cb5 (patch) | |
| tree | 6cc793efe8fc8d2950d7b313bfde79b2ecf40d24 /driver | |
| parent | 7cfaf10b604372044f53cb65b03df33c23f8b26d (diff) | |
| parent | 3324ece265091490d5380caf753d76aeee059d3f (diff) | |
| download | compcert-951963b380f1ff1e0b55f8303e4ae098cedb3cb5.tar.gz compcert-951963b380f1ff1e0b55f8303e4ae098cedb3cb5.zip | |
Merge branch 'new-builtins'
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Compiler.v | 8 | ||||
| -rw-r--r-- | driver/Compopts.v | 3 | ||||
| -rw-r--r-- | driver/Driver.ml | 6 |
3 files changed, 14 insertions, 3 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index 0afa7bfb..3920665e 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -51,6 +51,7 @@ Require Allocation. Require Tunneling. Require Linearize. Require CleanupLabels. +Require Debugvar. Require Stacking. Require Asmgen. (** Proofs of semantic preservation. *) @@ -71,6 +72,7 @@ Require Allocproof. Require Tunnelingproof. Require Linearizeproof. Require CleanupLabelsproof. +Require Debugvarproof. Require Stackingproof. Require Asmgenproof. (** Command-line flags. *) @@ -144,6 +146,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ time "Branch tunneling" Tunneling.tunnel_program @@@ time "CFG linearization" Linearize.transf_program @@ time "Label cleanup" CleanupLabels.transf_program + @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program) @@@ time "Mach generation" Stacking.transf_program @@ print print_Mach @@@ time "Asm generation" Asmgen.transf_program. @@ -253,7 +256,8 @@ Proof. set (p5 := Tunneling.tunnel_program p4) in *. destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate. set (p7 := CleanupLabels.transf_program p6) in *. - destruct (Stacking.transf_program p7) as [p8|] eqn:?; simpl in H; try discriminate. + 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 compose_forward_simulation with (RTL.semantics p11). @@ -278,6 +282,8 @@ Proof. apply Linearizeproof.transf_program_correct; auto. apply compose_forward_simulation with (Linear.semantics p7). 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). apply Stackingproof.transf_program_correct. exact Asmgenproof.return_address_exists. diff --git a/driver/Compopts.v b/driver/Compopts.v index d0c6686e..2a213350 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -41,3 +41,6 @@ Parameter optim_redundancy: unit -> bool. (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. + +(** Flag -g. For insertion of debugging information. *) +Parameter debug: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index b646dc83..f53de821 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -179,9 +179,11 @@ let compile_c_ast sourcename csyntax ofile debug = set_dest PrintMach.destination option_dmach ".mach"; (* Convert to Asm *) let asm = - match Compiler.transf_c_program csyntax with + match Compiler.apply_partial + (Compiler.transf_c_program csyntax) + Asmexpand.expand_program with | Errors.OK asm -> - Asmexpand.expand_program asm + asm | Errors.Error msg -> eprintf "%s: %a" sourcename print_error msg; exit 2 in |