From 6f9d16bb67f32463d98771f3f155297c4ea4b3b7 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 23 Apr 2022 09:37:02 +0100
Subject: Fix translation passes with new semantics

---
 src/hls/RTLPar.v | 23 +++++++++--------------
 1 file changed, 9 insertions(+), 14 deletions(-)

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

diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index d769b43..e6aa002 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -30,7 +30,7 @@ Require Import compcert.verilog.Op.
 
 Require Import vericert.hls.RTLBlockInstr.
 
-Definition bb := list (list instr).
+Definition bb := list (list (list instr)).
 
 Definition bblock := @bblock bb.
 Definition code := @code bb.
@@ -50,27 +50,22 @@ Section RELSEM.
   Definition step_instr_seq := step_list step_instr_list.
   Definition step_instr_block := step_list step_instr_seq.
 
-  Inductive step: state -> trace -> state -> Prop :=
+  Variant step: state -> trace -> state -> Prop :=
   | exec_bblock:
-    forall s f sp pc rs rs' m m' bb pr pr',
-      step_instr_block sp (mk_instr_state rs pr m) bb
+    forall s f sp pc rs rs' m m' bb pr pr' state t,
+      f.(fn_code) ! pc = Some bb ->
+      step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body)
                           (mk_instr_state rs' pr' m') ->
-      step (State s f sp pc bb rs pr m) E0 (JumpState s f sp pc rs' pr' m')
-  | exec_jumpstate :
-    forall s f sp pc rs pr m block t st,
-      f.(fn_code) ! pc = Some block ->
-      step_cf_instr ge (JumpState s f sp pc rs pr m) block.(bb_exit) t st ->
-      step (JumpState s f sp pc rs pr m) t st
+      step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t state ->
+      step (State s f sp pc rs pr m) t state
   | exec_function_internal:
     forall s f args m m' stk bb cf,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
       f.(fn_code) ! (f.(fn_entrypoint)) = Some (mk_bblock bb cf) ->
       step (Callstate s (Internal f) args m)
-        E0 (State s
-                  f
+        E0 (State s f
                   (Vptr stk Ptrofs.zero)
                   f.(fn_entrypoint)
-                  bb
                   (init_regs args f.(fn_params))
                   (PMap.init false)
                   m')
@@ -82,7 +77,7 @@ Section RELSEM.
   | exec_return:
     forall res f sp pc rs s vres m pr,
       step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
-        E0 (State s f sp pc nil (rs#res <- vres) pr m).
+        E0 (State s f sp pc (rs#res <- vres) pr m).
 
 End RELSEM.
 
-- 
cgit