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

4 files changed, 372 insertions, 13 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index c8dfa0af..d7ffa118 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -175,6 +175,23 @@ Definition find_function (ros: reg + ident) (rs: regset) : option fundef :=
 
 Local Open Scope option_monad_scope.
 
+(* (* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *)
+
+Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop :=
+  | has_loaded_normal a trap
+      (EVAL: eval_addressing ge sp addr rs##args = Some a)
+      (LOAD: Mem.loadv chunk m a = Some v)
+      : has_loaded sp rs m chunk addr args v trap
+  | has_loaded_default
+      (LOAD: forall a, eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = None)
+      (DEFAULT: v = default_notrap_load_value chunk)
+      : has_loaded sp rs m chunk addr args v NOTRAP 
+  .
+
+(* TODO: move this scheme in "Memory" module if this scheme is useful ! *)
+
+*)
+
 (** internal big-step execution of one iblock *)
 Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop :=
   | exec_final rs m fin: iblock_istep sp rs m (BF fin) rs m (Some fin)
@@ -186,6 +203,11 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi
      (EVAL: eval_addressing ge sp addr rs##args = Some a)
      (LOAD: Mem.loadv chunk m a = Some v)
      : iblock_istep sp rs m (Bload TRAP chunk addr args dst) (rs#dst <- v) m None
+(* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above
+  | exec_load rs m trap chunk addr args dst v
+      (LOAD: has_loaded sp rs m chunk addr args v trap)
+     : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None
+*)
   | exec_store rs m chunk addr args src a m' 
      (EVAL: eval_addressing ge sp addr rs##args = Some a)
      (STORE: Mem.storev chunk m a rs#src = Some m')
@@ -764,11 +786,6 @@ Definition verify_function dupmap f f' : res unit :=
   do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f');
   verify_cfg dupmap (fn_code f) (RTL.fn_code f').
 
-Definition is_seq (ib: iblock): bool :=
- match ib with
- | Bseq _ _ => true 
- | _ => false
- end.
 
 Definition is_atom (ib: iblock): bool :=
  match ib with
@@ -776,6 +793,67 @@ Definition is_atom (ib: iblock): bool :=
  | _ => true
  end.
 
+Inductive is_expand: iblock -> Prop :=
+  | exp_Bseq ib1 ib2:
+     is_atom ib1 = true ->
+     is_expand ib2 -> 
+     is_expand (Bseq ib1 ib2)
+  | exp_Bcond cond args ib1 ib2 i:
+     is_expand ib1 ->
+     is_expand ib2 -> 
+     is_expand (Bcond cond args ib1 ib2 i)
+  | exp_others ib:
+     is_atom ib = true ->
+     is_expand ib
+     .
+Local Hint Constructors is_expand: core.
+
+Fixpoint expand (ib: iblock) (k: option iblock): iblock :=
+  match ib with
+  | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k))
+  | Bcond cond args ib1 ib2 i => 
+     Bcond cond args (expand ib1 k) (expand ib2 k) i
+  | ib => 
+    match k with 
+    | None => ib
+    | Some rem => Bseq ib rem
+    end
+  end.
+
+Lemma expand_correct ib: forall k,
+  (match k with Some rem => is_expand rem | None => True end)
+  -> is_expand (expand ib k).
+Proof.
+  induction ib; simpl; intros; try autodestruct; auto.
+Qed.
+
+Lemma expand_None_correct ib: 
+   is_expand (expand ib None).
+Proof.
+  apply expand_correct; simpl; auto.
+Qed.
+
+Definition expand_code (cfg: code): code :=
+  (PTree.map (fun _ ib => {| entry:=expand ib.(entry) None; input_regs := ib.(input_regs) |}) cfg).
+
+Lemma expand_code_correct cfg pc ib :
+  (expand_code cfg)!pc=Some ib -> is_expand (ib.(entry)).
+Proof.
+  unfold expand_code.
+  rewrite PTree.gmap.
+  destruct (cfg!pc); simpl; intros; try_simplify_someHyps.
+  apply expand_None_correct; auto.
+Qed.
+
+
+(* TODO: eliminer toute la suite quand "right_assoc" sera remplace par "expand" *)
+
+Definition is_seq (ib: iblock): bool :=
+ match ib with
+ | Bseq _ _ => true 
+ | _ => false
+ end.
+
 
 Inductive is_right_assoc: iblock -> Prop :=
   | ira_Bseq ib1 ib2:
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 7025b90c..0a2c0a04 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 := {
+Record iblock_exec_context := Bctx {
   cge: BTL.genv;
-  csp: val;
   cstk: list stackframe;
   cf: function;
+  csp: val;
   crs0: regset;
   cm0: mem
 }.
@@ -431,6 +430,103 @@ Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
         E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m)
 .
 
+(** * Preservation properties *)
+
+Section SymbValPreserved.
+
+Variable ge ge': BTL.genv.
+
+Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.
+
+Hypothesis senv_preserved_BTL: Senv.equiv ge ge'.
+
+Lemma senv_find_symbol_preserved id:
+  Senv.find_symbol ge id = Senv.find_symbol ge' id.
+Proof.
+  destruct senv_preserved_BTL as (A & B & C). congruence.
+Qed.
+
+Lemma senv_symbol_address_preserved id ofs:
+  Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs.
+Proof.
+  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
+  reflexivity.
+Qed.
+
+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 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 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.
+  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
+    erewrite <- eval_addressing_preserved; eauto.
+    destruct (eval_addressing _ sp _ _); auto.
+    rewrite IHsv; auto.
+  + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto.
+    rewrite IHsv0; auto.
+  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
+    erewrite <- eval_addressing_preserved; eauto.
+    destruct (eval_addressing _ sp _ _); auto.
+    rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto.
+    rewrite IHsv1; auto.
+Qed.
+
+Lemma seval_builtin_arg_preserved m: forall 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).
+  - rewrite <- eval_sval_preserved. assumption.
+  - rewrite <- senv_symbol_address_preserved. assumption.
+  - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal.
+Qed.
+
+Lemma seval_builtin_args_preserved 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 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.
+  rewrite IHlsv; auto.
+Qed.
+
+Lemma smem_eval_preserved 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.
+  erewrite <- eval_addressing_preserved; eauto.
+  destruct (eval_addressing _ sp _ _); auto.
+  rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto.
+  rewrite eval_sval_preserved; auto.
+Qed.
+
+Lemma seval_condition_preserved 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.
+  rewrite smem_eval_preserved; auto.
+Qed.
+
+End SymbValPreserved.
 
 
 (* Syntax and Semantics of symbolic internal states *)
@@ -521,19 +617,199 @@ 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)
+  | Sabort
  .
 
-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: Sabort: 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 => Sabort (* 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 _ => Sabort).
+
+Local Hint Constructors sem_sstate: core.
+Local Hint Resolve sexec_op_correct sexec_final_svf_correct 
+                   sexec_load_TRAP_correct sexec_store_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 sis k
+  (SIS: sem_sistate ctx sis rs m)
+  (CONT: match ofin with
+         | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx t s (k sis')
+         | Some fin => final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
+         end),
+  sem_sstate ctx t s (sexec_rec ib sis k).
+Proof.
+  induction ISTEP; simpl; try autodestruct; eauto.
+  (* condition *)
+  all: intros;
+    eapply sem_Scond; eauto; [
+      erewrite seval_condition_eq; eauto |
+      replace (if b then sexec_rec ifso sis k else sexec_rec ifnot sis k) with (sexec_rec (if b then ifso else ifnot) sis k); 
+      try autodestruct; 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).
+  eapply sexec_rec_correct; simpl; eauto.
+Qed.
diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v
index 14aecb21..2b2bd15c 100644
--- a/scheduling/RTLtoBTL.v
+++ b/scheduling/RTLtoBTL.v
@@ -12,6 +12,9 @@ Local Open Scope error_monad_scope.
 Definition transf_function (f: RTL.function) : res BTL.function :=
   let (tcte, dupmap) := rtl2btl f in
   let (tc, te) := tcte in
+  (* TODO, pour finir la preuve: remplacer ci-dessous "right_assoc_code" par "expand_code" 
+     on s'arrangera pour éliminer cette transformation "coûteuse" à la fin !
+  *)
   let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) (right_assoc_code tc) te in
   do u <- verify_function dupmap f' f;
   OK f'.
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 1db088d2..efc22eb6 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -6,6 +6,8 @@ Require Import Errors Linking RTLtoBTL.
 
 Require Import Linking.
 
+(* TODO: remplacer "right_assoc" par "expand" ci-dessous *)
+
 Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
   dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
   dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);