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

6 files changed, 202 insertions, 79 deletions

diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v
index 7855d375..9f646ad0 100644
--- a/scheduling/RTLpathLivegen.v
+++ b/scheduling/RTLpathLivegen.v
@@ -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.
 
diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index db3fc9d4..9b93bc32 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -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
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index bce428e3..e39e21f0 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -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.
diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v
index eec0bc51..aa8db342 100644
--- a/scheduling/RTLpathSE_theory.v
+++ b/scheduling/RTLpathSE_theory.v
@@ -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: 
diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v
index 72a4ee01..a9c2fa76 100644
--- a/scheduling/RTLpathSchedulerproof.v
+++ b/scheduling/RTLpathSchedulerproof.v
@@ -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 *)
diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v
index 0ddc3142..63b914ec 100644
--- a/scheduling/RTLpathWFcheck.v
+++ b/scheduling/RTLpathWFcheck.v
@@ -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.