Add intermediate files

4 files changed, 143 insertions, 78 deletions

diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index fbd3222..d8c119c 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -91,16 +91,19 @@ function.
 
   Variant step: state -> trace -> state -> Prop :=
   | exec_bblock:
-    forall s f sp pc rs rs' m m' t s' bb pr pr',
-      f.(fn_code)!pc = Some bb ->
-      step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body)
+    forall s f sp pc rs rs' m m' bb pr pr',
+      step_instr_list sp (mk_instr_state rs pr m) bb
                          (mk_instr_state rs' pr' m') ->
-      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'
+      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
   | exec_function_internal:
-    forall s f args m m' stk bb,
+    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 bb ->
+      f.(fn_code) ! (f.(fn_entrypoint)) = Some (mk_bblock bb cf) ->
       step (Callstate s (Internal f) args m)
            E0 (State s f
                      (Vptr stk Ptrofs.zero)
@@ -115,9 +118,9 @@ function.
       step (Callstate s (External ef) args m)
            t (Returnstate s res m')
   | exec_return:
-    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).
+    forall res f sp pc rs s vres m pr,
+      step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
+           E0 (JumpState s f sp pc (rs#res <- vres) pr m).
 
 End RELSEM.
 
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index f3df2c4..b6545ee 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -28,8 +28,6 @@ therefore at the top-level of the instructions.
 .. coq:: none
 |*)
 
-Require Import Coq.micromega.Lia.
-
 Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Events.
@@ -245,7 +243,6 @@ 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 *)
@@ -255,7 +252,41 @@ Section DEFINITION.
 State Definition
 ----------------
 
-Definition of the ``state`` type, which is used by the ``step`` functions.
+Definition of the ``state`` type, which is used by the ``step`` functions.  This
+state definition is a bit strange when compared to other state definitions in
+CompCert.  The main reason for that is the inclusion of ``list bblock_body``,
+even though theoretically this is not necessary as one can use the program
+counter ``pc`` to index the current function and find the whole basic block that
+needs to be executed.
+
+However, the state definition needs to be viable for a translation from ``RTL``
+into ``RTLBlock``, as well as larger grained optimisations such as scheduling.
+The proof of semantic correctness of the first translation requires that the
+instructions are executed one after another.  As it is not possible to perform
+multiple steps in the input language for one step in the output language,
+without showing that the ``state`` is reduced by some measure, the current basic
+block needs to be present inside of the state.
+
+The ideal solution to this would be to have two indices, one which finds the
+current basic block to execute, and another which keeps track of the offset.
+This would make the basic block generation proof much simpler, because there is
+a direct correlation between the program counter in ``RTL`` and the program
+counter in addition to the offset in ``RTLBlock``.
+
+On the other hand, the best solution for proving scheduling correct would be a
+pure big step style semantics for executing the basic block.  This would not
+need to include anything relating to the basic block in the state, as it would
+execute each basic block at a time.  Referring to each instruction individually
+becomes impossible then, because the state transition skips over it directly.
+
+Finally, the way the state is actually implemented is using a mixture of the two
+methods above.  Instead of having two indices, the internal index is instead a
+list of remaining instructions to executed in the current block.  In case of
+transformations that need to reason about each instruction individually, the
+list of instructions will be reduced one instruction at a time.  However, in the
+case of transformations that only need to reason about basic blocks at a time
+will only use the fact that one can transform a list of instructions into a next
+state transition (``JumpState``).
 |*)
 
   Variant state : Type :=
@@ -264,12 +295,21 @@ Definition of the ``state`` type, which is used by the ``step`` functions.
              (f: function)            (**r current function *)
              (sp: val)                (**r stack pointer *)
              (pc: node)               (**r current program point in [c] *)
-             (il: bblock)   (**r basic block body that is
-                                 currently executing. *)
+             (il: list bblock_body)   (**r basic block body that is
+                                           currently executing. *)
              (rs: regset)             (**r register state *)
              (pr: predset)            (**r predicate register state *)
              (m: mem),                (**r memory state *)
         state
+    | JumpState:
+        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 *)
+               (pr: predset)            (**r predicate register state *)
+               (m: mem),                (**r memory state *)
+          state
     | Callstate:
       forall (stack: list stackframe) (**r call stack *)
              (f: fundef)              (**r function to call *)
@@ -382,66 +422,68 @@ Step Control-Flow Instruction
 =============================
 |*)
 
-  Inductive step_cf_instr: state -> trace -> state -> Prop :=
+  Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
   | exec_RBcall:
-    forall s f sp rs m res fd ros sig args pc pc' pr bb,
+    forall s f sp rs m res fd ros sig args pc pc' pr,
       find_function ros rs = Some fd ->
       funsig fd = sig ->
-      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)
+        (JumpState s f sp pc rs pr m) (RBcall sig ros args res pc')
+        E0 (Callstate (Stackframe res f sp pc' 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)
+        (JumpState s f (Vptr stk Ptrofs.zero) pc rs pr m)
+        (RBtailcall sig ros args)
         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,
+    forall s f sp rs m ef args res pc' vargs t vres m' pc pr bb' cf',
+      f.(fn_code)!pc' = Some (mk_bblock bb' cf') ->
       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')
+        (JumpState s f sp pc rs pr m) (RBbuiltin ef args res pc')
+        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,
+    forall s f sp rs m cond args ifso ifnot b pc pc' pr bb' cf',
+      f.(fn_code)!pc' = Some (mk_bblock bb' cf') ->
       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)
+        (JumpState s f sp pc rs pr m)
+        (RBcond cond args ifso ifnot)
+        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,
+    forall s f sp rs m arg tbl n pc pc' pr bb' cf',
+      f.(fn_code)!pc' = Some (mk_bblock bb' cf') ->
       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)
+        (JumpState s f sp pc rs pr m)
+        (RBjumptable arg tbl)
+        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)
+        (JumpState s f (Vptr stk Ptrofs.zero) pc rs pr m)
+        (RBreturn or)
         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 ->
-      step_cf_instr (State s f sp pc (mk_bblock nil (RBgoto pc')) rs pr m) E0
-                    (State s f sp pc' bb rs pr m)
+    forall s f sp pc rs pr m pc' bb' cf',
+      f.(fn_code)!pc' = Some (mk_bblock bb' cf') ->
+      step_cf_instr (JumpState s f sp pc rs pr m)
+                    (RBgoto pc') E0 (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' ->
+        (JumpState s f sp pc
+               rs pr m) (if eval_predf pr p then cf1 else cf2) t st' ->
       step_cf_instr
-        (State s f sp pc (mk_bblock nil (RBpred_cf p cf1 cf2)) rs pr m)
+        (JumpState s f sp pc rs pr m) (RBpred_cf p cf1 cf2)
         t st'.
 
 End RELSEM.
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index a0a1ee8..a77c791 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -63,12 +63,14 @@ then the equivalent control-flow instruction ending the basic block.
 
 Parameter find_block_spec : code -> node -> node -> Prop.
 
+Definition offset (pc pc': positive): nat := Pos.to_nat pc' - Pos.to_nat pc.
+
 Definition find_instr_spec (c: code) (n: node) (i: RTL.instruction)
            (n': node) (i': instr) :=
-    find_block_spec c n n'
-    /\ exists il,
+  find_block_spec c n n' /\
+  exists il,
       c ! n' = Some il
-      /\ nth_error il.(bb_body) (Pos.to_nat n - Pos.to_nat n')%nat = Some i'.
+      /\ nth_error il.(bb_body) (offset n n') = Some i'.
 
 (*|
 .. index::
@@ -80,49 +82,61 @@ Translation Specification
 This specification should describe the translation that the unverified
 transformation performs.  This should be proven from the validation of the
 transformation.
+
+This also specifies ``x'`` relative to x given the code.
 |*)
 
-Variant transl_code_spec (c: RTL.code) (tc: code) :=
+Variant transl_code_spec (c: RTL.code) (tc: code) (x x': node): Prop :=
 | transl_code_standard_bb :
-  forall x x' i i',
+  forall i i',
     c ! x = Some i ->
     find_instr_spec tc x i x' i' ->
     Is_true (check_instr x i i') ->
-    transl_code_spec c tc
+    transl_code_spec c tc x x'
 | transl_code_standard_cf :
-  forall x x' i i' il,
+  forall i i' il,
     c ! x = Some i ->
     tc ! x' = Some il ->
     find_instr_spec tc x i x' i' ->
     Is_true (check_cf_instr_body i i') ->
     Is_true (check_cf_instr i il.(bb_exit)) ->
-    transl_code_spec c tc
+    transl_code_spec c tc x x'
 .
 
-Lemma transl_function_correct :
-  forall f tf,
-    transl_function f = OK tf ->
-    transl_code_spec f.(RTL.fn_code) tf.(fn_code).
-Proof. Admitted.
+(*|
+Matches the basic block that should be present in the state.  This simulates the
+small step execution of the basic block from the big step semantics that are
+currently present.
+|*)
+
+Variant match_bblock (tc: code) (pc pc': node): list instr -> Prop :=
+| match_bblock_intro :
+  forall bb cf,
+    tc ! pc' = Some (mk_bblock bb cf) ->
+    match_bblock tc pc pc' (list_drop (offset pc pc') bb).
 
 Variant match_stackframe : RTL.stackframe -> stackframe -> Prop :=
 | match_stackframe_init :
-  forall a b,
-    match_stackframe a b.
+  forall res f tf sp pc pc' rs
+    (TF: transl_function f = OK tf)
+    (PC: transl_code_spec f.(RTL.fn_code) tf.(fn_code) pc pc'),
+    match_stackframe (RTL.Stackframe res f sp pc rs)
+                     (Stackframe res tf sp pc' rs (PMap.init false)).
+
+(*|
+The ``match_states`` predicate defines how to find the correct ``bb`` that
+should be executed, as well as the value of ``pc``.
+|*)
 
 Variant match_states : RTL.state -> RTLBlock.state -> Prop :=
 | match_state :
-  forall stk stk' f tf sp pc rs m pc' ps bb
+  forall stk stk' f tf sp pc rs m pc' bb
          (TF: transl_function f = OK tf)
-         (PC: find_block_spec tf.(fn_code) pc pc')
+         (PC: transl_code_spec f.(RTL.fn_code) tf.(fn_code) pc pc')
          (STK: Forall2 match_stackframe stk stk')
-         (BB: forall i bb',
-             f.(RTL.fn_code) ! pc = Some i ->
-             tf.(fn_code) ! pc' = Some bb' ->
-             list_drop (Pos.to_nat pc' - Pos.to_nat pc)%nat bb'.(bb_body) = i' :: bb
-         ),
+         (BB: match_bblock tf.(fn_code) pc pc' bb),
     match_states (RTL.State stk f sp pc rs m)
-                 (State stk' tf sp pc' bb rs ps m).
+                 (State stk' tf sp pc' bb rs (PMap.init false) 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.
@@ -151,7 +165,10 @@ Section CORRECTNESS.
       Smallstep.initial_state (RTL.semantics prog) s1 ->
       exists s2 : Smallstep.state (semantics tprog),
         Smallstep.initial_state (semantics tprog) s2 /\ match_states s1 s2.
-  Proof. Admitted.
+  Proof.
+    induction 1.
+
+    econstructor. simplify. econstructor.
 
   Lemma transl_final_states :
     forall (s1 : Smallstep.state (RTL.semantics prog))
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index 2c60116..d769b43 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -52,16 +52,19 @@ Section RELSEM.
 
   Inductive step: state -> trace -> state -> Prop :=
   | exec_bblock:
-    forall s (f: function) sp pc rs rs' m m' t s' bb pr pr',
-      f.(fn_code)!pc = Some bb ->
-      step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body)
+    forall s f sp pc rs rs' m m' bb pr pr',
+      step_instr_block sp (mk_instr_state rs pr m) bb
                           (mk_instr_state rs' pr' m') ->
-      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'
+      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
   | exec_function_internal:
-    forall s f args m m' stk bb,
+    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 bb ->
+      f.(fn_code) ! (f.(fn_entrypoint)) = Some (mk_bblock bb cf) ->
       step (Callstate s (Internal f) args m)
         E0 (State s
                   f
@@ -75,11 +78,11 @@ Section RELSEM.
     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')
+           t (Returnstate s res m')
   | exec_return:
-    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).
+    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).
 
 End RELSEM.