------------------------------------------------------------------------------ -- -- -- OCARINA COMPONENTS -- -- -- -- O C A R I N A . C H E C K E R _ T E S T S U I T E -- -- -- -- B o d y -- -- -- -- Copyright (C) 2007, GET-Telecom Paris. -- -- -- -- Ocarina is free software; you can redistribute it and/or modify -- -- it under terms of the GNU General Public License as published by the -- -- Free Software Foundation; either version 2, or (at your option) any -- -- later version. Ocarina 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 distributed with Ocarina; see file COPYING. -- -- If not, write to the Free Software Foundation, 51 Franklin Street, Fifth -- -- Floor, Boston, MA 02111-1301, USA. -- -- -- -- As a special exception, if other files instantiate generics from this -- -- unit, or you link this unit with other files to produce an executable, -- -- this unit does not by itself cause the resulting executable to be -- -- covered by the GNU General Public License. This exception does not -- -- however invalidate any other reasons why the executable file might be -- -- covered by the GNU Public License. -- -- -- -- Ocarina is maintained by the Ocarina team -- -- (ocarina-users@listes.enst.fr) -- -- -- ------------------------------------------------------------------------------ -- This package contains basic templates for non-functional properties -- to be verified in the AADL model with Ocarina.Expander; with Ocarina.Expander.Queries; with Ocarina.Checker.Queries; with Ocarina.Nutils; with Namet; with Ocarina.Nodes; with Ocarina.Checker.Queries.Subcomponent_Predicates; with Ocarina.Checker.Queries.Call_Predicates; with Ocarina.Checker.Queries.Connected_Predicates; with Ocarina.Checker.Queries.Bound_Predicates; with Ocarina.Checker.Queries.Access_Predicates; -- Only for debugging purposes with Ocarina.Debug; use Ocarina.Debug; package body Ocarina.Checker_Testsuite is use Ocarina.Expander; use Ocarina.Expander.Queries; use Ocarina.Checker.Queries; use Namet; use Ocarina.Nutils; use Ocarina.Nodes; package OCAP renames Ocarina.Checker.Queries.Access_Predicates.Access_Query; package OCBP renames Ocarina.Checker.Queries.Bound_Predicates.Bound_Query; package OCSP renames Ocarina.Checker.Queries.Subcomponent_Predicates.Subcomponent_Query; package OCCP renames Ocarina.Checker.Queries.Call_Predicates.Call_Query; package OCNCP renames Ocarina.Checker.Queries.Connected_Predicates.Connected_Query; function Get_Size_Property (E : Node_Id; Property_Name : String) return Natural; -- Return property's size value in Bytes procedure Instanciate_Ocarina_Tree (Distributed_Application_Root : Node_Id; Instance_Root : out Node_Id); ------------------------------ -- Instanciate_Ocarina_Tree -- ------------------------------ procedure Instanciate_Ocarina_Tree (Distributed_Application_Root : Node_Id; Instance_Root : out Node_Id) is begin -- Instantiation of the AADL tree Instance_Root := Expand_Model (Distributed_Application_Root); -- Abort if the instantiation failed if No (Instance_Root) then W_Line ("The AADL model cannot be expanded."); raise Program_Error; end if; end Instanciate_Ocarina_Tree; -------------------------- -- Perform_All_Checking -- -------------------------- procedure Perform_All_Checking (Distributed_Application_Root : Node_Id; Options : Checker_Options) is Instance_Root : Node_Id; begin Instanciate_Ocarina_Tree (Distributed_Application_Root, Instance_Root); if Options.OS_Related_Checking then Do_Check_Mutexes (Instance_Root); Do_Check_Processes (Instance_Root); Do_Check_Connections (Instance_Root); Do_Check_Access (Instance_Root); end if; if Options.Hardware_Related_Checking then Do_Check_Memory_Size (Instance_Root); Do_Check_Stack_Size (Instance_Root); Do_Check_Buses_Size (Instance_Root); end if; end Perform_All_Checking; --------------------- -- Do_Check_Access -- --------------------- procedure Do_Check_Access (Instance_Root : Node_Id) is pragma Unreferenced (Instance_Root); R1 : Result_Set; R2 : Result_Set; Result : Result_Set; begin W_Line ("Checking data access... "); R1 := Get_Instances_Of_Component_Type (C_Data); R2 := Get_Instances_Of_Component_Type (C_Thread); for I in 1 .. Cardinal (R1) loop -- 1/ We search all processes bound to a given processor -- instance Result := OCAP.Get_Instances_Verifying_Predicate (R2, Get (R1, I)); W_Line (Image (Int (Cardinal (Result))) & " threads access to data " & Get_Name_String (Compute_Full_Name_Of_Instance (Get (R1, I)))); end loop; end Do_Check_Access; ---------------------- -- Do_Check_Mutexes -- ---------------------- procedure Do_Check_Mutexes (Instance_Root : Node_Id) is pragma Unreferenced (Instance_Root); Property_Name : constant String := "rtos_properties::max_mutexes_number"; R1 : Result_Set; R2 : Result_Set; R3 : Result_Set; Result : Result_Set; Result_2 : Result_Set; Final_Result : Result_Set; begin W_Line ("Checking mutexes number... "); R1 := Get_Instances_Of_Component_Type (C_Data); R2 := Get_Instances_Of_Component_Type (C_Process); R3 := Get_Instances_Of_Component_Type (C_Processor); for I in 1 .. Cardinal (R3) loop Final_Result := Empty_Set; -- 1/ We search all processes bound to a given processor -- instance Result := OCBP.Get_Instances_Verifying_Predicate (R2, Get (R3, I)); for J in 1 .. Cardinal (Result) loop -- 2/ We search all data which are subcomponent of a -- given process instance Result_2 := OCSP.Get_Instances_Verifying_Predicate (R1, Get (Result, J), PSO_Direct); Final_Result := Union (Final_Result, Result_2); end loop; if Is_Defined_Property (Get (R3, I), Property_Name) and then Int (Get_Integer_Property (Get (R3, I), Property_Name)) < Int (Cardinal (Final_Result)) then W_Line ("Failed!"); W_Str ("The processor "); Write_Name (Compute_Full_Name_Of_Instance (Get (R3, I))); W_Line (" manages too many mutexes."); raise Program_Error; else W_Str ("* The processor "); Write_Name (Compute_Full_Name_Of_Instance (Get (R3, I))); W_Line (" manages " & Image (Int (Cardinal (Final_Result))) & " mutexes."); end if; end loop; end Do_Check_Mutexes; ------------------------ -- Do_Check_Processes -- ------------------------ procedure Do_Check_Processes (Instance_Root : Node_Id) is pragma Unreferenced (Instance_Root); Property_Name : constant String := "rtos_properties::max_processes_number"; R1 : Result_Set; R2 : Result_Set; Result : Result_Set; begin W_Line ("Checking processes number... "); R1 := Get_Instances_Of_Component_Type (C_Process); R2 := Get_Instances_Of_Component_Type (C_Processor); for I in 1 .. Cardinal (R2) loop -- 1/ We search all processes bound to a given processor -- instance Result := OCBP.Get_Instances_Verifying_Predicate (R1, Get (R2, I)); if Is_Defined_Property (Get (R2, I), Property_Name) and then Int (Get_Integer_Property (Get (R2, I), Property_Name)) < Int (Cardinal (Result)) then W_Line ("Failed!"); W_Str ("The processor "); Write_Name (Compute_Full_Name_Of_Instance (Get (R2, I))); W_Line (" runs too many processes."); raise Program_Error; else W_Str ("* The processor "); Write_Name (Compute_Full_Name_Of_Instance (Get (R2, I))); W_Line (" runs " & Image (Int (Cardinal (Result))) & " processes."); end if; end loop; end Do_Check_Processes; -------------------------- -- Do_Check_memory_Size -- -------------------------- procedure Do_Check_memory_Size (Instance_Root : Node_Id) is pragma Unreferenced (Instance_Root); function Compute_Max_Memory_Size (Set : Result_Set) return Natural; ----------------------------- -- Compute_Max_Memory_Size -- ----------------------------- function Compute_Max_Memory_Size (Set : Result_Set) return Natural is --------------------------- -- Compute_Memory_Needed -- --------------------------- function Compute_Memory_Needed (E : Node_Id) return Natural is Property_Data_Name : constant String := "source_data_size"; Property_Code_Name : constant String := "source_code_size"; Property_Heap_Name : constant String := "source_heap_size"; Value : Natural := 0; begin if Is_Defined_Property (E, Property_Data_Name) then Value := Get_Size_Property (E, Property_Data_Name); end if; if Is_Defined_Property (E, Property_Code_Name) then Value := Value + Get_Size_Property (E, Property_Code_Name); end if; if Is_Defined_Property (E, Property_Heap_Name) then Value := Value + Get_Size_Property (E, Property_Heap_Name); end if; return Value; end Compute_Memory_Needed; Total_Val : Natural := 0; begin for I in 1 .. Cardinal (Set) loop Total_Val := Total_Val + Compute_Memory_Needed (Corresponding_Instance (Get (Set, I))); end loop; return Total_Val; end Compute_Max_Memory_Size; R1, R2, R3, R4 : Result_Set; Result : Result_Set; Result_2 : Result_Set; Processor_Stack : Natural; Process_Stack : Natural; Thread_Calls_Set : Result_Set; Thread_Stack : Natural := 0; Memory_Size : Natural := 0; begin W_Line ("Checking memory size... "); R1 := Get_Instances_Of_Component_Type (C_Thread); R2 := Get_Instances_Of_Component_Type (C_Process); R3 := Get_Instances_Of_Component_Type (C_Processor); R4 := Get_Instances_Of_Component_Type (C_Subprogram_Call); for I in 1 .. Cardinal (R3) loop -- 1/ We search all processes bound to a given processor -- instance Result := OCBP.Get_Instances_Verifying_Predicate (R2, Get (R3, I)); Processor_Stack := 0; for J in 1 .. Cardinal (Result) loop -- 2/ We search all threads which are subcomponent of a -- given process instance Result_2 := OCSP.Get_Instances_Verifying_Predicate (R1, Get (Result, J)); Process_Stack := 0; for K in 1 .. Cardinal (Result_2) loop Thread_Calls_Set := OCCP.Get_Instances_Verifying_Predicate (R4, Get (Result_2, K), PSO_Recursive); Thread_Stack := Compute_Max_Memory_Size (Thread_Calls_Set); Process_Stack := Process_Stack + Thread_Stack; end loop; Processor_Stack := Processor_Stack + Process_Stack; end loop; -- We search for memories binded to the processor -- and sum availabel memory space Memory_Size := 0; declare Proc : constant Node_Id := Get (R3, I); Str : constant String := "actual_memory_binding"; Mem : Node_Id; begin -- if the processor is in the memory binding list -- we add memory size do the processor availability if Is_Defined_Reference_Property (Proc, Str) then Mem := Get_Reference_Property (Proc, Str); Memory_Size := Memory_Size + Get_Size_Property (Mem, "rtos_properties::memory_size"); end if; if Processor_Stack > Memory_Size then W_Line ("Failed!"); Write_Name (Compute_Full_Name_Of_Instance (Proc)); W_Line (" memory is not large enought."); raise Program_Error; else W_Str ("* The processor "); Write_Name (Compute_Full_Name_Of_Instance (Proc)); W_Str (" uses " & Image (Int (Processor_Stack)) & " Bytes out of "); W_Line (Image (Int (Memory_Size))); end if; end; end loop; end Do_Check_Memory_Size; ------------------------- -- Do_Check_Stack_Size -- ------------------------- procedure Do_Check_Stack_Size (Instance_Root : Node_Id) is pragma Unreferenced (Instance_Root); function Compute_Max_Stack_Size (E : Node_Id) return Natural; ---------------------------- -- Compute_Max_Stack_Size -- ---------------------------- function Compute_Max_Stack_Size (E : Node_Id) return Natural is -------------------------- -- Compute_Stack_Needed -- -------------------------- function Compute_Stack_Needed (E : Node_Id) return Natural is Property_Data_Name : constant String := "source_data_size"; Property_Heap_Name : constant String := "source_heap_size"; Value : Natural := 0; begin if Is_Defined_Property (E, Property_Data_Name) then Value := Get_Size_Property (E, Property_Data_Name); end if; if Is_Defined_Property (E, Property_Heap_Name) then Value := Value + Get_Size_Property (E, Property_Heap_Name); end if; return Value; end Compute_Stack_Needed; Call_Seq : Node_Id; N : Node_Id; Total_Val : Natural := 0; Tmp_Val : Natural; begin if not Is_Empty (Calls (E)) then Call_Seq := First_Node (Calls (E)); else return Compute_Stack_Needed (E); end if; if not Is_Empty (Subprogram_Calls (Call_Seq)) then while Present (Call_Seq) loop if not Is_Empty (Subprogram_Calls (Call_Seq)) then N := First_Node (Subprogram_Calls (Call_Seq)); while Present (N) loop Tmp_Val := Compute_Max_Stack_Size (Corresponding_Instance (N)); if Tmp_Val > Total_Val then Total_Val := Tmp_Val; end if; N := Next_Node (N); end loop; Call_Seq := Next_Node (Call_Seq); end if; end loop; end if; return Total_Val + Compute_Stack_Needed (E); end Compute_Max_Stack_Size; R1, R2, R3 : Result_Set; Result : Result_Set; Result_2 : Result_Set; Processor_Stack : Natural := 0; Process_Stack : Natural := 0; Thread_Stack : Natural := 0; Memory_Size : Natural := 0; begin W_Line ("Checking memory stack... "); R1 := Get_Instances_Of_Component_Type (C_Thread); R2 := Get_Instances_Of_Component_Type (C_Process); R3 := Get_Instances_Of_Component_Type (C_Processor); for I in 1 .. Cardinal (R3) loop -- 1/ We search all processes bound to a given processor -- instance Result := OCBP.Get_Instances_Verifying_Predicate (R2, Get (R3, I)); for J in 1 .. Cardinal (Result) loop Process_Stack := 0; -- 2/ We search all threads which are subcomponent of a -- given process instance Result_2 := OCSP.Get_Instances_Verifying_Predicate (R1, Get (Result, J)); for K in 1 .. Cardinal (Result_2) loop Thread_Stack := Compute_Max_Stack_Size (Get (Result_2, K)); if Thread_Stack > Process_Stack then Process_Stack := Thread_Stack; end if; end loop; if Process_Stack > Processor_Stack then Processor_Stack := Process_Stack; end if; end loop; -- We search for memories binded to the processor -- and sum availabel memory space Memory_Size := 0; declare Proc : constant Node_Id := Get (R3, I); Str : constant String := "actual_memory_binding"; Mem : Node_Id; Mem_Size : Natural; begin -- we search for the largest available memory for the processor if Is_Defined_Reference_Property (Proc, Str) then Mem := Get_Reference_Property (Proc, Str); Mem_Size := Get_Size_Property (Mem, "rtos_properties::memory_size"); if Mem_Size > Memory_Size then Memory_Size := Mem_Size; end if; end if; if Processor_Stack > Memory_Size then W_Line ("Failed!"); W_Str ("No memory is large enought in order to host "); Write_Name (Compute_Full_Name_Of_Instance (Proc)); W_Line (" stack"); raise Program_Error; else W_Str ("* The processor "); Write_Name (Compute_Full_Name_Of_Instance (Proc)); W_Str (" stack is " & Image (Int (Processor_Stack)) & " Bytes out of "); W_Line (Image (Int (Memory_Size))); end if; end; end loop; end Do_Check_Stack_Size; ----------------------- -- Get_Size_Property -- ----------------------- function Get_Size_Property (E : Node_Id; Property_Name : String) return Natural is V : Node_Id; U : Node_Id; Result : Natural; begin if Is_Defined_Integer_Property (E, Property_Name) then V := Get_Value_Of_Property_Association (E, Property_Name); if Present (V) and then Present (Unit_Identifier (V)) then U := Unit_Identifier (V); -- Get the value Result := Natural (Get_Integer_Property (E, Property_Name)); -- Convert the value to its unit declare Str : constant String := Get_Name_String (Name (U)); begin if Str = "bits" then Result := Result / 8; elsif Str = "b" then null; elsif Str = "kb" then Result := Result * 1024; elsif Str = "mb" then Result := Result * 1048576; elsif Str = "gb" then Result := Result * 1073741824; end if; return Result; end; end if; end if; return 0; end Get_Size_Property; -------------------------- -- Do_Check_Connections -- -------------------------- procedure Do_Check_Connections (Instance_Root : Node_Id) is pragma Unreferenced (Instance_Root); Property_Name : constant String := "rtos_properties::max_connections_number"; R1 : Result_Set; R2 : Result_Set; Bound_Processes : Result_Set; Process_Connections : Result_Set; OS_Connections : Result_Set; begin W_Line ("Checking connections number... "); R1 := Get_Instances_Of_Component_Type (C_Process); R2 := Get_Instances_Of_Component_Type (C_Processor); for I in 1 .. Cardinal (R2) loop -- 1/ We search all processes bound to a given processor -- instance Bound_Processes := OCBP.Get_Instances_Verifying_Predicate (R1, Get (R2, I)); -- For each bound process, we sum connections OS_Connections := Empty_Set; for J in 1 .. Cardinal (Bound_Processes) loop Process_Connections := OCNCP.Get_Instances_Verifying_Predicate (R1, Get (Bound_Processes, J)); OS_Connections := Union (OS_Connections, Process_Connections); end loop; if Is_Defined_Property (Get (R2, I), Property_Name) and then Int (Get_Integer_Property (Get (R2, I), Property_Name)) < Int (Cardinal (OS_Connections)) then W_Line ("Failed!"); W_Str ("The processor "); Write_Name (Compute_Full_Name_Of_Instance (Get (R2, I))); W_Line (" manages too many connections."); raise Program_Error; else W_Str ("* The processor "); Write_Name (Compute_Full_Name_Of_Instance (Get (R2, I))); W_Line (" manages " & Image (Int (Cardinal (OS_Connections))) & " connections"); end if; end loop; end Do_Check_Connections; ------------------------- -- Do_Check_Buses_Size -- ------------------------- procedure Do_Check_Buses_Size (Instance_Root : Node_Id) is pragma Unreferenced (Instance_Root); Buses_Set : Result_Set; Connections_Set : Result_Set; Result : Result_Set; Bus : Node_Id; N : Node_Id; Data_Size : Natural; Property_Size_Name : constant String := "source_data_size"; begin W_Line ("Checking buses size... "); Buses_Set := Get_Instances_Of_Component_Type (C_Bus); Connections_Set := Get_Instances_Of_Component_Type (C_Connection); for I in 1 .. Cardinal (Buses_Set) loop -- 1/ We search all conenctions bound to a given bus -- instance Bus := Get (Buses_Set, I); Result := OCBP.Get_Instances_Verifying_Predicate (Connections_Set, Bus); -- 2/ We compute the size of the data passing through -- the bus' conenctions Data_Size := 0; for J in 1 .. Cardinal (Result) loop N := Item (Last_Node (Path (Source (Get (Result, J))))); if Is_Data (N) then -- find the corresponding data component instance N := Corresponding_Instance (N); if Is_Defined_Property (N, Property_Size_Name) then Data_Size := Data_Size + Get_Size_Property (N, Property_Size_Name); end if; end if; end loop; W_Str ("* The bus "); Write_Name (Compute_Full_Name_Of_Instance (Bus)); W_Line (" actual rate is " & Image (Int (Data_Size))); end loop; end Do_Check_Buses_Size; end Ocarina.Checker_Testsuite;