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
123
124
125
|
(* *********************************************************************)
(* *)
(* 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 Maps.
Require Import AST.
Require Import Integers.
Require Import Memdata.
Require Import Op.
Require Import RTL.
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, f) (prog_funct p) -> wt_fundef f.
|
