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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Type system for the Mach intermediate language. *)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Memory.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Import Conventions.
Require Import Mach.
(** * Typing rules *)
Inductive wt_instr : instruction -> Prop :=
| wt_Mlabel:
forall lbl,
wt_instr (Mlabel lbl)
| wt_Mgetstack:
forall ofs ty r,
mreg_type r = ty ->
wt_instr (Mgetstack ofs ty r)
| wt_Msetstack:
forall ofs ty r,
mreg_type r = ty ->
wt_instr (Msetstack r ofs ty)
| wt_Mgetparam:
forall ofs ty r,
mreg_type r = ty ->
wt_instr (Mgetparam ofs ty r)
| wt_Mopmove:
forall r1 r,
mreg_type r1 = mreg_type r ->
wt_instr (Mop Omove (r1 :: nil) r)
| wt_Mop:
forall op args res,
op <> Omove ->
(List.map mreg_type args, mreg_type res) = type_of_operation op ->
wt_instr (Mop op args res)
| wt_Mload:
forall chunk addr args dst,
List.map mreg_type args = type_of_addressing addr ->
mreg_type dst = type_of_chunk chunk ->
wt_instr (Mload chunk addr args dst)
| wt_Mstore:
forall chunk addr args src,
List.map mreg_type args = type_of_addressing addr ->
mreg_type src = type_of_chunk chunk ->
wt_instr (Mstore chunk addr args src)
| wt_Mcall:
forall sig ros,
match ros with inl r => mreg_type r = Tint | inr s => True end ->
wt_instr (Mcall sig ros)
| wt_Mtailcall:
forall sig ros,
tailcall_possible sig ->
match ros with inl r => mreg_type r = Tint | inr s => True end ->
wt_instr (Mtailcall sig ros)
| wt_Mbuiltin:
forall ef args res,
List.map mreg_type args = (ef_sig ef).(sig_args) ->
mreg_type res = proj_sig_res (ef_sig ef) ->
wt_instr (Mbuiltin ef args res)
| wt_Mannot:
forall ef args,
ef_reloads ef = false ->
wt_instr (Mannot ef args)
| wt_Mgoto:
forall lbl,
wt_instr (Mgoto lbl)
| wt_Mcond:
forall cond args lbl,
List.map mreg_type args = type_of_condition cond ->
wt_instr (Mcond cond args lbl)
| wt_Mjumptable:
forall arg tbl,
mreg_type arg = Tint ->
list_length_z tbl * 4 <= Int.max_unsigned ->
wt_instr (Mjumptable arg tbl)
| wt_Mreturn:
wt_instr Mreturn.
Record wt_function (f: function) : Prop := mk_wt_function {
wt_function_instrs:
forall instr, In instr f.(fn_code) -> wt_instr instr;
wt_function_stacksize:
0 <= f.(fn_stacksize) <= Int.max_unsigned
}.
Inductive wt_fundef: fundef -> Prop :=
| wt_fundef_external: forall ef,
wt_fundef (External ef)
| wt_function_internal: forall f,
wt_function f ->
wt_fundef (Internal f).
Definition wt_program (p: program) : Prop :=
forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
|
