Не надо тратить годы, уже всё потрачено другими людьми. Тут достаточно одного предиката orient2d. Там же Джонатан Шевчук и сишный код выложил, причём в public domain.
Там разделены авторизация и голосование, используя одно, нельзя проверить другое. Дальше в протоколе гарантируется тайность и полная проверяемость голосования. Полная проверяемость гарантируется при предположении, что регистратор и непосредственно урна не являются нечестными одновременно. Это возможно обеспечить опубликованием списков голосующих.
Я не призываю использовать непосредственно этот протокол, я просто говорю, что математики работают над вопросом, и подвижки очень даже есть.
Ну SSA строить у меня в планах как раз и было, но скажите, пожалуйста, если мы переведём код в SSA, и будем делать анализ IR, то найти всякого в IR можно. Но как сохранить соответствие с исходным кодом? Мы же хотим сигнализировать не просто о проблеме, а о конкретной строчке исходного кода...
Конечно, интересно. Только я в этом не понимаю ничего, никогда не обучался информатике :)
У меня очень примитивный игрушечный язык, поэтому всякие ошибки типа вылезания за границы и вообще арифметики указателей просто нет. А вот всякие if true и использование неинициализированных переменных можно попробвать и половить, опять же, чисто для развлечения и иллюстрации. Для if true, насколько я понимаю, нужно делать flow analysis.
Пока что я встречал такое словосочетание только в примерах оптимизирующих компиляторов, когда мы переводим AST уже в какой-нибудь трёхадресный код. А как это выглядит в случае анализатора?
Вообще у меня в планах было добавить оптимизации ещё...
Любопытная статья! Я, наверное, читаю слишком через строчку, а вы весь код где-то выложили или только на кусочки в статью нарезали? Я вот недавно писал игрушечный компилятор за выходные (тоже два дня :), было бы интересно к нему прикрутить подобный анализатор на пару-тройку правил.
Раздумываю о хорошей иллюстрации для работы парсера. Там кода всего ничего, но иллюстрировать алгоритм динамического программирования не самая очевидная вещь.
Может быть, мы и говорим об одном и том же эффекте, но я настаиваю на том, что о нём нужно говорить правильными словами, иначе мы продолжаем вводить новичков в заблуждение. Ещё раз, UB - свойство всей программы, а не одной инструкции, поэтому ни о каком времени говорить нельзя.
Ну а документация не может быть трактуемой двояко: "результат вычисления 2+2 равен 5 или -3" - это не документация поведения, а мусор.
На этом, пожалуй, я действительно сворачиваю своё участие в ветке. Ссылки на стандарт я привёл, и, хотя он, к сожалению, написан на человеческом (а значит, позволяющем двоякое толкование) языке, нужные ключевые слова содержит. Кому интересно копать, тот докопается до того, что ему нужно.
наличие ub в программе может поменять её поведение, даже до его возникновения.
Вот тут у вас фундаментальная ошибка. UB - не свойство операции, это свойство программы в целом. Некорректно говорить о поведении программы до возникновения UB.
А вот если говорит: «may result in any valid int value, or crash the program», то такая замена всё ещё оправдана.
И тут ошибка. Well-formed и well-defined, никакой двоякости трактования не допускается.
От трейса не зависит, поскольку доказательство ведётся не совсем так. Разумеется, для смелых предположений оптимизатора ему нужен весь контекст целиком. И если кто-то мог скопировать адрес вашей переменной раньше, компилятор смелых предположений делать не будет.
Про экспоненциальное время - не в тему, существующие ныне компиляторы очень сильны в оптимизации, но при этом очень близоруки. Если им не помогать активно, то они ни черта доказать (и как следствие, оптимизировать) не смогут.
Я пытаюсь подкреплять своё понимание ссылками на стандарт, иначе разговор неконструктивен. Если unspecified может себя вести как ни попадя, тогда и impementation-defined должен себя вести так же, см. различие только в требовании стандарта о документации поведения. И при этом мы говорим про well-formed программы.
UB не путешествует во времени. Просто поведение логических выводов компилятора для программы, допускающей UB, может быть неочевидно для программиста. Компилятор исходит из предпосылки, что UB не может происходить. Из этого следуют ограничения на интервалы допустимых переменных. Из этого следует удаление ненужных кусков кода (таких, как if false), а за этим могут быть любые сюрпризы.
Говоря школьным языком, если мы допустим, что пятый постулат нарушается (см. UB), это не означает, что Евклид (или Лобачевский) воскресли. Это просто означает, что при неверности пятого постулата мы попадаем в рамки неевклидовой геометрии.
behavior for which this document imposes no requirements
3.64[defns.unspecified]unspecified behavior
behavior, for a well-formed program ([defns.well.formed]) construct and correct data, that depends on the implementation
Unspecified ситуация всегда одинаково обрабатывается одной и той же версией компилятора. От implementation defined она отличается только необходимостью документации.
Несогласен с первым пунктом, поскольку в таком сценарии вывод компилятора ломается непредсказуемо, что не согласуется с тем, что поведение op1 определено разработчиками компилятора.
UB по переполнению существует по множеству причин, например, чтобы класть 32 битные инты в 64 битные регистры.
Давайте я выражу ту же самую мысль, но чуть-чуть другими словами.
Компилятор - это переводчик с одного языка на другой, например, в случае си - с с си на ассемблер (оптимизация - это тоже часть перевода). Как и в случае с переводом с одного человеческого языка на другой, мы ни в коем случае не хотим, чтобы переводчик порол отсебятину, мы хотим, чтобы перевод точно соответствовал оригиналу.
К счастью, литературные качества нас не интересуют в случае машинных языков, поэтому есть довольно чёткие критерии эквивалентности кусков кода.
Поэтому переводчик обязан убедиться, что A op1 B и A op2 B дают одинаковые результаты для всех допустимых значений A и B.
Если переполнение разрешено стандартом (опять же, в любой форме, будь то unspecified, impelementation defined или standard-defined), то A и B могут быть любыми целыми числами, и в такой ситуации замена A op1 B на A op2 B недопустима, поскольку результаты двух операций будут отличаться на некоторых наборах A и B.
Если же переполнение UB, то компилятор исходит из предпосылки, что A и B таковы, что выражение A op1 B не переполняется, поскольку программист позаботился об этом. И тогда компилятор имеет полное право произвести замену.
Таким образом, механизм UB развязывает руки компилятору, перекладывая часть ответственности (в частности, по работе с большими числами) с компилятора на программиста, и тем самым ускоряя основную массу программ.
Нет, не подойдёт. Код после оптимизации обязан быть эквивалентным исходному коду, и компилятор эту эквивалентность обязан доказать.
Если переполнение разрешено, пусть и в виде implementation defined/unspecified, то замена на неэквивалентную (в случае переполнения) операцию недопустима.
Я не очень улавливаю вашу мысль. Она в том, что я не понимаю разницы между unspecified и undefined или мы уже о чём-то другом? Сформулируйте точно, пожалуйста.
Моё утверждение: введение концепта UB расширяет возможности оптимизатору, в том числе для работы на большем количестве железок.
Пусть у нас есть две операции op1 и op2 над двумя числами A и B. Вот я в коде пишу C = A op1 B. Оптимизатор компилятора хочет заменить эту инструкцию на другую, более дешёвую C = A op2 B. Но предположим, что такая замена эквиалентна только при условии непереполнения A op1 B. Если переполнение undefined, то компилятор имеет право сделать замену, поскольку это забота программиста не допустить UB. Если же переполнение unspecified, то замену делать нельзя.
Так. Давайте по порядку. Unspecified behavior это то же самое, что implementation defined, то есть, оно хорошо определено и работает всегда одинаково, но разработчики компилятора (выделение важно́) не обязаны документировать поведение (в отличие от implementation-defined).
Undefined же не имеет вообще никаких ограничений по поводу того, что случится. И да, в том числе «запустить ядерные ракеты». Для алгебраических упрощений это может быть важным, поскольку компилятор не обязан гарантировать результат работы конкретной машины. То есть, конкретная машина может работать с дополнительным кодом, а может и нет.
Компилятор же исходит из предположения, что программист умный и внимательный, и не допускает появления UB. Что позволяет доказать корректность преобразований его оптимизатора.
Таким образом, я не думаю, что я путаю unspecified и undefined, ваше обоснование меня не убедило.
Не надо тратить годы, уже всё потрачено другими людьми. Тут достаточно одного предиката orient2d. Там же Джонатан Шевчук и сишный код выложил, причём в public domain.
Там разделены авторизация и голосование, используя одно, нельзя проверить другое. Дальше в протоколе гарантируется тайность и полная проверяемость голосования. Полная проверяемость гарантируется при предположении, что регистратор и непосредственно урна не являются нечестными одновременно. Это возможно обеспечить опубликованием списков голосующих.
Я не призываю использовать непосредственно этот протокол, я просто говорю, что математики работают над вопросом, и подвижки очень даже есть.
Ну математики не зря хлеб едят. Вот система, которая позволяет выполнить ваши два требования:
https://www.belenios.org/howitworks.html
Ну SSA строить у меня в планах как раз и было, но скажите, пожалуйста, если мы переведём код в SSA, и будем делать анализ IR, то найти всякого в IR можно. Но как сохранить соответствие с исходным кодом? Мы же хотим сигнализировать не просто о проблеме, а о конкретной строчке исходного кода...
Спрашивать с 500 строк питоновского кода генерировать непосредственно машинный код - это чуть перебор :)
Target language - это GNU ассемблер.
Конечно, интересно. Только я в этом не понимаю ничего, никогда не обучался информатике :)
У меня очень примитивный игрушечный язык, поэтому всякие ошибки типа вылезания за границы и вообще арифметики указателей просто нет. А вот всякие if true и использование неинициализированных переменных можно попробвать и половить, опять же, чисто для развлечения и иллюстрации. Для if true, насколько я понимаю, нужно делать flow analysis.
Пока что я встречал такое словосочетание только в примерах оптимизирующих компиляторов, когда мы переводим AST уже в какой-нибудь трёхадресный код. А как это выглядит в случае анализатора?
Вообще у меня в планах было добавить оптимизации ещё...
Любопытная статья! Я, наверное, читаю слишком через строчку, а вы весь код где-то выложили или только на кусочки в статью нарезали? Я вот недавно писал игрушечный компилятор за выходные (тоже два дня :), было бы интересно к нему прикрутить подобный анализатор на пару-тройку правил.
Раздумываю о хорошей иллюстрации для работы парсера. Там кода всего ничего, но иллюстрировать алгоритм динамического программирования не самая очевидная вещь.
Может быть, мы и говорим об одном и том же эффекте, но я настаиваю на том, что о нём нужно говорить правильными словами, иначе мы продолжаем вводить новичков в заблуждение. Ещё раз, UB - свойство всей программы, а не одной инструкции, поэтому ни о каком времени говорить нельзя.
Ну а документация не может быть трактуемой двояко: "результат вычисления 2+2 равен 5 или -3" - это не документация поведения, а мусор.
На этом, пожалуй, я действительно сворачиваю своё участие в ветке. Ссылки на стандарт я привёл, и, хотя он, к сожалению, написан на человеческом (а значит, позволяющем двоякое толкование) языке, нужные ключевые слова содержит. Кому интересно копать, тот докопается до того, что ему нужно.
и это вы написали в ветке, в которой первая фраза @mayorovp была буквально «потому что без UB невозможна вообще никакая оптимизация» :)
Вот тут у вас фундаментальная ошибка. UB - не свойство операции, это свойство программы в целом. Некорректно говорить о поведении программы до возникновения UB.
И тут ошибка. Well-formed и well-defined, никакой двоякости трактования не допускается.
Я ничего не предлагаю. Я рассказываю, как работают компиляторы сегодня.
От трейса не зависит, поскольку доказательство ведётся не совсем так. Разумеется, для смелых предположений оптимизатора ему нужен весь контекст целиком. И если кто-то мог скопировать адрес вашей переменной раньше, компилятор смелых предположений делать не будет.
Про экспоненциальное время - не в тему, существующие ныне компиляторы очень сильны в оптимизации, но при этом очень близоруки. Если им не помогать активно, то они ни черта доказать (и как следствие, оптимизировать) не смогут.
Я пытаюсь подкреплять своё понимание ссылками на стандарт, иначе разговор неконструктивен. Если unspecified может себя вести как ни попадя, тогда и impementation-defined должен себя вести так же, см. различие только в требовании стандарта о документации поведения. И при этом мы говорим про well-formed программы.
UB не путешествует во времени. Просто поведение логических выводов компилятора для программы, допускающей UB, может быть неочевидно для программиста. Компилятор исходит из предпосылки, что UB не может происходить. Из этого следуют ограничения на интервалы допустимых переменных. Из этого следует удаление ненужных кусков кода (таких, как
if false), а за этим могут быть любые сюрпризы.Говоря школьным языком, если мы допустим, что пятый постулат нарушается (см. UB), это не означает, что Евклид (или Лобачевский) воскресли. Это просто означает, что при неверности пятого постулата мы попадаем в рамки неевклидовой геометрии.
Мне кажется, что вы введены в заблуждение схожестью слов unspecified и undefined. Чтобы не быть голословным, давайте я процитирую:
Unspecified ситуация всегда одинаково обрабатывается одной и той же версией компилятора. От implementation defined она отличается только необходимостью документации.
Несогласен с первым пунктом, поскольку в таком сценарии вывод компилятора ломается непредсказуемо, что не согласуется с тем, что поведение op1 определено разработчиками компилятора.
UB по переполнению существует по множеству причин, например, чтобы класть 32 битные инты в 64 битные регистры.
Давайте я выражу ту же самую мысль, но чуть-чуть другими словами.
Компилятор - это переводчик с одного языка на другой, например, в случае си - с с си на ассемблер (оптимизация - это тоже часть перевода). Как и в случае с переводом с одного человеческого языка на другой, мы ни в коем случае не хотим, чтобы переводчик порол отсебятину, мы хотим, чтобы перевод точно соответствовал оригиналу.
К счастью, литературные качества нас не интересуют в случае машинных языков, поэтому есть довольно чёткие критерии эквивалентности кусков кода.
Поэтому переводчик обязан убедиться, что A op1 B и A op2 B дают одинаковые результаты для всех допустимых значений A и B.
Если переполнение разрешено стандартом (опять же, в любой форме, будь то unspecified, impelementation defined или standard-defined), то A и B могут быть любыми целыми числами, и в такой ситуации замена A op1 B на A op2 B недопустима, поскольку результаты двух операций будут отличаться на некоторых наборах A и B.
Если же переполнение UB, то компилятор исходит из предпосылки, что A и B таковы, что выражение A op1 B не переполняется, поскольку программист позаботился об этом. И тогда компилятор имеет полное право произвести замену.
Таким образом, механизм UB развязывает руки компилятору, перекладывая часть ответственности (в частности, по работе с большими числами) с компилятора на программиста, и тем самым ускоряя основную массу программ.
Нет, не подойдёт. Код после оптимизации обязан быть эквивалентным исходному коду, и компилятор эту эквивалентность обязан доказать.
Если переполнение разрешено, пусть и в виде implementation defined/unspecified, то замена на неэквивалентную (в случае переполнения) операцию недопустима.
Я не очень улавливаю вашу мысль. Она в том, что я не понимаю разницы между unspecified и undefined или мы уже о чём-то другом? Сформулируйте точно, пожалуйста.
Моё утверждение: введение концепта UB расширяет возможности оптимизатору, в том числе для работы на большем количестве железок.
Пусть у нас есть две операции op1 и op2 над двумя числами A и B. Вот я в коде пишу C = A op1 B. Оптимизатор компилятора хочет заменить эту инструкцию на другую, более дешёвую C = A op2 B. Но предположим, что такая замена эквиалентна только при условии непереполнения A op1 B. Если переполнение undefined, то компилятор имеет право сделать замену, поскольку это забота программиста не допустить UB. Если же переполнение unspecified, то замену делать нельзя.
Так. Давайте по порядку. Unspecified behavior это то же самое, что implementation defined, то есть, оно хорошо определено и работает всегда одинаково, но разработчики компилятора (выделение важно́) не обязаны документировать поведение (в отличие от implementation-defined).
Undefined же не имеет вообще никаких ограничений по поводу того, что случится. И да, в том числе «запустить ядерные ракеты». Для алгебраических упрощений это может быть важным, поскольку компилятор не обязан гарантировать результат работы конкретной машины. То есть, конкретная машина может работать с дополнительным кодом, а может и нет.
Компилятор же исходит из предположения, что программист умный и внимательный, и не допускает появления UB. Что позволяет доказать корректность преобразований его оптимизатора.
Таким образом, я не думаю, что я путаю unspecified и undefined, ваше обоснование меня не убедило.