diff options
Diffstat (limited to 'src/translation')
-rw-r--r-- | src/translation/HTLgen.v | 81 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 525 | ||||
-rw-r--r-- | src/translation/HTLgenspec.v | 27 | ||||
-rw-r--r-- | src/translation/Veriloggen.v | 5 |
4 files changed, 552 insertions, 86 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index f109a8e..44b2937 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -17,7 +17,7 @@ *) From compcert Require Import Maps. -From compcert Require Errors Globalenvs. +From compcert Require Errors Globalenvs Integers. From compcert Require Import AST RTL. From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad. @@ -131,7 +131,7 @@ Lemma declare_reg_state_incr : s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)). @@ -142,7 +142,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)) @@ -280,19 +280,28 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") end. +Definition check_address_parameter (p : Z) : bool := + Z.eqb (Z.modulo p 4) 0 + && Z.leb Integers.Ptrofs.min_signed p + && Z.leb p Integers.Ptrofs.min_signed. + Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := - match a, args with + match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off) - | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off)) | Op.Ascaled scale offset, r1::nil => - ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) - | Op.Aindexed2scaled scale offset, r1::r2::nil => - ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - (* Stack arrays/referenced variables *) + if (check_address_parameter scale) && (check_address_parameter offset) + then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter scale) && (check_address_parameter offset) + then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) - ret (Vlit (ZToValue 32 a)) - | _, _ => error (Errors.msg "Htlgen: eff_addressing instruction not implemented: other") + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter a) + then ret (Vlit (ZToValue 32 a)) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. (** Translate an instruction to a statement. FIX mulhs mulhu *) @@ -374,24 +383,25 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) (args : list reg) (stack : reg) : mon expr := - match addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) - | Op.Aindexed off, r1::nil => (* FIXME: Cannot guarantee alignment *) + match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Mint32, Op.Aindexed off, r1::nil => ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4))))) - | Op.Ascaled scale offset, r1::nil => - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + | Mint32, Op.Ascaled scale offset, r1::nil => + if (check_address_parameter scale) && (check_address_parameter offset) then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4))))) else error (Errors.msg "Htlgen: translate_arr_access address misaligned") - | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter scale) && (check_address_parameter offset) then ret (Vvari stack (Vbinop Vadd (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (offset / 4)))) (boplitz Vmul r2 (scale / 4)))) else error (Errors.msg "Htlgen: translate_arr_access address misaligned") - | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) - if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) - else error (Errors.msg "Htlgen: eff_addressing misaligned stack offset") - | _, _ => error (Errors.msg "Htlgen: translate_arr_access unsupported addressing") + | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter a) + then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) + else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset") + | _, _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing") end. Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := @@ -418,10 +428,10 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Iload mem addr args dst n' => do src <- translate_arr_access mem addr args stack; do _ <- declare_reg None dst 32; - add_instr n n' (block dst src) + add_instr n n' (nonblock dst src) | Istore mem addr args src n' => do dst <- translate_arr_access mem addr args stack; - add_instr n n' (Vblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") @@ -447,7 +457,7 @@ Lemma create_reg_state_incr: s.(st_st) (Pos.succ (st_freshreg s)) (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) s.(st_arrdecls) (st_datapath s) (st_controllogic s)). @@ -459,7 +469,7 @@ Definition create_reg (i : option io) (sz : nat) : mon reg := s.(st_st) (Pos.succ r) (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, Scalar sz) s.(st_scldecls)) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) (st_arrdecls s) (st_datapath s) (st_controllogic s)) @@ -472,27 +482,28 @@ Lemma create_arr_state_incr: (Pos.succ (st_freshreg s)) (st_freshstate s) s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls)) + (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 := +Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := fun s => let r := s.(st_freshreg) in - OK r (mkstate + OK (r, ln) (mkstate s.(st_st) (Pos.succ r) (st_freshstate s) s.(st_scldecls) - (AssocMap.set s.(st_freshreg) (i, Array sz ln) s.(st_arrdecls)) + (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). Definition transf_module (f: function) : mon module := + if (Z.eq_dec (Z.modulo f.(fn_stacksize) 4) 0) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; - do stack <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); + 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; @@ -506,20 +517,22 @@ Definition transf_module (f: function) : mon module := f.(fn_entrypoint) current_state.(st_st) stack + stack_len fin rtrn start rst clk current_state.(st_scldecls) - current_state.(st_arrdecls)). + current_state.(st_arrdecls)) + else error (Errors.msg "Stack size misalignment."). Definition max_state (f: function) : state := let st := Pos.succ (max_reg_function f) in mkstate st (Pos.succ st) (Pos.succ (max_pc_function f)) - (AssocMap.set st (None, Scalar 32) (st_scldecls (init_state st))) + (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) (st_arrdecls (init_state st)) (st_datapath (init_state st)) (st_controllogic (init_state st)). diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 9786d23..60f0d73 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -18,9 +18,11 @@ From compcert Require RTL Registers AST Integers. From compcert Require Import Globalenvs Memory. -From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap. +From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array. From coqup Require HTL Verilog. +Require Import Lia. + Local Open Scope assocmap. Hint Resolve Smallstep.forward_simulation_plus : htlproof. @@ -42,44 +44,68 @@ Definition state_st_wf (m : HTL.module) (s : HTL.state) := asa!(m.(HTL.mod_st)) = Some (posToValue 32 st). Hint Unfold state_st_wf : htlproof. -Inductive match_stacks : list RTL.stackframe -> list HTL.stackframe -> Prop := +Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : + Verilog.assocmap_arr -> Prop := +| match_arr : forall asa stack, + asa ! (m.(HTL.mod_stk)) = Some stack /\ + stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\ + (forall ptr, + 0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) -> + opt_val_value_lessdef (Mem.loadv AST.Mint32 mem + (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))) + (Option.default (NToValue 32 0) + (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> + match_arrs m f sp mem asa. + +Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop := | match_stacks_nil : - match_stacks nil nil + match_stacks mem nil nil | match_stacks_cons : - forall cs lr r f sp pc rs m assoc + forall cs lr r f sp pc rs m asr asa (TF : tr_module f m) - (ST: match_stacks cs lr) - (MA: match_assocmaps f rs assoc), - match_stacks (RTL.Stackframe r f sp pc rs :: cs) - (HTL.Stackframe r m pc assoc :: lr). - -Inductive match_arrs (m : HTL.module) : RTL.function -> mem -> AssocMap.t (list value) -> Prop := -| match_arr : forall mem asa stack sp f sz, - sz = f.(RTL.fn_stacksize) -> - asa ! (m.(HTL.mod_stk)) = Some stack -> - (forall ptr, - 0 <= ptr < sz -> - nth_error stack (Z.to_nat ptr) = - (Coquplib.Option.bind (Mem.loadv AST.Mint32 mem - (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr))) - valToValue)) -> - match_arrs m f mem asa. + (ST: match_stacks mem cs lr) + (MA: match_assocmaps f rs asr) + (MARR : match_arrs m f sp mem asa), + match_stacks mem (RTL.Stackframe r f sp pc rs :: cs) + (HTL.Stackframe r m pc asr asa :: lr). + +Definition stack_based (v : Values.val) (sp : Values.block) : Prop := + match v with + | Values.Vptr sp' off => sp' = sp + | _ => 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. + +Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z) + (sp : Values.val) : Prop := + forall ptr, + 0 <= ptr < (stack_length / 4) -> + stack_based (Option.default + Values.Vundef + (Mem.loadv AST.Mint32 m + (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))) + spb. Inductive match_states : RTL.state -> HTL.state -> Prop := -| match_state : forall asa asr sf f sp rs mem m st res +| match_state : forall asa asr sf f sp sp' rs mem m st res (MASSOC : match_assocmaps f rs asr) (TF : tr_module f m) (WF : state_st_wf m (HTL.State res m st asr asa)) - (MS : match_stacks sf res) - (MA : match_arrs m f mem asa), + (MS : match_stacks 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), match_states (RTL.State sf f sp st rs mem) (HTL.State res m st asr asa) | match_returnstate : forall - v v' stack m res - (MS : match_stacks stack res), + v v' stack mem res + (MS : match_stacks mem stack res), val_value_lessdef v v' -> - match_states (RTL.Returnstate stack v m) (HTL.Returnstate res v') + match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v') | match_initial_call : forall f m m0 (TF : tr_module f m), @@ -129,6 +155,33 @@ Proof. Qed. Hint Resolve regs_lessdef_add_match : htlproof. +Lemma list_combine_none : + forall n l, + length l = n -> + list_combine Verilog.merge_cell (list_repeat None n) l = l. +Proof. + induction n; intros; simplify. + - symmetry. apply length_zero_iff_nil. auto. + - destruct l; simplify. + rewrite list_repeat_cons. + simplify. f_equal. + eauto. +Qed. + +Lemma combine_none : + forall n a, + a.(arr_length) = n -> + arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. +Proof. + intros. + unfold combine. + simplify. + + rewrite <- (arr_wf a) in H. + apply list_combine_none. + assumption. +Qed. + (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) Lemma assumption_32bit : forall v, @@ -297,21 +350,51 @@ Section CORRECTNESS. eapply HTL.step_module; eauto. (* processing of state *) econstructor. - simpl. trivial. + simplify. econstructor. econstructor. econstructor. + simplify. - (* prove stval *) - unfold merge_assocmap. - unfold_merge. simpl. apply AssocMap.gss. + unfold Verilog.merge_regs. + unfold_merge. apply AssocMap.gss. (* prove match_state *) rewrite assumption_32bit. - constructor; auto. + econstructor; simplify; eauto. + + unfold Verilog.merge_regs. unfold_merge. simpl. apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. + unfold Verilog.merge_regs. unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss. + + (* prove match_arrs *) + invert MARR. simplify. + unfold HTL.empty_stack. simplify. unfold Verilog.merge_arrs. + econstructor. + simplify. repeat split. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H1. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len; auto. + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. + + assumption. + - (* Iop *) (* destruct v eqn:?; *) (* try ( *) @@ -390,8 +473,349 @@ Section CORRECTNESS. (* assumption. *) admit. - - admit. - - admit. + Ltac rt := + repeat match goal with + | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate + | [ _ : context[if (?x && ?y) then _ else _] |- _ ] => + let EQ1 := fresh "EQ" in + let EQ2 := fresh "EQ" in + destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in * + | [ _ : context[if ?x then _ else _] |- _ ] => + let EQ := fresh "EQ" in + destruct x eqn:EQ; simpl in * + | [ H : ret _ _ = _ |- _ ] => invert H + | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x + end. + + Opaque Z.mul. + + - (* FIXME: Should be able to use the spec to avoid destructing here. *) + destruct c, chunk, addr, args; simplify; rt; simplify. + + + admit. (* FIXME: Alignment *) + + + (* FIXME: Why is this degenerate? Should we support this mode? *) + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; discriminate. + + + invert MARR. simplify. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + + unfold reg_stack_based_pointers in RSBP. + pose proof (RSBP r0) as RSBPr0. + pose proof (RSBP r1) as RSBPr1. + + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; + destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify. + + rewrite ARCHI in H1. simplify. + subst. + + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. simplify. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ1]). (* FIXME: These will be shelved and cause sadness. *) + eapply Verilog.erun_Vbinop with (EQ := ?[EQ2]). + eapply Verilog.erun_Vbinop with (EQ := ?[EQ3]). + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + eapply Verilog.erun_Vbinop with (EQ := ?[EQ4]). + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. + econstructor. (* FIXME: Oh dear. *) + + unfold Verilog.arr_assocmap_lookup. simplify. setoid_rewrite H3. + f_equal. + + simplify. unfold Verilog.merge_regs. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + simplify. rewrite assumption_32bit. + econstructor; simplify; eauto. + + unfold Verilog.merge_regs. unfold_merge. + apply regs_lessdef_add_match. + + pose proof H1. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) by reflexivity. + rewrite H4 in H5. + setoid_rewrite Integers.Ptrofs.add_zero_l in H5. + + specialize (H5 (uvalueToZ + (vplus (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) (ZToValue 32 (z0 / 4)) ?EQ2) + (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) ?EQ1))). + + assert (0 <= uvalueToZ + (vplus (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) (ZToValue 32 (z0 / 4)) ?EQ2) + (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) ?EQ1) < + Z.of_nat (Z.to_nat (RTL.fn_stacksize f / 4))) by admit. + apply H5 in H6. + + invert MASSOC. + pose proof (H7 r0). + pose proof (H7 r1). + assert (HPler0 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + assert (HPler1 : Ple r1 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H8 in HPler0. + apply H10 in HPler1. + invert HPler0; invert HPler1; try congruence. + rewrite EQr0 in H12. + rewrite EQr1 in H13. + + assert ((Integers.Ptrofs.unsigned + (Integers.Ptrofs.add i0 + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) + (Integers.Int.repr z0))))) = + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.repr + (4 * + uvalueToZ + (vplus + (vplus (vdivs asr # r0 (ZToValue 32 4) ?EQ3) + (ZToValue 32 (z0 / 4)) ?EQ2) + (vmul asr # r1 (ZToValue 32 (z / 4)) ?EQ4) + ?EQ1))))) by admit. + + rewrite <- H19 in H6. + rewrite H0 in H6. + invert H6. + assert (forall x, Z.to_nat (uvalueToZ x) = valueToNat x) as VALUE_IDENTITY by admit. + rewrite VALUE_IDENTITY in H21. + assumption. + + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H3. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len. + congruence. + + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. + assumption. + + unfold reg_stack_based_pointers. intros. + destruct (Pos.eq_dec r2 dst); subst. + + rewrite Registers.Regmap.gss. + + unfold arr_stack_based_pointers in ASBP. + specialize (ASBP ((Integers.Ptrofs.unsigned + (Integers.Ptrofs.add i0 + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) + (Integers.Int.repr z0))))) / 4)). + exploit ASBP; auto; intros. + 1: { + split. + - admit. (*apply Z.div_pos; lia.*) + - admit. (* apply Zmult_lt_reg_r with (p := 4); try lia. *) + (* repeat rewrite ZLib.div_mul_undo; lia. *) + } + replace (4 * ((Integers.Ptrofs.unsigned + (Integers.Ptrofs.add i0 + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) + (Integers.Int.repr z0))))) / 4)) with (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add i0 + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul i1 (Integers.Int.repr z)) + (Integers.Int.repr z0))))) in H0. + 2: { + rewrite Z.mul_comm. + admit. + (* rewrite ZLib.div_mul_undo; lia. *) + } + rewrite Integers.Ptrofs.repr_unsigned in H0. + simplify. + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) by reflexivity. + rewrite H4 in H0. + setoid_rewrite Integers.Ptrofs.add_zero_l in H0. + rewrite H1 in H0. + simplify. + assumption. + + rewrite Registers.Regmap.gso; auto. + + + invert MARR. simplify. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + rewrite ARCHI in H0. simplify. + + (** Here we are assuming that any stack read will be within the bounds + of the activation record. *) + assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit. + assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. econstructor. simplify. + + unfold Verilog.arr_assocmap_lookup. setoid_rewrite H3. + f_equal. + + simplify. unfold Verilog.merge_regs. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + simplify. rewrite assumption_32bit. + econstructor; simplify; eauto. + + unfold Verilog.merge_regs. unfold_merge. + apply regs_lessdef_add_match. + + (** Equality proof *) + (* FIXME: 32-bit issue. *) + assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) as VALUE_IDENTITY by admit. + rewrite VALUE_IDENTITY. + specialize (H5 (Integers.Ptrofs.unsigned i0 / 4)). + rewrite Z2Nat.id in H5; try lia. + exploit H5; auto; intros. + 1: { + split. + - apply Z.div_pos; lia. + - apply Zmult_lt_reg_r with (p := 4); try lia. + repeat rewrite ZLib.div_mul_undo; lia. + } + 2: { + assert (0 < RTL.fn_stacksize f) by lia. + apply Z.div_pos; lia. + } + replace (4 * (Integers.Ptrofs.unsigned i0 / 4)) with (Integers.Ptrofs.unsigned i0) in H0. + 2: { + rewrite Z.mul_comm. + rewrite ZLib.div_mul_undo; lia. + } + rewrite Integers.Ptrofs.repr_unsigned in H0. + rewrite H1 in H0. + invert H0. assumption. + + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + unfold state_st_wf. inversion 1. simplify. + unfold Verilog.merge_regs. + unfold_merge. rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + econstructor. + repeat split; simplify. + unfold HTL.empty_stack. + simplify. + unfold Verilog.merge_arrs. + + rewrite AssocMap.gcombine. + 2: { reflexivity. } + rewrite AssocMap.gss. + unfold Verilog.merge_arr. + setoid_rewrite H3. + reflexivity. + + rewrite combine_length. + unfold arr_repeat. simplify. + rewrite list_repeat_len. + reflexivity. + + unfold arr_repeat. simplify. + rewrite list_repeat_len. + congruence. + + intros. + erewrite array_get_error_equal. + eauto. apply combine_none. + assumption. + + unfold reg_stack_based_pointers. intros. + destruct (Pos.eq_dec r0 dst); subst. + + rewrite Registers.Regmap.gss. + + unfold arr_stack_based_pointers in ASBP. + specialize (ASBP (Integers.Ptrofs.unsigned i0 / 4)). + exploit ASBP; auto; intros. + 1: { + split. + - apply Z.div_pos; lia. + - apply Zmult_lt_reg_r with (p := 4); try lia. + repeat rewrite ZLib.div_mul_undo; lia. + } + replace (4 * (Integers.Ptrofs.unsigned i0 / 4)) with (Integers.Ptrofs.unsigned i0) in H0. + 2: { + rewrite Z.mul_comm. + rewrite ZLib.div_mul_undo; lia. + } + rewrite Integers.Ptrofs.repr_unsigned in H0. + simplify. + rewrite H1 in H0. + simplify. + assumption. + + rewrite Registers.Regmap.gso; auto. + + - destruct c, chunk, addr, args; simplify; rt; simplify. + + admit. + + admit. + + admit. + + (* + eexists. split. *) + (* eapply Smallstep.plus_one. *) + (* eapply HTL.step_module; eauto. *) + (* econstructor. econstructor. econstructor. simplify. *) + + admit. - eexists. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. @@ -453,8 +877,7 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. - constructor. - constructor. + constructor. constructor. unfold_merge. simpl. rewrite AssocMap.gso. @@ -470,7 +893,8 @@ Section CORRECTNESS. apply AssocMap.gss. rewrite Events.E0_left. reflexivity. constructor. - assumption. + + admit. constructor. - econstructor. split. @@ -499,21 +923,38 @@ Section CORRECTNESS. apply AssocMap.gss. rewrite Events.E0_left. trivial. - constructor. assumption. simpl. inversion MASSOC. subst. + constructor. + admit. + + simpl. inversion MASSOC. subst. unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. apply st_greater_than_res. - inversion MSTATE; subst. inversion TF; subst. econstructor. split. apply Smallstep.plus_one. - eapply HTL.step_call. + eapply HTL.step_call. simpl. constructor. apply regs_lessdef_add_greater. apply greater_than_max_func. apply init_reg_assoc_empty. assumption. unfold state_st_wf. intros. inv H1. apply AssocMap.gss. constructor. - admit. + econstructor; simpl. + reflexivity. + rewrite AssocMap.gss. reflexivity. + intros. + destruct (Mem.load AST.Mint32 m' stk + (Integers.Ptrofs.unsigned (Integers.Ptrofs.add + Integers.Ptrofs.zero + (Integers.Ptrofs.repr 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. - inversion MSTATE; subst. inversion MS; subst. econstructor. split. apply Smallstep.plus_one. @@ -525,13 +966,11 @@ Section CORRECTNESS. unfold state_st_wf. intros. inv H. rewrite AssocMap.gso. rewrite AssocMap.gss. trivial. apply st_greater_than_res. - admit. - Unshelve. exact (AssocMap.empty value). exact (AssocMap.empty value). - admit. - admit. + exact (AssocMap.empty value). + exact (AssocMap.empty value). (* exact (ZToValue 32 0). *) (* exact (AssocMap.empty value). *) (* exact (AssocMap.empty value). *) diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 887a696..f600dc4 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -163,11 +163,11 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - | tr_instr_Iload : forall mem addr args s s' i c dst n, 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) (block dst c) (state_goto st n) + 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, 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) (Vblock c (Vvar src)) + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) (state_goto st n). Hint Constructors tr_instr : htlspec. @@ -184,14 +184,16 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk m start rst clk scldecls arrdecls, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls, (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) -> + 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 -> m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk fin rtrn start rst clk scldecls arrdecls) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls) -> tr_module f m. Hint Constructors tr_module : htlspec. @@ -432,6 +434,12 @@ Proof. Admitted. 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. +Proof. + inversion 1. reflexivity. +Qed. + Theorem transl_module_correct : forall f m, transl_module f = Errors.OK m -> tr_module f m. @@ -444,12 +452,17 @@ Proof. inversion s; subst. unfold transf_module in *. - monadInv Heqr. + destruct (Z.eq_dec (RTL.fn_stacksize f mod 4) 0); monadInv Heqr. + + (* TODO: We should be able to fold this into the automation. *) + pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. + rewrite <- STK_LEN. + econstructor; simpl; trivial. intros. inv_incr. assert (EQ3D := EQ3). - destruct x3. + destruct x4. apply collect_declare_datapath_trans in EQ3. apply collect_declare_controllogic_trans in EQ3D. assert (STC: st_controllogic s10 = st_controllogic s3) by congruence. diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index efe3565..2b9974b 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -29,13 +29,13 @@ Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item := match scldecl with - | (r, (io, Scalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' + | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' | nil => nil end. Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item := match arrdecl with - | (r, (io, Array sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' + | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' | nil => nil end. @@ -56,6 +56,7 @@ Definition transl_module (m : HTL.module) : Verilog.module := m.(mod_return) m.(mod_st) m.(mod_stk) + m.(mod_stk_len) m.(mod_params) body m.(mod_entrypoint). |