------------------------------------------------------------------------------ ------------------------------------------------------------------------------ -- Cheddar is a GNU GPL real-time scheduling analysis tool. -- This program provides services to automatically check schedulability and -- other performance criteria of real-time architecture models. -- -- Copyright (C) 2002-2016, Frank Singhoff, Alain Plantec, Jerome Legrand -- -- The Cheddar project was started in 2002 by -- Frank Singhoff, Lab-STICC UMR 6285 laboratory, Université de Bretagne Occidentale -- -- Cheddar has been published in the "Agence de Protection des Programmes/France" in 2008. -- Since 2008, Ellidiss technologies also contributes to the development of -- Cheddar and provides industrial support. -- -- The full list of contributors and sponsors can be found in AUTHORS.txt and SPONSORS.txt -- -- 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 2 of the License, 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, write to the Free Software -- Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -- -- -- Contact : cheddar@listes.univ-brest.fr -- ------------------------------------------------------------------------------ -- Last update : -- $Rev: 1249 $ -- $Date: 2014-08-28 07:02:15 +0200 (Fri, 28 Aug 2014) $ -- $Author: singhoff $ ------------------------------------------------------------------------------ ------------------------------------------------------------------------------ with Ada.Exceptions; use Ada.Exceptions; with Time_Unit_Events; use Time_Unit_Events; use Time_Unit_Events.Time_Unit_Package; with Tasks; use Tasks; with Resources; use Resources; use Resources.resource_accesses; with Translate; use Translate; with Objects; use Objects; with Objects.extended; use Objects.extended; with integer_util; with initialize_framework; use initialize_framework; with text_io; use text_io; with scheduler_interface.extended; use scheduler_interface.extended; package body Address_Space_Set is procedure Add_Address_Space (My_Address_Spaces : in out Address_Spaces_Set; Name : in Unbounded_String; Cpu_Name : in Unbounded_String; Text_Memory_Size : in Integer; Stack_Memory_Size : in Integer; Data_Memory_Size : in Integer; Heap_Memory_Size : in Integer; Is_Preemptive : in Preemptives_Type := preemptive; Quantum : in Integer := 0; File_Name : in Unbounded_String := empty_string; A_Scheduler : in Schedulers_Type := No_Scheduling_Protocol; automaton_name : in Unbounded_String := empty_string; mils_confidentiality_level : in MILS_Confidentiality_Level_Type := Top_Secret; mils_integrity_level : in MILS_Integrity_Level_Type := High; mils_component : in MILS_Component_Type := SLS; mils_partition : in MILS_Partition_Type := Device; mils_compliant : in Boolean := True ) is Dummy : Address_Space_Ptr; begin Add_Address_Space (My_Address_Spaces, Dummy, Name, Cpu_Name, Text_Memory_Size, Stack_Memory_Size, Data_Memory_Size, Heap_Memory_Size, Is_Preemptive, Quantum, File_Name, A_Scheduler, automaton_name, mils_confidentiality_level, mils_integrity_level, mils_component, mils_partition, mils_compliant ); end Add_Address_Space; procedure Check_Address_Space (My_Address_Spaces : in Address_Spaces_Set; Name : in Unbounded_String; Cpu_Name : in Unbounded_String; Text_Memory_Size : in Integer; Stack_Memory_Size : in Integer; Data_Memory_Size : in Integer; Heap_Memory_Size : in Integer; Is_Preemptive : in Preemptives_Type := preemptive; Quantum : in Integer := 0; File_Name : in Unbounded_String := empty_string; A_Scheduler : in Schedulers_Type := No_Scheduling_Protocol; automaton_name : in Unbounded_String := empty_string; mils_confidentiality_level : in MILS_Confidentiality_Level_Type := Top_Secret; mils_integrity_level : in MILS_Integrity_Level_Type := High; mils_component : in MILS_Component_Type := SLS; mils_partition : in MILS_Partition_Type := Device; mils_compliant : in Boolean := True ) is begin if Name = "" then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & Lb_Address_Space_Name (Current_Language) & Lb_Mandatory (Current_Language))); end if; if not Is_A_Valid_Identifier (Name) then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & Lb_Address_Space_Name (Current_Language) & Lb_Colon & Lb_Invalid_Identifier (Current_Language))); end if; if Cpu_Name = "" then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Processor_Name (Current_Language) & Lb_Mandatory (Current_Language))); end if; if not Is_A_Valid_Identifier (cpu_Name) then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & Lb_processor_Name (Current_Language) & Lb_Colon & Lb_Invalid_Identifier (Current_Language))); end if; if (Text_Memory_Size < 0) then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & Lb_Text_Memory_Size (Current_Language) & Lb_Must_Be (Current_Language) & Lb_greater_or_equal_than (Current_Language) & "0")); end if; if (Data_Memory_Size < 0) then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & Lb_Data_Memory_Size (Current_Language) & Lb_Must_Be (Current_Language) & Lb_greater_or_equal_than (Current_Language) & "0")); end if; if (Heap_Memory_Size < 0) then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & Lb_Heap_Memory_Size (Current_Language) & Lb_Must_Be (Current_Language) & Lb_greater_or_equal_than (Current_Language) & "0")); end if; if (Stack_Memory_Size < 0) then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & Lb_Stack_Memory_Size (Current_Language) & Lb_Must_Be (Current_Language) & Lb_greater_or_equal_than (Current_Language) & "0")); end if; if (File_Name /= "") and (A_Scheduler /= Automata_User_Defined_Protocol) and (A_Scheduler /= compiled_User_Defined_Protocol) and (A_Scheduler /= pipeline_User_Defined_Protocol) then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & Lb_File_Name_Control (Current_Language))); end if; if not Is_A_Valid_Identifier (file_name) then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & name & " , " & file_Name & " : " & Lb_Parametric_File_Name (Current_Language) & Lb_Colon & Lb_Invalid_Identifier (Current_Language))); end if; if (Quantum < 0) then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & "Quantum" & Lb_Must_Be (Current_Language) & Lb_greater_or_equal_than (Current_Language) & "0")); end if; if a_scheduler /= Rate_Monotonic_Protocol and a_scheduler /= Deadline_Monotonic_Protocol and a_scheduler /= Posix_1003_Highest_Priority_First_Protocol and a_scheduler /= Earliest_Deadline_First_Protocol and a_scheduler /= Least_Laxity_First_Protocol and a_scheduler /= Round_Robin_Protocol and a_scheduler /= Maximum_Urgency_First_Based_On_Deadline_Protocol and a_scheduler /= Maximum_Urgency_First_Based_On_Laxity_Protocol and a_scheduler /= Time_Sharing_Based_On_Wait_Time_Protocol and a_scheduler /= Time_Sharing_Based_On_Cpu_Usage_Protocol and a_scheduler /= D_Over_Protocol and a_scheduler /= Automata_User_Defined_Protocol and a_scheduler /= Compiled_User_Defined_Protocol and a_scheduler /= No_Scheduling_Protocol then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & Lb_Invalid_Scheduler (Current_Language))); end if; end Check_Address_Space; procedure Add_Address_Space (My_Address_Spaces : in out Address_Spaces_Set; A_Address_Space : in out Address_Space_Ptr; Name : in Unbounded_String; Cpu_Name : in Unbounded_String; Text_Memory_Size : in Integer; Stack_Memory_Size : in Integer; Data_Memory_Size : in Integer; Heap_Memory_Size : in Integer; Is_Preemptive : in Preemptives_Type := preemptive; Quantum : in Integer := 0; File_Name : in Unbounded_String := empty_string; A_Scheduler : in Schedulers_Type := No_Scheduling_Protocol; automaton_name : in Unbounded_String := empty_string; mils_confidentiality_level : in MILS_Confidentiality_Level_Type := Top_Secret; mils_integrity_level : in MILS_Integrity_Level_Type := High; mils_component : in MILS_Component_Type := SLS; mils_partition : in MILS_Partition_Type := Device; mils_compliant : in Boolean := True ) is My_Iterator : Address_Spaces_Iterator; begin check_initialize; Check_Address_Space (My_Address_Spaces, Name, Cpu_Name, Text_Memory_Size, Stack_Memory_Size, Data_Memory_Size, Heap_Memory_Size, Is_Preemptive, Quantum, File_Name, A_Scheduler, automaton_name, mils_confidentiality_level, mils_integrity_level, mils_component, mils_partition, mils_compliant ); if (get_number_of_elements (My_Address_Spaces) > 0) then reset_iterator (My_Address_Spaces, My_Iterator); loop current_element (My_Address_Spaces, A_Address_Space, My_Iterator); if (Name = A_Address_Space.name) then Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Address_Space (Current_Language) & " " & Name & " : " & Lb_Address_Space_Name (Current_Language) & Lb_Already_Defined (Current_Language))); end if; exit when is_last_element (My_Address_Spaces, My_Iterator); next_element (My_Address_Spaces, My_Iterator); end loop; end if; A_Address_Space := new address_space; A_Address_Space.cpu_name := Cpu_Name; A_Address_Space.name := Name; A_Address_Space.text_memory_size := Text_Memory_Size; A_Address_Space.stack_memory_size := Stack_Memory_Size; A_Address_Space.data_memory_size := Data_Memory_Size; A_Address_Space.heap_memory_size := Heap_Memory_Size; A_Address_Space.mils_confidentiality_level := mils_confidentiality_level; A_Address_Space.mils_integrity_level := mils_integrity_level; A_Address_Space.mils_component := mils_component; A_Address_Space.mils_partition := mils_partition; A_Address_Space.mils_compliant := mils_compliant; a_Address_Space.scheduling.quantum:= quantum; a_Address_Space.scheduling.automaton_name:= automaton_name; a_Address_Space.scheduling.scheduler_type:= a_scheduler; a_Address_Space.scheduling.preemptive_type:= is_preemptive; a_Address_Space.scheduling.user_defined_scheduler_source_file_name:= file_name; a_Address_Space.scheduling.period:=0; a_Address_Space.scheduling.priority:=0; a_Address_Space.scheduling.start_time:=0; a_Address_Space.scheduling.capacity:=0; add (My_Address_Spaces, A_Address_Space); exception when Generic_Address_Space_Set.full_set => Raise_Exception (Invalid_Parameter'Identity, To_String (Lb_Can_Not_Define_More_Address_Spaces (Current_Language))); end Add_Address_Space; function Search_Address_Space_by_id (My_Address_Spaces : in Address_Spaces_Set; id : in Unbounded_String) return Address_Space_Ptr is My_Iterator : Address_Spaces_Iterator; A_Addr : Address_Space_Ptr; Result : Address_Space_Ptr; Found : Boolean := False; begin if not is_empty(My_Address_Spaces) then reset_iterator (My_Address_Spaces, My_Iterator); loop current_element (My_Address_Spaces, A_Addr, My_Iterator); if (A_Addr.cheddar_private_id = id) then Found := True; Result := A_Addr; end if; exit when is_last_element (My_Address_Spaces, My_Iterator); next_element (My_Address_Spaces, My_Iterator); end loop; end if; if not Found then Raise_Exception (Address_Space_Not_Found'Identity, To_String (Lb_Address_Space_id (Current_Language) & "=" & id)); end if; return Result; end Search_Address_Space_by_id; function Search_Address_Space (My_Address_Spaces : in Address_Spaces_Set; Name : in Unbounded_String) return Address_Space_Ptr is My_Iterator : Address_Spaces_Iterator; A_Addr : Address_Space_Ptr; Result : Address_Space_Ptr; Found : Boolean := False; begin if not is_empty(My_Address_Spaces) then reset_iterator (My_Address_Spaces, My_Iterator); loop current_element (My_Address_Spaces, A_Addr, My_Iterator); if (A_Addr.name = Name) then Found := True; Result := A_Addr; end if; exit when is_last_element (My_Address_Spaces, My_Iterator); next_element (My_Address_Spaces, My_Iterator); end loop; end if; if not Found then Raise_Exception (Address_Space_Not_Found'Identity, To_String (Lb_Address_Space_Name (Current_Language) & "=" & Name)); end if; return Result; end Search_Address_Space; function Address_Space_Is_Present (My_Address_Spaces : in Address_Spaces_Set; Name : in Unbounded_String) return Boolean is My_Iterator : Address_Spaces_Iterator; A_Address_Space : Address_Space_Ptr; Found : Boolean := False; begin if is_empty (My_Address_Spaces) then return False; else reset_iterator (My_Address_Spaces, My_Iterator); loop current_element (My_Address_Spaces, A_Address_Space, My_Iterator); if (A_Address_Space.name = Name) then Found := True; end if; exit when is_last_element (My_Address_Spaces, My_Iterator); next_element (My_Address_Spaces, My_Iterator); end loop; return Found; end if; end Address_Space_Is_Present; procedure Delete_Processor (My_Address_Spaces : in out Address_Spaces_Set; A_Processor : in Unbounded_String) is Tmp : Address_Spaces_Set; A_Address_Space : Address_Space_Ptr; My_Iterator : Address_Spaces_Iterator; begin if (get_number_of_elements (My_Address_Spaces) > 0) then reset_iterator (My_Address_Spaces, My_Iterator); loop current_element (My_Address_Spaces, A_Address_Space, My_Iterator); if (A_Address_Space.cpu_name = A_Processor) then add (Tmp, A_Address_Space); end if; exit when is_last_element (My_Address_Spaces, My_Iterator); next_element (My_Address_Spaces, My_Iterator); end loop; if not is_empty (Tmp) then reset_iterator (My_Address_Spaces, My_Iterator); loop current_element (Tmp, A_Address_Space, My_Iterator); delete (My_Address_Spaces, A_Address_Space); exit when is_last_element (Tmp, My_Iterator); next_element (Tmp, My_Iterator); end loop; reset (Tmp, False); end if; end if; end Delete_Processor; -- -- AADL export sub-programs -- function Export_Aadl_Implementations (My_Address_Spaces : in Address_Spaces_Set; My_Tasks : in Tasks_Set; My_Resources : in Resources_Set) return Unbounded_String is My_Iterator1 : Address_Spaces_Iterator; A_Address_Space : Address_Space_Ptr; My_Iterator2 : Tasks_Iterator; A_Task : Generic_Task_Ptr; My_Iterator3 : Resources_Iterator; A_Resource : Generic_Resource_Ptr; Result : Unbounded_String := empty_string; Thread_Subcomponents : Unbounded_String := empty_string; Data_Subcomponents : Unbounded_String := empty_string; First_Resource : Boolean := True; begin if not is_empty (My_Address_Spaces) then reset_iterator (My_Address_Spaces, My_Iterator1); loop current_element (My_Address_Spaces, A_Address_Space, My_Iterator1); Result := Result & To_Unbounded_String ("process " & To_String (A_Address_Space.name)) & unbounded_lf; Result := Result & To_Unbounded_String ("end " & To_String (A_Address_Space.name) & ";") & unbounded_lf; Result := Result & unbounded_lf; Result := Result & To_Unbounded_String ("process implementation " & To_String (A_Address_Space.name) & ".Impl") & unbounded_lf; Thread_Subcomponents := Export_Aadl_Declarations (My_Tasks, A_Address_Space.name, 2); Data_Subcomponents := Export_Aadl_Declarations (My_Resources, A_Address_Space.name, 2); if (Thread_Subcomponents /= empty_string) or (Data_Subcomponents /= empty_string) then Result := Result & To_Unbounded_String (ASCII.HT & "subcomponents") & unbounded_lf & Thread_Subcomponents & Data_Subcomponents; end if; if Data_Subcomponents /= empty_string then reset_iterator (My_Tasks, My_Iterator2); Result := Result & To_Unbounded_String (ASCII.HT & "connections") & unbounded_lf; loop current_element (My_Tasks, A_Task, My_Iterator2); if A_Task.address_space_name = A_Address_Space.name then Result := Result & Export_Aadl_Connections (My_Resources, A_Task.name, 2); end if; exit when is_last_element (My_Tasks, My_Iterator2); next_element (My_Tasks, My_Iterator2); end loop; end if; Result := Result & To_Unbounded_String (ASCII.HT & "properties") & unbounded_lf; Result := Result & To_Unbounded_String (ASCII.HT & ASCII.HT & "Cheddar_Properties::Source_Global_Text_Size => " & A_Address_Space.text_memory_size'Img & " kb ;") & unbounded_lf; Result := Result & To_Unbounded_String (ASCII.HT & ASCII.HT & "Cheddar_Properties::Source_Global_Data_Size => " & A_Address_Space.data_memory_size'Img & " kb ;") & unbounded_lf; Result := Result & To_Unbounded_String (ASCII.HT & ASCII.HT & "Cheddar_Properties::Source_Global_Heap_Size => " & A_Address_Space.heap_memory_size'Img & " kb ;") & unbounded_lf; Result := Result & To_Unbounded_String (ASCII.HT & ASCII.HT & "Cheddar_Properties::Source_Global_Stack_Size => " & A_Address_Space.stack_memory_size'Img & " kb ;") & unbounded_lf; if A_Address_Space.scheduling.scheduler_type /= No_Scheduling_Protocol then Result := Result & Export_Aadl_Properties (A_Address_Space.scheduling, 2); end if; if Data_Subcomponents /= empty_string then Result := Result & To_Unbounded_String (ASCII.HT & ASCII.HT & "Cheddar_Properties::Critical_Section => (") & unbounded_lf; reset_iterator (My_Resources, My_Iterator3); loop current_element (My_Resources, A_Resource, My_Iterator3); if A_Resource.address_space_name = A_Address_Space.name then if A_Resource.critical_sections.nb_entries /= 0 then if not First_Resource then Result := Result & To_Unbounded_String (",") & unbounded_lf; end if; First_Resource := False; for I in 0 .. A_Resource.critical_sections.nb_entries - 1 loop Result := Result & ASCII.HT & ASCII.HT & ASCII.HT & """" & "instancied_" & To_String (A_Resource.name) & """" & "," & unbounded_lf; Result := Result & To_Unbounded_String (ASCII.HT & ASCII.HT & ASCII.HT & """" & "instancied_" & To_String (A_Resource.critical_sections.entries (I).item) & """,""" & To_String (integer_util.format (A_Resource.critical_sections.entries (I).data. task_begin)) & """,""" & To_String (integer_util.format (A_Resource.critical_sections.entries (I).data. task_end)) & """"); if I /= A_Resource.critical_sections.nb_entries - 1 then Result := Result & To_Unbounded_String (","); Result := Result & unbounded_lf; end if; end loop; end if; end if; exit when is_last_element (My_Resources, My_Iterator3); next_element (My_Resources, My_Iterator3); end loop; Result := Result & To_Unbounded_String (ASCII.HT & ASCII.HT & ASCII.HT & ");") & unbounded_lf; end if; Result := Result & To_Unbounded_String ("end " & To_String (A_Address_Space.name) & ".Impl;") & unbounded_lf; Result := Result & unbounded_lf; exit when is_last_element (My_Address_Spaces, My_Iterator1); next_element (My_Address_Spaces, My_Iterator1); end loop; end if; return Result; end Export_Aadl_Implementations; function Export_Aadl_Declarations (My_Address_Spaces : in Address_Spaces_Set; Number_Of_Ht : in Natural) return Unbounded_String is My_Iterator : Address_Spaces_Iterator; A_Address_Space : Address_Space_Ptr; Result : Unbounded_String := empty_string; begin if not is_empty (My_Address_Spaces) then reset_iterator (My_Address_Spaces, My_Iterator); loop current_element (My_Address_Spaces, A_Address_Space, My_Iterator); for I in 1 .. Number_Of_Ht loop Result := Result & ASCII.HT; end loop; Result := Result & To_Unbounded_String ("instancied_" & To_String (A_Address_Space.name) & " : process " & To_String (A_Address_Space.name) & ".Impl;") & unbounded_lf; exit when is_last_element (My_Address_Spaces, My_Iterator); next_element (My_Address_Spaces, My_Iterator); end loop; end if; return Result; end Export_Aadl_Declarations; function Export_Aadl_Properties (My_Address_Spaces : in Address_Spaces_Set; Number_Of_Ht : in Natural) return Unbounded_String is My_Iterator : Address_Spaces_Iterator; A_Address_Space : Address_Space_Ptr; Result : Unbounded_String := empty_string; begin if not is_empty (My_Address_Spaces) then reset_iterator (My_Address_Spaces, My_Iterator); loop current_element (My_Address_Spaces, A_Address_Space, My_Iterator); for I in 1 .. Number_Of_Ht loop Result := Result & ASCII.HT; end loop; Result := Result & To_Unbounded_String ("Actual_Processor_Binding => reference instancied_" & To_String (A_Address_Space.cpu_name) & " applies to instancied_" & To_String (A_Address_Space.name) & ";") & unbounded_lf; exit when is_last_element (My_Address_Spaces, My_Iterator); next_element (My_Address_Spaces, My_Iterator); end loop; end if; return Result; end Export_Aadl_Properties; procedure Check_entity_referencing_processor (My_Address_Spaces : in Address_Spaces_Set; A_processor : in Unbounded_String) is My_Iterator : Address_Spaces_Iterator; A_Addr : Address_Space_Ptr; begin if (get_number_of_elements (My_Address_Spaces) > 0) then reset_iterator (My_Address_Spaces, My_Iterator); loop current_element (My_Address_Spaces, A_addr, My_Iterator); if (A_addr.cpu_name = A_processor) then Raise_Exception (Invalid_Parameter'Identity, To_String ( lb_processor (Current_Language) & " " & a_processor & " : " & lb_address_space (Current_Language) & " " & a_addr.Name & " : " & lb_entity_referenced_elsewhere(current_language) )); end if; exit when is_last_element (My_Address_Spaces, My_Iterator); next_element (My_Address_Spaces, My_Iterator); end loop; end if; end Check_entity_referencing_processor; end Address_Space_Set;