aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/hls/HTL.v73
-rw-r--r--src/hls/HTLgenproof.v44
2 files changed, 66 insertions, 51 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 0706b20..12b6493 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -119,32 +119,34 @@ Definition find_module (i: ident) (ge : genv) : option module :=
end.
Inductive stackframe : Type :=
- Stackframe :
- forall (m : module)
- (st : node)
- (reg_assoc : Verilog.assocmap_reg)
- (arr_assoc : Verilog.assocmap_arr),
- stackframe.
+ Stackframe : forall (mid : ident)
+ (m : module)
+ (st : node)
+ (reg_assoc : Verilog.assocmap_reg)
+ (arr_assoc : Verilog.assocmap_arr),
+ stackframe.
Inductive state : Type :=
| State :
forall (stack : list stackframe)
+ (mid : ident)
(m : module)
(st : node)
(reg_assoc : Verilog.assocmap_reg)
(arr_assoc : Verilog.assocmap_arr), state
| Returnstate :
forall (res : list stackframe)
- (mid : ident)
+ (mid : ident) (** Name of the callee *)
(v : value), state
| Callstate :
forall (stack : list stackframe)
+ (mid : ident)
(m : module)
(args : list value), state.
Inductive step : genv -> state -> Events.trace -> state -> Prop :=
| step_module :
- forall g m st sf ctrl_stmnt data_stmnt
+ forall g mid m st sf ctrl_stmnt data_stmnt
asr asa
basr1 basa1 nasr1 nasa1
basr2 basa2 nasr2 nasa2
@@ -172,49 +174,60 @@ 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 asr asa) Events.E0 (State sf m pstval asr' asa')
+ step g
+ (State sf mid m st asr asa) Events.E0
+ (State sf mid m pstval asr' asa')
| step_finish :
forall g m st asr asa retval sf mid,
asr!(m.(mod_finish)) = Some (ZToValue 1) ->
asr!(m.(mod_return)) = Some retval ->
- (* FIXME: We need to check that mid actually matches the current module *)
- step g (State sf m st asr asa) Events.E0 (Returnstate sf mid retval)
+ step g
+ (State sf mid m st asr asa) Events.E0
+ (Returnstate sf mid retval)
| step_initcall :
- forall g m st asr asa sf othermod_id othermod othermod_reset othermod_params othermod_param_vals,
- find_module othermod_id g = Some othermod ->
+ forall g callerid caller st asr asa sf callee_id callee callee_reset callee_params callee_param_vals,
+ find_module callee_id g = Some callee ->
- m.(mod_externctrl)!othermod_reset = Some (othermod_id, ctrl_reset) ->
- (forall n param, nth_error othermod_params n = Some param ->
- m.(mod_externctrl)!param = Some (othermod_id, ctrl_param n)) ->
+ caller.(mod_externctrl)!callee_reset = Some (callee_id, ctrl_reset) ->
+ (forall n param, nth_error callee_params n = Some param ->
+ caller.(mod_externctrl)!param = Some (callee_id, ctrl_param n)) ->
(* The fact that this is the only condition on the current state to trigger
a call introduces non-determinism into the semantics. The semantics
permit initiating a call from any state where a reset has been set to 0.
*)
- asr!othermod_reset = Some (ZToValue 0) ->
- othermod_param_vals = List.map (fun p => asr#p) othermod_params ->
+ asr!callee_reset = Some (ZToValue 0) ->
+ callee_param_vals = List.map (fun p => asr#p) callee_params ->
+
+ step g
+ (State sf callerid caller st asr asa) Events.E0
+ (Callstate (Stackframe callerid caller st asr asa :: sf)
+ callee_id callee callee_param_vals)
- step g (State sf m st asr asa) Events.E0
- (Callstate (Stackframe m st asr asa :: sf) othermod othermod_param_vals)
| step_call :
- forall g m args res,
- step g (Callstate res m args) Events.E0
- (State res m m.(mod_entrypoint)
+ forall g mid m args res,
+ step g
+ (Callstate res mid m args) Events.E0
+ (State res mid 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 asr asa othermod_id othermod_return othermod_finish i r sf pc mst,
- mst = mod_st m ->
+ forall g callerid caller asr asa callee_id callee_return callee_finish i sf pc mst,
+ mst = mod_st caller ->
- m.(mod_externctrl)!othermod_return = Some (othermod_id, ctrl_return) ->
- m.(mod_externctrl)!othermod_finish = Some (othermod_id, ctrl_finish) ->
+ caller.(mod_externctrl)!callee_return = Some (callee_id, ctrl_return) ->
+ caller.(mod_externctrl)!callee_finish = Some (callee_id, ctrl_finish) ->
- step g (Returnstate (Stackframe m pc asr asa :: sf) othermod_id i) Events.E0
- (State sf m pc (asr # mst <- (posToValue pc) # othermod_finish <- (ZToValue 1) # r <- i) asa).
+ step g
+ (Returnstate (Stackframe callerid caller pc asr asa :: sf) callee_id i) Events.E0
+ (State sf callerid caller pc
+ (asr # mst <- (posToValue pc) # callee_finish <- (ZToValue 1) # callee_return <- i)
+ asa).
Hint Constructors step : htl.
Inductive initial_state (p: program): state -> Prop :=
@@ -223,7 +236,7 @@ Inductive initial_state (p: program): state -> Prop :=
Globalenvs.Genv.init_mem p = Some m0 ->
Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) ->
- initial_state p (Callstate nil m nil).
+ initial_state p (Callstate nil p.(AST.prog_main) m nil).
Inductive final_state : state -> Integers.int -> Prop :=
| final_state_intro : forall retval mid retvali,
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 077a8dc..d07d75e 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -55,8 +55,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 asa asr res,
- s = HTL.State res m st asa asr ->
+ forall mid st asa asr res,
+ s = HTL.State res mid m st asa asr ->
asa!(m.(HTL.mod_st)) = Some (posToValue st).
Hint Unfold state_st_wf : htlproof.
@@ -115,11 +115,11 @@ Inductive match_externctrl (m : HTL.module) (asr : assocmap) : Prop :=
match_externctrl m asr.
Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall asa asr sf f sp sp' rs mem m st res
+| match_state : forall asa asr sf f sp sp' rs mem mid m st res
(MASSOC : match_assocmaps f rs asr)
(TF : tr_module f m)
- (WF : state_st_wf m (HTL.State res m st asr asa))
- (MF : match_frames sf res)
+ (WF : state_st_wf m (HTL.State res mid m st asr asa))
+ (MF : match_frames mid sf res)
(MARR : match_arrs m f sp mem asa)
(SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
(RSBP : reg_stack_based_pointers sp' rs)
@@ -128,16 +128,18 @@ Inductive match_states : RTL.state -> HTL.state -> Prop :=
(CONST : match_constants m asr)
(EXTERN : match_externctrl m asr),
match_states (RTL.State sf f sp st rs mem)
- (HTL.State res m st asr asa)
+ (HTL.State res mid m st asr asa)
| match_returnstate :
- forall v v' stack mem res mid
- (MF : match_frames stack res),
+ forall v v' rtl_stk htl_stk mem mid
+ (MF : match_frames mid rtl_stk htl_stk),
val_value_lessdef v v' ->
- match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res mid v')
+ match_states (RTL.Returnstate rtl_stk v mem)
+ (HTL.Returnstate htl_stk mid v')
| match_initial_call :
- forall f m m0
+ forall f mid m m0
(TF : tr_module f m),
- match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil).
+ match_states (RTL.Callstate nil (AST.Internal f) nil m0)
+ (HTL.Callstate nil mid m nil).
Hint Constructors match_states : htlproof.
Definition match_prog (p: RTL.program) (tp: HTL.program) :=
@@ -619,8 +621,8 @@ Section CORRECTNESS.
).
Lemma eval_cond_correct :
- 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 stk f sp pc rs mid 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 mid 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 ->
@@ -750,8 +752,8 @@ Section CORRECTNESS.
Qed.
Lemma eval_cond_correct' :
- 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 e stk f sp pc rs m res mid ml st asr asa v f' s s' args i cond,
+ match_states (RTL.State stk f sp pc rs m) (HTL.State res mid 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 ->
@@ -763,8 +765,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 n,
- match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
+ forall s sp rs m v e asr asa f f' stk s' i pc res0 pc' args res mid ml st n,
+ match_states (RTL.State stk f sp pc rs m) (HTL.State res mid 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 =>
@@ -825,8 +827,8 @@ Section CORRECTNESS.
Qed.
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 ,
- match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) ->
+ forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res mid ml st ,
+ match_states (RTL.State stk f sp pc rs m) (HTL.State res mid 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 ->
@@ -1043,10 +1045,10 @@ Section CORRECTNESS.
*)
Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
- forall m asr asa fin rtrn st stmt trans res,
+ forall mid 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 asr asa) Events.E0 (HTL.State res m st asr' asa').
+ HTL.step tge (HTL.State res mid m st asr asa) Events.E0 (HTL.State res mid m st asr' asa').
Opaque combine.
generated by cgit (git 2.34.1) at 2024-06-30 21:23:06 +0000