start a model of symbolic execution in Continuation-Passing-Style

1 files changed, 233 insertions, 18 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 4d5314f2..8aa8f32b 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -13,12 +13,11 @@ Require Import RTL BTL OptionMonad.
 Ltac inversion_SOME := fail.  (* deprecated tactic of OptionMonad: use autodestruct instead *)
 Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *)
 
-
 Record iblock_exec_context := Bctx {
   cge: BTL.genv;
-  csp: val;
   cstk: list stackframe;
   cf: function;
+  csp: val;
   crs0: regset;
   cm0: mem
 }.
@@ -454,17 +453,17 @@ Proof.
   reflexivity.
 Qed.
 
-Variable sp: val.
 Variable stk stk': list stackframe.
 Variable f f': function.
+Variable sp: val.
 Variable rs0: regset.
 Variable m0: mem.
 
 Lemma eval_sval_preserved sv:
-  eval_sval (Bctx ge sp stk f rs0 m0) sv = eval_sval (Bctx ge' sp stk' f' rs0 m0) sv.
+  eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv.
 Proof.
-  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge sp stk f rs0 m0) lsv = eval_list_sval (Bctx ge' sp stk' f' rs0 m0) lsv)
-                                   (P1 := fun sm => eval_smem (Bctx ge sp stk f rs0 m0) sm = eval_smem (Bctx ge' sp stk' f' rs0 m0) sm); simpl; auto.
+  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv)
+                                   (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto.
   + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto.
     rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto.
     erewrite eval_operation_preserved; eauto.
@@ -482,8 +481,8 @@ Proof.
 Qed.
 
 Lemma seval_builtin_arg_preserved m: forall bs varg,
-  seval_builtin_arg (Bctx ge sp stk f rs0 m0) m bs varg ->
-  seval_builtin_arg (Bctx ge' sp stk' f' rs0 m0) m bs varg.
+  seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg ->
+  seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg.
 Proof.
   induction 1; simpl.
   all: try (constructor; auto).
@@ -493,15 +492,15 @@ Proof.
 Qed.
 
 Lemma seval_builtin_args_preserved m lbs vargs:
-  seval_builtin_args (Bctx ge sp stk f rs0 m0) m lbs vargs ->
-  seval_builtin_args (Bctx ge' sp stk' f' rs0 m0) m lbs vargs.
+  seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs ->
+  seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs.
 Proof.
   induction 1; constructor; eauto.
   eapply seval_builtin_arg_preserved; auto.
 Qed.
 
 Lemma list_sval_eval_preserved lsv: 
-  eval_list_sval (Bctx ge sp stk f rs0 m0) lsv = eval_list_sval (Bctx ge' sp stk' f' rs0 m0) lsv.
+  eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv.
 Proof.
   induction lsv; simpl; auto.
   rewrite eval_sval_preserved. destruct (eval_sval _ _); auto.
@@ -509,7 +508,7 @@ Proof.
 Qed.
 
 Lemma smem_eval_preserved sm: 
-  eval_smem (Bctx ge sp stk f rs0 m0) sm = eval_smem (Bctx ge' sp stk' f' rs0 m0) sm.
+  eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm.
 Proof.
   induction sm; simpl; auto.
   rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
@@ -520,7 +519,7 @@ Proof.
 Qed.
 
 Lemma seval_condition_preserved cond lsv sm:
-  seval_condition (Bctx ge sp stk f rs0 m0) cond lsv sm = seval_condition (Bctx ge' sp stk' f' rs0 m0) cond lsv sm.
+  seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm.
 Proof.
   unfold seval_condition.
   rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
@@ -618,19 +617,235 @@ Proof.
     congruence.
 Qed.
 
+
+(** * symbolic execution of basic instructions *)
+
+Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}.
+
+Lemma sis_init_correct ctx:
+  sem_sistate ctx sis_init (crs0 ctx) (cm0 ctx).
+Proof.
+  unfold sis_init, sem_sistate; simpl; intuition eauto.
+Qed.
+
+Definition set_sreg (r:reg) (sv:sval) (sis:sistate): sistate :=
+  {| si_pre:=(fun ctx => eval_sval ctx (sis.(si_sreg) r) <> None /\ (sis.(si_pre) ctx));
+     si_sreg:=fun y => if Pos.eq_dec r y then sv else sis.(si_sreg) y;
+     si_smem:= sis.(si_smem)|}.
+
+Lemma set_sreg_correct ctx dst sv sis (rs rs': regset) m:
+  sem_sistate ctx sis rs m -> 
+  (eval_sval ctx sv = Some rs' # dst) ->
+  (forall r, r <> dst -> rs'#r = rs#r) ->
+  sem_sistate ctx (set_sreg dst sv sis) rs' m.
+Proof.
+  intros (PRE&MEM&REG) NEW OLD.
+  unfold sem_sistate, set_sreg; simpl.
+  intuition.
+  - rewrite REG in *; congruence.
+  - destruct (Pos.eq_dec dst r); simpl; subst; eauto.
+    rewrite REG in *. rewrite OLD; eauto.
+Qed.
+
+Definition set_smem (sm:smem) (sis:sistate): sistate :=
+  {| si_pre:=(fun ctx => eval_smem ctx sis.(si_smem) <> None /\ (sis.(si_pre) ctx));
+     si_sreg:= sis.(si_sreg);
+     si_smem:= sm |}.
+
+Lemma set_smem_correct ctx sm sis rs m m':
+  sem_sistate ctx sis rs m ->
+  eval_smem ctx sm = Some m' ->
+  sem_sistate ctx (set_smem sm sis) rs m'.
+Proof.
+  intros (PRE&MEM&REG) NEW.
+  unfold sem_sistate, set_smem; simpl.
+  intuition.
+  rewrite MEM in *; congruence.
+Qed.
+
+Definition sexec_op op args dst sis: sistate :=
+   let args := list_sval_inj (List.map sis.(si_sreg) args) in
+   set_sreg dst (Sop op args sis.(si_smem)) sis.
+
+Lemma sexec_op_correct ctx op args dst sis rs m v
+ (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = Some v)
+ (SIS: sem_sistate ctx sis rs m)
+ :(sem_sistate ctx (sexec_op op args dst sis) (rs#dst <- v) m).
+Proof.
+  eapply set_sreg_correct; eauto.
+  - simpl. destruct SIS as (PRE&MEM&REG).
+    rewrite Regmap.gss; simpl; auto.
+    erewrite eval_list_sval_inj; simpl; auto.
+    try_simplify_someHyps.
+  - intros; rewrite Regmap.gso; auto.
+Qed.
+
+Definition sexec_load trap chunk addr args dst sis: sistate :=
+   let args := list_sval_inj (List.map sis.(si_sreg) args) in
+   set_sreg dst (Sload sis.(si_smem) trap chunk addr args) sis.
+
+Lemma sexec_load_TRAP_correct ctx chunk addr args dst sis rs m a v
+ (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a)
+ (LOAD: Mem.loadv chunk m a = Some v)
+ (SIS: sem_sistate ctx sis rs m)
+ :(sem_sistate ctx (sexec_load TRAP chunk addr args dst sis) (rs#dst <- v) m).
+Proof.
+  eapply set_sreg_correct; eauto.
+  - simpl. destruct SIS as (PRE&MEM&REG).
+    rewrite Regmap.gss; simpl; auto.
+    erewrite eval_list_sval_inj; simpl; auto.
+    try_simplify_someHyps.
+  - intros; rewrite Regmap.gso; auto.
+Qed.
+
+Definition sexec_store chunk addr args src sis: sistate :=
+   let args := list_sval_inj (List.map sis.(si_sreg) args) in
+   let src := sis.(si_sreg) src in
+   let sm := Sstore sis.(si_smem) chunk addr args src in
+   set_smem sm sis.
+
+Lemma sexec_store_correct ctx chunk addr args src sis rs m m' a
+ (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a)
+ (STORE: Mem.storev chunk m a (rs # src) = Some m')
+ (SIS: sem_sistate ctx sis rs m)
+ :(sem_sistate ctx (sexec_store chunk addr args src sis) rs m').
+Proof.
+  eapply set_smem_correct; eauto.
+  simpl. destruct SIS as (PRE&MEM&REG).
+  erewrite eval_list_sval_inj; simpl; auto.
+  try_simplify_someHyps.
+  rewrite REG; auto.
+Qed.
+
+Lemma seval_condition_eq ctx cond args sis rs m
+  (SIS : sem_sistate ctx sis rs m)
+  :seval_condition ctx cond (list_sval_inj (map (si_sreg sis) args)) (si_smem sis) = eval_condition cond rs ## args m.
+Proof.
+  destruct SIS as (PRE&MEM&REG); unfold seval_condition; simpl.
+  erewrite eval_list_sval_inj; simpl; auto.
+  erewrite MEM; auto.
+Qed.
+
+(** * symbolic execution of blocks *)
+
 (* symbolic state *)
 Inductive sstate :=
   | Sfinal (sis: sistate) (sfv: sfval)
   | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate)
+  | Sdead
  .
 
-Inductive sem_internal_sstate ctx rs m t s: sstate -> Prop :=
-  | sem_Sfinal sis sfv
+(* transition (t,s) produced by a sstate in initial context ctx *)
+Inductive sem_sstate ctx t s: sstate -> Prop :=
+  | sem_Sfinal sis sfv rs m
      (SIS: sem_sistate ctx sis rs m)
      (SFV: sem_sfval ctx sfv rs m t s)
-     : sem_internal_sstate ctx rs m t s (Sfinal sis sfv)
+     : sem_sstate ctx t s (Sfinal sis sfv)
   | sem_Scond b cond args sm ifso ifnot
      (SEVAL: seval_condition ctx cond args sm = Some b)
-     (SELECT: sem_internal_sstate ctx rs m t s (if b then ifso else ifnot))
-     : sem_internal_sstate ctx rs m t s (Scond cond args sm ifso ifnot)
+     (SELECT: sem_sstate ctx t s (if b then ifso else ifnot))
+     : sem_sstate ctx t s (Scond cond args sm ifso ifnot)
+  (* NB: Sdead: fails to produce a transition *) 
   .
+
+(** * Idée de l'execution symbolique en Continuation Passing Style 
+
+[k] ci-dessous est la continuation (c-a-d. la suite de la construction de l'arbre qu'on va appliquer dans chaque branche)
+
+Rem: si manipuler une telle continuation s'avère compliqué dans les preuves,
+il faudra faire autrement dans le modèle -- par exemple avec une structure de donnée 
+pour représenter l'ensemble des chemins.
+(même si on peut conserver le CPS dans l'implem finale, pour l'efficacité).
+
+*)
+
+Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := 
+  match ib with
+  | BF fin => Sfinal sis (sexec_final_sfv fin sis)
+  (* basic instructions *)
+  | Bnop => k sis
+  | Bop op args res => k (sexec_op op args res sis)
+  | Bload TRAP chunk addr args dst => k (sexec_load TRAP chunk addr args dst sis)
+  | Bload NOTRAP chunk addr args dst => Sdead (* TODO *)
+  | Bstore chunk addr args src => k (sexec_store chunk addr args src sis)
+ (* composed instructions *)
+  | Bseq ib1 ib2 =>
+      sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) 
+  | Bcond cond args ifso ifnot _ =>
+      let args := list_sval_inj (List.map sis.(si_sreg) args) in
+      let ifso := sexec_rec ifso sis k in
+      let ifnot := sexec_rec ifnot sis k in
+      Scond cond args sis.(si_smem) ifso ifnot
+  end
+  .
+
+Definition sexec ib := sexec_rec ib sis_init (fun _ => Sdead).
+
+Local Hint Constructors sem_sstate: core.
+Local Hint Resolve sexec_final_svf_correct sis_init_correct: core.
+
+Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
+  (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): 
+  forall k 
+  (CONT: forall sis, ofin = None -> sem_sistate ctx sis rs1 m1 -> sem_sstate ctx t s (k sis))
+  sis 
+  (SIS: sem_sistate ctx sis rs m)
+  , match ofin with
+    | Some fin =>
+        final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s -> 
+        sem_sstate ctx t s (sexec_rec ib sis k)
+    | None => sem_sstate ctx t s (sexec_rec ib sis k)
+    end.
+Proof.
+  induction ISTEP; simpl; eauto.
+  - (* op *)
+    intros; eapply CONT; eauto.
+    eapply sexec_op_correct; eauto.
+  - (* load *)
+    intros; eapply CONT; eauto.
+    eapply sexec_load_TRAP_correct; eauto.
+  - (* store *)
+    intros; eapply CONT; eauto.
+    eapply sexec_store_correct; eauto.
+  - (* seq_stop *)
+    intros; eapply IHISTEP; eauto.
+    try congruence.
+  - (* seq_continue *)
+    intros. destruct ofin as [fin|].
+    + (* Some *)
+      clear CONT.
+      intros; eapply IHISTEP1; eauto.
+      intros; eapply IHISTEP2; eauto.
+      try congruence.
+    + (* None *)
+      intros; eapply IHISTEP1; eauto.
+  - (* cond *)
+    intros.
+    assert (IFEQ: (if b then sexec_rec ifso sis k else sexec_rec ifnot sis k) = sexec_rec (if b then ifso else ifnot) sis k).
+    { destruct b; simpl; auto. }
+    destruct ofin as [fin|].
+    + (* Some *)
+      clear CONT.
+      intro FSTEP; eapply sem_Scond; eauto.
+      * erewrite seval_condition_eq; eauto.
+      * rewrite IFEQ. 
+        eapply IHISTEP; eauto.
+        try congruence.
+    + (* None *)
+      eapply sem_Scond; eauto.
+      * erewrite seval_condition_eq; eauto.
+      * rewrite IFEQ. 
+        eapply IHISTEP; eauto.
+Qed.
+
+(* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) 
+  (sexec is a correct over-approximation)
+*)
+Theorem sexec_correct ctx ib t s: 
+  iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
+  sem_sstate ctx t s (sexec ib).
+Proof.
+  destruct 1 as (rs' & m' & fin & ISTEP & FSTEP).
+  unfold sexec.
+  exploit sexec_rec_correct; simpl; eauto || congruence.
+Qed.