Merge branch 'CompCert_RTLpath_simuX' into kvx-work

Makefile

@@ -140,7 +140,7 @@ SCHEDULING= \
   RTLpathLivegen.v         RTLpathSE_impl.v \
   RTLpathproof.v           RTLpathSE_theory.v \
   RTLpathSchedulerproof.v  RTLpath.v \
-  RTLpathScheduler.v
+  RTLpathScheduler.v       RTLpathWFcheck.v
 
 # C front-end modules (in cfrontend/)
 

scheduling/RTLpathScheduler.v

@@ -7,7 +7,7 @@ This module is inspired from [Duplicate] and [Duplicateproof]
 Require Import AST Linking Values Maps Globalenvs Smallstep Registers.
 Require Import Coqlib Maps Events Errors Op.
 Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory RTLpathSE_impl.
-
+Require RTLpathWFcheck.
 
 Notation "'ASSERT' A 'WITH' MSG 'IN' B" := (if A then B else Error (msg MSG))
          (at level 200, A at level 100, B at level 200)
@@ -32,14 +32,14 @@ Extract Constant untrusted_scheduler => "RTLpathScheduleraux.scheduler".
 
 Program Definition function_builder (tfr: RTL.function) (tpm: path_map) : 
   { r : res RTLpath.function | forall f', r = OK f' -> fn_RTL f' = tfr} :=
-  match RTLpathLivegen.function_checker tfr tpm with
+  match RTLpathWFcheck.function_checker tfr tpm with
   | false => Error (msg "In function_builder: (tfr, tpm) is not wellformed")
   | true => OK {| fn_RTL := tfr; fn_path := tpm |}
   end.
 Next Obligation.
-  apply function_checker_path_entry. auto.
+  apply RTLpathWFcheck.function_checker_path_entry. auto.
 Defined. Next Obligation.
-  apply function_checker_wellformed_path_map. auto.
+  apply RTLpathWFcheck.function_checker_wellformed_path_map. auto.
 Defined.
 
 Definition entrypoint_check (dm: PTree.t node) (fr tfr: RTL.function) : res unit :=

scheduling/RTLpathWFcheck.v

+Require Import Coqlib.
+Require Import Maps.
+Require Import Lattice.
+Require Import AST.
+Require Import Op.
+Require Import Registers.
+Require Import Globalenvs Smallstep RTL RTLpath.
+Require Import Bool Errors.
+Require Import Program.
+Require RTLpathLivegen.
+
+Local Open Scope lazy_bool_scope.
+
+Local Open Scope option_monad_scope.
+
+Definition exit_checker {A} (pm: path_map) (pc: node) (v:A): option A :=
+   SOME path <- pm!pc IN
+   Some v.
+
+Lemma exit_checker_path_entry A (pm: path_map) (pc: node) (v:A) res:
+  exit_checker pm pc v = Some res -> path_entry pm pc.
+Proof.
+  unfold exit_checker, path_entry.
+  inversion_SOME path; simpl; congruence.
+Qed.
+
+Lemma exit_checker_res A (pm: path_map) (pc: node) (v:A) res:
+  exit_checker pm pc v = Some res -> v=res.
+Proof.
+  unfold exit_checker, path_entry.
+  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 ? *)
+  end.
+
+Local Hint Resolve exit_checker_path_entry: core.
+
+Lemma iinst_checker_path_entry (pm: path_map) (i: instruction) res pc:
+  iinst_checker pm i = Some res -> 
+  early_exit i = Some pc -> path_entry pm pc.
+Proof.
+  destruct i; simpl; try_simplify_someHyps; subst.
+Qed.
+
+Lemma iinst_checker_default_succ (pm: path_map) (i: instruction) res pc:
+  iinst_checker pm i = Some res -> 
+  pc = res ->
+  default_succ i = Some pc.
+Proof.
+  destruct i; simpl; try_simplify_someHyps; subst;
+  repeat (inversion_ASSERT); try_simplify_someHyps.
+  intros; exploit exit_checker_res; eauto.
+  intros; subst. simpl; auto.
+Qed.
+
+Fixpoint ipath_checker (ps:nat) (f: RTL.function) (pm: path_map) (pc:node): option (node) :=
+  match ps with
+  | O => Some (pc)
+  | S p =>
+    SOME i <- f.(fn_code)!pc IN
+    SOME res <- iinst_checker pm i IN
+    ipath_checker p f pm res
+  end.
+
+Lemma ipath_checker_wellformed f pm ps: forall pc res,
+   ipath_checker ps f pm pc = Some res -> 
+   wellformed_path f.(fn_code) pm 0 res ->
+   wellformed_path f.(fn_code) pm ps pc.
+Proof.
+  induction ps; simpl; try_simplify_someHyps.
+  inversion_SOME i; inversion_SOME res'.
+  intros. eapply wf_internal_node; eauto.
+  * eapply iinst_checker_default_succ; eauto.
+  * intros; eapply iinst_checker_path_entry; eauto.
+Qed.
+
+Fixpoint exit_list_checker (pm: path_map) (l: list node): bool :=
+   match l with
+   | nil => true
+   | pc::l' => exit_checker pm pc tt &&& exit_list_checker pm l'
+   end.
+
+Lemma exit_list_checker_correct pm l pc:
+  exit_list_checker pm l = true -> List.In pc l -> exit_checker pm pc tt = Some tt.
+Proof.
+  intros EXIT PC; induction l; intuition.
+  simpl in * |-. rewrite RTLpathLivegen.lazy_and_Some_tt_true in EXIT.
+  firstorder (subst; eauto).
+Qed.
+
+Local Hint Resolve exit_list_checker_correct: core.
+
+Definition inst_checker (pm: path_map) (i: instruction): option unit :=
+   match i with
+   | Icall sig ros args res pc' =>
+      exit_checker pm pc' tt
+   | Itailcall sig ros args =>
+      Some tt
+   | Ibuiltin ef args res pc' =>
+      exit_checker pm pc' tt
+   | Ijumptable arg tbl =>
+      ASSERT exit_list_checker pm tbl IN
+      Some tt
+   | Ireturn optarg =>
+      Some tt
+   | _ => 
+      SOME res <- iinst_checker pm i IN
+      exit_checker pm res tt
+   end.
+
+Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (i: instruction):
+  inst_checker pm i = Some tt ->
+  c!pc = Some i -> wellformed_path c pm 0 pc.
+Proof.
+  intros CHECK PC. eapply wf_last_node; eauto.
+  clear c pc PC. intros pc PC.
+  destruct i; simpl in * |- *; intuition (subst; eauto);
+  try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
+  intros X; exploit exit_checker_res; eauto.
+  clear X. intros; subst; eauto.
+Qed.
+
+Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
+   SOME res <- ipath_checker (path.(psize)) f pm pc  IN
+   SOME i <- f.(fn_code)!res IN
+   inst_checker pm i.
+
+Lemma path_checker_wellformed f pm pc path:
+   path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.
+Proof.
+  unfold path_checker.
+  inversion_SOME res.
+  inversion_SOME i.
+  intros; eapply ipath_checker_wellformed; eauto.
+  eapply inst_checker_wellformed; eauto.
+Qed.
+
+Fixpoint list_path_checker f pm (l:list (node*path_info)): bool :=
+  match l with
+  | nil => true
+  | (pc, path)::l' =>
+      path_checker f pm pc path &&& list_path_checker f pm l'
+  end.
+
+Lemma list_path_checker_correct f pm l: 
+  list_path_checker f pm l = true -> forall e, List.In e l -> path_checker f pm (fst e) (snd e) = Some tt.
+Proof.
+  intros CHECKER e H; induction l as [|(pc & path) l]; intuition.
+  simpl in * |- *. rewrite RTLpathLivegen.lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
+Qed.
+
+Definition function_checker (f: RTL.function) (pm: path_map): bool := 
+  pm!(f.(fn_entrypoint)) &&& list_path_checker f pm (PTree.elements pm).
+
+Lemma function_checker_correct f pm pc path: 
+  function_checker f pm = true -> 
+  pm!pc = Some path -> 
+  path_checker f pm pc path = Some tt.
+Proof.
+  unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true.
+  intros (ENTRY & PATH) PC.
+  exploit list_path_checker_correct; eauto.
+  - eapply PTree.elements_correct; eauto.
+  - simpl; auto.
+Qed.
+
+Lemma function_checker_wellformed_path_map f pm:
+  function_checker f pm = true -> wellformed_path_map f.(fn_code) pm.
+Proof.
+  unfold wellformed_path_map.
+  intros; eapply path_checker_wellformed; eauto.
+  intros; eapply function_checker_correct; eauto.
+Qed.
+
+Lemma function_checker_path_entry f pm:
+  function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)).
+Proof.
+  unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true;
+  unfold path_entry. firstorder congruence.
+Qed.