/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/iv/iv_boogie_printer.e
ViewVC logotype

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/iv/iv_boogie_printer.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: 15955 byte(s)
AutoProof: special translation for lemma and functional
1 note
2 description: "[
3 IV-visitor that generates Boogie code.
4 ]"
5 date: "$Date$"
6 revision: "$Revision$"
7
8 class
9 IV_BOOGIE_PRINTER
10
11 inherit
12
13 IV_UNIVERSE_VISITOR
14
15 IV_CONTRACT_VISITOR
16
17 IV_STATEMENT_VISITOR
18
19 IV_EXPRESSION_VISITOR
20
21 IV_TYPE_VISITOR
22
23 create
24 make
25
26 feature {NONE} -- Initialization
27
28 make
29 -- Initialize universe visitor.
30 do
31 reset
32 end
33
34 feature -- Access
35
36 output: E2B_BOOGIE_TEXT
37 -- Boogie text output.
38
39 feature -- Basic operations
40
41 reset
42 -- Reset universe visitor.
43 do
44 create output
45 end
46
47 feature -- Universe Visitor
48
49 process_function (a_function: IV_FUNCTION)
50 -- <Precursor>
51 do
52 output.put ("function ")
53 if a_function.is_inline then
54 output.put ("{ :inline } ")
55 end
56 output.put (a_function.name)
57 output.put ("(")
58 across a_function.arguments as i loop
59 if i.cursor_index /= 1 then
60 output.put (", ")
61 end
62 process_entity_declaration (i.item)
63 end
64 output.put (") returns (")
65 a_function.type.process (Current)
66 output.put (")")
67 if attached a_function.body as l_body then
68 output.put (" {")
69 output.put_new_line
70 output.indent
71 output.put (output.indentation_string)
72 l_body.process (Current)
73 output.unindent
74 output.put_new_line
75 output.put ("}")
76 else
77 output.put (";")
78 end
79 output.put_new_line
80 output.put_new_line
81 end
82
83 process_variable (a_variable: IV_VARIABLE)
84 -- <Precursor>
85 do
86 output.put ("var ")
87 process_entity_declaration (a_variable)
88 output.put (";")
89 output.put_new_line
90 output.put_new_line
91 end
92
93 process_constant (a_constant: IV_CONSTANT)
94 -- <Precursor>
95 do
96 output.put ("const ")
97 if a_constant.is_unique then
98 output.put ("unique ")
99 end
100 output.put (a_constant.name)
101 output.put (": ")
102 a_constant.type.process (Current)
103 output.put (";")
104 output.put_new_line
105 output.put_new_line
106 end
107
108 process_axiom (a_axiom: IV_AXIOM)
109 -- <Precursor>
110 do
111 output.put ("axiom (")
112 a_axiom.expression.process (Current)
113 output.put (");")
114 output.put_new_line
115 output.put_new_line
116 end
117
118 process_procedure (a_procedure: IV_PROCEDURE)
119 -- <Precursor>
120 do
121 output.put ("procedure ")
122 output.put (a_procedure.name)
123 output.put ("(")
124 across a_procedure.arguments as i loop
125 if i.cursor_index /= 1 then
126 output.put (", ")
127 end
128 process_entity_declaration (i.item)
129 end
130 output.put (")")
131 if not a_procedure.results.is_empty then
132 output.put (" returns (")
133 across a_procedure.results as i loop
134 if i.cursor_index /= 1 then
135 output.put (", ")
136 end
137 process_entity_declaration (i.item)
138 end
139 output.put (")")
140 end
141 output.put (";")
142 output.put_new_line
143 output.indent
144 across a_procedure.contracts as i loop
145 i.item.process (Current)
146 end
147 output.unindent
148 output.put_new_line
149 across a_procedure.implementations as i loop
150 i.item.process (Current)
151 end
152 output.put_new_line
153 output.put_new_line
154 end
155
156 process_implementation (a_implementation: IV_IMPLEMENTATION)
157 -- <Precursor>
158 do
159 output.put ("implementation ")
160 output.put (a_implementation.procedure.name)
161 output.put ("(")
162 across a_implementation.procedure.arguments as i loop
163 if i.cursor_index /= 1 then
164 output.put (", ")
165 end
166 output.put (i.item.name)
167 output.put (": ")
168 i.item.type.process (Current)
169 end
170 output.put (")")
171 if not a_implementation.procedure.results.is_empty then
172 output.put (" returns (")
173 across a_implementation.procedure.results as i loop
174 if i.cursor_index /= 1 then
175 output.put (", ")
176 end
177 output.put (i.item.name)
178 output.put (": ")
179 i.item.type.process (Current)
180 end
181 output.put (")")
182 end
183 output.put_new_line
184 output.put ("{")
185 output.put_new_line
186 output.indent
187 if not a_implementation.locals.is_empty or not a_implementation.procedure.results.is_empty then
188 across a_implementation.locals as i loop
189 output.put_indentation
190 output.put ("var ")
191 output.put (i.item.name)
192 output.put (": ")
193 i.item.type.process (Current)
194 output.put (";")
195 output.put_new_line
196 end
197 output.put_new_line
198 output.put_line ("init_locals:")
199 across a_implementation.locals as i loop
200 -- No defaults needed for auxiliary locals of Boogie types, like HeapType:
201 if default_value (i.item.type) /= Void then
202 output.put_indentation
203 output.put (i.item.name)
204 output.put (" := ")
205 output.put (default_value (i.item.type))
206 output.put (";")
207 output.put_new_line
208 end
209 end
210 across a_implementation.procedure.results as i loop
211 output.put_indentation
212 output.put (i.item.name)
213 output.put (" := ")
214 output.put (default_value (i.item.type))
215 output.put (";")
216 output.put_new_line
217 end
218 output.put_new_line
219 end
220 a_implementation.body.process (Current)
221 output.unindent
222 output.put ("}")
223 output.put_new_line
224 output.put_new_line
225 end
226
227 feature -- Contract visitor
228
229 process_precondition (a_precondition: IV_PRECONDITION)
230 -- <Precursor>
231 do
232 output.put_indentation
233 if a_precondition.is_free then
234 output.put ("free ")
235 end
236 output.put ("requires ")
237 a_precondition.expression.process (Current)
238 output.put (";")
239 print_assertion_information (a_precondition)
240 output.put_new_line
241 end
242
243 process_postcondition (a_postcondition: IV_POSTCONDITION)
244 -- <Precursor>
245 do
246 output.put_indentation
247 if a_postcondition.is_free then
248 output.put ("free ")
249 end
250 output.put ("ensures ")
251 a_postcondition.expression.process (Current)
252 output.put (";")
253 print_assertion_information (a_postcondition)
254 output.put_new_line
255 end
256
257 process_modifies (a_modifies: IV_MODIFIES)
258 -- <Precursor>
259 do
260 output.put_indentation
261 output.put ("modifies ")
262 across a_modifies.names as i loop
263 if i.cursor_index /= 1 then
264 output.put (", ")
265 end
266 output.put (i.item)
267 end
268 output.put (";")
269 output.put_new_line
270 end
271
272 feature -- Statement Visitor
273
274 process_assert (a_assert: IV_ASSERT)
275 -- <Precursor>
276 do
277 output.put_indentation
278 output.put ("assert ")
279 a_assert.expression.process (Current)
280 output.put (";")
281 print_assertion_information (a_assert)
282 output.put_new_line
283 end
284
285 process_assume (a_assume: IV_ASSUME)
286 -- <Precursor>
287 do
288 output.put_indentation
289 output.put ("assume ")
290 if attached a_assume.attribute_string then
291 output.put ("{" + a_assume.attribute_string + "} ")
292 end
293 a_assume.expression.process (Current)
294 output.put (";")
295 output.put_new_line
296 end
297
298 process_assignment (a_assignment: IV_ASSIGNMENT)
299 -- <Precursor>
300 do
301 output.put_indentation
302 a_assignment.target.process (Current)
303 output.put (" := ")
304 a_assignment.source.process (Current)
305 output.put (";")
306 output.put_new_line
307 end
308
309 process_block (a_block: IV_BLOCK)
310 -- <Precursor>
311 do
312 if not a_block.name.is_empty then
313 output.put_indentation
314 output.put (a_block.name)
315 output.put (":")
316 output.put_new_line
317 end
318 across a_block.statements as i loop
319 print_statement_origin_information (i.item)
320 i.item.process (Current)
321 end
322 end
323
324 process_conditional (a_conditional: IV_CONDITIONAL)
325 -- <Precursor>
326 do
327 output.put_indentation
328 output.put ("if (")
329 a_conditional.condition.process (Current)
330 output.put (") {")
331 output.put_new_line
332 output.indent
333 a_conditional.then_block.process (Current)
334 output.unindent
335 output.put_line ("} else {")
336 output.indent
337 a_conditional.else_block.process (Current)
338 output.unindent
339 output.put_line ("}")
340 end
341
342 process_havoc (a_havoc: IV_HAVOC)
343 -- <Precursor>
344 do
345 output.put_indentation
346 output.put ("havoc ")
347 across a_havoc.names as i loop
348 if i.cursor_index /= 1 then
349 output.put (", ")
350 end
351 output.put (i.item)
352 end
353 output.put (";")
354 output.put_new_line
355 end
356
357 process_label (a_label: IV_LABEL)
358 -- <Precursor>
359 do
360 check False end
361 end
362
363 process_loop (a_loop: IV_LOOP)
364 -- <Precursor>
365 do
366 output.put_indentation
367 output.put ("while (")
368 if a_loop.is_until_loop then
369 output.put ("!(")
370 end
371 a_loop.condition.process (Current)
372 if a_loop.is_until_loop then
373 output.put (")")
374 end
375 output.put (")")
376 output.put_new_line
377 output.indent
378 across a_loop.invariants as i loop
379 output.put_indentation
380 i.item.process (Current)
381 output.put (";")
382 output.put_new_line
383 end
384 output.unindent
385 output.put_line ("{")
386 a_loop.body.process (Current)
387 output.put_line ("}")
388 end
389
390 process_goto (a_goto: IV_GOTO)
391 -- <Precursor>
392 do
393 output.put_indentation
394 output.put ("goto ")
395 across a_goto.blocks as i loop
396 if i.cursor_index /= 1 then
397 output.put (", ")
398 end
399 output.put (i.item.name)
400 end
401 output.put (";")
402 output.put_new_line
403 end
404
405 process_procedure_call (a_call: IV_PROCEDURE_CALL)
406 -- <Precursor>
407 do
408 output.put_indentation
409 output.put ("call ")
410 if attached a_call.target as l_target then
411 l_target.process (Current)
412 output.put (" := ")
413 end
414 output.put (a_call.name)
415 output.put ("(")
416 across a_call.arguments as i loop
417 if i.cursor_index /= 1 then
418 output.put (", ")
419 end
420 i.item.process (Current)
421 end
422 output.put (");")
423 output.put_new_line
424 end
425
426 process_return (a_return: IV_RETURN)
427 -- <Precursor>
428 do
429 output.put_indentation
430 output.put ("return;")
431 output.put_new_line
432 end
433
434 print_statement_origin_information (a_statement: IV_STATEMENT)
435 -- Print origin information of `a_statement'.
436 do
437 if attached a_statement.origin_information as l_origin then
438 output.put_comment_line (l_origin.file + ":" + l_origin.line.out)
439 if l_origin.line > 0 then
440 output.put_comment_line (l_origin.text_of_line)
441 end
442 end
443 end
444
445 print_assertion_information (a_assertion: IV_ASSERTION)
446 -- Print assertion information of `a_assertion'.
447 do
448 if attached a_assertion.information as l_info then
449 output.put (" // ")
450 output.put (l_info.type)
451 if attached l_info.tag as l_tag then
452 output.put (" tag:")
453 output.put (l_tag)
454 end
455 if attached l_info.line as l_line then
456 output.put (" line:")
457 output.put (l_line)
458 end
459 end
460 end
461
462 feature -- Expression Visitor
463
464 process_binary_operation (a_operation: IV_BINARY_OPERATION)
465 -- <Precursor>
466 local
467 l_do_left_par, l_do_right_par: BOOLEAN
468 do
469 l_do_left_par :=
470 (a_operation.operator /~ "&&" and a_operation.operator /~ "||") or
471 not (attached {IV_BINARY_OPERATION} a_operation.left as l_b and then l_b.operator ~ a_operation.operator)
472 l_do_right_par :=
473 (a_operation.operator /~ "&&" and a_operation.operator /~ "||") or
474 not (attached {IV_BINARY_OPERATION} a_operation.right as l_b and then l_b.operator ~ a_operation.operator)
475
476 if l_do_left_par then
477 output.put ("(")
478 a_operation.left.process (Current)
479 output.put (")")
480 else
481 a_operation.left.process (Current)
482 end
483 output.put (" ")
484 output.put (a_operation.operator)
485 output.put (" ")
486 if l_do_right_par then
487 output.put ("(")
488 a_operation.right.process (Current)
489 output.put (")")
490 else
491 a_operation.right.process (Current)
492 end
493 end
494
495 process_conditional_expression (a_conditional: IV_CONDITIONAL_EXPRESSION)
496 -- <Precursor>
497 do
498 output.put ("if ")
499 a_conditional.condition.process (Current)
500 output.put (" then ")
501 a_conditional.then_expression.process (Current)
502 output.put (" else ")
503 a_conditional.else_expression.process (Current)
504 end
505
506 process_entity (a_entity: IV_ENTITY)
507 -- <Precursor>
508 do
509 output.put (a_entity.name)
510 end
511
512 process_exists (a_exists: IV_EXISTS)
513 -- <Precursor>
514 do
515 process_quantifier ("exists", a_exists)
516 end
517
518 process_forall (a_forall: IV_FORALL)
519 -- <Precursor>
520 do
521 process_quantifier ("forall", a_forall)
522 end
523
524 process_function_call (a_call: IV_FUNCTION_CALL)
525 -- <Precursor>
526 do
527 output.put (a_call.name)
528 output.put ("(")
529 across a_call.arguments as i loop
530 if i.cursor_index /= 1 then
531 output.put (", ")
532 end
533 i.item.process (Current)
534 end
535 output.put (")")
536 end
537
538 process_map_access (a_map_access: IV_MAP_ACCESS)
539 -- <Precursor>
540 do
541 a_map_access.target.process (Current)
542 output.put ("[")
543 across a_map_access.indexes as i loop
544 if i.cursor_index /= 1 then
545 output.put (", ")
546 end
547 i.item.process (Current)
548 end
549 output.put ("]")
550 end
551
552 process_unary_operation (a_operation: IV_UNARY_OPERATION)
553 -- <Precursor>
554 do
555 output.put (a_operation.operator)
556 output.put ("(")
557 a_operation.expression.process (Current)
558 output.put (")")
559 end
560
561 process_value (a_value: IV_VALUE)
562 -- <Precursor>
563 do
564 output.put (a_value.value)
565 end
566
567 feature -- Type Visitor
568
569 process_boolean_type (a_type: IV_BASIC_TYPE)
570 -- <Precursor>
571 do
572 output.put ("bool")
573 end
574
575 process_integer_type (a_type: IV_BASIC_TYPE)
576 -- <Precursor>
577 do
578 output.put ("int")
579 end
580
581 process_real_type (a_type: IV_BASIC_TYPE)
582 -- <Precursor>
583 do
584 output.put ("real")
585 end
586
587 process_reference_type (a_type: IV_BASIC_TYPE)
588 -- <Precursor>
589 do
590 output.put ("ref")
591 end
592
593 process_generic_type (a_type: IV_GENERIC_TYPE)
594 -- <Precursor>
595 do
596 output.put ("beta")
597 -- check False end
598 end
599
600 process_type_type (a_type: IV_BASIC_TYPE)
601 -- <Precursor>
602 do
603 output.put ("Type")
604 end
605
606 process_heap_type (a_type: IV_BASIC_TYPE)
607 -- <Precursor>
608 do
609 output.put ("HeapType")
610 end
611
612 process_frame_type (a_type: IV_BASIC_TYPE)
613 -- Process frame type.
614 do
615 output.put ("Frame")
616 end
617
618 process_field_type (a_type: IV_FIELD_TYPE)
619 -- <Precursor>
620 do
621 output.put ("Field ")
622 if a_type.content_type.is_map or a_type.content_type.is_seq then
623 output.put ("(")
624 a_type.content_type.process (Current)
625 output.put (")")
626 else
627 a_type.content_type.process (Current)
628 end
629 end
630
631 process_set_type (a_type: IV_SET_TYPE)
632 -- <Precursor>
633 do
634 output.put ("Set ")
635 a_type.content_type.process (Current)
636 end
637
638 process_seq_type (a_type: IV_SEQ_TYPE)
639 -- <Precursor>
640 do
641 output.put ("Seq ")
642 a_type.content_type.process (Current)
643 end
644
645 feature -- Other
646
647 process_entity_declaration (a_declaration: IV_ENTITY_DECLARATION)
648 -- <Precursor>
649 do
650 -- TODO: extract this helper function to some parent
651 output.put (a_declaration.name)
652 output.put (": ")
653 a_declaration.type.process (Current)
654 if attached a_declaration.property as l_property then
655 output.put (" where ")
656 l_property.process (Current)
657 end
658 end
659
660 process_quantifier (a_keyword: STRING; a_quantifier: IV_QUANTIFIER)
661 -- Process quantifier `a_quantifier'.
662 local
663 l_generic_printed: BOOLEAN
664 do
665 across a_quantifier.bound_variables as i until l_generic_printed loop
666 if attached {IV_GENERIC_TYPE} i.item.type or attached {IV_FIELD_TYPE} i.item.type then
667 l_generic_printed := True
668 end
669 end
670
671 output.put ("(")
672 output.put (a_keyword)
673 if l_generic_printed then
674 output.put ("<beta>")
675 end
676 output.put (" ")
677 across a_quantifier.bound_variables as i loop
678 if i.cursor_index /= 1 then
679 output.put (", ")
680 end
681 process_entity_declaration (i.item)
682 end
683 output.put (" :: ")
684 across a_quantifier.triggers as i loop
685 output.put ("{ ")
686 i.item.process (Current)
687 output.put (" } ")
688 end
689 a_quantifier.expression.process (Current)
690 output.put (")")
691 end
692
693 default_value (a_type: IV_TYPE): STRING
694 -- Default value for type `a_type'.
695 local
696 l_printer: like Current
697 do
698 if a_type.is_boolean then
699 Result := "false"
700 elseif a_type.is_integer then
701 Result := "0"
702 elseif a_type.is_real then
703 Result := "0.0"
704 elseif a_type.is_set then
705 Result := "Set#Empty()"
706 elseif a_type.is_seq then
707 Result := "Seq#Empty()"
708 elseif a_type.is_reference then
709 Result := "Void"
710 else
711 Result := Void
712 end
713 end
714
715 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23