------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- 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.Text_IO; 		use Ada.Text_IO;
with Systems; 			use Systems;
with Dependencies; 		use Dependencies; 
with Task_Dependencies; 	use Task_Dependencies; 
with Task_Dependencies; 	use Task_Dependencies.Half_Dep_Set;
with Tasks;			use Tasks;
with Task_Set;                  use Task_Set;
with Message_Set ; 		use Message_Set; 
with Messages; 			use Messages; 
with MILS_Security;		use MILS_Security;
with Ada.Strings.Unbounded;     use Ada.Strings.Unbounded;
with Debug;                     use Debug;
with sets;

package body mils_analysis is 
 N: integer:=100;
 num_tasks: Tasks_Range:=0;
 type matrice is array (1 .. N, 1 .. N) of Integer ;

 M: matrice;
-- function bell_lapadula  (Sys : System; allowed_dependencies : Tasks_Dependencies_Ptr) return boolean is
 function bell_lapadula_Int  (Sys : System ) return Integer is 
      
      My_iterator: Tasks_Dependencies_Iterator;
      Dep_Ptr: Dependency_Ptr;
      My_dependencies: Tasks_Dependencies_Ptr;
      i: Integer:=0;
   begin
     
      My_dependencies:= Sys.Dependencies;
      if is_empty( My_dependencies.Depends) then 
         return 0;
      else 
      reset_iterator(My_dependencies.Depends, My_iterator);
      loop
         current_element(My_dependencies.Depends, Dep_Ptr, My_iterator);  
            if (Dep_Ptr.type_of_dependency=asynchronous_communication_dependency)then 
               if ((Dep_Ptr.asynchronous_communication_dependent_task.mils_task/=Downgrader) AND (Dep_Ptr.asynchronous_communication_dependent_task.mils_task/=Upgrader)) then

                  if((Dep_Ptr.asynchronous_communication_dependent_task.MILS_Confidentiality_Level < Dep_Ptr.asynchronous_communication_dependency_object.MILS_Confidentiality_Level) 
                     AND ((Dep_Ptr.asynchronous_communication_orientation= From_Object_To_Task) OR (Dep_Ptr.asynchronous_communication_orientation= From_Object_To_Task))) then
--                 Put_Line("Dep_Ptr.asynchronous_communication_dependent_task :" &  To_String(Dep_Ptr.asynchronous_communication_dependent_task.name));
--                 Put_Line("Dep_Ptr.asynchronous_communication_dependency_object :" &  To_String(Dep_Ptr.asynchronous_communication_dependency_object.name));
--                 Put_Line(" From_Object_To_Task" );
                     i:=i+1;
                  elsif ((Dep_Ptr.asynchronous_communication_dependency_object.MILS_Confidentiality_Level < Dep_Ptr.asynchronous_communication_dependent_task.MILS_Confidentiality_Level) 
                         AND (Dep_Ptr.asynchronous_communication_orientation= From_Task_To_Object)) Then
--                 Put_Line("Dep_Ptr.asynchronous_communication_dependent_task :" &  To_String(Dep_Ptr.asynchronous_communication_dependent_task.name));
--                 Put_Line("Dep_Ptr.asynchronous_communication_dependency_object :" &  To_String(Dep_Ptr.asynchronous_communication_dependency_object.name));
--                 Put_Line(" From_Task_To_Object" );
                     i:=i+1;
                  end if;
               end if;

            elsif(Dep_Ptr.type_of_dependency=precedence_dependency)then

               if (Dep_Ptr.precedence_sink.mils_confidentiality_level<Dep_Ptr.precedence_source.mils_confidentiality_level) then 
                  if ((Dep_Ptr.precedence_source.mils_task/=Downgrader) AND (Dep_Ptr.precedence_source.mils_task/=Upgrader)AND
                        (Dep_Ptr.precedence_sink.mils_task/=Downgrader)AND (Dep_Ptr.precedence_sink.mils_task/=Upgrader)) then
                     i:=i+1;
--                    Put_Line(" bell precedence_source :" &  To_String(Dep_Ptr.precedence_source.name));
--                    Put_Line("bell precedence_sink :" &  To_String(Dep_Ptr.precedence_sink.name));
                  end if; 
               end if;
            end if; 			
         exit when is_last_element (My_Dependencies.Depends, My_Iterator);
            next_element (My_Dependencies.Depends, My_Iterator);
         end loop;		 		
         return i;
      end if;
   end bell_lapadula_Int;
   
   function bell_lapadula  (Sys : System ) return Boolean is 
      j:Integer:=0;
   Begin
      j:=bell_lapadula_Int(Sys);
      Put_Debug("bell_lapadula_int:" & j'Img);
      if (j=0) then 
         return True;
      else 
         return False;
      end if;
   
   end bell_lapadula;

   function biba_Int (Sys : System) return Integer is
      My_iterator: Tasks_Dependencies_Iterator;
      Dep_Ptr: Dependency_Ptr;
      My_dependencies: Tasks_Dependencies_Ptr;
      i: Integer:=0;
   begin

      My_dependencies := Sys.Dependencies;
      if is_empty( My_dependencies.Depends) then 
         return 0;
         else 
      reset_iterator(My_dependencies.Depends, My_iterator);
      loop
            current_element(My_dependencies.Depends, Dep_Ptr, My_iterator);
            
            if (Dep_Ptr.type_of_dependency=asynchronous_communication_dependency)then 
               
               if ((Dep_Ptr.asynchronous_communication_dependent_task.mils_task/=Downgrader) AND (Dep_Ptr.asynchronous_communication_dependent_task.mils_task/=Upgrader)) then
              
                  if ((Dep_Ptr.asynchronous_communication_dependency_object.mils_integrity_level < Dep_Ptr.asynchronous_communication_dependent_task.mils_integrity_level) 
                      AND (Dep_Ptr.asynchronous_communication_orientation= From_Object_To_Task)) Then
--                 Put_Line("Dep_Ptr.asynchronous_communication_dependent_task :" &  To_String(Dep_Ptr.asynchronous_communication_dependent_task.name));
--                 Put_Line("Dep_Ptr.asynchronous_communication_dependency_object :" &  To_String(Dep_Ptr.asynchronous_communication_dependency_object.name));
--                 Put_Line(" From_Object_To_Task" );
                     i:=i+1;
                  elsif((Dep_Ptr.asynchronous_communication_dependent_task.mils_integrity_level < Dep_Ptr.asynchronous_communication_dependency_object.mils_integrity_level) 
                     AND (Dep_Ptr.asynchronous_communication_orientation= From_Task_To_Object)) then
--                 Put_Line("Dep_Ptr.asynchronous_communication_dependent_task :" &  To_String(Dep_Ptr.asynchronous_communication_dependent_task.name));
--                 Put_Line("Dep_Ptr.asynchronous_communication_dependency_object :" &  To_String(Dep_Ptr.asynchronous_communication_dependency_object.name));
--                 Put_Line(" From_Task_To_Object" );
                     i:=i+1;
                  end if; 
                  end if;

            elsif (Dep_Ptr.type_of_dependency=remote_procedure_call_dependency)then
               if ((Dep_Ptr.remote_procedure_call_server.mils_task/=Downgrader) AND (Dep_Ptr.remote_procedure_call_server.mils_task/=Upgrader)AND
                     (Dep_Ptr.remote_procedure_call_client.mils_task/=Downgrader)AND (Dep_Ptr.remote_procedure_call_client.mils_task/=Upgrader)) then
                      
                  if(Dep_Ptr.remote_procedure_call_server.mils_integrity_level < Dep_Ptr.remote_procedure_call_client.mils_integrity_level) then

--                       Put_Line("remote_procedure_call_server :" &  To_String(Dep_Ptr.remote_procedure_call_server.name));
--                       Put_Line("remote_procedure_call_client :" &  To_String(Dep_Ptr.remote_procedure_call_client.name));
                         i:=i+1;
                   end if; 
                   end if;
                   
            elsif(Dep_Ptr.type_of_dependency=precedence_dependency)then

               if (Dep_Ptr.precedence_source.mils_integrity_level<Dep_Ptr.precedence_sink.mils_integrity_level) then
                                                
                  if ((Dep_Ptr.precedence_source.mils_task/=Downgrader) AND (Dep_Ptr.precedence_source.mils_task/=Upgrader)AND
                 (Dep_Ptr.precedence_sink.mils_task/=Downgrader)AND (Dep_Ptr.precedence_sink.mils_task/=Upgrader)) then
                     i:=i+1;
--                    Put_Line("biba precedence_source :" &  To_String(Dep_Ptr.precedence_source.name));
--                    Put_Line("biba precedence_sink :" &  To_String(Dep_Ptr.precedence_sink.name));                 
                  
                  end if; 
               end if;
               end if;
               exit when is_last_element (My_Dependencies.Depends, My_Iterator);
               next_element (My_Dependencies.Depends, My_Iterator);
         end loop;
         return i;
         end if;
   end biba_Int;
   
   function biba (Sys : System) return boolean is
      j:Integer:=0;
   begin
      j:= biba_Int(Sys);
      Put_Debug("Biba_int:" & j'Img);
      if(j=0) then
         return True;
      else
         return False;
      end if;
      
   end biba;

   procedure Warshall(Sys: System) is
      My_iterator: Tasks_Dependencies_Iterator;
      My_iterator1: Tasks_Dependencies_Iterator;
      Dep_Ptr: Dependency_Ptr;
      Dep_Ptr1: Dependency_Ptr;
      My_dependencies: Tasks_Dependencies_Ptr;
      My_dependencies2: Tasks_Dependencies_Ptr;

      
   begin
      for i in 1..N loop
         for j in 1.. N loop
            M(i,j):=0;
         end loop;
      end loop;
      num_tasks:= Get_Number_Of_Task_From_Processor(My_tasks => Sys.Tasks,
                                                    Processor_Name => To_Unbounded_String("Processor"));
      My_dependencies := Sys.Dependencies;
      reset_iterator(My_dependencies.Depends, My_iterator);
      loop
         current_element(My_dependencies.Depends, Dep_Ptr, My_iterator);
         if (Dep_Ptr.type_of_dependency=asynchronous_communication_dependency)then 
            if (Dep_Ptr.asynchronous_communication_orientation= From_Task_To_Object)then
               My_dependencies2 :=Sys.Dependencies;
               reset_iterator(My_dependencies2.Depends, My_iterator1);
               loop
                  current_element(My_dependencies2.Depends, Dep_Ptr1, My_iterator1);
                  if (Dep_Ptr1.type_of_dependency=asynchronous_communication_dependency)then
                     if(( Dep_Ptr.asynchronous_communication_dependency_object.name=Dep_Ptr1.asynchronous_communication_dependency_object.name)
                        AND (Dep_Ptr1.asynchronous_communication_orientation= From_Object_To_Task)) then
                        M(Integer'Value(To_String(Dep_Ptr.asynchronous_communication_dependent_task.name)),Integer'Value(To_String(Dep_Ptr1.asynchronous_communication_dependent_task.name))):=1;
     
                     end if;
                  end if;
                  exit when is_last_element (My_dependencies2.Depends, My_Iterator1);
                  next_element (My_dependencies2.Depends, My_Iterator1);
               end loop;
            end if;
         elsif (Dep_Ptr.type_of_dependency=remote_procedure_call_dependency)then
            M(Integer'Value(To_String(Dep_Ptr.remote_procedure_call_server.name)),Integer'Value(To_String(Dep_Ptr.remote_procedure_call_client.name))):=1;
            
         elsif(Dep_Ptr.type_of_dependency=precedence_dependency)then
            M(Integer'Value(To_String(Dep_Ptr.precedence_source.name)),Integer'Value(To_String(Dep_Ptr.precedence_sink.name))):=1;
            
         elsif(Dep_Ptr.type_of_dependency=queueing_buffer_dependency)then
            if (Dep_Ptr.buffer_orientation= From_Task_To_Object)then
               My_dependencies2 :=Sys.Dependencies;
               reset_iterator(My_dependencies2.Depends, My_iterator1);
               loop
                  current_element(My_dependencies2.Depends, Dep_Ptr1, My_iterator1); 
                  if (Dep_Ptr1.type_of_dependency=queueing_buffer_dependency)then
                     if(( Dep_Ptr.buffer_dependency_object.name=Dep_Ptr1.buffer_dependency_object.name)
                        AND (Dep_Ptr1.buffer_orientation= From_Object_To_Task)) Then
                        M(Integer'Value(To_String(Dep_Ptr.buffer_dependent_task.name)),Integer'Value(To_String(Dep_Ptr1.buffer_dependent_task.name))):=1;
                     end if;
                  end if;
                  exit when is_last_element (My_dependencies2.Depends, My_Iterator1);
                  next_element (My_dependencies2.Depends, My_Iterator1);
                  end loop;
            end if;
            end if;
         exit when is_last_element (My_Dependencies.Depends, My_Iterator);
         next_element (My_Dependencies.Depends, My_Iterator);
      end loop;
      for a in 1..Natural(num_tasks) loop
         for i in 1..Natural(num_tasks) loop
            for j in 1..Natural(num_tasks) loop
               for k in 1..Natural(num_tasks) loop
                  if (M(i,k)*M(k,j)=1) then
                    M(i, j):=1;
               end if;
            end loop;
         end loop;
      end loop;
      end loop;
        
   end Warshall;

   function chinese_wall_Int (Sys : System; COIs : array_tasks_set)  return Integer is
      My_COI_tasks: Tasks_Set;
      Tasks_Ptr: Generic_Task_Ptr; 
      Tasks_Ptr1: Generic_Task_Ptr;
      My_iterator:Tasks_Iterator;
      My_iterator1:Tasks_Iterator;
      k:Integer:=0;
   begin
      Warshall(Sys);
         Put_Line("Tasks_Number "&num_tasks'img);
         for i in 1..Natural(num_tasks) loop
            for j in 1..Natural(num_tasks) loop
                 Put_Line(" "&M(i,j)'img);
            end loop;
         end loop;
      for i in COIs'Range loop
         My_COI_tasks:=COIs(i);
         reset_iterator (COIs(i), My_Iterator);
         loop 
            current_element(COIs(i),Tasks_Ptr,My_iterator);
            reset_iterator (My_COI_tasks, My_Iterator1);
            loop
               current_element(My_COI_tasks,Tasks_Ptr1,My_iterator1);
               if ((Tasks_Ptr.name/=Tasks_Ptr1.name)AND ( M(Integer'Value(To_String(Tasks_Ptr.name)), Integer'Value(To_String(Tasks_Ptr1.name)))=1)) Then
                  k:=k+1;
               end if;
               exit when is_last_element (My_COI_tasks, My_Iterator1);
               next_element (My_COI_tasks, My_Iterator1);  
            end loop;
            exit when is_last_element (COIs(i), My_Iterator);
            next_element (COIs(i), My_Iterator);
         end loop;
      end loop;
    return k;
   end chinese_wall_Int;
   
    function chinese_wall (Sys : System; COIs : array_tasks_set)  return boolean is
      
      i:Integer:=0;
   begin
      i:= chinese_wall_Int(Sys,COIs);
      Put_Debug("chinese_wall_Int:" & i'Img);
      if(i=0) then
         return True;
      else
         return False;
      end if;
      
      end chinese_wall;
   
   
end mils_analysis;