diff options
Diffstat (limited to 'mppa_k1c/NeedOp.v')
| -rw-r--r-- | mppa_k1c/NeedOp.v | 253 |
1 files changed, 246 insertions, 7 deletions
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 2577370c..ba051c90 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -117,6 +117,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) | Ocmp c => needs_of_condition c + | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => op3 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := @@ -145,19 +146,75 @@ Section SOUNDNESS. Variable ge: genv. Variable sp: block. -Variables m m': mem. -Hypothesis PERM: forall b ofs k p, Mem.perm m b ofs k p -> Mem.perm m' b ofs k p. +Variables m1 m2: mem. +Hypothesis PERM: forall b ofs k p, Mem.perm m1 b ofs k p -> Mem.perm m2 b ofs k p. Lemma needs_of_condition_sound: forall cond args b args', - eval_condition cond args m = Some b -> + eval_condition cond args m1 = Some b -> vagree_list args args' (needs_of_condition cond) -> - eval_condition cond args' m' = Some b. + eval_condition cond args' m2 = Some b. Proof. intros. unfold needs_of_condition in H0. eapply default_needs_of_condition_sound; eauto. Qed. +Let valid_pointer_inj: + forall b1 ofs b2 delta, + inject_id b1 = Some(b2, delta) -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. +Proof. + unfold inject_id; intros. inv H. rewrite Ptrofs.add_zero. + rewrite Mem.valid_pointer_nonempty_perm in *. eauto. +Qed. + +Let weak_valid_pointer_inj: + forall b1 ofs b2 delta, + inject_id b1 = Some(b2, delta) -> + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. +Proof. + unfold inject_id; intros. inv H. rewrite Ptrofs.add_zero. + rewrite Mem.weak_valid_pointer_spec in *. + rewrite ! Mem.valid_pointer_nonempty_perm in *. + destruct H0; [left|right]; eauto. +Qed. + +Let weak_valid_pointer_no_overflow: + forall b1 ofs b2 delta, + inject_id b1 = Some(b2, delta) -> + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. +Proof. + unfold inject_id; intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2. +Qed. + +Let valid_different_pointers_inj: + forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, + b1 <> b2 -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> + inject_id b1 = Some (b1', delta1) -> + inject_id b2 = Some (b2', delta2) -> + b1' <> b2' \/ + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). +Proof. + unfold inject_id; intros. left; congruence. +Qed. + +Lemma needs_of_condition0_sound: + forall cond arg1 b arg2, + eval_condition0 cond arg1 m1 = Some b -> + vagree arg1 arg2 All -> + eval_condition0 cond arg2 m2 = Some b. +Proof. + intros until arg2. + intros Hcond Hagree. + apply eval_condition0_inj with (f := inject_id) (m1 := m1) (v1 := arg1); simpl; auto. + apply val_inject_lessdef. apply lessdef_vagree. assumption. +Qed. + Lemma addl_sound: forall v1 w1 v2 w2 x, vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> @@ -185,6 +242,180 @@ Proof. inv H. inv H0. trivial. Qed. + +Lemma select_sound: + forall cond v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (eval_select cond v0 v1 v2 m1) (eval_select cond w0 w1 w2 m2) x. +Proof. + intros. + destruct x; simpl in *; trivial. + - rewrite eval_select_to2. + rewrite eval_select_to2. + unfold eval_select2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + apply iagree_refl. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + apply iagree_refl. + - rewrite eval_select_to2. + rewrite eval_select_to2. + unfold eval_select2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. +Qed. + +Lemma selectl_sound: + forall cond v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (eval_selectl cond v0 v1 v2 m1) (eval_selectl cond w0 w1 w2 m2) x. +Proof. + intros. + destruct x; simpl in *; trivial. + - rewrite eval_selectl_to2. + rewrite eval_selectl_to2. + unfold eval_selectl2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + - rewrite eval_selectl_to2. + rewrite eval_selectl_to2. + unfold eval_selectl2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. +Qed. + +Lemma selectf_sound: + forall cond v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (eval_selectf cond v0 v1 v2 m1) (eval_selectf cond w0 w1 w2 m2) x. +Proof. + intros. + destruct x; simpl in *; trivial. + - rewrite eval_selectf_to2. + rewrite eval_selectf_to2. + unfold eval_selectf2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + - rewrite eval_selectf_to2. + rewrite eval_selectf_to2. + unfold eval_selectf2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. +Qed. + +Lemma selectfs_sound: + forall cond v0 w0 v1 w1 v2 w2 x, + vagree v0 w0 (default x) -> + vagree v1 w1 (default x) -> + vagree v2 w2 (default x) -> + vagree (eval_selectfs cond v0 v1 v2 m1) (eval_selectfs cond w0 w1 w2 m2) x. +Proof. + intros. + destruct x; simpl in *; trivial. + - rewrite eval_selectfs_to2. + rewrite eval_selectfs_to2. + unfold eval_selectfs2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + destruct w1; trivial. + - rewrite eval_selectfs_to2. + rewrite eval_selectfs_to2. + unfold eval_selectfs2. + assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)). + assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)). + destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial. + destruct b. + + rewrite Hneedstrue; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. + + rewrite Hneedsfalse; trivial. + inv H; trivial. + destruct w0; trivial. + inv H0; trivial. +Qed. Remark default_idem: forall nv, default (default nv) = default nv. Proof. @@ -193,11 +424,11 @@ Qed. Lemma needs_of_operation_sound: forall op args v nv args', - eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op args m1 = Some v -> vagree_list args args' (needs_of_operation op nv) -> nv <> Nothing -> exists v', - eval_operation ge (Vptr sp Ptrofs.zero) op args' m' = Some v' + eval_operation ge (Vptr sp Ptrofs.zero) op args' m2 = Some v' /\ vagree v v' nv. Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); @@ -238,12 +469,20 @@ Proof. apply mull_sound; trivial. rewrite default_idem; trivial. rewrite default_idem; trivial. + (* select *) +- apply select_sound; trivial. + (* selectl *) +- apply selectl_sound; trivial. + (* selectf *) +- apply selectf_sound; trivial. + (* selectfs *) +- apply selectfs_sound; trivial. Qed. Lemma operation_is_redundant_sound: forall op nv arg1 args v arg1' args', operation_is_redundant op nv = true -> - eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m1 = Some v -> vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) -> vagree v arg1' nv. Proof. |