From 24afca4d2800afbcdd80ddf49faaa0b2751c1a77 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 22 Jan 2021 14:48:26 +0000
Subject: Add semantics for RTLBlock

---
 src/hls/RTLBlock.v      | 72 +++++++++++++++++++++++++++++++++++++++++++++----
 src/hls/RTLBlockInstr.v |  8 +-----
 2 files changed, 68 insertions(+), 12 deletions(-)

(limited to 'src/hls')

diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index a8efa33..4a42e7e 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -70,6 +70,14 @@ Inductive state : Type :=
            (rs: regset)             (**r register state *)
            (m: mem),                (**r memory state *)
     state
+| Block:
+    forall (stack: list stackframe) (**r call stack *)
+           (f: function)            (**r current function *)
+           (sp: val)                (**r stack pointer *)
+           (cfi: cf_instr)          (**r The control flow instruction to execute. *)
+           (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 *)
@@ -101,11 +109,65 @@ Section RELSEM.
 
   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 .
-
+      forall stack f sp pc rs m rs' m' bb cfi,
+      (fn_code f)!pc = Some (mk_bblock bb cfi) ->
+      step_instr_list _ ge sp (InstrState rs m) bb (InstrState rs' m') ->
+      step (State stack f sp pc rs m) E0 (Block stack f sp cfi rs' m')
+  | exec_RBcall:
+      forall s f sp rs m res fd ros sig args pc',
+      find_function ros rs = Some fd ->
+      funsig fd = sig ->
+      step (Block s f sp (RBcall sig ros args res pc') rs m)
+           E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m)
+  | exec_RBtailcall:
+      forall s f stk rs m sig ros args fd m',
+      find_function ros rs = Some fd ->
+      funsig fd = sig ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      step (Block s f (Vptr stk Ptrofs.zero) (RBtailcall sig ros args) rs m)
+        E0 (Callstate s fd rs##args m')
+  | exec_RBbuiltin:
+      forall s f sp rs m ef args res pc' vargs t vres m',
+      eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
+      external_call ef ge vargs m t vres m' ->
+      step (Block s f sp (RBbuiltin ef args res pc') rs m)
+         t (State s f sp pc' (regmap_setres res vres rs) m')
+  | exec_RBcond:
+      forall s f sp rs m cond args ifso ifnot b pc',
+      eval_condition cond rs##args m = Some b ->
+      pc' = (if b then ifso else ifnot) ->
+      step (Block s f sp (RBcond cond args ifso ifnot) rs m)
+        E0 (State s f sp pc' rs m)
+  | exec_RBjumptable:
+      forall s f sp rs m arg tbl n pc',
+      rs#arg = Vint n ->
+      list_nth_z tbl (Int.unsigned n) = Some pc' ->
+      step (Block s f sp (RBjumptable arg tbl) rs m)
+        E0 (State s f sp pc' rs m)
+  | exec_Ireturn:
+      forall s f stk rs m or m',
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      step (Block s f (Vptr stk Ptrofs.zero) (RBreturn or) rs m)
+        E0 (Returnstate s (regmap_optget or Vundef rs) m')
+  | exec_function_internal:
+      forall s f args m m' stk,
+      Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
+      step (Callstate s (Internal f) args m)
+        E0 (State s
+                  f
+                  (Vptr stk Ptrofs.zero)
+                  f.(fn_entrypoint)
+                  (init_regs args f.(fn_params))
+                  m')
+  | exec_function_external:
+      forall s ef args res t m m',
+      external_call ef ge args m t res m' ->
+      step (Callstate s (External ef) args m)
+         t (Returnstate s res m')
+  | exec_return:
+      forall res f sp pc rs s vres m,
+      step (Returnstate (Stackframe res f sp pc rs :: s) vres m)
+        E0 (State s f sp pc (rs#res <- vres) m).
 End RELSEM.
 
 (*
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index f9d1073..a3f058a 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -47,7 +47,7 @@ Inductive cf_instr : Type :=
 
 Record bblock (bblock_body : Type) : Type := mk_bblock {
     bb_body: bblock_body;
-    bb_exit: option cf_instr
+    bb_exit: cf_instr
   }.
 Arguments mk_bblock [bblock_body].
 Arguments bb_body [bblock_body].
@@ -102,10 +102,6 @@ Inductive instr_state : Type :=
            (m: mem),
     instr_state.
 
-Inductive cf_instr_state : Type :=
-| CfInstrState:
-    forall ()
-
 Section RELSEM.
 
   Context (fundef: Type).
@@ -149,6 +145,4 @@ Section RELSEM.
         forall state,
         step_instr_list state nil state.
 
-  Inductive step_cf_instr:
-
 End RELSEM.
-- 
cgit