Merge branch 'BTL_fsem' into BTL

1 files changed, 483 insertions, 8 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index caa48920..2be4fcac 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -17,6 +17,9 @@
 Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import RTL Op Registers OptionMonad.
+Require Import Lia.
+
+Import ListNotations.
 
 (** * Abstract syntax *)
 
@@ -91,7 +94,7 @@ Coercion BF: final >-> Funclass.
 
 Record iblock_info := { 
   entry: iblock;
-  input_regs: Regset.t; (* extra liveness information ignored by BTL semantics *)
+  input_regs: Regset.t (* extra liveness information for BTL functional semantics *)
   binfo: block_info (* Ghost field used in oracles *)
 }.
 
@@ -168,8 +171,26 @@ Record outcome := out {
    _fin: option final 
 }.
 
+(* follows RTL semantics to set the result of builtin *)
+Definition reg_builtin_res (res: builtin_res reg): option reg :=
+  match res with
+  | BR r => Some r
+  | _ => None
+  end.
+
 Section RELSEM.
 
+(** [step] (and in particular [final_step]) is parametrized by function [tr_exit] to transfer registers on each iblock exit.
+
+    In particular, [tr_exit f lpc or rs] computes from [rs] the [rs'] on which the execution from iblock [pc] in [lpc] in [f] may start.
+
+    Here, [or] is an optional register that will be assigned after exiting the iblock, but before entering in [pc]: e.g. the register set by a function call
+    before entering in return address.
+
+*)
+
+Variable tr_exit: function -> list exit -> option reg -> regset -> regset.
+
 Variable ge: genv.
 
 Definition find_function (ros: reg + ident) (rs: regset) : option fundef :=
@@ -280,10 +301,12 @@ Proof.
     destruct o; try_simplify_someHyps; subst; eauto.
 Qed.
 
+Local Open Scope list_scope.
+
 Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
   | exec_Bgoto pc:
       final_step stack f sp rs m (Bgoto pc) E0
-                 (State stack f sp pc rs m)
+                 (State stack f sp pc (tr_exit f [pc] None rs) m)
   | exec_Breturn or stk m':
       sp = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
@@ -293,7 +316,7 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       final_step stack f sp rs m (Bcall sig ros args res pc')
-        E0 (Callstate (Stackframe res f sp pc' rs :: stack) fd rs##args m)
+        E0 (Callstate (Stackframe res f sp pc' (tr_exit f [pc'] (Some res) rs) :: stack) fd rs##args m)
   | exec_Btailcall sig ros args stk m' fd:
       find_function ros rs = Some fd ->
       funsig fd = sig ->
@@ -305,12 +328,12 @@ Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
       external_call ef ge vargs m t vres m' ->
       final_step stack f sp rs m (Bbuiltin ef args res pc')
-         t (State stack f sp pc' (regmap_setres res vres rs) m')
+         t (State stack f sp pc' (regmap_setres res vres (tr_exit f [pc'] (reg_builtin_res res) rs)) m')
   | exec_Bjumptable arg tbl n pc':
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
       final_step stack f sp rs m (Bjumptable arg tbl)
-        E0 (State stack f sp pc' rs m)
+        E0 (State stack f sp pc' (tr_exit f tbl None rs) m)
 .
 
 (** big-step execution of one iblock *)
@@ -367,11 +390,463 @@ Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall r m,
       final_state (Returnstate nil (Vint r) m) r.
 
-(** The small-step semantics for a program. *)
+(** The "raw" CFG small-step semantics for a BTL program (e.g. close to RTL semantics) *)
+
+(* tid = transfer_identity *)
+Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs.
+
+Definition cfgsem (p: program) :=
+  Semantics (step tid) (initial_state p) final_state (Genv.globalenv p).
+
+(** The full "functional" small-step semantics for a BTL program.
+    at each exit, we only transfer register in "input_regs" (i.e. "alive" registers).
+*)
+Definition transfer_regs (inputs: list reg) (rs: regset): regset :=
+  init_regs (rs##inputs) inputs.
+
+Lemma transfer_regs_inputs inputs rs r:
+  List.In r inputs -> (transfer_regs inputs rs)#r = rs#r.
+Proof.
+  unfold transfer_regs; induction inputs; simpl; intuition subst.
+  - rewrite Regmap.gss; auto.
+  - destruct (Pos.eq_dec a r).
+    + subst; rewrite Regmap.gss; auto.
+    + rewrite Regmap.gso; auto.
+Qed.
+
+Lemma transfer_regs_dead inputs rs r:
+  ~List.In r inputs -> (transfer_regs inputs rs)#r = Vundef.
+Proof.
+  unfold transfer_regs; induction inputs; simpl; intuition subst.
+  - rewrite Regmap.gi; auto.
+  - rewrite Regmap.gso; auto.
+Qed.
+
+Fixpoint union_inputs (f:function) (tbl: list exit): Regset.t :=
+  match tbl with
+  | nil => Regset.empty
+  | pc::l => let rs:= union_inputs f l in
+             match f.(fn_code)!pc with
+             | None => rs
+             | Some ib => Regset.union rs ib.(input_regs)
+             end
+  end.
+
+(* TODO: lemma not yet used
+
+Lemma union_inputs_In f tbl r:
+  Regset.In r (union_inputs f tbl) -> (exists pc, List.In pc tbl /\ exists ib, f.(fn_code)!pc = Some ib /\ Regset.In r ib.(input_regs)).
+Proof.
+  induction tbl as [|pc l]; simpl; intros.
+  - exploit Regset.empty_1; eauto. intuition.
+  - destruct ((fn_code f) ! pc) eqn:ATpc.
+    + exploit Regset.union_1; eauto.
+      destruct 1 as [X1|X1].
+      * destruct IHl as (pc' & H1 & H2); eauto.
+      * eexists; intuition eauto.
+    + destruct IHl as (pc' & H1 & H2); eauto.
+Qed.
+
+Lemma union_inputs_notIn f tbl r: 
+   (forall pc ib, List.In pc tbl -> f.(fn_code)!pc = Some ib -> ~Regset.In r ib.(input_regs))
+    -> ~Regset.In r (union_inputs f tbl).
+Proof.
+  induction tbl as [|pc l]; simpl; intuition eauto.
+  - exploit Regset.empty_1; eauto.
+  - destruct ((fn_code f) ! pc) eqn:ATpc; intuition eauto.
+    exploit Regset.union_1; intuition eauto.
+Qed.
+*)
+
+(* This function computes the union of the inputs associated to the exits
+                   minus the optional register in [or] (typically the result of a call or a builtin).
+   i.e. similar to [pre_output_regs] in RTLpath.
+*)
+Definition pre_inputs (f:function) (tbl: list exit) (or: option reg): Regset.t :=
+ let rs := union_inputs f tbl in
+ match or with 
+ | Some r => Regset.remove r rs
+ | None => rs
+ end
+ .
+
+(* TODO: lemma pre_inputs_In + pre_inputs_notIn ? *)
+
+Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset 
+  := transfer_regs (Regset.elements (pre_inputs f tbl or)).
+
+
+(* TODO: move this elsewhere *)
+Lemma SetoidList_InA_eq_equiv A (l: list A): forall x,
+  SetoidList.InA (fun x y => x = y) x l <-> List.In x l.
+Proof.
+  intros x; split.
+  - induction 1; simpl; eauto.
+  - induction l; simpl; intuition.
+Qed.
+
+Lemma tr_pre_inputs f tbl or rs r:
+  Regset.In r (pre_inputs f tbl or) -> (tr_inputs f tbl or rs)#r = rs#r.
+Proof.
+  intros; eapply transfer_regs_inputs.
+  rewrite <- SetoidList_InA_eq_equiv.
+  eapply Regset.elements_1; eauto.
+Qed.
+
+Lemma tr_inputs_dead f tbl or rs r:
+  ~(Regset.In r (pre_inputs f tbl or)) -> (tr_inputs f tbl or rs)#r = Vundef.
+Proof.
+  intros X; eapply transfer_regs_dead; intuition eauto.
+  eapply X. eapply Regset.elements_2. 
+  rewrite -> SetoidList_InA_eq_equiv; eauto.
+Qed.
+
+Local Hint Resolve tr_pre_inputs Regset.mem_2 Regset.mem_1: core.
+
+Lemma tr_inputs_get f tbl or rs r:
+  (tr_inputs f tbl or rs)#r = if Regset.mem r (pre_inputs f tbl or) then rs#r else Vundef.
+Proof.
+  autodestruct; eauto.
+  intros; apply tr_inputs_dead; eauto.
+  intro X; exploit Regset.mem_1; eauto.
+  congruence.
+Qed.
+
+(* TODO: not yet used
+Lemma tr_inputs_ext f tbl or rs1 rs2:
+  (forall r, Regset.In r (pre_inputs f tbl or) -> rs1#r = rs2#r) ->
+  (forall r, (tr_inputs f tbl or rs1)#r = (tr_inputs f tbl or rs2)#r).
+Proof.
+  intros EQ r. rewrite !tr_inputs_get.
+  autodestruct; auto.
+Qed.
+*)
+
+Definition fsem (p: program) :=
+  Semantics (step tr_inputs) (initial_state p) final_state (Genv.globalenv p).
+
+Local Open Scope list_scope.
+
+Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: final): A := 
+  match i with
+  | Bgoto pc => tr f [pc] None
+  | Bcall _ _ _ res pc => tr f [pc] (Some res)
+  | Btailcall _ _ args => tr f [] None
+  | Bbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res)
+  | Breturn _ => tr f [] None
+  | Bjumptable _ tbl => tr f tbl None
+  end.
+
+Definition tr_regs: function -> final -> regset -> regset :=
+  poly_tr tr_inputs.
+
+(* TODO: NOT USEFUL ?
+Definition liveout: function -> final -> Regset.t :=
+  poly_tr pre_inputs.
+
+Lemma tr_regs_liveout_equiv f fi : tr_regs f fi = transfer_regs (Regset.elements (liveout f fi)).
+Proof.
+  destruct fi; simpl; auto.
+Qed.
+
+Local Hint Resolve tr_inputs_get: core.
+
+Lemma tr_regs_get f fi rs r: (tr_regs f fi rs)#r = if Regset.mem r (liveout f fi) then rs#r else Vundef.
+Proof.
+   Local Opaque pre_inputs.
+   destruct fi; simpl; auto.
+Qed.
+*)
+
+(* * Comparing BTL semantics modulo extensionality of [regset].
+
+NB: This is at least used in BTL_SEtheory (and probably in the future BTL_SchedulerProof).
+
+*)
+Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
+  | equiv_stackframe_intro res f sp pc (rs1 rs2: regset)
+      (EQUIV: forall r, rs1#r = rs2#r)
+      :equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  .
+
+Inductive equiv_state: state -> state -> Prop :=
+  | State_equiv stk1 stk2 f sp pc rs1 m rs2
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      (EQUIV: forall r, rs1#r = rs2#r)
+      :equiv_state (State stk1 f sp pc rs1 m) (State stk2 f sp pc rs2 m)
+  | Call_equiv stk1 stk2 f args m
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      :equiv_state (Callstate stk1 f args m) (Callstate stk2 f args m)
+  | Return_equiv stk1 stk2 v m
+      (STACKS: list_forall2 equiv_stackframe stk1 stk2)
+      :equiv_state (Returnstate stk1 v m) (Returnstate stk2 v m)
+  .
+Local Hint Constructors equiv_stackframe equiv_state: core.
+
+Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
+Proof.
+  destruct stf; eauto.
+Qed.
+
+Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk.
+Proof.
+  Local Hint Resolve equiv_stackframe_refl: core.
+  induction stk; simpl; constructor; auto.
+Qed.
+Local Hint Resolve equiv_stack_refl: core.
+
+Lemma equiv_state_refl s: equiv_state s s.
+Proof.
+  induction s; simpl; constructor; auto.
+Qed.
+
+Lemma equiv_stackframe_trans stf1 stf2 stf3:
+  equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3.
+Proof.
+  destruct 1; intros EQ; inv EQ; try econstructor; eauto.
+  intros; eapply eq_trans; eauto.
+Qed.
+Local Hint Resolve equiv_stackframe_trans: core.
+
+Lemma equiv_stack_trans stk1 stk2:
+  list_forall2 equiv_stackframe stk1 stk2 -> 
+  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
+  list_forall2 equiv_stackframe stk1 stk3.
+Proof.
+  induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
+Qed.
+
+Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3.
+Proof.
+  Local Hint Resolve equiv_stack_trans: core.
+  destruct 1; intros EQ; inv EQ; econstructor; eauto.
+  intros; eapply eq_trans; eauto.
+Qed.
+
+Lemma regmap_setres_eq (rs rs': regset) res vres:
+  (forall r, rs # r = rs' # r) ->
+  forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r.
+Proof.
+  intros RSEQ r. destruct res; simpl; try congruence.
+  destruct (peq x r).
+  - subst. repeat (rewrite Regmap.gss). reflexivity.
+  - repeat (rewrite Regmap.gso); auto.
+Qed.
+
+(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation.
+
+We start by extending the previous [equiv_*] stuff for [Val.lessdef]: we need to also compare memories 
+for Mem.extends, because Vundef values are propagated in memory through stores, allocation, etc.
+
+*)
+
+Inductive lessdef_stackframe: stackframe -> stackframe -> Prop :=
+  | lessdef_stackframe_intro res f sp pc rs1 rs2
+      (REGS: forall r, Val.lessdef rs1#r rs2#r)
+      :lessdef_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  .
+
+Inductive lessdef_state: state -> state -> Prop :=
+  | State_lessdef stk1 stk2 f sp pc rs1 m1 rs2 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (REGS: forall r, Val.lessdef rs1#r rs2#r)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (State stk1 f sp pc rs1 m1) (State stk2 f sp pc rs2 m2)
+  | Call_lessdef stk1 stk2 f args1 args2 m1 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (ARGS: Val.lessdef_list args1 args2)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (Callstate stk1 f args1 m1) (Callstate stk2 f args2 m2)
+  | Return_lessdef stk1 stk2 v1 v2 m1 m2
+      (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+      (REGS: Val.lessdef v1 v2)
+      (MEMS: Mem.extends m1 m2)
+      :lessdef_state (Returnstate stk1 v1 m1) (Returnstate stk2 v2 m2)
+  .
+Local Hint Constructors lessdef_stackframe lessdef_state: core.
+
+Lemma lessdef_stackframe_refl stf: lessdef_stackframe stf stf.
+Proof.
+  destruct stf; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stackframe_refl: core.
+Lemma lessdef_stack_refl stk: list_forall2 lessdef_stackframe stk stk.
+Proof.
+  induction stk; simpl; constructor; auto.
+Qed.
+
+Local Hint Resolve lessdef_stack_refl: core.
+
+Lemma lessdef_list_refl args: Val.lessdef_list args args.
+Proof.
+  induction args; simpl; auto.
+Qed.
+
+Local Hint Resolve lessdef_list_refl Mem.extends_refl: core.
+
+Lemma lessdef_state_refl s: lessdef_state s s.
+Proof.
+  induction s; simpl; constructor; auto.
+Qed.
 
-Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
+Local Hint Resolve Val.lessdef_trans: core.
+Lemma lessdef_stackframe_trans stf1 stf2 stf3:
+  lessdef_stackframe stf1 stf2 -> lessdef_stackframe stf2 stf3 -> lessdef_stackframe stf1 stf3.
+Proof.
+  destruct 1. intros LD; inv LD; try econstructor; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stackframe_trans: core.
+Lemma lessdef_stack_trans stk1 stk2:
+  list_forall2 lessdef_stackframe stk1 stk2 -> 
+  forall stk3, list_forall2 lessdef_stackframe stk2 stk3 -> 
+  list_forall2 lessdef_stackframe stk1 stk3.
+Proof.
+  induction 1; intros stk3 LD; inv LD; econstructor; eauto.
+Qed.
+
+Local Hint Resolve lessdef_stack_trans Mem.extends_extends_compose Val.lessdef_list_trans: core.
+Lemma lessdef_state_trans s1 s2 s3: lessdef_state s1 s2 -> lessdef_state s2 s3 -> lessdef_state s1 s3.
+Proof.
+  destruct 1; intros LD; inv LD; econstructor; eauto.
+Qed.
+
+Lemma init_regs_lessdef_preserv args1 args2
+  (ARGS : Val.lessdef_list args1 args2)
+  : forall rl r, Val.lessdef (init_regs args1 rl)#r (init_regs args2 rl)#r.
+Proof.
+  induction ARGS; simpl; auto.
+  intros rl r1; destruct rl; simpl in *; auto.
+  eapply set_reg_lessdef; eauto.
+  intros r2; eauto.
+Qed.
+Local Hint Resolve init_regs_lessdef_preserv: core.
+
+Lemma tr_inputs_lessdef f rs1 rs2 tbl or r
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  :Val.lessdef (tr_inputs f tbl or rs1)#r (tid f tbl or rs2)#r.
+Proof.
+  unfold tid; rewrite tr_inputs_get.
+  autodestruct.
+Qed.
+Local Hint Resolve tr_inputs_lessdef: core.
 
+Lemma find_function_lessdef ge ros rs1 rs2 fd
+  (FIND: find_function ge ros rs1 = Some fd)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  : find_function ge ros rs2 = Some fd.
+Proof.
+  destruct ros; simpl in *; auto.
+  exploit Genv.find_funct_inv; eauto.
+  intros (b & EQ).
+  destruct (REGS r); try congruence.
+Qed.
+Local Hint Resolve find_function_lessdef regs_lessdef_regs: core.
+
+
+Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of
+  (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of)
+  rs2 m2
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS: Mem.extends m1 m2)
+  : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) 
+     /\ (forall r, Val.lessdef rs1'#r rs2'#r)
+     /\ (Mem.extends m1' m2').
+Proof.
+  induction ISTEP; simpl; try_simplify_someHyps.
+Admitted.
+
+Local Hint Constructors final_step list_forall2: core.
+Local Hint Unfold regs_lessdef: core.
+
+Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
+  (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1)
+  (STACKS: list_forall2 lessdef_stackframe stk1 stk2)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS: Mem.extends m1 m2)
+  : exists s2, final_step tid ge stk2 f sp rs2 m2 fin t s2
+               /\ lessdef_state s1 s2.
+Proof.
+  destruct FSTEP; try (eexists; split; simpl; econstructor; eauto; fail).
+  - (* return *)
+    exploit Mem.free_parallel_extends; eauto.
+    intros (m2' & FREE & MEMS2).
+    eexists; split; simpl; econstructor; eauto.
+    destruct or; simpl; auto.
+  - (* tailcall *)
+    exploit Mem.free_parallel_extends; eauto.
+    intros (m2' & FREE & MEMS2).
+    eexists; split; simpl; econstructor; eauto.
+  - (* builtin *)
+    exploit (eval_builtin_args_lessdef (ge:=ge) (e1:=(fun r => rs1 # r)) (fun r => rs2 # r)); eauto.
+    intros (vl2' & BARGS & VARGS).
+    exploit external_call_mem_extends; eauto.
+    intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED).
+    eexists; split; simpl; econstructor; eauto.
+    intros; apply set_res_lessdef; eauto.
+  - (* jumptable *)
+    eexists; split; simpl; econstructor; eauto.
+    destruct (REGS arg); try congruence.
+Qed.
+
+Lemma fsem2cfgsem_ibstep_simu ge stk1 stk2 f sp rs1 m1 ib t s1 rs2 m2
+  (STEP: iblock_step tr_inputs ge stk1 f sp rs1 m1 ib t s1)
+  (STACKS : list_forall2 lessdef_stackframe stk1 stk2)
+  (REGS: forall r, Val.lessdef rs1#r rs2#r)
+  (MEMS : Mem.extends m1 m2)
+  : exists s2, iblock_step tid ge stk2 f sp rs2 m2 ib t s2
+               /\ lessdef_state s1 s2.
+Proof.
+  destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP).
+  exploit fsem2cfgsem_ibistep_simu; eauto.
+  intros (rs2' & m2' & ISTEP2 & REGS2 & MEMS2).
+  rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP REGS MEMS.
+  exploit fsem2cfgsem_finalstep_simu; eauto.
+  intros (s2 & FSTEP2 & LESSDEF). clear FSTEP.
+  unfold iblock_step; eexists; split; eauto.
+Qed.
+
+Local Hint Constructors step: core.
+
+Lemma fsem2cfgsem_step_simu ge s1 t s1' s2
+ (STEP: step tr_inputs ge s1 t s1')
+ (REGS: lessdef_state s1 s2)
+ :exists s2' : state,
+   step tid ge s2 t s2' /\
+   lessdef_state s1' s2'.
+Proof.
+  destruct STEP; inv REGS.
+  - (* iblock *)
+    intros; exploit fsem2cfgsem_ibstep_simu; eauto. clear STEP.
+    intros (s2 & STEP2 & REGS2).
+    eexists; split; eauto.
+  - (* internal call *)
+    exploit (Mem.alloc_extends m m2 0 (fn_stacksize f) stk m' 0 (fn_stacksize f)); eauto.
+    1-2: lia.
+    intros (m2' & ALLOC2 & MEMS2). clear ALLOC MEMS.
+    eexists; split; econstructor; eauto.
+  - (* external call *)
+    exploit external_call_mem_extends; eauto.
+    intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). clear EXTCALL MEMS.
+    eexists; split; econstructor; eauto.
+  - (* return *)
+    inversion STACKS as [|d1 d2 d3 d4 STF2 STK2]. subst.
+    inv STF2.
+    eexists; split; econstructor; eauto.
+    intros; eapply set_reg_lessdef; eauto.
+Qed.
+
+Theorem fsem2cfgsem prog:
+  forward_simulation (fsem prog) (cfgsem prog).
+Proof.
+  eapply forward_simulation_step with lessdef_state; simpl; auto.
+  - destruct 1; intros; eexists; intuition eauto. econstructor; eauto.
+  - intros s1 s2 r REGS FINAL; destruct FINAL.
+     inv REGS; inv STACKS; inv REGS0.
+     econstructor; eauto.
+  - intros; eapply fsem2cfgsem_step_simu; eauto.
+Qed.
 
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)