From 6f9d16bb67f32463d98771f3f155297c4ea4b3b7 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 23 Apr 2022 09:37:02 +0100 Subject: Fix translation passes with new semantics --- src/hls/RICtransf.v | 7 ++- src/hls/RTLBlock.v | 5 ++- src/hls/RTLBlockgenproof.v | 110 ++++++++++++++++++++++++--------------------- src/hls/RTLPar.v | 23 ++++------ src/hls/RTLParFUgen.v | 2 +- 5 files changed, 75 insertions(+), 72 deletions(-) (limited to 'src') diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v index 3b82b29..886c23d 100644 --- a/src/hls/RICtransf.v +++ b/src/hls/RICtransf.v @@ -49,11 +49,10 @@ Fixpoint existsb_val {A B} (f: A -> option B) (l : list A) : option B := end end. -Definition includes_setpred (bb: list (list instr)) := - existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end)) bb. +Definition includes_setpred (bb: bb) := + existsb_val (existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end))) bb. -Definition add_bb (should_split: bool) (i: list (list instr)) - (bbc: list (list (list instr)) * list (list (list instr))) := +Definition add_bb (should_split: bool) (i: bb) (bbc: list bb * list bb) := match bbc with | (a, b) => if should_split then (a, i::b) else (i::a, b) end. diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index b9e9914..19ac4f5 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -93,9 +93,10 @@ function. | exec_bblock: forall s f sp pc rs rs' m m' bb pr pr' t state, 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_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 state -> - step (State s f sp pc rs pr m) E0 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) -> diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index b191c09..7931874 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -30,6 +30,7 @@ Require Import compcert.common.Globalenvs. Require Import compcert.lib.Maps. Require Import compcert.backend.Registers. Require compcert.common.Smallstep. +Require Import compcert.common.Events. Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlockInstr. @@ -94,23 +95,28 @@ transformation. This also specifies ``x'`` relative to x given the code. |*) -Variant transl_code_spec (c: RTL.code) (tc: code) (x x': node): Prop := +Variant transl_code_spec (c: RTL.code) (tc: code) (x x': node) (i: RTL.instruction) (i': instr): Prop := | transl_code_standard_bb : - forall i i', c ! x = Some i -> - find_instr_spec tc x i x' i' -> Is_true (check_instr x i i') -> - transl_code_spec c tc x x' + transl_code_spec c tc x x' i i' | transl_code_standard_cf : - forall i i' il, + forall il, c ! x = Some i -> tc ! x' = Some il -> - find_instr_spec tc x i x' i' -> Is_true (check_cf_instr_body i i') -> Is_true (check_cf_instr i il.(bb_exit)) -> - transl_code_spec c tc x x' + transl_code_spec c tc x x' i i' . +Section CORRECTNESS. + + Context (prog : RTL.program). + Context (tprog : RTLBlock.program). + + Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : genv := Globalenvs.Genv.globalenv tprog. + (*| Matches the basic block that should be present in the state. This simulates the small step execution of the basic block from the big step semantics that are @@ -122,57 +128,59 @@ It doesn't have to find the value because it's given as an input, and the finding is actually done at that higher level already. |*) -Variant match_bblock (tc: code) (pc pc': node): list instr -> Prop := -| match_bblock_intro : - forall bb cf, - tc ! pc' = Some (mk_bblock bb cf) -> - match_bblock tc pc pc' (list_drop (offset pc pc') bb). - -Variant match_stackframe : RTL.stackframe -> stackframe -> Prop := -| match_stackframe_init : - forall res f tf sp pc pc' rs - (TF: transl_function f = OK tf) - (PC: transl_code_spec f.(RTL.fn_code) tf.(fn_code) pc pc'), - match_stackframe (RTL.Stackframe res f sp pc rs) - (Stackframe res tf sp pc' rs (PMap.init false)). + Variant match_bblock (tc: code) (pc pc': node): list instr -> Prop := + | match_bblock_intro : + forall bb cf, + tc ! pc' = Some (mk_bblock bb cf) -> + match_bblock tc pc pc' (list_drop (offset pc pc') bb). + + Variant match_stackframe : RTL.stackframe -> stackframe -> Prop := + | match_stackframe_init : + forall res f tf sp pc pc' rs i i' + (TF: transl_function f = OK tf) + (TF: find_instr_spec tf.(fn_code) pc i pc' i') + (PC: transl_code_spec f.(RTL.fn_code) tf.(fn_code) pc pc' i i'), + match_stackframe (RTL.Stackframe res f sp pc rs) + (Stackframe res tf sp pc' rs (PMap.init false)). (*| -The ``match_states`` predicate defines how to find the correct ``bb`` that -should be executed, as well as the value of ``pc``. +Initially, the idea was to define the ``match_states`` predicate normally to +defines how to find the correct ``bb`` that should be executed, as well as the +value of ``pc``. However, this does not quite work when proving the equivalence +of the translation from ``RTL`` to ``RTLBlock``, because one cannot match one +transition to a transition in RTLBlock. The alternative to this is to include a +proof inside of the ``match_states`` that shows that the execution from the +``pc`` of the start of the basic block to the current point is the same as the +whole execution (in one big step) of the basic block. |*) -Variant match_states : RTL.state -> RTLBlock.state -> Prop := -| match_state : - forall stk stk' f tf sp pc rs m pc' bb - (TF: transl_function f = OK tf) - (PC: transl_code_spec f.(RTL.fn_code) tf.(fn_code) pc pc') - (STK: Forall2 match_stackframe stk stk') - (BB: match_bblock tf.(fn_code) pc pc' bb), - match_states (RTL.State stk f sp pc rs m) - (State stk' tf sp pc' bb rs (PMap.init false) m) -| match_callstate : - forall cs cs' f tf args m - (TF: transl_fundef f = OK tf) - (STK: Forall2 match_stackframe cs cs'), - match_states (RTL.Callstate cs f args m) (Callstate cs' tf args m) -| match_returnstate : - forall cs cs' v m - (STK: Forall2 match_stackframe cs cs'), - match_states (RTL.Returnstate cs v m) (Returnstate cs' v 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. - -Section CORRECTNESS. - - Context (prog : RTL.program). - Context (tprog : RTLBlock.program). + Variant match_states : option bb -> RTL.state -> RTLBlock.state -> Prop := + | match_state : + forall stk stk' f tf sp pc rs m rs' m' pc0 bb i i' b rs0 m0 + (TF: transl_function f = OK tf) + (TF: find_instr_spec tf.(fn_code) pc i pc0 i') + (PC: transl_code_spec f.(RTL.fn_code) tf.(fn_code) pc pc0 i i') + (STK: Forall2 match_stackframe stk stk') + (STARSIMU: Smallstep.star RTL.step ge (RTL.State stk f sp pc0 rs0 m0) + E0 (RTL.State stk f sp pc rs m)) + (BB: match_bblock tf.(fn_code) pc pc0 bb), + match_states (Some b) (RTL.State stk f sp pc rs m) + (State stk' tf sp pc0 rs' (PMap.init false) m') + | match_callstate : + forall cs cs' f tf args m + (TF: transl_fundef f = OK tf) + (STK: Forall2 match_stackframe cs cs'), + match_states None (RTL.Callstate cs f args m) (Callstate cs' tf args m) + | match_returnstate : + forall cs cs' v m + (STK: Forall2 match_stackframe cs cs'), + match_states None (RTL.Returnstate cs v m) (Returnstate cs' v 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. Context (TRANSL : match_prog prog tprog). - Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. - Let tge : genv := Globalenvs.Genv.globalenv tprog. - Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed. 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. diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v index a104056..49ee6e7 100644 --- a/src/hls/RTLParFUgen.v +++ b/src/hls/RTLParFUgen.v @@ -134,7 +134,7 @@ Definition insert_extra (pt: PTree.t (list instr)) (curr: list (list instr)) | None => ((cycle + 1)%positive, curr :: bb) end. -Definition transl_bb (res: resources) (bb: list RTLPar.bb): Errors.res RTLParFU.bblock_body := +Definition transl_bb (res: resources) (bb: RTLPar.bb): Errors.res RTLParFU.bblock_body := do (litr, n) <- fold_right (transl_seq_block res) (OK (nil, PTree.empty _, 1%positive)) bb; let (li, tr) := litr in OK (snd (fold_right (insert_extra tr) (1%positive, nil) li)). -- cgit