diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Deadcodeproof.v | 7 | ||||
-rw-r--r-- | backend/Inliningspec.v | 4 | ||||
-rw-r--r-- | backend/Kildall.v | 56 | ||||
-rw-r--r-- | backend/Selectionproof.v | 4 | ||||
-rw-r--r-- | backend/Stackingproof.v | 2 | ||||
-rw-r--r-- | backend/ValueDomain.v | 2 |
6 files changed, 36 insertions, 39 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 26953479..a8d79c3f 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -168,8 +168,7 @@ Proof. + subst b0. apply SETN with (access := fun ofs => Mem.perm m1' b ofs Cur Readable /\ Q b ofs); auto. intros. destruct H5. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. - apply H1; auto. -+ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. apply H1; auto. ++ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. - rewrite (Mem.nextblock_storebytes _ _ _ _ _ H0). rewrite (Mem.nextblock_storebytes _ _ _ _ _ ST2). eapply ma_nextblock; eauto. @@ -551,7 +550,7 @@ Proof. intros. exploit analyze_successors; eauto. rewrite ANPC; simpl. intros [A B]. econstructor; eauto. eapply eagree_ge; eauto. - eapply magree_monotone; eauto. intros; apply B; auto. + eapply magree_monotone; eauto. Qed. (** Builtin arguments and results *) @@ -1134,5 +1133,3 @@ Proof. Qed. End PRESERVATION. - - diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 23770cb7..f56d6d18 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -512,7 +512,7 @@ Proof. assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega. omega. intros. simpl in H. rewrite S1. - transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. + transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; xomega. eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. red; simpl. subst s2; simpl in *. xomega. red; simpl. split. auto. apply align_le. apply min_alignment_pos. @@ -542,7 +542,7 @@ Proof. assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega. omega. intros. simpl in H. rewrite S1. - transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. + transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. red; simpl. subst s2; simpl in *; xomega. diff --git a/backend/Kildall.v b/backend/Kildall.v index 87090f5d..a2b49d56 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -74,7 +74,7 @@ Module Type DATAFLOW_SOLVER. point. [transf] is the transfer function, [ep] the entry point, and [ev] the minimal abstract value for [ep]. *) - Variable fixpoint: + Parameter fixpoint: forall {A: Type} (code: PTree.t A) (successors: A -> list positive) (transf: positive -> L.t -> L.t) (ep: positive) (ev: L.t), @@ -83,7 +83,7 @@ Module Type DATAFLOW_SOLVER. (** The [fixpoint_solution] theorem shows that the returned solution, if any, satisfies the dataflow inequations. *) - Hypothesis fixpoint_solution: + Axiom fixpoint_solution: forall A (code: PTree.t A) successors transf ep ev res n instr s, fixpoint code successors transf ep ev = Some res -> code!n = Some instr -> In s (successors instr) -> @@ -93,7 +93,7 @@ Module Type DATAFLOW_SOLVER. (** The [fixpoint_entry] theorem shows that the returned solution, if any, satisfies the additional constraint over the entry point. *) - Hypothesis fixpoint_entry: + Axiom fixpoint_entry: forall A (code: PTree.t A) successors transf ep ev res, fixpoint code successors transf ep ev = Some res -> L.ge res!!ep ev. @@ -102,7 +102,7 @@ Module Type DATAFLOW_SOLVER. and that holds for [L.bot] also holds for the results of the analysis. *) - Hypothesis fixpoint_invariant: + Axiom fixpoint_invariant: forall A (code: PTree.t A) successors transf ep ev (P: L.t -> Prop), P L.bot -> @@ -124,23 +124,23 @@ End DATAFLOW_SOLVER. Module Type NODE_SET. - Variable t: Type. - Variable empty: t. - Variable add: positive -> t -> t. - Variable pick: t -> option (positive * t). - Variable all_nodes: forall {A: Type}, PTree.t A -> t. + Parameter t: Type. + Parameter empty: t. + Parameter add: positive -> t -> t. + Parameter pick: t -> option (positive * t). + Parameter all_nodes: forall {A: Type}, PTree.t A -> t. - Variable In: positive -> t -> Prop. - Hypothesis empty_spec: + Parameter In: positive -> t -> Prop. + Axiom empty_spec: forall n, ~In n empty. - Hypothesis add_spec: + Axiom add_spec: forall n n' s, In n' (add n s) <-> n = n' \/ In n' s. - Hypothesis pick_none: + Axiom pick_none: forall s n, pick s = None -> ~In n s. - Hypothesis pick_some: + Axiom pick_some: forall s n s', pick s = Some(n, s') -> forall n', In n' s <-> n = n' \/ In n' s'. - Hypothesis all_nodes_spec: + Axiom all_nodes_spec: forall A (code: PTree.t A) n instr, code!n = Some instr -> In n (all_nodes code). @@ -900,7 +900,7 @@ Module Type BACKWARD_DATAFLOW_SOLVER. is a finite map returning the list of successors of the given program point. [transf] is the transfer function. *) - Variable fixpoint: + Parameter fixpoint: forall {A: Type} (code: PTree.t A) (successors: A -> list positive) (transf: positive -> L.t -> L.t), option (PMap.t L.t). @@ -908,7 +908,7 @@ Module Type BACKWARD_DATAFLOW_SOLVER. (** The [fixpoint_solution] theorem shows that the returned solution, if any, satisfies the backward dataflow inequations. *) - Hypothesis fixpoint_solution: + Axiom fixpoint_solution: forall A (code: PTree.t A) successors transf res n instr s, fixpoint code successors transf = Some res -> code!n = Some instr -> In s (successors instr) -> @@ -918,12 +918,12 @@ Module Type BACKWARD_DATAFLOW_SOLVER. (** [fixpoint_allnodes] is a variant of [fixpoint], less algorithmically efficient, but correct without any hypothesis on the transfer function. *) - Variable fixpoint_allnodes: + Parameter fixpoint_allnodes: forall {A: Type} (code: PTree.t A) (successors: A -> list positive) (transf: positive -> L.t -> L.t), option (PMap.t L.t). - Hypothesis fixpoint_allnodes_solution: + Axiom fixpoint_allnodes_solution: forall A (code: PTree.t A) successors transf res n instr s, fixpoint_allnodes code successors transf = Some res -> code!n = Some instr -> In s (successors instr) -> @@ -1089,11 +1089,11 @@ End Backward_Dataflow_Solver. Module Type ORDERED_TYPE_WITH_TOP. - Variable t: Type. - Variable ge: t -> t -> Prop. - Variable top: t. - Hypothesis top_ge: forall x, ge top x. - Hypothesis refl_ge: forall x, ge x x. + Parameter t: Type. + Parameter ge: t -> t -> Prop. + Parameter top: t. + Axiom top_ge: forall x, ge top x. + Axiom refl_ge: forall x, ge x x. End ORDERED_TYPE_WITH_TOP. @@ -1105,24 +1105,24 @@ Module Type BBLOCK_SOLVER. Declare Module L: ORDERED_TYPE_WITH_TOP. - Variable fixpoint: + Parameter fixpoint: forall {A: Type} (code: PTree.t A) (successors: A -> list positive) (transf: positive -> L.t -> L.t) (entrypoint: positive), option (PMap.t L.t). - Hypothesis fixpoint_solution: + Axiom fixpoint_solution: forall A (code: PTree.t A) successors transf entrypoint res n instr s, fixpoint code successors transf entrypoint = Some res -> code!n = Some instr -> In s (successors instr) -> L.ge res!!s (transf n res!!n). - Hypothesis fixpoint_entry: + Axiom fixpoint_entry: forall A (code: PTree.t A) successors transf entrypoint res, fixpoint code successors transf entrypoint = Some res -> res!!entrypoint = L.top. - Hypothesis fixpoint_invariant: + Axiom fixpoint_invariant: forall A (code: PTree.t A) successors transf entrypoint (P: L.t -> Prop), P L.top -> diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index aad3add4..a57e5ea6 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -865,9 +865,9 @@ Qed. Remark match_call_cont_cont: forall k k', match_call_cont k k' -> exists cunit hf, match_cont cunit hf k k'. Proof. - intros. refine (let cunit : Cminor.program := _ in _). + intros. simple refine (let cunit : Cminor.program := _ in _). econstructor. apply nil. apply nil. apply xH. - refine (let hf : helper_functions := _ in _). + simple refine (let hf : helper_functions := _ in _). econstructor; apply xH. exists cunit, hf; auto. Qed. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index da024a25..0e9c58b3 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1585,7 +1585,7 @@ Lemma find_function_translated: /\ Genv.find_funct_ptr tge bf = Some tf /\ transf_fundef f = OK tf. Proof. - intros until f; intros AG [bound [_ []]] FF. + intros until f; intros AG [bound [_ [?????]]] FF. destruct ros; simpl in FF. - exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in FF. rewrite Genv.find_funct_find_funct_ptr in FF. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 3c80d733..bc09c3dc 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3739,7 +3739,7 @@ Proof. - (* contents *) intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst. rewrite Zplus_0_r. - set (mv := ZMap.get ofs (Mem.mem_contents m)#b1). + set (mv := ZMap.get ofs (PMap.get b1 (Mem.mem_contents m))). assert (Mem.loadbytes m b1 ofs 1 = Some (mv :: nil)). { Local Transparent Mem.loadbytes. |