Thomas Heijligen has uploaded this change for review. ( https://review.coreboot.org/c/libhwbase/+/37530 )
Change subject: [WIP] Printf like debugging ......................................................................
[WIP] Printf like debugging
Change-Id: I4989761d1b127c67510e50d7ecc657e4b0f475e5 Signed-off-by: Thomas Heijligen thomas.heijligen@secunet.com --- M debug/Makefile.inc A debug/hw-print.adb A debug/hw-print.ads M gnat.adc 4 files changed, 282 insertions(+), 0 deletions(-)
git pull ssh://review.coreboot.org:29418/libhwbase refs/changes/30/37530/1
diff --git a/debug/Makefile.inc b/debug/Makefile.inc index b636a6f..7528e8c 100644 --- a/debug/Makefile.inc +++ b/debug/Makefile.inc @@ -1,4 +1,6 @@ hw-y += hw-debug.ads hw-y += hw-debug.adb +hw-y += hw-print.ads +hw-y += hw-print.adb hw-$(CONFIG_HWBASE_DEBUG_NULL) += null/hw-debug_sink.ads hw-$(CONFIG_HWBASE_DEBUG_TEXT_IO) += text_io/hw-debug_sink.ads diff --git a/debug/hw-print.adb b/debug/hw-print.adb new file mode 100644 index 0000000..ab9e623 --- /dev/null +++ b/debug/hw-print.adb @@ -0,0 +1,269 @@ +with HW; +with HW.Debug; +with Interfaces; +use HW; +use HW.Debug; +use Interfaces; + +package body HW.Print with + SPARK_Mode => On +is + + type Arg_Conversion is + (Arg_Invalid, + Arg_Int, + Arg_UInt, + Arg_Hex, + Arg_Char, + Arg_String + ); + + type Arg_Flags is + (Arg_Flag_Alternate_Form, + Arg_Flag_Padding, + Arg_Flag_Left_Adjusted, + Arg_Flag_Space, + Arg_Flag_Sign + ); + + type Arg_Flag_List is array (Arg_Flags) of Boolean; + + type Arg_Length is + (Arg_Length_Normal, + Arg_Length_Long, + Arg_Length_Long_Long + ); + + type Arg_T is record + Conversion : Arg_Conversion; + Flags : Arg_Flag_List; + Length : Arg_Length; + Padding : Natural; + Position : Integer; + end record; + +----------------------------------------------------------------------------------------------- + + procedure Parse_And_Put (Format_String : in String; Arg : out Arg_T; Pos : in out Integer) with + Pre => Format_String'First <= Format_String'Last and Pos >= Format_String'First and Format_String'Last < Integer'Last + is + + function Char_To_UInt (Item : in Character) return Natural with + Pre => Item in '0' .. '9' + is begin + return Character'Pos (Item) - Character'Pos ('0'); + end Char_To_UInt; + + type State_T is ( + State_Normal, + State_Arg_Flags, + State_Arg_Flag_Padding, + State_Arg_Modifier, + State_Arg_Modifier_Length, + State_Arg_Conversion + ); + + State : State_T := State_Normal; + + begin + + Arg := (Conversion => Arg_Invalid, Flags => (others => false), Length => Arg_Length_Normal, Padding => 0, Position => 0); + + while Pos <= Format_String'Last loop + pragma loop_invariant (Pos >= Format_String'First); + + case State is + when State_Normal => + case Format_String (Pos) is + when '%' => + State := State_Arg_Flags; + Arg.Position := Pos; + when others => + Put (Format_String (Pos .. Pos)); + end case; + + when State_Arg_Flags => + case Format_String (Pos) is + when '%' => + State := State_Normal; + Put ("%"); + when '#' => + Arg.Flags (Arg_Flag_Alternate_Form) := True; + when '0' => + Arg.Flags (Arg_Flag_Padding) := True; + when '-' => + Arg.Flags (Arg_Flag_Left_Adjusted) := True; + when ' ' => + Arg.Flags (Arg_Flag_Space) := True; + when '+' => + Arg.Flags (Arg_Flag_Sign) := True; + when others => + Pos := Pos - 1; + State := State_Arg_Flag_Padding; + end case; + + when State_Arg_Flag_Padding => + case Format_String (Pos) is + when '0' .. '9' => + Arg.Padding := Arg.Padding * 10 + Char_To_UInt (Format_String (Pos)); + when others => + Pos := Pos - 1; + State := State_Arg_Modifier; + end case; + + when State_Arg_Modifier => + case Format_String (Pos) is + when 'l' => + Arg.Length := Arg_Length_Long; + State := State_Arg_Modifier_Length; + when others => + Pos := Pos - 1; + State := State_Arg_Conversion; + end case; + + when State_Arg_Modifier_Length => + case Format_String (Pos) is + when 'l' => + Arg.Length := Arg_Length_Long_Long; + when others => + Pos := Pos - 1; + State := State_Arg_Modifier; + end case; + + when State_Arg_Conversion => + case Format_String (Pos) is + when 'd' => + Arg.Conversion := Arg_Int; + when 'i' => + Arg.Conversion := Arg_Int; + when 'x' => + Arg.Conversion := Arg_Hex; + when 'u' => + Arg.Conversion := Arg_UInt; + when 'c' => + Arg.Conversion := Arg_Char; + when 's' => + Arg.Conversion := Arg_String; + when others => + null; + end case; + Pos := Pos + 1; + exit; + end case; + Pos := Pos + 1; + end loop; + + end Parse_And_Put; + +---------------------------------------------------------------------------------------------- + + subtype Word64_String_Range is Positive range 1 .. 20; + subtype Word64_String is String (Word64_String_Range); + type Int_Format is (Base_10, Base_16); + + procedure Word64_To_String + (Output_String : out Word64_String; + String_Begin : out Word64_String_Range; + Item : in Word64; + Base : in Int_Format) + is + + function Get_Character (Item : Word64; Base : Word64) return Character with + Pre => Base > 0 and Base <= 16 + is + + subtype Hex_Range is Natural range 0 .. 15; + type Hex_Characters is array (Hex_Range) of Character; + Character_Set : constant Hex_Characters := ('0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f'); + Tmp : Word64; + begin + Tmp := Item rem Base; + -- GNATprove can't prove mod + --pragma assert ( Tmp = Item mod Base); + if Tmp > 15 then + Tmp := 15; + end if; + return Character_Set (Natural (Tmp)); + end Get_Character; + + + Item_C : Word64; + Item_B : Word64; + begin + Item_C := Item; + Output_String:= " "; + String_Begin := Output_String'Last; + + case (Base) is + when Base_10 => + Item_B := 10; + when Base_16 => + Item_B := 16; + end case; + + loop + Output_String (String_Begin) := Get_Character (Item_C, Item_B); + Item_C := Item_C / Item_B; + pragma loop_invariant (Item_C < Item_B ** String_Begin); + exit when Item_C = 0; + String_Begin := String_Begin - 1; + end loop; + + end Word64_To_String; + +--------------------------------------------------------------------------------------------------------- + + procedure Put_Arg (Item : in Word64; Arg : in Arg_T; Pos : in out Integer) is + Base : Int_Format; + Output : Word64_String; + Output_Begin : Word64_String_Range; + begin + + case Arg.Conversion is + when Arg_UInt => + Base := Base_10; + + when Arg_Hex => + Base := Base_16; + + when others => + Pos := Arg.Position + 1; + Put("%"); + return; + end case; + + Word64_To_String (Output, Output_Begin, Item, Base); + Put (Output (Output_Begin .. Output'Last)); + + end Put_Arg; + + ----------------------------------------------------------------------------------------------- + ----------------------------------------------------------------------------------------------- + + procedure Printf (Format_String : in String) is + begin + Put (Format_String); + end Printf; + + ----------------------------------------------------------------------------------------------- + procedure Printf (Format_String : in String; Arg_1 : in Word64) is + Arg : Arg_T; + Pos : Integer; + begin + Pos := Format_String'First; + Parse_And_Put (Format_String, Arg, Pos); + Put_Arg (Arg_1, Arg, Pos); + + Put (format_String (Pos .. Format_String'Last)); + end Printf; + + ----------------------------------------------------------------------------------------------- + + -- procedure Printk (Level : in Debug_Level; Format_String : in String) is + -- begin + -- if Do_Print (Level) then + -- Printf (Format_String); + -- end if; + -- end Printk; + +end HW.Print; diff --git a/debug/hw-print.ads b/debug/hw-print.ads new file mode 100644 index 0000000..788ffd2 --- /dev/null +++ b/debug/hw-print.ads @@ -0,0 +1,10 @@ +package HW.Print is + + type Debug_Level is (Emerg, Alert, Crit, Err, Warning, Notice, Info, Debug, Spew); + + procedure Printf (Format_String : in String); + procedure Printf (Format_String : in String; Arg_1 : in Word64); + +-- procedure Printk (Level : in Debug_Level; Format_String : in String); + +end HW.Print; diff --git a/gnat.adc b/gnat.adc index 3494eba..2d49df2 100644 --- a/gnat.adc +++ b/gnat.adc @@ -1,6 +1,7 @@ pragma Restrictions (No_Allocators); pragma Restrictions (No_Calendar); pragma Restrictions (No_Dispatch); + pragma Restrictions (No_Fixed_Point); pragma Restrictions (No_Floating_Point); pragma Restrictions (No_Implicit_Dynamic_Code);
Nico Huber has posted comments on this change. ( https://review.coreboot.org/c/libhwbase/+/37530 )
Change subject: [WIP] Printf like debugging ......................................................................
Patch Set 1:
(8 comments)
I like SPARK ;) this is so much better to read than what I would have expected from a C implementation. Beside the indentation of course, we need to work on your editor configuration :)
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb File debug/hw-print.adb:
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@47 PS1, Line 47: Parse_And_Put This is rather Put_And_Parse :)
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@82 PS1, Line 82: Put (Format_String (Pos .. Pos)); Slight optimization: Currently this puts chars one by one. If we'd keep the start and end of the non-format string, we could put it all at once.
e.g. on top
is Non_Format_Start : constant Integer := Pos; Non_Format_End : Integer; ... begin
then here
when '%' => Non_Format_End := Pos;
and in the end
if Arg.Conversion = Arg_Invalid then Put (Format_String); elsif Non_Format_End > Integer'First then Put (Format_String (Non_Format_Start .. Non_Format_End - 1)); end if;
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@118 PS1, Line 118: State := State_Arg_Modifier_Length; Alternatively, we could skip the `Modifier_Length` substate and use the state of `Arg.Length` instead, e.g.
when State_Arg_Modifier => case Format_String (Pos) is when 'l' => case Arg.Length is when Arg_Length_Normal => Arg.Length := Arg_Length_Long; when Arg_Length_Long => Arg.Length := Arg_Length_Long_Long; when others => Pos := Pos - 1; State := State_Arg_Conversion; end case; when others => Pos := Pos - 1; State := State_Arg_Conversion; end case;
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@130 PS1, Line 130: State := State_Arg_Modifier; Nit, we already know that `State_Arg_Modifier` will fall through to `State_Arg_Conversion`. We can as well go directly to the latter.
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@162 PS1, Line 162: type Int_Format is (Base_10, Base_16); This enumeration type doesn't seem too useful. Just using
subtype Int_Format is Positive range 2 .. 16;
would make the code easier to read (less conversions, but still type safe).
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@162 PS1, Line 162: Int_Format Maybe `Int_Base` instead?
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@166 PS1, Line 166: String_Begin Maybe just name it `Pos`. Less clear for the caller, but would make the code in here easier to read.
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@207 PS1, Line 207: pragma loop_invariant (Item_C < Item_B ** String_Begin); Maybe we have to make it explicit that `Item_B` doesn't change in the loop. I'll give that a shot.
Nico Huber has posted comments on this change. ( https://review.coreboot.org/c/libhwbase/+/37530 )
Change subject: [WIP] Printf like debugging ......................................................................
Patch Set 1:
(3 comments)
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb File debug/hw-print.adb:
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@48 PS1, Line 48: Format_String'First <= Format_String'Last and First precondition seems not needed (anymore)?
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@108 PS1, Line 108: Arg.Padding := Arg.Padding * 10 + Char_To_UInt (Format_String (Pos)); GNATprove is right to complain here about potential overflows. We don't know what string we will be called with, e.g. if it starts with "%111111111111" it would overflow.
So we need to explicitly check
if Arg.Padding <= Natural'Last / 10 - 9 then
I would say, we can just ignore errors.
To prove this, we need to know that Char_To_UInt() returns at most 9. Three ways come to mind:
Make it an expression function (this way callers know exactly what it does):
function Char_To_UInt (Item : in Character) return Natural is (Character'Pos (Item) - Character'Pos ('0')) with Pre => Item in '0' .. '9';
Constrain the return type, e.g.
subtype Decimal_Digit is Natural range 0 .. 9;
Or add a post condition:
Post => Char_To_UInt'Result in 0 .. 9;
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@207 PS1, Line 207: pragma loop_invariant (Item_C < Item_B ** String_Begin);
Maybe we have to make it explicit that `Item_B` doesn't change in […]
Meh, whatever, even with that and without overflowing Word64 in the exponentiation, I don't get anything useful.
Making the code more explicit shouldn't hurt:
for Pos in reverse Word64_String_Range loop Output_String (Pos) := ... ... String_Begin := Pos; exit when Item_C = 0; end loop;
Paul Menzel has posted comments on this change. ( https://review.coreboot.org/c/libhwbase/+/37530 )
Change subject: [WIP] Printf like debugging ......................................................................
Patch Set 1:
(2 comments)
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb File debug/hw-print.adb:
https://review.coreboot.org/c/libhwbase/+/37530/1/debug/hw-print.adb@11 PS1, Line 11: Remove trailing spaces?
https://review.coreboot.org/c/libhwbase/+/37530/1/gnat.adc File gnat.adc:
https://review.coreboot.org/c/libhwbase/+/37530/1/gnat.adc@4 PS1, Line 4: Unrelated.
Hello Nico Huber, Patrick Georgi, Martin Roth,
I'd like you to reexamine a change. Please visit
https://review.coreboot.org/c/libhwbase/+/37530
to look at the new patch set (#2).
Change subject: [WIP] Printf like debugging ......................................................................
[WIP] Printf like debugging
Change-Id: I4989761d1b127c67510e50d7ecc657e4b0f475e5 Signed-off-by: Thomas Heijligen thomas.heijligen@secunet.com --- M debug/Makefile.inc A debug/hw-print.adb A debug/hw-print.ads 3 files changed, 290 insertions(+), 0 deletions(-)
git pull ssh://review.coreboot.org:29418/libhwbase refs/changes/30/37530/2
Hello Nico Huber, Patrick Georgi, Martin Roth,
I'd like you to reexamine a change. Please visit
https://review.coreboot.org/c/libhwbase/+/37530
to look at the new patch set (#3).
Change subject: [WIP] Printf like debugging ......................................................................
[WIP] Printf like debugging
Change-Id: I4989761d1b127c67510e50d7ecc657e4b0f475e5 Signed-off-by: Thomas Heijligen thomas.heijligen@secunet.com --- M debug/Makefile.inc A debug/hw-print.adb A debug/hw-print.ads 3 files changed, 437 insertions(+), 0 deletions(-)
git pull ssh://review.coreboot.org:29418/libhwbase refs/changes/30/37530/3
-
Nico Huber (Code Review) -
Paul Menzel (Code Review)
-
Thomas Heijligen (Code Review)