diff options
| -rw-r--r-- | src/translation/HTLgen.v | 19 | ||||
| -rw-r--r-- | src/translation/HTLgenproof.v | 256 | ||||
| -rw-r--r-- | src/translation/HTLgenspec.v | 18 | ||||
| -rw-r--r-- | src/verilog/HTL.v | 21 | ||||
| -rw-r--r-- | src/verilog/Value.v | 5 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 8 |
6 files changed, 269 insertions, 58 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index a891d6c..c73aaa7 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -335,21 +335,21 @@ 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 => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *) - | Op.Ascaled scale offset, r1::nil => + 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 (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *) + | Mint32, Op.Ascaled scale offset, r1::nil => if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4))))) else error (Errors.msg "Veriloggen: translate_arr_access address misaligned") - | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + | Mint32, 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)) then ret (Vvari stack (Vbinop Vadd (boplitz Vadd r1 (offset / 4)) (boplitz Vmul r2 (scale / 4)))) else error (Errors.msg "Veriloggen: translate_arr_access address misaligned") - | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + | Mint32, 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 "Veriloggen: eff_addressing misaligned stack offset") - | _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing") + | _, _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing") end. Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := @@ -421,9 +421,9 @@ Lemma create_arr_state_incr: (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) @@ -436,7 +436,7 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon reg := Definition transf_module (f: function) : mon module := 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; @@ -450,6 +450,7 @@ Definition transf_module (f: function) : mon module := f.(fn_entrypoint) current_state.(st_st) stack + stack_len fin rtrn start diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 4b7f268..773497b 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -42,44 +42,45 @@ 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 := -| match_stacks_nil : - match_stacks nil nil -| match_stacks_cons : - forall cs lr r f sp pc rs m assoc - (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) -> +Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : + AssocMap.t (list value) -> Prop := +| match_arr : forall asa stack, + m.(HTL.mod_stk_len) = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> 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 + 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 ptr))) - valToValue)) -> - match_arrs m f mem asa. + (nth (Z.to_nat ptr / 4) stack (ZToValue 32 0))) -> + match_arrs m f sp mem asa. + +Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop := +| match_stacks_nil : + match_stacks mem nil nil +| match_stacks_cons : + forall cs lr r f sp pc rs m asr asa + (TF : tr_module f m) + (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). Inductive match_states : RTL.state -> HTL.state -> Prop := | match_state : forall asa asr sf f 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), 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), @@ -390,8 +391,176 @@ Section CORRECTNESS. (* assumption. *) admit. - - admit. - - admit. + Ltac invert x := inversion x; subst; clear x. + + Ltac clear_obvious := + repeat match goal with + | [ H : ex _ |- _ ] => invert H + | [ H : Some _ = Some _ |- _ ] => invert H + end. + + Ltac simplify := simpl in *; clear_obvious; simpl in *; try discriminate. + + 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 Nat.div. + + - destruct c, chunk, addr, args; simplify; rt; simplify. + + + admit. (* FIXME: Alignment *) + + admit. + + admit. + + + invert MARR. simplify. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + rewrite ARCHI in H0. simplify. + + (* Out of bounds reads are undefined behaviour. *) + assert (forall ptr v, f.(RTL.fn_stacksize) <= ptr -> + Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr)) = Some v -> + v = Values.Vundef) as INVALID_READ by admit. + + (* Case split on whether read is out of bounds. *) + destruct (RTL.fn_stacksize f <=? Integers.Ptrofs.unsigned i0) eqn:BOUND. + * assert (RTL.fn_stacksize f <= Integers.Ptrofs.unsigned i0) as OUT_OF_BOUNDS. { + apply Zle_bool_imp_le. assumption. + } + eapply INVALID_READ in OUT_OF_BOUNDS. + 2: { rewrite Integers.Ptrofs.repr_unsigned. eassumption. } + + 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. rewrite H3. + reflexivity. + + simplify. unfold_merge. apply AssocMap.gss. + + simplify. rewrite assumption_32bit. + constructor. + + unfold_merge. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + + apply regs_lessdef_add_match. + rewrite OUT_OF_BOUNDS. + constructor. assumption. + + assumption. + + unfold state_st_wf. inversion 1. simplify. + unfold_merge. apply AssocMap.gss. + + assumption. + + econstructor; simplify; try reflexivity; eassumption. + + * assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as IN_BOUNDS. { + rewrite Z.leb_antisym in BOUND. + rewrite negb_false_iff in BOUND. + apply Zlt_is_lt_bool. assumption. + } + + 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. rewrite H3. + reflexivity. + + simplify. unfold_merge. apply AssocMap.gss. + + simplify. rewrite assumption_32bit. + constructor. + + unfold_merge. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + + apply regs_lessdef_add_match. + + assert (exists ptr, (Z.to_nat ptr / 4)%nat = (valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned i0 / 4)))) + by admit. + simplify. rewrite <- H5. + specialize (H4 x). + assert (0 <= x < Z.of_nat (Z.to_nat (RTL.fn_stacksize f / 4))) by admit. + apply H4 in H0. + invert H0. + assert (Integers.Ptrofs.repr x = i0) by admit. + rewrite H0 in H6. + rewrite H1 in H6. + invert H6. + assumption. + + assert (Integers.Ptrofs.repr x = i0) by admit. + rewrite H0 in H7. + rewrite H1 in H7. + discriminate. + + assumption. + + assumption. + + unfold state_st_wf. inversion 1. simplify. + unfold_merge. apply AssocMap.gss. + + assumption. + + econstructor; simplify; try reflexivity; eassumption. + + - 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. + eapply Verilog.stmnt_runp_Vblock_arr. simplify. + econstructor. econstructor. econstructor. simplify. + + reflexivity. + + unfold_merge. apply AssocMap.gss. + + simplify. rewrite assumption_32bit. econstructor. + + unfold_merge. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + assumption. + + unfold state_st_wf. inversion 1. simplify. + unfold_merge. apply AssocMap.gss. + + admit. + + econstructor; simplify; try reflexivity. + admit. + - eexists. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. @@ -453,8 +622,7 @@ Section CORRECTNESS. econstructor; simpl; trivial. constructor. - constructor. - constructor. + constructor. constructor. unfold_merge. simpl. rewrite AssocMap.gso. @@ -470,7 +638,8 @@ Section CORRECTNESS. apply AssocMap.gss. rewrite Events.E0_left. reflexivity. constructor. - assumption. + + admit. constructor. - econstructor. split. @@ -499,21 +668,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 +711,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 7909688..57d2d87 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -184,14 +184,15 @@ 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) -> 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 +433,12 @@ Proof. Qed. Hint Resolve iter_expand_instr_spec : htlspec. +Lemma create_arr_inv : forall x y z a b c d, + create_arr 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. @@ -445,6 +452,11 @@ Proof. unfold transf_module in *. 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. diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index c07d672..c509248 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -46,6 +46,7 @@ Record module: Type := mod_entrypoint : node; mod_st : reg; mod_stk : reg; + mod_stk_len : nat; mod_finish : reg; mod_return : reg; mod_start : reg; @@ -65,6 +66,14 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := | _, _ => empty_assocmap end. +Fixpoint zeroes' (acc : list value) (n : nat) : list value := + match n with + | O => acc + | S n => zeroes' ((NToValue 32 0)::acc) n + end. + +Definition zeroes : nat -> list value := zeroes' nil. + (** * Operational Semantics *) Definition genv := Globalenvs.Genv.t fundef unit. @@ -74,7 +83,8 @@ Inductive stackframe : Type := forall (res : reg) (m : module) (pc : node) - (assoc : assocmap), + (reg_assoc : assocmap) + (arr_assoc : AssocMap.t (list value)), stackframe. Inductive state : Type := @@ -130,13 +140,12 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (State res m m.(mod_entrypoint) (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint)) (init_regs args m.(mod_params))) - (AssocMap.empty (list value))) + (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (list value)))) | step_return : - forall g m asr i r sf pc mst, + forall g m asr asa i r sf pc mst, mst = mod_st m -> - step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 - (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) - (AssocMap.empty (list value))). + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa). Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := diff --git a/src/verilog/Value.v b/src/verilog/Value.v index d527b15..b1ee353 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -296,6 +296,11 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. +Inductive opt_val_value_lessdef: option val -> value -> Prop := +| opt_lessdef_some: + forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' +| opt_lessdef_none: forall v, opt_val_value_lessdef None v. + Lemma valueToZ_ZToValue : forall n z, (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index b4b2f00..8b83d49 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -56,10 +56,10 @@ Definition merge_associations {A : Type} (assoc : associations A) := mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking)) (AssocMap.empty A). -Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := +Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : value := match a ! r with - | None => None - | Some arr => nth_error arr i + | None => natToValue 32 0 + | Some arr => nth i arr (natToValue 32 0) end. Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A := @@ -324,7 +324,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop | erun_Vvari : forall fext reg stack v iexp i r, expr_runp fext reg stack iexp i -> - arr_assocmap_lookup stack r (valueToNat i) = Some v -> + arr_assocmap_lookup stack r (valueToNat i) = v -> expr_runp fext reg stack (Vvari r iexp) v | erun_Vinputvar : forall fext reg stack r v, |