diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-07-03 21:05:45 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-03 21:05:45 +0100 |
commit | 594c2825012d94675317f51cf6a3e97c2f88cd02 (patch) | |
tree | 19c6b85504a9040cb48161325cdda14208ae9155 /src/translation/HTLgenproof.v | |
parent | b5144a6f513c5c6e3344dcc935117706637ddd3f (diff) | |
download | vericert-kvx-594c2825012d94675317f51cf6a3e97c2f88cd02.tar.gz vericert-kvx-594c2825012d94675317f51cf6a3e97c2f88cd02.zip |
Fixing HTLgenproof
Diffstat (limited to 'src/translation/HTLgenproof.v')
-rw-r--r-- | src/translation/HTLgenproof.v | 45 |
1 files changed, 32 insertions, 13 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 956c3ed..79bca49 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -16,9 +16,9 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require RTL Registers AST Integers. -From compcert Require Import Globalenvs Memory. -From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap Array IntegerExtra ZExtra. +From compcert Require RTL Registers AST. +From compcert Require Import Integers Globalenvs Memory. +From coqup Require Import Coquplib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra. From coqup Require HTL Verilog. Require Import Lia. @@ -41,7 +41,7 @@ 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 -> - asa!(m.(HTL.mod_st)) = Some (posToValue 32 st). + 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) : @@ -53,7 +53,7 @@ Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (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 (4 * ptr)))) - (Option.default (NToValue 32 0) + (Option.default (NToValue 0) (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> match_arrs m f sp mem asa. @@ -254,12 +254,6 @@ Proof. assumption. Qed. -(* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) -Lemma assumption_32bit : - forall v, - valueToPos (posToValue 32 v) = v. -Admitted. - Ltac inv_state := match goal with MSTATE : match_states _ _ |- _ => @@ -358,6 +352,14 @@ Section CORRECTNESS. (Genv.senv_transf_partial TRANSL'). Hint Resolve senv_preserved : htlproof. + Lemma ptrofs_inj : + forall a b, + Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b. + Proof. + intros. rewrite <- Ptrofs.repr_unsigned. symmetry. rewrite <- Ptrofs.repr_unsigned. + rewrite H. auto. + 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) -> @@ -373,12 +375,29 @@ Section CORRECTNESS. - 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. + - eexists. split. constructor. constructor. auto. - 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. + unfold Verilog.unop_run. unfold Values.Val.neg. destruct (Registers.Regmap.get r rs) eqn:?; constructor. + inv HPle. auto. + - inv Heql. + assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + assert (HPle0 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle. apply H in HPle0. + eexists. split. econstructor; eauto. constructor. trivial. + constructor. trivial. simplify. inv HPle. inv HPle0; constructor; auto. + + inv HPle0. constructor. unfold valueToPtr. Search Integers.Ptrofs.sub Integers.int. + pose proof Integers.Ptrofs.agree32_sub. unfold Integers.Ptrofs.agree32 in H3. + Print Integers.Ptrofs.agree32. unfold Ptrofs.of_int. simpl. + apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H3 in H4. + rewrite Ptrofs.unsigned_repr. apply H4. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. + auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. Lemma eval_cond_correct : forall cond (args : list Registers.reg) s1 c s' i rs args m b f asr asa, |