some advance

1 files changed, 154 insertions, 14 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index 5c974efd..bf47b6da 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -1,4 +1,4 @@
-Require Import AST Maps.
+Require Import Coqlib AST Maps.
 Require Import Op Registers.
 Require Import RTL BTL.
 Require Import BTL_SEsimuref BTL_SEtheory OptionMonad.
@@ -13,6 +13,10 @@ Local Open Scope impure.
 Import ListNotations.
 Local Open Scope list_scope.
 
+(** Tactics *)
+
+Ltac simplify_SOME x := repeat inversion_SOME x; try_simplify_someHyps.
+
 (** Notations to make lemmas more readable *)
 Notation "'sval_refines' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2)
   (only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level): hse.
@@ -160,10 +164,10 @@ Definition hSload (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr:
    hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := hv |}.
 
 Lemma hSload_correct sm1 trap chunk addr lsv1:
-  WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2 hid
+  WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2
     (LR: list_sval_refines ctx lsv1 lsv2)
     (MR: smem_refines ctx sm1 sm2),
-    sval_refines ctx hv (Sload sm2 trap chunk addr lsv2 hid).
+    sval_refines ctx hv (Sload sm2 trap chunk addr lsv2 unknown_hid).
 Proof.
   wlp_simplify.
   rewrite <- LR, <- MR.
@@ -254,25 +258,161 @@ Qed.
 Global Opaque hSstore.
 Local Hint Resolve hSstore_correct: wlp.
 
-Definition hris_sreg_eval ctx hris r := eval_sval ctx (ris_sreg_get hris r).
+Definition hrs_sreg_eval ctx hrs r := eval_sval ctx (ris_sreg_get hrs r).
 
-Definition hris_sreg_get (hris: ristate) r: ?? sval :=
-   match PTree.get r hris with
-   | None => if ris_input_init hris then hSinput r else hSundef
+Definition hrs_sreg_get (hrs: ristate) r: ?? sval :=
+   match PTree.get r hrs with
+   | None => if ris_input_init hrs then hSinput r else hSundef
    | Some sv => RET sv
    end.
-Coercion hris_sreg_get: ristate >-> Funclass.
+Coercion hrs_sreg_get: ristate >-> Funclass.
 
-Lemma hris_sreg_get_correct hris r:
-  WHEN hris_sreg_get hris r ~> sv THEN forall ctx (f: reg -> sval)
-  (RR: forall r, hris_sreg_eval ctx hris r = eval_sval ctx (f r)),
+Lemma hrs_sreg_get_correct hrs r:
+  WHEN hrs_sreg_get hrs r ~> sv THEN forall ctx (f: reg -> sval)
+  (RR: forall r, hrs_sreg_eval ctx hrs r = eval_sval ctx (f r)),
   sval_refines ctx sv (f r).
 Proof.
-  unfold hris_sreg_eval, ris_sreg_get. wlp_simplify; rewrite <- RR; rewrite H; auto;
+  unfold hrs_sreg_eval, ris_sreg_get. wlp_simplify; rewrite <- RR; rewrite H; auto;
   rewrite H0, H1; simpl; auto.
 Qed.
-Global Opaque hris_sreg_get.
-Local Hint Resolve hris_sreg_get_correct: wlp.
+Global Opaque hrs_sreg_get.
+Local Hint Resolve hrs_sreg_get_correct: wlp.
+
+Fixpoint hlist_args (hrs: ristate) (l: list reg): ?? list_sval :=
+  match l with
+  | nil => hSnil()
+  | r::l =>
+    DO v <~ hrs_sreg_get hrs r;;
+    DO lsv <~ hlist_args hrs l;;
+    hScons v lsv
+  end.
+
+Lemma hlist_args_correct hrs l:
+  WHEN hlist_args hrs l ~> lsv THEN forall ctx (f: reg -> sval)
+    (RR: forall r, hrs_sreg_eval ctx hrs r = eval_sval ctx (f r)),
+    list_sval_refines ctx lsv (list_sval_inj (List.map f l)).
+Proof.
+  induction l; wlp_simplify.
+Qed.
+Global Opaque hlist_args.
+Local Hint Resolve hlist_args_correct: wlp.
+
+(** Convert a "fake" hash-consed term into a "real" hash-consed term *)
+
+Fixpoint fsval_proj sv: ?? sval :=
+  match sv with
+  | Sundef hc =>
+      DO b <~ phys_eq hc unknown_hid;;
+      if b then hSundef else RET sv
+  | Sinput r hc => 
+      DO b <~ phys_eq hc unknown_hid;;
+      if b then hSinput r (* was not yet really hash-consed *)
+      else RET sv (* already hash-consed *)
+  | Sop op hl hc => 
+      DO b <~ phys_eq hc unknown_hid;;
+      if b then (* was not yet really hash-consed *) 
+        DO hl' <~ fsval_list_proj hl;;
+        hSop op hl'
+      else RET sv (* already hash-consed *)
+  | Sload hm t chk addr hl _ => RET sv (* FIXME TODO gourdinl ? *)
+  end
+with fsval_list_proj sl: ?? list_sval :=
+  match sl with
+  | Snil hc => 
+      DO b <~ phys_eq hc unknown_hid;;
+      if b then hSnil() (* was not yet really hash-consed *)
+      else RET sl (* already hash-consed *)
+  | Scons hv hl hc => 
+      DO b <~ phys_eq hc unknown_hid;;
+      if b then (* was not yet really hash-consed *)
+        DO hv' <~ fsval_proj hv;;
+        DO hl' <~ fsval_list_proj hl;;
+        hScons hv' hl' 
+      else RET sl (* already hash-consed *)
+  end.
+
+Lemma fsval_proj_correct sv:
+  WHEN fsval_proj sv ~> sv' THEN forall ctx,
+  eval_sval ctx sv = eval_sval ctx sv'.
+Proof.
+ induction sv using sval_mut 
+ with (P0 := fun lsv => 
+       WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx,
+         eval_list_sval ctx lsv = eval_list_sval ctx lsv')
+       (P1 := fun sm => True); try (wlp_simplify; tauto).
+ - wlp_xsimplify ltac:(intuition eauto with wlp_raw wlp).
+   rewrite H, H0; auto.
+ - wlp_simplify; erewrite H0, H1; eauto.
+Qed.
+Global Opaque fsval_proj.
+Local Hint Resolve fsval_proj_correct: wlp.
+
+Lemma fsval_list_proj_correct lsv:
+  WHEN fsval_list_proj lsv ~> lsv' THEN forall ctx,
+  eval_list_sval ctx lsv = eval_list_sval ctx lsv'.
+Proof.
+  induction lsv; wlp_simplify.
+  erewrite H0, H1; eauto.
+Qed.
+Global Opaque fsval_list_proj.
+Local Hint Resolve fsval_list_proj_correct: wlp.
+
+(** ** Assignment of memory *)
+
+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;;
+  RET (rset_smem hm hrs).
+
+Lemma hrexec_store_correct chunk addr args src hrs:
+  WHEN hrexec_store chunk addr args src hrs ~> hrs' THEN forall ctx sis
+  (REF: ris_refines ctx hrs sis),
+  ris_refines ctx hrs' (sexec_store chunk addr args src sis).
+Proof.
+  wlp_simplify.
+  eapply rset_mem_correct; simpl; eauto.
+  - intros X; erewrite H1; eauto.
+    rewrite X. simplify_SOME z.
+  - intros X; inversion REF.
+    erewrite H1; eauto.
+Qed.
+
+(** ** Assignment of registers *)
+
+(** locally new symbolic values during symbolic execution *)
+Inductive root_sval: Type :=
+| Rop (op: operation)
+| Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing)
+.
+
+Definition root_apply (rsv: root_sval) (lr: list reg) (st: sistate): sval :=
+  let lsv := list_sval_inj (List.map (si_sreg st) lr) in
+  let sm := si_smem st in
+  match rsv with
+  | Rop op => fSop op lsv
+  | Rload trap chunk addr => fSload sm trap chunk addr lsv
+  end.
+Coercion root_apply: root_sval >-> Funclass.
+
+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
+  end.
+
+Lemma root_happly_correct (rsv: root_sval) lr hrs:
+  WHEN root_happly rsv lr hrs ~> sv THEN forall ctx st
+  (REF: ris_refines ctx hrs st)
+  (OK: ris_ok ctx hrs),
+  sval_refines ctx sv (rsv lr st).
+Proof.
+  unfold root_apply, root_happly; destruct rsv; wlp_simplify; inv REF;
+  erewrite H0, H; eauto.
+Qed.
+Global Opaque root_happly.
+Hint Resolve root_happly_correct: wlp.
 
 Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
   match o with