blob: 38fbd6d3d582187d77af96442c156ec0c290440a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* Léo Gourdin UGA, VERIMAG *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
(** Common definition and proofs on Asmblock required by various modules *)
Require Import Coqlib.
Require Import Integers.
Require Import Memory.
Require Import Globalenvs.
Require Import Values.
Require Import Asmblock.
Require Import Axioms.
Definition bblock_simu (lk: aarch64_linker) (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
forall rs m rs' m' t,
exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk ge f bb' rs m t rs' m'.
Definition bblock_simu_aux (lk: aarch64_linker) (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
forall rs m,
bbstep lk ge f bb rs m <> Stuck ->
bbstep lk ge f bb rs m = bbstep lk ge f bb' rs m.
Hint Extern 2 (_ <> _) => congruence: asmgen.
Lemma preg_of_data:
forall r, data_preg (preg_of r) = true.
Proof.
intros. destruct r; reflexivity.
Qed.
Lemma dreg_of_data:
forall r, data_preg (dreg_of r) = true.
Proof.
intros. destruct r; reflexivity.
Qed.
Hint Resolve preg_of_data dreg_of_data: asmgen.
Lemma data_diff:
forall r r',
data_preg r = true -> data_preg r' = false -> r <> r'.
Proof.
congruence.
Qed.
Hint Resolve data_diff: asmgen.
Lemma preg_of_not_PC:
forall r, preg_of r <> PC.
Proof.
intros. apply data_diff; auto with asmgen.
Qed.
Lemma preg_of_not_SP:
forall r, preg_of r <> SP.
Proof.
intros. unfold preg_of; destruct r; simpl; try discriminate.
Qed.
Ltac desif :=
repeat match goal with
| [ |- context[ if ?f then _ else _ ] ] => destruct f
end.
Ltac decomp :=
repeat match goal with
| [ |- context[ match (?rs ?r) with | _ => _ end ] ] => destruct (rs r)
end.
Ltac Simplif :=
((desif)
|| (try unfold compare_long)
|| (try unfold compare_int)
|| (try unfold compare_float)
|| (try unfold compare_single)
|| decomp
|| (rewrite Pregmap.gss)
|| (rewrite Pregmap.gso by eauto with asmgen)
); auto with asmgen.
Ltac Simpl := repeat Simplif.
Section EPC.
Variable lk: aarch64_linker.
(* For Asmblockgenproof0 *)
Theorem exec_basic_instr_pc:
forall ge b rs1 m1 rs2 m2,
exec_basic lk ge b rs1 m1 = Next rs2 m2 ->
rs2 PC = rs1 PC.
Proof.
intros. destruct b; try destruct i; try destruct i; try destruct ld; try destruct ld;
try destruct st; try destruct st; try destruct a.
all: try (inv H; simpl in *; auto; Simpl).
all: try (try unfold exec_load_rd_a in H1; try destruct (Mem.loadv _ _ _); inv H1; Simpl).
all: try (try unfold exec_load_double in H0; destruct (Mem.loadv _ _ _); simpl in *;
try destruct (Mem.loadv _ _ _); simpl in *; inv H0; Simpl).
all: try (try unfold exec_store_rs_a in H0; try destruct (Mem.storev _ _ _); inv H0; auto; Simpl).
all: try (try unfold exec_store_double in H1; destruct (Mem.storev _ _ _); simpl in *;
try destruct (Mem.storev _ _ _); simpl in *; inv H1; auto; Simpl).
- (* alloc *)
destruct (Mem.alloc _ _ _); destruct (Mem.store _ _ _); inv H1; auto; Simpl.
- (* free *)
destruct (rs1 SP); try discriminate; destruct (Mem.free _ _ _ _); inv H1; Simpl.
Qed.
End EPC.
|
