diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-04-23 09:37:02 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-04-23 09:37:02 +0100 |
| commit | 6f9d16bb67f32463d98771f3f155297c4ea4b3b7 (patch) | |
| tree | 1d04c6794b53981a340af2d3b72971d8c9a02d8e /src/hls/RTLPar.v | |
| parent | 1dce00e3afe9398a84239cc5f5d44c68b0b5c474 (diff) | |
| download | vericert-6f9d16bb67f32463d98771f3f155297c4ea4b3b7.tar.gz vericert-6f9d16bb67f32463d98771f3f155297c4ea4b3b7.zip | |
Fix translation passes with new semantics
Diffstat (limited to 'src/hls/RTLPar.v')
| -rw-r--r-- | src/hls/RTLPar.v | 23 |
1 files changed, 9 insertions, 14 deletions
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. |