diff options
| -rw-r--r-- | mppa_k1c/lib/Machblock.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/lib/Machblockgen.v | 13 |
2 files changed, 6 insertions, 11 deletions
diff --git a/mppa_k1c/lib/Machblock.v b/mppa_k1c/lib/Machblock.v index 30393fd5..2759c49d 100644 --- a/mppa_k1c/lib/Machblock.v +++ b/mppa_k1c/lib/Machblock.v @@ -14,7 +14,7 @@ Require Stacklayout. Require Import Mach. Require Import Linking. -(** instructions "basiques" (ie non control-flow) *) +(** basic instructions (ie no control-flow) *) Inductive basic_inst: Type := | MBgetstack: ptrofs -> typ -> mreg -> basic_inst | MBsetstack: mreg -> ptrofs -> typ -> basic_inst @@ -26,7 +26,7 @@ Inductive basic_inst: Type := Definition bblock_body := list basic_inst. -(** instructions de control flow *) +(** control flow instructions *) Inductive control_flow_inst: Type := | MBcall: signature -> mreg + ident -> control_flow_inst | MBtailcall: signature -> mreg + ident -> control_flow_inst diff --git a/mppa_k1c/lib/Machblockgen.v b/mppa_k1c/lib/Machblockgen.v index 4dfc309e..db48934e 100644 --- a/mppa_k1c/lib/Machblockgen.v +++ b/mppa_k1c/lib/Machblockgen.v @@ -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,7 +98,7 @@ 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 |