diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backend/Inject.v | 7 | ||||
| -rw-r--r-- | backend/Injectproof.v | 21 |
3 files changed, 11 insertions, 19 deletions
@@ -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. +*) |