转发导致堆栈溢出

Question

我试图证明在排序列表中插入值的实现的正确性。我已经证明了与在排序列表中插入值相关的有用引理，现在我正在继续使用“funspec”。

该函数的C代码：

void EnqueueLink(unsigned int *list, unsigned int id, unsigned int prio)
{
    unsigned int qAct = list[0];
    unsigned int lAct = 0;

    while ( (qAct != 0) && (FindPrio(qAct) >= prio) )
    {
        lAct = qAct;
        qAct = list[qAct];
    }

    /* Now we insert tAct between lAct and qAct and recompute the queue head.
    */
    list[lAct] = id;
    list[id] = qAct;
    OS_GetData()->listQueueHead = OS_GetPtrs(list[0]); // returns pointers
}

在不损失代码语义的情况下进行一些解释：函数

EnqueueLink

有 3 个参数。第一个参数是一个（排序的）列表，第二个参数是一些“id”，我们要根据其“优先级”对其进行排序。 while 循环解析列表，直到找到正确的位置 (lAct)。

我已经定义了这段代码的“funspecs”：

Definition enqueue_spec : ident * funspec :=
DECLARE _EnqueueLink
WITH list : val, id: Z, prio: Z, sh : share, tasks : list Z
 PRE [ tptr tuint, tuint, tuint ]
  PROP  (writable_share sh; 0 <= prio <= Int.max_unsigned;
         Forall (fun x => 0 <= x <= Int.max_unsigned) tasks; LocallySorted Z.ge tasks)
  PARAMS (list; Vint(Int.repr id); Vint (Int.repr prio))
  SEP   (data_at sh (tarray tuint Int.max_unsigned) (map Vint (map Int.repr tasks)) taskActivations)
 POST [ tvoid ]
  PROP (LocallySorted Z.ge (insert id tasks)) RETURN ()
  SEP  (data_at sh (tarray tuint Int.max_unsigned) (map Vint (map Int.repr (insert tAct tasks))) taskActivations).

Definition Gprog := [enqueue_spec].

Lemma body_enqueuelink: semax_body Vprog Gprog f_EnqueueLink enqueue_spec.

Proof.

start_function. forward.

Admitted.

body_enqueuelink

中的“前进”策略会导致堆栈溢出（双关语）。

规范说明：我试图证明给定一个排序列表（比如说任务），插入新任务的这个 C 函数会呈现一个添加了新任务的排序列表。

如果能够获得一些关于如何从这里开始的想法，那就太好了。由于我对 VST 还很陌生，因此我们将非常感谢任何验证“funspecs”的帮助。

在数学方面，我证明了使用以下修复点插入元素后，本地排序的列表仍保持本地排序：

Fixpoint insert (x : Z) (l:list Z) : list Z :=
  match l with
  | nil => x :: nil 
  | (h :: t) =>
    match Z_ge_lt_dec x h with
    | right _ => h :: (insert x t)
    | left _ => x :: (h :: t) end
  end.

Answer 1

这是一个非常大的数组，

tarray tuint Int.max_unsigned

。也许您想要一个大小为 N 的数组，其中

0 < N <= Int.max_unsigned

。