From 7bc2a5e6d2694f144e49fe60af6ddfd0e8a0aba0 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 30 Jun 2021 15:59:25 +0200
Subject: coercions and simplify

---
 scheduling/BTL_SEimpl.v    | 92 +++++++++++++++++++++++++++++++++++++++++++++-
 scheduling/BTL_SEsimuref.v |  2 +-
 2 files changed, 91 insertions(+), 3 deletions(-)

(limited to 'scheduling')

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index bf47b6da..f01f1cc0 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -362,7 +362,7 @@ Local Hint Resolve fsval_list_proj_correct: wlp.
 Definition hrexec_store chunk addr args src hrs: ?? ristate :=
   DO hargs <~ hlist_args hrs args;;
   DO hsrc <~ hrs_sreg_get hrs src;;
-  DO hm <~ hSstore hrs.(ris_smem) chunk addr hargs hsrc;;
+  DO hm <~ hSstore hrs chunk addr hargs hsrc;;
   RET (rset_smem hm hrs).
 
 Lemma hrexec_store_correct chunk addr args src hrs:
@@ -399,7 +399,7 @@ Definition root_happly (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :
   DO lsv <~ hlist_args hrs lr;;
   match rsv with
   | Rop op => hSop op lsv
-  | Rload trap chunk addr => hSload hrs.(ris_smem) trap chunk addr lsv
+  | Rload trap chunk addr => hSload hrs trap chunk addr lsv
   end.
 
 Lemma root_happly_correct (rsv: root_sval) lr hrs:
@@ -414,6 +414,94 @@ Qed.
 Global Opaque root_happly.
 Hint Resolve root_happly_correct: wlp.
 
+Local Open Scope lazy_bool_scope.
+
+(* NB: return [false] if the rsv cannot fail *)
+Definition may_trap (rsv: root_sval) (lr: list reg): bool :=
+  match rsv with 
+  | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lr) (args_of_operation op))  (* cf. lemma is_trapping_op_sound *)
+  | Rload TRAP _ _  => true
+  | _ => false
+  end.
+
+Lemma lazy_orb_negb_false (b1 b2:bool):
+  (b1 ||| negb b2) = false <-> (b1 = false /\ b2 = true).
+Proof.
+  unfold negb. repeat autodestruct; simpl; intuition (try congruence).
+Qed.
+
+Lemma eval_list_sval_length ctx (f: reg -> sval) (l:list reg):
+  forall l', eval_list_sval ctx (list_sval_inj (List.map f l)) = Some l' ->
+  Datatypes.length l = Datatypes.length l'.
+Proof.
+  induction l.
+  - simpl. intros. inv H. reflexivity.
+  - simpl. intros. destruct (eval_sval _ _); [|discriminate].
+    destruct (eval_list_sval _ _) eqn:SLS; [|discriminate]. inv H. simpl.
+    erewrite IHl; eauto.
+Qed.
+
+Lemma may_trap_correct ctx (rsv: root_sval) (lr: list reg) st:
+  may_trap rsv lr = false -> 
+  eval_list_sval ctx (list_sval_inj (List.map (si_sreg st) lr)) <> None ->
+  eval_smem ctx (si_smem st) <> None ->
+  eval_sval ctx (rsv lr st) <> None.
+Proof.
+  destruct rsv; simpl; try congruence.
+  - rewrite lazy_orb_negb_false. intros (TRAP1 & LEN) OK1 OK2.
+    autodestruct; try congruence. intros.
+    eapply is_trapping_op_sound; eauto.
+    erewrite <- eval_list_sval_length; eauto.
+    apply Nat.eqb_eq in LEN.
+    assumption.
+  - intros X OK1 OK2.
+    repeat autodestruct; try congruence.
+Qed.
+
+(** simplify a symbolic value before assignment to a register *)
+Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :=
+  match rsv with
+  | Rop op =>
+     match is_move_operation op lr with
+     | Some arg => hrs_sreg_get hrs arg (* optimization of Omove *)
+     | None =>
+         DO lsv <~ hlist_args hrs lr;;
+         hSop op lsv
+        (* TODO gourdinl
+       match target_op_simplify op lr hst with
+       | Some fhv => fsval_proj fhv
+       | None =>
+         hSop op lhsv
+           end*)
+     end
+  | Rload _ chunk addr => 
+       DO lhsv <~ hlist_args hrs lr;;
+       hSload hrs NOTRAP chunk addr lhsv
+  end.
+
+Lemma simplify_correct rsv lr hrs:
+  WHEN simplify rsv lr hrs ~> hv THEN forall ctx st
+    (REF: ris_refines ctx hrs st)
+    (OK0: ris_ok ctx hrs)
+    (OK1: eval_sval ctx (rsv lr st) <> None),
+    sval_refines ctx hv (rsv lr st).
+Proof.
+  destruct rsv; simpl; auto.
+  - (* Rop *)
+    destruct (is_move_operation _ _) eqn: Hmove.
+    { wlp_simplify; exploit is_move_operation_correct; eauto.
+      intros (Hop & Hlsv); subst; simpl in *. inv REF.
+      simplify_SOME z; erewrite H; eauto. }
+    wlp_simplify; inv REF. erewrite H0; eauto.
+  - (* Rload *)
+    destruct trap; wlp_simplify; inv REF.
+    + erewrite H0, H, MEM_EQ; eauto.
+      repeat simplify_SOME z.
+      * destruct (Memory.Mem.loadv _ _ _); try congruence.
+      * rewrite H1 in OK1; congruence.
+    + erewrite H0; eauto.
+Qed.
+
 Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
   match o with
   | Some x => RET x
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 9c84532b..66abe6e1 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -20,7 +20,7 @@ Record ristate :=
   { 
     (** [ris_smem] represents the current smem symbolic evaluations.
         (we also recover the history of smem in ris_smem)  *)
-    ris_smem: smem;
+    ris_smem:> smem;
     (** For the values in registers:
         1) we store a list of sval evaluations
         2) we encode the symbolic regset by a PTree + a boolean indicating the default sval
-- 
cgit