From 301713c2419196344003dd9708f16ef2eb9f7b37 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 22 Jan 2021 09:31:07 +0000
Subject: Add semantics for RTLBlockInstr and RTLBlock

---
 src/hls/RTLBlockInstr.v | 35 +++++++++++++++++++++--------------
 1 file changed, 21 insertions(+), 14 deletions(-)

(limited to 'src/hls/RTLBlockInstr.v')

diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 8549209..f9d1073 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -49,6 +49,7 @@ Record bblock (bblock_body : Type) : Type := mk_bblock {
     bb_body: bblock_body;
     bb_exit: option cf_instr
   }.
+Arguments mk_bblock [bblock_body].
 Arguments bb_body [bblock_body].
 Arguments bb_exit [bblock_body].
 
@@ -96,37 +97,41 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   end.
 
 Inductive instr_state : Type :=
-  | InstrState :
-      forall (rs : regset)
-             (m : mem),
-      instr_state.
+| InstrState:
+    forall (rs: regset)
+           (m: mem),
+    instr_state.
+
+Inductive cf_instr_state : Type :=
+| CfInstrState:
+    forall ()
 
 Section RELSEM.
 
-  Context (fundef : Type).
+  Context (fundef: Type).
 
   Definition genv := Genv.t fundef unit.
 
-  Context (ge : genv) (sp : val).
+  Context (ge: genv) (sp: val).
 
-  Inductive step_instr : instr_state -> instr -> instr_state -> Prop :=
-  | exec_RBnop :
+  Inductive step_instr: instr_state -> instr -> instr_state -> Prop :=
+  | exec_RBnop:
       forall rs m,
       step_instr (InstrState rs m) RBnop (InstrState rs m)
-  | exec_RBop :
+  | exec_RBop:
       forall op v res args rs m,
       eval_operation ge sp op rs##args m = Some v ->
       step_instr (InstrState rs m)
                  (RBop op args res)
                  (InstrState (rs#res <- v) m)
-  | exec_RBload :
+  | exec_RBload:
       forall addr rs args a chunk m v dst,
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.loadv chunk m a = Some v ->
       step_instr (InstrState rs m)
                  (RBload chunk addr args dst)
                  (InstrState (rs#dst <- v) m)
-  | exec_RBstore :
+  | exec_RBstore:
       forall addr rs args a chunk m src m',
       eval_addressing ge sp addr rs##args = Some a ->
       Mem.storev chunk m a rs#src = Some m' ->
@@ -134,14 +139,16 @@ Section RELSEM.
                  (RBstore chunk addr args src)
                  (InstrState rs m').
 
-  Inductive step_instr_list : instr_state -> list instr -> instr_state -> Prop :=
-    | exec_RBcons :
+  Inductive step_instr_list: instr_state -> list instr -> instr_state -> Prop :=
+    | exec_RBcons:
         forall state i state' state'' instrs,
         step_instr state i state' ->
         step_instr_list state' instrs state'' ->
         step_instr_list state (i :: instrs) state''
-    | exec_RBnil :
+    | exec_RBnil:
         forall state,
         step_instr_list state nil state.
 
+  Inductive step_cf_instr:
+
 End RELSEM.
-- 
cgit