Верно ли, что field_compatible (tarray (tptr tcell) 0) = (tptr tcell)? Правильный ли такой подход к body_incr? - PullRequest
Новая
       83

Верно ли, что field_compatible (tarray (tptr tcell) 0) = (tptr tcell)? Правильный ли такой подход к body_incr?

0 голосов
/ 13 июля 2020

Я почти закончил работу над поддающимся проверке модулем c основ программного обеспечения. Осталось всего два доказательства! https://www.cs.princeton.edu/~appel/vc/vc-0.9.5/Verif_hash.html Этот вопрос относится к окончательному доказательству body_incr.

Я не совсем уверен, правильное ли направление, которое я беру. Я собираюсь вставить доказательство, которое у меня есть, начиная с критической точки, а именно этой строки в коде C: 

_incr_list([((_table -> _buckets) + _b)%expr; (_s)%expr]

Мое доказательство продолжается на этом этапе как таковое 

forward_call (
field_address0 (tarray (tptr tcell) N) [ArraySubsc h] (field_address thashtable [StructField _buckets] table)
, (Znth h (map fst cts)), s, sigma, gv).
simpl.
rewrite isptr_offset_val_zero by auto.
rewrite sem_add_pi_ptr_special.
simpl.
rewrite body_incr_field_address_lemma.
entailer!.
rep_omega.
assumption.
rewrite field_compatible_Tarray_split with (i:=h) in H.
destruct H.
rewrite field_compatible_Tarray_split with (i:=0) in H2.
destruct H2.

Примечание: у меня просто изначально было table вместо более длинной части, но это, похоже, не дало мне информации, необходимой для достижения прогресса в доказательстве, но использование этого, похоже, позволило мне добиться большего прогресса. Я думаю, что, возможно, я использую это доказательство неверным образом ... но я думаю, что я добился достаточного прогресса, чтобы стоить вопроса и, возможно, лучше понять, где я ошибаюсь, и как все эти арифметические указатели c представлен в проверяемом c (я должен признать, что не очень понимаю это). Хотя в некотором смысле последние два приложения field_compatible_Tarray_split похожи на то, что дает нам iter_sepcon_split3 ... 

Espec : OracleKind
table, s : val
sigma : list byte
gv : globals
Delta_specs : PTree.t funspec
cts : list (list (list byte * Z) * val)
h := hashfun sigma mod N : Z
Hmax : list_get sigma (Znth h (map fst cts)) < Int.max_unsigned
Htable : isptr table
H0 : 0 <= h < N
H1 : Zlength cts = N
Frame := ?Frame : list mpred
PNtable : is_pointer_or_null table
PNs : is_pointer_or_null s
H : field_compatible (tarray (tptr tcell) h) []
      (field_address thashtable [StructField _buckets] table)
H2 : field_compatible (tarray (tptr tcell) 0) []
       (field_address0 (tarray (tptr tcell) N) [ArraySubsc h]
          (field_address thashtable [StructField _buckets] table))
H3 : field_compatible (tarray (tptr tcell) (N - h - 0)) []
       (field_address0 (tarray (tptr tcell) (N - h)) [
          ArraySubsc 0]
          (field_address0 (tarray (tptr tcell) N) [
             ArraySubsc h]
             (field_address thashtable [StructField _buckets] table)))

========================= (1 / 8)

field_compatible (tptr tcell) []
  (field_address0 (tarray (tptr tcell) N) [ArraySubsc h]
     (field_address thashtable [StructField _buckets] table))

Ключ, который так заманчиво близок, - это предположение 

H2 : field_compatible (tarray (tptr tcell) 0) []
       (field_address0 (tarray (tptr tcell) N) [ArraySubsc h]
          (field_address thashtable [StructField _buckets] table))

Кажется, что массив без размера должен иметь возможность разворачиваться до элемента. (если я неправильно понял, как работает размер, я могу просто изменить, чтобы использовать (i: = 1) выше).

Но я вроде как попал сюда ... Я пытался выяснить, есть ли это способ рассуждать о том, что «массив ничего не значит просто указатель», но, может быть, это не так? Опять же, я думаю, что ударил свое понимание различий между field_compatible (tarray (tptr tcell) 0), field_compatible (tarray (tptr tcell) 1) и field_compatible (tptr tcell) 0.

Итак, я думаю, есть два вопроса, один большой, один маленький ... большой если это хороший способ доказательства. Если это так, то это утверждение (или что-то в этом роде) верно?

И поскольку в нем говорится, что есть 8 целей, большинство из них - математические, созданные моими приложениями, вот нетривиальные one: 

========================= (7 / 8)

(malloc_token Ews thashtable table *
 (!! field_compatible (tarray (tptr tcell) N) []
       (field_address thashtable [StructField _buckets] table) &&
  (data_at Ews (tarray (tptr tcell) 1) (sublist h (h + 1) (map snd cts))
     (field_address0 (tarray (tptr tcell) N) [ArraySubsc h]
        (field_address thashtable [StructField _buckets] table)) *
   array_with_hole Ews (tptr tcell) h (h + 1) N (map snd cts)
     (field_address thashtable [StructField _buckets] table))) *
 iter_sepcon (uncurry listrep) cts)%logic
|-- (listboxrep (Znth h (map fst cts))
       (field_address0 (tarray (tptr tcell) N) [ArraySubsc h]
          (field_address thashtable [StructField _buckets] table)) *
     fold_right_sepcon Frame)%logic

========================= (8 / 8)

ENTAIL Delta,
PROP ( )
LOCAL (temp _b (Vint (Int.repr h)); temp _table table;
temp _s s; gvars gv)
(SEPx
   (listboxrep (list_incr sigma (Znth h (map fst cts)))
      (field_address0 (tarray (tptr tcell) N) [ArraySubsc h]
         (field_address thashtable [StructField _buckets] table))
    :: cstring Ews sigma s :: mem_mgr gv :: ?Frame))
|-- (PROP ( )
     LOCAL ()
     SEP (hashtable_rep (hashtable_incr sigma (map fst cts)) table;
     cstring Ews sigma s; mem_mgr gv) * stackframe_of f_incr)%logic

Трудно сказать, верны они или нет, но они не выглядят явно неправильными. Второе немного беспокоит, потому что, когда я использовал entailer, у меня получилось stuff here |-- emp b / c hashtable_rep отменено ... но я следую примеру, где мы фактически не устанавливаем никаких инвариантов l oop или еще много чего, поэтому я не думаю, что это должно быть проблемой?

Заранее спасибо

...