Disable SPARK for Copy_DMA_[In|Out] body
[libxhcidbg.git] / src / hw-dbc-transfers.adb
1 --
2 -- Copyright (C) 2016-2017 secunet Security Networks AG
3 --
4 -- This program is free software; you can redistribute it and/or modify
5 -- it under the terms of the GNU General Public License as published by
6 -- the Free Software Foundation; either version 2 of the License, or
7 -- (at your option) any later version.
8 --
9 -- This program is distributed in the hope that it will be useful,
10 -- but WITHOUT ANY WARRANTY; without even the implied warranty of
11 -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12 -- GNU General Public License for more details.
13 --
14
15 with System;
16
17 with HW.Debug;
18 with HW.DbC.Transfer_Info;
19 with HW.DbC.Transfer_Rings;
20
21 package body HW.DbC.Transfers
22 is
23
24    Debug_TDs : constant Boolean := False;
25
26    Num_Receive_TDs : constant := 2;
27
28    ----------------------------------------------------------------------------
29
30    procedure Start_Bulk (Id : DbC.Transfer_Id; Start_Now : Boolean)
31    is
32       EP : constant Endpoint_Range  := Transfer_Info.Get_Endpoint (Id);
33       Len : constant Natural        := Transfer_Info.Get_Length (Id);
34       Pointer : constant Word64     := Transfer_Info.Physical (Id);
35    begin
36       -- It's just one TRB.
37       Transfer_Rings.Enqueue_Data_TRB
38         (EP                => EP,
39          Data_Length       => Len,
40          Data_Buf          => Pointer,
41          Toggle_CS         => Start_Now);
42
43       if Start_Now then
44          Ring_Doorbell (EP);
45       end if;
46
47       pragma Debug (Debug_TDs, Debug.Put ("TD  started; Length: "));
48       pragma Debug (Debug_TDs, Debug.Put_Int32 (Int32 (Len)));
49       pragma Debug (Debug_TDs, Debug.Put ("; Transfer: "));
50       pragma Debug (Debug_TDs, Debug.Put_Word16 (Word16 (Id)));
51       pragma Debug (Debug_TDs, Debug.Put_Reg64 ("; Pointer", Pointer));
52    end Start_Bulk;
53
54    ----------------------------------------------------------------------------
55
56    procedure Reset (Initial_Reset : Boolean)
57    is
58       Id : Transfer_Id;
59       Ctr : Word64;
60       Success : Boolean;
61    begin
62       Transfer_Rings.Initialize (2);
63       Transfer_Rings.Initialize (3);
64
65       if Initial_Reset then
66          for I in 1 .. Num_Receive_TDs loop
67             Transfer_Info.Start
68               (Endpoint    => 3,
69                Length      => Max_Bulk_Size,
70                Id          => Id,
71                Success     => Success);
72             exit when not Success;
73             Start_Bulk (Id, False);
74          end loop;
75       else
76          Ctr := 0;
77          loop
78             Transfer_Info.Walk_Started (Ctr, Id, Success);
79             exit when not Success;
80             Start_Bulk (Id, False);
81          end loop;
82       end if;
83    end Reset;
84
85    procedure Start
86    is
87    begin
88       for EP in Endpoint_Range loop
89          Transfer_Rings.Toggle_CS (EP);
90          Ring_Doorbell (EP);
91       end loop;
92    end Start;
93
94    ----------------------------------------------------------------------------
95
96    subtype DMA_Range is Natural range 0 .. Max_Bulk_Size - 1;
97    subtype DMA_Buffer is Buffer (DMA_Range);
98
99    procedure Copy_DMA_In
100      (Id       : in     Transfer_Id;
101       Buf      : in out Buffer;
102       Len      : in     Natural;
103       DMA_Off  : in     Natural);
104    procedure Copy_DMA_In
105      (Id       : in     Transfer_Id;
106       Buf      : in out Buffer;
107       Len      : in     Natural;
108       DMA_Off  : in     Natural)
109    with SPARK_Mode => Off
110    is
111       DMA_Buf : DMA_Buffer
112       with Address => System'To_Address (Transfer_Info.Physical (Id));
113       DMA_Len : constant Natural := Natural'Min (Max_Bulk_Size - DMA_Off, Len);
114    begin
115       Buf (Buf'First .. Buf'First + DMA_Len - 1) :=
116          DMA_Buf (DMA_Off .. DMA_Off + DMA_Len - 1);
117    end Copy_DMA_In;
118
119    procedure Copy_DMA_Out
120      (Id       : Transfer_Id;
121       Buf      : Buffer;
122       Off      : Natural;
123       Len      : Natural;
124       DMA_Off  : Natural := 0);
125    procedure Copy_DMA_Out
126      (Id       : Transfer_Id;
127       Buf      : Buffer;
128       Off      : Natural;
129       Len      : Natural;
130       DMA_Off  : Natural := 0)
131    with SPARK_Mode => Off
132    is
133       DMA_Buf : DMA_Buffer
134       with Address => System'To_Address (Transfer_Info.Physical (Id));
135       DMA_Len : constant Natural := Natural'Min (Max_Bulk_Size - DMA_Off, Len);
136    begin
137       DMA_Buf (DMA_Off .. DMA_Off + DMA_Len - 1) :=
138          Buf (Off .. Off + DMA_Len - 1);
139    end Copy_DMA_Out;
140
141    ----------------------------------------------------------------------------
142
143    procedure Receive
144      (Buf : in out Buffer;
145       Len : in out Natural)
146    is
147       Id : Transfer_Id;
148       Ctr : Word64;
149       Success : Boolean;
150    begin
151       Ctr := 0;
152       loop
153          Transfer_Info.Walk_Finished (3, Ctr, Id, Success);
154          exit when
155             not Success or else
156             (Transfer_Info.Get_Status (Id) = DbC.Success or
157              Transfer_Info.Get_Status (Id) = DbC.Data_Residue);
158          Transfer_Info.Restart (Id, Max_Bulk_Size);  -- ignore failed transfers
159          Start_Bulk (Id, True);
160       end loop;
161       if Success then
162          Len := Natural'Min
163            (Len,
164             Transfer_Info.Get_Length (Id) - Transfer_Info.Get_Offset (Id));
165          Copy_DMA_In
166            (Id       => Id,
167             Buf      => Buf,
168             Len      => Len,
169             DMA_Off  => Transfer_Info.Get_Offset (Id));
170          Transfer_Info.Set_Offset (Id, Transfer_Info.Get_Offset (Id) + Len);
171          if Transfer_Info.Get_Offset (Id) = Transfer_Info.Get_Length (Id) then
172             Transfer_Info.Restart (Id, Max_Bulk_Size);
173             Start_Bulk (Id, True);
174          end if;
175       else
176          Len := 0;
177       end if;
178    end Receive;
179
180    ----------------------------------------------------------------------------
181
182    procedure Process_Finished_Sends
183    is
184       Id : Transfer_Id;
185       Ctr : Word64;
186       Success : Boolean;
187    begin
188       Ctr := 0;
189       loop
190          Transfer_Info.Walk_Finished (2, Ctr, Id, Success);
191          exit when not Success;
192          Transfer_Info.Reset (Id);
193       end loop;
194    end Process_Finished_Sends;
195
196    ----------------------------------------------------------------------------
197
198    procedure Send
199      (Buf         : in     Buffer;
200       Len         : in out Natural;
201       Start_Now   : in     Boolean;
202       Success     :    out Boolean)
203    is
204       Id : Transfer_Id;
205       Offset : Natural;
206       Appended : Natural := 0;
207    begin
208       if not Transfer_Rings.Last_Started (2) then
209          Appended := Len;
210          Transfer_Info.Append (2, Appended, Offset, Id);
211          if Appended > 0 then
212             Copy_DMA_Out
213               (Id       => Id,
214                Buf      => Buf,
215                Off      => Buf'First,
216                Len      => Appended,
217                DMA_Off  => Offset);
218             Transfer_Rings.Requeue_Data_TRB
219               (EP       => 2,
220                Length   => Transfer_Info.Get_Length (Id),
221                Buf_Addr => Transfer_Info.Physical (Id));
222          end if;
223       end if;
224       Success := True;
225
226       if Len > Appended then
227          Len := Natural'Min (Len - Appended, Max_Bulk_Size);
228
229          Process_Finished_Sends;
230
231          Transfer_Info.Start
232            (Endpoint    => 2,
233             Length      => Len,
234             Id          => Id,
235             Success     => Success);
236
237          if Success and not Transfer_Rings.Full (2) then
238             Copy_DMA_Out
239               (Id       => Id,
240                Buf      => Buf,
241                Off      => Buf'First + Appended,
242                Len      => Len);
243
244             Start_Bulk (Id, Start_Now);
245          else
246             Success := False;
247          end if;
248
249          if Success then
250             Len := Len + Appended;
251          else
252             Len := Appended;
253          end if;
254       end if;
255    end Send;
256
257 end HW.DbC.Transfers;
258
259 --  vim: set ts=8 sts=3 sw=3 et: