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.v | 34 ++++++++++++++++++++++++----------
 1 file changed, 24 insertions(+), 10 deletions(-)

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 4ae7a6dd..954b4cb4 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -18,6 +18,8 @@ Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import RTL Op Registers OptionMonad.
 
+Import ListNotations.
+
 (** * Abstract syntax *)
 
 Definition exit := node.  (* we may generalize this with register renamings at exit, 
@@ -159,12 +161,15 @@ 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.
@@ -286,7 +291,6 @@ Proof.
     destruct o; try_simplify_someHyps; subst; eauto.
 Qed.
 
-Import ListNotations.
 Local Open Scope list_scope.
 
 Inductive final_step stack f sp rs m: final -> trace -> state -> Prop :=
@@ -314,10 +318,7 @@ 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')
-         (* TODO: not clear that this is the better choice ! 
-            we coud also do something like [regmap_setres res vres (tr_exit f [pc'] (reg_builtin_res res) rs)]
-         *)
-         t (State stack f sp pc' (tr_exit f [pc'] None (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' ->
@@ -455,8 +456,6 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t
 Definition tr_inputs (f:function) (pc: list exit) (or:option reg): regset -> regset 
   := transfer_regs (Regset.elements (inputs_exit f pc 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.
@@ -503,6 +502,21 @@ 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 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.
+
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
 
 (** Matching BTL and RTL code 
-- 
cgit