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

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

parents 3ce99d1f 91699fd3
......@@ -133,6 +133,7 @@ BACKEND=\
Mach.v \
Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
Asm.v Asmgen.v Asmgenproof.v Asmaux.v \
RTLpathSE_simplify.v \
$(BACKENDLIB)
SCHEDULING= \
......
......@@ -201,7 +201,7 @@ Inductive instruction: Type :=
| Pstrx_a (rs: ireg) (a: addressing) (**r store int64 as any64 *)
| Pstrb (rs: ireg) (a: addressing) (**r store int8 *)
| Pstrh (rs: ireg) (a: addressing) (**r store int16 *)
| Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *)
| Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int32 *)
| Pstpx (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *)
(** Integer arithmetic, immediate *)
| Paddimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z) (**r addition *)
......
Require Import Op Registers.
Require Import RTLpathSE_theory.
Require Import RTLpathSE_simu_specs.
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.
......@@ -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.
......
......@@ -229,12 +229,14 @@ let get_outputs liveness f n pi =
fun n -> get_some @@ PTree.get n liveness
) path_last_successors in
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 por = match last_instruction with (* see RTLpathLivegen.final_inst_checker *)
| Icall (_, _, _, res, _) -> Regset.remove res outputs
| Ibuiltin (_, _, res, _) -> Liveness.reg_list_dead (AST.params_of_builtin_res res) outputs
| Itailcall (_, _, _) | Ireturn _ ->
assert (outputs = Regset.empty); (* defensive check for performance *)
outputs
| _ -> outputs
in (por, outputs)
let set_pathmap_liveness f pm =
let liveness = analyze f in
......@@ -245,13 +247,12 @@ let set_pathmap_liveness f pm =
let inputs = get_some @@ PTree.get n liveness in
let (por, outputs) = get_outputs liveness f n pi in
new_pm := PTree.set n
{psize=pi.psize; input_regs=inputs; pre_output_regs=por; output_regs=outputs} !new_pm (* FIXME: STUB *)
{psize=pi.psize; input_regs=inputs; pre_output_regs=por; output_regs=outputs} !new_pm
) (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 "\ninput_regs=";
print_regset pi.input_regs;
......@@ -260,7 +261,6 @@ let print_path_info pi = begin
debug "\n; output_regs=";
print_regset pi.output_regs;
debug ")\n"
(*debug_flag := false*)
end
let print_path_map path_map = begin
......
......@@ -8,6 +8,7 @@ Require Import Errors.
Require Import RTLpathSE_theory RTLpathLivegenproof.
Require Import Axioms RTLpathSE_simu_specs.
Require Import Asmgen Asmgenproof1.
Require Import Axioms RTLpathSE_simu_specs RTLpathSE_simplify.
Local Open Scope error_monad_scope.
Local Open Scope option_monad_scope.
......@@ -431,6 +432,113 @@ 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 *)
(* END "fake" hsval ... *)
(** Convert a "fake" hash-consed term into a "real" hash-consed term *)
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.
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;
......@@ -854,8 +962,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
| Rop ((Ocmp cond) as op) =>
match cond, lr with
......@@ -1803,29 +1915,22 @@ Lemma simplify_correct rsv lr hst:
sval_refines ge sp rs0 m0 hv (rsv lr st).
Proof.
destruct rsv; simpl; auto.
- destruct op eqn:EQOP; try apply simplify_nothing.
{ 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.
+ apply simplify_nothing. }
{ destruct cond; repeat (destruct lr; try apply simplify_nothing).
+ apply simplify_ccomp_correct.
+ apply simplify_ccompu_correct.
+ admit.
+ admit.
+ apply simplify_ccompl_correct.
+ apply simplify_ccomplu_correct.
+ admit.
+ admit.
+ apply simplify_ccompf_correct.
+ apply simplify_cnotcompf_correct.
+ apply simplify_ccompfs_correct.
+ apply simplify_cnotcompfs_correct. }
- (* Rop *)
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. }
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.
......@@ -2104,6 +2209,48 @@ Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list
(** ** 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' =>
......@@ -2123,10 +2270,9 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) :
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 (* TODO jumptable ? *)
| _ => 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.
......
......@@ -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