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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 93378 - (show annotations)
Thu Nov 14 15:57:08 2013 UTC (5 years, 11 months ago) by julian
File size: 29855 byte(s)
AutoProof: continued ownership implementation.

1 note
2 description: "[
3 TODO
4 ]"
5 date: "$Date$"
6 revision: "$Revision$"
7
8 deferred class
9 E2B_EXPRESSION_TRANSLATOR
10
11 inherit
12
13 E2B_VISITOR
14 redefine
15 process_agent_call_b,
16 process_argument_b,
17 process_array_const_b,
18 process_attribute_b,
19 process_bin_and_b,
20 process_bin_and_then_b,
21 process_bin_div_b,
22 process_bin_eq_b,
23 process_bin_free_b,
24 process_bin_ge_b,
25 process_bin_gt_b,
26 process_bin_implies_b,
27 process_bin_le_b,
28 process_bin_lt_b,
29 process_bin_minus_b,
30 process_bin_ne_b,
31 process_bin_mod_b,
32 process_bin_or_b,
33 process_bin_or_else_b,
34 process_bin_plus_b,
35 process_bin_power_b,
36 process_bin_slash_b,
37 process_bin_star_b,
38 process_bin_tilde_b,
39 process_bin_xor_b,
40 process_bool_const_b,
41 process_char_const_b,
42 process_char_val_b,
43 process_constant_b,
44 process_creation_expr_b,
45 process_current_b,
46 process_external_b,
47 process_feature_b,
48 process_if_expression_b,
49 process_int64_val_b,
50 process_int_val_b,
51 process_integer_constant,
52 process_local_b,
53 process_loop_expr_b,
54 process_nat64_val_b,
55 process_nat_val_b,
56 process_nested_b,
57 process_object_test_b,
58 process_object_test_local_b,
59 process_parameter_b,
60 process_paran_b,
61 process_result_b,
62 process_real_const_b,
63 process_routine_creation_b,
64 process_string_b,
65 process_tuple_access_b,
66 process_tuple_const_b,
67 process_type_expr_b,
68 process_un_free_b,
69 process_un_minus_b,
70 process_un_not_b,
71 process_un_old_b,
72 process_void_b
73 end
74
75 E2B_SHARED_CONTEXT
76 export {NONE} all end
77
78 IV_SHARED_TYPES
79
80 IV_SHARED_FACTORY
81
82 SHARED_BYTE_CONTEXT
83
84 COMPILER_EXPORTER
85
86 feature {NONE} -- Initialization
87
88 make
89 -- Initialize translator.
90 do
91 reset
92 end
93
94 feature -- Access
95
96 entity_mapping: E2B_ENTITY_MAPPING
97 -- Entity mapping used for translation.
98
99 last_expression: IV_EXPRESSION
100 -- Last generated expression.
101
102 context_feature: FEATURE_I
103 -- Context of expression.
104
105 context_type: TYPE_A
106 -- Context of expression.
107
108 current_target: IV_EXPRESSION
109 -- Current target.
110
111 current_target_type: TYPE_A
112 -- Type of current target type.
113
114 locals_map: HASH_TABLE [IV_EXPRESSION, INTEGER]
115 -- Mapping of object test locals to entities.
116
117 across_handler_map: HASH_TABLE [E2B_ACROSS_HANDLER, INTEGER]
118 -- Mapping of object test locals from across loops to across handlers.
119
120 feature -- Element change
121
122 set_last_expression (a_expression: IV_EXPRESSION)
123 -- Set `last_expression' to `a_expression'.
124 do
125 last_expression := a_expression
126 end
127
128 feature -- Basic operations
129
130 set_context (a_feature: FEATURE_I; a_type: TYPE_A)
131 -- Set context of expression to `a_feature' in type `a_type'.
132 require
133 a_type_attached: attached a_type
134 do
135 context_feature := a_feature
136 context_type := a_type
137 current_target_type := a_type
138 current_target := entity_mapping.current_expression
139 if a_feature /= Void and then a_feature.has_return_value then
140 entity_mapping.set_default_result (a_feature.type.instantiated_in (current_target_type))
141 end
142 end
143
144 copy_entity_mapping (a_entity_mapping: E2B_ENTITY_MAPPING)
145 -- Set `entity_mapping' to a copy of `a_entity_mapping'.
146 do
147 create entity_mapping.make_copy (a_entity_mapping)
148 current_target := entity_mapping.current_expression
149 end
150
151 reset
152 -- Reset expression translator.
153 do
154 last_expression := Void
155 context_feature := Void
156 context_type := Void
157 current_target := Void
158 current_target_type := Void
159 create entity_mapping.make
160 create locals_map.make (10)
161 create across_handler_map.make (10)
162 create safety_check_condition.make
163 create parameters_stack.make
164 end
165
166 feature -- Visitors
167
168 process_agent_call_b (a_node: AGENT_CALL_B)
169 -- <Precursor>
170 do
171 last_expression := dummy_node (a_node.type)
172 end
173
174 process_argument_b (a_node: ARGUMENT_B)
175 -- <Precursor>
176 local
177 l_name: STRING
178 l_type: IV_TYPE
179 do
180 last_expression := entity_mapping.argument (context_feature, context_type, a_node.position)
181 end
182
183 process_array_const_b (a_node: ARRAY_CONST_B)
184 -- <Precursor>
185 do
186 last_expression := dummy_node (a_node.type)
187 end
188
189 process_attribute_b (a_node: ATTRIBUTE_B)
190 -- <Precursor>
191 local
192 l_feature: FEATURE_I
193 do
194 l_feature := helper.feature_for_call_access (a_node, current_target_type)
195
196 process_attribute_call (l_feature)
197 end
198
199 process_binary (a_node: BINARY_B; a_operator: STRING)
200 -- Process binary node `a_node' with operator `a_operator'.
201 local
202 l_left, l_right: IV_EXPRESSION
203 l_type: IV_TYPE
204 l_fcall: IV_FUNCTION_CALL
205 l_fname: STRING
206 do
207 safe_process (a_node.left)
208 l_left := last_expression
209 safe_process (a_node.right)
210 l_right := last_expression
211 l_type := types.for_type_a (a_node.type)
212
213 if l_left.type.is_set then
214 (create {E2B_CUSTOM_MML_HANDLER}).handle_binary (Current, l_left, l_right, a_operator)
215 else
216 if is_in_quantifier then
217 if a_operator ~ "+" then
218 last_expression := factory.function_call ("add", << l_left, l_right >>, types.int)
219 elseif a_operator ~ "-" then
220 last_expression := factory.function_call ("subtract", << l_left, l_right >>, types.int)
221 elseif a_operator ~ "*" then
222 last_expression := factory.function_call ("multiply", << l_left, l_right >>, types.int)
223 else
224 create {IV_BINARY_OPERATION} last_expression.make (l_left, a_operator, l_right, l_type)
225 end
226 else
227 create {IV_BINARY_OPERATION} last_expression.make (l_left, a_operator, l_right, l_type)
228 end
229 if
230 options.is_checking_overflow and then
231 (a_node.left.type.is_integer or a_node.left.type.is_natural) and then
232 (a_operator ~ "+" or a_operator ~ "-")
233 then
234 -- Arithmetic operation
235 l_fname := "is_" + a_node.left.type.associated_class.name.as_lower
236 create l_fcall.make (l_fname, types.bool)
237 l_fcall.add_argument (last_expression)
238 add_safety_check (l_fcall, "overflow", Void)
239 end
240 end
241 end
242
243 process_binary_semistrict (a_node: BINARY_B; a_operator: STRING; a_positive: BOOLEAN)
244 -- Process binary node `a_node' with operator `a_operator'.
245 -- If `a_positive' is set, then the left expression has to `true' to trigger
246 -- evaluation of right expression, otherwise it has to be false.
247 local
248 l_left, l_right: IV_EXPRESSION
249 l_type: IV_TYPE
250 l_fcall: IV_FUNCTION_CALL
251 l_fname: STRING
252 l_safety_check_condition: IV_EXPRESSION
253 l_not: IV_UNARY_OPERATION
254 do
255 safe_process (a_node.left)
256 l_left := last_expression
257
258 if a_positive then
259 l_safety_check_condition := l_left
260 else
261 l_safety_check_condition := factory.not_ (l_left)
262 end
263 if not safety_check_condition.is_empty then
264 l_safety_check_condition := factory.and_ (safety_check_condition.item, l_safety_check_condition)
265 end
266 safety_check_condition.extend (l_safety_check_condition)
267
268 safe_process (a_node.right)
269 l_right := last_expression
270 l_type := types.for_type_a (a_node.type)
271 create {IV_BINARY_OPERATION} last_expression.make (l_left, a_operator, l_right, l_type)
272
273 safety_check_condition.remove
274 end
275
276 process_binary_infix (a_node: BINARY_B)
277 -- Process binary infix node `a_node'.
278 do
279 a_node.nested_b.process (Current)
280 end
281
282 process_bin_and_b (a_node: BIN_AND_B)
283 -- <Precursor>
284 do
285 process_binary (a_node, "&&")
286 end
287
288 process_bin_and_then_b (a_node: B_AND_THEN_B)
289 -- <Precursor>
290 do
291 process_binary_semistrict (a_node, "&&", True)
292 end
293
294 process_bin_div_b (a_node: BIN_DIV_B)
295 -- <Precursor>
296 do
297 if a_node.type.is_real_32 or a_node.type.is_real_64 then
298 process_binary (a_node, "/")
299 elseif a_node.is_built_in then
300 process_binary (a_node, "div")
301 else
302 process_binary_infix (a_node)
303 end
304 end
305
306 process_bin_eq_b (a_node: BIN_EQ_B)
307 -- <Precursor>
308 do
309 process_binary (a_node, "==")
310 end
311
312 process_bin_free_b (a_node: BIN_FREE_B)
313 -- <Precursor>
314 do
315 process_binary_infix (a_node)
316 end
317
318 process_bin_ge_b (a_node: BIN_GE_B)
319 -- <Precursor>
320 do
321 if a_node.is_built_in then
322 process_binary (a_node, ">=")
323 else
324 process_binary_infix (a_node)
325 end
326 end
327
328 process_bin_gt_b (a_node: BIN_GT_B)
329 -- <Precursor>
330 do
331 if a_node.is_built_in then
332 process_binary (a_node, ">")
333 else
334 process_binary_infix (a_node)
335 end
336 end
337
338 process_bin_implies_b (a_node: B_IMPLIES_B)
339 -- <Precursor>
340 do
341 process_binary_semistrict (a_node, "==>", True)
342 end
343
344 process_bin_le_b (a_node: BIN_LE_B)
345 -- <Precursor>
346 do
347 if a_node.is_built_in then
348 process_binary (a_node, "<=")
349 else
350 process_binary_infix (a_node)
351 end
352 end
353
354 process_bin_lt_b (a_node: BIN_LT_B)
355 -- <Precursor>
356 do
357 if a_node.is_built_in then
358 process_binary (a_node, "<")
359 else
360 process_binary_infix (a_node)
361 end
362 end
363
364 process_bin_minus_b (a_node: BIN_MINUS_B)
365 -- <Precursor>
366 do
367 if a_node.is_built_in then
368 process_binary (a_node, "-")
369 else
370 process_binary_infix (a_node)
371 end
372 end
373
374 process_bin_mod_b (a_node: BIN_MOD_B)
375 -- <Precursor>
376 do
377 process_binary (a_node, "mod")
378 end
379
380 process_bin_ne_b (a_node: BIN_NE_B)
381 -- <Precursor>
382 do
383 process_binary (a_node, "!=")
384 end
385
386 process_bin_or_b (a_node: BIN_OR_B)
387 -- <Precursor>
388 do
389 process_binary (a_node, "||")
390 end
391
392 process_bin_or_else_b (a_node: B_OR_ELSE_B)
393 -- <Precursor>
394 do
395 process_binary_semistrict (a_node, "||", False)
396 end
397
398 process_bin_plus_b (a_node: BIN_PLUS_B)
399 -- <Precursor>
400 do
401 if a_node.is_built_in then
402 process_binary (a_node, "+")
403 else
404 process_binary_infix (a_node)
405 end
406 end
407
408 process_bin_power_b (a_node: BIN_POWER_B)
409 -- <Precursor>
410 do
411 if a_node.is_built_in then
412 process_binary (a_node, "**")
413 else
414 process_binary_infix (a_node)
415 end
416 end
417
418 process_bin_slash_b (a_node: BIN_SLASH_B)
419 -- <Precursor>
420 do
421 if a_node.is_built_in then
422 process_binary (a_node, "/")
423 else
424 process_binary_infix (a_node)
425 end
426 end
427
428 process_bin_star_b (a_node: BIN_STAR_B)
429 -- <Precursor>
430 do
431 if a_node.is_built_in then
432 process_binary (a_node, "*")
433 else
434 process_binary_infix (a_node)
435 end
436 end
437
438 process_bin_xor_b (a_node: BIN_XOR_B)
439 -- <Precursor>
440 do
441 process_binary (a_node, "!=")
442 end
443
444 process_bin_tilde_b (a_node: BIN_TILDE_B)
445 -- <Precursor>
446 do
447 -- TODO: handle "is_equal"
448 process_binary (a_node, "==")
449 end
450
451 process_bool_const_b (a_node: BOOL_CONST_B)
452 -- <Precursor>
453 do
454 if a_node.value then
455 last_expression := factory.true_
456 else
457 last_expression := factory.false_
458 end
459 end
460
461 process_current_b (a_node: CURRENT_B)
462 -- <Precursor>
463 local
464 l_type: LIKE_CURRENT
465 do
466 last_expression := entity_mapping.current_expression
467 end
468
469 process_char_const_b (a_node: CHAR_CONST_B)
470 -- <Precursor>
471 do
472 last_expression := factory.int_value (a_node.value.code)
473 end
474
475 process_char_val_b (a_node: CHAR_VAL_B)
476 -- <Precursor>
477 do
478 last_expression := factory.int_value (a_node.value.code)
479 end
480
481 process_constant_b (a_node: CONSTANT_B)
482 -- <Precursor>
483 local
484 l_bool: BOOL_VALUE_I
485 l_char: CHAR_VALUE_I
486 do
487 if a_node.value.is_boolean then
488 l_bool ?= a_node.value
489 check l_bool /= Void end
490 if l_bool.boolean_value then
491 last_expression := factory.true_
492 else
493 last_expression := factory.false_
494 end
495 elseif a_node.value.is_integer or a_node.value.is_numeric then
496 create {IV_VALUE} last_expression.make (a_node.value.string_value, types.int)
497 elseif a_node.value.is_character then
498 l_char ?= a_node.value
499 check l_char /= Void end
500 last_expression := factory.int_value (l_char.character_value.code)
501 elseif a_node.value.is_real then
502 last_expression := dummy_node (a_node.type)
503 else
504 last_expression := dummy_node (a_node.type)
505 end
506 end
507
508 process_creation_expr_b (a_node: CREATION_EXPR_B)
509 -- <Precursor>
510 do
511 last_expression := dummy_node (a_node.type)
512 end
513
514 process_external_b (a_node: EXTERNAL_B)
515 -- <Precursor>
516 local
517 l_feature: FEATURE_I
518 l_current_type: TYPE_A
519 l_handler: E2B_CUSTOM_CALL_HANDLER
520 do
521 l_current_type := current_target_type
522
523 current_target_type := a_node.type
524 l_feature := helper.feature_for_call_access (a_node, current_target_type)
525 check feature_valid: l_feature /= Void end
526 l_handler := translation_mapping.handler_for_call (current_target_type, l_feature)
527 if l_handler /= Void then
528 process_special_routine_call (l_handler, l_feature, a_node.parameters)
529 else
530 process_routine_call (l_feature, a_node.parameters, False)
531 end
532
533 current_target_type := l_current_type
534 end
535
536 process_feature_b (a_node: FEATURE_B)
537 -- <Precursor>
538 local
539 l_feature: FEATURE_I
540 l_constant: CONSTANT_I
541 l_handler: E2B_CUSTOM_CALL_HANDLER
542 do
543 l_feature := helper.feature_for_call_access (a_node, current_target_type)
544 check feature_valid: l_feature /= Void end
545
546 if l_feature.is_attribute then
547 process_attribute_call (l_feature)
548 elseif l_feature.is_constant then
549 l_constant ?= l_feature
550 check l_constant /= Void end
551 process_constant_call (l_constant)
552 elseif l_feature.is_routine then
553 l_handler := translation_mapping.handler_for_call (current_target_type, l_feature)
554 if l_handler /= Void then
555 process_special_routine_call (l_handler, l_feature, a_node.parameters)
556 else
557 process_routine_call (l_feature, a_node.parameters, False)
558 end
559 else
560 -- TODO: what else is there?
561 check False end
562 end
563 end
564
565 process_if_expression_b (a_node: IF_EXPRESSION_B)
566 -- <Precursor>
567 local
568 l_cond, l_then, l_else: IV_EXPRESSION
569 do
570 check a_node.elsif_list = Void or else a_node.elsif_list.is_empty end
571
572 safe_process (a_node.condition)
573 l_cond := last_expression
574 safe_process (a_node.then_expression)
575 l_then := last_expression
576 safe_process (a_node.else_expression)
577 l_else := last_expression
578 create {IV_CONDITIONAL_EXPRESSION} last_expression.make_if_then_else (l_cond, l_then, l_else)
579 end
580
581 process_int64_val_b (a_node: INT64_VAL_B)
582 -- <Precursor>
583 do
584 last_expression := factory.int64_value (a_node.value)
585 end
586
587 process_int_val_b (a_node: INT_VAL_B)
588 -- <Precursor>
589 do
590 last_expression := factory.int_value (a_node.value)
591 end
592
593 process_integer_constant (a_node: INTEGER_CONSTANT)
594 -- <Precursor>
595 do
596 if attached {INTEGER_A} a_node.type then
597 last_expression := factory.int64_value (a_node.integer_64_value)
598 else
599 last_expression := factory.nat64_value (a_node.natural_64_value)
600 end
601 end
602
603 process_local_b (a_node: LOCAL_B)
604 -- <Precursor>
605 local
606 l_name: STRING
607 l_type: IV_TYPE
608 do
609 last_expression := entity_mapping.local_ (a_node.position)
610 end
611
612 process_loop_expr_b (a_node: LOOP_EXPR_B)
613 -- <Precursor>
614 local
615 l_assign: ASSIGN_B
616 l_object_test_local: OBJECT_TEST_LOCAL_B
617 l_nested: NESTED_B
618 l_access: ACCESS_EXPR_B
619 l_bin_free: BIN_FREE_B
620 l_name: STRING
621 l_across_handler: E2B_ACROSS_HANDLER
622 do
623 l_assign ?= a_node.iteration_code.first
624 check l_assign /= Void end
625 l_object_test_local ?= l_assign.target
626 check l_object_test_local /= Void end
627 l_nested ?= l_assign.source
628 check l_nested /= Void end
629 l_access ?= l_nested.target
630 check l_access /= Void end
631
632 l_name := l_nested.target.type.associated_class.name_in_upper
633 if l_name ~ "ARRAY" then
634 create {E2B_ARRAY_ACROSS_HANDLER} l_across_handler.make (Current, a_node, l_nested.target, l_object_test_local)
635 elseif l_name ~ "INTEGER_INTERVAL" then
636 l_bin_free ?= l_access.expr
637 check l_bin_free /= Void end
638 create {E2B_INTERVAL_ACROSS_HANDLER} l_across_handler.make (Current, a_node, l_bin_free, l_object_test_local)
639 elseif l_name ~ "MML_SET" then
640 create {E2B_SET_ACROSS_HANDLER} l_across_handler.make (Current, a_node, l_nested.target, l_object_test_local)
641 else
642 last_expression := dummy_node (a_node.type)
643 end
644
645 is_in_quantifier := True
646
647 if attached l_across_handler then
648 across_handler_map.put (l_across_handler, l_object_test_local.position)
649 l_across_handler.handle_across_expression (a_node)
650 across_handler_map.remove (l_object_test_local.position)
651 end
652
653 is_in_quantifier := False
654 end
655
656 process_nat64_val_b (a_node: NAT64_VAL_B)
657 -- <Precursor>
658 do
659 create {IV_VALUE} last_expression.make (a_node.value.out, types.int)
660 end
661
662 process_nat_val_b (a_node: NAT_VAL_B)
663 -- <Precursor>
664 do
665 create {IV_VALUE} last_expression.make (a_node.value.out, types.int)
666 end
667
668 process_nested_b (a_node: NESTED_B)
669 -- <Precursor>
670 local
671 l_temp_expression: IV_EXPRESSION
672 l_target: IV_EXPRESSION
673 l_target_name: STRING
674 l_target_type: TYPE_A
675 l_formal: FORMAL_A
676
677 l_object_test_local: OBJECT_TEST_LOCAL_B
678 l_across_handler: E2B_ACROSS_HANDLER
679 l_feature: FEATURE_B
680 l_nested: NESTED_B
681 l_call: IV_FUNCTION_CALL
682 l_info: IV_ASSERTION_INFORMATION
683 l_handler: E2B_CUSTOM_NESTED_HANDLER
684 l_name: STRING
685 do
686 l_handler := translation_mapping.handler_for_nested (a_node)
687 l_object_test_local ?= a_node.target
688 if l_object_test_local /= Void and then across_handler_map.has (l_object_test_local.position) then
689 -- Special mapping of object test local in across loop
690 l_across_handler := across_handler_map.item (l_object_test_local.position)
691 l_nested ?= a_node.message
692 if l_nested /= Void then
693 l_feature ?= l_nested.target
694 else
695 l_feature ?= a_node.message
696 end
697 check l_feature /= Void end
698 l_name := l_feature.feature_name.as_lower
699 if l_name ~ "item" then
700 l_across_handler.handle_call_item (Void)
701 elseif l_name ~ "index" or l_name ~ "cursor_index" then
702 l_across_handler.handle_call_cursor_index (Void)
703 elseif l_name ~ "after" then
704 l_across_handler.handle_call_after (Void)
705 elseif l_name ~ "is_wrapped" or l_name ~ "is_open" then
706 last_expression := dummy_node (a_node.type)
707 else
708 check False end
709 last_expression := dummy_node (a_node.type)
710 end
711 if l_nested /= Void then
712 l_target := current_target
713 l_target_type := current_target_type
714
715 current_target := last_expression
716 current_target_type := l_nested.target.type
717 l_nested.message.process (Current)
718
719 current_target := l_target
720 current_target_type := l_target_type
721 end
722 elseif l_handler /= Void then
723 if attached {E2B_BODY_EXPRESSION_TRANSLATOR} Current as t then
724 l_handler.handle_nested_in_body (t, a_node)
725 elseif attached {E2B_CONTRACT_EXPRESSION_TRANSLATOR} Current as t then
726 l_handler.handle_nested_in_contract (t, a_node)
727 else
728 check False end
729 end
730 if last_expression = Void then
731 last_expression := dummy_node (a_node.type)
732 end
733 else
734 l_temp_expression := last_expression
735
736 -- Evaluate target
737 safe_process (a_node.target)
738
739 -- Use target as new `Current' reference
740 l_target := current_target
741 l_target_type := current_target_type
742 current_target := last_expression
743 if a_node.target.type.is_like_current then
744 current_target_type := l_target_type
745 else
746 current_target_type := a_node.target.type.deep_actual_type
747 end
748 check not current_target_type.is_like end
749 if current_target_type.is_formal then
750 l_formal ?= current_target_type
751 current_target_type := l_target_type.associated_class.constraint (l_formal.position)
752 end
753
754 -- Check if target is attached;
755 -- skip if target is expanded or a mathematical type
756 if not (current_target_type.is_expanded or types.is_mml_type (current_target_type)) then
757 translation_pool.add_type (current_target_type)
758 create l_call.make ("attached", types.bool)
759 l_call.add_argument (entity_mapping.heap)
760 l_call.add_argument (current_target)
761 l_call.add_argument (create {IV_VALUE}.make (name_translator.boogie_name_for_type (current_target_type), types.type))
762 add_safety_check (l_call, "attached", "implicit_attachment")
763 end
764
765 -- Evaluate message with original expression
766 -- if attached {CL_TYPE_A} current_target_type as l_cl_type then
767 -- if not l_cl_type.has_associated_class_type (Void) then
768 -- l_cl_type.associated_class.update_types (l_cl_type)
769 -- end
770 -- context.change_class_type_context (
771 -- l_cl_type.associated_class_type (Void),
772 -- l_cl_type,
773 -- l_cl_type.associated_class_type (Void),
774 -- l_cl_type)
775 -- end
776
777 -- helper.set_up_byte_context (Void, current_target_type)
778 -- helper.set_up_byte_context_type (current_target_type, context_type)
779 last_expression := l_temp_expression
780 safe_process (a_node.message)
781
782 -- Restore `Current' reference
783 -- if attached {CL_TYPE_A} current_target_type as l_cl_type then
784 -- if context.is_class_type_changed then
785 -- context.restore_class_type_context
786 -- else
787 -- -- TODO: should never happen, but does
788 -- end
789 -- end
790 current_target := l_target
791 current_target_type := l_target_type
792 -- helper.set_up_byte_context (Void, current_target_type)
793 -- helper.set_up_byte_context_type (current_target_type, context_type)
794 end
795 end
796
797 process_object_test_b (a_node: OBJECT_TEST_B)
798 -- <Precursor>
799 local
800 l_type_check: IV_BINARY_OPERATION
801 l_expr: IV_EXPRESSION
802 do
803 safe_process (a_node.expression)
804 l_expr := last_expression
805 if a_node.is_void_check then
806 last_expression := factory.not_equal (l_expr, factory.void_)
807 else
808 check attached a_node.info end
809 -- Normalize integer types
810 if a_node.info.type_to_create.is_integer or a_node.info.type_to_create.is_natural then
811 l_type_check := factory.sub_type (factory.type_of (l_expr), create {IV_ENTITY}.make ("INTEGER", types.type))
812 else
813 l_type_check := factory.sub_type (factory.type_of (l_expr), factory.type_value (a_node.info.type_to_create))
814 end
815 last_expression := factory.and_ (factory.not_equal (l_expr, factory.void_), l_type_check)
816 end
817 if attached a_node.target then
818 -- Check for possible unboxing of basic types
819 if a_node.expression.type.is_reference then
820 if a_node.target.type.is_boolean then
821 l_expr := factory.function_call ("unboxed_bool", << l_expr >>, types.bool)
822 elseif a_node.target.type.is_integer or a_node.target.type.is_natural then
823 l_expr := factory.function_call ("unboxed_int", << l_expr >>, types.int)
824 end
825 end
826 locals_map.force (l_expr, a_node.target.position)
827 end
828 end
829
830 process_object_test_local_b (a_node: OBJECT_TEST_LOCAL_B)
831 -- <Precursor>
832 do
833 if locals_map.has_key (a_node.position) then
834 last_expression := locals_map.item (a_node.position)
835 else
836 check False end
837 last_expression := dummy_node (a_node.type)
838 end
839 end
840
841 process_parameter_b (a_node: PARAMETER_B)
842 -- <Precursor>
843 local
844 l_context_type: CL_TYPE_A
845 l_target: IV_EXPRESSION
846 l_target_type: TYPE_A
847 l_last_expression: IV_EXPRESSION
848 do
849 check not parameters_stack.is_empty end
850
851 -- Process arguments in context of feature
852 l_target := current_target
853 l_target_type := current_target_type
854 l_last_expression := last_expression
855
856 current_target := entity_mapping.current_expression
857 current_target_type := context_type
858 last_expression := Void
859
860 safe_process (a_node.expression)
861 parameters_stack.item.extend (last_expression)
862
863 last_expression := l_last_expression
864 current_target := l_target
865 current_target_type := l_target_type
866 end
867
868 process_paran_b (a_node: PARAN_B)
869 -- <Precursor>
870 do
871 safe_process (a_node.expr)
872 end
873
874 process_result_b (a_node: RESULT_B)
875 -- <Precursor>
876 local
877 l_name: STRING
878 l_type: IV_TYPE
879 do
880 last_expression := entity_mapping.result_expression
881 end
882
883 process_real_const_b (a_node: REAL_CONST_B)
884 -- <Precursor>
885 do
886 create {IV_VALUE} last_expression.make (a_node.value, types.real)
887 end
888
889 process_routine_creation_b (a_node: ROUTINE_CREATION_B)
890 -- <Precursor>
891 do
892 last_expression := dummy_node (a_node.type)
893 end
894
895 process_string_b (a_node: STRING_B)
896 -- <Precursor>
897 do
898 last_expression := dummy_node (a_node.type)
899 end
900
901 process_tuple_access_b (a_node: TUPLE_ACCESS_B)
902 -- <Precursor>
903 local
904 l_call: IV_FUNCTION_CALL
905 do
906 last_expression := factory.function_call (
907 "fun.TUPLE.item",
908 <<
909 entity_mapping.heap,
910 current_target,
911 factory.int_value (a_node.position)
912 >>,
913 types.generic_type)
914 end
915
916 process_tuple_const_b (a_node: TUPLE_CONST_B)
917 -- <Precursor>
918 do
919 last_expression := dummy_node (a_node.type)
920 end
921
922 process_type_expr_b (a_node: TYPE_EXPR_B)
923 -- <Precursor>
924 local
925 l_type: TYPE_A
926 do
927 l_type := a_node.type_type.deep_actual_type
928 translation_pool.add_type (l_type)
929 last_expression := factory.type_value (l_type)
930 end
931
932 process_un_free_b (a_node: UN_FREE_B)
933 -- <Precursor>
934 do
935 -- TODO: implement
936 end
937
938 process_un_minus_b (a_node: UN_MINUS_B)
939 -- <Precursor>
940 do
941 safe_process (a_node.expr)
942 create {IV_UNARY_OPERATION} last_expression.make ("-", last_expression, types.for_type_a (a_node.type))
943 end
944
945 process_un_not_b (a_node: UN_NOT_B)
946 -- <Precursor>
947 do
948 safe_process (a_node.expr)
949 create {IV_UNARY_OPERATION} last_expression.make ("!", last_expression, types.for_type_a (a_node.type))
950 end
951
952 process_un_old_b (a_node: UN_OLD_B)
953 -- <Precursor>
954 do
955 check False end
956 last_expression := dummy_node (a_node.type)
957 end
958
959 process_void_b (a_node: VOID_B)
960 -- <Precursor>
961 do
962 last_expression := factory.void_
963 end
964
965 feature -- Translation
966
967 process_attribute_call (a_feature: FEATURE_I)
968 -- Process call to attribute `a_feature'.
969 require
970 is_attribute: a_feature.is_attribute
971 local
972 l_current: IV_ENTITY
973 l_field: IV_ENTITY
974 l_heap_access: IV_HEAP_ACCESS
975 do
976 translation_pool.add_referenced_feature (a_feature, current_target_type)
977
978 check current_target /= Void end
979 create l_field.make (
980 name_translator.boogie_name_for_feature (a_feature, current_target_type),
981 types.field (types.for_type_in_context (a_feature.type, current_target_type))
982 )
983 create l_heap_access.make (entity_mapping.heap.name, current_target, l_field)
984 last_expression := l_heap_access
985 end
986
987 process_constant_call (a_feature: CONSTANT_I)
988 -- Process call to constant `a_feature'.
989 do
990 if a_feature.value.is_string then
991 last_expression := dummy_node (a_feature.type)
992 elseif a_feature.value.is_boolean then
993 create {IV_VALUE} last_expression.make (a_feature.value.string_value.as_lower, types.bool)
994 elseif a_feature.value.is_integer then
995 create {IV_VALUE} last_expression.make (a_feature.value.string_value, types.int)
996 elseif a_feature.value.is_character then
997 last_expression := dummy_node (a_feature.type)
998 else
999 last_expression := dummy_node (a_feature.type)
1000 end
1001 end
1002
1003 process_routine_call (a_feature: FEATURE_I; a_parameters: BYTE_LIST [PARAMETER_B]; a_for_creator: BOOLEAN)
1004 -- Process feature call.
1005 require
1006 not_attribute: a_feature.is_routine
1007 deferred
1008 end
1009
1010 process_special_routine_call (a_handler: E2B_CUSTOM_CALL_HANDLER; a_feature: FEATURE_I; a_parameters: BYTE_LIST [PARAMETER_B])
1011 -- Process feature call with custom handler.
1012 require
1013 not_attribute: a_feature.is_routine
1014 deferred
1015 end
1016
1017 add_safety_check (a_expression: IV_EXPRESSION; a_name: STRING; a_tag: STRING)
1018 -- Add safety check `a_expression' of type `a_name'.
1019 require
1020 boolean_expression: a_expression.type.is_boolean
1021 deferred
1022 end
1023
1024 safety_check_condition: LINKED_STACK [IV_EXPRESSION]
1025 -- Stack of safety check conditions.
1026
1027 implies_safety_expression (a_expr: IV_EXPRESSION): IV_EXPRESSION
1028 do
1029 if safety_check_condition.is_empty then
1030 Result := a_expr
1031 else
1032 create {IV_BINARY_OPERATION} Result.make (safety_check_condition.item, "==>", a_expr, types.bool)
1033 end
1034 end
1035
1036 process_parameters (a_parameters: BYTE_LIST [PARAMETER_B])
1037 -- Process parameter list `a_parameters'.
1038 local
1039 l_list: LINKED_LIST [IV_EXPRESSION]
1040 do
1041 create l_list.make
1042 parameters_stack.extend (l_list)
1043 safe_process (a_parameters)
1044 last_parameters := parameters_stack.item
1045 parameters_stack.remove
1046 end
1047
1048 process_argument_expression (a_expr: EXPR_B): IV_EXPRESSION
1049 -- Process `a_expr' in the context of the routine.
1050 local
1051 l_context_type: CL_TYPE_A
1052 l_target: IV_EXPRESSION
1053 l_target_type: TYPE_A
1054 l_last_expression: IV_EXPRESSION
1055 do
1056 l_target := current_target
1057 l_target_type := current_target_type
1058 l_last_expression := last_expression
1059
1060 current_target := entity_mapping.current_expression
1061 current_target_type := context_type
1062 last_expression := Void
1063
1064 safe_process (a_expr)
1065 Result := last_expression
1066
1067 last_expression := l_last_expression
1068 current_target := l_target
1069 current_target_type := l_target_type
1070 end
1071
1072 feature {E2B_ACROSS_HANDLER, E2B_CUSTOM_CALL_HANDLER, E2B_CUSTOM_NESTED_HANDLER} -- Implementation
1073
1074 parameters_stack: LINKED_STACK [LINKED_LIST [IV_EXPRESSION]]
1075 -- Stack of procedure calls.
1076
1077 last_parameters: LINKED_LIST [IV_EXPRESSION]
1078 -- List of last processed parameters.
1079
1080 last_local: IV_ENTITY
1081 -- Last created local.
1082
1083 create_iterator (a_type: IV_TYPE)
1084 -- Create new unbound iterator.
1085 local
1086 l_name: STRING
1087 do
1088 create last_local.make (helper.unique_identifier ("i"), a_type)
1089 end
1090
1091 is_in_quantifier: BOOLEAN
1092 -- Is current expression inside a quantifier?
1093
1094 dummy_node (a_type: TYPE_A): IV_EXPRESSION
1095 -- Dummy node for type `a_type'.
1096 local
1097 l_type: TYPE_A
1098 do
1099 l_type := a_type.deep_actual_type
1100 if l_type.is_integer or l_type.is_natural or l_type.is_character or l_type.is_character_32 then
1101 create {IV_VALUE} Result.make ("0", types.int)
1102 elseif l_type.is_boolean then
1103 create {IV_VALUE} Result.make ("false", types.bool)
1104 elseif l_type.is_expanded then
1105 create {IV_VALUE} Result.make ("Unknown", types.generic_type)
1106 else
1107 create {IV_VALUE} Result.make ("Void", types.ref)
1108 end
1109 end
1110
1111 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23