Skip to content

Commit 3776197

Browse files
damakidamaki
committed
Initial commit
0 parents  commit 3776197

8 files changed

+535
-0
lines changed

‎.gitignore

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
obj
2+
lib
3+
alire/build

‎LICENSE

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
Copyright (c) 2020 Daniel King
2+
3+
Permission is hereby granted, free of charge, to any person obtaining a copy of
4+
this software and associated documentation files (the "Software"), to deal in
5+
the Software without restriction, including without limitation the rights to
6+
use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
7+
of the Software, and to permit persons to whom the Software is furnished to do
8+
so, subject to the following conditions:
9+
10+
The above copyright notice and this permission notice shall be included in all
11+
copies or substantial portions of the Software.
12+
13+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
14+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
15+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
16+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
17+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
18+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
19+
SOFTWARE.

‎README.md

+69
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
# Consistent Overhead Byte Stuffing (COBS)
2+
This repository provides an implementation of a COBS[1] encoder and
3+
decoder using the SPARK programming language.
4+
5+
## License
6+
All files are licensed under the MIT license.
7+
8+
## SPARK
9+
The code adopts the silver level of SPARK adoption[2]. At the silver
10+
level the code is formally verified by the SPARK toolset to have
11+
the following properties:
12+
* no reads of uninitialized variables
13+
* no unintended accesses of global data
14+
* absence of run-time errors (AoRTE):
15+
* no integer overflow
16+
* no type range violations
17+
* no divisions by zero
18+
* no out-of-bounds array accesses
19+
* all loops are guaranteed to terminate
20+
21+
## Examples
22+
COBS frames can be encoded and decoded via two subprograms:
23+
`COBS.Encode` and `COBS.Decode`. Here's an example to encode
24+
a byte array using COBS:
25+
26+
```Ada
27+
with Ada.Storage_Elements; use Ada.Storage_Elements;
28+
with COBS;
29+
30+
procedure Example
31+
is
32+
Unencoded : Storage_Array (1 .. 5) := (1, 2, 3, 0, 4);
33+
Encoded : Storage_Array (1 .. 7);
34+
Length : Storage_Count;
35+
begin
36+
COBS.Encode (Unencoded, Encoded, Length);
37+
38+
-- Encoded = (4, 1, 2, 3, 2, 4, 0);
39+
-- Length = 7
40+
end Example;
41+
```
42+
43+
The `COBS` package uses Ada's `System.Storage_Elements.Storage_Array`
44+
for its byte array buffers. If custom byte array types are needed, then
45+
the `Generic_COBS` package can be used to instantiate the encoder/decoder
46+
for custom user-defined types.
47+
48+
```Ada
49+
with Interfaces; use Interfaces;
50+
with Generic_COBS;
51+
52+
package Example
53+
is
54+
type Byte_Array is array (Positive range <>) of Unsigned_8;
55+
56+
type My_COBS is new Generic_COBS (Byte => Unsigned_8,
57+
Index => Positive,
58+
Byte_Count => Positive,
59+
Byte_Array => Byte_Array);
60+
end Example;
61+
```
62+
63+
## References
64+
65+
[1] Consistent Overheady Byte Stuffing
66+
https://en.wikipedia.org/wiki/Consistent_Overhead_Byte_Stuffing
67+
68+
[2] Implementation Guidance for the Adoption of SPARK, Adacore and Thales, 2018/09/07
69+
https://www.adacore.com/books/implementation-guidance-spark

‎alire/cobs.toml

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
["0.0.0"]
2+
origin = "file://.."
3+
[general]
4+
description = "Consistent Overhead Byte Stuffing (COBS) encoder/decoder"
5+
maintainers = [
6+
"damaki.gh@gmail.com",
7+
]
8+
maintainers-logins = [
9+
"damaki",
10+
]
11+

‎cobs.gpr

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
project Cobs is
2+
3+
for Library_Name use "Cobs";
4+
for Source_Dirs use ("src");
5+
for Object_Dir use "obj";
6+
for Library_Dir use "lib";
7+
8+
package Builder is
9+
for Switches ("ada") use ("-j0", "-g");
10+
end Builder;
11+
12+
package Compiler is
13+
for Switches ("ada") use ("-g", "-O2", "-gnatn", "-funroll-loops", "-ffunction-sections", "-fdata-sections", "-fcallgraph-info=su,da", "-gnatp", "-gnatVa", "-gnatwae", "-gnaty3AL6M100OSabcefhiklnoprstux");
14+
end Compiler;
15+
16+
end Cobs;
17+

‎src/cobs.ads

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
-------------------------------------------------------------------------------
2+
-- Copyright (c) 2020 Daniel King
3+
--
4+
-- Permission is hereby granted, free of charge, to any person obtaining a
5+
-- copy of this software and associated documentation files (the "Software"),
6+
-- to deal in the Software without restriction, including without limitation
7+
-- the rights to use, copy, modify, merge, publish, distribute, sublicense,
8+
-- and/or sell copies of the Software, and to permit persons to whom the
9+
-- Software is furnished to do so, subject to the following conditions:
10+
--
11+
-- The above copyright notice and this permission notice shall be included in
12+
-- all copies or substantial portions of the Software.
13+
--
14+
-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15+
-- IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16+
-- FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17+
-- AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18+
-- LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
19+
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
20+
-- DEALINGS IN THE SOFTWARE.
21+
-------------------------------------------------------------------------------
22+
pragma SPARK_Mode (On);
23+
24+
with Generic_COBS;
25+
with System.Storage_Elements;
26+
27+
-- This is an instantiation of the COBS encoder/decoder based on
28+
-- the types defined in System.Storage_Elements.
29+
--
30+
-- This instantiation is only valid for systems that have a
31+
-- 8-bit Storage_Element type.
32+
package COBS is new Generic_COBS
33+
(Byte => System.Storage_Elements.Storage_Element,
34+
Index => System.Storage_Elements.Storage_Offset,
35+
Byte_Count => System.Storage_Elements.Storage_Count,
36+
Byte_Array => System.Storage_Elements.Storage_Array) with Pure;

‎src/generic_cobs.adb

+180
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
-------------------------------------------------------------------------------
2+
-- Copyright (c) 2020 Daniel King
3+
--
4+
-- Permission is hereby granted, free of charge, to any person obtaining a
5+
-- copy of this software and associated documentation files (the "Software"),
6+
-- to deal in the Software without restriction, including without limitation
7+
-- the rights to use, copy, modify, merge, publish, distribute, sublicense,
8+
-- and/or sell copies of the Software, and to permit persons to whom the
9+
-- Software is furnished to do so, subject to the following conditions:
10+
--
11+
-- The above copyright notice and this permission notice shall be included in
12+
-- all copies or substantial portions of the Software.
13+
--
14+
-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15+
-- IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16+
-- FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17+
-- AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18+
-- LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
19+
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
20+
-- DEALINGS IN THE SOFTWARE.
21+
-------------------------------------------------------------------------------
22+
package body Generic_COBS
23+
with Pure, SPARK_Mode => On
24+
is
25+
26+
------------
27+
-- Decode --
28+
------------
29+
30+
procedure Decode (Input : in Byte_Array;
31+
Output : out Byte_Array;
32+
Length : out Byte_Count) is
33+
B : Byte;
34+
Code : Byte := Byte'Last;
35+
Run_Length : Byte_Count := 0;
36+
37+
begin
38+
Length := 0;
39+
40+
for I in 0 .. Index'Base (Input'Length - 1) loop
41+
pragma Loop_Invariant (Length <= Byte_Count (I));
42+
pragma Loop_Invariant (for all J in 0 .. Length - 1 =>
43+
Output (Output'First + Index'Base (J))'Initialized);
44+
45+
B := Input (Input'First + I);
46+
47+
exit when B = Frame_Delimiter;
48+
49+
if Run_Length > 0 then
50+
Output (Output'First + Index'Base (Length)) := B;
51+
Length := Length + 1;
52+
53+
else
54+
if Code /= Byte'Last then
55+
Output (Output'First + Index'Base (Length)) := Frame_Delimiter;
56+
Length := Length + 1;
57+
end if;
58+
59+
Code := B;
60+
Run_Length := Byte_Count (Byte'Pos (B));
61+
62+
exit when B = Frame_Delimiter;
63+
end if;
64+
65+
Run_Length := Run_Length - 1;
66+
end loop;
67+
end Decode;
68+
69+
------------
70+
-- Encode --
71+
------------
72+
73+
procedure Encode (Input : in Byte_Array;
74+
Output : out Byte_Array;
75+
Length : out Byte_Count) is
76+
Block_Length : Positive_Byte_Count;
77+
Offset : Byte_Count;
78+
Remaining : Byte_Count;
79+
80+
Nb_Overhead_Bytes : Positive_Byte_Count with Ghost;
81+
82+
begin
83+
-- Encode first block
84+
Encode_Block (Input, Output, Length);
85+
86+
Offset := Length - 1;
87+
Remaining := Input'Length - (Length - 1);
88+
Nb_Overhead_Bytes := 1;
89+
90+
while Remaining > 0 loop
91+
pragma Loop_Variant (Decreases => Remaining,
92+
Increases => Offset,
93+
Increases => Length,
94+
Increases => Nb_Overhead_Bytes);
95+
pragma Loop_Invariant (Offset + Remaining = Input'Length);
96+
pragma Loop_Invariant (Length = Offset + Nb_Overhead_Bytes);
97+
pragma Loop_Invariant (Nb_Overhead_Bytes < Max_Overhead_Bytes (Offset));
98+
pragma Loop_Invariant (for all I in Output'First ..
99+
Output'First + Index'Base (Length - 1) =>
100+
Output (I)'Initialized);
101+
102+
Encode_Block (Input (Input'First + Index'Base (Offset) .. Input'Last),
103+
Output (Output'First + Index'Base (Length) .. Output'Last),
104+
Block_Length);
105+
106+
Nb_Overhead_Bytes := Nb_Overhead_Bytes + 1;
107+
108+
Length := Length + Block_Length;
109+
Offset := Offset + (Block_Length - 1);
110+
Remaining := Remaining - (Block_Length - 1);
111+
end loop;
112+
113+
Output (Output'First + Index'Base (Length)) := Frame_Delimiter;
114+
115+
Length := Length + 1;
116+
end Encode;
117+
118+
--------------------
119+
-- Encode_Block --
120+
--------------------
121+
122+
procedure Encode_Block (Input : in Byte_Array;
123+
Output : out Byte_Array;
124+
Length : out Byte_Count) is
125+
B : Byte;
126+
127+
Code : Positive_Byte_Count := 1;
128+
-- Keeps track of the length of the current run of non-zero octets.
129+
-- Note that this can be 1 more than Max_Run_Size since this is
130+
-- 1 more than the current run length (it includes the overhead octet
131+
-- in its count).
132+
133+
Code_Pos : Index := Output'First;
134+
-- The position in 'Output' of the previous overhead/zero octet.
135+
-- When a run of up to 254 non-zero octets is completed (and thus the
136+
-- length of the run is now known), then the byte at this position in
137+
-- 'Output' is updated with the run length.
138+
139+
begin
140+
Length := 1; -- Initial overhead octet is appended.
141+
142+
if Input'Length > 0 then
143+
for I in Byte_Count range 0 .. Input'Length - 1 loop
144+
pragma Loop_Invariant (Code <= Maximum_Run_Length + 1);
145+
pragma Loop_Invariant (Code = Length - Byte_Count (Code_Pos - Output'First));
146+
pragma Loop_Invariant (Code_Pos in Output'First ..
147+
Output'First + Index'Base (Length) - 1);
148+
pragma Loop_Invariant (Length = Byte_Count (I + 1));
149+
pragma Loop_Invariant (for all I in Output'First ..
150+
Output'First + Index'Base (Length) - 1 =>
151+
(if I /= Code_Pos then
152+
Output (I)'Initialized));
153+
154+
-- Stop when a complete block is reached.
155+
exit when Code = Maximum_Run_Length + 1;
156+
157+
B := Input (Input'First + Index'Base (I));
158+
if B /= Frame_Delimiter then
159+
-- Copy non-zero byte
160+
161+
Output (Output'First + Index'Base (Length)) := B;
162+
163+
Code := Code + 1;
164+
Length := Length + 1;
165+
166+
else
167+
-- Replace zero byte
168+
169+
Output (Code_Pos) := Byte'Val (Code);
170+
Code_Pos := Output'First + Index'Base (Length);
171+
Length := Length + 1;
172+
Code := 1;
173+
end if;
174+
end loop;
175+
end if;
176+
177+
Output (Code_Pos) := Byte'Val (Code);
178+
end Encode_Block;
179+
180+
end Generic_COBS;

0 commit comments

Comments
 (0)