diff options
Diffstat (limited to 'kvx/lib/Machblock.v')
| -rw-r--r-- | kvx/lib/Machblock.v | 29 |
1 files changed, 18 insertions, 11 deletions
diff --git a/kvx/lib/Machblock.v b/kvx/lib/Machblock.v index 08e0eba2..404c2a96 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; @@ -65,7 +70,7 @@ Lemma bblock_eq: b1 = b2. Proof. intros. destruct b1. destruct b2. - simpl in *. subst. auto. + cbn in *. subst. auto. Qed. Definition length_opt {A} (o: option A) : nat := @@ -80,17 +85,19 @@ Lemma size_null b: size b = 0%nat -> header b = nil /\ body b = nil /\ exit b = None. Proof. - destruct b as [h b e]. simpl. unfold size. simpl. + destruct b as [h b e]. cbn. unfold size. cbn. intros H. assert (length h = 0%nat) as Hh; [ omega |]. assert (length b = 0%nat) as Hb; [ omega |]. assert (length_opt e = 0%nat) as He; [ omega|]. repeat split. - destruct h; try (simpl in Hh; discriminate); auto. - destruct b; try (simpl in Hb; discriminate); auto. - destruct e; try (simpl in He; discriminate); auto. + destruct h; try (cbn in Hh; discriminate); auto. + destruct b; try (cbn in Hb; discriminate); auto. + destruct e; try (cbn 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. @@ -120,13 +127,13 @@ Definition is_label (lbl: label) (bb: bblock) : bool := Lemma is_label_correct_true lbl bb: List.In lbl (header bb) <-> is_label lbl bb = true. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. Lemma is_label_correct_false lbl bb: ~(List.In lbl (header bb)) <-> is_label lbl bb = false. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. @@ -155,7 +162,7 @@ Definition find_function_ptr Genv.find_symbol ge symb end. -(** Machblock execution states. *) +(** ** Machblock execution states. *) Inductive stackframe: Type := | Stackframe: |