aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/CSE3analysis.v39
-rw-r--r--backend/CSE3analysisproof.v107
-rw-r--r--backend/CSE3proof.v3
-rw-r--r--extraction/extraction.v2
4 files changed, 106 insertions, 45 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index cd7e3d84..34df644e 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -227,29 +227,44 @@ Section OPERATIONS.
Definition kill_mem (rel : RELATION.t) : RELATION.t :=
PSet.subtract rel (eq_kill_mem ctx tt).
- Definition pick_source (l : list reg) := (* todo: take min? *)
+ Definition reg_min (x y : reg) :=
+ if plt x y then x else y.
+
+ Fixpoint reg_min_rec (l : list reg) (before : reg) :=
+ match l with
+ | h::t => reg_min_rec t (reg_min before h)
+ | nil => before
+ end.
+
+ Definition pick_source (l : list reg) :=
match l with
- | h::t => Some h
+ | h::t => Some (reg_min_rec t h)
| nil => None
end.
-
- Definition forward_move (rel : RELATION.t) (x : reg) : reg :=
- match pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x))) with
- | None => x
- | Some eqno =>
+
+ Fixpoint get_sources (x : reg) eqs :=
+ match eqs with
+ | nil => nil
+ | eqno::others =>
match eq_catalog ctx eqno with
| Some eq =>
if is_smove (eq_op eq) && peq x (eq_lhs eq)
then
match eq_args eq with
- | src::nil => src
- | _ => x
+ | src::nil => src :: (get_sources x others)
+ | _ => get_sources x others
end
- else x
- | _ => x
+ else get_sources x others
+ | _ => get_sources x others
end
end.
-
+
+ Definition forward_move (rel : RELATION.t) (x : reg) : reg :=
+ match pick_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with
+ | None => x
+ | Some src => src
+ end.
+
Definition forward_move_l (rel : RELATION.t) : list reg -> list reg :=
List.map (forward_move rel).
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index ea4d37ca..12048010 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -478,6 +478,27 @@ Section SOUNDNESS.
rewrite negb_true_iff in H.
intuition.
Qed.
+
+ Lemma reg_min_sound:
+ forall x y, (reg_min x y) = x \/ (reg_min x y) = y.
+ Proof.
+ intros; unfold reg_min.
+ destruct plt; auto.
+ Qed.
+
+ Lemma reg_min_rec_sound :
+ forall (l : list reg) (before : reg),
+ In (reg_min_rec l before) l \/
+ reg_min_rec l before = before.
+ Proof.
+ induction l; cbn.
+ { auto. }
+ intro bef.
+ destruct (IHl (reg_min bef a)).
+ { auto. }
+ rewrite H.
+ destruct (reg_min_sound bef a); auto.
+ Qed.
Lemma pick_source_sound :
forall (l : list reg),
@@ -486,47 +507,71 @@ Section SOUNDNESS.
| None => True
end.
Proof.
- unfold pick_source.
- destruct l; simpl; trivial.
- left; trivial.
+ destruct l; cbn; trivial.
+ destruct (reg_min_rec_sound l r); auto.
Qed.
-
+
Hint Resolve pick_source_sound : cse3.
+ Theorem get_sources_sound :
+ forall l src rs m x,
+ (forall i eq,
+ In i l ->
+ eq_catalog ctx i = Some eq ->
+ sem_eq eq rs m) ->
+ (In src (get_sources (ctx := ctx) x l)) ->
+ rs # src = rs # x.
+ Proof.
+ induction l; cbn; intros until x; intros SEM IN.
+ contradiction.
+ destruct (eq_catalog ctx a) eqn:CATALOG.
+ 2: eauto using IHl; fail.
+ pose proof (SEM a e) as SEMeq.
+ destruct e; cbn in *.
+ destruct (is_smove eq_op && peq x eq_lhs) eqn:CORRECT.
+ 2: eauto using IHl; fail.
+ destruct eq_args.
+ eauto using IHl; fail.
+ destruct eq_args.
+ 2: eauto using IHl; fail.
+ cbn in IN.
+ destruct IN.
+ 2: eauto using IHl; fail.
+ rewrite andb_true_iff in CORRECT.
+ intuition.
+ destruct (peq x eq_lhs).
+ 2: discriminate.
+ subst eq_lhs.
+ destruct (is_smove eq_op).
+ 2: discriminate.
+ subst eq_op.
+ subst src.
+ cbn in H2.
+ symmetry.
+ assumption.
+ Qed.
+
Theorem forward_move_sound :
forall rel rs m x,
(sem_rel rel rs m) ->
rs # (forward_move (ctx := ctx) rel x) = rs # x.
Proof.
- unfold sem_rel, forward_move.
- intros until x.
- intro REL.
- pose proof (pick_source_sound (PSet.elements (PSet.inter rel (eq_moves ctx x)))) as ELEMENT.
- destruct (pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x)))).
- 2: reflexivity.
- destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG.
- 2: reflexivity.
- specialize REL with (i := r) (eq0 := eq).
- destruct (is_smove (eq_op eq)) as [MOVE | ].
- 2: reflexivity.
- destruct (peq x (eq_lhs eq)).
+ unfold forward_move.
+ intros until x; intros REL.
+ pose proof (pick_source_sound (get_sources (ctx := ctx) x (PSet.elements (PSet.inter rel (eq_moves ctx x))))) as PICK.
+ destruct pick_source.
2: reflexivity.
- simpl.
- subst x.
- rewrite PSet.elements_spec in ELEMENT.
- rewrite PSet.ginter in ELEMENT.
- rewrite andb_true_iff in ELEMENT.
- unfold sem_eq in REL.
- rewrite MOVE in REL.
- simpl in REL.
- destruct (eq_args eq) as [ | h t].
- reflexivity.
- destruct t.
- 2: reflexivity.
- simpl in REL.
- intuition congruence.
+ apply get_sources_sound with (l := (PSet.elements (PSet.inter rel (eq_moves ctx x)))) (m:=m).
+ 2: assumption.
+ intros i eq IN CATALOG.
+ rewrite PSet.elements_spec in IN.
+ rewrite PSet.ginter in IN.
+ rewrite andb_true_iff in IN.
+ destruct IN.
+ unfold sem_rel in REL.
+ apply REL with (i:=i); assumption.
Qed.
-
+
Hint Resolve forward_move_sound : cse3.
Theorem forward_move_l_sound :
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 3fbc9912..5dd5ee04 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -63,7 +63,7 @@ Proof.
destruct rel as [rel | ]; simpl; intros.
2: contradiction.
eapply forward_move_sound; eauto.
- Qed.
+Qed.
Lemma forward_move_l_b_sound :
forall rel rs m x,
@@ -447,7 +447,6 @@ Lemma step_simulation:
forall S1 t S2, RTL.step ge S1 t S2 ->
forall S1', match_states S1 S1' ->
exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
-Proof.
induction 1; intros S1' MS; inv MS.
- (* Inop *)
exists (State ts tf sp pc' rs m). split.
diff --git a/extraction/extraction.v b/extraction/extraction.v
index bd396cd8..c5fa7a62 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -127,6 +127,8 @@ Extract Constant Compopts.optim_CSE3_across_merges =>
"fun _ -> !Clflags.option_fcse3_across_merges".
Extract Constant Compopts.optim_CSE3_glb =>
"fun _ -> !Clflags.option_fcse3_glb".
+Extract Constant Compopts.optim_CSE3_trivial_ops =>
+ "fun _ -> !Clflags.option_fcse3_trivial_ops".
Extract Constant Compopts.optim_move_loop_invariants =>
"fun _ -> !Clflags.option_fmove_loop_invariants".
generated by cgit (git 2.34.1) at 2024-05-20 04:00:52 +0000