/[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 94771 - (show annotations)
Thu Apr 3 12:37:44 2014 UTC (5 years, 6 months ago) by polikarn
File size: 19619 byte(s)
Bugfix: redefinitions now taken into account when calculating replaced model queries.
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_boogie_procedure: detachable IV_PROCEDURE
20 -- Currently generated Boogie procedure (if any).
21
22 feature -- Element change
23
24 set_up_boogie_procedure (a_boogie_name: STRING)
25 -- Set up `current_boogie_procedure'.
26 do
27 current_boogie_procedure := boogie_universe.procedure_named (a_boogie_name)
28 if not attached current_boogie_procedure then
29 create current_boogie_procedure.make (a_boogie_name)
30 boogie_universe.add_declaration (current_boogie_procedure)
31 end
32 ensure
33 current_boogie_procedure_set: attached current_boogie_procedure
34 current_boogie_procedure_named: current_boogie_procedure.name ~ a_boogie_name
35 current_boogie_procedure_added: boogie_universe.procedure_named (a_boogie_name) = current_boogie_procedure
36 end
37
38 feature -- Helper functions: arguments and result
39
40 arguments_of (a_feature: FEATURE_I; a_context: CL_TYPE_A): ARRAYED_LIST [TUPLE [name: STRING; type: CL_TYPE_A; boogie_type: IV_TYPE]]
41 -- List of feature arguments of `a_feature'.
42 require
43 a_feature_attached: attached a_feature
44 a_context_attached: attached a_context
45 local
46 i: INTEGER
47 l_type: CL_TYPE_A
48 do
49 create Result.make (a_feature.argument_count)
50 from i := 1 until i > a_feature.argument_count loop
51 l_type := helper.class_type_in_context (a_feature.arguments.i_th (i), a_context.base_class, a_feature, a_context)
52 Result.extend([
53 a_feature.arguments.item_name (i),
54 l_type,
55 types.for_class_type (l_type)
56 ])
57 i := i + 1
58 end
59 end
60
61 arguments_of_current_feature: like arguments_of
62 -- List of arguments of `current_feature'.
63 require
64 current_feature_set: attached current_feature
65 current_type_set: attached current_type
66 do
67 Result := arguments_of (current_feature, current_type)
68 end
69
70 add_argument_with_property (a_name: STRING; a_type: CL_TYPE_A; a_boogie_type: IV_TYPE)
71 -- Add argument and property to current procedure.
72 require
73 current_procedure_set: attached current_boogie_procedure
74 local
75 l_pre: IV_PRECONDITION
76 do
77 current_boogie_procedure.add_argument (a_name, a_boogie_type)
78 create l_pre.make (types.type_property (a_type, factory.global_heap, factory.entity (a_name, a_boogie_type)))
79 l_pre.set_free
80 l_pre.node_info.set_attribute ("info", "type property for argument " + a_name)
81 current_boogie_procedure.add_contract (l_pre)
82 translation_pool.add_type (a_type)
83 end
84
85 add_result_with_property
86 -- Add result to current procedure.
87 local
88 l_type: CL_TYPE_A
89 l_iv_type: IV_TYPE
90 do
91 if current_feature.has_return_value then
92 l_type := helper.class_type_in_context (current_feature.type, current_type.base_class, current_feature, current_type)
93 l_iv_type := types.for_class_type (l_type)
94 translation_pool.add_type (l_type)
95 current_boogie_procedure.add_result_with_property (
96 "Result",
97 l_iv_type,
98 types.type_property (l_type, factory.global_heap, factory.entity ("Result", l_iv_type)))
99 end
100 end
101
102 feature -- Helper functions: contracts
103
104 contracts_of (a_feature: FEATURE_I; a_type: TYPE_A): TUPLE [pre, post, modifies, reads, decreases: LIST [E2B_ASSERT_ORIGIN]]
105 -- Contracts for feature `a_feature' of type `a_type' separated into preconditions, postconiditons, modify clauses, read clauses, and decreases clauses;
106 -- with their origin class.
107 local
108 l_pre, l_post, l_modifies, l_reads, l_decreases: LINKED_LIST [E2B_ASSERT_ORIGIN]
109 l_class: CLASS_C
110 l_name: STRING_32
111 do
112 create l_pre.make
113 create l_post.make
114 create l_modifies.make
115 create l_reads.make
116 create l_decreases.make
117
118 helper.set_up_byte_context (a_feature, a_type)
119 if attached Context.byte_code as l_byte_code then
120 -- Process pre/post-conditions
121 l_class := a_feature.written_class
122 if l_byte_code.precondition /= Void then
123 across l_byte_code.precondition as p loop
124 l_pre.extend (create {E2B_ASSERT_ORIGIN}.make (p.item, l_class))
125 end
126 end
127 if l_byte_code.postcondition /= Void then
128 across l_byte_code.postcondition as p loop
129 l_post.extend (create {E2B_ASSERT_ORIGIN}.make (p.item, l_class))
130 end
131 end
132 if a_feature.assert_id_set /= Void and not a_type.is_basic then
133 -- Feature has inherited assertions
134 l_byte_code.formulate_inherited_assertions (a_feature.assert_id_set)
135 across Context.inherited_assertion.precondition_list as i loop
136 l_class := Context.inherited_assertion.precondition_types [i.target_index].type.base_class
137 across i.item as p loop
138 l_pre.extend (create {E2B_ASSERT_ORIGIN}.make (p.item, l_class))
139 end
140 end
141
142 across Context.inherited_assertion.postcondition_list as i loop
143 l_class := Context.inherited_assertion.postcondition_types [i.target_index].type.base_class
144 across i.item as p loop
145 l_post.extend (create {E2B_ASSERT_ORIGIN}.make (p.item, l_class))
146 end
147 end
148 end
149 end
150 from
151 l_pre.start
152 until
153 l_pre.after
154 loop
155 if helper.is_clause_reads (l_pre.item.clause) then
156 l_reads.extend (l_pre.item)
157 l_pre.remove
158 elseif helper.is_clause_modify (l_pre.item.clause) then
159 l_modifies.extend (l_pre.item)
160 l_pre.remove
161 elseif helper.is_clause_decreases (l_pre.item.clause) then
162 l_decreases.extend (l_pre.item)
163 l_pre.remove
164 else
165 l_pre.forth
166 end
167 end
168 from
169 l_post.start
170 until
171 l_post.after
172 loop
173 if helper.is_clause_reads (l_post.item.clause) then
174 helper.add_semantic_warning (a_feature, messages.invalid_context_for_special_predicate ("Read"), l_post.item.clause.line_number)
175 l_post.remove
176 elseif helper.is_clause_modify (l_post.item.clause) then
177 helper.add_semantic_warning (a_feature, messages.invalid_context_for_special_predicate ("Modify"), l_post.item.clause.line_number)
178 l_post.remove
179 elseif helper.is_clause_decreases (l_post.item.clause) then
180 helper.add_semantic_warning (a_feature, messages.invalid_context_for_special_predicate ("Decrease"), l_post.item.clause.line_number)
181 l_post.remove
182 else
183 l_post.forth
184 end
185 end
186 Result := [l_pre, l_post, l_modifies, l_reads, l_decreases]
187 end
188
189 contracts_of_current_feature: like contracts_of
190 -- Contracts for `current_feature'.
191 do
192 Result := contracts_of (current_feature, current_type)
193 end
194
195 pre_post_expressions_of (a_feature: FEATURE_I; a_type: CL_TYPE_A; a_mapping: E2B_ENTITY_MAPPING): TUPLE [pre: IV_EXPRESSION; post: IV_EXPRESSION]
196 -- Contracts for feature `a_feature' of type `a_type' as expressions.
197 local
198 l_contracts: like contracts_of
199 l_pre: IV_EXPRESSION
200 l_post: IV_EXPRESSION
201 l_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR
202 do
203 l_contracts := contracts_of (a_feature, a_type)
204
205 create l_translator.make
206 l_translator.set_context (a_feature, a_type)
207 l_translator.copy_entity_mapping (a_mapping)
208
209 l_pre := factory.true_
210 across l_contracts.pre as c loop
211 l_translator.set_origin_class (c.item.origin)
212 helper.set_up_byte_context (c.item.origin.feature_of_rout_id (a_feature.rout_id_set.first),
213 helper.class_type_in_context (c.item.origin.actual_type, c.item.origin, Void, current_type))
214 c.item.clause.process (l_translator)
215 l_pre := factory.and_clean (l_pre, l_translator.last_expression)
216 end
217 l_post := factory.true_
218 across l_contracts.post as c loop
219 l_translator.set_origin_class (c.item.origin)
220 helper.set_up_byte_context (c.item.origin.feature_of_rout_id (a_feature.rout_id_set.first),
221 helper.class_type_in_context (c.item.origin.actual_type, c.item.origin, Void, current_type))
222 c.item.clause.process (l_translator)
223 l_post := factory.and_clean (l_post, l_translator.last_expression)
224 end
225 helper.set_up_byte_context (a_feature, a_type)
226 Result := [l_pre, l_post]
227 end
228
229 modify_expressions_of (a_clauses: LIST [E2B_ASSERT_ORIGIN]; a_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR): TUPLE [full_objects: LIST [IV_EXPRESSION]; partial_objects: LIST [E2B_FRAME_ELEMENT]; model_objects: LIST [E2B_FRAME_ELEMENT]]
230 -- List of fully modified and partially modified objects extracted from modifies clauses `a_clauses'.
231 do
232 Result := [
233 frame_full_objects_of (a_clauses, "modify", a_translator),
234 frame_partial_objects_of (a_clauses, "modify_field", a_translator, False),
235 frame_partial_objects_of (a_clauses, "modify_model", a_translator, True)
236 ]
237 -- Add `closed' to all model frames
238 across Result.model_objects as m loop
239 if across m.item.fields as f all f.item.name /~ "closed" end then
240 m.item.fields.extend (factory.entity ("closed", types.field (types.bool)))
241 end
242 end
243 end
244
245 read_expressions_of (a_clauses: LIST [E2B_ASSERT_ORIGIN]; a_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR): TUPLE [full_objects: LIST [IV_EXPRESSION]; partial_objects: LIST [E2B_FRAME_ELEMENT]; model_objects: LIST [E2B_FRAME_ELEMENT]]
246 -- List of fully modified and partially modified objects extracted from modifies clauses `a_clauses'.
247 do
248 Result := [
249 frame_full_objects_of (a_clauses, "reads", a_translator),
250 frame_partial_objects_of (a_clauses, "reads_field", a_translator, False),
251 frame_partial_objects_of (a_clauses, "reads_model", a_translator, True)
252 ]
253 end
254
255 frame_full_objects_of (a_clauses: LIST [E2B_ASSERT_ORIGIN]; a_function: STRING; a_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR): LIST [IV_EXPRESSION]
256 -- Full object descriptions extracted from `a_clauses' and translated with `a_translator', given as arguments to `a_function'.
257 local
258 l_objects_type: like translate_contained_expressions
259 l_name: STRING_32
260 do
261 create {LINKED_LIST [IV_EXPRESSION]} Result.make
262
263 across
264 a_clauses as i
265 loop
266 if attached {FEATURE_B} i.item.clause.expr as l_call then
267 l_name := names_heap.item_32 (l_call.feature_name_id)
268 if l_name ~ a_function then
269 a_translator.set_origin_class (i.item.origin)
270 l_objects_type := translate_contained_expressions (l_call.parameters.i_th (1).expression, a_translator, True)
271 Result.append (l_objects_type.expressions)
272 end
273 end
274 end
275 end
276
277 frame_partial_objects_of (a_clauses: LIST [E2B_ASSERT_ORIGIN]; a_function: STRING; a_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR; a_check_model: BOOLEAN): LIST [E2B_FRAME_ELEMENT]
278 -- Partial object descriptions extracted from `a_clauses' and translated with `a_translator', given as arguments to `a_function'.
279 local
280 l_fieldnames: LINKED_LIST [STRING_32]
281 l_fields: LINKED_LIST [IV_ENTITY]
282 l_objects_type: like translate_contained_expressions
283 l_name: STRING_32
284 l_type: CL_TYPE_A
285 l_attr, l_to_set, l_new_version: FEATURE_I
286 l_boogie_type: IV_TYPE
287 l_field: IV_ENTITY
288 l_origin: CLASS_C
289 do
290 create {LINKED_LIST [E2B_FRAME_ELEMENT]} Result.make
291
292 across
293 a_clauses as i
294 loop
295 if attached {FEATURE_B} i.item.clause.expr as l_call then
296 l_name := names_heap.item_32 (l_call.feature_name_id)
297 if l_name ~ a_function then
298 a_translator.set_origin_class (i.item.origin)
299 l_objects_type := translate_contained_expressions (l_call.parameters.i_th (2).expression, a_translator, True)
300 create l_fields.make
301
302 if l_objects_type.expressions.first /= Void then
303 l_type := helper.class_type_in_context (l_objects_type.type, i.item.origin, current_feature, current_type)
304
305 create l_fieldnames.make
306 if attached {STRING_B} l_call.parameters.i_th (1).expression as l_string then
307 l_fieldnames.extend (l_string.value)
308 elseif attached {TUPLE_CONST_B} l_call.parameters.i_th (1).expression as l_tuple then
309 across l_tuple.expressions as j loop
310 if attached {STRING_B} j.item as l_string then
311 l_fieldnames.extend (l_string.value)
312 else
313 helper.add_semantic_error (current_feature, messages.first_argument_string_or_tuple, i.item.clause.line_number)
314 end
315 end
316 else
317 helper.add_semantic_error (current_feature, messages.first_argument_string_or_tuple, i.item.clause.line_number)
318 end
319
320 l_origin := helper.class_type_in_context (
321 l_objects_type.type,
322 i.item.origin,
323 current_feature,
324 helper.class_type_from_class (i.item.origin, current_type)).base_class
325 across l_fieldnames as f loop
326 if a_check_model then
327 l_attr := l_origin.feature_named_32 (f.item)
328 if attached l_attr and then helper.is_model_query (l_origin, l_attr) then
329 l_new_version := l_type.base_class.feature_of_rout_id_set (l_attr.rout_id_set)
330 l_field := helper.field_from_attribute (l_new_version, l_type)
331 l_fields.extend (l_field)
332 -- Add replaced model queries
333 across helper.replaced_model_queries (l_new_version, l_type.base_class) as m loop
334 l_field := helper.field_from_attribute (m.item, l_type)
335 if across l_fields as fi all not fi.item.same_expression (l_field) end then
336 l_fields.extend (l_field)
337 end
338 end
339 -- Add replacing model queries
340 across helper.replacing_model_queries (l_attr, l_origin, l_type.base_class) as m loop
341 l_field := helper.field_from_attribute (m.item, l_type)
342 if across l_fields as fi all not fi.item.same_expression (l_field) end then
343 l_fields.extend (l_field)
344 end
345 end
346 else
347 helper.add_semantic_error (current_feature, messages.unknown_model (f.item, l_origin.name_in_upper), i.item.clause.line_number)
348 end
349 else
350 l_attr := helper.attribute_from_string (f.item, l_type, l_origin, current_feature, i.item.clause.line_number)
351 if attached l_attr then
352 l_fields.extend (helper.field_from_attribute (l_attr, l_type))
353 end
354 end
355 end
356 end
357 Result.extend (create {E2B_FRAME_ELEMENT}.make (l_objects_type.expressions, l_fields, l_objects_type.type, i.item.origin))
358 end
359 else
360 check internal_error: False end
361 end
362 end
363 end
364
365 is_pure (a_mods: like modify_expressions_of): BOOLEAN
366 -- Is `a_mods' an empty frame?
367 do
368 Result := (a_mods.full_objects.is_empty or else a_mods.full_objects.first = Void) and
369 (a_mods.partial_objects.is_empty or else a_mods.partial_objects.first.objects.first = Void) and
370 (a_mods.model_objects.is_empty or else a_mods.model_objects.first.objects.first = Void)
371 end
372
373 frame_definition (a_mods: like modify_expressions_of; a_lhs: IV_EXPRESSION): IV_FORALL
374 -- Expression that claims that `a_lhs' is the frame encoded in `a_mods'
375 -- (forall o, f :: a_lhs[o, f] <==> is_partially_modifiable[o, f] || is_model_modifiable[o, f] || is_fully_modifiable[o])
376 local
377 l_expr, l_f_conjunct: IV_EXPRESSION
378 l_type_var: IV_VAR_TYPE
379 l_o, l_f: IV_ENTITY
380 l_access: IV_MAP_ACCESS
381 l_written_type, l_type: CL_TYPE_A
382 r: E2B_FRAME_ELEMENT
383 do
384 create l_type_var.make_fresh
385 create l_o.make ("$o", types.ref)
386 create l_f.make ("$f", types.field (l_type_var))
387 create l_access.make (a_lhs, << l_o, l_f >>)
388 l_expr := factory.false_
389
390 -- Axiom rhs: a big disjunction
391 -- Go over partially modifiable objects
392 across a_mods.partial_objects as restriction loop
393 l_f_conjunct := factory.false_
394 across restriction.item.fields as f loop
395 l_f_conjunct := factory.or_clean (l_f_conjunct, factory.equal (l_f, f.item))
396 end
397 l_expr := factory.or_clean (l_expr, factory.and_ (is_object_in_frame (l_o, restriction.item.objects), l_f_conjunct))
398 end
399 -- Go over model-modifiable objects
400 across a_mods.model_objects as restriction loop
401 r := restriction.item
402 -- The type of the objects as seen where the frame clause was written
403 l_written_type := helper.class_type_in_context (r.type, r.origin, current_feature, helper.class_type_from_class (r.origin, current_type))
404 -- The type of the objects as seen in the `current_type'
405 l_type := helper.class_type_in_context (r.type, r.origin, current_feature, current_type)
406 -- Either `l_f' is not a model query in `l_type'
407 l_f_conjunct := factory.not_ (factory.function_call ("IsModelField", << l_f, factory.type_value (l_type) >>, types.bool))
408 -- Or it is one of `r.fields'
409 across r.fields as f loop
410 l_f_conjunct := factory.or_ (l_f_conjunct,factory.equal (l_f, f.item))
411 end
412 l_expr := factory.or_clean (l_expr, factory.and_ (is_object_in_frame (l_o, r.objects), l_f_conjunct))
413 end
414 -- Go over fully modifiable objects
415 l_expr := factory.or_clean (l_expr, is_object_in_frame (l_o, a_mods.full_objects))
416 -- Finally create the quantifier
417 create Result.make (factory.equiv (l_access, l_expr))
418 Result.add_type_variable (l_type_var.name)
419 Result.add_bound_variable (l_o)
420 Result.add_bound_variable (l_f)
421 Result.add_trigger (l_access)
422 end
423
424 is_object_in_frame (a_var: IV_EXPRESSION; a_objects: LIST [IV_EXPRESSION]): IV_EXPRESSION
425 -- Expression stating that `a_var' is one of `a_objects',
426 -- where elements of `a_objects' can be individual objects or sets.
427 local
428 l_disjunct: IV_EXPRESSION
429 do
430 Result := factory.false_
431 across a_objects as o loop
432 if o.item = Void then
433 l_disjunct := factory.false_
434 elseif o.item.type ~ types.ref then
435 l_disjunct := factory.equal (a_var, o.item)
436 else
437 check o.item.type ~ types.set (types.ref) end
438 l_disjunct := factory.map_access (o.item, << a_var >>)
439 end
440 Result := factory.or_clean (Result, l_disjunct)
441 end
442 end
443
444 decreases_expressions_of (a_clauses: LIST [E2B_ASSERT_ORIGIN]; a_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR): LIST [IV_EXPRESSION]
445 -- List of variants extracted from decreases clauses `a_clauses'.
446 do
447 create {LINKED_LIST [IV_EXPRESSION]} Result.make
448 across
449 a_clauses as i
450 loop
451 if attached {FEATURE_B} i.item.clause.expr as l_call then
452 a_translator.set_origin_class (i.item.origin)
453 Result.append (translate_contained_expressions (l_call.parameters.i_th (1).expression, a_translator, False).expressions)
454 else
455 check internal_error: False end
456 end
457 end
458 end
459
460 translate_contained_expressions (a_expr: EXPR_B; a_translator: E2B_EXPRESSION_TRANSLATOR; convert_to_set: BOOLEAN): TUPLE [expressions: LINKED_LIST [IV_EXPRESSION]; type: TYPE_A]
461 -- Translate expressions in `a_expr' using `a_translator'; if `convert_to_set', convert all expressions of logical types to sets.
462 local
463 l_expr_list: LINKED_LIST [EXPR_B]
464 l_expressions: LINKED_LIST [IV_EXPRESSION]
465 l_type: TYPE_A
466 do
467 create l_expr_list.make
468 if attached {TUPLE_CONST_B} a_expr as l_tuple then
469 across l_tuple.expressions as i loop
470 l_expr_list.extend (i.item)
471 end
472 if l_tuple.expressions.is_empty then
473 l_expr_list.extend (Void)
474 end
475 else
476 l_expr_list.extend (a_expr)
477 end
478 create l_expressions.make
479 across l_expr_list as k loop
480 if k.item = Void then
481 l_expressions.extend (Void)
482 elseif convert_to_set and helper.is_class_logical (a_translator.class_type_in_current_context (k.item.type).base_class) then
483 a_translator.process_as_set (k.item, types.ref)
484 l_expressions.extend (a_translator.last_expression)
485 l_type := a_translator.last_set_content_type
486 else
487 k.item.process (a_translator)
488 l_expressions.extend (a_translator.last_expression)
489 l_type := k.item.type
490 end
491 end
492 Result := [l_expressions, l_type]
493 end
494
495 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23