Instantly share code, notes, and snippets.

Embed
What would you like to do?
Try to verify FreeRTOS using VeriFast
= VeriFastFreeRTOSに注釈を付ける
[2018-06-01 09:59]
<<<VeriFast
<<<FreeRTOS
<<<C99
eldeshさんのアドバイスに従ってもっとも小さい実例からはじめよう。
== lib/FreeRTOS/tasks.c
list.cはマクロもあって、検証がつらい気がする。
躊躇なく偽のヘッダを使うことを前提にtasks.cを検証してみる。
```
$ vfide -I verifast_inc lib/FreeRTOS/tasks.c
$ verifast -disable_overflow_check -c -I verifast_inc lib/FreeRTOS/tasks.c
```
最初の検査対象の案。有意な例でやる気を上げたい:
```
[592-641]
TaskHandle_t xTaskCreateStatic(
TaskFunction_t pxTaskCode,
const char * const pcName,
const uint32_t ulStackDepth,
void * const pvParameters,
UBaseType_t uxPriority,
StackType_t * const puxStackBuffer,
StaticTask_t * const pxTaskBuffer )
[743-829]
BaseType_t xTaskCreate(
TaskFunction_t pxTaskCode,
const char * const pcName,
const configSTACK_DEPTH_TYPE usStackDepth,
void * const pvParameters,
UBaseType_t uxPriority,
TaskHandle_t * const pxCreatedTask )
```
明示的なキャストがないので、xTaskCreateの方がいいんではないか。
=== xTaskCreate関数を検証する
pvPortMalloc( ( ( ( size_t ) usStackDepth ) * sizeof( StackType_t ) ) ) でエラー。
pvPortMalloc( ( usStackDepth * sizeof( StackType_t ) ) ) は通る。
typedef int size_tしても通る。もちろんverifastのテストに失敗するけど。
どうやら単純にmallocの引数がintで、size_tを引数に取ることが問題らしい。
例えば、以下も同じエラーになる:
```
#include "stddef.h"
#include "stdlib.h"
int main()
//@ requires true;
//@ ensures true;
{
size_t a;
void *p;
p = malloc(a);
return 0;
}
```
そもそもmallocsize_tを引数に取るべきでは?
というか、sizeof()を直接mallocに食わせると正常で、size_t型の変数経由で食わせるとエラーになる:
```
#include "stddef.h"
#include "stdlib.h"
int main()
//@ requires true;
//@ ensures true;
{
size_t a;
int b;
void *p;
a = sizeof(size_t);
// b = sizeof(size_t); // error!
// p = malloc(a); // error!
p = malloc(sizeof(size_t));
return 0;
}
```
なぜmallocの引数はintなのか?size_tであるべきでは?
https://github.com/verifast/verifast/issues/29 で解説されていた。以下の部分でint決め打ちにしている。
```
| WFunCall (l, "malloc", [], [Operation (lmul, Mul, ([e; SizeofExpr (ls, te)] | [SizeofExpr (ls, te); e]))]) ->
if pure then static_error l "Cannot call a non-pure function from a pure context." None;
let elemTp = check_pure_type (pn,ilist) tparams te in
let w = check_expr_t (pn,ilist) tparams tenv e intType in
```
めんどうなので、size_tキャストを削除しよう。コードの安全性が劣化しているけど。。。
ヒープチャンクがリークしている。以下のような述語を定義して関数から返す必要がある:
```
/*@
predicate tskTaskControlBlock(struct tskTaskControlBlock *tcb) =
tcb->pxTopOfStack |-> _
...構造体メンバーをなんとかする...
&*& malloc_block_tskTaskControlBlock(tcb);
@*/
```
その他なんやかんやあって、グローバルの構造体配列にアクセスしたい:
```
PRIVILEGED_DATA static List_t pxReadyTasksLists[ configMAX_PRIORITIES ];
// --snip--
#define prvAddTaskToReadyList( pxTCB ) \
traceMOVED_TASK_TO_READY_STATE( pxTCB ); \
taskRECORD_READY_PRIORITY( ( pxTCB )->uxPriority ); \
vListInsertEnd( &( pxReadyTasksLists[ ( pxTCB )->uxPriority ] ), &( ( pxTCB )->xStateListItem ) ); \
tracePOST_MOVED_TASK_TO_READY_STATE( pxTCB )
```
b487749b8c8f83f97152224609df8d41a54b86c2pxReadyTasksListsを関数で使えるようになったが、"Taking the address of this expression is not supported."が出る。
```
let rec eval_core_cps0 eval_core ev state ass_term read_field env e cont =
(* --snip-- *)
| AddressOf (l, e) ->
begin
match e with
WRead (le, e, fparent, fname, frange, fstatic, fvalue, fghost) ->
(* MS Visual C++ behavior: http://msdn.microsoft.com/en-us/library/hx1b6kkd.aspx (= depends on command-line switches and pragmas) *)
(* GCC documentation is not clear about it. *)
ev state e $. fun state v ->
cont state (field_address l v fparent fname)
| WVar (l, x, GlobalName) ->
let Some (l, tp, symbol, init) = try_assoc x globalmap in cont state symbol
(* The address of a function symbol is commonly used in the
assignment of function pointers. We tread (&function) in the
same way as (function), which is what most compilers do: *)
| WVar (l, x, FuncName) ->
cont state (List.assoc x all_funcnameterms)
| _ -> static_error l "Taking the address of this expression is not supported." None (* <= ココでエラーになる *)
end
```
とりあえず以下でバグ報告した。Bartがんばって。。。
https://github.com/verifast/verifast/issues/146
この例ではWReadArrayというのがマッチするらしい。
```
WReadArray of loc * expr * type_ * expr
```
* loc: ソースコード位置
* expr: (たぶん)配列本体の式
* type: 配列の型
* expr: (たぶん)インデックスの式
xxx WReadArrayの加工例
xxx AddressOfでは何すればいいのか?
eval_core_cps0CPSで式を評価しているっぽい。
* cont state termnode
xxx termnodeはどうやって得ればいいのか?
xxx 結局どうすればいいの?
=== xTaskCreateStatic関数を検証する
`StaticTask_t * const pxTaskBuffer`を`StaticTask_t **pxTaskBuffer`と解釈される。
xxx 直す
=== 内側にvolatile/constした変数
```
PRIVILEGED_DATA TCB_t * volatile pxCurrentTCB = NULL;
```
単純に無視してしまえば良いのでは。どうも外側にvolatileを置くのはすでに対応済み(無視している)。
以下の修正をVeriFastに加えた。
```
and
parse_type_suffix t0 = parser
[< '(l, Kwd "*"); t = parse_type_suffix (PtrTypeExpr (l, t0)) >] -> t
| [< '(l, Kwd "volatile"); t = parse_type_suffix (PtrTypeExpr (l, t0)) >] -> t
| [< '(l, Kwd "const"); t = parse_type_suffix (PtrTypeExpr (l, t0)) >] -> t
| [< '(l, Kwd "["); '(_, Kwd "]"); t = parse_type_suffix (ArrayTypeExpr (l,t0)) >] -> t
| [< >] -> t0
```
=== #if( configINCLUDE_FREERTOS_TASK_C_ADDITIONS_H == 1 ) でエラー
`#if (foo == bar)` に対応していない?
```
#define configINCLUDE_FREERTOS_TASK_C_ADDITIONS_H 0
```
して回避した。
=== `#define portSTACK_GROWTH (-1)`を`#if`の中で使うとパースエラー
以下のpatchをVeriFastにあてた。
```
and
parse_expr_primary = parser
[< '(l, Ident _) >] -> IntLit (l, zero_big_int, false, false, NoLSuffix)
| [< '(l, Int (n, dec, usuffix, lsuffix)) >] -> IntLit (l, n, dec, usuffix, lsuffix)
| [< '(l, Kwd "-"); '(l, Int (n, dec, usuffix, lsuffix)) >] -> IntLit (l, minus_big_int n, dec, usuffix, lsuffix)
```
=== `configLIST_VOLATILE TCB_t *pxNextTCB, *pxFirstTCB;`でエラー
xxx configUSE_TRACE_FACILITYを一旦0にする
== lib/FreeRTOS/list.c
マクロがヘッダにあるから辛いと思ったのだけれど...
* 短かいマクロは使用元で注釈
* 長いマクロは偽のヘッダでinline関数に変換
すれば乗り切れるんじゃないかと思えてきた。
```
$ vfide -I verifast_inc lib/FreeRTOS/list.c
$ verifast -c -I verifast_inc lib/FreeRTOS/list.c
```
constでローカル変数が使えない。以下のpatchならパースだけは通る。
```
--- a/lib/FreeRTOS/list.c
+++ b/lib/FreeRTOS/list.c
@@ -73,7 +73,7 @@ void vListInitialiseItem( ListItem_t * const pxItem )
void vListInsertEnd( List_t * const pxList, ListItem_t * const pxNewListItem )
{
-ListItem_t * const pxIndex = pxList->pxIndex;
+ListItem_t *pxIndex = pxList->pxIndex;
/* Only effective when configASSERT() is also defined, these tests may catch
the list data structures being overwritten in memory. They will not catch
@@ -171,7 +171,7 @@ UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove )
{
/* The list item knows which list it is in. Obtain the list from the list
item. */
-List_t * const pxList = ( List_t * ) pxItemToRemove->pvContainer;
+List_t *pxList = ( List_t * ) pxItemToRemove->pvContainer;
pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious;
pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext;
```
もうパーサ直すのめんどうだし、後の開発のためにもならないし、list.cを上記の通り修正してしまうことにする。
=== vListInitialise関数を検証する
xxx またキャストだ。。。以下で逃げれるんだろうか。。。
```
void *tmp = &( pxList->xListEnd );
pxList->pxIndex = ( ListItem_t * ) tmp;
```
== (偽のヘッダを使わずに) lib/FreeRTOS/list.c
```
$ vfide -D ESP_PLATFORM -D HAVE_CONFIG_H -D __XTENSA__ -D __IEEE_LITTLE_ENDIAN -I /home/kiwamu/src/amazon-freertos/demos/espressif/esp32_devkitc_esp_wrover_kit/common/application_code/espressif_code/freertos/include -I /home/kiwamu/src/amazon-freertos/demos/espressif/esp32_devkitc_esp_wrover_kit/common/config_files -I /home/kiwamu/src/amazon-freertos/lib/include -I /home/kiwamu/src/amazon-freertos/lib/include/private -I /home/kiwamu/src/amazon-freertos/lib/FreeRTOS/portable/ThirdParty/GCC/Xtensa_ESP32/include -I /home/kiwamu/src/amazon-freertos/lib/FreeRTOS-Plus-TCP/include -I /home/kiwamu/src/amazon-freertos/lib/FreeRTOS-Plus-TCP/source/portable/Compiler/GCC -I /home/kiwamu/src/amazon-freertos/lib/third_party/jsmn -I /home/kiwamu/src/amazon-freertos/demos/common/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/app_trace/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/app_update/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/bootloader_support/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/console -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/cxx/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/driver/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/esp32/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/esp_adc_cal/include -I /home/kiwamu/src/amazon-freertos/demos/espressif/esp32_devkitc_esp_wrover_kit/common/application_code/espressif_code/ethernet/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/expat/port/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/expat/include/expat -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/fatfs/src -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/heap/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/log/include -I /home/kiwamu/src/amazon-freertos/demos/espressif/esp32_devkitc_esp_wrover_kit/common/application_code/espressif_code/mbedtls/port/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mbedtls/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/micro-ecc/micro-ecc -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/newlib/platform_include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/newlib/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/nghttp/port/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/nghttp/nghttp2/lib/includes -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/nvs_flash/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/openssl/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/pthread/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/sdmmc/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/soc/esp32/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/soc/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/spi_flash/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/spiffs/include -I /home/kiwamu/src/amazon-freertos/demos/espressif/esp32_devkitc_esp_wrover_kit/common/application_code/espressif_code/tcpip_adapter/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/ulp/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/vfs/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/wear_levelling/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/wpa_supplicant/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/wpa_supplicant/port/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/esp32/include -I /home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/xtensa-debug-module/include -I /home/kiwamu/src/amazon-freertos/demos/espressif/esp32_devkitc_esp_wrover_kit/make/build/include -I lib/FreeRTOS lib/FreeRTOS/list.c
```
でソースコードをごにょっとすればパースできそう。
=== パースを通す
__XTENSA__は-Dオプションで渡しているのにどこで消えてしまうのか?
```
#if (defined(__XTENSA__))
# ifdef __XTENSA_EB__
# define __IEEE_BIG_ENDIAN
# else
# define __IEEE_LITTLE_ENDIAN
# endif
#endif
#ifndef __IEEE_BIG_ENDIAN
#ifndef __IEEE_LITTLE_ENDIAN
#error Endianess not declared!! // <= エラー
#endif /* not __IEEE_LITTLE_ENDIAN */
#endif /* not __IEEE_BIG_ENDIAN */
```
__IEEE_LITTLE_ENDIANは定義されているように見える。
amazon-freertos/demos/espressif/esp32_devkitc_esp_wrover_kit/makeでmake menuconfig; makeしてみると:
```
/home/kiwamu/src/amazon-freertos/lib/third_party/mcu_vendor/espressif/esp-idf/components/newlib/include/machine/ieeefp.h:430:2: error: #error __IEEE_LITTLE_ENDIAN defined!
```
ならば__IEEE_LITTLE_ENDIANを-Dオプションで単純に指定してしまっては?逃げられるところは逃げたい。今のVeriFastは曳光弾じゃなくプロトタイプなんだ。
が、指定しても同じエラーになる。なぜなんだ。。。
あ。-D __IEEE_LITTLE_ENDIANを指定すると以下のエラーが出なくなる:
```
#ifdef __IEEE_BIG_ENDIAN
#error __IEEE_BIG_ENDIAN defined!
#endif
#ifdef __IEEE_LITTLE_ENDIAN
#error __IEEE_LITTLE_ENDIAN defined! // <= このエラーは-D __IEEE_LITTLE_ENDIANを指定しない時だけ発生する
#endif
```
ややこしい、-D __IEEE_LITTLE_ENDIANを指定しない場合にしぼって調査したい。
わかった。単純に#errorがパースエラーになっているだけのようだ。パーサがまだ#errorに対応していないんだと思う。
いや落ち着いて考えるとプリプロセッサが通った後では全ての#errorが消えていないと何の道エラーにしなければならないのでは。
xxx プリプロセッサの挙動の傾向を調べる
xxx lexer.ml#skip_blockを読んでみる
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment