diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-21 16:26:30 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-05-21 16:26:30 +0000 |
| commit | 0053b1aa1d26da5d1f995a603b127daf799c2da9 (patch) | |
| tree | fec49ad37e5edffa5be742bafcadff3c8b8ede7f /arm/ConstpropOpproof.v | |
| parent | 219a2d178dcd5cc625f6b6261759f392cfca367b (diff) | |
| download | compcert-kvx-0053b1aa1d26da5d1f995a603b127daf799c2da9.tar.gz compcert-kvx-0053b1aa1d26da5d1f995a603b127daf799c2da9.zip | |
Merge of the newmem branch:
- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/ConstpropOpproof.v')
| -rw-r--r-- | arm/ConstpropOpproof.v | 26 |
1 files changed, 24 insertions, 2 deletions
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index bf3b216c..242f29b0 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -124,7 +124,7 @@ Proof. unfold eval_static_operation. case (eval_static_operation_match op al); intros; InvVLMA; simpl in *; FuncInv; try (subst v); try (rewrite eval_static_shift_correct); auto. - + destruct (propagate_float_constants tt); simpl; auto. rewrite shift_symbol_address; auto. rewrite shift_symbol_address; auto. rewrite Val.add_assoc; auto. @@ -145,7 +145,8 @@ Proof. destruct (Int.ltu n2 Int.iwordsize); simpl; auto. unfold eval_static_intoffloat. destruct (Float.intoffloat n1); simpl in H0; inv H0; simpl; auto. unfold eval_static_intuoffloat. destruct (Float.intuoffloat n1); simpl in H0; inv H0; simpl; auto. - + destruct (propagate_float_constants tt); 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). @@ -153,6 +154,27 @@ 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); try (rewrite eval_static_shift_correct); 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. + rewrite Val.add_assoc. auto. +Qed. + (** * Correctness of strength reduction *) (** We now show that strength reduction over operators and addressing |