diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-09-11 15:13:12 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-11 15:13:12 +0200 |
| commit | 7601fb5e792a5305336e5cda9794c4041d053b95 (patch) | |
| tree | f0dc0acd7bb5ad6dae80e4389fb165fa93eb3cb8 /common | |
| parent | d3eba50731c23546c6e9ccb14230460fc1da592e (diff) | |
| parent | c243b565ab0744086e10efcfee16768f6c3cf880 (diff) | |
| download | compcert-7601fb5e792a5305336e5cda9794c4041d053b95.tar.gz compcert-7601fb5e792a5305336e5cda9794c4041d053b95.zip | |
Merge pull request #313 from AbsInt/aarch64
Support target architecture AArch64 (ARMv8 in 64-bit mode)
Diffstat (limited to 'common')
| -rw-r--r-- | common/Errors.v | 2 | ||||
| -rw-r--r-- | common/Values.v | 24 |
2 files changed, 23 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 2eb778a5..de317734 100644 --- a/common/Values.v +++ b/common/Values.v @@ -783,6 +783,18 @@ 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 *) Section COMPARISONS. @@ -1898,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: |