diff options
Diffstat (limited to 'kvx/lib/Machblock.v')
| -rw-r--r-- | kvx/lib/Machblock.v | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/kvx/lib/Machblock.v b/kvx/lib/Machblock.v index 08e0eba2..edae0ed4 100644 --- a/kvx/lib/Machblock.v +++ b/kvx/lib/Machblock.v @@ -12,6 +12,8 @@ (* *) (* *************************************************************) +(** Abstract syntax and semantics of a Mach variant, structured with basic-blocks. *) + Require Import Coqlib. Require Import Maps. Require Import AST. @@ -28,7 +30,9 @@ Require Stacklayout. Require Import Mach. Require Import Linking. -(** basic instructions (ie no control-flow) *) +(** * Abstract Syntax *) + +(** ** basic instructions (ie no control-flow) *) Inductive basic_inst: Type := | MBgetstack: ptrofs -> typ -> mreg -> basic_inst | MBsetstack: mreg -> ptrofs -> typ -> basic_inst @@ -40,7 +44,7 @@ Inductive basic_inst: Type := Definition bblock_body := list basic_inst. -(** control flow instructions *) +(** ** control flow instructions *) Inductive control_flow_inst: Type := | MBcall: signature -> mreg + ident -> control_flow_inst | MBtailcall: signature -> mreg + ident -> control_flow_inst @@ -51,6 +55,7 @@ Inductive control_flow_inst: Type := | MBreturn: control_flow_inst . +(** ** basic block *) Record bblock := mk_bblock { header: list label; body: bblock_body; @@ -91,6 +96,8 @@ Proof. destruct e; try (simpl in He; discriminate); auto. Qed. +(** ** programs *) + Definition code := list bblock. Record function: Type := mkfunction @@ -106,7 +113,7 @@ Definition program := AST.program fundef unit. Definition genv := Genv.t fundef unit. -(*** sémantique ***) +(** * Operational (blockstep) semantics ***) Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. Proof. @@ -155,7 +162,7 @@ Definition find_function_ptr Genv.find_symbol ge symb end. -(** Machblock execution states. *) +(** ** Machblock execution states. *) Inductive stackframe: Type := | Stackframe: |