forked from kframework/c-semantics
-
Notifications
You must be signed in to change notification settings - Fork 0
/
function-def.k
217 lines (195 loc) · 8.34 KB
/
function-def.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
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
module C-FUNCTION-DEF-SYNTAX
syntax K ::= initFunction(K, K) [strict]
syntax Bool ::= hasDupParams(Type) [function]
endmodule
module C-FUNCTION-DEF
imports C-FUNCTION-DEF-SYNTAX
imports C-DECL-DEFINITION-SYNTAX
imports C-DECL-INITIALIZER-SYNTAX
imports C-DYNAMIC-SYNTAX
imports C-ENV-SYNTAX
imports C-ERROR-SYNTAX
imports C-MEMORY-ALLOC-SYNTAX
imports C-PROCESS-LABEL-SYNTAX
imports C-SYMBOLIC-VALUE-SYNTAX
imports C-SYMLOC-SYNTAX
imports C-SYNTAX
imports C-TYPING-SYNTAX
imports C-BINDING-SYNTAX
imports COMPAT-SYNTAX
rule FunctionDefinition(typedDeclaration(T:Type, X:CId), Blk:K)
=> declare(
typedDeclaration(toPrototype(T), X),
initializer(initFunction(
&(X),
functionObject(X,
// The sanitized declared parameters.
elideList(getParams(emptyToVoid(T))),
// The "prototype" -- basically a type with the same
// parameters as above, but the parameters are set to
// .List if there isn't actually a prototype.
toPrototype(T),
Goto(funLabel(X)))
))
)
~> calculateGotoMap(X, Label(funLabel(X), safeBody(X, Blk)))
~> processFunDef(X, Blk)
when isFunctionType(T) andBool notBool hasDupParams(T)
[structural]
rule (. => ERROR("FD1", "duplicate parameters in "
+String "function definition."))
~> FunctionDefinition(typedDeclaration(T:Type, _), _)
when hasDupParams(T)
// TODO(chathhorn): possibly check that old-style declarations are
// promoted types?
// Turns empty param list into void and turns an old-style param list into
// the empty list so that arguments will be promoted on call.
syntax Type ::= toPrototype(Type) [function]
rule toPrototype(T:Type) => elideDeclParams(emptyToVoid(T))
when notBool isOldStyleFunctionType(T)
rule toPrototype(T:Type) => setParams(T, .List)
when isOldStyleFunctionType(T)
syntax Type ::= emptyToVoid(Type) [function]
rule emptyToVoid(T:Type)
=> setParams(T, ListItem(typedDeclaration(t(.Set, void), #NoName)))
when isFunctionType(T)
andBool (getParams(T) ==List .List)
rule emptyToVoid(T:Type) => T
when notBool isFunctionType(T)
orBool (getParams(T) =/=List .List)
syntax K ::= processFunDef(CId, K)
rule <k> processFunDef(X:CId, Blk:K)
=> checkFunDefType(X, Proto)
~> staticEval(X, Params, Blk)
...</k>
<env>... X |-> Base:SymBase ...</env>
<functions>...
Base |-> functionObject(_, Params:List, Proto:Type, _)
...</functions>
[structural]
syntax K ::= checkFunDefType(CId, Type)
rule checkFunDefType(X:CId, T:Type) => .
when notBool isFunctionType(getReturn(T))
andBool notBool isArrayType(getReturn(T))
andBool areVoidOrComplete(getParams(T))
andBool (X =/=K Identifier("main"))
[structural]
rule checkFunDefType(X:CId, T:Type) => checkMainDef(T)
when isVoidOrComplete(getReturn(T))
andBool areVoidOrComplete(getParams(T))
andBool (X ==K Identifier("main"))
[structural]
rule (. => UNDEF("FD2", "invalid return type in function definition.",
"6.7.6.3:1"))
~> checkFunDefType(_, T:Type)
when isFunctionType(getReturn(T)) orBool isArrayType(getReturn(T))
[structural]
rule (. => UNDEF("FD3", "incomplete parameter type in "
+String "function definition.", "6.7.6.3:4"))
~> checkFunDefType(_, T:Type)
when notBool areVoidOrComplete(getParams(T))
[structural]
syntax Bool ::= isVoidOrComplete(Type) [function]
rule isVoidOrComplete(T:Type)
=> isCompleteType(T)
orBool isVoidType(T)
orBool isIncompleteArrayType(T)
syntax Bool ::= areVoidOrComplete(List) [function]
rule areVoidOrComplete(L:List) => all(L, 'isVoidOrComplete) ==K true
syntax K ::= checkMainDef(Type)
rule checkMainDef(t(_, functionType(t(_, int),
ListItem(t(_, void)))))
=> .
[structural]
rule checkMainDef(t(_, functionType(t(_, int),
ListItem(t(_, int)) ListItem(T:Type))))
=> .
when #isArgvType(T) ==K true
[structural]
rule (. => ERROR("FD4", "definition of main requires a prototype (5.1.2.2.1p1)."))
~> checkMainDef(T:Type)
when isOldStyleFunctionType(T)
[structural]
rule (. => ERROR("FD5", "main must return an int.", 4) )
~> checkMainDef(t(_, functionType(t(_, T:SimpleType), _)))
when T =/=K int
[structural]
rule (. => ERROR("FD6", "if main has arguments, the type of the first argument must be equivalent to int.", 4) )
~> checkMainDef(t(_, functionType(_, ListItem(t(_, T:SimpleType)) _)))
when T =/=K int andBool T =/=K void
[structural]
rule (. => ERROR("FD7", "if main has arguments, the type of the second argument must be equivalent to char**.") )
~> checkMainDef(t(_, functionType(_, ListItem(_:Type) ListItem(T:Type))))
when #isArgvType(T) =/=K true
[structural]
rule (. => ERROR("FD8", "main must have zero or two parameters.") )
~> checkMainDef(t(_, functionType(_, Params:List)))
when lengthList(Params) >Int 2
[structural]
rule (. => ERROR("FD9", "main must have zero or two parameters.") )
~> checkMainDef(t(_, functionType(_, ListItem(t(_, T:SimpleType)))))
when T =/=K void
[structural]
syntax Bool ::= "#isArgvType" "(" Type ")" [function]
rule #isArgvType(t(_, incompleteArrayType(t(_, pointerType(t(_, T:SimpleType))))))
=> true
when T ==K char // char is an alias.
rule #isArgvType(t(_, pointerType(t(_, pointerType(t(_, T:SimpleType))))))
=> true
when T ==K char
rule <k> initFunction(
tv(Loc:SymLoc, t(_, pointerType(T:Type))), Fun:KResult)
=> .
...</k>
<functions> M:Map => M[Fun <- base(Loc)] </functions>
when isFunctionType(T) andBool (notBool base(Loc) in keys(M))
[structural]
syntax K ::= safeBody(CId, K) [function]
rule safeBody(X:CId, Blk:K)
=> Blk ~> Return(NothingExpression)
when X =/=K Identifier("main")
rule safeBody(Identifier("main"), Blk:K)
=> Blk ~> Return(tv(0, t(.Set, int)))
syntax K ::= "returnToFileScope"
syntax K ::= staticEval(CId, List, K)
rule <k> staticEval(X:CId, Params:List, Blk:K)
=> pushBlock
~> dummyBind(Params)
~> Blk
~> popBlock
~> returnToFileScope
...</k>
<curr-function> _ => X </curr-function>
[structural]
rule <k> returnToFileScope => . ...</k>
<curr-function> _ => file-scope </curr-function>
[structural]
syntax Bool ::= "#hasDupParams'" "(" Type ")" [function]
rule hasDupParams(T:Type) => #hasDupParams'(T) ==K true
rule #hasDupParams'(typedDeclaration(T:Type, _)) => #hasDupParams'(T)
rule #hasDupParams'(t(_, functionType(_, P:List))) => #hasDupIds'(P)
syntax Bool ::= hasDupIds(List) [function]
syntax Bool ::= "#hasDupIds'" "(" List ")" [function]
rule hasDupIds(P:List) => #hasDupIds'(P) ==K true
rule #hasDupIds'(
_
ListItem(typedDeclaration(_, X:CId))
_
ListItem(typedDeclaration(_, X:CId))
_
) => true
syntax K ::= dummyBind(List)
rule dummyBind(.List) => .
[structural]
rule dummyBind(ListItem(variadic)) => .
[structural]
rule dummyBind(ListItem(typedDeclaration(T:Type, _))) => .
when isVoidType(T)
[structural]
rule dummyBind(ListItem(typedDeclaration(T:Type, X:CId)) Params:List)
=> addToEnv(X, symVal)
~> giveType(X, T)
~> dummyBind(Params)
when notBool isVoidType(T)
[structural]
endmodule