Аннотация-Точный анализ поведения объектно- Хороший алгоритм решения систем ограничений также ориентированного кода в изоляции от точек его вы- должен гарантированно останавливаться и выдавать зова может потребовать рассуждений о взаимоотно- корректный ответ, если все типы в системе ограничесшаенпиоядхрообтнкорыитзыучхетниыпонво.мВинраалбьонтаыхеКсеинснтеедмиыитПипиорв- ний относятся к этому сужению. с вариантностью, показана неразрешимость подти- Наконец, во время анализа библиотечной функции в пирования закрытых типов и предложены ограни- изоляции от проекта, ее использующего, может быть чения на систему типов, делающие задачу разреши- известна только часть таблицы классов. К примемой. Открытые типы, тем не менее, остаются неизу- ру, предположим, что класс , как и его поточпернонцыедмуир,ыидлвясезаедщачеинвеыспуощлнеистмвоусетти рсиазсртеемшыаюощгреай- мок и все классы в иерархии между и ничений на открытые типы. В данной работе пред- , не реализуют интерфейс ; представлен алгоритм, сводящий задачу выполнимости положим также, что в известной анализатору части системы ограничений на .NET-типы к задаче вы- таблицы классов не существует типов, наследующих полнимости предложений логики первого порядка. класс и реализующих интерфейс одзИуслсьлтеидроувюанщаиееголозгаивчеерсшкаиеемкоосдтиьриовпкоикапзраинноа,дчлтеожрает- новременно. Рассмотрим теперь систему ограничений к разрешимому фрагменту логики первого порядка. ^ . Очевидно, что несмотря на отсутствие классов-кандидатов на роль в I. Введение известной таблице типов, такая система ограничений При статическом анализе функций, написанных все еще выполнима - достаточно ввести новый тип, на объектно-ориентированных языках программирова- наследующий и реализующий . Пония, нередко возникает необходимость проверки вы- лезной в таком случае может служить возможность полнимости некоторой системы ограничений на типы автоматического конструирования объявлений типови типовые переменные. К примеру, если в некоторой кандидатов на роль : к примеру, верификатор может точке исполнения программы известно, что типовая использовать такие объявления для автоматической гепеременная - подтип класса , а тип - брат в нерации исполняемого файла, воспроизводящего ошииерархии наследования, анализатор может определить бочную трассу в библиотеке. Тем не менее, при добавнедостижимость из нее веток, защищенных условием лении ограничения , система становится ; для этого достаточно обнаружить противоре- противоречивой, но единственный способ доказать это чивость системы ограничений ^ . - перебрать все базовые классы класса . Для современных объектно-ориентированных язы- Необходимость учета всех подобных деталей вместе ков (таких как C# и Java) задача определения вы- со сложностью системы типов анализируемого языка полнимости системы ограничений на типы является делает задачу анализа ограничений на типы крайне особенно нетривиальной. Во-первых, во время анализа громоздкой и сложной. К тому же удобно было бы больших программ могут возникать объемные системы иметь возможность комбинировать ограничения на тиограничений, являющиеся достаточно хитрой комби- пы с другими условиями (например, арифметическинацией элементарных ограничений и их отрицаний, ми). К счастью, существуют SMT-решатели - инструсоединенных логическими связками. Во-вторых, ситу- менты эффективного поиска моделей формул логики ация довольно сильно усугубляется сложностью самих первого порядка, в которой некоторым символам присистем типов: как известно, в номинальных системах писана особая интерпретация [1, 4]. Современные SMTтипов с вариантностью даже задача определения, яв- решатели поддерживают большое количество теорий, ляется ли один закрытый тип подтипом другого, нераз- включая линейную арифметику, алгебраические типы решима [10], а обобщения в Java тьюринг-полны [7]. данных, неинтерпретируемые функции и т.д. Следует также заметить, что в случае платформы В данной работе представлен алгоритм решения си.NET известно разрешимое сужение системы типов. стем ограничений на типы в платформе .NET. Ал-
горитм кодирует систему ограничений в предложение логики первого порядка и использует SMT-решатель для поиска ее модели. Показано, что для разрешимого фрагмента системы типов .NET алгоритм кодирования всегда останавливается и выдает предложение из разрешимого фрагмента логики первого порядка. Модели, получаемые от SMT-решателя, содержат логическую интерпретацию для отношения подтипирования и могут быть использованы для конструирования объявлений типов, явно не присутствующих в части таблицы классов, отправленной в решатель. Насколько известно авторам, это первая работа, обсуждающая применение SMT-решателей для анализа системы типов объектноориентированного языка во всей ее полноте. Несмотря на заточенность данной работы под систему типов .NET, подход может быть адаптирован для других объектно-ориентированных языков со сложной системой типов (таких как Java и Scala).
II. Обзор существующих работ Существует большое количество работ, посвященных статическому анализу различных систем типов. Среди них есть и такие, в которых анализ осуществляется путём кодирования типов в формулы языка логики первого порядка и анализа их выполнимости при помощи SMT-решателей [2, 3, 6, 8, 11, 12, 15, 16].
Например, в работе [11] подробно описывается кодирование инвариантных обобщенных типов в логику первого порядка с использованием логического представления алгебраических типов данных. Но в ней никак не затрагивается кодирование отношения подтипирования. Напротив, в работе [16] предложен способ аксиоматизации логики первого порядка с номинальной типизацией, в которой есть аналоги типовых операторов (is, as, оператор преобразования типа). Однако её недостаточно, чтобы закодировать систему типов .NET с её структурными элементами.
Важной вехой является статья Кеннеди и Пирса, которая исследует подтипирование в номинальных системах типов с вариантностью и систему типов .NET в частности [10]. В работе показано, что отношение подтипирования в таких системах неразрешимо даже для закрытых типов и предъявлены несколько разрешимых фрагментов. Однако задача подтипирования для открытых типов является более общей, и к ней нельзя напрямую применить подход, описанный в [10].
III. Система типов .NET1 В своей основе система типов .NET является номинальной (см. ниже), однако в ней имеются и элементы структурной системы типов: к примеру, обобщения интерфейсов и делегатов могут явно определять вариантность своих типовых параметров, а массивы ковариантны по типу своего элемента.
Типы (обозначим их как , , и ) можно разделить на два вида: типовые переменные , и и сконструированные типы < >, где — это конструктор типа, а — упорядоченный список аргументов типов. Закрытыми будем называть типы, которые в листьях дерева конструкторов не содержат типовые переменные. Открытыми назовём все типы, которые не являются закрытыми. Высотой типа будем называть высоту дерева его конструкторов. Обозначим высоту функцией ℎ .
В рамках данной работы можно считать, что все типы являются подтипами System.Object: типы указателей здесь рассматриваться не будут из-за тривиальности их подтипирования.
Номинальность системы типов означает, что отношение подтипирования явно определяется в коде программы и может быть представлено в виде конечной таблицы классов. Каждая запись в таблице классов для системы типов .NET имеет следующий вид: ˚< > ă:: 1, . . . , Для каждого типового параметра имеется запись, которая ограничивает его: # ˚ ă: 1, . . . , (1) Без потери общности можно считать, что в таблице классов нет двух типовых переменных с одним названием (иначе переименуем их).
Левая часть каждой записи в таблице классов содержит аннотацию типа, помещаемую вместо *. Аннотация указывает, является ли тип интерфейсом (в таком случае будет записана буква ), типом значения ( ), ссылочным типом ( ), классом, массивом или делегатом ( ), запечатанным типом (аннотация взята в квадратную рамку, например, ) и имеется ли у типа конструктор без аргументов (в таком случае около буквы записана пара скобок).
Например, для System.Object, System.IComparable и структуры S (не реализующей ни одного интерфейса), записи будут выглядеть следующим образом:
ă::
S ()
ă:: System.ValueType Символ ă:: обозначает отношение номинального подтипирования. Доопределим также < > ă:: r { s . Через ă::` обозначим его транзитивное замыкание. Отношение ă::` отражает номинальность системы типов, но его не достаточно, чтобы выразить структурные элементы. Для отражения вариантности, потребуем от записей таблицы классов иметь вид ˚< 1 1, . . . , > ă:: 1, . . . , , ˝ (инвариантность), ` (ковариантность), ´ (контравариантность). Положим # d“ef и носительно вариантности: например, запрещено < ´ > < ` > ă:: . . . ă:: < > 3) запечатанному типу (в т.ч. делегату или массиву) разрешено появляться в правой части записи только в качестве типового аргумента; 4) в правой части любой записи может стоять максимум один тип с аннотацией (множественное наследование запрещено); 5) аннотации не должны противоречить естественным ограничениям .NET (интерфейс не может быть запечатанным или иметь конструктор без аргументов, типы значений обязательно запечатаны и имеют конструктор без аргументов и т.д.). Определение 1. Расширением таблицы классов называется таблица классов, в которой содержатся все записи из
, а все левые части прочих записей содержат лишь конструкторы и их типовые переменные, не входящие ни в одну из левых частей .
Наконец, можно определить отношение подтипирования с учетом вариантности. Определение 2. Отношение подтипирования для закрытых типов ă: задается следующими правилами: (Super) (Var) for each
ă: p # q < > ă: < > < > ă::
r { s ă: < > < > ă: < > ă: ă:` ă:˝ ă: ă:´ ‰ Предложение 1. Отношение подтипирования ă: разрешимо для закрытых типов, при условии, что таблица классов будет нерасширяющийся.
За определением нерасширяемости таблицы классов и доказательством Предложения 1 читатель отсылается к работе [10]. Из этого следует разрешимость подтипирования для закрытых типов .NET, т.к. по спецификации любая расширяемая таблица классов отклоняется средой выполнения [5].
Другими словами, работа [10] доказывает существование алгоритма, принимающего на вход любую таблицу классов (прошедшую валидацию среды выполнения .NET) и утверждение вида ă: , где и — закрытые типы. Данная работа решает аналогичную задачу, но для открытых типов.
ă:
ă: Очевидно, вопрос в случае открытых типов сам по себе не имеет смысла: уже для двух типовых переменных на вопрос можно дать как утвердительный, так и отрицательный ответ; такая постановка имеет смысл лишь при связывании типовых переменных кванторами. Естественной, поэтому, будет формулировка задачи в терминах логики первого порядка. where Y: Rec<X> {}
Rec pq<Z> Z X Y ă:: ă:: System.Object ă: System.Object ă: Rec<Y> ă: Rec<X>
Наложим ограничения на таблицу классов: 1) отношение ă::` должно быть ацикличным;
IV. Алгоритм На протяжении всей главы предполагается, что имеется и зафиксирована таблица классов “ q будут записываться как ă: и ‰ . щей задачи. По натуральному числу ℎ и данной формуле P L без кванторов необходимо построить такую модель M “ pD , q, что M ( Dp q, либо доказать, что такой модели не существует. Однако на M должен накладываться набор ограничений; Данная глава описывает алгоритм решения следую- A. Язык L формирование ограничений на конструкторы без параметров, (8) формирование ограничений на типовые параметры и (9) формирование окончательной формулы. Шаг 2 предполагает наличие предиката-оракула
, который для пары замкнутых типов определяет, является ли первый подтипом второго, используя таблицу классов
Далее будет дано общее описание языка L и детальное описание каждого шага алгоритма, проанализирована разрешимость выполнимости формул языка L , выдаваемых алгоритмом, а также представлен способ преобразования модели M
обратно в модель M . Доказательство корректности сведения, хоть и представляет интерес, опущено из-за недостатка места.
Язык L описывается сигнатурой pH, P q, где P “ tă:, , , , ℎ и ℎ — двухместные предикатные символы, а
— одноместные. За V обозначим счетное множество предметных переменных, в идентификаторах u. Здесь ă:, Пример 4. Рассмотрим системы ограничений (форму- замыкание конечного множества типов конечно.
IBox<Thing> (невыполнимо из-за за- п.(c) Определения 3). Обозначим за , p q замыкание множество, содержащее . Определение 3. Множество типов
будем называть замкнутым относительно декомпозиции, наследования и ограничений (далее просто замкнутым), если 1, . . . , (a) < > P
P
ñ @, P , где ñ
P , (b)
P ^
ă:: — элементы правой части в записи таблицы классов ă: 1, . . . , . Замыканием множества
(обозначается p q) будем называть минимальное замкнутое Теорема 1. Для нерасширяющийся таблицы классов Доказательство. В доказательстве Теоремы 9 в работе [10] показан аналогичный факт для замыкания относительно декомпозиции и наследования (т.е. без учета относительно декомпозиции и наследования.
Пусть теперь дано конечное множество . Заметим, двух шагов до достижения неподвижной точки: что взятие замыкания p q аналогично выполнению 2) вычисление нового 1) вычисление 1 “ , p q; ство всех элементов всех правых частей записей таблицы классов вида ă: 1, . . . , , где
P 1. Итак, если
— конечное множество, то 1 — также конечное множество, что влечет конечность нового “ 1 Y , где — множества замкнутых типов; вать замкнутый тип < >; ‚ pă:q Ď D ˆ D
— отношение подтипирования из Определения 2, заданное некоторым расширением таблицы классов
, а Dp q — экзистенциальное где 1, . . . ,
— свободные переменные в ); замыкание формулы (т.е. формула D 1, . . . , . , ‚ — оценка переменных p q и P max ℎ p p qq
p q ď ℎ ‚ семантика равенства стандартна. лы ) для таблиц классов из примеров 1—3: 1) X ă: IBuilder<Symbol> ^ X ă: Line ^ Line ă: Y
(выполнимо, если X — новый тип, а Y — Line) 2) Thing
ă: цикливания правил вывода) новые типы) 3) X ă: Y ^ Y ă: X (выполнимо, если X и Y— Основным препятствием для применения решателей логики первого порядка к данной задаче является наличие ограничения (и притом нетривиального) на искомую модель. Алгоритм решает эту проблему, переводя формулу на другой язык первого порядка L , для которого уже может быть применен решатель. Перевод осуществляется в несколько шагов: (1) за‚ носитель D
должен быть подмножеством множе- которых разрешим использовать «<» и «>». ‚ для каждого
P F , p qp q должен конструиро- B. Замыкание множества типов мыкание множества типов, (2) расширение отношения множества (к 1 добавляется конечное множество подтипирования, (3) формирование аксиом частичнозаписей , т.к. количество типовых переменных в 1 го порядка, (4) запрет множественного наследования, конечно). Наконец, заметим, что каждая итерация ал(5) формирование ограничений на запечатанные типы, горитма добавляет к лишь типовые переменные, (6) формирование ограничений на ссылочность, (7) явно содержащиеся в таблице классов. Но т.к. таблица извольное инъективное отображение Обозначим за объединение множеств 1 и
. Так как множество
будет конечным, по Теореме 1 его замыкание p q также будет конечным. Выберем про
: p q Ñ Обозначим за образ p p qq. Очевидно,
задает взаимно-однозначное соответствие между p q и
V .
p q истинен, если “ и ´1p q является применением какого-либо функционального символа в L , и ложен в ином случае2: p q d“ef ł “ p q q — функция, возвращающая множе
p, q d“ef < >( “1, где все типовые переменные различны; pℎ, q —
функция, возвращающая максимальное число раз, которое можно использовать один и тот же конструктор арности
из множества
для построения типа высоты ℎ : pℎ, q “
$ def & % ℎ ´´11 , ℎ 0, ℎ “ 1 и ‰ 0 1, ℎ “ 1 и “ 0 Теперь можно определить функцию зультат её применения к выходным данным и реи ℎ : классов конечна, количество итераций также конечно, Пример 5. Для примера 4.1 и ℎ = 1, p, ℎ q “ def Ť P d“ef
p, p, ℎ q pℎ, qq где ,
определяется одним из четырех способов. ‚ Если и A, и B — закрытые типы, то решение об их подтипировании принимает оракул
:
“ tX, Y, Line, IBuilder<Symbol>, Lineu p q “ tX, Y, Line, IBuilder<Symbol>,
IBuilder<X>, IBuilder<Y>, System.Objectu p q “ p “ Lineq _ p “ Symbolq_ p “ IComponentq _ p “ IBuilder<Symbol>q_ p “ IBuilder<Line>q _ p “ IBuilder<X>q_ p “ IBuilder<Y>q _ p “ System.Objectq Для примера 4.2 и h = 2,
“ tThing, IBox<Thing>, IBox<Z>u p q “ tThing, IBox<Thing>, IBox<Z>,
p q “ p “ Thingq _ p “ IBox<IBox<Thing>>q_ p “ IBox<Thing>q _ p “ IBox<Z>q_ p “ System.Objectq C. Расширение отношение подтипирования После построения замыкания множества типов p q и сопоставления им переменных алгоритм распространяет отношение подтипирования на пары типов в p q, вводя предикат p, d“ef ľ , , qP p qˆ p q, ı отображает применение правила Var. , случае является конъюнкцией формул (2) и (3). Пример 7. Для примера 4.1,
IBuilder<X> ă: IBuilder<Y> ô X ă: Y В процессе применения правил вывода может произойти зацикливание (occurs check ). В тексте спецификации CLI [5] отсутствует явное указание на в разделе I.8.7.1 сказано, что отношение подтиповедение среды в ситуации occurs check, однако или ).
Множественное наследование в .NET разрешено только для интерфейсов. Если какой-то тип является подтипом не-интерфейса, то он не является интерфейсом, c одним исключением: тип System.Object является классом, но также является подтипом для интерфейсов. Для отражения этих свойств используются предикатные символы символ и
. Предикатный истинен для всех интерфейсов (т.е. типов, аннотированых в
буквой ) и ложен для неинтерфейсов (т.е. типов, аннотированых в буквой
(в противном случае, решатель запрета наследования запечатанного типа: пирования есть наименьшее отношение, замкнутое относительно набора некоторых правил. Из этого следует, что ситуация occurs check отвергает подтипирование одного типа другим. Итак, в случае зацикливания вывода добавляется правило
ă: q^ ă: ^ ă: ñ “ q^ ă: ^ ă: ñ ă: q d“ef
“ def ľ p
q, аннотирован « » аннотирован «q,» или « »
P p p ă: ô ^ p@, , . p, q _ p qq
p, q ^ p, qq^
p q ñ p q ^
p, qqq^ p q ^ ă: ^ ‰ System.Object ñ запеча таqн,ный P p ă: ñ “ _
p q Пример 10. Для примера 4.1: ă: Symbol ñ “ Symbol _
p q G. Ссылочные типы и типы значений
Для каждого типового параметра можно указать, будет ли он типом значения или ссылочным типом. Это можно сделать, добавив аннотацию или
соответственно. Наличие такой аннотации в таблице классов гарантирует, что в ней будет запись с конструктором System.ValueType. Эти ограничения будут представлены в виде формулы p q “ ă: pSystem.ValueTypeq^ ‰ pSystem.ValueTypeq def ľ ` p p qq “ ˘ ^
ľ ` p p qq˘ H. Конструкторы без параметров
В некоторых случаях существенны ограничения на переменные вида where X : new(). К примеру, если для такой переменной известно, что < > ă: , а в иерархии < > лишь System.Object имеет конструктор без параметров, можно заключить, что
является типом System.Object. Ограничения на конструктор без параметров кодируются символом ℎ
. “ def ľ ℎ P p q, ничений возможна из-за ограничений на таблицу классов (она должна быть нерасширяемой) и из-за требования на отсутствие кванторов в .
M. Преобразование модели
Пусть Dp q имеет модель M “ pD , q с конечным носителем pD q. Более того, как сказано в конце предыдущей секции, вместе с моделью можно получить оценку : Ñ D
переменных под кванторами существования. Данная секция обсуждает, как перейти от M к модели M “ pD , q формулы Dp q в L . Лемма 1. Если для некоторого P D , p < >q P и ´1pt uq и p < >q P p p qq “ p p qq.
´1pt uq, то конструкторы вил (2) и (3) к условиям леммы. тогда p p < >qq ‰
p p q Лемма 2. Если существуют сконструированный тип < > и тип такие, что D.
p p qq “ p p q, Утверждение Леммы 2 можно вывести из набора аксиом 4. отображения : D
носителя M Лемма 1 и Лемма 2 дают способ конструирования
Ñ D , сопоставляющее элементы замкнутым типам. Возьмем отображение ℎ : D
Ñ D , сопоставляющее элементу из D
произвольный нульарный (и потому замкнутый) конструктор типа, отсутствующий в таблице классов . Обозначим за
p q множество свободных типовых переменных . Теперь можно индуктивно определить отображение .
p q “ def " ℎ < p q>, если p < >q P ´1pt uq p q, если ´1` ´1pt uq ˘
Ď p q По Лемме 1 отображение определено корректно, а по лемме 2 является определенным на всём D .
Отображение ˝ ˝ является оценкой на
p q. Модель же M целиком определяется расширением табdef ľ ` p q ă: p 1q˘ ^ . . . ^ ` p q ă: p q˘ “ J. Запрет бесконечных типов
Так как в системе типов .NET у всех типов конечная высота, а текущие аксиомы не запрещают иметь бесконечную высоту, надо явно указать это свойство: def Ź @. “ < >P p q def . p, p < >qq ô Ž “ p q _ p,
p заменой каждого атома ă: Тогда результатом является
“ K. Формирование окончательной формулы
Наконец, алгоритм создает окончательную кодировку в L . Пусть — формула, полученная из
на атом p q ă“: p q. d“ef ^ L. Разрешимость ^ ^ ^ ^ ^
^ ^ Полученный список формул принадлежит разрешимому фрагменту логики первого порядка, который называется efectively propositional logic
(EPR) [14]. Алгоритм эффективного решения EPR с равенством, использующий подстановочные множества, реализован, к примеру, в SMT-решателе Z3 [13]. нее есть модель с конечным носителем. Другое важное замечание состоит в том, что алгоритмы решения EPR первым шагом обычно сколемизируют переменные под кванторами существования в функциональные Важно, что если у EPR-формулы есть модель, то у ния для элементов , транзитивное замыкание котоконстанты. Таким образом, в случае выполнимости классов 1 получается из добавлением записи формулы , от решателя можно получить оценку пе- ℎ ременных под кванторами существования. 1 , . . . , — элементы множества . Аннотации для
p q ˚ ă:: p 1 q, . . . , p q для каждого P . Здесь t u “0 Ă L 8
утверждения ℎ L . претаций одноместных предикатных символов языка
p q определяются очевидным образом из интерТеорема 2. D ℎ P N и семейство формул в пренексной нормальной форме без кванторов существования
таких, что выполняются следующие имеет модель менных имеет модель p q и P
SMT-based Static Type Inference for Python 3. 2017. [9] J van Leeuwen JA La Poutr´e. «Maintenance of transitive closures and
transitive reductions of graphs». В: International
Workshop on
GraphTheoretic Concepts in Computer Science. Springer. an SMT solver». В: ACM Sigplan Notices. Т. 45. 9. from its call points may require reasoning about the ACM. 2010, с. 105—116. [3] Daniel de
Carvalho и др. «Jolie Static
Type Checker: a prototype». В: Моделирование и анализ информационных систем 24.6 (2017), с. 704—717. [4] Leonardo De Moura и Nikolaj Bjørner. «Z3: An eficient SMT solver». В:
International conference on Tools and Algorithms for the Construction and
Analysis of Systems. Springer. 2008, с. 337—340. [5] TC39 Ecma. TG3. Common Language Infrastructure
(CLI). Standard ECMA-335, June 2005. [6] Nils Gesbert, Pierre Genev`es и Nabil Laya¨ıda. «A logical approach to deciding semantic subtyping». В: ACM Transactions on Programming Languages and Systems (TOPLAS) 38.1 (2015), с. 3. [7] Radu Grigore. «Java generics are turing complete».
В: ACM SIGPLAN Notices. Т. 52. 1. ACM. 2017, с. 73—85.
relationships of open types. A.Kennedy and
B.Pierce extensively studied nominal type systems with variance, showed undecidability of subtyping relation
between ground types and proposed the decidable fragments of the type system. Open types, however, remain unexplored, and still there is no decision procedure for the problem of satisfiability of constraints on the open types. In this paper we present an algorithm
that reduces the problem of satisfiability of the constraints on the system of .NET-types to a satisfiability problem in first-order logic. Termination is investigated and the resulting logical encodings are shown to belong to a decidable fragment of the first-order logic.