diff options
Diffstat (limited to 'kvx/Asm.v')
| -rw-r--r-- | kvx/Asm.v | 50 |
1 files changed, 26 insertions, 24 deletions
@@ -13,7 +13,7 @@ (* *) (* *************************************************************) -(** * Abstract syntax for KVX textual assembly language. +(** Abstract syntax for KVX textual assembly language. Each emittable instruction is defined here. ';;' is also defined as an instruction. The goal of this representation is to stay compatible with the rest of the generic backend of CompCert @@ -49,7 +49,7 @@ Inductive addressing : Type := | ARegXS (ro: ireg) . -(** Syntax *) +(** * Syntax *) Inductive instruction : Type := (** pseudo instructions *) | Pallocframe (sz: Z) (pos: ptrofs) (**r allocate new stack frame *) @@ -104,7 +104,7 @@ Inductive instruction : Type := | Pclzll (rd rs: ireg) | Pstsud (rd rs1 rs2: ireg) - (** Loads **) + (** Loads *) | Plb (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *) | Plbu (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte unsigned *) | Plh (trap: trapping_mode) (rd: ireg) (ra: ireg) (ofs: addressing) (**r load half word *) @@ -118,7 +118,7 @@ Inductive instruction : Type := | Plq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r load 2*64-bit *) | Plo (rs: gpreg_o) (ra: ireg) (ofs: addressing) (**r load 4*64-bit *) - (** Stores **) + (** Stores *) | Psb (rs: ireg) (ra: ireg) (ofs: addressing) (**r store byte *) | Psh (rs: ireg) (ra: ireg) (ofs: addressing) (**r store half byte *) | Psw (rs: ireg) (ra: ireg) (ofs: addressing) (**r store int32 *) @@ -547,6 +547,8 @@ Definition basic_to_instruction (b: basic) := | PStoreORRO qrs ra ofs => Pso qrs ra (AOff ofs) end. +(** * Semantics (given through the existence of well-formed VLIW program) *) + Section RELSEM. Definition code := list instruction. @@ -609,15 +611,15 @@ Program Definition genv_trans (ge: genv) : Asmvliw.genv := Genv.genv_defs := PTree.map1 globdef_proj (Genv.genv_defs ge); Genv.genv_next := Genv.genv_next ge |}. Next Obligation. - destruct ge. simpl in *. eauto. + destruct ge. cbn in *. eauto. Qed. Next Obligation. - destruct ge; simpl in *. + destruct ge; cbn in *. rewrite PTree.gmap1 in H. destruct (genv_defs ! b) eqn:GEN. - eauto. - discriminate. Qed. Next Obligation. - destruct ge; simpl in *. + destruct ge; cbn in *. eauto. Qed. @@ -653,14 +655,14 @@ Program Definition transf_function (f: Asmvliw.function) : function := Lemma transf_function_proj: forall f, function_proj (transf_function f) = f. Proof. - intros f. destruct f as [sig blks]. unfold function_proj. simpl. auto. + intros f. destruct f as [sig blks]. unfold function_proj. cbn. auto. Qed. Definition transf_fundef : Asmvliw.fundef -> fundef := AST.transf_fundef transf_function. Lemma transf_fundef_proj: forall f, fundef_proj (transf_fundef f) = f. Proof. - intros f. destruct f as [f|e]; simpl; auto. + intros f. destruct f as [f|e]; cbn; auto. rewrite transf_function_proj. auto. Qed. @@ -672,18 +674,18 @@ Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B), prog_main p1 = prog_main p2 -> p1 = p2. Proof. - intros. destruct p1. destruct p2. simpl in *. subst. auto. + intros. destruct p1. destruct p2. cbn in *. subst. auto. Qed. Lemma transf_program_proj: forall p, program_proj (transf_program p) = p. Proof. - intros p. destruct p as [defs pub main]. unfold program_proj. simpl. - apply program_equals; simpl; auto. + intros p. destruct p as [defs pub main]. unfold program_proj. cbn. + apply program_equals; cbn; auto. induction defs. - - simpl; auto. - - simpl. rewrite IHdefs. - destruct a as [id gd]; simpl. - destruct gd as [f|v]; simpl; auto. + - cbn; auto. + - cbn. rewrite IHdefs. + destruct a as [id gd]; cbn. + destruct gd as [f|v]; cbn; auto. rewrite transf_fundef_proj. auto. Qed. @@ -705,16 +707,16 @@ Lemma match_program_transf: forall p tp, match_prog p tp -> transf_program p = tp. Proof. intros p tp H. inversion_clear H. inv H1. - destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. simpl in *. - subst. unfold transf_program. unfold transform_program. simpl. - apply program_equals; simpl; auto. - induction H0; simpl; auto. + destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. cbn in *. + subst. unfold transf_program. unfold transform_program. cbn. + apply program_equals; cbn; auto. + induction H0; cbn; auto. rewrite IHlist_forall2. apply cons_extract. destruct a1 as [ida gda]. destruct b1 as [idb gdb]. - simpl in *. + cbn in *. inv H. inv H2. - - simpl in *. subst. auto. - - simpl in *. subst. inv H. auto. + - cbn in *. subst. auto. + - cbn in *. subst. inv H. auto. Qed. Section PRESERVATION. @@ -742,7 +744,7 @@ Proof. pose proof (match_program_transf prog tprog TRANSF) as TR. subst. unfold semantics. rewrite transf_program_proj. - eapply forward_simulation_step with (match_states := match_states); simpl; auto. + eapply forward_simulation_step with (match_states := match_states); cbn; auto. - intros. exists s1. split; auto. congruence. - intros. inv H. auto. - intros. exists s1'. inv H0. split; auto. congruence. |