diff options
Diffstat (limited to 'powerpc/ConstpropOpproof.v')
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 3b5021e..1c050bd 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -118,6 +118,8 @@ Proof. case (eval_static_operation_match op al); intros; InvVLMA; simpl in *; FuncInv; try subst v; auto. + destruct (propagate_float_constants tt); simpl; auto. + rewrite shift_symbol_address; auto. rewrite Int.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut. auto. @@ -149,6 +151,8 @@ Proof. unfold eval_static_intoffloat. destruct (Float.intoffloat n1); simpl in H0; inv H0. simpl; auto. + destruct (propagate_float_constants tt); simpl; auto. + unfold eval_static_condition_val, Val.of_optbool. destruct (eval_static_condition c vl0) as []_eqn. rewrite (eval_static_condition_correct _ _ _ m _ H Heqo). @@ -156,6 +160,26 @@ Proof. simpl; auto. Qed. +Lemma eval_static_addressing_correct: + forall addr al vl v, + val_list_match_approx al vl -> + eval_addressing ge sp addr vl = Some v -> + val_match_approx (eval_static_addressing addr al) v. +Proof. + intros until v. unfold eval_static_addressing. + case (eval_static_addressing_match addr al); intros; + InvVLMA; simpl in *; FuncInv; try subst v; auto. + rewrite shift_symbol_address; auto. + rewrite Val.add_assoc. auto. + repeat rewrite shift_symbol_address. auto. + fold (Val.add (Vint n1) (symbol_address ge id ofs)). + repeat rewrite shift_symbol_address. apply Val.add_commut. + repeat rewrite Val.add_assoc. auto. + fold (Val.add (Vint n1) (Val.add sp (Vint ofs))). + rewrite Val.add_permut. decEq. rewrite Val.add_commut. auto. + rewrite shift_symbol_address. auto. +Qed. + (** * Correctness of strength reduction *) (** We now show that strength reduction over operators and addressing |