From 3e47c1b17e8ff03400106a80117eb86d7e7f9da6 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 2 Feb 2021 13:30:57 +0100
Subject: Expansion of Ccompimm in RTL [Admitted checker]

---
 riscV/ValueAOp.v | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

(limited to 'riscV/ValueAOp.v')

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index f4b7b4d6..ec4492ff 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -17,6 +17,15 @@ Require Import Zbits.
 
 (** Value analysis for RISC V operators *)
 
+Definition zero32 := (I Int.zero).
+  
+Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 vz: aval): B :=
+  match optR0 with
+  | None => sem v1 v2
+  | Some true => sem vz v1
+  | Some false => sem v1 vz
+  end.
+
 Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
   match cond, vl with
   | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2
@@ -137,6 +146,13 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osingleoflong, v1::nil => singleoflong v1
   | Osingleoflongu, v1::nil => singleoflongu v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
+  | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32)
+  | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32)
+  | OEsltw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32)
+  | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n))
+  | OExoriw n, v1::nil => xor v1 (I n)
+  | OEluiw n, nil => I (Int.shl n (Int.repr 12))
+  | OEaddiwr0 n, nil => add (I n) zero32
   | _, _ => Vbot
   end.
 
@@ -201,6 +217,29 @@ Proof.
   rewrite Ptrofs.add_zero_l; eauto with va.
 Qed.
 
+Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR0 m,
+  c = Ceq \/ c = Cne ->
+  vmatch bc a1 b1 ->
+  vmatch bc a0 b0 ->
+  vmatch bc (Op.apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32)
+  (of_optbool (apply_bin_r0 optR0 (cmpu_bool c) b1 b0 zero32)).
+Proof.
+  intros.
+  destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0;
+  apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
+Qed.
+
+Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0,
+  vmatch bc a1 b1 ->
+  vmatch bc a0 b0 ->
+  vmatch bc (Op.apply_bin_r0 optR0 (Val.cmp Clt) a1 a0 Op.zero32)
+  (of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) b1 b0 zero32)).
+Proof.
+  intros.
+  destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0;
+  apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
+Qed.
+
 Theorem eval_static_operation_sound:
   forall op vargs m vres aargs,
   eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres ->
@@ -213,6 +252,11 @@ Proof.
   destruct (propagate_float_constants tt); constructor.
   rewrite Ptrofs.add_zero_l; eauto with va.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
+  
+  1,2: apply eval_cmpu_sound; auto.
+  apply eval_cmp_sound; auto.
+  unfold Val.cmp; apply of_optbool_sound; eauto with va.
+  unfold zero32; simpl. eauto with va.
 Qed.
 
 End SOUNDNESS.
-- 
cgit