Checker for wellformed path

scheduling/RTLpathWFcheck.v

@@ -13,12 +13,185 @@ 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 lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true.
+Proof.
+  destruct o; simpl; intuition. 
+  - eauto.
+  - firstorder. try_simplify_someHyps.
+Qed.
+
+Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true.
+Proof.
+   intros; rewrite lazy_and_Some_true; firstorder.
+   destruct x; auto.
+Qed.
+
+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 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 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)) &&& true. (* TODO: &&& list_path_checker f pm (PTree.elements pm) *)
+  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 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.
-Admitted.
+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)).