diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-06 09:49:50 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-06 09:49:50 +0200 |
| commit | fecf2472ee5c2f6da25eb1ea340e0f07dcdaec69 (patch) | |
| tree | 5bbe7afa05895ba7857b86e7c5d7d40c29076e1b | |
| parent | 67c58f9ee025fb2fc0de6d932366b7e5db7a6678 (diff) | |
| download | compcert-kvx-fecf2472ee5c2f6da25eb1ea340e0f07dcdaec69.tar.gz compcert-kvx-fecf2472ee5c2f6da25eb1ea340e0f07dcdaec69.zip | |
Regression: compile-time evaluation of ((struct s *)0)->field
This somewhat useful idiom was broken when Val.add was replaced by Val.offset_ptr in the Efield case. This commit restores the previous behavior.
This used to be supported (and is useful
| -rw-r--r-- | cfrontend/Initializers.v | 4 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 7 |
2 files changed, 7 insertions, 4 deletions
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 5b7e52c8..19518aea 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -119,7 +119,9 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := do co <- lookup_composite ce id; do delta <- field_offset ce f (co_members co); do v <- constval ce l; - OK (Val.offset_ptr v (Ptrofs.repr delta)) + OK (if Archi.ptr64 + then Val.addl v (Vlong (Int64.repr delta)) + else Val.add v (Vint (Int.repr delta))) | Tunion id _ => constval ce l | _ => diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 49ac858e..fee25c48 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -446,9 +446,10 @@ Proof. (* field struct *) rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ. exploit constval_rvalue; eauto. intro MV. inv MV. - simpl. replace x0 with delta by congruence. econstructor; eauto. - rewrite ! Ptrofs.add_assoc. f_equal. apply Ptrofs.add_commut. - simpl. auto. + replace x0 with delta by congruence. rewrite Ptrofs.add_assoc. rewrite (Ptrofs.add_commut (Ptrofs.repr delta0)). + simpl; destruct Archi.ptr64 eqn:SF; + econstructor; eauto; rewrite ! Ptrofs.add_assoc; f_equal; f_equal; symmetry; auto with ptrofs. + destruct Archi.ptr64; auto. (* field union *) rewrite H0 in CV. eauto. Qed. |