Skip to content

GitLab

Commit 313443c8 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

[Intermediate] Adding fake hsval for Ccomp expansion

parent 7bc14dbf
Hide whitespace changes
Inline Side-by-side
riscV/ExpansionOracle.ml
View file @ 313443c8
......@@ -370,7 +370,7 @@ let rec write_tree exp current code' new_order =
| _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
let expanse (sb : superblock) code pm =
(*debug_flag := true;*)
debug_flag := true;
let new_order = ref [] in
let liveins = ref sb.liveins in
let exp = ref [] in
......@@ -388,7 +388,7 @@ let expanse (sb : superblock) code pm =
debug "Iop/Ccomp\n";
exp := cond_int32s false c a1 a2 dest succ [];
was_exp := true
| Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
(*| Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
debug "Iop/Ccompu\n";
exp := cond_int32u false c a1 a2 dest succ [];
was_exp := true
......@@ -492,7 +492,7 @@ let expanse (sb : superblock) code pm =
debug "Icond/Cnotcompfs\n";
exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 [];
was_branch := true;
was_exp := true
was_exp := true*)
| _ -> new_order := n :: !new_order);
if !was_exp then (
node := !node + 1;
......@@ -510,7 +510,7 @@ let expanse (sb : superblock) code pm =
sb.instructions;
sb.instructions <- Array.of_list (List.rev !new_order);
sb.liveins <- !liveins;
(*debug_flag := false;*)
debug_flag := false;
(!code', !pm')
let rec find_last_node_reg = function
......
riscV/RTLpathSE_simplify.v
View file @ 313443c8
Require Import Integers.
Require Import Op Registers.
Require Import RTLpathSE_theory.
Require Import RTLpathSE_simu_specs.
(* Useful functions for conditions/branches expansion *)
Definition is_inv_cmp_int (cmp: comparison) : bool :=
match cmp with | Cle | Cgt => true | _ => false end.
Definition is_inv_cmp_float (cmp: comparison) : bool :=
match cmp with | Cge | Cgt => true | _ => false end.
Definition make_optR0 (is_x0 is_inv: bool) : option bool :=
if is_x0 then Some is_inv else None.
(* Functions to manage lists of "fake" values *)
Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval :=
let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in
let lhsv := fScons hvfirst fSnil in
fScons hvsec lhsv.
Definition make_lhsv_single (hvs: hsval) : list_hsval :=
fScons hvs fSnil.
(* Expansion functions *)
Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
| Ceq => fSop (OEseqw optR0) lhsv
| Cne => fSop (OEsnew optR0) lhsv
| Clt | Cgt => fSop (OEsltw optR0) lhsv
| Cle | Cge =>
let hvs := (fSop (OEsltw optR0) lhsv) in
let hl := make_lhsv_single hvs in
fSop (OExoriw Int.one) hl
end.
(* Target op simplifications using "fake" values *)
Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
None. (* default implementation *)
match op, lr with
| Ocmp (Ccomp c), a1 :: a2 :: nil =>
let fv1 := fsi_sreg_get hst a1 in
let fv2 := fsi_sreg_get hst a2 in
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
let lhsv := make_lhsv_cmp is_inv fv1 fv2 in
Some (cond_int32s c lhsv optR0)
(*| Ocmp (Ccompu c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int32u c lhsv optR0
| Ocmp (Ccompimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int32s c hv1 imm
| Ocmp (Ccompuimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int32u c hv1 imm
| Ocmp (Ccompl c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int64s c lhsv optR0
| Ocmp (Ccomplu c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int64u c lhsv optR0
| Ocmp (Ccomplimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64s c hv1 imm
| Ocmp (Ccompluimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64u c hv1 imm
| Ocmp (Ccompf c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp false cond_float c lhsv
| Ocmp (Cnotcompf c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp true cond_float c lhsv
| Ocmp (Ccompfs c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp false cond_single c lhsv
| Ocmp (Cnotcompfs c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp true cond_single c lhsv*)
| _, _ => None
end.
Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
(H: target_op_simplify op lr hst = Some fsv)
......@@ -12,8 +117,8 @@ Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
(OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args)
(OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m),
seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m.
Proof.
Proof. Admitted. (*
unfold target_op_simplify; simpl. congruence.
Qed.
Qed.*)
Global Opaque target_op_simplify.
scheduling/RTLpathSE_impl.v
View file @ 313443c8
......@@ -432,63 +432,6 @@ Qed.
Global Opaque hlist_args.
Local Hint Resolve hlist_args_correct: wlp.
(* BEGIN "fake" hsval without real hash-consing *)
(* TODO:
1) put these definitions elsewhere ? in RTLpathSE_simu_specs.v ?
2) reuse these definitions in hSinput, hSop, etc
in order to factorize proofs ?
*)
Definition fSinput (r: reg): hsval :=
HSinput r unknown_hid.
Lemma fSinput_correct r ge sp rs0 m0: (* useless trivial lemma ? *)
sval_refines ge sp rs0 m0 (fSinput r) (Sinput r).
Proof.
auto.
Qed.
Definition fSop (op:operation) (lhsv: list_hsval): hsval :=
HSop op lhsv unknown_hid.
Lemma fSop_correct op lhsv ge sp rs0 m0 lsv sm m: forall
(MEM: seval_smem ge sp sm rs0 m0 = Some m)
(MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
(LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
sval_refines ge sp rs0 m0 (fSop op lhsv) (Sop op lsv sm).
Proof.
intros; simpl. rewrite <- LR, MEM.
destruct (seval_list_sval _ _ _ _); try congruence.
eapply op_valid_pointer_eq; eauto.
Qed.
Definition fsi_sreg_get (hst: PTree.t hsval) r: hsval :=
match PTree.get r hst with
| None => fSinput r
| Some sv => sv
end.
Lemma fsi_sreg_get_correct hst r ge sp rs0 m0 (f: reg -> sval): forall
(RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
sval_refines ge sp rs0 m0 (fsi_sreg_get hst r) (f r).
Proof.
unfold hsi_sreg_eval, hsi_sreg_proj, fsi_sreg_get; intros; simpl.
rewrite <- RR. destruct (hst ! r); simpl; auto.
Qed.
Definition fSnil: list_hsval :=
HSnil unknown_hid.
(* TODO: Lemma fSnil_correct *)
Definition fScons (hsv: hsval) (lhsv: list_hsval): list_hsval :=
HScons hsv lhsv unknown_hid.
(* TODO: Lemma fScons_correct *)
(* END "fake" hsval ... *)
(** Convert a "fake" hash-consed term into a "real" hash-consed term *)
Fixpoint fsval_proj hsv: ?? hsval :=
......@@ -707,15 +650,6 @@ Qed.
(* TODO gourdinl MOVE EXPANSIONS BELOW ELSEWHERE *)
Definition is_inv_cmp_int (cmp: comparison) : bool :=
match cmp with | Cle | Cgt => true | _ => false end.
Definition is_inv_cmp_float (cmp: comparison) : bool :=
match cmp with | Cge | Cgt => true | _ => false end.
Definition make_optR0 (is_x0 is_inv: bool) : option bool :=
if is_x0 then Some is_inv else None.
(* TODO gourdinl IF NEEDED LATER Fixpoint hlist_sval (l: list hsval): ?? list_hsval :=
match l with
| nil => hSnil()
......@@ -724,18 +658,7 @@ Definition make_optR0 (is_x0 is_inv: bool) : option bool :=
hScons r lhsv
end.*)
Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : ?? list_hsval :=
DO hnil <~ hSnil();;
let (hvfirst, hvsec) := if is_inv then (hv1, hv2) else (hv2, hv1) in
DO lhsv <~ hScons hvfirst hnil;;
DO lhsv <~ hScons hvsec lhsv;;
RET lhsv.
Definition make_lhsv_single (hvs: hsval) : ?? list_hsval :=
DO hnil <~ hSnil();;
DO hl <~ hScons hvs hnil;;
RET hl.
(*
Definition load_hilo32 (hi lo: int) :=
DO hnil <~ hSnil();;
if Int.eq lo Int.zero then
......@@ -805,16 +728,6 @@ Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.
Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
| Ceq => hSop (OEseqw optR0) lhsv
| Cne => hSop (OEsnew optR0) lhsv
| Clt | Cgt => hSop (OEsltw optR0) lhsv
| Cle | Cge =>
DO hvs <~ (hSop (OEsltw optR0) lhsv);;
DO hl <~ make_lhsv_single hvs;;
hSop (OExoriw Int.one) hl
end.
Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) :=
match cmp with
......@@ -954,11 +867,12 @@ Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) :=
DO hl <~ make_lhsv_cmp is_inv hv1 hvs;;
cond_int64u cmp hl optR0
end.
*)
(** simplify a symbolic value before assignment to a register *)
Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
match rsv with
| Rop (Omove as op) =>
| Rop op =>
match is_move_operation op lr with
| Some arg => hsi_sreg_get hst arg (* optimization of Omove *)
| None =>
......@@ -969,84 +883,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
hSop op lhsv
end
end
| Rop ((Ocmp cond) as op) =>
match cond, lr with
| (Ccomp c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int32s c lhsv optR0
| (Ccompu c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int32u c lhsv optR0
| (Ccompimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int32s c hv1 imm
| (Ccompuimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int32u c hv1 imm
| (Ccompl c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int64s c lhsv optR0
| (Ccomplu c), a1 :: a2 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
DO hv2 <~ hsi_sreg_get hst a2;;
let is_inv := is_inv_cmp_int c in
let optR0 := make_optR0 false is_inv in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
cond_int64u c lhsv optR0
| (Ccomplimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64s c hv1 imm
| (Ccompluimm c imm), a1 :: nil =>
DO hv1 <~ hsi_sreg_get hst a1;;
expanse_condimm_int64u c hv1 imm
| (Ccompf c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp false cond_float c lhsv
| (Cnotcompf c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp true cond_float c lhsv
| (Ccompfs c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp false cond_single c lhsv
| (Cnotcompfs c), f1 :: f2 :: nil =>
DO hv1 <~ hsi_sreg_get hst f1;;
DO hv2 <~ hsi_sreg_get hst f2;;
let is_inv := is_inv_cmp_float c in
DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
expanse_cond_fp true cond_single c lhsv
| _, _ =>
DO lhsv <~ hlist_args hst lr;;
hSop op lhsv
end
| Rop op =>
DO lhsv <~ hlist_args hst lr;;
hSop op lhsv
| Rload _ chunk addr =>
DO lhsv <~ hlist_args hst lr;;
hSload hst NOTRAP chunk addr lhsv
end.
(*
Lemma simplify_nothing lr (hst: hsistate_local) op:
WHEN DO lhsv <~ hlist_args hst lr;; hSop op lhsv ~> hv
THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset)
......@@ -1905,7 +1747,7 @@ Proof.
4: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl.
5: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl.
all: destruct (Float32.cmp _ _ _); trivial.
Qed.
Qed.*)
Lemma simplify_correct rsv lr hst:
WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st
......@@ -2053,6 +1895,7 @@ Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) :
if is_inv then
hlist_args prev*)
(*
Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) :=
match cmp with
| Ceq => CEbeqw optR0
......@@ -2205,7 +2048,7 @@ Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list
| _, _ =>
DO vargs <~ hlist_args prev args;;
RET (cond, vargs)
end.
end.*)
(** ** Execution of one instruction *)
......
scheduling/RTLpathSE_simu_specs.v
View file @ 313443c8
......@@ -12,6 +12,7 @@ Local Open Scope error_monad_scope.
Local Open Scope option_monad_scope.
Require Export Impure.ImpHCons.
Import HConsing.
Import ListNotations.
Local Open Scope list_scope.
......@@ -304,6 +305,66 @@ Inductive hfinal_refines: hsfval -> sfval -> Prop :=
End HFINAL_REFINES.
(* TODO gourdinl Leave this here ? *)
Section FAKE_HSVAL.
(* BEGIN "fake" hsval without real hash-consing *)
(* TODO:
1) put these definitions elsewhere ? in RTLpathSE_simu_specs.v ?
2) reuse these definitions in hSinput, hSop, etc
in order to factorize proofs ?
*)
Definition fSinput (r: reg): hsval :=
HSinput r unknown_hid.
Lemma fSinput_correct r ge sp rs0 m0: (* useless trivial lemma ? *)
sval_refines ge sp rs0 m0 (fSinput r) (Sinput r).
Proof.
auto.
Qed.
Definition fSop (op:operation) (lhsv: list_hsval): hsval :=
HSop op lhsv unknown_hid.
Lemma fSop_correct op lhsv ge sp rs0 m0 lsv sm m: forall
(MEM: seval_smem ge sp sm rs0 m0 = Some m)
(MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
(LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
sval_refines ge sp rs0 m0 (fSop op lhsv) (Sop op lsv sm).
Proof.
intros; simpl. rewrite <- LR, MEM.
destruct (seval_list_sval _ _ _ _); try congruence.
eapply op_valid_pointer_eq; eauto.
Qed.
Definition fsi_sreg_get (hst: PTree.t hsval) r: hsval :=
match PTree.get r hst with
| None => fSinput r
| Some sv => sv
end.
Lemma fsi_sreg_get_correct hst r ge sp rs0 m0 (f: reg -> sval): forall
(RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
sval_refines ge sp rs0 m0 (fsi_sreg_get hst r) (f r).
Proof.
unfold hsi_sreg_eval, hsi_sreg_proj, fsi_sreg_get; intros; simpl.
rewrite <- RR. destruct (hst ! r); simpl; auto.
Qed.
Definition fSnil: list_hsval :=
HSnil unknown_hid.
(* TODO: Lemma fSnil_correct *)
Definition fScons (hsv: hsval) (lhsv: list_hsval): list_hsval :=
HScons hsv lhsv unknown_hid.
(* TODO: Lemma fScons_correct *)
(* END "fake" hsval ... *)
End FAKE_HSVAL.
Record hsstate := { hinternal:> hsistate; hfinal: hsfval }.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment