From 6034a8b96babe2fb4a3a4ed3802326120ffb7ba0 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 22 Jan 2021 14:51:11 +0000
Subject: Add top-level semantics definitions

---
 src/hls/RTLBlock.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'src/hls/RTLBlock.v')

diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 4a42e7e..23aa8c2 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -168,8 +168,25 @@ Section RELSEM.
       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).
+
 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).
+
 (*
 
 Inductive stackframe : Type :=
-- 
cgit