starting refinement of symbolic execution

1 files changed, 9 insertions, 9 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 9ab64d7d..4b4571e4 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -437,7 +437,7 @@ Inductive sem_sfval ctx stk: sfval -> regset -> mem -> trace -> state -> Prop :=
 
 (* 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 }.
+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 (sis: sistate) (rs: regset) (m: mem): Prop :=
@@ -446,25 +446,25 @@ Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop :=
   /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r).
 
 (** * Symbolic execution of final step *)
-Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
+Definition sexec_final_sfv (i: final) (sreg: reg -> sval): 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
+    let svos := sum_left_map sreg ros in
+    let sargs := list_sval_inj (List.map 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
+    let svos := sum_left_map sreg ros in
+    let sargs := list_sval_inj (List.map sreg args) in
     Stailcall sig svos sargs
   | Bbuiltin ef args res pc =>
-    let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in
+    let sargs := List.map (builtin_arg_map sreg) args in
     Sbuiltin ef sargs res pc
   | Breturn or => 
-    let sor := SOME r <- or IN Some (sis.(si_sreg) r) in
+    let sor := SOME r <- or IN Some (sreg r) in
     Sreturn sor
   | Bjumptable reg tbl =>
-    let sv := sis.(si_sreg) reg in
+    let sv := sreg reg in
     Sjumptable sv tbl
   end.