diff options
Diffstat (limited to 'cparser/validator/Interpreter_safe.v')
| -rw-r--r-- | cparser/validator/Interpreter_safe.v | 275 |
1 files changed, 275 insertions, 0 deletions
diff --git a/cparser/validator/Interpreter_safe.v b/cparser/validator/Interpreter_safe.v new file mode 100644 index 0000000..f094ddc --- /dev/null +++ b/cparser/validator/Interpreter_safe.v @@ -0,0 +1,275 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Streams. +Require Import Equality. +Require Import List. +Require Import Syntax. +Require Import Alphabet. +Require Grammar. +Require Automaton. +Require Validator_safe. +Require Interpreter. + +Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A). +Module Import Valid := Validator_safe.Make A. + +(** * A correct automaton does not crash **) + +Section Safety_proof. + +Hypothesis safe: safe. + +Proposition shift_head_symbs: shift_head_symbs. +Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. +Proposition goto_head_symbs: goto_head_symbs. +Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. +Proposition shift_past_state: shift_past_state. +Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. +Proposition goto_past_state: goto_past_state. +Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. +Proposition reduce_ok: reduce_ok. +Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. + +(** We prove that a correct automaton won't crash : the interpreter will + not return [Err] **) + +Variable init : initstate. + +(** The stack of states of an automaton stack **) +Definition state_stack_of_stack (stack:stack) := + (List.map + (fun cell:sigT noninitstate_type => singleton_state_pred (projT1 cell)) + stack ++ [singleton_state_pred init])%list. + +(** The stack of symbols of an automaton stack **) +Definition symb_stack_of_stack (stack:stack) := + List.map + (fun cell:sigT noninitstate_type => last_symb_of_non_init_state (projT1 cell)) + stack. + +(** The stack invariant : it basically states that the assumptions on the + states are true. **) +Inductive stack_invariant: stack -> Prop := + | stack_invariant_constr: + forall stack, + prefix (head_symbs_of_state (state_of_stack init stack)) + (symb_stack_of_stack stack) -> + prefix_pred (head_states_of_state (state_of_stack init stack)) + (state_stack_of_stack stack) -> + stack_invariant_rec stack -> + stack_invariant stack +with stack_invariant_rec: stack -> Prop := + | stack_invariant_rec_nil: + stack_invariant_rec [] + | stack_invariant_rec_cons: + forall state_cur st stack_rec, + stack_invariant stack_rec -> + stack_invariant_rec (existT _ state_cur st::stack_rec). + +(** [pop] conserves the stack invariant and does not crash + under the assumption that we can pop at this place. + Moreover, after a pop, the top state of the stack is allowed. **) +Lemma pop_stack_invariant_conserved + (symbols_to_pop:list symbol) (stack_cur:stack) A action: + stack_invariant stack_cur -> + prefix symbols_to_pop (head_symbs_of_state (state_of_stack init stack_cur)) -> + match pop symbols_to_pop stack_cur (A:=A) action with + | OK (stack_new, _) => + stack_invariant stack_new /\ + state_valid_after_pop + (state_of_stack init stack_new) symbols_to_pop + (head_states_of_state (state_of_stack init stack_cur)) + | Err => False + end. +Proof with eauto. + intros. + pose proof H. + destruct H. + revert H H0 H1 H2 H3. + generalize (head_symbs_of_state (state_of_stack init stack0)). + generalize (head_states_of_state (state_of_stack init stack0)). + revert stack0 A action. + induction symbols_to_pop; intros. + - split... + destruct l; constructor. + inversion H2; subst. + specialize (H7 (state_of_stack init stack0)). + destruct (f2 (state_of_stack init stack0)) as [] eqn:? ... + destruct stack0 as [|[]]; simpl in *. + + inversion H6; subst. + unfold singleton_state_pred in Heqb0. + now rewrite compare_refl in Heqb0; discriminate. + + inversion H6; subst. + unfold singleton_state_pred in Heqb0. + now rewrite compare_refl in Heqb0; discriminate. + - destruct stack0 as [|[]]; unfold pop. + + inversion H0; subst. + now inversion H. + + fold pop. + destruct (compare_eqdec (last_symb_of_non_init_state x) a). + * inversion H0; subst. clear H0. + inversion H; subst. clear H. + dependent destruction H3; simpl. + assert (prefix_pred (List.tl l) (state_stack_of_stack stack0)). + unfold tl; destruct l; [constructor | inversion H2]... + pose proof H. destruct H3. + specialize (IHsymbols_to_pop stack0 A (action0 n) _ _ H4 H7 H H0 H6). + revert IHsymbols_to_pop. + fold (noninitstate_type x); generalize (pop symbols_to_pop stack0 (action0 n)). + destruct r as [|[]]; intuition... + destruct l; constructor... + * apply n0. + inversion H0; subst. + inversion H; subst... +Qed. + +(** [prefix] is associative **) +Lemma prefix_ass: + forall (l1 l2 l3:list symbol), prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3. +Proof. +induction l1; intros. +constructor. +inversion H; subst. +inversion H0; subst. +constructor; eauto. +Qed. + +(** [prefix_pred] is associative **) +Lemma prefix_pred_ass: + forall (l1 l2 l3:list (state->bool)), + prefix_pred l1 l2 -> prefix_pred l2 l3 -> prefix_pred l1 l3. +Proof. +induction l1; intros. +constructor. +inversion H; subst. +inversion H0; subst. +constructor; eauto. +intro. +specialize (H3 x). +specialize (H4 x). +destruct (f0 x); simpl in *; intuition. +rewrite H4 in H3; intuition. +Qed. + +(** If we have the right to reduce at this state, then the stack invariant + is conserved by [reduce_step] and [reduce_step] does not crash. **) +Lemma reduce_step_stack_invariant_conserved stack prod buff: + stack_invariant stack -> + valid_for_reduce (state_of_stack init stack) prod -> + match reduce_step init stack prod buff with + | OK (Fail_sr | Accept_sr _ _) => True + | OK (Progress_sr stack_new _) => stack_invariant stack_new + | Err => False + end. +Proof with eauto. +unfold valid_for_reduce. +intuition. +unfold reduce_step. +pose proof (pop_stack_invariant_conserved (prod_rhs_rev prod) stack _ (prod_action' prod)). +destruct (pop (prod_rhs_rev prod) stack (prod_action' prod)) as [|[]]. +apply H0... +destruct H0... +pose proof (goto_head_symbs (state_of_stack init s) (prod_lhs prod)). +pose proof (goto_past_state (state_of_stack init s) (prod_lhs prod)). +unfold bind2. +destruct H0. +specialize (H2 _ H3)... +destruct (goto_table (state_of_stack init stack0) (prod_lhs prod)) as [[]|]. +constructor. +simpl. +constructor. +eapply prefix_ass... +unfold state_stack_of_stack; simpl; constructor. +intro; destruct (singleton_state_pred x x0); reflexivity. +eapply prefix_pred_ass... +constructor... +constructor... +destruct stack0 as [|[]]... +destruct (compare_eqdec (prod_lhs prod) (start_nt init))... +apply n, H2, eq_refl. +apply H2, eq_refl. +Qed. + +(** If the automaton is safe, then the stack invariant is conserved by + [step] and [step] does not crash. **) +Lemma step_stack_invariant_conserved (stack:stack) buffer: + stack_invariant stack -> + match step init stack buffer with + | OK (Fail_sr | Accept_sr _ _) => True + | OK (Progress_sr stack_new _) => stack_invariant stack_new + | Err => False + end. +Proof with eauto. +intro. +unfold step. +pose proof (shift_head_symbs (state_of_stack init stack)). +pose proof (shift_past_state (state_of_stack init stack)). +pose proof (reduce_ok (state_of_stack init stack)). +destruct (action_table (state_of_stack init stack)). +apply reduce_step_stack_invariant_conserved... +destruct buffer as [[]]; simpl. +specialize (H0 x); specialize (H1 x); specialize (H2 x). +destruct (l x)... +destruct H. +constructor. +unfold state_of_stack. +constructor. +eapply prefix_ass... +unfold state_stack_of_stack; simpl; constructor. +intro; destruct (singleton_state_pred s0 x0)... +eapply prefix_pred_ass... +constructor... +constructor... +apply reduce_step_stack_invariant_conserved... +Qed. + +(** If the automaton is safe, then it does not crash **) +Theorem parse_no_err buffer n_steps: + parse init buffer n_steps <> Err. +Proof with eauto. +unfold parse. +assert (stack_invariant []). +constructor. +constructor. +unfold state_stack_of_stack; simpl; constructor. +intro; destruct (singleton_state_pred init x)... +constructor. +constructor. +revert H. +generalize buffer ([]:stack). +induction n_steps; simpl. +now discriminate. +intros. +pose proof (step_stack_invariant_conserved s buffer0 H). +destruct (step init s buffer0) as [|[]]; simpl... +discriminate. +discriminate. +Qed. + +(** A version of [parse] that uses safeness in order to return a + [parse_result], and not a [result parse_result] : we have proven that + parsing does not return [Err]. **) +Definition parse_with_safe (buffer:Stream token) (n_steps:nat): + parse_result init. +Proof with eauto. +pose proof (parse_no_err buffer n_steps). +destruct (parse init buffer n_steps)... +congruence. +Defined. + +End Safety_proof. + +End Make. |