class E2B_CUSTOM_OWNERSHIP_HANDLER inherit E2B_CUSTOM_CALL_HANDLER SHARED_WORKBENCH SHARED_SERVER feature -- Status report is_handling_call (a_target_type: TYPE_A; a_feature: FEATURE_I): BOOLEAN -- <Precursor> do Result := (translation_mapping.builtin_any_functions.has (a_feature.feature_name) or translation_mapping.builtin_any_procedures.has (a_feature.feature_name) or translation_mapping.ghost_access.has (a_feature.feature_name) or translation_mapping.ghost_setter.has (a_feature.feature_name)) end feature -- Basic operations handle_routine_call_in_body (a_translator: E2B_BODY_EXPRESSION_TRANSLATOR; a_feature: FEATURE_I; a_parameters: BYTE_LIST [PARAMETER_B]) -- <Precursor> local l_name: STRING l_call: IV_PROCEDURE_CALL l_type: IV_TYPE l_trig: IV_FUNCTION_CALL l_old_side_effect: LINKED_LIST [IV_STATEMENT] do l_name := a_feature.feature_name if l_name ~ "use_definition" then l_old_side_effect := a_translator.side_effect a_translator.clear_side_effect a_translator.process_parameters (a_parameters) a_translator.restore_side_effect (l_old_side_effect) check a_translator.last_parameters.count = 1 end if attached {IV_FUNCTION_CALL} a_translator.last_parameters.first as l_fcall then create l_trig.make (name_translator.boogie_function_trigger (l_fcall.name), types.bool) l_trig.arguments.append (l_fcall.arguments) a_translator.side_effect.extend (create {IV_ASSERT}.make_assume (l_trig)) end elseif l_name ~ "transitive_owns" then a_translator.process_builtin_function_call (a_feature, a_parameters, "trans_owns") elseif l_name ~ "ownership_domain" then a_translator.process_builtin_function_call (a_feature, a_parameters, "domain") elseif translation_mapping.builtin_any_functions.has (l_name) then a_translator.process_builtin_function_call (a_feature, a_parameters, l_name) elseif l_name ~ "unwrap_no_inv" then a_translator.process_builtin_routine_call (a_feature, a_parameters, "unwrap") elseif translation_mapping.builtin_any_procedures.has (l_name) then pre_builtin_call (a_translator, a_feature) a_translator.process_builtin_routine_call (a_feature, a_parameters, l_name) post_builtin_call (a_translator, a_feature) elseif translation_mapping.ghost_access.has (l_name) then if l_name ~ "closed" then l_type := types.bool a_translator.set_last_expression (factory.function_call ("is_closed", << a_translator.entity_mapping.heap, a_translator.current_target >>, l_type)) else l_type := translation_mapping.ghost_access_type (l_name) a_translator.set_last_expression (factory.heap_access (a_translator.entity_mapping.heap, a_translator.current_target, l_name, l_type)) end elseif translation_mapping.ghost_setter.has (l_name) then l_name := l_name.substring (5, l_name.count) a_translator.process_builtin_routine_call (a_feature, a_parameters, "xyz") if attached {IV_PROCEDURE_CALL} a_translator.side_effect.last as c then a_translator.side_effect.finish a_translator.side_effect.remove -- last side effect is actual call, here to non-existing "xyz" a_translator.set_last_expression (Void) l_call := factory.procedure_call ("update_heap", << a_translator.current_target, factory.entity (l_name, types.field ((create {E2B_SPECIAL_MAPPING}.make).ghost_access_type (l_name))), c.arguments.i_th (2)>>) l_call.node_info.set_line (a_translator.context_line_number) a_translator.side_effect.extend (l_call) end else check false end end end handle_routine_call_in_contract (a_translator: E2B_CONTRACT_EXPRESSION_TRANSLATOR; a_feature: FEATURE_I; a_parameters: BYTE_LIST [PARAMETER_B]) -- <Precursor> local l_name: STRING l_type: IV_TYPE l_tag_filters: LIST [STRING] l_attr: FEATURE_I l_partial_inv_class: CLASS_C do l_name := a_feature.feature_name if translation_mapping.builtin_any_functions.has (l_name) then if l_name ~ "inv_without" then l_tag_filters := extract_tags (a_parameters) -- Determine the class whose invariant is taken as reference: -- if target is Current, then it is the origin class of the contract clause, -- otherwise, it is the type of the target if a_translator.current_target.same_expression (a_translator.entity_mapping.current_expression) then l_partial_inv_class := a_translator.origin_class else l_partial_inv_class := a_translator.current_target_type.base_class end check_valid_class_inv_tags (l_partial_inv_class, a_translator.context_feature, a_translator.context_line_number, l_tag_filters) translation_pool.add_filtered_invariant_function (a_translator.current_target_type, Void, l_tag_filters, l_partial_inv_class) a_translator.set_last_expression(factory.function_call ( name_translator.boogie_function_for_filtered_invariant (a_translator.current_target_type, Void, l_tag_filters, l_partial_inv_class), << a_translator.entity_mapping.heap, a_translator.current_target >>, types.bool)) elseif l_name ~ "inv_only" then l_tag_filters := extract_tags (a_parameters) if a_translator.current_target.same_expression (a_translator.entity_mapping.current_expression) then l_partial_inv_class := a_translator.origin_class else l_partial_inv_class := a_translator.current_target_type.base_class end check_valid_class_inv_tags (l_partial_inv_class, a_translator.context_feature, a_translator.context_line_number, l_tag_filters) translation_pool.add_filtered_invariant_function (a_translator.current_target_type, l_tag_filters, Void, l_partial_inv_class) a_translator.set_last_expression(factory.function_call ( name_translator.boogie_function_for_filtered_invariant (a_translator.current_target_type, l_tag_filters, Void, l_partial_inv_class), << a_translator.entity_mapping.heap, a_translator.current_target >>, types.bool)) elseif l_name ~ "inv" then a_translator.process_builtin_routine_call (a_feature, a_parameters, "user_inv") elseif l_name ~ "is_field_writable" then if attached {STRING_B} a_parameters.first.expression as l_string then -- ToDo: can origin class be different? l_attr := helper.attribute_from_string (l_string.value, a_translator.current_target_type, a_translator.current_target_type.base_class, a_translator.context_feature, a_translator.context_line_number) if attached l_attr then a_translator.set_last_expression (factory.frame_access ( a_translator.context_writable, a_translator.current_target, helper.field_from_attribute (l_attr, a_translator.current_target_type))) end else helper.add_semantic_error (a_translator.context_feature, messages.first_argument_string, a_translator.context_line_number) end elseif l_name ~ "is_fully_writable" then a_translator.set_last_expression (factory.function_call ( "has_whole_object", << a_translator.context_writable, a_translator.current_target>>, types.bool)) elseif l_name ~ "is_field_readable" then if attached a_translator.context_readable then if attached {STRING_B} a_parameters.first.expression as l_string then l_attr := helper.attribute_from_string (l_string.value, a_translator.current_target_type, a_translator.current_target_type.base_class, a_translator.context_feature, a_translator.context_line_number) if attached l_attr then a_translator.set_last_expression (factory.frame_access ( a_translator.context_readable, a_translator.current_target, helper.field_from_attribute (l_attr, a_translator.current_target_type))) end else helper.add_semantic_error (a_translator.context_feature, messages.first_argument_string, a_translator.context_line_number) end else helper.add_semantic_warning (a_translator.context_feature, messages.invalid_context_for_read_predicate, a_translator.context_line_number) a_translator.set_last_expression (factory.true_) end elseif l_name ~ "is_fully_readable" then if attached a_translator.context_readable then a_translator.set_last_expression (factory.function_call ( "has_whole_object", << a_translator.context_readable, a_translator.current_target>>, types.bool)) else helper.add_semantic_warning (a_translator.context_feature, messages.invalid_context_for_read_predicate, a_translator.context_line_number) a_translator.set_last_expression (factory.true_) end elseif l_name ~ "transitive_owns" then a_translator.process_builtin_routine_call (a_feature, a_parameters, "trans_owns") elseif l_name ~ "ownership_domain" then a_translator.process_builtin_routine_call (a_feature, a_parameters, "domain") elseif l_name ~ "universe" then a_translator.set_last_expression (factory.entity ("universe", types.set (types.ref))) elseif l_name ~ "is_fresh" then a_translator.set_last_expression (factory.not_ (factory.heap_access ( factory.old_ (factory.global_heap), a_translator.current_target, "allocated", types.bool))) else a_translator.process_builtin_routine_call (a_feature, a_parameters, l_name) end elseif translation_mapping.ghost_access.has (l_name) then if l_name ~ "closed" then l_type := types.bool a_translator.set_last_expression (factory.function_call ("is_closed", << a_translator.entity_mapping.heap, a_translator.current_target >>, l_type)) else l_type := translation_mapping.ghost_access_type (l_name) a_translator.set_last_expression (factory.heap_access (a_translator.entity_mapping.heap, a_translator.current_target, l_name, l_type)) end else -- cannot happen check False end end end extract_tags (a_parameters: BYTE_LIST [PARAMETER_B]): LIST [STRING] do check a_parameters.count = 1 end create {LINKED_LIST [STRING]} Result.make Result.compare_objects if attached {STRING_B} a_parameters.first.expression as l_string then Result.extend (l_string.value) elseif attached {TUPLE_CONST_B} a_parameters.first.expression as l_tuple then across l_tuple.expressions as i loop if attached {STRING_B} i as l_string then Result.extend (l_string.value) else check False end end end else check False end end end check_valid_class_inv_tags (a_class: CLASS_C; a_context_feature: FEATURE_I; a_line_number: INTEGER; a_tags: LIST [READABLE_STRING_8]) -- Check if `a_tags' only lists valid class invariant of `a_class'. -- Otherwise report error in feature `a_context_feature'. local l_tags_copy: LINKED_LIST [READABLE_STRING_8] l_string: STRING_32 do create l_tags_copy.make l_tags_copy.append (a_tags) l_tags_copy.compare_objects -- Remove default tags across translation_mapping.default_tags as t loop l_tags_copy.prune_all (t) end -- Remove user-defined tags check_flat_inv_tags (a_class, l_tags_copy) if not l_tags_copy.is_empty then l_string := {STRING_32} "" across l_tags_copy as i loop l_string.append ({UTF_CONVERTER}.utf_8_string_8_to_string_32 (i)) l_string.append ({STRING_32} ", ") end l_string.remove_tail (2) helper.add_semantic_error (a_context_feature, messages.invalid_tag (l_string, a_class.name_in_upper), a_line_number) end end check_flat_inv_tags (a_class: CLASS_C; a_tags: LIST [READABLE_STRING_8]) -- Remove from `a_tags' all class invariant tags present in `a_class' and its ancestors. local l_classes: FIXED_LIST [CLASS_C] do if inv_byte_server.has (a_class.class_id) then across inv_byte_server.item (a_class.class_id).byte_list as node loop if attached {ASSERT_B} node as a then a_tags.prune_all (a.tag) end end end from l_classes := a_class.parents_classes l_classes.start until l_classes.after loop if l_classes.item.class_id /= system.any_id then check_flat_inv_tags (l_classes.item, a_tags) end l_classes.forth end end pre_builtin_call (a_translator: E2B_BODY_EXPRESSION_TRANSLATOR; a_feature: FEATURE_I) -- Insert code before calling a built-in procedure `a_feature_name'. local l_type_translator: E2B_TYPE_TRANSLATOR l_check: IV_EXPRESSION do -- If processing a call to `wrap', -- generate appropriate guarded assignments to implicit model queries and an invariant check if a_feature.feature_name ~ "wrap" then if use_static_invariant (a_translator) then -- Check exact invariant definition. create l_type_translator l_type_translator.translate_inline_invariant_check (a_translator.current_target_type, a_translator.current_target) across helper.ghost_attributes (a_translator.current_target_type.base_class) as a loop set_implicit_ghost (a_translator, a) end across l_type_translator.last_clauses as c loop c.node_info.set_line (a_translator.context_line_number) c.node_info.set_attribute ("cid", a_feature.written_class.class_id.out) c.node_info.set_attribute ("rid", a_feature.rout_id_set.first.out) if options.is_inv_check_independent then a_translator.add_independent_check (c) else a_translator.side_effect.extend (c) end end else -- Use dynamically bound invariant function. l_check := factory.function_call ("user_inv", << a_translator.entity_mapping.heap, a_translator.current_target >>, types.bool) a_translator.add_safety_check (l_check, "inv", "unknown_invariant", a_translator.context_line_number) a_translator.last_safety_check.node_info.set_attribute ("cid", a_feature.written_class.class_id.out) a_translator.last_safety_check.node_info.set_attribute ("rid", a_feature.rout_id_set.first.out) end end end post_builtin_call (a_translator: E2B_BODY_EXPRESSION_TRANSLATOR; a_feature: FEATURE_I) -- Insert code after calling a built-in procedure `a_feature_name'. local l_assume: IV_ASSERT do -- If processing a call to `unwrap', -- assume either generic `user_inv' or class-specific invariant function, depending if the target is `Current'. if a_feature.feature_name ~ "unwrap" then if use_static_invariant (a_translator) then -- Use exact invariant definition. create l_assume.make_assume ( factory.function_call (name_translator.boogie_function_for_invariant (a_translator.current_target_type), << a_translator.entity_mapping.heap, a_translator.current_target >>, types.bool)) a_translator.side_effect.extend (l_assume) else -- Use dynamically bound invariant function. create l_assume.make_assume ( factory.function_call ("user_inv", << a_translator.entity_mapping.heap, a_translator.current_target >>, types.bool)) a_translator.side_effect.extend (l_assume) if not helper.is_manual_inv (a_translator.context_feature) and not helper.is_manual_inv_class (a_translator.context_type.base_class) then create l_assume.make_assume (factory.function_call ("inv_frame_trigger", << a_translator.current_target >>, types.bool)) a_translator.side_effect.extend (l_assume) end end end end use_static_invariant (a_translator: E2B_BODY_EXPRESSION_TRANSLATOR): BOOLEAN -- Should the static definition of the invariant be used for the current target of `a_translator'? do -- Yes if the current target is "Current" and the context feature is not marked as nonvariant, -- or the type of the target is exact. Result := (a_translator.current_target.same_expression (a_translator.entity_mapping.current_expression) and not helper.is_nonvariant (a_translator.context_feature)) or helper.is_type_exact (a_translator.current_target_type, a_translator.current_target_type, a_translator.context_feature) end set_implicit_ghost (a_translator: E2B_BODY_EXPRESSION_TRANSLATOR; a_attr: FEATURE_I) -- If the definition of `a_attr' in `current_target_type' is statically known, -- generate a guarded update and store it in the side effect of `a_translator'. local l_function: IV_FUNCTION l_field: IV_ENTITY l_pcall: IV_PROCEDURE_CALL l_fcall: IV_FUNCTION_CALL l_if: IV_CONDITIONAL do -- Get definition of `a_field_name' for `current_target_type'; -- if it exists, generate a guarded assignment. l_field := helper.field_from_attribute (a_attr, a_translator.current_target_type) l_function := boogie_universe.function_named ( name_translator.boogie_function_for_ghost_definition (a_translator.current_target_type, l_field.name)) if attached l_function then create l_pcall.make ("update_heap") l_pcall.add_argument (a_translator.current_target) l_pcall.add_argument (l_field) l_pcall.add_argument (factory.function_call (l_function.name, << a_translator.entity_mapping.heap, a_translator.current_target >>, types.field_content_type (l_field.type))) l_pcall.node_info.set_attribute ("default", a_attr.feature_name) l_pcall.node_info.set_line (a_translator.context_line_number) -- Create a condition that l_field is in the modify clause of the current function -- (modify clause is used instead of writable, since it is not possible to prove that something is not writable) create l_fcall.make (name_translator.boogie_function_for_write_frame (a_translator.context_feature, a_translator.context_type), types.frame) l_fcall.add_argument (factory.global_heap) across a_translator.context_implementation.procedure.arguments as i loop l_fcall.add_argument (i.entity) end create l_if.make_if_then (factory.frame_access (l_fcall, a_translator.current_target, l_field), factory.singleton_block (l_pcall)) a_translator.side_effect.extend (l_if) end end note date: "$Date$" revision: "$Revision$" copyright: "Copyright (c) 2012-2014 ETH Zurich", "Copyright (c) 2018-2019 Politecnico di Milano", "Copyright (c) 2022 Schaffhausen Institute of Technology" author: "Julian Tschannen", "Nadia Polikarpova", "Alexander Kogtenkov" license: "GNU General Public License" license_name: "GPL" EIS: "name=GPL", "src=https://www.gnu.org/licenses/gpl.html", "tag=license" copying: "[ This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 1, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program. If not, see <https://www.gnu.org/licenses/>. ]" end