From c962467b9ab483beb17a4c264ee30242cdbafb7d Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 3 May 2021 12:08:04 +0100 Subject: Use ltac:() instead of Program in HTLgen Program rewrites match statements, making proofs much harder. --- src/hls/HTLgen.v | 256 +++++++++++++++++++++++++------------------------------ 1 file changed, 116 insertions(+), 140 deletions(-) (limited to 'src/hls/HTLgen.v') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 7ab14bd..ea6c545 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -136,62 +136,72 @@ Proof. intros. case (s.(st_controllogic)!n); tauto. Defined. -Program Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := +(** Used for discharging the st_incr proof in simple operations *) +Ltac htl_st_tac := constructor; intros; simpl; auto with htlh. + +(** Used for discharging the st_incr proof in operations that add instructions. + Assumes that check_empty_node_(datapath|controllogic) has been used and matched + on. *) +Ltac add_instr_st_tac := + htl_st_tac; + match goal with + | [ STM : (st_datapath ?s) ! ?n = None, TRANS : (st_controllogic ?s) ! ?n = None, n0 : positive |- _] => + destruct (peq n n0) + end; + subst; auto with htlh. + + +Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := fun s => 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)) _. -Next Obligation. auto with htlh. Defined. - -Program Definition create_reg (i : option io) (sz : nat) : mon reg := + (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:(htl_st_tac). + +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_externctrl s) - (st_datapath s) - (st_controllogic s)) _. -Next Obligation. constructor; simpl; auto with htlh. Defined. - -Program Definition map_externctrl (othermod : ident) (ctrl : controlsignal) : mon reg := + 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_externctrl s) + (st_datapath s) + (st_controllogic s)) ltac:(htl_st_tac). + +Definition map_externctrl (othermod : ident) (ctrl : controlsignal) : mon reg := do r <- create_reg None (controlsignal_sz ctrl); fun s => OK r (mkstate - s.(st_st) - (st_freshreg s) - (st_freshstate s) - (st_scldecls s) - (st_arrdecls s) - (AssocMap.set r (othermod, ctrl) (st_externctrl s)) - (st_datapath s) - (st_controllogic s)) _. -Next Obligation. constructor; simpl; auto with htlh. Defined. - -Program Definition create_state : mon node := + s.(st_st) + (st_freshreg s) + (st_freshstate s) + (st_scldecls s) + (st_arrdecls s) + (AssocMap.set r (othermod, ctrl) (st_externctrl s)) + (st_datapath s) + (st_controllogic s)) ltac:(htl_st_tac). + +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_externctrl s) - (st_datapath s) - (st_controllogic s)) _. -Next Obligation. constructor; simpl; eauto with htlh. Defined. - -Program 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 + OK r (mkstate + s.(st_st) + (st_freshreg s) + (Pos.succ (st_freshstate s)) + (st_scldecls s) + (st_arrdecls s) + (st_externctrl s) + (st_datapath s) + (st_controllogic s)) ltac:(htl_st_tac). + +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) @@ -199,20 +209,14 @@ Program Definition add_instr (n : node) (n' : node) (st : datapath_stmnt) : mon 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))) _ - | _, _ => Error (Errors.msg "HTL.add_instr") - end. -Next Obligation. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Defined. - -Program 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 + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) ltac:(add_instr_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) @@ -220,20 +224,14 @@ Program Definition add_instr_wait (wait_reg : reg) (n : node) (n' : node) (st : s.(st_arrdecls) (st_externctrl s) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n (state_wait (st_st s) wait_reg n') s.(st_controllogic))) _ - | _, _ => Error (Errors.msg "HTL.add_instr_wait") - end. -Next Obligation. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Defined. - -Program 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 + (AssocMap.set n (state_wait (st_st s) wait_reg n') s.(st_controllogic))) ltac:(add_instr_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) @@ -241,21 +239,14 @@ Program Definition add_instr_skip (n : node) (st : datapath_stmnt) : mon unit := s.(st_arrdecls) (st_externctrl s) (AssocMap.set n st s.(st_datapath)) - (AssocMap.set n Vskip s.(st_controllogic))) - _ - | _, _ => Error (Errors.msg "HTL.add_instr") - end. -Next Obligation. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Defined. - -Program 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 + (AssocMap.set n Vskip s.(st_controllogic))) ltac:(add_instr_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) @@ -263,15 +254,9 @@ Program Definition add_node_skip (n : node) (st : control_stmnt) : mon unit := s.(st_arrdecls) (st_externctrl s) (AssocMap.set n Vskip s.(st_datapath)) - (AssocMap.set n st s.(st_controllogic))) - _ - | _, _ => Error (Errors.msg "HTL.add_instr") - end. -Next Obligation. - constructor; intros; - try (simpl; destruct (peq n n0); subst); - auto with htlh. -Defined. + (AssocMap.set n st s.(st_controllogic))) ltac:(add_instr_st_tac) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr := match c, args with @@ -405,27 +390,20 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") end. -Program 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 +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 s.(st_st) - (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))) - _ - | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") - end. -Next Obligation. - intros. apply state_incr_intro; simpl; - try (intros; destruct (peq n0 n); subst); - auto with htlh. -Defined. + (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:(add_instr_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 := @@ -550,18 +528,17 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni end end. -Program Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := +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_externctrl s) - (st_datapath s) - (st_controllogic s)) _. -Next Obligation. constructor; simpl; auto with htlh. Defined. + 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:(htl_st_tac). Definition stack_correct (sz : Z) : bool := (0 <=? sz) && (sz OK (renumber_freshreg st) (mk_renumber_state (Pos.succ (renumber_freshreg st)) (PTree.set r (renumber_freshreg st) (renumber_regmap st))) - _. - Next Obligation. unfold st_prop; auto. Defined. + ltac:(auto with htl_renumber). - Program Definition clear_regmap : mon unit := + Definition clear_regmap : mon unit := fun st => OK tt (mk_renumber_state (renumber_freshreg st) (PTree.empty reg)) - _. - Next Obligation. unfold st_prop; auto. Defined. + ltac:(auto with htl_renumber). Definition renumber_reg (r : reg) : mon reg := do st <- get; -- cgit