Add semantics for RTLBlockInstr and RTLBlock

2 files changed, 72 insertions, 22 deletions

diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 8a8f7f9..a8efa33 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -32,7 +32,7 @@ Require Import vericert.hls.RTLBlockInstr.
 
 Definition bblock_body : Type := list instr.
 
-Definition code : Type := PTree.t (bblock bblock_body).
+Definition code : Type := PTree.t (@bblock bblock_body).
 
 Record function: Type := mkfunction {
   fn_sig: signature;
@@ -52,17 +52,60 @@ Definition funsig (fd: fundef) :=
   | External ef => ef_sig ef
   end.
 
-Definition genv := Genv.t fundef unit.
-Definition regset := Regmap.t val.
+Inductive stackframe : Type :=
+| Stackframe:
+    forall (res: reg)            (**r where to store the result *)
+           (f: function)         (**r calling function *)
+           (sp: val)             (**r stack pointer in calling function *)
+           (pc: node)            (**r program point in calling function *)
+           (rs: regset),         (**r register state in calling function *)
+    stackframe.
 
-Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
-  match rl, vl with
-  | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
-  | _, _ => Regmap.init Vundef
-  end.
+Inductive state : Type :=
+| State:
+    forall (stack: list stackframe) (**r call stack *)
+           (f: function)            (**r current function *)
+           (sp: val)                (**r stack pointer *)
+           (pc: node)               (**r current program point in [c] *)
+           (rs: regset)             (**r register state *)
+           (m: mem),                (**r memory state *)
+    state
+| Callstate:
+    forall (stack: list stackframe) (**r call stack *)
+           (f: fundef)              (**r function to call *)
+           (args: list val)         (**r arguments to the call *)
+           (m: mem),                (**r memory state *)
+    state
+| Returnstate:
+    forall (stack: list stackframe) (**r call stack *)
+           (v: val)                 (**r return value for the call *)
+           (m: mem),                (**r memory state *)
+    state.
+
+Definition genv := Genv.t fundef unit.
 
 Section RELSEM.
 
+  Context (ge: genv).
+
+  Definition find_function
+             (ros: reg + ident) (rs: regset) : option fundef :=
+    match ros with
+    | inl r => Genv.find_funct ge rs#r
+    | inr symb =>
+      match Genv.find_symbol ge symb with
+      | None => None
+      | Some b => Genv.find_funct_ptr ge b
+      end
+    end.
+
+  Inductive step: state -> trace -> state -> Prop :=
+  | exec_bblock:
+      forall f pc bb cfi,
+      (fn_code f)!pc = Some (mk_bblock _ bb cfi) ->
+      step_instr_list (InstrState rs m) bb (InstrState rs' m')
+      step .
+
 End RELSEM.
 
 (*
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.