diff options
Diffstat (limited to 'src/hls')
| -rw-r--r-- | src/hls/ApplyExternctrl.v | 202 | ||||
| -rw-r--r-- | src/hls/AssocMap.v | 17 | ||||
| -rw-r--r-- | src/hls/HTL.v | 141 | ||||
| -rw-r--r-- | src/hls/HTLBlockgen.v | 167 | ||||
| -rw-r--r-- | src/hls/HTLPargen.v | 23 | ||||
| -rw-r--r-- | src/hls/HTLgen.v | 516 | ||||
| -rw-r--r-- | src/hls/HTLgenproof.v | 1214 | ||||
| -rw-r--r-- | src/hls/HTLgenspec.v | 921 | ||||
| -rw-r--r-- | src/hls/PrintHTL.ml | 69 | ||||
| -rw-r--r-- | src/hls/PrintVerilog.mli | 2 | ||||
| -rw-r--r-- | src/hls/Renaming.v | 231 | ||||
| -rw-r--r-- | src/hls/Verilog.v | 14 | ||||
| -rw-r--r-- | src/hls/Veriloggen.v | 202 | ||||
| -rw-r--r-- | src/hls/Veriloggenproof.v | 739 |
14 files changed, 2711 insertions, 1747 deletions
diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v new file mode 100644 index 0000000..b024b9e --- /dev/null +++ b/src/hls/ApplyExternctrl.v @@ -0,0 +1,202 @@ +Require Import compcert.common.Errors. +Require Import compcert.common.AST. + +Require Import vericert.common.Maps. +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.HTL. +Require Import vericert.hls.Verilog. + +Import ListNotations. + +Section APPLY_EXTERNCTRL. + Local Open Scope assocmap. + Local Open Scope error_monad_scope. + + Variable prog : HTL.program. + Variable m : HTL.module. + + Let modmap := prog_modmap prog. + + Definition global_clk := + match modmap ! (AST.prog_main prog) with + | None => Error (msg "ApplyExternctrl: No main") + | Some main => OK (HTL.mod_clk main) + end. + + Definition get_mod_signal (othermod : HTL.module) (signal : HTL.controlsignal) := + match signal with + | ctrl_finish => OK (HTL.mod_finish othermod) + | ctrl_return => OK (HTL.mod_return othermod) + | ctrl_start => OK (HTL.mod_start othermod) + | ctrl_reset => OK (HTL.mod_reset othermod) + | ctrl_clk => OK (HTL.mod_clk othermod) + | ctrl_param idx => + match List.nth_error (HTL.mod_params othermod) idx with + | Some r => OK r + | None => Error (msg "Module does not have nth parameter") + end + end. + + Definition reg_apply_externctrl (r : Verilog.reg) : res reg := + match (HTL.mod_externctrl m) ! r with + | None => OK r + | Some (m, signal) => + match modmap ! m with + | None => Error (msg "Veriloggen: Could not find definition for called module") + | Some othermod => get_mod_signal othermod signal + end + end. + + Fixpoint expr_apply_externctrl (expr : Verilog.expr) {struct expr} : res Verilog.expr := + match expr with + | Vlit n => + OK (Vlit n) + | Vvar r => + do r' <- reg_apply_externctrl r; + OK (Vvar r') + | Vvari r e => + do r' <- reg_apply_externctrl r; + do e' <- expr_apply_externctrl e; + OK (Vvari r e) + | Vrange r e1 e2 => + do r' <- reg_apply_externctrl r; + do e1' <- expr_apply_externctrl e1; + do e2' <- expr_apply_externctrl e2; + OK (Vrange r' e1' e2') + | Vinputvar r => + do r' <- reg_apply_externctrl r; + OK (Vinputvar r') + | Vbinop op e1 e2 => + do e1' <- expr_apply_externctrl e1; + do e2' <- expr_apply_externctrl e2; + OK (Vbinop op e1' e2') + | Vunop op e => + do e' <- expr_apply_externctrl e; + OK (Vunop op e') + | Vternary e1 e2 e3 => + do e1' <- expr_apply_externctrl e1; + do e2' <- expr_apply_externctrl e2; + do e3' <- expr_apply_externctrl e3; + OK (Vternary e1' e2' e3') + end. + + Definition mmap_option {A B} (f : A -> res B) (opt : option A) : res (option B) := + match opt with + | None => OK None + | Some a => do a' <- f a; OK (Some a') + end. + + Definition cases_apply_externctrl_ (stmnt_apply_externctrl_ : Verilog.stmnt -> res Verilog.stmnt) := + fix cases_apply_externctrl (cs : list (Verilog.expr * Verilog.stmnt)) := + match cs with + | nil => OK nil + | (c_e, c_s) :: tl => + do c_e' <- expr_apply_externctrl c_e; + do c_s' <- stmnt_apply_externctrl_ c_s; + do tl' <- cases_apply_externctrl tl; + OK ((c_e', c_s') :: tl') + end. + + Fixpoint stmnt_apply_externctrl (stmnt : Verilog.stmnt) {struct stmnt} : res Verilog.stmnt := + match stmnt with + | Vskip => OK Vskip + | Vseq s1 s2 => + do s1' <- stmnt_apply_externctrl s1; + do s2' <- stmnt_apply_externctrl s2; + OK (Vseq s1' s2') + | Vcond e s1 s2 => + do e' <- expr_apply_externctrl e; + do s1' <- stmnt_apply_externctrl s1; + do s2' <- stmnt_apply_externctrl s2; + OK (Vcond e' s1' s2') + | Vcase e cases def => + do e' <- expr_apply_externctrl e; + do cases' <- cases_apply_externctrl_ stmnt_apply_externctrl cases; + do def' <- mmap_option (fun x => stmnt_apply_externctrl x) def; + OK (Vcase e' cases' def') + | Vblock e1 e2 => + do e1' <- expr_apply_externctrl e1; + do e2' <- expr_apply_externctrl e2; + OK (Vblock e1' e2') + | Vnonblock e1 e2 => + do e1' <- expr_apply_externctrl e1; + do e2' <- expr_apply_externctrl e2; + OK (Vnonblock e1' e2') + end. + + (* Unused. Defined for completeness *) + Definition cases_apply_externctrl := cases_apply_externctrl_ stmnt_apply_externctrl. + + Fixpoint xassocmap_apply_externctrl {A} (regmap : list (reg * A)) : res (list (reg * A)) := + match regmap with + | nil => OK nil + | (r, v) :: l => + do r' <- reg_apply_externctrl r; + do l' <- xassocmap_apply_externctrl l; + OK ((r', v) :: l') + end. + + Definition assocmap_apply_externctrl {A} (regmap : AssocMap.t A) : res (AssocMap.t A) := + do l <- xassocmap_apply_externctrl (AssocMap.elements regmap); + OK (AssocMap_Properties.of_list l). + + Definition module_apply_externctrl : res HTL.module := + do mod_start' <- reg_apply_externctrl (HTL.mod_start m); + do mod_reset' <- reg_apply_externctrl (HTL.mod_reset m); + do mod_clk' <- global_clk; + do mod_finish' <- reg_apply_externctrl (HTL.mod_finish m); + do mod_return' <- reg_apply_externctrl (HTL.mod_return m); + do mod_st' <- reg_apply_externctrl (HTL.mod_st m); + do mod_stk' <- reg_apply_externctrl (HTL.mod_stk m); + do mod_params' <- mmap reg_apply_externctrl (HTL.mod_params m); + do mod_controllogic' <- PTree.traverse1 stmnt_apply_externctrl (HTL.mod_controllogic m); + do mod_datapath' <- PTree.traverse1 stmnt_apply_externctrl (HTL.mod_datapath m); + + do mod_scldecls' <- assocmap_apply_externctrl (HTL.mod_scldecls m); + do mod_arrdecls' <- assocmap_apply_externctrl (HTL.mod_arrdecls m); + do mod_externctrl' <- assocmap_apply_externctrl (HTL.mod_externctrl m); + + match zle (Z.pos (max_pc_map mod_datapath')) Integers.Int.max_unsigned, + zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned with + | left LEDATA, left LECTRL => + OK (HTL.mkmodule + mod_params' + mod_datapath' + mod_controllogic' + (HTL.mod_entrypoint m) + mod_st' + mod_stk' + (HTL.mod_stk_len m) + mod_finish' + mod_return' + mod_start' + mod_reset' + mod_clk' + mod_scldecls' + mod_arrdecls' + mod_externctrl' + (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) + | _, _ => Error (Errors.msg "More than 2^32 states.") + end. +End APPLY_EXTERNCTRL. + +Definition transf_fundef (prog : HTL.program) := transf_partial_fundef (module_apply_externctrl prog). +Definition transf_program (prog : HTL.program) := transform_partial_program (transf_fundef prog) prog. + +(* Semantics *) + +Definition match_prog : HTL.program -> HTL.program -> Prop := + Linking.match_program (fun ctx f tf => ApplyExternctrl.transf_fundef ctx f = OK tf) eq. + +Lemma transf_program_match : forall p tp, + ApplyExternctrl.transf_program p = OK tp -> match_prog p tp. +Admitted. + +Lemma transf_program_correct : forall p tp, + match_prog p tp -> Smallstep.forward_simulation (HTL.semantics p) (HTL.semantics tp). +Admitted. + +Instance TransfLink : Linking.TransfLink match_prog. +Admitted. diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index 98eda9c..7b9ef9f 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -25,6 +25,7 @@ Require Import vericert.hls.ValueInt. Definition reg := positive. Module AssocMap := Maps.PTree. +Module AssocMap_Properties := Maps.PTree_Properties. Module AssocMapExt. Import AssocMap. @@ -229,3 +230,19 @@ Lemma find_get_assocmap : assoc ! r = Some v -> assoc # r = v. Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed. + +Lemma fso : forall m v k1 k2, k1 <> k2 -> (m # k1 <- v) # k2 = m # k2. +Proof. + unfold "_ # _". + unfold AssocMapExt.get_default. + intros. + destruct_match; rewrite AssocMap.gso in Heqo by auto; rewrite Heqo; auto. +Qed. + +Lemma fss : forall m v k, (m # k <- v) # k = v. +Proof. + unfold "_ # _". + unfold AssocMapExt.get_default. + intros. + destruct_match; rewrite AssocMap.gss in Heqo by auto; inv Heqo; crush. +Qed. diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 61ea541..886f86d 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -31,6 +31,7 @@ Require Import vericert.common.Vericertlib. Require Import vericert.hls.ValueInt. Require Import vericert.hls.AssocMap. Require Import vericert.hls.Array. +Require Import vericert.common.Maps. Require vericert.hls.Verilog. Local Open Scope positive. @@ -45,9 +46,12 @@ Local Open Scope assocmap. Definition reg := positive. Definition node := positive. +Definition ident := positive. -Definition datapath := PTree.t Verilog.stmnt. -Definition controllogic := PTree.t Verilog.stmnt. +Definition datapath_stmnt := Verilog.stmnt. +Definition datapath := PTree.t datapath_stmnt. +Definition control_stmnt := Verilog.stmnt. +Definition controllogic := PTree.t control_stmnt. Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := forall p0 : positive, @@ -72,6 +76,21 @@ Record ram := mk_ram { Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g. +Inductive controlsignal : Type := + | ctrl_finish : controlsignal + | ctrl_return : controlsignal + | ctrl_start : controlsignal + | ctrl_reset : controlsignal + | ctrl_clk : controlsignal + | ctrl_param (idx : nat) : controlsignal. + +Definition controlsignal_sz (s : controlsignal) : nat := + match s with + | ctrl_param _ => 32 + | ctrl_return => 32 + | _ => 1 + end. + Record module: Type := mkmodule { mod_params : list reg; @@ -88,6 +107,10 @@ Record module: Type := mod_clk : reg; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); + (** Map from registers in this module to control registers in other modules. + These will be mapped to the same verilog register. *) + mod_externctrl : AssocMap.t (ident * controlsignal); + mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); mod_ram : option ram; mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath; mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk; @@ -108,31 +131,59 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := Definition empty_stack (m : module) : Verilog.assocmap_arr := (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)). + +Definition prog_modmap (p : HTL.program) := + PTree_Properties.of_list (Option.map_option + (fun a => match a with + | (ident, (AST.Gfun (AST.Internal f))) => Some (ident, f) + | _ => None + end) + (AST.prog_defs p)). + +Lemma max_pc_wf : + forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + @map_well_formed T m. +Proof. + unfold map_well_formed. intros. + exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. + apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. + unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. + simplify. transitivity (Z.pos (max_pc_map m)); eauto. +Qed. + (** * Operational Semantics *) Definition genv := Globalenvs.Genv.t fundef unit. +Definition find_func {F V} (ge : Globalenvs.Genv.t F V) (symb : AST.ident) : option F := + match Globalenvs.Genv.find_symbol ge symb with + | None => None + | Some b => Globalenvs.Genv.find_funct_ptr ge b + end. + Inductive stackframe : Type := - Stackframe : - forall (res : reg) - (m : module) - (pc : 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) (** Name of the callee *) (v : value), state | Callstate : forall (stack : list stackframe) + (mid : ident) (m : module) (args : list value), state. @@ -172,7 +223,7 @@ Inductive exec_ram: Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : - forall g m st sf ctrl data + forall g mid m st sf ctrl_stmnt data_stmnt asr asa basr1 basa1 nasr1 nasa1 basr2 basa2 nasr2 nasa2 @@ -182,19 +233,19 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asr!(mod_reset m) = Some (ZToValue 0) -> asr!(mod_finish m) = Some (ZToValue 0) -> asr!(m.(mod_st)) = Some (posToValue st) -> - m.(mod_controllogic)!st = Some ctrl -> - m.(mod_datapath)!st = Some data -> + m.(mod_controllogic)!st = Some ctrl_stmnt -> + m.(mod_datapath)!st = Some data_stmnt -> Verilog.stmnt_runp f (Verilog.mkassociations asr empty_assocmap) (Verilog.mkassociations asa (empty_stack m)) - ctrl + ctrl_stmnt (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) -> basr1!(m.(mod_st)) = Some (posToValue st) -> Verilog.stmnt_runp f (Verilog.mkassociations basr1 nasr1) (Verilog.mkassociations basa1 nasa1) - data + data_stmnt (Verilog.mkassociations basr2 nasr2) (Verilog.mkassociations basa2 nasa2) -> exec_ram @@ -206,27 +257,61 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := asr' = Verilog.merge_regs nasr3 basr3 -> asa' = Verilog.merge_arrs nasa3 basa3 -> asr'!(m.(mod_st)) = Some (posToValue pstval) -> - (Z.pos pstval <= Integers.Int.max_unsigned)%Z -> - step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') + Z.pos pstval <= Integers.Int.max_unsigned -> + 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, + forall g m st asr asa retval sf mid, asr!(m.(mod_finish)) = Some (ZToValue 1) -> asr!(m.(mod_return)) = Some retval -> - step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) + + step g + (State sf mid m st asr asa) Events.E0 + (Returnstate sf mid retval) +| step_initcall : + forall g callerid caller st asr asa sf callee_id callee callee_reset callee_params callee_param_vals, + find_func g callee_id = Some (AST.Internal callee) -> + + 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!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_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 i r sf pc mst, - mst = mod_st m -> - step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 - (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). + forall g callerid caller asr asa callee_id callee_return callee_finish i sf pc mst, + mst = mod_st caller -> + + caller.(mod_externctrl)!callee_return = Some (callee_id, ctrl_return) -> + caller.(mod_externctrl)!callee_finish = Some (callee_id, ctrl_finish) -> + + 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 := @@ -235,12 +320,12 @@ 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 retvali, +| final_state_intro : forall retval mid retvali, retvali = valueToInt retval -> - final_state (Returnstate nil retval) retvali. + final_state (Returnstate nil mid retval) retvali. Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state diff --git a/src/hls/HTLBlockgen.v b/src/hls/HTLBlockgen.v index 5f40962..b9fc1d9 100644 --- a/src/hls/HTLBlockgen.v +++ b/src/hls/HTLBlockgen.v @@ -43,8 +43,8 @@ Definition init_state (st : reg) : state := 1%positive (AssocMap.empty (option io * scl_decl)) (AssocMap.empty (option io * arr_decl)) - (AssocMap.empty stmnt) - (AssocMap.empty stmnt). + (AssocMap.empty datapath_stmnt) + (AssocMap.empty control_stmnt). Module HTLState <: State. @@ -87,11 +87,17 @@ Module HTLMonadExtra := Monad.MonadExtra(HTLMonad). Import HTLMonadExtra. Export MonadNotation. -Definition state_goto (st : reg) (n : node) : stmnt := - Vnonblock (Vvar st) (Vlit (posToValue n)). +Definition data_vstmnt : Verilog.stmnt -> HTL.datapath_stmnt := HTLDataVstmnt. +Definition ctrl_vstmnt : Verilog.stmnt -> HTL.control_stmnt := HTLCtrlVstmnt. -Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := - Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). +Definition state_goto (st : reg) (n : node) : control_stmnt := + ctrl_vstmnt (Vnonblock (Vvar st) (Vlit (posToValue n))). + +Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : control_stmnt := + ctrl_vstmnt (Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2))). + +Definition nonblock (dst : reg) (e : expr) := (Vnonblock (Vvar dst) e). +Definition block (dst : reg) (e : expr) := (Vblock (Vvar dst) e). Definition check_empty_node_datapath: forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. @@ -105,25 +111,6 @@ Proof. intros. case (s.(st_controllogic)!n); tauto. Defined. -Lemma add_instr_state_incr : - forall s n n' st, - (st_datapath s)!n = None -> - (st_controllogic s)!n = None -> - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). -Proof. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Qed. - Lemma declare_reg_state_incr : forall i s r sz, st_incr s @@ -148,7 +135,50 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := s.(st_controllogic)) (declare_reg_state_incr i s r sz). -Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := +Lemma create_state_state_incr: + forall s, + st_incr s (mkstate + s.(st_st) + (st_freshreg s) + (Pos.succ (st_freshstate s)) + (st_scldecls s) + (st_arrdecls s) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_state : mon node := + fun s => let r := s.(st_freshstate) in + OK r (mkstate + s.(st_st) + (st_freshreg s) + (Pos.succ (st_freshstate s)) + (st_scldecls s) + (st_arrdecls s) + (st_datapath s) + (st_controllogic s)) + (create_state_state_incr s). + +Lemma add_instr_state_incr : + forall s n n' st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with | left STM, left TRANS => @@ -176,14 +206,33 @@ Lemma add_instr_skip_state_incr : s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))). + (AssocMap.set n (ctrl_vstmnt Vskip) s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Lemma add_instr_wait_state_incr : + forall wait_mod s n n' st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (HTLwait wait_mod s.(st_st) (Vlit (posToValue n'))) s.(st_controllogic))). Proof. constructor; intros; try (simpl; destruct (peq n n0); subst); auto with htlh. Qed. -Definition add_instr_skip (n : node) (st : stmnt) : mon unit := +Definition add_instr_wait (wait_mod : ident) (n : node) (n' : node) (st : datapath_stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with | left STM, left TRANS => @@ -194,7 +243,23 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit := s.(st_scldecls) s.(st_arrdecls) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))) + (AssocMap.set n (HTLwait wait_mod s.(st_st) (Vlit (posToValue n'))) s.(st_controllogic))) + (add_instr_wait_state_incr wait_mod s n n' st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr_wait") + end. + +Definition add_instr_skip (n : node) (st : datapath_stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (ctrl_vstmnt Vskip) s.(st_controllogic))) (add_instr_skip_state_incr s n st STM TRANS) | _, _ => Error (Errors.msg "HTL.add_instr") end. @@ -210,7 +275,7 @@ Lemma add_node_skip_state_incr : (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n (data_vstmnt Vskip) s.(st_datapath)) (AssocMap.set n st s.(st_controllogic))). Proof. constructor; intros; @@ -218,7 +283,7 @@ Proof. auto with htlh. Qed. -Definition add_node_skip (n : node) (st : stmnt) : mon unit := +Definition add_node_skip (n : node) (st : control_stmnt) : mon unit := fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with | left STM, left TRANS => @@ -228,15 +293,12 @@ Definition add_node_skip (n : node) (st : stmnt) : mon unit := (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n (data_vstmnt Vskip) s.(st_datapath)) (AssocMap.set n st s.(st_controllogic))) (add_node_skip_state_incr s n st STM TRANS) | _, _ => Error (Errors.msg "HTL.add_instr") end. -Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. -Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. - Definition bop (op : binop) (r1 r2 : reg) : expr := Vbinop op (Vvar r1) (Vvar r2). @@ -386,7 +448,7 @@ Lemma add_branch_instr_state_incr: (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (data_vstmnt Vskip) (st_datapath s)) (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). Proof. intros. apply state_incr_intro; simpl; @@ -404,7 +466,7 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (data_vstmnt Vskip) (st_datapath s)) (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") @@ -450,26 +512,33 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni match i with | Inop n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then - add_instr n n' Vskip + add_instr n n' (data_vstmnt Vskip) else error (Errors.msg "State is larger than 2^32.") | Iop op args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then do instr <- translate_instr op args; do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst instr) + add_instr n n' (data_vstmnt (nonblock dst instr)) else error (Errors.msg "State is larger than 2^32.") | Iload mem addr args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then do src <- translate_arr_access mem addr args stack; do _ <- declare_reg None dst 32; - add_instr n n' (nonblock dst src) + add_instr n n' (data_vstmnt (nonblock dst src)) else error (Errors.msg "State is larger than 2^32.") | Istore mem addr args src n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then do dst <- translate_arr_access mem addr args stack; - add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + add_instr n n' (data_vstmnt (Vnonblock dst (Vvar src))) (* TODO: Could juse use add_instr? reg exists. *) + else error (Errors.msg "State is larger than 2^32.") + | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.") + | Icall sig (inr fn) args dst n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do _ <- declare_reg None dst 32; + do join_state <- create_state; + do _ <- add_instr n join_state (HTLfork fn args); + add_instr_wait fn join_state n' (HTLjoin fn dst) else error (Errors.msg "State is larger than 2^32.") - | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") | Icond cond args n1 n2 => @@ -484,9 +553,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Ireturn r => match r with | Some r' => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))) + add_instr_skip n (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))) | None => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))) + add_instr_skip n (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))) end end end. @@ -542,11 +611,11 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). -Definition max_pc_map (m : Maps.PTree.t stmnt) := +Definition max_pc_map {A: Type} (m : Maps.PTree.t A) := PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. Lemma max_pc_map_sound: - forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). + forall A m pc i, m!pc = Some i -> Ple pc (@max_pc_map A m). Proof. intros until i. unfold max_pc_function. apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). @@ -561,8 +630,8 @@ Proof. Qed. Lemma max_pc_wf : - forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> - map_well_formed m. + forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + @map_well_formed T m. Proof. unfold map_well_formed. intros. exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. @@ -600,7 +669,7 @@ Definition transf_module (f: function) : mon module := clk current_state.(st_scldecls) current_state.(st_arrdecls) - (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) + (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) | _, _ => error (Errors.msg "More than 2^32 states.") end else error (Errors.msg "Stack size misalignment."). diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 9e1f156..d292722 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -57,8 +57,8 @@ Definition init_state (st : reg) : state := 1%positive (AssocMap.empty (option io * scl_decl)) (AssocMap.empty (option io * arr_decl)) - (AssocMap.empty stmnt) - (AssocMap.empty stmnt). + (AssocMap.empty datapath_stmnt) + (AssocMap.empty control_stmnt). Module HTLState <: State. @@ -516,13 +516,13 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := (st_controllogic s)) (create_arr_state_incr s sz ln i). -Definition max_pc_map (m : Maps.PTree.t stmnt) := +Definition max_pc_map {A: Type} (m : Maps.PTree.t A) := PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. Lemma max_pc_map_sound: - forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). + forall A m pc i, m!pc = Some i -> Ple pc (@max_pc_map A m). Proof. - intros until i. + intros until i. unfold max_pc_function. apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). (* extensionality *) intros. apply H0. rewrite H; auto. @@ -530,14 +530,13 @@ Proof. rewrite PTree.gempty. congruence. (* inductive case *) intros. rewrite PTree.gsspec in H2. destruct (peq pc k). - inv H2. unfold Ple, Plt in *. lia. - apply Ple_trans with a. auto. - unfold Ple, Plt in *. lia. + inv H2. xomega. + apply Ple_trans with a. auto. xomega. Qed. Lemma max_pc_wf : - forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> - map_well_formed m. + forall T m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + @map_well_formed T m. Proof. unfold map_well_formed. intros. exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. @@ -591,7 +590,8 @@ Definition add_data_instr (n : node) (st : stmnt) : mon unit := (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) - (AssocMap.set n (Vseq (AssocMapExt.get_default _ Vskip n s.(st_datapath)) st) s.(st_datapath)) + (AssocMap.set n (Vseq (AssocMapExt.get_default + _ Vskip n s.(st_datapath)) st) s.(st_datapath)) s.(st_controllogic)) (add_data_instr_state_incr s n st). @@ -655,7 +655,6 @@ Abort. (AssocMap.set n st s.(st_controllogic))) (add_control_instr_force_state_incr s n st). - Fixpoint pred_expr (preg: reg) (p: pred_op) := match p with | Pvar pred => diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 4d60a24..0b7f3ec 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -21,6 +21,7 @@ Require Import Coq.micromega.Lia. Require Import compcert.lib.Maps. Require compcert.common.Errors. +Require Import compcert.lib.Integers. Require compcert.common.Globalenvs. Require compcert.lib.Integers. Require Import compcert.common.AST. @@ -28,6 +29,7 @@ Require Import compcert.backend.RTL. Require Import vericert.common.Statemonad. Require Import vericert.common.Vericertlib. +Require Import vericert.common.Maps. Require Import vericert.hls.AssocMap. Require Import vericert.hls.HTL. Require Import vericert.hls.ValueInt. @@ -45,6 +47,7 @@ Record state: Type := mkstate { st_freshstate: node; st_scldecls: AssocMap.t (option io * scl_decl); st_arrdecls: AssocMap.t (option io * arr_decl); + st_externctrl : AssocMap.t (ident * controlsignal); st_datapath: datapath; st_controllogic: controllogic; }. @@ -55,38 +58,64 @@ Definition init_state (st : reg) : state := 1%positive (AssocMap.empty (option io * scl_decl)) (AssocMap.empty (option io * arr_decl)) - (AssocMap.empty stmnt) - (AssocMap.empty stmnt). + (AssocMap.empty (ident * controlsignal)) + (AssocMap.empty datapath_stmnt) + (AssocMap.empty control_stmnt). + +(** Describes a map that is created incrementally in the monad, i.e. only new + values can be added, not changed or deleted. *) +Definition map_incr {S B} (map : S -> PTree.t B) (s1 s2 : S) := + forall n, s1.(map)!n = None \/ + s2.(map)!n = s1.(map)!n. +Hint Unfold map_incr : htlh. Module HTLState <: State. Definition st := state. Inductive st_incr: state -> state -> Prop := - state_incr_intro: + | state_incr_intro: forall (s1 s2: state), - st_st s1 = st_st s2 -> - Ple s1.(st_freshreg) s2.(st_freshreg) -> - Ple s1.(st_freshstate) s2.(st_freshstate) -> - (forall n, - s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -> - (forall n, - s1.(st_controllogic)!n = None - \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> - st_incr s1 s2. + st_st s1 = st_st s2 -> + Ple s1.(st_freshreg) s2.(st_freshreg) -> + Ple s1.(st_freshstate) s2.(st_freshstate) -> + map_incr st_datapath s1 s2 -> + map_incr st_controllogic s1 s2 -> + map_incr st_externctrl s1 s2 -> + (forall n, (st_externctrl s1) ! n = None -> + (exists x, (st_externctrl s2) ! n = Some x) -> + (n >= st_freshreg s1)%positive) -> + st_incr s1 s2. Hint Constructors st_incr : htlh. Definition st_prop := st_incr. Hint Unfold st_prop : htlh. - Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. + Lemma st_refl : forall s, st_prop s s. + Proof. split; try solve [ auto with htlh; crush ]. Qed. Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. Proof. - intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence. - - destruct H4 with n; destruct H8 with n; intuition congruence. - - destruct H5 with n; destruct H9 with n; intuition congruence. + intros * H0 H1. inv H0. inv H1. + split; autounfold with htlh in *; intros; try solve [crush]. + - destruct H4 with n; destruct H10 with n; intuition crush. + - destruct H5 with n; destruct H11 with n; intuition crush. + - destruct H6 with n; destruct H12 with n; intuition crush. + - destruct H6 with n; destruct H12 with n. + + specialize (H13 n ltac:(auto) ltac:(auto)). + crush. + + apply H7; auto. + rewrite <- H16. + auto. + + specialize (H13 n ltac:(auto) ltac:(auto)). + unfold Ple in *. + lia. + + contradict H14. + rewrite H16. + rewrite H15. + rewrite H1. + intuition crush. Qed. End HTLState. @@ -99,12 +128,28 @@ Module HTLMonadExtra := Monad.MonadExtra(HTLMonad). Import HTLMonadExtra. Export MonadNotation. -Definition state_goto (st : reg) (n : node) : stmnt := +Definition bop (op : binop) (r1 r2 : reg) : expr := + Vbinop op (Vvar r1) (Vvar r2). + +Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := + Vbinop op (Vvar r) (Vlit (intToValue l)). + +Definition boplitz (op: binop) (r: reg) (l: Z) : expr := + Vbinop op (Vvar r) (Vlit (ZToValue l)). + +Definition state_goto (st : reg) (n : node) : control_stmnt := Vnonblock (Vvar st) (Vlit (posToValue n)). -Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := +Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : control_stmnt := Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). +Definition state_wait (st wait_reg : reg) (n : node) : control_stmnt := + Vcond (boplitz Veq wait_reg 1) (Vnonblock (Vvar st) (posToExpr n)) Vskip. + +Definition nonblock (dst : reg) (e : expr) := (Vnonblock (Vvar dst) e). + +Definition block (dst : reg) (e : expr) := (Vblock (Vvar dst) e). + Definition check_empty_node_datapath: forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. Proof. @@ -117,146 +162,140 @@ Proof. intros. case (s.(st_controllogic)!n); tauto. Defined. -Lemma add_instr_state_incr : - forall s n n' st, - (st_datapath s)!n = None -> - (st_controllogic s)!n = None -> - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). +Definition check_unmapped_externctrl: + forall (s: state) (n: reg), { s.(st_externctrl)!n = None } + { True }. Proof. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Qed. + intros. case (s.(st_externctrl)!n); tauto. +Defined. -Lemma declare_reg_state_incr : - forall i s r sz, - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - s.(st_freshstate) - (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - s.(st_datapath) - s.(st_controllogic)). -Proof. auto with htlh. Qed. +(** Used for discharging the st_incr proof in simple operations *) +Local Ltac st_tac := + constructor; autounfold with htlh in *; intros; simpl; auto with htlh; + match goal with + | [ H : (?map ?s) ! ?n = None, n' : positive |- _] => destruct (peq n n') + end; + subst; auto with htlh; intuition crush. Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := fun s => OK tt (mkstate - s.(st_st) - s.(st_freshreg) - s.(st_freshstate) - (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - s.(st_datapath) - s.(st_controllogic)) - (declare_reg_state_incr i s r sz). - -Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := - fun s => - match check_empty_node_datapath s n, check_empty_node_controllogic s n with - | left STM, left TRANS => - OK tt (mkstate + (st_st s) + (st_freshreg s) + (st_freshstate s) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) + (st_arrdecls s) + (st_externctrl s) + (st_datapath s) + (st_controllogic s)) ltac:(st_tac). + +Definition create_reg (i : option io) (sz : nat) : mon reg := + fun s => let r := s.(st_freshreg) in + OK r (mkstate + (st_st s) + (Pos.succ r) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + (st_arrdecls s) + (st_externctrl s) + (st_datapath s) + (st_controllogic s)) ltac:(st_tac). + +Definition map_externctrl (othermod : ident) (ctrl : controlsignal) : mon reg. + refine ( + fun s => match check_unmapped_externctrl s (st_freshreg s) with + | left CTRL => OK (st_freshreg s) (mkstate + (st_st s) + (st_freshreg s) + (st_freshstate s) + (st_scldecls s) + (st_arrdecls s) + (AssocMap.set (st_freshreg s) (othermod, ctrl) (st_externctrl s)) + (st_datapath s) + (st_controllogic s)) _ + | right CTRL => Error (Errors.msg "HTL.map_externctrl") + end). + st_tac. + rewrite PTree.gsspec in *. + destruct_match; crush. +Defined. + +Definition create_state : mon node. + refine (fun s => let r := s.(st_freshstate) in + if Z.leb (Z.pos s.(st_freshstate)) Integers.Int.max_unsigned + then OK r (mkstate + (st_st s) + (st_freshreg s) + (Pos.succ (st_freshstate s)) + (st_scldecls s) + (st_arrdecls s) + (st_externctrl s) + (st_datapath s) + (st_controllogic s)) _ + else Error (Errors.msg "HTL.create_state")). + split; autounfold with htlh; crush. +Defined. + +Lemma create_state_max : forall s s' i x, create_state s = OK x s' i -> Z.pos x <= Int.max_unsigned. +Admitted. + +Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon unit := + fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate s.(st_st) s.(st_freshreg) (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) + (st_externctrl s) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) - (add_instr_state_incr s n n' st STM TRANS) - | _, _ => Error (Errors.msg "HTL.add_instr") - end. - -Lemma add_instr_skip_state_incr : - forall s n st, - (st_datapath s)!n = None -> - (st_controllogic s)!n = None -> - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))). -Proof. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Qed. - -Definition add_instr_skip (n : node) (st : stmnt) : mon unit := - fun s => - match check_empty_node_datapath s n, check_empty_node_controllogic s n with - | left STM, left TRANS => - OK tt (mkstate + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) ltac:(st_tac) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + +Definition add_instr_wait (wait_reg : reg) (n : node) (n' : node) (st : datapath_stmnt) : mon unit := + fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate s.(st_st) s.(st_freshreg) (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) + (st_externctrl s) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))) - (add_instr_skip_state_incr s n st STM TRANS) - | _, _ => Error (Errors.msg "HTL.add_instr") - end. - -Lemma add_node_skip_state_incr : - forall s n st, - (st_datapath s)!n = None -> - (st_controllogic s)!n = None -> - st_incr s - (mkstate - s.(st_st) - s.(st_freshreg) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n Vskip s.(st_datapath)) - (AssocMap.set n st s.(st_controllogic))). -Proof. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Qed. - -Definition add_node_skip (n : node) (st : stmnt) : mon unit := - fun s => - match check_empty_node_datapath s n, check_empty_node_controllogic s n with - | left STM, left TRANS => - OK tt (mkstate + (AssocMap.set n (state_wait (st_st s) wait_reg n') s.(st_controllogic))) ltac:(st_tac) + | _, _ => Error (Errors.msg "HTL.add_instr_wait") + end. + +Definition add_instr_skip (n : node) (st : datapath_stmnt) : mon unit := + fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate s.(st_st) s.(st_freshreg) (st_freshstate s) s.(st_scldecls) s.(st_arrdecls) + (st_externctrl s) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))) ltac:(st_tac) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + +Definition add_node_skip (n : node) (st : control_stmnt) : mon unit := + fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (st_externctrl s) (AssocMap.set n Vskip s.(st_datapath)) - (AssocMap.set n st s.(st_controllogic))) - (add_node_skip_state_incr s n st STM TRANS) - | _, _ => Error (Errors.msg "HTL.add_instr") - end. - -Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. -Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. - -Definition bop (op : binop) (r1 r2 : reg) : expr := - Vbinop op (Vvar r1) (Vvar r2). - -Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := - Vbinop op (Vvar r) (Vlit (intToValue l)). - -Definition boplitz (op: binop) (r: reg) (l: Z) : expr := - Vbinop op (Vvar r) (Vlit (ZToValue l)). + (AssocMap.set n st s.(st_controllogic))) ltac:(st_tac) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr := match c, args with @@ -370,10 +409,12 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Oshlimm n, r::nil => ret (boplit Vshl r n) | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) - | Op.Oshrximm n, r::nil => - ret (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0))) - (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n))) - (Vbinop Vshru (Vvar r) (Vlit n))) + | Op.Oshrximm n, r::nil => ret (Vternary (Vbinop Vlt (Vvar r) (Vlit (ZToValue 0))) + (Vunop Vneg (Vbinop Vshru (Vunop Vneg (Vvar r)) (Vlit n))) + (Vbinop Vshru (Vvar r) (Vlit n))) + (*ret (Vbinop Vdiv (Vvar r) + (Vbinop Vshl (Vlit (ZToValue 1)) + (Vlit (intToValue n))))*) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") @@ -388,39 +429,20 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") end. -Lemma add_branch_instr_state_incr: - forall s e n n1 n2, - (st_datapath s) ! n = None -> - (st_controllogic s) ! n = None -> - st_incr s (mkstate - s.(st_st) - (st_freshreg s) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n Vskip (st_datapath s)) - (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). -Proof. - intros. apply state_incr_intro; simpl; - try (intros; destruct (peq n0 n); subst); - auto with htlh. -Qed. - Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := - fun s => - match check_empty_node_datapath s n, check_empty_node_controllogic s n with - | left NSTM, left NTRANS => - OK tt (mkstate + fun s => match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left NSTM, left NTRANS => + OK tt (mkstate s.(st_st) - (st_freshreg s) - (st_freshstate s) - s.(st_scldecls) - s.(st_arrdecls) - (AssocMap.set n Vskip (st_datapath s)) - (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) - (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) - | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") - end. + (st_freshreg s) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (st_externctrl s) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) ltac:(st_tac) + | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") + end. Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) (args : list reg) (stack : reg) : mon expr := @@ -456,7 +478,47 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := end) (enumerate 0 ns). -Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := +Fixpoint nonblock_all pairs := + match pairs with + | (dst, src) :: pairs' => Vseq (nonblock dst (Vvar src)) (nonblock_all pairs') + | nil => Vskip + end. + +(** [fork] a datapath statement which sets up the execution of a function *) +Definition fork (rst : reg) (params : list (reg * reg)) : datapath_stmnt := + let reset_mod := Vnonblock (Vvar rst) (posToLit 1) in + let assign_params := nonblock_all params in + Vseq reset_mod assign_params. + +Definition join (fn_rtrn fn_rst fn_dst : reg) : datapath_stmnt := + let set_result := Vnonblock (Vvar fn_dst) (Vvar fn_rtrn) in + let stop_reset := Vnonblock (Vvar fn_rst) (Vlit (ZToValue 0)) in + Vseq stop_reset set_result. + +Definition return_val r := + match r with + | Some r' => Vvar r' + | None => Vlit (ZToValue 0%Z) + end. + +Definition do_return fin rtrn r := + Vseq (block fin (Vlit (ZToValue 1%Z))) + (block rtrn (return_val r)). + +Definition idle fin := nonblock fin (Vlit (ZToValue 0%Z)). + +Fixpoint xmap_externctrl_params (n : nat) (fn : ident) (l : list reg) := + match l with + | nil => ret nil + | arg::args => + do param_reg <- map_externctrl fn (ctrl_param n); + do rest <- xmap_externctrl_params (S n) fn args; + ret ((param_reg, arg) :: rest) + end. + +Definition map_externctrl_params := xmap_externctrl_params 0. + +Definition transf_instr (ge : RTL.genv) (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with (n, i) => match i with @@ -481,7 +543,28 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni do dst <- translate_arr_access mem addr args stack; add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) else error (Errors.msg "State is larger than 2^32.") - | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") + | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.") + | Icall sig (inr fn) args dst n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned + then match find_func ge fn with + | Some (AST.Internal _) => + do params <- map_externctrl_params fn args; + + do _ <- declare_reg None dst 32; + do join_state <- create_state; + + do finish_reg <- map_externctrl fn ctrl_finish; + do reset_reg <- map_externctrl fn ctrl_reset; + do return_reg <- map_externctrl fn ctrl_return; + + let fork_instr := fork reset_reg params in + let join_instr := join return_reg reset_reg dst in + + do _ <- add_instr n join_state fork_instr; + add_instr_wait finish_reg join_state n' join_instr + | _ => error (Errors.msg "Call to non-internal function") + end + else error (Errors.msg "State is larger than 2^32.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") | Icond cond args n1 n2 => @@ -494,68 +577,28 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*) error (Errors.msg "Ijumptable: Case statement not supported.") | Ireturn r => - match r with - | Some r' => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))) - | None => - add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))) - end + do idle_state <- create_state; + do _ <- add_instr n idle_state (do_return fin rtrn r); + add_instr_skip idle_state (idle fin) end end. -Lemma create_reg_state_incr: - forall s sz i, - st_incr s (mkstate - s.(st_st) - (Pos.succ (st_freshreg s)) - (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) - s.(st_arrdecls) - (st_datapath s) - (st_controllogic s)). -Proof. constructor; simpl; auto with htlh. Qed. - -Definition create_reg (i : option io) (sz : nat) : mon reg := - fun s => let r := s.(st_freshreg) in - OK r (mkstate - s.(st_st) - (Pos.succ r) - (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) - (st_arrdecls s) - (st_datapath s) - (st_controllogic s)) - (create_reg_state_incr s sz i). - -Lemma create_arr_state_incr: - forall s sz ln i, - st_incr s (mkstate - s.(st_st) - (Pos.succ (st_freshreg s)) - (st_freshstate s) - s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) - (st_datapath s) - (st_controllogic s)). -Proof. constructor; simpl; auto with htlh. Qed. - Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := fun s => let r := s.(st_freshreg) in - OK (r, ln) (mkstate - s.(st_st) - (Pos.succ r) - (st_freshstate s) - s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) - (st_datapath s) - (st_controllogic s)) - (create_arr_state_incr s sz ln i). + OK (r, ln) (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + s.(st_scldecls) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) + (st_externctrl s) + (st_datapath s) + (st_controllogic s)) ltac:(st_tac). Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). -Definition max_pc_map (m : Maps.PTree.t stmnt) := - PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. +Definition declare_params params := collectlist (fun r => declare_reg (Some Vinput) r 32) params. Lemma max_pc_map_sound: forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). @@ -597,14 +640,14 @@ Defined. Definition transf_module (f: function) : mon HTL.module. refine ( if stack_correct f.(fn_stacksize) then + do _ <- declare_params (RTL.fn_params f); do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); - do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); - do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); do start <- create_reg (Some Vinput) 1; do rst <- create_reg (Some Vinput) 1; do clk <- create_reg (Some Vinput) 1; + do _ <- collectlist (transf_instr ge fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); do current_state <- get; match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned, @@ -627,6 +670,7 @@ Definition transf_module (f: function) : mon HTL.module. clk current_state.(st_scldecls) current_state.(st_arrdecls) + current_state.(st_externctrl) None (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)) MORD @@ -644,13 +688,23 @@ Definition max_state (f: function) : state := (Pos.succ (RTL.max_pc_function f)) (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) (st_arrdecls (init_state st)) + (st_externctrl (init_state st)) (st_datapath (init_state st)) (st_controllogic (init_state st)). -Definition transl_module (f : function) : Errors.res HTL.module := - run_mon (max_state f) (transf_module f). +Definition prog_funmap (prog : RTL.program) : (PTree.t RTL.fundef) := + AssocMap_Properties.of_list ( + Option.map_option (fun '(ident, def) => match def with + | AST.Gfun f => Some (ident, f) + | _ => None + end) + (AST.prog_defs prog) + ). + +Definition transl_module (prog : RTL.program) (f : function) : Errors.res HTL.module := + run_mon (max_state f) (transf_module (Globalenvs.Genv.globalenv prog) (AST.prog_main prog) f). -Definition transl_fundef := transf_partial_fundef transl_module. +Definition transl_fundef prog := transf_partial_fundef (transl_module prog). Definition main_is_internal (p : RTL.program) : bool := let ge := Globalenvs.Genv.globalenv p in @@ -665,5 +719,5 @@ Definition main_is_internal (p : RTL.program) : bool := Definition transl_program (p : RTL.program) : Errors.res HTL.program := if main_is_internal p - then transform_partial_program transl_fundef p + then transform_partial_program (transl_fundef p) p else Errors.Error (Errors.msg "Main function is not Internal."). diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 1aac3b7..c2cbbf8 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -24,10 +24,12 @@ Require Import compcert.common.Globalenvs. Require Import compcert.common.Linking. Require Import compcert.common.Memory. Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. Require Import vericert.common.IntegerExtra. Require Import vericert.common.Vericertlib. Require Import vericert.common.ZExtra. +Require Import vericert.common.ListExtra. Require Import vericert.hls.Array. Require Import vericert.hls.AssocMap. Require vericert.hls.HTL. @@ -46,6 +48,8 @@ Hint Resolve AssocMap.gso : htlproof. Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. +Hint Constructors val_value_lessdef : htlproof. + Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := match_assocmap : forall f rs am, (forall r, Ple r (RTL.max_reg_function f) -> @@ -54,12 +58,12 @@ 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. -Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : +Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : Memory.mem) : Verilog.assocmap_arr -> Prop := | match_arr : forall asa stack, asa ! (m.(HTL.mod_stk)) = Some stack /\ @@ -78,6 +82,12 @@ Definition stack_based (v : Values.val) (sp : Values.block) : Prop := | _ => True end. +Definition not_pointer (v : Values.val) : Prop := + match v with + | Values.Vptr _ _ => False + | _ => True + end. + Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop := forall r, stack_based (Registers.Regmap.get r rs) sp. @@ -98,10 +108,6 @@ Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop := Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\ Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None. -Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop := -| match_frames_nil : - match_frames nil nil. - Inductive match_constants : HTL.module -> assocmap -> Prop := match_constant : forall m asr, @@ -109,34 +115,72 @@ Inductive match_constants : HTL.module -> assocmap -> Prop := asr!(HTL.mod_finish m) = Some (ZToValue 0) -> 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 res +(** The caller needs to have externctrl signals for the current module *) +Definition has_externctrl (caller : HTL.module) (current_id : HTL.ident) (ret rst fin : HTL.reg) := + (HTL.mod_externctrl caller)!ret = Some (current_id, HTL.ctrl_return) /\ + (HTL.mod_externctrl caller)!rst = Some (current_id, HTL.ctrl_reset) /\ + (HTL.mod_externctrl caller)!fin = Some (current_id, HTL.ctrl_finish). + +Inductive match_frames (ge : RTL.genv) (current_id : HTL.ident) (mem : Memory.mem) + : (list RTL.stackframe) -> (list HTL.stackframe) -> Prop := +| match_frames_nil : + match_frames ge current_id mem nil nil +| match_frames_cons : + forall dst f sp sp' rs mid m pc st asr asa rtl_tl htl_tl ret rst fin + (MASSOC : match_assocmaps f rs asr) + (TF : tr_module ge f m) + (MARR : match_arrs m f sp mem asa) + (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) + (RSBP : reg_stack_based_pointers sp' rs) + (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) + (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem) + (CONST : match_constants m asr) + (EXTERN_CALLER : has_externctrl m current_id ret rst fin) + (JOIN_CTRL : (HTL.mod_controllogic m)!st = Some (state_wait (HTL.mod_st m) fin pc)) + (JOIN_DATA : (HTL.mod_datapath m)!st = Some (join ret rst dst)) + (TAILS : match_frames ge mid mem rtl_tl htl_tl) + (DST : Ple dst (RTL.max_reg_function f)) + (PC : (Z.pos pc <= Int.max_unsigned)), + match_frames ge current_id mem + ((RTL.Stackframe dst f sp pc rs) :: rtl_tl) + ((HTL.Stackframe mid m st asr asa) :: htl_tl). + +Inductive match_states (ge : RTL.genv) : RTL.state -> HTL.state -> Prop := +| 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) + (TF : tr_module ge f m) + (WF : state_st_wf m (HTL.State res mid m st asr asa)) + (MF : match_frames ge mid mem 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) (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) (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 asr asa) + match_states ge + (RTL.State sf f sp st rs mem) + (HTL.State res mid m st asr asa) | match_returnstate : - forall - v v' stack mem res - (MF : match_frames stack res), - val_value_lessdef v v' -> - match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v') -| match_initial_call : - forall f m m0 - (TF : tr_module f m), - match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil). + forall v v' rtl_stk htl_stk mem mid + (MF : match_frames ge mid mem rtl_stk htl_stk) + (MV : val_value_lessdef v v') + (NP : not_pointer v), + match_states ge + (RTL.Returnstate rtl_stk v mem) + (HTL.Returnstate htl_stk mid v') +| match_call : + forall f m rtl_args htl_args mid mem rtl_stk htl_stk + (TF : tr_module ge f m) + (MF : match_frames ge mid mem rtl_stk htl_stk) + (NP : Forall not_pointer rtl_args) + (MARGS : list_forall2 val_value_lessdef rtl_args htl_args), + match_states ge + (RTL.Callstate rtl_stk (AST.Internal f) rtl_args mem) + (HTL.Callstate htl_stk mid m htl_args). Hint Constructors match_states : htlproof. Definition match_prog (p: RTL.program) (tp: HTL.program) := - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ + Linking.match_program (fun cu f tf => transl_fundef p f = Errors.OK tf) eq p tp /\ main_is_internal p = true. Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program): @@ -158,7 +202,7 @@ Proof. Qed. Definition match_prog' (p: RTL.program) (tp: HTL.program) := - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + Linking.match_program (fun cu f tf => transl_fundef p f = Errors.OK tf) eq p tp. Lemma match_prog_matches : forall p tp, match_prog p tp -> match_prog' p tp. @@ -174,6 +218,15 @@ Proof. assumption. Qed. +Lemma regs_lessdef_empty : forall f, match_assocmaps f (Registers.Regmap.init Values.Vundef) empty_assocmap. +Proof. + constructor. intros. + unfold Registers.Regmap.init, "_ !! _", "_ # _", empty_assocmap, AssocMapExt.get_default. + repeat rewrite PTree.gempty. + constructor. +Qed. +Hint Resolve regs_lessdef_empty : htlproof. + Lemma regs_lessdef_add_greater : forall f rs1 rs2 n v, Plt (RTL.max_reg_function f) n -> @@ -296,19 +349,24 @@ Proof. assumption. Qed. +Lemma option_inv : + forall A x y, + @Some A x = Some y -> x = y. +Proof. intros. inversion H. trivial. Qed. + Ltac inv_state := match goal with - MSTATE : match_states _ _ |- _ => + MSTATE : match_states _ _ _ |- _ => inversion MSTATE; match goal with - TF : tr_module _ _ |- _ => + TF : tr_module _ _ _ |- _ => 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 + try match goal with TI : context[tr_instr] |- _ => inversion TI end @@ -325,6 +383,17 @@ Ltac unfold_func H := | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H) end. +Ltac not_control_reg := + solve [ + unfold Ple, Plt in *; + try multimatch goal with + | [ H : forall r, (exists x, _ ! r = Some x) -> (r > _)%positive + |- context[?r'] + ] => pose proof (H r' ltac:(eauto)) + end; + lia + ]. + Lemma init_reg_assoc_empty : forall f l, match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l). @@ -355,14 +424,51 @@ Section CORRECTNESS. Variable prog : RTL.program. Variable tprog : HTL.program. + Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. + Hypothesis TRANSL : match_prog prog tprog. - Lemma TRANSL' : - Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. - Proof. intros; apply match_prog_matches; assumption. Qed. + Axiom no_pointer_return : forall (rs : RTL.regset) r s (f : RTL.function) sp pc rs mem f S, + (RTL.fn_code f) ! pc = Some (RTL.Ireturn (Some r)) -> + match_states ge (RTL.State s f sp pc rs mem) S -> + (not_pointer rs !! r). - Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. - Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. + (** The following are assumed to be guaranteed by an inlining pass previous to + this translation. [ only_main_stores ] should be a direct result of that + inlining. + + [ no_stack_functions ] and [ no_stack_calls ] might be provable as + corollaries of [ only_main_stores ] + *) + Axiom only_main_stores : forall rtl_stk f sp pc pc' rs mem htl_stk mid m asr asa a b c d, + match_states ge (RTL.State rtl_stk f sp pc rs mem) (HTL.State htl_stk mid m pc asr asa) -> + (RTL.fn_code f) ! pc = Some (RTL.Istore a b c d pc') -> + (rtl_stk = nil /\ htl_stk = nil). + + Axiom no_stack_functions : forall f sp rs mem st rtl_stk S, + match_states ge (RTL.State rtl_stk f sp st rs mem) S -> + (RTL.fn_stacksize f) = 0 \/ rtl_stk = nil. + + Axiom no_stack_calls : forall f mem args rtl_stk S, + match_states ge (RTL.Callstate rtl_stk (AST.Internal f) args mem) S -> + (RTL.fn_stacksize f) = 0 \/ rtl_stk = nil. + + (** The following admitted lemmas should be provable *) + Lemma mem_free_zero : forall mem blk, Mem.free mem blk 0 0 = Some mem. + Admitted. + + Lemma mem_alloc_zero : forall mem, exists blk, Mem.alloc mem 0 0 = (mem, blk). + Admitted. + + Lemma match_arrs_empty : forall m f sp mem asa, + match_arrs m f sp mem asa -> + match_arrs m f sp mem (Verilog.merge_arrs (HTL.empty_stack m) asa). + Admitted. + + Lemma TRANSL' : + Linking.match_program (fun cu f tf => transl_fundef prog f = Errors.OK tf) eq prog tprog. + Proof. pose proof match_prog_matches as H. unfold match_prog' in H. auto. Qed. Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -372,7 +478,7 @@ Section CORRECTNESS. forall (b: Values.block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef prog f = Errors.OK tf. Proof. intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -382,7 +488,7 @@ Section CORRECTNESS. forall (v: Values.val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. + Genv.find_funct tge v = Some tf /\ transl_fundef prog f = Errors.OK tf. Proof. intros. exploit (Genv.find_funct_match TRANSL'); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -592,14 +698,14 @@ Section CORRECTNESS. end. 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 ge (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 -> Verilog.expr_runp f' asr asa e (boolToValue b). Proof. - intros stk f sp pc rs m res ml st asr asa e b f' s s' args i cond MSTATE MAX_FUN EVAL TR_INSTR. + intros * MSTATE MAX_FUN EVAL TR_INSTR. pose proof MSTATE as MSTATE_2. inv MSTATE. inv MASSOC. unfold translate_condition, translate_comparison, translate_comparisonu, translate_comparison_imm, @@ -723,21 +829,21 @@ 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 ge (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 -> exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. - intros e stk f sp pc rs m res ml st asr asa v f' s s' args i cond MSTATE MAX_FUN EVAL TR_INSTR. + intros * MSTATE MAX_FUN EVAL TR_INSTR. unfold translate_condition, translate_comparison, translate_comparisonu, translate_comparison_imm, translate_comparison_immu, bop, boplit in *. repeat unfold_match TR_INSTR; inv TR_INSTR; repeat econstructor. 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 ge (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 => @@ -745,13 +851,10 @@ Section CORRECTNESS. translate_instr (Op.Oshrximm n) args s = OK e s' i -> exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. Proof. - intros s sp rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st n MSTATE INSTR EVAL TR_INSTR. + intros * MSTATE INSTR EVAL TR_INSTR. pose proof MSTATE as MSTATE_2. inv MSTATE. inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR; unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL. - (*repeat (simplify; eval_correct_tac; unfold valueToInt in * ). - destruct (Z_lt_ge_dec (Int.signed i0) 0). - econstructor.*) unfold Values.Val.shrx in *. destruct v0; try discriminate. destruct (Int.ltu n (Int.repr 31)) eqn:?; try discriminate. @@ -801,15 +904,15 @@ 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 ge (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 -> translate_instr op args s = OK e s' i -> exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. Proof. - intros s sp op rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st MSTATE INSTR EVAL TR_INSTR. + intros * MSTATE INSTR EVAL TR_INSTR. pose proof MSTATE as MSTATE_2. inv MSTATE. inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR; unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL; @@ -836,8 +939,6 @@ Section CORRECTNESS. - rewrite Heqb in Heqb0. discriminate. - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. - rewrite Heqb in Heqb0. discriminate. - (*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu, - repeat (rewrite Int.unsigned_repr). auto.*) - assert (Int.unsigned n <= 30). { unfold Int.ltu in *. destruct (zlt (Int.unsigned n) (Int.unsigned (Int.repr 31))); try discriminate. rewrite Int.unsigned_repr in l by (simplify; lia). @@ -1021,10 +1122,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. @@ -1077,31 +1178,25 @@ Section CORRECTNESS. (rs : RTL.regset) (m : mem) (pc' : RTL.node), (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states ge (RTL.State s f sp pc' rs m) R2. Proof. - intros s f sp pc rs m pc' H R1 MSTATE. + intros * H R1 MSTATE. inv_state. unfold match_prog in TRANSL. - econstructor. + eexists. split. - apply Smallstep.plus_one. - eapply HTL.step_module; eauto. - inv CONST; assumption. - inv CONST; assumption. - (* processing of state *) - econstructor. - crush. - econstructor. - econstructor. - econstructor. - - all: invert MARR; big_tac. - - inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. - + - apply Smallstep.plus_one. + eapply HTL.step_module; eauto. + + inv CONST; assumption. + + inv CONST; assumption. + + repeat constructor. + + repeat constructor. + + big_tac. + - inv CONST. inv MARR. simplify. big_tac. + constructor; rewrite AssocMap.gso; crush. Unshelve. exact tt. Qed. Hint Resolve transl_inop_correct : htlproof. @@ -1113,50 +1208,486 @@ Section CORRECTNESS. (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. + match_states ge (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. Proof. - intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE. + intros * H H0 R1 MSTATE. inv_state. inv MARR. exploit eval_correct; eauto. intros. inversion H1. inversion H2. - econstructor. split. + eexists. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. - inv CONST. assumption. - inv CONST. assumption. - econstructor; simpl; trivial. - constructor; trivial. - econstructor; simpl; eauto. - simpl. econstructor. econstructor. - apply H5. simplify. + - inv CONST. assumption. + - inv CONST. assumption. + - repeat econstructor. + - repeat econstructor. intuition eauto. + - big_tac. + assert (Ple res0 (RTL.max_reg_function f)) + by eauto using RTL.max_reg_function_def. + xomega. + - big_tac. + + apply regs_lessdef_add_match. assumption. + apply regs_lessdef_add_greater. unfold Plt; lia. assumption. + + assert (HPle: Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + unfold Ple in HPle; lia. + + eapply op_stack_based; eauto. + + inv CONST. constructor; simplify. + * rewrite AssocMap.gso. rewrite AssocMap.gso. + assumption. lia. + assert (HPle: Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + unfold Ple in HPle. lia. + * rewrite AssocMap.gso. rewrite AssocMap.gso. + assumption. lia. + assert (HPle: Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + unfold Ple in HPle. lia. + Unshelve. exact tt. + Qed. + Hint Resolve transl_iop_correct : htlproof. - all: big_tac. + Lemma match_args : forall rtl_args htl_args params f, + list_forall2 val_value_lessdef rtl_args htl_args -> + match_assocmaps f (RTL.init_regs rtl_args params) (HTL.init_regs htl_args params). + Proof. + induction rtl_args; intros * H; inv H. + - destruct params; eauto with htlproof. + - destruct params; eauto using regs_lessdef_add_match with htlproof. + Qed. - assert (HPle: Ple res0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + Lemma stack_based_set : forall sp r v rs, + stack_based v sp -> + reg_stack_based_pointers sp rs -> + reg_stack_based_pointers sp (Registers.Regmap.set r v rs). + Proof. + unfold reg_stack_based_pointers, Registers.Regmap.set, "_ !! _". + intros * ? ? r0. + simpl. + destruct (peq r r0); subst. + - rewrite AssocMap.gss; auto. + - rewrite AssocMap.gso; auto. + Qed. - unfold Ple in HPle. lia. - apply regs_lessdef_add_match. assumption. - apply regs_lessdef_add_greater. unfold Plt; lia. assumption. - assert (HPle: Ple res0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle; lia. - eapply op_stack_based; eauto. - inv CONST. constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. - assumption. lia. - assert (HPle: Ple res0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. - rewrite AssocMap.gso. rewrite AssocMap.gso. - assumption. lia. - assert (HPle: Ple res0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. - Unshelve. exact tt. + Lemma stack_based_non_pointers : forall args params stk, + Forall not_pointer args -> + reg_stack_based_pointers stk (RTL.init_regs args params). + Proof. + unfold reg_stack_based_pointers. + induction args; intros * NP *. + + destruct params; + simpl; + unfold "_ !! _"; + rewrite PTree.gempty; + crush. + + destruct params; simpl. + * unfold "_ !! _". rewrite PTree.gempty. crush. + * inv NP. + apply stack_based_set; + [ destruct a; crush + | unfold reg_stack_based_pointers; auto + ]. Qed. - Hint Resolve transl_iop_correct : htlproof. + + Lemma transl_callstate_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) + (m : mem) (m' : Mem.mem') (stk : Values.block), + Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> + forall R1 : HTL.state, + match_states ge (RTL.Callstate s (AST.Internal f) args m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states ge + (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) + (RTL.init_regs args (RTL.fn_params f)) m') R2. + Proof. + intros * ? * MSTATE. + inversion MSTATE. + inversion TF. + simplify. + eexists. split. + apply Smallstep.plus_one. + solve [constructor]. + + simplify. + econstructor; try solve [big_tac]. + - repeat apply regs_lessdef_add_greater; try not_control_reg. + eauto using match_args. + - edestruct no_stack_calls; eauto. + + replace (RTL.fn_stacksize f) with 0 in * + by assumption. + replace m' with m + by (destruct (mem_alloc_zero m); crush). + assumption. + + subst. inv MF. constructor. + - big_tac. + admit. + - eauto using stack_based_non_pointers. + - (* Stack based stack pointer *) + unfold arr_stack_based_pointers; intros. + admit. + - (* Stack bounds *) + admit. + - constructor; simplify. + + rewrite AssocMap.gss; crush. + + rewrite AssocMap.gso by not_control_reg. + rewrite AssocMap.gss. crush. + Admitted. + Hint Resolve transl_callstate_correct : htlproof. + + Lemma only_internal_calls : forall fd fn rs, + RTL.find_function ge (inr fn) rs = Some fd -> + (exists f : RTL.function, HTL.find_func ge fn = Some (AST.Internal f)) -> + (exists f, fd = AST.Internal f). + Proof. + intros * ? [? ?]. + unfold HTL.find_func in *. + unfold RTL.find_function in *. + destruct (Genv.find_symbol ge fn); try discriminate. + exists x. crush. + Qed. + + Fixpoint assign_all acc (rs : list reg) (vals : list value) := + match rs, vals with + | r::rs', val::vals' => assign_all (acc # r <- val) rs' vals' + | _, _ => acc + end. + + Notation "a ## b '<-' c" := (assign_all a b c) (at level 1, b at next level) : assocmap. + + Lemma assign_all_nil : forall a rs, a ## rs <- nil = a. + Proof. destruct rs; crush. Qed. + + Lemma assign_all_out : forall rs vs a r, (forall v, ~ In (r, v) (List.combine rs vs)) -> (a ## rs <- vs) ! r = a ! r. + Proof. + induction rs; intros * H. + - trivial. + - destruct vs. + + rewrite assign_all_nil. + trivial. + + simpl. + rewrite IHrs. + rewrite AssocMap.gso. + crush. + * simpl (List.combine _ _) in *. + specialize (H v). + rewrite not_in_cons in H. + inv H. + crush. + * intros v0. + specialize (H v0). + simpl (List.combine _ _) in *. + rewrite not_in_cons in H. + crush. + Qed. + + Lemma nonblock_all_exec : forall from_regs to_regs f basr nasr basa nasa, + Verilog.stmnt_runp + f + {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := nasr |} + {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |} + (nonblock_all (List.combine to_regs from_regs)) + {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := nasr ## to_regs <- (basr##from_regs) |} + {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |}. + Proof. + induction from_regs; intros. + - rewrite combine_nil, assign_all_nil. + constructor. + - destruct to_regs; try solve [ constructor ]. + simpl. + econstructor. + + repeat econstructor. + + eapply IHfrom_regs. + Qed. + + Lemma fork_exec : forall f basr nasr basa nasa rst to_regs from_regs, + Verilog.stmnt_runp + f + {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := nasr |} + {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |} + (fork rst (List.combine to_regs from_regs)) + {| Verilog.assoc_blocking := basr; Verilog.assoc_nonblocking := (nasr # rst <- (ZToValue 1)) ## to_regs <- (basr##from_regs) |} + {| Verilog.assoc_blocking := basa; Verilog.assoc_nonblocking := nasa |}. + Proof. + intros. + unfold fork. + econstructor. + - repeat econstructor. + - unfold Verilog.nonblock_reg; simpl. + eapply nonblock_all_exec. + Qed. + + Lemma transl_find : forall fn f, + HTL.find_func ge fn = Some (AST.Internal f) -> + match_prog prog tprog -> + (exists f', HTL.find_func tge fn = Some (AST.Internal f')). + Proof. + intros. + unfold HTL.find_func in *. + rewrite symbols_preserved. + destruct (Genv.find_symbol ge fn); try discriminate. + destruct (function_ptr_translated _ _ H) as [? [? ?]]. + replace (Genv.find_funct_ptr tge b). + inversion H2. + destruct (transl_module prog f); try discriminate. + inversion H4. + exists m. crush. + Qed. + + Lemma param_mapping_correct : + forall fn (args : list reg) fn_params (externctrl : AssocMap.t (HTL.ident * HTL.controlsignal)), + length args = length fn_params -> + (forall n arg, nth_error args n = Some arg -> + exists r, List.nth_error fn_params n = Some r /\ + externctrl ! r = Some (fn, HTL.ctrl_param n)) -> + (forall n param, nth_error fn_params n = Some param -> + externctrl!param = Some (fn, HTL.ctrl_param n)). + Proof. + intros * Hlen Htr * Hfn_params. + + assert (H : exists arg, nth_error args n = Some arg). { + apply length_nth_error. + apply nth_error_length in Hfn_params. + lia. + } + destruct H as [ arg H ]. + edestruct (Htr _ _ H) as [? [? ?]]. + + enough (Some x = Some param) by crush. + congruence. + Qed. + + Lemma transl_icall_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) + (pc : positive) (rs : RTL.regset) (m : mem) sig fn fd args dst pc', + (RTL.fn_code f) ! pc = Some (RTL.Icall sig fn args dst pc') -> + RTL.find_function ge fn rs = Some fd -> + forall R1 : HTL.state, + match_states ge (RTL.State s f sp pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states ge (RTL.Callstate (RTL.Stackframe dst f sp pc' rs :: s) fd + (List.map (fun r => Registers.Regmap.get r rs) args) m) + R2. + Proof. + intros * H Hfunc * MSTATE. + inv_state. + edestruct (only_internal_calls fd); eauto; subst fd. + inv CONST. + simplify. + destruct (transl_find _ _ ltac:(eauto) TRANSL). + eexists. split. + - eapply Smallstep.plus_three; simpl in *. + + eapply HTL.step_module; simpl. + * auto. + * auto. + * eauto. + * eauto. + * eauto. + * repeat econstructor; eauto. + * repeat econstructor; eauto. + * eapply fork_exec. + * trivial. + * trivial. + * eapply AssocMapExt.merge_correct_1. + rewrite assign_all_out. + -- big_tac. + not_control_reg. + -- intros ? Hneg. + apply List.in_combine_l in Hneg. + insterU H6. + insterU H19. + (* All of x4 are in externctrl (by H6), but st1 is not because it is a control register *) + admit. + * eauto. + + eapply HTL.step_module; trivial. + * simpl. + apply AssocMapExt.merge_correct_2; auto. + rewrite assign_all_out by admit. + rewrite AssocMap.gso by not_control_reg. + rewrite AssocMap.gso by lia. + apply AssocMap.gempty. + * simpl. + apply AssocMapExt.merge_correct_2; auto. + rewrite assign_all_out by admit. + rewrite AssocMap.gso by not_control_reg. + rewrite AssocMap.gso by lia. + apply AssocMap.gempty. + * simpl. + apply AssocMapExt.merge_correct_1; auto. + rewrite assign_all_out by admit. + rewrite AssocMap.gso by not_control_reg. + apply AssocMap.gss. + * eauto. + * eauto. + * unfold state_wait. + eapply Verilog.stmnt_runp_Vcond_false. + -- simpl. econstructor; econstructor; simpl. + replace (Verilog.merge_regs ((empty_assocmap # st1 <- (posToValue x0)) # x1 <- (ZToValue 1)) ## x4 <- (asr ## args) asr) # x3 + with (ZToValue 0) by admit. + trivial. + -- auto. + -- econstructor. + * simpl. + apply AssocMapExt.merge_correct_1; auto. + rewrite assign_all_out by admit. + rewrite AssocMap.gso by not_control_reg. + apply AssocMap.gss. + * repeat econstructor. + * simpl. + apply AssocMapExt.merge_correct_2. + big_tac. + apply AssocMap.gempty. + not_control_reg. + assert (Ple dst (RTL.max_reg_function f)) + by eauto using RTL.max_reg_function_def. + xomega. + apply AssocMapExt.merge_correct_1. + rewrite assign_all_out by admit. + rewrite AssocMap.gso by not_control_reg. + apply AssocMap.gss. + * admit. + + eapply HTL.step_initcall. + * eassumption. + * eassumption. + * eauto using param_mapping_correct. + * big_tac. + assert (dst <= (RTL.max_reg_function f))%positive + by (eapply RTL.max_reg_function_def; eauto). + not_control_reg. + * simpl; trivial. + + eauto with htlproof. + - econstructor; try solve [repeat econstructor; eauto with htlproof ]. + + admit. + + (* Match stackframes *) admit. + + (* Argument values match *) admit. + Admitted. + Hint Resolve transl_icall_correct : htlproof. + Close Scope rtl. + + Lemma return_val_exec_spec : forall f or asr asa, + Verilog.expr_runp f asr asa (return_val or) + (match or with + | Some r => asr#r + | None => ZToValue 0 + end). + Proof. destruct or; repeat econstructor. Qed. + + Lemma transl_ireturn_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) + (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) + (m' : mem), + (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> + Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> + forall R1 : HTL.state, + match_states ge (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states ge (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. + Proof. + intros * H H0 * MSTATE. + inv_state. + inv CONST. simplify. + eexists. split. + - eapply Smallstep.plus_two. + + eapply HTL.step_module; try solve [ repeat econstructor; eauto ]. + * repeat econstructor. apply return_val_exec_spec. + * big_tac. + * inversion wf. + eapply H10. + eapply AssocMapExt.elements_iff. + eauto. + + eapply HTL.step_finish; big_tac. + + eauto with htlproof. + - constructor; eauto with htlproof. + + edestruct no_stack_functions; eauto. + * replace (RTL.fn_stacksize f) in *. + replace m' with m by + (pose proof (mem_free_zero m ltac:(auto)); crush). + assumption. + * subst. inv MF. constructor. + + destruct or. + * rewrite fso. (* Return value is not fin *) + { + big_tac. + inv MASSOC. + apply H10. + eapply RTL.max_reg_function_use. + simpl; eauto. + simpl; eauto. + } + assert (Ple r (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; crush). + xomega. + * simpl. eauto with htlproof. + + destruct or; simpl; eauto using no_pointer_return. + Unshelve. try exact tt; eauto. + Qed. + Hint Resolve transl_ireturn_correct : htlproof. + + Lemma transl_returnstate_correct: + forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) + (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) + (R1 : HTL.state), + match_states ge (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states ge (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. + Proof. + intros * MSTATE. + inv MSTATE. + inversion MF. + inversion EXTERN_CALLER. + simplify. + eexists; split. + - eapply Smallstep.plus_two. + + (* Return to caller *) + repeat econstructor; eauto. + + (* Join *) + inv CONST. + econstructor; eauto. + * big_tac; inv TF; simplify; not_control_reg. + * big_tac; inv TF; simplify; not_control_reg. + * big_tac; inv TF; simplify; not_control_reg. + * (* control logic *) + repeat econstructor. big_tac. simpl. + rewrite fso by crush. + rewrite fss. crush. + * big_tac; inv TF; simplify; not_control_reg. + * repeat econstructor. + * big_tac; inv TF; simplify; not_control_reg. + + trivial. + - simpl. + eapply match_state; simpl; eauto. + + big_tac. + inv TF. simplify. + eapply regs_lessdef_add_match. rewrite fss; eauto. + repeat eapply regs_lessdef_add_greater; eauto; not_control_reg. + + unfold state_st_wf. + intros * Hwf. + inv Hwf. + inv TF. + big_tac. + not_control_reg. + + auto using match_arrs_empty. + + eapply stack_based_set; eauto. + unfold not_pointer in *. + destruct vres; crush. + + (* match_constants *) + inv CONST. + inv TF. + big_tac. + constructor. + * simplify. + rewrite AssocMap.fss. + repeat rewrite AssocMap.gso; auto; not_control_reg. + * simplify. + repeat rewrite AssocMap.gso; auto; not_control_reg. + Unshelve. all: try exact tt; eauto. + Qed. + Hint Resolve transl_returnstate_correct : htlproof. Ltac tac := repeat match goal with @@ -1239,7 +1770,6 @@ Section CORRECTNESS. } rewrite <- H. auto. - Qed. Lemma offset_expr_ok_3 : @@ -1257,13 +1787,15 @@ Section CORRECTNESS. Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> Mem.loadv chunk m a = Some v -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. + match_states ge (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. Proof. intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. - inv_state. inv_arr_access. + inv_state. + + inv_arr_access. + (** Preamble *) invert MARR. inv CONST. crush. @@ -1336,28 +1868,29 @@ Section CORRECTNESS. inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; clear NORMALISE_BOUND. + (** Start of proof proper *) eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. crush. + econstructor. econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - econstructor. econstructor. + econstructor. all: big_tac. 1: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. + assert (HPle : (dst <= (RTL.max_reg_function f))%positive) + by (eapply RTL.max_reg_function_def; eauto). + lia. } 2: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. + assert (HPle : (dst <= (RTL.max_reg_function f))%positive) + by (eapply RTL.max_reg_function_def; eauto). + lia. } (** Match assocmaps *) @@ -1377,7 +1910,10 @@ Section CORRECTNESS. specialize (ASBP (Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). exploit ASBP; big_tac. - rewrite NORMALISE in H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption. + match goal with + | [ H: context[stack_based] |- _ ] => rewrite NORMALISE in H; rewrite HeqOFFSET in H; rewrite H1 in H + end. + assumption. constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. assumption. lia. assert (HPle: Ple dst (RTL.max_reg_function f)) @@ -1417,7 +1953,7 @@ Section CORRECTNESS. apply H11 in HPler1. invert HPler0; invert HPler1; try congruence. rewrite EQr0 in H13. - rewrite EQr1 in H14. + rewrite EQr1 in H22. invert H13. invert H14. clear H0. clear H8. clear H11. @@ -1432,7 +1968,8 @@ Section CORRECTNESS. (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. - apply Zdivide_mod. assumption. } + apply Zdivide_mod. unfold valueToPtr in *. unfold uvalueToZ in *. unfold Ptrofs.of_int in *. unfold valueToInt in *. + inversion H22. subst. assumption. } (** Read bounds proof *) assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. @@ -1474,21 +2011,27 @@ Section CORRECTNESS. eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. crush. + econstructor. econstructor. econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. auto. econstructor. - econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. all: big_tac. - 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } + 1: { + assert (HPle : Ple dst (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto). + rewrite Pcompare_eq_Gt in *. + xomega. + } - 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } + 2: { + assert (HPle : Ple dst (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto). + rewrite Pcompare_eq_Gt in *. + xomega. + } (** Match assocmaps *) apply regs_lessdef_add_match; big_tac. @@ -1502,23 +2045,30 @@ Section CORRECTNESS. (Integers.Ptrofs.repr 4)))). exploit H9; big_tac. + (* This should have been solved somewhere above here *) + match goal with + | [ |- match_assocmaps _ _ _ ] => admit + end. + (** RSBP preservation *) unfold arr_stack_based_pointers in ASBP. specialize (ASBP (Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). exploit ASBP; big_tac. - rewrite NORMALISE in H14. rewrite HeqOFFSET in H14. rewrite H1 in H14. assumption. + rewrite NORMALISE in H14. rewrite HeqOFFSET in H14. + inversion H22. replace (asr # r1) in *. rewrite H1 in *. assumption. + rewrite Pcompare_eq_Gt in *. constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. assumption. lia. assert (HPle: Ple dst (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. + by (eapply RTL.max_reg_function_def; eauto). + xomega. rewrite AssocMap.gso. rewrite AssocMap.gso. assumption. lia. assert (HPle: Ple dst (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - unfold Ple in HPle. lia. + xomega. + invert MARR. inv CONST. crush. @@ -1533,7 +2083,7 @@ Section CORRECTNESS. rewrite ZERO in H1. clear ZERO. rewrite Integers.Ptrofs.add_zero_l in H1. - remember i0 as OFFSET. + remember i as OFFSET. (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. @@ -1578,18 +2128,20 @@ Section CORRECTNESS. eexists. split. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. - econstructor. econstructor. econstructor. crush. - econstructor. econstructor. econstructor. econstructor. crush. + repeat econstructor. crush. + repeat econstructor. crush. all: big_tac. - 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } + 1: { + assert (HPle : Ple dst (RTL.max_reg_function f)) by (eauto using RTL.max_reg_function_def). + xomega. + } - 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } + 2: { + assert (HPle : Ple dst (RTL.max_reg_function f)) by (eauto using RTL.max_reg_function_def). + xomega. + } (** Match assocmaps *) apply regs_lessdef_add_match; big_tac. @@ -1622,13 +2174,8 @@ Section CORRECTNESS. unfold Ple in HPle. lia. Unshelve. - exact (Values.Vint (Int.repr 0)). - exact tt. - exact (Values.Vint (Int.repr 0)). - exact tt. - exact (Values.Vint (Int.repr 0)). - exact tt. - Qed. + all: try (exact tt); auto. + Admitted. Hint Resolve transl_iload_correct : htlproof. Lemma transl_istore_correct: @@ -1640,9 +2187,9 @@ Section CORRECTNESS. Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states ge (RTL.State s f sp pc' rs m') R2. Proof. intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. inv_state. inv_arr_access. @@ -1725,6 +2272,8 @@ Section CORRECTNESS. unfold_merge. apply AssocMap.gss. + edestruct only_main_stores; eauto. subst; constructor. + (** Equality proof *) assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. @@ -1828,9 +2377,9 @@ Section CORRECTNESS. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. - rewrite Z2Nat.id in H15; try lia. - apply Zmult_lt_compat_r with (p := 4) in H15; try lia. - rewrite ZLib.div_mul_undo in H15; try lia. + rewrite Z2Nat.id in *; try lia. + apply Zmult_lt_compat_r with (p := 4) in H27; try lia. + rewrite ZLib.div_mul_undo in *; try lia. split; try lia. apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } @@ -1894,8 +2443,8 @@ Section CORRECTNESS. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. invert H11. - apply Zmult_lt_compat_r with (p := 4) in H14; try lia. - rewrite ZLib.div_mul_undo in H14; try lia. + apply Zmult_lt_compat_r with (p := 4) in H22; try lia. + rewrite ZLib.div_mul_undo in *; try lia. split; try lia. apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } @@ -1965,8 +2514,8 @@ Section CORRECTNESS. apply H11 in HPler1. invert HPler0; invert HPler1; try congruence. rewrite EQr0 in H13. - rewrite EQr1 in H14. - invert H13. invert H14. + rewrite EQr1 in H22. + invert H13. invert H22. clear H0. clear H8. clear H11. unfold check_address_parameter_signed in *; @@ -2026,6 +2575,8 @@ Section CORRECTNESS. unfold_merge. apply AssocMap.gss. + edestruct only_main_stores; eauto; subst; constructor. + (** Equality proof *) assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. @@ -2094,20 +2645,20 @@ Section CORRECTNESS. erewrite combine_lookup_second. simpl. assert (Ple src (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simpl; auto); - apply H14 in H15. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H15; eauto. + by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H22 in H27. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H27; eauto. rewrite <- array_set_len. unfold arr_repeat. crush. rewrite list_repeat_len. auto. assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H15. - rewrite Z_div_mult in H15; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H15 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H15; unfold_constants; try lia. - rewrite H15. rewrite <- offset_expr_ok_2. + rewrite Z.mul_comm in H27. + rewrite Z_div_mult in H27; try lia. + replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H27 by reflexivity. + rewrite <- PtrofsExtra.divu_unsigned in H27; unfold_constants; try lia. + rewrite H27. rewrite <- offset_expr_ok_2. rewrite HeqOFFSET in *. rewrite array_get_error_set_bound. reflexivity. @@ -2128,9 +2679,9 @@ Section CORRECTNESS. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. - rewrite Z2Nat.id in H17; try lia. - apply Zmult_lt_compat_r with (p := 4) in H17; try lia. - rewrite ZLib.div_mul_undo in H17; try lia. + rewrite Z2Nat.id in *; try lia. + apply Zmult_lt_compat_r with (p := 4) in H29; try lia. + rewrite ZLib.div_mul_undo in H29; try lia. split; try lia. apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } @@ -2155,7 +2706,7 @@ Section CORRECTNESS. unfold_constants. intro. rewrite HeqOFFSET in *. - apply Z2Nat.inj_iff in H15; try lia. + apply Z2Nat.inj_iff in H27; try lia. apply Z.div_pos; try lia. apply Integers.Ptrofs.unsigned_range. apply Integers.Ptrofs.unsigned_range_2. @@ -2176,7 +2727,7 @@ Section CORRECTNESS. crush. destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. destruct (Archi.ptr64); try discriminate. - pose proof (RSBP src). rewrite EQ_SRC in H14. + pose proof (RSBP src). rewrite EQ_SRC in H22. assumption. simpl. @@ -2194,9 +2745,9 @@ Section CORRECTNESS. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. - invert H14. - apply Zmult_lt_compat_r with (p := 4) in H16; try lia. - rewrite ZLib.div_mul_undo in H16; try lia. + invert H22. + apply Zmult_lt_compat_r with (p := 4) in H28; try lia. + rewrite ZLib.div_mul_undo in H28; try lia. split; try lia. apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } @@ -2222,13 +2773,13 @@ Section CORRECTNESS. (Integers.Ptrofs.unsigned (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) (Integers.Ptrofs.repr ptr))) Writable). - { pose proof H1. eapply Mem.store_valid_access_2 in H14. - exact H14. eapply Mem.store_valid_access_3. eassumption. } + { pose proof H1. eapply Mem.store_valid_access_2 in H22. + exact H22. eapply Mem.store_valid_access_3. eassumption. } pose proof (Mem.valid_access_store m AST.Mint32 sp' (Integers.Ptrofs.unsigned (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) (Integers.Ptrofs.repr ptr))) v). - apply X in H14. invert H14. congruence. + apply X in H22. invert H22. congruence. constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. assumption. lia. @@ -2248,7 +2799,7 @@ Section CORRECTNESS. rewrite ZERO in H1. clear ZERO. rewrite Integers.Ptrofs.add_zero_l in H1. - remember i0 as OFFSET. + remember i as OFFSET. (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. @@ -2295,6 +2846,9 @@ Section CORRECTNESS. unfold_merge. apply AssocMap.gss. + (** Match frames *) + edestruct only_main_stores; eauto; subst; constructor. + (** Equality proof *) assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. @@ -2346,7 +2900,7 @@ Section CORRECTNESS. rewrite H4. apply list_repeat_len. - remember i0 as OFFSET. + remember i as OFFSET. destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). erewrite Mem.load_store_same. @@ -2492,12 +3046,7 @@ Section CORRECTNESS. assumption. lia. Unshelve. - exact tt. - exact (Values.Vint (Int.repr 0)). - exact tt. - exact (Values.Vint (Int.repr 0)). - exact tt. - exact (Values.Vint (Int.repr 0)). + all: try (exact tt); auto. Qed. Hint Resolve transl_istore_correct : htlproof. @@ -2509,15 +3058,17 @@ Section CORRECTNESS. Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> pc' = (if b then ifso else ifnot) -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states ge (RTL.State s f sp pc' rs m) R2. Proof. intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE. inv_state. destruct b. - eexists. split. apply Smallstep.plus_one. - clear H33. + match goal with + | [H : Z.pos ifnot <= Int.max_unsigned |- _] => clear H + end. eapply HTL.step_module; eauto. inv CONST; assumption. inv CONST; assumption. @@ -2525,7 +3076,7 @@ Section CORRECTNESS. constructor; trivial. eapply Verilog.erun_Vternary_true; simpl; eauto. eapply eval_cond_correct; eauto. intros. - intros. eapply RTL.max_reg_function_use. apply H22. auto. + intros. eapply RTL.max_reg_function_use. eauto. auto. econstructor. auto. simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. @@ -2533,8 +3084,11 @@ Section CORRECTNESS. inv MARR. inv CONST. big_tac. constructor; rewrite AssocMap.gso; simplify; try assumption; lia. + - eexists. split. apply Smallstep.plus_one. - clear H32. + match goal with + | [H : Z.pos ifso <= Int.max_unsigned |- _] => clear H + end. eapply HTL.step_module; eauto. inv CONST; assumption. inv CONST; assumption. @@ -2542,7 +3096,7 @@ Section CORRECTNESS. constructor; trivial. eapply Verilog.erun_Vternary_false; simpl; eauto. eapply eval_cond_correct; eauto. intros. - intros. eapply RTL.max_reg_function_use. apply H22. auto. + intros. eapply RTL.max_reg_function_use. eauto. auto. econstructor. auto. simpl. econstructor. constructor. unfold Verilog.merge_regs. unfold_merge. simpl. apply AssocMap.gss. @@ -2563,229 +3117,14 @@ Section CORRECTNESS. Registers.Regmap.get arg rs = Values.Vint n -> list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states ge (RTL.State s f sp pc' rs m) R2. Proof. intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. Hint Resolve transl_ijumptable_correct : htlproof.*) - Lemma transl_ireturn_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) - (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) - (m' : mem), - (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> - Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> - forall R1 : HTL.state, - match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. - Proof. - intros s f stk pc rs m or m' H H0 R1 MSTATE. - inv_state. - - - econstructor. split. - eapply Smallstep.plus_two. - - eapply HTL.step_module; eauto. - inv CONST; assumption. - inv CONST; assumption. - constructor. - econstructor; simpl; trivial. - econstructor; simpl; trivial. - constructor. - econstructor; simpl; trivial. - constructor. - - constructor. constructor. constructor. - - unfold state_st_wf in WF; big_tac; eauto. - destruct wf1 as [HCTRL HDATA]. apply HCTRL. - apply AssocMapExt.elements_iff. eexists. - match goal with H: control ! pc = Some _ |- _ => apply H end. - - apply HTL.step_finish. - unfold Verilog.merge_regs. - unfold_merge; simpl. - rewrite AssocMap.gso. - apply AssocMap.gss. lia. - apply AssocMap.gss. - rewrite Events.E0_left. reflexivity. - - constructor; auto. - constructor. - - (* FIXME: Duplication *) - - econstructor. split. - eapply Smallstep.plus_two. - eapply HTL.step_module; eauto. - inv CONST; assumption. - inv CONST; assumption. - constructor. - econstructor; simpl; trivial. - econstructor; simpl; trivial. - constructor. constructor. constructor. - constructor. constructor. constructor. - constructor. - - unfold state_st_wf in WF; big_tac; eauto. - - destruct wf1 as [HCTRL HDATA]. apply HCTRL. - apply AssocMapExt.elements_iff. eexists. - match goal with H: control ! pc = Some _ |- _ => apply H end. - - apply HTL.step_finish. - unfold Verilog.merge_regs. - unfold_merge. - unfold_merge. - rewrite AssocMap.gso. - apply AssocMap.gss. simpl; lia. - apply AssocMap.gss. - rewrite Events.E0_left. trivial. - - constructor; auto. - - simpl. inversion MASSOC. subst. - unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. - apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. - assert (HPle : Ple r (RTL.max_reg_function f)). - eapply RTL.max_reg_function_use. eassumption. simpl; auto. - apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - - Unshelve. - all: constructor. - Qed. - Hint Resolve transl_ireturn_correct : htlproof. - - Lemma transl_callstate_correct: - forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) - (m : mem) (m' : Mem.mem') (stk : Values.block), - Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> - forall R1 : HTL.state, - match_states (RTL.Callstate s (AST.Internal f) args m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states - (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) - (RTL.init_regs args (RTL.fn_params f)) m') R2. - Proof. - intros s f args m m' stk H R1 MSTATE. - - inversion MSTATE; subst. inversion TF; subst. - econstructor. split. apply Smallstep.plus_one. - eapply HTL.step_call. crush. - - apply match_state with (sp' := stk); eauto. - - all: big_tac. - - apply regs_lessdef_add_greater. unfold Plt; lia. - apply regs_lessdef_add_greater. unfold Plt; lia. - apply regs_lessdef_add_greater. unfold Plt; lia. - apply init_reg_assoc_empty. - - constructor. - - destruct (Mem.load AST.Mint32 m' stk - (Integers.Ptrofs.unsigned (Integers.Ptrofs.add - Integers.Ptrofs.zero - (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. - pose proof Mem.load_alloc_same as LOAD_ALLOC. - pose proof H as ALLOC. - eapply LOAD_ALLOC in ALLOC. - 2: { exact LOAD. } - ptrofs. rewrite LOAD. - rewrite ALLOC. - repeat constructor. - - ptrofs. rewrite LOAD. - repeat constructor. - - unfold reg_stack_based_pointers. intros. - unfold RTL.init_regs; crush. - destruct (RTL.fn_params f); - rewrite Registers.Regmap.gi; constructor. - - unfold arr_stack_based_pointers. intros. - crush. - destruct (Mem.load AST.Mint32 m' stk - (Integers.Ptrofs.unsigned (Integers.Ptrofs.add - Integers.Ptrofs.zero - (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. - pose proof Mem.load_alloc_same as LOAD_ALLOC. - pose proof H as ALLOC. - eapply LOAD_ALLOC in ALLOC. - 2: { exact LOAD. } - rewrite ALLOC. - repeat constructor. - constructor. - - Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *) - Transparent Mem.load. - Transparent Mem.store. - unfold stack_bounds. - split. - - unfold Mem.alloc in H. - invert H. - crush. - unfold Mem.load. - intros. - match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H4. - unfold Mem.perm in H4. crush. - unfold Mem.perm_order' in H4. - small_tac. - exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. - rewrite Maps.PMap.gss in H8. - match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. - crush. - apply proj_sumbool_true in H10. lia. - - unfold Mem.alloc in H. - invert H. - crush. - unfold Mem.store. - intros. - match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. - invert v0. unfold Mem.range_perm in H4. - unfold Mem.perm in H4. crush. - unfold Mem.perm_order' in H4. - small_tac. - exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. - rewrite Maps.PMap.gss in H8. - match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. - crush. - apply proj_sumbool_true in H10. lia. - constructor. simplify. rewrite AssocMap.gss. - simplify. rewrite AssocMap.gso. apply AssocMap.gss. simplify. lia. - Opaque Mem.alloc. - Opaque Mem.load. - Opaque Mem.store. - Qed. - Hint Resolve transl_callstate_correct : htlproof. - - Lemma transl_returnstate_correct: - forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) - (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) - (R1 : HTL.state), - match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> - exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. - Proof. - intros res0 f sp pc rs s vres m R1 MSTATE. - inversion MSTATE. inversion MF. - Qed. - Hint Resolve transl_returnstate_correct : htlproof. - - Lemma option_inv : - forall A x y, - @Some A x = Some y -> x = y. - Proof. intros. inversion H. trivial. Qed. - Lemma main_tprog_internal : forall b, Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b -> @@ -2803,19 +3142,26 @@ Section CORRECTNESS. trivial. symmetry; eapply Linking.match_program_main; eauto. Qed. + Hint Constructors list_forall2 : htlproof. + Hint Constructors match_frames : htlproof. + Lemma transl_initial_states : forall s1 : Smallstep.state (RTL.semantics prog), Smallstep.initial_state (RTL.semantics prog) s1 -> exists s2 : Smallstep.state (HTL.semantics tprog), - Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2. + Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states ge s1 s2. Proof. induction 1. - destruct TRANSL. unfold main_is_internal in H4. - repeat (unfold_match H4). - assert (f = AST.Internal f1). apply option_inv. - rewrite <- Heqo0. rewrite <- H1. replace b with b0. - auto. apply option_inv. rewrite <- H0. rewrite <- Heqo. - trivial. + destruct TRANSL. + unfold main_is_internal in H4. repeat (unfold_match H4). + assert (f = AST.Internal f1). + { + apply option_inv. + rewrite <- Heqo0. rewrite <- H1. replace b with b0. + auto. apply option_inv. rewrite <- H0. rewrite <- Heqo. + trivial. + } + exploit function_ptr_translated; eauto. intros [tf [A B]]. unfold transl_fundef, Errors.bind in B. @@ -2826,18 +3172,17 @@ Section CORRECTNESS. apply Heqo. symmetry; eapply Linking.match_program_main; eauto. inversion H5. econstructor; split. econstructor. - apply (Genv.init_mem_transf_partial TRANSL'); eauto. - replace (AST.prog_main tprog) with (AST.prog_main prog). - rewrite symbols_preserved; eauto. - symmetry; eapply Linking.match_program_main; eauto. - apply H6. - - constructor. - apply transl_module_correct. - assert (Some (AST.Internal x) = Some (AST.Internal m)). - replace (AST.fundef HTL.module) with (HTL.fundef). - rewrite <- H6. setoid_rewrite <- A. trivial. - trivial. inv H7. assumption. + - apply (Genv.init_mem_transf_partial TRANSL'); eauto. + - replace (AST.prog_main tprog) with (AST.prog_main prog) + by (symmetry; eapply Linking.match_program_main; eauto). + rewrite symbols_preserved; eauto. + - eauto. + - constructor; auto with htlproof. + apply transl_module_correct. + assert (Some (AST.Internal x) = Some (AST.Internal m)) as Heqm. + { rewrite <- H6. setoid_rewrite <- A. trivial. } + inv Heqm. + assumption. Qed. Hint Resolve transl_initial_states : htlproof. @@ -2845,11 +3190,13 @@ Section CORRECTNESS. forall (s1 : Smallstep.state (RTL.semantics prog)) (s2 : Smallstep.state (HTL.semantics tprog)) (r : Integers.Int.int), - match_states s1 s2 -> + match_states ge s1 s2 -> Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r. Proof. - intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity. + intros. + repeat match goal with [ H : _ |- _ ] => try inv H end. + repeat constructor; auto. Qed. Hint Resolve transl_final_states : htlproof. @@ -2857,11 +3204,12 @@ Section CORRECTNESS. forall (S1 : RTL.state) t S2, RTL.step ge S1 t S2 -> forall (R1 : HTL.state), - match_states S1 R1 -> - exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. + match_states ge S1 R1 -> + exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states ge S2 R2. Proof. - induction 1; eauto with htlproof; (intros; inv_state). + induction 1; eauto with htlproof; try solve [ intros; inv_state ]. Qed. + Hint Resolve transl_step_correct : htlproof. Theorem transf_program_correct: diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 16bdcaf..934f3f4 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -21,19 +21,136 @@ Require Import Coq.micromega.Lia. Require compcert.backend.RTL. Require compcert.common.Errors. +Require compcert.common.Globalenvs. Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require compcert.verilog.Op. Require Import vericert.common.Vericertlib. +Require Import vericert.common.ListExtra. Require Import vericert.hls.Verilog. Require Import vericert.hls.ValueInt. Require Import vericert.hls.HTL. Require Import vericert.hls.HTLgen. Require Import vericert.hls.AssocMap. +From Hammer Require Import Tactics. + +(** * Relational specification of the translation *) + +(** We now define inductive predicates that characterise the fact that the +statemachine that is created by the translation contains the correct +translations for each of the elements *) + +(** [tr_instr] describes the translation of instructions that are directly translated into a single state *) +Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt -> control_stmnt -> Prop := +| tr_instr_Inop : + forall n, + Z.pos n <= Int.max_unsigned -> + tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) +| tr_instr_Iop : + forall n op args dst s s' e i, + Z.pos n <= Int.max_unsigned -> + translate_instr op args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) +| tr_instr_Icond : + forall n1 n2 cond args s s' i c, + Z.pos n1 <= Int.max_unsigned -> + Z.pos n2 <= Int.max_unsigned -> + translate_condition cond args s = OK c s' i -> + tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) +| tr_instr_Iload : + forall mem addr args s s' i c dst n, + Z.pos n <= Int.max_unsigned -> + translate_arr_access mem addr args stk s = OK c s' i -> + tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (Vnonblock (Vvar dst) c) (state_goto st n) +| tr_instr_Istore : + forall mem addr args s s' i c src n, + Z.pos n <= Int.max_unsigned -> + translate_arr_access mem addr args stk s = OK c s' i -> + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) + (state_goto st n). +(*| tr_instr_Ijumptable : + forall cexpr tbl r, + cexpr = tbl_to_case_expr st tbl -> + tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*) +Hint Constructors tr_instr : htlspec. + +Inductive tr_code (ge : RTL.genv) (c : RTL.code) (pc : RTL.node) (stmnts : datapath) (trans : controllogic) + (externctrl : AssocMap.t (ident * controlsignal)) (fin rtrn st stk : reg) : RTL.instruction -> Prop := +| tr_code_single : + forall i s t, + c!pc = Some i -> + stmnts!pc = Some s -> + trans!pc = Some t -> + tr_instr fin rtrn st stk i s t -> + tr_code ge c pc stmnts trans externctrl fin rtrn st stk i +| tr_code_call : + forall sig fn args dst n, + c!pc = Some (RTL.Icall sig (inr fn) args dst n) -> + (exists fd, find_func ge fn = Some (AST.Internal fd)) -> + Z.pos n <= Int.max_unsigned -> + + (exists pc2 fn_rst fn_return fn_finish fn_params, + externctrl ! fn_rst = Some (fn, ctrl_reset) /\ + externctrl ! fn_return = Some (fn, ctrl_return) /\ + externctrl ! fn_finish = Some (fn, ctrl_finish) /\ + length args = length fn_params /\ + (forall n arg, List.nth_error args n = Some arg -> + exists r, List.nth_error fn_params n = Some r /\ + externctrl ! r = Some (fn, ctrl_param n)) /\ + Z.pos pc2 <= Int.max_unsigned /\ + stmnts!pc = Some (fork fn_rst (List.combine fn_params args)) /\ + trans!pc = Some (state_goto st pc2) /\ + stmnts!pc2 = Some (join fn_return fn_rst dst) /\ + trans!pc2 = Some (state_wait st fn_finish n)) -> + + tr_code ge c pc stmnts trans externctrl fin rtrn st stk (RTL.Icall sig (inr fn) args dst n) +| tr_code_return : + forall r, + c!pc = Some (RTL.Ireturn r) -> + + (exists pc2, + stmnts!pc = Some (do_return fin rtrn r) /\ + trans!pc = Some (state_goto st pc2) /\ + stmnts!pc2 = Some (idle fin) /\ + trans!pc2 = Some Vskip) -> + + tr_code ge c pc stmnts trans externctrl fin rtrn st stk (RTL.Ireturn r). +Hint Constructors tr_code : htlspec. + +Inductive tr_module (ge : RTL.genv) (f : RTL.function) : module -> Prop := + tr_module_intro : + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls externctrl wf, + m = (mkmodule f.(RTL.fn_params) + data + control + f.(RTL.fn_entrypoint) + st stk stk_len fin rtrn start rst clk scldecls arrdecls externctrl wf) -> + (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> + tr_code ge f.(RTL.fn_code) pc data control externctrl fin rtrn st stk i) -> + stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> + Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> + (st > (RTL.max_reg_function f))%positive -> + (fin > st)%positive -> + (rtrn > fin)%positive -> + (stk > rtrn)%positive -> + (start > stk)%positive -> + (rst > start)%positive -> + (clk > rst)%positive -> + (forall n, (exists x, externctrl!n = Some x) -> (n > clk)%positive) -> + tr_module ge f m. +Hint Constructors tr_module : htlspec. + Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. Hint Resolve Maps.PTree.elements_correct : htlspec. +Hint Resolve Maps.PTree.gss : htlspec. +Hint Resolve PTree.elements_complete : htlspec. +Hint Resolve -> Z.leb_le : htlspec. + +Hint Unfold block : htlspec. +Hint Unfold nonblock : htlspec. Remark bind_inversion: forall (A B: Type) (f: mon A) (g: A -> mon B) @@ -41,13 +158,7 @@ Remark bind_inversion: bind f g s1 = OK y s3 i -> exists x, exists s2, exists i1, exists i2, f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2. -Proof. - intros until i. unfold bind. destruct (f s1); intros. - discriminate. - exists a; exists s'; exists s. - destruct (g a s'); inv H. - exists s0; auto. -Qed. +Proof. unfold bind. sauto. Qed. Remark bind2_inversion: forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) @@ -55,15 +166,12 @@ Remark bind2_inversion: bind2 f g s1 = OK z s3 i -> exists x, exists y, exists s2, exists i1, exists i2, f s1 = OK (x, y) s2 i1 /\ g x y s2 = OK z s3 i2. -Proof. - unfold bind2; intros. - exploit bind_inversion; eauto. - intros [[x y] [s2 [i1 [i2 [P Q]]]]]. simpl in Q. - exists x; exists y; exists s2; exists i1; exists i2; auto. -Qed. +Proof. sauto using bind_inversion. Qed. Ltac monadInv1 H := match type of H with + | ((match ?x with | _ => _ end) = OK _ _ _) => + destruct x eqn:?; try discriminate; try monadInv1 H | (OK _ _ _ = OK _ _ _) => inversion H; clear H; try subst | (Error _ _ = OK _ _ _) => @@ -98,6 +206,7 @@ Ltac monadInv1 H := Ltac monadInv H := match type of H with | (ret _ _ = OK _ _ _) => monadInv1 H + | (OK _ _ = OK _ _ _) => monadInv1 H | (error _ _ = OK _ _ _) => monadInv1 H | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H @@ -119,538 +228,330 @@ Ltac monadInv H := ((progress simpl in H) || unfold F in H); monadInv1 H end. -(** * Relational specification of the translation *) - -(** We now define inductive predicates that characterise the fact that the -statemachine that is created by the translation contains the correct -translations for each of the elements *) - -Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := -| tr_instr_Inop : - forall n, - Z.pos n <= Int.max_unsigned -> - tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) -| tr_instr_Iop : - forall n op args dst s s' e i, - Z.pos n <= Int.max_unsigned -> - translate_instr op args s = OK e s' i -> - tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) -| tr_instr_Icond : - forall n1 n2 cond args s s' i c, - Z.pos n1 <= Int.max_unsigned -> - Z.pos n2 <= Int.max_unsigned -> - translate_condition cond args s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) -| tr_instr_Ireturn_None : - tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%Z))) - (block rtrn (Vlit (ZToValue 0%Z)))) Vskip -| tr_instr_Ireturn_Some : - forall r, - tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) - (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip -| tr_instr_Iload : - forall mem addr args s s' i c dst n, - Z.pos n <= Int.max_unsigned -> - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) -| tr_instr_Istore : - forall mem addr args s s' i c src n, - Z.pos n <= Int.max_unsigned -> - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) - (state_goto st n). -(*| tr_instr_Ijumptable : - forall cexpr tbl r, - cexpr = tbl_to_case_expr st tbl -> - tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*) -Hint Constructors tr_instr : htlspec. - -Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) - (fin rtrn st stk : reg) : Prop := - tr_code_intro : - forall s t, - c!pc = Some i -> - stmnts!pc = Some s -> - trans!pc = Some t -> - tr_instr fin rtrn st stk i s t -> - tr_code c pc i stmnts trans fin rtrn st stk. -Hint Constructors tr_code : htlspec. - -Inductive tr_module (f : RTL.function) : module -> Prop := - tr_module_intro : - forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf1 wf2 wf3 wf4, - m = (mkmodule f.(RTL.fn_params) - data - control - f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf1 wf2 wf3 wf4) -> - (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> - tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> - stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> - Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> - 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> - st = ((RTL.max_reg_function f) + 1)%positive -> - fin = ((RTL.max_reg_function f) + 2)%positive -> - rtrn = ((RTL.max_reg_function f) + 3)%positive -> - stk = ((RTL.max_reg_function f) + 4)%positive -> - start = ((RTL.max_reg_function f) + 5)%positive -> - rst = ((RTL.max_reg_function f) + 6)%positive -> - clk = ((RTL.max_reg_function f) + 7)%positive -> - tr_module f m. -Hint Constructors tr_module : htlspec. - -Lemma create_reg_datapath_trans : - forall sz s s' x i iop, - create_reg iop sz s = OK x s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_datapath_trans : htlspec. - -Lemma create_reg_controllogic_trans : - forall sz s s' x i iop, - create_reg iop sz s = OK x s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_controllogic_trans : htlspec. - -Lemma declare_reg_datapath_trans : - forall sz s s' x i iop r, - declare_reg iop r sz s = OK x s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_datapath_trans : htlspec. - -Lemma declare_reg_controllogic_trans : - forall sz s s' x i iop r, - declare_reg iop r sz s = OK x s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_controllogic_trans : htlspec. - -Lemma declare_reg_freshreg_trans : - forall sz s s' x i iop r, - declare_reg iop r sz s = OK x s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. inversion 1; auto. Qed. -Hint Resolve declare_reg_freshreg_trans : htlspec. - -Lemma create_arr_datapath_trans : - forall sz ln s s' x i iop, - create_arr iop sz ln s = OK x s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_arr_datapath_trans : htlspec. - -Lemma create_arr_controllogic_trans : - forall sz ln s s' x i iop, - create_arr iop sz ln s = OK x s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_arr_controllogic_trans : htlspec. - -Lemma get_refl_x : - forall s s' x i, - get s = OK x s' i -> - s = x. -Proof. inversion 1. trivial. Qed. -Hint Resolve get_refl_x : htlspec. - -Lemma get_refl_s : - forall s s' x i, - get s = OK x s' i -> - s = s'. -Proof. inversion 1. trivial. Qed. -Hint Resolve get_refl_s : htlspec. - -Ltac inv_incr := - repeat match goal with - | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); eapply create_reg_datapath_trans in H; - eapply create_reg_controllogic_trans in H1 - | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); eapply create_arr_datapath_trans in H; - eapply create_arr_controllogic_trans in H1 - | [ H: get ?s = OK _ _ _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; - subst - | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H - | [ H: st_incr _ _ |- _ ] => destruct st_incr +Ltac rewrite_states := + match goal with + | [ H: ?x ?s = ?x ?s' |- _ ] => + let c1 := fresh "c" in + let c2 := fresh "c" in + learn (?x ?s) as c1; learn (?x ?s') as c2; try subst end. -Lemma collect_controllogic_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_datapath_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_freshreg_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_declare_controllogic_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. - intros. eapply collect_controllogic_trans; try eassumption. - intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. -Qed. - -Lemma collect_declare_datapath_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. - intros. eapply collect_datapath_trans; try eassumption. - intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. -Qed. - -Lemma collect_declare_freshreg_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. eapply collect_freshreg_trans; try eassumption. - inversion 1. auto. -Qed. +Ltac saturate_incr := + repeat match goal with + | [INCR1 : st_prop ?s1 ?s2, INCR2 : st_prop ?s2 ?s3 |- _] => + let INCR3 := fresh "INCR" in + learn (st_trans s1 s2 s3 INCR1 INCR2) + end. -Ltac unfold_match H := - match type of H with - | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate +(** Used to solve goals that follow directly from a single monadic operation *) +Ltac intro_step := + match goal with + | [ H : _ = OK _ _ _ |- _ ] => solve [ monadInv H; simplify; eauto with htlspec ] end. -Lemma translate_eff_addressing_freshreg_trans : - forall op args s r s' i, - translate_eff_addressing op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. - -Lemma translate_comparison_freshreg_trans : - forall op args s r s' i, - translate_comparison op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparison_freshreg_trans : htlspec. +(** Used to transfer a result about one of the maps in the state from one + state to a latter one *) +Ltac trans_step s1 s2 := + saturate_incr; + match goal with + | [ INCR : st_prop s1 s2 |- _ ] => try solve [inversion INCR; crush]; destruct INCR + end; + solve [ + match goal with + | [ MAP_INCR : HTLgen.map_incr ?map _ _ |- (?map _) ! ?idx = _ ] => + destruct MAP_INCR with idx; try crush_trans; crush + end + ]. + +(* FIXME: monad_crush can be slow when there are a lot of intermediate states. *) + +(* Try to prove a goal about a state by first proving it for an earlier state and then transfering it to the final. *) +Ltac monad_crush := + match goal with + | [ finalstate : st, prevstate : st |- _] => + match goal with + | [ |- context f[finalstate]] => + let inter := context f[prevstate] in + try solve [ + match inter with + | context f[finalstate] => + let inter := context f[prevstate] in + solve [assert inter by intro_step; trans_step prevstate finalstate] + end + ]; + solve [assert inter by intro_step; trans_step prevstate finalstate] + end + end. -Lemma translate_comparisonu_freshreg_trans : - forall op args s r s' i, - translate_comparisonu op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparisonu_freshreg_trans : htlspec. +Ltac full_split := repeat match goal with [ |- _ /\ _ ] => split end. -Lemma translate_comparison_imm_freshreg_trans : - forall op args s r s' i n, - translate_comparison_imm op args n s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. +Ltac relevant_monad_inv := + multimatch goal with + | [ EQ : _ ?s = OK ?x _ _ |- context[?x] ] => monadInv EQ + | [ EQ : _ ?s = OK (?x, _) _ _ |- context[?x] ] => monadInv EQ + | [ EQ : _ ?s = OK (_, ?x) _ _ |- context[?x] ] => monadInv EQ + | [ EQ : _ ?s = OK (_, ?x) _ _ |- context[?x] ] => monadInv EQ + end. -Lemma translate_comparison_immu_freshreg_trans : - forall op args s r s' i n, - translate_comparison_immu op args n s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparison_immu_freshreg_trans : htlspec. +Ltac any_monad_inv := + relevant_monad_inv + + multimatch goal with + | [ EQ : _ ?s = OK _ _ _ |- _ ] => monadInv EQ + end. -Lemma translate_condition_freshreg_trans : - forall op args s r s' i, - translate_condition op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. -Qed. -Hint Resolve translate_condition_freshreg_trans : htlspec. +Ltac some_incr := + saturate_incr; + multimatch goal with + | [ INCR : st_prop _ _ |- _ ] => inversion INCR + end. -Lemma translate_instr_freshreg_trans : - forall op args s r s' i, - translate_instr op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). +Lemma helper__map_externctrl_params_args : forall args param_pairs fn s s' k i, + xmap_externctrl_params k fn args s = OK param_pairs s' i -> + snd (List.split param_pairs) = args. Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. - monadInv H1. eauto with htlspec. + induction args. + - sauto. + - intros. monadInv H. sauto. Qed. -Hint Resolve translate_instr_freshreg_trans : htlspec. -Lemma translate_arr_access_freshreg_trans : - forall mem addr args st s r s' i, - translate_arr_access mem addr args st s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. -Qed. -Hint Resolve translate_arr_access_freshreg_trans : htlspec. - -Lemma add_instr_freshreg_trans : - forall n n' st s r s' i, - add_instr n n' st s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_instr_freshreg_trans : htlspec. - -Lemma add_branch_instr_freshreg_trans : - forall n n0 n1 e s r s' i, - add_branch_instr e n n0 n1 s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_branch_instr_freshreg_trans : htlspec. - -Lemma add_node_skip_freshreg_trans : - forall n1 n2 s r s' i, - add_node_skip n1 n2 s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_node_skip_freshreg_trans : htlspec. - -Lemma add_instr_skip_freshreg_trans : - forall n1 n2 s r s' i, - add_instr_skip n1 n2 s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_instr_skip_freshreg_trans : htlspec. - -Lemma transf_instr_freshreg_trans : - forall fin ret st instr s v s' i, - transf_instr fin ret st instr s = OK v s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. destruct instr eqn:?. subst. unfold transf_instr in H. - destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. - - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. - apply declare_reg_freshreg_trans in EQ1. congruence. - - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. - apply declare_reg_freshreg_trans in EQ1. congruence. - - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. - - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. - congruence. - (*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*) -Qed. -Hint Resolve transf_instr_freshreg_trans : htlspec. +Lemma map_externctrl_params_args : forall args param_pairs fn s s' i, + map_externctrl_params fn args s = OK param_pairs s' i -> + snd (List.split param_pairs) = args. +Proof. sauto use: helper__map_externctrl_params_args. Qed. -Lemma collect_trans_instr_freshreg_trans : - forall fin ret st l s s' i, - HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> - s.(st_freshreg) = s'.(st_freshreg). +Lemma helper__map_externctrl_params_spec : forall args n param_pairs k fn s s' i, + xmap_externctrl_params k fn args s = OK param_pairs s' i -> + (n < length args)%nat -> + exists r, (List.nth_error (fst (List.split param_pairs)) n = Some r) /\ + (s'.(st_externctrl) ! r = Some (fn, ctrl_param (n+k))). Proof. - intros. eapply collect_freshreg_trans; try eassumption. - eauto with htlspec. -Qed. - -Ltac rewrite_states := - match goal with - | [ H: ?x ?s = ?x ?s' |- _ ] => - let c1 := fresh "c" in - let c2 := fresh "c" in - remember (?x ?s) as c1; remember (?x ?s') as c2; try subst - end. - -Ltac inv_add_instr' H := - match type of H with - | ?f _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ _ _ _ = OK _ _ _ => unfold f in H - end; repeat unfold_match H; inversion H. - -Ltac inv_add_instr := - match goal with - | H: (if ?c then _ else _) _ = OK _ _ _ |- _ => destruct c eqn:EQN; try discriminate; inv_add_instr - | H: context[add_instr_skip _ _ _] |- _ => - inv_add_instr' H - | H: context[add_instr_skip _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_instr _ _ _ _] |- _ => - inv_add_instr' H - | H: context[add_instr _ _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_branch_instr _ _ _ _ _] |- _ => - inv_add_instr' H - | H: context[add_branch_instr _ _ _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_node_skip _ _ _] |- _ => - inv_add_instr' H - | H: context[add_node_skip _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - end. - -Ltac destruct_optional := - match goal with H: option ?r |- _ => destruct H end. + induction args. + - sauto use: nth_error_nil. + - intros. + monadInv H. + destruct n; simplify. + + destruct (split x0). simpl. + exists x. crush. monad_crush. + + destruct (IHargs n _ _ _ _ _ _ EQ1 ltac:(lia)). + destruct (split _). simpl in *. + eexists. replace (S (n + k))%nat with (n + S k)%nat by lia. + eassumption. + Qed. + +Lemma map_externctrl_params_spec : forall args n param_pairs fn s s' i, + map_externctrl_params fn args s = OK param_pairs s' i -> + (n < length args)%nat -> + exists r, (List.nth_error (fst (List.split param_pairs)) n = Some r) /\ + (s'.(st_externctrl) ! r = Some (fn, ctrl_param n)). +Proof. sauto use: helper__map_externctrl_params_spec. Qed. +Hint Resolve map_externctrl_params_spec : htlspec. Lemma iter_expand_instr_spec : - forall l fin rtrn stack s s' i x c, - HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> + forall l prog fin rtrn stack s s' i x c, + HTLMonadExtra.collectlist (transf_instr (Globalenvs.Genv.globalenv prog) fin rtrn stack) l s = OK x s' i -> list_norepet (List.map fst l) -> (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> - (forall pc instr, In (pc, instr) l -> - c!pc = Some instr -> - tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). + (forall pc instr, In (pc, instr) l -> c!pc = Some instr -> + tr_code (Globalenvs.Genv.globalenv prog) c pc s'.(st_datapath) s'.(st_controllogic) s'.(st_externctrl) fin rtrn s'.(st_st) stack instr). Proof. - induction l; simpl; intros; try contradiction. - destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. + (** Used to solve the simpler cases of tr_code: those involving tr_instr *) + Ltac tr_code_simple_tac := + eapply tr_code_single; + match goal with + | [ H : (?pc, _) = (?pc, ?instr) \/ In (?pc, ?instr) _ |- _ ] => + inversion H; + do 2 + match goal with + | [ H' : In (_, _) _ |- _ ] => solve [ eapply in_map with (f:=fst) in H'; contradiction ] + | [ H' : (pc, _) = (pc, instr) |- _ ] => inversion H' + end; + simplify; eauto with htlspec + end; + monad_crush. + + induction l; crush. + destruct a as [pc1 instr1]; simplify. inv H0. monadInv H. destruct (peq pc pc1). - subst. - destruct instr1 eqn:?; try discriminate; - try destruct_optional; inv_add_instr; econstructor; try assumption. - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. - apply Z.leb_le. assumption. - eapply in_map with (f := fst) in H9. contradiction. - - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. - econstructor. apply Z.leb_le; assumption. - apply EQ1. eapply in_map with (f := fst) in H14. contradiction. - - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. - econstructor. apply Z.leb_le; assumption. - apply EQ1. eapply in_map with (f := fst) in H14. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct H2. - * inversion H2. - replace (st_st s2) with (st_st s0) by congruence. - econstructor. apply Z.leb_le; assumption. - eauto with htlspec. - * apply in_map with (f := fst) in H2. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct H2. - * inversion H2. - replace (st_st s2) with (st_st s0) by congruence. - econstructor; try (apply Z.leb_le; apply andb_prop in EQN; apply EQN). - eauto with htlspec. - * apply in_map with (f := fst) in H2. contradiction. - - (*+ destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. - * inversion H14. constructor. congruence. - * apply in_map with (f := fst) in H14. contradiction. - *) - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. - * inversion H9. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H9. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. - * inversion H9. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H9. contradiction. - - - eapply IHl. apply EQ0. assumption. - destruct H2. inversion H2. subst. contradiction. - intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. - destruct H2. inv H2. contradiction. assumption. assumption. + destruct instr1 eqn:instr_eq; + repeat destruct_match; try discriminate; try monadInv1 EQ. + + (* Inop *) tr_code_simple_tac. + + (* Iop *) tr_code_simple_tac. + + (* Iload *) tr_code_simple_tac. + + (* Istore *) tr_code_simple_tac. + + (* Icall *) + inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. + inversion H. + + eapply tr_code_call; eauto; crush. + + repeat (eapply ex_intro). + + repeat (apply conj). + * monad_crush. + * monad_crush. + * monad_crush. + * transitivity (length x1). + replace l0 with (snd (List.split x1)). + apply split_length_r. + eapply map_externctrl_params_args; eassumption. + auto using split_length_l. + * intros. + destruct (map_externctrl_params_args _ _ _ _ _ _ EQ1); eauto using nth_error_length. + destruct (map_externctrl_params_spec _ n0 _ _ _ _ _ EQ1); eauto using nth_error_length. + exists x8. simplify; eauto. + monad_crush. + * eapply create_state_max; eassumption. + * replace x5 with (st_freshreg s6) in * by intro_step. + replace l0 with (snd (split x1)) by + eauto using map_externctrl_params_args. + rewrite combine_split. + monad_crush. + * monad_crush. + * replace x6 with (st_freshreg s7) in * by intro_step. + replace x5 with (st_freshreg s6) in * by intro_step. + monad_crush. + * replace x4 with (st_freshreg s5) in * by intro_step. + monad_crush. + + (* Icond *) tr_code_simple_tac. + + (* Ireturn *) + inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. + inversion H. + eapply tr_code_return; crush; eexists; simplify; monad_crush. + - eapply IHl; eauto. + intuition crush. Qed. Hint Resolve iter_expand_instr_spec : htlspec. -Lemma create_arr_inv : forall w x y z a b c d, - create_arr w x y z = OK (a, b) c d -> - y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). +Lemma map_incr_some : forall {A} map (s s' : st) idx (x : A), + (map s) ! idx = Some x -> + map_incr map s s' -> + (map s') ! idx = Some x. +Proof. intros * ? Hincr. destruct Hincr with idx; crush. Qed. +Hint Resolve map_incr_some : htlspec. + +Lemma tr_code_trans : forall ge c pc instr fin rtrn stack s s', + tr_code ge c pc (st_datapath s) (st_controllogic s) (st_externctrl s) fin rtrn (st_st s) stack instr -> + st_prop s s' -> + tr_code ge c pc (st_datapath s') (st_controllogic s') (st_externctrl s') fin rtrn (st_st s') stack instr. Proof. - inversion 1; split; auto. + intros * Htr Htrans. + destruct Htr. + + eapply tr_code_single. + * trans_step s s'. + * inversion Htrans. + destruct H6 with pc. crush. + replace ((st_datapath s') ! pc). + eassumption. + * inversion Htrans. + destruct H7 with pc. crush. + replace ((st_controllogic s') ! pc). + eassumption. + * inversion Htrans. crush. + + eapply tr_code_call; eauto with htlspec. + simplify. + inversion Htrans. + replace (st_st s'). + repeat (eapply ex_intro). + repeat (apply conj). + * eapply map_incr_some; inversion Htrans; eauto with htlspec. + * eapply map_incr_some; inversion Htrans; eauto with htlspec. + * eapply map_incr_some; inversion Htrans; eauto with htlspec. + * eassumption. + * intros. + destruct (H6 n0 ltac:(auto) ltac:(auto)) as [r [? ?]]. + eexists. split; eauto with htlspec. + * eauto with htlspec. + * eauto with htlspec. + * eauto with htlspec. + * eauto with htlspec. + * eauto with htlspec. + + eapply tr_code_return; eauto with htlspec. + inversion Htrans. + simplify. eexists. + replace (st_st s'). + repeat split; eauto with htlspec. + Unshelve. all: eauto. Qed. +Hint Resolve tr_code_trans : htlspec. -Lemma create_reg_inv : forall a b s r s' i, - create_reg a b s = OK r s' i -> - r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). +Lemma declare_params_freshreg_trans : forall params s s' x i, + declare_params params s = OK x s' i -> + st_freshreg s = st_freshreg s'. Proof. - inversion 1; auto. + induction params; unfold declare_params in *; intros * H. + - inv H. trivial. + - monadInv H. + transitivity (st_freshreg s0). + + monadInv EQ. auto. + + eauto. Qed. +Hint Resolve declare_params_freshreg_trans : htlspec. + +Lemma declare_params_externctrl_trans : forall params s s' x i, + declare_params params s = OK x s' i -> + st_externctrl s = st_externctrl s'. +Proof. + induction params; unfold declare_params in *; intros * H. + - inv H. trivial. + - monadInv H. + transitivity (st_externctrl s0). + + monadInv EQ. auto. + + eauto. +Qed. +Hint Resolve declare_params_freshreg_trans : htlspec. Theorem transl_module_correct : - forall f m, - transl_module f = Errors.OK m -> tr_module f m. + forall p f m, + transl_module p f = Errors.OK m -> tr_module (Globalenvs.Genv.globalenv p) f m. Proof. - intros until m. - unfold transl_module. - unfold run_mon. - destruct (transf_module f (max_state f)) eqn:?; try discriminate. - intros. inv H. + intros * H. + unfold transl_module in *. + unfold run_mon in *. + unfold_match H. + inv H. inversion s; subst. unfold transf_module in *. unfold stack_correct in *. - destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; - destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH; - destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN; - crush; - monadInv Heqr. - - repeat unfold_match EQ9. monadInv EQ9. - - (* TODO: We should be able to fold this into the automation. *) - pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5. - pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL. - pose proof (create_reg_inv _ _ _ _ _ _ EQ1) as RET_VAL. inv RET_VAL. - destruct x3. destruct x4. - pose proof (collect_trans_instr_freshreg_trans _ _ _ _ _ _ _ EQ2) as TR_INSTR. - pose proof (collect_declare_freshreg_trans _ _ _ _ _ _ EQ3) as TR_DEC. - pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL. - pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL. - pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL. - rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence. - rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *. - inv_incr. - econstructor; simpl; auto; try lia. - intros. - assert (EQ3D := EQ3). - apply collect_declare_datapath_trans in EQ3. - apply collect_declare_controllogic_trans in EQ3D. - replace (st_controllogic s10) with (st_controllogic s3) by congruence. - replace (st_datapath s10) with (st_datapath s3) by congruence. - replace (st_st s10) with (st_st s3) by congruence. - eapply iter_expand_instr_spec; eauto with htlspec. - rewrite H5. rewrite H7. apply EQ2. - apply PTree.elements_complete. - eauto with htlspec. - erewrite <- collect_declare_freshreg_trans; try eassumption. - lia. + destruct_match; simplify; crush. + monadInv Heqr. + + repeat destruct_match; crush. + repeat match goal with + | [ EQ : ret _ _ = OK _ _ _ |- _ ] => monadInv EQ + | [ EQ : OK _ _ _ = OK _ _ _ |- _ ] => monadInv EQ + | [ EQ : get _ = OK _ _ _ |- _ ] => monadInv EQ + end. + + econstructor; + eauto with htlspec; + try solve [ repeat relevant_monad_inv; crush ]. + - auto_apply declare_params_freshreg_trans. + replace (st_st s'). + monadInv EQ1. + inversion INCR. + repeat match goal with + | [ H : context[st_freshreg (max_state _)] |- _ ] => unfold max_state in H; simpl in H + end. + crush. + - assert (forall n, (st_externctrl (max_state f)) ! n = None) by (simplify; eauto using AssocMap.gempty). + assert (forall n, (st_externctrl s0) ! n = None) by (erewrite <- (declare_params_externctrl_trans); eauto). + assert (forall n, (st_externctrl s1) ! n = None) by (any_monad_inv; simplify; auto). + assert (forall n, (st_externctrl s2) ! n = None) by (any_monad_inv; simplify; auto). + assert (forall n, (st_externctrl s3) ! n = None) by (any_monad_inv; simplify; auto). + assert (forall n, (st_externctrl s4) ! n = None) by (any_monad_inv; simplify; auto). + assert (forall n, (st_externctrl s5) ! n = None) by (any_monad_inv; simplify; auto). + + assert (forall n, (st_externctrl s6) ! n = None) by (any_monad_inv; simplify; auto). + assert ((st_freshreg s6) > x6)%positive by (relevant_monad_inv; simplify; crush). + + intros. + repeat match goal with + | [ H: forall (_ : positive), _ |- _ ] => specialize (H r) + end. + + enough (n >= st_freshreg s6)%positive by lia. + inversion INCR13. + auto. Qed. diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml index a75d0ee..8608784 100644 --- a/src/hls/PrintHTL.ml +++ b/src/hls/PrintHTL.ml @@ -30,34 +30,53 @@ open VericertClflags let pstr pp = fprintf pp "%s" -let reg pp r = - fprintf pp "x%d" (P.to_int r) +let concat = String.concat "" -let rec regs pp = function - | [] -> () - | [r] -> reg pp r - | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl +let rec intersperse c = function + | [] -> [] + | [x] -> [x] + | x :: xs -> x :: c :: intersperse c xs + +let register a = sprintf "reg_%d" (P.to_int a) +let registers a = String.concat "" (intersperse ", " (List.map register a)) let print_instruction pp (pc, i) = fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i) +let string_controlsignal = function + | Coq_ctrl_finish -> "finish" + | Coq_ctrl_return -> "return" + | Coq_ctrl_start -> "start" + | Coq_ctrl_reset -> "rst" + | Coq_ctrl_clk -> "clk" + | Coq_ctrl_param idx -> sprintf "param_%d" (Nat.to_int idx) + +let print_externctrl pp ((local_reg : reg), ((target_mod: ident), (target_reg: controlsignal))) = + fprintf pp "%s -> %s.%s\n" (register local_reg) (extern_atom target_mod) (string_controlsignal target_reg) + +let ptree_to_list ptree = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements ptree)) + let print_module pp id f = - fprintf pp "%s(%a) {\n" (extern_atom id) regs f.mod_params; - let datapath = - List.sort - (fun (pc1, _) (pc2, _) -> compare pc2 pc1) - (List.rev_map - (fun (pc, i) -> (P.to_int pc, i)) - (PTree.elements f.mod_datapath)) in - let controllogic = - List.sort - (fun (pc1, _) (pc2, _) -> compare pc2 pc1) - (List.rev_map - (fun (pc, i) -> (P.to_int pc, i)) - (PTree.elements f.mod_controllogic)) in - fprintf pp " datapath {\n"; + fprintf pp "%s(%s) {\n" (extern_atom id) (registers f.mod_params); + + let externctrl = PTree.elements f.mod_externctrl in + let datapath = ptree_to_list f.mod_datapath in + let controllogic = ptree_to_list f.mod_controllogic in + + fprintf pp "externctrl {\n"; + List.iter (print_externctrl pp) externctrl; + fprintf pp " }\n\n"; + + fprintf pp "datapath {\n"; List.iter (print_instruction pp) datapath; - fprintf pp " }\n\n controllogic {\n"; + fprintf pp " }\n\n"; + + fprintf pp "controllogic {\n"; List.iter (print_instruction pp) controllogic; fprintf pp " }\n}\n\n" @@ -71,10 +90,10 @@ let print_program pp prog = let destination : string option ref = ref None -let print_if prog = +let print_if passno prog = match !destination with | None -> () | Some f -> - let oc = open_out f in - print_program oc prog; - close_out oc + let oc = open_out (f ^ "." ^ Z.to_string passno) in + print_program oc prog; + close_out oc diff --git a/src/hls/PrintVerilog.mli b/src/hls/PrintVerilog.mli index 6a15ee9..dbb8ba0 100644 --- a/src/hls/PrintVerilog.mli +++ b/src/hls/PrintVerilog.mli @@ -18,6 +18,8 @@ val pprint_stmnt : int -> Verilog.stmnt -> string +val pprint_expr : Verilog.expr -> string + val print_value : out_channel -> ValueInt.value -> unit val print_program : bool -> out_channel -> Verilog.program -> unit diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v new file mode 100644 index 0000000..b9fbcaa --- /dev/null +++ b/src/hls/Renaming.v @@ -0,0 +1,231 @@ +Require Import compcert.common.AST. + +Require Import vericert.hls.HTL. +Require Import vericert.hls.Verilog. +Require Import vericert.hls.AssocMap. + +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.common.Maps. + +Record renumber_state: Type := + mk_renumber_state { + renumber_freshreg : reg; + renumber_regmap : PTree.t reg; + }. + +Module RenumberState <: State. + Definition st := renumber_state. + + Definition st_prop (st1 st2 : st) := True. + Hint Unfold st_prop : htl_renumber. + + Lemma st_refl : forall (s : st), st_prop s s. + Proof. constructor. Qed. + + Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. + Proof. constructor. Qed. +End RenumberState. + +Module RenumberMonad := Statemonad(RenumberState). +Module RenumberMonadExtra := Monad.MonadExtra(RenumberMonad). + +Import RenumberMonad. +Import RenumberState. +Import RenumberMonadExtra. +Import MonadNotation. + +Definition map_reg (r: reg) : mon reg := + fun st => OK + (renumber_freshreg st) + (mk_renumber_state (Pos.succ (renumber_freshreg st)) + (PTree.set r (renumber_freshreg st) (renumber_regmap st))) + ltac:(auto with htl_renumber). + +Definition clear_regmap : mon unit := + fun st => OK + tt + (mk_renumber_state (renumber_freshreg st) + (PTree.empty reg)) + ltac:(auto with htl_renumber). + +Definition renumber_reg (r : reg) : mon reg := + do st <- get; + match PTree.get r (renumber_regmap st) with + | Some reg' => ret reg' + | None => map_reg r + end. + +Fixpoint renumber_expr (expr : Verilog.expr) := + match expr with + | Vlit val => ret (Vlit val) + | Vvar reg => + do reg' <- renumber_reg reg; + ret (Vvar reg') + | Vvari reg e => + do reg' <- renumber_reg reg; + do e' <- renumber_expr e; + ret (Vvari reg' e') + | Vinputvar reg => + do reg' <- renumber_reg reg; + ret (Vvar reg') + | Vbinop op e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vbinop op e1' e2') + | Vunop op e => + do e' <- renumber_expr e; + ret (Vunop op e') + | Vternary e1 e2 e3 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + do e3' <- renumber_expr e3; + ret (Vternary e1' e2' e3') + | Vrange r e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + do r' <- renumber_reg r; + ret (Vrange r e1' e2') + end. + +Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := + match stmnt with + | Vskip => ret Vskip + | Vseq s1 s2 => + do s1' <- renumber_stmnt s1; + do s2' <- renumber_stmnt s2; + ret (Vseq s1' s2') + | Vcond e s1 s2 => + do e' <- renumber_expr e; + do s1' <- renumber_stmnt s1; + do s2' <- renumber_stmnt s2; + ret (Vcond e' s1' s2') + | Vcase e cs def => + do e' <- renumber_expr e; + do cs' <- sequence (map + (fun (c : (Verilog.expr * Verilog.stmnt)) => + let (c_expr, c_stmnt) := c in + do expr' <- renumber_expr c_expr; + do stmnt' <- renumber_stmnt c_stmnt; + ret (expr', stmnt')) cs); + do def' <- match def with + | None => ret None + | Some d => do def' <- renumber_stmnt d; ret (Some def') + end; + ret (Vcase e' cs' def') + | Vblock e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vblock e1' e2') + | Vnonblock e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vnonblock e1' e2') + end. + +Fixpoint xrenumber_reg_assocmap {A} (regmap : list (reg * A)) : mon (list (reg * A)) := + match regmap with + | nil => ret nil + | (r, v) :: l => + do r' <- renumber_reg r; + do l' <- xrenumber_reg_assocmap l; + ret ((r', v) :: l') + end. + +Definition renumber_reg_assocmap {A} (regmap : AssocMap.t A) : mon (AssocMap.t A) := + do l <- xrenumber_reg_assocmap (AssocMap.elements regmap); + ret (AssocMap_Properties.of_list l). + +Definition renumber_module (m : HTL.module) : mon HTL.module := + do mod_start' <- renumber_reg (HTL.mod_start m); + do mod_reset' <- renumber_reg (HTL.mod_reset m); + do mod_clk' <- renumber_reg (HTL.mod_clk m); + do mod_finish' <- renumber_reg (HTL.mod_finish m); + do mod_return' <- renumber_reg (HTL.mod_return m); + do mod_st' <- renumber_reg (HTL.mod_st m); + do mod_stk' <- renumber_reg (HTL.mod_stk m); + do mod_params' <- traverselist renumber_reg (HTL.mod_params m); + do mod_controllogic' <- traverse_ptree1 renumber_stmnt (HTL.mod_controllogic m); + do mod_datapath' <- traverse_ptree1 renumber_stmnt (HTL.mod_datapath m); + + do mod_scldecls' <- renumber_reg_assocmap (HTL.mod_scldecls m); + do mod_arrdecls' <- renumber_reg_assocmap (HTL.mod_arrdecls m); + do mod_externctrl' <- renumber_reg_assocmap (HTL.mod_externctrl m); + + do _ <- clear_regmap; + + match zle (Z.pos (max_pc_map mod_datapath')) Integers.Int.max_unsigned, + zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned with + | left LEDATA, left LECTRL => + ret (HTL.mkmodule + mod_params' + mod_datapath' + mod_controllogic' + (HTL.mod_entrypoint m) + mod_st' + mod_stk' + (HTL.mod_stk_len m) + mod_finish' + mod_return' + mod_start' + mod_reset' + mod_clk' + mod_scldecls' + mod_arrdecls' + mod_externctrl' + (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) + | _, _ => error (Errors.msg "More than 2^32 states.") + end. + +Definition renumber_fundef (fundef : HTL.fundef) : mon HTL.fundef := + match fundef with + | Internal m => do renumbered <- renumber_module m; ret (Internal renumbered) + | _ => ret fundef + end. + +Section TRANSF_PROGRAM_STATEFUL. + Import RenumberMonad. + Import RenumberState. + Import RenumberMonadExtra. + Import MonadNotation. + + Variables A B V : Type. + Variable transf_fun: ident -> A -> RenumberMonad.mon B. + + Fixpoint transf_globdefs (l: list (ident * globdef A V)) : RenumberMonad.mon (list (ident * globdef B V)) := + match l with + | nil => RenumberMonad.ret nil + | (id, Gfun f) :: l' => + do tf <- transf_fun id f; + do tl' <- transf_globdefs l'; + RenumberMonad.ret ((id, Gfun tf) :: tl') + | (id, Gvar v) :: l' => + do tl' <- transf_globdefs l'; + RenumberMonad.ret ((id, Gvar v) :: tl') + end. + + Definition transform_stateful_program (init_state : RenumberState.st) (p: AST.program A V) : Errors.res (AST.program B V) := + RenumberMonad.run_mon init_state ( + do gl' <- transf_globdefs p.(prog_defs); + RenumberMonad.ret (mkprogram gl' p.(prog_public) p.(prog_main))). + +End TRANSF_PROGRAM_STATEFUL. + +Definition transf_program (p : HTL.program) : Errors.res HTL.program := + transform_stateful_program _ _ _ + (fun _ f => renumber_fundef f) + (mk_renumber_state 1%positive (PTree.empty reg)) + p. + +Definition match_prog : HTL.program -> HTL.program -> Prop := fun _ _ => True. + +Instance TransfRenamingLink : Linking.TransfLink match_prog. +Admitted. + +Lemma transf_program_match : forall p tp, + Renaming.transf_program p = Errors.OK tp -> match_prog p tp. +Admitted. + +Lemma transf_program_correct : forall p tp, + match_prog p tp -> Smallstep.forward_simulation (HTL.semantics p) (HTL.semantics tp). +Admitted. diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 1dc7e99..0df8b7e 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -293,6 +293,20 @@ Definition posToLit (p : positive) : expr := Definition fext := unit. Definition fextclk := nat -> fext. +Definition map_body (f : list module_item -> list module_item) (m : module) := + mkmodule + (mod_start m) + (mod_reset m) + (mod_clk m) + (mod_finish m) + (mod_return m) + (mod_st m) + (mod_stk m) + (mod_stk_len m) + (mod_args m) + (f (mod_body m)) + (mod_entrypoint m). + (** ** State The [state] contains the following items: diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index aba2293..1ded68a 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -1,6 +1,7 @@ (* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * 2021 Michalis Pardalos <mpardalos@gmail.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -17,88 +18,133 @@ *) Require Import compcert.common.AST. -Require compcert.common.Errors. -Require Import compcert.lib.Maps. +Require Import compcert.common.Errors. +Require Import vericert.common.Maps. +Require Import vericert.common.Statemonad. Require Import vericert.common.Vericertlib. Require Import vericert.hls.AssocMap. Require Import vericert.hls.HTL. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. +Import ListNotations. -Definition transl_list_fun (a : node * Verilog.stmnt) := - let (n, stmnt) := a in - (Vlit (posToValue n), stmnt). - -Definition transl_list st := map transl_list_fun st. - -Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) := - match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end. - -Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. - -Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := - match a with (r, (io, VArray sz l)) => (Vdeclarr io r sz l) end. - -Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. - -Definition inst_ram clk ram := - Valways (Vnegedge clk) - (Vcond (Vbinop Vne (Vvar (ram_u_en ram)) (Vvar (ram_en ram))) - (Vseq (Vcond (Vvar (ram_wr_en ram)) - (Vnonblock (Vvari (ram_mem ram) (Vvar (ram_addr ram))) - (Vvar (ram_d_in ram))) - (Vnonblock (Vvar (ram_d_out ram)) - (Vvari (ram_mem ram) (Vvar (ram_addr ram))))) - (Vnonblock (Vvar (ram_en ram)) (Vvar (ram_u_en ram)))) - Vskip). - -Definition transl_module (m : HTL.module) : Verilog.module := - let case_el_ctrl := list_to_stmnt (transl_list (PTree.elements m.(mod_controllogic))) in - let case_el_data := list_to_stmnt (transl_list (PTree.elements m.(mod_datapath))) in - match m.(HTL.mod_ram) with - | Some ram => - let body := - Valways (Vposedge m.(HTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(HTL.mod_reset)) (Vlit (ZToValue 1))) - (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint)))) - (Vcase (Vvar m.(HTL.mod_st)) case_el_ctrl (Some Vskip))) - :: Valways (Vposedge m.(HTL.mod_clk)) (Vcase (Vvar m.(HTL.mod_st)) case_el_data (Some Vskip)) - :: inst_ram m.(HTL.mod_clk) ram - :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) - ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in - Verilog.mkmodule m.(HTL.mod_start) - m.(HTL.mod_reset) - m.(HTL.mod_clk) - m.(HTL.mod_finish) - m.(HTL.mod_return) - m.(HTL.mod_st) - m.(HTL.mod_stk) - m.(HTL.mod_stk_len) - m.(HTL.mod_params) - body - m.(HTL.mod_entrypoint) - | None => - let body := - Valways (Vposedge m.(HTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(HTL.mod_reset)) (Vlit (ZToValue 1))) - (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint)))) - (Vcase (Vvar m.(HTL.mod_st)) case_el_ctrl (Some Vskip))) - :: Valways (Vposedge m.(HTL.mod_clk)) (Vcase (Vvar m.(HTL.mod_st)) case_el_data (Some Vskip)) - :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) - ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in - Verilog.mkmodule m.(HTL.mod_start) - m.(HTL.mod_reset) - m.(HTL.mod_clk) - m.(HTL.mod_finish) - m.(HTL.mod_return) - m.(HTL.mod_st) - m.(HTL.mod_stk) - m.(HTL.mod_stk_len) - m.(HTL.mod_params) - body - m.(HTL.mod_entrypoint) - end. - -Definition transl_fundef := transf_fundef transl_module. - -Definition transl_program (p: HTL.program) : Verilog.program := - transform_program transl_fundef p. +Section TRANSLATE. + Local Open Scope error_monad_scope. + + Definition transl_states : list (HTL.node * HTL.datapath_stmnt) -> list (Verilog.expr * Verilog.stmnt) := + map (fun '(n, s) => (Verilog.Vlit (posToValue n), s)). + + Definition scl_to_Vdecls := + map (fun '(r, (io, Verilog.VScalar sz)) => Vdeclaration (Vdecl io r sz)). + + Definition arr_to_Vdeclarrs := + map (fun '(r, (io, Verilog.VArray sz l)) => Vdeclaration (Vdeclarr io r sz l)). + + Definition called_functions (main_name : ident) (m : HTL.module) : list ident := + (* remove duplicates *) + List.nodup Pos.eq_dec + (* Take just the module name *) + (List.map (Basics.compose fst snd) + (* Remove the main module if it's referenced *) + (List.filter (fun it => negb (Pos.eqb (fst (snd it)) main_name)) + (PTree.elements (HTL.mod_externctrl m)))). + + (** Clean up declarations for an inlined module. Make IO decls into reg, and remove the clk declaration *) + Definition clean_up_decl (clk : reg) (it : Verilog.module_item) := + match it with + | Vdeclaration (Vdecl _ reg sz) => + if Pos.eqb reg clk + then None + else Some (Vdeclaration (Vdecl None reg sz)) + | Vdeclaration (Vdeclarr (Some _) reg sz len) => + Some (Vdeclaration (Vdeclarr None reg sz len)) + | _ => Some it + end. + + Definition mod_body (m : HTL.module) := + + + (* FIXME Remove the fuel parameter (recursion limit)*) + Fixpoint transl_module (fuel : nat) (prog : HTL.program) (externclk : option reg) (m : HTL.module) : res Verilog.module := + match fuel with + | O => Error (msg "Veriloggen: transl_module recursion too deep") + | S fuel' => + let clk := match externclk with + | None => HTL.mod_clk m + | Some c => c + end in + + let inline_names := called_functions (AST.prog_main prog) m in + let modmap := prog_modmap prog in + let htl_modules := PTree.filter + (fun m _ => List.existsb (Pos.eqb m) inline_names) + modmap in + do translated_modules <- PTree.traverse (fun _ => transl_module fuel' prog (Some clk)) htl_modules; + let cleaned_modules := PTree.map1 (map_body (Option.map_option (clean_up_decl clk))) + translated_modules in + + + let case_el_ctrl := transl_states (PTree.elements (HTL.mod_controllogic m)) in + let case_el_data := transl_states (PTree.elements (HTL.mod_datapath m)) in + + let externctrl := HTL.mod_externctrl m in + + (* Only declare the clock if this is the top-level module, i.e. there is no inherited clock *) + let maybe_clk_decl := match externclk with + | None => scl_to_Vdecls [(clk, (Some Vinput, VScalar 1))] + | Some _ => [] + end in + + let local_arrdecls := PTree.filter (fun r _ => negb (PTree.contains r externctrl)) (HTL.mod_arrdecls m) in + let arr_decls := arr_to_Vdeclarrs (AssocMap.elements local_arrdecls) in + + let local_scldecls := PTree.filter (fun r _ => negb (PTree.contains r externctrl)) (HTL.mod_scldecls m) in + let scl_decls := scl_to_Vdecls (AssocMap.elements local_scldecls) in + + let body : list Verilog.module_item := + match (HTL.mod_ram m) with + | Some ram => + Valways (Vposedge clk) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1))) + (Vseq + (Vnonblock (Vvar (HTL.mod_st m)) (Vlit (posToValue (HTL.mod_entrypoint m)))) + (Vnonblock (Vvar (HTL.mod_finish m)) (Vlit (ZToValue 0)))) + (Vcase (Vvar (HTL.mod_st m)) case_el_ctrl (Some Vskip))) + :: Valways (Vposedge clk) (Vcase (Vvar (HTL.mod_st m)) case_el_data (Some Vskip)) + :: inst_ram m.(HTL.mod_clk) ram + :: arr_decls + ++ scl_decls + ++ maybe_clk_decl + ++ List.flat_map Verilog.mod_body (List.map snd (PTree.elements cleaned_modules)) + | Nothing => + Valways (Vposedge clk) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1))) + (Vseq + (Vnonblock (Vvar (HTL.mod_st m)) (Vlit (posToValue (HTL.mod_entrypoint m)))) + (Vnonblock (Vvar (HTL.mod_finish m)) (Vlit (ZToValue 0)))) + (Vcase (Vvar (HTL.mod_st m)) case_el_ctrl (Some Vskip))) + :: Valways (Vposedge clk) (Vcase (Vvar (HTL.mod_st m)) case_el_data (Some Vskip)) + :: arr_decls + ++ scl_decls + ++ maybe_clk_decl + ++ List.flat_map Verilog.mod_body (List.map snd (PTree.elements cleaned_modules)) + end + in + + OK (Verilog.mkmodule + (HTL.mod_start m) + (HTL.mod_reset m) + (HTL.mod_clk m) + (HTL.mod_finish m) + (HTL.mod_return m) + (HTL.mod_st m) + (HTL.mod_stk m) + (HTL.mod_stk_len m) + (HTL.mod_params m) + body + (HTL.mod_entrypoint m)) + end. + + Definition transl_fundef (prog : HTL.program) := transf_partial_fundef (transl_module 10 prog None). + Definition transl_program (prog : HTL.program) := transform_partial_program (transl_fundef prog) prog. + +End TRANSLATE. diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index b621632..c54f726 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -17,6 +17,7 @@ *) From compcert Require Import Smallstep Linking Integers Globalenvs. +From compcert Require Errors. From vericert Require HTL. From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap. Require Import Lia. @@ -24,206 +25,244 @@ Require Import Lia. Local Open Scope assocmap. Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := - match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog. + match_program (fun cu f tf => Errors.OK tf = transl_fundef prog f) eq prog tprog. Lemma transf_program_match: - forall prog, match_prog prog (transl_program prog). + forall prog tprog, transl_program prog = Errors.OK tprog -> match_prog prog tprog. Proof. - intros. eapply match_transform_program_contextual. auto. + intros. unfold transl_program in *. eapply match_transform_partial_program_contextual; eauto. Qed. -Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := -| match_stack : - forall res m pc reg_assoc arr_assoc hstk vstk, - match_stacks hstk vstk -> - match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk) - (Stackframe res (transl_module m) pc - reg_assoc arr_assoc :: vstk) -| match_stack_nil : match_stacks nil nil. - -Inductive match_states : HTL.state -> state -> Prop := -| match_state : - forall m st reg_assoc arr_assoc hstk vstk, - match_stacks hstk vstk -> - match_states (HTL.State hstk m st reg_assoc arr_assoc) - (State vstk (transl_module m) st reg_assoc arr_assoc) -| match_returnstate : - forall v hstk vstk, - match_stacks hstk vstk -> - match_states (HTL.Returnstate hstk v) (Returnstate vstk v) -| match_initial_call : - forall m, - match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). - -Lemma Vlit_inj : - forall a b, Vlit a = Vlit b -> a = b. -Proof. inversion 1. trivial. Qed. - -Lemma posToValue_inj : - forall a b, - 0 <= Z.pos a <= Int.max_unsigned -> - 0 <= Z.pos b <= Int.max_unsigned -> - posToValue a = posToValue b -> - a = b. -Proof. - intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id. - rewrite <- Int.unsigned_repr at 1; try assumption. - symmetry. - rewrite <- Int.unsigned_repr at 1; try assumption. - unfold posToValue in *. rewrite H1; auto. -Qed. - -Lemma valueToPos_inj : - forall a b, - 0 < Int.unsigned a -> - 0 < Int.unsigned b -> - valueToPos a = valueToPos b -> - a = b. -Proof. - intros. unfold valueToPos in *. - rewrite <- Int.repr_unsigned at 1. - rewrite <- Int.repr_unsigned. - apply Pos2Z.inj_iff in H1. - rewrite Z2Pos.id in H1; auto. - rewrite Z2Pos.id in H1; auto. - rewrite H1. auto. -Qed. - -Lemma unsigned_posToValue_le : - forall p, - Z.pos p <= Int.max_unsigned -> - 0 < Int.unsigned (posToValue p). -Proof. - intros. unfold posToValue. rewrite Int.unsigned_repr; lia. -Qed. - -Lemma transl_list_fun_fst : - forall p1 p2 a b, - 0 <= Z.pos p1 <= Int.max_unsigned -> - 0 <= Z.pos p2 <= Int.max_unsigned -> - transl_list_fun (p1, a) = transl_list_fun (p2, b) -> - (p1, a) = (p2, b). -Proof. - intros. unfold transl_list_fun in H1. apply pair_equal_spec in H1. - destruct H1. rewrite H2. apply Vlit_inj in H1. - apply posToValue_inj in H1; try assumption. - rewrite H1; auto. -Qed. - -Lemma Zle_relax : - forall p q r, - p < q <= r -> - p <= q <= r. -Proof. lia. Qed. -Hint Resolve Zle_relax : verilogproof. - -Lemma transl_in : - forall l p, - 0 <= Z.pos p <= Int.max_unsigned -> - (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> - In p (map fst l). -Proof. - induction l. - - simplify. auto. - - intros. destruct a. simplify. destruct (peq p0 p); auto. - right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction. - auto with verilogproof. - apply IHl; auto. -Qed. - -Lemma transl_notin : - forall l p, - 0 <= Z.pos p <= Int.max_unsigned -> - (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_list l)). -Proof. - induction l; auto. intros. destruct a. unfold not in *. intros. - simplify. - destruct (peq p0 p). apply H1. auto. apply H1. - unfold transl_list in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H. - contradiction. - auto with verilogproof. auto. - right. apply transl_in; auto. -Qed. - -Lemma transl_norepet : - forall l, - (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_list l)). -Proof. - induction l. - - intros. simpl. apply list_norepet_nil. - - destruct a. intros. simpl. apply list_norepet_cons. - inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto. - intros. apply H. destruct (peq p0 p); subst; simplify; auto. - assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto. - simplify. inv H0. assumption. -Qed. - -Lemma transl_list_correct : - forall l v ev f asr asa asrn asan asr' asa' asrn' asan', - (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - list_norepet (List.map fst l) -> - asr!ev = Some v -> - (forall p s, - In (p, s) l -> - v = posToValue p -> - stmnt_runp f - {| assoc_blocking := asr; assoc_nonblocking := asrn |} - {| assoc_blocking := asa; assoc_nonblocking := asan |} - s - {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} - {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> - stmnt_runp f - {| assoc_blocking := asr; assoc_nonblocking := asrn |} - {| assoc_blocking := asa; assoc_nonblocking := asan |} - (Vcase (Vvar ev) (list_to_stmnt (transl_list l)) (Some Vskip)) - {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} - {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). -Proof. - induction l as [| a l IHl]. - - contradiction. - - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN. - destruct a as [p' s']. simplify. - destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match. - constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default. - rewrite ASSOC. trivial. constructor. auto. - inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption. - inv NOREP. eapply in_map with (f := fst) in INV. contradiction. - - eapply stmnt_runp_Vcase_nomatch. constructor. simplify. - unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC. - trivial. constructor. unfold not. intros. apply n. apply posToValue_inj. - apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction. - eapply in_map with (f := fst) in H0. auto. - apply Zle_relax. apply BOUND; auto. auto. - - eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. - trivial. assumption. -Qed. -Hint Resolve transl_list_correct : verilogproof. - -Lemma pc_wf : - forall A m p v, - (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> - m!p = Some v -> - 0 <= Z.pos p <= Int.max_unsigned. -Proof. - intros A m p v LT S. apply Zle_relax. apply LT. - apply AssocMap.elements_correct in S. remember (p, v) as x. - exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto. -Qed. - -Lemma mis_stepp_decl : - forall l asr asa f, - mis_stepp f asr asa (map Vdeclaration l) asr asa. -Proof. - induction l. - - intros. constructor. - - intros. simplify. econstructor. constructor. auto. -Qed. -Hint Resolve mis_stepp_decl : verilogproof. +Instance TransfVerilogLink : TransfLink Veriloggenproof.match_prog. +Admitted. + +(* Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := *) +(* | match_stack : *) +(* forall res m pc reg_assoc arr_assoc hstk vstk, *) +(* match_stacks hstk vstk -> *) +(* match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk) *) +(* (Stackframe res (transl_module m) pc *) +(* reg_assoc arr_assoc :: vstk) *) +(* | match_stack_nil : match_stacks nil nil. *) + +(* Inductive match_states : HTL.state -> state -> Prop := *) +(* | match_state : *) +(* forall m st reg_assoc arr_assoc hstk vstk, *) +(* match_stacks hstk vstk -> *) +(* match_states (HTL.State hstk m st reg_assoc arr_assoc) *) +(* (State vstk (transl_module m) st reg_assoc arr_assoc) *) +(* | match_returnstate : *) +(* forall v hstk vstk, *) +(* match_stacks hstk vstk -> *) +(* match_states (HTL.Returnstate hstk v) (Returnstate vstk v) *) +(* | match_initial_call : *) +(* forall m, *) +(* match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). *) + +(* Lemma Vlit_inj : *) +(* forall a b, Vlit a = Vlit b -> a = b. *) +(* Proof. inversion 1. trivial. Qed. *) + +(* Lemma posToValue_inj : *) +(* forall a b, *) +(* 0 <= Z.pos a <= Int.max_unsigned -> *) +(* 0 <= Z.pos b <= Int.max_unsigned -> *) +(* posToValue a = posToValue b -> *) +(* a = b. *) +(* Proof. *) +(* intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id. *) +(* rewrite <- Int.unsigned_repr at 1; try assumption. *) +(* symmetry. *) +(* rewrite <- Int.unsigned_repr at 1; try assumption. *) +(* unfold posToValue in *. rewrite H1; auto. *) +(* Qed. *) + +(* Lemma valueToPos_inj : *) +(* forall a b, *) +(* 0 < Int.unsigned a -> *) +(* 0 < Int.unsigned b -> *) +(* valueToPos a = valueToPos b -> *) +(* a = b. *) +(* Proof. *) +(* intros. unfold valueToPos in *. *) +(* rewrite <- Int.repr_unsigned at 1. *) +(* rewrite <- Int.repr_unsigned. *) +(* apply Pos2Z.inj_iff in H1. *) +(* rewrite Z2Pos.id in H1; auto. *) +(* rewrite Z2Pos.id in H1; auto. *) +(* rewrite H1. auto. *) +(* Qed. *) + +(* Lemma unsigned_posToValue_le : *) +(* forall p, *) +(* Z.pos p <= Int.max_unsigned -> *) +(* 0 < Int.unsigned (posToValue p). *) +(* Proof. *) +(* intros. unfold posToValue. rewrite Int.unsigned_repr; lia. *) +(* Qed. *) + +(* Lemma transl_ctrl_fun_fst : *) +(* forall p1 p2 a b, *) +(* 0 <= Z.pos p1 <= Int.max_unsigned -> *) +(* 0 <= Z.pos p2 <= Int.max_unsigned -> *) +(* transl_ctrl_fun (p1, a) = transl_ctrl_fun (p2, b) -> *) +(* (p1, a) = (p2, b). *) +(* Proof. *) +(* intros. unfold transl_ctrl_fun in H1. apply pair_equal_spec in H1. *) +(* destruct H1. rewrite H2. apply Vlit_inj in H1. *) +(* apply posToValue_inj in H1; try assumption. *) +(* rewrite H1; auto. *) +(* Qed. *) + +(* Lemma transl_data_fun_fst : *) +(* forall p1 p2 a b, *) +(* 0 <= Z.pos p1 <= Int.max_unsigned -> *) +(* 0 <= Z.pos p2 <= Int.max_unsigned -> *) +(* transl_datapath_fun (p1, a) = transl_datapath_fun (p2, b) -> *) +(* p1 = p2. *) +(* Proof. *) +(* intros. *) +(* unfold transl_datapath_fun in H1. apply pair_equal_spec in H1. destruct H1. *) +(* apply Vlit_inj in H1. apply posToValue_inj in H1; assumption. *) +(* Qed. *) + +(* Lemma Zle_relax : *) +(* forall p q r, *) +(* p < q <= r -> *) +(* p <= q <= r. *) +(* Proof. lia. Qed. *) +(* Hint Resolve Zle_relax : verilogproof. *) + +(* Lemma transl_in : *) +(* forall l p, *) +(* 0 <= Z.pos p <= Int.max_unsigned -> *) +(* (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* In (Vlit (posToValue p)) (map fst (map transl_ctrl_fun l)) -> *) +(* In p (map fst l). *) +(* Proof. *) +(* induction l. *) +(* - simplify. auto. *) +(* - intros. destruct a. simplify. destruct (peq p0 p); auto. *) +(* right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction. *) +(* auto with verilogproof. *) +(* apply IHl; auto. *) +(* Qed. *) + +(* Lemma transl_notin : *) +(* forall l p, *) +(* 0 <= Z.pos p <= Int.max_unsigned -> *) +(* (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_ctrl l)). *) +(* Proof. *) +(* induction l; auto. intros. destruct a. unfold not in *. intros. *) +(* simplify. *) +(* destruct (peq p0 p). apply H1. auto. apply H1. *) +(* unfold transl_ctrl in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H. *) +(* contradiction. *) +(* auto with verilogproof. auto. *) +(* right. apply transl_in; auto. *) +(* Qed. *) + +(* Lemma transl_norepet : *) +(* forall l, *) +(* (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_ctrl l)). *) +(* Proof. *) +(* induction l. *) +(* - intros. simpl. apply list_norepet_nil. *) +(* - destruct a. intros. simpl. apply list_norepet_cons. *) +(* inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto. *) +(* intros. apply H. destruct (peq p0 p); subst; simplify; auto. *) +(* assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto. *) +(* simplify. inv H0. assumption. *) +(* Qed. *) + +(* Lemma transl_ctrl_correct : *) +(* forall l v ev f asr asa asrn asan asr' asa' asrn' asan', *) +(* (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* list_norepet (List.map fst l) -> *) +(* asr!ev = Some v -> *) +(* (forall p s, *) +(* In (p, s) l -> *) +(* v = posToValue p -> *) +(* stmnt_runp f *) +(* {| assoc_blocking := asr; assoc_nonblocking := asrn |} *) +(* {| assoc_blocking := asa; assoc_nonblocking := asan |} *) +(* s *) +(* {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *) +(* {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> *) +(* stmnt_runp f *) +(* {| assoc_blocking := asr; assoc_nonblocking := asrn |} *) +(* {| assoc_blocking := asa; assoc_nonblocking := asan |} *) +(* (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip)) *) +(* {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *) +(* {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). *) +(* Proof. *) +(* induction l as [| a l IHl]. *) +(* - contradiction. *) +(* - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN. *) +(* destruct a as [p' s']. simplify. *) +(* destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match. *) +(* constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default. *) +(* rewrite ASSOC. trivial. constructor. auto. *) +(* inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption. *) +(* inv NOREP. eapply in_map with (f := fst) in INV. contradiction. *) + +(* eapply stmnt_runp_Vcase_nomatch. constructor. simplify. *) +(* unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC. *) +(* trivial. constructor. unfold not. intros. apply n. apply posToValue_inj. *) +(* apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction. *) +(* eapply in_map with (f := fst) in H0. auto. *) +(* apply Zle_relax. apply BOUND; auto. auto. *) + +(* eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. *) +(* trivial. assumption. *) +(* Qed. *) +(* Hint Resolve transl_ctrl_correct : verilogproof. *) + +(* (* FIXME Probably wrong we probably need some statemnt about datapath_statement_runp *) *) +(* Lemma transl_datapath_correct : *) +(* forall l v ev f asr asa asrn asan asr' asa' asrn' asan', *) +(* (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* list_norepet (List.map fst l) -> *) +(* asr!ev = Some v -> *) +(* (forall p s, *) +(* In (p, s) l -> *) +(* v = posToValue p -> *) +(* stmnt_runp f *) +(* {| assoc_blocking := asr; assoc_nonblocking := asrn |} *) +(* {| assoc_blocking := asa; assoc_nonblocking := asan |} *) +(* s *) +(* {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *) +(* {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> *) +(* stmnt_runp f *) +(* {| assoc_blocking := asr; assoc_nonblocking := asrn |} *) +(* {| assoc_blocking := asa; assoc_nonblocking := asan |} *) +(* (Vcase (Vvar ev) (transl_ctrl l) (Some Vskip)) *) +(* {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} *) +(* {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). *) +(* Proof. Admitted. *) + +(* Lemma pc_wf : *) +(* forall A m p v, *) +(* (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> *) +(* m!p = Some v -> *) +(* 0 <= Z.pos p <= Int.max_unsigned. *) +(* Proof. *) +(* intros A m p v LT S. apply Zle_relax. apply LT. *) +(* apply AssocMap.elements_correct in S. remember (p, v) as x. *) +(* exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto. *) +(* Qed. *) + +(* Lemma mis_stepp_decl : *) +(* forall l asr asa f, *) +(* mis_stepp f asr asa (map Vdeclaration l) asr asa. *) +(* Proof. *) +(* induction l. *) +(* - intros. constructor. *) +(* - intros. simplify. econstructor. constructor. auto. *) +(* Qed. *) +(* Hint Resolve mis_stepp_decl : verilogproof. *) Lemma mis_stepp_negedge_decl : forall l asr asa f, @@ -350,195 +389,133 @@ Section CORRECTNESS. Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed. Hint Resolve symbols_preserved : verilogproof. - Lemma function_ptr_translated: - forall (b: Values.block) (f: HTL.fundef), - Genv.find_funct_ptr ge b = Some f -> - exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf. - Proof. - intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. - intros (cu & tf & P & Q & R); exists tf; auto. - Qed. - Hint Resolve function_ptr_translated : verilogproof. - - Lemma functions_translated: - forall (v: Values.val) (f: HTL.fundef), - Genv.find_funct ge v = Some f -> - exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef f = tf. - Proof. - intros. exploit (Genv.find_funct_match TRANSL); eauto. - intros (cu & tf & P & Q & R); exists tf; auto. - Qed. - Hint Resolve functions_translated : verilogproof. - - Lemma senv_preserved: - Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). - Proof. - intros. eapply (Genv.senv_match TRANSL). - Qed. - Hint Resolve senv_preserved : verilogproof. - - Ltac unfold_replace := - match goal with - | H: HTL.mod_ram _ = _ |- context[transl_module] => - unfold transl_module; rewrite H - end. - - Theorem transl_step_correct : - forall (S1 : HTL.state) t S2, - HTL.step ge S1 t S2 -> - forall (R1 : state), - match_states S1 R1 -> - exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. - Proof. - induction 1; intros R1 MSTATE; inv MSTATE; destruct (HTL.mod_ram m) eqn:?. - - econstructor; split. apply Smallstep.plus_one. econstructor. - unfold_replace. assumption. unfold_replace. assumption. - unfold_replace. eassumption. apply valueToPos_posToValue. - split. lia. - eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. - unfold_replace. - econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. - simpl. unfold find_assocmap. unfold AssocMapExt.get_default. - rewrite H. trivial. - - econstructor. simpl. auto. auto. - - eapply transl_list_correct. - intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. - apply Maps.PTree.elements_keys_norepet. eassumption. - 2: { apply valueToPos_inj. apply unsigned_posToValue_le. - eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. - apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. - destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. trivial. - } - apply Maps.PTree.elements_correct. eassumption. eassumption. - - econstructor. econstructor. - - eapply transl_list_correct. - intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. - auto. apply Maps.PTree.elements_keys_norepet. eassumption. - 2: { apply valueToPos_inj. apply unsigned_posToValue_le. - eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. - apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. - destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. trivial. - } - apply Maps.PTree.elements_correct. eassumption. eassumption. - econstructor. econstructor. - apply mis_stepp_decl. simplify. unfold_replace. simplify. - econstructor. econstructor. econstructor. econstructor. - econstructor. - apply ram_exec_match. eauto. - apply mis_stepp_negedge_decl. simplify. auto. auto. - rewrite_eq. eauto. auto. - rewrite valueToPos_posToValue. econstructor. auto. - simplify; lia. - - inv H7. econstructor; split. apply Smallstep.plus_one. econstructor. - unfold_replace. assumption. unfold_replace. assumption. - unfold_replace. eassumption. apply valueToPos_posToValue. - split. lia. - eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. - unfold_replace. - econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. - simpl. unfold find_assocmap. unfold AssocMapExt.get_default. - rewrite H. trivial. - - econstructor. simpl. auto. auto. - - eapply transl_list_correct. - intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. - apply Maps.PTree.elements_keys_norepet. eassumption. - 2: { apply valueToPos_inj. apply unsigned_posToValue_le. - eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. - apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. - destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. trivial. - } - apply Maps.PTree.elements_correct. eassumption. eassumption. - - econstructor. econstructor. - - eapply transl_list_correct. - intros. split. lia. pose proof (HTL.mod_wf m) as HP. - destruct HP as [_ HP]; auto. - apply Maps.PTree.elements_keys_norepet. eassumption. - 2: { apply valueToPos_inj. apply unsigned_posToValue_le. - eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. - apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. - destruct HP as [HP _]. - split. lia. apply HP. eassumption. eassumption. trivial. - } - apply Maps.PTree.elements_correct. eassumption. eassumption. - - apply mis_stepp_decl. simplify. - unfold_replace. - repeat econstructor. apply mis_stepp_negedge_decl. trivial. trivial. - simpl. unfold_replace. eassumption. auto. simplify. - rewrite valueToPos_posToValue. constructor; eassumption. simplify; lia. - - econstructor; split. apply Smallstep.plus_one. apply step_finish. - rewrite_eq. assumption. - rewrite_eq. eassumption. - econstructor; auto. - - econstructor; split. apply Smallstep.plus_one. apply step_finish. - unfold transl_module. rewrite Heqo. simplify. - assumption. unfold_replace. eassumption. - constructor; assumption. - - econstructor; split. apply Smallstep.plus_one. constructor. - repeat rewrite_eq. constructor. constructor. - - econstructor; split. apply Smallstep.plus_one. constructor. - repeat rewrite_eq. constructor. constructor. - - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. - repeat rewrite_eq. apply match_state. assumption. - - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. - repeat rewrite_eq. apply match_state. assumption. - Qed. - Hint Resolve transl_step_correct : verilogproof. - - Lemma transl_initial_states : - forall s1 : Smallstep.state (HTL.semantics prog), - Smallstep.initial_state (HTL.semantics prog) s1 -> - exists s2 : Smallstep.state (Verilog.semantics tprog), - Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2. - Proof. - induction 1. - econstructor; split. econstructor. - apply (Genv.init_mem_transf TRANSL); eauto. - rewrite symbols_preserved. - replace (AST.prog_main tprog) with (AST.prog_main prog); eauto. - symmetry; eapply Linking.match_program_main; eauto. - exploit function_ptr_translated; eauto. intros [tf [A B]]. - inv B. eauto. - constructor. - Qed. - Hint Resolve transl_initial_states : verilogproof. - - Lemma transl_final_states : - forall (s1 : Smallstep.state (HTL.semantics prog)) - (s2 : Smallstep.state (Verilog.semantics tprog)) - (r : Integers.Int.int), - match_states s1 s2 -> - Smallstep.final_state (HTL.semantics prog) s1 r -> - Smallstep.final_state (Verilog.semantics tprog) s2 r. - Proof. - intros. inv H0. inv H. inv H3. constructor. reflexivity. - Qed. - Hint Resolve transl_final_states : verilogproof. +(* Lemma function_ptr_translated: *) +(* forall (b: Values.block) (f: HTL.fundef), *) +(* Genv.find_funct_ptr ge b = Some f -> *) +(* exists tf, *) +(* Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf. *) +(* Proof. *) +(* intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. *) +(* intros (cu & tf & P & Q & R); exists tf; auto. *) +(* Qed. *) +(* Hint Resolve function_ptr_translated : verilogproof. *) + +(* Lemma functions_translated: *) +(* forall (v: Values.val) (f: HTL.fundef), *) +(* Genv.find_funct ge v = Some f -> *) +(* exists tf, *) +(* Genv.find_funct tge v = Some tf /\ transl_fundef f = tf. *) +(* Proof. *) +(* intros. exploit (Genv.find_funct_match TRANSL); eauto. *) +(* intros (cu & tf & P & Q & R); exists tf; auto. *) +(* Qed. *) +(* Hint Resolve functions_translated : verilogproof. *) + +(* Lemma senv_preserved: *) +(* Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). *) +(* Proof. *) +(* intros. eapply (Genv.senv_match TRANSL). *) +(* Qed. *) +(* Hint Resolve senv_preserved : verilogproof. *) + +(* Theorem transl_step_correct : *) +(* forall (S1 : HTL.state) t S2, *) +(* HTL.step ge S1 t S2 -> *) +(* forall (R1 : state), *) +(* match_states S1 R1 -> *) +(* exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. *) +(* Proof. *) +(* induction 1; intros R1 MSTATE; inv MSTATE. *) +(* - econstructor; split. apply Smallstep.plus_one. econstructor. *) +(* assumption. assumption. eassumption. apply valueToPos_posToValue. *) +(* split. lia. *) +(* eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. *) +(* split. lia. apply HP. eassumption. eassumption. *) +(* econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. *) +(* simpl. unfold find_assocmap. unfold AssocMapExt.get_default. *) +(* rewrite H. trivial. *) + +(* econstructor. simpl. auto. auto. *) + +(* eapply transl_ctrl_correct. *) +(* intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. *) +(* apply Maps.PTree.elements_keys_norepet. eassumption. *) +(* 2: { apply valueToPos_inj. apply unsigned_posToValue_le. *) +(* eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. *) +(* split. lia. apply HP. eassumption. eassumption. *) +(* apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. *) +(* destruct HP as [HP _]. *) +(* split. lia. apply HP. eassumption. eassumption. trivial. *) +(* } *) +(* apply Maps.PTree.elements_correct. eassumption. eassumption. *) + +(* econstructor. econstructor. *) + +(* { admit. *) +(* (* *) *) +(* (* eapply transl_list_correct. *) *) +(* (* intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. *) *) +(* (* apply Maps.PTree.elements_keys_norepet. eassumption. *) *) +(* (* 2: { apply valueToPos_inj. apply unsigned_posToValue_le. *) *) +(* (* eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. *) *) +(* (* split. lia. apply HP. eassumption. eassumption. *) *) +(* (* apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. *) *) +(* (* destruct HP as [HP _]. *) *) +(* (* split. lia. apply HP. eassumption. eassumption. trivial. *) *) +(* (* } *) *) +(* (* apply Maps.PTree.elements_correct. eassumption. eassumption. *) *) +(* (* *) *) +(* } *) + +(* apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. *) +(* rewrite valueToPos_posToValue. constructor; assumption. lia. *) +(* - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. *) +(* constructor; assumption. *) +(* - econstructor; split. apply Smallstep.plus_one. constructor. *) + +(* constructor. constructor. *) +(* - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. *) + +(* apply match_state. assumption. *) +(* Admitted. *) +(* Hint Resolve transl_step_correct : verilogproof. *) + +(* Lemma transl_initial_states : *) +(* forall s1 : Smallstep.state (HTL.semantics prog), *) +(* Smallstep.initial_state (HTL.semantics prog) s1 -> *) +(* exists s2 : Smallstep.state (Verilog.semantics tprog), *) +(* Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2. *) +(* Proof. *) +(* induction 1. *) +(* econstructor; split. econstructor. *) +(* apply (Genv.init_mem_transf TRANSL); eauto. *) +(* rewrite symbols_preserved. *) +(* replace (AST.prog_main tprog) with (AST.prog_main prog); eauto. *) +(* symmetry; eapply Linking.match_program_main; eauto. *) +(* exploit function_ptr_translated; eauto. intros [tf [A B]]. *) +(* inv B. eauto. *) +(* constructor. *) +(* Qed. *) +(* Hint Resolve transl_initial_states : verilogproof. *) + +(* Lemma transl_final_states : *) +(* forall (s1 : Smallstep.state (HTL.semantics prog)) *) +(* (s2 : Smallstep.state (Verilog.semantics tprog)) *) +(* (r : Integers.Int.int), *) +(* match_states s1 s2 -> *) +(* Smallstep.final_state (HTL.semantics prog) s1 r -> *) +(* Smallstep.final_state (Verilog.semantics tprog) s2 r. *) +(* Proof. *) +(* intros. inv H0. inv H. inv H3. constructor. reflexivity. *) +(* Qed. *) +(* Hint Resolve transl_final_states : verilogproof. *) Theorem transf_program_correct: forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). Proof. - eapply Smallstep.forward_simulation_plus; eauto with verilogproof. - apply senv_preserved. - Qed. + (* eapply Smallstep.forward_simulation_plus; eauto with verilogproof. *) + (* apply senv_preserved. *) + admit. + Admitted. End CORRECTNESS. |