Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

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

a bit more cleaning

parent 8faafc76
......@@ -46,7 +46,6 @@ Proof.
inversion_ASSERT; try_simplify_someHyps.
Qed.
(* FIXME - what about trap? *)
Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option (Regset.t * node) :=
match i with
| Inop pc' => Some (alive, pc')
......@@ -63,7 +62,7 @@ Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): opti
| Icond cond args ifso ifnot _ =>
ASSERT list_mem args alive IN
exit_checker pm alive ifso (alive, ifnot)
| _ => None (* TODO jumptable ? *)
| _ => None
end.
......@@ -109,6 +108,20 @@ Proof.
* intros; eapply iinst_checker_path_entry; eauto.
Qed.
Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res,
ipath_checker path f (fn_path f) alive pc = Some res
-> nth_default_succ (fn_code f) path pc = Some (snd res).
Proof.
induction path; simpl.
+ try_simplify_someHyps.
+ intros alive pc res.
inversion_SOME i; intros INST.
inversion_SOME res0; intros ICHK IPCHK.
rewrite INST.
erewrite iinst_checker_default_succ; eauto.
Qed.
Definition reg_option_mem (or: option reg) (alive: Regset.t) :=
match or with None => true | Some r => Regset.mem r alive end.
......
......@@ -764,7 +764,7 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) :
DO vargs <~ hlist_args prev args ;;
let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in
RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |})
| _ => RET None (* TODO jumptable ? *)
| _ => RET None
end.
......
......@@ -345,31 +345,13 @@ Qed.
Lemma ssem_local_exclude_sabort_local ge sp loc rs m rs' m':
ssem_local ge sp loc rs m rs' m' ->
(* all_fallthrough ge sp (si_exits st) rs m -> *)
sabort_local ge sp loc rs m ->
False.
Proof.
intros SIML (* ALLF *) ABORT. inv SIML. destruct H0 as (H0 & H0').
intros SIML ABORT. inv SIML. destruct H0 as (H0 & H0').
inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
Qed.
(* TODO: remove this JUNK ?
Lemma ssem_local_exclude_sabort_exit ge sp st ext lx rs m rs' m':
ssem_local ge sp (si_local st) rs m rs' m' ->
all_fallthrough ge sp (si_exits st) rs m ->
is_tail (ext :: lx) (si_exits st) ->
sabort_exit ge sp ext rs m ->
False.
Proof.
intros SSEML ALLF TAIL ABORT.
inv ABORT.
- exploit ALLF; eauto. congruence.
- (* FIXME Problem : if we have a ssem_local, this means we ONLY evaluated the conditions,
but we NEVER actually evaluated the si_elocal from the sistate_exit ! So we cannot prove
a lack of abort on the si_elocal.. We must change the definitions *)
Abort.
*)
Lemma ssem_local_exclude_sabort ge sp st rs m rs' m':
ssem_local ge sp (si_local st) rs m rs' m' ->
all_fallthrough ge sp (si_exits st) rs m ->
......@@ -497,7 +479,7 @@ Definition siexec_inst (i: instruction) (st: sistate): option sistate :=
let vargs := list_sval_inj (List.map prev.(si_sreg) args) in
let ex := {| si_cond:=cond; si_scondargs:=vargs; si_elocal := prev; si_ifso := ifso |} in
Some {| si_pc := ifnot; si_exits := ex::st.(si_exits); si_local := prev |}
| _ => None (* TODO jumptable ? *)
| _ => None
end.
Lemma seval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs:
......
......@@ -260,19 +260,6 @@ Proof.
+ rewrite <- H. erewrite <- seval_preserved; eauto.
Qed.
Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res,
ipath_checker path f (fn_path f) alive pc = Some res
-> nth_default_succ (fn_code f) path pc = Some (snd res).
Proof.
induction path; simpl.
+ try_simplify_someHyps.
+ intros alive pc res.
inversion_SOME i; intros INST.
inversion_SOME res0; intros ICHK IPCHK.
rewrite INST.
erewrite iinst_checker_default_succ; eauto.
Qed.
Lemma siexec_snone_por_correct rs' is t s alive path0 i sp s0 st0 stk stk' f rs0 m0: forall
(SSEM2 : ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone
(irs is) (imem is) t s)
......@@ -331,17 +318,14 @@ Qed.
Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs':
(liveness_ok_function f) ->
(fn_path f) ! pc0 = Some path0 ->
(* path_step ge pge path0.(psize) stk f sp rs0 m0 pc0 t s -> *) (* NB: should be useless *)
sexec f pc0 = Some st ->
(* icontinue is = true -> *)
list_forall2 match_stackframes stk stk' ->
(* ssem_internal ge sp st rs0 m0 is -> *)
ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) (irs is) (imem is) t s ->
eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
exists s', ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' (imem is) t s' /\ eqlive_states s s'.
Proof.
Local Hint Resolve eqlive_stacks_refl: core.
intros LIVE PATH0 (*PSTEP*) SEXEC (*CONT*) STK (*SSEM1*) SSEM2 EQLIVE.
intros LIVE PATH0 SEXEC STK SSEM2 EQLIVE.
(* start decomposing path_checker *)
generalize (LIVE pc0 path0 PATH0).
unfold path_checker.
......@@ -413,7 +397,6 @@ Qed.
(* The main theorem on simulation of symbolic states ! *)
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 -> *)
sexec f pc0 = Some st ->
match_function dm f f' ->
liveness_ok_function f ->
......@@ -422,7 +405,7 @@ Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
(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 PATH0 (*STEP*) SEXEC MFUNC LIVE STACKS SEM SIMU.
intros PATH0 SEXEC 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 in *.
- (* sem_early *)
......
......@@ -31,14 +31,13 @@ Proof.
inversion_SOME path; try_simplify_someHyps.
Qed.
(* FIXME - what about trap? *)
Definition iinst_checker (pm: path_map) (i: instruction): option (node) :=
match i with
| Inop pc' | Iop _ _ _ pc' | Iload _ _ _ _ _ pc'
| Istore _ _ _ _ pc' => Some (pc')
| Icond cond args ifso ifnot _ =>
exit_checker pm ifso ifnot
| _ => None (* TODO jumptable ? *)
| _ => None
end.
Local Hint Resolve exit_checker_path_entry: core.
......
Markdown is supported
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