From 997d7f1a90eb7f66de8b0c63fc801f9f7ef90d77 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 23 Feb 2021 17:32:54 +0100
Subject: add target_cbranch_expanse

---
 scheduling/RTLpathSE_impl.v | 54 +++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 52 insertions(+), 2 deletions(-)

(limited to 'scheduling')

diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index bd7ae2ad..738057fd 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -529,6 +529,14 @@ Admitted.
 Global Opaque fsval_proj.
 Local Hint Resolve fsval_proj_correct: wlp.
 
+Lemma fsval_list_proj_correct lhsv:
+  WHEN fsval_list_proj lhsv ~> lhsv' THEN forall ge sp rs0 m0,
+  seval_list_hsval ge sp lhsv rs0 m0 = seval_list_hsval ge sp lhsv' rs0 m0.
+Admitted.
+Global Opaque fsval_list_proj.
+Local Hint Resolve fsval_list_proj_correct: wlp.
+
+
 (** ** Assignment of memory *)
 Definition hslocal_set_smem (hst:hsistate_local) hm :=
   {| hsi_smem := hm;
@@ -870,6 +878,48 @@ Local Hint Resolve hslocal_set_sreg_correct: wlp.
 
 (** ** Execution of one instruction *)
 
+
+(* TODO: This function could be defined in a specific file for each target *)
+Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
+  None.
+
+Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
+  (TARGET: target_cbranch_expanse hst c l = Some (c', l'))
+  (LREF : hsilocal_refines ge sp rs0 m0 hst st)
+  (OK: hsok_local ge sp rs0 m0 hst),
+  seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
+  seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
+Proof.
+  unfold target_cbranch_expanse; simpl; intros; try congruence.
+Qed.
+Global Opaque target_cbranch_expanse.
+
+Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) :=
+    match  target_cbranch_expanse prev cond args with
+    | Some (cond', vargs) => 
+      DO vargs' <~ fsval_list_proj vargs;;
+      RET (cond', vargs)
+    | None =>
+      DO vargs <~ hlist_args prev args ;;
+      RET (cond, vargs)
+    end.
+
+Lemma cbranch_expanse_correct hst c l:
+ WHEN cbranch_expanse hst c l ~> r THEN forall ge sp rs0 m0 st
+  (LREF : hsilocal_refines ge sp rs0 m0 hst st)
+  (OK: hsok_local ge sp rs0 m0 hst),
+  seval_condition ge sp (fst r) (hsval_list_proj (snd r)) (si_smem st) rs0 m0 =
+  seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
+Proof.
+  unfold cbranch_expanse.
+  destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify.
+  + destruct p as [c' l']; simpl.
+    exploit target_cbranch_expanse_correct; eauto.
+  + unfold seval_condition; erewrite H; eauto.
+Qed.
+Local Hint Resolve cbranch_expanse_correct: wlp.
+Global Opaque cbranch_expanse.
+
 Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) := 
   match i with
   | Inop pc' => 
@@ -885,13 +935,13 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) :
       RET (Some (hsist_set_local hst pc' next))
   | Icond cond args ifso ifnot _ =>
       let prev := hst.(hsi_local) in
-      DO vargs <~ hlist_args prev args ;;
+      DO res <~ cbranch_expanse prev cond args;;
+      let (cond, vargs) := res in
       let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in
       RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |})
   | _ => RET None
   end.
 
-
 Remark hsiexec_inst_None_correct i hst:
   WHEN hsiexec_inst i hst ~> o THEN forall st, o = None -> siexec_inst i st = None.
 Proof.
-- 
cgit