diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/hls/RTLBlock.v | 17 | ||||
-rw-r--r-- | src/hls/RTLBlockInstr.v | 44 | ||||
-rw-r--r-- | src/hls/RTLBlockgenproof.v | 10 | ||||
-rw-r--r-- | src/hls/RTLPar.v | 13 | ||||
-rw-r--r-- | src/hls/RTLPargenproof.v | 2 |
5 files changed, 54 insertions, 32 deletions
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index 2c9d8ae..fbd3222 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -68,6 +68,9 @@ Instruction list step The ``step_instr_list`` definition describes the execution of a list of instructions in one big step, inductively traversing the list of instructions and applying the ``step_instr``. + +This is simply using the high-level function ``step_list``, which is a general +function that can execute lists of things, given their execution rule. |*) Definition step_instr_list := step_list (step_instr ge). @@ -77,7 +80,13 @@ Top-level step -------------- The step function itself then uses this big step of the list of instructions to -then show a transition from basic block to basic block. +then show a transition from basic block to basic block. The one particular +aspect of this is that the basic block is also part of the state, which has to +be correctly set during the execution of the function. Function calls and +function returns then also need to set the basic block properly. This means +that the basic block of the returning function also needs to be stored in the +stackframe, as that is the only assumption one can make when returning from a +function. |*) Variant step: state -> trace -> state -> Prop := @@ -106,9 +115,9 @@ then show a transition from basic block to basic block. step (Callstate s (External ef) args m) t (Returnstate s res m') | 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). + forall res f sp pc rs s vres m pr bb, + step (Returnstate (Stackframe res f sp pc bb rs pr :: s) vres m) + E0 (State s f sp pc bb (rs#res <- vres) pr m). End RELSEM. diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index f91c5c0..f3df2c4 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -245,6 +245,7 @@ Section DEFINITION. (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) (pc: node) (**r program point in calling function *) + (bb: bblock) (rs: regset) (**r register state in calling function *) (pr: predset), (**r predicate state of the calling function *) @@ -383,44 +384,51 @@ Step Control-Flow Instruction Inductive step_cf_instr: state -> trace -> state -> Prop := | exec_RBcall: - forall s f sp rs m res fd ros sig args pc pc' pr, + forall s f sp rs m res fd ros sig args pc pc' pr bb, find_function ros rs = Some fd -> funsig fd = sig -> - step_cf_instr (State s f sp pc (mk_bblock nil (RBcall sig ros args res pc')) rs pr m) - E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m) + f.(fn_code) ! pc' = Some bb -> + step_cf_instr + (State s f sp pc (mk_bblock nil (RBcall sig ros args res pc')) rs pr m) + E0 (Callstate (Stackframe res f sp pc' bb rs pr :: s) fd rs##args m) | exec_RBtailcall: forall s f 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 (Vptr stk Ptrofs.zero) pc (mk_bblock nil (RBtailcall sig ros args)) rs pr m) - E0 (Callstate s fd rs##args m') + step_cf_instr + (State s f (Vptr stk Ptrofs.zero) pc (mk_bblock nil (RBtailcall sig ros args)) rs pr m) + E0 (Callstate s fd rs##args m') | exec_RBbuiltin: forall s f sp rs m ef args res pc' vargs t vres m' pc pr bb, eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> f.(fn_code) ! pc' = Some bb -> - step_cf_instr (State s f sp pc (mk_bblock nil (RBbuiltin ef args res pc')) rs pr m) - t (State s f sp pc' bb (regmap_setres res vres rs) pr m') + step_cf_instr + (State s f sp pc (mk_bblock nil (RBbuiltin ef args res pc')) rs pr m) + t (State s f sp pc' bb (regmap_setres res vres rs) pr m') | exec_RBcond: forall s f sp rs m cond args ifso ifnot b pc pc' pr bb, eval_condition cond rs##args m = Some b -> pc' = (if b then ifso else ifnot) -> f.(fn_code) ! pc' = Some bb -> - step_cf_instr (State s f sp pc (mk_bblock nil (RBcond cond args ifso ifnot)) rs pr m) - E0 (State s f sp pc' bb rs pr m) + step_cf_instr + (State s f sp pc (mk_bblock nil (RBcond cond args ifso ifnot)) rs pr m) + E0 (State s f sp pc' bb rs pr m) | exec_RBjumptable: forall s f sp rs m arg tbl n pc pc' pr bb, rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> f.(fn_code) ! pc' = Some bb -> - step_cf_instr (State s f sp pc (mk_bblock nil (RBjumptable arg tbl)) rs pr m) - E0 (State s f sp pc' bb rs pr m) + step_cf_instr + (State s f sp pc (mk_bblock nil (RBjumptable arg tbl)) rs pr m) + E0 (State s f sp pc' bb rs pr m) | exec_RBreturn: forall s f stk rs m or pc m' pr, Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc (mk_bblock nil (RBreturn or)) rs pr m) - E0 (Returnstate s (regmap_optget or Vundef rs) m') + step_cf_instr + (State s f (Vptr stk Ptrofs.zero) pc (mk_bblock nil (RBreturn or)) rs pr m) + E0 (Returnstate s (regmap_optget or Vundef rs) m') | exec_RBgoto: forall s f sp pc rs pr m pc' bb, f.(fn_code) ! pc' = Some bb -> @@ -428,8 +436,12 @@ Step Control-Flow Instruction (State s f sp pc' bb rs pr m) | exec_RBpred_cf: forall s f sp pc rs pr m cf1 cf2 st' p t, - step_cf_instr (State s f sp pc (mk_bblock nil (if eval_predf pr p then cf1 else cf2)) rs pr m) t st' -> - step_cf_instr (State s f sp pc (mk_bblock nil (RBpred_cf p cf1 cf2)) rs pr m) - t st'. + step_cf_instr + (State s f sp pc + (mk_bblock nil (if eval_predf pr p then cf1 else cf2)) + rs pr m) t st' -> + step_cf_instr + (State s f sp pc (mk_bblock nil (RBpred_cf p cf1 cf2)) rs pr m) + t st'. End RELSEM. diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index f870278..f57af34 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -87,15 +87,15 @@ Variant transl_code_spec (c: RTL.code) (tc: code) := forall x x' i i', c ! x = Some i -> find_instr_spec tc x i x' i' -> - check_instr x i i' = true -> + Is_true (check_instr x i i') -> transl_code_spec c tc | transl_code_standard_cf : forall x x' i i' il, c ! x = Some i -> tc ! x' = Some il -> find_instr_spec tc x i x' i' -> - check_cf_instr_body i i' = true -> - check_cf_instr i il.(bb_exit) = true -> + Is_true (check_cf_instr_body i i') -> + Is_true (check_cf_instr i il.(bb_exit)) -> transl_code_spec c tc . @@ -112,12 +112,12 @@ Variant match_stackframe : RTL.stackframe -> stackframe -> Prop := Variant match_states : RTL.state -> RTLBlock.state -> Prop := | match_state : - forall stk stk' f tf sp pc rs m pc' ps + forall stk stk' f tf sp pc rs m pc' ps bb (TF: transl_function f = OK tf) (PC: find_block_spec tf.(fn_code) pc pc') (STK: Forall2 match_stackframe stk stk'), match_states (RTL.State stk f sp pc rs m) - (State stk' tf sp pc' nil rs ps m). + (State stk' tf sp pc' bb rs ps m). Definition match_prog (p: RTL.program) (tp: RTLBlock.program) := Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index a3631ec..61e968e 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -55,17 +55,18 @@ Section RELSEM. 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_cf_instr ge (State s f sp pc nil rs' pr' m') bb.(bb_exit) t s' -> + step_cf_instr ge (State s f sp pc (mk_bblock nil bb.(bb_exit)) rs' pr' m') t s' -> step (State s f sp pc bb rs pr m) t s' | exec_function_internal: - forall s f args m m' stk, + forall s f args m m' stk bb, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> + f.(fn_code) ! (f.(fn_entrypoint)) = Some bb -> step (Callstate s (Internal f) args m) E0 (State s f (Vptr stk Ptrofs.zero) f.(fn_entrypoint) - nil + bb (init_regs args f.(fn_params)) (PMap.init false) m') @@ -75,9 +76,9 @@ Section RELSEM. step (Callstate s (External ef) args m) t (Returnstate s res m') | 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). + forall res f sp pc rs s vres m pr bb, + step (Returnstate (Stackframe res f sp pc bb rs pr :: s) vres m) + E0 (State s f sp pc bb (rs#res <- vres) pr m). End RELSEM. diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 215aef5..fac6455 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -631,7 +631,7 @@ Qed. Lemma step_instr_seq_matches : forall a ge sp st st', - step_instr_seq ge sp st a st' -> + step_instr_seq ge sp st a st' -> forall tst, match_states st tst -> exists tst', step_instr_seq ge sp tst a tst' /\ match_states st' tst'. |