From d858606e8400e6aab627f4aac5ec33ce9c2c80fe Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Thu, 20 May 2021 18:34:46 +0200
Subject: defines fsem (aka functional semantics) of BTL

---
 scheduling/BTL_SEtheory.v | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

(limited to 'scheduling/BTL_SEtheory.v')

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index b9a05a8a..5125ea3c 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -4,6 +4,8 @@ NB: an efficient implementation with hash-consing will be defined in another fil
 
 *)
 
+(* TODO: A REVOIR - remplacer les [tid] par [tr_inputs] pour montrer la bisimulation avec [fsem] plutôt. *)
+
 Require Import Coqlib Maps Floats.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import Op Registers.
@@ -580,7 +582,7 @@ 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 -> 
+  final_step tid (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). 
@@ -604,10 +606,12 @@ Local Hint Resolve seval_builtin_args_exact: core.
 Lemma sexec_final_svf_exact 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.
+  -> final_step tid (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.
+  + (* Bgoto *)
+    econstructor.
   + (* Breturn *)
     enough (v=regmap_optget res Vundef rs) as ->; eauto.
     destruct res; simpl in *; congruence.
@@ -621,6 +625,8 @@ Proof.
     intros; eapply exec_Btailcall; eauto.
     destruct fn; simpl in * |- *; auto.
     rewrite REG in * |- ; auto.
+  + (* Bbuiltin *)
+    eapply (exec_Bbuiltin tid); eauto.
   + (* Bjumptable *)
     eapply exec_Bjumptable; eauto.
     congruence.
@@ -799,7 +805,7 @@ Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
   (SIS: sem_sistate ctx sis rs m)
   (CONT: match ofin with
          | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx t s (k sis')
-         | Some fin => final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
+         | Some fin => final_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
          end),
   sem_sstate ctx t s (sexec_rec ib sis k).
 Proof.
@@ -816,7 +822,7 @@ Qed.
   (sexec is a correct over-approximation)
 *)
 Theorem sexec_correct ctx ib t s: 
-  iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
+  iblock_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
   sem_sstate ctx t s (sexec ib).
 Proof.
   destruct 1 as (rs' & m' & fin & ISTEP & FSTEP).
@@ -1049,7 +1055,7 @@ Lemma sexec_rec_exact ctx ib t s1: forall sis k
   ,
      match iblock_istep_run (cge ctx) (csp ctx) ib rs m with
      | Some (out rs' m' (Some fin)) =>
-        exists s2, final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
+        exists s2, final_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
      | Some (out rs' m' None) => exists sis', (sem_sstate ctx t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m')
      | None => False
      end.
@@ -1095,7 +1101,7 @@ Qed.
 *)
 Theorem sexec_exact ctx ib t s1: 
   sem_sstate ctx t s1 (sexec ib) ->
-  exists s2, iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
+  exists s2, iblock_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
              /\ equiv_state s1 s2.
 Proof.
   intros; exploit sexec_rec_exact; eauto.
-- 
cgit