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 91699fd3 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Merge branch 'riscv-work-rules' of...

Merge branch 'riscv-work-rules' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into riscv-work-rules
parents 4192b5f4 997d7f1a
......@@ -529,6 +529,14 @@ Admitted.
Global Opaque fsval_proj.
Local Hint Resolve fsval_proj_correct: wlp.
Lemma fsval_list_proj_correct lhsv:
WHEN fsval_list_proj lhsv ~> lhsv' THEN forall ge sp rs0 m0,
seval_list_hsval ge sp lhsv rs0 m0 = seval_list_hsval ge sp lhsv' rs0 m0.
Admitted.
Global Opaque fsval_list_proj.
Local Hint Resolve fsval_list_proj_correct: wlp.
(** ** Assignment of memory *)
Definition hslocal_set_smem (hst:hsistate_local) hm :=
{| hsi_smem := hm;
......@@ -853,6 +861,48 @@ Local Hint Resolve hslocal_set_sreg_correct: wlp.
(** ** Execution of one instruction *)
(* TODO: This function could be defined in a specific file for each target *)
Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
None.
Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
(TARGET: target_cbranch_expanse hst c l = Some (c', l'))
(LREF : hsilocal_refines ge sp rs0 m0 hst st)
(OK: hsok_local ge sp rs0 m0 hst),
seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
Proof.
unfold target_cbranch_expanse; simpl; intros; try congruence.
Qed.
Global Opaque target_cbranch_expanse.
Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) :=
match target_cbranch_expanse prev cond args with
| Some (cond', vargs) =>
DO vargs' <~ fsval_list_proj vargs;;
RET (cond', vargs)
| None =>
DO vargs <~ hlist_args prev args ;;
RET (cond, vargs)
end.
Lemma cbranch_expanse_correct hst c l:
WHEN cbranch_expanse hst c l ~> r THEN forall ge sp rs0 m0 st
(LREF : hsilocal_refines ge sp rs0 m0 hst st)
(OK: hsok_local ge sp rs0 m0 hst),
seval_condition ge sp (fst r) (hsval_list_proj (snd r)) (si_smem st) rs0 m0 =
seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
Proof.
unfold cbranch_expanse.
destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify.
+ destruct p as [c' l']; simpl.
exploit target_cbranch_expanse_correct; eauto.
+ unfold seval_condition; erewrite H; eauto.
Qed.
Local Hint Resolve cbranch_expanse_correct: wlp.
Global Opaque cbranch_expanse.
Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) :=
match i with
| Inop pc' =>
......@@ -868,13 +918,13 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) :
RET (Some (hsist_set_local hst pc' next))
| Icond cond args ifso ifnot _ =>
let prev := hst.(hsi_local) in
DO vargs <~ hlist_args prev args ;;
DO res <~ cbranch_expanse prev cond args;;
let (cond, vargs) := res in
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
end.
Remark hsiexec_inst_None_correct i hst:
WHEN hsiexec_inst i hst ~> o THEN forall st, o = None -> siexec_inst i st = None.
Proof.
......
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