Work on semantics for RTLBlockInstr

4 files changed, 57 insertions, 22 deletions

diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index ecd7561..60b6948 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -36,7 +36,7 @@ RTLBlock
 ========
 |*)
 
-Definition bb := list instr.
+Definition bb := instr.
 
 Definition bblock := @bblock bb.
 Definition code := @code bb.
@@ -95,8 +95,8 @@ then show a transition from basic block to basic block.
       f.(fn_code)!pc = Some bb ->
       step_instr_list 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 rs' pr' m') bb.(bb_exit) t s' ->
-      step (State s f sp pc rs pr m) t s'
+      step_cf_instr ge (State s f sp pc nil rs' pr' m') bb.(bb_exit) t s' ->
+      step (State s f sp pc nil rs pr m) t s'
   | exec_function_internal:
     forall s f args m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
@@ -104,6 +104,7 @@ then show a transition from basic block to basic block.
            E0 (State s f
                      (Vptr stk Ptrofs.zero)
                      f.(fn_entrypoint)
+                         nil
                          (init_regs args f.(fn_params))
                          (PMap.init false)
                          m')
@@ -115,7 +116,7 @@ then show a transition from basic block to basic block.
   | 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 (rs#res <- vres) pr m).
+           E0 (State s f sp pc nil (rs#res <- vres) pr m).
 
 End RELSEM.
 
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index cd23da3..35ae03e 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -215,7 +215,7 @@ Section DEFINITION.
   Context {bblock_body: Type}.
 
   Record bblock : Type := mk_bblock {
-    bb_body: bblock_body;
+    bb_body: list bblock_body;
     bb_exit: cf_instr
   }.
 
@@ -263,6 +263,7 @@ 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: list bblock_body)
              (rs: regset)             (**r register state *)
              (pr: predset)            (**r predicate register state *)
              (m: mem),                (**r memory state *)
@@ -373,48 +374,48 @@ Step Control-Flow Instruction
     forall s f sp rs m res fd ros sig args pc pc' pr,
       find_function ros rs = Some fd ->
       funsig fd = sig ->
-      step_cf_instr (State s f sp pc rs pr m) (RBcall sig ros args res pc')
+      step_cf_instr (State s f sp pc nil 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 rs pr m)
+      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc nil 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,
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
       external_call ef ge vargs m t vres m' ->
-      step_cf_instr (State s f sp pc rs pr m) (RBbuiltin ef args res pc')
-         t (State s f sp pc' (regmap_setres res vres rs) pr m')
+      step_cf_instr (State s f sp pc nil rs pr m) (RBbuiltin ef args res pc')
+         t (State s f sp pc' nil (regmap_setres res vres rs) pr m')
   | exec_RBcond:
       forall s f sp rs m cond args ifso ifnot b pc pc' pr,
       eval_condition cond rs##args m = Some b ->
       pc' = (if b then ifso else ifnot) ->
-      step_cf_instr (State s f sp pc rs pr m) (RBcond cond args ifso ifnot)
-        E0 (State s f sp pc' rs pr m)
+      step_cf_instr (State s f sp pc nil rs pr m) (RBcond cond args ifso ifnot)
+        E0 (State s f sp pc' nil rs pr m)
   | exec_RBjumptable:
       forall s f sp rs m arg tbl n pc pc' pr,
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
-      step_cf_instr (State s f sp pc rs pr m) (RBjumptable arg tbl)
-        E0 (State s f sp pc' rs pr m)
+      step_cf_instr (State s f sp pc nil rs pr m) (RBjumptable arg tbl)
+        E0 (State s f sp pc' nil 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 rs pr m) (RBreturn or)
+      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc nil 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',
-      step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0
-                    (State s f sp pc' rs pr m)
+      step_cf_instr (State s f sp pc nil rs pr m) (RBgoto pc') E0
+                    (State s f sp pc' nil 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 rs pr m)
+      step_cf_instr (State s f sp pc nil rs pr m)
                     (if eval_predf pr p then cf1 else cf2) t st' ->
-      step_cf_instr (State s f sp pc rs pr m)
+      step_cf_instr (State s f sp pc nil 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 8434542..42d471c 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -25,8 +25,9 @@ RTLBlockgenproof
 
 Require compcert.backend.RTL.
 Require Import compcert.common.AST.
-Require Import compcert.lib.Maps.
 Require Import compcert.common.Errors.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.RTLBlockInstr.
@@ -81,7 +82,7 @@ transformation performs.  This should be proven from the validation of the
 transformation.
 |*)
 
-Inductive transl_code_spec (c: RTL.code) (tc: code) :=
+Variant transl_code_spec (c: RTL.code) (tc: code) :=
 | transl_code_standard_bb :
   forall x x' i i',
     c ! x = Some i ->
@@ -128,9 +129,41 @@ Section CORRECTNESS.
 
   Context (TRANSL : match_prog prog tprog).
 
+  Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
+  Let tge : genv := Globalenvs.Genv.globalenv tprog.
+
+  Lemma symbols_preserved:
+    forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+  Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
+
+  Lemma senv_preserved:
+    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+  Proof using TRANSL. intros; eapply (Genv.senv_transf_partial TRANSL). Qed.
+  #[local] Hint Resolve senv_preserved : rtlgp.
+
+  Lemma transl_initial_states :
+    forall s1 : Smallstep.state (RTL.semantics prog),
+      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.
+
+  Lemma transl_final_states :
+    forall (s1 : Smallstep.state (RTL.semantics prog))
+           (s2 : Smallstep.state (semantics tprog))
+           (r : Integers.Int.int),
+      match_states s1 s2 ->
+      Smallstep.final_state (RTL.semantics prog) s1 r ->
+      Smallstep.final_state (semantics tprog) s2 r.
+  Proof. Admitted.
+
   Theorem transf_program_correct:
     Smallstep.forward_simulation (RTL.semantics prog)
                                  (RTLBlock.semantics tprog).
-  Proof. Admitted.
+  Proof.
+    eapply Smallstep.forward_simulation_plus.
+    apply senv_preserved.
+    admit.
+    eauto using transl_final_states.
 
 End CORRECTNESS.
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index e0f657c..a36177e 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 (list instr)).
+Definition bb := list (list instr).
 
 Definition bblock := @bblock bb.
 Definition code := @code bb.