diff options
Diffstat (limited to 'src/hls/RTLBlock.v')
-rw-r--r-- | src/hls/RTLBlock.v | 59 |
1 files changed, 51 insertions, 8 deletions
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index 8a8f7f9..a8efa33 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -32,7 +32,7 @@ Require Import vericert.hls.RTLBlockInstr. Definition bblock_body : Type := list instr. -Definition code : Type := PTree.t (bblock bblock_body). +Definition code : Type := PTree.t (@bblock bblock_body). Record function: Type := mkfunction { fn_sig: signature; @@ -52,17 +52,60 @@ Definition funsig (fd: fundef) := | External ef => ef_sig ef end. -Definition genv := Genv.t fundef unit. -Definition regset := Regmap.t val. +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. -Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := - match rl, vl with - | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) - | _, _ => Regmap.init Vundef - end. +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 *) + 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. + +Definition genv := Genv.t fundef unit. Section RELSEM. + Context (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_bblock: + forall f pc bb cfi, + (fn_code f)!pc = Some (mk_bblock _ bb cfi) -> + step_instr_list (InstrState rs m) bb (InstrState rs' m') + step . + End RELSEM. (* |