Merge branch 'riscv-work-rules' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into riscv-work-rules

1 files changed, 52 insertions, 2 deletions

diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index a7f1323d..d4ea09d6 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;
@@ -853,6 +861,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' => 
@@ -868,13 +918,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.