Remove "active_call" from HTL semantics

added previously to support the fork/wait/join HTL instructions which
have since been removed

2 files changed, 24 insertions, 28 deletions

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 8474878..06ad26a 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -114,15 +114,12 @@ Definition find_module (i: ident) (ge : genv) : option fundef :=
    | Some b => Globalenvs.Genv.find_funct_ptr ge b
    end.
 
-Inductive active_call : Type :=
-  | ActiveCall (m : ident) (args : list value).
 
 Inductive stackframe : Type :=
   Stackframe :
     forall  (res : reg)
             (m : module)
             (st : node)
-            (forked_modules : list active_call)
             (reg_assoc : Verilog.assocmap_reg)
             (arr_assoc : Verilog.assocmap_arr),
       stackframe.
@@ -132,7 +129,6 @@ Inductive state : Type :=
     forall (stack : list stackframe)
            (m : module)
            (st : node)
-           (forked_modules : list active_call)
            (reg_assoc : Verilog.assocmap_reg)
            (arr_assoc : Verilog.assocmap_arr), state
 | Returnstate :
@@ -149,7 +145,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       asr asa
       basr1 basa1 nasr1 nasa1
       basr2 basa2 nasr2 nasa2
-      calls asr' asa'
+      asr' asa'
       f pstval,
       asr!(mod_reset m) = Some (ZToValue 0) ->
       asr!(mod_finish m) = Some (ZToValue 0) ->
@@ -173,26 +169,26 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       asa' = Verilog.merge_arrs nasa2 basa2 ->
       asr'!(m.(mod_st)) = Some (posToValue pstval) ->
       Z.pos pstval <= Integers.Int.max_unsigned ->
-      step g (State sf m st calls asr asa) Events.E0 (State sf m pstval calls asr' asa')
+      step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
 | step_finish :
-    forall g m st calls asr asa retval sf,
+    forall g m st asr asa retval sf,
     asr!(m.(mod_finish)) = Some (ZToValue 1) ->
     asr!(m.(mod_return)) = Some retval ->
-    step g (State sf m st calls asr asa) Events.E0 (Returnstate sf retval)
+    step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
 | step_call :
     forall g m args res,
       step g (Callstate res m args) Events.E0
-           (State res m m.(mod_entrypoint) nil
+           (State res m m.(mod_entrypoint)
              (AssocMap.set (mod_reset m) (ZToValue 0)
               (AssocMap.set (mod_finish m) (ZToValue 0)
                (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint))
                 (init_regs args m.(mod_params)))))
              (empty_stack m))
 | step_return :
-    forall g m calls asr asa i r sf pc mst,
+    forall g m asr asa i r sf pc mst,
       mst = mod_st m ->
-      step g (Returnstate (Stackframe r m pc calls asr asa :: sf) i) Events.E0
-           (State sf m pc calls ((asr # mst <- (posToValue pc)) # r <- i) asa).
+      step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
+           (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa).
 Hint Constructors step : htl.
 
 Inductive initial_state (p: program): state -> Prop :=
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 8c2d4af..a486897 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -54,8 +54,8 @@ Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
 Hint Constructors match_assocmaps : htlproof.
 
 Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
-  forall st calls asa asr res,
-  s = HTL.State res m st calls asa asr ->
+  forall st asa asr res,
+  s = HTL.State res m st asa asr ->
   asa!(m.(HTL.mod_st)) = Some (posToValue st).
 Hint Unfold state_st_wf : htlproof.
 
@@ -110,10 +110,10 @@ Inductive match_constants : HTL.module -> assocmap -> Prop :=
       match_constants m asr.
 
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall asa asr sf f sp sp' rs mem m st calls res
+| match_state : forall asa asr sf f sp sp' rs mem m st res
     (MASSOC : match_assocmaps f rs asr)
     (TF : tr_module f m)
-    (WF : state_st_wf m (HTL.State res m st calls asr asa))
+    (WF : state_st_wf m (HTL.State res m st asr asa))
     (MF : match_frames sf res)
     (MARR : match_arrs m f sp mem asa)
     (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
@@ -122,7 +122,7 @@ Inductive match_states : RTL.state -> HTL.state -> Prop :=
     (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem)
     (CONST : match_constants m asr),
     match_states (RTL.State sf f sp st rs mem)
-                 (HTL.State res m st calls asr asa)
+                 (HTL.State res m st asr asa)
 | match_returnstate :
     forall
       v v' stack mem res
@@ -305,7 +305,7 @@ Ltac inv_state :=
       inversion TF;
       match goal with
         TC : forall _ _,
-          Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _,
+          Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _ _,
         H : Maps.PTree.get _ _ = Some _ |- _ =>
         apply TC in H; inversion H;
         match goal with
@@ -593,8 +593,8 @@ Section CORRECTNESS.
         end.
 
   Lemma eval_cond_correct :
-    forall stk f sp pc rs m res ml st calls asr asa e b f' s s' args i cond,
-      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st calls asr asa) ->
+    forall stk f sp pc rs m res ml st asr asa e b f' s s' args i cond,
+      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
       (forall v, In v args -> Ple v (RTL.max_reg_function f)) ->
       Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b ->
       translate_condition cond args s = OK e s' i ->
@@ -724,8 +724,8 @@ Section CORRECTNESS.
   Qed.
 
   Lemma eval_cond_correct' :
-    forall e stk f sp pc rs m res ml st calls asr asa v f' s s' args i cond,
-      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st calls asr asa) ->
+    forall e stk f sp pc rs m res ml st asr asa v f' s s' args i cond,
+      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
       (forall v, In v args -> Ple v (RTL.max_reg_function f)) ->
       Values.Val.of_optbool None = v ->
       translate_condition cond args s = OK e s' i ->
@@ -737,8 +737,8 @@ Section CORRECTNESS.
   Qed.
 
   Lemma eval_correct_Oshrximm :
-    forall s sp rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st calls n,
-      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st calls asr asa) ->
+    forall s sp rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st n,
+      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
       (RTL.fn_code f) ! pc = Some (RTL.Iop (Op.Oshrximm n) args res0 pc') ->
       Op.eval_operation ge sp (Op.Oshrximm n)
                         (List.map (fun r : BinNums.positive =>
@@ -802,8 +802,8 @@ Section CORRECTNESS.
   Admitted.
 
   Lemma eval_correct :
-    forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st calls,
-      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st calls asr asa) ->
+    forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st ,
+      match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
       (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') ->
       Op.eval_operation ge sp op
                         (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
@@ -1022,10 +1022,10 @@ Section CORRECTNESS.
    *)
 
   Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
-    forall m asr asa fin rtrn st calls stmt trans res,
+    forall m asr asa fin rtrn st stmt trans res,
       tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans ->
       exists asr' asa',
-        HTL.step tge (HTL.State res m st calls asr asa) Events.E0 (HTL.State res m st calls asr' asa').
+        HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa').
 
   Opaque combine.