From bb185aa85ddf32feed61d7888c1b199fffdd821f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 25 Apr 2019 10:32:38 +0200 Subject: IT COMPILES --- mppa_k1c/Asm.v | 2 +- mppa_k1c/Asmvliw.v | 2 +- mppa_k1c/Op.v | 4 ++-- mppa_k1c/SelectOp.vp | 10 ++++----- mppa_k1c/SelectOpproof.v | 53 +++++++++++++++++++++++++----------------------- mppa_k1c/ValueAOp.v | 12 +++++------ 6 files changed, 43 insertions(+), 40 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 2c3eef1f..290691f4 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -130,7 +130,7 @@ Inductive instruction : Type := | Psxwd (rd rs: ireg) (**r Sign Extend Word to Double Word *) | Pzxwd (rd rs: ireg) (**r Zero Extend Word to Double Word *) - | Pextfz (rd : ireg) (rs : ireg) (stop : int) (start : int) (**r extract bitfields unsigned *) + | Pextfz (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *) | Pfabsd (rd rs: ireg) (**r float absolute double *) | Pfabsw (rd rs: ireg) (**r float absolute word *) | Pfnegd (rd rs: ireg) (**r float negate double *) diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index a347b6fc..b39ebd0e 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -307,7 +307,7 @@ Inductive arith_name_rr : Type := | Psxwd (**r Sign Extend Word to Double Word *) | Pzxwd (**r Zero Extend Word to Double Word *) (* | Pextfs (stop : int) (start : int) (**r extract bit field, signed *) *) - | Pextfz (stop : int) (start : int) (**r extract bit field, unsigned *) + | Pextfz (stop : Z) (start : Z) (**r extract bit field, unsigned *) | Pfabsd (**r float absolute double *) | Pfabsw (**r float absolute word *) diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 8180c43f..8293af1e 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -198,7 +198,7 @@ Inductive operation : Type := | Oselectl (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) | Oselectf (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) | Oselectfs (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) - | Oextfz (stop : int) (start : int). + | Oextfz (stop : Z) (start : Z). (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -233,7 +233,7 @@ Defined. Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0 Z.eq_dec; intros. decide equality. Defined. diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 8f953425..3e36a51c 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -203,11 +203,11 @@ Nondetfunction shrimm (e1: expr) (n: int) := then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil) | Eop (Oshlimm n1) (t1:::Enil) => - let stop := Int.sub Int.iwordsize (Int.add n1 Int.one) in - let start := Int.sub (Int.add (Int.add n stop) Int.one) Int.iwordsize in - if (Int.cmp Cle start stop) - && (Int.cmp Cge start Int.zero) - && (Int.cmp Clt stop Int.iwordsize) + let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in + let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in + if (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int.zwordsize) then Eop (Oextfz stop start) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil) | _ => diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 954ffba2..d072bb7b 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -321,7 +321,7 @@ Proof. predSpec Int.eq Int.eq_spec n Int.zero. intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto. - destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl. + destruct (Int.ltu n Int.iwordsize) eqn:LT. destruct (shrimm_match a); intros; InvEval. - exists (Vint (Int.shr n1 n)); split. EvalOp. simpl. rewrite LT; auto. @@ -335,34 +335,37 @@ Proof. subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. simpl. auto. - subst x. + simpl negb. + cbn iota. destruct (_ && _ && _) eqn:BOUNDS. - + exists (Val.extfz (Int.sub Int.iwordsize (Int.add n1 Int.one)) - (Int.sub - (Int.add - (Int.add n (Int.sub Int.iwordsize (Int.add n1 Int.one))) - Int.one) Int.iwordsize) v1). + + exists (Val.extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) + (Z.sub + (Z.add + (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))) + Z.one) Int.zwordsize) v1). split. ++ EvalOp. ++ unfold Val.extfz. - * simpl. rewrite BOUNDS. - destruct v1; simpl; trivial. - destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial. - destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial. - replace (Int.sub Int.iwordsize - (Int.add (Int.sub Int.iwordsize (Int.add n1 Int.one)) Int.one)) with n1. - replace (Int.sub Int.iwordsize - (Int.sub - (Int.add (Int.sub Int.iwordsize (Int.add n1 Int.one)) Int.one) - (Int.sub - (Int.add - (Int.add n (Int.sub Int.iwordsize (Int.add n1 Int.one))) - Int.one) Int.iwordsize))) with n. - constructor. - ** repeat (try rewrite Int.add_signed; try rewrite Int.sub_signed; try rewrite Int.signed_repr). - rewrite <- (Int.repr_signed n) at 1. - f_equal. - omega. - + rewrite BOUNDS. + destruct v1; try (simpl; apply Val.lessdef_undef). + replace (Z.sub Int.zwordsize + (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1). + replace (Z.sub Int.zwordsize + (Z.sub + (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one) + (Z.sub + (Z.add + (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))) + Z.one) Int.zwordsize))) with (Int.unsigned n). + * rewrite Int.repr_unsigned. + rewrite Int.repr_unsigned. + simpl. + destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial. + simpl. + destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial. + * omega. + * omega. + + TrivialExists. constructor. econstructor. constructor. eassumption. constructor. simpl. reflexivity. constructor. simpl. reflexivity. - TrivialExists. - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto. diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 64002cef..e498d237 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -75,15 +75,15 @@ Definition eval_static_selectfs (cond : condition0) (v0 v1 vselect : aval) : ava end. -Definition eval_static_extfz (stop : int) (start : int) (v : aval) := - if (Int.cmp Cle start stop) - && (Int.cmp Cge start Int.zero) - && (Int.cmp Clt stop Int.iwordsize) +Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) := + if (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int.zwordsize) then - let stop' := Int.add stop Int.one in + let stop' := Z.add stop Z.one in match v with | I w => - I (Int.shr (Int.shl w (Int.sub Int.iwordsize stop')) (Int.sub Int.iwordsize (Int.sub stop' start))) + I (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start)))) | _ => Vtop end else Vtop. -- cgit