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
|
(* *********************************************************************)
(* *)
(* 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 AST.
Require Import Integers.
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, Gfun f) (prog_defs p) -> wt_fundef f.
|
