Skip to content

GitLab

O
Ocarina
Commit b69f3152 authored by jhugues's avatar jhugues
Browse files
Options

* REAL: add cos, sin, tan, cosh, sinh, tanh, ln, exp, sqrt 

          functions



git-svn-id: https://tecsw.estec.esa.int/svn/taste/trunk/ocarina@4800 129961e7-ef38-4bb5-a8f7-c9a525a55882
parent 736a099b
Hide whitespace changes
Inline Side-by-side
Showing with 373 additions and 52 deletions
src/backends/ocarina-backends-real.adb
View file @ b69f3152
......@@ -31,6 +31,7 @@
-- --
------------------------------------------------------------------------------
with Ada.Numerics.Generic_Elementary_Functions;
with Namet;
with Output;
with Locations; use Locations;
......@@ -59,6 +60,10 @@ with Unchecked_Deallocation;
package body Ocarina.Backends.REAL is
package Numerics is
new Ada.Numerics.Generic_Elementary_Functions (Long_Long_Float);
use Numerics;
use Ocarina.ME_REAL.REAL_Tree.Nodes;
use Ocarina.ME_REAL.REAL_Tree.Nutils;
use Ocarina.ME_REAL.REAL_Tree.Utils;
......@@ -1159,22 +1164,26 @@ package body Ocarina.Backends.REAL is
Ret := RT_Error;
return;
end if;
V := Get_Value_Type (R1);
V2 := Get_Value_Type (R2);
V := V - V2;
Result := New_Value (V);
case V.T is
when LT_Integer =>
Ret := RT_Integer;
declare
V3 : Value_Type;
begin
V := Get_Value_Type (R1);
V2 := Get_Value_Type (R2);
V3 := V - V2;
Result := New_Value (V3);
case V.T is
when LT_Integer =>
Ret := RT_Integer;
when LT_Real =>
Ret := RT_Float;
when LT_Real =>
Ret := RT_Float;
when others =>
Display_Located_Error
(Loc (E), "expected numeric value",
Fatal => True);
end case;
when others =>
Display_Located_Error
(Loc (E), "expected numeric value",
Fatal => True);
end case;
end;
when OV_Star =>
declare
......@@ -1222,27 +1231,31 @@ package body Ocarina.Backends.REAL is
end if;
when OV_Slash =>
Compute_Check_Expression (Right_Expr (E), T2, R2);
if T2 = RT_Error then
Ret := RT_Error;
return;
end if;
V := Get_Value_Type (R1);
V2 := Get_Value_Type (R2);
V := V / V2;
Result := New_Value (V);
case V.T is
when LT_Integer =>
Ret := RT_Integer;
declare
V3 : Value_Type;
begin
Compute_Check_Expression (Right_Expr (E), T2, R2);
if T2 = RT_Error then
Ret := RT_Error;
return;
end if;
V := Get_Value_Type (R1);
V2 := Get_Value_Type (R2);
V3 := V / V2;
Result := New_Value (V3);
case V.T is
when LT_Integer =>
Ret := RT_Integer;
when LT_Real =>
Ret := RT_Float;
when LT_Real =>
Ret := RT_Float;
when others =>
Display_Located_Error
(Loc (E), "expected numeric value",
Fatal => True);
end case;
when others =>
Display_Located_Error
(Loc (E), "expected numeric value",
Fatal => True);
end case;
end;
when OV_Power =>
Compute_Check_Expression (Right_Expr (E), T2, R2);
......@@ -2883,6 +2896,46 @@ package body Ocarina.Backends.REAL is
Result := New_Boolean_Value (Local_Is_In);
end;
when FC_Cos | FC_Sin | FC_Tan | FC_Cosh | FC_Sinh | FC_Tanh
| FC_Ln | FC_Exp | FC_Sqrt =>
declare
VT : Value_Type;
R : Value_Id;
T2 : Return_Type;
begin
Compute_Check_Expression
(First_Node (Parameters (E)), T2, R);
if T2 = RT_Error then
T := RT_Error;
return;
end if;
VT := Get_Value_Type (R);
case Code (E) is
when FC_Cos =>
Result := New_Real_Value (Cos (VT.RVal));
when FC_Sin =>
Result := New_Real_Value (Sin (VT.RVal));
when FC_Tan =>
Result := New_Real_Value (Tan (VT.RVal));
when FC_Cosh =>
Result := New_Real_Value (Cosh (VT.RVal));
when FC_Sinh =>
Result := New_Real_Value (Sinh (VT.RVal));
when FC_Tanh =>
Result := New_Real_Value (Tanh (VT.RVal));
when FC_Ln =>
Result := New_Real_Value (Log (VT.RVal));
when FC_Exp =>
Result := New_Real_Value (Exp (VT.RVal));
when FC_Sqrt =>
Result := New_Real_Value (Sqrt (VT.RVal));
when others =>
raise Program_Error;
end case;
T := RT_Float;
end;
when others =>
Display_Located_Error
(Loc (E), "Unknown or not implemented verification function",
......
src/core/model/ocarina-analyzer-real.adb
View file @ b69f3152
......@@ -2099,9 +2099,7 @@ package body Ocarina.Analyzer.REAL is
begin
Success := True;
while Present (N) and then Success loop
case Kind (N) is
when K_Check_Subprogram_Call
| K_Check_Expression
| K_Ternary_Expression
......@@ -2498,6 +2496,94 @@ package body Ocarina.Analyzer.REAL is
return;
end if;
when FC_Cos | FC_Sin | FC_Tan | FC_Cosh | FC_Sinh | FC_Tanh
| FC_Ln | FC_Exp | FC_Sqrt =>
Set_Returned_Type (S, RT_Float);
declare
Is_List : Boolean := False;
Iter : Int := 0;
P, Var : Node_Id;
begin
while Present (N) and then Success loop
case Kind (N) is
when K_Check_Subprogram_Call
| K_Check_Expression
| K_Ternary_Expression
| K_Var_Reference =>
Analyze_Verification_Expression (N, Success);
if not Success then
return;
end if;
if Returned_Type (N) = RT_Integer then
null;
elsif Returned_Type (N) = RT_Int_List then
if Iter = 0 then
Is_List := True;
else
Success := False;
end if;
else
Success := False;
return;
end if;
when K_Literal =>
declare
use Ocarina.REAL_Values;
V : constant Value_Type
:= Get_Value_Type (Value (N));
begin
Success := (V.T = LT_Real);
end;
when K_Identifier =>
Var := Find_Variable (Name (N));
if No (Var) then
Display_Analyzer_Error
(No_Node,
"Could not find variable " &
Get_Name_String (Name (Identifier (N))),
Loc => Loc (N));
Success := False;
exit;
end if;
P := Make_Var_Reference (Name (N));
Set_Referenced_Var (P, Var);
Replace_Node_To_List (Parameters (S), N, P);
Analyze_Verification_Expression (P, Success);
if Success then
if Returned_Type (P) = RT_Integer then
Success := not Is_List;
elsif Returned_Type (P) = RT_Int_List then
Is_List := True;
else
Success := False;
end if;
else
return;
end if;
when others =>
Success := False;
end case;
Iter := Iter + 1;
N := Next_Node (N);
end loop;
if not Success
or else (Iter >= 1 and then Is_List) then
Display_Analyzer_Error
(No_Node,
"expected a float as parameter",
Loc => Loc (S));
return;
end if;
end;
when others =>
Set_Returned_Type (S, Get_Returned_Type (Code (S)));
......
src/core/tree/ocarina-me_real-real_tree-utils.adb
View file @ b69f3152
......@@ -119,7 +119,6 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is
P : Boolean := False;
L : Natural := 0;
begin
-- Search the last occurence of "::"
for I in 1 .. M loop
......@@ -144,8 +143,7 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is
-- Translate_Predefined_Sets --
-------------------------------
function Translate_Predefined_Sets (T : Token_Type) return Value_Id
is
function Translate_Predefined_Sets (T : Token_Type) return Value_Id is
begin
case T is
when T_Processor_Set =>
......@@ -198,8 +196,7 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is
-- Translate_Predefined_Sets --
-------------------------------
function Translate_Predefined_Sets (T : Value_Id) return Token_Type
is
function Translate_Predefined_Sets (T : Value_Id) return Token_Type is
begin
case T is
when SV_Processor_Set =>
......@@ -252,8 +249,7 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is
-- Translate_Function_Code --
-----------------------------
function Translate_Function_Code (T : Token_Type) return Value_Id
is
function Translate_Function_Code (T : Token_Type) return Value_Id is
begin
case T is
when T_Is_Subcomponent_Of =>
......@@ -332,6 +328,24 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is
return FC_Head;
when T_Queue =>
return FC_Queue;
when T_Cos =>
return FC_Cos;
when T_Sin =>
return FC_Sin;
when T_Tan =>
return FC_Tan;
when T_Cosh =>
return FC_Cosh;
when T_Sinh =>
return FC_Sinh;
when T_Tanh =>
return FC_Tanh;
when T_Ln =>
return FC_Ln;
when T_Exp =>
return FC_Exp;
when T_Sqrt =>
return FC_Sqrt;
when others =>
DE ("Unknown REAL function");
return FC_Unknown;
......@@ -343,8 +357,7 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is
-- Get_Returned_Type --
-----------------------
function Get_Returned_Type (T : Value_Id) return Return_Type
is
function Get_Returned_Type (T : Value_Id) return Return_Type is
begin
case T is
when FC_Is_Subcomponent_Of =>
......@@ -407,6 +420,8 @@ package body Ocarina.ME_REAL.REAL_Tree.Utils is
return RT_Unknown;
when FC_Queue =>
return RT_Unknown;
when FC_Cos | FC_Sin | FC_Tan =>
return RT_Float;
when others =>
DE ("Unable to determine REAL function returning type");
return RT_Error;
......
src/core/tree/ocarina-me_real-real_tree-utils.ads
View file @ b69f3152
......@@ -123,14 +123,23 @@ package Ocarina.ME_REAL.REAL_Tree.Utils is
FC_All_Equals : constant := 39;
FC_Product : constant := 40;
FC_Sum : constant := 41;
FC_MMax : constant := 50;
FC_MMin : constant := 51;
FC_MAll_Equals : constant := 52;
FC_MProduct : constant := 53;
FC_MSum : constant := 54;
FC_Unknown : constant := 55;
FC_Cos : constant := 42;
FC_Sin : constant := 43;
FC_Tan : constant := 44;
FC_Cosh : constant := 45;
FC_Sinh : constant := 46;
FC_Tanh : constant := 47;
FC_Ln : constant := 48;
FC_Exp : constant := 49;
FC_Sqrt : constant := 50;
FC_MMax : constant := 60;
FC_MMin : constant := 61;
FC_MAll_Equals : constant := 62;
FC_MProduct : constant := 63;
FC_MSum : constant := 64;
FC_Unknown : constant := 65;
-- return types
......
src/core/tree/ocarina-me_real-tokens.adb
View file @ b69f3152
......@@ -165,6 +165,16 @@ package body Ocarina.ME_REAL.Tokens is
New_Token (T_List, "List");
New_Token (T_Float, "Float");
New_Token (T_Max, "Max");
New_Token (T_Cos, "cos");
New_Token (T_Sin, "sin");
New_Token (T_Tan, "tan");
New_Token (T_Cosh, "cosh");
New_Token (T_Sinh, "sinh");
New_Token (T_Tanh, "tanh");
New_Token (T_Ln, "ln");
New_Token (T_Exp, "exp");
New_Token (T_Sqrt, "sqrt");
New_Token (T_LCM, "LCM");
New_Token (T_GCD, "GCD");
New_Token (T_Non_Null, "Non_Null");
......
src/core/tree/ocarina-me_real-tokens.ads
View file @ b69f3152
......@@ -138,6 +138,16 @@ package Ocarina.ME_REAL.Tokens is
T_Integer,
T_Max,
T_Min,
T_Cos,
T_Sin,
T_Tan,
T_Cosh,
T_Sinh,
T_Tanh,
T_Ln,
T_Exp,
T_Sqrt,
T_Is_In, -- Checks weither list_1 is included into list_2
T_LCM, -- Lowest Common Multiple
T_GCD, -- Greatest Common Divisor
......
tests/MANIFEST
View file @ b69f3152
......@@ -247,6 +247,7 @@ tests/real-annexes-execution/test_real_exec_02.aadl
tests/real-annexes-execution/test_real_exec_03.aadl
tests/real-annexes-execution/test_real_exec_04.aadl
tests/real-annexes-execution/test_real_exec_05.aadl
tests/real-annexes-execution/test_real_exec_06.aadl
tests/real-annexes-execution-environment/test_real_exec_env_01.aadl
tests/real_units/validation.aadl
tests/ticket_46/test.aadl
......
tests/real-annexes-execution/test_real_exec_06.aadl 0 → 100644
View file @ b69f3152
package Test5_REAL
public
-----------------
-- Subprograms --
-----------------
subprogram Hello_Spg_1
properties
source_language => Ada95;
source_name => "Hello.Hello_Spg_1";
end Hello_Spg_1;
subprogram Hello_Spg_2
properties
source_language => Ada95;
source_name => "Hello.Hello_Spg_2";
end Hello_Spg_2;
-------------
-- Threads --
-------------
thread Task
end Task;
thread implementation Task.impl_1
calls
MyCalls : {
P_Spg : subprogram Hello_Spg_1;
};
properties
Dispatch_Protocol => periodic;
Period => 1000ms;
Compute_Execution_time => 0 ms .. 3 ms;
Deadline => 1000 ms;
Source_Stack_Size => 13952 Bytes;
end Task.impl_1;
thread implementation Task.impl_2
calls
MyCall : {
P_Spg : subprogram Hello_Spg_2;
};
properties
Dispatch_Protocol => periodic;
Period => 500ms;
Compute_Execution_time => 0 ms .. 3 ms;
Deadline => 500 ms;
Source_Stack_Size => 13952 Bytes;
end Task.impl_2;
---------------
-- Processor --
---------------
processor cpurm
end cpurm;
processor implementation cpurm.impl
properties
Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol);
end cpurm.impl;
---------------
-- Processes --
---------------
process node_a
end node_a;
process implementation node_a.impl
subcomponents
Task1 : thread Task.impl_1;
Task2 : thread Task.impl_2;
annex real_specification {**
-- Tests references properties extraction
theorem test_reference_property
foreach cpu in processor_set do
var cos_x := cos (1.0);
var sin_x := sin (1.0);
var tan_x := tan (1.0);
var cosh_x := cosh (1.0);
var sinh_x := sinh (1.0);
var tanh_x := tanh (1.0);
var ln_x := ln (2.0);
var exp_x := exp (1.0);
var sqrt_x := sqrt (2.0);
check (1 = 1);
end test_reference_property;
**};
end node_a.impl;
------------
-- System --
------------
system rma
end rma;
system implementation rma.ERC32
subcomponents
node_a : process node_a.impl;
cpu_rm : processor cpurm.impl;
properties
Actual_Processor_Binding => (reference (cpu_rm)) applies to node_a;
end rma.ERC32;
end Test5_REAL;
tests/real-annexes-execution/test_real_exec_06.aadl.out 0 → 100644
View file @ b69f3152
test_reference_property execution
-------------------------------------
Evaluating theorem test_reference_property
* Iterate for variable: rma.erc32_cpu_rm
-> value for cos_x is 0.540302305868139717
-> value for sin_x is 0.841470984807896507
-> value for tan_x is 1.55740772465490223
-> value for cosh_x is 1.54308063481524378
-> value for sinh_x is 1.17520119364380146
-> value for tanh_x is 0.761594155955764888
-> value for ln_x is 0.693147180559945309
-> value for exp_x is 2.71828182845904524
-> value for sqrt_x is 1.41421356237309505
=> Result: TRUE
theorem test_reference_property is: TRUE
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment