From 70db0c8a5cd5fb21e92de32cc4eb5774baf60610 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 4 Apr 2019 06:07:00 +0200 Subject: prepare for conditions in cmove --- mppa_k1c/Asmblockgenproof1.v | 8 ++++---- mppa_k1c/NeedOp.v | 8 ++++---- mppa_k1c/Op.v | 33 ++++++++++++++++++++++++--------- mppa_k1c/SelectOpproof.v | 4 ++-- 4 files changed, 34 insertions(+), 19 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index f75f0bd3..698d64d6 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1642,7 +1642,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold select. + * unfold eval_select. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. @@ -1656,7 +1656,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold selectl. + * unfold eval_selectl. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. @@ -1670,7 +1670,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold selectl. + * unfold eval_selectf. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. @@ -1684,7 +1684,7 @@ Opaque Int.eq. + eapply exec_straight_one. simpl; reflexivity. + split. - * unfold selectl. + * unfold eval_selectfs. destruct (rs x1) eqn:eqX1; try constructor. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index f3ce8361..ee3c4e27 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -192,7 +192,7 @@ Lemma select_sound: vagree v0 w0 (default x) -> vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> - vagree (select v0 v1 v2) (select w0 w1 w2) x. + vagree (eval_select v0 v1 v2) (eval_select w0 w1 w2) x. Proof. unfold default; intros. destruct x; trivial. @@ -213,7 +213,7 @@ Lemma selectl_sound: vagree v0 w0 (default x) -> vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> - vagree (selectl v0 v1 v2) (selectl w0 w1 w2) x. + vagree (eval_selectl v0 v1 v2) (eval_selectl w0 w1 w2) x. Proof. unfold default; intros. destruct x; trivial. @@ -232,7 +232,7 @@ Lemma selectf_sound: vagree v0 w0 (default x) -> vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> - vagree (selectf v0 v1 v2) (selectf w0 w1 w2) x. + vagree (eval_selectf v0 v1 v2) (eval_selectf w0 w1 w2) x. Proof. unfold default; intros. destruct x; trivial. @@ -251,7 +251,7 @@ Lemma selectfs_sound: vagree v0 w0 (default x) -> vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> - vagree (selectfs v0 v1 v2) (selectfs w0 w1 w2) x. + vagree (eval_selectfs v0 v1 v2) (eval_selectfs w0 w1 w2) x. Proof. unfold default; intros. destruct x; trivial. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 5afd0cb9..551d2dfb 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -51,6 +51,12 @@ Inductive condition : Type := | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *) +Inductive condition0 : Type := + | Ccomp0 (c: comparison) (**r signed integer comparison with 0 *) + | Ccompu0 (c: comparison) (**r unsigned integer comparison with 0 *) + | Ccompl0 (c: comparison) (**r signed 64-bit integer comparison with 0 *) + | Ccomplu0 (c: comparison). (**r unsigned 64-bit integer comparison with 0 *) + (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -237,7 +243,7 @@ Global Opaque eq_condition eq_addressing eq_operation. to lists of values. Return [None] when the computation can trigger an error, e.g. integer division by zero. [eval_condition] returns a boolean, [eval_operation] and [eval_addressing] return a value. *) - + Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2 @@ -254,8 +260,17 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) | _, _ => None end. + +Definition eval_condition0 (cond: condition0) (vl: list val) (m: mem): option bool := + match cond, vl with + | Ccomp0 c, v1 :: nil => Val.cmp_bool c v1 (Vint Int.zero) + | Ccompu0 c, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint Int.zero) + | Ccompl0 c, v1 :: nil => Val.cmpl_bool c v1 (Vlong Int64.zero) + | Ccomplu0 c, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong Int64.zero) + | _, _ => None + end. -Definition select (v0 : val) (v1 : val) (vselect : val) : val := +Definition eval_select (v0 : val) (v1 : val) (vselect : val) : val := match vselect with | Vint iselect => match v0 with @@ -272,7 +287,7 @@ Definition select (v0 : val) (v1 : val) (vselect : val) : val := | _ => Vundef end. -Definition selectl (v0 : val) (v1 : val) (vselect : val) : val := +Definition eval_selectl (v0 : val) (v1 : val) (vselect : val) : val := match vselect with | Vint iselect => match v0 with @@ -289,7 +304,7 @@ Definition selectl (v0 : val) (v1 : val) (vselect : val) : val := | _ => Vundef end. -Definition selectf (v0 : val) (v1 : val) (vselect : val) : val := +Definition eval_selectf (v0 : val) (v1 : val) (vselect : val) : val := match vselect with | Vint iselect => match v0 with @@ -306,7 +321,7 @@ Definition selectf (v0 : val) (v1 : val) (vselect : val) : val := | _ => Vundef end. -Definition selectfs (v0 : val) (v1 : val) (vselect : val) : val := +Definition eval_selectfs (v0 : val) (v1 : val) (vselect : val) : val := match vselect with | Vint iselect => match v0 with @@ -451,10 +466,10 @@ Definition eval_operation | Osingleoflong, v1::nil => Val.singleoflong v1 | Osingleoflongu, v1::nil => Val.singleoflongu v1 | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) - | Oselect, v0::v1::vselect::nil => Some (select v0 v1 vselect) - | Oselectl, v0::v1::vselect::nil => Some (selectl v0 v1 vselect) - | Oselectf, v0::v1::vselect::nil => Some (selectf v0 v1 vselect) - | Oselectfs, v0::v1::vselect::nil => Some (selectfs v0 v1 vselect) + | Oselect, v0::v1::vselect::nil => Some (eval_select v0 v1 vselect) + | Oselectl, v0::v1::vselect::nil => Some (eval_selectl v0 v1 vselect) + | Oselectf, v0::v1::vselect::nil => Some (eval_selectf v0 v1 vselect) + | Oselectfs, v0::v1::vselect::nil => Some (eval_selectfs v0 v1 vselect) | _, _ => None end. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 5a19510a..20ba74a1 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -568,7 +568,7 @@ Proof. predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT. TrivialExists. simpl in *. - unfold select. + unfold eval_select. f_equal. inv H6. inv H7. @@ -606,7 +606,7 @@ Proof. predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT. TrivialExists. simpl in *. - unfold select. + unfold eval_select. f_equal. inv H6. inv H7. -- cgit