From 8bffc33d8f45ab31dc5a0b6d14637a79153ad290 Mon Sep 17 00:00:00 2001 From: Johannes Kliemann Date: Mon, 16 Apr 2018 14:01:41 +0200 Subject: [PATCH] ada: test secondary stack --- repos/libports/run/ada_secondary_stack.run | 33 +++++ .../src/test/ada_secondary_stack/main.cc | 46 +++++++ .../src/test/ada_secondary_stack/stack.adb | 116 ++++++++++++++++++ .../src/test/ada_secondary_stack/stack.ads | 45 +++++++ .../src/test/ada_secondary_stack/stack.gpr | 5 + .../src/test/ada_secondary_stack/target.mk | 4 + 6 files changed, 249 insertions(+) create mode 100644 repos/libports/run/ada_secondary_stack.run create mode 100644 repos/libports/src/test/ada_secondary_stack/main.cc create mode 100644 repos/libports/src/test/ada_secondary_stack/stack.adb create mode 100644 repos/libports/src/test/ada_secondary_stack/stack.ads create mode 100644 repos/libports/src/test/ada_secondary_stack/stack.gpr create mode 100644 repos/libports/src/test/ada_secondary_stack/target.mk diff --git a/repos/libports/run/ada_secondary_stack.run b/repos/libports/run/ada_secondary_stack.run new file mode 100644 index 0000000000..1f548ad508 --- /dev/null +++ b/repos/libports/run/ada_secondary_stack.run @@ -0,0 +1,33 @@ +build "core init test/ada_secondary_stack" + +create_boot_directory + +install_config { + + + + + + + + + + + + + + + +} + +build_boot_image "core ld.lib.so ada.lib.so init test-ada_secondary_stack" + +append qemu_args "-nographic " + +run_genode_until {child "test-ada_secondary_stack" exited with exit value 0.*} 20 + +grep_output {successful} + +compare_output_to { + [init -> test-ada_secondary_stack] secondary stack test successful +} diff --git a/repos/libports/src/test/ada_secondary_stack/main.cc b/repos/libports/src/test/ada_secondary_stack/main.cc new file mode 100644 index 0000000000..9e55581a28 --- /dev/null +++ b/repos/libports/src/test/ada_secondary_stack/main.cc @@ -0,0 +1,46 @@ + +#include +#include + +extern "C" void stack__calloc(int); +extern "C" void stack__ralloc(); +extern "C" void stack__salloc(); + +extern "C" void print_stack(char* data) +{ + Genode::log(Genode::Cstring(data)); +} + +extern "C" void print_recursion(int r) +{ + Genode::log("recursion: ", r); +} + +extern "C" void print_stage(int s) +{ + Genode::log("stage: ", s); +} + +extern "C" void __gnat_rcheck_CE_Overflow_Check() +{ + Genode::warning(__func__, " not implemented"); +} + +void Component::construct(Genode::Env &env) +{ + Genode::log("running iteration test"); + stack__calloc(32); + stack__calloc(128); + stack__calloc(512); + stack__calloc(1024); + + Genode::log("running recursion test"); + stack__ralloc(); + + Genode::log("running stage test"); + stack__salloc(); + + Genode::log("secondary stack test successful"); + + env.parent().exit(0); +} diff --git a/repos/libports/src/test/ada_secondary_stack/stack.adb b/repos/libports/src/test/ada_secondary_stack/stack.adb new file mode 100644 index 0000000000..699579a42f --- /dev/null +++ b/repos/libports/src/test/ada_secondary_stack/stack.adb @@ -0,0 +1,116 @@ +with System; + +package body Stack +with SPARK_Mode +is + + pragma Suppress (All_Checks); + + ------------ + -- Calloc -- + ------------ + + procedure Calloc + (Size : Integer) + with SPARK_Mode => Off + is + procedure Print (Str : System.Address) + with + Import, + Convention => C, + External_Name => "print_stack"; + + Buf : Buffer := Alloc (Size) & Character'Val (0); + begin + Print (Buf'Address); + end Calloc; + + procedure Ralloc + is + R : constant Integer := 0; + B : Buffer := Recursive_Alloc (R); + begin + null; + end Ralloc; + + ----------- + -- Alloc -- + ----------- + + function Alloc + (Size : Integer) + return Buffer + is + Buf : constant Buffer (1 .. Size) := (others => '0'); + begin + return Buf; + end Alloc; + + function Recursive_Alloc (Round : Integer) return Buffer + is + procedure Print (R : Integer) + with + Import, + Convention => C, + External_Name => "print_recursion"; + + Buf : constant Buffer (1 .. 256) := (others => '0'); + begin + Print (Round); + if Round < 10 then + return Buf & Recursive_Alloc (Round + 1); + else + return Buf; + end if; + end Recursive_Alloc; + + procedure Salloc + is + S : constant Integer := 16; + B : Buffer := Stage_1 (S); + begin + Print_Stage (0); + end Salloc; + + function Stage_1 ( + Size : Integer + ) return Buffer + is + Buf : Buffer (1 .. Size) := (others => '0'); + begin + Print_Stage (1); + declare + Buf_2 : constant Buffer := Stage_2 (Size); + begin + Buf := Buf_2; + end; + return Buf; + end Stage_1; + + + function Stage_2 ( + Size : Integer + ) return Buffer + is + Buf : Buffer (1 .. Size); + begin + Print_Stage (2); + declare + Buf2 : constant Buffer := Stage_3 (Size); + begin + Buf := Buf2; + end; + return Buf; + end Stage_2; + + function Stage_3 ( + Size : Integer + ) return Buffer + is + Buf : Buffer (1 .. Size) := (others => '3'); + begin + Print_Stage (3); + return Buf; + end Stage_3; + +end Stack; diff --git a/repos/libports/src/test/ada_secondary_stack/stack.ads b/repos/libports/src/test/ada_secondary_stack/stack.ads new file mode 100644 index 0000000000..ea60571564 --- /dev/null +++ b/repos/libports/src/test/ada_secondary_stack/stack.ads @@ -0,0 +1,45 @@ +package Stack +with SPARK_Mode +is + + type Buffer is array (Integer range <>) of Character; + + procedure Calloc ( + Size : Integer + ); + + procedure Ralloc; + + function Alloc ( + Size : Integer + ) return Buffer; + + function Recursive_Alloc ( + Round : Integer + ) return Buffer; + + procedure Salloc; + + function Stage_1 ( + Size : Integer + ) return Buffer; + + function Stage_2 ( + Size : Integer + ) return Buffer; + + function Stage_3 ( + Size : Integer + ) return Buffer; + +private + + procedure Print_Stage ( + Stage : Integer + ) + with + Import, + Convention => C, + External_Name => "print_stage"; + +end Stack; diff --git a/repos/libports/src/test/ada_secondary_stack/stack.gpr b/repos/libports/src/test/ada_secondary_stack/stack.gpr new file mode 100644 index 0000000000..3294881527 --- /dev/null +++ b/repos/libports/src/test/ada_secondary_stack/stack.gpr @@ -0,0 +1,5 @@ +project stack is + + for Source_Dirs use ("."); + +end stack; diff --git a/repos/libports/src/test/ada_secondary_stack/target.mk b/repos/libports/src/test/ada_secondary_stack/target.mk new file mode 100644 index 0000000000..393a7c5255 --- /dev/null +++ b/repos/libports/src/test/ada_secondary_stack/target.mk @@ -0,0 +1,4 @@ +TARGET = test-ada_secondary_stack +SRC_ADB = stack.adb +SRC_CC = main.cc +LIBS = base ada