diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 18:55:20 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 18:55:20 +0200 |
commit | aa5b5a4e618b6a0aecc227021080aa4b901d806f (patch) | |
tree | 0cf0c0bd42a05b49951d896cf2b5270aabdb9316 /common | |
parent | a363d6b93df8fbde24c945551cfea5d845b57fc4 (diff) | |
parent | 24406a351e9d64c2953b0b9fc7ef0b3d79db9b85 (diff) | |
download | compcert-kvx-aa5b5a4e618b6a0aecc227021080aa4b901d806f.tar.gz compcert-kvx-aa5b5a4e618b6a0aecc227021080aa4b901d806f.zip |
Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workv3.6_mppa_2019-09-20
merge with v3.6
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: |