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

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_attribute_translator.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: 9676 byte(s)
Bugfix: redefinitions now taken into account when calculating replaced model queries.
1 note
2 description: "[
3 Translator for Eiffel attributes.
4 ]"
5 date: "$Date$"
6 revision: "$Revision$"
7
8 class
9 E2B_ATTRIBUTE_TRANSLATOR
10
11 inherit
12
13 E2B_FEATURE_TRANSLATOR
14
15 COMPILER_EXPORTER
16
17 feature -- Basic operations
18
19 translate (a_feature: FEATURE_I; a_context_type: CL_TYPE_A)
20 -- Translate feature `a_feature' of type `a_context_type'.
21 require
22 is_attribute: a_feature.is_attribute
23 local
24 l_attribute_name, l_old_name: STRING
25 l_class_type, l_written_type: CL_TYPE_A
26 l_type_prop, l_expr, l_context_type: IV_EXPRESSION
27 l_forall: IV_FORALL
28 l_heap, l_o, l_f: IV_ENTITY
29 l_heap_access: IV_MAP_ACCESS
30 l_boogie_type: IV_TYPE
31 is_ghost: BOOLEAN
32 do
33 set_context (a_feature, a_context_type)
34 l_class_type := helper.class_type_in_context (current_feature.type, current_type.base_class, Void, current_type)
35 l_attribute_name := name_translator.boogie_procedure_for_feature (current_feature, current_type)
36 l_boogie_type := types.for_class_type (l_class_type)
37 l_context_type := factory.type_value (current_type)
38 l_f := factory.entity (l_attribute_name, types.field (l_boogie_type))
39 is_ghost := helper.is_ghost (current_feature)
40
41 -- Add field declaration
42 boogie_universe.add_declaration (create {IV_CONSTANT}.make (l_f.name, l_f.type))
43
44 -- Add field ID
45 boogie_universe.add_declaration (create {IV_AXIOM}.make (factory.equal (
46 factory.function_call ("FieldId", << l_f, l_context_type >>, types.int),
47 factory.int_value (current_feature.feature_id))))
48
49
50 -- Add equivalences
51 across previous_versions as prev loop
52 if prev.item.is_attribute then
53 -- Check that properties match
54 if helper.is_ghost (prev.item) /= is_ghost then
55 helper.add_semantic_error (current_feature, messages.invalid_ghost_status (prev.item.feature_name_32, prev.item.written_class.name_in_upper), -1)
56 end
57
58 l_written_type := helper.class_type_from_class (prev.item.written_class, current_type)
59 l_old_name := name_translator.boogie_procedure_for_feature (prev.item, l_written_type)
60 translation_pool.add_referenced_feature (prev.item, l_written_type)
61 boogie_universe.add_declaration (create {IV_AXIOM}.make (factory.equal (l_f, create {IV_ENTITY}.make (l_old_name, l_f.type))))
62 end
63 end
64
65 -- Mark field as a ghost or non-ghost
66 l_expr := factory.function_call ("IsGhostField", << l_f >>, types.bool)
67 if is_ghost then
68 boogie_universe.add_declaration (create {IV_AXIOM}.make (l_expr))
69 else
70 boogie_universe.add_declaration (create {IV_AXIOM}.make (factory.not_ (l_expr)))
71 end
72
73 -- Add type properties
74 l_heap := factory.heap_entity ("heap")
75 l_o := factory.ref_entity ("o")
76 l_heap_access := factory.heap_access (l_heap, l_o, l_attribute_name, l_boogie_type)
77 l_type_prop := types.type_property (l_class_type, l_heap, l_heap_access)
78 if not l_type_prop.is_true then
79 l_type_prop := factory.implies_ (factory.and_ (
80 factory.is_heap (l_heap),
81 factory.function_call ("attached", << l_heap, l_o, l_context_type >>, types.bool)),
82 l_type_prop)
83 create l_forall.make (l_type_prop)
84 l_forall.add_bound_variable (l_heap)
85 l_forall.add_bound_variable (l_o)
86 l_forall.add_trigger (l_heap_access)
87 boogie_universe.add_declaration (create {IV_AXIOM}.make (l_forall))
88 end
89
90 -- Check if it replaces old models correctly
91 check_model_replacement
92
93 -- Add guard
94 generate_guard (l_class_type, l_attribute_name, l_boogie_type)
95
96 -- Add translation references
97 translation_pool.add_type (l_class_type)
98
99 -- elseif a_feature.type.is_integer or a_feature.type.is_natural then
100 -- create l_heap_access.make ("heap", create {IV_ENTITY}.make ("o", types.ref), create {IV_ENTITY}.make (l_boogie_name, l_constant.type))
101 -- create l_call.make ("is_" + a_feature.type.associated_class.name.as_lower, types.bool)
102 -- l_call.add_argument (l_heap_access)
103 -- create l_forall.make (l_call)
104 -- l_forall.add_bound_variable ("heap", types.heap_type)
105 -- l_forall.add_bound_variable ("o", types.ref)
106 -- create l_axiom.make (l_forall)
107 -- boogie_universe.add_declaration (l_axiom)
108 -- end
109 end
110
111 generate_guard (a_type: CL_TYPE_A; a_boogie_name: STRING; a_boogie_type: IV_TYPE)
112 -- Generate update guard for attribute `current_feature' of type `a_type' inside `current_type',
113 -- where the Boogie translation of the attribute has name `a_boogie_name' and type `a_boogie_type'.
114 local
115 l_guard_feature: FEATURE_I
116 l_h, l_cur, l_f, l_v, l_o: IV_ENTITY
117 l_fcall: IV_FUNCTION_CALL
118 l_guard, l_fname: STRING
119 l_def: IV_EXPRESSION
120 l_forall: IV_FORALL
121 do
122 create l_h.make ("heap", types.heap)
123 create l_cur.make ("current", types.ref)
124 create l_f.make (a_boogie_name, types.field (a_boogie_type))
125 create l_v.make ("v", a_boogie_type)
126 create l_o.make ("o", types.ref)
127 l_fcall := factory.function_call ("guard", << l_h, l_cur, l_f, l_v, l_o >>, types.bool)
128
129 l_guard := helper.guard_for_attribute (current_feature)
130 if l_guard.as_lower ~ "true" then
131 -- The guard is trivially true
132 create l_forall.make (l_fcall)
133 elseif l_guard.as_lower ~ "false" then
134 -- The guard is trivially false
135 create l_forall.make (factory.not_ (l_fcall))
136 else
137 l_guard_feature := current_type.base_class.feature_named_32 (l_guard)
138 if not l_guard.is_empty and is_valid_guard_feature (l_guard, l_guard_feature, a_type) then
139 translation_pool.add_referenced_feature (l_guard_feature, current_type)
140 -- Generate guard axiom from `l_guard_feature'
141 l_fname := name_translator.boogie_function_for_feature (l_guard_feature, current_type)
142 l_def := factory.function_call (name_translator.boogie_free_function_precondition (l_fname), << l_h, l_cur, l_v, l_o >>, types.bool)
143 l_def := factory.and_ (l_def,
144 factory.function_call (name_translator.boogie_function_precondition (l_fname), << l_h, l_cur, l_v, l_o >>, types.bool))
145 l_def := factory.and_ (l_def,
146 factory.function_call (l_fname, << l_h, l_cur, l_v, l_o >>, types.bool))
147 create l_forall.make (factory.equiv (l_fcall, l_def))
148 else
149 -- No guard defined: apply default
150 create l_forall.make (factory.equiv (l_fcall,
151 factory.function_call ("user_inv", << factory.map_update (l_h, << l_cur, l_f >>, l_v), l_o >>, types.bool)))
152 end
153 end
154
155 l_forall.add_bound_variable (l_h)
156 l_forall.add_bound_variable (l_cur)
157 l_forall.add_bound_variable (l_v)
158 l_forall.add_bound_variable (l_o)
159 l_forall.add_trigger (l_fcall)
160 boogie_universe.add_declaration (create {IV_AXIOM}.make (l_forall))
161 end
162
163 feature {NONE} -- Implementation
164
165 previous_versions: LINKED_LIST [FEATURE_I]
166 -- Versions of `current_feature' from ancestors of `current_type' if inherited or redefined.
167 do
168 if current_feature.written_in /= current_type.base_class.class_id then
169 -- Inherited attribute: return the class where it is written in
170 create Result.make
171 Result.extend (current_feature.written_class.feature_of_body_index (current_feature.body_index))
172 else
173 Result := helper.all_versions (current_feature)
174 Result.start
175 Result.remove
176 end
177 end
178
179 is_valid_guard_feature (a_guard_name: STRING_32; a_guard_feature: FEATURE_I; a_attr_type: CL_TYPE_A): BOOLEAN
180 -- Does `a_guard_feature' have a valid signature for an update guard for an attribute of type `a_attr_type'?
181 do
182 if a_guard_feature = Void then
183 helper.add_semantic_error (current_feature, messages.unknown_feature (a_guard_name, current_type.base_class.name_in_upper), -1)
184 elseif not helper.is_functional (a_guard_feature) then
185 helper.add_semantic_error (a_guard_feature, messages.guard_feature_not_functional, -1)
186 elseif not (a_guard_feature.has_return_value and then a_guard_feature.type.is_boolean) then
187 helper.add_semantic_error (a_guard_feature, messages.guard_feature_not_predicate, -1)
188 elseif a_guard_feature.argument_count /= 2 then
189 helper.add_semantic_error (a_guard_feature, messages.guard_feature_arg_count, -1)
190 elseif not a_guard_feature.arguments [1].same_as (a_attr_type) then
191 helper.add_semantic_error (a_guard_feature, messages.guard_feature_arg1, -1)
192 elseif not a_guard_feature.arguments [2].same_as (system.any_type) then
193 helper.add_semantic_error (a_guard_feature, messages.guard_feature_arg2, -1)
194 else
195 Result := True
196 end
197 end
198
199 check_model_replacement
200 -- For an immediate attribute with a "replaces" clause,
201 -- check that is didn't use to be a model query in any parent.
202 local
203 l_old_version, l_replaced: FEATURE_I
204 found: BOOLEAN
205 do
206 if current_feature.written_in = current_type.base_class.class_id then
207 across helper.feature_note_values (current_feature, "replaces") as f loop
208 l_replaced := current_type.base_class.feature_named_32 (f.item)
209 if attached l_replaced then
210 across current_type.base_class.parents_classes as c until found loop
211 l_old_version := c.item.feature_of_rout_id_set (current_feature.rout_id_set)
212 -- If both `current_feature' and `l_replaced' are model queries of `c.item',
213 -- this will cause child's model frames to be bigger than parent's
214 if attached l_old_version and then
215 (helper.is_model_query (c.item, l_old_version) and helper.is_model_query (c.item, l_replaced)) then
216 helper.add_semantic_error (current_feature, messages.invalid_model_replacement (current_feature.feature_name_32, c.item.name_in_upper), -1)
217 found := True
218 end
219 end
220 else
221 helper.add_semantic_error (current_feature, messages.unknown_model (f.item, current_type.base_class.name_in_upper), -1)
222 end
223 end
224 end
225 end
226
227 end

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.23