VeriFastでFreeRTOSに注釈を付ける

memo.rd

= 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を読んでみる