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

3 files changed, 351 insertions, 27 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 6d74ccf9..fdefe205 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -9,8 +9,6 @@
     - Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement !
 
     TODO: A REVOIR COMPLETEMENT.
-    - essayer de découper chaque relation de raffinement en une fonction "projection/abstraction" (à la "hsval_proj" à renommer en "hsval_abstract") 
-      et une équivalence sur la représentation abstraite.
     - introduire "fake" hash-consed values (à renommer en "refined" plutôt que "fake").
 
 *)
@@ -48,7 +46,7 @@ Record ristate :=
         1) we store a list of sval evaluations
         2) we encode the symbolic regset by a PTree + a boolean indicating the default sval *)
     ris_input_init: bool;
-    ris_ok_sval: list sval;
+    ok_rsval: list sval;
     ris_sreg:> PTree.t sval
   }.
 
@@ -61,7 +59,7 @@ Coercion ris_sreg_get: ristate >-> Funclass.
 
 Record ris_ok ctx (ris: ristate) : Prop := {
    OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None;
-   OK_RREG: forall sv, List.In sv (ris_ok_sval ris) -> eval_sval ctx sv <> None
+   OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None
 }.
 Local Hint Resolve OK_RMEM OK_RREG: core.
 Local Hint Constructors ris_ok: core.
@@ -77,7 +75,7 @@ Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ VALID_PRESERV: core.
 Local Hint Constructors ris_refines: core.
 
 Record ris_simu ris1 ris2: Prop := {
-  SIMU_FAILS: forall sv, List.In sv ris2.(ris_ok_sval) -> List.In sv ris1.(ris_ok_sval);
+  SIMU_FAILS: forall sv, List.In sv ris2.(ok_rsval) -> List.In sv ris1.(ok_rsval);
   SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem);
   SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r
 }.
@@ -307,7 +305,7 @@ Proof.
   destruct i; simpl; unfold sum_left_map; try autodestruct; eauto.
 Qed.
 
-Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ris_ok_sval := nil; ris_sreg := PTree.empty _ |}.
+Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.
 
 Lemma ris_init_correct ctx:
   ris_refines ctx ris_init sis_init.
@@ -323,11 +321,11 @@ Qed.
 Definition rset_smem rm (ris:ristate): ristate :=
   {| ris_smem := rm;
      ris_input_init := ris.(ris_input_init);
-     ris_ok_sval := ris.(ris_ok_sval);
+     ok_rsval := ris.(ok_rsval);
      ris_sreg:= ris.(ris_sreg)
   |}.
 
-Lemma sis_ok_set_mem ctx sm sis:
+Lemma ok_set_mem ctx sm sis:
   sis_ok ctx (set_smem sm sis)
   <-> (sis_ok ctx sis /\ eval_smem ctx sm <> None).
 Proof.
@@ -335,7 +333,7 @@ Proof.
   intuition eauto.
 Qed.
 
-Lemma ris_ok_set_mem ctx rm (ris: ristate):
+Lemma ok_rset_mem ctx rm (ris: ristate):
   (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) ->
   ris_ok ctx (rset_smem rm ris)
   <-> (ris_ok ctx ris /\ eval_smem ctx rm <> None).
@@ -343,7 +341,7 @@ Proof.
    split; destruct 1; econstructor; simpl in *; eauto.
 Qed.
 
-Lemma rset_mem_refpreserv ctx rm sm ris sis:
+Lemma rset_mem_correct ctx rm sm ris sis:
   (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) ->
   (forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs) ->
   ris_refines ctx ris sis ->
@@ -352,23 +350,308 @@ Lemma rset_mem_refpreserv ctx rm sm ris sis:
 Proof.
   destruct 3; intros.
   econstructor; eauto.
-  + rewrite sis_ok_set_mem, ris_ok_set_mem; intuition congruence.
-  + rewrite ris_ok_set_mem; intuition eauto.
-  + rewrite ris_ok_set_mem; intuition eauto.
+  + rewrite ok_set_mem, ok_rset_mem; intuition congruence.
+  + rewrite ok_rset_mem; intuition eauto.
+  + rewrite ok_rset_mem; intuition eauto.
 Qed.
 
-(** TODO: could be useful ?
-Lemma seval_condition_valid_preserv ctx cond args sm b
+Definition rexec_store chunk addr args src ris: ristate :=
+   let args := list_sval_inj (List.map (ris_sreg_get ris) args) in
+   let src := ris_sreg_get ris src in
+   let rm := Sstore ris.(ris_smem) chunk addr args src in
+   rset_smem rm ris.
+
+Lemma rexec_store_correct ctx chunk addr args src ris sis:
+  ris_refines ctx ris sis ->
+  ris_refines ctx (rexec_store chunk addr args src ris) (sexec_store chunk addr args src sis).
+Proof.
+  intros REF; eapply rset_mem_correct; simpl; eauto.
+  + intros X; rewrite X. repeat autodestruct; eauto.
+  + intros m b ofs; repeat autodestruct.
+    intros; erewrite <- Mem.storev_preserv_valid; [| eauto].
+    eauto.
+  + intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ, REG_EQ; eauto.
+Qed.
+
+(* TODO: reintroduire le "root_apply" ? *)
+
+Definition rset_sreg r rsv (ris:ristate): ristate :=
+  {| ris_smem := ris.(ris_smem);
+     ris_input_init := ris.(ris_input_init);
+     ok_rsval := rsv::ris.(ok_rsval); (* TODO: A CHANGER ? *)
+     ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *)
+  |}.
+
+Lemma ok_set_sreg ctx r sv sis:
+  sis_ok ctx (set_sreg r sv sis)
+  <-> (sis_ok ctx sis /\ eval_sval ctx sv <> None).
+Proof.
+  unfold set_sreg; split.
+  + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split.
+    - econstructor; eauto.
+      intros r0; generalize (SREG r0); destruct (Pos.eq_dec r r0); try congruence.
+    - generalize (SREG r); destruct (Pos.eq_dec r r); try congruence.
+  + intros ([PRE SMEM SREG] & SVAL).
+    econstructor; simpl; eauto.
+    intros r0;  destruct (Pos.eq_dec r r0); try congruence.
+Qed.
+
+Lemma ok_rset_sreg ctx r rsv ris:
+  ris_ok ctx (rset_sreg r rsv ris)
+  <-> (ris_ok ctx ris /\ eval_sval ctx rsv <> None).
+Proof.
+   split; destruct 1; econstructor; simpl in *; eauto.
+   intuition subst; eauto.
+   exploit OK_RREG; eauto.
+Qed.
+
+Lemma rset_reg_correct ctx r rsv sv ris sis:
+  ris_refines ctx ris sis ->
+  (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) ->
+  ris_refines ctx (rset_sreg r rsv ris) (set_sreg r sv sis).
+Proof.
+  destruct 1; intros.
+  econstructor; eauto.
+  + rewrite ok_set_sreg, ok_rset_sreg; intuition congruence.
+  + rewrite ok_rset_sreg; intuition eauto.
+  + rewrite ok_rset_sreg. intros; unfold rset_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto.
+    destruct (Pos.eq_dec _ _).
+    * subst; rewrite PTree.gss; eauto.
+    * rewrite PTree.gso; eauto.
+Qed.
+
+Definition rexec_op op args dst (ris:ristate): ristate :=
+   let args := list_sval_inj (List.map ris args) in
+   rset_sreg dst (Sop op args Sinit) ris.
+
+Lemma rexec_op_correct ctx op args dst ris sis:
+  ris_refines ctx ris sis ->
+  ris_refines ctx (rexec_op op args dst ris) (sexec_op op args dst sis).
+Proof.
+  intros REF; eapply rset_reg_correct; simpl; eauto.
+  intros OK; erewrite eval_list_sval_refpreserv; eauto.
+  do 2 autodestruct; auto.
+  + intros. erewrite <- op_valid_pointer_eq; eauto.
+  + erewrite <- MEM_EQ; eauto.
+    intros; exploit OK_RMEM; eauto. destruct 1.
+Qed.
+
+Definition rexec_load trap chunk addr args dst (ris:ristate): ristate :=
+   let args := list_sval_inj (List.map ris args) in
+   rset_sreg dst (Sload ris.(ris_smem) trap chunk addr args) ris.
+
+Lemma rexec_load_correct ctx trap chunk addr args dst ris sis:
+  ris_refines ctx ris sis ->
+  ris_refines ctx (rexec_load trap chunk addr args dst ris) (sexec_load trap chunk addr args dst sis).
+Proof.
+  intros REF; eapply rset_reg_correct; simpl; eauto.
+  intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ; eauto.
+Qed.
+
+Lemma seval_condition_valid_preserv ctx cond args sm
+  (OK: eval_smem ctx sm <> None)
   (VALID_PRESERV: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs)
-  :seval_condition ctx cond args sm = Some b ->
-   seval_condition ctx cond args Sinit = Some b.
+  :seval_condition ctx cond args sm = seval_condition ctx cond args Sinit.
 Proof.
   unfold seval_condition; autodestruct; simpl; try congruence.
   intros EVAL_LIST.
   autodestruct; try congruence.
-  intros MEM COND. rewrite <- COND.
+  intros.
   eapply cond_valid_pointer_eq; intros.
   exploit VALID_PRESERV; eauto.
 Qed.
-*)
+
+Lemma seval_condition_refpreserv ctx cond args ris sis:
+  ris_refines ctx ris sis ->
+  ris_ok ctx ris ->
+  seval_condition ctx cond (list_sval_inj (map ris args)) Sinit =
+  seval_condition ctx cond (list_sval_inj (map sis args)) Sinit.
+Proof.
+  intros; unfold seval_condition.
+  erewrite eval_list_sval_refpreserv; eauto.
+Qed.
+
+
+(* transfer *)
+
+Definition rseto_sreg r rsv (ris:ristate): ristate :=
+  {| ris_smem := ris.(ris_smem);
+     ris_input_init := ris.(ris_input_init);
+     ok_rsval := ris.(ok_rsval);
+     ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *)
+  |}.
+
+Lemma ok_rseto_sreg ctx r rsv ris:
+  ris_ok ctx (rseto_sreg r rsv ris)
+  <-> (ris_ok ctx ris).
+Proof.
+   split; destruct 1; econstructor; simpl in *; eauto.
+Qed.
+
+Lemma rseto_reg_correct ctx r rsv sv ris sis:
+  ris_refines ctx ris sis ->
+  (ris_ok ctx ris -> eval_sval ctx rsv <> None) ->
+  (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) ->
+  ris_refines ctx (rseto_sreg r rsv ris) (set_sreg r sv sis).
+Proof.
+  destruct 1; intros.
+  econstructor; eauto.
+  + rewrite ok_set_sreg, ok_rseto_sreg; intuition congruence.
+  + rewrite ok_rseto_sreg; intuition eauto.
+  + rewrite ok_rseto_sreg. intros; unfold rseto_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto.
+    destruct (Pos.eq_dec _ _).
+    * subst; rewrite PTree.gss; eauto.
+    * rewrite PTree.gso; eauto.
+Qed.
+
+Fixpoint transfer_ris (inputs: list reg) (ris:ristate): ristate :=
+  match inputs with
+  | nil =>   {| ris_smem := ris.(ris_smem);
+                ris_input_init := false;
+                ok_rsval := ris.(ok_rsval);
+                ris_sreg:= PTree.empty _
+             |}
+  | r::l => rseto_sreg r (ris_sreg_get ris r) (transfer_ris l ris)
+  end.
+
+Definition transfer_sis (inputs: list reg) (sis:sistate): sistate :=
+   {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None);
+      si_sreg := transfer_sreg inputs sis;
+      si_smem := sis.(si_smem) |}.
+
+Lemma ok_transfer_sis ctx inputs sis:
+  sis_ok ctx (transfer_sis inputs sis)
+  <-> (sis_ok ctx sis).
+Proof.
+  unfold transfer_sis. induction inputs as [|r l]; simpl.
+  + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence.
+  + split.
+    * destruct 1; econstructor; simpl in *; intuition eauto.
+    * intros X; generalize X. rewrite <- IHl in X; clear IHl.
+      intros [PRE SMEM SREG].
+      econstructor; simpl; eauto.
+      intros r0;  destruct (Pos.eq_dec r r0); try congruence.
+      intros H; eapply OK_SREG; eauto.
+Qed.
+
+Lemma ok_transfer_ris ctx inputs ris:
+  ris_ok ctx (transfer_ris inputs ris)
+  <-> (ris_ok ctx ris).
+Proof.
+  induction inputs as [|r l]; simpl.
+  + split; destruct 1; econstructor; simpl in *; intuition eauto.
+  + rewrite ok_rseto_sreg. auto.
+Qed.
+
+Lemma transfer_ris_correct ctx inputs ris sis:
+  ris_refines ctx ris sis ->
+  ris_refines ctx (transfer_ris inputs ris) (transfer_sis inputs sis).
+Proof.
+  destruct 1; intros.
+  induction inputs as [|r l].
+  + econstructor; eauto.
+    * erewrite ok_transfer_sis, ok_transfer_ris; eauto.
+    * erewrite ok_transfer_ris; eauto.
+    * erewrite ok_transfer_ris; simpl; unfold ris_sreg_get; simpl; eauto.
+      intros; rewrite PTree.gempty. simpl; auto.
+  + econstructor; eauto.
+    * erewrite ok_transfer_sis, ok_transfer_ris; eauto.
+    * erewrite ok_transfer_ris; simpl.
+      intros; erewrite MEM_EQ. 2: eauto.
+      - unfold transfer_sis; simpl; eauto.
+      - rewrite ok_transfer_ris; simpl; eauto.
+    * erewrite ok_transfer_ris; simpl.
+      intros H r0.
+      erewrite REG_EQ. 2: eapply rseto_reg_correct; eauto.
+      - unfold set_sreg; simpl; auto.
+        destruct (Pos.eq_dec _ _); simpl; auto.
+      - intros. rewrite REG_EQ0; auto. apply OK_SREG; tauto.
+      - rewrite ok_rseto_sreg, ok_transfer_ris. auto.
+Qed.
+
+Definition alt_tr_sis := poly_tr (fun f tbl or => transfer_sis (Regset.elements (pre_inputs f tbl or))).
+
+Lemma tr_sis_alt_def f fi sis:
+  alt_tr_sis f fi sis = tr_sis f fi sis.
+Proof.
+  unfold tr_sis, str_inputs. destruct fi; simpl; auto.
+Qed.
+
+Definition tr_ris := poly_tr (fun f tbl or => transfer_ris (Regset.elements (pre_inputs f tbl or))).
+
+Local Hint Resolve transfer_ris_correct ok_transfer_ris: core.
+Local Opaque transfer_ris.
+
+Lemma ok_tr_ris ctx f fi ris:
+  ris_ok ctx (tr_ris f fi ris)
+  <-> (ris_ok ctx ris).
+Proof.
+   destruct fi; simpl; eauto.
+Qed.
+
+Lemma ok_tr_ris_imp ctx f fi ris:
+  ris_ok ctx (tr_ris f fi ris)
+  -> (ris_ok ctx ris).
+Proof.
+  rewrite ok_tr_ris; auto.
+Qed.
+
+
+Lemma tr_ris_correct ctx f fi ris sis:
+  ris_refines ctx ris sis ->
+  ris_refines ctx (tr_ris f fi ris) (tr_sis f fi sis).
+Proof.
+  intros REF. rewrite <- tr_sis_alt_def.
+  destruct fi; simpl; eauto.
+Qed.
+
+Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := 
+  match ib with
+  | BF fin _ => Rfinal (tr_ris f fin ris) (sexec_final_sfv fin ris)
+  (* basic instructions *)
+  | Bnop _ => k ris
+  | Bop op args res _ => k (rexec_op op args res ris)
+  | Bload TRAP chunk addr args dst _ => k (rexec_load TRAP chunk addr args dst ris)
+  | Bload NOTRAP chunk addr args dst _ => Rabort
+  | Bstore chunk addr args src _ => k (rexec_store chunk addr args src ris)
+ (* composed instructions *)
+  | Bseq ib1 ib2 =>
+      rexec_rec f ib1 ris (fun ris2 => rexec_rec f ib2 ris2 k)
+  | Bcond cond args ifso ifnot _ =>
+      let args := list_sval_inj (List.map ris args) in
+      let ifso := rexec_rec f ifso ris k in
+      let ifnot := rexec_rec f ifnot ris k in
+      Rcond cond args ifso ifnot
+  end
+  .
+
+Local Hint Constructors rst_refines: core.
+Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ok_tr_ris_imp 
+  rexec_op_correct rexec_load_correct rexec_store_correct: core.
+
+Lemma rexec_rec_correct ctx f ib: 
+  forall ris sis rk k
+  (CONT: forall rs ss, ris_refines ctx rs ss -> rst_refines ctx (rk rs) (k ss))
+  (REF: ris_refines ctx ris sis)
+  (*OK: ris_ok ctx ris*)
+  , rst_refines ctx (rexec_rec f ib ris rk) (sexec_rec f ib sis k).
+Proof.
+  induction ib; simpl; eauto.
+  - (* load *) autodestruct; eauto.
+  - intros.
+    econstructor; eauto.
+    symmetry.
+    erewrite seval_condition_valid_preserv; eauto.
+Admitted.
+
+Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort).
+
+Lemma rexec_correct ctx f ib:
+  rst_refines ctx (rexec f ib) (sexec f ib).
+Proof.
+  eapply rexec_rec_correct; eauto.
+  (* econstructor; simpl; auto. congruence. *)
+Qed.
+
+
 
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 4b4571e4..464bb0f0 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -630,7 +630,7 @@ Qed.
 Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval :=
   match inputs with
   | nil => fun r => Sundef 
-  | r1::l => fun r => if Pos.eq_dec r r1 then sreg r1 else transfer_sreg l sreg r
+  | r1::l => fun r => if Pos.eq_dec r1 r then sreg r1 else transfer_sreg l sreg r
   end.
 
 Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (pre_inputs f tbl or)).
@@ -655,15 +655,12 @@ Definition tr_sis f (fi: final) (sis: sistate) :=
      si_sreg := poly_tr str_inputs f fi sis.(si_sreg); 
      si_smem := sis.(si_smem) |}.
 
-Definition sreg_eval ctx (sis: sistate) (r: reg): option val :=
-  eval_sval ctx (sis.(si_sreg) r).
-
 Lemma tr_sis_regs_correct_aux ctx fin sis rs m:
   sem_sistate ctx sis rs m ->
-  (forall r, sreg_eval ctx (tr_sis (cf ctx) fin sis) r = Some (tr_regs (cf ctx) fin rs) # r).
+  (forall r, eval_sval ctx (tr_sis (cf ctx) fin sis r) = Some (tr_regs (cf ctx) fin rs) # r).
 Proof.
   Local Opaque str_inputs.
-  unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG).
+  simpl. destruct 1 as (_ & _ & REG).
   destruct fin; simpl; eauto.
 Qed.
 
@@ -842,7 +839,7 @@ Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2:
 Proof.
   intros H1 H2.
   lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto.
-  unfold sreg_eval; intros X.
+  intros X.
   destruct H1 as (_&MEM1&REG1).
   destruct H2 as (_&MEM2&REG2); simpl in *.
   intuition try congruence.
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index 954143c1..9dd21be9 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -346,13 +346,57 @@ Au final, on obtient deux BDD identiques sur cet exemple (sans explosion combina
 
 Extends the symbolic simulation test to support invariants at block entry, including global renaming of registers. Case-study: support of strength-reduction.
 
-**IDEAS**
+**PRELIMINARY IDEAS**
 
 - En pratique, il faudrait affiner la sémantique symbolique des "jumptable" pour que ça marche bien: avec un "état symbolique interne" par sortie (au lieu d'un état symbolique interne global dans la sémantique actuelle). Ça semble nécessaire pour gérer les invariants de renommage par exemple: en effet, il y a potentiellement un renommage différent pour chaque sortie.
 Une solution possible: calquer Bjumptable sur Bcond (c-a-d autoriser les Bjumptable en milieu de blocs). On pourrait étendre la prédiction de branchement par profiling aux jumptables (par exemple, avoir des superblocks avec des jumptables au milieu). Un autre intérêt: simplifier (un peu) le support pour des formes SSA partielles (cf. ci-dessous). Ceci dit, ça compliquerait les choses à plein d'endroits (type Coq [iblock] mutuellement inductif avec [list_iblock] pour avoir les bons principes d'inductions, etc) pour des gains minimes en pratiques ?
 
 - Est-ce qu'il ne faut pas envisager une combinaison "execution symbolique + value analysis" ? La value analysis pourrait se faire directement sur la sémantique symbolique (donc en sortie de l'exécution symbolique), avec un mécanisme de mémoïsation (pour éviter les calculs redondants dus à la duplication de termes dans l'état symbolique). Intérêts: la value analysis ne se ferait que sur les registres live. Elle serait aussi plus sans doute un peu simple (par exemple inutile d'avoir un "join": on peut se contenter d'un test d'inclusion sur chacun des chemins).
 
+**EXAMPLE OF STRENGTH REDUCTION**
+
+On veut passer du code C1:
+
+    init: // inputs: int *t,  int n, int s 
+    int i=0;
+    loop: // inputs: int *t,  int n, int s, int i 
+        if (i >= n) goto exit;
+        s += t[i];
+        i += 1;
+        goto loop;
+    exit: // inputs: int *t,  int s
+    
+au code C2:
+
+    init: // inputs: int *t,  int n, int s 
+    int *ti = t;
+    int *tn = t+n;
+    loop: // inputs: int *t,  int s, int *ti, int *tn
+        if (ti >= tn) goto exit;
+        s += *ti;
+        ti += 4;
+        goto loop;
+    exit; // inputs: int *t,  int s
+        
+Pour donner la correspondance entre les variables des 2 blocs, pour chaque entrée "pc", on introduit une "fonction" de C1@pc.(inputs) -> C2@pc.(inputs).
+
+Typiquement, cette fonction est codable comme un map associant une valeur symbolique sur les C1@pc.(inputs) aux variables de C2@pc.(inputs). Exemple:
+
+    init: // map vide (identité)
+    loop:
+        ti = t+i
+        tn = t+n
+    exit: // map vide (identité)
+ 
+Si on note `TRANSFER` cette fonction, alors la vérification par
+exécution symbolique que le bloc `ib1` est simulé par `ib2` modulo
+`TRANSFER` sur l'entrée `pc` se ramène à montrer `ib1[TRANSFER]` avec
+`TRANSFER(pc); ib2` pour la simulation symbolique usuelle.
+ 
+Ci-dessus `ib1[TRANSFER]` dit qu'on a appliqué `TRANSFER(pc')` sur chacune des sorties `pc'` de `ib1`.
+
+**REM** pour que ce soit correct, il faut sans doute vérifier une condition du style `ok(ib1) => ok(ib1[TRANSFER])`...
+
 ## Support of SSA-optimizations
 
 Minimum feature: extends BTL with "register renamings" at exits. This should enable to represent SSA-forms in BTL IR, more or less like in MLIR.