From 6a3f3a62452670380827f9e39dd28c5092741099 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 21 Feb 2018 17:45:44 +0100 Subject: Hook for MPPA_K1c (generates Risc-V code for now) --- driver/Configuration.ml | 2 +- driver/Frontend.ml | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 972fd295..eae3aaab 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -123,7 +123,7 @@ let get_bool_config key = let arch = match get_config_string "arch" with - | "powerpc"|"arm"|"x86"|"riscV" as a -> a + | "powerpc"|"arm"|"x86"|"riscV"|"mppa_k1c" as a -> a | v -> bad_config "arch" [v] let model = get_config_string "model" let abi = get_config_string "abi" diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 209e72e9..db84a9f9 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -83,6 +83,7 @@ let init () = | "riscV" -> if Configuration.model = "64" then Machine.rv64 else Machine.rv32 + | "mppa_k1c" -> Machine.mppa_k1c | _ -> assert false end; Builtins.set C2C.builtins; -- cgit From 0236781c3ff798b60c5c8171a0f9b6cd569f7995 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 24 May 2018 15:06:18 +0200 Subject: Machblock: Mach language with basic blocks --- driver/ForwardSimulationBlock.v | 236 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 236 insertions(+) create mode 100644 driver/ForwardSimulationBlock.v (limited to 'driver') diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v new file mode 100644 index 00000000..43cf58c3 --- /dev/null +++ b/driver/ForwardSimulationBlock.v @@ -0,0 +1,236 @@ +(*** + +Variante de Forward Simulation pour les blocks. + +***) + +Require Import Relations. +Require Import Wellfounded. +Require Import Coqlib. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. + + +Local Open Scope nat_scope. + + +Section ForwardSimuBlock. + +Variable L1 L2: semantics. + +Local Hint Resolve starN_refl starN_step. + + +(* TODO: faut-il se baser sur [starN] ou un type inductif équivalent + (qui ferait les step dans l'ordre ci-dessous) ? + + => Voir ce qui est le plus facile pour prouver l'hypothèse [simu_end_block] ci-dessous... +*) + +Lemma starN_last_step n s t1 s': + starN (step L1) (globalenv L1) n s t1 s' -> + forall (t t2:trace) s'', + Step L1 s' t2 s'' -> t = t1 ** t2 -> starN (step L1) (globalenv L1) (S n) s t s''. +Proof. + induction 1; simpl. + + intros t t1 s0; autorewrite with trace_rewrite. + intros; subst; eapply starN_step; eauto. + autorewrite with trace_rewrite; auto. + + intros. eapply starN_step; eauto. + intros; subst; autorewrite with trace_rewrite; auto. +Qed. + +(** Hypothèses de la preuve *) + +Variable dist_end_block: state L1 -> nat. + +Hypothesis simu_mid_block: + forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). + +Hypothesis public_preserved: + forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. + +Variable build_block: state L1 -> state L2. + +Hypothesis match_initial_states: + forall s1, initial_state L1 s1 -> initial_state L2 (build_block s1). + +Hypothesis match_final_states: + forall s1 r, final_state L1 s1 r -> final_state L2 (build_block s1) r. + +Hypothesis final_states_end_block: + forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. + +Hypothesis simu_end_block: + forall s1 t s1', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> Step L2 (build_block s1) t (build_block s1'). + + +(** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) + +Definition star_in_block (head current: state L1): Prop := + dist_end_block head >= dist_end_block current + /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. + +Lemma star_in_block_step (head previous next: state L1): + forall t, star_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> star_in_block head next. +Proof. + intros t [H1 H2] H3 H4. + destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. + constructor 1. + + omega. + + cutrewrite (dist_end_block head - dist_end_block next = S (dist_end_block head - dist_end_block previous)). + - eapply starN_last_step; eauto. + - omega. +Qed. + +Lemma star_in_block_init (head current: state L1): + forall t, Step L1 head t current -> (dist_end_block head)<>0 -> star_in_block head current. +Proof. + intros t H3 H4. + destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. + constructor 1. + + omega. + + cutrewrite (dist_end_block head - dist_end_block current = 1). + - eapply starN_last_step; eauto. + - omega. +Qed. + + +Record memostate := { + real: state L1; + memorized: option (state L1); + memo_star: forall head, memorized = Some head -> star_in_block head real; + memo_final: forall r, final_state L1 real r -> memorized = None +}. + +Definition head (s: memostate): state L1 := + match memorized s with + | None => real s + | Some s' => s' + end. + +Lemma head_star (s: memostate): star_in_block (head s) (real s). +Proof. + destruct s as [rs ms Hs]. simpl. + destruct ms as [ms|]; unfold head; simpl; auto. + constructor 1. + omega. + cutrewrite ((dist_end_block rs - dist_end_block rs)%nat=O). + + apply starN_refl; auto. + + omega. +Qed. + +Inductive is_well_memorized (s s': memostate): Prop := + | StartBloc: + dist_end_block (real s) <> O -> + memorized s = None -> + memorized s' = Some (real s) -> + is_well_memorized s s' + | MidBloc: + dist_end_block (real s) <> O -> + memorized s <> None -> + memorized s' = memorized s -> + is_well_memorized s s' + | ExitBloc: + dist_end_block (real s) = O -> + memorized s' = None -> + is_well_memorized s s'. + +Local Hint Resolve StartBloc MidBloc ExitBloc. + +Definition memoL1 := {| + state := memostate; + genvtype := genvtype L1; + step := fun ge s t s' => + step L1 ge (real s) t (real s') + /\ is_well_memorized s s' ; + initial_state := fun s => initial_state L1 (real s) /\ memorized s = None; + final_state := fun s r => final_state L1 (real s) r; + globalenv:= globalenv L1; + symbolenv:= symbolenv L1 +|}. + + +(** Preuve des 2 forward simulations: L1 -> memoL1 et memoL1 -> L2 *) + +Lemma discr_dist_end s: + {dist_end_block s = O} + {dist_end_block s <> O}. +Proof. + destruct (dist_end_block s); simpl; intuition. +Qed. + +Lemma memo_simulation_step: + forall s1 t s1', Step L1 s1 t s1' -> + forall s2, s1 = (real s2) -> exists s2', Step memoL1 s2 t s2' /\ s1' = (real s2'). +Proof. + intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. simpl in H2; subst. + destruct (discr_dist_end rs2) as [H3 | H3]. + + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); simpl. + intuition. + + destruct ms2 as [s|]. + - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); simpl. + intuition. + - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); simpl. + intuition. + Unshelve. + * intros; discriminate. + * intros; auto. + * intros head X; injection X; clear X; intros; subst. + eapply star_in_block_step; eauto. + * intros r X; erewrite final_states_end_block in H3; intuition eauto. + * intros head X; injection X; clear X; intros; subst. + eapply star_in_block_init; eauto. + * intros r X; erewrite final_states_end_block in H3; intuition eauto. +Qed. + +Lemma forward_memo_simulation_1: forward_simulation L1 memoL1. +Proof. + apply forward_simulation_step with (match_states:=fun s1 s2 => s1 = (real s2)); auto. + + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); simpl. + intuition. + + intros; subst; auto. + + intros; exploit memo_simulation_step; eauto. + Unshelve. + * intros; discriminate. + * auto. +Qed. + +Lemma forward_memo_simulation_2: forward_simulation memoL1 L2. +Proof. + apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => s2 = (build_block (head s1))); auto. + + unfold memoL1; simpl. intros s1 [H0 H1]; eapply ex_intro with (x:=(build_block (real s1))). + unfold head. rewrite H1. intuition. + + intros s1 s2 r X H0. subst. unfold head. + erewrite memo_final; eauto. + eapply H0. + + unfold memoL1; simpl. + intros s1 t s1' [H1 H2] s H; subst. + destruct H2. + - (* StartBloc *) + constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H3 H4]; auto. + unfold head. rewrite H0. rewrite H2. rewrite H4. intuition. + - (* MidBloc *) + constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H3 H4]; auto. + unfold head. rewrite H2. rewrite H4. intuition. + destruct (memorized s1); simpl; auto. destruct H0; auto. + - (* EndBloc *) + constructor 1. + eapply ex_intro; intuition eauto. + apply simu_end_block. + destruct (head_star s1) as [H2 H3]. + cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3. + unfold head; rewrite H0; simpl. + eapply starN_last_step; eauto. + omega. +Qed. + +Lemma forward_simulation_block: forward_simulation L1 L2. +Proof. + eapply compose_forward_simulations. + eapply forward_memo_simulation_1. + apply forward_memo_simulation_2. +Qed. + + +End ForwardSimuBlock. \ No newline at end of file -- cgit From cb6627f0d3668a6d641f491a3e58f3eb36f741e6 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 26 Jun 2018 10:59:29 +0200 Subject: Generalization of ForwardSimulationBlock --- driver/ForwardSimulationBlock.v | 57 +++++++++++++++++------------------------ 1 file changed, 24 insertions(+), 33 deletions(-) (limited to 'driver') diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v index 43cf58c3..8c1fcb08 100644 --- a/driver/ForwardSimulationBlock.v +++ b/driver/ForwardSimulationBlock.v @@ -21,13 +21,6 @@ Variable L1 L2: semantics. Local Hint Resolve starN_refl starN_step. - -(* TODO: faut-il se baser sur [starN] ou un type inductif équivalent - (qui ferait les step dans l'ordre ci-dessous) ? - - => Voir ce qui est le plus facile pour prouver l'hypothèse [simu_end_block] ci-dessous... -*) - Lemma starN_last_step n s t1 s': starN (step L1) (globalenv L1) n s t1 s' -> forall (t t2:trace) s'', @@ -51,19 +44,19 @@ Hypothesis simu_mid_block: Hypothesis public_preserved: forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. -Variable build_block: state L1 -> state L2. +Variable match_states: state L1 -> state L2 -> Prop. Hypothesis match_initial_states: - forall s1, initial_state L1 s1 -> initial_state L2 (build_block s1). + forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2. Hypothesis match_final_states: - forall s1 r, final_state L1 s1 r -> final_state L2 (build_block s1) r. + forall s1 s2 r, final_state L1 s1 r -> match_states s1 s2 -> final_state L2 s2 r. Hypothesis final_states_end_block: forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. Hypothesis simu_end_block: - forall s1 t s1', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> Step L2 (build_block s1) t (build_block s1'). + forall s1 t s1' s2, starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> match_states s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states s1' s2'. (** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) @@ -198,31 +191,29 @@ Qed. Lemma forward_memo_simulation_2: forward_simulation memoL1 L2. Proof. - apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => s2 = (build_block (head s1))); auto. - + unfold memoL1; simpl. intros s1 [H0 H1]; eapply ex_intro with (x:=(build_block (real s1))). - unfold head. rewrite H1. intuition. - + intros s1 s2 r X H0. subst. unfold head. - erewrite memo_final; eauto. - eapply H0. - + unfold memoL1; simpl. - intros s1 t s1' [H1 H2] s H; subst. - destruct H2. + unfold memoL1; simpl. + apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); simpl; auto. + + intros s1 [H0 H1]; destruct (match_initial_states (real s1) H0). + unfold head; rewrite H1. + intuition eauto. + + intros s1 s2 r X H0; unfold head in X. + erewrite memo_final in X; eauto. + + intros s1 t s1' [H1 H2] s2 H; subst. + destruct H2 as [ H0 H2 H3 | H0 H2 H3 | H0 H2]. - (* StartBloc *) - constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H3 H4]; auto. - unfold head. rewrite H0. rewrite H2. rewrite H4. intuition. + constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto. + unfold head in * |- *. rewrite H2 in H. rewrite H3. rewrite H4. intuition. - (* MidBloc *) - constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H3 H4]; auto. - unfold head. rewrite H2. rewrite H4. intuition. - destruct (memorized s1); simpl; auto. destruct H0; auto. + constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto. + unfold head in * |- *. rewrite H3. rewrite H4. intuition. + destruct (memorized s1); simpl; auto. tauto. - (* EndBloc *) - constructor 1. - eapply ex_intro; intuition eauto. - apply simu_end_block. - destruct (head_star s1) as [H2 H3]. - cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3. - unfold head; rewrite H0; simpl. - eapply starN_last_step; eauto. - omega. + constructor 1. + destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. + * destruct (head_star s1) as [H4 H3]. + cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3; try omega. + eapply starN_last_step; eauto. + * unfold head; rewrite H2; simpl. intuition eauto. Qed. Lemma forward_simulation_block: forward_simulation L1 L2. -- cgit From 2e93b668df554edbfec0c23de7b14caf95a48b1d Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 28 Jun 2018 10:38:26 +0200 Subject: Machblock: adaptation to the generalized ForwardSimulationBlock --- driver/ForwardSimulationBlock.v | 111 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 103 insertions(+), 8 deletions(-) (limited to 'driver') diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v index 8c1fcb08..a9569e08 100644 --- a/driver/ForwardSimulationBlock.v +++ b/driver/ForwardSimulationBlock.v @@ -1,6 +1,7 @@ (*** -Variante de Forward Simulation pour les blocks. +Auxiliary lemmas on starN and forward_simulation +in order to prove the forward simulation of Mach -> Machblock. ***) @@ -15,16 +16,36 @@ Require Import Smallstep. Local Open Scope nat_scope. -Section ForwardSimuBlock. +(** Auxiliary lemma on starN *) +Section starN_lemma. -Variable L1 L2: semantics. +Variable L: semantics. -Local Hint Resolve starN_refl starN_step. +Local Hint Resolve starN_refl starN_step Eapp_assoc. + +Lemma starN_split n s t s': + starN (step L) (globalenv L) n s t s' -> + forall m k, n=m+k -> + exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. +Proof. + induction 1; simpl. + + intros m k H; assert (X: m=0); try omega. + assert (X0: k=0); try omega. + subst; repeat (eapply ex_intro); intuition eauto. + + intros m; destruct m as [| m']; simpl. + - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. + - intros k H2. inversion H2. + exploit (IHstarN m' k); eauto. intro. + destruct H3 as (t5 & t6 & s0 & H5 & H6 & H7). + repeat (eapply ex_intro). + instantiate (1 := t6); instantiate (1 := t1 ** t5); instantiate (1 := s0). + intuition eauto. subst. auto. +Qed. Lemma starN_last_step n s t1 s': - starN (step L1) (globalenv L1) n s t1 s' -> + starN (step L) (globalenv L) n s t1 s' -> forall (t t2:trace) s'', - Step L1 s' t2 s'' -> t = t1 ** t2 -> starN (step L1) (globalenv L1) (S n) s t s''. + Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. Proof. induction 1; simpl. + intros t t1 s0; autorewrite with trace_rewrite. @@ -34,6 +55,17 @@ Proof. intros; subst; autorewrite with trace_rewrite; auto. Qed. +End starN_lemma. + + + +(** General scheme from a "match_states" relation *) + +Section ForwardSimuBlock_REL. + +Variable L1 L2: semantics. + + (** Hypothèses de la preuve *) Variable dist_end_block: state L1 -> nat. @@ -61,6 +93,8 @@ Hypothesis simu_end_block: (** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) +Local Hint Resolve starN_refl starN_step. + Definition star_in_block (head current: state L1): Prop := dist_end_block head >= dist_end_block current /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. @@ -216,7 +250,7 @@ Proof. * unfold head; rewrite H2; simpl. intuition eauto. Qed. -Lemma forward_simulation_block: forward_simulation L1 L2. +Lemma forward_simulation_block_rel: forward_simulation L1 L2. Proof. eapply compose_forward_simulations. eapply forward_memo_simulation_1. @@ -224,4 +258,65 @@ Proof. Qed. -End ForwardSimuBlock. \ No newline at end of file +End ForwardSimuBlock_REL. + + + +(* An instance of the previous scheme, when there is a translation from L1 states to L2 states + +Here, we do not require that the sequence of S2 states does exactly match the sequence of L1 states by trans_state. +This is because the exact matching is broken in Machblock on "goto" instruction (due to the find_label). + +However, the Machblock state after a goto remains "equivalent" to the trans_state of the Mach state in the sense of "equiv_on_next_step" below... + +*) + +Section ForwardSimuBlock_TRANS. + +Variable L1 L2: semantics. + +Variable trans_state: state L1 -> state L2. + +Definition equiv_on_next_step (P Q: Prop) s2_a s2_b: Prop := + (P -> (forall t s', Step L2 s2_a t s' <-> Step L2 s2_b t s')) /\ (Q -> (forall r, (final_state L2 s2_a r) <-> (final_state L2 s2_b r))). + +Definition match_states s1 s2: Prop := + equiv_on_next_step (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 (trans_state s1). + +Lemma match_states_trans_state s1: match_states s1 (trans_state s1). +Proof. + unfold match_states, equiv_on_next_step. intuition. +Qed. + +Variable dist_end_block: state L1 -> nat. + +Hypothesis simu_mid_block: + forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). + +Hypothesis public_preserved: + forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. + +Hypothesis match_initial_states: + forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2. + +Hypothesis match_final_states: + forall s1 r, final_state L1 s1 r -> final_state L2 (trans_state s1) r. + +Hypothesis final_states_end_block: + forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. + +Hypothesis simu_end_block: + forall s1 t s1', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> exists s2', Step L2 (trans_state s1) t s2' /\ match_states s1' s2'. + +Lemma forward_simulation_block_trans: forward_simulation L1 L2. +Proof. + eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states); try tauto. + + (* final_states *) intros s1 s2 r H1 [H2 H3]. rewrite H3; eauto. + + (* simu_end_block *) + intros s1 t s1' s2 H1 [H2a H2b]. exploit simu_end_block; eauto. + intros (s2' & H3 & H4); econstructor 1; intuition eauto. + rewrite H2a; auto. + inversion_clear H1. eauto. +Qed. + +End ForwardSimuBlock_TRANS. \ No newline at end of file -- cgit From edb93401b3621e8e9731c0a50afdbcc441d7f495 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 12 Jul 2018 14:58:06 +0200 Subject: Machblock: some renaming and proof simplifications --- driver/ForwardSimulationBlock.v | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'driver') diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v index a9569e08..dc8beb29 100644 --- a/driver/ForwardSimulationBlock.v +++ b/driver/ForwardSimulationBlock.v @@ -42,7 +42,7 @@ Proof. intuition eauto. subst. auto. Qed. -Lemma starN_last_step n s t1 s': +Lemma starN_tailstep n s t1 s': starN (step L) (globalenv L) n s t1 s' -> forall (t t2:trace) s'', Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. @@ -95,31 +95,31 @@ Hypothesis simu_end_block: Local Hint Resolve starN_refl starN_step. -Definition star_in_block (head current: state L1): Prop := +Definition follows_in_block (head current: state L1): Prop := dist_end_block head >= dist_end_block current /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. -Lemma star_in_block_step (head previous next: state L1): - forall t, star_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> star_in_block head next. +Lemma follows_in_block_step (head previous next: state L1): + forall t, follows_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> follows_in_block head next. Proof. intros t [H1 H2] H3 H4. destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. constructor 1. + omega. + cutrewrite (dist_end_block head - dist_end_block next = S (dist_end_block head - dist_end_block previous)). - - eapply starN_last_step; eauto. + - eapply starN_tailstep; eauto. - omega. Qed. -Lemma star_in_block_init (head current: state L1): - forall t, Step L1 head t current -> (dist_end_block head)<>0 -> star_in_block head current. +Lemma follows_in_block_init (head current: state L1): + forall t, Step L1 head t current -> (dist_end_block head)<>0 -> follows_in_block head current. Proof. intros t H3 H4. destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. constructor 1. + omega. + cutrewrite (dist_end_block head - dist_end_block current = 1). - - eapply starN_last_step; eauto. + - eapply starN_tailstep; eauto. - omega. Qed. @@ -127,7 +127,7 @@ Qed. Record memostate := { real: state L1; memorized: option (state L1); - memo_star: forall head, memorized = Some head -> star_in_block head real; + memo_star: forall head, memorized = Some head -> follows_in_block head real; memo_final: forall r, final_state L1 real r -> memorized = None }. @@ -137,7 +137,7 @@ Definition head (s: memostate): state L1 := | Some s' => s' end. -Lemma head_star (s: memostate): star_in_block (head s) (real s). +Lemma head_followed (s: memostate): follows_in_block (head s) (real s). Proof. destruct s as [rs ms Hs]. simpl. destruct ms as [ms|]; unfold head; simpl; auto. @@ -204,10 +204,10 @@ Proof. * intros; discriminate. * intros; auto. * intros head X; injection X; clear X; intros; subst. - eapply star_in_block_step; eauto. + eapply follows_in_block_step; eauto. * intros r X; erewrite final_states_end_block in H3; intuition eauto. * intros head X; injection X; clear X; intros; subst. - eapply star_in_block_init; eauto. + eapply follows_in_block_init; eauto. * intros r X; erewrite final_states_end_block in H3; intuition eauto. Qed. @@ -244,9 +244,9 @@ Proof. - (* EndBloc *) constructor 1. destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. - * destruct (head_star s1) as [H4 H3]. + * destruct (head_followed s1) as [H4 H3]. cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3; try omega. - eapply starN_last_step; eauto. + eapply starN_tailstep; eauto. * unfold head; rewrite H2; simpl. intuition eauto. Qed. @@ -319,4 +319,4 @@ Proof. inversion_clear H1. eauto. Qed. -End ForwardSimuBlock_TRANS. \ No newline at end of file +End ForwardSimuBlock_TRANS. -- cgit From 672d9ea4489158f6a6b7175463c6514a91d1490d Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 5 Sep 2018 15:15:48 +0200 Subject: Rajout d'un return_address_offset. Besoin de changer forward_simu de mach machblock --- driver/Compiler.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..1cb5bd36 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 := Asmgenproof0.return_address_offset). + eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof.return_address_offset). exact Asmgenproof.return_address_exists. eassumption. eapply Asmgenproof.transf_program_correct; eassumption. -- cgit From 3d38bf85c8ac3a83fe7aaeb5e01bb9a8403e6a60 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 26 Nov 2018 15:31:46 +0100 Subject: Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow that --- driver/ForwardSimulationBlock.v | 322 ---------------------------------------- 1 file changed, 322 deletions(-) delete mode 100644 driver/ForwardSimulationBlock.v (limited to 'driver') diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v deleted file mode 100644 index dc8beb29..00000000 --- a/driver/ForwardSimulationBlock.v +++ /dev/null @@ -1,322 +0,0 @@ -(*** - -Auxiliary lemmas on starN and forward_simulation -in order to prove the forward simulation of Mach -> Machblock. - -***) - -Require Import Relations. -Require Import Wellfounded. -Require Import Coqlib. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. - - -Local Open Scope nat_scope. - - -(** Auxiliary lemma on starN *) -Section starN_lemma. - -Variable L: semantics. - -Local Hint Resolve starN_refl starN_step Eapp_assoc. - -Lemma starN_split n s t s': - starN (step L) (globalenv L) n s t s' -> - forall m k, n=m+k -> - exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. -Proof. - induction 1; simpl. - + intros m k H; assert (X: m=0); try omega. - assert (X0: k=0); try omega. - subst; repeat (eapply ex_intro); intuition eauto. - + intros m; destruct m as [| m']; simpl. - - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. - - intros k H2. inversion H2. - exploit (IHstarN m' k); eauto. intro. - destruct H3 as (t5 & t6 & s0 & H5 & H6 & H7). - repeat (eapply ex_intro). - instantiate (1 := t6); instantiate (1 := t1 ** t5); instantiate (1 := s0). - intuition eauto. subst. auto. -Qed. - -Lemma starN_tailstep n s t1 s': - starN (step L) (globalenv L) n s t1 s' -> - forall (t t2:trace) s'', - Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. -Proof. - induction 1; simpl. - + intros t t1 s0; autorewrite with trace_rewrite. - intros; subst; eapply starN_step; eauto. - autorewrite with trace_rewrite; auto. - + intros. eapply starN_step; eauto. - intros; subst; autorewrite with trace_rewrite; auto. -Qed. - -End starN_lemma. - - - -(** General scheme from a "match_states" relation *) - -Section ForwardSimuBlock_REL. - -Variable L1 L2: semantics. - - -(** Hypothèses de la preuve *) - -Variable dist_end_block: state L1 -> nat. - -Hypothesis simu_mid_block: - forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). - -Hypothesis public_preserved: - forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. - -Variable match_states: state L1 -> state L2 -> Prop. - -Hypothesis match_initial_states: - forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2. - -Hypothesis match_final_states: - forall s1 s2 r, final_state L1 s1 r -> match_states s1 s2 -> final_state L2 s2 r. - -Hypothesis final_states_end_block: - forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. - -Hypothesis simu_end_block: - forall s1 t s1' s2, starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> match_states s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states s1' s2'. - - -(** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) - -Local Hint Resolve starN_refl starN_step. - -Definition follows_in_block (head current: state L1): Prop := - dist_end_block head >= dist_end_block current - /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. - -Lemma follows_in_block_step (head previous next: state L1): - forall t, follows_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> follows_in_block head next. -Proof. - intros t [H1 H2] H3 H4. - destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. - constructor 1. - + omega. - + cutrewrite (dist_end_block head - dist_end_block next = S (dist_end_block head - dist_end_block previous)). - - eapply starN_tailstep; eauto. - - omega. -Qed. - -Lemma follows_in_block_init (head current: state L1): - forall t, Step L1 head t current -> (dist_end_block head)<>0 -> follows_in_block head current. -Proof. - intros t H3 H4. - destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. - constructor 1. - + omega. - + cutrewrite (dist_end_block head - dist_end_block current = 1). - - eapply starN_tailstep; eauto. - - omega. -Qed. - - -Record memostate := { - real: state L1; - memorized: option (state L1); - memo_star: forall head, memorized = Some head -> follows_in_block head real; - memo_final: forall r, final_state L1 real r -> memorized = None -}. - -Definition head (s: memostate): state L1 := - match memorized s with - | None => real s - | Some s' => s' - end. - -Lemma head_followed (s: memostate): follows_in_block (head s) (real s). -Proof. - destruct s as [rs ms Hs]. simpl. - destruct ms as [ms|]; unfold head; simpl; auto. - constructor 1. - omega. - cutrewrite ((dist_end_block rs - dist_end_block rs)%nat=O). - + apply starN_refl; auto. - + omega. -Qed. - -Inductive is_well_memorized (s s': memostate): Prop := - | StartBloc: - dist_end_block (real s) <> O -> - memorized s = None -> - memorized s' = Some (real s) -> - is_well_memorized s s' - | MidBloc: - dist_end_block (real s) <> O -> - memorized s <> None -> - memorized s' = memorized s -> - is_well_memorized s s' - | ExitBloc: - dist_end_block (real s) = O -> - memorized s' = None -> - is_well_memorized s s'. - -Local Hint Resolve StartBloc MidBloc ExitBloc. - -Definition memoL1 := {| - state := memostate; - genvtype := genvtype L1; - step := fun ge s t s' => - step L1 ge (real s) t (real s') - /\ is_well_memorized s s' ; - initial_state := fun s => initial_state L1 (real s) /\ memorized s = None; - final_state := fun s r => final_state L1 (real s) r; - globalenv:= globalenv L1; - symbolenv:= symbolenv L1 -|}. - - -(** Preuve des 2 forward simulations: L1 -> memoL1 et memoL1 -> L2 *) - -Lemma discr_dist_end s: - {dist_end_block s = O} + {dist_end_block s <> O}. -Proof. - destruct (dist_end_block s); simpl; intuition. -Qed. - -Lemma memo_simulation_step: - forall s1 t s1', Step L1 s1 t s1' -> - forall s2, s1 = (real s2) -> exists s2', Step memoL1 s2 t s2' /\ s1' = (real s2'). -Proof. - intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. simpl in H2; subst. - destruct (discr_dist_end rs2) as [H3 | H3]. - + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); simpl. - intuition. - + destruct ms2 as [s|]. - - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); simpl. - intuition. - - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); simpl. - intuition. - Unshelve. - * intros; discriminate. - * intros; auto. - * intros head X; injection X; clear X; intros; subst. - eapply follows_in_block_step; eauto. - * intros r X; erewrite final_states_end_block in H3; intuition eauto. - * intros head X; injection X; clear X; intros; subst. - eapply follows_in_block_init; eauto. - * intros r X; erewrite final_states_end_block in H3; intuition eauto. -Qed. - -Lemma forward_memo_simulation_1: forward_simulation L1 memoL1. -Proof. - apply forward_simulation_step with (match_states:=fun s1 s2 => s1 = (real s2)); auto. - + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); simpl. - intuition. - + intros; subst; auto. - + intros; exploit memo_simulation_step; eauto. - Unshelve. - * intros; discriminate. - * auto. -Qed. - -Lemma forward_memo_simulation_2: forward_simulation memoL1 L2. -Proof. - unfold memoL1; simpl. - apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); simpl; auto. - + intros s1 [H0 H1]; destruct (match_initial_states (real s1) H0). - unfold head; rewrite H1. - intuition eauto. - + intros s1 s2 r X H0; unfold head in X. - erewrite memo_final in X; eauto. - + intros s1 t s1' [H1 H2] s2 H; subst. - destruct H2 as [ H0 H2 H3 | H0 H2 H3 | H0 H2]. - - (* StartBloc *) - constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto. - unfold head in * |- *. rewrite H2 in H. rewrite H3. rewrite H4. intuition. - - (* MidBloc *) - constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto. - unfold head in * |- *. rewrite H3. rewrite H4. intuition. - destruct (memorized s1); simpl; auto. tauto. - - (* EndBloc *) - constructor 1. - destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. - * destruct (head_followed s1) as [H4 H3]. - cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3; try omega. - eapply starN_tailstep; eauto. - * unfold head; rewrite H2; simpl. intuition eauto. -Qed. - -Lemma forward_simulation_block_rel: forward_simulation L1 L2. -Proof. - eapply compose_forward_simulations. - eapply forward_memo_simulation_1. - apply forward_memo_simulation_2. -Qed. - - -End ForwardSimuBlock_REL. - - - -(* An instance of the previous scheme, when there is a translation from L1 states to L2 states - -Here, we do not require that the sequence of S2 states does exactly match the sequence of L1 states by trans_state. -This is because the exact matching is broken in Machblock on "goto" instruction (due to the find_label). - -However, the Machblock state after a goto remains "equivalent" to the trans_state of the Mach state in the sense of "equiv_on_next_step" below... - -*) - -Section ForwardSimuBlock_TRANS. - -Variable L1 L2: semantics. - -Variable trans_state: state L1 -> state L2. - -Definition equiv_on_next_step (P Q: Prop) s2_a s2_b: Prop := - (P -> (forall t s', Step L2 s2_a t s' <-> Step L2 s2_b t s')) /\ (Q -> (forall r, (final_state L2 s2_a r) <-> (final_state L2 s2_b r))). - -Definition match_states s1 s2: Prop := - equiv_on_next_step (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 (trans_state s1). - -Lemma match_states_trans_state s1: match_states s1 (trans_state s1). -Proof. - unfold match_states, equiv_on_next_step. intuition. -Qed. - -Variable dist_end_block: state L1 -> nat. - -Hypothesis simu_mid_block: - forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). - -Hypothesis public_preserved: - forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. - -Hypothesis match_initial_states: - forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2. - -Hypothesis match_final_states: - forall s1 r, final_state L1 s1 r -> final_state L2 (trans_state s1) r. - -Hypothesis final_states_end_block: - forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. - -Hypothesis simu_end_block: - forall s1 t s1', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> exists s2', Step L2 (trans_state s1) t s2' /\ match_states s1' s2'. - -Lemma forward_simulation_block_trans: forward_simulation L1 L2. -Proof. - eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states); try tauto. - + (* final_states *) intros s1 s2 r H1 [H2 H3]. rewrite H3; eauto. - + (* simu_end_block *) - intros s1 t s1' s2 H1 [H2a H2b]. exploit simu_end_block; eauto. - intros (s2' & H3 & H4); econstructor 1; intuition eauto. - rewrite H2a; auto. - inversion_clear H1. eauto. -Qed. - -End ForwardSimuBlock_TRANS. -- cgit From 5631ccb7c416bb7ecbe7920cb432a78436c0a7ac Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 26 Nov 2018 17:35:31 +0100 Subject: BROKEN - works for x86, not for k1 anymore --- driver/Compiler.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') 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. -- cgit From 3af2dc7aaa8c8139ddd26589258f2b289425f591 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 27 Nov 2018 15:34:34 +0100 Subject: Compiles for x86 and mppa_k1c (except Asmexpandaux.ml) --- driver/Compiler.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..6d398327 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -69,7 +69,7 @@ Require Linearizeproof. Require CleanupLabelsproof. Require Debugvarproof. Require Stackingproof. -Require Asmgenproof. +Require Import Asmgenproof. (** Command-line flags. *) Require Import Compopts. -- cgit From 458df74c1280ab4f6131272b20f8613cbd683f87 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 18 Jan 2019 15:22:03 +0100 Subject: -O0 will not perform postpass scheduling --- driver/Clflags.ml | 1 + driver/Compopts.v | 3 +++ driver/Driver.ml | 4 +++- 3 files changed, 7 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index a886ee9b..99ee41e7 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -27,6 +27,7 @@ let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true +let option_fpostpass = ref true let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Compopts.v b/driver/Compopts.v index 2a213350..e6eecc9b 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -39,6 +39,9 @@ Parameter optim_CSE: unit -> bool. (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. +(** Flag -fpostpass. Postpass scheduling for K1 architecture *) +Parameter optim_postpass: unit -> bool. + (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 8ab8557c..467cf989 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -193,6 +193,7 @@ Processing options: (=0: none, =1: limited, =2: full; default is full) -fcse Perform common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] + -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] @@ -249,7 +250,7 @@ let dump_mnemonics destfile = exit 0 let optimization_options = [ - option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy; option_finline_functions_called_once; + option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy; option_fpostpass; option_finline_functions_called_once; ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -361,6 +362,7 @@ let cmdline_actions = @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy + @ f_opt "postpass" option_fpostpass @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once (* Code generation options *) -- cgit From 50affca71434b1e1ca3e75ce8f62a304ed1913cf Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 1 Mar 2019 12:06:09 +0100 Subject: Added long double = double by default on Kalray architecture --- driver/Clflags.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 99ee41e7..77fae8ee 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -15,7 +15,7 @@ let prepro_options = ref ([]: string list) let linker_options = ref ([]: string list) let assembler_options = ref ([]: string list) -let option_flongdouble = ref false +let option_flongdouble = ref (Configuration.arch = "mppa_k1c") let option_fstruct_passing = ref false let option_fbitfields = ref false let option_fvararg_calls = ref true -- cgit From 8f337598016aa49ff6554085b406b7e6026bfc3d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 12 Mar 2019 17:22:46 +0100 Subject: -fpostpass-ilp --- driver/Clflags.ml | 1 + driver/Driver.ml | 2 ++ 2 files changed, 3 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 77fae8ee..4d70d350 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,6 +28,7 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true let option_fpostpass = ref true +let option_fpostpass_ilp = ref false let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Driver.ml b/driver/Driver.ml index 467cf989..c68c066a 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,6 +194,7 @@ Processing options: -fcse Perform common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] + -fpostpass-ilp Use integer linear programming for postpass scheduling [off] -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] @@ -363,6 +364,7 @@ let cmdline_actions = @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass + @ f_opt "postpass-ilp" option_fpostpass_ilp @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once (* Code generation options *) -- cgit From 60c0b75a8dcf475d3fb443e0dac50dac34e01d12 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 12 Mar 2019 17:58:48 +0100 Subject: Added a flag for changing the scheduler (not any choice available right now) --- driver/Clflags.ml | 1 + driver/Compopts.v | 3 +++ driver/Driver.ml | 2 ++ 3 files changed, 6 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 77fae8ee..fe7aef10 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,6 +28,7 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true let option_fpostpass = ref true +let option_pp_optimizer = ref 1 let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Compopts.v b/driver/Compopts.v index e6eecc9b..16ad7c33 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -42,6 +42,9 @@ Parameter optim_redundancy: unit -> bool. (** Flag -fpostpass. Postpass scheduling for K1 architecture *) Parameter optim_postpass: unit -> bool. +(** Flag -fpp_optimizer, to specify the postpass optimizer to use *) +Parameter optim_pp_optimizer: unit -> nat. + (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 467cf989..36d55913 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,6 +194,7 @@ Processing options: -fcse Perform common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] + -pp-optimizer Select the postpass optimizer to use if -fpostpass is active [list_scheduler] -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] @@ -295,6 +296,7 @@ let cmdline_actions = Exact "-O", Unit (set_all optimization_options); _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; + Exact "-pp-optimizer", String(fun s -> option_pp_optimizer := if (s == "list_scheduler") then 1 else 0); Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); -- cgit From 50f25f57749d3eb46d859350719c9324fb75afa2 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 12 Mar 2019 18:03:22 +0100 Subject: Added cascaded_scheduler but the flag does not work --- driver/Driver.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 36d55913..94f89e99 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,7 +194,8 @@ Processing options: -fcse Perform common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] - -pp-optimizer Select the postpass optimizer to use if -fpostpass is active [list_scheduler] + -pp-optimizer Select the postpass optimizer to use if -fpostpass is active + (possible values: list_scheduler, cascaded_scheduler) [list_scheduler] -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] @@ -296,7 +297,7 @@ let cmdline_actions = Exact "-O", Unit (set_all optimization_options); _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; - Exact "-pp-optimizer", String(fun s -> option_pp_optimizer := if (s == "list_scheduler") then 1 else 0); + Exact "-pp-optimizer", String(fun s -> option_pp_optimizer := if (s == "list_scheduler") then 1 else if (s == "cascaded_scheduler") then 2 else 0); Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); -- cgit From 72e3e2dd1c73469ac2475c2787d2e85437d53b35 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 12 Mar 2019 20:44:06 +0100 Subject: -fpostpass-ilp --- driver/Compopts.v | 3 --- driver/Driver.ml | 1 - 2 files changed, 4 deletions(-) (limited to 'driver') diff --git a/driver/Compopts.v b/driver/Compopts.v index 16ad7c33..e6eecc9b 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -42,9 +42,6 @@ Parameter optim_redundancy: unit -> bool. (** Flag -fpostpass. Postpass scheduling for K1 architecture *) Parameter optim_postpass: unit -> bool. -(** Flag -fpp_optimizer, to specify the postpass optimizer to use *) -Parameter optim_pp_optimizer: unit -> nat. - (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 98e057d4..c68c066a 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -296,7 +296,6 @@ let cmdline_actions = Exact "-O", Unit (set_all optimization_options); _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; - Exact "-pp-optimizer", String(fun s -> option_pp_optimizer := if (s == "list_scheduler") then 1 else if (s == "cascaded_scheduler") then 2 else 0); Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); -- cgit From c3003517a048d7469a314fc245118ed72e2158dd Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 29 Apr 2019 18:02:58 +0200 Subject: The scheduler selection works, but the argument is not optional yet (-fpostpass nameofscheduler) --- driver/Clflags.ml | 2 +- driver/Driver.ml | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 4d70d350..5b8ad443 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,7 +28,7 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true let option_fpostpass = ref true -let option_fpostpass_ilp = ref false +let option_fpostpass_sched = ref "list" let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Driver.ml b/driver/Driver.ml index c68c066a..9a2eca1f 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -264,6 +264,10 @@ 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 + let f_opt_postpass name ref = + [Exact("-f" ^ name), String + (fun s -> (option_fpostpass_sched := (if s == "" then "list" else s)); ref := true); + Exact("-fno-" ^ name), Unset ref] in [ (* Getting help *) Exact "-help", Unit print_usage_and_exit; @@ -363,8 +367,7 @@ let cmdline_actions = @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy - @ f_opt "postpass" option_fpostpass - @ f_opt "postpass-ilp" option_fpostpass_ilp + @ f_opt_postpass "postpass" option_fpostpass @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once (* Code generation options *) -- cgit From e570597b2f80a2a86b8672a40387dc63fd31b555 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 30 Apr 2019 11:08:38 +0200 Subject: Setting fpostpass= option --- driver/Driver.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 9a2eca1f..2672ed99 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -194,7 +194,8 @@ Processing options: -fcse Perform common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] - -fpostpass-ilp Use integer linear programming for postpass scheduling [off] + -fpostpass= Perform postpass scheduling with the specified optimization [list] + (=list: list scheduling, =ilp: ILP, =dumb: just packing bundles) -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] @@ -264,10 +265,10 @@ 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 - let f_opt_postpass name ref = - [Exact("-f" ^ name), String - (fun s -> (option_fpostpass_sched := (if s == "" then "list" else s)); ref := true); - Exact("-fno-" ^ name), Unset ref] in + let f_opt_str name ref strref = + [Exact("-f" ^ name ^ "="), String + (fun s -> (strref := (if s == "" then "list" else s)); ref := true) + ] in [ (* Getting help *) Exact "-help", Unit print_usage_and_exit; @@ -367,7 +368,8 @@ let cmdline_actions = @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy - @ f_opt_postpass "postpass" option_fpostpass + @ f_opt "postpass" option_fpostpass + @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once (* Code generation options *) -- cgit From 9f256a4ad30c93749e6c1192a84f996feac3b023 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 2 May 2019 09:32:49 +0200 Subject: command line options (still incomplete) --- driver/Clflags.ml | 4 ++++ driver/Compopts.v | 9 +++++++++ driver/Driver.ml | 3 +++ 3 files changed, 16 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 4d70d350..76afa4b4 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -66,3 +66,7 @@ let option_small_const = ref (!option_small_data) let option_timings = ref false let stdlib_path = ref Configuration.stdlib_path let use_standard_headers = ref Configuration.has_standard_headers + +let option_fglobaladdrtmp = ref false +let option_fglobaladdroffset = ref false +let option_fxsaddr = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index e6eecc9b..3bb7a474 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -42,6 +42,15 @@ Parameter optim_redundancy: unit -> bool. (** Flag -fpostpass. Postpass scheduling for K1 architecture *) Parameter optim_postpass: unit -> bool. +(** FIXME TEMPORARY Flag -fglobaladdrtmp. Use a temporary register for loading the address of global variables (default false) *) +Parameter optim_fglobaladdrtmp: unit -> bool. + +(** FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses (default false) *) +Parameter optim_fglobaladdroffset: unit -> bool. + +(** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *) +Parameter optim_fxsaddr: unit -> bool. + (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index c68c066a..505a1d35 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -367,6 +367,9 @@ let cmdline_actions = @ f_opt "postpass-ilp" option_fpostpass_ilp @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once + @ f_opt "globaladdrtmp" option_fglobaladdrtmp + @ f_opt "globaladdroffset" option_fglobaladdroffset + @ f_opt "xsaddr" option_fxsaddr (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) -- cgit From fb77ce264f957a1ee3f87e537b55afbb10785ecf Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 3 May 2019 10:43:53 +0200 Subject: Renaming "dumb" scheduling into "greedy" --- driver/Driver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 35b5db86..3b0830ad 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -195,7 +195,7 @@ Processing options: -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] - (=list: list scheduling, =ilp: ILP, =dumb: just packing bundles) + (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] -- cgit From cba53c98b999eea7984e4ffd24a9449abea3e0e2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 3 May 2019 11:29:40 +0200 Subject: -fcoalesce-mem --- driver/Clflags.ml | 1 + driver/Compopts.v | 3 +++ driver/Driver.ml | 1 + 3 files changed, 5 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 46f19dcf..b1afab6f 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -70,3 +70,4 @@ let use_standard_headers = ref Configuration.has_standard_headers let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true +let option_coalesce_mem = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index 3bb7a474..f7de596c 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -51,6 +51,9 @@ Parameter optim_fglobaladdroffset: unit -> bool. (** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *) Parameter optim_fxsaddr: unit -> bool. +(** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *) +Parameter optim_coalesce_mem: unit -> bool. + (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 35b5db86..804fc3c9 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -375,6 +375,7 @@ let cmdline_actions = @ f_opt "globaladdrtmp" option_fglobaladdrtmp @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr + @ f_opt "coalesce-mem" option_coalesce_mem (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) -- cgit From 66ee59d3dc8a861b468cfaf0ff46fc71dfb8fec2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 21:54:18 +0200 Subject: option -faddx (off by default until questions cleared) --- driver/Clflags.ml | 3 ++- driver/Compopts.v | 9 ++++++--- driver/Driver.ml | 3 ++- 3 files changed, 10 insertions(+), 5 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b1afab6f..651d644e 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -70,4 +70,5 @@ let use_standard_headers = ref Configuration.has_standard_headers let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true -let option_coalesce_mem = ref true +let option_faddx = ref false +let option_fcoalesce_mem = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index f7de596c..9c6448b7 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -43,17 +43,20 @@ Parameter optim_redundancy: unit -> bool. Parameter optim_postpass: unit -> bool. (** FIXME TEMPORARY Flag -fglobaladdrtmp. Use a temporary register for loading the address of global variables (default false) *) -Parameter optim_fglobaladdrtmp: unit -> bool. +Parameter optim_globaladdrtmp: unit -> bool. (** FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses (default false) *) -Parameter optim_fglobaladdroffset: unit -> bool. +Parameter optim_globaladdroffset: unit -> bool. (** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *) -Parameter optim_fxsaddr: unit -> bool. +Parameter optim_xsaddr: unit -> bool. (** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *) Parameter optim_coalesce_mem: unit -> bool. +(** FIXME TEMPORARY Flag -faddx. Fuse (default false) *) +Parameter optim_addx: unit -> bool. + (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index cfafcaa3..74e7ae77 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -375,7 +375,8 @@ let cmdline_actions = @ f_opt "globaladdrtmp" option_fglobaladdrtmp @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr - @ f_opt "coalesce-mem" option_coalesce_mem + @ f_opt "addx" option_faddx + @ f_opt "coalesce-mem" option_fcoalesce_mem (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) -- cgit From 95938a8732b572d61955b1de8c49362c9e162640 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 31 May 2019 19:15:19 +0200 Subject: If-conversion optimization Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches. --- driver/Clflags.ml | 2 ++ driver/Driver.ml | 10 ++++++++-- 2 files changed, 10 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index fc12863d..d27871ef 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -27,6 +27,8 @@ let option_ftailcalls = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true +let option_fifconversion = ref true +let option_ffavor_branchless = ref false let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Driver.ml b/driver/Driver.ml index 50f14d13..84392ef6 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -196,6 +196,9 @@ Processing options: -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] + -fif-conversion Perform if-conversion (generation of conditional moves) [on] + -ffavor-branchless Favor the generation of branch-free instruction sequences, + even when possibly more costly than the default [off] Code generation options: (use -fno- to turn off -f) -ffpu Use FP registers for some integer operations [on] -fsmall-data Set maximal size for allocation in small data area @@ -250,7 +253,8 @@ let dump_mnemonics destfile = exit 0 let optimization_options = [ - option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy; option_finline_functions_called_once; + option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; + option_fredundancy; option_finline_functions_called_once; ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -301,7 +305,8 @@ let cmdline_actions = Exact "-Os", Set option_Osize; Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); - Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); + Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); + Exact "-ffavor-branchless", Set option_ffavor_branchless; Exact "-falign-functions", Integer(fun n -> check_align n; option_falignfunctions := Some n); Exact "-falign-branch-targets", Integer(fun n -> check_align n; option_falignbranchtargets := n); Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n);] @ @@ -364,6 +369,7 @@ let cmdline_actions = (* Optimization options *) (* -f options: come in -f and -fno- variants *) @ f_opt "tailcalls" option_ftailcalls + @ f_opt "if-conversion" option_fifconversion @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy -- cgit From 31802695bf6673831674836817456142ab293e6b Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 17 Jul 2019 16:41:11 +0200 Subject: (#142) Desactivating scheduling when using -O1 optimization --- driver/Driver.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 404271cd..9748ebf6 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -185,7 +185,8 @@ Processing options: {|Optimization options: (use -fno- to turn off -f) -O Optimize the compiled code [on by default] -O0 Do not optimize the compiled code - -O1 -O2 -O3 Synonymous for -O + -O1 Perform all optimization passes except scheduling + -O2 -O3 Synonymous for -O -Os Optimize for code size in preference to code speed -ftailcalls Optimize function calls in tail position [on] -fconst-prop Perform global constant propagation [on] @@ -308,6 +309,7 @@ let cmdline_actions = [ Exact "-O0", Unit (unset_all optimization_options); Exact "-O", Unit (set_all optimization_options); + _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false); _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-fsmall-data", Integer(fun n -> option_small_data := n); -- cgit From 4c379d48b35e7c8156f3953fede31d5e47faf8ca Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 19 Jul 2019 18:59:44 +0200 Subject: helpers broke compilation --- driver/Driver.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 05d51402..288bb436 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -258,11 +258,7 @@ let dump_mnemonics destfile = let optimization_options = [ option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; -<<<<<<< HEAD option_fpostpass; option_fredundancy; option_finline_functions_called_once; -======= - option_fredundancy; option_finline; option_finline_functions_called_once; ->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf ] let set_all opts () = List.iter (fun r -> r := true) opts -- cgit From 863b65cc49fb49ad203694cac36e3cbd4f45dab7 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 3 Sep 2019 17:34:02 +0200 Subject: Stubs for Duplicate pass --- driver/Compiler.v | 64 +++++++++++++++++++++++++++++++------------------------ 1 file changed, 36 insertions(+), 28 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 6d398327..49fa2e86 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -38,6 +38,7 @@ Require RTLgen. Require Tailcall. Require Inlining. Require Renumber. +Require Duplicate. Require Constprop. Require CSE. Require Deadcode. @@ -59,6 +60,7 @@ Require RTLgenproof. Require Tailcallproof. Require Inliningproof. Require Renumberproof. +Require Duplicateproof. Require Constpropproof. Require CSEproof. Require Deadcodeproof. @@ -126,16 +128,18 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ time "Duplicating" Duplicate.transf_program @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 7) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 8) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -238,6 +242,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog + ::: mkpass Duplicateproof.match_prog ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -281,17 +286,18 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. - set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. - destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. - destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. - set (p16 := Tunneling.tunnel_program p15) in *. - destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. - set (p18 := CleanupLabels.transf_program p17) in *. - destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate. - destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. + set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. + destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + set (p17 := Tunneling.tunnel_program p16) in *. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + set (p19 := CleanupLabels.transf_program p18) in *. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -302,17 +308,18 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. - exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. - exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14; split. apply Unusedglobproof.transf_program_match; auto. - exists p15; split. apply Allocproof.transf_program_match; auto. - exists p16; split. apply Tunnelingproof.transf_program_match. - exists p17; split. apply Linearizeproof.transf_program_match; auto. - exists p18; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p20; split. apply Stackingproof.transf_program_match; auto. + exists p10; split. apply Duplicateproof.transf_program_match; auto. + exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. + exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. + exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p15; split. apply Unusedglobproof.transf_program_match; auto. + exists p16; split. apply Allocproof.transf_program_match; auto. + exists p17; split. apply Tunnelingproof.transf_program_match. + exists p18; split. apply Linearizeproof.transf_program_match; auto. + exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. + exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. + exists p21; split. apply Stackingproof.transf_program_match; auto. exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -364,7 +371,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -383,6 +390,7 @@ Ltac DestructM := eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply Duplicateproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. -- cgit From 4392758d3e9032edb1ea4a899b92fef886749fca Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 9 Sep 2019 22:34:21 +0200 Subject: -fall-loads-nontrap --- driver/Clflags.ml | 1 + driver/Compiler.v | 13 +++++++++++-- driver/Compopts.v | 3 +++ driver/Driver.ml | 1 + 4 files changed, 16 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index cf1220d1..fd8227c9 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -75,3 +75,4 @@ let option_fglobaladdroffset = ref false let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true +let option_all_loads_nontrap = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index 6d398327..d006a7d1 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -42,6 +42,7 @@ Require Constprop. Require CSE. Require Deadcode. Require Unusedglob. +Require Allnontrap. Require Allocation. Require Tunneling. Require Linearize. @@ -63,6 +64,7 @@ Require Constpropproof. Require CSEproof. Require Deadcodeproof. Require Unusedglobproof. +Require Allnontrapproof. Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -136,6 +138,8 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 7) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 8) + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -243,6 +247,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass Unusedglobproof.match_prog + ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog ::: mkpass Linearizeproof.match_prog @@ -286,7 +291,8 @@ Proof. destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. + set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. + destruct (Allocation.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. set (p16 := Tunneling.tunnel_program p15) in *. destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. set (p18 := CleanupLabels.transf_program p17) in *. @@ -307,6 +313,7 @@ Proof. exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14; split. apply Unusedglobproof.transf_program_match; auto. + exists p14bis; split. apply total_if_match. apply Allnontrapproof.transf_program_match. exists p15; split. apply Allocproof.transf_program_match; auto. exists p16; split. apply Tunnelingproof.transf_program_match. exists p17; split. apply Linearizeproof.transf_program_match; auto. @@ -364,7 +371,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -393,6 +400,8 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Unusedglobproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. eapply compose_forward_simulations. eapply Allocproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index 9c6448b7..26d888ae 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -62,3 +62,6 @@ Parameter thumb: unit -> bool. (** Flag -g. For insertion of debugging information. *) Parameter debug: unit -> bool. + +(** Flag -fall-loads-nontrap. Turn user loads into non trapping. *) +Parameter all_loads_nontrap: unit -> bool. \ No newline at end of file diff --git a/driver/Driver.ml b/driver/Driver.ml index 288bb436..59b7b222 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -391,6 +391,7 @@ let cmdline_actions = @ f_opt "xsaddr" option_fxsaddr @ f_opt "addx" option_faddx @ f_opt "coalesce-mem" option_fcoalesce_mem + @ f_opt "all-loads-nontrap" option_all_loads_nontrap (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) -- cgit From a42baf15372e64f398685aaef079a82ea0db834e Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 18 Sep 2019 14:05:09 +0200 Subject: Timings for Machblockgen, Asmblockgen and postpass scheduling --- driver/Compiler.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 6d398327..c683c136 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -144,7 +144,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.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. + @@@ time "Total Mach->Asm generation" Asmgen.transf_program. Definition transf_cminor_program (p: Cminor.program) : res Asm.program := OK p -- cgit From adc142066720798ca2e6f7709de6fba93559a336 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 20 Sep 2019 17:07:16 +0200 Subject: fix compiling --- driver/Compopts.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'driver') diff --git a/driver/Compopts.v b/driver/Compopts.v index 9c6448b7..4f86901b 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -62,3 +62,7 @@ Parameter thumb: unit -> bool. (** Flag -g. For insertion of debugging information. *) Parameter debug: unit -> bool. + +(* TODO is there a more appropriate place? *) +Require Import Coqlib. +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. -- cgit From 4e0258fcb21aa0d23c04d4b58dbd4d34672234c1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 20 Sep 2019 20:39:43 +0200 Subject: to v3.6 --- driver/Compopts.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Compopts.v b/driver/Compopts.v index 26d888ae..6e3b0d62 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -64,4 +64,8 @@ Parameter thumb: unit -> bool. Parameter debug: unit -> bool. (** Flag -fall-loads-nontrap. Turn user loads into non trapping. *) -Parameter all_loads_nontrap: unit -> bool. \ No newline at end of file +Parameter all_loads_nontrap: unit -> bool. + +(* TODO is there a more appropriate place? *) +Require Import Coqlib. +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. -- cgit From 553714035fc08f9b145b89b3dd7c455f06e917df Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Dec 2019 21:39:20 +0100 Subject: finish merge --- driver/Compiler.v | 50 +++++++++++++++++++------------------------------- 1 file changed, 19 insertions(+), 31 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index f948d595..72db86e9 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -141,8 +141,9 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 8) @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program - @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 9) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 10) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -250,8 +251,8 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) - ::: mkpass Unusedglobproof.match_prog ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) + ::: mkpass Unusedglobproof.match_prog ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog ::: mkpass Linearizeproof.match_prog @@ -290,18 +291,19 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. - set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. - destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. - destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. + destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. + set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. + destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Allocation.transf_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - set (p16 := Tunneling.tunnel_program p15) in *. - destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. - set (p18 := CleanupLabels.transf_program p17) in *. - destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate. - destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + set (p17 := Tunneling.tunnel_program p16) in *. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + set (p19 := CleanupLabels.transf_program p18) in *. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -312,25 +314,12 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. -<<<<<<< HEAD - exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. - exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14; split. apply Unusedglobproof.transf_program_match; auto. - exists p14bis; split. apply total_if_match. apply Allnontrapproof.transf_program_match. - exists p15; split. apply Allocproof.transf_program_match; auto. - exists p16; split. apply Tunnelingproof.transf_program_match. - exists p17; split. apply Linearizeproof.transf_program_match; auto. - exists p18; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p20; split. apply Stackingproof.transf_program_match; auto. -======= exists p10; split. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. exists p16; split. apply Allocproof.transf_program_match; auto. exists p17; split. apply Tunnelingproof.transf_program_match. @@ -338,7 +327,6 @@ Proof. exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. exists p21; split. apply Stackingproof.transf_program_match; auto. ->>>>>>> origin/mppa-work exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -390,7 +378,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p23)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -418,10 +406,10 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. + eapply compose_forward_simulations. + eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Allocproof.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit From 2347476653201f154ffaea84f520e41cc0f32090 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Jan 2020 12:46:10 +0100 Subject: connect forward-moves to compiler --- driver/Clflags.ml | 3 ++- driver/Compiler.v | 19 ++++++++++++++----- driver/Compopts.v | 3 +++ driver/Driver.ml | 1 + 4 files changed, 20 insertions(+), 6 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index fd8227c9..9aa4a2bf 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -74,5 +74,6 @@ let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true let option_faddx = ref false -let option_fcoalesce_mem = ref true +let option_fcoalesce_mem = ref true +let option_fforward_moves = ref true let option_all_loads_nontrap = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index 72db86e9..24964237 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -41,6 +41,7 @@ Require Renumber. Require Duplicate. Require Constprop. Require CSE. +Require ForwardMoves. Require Deadcode. Require Unusedglob. Require Allnontrap. @@ -64,6 +65,7 @@ Require Renumberproof. Require Duplicateproof. Require Constpropproof. Require CSEproof. +Require ForwardMovesproof. Require Deadcodeproof. Require Unusedglobproof. Require Allnontrapproof. @@ -138,12 +140,14 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 6) @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 7) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 8) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 9) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 10) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 11) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -250,6 +254,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) + ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) ::: mkpass Unusedglobproof.match_prog @@ -295,7 +300,8 @@ Proof. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p13bis := total_if optim_forward_moves ForwardMoves.transf_program p13) in *. + destruct (partial_if optim_redundancy Deadcode.transf_program p13bis) as [p14|e] eqn:P14; simpl in T; try discriminate. set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. @@ -318,6 +324,7 @@ Proof. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p13bis; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. exists p15; split. apply Unusedglobproof.transf_program_match; auto. @@ -378,7 +385,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p23)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p24)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -404,6 +411,8 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index 6e3b0d62..fdd2b1d6 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -66,6 +66,9 @@ Parameter debug: unit -> bool. (** Flag -fall-loads-nontrap. Turn user loads into non trapping. *) Parameter all_loads_nontrap: unit -> bool. +(** Flag -fforward-moves. Forward moves after CSE. *) +Parameter optim_forward_moves: unit -> bool. + (* TODO is there a more appropriate place? *) Require Import Coqlib. Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. diff --git a/driver/Driver.ml b/driver/Driver.ml index 59b7b222..eab66a2b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -392,6 +392,7 @@ let cmdline_actions = @ f_opt "addx" option_faddx @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap + @ f_opt "forward-moves" option_fforward_moves (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) -- cgit From fd2181ce5f6a3a5ba27349d1642ee4c59a6d9b34 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 17 Jan 2020 11:08:11 +0100 Subject: Added description for forward moves --- driver/Driver.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index eab66a2b..992cf8c4 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -199,6 +199,7 @@ Processing options: -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) + -fforward-moves Forward moves after CSE -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their single caller [on] -- cgit From 893827f54addca2facc19a8f342b380d63114130 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 27 Jan 2020 11:43:00 +0100 Subject: Added a flag to desactivate tail duplication --- driver/Clflags.ml | 1 + driver/Compiler.v | 11 ++++++----- driver/Compopts.v | 4 ++++ driver/Driver.ml | 5 ++++- 4 files changed, 15 insertions(+), 6 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 9aa4a2bf..67ec9702 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -24,6 +24,7 @@ let option_fpacked_structs = ref false let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true +let option_fduplicate = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true diff --git a/driver/Compiler.v b/driver/Compiler.v index 24964237..9f53a4fc 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -132,7 +132,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@@ time "Duplicating" Duplicate.transf_program + @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 4) @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) @@ -250,7 +250,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog - ::: mkpass Duplicateproof.match_prog + ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -296,7 +296,7 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. @@ -320,7 +320,7 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. - exists p10; split. apply Duplicateproof.transf_program_match; auto. + exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. @@ -404,7 +404,8 @@ Ltac DestructM := eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. eapply Duplicateproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index fdd2b1d6..a979c69b 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -27,6 +27,10 @@ Parameter generate_float_constants: unit -> bool. (** For value analysis. Currently always false. *) Parameter va_strict: unit -> bool. +(** Flag -fduplicate. For tail duplication optimization. Necessary to have + * bigger superblocks *) +Parameter optim_duplicate: unit -> bool. + (** Flag -ftailcalls. For tail call optimization. *) Parameter optim_tailcalls: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 992cf8c4..5d08dc6b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -199,6 +199,7 @@ Processing options: -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) + -fduplicate Perform tail duplication to form superblocks on predicted traces -fforward-moves Forward moves after CSE -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -260,6 +261,7 @@ let dump_mnemonics destfile = let optimization_options = [ option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; option_fpostpass; option_fredundancy; option_finline_functions_called_once; + option_fduplicate ] let set_all opts () = List.iter (fun r -> r := true) opts @@ -310,7 +312,7 @@ let cmdline_actions = [ Exact "-O0", Unit (unset_all optimization_options); Exact "-O", Unit (set_all optimization_options); - _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false); + _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false; option_fduplicate := false); _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-Obranchless", Set option_Obranchless; @@ -384,6 +386,7 @@ let cmdline_actions = @ f_opt "cse" option_fcse @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass + @ f_opt "duplicate" option_fduplicate @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once -- cgit From b54d18e2e26b3f7745870894d8087162eb33c545 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 27 Jan 2020 13:25:56 +0100 Subject: Tail duplication optimization defaulting to off --- driver/Clflags.ml | 2 +- driver/Driver.ml | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 67ec9702..088845fe 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -24,10 +24,10 @@ let option_fpacked_structs = ref false let option_ffpu = ref true let option_ffloatconstprop = ref 2 let option_ftailcalls = ref true -let option_fduplicate = ref true let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true +let option_fduplicate = ref false let option_fpostpass = ref true let option_fpostpass_sched = ref "list" let option_fifconversion = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 5d08dc6b..129248dc 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -261,7 +261,6 @@ let dump_mnemonics destfile = let optimization_options = [ option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse; option_fpostpass; option_fredundancy; option_finline_functions_called_once; - option_fduplicate ] let set_all opts () = List.iter (fun r -> r := true) opts -- cgit From 7dca7590aa212806ee939244b253a6a067f34bfc Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 3 Feb 2020 10:52:53 +0100 Subject: Added flag to desactivate condition inversion --- driver/Clflags.ml | 1 + driver/Driver.ml | 3 +++ 2 files changed, 4 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 088845fe..a195e38b 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,6 +28,7 @@ let option_fconstprop = ref true let option_fcse = ref true let option_fredundancy = ref true let option_fduplicate = ref false +let option_finvertcond = ref true (* only active if option_fduplicate is also true *) let option_fpostpass = ref true let option_fpostpass_sched = ref "list" let option_fifconversion = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 129248dc..3af1a937 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -200,6 +200,8 @@ Processing options: -fpostpass= Perform postpass scheduling with the specified optimization [list] (=list: list scheduling, =ilp: ILP, =greedy: just packing bundles) -fduplicate Perform tail duplication to form superblocks on predicted traces + -finvertcond Invert conditions based on predicted paths (to prefer fallthrough). + Requires -fduplicate to be also activated [on] -fforward-moves Forward moves after CSE -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -386,6 +388,7 @@ let cmdline_actions = @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass @ f_opt "duplicate" option_fduplicate + @ f_opt "invertcond" option_finvertcond @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once -- cgit From 117a26880e27ae7d8efcb26d194c5ded3be642d6 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 12 Feb 2020 16:47:03 +0100 Subject: Added option -ftracelinearize which linearizes based on ifnot branches --- driver/Clflags.ml | 1 + driver/Driver.ml | 3 +++ 2 files changed, 4 insertions(+) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index a195e38b..a4ebee9c 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -29,6 +29,7 @@ let option_fcse = ref true let option_fredundancy = ref true let option_fduplicate = ref false let option_finvertcond = ref true (* only active if option_fduplicate is also true *) +let option_ftracelinearize = ref false let option_fpostpass = ref true let option_fpostpass_sched = ref "list" let option_fifconversion = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 3af1a937..70a3739b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -202,6 +202,8 @@ Processing options: -fduplicate Perform tail duplication to form superblocks on predicted traces -finvertcond Invert conditions based on predicted paths (to prefer fallthrough). Requires -fduplicate to be also activated [on] + -ftracelinearize Linearizes based on the traces identified by duplicate phase + It is recommended to also activate -fduplicate with this pass [off] -fforward-moves Forward moves after CSE -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -389,6 +391,7 @@ let cmdline_actions = @ f_opt "postpass" option_fpostpass @ f_opt "duplicate" option_fduplicate @ f_opt "invertcond" option_finvertcond + @ f_opt "tracelinearize" option_ftracelinearize @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched @ f_opt "inline" option_finline @ f_opt "inline-functions-called-once" option_finline_functions_called_once -- cgit