From 07f2bfbd62568e2e0d983ccb33d020bf6985e874 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 29 Mar 2020 18:30:01 +0200 Subject: nop insertion at entrypoint --- Makefile | 2 +- driver/Compiler.v | 38 +++++++++++++++++++++++--------------- 2 files changed, 24 insertions(+), 16 deletions(-) diff --git a/Makefile b/Makefile index 8aa5e98a..ec5e2cd0 100644 --- a/Makefile +++ b/Makefile @@ -94,7 +94,7 @@ BACKEND=\ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ ForwardMoves.v ForwardMovesproof.v \ - FirstNop.v \ + FirstNop.v FirstNopproof.v \ Allnontrap.v Allnontrapproof.v \ Allocation.v Allocproof.v \ Tunneling.v Tunnelingproof.v \ diff --git a/driver/Compiler.v b/driver/Compiler.v index 47fb8236..cc1e7917 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -37,6 +37,7 @@ Require Selection. Require RTLgen. Require Tailcall. Require Inlining. +Require FirstNop. Require Renumber. Require Duplicate. Require Constprop. @@ -63,6 +64,7 @@ Require Selectionproof. Require RTLgenproof. Require Tailcallproof. Require Inliningproof. +Require FirstNopproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. @@ -134,28 +136,30 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 1) @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) - @@ time "Renumbering" Renumber.transf_program + @@ time "Inserting initial nop" FirstNop.transf_program @@ print (print_RTL 3) - @@@ time "Tail-duplicating" Duplicate.transf_program + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ time "Tail-duplicating" Duplicate.transf_program @@ print (print_RTL 5) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 7) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 8) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 9) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 10) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 11) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 12) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 13) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 14) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -257,6 +261,7 @@ Definition CompCert's_passes := ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog + ::: mkpass FirstNopproof.match_prog ::: mkpass Renumberproof.match_prog ::: mkpass Duplicateproof.match_prog ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) @@ -305,8 +310,9 @@ Proof. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. 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. + set (p9 := FirstNop.transf_program p8) in *. + set (p9bis := Renumber.transf_program p9) in *. + destruct (Duplicate.transf_program p9bis) 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. @@ -331,7 +337,8 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. 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 p9; split. apply FirstNopproof.transf_program_match; auto. + exists p9bis; split. apply Renumberproof.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. @@ -399,7 +406,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 p26)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p27)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -417,6 +424,7 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply FirstNopproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Duplicateproof.transf_program_correct; eassumption. -- cgit From 4aad20a92dc926d8c537e65946ca03bf2b6b02b9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 29 Mar 2020 23:01:15 +0200 Subject: begin coding dead code injector --- backend/Inject.v | 60 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 backend/Inject.v diff --git a/backend/Inject.v b/backend/Inject.v new file mode 100644 index 00000000..dd70556a --- /dev/null +++ b/backend/Inject.v @@ -0,0 +1,60 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. + +Inductive inj_instr : Type := + | INJop: operation -> list reg -> reg -> inj_instr + | INJload: memory_chunk -> addressing -> list reg -> reg -> inj_instr. + +Definition inject_instr (i : inj_instr) (pc' : node) : instruction := + match i with + | INJop op args dst => Iop op args dst pc' + | INJload chunk addr args dst => Iload NOTRAP chunk addr args dst pc' + end. + +Fixpoint inject_list (prog : code) (pc : node) (dst : node) + (l : list inj_instr) : node * code := + let pc' := Pos.succ pc in + match l with + | nil => (pc', PTree.set pc (Inop dst) prog) + | h::t => + inject_list (PTree.set pc (inject_instr h pc') prog) + pc' dst t + end. + +Definition successor (i : instruction) : node := + match i with + | Inop pc' => pc' + | Iop _ _ _ pc' => pc' + | Iload _ _ _ _ _ pc' => pc' + | Istore _ _ _ _ pc' => pc' + | Icall _ _ _ _ pc' => pc' + | Ibuiltin _ _ _ pc' => pc' + | Icond _ _ pc' _ => pc' + | Itailcall _ _ _ + | Ijumptable _ _ + | Ireturn _ => 1%positive + end. + +Definition alter_successor (i : instruction) (pc' : node) : instruction := + match i with + | Inop _ => Inop pc' + | Iop op args dst _ => Iop op args dst pc' + | Iload trap chunk addr args dst _ => Iload trap chunk addr args dst pc' + | Istore chunk addr args src _ => Istore chunk addr args src pc' + | Icall sig ri args dst _ => Icall sig ri args dst pc' + | Ibuiltin ef args res _ => Ibuiltin ef args res pc' + | Icond cond args _ pc2 => Icond cond args pc' pc2 + | Itailcall _ _ _ + | Ijumptable _ _ + | Ireturn _ => i + end. + +Definition inject_at (prog : code) (pc extra_pc : node) + (l : list inj_instr) : node * code := + match PTree.get pc prog with + | Some i => + inject_list (PTree.set pc (alter_successor i extra_pc) prog) + extra_pc (successor i) l + | None => inject_list prog extra_pc 1%positive l (* does not happen *) + end. -- cgit From fd00d28f8065acf9b09a6510e1612a91e30ca29c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 10:12:09 +0200 Subject: more on injection --- Makefile | 1 + backend/Inject.v | 6 ++++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index ec5e2cd0..4cf9ccf1 100644 --- a/Makefile +++ b/Makefile @@ -86,6 +86,7 @@ BACKEND=\ Kildall.v Liveness.v \ ValueDomain.v ValueAOp.v ValueAnalysis.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ + Inject.v \ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ diff --git a/backend/Inject.v b/backend/Inject.v index dd70556a..66ef9ce8 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -2,6 +2,8 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL. +Local Open Scope positive. + Inductive inj_instr : Type := | INJop: operation -> list reg -> reg -> inj_instr | INJload: memory_chunk -> addressing -> list reg -> reg -> inj_instr. @@ -33,7 +35,7 @@ Definition successor (i : instruction) : node := | Icond _ _ pc' _ => pc' | Itailcall _ _ _ | Ijumptable _ _ - | Ireturn _ => 1%positive + | Ireturn _ => 1 end. Definition alter_successor (i : instruction) (pc' : node) : instruction := @@ -56,5 +58,5 @@ Definition inject_at (prog : code) (pc extra_pc : node) | Some i => inject_list (PTree.set pc (alter_successor i extra_pc) prog) extra_pc (successor i) l - | None => inject_list prog extra_pc 1%positive l (* does not happen *) + | None => inject_list prog extra_pc 1 l (* does not happen *) end. -- cgit From bae72eeffdd23c3444a097f5f901333c6c70af8b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 10:59:38 +0200 Subject: more on injection --- backend/Inject.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/backend/Inject.v b/backend/Inject.v index 66ef9ce8..a3f2b343 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -60,3 +60,13 @@ Definition inject_at (prog : code) (pc extra_pc : node) extra_pc (successor i) l | None => inject_list prog extra_pc 1 l (* does not happen *) end. + +Definition inject_at' (already : node * code) pc l := + let (extra_pc, prog) := already in + inject_at prog pc extra_pc l. + +Definition inject' (prog : code) (extra_pc : node) (injections : PTree.t (list inj_instr)) := + PTree.fold inject_at' injections (extra_pc, prog). + +Definition inject prog extra_pc injections : code := + snd (inject' prog extra_pc injections). -- cgit From 46b9d0b4e7b37609ec62969af7354967f19e8822 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 11:49:47 +0200 Subject: preservation lemmas --- backend/Injectproof.v | 155 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 155 insertions(+) create mode 100644 backend/Injectproof.v diff --git a/backend/Injectproof.v b/backend/Injectproof.v new file mode 100644 index 00000000..b7bc4e64 --- /dev/null +++ b/backend/Injectproof.v @@ -0,0 +1,155 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. +Require Import Inject. +Require Import Lia. + +Local Open Scope positive. + +Lemma inject_list_preserves: + forall l prog pc dst pc0, + pc0 < pc -> + PTree.get pc0 (snd (inject_list prog pc dst l)) = PTree.get pc0 prog. +Proof. + induction l; intros; simpl. + - apply PTree.gso. lia. + - rewrite IHl by lia. + apply PTree.gso. lia. +Qed. + +Fixpoint pos_add_nat x n := + match n with + | O => x + | S n' => Pos.succ (pos_add_nat x n') + end. + +Lemma pos_add_nat_increases : forall x n, x <= (pos_add_nat x n). +Proof. + induction n; simpl; lia. +Qed. + +Lemma pos_add_nat_succ : forall n x, + Pos.succ (pos_add_nat x n) = pos_add_nat (Pos.succ x) n. +Proof. + induction n; simpl; intros; trivial. + rewrite IHn. + reflexivity. +Qed. + +Lemma inject_list_increases: + forall l prog pc dst, + (fst (inject_list prog pc dst l)) = pos_add_nat pc (S (List.length l)). +Proof. + induction l; simpl; intros; trivial. + rewrite IHl. + simpl. + rewrite <- pos_add_nat_succ. + reflexivity. +Qed. + +Lemma inject_at_preserves : + forall prog pc extra_pc l pc0, + pc0 < extra_pc -> + pc0 <> pc -> + PTree.get pc0 (snd (inject_at prog pc extra_pc l)) = PTree.get pc0 prog. +Proof. + intros. unfold inject_at. + destruct (PTree.get pc prog) eqn:GET. + - rewrite inject_list_preserves; trivial. + apply PTree.gso; lia. + - apply inject_list_preserves; trivial. +Qed. + +Lemma inject_at_redirects: + forall prog pc extra_pc l i, + pc < extra_pc -> + PTree.get pc prog = Some i -> + PTree.get pc (snd (inject_at prog pc extra_pc l)) = + Some (alter_successor i extra_pc). +Proof. + intros until i. intros BEFORE GET. unfold inject_at. + rewrite GET. + rewrite inject_list_preserves by trivial. + apply PTree.gss. +Qed. + +Lemma inject_at_redirects_none: + forall prog pc extra_pc l, + pc < extra_pc -> + PTree.get pc prog = None -> + PTree.get pc (snd (inject_at prog pc extra_pc l)) = None. +Proof. + intros until l. intros BEFORE GET. unfold inject_at. + rewrite GET. + rewrite inject_list_preserves by trivial. + assumption. +Qed. + +Lemma inject_at_increases: + forall prog pc extra_pc l, + (fst (inject_at prog pc extra_pc l)) = pos_add_nat extra_pc (S (List.length l)). +Proof. + intros. unfold inject_at. + destruct (PTree.get pc prog). + all: apply inject_list_increases. +Qed. + +Definition inject_l (prog : code) extra_pc injections := + List.fold_left (fun already (injection : node * (list inj_instr)) => + inject_at' already (fst injection) (snd injection)) + injections + (extra_pc, prog). + +Lemma pair_expand: + forall { A B : Type } (p : A*B), + p = ((fst p), (snd p)). +Proof. + destruct p; simpl; trivial. +Qed. + +Lemma inject_l_preserves : + forall injections prog extra_pc pc0, + pc0 < extra_pc -> + List.forallb (fun injection => if peq (fst injection) pc0 then false else true) injections = true -> + PTree.get pc0 (snd (inject_l prog extra_pc injections)) = PTree.get pc0 prog. +Proof. + induction injections; + intros until pc0; intros BEFORE ALL; simpl; trivial. + unfold inject_l. + destruct a as [pc l]. simpl. + simpl in ALL. + rewrite andb_true_iff in ALL. + destruct ALL as [NEQ ALL]. + rewrite pair_expand with (p := inject_at prog pc extra_pc l). + fold (inject_l (snd (inject_at prog pc extra_pc l)) + (fst (inject_at prog pc extra_pc l)) + injections). + rewrite IHinjections; trivial. + - apply inject_at_preserves; trivial. + destruct (peq pc pc0); congruence. + - rewrite inject_at_increases. + pose proof (pos_add_nat_increases extra_pc (S (Datatypes.length l))). + lia. +Qed. + +Lemma inject'_preserves : + forall injections prog extra_pc pc0, + pc0 < extra_pc -> + PTree.get pc0 injections = None -> + PTree.get pc0 (snd (inject' prog extra_pc injections)) = PTree.get pc0 prog. +Proof. + intros. unfold inject'. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : node * code) (p : positive * list inj_instr) => + inject_at' a (fst p) (snd p)) (PTree.elements injections) + (extra_pc, prog)) with (inject_l prog extra_pc (PTree.elements injections)). + apply inject_l_preserves; trivial. + rewrite List.forallb_forall. + intros injection IN. + destruct injection as [pc l]. + simpl. + apply PTree.elements_complete in IN. + destruct (peq pc pc0); trivial. + congruence. +Qed. -- cgit From a117ebbcb63ef0d73772e0073f23238a5642723a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 14:26:25 +0200 Subject: injector injects.. --- backend/Injectproof.v | 69 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index b7bc4e64..7a991a8c 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -47,6 +47,65 @@ Proof. reflexivity. Qed. +Program Fixpoint bounded_nth + {T : Type} (k : nat) (l : list T) (BOUND : (k < List.length l)%nat) : T := + match k, l with + | O, h::_ => h + | (S k'), _::l' => bounded_nth k' l' _ + | _, nil => _ + end. +Obligation 1. +Proof. + simpl in BOUND. + lia. +Qed. +Obligation 2. +Proof. + simpl in BOUND. + lia. +Qed. + +Program Definition bounded_nth_S_statement : Prop := + forall {T : Type} (k : nat) (h : T) (l : list T) (BOUND : (k < List.length l)%nat), + bounded_nth (S k) (h::l) _ = bounded_nth k l BOUND. +Obligation 1. +lia. +Qed. + +Lemma bounded_nth_proof_irr : + forall {T : Type} (k : nat) (l : list T) + (BOUND1 BOUND2 : (k < List.length l)%nat), + (bounded_nth k l BOUND1) = (bounded_nth k l BOUND2). +Proof. + induction k; destruct l; simpl; intros; trivial; lia. +Qed. + +Lemma bounded_nth_S : bounded_nth_S_statement. +Proof. + unfold bounded_nth_S_statement. + induction k; destruct l; simpl; intros; trivial. + 1, 2: lia. + apply bounded_nth_proof_irr. +Qed. + +Lemma inject_list_injected: + forall l prog pc dst k (BOUND : (k < (List.length l))%nat), + PTree.get (pos_add_nat pc k) (snd (inject_list prog pc dst l)) = + Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat pc k))). +Proof. + induction l; simpl; intros. + - lia. + - simpl. + destruct k as [ | k]. + + admit. + + simpl pos_add_nat. + rewrite pos_add_nat_succ. + erewrite IHl. + f_equal. f_equal. + simpl. + apply bounded_nth_proof_irr. +Qed. + Lemma inject_at_preserves : forall prog pc extra_pc l pc0, pc0 < extra_pc -> @@ -153,3 +212,13 @@ Proof. destruct (peq pc pc0); trivial. congruence. Qed. + +Lemma inject_preserves : + forall injections prog extra_pc pc0, + pc0 < extra_pc -> + PTree.get pc0 injections = None -> + PTree.get pc0 (inject prog extra_pc injections) = PTree.get pc0 prog. +Proof. + unfold inject'. + apply inject'_preserves. +Qed. -- cgit From d1adc4858ec70963233945542b717fcd1459a96a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 14:33:35 +0200 Subject: injector injects the end --- backend/Injectproof.v | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 7a991a8c..eeaadb2a 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -96,16 +96,31 @@ Proof. induction l; simpl; intros. - lia. - simpl. - destruct k as [ | k]. - + admit. - + simpl pos_add_nat. - rewrite pos_add_nat_succ. + destruct k as [ | k]; simpl pos_add_nat. + + simpl bounded_nth. + rewrite inject_list_preserves by lia. + apply PTree.gss. + + rewrite pos_add_nat_succ. erewrite IHl. f_equal. f_equal. simpl. apply bounded_nth_proof_irr. + Unshelve. + lia. Qed. +Lemma inject_list_injected_end: + forall l prog pc dst, + PTree.get (pos_add_nat pc (List.length l)) + (snd (inject_list prog pc dst l)) = + Some (Inop dst). +Proof. + induction l; simpl; intros. + - apply PTree.gss. + - rewrite pos_add_nat_succ. + apply IHl. +Qed. + Lemma inject_at_preserves : forall prog pc extra_pc l pc0, pc0 < extra_pc -> -- cgit From 020f1dfa53642fa452f73cbe71103572c2cc2cea Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 14:55:49 +0200 Subject: inject_at injects the end --- backend/Injectproof.v | 31 ++++++++++++++++++++++++++----- 1 file changed, 26 insertions(+), 5 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index eeaadb2a..a568d519 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -168,11 +168,26 @@ Proof. all: apply inject_list_increases. Qed. -Definition inject_l (prog : code) extra_pc injections := - List.fold_left (fun already (injection : node * (list inj_instr)) => - inject_at' already (fst injection) (snd injection)) - injections - (extra_pc, prog). +Lemma inject_at_injected: + forall l prog pc extra_pc k (BOUND : (k < (List.length l))%nat), + PTree.get (pos_add_nat extra_pc k) (snd (inject_at prog pc extra_pc l)) = + Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat extra_pc k))). +Proof. + intros. unfold inject_at. + destruct (prog ! pc); apply inject_list_injected. +Qed. + +Lemma inject_at_injected_end: + forall l prog pc extra_pc i, + PTree.get pc prog = Some i -> + PTree.get (pos_add_nat extra_pc (List.length l)) + (snd (inject_at prog pc extra_pc l)) = + Some (Inop (successor i)). +Proof. + intros until i. intro REW. unfold inject_at. + rewrite REW. + apply inject_list_injected_end. +Qed. Lemma pair_expand: forall { A B : Type } (p : A*B), @@ -181,6 +196,12 @@ Proof. destruct p; simpl; trivial. Qed. +Definition inject_l (prog : code) extra_pc injections := + List.fold_left (fun already (injection : node * (list inj_instr)) => + inject_at' already (fst injection) (snd injection)) + injections + (extra_pc, prog). + Lemma inject_l_preserves : forall injections prog extra_pc pc0, pc0 < extra_pc -> -- cgit From 4c65d76a7b00c01f812db3e1464fec4ecb5562c5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 15:20:10 +0200 Subject: injection positions are ok --- backend/Injectproof.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index a568d519..838230e4 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -196,12 +196,36 @@ Proof. destruct p; simpl; trivial. Qed. +Fixpoint inject_l_position extra_pc + (injections : list (node * (list inj_instr))) : node := + match injections with + | nil => extra_pc + | (pc,l)::t => inject_l_position + (Pos.succ (pos_add_nat extra_pc (List.length l))) t + end. + Definition inject_l (prog : code) extra_pc injections := List.fold_left (fun already (injection : node * (list inj_instr)) => inject_at' already (fst injection) (snd injection)) injections (extra_pc, prog). +Lemma inject_l_position_ok: + forall injections prog extra_pc, + (fst (inject_l prog extra_pc injections)) = + inject_l_position extra_pc injections. +Proof. + induction injections; intros; simpl; trivial. + destruct a as [pc l]. + unfold inject_l. simpl. + rewrite (pair_expand (inject_at prog pc extra_pc l)). + fold (inject_l (snd (inject_at prog pc extra_pc l)) (fst (inject_at prog pc extra_pc l)) injections). + rewrite IHinjections. + f_equal. + rewrite inject_at_increases. + reflexivity. +Qed. + Lemma inject_l_preserves : forall injections prog extra_pc pc0, pc0 < extra_pc -> -- cgit From a4fcfbeb5bdef46b41f2a553fff72d98ea38629b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 16:26:54 +0200 Subject: injection positions.. --- backend/Injectproof.v | 53 +++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 49 insertions(+), 4 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 838230e4..41bbd028 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -197,11 +197,17 @@ Proof. Qed. Fixpoint inject_l_position extra_pc - (injections : list (node * (list inj_instr))) : node := + (injections : list (node * (list inj_instr))) + (k : nat) {struct injections} : node := match injections with | nil => extra_pc - | (pc,l)::t => inject_l_position - (Pos.succ (pos_add_nat extra_pc (List.length l))) t + | (pc,l)::l' => + match k with + | O => extra_pc + | S k' => + inject_l_position + (Pos.succ (pos_add_nat extra_pc (List.length l))) l' k' + end end. Definition inject_l (prog : code) extra_pc injections := @@ -210,6 +216,7 @@ Definition inject_l (prog : code) extra_pc injections := injections (extra_pc, prog). +(* Lemma inject_l_position_ok: forall injections prog extra_pc, (fst (inject_l prog extra_pc injections)) = @@ -225,7 +232,7 @@ Proof. rewrite inject_at_increases. reflexivity. Qed. - +*) Lemma inject_l_preserves : forall injections prog extra_pc pc0, pc0 < extra_pc -> @@ -251,6 +258,44 @@ Proof. lia. Qed. +Lemma nth_error_nil : forall { T : Type} k, + nth_error (@nil T) k = None. +Proof. + destruct k; simpl; trivial. +Qed. + +Lemma inject_l_injected: + forall injections prog injnum pc l extra_pc k + (NUMBER : nth_error injections injnum = Some (pc, l)) + (BOUND : (k < (List.length l))%nat), + PTree.get (pos_add_nat (inject_l_position extra_pc injections injnum) k) + (snd (inject_l prog extra_pc injections)) = + Some (inject_instr (bounded_nth k l BOUND) + (Pos.succ (pos_add_nat (inject_l_position extra_pc injections injnum) k))). +Proof. + induction injections; intros. + { rewrite nth_error_nil in NUMBER. + discriminate NUMBER. + } + unfold inject_l. + destruct a as [pc' l']. + simpl fold_left. + rewrite pair_expand with (p := inject_at prog pc' extra_pc l'). + progress fold (inject_l (snd (inject_at prog pc' extra_pc l')) + (fst (inject_at prog pc' extra_pc l')) + injections). + destruct injnum as [ | injnum']; simpl in NUMBER. + { inv NUMBER. + rewrite inject_l_preserves; simpl. + - apply inject_at_injected. + - rewrite inject_at_increases. + simpl. + } + rewrite <- IHinjections. + + destruct (prog ! pc); apply inject_list_injected. +Qed. + Lemma inject'_preserves : forall injections prog extra_pc pc0, pc0 < extra_pc -> -- cgit From 94e9e486b3bf1dfe6dc095973709b1716d07515d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 16:50:55 +0200 Subject: inject_l injected --- backend/Injectproof.v | 47 +++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 43 insertions(+), 4 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 41bbd028..a805aa3e 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -36,6 +36,21 @@ Proof. reflexivity. Qed. +Lemma pos_add_nat_monotone : forall x n1 n2, + (n1 < n2) % nat -> + (pos_add_nat x n1) < (pos_add_nat x n2). +Proof. + induction n1; destruct n2; intros. + - lia. + - simpl. + pose proof (pos_add_nat_increases x n2). + lia. + - lia. + - simpl. + specialize IHn1 with n2. + lia. +Qed. + Lemma inject_list_increases: forall l prog pc dst, (fst (inject_list prog pc dst l)) = pos_add_nat pc (S (List.length l)). @@ -266,6 +281,7 @@ Qed. Lemma inject_l_injected: forall injections prog injnum pc l extra_pc k + (BELOW : forallb (fun injection => (fst injection) Date: Mon, 30 Mar 2020 17:40:54 +0200 Subject: inject_l injected_end --- backend/Injectproof.v | 90 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 90 insertions(+) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index a805aa3e..f048bfb9 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -335,6 +335,96 @@ Proof. lia. Qed. +Lemma inject_l_injected_end: + forall injections prog injnum pc i l extra_pc + (BEFORE : PTree.get pc prog = Some i) + (DISTINCT : list_norepet (map fst injections)) + (BELOW : forallb (fun injection => (fst injection) -- cgit From b937a4c10226930b7109ae6c9707255e53a0dd2b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 18:27:23 +0200 Subject: inject_l_redirects --- backend/Injectproof.v | 82 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index f048bfb9..b0dcfad5 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -425,6 +425,88 @@ Proof. } Qed. + +Lemma inject_l_redirects: + forall injections prog injnum pc i l extra_pc + (BEFORE : PTree.get pc prog = Some i) + (DISTINCT : list_norepet (map fst injections)) + (BELOW : forallb (fun injection => (fst injection) -- cgit From 27c8e10f4e0a3eee6bf9feb03d0f12990f74badd Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 18:46:50 +0200 Subject: use inject_l --- Makefile | 2 +- backend/Inject.v | 7 +++++++ backend/Injectproof.v | 21 +++------------------ 3 files changed, 11 insertions(+), 19 deletions(-) diff --git a/Makefile b/Makefile index 4cf9ccf1..f005d048 100644 --- a/Makefile +++ b/Makefile @@ -86,7 +86,7 @@ BACKEND=\ Kildall.v Liveness.v \ ValueDomain.v ValueAOp.v ValueAnalysis.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ - Inject.v \ + Inject.v Injectproof.v \ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ diff --git a/backend/Inject.v b/backend/Inject.v index a3f2b343..6799ec8a 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -65,8 +65,15 @@ Definition inject_at' (already : node * code) pc l := let (extra_pc, prog) := already in inject_at prog pc extra_pc l. +Definition inject_l (prog : code) extra_pc injections := + List.fold_left (fun already (injection : node * (list inj_instr)) => + inject_at' already (fst injection) (snd injection)) + injections + (extra_pc, prog). +(* Definition inject' (prog : code) (extra_pc : node) (injections : PTree.t (list inj_instr)) := PTree.fold inject_at' injections (extra_pc, prog). Definition inject prog extra_pc injections : code := snd (inject' prog extra_pc injections). +*) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index b0dcfad5..80b217bc 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -81,7 +81,7 @@ Proof. Qed. Program Definition bounded_nth_S_statement : Prop := - forall {T : Type} (k : nat) (h : T) (l : list T) (BOUND : (k < List.length l)%nat), + forall (T : Type) (k : nat) (h : T) (l : list T) (BOUND : (k < List.length l)%nat), bounded_nth (S k) (h::l) _ = bounded_nth k l BOUND. Obligation 1. lia. @@ -231,23 +231,6 @@ Definition inject_l (prog : code) extra_pc injections := injections (extra_pc, prog). -(* -Lemma inject_l_position_ok: - forall injections prog extra_pc, - (fst (inject_l prog extra_pc injections)) = - inject_l_position extra_pc injections. -Proof. - induction injections; intros; simpl; trivial. - destruct a as [pc l]. - unfold inject_l. simpl. - rewrite (pair_expand (inject_at prog pc extra_pc l)). - fold (inject_l (snd (inject_at prog pc extra_pc l)) (fst (inject_at prog pc extra_pc l)) injections). - rewrite IHinjections. - f_equal. - rewrite inject_at_increases. - reflexivity. -Qed. -*) Lemma inject_l_preserves : forall injections prog extra_pc pc0, pc0 < extra_pc -> @@ -507,6 +490,7 @@ Proof. } Qed. +(* Lemma inject'_preserves : forall injections prog extra_pc pc0, pc0 < extra_pc -> @@ -538,3 +522,4 @@ Proof. unfold inject'. apply inject'_preserves. Qed. +*) -- cgit From 3655a7585c925c0bb5825a8b65bec3d8323ad3b6 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 19:20:24 +0200 Subject: injector wrapper function --- backend/Inject.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/backend/Inject.v b/backend/Inject.v index 6799ec8a..e65cb060 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -77,3 +77,25 @@ Definition inject' (prog : code) (extra_pc : node) (injections : PTree.t (list i Definition inject prog extra_pc injections : code := snd (inject' prog extra_pc injections). *) + +Section INJECTOR. + Variable gen_injections : function -> PTree.t (list inj_instr). + + Definition transf_function (f : function) : res function := + let injections := PTree.elements (gen_injections f) in + let max_pc := max_pc_function f in + if List.forallb (fun injection => (fst injection) <=? max_pc) injections + then + OK {| fn_sig := f.(fn_sig); + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := snd (inject_l (fn_code f) (Pos.succ max_pc) injections); + fn_entrypoint := f.(fn_entrypoint) |} + else Error (msg "Inject.transf_function: injections at bad locations"). + +Definition transf_fundef (fd: fundef) : res fundef := + AST.transf_partial_fundef transf_function fd. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p. +End INJECTOR. -- cgit From cc2518fa3ace7e1a74f3717434fc6daebea522fa Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 19:49:57 +0200 Subject: more proofs on injector --- backend/Injectproof.v | 174 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 173 insertions(+), 1 deletion(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 80b217bc..05c57569 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1,6 +1,6 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. -Require Import Memory Registers Op RTL. +Require Import Memory Registers Op RTL Globalenvs Values. Require Import Inject. Require Import Lia. @@ -523,3 +523,175 @@ Proof. apply inject'_preserves. Qed. *) + +Section INJECTOR. + Variable gen_injections : function -> PTree.t (list inj_instr). + + Definition match_prog (p tp: RTL.program) := + match_program (fun ctx f tf => transf_fundef gen_injections f = OK tf) eq p tp. + + Lemma transf_program_match: + forall p tp, transf_program gen_injections p = OK tp -> match_prog p tp. + Proof. + intros. eapply match_transform_partial_program; eauto. + Qed. + + Section PRESERVATION. + + Variables prog tprog: program. + Hypothesis TRANSF: match_prog prog tprog. + Let ge := Genv.globalenv prog. + Let tge := Genv.globalenv tprog. + + Definition match_regs (f : function) (rs rs' : regset) := + forall r, r <= max_reg_function f -> (rs'#r = rs#r). + + Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := + | match_frames_intro: forall res f tf sp pc rs trs + (FUN : transf_function gen_injections f = OK tf) + (REGS : match_regs f rs trs), + match_frames (Stackframe res f sp pc rs) + (Stackframe res tf sp pc trs). + + Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall s f tf sp pc rs trs m ts + (FUN : transf_function gen_injections f = OK tf) + (STACKS: list_forall2 match_frames s ts) + (REGS: match_regs f rs trs), + match_states (State s f sp pc rs m) (State ts tf sp pc trs m) + | match_states_call: + forall s fd tfd args m ts + (FUN : transf_fundef gen_injections fd = OK tfd) + (STACKS: list_forall2 match_frames s ts), + match_states (Callstate s fd args m) (Callstate ts tfd args m) + | match_states_return: + forall s res m ts + (STACKS: list_forall2 match_frames s ts), + match_states (Returnstate s res m) + (Returnstate ts res m). + + Lemma functions_translated: + forall (v: val) (f: RTL.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ + transf_fundef gen_injections f = OK tf. + Proof. + apply (Genv.find_funct_transf_partial TRANSF). + Qed. + + Lemma function_ptr_translated: + forall (b: block) (f: RTL.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ + transf_fundef gen_injections f = OK tf. + Proof. + apply (Genv.find_funct_ptr_transf_partial TRANSF). + Qed. + + Lemma symbols_preserved: + forall id, + Genv.find_symbol tge id = Genv.find_symbol ge id. + Proof. + apply (Genv.find_symbol_match TRANSF). + Qed. + + Lemma senv_preserved: + Senv.equiv ge tge. + Proof. + apply (Genv.senv_match TRANSF). + Qed. + + Lemma sig_preserved: + forall f tf, transf_fundef gen_injections f = OK tf + -> funsig tf = funsig f. + Proof. + destruct f; simpl; intros; monadInv H; trivial. + unfold transf_function in *. + destruct forallb in EQ. + 2: discriminate. + inv EQ. + reflexivity. + Qed. + + Lemma stacksize_preserved: + forall f tf, transf_function gen_injections f = OK tf -> + fn_stacksize tf = fn_stacksize f. + Proof. + destruct f. + unfold transf_function. + intros. + destruct forallb in H. + 2: discriminate. + inv H. + reflexivity. + Qed. + + Lemma params_preserved: + forall f tf, transf_function gen_injections f = OK tf -> + fn_params tf = fn_params f. + Proof. + destruct f. + unfold transf_function. + intros. + destruct forallb in H. + 2: discriminate. + inv H. + reflexivity. + Qed. + + Lemma entrypoint_preserved: + forall f tf, transf_function gen_injections f = OK tf -> + fn_entrypoint tf = fn_entrypoint f. + Proof. + destruct f. + unfold transf_function. + intros. + destruct forallb in H. + 2: discriminate. + inv H. + reflexivity. + Qed. + + Lemma sig_preserved2: + forall f tf, transf_function gen_injections f = OK tf -> + fn_sig tf = fn_sig f. + Proof. + destruct f. + unfold transf_function. + intros. + destruct forallb in H. + 2: discriminate. + inv H. + reflexivity. + Qed. + + Lemma transf_initial_states: + forall S1, RTL.initial_state prog S1 -> + exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2. + Proof. + intros. inversion H. + exploit function_ptr_translated; eauto. + intros (tf & A & B). + exists (Callstate nil tf nil m0); split. + - econstructor; eauto. + + eapply (Genv.init_mem_match TRANSF); eauto. + + replace (prog_main tprog) with (prog_main prog). + rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main; eauto. + + rewrite <- H3. eapply sig_preserved; eauto. + - constructor; trivial. + constructor. + Qed. + + Lemma transf_final_states: + forall S1 S2 r, match_states S1 S2 -> + final_state S1 r -> final_state S2 r. + Proof. + intros. inv H0. inv H. inv STACKS. constructor. + Qed. + +End PRESERVATION. +End INJECTOR. -- cgit From 3d4806d52f65099192adc34a2c6b2c5979537fd3 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 20:11:36 +0200 Subject: additional checks --- backend/Inject.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/backend/Inject.v b/backend/Inject.v index e65cb060..6da10019 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -84,7 +84,17 @@ Section INJECTOR. Definition transf_function (f : function) : res function := let injections := PTree.elements (gen_injections f) in let max_pc := max_pc_function f in - if List.forallb (fun injection => (fst injection) <=? max_pc) injections + let max_reg := max_reg_function f in + if List.forallb + (fun injection => + ((fst injection) <=? max_pc) && + (List.forallb + (fun (i : inj_instr) => + (match i with + | INJop _ _ res => res + | INJload _ _ _ res => res + end) <=? max_reg) (snd injection)) + ) injections then OK {| fn_sig := f.(fn_sig); fn_params := f.(fn_params); -- cgit From a779d35bad9faf3bbfc5bf898565256bd40edf33 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 22:17:12 +0200 Subject: lemma on stepping through non trapping instructions --- backend/Inject.v | 28 ++++++++----- backend/Injectproof.v | 106 +++++++++++++++++++++++++++++++++++++++++++++++--- mppa_k1c/Op.v | 11 ++++-- 3 files changed, 126 insertions(+), 19 deletions(-) diff --git a/backend/Inject.v b/backend/Inject.v index 6da10019..6ef32ccb 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -81,20 +81,28 @@ Definition inject prog extra_pc injections : code := Section INJECTOR. Variable gen_injections : function -> PTree.t (list inj_instr). + Definition valid_injection_instr (max_reg : reg) (i : inj_instr) := + match i with + | INJop op args res => (max_reg max_reg + ((fst injection) <=? max_pc) && + (List.forallb (valid_injection_instr max_reg) (snd injection)) + ). + + Definition valid_injections f := + valid_injections1 (max_pc_function f) (max_reg_function f). + Definition transf_function (f : function) : res function := let injections := PTree.elements (gen_injections f) in let max_pc := max_pc_function f in let max_reg := max_reg_function f in - if List.forallb - (fun injection => - ((fst injection) <=? max_pc) && - (List.forallb - (fun (i : inj_instr) => - (match i with - | INJop _ _ res => res - | INJload _ _ _ res => res - end) <=? max_reg) (snd injection)) - ) injections + if valid_injections1 max_pc max_reg injections then OK {| fn_sig := f.(fn_sig); fn_params := f.(fn_params); diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 05c57569..e3c9007b 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1,6 +1,6 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. -Require Import Memory Registers Op RTL Globalenvs Values. +Require Import Memory Registers Op RTL Globalenvs Values Events. Require Import Inject. Require Import Lia. @@ -545,6 +545,11 @@ Section INJECTOR. Definition match_regs (f : function) (rs rs' : regset) := forall r, r <= max_reg_function f -> (rs'#r = rs#r). + + Lemma match_regs_refl : forall f rs, match_regs f rs rs. + Proof. + unfold match_regs. intros. trivial. + Qed. Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := | match_frames_intro: forall res f tf sp pc rs trs @@ -610,7 +615,7 @@ Section INJECTOR. Proof. destruct f; simpl; intros; monadInv H; trivial. unfold transf_function in *. - destruct forallb in EQ. + destruct valid_injections1 in EQ. 2: discriminate. inv EQ. reflexivity. @@ -623,7 +628,7 @@ Section INJECTOR. destruct f. unfold transf_function. intros. - destruct forallb in H. + destruct valid_injections1 in H. 2: discriminate. inv H. reflexivity. @@ -636,7 +641,7 @@ Section INJECTOR. destruct f. unfold transf_function. intros. - destruct forallb in H. + destruct valid_injections1 in H. 2: discriminate. inv H. reflexivity. @@ -649,7 +654,7 @@ Section INJECTOR. destruct f. unfold transf_function. intros. - destruct forallb in H. + destruct valid_injections1 in H. 2: discriminate. inv H. reflexivity. @@ -662,7 +667,7 @@ Section INJECTOR. destruct f. unfold transf_function. intros. - destruct forallb in H. + destruct valid_injections1 in H. 2: discriminate. inv H. reflexivity. @@ -693,5 +698,94 @@ Section INJECTOR. intros. inv H0. inv H. inv STACKS. constructor. Qed. + Lemma assign_above: + forall f trs res v, + (max_reg_function f) < res -> + match_regs f trs trs # res <- v. + Proof. + unfold match_regs. + intros. + apply Regmap.gso. + lia. + Qed. + + Lemma transf_function_inj_step: + forall ts f tf sp pc trs m ii + (FUN : transf_function gen_injections f = OK tf) + (GET : (fn_code tf) ! pc = Some (inject_instr ii (Pos.succ pc))) + (VALID : valid_injection_instr (max_reg_function f) ii = true), + exists trs', + RTL.step ge + (State ts tf sp pc trs m) E0 + (State ts tf sp (Pos.succ pc) trs' m) /\ + match_regs (f : function) trs trs'. + Proof. + destruct ii as [op args res | chunk addr args res]; simpl; intros. + - repeat rewrite andb_true_iff in VALID. + rewrite negb_true_iff in VALID. + destruct VALID as (MAX_REG & NOTRAP & LENGTH). + rewrite Pos.ltb_lt in MAX_REG. + rewrite Nat.eqb_eq in LENGTH. + destruct (eval_operation ge sp op trs ## args m) as [v | ] eqn:EVAL. + + exists (trs # res <- v). + split. + * apply exec_Iop with (op := op) (args := args) (res := res); assumption. + * apply assign_above; auto. + + exfalso. + generalize EVAL. + apply is_trapping_op_sound; trivial. + rewrite map_length. + assumption. + - rewrite Pos.ltb_lt in VALID. + destruct (eval_addressing ge sp addr trs ## args) as [a | ] eqn:ADDR. + + destruct (Mem.loadv chunk m a) as [v | ] eqn:LOAD. + * exists (trs # res <- v). + split. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); assumption. + ** apply assign_above; auto. + * exists (trs # res <- Vundef). + split. + ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); assumption. + ** apply assign_above; auto. + + exists (trs # res <- Vundef). + split. + * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args) (dst := res); assumption. + * apply assign_above; auto. + Qed. + + (* TODO + Lemma transf_function_starstep : + forall ts f tf sp m inj_n src_pc inj_pc inj_code + (FUN : transf_function gen_injections f = OK tf) + (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + Some (src_pc, inj_code)) + (POSITION : inject_l_position (Pos.succ (max_pc_function f)) + (PTree.elements (gen_injections f)) inj_n = inj_pc) + (k : nat) + (CUR : (k <= (List.length inj_code))%nat) + (trs : regset), + exists trs', + match_regs (f : function) trs trs' /\ + Smallstep.star RTL.step ge + (State ts tf sp (pos_add_nat inj_pc + ((List.length inj_code) - k)%nat) trs m) E0 + (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs' m). + Proof. + induction k; simpl; intros. + { rewrite Nat.sub_0_r. + exists trs. + split. + - apply match_regs_refl. + - constructor. + } + assert (k <= Datatypes.length inj_code)%nat as KK by lia. + pose proof (IHk KK) as IH. + clear IHk KK. + assert ( + exists trs'. + split. + assumption. +*) + End PRESERVATION. End INJECTOR. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 92061d04..4caac9e1 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -1045,14 +1045,19 @@ Definition is_trapping_op (op : operation) := | _ => false end. +Definition args_of_operation op := + if eq_operation op Omove + then 1%nat + else List.length (fst (type_of_operation op)). + Lemma is_trapping_op_sound: forall op vl sp m, - op <> Omove -> is_trapping_op op = false -> - (List.length vl) = (List.length (fst (type_of_operation op))) -> + (List.length vl) = args_of_operation op -> eval_operation genv sp op vl m <> None. Proof. - destruct op; intros; simpl in *; try congruence. + unfold args_of_operation. + destruct op; destruct eq_operation; intros; simpl in *; try congruence. all: try (destruct vl as [ | vh1 vl1]; try discriminate). all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). -- cgit From 1ba9cba60f5cf4fe0a2c1d620881cad2383c0027 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 00:34:14 +0200 Subject: one more admit --- backend/Injectproof.v | 92 +++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 85 insertions(+), 7 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index e3c9007b..c3de5e47 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -225,6 +225,19 @@ Fixpoint inject_l_position extra_pc end end. +Lemma inject_l_position_increases : forall injections pc k, + pc <= inject_l_position pc injections k. +Proof. + induction injections; simpl; intros. + lia. + destruct a as [_ l]. + destruct k. + lia. + specialize IHinjections with (pc := (Pos.succ (pos_add_nat pc (Datatypes.length l)))) (k := k). + assert (pc <= (pos_add_nat pc (Datatypes.length l))) by apply pos_add_nat_increases. + lia. +Qed. + Definition inject_l (prog : code) extra_pc injections := List.fold_left (fun already (injection : node * (list inj_instr)) => inject_at' already (fst injection) (snd injection)) @@ -550,6 +563,15 @@ Section INJECTOR. Proof. unfold match_regs. intros. trivial. Qed. + + Lemma match_regs_trans : forall f rs1 rs2 rs3, + match_regs f rs1 rs2 -> match_regs f rs2 rs3 -> match_regs f rs1 rs3. + Proof. + unfold match_regs. intros until rs3. intros M12 M23 r. + specialize M12 with r. + specialize M23 with r. + intuition congruence. + Qed. Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := | match_frames_intro: forall res f tf sp pc rs trs @@ -753,8 +775,7 @@ Section INJECTOR. * apply assign_above; auto. Qed. - (* TODO - Lemma transf_function_starstep : + Lemma transf_function_inj_starstep : forall ts f tf sp m inj_n src_pc inj_pc inj_code (FUN : transf_function gen_injections f = OK tf) (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = @@ -781,11 +802,68 @@ Section INJECTOR. assert (k <= Datatypes.length inj_code)%nat as KK by lia. pose proof (IHk KK) as IH. clear IHk KK. - assert ( - exists trs'. - split. - assumption. -*) + pose proof FUN as VALIDATE. + unfold transf_function, valid_injections1 in VALIDATE. + destruct forallb eqn:FORALL in VALIDATE. + 2: discriminate. + injection VALIDATE. + intro TF. + symmetry in TF. + pose proof (inject_l_injected (PTree.elements (gen_injections f)) (fn_code f) inj_n src_pc inj_code (Pos.succ (max_pc_function f)) ((List.length inj_code) - (S k))%nat) as INJECTED. + lapply INJECTED. + { clear INJECTED. + intro INJECTED. + assert ((Datatypes.length inj_code - S k < + Datatypes.length inj_code)%nat) as LESS by lia. + pose proof (INJECTED INJ LESS) as INJ'. + replace (snd + (inject_l (fn_code f) (Pos.succ (max_pc_function f)) + (PTree.elements (gen_injections f)))) with (fn_code tf) in INJ'. + 2: rewrite TF; simpl; reflexivity. apply transf_function_inj_step with (f:=f) (ts:=ts) (sp:=sp) (trs:=trs) (m := m) in INJ'. + 2: assumption. + { + destruct INJ' as [trs'' [STEP STEPMATCH]]. + destruct (IH trs'') as [trs' [STARSTEPMATCH STARSTEP]]. + exists trs'. + split. + { apply match_regs_trans with (rs2 := trs''); assumption. } + eapply Smallstep.star_step with (t1:=E0) (t2:=E0). + { + rewrite POSITION in STEP. + exact STEP. + } + { + replace (Datatypes.length inj_code - k)%nat + with (S (Datatypes.length inj_code - (S k)))%nat in STARSTEP by lia. + simpl pos_add_nat in STARSTEP. + exact STARSTEP. + } + constructor. + } + rewrite forallb_forall in FORALL. + specialize FORALL with (src_pc, inj_code). + lapply FORALL. + { + simpl. + rewrite andb_true_iff. + intros (SRC & ALL_VALID). + rewrite forallb_forall in ALL_VALID. + apply ALL_VALID. + admit. + } + apply nth_error_In with (n := inj_n). + assumption. + } + rewrite forallb_forall in FORALL. + rewrite forallb_forall. + intros x INx. + rewrite Pos.ltb_lt. + pose proof (FORALL x INx) as ALLx. + rewrite andb_true_iff in ALLx. + destruct ALLx as [ALLx1 ALLx2]. + rewrite Pos.leb_le in ALLx1. + lia. + Admitted. End PRESERVATION. End INJECTOR. -- cgit From 2ebd2eced4437aea823442dd15f160917590cb8a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 00:45:57 +0200 Subject: injector "ghost steps" --- backend/Injectproof.v | 39 +++++++++++++++++++++++++++++++++++---- 1 file changed, 35 insertions(+), 4 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index c3de5e47..dac93d41 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -775,7 +775,17 @@ Section INJECTOR. * apply assign_above; auto. Qed. - Lemma transf_function_inj_starstep : + Lemma bounded_nth_In: forall {T : Type} (l : list T) k LESS, + In (bounded_nth k l LESS) l. + Proof. + induction l; simpl; intros. + lia. + destruct k; simpl. + - left; trivial. + - right. apply IHl. + Qed. + + Lemma transf_function_inj_starstep_rec : forall ts f tf sp m inj_n src_pc inj_pc inj_code (FUN : transf_function gen_injections f = OK tf) (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = @@ -849,7 +859,7 @@ Section INJECTOR. intros (SRC & ALL_VALID). rewrite forallb_forall in ALL_VALID. apply ALL_VALID. - admit. + apply bounded_nth_In. } apply nth_error_In with (n := inj_n). assumption. @@ -863,7 +873,28 @@ Section INJECTOR. destruct ALLx as [ALLx1 ALLx2]. rewrite Pos.leb_le in ALLx1. lia. - Admitted. - + Qed. + + Lemma transf_function_inj_starstep : + forall ts f tf sp m inj_n src_pc inj_pc inj_code + (FUN : transf_function gen_injections f = OK tf) + (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + Some (src_pc, inj_code)) + (POSITION : inject_l_position (Pos.succ (max_pc_function f)) + (PTree.elements (gen_injections f)) inj_n = inj_pc) + (trs : regset), + exists trs', + match_regs (f : function) trs trs' /\ + Smallstep.star RTL.step ge + (State ts tf sp inj_pc trs m) E0 + (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs' m). + Proof. + intros. + replace (State ts tf sp inj_pc trs m) with (State ts tf sp (pos_add_nat inj_pc ((List.length inj_code) - (List.length inj_code))%nat) trs m). + eapply transf_function_inj_starstep_rec; eauto. + f_equal. + rewrite <- minus_n_n. + reflexivity. + Qed. End PRESERVATION. End INJECTOR. -- cgit From 63e2afe7ee5507a724bed691ad76fad635754882 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 11:13:38 +0200 Subject: transf_function_inj_end --- backend/Injectproof.v | 57 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index dac93d41..c3382d72 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -896,5 +896,62 @@ Section INJECTOR. rewrite <- minus_n_n. reflexivity. Qed. + + Lemma transf_function_inj_end : + forall ts f tf sp m inj_n src_pc inj_pc inj_code i + (FUN : transf_function gen_injections f = OK tf) + (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + Some (src_pc, inj_code)) + (SRC: (fn_code f) ! src_pc = Some i) + (POSITION : inject_l_position (Pos.succ (max_pc_function f)) + (PTree.elements (gen_injections f)) inj_n = inj_pc) + (trs : regset), + RTL.step ge + (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs m) E0 + (State ts tf sp (successor i) trs m). + Proof. + intros. + pose proof FUN as VALIDATE. + unfold transf_function, valid_injections1 in VALIDATE. + destruct forallb eqn:FORALL in VALIDATE. + 2: discriminate. + injection VALIDATE. + intro TF. + symmetry in TF. + Check inject_l_injected_end. + pose proof (inject_l_injected_end (PTree.elements (gen_injections f)) (fn_code f) inj_n src_pc i inj_code (Pos.succ (max_pc_function f))) as INJECTED. + lapply INJECTED. + 2: assumption. + clear INJECTED. + intro INJECTED. + lapply INJECTED. + 2: apply (PTree.elements_keys_norepet (gen_injections f)); fail. + clear INJECTED. + intro INJECTED. + lapply INJECTED. + { clear INJECTED. + intro INJECTED. + pose proof (INJECTED INJ) as INJ'. + clear INJECTED. + replace (snd + (inject_l (fn_code f) (Pos.succ (max_pc_function f)) + (PTree.elements (gen_injections f)))) with (fn_code tf) in INJ'. + 2: rewrite TF; simpl; reflexivity. + rewrite POSITION in INJ'. + apply exec_Inop. + assumption. + } + clear INJECTED. + rewrite forallb_forall in FORALL. + rewrite forallb_forall. + intros x INx. + rewrite Pos.ltb_lt. + pose proof (FORALL x INx) as ALLx. + rewrite andb_true_iff in ALLx. + destruct ALLx as [ALLx1 ALLx2]. + rewrite Pos.leb_le in ALLx1. + lia. + Qed. + End PRESERVATION. End INJECTOR. -- cgit From 764b167efe9edb3d0d20e8ea37263320c42f3036 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 11:22:56 +0200 Subject: transf_function_inj_plusstep --- backend/Injectproof.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index c3382d72..51d049b1 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -953,5 +953,30 @@ Section INJECTOR. lia. Qed. + Lemma transf_function_inj_plusstep : + forall ts f tf sp m inj_n src_pc inj_pc inj_code i + (FUN : transf_function gen_injections f = OK tf) + (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + Some (src_pc, inj_code)) + (SRC: (fn_code f) ! src_pc = Some i) + (POSITION : inject_l_position (Pos.succ (max_pc_function f)) + (PTree.elements (gen_injections f)) inj_n = inj_pc) + (trs : regset), + exists trs', + match_regs (f : function) trs trs' /\ + Smallstep.plus RTL.step ge + (State ts tf sp inj_pc trs m) E0 + (State ts tf sp (successor i) trs' m). + Proof. + intros. + destruct (transf_function_inj_starstep ts f tf sp m inj_n src_pc inj_pc inj_code FUN INJ POSITION trs) as [trs' [MATCH PLUS]]. + exists trs'. + split. assumption. + eapply Smallstep.plus_right. + exact PLUS. + eapply transf_function_inj_end; eassumption. + reflexivity. + Qed. + End PRESERVATION. End INJECTOR. -- cgit From 7de591569308917c9ffcd4626c94872e390811a2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 11:49:21 +0200 Subject: INJnop --- backend/Inject.v | 3 +++ backend/Injectproof.v | 6 +++++- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/backend/Inject.v b/backend/Inject.v index 6ef32ccb..57aa343b 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -5,11 +5,13 @@ Require Import Memory Registers Op RTL. Local Open Scope positive. Inductive inj_instr : Type := + | INJnop | INJop: operation -> list reg -> reg -> inj_instr | INJload: memory_chunk -> addressing -> list reg -> reg -> inj_instr. Definition inject_instr (i : inj_instr) (pc' : node) : instruction := match i with + | INJnop => Inop pc' | INJop op args dst => Iop op args dst pc' | INJload chunk addr args dst => Iload NOTRAP chunk addr args dst pc' end. @@ -83,6 +85,7 @@ Section INJECTOR. Definition valid_injection_instr (max_reg : reg) (i : inj_instr) := match i with + | INJnop => true | INJop op args res => (max_reg max_reg Date: Tue, 31 Mar 2020 12:54:59 +0200 Subject: transf_function_redirects --- backend/Injectproof.v | 109 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 109 insertions(+) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 7ce401cb..de60a4d6 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -981,6 +981,115 @@ Section INJECTOR. eapply transf_function_inj_end; eassumption. reflexivity. Qed. + + Lemma transf_function_preserves: + forall f tf pc + (FUN : transf_function gen_injections f = OK tf) + (LESS : pc <= max_pc_function f) + (NOCHANGE : (gen_injections f) ! pc = None), + (fn_code tf) ! pc = (fn_code f) ! pc. + Proof. + intros. + unfold transf_function in FUN. + destruct valid_injections1 in FUN. + 2: discriminate. + inv FUN. + simpl. + apply inject_l_preserves. + lia. + rewrite forallb_forall. + intros x INx. + destruct peq; trivial. + subst pc. + exfalso. + destruct x as [pc ii]. + simpl in *. + apply PTree.elements_complete in INx. + congruence. + Qed. + + Lemma transf_function_redirects: + forall f tf pc injl ii + (FUN : transf_function gen_injections f = OK tf) + (LESS : pc <= max_pc_function f) + (INJECTION : (gen_injections f) ! pc = Some injl) + (INSTR: (fn_code f) ! pc = Some ii), + exists pc' : node, + (fn_code tf) ! pc = Some (alter_successor ii pc') /\ + (forall ts sp m trs, + exists trs', + match_regs f trs trs' /\ + Smallstep.plus RTL.step ge + (State ts tf sp pc' trs m) E0 + (State ts tf sp (successor ii) trs' m)). + Proof. + intros. + apply PTree.elements_correct in INJECTION. + apply In_nth_error in INJECTION. + destruct INJECTION as [injn INJECTION]. + exists (inject_l_position (Pos.succ (max_pc_function f)) + (PTree.elements (gen_injections f)) injn). + split. + { unfold transf_function in FUN. + destruct (valid_injections1) eqn:VALID in FUN. + 2: discriminate. + inv FUN. + simpl. + apply inject_l_redirects with (l := injl); auto. + apply PTree.elements_keys_norepet. + unfold valid_injections1 in VALID. + rewrite forallb_forall in VALID. + rewrite forallb_forall. + intros x INx. + pose proof (VALID x INx) as VALIDx. + clear VALID. + rewrite andb_true_iff in VALIDx. + rewrite Pos.leb_le in VALIDx. + destruct VALIDx as [VALIDx1 VALIDx2]. + rewrite Pos.ltb_lt. + lia. + } + intros. + pose proof (transf_function_inj_plusstep ts f tf sp m injn pc + (inject_l_position (Pos.succ (max_pc_function f)) + (PTree.elements (gen_injections f)) injn) + injl ii FUN INJECTION INSTR) as TRANS. + lapply TRANS. + 2: reflexivity. + clear TRANS. + intro TRANS. + exact (TRANS trs). + Qed. + + Theorem transf_step_correct: + forall s1 t s2, step ge s1 t s2 -> + forall ts1 (MS: match_states s1 ts1), + exists ts2, Smallstep.plus step tge ts1 t ts2 /\ match_states s2 ts2. + Proof. + induction 1; intros ts1 MS; inv MS; try (inv TRC). + - (* nop *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + econstructor; split. + * eapply Smallstep.plus_left. + ** apply exec_Inop. + ** + + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Inop. + rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + * constructor; trivial. + Admitted. + Theorem transf_program_correct: + Smallstep.forward_simulation (semantics prog) (semantics tprog). + Proof. + eapply Smallstep.forward_simulation_plus. + apply senv_preserved. + eexact transf_initial_states. + eexact transf_final_states. + eexact transf_step_correct. + Qed. + End PRESERVATION. End INJECTOR. -- cgit From 4e3a12b9d9811b7da429cb2fd0b0c986582093a2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 14:10:22 +0200 Subject: lots of admits to be filled --- backend/Injectproof.v | 147 +++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 134 insertions(+), 13 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index de60a4d6..3ed9c8b7 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -737,7 +737,7 @@ Section INJECTOR. (GET : (fn_code tf) ! pc = Some (inject_instr ii (Pos.succ pc))) (VALID : valid_injection_instr (max_reg_function f) ii = true), exists trs', - RTL.step ge + RTL.step tge (State ts tf sp pc trs m) E0 (State ts tf sp (Pos.succ pc) trs' m) /\ match_regs (f : function) trs trs'. @@ -755,7 +755,10 @@ Section INJECTOR. destruct (eval_operation ge sp op trs ## args m) as [v | ] eqn:EVAL. + exists (trs # res <- v). split. - * apply exec_Iop with (op := op) (args := args) (res := res); assumption. + * apply exec_Iop with (op := op) (args := args) (res := res); trivial. + rewrite eval_operation_preserved with (ge1 := ge). + assumption. + exact symbols_preserved. * apply assign_above; auto. + exfalso. generalize EVAL. @@ -767,15 +770,24 @@ Section INJECTOR. + destruct (Mem.loadv chunk m a) as [v | ] eqn:LOAD. * exists (trs # res <- v). split. - ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); assumption. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial. + rewrite eval_addressing_preserved with (ge1 := ge). + assumption. + exact symbols_preserved. ** apply assign_above; auto. * exists (trs # res <- Vundef). split. - ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); assumption. + ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial. + rewrite eval_addressing_preserved with (ge1 := ge). + assumption. + exact symbols_preserved. ** apply assign_above; auto. + exists (trs # res <- Vundef). split. - * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args) (dst := res); assumption. + * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial. + rewrite eval_addressing_preserved with (ge1 := ge). + assumption. + exact symbols_preserved. * apply assign_above; auto. Qed. @@ -801,7 +813,7 @@ Section INJECTOR. (trs : regset), exists trs', match_regs (f : function) trs trs' /\ - Smallstep.star RTL.step ge + Smallstep.star RTL.step tge (State ts tf sp (pos_add_nat inj_pc ((List.length inj_code) - k)%nat) trs m) E0 (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs' m). @@ -889,7 +901,7 @@ Section INJECTOR. (trs : regset), exists trs', match_regs (f : function) trs trs' /\ - Smallstep.star RTL.step ge + Smallstep.star RTL.step tge (State ts tf sp inj_pc trs m) E0 (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs' m). Proof. @@ -910,7 +922,7 @@ Section INJECTOR. (POSITION : inject_l_position (Pos.succ (max_pc_function f)) (PTree.elements (gen_injections f)) inj_n = inj_pc) (trs : regset), - RTL.step ge + RTL.step tge (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs m) E0 (State ts tf sp (successor i) trs m). Proof. @@ -968,7 +980,7 @@ Section INJECTOR. (trs : regset), exists trs', match_regs (f : function) trs trs' /\ - Smallstep.plus RTL.step ge + Smallstep.plus RTL.step tge (State ts tf sp inj_pc trs m) E0 (State ts tf sp (successor i) trs' m). Proof. @@ -1019,7 +1031,7 @@ Section INJECTOR. (forall ts sp m trs, exists trs', match_regs f trs trs' /\ - Smallstep.plus RTL.step ge + Smallstep.plus RTL.step tge (State ts tf sp pc' trs m) E0 (State ts tf sp (successor ii) trs' m)). Proof. @@ -1060,7 +1072,50 @@ Section INJECTOR. intro TRANS. exact (TRANS trs). Qed. - + + Lemma transf_function_preserves_uses: + forall f tf pc rs trs ii + (FUN : transf_function gen_injections f = OK tf) + (MATCH : match_regs f rs trs) + (INSTR : (fn_code f) ! pc = Some ii), + trs ## (instr_uses ii) = rs ## (instr_uses ii). + Proof. + intros. + assert (forall r, In r (instr_uses ii) -> + trs # r = rs # r) as SAME. + { + intros r INr. + apply MATCH. + apply (max_reg_function_use f pc ii); auto. + } + induction (instr_uses ii); simpl; trivial. + f_equal. + - apply SAME. constructor; trivial. + - apply IHl. intros. + apply SAME. right. assumption. + Qed. + + Lemma match_regs_write: + forall f rs trs res v + (MATCH : match_regs f rs trs), + match_regs f (rs # res <- v) (trs # res <- v). + Proof. + intros. + intros r LESS. + destruct (peq r res). + { + subst r. + rewrite Regmap.gss. + symmetry. + apply Regmap.gss. + } + rewrite Regmap.gso. + rewrite Regmap.gso. + all: trivial. + apply MATCH. + trivial. + Qed. + Theorem transf_step_correct: forall s1 t s2, step ge s1 t s2 -> forall ts1 (MS: match_states s1 ts1), @@ -1069,16 +1124,82 @@ Section INJECTOR. induction 1; intros ts1 MS; inv MS; try (inv TRC). - (* nop *) destruct ((gen_injections f) ! pc) eqn:INJECTION. - + econstructor; split. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) (trs := trs). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. * eapply Smallstep.plus_left. ** apply exec_Inop. - ** + exact ALTER. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + * constructor; trivial. + apply match_regs_trans with (rs2 := trs); assumption. + econstructor; split. * apply Smallstep.plus_one. apply exec_Inop. rewrite transf_function_preserves with (f:=f); eauto. eapply max_pc_function_sound; eauto. * constructor; trivial. + - (* op *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) + (trs := trs # res <- v). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * eapply Smallstep.plus_left. + ** apply exec_Iop with (op := op) (args := args). + exact ALTER. + rewrite eval_operation_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iop op args res pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. + eassumption. + } + exact symbols_preserved. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + * constructor; trivial. + apply match_regs_trans with (rs2 := trs # res <- v); trivial. + apply match_regs_write. + assumption. + + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Iop with (op := op) (args := args). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** rewrite eval_operation_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iop op args res pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. + eassumption. + } + exact symbols_preserved. + * constructor; trivial. + apply match_regs_write. + assumption. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. + - admit. Admitted. Theorem transf_program_correct: -- cgit From 3d4acdb480ff33e09ad4a96548548f7876c4e78e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 14:21:05 +0200 Subject: loads --- backend/Injectproof.v | 129 ++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 126 insertions(+), 3 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 3ed9c8b7..36d3341c 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1144,6 +1144,7 @@ Section INJECTOR. rewrite transf_function_preserves with (f:=f); eauto. eapply max_pc_function_sound; eauto. * constructor; trivial. + - (* op *) destruct ((gen_injections f) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. @@ -1187,9 +1188,131 @@ Section INJECTOR. * constructor; trivial. apply match_regs_write. assumption. - - admit. - - admit. - - admit. + + - (* load *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) + (trs := trs # dst <- v). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * eapply Smallstep.plus_left. + ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args) (a := a). + exact ALTER. + rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + eassumption. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + * constructor; trivial. + apply match_regs_trans with (rs2 := trs # dst <- v); trivial. + apply match_regs_write. + assumption. + + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args) (a := a). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + ** eassumption. + * constructor; trivial. + apply match_regs_write. + assumption. + + - (* load notrap1 *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) + (trs := trs # dst <- Vundef). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * eapply Smallstep.plus_left. + ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args). + exact ALTER. + rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + * constructor; trivial. + apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial. + apply match_regs_write. + assumption. + + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + * constructor; trivial. + apply match_regs_write. + assumption. + + - (* load notrap2 *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) + (trs := trs # dst <- Vundef). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * eapply Smallstep.plus_left. + ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (a := a). + exact ALTER. + rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + eassumption. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + * constructor; trivial. + apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial. + apply match_regs_write. + assumption. + + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (a := a). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + ** eassumption. + * constructor; trivial. + apply match_regs_write. + assumption. + - admit. - admit. - admit. -- cgit From 468b01d591a4fb03c7660c8cda1953414bc9b8bc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 14:30:58 +0200 Subject: store --- backend/Injectproof.v | 43 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 36d3341c..b2ea2562 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1313,7 +1313,48 @@ Section INJECTOR. apply match_regs_write. assumption. - - admit. + - (* store *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m') (trs := trs). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * eapply Smallstep.plus_left. + ** apply exec_Istore with (chunk := chunk) (addr := addr) (args := args) (a := a) (src := src). + exact ALTER. + rewrite eval_addressing_preserved with (ge1 := ge). + { + replace (trs ## args) with (tl (trs ## (instr_uses (Istore chunk addr args src pc')))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + replace (trs # src) with (hd Vundef (trs ## (instr_uses (Istore chunk addr args src pc')))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. + eassumption. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + * constructor; trivial. + apply match_regs_trans with (rs2 := trs); trivial. + + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Istore with (chunk := chunk) (addr := addr) (args := args) (a := a) (src := src). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** rewrite eval_addressing_preserved with (ge1 := ge). + { + replace (trs ## args) with (tl (trs ## (instr_uses (Istore chunk addr args src pc')))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + ** replace (trs # src) with (hd Vundef (trs ## (instr_uses (Istore chunk addr args src pc')))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. + eassumption. + * constructor; trivial. - admit. - admit. - admit. -- cgit From d05a507e17762e5a0887b868ad2f904c08634c06 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 15:31:48 +0200 Subject: call (could not handle it) --- backend/Injectproof.v | 63 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 62 insertions(+), 1 deletion(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index b2ea2562..a895355d 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1115,6 +1115,25 @@ Section INJECTOR. apply MATCH. trivial. Qed. + + Lemma transf_function_preserves_ros: + forall f tf pc rs trs ros args res fd pc' sig + (FUN : transf_function gen_injections f = OK tf) + (MATCH : match_regs f rs trs) + (INSTR : (fn_code f) ! pc = Some (Icall sig ros args res pc')) + (FIND : find_function ge ros rs = Some fd), + exists tfd, find_function tge ros trs = Some tfd + /\ transf_fundef gen_injections fd = OK tfd. + Proof. + intros; destruct ros as [r|id]. + - apply functions_translated; auto. + replace (trs # r) with (hd Vundef (trs ## (instr_uses (Icall sig (inl r) args res pc')))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + - simpl. rewrite symbols_preserved. + simpl in FIND. + destruct (Genv.find_symbol ge id); try congruence. + eapply function_ptr_translated; eauto. + Qed. Theorem transf_step_correct: forall s1 t s2, step ge s1 t s2 -> @@ -1355,7 +1374,49 @@ Section INJECTOR. simpl. eassumption. * constructor; trivial. - - admit. + - (* call *) + destruct (transf_function_preserves_ros f tf pc rs trs ros args res fd pc' (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]]. + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + simpl in ALTER. + econstructor; split. + * eapply Smallstep.plus_one. + apply exec_Icall with (args := args) (sig := (funsig fd)) (ros := ros). + exact ALTER. + exact TFD1. + apply sig_preserved; auto. + * destruct ros as [r | id]. + ** replace (trs ## args) with (tl (trs ## (instr_uses (Icall (funsig fd) (inl r) args res pc')))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + apply match_states_call; auto. + constructor; auto. + constructor; auto. + ** replace (trs ## args) with (trs ## (instr_uses (Icall (funsig fd) (inr id) args res pc'))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + apply match_states_call; auto. + constructor; auto. + constructor; auto. + + econstructor; split. + * eapply Smallstep.plus_one. + apply exec_Icall with (args := args) (sig := (funsig fd)) (ros := ros). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** exact TFD1. + ** apply sig_preserved; auto. + * destruct ros as [r | id]. + ** replace (trs ## args) with (tl (trs ## (instr_uses (Icall (funsig fd) (inl r) args res pc')))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + apply match_states_call; auto. + constructor; auto. + constructor; auto. + ** replace (trs ## args) with (trs ## (instr_uses (Icall (funsig fd) (inr id) args res pc'))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + apply match_states_call; auto. + constructor; auto. + constructor; auto. + - admit. - admit. - admit. -- cgit From 52864f86e9504896df8ff543c9f352f268ef1ae4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 15:52:35 +0200 Subject: tailcall --- backend/Injectproof.v | 59 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 58 insertions(+), 1 deletion(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index a895355d..6513a8d0 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1134,6 +1134,25 @@ Section INJECTOR. destruct (Genv.find_symbol ge id); try congruence. eapply function_ptr_translated; eauto. Qed. + + Lemma transf_function_preserves_ros_tail: + forall f tf pc rs trs ros args fd sig + (FUN : transf_function gen_injections f = OK tf) + (MATCH : match_regs f rs trs) + (INSTR : (fn_code f) ! pc = Some (Itailcall sig ros args)) + (FIND : find_function ge ros rs = Some fd), + exists tfd, find_function tge ros trs = Some tfd + /\ transf_fundef gen_injections fd = OK tfd. + Proof. + intros; destruct ros as [r|id]. + - apply functions_translated; auto. + replace (trs # r) with (hd Vundef (trs ## (instr_uses (Itailcall sig (inl r) args)))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + - simpl. rewrite symbols_preserved. + simpl in FIND. + destruct (Genv.find_symbol ge id); try congruence. + eapply function_ptr_translated; eauto. + Qed. Theorem transf_step_correct: forall s1 t s2, step ge s1 t s2 -> @@ -1417,7 +1436,45 @@ Section INJECTOR. constructor; auto. constructor; auto. - - admit. + - (* tailcall *) + destruct (transf_function_preserves_ros_tail f tf pc rs trs ros args fd (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]]. + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + simpl in ALTER. + econstructor; split. + * eapply Smallstep.plus_one. + apply exec_Itailcall with (args := args) (sig := (funsig fd)) (ros := ros). + exact ALTER. + exact TFD1. + apply sig_preserved; auto. + rewrite stacksize_preserved with (f:=f) by trivial. + eassumption. + * destruct ros as [r | id]. + ** replace (trs ## args) with (tl (trs ## (instr_uses (Itailcall (funsig fd) (inl r) args)))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + apply match_states_call; auto. + ** replace (trs ## args) with (trs ## (instr_uses (Itailcall (funsig fd) (inr id) args))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + apply match_states_call; auto. + + econstructor; split. + * eapply Smallstep.plus_one. + apply exec_Itailcall with (args := args) (sig := (funsig fd)) (ros := ros). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** exact TFD1. + ** apply sig_preserved; auto. + ** rewrite stacksize_preserved with (f:=f) by trivial. + eassumption. + * destruct ros as [r | id]. + ** replace (trs ## args) with (tl (trs ## (instr_uses (Itailcall (funsig fd) (inl r) args)))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + apply match_states_call; auto. + ** replace (trs ## args) with (trs ## (instr_uses (Itailcall (funsig fd) (inr id) args))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + apply match_states_call; auto. + - admit. - admit. - admit. -- cgit From ba1c4372b984293ca75a524eb0e532d354377ade Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 16:11:45 +0200 Subject: builtin (incomplete) --- backend/Injectproof.v | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 6513a8d0..306e855b 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1475,6 +1475,39 @@ Section INJECTOR. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. apply match_states_call; auto. + - (* builtin *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m') + (trs := (regmap_setres res vres trs)). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * eapply Smallstep.plus_left. + ** apply exec_Ibuiltin with (ef := ef) (args := args) (res := res) (vargs := vargs). + *** exact ALTER. + *** apply eval_builtin_args_preserved with (ge1 := ge); eauto. + exact symbols_preserved. + admit. + *** eapply external_call_symbols_preserved; eauto. apply senv_preserved. + ** apply Smallstep.plus_star. + exact PLUS. + ** symmetry. apply E0_right. + * constructor; trivial. + apply match_regs_trans with (rs2 := (regmap_setres res vres trs)); trivial. + admit. + + econstructor; split. + * eapply Smallstep.plus_one. + apply exec_Ibuiltin with (ef := ef) (args := args) (res := res) (vargs := vargs). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** apply eval_builtin_args_preserved with (ge1 := ge); eauto. + exact symbols_preserved. + admit. + ** eapply external_call_symbols_preserved; eauto. apply senv_preserved. + * admit. + - admit. - admit. - admit. -- cgit From e55776fd96f78518da49dfa9e856c3e070353fc9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 16:25:41 +0200 Subject: cond --- backend/Injectproof.v | 56 +++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 54 insertions(+), 2 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 306e855b..11472c0e 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1508,8 +1508,60 @@ Section INJECTOR. ** eapply external_call_symbols_preserved; eauto. apply senv_preserved. * admit. - - admit. - - admit. + - (* cond *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + destruct b eqn:B. + ++ exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) (trs := trs). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * eapply Smallstep.plus_left. + ** apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot). + exact ALTER. + replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. reflexivity. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + * simpl. constructor; auto. + apply match_regs_trans with (rs2:=trs); auto. + + ++ exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) (trs := trs). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * eapply Smallstep.plus_one. + apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot). + exact ALTER. + replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. reflexivity. + * simpl. constructor; auto. + + destruct b eqn:B. + * econstructor; split. + ** eapply Smallstep.plus_one. + apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot). + *** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + *** replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + *** reflexivity. + ** constructor; auto. + * econstructor; split. + ** eapply Smallstep.plus_one. + apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot). + *** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + *** replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + *** reflexivity. + ** constructor; auto. + - admit. - admit. - admit. -- cgit From e52663259c93ee91a74c57df9ff554d799d42320 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 16:40:52 +0200 Subject: jumptable --- backend/Injectproof.v | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 11472c0e..7576fb30 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1562,7 +1562,28 @@ Section INJECTOR. *** reflexivity. ** constructor; auto. - - admit. + - destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) (trs := trs). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Ijumptable with (arg := arg) (tbl := tbl) (n := n); trivial. + replace (trs # arg) with (hd Vundef (trs ## (instr_uses (Ijumptable arg tbl)))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + eassumption. + * constructor; trivial. + + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Ijumptable with (arg := arg) (tbl := tbl) (n := n); trivial. + rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + replace (trs # arg) with (hd Vundef (trs ## (instr_uses (Ijumptable arg tbl)))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + eassumption. + * constructor; trivial. - admit. - admit. - admit. -- cgit From 501d6501b9de645843cfa1e1408ba3fe9318223f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 16:51:36 +0200 Subject: return --- backend/Injectproof.v | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 7576fb30..013bc247 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1584,7 +1584,35 @@ Section INJECTOR. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. eassumption. * constructor; trivial. - - admit. + - (* return *) + destruct ((gen_injections f) ! pc) eqn:INJECTION. + + exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := (Vptr stk Ptrofs.zero)) (m := m) (trs := trs). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Ireturn. + exact ALTER. + rewrite stacksize_preserved with (f:=f); eassumption. + * destruct or as [r | ]; simpl. + ** replace (trs # r) with (hd Vundef (trs ## (instr_uses (Ireturn (Some r))))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + constructor; auto. + ** constructor; auto. + + econstructor; split. + * apply Smallstep.plus_one. + apply exec_Ireturn. + rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + rewrite stacksize_preserved with (f:=f); eassumption. + * destruct or as [r | ]; simpl. + ** replace (trs # r) with (hd Vundef (trs ## (instr_uses (Ireturn (Some r))))) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + constructor; auto. + ** constructor; auto. + - admit. - admit. - admit. -- cgit From ee6b5b9e5445f64b26776cf16c2b9cef60b84574 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 17:03:24 +0200 Subject: internal call --- backend/Injectproof.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 013bc247..40c39b89 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1613,7 +1613,17 @@ Section INJECTOR. constructor; auto. ** constructor; auto. - - admit. + - (* internal call *) + monadInv FUN. + econstructor; split. + + apply Smallstep.plus_one. + apply exec_function_internal. + rewrite stacksize_preserved with (f:=f) by assumption. + eassumption. + + rewrite entrypoint_preserved with (f:=f)(tf:=x) by assumption. + constructor; auto. + rewrite params_preserved with (f:=f)(tf:=x) by assumption. + apply match_regs_refl. - admit. - admit. Admitted. -- cgit From 7c18e5fbe3dee48b6a7f38d19cbb19427e6722fd Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 17:07:23 +0200 Subject: external call --- backend/Injectproof.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 40c39b89..c9493baf 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1624,7 +1624,14 @@ Section INJECTOR. constructor; auto. rewrite params_preserved with (f:=f)(tf:=x) by assumption. apply match_regs_refl. - - admit. + - (* external call *) + monadInv FUN. + econstructor; split. + + apply Smallstep.plus_one. + apply exec_function_external. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor; auto. + - admit. Admitted. -- cgit From cc2d5def041128ae6dcbf46455db3341e74e995c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 17:12:42 +0200 Subject: except for builtins, finished the proof --- backend/Inject.v | 2 +- backend/Injectproof.v | 10 ++++++++-- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/backend/Inject.v b/backend/Inject.v index 57aa343b..1a8ec24a 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -46,9 +46,9 @@ Definition alter_successor (i : instruction) (pc' : node) : instruction := | Iop op args dst _ => Iop op args dst pc' | Iload trap chunk addr args dst _ => Iload trap chunk addr args dst pc' | Istore chunk addr args src _ => Istore chunk addr args src pc' - | Icall sig ri args dst _ => Icall sig ri args dst pc' | Ibuiltin ef args res _ => Ibuiltin ef args res pc' | Icond cond args _ pc2 => Icond cond args pc' pc2 + | Icall _ _ _ _ _ | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => i diff --git a/backend/Injectproof.v b/backend/Injectproof.v index c9493baf..2bfd9701 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -934,7 +934,6 @@ Section INJECTOR. injection VALIDATE. intro TF. symmetry in TF. - Check inject_l_injected_end. pose proof (inject_l_injected_end (PTree.elements (gen_injections f)) (fn_code f) inj_n src_pc i inj_code (Pos.succ (max_pc_function f))) as INJECTED. lapply INJECTED. 2: assumption. @@ -1632,7 +1631,14 @@ Section INJECTOR. eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. - - admit. + - (* return *) + inv STACKS. inv H1. + econstructor; split. + + apply Smallstep.plus_one. + apply exec_return. + + constructor; trivial. + apply match_regs_write. + assumption. Admitted. Theorem transf_program_correct: -- cgit From 031b1525ad7f27fa67f48ae83b101b5c2b969af7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 18:56:17 +0200 Subject: more about builtin args --- backend/Injectproof.v | 84 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 83 insertions(+), 1 deletion(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 2bfd9701..93cbdc10 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1094,6 +1094,87 @@ Section INJECTOR. apply SAME. right. assumption. Qed. + (* + Lemma transf_function_preserves_builtin_arg: + forall rs trs ef res sp m pc' + (arg : builtin_arg reg) + (SAME : (forall r, + In r (instr_uses (Ibuiltin ef args res pc')) -> + trs # r = rs # r) ) + varg + (EVAL : eval_builtin_arg ge (fun r => rs#r) sp m arg varg), + eval_builtin_arg ge (fun r => trs#r) sp m arg varg. + Proof. + *) + + Lemma transf_function_preserves_builtin_args_rec: + forall rs trs ef res sp m pc' + (args : list (builtin_arg reg)) + (SAME : (forall r, + In r (instr_uses (Ibuiltin ef args res pc')) -> + trs # r = rs # r) ) + (vargs : list val) + (EVAL : eval_builtin_args ge (fun r => rs#r) sp m args vargs), + eval_builtin_args ge (fun r => trs#r) sp m args vargs. + Proof. + unfold eval_builtin_args. + induction args; intros; inv EVAL. + - constructor. + - constructor. + + induction H1. + all: try (constructor; auto; fail). + * rewrite <- SAME. + apply eval_BA. + simpl. + left. reflexivity. + * constructor. + ** apply IHeval_builtin_arg1. + intros r INr. + apply SAME. + simpl. + simpl in INr. + rewrite in_app in INr. + rewrite in_app. + rewrite in_app. + tauto. + ** apply IHeval_builtin_arg2. + intros r INr. + apply SAME. + simpl. + simpl in INr. + rewrite in_app in INr. + rewrite in_app. + rewrite in_app. + tauto. + * constructor. + ** apply IHeval_builtin_arg1. + intros r INr. + apply SAME. + simpl. + simpl in INr. + rewrite in_app in INr. + rewrite in_app. + rewrite in_app. + tauto. + ** apply IHeval_builtin_arg2. + intros r INr. + apply SAME. + simpl. + simpl in INr. + rewrite in_app in INr. + rewrite in_app. + rewrite in_app. + tauto. + + apply IHargs. + 2: assumption. + intros r INr. + apply SAME. + simpl. + apply in_or_app. + right. + exact INr. + Qed. + Lemma match_regs_write: forall f rs trs res v (MATCH : match_regs f rs trs), @@ -1488,7 +1569,8 @@ Section INJECTOR. *** exact ALTER. *** apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - admit. + Compute (instr_uses (Ibuiltin ef args res pc')). + (instr_uses *** eapply external_call_symbols_preserved; eauto. apply senv_preserved. ** apply Smallstep.plus_star. exact PLUS. -- cgit From e4c053f3ddfb8fbea125ba5100293e013900d0b1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 19:02:02 +0200 Subject: resolved an "admit" --- backend/Injectproof.v | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 93cbdc10..0a53dc9f 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1174,7 +1174,25 @@ Section INJECTOR. right. exact INr. Qed. - + + Lemma transf_function_preserves_builtin_args: + forall f tf pc rs trs ef res sp m pc' + (args : list (builtin_arg reg)) + (FUN : transf_function gen_injections f = OK tf) + (MATCH : match_regs f rs trs) + (INSTR : (fn_code f) ! pc = Some (Ibuiltin ef args res pc')) + (vargs : list val) + (EVAL : eval_builtin_args ge (fun r => rs#r) sp m args vargs), + eval_builtin_args ge (fun r => trs#r) sp m args vargs. + Proof. + intros. + apply transf_function_preserves_builtin_args_rec with (rs := rs) (ef := ef) (res := res) (pc' := pc'). + intros r INr. + apply MATCH. + apply (max_reg_function_use f pc (Ibuiltin ef args res pc')). + all: auto. + Qed. + Lemma match_regs_write: forall f rs trs res v (MATCH : match_regs f rs trs), @@ -1569,8 +1587,7 @@ Section INJECTOR. *** exact ALTER. *** apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - Compute (instr_uses (Ibuiltin ef args res pc')). - (instr_uses + apply transf_function_preserves_builtin_args with (f:=f) (tf:=tf) (pc:=pc) (rs:=rs) (ef:=ef) (res0:=res) (pc':=pc'); auto. *** eapply external_call_symbols_preserved; eauto. apply senv_preserved. ** apply Smallstep.plus_star. exact PLUS. -- cgit From 3d87236deffbcbfd8d56a9080482071602f9ea01 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 19:05:03 +0200 Subject: fewer admits --- backend/Injectproof.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 0a53dc9f..7ba4b9f7 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1214,6 +1214,15 @@ Section INJECTOR. trivial. Qed. + Lemma match_regs_setres: + forall f res rs trs vres + (MATCH : match_regs f rs trs), + match_regs f (regmap_setres res vres rs) (regmap_setres res vres trs). + Proof. + induction res; simpl; intros; trivial. + apply match_regs_write; auto. + Qed. + Lemma transf_function_preserves_ros: forall f tf pc rs trs ros args res fd pc' sig (FUN : transf_function gen_injections f = OK tf) @@ -1594,7 +1603,8 @@ Section INJECTOR. ** symmetry. apply E0_right. * constructor; trivial. apply match_regs_trans with (rs2 := (regmap_setres res vres trs)); trivial. - admit. + apply match_regs_setres. + assumption. + econstructor; split. * eapply Smallstep.plus_one. apply exec_Ibuiltin with (ef := ef) (args := args) (res := res) (vargs := vargs). -- cgit From 7893d5ece9a06d2ec09eb0a9c1e5207a15668723 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 31 Mar 2020 19:06:42 +0200 Subject: no more admitted --- backend/Injectproof.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 7ba4b9f7..b63f9498 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1612,9 +1612,11 @@ Section INJECTOR. eapply max_pc_function_sound; eauto. ** apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - admit. + apply transf_function_preserves_builtin_args with (f:=f) (tf:=tf) (pc:=pc) (rs:=rs) (ef:=ef) (res0:=res) (pc':=pc'); auto. ** eapply external_call_symbols_preserved; eauto. apply senv_preserved. - * admit. + * constructor; auto. + apply match_regs_setres. + assumption. - (* cond *) destruct ((gen_injections f) ! pc) eqn:INJECTION. @@ -1748,7 +1750,7 @@ Section INJECTOR. + constructor; trivial. apply match_regs_write. assumption. - Admitted. + Qed. Theorem transf_program_correct: Smallstep.forward_simulation (semantics prog) (semantics tprog). -- cgit From 87a4d7e9f493876821e26548d379132f16a7a8ea Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 08:10:08 +0200 Subject: preparatory work for allowing injection after calls --- backend/Injectproof.v | 46 ++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 40 insertions(+), 6 deletions(-) diff --git a/backend/Injectproof.v b/backend/Injectproof.v index b63f9498..dfecbac7 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -572,13 +572,20 @@ Section INJECTOR. specialize M23 with r. intuition congruence. Qed. - + Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := - | match_frames_intro: forall res f tf sp pc rs trs + | match_frames_intro: forall res f tf sp pc pc' rs trs (FUN : transf_function gen_injections f = OK tf) - (REGS : match_regs f rs trs), + (REGS : match_regs f rs trs) + (STAR: + forall ts m trs1, + exists trs2, + (match_regs f trs1 trs2) /\ + Smallstep.star RTL.step tge + (State ts tf sp pc' trs1 m) E0 + (State ts tf sp pc trs2 m)), match_frames (Stackframe res f sp pc rs) - (Stackframe res tf sp pc trs). + (Stackframe res tf sp pc' trs). Inductive match_states: state -> state -> Prop := | match_states_intro: @@ -1519,11 +1526,23 @@ Section INJECTOR. apply match_states_call; auto. constructor; auto. constructor; auto. + + (* FIXME *) + intros. + exists trs1. split. + apply match_regs_refl. + constructor. + ** replace (trs ## args) with (trs ## (instr_uses (Icall (funsig fd) (inr id) args res pc'))) by reflexivity. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. apply match_states_call; auto. constructor; auto. constructor; auto. + (* FIXME *) + intros. + exists trs1. split. + apply match_regs_refl. + constructor. + econstructor; split. * eapply Smallstep.plus_one. apply exec_Icall with (args := args) (sig := (funsig fd)) (ros := ros). @@ -1537,11 +1556,21 @@ Section INJECTOR. apply match_states_call; auto. constructor; auto. constructor; auto. + (* FIXME *) + intros. + exists trs1. split. + apply match_regs_refl. + constructor. ** replace (trs ## args) with (trs ## (instr_uses (Icall (funsig fd) (inr id) args res pc'))) by reflexivity. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. apply match_states_call; auto. constructor; auto. constructor; auto. + (* FIXME *) + intros. + exists trs1. split. + apply match_regs_refl. + constructor. - (* tailcall *) destruct (transf_function_preserves_ros_tail f tf pc rs trs ros args fd (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]]. @@ -1744,12 +1773,17 @@ Section INJECTOR. - (* return *) inv STACKS. inv H1. + destruct (STAR bl m (trs # res <- vres)) as [trs2 [MATCH' STAR']]. econstructor; split. - + apply Smallstep.plus_one. - apply exec_return. + + eapply Smallstep.plus_left. + * apply exec_return. + * exact STAR'. + * reflexivity. + constructor; trivial. + apply match_regs_trans with (rs2 := (trs # res <- vres)). apply match_regs_write. assumption. + assumption. Qed. Theorem transf_program_correct: -- cgit From 82c4699c8d5dd12e29b79045b6b8d2daf573ac91 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 08:27:57 +0200 Subject: now able to inject on Call --- backend/Inject.v | 2 +- backend/Injectproof.v | 33 +++++++++++++++------------------ 2 files changed, 16 insertions(+), 19 deletions(-) diff --git a/backend/Inject.v b/backend/Inject.v index 1a8ec24a..4bb25615 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -48,7 +48,7 @@ Definition alter_successor (i : instruction) (pc' : node) : instruction := | Istore chunk addr args src _ => Istore chunk addr args src pc' | Ibuiltin ef args res _ => Ibuiltin ef args res pc' | Icond cond args _ pc2 => Icond cond args pc' pc2 - | Icall _ _ _ _ _ + | Icall sig ros args res _ => Icall sig ros args res pc' | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => i diff --git a/backend/Injectproof.v b/backend/Injectproof.v index dfecbac7..1dd26a24 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1527,22 +1527,22 @@ Section INJECTOR. constructor; auto. constructor; auto. - (* FIXME *) intros. - exists trs1. split. - apply match_regs_refl. - constructor. + destruct (SKIP ts0 sp m0 trs1) as [trs2 [MATCH PLUS]]. + exists trs2. split. assumption. + apply Smallstep.plus_star. exact PLUS. ** replace (trs ## args) with (trs ## (instr_uses (Icall (funsig fd) (inr id) args res pc'))) by reflexivity. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. apply match_states_call; auto. constructor; auto. constructor; auto. - (* FIXME *) + intros. - exists trs1. split. - apply match_regs_refl. - constructor. + destruct (SKIP ts0 sp m0 trs1) as [trs2 [MATCH PLUS]]. + exists trs2. split. assumption. + apply Smallstep.plus_star. exact PLUS. + + econstructor; split. * eapply Smallstep.plus_one. apply exec_Icall with (args := args) (sig := (funsig fd)) (ros := ros). @@ -1556,21 +1556,18 @@ Section INJECTOR. apply match_states_call; auto. constructor; auto. constructor; auto. - (* FIXME *) - intros. - exists trs1. split. - apply match_regs_refl. - constructor. + + intros. exists trs1. split. + apply match_regs_refl. constructor. + ** replace (trs ## args) with (trs ## (instr_uses (Icall (funsig fd) (inr id) args res pc'))) by reflexivity. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. apply match_states_call; auto. constructor; auto. constructor; auto. - (* FIXME *) - intros. - exists trs1. split. - apply match_regs_refl. - constructor. + + intros. exists trs1. split. + apply match_regs_refl. constructor. - (* tailcall *) destruct (transf_function_preserves_ros_tail f tf pc rs trs ros args fd (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]]. -- cgit From aedaa5cb1435008d1d872b7d6687bec5843798a0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 09:15:28 +0200 Subject: adapting new stuff for ARM and AArch64 --- aarch64/Op.v | 11 ++++++++--- arm/Op.v | 11 ++++++++--- backend/FirstNopproof.v | 17 ++++++++--------- backend/Injectproof.v | 15 ++++++--------- 4 files changed, 30 insertions(+), 24 deletions(-) diff --git a/aarch64/Op.v b/aarch64/Op.v index c0b9d435..afc25aa6 100644 --- a/aarch64/Op.v +++ b/aarch64/Op.v @@ -938,14 +938,19 @@ Definition is_trapping_op (op : operation) := end. +Definition args_of_operation op := + if eq_operation op Omove + then 1%nat + else List.length (fst (type_of_operation op)). + Lemma is_trapping_op_sound: forall op vl sp m, - op <> Omove -> is_trapping_op op = false -> - (List.length vl) = (List.length (fst (type_of_operation op))) -> + (List.length vl) = args_of_operation op -> eval_operation genv sp op vl m <> None. Proof. - destruct op; intros; simpl in *; try congruence. + unfold args_of_operation. + destruct op; destruct eq_operation; intros; simpl in *; try congruence. all: try (destruct vl as [ | vh1 vl1]; try discriminate). all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). diff --git a/arm/Op.v b/arm/Op.v index 671bdbe4..25e48ce1 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -531,14 +531,19 @@ Definition is_trapping_op (op : operation) := end. +Definition args_of_operation op := + if eq_operation op Omove + then 1%nat + else List.length (fst (type_of_operation op)). + Lemma is_trapping_op_sound: forall op vl sp m, - op <> Omove -> is_trapping_op op = false -> - (List.length vl) = (List.length (fst (type_of_operation op))) -> + (List.length vl) = args_of_operation op -> eval_operation genv sp op vl m <> None. Proof. - destruct op; intros; simpl in *; try congruence. + unfold args_of_operation. + destruct op; destruct eq_operation; intros; simpl in *; try congruence. all: try (destruct vl as [ | vh1 vl1]; try discriminate). all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). diff --git a/backend/FirstNopproof.v b/backend/FirstNopproof.v index 5d9a7d6a..a5d63c25 100644 --- a/backend/FirstNopproof.v +++ b/backend/FirstNopproof.v @@ -168,26 +168,25 @@ Proof. + constructor; auto with firstnop. - left. econstructor. split. + eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop. - rewrite <- H0. - apply eval_addressing_preserved. - apply symbols_preserved. + all: rewrite <- H0. + all: auto using eval_addressing_preserved, symbols_preserved. + constructor; auto with firstnop. - left. econstructor. split. + eapply plus_one. eapply exec_Iload_notrap1; eauto with firstnop. - rewrite <- H0. - apply eval_addressing_preserved. + all: rewrite <- H0; + apply eval_addressing_preserved; apply symbols_preserved. + constructor; auto with firstnop. - left. econstructor. split. + eapply plus_one. eapply exec_Iload_notrap2; eauto with firstnop. - rewrite <- H0. - apply eval_addressing_preserved. + all: rewrite <- H0; + apply eval_addressing_preserved; apply symbols_preserved. + constructor; auto with firstnop. - left. econstructor. split. + eapply plus_one. eapply exec_Istore; eauto with firstnop. - rewrite <- H0. - apply eval_addressing_preserved. + all: rewrite <- H0; + apply eval_addressing_preserved; apply symbols_preserved. + constructor; auto with firstnop. - left. econstructor. split. diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 1dd26a24..77cae8a1 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -778,23 +778,20 @@ Section INJECTOR. * exists (trs # res <- v). split. ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial. - rewrite eval_addressing_preserved with (ge1 := ge). - assumption. - exact symbols_preserved. + all: try rewrite eval_addressing_preserved with (ge1 := ge). + all: auto using symbols_preserved. ** apply assign_above; auto. * exists (trs # res <- Vundef). split. ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial. - rewrite eval_addressing_preserved with (ge1 := ge). - assumption. - exact symbols_preserved. + all: rewrite eval_addressing_preserved with (ge1 := ge). + all: auto using symbols_preserved. ** apply assign_above; auto. + exists (trs # res <- Vundef). split. * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial. - rewrite eval_addressing_preserved with (ge1 := ge). - assumption. - exact symbols_preserved. + all: rewrite eval_addressing_preserved with (ge1 := ge). + all: auto using symbols_preserved. * apply assign_above; auto. Qed. -- cgit From 8e3ae6d6ff625dc8f93c54392b80b836b613c3cc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 09:30:18 +0200 Subject: porting to ppc riscV x86 --- powerpc/Op.v | 12 +++++++++--- riscV/Op.v | 12 +++++++++--- x86/Op.v | 11 ++++++++--- 3 files changed, 26 insertions(+), 9 deletions(-) diff --git a/powerpc/Op.v b/powerpc/Op.v index b73cb14b..a0ee5bb8 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -592,14 +592,20 @@ Definition is_trapping_op (op : operation) := | _ => false end. +Definition args_of_operation op := + if eq_operation op Omove + then 1%nat + else List.length (fst (type_of_operation op)). + + Lemma is_trapping_op_sound: forall op vl sp m, - op <> Omove -> is_trapping_op op = false -> - (List.length vl) = (List.length (fst (type_of_operation op))) -> + (List.length vl) = args_of_operation op -> eval_operation genv sp op vl m <> None. Proof. - destruct op; intros; simpl in *; try congruence. + unfold args_of_operation. + destruct op; destruct eq_operation; intros; simpl in *; try congruence. all: try (destruct vl as [ | vh1 vl1]; try discriminate). all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). diff --git a/riscV/Op.v b/riscV/Op.v index a71696c7..14d07e0b 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -682,15 +682,21 @@ Definition is_trapping_op (op : operation) := | Ofloatoflong | Ofloatoflongu => true | _ => false end. + + +Definition args_of_operation op := + if eq_operation op Omove + then 1%nat + else List.length (fst (type_of_operation op)). Lemma is_trapping_op_sound: forall op vl sp m, - op <> Omove -> is_trapping_op op = false -> - (List.length vl) = (List.length (fst (type_of_operation op))) -> + (List.length vl) = args_of_operation op -> eval_operation genv sp op vl m <> None. Proof. - destruct op; intros; simpl in *; try congruence. + unfold args_of_operation. + destruct op; destruct eq_operation; intros; simpl in *; try congruence. all: try (destruct vl as [ | vh1 vl1]; try discriminate). all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). diff --git a/x86/Op.v b/x86/Op.v index 15672bbe..28e6dbd8 100644 --- a/x86/Op.v +++ b/x86/Op.v @@ -760,14 +760,19 @@ Definition is_trapping_op (op : operation) := | _ => false end. +Definition args_of_operation op := + if eq_operation op Omove + then 1%nat + else List.length (fst (type_of_operation op)). + Lemma is_trapping_op_sound: forall op vl sp m, - op <> Omove -> is_trapping_op op = false -> - (List.length vl) = (List.length (fst (type_of_operation op))) -> + (List.length vl) = args_of_operation op -> eval_operation genv sp op vl m <> None. Proof. - destruct op; intros; simpl in *; try congruence. + unfold args_of_operation. + destruct op; destruct eq_operation; intros; simpl in *; try congruence. all: try (destruct vl as [ | vh1 vl1]; try discriminate). all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). -- cgit From d0590cab5ee32df395c129ee3edfa2dc3aaa202d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 13:30:30 +0200 Subject: begin adapting for LICM phase --- backend/Inject.v | 4 ++-- backend/Injectproof.v | 60 ++++++++++++++++++++++++------------------------- driver/Clflags.ml | 1 + driver/Compopts.v | 3 +++ driver/Driver.ml | 2 ++ extraction/extraction.v | 3 +++ 6 files changed, 41 insertions(+), 32 deletions(-) diff --git a/backend/Inject.v b/backend/Inject.v index 4bb25615..2350c149 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -81,7 +81,7 @@ Definition inject prog extra_pc injections : code := *) Section INJECTOR. - Variable gen_injections : function -> PTree.t (list inj_instr). + Variable gen_injections : function -> node -> reg -> PTree.t (list inj_instr). Definition valid_injection_instr (max_reg : reg) (i : inj_instr) := match i with @@ -102,9 +102,9 @@ Section INJECTOR. valid_injections1 (max_pc_function f) (max_reg_function f). Definition transf_function (f : function) : res function := - let injections := PTree.elements (gen_injections f) in let max_pc := max_pc_function f in let max_reg := max_reg_function f in + let injections := PTree.elements (gen_injections f max_pc max_reg) in if valid_injections1 max_pc max_reg injections then OK {| fn_sig := f.(fn_sig); diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 77cae8a1..2506bcc8 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -538,7 +538,7 @@ Qed. *) Section INJECTOR. - Variable gen_injections : function -> PTree.t (list inj_instr). + Variable gen_injections : function -> node -> reg -> PTree.t (list inj_instr). Definition match_prog (p tp: RTL.program) := match_program (fun ctx f tf => transf_fundef gen_injections f = OK tf) eq p tp. @@ -808,10 +808,10 @@ Section INJECTOR. Lemma transf_function_inj_starstep_rec : forall ts f tf sp m inj_n src_pc inj_pc inj_code (FUN : transf_function gen_injections f = OK tf) - (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = Some (src_pc, inj_code)) (POSITION : inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) inj_n = inj_pc) + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc) (k : nat) (CUR : (k <= (List.length inj_code))%nat) (trs : regset), @@ -839,7 +839,7 @@ Section INJECTOR. injection VALIDATE. intro TF. symmetry in TF. - pose proof (inject_l_injected (PTree.elements (gen_injections f)) (fn_code f) inj_n src_pc inj_code (Pos.succ (max_pc_function f)) ((List.length inj_code) - (S k))%nat) as INJECTED. + pose proof (inject_l_injected (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) (fn_code f) inj_n src_pc inj_code (Pos.succ (max_pc_function f)) ((List.length inj_code) - (S k))%nat) as INJECTED. lapply INJECTED. { clear INJECTED. intro INJECTED. @@ -848,7 +848,7 @@ Section INJECTOR. pose proof (INJECTED INJ LESS) as INJ'. replace (snd (inject_l (fn_code f) (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)))) with (fn_code tf) in INJ'. + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))))) with (fn_code tf) in INJ'. 2: rewrite TF; simpl; reflexivity. apply transf_function_inj_step with (f:=f) (ts:=ts) (sp:=sp) (trs:=trs) (m := m) in INJ'. 2: assumption. { @@ -898,10 +898,10 @@ Section INJECTOR. Lemma transf_function_inj_starstep : forall ts f tf sp m inj_n src_pc inj_pc inj_code (FUN : transf_function gen_injections f = OK tf) - (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = Some (src_pc, inj_code)) (POSITION : inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) inj_n = inj_pc) + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc) (trs : regset), exists trs', match_regs (f : function) trs trs' /\ @@ -920,11 +920,11 @@ Section INJECTOR. Lemma transf_function_inj_end : forall ts f tf sp m inj_n src_pc inj_pc inj_code i (FUN : transf_function gen_injections f = OK tf) - (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = Some (src_pc, inj_code)) (SRC: (fn_code f) ! src_pc = Some i) (POSITION : inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) inj_n = inj_pc) + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc) (trs : regset), RTL.step tge (State ts tf sp (pos_add_nat inj_pc (List.length inj_code)) trs m) E0 @@ -938,13 +938,13 @@ Section INJECTOR. injection VALIDATE. intro TF. symmetry in TF. - pose proof (inject_l_injected_end (PTree.elements (gen_injections f)) (fn_code f) inj_n src_pc i inj_code (Pos.succ (max_pc_function f))) as INJECTED. + pose proof (inject_l_injected_end (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) (fn_code f) inj_n src_pc i inj_code (Pos.succ (max_pc_function f))) as INJECTED. lapply INJECTED. 2: assumption. clear INJECTED. intro INJECTED. lapply INJECTED. - 2: apply (PTree.elements_keys_norepet (gen_injections f)); fail. + 2: apply (PTree.elements_keys_norepet (gen_injections f (max_pc_function f) (max_reg_function f))); fail. clear INJECTED. intro INJECTED. lapply INJECTED. @@ -954,7 +954,7 @@ Section INJECTOR. clear INJECTED. replace (snd (inject_l (fn_code f) (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)))) with (fn_code tf) in INJ'. + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))))) with (fn_code tf) in INJ'. 2: rewrite TF; simpl; reflexivity. rewrite POSITION in INJ'. apply exec_Inop. @@ -975,11 +975,11 @@ Section INJECTOR. Lemma transf_function_inj_plusstep : forall ts f tf sp m inj_n src_pc inj_pc inj_code i (FUN : transf_function gen_injections f = OK tf) - (INJ : nth_error (PTree.elements (gen_injections f)) inj_n = + (INJ : nth_error (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = Some (src_pc, inj_code)) (SRC: (fn_code f) ! src_pc = Some i) (POSITION : inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) inj_n = inj_pc) + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) inj_n = inj_pc) (trs : regset), exists trs', match_regs (f : function) trs trs' /\ @@ -1001,7 +1001,7 @@ Section INJECTOR. forall f tf pc (FUN : transf_function gen_injections f = OK tf) (LESS : pc <= max_pc_function f) - (NOCHANGE : (gen_injections f) ! pc = None), + (NOCHANGE : (gen_injections f (max_pc_function f) (max_reg_function f)) ! pc = None), (fn_code tf) ! pc = (fn_code f) ! pc. Proof. intros. @@ -1027,7 +1027,7 @@ Section INJECTOR. forall f tf pc injl ii (FUN : transf_function gen_injections f = OK tf) (LESS : pc <= max_pc_function f) - (INJECTION : (gen_injections f) ! pc = Some injl) + (INJECTION : (gen_injections f (max_pc_function f) (max_reg_function f)) ! pc = Some injl) (INSTR: (fn_code f) ! pc = Some ii), exists pc' : node, (fn_code tf) ! pc = Some (alter_successor ii pc') /\ @@ -1043,7 +1043,7 @@ Section INJECTOR. apply In_nth_error in INJECTION. destruct INJECTION as [injn INJECTION]. exists (inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) injn). + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) injn). split. { unfold transf_function in FUN. destruct (valid_injections1) eqn:VALID in FUN. @@ -1067,7 +1067,7 @@ Section INJECTOR. intros. pose proof (transf_function_inj_plusstep ts f tf sp m injn pc (inject_l_position (Pos.succ (max_pc_function f)) - (PTree.elements (gen_injections f)) injn) + (PTree.elements (gen_injections f (max_pc_function f) (max_reg_function f))) injn) injl ii FUN INJECTION INSTR) as TRANS. lapply TRANS. 2: reflexivity. @@ -1272,7 +1272,7 @@ Section INJECTOR. Proof. induction 1; intros ts1 MS; inv MS; try (inv TRC). - (* nop *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1295,7 +1295,7 @@ Section INJECTOR. * constructor; trivial. - (* op *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1339,7 +1339,7 @@ Section INJECTOR. assumption. - (* load *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1381,7 +1381,7 @@ Section INJECTOR. assumption. - (* load notrap1 *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1421,7 +1421,7 @@ Section INJECTOR. assumption. - (* load notrap2 *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1463,7 +1463,7 @@ Section INJECTOR. assumption. - (* store *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1506,7 +1506,7 @@ Section INJECTOR. * constructor; trivial. - (* call *) destruct (transf_function_preserves_ros f tf pc rs trs ros args res fd pc' (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]]. - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1568,7 +1568,7 @@ Section INJECTOR. - (* tailcall *) destruct (transf_function_preserves_ros_tail f tf pc rs trs ros args fd (funsig fd) FUN REGS H H0) as [tfd [TFD1 TFD2]]. - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1606,7 +1606,7 @@ Section INJECTOR. apply match_states_call; auto. - (* builtin *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1642,7 +1642,7 @@ Section INJECTOR. assumption. - (* cond *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + destruct b eqn:B. ++ exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } @@ -1695,7 +1695,7 @@ Section INJECTOR. *** reflexivity. ** constructor; auto. - - destruct ((gen_injections f) ! pc) eqn:INJECTION. + - destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. @@ -1718,7 +1718,7 @@ Section INJECTOR. eassumption. * constructor; trivial. - (* return *) - destruct ((gen_injections f) ! pc) eqn:INJECTION. + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } intros [pc_inj [ALTER SKIP]]. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ff2647a7..ae96e820 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -82,5 +82,6 @@ let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true let option_fforward_moves = ref true +let option_fmove_loop_invariants = ref false let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 diff --git a/driver/Compopts.v b/driver/Compopts.v index a3181da8..e4dae87d 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -48,6 +48,9 @@ Parameter optim_CSE3: unit -> bool. (** Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. *) Parameter optim_CSE3_alias_analysis: unit -> bool. +(** Flag -fmove-loop-invariants. *) +Parameter optim_move_loop_invariants: unit -> bool. + (** Flag -fredundancy. For dead code elimination. *) Parameter optim_redundancy: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index b167dbd1..0f9e637c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -199,6 +199,7 @@ Processing options: -fcse2 Perform inter-loop common subexpression elimination [off] -fcse3 Perform inter-loop common subexpression elimination [on] -fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on] + -fmove-loop-invariants Perform loop-invariant code motion [off] -fredundancy Perform redundancy elimination [on] -fpostpass Perform postpass scheduling (only for K1 architecture) [on] -fpostpass= Perform postpass scheduling with the specified optimization [list] @@ -401,6 +402,7 @@ let cmdline_actions = @ f_opt "cse2" option_fcse2 @ f_opt "cse3" option_fcse3 @ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis + @ f_opt "move-loop-invariants" option_fmove_loop_invariants @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ] diff --git a/extraction/extraction.v b/extraction/extraction.v index cb461361..1bb5a709 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -120,6 +120,9 @@ Extract Constant Compopts.optim_CSE3 => "fun _ -> !Clflags.option_fcse3". Extract Constant Compopts.optim_CSE3_alias_analysis => "fun _ -> !Clflags.option_fcse3_alias_analysis". +Extract Constant Compopts.optim_move_loop_invariants => + "fun _ -> !Clflags.option_fmove_loop_invariants". + Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". Extract Constant Compopts.optim_postpass => -- cgit From 6379f6291eea909426f074db67837b04a1dec9ae Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 14:24:05 +0200 Subject: attempt at compiling --- Makefile | 1 + backend/LICM.v | 9 +++++++++ backend/LICMproof.v | 21 +++++++++++++++++++++ driver/Compiler.v | 36 ++++++++++++++++++++++++------------ 4 files changed, 55 insertions(+), 12 deletions(-) create mode 100644 backend/LICM.v create mode 100644 backend/LICMproof.v diff --git a/Makefile b/Makefile index f005d048..b7fed0d4 100644 --- a/Makefile +++ b/Makefile @@ -91,6 +91,7 @@ BACKEND=\ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ CSE3analysis.v CSE3analysisproof.v CSE3.v CSE3proof.v \ + LICM.v LICMproof.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ diff --git a/backend/LICM.v b/backend/LICM.v new file mode 100644 index 00000000..1b5334ba --- /dev/null +++ b/backend/LICM.v @@ -0,0 +1,9 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. +Require Inject. + +Definition gen_injections (f : function) (max_pc : node) (max_reg : reg): + PTree.t (list Inject.inj_instr) := PTree.empty (list Inject.inj_instr). + +Definition transf_program := Inject.transf_program gen_injections. diff --git a/backend/LICMproof.v b/backend/LICMproof.v new file mode 100644 index 00000000..065a7f74 --- /dev/null +++ b/backend/LICMproof.v @@ -0,0 +1,21 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. +Require Import LICM. +Require Injectproof. + +Definition match_prog : program -> program -> Prop := + Injectproof.match_prog gen_injections. + +Section PRESERVATION. + + Variables prog tprog: program. + Hypothesis TRANSF: match_prog prog tprog. + + Theorem transf_program_correct : + Smallstep.forward_simulation (semantics prog) (semantics tprog). + Proof. + apply Injectproof.transf_program_correct with (gen_injections := gen_injections). + exact TRANSF. + Qed. +End PRESERVATION. diff --git a/driver/Compiler.v b/driver/Compiler.v index 5175abdb..dbf62368 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -41,6 +41,7 @@ Require FirstNop. Require Renumber. Require Duplicate. Require Constprop. +Require LICM. Require CSE. Require ForwardMoves. Require CSE2. @@ -68,6 +69,7 @@ Require FirstNopproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. +Require LICMproof. Require CSEproof. Require ForwardMovesproof. Require CSE2proof. @@ -136,7 +138,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 1) @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) - @@ time "Inserting initial nop" FirstNop.transf_program + @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program) @@ print (print_RTL 3) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 4) @@ -144,22 +146,26 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 5) @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 6) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ time "Renumbering pre LICM" Renumber.transf_program @@ print (print_RTL 7) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program) @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 10) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 11) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) @@ print (print_RTL 12) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 13) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 14) + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@ print (print_RTL 15) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 16) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -261,10 +267,11 @@ Definition CompCert's_passes := ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog - ::: mkpass FirstNopproof.match_prog + ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) ::: mkpass Renumberproof.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_move_loop_invariants LICMproof.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_CSE2 CSE2proof.match_prog) @@ -308,14 +315,19 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. + ::: mkpass (match_if Compopts.optim_move_loop_invariants LICM.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) + ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) 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 := FirstNop.transf_program p8) in *. + set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) in *. set (p9bis := Renumber.transf_program p9) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) 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_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. + set (p12ter :=(total_if optim_move_loop_invariant Renumber.transf_program p12bis)) in *. + destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. -- cgit From a3d40b88608b8b5e7e615346ea1c33198355cbbc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 14:45:25 +0200 Subject: clearer types --- backend/LICM.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/backend/LICM.v b/backend/LICM.v index 1b5334ba..d45eef43 100644 --- a/backend/LICM.v +++ b/backend/LICM.v @@ -6,4 +6,7 @@ Require Inject. Definition gen_injections (f : function) (max_pc : node) (max_reg : reg): PTree.t (list Inject.inj_instr) := PTree.empty (list Inject.inj_instr). -Definition transf_program := Inject.transf_program gen_injections. +Opaque gen_injections. + +Definition transf_program : program -> res program := + Inject.transf_program gen_injections. -- cgit From 01f42ef55d91bbb57b47ecc2be7e691165778980 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 15:38:06 +0200 Subject: fix Compiler.v --- backend/LICMproof.v | 6 ++++++ driver/Compiler.v | 28 ++++++++++++++++------------ 2 files changed, 22 insertions(+), 12 deletions(-) diff --git a/backend/LICMproof.v b/backend/LICMproof.v index 065a7f74..2b76b668 100644 --- a/backend/LICMproof.v +++ b/backend/LICMproof.v @@ -12,6 +12,12 @@ Section PRESERVATION. Variables prog tprog: program. Hypothesis TRANSF: match_prog prog tprog. + Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. + Proof. + intros. eapply match_transform_partial_program_contextual; eauto. + Qed. + Theorem transf_program_correct : Smallstep.forward_simulation (semantics prog) (semantics tprog). Proof. diff --git a/driver/Compiler.v b/driver/Compiler.v index dbf62368..89a15d93 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -271,8 +271,9 @@ Definition CompCert's_passes := ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) + ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) - ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) @@ -315,18 +316,15 @@ Proof. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - ::: mkpass (match_if Compopts.optim_move_loop_invariants LICM.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) 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 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) in *. set (p9bis := Renumber.transf_program p9) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) 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 *. + set (p12 := Renumber.transf_program p11) in *. destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. - set (p12ter :=(total_if optim_move_loop_invariant Renumber.transf_program p12bis)) in *. + set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. @@ -349,11 +347,13 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. 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 FirstNopproof.transf_program_match; auto. - exists p9bis; split. apply Renumberproof.transf_program_match; auto. + exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. + exists p9bis; split. apply Renumberproof.transf_program_match. 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 p12; split. apply Renumberproof.transf_program_match. + exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. + exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. @@ -418,7 +418,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 p27)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p29)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -436,12 +436,16 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. eapply FirstNopproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. eapply compose_forward_simulations. eapply Renumberproof.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 match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. + eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. eapply compose_forward_simulations. -- cgit From 87d2c34910a017c13a908cfe2cf2c627e56e6cfe Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 15:46:03 +0200 Subject: reordering passes --- driver/Compiler.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/driver/Compiler.v b/driver/Compiler.v index 89a15d93..e6d39152 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -144,9 +144,9 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 4) @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 5) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@ time "Renumbering pre constprop" Renumber.transf_program @@ print (print_RTL 6) - @@ time "Renumbering pre LICM" Renumber.transf_program + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 7) @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) @@ print (print_RTL 8) @@ -270,8 +270,8 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) - ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass Renumberproof.match_prog + ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -321,8 +321,8 @@ Proof. set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) in *. set (p9bis := Renumber.transf_program p9) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. - set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. - set (p12 := Renumber.transf_program p11) in *. + set (p11 := Renumber.transf_program p10) in *. + set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. @@ -350,8 +350,8 @@ Proof. exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. exists p9bis; split. apply Renumberproof.transf_program_match. 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 Renumberproof.transf_program_match. + exists p11; split. apply Renumberproof.transf_program_match. + exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. @@ -442,8 +442,8 @@ Ltac DestructM := 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. eapply Renumberproof.transf_program_correct; eassumption. + eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit From aebbc43842ec0c49058b718c685e08edf11ce614 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 16:15:54 +0200 Subject: route through LICMaux --- backend/LICM.v | 5 +---- backend/LICMaux.ml | 4 ++++ extraction/extraction.v | 3 +++ 3 files changed, 8 insertions(+), 4 deletions(-) create mode 100644 backend/LICMaux.ml diff --git a/backend/LICM.v b/backend/LICM.v index d45eef43..0a0a1c7d 100644 --- a/backend/LICM.v +++ b/backend/LICM.v @@ -3,10 +3,7 @@ Require Import AST Linking. Require Import Memory Registers Op RTL. Require Inject. -Definition gen_injections (f : function) (max_pc : node) (max_reg : reg): - PTree.t (list Inject.inj_instr) := PTree.empty (list Inject.inj_instr). - -Opaque gen_injections. +Axiom gen_injections : function -> node -> reg -> PTree.t (list Inject.inj_instr). Definition transf_program : program -> res program := Inject.transf_program gen_injections. diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml new file mode 100644 index 00000000..542b6ea8 --- /dev/null +++ b/backend/LICMaux.ml @@ -0,0 +1,4 @@ +open RTL;; + +let gen_injections (f : function) (max_pc : node) (max_reg : reg) = + PTree.empty;; diff --git a/extraction/extraction.v b/extraction/extraction.v index 1bb5a709..b102503b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -87,6 +87,9 @@ Extract Inlined Constant Inlining.inlining_info => "Inliningaux.inlining_info". Extract Inlined Constant Inlining.inlining_analysis => "Inliningaux.inlining_analysis". Extraction Inline Inlining.ret Inlining.bind. +(* Loop invariant code motion *) +Extract Inlined Constant LICM.gen_injections => "LICMaux.gen_injections". + (* Allocation *) Extract Constant Allocation.regalloc => "Regalloc.regalloc". -- cgit From 34bb4b19299e21e87871c7159567ac425c70e6b4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 17:18:50 +0200 Subject: toy example for injecting code --- backend/LICMaux.ml | 31 +++++++++++++++++++++++++++++-- 1 file changed, 29 insertions(+), 2 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 542b6ea8..3f7d61b1 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -1,4 +1,31 @@ open RTL;; +open Camlcoq;; +open Maps;; +open Integers;; -let gen_injections (f : function) (max_pc : node) (max_reg : reg) = - PTree.empty;; +type reg = P.t;; + +module IntSet = Set.Make(struct type t=int let compare = (-) end);; + +let loop_headers (f : coq_function) = + PTree.fold (fun (already : IntSet.t) + (coq_pc : node) (instr : instruction) -> + let pc = P.to_int coq_pc in + List.fold_left (fun (already : IntSet.t) (coq_pc' : node) -> + let pc' = P.to_int coq_pc' in + if pc' >= pc + then IntSet.add pc' already + else already) already (successors_instr instr)) + f.fn_code IntSet.empty;; + +let print_loop_headers f = + print_endline "Loop headers"; + IntSet.iter + (fun i -> Printf.printf "%d " i) + (loop_headers f); + print_newline ();; + +let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg): + (Inject.inj_instr list) PTree.t = + let max_reg = P.to_int coq_max_reg in + PTree.set coq_max_pc [Inject.INJload(AST.Mint32, (Op.Aindexed (Ptrofs.of_int (Z.of_sint 0))), [P.of_int 1], P.of_int (max_reg+1))] PTree.empty;; -- cgit From 5450d5054dc84d31c820b6d60c87c628290d5487 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 15 Apr 2020 11:11:05 +0200 Subject: Coq error message update in configure --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure b/configure index cb2f52ba..366ab847 100755 --- a/configure +++ b/configure @@ -575,7 +575,7 @@ case "$coq_ver" in if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires one of the following Coq versions: 8.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0" + echo "Error: CompCert requires one of the following Coq versions: 8.11.1, 8.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0" missingtools=true fi;; "") -- cgit From ba32e5daa1ff343a1a0b89e65c2ba5764c9cef04 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 14:10:51 +0200 Subject: progress on CSE2 builtins --- backend/CSE2.v | 31 +++++-------------------------- backend/CSE2proof.v | 20 +++++++++++++++----- 2 files changed, 20 insertions(+), 31 deletions(-) diff --git a/backend/CSE2.v b/backend/CSE2.v index 900a7517..e2ab9f07 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -375,33 +375,12 @@ Definition load (chunk: memory_chunk) (addr : addressing) | None => load1 chunk addr dst args rel end. -(* NO LONGER NEEDED -Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop := - match l with - | nil => True - | (r,sv)::tail => (tr ! r) = Some sv /\ list_represents tail tr +Fixpoint kill_builtin_res res rel := + match res with + | BR r => kill_reg r rel + | _ => rel end. -Lemma elements_represent : - forall { X : Type }, - forall tr : (PTree.t X), - (list_represents (PTree.elements tr) tr). -Proof. - intros. - generalize (PTree.elements_complete tr). - generalize (PTree.elements tr). - induction l; simpl; trivial. - intro COMPLETE. - destruct a as [ r sv ]. - split. - { - apply COMPLETE. - left; reflexivity. - } - apply IHl; auto. -Qed. -*) - Definition apply_instr instr (rel : RELATION.t) : RB.t := match instr with | Inop _ @@ -411,7 +390,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t := | Iop op args dst _ => Some (gen_oper op dst args rel) | Iload trap chunk addr args dst _ => Some (load chunk addr dst args rel) | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) - | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) + | Ibuiltin _ _ res _ => Some (kill_builtin_res res (kill_mem rel)) | Itailcall _ _ _ | Ireturn _ => RB.bot end. diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 309ccce1..e61cde3d 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1033,7 +1033,16 @@ Proof. assumption. } intuition congruence. -Qed. +Qed. + +Lemma kill_builtin_res_sound: + forall res (m : mem) (rs : regset) vres (rel : RELATION.t) + (REL : sem_rel m rel rs), + (sem_rel m (kill_builtin_res res rel) (regmap_setres res vres rs)). +Proof. + destruct res; simpl; intros; trivial. + apply kill_reg_sound; trivial. +Qed. End SOUNDNESS. Definition match_prog (p tp: RTL.program) := @@ -1578,9 +1587,9 @@ Proof. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some RELATION.top). + apply sem_rel_b_ge with (rb2 := Some (kill_builtin_res res (kill_mem mpc))). { - replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)). + replace (Some (kill_builtin_res res (kill_mem mpc))) with (apply_instr' (fn_code f) pc (map # pc)). { eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. 2: apply apply_instr'_bot. @@ -1591,8 +1600,9 @@ Proof. rewrite MPC. reflexivity. } - apply top_ok. - + apply kill_builtin_res_sound. + apply kill_mem_sound with (m := m). + assumption. (* cond *) - econstructor; split. -- cgit From b3431b1d9ee5121883d307cff0b62b7e53369891 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 15:29:24 +0200 Subject: refine the rules for builtins --- backend/CSE2.v | 19 ++++++++++++++++++- backend/CSE2proof.v | 23 +++++++++++++++++++---- 2 files changed, 37 insertions(+), 5 deletions(-) diff --git a/backend/CSE2.v b/backend/CSE2.v index e2ab9f07..d9fe5799 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -381,6 +381,23 @@ Fixpoint kill_builtin_res res rel := | _ => rel end. +Definition apply_external_call ef (rel : RELATION.t) : RELATION.t := + match ef with + | EF_builtin name sg + | EF_runtime name sg => + match Builtins.lookup_builtin_function name sg with + | Some bf => rel + | None => kill_mem rel + end + | EF_malloc (* FIXME *) + | EF_external _ _ + | EF_vstore _ + | EF_free (* FIXME *) + | EF_memcpy _ _ (* FIXME *) + | EF_inline_asm _ _ _ => kill_mem rel + | _ => rel + end. + Definition apply_instr instr (rel : RELATION.t) : RB.t := match instr with | Inop _ @@ -390,7 +407,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t := | Iop op args dst _ => Some (gen_oper op dst args rel) | Iload trap chunk addr args dst _ => Some (load chunk addr dst args rel) | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) - | Ibuiltin _ _ res _ => Some (kill_builtin_res res (kill_mem rel)) + | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel)) | Itailcall _ _ _ | Ireturn _ => RB.bot end. diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index e61cde3d..9e0ad909 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1125,6 +1125,22 @@ Definition is_killed_in_fmap fmap pc res := | Some map => is_killed_in_map map pc res end. +Lemma external_call_sound: + forall ef (rel : RELATION.t) sp (m m' : mem) (rs : regset) vargs t vres + (REL : sem_rel fundef unit ge sp m rel rs) + (CALL : external_call ef ge vargs m t vres m'), + sem_rel fundef unit ge sp m' (apply_external_call ef rel) rs. +Proof. + destruct ef; intros; simpl in *. + all: eauto using kill_mem_sound. + all: unfold builtin_or_external_sem in *. + 1, 2: destruct (Builtins.lookup_builtin_function name sg); + eauto using kill_mem_sound; + inv CALL; eauto using kill_mem_sound. + all: inv CALL. + all: eauto using kill_mem_sound. +Qed. + Definition sem_rel_b' := sem_rel_b fundef unit ge. Definition fmap_sem' := fmap_sem fundef unit ge. Definition subst_arg_ok' := subst_arg_ok fundef unit ge. @@ -1587,9 +1603,9 @@ Proof. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some (kill_builtin_res res (kill_mem mpc))). + apply sem_rel_b_ge with (rb2 := Some (kill_builtin_res res (apply_external_call ef mpc))). { - replace (Some (kill_builtin_res res (kill_mem mpc))) with (apply_instr' (fn_code f) pc (map # pc)). + replace (Some (kill_builtin_res res (apply_external_call ef mpc))) with (apply_instr' (fn_code f) pc (map # pc)). { eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. 2: apply apply_instr'_bot. @@ -1601,8 +1617,7 @@ Proof. reflexivity. } apply kill_builtin_res_sound. - apply kill_mem_sound with (m := m). - assumption. + eapply external_call_sound with (m := m); eassumption. (* cond *) - econstructor; split. -- cgit From 60e4ad85c6cd433c9e28c9e407a957ca3a302c22 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 18:00:14 +0200 Subject: CSE3: better builtin handling --- backend/CSE2.v | 2 +- backend/CSE3analysis.v | 25 ++++++++++++++++++++++++- backend/CSE3analysisproof.v | 30 ++++++++++++++++++++++++++++++ backend/CSE3proof.v | 8 +++++--- 4 files changed, 60 insertions(+), 5 deletions(-) diff --git a/backend/CSE2.v b/backend/CSE2.v index cad740ba..8e2307b0 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -262,7 +262,7 @@ Definition load (chunk: memory_chunk) (addr : addressing) | None => load1 chunk addr dst args rel end. -Fixpoint kill_builtin_res res rel := +Definition kill_builtin_res res rel := match res with | BR r => kill_reg r rel | _ => rel diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 90ce4ce7..bc5d3244 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -325,6 +325,29 @@ Section OPERATIONS. (rel : RELATION.t) : RELATION.t := store1 chunk addr (forward_move_l rel args) src ty rel. + Definition kill_builtin_res res rel := + match res with + | BR r => kill_reg r rel + | _ => rel + end. + + Definition apply_external_call ef (rel : RELATION.t) : RELATION.t := + match ef with + | EF_builtin name sg + | EF_runtime name sg => + match Builtins.lookup_builtin_function name sg with + | Some bf => rel + | None => kill_mem rel + end + | EF_malloc (* FIXME *) + | EF_external _ _ + | EF_vstore _ + | EF_free (* FIXME *) + | EF_memcpy _ _ (* FIXME *) + | EF_inline_asm _ _ _ => kill_mem rel + | _ => rel + end. + Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t := match instr with | Inop _ @@ -335,7 +358,7 @@ Section OPERATIONS. | Iop op args dst _ => Some (oper dst (SOp op) args rel) | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel) | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) - | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) + | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel)) | Itailcall _ _ _ | Ireturn _ => RB.bot end. End PER_NODE. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index b87ec92c..f4ec7a10 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -869,6 +869,36 @@ Section SOUNDNESS. Hint Resolve store_sound : cse3. + Lemma kill_builtin_res_sound: + forall res (m : mem) (rs : regset) vres (rel : RELATION.t) + (REL : sem_rel rel rs m), + (sem_rel (kill_builtin_res (ctx:=ctx) res rel) + (regmap_setres res vres rs) m). + Proof. + destruct res; simpl; intros; trivial. + apply kill_reg_sound; trivial. + Qed. + + Hint Resolve kill_builtin_res_sound : cse3. + + Lemma external_call_sound: + forall ge ef (rel : RELATION.t) (m m' : mem) (rs : regset) vargs t vres + (REL : sem_rel rel rs m) + (CALL : external_call ef ge vargs m t vres m'), + sem_rel (apply_external_call (ctx:=ctx) ef rel) rs m'. + Proof. + destruct ef; intros; simpl in *. + all: eauto using kill_mem_sound. + all: unfold builtin_or_external_sem in *. + 1, 2: destruct (Builtins.lookup_builtin_function name sg); + eauto using kill_mem_sound; + inv CALL; eauto using kill_mem_sound. + all: inv CALL. + all: eauto using kill_mem_sound. + Qed. + + Hint Resolve external_call_sound : cse3. + Section INDUCTIVENESS. Variable fn : RTL.function. Variable tenv : typing_env. diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 19fb20be..53872e62 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -224,7 +224,6 @@ Proof. eapply function_ptr_translated; eauto. Qed. -Check sem_rel_b. Inductive match_stackframes: list stackframe -> list stackframe -> signature -> Prop := | match_stackframes_nil: forall sg, sg.(sig_res) = Tint -> @@ -428,8 +427,8 @@ Ltac IND_STEP := destruct ((fst (preanalysis tenv fn)) # mpc) as [zinv | ]; simpl in *; intuition; - eapply rel_ge; eauto with cse3; - idtac mpc mpc' fn minstr + eapply rel_ge; eauto with cse3 (* ; for printing + idtac mpc mpc' fn minstr *) end. Lemma if_same : forall {T : Type} (b : bool) (x : T), @@ -753,6 +752,9 @@ Proof. + econstructor; eauto. * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt. * IND_STEP. + apply kill_builtin_res_sound; eauto with cse3. + eapply external_call_sound; eauto with cse3. + - (* Icond *) econstructor. split. + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. -- cgit From 6ae48a2f079d6c420df57cb8616692c3d6cdd0ca Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 18:01:25 +0200 Subject: adapt for Icond with predicted direction --- backend/CSE3.v | 4 ++-- backend/CSE3analysis.v | 2 +- backend/Inject.v | 4 ++-- backend/Injectproof.v | 16 ++++++++-------- 4 files changed, 13 insertions(+), 13 deletions(-) diff --git a/backend/CSE3.v b/backend/CSE3.v index d0dc3aef..352cc895 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -62,8 +62,8 @@ Definition transf_instr (fmap : PMap.t RB.t) Icall sig ros (subst_args fmap pc args) dst s | Itailcall sig ros args => Itailcall sig ros (subst_args fmap pc args) - | Icond cond args s1 s2 => - Icond cond (subst_args fmap pc args) s1 s2 + | Icond cond args s1 s2 expected => + Icond cond (subst_args fmap pc args) s1 s2 expected | Ijumptable arg tbl => Ijumptable (subst_arg fmap pc arg) tbl | Ireturn (Some arg) => diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 12fb2d1f..90ce4ce7 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -328,7 +328,7 @@ Section OPERATIONS. Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t := match instr with | Inop _ - | Icond _ _ _ _ + | Icond _ _ _ _ _ | Ijumptable _ _ => Some rel | Istore chunk addr args src _ => Some (store chunk addr args src (tenv src) rel) diff --git a/backend/Inject.v b/backend/Inject.v index 2350c149..971a5423 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -34,7 +34,7 @@ Definition successor (i : instruction) : node := | Istore _ _ _ _ pc' => pc' | Icall _ _ _ _ pc' => pc' | Ibuiltin _ _ _ pc' => pc' - | Icond _ _ pc' _ => pc' + | Icond _ _ pc' _ _ => pc' | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => 1 @@ -47,7 +47,7 @@ Definition alter_successor (i : instruction) (pc' : node) : instruction := | Iload trap chunk addr args dst _ => Iload trap chunk addr args dst pc' | Istore chunk addr args src _ => Istore chunk addr args src pc' | Ibuiltin ef args res _ => Ibuiltin ef args res pc' - | Icond cond args _ pc2 => Icond cond args pc' pc2 + | Icond cond args _ pc2 expected => Icond cond args pc' pc2 expected | Icall sig ros args res _ => Icall sig ros args res pc' | Itailcall _ _ _ | Ijumptable _ _ diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 2506bcc8..75fed25f 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -1651,9 +1651,9 @@ Section INJECTOR. destruct SKIP as [trs' [MATCH PLUS]]. econstructor; split. * eapply Smallstep.plus_left. - ** apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot). + ** apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot) (predb := predb). exact ALTER. - replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. simpl. reflexivity. ** apply Smallstep.plus_star. @@ -1669,28 +1669,28 @@ Section INJECTOR. destruct SKIP as [trs' [MATCH PLUS]]. econstructor; split. * eapply Smallstep.plus_one. - apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot). + apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := pc_inj) (ifnot := ifnot) (predb := predb). exact ALTER. - replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. simpl. reflexivity. * simpl. constructor; auto. + destruct b eqn:B. * econstructor; split. ** eapply Smallstep.plus_one. - apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot). + apply exec_Icond with (b := true) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot) (predb := predb). *** rewrite transf_function_preserves with (f:=f); eauto. eapply max_pc_function_sound; eauto. - *** replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + *** replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. *** reflexivity. ** constructor; auto. * econstructor; split. ** eapply Smallstep.plus_one. - apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot). + apply exec_Icond with (b := false) (cond := cond) (args := args) (ifso := ifso) (ifnot := ifnot) (predb := predb). *** rewrite transf_function_preserves with (f:=f); eauto. eapply max_pc_function_sound; eauto. - *** replace args with (instr_uses (Icond cond args ifso ifnot)) by reflexivity. + *** replace args with (instr_uses (Icond cond args ifso ifnot predb)) by reflexivity. rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. *** reflexivity. ** constructor; auto. -- cgit From 931b424732474cef10858af4959af6f53a082581 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 20:34:23 +0200 Subject: begin HashedMaps --- lib/HashedMap.v | 332 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 332 insertions(+) create mode 100644 lib/HashedMap.v diff --git a/lib/HashedMap.v b/lib/HashedMap.v new file mode 100644 index 00000000..baeb524c --- /dev/null +++ b/lib/HashedMap.v @@ -0,0 +1,332 @@ +Require Import ZArith. +Require Import Bool. +Require Import List. +Require Coq.Logic.Eqdep_dec. + +(* begin from Maps *) +Fixpoint prev_append (i j: positive) {struct i} : positive := + match i with + | xH => j + | xI i' => prev_append i' (xI j) + | xO i' => prev_append i' (xO j) + end. + +Definition prev (i: positive) : positive := + prev_append i xH. + +Lemma prev_append_prev i j: + prev (prev_append i j) = prev_append j i. +Proof. + revert j. unfold prev. + induction i as [i IH|i IH|]. 3: reflexivity. + intros j. simpl. rewrite IH. reflexivity. + intros j. simpl. rewrite IH. reflexivity. +Qed. + +Lemma prev_involutive i : + prev (prev i) = i. +Proof (prev_append_prev i xH). + +Lemma prev_append_inj i j j' : + prev_append i j = prev_append i j' -> j = j'. +Proof. + revert j j'. + induction i as [i Hi|i Hi|]; intros j j' H; auto; + specialize (Hi _ _ H); congruence. +Qed. + +(* end from Maps *) + +Lemma orb_idem: forall b, orb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_idem: forall b, andb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_negb_false: forall b, andb b (negb b) = false. +Proof. + destruct b; reflexivity. +Qed. + +Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false : pmap. + +Parameter T : Type. +Parameter T_eq_dec : forall (x y : T), {x = y} + {x <> y}. + +Inductive pmap : Type := +| Empty : pmap +| Node : pmap -> option T -> pmap -> pmap. +Definition empty := Empty. + +Definition is_empty x := + match x with + | Empty => true + | Node _ _ _ => false + end. + +Definition is_some (x : option T) := + match x with + | Some _ => true + | None => false + end. + +Fixpoint wf x := + match x with + | Empty => true + | Node b0 f b1 => + (wf b0) && (wf b1) && + ((negb (is_empty b0)) || (is_some f) || (negb (is_empty b1))) + end. + +Definition iswf x := (wf x)=true. + +Lemma empty_wf : iswf empty. +Proof. + reflexivity. +Qed. + +Definition pmap_eq : + forall s s': pmap, { s=s' } + { s <> s' }. +Proof. + generalize T_eq_dec. + induction s; destruct s'; repeat decide equality. +Qed. + +Fixpoint get (i : positive) (s : pmap) {struct i} : option T := + match s with + | Empty => None + | Node b0 f b1 => + match i with + | xH => f + | xO ii => get ii b0 + | xI ii => get ii b1 + end + end. + +Lemma gempty : + forall i : positive, + get i Empty = None. +Proof. + destruct i; simpl; reflexivity. +Qed. + +Hint Resolve gempty : pmap. +Hint Rewrite gempty : pmap. + +Definition node (b0 : pmap) (f : option T) (b1 : pmap) : pmap := + match b0, f, b1 with + | Empty, None, Empty => Empty + | _, _, _ => Node b0 f b1 + end. + +Lemma wf_node : + forall b0 f b1, + iswf b0 -> iswf b1 -> iswf (node b0 f b1). +Proof. + destruct b0; destruct f; destruct b1; simpl. + all: unfold iswf; simpl; intros; trivial. + all: autorewrite with pmap; trivial. + all: rewrite H. + all: rewrite H0. + all: reflexivity. +Qed. + +Hint Resolve wf_node: pmap. + +Lemma gnode : + forall b0 f b1 i, + get i (node b0 f b1) = + get i (Node b0 f b1). +Proof. + destruct b0; simpl; trivial. + destruct f; simpl; trivial. + destruct b1; simpl; trivial. + intro. + rewrite gempty. + destruct i; simpl; trivial. + all: symmetry; apply gempty. +Qed. + +Hint Rewrite gnode : pmap. + +Fixpoint set (i : positive) (j : T) (s : pmap) {struct i} : pmap := + match s with + | Empty => + match i with + | xH => Node Empty (Some j) Empty + | xO ii => Node (set ii j Empty) None Empty + | xI ii => Node Empty None (set ii j Empty) + end + | Node b0 f b1 => + match i with + | xH => Node b0 (Some j) b1 + | xO ii => Node (set ii j b0) f b1 + | xI ii => Node b0 f (set ii j b1) + end + end. + +Lemma set_nonempty: + forall i j s, is_empty (set i j s) = false. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Hint Rewrite set_nonempty : pmap. +Hint Resolve set_nonempty : pmap. + +Lemma wf_set: + forall i j s, (iswf s) -> (iswf (set i j s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: autorewrite with pmap; simpl; trivial. + 1,3: auto with pmap. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: intuition. +Qed. + +Hint Resolve wf_set : pset. + +Theorem gss : + forall (i : positive) (j : T) (s : pmap), + get i (set i j s) = Some j. +Proof. + induction i; destruct s; simpl; auto. +Qed. + +Hint Resolve gss : pmap. +Hint Rewrite gss : pmap. + +Theorem gso : + forall (i j : positive) (k : T) (s : pmap), + i <> j -> + get j (set i k s) = get j s. +Proof. + induction i; destruct j; destruct s; simpl; intro; auto with pmap. + 5, 6: congruence. + all: rewrite IHi by congruence. + all: trivial. + all: apply gempty. +Qed. + +Hint Resolve gso : pmap. + +Fixpoint remove (i : positive) (s : pmap) { struct i } : pmap := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 None b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => node (remove ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 f (remove ii b1) + end + end. + +Lemma wf_remove : + forall i s, (iswf s) -> (iswf (remove i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: apply wf_node. + all: intuition. + all: apply IHi. + all: assumption. +Qed. + +Fixpoint remove_noncanon (i : positive) (s : pmap) { struct i } : pmap := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 None b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node (remove_noncanon ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 f (remove_noncanon ii b1) + end + end. + +Lemma remove_noncanon_same: + forall i j s, (get j (remove i s)) = (get j (remove_noncanon i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: rewrite gnode. + 3: reflexivity. + all: destruct j; simpl; trivial. +Qed. + +Lemma remove_empty : + forall i, remove i Empty = Empty. +Proof. + induction i; simpl; trivial. +Qed. + +Hint Rewrite remove_empty : pmap. +Hint Resolve remove_empty : pmap. + +Lemma gremove_noncanon_s : + forall i : positive, + forall s : pmap, + get i (remove_noncanon i s) = None. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Theorem grs : + forall i : positive, + forall s : pmap, + get i (remove i s) = None. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_s. +Qed. + +Hint Resolve grs : pmap. +Hint Rewrite grs : pmap. + +Lemma gremove_noncanon_o : + forall i j : positive, + forall s : pmap, + i<>j -> + get j (remove_noncanon i s) = get j s. +Proof. + induction i; destruct j; destruct s; simpl; intro; trivial. + 1, 2: rewrite IHi by congruence. + 1, 2: reflexivity. + congruence. +Qed. + +Theorem gro : + forall (i j : positive) (s : pmap), + i<>j -> + get j (remove i s) = get j s. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_o. + assumption. +Qed. + +Hint Resolve gro : pmap. -- cgit From 0575b91176870ac5d1c5692d19059a12e4d9667c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 22:23:11 +0200 Subject: gmap2_idem_Empty --- lib/HashedMap.v | 54 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/lib/HashedMap.v b/lib/HashedMap.v index baeb524c..1baff1a1 100644 --- a/lib/HashedMap.v +++ b/lib/HashedMap.v @@ -330,3 +330,57 @@ Proof. Qed. Hint Resolve gro : pmap. + +Section MAP2_IDEM. + Variable f : option T -> option T -> option T. + Hypothesis f_idem : forall x, f x x = x. + + Fixpoint map2_idem_Empty (b : pmap) := + match b with + | Empty => Empty + | Node b0 bf b1 => + node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1) + end. + + Lemma gmap2_idem_Empty: forall i b, + get i (map2_idem_Empty b) = f None (get i b). + Proof. + induction i; destruct b as [ | b0 bf b1]; intros; simpl in *. + all: try congruence. + - replace + (match node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1) with + | Empty => None + | Node _ _ c1 => get i c1 + end) + with (get (xI i) (node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1))). + + rewrite gnode. + simpl. apply IHi. + + destruct node; auto with pmap. + - replace + (match node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1) with + | Empty => None + | Node c0 _ _ => get i c0 + end) + with (get (xO i) (node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1))). + + rewrite gnode. + simpl. apply IHi. + + destruct node; auto with pmap. + - change (match node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1) with + | Empty => None + | Node _ cf _ => cf + end) with (get xH (node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1))). + rewrite gnode. reflexivity. + Qed. + + Fixpoint map2_idem (a b : pmap) := + match a with + | Empty => map2_idem_Empty b + | (Node a0 af a1) => + match b with + | (Node b0 bf b1) => + node (map2_idem a0 b0) (f af bf) (map2_idem a1 b1) + | Empty => + node (map2_idem a0 Empty) (f af None) (map2_idem a1 Empty) + end + end. + -- cgit From 48ba6c006c966227b8a0b96ed48203af36835615 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 22:54:21 +0200 Subject: gmap2_idem --- lib/HashedMap.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/lib/HashedMap.v b/lib/HashedMap.v index 1baff1a1..21f35af8 100644 --- a/lib/HashedMap.v +++ b/lib/HashedMap.v @@ -384,3 +384,19 @@ Section MAP2_IDEM. end end. + Lemma gmap2_idem: forall a b i, + get i (map2_idem a b) = f (get i a) (get i b). + Proof. + induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. + { rewrite gmap2_idem_Empty. + rewrite gempty. + reflexivity. } + destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. + - destruct i; simpl. + + rewrite IHa1. rewrite gempty. + reflexivity. + + rewrite IHa0. rewrite gempty. + reflexivity. + + reflexivity. + - destruct i; simpl; congruence. + Qed. -- cgit From 33927b62b2d443ae3989b9565dac51070d9d8a86 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 23:14:50 +0200 Subject: gmap2_idem --- lib/HashedMap.v | 176 +++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 111 insertions(+), 65 deletions(-) diff --git a/lib/HashedMap.v b/lib/HashedMap.v index 21f35af8..df724867 100644 --- a/lib/HashedMap.v +++ b/lib/HashedMap.v @@ -331,72 +331,118 @@ Qed. Hint Resolve gro : pmap. -Section MAP2_IDEM. +Section MAP2. + Variable f : option T -> option T -> option T. - Hypothesis f_idem : forall x, f x x = x. - Fixpoint map2_idem_Empty (b : pmap) := - match b with - | Empty => Empty - | Node b0 bf b1 => - node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1) - end. - - Lemma gmap2_idem_Empty: forall i b, - get i (map2_idem_Empty b) = f None (get i b). - Proof. - induction i; destruct b as [ | b0 bf b1]; intros; simpl in *. - all: try congruence. - - replace - (match node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1) with - | Empty => None - | Node _ _ c1 => get i c1 - end) - with (get (xI i) (node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1))). - + rewrite gnode. - simpl. apply IHi. - + destruct node; auto with pmap. - - replace - (match node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1) with - | Empty => None - | Node c0 _ _ => get i c0 - end) - with (get (xO i) (node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1))). - + rewrite gnode. - simpl. apply IHi. - + destruct node; auto with pmap. - - change (match node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1) with - | Empty => None - | Node _ cf _ => cf - end) with (get xH (node (map2_idem_Empty b0) (f None bf) (map2_idem_Empty b1))). - rewrite gnode. reflexivity. - Qed. - - Fixpoint map2_idem (a b : pmap) := - match a with - | Empty => map2_idem_Empty b - | (Node a0 af a1) => + Section NONE_NONE. + Hypothesis f_none_none : f None None = None. + + Fixpoint map2_Empty (b : pmap) := match b with - | (Node b0 bf b1) => - node (map2_idem a0 b0) (f af bf) (map2_idem a1 b1) - | Empty => - node (map2_idem a0 Empty) (f af None) (map2_idem a1 Empty) - end - end. + | Empty => Empty + | Node b0 bf b1 => + node (map2_Empty b0) (f None bf) (map2_Empty b1) + end. + + Lemma gmap2_Empty: forall i b, + get i (map2_Empty b) = f None (get i b). + Proof. + induction i; destruct b as [ | b0 bf b1]; intros; simpl in *. + all: try congruence. + - replace + (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node _ _ c1 => get i c1 + end) + with (get (xI i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + + rewrite gnode. + simpl. apply IHi. + + destruct node; auto with pmap. + - replace + (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node c0 _ _ => get i c0 + end) + with (get (xO i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + + rewrite gnode. + simpl. apply IHi. + + destruct node; auto with pmap. + - change (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node _ cf _ => cf + end) with (get xH (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + rewrite gnode. reflexivity. + Qed. + + Fixpoint map2 (a b : pmap) := + match a with + | Empty => map2_Empty b + | (Node a0 af a1) => + match b with + | (Node b0 bf b1) => + node (map2 a0 b0) (f af bf) (map2 a1 b1) + | Empty => + node (map2 a0 Empty) (f af None) (map2 a1 Empty) + end + end. - Lemma gmap2_idem: forall a b i, - get i (map2_idem a b) = f (get i a) (get i b). - Proof. - induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. - { rewrite gmap2_idem_Empty. - rewrite gempty. - reflexivity. } - destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. - - destruct i; simpl. - + rewrite IHa1. rewrite gempty. - reflexivity. - + rewrite IHa0. rewrite gempty. - reflexivity. - + reflexivity. - - destruct i; simpl; congruence. - Qed. + Lemma gmap2: forall a b i, + get i (map2 a b) = f (get i a) (get i b). + Proof. + induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. + { rewrite gmap2_Empty. + rewrite gempty. + reflexivity. } + destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. + - destruct i; simpl. + + rewrite IHa1. rewrite gempty. + reflexivity. + + rewrite IHa0. rewrite gempty. + reflexivity. + + reflexivity. + - destruct i; simpl; congruence. + Qed. + End NONE_NONE. + + Section IDEM. + Hypothesis f_idem : forall x, f x x = x. + + Fixpoint map2_idem (a b : pmap) := + if pmap_eq a b then a else + match a with + | Empty => map2_Empty b + | (Node a0 af a1) => + match b with + | (Node b0 bf b1) => + node (map2_idem a0 b0) (f af bf) (map2_idem a1 b1) + | Empty => + node (map2_idem a0 Empty) (f af None) (map2_idem a1 Empty) + end + end. + + Lemma gmap2_idem: forall a b i, + get i (map2_idem a b) = f (get i a) (get i b). + Proof. + induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. + { destruct pmap_eq. + - subst b. rewrite gempty. congruence. + - rewrite gempty. + rewrite gmap2_Empty by congruence. + reflexivity. + } + destruct pmap_eq. + { subst b. + congruence. + } + destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. + - destruct i; simpl. + + rewrite IHa1. rewrite gempty. + reflexivity. + + rewrite IHa0. rewrite gempty. + reflexivity. + + reflexivity. + - destruct i; simpl; congruence. + Qed. + End IDEM. +End MAP2. -- cgit From 540fbd2e6d63c1be0dd520499132c134f5b0f8b3 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 23:18:26 +0200 Subject: moved to extra --- backend/LICMaux.ml | 25 +-- lib/HashedMap.v | 448 -------------------------------------------------- lib/extra/HashedMap.v | 448 ++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 457 insertions(+), 464 deletions(-) delete mode 100644 lib/HashedMap.v create mode 100644 lib/extra/HashedMap.v diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 3f7d61b1..96214054 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -1,31 +1,24 @@ open RTL;; open Camlcoq;; open Maps;; -open Integers;; type reg = P.t;; -module IntSet = Set.Make(struct type t=int let compare = (-) end);; - -let loop_headers (f : coq_function) = - PTree.fold (fun (already : IntSet.t) - (coq_pc : node) (instr : instruction) -> - let pc = P.to_int coq_pc in - List.fold_left (fun (already : IntSet.t) (coq_pc' : node) -> - let pc' = P.to_int coq_pc' in - if pc' >= pc - then IntSet.add pc' already - else already) already (successors_instr instr)) - f.fn_code IntSet.empty;; +let loop_headers (f : coq_function) : RTL.node list = + List.map fst (List.filter snd (PTree.elements (Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint)));; let print_loop_headers f = print_endline "Loop headers"; - IntSet.iter - (fun i -> Printf.printf "%d " i) + List.iter + (fun i -> Printf.printf "%d " (P.to_int i)) (loop_headers f); print_newline ();; let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg): - (Inject.inj_instr list) PTree.t = + (Inject.inj_instr list) PTree.t = + let _ = print_loop_headers f in + PTree.empty;; +(* let max_reg = P.to_int coq_max_reg in PTree.set coq_max_pc [Inject.INJload(AST.Mint32, (Op.Aindexed (Ptrofs.of_int (Z.of_sint 0))), [P.of_int 1], P.of_int (max_reg+1))] PTree.empty;; + *) diff --git a/lib/HashedMap.v b/lib/HashedMap.v deleted file mode 100644 index df724867..00000000 --- a/lib/HashedMap.v +++ /dev/null @@ -1,448 +0,0 @@ -Require Import ZArith. -Require Import Bool. -Require Import List. -Require Coq.Logic.Eqdep_dec. - -(* begin from Maps *) -Fixpoint prev_append (i j: positive) {struct i} : positive := - match i with - | xH => j - | xI i' => prev_append i' (xI j) - | xO i' => prev_append i' (xO j) - end. - -Definition prev (i: positive) : positive := - prev_append i xH. - -Lemma prev_append_prev i j: - prev (prev_append i j) = prev_append j i. -Proof. - revert j. unfold prev. - induction i as [i IH|i IH|]. 3: reflexivity. - intros j. simpl. rewrite IH. reflexivity. - intros j. simpl. rewrite IH. reflexivity. -Qed. - -Lemma prev_involutive i : - prev (prev i) = i. -Proof (prev_append_prev i xH). - -Lemma prev_append_inj i j j' : - prev_append i j = prev_append i j' -> j = j'. -Proof. - revert j j'. - induction i as [i Hi|i Hi|]; intros j j' H; auto; - specialize (Hi _ _ H); congruence. -Qed. - -(* end from Maps *) - -Lemma orb_idem: forall b, orb b b = b. -Proof. - destruct b; reflexivity. -Qed. - -Lemma andb_idem: forall b, andb b b = b. -Proof. - destruct b; reflexivity. -Qed. - -Lemma andb_negb_false: forall b, andb b (negb b) = false. -Proof. - destruct b; reflexivity. -Qed. - -Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false : pmap. - -Parameter T : Type. -Parameter T_eq_dec : forall (x y : T), {x = y} + {x <> y}. - -Inductive pmap : Type := -| Empty : pmap -| Node : pmap -> option T -> pmap -> pmap. -Definition empty := Empty. - -Definition is_empty x := - match x with - | Empty => true - | Node _ _ _ => false - end. - -Definition is_some (x : option T) := - match x with - | Some _ => true - | None => false - end. - -Fixpoint wf x := - match x with - | Empty => true - | Node b0 f b1 => - (wf b0) && (wf b1) && - ((negb (is_empty b0)) || (is_some f) || (negb (is_empty b1))) - end. - -Definition iswf x := (wf x)=true. - -Lemma empty_wf : iswf empty. -Proof. - reflexivity. -Qed. - -Definition pmap_eq : - forall s s': pmap, { s=s' } + { s <> s' }. -Proof. - generalize T_eq_dec. - induction s; destruct s'; repeat decide equality. -Qed. - -Fixpoint get (i : positive) (s : pmap) {struct i} : option T := - match s with - | Empty => None - | Node b0 f b1 => - match i with - | xH => f - | xO ii => get ii b0 - | xI ii => get ii b1 - end - end. - -Lemma gempty : - forall i : positive, - get i Empty = None. -Proof. - destruct i; simpl; reflexivity. -Qed. - -Hint Resolve gempty : pmap. -Hint Rewrite gempty : pmap. - -Definition node (b0 : pmap) (f : option T) (b1 : pmap) : pmap := - match b0, f, b1 with - | Empty, None, Empty => Empty - | _, _, _ => Node b0 f b1 - end. - -Lemma wf_node : - forall b0 f b1, - iswf b0 -> iswf b1 -> iswf (node b0 f b1). -Proof. - destruct b0; destruct f; destruct b1; simpl. - all: unfold iswf; simpl; intros; trivial. - all: autorewrite with pmap; trivial. - all: rewrite H. - all: rewrite H0. - all: reflexivity. -Qed. - -Hint Resolve wf_node: pmap. - -Lemma gnode : - forall b0 f b1 i, - get i (node b0 f b1) = - get i (Node b0 f b1). -Proof. - destruct b0; simpl; trivial. - destruct f; simpl; trivial. - destruct b1; simpl; trivial. - intro. - rewrite gempty. - destruct i; simpl; trivial. - all: symmetry; apply gempty. -Qed. - -Hint Rewrite gnode : pmap. - -Fixpoint set (i : positive) (j : T) (s : pmap) {struct i} : pmap := - match s with - | Empty => - match i with - | xH => Node Empty (Some j) Empty - | xO ii => Node (set ii j Empty) None Empty - | xI ii => Node Empty None (set ii j Empty) - end - | Node b0 f b1 => - match i with - | xH => Node b0 (Some j) b1 - | xO ii => Node (set ii j b0) f b1 - | xI ii => Node b0 f (set ii j b1) - end - end. - -Lemma set_nonempty: - forall i j s, is_empty (set i j s) = false. -Proof. - induction i; destruct s; simpl; trivial. -Qed. - -Hint Rewrite set_nonempty : pmap. -Hint Resolve set_nonempty : pmap. - -Lemma wf_set: - forall i j s, (iswf s) -> (iswf (set i j s)). -Proof. - induction i; destruct s; simpl; trivial. - all: unfold iswf in *; simpl. - all: autorewrite with pmap; simpl; trivial. - 1,3: auto with pmap. - all: intro Z. - all: repeat rewrite andb_true_iff in Z. - all: intuition. -Qed. - -Hint Resolve wf_set : pset. - -Theorem gss : - forall (i : positive) (j : T) (s : pmap), - get i (set i j s) = Some j. -Proof. - induction i; destruct s; simpl; auto. -Qed. - -Hint Resolve gss : pmap. -Hint Rewrite gss : pmap. - -Theorem gso : - forall (i j : positive) (k : T) (s : pmap), - i <> j -> - get j (set i k s) = get j s. -Proof. - induction i; destruct j; destruct s; simpl; intro; auto with pmap. - 5, 6: congruence. - all: rewrite IHi by congruence. - all: trivial. - all: apply gempty. -Qed. - -Hint Resolve gso : pmap. - -Fixpoint remove (i : positive) (s : pmap) { struct i } : pmap := - match i with - | xH => - match s with - | Empty => Empty - | Node b0 f b1 => node b0 None b1 - end - | xO ii => - match s with - | Empty => Empty - | Node b0 f b1 => node (remove ii b0) f b1 - end - | xI ii => - match s with - | Empty => Empty - | Node b0 f b1 => node b0 f (remove ii b1) - end - end. - -Lemma wf_remove : - forall i s, (iswf s) -> (iswf (remove i s)). -Proof. - induction i; destruct s; simpl; trivial. - all: unfold iswf in *; simpl. - all: intro Z. - all: repeat rewrite andb_true_iff in Z. - all: apply wf_node. - all: intuition. - all: apply IHi. - all: assumption. -Qed. - -Fixpoint remove_noncanon (i : positive) (s : pmap) { struct i } : pmap := - match i with - | xH => - match s with - | Empty => Empty - | Node b0 f b1 => Node b0 None b1 - end - | xO ii => - match s with - | Empty => Empty - | Node b0 f b1 => Node (remove_noncanon ii b0) f b1 - end - | xI ii => - match s with - | Empty => Empty - | Node b0 f b1 => Node b0 f (remove_noncanon ii b1) - end - end. - -Lemma remove_noncanon_same: - forall i j s, (get j (remove i s)) = (get j (remove_noncanon i s)). -Proof. - induction i; destruct s; simpl; trivial. - all: rewrite gnode. - 3: reflexivity. - all: destruct j; simpl; trivial. -Qed. - -Lemma remove_empty : - forall i, remove i Empty = Empty. -Proof. - induction i; simpl; trivial. -Qed. - -Hint Rewrite remove_empty : pmap. -Hint Resolve remove_empty : pmap. - -Lemma gremove_noncanon_s : - forall i : positive, - forall s : pmap, - get i (remove_noncanon i s) = None. -Proof. - induction i; destruct s; simpl; trivial. -Qed. - -Theorem grs : - forall i : positive, - forall s : pmap, - get i (remove i s) = None. -Proof. - intros. - rewrite remove_noncanon_same. - apply gremove_noncanon_s. -Qed. - -Hint Resolve grs : pmap. -Hint Rewrite grs : pmap. - -Lemma gremove_noncanon_o : - forall i j : positive, - forall s : pmap, - i<>j -> - get j (remove_noncanon i s) = get j s. -Proof. - induction i; destruct j; destruct s; simpl; intro; trivial. - 1, 2: rewrite IHi by congruence. - 1, 2: reflexivity. - congruence. -Qed. - -Theorem gro : - forall (i j : positive) (s : pmap), - i<>j -> - get j (remove i s) = get j s. -Proof. - intros. - rewrite remove_noncanon_same. - apply gremove_noncanon_o. - assumption. -Qed. - -Hint Resolve gro : pmap. - -Section MAP2. - - Variable f : option T -> option T -> option T. - - Section NONE_NONE. - Hypothesis f_none_none : f None None = None. - - Fixpoint map2_Empty (b : pmap) := - match b with - | Empty => Empty - | Node b0 bf b1 => - node (map2_Empty b0) (f None bf) (map2_Empty b1) - end. - - Lemma gmap2_Empty: forall i b, - get i (map2_Empty b) = f None (get i b). - Proof. - induction i; destruct b as [ | b0 bf b1]; intros; simpl in *. - all: try congruence. - - replace - (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with - | Empty => None - | Node _ _ c1 => get i c1 - end) - with (get (xI i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))). - + rewrite gnode. - simpl. apply IHi. - + destruct node; auto with pmap. - - replace - (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with - | Empty => None - | Node c0 _ _ => get i c0 - end) - with (get (xO i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))). - + rewrite gnode. - simpl. apply IHi. - + destruct node; auto with pmap. - - change (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with - | Empty => None - | Node _ cf _ => cf - end) with (get xH (node (map2_Empty b0) (f None bf) (map2_Empty b1))). - rewrite gnode. reflexivity. - Qed. - - Fixpoint map2 (a b : pmap) := - match a with - | Empty => map2_Empty b - | (Node a0 af a1) => - match b with - | (Node b0 bf b1) => - node (map2 a0 b0) (f af bf) (map2 a1 b1) - | Empty => - node (map2 a0 Empty) (f af None) (map2 a1 Empty) - end - end. - - Lemma gmap2: forall a b i, - get i (map2 a b) = f (get i a) (get i b). - Proof. - induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. - { rewrite gmap2_Empty. - rewrite gempty. - reflexivity. } - destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. - - destruct i; simpl. - + rewrite IHa1. rewrite gempty. - reflexivity. - + rewrite IHa0. rewrite gempty. - reflexivity. - + reflexivity. - - destruct i; simpl; congruence. - Qed. - End NONE_NONE. - - Section IDEM. - Hypothesis f_idem : forall x, f x x = x. - - Fixpoint map2_idem (a b : pmap) := - if pmap_eq a b then a else - match a with - | Empty => map2_Empty b - | (Node a0 af a1) => - match b with - | (Node b0 bf b1) => - node (map2_idem a0 b0) (f af bf) (map2_idem a1 b1) - | Empty => - node (map2_idem a0 Empty) (f af None) (map2_idem a1 Empty) - end - end. - - Lemma gmap2_idem: forall a b i, - get i (map2_idem a b) = f (get i a) (get i b). - Proof. - induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. - { destruct pmap_eq. - - subst b. rewrite gempty. congruence. - - rewrite gempty. - rewrite gmap2_Empty by congruence. - reflexivity. - } - destruct pmap_eq. - { subst b. - congruence. - } - destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. - - destruct i; simpl. - + rewrite IHa1. rewrite gempty. - reflexivity. - + rewrite IHa0. rewrite gempty. - reflexivity. - + reflexivity. - - destruct i; simpl; congruence. - Qed. - End IDEM. -End MAP2. diff --git a/lib/extra/HashedMap.v b/lib/extra/HashedMap.v new file mode 100644 index 00000000..df724867 --- /dev/null +++ b/lib/extra/HashedMap.v @@ -0,0 +1,448 @@ +Require Import ZArith. +Require Import Bool. +Require Import List. +Require Coq.Logic.Eqdep_dec. + +(* begin from Maps *) +Fixpoint prev_append (i j: positive) {struct i} : positive := + match i with + | xH => j + | xI i' => prev_append i' (xI j) + | xO i' => prev_append i' (xO j) + end. + +Definition prev (i: positive) : positive := + prev_append i xH. + +Lemma prev_append_prev i j: + prev (prev_append i j) = prev_append j i. +Proof. + revert j. unfold prev. + induction i as [i IH|i IH|]. 3: reflexivity. + intros j. simpl. rewrite IH. reflexivity. + intros j. simpl. rewrite IH. reflexivity. +Qed. + +Lemma prev_involutive i : + prev (prev i) = i. +Proof (prev_append_prev i xH). + +Lemma prev_append_inj i j j' : + prev_append i j = prev_append i j' -> j = j'. +Proof. + revert j j'. + induction i as [i Hi|i Hi|]; intros j j' H; auto; + specialize (Hi _ _ H); congruence. +Qed. + +(* end from Maps *) + +Lemma orb_idem: forall b, orb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_idem: forall b, andb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_negb_false: forall b, andb b (negb b) = false. +Proof. + destruct b; reflexivity. +Qed. + +Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false : pmap. + +Parameter T : Type. +Parameter T_eq_dec : forall (x y : T), {x = y} + {x <> y}. + +Inductive pmap : Type := +| Empty : pmap +| Node : pmap -> option T -> pmap -> pmap. +Definition empty := Empty. + +Definition is_empty x := + match x with + | Empty => true + | Node _ _ _ => false + end. + +Definition is_some (x : option T) := + match x with + | Some _ => true + | None => false + end. + +Fixpoint wf x := + match x with + | Empty => true + | Node b0 f b1 => + (wf b0) && (wf b1) && + ((negb (is_empty b0)) || (is_some f) || (negb (is_empty b1))) + end. + +Definition iswf x := (wf x)=true. + +Lemma empty_wf : iswf empty. +Proof. + reflexivity. +Qed. + +Definition pmap_eq : + forall s s': pmap, { s=s' } + { s <> s' }. +Proof. + generalize T_eq_dec. + induction s; destruct s'; repeat decide equality. +Qed. + +Fixpoint get (i : positive) (s : pmap) {struct i} : option T := + match s with + | Empty => None + | Node b0 f b1 => + match i with + | xH => f + | xO ii => get ii b0 + | xI ii => get ii b1 + end + end. + +Lemma gempty : + forall i : positive, + get i Empty = None. +Proof. + destruct i; simpl; reflexivity. +Qed. + +Hint Resolve gempty : pmap. +Hint Rewrite gempty : pmap. + +Definition node (b0 : pmap) (f : option T) (b1 : pmap) : pmap := + match b0, f, b1 with + | Empty, None, Empty => Empty + | _, _, _ => Node b0 f b1 + end. + +Lemma wf_node : + forall b0 f b1, + iswf b0 -> iswf b1 -> iswf (node b0 f b1). +Proof. + destruct b0; destruct f; destruct b1; simpl. + all: unfold iswf; simpl; intros; trivial. + all: autorewrite with pmap; trivial. + all: rewrite H. + all: rewrite H0. + all: reflexivity. +Qed. + +Hint Resolve wf_node: pmap. + +Lemma gnode : + forall b0 f b1 i, + get i (node b0 f b1) = + get i (Node b0 f b1). +Proof. + destruct b0; simpl; trivial. + destruct f; simpl; trivial. + destruct b1; simpl; trivial. + intro. + rewrite gempty. + destruct i; simpl; trivial. + all: symmetry; apply gempty. +Qed. + +Hint Rewrite gnode : pmap. + +Fixpoint set (i : positive) (j : T) (s : pmap) {struct i} : pmap := + match s with + | Empty => + match i with + | xH => Node Empty (Some j) Empty + | xO ii => Node (set ii j Empty) None Empty + | xI ii => Node Empty None (set ii j Empty) + end + | Node b0 f b1 => + match i with + | xH => Node b0 (Some j) b1 + | xO ii => Node (set ii j b0) f b1 + | xI ii => Node b0 f (set ii j b1) + end + end. + +Lemma set_nonempty: + forall i j s, is_empty (set i j s) = false. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Hint Rewrite set_nonempty : pmap. +Hint Resolve set_nonempty : pmap. + +Lemma wf_set: + forall i j s, (iswf s) -> (iswf (set i j s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: autorewrite with pmap; simpl; trivial. + 1,3: auto with pmap. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: intuition. +Qed. + +Hint Resolve wf_set : pset. + +Theorem gss : + forall (i : positive) (j : T) (s : pmap), + get i (set i j s) = Some j. +Proof. + induction i; destruct s; simpl; auto. +Qed. + +Hint Resolve gss : pmap. +Hint Rewrite gss : pmap. + +Theorem gso : + forall (i j : positive) (k : T) (s : pmap), + i <> j -> + get j (set i k s) = get j s. +Proof. + induction i; destruct j; destruct s; simpl; intro; auto with pmap. + 5, 6: congruence. + all: rewrite IHi by congruence. + all: trivial. + all: apply gempty. +Qed. + +Hint Resolve gso : pmap. + +Fixpoint remove (i : positive) (s : pmap) { struct i } : pmap := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 None b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => node (remove ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 f (remove ii b1) + end + end. + +Lemma wf_remove : + forall i s, (iswf s) -> (iswf (remove i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: apply wf_node. + all: intuition. + all: apply IHi. + all: assumption. +Qed. + +Fixpoint remove_noncanon (i : positive) (s : pmap) { struct i } : pmap := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 None b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node (remove_noncanon ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 f (remove_noncanon ii b1) + end + end. + +Lemma remove_noncanon_same: + forall i j s, (get j (remove i s)) = (get j (remove_noncanon i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: rewrite gnode. + 3: reflexivity. + all: destruct j; simpl; trivial. +Qed. + +Lemma remove_empty : + forall i, remove i Empty = Empty. +Proof. + induction i; simpl; trivial. +Qed. + +Hint Rewrite remove_empty : pmap. +Hint Resolve remove_empty : pmap. + +Lemma gremove_noncanon_s : + forall i : positive, + forall s : pmap, + get i (remove_noncanon i s) = None. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Theorem grs : + forall i : positive, + forall s : pmap, + get i (remove i s) = None. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_s. +Qed. + +Hint Resolve grs : pmap. +Hint Rewrite grs : pmap. + +Lemma gremove_noncanon_o : + forall i j : positive, + forall s : pmap, + i<>j -> + get j (remove_noncanon i s) = get j s. +Proof. + induction i; destruct j; destruct s; simpl; intro; trivial. + 1, 2: rewrite IHi by congruence. + 1, 2: reflexivity. + congruence. +Qed. + +Theorem gro : + forall (i j : positive) (s : pmap), + i<>j -> + get j (remove i s) = get j s. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_o. + assumption. +Qed. + +Hint Resolve gro : pmap. + +Section MAP2. + + Variable f : option T -> option T -> option T. + + Section NONE_NONE. + Hypothesis f_none_none : f None None = None. + + Fixpoint map2_Empty (b : pmap) := + match b with + | Empty => Empty + | Node b0 bf b1 => + node (map2_Empty b0) (f None bf) (map2_Empty b1) + end. + + Lemma gmap2_Empty: forall i b, + get i (map2_Empty b) = f None (get i b). + Proof. + induction i; destruct b as [ | b0 bf b1]; intros; simpl in *. + all: try congruence. + - replace + (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node _ _ c1 => get i c1 + end) + with (get (xI i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + + rewrite gnode. + simpl. apply IHi. + + destruct node; auto with pmap. + - replace + (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node c0 _ _ => get i c0 + end) + with (get (xO i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + + rewrite gnode. + simpl. apply IHi. + + destruct node; auto with pmap. + - change (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node _ cf _ => cf + end) with (get xH (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + rewrite gnode. reflexivity. + Qed. + + Fixpoint map2 (a b : pmap) := + match a with + | Empty => map2_Empty b + | (Node a0 af a1) => + match b with + | (Node b0 bf b1) => + node (map2 a0 b0) (f af bf) (map2 a1 b1) + | Empty => + node (map2 a0 Empty) (f af None) (map2 a1 Empty) + end + end. + + Lemma gmap2: forall a b i, + get i (map2 a b) = f (get i a) (get i b). + Proof. + induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. + { rewrite gmap2_Empty. + rewrite gempty. + reflexivity. } + destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. + - destruct i; simpl. + + rewrite IHa1. rewrite gempty. + reflexivity. + + rewrite IHa0. rewrite gempty. + reflexivity. + + reflexivity. + - destruct i; simpl; congruence. + Qed. + End NONE_NONE. + + Section IDEM. + Hypothesis f_idem : forall x, f x x = x. + + Fixpoint map2_idem (a b : pmap) := + if pmap_eq a b then a else + match a with + | Empty => map2_Empty b + | (Node a0 af a1) => + match b with + | (Node b0 bf b1) => + node (map2_idem a0 b0) (f af bf) (map2_idem a1 b1) + | Empty => + node (map2_idem a0 Empty) (f af None) (map2_idem a1 Empty) + end + end. + + Lemma gmap2_idem: forall a b i, + get i (map2_idem a b) = f (get i a) (get i b). + Proof. + induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. + { destruct pmap_eq. + - subst b. rewrite gempty. congruence. + - rewrite gempty. + rewrite gmap2_Empty by congruence. + reflexivity. + } + destruct pmap_eq. + { subst b. + congruence. + } + destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. + - destruct i; simpl. + + rewrite IHa1. rewrite gempty. + reflexivity. + + rewrite IHa0. rewrite gempty. + reflexivity. + + reflexivity. + - destruct i; simpl; congruence. + Qed. + End IDEM. +End MAP2. -- cgit From 967dbc3b939784ef3246bb5e931a62da26cf51a9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 17 Apr 2020 12:27:48 +0200 Subject: find inner loops --- backend/LICMaux.ml | 58 +++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 57 insertions(+), 1 deletion(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 96214054..82cd74a2 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -1,9 +1,65 @@ open RTL;; open Camlcoq;; open Maps;; +open Kildall;; type reg = P.t;; +module Dominator = + struct + type t = Unreachable | Dominated of int | Multiple + let bot = Unreachable and top = Multiple + let beq a b = + match a, b with + | Unreachable, Unreachable + | Multiple, Multiple -> true + | (Dominated x), (Dominated y) -> x = y + | _ -> false + let lub a b = + match a, b with + | Multiple, _ + | _, Multiple -> Multiple + | Unreachable, x + | x, Unreachable -> x + | (Dominated x), (Dominated y) when x=y -> a + | (Dominated _), (Dominated _) -> Multiple + + let pp oc = function + | Unreachable -> output_string oc "unreachable" + | Multiple -> output_string oc "multiple" + | Dominated x -> Printf.fprintf oc "%d" x;; + end + +module Dominator_Solver = Dataflow_Solver(Dominator)(NodeSetForward) + +let apply_dominator (is_marked : node -> bool) (pc : node) + (before : Dominator.t) : Dominator.t = + match before with + | Dominator.Unreachable -> before + | _ -> + if is_marked pc + then Dominator.Dominated (P.to_int pc) + else before;; + +let dominated_parts (f : coq_function) : Dominator.t PMap.t option = + let headers = Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint in + Dominator_Solver.fixpoint f.fn_code RTL.successors_instr + (apply_dominator (fun pc -> match PTree.get pc headers with + | Some x -> x + | None -> false)) f.fn_entrypoint + Dominator.top;; + +let print_dominated_parts oc f = + match dominated_parts f with + | None -> output_string oc "error\n" + | Some parts -> + List.iter + (fun (pc, instr) -> + Printf.fprintf oc "%d : %a\n" (P.to_int pc) Dominator.pp + (PMap.get pc parts) + ) + (PTree.elements f.fn_code);; + let loop_headers (f : coq_function) : RTL.node list = List.map fst (List.filter snd (PTree.elements (Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint)));; @@ -16,7 +72,7 @@ let print_loop_headers f = let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg): (Inject.inj_instr list) PTree.t = - let _ = print_loop_headers f in + let _ = print_dominated_parts stdout f in PTree.empty;; (* let max_reg = P.to_int coq_max_reg in -- cgit From 871643ce4897ba645d922812a3fb546bdb2f48a4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 18 Apr 2020 11:29:18 +0200 Subject: headers vs dominators --- backend/LICMaux.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 82cd74a2..e236b173 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -41,16 +41,18 @@ let apply_dominator (is_marked : node -> bool) (pc : node) then Dominator.Dominated (P.to_int pc) else before;; -let dominated_parts (f : coq_function) : Dominator.t PMap.t option = +let dominated_parts (f : coq_function) : + (bool PTree.t) * (Dominator.t PMap.t option) = let headers = Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint in - Dominator_Solver.fixpoint f.fn_code RTL.successors_instr + let dominated = Dominator_Solver.fixpoint f.fn_code RTL.successors_instr (apply_dominator (fun pc -> match PTree.get pc headers with | Some x -> x | None -> false)) f.fn_entrypoint - Dominator.top;; + Dominator.top in + (headers, dominated);; let print_dominated_parts oc f = - match dominated_parts f with + match snd (dominated_parts f) with | None -> output_string oc "error\n" | Some parts -> List.iter -- cgit From 669612fc3165cd9898decb7ae5c70f9fb4ef327b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 18 Apr 2020 17:12:42 +0200 Subject: dominated parts --- backend/LICMaux.ml | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index e236b173..52e5077f 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -2,6 +2,7 @@ open RTL;; open Camlcoq;; open Maps;; open Kildall;; +open HashedSet;; type reg = P.t;; @@ -41,7 +42,7 @@ let apply_dominator (is_marked : node -> bool) (pc : node) then Dominator.Dominated (P.to_int pc) else before;; -let dominated_parts (f : coq_function) : +let dominated_parts1 (f : coq_function) : (bool PTree.t) * (Dominator.t PMap.t option) = let headers = Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint in let dominated = Dominator_Solver.fixpoint f.fn_code RTL.successors_instr @@ -51,8 +52,20 @@ let dominated_parts (f : coq_function) : Dominator.top in (headers, dominated);; +(* unfinished *) +let dominated_parts (f : coq_function) : + PSet.t PTree.t = + let (headers, dominated) = dominated_parts1 f in + match dominated with + | None -> failwith "dominated_parts" + | Some dominated -> + PTree.fold (fun before pc flag -> + if flag + then PTree.set pc PSet.empty before + else before) headers PTree.empty;; + let print_dominated_parts oc f = - match snd (dominated_parts f) with + match snd (dominated_parts1 f) with | None -> output_string oc "error\n" | Some parts -> List.iter -- cgit From a352cc3f9b9355e8b823750b9c4e5e1d37606dc4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 18 Apr 2020 19:01:48 +0200 Subject: dominated sets --- backend/LICMaux.ml | 34 ++++++++++++++++++++++++++++++---- 1 file changed, 30 insertions(+), 4 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 52e5077f..66c1530e 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -57,14 +57,40 @@ let dominated_parts (f : coq_function) : PSet.t PTree.t = let (headers, dominated) = dominated_parts1 f in match dominated with - | None -> failwith "dominated_parts" + | None -> failwith "dominated_parts 1" | Some dominated -> - PTree.fold (fun before pc flag -> + let singletons = + PTree.fold (fun before pc flag -> if flag - then PTree.set pc PSet.empty before - else before) headers PTree.empty;; + then PTree.set pc (PSet.add pc PSet.empty) before + else before) headers PTree.empty in + PTree.fold (fun before pc ii -> + match PMap.get pc dominated with + | Dominator.Dominated x -> + let px = P.of_int x in + (match PTree.get px before with + | None -> failwith "dominated_parts 2" + | Some old -> + PTree.set px (PSet.add pc old) before) + | _ -> before) f.fn_code singletons;; + +let pp_pset oc s = + output_string oc "{ "; + let first = ref true in + List.iter (fun x -> + (if !first + then first := false + else output_string oc ", "); + Printf.printf "%d" x) + (List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s))); + output_string oc " }";; let print_dominated_parts oc f = + List.iter (fun (header, nodes) -> + Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) + (PTree.elements (dominated_parts f));; + +let print_dominated_parts1 oc f = match snd (dominated_parts1 f) with | None -> output_string oc "error\n" | Some parts -> -- cgit From 9c68c213d09347316f3bd150dc4c34798c317db1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 18 Apr 2020 21:47:46 +0200 Subject: backward iterator --- backend/LICMaux.ml | 33 +++++++++++++++++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 66c1530e..269d9353 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -53,8 +53,7 @@ let dominated_parts1 (f : coq_function) : (headers, dominated);; (* unfinished *) -let dominated_parts (f : coq_function) : - PSet.t PTree.t = +let dominated_parts (f : coq_function) : PSet.t PTree.t = let (headers, dominated) = dominated_parts1 f in match dominated with | None -> failwith "dominated_parts 1" @@ -74,6 +73,36 @@ let dominated_parts (f : coq_function) : PTree.set px (PSet.add pc old) before) | _ -> before) f.fn_code singletons;; +let graph_traversal (initial_node : P.t) + (successor_iterator : P.t -> (P.t -> unit) -> unit) : PSet.t = + let seen = ref PSet.empty + and stack = Stack.create () in + Stack.push initial_node stack; + while not (Stack.is_empty stack) + do + let vertex = Stack.pop stack in + if not (PSet.contains !seen vertex) + then + begin + seen := PSet.add vertex !seen; + successor_iterator vertex (fun x -> Stack.push x stack) + end + done; + !seen;; + +let filter_dominated_part (predecessors : P.t list PTree.t) + (header : P.t) (dominated_part : PSet.t) = + graph_traversal header + (fun (vertex : P.t) (f : P.t -> unit) -> + match PTree.get vertex predecessors with + | None -> () + | Some l -> + List.iter + (fun x -> + if PSet.contains dominated_part x + then f x) l + );; + let pp_pset oc s = output_string oc "{ "; let first = ref true in -- cgit From 2efb64e96105c90f68f22a0a0bc386d1ac039354 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 18 Apr 2020 22:00:49 +0200 Subject: compute inner loops --- backend/LICMaux.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 269d9353..ecc11a00 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -52,7 +52,6 @@ let dominated_parts1 (f : coq_function) : Dominator.top in (headers, dominated);; -(* unfinished *) let dominated_parts (f : coq_function) : PSet.t PTree.t = let (headers, dominated) = dominated_parts1 f in match dominated with @@ -103,6 +102,11 @@ let filter_dominated_part (predecessors : P.t list PTree.t) then f x) l );; +let inner_loops (f : coq_function) : PSet.t PTree.t = + let parts = dominated_parts f + and predecessors = Kildall.make_predecessors f.fn_code RTL.successors_instr in + PTree.map (filter_dominated_part predecessors) parts;; + let pp_pset oc s = output_string oc "{ "; let first = ref true in @@ -119,6 +123,11 @@ let print_dominated_parts oc f = Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) (PTree.elements (dominated_parts f));; +let print_inner_loops oc f = + List.iter (fun (header, nodes) -> + Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) + (PTree.elements (inner_loops f));; + let print_dominated_parts1 oc f = match snd (dominated_parts1 f) with | None -> output_string oc "error\n" @@ -142,7 +151,7 @@ let print_loop_headers f = let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg): (Inject.inj_instr list) PTree.t = - let _ = print_dominated_parts stdout f in + let _ = print_inner_loops stdout f in PTree.empty;; (* let max_reg = P.to_int coq_max_reg in -- cgit From 300e51261c090e6a66bd0e0004bb530b64caf6e9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 18 Apr 2020 22:37:01 +0200 Subject: pp_list --- backend/LICMaux.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index ecc11a00..39e336eb 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -107,17 +107,20 @@ let inner_loops (f : coq_function) : PSet.t PTree.t = and predecessors = Kildall.make_predecessors f.fn_code RTL.successors_instr in PTree.map (filter_dominated_part predecessors) parts;; -let pp_pset oc s = +let pp_list pp_item oc l = output_string oc "{ "; let first = ref true in List.iter (fun x -> (if !first then first := false else output_string oc ", "); - Printf.printf "%d" x) - (List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s))); + pp_item oc x) l; output_string oc " }";; +let pp_pset oc s = + pp_list (fun oc -> Printf.fprintf oc "%d") oc + (List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s)));; + let print_dominated_parts oc f = List.iter (fun (header, nodes) -> Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) -- cgit From 9c97918742e00798bad8c7862de92831bb62a69e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 17:26:05 +0200 Subject: try building injection lists --- backend/LICMaux.ml | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 39e336eb..5028869f 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -3,6 +3,7 @@ open Camlcoq;; open Maps;; open Kildall;; open HashedSet;; +open Inject;; type reg = P.t;; @@ -107,6 +108,57 @@ let inner_loops (f : coq_function) : PSet.t PTree.t = and predecessors = Kildall.make_predecessors f.fn_code RTL.successors_instr in PTree.map (filter_dominated_part predecessors) parts;; +let map_reg mapper r = + match PTree.get r mapper with + | None -> r + | Some x -> x;; + +let rewrite_loop_body (last_alloc : reg ref) + (insns : RTL.code) (header : P.t) (loop_body : PSet.t) = + let seen = ref PSet.empty + and stack = Stack.create () + and rewritten = ref [] in + let add_inj ii = rewritten := ii::!rewritten in + Stack.push (header, PTree.empty) stack; + while not (Stack.is_empty stack) + do + let (pc, mapper) = Stack.pop stack in + if not (PSet.contains !seen pc) + then + begin + seen := PSet.add pc !seen; + match PTree.get pc insns with + | None -> () + | Some ii -> + let mapper' = + match ii with + | Iop(op, args, res, pc') -> + let new_res = P.succ !last_alloc in + last_alloc := new_res; + add_inj (INJop(op, + (List.map (map_reg mapper) args), + new_res)); + PTree.set res new_res mapper + | Iload(trap, chunk, addr, args, res, pc') -> + let new_res = P.succ !last_alloc in + last_alloc := new_res; + add_inj (INJload(chunk, addr, + (List.map (map_reg mapper) args), + new_res)); + PTree.set res new_res mapper + | _ -> mapper in + List.iter (fun x -> Stack.push (x, mapper') stack) + (successors_instr ii) + end + done; + List.rev !rewritten;; + +(* +| INJnop +| INJop of operation * reg list * reg +| INJload of memory_chunk * addressing * reg list * reg + *) + let pp_list pp_item oc l = output_string oc "{ "; let first = ref true in -- cgit From 1e361a51e7efa560f378db2c0c9993261cabe008 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 17:50:49 +0200 Subject: synthesize injection lists --- backend/LICMaux.ml | 38 ++++++++++++++++++++++++++++++-------- 1 file changed, 30 insertions(+), 8 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 5028869f..531f1f9e 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -147,18 +147,40 @@ let rewrite_loop_body (last_alloc : reg ref) new_res)); PTree.set res new_res mapper | _ -> mapper in - List.iter (fun x -> Stack.push (x, mapper') stack) + List.iter (fun x -> + if PSet.contains loop_body x + then Stack.push (x, mapper') stack) (successors_instr ii) end done; List.rev !rewritten;; -(* -| INJnop -| INJop of operation * reg list * reg -| INJload of memory_chunk * addressing * reg list * reg - *) - +let pp_inj_instr (oc : out_channel) (ii : inj_instr) = + match ii with + | INJnop -> output_string oc "nop" + | INJop(op, args, res) -> + Printf.fprintf oc "%a = %a" + PrintRTL.reg res (PrintOp.print_operation PrintRTL.reg) (op, args) + | INJload(chunk, addr, args, dst) -> + Printf.fprintf oc "%a = %s[%a]" + PrintRTL.reg dst (PrintAST.name_of_chunk chunk) + (PrintOp.print_addressing PrintRTL.reg) (addr, args);; + +let pp_inj_list (oc : out_channel) (l : inj_instr list) = + List.iter (Printf.fprintf oc "%a; " pp_inj_instr) l;; + +let pp_injections (oc : out_channel) (injections : inj_instr list PTree.t) = + List.iter + (fun (pc, injl) -> + Printf.fprintf oc "%d : %a\n" (P.to_int pc) pp_inj_list injl) + (PTree.elements injections);; + +let compute_injections (f : coq_function) = + let loop_bodies = inner_loops f + and last_alloc = ref (max_reg_function f) in + PTree.map + (rewrite_loop_body last_alloc f.fn_code) loop_bodies;; + let pp_list pp_item oc l = output_string oc "{ "; let first = ref true in @@ -206,7 +228,7 @@ let print_loop_headers f = let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg): (Inject.inj_instr list) PTree.t = - let _ = print_inner_loops stdout f in + let _ = pp_injections stdout (compute_injections f) in PTree.empty;; (* let max_reg = P.to_int coq_max_reg in -- cgit From 9010b8750aecd3a1ab45944b7dd4af3f33768f71 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 18:49:34 +0200 Subject: compute injections --- backend/LICMaux.ml | 39 ++++++++++++++++++++++++++++----------- 1 file changed, 28 insertions(+), 11 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 531f1f9e..314a5cf4 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -53,7 +53,7 @@ let dominated_parts1 (f : coq_function) : Dominator.top in (headers, dominated);; -let dominated_parts (f : coq_function) : PSet.t PTree.t = +let dominated_parts (f : coq_function) : Dominator.t PMap.t * PSet.t PTree.t = let (headers, dominated) = dominated_parts1 f in match dominated with | None -> failwith "dominated_parts 1" @@ -63,6 +63,7 @@ let dominated_parts (f : coq_function) : PSet.t PTree.t = if flag then PTree.set pc (PSet.add pc PSet.empty) before else before) headers PTree.empty in + (dominated, PTree.fold (fun before pc ii -> match PMap.get pc dominated with | Dominator.Dominated x -> @@ -71,7 +72,7 @@ let dominated_parts (f : coq_function) : PSet.t PTree.t = | None -> failwith "dominated_parts 2" | Some old -> PTree.set px (PSet.add pc old) before) - | _ -> before) f.fn_code singletons;; + | _ -> before) f.fn_code singletons);; let graph_traversal (initial_node : P.t) (successor_iterator : P.t -> (P.t -> unit) -> unit) : PSet.t = @@ -103,10 +104,10 @@ let filter_dominated_part (predecessors : P.t list PTree.t) then f x) l );; -let inner_loops (f : coq_function) : PSet.t PTree.t = - let parts = dominated_parts f +let inner_loops (f : coq_function) = + let (dominated, parts) = dominated_parts f and predecessors = Kildall.make_predecessors f.fn_code RTL.successors_instr in - PTree.map (filter_dominated_part predecessors) parts;; + (dominated, predecessors, PTree.map (filter_dominated_part predecessors) parts);; let map_reg mapper r = match PTree.get r mapper with @@ -175,11 +176,27 @@ let pp_injections (oc : out_channel) (injections : inj_instr list PTree.t) = Printf.fprintf oc "%d : %a\n" (P.to_int pc) pp_inj_list injl) (PTree.elements injections);; -let compute_injections (f : coq_function) = - let loop_bodies = inner_loops f +let compute_injections1 (f : coq_function) = + let (dominated, predecessors, loop_bodies) = inner_loops f and last_alloc = ref (max_reg_function f) in - PTree.map - (rewrite_loop_body last_alloc f.fn_code) loop_bodies;; + (dominated, predecessors, + PTree.map (fun header body -> + (body, rewrite_loop_body last_alloc f.fn_code header body)) loop_bodies);; + +let compute_injections (f : coq_function) : inj_instr list PTree.t = + let (dominated, predecessors, injections) = compute_injections1 f in + let output_map = ref PTree.empty in + List.iter + (fun (header, (body, inj)) -> + match PTree.get header predecessors with + | None -> failwith "compute_injections" + | Some l -> + List.iter (fun predecessor -> + if (PMap.get predecessor dominated)<>Dominator.Unreachable && + not (PSet.contains body predecessor) + then output_map := PTree.set predecessor inj !output_map) l) + (PTree.elements injections); + !output_map;; let pp_list pp_item oc l = output_string oc "{ "; @@ -198,12 +215,12 @@ let pp_pset oc s = let print_dominated_parts oc f = List.iter (fun (header, nodes) -> Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) - (PTree.elements (dominated_parts f));; + (PTree.elements (snd (dominated_parts f)));; let print_inner_loops oc f = List.iter (fun (header, nodes) -> Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) - (PTree.elements (inner_loops f));; + (PTree.elements (let (_,_,l) = (inner_loops f) in l));; let print_dominated_parts1 oc f = match snd (dominated_parts1 f) with -- cgit From d0163625ad55f8b01a3c002dd52be83b8a26e35e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 19:50:14 +0200 Subject: test whether the instructions are allowed --- aarch64/Archi.v | 2 ++ arm/Archi.v | 2 ++ backend/LICMaux.ml | 14 ++++++-------- mppa_k1c/Archi.v | 6 ++++-- powerpc/Archi.v | 2 ++ riscV/Archi.v | 2 ++ test/monniaux/cse2/noloopinvariant.c | 6 ++++++ x86_32/Archi.v | 2 ++ x86_64/Archi.v | 2 ++ 9 files changed, 28 insertions(+), 10 deletions(-) create mode 100644 test/monniaux/cse2/noloopinvariant.c diff --git a/aarch64/Archi.v b/aarch64/Archi.v index aef4ab77..7d7b6887 100644 --- a/aarch64/Archi.v +++ b/aarch64/Archi.v @@ -86,3 +86,5 @@ Global Opaque ptr64 big_endian splitlong (** Whether to generate position-independent code or not *) Parameter pic_code: unit -> bool. + +Definition has_notrap_loads := false. diff --git a/arm/Archi.v b/arm/Archi.v index 16d6c71d..738341cc 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -97,3 +97,5 @@ Parameter abi: abi_kind. (** Whether instructions added with Thumb2 are supported. True for ARMv6T2 and above. *) Parameter thumb2_support: bool. + +Definition has_notrap_loads := false. diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 314a5cf4..0368b94f 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -133,14 +133,15 @@ let rewrite_loop_body (last_alloc : reg ref) | Some ii -> let mapper' = match ii with - | Iop(op, args, res, pc') -> + | Iop(op, args, res, pc') when not (Op.is_trapping_op op) -> let new_res = P.succ !last_alloc in last_alloc := new_res; add_inj (INJop(op, (List.map (map_reg mapper) args), new_res)); PTree.set res new_res mapper - | Iload(trap, chunk, addr, args, res, pc') -> + | Iload(trap, chunk, addr, args, res, pc') + when Archi.has_notrap_loads -> let new_res = P.succ !last_alloc in last_alloc := new_res; add_inj (INJload(chunk, addr, @@ -245,9 +246,6 @@ let print_loop_headers f = let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg): (Inject.inj_instr list) PTree.t = - let _ = pp_injections stdout (compute_injections f) in - PTree.empty;; -(* - let max_reg = P.to_int coq_max_reg in - PTree.set coq_max_pc [Inject.INJload(AST.Mint32, (Op.Aindexed (Ptrofs.of_int (Z.of_sint 0))), [P.of_int 1], P.of_int (max_reg+1))] PTree.empty;; - *) + let injections = compute_injections f in + let () = pp_injections stdout injections in + injections;; diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v index 69b32c7c..587f768e 100644 --- a/mppa_k1c/Archi.v +++ b/mppa_k1c/Archi.v @@ -26,11 +26,11 @@ Definition big_endian := false. Definition align_int64 := 8%Z. Definition align_float64 := 8%Z. -Definition splitlong := negb ptr64. +Definition splitlong := false. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. Proof. - unfold splitlong. destruct ptr64; simpl; congruence. + unfold splitlong. congruence. Qed. (** THIS IS NOT CHECKED ! NONE OF THIS ! *) @@ -77,3 +77,5 @@ Global Opaque ptr64 big_endian splitlong (** Whether to generate position-independent code or not *) Parameter pic_code: unit -> bool. + +Definition has_notrap_loads := true. diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 10f38391..8f96dafc 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -71,3 +71,5 @@ Global Opaque ptr64 big_endian splitlong default_nan_32 choose_nan_32 fma_order fma_invalid_mul_is_nan float_of_single_preserves_sNaN. + +Definition has_notrap_loads := false. diff --git a/riscV/Archi.v b/riscV/Archi.v index 61d129d0..9bdaad99 100644 --- a/riscV/Archi.v +++ b/riscV/Archi.v @@ -72,3 +72,5 @@ Global Opaque ptr64 big_endian splitlong (** Whether to generate position-independent code or not *) Parameter pic_code: unit -> bool. + +Definition has_notrap_loads := false. diff --git a/test/monniaux/cse2/noloopinvariant.c b/test/monniaux/cse2/noloopinvariant.c new file mode 100644 index 00000000..5c7789bf --- /dev/null +++ b/test/monniaux/cse2/noloopinvariant.c @@ -0,0 +1,6 @@ +int toto(int *t, int n) { + for(int i=1; i t[0]) return i; + } + return 0; +} diff --git a/x86_32/Archi.v b/x86_32/Archi.v index e9d05c14..4681784d 100644 --- a/x86_32/Archi.v +++ b/x86_32/Archi.v @@ -64,3 +64,5 @@ Global Opaque ptr64 big_endian splitlong default_nan_32 choose_nan_32 fma_order fma_invalid_mul_is_nan float_of_single_preserves_sNaN. + +Definition has_notrap_loads := false. diff --git a/x86_64/Archi.v b/x86_64/Archi.v index 959d8dc1..0e3c55f8 100644 --- a/x86_64/Archi.v +++ b/x86_64/Archi.v @@ -64,3 +64,5 @@ Global Opaque ptr64 big_endian splitlong default_nan_32 choose_nan_32 fma_order fma_invalid_mul_is_nan float_of_single_preserves_sNaN. + +Definition has_notrap_loads := false. -- cgit From 22d8683c16e863dc44ef45d66a4530d8c63d2c30 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 20:03:49 +0200 Subject: forgotten extraction --- extraction/extraction.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/extraction/extraction.v b/extraction/extraction.v index b102503b..18637336 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -224,4 +224,5 @@ Separate Extraction Floats.Float32.from_parsed Floats.Float.from_parsed Globalenvs.Senv.invert_symbol Parser.translation_unit_file - Compopts.optim_postpass. + Compopts.optim_postpass + Archi.has_notrap_loads. -- cgit From a95735290d61f50a388895ef86627becd67c4553 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 20:04:15 +0200 Subject: activate LICM --- backend/LICMaux.ml | 2 +- driver/Clflags.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 0368b94f..32044cc9 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -247,5 +247,5 @@ let print_loop_headers f = let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg): (Inject.inj_instr list) PTree.t = let injections = compute_injections f in - let () = pp_injections stdout injections in + (* let () = pp_injections stdout injections in *) injections;; diff --git a/driver/Clflags.ml b/driver/Clflags.ml index ae96e820..8deb5224 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -82,6 +82,6 @@ let option_fxsaddr = ref true let option_faddx = ref false let option_fcoalesce_mem = ref true let option_fforward_moves = ref true -let option_fmove_loop_invariants = ref false +let option_fmove_loop_invariants = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 -- cgit From eead578fde08a1555086ed75714bca3ca1f9b1dc Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 19 Apr 2020 21:14:21 +0200 Subject: add options for controlling madd and notrap selection --- backend/LICMaux.ml | 3 ++- driver/Clflags.ml | 4 +++- driver/Compopts.v | 3 +++ driver/Driver.ml | 2 ++ extraction/extraction.v | 2 ++ mppa_k1c/SelectOp.vp | 22 ++++++++++++++++------ mppa_k1c/SelectOpproof.v | 27 ++++++++++++++++++--------- 7 files changed, 46 insertions(+), 17 deletions(-) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 32044cc9..4ebc7844 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -141,7 +141,8 @@ let rewrite_loop_body (last_alloc : reg ref) new_res)); PTree.set res new_res mapper | Iload(trap, chunk, addr, args, res, pc') - when Archi.has_notrap_loads -> + when Archi.has_notrap_loads && + !Clflags.option_fnontrap_loads -> let new_res = P.succ !last_alloc in last_alloc := new_res; add_inj (INJload(chunk, addr, diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 8deb5224..8e3305ef 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -79,9 +79,11 @@ 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_faddx = ref false +let option_faddx = ref false +let option_fmadd = ref true let option_fcoalesce_mem = ref true let option_fforward_moves = ref true let option_fmove_loop_invariants = ref true +let option_fnontrap_loads = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 diff --git a/driver/Compopts.v b/driver/Compopts.v index e4dae87d..5acd2640 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -69,6 +69,9 @@ 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 true) *) +Parameter optim_madd: unit -> bool. + (** FIXME TEMPORARY Flag -faddx. Fuse (default false) *) Parameter optim_addx: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index 0f9e637c..6a9e9b92 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -415,6 +415,8 @@ let cmdline_actions = @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr @ f_opt "addx" option_faddx + @ f_opt "madd" option_fmadd + @ f_opt "nontrap-loads" option_fnontrap_loads @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap @ f_opt "forward-moves" option_fforward_moves diff --git a/extraction/extraction.v b/extraction/extraction.v index 18637336..b6aa3409 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -142,6 +142,8 @@ Extract Constant Compopts.optim_xsaddr => "fun _ -> !Clflags.option_fxsaddr". Extract Constant Compopts.optim_addx => "fun _ -> !Clflags.option_faddx". +Extract Constant Compopts.optim_madd => + "fun _ -> !Clflags.option_fmadd". Extract Constant Compopts.optim_coalesce_mem => "fun _ -> !Clflags.option_fcoalesce_mem". Extract Constant Compopts.optim_forward_moves => diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index ec3985c5..0974f872 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -168,13 +168,21 @@ Nondetfunction add (e1: expr) (e2: expr) := | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) | t1, (Eop Omul (t2:::t3:::Enil)) => - Eop Omadd (t1:::t2:::t3:::Enil) + if Compopts.optim_madd tt + then Eop Omadd (t1:::t2:::t3:::Enil) + else Eop Oadd (e1:::e2:::Enil) | (Eop Omul (t2:::t3:::Enil)), t1 => - Eop Omadd (t1:::t2:::t3:::Enil) + if Compopts.optim_madd tt + then Eop Omadd (t1:::t2:::t3:::Enil) + else Eop Oadd (e1:::e2:::Enil) | t1, (Eop (Omulimm n) (t2:::Enil)) => - Eop (Omaddimm n) (t1:::t2:::Enil) + if Compopts.optim_madd tt + then Eop (Omaddimm n) (t1:::t2:::Enil) + else Eop Oadd (e1:::e2:::Enil) | (Eop (Omulimm n) (t2:::Enil)), t1 => - Eop (Omaddimm n) (t1:::t2:::Enil) + if Compopts.optim_madd tt + then Eop (Omaddimm n) (t1:::t2:::Enil) + else Eop Oadd (e1:::e2:::Enil) | (Eop (Oshlimm n) (t1:::Enil)), t2 => add_shlimm n t1 t2 | t2, (Eop (Oshlimm n) (t1:::Enil)) => @@ -197,7 +205,9 @@ Nondetfunction sub (e1: expr) (e2: expr) := | t1, (Eop Omul (t2:::t3:::Enil)) => Eop Omsub (t1:::t2:::t3:::Enil) | t1, (Eop (Omulimm n) (t2:::Enil)) => - Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil) + if Compopts.optim_madd tt + then Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil) + else Eop Osub (e1:::e2:::Enil) | _, _ => Eop Osub (e1:::e2:::Enil) end. @@ -712,4 +722,4 @@ End SELECT. (* Local Variables: *) (* mode: coq *) -(* End: *) \ No newline at end of file +(* End: *) diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index d3eb1dde..368f78f4 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -350,13 +350,19 @@ Proof. apply eval_addimm. EvalOp. repeat rewrite Val.add_assoc. reflexivity. - (* Omadd *) - subst. TrivialExists. + subst. destruct (Compopts.optim_madd tt); TrivialExists; + repeat (eauto; econstructor; simpl). - (* Omadd rev *) - subst. rewrite Val.add_commut. TrivialExists. + subst. destruct (Compopts.optim_madd tt); TrivialExists; + repeat (eauto; econstructor; simpl). + simpl. rewrite Val.add_commut. reflexivity. - (* Omaddimm *) - subst. TrivialExists. + subst. destruct (Compopts.optim_madd tt); TrivialExists; + repeat (eauto; econstructor; simpl). - (* Omaddimm rev *) - subst. rewrite Val.add_commut. TrivialExists. + subst. destruct (Compopts.optim_madd tt); TrivialExists; + repeat (eauto; econstructor; simpl). + simpl. rewrite Val.add_commut. reflexivity. (* Oaddx *) - subst. pose proof eval_addx as ADDX. unfold binary_constructor_sound in ADDX. @@ -380,11 +386,14 @@ Proof. - subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp. - subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp. - TrivialExists. simpl. subst. reflexivity. - - TrivialExists. simpl. subst. - rewrite sub_add_neg. - rewrite neg_mul_distr_r. - unfold Val.neg. - reflexivity. + - destruct (Compopts.optim_madd tt). + + TrivialExists. simpl. subst. + rewrite sub_add_neg. + rewrite neg_mul_distr_r. + unfold Val.neg. + reflexivity. + + TrivialExists. repeat (eauto; econstructor). + simpl. subst. reflexivity. - TrivialExists. Qed. -- cgit