From 85aa6d418e077a9f492f800b3f61fb5ead705e4d Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 25 May 2021 18:25:22 +0200
Subject: fix Builtin semantics

---
 scheduling/BTL_SEtheory.v | 30 +++---------------------------
 1 file changed, 3 insertions(+), 27 deletions(-)

(limited to 'scheduling/BTL_SEtheory.v')

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index fb7c650f..d682f776 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -441,10 +441,10 @@ Inductive sem_sfval ctx (rsx: reg -> option val): sfval -> regset -> mem -> trac
   | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs rs':
       seval_builtin_args ctx m sargs vargs ->
       external_call ef (cge ctx) vargs m t vres m' ->
-      rs' = tr_inputs ctx.(cf) [pc] None (regmap_setres res vres rs) ->
+      rs' = tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs ->
       (forall r, rsx r = Some rs'#r) ->
       sem_sfval ctx rsx (Sbuiltin ef sargs res pc) rs m
-        t (State (cstk ctx) (cf ctx) (csp ctx) 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 rs':
       eval_sval ctx sv = Some (Vint n) ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
@@ -611,28 +611,6 @@ Admitted.
 
 Local Hint Resolve transfer_sis_correct: core.
 
-(* TODO: move the 3 below functions in [BTL] ?
-   Could be reused for liveness checking ?
-*)
-Definition reg_builtin_res (res: builtin_res reg): option reg :=
-  match res with
-  | BR r => Some r
-  | _ => None
-  end.
-
-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 sig ros args res pc => tr f [pc] (Some res)
-  | Btailcall sig ros args => tr f [] None
-  | Bbuiltin ef args res pc => tr f [pc] (reg_builtin_res res)
-  | Breturn or => tr f [] None
-  | Bjumptable reg tbl => tr f tbl None
-  end.
-
-Definition tr_regs: function -> final -> regset -> regset :=
-  poly_tr tr_inputs.
-
 Definition tr_sis: function -> final -> sistate -> sistate := 
   poly_tr transfer_sis.
 
@@ -695,9 +673,8 @@ Proof.
     - erewrite eval_list_sval_inj; simpl; auto.
   + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto.
     eapply seval_builtin_args_correct; eauto.
-    admit.
   + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence.
-Admitted.
+Qed.
 
 Local Hint Constructors final_step: core.
 Local Hint Resolve seval_builtin_args_exact: core.
@@ -727,7 +704,6 @@ 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 |}.
-- 
cgit