diff options
Diffstat (limited to 'mppa_k1c/lib/Machblockgen.v')
| -rw-r--r-- | mppa_k1c/lib/Machblockgen.v | 23 |
1 files changed, 9 insertions, 14 deletions
diff --git a/mppa_k1c/lib/Machblockgen.v b/mppa_k1c/lib/Machblockgen.v index 4dfc309e..2ba42814 100644 --- a/mppa_k1c/lib/Machblockgen.v +++ b/mppa_k1c/lib/Machblockgen.v @@ -33,7 +33,7 @@ Definition trans_inst (i:Mach.instruction) : Machblock_inst := | Msetstack src ofs ty => MB_basic (MBsetstack src ofs ty) | Mgetparam ofs ty dst => MB_basic (MBgetparam ofs ty dst) | Mop op args res => MB_basic (MBop op args res) - | Mload chunk addr args dst => MB_basic (MBload chunk addr args dst) + | Mload trap chunk addr args dst=> MB_basic (MBload trap chunk addr args dst) | Mstore chunk addr args src => MB_basic (MBstore chunk addr args src) | Mlabel l => MB_label l end. @@ -57,12 +57,9 @@ Definition add_to_new_bblock (i:Machblock_inst) : bblock := | MB_cfi i => cfi_bblock i end. -(* ajout d'une instruction en début d'une liste de blocks *) -(* Soit /1\ ajout en tête de block, soit /2\ ajout dans un nouveau block*) -(* bl est vide -> /2\ *) -(* cfi -> /2\ (ajout dans exit)*) -(* basic -> /1\ si header vide, /2\ si a un header *) -(* label -> /1\ (dans header)*) +(** Adding an instruction to the beginning of a bblock list + * Either adding the instruction to the head of the list, + * or create a new bblock with the instruction *) Definition add_to_code (i:Machblock_inst) (bl:code) : code := match bl with | bh::bl0 => match i with @@ -86,8 +83,6 @@ Fixpoint trans_code_rev (c: Mach.code) (bl:code) : code := Function trans_code (c: Mach.code) : code := trans_code_rev (List.rev_append c nil) nil. - -(* à finir pour passer des Mach.function au function, etc. *) Definition transf_function (f: Mach.function) : function := {| fn_sig:=Mach.fn_sig f; fn_code:=trans_code (Mach.fn_code f); @@ -103,14 +98,14 @@ Definition transf_program (src: Mach.program) : program := transform_program transf_fundef src. -(** Abstraction de trans_code *) +(** Abstracting trans_code *) Inductive is_end_block: Machblock_inst -> code -> Prop := | End_empty mbi: is_end_block mbi nil | End_basic bi bh bl: header bh <> nil -> is_end_block (MB_basic bi) (bh::bl) | End_cfi cfi bl: bl <> nil -> is_end_block (MB_cfi cfi) bl. -Local Hint Resolve End_empty End_basic End_cfi. +Local Hint Resolve End_empty End_basic End_cfi: core. Inductive is_trans_code: Mach.code -> code -> Prop := | Tr_nil: is_trans_code nil nil @@ -128,7 +123,7 @@ Inductive is_trans_code: Mach.code -> code -> Prop := header bh = nil -> is_trans_code (i::c) (add_basic bi bh::bl). -Local Hint Resolve Tr_nil Tr_end_block. +Local Hint Resolve Tr_nil Tr_end_block: core. Lemma add_to_code_is_trans_code i c bl: is_trans_code c bl -> @@ -150,7 +145,7 @@ Proof. rewrite <- Heqti. eapply End_cfi. congruence. Qed. -Local Hint Resolve add_to_code_is_trans_code. +Local Hint Resolve add_to_code_is_trans_code: core. Lemma trans_code_is_trans_code_rev c1: forall c2 mbi, is_trans_code c2 mbi -> @@ -190,7 +185,7 @@ Proof. exists mbi1. split; congruence. Qed. -Local Hint Resolve trans_code_is_trans_code. +Local Hint Resolve trans_code_is_trans_code: core. Theorem is_trans_code_inv c bl: is_trans_code c bl <-> bl=(trans_code c). Proof. |