Add basic blocks to the stackframe

5 files changed, 54 insertions, 32 deletions

diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 2c9d8ae..fbd3222 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -68,6 +68,9 @@ Instruction list step
 The ``step_instr_list`` definition describes the execution of a list of
 instructions in one big step, inductively traversing the list of instructions
 and applying the ``step_instr``.
+
+This is simply using the high-level function ``step_list``, which is a general
+function that can execute lists of things, given their execution rule.
 |*)
 
   Definition step_instr_list := step_list (step_instr ge).
@@ -77,7 +80,13 @@ Top-level step
 --------------
 
 The step function itself then uses this big step of the list of instructions to
-then show a transition from basic block to basic block.
+then show a transition from basic block to basic block.  The one particular
+aspect of this is that the basic block is also part of the state, which has to
+be correctly set during the execution of the function.  Function calls and
+function returns then also need to set the basic block properly.  This means
+that the basic block of the returning function also needs to be stored in the
+stackframe, as that is the only assumption one can make when returning from a
+function.
 |*)
 
   Variant step: state -> trace -> state -> Prop :=
@@ -106,9 +115,9 @@ then show a transition from basic block to basic block.
       step (Callstate s (External ef) args m)
            t (Returnstate s res m')
   | 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).
+    forall res f sp pc rs s vres m pr bb,
+      step (Returnstate (Stackframe res f sp pc bb rs pr :: s) vres m)
+           E0 (State s f sp pc bb (rs#res <- vres) pr m).
 
 End RELSEM.
 
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index f91c5c0..f3df2c4 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -245,6 +245,7 @@ Section DEFINITION.
            (f: function)         (**r calling function *)
            (sp: val)             (**r stack pointer in calling function *)
            (pc: node)            (**r program point in calling function *)
+           (bb: bblock)
            (rs: regset)          (**r register state in calling function *)
            (pr: predset),        (**r predicate state of the calling
                                         function *)
@@ -383,44 +384,51 @@ Step Control-Flow Instruction
 
   Inductive step_cf_instr: state -> trace -> state -> Prop :=
   | exec_RBcall:
-    forall s f sp rs m res fd ros sig args pc pc' pr,
+    forall s f sp rs m res fd ros sig args pc pc' pr bb,
       find_function ros rs = Some fd ->
       funsig fd = sig ->
-      step_cf_instr (State s f sp pc (mk_bblock nil (RBcall sig ros args res pc')) rs pr m)
-                    E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m)
+      f.(fn_code) ! pc' = Some bb ->
+      step_cf_instr
+        (State s f sp pc (mk_bblock nil (RBcall sig ros args res pc')) rs pr m)
+        E0 (Callstate (Stackframe res f sp pc' bb rs pr :: s) fd rs##args m)
   | exec_RBtailcall:
     forall s f stk rs m sig ros args fd m' pc pr,
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc (mk_bblock nil (RBtailcall sig ros args)) rs pr m)
-                    E0 (Callstate s fd rs##args m')
+      step_cf_instr
+        (State s f (Vptr stk Ptrofs.zero) pc (mk_bblock nil (RBtailcall sig ros args)) rs pr m)
+        E0 (Callstate s fd rs##args m')
   | exec_RBbuiltin:
     forall s f sp rs m ef args res pc' vargs t vres m' pc pr bb,
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
       external_call ef ge vargs m t vres m' ->
       f.(fn_code) ! pc' = Some bb ->
-      step_cf_instr (State s f sp pc (mk_bblock nil (RBbuiltin ef args res pc')) rs pr m)
-                    t (State s f sp pc' bb (regmap_setres res vres rs) pr m')
+      step_cf_instr
+        (State s f sp pc (mk_bblock nil (RBbuiltin ef args res pc')) rs pr m)
+        t (State s f sp pc' bb (regmap_setres res vres rs) pr m')
   | exec_RBcond:
     forall s f sp rs m cond args ifso ifnot b pc pc' pr bb,
       eval_condition cond rs##args m = Some b ->
       pc' = (if b then ifso else ifnot) ->
       f.(fn_code) ! pc' = Some bb ->
-      step_cf_instr (State s f sp pc (mk_bblock nil (RBcond cond args ifso ifnot)) rs pr m)
-                    E0 (State s f sp pc' bb rs pr m)
+      step_cf_instr
+        (State s f sp pc (mk_bblock nil (RBcond cond args ifso ifnot)) rs pr m)
+        E0 (State s f sp pc' bb rs pr m)
   | exec_RBjumptable:
     forall s f sp rs m arg tbl n pc pc' pr bb,
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
       f.(fn_code) ! pc' = Some bb ->
-      step_cf_instr (State s f sp pc (mk_bblock nil (RBjumptable arg tbl)) rs pr m)
-                    E0 (State s f sp pc' bb rs pr m)
+      step_cf_instr
+        (State s f sp pc (mk_bblock nil (RBjumptable arg tbl)) rs pr m)
+        E0 (State s f sp pc' bb rs pr m)
   | exec_RBreturn:
     forall s f stk rs m or pc m' pr,
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc (mk_bblock nil (RBreturn or)) rs pr m)
-                    E0 (Returnstate s (regmap_optget or Vundef rs) m')
+      step_cf_instr
+        (State s f (Vptr stk Ptrofs.zero) pc (mk_bblock nil (RBreturn or)) rs pr m)
+        E0 (Returnstate s (regmap_optget or Vundef rs) m')
   | exec_RBgoto:
     forall s f sp pc rs pr m pc' bb,
       f.(fn_code) ! pc' = Some bb ->
@@ -428,8 +436,12 @@ Step Control-Flow Instruction
                     (State s f sp pc' bb rs pr m)
   | exec_RBpred_cf:
     forall s f sp pc rs pr m cf1 cf2 st' p t,
-      step_cf_instr (State s f sp pc (mk_bblock nil (if eval_predf pr p then cf1 else cf2)) rs pr m) t st' ->
-      step_cf_instr (State s f sp pc (mk_bblock nil (RBpred_cf p cf1 cf2)) rs pr m)
-                     t st'.
+      step_cf_instr
+        (State s f sp pc
+               (mk_bblock nil (if eval_predf pr p then cf1 else cf2))
+               rs pr m) t st' ->
+      step_cf_instr
+        (State s f sp pc (mk_bblock nil (RBpred_cf p cf1 cf2)) rs pr m)
+        t st'.
 
 End RELSEM.
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index f870278..f57af34 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -87,15 +87,15 @@ Variant transl_code_spec (c: RTL.code) (tc: code) :=
   forall x x' i i',
     c ! x = Some i ->
     find_instr_spec tc x i x' i' ->
-    check_instr x i i' = true ->
+    Is_true (check_instr x i i') ->
     transl_code_spec c tc
 | transl_code_standard_cf :
   forall x x' i i' il,
     c ! x = Some i ->
     tc ! x' = Some il ->
     find_instr_spec tc x i x' i' ->
-    check_cf_instr_body i i' = true ->
-    check_cf_instr i il.(bb_exit) = true ->
+    Is_true (check_cf_instr_body i i') ->
+    Is_true (check_cf_instr i il.(bb_exit)) ->
     transl_code_spec c tc
 .
 
@@ -112,12 +112,12 @@ Variant match_stackframe : RTL.stackframe -> stackframe -> Prop :=
 
 Variant match_states : RTL.state -> RTLBlock.state -> Prop :=
 | match_state :
-  forall stk stk' f tf sp pc rs m pc' ps
+  forall stk stk' f tf sp pc rs m pc' ps bb
          (TF: transl_function f = OK tf)
          (PC: find_block_spec tf.(fn_code) pc pc')
          (STK: Forall2 match_stackframe stk stk'),
     match_states (RTL.State stk f sp pc rs m)
-                 (State stk' tf sp pc' nil rs ps m).
+                 (State stk' tf sp pc' bb rs ps m).
 
 Definition match_prog (p: RTL.program) (tp: RTLBlock.program) :=
   Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index a3631ec..61e968e 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -55,17 +55,18 @@ Section RELSEM.
       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_cf_instr ge (State s f sp pc nil rs' pr' m') bb.(bb_exit) t s' ->
+      step_cf_instr ge (State s f sp pc (mk_bblock nil bb.(bb_exit)) rs' pr' m') t s' ->
       step (State s f sp pc bb rs pr m) t s'
   | exec_function_internal:
-    forall s f args m m' stk,
+    forall s f args m m' stk bb,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
+      f.(fn_code) ! (f.(fn_entrypoint)) = Some bb ->
       step (Callstate s (Internal f) args m)
         E0 (State s
                   f
                   (Vptr stk Ptrofs.zero)
                   f.(fn_entrypoint)
-                  nil
+                  bb
                   (init_regs args f.(fn_params))
                   (PMap.init false)
                   m')
@@ -75,9 +76,9 @@ Section RELSEM.
       step (Callstate s (External ef) args m)
          t (Returnstate s res m')
   | 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).
+    forall res f sp pc rs s vres m pr bb,
+      step (Returnstate (Stackframe res f sp pc bb rs pr :: s) vres m)
+        E0 (State s f sp pc bb (rs#res <- vres) pr m).
 
 End RELSEM.
 
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 215aef5..fac6455 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -631,7 +631,7 @@ Qed.
 
 Lemma step_instr_seq_matches :
   forall a ge sp st st',
-  step_instr_seq ge sp st a st' ->
+   step_instr_seq ge sp st a st' ->
   forall tst, match_states st tst ->
               exists tst', step_instr_seq ge sp tst a tst'
                            /\ match_states st' tst'.