ehmry/genode
ehmry
/
genode
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

ada: replace local runtime implementation with port 

Fixes #3044
This commit is contained in:
Johannes Kliemann 2018-11-15 17:46:33 +01:00 committed by Christian Helmuth
parent dee4d43eb9
commit eb7c367e25
23 changed files with 142 additions and 1424 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
repos/libports/include/ada/exception.h
View File

@ -16,16 +16,47 @@
namespace Ada {
namespace Exception {
class Program_Error : Genode::Exception {};
class Constraint_Error : Genode::Exception {};
class Storage_Error : Genode::Exception {};
class Undefined_Error : Genode::Exception {};
class Length_Check : Constraint_Error {};
class Overflow_Check : Constraint_Error {};
class Invalid_Data : Constraint_Error {};
class Range_Check : Constraint_Error {};
class Index_Check : Constraint_Error {};
class Discriminant_Check : Constraint_Error {};
class Divide_By_Zero : Constraint_Error {};
class Program_Error : Genode::Exception {};
class Constraint_Error : Genode::Exception {};
class Storage_Error : Genode::Exception {};
class Access_Check : Constraint_Error {};
class Null_Access_Parameter : Constraint_Error {};
class Discriminant_Check : Constraint_Error {};
class Divide_By_Zero : Constraint_Error {};
class Index_Check : Constraint_Error {};
class Invalid_Data : Constraint_Error {};
class Length_Check : Constraint_Error {};
class Null_Exception_Id : Constraint_Error {};
class Null_Not_Allowed : Constraint_Error {};
class Overflow_Check : Constraint_Error {};
class Partition_Check : Constraint_Error {};
class Range_Check : Constraint_Error {};
class Tag_Check : Constraint_Error {};
class Access_Before_Elaboration : Program_Error {};
class Accessibility_Check : Program_Error {};
class Address_Of_Intrinsic : Program_Error {};
class Aliased_Parameters : Program_Error {};
class All_Guards_Closed : Program_Error {};
class Bad_Predicated_Generic_Type : Program_Error {};
class Current_Task_In_Entry_Body : Program_Error {};
class Duplicated_Entry_Address : Program_Error {};
class Implicit_Return : Program_Error {};
class Misaligned_Address_Value : Program_Error {};
class Missing_Return : Program_Error {};
class Overlaid_Controlled_Object : Program_Error {};
class Non_Transportable_Actual : Program_Error {};
class Potentially_Blocking_Operation : Program_Error {};
class Stream_Operation_Not_Allowed : Program_Error {};
class Stubbed_Subprogram_Called : Program_Error {};
class Unchecked_Union_Restriction : Program_Error {};
class Finalize_Raised_Exception : Program_Error {};
class Empty_Storage_Pool : Storage_Error {};
class Infinite_Recursion : Storage_Error {};
class Object_Too_Large : Storage_Error {};
}
}

48
repos/libports/lib/mk/ada.mk
View File

@ -4,30 +4,50 @@ include $(REP_DIR)/lib/mk/ada.inc
ADALIB = $(ADA_RTS)/adalib
ADAINCLUDE = $(ADA_RTS)/adainclude
PACKAGES = system s-stoele s-secsta a-except s-conca2 s-arit64
ADA_RTS_SOURCE = $(call select_from_ports,ada-runtime)/ada-runtime/contrib/gcc-6.3.0
ADA_RUNTIME_DIR = $(call select_from_ports,ada-runtime)/ada-runtime/src
ADA_RUNTIME_LIB_DIR = $(call select_from_ports,ada-runtime)/ada-runtime/src/lib
ADA_RUNTIME_PLATFORM_DIR = $(call select_from_ports,ada-runtime)/ada-runtime/platform
body_exists := $(filter $1.adb,$(shell if [ -e $2/$1.adb ]; then echo $1.adb; fi))
SRC_ADS += $(foreach package, $(PACKAGES), $(package).ads)
SRC_ADB += $(foreach package, $(PACKAGES), $(body_exists, $(package), $(ADA_RTS_SOURCE)))
SRC_ADB += $(foreach package, $(PACKAGES), $(body_exists, $(package), $(REP_DIR)/src/lib/ada/runtime))
SRC_ADS += system.ads \
s-soflin.ads \
s-imgint.ads \
s-stoele.ads \
s-secsta.ads \
interfac.ads \
a-except.ads
CUSTOM_ADA_MAKE = $(CC)
CUSTOM_ADA_FLAGS = -c -gnatg -gnatp -gnatpg -gnatn2
CUSTOM_ADA_OPT = $(CC_ADA_OPT)
CUSTOM_ADA_INCLUDE = -I- -I$(REP_DIR)/src/lib/ada/runtime -I$(ADA_RTS_SOURCE) -I$(REP_DIR)/src/lib/ada/runtimelib
CUSTOM_ADA_INCLUDE = -I- -I$(ADA_RUNTIME_DIR) -I$(ADA_RTS_SOURCE) -I$(ADA_RUNTIME_LIB_DIR)
# pure C runtime implementations
SRC_CC += a-except_c.cc s-soflin_c.cc a-exctab_c.cc
INC_DIR += $(ADA_RUNTIME_LIB_DIR)
# C runtime glue code
SRC_CC += s-secsta_c.cc libc.cc
SRC_CC += genode.cc
# Ada packages that implement runtime functionality
SRC_ADB += ss_utils.adb
SRC_ADB += ss_utils.adb string_utils.adb platform.adb
vpath %.cc $(REP_DIR)/src/lib/ada/runtimelib
vpath %.adb $(REP_DIR)/src/lib/ada/runtime $(ADA_RTS_SOURCE) $(REP_DIR)/src/lib/ada/runtimelib
vpath %.ads $(REP_DIR)/src/lib/ada/runtime $(ADA_RTS_SOURCE)
vpath %.cc $(ADA_RUNTIME_PLATFORM_DIR)
vpath system.ads $(ADA_RTS_SOURCE)
vpath s-soflin.ads $(ADA_RUNTIME_DIR)
vpath s-stoele.ads $(ADA_RTS_SOURCE)
vpath s-secsta.ads $(ADA_RUNTIME_DIR)
vpath s-imgint.ads $(ADA_RTS_SOURCE)
vpath a-except.ads $(ADA_RUNTIME_DIR)
vpath interfac.ads $(ADA_RTS_SOURCE)
vpath s-stoele.adb $(ADA_RTS_SOURCE)
vpath s-secsta.adb $(ADA_RUNTIME_DIR)
vpath s-soflin.adb $(ADA_RUNTIME_DIR)
vpath s-imgint.adb $(ADA_RTS_SOURCE)
vpath a-except.adb $(ADA_RUNTIME_DIR)
vpath platform.% $(ADA_RUNTIME_LIB_DIR)
vpath string_utils.% $(ADA_RUNTIME_LIB_DIR)
vpath ss_utils.% $(ADA_RUNTIME_LIB_DIR)
SHARED_LIB = yes

1
repos/libports/ports/ada-runtime.hash Normal file
View File

@ -0,0 +1 @@
1898150e6e4544954634733a2384674b0193d4fd

7
repos/libports/ports/ada-runtime.port Normal file
View File

@ -0,0 +1,7 @@
LICENSE := AGPLv3
VERSION := 0
DOWNLOADS := ada-runtime.git
URL(ada-runtime) := https://github.com/Componolit/ada-runtime.git
REV(ada-runtime) := 82e4df4ed4ae73b9e391dc250d25a524d69a7598
DIR(ada-runtime) := ada-runtime

65
repos/libports/recipes/api/ada/content.mk
View File

@ -1,4 +1,38 @@
PORT_DIR := $(call port_dir,$(GENODE_DIR)/repos/ports/ports/gcc)
ADA_RT_DIR := $(call port_dir,$(GENODE_DIR)/repos/libports/ports/ada-runtime)
MIRROR_FROM_ADA_RT_DIR := \
$(addprefix ada-runtime/contrib/gcc-6.3.0/,\
ada.ads \
system.ads \
s-stoele.ads \
a-unccon.ads \
)\
$(addprefix ada-runtime/src/,\
s-stalib.ads \
a-except.ads \
s-secsta.ads \
s-parame.ads \
s-soflin.ads \
)\
$(addprefix ada-runtime/src/lib/,\
ss_utils.ads \
)
# $(addprefix ada-runtime/src/,\
s-stache.ads \
s-conca2.ads \
s-arit64.ads \
)\
$(addprefix ada-runtime/contrib/gcc-6.3.0/,\
interfac.ads \
system.ads \
)
content: $(MIRROR_FROM_ADA_RT_DIR)
$(MIRROR_FROM_ADA_RT_DIR):
mkdir -p src/noux-pkg/gcc/gcc/ada/
cp -r $(ADA_RT_DIR)/$@ src/noux-pkg/gcc/gcc/ada/
MIRROR_FROM_REP_DIR := \
lib/import/import-ada.mk \
@ -10,35 +44,8 @@ content: $(MIRROR_FROM_REP_DIR)
$(MIRROR_FROM_REP_DIR):
$(mirror_from_rep_dir)
content: LICENSE
LICENSE:
cp $(PORT_DIR)/src/noux-pkg/gcc/gcc/COPYING $@
MIRROR_FROM_PORT_DIR := $(addprefix src/noux-pkg/gcc/gcc/ada/,\
a-except.ads \
s-parame.ads \
s-stalib.ads \
s-traent.ads \
s-soflin.ads \
s-stache.ads \
s-stoele.ads \
s-secsta.ads \
s-conca2.ads \
s-arit64.ads \
ada.ads \
interfac.ads \
a-unccon.ads \
system.ads )
content: $(MIRROR_FROM_PORT_DIR)
$(MIRROR_FROM_PORT_DIR):
mkdir -p $(dir $@)
cp -r $(PORT_DIR)/$@ $@
content: lib/mk/ada.mk
lib/mk/ada.mk:
mkdir -p $(dir $@)
cp -r $(REP_DIR)/lib/mk/ada.inc $@
cp -r $(REP_DIR)/lib/mk/ada.inc $@

2
repos/libports/recipes/pkg/test-ada_exception/runtime
View File

@ -4,7 +4,7 @@
<timeout meaning="failed" sec="20" />
<log meaning="succeeded">
[init -> test-ada_exception] Ada exception test*
[init -> test-ada_exception] Error: Program Error in except.adb at line 6*
[init -> test-ada_exception] Error: Exception raised: explicit raise in except.adb: 6
[init -> test-ada_exception] Caught Ada::Exception::Program_Error*
[init] child "test-ada_exception" exited with exit value 0
</log>

60
repos/libports/recipes/src/ada/content.mk
View File

@ -1,35 +1,25 @@
PORT_DIR := $(call port_dir,$(GENODE_DIR)/repos/ports/ports/gcc)
ADA_RT_DIR := $(call port_dir,$(GENODE_DIR)/repos/libports/ports/ada-runtime)
MIRROR_FROM_PORT_DIR := $(addprefix src/noux-pkg/gcc/gcc/ada/,\
a-except.ads \
a-except.adb \
s-parame.ads \
s-parame.adb \
s-stalib.ads \
s-stalib.adb \
s-traent.ads \
s-traent.adb \
s-soflin.ads \
s-stache.ads \
s-stache.adb \
s-stoele.ads \
s-stoele.adb \
s-secsta.ads \
s-secsta.adb \
s-conca2.ads \
s-conca2.adb \
s-arit64.ads \
s-arit64.adb \
ada.ads \
interfac.ads \
a-unccon.ads \
system.ads )
MIRROR_FROM_ADA_RT_DIR := \
$(addprefix ada-runtime/contrib/gcc-6.3.0/,\
ada.ads \
system.ads \
interfac.ads \
s-unstyp.ads \
s-stoele.ads \
s-stoele.adb \
s-imgint.ads \
s-imgint.adb \
a-unccon.ads \
) \
ada-runtime/src \
ada-runtime/platform/genode.cc
content: $(MIRROR_FROM_PORT_DIR)
content: $(MIRROR_FROM_ADA_RT_DIR)
$(MIRROR_FROM_PORT_DIR):
$(MIRROR_FROM_ADA_RT_DIR):
mkdir -p $(dir $@)
cp -r $(PORT_DIR)/$@ $@
cp -r $(ADA_RT_DIR)/$@ $@
MIRROR_FROM_REP_DIR := \
lib/mk/ada.mk \
@ -42,14 +32,8 @@ content: $(MIRROR_FROM_REP_DIR)
$(MIRROR_FROM_REP_DIR):
$(mirror_from_rep_dir)
content: src/lib/ada
content: src/lib/ada/target.mk
src/lib/ada:
mkdir -p $@
cp -r $(REP_DIR)/$@/* $@/
echo "LIBS = ada" > $@/target.mk
content: LICENSE
LICENSE:
cp $(PORT_DIR)/src/noux-pkg/gcc/gcc/COPYING $@
src/lib/ada/target.mk:
mkdir -p $(dir $@)
echo "LIBS = ada" > $@

82
repos/libports/src/lib/ada/runtime/a-except.adb
View File

@ -1,82 +0,0 @@
--
-- \brief Ada exceptions
-- \author Johannes Kliemann
-- \date 2018-06-25
--
-- Copyright (C) 2018 Genode Labs GmbH
-- Copyright (C) 2018 Componolit GmbH
--
-- This file is part of the Genode OS framework, which is distributed
-- under the terms of the GNU Affero General Public License version 3.
--
package body Ada.Exceptions is
----------------------------
-- Raise_Exception_Always --
----------------------------
procedure Raise_Exception_Always (
E : Exception_Id;
Message : String := ""
)
is
procedure Raise_Ada_Exception (
Name : System.Address;
Msg : System.Address
)
with
Import,
Convention => C,
External_Name => "raise_ada_exception";
C_Msg : String := Message & Character'Val (0);
begin
Warn_Not_Implemented ("Raise_Exception_Always");
Raise_Ada_Exception (E.Full_Name, C_Msg'Address);
end Raise_Exception_Always;
procedure Raise_Exception (
E : Exception_Id;
Message : String := ""
)
is
begin
Raise_Exception_Always (E, Message);
end Raise_Exception;
procedure Reraise_Occurrence_No_Defer (
X : Exception_Occurrence
)
is
pragma Unreferenced (X);
begin
Warn_Not_Implemented ("Reraise_Occurrence_No_Defer");
end Reraise_Occurrence_No_Defer;
procedure Save_Occurrence (
Target : out Exception_Occurrence;
Source : Exception_Occurrence
)
is
begin
Warn_Not_Implemented ("Save_Occurrence");
Target := Source;
end Save_Occurrence;
procedure Warn_Not_Implemented (
Name : String
)
is
procedure C_Warn_Unimplemented_Function (
Func : System.Address
)
with
Import,
Convention => C,
External_Name => "warn_unimplemented_function";
C_Name : String := Name & Character'Val (0);
begin
C_Warn_Unimplemented_Function (C_Name'Address);
end Warn_Not_Implemented;
end Ada.Exceptions;

72
repos/libports/src/lib/ada/runtime/a-except.ads
View File

@ -1,72 +0,0 @@
--
-- \brief Ada exceptions
-- \author Johannes Kliemann
-- \date 2018-06-25
--
-- Copyright (C) 2018 Genode Labs GmbH
-- Copyright (C) 2018 Componolit GmbH
--
-- This file is part of the Genode OS framework, which is distributed
-- under the terms of the GNU Affero General Public License version 3.
--
with System;
package Ada.Exceptions is
type Exception_Id is private;
type Exception_Occurrence is limited private;
type Exception_Occurrence_Access is access all Exception_Occurrence;
procedure Raise_Exception_Always (
E : Exception_Id;
Message : String := ""
)
with
Export,
Convention => Ada,
External_Name => "__gnat_raise_exception";
procedure Raise_Exception (
E : Exception_Id;
Message : String := ""
);
procedure Reraise_Occurrence_No_Defer (
X : Exception_Occurrence
);
procedure Save_Occurrence (
Target : out Exception_Occurrence;
Source : Exception_Occurrence
);
private
-- the following declarations belong to s-stalib.ads
-- begin s-stalib.ads
type Exception_Data;
type Exception_Data_Ptr is access all Exception_Data;
type Raise_Action is access procedure;
type Exception_Data is record
Not_Handled_By_Others : Boolean;
Lang : Character;
Name_Length : Natural;
Full_Name : System.Address;
HTable_Ptr : Exception_Data_Ptr;
Foreign_Data : System.Address;
Raise_Hook : Raise_Action;
end record;
-- end s-stalib.ads
type Exception_Id is new Exception_Data_Ptr;
type Exception_Occurrence is record
null;
end record;
procedure Warn_Not_Implemented (
Name : String
);
end Ada.Exceptions;

64
repos/libports/src/lib/ada/runtime/s-secsta.adb
View File

@ -1,64 +0,0 @@
--
-- \brief Ada secondary stack
-- \author Johannes Kliemann
-- \date 2018-04-16
--
-- Copyright (C) 2018 Genode Labs GmbH
-- Copyright (C) 2018 Componolit GmbH
--
-- This file is part of the Genode OS framework, which is distributed
-- under the terms of the GNU Affero General Public License version 3.
--
package body System.Secondary_Stack is
procedure SS_Allocate (
Address : out System.Address;
Storage_Size : SSE.Storage_Count
)
is
T : constant Ss_Utils.Thread := Ss_Utils.C_Get_Thread;
begin
if T /= Ss_Utils.Invalid_Thread then
Ss_Utils.S_Allocate (Address,
Storage_Size,
Thread_Registry,
T);
else
raise Program_Error;
end if;
end SS_Allocate;
function SS_Mark return Mark_Id
is
M : Mark_Id;
T : constant Ss_Utils.Thread := Ss_Utils.C_Get_Thread;
begin
if T /= Ss_Utils.Invalid_Thread then
Ss_Utils.S_Mark (M.Sstk,
SSE.Storage_Count (M.Sptr),
Thread_Registry,
T);
else
raise Program_Error;
end if;
return M;
end SS_Mark;
procedure SS_Release (
M : Mark_Id
)
is
T : constant Ss_Utils.Thread := Ss_Utils.C_Get_Thread;
begin
if T /= Ss_Utils.Invalid_Thread then
Ss_Utils.S_Release (M.Sstk,
SSE.Storage_Count (M.Sptr),
Thread_Registry,
T);
else
raise Program_Error;
end if;
end SS_Release;
end System.Secondary_Stack;

46
repos/libports/src/lib/ada/runtime/s-secsta.ads
View File

@ -1,46 +0,0 @@
--
-- \brief Ada secondary stack
-- \author Johannes Kliemann
-- \date 2018-04-16
--
-- Copyright (C) 2018 Genode Labs GmbH
-- Copyright (C) 2018 Componolit GmbH
--
-- This file is part of the Genode OS framework, which is distributed
-- under the terms of the GNU Affero General Public License version 3.
--
with System.Storage_Elements;
with Ss_Utils;
use all type Ss_Utils.Thread;
package System.Secondary_Stack is
package SSE renames System.Storage_Elements;
type Mark_Id is private;
procedure SS_Allocate (
Address : out System.Address;
Storage_Size : SSE.Storage_Count
);
function SS_Mark return Mark_Id;
procedure SS_Release (
M : Mark_Id
);
private
SS_Pool : Integer;
-- This is not used but needed since the build will fail otherwise
type Mark_Id is record
Sstk : System.Address;
Sptr : SSE.Integer_Address;
end record;
Thread_Registry : Ss_Utils.Registry := Ss_Utils.Null_Registry;
end System.Secondary_Stack;

117
repos/libports/src/lib/ada/runtimelib/a-except_c.cc
View File

@ -1,117 +0,0 @@
/*
* \brief Implementation of Ada exception functions, propagating to C++
* \author Alexander Senier
* \author Johannes Kliemann
* \date 2018-04-16
*
*/
/*
* Copyright (C) 2018 Genode Labs GmbH
* Copyright (C) 2018 Componolit GmbH
*
* This file is part of the Genode OS framework, which is distributed
* under the terms of the GNU Affero General Public License version 3.
*/
#include <base/log.h>
#include <util/string.h>
#include <ada/exception.h>
extern "C" {
/* Program Error */
void __gnat_rcheck_PE_Explicit_Raise(char *file, int line)
{
Genode::error("Program Error in ", Genode::Cstring(file), " at line ", line);
throw Ada::Exception::Program_Error();
}
/* Constraint Error */
void constraint_error(char *file, int line)
{
Genode::error("Constraint Error in ", Genode::Cstring(file), " at line ", line);
throw Ada::Exception::Constraint_Error();
}
void __gnat_rcheck_CE_Explicit_Raise(char *file, int line)
{
constraint_error(file, line);
}
/* Storage Error */
void __gnat_rcheck_SE_Explicit_Raise(char *file, int line)
{
Genode::error("Storage Error in ", Genode::Cstring(file), " at line ", line);
throw Ada::Exception::Storage_Error();
}
/* Constraint Error subtypes */
/* Length check failed */
void __gnat_rcheck_CE_Length_Check(char *file, int line)
{
Genode::error("Constraint Error: Length check failed in ",
Genode::Cstring(file), " at line ", line);
throw Ada::Exception::Length_Check();
}
/* Overflow check failed */
void __gnat_rcheck_CE_Overflow_Check(char *file, int line)
{
Genode::error("Constraint Error: Overflow check failed in ",
Genode::Cstring(file), " at line ", line);
throw Ada::Exception::Overflow_Check();
}
/* Invalid data */
void __gnat_rcheck_CE_Invalid_Data(char *file, int line)
{
Genode::error("Constraint Error: Invalid data in ",
Genode::Cstring(file), " at line ", line);
throw Ada::Exception::Invalid_Data();
}
/* Range check failed */
void __gnat_rcheck_CE_Range_Check(char *file, int line)
{
Genode::error("Constraint Error: Range check failed in ",
Genode::Cstring(file), " at line ", line);
throw Ada::Exception::Range_Check();
}
/* Index check failed */
void __gnat_rcheck_CE_Index_Check(char *file, int line)
{
Genode::error("Constraint Error: Index check failed in ",
Genode::Cstring(file), " at line ", line);
throw Ada::Exception::Index_Check();
}
/* Discriminant check failed */
void __gnat_rcheck_CE_Discriminant_Check(char *file, int line)
{
Genode::error("Constraint Error: Discriminant check failed in ",
Genode::Cstring(file), " at line ", line);
throw Ada::Exception::Discriminant_Check();
}
/* Divide by 0 */
void __gnat_rcheck_CE_Divide_By_Zero(char *file, int line)
{
Genode::error("Constraint Error: Divide by zero in ",
Genode::Cstring(file), " at line ", line);
throw Ada::Exception::Divide_By_Zero();
}
void raise_ada_exception(char *name, char *message)
{
Genode::error(Genode::Cstring(name), " raised: ", Genode::Cstring(message));
}
void warn_unimplemented_function(char *func)
{
Genode::warning(Genode::Cstring(func), " unimplemented");
}
}

25
repos/libports/src/lib/ada/runtimelib/a-exctab_c.cc
View File

@ -1,25 +0,0 @@
/*
* \brief Provide dummy for custom Ada exceptions
* \author Johannes Kliemann
* \date 2018-06-25
*
*/
/*
* Copyright (C) 2018 Genode Labs GmbH
* Copyright (C) 2018 Componolit GmbH
*
* This file is part of the Genode OS framework, which is distributed
* under the terms of the GNU Affero General Public License version 3.
*/
#include <base/log.h>
extern "C" {
void system__exception_table__register()
{
Genode::warning(__func__, " not implemented");
}
}

5
repos/libports/src/lib/ada/runtimelib/genode_rts.gpr
View File

@ -1,5 +0,0 @@
project genode_rts is
for Source_Dirs use (".");
end genode_rts;

490
repos/libports/src/lib/ada/runtimelib/gnattest/tests/ss_utils-test_data-tests.adb
View File

@ -1,490 +0,0 @@
-- This package has been generated automatically by GNATtest.
-- You are allowed to add your code to the bodies of test routines.
-- Such changes will be kept during further regeneration of this file.
-- All code placed outside of test routine bodies will be lost. The
-- code intended to set up and tear down the test environment should be
-- placed into Ss_Utils.Test_Data.
with AUnit.Assertions; use AUnit.Assertions;
with System.Assertions;
-- begin read only
-- id:2.2/00/
--
-- This section can be used to add with clauses if necessary.
--
-- end read only
with System.Memory;
-- begin read only
-- end read only
package body Ss_Utils.Test_Data.Tests is
-- begin read only
-- id:2.2/01/
--
-- This section can be used to add global variables and other elements.
--
-- end read only
package SSE renames System.Storage_Elements;
Alloc_Success : Boolean := False;
Valid_Thread : Thread := Thread (SSE.To_Address (16#1000#));
function C_Alloc (T : Thread; Size : SSE.Storage_Count) return System.Address
with
Export,
Convention => C,
External_Name => "allocate_secondary_stack";
function C_Alloc (T : Thread; Size : SSE.Storage_Count) return System.Address
is
begin
if Alloc_Success then
return System.Memory.Alloc (System.Memory.size_t (Size));
else
return System.Null_Address;
end if;
end C_Alloc;
procedure Get_Mark_Full_Registry
is
E : Mark;
R : Registry := Null_Registry;
T : constant Thread := Thread (System.Storage_Elements.To_Address (42));
begin
for I in R'Range loop
R (I).Id := Valid_Thread;
end loop;
Get_Mark (T, R, E);
end Get_Mark_Full_Registry;
procedure Get_Mark_Invalid_Thread
is
E : Mark;
R : Registry := Null_Registry;
begin
Get_Mark (Invalid_Thread, R, E);
end Get_Mark_Invalid_Thread;
procedure Set_Mark_Unknown_Thread
is
T : Thread := Valid_Thread;
R : Registry := Null_Registry;
M : Mark := (Base => System.Storage_Elements.To_Address (42),
Top => 8);
begin
Set_Mark (T, M, R);
end Set_Mark_Unknown_Thread;
procedure Set_Mark_Invalid_Thread
is
T : Thread := Invalid_Thread;
R : Registry := Null_Registry;
M : Mark := (Base => System.Storage_Elements.To_Address (42),
Top => 8);
begin
Set_Mark (T, M, R);
end Set_Mark_Invalid_Thread;
procedure Set_Mark_Invalid_Stack
is
T : Thread := Valid_Thread;
R : Registry := Null_Registry;
M : Mark := (Base => System.Null_Address,
Top => 0);
begin
R (0).Id := T;
R (0).Data := M;
R (0).Data.Base := System.Storage_Elements.To_Address (42);
Set_Mark (T, M, R);
end Set_Mark_Invalid_Stack;
procedure Alloc_Stack_With_Null_Ptr
is
Ptr : System.Address;
begin
Alloc_Success := False;
Ptr := Allocate_Stack (Valid_Thread, 0);
end Alloc_Stack_With_Null_Ptr;
procedure Alloc_Stack_With_Invalid_Thread
is
Ptr : System.Address;
begin
Alloc_Success := True;
Ptr := Allocate_Stack (Invalid_Thread, 0);
end Alloc_Stack_With_Invalid_Thread;
procedure S_Allocate_Stack_Overflow_1
is
T : Thread := Valid_Thread;
Reg : Registry := Null_Registry;
Stack_Ptr : System.Address;
begin
S_Allocate (Stack_Ptr, Secondary_Stack_Size * 2, Reg, T);
end S_Allocate_Stack_Overflow_1;
procedure S_Allocate_Stack_Overflow_2
is
T : Thread := Valid_Thread;
Reg : Registry := Null_Registry;
Stack_Ptr : System.Address;
begin
for I in 0 .. 1024 loop
S_Allocate (Stack_Ptr, SSE.Storage_Offset (1024), Reg, T);
end loop;
end S_Allocate_Stack_Overflow_2;
procedure S_Release_High_Mark
is
T : Thread := Valid_Thread;
Reg : Registry := Null_Registry;
Mark_Id : SSE.Storage_Count;
Mark_Base : System.Address;
Stack_Ptr : System.Address;
begin
S_Allocate (Stack_Ptr, 8, Reg, T);
S_Mark (Mark_Base, Mark_Id, Reg, T);
S_Release (Mark_Base, Mark_Id + 1, Reg, T);
end S_Release_High_Mark;
-- begin read only
-- end read only
-- begin read only
procedure Test_Get_Mark (Gnattest_T : in out Test);
procedure Test_Get_Mark_205a8b (Gnattest_T : in out Test) renames Test_Get_Mark;
-- id:2.2/205a8b09655a71fc/Get_Mark/1/0/
procedure Test_Get_Mark (Gnattest_T : in out Test) is
-- ss_utils.ads:36:4:Get_Mark
-- end read only
pragma Unreferenced (Gnattest_T);
T1 : Thread := Thread (System.Storage_Elements.To_Address (1));
T2 : Thread := Thread (System.Storage_Elements.To_Address (2));
Reg : Registry := Null_Registry;
Test_Mark : Mark;
T1_Mark : Mark := (Base => System.Null_Address,
Top => 0);
T2_Mark : Mark := (Base => System.Storage_Elements.To_Address (42),
Top => 4);
begin
Alloc_Success := True;
AUnit.Assertions.Assert_Exception (Get_Mark_Invalid_Thread'Access,
"Get mark with invalid thread failed");
AUnit.Assertions.Assert_Exception (Get_Mark_Full_Registry'Access,
"Get mark with full registry failed");
Get_Mark (T1, Reg, Test_Mark);
AUnit.Assertions.Assert (Test_Mark.Base /= System.Null_Address,
"Stack not initialized");
AUnit.Assertions.Assert (Test_Mark.Top = 0,
"Top not null after initialization");
Get_Mark (T1, Reg, T1_Mark);
AUnit.Assertions.Assert (Test_Mark = T1_Mark,
"Failed to get T1 mark");
Reg (2).Id := T2;
Reg (2).Data := T2_Mark;
Get_Mark (T2, Reg, Test_Mark);
AUnit.Assertions.Assert (Test_Mark = T2_Mark,
"Failed to get T2 mark");
-- begin read only
end Test_Get_Mark;
-- end read only
-- begin read only
procedure Test_Set_Mark (Gnattest_T : in out Test);
procedure Test_Set_Mark_75973c (Gnattest_T : in out Test) renames Test_Set_Mark;
-- id:2.2/75973c43cd4409b1/Set_Mark/1/0/
procedure Test_Set_Mark (Gnattest_T : in out Test) is
-- ss_utils.ads:44:4:Set_Mark
-- end read only
pragma Unreferenced (Gnattest_T);
Reg : Registry := Null_Registry;
E1 : Mark;
E2 : Mark;
T : Thread := Valid_Thread;
begin
AUnit.Assertions.Assert_Exception (Set_Mark_Unknown_Thread'Access,
"Set mark on unknown thread failed");
AUnit.Assertions.Assert_Exception (Set_Mark_Invalid_Thread'Access,
"Set mark on invalid thread failed");
AUnit.Assertions.Assert_Exception (Set_Mark_Invalid_Stack'Access,
"Set mark on invalid stack failed");
Get_Mark (T, Reg, E1);
E1.Top := 42;
Set_Mark (T, E1, Reg);
Get_Mark (T, Reg, E2);
AUnit.Assertions.Assert (E1 = E2,
"Storing mark failed");
-- begin read only
end Test_Set_Mark;
-- end read only
-- begin read only
procedure Test_Allocate_Stack (Gnattest_T : in out Test);
procedure Test_Allocate_Stack_247b78 (Gnattest_T : in out Test) renames Test_Allocate_Stack;
-- id:2.2/247b786dfb10deba/Allocate_Stack/1/0/
procedure Test_Allocate_Stack (Gnattest_T : in out Test) is
-- ss_utils.ads:53:4:Allocate_Stack
-- end read only
pragma Unreferenced (Gnattest_T);
begin
Alloc_Success := True;
AUnit.Assertions.Assert (Allocate_Stack (Valid_Thread, 0) /= System.Null_Address,
"Allocate stack failed");
AUnit.Assertions.Assert_Exception (Alloc_Stack_With_Null_Ptr'Access,
"Allocate stack with null failed");
AUnit.Assertions.Assert_Exception (Alloc_Stack_With_Invalid_Thread'Access,
"Allocate stack with invalid thread failed");
-- begin read only
end Test_Allocate_Stack;
-- end read only
-- begin read only
procedure Test_S_Allocate (Gnattest_T : in out Test);
procedure Test_S_Allocate_70b783 (Gnattest_T : in out Test) renames Test_S_Allocate;
-- id:2.2/70b783c9ffa2dd5e/S_Allocate/1/0/
procedure Test_S_Allocate (Gnattest_T : in out Test) is
-- ss_utils.ads:61:4:S_Allocate
-- end read only
pragma Unreferenced (Gnattest_T);
Reg : Registry := Null_Registry;
M : Mark;
T : Thread := Valid_Thread;
Stack_Base : System.Address;
Stack_Ptr : System.Address;
begin
Alloc_Success := True;
Get_Mark (T, Reg, M);
AUnit.Assertions.Assert (M.Base /= System.Null_Address,
"Base allocation failed");
AUnit.Assertions.Assert (M.Top = 0,
"Top not initialized with 0");
Stack_Base := M.Base;
S_Allocate (Stack_Ptr, 8, Reg, T);
AUnit.Assertions.Assert (Stack_Base - 8 = Stack_Ptr,
"Invalid base move");
Get_Mark (T, Reg, M);
AUnit.Assertions.Assert (M.Top = 8,
"Unmodified top");
S_Allocate (Stack_Ptr, 8, Reg, T);
AUnit.Assertions.Assert (Stack_Base - 16 = Stack_Ptr,
"Invalid stack ptr");
Get_Mark (T, Reg, M);
AUnit.Assertions.Assert (M.Top = 16,
"Invalid top");
Reg := Null_Registry;
S_Allocate (Stack_Ptr, 8, Reg, T);
Get_Mark (T, Reg, M);
AUnit.Assertions.Assert (Stack_Ptr /= System.Null_Address,
"Initial Base allocation failed");
AUnit.Assertions.Assert (M.Base - 8 = Stack_Ptr,
"Invalid Stack initialization");
AUnit.Assertions.Assert (M.Top = 8,
"Top not set correctly");
AUnit.Assertions.Assert_Exception (S_Allocate_Stack_Overflow_1'Access,
"Failed to detect stack overflow 1");
AUnit.Assertions.Assert_Exception (S_Allocate_Stack_Overflow_2'Access,
"Failed to detect stack overflow 2");
-- begin read only
end Test_S_Allocate;
-- end read only
-- begin read only
procedure Test_S_Mark (Gnattest_T : in out Test);
procedure Test_S_Mark_a8299f (Gnattest_T : in out Test) renames Test_S_Mark;
-- id:2.2/a8299fa36da74b68/S_Mark/1/0/
procedure Test_S_Mark (Gnattest_T : in out Test) is
-- ss_utils.ads:68:4:S_Mark
-- end read only
pragma Unreferenced (Gnattest_T);
Reg : Registry := Null_Registry;
M : Mark;
S_Addr : System.Address;
S_Pos : SSE.Storage_Count;
T : Thread := Valid_Thread;
Stack_Ptr : System.Address;
begin
S_Allocate (Stack_Ptr, 8, Reg, T);
S_Mark (S_Addr, S_Pos, Reg, T);
Get_Mark (T, Reg, M);
AUnit.Assertions.Assert (S_Pos = M.Top and S_Pos = 8 and S_Addr = M.Base,
"Invalid mark location");
Reg := Null_Registry;
S_Mark (S_Addr, S_Pos, Reg, T);
Get_Mark (T, Reg, M);
AUnit.Assertions.Assert (S_Addr = M.Base,
"Mark did not initialize stack");
AUnit.Assertions.Assert (M.Top = 0 and S_Pos = 0,
"Mark did not initialize top");
-- begin read only
end Test_S_Mark;
-- end read only
-- begin read only
procedure Test_S_Release (Gnattest_T : in out Test);
procedure Test_S_Release_666a46 (Gnattest_T : in out Test) renames Test_S_Release;
-- id:2.2/666a463f3bb6be9f/S_Release/1/0/
procedure Test_S_Release (Gnattest_T : in out Test) is
-- ss_utils.ads:74:4:S_Release
-- end read only
pragma Unreferenced (Gnattest_T);
Reg : Registry := Null_Registry;
M : Mark;
Stack_Ptr : System.Address;
Mark_Id : System.Address;
Mark_Pos : SSE.Storage_Count;
T : Thread := Valid_Thread;
begin
AUnit.Assertions.Assert_Exception (S_Release_High_Mark'Access,
"Invalid stack release");
S_Allocate (Stack_Ptr, 8, Reg, T);
S_Mark (Mark_Id, Mark_Pos, Reg, T);
S_Allocate (Stack_Ptr, 4, Reg, T);
S_Allocate (Stack_Ptr, 4, Reg, T);
Get_Mark (T, Reg, M);
AUnit.Assertions.Assert (M.Top = 16,
"Top not initialized correctly");
AUnit.Assertions.Assert (Stack_Ptr /= Mark_Id - Mark_Pos,
"Mark not set correctly");
S_Release (Mark_Id, Mark_Pos, Reg, T);
Get_Mark (T, Reg, M);
AUnit.Assertions.Assert (M.Top = 8,
"Top not reset correctly");
AUnit.Assertions.Assert (M.Top = Mark_Pos,
"Invalid mark id");
S_Allocate (Stack_Ptr, 8, Reg, T);
AUnit.Assertions.Assert (Mark_Id - Mark_Pos = Stack_Ptr + 8,
"Invalid stack ptr location");
-- begin read only
end Test_S_Release;
-- end read only
-- begin read only
procedure Test_C_Alloc (Gnattest_T : in out Test);
procedure Test_C_Alloc_08db82 (Gnattest_T : in out Test) renames Test_C_Alloc;
-- id:2.2/08db82b0ee8ae041/C_Alloc/1/0/
procedure Test_C_Alloc (Gnattest_T : in out Test) is
-- ss_utils.ads:80:4:C_Alloc
-- end read only
pragma Unreferenced (Gnattest_T);
begin
Alloc_Success := True;
AUnit.Assertions.Assert (C_Alloc (Invalid_Thread, 0) /= System.Null_Address,
"Alloc test failed");
Alloc_Success := False;
AUnit.Assertions.Assert (C_Alloc (Invalid_Thread, 0) = System.Null_Address,
"Null Address test failed");
-- begin read only
end Test_C_Alloc;
-- end read only
-- begin read only
procedure Test_C_Free (Gnattest_T : in out Test);
procedure Test_C_Free_6747d0 (Gnattest_T : in out Test) renames Test_C_Free;
-- id:2.2/6747d08d1141dd9a/C_Free/1/0/
procedure Test_C_Free (Gnattest_T : in out Test) is
-- ss_utils.ads:88:4:C_Free
-- end read only
pragma Unreferenced (Gnattest_T);
begin
AUnit.Assertions.Assert (True, "C_Free");
-- begin read only
end Test_C_Free;
-- end read only
-- begin read only
procedure Test_C_Get_Thread (Gnattest_T : in out Test);
procedure Test_C_Get_Thread_97edc5 (Gnattest_T : in out Test) renames Test_C_Get_Thread;
-- id:2.2/97edc547916ca499/C_Get_Thread/1/0/
procedure Test_C_Get_Thread (Gnattest_T : in out Test) is
-- ss_utils.ads:94:4:C_Get_Thread
-- end read only
pragma Unreferenced (Gnattest_T);
begin
AUnit.Assertions.Assert (True, "C_Get_Thread");
-- begin read only
end Test_C_Get_Thread;
-- end read only
-- begin read only
-- procedure Test_Read_Mark (Gnattest_T : in out Test_);
-- procedure Test_Read_Mark_8404db (Gnattest_T : in out Test_) renames Test_Read_Mark;
-- id:2.2/8404db30c2a22d7a/Read_Mark/1/1/
-- procedure Test_Read_Mark (Gnattest_T : in out Test_) is
-- end read only
-- begin read only
-- end Test_Read_Mark;
-- end read only
-- begin read only
-- procedure Test_Write_Mark (Gnattest_T : in out Test_);
-- procedure Test_Write_Mark_99a74f (Gnattest_T : in out Test_) renames Test_Write_Mark;
-- id:2.2/99a74ffb3f48c3b7/Write_Mark/1/1/
-- procedure Test_Write_Mark (Gnattest_T : in out Test_) is
-- end read only
-- begin read only
-- end Test_Write_Mark;
-- end read only
-- begin read only
-- id:2.2/02/
--
-- This section can be used to add elaboration code for the global state.
--
begin
-- end read only
null;
-- begin read only
-- end read only
end Ss_Utils.Test_Data.Tests;

40
repos/libports/src/lib/ada/runtimelib/gnattest/tests/ss_utils-test_data-tests.ads
View File

@ -1,40 +0,0 @@
-- This package has been generated automatically by GNATtest.
-- Do not edit any part of it, see GNATtest documentation for more details.
-- begin read only
with Gnattest_Generated;
package Ss_Utils.Test_Data.Tests is
type Test is new GNATtest_Generated.GNATtest_Standard.Ss_Utils.Test_Data.Test
with null record;
procedure Test_Get_Mark_205a8b (Gnattest_T : in out Test);
-- ss_utils.ads:36:4:Get_Mark
procedure Test_Set_Mark_75973c (Gnattest_T : in out Test);
-- ss_utils.ads:44:4:Set_Mark
procedure Test_Allocate_Stack_247b78 (Gnattest_T : in out Test);
-- ss_utils.ads:53:4:Allocate_Stack
procedure Test_S_Allocate_70b783 (Gnattest_T : in out Test);
-- ss_utils.ads:61:4:S_Allocate
procedure Test_S_Mark_a8299f (Gnattest_T : in out Test);
-- ss_utils.ads:68:4:S_Mark
procedure Test_S_Release_666a46 (Gnattest_T : in out Test);
-- ss_utils.ads:74:4:S_Release
procedure Test_C_Alloc_08db82 (Gnattest_T : in out Test);
-- ss_utils.ads:80:4:C_Alloc
procedure Test_C_Free_6747d0 (Gnattest_T : in out Test);
-- ss_utils.ads:88:4:C_Free
procedure Test_C_Get_Thread_97edc5 (Gnattest_T : in out Test);
-- ss_utils.ads:94:4:C_Get_Thread
end Ss_Utils.Test_Data.Tests;
-- end read only

20
repos/libports/src/lib/ada/runtimelib/gnattest/tests/ss_utils-test_data.adb
View File

@ -1,20 +0,0 @@
-- This package is intended to set up and tear down the test environment.
-- Once created by GNATtest, this package will never be overwritten
-- automatically. Contents of this package can be modified in any way
-- except for sections surrounded by a 'read only' marker.
package body Ss_Utils.Test_Data is
procedure Set_Up (Gnattest_T : in out Test) is
pragma Unreferenced (Gnattest_T);
begin
null;
end Set_Up;
procedure Tear_Down (Gnattest_T : in out Test) is
pragma Unreferenced (Gnattest_T);
begin
null;
end Tear_Down;
end Ss_Utils.Test_Data;

18
repos/libports/src/lib/ada/runtimelib/gnattest/tests/ss_utils-test_data.ads
View File

@ -1,18 +0,0 @@
-- This package is intended to set up and tear down the test environment.
-- Once created by GNATtest, this package will never be overwritten
-- automatically. Contents of this package can be modified in any way
-- except for sections surrounded by a 'read only' marker.
with AUnit.Test_Fixtures;
package Ss_Utils.Test_Data is
-- begin read only
type Test is new AUnit.Test_Fixtures.Test_Fixture
-- end read only
with null record;
procedure Set_Up (Gnattest_T : in out Test);
procedure Tear_Down (Gnattest_T : in out Test);
end Ss_Utils.Test_Data;

10
repos/libports/src/lib/ada/runtimelib/libc.cc
View File

@ -1,10 +0,0 @@
#include <base/stdint.h>
#include <util/string.h>
extern "C" {
int memcmp(const void *s1, const void *s2, Genode::size_t n)
{
return Genode::memcmp(s1, s2, n);
}
}

28
repos/libports/src/lib/ada/runtimelib/s-secsta_c.cc
View File

@ -1,28 +0,0 @@
#include <base/log.h>
#include <base/thread.h>
/*
* The Mark_Id type defined in libports/src/lib/ada/libsrc/s-secsta.ads
* equal to the type defined in GCCs own implementation of s-secsta.ads.
* If the implementation used by GCC changes it needs to be changed in
* this library as well.
*/
#if !(__GNUC__ == 6 && __GNUC_MINOR__ == 3)
#warning Unsupported compiler version, check s-secsta.ads
#endif
extern "C" {
void *get_thread()
{
return static_cast<void *>(Genode::Thread::myself());
}
void *allocate_secondary_stack(void *thread, Genode::size_t size)
{
return static_cast<Genode::Thread *>(thread)->alloc_secondary_stack("ada thread", size);
}
}

50
repos/libports/src/lib/ada/runtimelib/s-soflin_c.cc
View File

@ -1,50 +0,0 @@
/*
* \brief Dummy implementation for Ada softlinks
* \author Johannes Kliemann
* \date 2018-04-16
*
*/
/*
* Copyright (C) 2018 Genode Labs GmbH
* Copyright (C) 2018 Componolit GmbH
*
* This file is part of the Genode OS framework, which is distributed
* under the terms of the GNU Affero General Public License version 3.
*/
#include <base/log.h>
extern "C" {
void system__soft_links__get_current_excep()
{
Genode::warning(__func__, " not implemented");
}
void system__soft_links__get_gnat_exception()
{
Genode::warning(__func__, " not implemented");
}
void system__soft_links__get_jmpbuf_address_soft()
{
Genode::warning(__func__, " not implemented");
}
void system__soft_links__set_jmpbuf_address_soft()
{
Genode::warning(__func__, " not implemented");
}
void system__soft_links__lock_task()
{
Genode::warning(__func__, " not implemented");
}
void system__soft_links__unlock_task()
{
Genode::warning(__func__, " not implemented");
}
}

158
repos/libports/src/lib/ada/runtimelib/ss_utils.adb
View File

@ -1,158 +0,0 @@
package body Ss_Utils
with SPARK_Mode
is
procedure Get_Mark (
T : Thread;
Thread_Registry : in out Registry;
E : out Mark
)
is
Thread_Entry : Long_Integer := -1;
First_Free_Entry : Long_Integer := -1;
begin
Search :
for E in Thread_Registry'Range loop
pragma Loop_Invariant (First_Free_Entry < 128);
pragma Loop_Invariant (Thread_Entry < 128);
if First_Free_Entry = -1 and then
Thread_Registry (E).Id = Invalid_Thread
then
First_Free_Entry := E;
end if;
if T = Thread_Registry (E).Id then
Thread_Entry := E;
exit Search;
end if;
end loop Search;
if Thread_Entry < 0 then
if First_Free_Entry >= 0 then
Thread_Registry (First_Free_Entry).Id := T;
Thread_Registry (First_Free_Entry).Data :=
(Base => System.Null_Address,
Top => 0);
Thread_Entry := First_Free_Entry;
else
raise Constraint_Error;
end if;
end if;
if Thread_Registry (Thread_Entry).Data.Base = System.Null_Address then
Thread_Registry (Thread_Entry).Data :=
(Base => Allocate_Stack (T, Secondary_Stack_Size),
Top => 0);
end if;
E := Thread_Registry (Thread_Entry).Data;
end Get_Mark;
procedure Set_Mark (
T : Thread;
M : Mark;
Thread_Registry : in out Registry
)
is
Thread_Entry : Long_Integer := -1;
begin
if T = Invalid_Thread then
raise Constraint_Error;
end if;
if M.Base = System.Null_Address then
raise Constraint_Error;
end if;
Search :
for E in Thread_Registry'Range loop
pragma Loop_Invariant (Thread_Entry < 128);
if T = Thread_Registry (E).Id then
Thread_Entry := E;
exit Search;
end if;
end loop Search;
if Thread_Entry < 0 then
raise Constraint_Error;
end if;
Thread_Registry (Thread_Entry).Data := M;
end Set_Mark;
function Allocate_Stack (
T : Thread;
Size : SSE.Storage_Count
) return System.Address
is
Stack : System.Address;
begin
if T = Invalid_Thread then
raise Constraint_Error;
end if;
Stack := C_Alloc (T, Size);
if Stack = System.Null_Address then
raise Storage_Error;
end if;
return Stack;
end Allocate_Stack;
procedure S_Allocate (
Address : out System.Address;
Storage_Size : SSE.Storage_Count;
Reg : in out Registry;
T : Thread
)
is
M : Mark;
begin
Get_Mark (T, Reg, M);
if M.Top < Secondary_Stack_Size and then
Storage_Size < Secondary_Stack_Size and then
Storage_Size + M.Top < Secondary_Stack_Size
then
M.Top := M.Top + Storage_Size;
Address := M.Base - M.Top;
else
raise Storage_Error;
end if;
Set_Mark (T, M, Reg);
end S_Allocate;
procedure S_Mark (
Stack_Base : out System.Address;
Stack_Ptr : out SSE.Storage_Count;
Reg : in out Registry;
T : Thread
)
is
M : Mark;
begin
Get_Mark (T, Reg, M);
Stack_Base := M.Base;
Stack_Ptr := M.Top;
end S_Mark;
procedure S_Release (
Stack_Base : System.Address;
Stack_Ptr : SSE.Storage_Count;
Reg : in out Registry;
T : Thread
)
is
LM : Mark;
begin
Get_Mark (T, Reg, LM);
if Stack_Ptr > LM.Top or Stack_Base /= LM.Base
then
raise Program_Error;
end if;
LM.Top := Stack_Ptr;
Set_Mark (T, LM, Reg);
end S_Release;
end Ss_Utils;

107
repos/libports/src/lib/ada/runtimelib/ss_utils.ads
View File

@ -1,107 +0,0 @@
with System;
with System.Storage_Elements;
use all type System.Address;
use all type System.Storage_Elements.Storage_Offset;
package Ss_Utils
with SPARK_Mode
is
package SSE renames System.Storage_Elements;
type Thread is new System.Address;
Invalid_Thread : constant Thread := Thread (System.Null_Address);
type Mark is
record
Base : System.Address;
Top : SSE.Storage_Count;
end record;
type Registry_Entry is
record
Id : Thread;
Data : Mark;
end record;
type Registry is array (Long_Integer range 0 .. 127) of Registry_Entry;
Null_Registry : constant Registry := (others =>
(Id => Invalid_Thread,
Data => (Base => System.Null_Address,
Top => 0)));
Secondary_Stack_Size : constant SSE.Storage_Count := 768 * 1024;
procedure Get_Mark (
T : Thread;
Thread_Registry : in out Registry;
E : out Mark
)
with
Pre => T /= Invalid_Thread,
Post => (E.Base /= System.Null_Address);
procedure Set_Mark (
T : Thread;
M : Mark;
Thread_Registry : in out Registry
)
with
Pre => (M.Base /= System.Null_Address and
T /= Invalid_Thread);
function Allocate_Stack (
T : Thread;
Size : SSE.Storage_Count
) return System.Address
with
Pre => T /= Invalid_Thread,
Post => Allocate_Stack'Result /= System.Null_Address;
procedure S_Allocate (
Address : out System.Address;
Storage_Size : SSE.Storage_Count;
Reg : in out Registry;
T : Thread
)
with
Pre => T /= Invalid_Thread;
procedure S_Mark (
Stack_Base : out System.Address;
Stack_Ptr : out SSE.Storage_Count;
Reg : in out Registry;
T : Thread
)
with
Pre => T /= Invalid_Thread;
procedure S_Release (
Stack_Base : System.Address;
Stack_Ptr : SSE.Storage_Count;
Reg : in out Registry;
T : Thread
)
with
Pre => T /= Invalid_Thread;
function C_Alloc (
T : Thread;
Size : SSE.Storage_Count
) return System.Address
with
Import,
Convention => C,
External_Name => "allocate_secondary_stack",
Pre => T /= Invalid_Thread,
Post => C_Alloc'Result /= System.Null_Address,
Global => null;
function C_Get_Thread return Thread
with
Import,
Convention => C,
External_Name => "get_thread";
end Ss_Utils;