AVM Verifier к Flash Log, как интерпретировать некоторые вещи? - PullRequest
3 голосов
/ 13 апреля 2011

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

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

MERGE FIRST

MERGE CURRENT

MERGE TARGET

ПОСЛЕ МЕРЖЕ

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

1 Ответ

0 голосов
/ 06 ноября 2011

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

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

...