diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 13:33:43 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 13:33:43 +0100 |
commit | a47d709fd9251f58032444fde27a3ad7e947c26d (patch) | |
tree | 8270330b3037657d5b5b28bb722ed4dd283ae0cf | |
parent | 7afc85c95aaec5cc0935733cac487e13f114cc46 (diff) | |
download | compcert-kvx-a47d709fd9251f58032444fde27a3ad7e947c26d.tar.gz compcert-kvx-a47d709fd9251f58032444fde27a3ad7e947c26d.zip |
Pselectd
-rw-r--r-- | riscV/ExtValues.v | 10 | ||||
-rw-r--r-- | riscV/SelectOp.vp | 4 | ||||
-rw-r--r-- | riscV/SelectOpproof.v | 19 |
3 files changed, 33 insertions, 0 deletions
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v index 3f283cdc..aebbe5c5 100644 --- a/riscV/ExtValues.v +++ b/riscV/ExtValues.v @@ -101,3 +101,13 @@ Proof. rewrite Int.eq_false. reflexivity. cbv. discriminate. Qed. + +Lemma float_bits_normalize: + forall v1, + ExtValues.float_of_bits (Val.normalize (ExtValues.bits_of_float v1) AST.Tlong) = + Val.normalize v1 AST.Tfloat. +Proof. + destruct v1; cbn; trivial. + f_equal. + apply Float.of_to_bits. +Qed. diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index 0e82f8ba..b6720e40 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -429,6 +429,10 @@ Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) ((Eop (Ocmp cond) args) ::: (Eop Ocast32signed (e1 ::: Enil)) ::: (Eop Ocast32signed (e2 ::: Enil)) ::: Enil)) ::: Enil)) + | Tfloat => Some (Eop Ofloat_of_bits ((Eop Oselectl + ((Eop (Ocmp cond) args) ::: + (Eop Obits_of_float (e1 ::: Enil)) ::: + (Eop Obits_of_float (e2 ::: Enil)) ::: Enil)) ::: Enil)) | _ => None end else None. diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 7f7474b6..c313fbaf 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -962,6 +962,25 @@ Proof. * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption. - inv H. TrivialExists. + cbn. constructor. + { econstructor. + { constructor. + { econstructor. eassumption. cbn. rewrite H3. reflexivity. } + constructor. econstructor. constructor. eassumption. + constructor. cbn. reflexivity. + constructor. econstructor. constructor. eassumption. constructor. + cbn. reflexivity. constructor. + } + constructor. + } + constructor. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + destruct b. + * rewrite ExtValues.select01_long_true. + apply ExtValues.float_bits_normalize. + * rewrite ExtValues.select01_long_false. + apply ExtValues.float_bits_normalize. + - inv H. TrivialExists. + + cbn. constructor. { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. } constructor. eassumption. constructor. eassumption. constructor. + cbn. f_equal. rewrite ExtValues.normalize_select01. |