diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | backend/Duplicate.v | 240 | ||||
| -rw-r--r-- | backend/Duplicateaux.ml | 13 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 467 | ||||
| -rw-r--r-- | common/AST.v | 19 | ||||
| -rw-r--r-- | driver/Compiler.v | 64 | ||||
| -rw-r--r-- | lib/Floats.v | 63 | ||||
| -rw-r--r-- | lib/Integers.v | 34 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 6 |
9 files changed, 876 insertions, 31 deletions
@@ -80,6 +80,7 @@ BACKEND=\ Tailcall.v Tailcallproof.v \ Inlining.v Inliningspec.v Inliningproof.v \ Renumber.v Renumberproof.v \ + Duplicate.v Duplicateproof.v \ RTLtyping.v \ Kildall.v Liveness.v \ ValueDomain.v ValueAOp.v ValueAnalysis.v \ diff --git a/backend/Duplicate.v b/backend/Duplicate.v new file mode 100644 index 00000000..d1458bd4 --- /dev/null +++ b/backend/Duplicate.v @@ -0,0 +1,240 @@ +(** RTL node duplication using external oracle. Used to form superblock + structures *) + +Require Import AST RTL Maps Globalenvs. +Require Import Coqlib Errors Op. + +Local Open Scope error_monad_scope. +Local Open Scope positive_scope. + +(** External oracle returning the new RTL code (entry point unchanged), + along with the new entrypoint, and a mapping of new nodes to old nodes *) +Axiom duplicate_aux: function -> code * node * (PTree.t node). + +Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux". + +Record xfunction : Type := + { fn_RTL: function; + fn_revmap: PTree.t node; + }. + +Definition xfundef := AST.fundef xfunction. +Definition xprogram := AST.program xfundef unit. +Definition xgenv := Genv.t xfundef unit. + +Definition fundef_RTL (fu: xfundef) : fundef := + match fu with + | Internal f => Internal (fn_RTL f) + | External ef => External ef + end. + +(** * Verification of node duplications *) + +Definition verify_mapping_entrypoint (f: function) (xf: xfunction) : res unit := + match ((fn_revmap xf)!(fn_entrypoint (fn_RTL xf))) with + | None => Error (msg "verify_mapping: No node in xf revmap for entrypoint") + | Some n => match (Pos.compare n (fn_entrypoint f)) with + | Eq => OK tt + | _ => Error (msg "verify_mapping_entrypoint: xf revmap for entrypoint does not correspond to the entrypoint of f") + end + end. + +Definition verify_is_copy revmap n n' := + match revmap!n' with + | None => Error(msg "verify_is_copy None") + | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end + end. + +Fixpoint verify_is_copy_list revmap ln ln' := + match ln with + | n::ln => match ln' with + | n'::ln' => do u <- verify_is_copy revmap n n'; + verify_is_copy_list revmap ln ln' + | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end + | nil => match ln' with + | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'") + | nil => OK tt end + end. + +Lemma product_eq {A B: Type} : + (forall (a b: A), {a=b} + {a<>b}) -> + (forall (c d: B), {c=d} + {c<>d}) -> + forall (x y: A+B), {x=y} + {x<>y}. +Proof. + intros H H'. intros. decide equality. +Qed. + +(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application" + * error when doing so *) +Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}. +Proof. + intros. + apply (builtin_arg_eq Pos.eq_dec). +Defined. +Global Opaque builtin_arg_eq_pos. + +Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}. +Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed. +Global Opaque builtin_res_eq_pos. + +Definition verify_match_inst revmap inst tinst := + match inst with + | Inop n => match tinst with Inop n' => do u <- verify_is_copy revmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end + + | Iop op lr r n => match tinst with + Iop op' lr' r' n' => + do u <- verify_is_copy revmap n n'; + if (eq_operation op op') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then + OK tt + else Error (msg "Different r in Iop") + else Error (msg "Different lr in Iop") + else Error(msg "Different operations in Iop") + | _ => Error(msg "verify_match_inst Inop") end + + | Iload m a lr r n => match tinst with + | Iload m' a' lr' r' n' => + do u <- verify_is_copy revmap n n'; + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r in Iload") + else Error (msg "Different lr in Iload") + else Error (msg "Different addressing in Iload") + else Error (msg "Different mchunk in Iload") + | _ => Error (msg "verify_match_inst Iload") end + + | Istore m a lr r n => match tinst with + | Istore m' a' lr' r' n' => + do u <- verify_is_copy revmap n n'; + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r in Istore") + else Error (msg "Different lr in Istore") + else Error (msg "Different addressing in Istore") + else Error (msg "Different mchunk in Istore") + | _ => Error (msg "verify_match_inst Istore") end + + | Icall s ri lr r n => match tinst with + | Icall s' ri' lr' r' n' => + do u <- verify_is_copy revmap n n'; + if (signature_eq s s') then + if (product_eq Pos.eq_dec ident_eq ri ri') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r r' in Icall") + else Error (msg "Different lr in Icall") + else Error (msg "Different ri in Icall") + else Error (msg "Different signatures in Icall") + | _ => Error (msg "verify_match_inst Icall") end + + | Itailcall s ri lr => match tinst with + | Itailcall s' ri' lr' => + if (signature_eq s s') then + if (product_eq Pos.eq_dec ident_eq ri ri') then + if (list_eq_dec Pos.eq_dec lr lr') then OK tt + else Error (msg "Different lr in Itailcall") + else Error (msg "Different ri in Itailcall") + else Error (msg "Different signatures in Itailcall") + | _ => Error (msg "verify_match_inst Itailcall") end + + | Ibuiltin ef lbar brr n => match tinst with + | Ibuiltin ef' lbar' brr' n' => + do u <- verify_is_copy revmap n n'; + if (external_function_eq ef ef') then + if (list_eq_dec builtin_arg_eq_pos lbar lbar') then + if (builtin_res_eq_pos brr brr') then OK tt + else Error (msg "Different brr in Ibuiltin") + else Error (msg "Different lbar in Ibuiltin") + else Error (msg "Different ef in Ibuiltin") + | _ => Error (msg "verify_match_inst Ibuiltin") end + + | Icond cond lr n1 n2 => match tinst with + | Icond cond' lr' n1' n2' => + do u1 <- verify_is_copy revmap n1 n1'; + do u2 <- verify_is_copy revmap n2 n2'; + if (condition_eq cond cond') then + if (list_eq_dec Pos.eq_dec lr lr') then OK tt + else Error (msg "Different lr in Icond") + else Error (msg "Different cond in Icond") + | _ => Error (msg "verify_match_inst Icond") end + + | Ijumptable r ln => match tinst with + | Ijumptable r' ln' => + do u <- verify_is_copy_list revmap ln ln'; + if (Pos.eq_dec r r') then OK tt + else Error (msg "Different r in Ijumptable") + | _ => Error (msg "verify_match_inst Ijumptable") end + + | Ireturn or => match tinst with + | Ireturn or' => + if (option_eq Pos.eq_dec or or') then OK tt + else Error (msg "Different or in Ireturn") + | _ => Error (msg "verify_match_inst Ireturn") end + end. + +Definition verify_mapping_mn f xf (m: positive*positive) := + let (tn, n) := m in + match (fn_code f)!n with + | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code f)!n") + | Some inst => match (fn_code (fn_RTL xf))!tn with + | None => Error (msg "verify_mapping_mn: Could not get an instruction at (fn_code xf)!tn") + | Some tinst => verify_match_inst (fn_revmap xf) inst tinst + end + end. + +Fixpoint verify_mapping_mn_rec f xf lm := + match lm with + | nil => OK tt + | m :: lm => do u <- verify_mapping_mn f xf m; + do u2 <- verify_mapping_mn_rec f xf lm; + OK tt + end. + +Definition verify_mapping_match_nodes (f: function) (xf: xfunction) : res unit := + verify_mapping_mn_rec f xf (PTree.elements (fn_revmap xf)). + +(** Verifies that the [fn_revmap] of the translated function [xf] is giving correct information in regards to [f] *) +Definition verify_mapping (f: function) (xf: xfunction) : res unit := + do u <- verify_mapping_entrypoint f xf; + do v <- verify_mapping_match_nodes f xf; OK tt. +(* TODO - verify the other axiom *) + +(** * Entry points *) + +Definition transf_function_aux (f: function) : res xfunction := + let (tcte, mp) := duplicate_aux f in + let (tc, te) := tcte in + let xf := {| fn_RTL := (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te); fn_revmap := mp |} in + do u <- verify_mapping f xf; + OK xf. + +Theorem transf_function_aux_preserves: + forall f xf, + transf_function_aux f = OK xf -> + fn_sig f = fn_sig (fn_RTL xf) /\ fn_params f = fn_params (fn_RTL xf) /\ fn_stacksize f = fn_stacksize (fn_RTL xf). +Proof. + intros. unfold transf_function_aux in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H. + repeat (split; try reflexivity). +Qed. + +Remark transf_function_aux_fnsig: forall f xf, transf_function_aux f = OK xf -> fn_sig f = fn_sig (fn_RTL xf). + Proof. apply transf_function_aux_preserves. Qed. +Remark transf_function_aux_fnparams: forall f xf, transf_function_aux f = OK xf -> fn_params f = fn_params (fn_RTL xf). + Proof. apply transf_function_aux_preserves. Qed. +Remark transf_function_aux_fnstacksize: forall f xf, transf_function_aux f = OK xf -> fn_stacksize f = fn_stacksize (fn_RTL xf). + Proof. apply transf_function_aux_preserves. Qed. + +Definition transf_function (f: function) : res function := + do xf <- transf_function_aux f; + OK (fn_RTL xf). + +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: program) : res program := + transform_partial_program transf_fundef p.
\ No newline at end of file diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml new file mode 100644 index 00000000..9ff2ae55 --- /dev/null +++ b/backend/Duplicateaux.ml @@ -0,0 +1,13 @@ +open RTL +open Maps + +let rec make_identity_ptree_rec = function +| [] -> PTree.empty +| m::lm -> let (n, _) = m in PTree.set n n (make_identity_ptree_rec lm) + +let make_identity_ptree f = make_identity_ptree_rec (PTree.elements (fn_code f)) + +(* For now, identity function *) +let duplicate_aux f = + let pTreeId = make_identity_ptree f + in (((fn_code f), (fn_entrypoint f)), pTreeId) diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v new file mode 100644 index 00000000..54dd6196 --- /dev/null +++ b/backend/Duplicateproof.v @@ -0,0 +1,467 @@ +(** Correctness proof for code duplication *) +Require Import AST Linking Errors Globalenvs Smallstep. +Require Import Coqlib Maps Events Values. +Require Import Op RTL Duplicate. + +Local Open Scope positive_scope. + +Definition match_prog (p tp: program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. + +(* est-ce plus simple de prendre is_copy: node -> node, avec un noeud hors CFG à la place de None ? *) +Inductive match_inst (is_copy: node -> option node): instruction -> instruction -> Prop := + | match_inst_nop: forall n n', + is_copy n' = (Some n) -> match_inst is_copy (Inop n) (Inop n') + | match_inst_op: forall n n' op lr r, + is_copy n' = (Some n) -> match_inst is_copy (Iop op lr r n) (Iop op lr r n') + | match_inst_load: forall n n' m a lr r, + is_copy n' = (Some n) -> match_inst is_copy (Iload m a lr r n) (Iload m a lr r n') + | match_inst_store: forall n n' m a lr r, + is_copy n' = (Some n) -> match_inst is_copy (Istore m a lr r n) (Istore m a lr r n') + | match_inst_call: forall n n' s ri lr r, + is_copy n' = (Some n) -> match_inst is_copy (Icall s ri lr r n) (Icall s ri lr r n') + | match_inst_tailcall: forall s ri lr, + match_inst is_copy (Itailcall s ri lr) (Itailcall s ri lr) + | match_inst_builtin: forall n n' ef la br, + is_copy n' = (Some n) -> match_inst is_copy (Ibuiltin ef la br n) (Ibuiltin ef la br n') + | match_inst_cond: forall ifso ifso' ifnot ifnot' c lr, + is_copy ifso' = (Some ifso) -> is_copy ifnot' = (Some ifnot) -> + match_inst is_copy (Icond c lr ifso ifnot) (Icond c lr ifso' ifnot') + | match_inst_jumptable: forall ln ln' r, + list_forall2 (fun n n' => (is_copy n' = (Some n))) ln ln' -> + match_inst is_copy (Ijumptable r ln) (Ijumptable r ln') + | match_inst_return: forall or, match_inst is_copy (Ireturn or) (Ireturn or). + +Lemma verify_mapping_mn_rec_step: + forall lb b f xf, + In b lb -> + verify_mapping_mn_rec f xf lb = OK tt -> + verify_mapping_mn f xf b = OK tt. +Proof. + induction lb; intros. + - monadInv H0. inversion H. + - inversion H. + + subst. monadInv H0. destruct x. assumption. + + monadInv H0. destruct x0. eapply IHlb; assumption. +Qed. + +Lemma verify_is_copy_correct: + forall xf n n', + verify_is_copy (fn_revmap xf) n n' = OK tt -> + (fn_revmap xf) ! n' = Some n. +Proof. + intros. unfold verify_is_copy in H. destruct (_ ! n') eqn:REVM; [|inversion H]. + destruct (n ?= n0) eqn:NP; try (inversion H; fail). + eapply Pos.compare_eq in NP. subst. + reflexivity. +Qed. + +Lemma verify_is_copy_list_correct: + forall xf ln ln', + verify_is_copy_list (fn_revmap xf) ln ln' = OK tt -> + list_forall2 (fun n n' => (fn_revmap xf) ! n' = Some n) ln ln'. +Proof. + induction ln. + - intros. destruct ln'; monadInv H. constructor. + - intros. destruct ln'; monadInv H. destruct x. apply verify_is_copy_correct in EQ. + eapply IHln in EQ0. constructor; assumption. +Qed. + +Lemma verify_match_inst_correct: + forall xf i i', + verify_match_inst (fn_revmap xf) i i' = OK tt -> + match_inst (fun nn => (fn_revmap xf) ! nn) i i'. +Proof. + intros. unfold verify_match_inst in H. + destruct i; try (inversion H; fail). +(* Inop *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + constructor; eauto. +(* Iop *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct (eq_operation _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst. + constructor. assumption. +(* Iload *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct (chunk_eq _ _); try discriminate. + destruct (eq_addressing _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst. + constructor. assumption. +(* Istore *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct (chunk_eq _ _); try discriminate. + destruct (eq_addressing _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst. + constructor. assumption. +(* Icall *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct (signature_eq _ _); try discriminate. + destruct (product_eq _ _ _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. subst. + constructor. assumption. +(* Itailcall *) + - destruct i'; try (inversion H; fail). + destruct (signature_eq _ _); try discriminate. + destruct (product_eq _ _ _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. subst. clear H. + constructor. +(* Ibuiltin *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct (external_function_eq _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (builtin_res_eq_pos _ _); try discriminate. subst. + constructor. assumption. +(* Icond *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_correct in EQ. + destruct x0. eapply verify_is_copy_correct in EQ1. + destruct (condition_eq _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. subst. + constructor; assumption. +(* Ijumptable *) + - destruct i'; try (inversion H; fail). monadInv H. + destruct x. eapply verify_is_copy_list_correct in EQ. + destruct (Pos.eq_dec _ _); try discriminate. subst. + constructor. assumption. +(* Ireturn *) + - destruct i'; try (inversion H; fail). + destruct (option_eq _ _ _); try discriminate. subst. clear H. + constructor. +Qed. + + +Lemma verify_mapping_mn_correct: + forall mp n n' i f xf tc, + mp ! n' = Some n -> + (fn_code f) ! n = Some i -> + (fn_code (fn_RTL xf)) = tc -> + fn_revmap xf = mp -> + verify_mapping_mn f xf (n', n) = OK tt -> + exists i', + tc ! n' = Some i' + /\ match_inst (fun nn => mp ! nn) i i'. +Proof. + intros. unfold verify_mapping_mn in H3. rewrite H0 in H3. clear H0. rewrite H1 in H3. clear H1. + destruct (tc ! n') eqn:TCN; [| inversion H3]. + exists i0. split; auto. rewrite <- H2. + eapply verify_match_inst_correct. assumption. +Qed. + + +Lemma verify_mapping_mn_rec_correct: + forall mp n n' i f xf tc, + mp ! n' = Some n -> + (fn_code f) ! n = Some i -> + (fn_code (fn_RTL xf)) = tc -> + fn_revmap xf = mp -> + verify_mapping_mn_rec f xf (PTree.elements mp) = OK tt -> + exists i', + tc ! n' = Some i' + /\ match_inst (fun nn => mp ! nn) i i'. +Proof. + intros. exploit PTree.elements_correct. eapply H. intros IN. + eapply verify_mapping_mn_rec_step in H3; eauto. + eapply verify_mapping_mn_correct; eauto. +Qed. + + +Theorem revmap_correct: forall f xf n n', + transf_function_aux f = OK xf -> + (fn_revmap xf)!n' = Some n -> + (forall i, (fn_code f)!n = Some i -> exists i', (fn_code (fn_RTL xf))!n' = Some i' /\ match_inst (fun n' => (fn_revmap xf)!n') i i'). +Proof. + intros until n'. intros TRANSF REVM i FNC. + unfold transf_function_aux in TRANSF. destruct (duplicate_aux f) as (tcte & mp). destruct tcte as (tc & te). monadInv TRANSF. + simpl in *. monadInv EQ. clear EQ0. + unfold verify_mapping_match_nodes in EQ. simpl in EQ. destruct x1. + eapply verify_mapping_mn_rec_correct. 5: eapply EQ. all: eauto. +Qed. + + +Theorem revmap_entrypoint: + forall f xf, transf_function_aux f = OK xf -> (fn_revmap xf)!(fn_entrypoint (fn_RTL xf)) = Some (fn_entrypoint f). +Proof. + intros. unfold transf_function_aux in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). + monadInv H. simpl. monadInv EQ. unfold verify_mapping_entrypoint in EQ0. simpl in EQ0. + destruct (mp ! te) eqn:PT; try discriminate. + destruct (n ?= fn_entrypoint f) eqn:EQQ; try discriminate. inv EQ0. + apply Pos.compare_eq in EQQ. congruence. +Qed. + +Section PRESERVATION. + +Variable prog: program. +Variable tprog: program. + +Hypothesis TRANSL: match_prog prog tprog. + +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + rewrite <- (Genv.find_symbol_match TRANSL). reflexivity. +Qed. + +Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z. +Proof. + unfold Senv.equiv. intuition congruence. +Qed. + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof. + eapply (Genv.senv_match TRANSL). +Qed. + +Lemma functions_translated: + forall (v: val) (f: fundef), + Genv.find_funct ge v = Some f -> + exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tge v = Some tf /\ linkorder cunit prog. +Proof. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & A & B & C). + repeat eexists; intuition eauto. + + unfold incl; auto. + + eapply linkorder_refl. +Qed. + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + exists tf, + Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. +Proof. + intros. + exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto. +Qed. + +Lemma function_sig_translated: + forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f. +Proof. + intros. destruct f. + - simpl in H. monadInv H. simpl. symmetry. monadInv EQ. apply transf_function_aux_preserves. assumption. + - simpl in H. monadInv H. (* monadInv EQ. *) reflexivity. +Qed. + +Lemma sig_preserved: + forall f tf, + transf_fundef f = OK tf -> + funsig tf = funsig f. +Proof. + unfold transf_fundef, transf_partial_fundef; intros. + destruct f. monadInv H. simpl. symmetry. monadInv EQ. apply transf_function_aux_preserves. assumption. + inv H. reflexivity. +Qed. + +Lemma list_nth_z_revmap: + forall ln f ln' (pc pc': node) val, + list_nth_z ln val = Some pc -> + list_forall2 (fun n n' => (fn_revmap f)!n' = Some n) ln ln' -> + exists pc', + list_nth_z ln' val = Some pc' + /\ (fn_revmap f)!pc' = Some pc. +Proof. + induction ln; intros until val; intros LNZ LFA. + - inv LNZ. + - inv LNZ. destruct (zeq val 0) eqn:ZEQ. + + inv H0. destruct ln'; inv LFA. + simpl. exists p. split; auto. + + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto. + intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. +Qed. + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + | match_stackframe_intro: + forall res f sp pc rs xf pc' + (TRANSF: transf_function_aux f = OK xf) + (DUPLIC: (fn_revmap xf)!pc' = Some pc), + match_stackframes (Stackframe res f sp pc rs) (Stackframe res (fn_RTL xf) sp pc' rs). + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall st f sp pc rs m st' xf pc' + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: transf_function_aux f = OK xf) + (DUPLIC: (fn_revmap xf)!pc' = Some pc), + match_states (State st f sp pc rs m) (State st' (fn_RTL xf) sp pc' rs m) + | match_states_call: + forall st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: transf_fundef f = OK f'), + match_states (Callstate st f args m) (Callstate st' f' args m) + | match_states_return: + forall st st' v m + (STACKS: list_forall2 match_stackframes st st'), + match_states (Returnstate st v m) (Returnstate st' v m). + +Theorem transf_initial_states: + forall s1, initial_state prog s1 -> + exists s2, initial_state tprog s2 /\ match_states s1 s2. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF). + eexists. split. + - econstructor. + + eapply (Genv.init_mem_transf_partial TRANSL); eauto. + + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main. eauto. + + exploit function_ptr_translated; eauto. + + destruct f. + * monadInv TRANSF. monadInv EQ. rewrite <- H3. symmetry; eapply transf_function_aux_preserves. assumption. + * monadInv TRANSF. (* monadInv EQ. *) assumption. + - constructor; eauto. constructor. +Qed. + +Theorem transf_final_states: + forall s1 s2 r, + match_states s1 s2 -> final_state s1 r -> final_state s2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Theorem step_simulation: + forall s1 t s1', step ge s1 t s1' -> + forall s2 (MS: match_states s1 s2), + exists s2', + step tge s2 t s2' + /\ match_states s1' s2'. +Proof. + induction 1; intros; inv MS. +(* Inop *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). + inv H3. + eexists. split. + + eapply exec_Inop; eauto. + + constructor; eauto. +(* Iop *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Iop; eauto. erewrite eval_operation_preserved; eauto. + + constructor; eauto. +(* Iload *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto. + + constructor; auto. +(* Istore *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto. + + constructor; auto. +(* Icall *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + destruct ros. + * simpl in H0. apply functions_translated in H0. + destruct H0 as (tf & cunit & TFUN & GFIND & LO). + eexists. split. + + eapply exec_Icall. eassumption. simpl. eassumption. + apply function_sig_translated. assumption. + + repeat (constructor; auto). + * simpl in H0. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. + apply function_ptr_translated in H0. destruct H0 as (tf & GFF & TF). + eexists. split. + + eapply exec_Icall. eassumption. simpl. rewrite symbols_preserved. rewrite GFS. + eassumption. apply function_sig_translated. assumption. + + repeat (constructor; auto). +(* Itailcall *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H10 & H11). inv H11. + pose symbols_preserved as SYMPRES. + destruct ros. + * simpl in H0. apply functions_translated in H0. + destruct H0 as (tf & cunit & TFUN & GFIND & LO). + eexists. split. + + eapply exec_Itailcall. eassumption. simpl. eassumption. + apply function_sig_translated. assumption. + erewrite <- transf_function_aux_fnstacksize; eauto. + + repeat (constructor; auto). + * simpl in H0. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. + apply function_ptr_translated in H0. destruct H0 as (tf & GFF & TF). + eexists. split. + + eapply exec_Itailcall. eassumption. simpl. rewrite symbols_preserved. rewrite GFS. + eassumption. apply function_sig_translated. assumption. + erewrite <- transf_function_aux_fnstacksize; eauto. + + repeat (constructor; auto). +(* Ibuiltin *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + + constructor; auto. +(* Icond *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Icond; eauto. + + constructor; auto. destruct b; auto. +(* Ijumptable *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + exploit list_nth_z_revmap; eauto. intros (pc'1 & LNZ & REVM). + eexists. split. + + eapply exec_Ijumptable; eauto. + + constructor; auto. +(* Ireturn *) + - eapply revmap_correct in DUPLIC; eauto. + destruct DUPLIC as (i' & H2 & H3). inv H3. + pose symbols_preserved as SYMPRES. + eexists. split. + + eapply exec_Ireturn; eauto. erewrite <- transf_function_aux_fnstacksize; eauto. + + constructor; auto. +(* exec_function_internal *) + - monadInv TRANSF. monadInv EQ. eexists. split. + + eapply exec_function_internal. erewrite <- transf_function_aux_fnstacksize; eauto. + + erewrite transf_function_aux_fnparams; eauto. + econstructor; eauto. apply revmap_entrypoint. assumption. +(* exec_function_external *) + - monadInv TRANSF. (* monadInv EQ. *) eexists. split. + + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor. assumption. +(* exec_return *) + - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split. + + constructor. + + inv H1. constructor; assumption. +Qed. + +Theorem transf_program_correct: + forward_simulation (semantics prog) (semantics tprog). +Proof. + eapply forward_simulation_step with match_states. + - eapply senv_preserved. + - eapply transf_initial_states. + - eapply transf_final_states. + - eapply step_simulation. +Qed. + +End PRESERVATION. diff --git a/common/AST.v b/common/AST.v index a91138c9..7ffe355d 100644 --- a/common/AST.v +++ b/common/AST.v @@ -17,7 +17,7 @@ the abstract syntax trees of many of the intermediate languages. *) Require Import String. -Require Import Coqlib Maps Errors Integers Floats. +Require Import Coqlib Maps Errors Integers Floats BinPos. Require Archi. Set Implicit Arguments. @@ -630,11 +630,28 @@ Inductive builtin_arg (A: Type) : Type := | BA_splitlong (hi lo: builtin_arg A) | BA_addptr (a1 a2: builtin_arg A). +Definition builtin_arg_eq {A: Type}: + (forall x y : A, {x = y} + {x <> y}) -> + forall (ba1 ba2: (builtin_arg A)), {ba1=ba2} + {ba1<>ba2}. +Proof. + intro. generalize Integers.int_eq int64_eq float_eq float32_eq chunk_eq ptrofs_eq ident_eq. + decide equality. +Defined. +Global Opaque builtin_arg_eq. + Inductive builtin_res (A: Type) : Type := | BR (x: A) | BR_none | BR_splitlong (hi lo: builtin_res A). +Definition builtin_res_eq {A: Type}: + (forall x y : A, {x = y} + {x <> y}) -> + forall (a b: builtin_res A), {a=b} + {a<>b}. +Proof. + intro. decide equality. +Defined. +Global Opaque builtin_res_eq. + Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident := match a with | BA_loadglobal chunk id ofs => id :: nil diff --git a/driver/Compiler.v b/driver/Compiler.v index c683c136..d7784f7a 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -38,6 +38,7 @@ Require RTLgen. Require Tailcall. Require Inlining. Require Renumber. +Require Duplicate. Require Constprop. Require CSE. Require Deadcode. @@ -59,6 +60,7 @@ Require RTLgenproof. Require Tailcallproof. Require Inliningproof. Require Renumberproof. +Require Duplicateproof. Require Constpropproof. Require CSEproof. Require Deadcodeproof. @@ -126,16 +128,18 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ time "Duplicating" Duplicate.transf_program @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 7) - @@@ time "Unused globals" Unusedglob.transform_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 8) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 9) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -238,6 +242,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog + ::: mkpass Duplicateproof.match_prog ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -281,17 +286,18 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p9 := Renumber.transf_program p8) in *. - set (p10 := total_if optim_constprop Constprop.transf_program p9) in *. - set (p11 := total_if optim_constprop Renumber.transf_program p10) in *. - destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate. - destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. - destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. - set (p16 := Tunneling.tunnel_program p15) in *. - destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate. - set (p18 := CleanupLabels.transf_program p17) in *. - destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate. - destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. + set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. + destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. + destruct (partial_if optim_redundancy Deadcode.transf_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. + destruct (Unusedglob.transform_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + set (p17 := Tunneling.tunnel_program p16) in *. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + set (p19 := CleanupLabels.transf_program p18) in *. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -302,17 +308,18 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. - exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match. - exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14; split. apply Unusedglobproof.transf_program_match; auto. - exists p15; split. apply Allocproof.transf_program_match; auto. - exists p16; split. apply Tunnelingproof.transf_program_match. - exists p17; split. apply Linearizeproof.transf_program_match; auto. - exists p18; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p20; split. apply Stackingproof.transf_program_match; auto. + exists p10; split. apply Duplicateproof.transf_program_match; auto. + exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. + exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. + exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p15; split. apply Unusedglobproof.transf_program_match; auto. + exists p16; split. apply Allocproof.transf_program_match; auto. + exists p17; split. apply Tunnelingproof.transf_program_match. + exists p18; split. apply Linearizeproof.transf_program_match; auto. + exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. + exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. + exists p21; split. apply Stackingproof.transf_program_match; auto. exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -364,7 +371,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p22)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -383,6 +390,7 @@ Ltac DestructM := eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. eapply Duplicateproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. diff --git a/lib/Floats.v b/lib/Floats.v index 13350dd0..272efa52 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -16,7 +16,7 @@ (** Formalization of floating-point numbers, using the Flocq library. *) -Require Import Coqlib Zbits Integers. +Require Import Coqlib Zbits Integers Axioms. (*From Flocq*) Require Import Binary Bits Core. Require Import IEEE754_extra. @@ -27,8 +27,69 @@ Close Scope R_scope. Open Scope Z_scope. Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *) + +Definition float_eq: forall (i1 i2: float), {i1=i2} + {i1<>i2}. +Proof. + intros. destruct i1. +(* B754_zero *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_infinity *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_nan *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + generalize (Pos.eq_dec pl pl0). intro. inv H. + ++ left. apply eqb_prop in BEQ. subst. + assert (e = e0) by (apply proof_irr). congruence. + ++ right. intro. inv H. contradiction. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_finite *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ; [apply eqb_prop in BEQ | apply eqb_false_iff in BEQ]. + generalize (Pos.eq_dec m m0). intro. inv H. + generalize (Z.eq_dec e e1). intro. inv H. + 1: { left. assert (e0 = e2) by (apply proof_irr). congruence. } + all: right; intro; inv H; contradiction. +Qed. + Definition float32 := binary32. (**r the type of IEE754 single-precision FP numbers *) +Definition float32_eq: forall (i1 i2: float32), {i1=i2} + {i1<>i2}. +Proof. + intros. destruct i1. +(* B754_zero *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_infinity *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_nan *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + generalize (Pos.eq_dec pl pl0). intro. inv H. + ++ left. apply eqb_prop in BEQ. subst. + assert (e = e0) by (apply proof_irr). congruence. + ++ right. intro. inv H. contradiction. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_finite *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ; [apply eqb_prop in BEQ | apply eqb_false_iff in BEQ]. + generalize (Pos.eq_dec m m0). intro. inv H. + generalize (Z.eq_dec e e1). intro. inv H. + 1: { left. assert (e0 = e2) by (apply proof_irr). congruence. } + all: right; intro; inv H; contradiction. +Qed. + (** Boolean-valued comparisons *) Definition cmp_of_comparison (c: comparison) (x: option Datatypes.comparison) : bool := diff --git a/lib/Integers.v b/lib/Integers.v index f4213332..08a416c1 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -16,7 +16,7 @@ (** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *) Require Import Eqdep_dec Zquot Zwf. -Require Import Coqlib Zbits. +Require Import Coqlib Zbits Axioms. Require Archi. (** * Comparisons *) @@ -29,6 +29,11 @@ Inductive comparison : Type := | Cgt : comparison (**r greater than *) | Cge : comparison. (**r greater than or equal *) +Definition comparison_eq: forall (x y: comparison), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + Definition negate_comparison (c: comparison): comparison := match c with | Ceq => Cne @@ -4156,8 +4161,26 @@ End Int64. Strategy 0 [Wordsize_64.wordsize]. +Definition int_eq: forall (i1 i2: int), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Notation int64 := Int64.int. +Definition int64_eq: forall (i1 i2: int64), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Global Opaque Int.repr Int64.repr Byte.repr. (** * Specialization to offsets in pointer values *) @@ -4434,6 +4457,15 @@ Strategy 0 [Wordsize_Ptrofs.wordsize]. Notation ptrofs := Ptrofs.int. +Definition ptrofs_eq: forall (i1 i2: ptrofs), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Global Opaque Ptrofs.repr. Hint Resolve Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index f9a774e8..ce9a5dcd 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -51,6 +51,12 @@ Inductive condition : Type := | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *) +Definition condition_eq: forall (x y: condition), {x = y} + {x <> y}. +Proof. + generalize comparison_eq int_eq int64_eq. + decide equality. +Defined. + Inductive condition0 : Type := | Ccomp0 (c: comparison) (**r signed integer comparison with 0 *) | Ccompu0 (c: comparison) (**r unsigned integer comparison with 0 *) |