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

2 files changed, 541 insertions, 1 deletions

diff --git a/Makefile b/Makefile
index 934b8586..29c1816f 100644
--- a/Makefile
+++ b/Makefile
@@ -143,7 +143,8 @@ SCHEDULING= \
   RTLpathproof.v           RTLpathSE_theory.v \
   RTLpathSchedulerproof.v  RTLpath.v \
   RTLpathScheduler.v       RTLpathWFcheck.v \
-  BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v
+  BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \
+  BTL_SEtheory.v
 
 # C front-end modules (in cfrontend/)
 
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
new file mode 100644
index 00000000..7025b90c
--- /dev/null
+++ b/scheduling/BTL_SEtheory.v
@@ -0,0 +1,539 @@
+(* A theory of symbolic execution on BTL
+
+NB: an efficient implementation with hash-consing will be defined in another file (some day)
+
+*)
+
+Require Import Coqlib Maps Floats.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+Require Import Op Registers.
+Require Import RTL BTL OptionMonad.
+
+(* TODO remove this, when copy-paste of RTLpathSE_theory is clearly over... *)
+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 := {
+  cge: BTL.genv;
+  csp: val;
+  cstk: list stackframe;
+  cf: function;
+  crs0: regset;
+  cm0: mem
+}.
+
+(** * Syntax and semantics of symbolic values *)
+
+(* symbolic value *)
+Inductive sval :=
+  | Sinput (r: reg)
+  | Sop (op:operation) (lsv: list_sval)  (sm: smem)
+  | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) 
+with list_sval := 
+  | Snil
+  | Scons (sv: sval) (lsv: list_sval)
+(* symbolic memory *)
+with smem :=
+  | Sinit 
+  | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval).
+
+Scheme sval_mut := Induction for sval Sort Prop
+with list_sval_mut := Induction for list_sval Sort Prop
+with smem_mut := Induction for smem Sort Prop.
+
+Fixpoint list_sval_inj (l: list sval): list_sval :=
+  match l with
+  | nil => Snil
+  | v::l => Scons v (list_sval_inj l)
+  end.
+
+Local Open Scope option_monad_scope.
+
+Fixpoint eval_sval ctx (sv: sval): option val :=
+  match sv with
+  | Sinput r => Some ((crs0 ctx)#r)
+  | Sop op l sm =>
+     SOME args <- eval_list_sval ctx l IN
+     SOME m <- eval_smem ctx sm IN
+     eval_operation (cge ctx) (csp ctx) op args m
+  | Sload sm trap chunk addr lsv =>
+      match trap with
+      | TRAP =>
+          SOME args <- eval_list_sval ctx lsv IN
+          SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN
+          SOME m <- eval_smem ctx sm IN
+          Mem.loadv chunk m a
+      | NOTRAP =>
+          SOME args <- eval_list_sval ctx lsv IN
+          match (eval_addressing (cge ctx) (csp ctx) addr args) with
+          | None => Some (default_notrap_load_value chunk)
+          | Some a =>
+              SOME m <- eval_smem ctx sm IN
+              match (Mem.loadv chunk m a) with
+              | None => Some (default_notrap_load_value chunk)
+              | Some val => Some val
+              end
+          end
+      end
+  end
+with eval_list_sval ctx (lsv: list_sval): option (list val) :=
+  match lsv with
+  | Snil => Some nil
+  | Scons sv lsv' => 
+    SOME v <- eval_sval ctx sv IN
+    SOME lv <- eval_list_sval ctx lsv' IN
+    Some (v::lv)
+  end
+with eval_smem ctx (sm: smem): option mem :=
+  match sm with
+  | Sinit => Some (cm0 ctx)
+  | Sstore sm chunk addr lsv srce =>
+     SOME args <- eval_list_sval ctx lsv IN
+     SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN
+     SOME m <- eval_smem ctx sm IN
+     SOME sv <- eval_sval ctx srce IN
+     Mem.storev chunk m a sv
+  end.
+
+Lemma eval_list_sval_inj ctx l (sreg: reg -> sval) rs: 
+  (forall r : reg, eval_sval ctx (sreg r) = Some (rs # r)) ->
+  eval_list_sval ctx (list_sval_inj (map sreg l)) = Some (rs ## l).
+Proof.
+  intros H; induction l as [|r l]; simpl; repeat autodestruct; auto.
+Qed.
+
+Definition seval_condition ctx (cond: condition) (lsv: list_sval) (sm: smem) : option bool :=
+  SOME args <- eval_list_sval ctx lsv IN
+  SOME m <- eval_smem ctx sm IN
+  eval_condition cond args m.
+
+
+(** * Auxiliary definitions on Builtins *)
+(* TODO: clean this. Some (cge ctx)neric stuffs could be put in [AST.v] *)
+
+Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *)
+
+Variable ctx: iblock_exec_context.
+Variable m: mem.
+
+Inductive seval_builtin_arg: builtin_arg sval -> val -> Prop :=
+  | seval_BA: forall x v,
+      eval_sval ctx x = Some v ->
+      seval_builtin_arg (BA x) v
+  | seval_BA_int: forall n,
+      seval_builtin_arg (BA_int n) (Vint n)
+  | seval_BA_long: forall n,
+      seval_builtin_arg (BA_long n) (Vlong n)
+  | seval_BA_float: forall n,
+      seval_builtin_arg (BA_float n) (Vfloat n)
+  | seval_BA_single: forall n,
+      seval_builtin_arg (BA_single n) (Vsingle n)
+  | seval_BA_loadstack: forall chunk ofs v,
+      Mem.loadv chunk m (Val.offset_ptr (csp ctx) ofs) = Some v ->
+      seval_builtin_arg (BA_loadstack chunk ofs) v
+  | seval_BA_addrstack: forall ofs,
+      seval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs)
+  | seval_BA_loadglobal: forall chunk id ofs v,
+      Mem.loadv chunk m (Senv.symbol_address (cge ctx) id ofs) = Some v ->
+      seval_builtin_arg (BA_loadglobal chunk id ofs) v
+  | seval_BA_addrglobal: forall id ofs,
+      seval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address (cge ctx) id ofs)
+  | seval_BA_splitlong: forall hi lo vhi vlo,
+      seval_builtin_arg hi vhi -> seval_builtin_arg lo vlo ->
+      seval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo)
+  | seval_BA_addptr: forall a1 a2 v1 v2,
+      seval_builtin_arg a1 v1 -> seval_builtin_arg a2 v2 ->
+      seval_builtin_arg (BA_addptr a1 a2)
+                       (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2)
+.
+
+Definition seval_builtin_args (al: list (builtin_arg sval)) (vl: list val) : Prop :=
+  list_forall2 seval_builtin_arg al vl.
+
+Lemma seval_builtin_arg_determ:
+  forall a v, seval_builtin_arg a v -> forall v', seval_builtin_arg a v' -> v' = v.
+Proof.
+  induction 1; intros v' EV; inv EV; try congruence.
+  f_equal; eauto.
+  apply IHseval_builtin_arg1 in H3. apply IHseval_builtin_arg2 in H5. subst; auto. 
+Qed.
+
+Lemma eval_builtin_args_determ:
+  forall al vl, seval_builtin_args al vl -> forall vl', seval_builtin_args al vl' -> vl' = vl.
+Proof.
+  induction 1; intros v' EV; inv EV; f_equal; eauto using seval_builtin_arg_determ.
+Qed.
+
+End SEVAL_BUILTIN_ARG.
+
+(* NB: (cge ctx)neric function that could be put into [AST] file *)
+Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B :=
+  match arg with
+  | BA x => BA (f x)
+  | BA_int n => BA_int n
+  | BA_long n => BA_long n
+  | BA_float f => BA_float f
+  | BA_single s => BA_single s
+  | BA_loadstack chunk ptr => BA_loadstack chunk ptr
+  | BA_addrstack ptr => BA_addrstack ptr
+  | BA_loadglobal chunk id ptr => BA_loadglobal chunk id ptr
+  | BA_addrglobal id ptr => BA_addrglobal id ptr
+  | BA_splitlong ba1 ba2 => BA_splitlong (builtin_arg_map f ba1) (builtin_arg_map f ba2)
+  | BA_addptr ba1 ba2 => BA_addptr (builtin_arg_map f ba1) (builtin_arg_map f ba2)
+  end.
+
+Lemma seval_builtin_arg_correct ctx rs m sreg: forall arg varg,
+  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
+  eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg ->
+  seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg.
+Proof.
+  induction arg.
+  all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence).
+  - intros varg SEVAL BARG. inv BARG. simpl. constructor.
+    eapply IHarg1; eauto. eapply IHarg2; eauto.
+  - intros varg SEVAL BARG. inv BARG. simpl. constructor.
+    eapply IHarg1; eauto. eapply IHarg2; eauto.
+Qed.
+
+Lemma seval_builtin_args_correct ctx rs m sreg args vargs:
+  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
+  eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs ->
+  seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs.
+Proof.
+  induction 2.
+  - constructor.
+  - simpl. constructor; [| assumption].
+    eapply seval_builtin_arg_correct; eauto.
+Qed.
+
+Lemma seval_builtin_arg_complete ctx rs m sreg: forall arg varg,
+  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
+  seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg ->
+  eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg.
+Proof.
+  induction arg.
+  all: intros varg SEVAL BARG; try (inv BARG; constructor; congruence).
+  - inv BARG. rewrite SEVAL in H0. inv H0. constructor.
+  - inv BARG. simpl. constructor.
+    eapply IHarg1; eauto. eapply IHarg2; eauto.
+  - inv BARG. simpl. constructor.
+    eapply IHarg1; eauto. eapply IHarg2; eauto.
+Qed.
+
+Lemma seval_builtin_args_complete ctx rs m sreg: forall args vargs,
+  (forall r, eval_sval ctx (sreg r) = Some rs # r) ->
+  seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs ->
+  eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs.
+Proof.
+  induction args.
+  - simpl. intros. inv H0. constructor.
+  - intros vargs SEVAL BARG. simpl in BARG. inv BARG.
+    constructor; [| eapply IHargs; eauto].
+    eapply seval_builtin_arg_complete; eauto.
+Qed.
+
+Fixpoint seval_builtin_sval ctx bsv :=
+  match bsv with
+  | BA sv => SOME v <- eval_sval ctx sv IN Some (BA v)
+  | BA_splitlong sv1 sv2 =>
+      SOME v1 <- seval_builtin_sval ctx sv1 IN
+      SOME v2 <- seval_builtin_sval ctx sv2 IN
+      Some (BA_splitlong v1 v2)
+  | BA_addptr sv1 sv2 =>
+      SOME v1 <- seval_builtin_sval ctx sv1 IN
+      SOME v2 <- seval_builtin_sval ctx sv2 IN
+      Some (BA_addptr v1 v2)
+  | BA_int i => Some (BA_int i)
+  | BA_long l => Some (BA_long l)
+  | BA_float f => Some (BA_float f)
+  | BA_single s => Some (BA_single s)
+  | BA_loadstack chk ptr => Some (BA_loadstack chk ptr)
+  | BA_addrstack ptr => Some (BA_addrstack ptr)
+  | BA_loadglobal chk id ptr => Some (BA_loadglobal chk id ptr)
+  | BA_addrglobal id ptr => Some (BA_addrglobal id ptr)
+  end.
+
+Fixpoint eval_list_builtin_sval ctx lbsv :=
+  match lbsv with
+  | nil => Some nil
+  | bsv::lbsv => SOME v <- seval_builtin_sval ctx bsv IN
+                 SOME lv <- eval_list_builtin_sval ctx lbsv IN
+                 Some (v::lv)
+  end.
+
+Lemma eval_list_builtin_sval_nil ctx lbs2:
+  eval_list_builtin_sval ctx lbs2 = Some nil ->
+  lbs2 = nil.
+Proof.
+  destruct lbs2; simpl; repeat autodestruct; congruence.
+Qed.
+
+Lemma seval_builtin_sval_arg ctx bs:
+   forall ba m v, 
+   seval_builtin_sval ctx bs = Some ba ->
+   eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v ->
+   seval_builtin_arg ctx m bs v.
+Proof.
+   induction bs; simpl; 
+   try (intros ba m v H; inversion H; subst; clear H;
+        intros H; inversion H; subst;
+        econstructor; auto; fail).
+   - intros ba m v; destruct (eval_sval _ _) eqn: SV;
+     intros H; inversion H; subst; clear H.
+     intros H; inversion H; subst.
+     econstructor; auto.
+   - intros ba m v. 
+     destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence.
+     destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence.
+     intros H; inversion H; subst; clear H.
+     intros H; inversion H; subst.
+     econstructor; eauto.
+   - intros ba m v. 
+     destruct (seval_builtin_sval _ bs1) eqn: SV1; try congruence.
+     destruct (seval_builtin_sval _ bs2) eqn: SV2; try congruence.
+     intros H; inversion H; subst; clear H.
+     intros H; inversion H; subst.
+     econstructor; eauto.
+Qed.
+
+Lemma seval_builtin_arg_sval ctx m v: forall bs,
+  seval_builtin_arg ctx m bs v ->
+  exists ba,
+    seval_builtin_sval ctx bs = Some ba
+    /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v.
+Proof.
+  induction 1.
+  all: try (eexists; constructor; [simpl; reflexivity | constructor]).
+  2-3: try assumption.
+  - eexists. constructor.
+    + simpl. rewrite H. reflexivity.
+    + constructor.
+  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
+    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
+    eexists. constructor.
+    + simpl. rewrite A1. rewrite A2. reflexivity.
+    + constructor; assumption. 
+  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
+    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
+    eexists. constructor.
+    + simpl. rewrite A1. rewrite A2. reflexivity.
+    + constructor; assumption.
+Qed.
+
+Lemma seval_builtin_sval_args ctx lbs:
+   forall lba m v, 
+   eval_list_builtin_sval ctx lbs = Some lba ->
+   list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba v ->
+   seval_builtin_args ctx m lbs v.
+Proof.
+  unfold seval_builtin_args; induction lbs; simpl; intros lba m v.
+  - intros H; inversion H; subst; clear H.
+    intros H; inversion H. econstructor.
+  - destruct (seval_builtin_sval _ _) eqn:SV; try congruence.
+    destruct (eval_list_builtin_sval _ _) eqn: SVL; try congruence.
+    intros H; inversion H; subst; clear H.
+    intros H; inversion H; subst; clear H. 
+    econstructor; eauto.
+    eapply seval_builtin_sval_arg; eauto.
+Qed.
+
+Lemma seval_builtin_args_sval ctx m lv: forall lbs,
+  seval_builtin_args ctx m lbs lv ->
+  exists lba,
+    eval_list_builtin_sval ctx lbs = Some lba
+    /\ list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba lv.
+Proof.
+  induction 1.
+  - eexists. constructor.
+    + simpl. reflexivity.
+    + constructor.
+  - destruct IHlist_forall2 as (lba & A & B).
+    apply seval_builtin_arg_sval in H. destruct H as (ba & A' & B').
+    eexists. constructor.
+    + simpl. rewrite A'. rewrite A. reflexivity.
+    + constructor; assumption.
+Qed.
+
+Lemma seval_builtin_sval_correct ctx m: forall bs1 v bs2,
+  seval_builtin_arg ctx m bs1 v ->
+  (seval_builtin_sval ctx bs1) = (seval_builtin_sval ctx bs2) ->
+  seval_builtin_arg ctx m bs2 v.
+Proof.
+  intros. exploit seval_builtin_arg_sval; eauto.
+  intros (ba & X1 & X2).
+  eapply seval_builtin_sval_arg; eauto.
+  congruence.
+Qed.
+
+Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1,
+  seval_builtin_args ctx m lbs1 vargs ->
+  forall lbs2, (eval_list_builtin_sval ctx lbs1) = (eval_list_builtin_sval ctx lbs2) ->
+  seval_builtin_args ctx m lbs2 vargs.
+Proof.
+  intros. exploit seval_builtin_args_sval; eauto.
+  intros (ba & X1 & X2).
+  eapply seval_builtin_sval_args; eauto.
+  congruence.
+Qed.
+
+(** * Symbolic (final) value of a block *)
+
+Inductive sfval :=
+  | Sgoto (pc: exit)
+  | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit)
+    (* NB: [res] the return register is hard-wired ! Is it restrictive ? *)
+  | Stailcall: signature -> sval + ident -> list_sval -> sfval
+  | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:exit)
+  | Sjumptable (sv: sval) (tbl: list exit)
+  | Sreturn: option sval -> sfval
+.
+
+Definition sfind_function ctx (svos : sval + ident): option fundef :=
+  match svos with
+  | inl sv => SOME v <- eval_sval ctx sv IN Genv.find_funct (cge ctx) v
+  | inr symb => SOME b <- Genv.find_symbol (cge ctx) symb IN Genv.find_funct_ptr (cge ctx) b
+  end
+.
+
+Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
+  | exec_Sgoto pc rs m:
+      sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs m)
+  | exec_Sreturn stk osv rs m m' v:
+      (csp ctx) = (Vptr stk Ptrofs.zero) ->
+      Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
+      match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v ->
+      sem_sfval ctx (Sreturn osv) rs m 
+         E0 (Returnstate (cstk ctx) v m')
+  | exec_Scall rs m sig svos lsv args res pc fd:
+      sfind_function ctx svos = Some fd ->
+      funsig fd = sig ->
+      eval_list_sval ctx lsv = Some args ->
+      sem_sfval ctx (Scall sig svos lsv res pc) rs m
+        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc rs :: (cstk ctx)) fd args m)
+  | exec_Stailcall stk rs m sig svos args fd m' lsv:
+      sfind_function ctx svos = Some fd ->
+      funsig fd = sig ->
+      (csp ctx) = Vptr stk Ptrofs.zero ->
+      Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
+      eval_list_sval ctx lsv = Some args ->
+      sem_sfval ctx (Stailcall sig svos lsv) rs m
+        E0 (Callstate (cstk ctx) fd args m')
+  | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs:
+      seval_builtin_args ctx m sargs vargs ->
+      external_call ef (cge ctx) vargs m t vres m' ->
+      sem_sfval ctx (Sbuiltin ef sargs res pc) rs m
+        t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs) m')
+  | exec_Sjumptable sv tbl pc' n rs m:
+      eval_sval ctx sv = Some (Vint n) ->
+      list_nth_z tbl (Int.unsigned n) = Some pc' ->
+      sem_sfval ctx (Sjumptable sv tbl) rs m
+        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m)
+.
+
+
+
+(* Syntax and Semantics of symbolic internal states *)
+(* [si_pre] is a precondition on initial context *)
+Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg: reg -> sval; si_smem: smem }.
+
+(* Predicate on which (rs, m) is a possible final state after evaluating [st] on ((crs0 ctx), (cm0 ctx)) *)
+Definition sem_sistate ctx (st: sistate) (rs: regset) (m: mem): Prop :=
+  st.(si_pre) ctx
+  /\ eval_smem ctx st.(si_smem) = Some m
+  /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r).
+
+Definition abort_sistate ctx (st: sistate): Prop :=
+  ~(st.(si_pre) ctx)
+  \/ eval_smem ctx st.(si_smem) = None
+  \/ exists (r: reg), eval_sval ctx (st.(si_sreg) r) = None.
+
+(** * Symbolic execution of final step *)
+Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
+  match i with
+  | Bgoto pc => Sgoto pc
+  | Bcall sig ros args res pc => 
+    let svos := sum_left_map sis.(si_sreg) ros in
+    let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
+    Scall sig svos sargs res pc
+  | Btailcall sig ros args =>
+    let svos := sum_left_map sis.(si_sreg) ros in
+    let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
+    Stailcall sig svos sargs
+  | Bbuiltin ef args res pc =>
+    let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in
+    Sbuiltin ef sargs res pc
+  | Breturn or => 
+    let sor := SOME r <- or IN Some (sis.(si_sreg) r) in
+    Sreturn sor
+  | Bjumptable reg tbl =>
+    let sv := sis.(si_sreg) reg in
+    Sjumptable sv tbl
+  end.
+
+Local Hint Constructors sem_sfval: core.
+
+Lemma sexec_final_svf_correct ctx i sis t rs m s:
+  sem_sistate ctx sis rs m ->
+  final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> 
+  sem_sfval ctx (sexec_final_sfv i sis) rs m t s.
+Proof.
+  intros (PRE&MEM&REG). 
+  destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto.
+  + (* Bcall *) intros; eapply exec_Scall; auto.
+    - destruct ros; simpl in * |- *; auto.
+      rewrite REG; auto.
+    - erewrite eval_list_sval_inj; simpl; auto.
+  + (* Btailcall *) intros. eapply exec_Stailcall; eauto.
+    - destruct ros; simpl in * |- *; eauto.
+      rewrite REG; eauto.
+    - erewrite eval_list_sval_inj; simpl; auto.
+  + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto.
+    eapply seval_builtin_args_correct; eauto.
+  + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence.
+Qed.
+
+Local Hint Constructors final_step: core.
+Local Hint Resolve seval_builtin_args_complete: core.
+
+Lemma sexec_final_svf_complete ctx i sis t rs m s:
+  sem_sistate ctx sis rs m ->
+  sem_sfval ctx (sexec_final_sfv i sis) rs m t s
+  -> final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
+Proof.
+  intros (PRE&MEM&REG).
+  destruct i; simpl; intros LAST; inv LAST; eauto.
+  + (* Breturn *)
+    enough (v=regmap_optget res Vundef rs) as ->; eauto.
+    destruct res; simpl in *; congruence.
+  + (* Bcall *)
+    erewrite eval_list_sval_inj in *; try_simplify_someHyps.
+    intros; eapply exec_Bcall; eauto.
+    destruct fn; simpl in * |- *; auto.
+    rewrite REG in * |- ; auto.
+  + (* Btailcall *)
+    erewrite eval_list_sval_inj in *; try_simplify_someHyps.
+    intros; eapply exec_Btailcall; eauto.
+    destruct fn; simpl in * |- *; auto.
+    rewrite REG in * |- ; auto.
+  + (* Bjumptable *)
+    eapply exec_Bjumptable; eauto.
+    congruence.
+Qed.
+
+(* symbolic state *)
+Inductive sstate :=
+  | Sfinal (sis: sistate) (sfv: sfval)
+  | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate)
+ .
+
+Inductive sem_internal_sstate ctx rs m t s: sstate -> Prop :=
+  | sem_Sfinal sis sfv
+     (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_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)
+  .