From 0b480d489a91f0d418523933b5e35288fcec65b1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 3 Jul 2020 12:14:39 +0100 Subject: Updates to Iop proof --- src/translation/HTLgen.v | 2 - src/translation/HTLgenproof.v | 190 ++++++++++++++++++++++-------------------- src/verilog/Value.v | 79 +++++++++++++++++- 3 files changed, 179 insertions(+), 92 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index b32ed9d..a2b77e6 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -353,8 +353,6 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := do tc <- translate_condition c rl; ret (Vternary tc (Vvar r1) (Vvar r2)) | Op.Olea a, _ => translate_eff_addressing a args - | Op.Oleal a, _ => translate_eff_addressing a args (* FIXME: Need to be careful here; large arrays might fail? *) - | Op.Ocast32signed, r::nil => ret (Vvar r) (* FIXME: Don't need to sign extend for now since everything is 32 bit? *) | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") end. diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 07417a7..956c3ed 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -359,22 +359,35 @@ Section CORRECTNESS. Hint Resolve senv_preserved : htlproof. Lemma eval_correct : - forall sp op rs args m v v' e asr asa f s s' i, + 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) -> + (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 -> + (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> translate_instr op args s = OK e s' i -> - val_value_lessdef v v' -> - Verilog.expr_runp f asr asa e v'. - Admitted. + 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. + 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); simplify. + - inv Heql. + assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle. eexists. split; try constructor; eauto. + - eexists. split. constructor. constructor. symmetry. apply valueToInt_intToValue. + - inv Heql. + assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle. + eexists. split. econstructor; eauto. constructor. trivial. + unfold Verilog.unop_run. Lemma eval_cond_correct : forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, - translate_condition cond args s1 = OK c s' i -> - Op.eval_condition - cond - (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) - m = Some b -> - Verilog.expr_runp f asr asa c (boolToValue 32 b). + translate_condition cond args s1 = OK c s' i -> + Op.eval_condition + cond + (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) + m = Some b -> + Verilog.expr_runp f asr asa c (boolToValue 32 b). Admitted. (** The proof of semantic preservation for the translation of instructions @@ -489,84 +502,83 @@ Section CORRECTNESS. 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. Proof. - intros s f sp pc rs m op args res0 pc' v H H0. - - (* Iop *) - (* destruct v eqn:?; *) - (* try ( *) - (* destruct op eqn:?; inversion H21; simpl in H0; repeat (unfold_match H0); *) - (* inversion H0; subst; simpl in *; try (unfold_func H4); try (unfold_func H5); *) - (* try (unfold_func H6); *) - (* try (unfold Op.eval_addressing32 in H6; repeat (unfold_match H6); inversion H6; *) - (* unfold_func H3); *) - - (* inversion Heql; inversion MASSOC; subst; *) - (* assert (HPle : Ple r (RTL.max_reg_function f)) *) - (* by (eapply RTL.max_reg_function_use; eauto; simpl; auto); *) - (* apply H1 in HPle; inversion HPle; *) - (* rewrite H2 in *; discriminate *) - (* ). *) - - (* + econstructor. split. *) - (* apply Smallstep.plus_one. *) - (* eapply HTL.step_module; eauto. *) - (* econstructor; simpl; trivial. *) - (* constructor; trivial. *) - (* econstructor; simpl; eauto. *) - (* eapply eval_correct; eauto. constructor. *) - (* unfold_merge. simpl. *) - (* rewrite AssocMap.gso. *) - (* apply AssocMap.gss. *) - (* apply st_greater_than_res. *) - - (* (* match_states *) *) - (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *) - (* rewrite <- H1. *) - (* constructor; auto. *) - (* unfold_merge. *) - (* apply regs_lessdef_add_match. *) - (* constructor. *) - (* apply regs_lessdef_add_greater. *) - (* apply greater_than_max_func. *) - (* assumption. *) - - (* unfold state_st_wf. intros. inversion H2. subst. *) - (* unfold_merge. *) - (* rewrite AssocMap.gso. *) - (* apply AssocMap.gss. *) - (* apply st_greater_than_res. *) - - (* + econstructor. split. *) - (* apply Smallstep.plus_one. *) - (* eapply HTL.step_module; eauto. *) - (* econstructor; simpl; trivial. *) - (* constructor; trivial. *) - (* econstructor; simpl; eauto. *) - (* eapply eval_correct; eauto. *) - (* constructor. rewrite valueToInt_intToValue. trivial. *) - (* unfold_merge. simpl. *) - (* rewrite AssocMap.gso. *) - (* apply AssocMap.gss. *) - (* apply st_greater_than_res. *) - - (* (* match_states *) *) - (* assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. *) - (* rewrite <- H1. *) - (* constructor. *) - (* unfold_merge. *) - (* apply regs_lessdef_add_match. *) - (* constructor. *) - (* symmetry. apply valueToInt_intToValue. *) - (* apply regs_lessdef_add_greater. *) - (* apply greater_than_max_func. *) - (* assumption. assumption. *) - - (* unfold state_st_wf. intros. inversion H2. subst. *) - (* unfold_merge. *) - (* rewrite AssocMap.gso. *) - (* apply AssocMap.gss. *) - (* apply st_greater_than_res. *) - (* assumption. *) + intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE. + inv_state. + exploit eval_correct; eauto. intros. inversion H1. inversion H2. + econstructor. split. + apply Smallstep.plus_one. + eapply HTL.step_module; eauto. + apply assumption_32bit. + econstructor; simpl; trivial. + constructor; trivial. + econstructor; simpl; eauto. + simpl. econstructor. econstructor. + apply H3. simplify. + + all: big_tac. + + assert (Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + + unfold Ple in H10. lia. + apply regs_lessdef_add_match. assumption. + apply regs_lessdef_add_greater. unfold Plt; lia. assumption. + assert (Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + unfold Ple in H12; lia. + unfold_merge. simpl. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + (*match_states*) + assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. + rewrite <- H1. + constructor; auto. + unfold_merge. + apply regs_lessdef_add_match. + constructor. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + unfold state_st_wf. intros. inversion H2. subst. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + + econstructor. split. + apply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor; simpl; trivial. + constructor; trivial. + econstructor; simpl; eauto. + eapply eval_correct; eauto. + constructor. rewrite valueToInt_intToValue. trivial. + unfold_merge. simpl. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + + match_states + assert (pc' = valueToPos (posToValue 32 pc')). auto using assumption_32bit. + rewrite <- H1. + constructor. + unfold_merge. + apply regs_lessdef_add_match. + constructor. + symmetry. apply valueToInt_intToValue. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. assumption. + + unfold state_st_wf. intros. inversion H2. subst. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. + apply st_greater_than_res. + assumption. Admitted. Hint Resolve transl_iop_correct : htlproof. diff --git a/src/verilog/Value.v b/src/verilog/Value.v index acabcf2..23ce0f7 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -88,9 +88,18 @@ Definition intToValue (i : Integers.int) : value := Definition valueToInt (i : value) : Integers.int := Int.repr (uvalueToZ i). +Definition ptrToValue (i : Integers.ptrofs) : value := + ZToValue Ptrofs.wordsize (Ptrofs.unsigned i). + +Definition valueToPtr (i : value) : Integers.ptrofs := + Ptrofs.repr (uvalueToZ i). + Definition valToValue (v : Values.val) : option value := match v with | Values.Vint i => Some (intToValue i) + | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z + then Some (ptrToValue off) + else None | Values.Vundef => Some (ZToValue 32 0%Z) | _ => None end. @@ -304,7 +313,7 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | val_value_lessdef_ptr: forall b off v', - off = Ptrofs.repr (uvalueToZ v') -> + off = valueToPtr v' -> (Z.modulo (uvalueToZ v') 4) = 0%Z -> val_value_lessdef (Vptr b off) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. @@ -382,6 +391,41 @@ Proof. apply Z.lt_le_pred in H. apply H. Qed. +Lemma valueToPtr_ptrToValue : + forall v, + valueToPtr (ptrToValue v) = v. +Proof. + intros. + unfold valueToPtr, ptrToValue. rewrite uvalueToZ_ZToValue. auto using Ptrofs.repr_unsigned. + split. apply Ptrofs.unsigned_range_2. + assert ((Ptrofs.unsigned v <= Ptrofs.max_unsigned)%Z) by apply Ptrofs.unsigned_range_2. + apply Z.lt_le_pred in H. apply H. +Qed. + +Lemma intToValue_valueToInt : + forall v, + vsize v = 32%nat -> + intToValue (valueToInt v) = v. +Proof. + intros. unfold valueToInt, intToValue. rewrite Int.unsigned_repr_eq. + unfold ZToValue, uvalueToZ. unfold Int.modulus. unfold Int.wordsize. unfold Wordsize_32.wordsize. + pose proof (uwordToZ_bound (vword v)). + rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. + rewrite <- H. rewrite two_power_nat_equiv. apply H0. +Qed. + +Lemma ptrToValue_valueToPtr : + forall v, + vsize v = 32%nat -> + ptrToValue (valueToPtr v) = v. +Proof. + intros. unfold valueToPtr, ptrToValue. rewrite Ptrofs.unsigned_repr_eq. + unfold ZToValue, uvalueToZ. unfold Ptrofs.modulus. unfold Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize. + pose proof (uwordToZ_bound (vword v)). + rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. + rewrite <- H. rewrite two_power_nat_equiv. apply H0. +Qed. + Lemma valToValue_lessdef : forall v v', valToValue v = Some v' -> @@ -391,6 +435,10 @@ Proof. destruct v; try discriminate; constructor. unfold valToValue in H. inversion H. symmetry. apply valueToInt_intToValue. + inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate. + inv H1. symmetry. apply valueToPtr_ptrToValue. + inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. + inv H1. apply Z.eqb_eq. apply Heqb0. Qed. Lemma boolToValue_ValueToBool : @@ -418,6 +466,17 @@ Proof. rewrite ZToWord_plus; auto. Qed. +Lemma zadd_vplus3 : + forall w1 w2, + (wordToN w1 + wordToN w2 < Npow2 32)%N -> + valueToN (vplus (mkvalue 32 w1) (mkvalue 32 w2) eq_refl) = + (valueToN (mkvalue 32 w1) + valueToN (mkvalue 32 w2))%N. +Proof. + intros. unfold vplus, map_word2. rewrite unify_word_unfold. unfold valueToN. + simplify. unfold wplus. unfold wordBin. Search wordToN NToWord. + rewrite wordToN_NToWord_2. trivial. assumption. +Qed. + Lemma wordsize_32 : Int.wordsize = 32%nat. Proof. auto. Qed. @@ -431,6 +490,24 @@ Proof. rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. Qed. +Lemma intadd_vplus2 : + forall v1 v2 EQ, + Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ). +Proof. + intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr). + rewrite zadd_vplus3. trivial. + +Lemma valadd_vplus : + forall v1 v2 v1' v2' v v' EQ, + val_value_lessdef v1 v1' -> + val_value_lessdef v2 v2' -> + Val.add v1 v2 = v -> + vplus v1' v2' EQ = v' -> + val_value_lessdef v v'. +Proof. + intros. inv H; inv H0; constructor; simplify. + - + Lemma zsub_vminus : forall sz z1 z2, (sz > 0)%nat -> -- cgit