VeriFastでFreeRTOSに注釈を付ける
= VeriFastでFreeRTOSに注釈を付ける | |
[2018-06-01 09:59] | |
<<<VeriFast | |
<<<FreeRTOS | |
<<<C99 | |
eldeshさんのアドバイスに従ってもっとも小さい実例からはじめよう。 | |
https://github.com/metasepi/amazon-freertos | |
== 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; | |
} | |
``` | |
そもそもmallocはsize_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 ) | |
``` | |
b487749b8c8f83f97152224609df8d41a54b86c2 でpxReadyTasksListsを関数で使えるようになったが、"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_cps0はCPSで式を評価しているっぽい。 | |
* 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