Commit c98683ff authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

specification of pre_output_regs for the simulation checker

parent aaaa8f52
......@@ -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
}.
......
......@@ -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
......@@ -240,7 +240,7 @@ let set_pathmap_liveness f pm =
let inputs = get_some @@ PTree.get n liveness in
let outputs = get_outputs liveness code 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=outputs; output_regs=outputs} !new_pm (* FIXME: STUB *)
) (PTree.elements pm);
!new_pm
end
......
......@@ -1149,22 +1149,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";;
......@@ -1192,7 +1176,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.
......@@ -1246,13 +1230,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.
......@@ -1386,18 +1370,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
......@@ -1411,8 +1395,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
......@@ -1423,7 +1409,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.
Proof.
intros SIMUC st1 st2 HREF1 HREF2 HDYN1 HDYN2.
assert (SEVALC:
......@@ -498,13 +482,13 @@ Proof.
constructor; [|constructor]; simpl; auto.
Qed.
Remark hsiexit_simu_siexit dm f ctx hse1 hse2 se1 se2:
hsiexit_simu dm f ctx hse1 hse2 ->
Remark hsiexit_simu_siexit dm f outframe ctx hse1 hse2 se1 se2:
hsiexit_simu dm f outframe ctx hse1 hse2 ->
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.
Proof.
auto.
Qed.
......@@ -513,15 +497,15 @@ Qed.
It is motivated by [hsiexit_simu_spec_correct theorem] below
*)
Definition hsiexits_simu dm f (ctx: simu_proof_context f) (lhse1 lhse2: list hsistate_exit): Prop :=
list_forall2 (hsiexit_simu dm f ctx) lhse1 lhse2.
Definition hsiexits_simu dm f outframe (ctx: simu_proof_context f) (lhse1 lhse2: list hsistate_exit): Prop :=
list_forall2 (hsiexit_simu dm f outframe ctx) lhse1 lhse2.
Definition hsiexits_simu_spec dm f lhse1 lhse2: Prop :=
list_forall2 (hsiexit_simu_spec dm f) lhse1 lhse2.
Theorem hsiexits_simu_spec_correct dm f lhse1 lhse2 ctx:
Theorem hsiexits_simu_spec_correct dm f outframe lhse1 lhse2 ctx:
hsiexits_simu_spec dm f lhse1 lhse2 ->
hsiexits_simu dm f ctx lhse1 lhse2.
hsiexits_simu dm f outframe ctx lhse1 lhse2.
Proof.
induction 1; [constructor|].
constructor; [|apply IHlist_forall2; assumption].
......@@ -529,8 +513,8 @@ Proof.
Qed.
Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2,
siexits_simu dm f lse1 lse2 ctx ->
Lemma siexits_simu_all_fallthrough dm f outframe ctx: forall lse1 lse2,
siexits_simu dm f outframe lse1 lse2 ctx ->
all_fallthrough (the_ge1 ctx) (the_sp ctx) lse1 (the_rs0 ctx) (the_m0 ctx) ->
(forall se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) ->
all_fallthrough (the_ge2 ctx) (the_sp ctx) lse2 (the_rs0 ctx) (the_m0 ctx).
......@@ -545,8 +529,8 @@ Proof.
Qed.
Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2:
siexits_simu dm f lse1 lse2 ctx ->
Lemma siexits_simu_all_fallthrough_upto dm f outframe ctx lse1 lse2:
siexits_simu dm f outframe lse1 lse2 ctx ->
forall ext1 lx1,
(forall se1, In se1 lx1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) ->
all_fallthrough_upto_exit (the_ge1 ctx) (the_sp ctx) ext1 lx1 lse1 (the_rs0 ctx) (the_m0 ctx) ->
......@@ -570,14 +554,14 @@ Proof.
Qed.
Lemma hsiexits_simu_siexits dm f ctx lhse1 lhse2:
hsiexits_simu dm f ctx lhse1 lhse2 ->
Lemma hsiexits_simu_siexits dm f outframe ctx lhse1 lhse2:
hsiexits_simu dm f outframe ctx lhse1 lhse2 ->
forall lse1 lse2,
hsiexits_refines_stat lhse1 lse1 ->
hsiexits_refines_stat lhse2 lse2 ->
hsiexits_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse1 lse1 ->
hsiexits_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse2 lse2 ->
siexits_simu dm f lse1 lse2 ctx.
siexits_simu dm f outframe lse1 lse2 ctx.
Proof.
induction 1.
- intros. inv H. inv H0. constructor.
......@@ -591,16 +575,16 @@ Qed.
It is motivated by [hsistate_simu_spec_correct theorem] below
*)
Definition hsistate_simu_spec dm f (hse1 hse2: hsistate) :=
Definition hsistate_simu_spec dm f outframe (hse1 hse2: hsistate) :=
list_forall2 (hsiexit_simu_spec dm f) (hsi_exits hse1) (hsi_exits hse2)
/\ hsilocal_simu_spec None (hsi_local hse1) (hsi_local hse2).
/\ hsilocal_simu_spec outframe (hsi_local hse1) (hsi_local hse2).
Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2,
Definition hsistate_simu dm f outframe (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2,
hsistate_refines_stat hst1 st1 ->
hsistate_refines_stat hst2 st2 ->
hsistate_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 ->
hsistate_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 ->
sistate_simu dm f st1 st2 ctx.
sistate_simu dm f outframe st1 st2 ctx.
Lemma list_forall2_nth_error {A} (l1 l2: list A) P:
list_forall2 P l1 l2 ->
......@@ -644,9 +628,9 @@ Proof.
rewrite H0; auto.
Qed.
Theorem hsistate_simu_spec_correct dm f hst1 hst2 ctx:
hsistate_simu_spec dm f hst1 hst2 ->
hsistate_simu dm f hst1 hst2 ctx.
Theorem hsistate_simu_spec_correct dm f outframe hst1 hst2 ctx:
hsistate_simu_spec dm f outframe hst1 hst2 ->
hsistate_simu dm f outframe hst1 hst2 ctx.
Proof.
intros (ESIMU & LSIMU) st1 st2 (PCREF1 & EREF1) (PCREF2 & EREF2) DREF1 DREF2 is1 SEMI.
destruct DREF1 as (DEREF1 & LREF1 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _).
......@@ -655,22 +639,23 @@ Proof.
- destruct SEMI as (SSEML & PCEQ & ALLFU).
exploit hsilocal_simu_spec_correct; eauto; [apply ctx|]. simpl. intro SSEML2.
exists (mk_istate (icontinue is1) (si_pc st2) (irs is1) (imem is1)). constructor.
+ unfold ssem_internal. simpl. rewrite ICONT. constructor; [assumption | constructor; [reflexivity |]].
+ unfold ssem_internal. simpl. rewrite ICONT. admit.
(* constructor; [assumption | constructor; [reflexivity |]].
eapply siexits_simu_all_fallthrough; eauto.
* eapply hsiexits_simu_siexits; eauto.
* eapply nested_sok_prop; eauto.
eapply ssem_local_sok; eauto.
eapply ssem_local_sok; eauto. *)
+ unfold istate_simu. rewrite ICONT. constructor; [simpl; assumption | constructor; [| reflexivity]].
constructor.
- destruct SEMI as (ext & lx & SSEME & ALLFU).
assert (SESIMU: siexits_simu dm f (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto).
assert (SESIMU: siexits_simu dm f outframe (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto).
exploit siexits_simu_all_fallthrough_upto; eauto.
* destruct ALLFU as (ITAIL & ALLF).
exploit nested_sok_tail; eauto. intros NESTED2.
inv NESTED2. destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok in SSEML.
eapply nested_sok_prop; eauto.
* intros (ext2 & lx2 & ALLFU2 & LENEQ).
assert (EXTSIMU: siexit_simu dm f ctx ext ext2). {
assert (EXTSIMU: siexit_simu dm f outframe ctx ext ext2). {
eapply list_forall2_nth_error; eauto.
- destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto.
- destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL.
......@@ -683,7 +668,7 @@ Proof.
+ unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ).
destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ).
exists path. repeat (constructor; auto).
Qed.
Admitted.
(** ** Specification of the simulation test on [sfval].
......@@ -858,18 +843,18 @@ Qed.
It is motivated by [hsstate_simu_spec_correct theorem] below
*)
Definition hsstate_simu_spec (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
hsistate_simu_spec dm f (hinternal hst1) (hinternal hst2)
Definition hsstate_simu_spec (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsstate) :=
hsistate_simu_spec dm f outframe (hinternal hst1) (hinternal hst2)
/\ hfinal_simu_spec dm f (hsi_pc (hinternal hst1)) (hsi_pc (hinternal hst2)) (hfinal hst1) (hfinal hst2).
Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
Definition hsstate_simu dm f outframe (hst1 hst2: hsstate) ctx: Prop :=
forall st1 st2,
hsstate_refines hst1 st1 ->
hsstate_refines hst2 st2 -> sstate_simu dm f st1 st2 ctx.
hsstate_refines hst2 st2 -> sstate_simu dm f outframe st1 st2 ctx.
Theorem hsstate_simu_spec_correct dm f ctx hst1 hst2:
hsstate_simu_spec dm f hst1 hst2 ->
hsstate_simu dm f hst1 hst2 ctx.
Theorem hsstate_simu_spec_correct dm f outframe ctx hst1 hst2:
hsstate_simu_spec dm f outframe hst1 hst2 ->
hsstate_simu dm f outframe hst1 hst2 ctx.
Proof.
intros (SCORE & FSIMU) st1 st2 (SREF1 & DREF1 & FREF1) (SREF2 & DREF2 & FREF2).
generalize SCORE. intro SIMU; eapply hsistate_simu_spec_correct in SIMU; eauto.
......
......@@ -1627,13 +1627,9 @@ Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop :=
/\ eqlive_reg alive is1.(irs) is2.(irs)
/\ is1.(imem) = is2.(imem).
Definition istate_simu f (srce: PTree.t node) is1 is2: Prop :=
Definition istate_simu f (srce: PTree.t node) outframe is1 is2: Prop :=
if is1.(icontinue) then
(* TODO: il faudra raffiner le (fun _ => True) si on veut autoriser l'oracle à
ajouter du "code mort" sur des registres non utilisés (loop invariant code motion à la David)
Typiquement, pour connaître la frame des registres vivants, il faudra faire une propagation en arrière
sur la dernière instruction du superblock. *)
istate_simulive (fun _ => True) srce is1 is2
istate_simulive (fun r => Regset.In r outframe) srce is1 is2
else
exists path, f.(fn_path)!(is1.(ipc)) = Some path
/\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2
......@@ -1651,10 +1647,10 @@ Record simu_proof_context {f1: RTLpath.function} := {
Arguments simu_proof_context: clear implicits.
(* NOTE: a pure semantic definition on [sistate], for a total freedom in refinements *)
Definition sistate_simu (dm: PTree.t node) (f: RTLpath.function) (st1 st2: sistate) (ctx: simu_proof_context f): Prop :=
Definition sistate_simu (dm: PTree.t node) (f: RTLpath.function) outframe (st1 st2: sistate) (ctx: simu_proof_context f): Prop :=
forall is1, ssem_internal (the_ge1 ctx) (the_sp ctx) st1 (the_rs0 ctx) (the_m0 ctx) is1 ->
exists is2, ssem_internal (the_ge2 ctx) (the_sp ctx) st2 (the_rs0 ctx) (the_m0 ctx) is2
/\ istate_simu f dm is1 is2.
/\ istate_simu f dm outframe is1 is2.
Inductive svident_simu (f: RTLpath.function) (ctx: simu_proof_context f): (sval + ident) -> (sval + ident) -> Prop :=
| Sleft_simu sv1 sv2:
......@@ -1885,13 +1881,14 @@ Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node)
= (seval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) ->
sfval_simu dm f opc1 opc2 ctx (Sreturn (Some sv1)) (Sreturn (Some sv2)).
Definition sstate_simu dm f (s1 s2: sstate) (ctx: simu_proof_context f): Prop :=
sistate_simu dm f s1.(internal) s2.(internal) ctx
/\ forall is1,
Definition sstate_simu dm f outframe (s1 s2: sstate) (ctx: simu_proof_context f): Prop :=
sistate_simu dm f outframe s1.(internal) s2.(internal) ctx
/\ forall is1,
ssem_internal (the_ge1 ctx) (the_sp ctx) s1 (the_rs0 ctx) (the_m0 ctx) is1 ->
is1.(icontinue) = true ->
sfval_simu dm f s1.(si_pc) s2.(si_pc) ctx s1.(final) s2.(final).
Definition sexec_simu dm (f1 f2: RTLpath.function) pc1 pc2: Prop :=
forall st1, sexec f1 pc1 = Some st1 ->
exists st2, sexec f2 pc2 = Some st2 /\ forall ctx, sstate_simu dm f1 st1 st2 ctx.
exists path st2, (fn_path f1)!pc1 = Some path /\ sexec f2 pc2 = Some st2
/\ forall ctx, sstate_simu dm f1 path.(pre_output_regs) st1 st2 ctx.
......@@ -167,12 +167,12 @@ Proof.
(* intros. eapply all_fundef_liveness_ok; eauto. *)
Qed.
Lemma sistate_simu f dupmap sp st st' rs m is
Lemma sistate_simu f dupmap outframe sp st st' rs m is
(LIVE: liveness_ok_function f):
ssem_internal ge sp st rs m is ->
sistate_simu dupmap f st st' (mkctx sp rs m LIVE)->
sistate_simu dupmap f outframe st st' (mkctx sp rs m LIVE)->
exists is',
ssem_internal tge sp st' rs m is' /\ istate_simu f dupmap is is'.
ssem_internal tge sp st' rs m is' /\ istate_simu f dupmap outframe is is'.
Proof.
intros SEM X; eapply X; eauto.
Qed.
......@@ -198,13 +198,12 @@ Lemma ssem_final_simu dm f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s
(LIVE: liveness_ok_function f):
match_function dm f f' ->
list_forall2 match_stackframes stk stk' ->
(* s_istate_simu f dupmap st st' -> *)
sfval_simu dm f st.(si_pc) st'.(si_pc) (mkctx sp rs0 m0 LIVE) sv sv' ->
ssem_final pge ge sp st.(si_pc) stk f rs0 m0 sv rs m t s ->
exists s', ssem_final tpge tge sp st'.(si_pc) stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
Proof.
Local Hint Resolve transf_fundef_correct: core.
intros FUN STK (* SIS *) SFV. destruct SFV; intros SEM; inv SEM; simpl in *.
intros FUN STK SFV. destruct SFV; intros SEM; inv SEM; simpl in *.
- (* Snone *)
exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
intros (path & PATH).
......@@ -253,18 +252,29 @@ Proof.
+ rewrite <- H. erewrite <- seval_preserved; eauto.
Qed.
Lemma pre_output_regs_correct f pc0 path0 stk sp (st:sstate) rs0 m0 t s' rs m rs':
(liveness_ok_function f) ->
(fn_path f) ! pc0 = Some path0 ->
path_step ge pge (psize path0) stk f sp rs0 m0 pc0 t s' ->
ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs m t s' ->
eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) rs rs' ->
ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' m t s'.
Admitted.
(* The main theorem on simulation of symbolic states ! *)
Theorem ssem_sstate_simu dm f f' stk stk' sp st st' rs m t s:
Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
(fn_path f) ! pc0 = Some path0 ->
path_step ge pge (psize path0) stk f sp rs m pc0 t s ->
match_function dm f f' ->
liveness_ok_function f ->
list_forall2 match_stackframes stk stk' ->
ssem pge ge sp st stk f rs m t s ->
(forall ctx: simu_proof_context f, sstate_simu dm f st st' ctx) ->
(forall ctx: simu_proof_context f, sstate_simu dm f (pre_output_regs path0) st st' ctx) ->
exists s', ssem tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
Proof.
intros MFUNC LIVE STACKS SEM SIMU.
intros PATH0 STEP MFUNC LIVE STACKS SEM SIMU.
destruct (SIMU (mkctx sp rs m LIVE)) as (SIMU1 & SIMU2); clear SIMU.
destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl.
destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl in *.
- (* sem_early *)
exploit sistate_simu; eauto.
unfold istate_simu; rewrite CONT.
......@@ -277,7 +287,9 @@ Proof.
exploit sistate_simu; eauto.
unfold istate_simu; rewrite CONT.
intros (is' & SEM' & (CONT' & RS' & M')(* & DMEQ *)).
rewrite <- eqlive_reg_triv in RS'.
exploit pre_output_regs_correct; eauto.
clear SEM2; intros SEM2.
(* exploit SIMU2; eauto. *)
exploit ssem_final_simu; eauto.
clear SEM2; intros (s0 & SEM2 & MATCH0).
exploit ssem_final_equiv; eauto.
......@@ -301,12 +313,13 @@ Proof.
intros (path' & PATH').
exists path'.
exploit (sexec_correct f pc pge ge sp path stk rs m t s); eauto.
intros (st & SYMB & SEM); clear STEP.
intros (st & SYMB & SEM).
exploit dupmap_correct; eauto.
clear SYMB; intros (st' & SYMB & SIMU).
clear SYMB; intros (path0 & st' & PATH0 & SYMB & SIMU).
rewrite PATH0 in PATH; inversion PATH; subst.
exploit ssem_sstate_simu; eauto.
intros (s0 & SEM0 & MATCH).
exploit sexec_exact; eauto.
exploit (sexec_exact f'); eauto.
intros (s' & STEP' & EQ).
exists s'; intuition.
eapply match_states_equiv; eauto.
......