/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_routine_translator_base.e
ViewVC logotype

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_routine_translator_base.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93597 - (show annotations)
Tue Dec 3 00:48:44 2013 UTC (5 years, 10 months ago) by julian
File size: 12776 byte(s)
AutoProof: special translation for lemma and functional
1 note
2 description: "[
3 Base class for routine translators.
4 ]"
5 date: "$Date$"
6 revision: "$Revision$"
7
8 deferred class
9 E2B_ROUTINE_TRANSLATOR_BASE
10
11 inherit
12
13 E2B_FEATURE_TRANSLATOR
14
15 INTERNAL_COMPILER_STRING_EXPORTER
16
17 feature -- Access
18
19 current_feature: FEATURE_I
20 -- Currently translated feature.
21
22 current_type: TYPE_A
23 -- Type of currently translated feature.
24
25 current_boogie_procedure: detachable IV_PROCEDURE
26 -- Currently generated Boogie procedure (if any).
27
28 feature -- Element change
29
30 set_context (a_feature: FEATURE_I; a_type: TYPE_A)
31 -- Set context of current translation.
32 do
33 current_feature := a_feature
34 if a_type.is_attached then
35 current_type := a_type
36 else
37 current_type := a_type.as_attached_type
38 end
39 ensure
40 current_feature_set: current_feature = a_feature
41 current_type_set: current_type.same_as (a_type.as_attached_type)
42 end
43
44 set_up_boogie_procedure (a_boogie_name: STRING)
45 -- Set up `current_boogie_procedure'.
46 do
47 current_boogie_procedure := boogie_universe.procedure_named (a_boogie_name)
48 if not attached current_boogie_procedure then
49 create current_boogie_procedure.make (a_boogie_name)
50 boogie_universe.add_declaration (current_boogie_procedure)
51 end
52 ensure
53 current_boogie_procedure_set: attached current_boogie_procedure
54 current_boogie_procedure_named: current_boogie_procedure.name ~ a_boogie_name
55 current_boogie_procedure_added: boogie_universe.procedure_named (a_boogie_name) = current_boogie_procedure
56 end
57
58 feature -- Helper functions: arguments and result
59
60 arguments_of (a_feature: FEATURE_I; a_context: TYPE_A): ARRAYED_LIST [TUPLE [name: STRING; type: TYPE_A; boogie_type: IV_TYPE]]
61 -- List of feature arguments of `a_feature'.
62 require
63 a_feature_attached: attached a_feature
64 a_context_attached: attached a_context
65 local
66 i: INTEGER
67 l_type: TYPE_A
68 do
69 create Result.make (a_feature.argument_count)
70 from i := 1 until i > a_feature.argument_count loop
71 l_type := a_feature.arguments.i_th (i).deep_actual_type.instantiated_in (a_context)
72 Result.extend([
73 a_feature.arguments.item_name (i),
74 l_type,
75 types.for_type_a (l_type)
76 ])
77 i := i + 1
78 end
79 end
80
81 arguments_of_current_feature: like arguments_of
82 -- List of arguments of `current_feature'.
83 require
84 current_feature_set: attached current_feature
85 current_type_set: attached current_type
86 do
87 Result := arguments_of (current_feature, current_type)
88 end
89
90 add_argument_with_property (a_name: STRING; a_type: TYPE_A; a_boogie_type: IV_TYPE)
91 -- Add argument and property to current procedure.
92 require
93 current_procedure_set: attached current_boogie_procedure
94 local
95 l_type_translator: E2B_TYPE_TRANSLATOR
96 l_pre: IV_PRECONDITION
97 do
98 current_boogie_procedure.add_argument (a_name, a_boogie_type)
99 create l_type_translator
100 l_type_translator.generate_argument_property (create {IV_ENTITY}.make (a_name, a_boogie_type), a_type)
101 if attached l_type_translator.last_property then
102 create l_pre.make (l_type_translator.last_property)
103 l_pre.set_free
104 l_pre.set_assertion_type ("type property for argument " + a_name)
105 current_boogie_procedure.add_contract (l_pre)
106 end
107 end
108
109 add_result_with_property
110 -- Add result to current procedure.
111 local
112 l_type: TYPE_A
113 l_iv_type: IV_TYPE
114 l_type_translator: E2B_TYPE_TRANSLATOR
115 do
116 if current_feature.has_return_value then
117 l_type := current_feature.type.deep_actual_type.instantiated_in (current_type)
118 l_iv_type := types.for_type_a (l_type)
119 create l_type_translator
120 l_type_translator.generate_argument_property (create {IV_ENTITY}.make ("Result", l_iv_type), l_type)
121 translation_pool.add_type (l_type)
122 current_boogie_procedure.add_result_with_property (
123 "Result",
124 l_iv_type,
125 l_type_translator.last_property)
126 end
127 end
128
129 feature -- Helper functions: contracts
130
131 contracts_of (a_feature: FEATURE_I; a_type: TYPE_A): TUPLE [pre, post, modifies, reads, decreases: LIST [ASSERT_B]]
132 -- Contracts for feature `a_feature' of type `a_type'.
133 local
134 l_pre, l_post, l_modifies, l_reads, l_decreases: LINKED_LIST [ASSERT_B]
135 l_name: STRING_32
136 do
137 create l_pre.make
138 create l_post.make
139 create l_modifies.make
140 create l_reads.make
141 create l_decreases.make
142
143 helper.set_up_byte_context (a_feature, a_type)
144 if attached Context.byte_code as l_byte_code then
145 -- Process pre/post-conditions
146 if l_byte_code.precondition /= Void then
147 l_byte_code.precondition.do_all (agent l_pre.extend (?))
148 end
149 if l_byte_code.postcondition /= Void then
150 l_byte_code.postcondition.do_all (agent l_post.extend (?))
151 end
152 if a_feature.assert_id_set /= Void and not a_type.is_basic then
153 -- Feature has inherited assertions
154 l_byte_code.formulate_inherited_assertions (a_feature.assert_id_set)
155 across Context.inherited_assertion.precondition_list as i loop
156 i.item.do_all (agent l_pre.extend (?))
157 end
158 across Context.inherited_assertion.postcondition_list as i loop
159 i.item.do_all (agent l_post.extend (?))
160 end
161 end
162 end
163 from
164 l_pre.start
165 until
166 l_pre.after
167 loop
168 if attached {FEATURE_B} l_pre.item.expr as l_call then
169 l_name := names_heap.item_32 (l_call.feature_name_id)
170 if l_name ~ "modify" or l_name ~ "modify_field" then
171 l_modifies.extend (l_pre.item)
172 l_pre.remove
173 elseif l_name ~ "reads" then
174 l_reads.extend (l_pre.item)
175 l_pre.remove
176 elseif l_name ~ "decreases" then
177 l_decreases.extend (l_pre.item)
178 l_pre.remove
179 else
180 l_pre.forth
181 end
182 else
183 l_pre.forth
184 end
185 end
186 from
187 l_post.start
188 until
189 l_post.after
190 loop
191 if attached {FEATURE_B} l_post.item.expr as l_call then
192 l_name := names_heap.item_32 (l_call.feature_name_id)
193 if l_name ~ "modify" or l_name ~ "modify_field" then
194 l_modifies.extend (l_post.item)
195 l_post.remove
196 elseif l_name ~ "reads" then
197 l_reads.extend (l_post.item)
198 l_post.remove
199 elseif l_name ~ "decreases" then
200 l_decreases.extend (l_post.item)
201 l_post.remove
202 else
203 l_post.forth
204 end
205 else
206 l_post.forth
207 end
208 end
209 Result := [l_pre, l_post, l_modifies, l_reads, l_decreases]
210 end
211
212 contracts_of_current_feature: like contracts_of
213 -- Contracts for `current_feature'.
214 do
215 Result := contracts_of (current_feature, current_type)
216 end
217
218 contract_expressions_of (a_feature: FEATURE_I; a_type: TYPE_A; a_mapping: E2B_ENTITY_MAPPING): TUPLE [pre: IV_EXPRESSION; post: IV_EXPRESSION]
219 -- Contracts for feature `a_feature' of type `a_type' as expressions.
220 local
221 l_contracts: like contracts_of
222 l_pre: IV_EXPRESSION
223 l_post: IV_EXPRESSION
224 l_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR
225 do
226 l_contracts := contracts_of (a_feature, a_type)
227 if l_contracts.pre.is_empty then
228 l_pre := factory.true_
229 else
230 across l_contracts.pre as c loop
231 create l_translator.make
232 l_translator.set_context (a_feature, a_type)
233 l_translator.copy_entity_mapping (a_mapping)
234 c.item.process (l_translator)
235 if attached l_pre then
236 l_pre := factory.and_ (l_pre, l_translator.last_expression)
237 else
238 l_pre := l_translator.last_expression
239 end
240 end
241 end
242 if l_contracts.post.is_empty then
243 l_post := factory.true_
244 else
245 across l_contracts.post as c loop
246 create l_translator.make
247 l_translator.set_context (a_feature, a_type)
248 l_translator.copy_entity_mapping (a_mapping)
249 c.item.process (l_translator)
250 if attached l_post then
251 l_post := factory.and_ (l_post, l_translator.last_expression)
252 else
253 l_post := l_translator.last_expression
254 end
255 end
256 end
257 Result := [l_pre, l_post]
258 end
259
260 modifies_expressions_of (a_feature: FEATURE_I; a_type: TYPE_A): TUPLE [fully_modified: LIST [IV_EXPRESSION]; part_modified: LIST [TUPLE [fields: LIST [IV_ENTITY]; objects: LIST [IV_EXPRESSION]]]]
261 -- Modifies expressions for feature `a_feature' of type `a_type'.
262 local
263 l_contracts: like contracts_of
264 l_fully_modified: LINKED_LIST [IV_EXPRESSION]
265 l_part_modified: LINKED_LIST [TUPLE [LINKED_LIST [IV_ENTITY], LINKED_LIST [IV_EXPRESSION]]]
266 l_fieldnames: LINKED_LIST [STRING_32]
267 l_fields: LINKED_LIST [IV_ENTITY]
268 l_objects: LINKED_LIST [IV_EXPRESSION]
269 l_name: STRING_32
270 l_type: TYPE_A
271 l_feature: FEATURE_I
272 l_boogie_type: IV_TYPE
273 do
274 create l_fully_modified.make
275 create l_part_modified.make
276 l_contracts := contracts_of (a_feature, a_type)
277
278 across
279 l_contracts.modifies as i
280 loop
281 if attached {FEATURE_B} i.item.expr as l_call then
282 l_name := names_heap.item_32 (l_call.feature_name_id)
283 if l_name ~ "modify" then
284 l_objects := translate_contained_expressions (l_call.parameters.i_th (1).expression)
285 l_fully_modified.append (l_objects)
286 elseif l_name ~ "modify_field" then
287 l_objects := translate_contained_expressions (l_call.parameters.i_th (2).expression)
288
289 if attached {TUPLE_CONST_B} l_call.parameters.i_th (2).expression as l_tuple then
290 l_type := l_tuple.expressions.first.type
291 else
292 l_type := l_call.parameters.i_th (2).expression.type
293 end
294 if l_type.is_like_current then
295 l_type := current_type
296 else
297 l_type := l_type.deep_actual_type
298 end
299 if l_type.base_class.name_in_upper ~ "MML_SET" or l_type.base_class.name_in_upper ~ "MML_SEQUENCE" then
300 l_type := l_type.generics.first
301 end
302
303 create l_fieldnames.make
304 if attached {STRING_B} l_call.parameters.i_th (1).expression as l_string then
305 l_fieldnames.extend (l_string.value)
306 elseif attached {TUPLE_CONST_B} l_call.parameters.i_th (1).expression as l_tuple then
307 across l_tuple.expressions as j loop
308 if attached {STRING_B} j.item as l_string then
309 l_fieldnames.extend (l_string.value)
310 else
311 helper.add_semantic_error (a_feature, messages.modify_field_first_argument_only_manifeststrings)
312 end
313 end
314 else
315 helper.add_semantic_error (a_feature, messages.modify_field_first_argument_string_or_tuple)
316 end
317
318 create l_fields.make
319 l_fields.compare_objects
320 across l_fieldnames as f loop
321 l_feature := l_type.base_class.feature_named_32 (f.item)
322 if l_feature = Void then
323 if f.item ~ "closed" then
324 l_name := "closed"
325 l_boogie_type := types.bool
326 else
327 l_name := Void
328 helper.add_semantic_error (a_feature, messages.modify_field_field_does_not_exist (f.item, l_type.base_class.name_in_upper))
329 end
330 else
331 if translation_mapping.ghost_access.has (f.item) then
332 l_name := f.item
333 l_boogie_type := translation_mapping.ghost_access_type (f.item)
334 elseif l_feature.is_attribute then
335 l_name := name_translator.boogie_name_for_feature (l_feature, l_type)
336 l_boogie_type := types.for_type_a (l_feature.type)
337 translation_pool.add_feature (l_feature, l_type)
338 else
339 l_name := Void
340 helper.add_semantic_error (a_feature, messages.modify_field_field_not_attribute (f.item))
341 end
342 end
343 if l_name /= Void then
344 l_fields.extend (create {IV_ENTITY}.make (l_name, types.field (l_boogie_type)))
345 end
346 end
347
348 l_part_modified.extend ([l_fields, l_objects])
349 else
350 check internal_error: False end
351 end
352 else
353 check internal_error: False end
354 end
355 end
356
357 Result := [l_fully_modified, l_part_modified]
358 end
359
360 translate_contained_expressions (a_expr: EXPR_B): LINKED_LIST [IV_EXPRESSION]
361 -- Translate expressions in `a_expr'.
362 local
363 l_expr_list: LINKED_LIST [EXPR_B]
364 do
365 create l_expr_list.make
366 if attached {TUPLE_CONST_B} a_expr as l_tuple then
367 across l_tuple.expressions as i loop
368 l_expr_list.extend (i.item)
369 end
370 if l_tuple.expressions.is_empty then
371 l_expr_list.extend (Void)
372 end
373 else
374 l_expr_list.extend (a_expr)
375 end
376 create Result.make
377 across l_expr_list as k loop
378 if k.item = Void then
379 Result.extend (Void)
380 else
381 Result.extend (translate_individual_expression (k.item))
382 end
383 end
384 end
385
386 translate_individual_expression (a_expr: EXPR_B): IV_EXPRESSION
387 local
388 l_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR
389 do
390 create l_translator.make
391 l_translator.entity_mapping.set_heap (create {IV_ENTITY}.make ("heap", types.heap))
392 l_translator.entity_mapping.set_current (create {IV_ENTITY}.make ("current", types.ref))
393 l_translator.set_context (current_feature, current_type)
394 a_expr.process (l_translator)
395 Result := l_translator.last_expression
396 end
397
398 end

Properties

Name Value
svn:eol-style native
svn:keywords Author Date ID Revision

  ViewVC Help
Powered by ViewVC 1.1.23