diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 16:20:11 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 16:20:11 +0200 |
| commit | 71cec9c9126ee4385ce12fd29dec557995d5a903 (patch) | |
| tree | 26e86fc9b15680721baea86d5294ee9faaf2508c /common | |
| parent | 1801685f8352b7a120d87d5b529d290728129529 (diff) | |
| parent | e1725209b2b4401adc63ce5238fa5db7c134609c (diff) | |
| download | compcert-kvx-71cec9c9126ee4385ce12fd29dec557995d5a903.tar.gz compcert-kvx-71cec9c9126ee4385ce12fd29dec557995d5a903.zip | |
Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'common')
| -rw-r--r-- | common/Errors.v | 2 | ||||
| -rw-r--r-- | common/Values.v | 23 |
2 files changed, 22 insertions, 3 deletions
diff --git a/common/Errors.v b/common/Errors.v index 28933313..6807735a 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -164,7 +164,7 @@ Ltac monadInv1 H := | (match ?X with left _ => _ | right _ => assertion_failed end = OK _) => destruct X; [try (monadInv1 H) | discriminate] | (match (negb ?X) with true => _ | false => assertion_failed end = OK _) => - destruct X as [] eqn:?; [discriminate | try (monadInv1 H)] + destruct X as [] eqn:?; simpl negb in H; [discriminate | try (monadInv1 H)] | (match ?X with true => _ | false => assertion_failed end = OK _) => destruct X as [] eqn:?; [try (monadInv1 H) | discriminate] | (mmap ?F ?L = OK ?M) => diff --git a/common/Values.v b/common/Values.v index 59e6388f..de317734 100644 --- a/common/Values.v +++ b/common/Values.v @@ -783,6 +783,17 @@ Definition rolml (v: val) (amount: int) (mask: int64): val := | _ => Vundef end. +Definition zero_ext_l (nbits: Z) (v: val) : val := + match v with + | Vlong n => Vlong(Int64.zero_ext nbits n) + | _ => Vundef + end. + +Definition sign_ext_l (nbits: Z) (v: val) : val := + match v with + | Vlong n => Vlong(Int64.sign_ext nbits n) + | _ => Vundef + end. (** Comparisons *) @@ -1899,10 +1910,18 @@ Qed. Lemma zero_ext_and: forall n v, - 0 < n < Int.zwordsize -> + 0 <= n -> Val.zero_ext n v = Val.and v (Vint (Int.repr (two_p n - 1))). Proof. - intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. omega. + intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. +Qed. + +Lemma zero_ext_andl: + forall n v, + 0 <= n -> + Val.zero_ext_l n v = Val.andl v (Vlong (Int64.repr (two_p n - 1))). +Proof. + intros. destruct v; simpl; auto. decEq. apply Int64.zero_ext_and; auto. Qed. Lemma rolm_lt_zero: |