Fix translation passes with new semantics

5 files changed, 75 insertions, 72 deletions

diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v
index 3b82b29..886c23d 100644
--- a/src/hls/RICtransf.v
+++ b/src/hls/RICtransf.v
@@ -49,11 +49,10 @@ Fixpoint existsb_val {A B} (f: A -> option B) (l : list A) : option B :=
       end
   end.
 
-Definition includes_setpred (bb: list (list instr)) :=
-  existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end)) bb.
+Definition includes_setpred (bb: bb) :=
+  existsb_val (existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end))) bb.
 
-Definition add_bb (should_split: bool) (i: list (list instr))
-           (bbc: list (list (list instr)) * list (list (list instr))) :=
+Definition add_bb (should_split: bool) (i: bb) (bbc: list bb * list bb) :=
   match bbc with
   | (a, b) => if should_split then (a, i::b) else (i::a, b)
   end.
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index b9e9914..19ac4f5 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -93,9 +93,10 @@ function.
     | exec_bblock:
       forall s f sp pc rs rs' m m' bb pr pr' t state,
         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_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 state ->
-        step (State s f sp pc rs pr m) E0 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) ->
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index b191c09..7931874 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -30,6 +30,7 @@ Require Import compcert.common.Globalenvs.
 Require Import compcert.lib.Maps.
 Require Import compcert.backend.Registers.
 Require compcert.common.Smallstep.
+Require Import compcert.common.Events.
 
 Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.RTLBlockInstr.
@@ -94,23 +95,28 @@ transformation.
 This also specifies ``x'`` relative to x given the code.
 |*)
 
-Variant transl_code_spec (c: RTL.code) (tc: code) (x x': node): Prop :=
+Variant transl_code_spec (c: RTL.code) (tc: code) (x x': node) (i: RTL.instruction) (i': instr): Prop :=
 | transl_code_standard_bb :
-  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 x x'
+    transl_code_spec c tc x x' i i'
 | transl_code_standard_cf :
-  forall i i' il,
+  forall 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 x x'
+    transl_code_spec c tc x x' i i'
 .
 
+Section CORRECTNESS.
+
+  Context (prog : RTL.program).
+  Context (tprog : RTLBlock.program).
+
+  Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
+  Let tge : genv := Globalenvs.Genv.globalenv tprog.
+
 (*|
 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
@@ -122,57 +128,59 @@ It doesn't have to find the value because it's given as an input, and the
 finding is actually done at that higher level already.
 |*)
 
-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 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)).
+  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 res f tf sp pc pc' rs i i'
+        (TF: transl_function f = OK tf)
+        (TF: find_instr_spec tf.(fn_code) pc i pc' i')
+        (PC: transl_code_spec f.(RTL.fn_code) tf.(fn_code) pc pc' i i'),
+        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``.
+Initially, the idea was to define the ``match_states`` predicate normally to
+defines how to find the correct ``bb`` that should be executed, as well as the
+value of ``pc``.  However, this does not quite work when proving the equivalence
+of the translation from ``RTL`` to ``RTLBlock``, because one cannot match one
+transition to a transition in RTLBlock.  The alternative to this is to include a
+proof inside of the ``match_states`` that shows that the execution from the
+``pc`` of the start of the basic block to the current point is the same as the
+whole execution (in one big step) of the basic block.
 |*)
 
-Variant match_states : RTL.state -> RTLBlock.state -> Prop :=
-| match_state :
-  forall stk stk' f tf sp pc rs m pc' bb
-         (TF: transl_function f = OK tf)
-         (PC: transl_code_spec f.(RTL.fn_code) tf.(fn_code) pc pc')
-         (STK: Forall2 match_stackframe stk stk')
-         (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 (PMap.init false) m)
-| match_callstate :
-  forall cs cs' f tf args m
-    (TF: transl_fundef f = OK tf)
-    (STK: Forall2 match_stackframe cs cs'),
-    match_states (RTL.Callstate cs f args m) (Callstate cs' tf args m)
-| match_returnstate :
-  forall cs cs' v m
-    (STK: Forall2 match_stackframe cs cs'),
-    match_states (RTL.Returnstate cs v m) (Returnstate cs' v 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.
-
-Section CORRECTNESS.
-
-  Context (prog : RTL.program).
-  Context (tprog : RTLBlock.program).
+  Variant match_states : option bb -> RTL.state -> RTLBlock.state -> Prop :=
+    | match_state :
+      forall stk stk' f tf sp pc rs m rs' m' pc0 bb i i' b rs0 m0
+        (TF: transl_function f = OK tf)
+        (TF: find_instr_spec tf.(fn_code) pc i pc0 i')
+        (PC: transl_code_spec f.(RTL.fn_code) tf.(fn_code) pc pc0 i i')
+        (STK: Forall2 match_stackframe stk stk')
+        (STARSIMU: Smallstep.star RTL.step ge (RTL.State stk f sp pc0 rs0 m0)
+                                  E0 (RTL.State stk f sp pc rs m))
+        (BB: match_bblock tf.(fn_code) pc pc0 bb),
+        match_states (Some b) (RTL.State stk f sp pc rs m)
+                     (State stk' tf sp pc0 rs' (PMap.init false) m')
+    | match_callstate :
+      forall cs cs' f tf args m
+        (TF: transl_fundef f = OK tf)
+        (STK: Forall2 match_stackframe cs cs'),
+        match_states None (RTL.Callstate cs f args m) (Callstate cs' tf args m)
+    | match_returnstate :
+      forall cs cs' v m
+        (STK: Forall2 match_stackframe cs cs'),
+        match_states None (RTL.Returnstate cs v m) (Returnstate cs' v 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.
 
   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.
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.
 
diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v
index a104056..49ee6e7 100644
--- a/src/hls/RTLParFUgen.v
+++ b/src/hls/RTLParFUgen.v
@@ -134,7 +134,7 @@ Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr))
   | None => ((cycle + 1)%positive, curr :: bb)
   end.
 
-Definition transl_bb (res: resources) (bb: list RTLPar.bb): Errors.res RTLParFU.bblock_body :=
+Definition transl_bb (res: resources) (bb: RTLPar.bb): Errors.res RTLParFU.bblock_body :=
   do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb;
   let (li, tr) := litr in
   OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)).