Commit 75a9af77 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

starting an interface for target rewriting rules.

parent 3b6a45c1
......@@ -430,6 +430,102 @@ 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 *)
Fixpoint fsval_proj hsv: ?? hsval :=
match hsv with
| HSinput r hc =>
DO b <~ phys_eq hc unknown_hid;;
if b
then hSinput r (* was not yet really hash-consed *)
else RET hsv (* already hash-consed *)
| HSop op hl hc =>
DO b <~ phys_eq hc unknown_hid;;
if b
then (* was not yet really hash-consed *)
DO hl' <~ fsval_list_proj hl;;
hSop op hl'
else RET hsv (* already hash-consed *)
| HSload hm t chk addr hl _ => RET hsv (* FIXME ? *)
end
with fsval_list_proj hl: ?? list_hsval :=
match hl with
| HSnil hc =>
DO b <~ phys_eq hc unknown_hid;;
if b
then hSnil() (* was not yet really hash-consed *)
else RET hl (* already hash-consed *)
| HScons hv hl hc =>
DO b <~ phys_eq hc unknown_hid;;
if b
then (* was not yet really hash-consed *)
DO hv' <~ fsval_proj hv;;
DO hl' <~ fsval_list_proj hl;;
hScons hv' hl'
else RET hl (* already hash-consed *)
end.
Lemma fsval_proj_correct hsv:
WHEN fsval_proj hsv ~> hsv' THEN forall ge sp rs0 m0,
seval_hsval ge sp hsv rs0 m0 = seval_hsval ge sp hsv' rs0 m0.
Admitted.
Global Opaque fsval_proj.
Local Hint Resolve fsval_proj_correct: wlp.
(* END "fake" hsval ... *)
(** ** Assignment of memory *)
Definition hslocal_set_smem (hst:hsistate_local) hm :=
{| hsi_smem := hm;
......@@ -596,6 +692,23 @@ Proof.
explore; try congruence.
Qed.
(* TODO: This function could be defined in a specific file for each target *)
Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
None. (* default implementation *)
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)
(REF: hsilocal_refines ge sp rs0 m0 hst st)
(OK0: hsok_local ge sp rs0 m0 hst)
(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.
unfold target_op_simplify; simpl. congruence.
Qed.
Global Opaque target_op_simplify.
(** simplify a symbolic value before assignment to a register *)
Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
match rsv with
......@@ -603,8 +716,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
match is_move_operation op lr with
| Some arg => hsi_sreg_get hst arg (** optimization of Omove *)
| None =>
DO lhsv <~ hlist_args hst lr;;
hSop op lhsv
match target_op_simplify op lr hst with
| Some fhv => fsval_proj fhv
| None =>
DO lhsv <~ hlist_args hst lr;;
hSop op lhsv
end
end
| Rload _ chunk addr =>
DO lhsv <~ hlist_args hst lr;;
......@@ -620,17 +737,21 @@ Lemma simplify_correct rsv lr hst:
Proof.
destruct rsv; simpl; auto.
- (* Rop *)
destruct (is_move_operation _ _) eqn: Hmove; wlp_simplify.
+ exploit is_move_operation_correct; eauto.
destruct (is_move_operation _ _) eqn: Hmove.
{ wlp_simplify; exploit is_move_operation_correct; eauto.
intros (Hop & Hlsv); subst; simpl in *.
simplify_SOME z.
* erewrite H; eauto.
* try_simplify_someHyps; congruence.
* congruence.
+ clear Hmove.
generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0.
destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto.
intro H0; clear H0; simplify_SOME z; congruence. (* absurd case *)
* congruence. }
destruct (target_op_simplify _ _ _) eqn: Htarget_op_simp; wlp_simplify.
{ destruct (seval_list_sval _ _ _) eqn: OKlist; try congruence.
destruct (seval_smem _ _ _ _ _) eqn: OKmem; try congruence.
rewrite <- H; exploit target_op_simplify_correct; eauto. }
clear Htarget_op_simp.
generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0.
destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto.
intro H0; clear H0; simplify_SOME z; congruence. (* absurd case *)
- (* Rload *)
destruct trap; wlp_simplify.
erewrite H0; eauto.
......
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