------------------------------------------------- ------------------------------- -- -- -- OCARINA COMPONENTS -- -- -- -- O C A R I N A . A N A L Y Z E R . L E G A L I T Y _ R U L E S -- -- -- -- B o d y -- -- -- -- Copyright (C) 2006-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) -- -- -- ------------------------------------------------------------------------------ with Locations; with Ocarina.Nodes; with Ocarina.Nutils; with Ocarina.Analyzer.Messages; with Ocarina.Entities.Components.Connections; package body Ocarina.Analyzer.Legality_Rules is use Locations; use Ocarina.Nodes; use Ocarina.Nutils; use Ocarina.Analyzer.Messages; use Ocarina.Entities.Components; use Ocarina.Entities.Components.Connections; function Check_Rules_In_Component_Type (Node : node_id; Rules : aadl_legality_rules) return Boolean; function Check_Rules_In_Component_Implementation (Node : node_id; Rules : aadl_legality_rules) return Boolean; ---------------------------- -- A_Component_Connection -- ---------------------------- function A_Component_Connection (Component : node_id; Connection : node_id; Rules : aadl_legality_rules) return Boolean is pragma assert (Present (Component) and then Present (Connection)); pragma unreferenced (Rules); OK : Boolean; Component_Categ : component_category; Connection_Categ : connection_type; begin if Kind (Component) /= k_component_implementation then DAE (Loc => Loc (Component), Node1 => Component, Message1 => " is not a component implementation"); return False; end if; if Kind (Connection) /= k_connection then DAE (Loc => Loc (Connection), Node1 => Connection, Message1 => " is not a connection."); return False; end if; -- Check the validity of the composition Component_Categ := component_category'val (Category (Component)); Connection_Categ := connection_type'val (Category (Connection)); case Component_Categ is when cc_data => OK := Connection_Categ = ct_access_bus or else Connection_Categ = ct_access_data; when cc_subprogram | cc_system | cc_threadgroup | cc_process | cc_thread => OK := True; when cc_bus | cc_processor | cc_memory | cc_device | cc_unknown => OK := False; end case; if OK then return True; else DAE (Loc => Loc (Connection), Node1 => Component, Node2 => Connection, Message1 => "cannot have ", Message2 => " as a connection"); return False; end if; end A_Component_Connection; ------------------------- -- A_Component_Feature -- ------------------------- function A_Component_Feature (Component : node_id; Feature : node_id; Rules : aadl_legality_rules) return Boolean is pragma assert (Present (Component) and then Present (Feature)); OK : Boolean; Component_Categ : component_category; begin if Kind (Component) /= k_component_type and then not Is_Refinement (Feature) then DAE (Loc => Loc (Component), Node1 => Component, Message1 => " is not a component type"); return False; end if; if Kind (Feature) /= k_port_group_spec and then Kind (Feature) /= k_port_spec and then Kind (Feature) /= k_parameter and then Kind (Feature) /= k_subprogram_spec and then Kind (Feature) /= k_subcomponent_access then DAE (Loc => Loc (Feature), Node1 => Feature, Message1 => " not a feature."); return False; end if; -- Check the validity of the composition Component_Categ := component_category'val (Category (Component)); case Rules is when standard => case Component_Categ is when cc_data => OK := (Kind (Feature) = k_subprogram_spec or else (Kind (Feature) = k_subcomponent_access and then Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_data)); when cc_subprogram => OK := Kind (Feature) = k_parameter or else Kind (Feature) = k_port_group_spec or else (Kind (Feature) = k_subcomponent_access and then not Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_data) or else (Kind (Feature) = k_port_spec and then not Is_In (Feature) and then Is_Event (Feature)); when cc_thread | cc_threadgroup | cc_process => OK := Kind (Feature) = k_port_group_spec or else Kind (Feature) = k_port_spec or else (Kind (Feature) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Feature)) = cc_data) or else (Kind (Feature) = k_subprogram_spec and then Is_Server (Feature)); when cc_processor => OK := ((Kind (Feature) = k_subprogram_spec and then Is_Server (Feature)) or else Kind (Feature) = k_port_spec or else Kind (Feature) = k_port_group_spec or else (Kind (Feature) = k_subcomponent_access and then not Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_bus)); when cc_memory | cc_bus => OK := Kind (Feature) = k_subcomponent_access and then not Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_bus; when cc_device => OK := Kind (Feature) = k_port_group_spec or else Kind (Feature) = k_port_spec or else (Kind (Feature) = k_subprogram_spec and then Is_Server (Feature)) or else (Kind (Feature) = k_subcomponent_access and then not Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_bus); when cc_system => OK := (Kind (Feature) = k_subprogram_spec and then Is_Server (Feature)) or else Kind (Feature) = k_port_spec or else Kind (Feature) = k_port_group_spec or else Kind (Feature) = k_subcomponent_access; when others => OK := False; end case; when devel => case Component_Categ is when cc_data => OK := (Kind (Feature) = k_subprogram_spec or else (Kind (Feature) = k_subcomponent_access and then Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_data)); when cc_subprogram => OK := Kind (Feature) = k_parameter or else Kind (Feature) = k_port_group_spec or else (Kind (Feature) = k_subcomponent_access and then not Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_data) or else (Kind (Feature) = k_subcomponent_access and then not Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_subprogram) or else (Kind (Feature) = k_port_spec and then not Is_In (Feature) and then Is_Event (Feature)); when cc_thread | cc_threadgroup | cc_process => OK := Kind (Feature) = k_port_group_spec or else Kind (Feature) = k_port_spec or else (Kind (Feature) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Feature)) = cc_data) or else (Kind (Feature) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Feature)) = cc_subprogram) or else (Kind (Feature) = k_subprogram_spec and then Is_Server (Feature)); when cc_processor => OK := ((Kind (Feature) = k_subprogram_spec and then Is_Server (Feature)) or else Kind (Feature) = k_port_spec or else Kind (Feature) = k_port_group_spec or else (Kind (Feature) = k_subcomponent_access and then not Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_data)); when cc_memory | cc_bus => OK := Kind (Feature) = k_subcomponent_access and then not Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_bus; when cc_device => OK := Kind (Feature) = k_port_group_spec or else Kind (Feature) = k_port_spec or else (Kind (Feature) = k_subprogram_spec and then Is_Server (Feature)) or else (Kind (Feature) = k_subcomponent_access and then not Is_Provided (Feature) and then component_category'val (Subcomponent_Category (Feature)) = cc_data); when cc_system => OK := (Kind (Feature) = k_subprogram_spec and then Is_Server (Feature)) or else Kind (Feature) = k_port_spec or else Kind (Feature) = k_port_group_spec or else Kind (Feature) = k_subcomponent_access; when others => OK := False; end case; end case; if OK then return True; else DAE (Loc => Loc (Feature), Node1 => Component, Node2 => Feature, Message1 => "cannot have ", Message2 => " as a feature"); return False; end if; end A_Component_Feature; ---------------------- -- A_Component_Flow -- ---------------------- function A_Component_Flow (Component : node_id; Flow : node_id; Rules : aadl_legality_rules) return Boolean is pragma assert (Present (Component) and then Present (Flow)); pragma unreferenced (Rules); OK : Boolean; Component_Categ : component_category; begin if Kind (Component) /= k_component_implementation then DAE (Loc => Loc (Component), Node1 => Component, Message1 => " is not a component implementation"); return False; end if; if Kind (Flow) /= k_flow_implementation and then Kind (Flow) /= k_end_to_end_flow_spec and then Kind (Flow) /= k_flow_implementation_refinement and then Kind (Flow) /= k_end_to_end_flow_refinement then DAE (Loc => Loc (Flow), Node1 => Flow, Message1 => " is not a flow."); return False; end if; -- Check the validity of the composition Component_Categ := component_category'val (Category (Component)); case Component_Categ is when cc_subprogram | cc_system | cc_threadgroup | cc_thread | cc_process | cc_processor | cc_device => OK := True; when cc_data | cc_bus | cc_memory | cc_unknown => OK := False; end case; if OK then return True; else DAE (Loc => Loc (Flow), Node1 => Component, Node2 => Flow, Message1 => "cannot have ", Message2 => " as a flow"); return False; end if; end A_Component_Flow; ------------------------------------ -- A_Component_Flow_Specification -- ------------------------------------ function A_Component_Flow_Specification (Component : node_id; Flow_Spec : node_id; Rules : aadl_legality_rules) return Boolean is pragma assert (Present (Component) and then Present (Flow_Spec)); pragma unreferenced (Rules); OK : Boolean; Component_Categ : component_category; begin if Kind (Component) /= k_component_type then DAE (Loc => Loc (Component), Node1 => Component, Message1 => " is not a component type"); return False; end if; if Kind (Flow_Spec) /= k_flow_spec then DAE (Loc => Loc (Flow_Spec), Node1 => Flow_Spec, Message1 => " is not a flow specification."); return False; end if; -- Check the validity of the composition Component_Categ := component_category'val (Category (Component)); case Component_Categ is when cc_subprogram | cc_system | cc_threadgroup | cc_thread | cc_process | cc_processor | cc_device => OK := True; when cc_data | cc_bus | cc_memory | cc_unknown => OK := False; end case; if OK then return True; else DAE (Loc => Loc (Flow_Spec), Node1 => Component, Node2 => Flow_Spec, Message1 => "cannot have ", Message2 => " as a flow specification"); return False; end if; end A_Component_Flow_Specification; ------------------------------ -- A_Component_Subcomponent -- ------------------------------ function A_Component_Subcomponent (Component : node_id; Subcomponent : node_id; Rules : aadl_legality_rules) return Boolean is pragma assert (Present (Component) and then Present (Subcomponent)); OK : Boolean; Component_Categ : component_category; Subcomponent_Categ : component_category; begin if Kind (Component) /= k_component_implementation then DAE (Loc => Loc (Component), Node1 => Component, Message1 => " is not a component implementation"); return False; end if; if Kind (Subcomponent) /= k_subcomponent then DAE (Loc => Loc (Subcomponent), Node1 => Subcomponent, Message1 => " is not a subcomponent"); return False; end if; -- Check the validity of the composition Component_Categ := component_category'val (Category (Component)); Subcomponent_Categ := component_category'val (Category (Subcomponent)); case Rules is when standard => case Component_Categ is when cc_data => case Subcomponent_Categ is when cc_data => OK := True; when others => OK := False; end case; when cc_subprogram | cc_bus | cc_device => OK := False; when cc_thread => case Subcomponent_Categ is when cc_data => OK := True; when others => OK := False; end case; when cc_threadgroup | cc_process => case Subcomponent_Categ is when cc_data | cc_thread | cc_threadgroup => OK := True; when others => OK := False; end case; when cc_memory | cc_processor => case Subcomponent_Categ is when cc_memory => OK := True; when others => OK := False; end case; when cc_system => case Subcomponent_Categ is when cc_data | cc_process | cc_processor | cc_memory | cc_device | cc_bus | cc_system => OK := True; when others => OK := False; end case; when others => OK := False; end case; when devel => case Component_Categ is when cc_data => case Subcomponent_Categ is when cc_data => OK := True; when others => OK := False; end case; when cc_bus | cc_device => OK := False; when cc_subprogram => case Subcomponent_Categ is when cc_data => OK := True; when others => OK := False; end case; when cc_thread => case Subcomponent_Categ is when cc_data | cc_subprogram => OK := True; when others => OK := False; end case; when cc_threadgroup | cc_process => case Subcomponent_Categ is when cc_data | cc_thread | cc_threadgroup | cc_subprogram => OK := True; when others => OK := False; end case; when cc_memory | cc_processor => case Subcomponent_Categ is when cc_memory => OK := True; when others => OK := False; end case; when cc_system => case Subcomponent_Categ is when cc_data | cc_process | cc_processor | cc_memory | cc_device | cc_bus | cc_system => OK := True; when others => OK := False; end case; when others => OK := False; end case; end case; if OK then return True; else DAE (Loc => Loc (Subcomponent), Node1 => Component, Node2 => Subcomponent, Message1 => "cannot have ", Message2 => " as a subcomponent"); return False; end if; end A_Component_Subcomponent; ------------------------------------------ -- A_Component_Subprogram_Call_Sequence -- ------------------------------------------ function A_Component_Subprogram_Call_Sequence (Component : node_id; Subprogram_Call_Seq : node_id; Rules : aadl_legality_rules) return Boolean is pragma assert (Present (Component) and then Present (Subprogram_Call_Seq)); pragma unreferenced (Rules); OK : Boolean; Component_Categ : component_category; begin if Kind (Component) /= k_component_implementation then DAE (Loc => Loc (Component), Node1 => Component, Message1 => " is not a component implementation"); return False; end if; if Kind (Subprogram_Call_Seq) /= k_subprogram_call_sequence then DAE (Loc => Loc (Subprogram_Call_Seq), Node1 => Subprogram_Call_Seq, Message1 => " is not a subprogram call sequence."); return False; end if; -- Check the validity of the composition Component_Categ := component_category'val (Category (Component)); case Component_Categ is when cc_subprogram | cc_thread => OK := True; when cc_data | cc_threadgroup | cc_process | cc_bus | cc_processor | cc_memory | cc_device | cc_system | cc_unknown => OK := False; end case; if OK then return True; else DAE (Loc => Loc (Subprogram_Call_Seq), Node1 => Component, Node2 => Subprogram_Call_Seq, Message1 => "cannot have ", Message2 => " as a subprogram call"); return False; end if; end A_Component_Subprogram_Call_Sequence; ----------------------------------- -- Check_Rules_In_Component_Type -- ----------------------------------- function Check_Rules_In_Component_Type (Node : node_id; Rules : aadl_legality_rules) return Boolean is pragma assert (Kind (Node) = k_component_type); List_Node : node_id; Success : Boolean := True; begin -- Features if not Is_Empty (Features (Node)) then List_Node := First_Node (Features (Node)); while Present (List_Node) loop Success := A_Component_Feature (Node, List_Node, Rules) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Flows if not Is_Empty (Flows (Node)) then List_Node := First_Node (Flows (Node)); while Present (List_Node) loop Success := A_Component_Flow_Specification (Node, List_Node, Rules) and then Success; List_Node := Next_Node (List_Node); end loop; end if; return Success; end Check_Rules_In_Component_Type; --------------------------------------------- -- Check_Rules_In_Component_Implementation -- --------------------------------------------- function Check_Rules_In_Component_Implementation (Node : node_id; Rules : aadl_legality_rules) return Boolean is pragma assert (Kind (Node) = k_component_implementation); List_Node : node_id; Success : Boolean := True; begin -- Type refinements if not Is_Empty (Refines_Type (Node)) then List_Node := First_Node (Refines_Type (Node)); while Present (List_Node) loop Success := A_Component_Feature (Node, List_Node, Rules) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Subcomponents if not Is_Empty (Subcomponents (Node)) then List_Node := First_Node (Subcomponents (Node)); while Present (List_Node) loop Success := A_Component_Subcomponent (Node, List_Node, Rules) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Call sequences if not Is_Empty (Calls (Node)) then List_Node := First_Node (Calls (Node)); while Present (List_Node) loop Success := A_Component_Subprogram_Call_Sequence (Node, List_Node, Rules) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Connections if not Is_Empty (Ocarina.Nodes.Connections (Node)) then List_Node := First_Node (Ocarina.Nodes.Connections (Node)); while Present (List_Node) loop Success := A_Component_Connection (Node, List_Node, Rules) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Flows if not Is_Empty (Flows (Node)) then List_Node := First_Node (Flows (Node)); while Present (List_Node) loop Success := A_Component_Flow (Node, List_Node, Rules) and then Success; List_Node := Next_Node (List_Node); end loop; end if; return Success; end Check_Rules_In_Component_Implementation; -------------------------- -- Check_Legality_Rules -- -------------------------- function Check_Legality_Rules (Root : node_id; Options : analyzer_options) return Boolean is pragma assert (Kind (Root) = k_aadl_specification); List_Node : node_id; Package_List_Node : node_id; Success : Boolean := True; begin if not Is_Empty (Declarations (Root)) then List_Node := First_Node (Declarations (Root)); while Present (List_Node) loop case Kind (List_Node) is when k_component_type => Success := Check_Rules_In_Component_Type (List_Node, Options.Legality_Rules) and then Success; when k_component_implementation => Success := Check_Rules_In_Component_Implementation (List_Node, Options.Legality_Rules) and then Success; when k_package_specification => if not Is_Empty (Declarations (List_Node)) then Package_List_Node := First_Node (Declarations (List_Node)); while Package_List_Node /= No_Node loop case Kind (Package_List_Node) is when k_component_type => Success := Check_Rules_In_Component_Type (Package_List_Node, Options.Legality_Rules) and then Success; when k_component_implementation => Success := Check_Rules_In_Component_Implementation (Package_List_Node, Options.Legality_Rules) and then Success; when others => null; end case; Package_List_Node := Next_Node (Package_List_Node); end loop; end if; when others => null; end case; List_Node := Next_Node (List_Node); end loop; end if; return Success; end Check_Legality_Rules; end Ocarina.Analyzer.Legality_Rules;