diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-26 21:42:33 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-27 09:46:24 +0200 |
commit | d76f6a446a8c4866d7e89b1b5b13b24a20e6d1dc (patch) | |
tree | 7b824d1c739f06d0692dc7790067495758c508aa /scheduling/BTL.v | |
parent | 47599a2ea88799d654ec644fe5ba9892087adb39 (diff) | |
download | compcert-kvx-d76f6a446a8c4866d7e89b1b5b13b24a20e6d1dc.tar.gz compcert-kvx-d76f6a446a8c4866d7e89b1b5b13b24a20e6d1dc.zip |
end of BTL_SEtheory w.r.t fsem
Diffstat (limited to 'scheduling/BTL.v')
-rw-r--r-- | scheduling/BTL.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 5f75231a..6f699cd0 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -391,10 +391,11 @@ Definition semantics (p: program) := (** The "functional" small-step semantics for a BTL program. at each exit, we only transfer register in "input_regs" (i.e. "alive" registers). *) - Definition transfer_regs (inputs: list reg) (rs: regset): regset := init_regs (rs##inputs) inputs. +(* TODO: LEMMA BELOW ON transfer_regs USEFUL ? *) + Lemma transfer_regs_inputs inputs rs r: List.In r inputs -> (transfer_regs inputs rs)#r = rs#r. Proof. @@ -456,6 +457,9 @@ Definition inputs_exit (f:function) (tbl: list exit) (or: option reg): Regset.t Definition tr_inputs (f:function) (tbl: list exit) (or:option reg): regset -> regset := transfer_regs (Regset.elements (inputs_exit f tbl or)). +(* TODO: BELOW, LEMMA on tr_inputs USEFUL ? *) + + (* 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. @@ -518,6 +522,7 @@ Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: fina Definition tr_regs: function -> final -> regset -> regset := poly_tr tr_inputs. +(* TODO: NOT USEFUL ? Definition liveout: function -> final -> Regset.t := poly_tr inputs_exit. @@ -533,7 +538,7 @@ Proof. Local Opaque inputs_exit. destruct fi; simpl; auto. Qed. - +*) (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) |