From b058fc94f5eb6386550f3407f45afeb01381e1ff Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Thu, 13 May 2021 16:44:31 +0100 Subject: Remove "active_call" from HTL semantics added previously to support the fork/wait/join HTL instructions which have since been removed --- src/hls/HTL.v | 20 ++++++++------------ src/hls/HTLgenproof.v | 32 ++++++++++++++++---------------- 2 files changed, 24 insertions(+), 28 deletions(-) (limited to 'src') diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 8474878..06ad26a 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -114,15 +114,12 @@ Definition find_module (i: ident) (ge : genv) : option fundef := | Some b => Globalenvs.Genv.find_funct_ptr ge b end. -Inductive active_call : Type := - | ActiveCall (m : ident) (args : list value). Inductive stackframe : Type := Stackframe : forall (res : reg) (m : module) (st : node) - (forked_modules : list active_call) (reg_assoc : Verilog.assocmap_reg) (arr_assoc : Verilog.assocmap_arr), stackframe. @@ -132,7 +129,6 @@ Inductive state : Type := forall (stack : list stackframe) (m : module) (st : node) - (forked_modules : list active_call) (reg_assoc : Verilog.assocmap_reg) (arr_assoc : Verilog.assocmap_arr), state | Returnstate : @@ -149,7 +145,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asr asa basr1 basa1 nasr1 nasa1 basr2 basa2 nasr2 nasa2 - calls asr' asa' + asr' asa' f pstval, asr!(mod_reset m) = Some (ZToValue 0) -> asr!(mod_finish m) = Some (ZToValue 0) -> @@ -173,26 +169,26 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asa' = Verilog.merge_arrs nasa2 basa2 -> asr'!(m.(mod_st)) = Some (posToValue pstval) -> Z.pos pstval <= Integers.Int.max_unsigned -> - step g (State sf m st calls asr asa) Events.E0 (State sf m pstval calls asr' asa') + step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') | step_finish : - forall g m st calls asr asa retval sf, + forall g m st asr asa retval sf, asr!(m.(mod_finish)) = Some (ZToValue 1) -> asr!(m.(mod_return)) = Some retval -> - step g (State sf m st calls asr asa) Events.E0 (Returnstate sf retval) + step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) | step_call : forall g m args res, step g (Callstate res m args) Events.E0 - (State res m m.(mod_entrypoint) nil + (State res m m.(mod_entrypoint) (AssocMap.set (mod_reset m) (ZToValue 0) (AssocMap.set (mod_finish m) (ZToValue 0) (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) (init_regs args m.(mod_params))))) (empty_stack m)) | step_return : - forall g m calls asr asa i r sf pc mst, + forall g m asr asa i r sf pc mst, mst = mod_st m -> - step g (Returnstate (Stackframe r m pc calls asr asa :: sf) i) Events.E0 - (State sf m pc calls ((asr # mst <- (posToValue pc)) # r <- i) asa). + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 8c2d4af..a486897 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -54,8 +54,8 @@ Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := Hint Constructors match_assocmaps : htlproof. Definition state_st_wf (m : HTL.module) (s : HTL.state) := - forall st calls asa asr res, - s = HTL.State res m st calls asa asr -> + forall st asa asr res, + s = HTL.State res m st asa asr -> asa!(m.(HTL.mod_st)) = Some (posToValue st). Hint Unfold state_st_wf : htlproof. @@ -110,10 +110,10 @@ Inductive match_constants : HTL.module -> assocmap -> Prop := match_constants m asr. Inductive match_states : RTL.state -> HTL.state -> Prop := -| match_state : forall asa asr sf f sp sp' rs mem m st calls res +| match_state : forall asa asr sf f sp sp' rs mem m st res (MASSOC : match_assocmaps f rs asr) (TF : tr_module f m) - (WF : state_st_wf m (HTL.State res m st calls asr asa)) + (WF : state_st_wf m (HTL.State res m st asr asa)) (MF : match_frames sf res) (MARR : match_arrs m f sp mem asa) (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) @@ -122,7 +122,7 @@ Inductive match_states : RTL.state -> HTL.state -> Prop := (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem) (CONST : match_constants m asr), match_states (RTL.State sf f sp st rs mem) - (HTL.State res m st calls asr asa) + (HTL.State res m st asr asa) | match_returnstate : forall v v' stack mem res @@ -305,7 +305,7 @@ Ltac inv_state := inversion TF; match goal with TC : forall _ _, - Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _, + Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _ _, H : Maps.PTree.get _ _ = Some _ |- _ => apply TC in H; inversion H; match goal with @@ -593,8 +593,8 @@ Section CORRECTNESS. end. Lemma eval_cond_correct : - forall stk f sp pc rs m res ml st calls asr asa e b f' s s' args i cond, - match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st calls asr asa) -> + forall stk f sp pc rs m res ml st asr asa e b f' s s' args i cond, + match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> (forall v, In v args -> Ple v (RTL.max_reg_function f)) -> Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> translate_condition cond args s = OK e s' i -> @@ -724,8 +724,8 @@ Section CORRECTNESS. Qed. Lemma eval_cond_correct' : - forall e stk f sp pc rs m res ml st calls asr asa v f' s s' args i cond, - match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st calls asr asa) -> + forall e stk f sp pc rs m res ml st asr asa v f' s s' args i cond, + match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> (forall v, In v args -> Ple v (RTL.max_reg_function f)) -> Values.Val.of_optbool None = v -> translate_condition cond args s = OK e s' i -> @@ -737,8 +737,8 @@ Section CORRECTNESS. Qed. Lemma eval_correct_Oshrximm : - forall s sp rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st calls n, - match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st calls asr asa) -> + forall s sp rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st n, + match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> (RTL.fn_code f) ! pc = Some (RTL.Iop (Op.Oshrximm n) args res0 pc') -> Op.eval_operation ge sp (Op.Oshrximm n) (List.map (fun r : BinNums.positive => @@ -802,8 +802,8 @@ Section CORRECTNESS. Admitted. Lemma eval_correct : - forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st calls, - match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st calls asr asa) -> + forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st , + match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> Op.eval_operation ge sp op (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> @@ -1022,10 +1022,10 @@ Section CORRECTNESS. *) Definition transl_instr_prop (instr : RTL.instruction) : Prop := - forall m asr asa fin rtrn st calls stmt trans res, + forall m asr asa fin rtrn st stmt trans res, tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans -> exists asr' asa', - HTL.step tge (HTL.State res m st calls asr asa) Events.E0 (HTL.State res m st calls asr' asa'). + HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). Opaque combine. -- cgit