forked from kframework/c-semantics
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathbinding.k
194 lines (176 loc) · 8.5 KB
/
binding.k
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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
module C-BINDING-SYNTAX
imports C-SYNTAX
imports C-DYNAMIC-SYNTAX
// RValues, Types, CIds
syntax KItem ::= bind(List, List, List)
syntax KItem ::= bindParam(CId, Type, K) [klabel(bindParam3)]
syntax KItem ::= bindParam(CId)
syntax Bool ::= areArgPromoted(List) [function]
syntax Type ::= elideDecl(Type) [function]
endmodule
module C-BINDING
imports C-BINDING-SYNTAX
imports C-COMMON-PROMOTION-SYNTAX
imports C-CONVERSION-SYNTAX
imports C-ENV-SYNTAX
imports C-ERROR-SYNTAX
imports C-MEMORY-ALLOC-SYNTAX
imports C-SYMLOC-SYNTAX
imports C-TYPING-COMPATIBILITY-SYNTAX
imports C-TYPING-SYNTAX
imports C-SETTINGS-SYNTAX
imports C-CONFIGURATION
// Construct the function parameters. Takes three lists: (1) the formal
// parameters (ids and types) from the function definition, (2) the
// prototype for the function, if any (as a list of parameter types), and
// (3) the actual, evaluated arguments being passed during this call. If
// the second list is empty, then the parameters need to be promoted. If
// the first list doesn't have ids, then we're dealing with a builtin, so
// we need to make up identifiers.
// Prototype.
rule (.K => bindParam(X, T, V))
~> bind(
(ListItem(typedDeclaration(T:Type, X:CId)) => .List) _,
(ListItem(_) => .List) _,
(ListItem(V:RValue) => .List) _)
requires notBool isVoidType(T)
[structural]
// No prototype -- but the args must still have ids/types in the def.
rule (.K => bindParam(X, T, argPromote(V)))
~> bind(
(ListItem(typedDeclaration(T:Type, X:CId)) => .List) _,
.List,
(ListItem(V:RValue) => .List) _)
requires #arePromotedTypesCompat(value(V):>CValue, T, type(V))
[structural]
rule (.K => UNDEF("CB1", "Types of function call arguments aren't "
+String "compatible with declared types after promotions.", "6.5.2.2:6, J.2:1 item 39"))
~> bind(
ListItem(typedDeclaration(T:Type, _)) _,
.List,
ListItem(V:RValue) _)
requires notBool #arePromotedTypesCompat(value(V):>CValue, T, type(V))
andBool notBool isVoidType(T)
[structural]
rule (.K => UNDEF("CB2", "Function call has fewer arguments than "
+String "parameters in function definition.", "6.5.2.2:6, J.2:1 item 38"))
~> bind(
ListItem(T:Type) _,
_,
.List)
requires notBool isVoidType(T)
rule (.K => UNDEF("CB3", "Function call has more arguments than "
+String "parameters in function definition.", "6.5.2.2:6, J.2:1 item 38"))
~> bind(.List, _, ListItem(_) _)
rule (.K => UNDEF("CB4", "Function defined with no parameters "
+String "called with arguments.", "6.5.2.2:6, J.2:1 item 38"))
~> bind(ListItem(T:Type), _, ListItem(_) _)
requires isVoidType(T)
// Variadic.
rule bind(ListItem(variadic), ListItem(variadic), Vs:List)
=> bindVariadics(Vs, 0)
[structural]
// No params.
rule bind(ListItem(T:Type), ListItem(T':Type), .List) => .K
requires isVoidType(T) andBool isVoidType(T')
[structural]
rule bind(ListItem(T:Type), .List, .List) => .K
requires isVoidType(T)
[structural]
// Builtins -- they don't have named parameters.
rule <k> (.K => bindParam(unnamed(N, Tu), T, V))
~> bind(
(ListItem(T:Type) => .List) _,
(ListItem(_) => .List) _,
(ListItem(V:RValue) => .List) _)
...</k>
<curr-tu> Tu:String </curr-tu>
<tu-id> Tu </tu-id>
<next-unnamed> N:Int => N +Int 1 </next-unnamed>
requires T =/=K variadic
andBool notBool isTypedDeclaration(T)
[structural]
rule bind(.List, .List, .List) => .K
[structural]
rule elideDecl(typedDeclaration(T:Type, _)) => T
rule elideDecl(T:Type) => T [owise]
syntax KItem ::= bindVariadics(List, Int)
rule (.K => bindParam(vararg(N), stripConstants(type(argPromote(V))), argPromote(V)))
~> bindVariadics(
(ListItem(V:RValue) => .List) _,
(N:Int => N +Int 1))
[structural]
// Make one past the last variadic a legal address.
rule bindVariadics(.List, N:Int) => bindParam(vararg(N))
[structural]
// n1494 6.5.2.2:6 If the expression that denotes the called function has
// a type that does not include a prototype, the integer promotions are
// performed on each argument, and arguments that have type float are
// promoted to double. These are called the default argument promotions.
// If the number of arguments does not equal the number of parameters, the
// behavior is undefined. If the function is defined with a type that
// includes a prototype, and either the prototype ends with an ellipsis (,
// ...) or the types of the arguments after promotion are not compatible
// with the types of the parameters, the behavior is undefined. If the
// function is defined with a type that does not include a prototype, and
// the types of the arguments after promotion are not compatible with
// those of the parameters after promotion, the behavior is undefined,
// except for the following cases:
//
// -- one promoted type is a signed integer type, the other promoted type
// is the corresponding unsigned integer type, and the value is
// representable in both types;
//
// -- both types are pointers to qualified or unqualified versions of a
// character type or void
syntax Bool ::= #arePromotedTypesCompat(CValue, Type, Type)
[function]
rule #arePromotedTypesCompat(_, T:Type, T':Type) => true
requires areCompatible(argPromoteType(T), argPromoteType(T'))
rule #arePromotedTypesCompat(V:Int, T:Type, T':SignedIntegerType) => true
requires (argPromoteType(T)
==K correspondingUnsignedType(argPromoteType(T')))
andBool representable(V, argPromoteType(T))
andBool representable(V,
correspondingUnsignedType(argPromoteType(T')))
rule #arePromotedTypesCompat(V:Int, T:SignedIntegerType, T':Type) => true
requires (argPromoteType(T')
==K correspondingUnsignedType(argPromoteType(T)))
andBool representable(V, argPromoteType(T'))
andBool representable(V,
correspondingUnsignedType(argPromoteType(T)))
rule #arePromotedTypesCompat(_, T:PointerType, T':PointerType) => true
requires (isCharType(innerType(argPromoteType(T)))
orBool isVoidType(innerType(argPromoteType(T))))
andBool (isCharType(innerType(argPromoteType(T')))
orBool isVoidType(innerType(argPromoteType(T'))))
rule #arePromotedTypesCompat(_, _, _) => false [owise]
syntax Bool ::= representable(Int, Type) [function]
rule representable(V:Int, T:Type)
=> (V <=Int max(T)) andBool (V >=Int min(T))
syntax RValue ::= argPromote(K) [function]
rule argPromote(V:RValue) => cast(argPromoteType(type(V)), V)
// "integer promotions" are used when doing arithmetic conversions, and
// for unary ~, +, - "usual arithmetic conversions" are used when doing
// binary arithmetic on numbers, and are used to find a common type there
// is another set of promotions called "default argument promotions" used
// when calling functions where the type information is not complete. This
// is equivalent to integer promotions + (float => double)
syntax Type ::= argPromoteType(Type) [function]
rule argPromoteType(t(Mods:Set, float))
=> t(Mods, double)
rule argPromoteType(t(Mods:Set, double))
=> t(Mods, double)
rule argPromoteType(t(Mods:Set, long-double))
=> t(Mods, long-double)
rule argPromoteType(T:IntegerType)
=> promote(T)
rule argPromoteType(T:Type) => T [owise]
// "are argument-promoted".
rule areArgPromoted(L:List) => true
requires all(L, #klabel(`isArgPromoted`))
rule areArgPromoted(_) => false [owise]
syntax Bool ::= isArgPromoted(Type) [function]
rule isArgPromoted(T:Type)
=> areCompatible(elideDecl(T), argPromoteType(elideDecl(T)))
endmodule