diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 14:51:11 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 14:51:11 +0000 |
| commit | 6034a8b96babe2fb4a3a4ed3802326120ffb7ba0 (patch) | |
| tree | 133967e4409311205dc100130716897c22634902 /src/hls/RTLBlock.v | |
| parent | 16be235ca8d8dfbee26139d602487c03f16de417 (diff) | |
| download | vericert-kvx-6034a8b96babe2fb4a3a4ed3802326120ffb7ba0.tar.gz vericert-kvx-6034a8b96babe2fb4a3a4ed3802326120ffb7ba0.zip | |
Add top-level semantics definitions
Diffstat (limited to 'src/hls/RTLBlock.v')
| -rw-r--r-- | src/hls/RTLBlock.v | 17 |
1 files changed, 17 insertions, 0 deletions
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 := |