From 32cfca30754f13cd91b228712cd65d3115a3f355 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 2 Nov 2020 19:38:17 +0000 Subject: WIP on RTLBlock semantics --- src/hls/RTLBlock.v | 110 +++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 98 insertions(+), 12 deletions(-) diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index a1c3f25..e5ce9a7 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -16,13 +16,9 @@ * along with this program. If not, see . *) -From compcert Require Import - Coqlib - AST - Maps - Op - RTL - Registers. +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. Definition node := positive. @@ -35,10 +31,10 @@ Inductive instruction : Type := Definition bblock_body : Type := list instruction. Inductive control_flow_inst : Type := -| RBcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst +(*| RBcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst | RBtailcall : signature -> reg + ident -> list reg -> control_flow_inst | RBbuiltin : external_function -> list (builtin_arg reg) -> - builtin_res reg -> node -> control_flow_inst + builtin_res reg -> node -> control_flow_inst*) | RBcond : condition -> list reg -> node -> node -> control_flow_inst | RBjumptable : reg -> list node -> control_flow_inst | RBreturn : option reg -> control_flow_inst @@ -46,7 +42,7 @@ Inductive control_flow_inst : Type := Record bblock : Type := mk_bblock { bb_body: bblock_body; - bb_exit: option control_flow_inst + bb_exit: control_flow_inst }. Definition code : Type := PTree.t bblock. @@ -71,11 +67,101 @@ Definition funsig (fd: fundef) := Definition successors_instr (i : control_flow_inst) : list node := match i with - | RBcall sig ros args res s => s :: nil +(* | RBcall sig ros args res s => s :: nil | RBtailcall sig ros args => nil - | RBbuiltin ef args res s => s :: nil + | RBbuiltin ef args res s => s :: nil*) | RBcond cond args ifso ifnot => ifso :: ifnot :: nil | RBjumptable arg tbl => tbl | RBreturn optarg => nil | RBgoto n => n :: nil end. + +Definition genv := Genv.t fundef unit. +Definition regset := Regmap.t val. + +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 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. + +Inductive cont : Type := + | C + | N. + +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 *) + (bblock: bblock) (**r bblock being executed *) + (c : cont), + 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. + +Variable 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_RBnop : + forall s f sp pc rs m ls ci, + step (State s f sp pc rs m (mk_bblock (RBnop :: ls) ci) C) E0 + (State s f sp (Pos.succ pc) rs m (mk_bblock ls ci) C) + | exec_RBop : + forall s f sp pc rs m ls args op res ci v, + eval_operation ge sp op rs##args m = Some v -> + step (State s f sp pc rs m (mk_bblock (RBop op args res :: ls) ci) C) E0 + (State s f sp (Pos.succ pc) rs m (mk_bblock ls ci) C) + | exec_RBload: + forall s f sp pc rs m chunk addr args dst a v ls ci, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + step (State s f sp pc rs m (mk_bblock (RBload chunk addr args dst :: ls) ci) C) + E0 (State s f sp (Pos.succ pc) (rs#dst <- v) m (mk_bblock ls ci) C) + | exec_RBstore: + forall s f sp pc rs m chunk addr args src a m' ls ci, + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a rs#src = Some m' -> + step (State s f sp pc rs m (mk_bblock (RBstore chunk addr args src :: ls) ci) C) + E0 (State s f sp (Pos.succ pc) rs m' (mk_bblock ls ci) C) + | exec_RBcond: + forall s f sp pc rs m cond args ifso ifnot b pc', + eval_condition cond rs##args m = Some b -> + pc' = (if b then ifso else ifnot) -> + step (State s f sp pc rs m (mk_bblock nil (RBcond cond args ifso ifnot)) C) + E0 (State s f sp pc' rs m (mk_bblock nil (RBcond cond args ifso ifnot)) N) +. -- cgit