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
120
121
122
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(** Typing rules for LTLin. *)
Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Op.
Require Import Locations.
Require Import LTLin.
Require LTLtyping.
Require Import Conventions.
(** The following predicates define a type system for LTLin similar to that
of LTL. *)
Section WT_INSTR.
Variable funsig: signature.
Inductive wt_instr : instruction -> Prop :=
| wt_Lopmove:
forall r1 r,
Loc.type r1 = Loc.type r -> loc_acceptable r1 -> loc_acceptable r ->
wt_instr (Lop Omove (r1 :: nil) r)
| wt_Lop:
forall op args res,
op <> Omove ->
(List.map Loc.type args, Loc.type res) = type_of_operation op ->
locs_acceptable args -> loc_acceptable res ->
wt_instr (Lop op args res)
| wt_Lload:
forall chunk addr args dst,
List.map Loc.type args = type_of_addressing addr ->
Loc.type dst = type_of_chunk chunk ->
locs_acceptable args -> loc_acceptable dst ->
wt_instr (Lload chunk addr args dst)
| wt_Lstore:
forall chunk addr args src,
List.map Loc.type args = type_of_addressing addr ->
Loc.type src = type_of_chunk chunk ->
locs_acceptable args -> loc_acceptable src ->
wt_instr (Lstore chunk addr args src)
| wt_Lcall:
forall sig ros args res,
List.map Loc.type args = sig.(sig_args) ->
Loc.type res = proj_sig_res sig ->
LTLtyping.call_loc_acceptable sig ros ->
locs_acceptable args -> loc_acceptable res ->
wt_instr (Lcall sig ros args res)
| wt_Ltailcall:
forall sig ros args,
List.map Loc.type args = sig.(sig_args) ->
LTLtyping.call_loc_acceptable sig ros ->
locs_acceptable args ->
sig.(sig_res) = funsig.(sig_res) ->
tailcall_possible sig ->
wt_instr (Ltailcall sig ros args)
| wt_Lbuiltin:
forall ef args res,
List.map Loc.type args = (ef_sig ef).(sig_args) ->
Loc.type res = proj_sig_res (ef_sig ef) ->
arity_ok (ef_sig ef).(sig_args) = true \/ ef_reloads ef = false ->
locs_acceptable args -> loc_acceptable res ->
wt_instr (Lbuiltin ef args res)
| wt_Llabel: forall lbl,
wt_instr (Llabel lbl)
| wt_Lgoto: forall lbl,
wt_instr (Lgoto lbl)
| wt_Lcond:
forall cond args lbl,
List.map Loc.type args = type_of_condition cond ->
locs_acceptable args ->
wt_instr (Lcond cond args lbl)
| wt_Ljumptable:
forall arg tbl,
Loc.type arg = Tint ->
loc_acceptable arg ->
list_length_z tbl * 4 <= Int.max_unsigned ->
wt_instr (Ljumptable arg tbl)
| wt_Lreturn:
forall optres,
option_map Loc.type optres = funsig.(sig_res) ->
match optres with None => True | Some r => loc_acceptable r end ->
wt_instr (Lreturn optres).
Definition wt_code (c: code) : Prop :=
forall i, In i c -> wt_instr i.
End WT_INSTR.
Record wt_function (f: function): Prop :=
mk_wt_function {
wt_params:
List.map Loc.type f.(fn_params) = f.(fn_sig).(sig_args);
wt_acceptable:
locs_acceptable f.(fn_params);
wt_norepet:
Loc.norepet f.(fn_params);
wt_instrs:
wt_code f.(fn_sig) f.(fn_code)
}.
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.
|
