diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 09:02:58 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 09:02:58 +0200 |
commit | 28312ed4869e3f63b0a113095d3344c0055ee2c5 (patch) | |
tree | 0726cb598de828429de082ab8978e27e9d089a4c /mppa_k1c | |
parent | cb3dc9a89d66741f4452becaf51d03a656e8e150 (diff) | |
parent | f2e996383571ba2cb794f9ecf9487a53bd370a0c (diff) | |
download | compcert-kvx-28312ed4869e3f63b0a113095d3344c0055ee2c5.tar.gz compcert-kvx-28312ed4869e3f63b0a113095d3344c0055ee2c5.zip |
Merge branch 'mppa-bitfields' into mppa-work
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/SelectLong.vp | 30 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 56 |
2 files changed, 86 insertions, 0 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index a2bc0587..3b9e5bf9 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -24,6 +24,7 @@ Require Import Op CminorSel. Require Import OpHelpers. Require Import SelectOp SplitLong. Require Import ExtValues. +Require Import DecBoolOps. Local Open Scope cminorsel_scope. Local Open Scope string_scope. @@ -311,6 +312,31 @@ Nondetfunction orl (e1: expr) (e2: expr) := && Int64.eq zero1 Int64.zero then Eop (Oselectl (Ccompl0 Cne)) (v0:::v1:::y0:::Enil) else Eop Oorl (e1:::e2:::Enil) + | (Eop (Oandlimm nmask) (prev:::Enil)), + (Eop (Oandlimm mask) + ((Eop (Oshllimm start) (fld:::Enil)):::Enil)) => + let zstart := Int.unsigned start in + let zstop := int64_highest_bit mask in + if is_bitfieldl zstop zstart + then + let mask' := Int64.repr (zbitfield_mask zstop zstart) in + if and_dec (Int64.eq_dec mask mask') + (Int64.eq_dec nmask (Int64.not mask')) + then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil) + else Eop Oorl (e1:::e2:::Enil) + else Eop Oorl (e1:::e2:::Enil) + | (Eop (Oandlimm nmask) (prev:::Enil)), + (Eop (Oandlimm mask) (fld:::Enil)) => + let zstart := 0 in + let zstop := int64_highest_bit mask in + if is_bitfieldl zstop zstart + then + let mask' := Int64.repr (zbitfield_mask zstop zstart) in + if and_dec (Int64.eq_dec mask mask') + (Int64.eq_dec nmask (Int64.not mask')) + then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil) + else Eop Oorl (e1:::e2:::Enil) + else Eop Oorl (e1:::e2:::Enil) | _, _ => Eop Oorl (e1:::e2:::Enil) end. @@ -421,3 +447,7 @@ Definition singleoflong (e: expr) := SplitLong.singleoflong e. Definition singleoflongu (e: expr) := SplitLong.singleoflongu e. End SELECT. + +(* Local Variables: *) +(* mode: coq *) +(* End: *)
\ No newline at end of file diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index b3cb1ce0..cf8eed2b 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -24,6 +24,7 @@ Require Import Cminor Op CminorSel. Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. +Require Import DecBoolOps. Local Open Scope cminorsel_scope. Local Open Scope string_scope. @@ -588,6 +589,61 @@ Proof. rewrite Int64.and_zero. rewrite Int64.or_zero. reflexivity. + + - (*insfl first case*) + destruct (is_bitfieldl _ _) eqn:Risbitfield. + + destruct (and_dec _ _) as [[Rmask Rnmask] | ]. + * rewrite Rnmask in *. + inv H. inv H0. inv H4. inv H3. inv H9. inv H8. + simpl in H6, H7. + inv H6. inv H7. + inv H4. inv H3. inv H7. + simpl in H6. + inv H6. + set (zstop := (int64_highest_bit mask)) in *. + set (zstart := (Int.unsigned start)) in *. + + TrivialExists. + simpl. f_equal. + + unfold insfl. + rewrite Risbitfield. + rewrite Rmask. + simpl. + unfold bitfield_maskl. + subst zstart. + rewrite Int.repr_unsigned. + reflexivity. + * TrivialExists. + + TrivialExists. + - destruct (is_bitfieldl _ _) eqn:Risbitfield. + + destruct (and_dec _ _) as [[Rmask Rnmask] | ]. + * rewrite Rnmask in *. + inv H. inv H0. inv H4. inv H6. inv H8. inv H3. inv H8. + inv H0. simpl in H7. inv H7. + set (zstop := (int64_highest_bit mask)) in *. + set (zstart := 0) in *. + + TrivialExists. simpl. f_equal. + unfold insfl. + rewrite Risbitfield. + rewrite Rmask. + simpl. + subst zstart. + f_equal. + destruct v0; simpl; trivial. + unfold Int.ltu, Int64.iwordsize', Int64.zwordsize, Int64.wordsize. + rewrite Int.unsigned_repr. + ** rewrite Int.unsigned_repr. + *** simpl. + rewrite Int64.shl'_zero. + reflexivity. + *** simpl. unfold Int.max_unsigned. unfold Int.modulus. + simpl. omega. + ** unfold Int.max_unsigned. unfold Int.modulus. + simpl. omega. + * TrivialExists. + + TrivialExists. - TrivialExists. Qed. |