diff options
| -rw-r--r-- | Makefile | 9 | ||||
| -rw-r--r-- | backend/Asmexpandaux.ml | 8 | ||||
| -rw-r--r-- | backend/Asmgenproof0.v | 6 | ||||
| -rw-r--r-- | backend/Lineartyping.v | 2 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 7 | ||||
| -rwxr-xr-x | configure | 3 | ||||
| -rw-r--r-- | driver/Compiler.v | 2 | ||||
| -rw-r--r-- | extraction/extraction.v | 1 |
8 files changed, 16 insertions, 22 deletions
@@ -21,6 +21,8 @@ else ARCHDIRS?=$(ARCH)_$(BITSIZE) $(ARCH) endif +BACKENDLIB?=Asmgenproof0.v Asmgenproof1.v + DIRS=lib common $(ARCHDIRS) backend cfrontend driver \ flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight \ cparser cparser/MenhirLib @@ -95,9 +97,8 @@ BACKEND=\ Debugvar.v Debugvarproof.v \ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ - Machblock.v Machblockgen.v Machblockgenproof.v \ - Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v \ - Asm.v Asmgen.v Asmgenproof.v + Asm.v Asmgen.v Asmgenproof.v \ + $(BACKENDLIB) # C front-end modules (in cfrontend/) @@ -120,7 +121,7 @@ PARSER=Cabs.v Parser.v # Putting everything together (in driver/) -DRIVER=Compopts.v Compiler.v Complements.v ForwardSimulationBlock.v +DRIVER=Compopts.v Compiler.v Complements.v # All source files diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index 0f666a65..f5c76925 100644 --- a/backend/Asmexpandaux.ml +++ b/backend/Asmexpandaux.ml @@ -26,9 +26,7 @@ let emit i = current_code := i :: !current_code (* Generation of fresh labels *) -(** dummy_funtion is now defined in Asm.v *) -(* let dummy_function = { fn_code = []; fn_sig = signature_main } *) - +let dummy_function = { fn_code = []; fn_sig = signature_main } let current_function = ref dummy_function let next_label = ref (None: label option) @@ -122,7 +120,7 @@ let expand_debug id sp preg simple l = begin match kind with | 1-> - emit i; aux lbl scopes rest + emit i;aux lbl scopes rest | 2 -> aux lbl scopes rest | 3 -> @@ -163,7 +161,7 @@ let expand_debug id sp preg simple l = | i::rest -> simple i; aux None scopes rest in (* We need to move all closing debug annotations before the last real statement *) let rec move_debug acc bcc = function - | (Pbuiltin(EF_debug (kind,_,_),_,_)) as i::rest -> + | (Pbuiltin(EF_debug (kind,_,_),_,_) as i)::rest -> let kind = (P.to_int kind) in if kind = 1 then move_debug acc (i::bcc) rest (* Do not move debug line *) diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 3e25c79b..70c4323c 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -39,14 +39,12 @@ Proof. unfold ireg_of; intros. destruct (preg_of r); inv H; auto. Qed. -(* FIXME - Replaced FR by IR for MPPA *) Lemma freg_of_eq: - forall r r', freg_of r = OK r' -> preg_of r = IR r'. + forall r r', freg_of r = OK r' -> preg_of r = FR r'. Proof. unfold freg_of; intros. destruct (preg_of r); inv H; auto. Qed. - Lemma preg_of_injective: forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. Proof. @@ -756,7 +754,7 @@ Lemma tail_nolabel_cons: Proof. intros. destruct H0. split. constructor; auto. - intros. simpl. rewrite <- H1. destruct i; destruct i; reflexivity || contradiction. + intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction. Qed. Hint Resolve tail_nolabel_refl: labels. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 55d86448..fc163719 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -324,7 +324,7 @@ Local Opaque mreg_type. apply wt_setreg; auto. eapply Val.has_subtype; eauto. change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. red; intros; subst op. simpl in ISMOVE. - destruct args; try discriminate. destruct args; discriminate; + destruct args; try discriminate. destruct args; discriminate. apply wt_undef_regs; auto. - (* load *) simpl in *; InvBooleans. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index c9b07427..ffd9b227 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1893,15 +1893,10 @@ Proof. exact symbols_preserved. eauto. econstructor; eauto with coqlib. apply agree_regs_set_reg; auto. - (* FIXME - MPPA specific *) - replace (destroyed_by_op op) with (@nil mreg). - replace (LTL.undef_regs nil rs) with rs. - apply agree_locs_set_reg; auto. auto. auto. -(* (* The generic proof is there *) rewrite transl_destroyed_by_op. apply agree_regs_undef_regs; auto. apply agree_locs_set_reg; auto. apply agree_locs_undef_locs. auto. apply destroyed_by_op_caller_save. apply frame_set_reg. apply frame_undef_regs. exact SEP. -*) + - (* Lload *) assert (exists a', eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' @@ -802,6 +802,9 @@ fi if [ "$arch" = "mppa_k1c" ]; then cat >> Makefile.config <<EOF ARCHDIRS=$arch $arch/lib +BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\ + Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v\ + ForwardSimulationBlock.v EOF fi diff --git a/driver/Compiler.v b/driver/Compiler.v index 1cb5bd36..75247f71 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -404,7 +404,7 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Debugvarproof.transf_program_correct. eapply compose_forward_simulations. - eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof.return_address_offset). + eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof0.return_address_offset). exact Asmgenproof.return_address_exists. eassumption. eapply Asmgenproof.transf_program_correct; eassumption. diff --git a/extraction/extraction.v b/extraction/extraction.v index 6ab2ce3a..a47a7237 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -167,7 +167,6 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction - Asm.dummy_function Asmgen.addptrofs Asmgen.storeind_ptr Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env |