AVM Verifier to Flash Log, как интерпретировать некоторые вещи?

Question

Верификатор AVM при обнаружении и ошибке записывает во флэш-журнал. В документации говорится, что верификатор посетит "все возможные ветки", где могут пройти прыжки. Однако это все еще довольно запутанно, когда вы пытаетесь проследить результаты. Есть какие-нибудь идеи, как правильно это интерпретировать? Весь поток кажется запутанным.

Например, каковы значения следующих маркировок.

МЕРЖЕ ПЕРВЫЙ

MERGE CURRENT

MERGE TARGET

ПОСЛЕ МЕРЖЕ

Кроме того, существуют машинные инструкции и состояние машины с регистрами, стеком областей действия и стеком операндов. Я понимаю, что когда я вижу инструкцию, а затем измененное состояние, например, PushFalse заставит логическое значение появиться в стеке операндов - (Boolean[B]). Но иногда состояние пишется даже без предшествующей ему инструкции, в сочетании с MERGE FIRST, MERGE CURRENT и т. Д. Что это значит?

Answer 1

К сожалению, это самое полное объяснение, которое я смог там найти.

http://hg.mozilla.org/tamarin-redux/file/3c8d01c7b51a/doc/verifier.txt