From 2d647ce5fdf5343a7d9961a63d66b5191706aeaf Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 22 Mar 2022 16:43:39 +0000 Subject: Add comments to allow for literate detangling --- src/hls/RTLBlock.v | 94 ++++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 84 insertions(+), 10 deletions(-) (limited to 'src/hls/RTLBlock.v') diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index bf5c37a..4fae701 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2021 Yann Herklotz + * Copyright (C) 2020-2022 Yann Herklotz * * 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 @@ -16,6 +16,7 @@ * along with this program. If not, see . *) +(* [[file:../../lit/scheduling.org::rtlblock-main][rtlblock-main]] *) Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Events. @@ -39,9 +40,32 @@ Definition fundef := @fundef bb. Definition program := @program bb. Definition funsig := @funsig bb. Definition stackframe := @stackframe bb. -Definition state := @state bb. + Definition genv := @genv bb. +Inductive state : Type := +| State: + forall (stack: list stackframe) (**r call stack *) + (f: function) (**r current function *) + (b: bb) (**r current block being executed *) + (sp: val) (**r stack pointer *) + (pc: node) (**r current program point in [c] *) + (rs: regset) (**r register state *) + (pr: predset) (**r predicate register state *) + (m: mem), (**r memory state *) + 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. Context (ge: genv). @@ -56,19 +80,68 @@ Section RELSEM. forall state sp, step_instr_list sp state nil state. + 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_cf_instr: state -> cf_instr -> trace -> state -> Prop := + | exec_RBcall: + forall s f b sp rs m res fd ros sig args pc pc' pr, + find_function ros rs = Some fd -> + funsig fd = sig -> + step_cf_instr (State s f b sp pc rs pr m) (RBcall sig ros args res pc') + E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m) + | exec_RBtailcall: + forall s f b stk rs m sig ros args fd m' pc pr, + find_function ros rs = Some fd -> + funsig fd = sig -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step_cf_instr (State s f b (Vptr stk Ptrofs.zero) pc rs pr m) (RBtailcall sig ros args) + E0 (Callstate s fd rs##args m') + | exec_RBbuiltin: + forall s f b sp rs m ef args res pc' vargs t vres m' pc pr, + eval_builtin_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + step_cf_instr (State s f b sp pc rs pr m) (RBbuiltin ef args res pc') + t (State s f b sp pc' (regmap_setres res vres rs) pr m') + | exec_RBcond: + forall s f block sp rs m cond args ifso ifnot b pc pc' pr, + eval_condition cond rs##args m = Some b -> + pc' = (if b then ifso else ifnot) -> + step_cf_instr (State s f block sp pc rs pr m) (RBcond cond args ifso ifnot) + E0 (State s f block sp pc' rs pr m) + | exec_RBjumptable: + forall s f b sp rs m arg tbl n pc pc' pr, + rs#arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some pc' -> + step_cf_instr (State s f b sp pc rs pr m) (RBjumptable arg tbl) + E0 (State s f b sp pc' rs pr m) + | exec_RBreturn: + forall s f b stk rs m or pc m' pr, + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step_cf_instr (State s f b (Vptr stk Ptrofs.zero) pc rs pr m) (RBreturn or) + E0 (Returnstate s (regmap_optget or Vundef rs) m') + | exec_RBgoto: + forall s f b sp pc rs pr m pc', + step_cf_instr (State s f b sp pc rs pr m) (RBgoto pc') E0 (State s f b sp pc' rs pr m) + | exec_RBpred_cf: + forall s f b sp pc rs pr m cf1 cf2 st' p t, + step_cf_instr (State s f b sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' -> + step_cf_instr (State s f b sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'. + Inductive step: state -> trace -> state -> Prop := - | exec_bblock: - forall s f sp pc rs rs' m m' t s' bb pr pr', - f.(fn_code)!pc = Some bb -> - step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> - step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> - step (State s f sp pc rs pr m) t s' | 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 + E0 (State s f (Vptr stk Ptrofs.zero) f.(fn_entrypoint) (init_regs args f.(fn_params)) @@ -101,3 +174,4 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). +(* rtlblock-main ends here *) -- cgit