Add semantics for RTLBlock

1 files changed, 67 insertions, 5 deletions

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.
 
 (*