-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathdfu.c
2498 lines (2249 loc) · 94.7 KB
/
dfu.c
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
/*
*
* Copyright 2018 The wookey project team <[email protected]>
* - Ryad Benadjila
* - Arnauld Michelizza
* - Mathieu Renard
* - Philippe Thierry
* - Philippe Trebuchet
*
* This package is free software; you can redistribute it and/or modify
* it under the terms of the GNU Lesser General Public License as published
* the Free Software Foundation; either version 2.1 of the License, or (at
* ur option) any later version.
*
* This package is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
* PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public License along
* with this package; if not, write to the Free Software Foundation, Inc., 51
* Franklin St, Fifth Floor, Boston, MA 02110-1301 USA
*
*/
#include "autoconf.h"
#include "libc/types.h"
#include "libc/syscall.h"
#include "libc/stdio.h"
#include "libc/sync.h"
#include "libc/nostd.h"
#include "libc/string.h"
#include "libc/queue.h"
#include "api/dfu.h"
#include "dfu_priv.h"
#include "dfu_desc.h"
#include "libc/sanhandlers.h"
#include "dfu_context.h"
#include "libusbctrl.h"
#ifdef __FRAMAC__
#include "framac/entrypoint.h"
#endif
/* This variable are read/write in separated temporal windows, making
* volatile or critical section usage usless
*/
static uint8_t read_firmware_data_cmd = 0;
/********* USB layer handling ***************/
/*
* These locks permit to detect if the below USB stack is ready or hasn't finished
* yet data transmission/reception. These flags are updated by callbacks executed by
* the USB below stack.
* As the USB stack can't hold data while its previous job is not finished, we manage
* the serialisation here
*/
static bool dfu_usb_read_in_progress = false;
static bool dfu_usb_write_in_progress = false;
/* pmo moved at the beginning of file for frama-c */
bool ready_for_data_receive = true;
bool ready_for_data_send = true;
/*@ assigns GHOST_opaque_drv_privates , dfu_usb_write_in_progress;
@ ensures dfu_usb_write_in_progress == \false; */
static inline void dfu_usb_driver_setup_send_zlp(void){
usb_backend_drv_send_zlp(0);
set_bool_with_membarrier(&dfu_usb_write_in_progress, false);
}
#if CONFIG_USR_LIB_DFU_DEBUG
static uint32_t read_cnt = 0;
#endif
/*@
@ requires
\separated(
&GHOST_opaque_libusbdci_privates,
&GHOST_num_ctx,
&dfu_usb_read_in_progress, &dfu_usb_write_in_progress,
&GHOST_opaque_drv_privates
);
@ assigns ready_for_data_receive,GHOST_opaque_drv_privates,
dfu_usb_read_in_progress, dfu_context.data_to_store,
dfu_usb_write_in_progress, dfu_context.block_in_progress,
dfu_context.poll_start, dfu_context.poll_timeout_ms;
*/
void dfu_usb_driver_setup_read(uint8_t *dst, uint32_t size){
#ifdef __FRAMAC__ //pmo to check
/*@ loop assigns ready_for_data_receive, dfu_usb_read_in_progress,
dfu_context.data_to_store; */
while(dfu_usb_read_in_progress == true){
request_data_membarrier();
/* emulate asyncrhonous events */
dfu_data_out_handler(0,0,0);
continue;
}
/*@ loop assigns dfu_usb_write_in_progress, dfu_context.block_in_progress,
dfu_context.poll_start, dfu_context.poll_timeout_ms; */
while(dfu_usb_write_in_progress == true){
request_data_membarrier();
/* emulate asyncrhonous events */
dfu_data_in_handler(0,0,0);
continue;
}
#else
while((dfu_usb_read_in_progress == true) || (dfu_usb_write_in_progress == true)){
request_data_membarrier();
continue;
}
#endif
set_bool_with_membarrier(&dfu_usb_read_in_progress, true);
#if CONFIG_USR_LIB_DFU_DEBUG
log_printf("==> READ %d dfu_usb_driver_setup_read %d\n", read_cnt, size);
set_u32_with_membarrier(&read_cnt, read_cnt + 1);
#endif
/* XXX: replace '0' with ep->ep_id */
usb_backend_drv_set_recv_fifo(dst, size, 0);
usb_backend_drv_activate_endpoint(0, USB_BACKEND_DRV_EP_DIR_OUT);
return;
}
/*@
@ requires \separated(&GHOST_opaque_drv_privates, &dfu_usb_write_in_progress);
@ assigns ready_for_data_receive,GHOST_opaque_drv_privates, dfu_usb_read_in_progress,
dfu_context.data_to_store, dfu_usb_write_in_progress,
dfu_context.block_in_progress, dfu_context.poll_start, dfu_context.poll_timeout_ms; */
static void dfu_usb_driver_stall_out(void){
#ifdef __FRAMAC__ //pmo to check
/*@ loop assigns ready_for_data_receive, dfu_usb_read_in_progress,
dfu_context.data_to_store; */
while(dfu_usb_read_in_progress == true){
request_data_membarrier();
/* emulate asyncrhonous events */
dfu_data_out_handler(0,0,0);
continue;
}
/*@ loop assigns dfu_usb_write_in_progress, dfu_context.block_in_progress,
dfu_context.poll_start, dfu_context.poll_timeout_ms; */
while(dfu_usb_write_in_progress == true){
request_data_membarrier();
/* emulate asyncrhonous events */
dfu_data_in_handler(0,0,0);
continue;
}
#else
while((dfu_usb_read_in_progress == true) || (dfu_usb_write_in_progress == true)){
request_data_membarrier();
continue;
}
#endif
set_bool_with_membarrier(&dfu_usb_write_in_progress, true);
log_printf("==> SEND dfu_usb_driver_stall_out\n");
/* XXX: replace 0 with ep->ep_id */
usb_backend_drv_stall(0, USB_BACKEND_DRV_EP_DIR_OUT);
set_bool_with_membarrier(&dfu_usb_write_in_progress, false);
return;
}
/*@
@ requires \separated(&dfu_usb_write_in_progress, &GHOST_opaque_drv_privates);
@ assigns dfu_usb_write_in_progress, GHOST_opaque_drv_privates;
*/
static void dfu_usb_driver_setup_send_status(int status __attribute__((unused)))
{
/* XXX: change 0 with ep->ep_dir */
dfu_usb_driver_setup_send_zlp();
return;
}
/*@
@ requires \separated(&dfu_usb_write_in_progress, &GHOST_opaque_drv_privates);
@ assigns ready_for_data_receive,GHOST_opaque_drv_privates,
dfu_usb_read_in_progress,
dfu_context.data_to_store, dfu_usb_write_in_progress,
dfu_context.block_in_progress, dfu_context.poll_start,
dfu_context.poll_timeout_ms, GHOST_in_eps[0].state;
*/
// PMO to check j'ai modifie le type d'arguement 1 de void * en uint8_t *
void dfu_usb_driver_setup_send(const uint8_t *src, uint32_t size) {
#ifdef __FRAMAC__ //pmo to check
/*@ loop assigns ready_for_data_receive, dfu_usb_read_in_progress,
dfu_context.data_to_store; */
while(dfu_usb_read_in_progress == true){
request_data_membarrier();
/* emulate asyncrhonous events */
dfu_data_out_handler(0,0,0);
continue;
}
/*@ loop assigns dfu_usb_write_in_progress, dfu_context.block_in_progress,
dfu_context.poll_start, dfu_context.poll_timeout_ms; */
while(dfu_usb_write_in_progress == true){
request_data_membarrier();
/* emulate asyncrhonous events */
dfu_data_in_handler(0,0,0);
continue;
}
#else
while((dfu_usb_read_in_progress == true) || (dfu_usb_write_in_progress == true)){
request_data_membarrier();
continue;
}
#endif
set_bool_with_membarrier(&dfu_usb_write_in_progress, true);
log_printf("==> SEND dfu_usb_driver_setup_send %d\n", size);
/* XXX: replace 0 with ep->ep_id */
usb_backend_drv_send_data((uint8_t *)src, size, 0);
usb_backend_drv_ack(0, USB_BACKEND_DRV_EP_DIR_OUT);
return;
}
/********************************************/
#if CONFIG_USR_LIB_DFU_DEBUG
static const char *request_name[] = {
"USB_RQST_DFU_DETACH",
"USB_RQST_DFU_DNLOAD",
"USB_RQST_DFU_UPLOAD",
"USB_RQST_DFU_GET_STATUS",
"USB_RQST_DFU_CLEAR_STATUS",
"USB_RQST_DFU_GET_STATE",
"USB_RQST_DFU_ABORT"
};
static const char *unknown_request_name = "UKNOWN REQUEST";
static const char *print_request_name(dfu_request_t req){
if(req <= 0x06){
return request_name[req];
}
else{
return unknown_request_name;
}
}
static const char *state_name[] = {
"APPIDLE",
"APPDETACH",
"DFUIDLE",
"DFUDNLOAD_SYNC",
"DFUDNBUSY",
"DFUDNLOAD_IDLE",
"DFUMANIFEST_SYNC",
"DFUMANIFEST",
"DFUMANIFEST_WAIT_RESET",
"DFUUPLOAD_IDLE",
"DFUERROR",
};
static const char *unknown_state_name = "UKNOWN STATE";
static const char *print_state_name(dfu_state_enum_t state){
if(state <= 0x0A){
return state_name[state];
}
else{
return unknown_state_name;
}
}
#endif
/*
* Association between a request and a transition to a next state. This couple
* depend on the current state and is use in the following structure
*/
typedef struct dfu_request_transition {
uint8_t request;
uint8_t target_state;
} dfu_request_transition_t;
/****************************************************************
* DFU state automaton formal definition and associate utility
* functions
***************************************************************/
/*
* all allowed transitions and target states for each current state
* empty fields are set as 0xff/0xff for request/state couple, which is
* an inexistent state and request
*
* This table associate each state of the DFU automaton with up to
* 5 potential allowed transitions/next_state couples. This permit to
* easily detect:
* 1) authorized transitions, based on the current state
* 2) next state, based on the current state and current transition
*
* If the next_state for the current transision is keeped to 0xff, this
* means that the current transition for the current state may lead to
* multiple next state depending on other informations (see the official
* DFU standard 1.1 state automaton (Figure A.1, p.28)). In this case,
* the transition handler has to handle this manually.
*/
static const struct {
dfu_state_enum_t state;
dfu_request_transition_t req_trans[5];
} dfu_automaton[] = {
{ APPIDLE, {
{USB_RQST_DFU_DETACH,APPDETACH},
{USB_RQST_DFU_GET_STATUS,APPIDLE},
{0xff,0xff},
{0xff,0xff},
{0xff,0xff}
}
},
{ APPDETACH, {
{USB_RQST_DFU_GET_STATUS,APPDETACH},
{USB_RQST_DFU_GET_STATUS,APPDETACH},
{0xff,0xff}, /* also detach timeout and USB reset */
{0xff,0xff},
{0xff,0xff}
}
},
{ DFUIDLE, {
{USB_RQST_DFU_DNLOAD,DFUDNLOAD_SYNC},
{USB_RQST_DFU_UPLOAD,DFUUPLOAD_IDLE},
{USB_RQST_DFU_ABORT,DFUIDLE},
{USB_RQST_DFU_GET_STATUS,DFUIDLE},
{USB_RQST_DFU_GET_STATE,DFUIDLE}
}
},
{ DFUDNLOAD_SYNC, {
{USB_RQST_DFU_GET_STATUS,0xff}, /* target state depends on more infos*/
{USB_RQST_DFU_ABORT,DFUIDLE},
{USB_RQST_DFU_GET_STATE,DFUDNLOAD_SYNC},
{0xff,0xff},
{0xff,0xff}
}
},
{ DFUDNBUSY, {
{USB_RQST_DFU_GET_STATUS,0xff},
/* leave only on timeout, although:
* timeout calculation is not accurate enough
* tu avoid potential races with the host during
* which a get_status() is performed just before
* going back to DNLOAD_SYNC state.
* For this particular case, we tolerate a short
* temporal window at the end of the timeout in which
* a get_status event can be received, if the timeout
* is (ms-accurate) reached.
*/
{0xff,0xff},
{0xff,0xff},
{0xff,0xff},
{0xff,0xff}
}
},
{ DFUDNLOAD_IDLE, {
{USB_RQST_DFU_DNLOAD,0xff}, /* target state depends on more infos*/
{USB_RQST_DFU_ABORT,DFUIDLE},
{USB_RQST_DFU_GET_STATUS,DFUDNLOAD_IDLE},
{USB_RQST_DFU_GET_STATE,DFUDNLOAD_IDLE},
{0xff,0xff}
}
},
{ DFUMANIFEST_SYNC, {
{USB_RQST_DFU_GET_STATUS,0xff}, /* target state depends on more infos*/
{USB_RQST_DFU_ABORT,DFUIDLE},
{USB_RQST_DFU_GET_STATE,DFUMANIFEST_SYNC},
{0xff,0xff},
{0xff,0xff}
}
},
{ DFUMANIFEST, {
{0xff,0xff}, /* only poll timeout */
{0xff,0xff},
{0xff,0xff},
{0xff,0xff},
{0xff,0xff}
}
},
{ DFUMANIFEST_WAIT_RESET,{
{0xff,0xff}, /* infinite loop, waiting for USB reset */
{0xff,0xff},
{0xff,0xff},
{0xff,0xff},
{0xff,0xff}
}
},
{ DFUUPLOAD_IDLE, {
{USB_RQST_DFU_UPLOAD,0xff}, /* depends (short frame or not) */
{USB_RQST_DFU_ABORT,DFUIDLE},
{USB_RQST_DFU_GET_STATUS,DFUUPLOAD_IDLE},
{USB_RQST_DFU_GET_STATE,DFUUPLOAD_IDLE},
{0xff,0xff}
}
},
{ DFUERROR, {
{USB_RQST_DFU_CLEAR_STATUS,DFUIDLE},
{USB_RQST_DFU_GET_STATUS,DFUERROR},
{USB_RQST_DFU_GET_STATE,DFUERROR},
{0xff,0xff},
{0xff,0xff}
}
},
};
/**********************************************
* DFU getters and setters
*********************************************/
/*@
@ assigns \nothing;
@ ensures \result == dfu_context.poll_timeout_ms;
*/
#ifndef __FRAMAC__
static
#endif
uint32_t dfu_get_poll_timeout(void){
dfu_context_t * dfu_ctx = dfu_get_context();
return dfu_ctx->poll_timeout_ms;
}
/*@
@ assigns \nothing;
@ ensures \result == dfu_context.state;
*/
#ifndef __FRAMAC__
static inline
#endif
uint8_t dfu_get_state() {
dfu_context_t * dfu_ctx = dfu_get_context();
return dfu_ctx->state;
}
/*@
@ assigns \nothing;
@ ensures \result == dfu_context.status;
*/
#ifndef __FRAMAC__
static inline
#endif
uint8_t dfu_get_status() {
dfu_context_t * dfu_ctx = dfu_get_context();
return dfu_ctx->status;
}
/*@
@ assigns \nothing;
*/
#ifndef __FRAMAC__
static
#endif
uint8_t dfu_get_status_string_id() {
// TODO
return 0;
}
/*@
@ assigns dfu_context.status;
@ ensures dfu_context.status == new_status;
*/
#ifndef __FRAMAC__
static inline
#endif
void dfu_set_status(const dfu_status_enum_t new_status) {
dfu_context_t * dfu_ctx = dfu_get_context();
dfu_ctx->status = new_status;
request_data_membarrier();
}
/*@
@ requires \valid(&dfu_context.state);
@ requires is_valid_dfu_state(new_state);
@ assigns dfu_context.state;
@ behavior pb :
@ assumes new_state >= DFUERROR;
@ ensures dfu_context.state == DFUERROR;
@
@ behavior ok :
@ assumes new_state < DFUERROR;
@ ensures dfu_context.state == new_state;
@
@ complete behaviors;
@ disjoint behaviors;
*/
#ifndef __FRAMAC__
static inline
#endif
void dfu_set_state(const uint8_t new_state)
{
dfu_context_t * dfu_ctx = dfu_get_context();
// CDE : new test to check invalid dfu state
if (new_state >= DFUERROR) {
/* should never happen ! fault protection code */
log_printf("PANIC! this should never happen. goto DFUERROR !");
dfu_ctx->state = DFUERROR;
goto err;
}
log_printf("state: %x => %x\n", dfu_ctx->state, new_state);
dfu_ctx->state = new_state;
err:
request_data_membarrier();
return;
}
/*@
@ assigns dfu_context.poll_timeout_ms,dfu_context.poll_start;
@ ensures dfu_context.poll_timeout_ms == t && dfu_context.poll_start == timestamp;
*/
#ifndef __FRAMAC__
static
#endif
void dfu_set_poll_timeout(uint16_t t, uint64_t timestamp)
{
dfu_context_t * dfu_ctx = dfu_get_context();
uint64_t ms;
uint8_t ret;
log_printf("setting poll_timeout_ms to %d\n", t);
dfu_ctx->poll_timeout_ms = t;
ret = sys_get_systick(&ms, PREC_MILLI);
if (ret != SYS_E_DONE) {
log_printf("Error: unable to get systick value !\n");
}
dfu_ctx->poll_start = timestamp;
request_data_membarrier();
}
/******************************************************
* DFU automaton management function (transition and
* state check)
*****************************************************/
/*!
* \brief return the next automaton state
*
* The next state is returned depending on the current state
* and the current request. In some case, it can be 0xff if multiple
* next states are possible.
*
* \param current_state the current automaton state
* \param request the current transition request
*
* \return the next state, or 0xff
*/
/* @
@ requires APPIDLE <= current_state <= DFUERROR;
@ assigns \nothing;
// TODO: specify function contract
*/
/* CDE function identical as usbctrl_next_state so fcn contract is similar
TODO : ensure \result == 0xff cannot be easily prooved, bacause transition table does not define precisely target_state
*/
/*@
@ requires is_valid_dfu_state(current_state);
@ requires is_valid_dfu_request(request);
@ assigns \nothing ;
@ ensures (\result != 0xff) ==> (\exists integer i; 0 <= i < 5 && dfu_automaton[current_state].req_trans[i].request == request
&& \result == dfu_automaton[current_state].req_trans[i].target_state) ;
@ ensures (\forall integer i; 0 <= i < 5 ==> dfu_automaton[current_state].req_trans[i].request != request) ==> (\result == 0xff) ;
*/
static uint8_t dfu_next_state(dfu_state_enum_t current_state, dfu_request_t request)
{
/*@
@ loop invariant 0 <= i <= 5 ;
@ loop invariant \valid_read(dfu_automaton[current_state].req_trans + (0..(5 -1)));
@ loop invariant (\forall integer prei ; 0 <= prei < i ==> dfu_automaton[current_state].req_trans[prei].request != request) ;
@ loop assigns i ;
@ loop variant 5 -i ;
*/
for (uint8_t i = 0; i < 5; ++i) {
if (dfu_automaton[current_state].req_trans[i].request == request) {
return (dfu_automaton[current_state].req_trans[i].target_state);
}
}
/* fallback, no corresponding request found for this state */
/*@ assert (\forall integer i; 0 <= i < 5 ==> dfu_automaton[current_state].req_trans[i].request != request) ; */
return 0xff;
}
/*!
* \brief Specify if the current request is valid for the current state
*
* See DFU standard 1.1 state automaton (Figure A.1, p.28)
*
* \param current_state the current automaton state
* \param request the current transition request
*
* \return true if the transition request is allowed for this state, or false
*/
// CDE TODO : ensures proove equivalence for \result == \false
/*@
@ requires is_valid_dfu_state(current_state);
@ requires is_valid_dfu_request(request);
@ requires is_valid_dfu_state(dfu_context.state);
@ requires \valid_read(dfu_automaton[current_state].req_trans + (0 .. 4));
@ requires \separated(&GHOST_opaque_libusbdci_privates, &GHOST_num_ctx, (struct __anonstruct_dfu_automaton_83 const *)dfu_automaton + (..),
&num_ctx, &dfu_usb_read_in_progress, &dfu_usb_write_in_progress,
&ready_for_data_receive, &ready_for_data_send, &dfu_context.state );
@ assigns dfu_context.state ;
@ ensures (\exists integer i; 0 <= i < 5 && dfu_automaton[current_state].req_trans[i].request == request) <==> \result == \true;
@ ensures (\forall integer i; 0 <= i < 5 ==> dfu_automaton[current_state].req_trans[i].request != request) <==> (dfu_context.state == DFUERROR && \result == \false) ;
*/
static bool dfu_is_valid_transition(dfu_state_enum_t current_state,
dfu_request_t request)
{
/*@ loop invariant 0 <= i <= 5;
@ loop invariant \valid_read(dfu_automaton[current_state].req_trans + (0 .. 4));
@ loop invariant dfu_context.state == \at(dfu_context.state, Pre) ;
@ loop invariant (\forall integer prei; 0 <= prei < i ==> dfu_automaton[current_state].req_trans[prei].request != request);
@ loop assigns i;
@ loop variant 5-i;
*/
for (uint8_t i = 0; i < 5; ++i) {
if (dfu_automaton[current_state].req_trans[i].request == request) {
/*@ assert dfu_context.state == \at(dfu_context.state, Pre); */
/*@ assert (dfu_automaton[current_state].req_trans[i].request == request);*/
/*@ assert \exists integer k; 0 <= k < 5 && dfu_automaton[current_state].req_trans[k].request == request ; */
return true;
}
}
/*@ assert (\forall integer i; 0 <= i < 5 ==> dfu_automaton[current_state].req_trans[i].request != request) ; */
/*@ assert dfu_context.state == \at(dfu_context.state, Pre); */
/*@ assert dfu_context == \at(dfu_context, Pre); */
/*
* Didn't find any request associated to current state. This is not a
* valid transition. We should fallback to DFUERROR state.
*/
log_printf("invalid transition from state %d, request %d\n", current_state, request);
dfu_set_state(DFUERROR);
/*@ assert dfu_context.state == DFUERROR; */
/* @ assert (\forall integer i; 0 <= i < 5 ==> dfu_automaton[current_state].req_trans[i].request != request) ; */
return false;
}
/*********************************************************************
* Mutexes, protection against race conditions...
********************************************************************/
/*
* \brief entering a critical section
*
* During this critical section, any ISR is postponed to avoid any
* race condition on variables shared in write-access between ISR and
* main thread. See sys_lock() syscall API documentation.
*
* Critical sections must be as short as possible to avoid border
* effects such as latency increase and ISR queue overloading.
*/
/*@
@ assigns \nothing;
*/
static inline void enter_critical_section(void)
{
uint8_t ret;
ret = sys_lock (LOCK_ENTER); /* Enter in critical section */
if(ret != SYS_E_DONE){
log_printf("Error: failed entering critical section!\n");
}
return;
}
/*
* \brief leaving a critical section
*
* Reallow the execution of the previously postponed task ISR.
*/
static inline void leave_critical_section(void)
{
uint8_t ret;
ret = sys_lock (LOCK_EXIT); /* Enter in critical section */
if(ret != SYS_E_DONE){
log_printf("Error: failed leaving critical section!\n");
}
return;
}
/**********************************************
* DFU globals
*********************************************/
typedef struct {
uint16_t id;
uint32_t size;
uint8_t * data;
} dfu_data_block_t;
/**********************************************
* DFU generic utility functions
*********************************************/
/*!
* Preparing the USB stack for stalling. This is requested
* when a local 'block_in_progress' is still executed while
* the host is requesting a status. The IP will then
* automatically send stall events while we finished the
* local treatement (read or write access)
*/
/*@
@ requires \separated(&GHOST_opaque_drv_privates, &dfu_usb_write_in_progress);
@ assigns ready_for_data_receive, GHOST_opaque_drv_privates,
dfu_usb_read_in_progress, dfu_context.data_to_store,
dfu_usb_write_in_progress, dfu_context.block_in_progress,
dfu_context.poll_start, dfu_context.poll_timeout_ms;
@*/
static void dfu_prepare_stall(void)
{
dfu_usb_driver_stall_out();
}
/*
* Manage various DFU errors. This can be:
* - STALLEDPKT (get status while the block_in_progress is not finished)
* - invalid transition request
* - invalid input size (data too big for local buffer)
* etc.
* DFU errors are sent back to the host:
* - for informational purpose
* - to support resiliency (reseting upload/download work...)
*/
/*@
@ requires OK <= new_status <= ERRSTALLEDPKT;
@ assigns ready_for_data_receive, dfu_usb_read_in_progress,
dfu_context.data_to_store, dfu_usb_write_in_progress,
dfu_context.block_in_progress, dfu_context.poll_start,
dfu_context.poll_timeout_ms, GHOST_opaque_drv_privates, dfu_context.status;
@ ensures dfu_context.status == new_status;
*/
static inline void dfu_error(const dfu_status_enum_t new_status)
{
log_printf("%s: status=%d\n", __func__, new_status);
if(new_status == ERRSTALLEDPKT){
log_printf("stalling...\n");
dfu_prepare_stall();
dfu_set_status(new_status);
return;
}
log_printf("state -> Error\n");
dfu_set_status(new_status);
request_data_membarrier();
}
/*@
@ assigns *b;
*/
static void dfu_release_block(dfu_data_block_t *b)
{
enter_critical_section();
if(b != NULL){
if(b->data != NULL){
#ifdef CONFIG_STD_MALLOC_LIGHT
wfree((void**)&b->data);
#endif
}
#ifdef CONFIG_STD_MALLOC_LIGHT
wfree((void**)&b);
#endif
}
/* PTH: value on stack, no impact */
b = NULL;
leave_critical_section();
}
static uint8_t dfu_validate_suffix(dfu_suffix_t * dfu_suffix __attribute__((unused)))
{
// TODO
return 1;
}
static uint8_t dfu_validate_sec_suffix(dfu_sec_metadata_hdr_t * dfu_sec_metadata_hdr __attribute__((unused)))
{
// TODO
return 1;
}
static uint8_t dfu_validate_memory_policy(uint32_t addr __attribute__((unused)),
uint32_t length __attribute__((unused)))
{
// TODO
return 1;
}
/**********************************************
* Storing and loading data handler, mostly dependent on
* user layer callback/
*********************************************/
/*
* The USB content as been read into local buffer and is waiting to be stored
* into the flash. This function does this
*/
/*@
@ behavior not_busy_and_not_load_sync :
@ assumes dfu_context.state != DFUDNBUSY && dfu_context.state != DFUDNLOAD_SYNC;
@ assigns \nothing;
@
@ behavior busy_or_load_sync :
@ assumes !(dfu_context.state != DFUDNBUSY && dfu_context.state != DFUDNLOAD_SYNC);
@ assigns dfu_context.data_out_current_block_nb, dfu_context.data_to_store;
@ ensures dfu_context.data_out_current_block_nb == \old(dfu_context.data_out_current_block_nb)+1 && dfu_context.data_to_store == \false;
@
@ complete behaviors;
@ disjoint behaviors;
@*/
static void dfu_store_data(void)
{
dfu_context_t * dfu_ctx = dfu_get_context();
if (dfu_get_state() != DFUDNBUSY && dfu_get_state() != DFUDNLOAD_SYNC) {
/* should not happend out of these two states. In that very case,
* there is no block in progress as the automaton is not in download
* mode
*/
return;
}
dfu_backend_write(dfu_ctx->data_out_buffer, dfu_ctx->data_out_length, dfu_ctx->data_out_nb_blocks);
// now set the write action as done
dfu_ctx->data_out_current_block_nb += 1;
/* store request sent, no more data to store by now */
dfu_ctx->data_to_store = false;
request_data_membarrier();
return;
}
/*@
@ behavior null_data:
@ assumes dfu_context.data_in_buffer == NULL;
@ assigns \nothing;
@
@ behavior notidle:
@ assumes dfu_context.data_in_buffer != NULL;
@ assumes dfu_context.state != DFUUPLOAD_IDLE;
@ assigns \nothing;
@
@ behavior idle:
@ assumes dfu_context.data_in_buffer != NULL;
@ assumes dfu_context.state == DFUUPLOAD_IDLE;
@ assigns dfu_context.data_in_current_block_nb;
@ ensures dfu_context.data_in_current_block_nb ==\old(dfu_context.data_in_current_block_nb) + 1;
@
@ complete behaviors;
@ disjoint behaviors;
*/
static void dfu_load_data(void)
{
dfu_context_t * dfu_ctx = dfu_get_context();
/* sanitation for buffers */
if (dfu_ctx->data_in_buffer == NULL) {
/* PTH: erroring ? */
goto err;
}
/*@ assert \valid(dfu_ctx->data_in_buffer+(0 .. dfu_ctx->data_in_length-1)); */
/* INFO: size is given by setup packet but the block number is not
* managed by the host, which only manage a file size */
if (dfu_get_state() != DFUUPLOAD_IDLE) {
/* should not happend out of these two states. In that very case,
* there is no block in progress as the automaton is not in download
* mode
*/
goto err;
}
dfu_backend_read(dfu_ctx->data_in_buffer, dfu_ctx->data_in_length);
// now set the write action as done
dfu_ctx->data_in_current_block_nb += 1;
request_data_membarrier();
/* store request sent, no more data to store by now */
err:
return;
}
/*
* This procedure is a *callback*. The DFU stack has no knowledge of
* when the effective storage backend write is finished and request the
* upper layer (the DFU application) to inform it when the write is finished.
*
* This function set the write action as finished and allows the host to
* send the next chunk and permit (if the poll_timeout is 0) to fo back to DNLOAD_SYNC
* or to DNLOAD_IDLE (depending on the current state)
*/
/*@
@ assigns dfu_context.block_in_progress, dfu_context.poll_start, dfu_context.poll_timeout_ms, dfu_context.poll_start;
@ ensures dfu_context.block_in_progress== 0 && dfu_context.poll_start == 0;
*/
void dfu_store_finished(void)
{
log_printf("%s\n", __func__);
dfu_context_t * dfu_ctx = dfu_get_context();
/*
Should be updated by the main loop. If upper layer received async IPC
saying that data has been stored, then update these fields:
*/
dfu_ctx->block_in_progress = 0;
dfu_ctx->poll_start = 0;
request_data_membarrier();
dfu_set_poll_timeout(0, 0);
}
/*
* same principle as for the dfu_store_finished. This permit to inform
* the DFU stack that its buffer has been fullfill with the firware chunk content and
* can now be sent to the host.
*/
/*@
@ behavior Ok:
@ assumes bytes_read < dfu_context.data_in_length;
@ assigns ready_for_data_receive, GHOST_opaque_drv_privates,
dfu_usb_read_in_progress, dfu_context.data_to_store,
dfu_usb_write_in_progress, dfu_context.block_in_progress,
dfu_context.poll_start, dfu_context.poll_timeout_ms,
GHOST_in_eps[0].state, dfu_context.data_in_nb_blocks,
dfu_context.data_in_length, dfu_context.data_in_current_block_nb,
dfu_context.block_in_progress, dfu_context.session_in_progress,
dfu_context.state;
@ ensures dfu_context.state == DFUIDLE;
@
@ behavior ko:
@ assumes bytes_read >= dfu_context.data_in_length;
@ assigns ready_for_data_receive, GHOST_opaque_drv_privates,
dfu_usb_read_in_progress, dfu_context.data_to_store,
dfu_usb_write_in_progress, dfu_context.block_in_progress,
dfu_context.poll_start, dfu_context.poll_timeout_ms,
GHOST_in_eps[0].state;
@ complete behaviors;
@ disjoint behaviors;
@*/
void dfu_load_finished(uint16_t bytes_read)
{
dfu_context_t * dfu_ctx = dfu_get_context();
/* Here we should send the data stored in the buffer by the app into
* the USB IP (upload mode) and then set block_in_progress as false
* INFO:
* The data sent is the number of effective read data, not the requested bytes
* number. This is due to the end of upload mechanism which is based on the
* detection on the received wLength value (from the host). When wLength is
* smaller than the one requested, the host considering that the upload is
* finished. bytes_read here is given by the DFU handling application depending
* on the number of bytes read for this chunk by the storage backend.
*/
/*
* XXX: FIXME: no fragmentation here ! done by libusbctrl !!!
*/
dfu_usb_driver_setup_send(dfu_ctx->data_in_buffer, bytes_read);
if (bytes_read < dfu_ctx->data_in_length) {
if ((bytes_read % 64) == 0) {
/* Inform the host through sending a zlp packet that upload is finished */
dfu_usb_driver_setup_send_zlp();
}
/* End of data read, going back to dfu_idle */
dfu_ctx->data_in_nb_blocks = 0;
dfu_ctx->data_in_length = 0;
dfu_ctx->data_in_current_block_nb = 0;
dfu_ctx->block_in_progress = 0;
dfu_ctx->session_in_progress = 0;
dfu_set_state(DFUIDLE);
request_data_membarrier();
}
}
/**********************************************
* Timeout management for DNBUSY state
*********************************************/
/*
* DNBUSY timeout is not timer-based. At each automaton schedule, we check
* if:
* 1) we are in DNBUSY state
* 2) we spent more time than the configured timeout
* if this is the case, we go back in DNLOAD_BUSY state
*/
// PMO todo with others behaviors
/*@ behavior notdfundbusy:
@ assumes dfu_context.state != DFUDNBUSY ;
@ assigns \nothing;
*/