Commit e438a919 authored by yoogx's avatar yoogx
Browse files

* Add generation of Ada 2012 and SPARK 2014 aspects for

          PolyORB-HI/Ada.

          As part of this change, the Job function of thread is now a procedure

          For openaadl/ocarina#132
parent 92057e35
.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.10.
.TH OCARINA "1" "mars 2016" "Ocarina 2.0w" "User Commands"
.TH OCARINA "1" "mars 2018" "Ocarina 2017.x" "User Commands"
.SH NAME
Ocarina \- manual page for Ocarina 2.0w
Ocarina \- manual page for Ocarina 2017.x
.SH SYNOPSIS
.B ocarina-config
[\fIOPTIONS\fR]
......
<!-- Creator : groff version 1.19.2 -->
<!-- CreationDate: Fri Mar 4 09:18:49 2016 -->
<!-- CreationDate: Sat Mar 3 22:09:49 2018 -->
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
......@@ -33,7 +33,7 @@
<p style="margin-left:11%; margin-top: 1em">Ocarina &minus;
manual page for Ocarina 2.0w</p>
manual page for Ocarina 2017.x</p>
<a name="SYNOPSIS"></a>
<h2>SYNOPSIS</h2>
......
.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.40.10.
.TH OCARINA "1" "mars 2016" "Ocarina 2.0w (Working Copy from rb472173)" "User Commands"
.TH OCARINA "1" "mars 2018" "Ocarina 2017.x (Working Copy from rc134071)" "User Commands"
.SH NAME
Ocarina \- manual page for Ocarina 2.0w (Working Copy from rb472173)
Ocarina \- manual page for Ocarina 2017.x (Working Copy from rc134071)
.SH SYNOPSIS
.B ocarina
[\fIswitches\fR] \fI<aadl_files>\fR
......@@ -60,6 +60,9 @@ Generate code using Ocarina backend 'ARG'
\fB\-\-list\-backends\fR
List available backends
.TP
\fB\-\-spark2014\fR
Generate SPARK2014 annotations
.TP
\fB\-b\fR
Compile generated code
.TP
......@@ -73,7 +76,7 @@ Set POK flavor (arinc653/deos/pok/vxworks)
Run Ocarina in terminal interactive mode
.TP
\fB\-real_theorem\fR ARG
Name of the main theorem to evaluate
Name of the main REAL theorem to evaluate
.TP
\fB\-real_lib\fR ARG
Add external library of REAL theorems
......@@ -96,7 +99,7 @@ Generate ASN1 deployment file (PolyORB\-HI\-C only)
\fB\-perf\fR
Enable profiling with gprof (PolyORB\-HI\-C only)
.SH COPYRIGHT
Copyright \(co 2003\-2009 Telecom ParisTech, 2010\-2016 ESA & ISAE
Copyright \(co 2003\-2009 Telecom ParisTech, 2010\-2018 ESA & ISAE
Build date:
.SH "SEE ALSO"
The full documentation for
......
<!-- Creator : groff version 1.19.2 -->
<!-- CreationDate: Fri Mar 4 09:18:50 2016 -->
<!-- CreationDate: Sat Mar 3 22:09:49 2018 -->
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
......@@ -34,8 +34,8 @@
<p style="margin-left:11%; margin-top: 1em">Ocarina &minus;
manual page for Ocarina 2.0w (Working Copy from
rb472173)</p>
manual page for Ocarina 2017.x (Working Copy from
rc134071)</p>
<a name="SYNOPSIS"></a>
<h2>SYNOPSIS</h2>
......@@ -270,6 +270,12 @@ Ocarina backend &rsquo;ARG&rsquo;</p></td>
<p style="margin-left:22%;">List available backends</p>
<p style="margin-left:11%;"><b>&minus;&minus;spark2014</b></p>
<p style="margin-left:22%;">Generate SPARK2014
annotations</p>
<table width="100%" border=0 rules="none" frame="void"
cellspacing="0" cellpadding="0">
<tr valign="top" align="left">
......@@ -337,8 +343,8 @@ terminal interactive mode</p></td>
<p style="margin-left:11%;"><b>&minus;real_theorem</b>
ARG</p>
<p style="margin-left:22%;">Name of the main theorem to
evaluate</p>
<p style="margin-left:22%;">Name of the main REAL theorem
to evaluate</p>
<p style="margin-left:11%;"><b>&minus;real_lib</b> ARG</p>
......@@ -425,7 +431,7 @@ with gprof (PolyORB&minus;HI&minus;C only)</p></td>
<p style="margin-left:11%; margin-top: 1em">Copyright
&copy; 2003&minus;2009 Telecom ParisTech, 2010&minus;2016
&copy; 2003&minus;2009 Telecom ParisTech, 2010&minus;2018
ESA &amp; ISAE Build date:</p>
<a name="SEE ALSO"></a>
......
......@@ -18,11 +18,12 @@ Usage: ocarina [switches] <aadl_files>
-x Parse AADL file as an AADL scenario file
-g ARG Generate code using Ocarina backend 'ARG'
--list-backends List available backends
--spark2014 Generate SPARK2014 annotations
-b Compile generated code
-z Clean code generated
-k ARG Set POK flavor (arinc653/deos/pok/vxworks)
-t Run Ocarina in terminal interactive mode
-real_theorem ARG Name of the main theorem to evaluate
-real_theorem ARG Name of the main REAL theorem to evaluate
-real_lib ARG Add external library of REAL theorems
-real_continue_eval Continue evaluation of REAL theorems after first failure (REAL backend)
-boundt_process ARG Generate .tpo file for process ARG (Bound-T backend)
......
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2017 ESA & ISAE. --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2018 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -81,6 +81,32 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
function Wait_For_Incoming_Events_Spec (E : Node_Id) return Node_Id;
-- Runtime routines provided for each AADL thread
function Runtime_Spec_Aspect_Definition return Node_Id;
-- Build aspect definition for runtime services
------------------------------------
-- Runtime_Spec_Aspect_Definition --
------------------------------------
function Runtime_Spec_Aspect_Definition return Node_Id is
begin
if Add_SPARK2014_Annotations then
return Make_Aspect_Specification
(Make_List_Id
(Make_Aspect (ASN (A_Volatile_Function)),
Make_Aspect
(ASN (A_Global),
Make_Global_Specification
(Make_List_Id
(Make_Moded_Global_List
(Mode_In,
Make_Defining_Identifier
(PN (P_Elaborated_Variables))))))));
else
return No_Node;
end if;
end Runtime_Spec_Aspect_Definition;
----------------------
-- Send_Output_Spec --
----------------------
......@@ -105,7 +131,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Subtype_Mark =>
Make_Defining_Identifier (Map_Port_Enumeration_Name (E)),
Parameter_Mode => Mode_In)),
Return_Type => RE (RE_Error_Kind));
Return_Type => RE (RE_Error_Kind),
Aspect_Specification => Runtime_Spec_Aspect_Definition);
return N;
end Send_Output_Spec;
......@@ -191,8 +218,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Make_Defining_Identifier (Map_Port_Enumeration_Name (E)),
Parameter_Mode => Mode_In)),
Return_Type =>
Make_Defining_Identifier (Map_Port_Interface_Name (E)));
Make_Defining_Identifier (Map_Port_Interface_Name (E)),
Aspect_Specification => Runtime_Spec_Aspect_Definition);
return N;
end Get_Value_Spec;
......@@ -219,7 +246,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Subtype_Mark =>
Make_Defining_Identifier (Map_Port_Enumeration_Name (E)),
Parameter_Mode => Mode_In)),
Return_Type => RE (RE_Entity_Type));
Return_Type => RE (RE_Entity_Type),
Aspect_Specification => Runtime_Spec_Aspect_Definition);
return N;
end Get_Sender_Spec;
......@@ -247,7 +275,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Subtype_Mark =>
Make_Defining_Identifier (Map_Port_Enumeration_Name (E)),
Parameter_Mode => Mode_In)),
Return_Type => RE (RE_Integer));
Return_Type => RE (RE_Integer),
Aspect_Specification => Runtime_Spec_Aspect_Definition);
return N;
end Get_Count_Spec;
......@@ -276,7 +305,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Subtype_Mark =>
Make_Defining_Identifier (Map_Port_Enumeration_Name (E)),
Parameter_Mode => Mode_In)),
Return_Type => RE (RE_Time));
Return_Type => RE (RE_Time),
Aspect_Specification => Runtime_Spec_Aspect_Definition);
return N;
end Get_Time_Stamp_Spec;
......@@ -903,20 +933,33 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
or else P = Thread_Hybrid
or else P = Thread_Aperiodic
then
N :=
Make_Parameter_Specification
(Defining_Identifier => Make_Defining_Identifier (PN (P_Port)),
Subtype_Mark =>
Make_Defining_Identifier (Map_Port_Enumeration_Name (E)));
Param_List := Make_List_Id (N);
Param_List := Make_List_Id
(Make_Parameter_Specification
(Defining_Identifier =>
Make_Defining_Identifier (PN (P_Port)),
Subtype_Mark =>
Make_Defining_Identifier (Map_Port_Enumeration_Name (E))),
Make_Parameter_Specification
(Defining_Identifier => Make_Defining_Identifier
(PN (P_Result)),
Subtype_Mark => RE (RE_Error_Kind),
Parameter_Mode => Mode_Out));
elsif P = Thread_Periodic
or else P = Thread_Background
then
Param_List := Make_List_Id
(Make_Parameter_Specification
(Defining_Identifier => Make_Defining_Identifier
(PN (P_Result)),
Subtype_Mark => RE (RE_Error_Kind),
Parameter_Mode => Mode_Out));
end if;
N :=
Make_Subprogram_Specification
(Defining_Identifier => Map_Task_Job_Identifier (E),
Parameter_Profile => Param_List,
Return_Type => RE (RE_Error_Kind));
Parameter_Profile => Param_List);
return N;
end Task_Job_Spec;
......@@ -1055,6 +1098,31 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Get_Scheduling_Protocol (Get_Bound_Processor (E));
The_System : constant Node_Id :=
Parent_Component (Parent_Subcomponent (E));
function Package_Spec_Aspect_Definition return Node_Id is
begin
if Add_SPARK2014_Annotations then
return Make_Aspect_Specification
(Make_List_Id
(Make_Aspect (ASN (A_Initializes),
Make_Initialization_Spec
(Make_List_Id
(Make_Defining_Identifier
(PN (P_Elaborated_Variables))))),
Make_Aspect
(ASN (A_Abstract_State),
Make_Abstract_State_List
(Make_List_Id
(Make_State_Name_With_Option
(Make_Defining_Identifier
(PN (P_Elaborated_Variables)),
Synchronous => True,
External => True))))));
else
return No_Node;
end if;
end Package_Spec_Aspect_Definition;
begin
Push_Entity (P);
Push_Entity (U);
......@@ -1090,6 +1158,9 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
-- the scheduler is set to non-preemptive mode.
end if;
ADN.Set_Aspect_Specification (Current_Package,
Package_Spec_Aspect_Definition);
-- Visit all the subcomponents of the process
if not AINU.Is_Empty (Subcomponents (E)) then
......@@ -1587,6 +1658,40 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
-- are appended after all entities generated for threads since
-- they need visibility on these entities.
Package_Body_Refined_States : List_Id := No_List;
function Runtime_Body_Aspect_Definition
(E : Node_Id; RR : Runtime_Routine) return Node_Id;
-- Build aspect definition for runtime services
------------------------------------
-- Runtime_Body_Aspect_Definition --
------------------------------------
function Runtime_Body_Aspect_Definition
(E : Node_Id; RR : Runtime_Routine) return Node_Id is
begin
if Add_SPARK2014_Annotations and then
(RR = RR_Send_Output or else
RR = RR_Get_Value or else
RR = RR_Get_Sender or else
RR = RR_Get_Count or else
RR = Rr_Get_Time_Stamp)
then
return Make_Aspect_Specification
(Make_List_Id
(Make_Aspect
(ASN (A_Refined_Global),
Make_Global_Specification
(Make_List_Id
(Make_Moded_Global_List
(Mode_In,
Map_Refined_Global_Name (E)))))));
else
return No_Node;
end if;
end Runtime_Body_Aspect_Definition;
-------------------
-- Task_Job_Body --
-------------------
......@@ -1714,14 +1819,9 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
-- The condition of validity is that the return value of
-- Get_Count is different from -1.
N :=
Make_Subprogram_Call
(Get_Fully_Qualified_Subprogram (SN (S_Get_Count)),
Make_List_Id (Map_Ada_Defining_Identifier (F)));
Condition :=
Make_Expression
(N,
(Map_Ada_Defining_Identifier (F, "C"),
Op_Not_Equal,
Make_Literal (New_Integer_Value (1, -1, 10)));
......@@ -2032,6 +2132,18 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
(Corresponding_Instance (F)));
Append_Node_To_List (N, Declarations);
N :=
Make_Object_Declaration
(Defining_Identifier =>
Map_Ada_Defining_Identifier (F, "C"),
Constant_Present => True,
Object_Definition => RE (RE_Integer),
Expression =>
Make_Subprogram_Call
(Get_Fully_Qualified_Subprogram (SN (S_Get_Count)),
Make_List_Id (Map_Ada_Defining_Identifier (F))));
Append_Node_To_List (N, Declarations);
-- Assign the port value
N := Make_Get_Valid_Value (F);
......@@ -2562,6 +2674,19 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Map_Ada_Data_Type_Designator
(Corresponding_Instance (F)));
Append_Node_To_List (N, Declarations);
N :=
Make_Object_Declaration
(Defining_Identifier =>
Map_Ada_Defining_Identifier (F, "C"),
Constant_Present => True,
Object_Definition => RE (RE_Integer),
Expression =>
Make_Subprogram_Call
(Get_Fully_Qualified_Subprogram
(SN (S_Get_Count)),
Make_List_Id
(Map_Ada_Defining_Identifier (F))));
Append_Node_To_List (N, Declarations);
-- Assign the port value
......@@ -2665,7 +2790,6 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Append_Node_To_List (N, Declarations);
end if;
end if;
end Make_Ports_Compute_Entrypoint;
--------------------------------------
......@@ -2825,26 +2949,6 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Expression => N);
Append_Node_To_List (N, Statements);
Need_Error_Initialization := False;
declare
Then_Statements : constant List_Id :=
New_List (ADN.K_Statement_List);
begin
N :=
Make_Return_Statement
(Make_Defining_Identifier (VN (V_Error)));
Append_Node_To_List (N, Then_Statements);
N :=
Make_If_Statement
(Condition =>
Make_Expression
(Make_Defining_Identifier (VN (V_Error)),
Op_Not_Equal,
RE (RE_Error_None)),
Then_Statements => Then_Statements);
Append_Node_To_List (N, Statements);
end;
end if;
end;
end if;
......@@ -2956,26 +3060,6 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Expression => N);
Append_Node_To_List (N, Statements);
Need_Error_Initialization := False;
declare
Then_Statements : constant List_Id :=
New_List (ADN.K_Statement_List);
begin
N :=
Make_Return_Statement
(Make_Defining_Identifier (VN (V_Error)));
Append_Node_To_List (N, Then_Statements);
N :=
Make_If_Statement
(Condition =>
Make_Expression
(Make_Defining_Identifier (VN (V_Error)),
Op_Not_Equal,
RE (RE_Error_None)),
Then_Statements => Then_Statements);
Append_Node_To_List (N, Statements);
end;
end if;
F := Next_Node (F);
......@@ -3124,7 +3208,11 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
N := Message_Comment ("Return error code");
Append_Node_To_List (N, Statements);
N := Make_Return_Statement (Make_Defining_Identifier (VN (V_Error)));
N :=
Make_Assignment_Statement
(Variable_Identifier =>
Make_Defining_Identifier (PN (P_Result)),
Expression => Make_Defining_Identifier (VN (V_Error)));
Append_Node_To_List (N, Statements);
N := Make_Subprogram_Implementation (Spec, Declarations, Statements);
......@@ -3992,7 +4080,8 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Make_Subprogram_Implementation
(Spec,
Declarations,
Statements);
Statements,
Runtime_Body_Aspect_Definition (E, RR));
Append_Node_To_List (N, Interrogation_Routine_List);
end Implement_Subprogram;
......@@ -4098,6 +4187,12 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
end Add_Alternative;
begin
-- Add the current interrogator to the package refined state
Append_Node_To_List
(Map_Refined_Global_Name (E),
Package_Body_Refined_States);
-- All the runtime routines below are also generated once
-- per thread component.
......@@ -4323,6 +4418,25 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
N : Node_Id;
The_System : constant Node_Id :=
Parent_Component (Parent_Subcomponent (E));
function Package_Body_Aspect_Definition return Node_Id is
begin
if Add_SPARK2014_Annotations then
return Make_Aspect_Specification
(Make_List_Id
(Make_Aspect
(ASN (A_Refined_State),
Make_Refinement_List
(Make_List_Id
(Make_Refinement_Clause
(Make_Defining_Identifier
(PN (P_Elaborated_Variables)),
Package_Body_Refined_States))))));
else
return No_Node;
end if;
end Package_Body_Aspect_Definition;
begin
Push_Entity (P);
Push_Entity (U);
......@@ -4342,6 +4456,7 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
-- Initialize the runtime routine list
Interrogation_Routine_List := New_List (ADN.K_Statement_List);
Package_Body_Refined_States := New_List (ADN.K_List_Id);
-- Visit all the subcomponents of the process
......@@ -4456,6 +4571,10 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
end loop;
end if;
ADN.Set_Aspect_Specification
(Current_Package,
Package_Body_Aspect_Definition);
-- Unmark all the marked types
Reset_Handlings;
......@@ -4661,9 +4780,12 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
-- Create the body of the parameterless subprogram that
-- executes the thread job.
--
-- Note it is added in the Interrogation_Routine_List to
-- avoid issues with Ada 2012 freezing rules.
N := Task_Job_Body (E);
Append_Node_To_List (N, ADN.Statements (Current_Package));
Append_Node_To_List (N, Interrogation_Routine_List);
end Visit_Thread_Instance;
----------------------------
......
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2017 ESA & ISAE. --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2018 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -1289,6 +1289,20 @@ package body Ocarina.Backends.PO_HI_Ada.Mapping is
"Interrogators");
end Map_Interrogators_Name;
-----------------------------
-- Map_Refined_Global_Name --
-----------------------------
function Map_Refined_Global_Name (E : Node_Id) return Node_Id is
begin
pragma Assert (AAU.Is_Thread (E));
Get_Name_String (Map_Interrogators_Name (E));
Add_Char_To_Name_Buffer ('.');
Get_Name_String_And_Append (PN (P_Elaborated_Variables));
return Make_Defining_Identifier (Name_Find, False);
end Map_Refined_Global_Name;
----------------------
-- Map_Deliver_Name --
----------------------
......
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2015 ESA & ISAE. --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2018 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -57,6 +57,8 @@ package Ocarina.Backends.PO_HI_Ada.Mapping is
function Map_Ada_Priority (P : Unsigned_Long_Long) return Node_Id;
-- Maps the given AADL priority into an Ada priority
function Map_Refined_Global_Name (E : Node_Id) return Node_Id;
function Map_Marshallers_Name (E : Node_Id) return Name_Id;
-- Maps a name for the marshallers package instantiation generated
-- for node E.
......
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2017 ESA & ISAE. --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2018 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -156,12 +156,14 @@ package Ocarina.Backends.PO_HI_Ada.Runtime is
RE_Error, -- Po..HI.Port_Kinds.Error
RE_Stream_Element_Array, -- Po..HI.Streams.Stream_Element_Array
RE_Stream_Element_Offset, -- Po..HI.Stream_Element_Offset
RE_Write, -- Polyorb_HI.Messages.Write
RE_Header_Size, -- Polyorb_HI.Messages.Header_Size
RE_Message_Type, -- Polyorb_HI.Messages.Message_Type
RE_Reallocate, -- Polyorb_HI.Messages.Reallocate