streaming mode, Ada support

ADA_RTL2/src/adaasn1rtl-encoding.adb

@@ -1,3 +1,4 @@
+with user_code;
 
 package body adaasn1rtl.encoding with Spark_Mode is
 
@@ -170,6 +171,8 @@ package body adaasn1rtl.encoding with Spark_Mode is
    is
       (Bitstream'(Size_In_Bytes    => Bitstream_Size_In_Bytes,
                  Current_Bit_Pos  => 0,
+                 pushDataPrm  => 0,
+                 fetchDataPrm => 0,
                  Buffer           => (others => 0)));
 
 
@@ -187,8 +190,9 @@ package body adaasn1rtl.encoding with Spark_Mode is
                bs.buffer(Current_Byte) and (not MASKS(Current_Bit)));
 
       bs.Current_Bit_Pos := bs.Current_Bit_Pos + 1;   
+      bitstrean_push_data_if_required(bs);
 
-      end;
+   end;
 
    procedure BitStream_ReadBit(bs : in out BitStream; Bit_Value : out BIT; result :    out Boolean)
    is
@@ -204,6 +208,7 @@ package body adaasn1rtl.encoding with Spark_Mode is
       end if;
 
       bs.Current_Bit_Pos := bs.Current_Bit_Pos + 1;   
+      bitstrean_fetch_data_if_required(bs);
    end;
 
 
@@ -233,6 +238,7 @@ package body adaasn1rtl.encoding with Spark_Mode is
          bs.buffer(Current_Byte) := ByteVal;
       end if;
        bs.Current_Bit_Pos := bs.Current_Bit_Pos + 8;
+       bitstrean_push_data_if_required(bs);
    end;
 
 
@@ -255,6 +261,8 @@ package body adaasn1rtl.encoding with Spark_Mode is
 --        end if;
       Byte_Value := BitStream_PeekByte(bs, 0);
       bs.Current_Bit_Pos := bs.Current_Bit_Pos + 8;
+      bitstrean_fetch_data_if_required(bs);
+
 
    end;
 
@@ -299,6 +307,8 @@ package body adaasn1rtl.encoding with Spark_Mode is
          Byte_Value := Byte_Value and 16#0F#;
       end if;
       bs.Current_Bit_Pos := bs.Current_Bit_Pos + 4;
+      bitstrean_fetch_data_if_required(bs);
+
    end;
 
 
@@ -342,6 +352,8 @@ package body adaasn1rtl.encoding with Spark_Mode is
 
          end if;
          bs.Current_Bit_Pos := bs.Current_Bit_Pos + nBits;
+         bitstrean_push_data_if_required(bs);
+
       end if;
    end;
 
@@ -406,6 +418,7 @@ package body adaasn1rtl.encoding with Spark_Mode is
 --        end if;
       Byte_Value := BitStream_PeekPartialByte(bs, 0, nBits);
       bs.Current_Bit_Pos := bs.Current_Bit_Pos + nBits;
+      bitstrean_fetch_data_if_required(bs);
    end;
 
    function BitStream_PeekPartialByte(bs : in BitStream; offset : Natural; nBits : in BIT_RANGE) return Asn1Byte
@@ -827,8 +840,46 @@ package body adaasn1rtl.encoding with Spark_Mode is
 
 
 
+--  
+--  void bitstrean_fetch_data_if_required(BitStream* pStrm) {
+--  	if (pStrm->currentByte == pStrm->count) {
+--  		fetchData(pStrm, pStrm->fetchDataPrm);
+--  		pStrm->currentByte = 0;
+--  	}
+--  }
+--  
+--  
+--  void bitstrean_push_data_if_required(BitStream* pStrm) {
+--  	if (pStrm->currentByte == pStrm->count) {
+--  		pushData(pStrm, pStrm->pushDataPrm);
+--  		pStrm->currentByte = 0;
+--  	}
+--  }
 
+pragma Warnings (Off, "formal parameter ""bs"" is not modified");
 
-
+    procedure bitstrean_fetch_data_if_required(bs : in out BitStream) 
+    is
+      Current_Byte : constant Integer   := bs.Buffer'First + bs.Current_Bit_Pos / 8;
+      Current_Bit  : constant BIT_RANGE := bs.Current_Bit_Pos mod 8;
+    begin
+        if Current_Bit = 0 and Current_Byte = bs.Size_In_Bytes+1 and bs.fetchDataPrm > 0 then
+            user_code.fetch_data(bs, bs.fetchDataPrm);
+            bs.Current_Bit_Pos := 0;
+        end if;
+    end;
+
+    procedure bitstrean_push_data_if_required(bs : in out BitStream) 
+    is
+      Current_Byte : constant Integer   := bs.Buffer'First + bs.Current_Bit_Pos / 8;
+      Current_Bit  : constant BIT_RANGE := bs.Current_Bit_Pos mod 8;
+    begin
+        if Current_Bit = 0 and Current_Byte = bs.Size_In_Bytes+1 and bs.fetchDataPrm > 0 then
+            user_code.push_data(bs, bs.pushDataPrm);
+            bs.Current_Bit_Pos := 0;
+        end if;
+    end;
+
+pragma Warnings (On, "formal parameter ""bs"" is not modified");
 
 end adaasn1rtl.encoding;

ADA_RTL2/src/adaasn1rtl-encoding.ads

@@ -25,11 +25,16 @@ package adaasn1rtl.encoding with Spark_Mode is
    type Bitstream  (Size_In_Bytes:Positive) is record
       Buffer           : OctetBuffer(1 .. Size_In_Bytes) ; 
       Current_Bit_Pos  : Natural;  --current bit for writing or reading in the bitsteam
+      pushDataPrm : Integer := 0;
+      fetchDataPrm : Integer := 0;
+
    end record;
 
    type BitstreamPtr  is record
       Size_In_Bytes    :   Positive;
       Current_Bit_Pos  : Natural;  --current bit for writing or reading in the bitsteam
+      pushDataPrm : Integer := 0;
+      fetchDataPrm : Integer := 0;
    end record;
 
 
@@ -400,6 +405,9 @@ package adaasn1rtl.encoding with Spark_Mode is
                 bs.Current_Bit_Pos   < Natural'Last - bit_terminated_pattern_size_in_bits and then  
                 bs.Size_In_Bytes < Positive'Last/8 and  then
                 bs.Current_Bit_Pos  <= bs.Size_In_Bytes * 8 - bit_terminated_pattern_size_in_bits;
-
+
+    procedure bitstrean_fetch_data_if_required(bs : in out BitStream);
+    procedure bitstrean_push_data_if_required(bs : in out BitStream);
+
 
 end adaasn1rtl.encoding;

Asn1f4/GenerateRTL.fs

@@ -60,7 +60,12 @@ let exportRTL outDir  (l:ProgrammingLanguage) (args:CommandLineSettings)=
         match args.encodings with
         | []    -> ()
         | _     ->
-            writeTextFile (Path.Combine(outDir, "adaasn1rtl-encoding.adb")) (rm.GetString("adaasn1rtl_encoding_adb",null))
+            let adaasn1rtl_encoding_adb = 
+                match args.streamingModeSupport with
+                | false -> rm.GetString("adaasn1rtl_encoding_adb",null).Replace("with user_code;","").Replace("user_code.push_data(bs, bs.pushDataPrm);","").Replace("user_code.fetch_data(bs, bs.fetchDataPrm);","")
+                | true  -> rm.GetString("adaasn1rtl_encoding_adb",null)
+
+            writeTextFile (Path.Combine(outDir, "adaasn1rtl-encoding.adb")) adaasn1rtl_encoding_adb
             writeTextFile (Path.Combine(outDir, "adaasn1rtl-encoding.ads")) (rm.GetString("adaasn1rtl_encoding_ads",null))
 
             if hasUper || hasAcn then

Docs/examples/streaming_mode/ada_out/GPS_project.gpr

@@ -0,0 +1,20 @@
+project GPS_Project is
+
+   for Object_Dir use "bin";
+   for Main use ("mainprogram.adb");
+
+   package Ide is
+      for Default_Switches ("examiner") use ("-vcg", "-dpc", "-sparklib", "-language=2005", "-index_file=spark.idx", "-warning_file=IgnoredExaminerWarnings.wrn", "-config=gnat.cfg", "-output_directory=examiner");
+      for Default_Switches ("sparksimp") use ("-p=4", "-nz", "-victor");
+   end Ide;
+
+   package Compiler is
+      for Default_Switches ("ada") use ("-gnatwae", "-gnat2012", "-g");
+   end Compiler;
+
+   package Pretty_Printer is
+      for Default_Switches ("ada") use ("-i4", "-M200", "--no-separate-is", "--no-separate-loop-then");
+   end Pretty_Printer;
+
+end GPS_Project;
+

Docs/examples/streaming_mode/ada_out/Makefile

@@ -0,0 +1,13 @@
+all:
+	gnatmake -gnat2012 -P GPS_project.gpr mainprogram.adb --subdirs=debug -cargs -g -O0 -gnatwe -gnatwa
+	touch builtWithoutCoverage
+
+coverage:
+	if [ -f builtWithoutCoverage ] ; then make clean ; fi
+	gnatmake -gnat2012 -P GPS_project.gpr mainprogram.adb --subdirs=debug -cargs -g -O0 -gnatwe -gnatwa -fprofile-arcs -ftest-coverage -largs -fprofile-arcs
+	cd bin/debug ; ./mainprogram
+	cd bin/debug ; gcov adaasn1rtl TASTE_Dataview
+
+clean:
+	rm -f builtWithoutCoverage ;
+	gnat clean -r -P GPS_project.gpr --subdirs=debug	

Docs/examples/streaming_mode/ada_out/gnat.cfg

@@ -0,0 +1,25 @@
+package Standard is
+   type Integer is range -2147483648 ..  2147483647;
+   type Float is digits  6 range -3.40282E+38 ..  3.40282E+38;
+   type Short_Short_Integer is range -128 ..  127;
+   type Short_Integer is range -32768 ..  32767;
+   type Long_Integer is range -9223372036854775808 ..  9223372036854775807;
+
+   type Short_Float is digits  6 range -3.40282E+38 ..  3.40282E+38;
+   type Long_Float is digits  15 range -1.79769313486232E+308 ..  1.79769313486232E+308;
+end Standard;
+
+
+package System is
+   Min_Int : constant := -9223372036854775808;
+   Max_Int : constant :=  9223372036854775807;
+
+   Max_Binary_Modulus    : constant := 2 ** 64;
+   Max_Mantissa          : constant := 63;
+
+   Word_Size : constant := 64;
+
+
+end System;
+
+

Docs/examples/streaming_mode/ada_out/mainprogram.adb

@@ -0,0 +1,12 @@
+
+
+with user_code;
+
+
+
+FUNCTION MainProgram RETURN INTEGER
+IS 
+BEGIN
+   user_code.streaming_mode_test;
+   return 0;
+end MainProgram;

Docs/examples/streaming_mode/ada_out/user_code.adb

@@ -0,0 +1,145 @@
+with Interfaces;
+
+WITH Ada.Text_IO;
+use Ada.Text_IO;
+WITH adaasn1rtl;
+with TASTE_Dataview;
+use TASTE_Dataview;
+use adaasn1rtl;
+
+with Ada.Sequential_IO;
+
+package body user_code is
+
+   package Seq_IO is new Ada.Sequential_IO(Asn1Byte);
+
+   procedure Write_BitStream_To_File (bs : in BitStream; Filename : in String) is
+      Out_File : Seq_IO.File_Type;
+      --Current_Bit  : constant BIT_RANGE := bs.Current_Bit_Pos mod 8;
+      --End_Byte : constant Integer   := bs.Buffer'First + bs.Current_Bit_Pos / 8 + (if Current_Bit > 0 then 1 else 0);
+   begin
+      Seq_IO.Create(Out_File, Seq_IO.Out_File, Filename);
+      for i in  bs.Buffer'Range loop
+         Seq_IO.Write(Out_File, bs.Buffer(i));
+      end loop;
+
+
+      Seq_IO.Close(Out_File);
+   end;
+
+
+
+
+
+
+procedure initialize(tc_data : in out A1) is
+i1 : integer;
+begin
+    i1 := 1;
+    while i1<= 1000 loop
+        pragma Loop_Invariant (i1 >=1 and i1<=1000);
+
+        tc_data.Data(i1).a11 := Interfaces.Unsigned_64(i1*50);
+            --set a12
+        tc_data.Data(i1).a12 := Interfaces.Unsigned_64(i1*50);
+
+        i1 := i1 + 1;
+    end loop;
+
+end;
+
+
+procedure encode_no_streaming_mode(val : in  A1; Filename : in String; success: out Boolean) is
+    result      : adaasn1rtl.ASN1_RESULT;
+    stream      : adaasn1rtl.encoding.Bitstream := adaasn1rtl.encoding.BitStream_init(TASTE_Dataview.A1_REQUIRED_BYTES_FOR_ENCODING);
+begin
+    TASTE_Dataview.A1_Encode(val, stream, result);
+    if result.Success then
+      Write_BitStream_To_File(stream, Filename);
+      success := true;
+    else
+       Put_Line ("Error: Encoding failed !!!");
+      success := false;
+    end if;
+
+end;
+
+
+procedure read_from_file(bs : in out adaasn1rtl.encoding.Bitstream; ft : in out Seq_IO.File_Type) is
+begin
+      for i in  bs.Buffer'Range loop
+         exit when Seq_IO.End_Of_File(ft);
+         Seq_IO.Read(ft, bs.Buffer(i));
+
+      end loop;
+
+end;
+
+ft : Seq_IO.File_Type;
+
+pragma Warnings (Off, "formal parameter ""prm"" is not referenced");
+
+procedure fetch_data(bs : in out BitStream; prm : Integer)
+is
+begin
+    read_from_file(bs,ft);
+end;
+pragma Warnings (On, "formal parameter ""prm"" is not referenced");
+
+
+procedure push_data(bs : in out BitStream; prm : Integer)
+is
+begin
+    null;
+end;
+
+
+procedure decode_with_streaming_mode(decodedPDU : out  A1; Filename : in String; result      : out adaasn1rtl.ASN1_RESULT) is
+
+    stream      : adaasn1rtl.encoding.Bitstream := adaasn1rtl.encoding.BitStream_init(1024);
+
+begin
+    Seq_IO.Open(ft,Seq_IO.In_File,Filename);
+    read_from_file(stream,ft);
+--    TASTE_Dataview.A1_Decode(decodedPDU, stream, result);
+    TASTE_Dataview.A1_Decode_aux(decodedPDU, Stream, result);
+
+    if result.Success then
+      Put_Line ("Suscess: Decoding OK !!!");
+    else
+      Put_Line ("Error: Decoding failed !!!");
+    end if;
+
+end;
+
+
+procedure streaming_mode_test
+is
+ encodedPDU :  A1;
+ decodedPDU :  A1;
+ success : boolean;
+ result      : adaasn1rtl.ASN1_RESULT;
+begin
+   initialize(encodedPDU);
+   encode_no_streaming_mode(encodedPDU, "foo3.bin", success);
+   if success then
+
+       decode_with_streaming_mode(decodedPDU, "foo3.bin", result);
+       if result.Success then
+            result := TASTE_Dataview.A1_IsConstraintValid(decodedPDU);
+            if result.Success then
+                   result.Success := TASTE_Dataview.A1_Equal(encodedPDU, decodedPDU);
+                   if result.Success then
+                        Put_Line ("Suscess !!!");
+                   else
+                        Put_Line ("Error encodedPDU <> decodedPDU");
+                   end if;
+            end if;
+
+       end if;
+   end if;
+
+end streaming_mode_test;
+
+
+end user_code;