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

Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-work

parents cc740857 aa51677a
......@@ -85,6 +85,7 @@ Record path_info := {
psize: nat; (* number minus 1 of instructions in the path *)
input_regs: Regset.t;
(** Registers that are used (as input_regs) by the "fallthrough successors" of the path *)
pre_output_regs: Regset.t;
(** This field is not used by the verificator, but is helpful for the superblock scheduler *)
output_regs: Regset.t
}.
......
......@@ -152,47 +152,69 @@ Qed.
Local Hint Resolve exit_list_checker_correct: core.
Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
match i with
| Icall sig ros args res pc' =>
ASSERT list_mem args alive IN
ASSERT reg_sum_mem ros alive IN
exit_checker pm (Regset.add res alive) pc' tt
exit_checker pm (Regset.add res por) pc' tt
| Itailcall sig ros args =>
ASSERT list_mem args alive IN
ASSERT reg_sum_mem ros alive IN
Some tt
| Ibuiltin ef args res pc' =>
ASSERT list_mem (params_of_builtin_args args) alive IN
exit_checker pm (reg_builtin_res res alive) pc' tt
ASSERT list_mem (params_of_builtin_args args) alive IN
exit_checker pm (reg_builtin_res res por) pc' tt
| Ijumptable arg tbl =>
ASSERT Regset.mem arg alive IN
ASSERT exit_list_checker pm alive tbl IN
ASSERT exit_list_checker pm por tbl IN
Some tt
| Ireturn optarg =>
ASSERT (reg_option_mem optarg) alive IN
ASSERT (reg_option_mem optarg) alive IN
Some tt
| _ =>
SOME res <- iinst_checker pm alive i IN
exit_checker pm (fst res) (snd res) tt
| _ => None
end.
Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
inst_checker pm alive i = Some tt ->
Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction):
final_inst_checker pm alive por i = Some tt ->
c!pc = Some i -> wellformed_path c pm 0 pc.
Proof.
intros CHECK PC. eapply wf_last_node; eauto.
clear c pc PC. intros pc PC.
destruct i; simpl in * |- *; intuition (subst; eauto);
try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
intros X; exploit exit_checker_res; eauto.
clear X. intros; subst; eauto.
Qed.
Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
match iinst_checker pm alive i with
| Some res =>
ASSERT Regset.subset por (fst res) IN
exit_checker pm por (snd res) tt
| _ =>
ASSERT Regset.subset por alive IN
final_inst_checker pm alive por i
end.
Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction):
inst_checker pm alive por i = Some tt ->
c!pc = Some i -> wellformed_path c pm 0 pc.
Proof.
unfold inst_checker.
destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl.
- simpl; intros CHECK2 PC. eapply wf_last_node; eauto.
destruct i; simpl in * |- *; intuition (subst; eauto);
try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
intros PC CHECK1 CHECK2.
intros; exploit exit_checker_res; eauto.
intros X; inversion X. intros; subst; eauto.
- simpl; intros CHECK2 PC. eapply final_inst_checker_wellformed; eauto.
generalize CHECK2. clear CHECK2. inversion_ASSERT. try_simplify_someHyps.
Qed.
Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc IN
SOME i <- f.(fn_code)!(snd res) IN
inst_checker pm (fst res) i.
inst_checker pm (fst res) (path.(pre_output_regs)) i.
Lemma path_checker_wellformed f pm pc path:
path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.
......
......@@ -99,7 +99,7 @@ let get_path_map code entry join_points =
dig_path_rec n'
end
| None -> Some ({ psize = (Camlcoq.Nat.of_int !psize);
input_regs = Regset.empty; output_regs = Regset.empty },
input_regs = Regset.empty; pre_output_regs = Regset.empty; output_regs = Regset.empty },
!path_successors @ successors_inst inst)
end
else None
......@@ -217,41 +217,50 @@ let analyze f =
let rec traverse code n size =
let inst = get_some @@ PTree.get n code in
if (size == 0) then inst
if (size == 0) then (inst, n)
else
let n' = get_some @@ predicted_successor inst in
traverse code n' (size-1)
let get_outputs liveness code n pi =
let last_instruction = traverse code n (Camlcoq.Nat.to_int pi.psize) in
let get_outputs liveness f n pi =
let (last_instruction, pc_last) = traverse f.fn_code n (Camlcoq.Nat.to_int pi.psize) in
let path_last_successors = successors_inst last_instruction in
let list_input_regs = List.map (
fun n -> get_some @@ PTree.get n liveness
) path_last_successors in
List.fold_left Regset.union Regset.empty list_input_regs
let outputs = List.fold_left Regset.union Regset.empty list_input_regs in
match last_instruction with
| Icall (_, _, _, _, _) | Itailcall (_, _, _)
| Ibuiltin (_, _, _, _) | Ijumptable (_, _)
| Ireturn _ -> ((transfer f pc_last outputs), outputs)
| _ -> (outputs, outputs)
let set_pathmap_liveness f pm =
let liveness = analyze f in
let new_pm = ref PTree.empty in
let code = f.fn_code in
begin
debug "Liveness: "; print_ptree_regset liveness; debug "\n";
List.iter (fun (n, pi) ->
let inputs = get_some @@ PTree.get n liveness in
let outputs = get_outputs liveness code n pi in
let (por, outputs) = get_outputs liveness f n pi in
new_pm := PTree.set n
{psize=pi.psize; input_regs=inputs; output_regs=outputs} !new_pm
{psize=pi.psize; input_regs=inputs; pre_output_regs=por; output_regs=outputs} !new_pm (* FIXME: STUB *)
) (PTree.elements pm);
!new_pm
end
let print_path_info pi = begin
(*debug_flag := true;*)
debug "(psize=%d; " (Camlcoq.Nat.to_int pi.psize);
debug "input_regs=";
debug "\ninput_regs=";
print_regset pi.input_regs;
debug "; output_regs=";
debug "\n; pre_output_regs=";
print_regset pi.pre_output_regs;
debug "\n; output_regs=";
print_regset pi.output_regs;
debug ")"
debug ")\n"
(*debug_flag := false*)
end
let print_path_map path_map = begin
......
......@@ -280,34 +280,22 @@ Proof.
intuition.
- (* Iload *)
inversion_ASSERT; try_simplify_someHyps.
destruct t. (* TODO - simplify that proof ? *)
+ inversion_SOME a0. intros EVAL.
erewrite <- eqlive_reg_listmem; eauto.
try_simplify_someHyps.
inversion_SOME v; try_simplify_someHyps.
repeat (econstructor; simpl; eauto).
eapply eqlive_reg_update.
eapply eqlive_reg_monotonic; eauto.
intros r0; rewrite regset_add_spec.
destruct t.
inversion_SOME a0. intros EVAL.
erewrite <- eqlive_reg_listmem; eauto.
try_simplify_someHyps.
inversion_SOME v; try_simplify_someHyps.
repeat (econstructor; simpl; eauto).
2:
erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto;
destruct (eval_addressing _ _ _ _);
try destruct (Memory.Mem.loadv _ _ _);
try (intros; inv H1; repeat (econstructor; simpl; eauto)).
all:
eapply eqlive_reg_update;
eapply eqlive_reg_monotonic; eauto;
intros r0; rewrite regset_add_spec;
intuition.
+ erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto.
destruct (eval_addressing _ _ _ _).
* destruct (Memory.Mem.loadv _ _ _).
** intros. inv H1. repeat (econstructor; simpl; eauto).
eapply eqlive_reg_update.
eapply eqlive_reg_monotonic; eauto.
intros r0; rewrite regset_add_spec.
intuition.
** intros. inv H1. repeat (econstructor; simpl; eauto).
eapply eqlive_reg_update.
eapply eqlive_reg_monotonic; eauto.
intros r0; rewrite regset_add_spec.
intuition.
* intros. inv H1. repeat (econstructor; simpl; eauto).
eapply eqlive_reg_update.
eapply eqlive_reg_monotonic; eauto.
intros r0; rewrite regset_add_spec.
intuition.
- (* Istore *)
(repeat inversion_ASSERT); try_simplify_someHyps.
inversion_SOME a0. intros EVAL.
......@@ -501,12 +489,23 @@ Proof.
intros H; erewrite (EQLIVE r); eauto.
Qed.
Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive por:
istep ge i sp rs m = Some st ->
final_inst_checker pm alive por i = None.
Proof.
destruct i; simpl; try congruence.
Qed.
(* is it useful ?
Lemma inst_checker_from_iinst_checker i sp rs m st pm alive:
istep ge i sp rs m = Some st ->
inst_checker pm alive i = (SOME res <- iinst_checker pm alive i IN exit_checker pm (fst res) (snd res) tt).
Proof.
destruct i; simpl; try congruence.
unfold inst_checker.
destruct (iinst_checker pm alive i); simpl; auto.
destruct i; simpl; try congruence.
Qed.
*)
Lemma exit_checker_eqlive_ext1 (pm: path_map) (alive: Regset.t) (pc: node) r rs1 rs2:
exit_checker pm (Regset.add r alive) pc tt = Some tt ->
......@@ -586,16 +585,17 @@ Proof.
* intuition. eapply IHtbl; eauto.
Qed.
Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
Lemma final_inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
list_forall2 eqlive_stackframes stk1 stk2 ->
eqlive_reg (ext alive) rs1 rs2 ->
Regset.Subset por alive ->
liveness_ok_function f ->
(fn_code f) ! pc = Some i ->
path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
inst_checker (fn_path f) alive i = Some tt ->
final_inst_checker (fn_path f) alive por i = Some tt ->
exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
Proof.
intros STACKS EQLIVE LIVENESS PC;
intros STACKS EQLIVE SUB LIVENESS PC;
destruct 1 as [i' sp pc rs1 m st1|
sp pc rs1 m sig ros args res pc' fd|
st1 pc rs1 m sig ros args fd m'|
......@@ -604,28 +604,12 @@ Proof.
st1 pc rs1 m optr m'];
try_simplify_someHyps.
+ (* istate *)
intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto.
inversion_SOME res.
intros.
destruct (icontinue st1) eqn: CONT.
- (* CONT => true *)
exploit iinst_checker_eqlive; eauto.
destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
repeat (econstructor; simpl; eauto).
rewrite <- MEM, <- PC2.
exploit exit_checker_eqlive; eauto.
intros (path & PATH & EQLIVE2).
eapply eqlive_states_intro; eauto.
erewrite <- iinst_checker_istep_continue; eauto.
- (* CONT => false *)
intros; exploit iinst_checker_eqlive_stopped; eauto.
destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
repeat (econstructor; simpl; eauto).
rewrite <- MEM, <- PC2.
eapply eqlive_states_intro; eauto.
intros PC ISTEP. erewrite final_inst_checker_from_iinst_checker; eauto.
congruence.
+ (* Icall *)
repeat inversion_ASSERT. intros.
exploit exit_checker_eqlive_ext1; eauto.
eapply eqlive_reg_monotonic; eauto.
intros (path & PATH & EQLIVE2).
eexists; split.
- eapply exec_Icall; eauto.
......@@ -645,6 +629,7 @@ Proof.
+ (* Ibuiltin *)
repeat inversion_ASSERT. intros.
exploit exit_checker_eqlive_builtin_res; eauto.
eapply eqlive_reg_monotonic; eauto.
intros (path & PATH & EQLIVE2).
eexists; split.
- eapply exec_Ibuiltin; eauto.
......@@ -654,6 +639,7 @@ Proof.
+ (* Ijumptable *)
repeat inversion_ASSERT. intros.
exploit exit_list_checker_eqlive; eauto.
eapply eqlive_reg_monotonic; eauto.
intros (path & PATH & EQLIVE2).
eexists; split.
- eapply exec_Ijumptable; eauto.
......@@ -669,6 +655,44 @@ Proof.
* eapply eqlive_states_return; eauto.
Qed.
Lemma inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
list_forall2 eqlive_stackframes stk1 stk2 ->
eqlive_reg (ext alive) rs1 rs2 ->
liveness_ok_function f ->
(fn_code f) ! pc = Some i ->
path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
inst_checker (fn_path f) alive por i = Some tt ->
exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
Proof.
unfold inst_checker;
intros STACKS EQLIVE LIVENESS PC.
destruct (iinst_checker (fn_path f) alive i) as [res|] eqn: IICHECKER.
+ destruct 1 as [i' sp pc rs1 m st1| | | | | ];
try_simplify_someHyps.
intros IICHECKER PC ISTEP. inversion_ASSERT.
intros.
destruct (icontinue st1) eqn: CONT.
- (* CONT => true *)
exploit iinst_checker_eqlive; eauto.
destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
repeat (econstructor; simpl; eauto).
rewrite <- MEM, <- PC2.
apply Regset.subset_2 in H.
exploit exit_checker_eqlive; eauto.
eapply eqlive_reg_monotonic; eauto.
intros (path & PATH & EQLIVE2).
eapply eqlive_states_intro; eauto.
erewrite <- iinst_checker_istep_continue; eauto.
- (* CONT => false *)
intros; exploit iinst_checker_eqlive_stopped; eauto.
destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
repeat (econstructor; simpl; eauto).
rewrite <- MEM, <- PC2.
eapply eqlive_states_intro; eauto.
+ inversion_ASSERT.
intros; exploit final_inst_checker_eqlive; eauto.
Qed.
Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2:
path_step ge pge (psize path) stk1 f sp rs1 m pc t s1 ->
list_forall2 eqlive_stackframes stk1 stk2 ->
......
......@@ -1923,22 +1923,6 @@ Qed.
Global Opaque PTree_frame_eq_check.
Local Hint Resolve PTree_frame_eq_check_correct: wlp.
Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
DEBUG("? last check");;
phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";;
PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2);;
Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
DEBUG("=> last check: OK").
Lemma hsilocal_simu_check_correct hst1 hst2:
WHEN hsilocal_simu_check hst1 hst2 ~> _ THEN
hsilocal_simu_spec None hst1 hst2.
Proof.
unfold hsilocal_simu_spec; wlp_simplify.
Qed.
Hint Resolve hsilocal_simu_check_correct: wlp.
Global Opaque hsilocal_simu_check.
Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
DEBUG("? frame check");;
phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";;
......@@ -1966,7 +1950,7 @@ Local Hint Resolve regset_elements_in: core.
Lemma hsilocal_frame_simu_check_correct hst1 hst2 alive:
WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> _ THEN
hsilocal_simu_spec (Some alive) hst1 hst2.
hsilocal_simu_spec alive hst1 hst2.
Proof.
unfold hsilocal_simu_spec; wlp_simplify. symmetry; eauto.
Qed.
......@@ -2020,13 +2004,13 @@ Qed.
Hint Resolve hsiexits_simu_check_correct: wlp.
Global Opaque hsiexits_simu_check.
Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsistate) :=
hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2);;
hsilocal_simu_check (hsi_local hst1) (hsi_local hst2).
hsilocal_frame_simu_check (Regset.elements outframe) (hsi_local hst1) (hsi_local hst2).
Lemma hsistate_simu_check_correct dm f hst1 hst2:
WHEN hsistate_simu_check dm f hst1 hst2 ~> _ THEN
hsistate_simu_spec dm f hst1 hst2.
Lemma hsistate_simu_check_correct dm f outframe hst1 hst2:
WHEN hsistate_simu_check dm f outframe hst1 hst2 ~> _ THEN
hsistate_simu_spec dm f outframe hst1 hst2.
Proof.
unfold hsistate_simu_spec; wlp_simplify.
Qed.
......@@ -2160,18 +2144,18 @@ Qed.
Hint Resolve sfval_simu_check_correct: wlp.
Global Opaque sfval_simu_check.
Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);;
Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsstate) :=
hsistate_simu_check dm f outframe (hinternal hst1) (hinternal hst2);;
sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2).
Lemma hsstate_simu_check_correct dm f hst1 hst2:
WHEN hsstate_simu_check dm f hst1 hst2 ~> _ THEN
hsstate_simu_spec dm f hst1 hst2.
Lemma hsstate_simu_check_correct dm f outframe hst1 hst2:
WHEN hsstate_simu_check dm f outframe hst1 hst2 ~> _ THEN
hsstate_simu_spec dm f outframe hst1 hst2.
Proof.
unfold hsstate_simu_spec; wlp_simplify.
Qed.
Hint Resolve hsstate_simu_check_correct: wlp.
Global Opaque hsstate_simu_check.
Global Opaque hsstate_simu_check.
Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit :=
let (pc2, pc1) := m in
......@@ -2185,8 +2169,10 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
DO hst1 <~ hsexec f pc1;;
XDEBUG pc2 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of output superblock: " +; name_pc)%string);;
DO hst2 <~ hsexec tf pc2;;
DO path <~ some_or_fail ((fn_path f)!pc1) "simu_check_single.internal_error.1";;
let outframe := path.(pre_output_regs) in
(* comparing the executions *)
hsstate_simu_check dm f hst1 hst2.
hsstate_simu_check dm f outframe hst1 hst2.
Lemma simu_check_single_correct dm tf f pc1 pc2:
WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN
......@@ -2197,7 +2183,7 @@ Proof.
intros (st2 & SEXEC2 & REF2). try_simplify_someHyps.
exploit H3; clear H3. 1-3: wlp_simplify.
intros (st3 & SEXEC3 & REF3). try_simplify_someHyps.
eexists. split; eauto.
eexists. eexists. split; eauto. split; eauto.
intros ctx.
eapply hsstate_simu_spec_correct; eauto.
Qed.
......
......@@ -18,10 +18,10 @@ Local Open Scope list_scope.
(** * Auxilary notions on simulation tests *)
Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) (sl1 sl2: sistate_local) (ctx: simu_proof_context f): Prop :=
Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) outframe (sl1 sl2: sistate_local) (ctx: simu_proof_context f): Prop :=
forall is1, ssem_local (the_ge1 ctx) (the_sp ctx) sl1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) ->
exists is2, ssem_local (the_ge2 ctx) (the_sp ctx) sl2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2)
/\ istate_simu f dm is1 is2.
/\ istate_simu f dm outframe is1 is2.
(* a kind of negation of sabort_local *)
Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop :=
......@@ -36,7 +36,7 @@ Proof.
intuition congruence.
Qed.
Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) (ctx: simu_proof_context f) (se1 se2: sistate_exit) :=
Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) outframe (ctx: simu_proof_context f) (se1 se2: sistate_exit) :=
(sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1) ->
(seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1)
(si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) =
......@@ -47,10 +47,10 @@ Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) (ctx: simu_proof
ssem_exit (the_ge1 ctx) (the_sp ctx) se1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) (ipc is1) ->
exists is2,
ssem_exit (the_ge2 ctx) (the_sp ctx) se2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) (ipc is2)
/\ istate_simu f dm is1 is2.
/\ istate_simu f dm outframe is1 is2.
Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) (lse1 lse2: list sistate_exit) (ctx: simu_proof_context f) :=
list_forall2 (siexit_simu dm f ctx) lse1 lse2.
Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) outframe (lse1 lse2: list sistate_exit) (ctx: simu_proof_context f) :=
list_forall2 (siexit_simu dm f outframe ctx) lse1 lse2.
(** * Implementation of Data-structure use in Hash-consing *)
......@@ -318,9 +318,9 @@ Definition hsstate_refines (hst: hsstate) (st:sstate): Prop :=
(** ** Specification of the simulation test on [hsistate_local].
It is motivated by [hsilocal_simu_spec_correct theorem] below
*)
Definition hsilocal_simu_spec (oalive: option Regset.t) (hst1 hst2: hsistate_local) :=
Definition hsilocal_simu_spec (alive: Regset.t) (hst1 hst2: hsistate_local) :=
List.incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
/\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> PTree.get r hst2 = PTree.get r hst1)
/\ (forall r, Regset.In r alive -> PTree.get r hst2 = PTree.get r hst1)
/\ hsi_smem hst1 = hsi_smem hst2.
Definition seval_sval_partial ge sp rs0 m0 hsv :=
......@@ -368,18 +368,14 @@ Proof.
- erewrite MEMOK in OKM. erewrite smem_eval_preserved; eauto.
Qed.
Theorem hsilocal_simu_spec_correct hst1 hst2 of ge1 ge2 sp rs0 m0 rs m st1 st2:
hsilocal_simu_spec of hst1 hst2 ->
Theorem hsilocal_simu_spec_correct hst1 hst2 alive ge1 ge2 sp rs0 m0 rs m st1 st2:
hsilocal_simu_spec alive hst1 hst2 ->
hsilocal_refines ge1 sp rs0 m0 hst1 st1 ->
hsilocal_refines ge2 sp rs0 m0 hst2 st2 ->
(forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
ssem_local ge1 sp st1 rs0 m0 rs m ->
match of with
| None => ssem_local ge2 sp st2 rs0 m0 rs m
| Some alive =>
let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2)
in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs'
end.
let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2)
in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs'.
Proof.
intros CORE HREF1 HREF2 GFS SEML.
refine (modusponens _ _ (ssem_local_refines_hok _ _ _ _ _ _ _ _ _ _) _); eauto.
......@@ -394,9 +390,8 @@ Proof.
rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3.
erewrite smem_eval_preserved; [| eapply GFS].
rewrite MEMEQ1; auto. }
destruct of as [alive |].
- constructor.
+ constructor; [assumption | constructor; [assumption|]].
constructor.
+ constructor; [assumption | constructor; [assumption|]].
destruct HREF2 as (B & _ & A & _).
(** B is used for the auto below. *)
assert (forall r : positive, hsi_sreg_eval ge2 sp hst2 r rs0 m0 = seval_sval ge2 sp (si_sreg st2 r) rs0 m0) by auto.
......@@ -420,17 +415,6 @@ Proof.
unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; [|assumption]. rewrite RSEQ. reflexivity.
++ rewrite <- RSEQ. rewrite <- B; [|assumption]. unfold hsi_sreg_eval, hsi_sreg_proj.
rewrite <- C; [|assumption]. rewrite HST2. reflexivity.
- constructor; [|constructor].
+ destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2.
+ destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _).
destruct CORE as (_ & _ & MEMEQ3).
rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3.
erewrite smem_eval_preserved; [| eapply GFS].
rewrite MEMEQ1; auto.
+ intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _).
destruct CORE as (_ & C & _). rewrite <- A; auto. unfold hsi_sreg_eval, hsi_sreg_proj.
rewrite C; [|auto]. erewrite seval_preserved; [| eapply GFS].
unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; auto.
Qed.
(** ** Specification of the simulation test on [hsistate_exit].
......@@ -438,17 +422,17 @@ Qed.
*)
Definition hsiexit_simu_spec dm f (hse1 hse2: hsistate_exit) :=
(exists path, (fn_path f) ! (hsi_ifso hse1) = Some path
/\ hsilocal_simu_spec (Some path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2))
/\ hsilocal_simu_spec path.(input_regs) (hsi_elocal hse1) (hsi_elocal hse2))
/\ dm ! (hsi_ifso hse2) = Some (hsi_ifso hse1)
/\ hsi_cond hse1 = hsi_cond hse2
/\ hsi_scondargs hse1 = hsi_scondargs hse2.
Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2,
Definition hsiexit_simu dm f outframe (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2,
hsiexit_refines_stat hse1 se1 ->
hsiexit_refines_stat hse2 se2 ->
hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 ->
hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
siexit_simu dm f ctx se1 se2.
siexit_simu dm f outframe ctx se1 se2.
Lemma hsiexit_simu_spec_nofail dm f hse1 hse2 ge1 ge2 sp rs m:
hsiexit_simu_spec dm f hse1 hse2 ->
......@@ -461,9 +445,9 @@ Proof.
eapply hsilocal_simu_spec_nofail; eauto.
Qed.
Theorem hsiexit_simu_spec_correct dm f hse1 hse2 ctx:
Theorem hsiexit_simu_spec_correct dm f outframe hse1 hse2 ctx:
hsiexit_simu_spec dm f hse1 hse2 ->
hsiexit_simu dm f ctx hse1 hse2.
hsiexit_simu dm f outframe ctx hse1 hse2.