From 313443c86dfecd9058949ccf58800874eebd22f6 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 23 Feb 2021 19:30:24 +0100
Subject: [Intermediate] Adding fake hsval for Ccomp expansion

---
 riscV/RTLpathSE_simplify.v | 111 +++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 108 insertions(+), 3 deletions(-)

(limited to 'riscV/RTLpathSE_simplify.v')

diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 4fadcfdc..b9fe504e 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -1,9 +1,114 @@
+Require Import Integers.
 Require Import Op Registers.
 Require Import RTLpathSE_theory.
 Require Import RTLpathSE_simu_specs.
 
+(* Useful functions for conditions/branches expansion *)
+
+Definition is_inv_cmp_int (cmp: comparison) : bool :=
+  match cmp with | Cle | Cgt => true | _ => false end.
+
+Definition is_inv_cmp_float (cmp: comparison) : bool :=
+  match cmp with | Cge | Cgt => true | _ => false end.
+
+Definition make_optR0 (is_x0 is_inv: bool) : option bool :=
+  if is_x0 then Some is_inv else None.
+
+(* Functions to manage lists of "fake" values *)
+
+Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval :=
+  let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in
+  let lhsv := fScons hvfirst fSnil in
+  fScons hvsec lhsv.
+
+Definition make_lhsv_single (hvs: hsval) : list_hsval :=
+  fScons hvs fSnil.
+
+(* Expansion functions *)
+
+Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
+  match cmp with
+  | Ceq => fSop (OEseqw optR0) lhsv
+  | Cne => fSop (OEsnew optR0) lhsv
+  | Clt | Cgt => fSop (OEsltw optR0) lhsv
+  | Cle | Cge =>
+      let hvs := (fSop (OEsltw optR0) lhsv) in
+      let hl := make_lhsv_single hvs in
+      fSop (OExoriw Int.one) hl
+  end.
+
+(* Target op simplifications using "fake" values *)
+
 Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
-  None.  (* default implementation *)
+  match op, lr with
+  | Ocmp (Ccomp c), a1 :: a2 :: nil =>
+      let fv1 := fsi_sreg_get hst a1 in
+      let fv2 := fsi_sreg_get hst a2 in
+      let is_inv := is_inv_cmp_int c in
+      let optR0 := make_optR0 false is_inv in
+      let lhsv := make_lhsv_cmp is_inv fv1 fv2 in
+      Some (cond_int32s c lhsv optR0)
+
+      (*| Ocmp (Ccompu c), a1 :: a2 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst a1;;
+      DO hv2 <~ hsi_sreg_get hst a2;;
+      let is_inv := is_inv_cmp_int c in
+      let optR0 := make_optR0 false is_inv in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+      cond_int32u c lhsv optR0
+  | Ocmp (Ccompimm c imm), a1 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst a1;;
+      expanse_condimm_int32s c hv1 imm
+  | Ocmp (Ccompuimm c imm), a1 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst a1;;
+      expanse_condimm_int32u c hv1 imm
+  | Ocmp (Ccompl c), a1 :: a2 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst a1;;
+      DO hv2 <~ hsi_sreg_get hst a2;;
+      let is_inv := is_inv_cmp_int c in
+      let optR0 := make_optR0 false is_inv in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+      cond_int64s c lhsv optR0
+  | Ocmp (Ccomplu c), a1 :: a2 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst a1;;
+      DO hv2 <~ hsi_sreg_get hst a2;;
+      let is_inv := is_inv_cmp_int c in
+      let optR0 := make_optR0 false is_inv in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+      cond_int64u c lhsv optR0
+  | Ocmp (Ccomplimm c imm), a1 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst a1;;
+      expanse_condimm_int64s c hv1 imm
+  | Ocmp (Ccompluimm c imm), a1 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst a1;;
+      expanse_condimm_int64u c hv1 imm
+  | Ocmp (Ccompf c), f1 :: f2 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst f1;;
+      DO hv2 <~ hsi_sreg_get hst f2;;
+      let is_inv := is_inv_cmp_float c in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+      expanse_cond_fp false cond_float c lhsv
+  | Ocmp (Cnotcompf c), f1 :: f2 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst f1;;
+      DO hv2 <~ hsi_sreg_get hst f2;;
+      let is_inv := is_inv_cmp_float c in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+      expanse_cond_fp true cond_float c lhsv
+  | Ocmp (Ccompfs c), f1 :: f2 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst f1;;
+      DO hv2 <~ hsi_sreg_get hst f2;;
+      let is_inv := is_inv_cmp_float c in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+      expanse_cond_fp false cond_single c lhsv
+  | Ocmp (Cnotcompfs c), f1 :: f2 :: nil =>
+      DO hv1 <~ hsi_sreg_get hst f1;;
+      DO hv2 <~ hsi_sreg_get hst f2;;
+      let is_inv := is_inv_cmp_float c in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+         expanse_cond_fp true cond_single c lhsv*)
+  | _, _ => None
+  end.
+
 
 Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
    (H: target_op_simplify op lr hst = Some fsv)
@@ -12,8 +117,8 @@ Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
    (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args)
    (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m),
    seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m.
-Proof.
+Proof. Admitted. (*
   unfold target_op_simplify; simpl. congruence.
-Qed.
+                    Qed.*)
 Global Opaque target_op_simplify.
 
-- 
cgit