Define RTLPar semantics

These semantics are similar to the RTLBlock semantics, except that more
states are needed to reason about the parallel execution in multiple
cycles.

2 files changed, 85 insertions, 172 deletions

diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 23aa8c2..32d7674 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -186,89 +186,3 @@ Inductive final_state: state -> int -> Prop :=
 
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
-
-(*
-
-Inductive stackframe : Type :=
-  | Stackframe:
-      forall (res: reg)            (**r where to store the result *)
-             (f: function)         (**r calling function *)
-             (sp: val)             (**r stack pointer in calling function *)
-             (pc: node)            (**r program point in calling function *)
-             (rs: regset),         (**r register state in calling function *)
-      stackframe.
-
-Inductive cont : Type :=
-  | C
-  | N.
-
-Inductive state : Type :=
-  | State:
-      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 *)
-             (m: mem)                 (**r memory state *)
-             (bblock: bblock)         (**r bblock being executed *)
-             (c : cont),
-      state
-  | Callstate:
-      forall (stack: list stackframe) (**r call stack *)
-             (f: fundef)              (**r function to call *)
-             (args: list val)         (**r arguments to the call *)
-             (m: mem),                (**r memory state *)
-      state
-  | Returnstate:
-      forall (stack: list stackframe) (**r call stack *)
-             (v: val)                 (**r return value for the call *)
-             (m: mem),                (**r memory state *)
-      state.
-
-Section RELSEM.
-
-Variable ge: genv.
-
-Definition find_function
-      (ros: reg + ident) (rs: regset) : option fundef :=
-  match ros with
-  | inl r => Genv.find_funct ge rs#r
-  | inr symb =>
-      match Genv.find_symbol ge symb with
-      | None => None
-      | Some b => Genv.find_funct_ptr ge b
-      end
-  end.
-
-Inductive step : state -> trace -> state -> Prop :=
-  | exec_RBnop :
-      forall s f sp pc rs m ls ci,
-      step (State s f sp pc rs m (mk_bblock (RBnop :: ls) ci) C) E0
-           (State s f sp (Pos.succ pc) rs m (mk_bblock ls ci) C)
-  | exec_RBop :
-      forall s f sp pc rs m ls args op res ci v,
-      eval_operation ge sp op rs##args m = Some v ->
-      step (State s f sp pc rs m (mk_bblock (RBop op args res :: ls) ci) C) E0
-           (State s f sp (Pos.succ pc) rs m (mk_bblock ls ci) C)
-  | exec_RBload:
-      forall s f sp pc rs m chunk addr args dst a v ls ci,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.loadv chunk m a = Some v ->
-      step (State s f sp pc rs m (mk_bblock (RBload chunk addr args dst :: ls) ci) C)
-        E0 (State s f sp (Pos.succ pc) (rs#dst <- v) m (mk_bblock ls ci) C)
-  | exec_RBstore:
-      forall s f sp pc rs m chunk addr args src a m' ls ci,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.storev chunk m a rs#src = Some m' ->
-      step (State s f sp pc rs m (mk_bblock (RBstore chunk addr args src :: ls) ci) C)
-        E0 (State s f sp (Pos.succ pc) rs m' (mk_bblock ls ci) C)
-  | exec_RBcond:
-      forall s f sp pc rs m cond args ifso ifnot b pc',
-      eval_condition cond rs##args m = Some b ->
-      pc' = (if b then ifso else ifnot) ->
-      step (State s f sp pc rs m (mk_bblock nil (RBcond cond args ifso ifnot)) C)
-        E0 (State s f sp pc' rs m (mk_bblock nil (RBcond cond args ifso ifnot)) N)
-.
-
-End RELSEM.
-*)
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index 36431ae..af6b0ab 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -1,6 +1,6 @@
 (*
  * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com>
  *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
@@ -54,10 +54,7 @@ Definition funsig (fd: fundef) :=
 
 Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
   let max_body := fold_left (fun x l => fold_left max_reg_instr l x) bb.(bb_body) m in
-  match bb.(bb_exit) with
-  | Some e => max_reg_cfi max_body e
-  | None => max_body
-  end.
+  max_reg_cfi max_body bb.(bb_exit).
 
 Definition max_reg_function (f: function) :=
   Pos.max
@@ -96,6 +93,14 @@ Inductive state : Type :=
              (rs: regset)             (**r register state *)
              (m: mem),                (**r memory state *)
       state
+  | Block:
+      forall (stack: list stackframe) (**r call stack *)
+             (f: function)            (**r current function *)
+             (sp: val)                (**r stack pointer *)
+             (bb: bblock)             (**r current basic block *)
+             (rs: regset)             (**r register state *)
+             (m: mem),                (**r memory state *)
+      state
   | Callstate:
       forall (stack: list stackframe) (**r call stack *)
              (f: fundef)              (**r function to call *)
@@ -110,7 +115,7 @@ Inductive state : Type :=
 
 Section RELSEM.
 
-  Context (ge : genv).
+  Context (ge: genv).
 
   Definition find_function
              (ros: reg + ident) (rs: regset) : option fundef :=
@@ -123,92 +128,86 @@ Section RELSEM.
       end
     end.
 
-  Inductive step_instruction : state -> trace -> state -> Prop :=
-  | exec_Inop:
-      forall s f sp pc rs m pc',
-        (fn_code f)!pc = Some(RPnop pc') ->
-        step (State s f sp pc rs m)
-             E0 (State s f sp pc' rs m)
-  | exec_Iop:
-      forall s f sp pc rs m op args res pc' v,
-        (fn_code f)!pc = Some(Iop op args res pc') ->
-        eval_operation ge sp op rs##args m = Some v ->
-        step (State s f sp pc rs m)
-             E0 (State s f sp pc' (rs#res <- v) m)
-  | exec_Iload:
-      forall s f sp pc rs m chunk addr args dst pc' a v,
-        (fn_code f)!pc = Some(Iload chunk addr args dst pc') ->
-        eval_addressing ge sp addr rs##args = Some a ->
-        Mem.loadv chunk m a = Some v ->
-        step (State s f sp pc rs m)
-             E0 (State s f sp pc' (rs#dst <- v) m)
-  | exec_Istore:
-      forall s f sp pc rs m chunk addr args src pc' a m',
-        (fn_code f)!pc = Some(Istore chunk addr args src pc') ->
-        eval_addressing ge sp addr rs##args = Some a ->
-        Mem.storev chunk m a rs#src = Some m' ->
-        step (State s f sp pc rs m)
-             E0 (State s f sp pc' rs m')
-  | exec_Icall:
-      forall s f sp pc rs m sig ros args res pc' fd,
-        (fn_code f)!pc = Some(Icall sig ros args res pc') ->
-        find_function ros rs = Some fd ->
-        funsig fd = sig ->
-        step (State s f sp pc rs m)
-             E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m)
-  | exec_Itailcall:
-      forall s f stk pc rs m sig ros args fd m',
-        (fn_code f)!pc = Some(Itailcall sig ros args) ->
-        find_function ros rs = Some fd ->
-        funsig fd = sig ->
-        Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-        step (State s f (Vptr stk Ptrofs.zero) pc rs m)
-             E0 (Callstate s fd rs##args m')
-  | exec_Ibuiltin:
-      forall s f sp pc rs m ef args res pc' vargs t vres m',
-        (fn_code f)!pc = Some(Ibuiltin ef args res pc') ->
-        eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
-        external_call ef ge vargs m t vres m' ->
-        step (State s f sp pc rs m)
-             t (State s f sp pc' (regmap_setres res vres rs) m')
-  | exec_Icond:
-      forall s f sp pc rs m cond args ifso ifnot b pc',
-        (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
-        eval_condition cond rs##args m = Some b ->
-        pc' = (if b then ifso else ifnot) ->
-        step (State s f sp pc rs m)
-             E0 (State s f sp pc' rs m)
-  | exec_Ijumptable:
-      forall s f sp pc rs m arg tbl n pc',
-        (fn_code f)!pc = Some(Ijumptable arg tbl) ->
-        rs#arg = Vint n ->
-        list_nth_z tbl (Int.unsigned n) = Some pc' ->
-        step (State s f sp pc rs m)
-             E0 (State s f sp pc' rs m)
+  Inductive step: state -> trace -> state -> Prop :=
+  | exec_bblock_enter:
+      forall stack f sp pc rs m rs' m' bb,
+      (fn_code f)!pc = Some bb ->
+      step (State stack f sp pc rs m) E0 (Block stack f sp bb rs' m')
+  | exec_bblock_instr_cons:
+      forall sp rs m rs' m' stack f bb bbs cfi,
+      step_instr_list _ ge sp (InstrState rs m) bb (InstrState rs' m') ->
+      step (Block stack f sp (mk_bblock (bb :: bbs) cfi) rs m) E0
+           (Block stack f sp (mk_bblock bbs cfi) rs' m')
+  | exec_RBcall:
+      forall s f sp rs m res fd ros sig args pc',
+      find_function ros rs = Some fd ->
+      funsig fd = sig ->
+      step (Block s f sp (mk_bblock nil (RBcall sig ros args res pc')) rs m)
+           E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m)
+  | exec_RBtailcall:
+      forall s f stk rs m sig ros args fd m',
+      find_function ros rs = Some fd ->
+      funsig fd = sig ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      step (Block s f (Vptr stk Ptrofs.zero) (mk_bblock nil (RBtailcall sig ros args)) rs m)
+        E0 (Callstate s fd rs##args m')
+  | exec_RBbuiltin:
+      forall s f sp rs m ef args res pc' vargs t vres m',
+      eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
+      external_call ef ge vargs m t vres m' ->
+      step (Block s f sp (mk_bblock nil (RBbuiltin ef args res pc')) rs m)
+         t (State s f sp pc' (regmap_setres res vres rs) m')
+  | exec_RBcond:
+      forall s f sp rs m cond args ifso ifnot b pc',
+      eval_condition cond rs##args m = Some b ->
+      pc' = (if b then ifso else ifnot) ->
+      step (Block s f sp (mk_bblock nil (RBcond cond args ifso ifnot)) rs m)
+        E0 (State s f sp pc' rs m)
+  | exec_RBjumptable:
+      forall s f sp rs m arg tbl n pc',
+      rs#arg = Vint n ->
+      list_nth_z tbl (Int.unsigned n) = Some pc' ->
+      step (Block s f sp (mk_bblock nil (RBjumptable arg tbl)) rs m)
+        E0 (State s f sp pc' rs m)
   | exec_Ireturn:
-      forall s f stk pc rs m or m',
-        (fn_code f)!pc = Some(Ireturn or) ->
-        Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-        step (State s f (Vptr stk Ptrofs.zero) pc rs m)
-             E0 (Returnstate s (regmap_optget or Vundef rs) m')
+      forall s f stk rs m or m',
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      step (Block s f (Vptr stk Ptrofs.zero) (mk_bblock nil (RBreturn or)) rs m)
+        E0 (Returnstate s (regmap_optget or Vundef rs) m')
   | exec_function_internal:
       forall s f args m m' stk,
-        Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
-        step (Callstate s (Internal f) args m)
-             E0 (State s
-                       f
-                       (Vptr stk Ptrofs.zero)
-                       f.(fn_entrypoint)
-                           (init_regs args f.(fn_params))
-                           m')
+      Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
+      step (Callstate s (Internal f) args m)
+        E0 (State s
+                  f
+                  (Vptr stk Ptrofs.zero)
+                  f.(fn_entrypoint)
+                  (init_regs args f.(fn_params))
+                  m')
   | exec_function_external:
       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')
+      external_call ef ge args m t res m' ->
+      step (Callstate s (External ef) args m)
+         t (Returnstate s res m')
   | exec_return:
       forall res f sp pc rs s vres m,
-        step (Returnstate (Stackframe res f sp pc rs :: s) vres m)
-             E0 (State s f sp pc (rs#res <- vres) m).
+      step (Returnstate (Stackframe res f sp pc rs :: s) vres m)
+        E0 (State s f sp pc (rs#res <- vres) m).
 
 End RELSEM.
+
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall b f m0,
+      let ge := Genv.globalenv p in
+      Genv.init_mem p = Some m0 ->
+      Genv.find_symbol ge p.(prog_main) = Some b ->
+      Genv.find_funct_ptr ge b = Some f ->
+      funsig f = signature_main ->
+      initial_state p (Callstate nil f nil m0).
+
+Inductive final_state: state -> int -> Prop :=
+  | final_state_intro: forall r m,
+      final_state (Returnstate nil (Vint r) m) r.
+
+Definition semantics (p: program) :=
+  Semantics step (initial_state p) final_state (Genv.globalenv p).